summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to 'compiler')
-rw-r--r--compiler/Config.ml67
-rw-r--r--compiler/Driver.ml36
-rw-r--r--compiler/Extract.ml (renamed from compiler/ExtractToBackend.ml)996
-rw-r--r--compiler/ExtractBase.ml (renamed from compiler/PureToExtract.ml)87
-rw-r--r--compiler/ExtractToCoq.ml8
-rw-r--r--compiler/ExtractToFStar.ml8
-rw-r--r--compiler/Logging.ml4
-rw-r--r--compiler/PureMicroPasses.ml1
-rw-r--r--compiler/PureUtils.ml4
-rw-r--r--compiler/SymbolicAst.ml4
-rw-r--r--compiler/SymbolicToPure.ml28
-rw-r--r--compiler/Translate.ml224
-rw-r--r--compiler/Values.ml1
-rw-r--r--compiler/dune6
14 files changed, 1058 insertions, 416 deletions
diff --git a/compiler/Config.ml b/compiler/Config.ml
index c9723bd4..95442761 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -1,5 +1,33 @@
(** Define the global configuration options *)
+(** {1 Backend choice} *)
+
+(** The choice of backend *)
+type backend = FStar | Coq
+
+let backend_names = [ "fstar"; "coq" ]
+
+(** Utility to compute the backend from an input parameter *)
+let backend_of_string (b : string) : backend option =
+ match b with "fstar" -> Some FStar | "coq" -> Some Coq | _ -> None
+
+let opt_backend : backend option ref = ref None
+
+let set_backend (b : string) : unit =
+ match backend_of_string b with
+ | Some b -> opt_backend := Some b
+ | None ->
+ (* We shouldn't get there: the string should have been checked as
+ belonging to the proper set *)
+ raise (Failure "Unexpected")
+
+(** The backend to which to extract.
+
+ We initialize it with a default value, but it always gets overwritten:
+ we check that the user provides a backend argument.
+ *)
+let backend = ref FStar
+
(** {1 Interpreter} *)
(** Check that invariants are maintained whenever we execute a statement *)
@@ -44,6 +72,39 @@ let allow_bottom_below_borrow = true
*)
let return_unit_end_abs_with_no_loans = true
+(** Forbids using field projectors for structures.
+
+ If we don't use field projectors, whenever we symbolically expand a structure
+ value (note that accessing a structure field in the symbolic execution triggers
+ its expansion), then instead of generating code like this:
+ {[
+ let x1 = s.f1 in
+ let x2 = s.f2 in
+ ...
+ ]}
+
+ we generate code like this:
+ {[
+ let Mkstruct x1 x2 ... = s in
+ ...
+ ]}
+
+ We use this for instance for Coq, because in Coq we can't define groups
+ of mutually recursive records and inductives. In such cases, we extract
+ the structures as inductives, which means that field projectors are not
+ always available.
+
+ TODO: we could define a notation to take care of this.
+ TODO: today dont_use_field_projectors is not useful actually.
+ *)
+let dont_use_field_projectors = ref false
+
+(** Deconstructing ADTs which have only one variant with let-bindings is not always
+ supported: this parameter controls whether we use let-bindings in such situations or not.
+ *)
+
+let always_deconstruct_adts_with_matches = ref false
+
(** {1 Translation} *)
(** Controls whether we need to use a state to model the external world
@@ -103,7 +164,7 @@ let test_trans_unit_functions = ref false
The body of such clauses must be defined by the user.
*)
-let extract_decreases_clauses = ref true
+let extract_decreases_clauses = ref false
(** In order to help the user, we can generate "template" decrease clauses
(i.e., definitions with proper signatures but dummy bodies) in a
@@ -113,10 +174,10 @@ let extract_template_decreases_clauses = ref false
(** {1 Micro passes} *)
-(** Some provers like F* don't support the decomposition of return values
+(** Some provers like F* and Coq don't support the decomposition of return values
in monadic let-bindings:
{[
- // NOT supported in F*
+ (* NOT supported in F*/Coq *)
let (x, y) <-- f ();
...
]}
diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index 3059ec2f..5089cb8e 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -33,6 +33,9 @@ let () =
let spec =
[
+ ( "-backend",
+ Arg.Symbol (backend_names, set_backend),
+ " Specify the backend to which to extract" );
("-dest", Arg.Set_string dest_dir, " Specify the output directory");
( "-decompose-monads",
Arg.Set decompose_monadic_let_bindings,
@@ -61,9 +64,9 @@ let () =
Arg.Set test_trans_unit_functions,
" Test the translated unit functions with the target theorem\n\
\ prover's normalizer" );
- ( "-no-decreases-clauses",
- Arg.Clear extract_decreases_clauses,
- " Do not add decrease clauses to the recursive definitions" );
+ ( "-decreases-clauses",
+ Arg.Set extract_decreases_clauses,
+ " Use decreases clauses for the recursive definitions" );
( "-no-state",
Arg.Clear use_state,
" Do not use state-error monads, simply use error monads" );
@@ -73,8 +76,8 @@ let () =
( "-template-clauses",
Arg.Set extract_template_decreases_clauses,
" Generate templates for the required decreases clauses, in a\n\
- \ dedicated file. Incompatible with \
- -no-decreases-clauses" );
+ \ dedicated file. Reauires -decreases-clauses"
+ );
( "-no-split-files",
Arg.Clear split_files,
" Don't split the definitions between different files for types,\n\
@@ -98,6 +101,29 @@ let () =
print_string usage;
exit 1
in
+
+ (* Check that the user specified a backend *)
+ let _ =
+ match !opt_backend with
+ | Some b -> backend := b
+ | None ->
+ print_string "Backend not specified (use the `-backend` argument)\n";
+ fail ()
+ in
+
+ (* In the case of Coq, we forbid using field projectors (see the comments for
+ [dont_use_field_projectors]).
+ Also, we always decompose ADT values with matches (decomposing with
+ let-bindings is not supported).
+ *)
+ let _ =
+ match !backend with
+ | FStar -> ()
+ | Coq ->
+ dont_use_field_projectors := true;
+ always_deconstruct_adts_with_matches := true
+ in
+
(* Retrieve and check the filename *)
let filename =
match !filenames with
diff --git a/compiler/ExtractToBackend.ml b/compiler/Extract.ml
index fc04ce90..f9c4d10a 100644
--- a/compiler/ExtractToBackend.ml
+++ b/compiler/Extract.ml
@@ -1,41 +1,19 @@
-(** Extract to F* *)
+(** The generic extraction *)
+(* Turn the whole module into a functor: it is very annoying to carry the
+ the formatter everywhere...
+*)
open Utils
open Pure
open PureUtils
open TranslateCore
-open PureToExtract
+open ExtractBase
open StringUtils
+open Config
module F = Format
-(** A qualifier for a type definition.
-
- Controls whether we should use [type ...] or [and ...] (for mutually
- recursive datatypes).
- *)
-type type_decl_qualif =
- | Type (** [type t = ...] *)
- | And (** [type t0 = ... and t1 = ...] *)
- | AssumeType (** [assume type t] *)
- | TypeVal (** In an fsti: [val t : Type0] *)
-
-(** A qualifier for function definitions.
-
- Controls whether we should use [let ...], [let rec ...] or [and ...],
- or only generate a declaration with [val] or [assume val]
- *)
-type fun_decl_qualif = Let | LetRec | And | Val | AssumeVal
-
-let fun_decl_qualif_keyword (qualif : fun_decl_qualif) : string =
- match qualif with
- | Let -> "let"
- | LetRec -> "let rec"
- | And -> "and"
- | Val -> "val"
- | AssumeVal -> "assume val"
-
(** Small helper to compute the name of an int type *)
-let fstar_int_name (int_ty : integer_type) =
+let int_name (int_ty : integer_type) =
match int_ty with
| Isize -> "isize"
| I8 -> "i8"
@@ -51,17 +29,17 @@ let fstar_int_name (int_ty : integer_type) =
| U128 -> "u128"
(** Small helper to compute the name of a unary operation *)
-let fstar_unop_name (unop : unop) : string =
+let unop_name (unop : unop) : string =
match unop with
- | Not -> "not"
- | Neg int_ty -> fstar_int_name int_ty ^ "_neg"
+ | Not -> ( match !backend with FStar -> "not" | Coq -> "negb")
+ | Neg int_ty -> int_name int_ty ^ "_neg"
| Cast _ -> raise (Failure "Unsupported")
(** Small helper to compute the name of a binary operation (note that many
binary operations like "less than" are extracted to primitive operations,
like [<].
*)
-let fstar_named_binop_name (binop : E.binop) (int_ty : integer_type) : string =
+let named_binop_name (binop : E.binop) (int_ty : integer_type) : string =
let binop =
match binop with
| Div -> "div"
@@ -71,64 +49,105 @@ let fstar_named_binop_name (binop : E.binop) (int_ty : integer_type) : string =
| Mul -> "mul"
| _ -> raise (Failure "Unreachable")
in
- fstar_int_name int_ty ^ "_" ^ binop
+ int_name int_ty ^ "_" ^ binop
-(** A list of keywords/identifiers used in F* and with which we want to check
- collision. *)
-let fstar_keywords =
+(** A list of keywords/identifiers used by the backend and with which we
+ want to check collision. *)
+let keywords () =
let named_unops =
- fstar_unop_name Not
- :: List.map (fun it -> fstar_unop_name (Neg it)) T.all_signed_int_types
+ unop_name Not
+ :: List.map (fun it -> unop_name (Neg it)) T.all_signed_int_types
in
let named_binops = [ E.Div; Rem; Add; Sub; Mul ] in
let named_binops =
List.concat
(List.map
- (fun bn ->
- List.map (fun it -> fstar_named_binop_name bn it) T.all_int_types)
+ (fun bn -> List.map (fun it -> named_binop_name bn it) T.all_int_types)
named_binops)
in
let misc =
- [
- "let";
- "rec";
- "in";
- "fn";
- "val";
- "int";
- "nat";
- "list";
- "FStar";
- "FStar.Mul";
- "type";
- "match";
- "with";
- "assert";
- "assert_norm";
- "assume";
- "Type0";
- "Type";
- "unit";
- "not";
- "scalar_cast";
- ]
+ match !backend with
+ | FStar ->
+ [
+ "let";
+ "rec";
+ "in";
+ "fun";
+ "fn";
+ "val";
+ "int";
+ "nat";
+ "list";
+ "FStar";
+ "FStar.Mul";
+ "type";
+ "match";
+ "with";
+ "assert";
+ "assert_norm";
+ "assume";
+ "Type0";
+ "Type";
+ "unit";
+ "not";
+ "scalar_cast";
+ ]
+ | Coq ->
+ [
+ "Record";
+ "Inductive";
+ "Fixpoint";
+ "Definition";
+ "Arguments";
+ "Notation";
+ "Check";
+ "Search";
+ "SearchPattern";
+ "Axiom";
+ "Type";
+ "Set";
+ "let";
+ "rec";
+ "in";
+ "unit";
+ "fun";
+ "type";
+ "int";
+ "nat";
+ "match";
+ "with";
+ "assert";
+ "not";
+ (* [tt] is unit *)
+ "tt";
+ "char_of_byte";
+ ]
in
List.concat [ named_unops; named_binops; misc ]
-let fstar_assumed_adts : (assumed_ty * string) list =
+let assumed_adts : (assumed_ty * string) list =
[ (State, "state"); (Result, "result"); (Option, "option"); (Vec, "vec") ]
-let fstar_assumed_structs : (assumed_ty * string) list = []
-
-let fstar_assumed_variants : (assumed_ty * VariantId.id * string) list =
- [
- (Result, result_return_id, "Return");
- (Result, result_fail_id, "Fail");
- (Option, option_some_id, "Some");
- (Option, option_none_id, "None");
- ]
-
-let fstar_assumed_llbc_functions :
+let assumed_structs : (assumed_ty * string) list = []
+
+let assumed_variants () : (assumed_ty * VariantId.id * string) list =
+ match !backend with
+ | FStar ->
+ [
+ (Result, result_return_id, "Return");
+ (Result, result_fail_id, "Fail");
+ (Option, option_some_id, "Some");
+ (Option, option_none_id, "None");
+ ]
+ | Coq ->
+ [
+ (Result, result_return_id, "Return");
+ (Result, result_fail_id, "Fail_");
+ (Option, option_some_id, "Some");
+ (Option, option_none_id, "None");
+ ]
+
+let assumed_llbc_functions :
(A.assumed_fun_id * T.RegionGroupId.id option * string) list =
let rg0 = Some T.RegionGroupId.zero in
[
@@ -146,25 +165,27 @@ let fstar_assumed_llbc_functions :
(VecIndexMut, rg0, "vec_index_mut_back");
]
-let fstar_assumed_pure_functions : (pure_assumed_fun_id * string) list =
- [ (Return, "return"); (Fail, "fail"); (Assert, "massert") ]
+let assumed_pure_functions : (pure_assumed_fun_id * string) list =
+ match !backend with
+ | FStar -> [ (Return, "return"); (Fail, "fail"); (Assert, "massert") ]
+ | Coq -> [ (Return, "return_"); (Fail, "fail_"); (Assert, "massert") ]
-let fstar_names_map_init : names_map_init =
+let names_map_init () : names_map_init =
{
- keywords = fstar_keywords;
- assumed_adts = fstar_assumed_adts;
- assumed_structs = fstar_assumed_structs;
- assumed_variants = fstar_assumed_variants;
- assumed_llbc_functions = fstar_assumed_llbc_functions;
- assumed_pure_functions = fstar_assumed_pure_functions;
+ keywords = keywords ();
+ assumed_adts;
+ assumed_structs;
+ assumed_variants = assumed_variants ();
+ assumed_llbc_functions;
+ assumed_pure_functions;
}
-let fstar_extract_unop (extract_expr : bool -> texpression -> unit)
+let extract_unop (extract_expr : bool -> texpression -> unit)
(fmt : F.formatter) (inside : bool) (unop : unop) (arg : texpression) : unit
=
match unop with
| Not | Neg _ ->
- let unop = fstar_unop_name unop in
+ let unop = unop_name unop in
if inside then F.pp_print_string fmt "(";
F.pp_print_string fmt unop;
F.pp_print_space fmt ();
@@ -186,7 +207,7 @@ let fstar_extract_unop (extract_expr : bool -> texpression -> unit)
extract_expr true arg;
if inside then F.pp_print_string fmt ")"
-let fstar_extract_binop (extract_expr : bool -> texpression -> unit)
+let extract_binop (extract_expr : bool -> texpression -> unit)
(fmt : F.formatter) (inside : bool) (binop : E.binop)
(int_ty : integer_type) (arg0 : texpression) (arg1 : texpression) : unit =
if inside then F.pp_print_string fmt "(";
@@ -203,13 +224,14 @@ let fstar_extract_binop (extract_expr : bool -> texpression -> unit)
| Gt -> ">"
| _ -> raise (Failure "Unreachable")
in
+ let binop = match !backend with FStar -> binop | Coq -> "s" ^ binop in
extract_expr false arg0;
F.pp_print_space fmt ();
F.pp_print_string fmt binop;
F.pp_print_space fmt ();
extract_expr false arg1
| Div | Rem | Add | Sub | Mul ->
- let binop = fstar_named_binop_name binop int_ty in
+ let binop = named_binop_name binop int_ty in
F.pp_print_string fmt binop;
F.pp_print_space fmt ();
extract_expr false arg0;
@@ -218,6 +240,52 @@ let fstar_extract_binop (extract_expr : bool -> texpression -> unit)
| BitXor | BitAnd | BitOr | Shl | Shr -> raise Unimplemented);
if inside then F.pp_print_string fmt ")"
+let type_decl_kind_to_qualif (kind : decl_kind)
+ (type_kind : type_decl_kind option) : string =
+ match !backend with
+ | FStar -> (
+ match kind with
+ | SingleNonRec -> "type"
+ | SingleRec -> "type"
+ | MutRecFirst -> "type"
+ | MutRecInner -> "and"
+ | MutRecLast -> "and"
+ | Assumed -> "assume type"
+ | Declared -> "val")
+ | Coq -> (
+ match (kind, type_kind) with
+ | SingleNonRec, Some Enum -> "Inductive"
+ | SingleNonRec, Some Struct -> "Record"
+ | (SingleRec | MutRecFirst), Some _ -> "Inductive"
+ | (MutRecInner | MutRecLast), Some _ ->
+ (* Coq doesn't support groups of mutually recursive definitions which mix
+ * records and inducties: we convert everything to records if this happens
+ *)
+ "with"
+ | (Assumed | Declared), None -> "Axiom"
+ | _ -> raise (Failure "Unexpected"))
+
+let fun_decl_kind_to_qualif (kind : decl_kind) =
+ match !backend with
+ | FStar -> (
+ match kind with
+ | SingleNonRec -> "let"
+ | SingleRec -> "let rec"
+ | MutRecFirst -> "let rec"
+ | MutRecInner -> "and"
+ | MutRecLast -> "and"
+ | Assumed -> "assume val"
+ | Declared -> "val")
+ | Coq -> (
+ match kind with
+ | SingleNonRec -> "Definition"
+ | SingleRec -> "Fixpoint"
+ | MutRecFirst -> "Fixpoint"
+ | MutRecInner -> "with"
+ | MutRecLast -> "with"
+ | 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
@@ -256,7 +324,7 @@ let fstar_extract_binop (extract_expr : bool -> texpression -> unit)
*)
let mk_formatter (ctx : trans_ctx) (crate_name : string)
(variant_concatenate_type_name : bool) : formatter =
- let int_name = fstar_int_name in
+ let int_name = int_name in
(* Prepare a name.
* The first id elem is always the crate: if it is the local crate,
@@ -291,7 +359,8 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
let type_name_to_snake_case name =
let name = get_type_name name in
let name = List.map to_snake_case name in
- String.concat "_" name
+ let name = String.concat "_" name in
+ match !backend with FStar -> 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)
@@ -309,7 +378,8 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
in
let struct_constructor (basename : name) : string =
let tname = type_name basename in
- "Mk" ^ tname
+ let prefix = match !backend with FStar -> "Mk" | Coq -> "mk" in
+ prefix ^ tname
in
let get_fun_name = get_name in
let fun_name_to_snake_case (fname : fun_name) : string =
@@ -381,7 +451,11 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
assert (List.length cl > 0);
let cl = List.map (fun s -> s.[0]) cl in
StringUtils.string_of_chars cl)
- | TypeVar _ -> "x" (* lacking imagination here... *)
+ | TypeVar _ -> (
+ (* TODO: use "t" also for F* *)
+ match !backend with
+ | FStar -> "x" (* lacking inspiration here... *)
+ | Coq -> "t" (* lacking inspiration here... *))
| Bool -> "b"
| Char -> "c"
| Integer _ -> "i"
@@ -390,22 +464,51 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
| Array _ | Slice _ -> raise Unimplemented)
in
let type_var_basename (_varset : StringSet.t) (basename : string) : string =
- (* This is *not* a no-op: type variables in Rust often start with
- * a capital letter *)
- to_snake_case basename
+ (* Rust type variables are snake-case and start with a capital letter *)
+ match !backend with
+ | FStar ->
+ (* This is *not* a no-op: this removes the capital letter *)
+ to_snake_case basename
+ | Coq -> basename
in
let append_index (basename : string) (i : int) : string =
basename ^ string_of_int i
in
- let extract_primitive_value (fmt : F.formatter) (_inside : bool)
+ let extract_primitive_value (fmt : F.formatter) (inside : bool)
(cv : primitive_value) : unit =
match cv with
- | Scalar sv -> F.pp_print_string fmt (Z.to_string sv.PV.value)
+ | Scalar sv -> (
+ match !backend with
+ | FStar -> F.pp_print_string fmt (Z.to_string sv.PV.value)
+ | Coq ->
+ if inside then F.pp_print_string fmt "(";
+ (* We need to add parentheses if the value is negative *)
+ if sv.PV.value >= Z.of_int 0 then
+ F.pp_print_string fmt (Z.to_string sv.PV.value)
+ else F.pp_print_string fmt ("(" ^ Z.to_string sv.PV.value ^ ")");
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt ("%" ^ int_name sv.PV.int_ty);
+ if inside then F.pp_print_string fmt ")")
| Bool b ->
let b = if b then "true" else "false" in
F.pp_print_string fmt b
- | Char c -> F.pp_print_string fmt ("'" ^ String.make 1 c ^ "'")
+ | Char c -> (
+ match !backend with
+ | FStar -> F.pp_print_string fmt ("'" ^ String.make 1 c ^ "'")
+ | Coq ->
+ if inside then F.pp_print_string fmt "(";
+ F.pp_print_string fmt "char_of_byte";
+ F.pp_print_space fmt ();
+ (* Convert the the char to ascii *)
+ let c =
+ let i = Char.code c in
+ let x0 = i / 16 in
+ let x1 = i mod 16 in
+ "Coq.Init.Byte.x" ^ string_of_int x0 ^ string_of_int x1
+ 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 =
@@ -420,6 +523,8 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
char_name = "char";
int_name;
str_name = "string";
+ type_decl_kind_to_qualif;
+ fun_decl_kind_to_qualif;
field_name;
variant_name;
struct_constructor;
@@ -431,10 +536,22 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
type_var_basename;
append_index;
extract_primitive_value;
- extract_unop = fstar_extract_unop;
- extract_binop = fstar_extract_binop;
+ extract_unop;
+ extract_binop;
}
+let mk_formatter_and_names_map (ctx : trans_ctx) (crate_name : string)
+ (variant_concatenate_type_name : bool) : formatter * names_map =
+ let fmt = mk_formatter ctx crate_name variant_concatenate_type_name in
+ let names_map = initialize_names_map fmt (names_map_init ()) in
+ (fmt, names_map)
+
+(** In Coq, a group of definitions must be ended with a "." *)
+let print_decl_end_delimiter (fmt : F.formatter) (kind : decl_kind) =
+ if !backend = Coq && decl_is_last_from_group kind then (
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt ".")
+
(** [inside] constrols whether we should add parentheses or not around type
applications (if [true] we add parentheses).
*)
@@ -444,7 +561,7 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
| Adt (type_id, tys) -> (
match type_id with
| Tuple ->
- (* This is a bit annoying, but in F* [()] is not the unit type:
+ (* This is a bit annoying, but in F*/Coq [()] is not the unit type:
* we have to write [unit]... *)
if tys = [] then F.pp_print_string fmt "unit"
else (
@@ -452,7 +569,8 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
Collections.List.iter_link
(fun () ->
F.pp_print_space fmt ();
- F.pp_print_string fmt "&";
+ let product = match !backend with FStar -> "&" | Coq -> "*" in
+ F.pp_print_string fmt product;
F.pp_print_space fmt ())
(extract_ty ctx fmt true) tys;
F.pp_print_string fmt ")")
@@ -516,68 +634,73 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
(* Return *)
ctx
-let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
- (def : type_decl) (fields : field list) : unit =
- (* We want to generate a definition which looks like this:
- {[
- type t = { x : int; y : bool; }
- ]}
-
- If there isn't enough space on one line:
- {[
- type t =
- {
- x : int; y : bool;
- }
- ]}
-
- And if there is even less space:
- {[
- type t =
- {
- x : int;
- y : bool;
- }
- ]}
-
- Also, in case there are no fields, we need to define the type as [unit]
- ([type t = {}] doesn't work in F* ).
- *)
- (* Note that we already printed: [type t =] *)
- if fields = [] then (
- F.pp_print_space fmt ();
- F.pp_print_string fmt "unit")
- else (
- F.pp_print_space fmt ();
- F.pp_print_string fmt "{";
- F.pp_print_break fmt 1 ctx.indent_incr;
- (* The body itself *)
- F.pp_open_hvbox fmt 0;
- (* Print the fields *)
- let print_field (field_id : FieldId.id) (f : field) : unit =
- let field_name = ctx_get_field (AdtId def.def_id) field_id ctx in
- F.pp_open_box fmt ctx.indent_incr;
- F.pp_print_string fmt field_name;
- F.pp_print_space fmt ();
- F.pp_print_string fmt ":";
- F.pp_print_space fmt ();
- extract_ty ctx fmt false f.field_ty;
- F.pp_print_string fmt ";";
- F.pp_close_box fmt ()
+(** Print the variants *)
+let extract_type_decl_variant (ctx : extraction_ctx) (fmt : F.formatter)
+ (type_name : string) (type_params : string list) (cons_name : string)
+ (fields : field list) : unit =
+ F.pp_print_space fmt ();
+ F.pp_open_hvbox fmt ctx.indent_incr;
+ (* variant box *)
+ (* [| Cons :]
+ * Note that we really don't want any break above so we print everything
+ * at once. *)
+ F.pp_print_string fmt ("| " ^ cons_name ^ " :");
+ F.pp_print_space fmt ();
+ let print_field (fid : FieldId.id) (f : field) (ctx : extraction_ctx) :
+ extraction_ctx =
+ (* Open the field box *)
+ F.pp_open_box fmt ctx.indent_incr;
+ (* Print the field names
+ * [ x :]
+ * Note that when printing fields, we register the field names as
+ * *variables*: they don't need to be unique at the top level. *)
+ let ctx =
+ match f.field_name with
+ | None -> ctx
+ | Some field_name ->
+ let var_id = VarId.of_int (FieldId.to_int fid) in
+ let field_name =
+ ctx.fmt.var_basename ctx.names_map.names_set (Some field_name)
+ f.field_ty
+ in
+ let ctx, field_name = ctx_add_var field_name var_id ctx in
+ F.pp_print_string fmt (field_name ^ " :");
+ F.pp_print_space fmt ();
+ ctx
in
- let fields = FieldId.mapi (fun fid f -> (fid, f)) fields in
- Collections.List.iter_link (F.pp_print_space fmt)
- (fun (fid, f) -> print_field fid f)
- fields;
- (* Close *)
+ (* Print the field type *)
+ extract_ty ctx fmt false f.field_ty;
+ (* Print the arrow [->]*)
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt "->";
+ (* Close the field box *)
F.pp_close_box fmt ();
F.pp_print_space fmt ();
- F.pp_print_string fmt "}")
+ (* Return *)
+ ctx
+ in
+ (* Print the fields *)
+ let fields = FieldId.mapi (fun fid f -> (fid, f)) fields in
+ let _ =
+ List.fold_left (fun ctx (fid, f) -> print_field fid f ctx) ctx fields
+ in
+ (* Print the final type *)
+ F.pp_open_hovbox fmt 0;
+ F.pp_print_string fmt type_name;
+ List.iter
+ (fun type_param ->
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt type_param)
+ type_params;
+ F.pp_close_box fmt ();
+ (* Close the variant box *)
+ F.pp_close_box fmt ()
+(* TODO: we don' need the [def_name] paramter: it can be retrieved from the context *)
let extract_type_decl_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
(def : type_decl) (def_name : string) (type_params : string list)
(variants : variant list) : unit =
- (* We want to generate a definition which looks like this:
+ (* We want to generate a definition which looks like this (taking F* as example):
{[
type list a = | Cons : a -> list a -> list a | Nil : list a
]}
@@ -609,70 +732,104 @@ let extract_type_decl_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
Note that we already printed: [type s =]
*)
+ let print_variant variant_id v =
+ let cons_name = ctx_get_variant (AdtId def.def_id) variant_id ctx in
+ let fields = v.fields in
+ extract_type_decl_variant ctx fmt def_name type_params cons_name fields
+ in
(* Print the variants *)
- let print_variant (variant_id : VariantId.id) (variant : variant) : unit =
- let variant_name = ctx_get_variant (AdtId def.def_id) variant_id ctx in
- F.pp_print_space fmt ();
- F.pp_open_hvbox fmt ctx.indent_incr;
- (* variant box *)
- (* [| Cons :]
- * Note that we really don't want any break above so we print everything
- * at once. *)
- F.pp_print_string fmt ("| " ^ variant_name ^ " :");
+ let variants = VariantId.mapi (fun vid v -> (vid, v)) variants in
+ List.iter (fun (vid, v) -> print_variant vid v) variants
+
+let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
+ (kind : decl_kind) (def : type_decl) (type_params : string list)
+ (fields : field list) : unit =
+ (* We want to generate a definition which looks like this (taking F* as example):
+ {[
+ type t = { x : int; y : bool; }
+ ]}
+
+ If there isn't enough space on one line:
+ {[
+ type t =
+ {
+ x : int; y : bool;
+ }
+ ]}
+
+ And if there is even less space:
+ {[
+ type t =
+ {
+ x : int;
+ y : bool;
+ }
+ ]}
+
+ Also, in case there are no fields, we need to define the type as [unit]
+ ([type t = {}] doesn't work in F* ).
+
+ Coq:
+ ====
+ We need to define the constructor name upon defining the struct (record, in Coq).
+ The syntex is:
+ {[
+ Record Foo = mkFoo { x : int; y : bool; }.
+ }]
+
+ Also, Coq doesn't support groups of mutually recursive inductives and records.
+ This is fine, because we can then define records as inductives, and leverage
+ the fact that when record fields are accessed, the records are symbolically
+ expanded which introduces let bindings of the form: [let RecordCons ... = x in ...].
+ As a consequence, we never use the record projectors (unless we reconstruct
+ them in the micro passes of course).
+ *)
+ (* Note that we already printed: [type t =] *)
+ let is_rec = decl_is_from_rec_group kind in
+ (* If Coq: print the constructor name *)
+ if !backend = Coq && not is_rec then (
F.pp_print_space fmt ();
- let print_field (fid : FieldId.id) (f : field) (ctx : extraction_ctx) :
- extraction_ctx =
- (* Open the field box *)
- F.pp_open_box fmt ctx.indent_incr;
- (* Print the field names
- * [ x :]
- * Note that when printing fields, we register the field names as
- * *variables*: they don't need to be unique at the top level. *)
- let ctx =
- match f.field_name with
- | None -> ctx
- | Some field_name ->
- let var_id = VarId.of_int (FieldId.to_int fid) in
- let field_name =
- ctx.fmt.var_basename ctx.names_map.names_set (Some field_name)
- f.field_ty
- in
- let ctx, field_name = ctx_add_var field_name var_id ctx in
- F.pp_print_string fmt (field_name ^ " :");
- F.pp_print_space fmt ();
- ctx
- in
- (* Print the field type *)
- extract_ty ctx fmt false f.field_ty;
- (* Print the arrow [->]*)
+ F.pp_print_string fmt (ctx_get_struct (AdtId def.def_id) ctx));
+ let _ =
+ if !backend = FStar && fields = [] then (
F.pp_print_space fmt ();
- F.pp_print_string fmt "->";
- (* Close the field box *)
- F.pp_close_box fmt ();
+ F.pp_print_string fmt "unit")
+ else if (not is_rec) || !backend = FStar then (
F.pp_print_space fmt ();
- (* Return *)
- ctx
- in
- (* Print the fields *)
- let fields = FieldId.mapi (fun fid f -> (fid, f)) variant.fields in
- let _ =
- List.fold_left (fun ctx (fid, f) -> print_field fid f ctx) ctx fields
- in
- (* Print the final type *)
- F.pp_open_hovbox fmt 0;
- F.pp_print_string fmt def_name;
- List.iter
- (fun type_param ->
+ F.pp_print_string fmt "{";
+ F.pp_print_break fmt 1 ctx.indent_incr;
+ (* The body itself *)
+ F.pp_open_hvbox fmt 0;
+ (* Print the fields *)
+ let print_field (field_id : FieldId.id) (f : field) : unit =
+ let field_name = ctx_get_field (AdtId def.def_id) field_id ctx in
+ F.pp_open_box fmt ctx.indent_incr;
+ F.pp_print_string fmt field_name;
F.pp_print_space fmt ();
- F.pp_print_string fmt type_param)
- type_params;
- F.pp_close_box fmt ();
- (* Close the variant box *)
- F.pp_close_box fmt ()
+ F.pp_print_string fmt ":";
+ F.pp_print_space fmt ();
+ extract_ty ctx fmt false f.field_ty;
+ F.pp_print_string fmt ";";
+ F.pp_close_box fmt ()
+ in
+ let fields = FieldId.mapi (fun fid f -> (fid, f)) fields in
+ Collections.List.iter_link (F.pp_print_space fmt)
+ (fun (fid, f) -> print_field fid f)
+ fields;
+ (* Close *)
+ F.pp_close_box fmt ();
+ F.pp_print_space fmt ();
+ 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
+ *)
+ assert (is_rec && !backend = Coq);
+ let cons_name = ctx_get_struct (AdtId def.def_id) ctx in
+ let def_name = ctx_get_local_type def.def_id ctx in
+ extract_type_decl_variant ctx fmt def_name type_params cons_name fields)
in
- (* Print the variants *)
- let variants = VariantId.mapi (fun vid v -> (vid, v)) variants in
- List.iter (fun (vid, v) -> print_variant vid v) variants
+ ()
(** Extract a type declaration.
@@ -680,7 +837,27 @@ let extract_type_decl_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
registered.
*)
let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter)
- (qualif : type_decl_qualif) (def : type_decl) : unit =
+ (kind : decl_kind) (def : type_decl) : unit =
+ let extract_body =
+ match kind with
+ | SingleNonRec | SingleRec | MutRecFirst | MutRecInner | MutRecLast -> true
+ | Assumed | Declared -> false
+ in
+ let type_kind =
+ if extract_body then
+ match def.kind with
+ | Struct _ -> Some Struct
+ | Enum _ -> Some Enum
+ | Opaque -> None
+ else None
+ in
+ (* If in Coq and the declaration is opaque, it must have the shape:
+ [Axiom Ident : forall (T0 ... Tn : Type), ... -> ... -> ...].
+
+ The boolean [is_opaque_coq] is used to detect this case.
+ *)
+ let is_opaque_coq = !backend = Coq && type_kind = None in
+ let use_forall = is_opaque_coq && def.type_params <> [] in
(* Retrieve the definition name *)
let def_name = ctx_get_local_type def.def_id ctx in
(* Add the type params - note that we need those bindings only for the
@@ -697,16 +874,16 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter)
(* Open a box for "type TYPE_NAME (TYPE_PARAMS) =" *)
F.pp_open_hovbox fmt ctx.indent_incr;
(* > "type TYPE_NAME" *)
- let extract_body, qualif =
- match qualif with
- | Type -> (true, "type")
- | And -> (true, "and")
- | AssumeType -> (false, "assume type")
- | TypeVal -> (false, "val")
- in
+ 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 -> "Type" in
if def.type_params <> [] then (
+ if use_forall then (
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt ":";
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt "forall");
F.pp_print_space fmt ();
F.pp_print_string fmt "(";
List.iter
@@ -717,34 +894,117 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter)
def.type_params;
F.pp_print_string fmt ":";
F.pp_print_space fmt ();
- F.pp_print_string fmt "Type0)");
+ F.pp_print_string fmt (type_keyword ^ ")"));
(* Print the "=" if we extract the body*)
if extract_body then (
F.pp_print_space fmt ();
- F.pp_print_string fmt "=")
+ let eq = match !backend with FStar -> "=" | Coq -> ":=" in
+ F.pp_print_string fmt eq)
else (
(* Otherwise print ": Type0" *)
+ if use_forall then F.pp_print_string fmt ","
+ else (
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt ":");
F.pp_print_space fmt ();
- F.pp_print_string fmt ":";
- F.pp_print_space fmt ();
- F.pp_print_string fmt "Type0");
+ F.pp_print_string fmt type_keyword);
(* Close the box for "type TYPE_NAME (TYPE_PARAMS) =" *)
F.pp_close_box fmt ();
(if extract_body then
match def.kind with
- | Struct fields -> extract_type_decl_struct_body ctx_body fmt def fields
+ | Struct fields ->
+ extract_type_decl_struct_body ctx_body fmt kind def type_params fields
| Enum variants ->
extract_type_decl_enum_body ctx_body fmt def def_name type_params
variants
| Opaque -> raise (Failure "Unreachable"));
+ (* If Coq: end the definition with a "." *)
+ print_decl_end_delimiter fmt kind;
(* Close the box for the definition *)
F.pp_close_box fmt ();
(* Add breaks to insert new lines between definitions *)
F.pp_print_break fmt 0 0
+(** Extract extra information for a type (e.g., [Arguments] information in Coq).
+
+ Note that all the names used for extraction should already have been
+ registered.
+ *)
+let extract_type_decl_extra_info (ctx : extraction_ctx) (fmt : F.formatter)
+ (kind : decl_kind) (decl : type_decl) : unit =
+ match !backend with
+ | FStar -> ()
+ | Coq -> (
+ (* Add the type params - note that we need those bindings only for the
+ * body translation (they are not top-level) *)
+ let _ctx_body, type_params = ctx_add_type_params decl.type_params ctx in
+ (* Auxiliary function to extract an [Arguments Cons {T} _ _.] instruction *)
+ let extract_arguments_info (cons_name : string) (fields : 'a list) : unit
+ =
+ (* Add a break before *)
+ F.pp_print_break fmt 0 0;
+ (* Open a box *)
+ F.pp_open_hovbox fmt ctx.indent_incr;
+ (* Small utility *)
+ let print_type_vars () =
+ List.iter
+ (fun (var : string) ->
+ F.pp_print_string fmt ("{" ^ var ^ "}");
+ F.pp_print_space fmt ())
+ type_params
+ in
+ let print_fields () =
+ List.iter
+ (fun _ ->
+ F.pp_print_string fmt "_";
+ F.pp_print_space fmt ())
+ fields
+ in
+ F.pp_print_break fmt 0 0;
+ F.pp_print_string fmt "Arguments";
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt cons_name;
+ F.pp_print_space fmt ();
+ print_type_vars ();
+ print_fields ();
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt ".";
+
+ (* Close the box *)
+ F.pp_close_box fmt ()
+ in
+
+ (* Generate the [Arguments] instruction *)
+ match decl.kind with
+ | Opaque -> ()
+ | Struct fields ->
+ let adt_id = AdtId decl.def_id in
+ (* Generate the instruction for the record constructor *)
+ let cons_name = ctx_get_struct adt_id ctx in
+ extract_arguments_info cons_name fields;
+ (* Generate the instruction for the record projectors, if there are *)
+ let is_rec = decl_is_from_rec_group kind in
+ if not is_rec then
+ FieldId.iteri
+ (fun fid _ ->
+ let cons_name = ctx_get_field adt_id fid ctx in
+ extract_arguments_info cons_name [])
+ fields;
+ (* Add breaks to insert new lines between definitions *)
+ F.pp_print_break fmt 0 0
+ | Enum variants ->
+ (* Generate the instructions *)
+ VariantId.iteri
+ (fun vid (v : variant) ->
+ let cons_name = ctx_get_variant (AdtId decl.def_id) vid ctx in
+ extract_arguments_info cons_name v.fields)
+ variants;
+ (* Add breaks to insert new lines between definitions *)
+ F.pp_print_break fmt 0 0)
+
(** Extract the state type declaration. *)
let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
- (qualif : type_decl_qualif) : unit =
+ (kind : decl_kind) : unit =
(* Add a break before *)
F.pp_print_break fmt 0 0;
(* Print a comment *)
@@ -755,27 +1015,48 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
F.pp_open_hvbox fmt 0;
(* Retrieve the name *)
let state_name = ctx_get_assumed_type State ctx in
- (* The qualif should be [AssumeType] or [TypeVal] *)
- (match qualif with
- | Type | And -> raise (Failure "Unexpected")
- | AssumeType ->
- F.pp_print_string fmt "assume";
- F.pp_print_space fmt ();
- F.pp_print_string fmt "type";
- 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 "Type0"
- | TypeVal ->
- F.pp_print_string fmt "val";
- 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 "Type0");
+ (* The kind should be [Assumed] or [Declared] *)
+ (match kind with
+ | SingleNonRec | SingleRec | MutRecFirst | MutRecInner | MutRecLast ->
+ raise (Failure "Unexpected")
+ | Assumed -> (
+ match !backend with
+ | FStar ->
+ F.pp_print_string fmt "assume";
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt "type";
+ 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 "Type0"
+ | Coq ->
+ 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.")
+ | Declared -> (
+ match !backend with
+ | FStar ->
+ F.pp_print_string fmt "val";
+ 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 "Type0"
+ | Coq ->
+ 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."));
(* Close the box for the definition *)
F.pp_close_box fmt ();
(* Add breaks to insert new lines between definitions *)
@@ -813,7 +1094,8 @@ let extract_global_decl_register_names (ctx : extraction_ctx)
Note that patterns can introduce new variables: we thus return an extraction
context updated with new bindings.
- TODO: we don't need something very generic anymore
+ TODO: we don't need something very generic anymore (some definitions used
+ to be polymorphic).
*)
let extract_adt_g_value
(extract_value : extraction_ctx -> bool -> 'v -> extraction_ctx)
@@ -823,17 +1105,23 @@ let extract_adt_g_value
match ty with
| Adt (Tuple, _) ->
(* Tuple *)
- F.pp_print_string fmt "(";
- let ctx =
- Collections.List.fold_left_link
- (fun () ->
- F.pp_print_string fmt ",";
- F.pp_print_space fmt ())
- (fun ctx v -> extract_value ctx false v)
- ctx field_values
- in
- F.pp_print_string fmt ")";
- ctx
+ (* This is very annoying: in Coq, we can't write [()] for the value of
+ type [unit], we have to write [tt]. *)
+ if !backend = Coq && field_values = [] then (
+ F.pp_print_string fmt "tt";
+ ctx)
+ else (
+ F.pp_print_string fmt "(";
+ let ctx =
+ Collections.List.fold_left_link
+ (fun () ->
+ F.pp_print_string fmt ",";
+ F.pp_print_space fmt ())
+ (fun ctx v -> extract_value ctx false v)
+ ctx field_values
+ in
+ F.pp_print_string fmt ")";
+ ctx)
| Adt (adt_id, _) ->
(* "Regular" ADT *)
(* We print something of the form: [Cons field0 ... fieldn].
@@ -1014,15 +1302,19 @@ and extract_adt_cons (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
| Tuple ->
(* Tuple *)
(* For now, we only support fully applied tuple constructors *)
+ (* This is very annoying: in Coq, we can't write [()] for the value of
+ type [unit], we have to write [tt]. *)
assert (List.length type_args = List.length args);
- F.pp_print_string fmt "(";
- Collections.List.iter_link
- (fun () ->
- F.pp_print_string fmt ",";
- F.pp_print_space fmt ())
- (fun v -> extract_texpression ctx fmt false v)
- args;
- F.pp_print_string fmt ")"
+ if !backend = Coq && args = [] then F.pp_print_string fmt "tt"
+ else (
+ F.pp_print_string fmt "(";
+ Collections.List.iter_link
+ (fun () ->
+ F.pp_print_string fmt ",";
+ F.pp_print_space fmt ())
+ (fun v -> extract_texpression ctx fmt false v)
+ args;
+ F.pp_print_string fmt ")")
| _ ->
(* "Regular" ADT *)
(* We print something of the form: [Cons field0 ... fieldn].
@@ -1062,7 +1354,10 @@ and extract_field_projector (ctx : extraction_ctx) (fmt : F.formatter)
(* We allow to break where the "." appears *)
F.pp_print_break fmt 0 0;
F.pp_print_string fmt ".";
- F.pp_print_string fmt field_name;
+ (* 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 ^ ")"));
(* Close the box *)
F.pp_close_box fmt ()
| arg :: args ->
@@ -1114,7 +1409,8 @@ and extract_Let (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
* a variable *)
let ctx = extract_typed_pattern ctx fmt true lv in
F.pp_print_space fmt ();
- F.pp_print_string fmt "<--";
+ let arrow = match !backend with FStar -> "<--" | Coq -> "<-" in
+ F.pp_print_string fmt arrow;
F.pp_print_space fmt ();
extract_texpression ctx fmt false re;
F.pp_print_string fmt ";";
@@ -1124,7 +1420,8 @@ and extract_Let (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 ();
- F.pp_print_string fmt "=";
+ let eq = match !backend with FStar -> "=" | Coq -> ":=" in
+ F.pp_print_string fmt eq;
F.pp_print_space fmt ();
extract_texpression ctx fmt false re;
F.pp_print_space fmt ();
@@ -1170,15 +1467,18 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
F.pp_open_hovbox fmt ctx.indent_incr;
(* Print the [begin] if necessary *)
let parenth = PureUtils.let_group_requires_parentheses e_branch in
+ let left_delim, right_delim =
+ match !backend with FStar -> ("begin", "end") | Coq -> ("(", ")")
+ in
if parenth then (
- F.pp_print_string fmt "begin";
+ F.pp_print_string fmt left_delim;
F.pp_print_space fmt ());
(* Print the branch expression *)
extract_texpression ctx fmt false e_branch;
(* Close the [begin ... end ] *)
if parenth then (
F.pp_print_space fmt ();
- F.pp_print_string fmt "end");
+ F.pp_print_string fmt right_delim);
(* Close the box for the branch *)
F.pp_close_box fmt ();
(* Close the box for the then/else+branch *)
@@ -1191,7 +1491,10 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
(* Open a box for the [match ... with] *)
F.pp_open_hovbox fmt ctx.indent_incr;
(* Print the [match ... with] *)
- F.pp_print_string fmt "begin match";
+ let match_begin =
+ match !backend with FStar -> "begin match" | Coq -> "match"
+ in
+ F.pp_print_string fmt match_begin;
F.pp_print_space fmt ();
let scrut_inside = PureUtils.let_group_requires_parentheses scrut in
extract_texpression ctx fmt scrut_inside scrut;
@@ -1210,7 +1513,8 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
F.pp_print_space fmt ();
let ctx = extract_typed_pattern ctx fmt false br.pat in
F.pp_print_space fmt ();
- F.pp_print_string fmt "->";
+ let arrow = match !backend with FStar -> "->" | Coq -> "=>" in
+ F.pp_print_string fmt arrow;
F.pp_print_space fmt ();
(* Open a box for the branch *)
F.pp_open_hovbox fmt ctx.indent_incr;
@@ -1258,7 +1562,8 @@ let extract_fun_parameters (ctx : extraction_ctx) (fmt : F.formatter)
def.signature.type_params;
F.pp_print_string fmt ":";
F.pp_print_space fmt ();
- F.pp_print_string fmt "Type0)";
+ let type_keyword = match !backend with FStar -> "Type0" | Coq -> "Type" in
+ F.pp_print_string fmt (type_keyword ^ ")");
(* Close the box for the type parameters *)
F.pp_close_box fmt ();
F.pp_print_space fmt ());
@@ -1305,8 +1610,10 @@ let extract_fun_input_parameters_types (ctx : extraction_ctx)
(** Extract a decrease clause function template body.
+ Only for F*.
+
In order to help the user, we can generate a template for the functions
- required by the decreases clauses. We simply generate definitions of
+ required by the decreases clauses for. We simply generate definitions of
the following form in a separate file:
{[
let f_decrease (t : Type0) (x : t) : nat = admit()
@@ -1319,6 +1626,7 @@ let extract_fun_input_parameters_types (ctx : extraction_ctx)
*)
let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter)
(def : fun_decl) : unit =
+ assert (!backend = FStar);
(* Retrieve the function name *)
let def_name = ctx_get_decreases_clause def.def_id ctx in
(* Add a break before *)
@@ -1371,14 +1679,10 @@ let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter)
it is useful for the decrease clause.
*)
let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
- (qualif : fun_decl_qualif) (has_decreases_clause : bool) (def : fun_decl) :
- unit =
+ (kind : decl_kind) (has_decreases_clause : bool) (def : fun_decl) : unit =
assert (not def.is_global_decl_body);
(* Retrieve the function name *)
let def_name = ctx_get_local_function def.def_id def.back_id ctx in
- (* (* Add the type parameters - note that we need those bindings only for the
- * body translation (they are not top-level) *)
- let ctx, _ = ctx_add_type_params def.signature.type_params ctx in *)
(* Add a break before *)
F.pp_print_break fmt 0 0;
(* Print a comment to link the extracted type to its original rust definition *)
@@ -1392,9 +1696,21 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_open_hovbox fmt ctx.indent_incr;
(* > "let FUN_NAME" *)
let is_opaque = Option.is_none def.body in
- let qualif = fun_decl_qualif_keyword qualif in
+ (* If in Coq and the declaration is opaque, it must have the shape:
+ [Axiom Ident : forall (T0 ... Tn : Type), ... -> ... -> ...].
+
+ The boolean [is_opaque_coq] is used to detect this case.
+ *)
+ let is_opaque_coq = !backend = Coq && is_opaque in
+ let use_forall = is_opaque_coq && def.signature.type_params <> [] in
+ (* *)
+ let qualif = ctx.fmt.fun_decl_kind_to_qualif kind in
F.pp_print_string fmt (qualif ^ " " ^ def_name);
F.pp_print_space fmt ();
+ if use_forall then (
+ F.pp_print_string fmt ":";
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt "forall");
(* Open a box for "(PARAMS) : EFFECT =" *)
F.pp_open_hvbox fmt 0;
(* Open a box for "(PARAMS)" *)
@@ -1408,7 +1724,7 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
* the bindings we introduced above.
* TODO: figure out a cleaner way *)
let _ =
- F.pp_print_string fmt ":";
+ if use_forall then F.pp_print_string fmt "," else F.pp_print_string fmt ":";
F.pp_print_space fmt ();
(* Open a box for the EFFECT *)
F.pp_open_hvbox fmt 0;
@@ -1421,6 +1737,7 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
if is_opaque then extract_fun_input_parameters_types ctx fmt def;
(* [Tot] *)
if has_decreases_clause then (
+ assert (!backend = FStar);
F.pp_print_string fmt "Tot";
F.pp_print_space fmt ());
extract_ty ctx fmt has_decreases_clause def.signature.output;
@@ -1429,6 +1746,7 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
(* Print the decrease clause - rk.: a function with a decreases clause
* is necessarily a transparent function *)
if has_decreases_clause then (
+ assert (!backend = FStar);
F.pp_print_space fmt ();
(* Open a box for the decrease clause *)
F.pp_open_hovbox fmt 0;
@@ -1476,7 +1794,8 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
(* Print the "=" *)
if not is_opaque then (
F.pp_print_space fmt ();
- F.pp_print_string fmt "=");
+ let eq = match !backend with FStar -> "=" | Coq -> ":=" in
+ F.pp_print_string fmt eq);
(* Close the box for "(PARAMS) : EFFECT =" *)
F.pp_close_box fmt ();
(* Close the box for "let FUN_NAME (PARAMS) : EFFECT =" *)
@@ -1487,16 +1806,22 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_open_hvbox fmt 0;
(* Extract the body *)
let _ = extract_texpression ctx_body fmt false (Option.get def.body).body in
+ (* Coq: add a "." *)
+ print_decl_end_delimiter fmt kind;
(* Close the box for the body *)
F.pp_close_box fmt ());
+ (* Coq: add a "." *)
+ if is_opaque_coq then print_decl_end_delimiter fmt kind;
(* Close the box for the definition *)
F.pp_close_box fmt ();
(* Add breaks to insert new lines between definitions *)
F.pp_print_break fmt 0 0
-(** Extract a global declaration body of the shape "QUALIF NAME : TYPE = BODY" with a custom body extractor *)
+(** Extract a global declaration body of the shape "QUALIF NAME : TYPE = BODY"
+ with a custom body extractor
+ *)
let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter)
- (qualif : fun_decl_qualif) (name : string) (ty : ty)
+ (kind : decl_kind) (name : string) (ty : ty)
(extract_body : (F.formatter -> unit) Option.t) : unit =
let is_opaque = Option.is_none extract_body in
@@ -1506,7 +1831,9 @@ let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter)
(* Open "QUALIF NAME : TYPE =" box (depth=1) *)
F.pp_open_hovbox fmt ctx.indent_incr;
(* Print "QUALIF NAME " *)
- F.pp_print_string fmt (fun_decl_qualif_keyword qualif ^ " " ^ name);
+ F.pp_print_string fmt (ctx.fmt.fun_decl_kind_to_qualif kind);
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt name;
F.pp_print_space fmt ();
(* Open ": TYPE =" box (depth=2) *)
@@ -1525,7 +1852,8 @@ let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter)
if not is_opaque then (
(* Print " =" *)
F.pp_print_space fmt ();
- F.pp_print_string fmt "=");
+ let eq = match !backend with FStar -> "=" | Coq -> ":=" in
+ F.pp_print_string fmt eq);
(* Close ": TYPE =" box (depth=2) *)
F.pp_close_box fmt ();
(* Close "QUALIF NAME : TYPE =" box (depth=1) *)
@@ -1539,16 +1867,22 @@ let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter)
(Option.get extract_body) fmt;
(* Close "BODY" box (depth=1) *)
F.pp_close_box fmt ());
+
+ (* Coq: add a "." *)
+ print_decl_end_delimiter fmt Declared;
+
(* Close the definition box (depth=0) *)
F.pp_close_box fmt ()
(** Extract a global declaration.
- We generate the body which computes the global value separately from the value declaration itself.
+
+ We generate the body which computes the global value separately from the
+ value declaration itself.
For example in Rust,
[static X: u32 = 3;]
- will be translated to:
+ will be translated to the following F*:
[let x_body : result u32 = Return 3]
[let x_c : u32 = eval_global x_body]
*)
@@ -1578,22 +1912,37 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
in
match body.body with
| None ->
- let qualif = if interface then Val else AssumeVal in
- extract_global_decl_body ctx fmt qualif decl_name decl_ty None
+ let kind = if interface then Declared else Assumed in
+ extract_global_decl_body ctx fmt kind decl_name decl_ty None
| Some body ->
- extract_global_decl_body ctx fmt Let body_name body_ty
+ extract_global_decl_body ctx fmt SingleNonRec body_name body_ty
(Some (fun fmt -> extract_texpression ctx fmt false body.body));
F.pp_print_break fmt 0 0;
- extract_global_decl_body ctx fmt Let decl_name decl_ty
- (Some (fun fmt -> F.pp_print_string fmt ("eval_global " ^ body_name)));
+ extract_global_decl_body ctx fmt SingleNonRec decl_name decl_ty
+ (Some
+ (fun fmt ->
+ let body =
+ match !backend with
+ | FStar -> "eval_global " ^ body_name
+ | Coq -> body_name ^ "%global"
+ in
+ F.pp_print_string fmt body));
+ (* Add a break to insert lines between declarations *)
F.pp_print_break fmt 0 0
(** Extract a unit test, if the function is a unit function (takes no
parameters, returns unit).
- A unit test simply checks that the function normalizes to [Return ()]:
+ A unit test simply checks that the function normalizes to [Return ()].
+
+ F*:
{[
- let _ = assert_norm (FUNCTION () = Return ())
+ let _ = assert_norm (FUNCTION = Return ())
+ ]}
+
+ Coq:
+ {[
+ Check (FUNCTION)%return).
]}
*)
let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
@@ -1616,21 +1965,34 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
(* Open a box for the test *)
F.pp_open_hovbox fmt ctx.indent_incr;
(* Print the test *)
- F.pp_print_string fmt "let _ =";
- F.pp_print_space fmt ();
- F.pp_print_string fmt "assert_norm";
- F.pp_print_space fmt ();
- F.pp_print_string fmt "(";
- let fun_name = ctx_get_local_function def.def_id def.back_id ctx in
- F.pp_print_string fmt fun_name;
- if sg.inputs <> [] then (
- F.pp_print_space fmt ();
- F.pp_print_string fmt "()");
- F.pp_print_space fmt ();
- 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 ^ " ())");
+ (match !backend with
+ | FStar ->
+ F.pp_print_string fmt "let _ =";
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt "assert_norm";
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt "(";
+ let fun_name = ctx_get_local_function def.def_id def.back_id ctx in
+ F.pp_print_string fmt fun_name;
+ if sg.inputs <> [] then (
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt "()");
+ F.pp_print_space fmt ();
+ 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 ^ " ())")
+ | Coq ->
+ F.pp_print_string fmt "Check";
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt "(";
+ let fun_name = ctx_get_local_function def.def_id def.back_id ctx in
+ F.pp_print_string fmt fun_name;
+ if sg.inputs <> [] then (
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt "()");
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt ")%return.");
(* Close the box for the test *)
F.pp_close_box fmt ();
(* Add a break after *)
diff --git a/compiler/PureToExtract.ml b/compiler/ExtractBase.ml
index 25ad6713..33939e6a 100644
--- a/compiler/PureToExtract.ml
+++ b/compiler/ExtractBase.ml
@@ -1,8 +1,4 @@
-(** This module is used to extract the pure ASTs to various theorem provers.
- It defines utilities and helpers to make the work as easy as possible:
- we try to factorize as much as possible the different extractions to the
- backends we target.
- *)
+(** Define base utilities for the extraction *)
open Pure
open TranslateCore
@@ -33,8 +29,79 @@ type type_name = Names.type_name
type global_name = Names.global_name
type fun_name = Names.fun_name
+(** Characterizes a declaration.
+
+ Is in particular useful to derive the proper keywords to introduce the
+ declarations/definitions.
+ *)
+type decl_kind =
+ | SingleNonRec
+ (** A single, non-recursive definition.
+
+ F*: [let x = ...]
+ Coq: [Definition x := ...]
+ *)
+ | SingleRec
+ (** A single, recursive definition.
+
+ F*: [let rec x = ...]
+ Coq: [Fixpoint x := ...]
+ *)
+ | MutRecFirst
+ (** The first definition of a group of mutually-recursive definitions.
+
+ F*: [type x0 = ... and x1 = ...]
+ Coq: [Fixpoing x0 := ... with x1 := ...]
+ *)
+ | MutRecInner
+ (** An inner definition in a group of mutually-recursive definitions. *)
+ | MutRecLast
+ (** The last definition in a group of mutually-recursive definitions.
+
+ We need this because in some theorem provers like Coq, we need to
+ delimit group of mutually recursive definitions (in particular, we
+ need to insert an end delimiter).
+ *)
+ | Assumed
+ (** An assumed definition.
+
+ F*: [assume val x]
+ Coq: [Axiom x : Type.]
+ *)
+ | Declared
+ (** Declare a type in an interface or a module signature.
+
+ Rem.: for now, in Coq, we don't declare module signatures: we
+ thus assume the corresponding declarations.
+
+ F*: [val x : Type0]
+ Coq: [Axiom x : Type.]
+ *)
+
+(** Return [true] if the declaration is the last from its group of declarations.
+
+ We need this because in some provers (e.g., Coq), we need to delimit the
+ end of a (group of) definition(s) (in Coq: with a ".").
+ *)
+let decl_is_last_from_group (kind : decl_kind) : bool =
+ match kind with
+ | SingleNonRec | SingleRec | MutRecLast | Assumed | Declared -> true
+ | MutRecFirst | MutRecInner -> false
+
+let decl_is_from_rec_group (kind : decl_kind) : bool =
+ match kind with
+ | SingleNonRec | Assumed | Declared -> false
+ | SingleRec | MutRecFirst | MutRecInner | MutRecLast -> true
+
+let decl_is_from_mut_rec_group (kind : decl_kind) : bool =
+ match kind with
+ | SingleNonRec | SingleRec | Assumed | Declared -> false
+ | MutRecFirst | MutRecInner | MutRecLast -> true
+
(* TODO: this should a module we give to a functor! *)
+type type_decl_kind = Enum | Struct
+
(** A formatter's role is twofold:
1. Come up with name suggestions.
For instance, provided some information about a function (its basename,
@@ -51,6 +118,16 @@ type formatter = {
char_name : string;
int_name : integer_type -> string;
str_name : string;
+ type_decl_kind_to_qualif : decl_kind -> type_decl_kind option -> string;
+ (** Compute the qualified for a type definition/declaration.
+
+ For instance: "type", "and", etc.
+ *)
+ fun_decl_kind_to_qualif : decl_kind -> string;
+ (** Compute the qualified for a function definition/declaration.
+
+ For instance: "let", "let rec", "and", etc.
+ *)
field_name : name -> FieldId.id -> string option -> string;
(** Inputs:
- type name
diff --git a/compiler/ExtractToCoq.ml b/compiler/ExtractToCoq.ml
new file mode 100644
index 00000000..3681adc3
--- /dev/null
+++ b/compiler/ExtractToCoq.ml
@@ -0,0 +1,8 @@
+(** Utilities for the extraction to Coq *)
+
+open Utils
+open Pure
+open TranslateCore
+open ExtractBase
+open StringUtils
+module F = Format
diff --git a/compiler/ExtractToFStar.ml b/compiler/ExtractToFStar.ml
new file mode 100644
index 00000000..21a6fc8f
--- /dev/null
+++ b/compiler/ExtractToFStar.ml
@@ -0,0 +1,8 @@
+(** Utilities for the extraction to F* *)
+
+open Utils
+open Pure
+open TranslateCore
+open ExtractBase
+open StringUtils
+module F = Format
diff --git a/compiler/Logging.ml b/compiler/Logging.ml
index 5f22506b..1d57fa5b 100644
--- a/compiler/Logging.ml
+++ b/compiler/Logging.ml
@@ -18,8 +18,8 @@ let symbolic_to_pure_log = L.get_logger "MainLogger.SymbolicToPure"
(** Logger for PureMicroPasses *)
let pure_micro_passes_log = L.get_logger "MainLogger.PureMicroPasses"
-(** Logger for PureToExtract *)
-let pure_to_extract_log = L.get_logger "MainLogger.PureToExtract"
+(** Logger for ExtractBase *)
+let pure_to_extract_log = L.get_logger "MainLogger.ExtractBase"
(** Logger for Interpreter *)
let interpreter_log = L.get_logger "MainLogger.Interpreter"
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 30fc4989..7b261516 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1250,6 +1250,7 @@ let apply_passes_to_def (ctx : trans_ctx) (def : fun_decl) : fun_decl option =
(lazy ("filter_useless:\n\n" ^ fun_decl_to_string ctx def ^ "\n"));
(* Simplify the aggregated ADTs.
+
Ex.:
{[
type struct = { f0 : nat; f1 : nat }
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index ff55f322..5a024d9e 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -398,9 +398,9 @@ let mk_simpl_tuple_texpression (vl : texpression list) : texpression =
let cons = { e = Qualif qualif; ty } in
mk_apps cons vl
-let mk_adt_pattern (adt_ty : ty) (variant_id : VariantId.id)
+let mk_adt_pattern (adt_ty : ty) (variant_id : VariantId.id option)
(vl : typed_pattern list) : typed_pattern =
- let value = PatAdt { variant_id = Some variant_id; field_values = vl } in
+ let value = PatAdt { variant_id; field_values = vl } in
{ value; ty = adt_ty }
let ty_as_integer (t : ty) : T.integer_type =
diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index 235e33e4..9d95db7f 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -26,6 +26,7 @@ type mplace = {
projection : E.projection;
(** We store the projection because we can, but it is actually not that useful *)
}
+[@@deriving show]
type call_id =
| Fun of A.fun_id * V.FunCallId.id
@@ -43,6 +44,7 @@ type call = {
dest : V.symbolic_value;
dest_place : mplace option; (** Meta information *)
}
+[@@deriving show]
(** Meta information, not necessary for synthesis but useful to guide it to
generate a pretty output.
@@ -51,6 +53,7 @@ type call = {
type meta =
| Assignment of mplace * V.typed_value * mplace option
(** We generated an assignment (destination, assigned value, src) *)
+[@@deriving show]
(** **Rk.:** here, {!expression} is not at all equivalent to the expressions
used in LLBC: they are a first step towards lambda-calculus expressions.
@@ -108,3 +111,4 @@ and expansion =
T.integer_type * (V.scalar_value * expression) list * expression
(** An integer expansion (i.e, a switch over an integer). The last
expression is for the "otherwise" branch. *)
+[@@deriving show]
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index a327c785..62be5efd 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1578,8 +1578,17 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
(* We don't do the same thing if there is a branching or not *)
match branches with
| [] -> raise (Failure "Unreachable")
- | [ (variant_id, svl, branch) ] -> (
- (* There is exactly one branch: no branching *)
+ | [ (variant_id, svl, branch) ]
+ when not
+ (TypesUtils.ty_is_custom_adt sv.V.sv_ty
+ && !Config.always_deconstruct_adts_with_matches) -> (
+ (* There is exactly one branch: no branching.
+
+ We can decompose the ADT value with a let-binding, unless
+ the backend doesn't support this (see {!Config.always_deconstruct_adts_with_matches}):
+ we *ignore* this branch (and go to the next one) if the ADT is a custom
+ adt, and [always_deconstruct_adts_with_matches] is true.
+ *)
let type_id, _, _ = TypesUtils.ty_as_adt sv.V.sv_ty in
let ctx, vars = fresh_vars_for_symbolic_values svl ctx in
let branch = translate_expression branch ctx in
@@ -1588,9 +1597,16 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
(* Detect if this is an enumeration or not *)
let tdef = bs_ctx_lookup_llbc_type_decl adt_id ctx in
let is_enum = type_decl_is_enum tdef in
- if is_enum then
- (* This is an enumeration: introduce an [ExpandEnum] let-binding *)
- let variant_id = Option.get variant_id in
+ (* We deconstruct the ADT with a let-binding in two situations:
+ - if the ADT is an enumeration (which must have exactly one branch)
+ - if we forbid using field projectors.
+
+ We forbid using field projectors in some situations, for example
+ if the backend is Coq. See '!Config.dont_use_field_projectors}.
+ *)
+ let use_let = is_enum || !Config.dont_use_field_projectors in
+ if use_let then
+ (* Introduce a let binding which expands the ADT *)
let lvars =
List.map (fun v -> mk_typed_pattern_from_var v None) vars
in
@@ -1665,8 +1681,6 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
let translate_branch (variant_id : T.VariantId.id option)
(svl : V.symbolic_value list) (branch : S.expression) :
match_branch =
- (* There *must* be a variant id - otherwise there can't be several branches *)
- let variant_id = Option.get variant_id in
let ctx, vars = fresh_vars_for_symbolic_values svl ctx in
let vars =
List.map (fun x -> mk_typed_pattern_from_var x None) vars
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 79d1c913..b2a28710 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -293,7 +293,7 @@ let translate_module_to_pure (crate : A.crate) :
(** Extraction context *)
type gen_ctx = {
crate : A.crate;
- extract_ctx : PureToExtract.extraction_ctx;
+ extract_ctx : ExtractBase.extraction_ctx;
trans_types : Pure.type_decl Pure.TypeDeclId.Map.t;
trans_funs : (bool * pure_fun_translation) A.FunDeclId.Map.t;
functions_with_decreases_clause : A.FunDeclId.Set.t;
@@ -342,30 +342,41 @@ let module_has_opaque_decls (ctx : gen_ctx) : bool * bool =
*)
let extract_definitions (fmt : Format.formatter) (config : gen_config)
(ctx : gen_ctx) : unit =
- (* Export the definition groups to the file, in the proper order *)
- let export_type (qualif : ExtractToBackend.type_decl_qualif)
- (id : Pure.TypeDeclId.id) : unit =
- (* Retrive the declaration *)
+ (* Export the definition groups to the file, in the proper order.
+ - [extract_decl]: extract the type declaration (if not filtered)
+ - [extract_extra_info]: extra the extra type information (e.g.,
+ the [Arguments] information in Coq).
+ *)
+ let export_type (kind : ExtractBase.decl_kind) (id : Pure.TypeDeclId.id)
+ (extract_decl : bool) (extract_extra_info : bool) : unit =
+ (* Retrieve the declaration *)
let def = Pure.TypeDeclId.Map.find id ctx.trans_types in
- (* Update the qualifier, if the type is opaque *)
- let is_opaque, qualif =
+ (* Update the kind, if the type is opaque *)
+ let is_opaque, kind =
match def.kind with
- | Enum _ | Struct _ -> (false, qualif)
+ | Enum _ | Struct _ -> (false, kind)
| Opaque ->
- let qualif =
- if config.interface then ExtractToBackend.TypeVal
- else ExtractToBackend.AssumeType
+ let kind =
+ if config.interface then ExtractBase.Declared
+ else ExtractBase.Assumed
in
- (true, qualif)
+ (true, kind)
in
(* Extract, if the config instructs to do so (depending on whether the type
* is opaque or not) *)
if
(is_opaque && config.extract_opaque)
|| ((not is_opaque) && config.extract_transparent)
- then ExtractToBackend.extract_type_decl ctx.extract_ctx fmt qualif def
+ then (
+ if extract_decl then
+ Extract.extract_type_decl ctx.extract_ctx fmt kind def;
+ if extract_extra_info then
+ Extract.extract_type_decl_extra_info ctx.extract_ctx fmt kind def)
in
+ let export_type_decl kind id = export_type kind id true false in
+ let export_type_extra_info kind id = export_type kind id false true in
+
(* Utility to check a function has a decrease clause *)
let has_decreases_clause (def : Pure.fun_decl) : bool =
A.FunDeclId.Set.mem def.def_id ctx.functions_with_decreases_clause
@@ -393,8 +404,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
(fun (_, (fwd, _)) ->
let has_decr_clause = has_decreases_clause fwd in
if has_decr_clause then
- ExtractToBackend.extract_template_decreases_clause ctx.extract_ctx fmt
- fwd)
+ Extract.extract_template_decreases_clause ctx.extract_ctx fmt fwd)
pure_ls;
(* Extract the function definitions *)
(if config.extract_fun_decls then
@@ -408,17 +418,25 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
else true
else false
in
+ let fls_length = List.length fls in
List.iteri
(fun i (fwd_def, def) ->
let is_opaque = Option.is_none fwd_def.Pure.body in
- let qualif =
+ let kind =
if is_opaque then
- if config.interface then ExtractToBackend.Val
- else ExtractToBackend.AssumeVal
- else if not is_rec then ExtractToBackend.Let
+ if config.interface then ExtractBase.Declared
+ else ExtractBase.Assumed
+ else if not is_rec then ExtractBase.SingleNonRec
else if is_mut_rec then
- if i = 0 then ExtractToBackend.LetRec else ExtractToBackend.And
- else ExtractToBackend.LetRec
+ (* If the functions are mutually recursive, we need to distinguish:
+ * - the first of the group
+ * - the last of the group
+ * - the inner functions
+ *)
+ if i = 0 then ExtractBase.MutRecFirst
+ else if i = fls_length - 1 then ExtractBase.MutRecLast
+ else ExtractBase.MutRecInner
+ else ExtractBase.SingleRec
in
let has_decr_clause =
has_decreases_clause def && config.extract_decreases_clauses
@@ -428,15 +446,14 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
((not is_opaque) && config.extract_transparent)
|| (is_opaque && config.extract_opaque)
then
- ExtractToBackend.extract_fun_decl ctx.extract_ctx fmt qualif
- has_decr_clause def)
+ Extract.extract_fun_decl ctx.extract_ctx fmt kind has_decr_clause def)
fls);
(* Insert unit tests if necessary *)
if config.test_trans_unit_functions then
List.iter
(fun (keep_fwd, (fwd, _)) ->
if keep_fwd then
- ExtractToBackend.extract_unit_test_if_unit_fun ctx.extract_ctx fmt fwd)
+ Extract.extract_unit_test_if_unit_fun ctx.extract_ctx fmt fwd)
pure_ls
in
@@ -454,32 +471,49 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
((not is_opaque) && config.extract_transparent)
|| (is_opaque && config.extract_opaque)
then
- ExtractToBackend.extract_global_decl ctx.extract_ctx fmt global body
+ Extract.extract_global_decl ctx.extract_ctx fmt global body
config.interface
in
let export_state_type () : unit =
- let qualif =
- if config.interface then ExtractToBackend.TypeVal
- else ExtractToBackend.AssumeType
+ let kind =
+ if config.interface then ExtractBase.Declared else ExtractBase.Assumed
in
- ExtractToBackend.extract_state_type fmt ctx.extract_ctx qualif
+ Extract.extract_state_type fmt ctx.extract_ctx kind
in
let export_decl (decl : A.declaration_group) : unit =
match decl with
| Type (NonRec id) ->
- if config.extract_types then export_type ExtractToBackend.Type id
+ if config.extract_types then (
+ let kind = ExtractBase.SingleNonRec in
+ (* Export the type declaration *)
+ export_type_decl kind id;
+ (* Export the extra information (ex.: [Arguments] instructions in Coq) *)
+ export_type_extra_info kind id)
| Type (Rec ids) ->
(* Rk.: we shouldn't have (mutually) recursive opaque types *)
- if config.extract_types then
+ let num_decls = List.length ids in
+ let is_mut_rec = num_decls > 1 in
+ if config.extract_types then (
+ let kind_from_index i =
+ if not is_mut_rec then ExtractBase.SingleRec
+ else if i = 0 then ExtractBase.MutRecFirst
+ else if i = num_decls - 1 then ExtractBase.MutRecLast
+ else ExtractBase.MutRecInner
+ in
+ (* Extract the type declarations *)
+ List.iteri
+ (fun i id ->
+ let kind = kind_from_index i in
+ export_type_decl kind id)
+ ids;
+ (* Export the extra information (ex.: [Arguments] instructions in Coq) *)
List.iteri
(fun i id ->
- let qualif =
- if i = 0 then ExtractToBackend.Type else ExtractToBackend.And
- in
- export_type qualif id)
- ids
+ let kind = kind_from_index i in
+ export_type_extra_info kind id)
+ ids)
| Fun (NonRec id) ->
(* Lookup *)
let pure_fun = A.FunDeclId.Map.find id ctx.trans_funs in
@@ -527,15 +561,33 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
(* Create the header *)
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 "module %s\n" module_name;
- Printf.fprintf out "open Primitives\n";
- (* Add the custom imports *)
- List.iter (fun m -> Printf.fprintf out "open %s\n" m) custom_imports;
- (* Add the custom includes *)
- List.iter (fun m -> Printf.fprintf out "include %s\n" m) custom_includes;
- (* Z3 options - note that we use fuel 1 because it its useful for the decrease clauses *)
- Printf.fprintf out "\n#set-options \"--z3rlimit 50 --fuel 1 --ifuel 1\"\n";
-
+ (match !Config.backend with
+ | FStar ->
+ Printf.fprintf out "module %s\n" module_name;
+ Printf.fprintf out "open Primitives\n";
+ (* Add the custom imports *)
+ List.iter (fun m -> Printf.fprintf out "open %s\n" m) custom_imports;
+ (* Add the custom includes *)
+ List.iter (fun m -> Printf.fprintf out "include %s\n" m) custom_includes;
+ (* Z3 options - note that we use fuel 1 because it its useful for the decrease clauses *)
+ Printf.fprintf out "\n#set-options \"--z3rlimit 50 --fuel 1 --ifuel 1\"\n"
+ | Coq ->
+ Printf.fprintf out "Require Import Primitives.\n";
+ Printf.fprintf out "Import Primitives.\n";
+ Printf.fprintf out "Require Import Coq.ZArith.ZArith.\n";
+ Printf.fprintf out "Local Open Scope Primitives_scope.\n";
+
+ (* Add the custom imports *)
+ List.iter
+ (fun m -> Printf.fprintf out "Require Import %s .\n" m)
+ custom_imports;
+ (* Add the custom includes *)
+ List.iter
+ (fun m ->
+ Printf.fprintf out "Require Export %s .\n" m;
+ Printf.fprintf out "Import %s .\n" m)
+ custom_includes;
+ Printf.fprintf out "Module %s .\n" module_name);
(* From now onwards, we use the formatter *)
(* Set the margin *)
Format.pp_set_margin fmt 80;
@@ -550,6 +602,11 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
Format.pp_close_box fmt ();
Format.pp_print_newline fmt ();
+ (* Close the module *)
+ (match !Config.backend with
+ | FStar -> ()
+ | Coq -> Printf.fprintf out "End %s .\n" module_name);
+
(* Some logging *)
log#linfo (lazy ("Generated: " ^ filename));
@@ -568,17 +625,12 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
* We initialize the names map by registering the keywords used in the
* language, as well as some primitive names ("u32", etc.) *)
let variant_concatenate_type_name = true in
- let fstar_fmt =
- ExtractToBackend.mk_formatter trans_ctx crate.name
+ let mk_formatter_and_names_map = Extract.mk_formatter_and_names_map in
+ let fmt, names_map =
+ mk_formatter_and_names_map trans_ctx crate.name
variant_concatenate_type_name
in
- let names_map =
- PureToExtract.initialize_names_map fstar_fmt
- ExtractToBackend.fstar_names_map_init
- in
- let ctx =
- { PureToExtract.trans_ctx; names_map; fmt = fstar_fmt; indent_incr = 2 }
- in
+ let ctx = { ExtractBase.trans_ctx; names_map; fmt; indent_incr = 2 } in
(* We need to compute which functions are recursive, in order to know
* whether we should generate a decrease clause or not. *)
@@ -596,7 +648,7 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
* sure there are no name clashes. *)
let ctx =
List.fold_left
- (fun ctx def -> ExtractToBackend.extract_type_decl_register_names ctx def)
+ (fun ctx def -> Extract.extract_type_decl_register_names ctx def)
ctx trans_types
in
@@ -612,14 +664,13 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
let is_global = (fst def).Pure.is_global_decl_body in
if is_global then ctx
else
- ExtractToBackend.extract_fun_decl_register_names ctx keep_fwd
- gen_decr_clause def)
+ Extract.extract_fun_decl_register_names ctx keep_fwd gen_decr_clause
+ def)
ctx trans_funs
in
let ctx =
- List.fold_left ExtractToBackend.extract_global_decl_register_names ctx
- crate.globals
+ List.fold_left Extract.extract_global_decl_register_names ctx crate.globals
in
(* Open the output file *)
@@ -658,12 +709,17 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
(* Create a directory with *default* permissions *)
Core_unix.mkdir_p dest_dir);
- (* Copy "Primitives.fst" *)
+ (* Copy the "Primitives" file *)
let _ =
(* Retrieve the executable's directory *)
let exe_dir = Filename.dirname Sys.argv.(0) in
- let src = open_in (exe_dir ^ "/backends/fstar/Primitives.fst") in
- let tgt_filename = Filename.concat dest_dir "Primitives.fst" in
+ let primitives_src, primitives_destname =
+ match !Config.backend with
+ | Config.FStar -> ("/backends/fstar/Primitives.fst", "Primitives.fst")
+ | Config.Coq -> ("/backends/coq/Primitives.v", "Primitives.v")
+ in
+ let src = open_in (exe_dir ^ primitives_src) in
+ let tgt_filename = Filename.concat dest_dir primitives_destname in
let tgt = open_out tgt_filename in
(* Very annoying: I couldn't find a "cp" function in the OCaml libraries... *)
try
@@ -689,6 +745,10 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
}
in
+ let module_delimiter =
+ match !Config.backend with FStar -> "." | Coq -> "__"
+ in
+
(* Extract one or several files, depending on the configuration *)
if !Config.split_files then (
let base_gen_config =
@@ -712,9 +772,16 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
(* Extract the types *)
(* If there are opaque types, we extract in an interface *)
- let types_filename_ext = if has_opaque_types then ".fsti" else ".fst" in
- let types_filename = extract_filebasename ^ ".Types" ^ types_filename_ext in
- let types_module = module_name ^ ".Types" in
+ let types_filename_ext =
+ match !Config.backend with
+ | FStar -> if has_opaque_types then ".fsti" else ".fst"
+ | Coq -> if has_opaque_types then ".v" else ".v"
+ in
+ let types_file_suffix = module_delimiter ^ "Types" in
+ let types_filename =
+ extract_filebasename ^ types_file_suffix ^ types_filename_ext
+ in
+ let types_module = module_name ^ types_file_suffix in
let types_config =
{
base_gen_config with
@@ -733,8 +800,12 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
&& not (A.FunDeclId.Set.is_empty rec_functions)
in
(if needs_clauses_module && !Config.extract_template_decreases_clauses then
- let clauses_filename = extract_filebasename ^ ".Clauses.Template.fst" in
- let clauses_module = module_name ^ ".Clauses.Template" in
+ let ext = match !Config.backend with FStar -> ".fst" | Coq -> ".v" in
+ let clauses_file_suffix =
+ module_delimiter ^ "Clauses" ^ module_delimiter ^ "Template"
+ in
+ let clauses_filename = extract_filebasename ^ clauses_file_suffix ^ ext in
+ let clauses_module = module_name ^ clauses_file_suffix in
let clauses_config =
{ base_gen_config with extract_template_decreases_clauses = true }
in
@@ -745,8 +816,10 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
(* Extract the opaque functions, if needed *)
let opaque_funs_module =
if has_opaque_funs then (
- let opaque_filename = extract_filebasename ^ ".Opaque.fsti" in
- let opaque_module = module_name ^ ".Opaque" in
+ let ext = match !Config.backend with FStar -> ".fsti" | Coq -> ".v" in
+ let opaque_file_suffix = module_delimiter ^ "Opaque" in
+ let opaque_filename = extract_filebasename ^ opaque_file_suffix ^ ext in
+ let opaque_module = module_name ^ opaque_file_suffix in
let opaque_config =
{
base_gen_config with
@@ -763,8 +836,10 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
in
(* Extract the functions *)
- let fun_filename = extract_filebasename ^ ".Funs.fst" in
- let fun_module = module_name ^ ".Funs" in
+ let ext = match !Config.backend with FStar -> ".fst" | Coq -> ".v" in
+ let fun_file_suffix = module_delimiter ^ "Funs" in
+ let fun_filename = extract_filebasename ^ fun_file_suffix ^ ext in
+ let fun_module = module_name ^ fun_file_suffix in
let fun_config =
{
base_gen_config with
@@ -773,7 +848,9 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
}
in
let clauses_module =
- if needs_clauses_module then [ module_name ^ ".Clauses" ] else []
+ if needs_clauses_module then
+ [ module_name ^ module_delimiter ^ "Clauses" ]
+ else []
in
extract_file fun_config gen_ctx fun_filename crate.A.name fun_module
": function definitions" []
@@ -794,6 +871,7 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
}
in
(* Add the extension for F* *)
- let extract_filename = extract_filebasename ^ ".fst" in
+ let ext = match !Config.backend with FStar -> ".fst" | Coq -> ".v" in
+ let extract_filename = extract_filebasename ^ ext in
extract_file gen_config gen_ctx extract_filename crate.A.name module_name ""
[] []
diff --git a/compiler/Values.ml b/compiler/Values.ml
index 44b22f9f..046f0482 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -817,3 +817,4 @@ type symbolic_expansion =
| SeAdt of (VariantId.id option * symbolic_value list)
| SeMutRef of BorrowId.id * symbolic_value
| SeSharedRef of BorrowId.Set.t * symbolic_value
+[@@deriving show]
diff --git a/compiler/dune b/compiler/dune
index 10aa9b10..b530340b 100644
--- a/compiler/dune
+++ b/compiler/dune
@@ -20,7 +20,10 @@
Cps
Expressions
ExpressionsUtils
- ExtractToBackend
+ Extract
+ ExtractBase
+ ExtractToCoq
+ ExtractToFStar
FunsAnalysis
Identifiers
InterpreterBorrowsCore
@@ -44,7 +47,6 @@
PrintPure
PureMicroPasses
Pure
- PureToExtract
PureTypeCheck
PureUtils
Scalars
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 01:00:11 +0000