Skip to content

Commit a86a913

Browse files
garesgares
committed
wip
1 parent 7d33e0e commit a86a913

File tree

6 files changed

+108
-85
lines changed

6 files changed

+108
-85
lines changed

‎coq-builtin.elpi‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -957,8 +957,7 @@ typeabbrev univ (ctype "univ").
957957
kind sort type.
958958
type prop sort. % impredicative sort of propositions
959959
type sprop sort. % impredicative sort of propositions with definitional proof irrelevance
960-
type typ univ ->
961-
sort. % predicative sort of data (carries a universe level)
960+
type typ univ -> sort. % predicative sort of data (carries a universe level)
962961

963962
% [coq.sort.leq S1 S2] constrains S1 <= S2
964963
external pred coq.sort.leq o:sort, o:sort.

‎src/coq_elpi_HOAS.ml‎

Lines changed: 73 additions & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -166,45 +166,6 @@ let isuniv, univout, (univ : Univ.Universe.t API.Conversion.t) =
166166
| _ -> univ_to_be_patched.API.Conversion.readback ~depth state t
167167
end
168168
}
169-
170-
let sort =
171-
let open API.AlgebraicData in declare {
172-
ty = API.Conversion.TyName "sort";
173-
doc = "Sorts (kinds of types)";
174-
pp = (fun fmt -> function
175-
| Sorts.Type _ -> Format.fprintf fmt "Type"
176-
| Sorts.Set -> Format.fprintf fmt "Set"
177-
| Sorts.Prop -> Format.fprintf fmt "Prop"
178-
| Sorts.SProp -> Format.fprintf fmt "SProp"
179-
| Sorts.QSort _ -> Format.fprintf fmt "Type");
180-
constructors = [
181-
K("prop","impredicative sort of propositions",N,
182-
B Sorts.prop,
183-
M (fun ~ok ~ko -> function Sorts.Prop -> ok | _ -> ko ()));
184-
K("sprop","impredicative sort of propositions with definitional proof irrelevance",N,
185-
B Sorts.sprop,
186-
M (fun ~ok ~ko -> function Sorts.SProp -> ok | _ -> ko ()));
187-
K("typ","predicative sort of data (carries a universe level)",A(univ,N),
188-
B (fun x -> Sorts.sort_of_univ x),
189-
M (fun ~ok ~ko -> function
190-
| Sorts.Type x -> ok x
191-
| Sorts.Set -> ok Univ.Universe.type0
192-
| _ -> ko ()));
193-
K("uvar","",A(F.uvar,N),
194-
BS (fun (k,_) state ->
195-
let m = S.get um state in
196-
try
197-
let u = UM.host k m in
198-
state, Sorts.sort_of_univ u
199-
with Not_found ->
200-
let state, (_,u) = new_univ_level_variable state in
201-
let state = S.update um state (UM.add k u) in
202-
state, Sorts.sort_of_univ u),
203-
M (fun ~ok ~ko _ -> ko ()));
204-
]
205-
} |> API.ContextualConversion.(!<)
206-
207-
208169
let universe_level_variable =
209170
let { CD.cin = levelin }, universe_level_variable_to_patch = CD.declare {
210171
CD.name = "univ.variable";
@@ -400,6 +361,59 @@ let pr_coq_ctx { env; db2name; db2rel } sigma =
400361
v 0 (Printer.pr_rel_context_of env sigma) ++ cut ()
401362
)
402363

