Expression (beluga.Synext.Comp.Expression)

type t =

| Variable of {
1. location : Syncom.Location.t;
2. identifier : Syncom.Identifier.t;
}
(*
Variable { identifier = "x"; _ } is the computation-level variable "x".
*)
| Constructor of {
1. location : Syncom.Location.t;
2. identifier : Syncom.Qualified_identifier.t;
}
(*
Constructor { identifier = "c"; _ } is the computation-level constant "c" referring to a constructor.
*)
| Program of {
1. location : Syncom.Location.t;
2. identifier : Syncom.Qualified_identifier.t;
}
(*
Program { identifier = "f"; _ } is the computation-level constant "f" referring to a value.
*)
| Fn of {
1. location : Syncom.Location.t;
2. parameters : (Syncom.Location.t * Syncom.Identifier.t Support.Option.t) Support.List1.t;
3. body : t;
}
(*
Fn { parameters = ["x1"; "x2"; ...; "xn"]; body; _ } is the computation-level abstraction fn x1, x2, ..., xn => body.
*)
| Mlam of {
1. location : Syncom.Location.t;
2. parameters : (Syncom.Location.t * (Syncom.Identifier.t Support.Option.t * [ `Plain | `Hash | `Dollar ])) Support.List1.t;
3. body : t;
}
(*
Mlam { parameters = ["X1"; "X2"; ...; "Xn"]; body; _ } is the computation-level abstraction over meta-objects mlam X1, X2, ..., Xn => body.
*)
| Fun of {
1. location : Syncom.Location.t;
2. branches : Cofunction_branch.t Support.List1.t;
}
(*
Fun { branches = [(p1s, e1); (p2, e2); ...; (pn, en)]; _ } is the pattern-matching computation-level abstraction fun p1 => e1 | p2 => e2 | ... | pn => en. Each of p1, p2, ..., pn is a non-empty list of comma-separated copatterns, making this a cofunction.
*)
| Let of {
1. location : Syncom.Location.t;
2. meta_context : Synext__.Synext_definition.Meta.Context.t;
3. pattern : Pattern.t;
4. scrutinee : t;
5. body : t;
}
(*
Let { pattern = p; scrutinee = e1; body = e2; _ } is the pattern-matching let-binding expression let p = e1 in e2.
*)
| Box of {
1. location : Syncom.Location.t;
2. meta_object : Synext__.Synext_definition.Meta.Object.t;
}
(*
Box { meta_object = C; _ } is the meta-object expression [C].
*)
| Impossible of {
1. location : Syncom.Location.t;
2. scrutinee : t;
}
(*
Impossible { expression = e; _ } is the pattern-matching with no branches impossible e.
*)
| Case of {
1. location : Syncom.Location.t;
2. scrutinee : t;
3. check_coverage : Stdlib.Bool.t;
4. branches : Case_branch.t Support.List1.t;
}
(*
Case { scrutinee = e; branches = [(p1, e1); (p2, e2); ...; (pn, en)]; check_coverage; _ } is the pattern-matching expression case e of p1 => e1 | p2 => e2 | ... | pn => en.
If check_coverage = false, then coverage-checking is disabled for this case-expression.
*)
| Tuple of {
1. location : Syncom.Location.t;
2. elements : t Support.List2.t;
}
(*
Tuple { elements = [e1; e2; ...; en]; _ } is the tuple expression (e1, e2, ..., en).
*)
| Hole of {
1. location : Syncom.Location.t;
2. label : Syncom.Identifier.t Support.Option.t;
}
(*
Hole { label = Option.Some "x"; _ } is the hole ?x ranging over computation-level expressions.
*)
| Box_hole of {
1. location : Syncom.Location.t;
}
(*
Box_hole _ is the hole _ ranging over meta-objects.
*)
| Application of {
1. location : Syncom.Location.t;
2. applicand : t;
3. arguments : t Support.List1.t;
}
(*
Application { applicand; arguments; _ } the application of applicand with arguments.
If applicand = Expression.Program _ | Expression.Constructor _ with resolved operator description operator, then List1.length arguments = Operator.arity operator.
*)
| Observation of {
1. location : Syncom.Location.t;
2. scrutinee : t;
3. destructor : Syncom.Qualified_identifier.t;
}
(*
Observation { scrutinee = e; destructor = "c"; _ } is the observation e .c.
*)
| Type_annotated of {
1. location : Syncom.Location.t;
2. expression : t;
3. typ : Typ.t;
}
(*
Type_annotated { expression = e; typ = t; _ } is the type-annotated computation-level expression e : t.
*)