Skip to content

Commit c20c098

Browse files
ppedrotppedrot
authored
Merge pull request #1224 from mattam82/sort-poly-flags
Adapt to rocq-prover/rocq#21419
2 parents ca1aff9 + 5b4910b commit c20c098

File tree

5 files changed

+23
-21
lines changed

5 files changed

+23
-21
lines changed

‎template-rocq/gen-src/specFloat.ml.orig‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -63,15 +63,15 @@ type location =
6363

6464
(** val location_rect : 'a1 -> (comparison -> 'a1) -> location -> 'a1 **)
6565

66-
let location_rect f f0 = function
67-
| Coq_loc_Exact -> f
68-
| Coq_loc_Inexact c -> f0 c
66+
let location_rect loc_Exact loc_Inexact = function
67+
| Coq_loc_Exact -> loc_Exact
68+
| Coq_loc_Inexact c -> loc_Inexact c
6969

7070
(** val location_rec : 'a1 -> (comparison -> 'a1) -> location -> 'a1 **)
7171

72-
let location_rec f f0 = function
73-
| Coq_loc_Exact -> f
74-
| Coq_loc_Inexact c -> f0 c
72+
let location_rec loc_Exact loc_Inexact = function
73+
| Coq_loc_Exact -> loc_Exact
74+
| Coq_loc_Inexact c -> loc_Inexact c
7575

7676
type shr_record = { shr_m : coq_Z; shr_r : bool; shr_s : bool }
7777

‎template-rocq/src/g_template_rocq.mlg‎

Lines changed: 10 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -58,12 +58,14 @@ let fresh_env () =
5858
env, sigma
5959

6060
let to_constr_evars sigma c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c
61+
62+
let poly_ind = poly PolyFlags.Inductive
6163
}
6264

6365
(** ********* Commands ********* *)
6466

