Generalise the types to allow scopelang ASTs to be typed

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. *)

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

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  *)

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;
 }

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

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
 

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 () =

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

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 =

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]