use Export.Coq when possible

Author: agontard

main.ml

@@ -1242,14 +1242,17 @@ and command = function
   | "abbrev"::_ -> wrong_nb_args()
 
   (* generate file to check mappings *)
-  | "check-mappings"::b::e::rn::[m](*::rq*) ->
+  | "check-mappings"::b::e::rn::m::rq ->
     Xmapcheck.base := b ;
+    Export.Coq.stt := true ;
+    Export.Coq.use_implicits := false ;
+    Export.Coq.use_notations := true ;
     Export.Coq.set_renaming rn ;
-    Export.Coq.set_encoding e ;
     Export.Coq.set_mapping m ;
-    Xmapcheck.check_that_unused_mappings_is_not_empty()
-    (* Xmapcheck.requiring := String.concat " " rq ;
-    Xmapcheck.generate_check_file() *)
+    Xmapcheck.unused_mappings := !Export.Coq.erase ;
+    Export.Coq.set_encoding e ;
+    Xmapcheck.requiring := String.concat " " rq ;
+    Xmapcheck.generate_check_file()
 
   | "check-mappings"::_ -> wrong_nb_args()
 

xmapcheck.ml

@@ -6,113 +6,13 @@ open Common open Pos open Error
 open Parsing open Syntax
 open Export.Coq
 
-let unused_mappings = ref !erase
-
-let check_that_unused_mappings_is_not_empty() = if StrSet.is_empty !unused_mappings && not (StrSet.is_empty !erase)
-  then print_string "Sadly, unused_mappings is empty."
-  else print_string "unused_mappings is, indeed, non-empty" 
-  
-
-(** Set encoding. *)
-
-let map_qid_builtin = ref QidMap.empty
-
-let set_encoding : string -> unit = fun f ->
-  let found = Array.make nb_builtins false in
-  let consume = function
-    | {elt=P_builtin(n,lp_qid);pos} ->
-        begin match index_of_name n with
-        | Some i ->
-            if Logger.log_enabled() then
-              log "builtin \"%s\" = %a" n Pretty.qident lp_qid;
-            builtin.(i) <- lp_qid.elt;
-            found.(i) <- true;
-            let b = builtin_of_index i in
-            map_qid_builtin := QidMap.add lp_qid.elt b !map_qid_builtin;
-            if b = El || b = Prf then
-              (if Logger.log_enabled() then log "erase %s" (snd lp_qid.elt);
-               erase := StrSet.add (snd lp_qid.elt) !erase)
-        | None -> fatal pos "Unknown builtin."
-        end
-    | {pos;_} -> fatal pos "Invalid command."
-  in
-  Stream.iter consume (Parser.parse_file f);
-  Array.iteri
-    (fun i b ->
-      if not b then
-        let pos =
-          Some {fname=Some f;start_line=0;start_col=0;end_line=0;end_col=0}
-        in fatal pos "Builtin %s undefined." (name_of_index i))
-    found
-
-(** Basic printing functions. We use Printf for efficiency reasons. *)
-let out = Printf.printf
-
-let char = output_char
-let string = output_string
-
-let prefix pre elt oc x = string oc pre; elt oc x
-let suffix elt suf oc x = elt oc x; string oc suf
-
-let list elt sep oc xs =
-  match xs with
-  | [] -> ()
-  | x::xs -> elt oc x; List.iter (prefix sep elt oc) xs
-
-(** Translation of identifiers. *)
-
-let translate_ident : string -> string = fun s ->
-  try StrMap.find s !rmap with Not_found -> s
-
-let raw_ident oc s = string oc (translate_ident s)
-
-let ident oc {elt;_} = raw_ident oc elt
+(* Initialised to Export.Coq.erase in main.ml *)
+let unused_mappings = ref StrSet.empty
 
 let untouched_ident oc ({elt;_} : p_ident) = string oc elt
 
