summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/Extract.ml259
-rw-r--r--compiler/ExtractBase.ml18
-rw-r--r--compiler/Translate.ml103
3 files changed, 203 insertions, 177 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 24f8d141..1057cc3b 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -17,9 +17,9 @@ let int_name (int_ty : integer_type) =
let isize, usize, i_format, u_format =
match !backend with
| FStar | Coq ->
- "isize", "usize", format_of_string "i%d", format_of_string "u%d"
+ ("isize", "usize", format_of_string "i%d", format_of_string "u%d")
| Lean ->
- "ISize", "USize", format_of_string "Int%d", format_of_string "UInt%d"
+ ("ISize", "USize", format_of_string "Int%d", format_of_string "UInt%d")
in
match int_ty with
| Isize -> isize
@@ -39,11 +39,10 @@ let int_name (int_ty : integer_type) =
let unop_name (unop : unop) : string =
match unop with
| Not -> ( match !backend with FStar | Lean -> "not" | Coq -> "negb")
- | Neg (int_ty: integer_type) ->
- begin match !backend with
+ | Neg (int_ty : integer_type) -> (
+ match !backend with
| Lean -> int_name int_ty ^ ".checked_neg"
- | _ -> int_name int_ty ^ "_neg"
- end
+ | _ -> int_name int_ty ^ "_neg")
| Cast _ -> raise (Failure "Unsupported")
(** Small helper to compute the name of a binary operation (note that many
@@ -74,8 +73,8 @@ let keywords () =
let named_binops = [ E.Div; Rem; Add; Sub; Mul ] in
let named_binops =
List.concat_map
- (fun bn -> List.map (fun it -> named_binop_name bn it) T.all_int_types)
- named_binops
+ (fun bn -> List.map (fun it -> named_binop_name bn it) T.all_int_types)
+ named_binops
in
let misc =
match !backend with
@@ -132,8 +131,7 @@ let keywords () =
"tt";
"char_of_byte";
]
- | Lean ->
- [] (* TODO *)
+ | Lean -> [] (* TODO *)
in
List.concat [ named_unops; named_binops; misc ]
@@ -202,7 +200,7 @@ let assumed_llbc_functions :
(VecIndexMut, rg0, "vec_index_mut_back");
]
-let assumed_pure_functions (): (pure_assumed_fun_id * string) list =
+let assumed_pure_functions () : (pure_assumed_fun_id * string) list =
match !backend with
| FStar ->
[
@@ -251,14 +249,12 @@ let extract_unop (extract_expr : bool -> texpression -> unit)
if inside then F.pp_print_string fmt "(";
F.pp_print_string fmt "scalar_cast";
F.pp_print_space fmt ();
- if !backend <> Lean then begin
+ if !backend <> Lean then (
F.pp_print_string fmt
(StringUtils.capitalize_first_letter
(PrintPure.integer_type_to_string src));
- F.pp_print_space fmt ()
- end;
- if !backend = Lean then
- F.pp_print_string fmt (int_name tgt)
+ F.pp_print_space fmt ());
+ if !backend = Lean then F.pp_print_string fmt (int_name tgt)
else
F.pp_print_string fmt
(StringUtils.capitalize_first_letter
@@ -284,7 +280,9 @@ let extract_binop (extract_expr : bool -> texpression -> unit)
| Gt -> ">"
| _ -> raise (Failure "Unreachable")
in
- let binop = match !backend with FStar | Lean -> binop | Coq -> "s" ^ binop in
+ let binop =
+ match !backend with FStar | Lean -> binop | Coq -> "s" ^ binop
+ in
extract_expr false arg0;
F.pp_print_space fmt ();
F.pp_print_string fmt binop;
@@ -301,7 +299,7 @@ let extract_binop (extract_expr : bool -> texpression -> unit)
if inside then F.pp_print_string fmt ")"
let type_decl_kind_to_qualif (kind : decl_kind)
- (type_kind : type_decl_kind option): string =
+ (type_kind : type_decl_kind option) : string =
match !backend with
| FStar -> (
match kind with
@@ -326,7 +324,8 @@ let type_decl_kind_to_qualif (kind : decl_kind)
| _ -> raise (Failure "Unexpected"))
| Lean -> (
match kind with
- | SingleNonRec -> if type_kind = Some Struct then "structure" else "inductive"
+ | SingleNonRec ->
+ if type_kind = Some Struct then "structure" else "inductive"
| SingleRec -> "inductive"
| MutRecFirst -> "mutual inductive"
| MutRecInner -> "inductive"
@@ -364,7 +363,6 @@ let fun_decl_kind_to_qualif (kind : decl_kind) =
| Assumed -> "axiom"
| Declared -> "axiom")
-
(**
[ctx]: we use the context to lookup type definitions, to retrieve type names.
This is used to compute variable names, when they have no basenames: in this
@@ -439,7 +437,9 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
let name = get_type_name name in
let name = List.map to_snake_case name in
let name = String.concat "_" name in
- match !backend with FStar | Lean -> name | Coq -> capitalize_first_letter name
+ match !backend with
+ | FStar | Lean -> name
+ | Coq -> capitalize_first_letter name
in
let type_name name = type_name_to_snake_case name ^ "_t" in
let field_name (def_name : name) (field_id : FieldId.id)
@@ -587,7 +587,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
F.pp_print_string fmt (int_name sv.int_ty);
F.pp_print_string fmt ".ofNatCore ";
Z.pp_print fmt sv.value;
- F.pp_print_string fmt (" (by intlit))"))
+ F.pp_print_string fmt " (by intlit))")
| Bool b ->
let b = if b then "true" else "false" in
F.pp_print_string fmt b
@@ -607,7 +607,6 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
in
F.pp_print_string fmt c;
if inside then F.pp_print_string fmt ")")
-
| String s ->
(* We need to replace all the line breaks *)
let s =
@@ -655,8 +654,7 @@ let print_decl_end_delimiter (fmt : F.formatter) (kind : decl_kind) =
F.pp_print_cut fmt ();
F.pp_print_string fmt ".")
-let unit_name () =
- match !backend with | Lean -> "Unit" | Coq | FStar -> "unit"
+let unit_name () = match !backend with Lean -> "Unit" | Coq | FStar -> "unit"
(** [inside] constrols whether we should add parentheses or not around type
applications (if [true] we add parentheses).
@@ -675,7 +673,9 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
Collections.List.iter_link
(fun () ->
F.pp_print_space fmt ();
- let product = match !backend with FStar -> "&" | Coq -> "*" | Lean -> "×" in
+ let product =
+ match !backend with FStar -> "&" | Coq -> "*" | Lean -> "×"
+ in
F.pp_print_string fmt product;
F.pp_print_space fmt ())
(extract_ty ctx fmt true) tys;
@@ -906,8 +906,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
if !backend = Coq && not is_rec then (
F.pp_print_string fmt (ctx_get_struct (AdtId def.def_id) ctx);
F.pp_print_string fmt " ");
- if !backend <> Lean then
- F.pp_print_string fmt "{";
+ if !backend <> Lean then F.pp_print_string fmt "{";
F.pp_print_break fmt 1 ctx.indent_incr;
(* The body itself *)
F.pp_open_hvbox fmt 0;
@@ -920,8 +919,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_string fmt ":";
F.pp_print_space fmt ();
extract_ty ctx fmt false f.field_ty;
- if !backend <> Lean then
- F.pp_print_string fmt ";";
+ if !backend <> Lean then F.pp_print_string fmt ";";
F.pp_close_box fmt ()
in
let fields = FieldId.mapi (fun fid f -> (fid, f)) fields in
@@ -931,8 +929,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
(* Close *)
F.pp_close_box fmt ();
F.pp_print_space fmt ();
- if !backend <> Lean then
- F.pp_print_string fmt "}")
+ if !backend <> Lean then F.pp_print_string fmt "}")
else (
(* We extract for Coq, and we have a recursive record, or a record in
a group of mutually recursive types: we extract it as an inductive type
@@ -945,12 +942,12 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
()
(** Extract a nestable, muti-line comment *)
-let extract_comment (fmt: F.formatter) (s: string): unit =
+let extract_comment (fmt : F.formatter) (s : string) : unit =
match !backend with
| Coq | FStar ->
F.pp_print_string fmt "(** ";
F.pp_print_string fmt s;
- F.pp_print_string fmt " *)";
+ F.pp_print_string fmt " *)"
| Lean ->
F.pp_print_string fmt "/- ";
F.pp_print_string fmt s;
@@ -1002,7 +999,9 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter)
let qualif = ctx.fmt.type_decl_kind_to_qualif kind type_kind in
F.pp_print_string fmt (qualif ^ " " ^ def_name);
(* Print the type parameters *)
- let type_keyword = match !backend with FStar -> "Type0" | Coq | Lean -> "Type" in
+ let type_keyword =
+ match !backend with FStar -> "Type0" | Coq | Lean -> "Type"
+ in
if def.type_params <> [] then (
if use_forall then (
F.pp_print_space fmt ();
@@ -1023,10 +1022,13 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter)
(* Print the "=" if we extract the body*)
if extract_body then (
F.pp_print_space fmt ();
- let eq = match !backend with
+ let eq =
+ match !backend with
| FStar -> "="
| Coq -> ":="
- | Lean -> if type_kind = Some Struct && kind = SingleNonRec then "where" else ":="
+ | Lean ->
+ if type_kind = Some Struct && kind = SingleNonRec then "where"
+ else ":="
in
F.pp_print_string fmt eq)
else (
@@ -1307,18 +1309,15 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
let state_name = ctx_get_assumed_type State ctx in
(* The syntax for Lean and Coq is almost identical. *)
let print_axiom () =
- if !backend = Coq then
- F.pp_print_string fmt "Axiom"
- else
- F.pp_print_string fmt "axiom";
+ if !backend = Coq then F.pp_print_string fmt "Axiom"
+ else F.pp_print_string fmt "axiom";
F.pp_print_space fmt ();
F.pp_print_string fmt state_name;
F.pp_print_space fmt ();
F.pp_print_string fmt ":";
F.pp_print_space fmt ();
F.pp_print_string fmt "Type";
- if !backend = Coq then
- F.pp_print_string fmt "."
+ if !backend = Coq then F.pp_print_string fmt "."
in
(* The kind should be [Assumed] or [Declared] *)
(match kind with
@@ -1336,8 +1335,7 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
F.pp_print_string fmt ":";
F.pp_print_space fmt ();
F.pp_print_string fmt "Type0"
- | Coq | Lean ->
- print_axiom ())
+ | Coq | Lean -> print_axiom ())
| Declared -> (
match !backend with
| FStar ->
@@ -1348,8 +1346,7 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
F.pp_print_string fmt ":";
F.pp_print_space fmt ();
F.pp_print_string fmt "Type0"
- | Coq | Lean ->
- print_axiom ()));
+ | Coq | Lean -> print_axiom ()));
(* Close the box for the definition *)
F.pp_close_box fmt ();
(* Add breaks to insert new lines between definitions *)
@@ -1367,8 +1364,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) (keep_fwd : bool)
if has_decreases_clause def then
let ctx = ctx_add_decreases_clause def ctx in
ctx_add_terminates_clause def ctx
- else
- ctx
+ else ctx
in
let ctx = List.fold_left register_decreases ctx (fwd :: loop_fwds) in
let register_fun ctx f = ctx_add_fun_decl (keep_fwd, def) f ctx in
@@ -1439,8 +1435,7 @@ let extract_adt_g_value
| Some vid ->
if !backend = Lean then
ctx_get_type adt_id ctx ^ "." ^ ctx_get_variant adt_id vid ctx
- else
- ctx_get_variant adt_id vid ctx
+ else ctx_get_variant adt_id vid ctx
| None -> ctx_get_struct adt_id ctx
in
if inside && field_values <> [] then F.pp_print_string fmt "(";
@@ -1579,9 +1574,10 @@ and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter)
(* Open a box for the function call *)
F.pp_open_hovbox fmt ctx.indent_incr;
(* Print the function name *)
- let fun_name = Option.value
- ~default:(ctx_get_function fun_id ctx)
- (ctx_maybe_get (DeclaredId fun_id) ctx)
+ let fun_name =
+ Option.value
+ ~default:(ctx_get_function fun_id ctx)
+ (ctx_maybe_get (DeclaredId fun_id) ctx)
in
F.pp_print_string fmt fun_name;
(* Print the type parameters *)
@@ -1641,18 +1637,26 @@ and extract_adt_cons (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
match adt_cons.variant_id with
| Some vid ->
if !backend = Lean then
- ctx_get_type adt_cons.adt_id ctx ^ "." ^ ctx_get_variant adt_cons.adt_id vid ctx
- else
- ctx_get_variant adt_cons.adt_id vid ctx
+ ctx_get_type adt_cons.adt_id ctx
+ ^ "."
+ ^ ctx_get_variant adt_cons.adt_id vid ctx
+ else ctx_get_variant adt_cons.adt_id vid ctx
| None -> ctx_get_struct adt_cons.adt_id ctx
in
let is_lean_struct = !backend = Lean && adt_cons.variant_id = None in
- if is_lean_struct then
+ if is_lean_struct then (
(* TODO: when only one or two fields differ, considering using the with
syntax (peephole optimization) *)
- let decl_id = match adt_cons.adt_id with | AdtId id -> id | _ -> assert false in
- let def_kind = (TypeDeclId.Map.find decl_id ctx.trans_ctx.type_context.type_decls).kind in
- let fields = match def_kind with | T.Struct fields -> fields | _ -> assert false in
+ let decl_id =
+ match adt_cons.adt_id with AdtId id -> id | _ -> assert false
+ in
+ let def_kind =
+ (TypeDeclId.Map.find decl_id ctx.trans_ctx.type_context.type_decls)
+ .kind
+ in
+ let fields =
+ match def_kind with T.Struct fields -> fields | _ -> assert false
+ in
let fields = FieldId.mapi (fun fid f -> (fid, f)) fields in
F.pp_open_hvbox fmt 0;
F.pp_open_hvbox fmt ctx.indent_incr;
@@ -1663,8 +1667,7 @@ and extract_adt_cons (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
Collections.List.iter_link
(fun () ->
F.pp_print_string fmt ",";
- F.pp_print_space fmt ()
- )
+ F.pp_print_space fmt ())
(fun ((fid, _), e) ->
F.pp_open_hvbox fmt ctx.indent_incr;
let f = ctx_get_field adt_cons.adt_id fid ctx in
@@ -1673,15 +1676,14 @@ and extract_adt_cons (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
F.pp_open_hvbox fmt ctx.indent_incr;
extract_texpression ctx fmt true e;
F.pp_close_box fmt ();
- F.pp_close_box fmt ()
- )
+ F.pp_close_box fmt ())
(List.combine fields args);
F.pp_close_box fmt ();
F.pp_close_box fmt ();
F.pp_close_box fmt ();
F.pp_print_space fmt ();
F.pp_print_string fmt "}";
- F.pp_close_box fmt ()
+ F.pp_close_box fmt ())
else
let use_parentheses = inside && args <> [] in
if use_parentheses then F.pp_print_string fmt "(";
@@ -1708,15 +1710,13 @@ and extract_field_projector (ctx : extraction_ctx) (fmt : F.formatter)
(* Extract the expression *)
extract_texpression ctx fmt true arg;
(* We allow to break where the "." appears (except Lean, it's a syntax error) *)
- if !backend <> Lean then
- F.pp_print_break fmt 0 0;
+ if !backend <> Lean then F.pp_print_break fmt 0 0;
F.pp_print_string fmt ".";
(* If in Coq, the field projection has to be parenthesized *)
(match !backend with
| FStar -> F.pp_print_string fmt field_name
| Coq -> F.pp_print_string fmt ("(" ^ field_name ^ ")")
- | Lean -> F.pp_print_string fmt field_name
- );
+ | Lean -> F.pp_print_string fmt field_name);
(* Close the box *)
F.pp_close_box fmt ()
| arg :: args ->
@@ -1780,7 +1780,11 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
if monadic && !backend = Coq then (
let ctx = extract_typed_pattern ctx fmt true lv in
F.pp_print_space fmt ();
- let arrow = match !backend with FStar -> "<--" | Coq -> "<-" | Lean -> failwith "impossible" in
+ let arrow =
+ match !backend with
+ | Coq -> "<-"
+ | FStar | Lean -> failwith "impossible"
+ in
F.pp_print_string fmt arrow;
F.pp_print_space fmt ();
extract_texpression ctx fmt false re;
@@ -1791,13 +1795,24 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
F.pp_print_space fmt ();
let ctx = extract_typed_pattern ctx fmt true lv in
F.pp_print_space fmt ();
- let eq = match !backend with FStar -> "=" | Coq -> ":=" | Lean -> if monadic then "<-" else ":=" in
+ let eq =
+ match !backend with
+ | FStar -> "="
+ | Coq -> ":="
+ | Lean -> if monadic then "<-" else ":="
+ in
F.pp_print_string fmt eq;
F.pp_print_space fmt ();
extract_texpression ctx fmt false re;
- F.pp_print_space fmt ();
- if !backend <> Lean then
- F.pp_print_string fmt "in";
+ (* In Lean, monadic let-bindings don't require to end with "in".
+
+ TODO: does this work because we add a line break? This is very annoying,
+ because we need to enforce there will be a line break. In order to fix
+ this, we should open a vbox instead of an hov_box.
+ *)
+ if !backend <> Lean then (
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt "in");
ctx)
in
(* Close the box for the let-binding *)
@@ -1809,11 +1824,10 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
let exists_monadic = List.exists (fun (m, _, _) -> m) lets in
(* If Lean, we rely on monadic blocks, so we insert a do and open a new box
immediately *)
- if !backend = Lean && exists_monadic then begin
+ if !backend = Lean && exists_monadic then (
F.pp_open_vbox fmt ctx.indent_incr;
F.pp_print_string fmt "do";
- F.pp_print_space fmt ();
- end;
+ F.pp_print_space fmt ());
let ctx =
List.fold_left
(fun ctx (monadic, lv, re) -> extract_let ctx monadic lv re)
@@ -1826,8 +1840,7 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
(* Close the box for the next expression *)
F.pp_close_box fmt ();
(* do-box (Lean only) *)
- if !backend = Lean && exists_monadic then
- F.pp_close_box fmt ();
+ if !backend = Lean && exists_monadic then F.pp_close_box fmt ();
(* Close parentheses *)
if inside && !backend <> Lean then F.pp_print_string fmt ")";
(* Close the box for the whole expression *)
@@ -1874,9 +1887,7 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
| Coq ->
F.pp_print_string fmt " (";
F.pp_print_cut fmt ()
- | Lean ->
- F.pp_print_cut fmt ()
- );
+ | Lean -> F.pp_print_cut fmt ());
(* Print the branch expression *)
extract_texpression ctx fmt false e_branch;
(* Close the parenthesized expression *)
@@ -1886,8 +1897,7 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
F.pp_print_space fmt ();
F.pp_print_string fmt "end"
| Coq -> F.pp_print_string fmt ")"
- | Lean -> ()
- );
+ | Lean -> ());
(* Close the box for the branch *)
if not parenth then F.pp_close_box fmt ();
(* Close the box for the then/else+branch *)
@@ -1940,8 +1950,7 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
(* End the match *)
F.pp_print_space fmt ();
(* Relying on indentation in Lean *)
- if !backend <> Lean then
- F.pp_print_string fmt "end");
+ if !backend <> Lean then F.pp_print_string fmt "end");
(* Close parentheses *)
if inside then F.pp_print_string fmt ")";
(* Close the box for the whole expression *)
@@ -1978,7 +1987,9 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx)
def.signature.type_params;
F.pp_print_string fmt ":";
F.pp_print_space fmt ();
- let type_keyword = match !backend with FStar -> "Type0" | Coq | Lean -> "Type" in
+ let type_keyword =
+ match !backend with FStar -> "Type0" | Coq | Lean -> "Type"
+ in
F.pp_print_string fmt (type_keyword ^ ")");
(* Close the box for the type parameters *)
F.pp_close_box fmt ());
@@ -2053,7 +2064,8 @@ let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter)
(* Add a break before *)
F.pp_print_break fmt 0 0;
(* Print a comment to link the extracted type to its original rust definition *)
- extract_comment fmt ("[" ^ Print.fun_name_to_string def.basename ^ "]: decreases clause");
+ extract_comment fmt
+ ("[" ^ Print.fun_name_to_string def.basename ^ "]: decreases clause");
F.pp_print_space fmt ();
(* Open a box for the definition, so that whenever possible it gets printed on
* one line *)
@@ -2102,7 +2114,8 @@ let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter)
defines a proof script (allowed to refer to function arguments) that proves
termination.
*)
-let extract_termination_and_decreasing (ctx: extraction_ctx) (fmt: F.formatter) (def: fun_decl): unit =
+let extract_termination_and_decreasing (ctx : extraction_ctx)
+ (fmt : F.formatter) (def : fun_decl) : unit =
assert (!backend = Lean);
(* Retrieve the function name *)
@@ -2111,7 +2124,8 @@ let extract_termination_and_decreasing (ctx: extraction_ctx) (fmt: F.formatter)
(* Add a break before *)
F.pp_print_break fmt 0 0;
(* Print a comment to link the extracted type to its original rust definition *)
- extract_comment fmt ("[" ^ Print.fun_name_to_string def.basename ^ "]: termination measure");
+ extract_comment fmt
+ ("[" ^ Print.fun_name_to_string def.basename ^ "]: termination measure");
F.pp_print_space fmt ();
(* Open a box for the definition, so that whenever possible it gets printed on
* one line *)
@@ -2136,11 +2150,11 @@ let extract_termination_and_decreasing (ctx: extraction_ctx) (fmt: F.formatter)
F.pp_close_box fmt ();
F.pp_print_space fmt ();
(* Tuple of the arguments *)
- let vars = List.map (fun (v: var) -> v.id) def_body.inputs in
+ let vars = List.map (fun (v : var) -> v.id) def_body.inputs in
if List.length vars = 1 then
F.pp_print_string fmt (ctx_get_var (List.hd vars) ctx_body)
- else begin
+ else (
F.pp_open_hovbox fmt 0;
F.pp_print_string fmt "(";
Collections.List.iter_link
@@ -2150,8 +2164,7 @@ let extract_termination_and_decreasing (ctx: extraction_ctx) (fmt: F.formatter)
(fun v -> F.pp_print_string fmt (ctx_get_var v ctx_body))
vars;
F.pp_print_string fmt ")";
- F.pp_close_box fmt ();
- end;
+ F.pp_close_box fmt ());
(* Close the box for "let FUN_NAME (PARAMS) : EFFECT = admit()" *)
F.pp_close_box fmt ();
(* Close the box for the whole definition *)
@@ -2176,9 +2189,9 @@ let extract_termination_and_decreasing (ctx: extraction_ctx) (fmt: F.formatter)
F.pp_open_hovbox fmt 0;
F.pp_print_string fmt "| `(tactic| ";
F.pp_print_string fmt def_name;
- F.pp_print_space fmt ();
- Collections.List.iter_link (F.pp_print_space fmt)
+ List.iter
(fun v ->
+ F.pp_print_space fmt ();
F.pp_print_string fmt "$";
F.pp_print_string fmt (ctx_get_var v ctx_body))
vars;
@@ -2230,10 +2243,9 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
(* *)
let qualif = ctx.fmt.fun_decl_kind_to_qualif kind in
(* For Lean: we generate a record of assumed functions *)
- if not (!backend = Lean && (kind = Assumed || kind = Declared)) then begin
+ if not (!backend = Lean && (kind = Assumed || kind = Declared)) then (
F.pp_print_string fmt qualif;
- F.pp_print_space fmt ()
- end;
+ F.pp_print_space fmt ());
F.pp_print_string fmt def_name;
F.pp_print_space fmt ();
if use_forall then (
@@ -2271,10 +2283,9 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
(* [Tot] *)
if has_decreases_clause then (
assert_backend_supports_decreases_clauses ();
- if !backend = FStar then begin
+ if !backend = FStar then (
F.pp_print_string fmt "Tot";
- F.pp_print_space fmt ()
- end);
+ F.pp_print_space fmt ()));
extract_ty ctx fmt has_decreases_clause def.signature.output;
(* Close the box for the return type *)
F.pp_close_box fmt ();
@@ -2355,26 +2366,28 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
(* Close the outer box for the definition *)
F.pp_close_box fmt ();
(* Termination clause *)
- if has_decreases_clause && !backend = Lean then begin
+ if has_decreases_clause && !backend = Lean then (
let def_body = Option.get def.body in
- let all_vars = List.map (fun (v: var) -> v.id) def_body.inputs in
+ let all_vars = List.map (fun (v : var) -> v.id) def_body.inputs in
let num_fwd_inputs =
def.signature.info.num_fwd_inputs_with_fuel_with_state
in
let vars = Collections.List.prefix num_fwd_inputs all_vars in
(* terminates_by *)
- let terminates_name = ctx_get_terminates_clause def.def_id def.loop_id ctx in
+ let terminates_name =
+ ctx_get_terminates_clause def.def_id def.loop_id ctx
+ in
F.pp_print_break fmt 0 0;
F.pp_open_hovbox fmt ctx.indent_incr;
F.pp_print_string fmt "termination_by";
F.pp_open_hovbox fmt 0;
F.pp_print_space fmt ();
F.pp_print_string fmt def_name;
- F.pp_print_space fmt ();
- Collections.List.iter_link
- (F.pp_print_space fmt)
- (fun v -> F.pp_print_string fmt (ctx_get_var v ctx_body))
+ List.iter
+ (fun v ->
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt (ctx_get_var v ctx_body))
all_vars;
F.pp_print_space fmt ();
F.pp_print_string fmt "=>";
@@ -2382,17 +2395,16 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_open_hovbox fmt 0;
F.pp_print_space fmt ();
F.pp_print_string fmt terminates_name;
- F.pp_print_space fmt ();
List.iter
(fun (p : type_var) ->
let pname = ctx_get_type_var p.index ctx in
- F.pp_print_string fmt pname;
- F.pp_print_space fmt ())
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt pname)
def.signature.type_params;
List.iter
(fun v ->
- F.pp_print_string fmt (ctx_get_var v ctx_body);
- F.pp_print_space fmt ())
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt (ctx_get_var v ctx_body))
vars;
F.pp_close_box fmt ();
F.pp_close_box fmt ();
@@ -2404,14 +2416,13 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_space fmt ();
F.pp_open_hvbox fmt ctx.indent_incr;
F.pp_print_string fmt decreases_name;
- F.pp_print_space fmt ();
- Collections.List.iter_link
- (F.pp_print_space fmt)
- (fun v -> F.pp_print_string fmt (ctx_get_var v ctx_body))
+ List.iter
+ (fun v ->
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt (ctx_get_var v ctx_body))
vars;
F.pp_close_box fmt ();
- F.pp_close_box fmt ()
- end;
+ F.pp_close_box fmt ());
(* Add breaks to insert new lines between definitions *)
F.pp_print_break fmt 0 0
@@ -2561,7 +2572,8 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
(* Add a break before *)
F.pp_print_break fmt 0 0;
(* Print a comment *)
- extract_comment fmt ("Unit test for [" ^ Print.fun_name_to_string def.basename ^ "]");
+ extract_comment fmt
+ ("Unit test for [" ^ Print.fun_name_to_string def.basename ^ "]");
F.pp_print_space fmt ();
(* Open a box for the test *)
F.pp_open_hovbox fmt ctx.indent_incr;
@@ -2613,8 +2625,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_string fmt "=";
F.pp_print_space fmt ();
let success = ctx_get_variant (Assumed Result) result_return_id ctx in
- F.pp_print_string fmt ("." ^ success ^ " ())")
- );
+ F.pp_print_string fmt ("." ^ success ^ " ())"));
(* Close the box for the test *)
F.pp_close_box fmt ();
(* Add a break after *)
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 4c4a9959..e96a80f9 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -51,7 +51,7 @@ type decl_kind =
(** The first definition of a group of mutually-recursive definitions.
F*: [type x0 = ... and x1 = ...]
- Coq: [Fixpoing x0 := ... with x1 := ...]
+ Coq: [Fixpoint x0 := ... with x1 := ...]
*)
| MutRecInner
(** An inner definition in a group of mutually-recursive definitions. *)
@@ -217,7 +217,6 @@ type formatter = {
the same purpose as in {!field:fun_name}.
- loop identifier, if this is for a loop
*)
-
var_basename : StringSet.t -> string option -> ty -> string;
(** Generates a variable basename.
@@ -471,8 +470,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
| GlobalId gid ->
let name = (A.GlobalDeclId.Map.find gid global_decls).name in
"global name: " ^ Print.global_name_to_string name
- | DeclaredId fid
- | FunId fid -> (
+ | DeclaredId fid | FunId fid -> (
match fid with
| FromLlbc (fid, lp_id, rg_id) ->
let fun_name =
@@ -781,12 +779,12 @@ let ctx_add_fun_decl (trans_group : bool * pure_fun_translation)
ctx.fmt.fun_name def.basename def.num_loops def.loop_id num_rgs rg_info
(keep_fwd, num_backs)
in
- let ctx = if def.body = None && !Config.backend = Lean then
- ctx_add
- (DeclaredId (FromLlbc (A.Regular def_id, def.loop_id, def.back_id)))
- ("opaque_defs." ^ name) ctx
- else
- ctx
+ let ctx =
+ if def.body = None && !Config.backend = Lean then
+ ctx_add
+ (DeclaredId (FromLlbc (A.Regular def_id, def.loop_id, def.back_id)))
+ ("opaque_defs." ^ name) ctx
+ else ctx
in
ctx_add
(FunId (FromLlbc (A.Regular def_id, def.loop_id, def.back_id)))
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index df7a750d..1c0bcf73 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -466,10 +466,9 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
let is_opaque = Option.is_none body.Pure.body in
if
- config.extract_globals && (
- ((not is_opaque) && config.extract_transparent)
- || (is_opaque && config.extract_opaque)
- )
+ config.extract_globals
+ && (((not is_opaque) && config.extract_transparent)
+ || (is_opaque && config.extract_opaque))
then
Extract.extract_global_decl ctx.extract_ctx fmt global body config.interface
@@ -564,7 +563,8 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
let has_decr_clause = has_decreases_clause decl in
if has_decr_clause then
if !Config.backend = Lean then
- Extract.extract_termination_and_decreasing ctx.extract_ctx fmt decl
+ Extract.extract_termination_and_decreasing ctx.extract_ctx fmt
+ decl
else
Extract.extract_template_decreases_clause ctx.extract_ctx fmt decl
in
@@ -661,24 +661,22 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
*)
if config.extract_state_type && config.extract_fun_decls then
export_state_type ();
- if config.extract_opaque && config.extract_fun_decls && !Config.backend = Lean then begin
+ if config.extract_opaque && config.extract_fun_decls && !Config.backend = Lean
+ then (
Format.pp_print_break fmt 0 0;
Format.pp_open_vbox fmt ctx.extract_ctx.indent_incr;
Format.pp_print_string fmt "structure OpaqueDefs where";
- Format.pp_print_break fmt 0 0
- end;
+ Format.pp_print_break fmt 0 0);
List.iter export_decl_group ctx.crate.declarations;
- if config.extract_opaque && !Config.backend = Lean then begin
- Format.pp_close_box fmt ()
- end;
+ if config.extract_opaque && !Config.backend = Lean then
+ Format.pp_close_box fmt ();
if config.extract_state_type && not config.extract_fun_decls then
export_state_type ()
let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
(rust_module_name : string) (module_name : string) (custom_msg : string)
- ?(custom_variables: string list = [])
- (custom_imports : string list) (custom_includes : string list)
- : unit =
+ ?(custom_variables : string list = []) (custom_imports : string list)
+ (custom_includes : string list) : unit =
(* Open the file and create the formatter *)
let out = open_out filename in
let fmt = Format.formatter_of_out_channel out in
@@ -691,14 +689,14 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
* internal count is consistent with the state of the file.
*)
(* Create the header *)
- begin match !Config.backend with
+ (match !Config.backend with
| Lean ->
Printf.fprintf out "-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS\n";
- Printf.fprintf out "-- [%s]%s\n" rust_module_name custom_msg;
+ Printf.fprintf out "-- [%s]%s\n" rust_module_name custom_msg
| Coq | FStar ->
- Printf.fprintf out "(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)\n";
- Printf.fprintf out "(** [%s]%s *)\n" rust_module_name custom_msg
- end;
+ Printf.fprintf out
+ "(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)\n";
+ Printf.fprintf out "(** [%s]%s *)\n" rust_module_name custom_msg);
(match !Config.backend with
| FStar ->
Printf.fprintf out "module %s\n" module_name;
@@ -732,11 +730,9 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
List.iter (fun m -> Printf.fprintf out "import %s\n" m) custom_imports;
(* Add the custom includes *)
List.iter (fun m -> Printf.fprintf out "import %s\n" m) custom_includes;
- if custom_variables <> [] then begin
+ if custom_variables <> [] then (
Printf.fprintf out "\n";
- List.iter (fun m -> Printf.fprintf out "%s\n" m) custom_variables
- end
- );
+ List.iter (fun m -> Printf.fprintf out "%s\n" m) custom_variables));
(* From now onwards, we use the formatter *)
(* Set the margin *)
Format.pp_set_margin fmt 80;
@@ -885,13 +881,11 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
(* Lean reflects the module hierarchy within the filesystem, so we need to
create more directories *)
- if !Config.backend = Lean then begin
- let (^^) = Filename.concat in
+ if !Config.backend = Lean then (
+ let ( ^^ ) = Filename.concat in
mkdir_if (dest_dir ^^ "Base");
mkdir_if (dest_dir ^^ module_name);
- if needs_clauses_module then
- mkdir_if (dest_dir ^^ module_name ^^ "Clauses");
- end;
+ if needs_clauses_module then mkdir_if (dest_dir ^^ module_name ^^ "Clauses"));
(* Copy the "Primitives" file *)
let _ =
@@ -936,7 +930,17 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
let file_delimiter =
if !Config.backend = Lean then "/" else module_delimiter
in
- let ext = match !Config.backend with FStar -> ".fst" | Coq -> ".v" | Lean -> ".lean" in
+ (* File extension for the "regular" modules *)
+ let ext =
+ match !Config.backend with FStar -> ".fst" | Coq -> ".v" | Lean -> ".lean"
+ in
+ (* File extension for the opaque module *)
+ let opaque_ext =
+ match !Config.backend with
+ | FStar -> ".fsti"
+ | Coq -> ".v"
+ | Lean -> ".lean"
+ in
(* Extract one or several files, depending on the configuration *)
if !Config.split_files then (
@@ -985,20 +989,28 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
": type definitions" [] [];
(* Extract the template clauses *)
- if needs_clauses_module && !Config.extract_template_decreases_clauses then (
- let clauses_filename = extract_filebasename ^ file_delimiter ^ "Clauses" ^ file_delimiter ^ "Template" ^ ext in
- let clauses_module = module_name ^ module_delimiter ^ "Clauses" ^ module_delimiter ^ "Template" in
- let clauses_config =
- { base_gen_config with extract_template_decreases_clauses = true }
- in
- extract_file clauses_config gen_ctx clauses_filename crate.A.name
- clauses_module ": templates for the decreases clauses" [ types_module ]
- []);
+ (if needs_clauses_module && !Config.extract_template_decreases_clauses then
+ let template_clauses_filename =
+ extract_filebasename ^ file_delimiter ^ "Clauses" ^ file_delimiter
+ ^ "Template" ^ ext
+ in
+ let template_clauses_module =
+ module_name ^ module_delimiter ^ "Clauses" ^ module_delimiter
+ ^ "Template"
+ in
+ let template_clauses_config =
+ { base_gen_config with extract_template_decreases_clauses = true }
+ in
+ extract_file template_clauses_config gen_ctx template_clauses_filename
+ crate.A.name template_clauses_module
+ ": templates for the decreases clauses" [ types_module ] []);
(* Extract the opaque functions, if needed *)
let opaque_funs_module =
if has_opaque_funs then (
- let opaque_filename = extract_filebasename ^ file_delimiter ^ "Opaque" ^ ext in
+ let opaque_filename =
+ extract_filebasename ^ file_delimiter ^ "Opaque" ^ opaque_ext
+ in
let opaque_module = module_name ^ module_delimiter ^ "Opaque" in
let opaque_config =
{
@@ -1028,13 +1040,18 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
in
let clauses_module =
if needs_clauses_module then
- [ module_name ^ module_delimiter ^ "Clauses" ^ module_delimiter ^ "Template"]
+ let clauses_submodule =
+ if !Config.backend = Lean then module_delimiter ^ "Clauses" else ""
+ in
+ [ module_name ^ clauses_submodule ^ module_delimiter ^ "Clauses" ]
+ else []
+ in
+ let custom_variables =
+ if has_opaque_funs then [ "section variable (opaque_defs: OpaqueDefs)" ]
else []
in
- let custom_variables = if has_opaque_funs then [ "section variable (opaque_defs: OpaqueDefs)" ] else [] in
extract_file fun_config gen_ctx fun_filename crate.A.name fun_module
- ": function definitions" []
- ~custom_variables
+ ": function definitions" [] ~custom_variables
([ types_module ] @ opaque_funs_module @ clauses_module))
else
let gen_config =
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 02:15:17 +0000