364+
let propc = E.Constants.declare_global_symbol "prop"
365+
let spropc = E.Constants.declare_global_symbol "sprop"
366+
let typc = E.Constants.declare_global_symbol "typ"
367+
368+
369+
let sort : (Sorts.t, _ coq_context, API.Data.constraints) API.ContextualConversion.t =
370+
let open API.ContextualConversion in
371+
{
372+
ty = API.Conversion.TyName "sort";
373+
pp_doc = (fun fmt () ->
374+
Format.fprintf fmt "%% Sorts (kinds of types)\n";
375+
Format.fprintf fmt "kind sort type.\n";
376+
Format.fprintf fmt "type prop sort. %% impredicative sort of propositions\n";
377+
Format.fprintf fmt "type sprop sort. %% impredicative sort of propositions with definitional proof irrelevance\n";
378+
Format.fprintf fmt "type typ univ -> sort. %% predicative sort of data (carries a universe level)\n";
379+
);
380+
pp = (fun fmt -> function
381+
| Sorts.Type _ -> Format.fprintf fmt "Type"
382+
| Sorts.Set -> Format.fprintf fmt "Set"
383+
| Sorts.Prop -> Format.fprintf fmt "Prop"
384+
| Sorts.SProp -> Format.fprintf fmt "SProp"
385+
| Sorts.QSort _ -> Format.fprintf fmt "QSort");
386+
embed = (fun ~depth { options } _ state s ->
387+
match s with
388+
| Sorts.Prop -> state, E.mkConst propc, []
389+
| Sorts.SProp -> state, E.mkConst spropc, []
390+
| Sorts.Set ->
391+
let state, u, gls = univ.embed ~depth state Univ.Universe.type0 in
392+
state, E.mkConst propc, gls
393+
| Sorts.Type u ->
394+
let state, u, gls = univ.embed ~depth state u in
395+
state, E.mkConst propc, gls
396+
| Sorts.QSort _ -> nYI "sort polymorphism");
397+
readback = (fun ~depth { options } _ state t ->
398+
match E.look ~depth t with
399+
| E.Const c when c == propc -> state, Sorts.prop, []
400+
| E.Const c when c == spropc -> state, Sorts.sprop, []
401+
| E.App(c,u,[]) when c == typc ->
402+
let state, u, gls = univ.readback ~depth state u in
403+
state, Sorts.sort_of_univ u ,gls
404+
| E.UnifVar(k,_) -> begin
405+
let m = S.get um state in
406+
try
407+
let u = UM.host k m in
408+
state, Sorts.sort_of_univ u, []
409+
with Not_found ->
410+
let state, (_,u) = new_univ_level_variable state in
411+
let state = S.update um state (UM.add k u) in
412+
state, Sorts.sort_of_univ u, []
413+
end
414+
| _ -> raise API.Conversion.(TypeErr(TyName"sort",depth,t)));
415+
}
416+
403417
let in_coq_fresh ~id_only =
404418
let mk_fresh dbl =
405419
Id.of_string_soft
@@ -949,18 +963,20 @@ let purge_algebraic_univs_sort state s =
949963
let state, _, _, s = force_level_of_universe state u in
950964
state, s
951965
| x -> state, x
952-
966+
967+
let sort = { sort with API.ContextualConversion.embed = (fun ~depth ctx csts state s ->
968+
let state, s =
969+
if ctx.options.algunivs = None || ctx.options.algunivs = Some false then
970+
purge_algebraic_univs_sort state (EConstr.ESorts.make s)
971+
else
972+
state, s in
973+
sort.API.ContextualConversion.embed ~depth ctx csts state s) }
974+
953975
let in_elpi_flex_sort t = E.mkApp sortc (E.mkApp typc t []) []
954-
955-
(* WIP: I do not know how to make this optional *)
956-
(* let sort = { sort with API.Conversion.embed = (fun ~depth state s ->
957-
let state, s = purge_algebraic_univs_sort state (EConstr.ESorts.make s) in
958-
sort.API.Conversion.embed ~depth state s) } *)
959-
960-
let in_elpi_sort ~depth state s =
961-
let state, s, gl = sort.API.Conversion.embed ~depth state s in
962-
assert(gl=[]);
963-
state, E.mkApp sortc s []
976+
977+
let in_elpi_sort ~depth ctx csts state s =
978+
let state, s, gl = sort.API.ContextualConversion.embed ~depth ctx csts state s in
979+
state, E.mkApp sortc s [], gl
964980

965981

