diff options
Diffstat (limited to '')
-rw-r--r-- | compiler/Errors.ml | 5 | ||||
-rw-r--r-- | compiler/Extract.ml | 8 | ||||
-rw-r--r-- | compiler/ExtractBase.ml | 4 | ||||
-rw-r--r-- | compiler/ExtractTypes.ml | 1 | ||||
-rw-r--r-- | compiler/Interpreter.ml | 3 | ||||
-rw-r--r-- | compiler/PrintPure.ml | 4 | ||||
-rw-r--r-- | compiler/Pure.ml | 8 | ||||
-rw-r--r-- | compiler/PureMicroPasses.ml | 4 | ||||
-rw-r--r-- | compiler/PureTypeCheck.ml | 1 | ||||
-rw-r--r-- | compiler/PureUtils.ml | 3 | ||||
-rw-r--r-- | compiler/SymbolicAst.ml | 1 | ||||
-rw-r--r-- | compiler/SymbolicToPure.ml | 4 |
12 files changed, 41 insertions, 5 deletions
diff --git a/compiler/Errors.ml b/compiler/Errors.ml index 53e56c44..30887593 100644 --- a/compiler/Errors.ml +++ b/compiler/Errors.ml @@ -1,6 +1,7 @@ let log = Logging.errors_log -let meta_to_string (span : Meta.span) = +let meta_to_string (meta : Meta.meta) = + let span = meta.span in let file = match span.file with Virtual s | Local s -> s in let loc_to_string (l : Meta.loc) : string = string_of_int l.line ^ ":" ^ string_of_int l.col @@ -10,7 +11,7 @@ let meta_to_string (span : Meta.span) = let format_error_message (meta : Meta.meta option) (msg : string) = let meta = - match meta with None -> "" | Some meta -> "\n" ^ meta_to_string meta.span + match meta with None -> "" | Some meta -> "\n" ^ meta_to_string meta in msg ^ meta diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 1f9c9117..ef5d5dce 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -297,6 +297,13 @@ let lets_require_wrap_in_do (meta : Meta.meta) - application argument: [f (exp)] - match/if scrutinee: [if exp then _ else _]/[match exp | _ -> _] *) + +let extract_errors (fmt : F.formatter) = + match !Config.backend with + | FStar | Coq -> F.pp_print_string fmt "admit" + | Lean -> F.pp_print_string fmt "sorry" + | HOL4 -> F.pp_print_string fmt "(* ERROR: could not generate the code *)" + let rec extract_texpression (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) (e : texpression) : unit = match e.e with @@ -323,6 +330,7 @@ let rec extract_texpression (meta : Meta.meta) (ctx : extraction_ctx) | Loop _ -> (* The loop nodes should have been eliminated in {!PureMicroPasses} *) craise __FILE__ __LINE__ meta "Unreachable" + | EError (_, _) -> extract_errors fmt (* Extract an application *or* a top-level qualif (function extraction has * to handle top-level qualifiers, so it seemed more natural to merge the diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 74ac9e32..faca2bde 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -1700,7 +1700,9 @@ let ctx_compute_var_basename (meta : Meta.meta) (ctx : extraction_ctx) | TLiteral lty -> ( match lty with TBool -> "b" | TChar -> "c" | TInteger _ -> "i") | TArrow _ -> "f" - | TTraitType (_, name) -> name_from_type_ident name) + | TTraitType (_, name) -> name_from_type_ident name + | Error -> "@Error") +(* TODO : Check*) (** Generates a type variable basename. *) let ctx_compute_type_var_basename (_ctx : extraction_ctx) (basename : string) : diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml index 1f0abf8a..350866e9 100644 --- a/compiler/ExtractTypes.ml +++ b/compiler/ExtractTypes.ml @@ -566,6 +566,7 @@ let rec extract_ty (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter) "Trait types are not supported yet when generating code for HOL4"; extract_trait_ref meta ctx fmt no_params_tys false trait_ref; F.pp_print_string fmt ("." ^ add_brackets type_name)) + | Error -> craise __FILE__ __LINE__ meta "TODO: Error message?" and extract_trait_ref (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t) (inside : bool) diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml index a65e1663..d0a54750 100644 --- a/compiler/Interpreter.ml +++ b/compiler/Interpreter.ml @@ -612,7 +612,8 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx) (* Evaluate the function *) let symbolic = - eval_function_body config (Option.get fdef.body).body cf_finish ctx + try eval_function_body config (Option.get fdef.body).body cf_finish ctx + with CFailure (meta, msg) -> Some (Error (meta, msg)) in (* Return *) diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index d0c243bb..12d554f2 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -164,6 +164,7 @@ let rec ty_to_string (env : fmt_env) (inside : bool) (ty : ty) : string = let trait_ref = trait_ref_to_string env false trait_ref in let s = trait_ref ^ "::" ^ type_name in if inside then "(" ^ s ^ ")" else s + | Error -> "@Error" and generic_args_to_strings (env : fmt_env) (inside : bool) (generics : generic_args) : string list = @@ -615,6 +616,9 @@ let rec texpression_to_string ?(metadata : Meta.meta option = None) let e = meta_s ^ "\n" ^ indent ^ e in if inside then "(" ^ e ^ ")" else e | MPlace _ -> "(" ^ meta_s ^ " " ^ e ^ ")") + | EError (meta, msg) -> + if Option.is_none meta then msg + else meta_to_string (Option.get meta) ^ " " ^ msg (* TODO formatting *) and app_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (inside : bool) (indent : string) (indent_incr : string) (app : texpression) diff --git a/compiler/Pure.ml b/compiler/Pure.ml index 7de7e0f4..7366783c 100644 --- a/compiler/Pure.ml +++ b/compiler/Pure.ml @@ -285,6 +285,7 @@ type ty = | TArrow of ty * ty | TTraitType of trait_ref * string (** The string is for the name of the associated type *) + | Error and trait_ref = { trait_id : trait_instance_id; @@ -621,6 +622,7 @@ class ['self] iter_expression_base = method visit_qualif : 'env -> qualif -> unit = fun _ _ -> () method visit_loop_id : 'env -> loop_id -> unit = fun _ _ -> () method visit_field_id : 'env -> field_id -> unit = fun _ _ -> () + method visit_meta : 'env -> Meta.meta -> unit = fun _ _ -> () end (** Ancestor for {!map_expression} visitor *) @@ -632,6 +634,7 @@ class ['self] map_expression_base = method visit_qualif : 'env -> qualif -> qualif = fun _ x -> x method visit_loop_id : 'env -> loop_id -> loop_id = fun _ x -> x method visit_field_id : 'env -> field_id -> field_id = fun _ x -> x + method visit_meta : 'env -> Meta.meta -> Meta.meta = fun _ x -> x end (** Ancestor for {!reduce_expression} visitor *) @@ -643,6 +646,7 @@ class virtual ['self] reduce_expression_base = method visit_qualif : 'env -> qualif -> 'a = fun _ _ -> self#zero method visit_loop_id : 'env -> loop_id -> 'a = fun _ _ -> self#zero method visit_field_id : 'env -> field_id -> 'a = fun _ _ -> self#zero + method visit_meta : 'env -> Meta.meta -> 'a = fun _ _ -> self#zero end (** Ancestor for {!mapreduce_expression} visitor *) @@ -662,6 +666,9 @@ class virtual ['self] mapreduce_expression_base = method visit_field_id : 'env -> field_id -> field_id * 'a = fun _ x -> (x, self#zero) + + method visit_meta : 'env -> Meta.meta -> Meta.meta * 'a = + fun _ x -> (x, self#zero) end (** **Rk.:** here, {!expression} is not at all equivalent to the expressions @@ -726,6 +733,7 @@ type expression = | Loop of loop (** See the comments for {!loop} *) | StructUpdate of struct_update (** See the comments for {!struct_update} *) | Meta of (emeta[@opaque]) * texpression (** Meta-information *) + | EError of Meta.meta option * string and switch_body = If of texpression * texpression | Match of match_branch list and match_branch = { pat : typed_pattern; branch : texpression } diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index 9fa07029..ebc5c65f 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -416,6 +416,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl = | StructUpdate supd -> update_struct_update supd ctx | Lambda (lb, e) -> update_lambda lb e ctx | Meta (meta, e) -> update_emeta meta e ctx + | EError (meta, msg) -> (ctx, EError (meta, msg)) in (ctx, { e; ty }) (* *) @@ -1006,7 +1007,8 @@ let filter_useless (_ctx : trans_ctx) (def : fun_decl) : fun_decl = match e with | Var _ | CVar _ | Const _ | App _ | Qualif _ | Meta (_, _) - | StructUpdate _ | Lambda _ -> + | StructUpdate _ | Lambda _ + | EError (_, _) -> super#visit_expression env e | Switch (scrut, switch) -> ( match switch with diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml index 53ff8983..098e2564 100644 --- a/compiler/PureTypeCheck.ml +++ b/compiler/PureTypeCheck.ml @@ -238,3 +238,4 @@ let rec check_texpression (meta : Meta.meta) (ctx : tc_ctx) (e : texpression) : | Meta (_, e_next) -> sanity_check __FILE__ __LINE__ (e_next.ty = e.ty) meta; check_texpression meta ctx e_next + | EError (meta, msg) -> craise_opt_meta __FILE__ __LINE__ meta msg diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml index 4bc90872..87f0b5f7 100644 --- a/compiler/PureUtils.ml +++ b/compiler/PureUtils.ml @@ -228,6 +228,9 @@ let rec let_group_requires_parentheses (meta : Meta.meta) (e : texpression) : | Loop _ -> (* Should have been eliminated *) craise __FILE__ __LINE__ meta "Unreachable" + | EError (meta, msg) -> + craise_opt_meta __FILE__ __LINE__ meta + msg (* TODO : check if true should'nt be returned instead ? *) let texpression_requires_parentheses meta e = match !Config.backend with diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml index e164fd49..f15a2c23 100644 --- a/compiler/SymbolicAst.ml +++ b/compiler/SymbolicAst.ml @@ -212,6 +212,7 @@ type expression = TODO: merge this with Return. *) | Meta of emeta * expression (** Meta information *) + | Error of Meta.meta option * string and loop = { loop_id : loop_id; diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 0c30f44c..1701891f 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -1963,6 +1963,9 @@ let eval_ctx_to_symbolic_assignments_info (ctx : bs_ctx) (* Return the computed information *) !info +let translate_meta (meta : Meta.meta option) (msg : string) : texpression = + { e = EError (meta, msg); ty = Error } + let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression = match e with | S.Return (ectx, opt_v) -> @@ -1989,6 +1992,7 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression = *) translate_forward_end ectx loop_input_values e back_e ctx | Loop loop -> translate_loop loop ctx + | Error (meta, msg) -> translate_meta meta msg and translate_panic (ctx : bs_ctx) : texpression = (* Here we use the function return type - note that it is ok because |