summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/Contexts.ml4
-rw-r--r--compiler/Crates.ml1
-rw-r--r--compiler/Driver.ml2
-rw-r--r--compiler/FunsAnalysis.ml3
-rw-r--r--compiler/Interpreter.ml15
-rw-r--r--compiler/InterpreterStatements.ml9
-rw-r--r--compiler/PrePasses.ml2
-rw-r--r--compiler/Pure.ml36
-rw-r--r--compiler/Translate.ml20
-rw-r--r--compiler/TypesAnalysis.ml6
-rw-r--r--compiler/dune1
11 files changed, 47 insertions, 52 deletions
diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 52815859..2d5fd907 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -210,7 +210,7 @@ let config_of_partial (mode : interpreter_mode) (config : partial_config) :
}
type type_context = {
- type_decls_groups : Crates.type_declaration_group TypeDeclId.Map.t;
+ type_decls_groups : type_declaration_group TypeDeclId.Map.t;
type_decls : type_decl TypeDeclId.Map.t;
type_infos : TypesAnalysis.type_infos;
}
@@ -391,7 +391,7 @@ let ctx_lookup_abs (ctx : eval_ctx) (abs_id : V.AbstractionId.id) : V.abs =
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 Crates.Rec _ -> true | Crates.NonRec _ -> false
+ match decl_group with Rec _ -> true | NonRec _ -> false
(** Visitor to iterate over the values in the *current* frame *)
class ['self] iter_frame =
diff --git a/compiler/Crates.ml b/compiler/Crates.ml
deleted file mode 100644
index 81f42cea..00000000
--- a/compiler/Crates.ml
+++ /dev/null
@@ -1 +0,0 @@
-include Charon.Crates
diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index ae9d238a..c8a1fef4 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -148,7 +148,7 @@ let () =
(* Load the module *)
let json = Yojson.Basic.from_file filename in
- match llbc_crate_of_json json with
+ match crate_of_json json with
| Error s ->
main_log#error "error: %s\n" s;
exit 1
diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml
index 39f85581..59373985 100644
--- a/compiler/FunsAnalysis.ml
+++ b/compiler/FunsAnalysis.ml
@@ -8,7 +8,6 @@
*)
open LlbcAst
-open Crates
module EU = ExpressionsUtils
(** Various information about a function.
@@ -26,7 +25,7 @@ type fun_info = {
(** Various information about a module's functions *)
type modules_funs_info = fun_info FunDeclId.Map.t
-let analyze_module (m : llbc_crate) (funs_map : fun_decl FunDeclId.Map.t)
+let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
(globals_map : global_decl GlobalDeclId.Map.t) (use_state : bool) :
modules_funs_info =
let infos = ref FunDeclId.Map.empty in
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index f93a0ae1..f92473f7 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -12,12 +12,12 @@ module SA = SymbolicAst
(** The local logger *)
let log = L.interpreter_log
-let compute_type_fun_global_contexts (m : Crates.llbc_crate) :
+let compute_type_fun_global_contexts (m : A.crate) :
C.type_context * C.fun_context * C.global_context =
- let type_decls_list, _, _ = Crates.split_declarations m.declarations in
- let type_decls, fun_decls, global_decls = Crates.compute_defs_maps m in
+ let type_decls_list, _, _ = split_declarations m.declarations in
+ let type_decls, fun_decls, global_decls = compute_defs_maps m in
let type_decls_groups, _funs_defs_groups, _globals_defs_groups =
- Crates.split_declarations_to_group_maps m.declarations
+ split_declarations_to_group_maps m.declarations
in
let type_infos =
TypesAnalysis.analyze_type_declarations type_decls type_decls_list
@@ -276,7 +276,7 @@ module Test = struct
(** Test a unit function (taking no arguments) by evaluating it in an empty
environment.
*)
- let test_unit_function (config : C.partial_config) (crate : Crates.llbc_crate)
+ let test_unit_function (config : C.partial_config) (crate : A.crate)
(fid : A.FunDeclId.id) : unit =
(* Retrieve the function declaration *)
let fdef = A.FunDeclId.nth crate.functions fid in
@@ -331,8 +331,7 @@ module Test = struct
&& List.length def.A.signature.inputs = 0
(** Test all the unit functions in a list of function definitions *)
- let test_unit_functions (config : C.partial_config)
- (crate : Crates.llbc_crate) : unit =
+ let test_unit_functions (config : C.partial_config) (crate : A.crate) : unit =
let unit_funs = List.filter fun_decl_is_transparent_unit crate.functions in
let test_unit_fun (def : A.fun_decl) : unit =
test_unit_function config crate def.A.def_id
@@ -373,7 +372,7 @@ module Test = struct
they are not supported by the symbolic interpreter.
*)
let test_functions_symbolic (config : C.partial_config) (synthesize : bool)
- (crate : Crates.llbc_crate) : unit =
+ (crate : A.crate) : unit =
(* Filter the functions which contain loops *)
let no_loop_funs =
List.filter
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 56ab05f3..fc3b0975 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -922,15 +922,14 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
(* Compose and apply *)
comp cc cf_eval_st cf ctx
-and eval_global (config : C.config) (dest : E.VarId.id)
- (gid : LA.GlobalDeclId.id) : st_cm_fun =
+and eval_global (config : C.config) (dest : E.place) (gid : LA.GlobalDeclId.id)
+ : st_cm_fun =
fun cf ctx ->
let global = C.ctx_lookup_global_decl ctx gid in
- let place = { E.var_id = dest; projection = [] } in
match config.mode with
| ConcreteMode ->
(* Treat the evaluation of the global as a call to the global body (without arguments) *)
- (eval_local_function_call_concrete config global.body_id [] [] [] place)
+ (eval_local_function_call_concrete config global.body_id [] [] [] dest)
cf ctx
| SymbolicMode ->
(* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be
@@ -939,7 +938,7 @@ and eval_global (config : C.config) (dest : E.VarId.id)
mk_fresh_symbolic_value V.Global (ety_no_regions_to_rty global.ty)
in
let cc =
- assign_to_place config (mk_typed_value_from_symbolic_value sval) place
+ assign_to_place config (mk_typed_value_from_symbolic_value sval) dest
in
let e = cc (cf Unit) ctx in
S.synthesize_global_eval gid sval e
diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml
index a09ae476..8f1354b7 100644
--- a/compiler/PrePasses.ml
+++ b/compiler/PrePasses.ml
@@ -49,6 +49,6 @@ let filter_drop_assigns (f : A.fun_decl) : A.fun_decl =
in
{ f with body }
-let apply_passes (m : Crates.llbc_crate) : Crates.llbc_crate =
+let apply_passes (m : A.crate) : A.crate =
let functions = List.map filter_drop_assigns m.functions in
{ m with functions }
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index f9c693c6..7f71cf7f 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -48,7 +48,7 @@ let option_none_id = T.option_none_id
type type_id = AdtId of TypeDeclId.id | Tuple | Assumed of assumed_ty
[@@deriving show, ord]
-(** Ancestor for iter visitor for [ty] *)
+(** Ancestor for iter visitor for {!ty} *)
class ['self] iter_ty_base =
object (_self : 'self)
inherit [_] VisitorsRuntime.iter
@@ -57,7 +57,7 @@ class ['self] iter_ty_base =
method visit_integer_type : 'env -> integer_type -> unit = fun _ _ -> ()
end
-(** Ancestor for map visitor for [ty] *)
+(** Ancestor for map visitor for {!ty} *)
class ['self] map_ty_base =
object (_self : 'self)
inherit [_] VisitorsRuntime.map
@@ -164,8 +164,8 @@ type mplace = {
type variant_id = VariantId.id [@@deriving show]
-(** Ancestor for [iter_pat_var_or_dummy] visitor *)
-class ['self] iter_value_base =
+(** Ancestor for {!iter_typed_pattern} visitor *)
+class ['self] iter_typed_pattern_base =
object (_self : 'self)
inherit [_] VisitorsRuntime.iter
@@ -178,8 +178,8 @@ class ['self] iter_value_base =
method visit_variant_id : 'env -> variant_id -> unit = fun _ _ -> ()
end
-(** Ancestor for [map_typed_rvalue] visitor *)
-class ['self] map_value_base =
+(** Ancestor for {!map_typed_pattern} visitor *)
+class ['self] map_typed_pattern_base =
object (_self : 'self)
inherit [_] VisitorsRuntime.map
@@ -192,8 +192,8 @@ class ['self] map_value_base =
method visit_variant_id : 'env -> variant_id -> variant_id = fun _ x -> x
end
-(** Ancestor for [reduce_typed_rvalue] visitor *)
-class virtual ['self] reduce_value_base =
+(** Ancestor for {!reduce_typed_pattern} visitor *)
+class virtual ['self] reduce_typed_pattern_base =
object (self : 'self)
inherit [_] VisitorsRuntime.reduce
@@ -206,8 +206,8 @@ class virtual ['self] reduce_value_base =
method visit_variant_id : 'env -> variant_id -> 'a = fun _ _ -> self#zero
end
-(** Ancestor for [mapreduce_typed_rvalue] visitor *)
-class virtual ['self] mapreduce_value_base =
+(** Ancestor for {!mapreduce_typed_pattern} visitor *)
+class virtual ['self] mapreduce_typed_pattern_base =
object (self : 'self)
inherit [_] VisitorsRuntime.mapreduce
@@ -247,7 +247,7 @@ and typed_pattern = { value : pattern; ty : ty }
{
name = "iter_typed_pattern";
variety = "iter";
- ancestors = [ "iter_value_base" ];
+ ancestors = [ "iter_typed_pattern_base" ];
nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
concrete = true;
polymorphic = false;
@@ -256,7 +256,7 @@ and typed_pattern = { value : pattern; ty : ty }
{
name = "map_typed_pattern";
variety = "map";
- ancestors = [ "map_value_base" ];
+ ancestors = [ "map_typed_pattern_base" ];
nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
concrete = true;
polymorphic = false;
@@ -265,7 +265,7 @@ and typed_pattern = { value : pattern; ty : ty }
{
name = "reduce_typed_pattern";
variety = "reduce";
- ancestors = [ "reduce_value_base" ];
+ ancestors = [ "reduce_typed_pattern_base" ];
nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
polymorphic = false;
},
@@ -273,7 +273,7 @@ and typed_pattern = { value : pattern; ty : ty }
{
name = "mapreduce_typed_pattern";
variety = "mapreduce";
- ancestors = [ "mapreduce_value_base" ];
+ ancestors = [ "mapreduce_typed_pattern_base" ];
nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
polymorphic = false;
}]
@@ -323,7 +323,7 @@ type qualif = { id : qualif_id; type_args : ty list } [@@deriving show]
type var_id = VarId.id [@@deriving show]
-(** Ancestor for [iter_expression] visitor *)
+(** Ancestor for {!iter_expression} visitor *)
class ['self] iter_expression_base =
object (_self : 'self)
inherit [_] iter_typed_pattern
@@ -332,7 +332,7 @@ class ['self] iter_expression_base =
method visit_qualif : 'env -> qualif -> unit = fun _ _ -> ()
end
-(** Ancestor for [map_expression] visitor *)
+(** Ancestor for {!map_expression} visitor *)
class ['self] map_expression_base =
object (_self : 'self)
inherit [_] map_typed_pattern
@@ -344,7 +344,7 @@ class ['self] map_expression_base =
method visit_qualif : 'env -> qualif -> qualif = fun _ x -> x
end
-(** Ancestor for [reduce_expression] visitor *)
+(** Ancestor for {!reduce_expression} visitor *)
class virtual ['self] reduce_expression_base =
object (self : 'self)
inherit [_] reduce_typed_pattern
@@ -356,7 +356,7 @@ class virtual ['self] reduce_expression_base =
method visit_qualif : 'env -> qualif -> 'a = fun _ _ -> self#zero
end
-(** Ancestor for [mapreduce_expression] visitor *)
+(** Ancestor for {!mapreduce_expression} visitor *)
class virtual ['self] mapreduce_expression_base =
object (self : 'self)
inherit [_] mapreduce_typed_pattern
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 8f3b94c4..35633d29 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -285,7 +285,7 @@ let translate_function_to_pure (config : C.partial_config)
(pure_forward, pure_backwards)
let translate_module_to_pure (config : C.partial_config)
- (mp_config : Micro.config) (use_state : bool) (crate : Crates.llbc_crate) :
+ (mp_config : Micro.config) (use_state : bool) (crate : A.crate) :
trans_ctx * Pure.type_decl list * (bool * pure_fun_translation) list =
(* Debug *)
log#ldebug (lazy "translate_module_to_pure");
@@ -357,7 +357,7 @@ let translate_module_to_pure (config : C.partial_config)
(** Extraction context *)
type gen_ctx = {
- crate : Crates.llbc_crate;
+ crate : A.crate;
extract_ctx : PureToExtract.extraction_ctx;
trans_types : Pure.type_decl Pure.TypeDeclId.Map.t;
trans_funs : (bool * pure_fun_translation) A.FunDeclId.Map.t;
@@ -533,7 +533,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
ExtractToFStar.extract_state_type fmt ctx.extract_ctx qualif
in
- let export_decl (decl : Crates.declaration_group) : unit =
+ let export_decl (decl : A.declaration_group) : unit =
match decl with
| Type (NonRec id) ->
if config.extract_types then export_type ExtractToFStar.Type id
@@ -627,7 +627,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
TODO: rename to translate_crate
*)
let translate_module (filename : string) (dest_dir : string) (config : config)
- (crate : Crates.llbc_crate) : unit =
+ (crate : A.crate) : unit =
(* Translate the module to the pure AST *)
let trans_ctx, trans_types, trans_funs =
translate_module_to_pure config.eval_config config.mp_config
@@ -654,7 +654,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
(List.concat
(List.map
(fun decl ->
- match decl with Crates.Fun (Rec ids) -> ids | _ -> [])
+ match decl with A.Fun (Rec ids) -> ids | _ -> [])
crate.declarations))
in
@@ -794,7 +794,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
interface = has_opaque_types;
}
in
- extract_file types_config gen_ctx types_filename crate.Crates.name
+ extract_file types_config gen_ctx types_filename crate.A.name
types_module ": type definitions" [] [];
(* Extract the template clauses *)
@@ -808,7 +808,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
let clauses_config =
{ base_gen_config with extract_template_decreases_clauses = true }
in
- extract_file clauses_config gen_ctx clauses_filename crate.Crates.name
+ extract_file clauses_config gen_ctx clauses_filename crate.A.name
clauses_module ": templates for the decreases clauses" [ types_module ]
[]);
@@ -826,7 +826,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
interface = true;
}
in
- extract_file opaque_config gen_ctx opaque_filename crate.Crates.name
+ extract_file opaque_config gen_ctx opaque_filename crate.A.name
opaque_module ": opaque function definitions" [] [ types_module ];
[ opaque_module ])
else []
@@ -845,7 +845,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
let clauses_module =
if needs_clauses_module then [ module_name ^ ".Clauses" ] else []
in
- extract_file fun_config gen_ctx fun_filename crate.Crates.name fun_module
+ extract_file fun_config gen_ctx fun_filename crate.A.name fun_module
": function definitions" []
([ types_module ] @ opaque_funs_module @ clauses_module))
else
@@ -867,5 +867,5 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
in
(* Add the extension for F* *)
let extract_filename = extract_filebasename ^ ".fst" in
- extract_file gen_config gen_ctx extract_filename crate.Crates.name
+ extract_file gen_config gen_ctx extract_filename crate.A.name
module_name "" [] []
diff --git a/compiler/TypesAnalysis.ml b/compiler/TypesAnalysis.ml
index 60ce5149..db6d3b98 100644
--- a/compiler/TypesAnalysis.ml
+++ b/compiler/TypesAnalysis.ml
@@ -1,5 +1,5 @@
open Types
-open Crates
+module A = LlbcAst
type subtype_info = {
under_borrow : bool; (** Are we inside a borrow? *)
@@ -275,7 +275,7 @@ let analyze_type_decl (updated : bool ref) (infos : type_infos)
infos
let analyze_type_declaration_group (type_decls : type_decl TypeDeclId.Map.t)
- (infos : type_infos) (decl : type_declaration_group) : type_infos =
+ (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
(* Retrieve the type definitions *)
@@ -309,7 +309,7 @@ let analyze_type_declaration_group (type_decls : type_decl TypeDeclId.Map.t)
Rk.: pay attention to the difference between type definitions and types!
*)
let analyze_type_declarations (type_decls : type_decl TypeDeclId.Map.t)
- (decls : type_declaration_group list) : type_infos =
+ (decls : A.type_declaration_group list) : type_infos =
List.fold_left
(fun infos decl -> analyze_type_declaration_group type_decls infos decl)
TypeDeclId.Map.empty decls
diff --git a/compiler/dune b/compiler/dune
index af4cdb08..0d340d59 100644
--- a/compiler/dune
+++ b/compiler/dune
@@ -17,7 +17,6 @@
ConstStrings
Contexts
Cps
- Crates
Expressions
ExpressionsUtils
ExtractToFStar
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 02:34:14 +0000