966982
(* ********************************* }}} ********************************** *)
@@ -1177,7 +1193,8 @@ let get_options ~depth hyps state =
11771193
no_tc = get_bool_option "coq:no_tc";
11781194
keepunivs = get_bool_option "coq:keepunivs";
11791195
redflags = get_redflags_option ();
1180-
1196+
algunivs = keeping_algebraic_universes @@ get_string_option "coq:algunivs";
1197+
}
11811198
let mk_coq_context ~options state =
11821199
let env = get_global_env state in
11831200
let section = section_ids env in
@@ -1319,7 +1336,10 @@ let rec constr2lp coq_ctx ~calldepth ~depth state t =
13191336
let args = CList.firstn argno args in
13201337
let state, args = CList.fold_left_map (aux ~depth env) state args in
13211338
state, E.mkUnifVar elpi_uvk ~args:(List.rev args) state
1322-
| C.Sort s -> in_elpi_sort ~depth state (EC.ESorts.kind sigma s)
1339+
| C.Sort s ->
1340+
let state, s, gl = in_elpi_sort ~depth coq_ctx API.RawData.no_constraints state (EC.ESorts.kind sigma s) in
1341+
gls := gl @ !gls;
1342+
state, s
13231343
| C.Cast (t,_,ty0) ->
13241344
let state, t = aux ~depth env state t in
13251345
let state, ty = aux ~depth env state ty0 in
@@ -1830,7 +1850,7 @@ and lp2constr ~calldepth syntactic_constraints coq_ctx ~depth state ?(on_ty=fals
18301850
debug Pp.(fun () -> str"lp2term@" ++ int depth ++ str":" ++ str(pp2string (P.term depth) t));
18311851
match E.look ~depth t with
18321852
| E.App(s,p,[]) when sortc == s ->
1833-
let state, u, gsl = sort.API.Conversion.readback ~depth state p in
1853+
let state, u, gsl = sort.API.ContextualConversion.readback ~depth coq_ctx syntactic_constraints state p in
18341854
state, EC.mkSort (EC.ESorts.make u), gsl
18351855
(* constants *)
18361856
| E.App(c,d,[]) when globalc == c ->

‎src/coq_elpi_HOAS.mli‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -148,7 +148,7 @@ val in_elpi_gr : depth:int -> State.t -> Names.GlobRef.t -> term
148148
val in_elpi_poly_gr : depth:int -> State.t -> Names.GlobRef.t -> term -> term
149149
val in_elpi_poly_gr_instance : depth:int -> State.t -> Names.GlobRef.t -> UVars.Instance.t -> term
150150
val in_elpi_flex_sort : term -> term
151-
val in_elpi_sort : depth:int -> state -> Sorts.t -> state * term
151+
val in_elpi_sort : depth:int -> 'a coq_context -> constraints -> state -> Sorts.t -> state * term * Conversion.extra_goals
152152
val in_elpi_prod : Name.t -> term -> term -> term
153153
val in_elpi_lam : Name.t -> term -> term -> term
154154
val in_elpi_let : Name.t -> term -> term -> term -> term
@@ -173,7 +173,7 @@ val gref : Names.GlobRef.t Conversion.t
173173
val inductive : inductive Conversion.t
174174
val constructor : constructor Conversion.t
175175
val constant : global_constant Conversion.t
176-
val sort : Sorts.t Conversion.t
176+
val sort : (Sorts.t,'a coq_context,constraints) ContextualConversion.t
177177
val global_constant_of_globref : Names.GlobRef.t -> global_constant
178178
val abbreviation : Globnames.abbreviation Conversion.t
179179
val implicit_kind : Glob_term.binding_kind Conversion.t

‎src/coq_elpi_builtins.ml‎

Lines changed: 26 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ module B = struct
1515
let ioarg_any = API.BuiltInPredicate.ioarg_any
1616
let ioargC = API.BuiltInPredicate.ioargC
1717
let ioargC_flex = API.BuiltInPredicate.ioargC_flex
18-
let ioarg_flex = API.BuiltInPredicate.ioarg_flex
18+
(*let ioarg_flex = API.BuiltInPredicate.ioarg_flex*)
1919
let ioarg_poly s = { ioarg_any with API.Conversion.ty = API.Conversion.TyName s }
2020
end
2121
module Pred = API.BuiltInPredicate
@@ -367,7 +367,7 @@ let cs_pattern =
367367
K("cs-default","",N,
368368
B Default_cs,
369369
M (fun ~ok ~ko -> function Default_cs -> ok | _ -> ko ()));
370-
K("cs-sort","",A(sort,N),
370+
K("cs-sort","",CA(sort,N),
371371
B (fun s -> Sort_cs (Sorts.family s)),
372372
MS (fun ~ok ~ko p state -> match p with
373373
| Sort_cs Sorts.InSet -> ok Sorts.set state
@@ -378,18 +378,18 @@ let cs_pattern =
378378
ok u state
379379
| _ -> ko state))
380380
]
381-
} |> CConv.(!<)
381+
}
382382

