Yet some more small improvements to the AST encoding

compiler/lcalc/closure_conversion.ml

@@ -86,6 +86,7 @@ let rec hoist_context_free_closures :
     [{ name = closure_var; closure = e }], Expr.make_var closure_var m
   | EApp _ ->
     Expr.map_gather ~acc:[] ~join:( @ ) ~f:(hoist_context_free_closures ctx) e
+  | _ -> .
  [@@warning "-32"]
 
 (** Returns the expression with closed closures and the set of free variables
@@ -237,6 +238,7 @@ let rec transform_closures_expr :
       Expr.make_let_in code_env_var
         (TAny, Expr.pos e)
         new_e1 call_expr (Expr.pos e) )
+  | _ -> .
 
 (* Here I have to reimplement Scope.map_exprs_in_lets because I'm changing the
    type *)

compiler/lcalc/compile_with_exceptions.ml

@@ -73,12 +73,12 @@ and translate_expr (ctx : 'm ctx) (e : 'm D.expr) : 'm A.expr boxed =
       (Marked.get_mark e)
   | EDefault { excepts; just; cons } ->
     translate_default ctx excepts just cons (Marked.get_mark e)
-  | ( ELit _ | EApp _ | EOp _ | EArray _ | EVar _ | EAbs _ | EIfThenElse _
-    | ETuple _ | ETupleAccess _ | EInj _ | EAssert _ | EStruct _
-    | EStructAccess _ | EMatch _ ) as e ->
-    Expr.map_raw ~fop:Operator.translate
-      ~floc:(function _ -> .)
-      ~f:(translate_expr ctx) (Marked.mark m e)
+  | EOp { op; tys } -> Expr.eop (Operator.translate op) tys m
+  | ( ELit _ | EApp _ | EArray _ | EVar _ | EAbs _ | EIfThenElse _ | ETuple _
+    | ETupleAccess _ | EInj _ | EAssert _ | EStruct _ | EStructAccess _
+    | EMatch _ ) as e ->
+    Expr.map ~f:(translate_expr ctx) (Marked.mark m e)
+  | _ -> .
 
 let rec translate_scope_lets
     (decl_ctx : decl_ctx)

compiler/lcalc/compile_without_exceptions.ml

@@ -300,9 +300,9 @@ let rec translate_and_hoist (ctx : 'm ctx) (e : 'm D.expr) :
     e', hoists
   | EArray es ->
     let es', hoists = es |> List.map (translate_and_hoist ctx) |> List.split in
-
     Expr.earray es' mark, disjoint_union_maps (Expr.pos e) hoists
   | EOp { op; tys } -> Expr.eop (Operator.translate op) tys mark, Var.Map.empty
+  | _ -> .
 
 and translate_expr ?(append_esome = true) (ctx : 'm ctx) (e : 'm D.expr) :
     'm A.expr boxed =

compiler/lcalc/to_ocaml.ml

