summaryrefslogtreecommitdiff
path: root/compiler/PureUtils.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/PureUtils.ml')
-rw-r--r--compiler/PureUtils.ml124
1 files changed, 62 insertions, 62 deletions
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 82a578d9..e7dcd933 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -80,10 +80,10 @@ let opt_dest_arrow_ty (ty : ty) : (ty * ty) option =
let is_arrow_ty (ty : ty) : bool = Option.is_some (opt_dest_arrow_ty ty)
-let dest_arrow_ty (meta : Meta.meta) (ty : ty) : ty * ty =
+let dest_arrow_ty (span : Meta.span) (ty : ty) : ty * ty =
match opt_dest_arrow_ty ty with
| Some (arg_ty, ret_ty) -> (arg_ty, ret_ty)
- | None -> craise __FILE__ __LINE__ meta "Not an arrow type"
+ | None -> craise __FILE__ __LINE__ span "Not an arrow type"
let compute_literal_type (cv : literal) : literal_type =
match cv with
@@ -91,7 +91,7 @@ let compute_literal_type (cv : literal) : literal_type =
| VBool _ -> TBool
| VChar _ -> TChar
| VStr _ | VByteStr _ ->
- craise_opt_meta __FILE__ __LINE__ None
+ craise_opt_span __FILE__ __LINE__ None
"String and byte string literals are unsupported"
let var_get_id (v : var) : VarId.id = v.id
@@ -222,34 +222,34 @@ let fun_sig_substitute (subst : subst) (sg : fun_sig) : inst_fun_sig =
Rem.: this function will *fail* if there are {!Pure.Loop}
nodes (you should call it on an expression where those nodes have been eliminated).
*)
-let rec let_group_requires_parentheses (meta : Meta.meta) (e : texpression) :
+let rec let_group_requires_parentheses (span : Meta.span) (e : texpression) :
bool =
match e.e with
| Var _ | CVar _ | Const _ | App _ | Qualif _ | StructUpdate _ -> false
| Let (monadic, _, _, next_e) ->
- if monadic then true else let_group_requires_parentheses meta next_e
+ if monadic then true else let_group_requires_parentheses span next_e
| Switch (_, _) -> false
- | Meta (_, next_e) -> let_group_requires_parentheses meta next_e
+ | Meta (_, next_e) -> let_group_requires_parentheses span next_e
| Lambda (_, _) ->
(* Being conservative here *)
true
| Loop _ ->
(* Should have been eliminated *)
- craise __FILE__ __LINE__ meta "Unreachable"
- | EError (meta, msg) ->
- craise_opt_meta __FILE__ __LINE__ meta
+ craise __FILE__ __LINE__ span "Unreachable"
+ | EError (span, msg) ->
+ craise_opt_span __FILE__ __LINE__ span
msg (* TODO : check if true should'nt be returned instead ? *)
-let texpression_requires_parentheses meta e =
+let texpression_requires_parentheses span e =
match !Config.backend with
| FStar | Lean -> false
- | Coq | HOL4 -> let_group_requires_parentheses meta e
+ | Coq | HOL4 -> let_group_requires_parentheses span e
let is_var (e : texpression) : bool =
match e.e with Var _ -> true | _ -> false
-let as_var (meta : Meta.meta) (e : texpression) : VarId.id =
- match e.e with Var v -> v | _ -> craise __FILE__ __LINE__ meta "Not a var"
+let as_var (span : Meta.span) (e : texpression) : VarId.id =
+ match e.e with Var v -> v | _ -> craise __FILE__ __LINE__ span "Not a var"
let is_cvar (e : texpression) : bool =
match e.e with CVar _ -> true | _ -> false
@@ -260,17 +260,17 @@ let is_global (e : texpression) : bool =
let is_const (e : texpression) : bool =
match e.e with Const _ -> true | _ -> false
-let ty_as_adt (meta : Meta.meta) (ty : ty) : type_id * generic_args =
+let ty_as_adt (span : Meta.span) (ty : ty) : type_id * generic_args =
match ty with
| TAdt (id, generics) -> (id, generics)
- | _ -> craise __FILE__ __LINE__ meta "Not an ADT"
+ | _ -> craise __FILE__ __LINE__ span "Not an ADT"
(** Remove the external occurrences of {!Meta} *)
-let rec unmeta (e : texpression) : texpression =
- match e.e with Meta (_, e) -> unmeta e | _ -> e
+let rec unspan (e : texpression) : texpression =
+ match e.e with Meta (_, e) -> unspan e | _ -> e
-(** Remove *all* the meta information *)
-let remove_meta (e : texpression) : texpression =
+(** Remove *all* the span information *)
+let remove_span (e : texpression) : texpression =
let obj =
object
inherit [_] map_expression as super
@@ -300,13 +300,13 @@ let rec destruct_lets (e : texpression) :
(** Destruct an expression into a list of nested lets, where there
is no interleaving between monadic and non-monadic lets.
*)
-let destruct_lets_no_interleave (meta : Meta.meta) (e : texpression) :
+let destruct_lets_no_interleave (span : Meta.span) (e : texpression) :
(bool * typed_pattern * texpression) list * texpression =
(* Find the "kind" of the first let (monadic or non-monadic) *)
let m =
match e.e with
| Let (monadic, _, _, _) -> monadic
- | _ -> craise __FILE__ __LINE__ meta "Not a let-binding"
+ | _ -> craise __FILE__ __LINE__ span "Not a let-binding"
in
(* Destruct the rest *)
let rec destruct_lets (e : texpression) :
@@ -333,11 +333,11 @@ let destruct_apps (e : texpression) : texpression * texpression list =
aux [] e
(** Make an [App (app, arg)] expression *)
-let mk_app (meta : Meta.meta) (app : texpression) (arg : texpression) :
+let mk_app (span : Meta.span) (app : texpression) (arg : texpression) :
texpression =
let raise_or_return msg =
(* We shouldn't get there, so we save an error (and eventually raise an exception) *)
- save_error __FILE__ __LINE__ (Some meta) msg;
+ save_error __FILE__ __LINE__ (Some span) msg;
let e = App (app, arg) in
(* Dummy type - TODO: introduce an error type *)
let ty = app.ty in
@@ -357,9 +357,9 @@ let mk_app (meta : Meta.meta) (app : texpression) (arg : texpression) :
| _ -> raise_or_return "Expected an arrow type"
(** The reverse of {!destruct_apps} *)
-let mk_apps (meta : Meta.meta) (app : texpression) (args : texpression list) :
+let mk_apps (span : Meta.span) (app : texpression) (args : texpression list) :
texpression =
- List.fold_left (fun app arg -> mk_app meta app arg) app args
+ List.fold_left (fun app arg -> mk_app span app arg) app args
(** Destruct an expression into a qualif identifier and a list of arguments,
* if possible *)
@@ -382,29 +382,29 @@ let opt_destruct_function_call (e : texpression) :
| FunOrOp fun_id -> Some (fun_id, qualif.generics, args)
| _ -> None)
-let opt_destruct_result (meta : Meta.meta) (ty : ty) : ty option =
+let opt_destruct_result (span : Meta.span) (ty : ty) : ty option =
match ty with
| TAdt (TAssumed TResult, generics) ->
- sanity_check __FILE__ __LINE__ (generics.const_generics = []) meta;
- sanity_check __FILE__ __LINE__ (generics.trait_refs = []) meta;
+ sanity_check __FILE__ __LINE__ (generics.const_generics = []) span;
+ sanity_check __FILE__ __LINE__ (generics.trait_refs = []) span;
Some (Collections.List.to_cons_nil generics.types)
| _ -> None
-let destruct_result (meta : Meta.meta) (ty : ty) : ty =
- Option.get (opt_destruct_result meta ty)
+let destruct_result (span : Meta.span) (ty : ty) : ty =
+ Option.get (opt_destruct_result span ty)
-let opt_destruct_tuple (meta : Meta.meta) (ty : ty) : ty list option =
+let opt_destruct_tuple (span : Meta.span) (ty : ty) : ty list option =
match ty with
| TAdt (TTuple, generics) ->
- sanity_check __FILE__ __LINE__ (generics.const_generics = []) meta;
- sanity_check __FILE__ __LINE__ (generics.trait_refs = []) meta;
+ sanity_check __FILE__ __LINE__ (generics.const_generics = []) span;
+ sanity_check __FILE__ __LINE__ (generics.trait_refs = []) span;
Some generics.types
| _ -> None
-let destruct_arrow (meta : Meta.meta) (ty : ty) : ty * ty =
+let destruct_arrow (span : Meta.span) (ty : ty) : ty * ty =
match ty with
| TArrow (ty0, ty1) -> (ty0, ty1)
- | _ -> craise __FILE__ __LINE__ meta "Not an arrow type"
+ | _ -> craise __FILE__ __LINE__ span "Not an arrow type"
let rec destruct_arrows (ty : ty) : ty list * ty =
match ty with
@@ -438,20 +438,20 @@ let iter_switch_body_branches (f : texpression -> unit) (sb : switch_body) :
f e_else
| Match branches -> List.iter (fun (b : match_branch) -> f b.branch) branches
-let mk_switch (meta : Meta.meta) (scrut : texpression) (sb : switch_body) :
+let mk_switch (span : Meta.span) (scrut : texpression) (sb : switch_body) :
texpression =
(* Sanity check: the scrutinee has the proper type *)
(match sb with
- | If (_, _) -> sanity_check __FILE__ __LINE__ (scrut.ty = TLiteral TBool) meta
+ | If (_, _) -> sanity_check __FILE__ __LINE__ (scrut.ty = TLiteral TBool) span
| Match branches ->
List.iter
(fun (b : match_branch) ->
- sanity_check __FILE__ __LINE__ (b.pat.ty = scrut.ty) meta)
+ sanity_check __FILE__ __LINE__ (b.pat.ty = scrut.ty) span)
branches);
(* Sanity check: all the branches have the same type *)
let ty = get_switch_body_ty sb in
iter_switch_body_branches
- (fun e -> sanity_check __FILE__ __LINE__ (e.ty = ty) meta)
+ (fun e -> sanity_check __FILE__ __LINE__ (e.ty = ty) span)
sb;
(* Put together *)
let e = Switch (scrut, sb) in
@@ -491,13 +491,13 @@ let mk_dummy_pattern (ty : ty) : typed_pattern =
let value = PatDummy in
{ value; ty }
-let mk_emeta (m : emeta) (e : texpression) : texpression =
+let mk_espan (m : espan) (e : texpression) : texpression =
let ty = e.ty in
let e = Meta (m, e) in
{ e; ty }
let mk_mplace_texpression (mp : mplace) (e : texpression) : texpression =
- mk_emeta (MPlace mp) e
+ mk_espan (MPlace mp) e
let mk_opt_mplace_texpression (mp : mplace option) (e : texpression) :
texpression =
@@ -517,7 +517,7 @@ let mk_simpl_tuple_pattern (vl : typed_pattern list) : typed_pattern =
{ value; ty }
(** Similar to {!mk_simpl_tuple_pattern} *)
-let mk_simpl_tuple_texpression (meta : Meta.meta) (vl : texpression list) :
+let mk_simpl_tuple_texpression (span : Meta.span) (vl : texpression list) :
texpression =
match vl with
| [ v ] -> v
@@ -531,22 +531,22 @@ let mk_simpl_tuple_texpression (meta : Meta.meta) (vl : texpression list) :
let qualif = { id; generics = mk_generic_args_from_types tys } in
(* Put everything together *)
let cons = { e = Qualif qualif; ty } in
- mk_apps meta cons vl
+ mk_apps span cons vl
let mk_adt_pattern (adt_ty : ty) (variant_id : VariantId.id option)
(vl : typed_pattern list) : typed_pattern =
let value = PatAdt { variant_id; field_values = vl } in
{ value; ty = adt_ty }
-let ty_as_integer (meta : Meta.meta) (t : ty) : T.integer_type =
+let ty_as_integer (span : Meta.span) (t : ty) : T.integer_type =
match t with
| TLiteral (TInteger int_ty) -> int_ty
- | _ -> craise __FILE__ __LINE__ meta "Unreachable"
+ | _ -> craise __FILE__ __LINE__ span "Unreachable"
-let ty_as_literal (meta : Meta.meta) (t : ty) : T.literal_type =
+let ty_as_literal (span : Meta.span) (t : ty) : T.literal_type =
match t with
| TLiteral ty -> ty
- | _ -> craise __FILE__ __LINE__ meta "Unreachable"
+ | _ -> craise __FILE__ __LINE__ span "Unreachable"
let mk_state_ty : ty = TAdt (TAssumed TState, empty_generic_args)
@@ -563,15 +563,15 @@ let mk_error (error : VariantId.id) : texpression =
let e = Qualif qualif in
{ e; ty }
-let unwrap_result_ty (meta : Meta.meta) (ty : ty) : ty =
+let unwrap_result_ty (span : Meta.span) (ty : ty) : ty =
match ty with
| TAdt
( TAssumed TResult,
{ types = [ ty ]; const_generics = []; trait_refs = [] } ) ->
ty
- | _ -> craise __FILE__ __LINE__ meta "not a result type"
+ | _ -> craise __FILE__ __LINE__ span "not a result type"
-let mk_result_fail_texpression (meta : Meta.meta) (error : texpression)
+let mk_result_fail_texpression (span : Meta.span) (error : texpression)
(ty : ty) : texpression =
let type_args = [ ty ] in
let ty = TAdt (TAssumed TResult, mk_generic_args_from_types type_args) in
@@ -582,14 +582,14 @@ let mk_result_fail_texpression (meta : Meta.meta) (error : texpression)
let cons_e = Qualif qualif in
let cons_ty = mk_arrow error.ty ty in
let cons = { e = cons_e; ty = cons_ty } in
- mk_app meta cons error
+ mk_app span cons error
-let mk_result_fail_texpression_with_error_id (meta : Meta.meta)
+let mk_result_fail_texpression_with_error_id (span : Meta.span)
(error : VariantId.id) (ty : ty) : texpression =
let error = mk_error error in
- mk_result_fail_texpression meta error ty
+ mk_result_fail_texpression span error ty
-let mk_result_ok_texpression (meta : Meta.meta) (v : texpression) : texpression
+let mk_result_ok_texpression (span : Meta.span) (v : texpression) : texpression
=
let type_args = [ v.ty ] in
let ty = TAdt (TAssumed TResult, mk_generic_args_from_types type_args) in
@@ -600,7 +600,7 @@ let mk_result_ok_texpression (meta : Meta.meta) (v : texpression) : texpression
let cons_e = Qualif qualif in
let cons_ty = mk_arrow v.ty ty in
let cons = { e = cons_e; ty = cons_ty } in
- mk_app meta cons v
+ mk_app span cons v
(** Create a [Fail err] pattern which captures the error *)
let mk_result_fail_pattern (error_pat : pattern) (ty : ty) : typed_pattern =
@@ -621,7 +621,7 @@ let mk_result_ok_pattern (v : typed_pattern) : typed_pattern =
let value = PatAdt { variant_id = Some result_ok_id; field_values = [ v ] } in
{ value; ty }
-let opt_unmeta_mplace (e : texpression) : mplace option * texpression =
+let opt_unspan_mplace (e : texpression) : mplace option * texpression =
match e.e with Meta (MPlace mp, e) -> (Some mp, e) | _ -> (None, e)
let mk_state_var (id : VarId.id) : var =
@@ -636,7 +636,7 @@ let mk_fuel_var (id : VarId.id) : var =
let mk_fuel_texpression (id : VarId.id) : texpression =
{ e = Var id; ty = mk_fuel_ty }
-let rec typed_pattern_to_texpression (meta : Meta.meta) (pat : typed_pattern) :
+let rec typed_pattern_to_texpression (span : Meta.span) (pat : typed_pattern) :
texpression option =
let e_opt =
match pat.value with
@@ -645,14 +645,14 @@ let rec typed_pattern_to_texpression (meta : Meta.meta) (pat : typed_pattern) :
| PatDummy -> None
| PatAdt av ->
let fields =
- List.map (typed_pattern_to_texpression meta) av.field_values
+ List.map (typed_pattern_to_texpression span) av.field_values
in
if List.mem None fields then None
else
let fields_values = List.map (fun e -> Option.get e) fields in
(* Retrieve the type id and the type args from the pat type (simpler this way *)
- let adt_id, generics = ty_as_adt meta pat.ty in
+ let adt_id, generics = ty_as_adt span pat.ty in
(* Create the constructor *)
let qualif_id = AdtCons { adt_id; variant_id = av.variant_id } in
@@ -665,7 +665,7 @@ let rec typed_pattern_to_texpression (meta : Meta.meta) (pat : typed_pattern) :
let cons = { e = cons_e; ty = cons_ty } in
(* Apply the constructor *)
- Some (mk_apps meta cons fields_values).e
+ Some (mk_apps span cons fields_values).e
in
match e_opt with None -> None | Some e -> Some { e; ty = pat.ty }
@@ -692,7 +692,7 @@ let trait_decl_is_empty (trait_decl : trait_decl) : bool =
is_local = _;
name = _;
llbc_name = _;
- meta = _;
+ span = _;
generics = _;
llbc_generics = _;
preds = _;
@@ -714,7 +714,7 @@ let trait_impl_is_empty (trait_impl : trait_impl) : bool =
is_local = _;
name = _;
llbc_name = _;
- meta = _;
+ span = _;
impl_trait = _;
llbc_impl_trait = _;
generics = _;