6567
VERNAC COMMAND EXTEND TemplateRocq_Test_Quote CLASSIFIED AS QUERY STATE program
66-
| #[ poly = polymorphic ] [ "MetaRocq" "Test" "Quote" constr(def) ] ->
68+
| #[ poly = poly_def ] [ "MetaRocq" "Test" "Quote" constr(def) ] ->
6769
{ fun ~pm -> let (env, evm) = fresh_env () in
6870
let (evm, def) = Constrintern.interp_open_constr env evm def in
6971
let (evm, pgm) = EConstr.fresh_global env evm (Lazy.force Template_monad.ptmTestQuote) in
@@ -73,7 +75,7 @@ VERNAC COMMAND EXTEND TemplateRocq_Test_Quote CLASSIFIED AS QUERY STATE program
7375
END
7476

7577
VERNAC COMMAND EXTEND TemplateRocq_Quote_Definition CLASSIFIED AS SIDEFF STATE program
76-
| #[ poly = polymorphic ] [ "MetaRocq" "Quote" "Definition" ident(name) ":=" constr(def) ] ->
78+
| #[ poly = poly_def ] [ "MetaRocq" "Quote" "Definition" ident(name) ":=" constr(def) ] ->
7779
{ fun ~pm -> let (env, evm) = fresh_env () in
7880
let (evm, def) = Constrintern.interp_open_constr env evm def in
7981
let (evm, pgm) = EConstr.fresh_global env evm (Lazy.force Template_monad.ptmQuoteDefinition) in
@@ -83,7 +85,7 @@ VERNAC COMMAND EXTEND TemplateRocq_Quote_Definition CLASSIFIED AS SIDEFF STATE p
8385
END
8486

8587
VERNAC COMMAND EXTEND TemplateRocq_Quote_Definition_Eval CLASSIFIED AS SIDEFF STATE program
86-
| #[ poly = polymorphic ] [ "MetaRocq" "Quote" "Definition" ident(name) ":=" "Eval" red_expr(rd) "in" constr(def) ] ->
88+
| #[ poly = poly_def ] [ "MetaRocq" "Quote" "Definition" ident(name) ":=" "Eval" red_expr(rd) "in" constr(def) ] ->
8789
{ fun ~pm -> let (env, evm) = fresh_env () in
8890
let (evm, def) = Constrintern.interp_open_constr env evm def in
8991
(* TODO : implem quoting of tactic reductions so that we can use ptmQuoteDefinitionRed *)
@@ -95,7 +97,7 @@ VERNAC COMMAND EXTEND TemplateRocq_Quote_Definition_Eval CLASSIFIED AS SIDEFF ST
9597
END
9698

9799
VERNAC COMMAND EXTEND TemplateRocq_Quote_Recursively_Definition CLASSIFIED AS SIDEFF STATE program
98-
| #[ poly = polymorphic ] [ "MetaRocq" "Quote" "Recursively" "Definition" ident(name) ":=" constr(def) ] ->
100+
| #[ poly = poly_def ] [ "MetaRocq" "Quote" "Recursively" "Definition" ident(name) ":=" constr(def) ] ->
99101
{ fun ~pm -> let (env, evm) = fresh_env () in
100102
let (evm, def) = Constrintern.interp_open_constr env evm def in
101103
let (evm, pgm) = EConstr.fresh_global env evm (Lazy.force Template_monad.ptmQuoteRecDefinition) in
@@ -105,7 +107,7 @@ VERNAC COMMAND EXTEND TemplateRocq_Quote_Recursively_Definition CLASSIFIED AS SI
105107
END
106108

107109
VERNAC COMMAND EXTEND TemplateRocq_Test_Unquote CLASSIFIED AS QUERY STATE program
108-
| #[ poly = polymorphic ] [ "MetaRocq" "Test" "Unquote" constr(def) ] ->
110+
| #[ poly = poly_def ] [ "MetaRocq" "Test" "Unquote" constr(def) ] ->
109111
{ fun ~pm -> let (env, evm) = fresh_env () in
110112
let (evm, def) = Constrintern.interp_open_constr env evm def in
111113
let (evm, pgm) = EConstr.fresh_global env evm (Lazy.force Template_monad.ptmTestUnquote) in
@@ -115,7 +117,7 @@ VERNAC COMMAND EXTEND TemplateRocq_Test_Unquote CLASSIFIED AS QUERY STATE progra
115117
END
116118

117119
VERNAC COMMAND EXTEND TemplateRocq_Make_Definition CLASSIFIED AS SIDEFF STATE program
118-
| #[ poly = polymorphic ] [ "MetaRocq" "Unquote" "Definition" ident(name) ":=" constr(def) ] ->
120+
| #[ poly = poly_def ] [ "MetaRocq" "Unquote" "Definition" ident(name) ":=" constr(def) ] ->
119121
{ fun ~pm -> let (env, evm) = fresh_env () in
120122
let (evm, def) = Constrintern.interp_open_constr env evm def in
121123
let (evm, pgm) = EConstr.fresh_global env evm (Lazy.force Template_monad.ptmMkDefinition) in
@@ -126,7 +128,7 @@ VERNAC COMMAND EXTEND TemplateRocq_Make_Definition CLASSIFIED AS SIDEFF STATE pr
126128
END
127129

128130
VERNAC COMMAND EXTEND TemplateRocq_Make_Inductive CLASSIFIED AS SIDEFF STATE program
129-
| #[ poly = polymorphic ] [ "MetaRocq" "Unquote" "Inductive" constr(def) ] ->
131+
| #[ poly = poly_ind ] [ "MetaRocq" "Unquote" "Inductive" constr(def) ] ->
130132
{ fun ~pm -> let (env, evm) = fresh_env () in
131133
let (evm, def) = Constrintern.interp_open_constr env evm def in
132134
let (evm, pgm) = EConstr.fresh_global env evm (Lazy.force Template_monad.ptmMkInductive) in
@@ -136,7 +138,7 @@ VERNAC COMMAND EXTEND TemplateRocq_Make_Inductive CLASSIFIED AS SIDEFF STATE pro
136138
END
137139

138140
VERNAC COMMAND EXTEND TemplateRocq_Run_Template_Program CLASSIFIED AS SIDEFF STATE program
139-
| #[ poly = polymorphic ] [ "MetaRocq" "Run" constr(def) ] ->
141+
| #[ poly = poly_def ] [ "MetaRocq" "Run" constr(def) ] ->
140142
{ fun ~pm -> let (env, evm) = fresh_env () in
141143
let (pgm, ctx) = Constrintern.interp_constr env evm def in
142144
let evm = Evd.from_ctx ctx in

‎template-rocq/src/plugin_core.ml‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -84,7 +84,7 @@ let tmEval (rd : reduction_strategy) (t : term) : term tm =
8484
let evd,t' = reduce env evd rd t in
8585
k ~st env evd t'
8686

87-
let tmDefinition (nm : ident) ?poly:(poly=false) ?opaque:(opaque=false) (typ : term option) (body : term) : kername tm =
87+
let tmDefinition (nm : ident) ?(poly=PolyFlags.default) ?opaque:(opaque=false) (typ : term option) (body : term) : kername tm =
8888
fun ~st env evm success _fail ->
8989
let cinfo = Declare.CInfo.make ~name:nm ~typ:(Option.map EConstr.of_constr typ) () in
9090
let info = Declare.Info.make ~poly ~kind:(Decls.(IsDefinition Definition)) () in
@@ -93,7 +93,7 @@ let tmDefinition (nm : ident) ?poly:(poly=false) ?opaque:(opaque=false) (typ : t
9393
let evm = Evd.from_env env in
9494
success ~st env evm (Names.Constant.canonical (Globnames.destConstRef n))
9595

96-
let tmAxiom (nm : ident) ?poly:(poly=false) (typ : term) : kername tm =
96+
let tmAxiom (nm : ident) ?(poly=PolyFlags.default) (typ : term) : kername tm =
9797
fun ~st env evm success _fail ->
9898
let univs = Evd.univ_entry ~poly evm in
9999
let param =
@@ -108,7 +108,7 @@ let tmAxiom (nm : ident) ?poly:(poly=false) (typ : term) : kername tm =
108108
success ~st (Global.env ()) evm (Names.Constant.canonical n)
109109

110110
(* this generates a lemma leaving a hole *)
111-
let tmLemma (nm : ident) ?poly:(poly=false)(ty : term) : kername tm =
111+
let tmLemma (nm : ident) ?(poly=PolyFlags.default) (ty : term) : kername tm =
112112
fun ~st env evm success _fail ->
113113
let kind = Decls.(IsDefinition Definition) in
114114
let hole = CAst.make (Constrexpr.CHole (Some Evar_kinds.(GQuestionMark default_question_mark))) in

‎template-rocq/src/plugin_core.mli‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -47,9 +47,9 @@ val tmFailString : string -> 'a tm
4747
val reduce : Environ.env -> Evd.evar_map -> reduction_strategy -> term -> Evd.evar_map * term
4848
val tmEval : reduction_strategy -> term -> term tm
4949

50-
val tmDefinition : ident -> ?poly:bool -> ?opaque:bool -> term option -> term -> kername tm
51-
val tmAxiom : ident -> ?poly:bool -> term -> kername tm
52-
val tmLemma : ident -> ?poly:bool -> term -> kername tm
50+
val tmDefinition : ident -> ?poly:PolyFlags.t -> ?opaque:bool -> term option -> term -> kername tm
51+
val tmAxiom : ident -> ?poly:PolyFlags.t -> term -> kername tm
52+
val tmLemma : ident -> ?poly:PolyFlags.t -> term -> kername tm
5353

5454
val tmFreshName : ident -> ident tm
5555

‎template-rocq/src/run_template_monad.mli‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
val declare_inductive : Environ.env -> Evd.evar_map -> bool -> Constr.t -> Evd.evar_map
22

33
val run_template_program_rec :
4-
poly:bool ->
4+
poly:PolyFlags.t ->
55
?intactic:bool ->
66
Constr.t Plugin_core.cont ->
77
st:Plugin_core.coq_state ->

0 commit comments

Comments
 (0)