From b40cff25ea731fd6b325135ad2929cc09f10d6bb Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Tue, 7 Nov 2017 14:13:50 +0100 Subject: [PATCH 1/3] Make the new behavior of command_constant (w.r.t. "full name") optional. By default, the Parametricity vernacular does not "qualify" the generated constant so this restore backward-compatibility. Bind the new behavior to the "qualified" version of the vernacular. --- src/abstraction.ml4 | 8 ++++++++ src/declare_translation.ml | 14 ++++++++------ 2 files changed, 16 insertions(+), 6 deletions(-) diff --git a/src/abstraction.ml4 b/src/abstraction.ml4 index aafee51..7af3420 100644 --- a/src/abstraction.ml4 +++ b/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) diff --git a/src/declare_translation.ml b/src/declare_translation.ml index 3f98cbd..68c33d8 100644 --- a/src/declare_translation.ml +++ b/src/declare_translation.ml @@ -309,7 +309,7 @@ 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 (constant : Names.constant) : string = let nstr = (translate_string arity @@ Names.Label.to_string @@ -321,10 +321,12 @@ let translateFullName arity (constant : Names.constant) : string = @@ Names.canonical_con @@ constant) 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 +337,7 @@ 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 constant) | Some name -> name in let kind = Decl_kinds.(Global, poly, DefinitionBody Definition) in @@ -371,14 +373,14 @@ let command_constructor ?(continuation = default_continuation) arity gref names ++ (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 | ConstructRef constructor -> From a546bfaf5506d73f7cf1b41ca15870981dd1eb8a Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Tue, 7 Nov 2017 17:08:46 +0100 Subject: [PATCH 2/3] Add support for "qualified" mode in command_reference_recursive (suggested by @aa755) --- src/abstraction.ml4 | 8 ++++++++ src/declare_translation.ml | 4 ++-- 2 files changed, 10 insertions(+), 2 deletions(-) diff --git a/src/abstraction.ml4 b/src/abstraction.ml4 index 7af3420..95a0551 100644 --- a/src/abstraction.ml4 +++ b/src/abstraction.ml4 @@ -88,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 diff --git a/src/declare_translation.ml b/src/declare_translation.ml index 68c33d8..6f4d5cc 100644 --- a/src/declare_translation.ml +++ b/src/declare_translation.ml @@ -386,7 +386,7 @@ let command_reference ?(continuation = default_continuation) ?(fullname = false) | 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 @@ -416,7 +416,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."); From dee19395faef038f7ba6ec04710f4bd5eb0ef8bf Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Tue, 7 Nov 2017 18:11:17 +0100 Subject: [PATCH 3/3] Add argument "fullname" in function "command_inductive". The function "translateFullName" now takes a "KerName.t" argument. --- src/declare_translation.ml | 25 ++++++++++++------------- 1 file changed, 12 insertions(+), 13 deletions(-) diff --git a/src/declare_translation.ml b/src/declare_translation.ml index 6f4d5cc..48f7e87 100644 --- a/src/declare_translation.ml +++ b/src/declare_translation.ml @@ -309,23 +309,21 @@ 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 ~fullname 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 if fullname then (String.concat "_o_" (plstr@[nstr])) else nstr - let command_constant ?(continuation = default_continuation) ~fullname arity constant names = let poly, opaque = let cb = Global.lookup_constant constant in @@ -337,7 +335,10 @@ let command_constant ?(continuation = default_continuation) ~fullname arity cons (match cb.const_body with Def _ -> false | _ -> true) in let name = match names with - | None -> Names.id_of_string (translateFullName ~fullname 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 @@ -348,7 +349,7 @@ let command_constant ?(continuation = default_continuation) ~fullname arity cons 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)) @@ -356,9 +357,8 @@ let command_inductive ?(continuation = default_continuation) arity inductive nam 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 @@ -366,7 +366,6 @@ let command_inductive ?(continuation = default_continuation) arity inductive nam 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 "'") @@ -382,7 +381,7 @@ let command_reference ?(continuation = default_continuation) ?(fullname = false) | ConstRef constant -> 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