Box the expression from the outside

For closed expressions, similar to Bindlib.unbox

Similar to unbox, but with an added assertion check on the expression being closed

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

Same as eabs but without binders' positions

The type of the mark, if typed, is assumed to correspond to the argument type, not the function type

Discards the attributes: useful when copying a mark around.

Discards the attributes: useful when copying a mark around.

Returns an empty mark, using the argument as type witness. Note that the custom part is kept on Custom marks

Adds the given type information only on typed marks

Identity on untyped marks

Raises Invalid_arg on custom marks

Raises Invalid_arg on custom marks

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

Type witness for untyped marks

Type witness for untyped marks

Only used in some backends where enums piggy-back on structs (e.g. C)

Fake structure (there is no corresponding decl) used for categorising PosLit terms in scalc

Shallow mapping on expressions (non recursive): applies the given function to all sub-terms of the given expression, and rebuilds the node.

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 e =
    let rec f e =
      match Mark.remove e with
      | EErrorOnEmpty e1 -> Expr.map ~f e1
      | _ -> Expr.map ~f e
    in
    f e

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 -> Expr.map ~f:translate e

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.

The typ argument, if specified, will apply a transformation both on type annotations, if present, and on types appearing within the AST nodes.

The op argument must be specified for the EAppOp case to be handled.

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. It opens binders unless you avoid sending binders to the function like the example below. 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 Mark.remove 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.

Warning: assumes no polymorphism, no type variables will be quantified

Same as make_abs without binders' positions

m is used as type witness, but both position and type are overriden

Remove thunking around an expression (this assumes it's the right form, raises Invalid_argument otherwise)

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

Removes surface logging calls and EErrorOnEmpty nodes. Shallow function

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

detyplify_application args arg_typs mkapp reconstructs a function application using mkapp, but transforming args into its individual tuple elements in the case where arg_typs expects multiple arguments but args is a single tuple

Simple printing without debug, use Print.expr () instead to follow the command-line debug setting

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

If true, the expression is guaranteed not to have any side-effect (logging, possible failure, or debug print)