Merge pull request rocq-community#3 from erikmd/make-fullname-optional

Add a "qualified" version for commands Parametricity & Parametricity Recursive.

Author: aa755

src/abstraction.ml4

@@ -57,6 +57,10 @@ VERNAC COMMAND EXTEND AbstractionReference CLASSIFIED AS SIDEFF
   [
     command_reference default_arity (Constrintern.intern_reference c) (Some name)
   ]
+| [ "Parametricity" reference(c) "qualified" ] -> 
+  [
+    command_reference ~fullname:true default_arity (Constrintern.intern_reference c) None
+  ]
 | [ "Parametricity" reference(c) "arity" int(arity) ] -> 
   [
     command_reference arity (Constrintern.intern_reference c) None  
@@ -65,6 +69,10 @@ VERNAC COMMAND EXTEND AbstractionReference CLASSIFIED AS SIDEFF
   [
     command_reference arity (Constrintern.intern_reference c) (Some name)  
   ]
+| [ "Parametricity" reference(c) "arity" int(arity) "qualified" ] ->
+  [
+    command_reference ~fullname:true arity (Constrintern.intern_reference c) None
+  ]
 | [ "Parametricity" reference(c)  "as" ident(name) "arity" integer(arity) ] -> 
   [
     command_reference arity (Constrintern.intern_reference c) (Some name)  
@@ -80,6 +88,14 @@ VERNAC COMMAND EXTEND AbstractionRecursive CLASSIFIED AS SIDEFF
   [
     command_reference_recursive arity (Constrintern.intern_reference c)
   ]
+| [ "Parametricity" "Recursive" reference(c) "qualified" ] ->
+  [
+    command_reference_recursive ~fullname:true default_arity (Constrintern.intern_reference c)
+  ]
+| [ "Parametricity" "Recursive" reference(c) "arity" integer(arity) "qualified" ] ->
+  [
+    command_reference_recursive ~fullname:true arity (Constrintern.intern_reference c)
+  ]
 END
 
 VERNAC COMMAND EXTEND Abstraction CLASSIFIED AS SIDEFF

src/declare_translation.ml

@@ -309,22 +309,22 @@ and declare_module ?(continuation = ignore) ?name arity mb  =
 let command_variable ?(continuation = default_continuation) arity variable names =
   error (Pp.str "Cannot translate an axiom nor a variable. Please use the 'Parametricity Realizer' command.")
 
-let translateFullName arity (constant : Names.constant) : string =
+let translateFullName ~fullname arity (kername : Names.KerName.t) : string =
   let nstr =
     (translate_string arity
      @@ Names.Label.to_string
-     @@ Names.Constant.label
-     @@ constant)in 
+     @@ Names.KerName.label
+     @@ kername) in 
   let pstr =
     (Names.ModPath.to_string
      @@ Names.modpath
-     @@ Names.canonical_con
-     @@ constant) in
+     @@ kername) in
   let plstr = Str.split (Str.regexp ("\.")) pstr in
-  (String.concat "_o_" (plstr@[nstr]))
+  if fullname then
+    (String.concat "_o_" (plstr@[nstr]))
+  else nstr
 
-
-let command_constant ?(continuation = default_continuation) arity constant names =
+let command_constant ?(continuation = default_continuation) ~fullname arity constant names =
   let poly, opaque =
     let cb = Global.lookup_constant constant in
     let open Declarations in
@@ -335,7 +335,10 @@ let command_constant ?(continuation = default_continuation) arity constant names
     (match cb.const_body with Def _ -> false | _ -> true)
   in
   let name = match names with
-      | None -> Names.id_of_string (translateFullName arity constant)
+      | None -> Names.id_of_string
+                @@ translateFullName ~fullname arity
+                @@ Names.Constant.canonical
+                @@ constant
       | Some name -> name
   in
   let kind = Decl_kinds.(Global, poly, DefinitionBody Definition) in
@@ -346,45 +349,43 @@ let command_constant ?(continuation = default_continuation) arity constant names
   let constr = mkConstU (fst pconst, EInstance.make @@ snd pconst) in
   declare_abstraction ~continuation ~opaque ~kind arity (ref evd) env constr name
 
-let command_inductive ?(continuation = default_continuation) arity inductive names =
+let command_inductive ?(continuation = default_continuation) ~fullname arity inductive names =
   let (evd, env) = Lemmas.get_current_context () in
   let evd, pind =
     Evd.(with_context_set univ_rigid evd (Universes.fresh_inductive_instance env inductive))
   in
   let name = match names with
       | None ->
              Names.id_of_string
-          @@ translate_string arity
-          @@ Names.Label.to_string
-          @@ Names.MutInd.label
+          @@ translateFullName ~fullname arity
+          @@ Names.MutInd.canonical
           @@ fst
 	  @@ fst
 	  @@ pind
       | Some name -> name
   in
   declare_inductive name ~continuation arity (ref evd) env pind
 
-
 let command_constructor ?(continuation = default_continuation) arity gref names =
   let open Pp in
   error ((str "'")
         ++ (Printer.pr_global gref)
         ++ (str "' is a constructor. To generate its parametric translation, please translate its inductive first."))
 
-let command_reference ?(continuation = default_continuation) arity gref names =
+let command_reference ?(continuation = default_continuation) ?(fullname = false) arity gref names =
    check_nothing_ongoing ();
    let open Globnames in
    match gref with
    | VarRef variable ->
      command_variable ~continuation arity variable names
    | ConstRef constant ->
-     command_constant ~continuation arity constant names
+     command_constant ~continuation ~fullname arity constant names
    | IndRef inductive ->
-     command_inductive ~continuation arity inductive names
+     command_inductive ~continuation ~fullname arity inductive names
    | ConstructRef constructor ->
      command_constructor ~continuation arity gref names
 
-let command_reference_recursive ?(continuation = default_continuation) arity gref =
+let command_reference_recursive ?(continuation = default_continuation) ?(fullname = false) arity gref =
   let open Globnames in
   let gref= Globnames.canonical_gr gref in
   let label = Names.Label.of_id (Nametab.basename_of_global gref) in
@@ -414,7 +415,7 @@ let command_reference_recursive ?(continuation = default_continuation) arity gre
   (* DEBUG: *)
   let open Pp in msg_info  (str "DepRefs:");
   List.iter (fun x -> let open Pp in msg_info (Printer.pr_global x)) dep_refs;
-  list_continuation continuation (fun continuation gref -> command_reference ~continuation arity gref None) dep_refs ()
+  list_continuation continuation (fun continuation gref -> command_reference ~continuation ~fullname arity gref None) dep_refs ()
 
 let translate_command arity c name =
   if !ongoing_translation then error (Pp.str "On going translation.");