summaryrefslogtreecommitdiff
path: root/src/LlbcAst.ml
diff options
context:
space:
mode:
authorSidney Congard2022-07-18 16:27:00 +0200
committerSidney Congard2022-07-18 16:27:23 +0200
commitf9b324be57708e9496ca6e9ac0b7e68ffd9e7108 (patch)
treef81bdfe1ddad63938df046ca361dcba2dfea6683 /src/LlbcAst.ml
parent8f14d69ae6683e58e1387ffe38ca3612e0530465 (diff)
Address much stuff of the PR, throw exceptions at remaining places
Diffstat (limited to 'src/LlbcAst.ml')
-rw-r--r--src/LlbcAst.ml21
1 files changed, 9 insertions, 12 deletions
diff --git a/src/LlbcAst.ml b/src/LlbcAst.ml
index 16733e20..aa9b0665 100644
--- a/src/LlbcAst.ml
+++ b/src/LlbcAst.ml
@@ -7,17 +7,6 @@ open Identifiers
module FunDeclId = IdGen ()
module GlobalDeclId = IdGen ()
-(* Strict type for the number of function declarations (see [global_to_fun_id] below) *)
-type global_id_converter = { fun_count : int }
-[@@deriving show]
-
-(** Converts a global id to its corresponding function id.
- To do so, it adds the global id to the number of function declarations :
- We have the bijection `global_id <=> fun_id + fun_id_count`.
-*)
-let global_to_fun_id (conv : global_id_converter) (gid : GlobalDeclId.id) : FunDeclId.id =
- FunDeclId.of_int ((GlobalDeclId.to_int gid) + conv.fun_count)
-
type var = {
index : VarId.id; (** Unique variable identifier *)
name : string option;
@@ -201,6 +190,14 @@ type fun_decl = {
name : fun_name;
signature : fun_sig;
body : fun_body option;
- is_global : bool;
+ is_global_body : bool;
+}
+[@@deriving show]
+
+type global_decl = {
+ def_id : GlobalDeclId.id;
+ body_id: FunDeclId.id;
+ name : global_name;
+ ty: ety;
}
[@@deriving show]