@@ -386,6 +386,7 @@ let rec format_expr (ctx : decl_ctx) (fmt : Format.formatter) (e : 'm expr) :
       format_with_parens body format_exception
       (exn, Expr.pos e)
       format_with_parens handler
+  | _ -> .
 
 let format_struct_embedding
     (fmt : Format.formatter)

compiler/shared_ast/definitions.ml

@@ -318,7 +318,11 @@ and ('a, 'b, 't) base_gexpr =
       args : ('a, 't) gexpr list;
     }
       -> ('a, [< all ], 't) base_gexpr
-  | EOp : { op : 'a operator; tys : typ list } -> ('a, [< all ], 't) base_gexpr
+  | EOp : {
+      op : 'b operator;
+      tys : typ list;
+    }
+      -> ('a, ([< all ] as 'b), 't) base_gexpr
   | EArray : ('a, 't) gexpr list -> ('a, [< all ], 't) base_gexpr
   | EVar : ('a, 't) naked_gexpr Bindlib.var -> ('a, _, 't) base_gexpr
   | EAbs : {
@@ -357,7 +361,7 @@ and ('a, 'b, 't) base_gexpr =
     }
       -> ('a, [< all ], 't) base_gexpr
   (* Early stages *)
-  | ELocation : 'a glocation -> ('a, [< all > `ExplicitScopes ], 't) base_gexpr
+  | ELocation : 'b glocation -> ('a, ([< all ] as 'b), 't) base_gexpr
   | EScopeCall : {
       scope : ScopeName.t;
       args : ('a, 't) gexpr ScopeVar.Map.t;

compiler/shared_ast/expr.ml

@@ -205,17 +205,15 @@ let maybe_ty (type m) ?(typ = TAny) (m : m mark) : typ =
 (* - Traversal functions - *)
 
 (* shallow map *)
-let map_raw
+let map
     (type a b)
     ~(f : (a, 'm1) gexpr -> (b, 'm2) boxed_gexpr)
-    ~(fop : a Op.t -> b Op.t)
-    ~(floc : a glocation -> b glocation)
     (e : ((a, b, 'm1) base_gexpr, 'm2) Marked.t) : (b, 'm2) boxed_gexpr =
   let m = Marked.get_mark e in
   match Marked.unmark e with
   | ELit l -> elit l m
   | EApp { f = e1; args } -> eapp (f e1) (List.map f args) m
-  | EOp { op; tys } -> eop (fop op) tys m
+  | EOp { op; tys } -> eop op tys m
   | EArray args -> earray (List.map f args) m
   | EVar v -> evar (Var.translate v) m
   | EAbs { binder; tys } ->
@@ -235,7 +233,7 @@ let map_raw
   | EErrorOnEmpty e1 -> eerroronempty (f e1) m
   | ECatch { body; exn; handler } -> ecatch (f body) exn (f handler) m
   | ERaise exn -> eraise exn m
-  | ELocation loc -> elocation (floc loc) m
+  | ELocation loc -> elocation loc m
   | EStruct { name; fields } ->
     let fields = StructField.Map.map f fields in
     estruct name fields m
@@ -249,7 +247,6 @@ let map_raw
     let fields = ScopeVar.Map.map f args in
     escopecall scope fields m
 
-let map = map_raw ~fop:(fun op -> op) ~floc:(fun loc -> loc)
 let rec map_top_down ~f e = map ~f:(map_top_down ~f) (f e)
 
 let map_marks ~f e =

compiler/shared_ast/expr.mli

@@ -97,9 +97,7 @@ val ecatch :
   (([< all > `Exceptions ] as 'a), 't) boxed_gexpr
 
 val eraise : except -> 't -> ([< all > `Exceptions ], 't) boxed_gexpr
-
-val elocation :
-  'a glocation -> 't -> (([< all > `ExplicitScopes ] as 'a), 't) boxed_gexpr
+val elocation : 'a glocation -> 't -> (([< all ] as 'a), 't) boxed_gexpr
 
 val estruct :
   StructName.t ->
@@ -179,15 +177,14 @@ val untype : ('a, 'm mark) gexpr -> ('a, untyped mark) boxed_gexpr
 (** {2 Traversal functions} *)
 
 val map :
-  f:(('a, 't1) gexpr -> ('a, 't2) boxed_gexpr) ->
-  (('a, 't1) naked_gexpr, 't2) Marked.t ->
-  ('a, 't2) boxed_gexpr
+  f:(('a, 'm1) gexpr -> ('b, 'm2) boxed_gexpr) ->
+  (('a, 'b, 'm1) base_gexpr, 'm2) Marked.t ->
+  ('b, 'm2) boxed_gexpr
 (** Shallow mapping on expressions (non recursive): applies the given function
     to all sub-terms of the given expression, and rebuilds the node.
 
-    When applying a map transform to an expression, this avoids expliciting all
-    cases that remain unchanged. For instance, if you want to remove all errors
-    on empty, you can write
+    This function makes it very concise to transform only certain nodes of the
+    AST. For instance, if you want to remove all errors on empty, you can write
 
     {[
       let remove_error_empty =
@@ -197,30 +194,21 @@ val map :
           | _ -> Expr.map f e
         in
         f e
-    ]} *)
+    ]}
 
-val map_raw :
-  f:(('a, 'm1) gexpr -> ('b, 'm2) boxed_gexpr) ->
-  fop:('a Op.t -> 'b Op.t) ->
-  floc:('a glocation -> 'b glocation) ->
-  (('a, 'b, 'm1) base_gexpr, 'm2) Marked.t ->
-  ('b, 'm2) boxed_gexpr
-(** Lower-level version of shallow [map] that can be used for transforming the
-    type of the AST. See [Lcalc.Compile_without_exceptions] for an example. The
-    structure is like this:
+    This can even be used to translate between different kinds of ASTs: see
+    [Lcalc.Compile_without_exceptions] for an example. The structure is like
+    this:
 
     {[
       let rec translate = function
         | SpecificCase e -> TargetCase (translate e)
-        | (All | Other | Common | Cases) as e -> map_raw ~f:translate e
+        | (All | Other | Common | Cases) as e -> Expr.map ~f:translate e
     ]}
 
-    This function makes it very concise to transform only certain nodes of the
-    AST.
-
-    The [e] parameter passed to [map_raw] here needs to have only the common
-    cases in its shallow type, but can still contain any node from the starting
-    AST deeper inside: this is where the second type parameter to [base_gexpr]
+    The [e] parameter passed to [map] here needs to have only the common cases
+    in its shallow type, but can still contain any node from the starting AST
+    deeper inside: this is where the second type parameter to [base_gexpr]
     becomes useful. *)
 
 val map_top_down :

compiler/verification/z3backend.real.ml

@@ -786,6 +786,7 @@ and translate_expr (ctx : context) (vc : typed expr) : context * Expr.expr =
         ] )
   | EEmptyError -> failwith "[Z3 encoding] LEmptyError literals not supported"
   | EErrorOnEmpty _ -> failwith "[Z3 encoding] ErrorOnEmpty unsupported"
+  | _ -> .
 
 (** [create_z3unit] creates a Z3 sort and expression corresponding to the unit
     type and value respectively. Concretely, we represent unit as a tuple with 0