diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/Pure.ml | 34 |
1 files changed, 21 insertions, 13 deletions
diff --git a/compiler/Pure.ml b/compiler/Pure.ml index f11397e9..a50dd5f9 100644 --- a/compiler/Pure.ml +++ b/compiler/Pure.ml @@ -281,22 +281,30 @@ and typed_pattern = { value : pattern; ty : ty } type unop = Not | Neg of integer_type | Cast of integer_type * integer_type [@@deriving show, ord] +(** Identifiers of assumed functions that we use only in the pure translation *) +type pure_assumed_fun_id = + | Return (** The monadic return *) + | Fail (** The monadic fail *) + | Assert (** Assertion *) +[@@deriving show, ord] + +(** A function identifier *) type fun_id = - | Regular of A.fun_id * T.RegionGroupId.id option - (** Backward id: [Some] if the function is a backward function, [None] - if it is a forward function. - - TODO: we need to redefine A.fun_id here, to add [fail] and - [return] (important to get a unified treatment of the state-error - monad). For now, when using the state-error monad: extraction - works only if we unfold all the monadic let-bindings, and we - then replace the content of the occurrences of [Return] to also - return the state (which is really super ugly). - TODO: also add Assert... + | FromLlbc of A.fun_id * T.RegionGroupId.id option + (** A function coming from LLBC. + + The region group id is the backward id:: [Some] if the function is a + backward function, [None] if it is a forward function. *) + | Pure of pure_assumed_fun_id + (** A function only used in the pure translation *) +[@@deriving show, ord] + +(** A function or an operation id *) +type fun_or_op_id = + | Fun of fun_id | Unop of unop | Binop of E.binop * integer_type - | Assert [@@deriving show, ord] (** An identifier for an ADT constructor *) @@ -309,7 +317,7 @@ type adt_cons_id = { adt_id : type_id; variant_id : variant_id option } type projection = { adt_id : type_id; field_id : FieldId.id } [@@deriving show] type qualif_id = - | Func of fun_id + | FunOrOp of fun_or_op_id (** A function or an operation *) | Global of GlobalDeclId.id | AdtCons of adt_cons_id (** A function or ADT constructor identifier *) | Proj of projection (** Field projector *) |