Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Adapt to coq/coq#18422 (indirect accessor handled through vernactypes) #121

Merged
merged 1 commit into from
Apr 7, 2024
Merged

Adapt to coq/coq#18422 (indirect accessor handled through vernactypes) #121

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
20 changes: 10 additions & 10 deletions src/abstraction.mlg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ VERNAC COMMAND EXTEND ParametricityDefined CLASSIFIED AS SIDEFF STATE program
}
END

VERNAC COMMAND EXTEND AbstractionReference CLASSIFIED AS SIDEFF
VERNAC COMMAND EXTEND AbstractionReference CLASSIFIED AS SIDEFF STATE opaque_access
| [ "Parametricity" ref(c) ] ->
{
command_reference default_arity (intern_reference_to_name c) None
Expand Down Expand Up @@ -79,7 +79,7 @@ VERNAC COMMAND EXTEND AbstractionReference CLASSIFIED AS SIDEFF
}
END

VERNAC COMMAND EXTEND AbstractionRecursive CLASSIFIED AS SIDEFF
VERNAC COMMAND EXTEND AbstractionRecursive CLASSIFIED AS SIDEFF STATE opaque_access
| [ "Parametricity" "Recursive" reference(c) ] ->
{
command_reference_recursive default_arity (intern_reference_to_name c)
Expand All @@ -98,7 +98,7 @@ VERNAC COMMAND EXTEND AbstractionRecursive CLASSIFIED AS SIDEFF
}
END

VERNAC COMMAND EXTEND Abstraction CLASSIFIED AS SIDEFF
VERNAC COMMAND EXTEND Abstraction CLASSIFIED AS SIDEFF STATE opaque_access
| [ "Parametricity" "Translation" constr(c) "as" ident(name)] ->
{
translate_command default_arity c name
Expand All @@ -113,30 +113,30 @@ VERNAC COMMAND EXTEND Abstraction CLASSIFIED AS SIDEFF
}
END

VERNAC COMMAND EXTEND TranslateModule CLASSIFIED AS SIDEFF
VERNAC COMMAND EXTEND TranslateModule CLASSIFIED AS SIDEFF STATE opaque_access
| [ "Parametricity" "Module" global(qid) ] ->
{
ignore (translate_module_command Parametricity.default_arity qid)
translate_module_command Parametricity.default_arity qid
}
| [ "Parametricity" "Module" global(qid) "as" ident(name) ] ->
{
ignore (translate_module_command ~name Parametricity.default_arity qid)
translate_module_command ~name Parametricity.default_arity qid
}
| [ "Parametricity" "Module" global(qid) "arity" integer(arity) ] ->
{
ignore (translate_module_command arity qid)
translate_module_command arity qid
}
| [ "Parametricity" "Module" global(qid) "as" ident(name) "arity" integer(arity) ] ->
{
ignore (translate_module_command ~name arity qid)
translate_module_command ~name arity qid
}
| [ "Parametricity" "Module" global(qid) "arity" integer(arity) "as" ident(name)] ->
{
ignore (translate_module_command ~name arity qid)
translate_module_command ~name arity qid
}
END

