summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/ExtractTypes.ml184
1 files changed, 41 insertions, 143 deletions
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 2fc0c117..cc0c351d 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -1666,15 +1666,15 @@ let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
(** Auxiliary function.
- Generate field projectors in Lean.
+ Generate field projectors for Lean and Coq.
- Recursive structs are defined as inductives in Lean.
+ Recursive structs are defined as inductives in Lean and Coq.
Field projectors allow to retrieve the facilities provided by
Lean structures.
*)
-let extract_type_decl_lean_record_field_projectors (ctx : extraction_ctx)
+let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
(fmt : F.formatter) (kind : decl_kind) (decl : type_decl) : unit =
- sanity_check __FILE__ __LINE__ (!backend = Lean) decl.meta;
+ sanity_check __FILE__ __LINE__ (!backend = Coq || !backend = Lean) decl.span;
match decl.kind with
| Opaque | Enum _ -> ()
| Struct fields ->
@@ -1683,18 +1683,18 @@ let extract_type_decl_lean_record_field_projectors (ctx : extraction_ctx)
if is_rec then
(* Add the type params *)
let ctx, type_params, cg_params, trait_clauses =
- ctx_add_generic_params decl.meta decl.llbc_name decl.llbc_generics
+ ctx_add_generic_params decl.span decl.llbc_name decl.llbc_generics
decl.generics ctx
in
(* Record_var will be the ADT argument to the projector *)
- let ctx, record_var = ctx_add_var decl.meta "x" (VarId.of_int 0) ctx in
+ let ctx, record_var = ctx_add_var decl.span "x" (VarId.of_int 0) ctx in
(* Field_var will be the variable in the constructor that is returned by the projector *)
- let ctx, field_var = ctx_add_var decl.meta "x" (VarId.of_int 1) ctx in
+ let ctx, field_var = ctx_add_var decl.span "x" (VarId.of_int 1) ctx in
(* Name of the ADT *)
- let def_name = ctx_get_local_type decl.meta decl.def_id ctx in
+ let def_name = ctx_get_local_type decl.span decl.def_id ctx in
(* Name of the ADT constructor. As we are in the struct case, we only have
one constructor *)
- let cons_name = ctx_get_struct decl.meta (TAdtId decl.def_id) ctx in
+ let cons_name = ctx_get_struct decl.span (TAdtId decl.def_id) ctx in
let extract_field_proj (field_id : FieldId.id) (_ : field) : unit =
F.pp_print_space fmt ();
@@ -1703,33 +1703,40 @@ let extract_type_decl_lean_record_field_projectors (ctx : extraction_ctx)
(* Inner box for the projector definition *)
F.pp_open_hvbox fmt ctx.indent_incr;
- (* Box for the attributes *)
- F.pp_open_vbox fmt 0;
- (* Annotate the projectors with both simp and reducible.
- The first one allows to automatically unfold when calling simp in proofs.
- The second ensures that projectors will interact well with the unifier *)
- F.pp_print_string fmt "@[simp, reducible]";
- F.pp_print_break fmt 0 0;
- (* Close box for the attributes *)
- F.pp_close_box fmt ();
+ (* For Lean: add some attributes *)
+ if !backend = Lean then (
+ (* Box for the attributes *)
+ F.pp_open_vbox fmt 0;
+ (* Annotate the projectors with both simp and reducible.
+ The first one allows to automatically unfold when calling simp in proofs.
+ The second ensures that projectors will interact well with the unifier *)
+ F.pp_print_string fmt "@[simp, reducible]";
+ F.pp_print_break fmt 0 0;
+ (* Close box for the attributes *)
+ F.pp_close_box fmt ());
(* Box for the [def ADT.proj ... :=] *)
F.pp_open_hovbox fmt ctx.indent_incr;
- F.pp_print_string fmt "def";
+ (match !backend with
+ | Lean -> F.pp_print_string fmt "def"
+ | Coq -> F.pp_print_string fmt "Definition"
+ | _ -> internal_error __FILE__ __LINE__ decl.span);
F.pp_print_space fmt ();
(* Print the function name. In Lean, the syntax ADT.proj will
- allow us to call x.proj for any x of type ADT *)
+ allow us to call x.proj for any x of type ADT. In Coq,
+ we will have to introduce a notation for the projector. *)
let field_name =
- ctx_get_field decl.meta (TAdtId decl.def_id) field_id ctx
+ ctx_get_field decl.span (TAdtId decl.def_id) field_id ctx
in
- F.pp_print_string fmt def_name;
- F.pp_print_string fmt ".";
+ if !backend = Lean then (
+ F.pp_print_string fmt def_name;
+ F.pp_print_string fmt ".");
F.pp_print_string fmt field_name;
(* Print the generics *)
let as_implicits = true in
- extract_generic_params decl.meta ctx fmt TypeDeclId.Set.empty
+ extract_generic_params decl.span ctx fmt TypeDeclId.Set.empty
~as_implicits decl.generics type_params cg_params trait_clauses;
(* Print the record parameter as "(x : ADT)" *)
@@ -1787,115 +1794,11 @@ let extract_type_decl_lean_record_field_projectors (ctx : extraction_ctx)
(* Close the box for the branch *)
F.pp_close_box fmt ();
- (* Close the box for the whole match *)
- F.pp_close_box fmt ();
-
- F.pp_close_box fmt ();
- (* Close the outer box for projector definition *)
- F.pp_close_box fmt ();
- (* Add breaks to insert new lines between definitions *)
- F.pp_print_break fmt 0 0
- in
-
- FieldId.iteri extract_field_proj fields
-
-(** Auxiliary function.
-
- Generate field projectors in Coq.
-
- Sometimes we extract records as inductives in Coq: when this happens we
- have to define the field projectors afterwards.
- *)
-let extract_type_decl_coq_record_field_projectors (ctx : extraction_ctx)
- (fmt : F.formatter) (kind : decl_kind) (decl : type_decl) : unit =
- sanity_check __FILE__ __LINE__ (!backend = Coq) decl.span;
- match decl.kind with
- | Opaque | Enum _ -> ()
- | Struct fields ->
- (* Records are extracted as inductives only if they are recursive *)
- let is_rec = decl_is_from_rec_group kind in
- if is_rec then
- (* Add the type params *)
- let ctx, type_params, cg_params, trait_clauses =
- ctx_add_generic_params decl.span decl.llbc_name decl.llbc_generics
- decl.generics ctx
- in
- let ctx, record_var = ctx_add_var decl.span "x" (VarId.of_int 0) ctx in
- let ctx, field_var = ctx_add_var decl.span "x" (VarId.of_int 1) ctx in
- let def_name = ctx_get_local_type decl.span decl.def_id ctx in
- let cons_name = ctx_get_struct decl.span (TAdtId decl.def_id) ctx in
- let extract_field_proj (field_id : FieldId.id) (_ : field) : unit =
- F.pp_print_space fmt ();
- (* Outer box for the projector definition *)
- F.pp_open_hvbox fmt 0;
- (* Inner box for the projector definition *)
- F.pp_open_hvbox fmt ctx.indent_incr;
- (* Open a box for the [Definition PROJ ... :=] *)
- F.pp_open_hovbox fmt ctx.indent_incr;
- F.pp_print_string fmt "Definition";
- F.pp_print_space fmt ();
- let field_name =
- ctx_get_field decl.span (TAdtId decl.def_id) field_id ctx
- in
- F.pp_print_string fmt field_name;
- (* Print the generics *)
- let as_implicits = true in
- extract_generic_params decl.span ctx fmt TypeDeclId.Set.empty
- ~as_implicits decl.generics type_params cg_params trait_clauses;
- (* Print the record parameter *)
- F.pp_print_space fmt ();
- F.pp_print_string fmt "(";
- F.pp_print_string fmt record_var;
- F.pp_print_space fmt ();
- F.pp_print_string fmt ":";
- F.pp_print_space fmt ();
- F.pp_print_string fmt def_name;
- List.iter
- (fun p ->
- F.pp_print_space fmt ();
- F.pp_print_string fmt p)
- type_params;
- F.pp_print_string fmt ")";
- (* *)
- F.pp_print_space fmt ();
- F.pp_print_string fmt ":=";
- (* Close the box for the [Definition PROJ ... :=] *)
- F.pp_close_box fmt ();
- F.pp_print_space fmt ();
- (* Open a box for the whole match *)
- F.pp_open_hvbox fmt 0;
- (* Open a box for the [match ... with] *)
- F.pp_open_hovbox fmt ctx.indent_incr;
- F.pp_print_string fmt "match";
- F.pp_print_space fmt ();
- F.pp_print_string fmt record_var;
- F.pp_print_space fmt ();
- F.pp_print_string fmt "with";
- (* Close the box for the [match ... with] *)
- F.pp_close_box fmt ();
-
- (* Open a box for the branch *)
- F.pp_open_hovbox fmt ctx.indent_incr;
- (* Print the match branch *)
- F.pp_print_space fmt ();
- F.pp_print_string fmt "|";
- F.pp_print_space fmt ();
- F.pp_print_string fmt cons_name;
- FieldId.iteri
- (fun id _ ->
- F.pp_print_space fmt ();
- if field_id = id then F.pp_print_string fmt field_var
- else F.pp_print_string fmt "_")
- fields;
- F.pp_print_space fmt ();
- F.pp_print_string fmt "=>";
- F.pp_print_space fmt ();
- F.pp_print_string fmt field_var;
- (* Close the box for the branch *)
- F.pp_close_box fmt ();
(* Print the [end] *)
- F.pp_print_space fmt ();
- F.pp_print_string fmt "end";
+ if !backend = Coq then (
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt "end");
+
(* Close the box for the whole match *)
F.pp_close_box fmt ();
(* Close the inner box projector *)
@@ -1904,12 +1807,13 @@ let extract_type_decl_coq_record_field_projectors (ctx : extraction_ctx)
if !backend = Coq then (
F.pp_print_cut fmt ();
F.pp_print_string fmt ".");
- (* Close the outer box projector *)
+ (* Close the outer box for projector definition *)
F.pp_close_box fmt ();
(* Add breaks to insert new lines between definitions *)
F.pp_print_break fmt 0 0
in
+ (* Only for Coq: we need to define a notation for the projector *)
let extract_proj_notation (field_id : FieldId.id) (_ : field) : unit =
F.pp_print_space fmt ();
(* Outer box for the projector definition *)
@@ -1950,7 +1854,7 @@ let extract_type_decl_coq_record_field_projectors (ctx : extraction_ctx)
let extract_field_proj_and_notation (field_id : FieldId.id)
(field : field) : unit =
extract_field_proj field_id field;
- extract_proj_notation field_id field
+ if !backend = Coq then extract_proj_notation field_id field
in
FieldId.iteri extract_field_proj_and_notation fields
@@ -1964,20 +1868,14 @@ let extract_type_decl_extra_info (ctx : extraction_ctx) (fmt : F.formatter)
(kind : decl_kind) (decl : type_decl) : unit =
match !backend with
| FStar | HOL4 -> ()
- | Lean ->
- if
- not
- (TypesUtils.type_decl_from_decl_id_is_tuple_struct
- ctx.trans_ctx.type_ctx.type_infos decl.def_id)
- then extract_type_decl_lean_record_field_projectors ctx fmt kind decl
- | Coq ->
+ | Lean | Coq ->
if
not
(TypesUtils.type_decl_from_decl_id_is_tuple_struct
ctx.trans_ctx.type_ctx.type_infos decl.def_id)
then (
- extract_type_decl_coq_arguments ctx fmt kind decl;
- extract_type_decl_coq_record_field_projectors ctx fmt kind decl)
+ if !backend = Coq then extract_type_decl_coq_arguments ctx fmt kind decl;
+ extract_type_decl_record_field_projectors ctx fmt kind decl)
(** Extract the state type declaration. *)
let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)