diff options
author | Son HO | 2024-03-18 07:23:00 +0100 |
---|---|---|
committer | GitHub | 2024-03-18 07:23:00 +0100 |
commit | a24f42ff7f0ae3c2aeb51decb0d0c90d6e50ffac (patch) | |
tree | 7c9e526912d4fcbde4ed2ff4c17988fd5c89c96e /compiler/Pure.ml | |
parent | d56946242859e0d375c1d44585b9da6d5fbe94cb (diff) | |
parent | 9e230d0c4378b5c992c820cc1f4322896f739095 (diff) |
Merge pull request #92 from AeneasVerif/son/globals
Add generics to constants/globals
Diffstat (limited to 'compiler/Pure.ml')
-rw-r--r-- | compiler/Pure.ml | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/compiler/Pure.ml b/compiler/Pure.ml index a735667e..cf6710aa 100644 --- a/compiler/Pure.ml +++ b/compiler/Pure.ml @@ -1087,6 +1087,26 @@ type fun_decl = { } [@@deriving show] +type global_decl = { + meta : meta; + def_id : GlobalDeclId.id; + is_local : bool; + llbc_name : llbc_name; (** The original LLBC name. *) + name : string; + (** We use the name only for printing purposes (for debugging): + the name used at extraction time will be derived from the + llbc_name. + *) + llbc_generics : Types.generic_params; + (** See the comment for [llbc_generics] in fun_decl. *) + generics : generic_params; + preds : predicates; + ty : ty; + kind : item_kind; + body_id : FunDeclId.id; +} +[@@deriving show] + type trait_decl = { def_id : trait_decl_id; is_local : bool; |