383383
let cs_instance = let open Conv in let open API.AlgebraicData in let open Structures.CSTable in declare {
384384
ty = TyName "cs-instance";
385385
doc = "Canonical Structure instances: (cs-instance Proj ValPat Inst)";
386386
pp = (fun fmt { solution } -> Format.fprintf fmt "@[%a@]" Pp.pp_with ((Printer.pr_global solution)));
387387
constructors = [
388-
K("cs-instance","",A(gref,A(cs_pattern,A(gref,N))),
388+
K("cs-instance","",A(gref,CA(cs_pattern,A(gref,N))),
389389
B (fun p v i -> assert false),
390390
M (fun ~ok ~ko { solution; value; projection } -> ok projection value solution))
391391
]
392-
} |> CConv.(!<)
392+
}
393393

394394

395395
type tc_priority = Computed of int | UserGiven of int
@@ -2275,13 +2275,13 @@ The different data types stay, since Coq will eventually become
22752275
able to handle algebraic universes consistently, making this purging
22762276
phase unnecessary.|};
22772277
MLData univ;
2278-
MLData sort;
2278+
MLDataC sort;
22792279
22802280
MLCode(Pred("coq.sort.leq",
2281-
InOut(B.ioarg_flex sort, "S1",
2282-
InOut(B.ioarg_flex sort, "S2",
2281+
CInOut(B.ioargC_flex sort, "S1",
2282+
CInOut(B.ioargC_flex sort, "S2",
22832283
Full(global, "constrains S1 <= S2"))),
2284-
(fun u1 u2 ~depth { options } _ -> on_global_state "coq.sort.leq"
2284+
(fun u1 u2 ~depth { options } _ -> grab_global_env "coq.sort.leq"
22852285
(fun state ->
22862286
match u1, u2 with
22872287
| Data u1, Data u2 ->
@@ -2295,10 +2295,10 @@ phase unnecessary.|};
22952295
DocAbove);
22962296
22972297
MLCode(Pred("coq.sort.eq",
2298-
InOut(B.ioarg_flex sort, "S1",
2299-
InOut(B.ioarg_flex sort, "S2",
2298+
CInOut(B.ioargC_flex sort, "S1",
2299+
CInOut(B.ioargC_flex sort, "S2",
23002300
Full(global, "constrains S1 = S2"))),
2301-
(fun u1 u2 ~depth { options } _ -> on_global_state "coq.sort.eq"
2301+
(fun u1 u2 ~depth { options } _ -> grab_global_env "coq.sort.eq"
23022302
(fun state ->
23032303
match u1, u2 with
23042304
| Data u1, Data u2 ->
@@ -2312,20 +2312,20 @@ phase unnecessary.|};
23122312
DocAbove);
23132313
23142314
MLCode(Pred("coq.sort.sup",
2315-
InOut(B.ioarg_flex sort, "S1",
2316-
InOut(B.ioarg_flex sort, "S2",
2317-
Full(unit_ctx, "constrains S2 = S1 + 1"))),
2315+
CInOut(B.ioargC_flex sort, "S1",
2316+
CInOut(B.ioargC_flex sort, "S2",
2317+
Full(global, "constrains S2 = S1 + 1"))),
23182318
(fun u1 u2 ~depth _ _ state ->
23192319
match u1, u2 with
23202320
| Data u1, Data u2 -> univ_super state u1 u2, !: u1 +! u2, []
23212321
| _ -> err Pp.(str"coq.sort.sup: called with _ as argument"))),
23222322
DocAbove);
23232323
23242324
MLCode(Pred("coq.sort.pts-triple",
2325-
InOut(B.ioarg_flex sort, "S1",
2326-
InOut(B.ioarg_flex sort, "S2",
2327-
Out(sort, "S3",
2328-
Full(unit_ctx, "constrains S3 = sort of product with domain in S1 and codomain in S2")))),
2325+
CInOut(B.ioargC_flex sort, "S1",
2326+
CInOut(B.ioargC_flex sort, "S2",
2327+
COut(sort, "S3",
2328+
Full(global, "constrains S3 = sort of product with domain in S1 and codomain in S2")))),
23292329
(fun u1 u2 _ ~depth _ _ state ->
23302330
match u1, u2 with
23312331
| Data u1, Data u2 -> let state, u3 = univ_product state u1 u2 in state, !: u1 +! u2 +! u3, []
@@ -2573,8 +2573,8 @@ declared as cumulative.|};
25732573
25742574
LPDoc "-- Databases (TC, CS, Coercions) ------------------------------------";
25752575
2576-
MLData cs_pattern;
2577-
MLData cs_instance;
2576+
MLDataC cs_pattern;
2577+
MLDataC cs_instance;
25782578
25792579
MLCode(Pred("coq.CS.declare-instance",
25802580
In(gref, "GR",
@@ -2587,16 +2587,16 @@ Supported attributes:
25872587
DocAbove);
25882588
25892589
MLCode(Pred("coq.CS.db",
2590-
Out(list cs_instance, "Db",
2590+
COut(CConv.(!>>) list cs_instance, "Db",
25912591
Read(global,"reads all instances")),
25922592
(fun _ ~depth _ _ _ ->
25932593
!: (Structures.CSTable.(entries ())))),
25942594
DocAbove);
25952595
25962596
MLCode(Pred("coq.CS.db-for",
25972597
In(B.unspec gref, "Proj",
2598-
In(B.unspec cs_pattern, "Value",
2599-
Out(list cs_instance, "Db",
2598+
CIn(B.unspecC cs_pattern, "Value",
2599+
COut(CConv.(!>>) list cs_instance, "Db",
26002600
Read(global,"reads all instances for a given Projection or canonical Value, or both")))),
26012601
(fun proj value _ ~depth _ _ state ->
26022602
let env = get_global_env state in
@@ -3190,7 +3190,7 @@ Universe constraints are put in the constraint store.|})))),
31903190
31913191
MLCode(Pred("coq.typecheck-ty",
31923192
CIn(term, "Ty",
3193-
InOut(B.ioarg sort, "U",
3193+
CInOut(B.ioargC sort, "U",
31943194
InOut(B.ioarg B.diagnostic, "Diagnostic",
31953195
Full (proof_context,
31963196
{|typchecks a type Ty returning its universe U. If U is provided, then
@@ -3311,7 +3311,7 @@ Supported attributes:
33113311
33123312
MLCode(Pred("coq.elaborate-ty-skeleton",
33133313
CIn(term_skeleton, "T",
3314-
Out(sort, "U",
3314+
COut(sort, "U",
33153315
COut(term, "E",
33163316
InOut(B.ioarg B.diagnostic, "Diagnostic",
33173317
Full (proof_context,{|elabotares T expecting it to be a type of sort U.

‎src/coq_elpi_glob_quotation.ml‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -175,8 +175,11 @@ let rec gterm2lp ~depth state x =
175175
let s = API.RawData.mkUnifVar f ~args:[] state in
176176
state, in_elpi_flex_sort s
177177
| GSort(UNamed (None, u)) ->
178+
let ctx, _ = Option.default (upcast @@ mk_coq_context ~options:(default_options ()) state, []) (get_ctx state) in
178179
let env = get_glob_env state in
179-
in_elpi_sort ~depth state (sort_name env (get_sigma state) u)
180+
let state, s, gls = in_elpi_sort ~depth ctx E.no_constraints state (sort_name env (get_sigma state) u) in
181+
assert(gls = []);
182+
state,s
180183
| GSort(_) -> nYI "(glob)HOAS for Type@{i j}"
181184

182185
| GProd(name,_,s,t) ->

‎tests/test_API_env.v‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -191,7 +191,8 @@ Elpi Query lp:{{
191191
lp:t lp:y true }})
192192
, constructor "K2x" (parameter "y" _ {{nat}} y\ arity {{
193193
lp:t lp:y false }}) ]),
194-
coq.typecheck-indt-decl D ok,
194+
coq.say D,
195+
std.assert-ok! (coq.typecheck-indt-decl D) "illtyped",
195196
coq.env.add-indt D _.
196197
}}.
197198

0 commit comments

Comments
 (0)