-let param_id oc idopt =
-  match idopt with
-  | Some id -> ident oc id
-  | None    -> char oc '_'
-
-let param_ids = list param_id " "
-
-let raw_path = list string "."
-
-let path oc {elt;_} = raw_path oc elt
-
-let qident oc {elt=(mp,s);_} =
-  match mp with
-  | [] -> raw_ident oc s
-  | _::_ -> raw_path oc mp; char oc '.'; raw_ident oc s
-
-(** Translation of terms. *)
-
-let stt = Stdlib.ref true
-let use_implicits = Stdlib.ref false
-let use_notations = Stdlib.ref true
-
-(* redefinition of p_get_args ignoring P_Wrap's. *)
-let p_get_args : p_term -> p_term * p_term list = fun t ->
-  let rec p_get_args t acc =
-    match t.elt with
-    | P_Appl(t, u) -> p_get_args t (u::acc)
-    | P_Wrap t -> p_get_args t acc
-    | _ -> t, acc
-  in p_get_args t []
-
-let app t default cases =
-  let h, ts = p_get_args t in
-  if !stt then
-    match h.elt with
-    | P_Iden({elt;_},expl) ->
-        begin match QidMap.find_opt elt !map_qid_builtin with
-        | None -> default h ts
-        | Some builtin -> cases h ts expl builtin
-        end
-    | _ -> default h ts
-  else default h ts
-
+(* Export.Coq.term but for each identifier encountered, update unused_mappings.
+   The other difference is that we assume use_notations = true, use_implicits = false*)
 let rec term ?(implicits=true) oc t =
   (*if Logger.log_enabled() then
     log "pp %a" (*Pos.short t.pos*) Pretty.term t;*)
@@ -149,21 +49,17 @@ let rec term ?(implicits=true) oc t =
   | P_Appl _ ->
       let default h ts = paren oc h ~implicits ; char oc ' '; list (paren ~implicits) " " oc ts in
       app t default
-        (fun h ts expl builtin ->
-          match !use_notations, !use_implicits && not expl, builtin, ts with
-          | _, _, (El|Prf), [u] -> term oc u ~implicits
-          | _, _, (Arr|Imp), [u;v] -> arrow oc u v ~implicits
-          | _, _, All, [_;{elt=P_Wrap({elt=P_Abst([_] as xs,u);_});_}]
-          | _, true, All, [{elt=P_Wrap({elt=P_Abst([_] as xs,u);_});_}]
-            -> prod oc xs u ~implicits
-          | _, _, Ex, [_;{elt=P_Wrap({elt=P_Abst([x],u);_});_}]
-          | _, true, Ex, [{elt=P_Wrap({elt=P_Abst([x],u);_});_}] ->
+        (fun h ts _ builtin ->
+          match builtin, ts with
+          | (El|Prf), [u] -> term oc u ~implicits
+          | (Arr|Imp), [u;v] -> arrow oc u v ~implicits
+          | All, [_;{elt=P_Wrap({elt=P_Abst([_] as xs,u);_});_}] -> prod oc xs u ~implicits
+          | Ex, [_;{elt=P_Wrap({elt=P_Abst([x],u);_});_}] ->
               string oc "exists "; raw_params oc x ~implicits; string oc ", "; term oc u ~implicits
-          | true, _, Eq, [_;u;v]
-          | true, true, Eq, [u;v] -> paren oc u ~implicits; string oc " = "; paren oc v ~implicits
-          | true, _, Or, [u;v] -> paren oc u ~implicits; string oc " \\/ "; paren oc v ~implicits
-          | true, _, And, [u;v] ->  paren oc u ~implicits; string oc " /\\ "; paren oc v ~implicits
-          | true, _, Not, [u] -> string oc "~ "; paren oc u ~implicits
+          | Eq, [_;u;v] -> paren oc u ~implicits; string oc " = "; paren oc v ~implicits
+          | Or, [u;v] -> paren oc u ~implicits; string oc " \\/ "; paren oc v ~implicits
+          | And, [u;v] ->  paren oc u ~implicits; string oc " /\\ "; paren oc v ~implicits
+          | Not, [u] -> string oc "~ "; paren oc u ~implicits
           | _ -> default h ts)
 
 and arrow ?(implicits=true) oc u v = paren oc u ~implicits ; string oc " -> "; term oc v ~implicits
@@ -209,11 +105,13 @@ and typopt ?(implicits=true) oc t = Option.iter (prefix " : " (term ~implicits)
 
 let is_lem x = is_opaq x || is_priv x
 
+(* Store the last unmapped object *)
 type unmapped_def_kind =
 | UMLem of string
 | UMDef of string
-
 let last_unmapped = ref (UMLem "")
+
+(* List of unmapped axioms with their type *)
 let axlist : (string*p_term) list ref = ref []
 
 (* Identify types, possibly parametrized *)
@@ -242,12 +140,16 @@ let command oc {elt; pos} =
           else p_sym_arg
       in
       begin match QidMap.find_opt ([],p_sym_nam.elt) !map_erased_qid_coq with
-(* Instead of erasing mapped terms, check their type *)
+      (* Instead of erasing mapped terms, check their type *)
       | Some s ->
         unused_mappings := StrSet.remove p_sym_nam.elt !unused_mappings;
         if List.mem p_sym_nam.elt ignore_mappings
         then ()
         else
+        (* remove implicit arguments, as they cannot be parsed by tactics.
+           types have no implicit arguments in the first place and should not start
+           with an @ (example: (list term) is a valid mapping for a type and won't work
+           with an @ in front) *)
         let s = match p_sym_typ with
           | Some t when not (is_Set t) && not (String.starts_with ~prefix:"@" s) -> "@" ^ s
           | _ -> s
@@ -265,7 +167,10 @@ let command oc {elt; pos} =
       | None -> 
         begin match p_sym_def, p_sym_trm, p_sym_arg, p_sym_typ with
           | true, Some _, _, Some _ when List.exists is_lem p_sym_mod ->
-            (* Do not translate lemmas to avoid nested proofs but still print them. *)
+            (* Do not translate lemmas to avoid nested proofs. *)
+            (* Also, use the last unmapped object to catch definitions mapped without the
+               definitional lemma or the converse *)
+            (* Notice that, for lemmas, the condition s ^ "_def" <> ... is always true. *)
             begin match !last_unmapped with
             | UMLem s | UMDef s when s ^ "_def" <> p_sym_nam.elt ->
               string oc "idtac \"Error: " ; untouched_ident oc p_sym_nam ;
@@ -336,16 +241,18 @@ Ltac conclusion := match goal with
 
 Goal True.\n"
 
+(* the $(BASE) library name *)
 let base = ref ""
 
+(* the $(REQUIRING) files to import *)
 let requiring = ref ""
 
 let lpfile name = !base ^ "_" ^ name ^ ".lp"
 
+(* read all lp files in a list *)
 let chainread oc = List.iter (fun name -> ast oc (Parser.parse_file (lpfile name)))
 
-let outputfile = !base ^ "_checkmappings.v"
-
+(* Error printing for an unmapped axiom *)
 let unmappedaxiom oc (name,typ) = string oc (name ^ " of type ") ; term oc typ 
 
 let generate_check_file_in oc =