Factor out the code for Lean and Coq

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)