diff options
Diffstat (limited to 'compiler/PureUtils.ml')
-rw-r--r-- | compiler/PureUtils.ml | 128 |
1 files changed, 72 insertions, 56 deletions
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml index 81e3fbe1..4bc90872 100644 --- a/compiler/PureUtils.ml +++ b/compiler/PureUtils.ml @@ -1,4 +1,5 @@ open Pure +open Errors (** Default logger *) let log = Logging.pure_utils_log @@ -74,10 +75,10 @@ let inputs_info_is_wf (info : inputs_info) : bool = let fun_sig_info_is_wf (info : fun_sig_info) : bool = inputs_info_is_wf info.fwd_info -let dest_arrow_ty (ty : ty) : ty * ty = +let dest_arrow_ty (meta : Meta.meta) (ty : ty) : ty * ty = match ty with | TArrow (arg_ty, ret_ty) -> (arg_ty, ret_ty) - | _ -> raise (Failure "Unreachable") + | _ -> craise __FILE__ __LINE__ meta "Not an arrow type" let compute_literal_type (cv : literal) : literal_type = match cv with @@ -213,30 +214,31 @@ 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 (e : texpression) : bool = +let rec let_group_requires_parentheses (meta : Meta.meta) (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 next_e + if monadic then true else let_group_requires_parentheses meta next_e | Switch (_, _) -> false - | Meta (_, next_e) -> let_group_requires_parentheses next_e + | Meta (_, next_e) -> let_group_requires_parentheses meta next_e | Lambda (_, _) -> (* Being conservative here *) true | Loop _ -> (* Should have been eliminated *) - raise (Failure "Unreachable") + craise __FILE__ __LINE__ meta "Unreachable" -let texpression_requires_parentheses e = +let texpression_requires_parentheses meta e = match !Config.backend with | FStar | Lean -> false - | Coq | HOL4 -> let_group_requires_parentheses e + | Coq | HOL4 -> let_group_requires_parentheses meta e let is_var (e : texpression) : bool = match e.e with Var _ -> true | _ -> false -let as_var (e : texpression) : VarId.id = - match e.e with Var v -> v | _ -> raise (Failure "Unreachable") +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 is_cvar (e : texpression) : bool = match e.e with CVar _ -> true | _ -> false @@ -247,10 +249,10 @@ let is_global (e : texpression) : bool = let is_const (e : texpression) : bool = match e.e with Const _ -> true | _ -> false -let ty_as_adt (ty : ty) : type_id * generic_args = +let ty_as_adt (meta : Meta.meta) (ty : ty) : type_id * generic_args = match ty with | TAdt (id, generics) -> (id, generics) - | _ -> raise (Failure "Unreachable") + | _ -> craise __FILE__ __LINE__ meta "Not an ADT" (** Remove the external occurrences of {!Meta} *) let rec unmeta (e : texpression) : texpression = @@ -287,13 +289,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 (e : texpression) : +let destruct_lets_no_interleave (meta : Meta.meta) (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 - | _ -> raise (Failure "Unreachable") + | _ -> craise __FILE__ __LINE__ meta "Not a let-binding" in (* Destruct the rest *) let rec destruct_lets (e : texpression) : @@ -320,14 +322,15 @@ let destruct_apps (e : texpression) : texpression * texpression list = aux [] e (** Make an [App (app, arg)] expression *) -let mk_app (app : texpression) (arg : texpression) : texpression = +let mk_app (meta : Meta.meta) (app : texpression) (arg : texpression) : + texpression = let raise_or_return msg = - if !Config.fail_hard then raise (Failure msg) - else - let e = App (app, arg) in - (* Dummy type - TODO: introduce an error type *) - let ty = app.ty in - { e; ty } + (* We shouldn't get there, so we save an error (and eventually raise an exception) *) + save_error __FILE__ __LINE__ (Some meta) msg; + let e = App (app, arg) in + (* Dummy type - TODO: introduce an error type *) + let ty = app.ty in + { e; ty } in match app.ty with | TArrow (ty0, ty1) -> @@ -343,8 +346,9 @@ let mk_app (app : texpression) (arg : texpression) : texpression = | _ -> raise_or_return "Expected an arrow type" (** The reverse of {!destruct_apps} *) -let mk_apps (app : texpression) (args : texpression list) : texpression = - List.fold_left (fun app arg -> mk_app app arg) app args +let mk_apps (meta : Meta.meta) (app : texpression) (args : texpression list) : + texpression = + List.fold_left (fun app arg -> mk_app meta app arg) app args (** Destruct an expression into a qualif identifier and a list of arguments, * if possible *) @@ -367,28 +371,29 @@ let opt_destruct_function_call (e : texpression) : | FunOrOp fun_id -> Some (fun_id, qualif.generics, args) | _ -> None) -let opt_destruct_result (ty : ty) : ty option = +let opt_destruct_result (meta : Meta.meta) (ty : ty) : ty option = match ty with | TAdt (TAssumed TResult, generics) -> - assert (generics.const_generics = []); - assert (generics.trait_refs = []); + sanity_check __FILE__ __LINE__ (generics.const_generics = []) meta; + sanity_check __FILE__ __LINE__ (generics.trait_refs = []) meta; Some (Collections.List.to_cons_nil generics.types) | _ -> None -let destruct_result (ty : ty) : ty = Option.get (opt_destruct_result ty) +let destruct_result (meta : Meta.meta) (ty : ty) : ty = + Option.get (opt_destruct_result meta ty) -let opt_destruct_tuple (ty : ty) : ty list option = +let opt_destruct_tuple (meta : Meta.meta) (ty : ty) : ty list option = match ty with | TAdt (TTuple, generics) -> - assert (generics.const_generics = []); - assert (generics.trait_refs = []); + sanity_check __FILE__ __LINE__ (generics.const_generics = []) meta; + sanity_check __FILE__ __LINE__ (generics.trait_refs = []) meta; Some generics.types | _ -> None -let destruct_arrow (ty : ty) : ty * ty = +let destruct_arrow (meta : Meta.meta) (ty : ty) : ty * ty = match ty with | TArrow (ty0, ty1) -> (ty0, ty1) - | _ -> raise (Failure "Not an arrow type") + | _ -> craise __FILE__ __LINE__ meta "Not an arrow type" let rec destruct_arrows (ty : ty) : ty list * ty = match ty with @@ -422,17 +427,21 @@ 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 (scrut : texpression) (sb : switch_body) : texpression = +let mk_switch (meta : Meta.meta) (scrut : texpression) (sb : switch_body) : + texpression = (* Sanity check: the scrutinee has the proper type *) (match sb with - | If (_, _) -> assert (scrut.ty = TLiteral TBool) + | If (_, _) -> sanity_check __FILE__ __LINE__ (scrut.ty = TLiteral TBool) meta | Match branches -> List.iter - (fun (b : match_branch) -> assert (b.pat.ty = scrut.ty)) + (fun (b : match_branch) -> + sanity_check __FILE__ __LINE__ (b.pat.ty = scrut.ty) meta) branches); (* Sanity check: all the branches have the same type *) let ty = get_switch_body_ty sb in - iter_switch_body_branches (fun e -> assert (e.ty = ty)) sb; + iter_switch_body_branches + (fun e -> sanity_check __FILE__ __LINE__ (e.ty = ty) meta) + sb; (* Put together *) let e = Switch (scrut, sb) in { e; ty } @@ -497,7 +506,8 @@ let mk_simpl_tuple_pattern (vl : typed_pattern list) : typed_pattern = { value; ty } (** Similar to {!mk_simpl_tuple_pattern} *) -let mk_simpl_tuple_texpression (vl : texpression list) : texpression = +let mk_simpl_tuple_texpression (meta : Meta.meta) (vl : texpression list) : + texpression = match vl with | [ v ] -> v | _ -> @@ -510,20 +520,22 @@ let mk_simpl_tuple_texpression (vl : texpression list) : texpression = let qualif = { id; generics = mk_generic_args_from_types tys } in (* Put everything together *) let cons = { e = Qualif qualif; ty } in - mk_apps cons vl + mk_apps meta 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 (t : ty) : T.integer_type = +let ty_as_integer (meta : Meta.meta) (t : ty) : T.integer_type = match t with | TLiteral (TInteger int_ty) -> int_ty - | _ -> raise (Failure "Unreachable") + | _ -> craise __FILE__ __LINE__ meta "Unreachable" -let ty_as_literal (t : ty) : T.literal_type = - match t with TLiteral ty -> ty | _ -> raise (Failure "Unreachable") +let ty_as_literal (meta : Meta.meta) (t : ty) : T.literal_type = + match t with + | TLiteral ty -> ty + | _ -> craise __FILE__ __LINE__ meta "Unreachable" let mk_state_ty : ty = TAdt (TAssumed TState, empty_generic_args) @@ -540,15 +552,16 @@ let mk_error (error : VariantId.id) : texpression = let e = Qualif qualif in { e; ty } -let unwrap_result_ty (ty : ty) : ty = +let unwrap_result_ty (meta : Meta.meta) (ty : ty) : ty = match ty with | TAdt ( TAssumed TResult, { types = [ ty ]; const_generics = []; trait_refs = [] } ) -> ty - | _ -> raise (Failure "not a result type") + | _ -> craise __FILE__ __LINE__ meta "not a result type" -let mk_result_fail_texpression (error : texpression) (ty : ty) : texpression = +let mk_result_fail_texpression (meta : Meta.meta) (error : texpression) + (ty : ty) : texpression = let type_args = [ ty ] in let ty = TAdt (TAssumed TResult, mk_generic_args_from_types type_args) in let id = @@ -558,14 +571,15 @@ let mk_result_fail_texpression (error : texpression) (ty : ty) : 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 cons error + mk_app meta cons error -let mk_result_fail_texpression_with_error_id (error : VariantId.id) (ty : ty) : - texpression = +let mk_result_fail_texpression_with_error_id (meta : Meta.meta) + (error : VariantId.id) (ty : ty) : texpression = let error = mk_error error in - mk_result_fail_texpression error ty + mk_result_fail_texpression meta error ty -let mk_result_return_texpression (v : texpression) : texpression = +let mk_result_return_texpression (meta : Meta.meta) (v : texpression) : + texpression = let type_args = [ v.ty ] in let ty = TAdt (TAssumed TResult, mk_generic_args_from_types type_args) in let id = @@ -575,7 +589,7 @@ let mk_result_return_texpression (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 cons v + mk_app meta cons v (** Create a [Fail err] pattern which captures the error *) let mk_result_fail_pattern (error_pat : pattern) (ty : ty) : typed_pattern = @@ -613,21 +627,23 @@ 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 (pat : typed_pattern) : texpression option - = +let rec typed_pattern_to_texpression (meta : Meta.meta) (pat : typed_pattern) : + texpression option = let e_opt = match pat.value with | PatConstant pv -> Some (Const pv) | PatVar (v, _) -> Some (Var v.id) | PatDummy -> None | PatAdt av -> - let fields = List.map typed_pattern_to_texpression av.field_values in + let fields = + List.map (typed_pattern_to_texpression meta) 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 pat.ty in + let adt_id, generics = ty_as_adt meta pat.ty in (* Create the constructor *) let qualif_id = AdtCons { adt_id; variant_id = av.variant_id } in @@ -640,7 +656,7 @@ let rec typed_pattern_to_texpression (pat : typed_pattern) : texpression option let cons = { e = cons_e; ty = cons_ty } in (* Apply the constructor *) - Some (mk_apps cons fields_values).e + Some (mk_apps meta cons fields_values).e in match e_opt with None -> None | Some e -> Some { e; ty = pat.ty } |