diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ExtractToFStar.ml | 24 | ||||
| -rw-r--r-- | src/PureToExtract.ml | 16 |
2 files changed, 17 insertions, 23 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index f2c481c0..7f271f02 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -797,7 +797,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) (keep_fwd : bool) (** Simply add the global name to the context. *) let extract_global_decl_register_names (ctx : extraction_ctx) (def : A.global_decl) : extraction_ctx = - ctx_add_global_decl def ctx + ctx_add_global_decl_body def ctx (** The following function factorizes the extraction of ADT values. @@ -852,7 +852,7 @@ let extract_adt_g_value (* Extract globals in the same way as variables *) let extract_global (ctx : extraction_ctx) (fmt : F.formatter) (id : A.GlobalDeclId.id) : unit = - F.pp_print_string fmt (ctx_get_global_decl id ctx) + F.pp_print_string fmt (ctx_get_global id ctx) (** [inside]: see [extract_ty]. @@ -1491,16 +1491,8 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) (* Add breaks to insert new lines between definitions *) F.pp_print_break fmt 0 0 -(* Change the suffix from "_c" to "_body" *) -let global_decl_to_body_name (decl : string) : string = - (* The declaration length without the global suffix *) - let base_len = String.length decl - 2 in - (* TODO: Use String.ends_with instead when a more recent version of OCaml is used *) - assert (String.sub decl base_len 2 = "_c"); - (String.sub decl 0 base_len) ^ "_body" - (** Extract a global definition of the shape "QUALIF NAME : TYPE = BODY" with a custom body extractor *) -let extract_global_definition (ctx : extraction_ctx) (fmt : F.formatter) +let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter) (qualif : fun_decl_qualif) (name : string) (ty : ty) (extract_body : (F.formatter -> unit) Option.t) : unit = @@ -1574,8 +1566,8 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_string fmt ("(** [" ^ Print.global_name_to_string global.name ^ "] *)"); F.pp_print_space fmt (); - let decl_name = ctx_get_global_decl global.def_id ctx in - let body_name = ctx_get_global_body global.def_id ctx in + let decl_name = ctx_get_global global.def_id ctx in + let body_name = ctx_get_function (Regular global.body_id) None ctx in let decl_ty, body_ty = let ty = body.signature.output in @@ -1586,13 +1578,13 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) match body.body with | None -> let qualif = if interface then Val else AssumeVal in - extract_global_definition ctx fmt qualif decl_name decl_ty None + extract_global_decl_body ctx fmt qualif decl_name decl_ty None | Some body -> - extract_global_definition ctx fmt Let body_name body_ty (Some (fun fmt -> + extract_global_decl_body ctx fmt Let body_name body_ty (Some (fun fmt -> extract_texpression ctx fmt false body.body )); F.pp_print_break fmt 0 0; - extract_global_definition ctx fmt Let decl_name decl_ty (Some (fun fmt -> + extract_global_decl_body ctx fmt Let decl_name decl_ty (Some (fun fmt -> F.pp_print_string fmt ("eval_global " ^ body_name) )); F.pp_print_break fmt 0 0 diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml index 1dc7eae9..b7d45deb 100644 --- a/src/PureToExtract.ml +++ b/src/PureToExtract.ml @@ -449,12 +449,9 @@ let ctx_get (id : id) (ctx : extraction_ctx) : string = log#serror ("Could not find: " ^ id_to_string id ctx); raise Not_found -let ctx_get_global_decl (id : A.GlobalDeclId.id) (ctx : extraction_ctx) : string = - ctx_get (GlobalId id) ctx ^ "_c" +let ctx_get_global (id : A.GlobalDeclId.id) (ctx : extraction_ctx) : string = + ctx_get (GlobalId id) ctx -let ctx_get_global_body (id : A.GlobalDeclId.id) (ctx : extraction_ctx) : string = - ctx_get (GlobalId id) ctx ^ "_body" - let ctx_get_function (id : A.fun_id) (rg : RegionGroupId.id option) (ctx : extraction_ctx) : string = @@ -585,9 +582,14 @@ let ctx_add_decrases_clause (def : fun_decl) (ctx : extraction_ctx) : let name = ctx.fmt.decreases_clause_name def.def_id def.basename in ctx_add (DecreasesClauseId (A.Regular def.def_id)) name ctx -let ctx_add_global_decl (def : A.global_decl) (ctx : extraction_ctx) : +let ctx_add_global_decl_body (def : A.global_decl) (ctx : extraction_ctx) : extraction_ctx = - ctx_add (GlobalId def.def_id) (ctx.fmt.global_name def.name) ctx + let name = ctx.fmt.global_name def.name in + let decl = GlobalId def.def_id in + let body = FunId (Regular def.body_id, None) in + let ctx = ctx_add decl (name ^ "_c") ctx in + let ctx = ctx_add body (name ^ "_body") ctx in + ctx let ctx_add_fun_decl (trans_group : bool * pure_fun_translation) (def : fun_decl) (ctx : extraction_ctx) : extraction_ctx = |