summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--compiler/Contexts.ml2
-rw-r--r--compiler/Driver.ml21
-rw-r--r--compiler/Extract.ml40
-rw-r--r--compiler/ExtractTypes.ml155
-rw-r--r--compiler/FunsAnalysis.ml4
-rw-r--r--compiler/Print.ml1
-rw-r--r--compiler/Pure.ml1
-rw-r--r--compiler/PureMicroPasses.ml29
-rw-r--r--compiler/SymbolicToPure.ml6
-rw-r--r--compiler/Translate.ml159
-rw-r--r--compiler/TranslateCore.ml3
-rw-r--r--compiler/TypesAnalysis.ml2
12 files changed, 244 insertions, 179 deletions
diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 41c84141..a2ae4f16 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -525,7 +525,7 @@ let ctx_set_abs_can_end (ctx : eval_ctx) (abs_id : AbstractionId.id)
let ctx_type_decl_is_rec (ctx : eval_ctx) (id : TypeDeclId.id) : bool =
let decl_group = TypeDeclId.Map.find id ctx.type_context.type_decls_groups in
- match decl_group with Rec _ -> true | NonRec _ -> false
+ match decl_group with RecGroup _ -> true | NonRecGroup _ -> false
(** Visitor to iterate over the values in the *current* frame *)
class ['self] iter_frame =
diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index aa293469..94e50a08 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -1,15 +1,10 @@
open Aeneas.LlbcOfJson
open Aeneas.Logging
-module T = Aeneas.Types
-module A = Aeneas.LlbcAst
-module I = Aeneas.Interpreter
+open Aeneas.LlbcAst
+open Aeneas.Interpreter
module EL = Easy_logging.Logging
-module TA = Aeneas.TypesAnalysis
-module Micro = Aeneas.PureMicroPasses
-module Print = Aeneas.Print
-module PrePasses = Aeneas.PrePasses
-module Translate = Aeneas.Translate
open Aeneas.Config
+open Aeneas
(** The local logger *)
let log = main_log
@@ -227,7 +222,9 @@ let () =
if
!backend = Lean && !extract_decreases_clauses
&& List.exists
- (function Aeneas.LlbcAst.Fun (Rec (_ :: _)) -> true | _ -> false)
+ (function
+ | Aeneas.LlbcAst.FunGroup (RecGroup (_ :: _)) -> true
+ | _ -> false)
m.declarations
then (
log#error
@@ -237,15 +234,15 @@ let () =
fail ());
(* Apply the pre-passes *)
- let m = PrePasses.apply_passes m in
+ let m = Aeneas.PrePasses.apply_passes m in
(* Some options for the execution *)
(* Test the unit functions with the concrete interpreter *)
- if !test_unit_functions then I.Test.test_unit_functions m;
+ if !test_unit_functions then Test.test_unit_functions m;
(* Translate the functions *)
- Translate.translate_crate filename dest_dir m;
+ Aeneas.Translate.translate_crate filename dest_dir m;
(* Print total elapsed time *)
log#linfo
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 04f6c2c3..cd62c15c 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -27,7 +27,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx)
let builtin =
let open ExtractBuiltin in
let funs_map = builtin_funs_map () in
- let sname = name_to_simple_name def.fwd.f.basename in
+ let sname = name_to_simple_name def.fwd.f.llbc_name in
SimpleNameMap.find_opt sname funs_map
in
(* Use the builtin names if necessary *)
@@ -65,7 +65,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx)
raise
(Failure
("Not found: "
- ^ Names.name_to_string f.basename
+ ^ name_to_string ctx f.llbc_name
^ ", "
^ Print.option_to_string Pure.show_loop_id f.loop_id
^ Print.option_to_string Pure.show_region_group_id
@@ -212,7 +212,7 @@ let fun_builtin_filter_types (id : FunDeclId.id) (types : 'a list)
let decl = FunDeclId.Map.find id ctx.trans_funs in
let err =
"Ill-formed builtin information for function "
- ^ Names.name_to_string decl.fwd.f.basename
+ ^ name_to_string ctx decl.fwd.f.llbc_name
^ ": "
^ string_of_int (List.length filter)
^ " filtering arguments provided for "
@@ -1137,7 +1137,7 @@ let extract_template_fstar_decreases_clause (ctx : extraction_ctx)
F.pp_print_break fmt 0 0;
(* Print a comment to link the extracted type to its original rust definition *)
extract_comment fmt
- [ "[" ^ Print.fun_name_to_string def.basename ^ "]: decreases clause" ];
+ [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases clause" ];
F.pp_print_space fmt ();
(* Open a box for the definition, so that whenever possible it gets printed on
* one line *)
@@ -1199,7 +1199,7 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
F.pp_print_break fmt 0 0;
(* Print a comment to link the extracted type to its original rust definition *)
extract_comment fmt
- [ "[" ^ Print.fun_name_to_string def.basename ^ "]: termination measure" ];
+ [ "[" ^ name_to_string ctx def.llbc_name ^ "]: termination measure" ];
F.pp_print_space fmt ();
(* Open a box for the definition, so that whenever possible it gets printed on
* one line *)
@@ -1253,7 +1253,7 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
(* syntax <def_name> term ... term : tactic *)
F.pp_print_break fmt 0 0;
extract_comment fmt
- [ "[" ^ Print.fun_name_to_string def.basename ^ "]: decreases_by tactic" ];
+ [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases_by tactic" ];
F.pp_print_space fmt ();
F.pp_open_hvbox fmt 0;
F.pp_print_string fmt "syntax \"";
@@ -1289,7 +1289,7 @@ let extract_fun_comment (ctx : extraction_ctx) (fmt : F.formatter)
(Pure.FunId (FRegular def.def_id), def.loop_id, def.back_id)
ctx.fun_name_info
in
- let comment_pre = "[" ^ Print.fun_name_to_string def.basename ^ "]: " in
+ let comment_pre = "[" ^ name_to_string ctx def.llbc_name ^ "]: " in
let comment =
let loop_comment =
match def.loop_id with
@@ -1766,13 +1766,13 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
(* Add a break then the name of the corresponding LLBC declaration *)
F.pp_print_break fmt 0 0;
- extract_comment fmt [ "[" ^ Print.global_name_to_string global.name ^ "]" ];
+ extract_comment fmt [ "[" ^ name_to_string ctx global.name ^ "]" ];
F.pp_print_space fmt ();
let decl_name = ctx_get_global global.def_id ctx in
let body_name =
ctx_get_function
- (FromLlbc (Pure.FunId (FRegular global.body_id), None, None))
+ (FromLlbc (Pure.FunId (FRegular global.body), None, None))
ctx
in
@@ -1958,8 +1958,10 @@ let extract_trait_decl_method_names (ctx : extraction_ctx)
=
(* We do something special to reuse the [ctx_compute_fun_decl]
function. TODO: make it cleaner. *)
- let basename : name = [ Ident item_name ] in
- let f = { f with basename } in
+ let llbc_name : Types.name =
+ [ Types.PeIdent (item_name, Disambiguator.zero) ]
+ in
+ let f = { f with llbc_name } in
let trans = A.FunDeclId.Map.find f.def_id ctx.trans_funs in
let name = ctx_compute_fun_name trans f ctx in
(* Add a prefix if necessary *)
@@ -1991,7 +1993,7 @@ let extract_trait_decl_method_names (ctx : extraction_ctx)
| None ->
let err =
"Ill-formed builtin information for trait decl \""
- ^ Names.name_to_string trait_decl.name
+ ^ name_to_string ctx trait_decl.llbc_name
^ "\", method \"" ^ item_name
^ "\": could not find name for region "
^ Print.option_to_string Pure.show_region_group_id
@@ -2022,7 +2024,7 @@ let extract_trait_decl_register_names (ctx : extraction_ctx)
(trait_decl : trait_decl) : extraction_ctx =
(* Lookup the information if this is a builtin trait *)
let open ExtractBuiltin in
- let sname = name_to_simple_name trait_decl.name in
+ let sname = name_to_simple_name trait_decl.llbc_name in
let builtin_info =
SimpleNameMap.find_opt sname (builtin_trait_decls_map ())
in
@@ -2059,8 +2061,8 @@ let extract_trait_impl_register_names (ctx : extraction_ctx)
(* Check if the trait implementation is builtin *)
let builtin_info =
let open ExtractBuiltin in
- let type_sname = name_to_simple_name trait_impl.name in
- let trait_sname = name_to_simple_name trait_decl.name in
+ let type_sname = name_to_simple_name trait_impl.llbc_name in
+ let trait_sname = name_to_simple_name trait_decl.llbc_name in
SimpleNamePairMap.find_opt (type_sname, trait_sname)
(builtin_trait_impls_map ())
in
@@ -2185,7 +2187,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_break fmt 0 0;
(* Print a comment to link the extracted type to its original rust definition *)
extract_comment fmt
- [ "Trait declaration: [" ^ Print.name_to_string decl.name ^ "]" ];
+ [ "Trait declaration: [" ^ name_to_string ctx decl.llbc_name ^ "]" ];
F.pp_print_break fmt 0 0;
(* Open two outer boxes for the definition, so that whenever possible it gets printed on
one line and indents are correct.
@@ -2466,14 +2468,14 @@ let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
(** Extract a trait implementation *)
let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
(impl : trait_impl) : unit =
- log#ldebug (lazy ("extract_trait_impl: " ^ Names.name_to_string impl.name));
+ log#ldebug (lazy ("extract_trait_impl: " ^ name_to_string ctx impl.llbc_name));
(* Retrieve the impl name *)
let impl_name = ctx_get_trait_impl impl.def_id ctx in
(* Add a break before *)
F.pp_print_break fmt 0 0;
(* Print a comment to link the extracted type to its original rust definition *)
extract_comment fmt
- [ "Trait implementation: [" ^ Print.name_to_string impl.name ^ "]" ];
+ [ "Trait implementation: [" ^ name_to_string ctx impl.llbc_name ^ "]" ];
F.pp_print_break fmt 0 0;
(* Open two outer boxes for the definition, so that whenever possible it gets printed on
@@ -2640,7 +2642,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_break fmt 0 0;
(* Print a comment *)
extract_comment fmt
- [ "Unit test for [" ^ Print.fun_name_to_string def.basename ^ "]" ];
+ [ "Unit test for [" ^ name_to_string ctx def.llbc_name ^ "]" ];
F.pp_print_space fmt ();
(* Open a box for the test *)
F.pp_open_hovbox fmt ctx.indent_incr;
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 553d5863..e4617d2c 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -309,7 +309,6 @@ let assumed_llbc_functions () :
(SliceIndexShared, None, "slice_index_usize");
(SliceIndexMut, None, "slice_index_usize");
(SliceIndexMut, rg0, "slice_update_usize");
- (SliceLen, None, "slice_len");
]
| Lean ->
[
@@ -323,7 +322,6 @@ let assumed_llbc_functions () :
(SliceIndexShared, None, "Slice.index_usize");
(SliceIndexMut, None, "Slice.index_usize");
(SliceIndexMut, rg0, "Slice.update_usize");
- (SliceLen, None, "Slice.len");
]
let assumed_pure_functions () : (pure_assumed_fun_id * string) list =
@@ -538,6 +536,11 @@ let type_keyword () =
| Coq | Lean -> "Type"
| HOL4 -> raise (Failure "Unexpected")
+let name_last_elem_as_ident (n : llbc_name) : string =
+ match Collections.List.last n with
+ | PeIdent (s, _) -> s
+ | PeImpl _ -> raise (Failure "Unexpected")
+
(**
[ctx]: we use the context to lookup type definitions, to retrieve type names.
This is used to compute variable names, when they have no basenames: in this
@@ -579,34 +582,90 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
let int_name = int_name in
(* Prepare a name.
- * The first id elem is always the crate: if it is the local crate,
- * we remove it.
- * We also remove all the disambiguators, then convert everything to strings.
- * **Rmk:** because we remove the disambiguators, there may be name collisions
- * (which is ok, because we check for name collisions and fail if there is any).
- *)
- let get_name (name : name) : string list =
+ The first id elem is always the crate: if it is the local crate,
+ we remove it. We ignore disambiguators (there may be collisions, but we
+ check if there are).
+ *)
+ let rec name_to_simple_name (name : llbc_name) : string list =
(* Rmk.: initially we only filtered the disambiguators equal to 0 *)
- let name = Names.filter_disambiguators name in
match name with
- | Ident crate :: name ->
- let name = if crate = crate_name then name else Ident crate :: name in
+ | (PeIdent (crate, _) as id) :: name ->
+ let name = if crate = crate_name then name else id :: name in
+ let open Types in
let name =
List.map
(function
- | Names.Ident s -> s
- | Disambiguator d -> Names.Disambiguator.to_string d)
+ | PeIdent (s, _) -> s
+ | PeImpl impl -> impl_elem_to_simple_name impl)
name
in
name
| _ ->
- raise (Failure ("Unexpected name shape: " ^ Print.name_to_string name))
+ raise
+ (Failure
+ ("Unexpected name shape: " ^ TranslateCore.name_to_string ctx name))
+ and impl_elem_to_simple_name (impl : Types.impl_elem) : string =
+ (* We do something simple for now.
+ TODO: we might want to do something different for impl elements which are
+ actually trait implementations, in order to prevent name collisions (it
+ is possible to define several times the same trait for the same type,
+ but with different instantiations of the type, or different trait
+ requirements *)
+ ty_to_simple_name impl.generics impl.ty
+ and ty_to_simple_name (generics : Types.generic_params) (ty : Types.ty) :
+ string =
+ (* We do something simple for now.
+ TODO: find a more principled way of converting types to names.
+ In particular, we might want to do something different for impl elements which are
+ actually trait implementations, in order to prevent name collisions (it
+ is possible to define several times the same trait for the same type,
+ but with different instantiations of the type, or different trait
+ requirements *)
+ match ty with
+ | TAdt (id, args) -> (
+ match id with
+ | TAdtId id ->
+ let def = TypeDeclId.Map.find id ctx.type_ctx.type_decls in
+ name_last_elem_as_ident def.name
+ | TTuple ->
+ (* TODO *)
+ "Tuple"
+ ^ String.concat ""
+ (List.map (ty_to_simple_name generics) args.types)
+ | TAssumed id -> Types.show_assumed_ty id)
+ | TVar vid ->
+ (* Use the variable name *)
+ (List.find (fun (v : type_var) -> v.index = vid) generics.types).name
+ | TLiteral lty ->
+ StringUtils.capitalize_first_letter
+ (Print.Types.literal_type_to_string lty)
+ | TNever -> raise (Failure "Unreachable")
+ | TRef (_, rty, rk) -> (
+ let rty = ty_to_simple_name generics rty in
+ match rk with
+ | RMut -> "MutBorrow" ^ rty
+ | RShared -> "SharedBorrow" ^ rty)
+ | TRawPtr (rty, rk) -> (
+ let rty = ty_to_simple_name generics rty in
+ match rk with RMut -> "MutPtr" ^ rty | RShared -> "ConstPtr" ^ rty)
+ | TTraitType (tr, _, name) ->
+ (* TODO: this is way too simple *)
+ let trait_decl =
+ TraitDeclId.Map.find tr.trait_decl_ref.trait_decl_id
+ ctx.trait_decls_ctx.trait_decls
+ in
+ name_last_elem_as_ident trait_decl.name ^ name
+ | TArrow (inputs, output) ->
+ "Arrow"
+ ^ String.concat ""
+ (List.map (ty_to_simple_name generics) (inputs @ [ output ]))
in
let flatten_name (name : string list) : string =
match !backend with
| FStar | Coq | HOL4 -> String.concat "_" name
| Lean -> String.concat "." name
in
+ let get_name name : string list = name_to_simple_name name in
let get_type_name = get_name in
let get_type_name_no_suffix name =
match !backend with
@@ -620,7 +679,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
| Coq | HOL4 -> get_type_name_no_suffix name ^ "_t"
| Lean -> get_type_name_no_suffix name
in
- let field_name (def_name : name) (field_id : FieldId.id)
+ let field_name (def_name : llbc_name) (field_id : FieldId.id)
(field_name : string option) : string =
let field_name_s =
match field_name with
@@ -639,7 +698,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
| Lean | HOL4 -> def_name
| Coq | FStar -> StringUtils.lowercase_first_letter def_name
in
- let variant_name (def_name : name) (variant : string) : string =
+ let variant_name (def_name : llbc_name) (variant : string) : string =
match !backend with
| FStar | Coq | HOL4 ->
let variant = to_camel_case variant in
@@ -649,7 +708,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
else variant
| Lean -> variant
in
- let struct_constructor (basename : name) : string =
+ let struct_constructor (basename : llbc_name) : string =
let tname = type_name basename in
ExtractBuiltin.mk_struct_constructor tname
in
@@ -661,15 +720,15 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
| FStar | Coq | HOL4 -> StringUtils.lowercase_first_letter fname
| Lean -> fname
in
- let global_name (name : global_name) : string =
+ let global_name (name : llbc_name) : string =
(* Converting to snake case also lowercases the letters (in Rust, global
* names are written in capital letters). *)
let parts = List.map to_snake_case (get_name name) in
String.concat "_" parts
in
- let fun_name (fname : fun_name) (num_loops : int) (loop_id : LoopId.id option)
- (num_rgs : int) (rg : region_group_info option) (filter_info : bool * int)
- : string =
+ let fun_name (fname : llbc_name) (num_loops : int)
+ (loop_id : LoopId.id option) (num_rgs : int)
+ (rg : region_group_info option) (filter_info : bool * int) : string =
let fname = get_fun_name fname in
(* Compute the suffix *)
let suffix = default_fun_suffix num_loops loop_id num_rgs rg filter_info in
@@ -678,7 +737,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
in
let trait_decl_name (trait_decl : trait_decl) : string =
- type_name trait_decl.name
+ type_name trait_decl.llbc_name
in
let trait_impl_name (trait_decl : trait_decl) (trait_impl : trait_impl) :
@@ -686,12 +745,14 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
(* TODO: provisional: we concatenate the trait impl name (which is its type)
with the trait decl name *)
let trait_decl =
- let name = trait_decl.name in
+ let name = trait_decl.llbc_name in
let name = get_type_name_no_suffix name ^ "Inst" in
(* Remove the occurrences of '.' *)
String.concat "" (String.split_on_char '.' name)
in
- let name = flatten_name (get_type_name trait_impl.name @ [ trait_decl ]) in
+ let name =
+ flatten_name (get_type_name trait_impl.llbc_name @ [ trait_decl ])
+ in
match !backend with
| FStar -> StringUtils.lowercase_first_letter name
| Coq | HOL4 | Lean -> name
@@ -745,7 +806,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
^ TraitClauseId.to_string clause.clause_id
in
- let termination_measure_name (_fid : A.FunDeclId.id) (fname : fun_name)
+ let termination_measure_name (_fid : A.FunDeclId.id) (fname : llbc_name)
(num_loops : int) (loop_id : LoopId.id option) : string =
let fname = get_fun_name fname in
let lp_suffix = default_fun_loop_suffix num_loops loop_id in
@@ -760,7 +821,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
fname ^ lp_suffix ^ suffix
in
- let decreases_proof_name (_fid : A.FunDeclId.id) (fname : fun_name)
+ let decreases_proof_name (_fid : A.FunDeclId.id) (fname : llbc_name)
(num_loops : int) (loop_id : LoopId.id option) : string =
let fname = get_fun_name fname in
let lp_suffix = default_fun_loop_suffix num_loops loop_id in
@@ -815,12 +876,12 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
| TAdtId adt_id ->
let def = TypeDeclId.Map.find adt_id ctx.type_ctx.type_decls in
(* Derive the var name from the last ident of the type name
- * Ex.: ["hashmap"; "HashMap"] ~~> "HashMap" -> "hash_map" -> "hm"
- *)
+ Ex.: ["hashmap"; "HashMap"] ~~> "HashMap" -> "hash_map" -> "hm"
+ *)
(* The name shouldn't be empty, and its last element should
* be an ident *)
- let cl = List.nth def.name (List.length def.name - 1) in
- name_from_type_ident (Names.as_ident cl))
+ let cl = Collections.List.last def.name in
+ name_from_type_ident (TypesUtils.as_ident cl))
| TVar _ -> (
(* TODO: use "t" also for F* *)
match !backend with
@@ -866,31 +927,31 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
match cv with
| VScalar sv -> (
match !backend with
- | FStar -> F.pp_print_string fmt (Z.to_string sv.PV.value)
+ | FStar -> F.pp_print_string fmt (Z.to_string sv.value)
| Coq | HOL4 | Lean ->
let print_brackets = inside && !backend = HOL4 in
if print_brackets then F.pp_print_string fmt "(";
(match !backend with
| Coq | Lean -> ()
| HOL4 ->
- F.pp_print_string fmt ("int_to_" ^ int_name sv.PV.int_ty);
+ F.pp_print_string fmt ("int_to_" ^ int_name sv.int_ty);
F.pp_print_space fmt ()
| _ -> raise (Failure "Unreachable"));
(* We need to add parentheses if the value is negative *)
- if sv.PV.value >= Z.of_int 0 then
- F.pp_print_string fmt (Z.to_string sv.PV.value)
+ if sv.value >= Z.of_int 0 then
+ F.pp_print_string fmt (Z.to_string sv.value)
else if !backend = Lean then
(* TODO: parsing issues with Lean because there are ambiguous
interpretations between int values and nat values *)
F.pp_print_string fmt
- ("(-(" ^ Z.to_string (Z.neg sv.PV.value) ^ ":Int))")
- else F.pp_print_string fmt ("(" ^ Z.to_string sv.PV.value ^ ")");
+ ("(-(" ^ Z.to_string (Z.neg sv.value) ^ ":Int))")
+ else F.pp_print_string fmt ("(" ^ Z.to_string sv.value ^ ")");
(match !backend with
| Coq ->
- let iname = int_name sv.PV.int_ty in
+ let iname = int_name sv.int_ty in
F.pp_print_string fmt ("%" ^ iname)
| Lean ->
- let iname = String.lowercase_ascii (int_name sv.PV.int_ty) in
+ let iname = String.lowercase_ascii (int_name sv.int_ty) in
F.pp_print_string fmt ("#" ^ iname)
| HOL4 -> ()
| _ -> raise (Failure "Unreachable"));
@@ -1426,7 +1487,7 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
extraction_ctx =
(* Lookup the builtin information, if there is *)
let open ExtractBuiltin in
- let sname = name_to_simple_name def.name in
+ let sname = name_to_simple_name def.llbc_name in
let info = SimpleNameMap.find_opt sname (builtin_types_map ()) in
(* Register the filtering information, if there is *)
let ctx =
@@ -1442,7 +1503,7 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
(* Compute and register the type def name *)
let def_name =
match info with
- | None -> ctx.fmt.type_name def.name
+ | None -> ctx.fmt.type_name def.llbc_name
| Some info -> info.extract_name
in
let ctx = ctx_add (TypeId (TAdtId def.def_id)) def_name ctx in
@@ -1460,10 +1521,10 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
let field_names =
FieldId.mapi
(fun fid (field : field) ->
- (fid, ctx.fmt.field_name def.name fid field.field_name))
+ (fid, ctx.fmt.field_name def.llbc_name fid field.field_name))
fields
in
- let cons_name = ctx.fmt.struct_constructor def.name in
+ let cons_name = ctx.fmt.struct_constructor def.llbc_name in
(field_names, cons_name)
| Some { body_info = Some (Struct (cons_name, field_names)); _ } ->
let field_names =
@@ -1499,12 +1560,12 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
VariantId.mapi
(fun variant_id (variant : variant) ->
let name =
- ctx.fmt.variant_name def.name variant.variant_name
+ ctx.fmt.variant_name def.llbc_name variant.variant_name
in
(* Add the type name prefix for Lean *)
let name =
if !Config.backend = Lean then
- let type_name = ctx.fmt.type_name def.name in
+ let type_name = ctx.fmt.type_name def.llbc_name in
type_name ^ "." ^ name
else name
in
@@ -1648,7 +1709,7 @@ let extract_type_decl_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
let print_variant _variant_id (v : variant) =
(* We don't lookup the name, because it may have a prefix for the type
id (in the case of Lean) *)
- let cons_name = ctx.fmt.variant_name def.name v.variant_name in
+ let cons_name = ctx.fmt.variant_name def.llbc_name v.variant_name in
let fields = v.fields in
extract_type_decl_variant ctx fmt type_decl_group def_name type_params
cg_params cons_name fields
@@ -2030,7 +2091,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
if !backend <> HOL4 || not (decl_is_first_from_group kind) then
F.pp_print_break fmt 0 0;
(* Print a comment to link the extracted type to its original rust definition *)
- extract_comment fmt [ "[" ^ Print.name_to_string def.name ^ "]" ];
+ extract_comment fmt [ "[" ^ name_to_string ctx def.llbc_name ^ "]" ];
F.pp_print_break fmt 0 0;
(* Open a box for the definition, so that whenever possible it gets printed on
* one line. Note however that in the case of Lean line breaks are important
diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml
index 57aa9e12..a07ad35a 100644
--- a/compiler/FunsAnalysis.ml
+++ b/compiler/FunsAnalysis.ml
@@ -164,7 +164,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
let analyze_fun_decl_group (d : fun_declaration_group) : unit =
(* Retrieve the function declarations *)
- let funs = match d with NonRec id -> [ id ] | Rec ids -> ids in
+ let funs = match d with NonRecGroup id -> [ id ] | RecGroup ids -> ids in
let funs = List.map (fun id -> FunDeclId.Map.find id funs_map) funs in
let fun_ids = List.map (fun (d : fun_decl) -> d.def_id) funs in
let fun_ids = FunDeclId.Set.of_list fun_ids in
@@ -183,7 +183,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
| GlobalGroup id :: decls' ->
(* Analyze a global by analyzing its body function *)
let global = GlobalDeclId.Map.find id globals_map in
- analyze_fun_decl_group (NonRec global.body);
+ analyze_fun_decl_group (NonRecGroup global.body);
analyze_decl_groups decls'
in
diff --git a/compiler/Print.ml b/compiler/Print.ml
index cd83a589..48a5a20b 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -1,6 +1,5 @@
include Charon.PrintUtils
include Charon.PrintLlbcAst
-open Charon.PrintPrimitiveValues
open Charon.PrintTypes
open Charon.PrintExpressions
open Charon.PrintLlbcAst.Ast
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index fa059499..40711e53 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -14,6 +14,7 @@ module GlobalDeclId = A.GlobalDeclId
module TraitDeclId = T.TraitDeclId
module TraitImplId = T.TraitImplId
module TraitClauseId = T.TraitClauseId
+module Disambiguator = T.Disambiguator
(** We redefine identifiers for loop: in {!Values}, the identifiers are global
(they monotonically increase across functions) while in {!module:Pure} we want
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index d2747a4b..2106c206 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -3,10 +3,13 @@
open Pure
open PureUtils
open TranslateCore
-module V = Values
(** The local logger *)
-let log = L.pure_micro_passes_log
+let log = Logging.pure_micro_passes_log
+
+let fun_decl_to_string (ctx : trans_ctx) (def : Pure.fun_decl) : string =
+ let fmt = trans_ctx_to_pure_fmt_env ctx in
+ PrintPure.fun_decl_to_string fmt def
(** Small utility.
@@ -597,8 +600,8 @@ let intro_struct_updates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
match
TypeDeclId.Map.find adt_id ctx.type_ctx.type_decls_groups
with
- | NonRec _ -> false
- | Rec _ -> true
+ | NonRecGroup _ -> false
+ | RecGroup _ -> true
in
(* Convert, if possible - note that for now for Lean and Coq
we don't support the structure syntax on recursive structures *)
@@ -1420,14 +1423,15 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list =
let loop_body = { inputs; inputs_lvs; body = loop_body } in
- let loop_def =
+ let loop_def : fun_decl =
{
def_id = def.def_id;
kind = def.kind;
num_loops;
loop_id = Some loop.loop_id;
back_id = def.back_id;
- basename = def.basename;
+ llbc_name = def.llbc_name;
+ name = def.name;
signature = loop_sig;
is_global_decl_body = def.is_global_decl_body;
body = Some loop_body;
@@ -1539,10 +1543,12 @@ let eliminate_box_functions (ctx : trans_ctx) (def : fun_decl) : fun_decl =
mk_unit_rvalue
| ( ( SliceIndexShared | SliceIndexMut | ArrayIndexShared
| ArrayIndexMut | ArrayToSliceShared | ArrayToSliceMut
- | ArrayRepeat | SliceLen ),
+ | ArrayRepeat ),
_ ) ->
super#visit_texpression env e)
- | Fun (FromLlbc (FunId (FRegular fid), _lp_id, rg_id)) -> (
+ | Fun (FromLlbc (FunId (FRegular fid), _lp_id, rg_id)) ->
+ failwith "TODO"
+ (*
(* Lookup the function name *)
let def = FunDeclId.Map.find fid ctx.fun_ctx.fun_decls in
match
@@ -1570,7 +1576,8 @@ let eliminate_box_functions (ctx : trans_ctx) (def : fun_decl) : fun_decl =
| _ -> raise (Failure "Unreachable")
in
mk_apps arg args
- | _ -> super#visit_texpression env e)
+ | _ -> super#visit_texpression env e
+ *)
| _ -> super#visit_texpression env e)
| _ -> super#visit_texpression env e
end
@@ -1918,9 +1925,7 @@ let apply_passes_to_def (ctx : trans_ctx) (def : fun_decl) :
(* Debug *)
log#ldebug
(lazy
- ("PureMicroPasses.apply_passes_to_def: "
- ^ Print.fun_name_to_string def.basename
- ^ " ("
+ ("PureMicroPasses.apply_passes_to_def: " ^ def.name ^ " ("
^ Print.option_to_string T.RegionGroupId.to_string def.back_id
^ ")"));
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 2460e040..4e12d31e 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -3036,9 +3036,9 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
(* return *)
def
-let translate_type_decls (ctx : Contexts.decls_ctx)
- (type_decls : T.type_decl list) : type_decl list =
- List.map (translate_type_decl ctx) type_decls
+let translate_type_decls (ctx : Contexts.decls_ctx) : type_decl list =
+ List.map (translate_type_decl ctx)
+ (TypeDeclId.Map.values ctx.type_ctx.type_decls)
(** Translates function signatures.
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 2aedb544..cf23fd44 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -1,11 +1,11 @@
-open InterpreterStatements
open Interpreter
-module L = Logging
-module T = Types
-module A = LlbcAst
+open Expressions
+open Types
+open Values
+open LlbcAst
+open Contexts
module SA = SymbolicAst
module Micro = PureMicroPasses
-module C = Contexts
open PureUtils
open TranslateCore
@@ -16,18 +16,17 @@ let log = TranslateCore.log
- the list of symbolic values used for the input values
- the generated symbolic AST
*)
-type symbolic_fun_translation = V.symbolic_value list * SA.expression
+type symbolic_fun_translation = symbolic_value list * SA.expression
(** Execute the symbolic interpreter on a function to generate a list of symbolic ASTs,
for the forward function and the backward functions.
*)
-let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : A.fun_decl)
- : symbolic_fun_translation option =
+let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : fun_decl) :
+ symbolic_fun_translation option =
(* Debug *)
log#ldebug
(lazy
- ("translate_function_to_symbolics: "
- ^ Print.fun_name_to_string fdef.A.name));
+ ("translate_function_to_symbolics: " ^ name_to_string trans_ctx fdef.name));
match fdef.body with
| None -> None
@@ -45,12 +44,11 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : A.fun_decl)
*)
let translate_function_to_pure (trans_ctx : trans_ctx)
(fun_sigs : SymbolicToPure.fun_sig_named_outputs RegularFunIdNotLoopMap.t)
- (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) (fdef : A.fun_decl)
- : pure_fun_translation_no_loops =
+ (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) (fdef : fun_decl) :
+ pure_fun_translation_no_loops =
(* Debug *)
log#ldebug
- (lazy
- ("translate_function_to_pure: " ^ Print.fun_name_to_string fdef.A.name));
+ (lazy ("translate_function_to_pure: " ^ name_to_string trans_ctx fdef.name));
let def_id = fdef.def_id in
@@ -61,22 +59,24 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
(* Initialize the context *)
let forward_sig =
- RegularFunIdNotLoopMap.find (E.FRegular def_id, None) fun_sigs
+ RegularFunIdNotLoopMap.find (FRegular def_id, None) fun_sigs
in
- let sv_to_var = V.SymbolicValueId.Map.empty in
+ let sv_to_var = SymbolicValueId.Map.empty in
let var_counter = Pure.VarId.generator_zero in
let state_var, var_counter = Pure.VarId.fresh var_counter in
let back_state_var, var_counter = Pure.VarId.fresh var_counter in
let fuel0, var_counter = Pure.VarId.fresh var_counter in
let fuel, var_counter = Pure.VarId.fresh var_counter in
- let calls = V.FunCallId.Map.empty in
- let abstractions = V.AbstractionId.Map.empty in
+ let calls = FunCallId.Map.empty in
+ let abstractions = AbstractionId.Map.empty in
let recursive_type_decls =
- T.TypeDeclId.Set.of_list
+ TypeDeclId.Set.of_list
(List.filter_map
(fun (tid, g) ->
- match g with Charon.GAst.NonRec _ -> None | Rec _ -> Some tid)
- (T.TypeDeclId.Map.bindings trans_ctx.type_ctx.type_decls_groups))
+ match g with
+ | Charon.GAst.NonRecGroup _ -> None
+ | RecGroup _ -> Some tid)
+ (TypeDeclId.Map.bindings trans_ctx.type_ctx.type_decls_groups))
in
let type_context =
{
@@ -104,9 +104,9 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
*)
let loop_ids_map =
match symbolic_trans with
- | None -> V.LoopId.Map.empty
+ | None -> LoopId.Map.empty
| Some (_, ast) ->
- let m = ref V.LoopId.Map.empty in
+ let m = ref LoopId.Map.empty in
let _, fresh_loop_id = Pure.LoopId.fresh_stateful_generator () in
let visitor =
@@ -115,10 +115,9 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
method! visit_loop env loop =
let _ =
- match V.LoopId.Map.find_opt loop.loop_id !m with
+ match LoopId.Map.find_opt loop.loop_id !m with
| Some _ -> ()
- | None ->
- m := V.LoopId.Map.add loop.loop_id (fresh_loop_id ()) !m
+ | None -> m := LoopId.Map.add loop.loop_id (fresh_loop_id ()) !m
in
super#visit_loop env loop
end
@@ -148,9 +147,9 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
fun_decl = fdef;
forward_inputs = [];
(* Empty for now *)
- backward_inputs = T.RegionGroupId.Map.empty;
+ backward_inputs = RegionGroupId.Map.empty;
(* Empty for now *)
- backward_outputs = T.RegionGroupId.Map.empty;
+ backward_outputs = RegionGroupId.Map.empty;
loop_backward_outputs = None;
(* Empty for now *)
calls;
@@ -171,7 +170,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
| Some body, Some (input_svs, _) ->
let forward_input_vars = LlbcAstUtils.fun_body_get_input_vars body in
let forward_input_varnames =
- List.map (fun (v : A.var) -> v.name) forward_input_vars
+ List.map (fun (v : var) -> v.name) forward_input_vars
in
let input_svs = List.combine forward_input_varnames input_svs in
let ctx, forward_inputs =
@@ -189,7 +188,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
in
(* Translate the backward functions *)
- let translate_backward (rg : T.region_group) : Pure.fun_decl =
+ let translate_backward (rg : region_group) : Pure.fun_decl =
(* For the backward inputs/outputs initialization: we use the fact that
* there are no nested borrows for now, and so that the region groups
* can't have parents *)
@@ -244,10 +243,10 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
SymbolicToPure.fresh_vars backward_outputs ctx
in
let backward_inputs =
- T.RegionGroupId.Map.singleton back_id backward_inputs
+ RegionGroupId.Map.singleton back_id backward_inputs
in
let backward_outputs =
- T.RegionGroupId.Map.singleton back_id backward_outputs
+ RegionGroupId.Map.singleton back_id backward_outputs
in
(* Put everything in the context *)
@@ -274,7 +273,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
(pure_forward, pure_backwards)
(* TODO: factor out the return type *)
-let translate_crate_to_pure (crate : A.crate) :
+let translate_crate_to_pure (crate : crate) :
trans_ctx
* Pure.type_decl list
* pure_fun_translation list
@@ -287,9 +286,7 @@ let translate_crate_to_pure (crate : A.crate) :
let trans_ctx = compute_contexts crate in
(* Translate all the type definitions *)
- let type_decls =
- SymbolicToPure.translate_type_decls (T.TypeDeclId.Map.values crate.types)
- in
+ let type_decls = SymbolicToPure.translate_type_decls trans_ctx in
(* Compute the type definition map *)
let type_decls_map =
@@ -301,24 +298,24 @@ let translate_crate_to_pure (crate : A.crate) :
let assumed_sigs =
List.map
(fun (info : Assumed.assumed_fun_info) ->
- ( E.FAssumed info.fun_id,
+ ( FAssumed info.fun_id,
List.map (fun _ -> None) info.fun_sig.inputs,
info.fun_sig ))
Assumed.assumed_fun_infos
in
let local_sigs =
List.map
- (fun (fdef : A.fun_decl) ->
+ (fun (fdef : fun_decl) ->
let input_names =
match fdef.body with
| None -> List.map (fun _ -> None) fdef.signature.inputs
| Some body ->
List.map
- (fun (v : A.var) -> v.name)
+ (fun (v : var) -> v.name)
(LlbcAstUtils.fun_body_get_input_vars body)
in
- (E.FRegular fdef.def_id, input_names, fdef.signature))
- (A.FunDeclId.Map.values crate.functions)
+ (FRegular fdef.def_id, input_names, fdef.signature))
+ (FunDeclId.Map.values crate.fun_decls)
in
let sigs = List.append assumed_sigs local_sigs in
let fun_sigs = SymbolicToPure.translate_fun_signatures trans_ctx sigs in
@@ -327,22 +324,21 @@ let translate_crate_to_pure (crate : A.crate) :
let pure_translations =
List.map
(translate_function_to_pure trans_ctx fun_sigs type_decls_map)
- (A.FunDeclId.Map.values crate.functions)
+ (FunDeclId.Map.values crate.fun_decls)
in
(* Translate the trait declarations *)
- let type_infos = trans_ctx.type_ctx.type_infos in
let trait_decls =
List.map
- (SymbolicToPure.translate_trait_decl type_infos)
- (T.TraitDeclId.Map.values trans_ctx.trait_decls_ctx.trait_decls)
+ (SymbolicToPure.translate_trait_decl trans_ctx)
+ (TraitDeclId.Map.values trans_ctx.trait_decls_ctx.trait_decls)
in
(* Translate the trait implementations *)
let trait_impls =
List.map
- (SymbolicToPure.translate_trait_impl type_infos)
- (T.TraitImplId.Map.values trans_ctx.trait_impls_ctx.trait_impls)
+ (SymbolicToPure.translate_trait_impl trans_ctx)
+ (TraitImplId.Map.values trans_ctx.trait_impls_ctx.trait_impls)
in
(* Apply the micro-passes *)
@@ -401,9 +397,9 @@ let crate_has_opaque_non_builtin_decls (ctx : gen_ctx) (filter_assumed : bool) :
log#ldebug
(lazy
("Opaque decls:" ^ "\n- types:\n"
- ^ String.concat ",\n" (List.map T.show_type_decl types)
+ ^ String.concat ",\n" (List.map show_type_decl types)
^ "\n- functions:\n"
- ^ String.concat ",\n" (List.map A.show_fun_decl funs)));
+ ^ String.concat ",\n" (List.map show_fun_decl funs)));
(types <> [], funs <> [])
(** Export a type declaration.
@@ -481,7 +477,7 @@ let export_types_group (fmt : Format.formatter) (config : gen_config)
let types_map = builtin_types_map () in
List.map
(fun (def : Pure.type_decl) ->
- let sname = name_to_simple_name def.name in
+ let sname = name_to_simple_name def.llbc_name in
SimpleNameMap.find_opt sname types_map <> None)
defs
in
@@ -531,10 +527,10 @@ let export_types_group (fmt : Format.formatter) (config : gen_config)
TODO: check correct behavior with opaque globals.
*)
let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
- (id : A.GlobalDeclId.id) : unit =
+ (id : GlobalDeclId.id) : unit =
let global_decls = ctx.trans_ctx.global_ctx.global_decls in
- let global = A.GlobalDeclId.Map.find id global_decls in
- let trans = A.FunDeclId.Map.find global.body_id ctx.trans_funs in
+ let global = GlobalDeclId.Map.find id global_decls in
+ let trans = FunDeclId.Map.find global.body ctx.trans_funs in
assert (trans.fwd.loops = []);
assert (trans.backs = []);
let body = trans.fwd.f in
@@ -665,7 +661,7 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
let funs_map = builtin_funs_map () in
List.map
(fun (trans : pure_fun_translation) ->
- let sname = name_to_simple_name trans.fwd.f.basename in
+ let sname = name_to_simple_name trans.fwd.f.llbc_name in
SimpleNameMap.find_opt sname funs_map <> None)
pure_ls
in
@@ -756,10 +752,10 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
let export_trait_decl (fmt : Format.formatter) (_config : gen_config)
(ctx : gen_ctx) (trait_decl_id : Pure.trait_decl_id) (extract_decl : bool)
(extract_extra_info : bool) : unit =
- let trait_decl = T.TraitDeclId.Map.find trait_decl_id ctx.trans_trait_decls in
+ let trait_decl = TraitDeclId.Map.find trait_decl_id ctx.trans_trait_decls in
(* Check if the trait declaration is builtin, in which case we ignore it *)
let open ExtractBuiltin in
- let sname = name_to_simple_name trait_decl.name in
+ let sname = name_to_simple_name trait_decl.llbc_name in
if SimpleNameMap.find_opt sname (builtin_trait_decls_map ()) = None then (
let ctx = { ctx with trait_decl_id = Some trait_decl.def_id } in
if extract_decl then Extract.extract_trait_decl ctx fmt trait_decl;
@@ -771,7 +767,7 @@ let export_trait_decl (fmt : Format.formatter) (_config : gen_config)
let export_trait_impl (fmt : Format.formatter) (_config : gen_config)
(ctx : gen_ctx) (trait_impl_id : Pure.trait_impl_id) : unit =
(* Lookup the definition *)
- let trait_impl = T.TraitImplId.Map.find trait_impl_id ctx.trans_trait_impls in
+ let trait_impl = TraitImplId.Map.find trait_impl_id ctx.trans_trait_impls in
let trait_decl =
Pure.TraitDeclId.Map.find trait_impl.impl_trait.trait_decl_id
ctx.trans_trait_decls
@@ -779,8 +775,8 @@ let export_trait_impl (fmt : Format.formatter) (_config : gen_config)
(* Check if the trait implementation is builtin *)
let builtin_info =
let open ExtractBuiltin in
- let type_sname = name_to_simple_name trait_impl.name in
- let trait_sname = name_to_simple_name trait_decl.name in
+ let type_sname = name_to_simple_name trait_impl.llbc_name in
+ let trait_sname = name_to_simple_name trait_decl.llbc_name in
SimpleNamePairMap.find_opt (type_sname, trait_sname)
(builtin_trait_impls_map ())
in
@@ -817,14 +813,15 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
Extract.extract_state_type fmt ctx kind
in
- let export_decl_group (dg : A.declaration_group) : unit =
+ let export_decl_group (dg : declaration_group) : unit =
match dg with
- | Type (NonRec id) ->
+ | TypeGroup (NonRecGroup id) ->
if config.extract_types then export_types_group false [ id ]
- | Type (Rec ids) -> if config.extract_types then export_types_group true ids
- | Fun (NonRec id) -> (
+ | TypeGroup (RecGroup ids) ->
+ if config.extract_types then export_types_group true ids
+ | FunGroup (NonRecGroup id) -> (
(* Lookup *)
- let pure_fun = A.FunDeclId.Map.find id ctx.trans_funs in
+ let pure_fun = FunDeclId.Map.find id ctx.trans_funs in
(* Special case: we skip trait method *declarations* (we will
extract their type directly in the records we generate for
the trait declarations themselves, there is no point in having
@@ -834,21 +831,21 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
| _ ->
(* Translate *)
export_functions_group [ pure_fun ])
- | Fun (Rec ids) ->
+ | FunGroup (RecGroup ids) ->
(* General case of mutually recursive functions *)
(* Lookup *)
let pure_funs =
- List.map (fun id -> A.FunDeclId.Map.find id ctx.trans_funs) ids
+ List.map (fun id -> FunDeclId.Map.find id ctx.trans_funs) ids
in
(* Translate *)
export_functions_group pure_funs
- | Global id -> export_global id
- | TraitDecl id ->
+ | GlobalGroup id -> export_global id
+ | TraitDeclGroup id ->
(* TODO: update to extract groups *)
if config.extract_trait_decls && config.extract_transparent then (
export_trait_decl_group id;
export_trait_decl_group_extra_info id)
- | TraitImpl id ->
+ | TraitImplGroup id ->
if config.extract_trait_impls && config.extract_transparent then
export_trait_impl id
in
@@ -986,7 +983,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
close_out out
(** Translate a crate and write the synthesized code to an output file. *)
-let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
+let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
unit =
(* Translate the module to the pure AST *)
let trans_ctx, trans_types, trans_funs, trans_trait_decls, trans_trait_impls =
@@ -1036,8 +1033,8 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
Pure.TypeDeclId.Map.of_list
(List.map (fun (d : Pure.type_decl) -> (d.def_id, d)) trans_types)
in
- let trans_funs : pure_fun_translation A.FunDeclId.Map.t =
- A.FunDeclId.Map.of_list
+ let trans_funs : pure_fun_translation FunDeclId.Map.t =
+ FunDeclId.Map.of_list
(List.map
(fun (trans : pure_fun_translation) -> (trans.fwd.f.def_id, trans))
trans_funs)
@@ -1046,13 +1043,13 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
(* Put everything in the context *)
let ctx =
let trans_trait_decls =
- T.TraitDeclId.Map.of_list
+ TraitDeclId.Map.of_list
(List.map
(fun (d : Pure.trait_decl) -> (d.def_id, d))
trans_trait_decls)
in
let trans_trait_impls =
- T.TraitImplId.Map.of_list
+ TraitImplId.Map.of_list
(List.map
(fun (d : Pure.trait_impl) -> (d.def_id, d))
trans_trait_impls)
@@ -1107,12 +1104,12 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
if is_global then ctx
else Extract.extract_fun_decl_register_names ctx gen_decr_clause trans)
ctx
- (A.FunDeclId.Map.values trans_funs)
+ (FunDeclId.Map.values trans_funs)
in
let ctx =
List.fold_left Extract.extract_global_decl_register_names ctx
- (A.GlobalDeclId.Map.values crate.globals)
+ (GlobalDeclId.Map.values crate.global_decls)
in
let ctx =
@@ -1291,7 +1288,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
namespace;
in_namespace = true;
crate_name;
- rust_module_name = crate.A.name;
+ rust_module_name = crate.name;
module_name = types_module;
custom_msg = ": type definitions";
custom_imports = [];
@@ -1319,7 +1316,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
namespace;
in_namespace = true;
crate_name;
- rust_module_name = crate.A.name;
+ rust_module_name = crate.name;
module_name = template_clauses_module;
custom_msg = ": templates for the decreases clauses";
custom_imports = [ types_module ];
@@ -1369,7 +1366,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
namespace;
in_namespace = false;
crate_name;
- rust_module_name = crate.A.name;
+ rust_module_name = crate.name;
module_name = opaque_module;
custom_msg;
custom_imports = [];
@@ -1408,7 +1405,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
namespace;
in_namespace = true;
crate_name;
- rust_module_name = crate.A.name;
+ rust_module_name = crate.name;
module_name = fun_module;
custom_msg = ": function definitions";
custom_imports = [];
@@ -1441,7 +1438,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
namespace;
in_namespace = true;
crate_name;
- rust_module_name = crate.A.name;
+ rust_module_name = crate.name;
module_name = crate_name;
custom_msg = "";
custom_imports = [];
diff --git a/compiler/TranslateCore.ml b/compiler/TranslateCore.ml
index a148175d..a974cdee 100644
--- a/compiler/TranslateCore.ml
+++ b/compiler/TranslateCore.ml
@@ -26,3 +26,6 @@ let trans_ctx_to_fmt_env (ctx : trans_ctx) : Print.fmt_env =
let trans_ctx_to_pure_fmt_env (ctx : trans_ctx) : PrintPure.fmt_env =
PrintPure.decls_ctx_to_fmt_env ctx
+
+let name_to_string (ctx : trans_ctx) =
+ Print.Types.name_to_string (trans_ctx_to_fmt_env ctx)
diff --git a/compiler/TypesAnalysis.ml b/compiler/TypesAnalysis.ml
index 659eac59..5371a3d7 100644
--- a/compiler/TypesAnalysis.ml
+++ b/compiler/TypesAnalysis.ml
@@ -283,7 +283,7 @@ let analyze_type_decl (updated : bool ref) (infos : type_infos)
let analyze_type_declaration_group (type_decls : type_decl TypeDeclId.Map.t)
(infos : type_infos) (decl : A.type_declaration_group) : type_infos =
(* Collect the identifiers used in the declaration group *)
- let ids = match decl with NonRec id -> [ id ] | Rec ids -> ids in
+ let ids = match decl with NonRecGroup id -> [ id ] | RecGroup ids -> ids in
(* Retrieve the type definitions *)
let decl_defs = List.map (fun id -> TypeDeclId.Map.find id type_decls) ids in
(* Initialize the type information for the current definitions *)
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-18 21:33:18 +0000