diff options
Diffstat (limited to 'compiler/Translate.ml')
| -rw-r--r-- | compiler/Translate.ml | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 60ae99f9..02d495c0 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -127,7 +127,7 @@ let translate_function_to_pure_aux (trans_ctx : trans_ctx) let ctx = { - meta = fdef.item_meta.meta; + span = fdef.item_meta.span; decls_ctx = trans_ctx; SymbolicToPure.bid = None; sg; @@ -179,7 +179,7 @@ let translate_function_to_pure_aux (trans_ctx : trans_ctx) SymbolicToPure.fresh_named_vars_for_symbolic_values input_svs ctx in { ctx with forward_inputs } - | _ -> craise __FILE__ __LINE__ fdef.item_meta.meta "Unreachable" + | _ -> craise __FILE__ __LINE__ fdef.item_meta.span "Unreachable" in (* Add the backward inputs *) @@ -204,10 +204,10 @@ let translate_function_to_pure (trans_ctx : trans_ctx) try Some (translate_function_to_pure_aux trans_ctx pure_type_decls fun_dsigs fdef) - with CFailure (meta, _) -> + with CFailure (span, _) -> let name = name_to_string trans_ctx fdef.name in let name_pattern = name_to_pattern_string trans_ctx fdef.name in - save_error __FILE__ __LINE__ meta + save_error __FILE__ __LINE__ span ("Could not translate the function '" ^ name ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'"); None @@ -244,10 +244,10 @@ let translate_crate_to_pure (crate : crate) : ( fdef.def_id, SymbolicToPure.translate_fun_sig_from_decl_to_decomposed trans_ctx fdef ) - with CFailure (meta, _) -> + with CFailure (span, _) -> let name = name_to_string trans_ctx fdef.name in let name_pattern = name_to_pattern_string trans_ctx fdef.name in - save_error __FILE__ __LINE__ meta + save_error __FILE__ __LINE__ span ("Could not translate the function signature of '" ^ name ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'"); @@ -267,10 +267,10 @@ let translate_crate_to_pure (crate : crate) : List.filter_map (fun d -> try Some (SymbolicToPure.translate_trait_decl trans_ctx d) - with CFailure (meta, _) -> + with CFailure (span, _) -> let name = name_to_string trans_ctx d.name in let name_pattern = name_to_pattern_string trans_ctx d.name in - save_error __FILE__ __LINE__ meta + save_error __FILE__ __LINE__ span ("Could not translate the trait declaration '" ^ name ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'" ); @@ -283,10 +283,10 @@ let translate_crate_to_pure (crate : crate) : List.filter_map (fun d -> try Some (SymbolicToPure.translate_trait_impl trans_ctx d) - with CFailure (meta, _) -> + with CFailure (span, _) -> let name = name_to_string trans_ctx d.name in let name_pattern = name_to_pattern_string trans_ctx d.name in - save_error __FILE__ __LINE__ meta + save_error __FILE__ __LINE__ span ("Could not translate the trait instance '" ^ name ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'" ); @@ -496,7 +496,7 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) let global_decls = ctx.trans_ctx.global_ctx.global_decls in let global = GlobalDeclId.Map.find id global_decls in let trans = FunDeclId.Map.find global.body ctx.trans_funs in - sanity_check __FILE__ __LINE__ (trans.loops = []) global.item_meta.meta; + sanity_check __FILE__ __LINE__ (trans.loops = []) global.item_meta.span; let body = trans.f in let is_opaque = Option.is_none body.Pure.body in @@ -521,10 +521,10 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) *) let global = try Some (SymbolicToPure.translate_global ctx.trans_ctx global) - with CFailure (meta, _) -> + with CFailure (span, _) -> let name = name_to_string ctx.trans_ctx global.name in let name_pattern = name_to_pattern_string ctx.trans_ctx global.name in - save_error __FILE__ __LINE__ meta + save_error __FILE__ __LINE__ span ("Could not translate the global declaration '" ^ name ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'"); None @@ -810,7 +810,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) export_functions_group pure_funs | GlobalGroup id -> export_global id | TraitDeclGroup (RecGroup _ids) -> - craise_opt_meta __FILE__ __LINE__ None + craise_opt_span __FILE__ __LINE__ None "Mutually recursive trait declarations are not supported" | TraitDeclGroup (NonRecGroup id) -> (* TODO: update to extract groups *) |