Box the expression from the outside

For closed expressions, similar to Bindlib.unbox

Rebuild the whole term, re-binding all variables and exposing free variables

Adds the given type information only on typed marks

Identity on untyped marks

Returns the corresponding type on a typed expr, or typ (defaulting to TAny) at the current position on an untyped one

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

  let remove_error_empty =
    let rec f e =
      match Marked.unmark e with
      | ErrorOnEmpty e1 -> Expr.map f e1
      | _ -> Expr.map f e
    in
    f e

Recursively applies f to the nodes of the expression tree. The type returned by f is hybrid since the mark at top-level has been rewritten, but not yet the marks in the subtrees.

Applies a function on all sub-terms of the given expression. Does not recurse, and doesn't open binders. Useful as helper for recursive calls within traversal functions. This can be used to compute free variables with e.g.:

  let rec free_vars = function
    | EVar v, _ -> Var.Set.singleton v
    | EAbs { binder; _ }, _ ->
      let vs, body = Bindlib.unmbind binder in
      Array.fold_right Var.Set.remove vs (free_vars body)
    | e ->
      shallow_fold (fun e -> Var.Set.union (free_vars e)) e Var.Set.empty

Shallow mapping similar to map, but additionally allows to gather an accumulator bottom-up. acc is the accumulator value returned on terminal nodes, and join is used to merge accumulators from the different sub-terms of an expression. acc is assumed to be a neutral element for join. Typically used with a set of variables used in the rewrite:

  let rec rewrite e =
    match Marked.unmark e with
    | Specific_case ->
      Var.Set.singleton x, some_rewrite_fun e
    | _ ->
      Expr.map_gather ~acc:Var.Set.empty ~join:Var.Set.union ~f:rewrite e
}]


See [Lcalc.closure_conversion] for a real-world example. 

make_default ?pos exceptions just cons builds a term semantically equivalent to <exceptions | just :- cons> (the EDefault constructor) while avoiding redundant nested constructions. The position is extracted from just by default.

Note that, due to the simplifications taking place, the result might not be of the form EDefault:

• <true :- x> is rewritten as x
• <ex | true :- def>, when def is a default term <j :- c> without exceptions, is collapsed into <ex | def>
• <ex | false :- _>, when ex is a single exception, is rewritten as ex

Builds a tuple; the mark argument is only used as witness and for position when building 0-uples

Removes all calls to Log unary operators in the AST, replacing them by their argument.

Determines if two expressions are equal, omitting their position information

Standard comparison function, suitable for e.g. Set.Make. Ignores position information

Used by the optimizer to know when to stop