diff --git a/compiler/desugared/desugared_to_scope.ml b/compiler/desugared/desugared_to_scope.ml index f11ecc43..c21d561b 100644 --- a/compiler/desugared/desugared_to_scope.ml +++ b/compiler/desugared/desugared_to_scope.ml @@ -27,18 +27,18 @@ type target_scope_vars = type ctx = { scope_var_mapping : target_scope_vars ScopeVarMap.t; - var_mapping : (Ast.expr, Scopelang.Ast.expr Var.t) Var.Map.t; + var_mapping : (Ast.expr, untyped Scopelang.Ast.expr Var.t) Var.Map.t; } let tag_with_log_entry - (e : Scopelang.Ast.expr) + (e : untyped Scopelang.Ast.expr) (l : log_entry) - (markings : Utils.Uid.MarkedString.info list) : Scopelang.Ast.expr = + (markings : Utils.Uid.MarkedString.info list) : untyped Scopelang.Ast.expr = ( EApp ((EOp (Unop (Log (l, markings))), Marked.get_mark e), [e]), Marked.get_mark e ) let rec translate_expr (ctx : ctx) (e : Ast.expr) : - Scopelang.Ast.expr Bindlib.box = + untyped Scopelang.Ast.expr Bindlib.box = let m = Marked.get_mark e in match Marked.unmark e with | ELocation (SubScopeVar (s_name, ss_name, s_var)) -> @@ -186,7 +186,7 @@ let rec rule_tree_to_expr (ctx : ctx) (def_pos : Pos.t) (is_func : Ast.expr Var.t option) - (tree : rule_tree) : Scopelang.Ast.expr Bindlib.box = + (tree : rule_tree) : untyped Scopelang.Ast.expr Bindlib.box = let emark = Untyped { pos = def_pos } in let exceptions, base_rules = match tree with Leaf r -> [], r | Node (exceptions, r) -> exceptions, r @@ -236,7 +236,7 @@ let rec rule_tree_to_expr base_rules in let translate_and_unbox_list (list : Ast.expr Bindlib.box list) : - Scopelang.Ast.expr Bindlib.box list = + untyped Scopelang.Ast.expr Bindlib.box list = List.map (fun e -> (* There are two levels of boxing here, the outermost is introduced by @@ -283,7 +283,7 @@ let rec rule_tree_to_expr that the result returned by the function is not empty *) let default = Bindlib.box_apply - (fun (default : Scopelang.Ast.expr) -> ErrorOnEmpty default, emark) + (fun (default : untyped Scopelang.Ast.expr) -> ErrorOnEmpty default, emark) default in Expr.make_abs @@ -303,7 +303,7 @@ let translate_def (typ : typ) (io : Scopelang.Ast.io) ~(is_cond : bool) - ~(is_subscope_var : bool) : Scopelang.Ast.expr = + ~(is_subscope_var : bool) : untyped Scopelang.Ast.expr = (* Here, we have to transform this list of rules into a default tree. *) let is_def_func = match Marked.unmark typ with TArrow (_, _) -> true | _ -> false @@ -411,7 +411,7 @@ let translate_def [Ast.empty_rule (Marked.get_mark typ) is_def_func_param_typ] ))) (** Translates a scope *) -let translate_scope (ctx : ctx) (scope : Ast.scope) : Scopelang.Ast.scope_decl = +let translate_scope (ctx : ctx) (scope : Ast.scope) : untyped Scopelang.Ast.scope_decl = let scope_dependencies = Dependency.build_scope_dependencies scope in Dependency.check_for_cycle scope scope_dependencies; let scope_ordering = @@ -633,7 +633,7 @@ let translate_scope (ctx : ctx) (scope : Ast.scope) : Scopelang.Ast.scope_decl = (** {1 API} *) -let translate_program (pgrm : Ast.program) : Scopelang.Ast.program = +let translate_program (pgrm : Ast.program) : untyped Scopelang.Ast.program = (* First we give mappings to all the locations between Desugared and Scopelang. This involves creating a new Scopelang scope variable for every state of a Desugared variable. *) diff --git a/compiler/desugared/desugared_to_scope.mli b/compiler/desugared/desugared_to_scope.mli index 7b8d2c12..b5314e7c 100644 --- a/compiler/desugared/desugared_to_scope.mli +++ b/compiler/desugared/desugared_to_scope.mli @@ -16,4 +16,4 @@ (** Translation from {!module: Desugared.Ast} to {!module: Scopelang.Ast} *) -val translate_program : Ast.program -> Scopelang.Ast.program +val translate_program : Ast.program -> Shared_ast.untyped Scopelang.Ast.program diff --git a/compiler/scopelang/ast.ml b/compiler/scopelang/ast.ml index eb5cd774..5dbcdb14 100644 --- a/compiler/scopelang/ast.ml +++ b/compiler/scopelang/ast.ml @@ -28,15 +28,9 @@ Set.Make (struct let compare = Expr.compare_location end) -type expr = (scopelang, untyped mark) gexpr +type 'm expr = (scopelang, 'm mark) gexpr -module ExprMap = Map.Make (struct - type t = expr - - let compare = Expr.compare -end) - -let rec locations_used (e : expr) : LocationSet.t = +let rec locations_used (e : 'm expr) : LocationSet.t = match Marked.unmark e with | ELocation l -> LocationSet.singleton (l, Expr.pos e) | EVar _ | ELit _ | EOp _ -> LocationSet.empty @@ -74,18 +68,20 @@ let rec locations_used (e : expr) : LocationSet.t = type io_input = NoInput | OnlyInput | Reentrant type io = { io_output : bool Marked.pos; io_input : io_input Marked.pos } -type rule = - | Definition of location Marked.pos * typ * io * expr - | Assertion of expr +type 'm rule = + | Definition of location Marked.pos * typ * io * 'm expr + | Assertion of 'm expr | Call of ScopeName.t * SubScopeName.t -type scope_decl = { +type 'm scope_decl = { scope_decl_name : ScopeName.t; scope_sig : (typ * io) ScopeVarMap.t; - scope_decl_rules : rule list; + scope_decl_rules : 'm rule list; } -type program = { - program_scopes : scope_decl ScopeMap.t; +type 'm program = { + program_scopes : 'm scope_decl ScopeMap.t; program_ctx : decl_ctx; } + +(* let type_program: untyped *) diff --git a/compiler/scopelang/ast.mli b/compiler/scopelang/ast.mli index 28179afd..dfd8795e 100644 --- a/compiler/scopelang/ast.mli +++ b/compiler/scopelang/ast.mli @@ -37,11 +37,9 @@ module LocationSet : Set.S with type elt = location Marked.pos (** {1 Abstract syntax tree} *) -type expr = (scopelang, untyped mark) gexpr +type 'm expr = (scopelang, 'm mark) gexpr -module ExprMap : Map.S with type key = expr - -val locations_used : expr -> LocationSet.t +val locations_used : 'm expr -> LocationSet.t (** This type characterizes the three levels of visibility for a given scope variable with regards to the scope's input and possible redefinitions inside @@ -64,18 +62,18 @@ type io = { } (** Characterization of the input/output status of a scope variable. *) -type rule = - | Definition of location Marked.pos * typ * io * expr - | Assertion of expr +type 'm rule = + | Definition of location Marked.pos * typ * io * 'm expr + | Assertion of 'm expr | Call of ScopeName.t * SubScopeName.t -type scope_decl = { +type 'm scope_decl = { scope_decl_name : ScopeName.t; scope_sig : (typ * io) ScopeVarMap.t; - scope_decl_rules : rule list; + scope_decl_rules : 'm rule list; } -type program = { - program_scopes : scope_decl ScopeMap.t; +type 'm program = { + program_scopes : 'm scope_decl ScopeMap.t; program_ctx : decl_ctx; } diff --git a/compiler/scopelang/dependency.ml b/compiler/scopelang/dependency.ml index 90ed3085..e8d210d7 100644 --- a/compiler/scopelang/dependency.ml +++ b/compiler/scopelang/dependency.ml @@ -45,7 +45,7 @@ module STopologicalTraversal = Graph.Topological.Make (SDependencies) module SSCC = Graph.Components.Make (SDependencies) (** Tarjan's stongly connected components algorithm, provided by OCamlGraph *) -let build_program_dep_graph (prgm : Ast.program) : SDependencies.t = +let build_program_dep_graph (prgm : 'm Ast.program) : SDependencies.t = let g = SDependencies.empty in let g = ScopeMap.fold diff --git a/compiler/scopelang/dependency.mli b/compiler/scopelang/dependency.mli index 3e8f7d39..5ccf1790 100644 --- a/compiler/scopelang/dependency.mli +++ b/compiler/scopelang/dependency.mli @@ -27,7 +27,7 @@ open Shared_ast module SDependencies : Graph.Sig.P with type V.t = ScopeName.t and type E.label = Pos.t -val build_program_dep_graph : Ast.program -> SDependencies.t +val build_program_dep_graph : 'm Ast.program -> SDependencies.t val check_for_cycle_in_scope : SDependencies.t -> unit val get_scope_ordering : SDependencies.t -> ScopeName.t list diff --git a/compiler/scopelang/print.ml b/compiler/scopelang/print.ml index 2d791364..a2d88d09 100644 --- a/compiler/scopelang/print.ml +++ b/compiler/scopelang/print.ml @@ -98,7 +98,7 @@ let scope ?(debug = false) ctx fmt (name, decl) = SubScopeName.format_t subscope_name Print.punctuation "]")) decl.scope_decl_rules -let program ?(debug : bool = false) (fmt : Format.formatter) (p : program) : +let program ?(debug : bool = false) (fmt : Format.formatter) (p : 'm program) : unit = let ctx = p.program_ctx in let pp_sep fmt () = diff --git a/compiler/scopelang/print.mli b/compiler/scopelang/print.mli index 77fbd320..4ec2f4fe 100644 --- a/compiler/scopelang/print.mli +++ b/compiler/scopelang/print.mli @@ -18,11 +18,11 @@ val scope : ?debug:bool (** [true] for debug printing *) -> Shared_ast.decl_ctx -> Format.formatter -> - Shared_ast.ScopeName.t * Ast.scope_decl -> + Shared_ast.ScopeName.t * 'm Ast.scope_decl -> unit val program : ?debug:bool (** [true] for debug printing *) -> Format.formatter -> - Ast.program -> + 'm Ast.program -> unit diff --git a/compiler/scopelang/scope_to_dcalc.ml b/compiler/scopelang/scope_to_dcalc.ml index b263b62b..b6c3cb64 100644 --- a/compiler/scopelang/scope_to_dcalc.ml +++ b/compiler/scopelang/scope_to_dcalc.ml @@ -35,7 +35,7 @@ type scope_sig_ctx = { type scope_sigs_ctx = scope_sig_ctx ScopeMap.t -type ctx = { +type 'm ctx = { structs : struct_ctx; enums : enum_ctx; scope_name : ScopeName.t; @@ -45,7 +45,7 @@ type ctx = { subscope_vars : (untyped Dcalc.Ast.expr Var.t * naked_typ * Ast.io) ScopeVarMap.t SubScopeMap.t; - local_vars : (Ast.expr, untyped Dcalc.Ast.expr Var.t) Var.Map.t; + local_vars : ('m Ast.expr, untyped Dcalc.Ast.expr Var.t) Var.Map.t; } let empty_ctx @@ -104,16 +104,21 @@ let tag_with_log_entry NOTE: the choice of the exception that will be triggered and show in the trace is arbitrary (but deterministic). *) -let collapse_similar_outcomes (excepts : Ast.expr list) : Ast.expr list = +let collapse_similar_outcomes (type m) (excepts : m Ast.expr list) : m Ast.expr list = + let module ExprMap = Map.Make (struct + type t = m Ast.expr + let compare = Expr.compare + end) + in let cons_map = List.fold_left (fun map -> function | (EDefault ([], _, cons), _) as e -> - Ast.ExprMap.update cons + ExprMap.update cons (fun prev -> Some (e :: Option.value ~default:[] prev)) map | _ -> map) - Ast.ExprMap.empty excepts + ExprMap.empty excepts in let _, excepts = List.fold_right @@ -127,16 +132,16 @@ let collapse_similar_outcomes (excepts : Ast.expr list) : Ast.expr list = [EDefault (acc, just, cons), pos] | _ -> assert false) [] - (Ast.ExprMap.find cons cons_map) + (ExprMap.find cons cons_map) in - Ast.ExprMap.add cons [] cons_map, collapsed_exc @ excepts + ExprMap.add cons [] cons_map, collapsed_exc @ excepts | e -> cons_map, e :: excepts) excepts (cons_map, []) in excepts -let rec translate_expr (ctx : ctx) (e : Ast.expr) : - untyped Dcalc.Ast.expr Bindlib.box = +let rec translate_expr (ctx : 'm ctx) (e : 'm Ast.expr) : + 'm Dcalc.Ast.expr Bindlib.box = Bindlib.box_apply (fun x -> Marked.same_mark_as x e) @@ match Marked.unmark e with @@ -355,12 +360,12 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr) : continuation yielding a [Dcalc.scope_body_expr] by giving it what should come later in the chain of let-bindings. *) let translate_rule - (ctx : ctx) - (rule : Ast.rule) + (ctx : 'm ctx) + (rule : 'm Ast.rule) ((sigma_name, pos_sigma) : Utils.Uid.MarkedString.info) : - (untyped Dcalc.Ast.expr scope_body_expr Bindlib.box -> - untyped Dcalc.Ast.expr scope_body_expr Bindlib.box) - * ctx = + ('m Dcalc.Ast.expr scope_body_expr Bindlib.box -> + 'm Dcalc.Ast.expr scope_body_expr Bindlib.box) + * 'm ctx = match rule with | Definition ((ScopelangScopeVar a, var_def_pos), tau, a_io, e) -> let a_name = ScopeVar.get_info (Marked.unmark a) in @@ -633,11 +638,11 @@ let translate_rule ctx ) let translate_rules - (ctx : ctx) - (rules : Ast.rule list) + (ctx : 'm ctx) + (rules : 'm Ast.rule list) ((sigma_name, pos_sigma) : Utils.Uid.MarkedString.info) (sigma_return_struct_name : StructName.t) : - untyped Dcalc.Ast.expr scope_body_expr Bindlib.box * ctx = + 'm Dcalc.Ast.expr scope_body_expr Bindlib.box * 'm ctx = let scope_lets, new_ctx = List.fold_left (fun (scope_lets, ctx) rule -> @@ -673,8 +678,8 @@ let translate_scope_decl (enum_ctx : enum_ctx) (sctx : scope_sigs_ctx) (scope_name : ScopeName.t) - (sigma : Ast.scope_decl) : - untyped Dcalc.Ast.expr scope_body Bindlib.box * struct_ctx = + (sigma : 'm Ast.scope_decl) : + 'm Dcalc.Ast.expr scope_body Bindlib.box * struct_ctx = let sigma_info = ScopeName.get_info sigma.scope_decl_name in let scope_sig = ScopeMap.find sigma.scope_decl_name sctx in let scope_variables = scope_sig.scope_sig_local_vars in @@ -800,8 +805,8 @@ let translate_scope_decl (input_destructurings rules_with_return_expr)), new_struct_ctx ) -let translate_program (prgm : Ast.program) : - untyped Dcalc.Ast.program * Dependency.TVertex.t list = +let translate_program (prgm : 'm Ast.program) : + 'm Dcalc.Ast.program * Dependency.TVertex.t list = let scope_dependencies = Dependency.build_program_dep_graph prgm in Dependency.check_for_cycle_in_scope scope_dependencies; let types_ordering = diff --git a/compiler/scopelang/scope_to_dcalc.mli b/compiler/scopelang/scope_to_dcalc.mli index 40ad6f43..a42cb5bf 100644 --- a/compiler/scopelang/scope_to_dcalc.mli +++ b/compiler/scopelang/scope_to_dcalc.mli @@ -17,7 +17,7 @@ (** Scope language to default calculus translator *) val translate_program : - Ast.program -> + Shared_ast.untyped Ast.program -> Shared_ast.untyped Dcalc.Ast.program * Dependency.TVertex.t list (** Usage [translate_program p] returns a tuple [(new_program, types_list)] where [new_program] is the map of translated scopes. Finally, [types_list]