VERNAC COMMAND EXTEND Realizer CLASSIFIED AS SIDEFF
VERNAC COMMAND EXTEND Realizer CLASSIFIED AS SIDEFF STATE opaque_access
| [ "Realizer" constr(c) "as" ident(name) ":=" constr(t) ] ->
{
realizer_command Parametricity.default_arity (Some name) c t
Expand Down
61 changes: 33 additions & 28 deletions src/declare_translation.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -70,18 +70,19 @@ let add_definition ~opaque ~hook ~poly ~scope ~kind ~tactic name env evd term ty
Some lemma
end

let declare_abstraction ?(opaque = false) ?(continuation = default_continuation) ~poly ~scope ~kind arity evdr env a name =
let declare_abstraction ~opaque_access ?(opaque = false) ?(continuation = default_continuation) ~poly ~scope ~kind arity evdr env a name =
Debug.debug_evar_map Debug.all "declare_abstraction, evd = " env !evdr;
debug [`Abstraction] "declare_abstraction, a =" env !evdr a;
let b = Retyping.get_type_of env !evdr a in
debug [`Abstraction] "declare_abstraction, b =" env !evdr b;
let b = Retyping.get_type_of env !evdr a in
let b_R = relation arity evdr env b in
let module P = WithOpaqueAccess(struct let access = opaque_access end) in
let b_R = P.relation arity evdr env b in
let sub = range (fun k -> prime !evdr arity k a) arity in
let b_R = EConstr.Vars.substl sub b_R in
let a_R = fun evd ->
let evdr = ref evd in
let a_R = translate arity evdr env a in
let a_R = P.translate arity evdr env a in
debug [`Abstraction] "a_R = " env !evdr a_R;
debug_evar_map Debug.all "abstraction, evar_map = " env !evdr;
!evdr, a_R
Expand All @@ -104,10 +105,11 @@ let declare_abstraction ?(opaque = false) ?(continuation = default_continuation)
let tactic = Relations.get_parametricity_tactic () in
add_definition ~tactic ~opaque ~poly ~scope ~kind ~hook name env evd a_R b_R

let declare_inductive name ?(continuation = default_continuation) arity evd env (((mut_ind, _) as ind, inst)) =
let declare_inductive ~opaque_access name ?(continuation = default_continuation) arity evd env (((mut_ind, _) as ind, inst)) =
let mut_body, _ = Inductive.lookup_mind_specif env ind in
debug_string [`Inductive] "Translating mind body ...";
let translation_entry = Parametricity.translate_mind_body name arity evd env mut_ind mut_body inst in
let module P = Parametricity.WithOpaqueAccess(struct let access = opaque_access end) in
let translation_entry = P.translate_mind_body name arity evd env mut_ind mut_body inst in
debug_string [`Inductive] ("Translating mind body ... done.");
debug_evar_map [`Inductive] "evar_map inductive " env !evd;
let size = Declarations.(Array.length mut_body.mind_packets) in
Expand Down Expand Up @@ -135,14 +137,15 @@ let translate_inductive_command arity c name =
let evd = ref sigma in
declare_inductive name arity evd env pind

let declare_realizer ?(continuation = default_continuation) ?kind ?real arity evd env name (var : constr) =
let declare_realizer ~opaque_access ?(continuation = default_continuation) ?kind ?real arity evd env name (var : constr) =
let gref = (match EConstr.kind !evd var with
| Var id -> Names.GlobRef.VarRef id
| Const (cst, _) -> Names.GlobRef.ConstRef cst
| _ -> error (Pp.str "Realizer works only for variables and constants.")) in
let evd', typ = Typing.type_of env !evd var in
evd := evd';
let typ_R = Parametricity.relation arity evd env typ in
let module P = Parametricity.WithOpaqueAccess(struct let access = opaque_access end) in
let typ_R = P.relation arity evd env typ in
let sub = range (fun _ -> var) arity in
let typ_R = Vars.substl sub typ_R in
let cpt = ref 0 in
Expand Down Expand Up @@ -182,24 +185,24 @@ let declare_realizer ?(continuation = default_continuation) ?kind ?real arity ev
let tactic = Relations.get_parametricity_tactic () in
add_definition ~tactic ~opaque:false ~poly ~scope ~kind ~hook name env sigma real typ_R

let realizer_command arity name var real =
let realizer_command ~opaque_access arity name var real =
let env = Global.env () in
let sigma = Evd.from_env env in
let (sigma, var) = Constrintern.interp_open_constr env sigma var in
RetrieveObl.check_evars env sigma;
let real = fun sigma -> Constrintern.interp_open_constr env sigma real in
ignore(declare_realizer arity (ref sigma) env name var ~real)
ignore(declare_realizer ~opaque_access arity (ref sigma) env name var ~real)

let rec list_continuation final f l _ = match l with [] -> final ()
| hd::tl -> f (list_continuation final f tl) hd

let rec translate_module_command ?name arity r =
let rec translate_module_command ~opaque_access ?name arity r =
check_nothing_ongoing ();
let qid = r in
let mb = try Global.lookup_module (Nametab.locate_module qid)
with Not_found -> error Pp.(str "Unknown Module " ++ pr_qualid qid)
in
declare_module ?name arity mb
declare_module ~opaque_access ?name arity mb

and id_of_module_path mp =
let open Names in
Expand All @@ -209,7 +212,7 @@ and id_of_module_path mp =
| MPfile dp -> List.hd (DirPath.repr dp)
| MPbound id -> MBId.to_id id

and declare_module ?(continuation = ignore) ?name arity mb =
and declare_module ~opaque_access ?(continuation = ignore) ?name arity mb =
debug_string [`Module] "--> declare_module";
let open Declarations in
let mp = mb.mod_mp in
Expand Down Expand Up @@ -242,7 +245,7 @@ and declare_module ?(continuation = ignore) ?name arity mb =
Evd.(with_sort_context_set univ_rigid evd (UnivGen.fresh_constant_instance env cst))
in
let evdr = ref evd in
ignore(declare_realizer ~continuation arity evdr env None (mkConstU (fst ucst, EInstance.make (snd ucst))))
ignore(declare_realizer ~opaque_access ~continuation arity evdr env None (mkConstU (fst ucst, EInstance.make (snd ucst))))

| (lab, SFBconst cb) ->
let opaque =
Expand Down Expand Up @@ -270,7 +273,7 @@ and declare_module ?(continuation = ignore) ?name arity mb =
debug [`Module] "type :" env !evdr typ
with e -> error (Pp.str (Printexc.to_string e)));
debug_string [`Module] (Printf.sprintf "constant field: '%s'." (Names.Label.to_string lab));
ignore(declare_abstraction ~opaque ~continuation ~poly ~scope ~kind arity evdr env c lab_R)
ignore(declare_abstraction ~opaque_access ~opaque ~continuation ~poly ~scope ~kind arity evdr env c lab_R)

| (lab, SFBmind _) ->
let env = Global.env () in
Expand All @@ -292,14 +295,14 @@ and declare_module ?(continuation = ignore) ?name arity mb =
@@ Names.MutInd.label
@@ mut_ind
in
declare_inductive ind_name ~continuation arity evdr env pind
declare_inductive ~opaque_access ind_name ~continuation arity evdr env pind
end
| (lab, SFBmodule mb') when
match mb'.mod_type with NoFunctor _ ->
(match mb'.mod_expr with FullStruct | Algebraic _ -> true | _ -> false)
| _ -> false
->
declare_module ~continuation arity mb'
declare_module ~opaque_access ~continuation arity mb'

| (lab, _) ->
Pp.(Flags.if_verbose msg_info (str (Printf.sprintf "Ignoring field '%s'." (Names.Label.to_string lab))));
Expand Down Expand Up @@ -332,7 +335,7 @@ let translateFullName ~fullname arity (kername : Names.KerName.t) : string =
(String.concat "_o_" (plstr@[nstr]))
else nstr

let command_constant ?(continuation = default_continuation) ~fullname arity constant names =
let command_constant ~opaque_access ?(continuation = default_continuation) ~fullname arity constant names =
let env = Global.env () in
let evd = Evd.from_env env in
let poly, opaque =
Expand All @@ -354,9 +357,10 @@ let command_constant ?(continuation = default_continuation) ~fullname arity cons
Evd.(with_sort_context_set univ_rigid evd (UnivGen.fresh_constant_instance env constant))
in
let constr = mkConstU (fst pconst, EInstance.make @@ snd pconst) in
declare_abstraction ~continuation ~opaque ~poly ~scope ~kind arity (ref evd) env constr name
declare_abstraction ~opaque_access ~continuation ~opaque ~poly ~scope ~kind
arity (ref evd) env constr name

let command_inductive ?(continuation = default_continuation) ~fullname arity inductive names =
let command_inductive ~opaque_access ?(continuation = default_continuation) ~fullname arity inductive names =
let env = Global.env () in
let evd = Evd.from_env env in
let evd, pind =
Expand All @@ -372,36 +376,37 @@ let command_inductive ?(continuation = default_continuation) ~fullname arity ind
@@ pind
| Some name -> name
in
declare_inductive name ~continuation arity (ref evd) env pind
declare_inductive ~opaque_access 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) ?(fullname = false) arity gref names =
let command_reference ~opaque_access ?(continuation = default_continuation) ?(fullname = false)
arity gref names =
check_nothing_ongoing ();
let open Names.GlobRef in
(* We ignore proofs for now *)
let _pstate = match gref with
| VarRef variable ->
command_variable ~continuation arity variable names
| ConstRef constant ->
command_constant ~continuation ~fullname arity constant names
command_constant ~opaque_access ~continuation ~fullname arity constant names
| IndRef inductive ->
command_inductive ~continuation ~fullname arity inductive names;
command_inductive ~opaque_access ~continuation ~fullname arity inductive names;
None
| ConstructRef constructor ->
command_constructor ~continuation arity gref names
in ()

let command_reference_recursive ?(continuation = default_continuation) ?(fullname = false) arity gref =
let command_reference_recursive ~opaque_access ?(continuation = default_continuation) ?(fullname = false) arity gref =
let gref= Globnames.canonical_gr gref in
let label = Names.Label.of_id (Nametab.basename_of_global gref) in
(* Assumptions doesn't care about the universes *)
let c, _ = UnivGen.fresh_global_instance (Global.env()) gref in
let (direct, graph, _) = Assumptions.traverse label c in
let (direct, graph, _) = Assumptions.traverse opaque_access label c in
let inductive_of_constructor ref =
let open Globnames in
let ref= Globnames.canonical_gr ref in
Expand All @@ -428,9 +433,9 @@ let command_reference_recursive ?(continuation = default_continuation) ?(fullnam
(* Pp.(msg_info (str "DepRefs:"));
* List.iter (fun x -> msg_info (Printer.pr_global x)) dep_refs; *)
list_continuation continuation (fun continuation gref ->
command_reference ~continuation ~fullname arity gref None) dep_refs ()
command_reference ~opaque_access ~continuation ~fullname arity gref None) dep_refs ()

let translate_command arity c name =
let translate_command ~opaque_access arity c name =
if !ongoing_translation then error (Pp.str "On going translation.");
(* Same comment as above *)
let env = Global.env () in
Expand All @@ -450,5 +455,5 @@ let translate_command arity c name =
in
let scope = Locality.(Global ImportDefaultBehavior) in
let kind = Decls.(IsDefinition Definition) in
let _ : Declare.Proof.t option = declare_abstraction ~opaque ~poly ~scope ~kind arity (ref evd) env c name in
let _ : Declare.Proof.t option = declare_abstraction ~opaque_access ~opaque ~poly ~scope ~kind arity (ref evd) env c name in
()
6 changes: 5 additions & 1 deletion src/parametricity.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -281,6 +281,9 @@ let lamn n env b =
(* compose_lam [xn:Tn;..;x1:T1] b = [x1:T1]..[xn:Tn]b *)
let compose_lam l b = lamn (List.length l) l b

(* use a functor to avoid having to thread this everywhere *)
module WithOpaqueAccess (Access:sig val access : Global.indirect_accessor end) = struct

(* G |- t ---> |G|, x1, x2 |- [x1,x2] in |t| *)
let rec relation order evd env (t : constr) : constr =
debug_string [`Relation] (Printf.sprintf "relation %d evd env t" order);
Expand Down Expand Up @@ -469,7 +472,7 @@ and translate_constant order (evd : Evd.evar_map ref) env cst : constr =
(* let evd' = Evd.add_constraints !evd cte_constraints in *)
(* evd := evd'; *)
let fold = mkConstU cst in
let (def, _) = Global.force_proof Library.indirect_accessor op in
let (def, _) = Global.force_proof Access.access op in
let def = CVars.subst_instance_constr names def in
let etyp = of_constr typ in
let edef = of_constr def in
Expand Down Expand Up @@ -1224,3 +1227,4 @@ and translate_mind_inductive name order evdr env ikn mut_entry inst (env_params,
List.map (to_constr !evdr) result
end
}
end
Loading