Skip to content

Commit

Permalink
wip
Browse files Browse the repository at this point in the history
  • Loading branch information
@gares
gares committed Feb 8, 2024
1 parent 7d33e0e commit a86a913
Show file tree
Hide file tree
Showing 6 changed files with 108 additions and 85 deletions.
3 changes: 1 addition & 2 deletions coq-builtin.elpi
View file
Original file line number Diff line number Diff line change
Expand Up @@ -957,8 +957,7 @@ typeabbrev univ (ctype "univ").
kind sort type.
type prop sort. % impredicative sort of propositions
type sprop sort. % impredicative sort of propositions with definitional proof irrelevance
type typ univ ->
sort. % predicative sort of data (carries a universe level)
type typ univ -> sort. % predicative sort of data (carries a universe level)

% [coq.sort.leq S1 S2] constrains S1 <= S2
external pred coq.sort.leq o:sort, o:sort.
Expand Down
126 changes: 73 additions & 53 deletions src/coq_elpi_HOAS.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -166,45 +166,6 @@ let isuniv, univout, (univ : Univ.Universe.t API.Conversion.t) =
| _ -> univ_to_be_patched.API.Conversion.readback ~depth state t
end
}

let sort =
let open API.AlgebraicData in declare {
ty = API.Conversion.TyName "sort";
doc = "Sorts (kinds of types)";
pp = (fun fmt -> function
| Sorts.Type _ -> Format.fprintf fmt "Type"
| Sorts.Set -> Format.fprintf fmt "Set"
| Sorts.Prop -> Format.fprintf fmt "Prop"
| Sorts.SProp -> Format.fprintf fmt "SProp"
| Sorts.QSort _ -> Format.fprintf fmt "Type");
constructors = [
K("prop","impredicative sort of propositions",N,
B Sorts.prop,
M (fun ~ok ~ko -> function Sorts.Prop -> ok | _ -> ko ()));
K("sprop","impredicative sort of propositions with definitional proof irrelevance",N,
B Sorts.sprop,
M (fun ~ok ~ko -> function Sorts.SProp -> ok | _ -> ko ()));
K("typ","predicative sort of data (carries a universe level)",A(univ,N),
B (fun x -> Sorts.sort_of_univ x),
M (fun ~ok ~ko -> function
| Sorts.Type x -> ok x
| Sorts.Set -> ok Univ.Universe.type0
| _ -> ko ()));
K("uvar","",A(F.uvar,N),
BS (fun (k,_) state ->
let m = S.get um state in
try
let u = UM.host k m in
state, Sorts.sort_of_univ u
with Not_found ->
let state, (_,u) = new_univ_level_variable state in
let state = S.update um state (UM.add k u) in
state, Sorts.sort_of_univ u),
M (fun ~ok ~ko _ -> ko ()));
]
} |> API.ContextualConversion.(!<)


let universe_level_variable =
let { CD.cin = levelin }, universe_level_variable_to_patch = CD.declare {
CD.name = "univ.variable";
Expand Down Expand Up @@ -400,6 +361,59 @@ let pr_coq_ctx { env; db2name; db2rel } sigma =
v 0 (Printer.pr_rel_context_of env sigma) ++ cut ()
)

let propc = E.Constants.declare_global_symbol "prop"
let spropc = E.Constants.declare_global_symbol "sprop"
let typc = E.Constants.declare_global_symbol "typ"


let sort : (Sorts.t, _ coq_context, API.Data.constraints) API.ContextualConversion.t =
let open API.ContextualConversion in
{
ty = API.Conversion.TyName "sort";
pp_doc = (fun fmt () ->
Format.fprintf fmt "%% Sorts (kinds of types)\n";
Format.fprintf fmt "kind sort type.\n";
Format.fprintf fmt "type prop sort. %% impredicative sort of propositions\n";
Format.fprintf fmt "type sprop sort. %% impredicative sort of propositions with definitional proof irrelevance\n";
Format.fprintf fmt "type typ univ -> sort. %% predicative sort of data (carries a universe level)\n";
);
pp = (fun fmt -> function
| Sorts.Type _ -> Format.fprintf fmt "Type"
| Sorts.Set -> Format.fprintf fmt "Set"
| Sorts.Prop -> Format.fprintf fmt "Prop"
| Sorts.SProp -> Format.fprintf fmt "SProp"
| Sorts.QSort _ -> Format.fprintf fmt "QSort");
embed = (fun ~depth { options } _ state s ->
match s with
| Sorts.Prop -> state, E.mkConst propc, []
| Sorts.SProp -> state, E.mkConst spropc, []
| Sorts.Set ->
let state, u, gls = univ.embed ~depth state Univ.Universe.type0 in
state, E.mkConst propc, gls
| Sorts.Type u ->
let state, u, gls = univ.embed ~depth state u in
state, E.mkConst propc, gls
| Sorts.QSort _ -> nYI "sort polymorphism");
readback = (fun ~depth { options } _ state t ->
match E.look ~depth t with
| E.Const c when c == propc -> state, Sorts.prop, []
| E.Const c when c == spropc -> state, Sorts.sprop, []
| E.App(c,u,[]) when c == typc ->
let state, u, gls = univ.readback ~depth state u in
state, Sorts.sort_of_univ u ,gls
| E.UnifVar(k,_) -> begin
let m = S.get um state in
try
let u = UM.host k m in
state, Sorts.sort_of_univ u, []
with Not_found ->
let state, (_,u) = new_univ_level_variable state in
let state = S.update um state (UM.add k u) in
state, Sorts.sort_of_univ u, []
end
| _ -> raise API.Conversion.(TypeErr(TyName"sort",depth,t)));
}

let in_coq_fresh ~id_only =
let mk_fresh dbl =
Id.of_string_soft
Expand Down Expand Up @@ -949,18 +963,20 @@ let purge_algebraic_univs_sort state s =
let state, _, _, s = force_level_of_universe state u in
state, s
| x -> state, x


let sort = { sort with API.ContextualConversion.embed = (fun ~depth ctx csts state s ->
let state, s =
if ctx.options.algunivs = None || ctx.options.algunivs = Some false then
purge_algebraic_univs_sort state (EConstr.ESorts.make s)
else
state, s in
sort.API.ContextualConversion.embed ~depth ctx csts state s) }

let in_elpi_flex_sort t = E.mkApp sortc (E.mkApp typc t []) []

(* WIP: I do not know how to make this optional *)
(* let sort = { sort with API.Conversion.embed = (fun ~depth state s ->
let state, s = purge_algebraic_univs_sort state (EConstr.ESorts.make s) in
sort.API.Conversion.embed ~depth state s) } *)

let in_elpi_sort ~depth state s =
let state, s, gl = sort.API.Conversion.embed ~depth state s in
assert(gl=[]);
state, E.mkApp sortc s []

let in_elpi_sort ~depth ctx csts state s =
let state, s, gl = sort.API.ContextualConversion.embed ~depth ctx csts state s in
state, E.mkApp sortc s [], gl


(* ********************************* }}} ********************************** *)
Expand Down Expand Up @@ -1177,7 +1193,8 @@ let get_options ~depth hyps state =
no_tc = get_bool_option "coq:no_tc";
keepunivs = get_bool_option "coq:keepunivs";
redflags = get_redflags_option ();

algunivs = keeping_algebraic_universes @@ get_string_option "coq:algunivs";
}
let mk_coq_context ~options state =
let env = get_global_env state in
let section = section_ids env in
Expand Down Expand Up @@ -1319,7 +1336,10 @@ let rec constr2lp coq_ctx ~calldepth ~depth state t =
let args = CList.firstn argno args in
let state, args = CList.fold_left_map (aux ~depth env) state args in
state, E.mkUnifVar elpi_uvk ~args:(List.rev args) state
| C.Sort s -> in_elpi_sort ~depth state (EC.ESorts.kind sigma s)
| C.Sort s ->
let state, s, gl = in_elpi_sort ~depth coq_ctx API.RawData.no_constraints state (EC.ESorts.kind sigma s) in
gls := gl @ !gls;
state, s
| C.Cast (t,_,ty0) ->
let state, t = aux ~depth env state t in
let state, ty = aux ~depth env state ty0 in
Expand Down Expand Up @@ -1830,7 +1850,7 @@ and lp2constr ~calldepth syntactic_constraints coq_ctx ~depth state ?(on_ty=fals
debug Pp.(fun () -> str"lp2term@" ++ int depth ++ str":" ++ str(pp2string (P.term depth) t));
match E.look ~depth t with
| E.App(s,p,[]) when sortc == s ->
let state, u, gsl = sort.API.Conversion.readback ~depth state p in
let state, u, gsl = sort.API.ContextualConversion.readback ~depth coq_ctx syntactic_constraints state p in
state, EC.mkSort (EC.ESorts.make u), gsl
(* constants *)
| E.App(c,d,[]) when globalc == c ->
Expand Down
4 changes: 2 additions & 2 deletions src/coq_elpi_HOAS.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -148,7 +148,7 @@ val in_elpi_gr : depth:int -> State.t -> Names.GlobRef.t -> term
val in_elpi_poly_gr : depth:int -> State.t -> Names.GlobRef.t -> term -> term
val in_elpi_poly_gr_instance : depth:int -> State.t -> Names.GlobRef.t -> UVars.Instance.t -> term
val in_elpi_flex_sort : term -> term
val in_elpi_sort : depth:int -> state -> Sorts.t -> state * term
val in_elpi_sort : depth:int -> 'a coq_context -> constraints -> state -> Sorts.t -> state * term * Conversion.extra_goals
val in_elpi_prod : Name.t -> term -> term -> term
val in_elpi_lam : Name.t -> term -> term -> term
val in_elpi_let : Name.t -> term -> term -> term -> term
Expand All @@ -173,7 +173,7 @@ val gref : Names.GlobRef.t Conversion.t
val inductive : inductive Conversion.t
val constructor : constructor Conversion.t
val constant : global_constant Conversion.t
val sort : Sorts.t Conversion.t
val sort : (Sorts.t,'a coq_context,constraints) ContextualConversion.t
val global_constant_of_globref : Names.GlobRef.t -> global_constant
val abbreviation : Globnames.abbreviation Conversion.t
val implicit_kind : Glob_term.binding_kind Conversion.t
Expand Down
52 changes: 26 additions & 26 deletions src/coq_elpi_builtins.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ module B = struct
let ioarg_any = API.BuiltInPredicate.ioarg_any
let ioargC = API.BuiltInPredicate.ioargC
let ioargC_flex = API.BuiltInPredicate.ioargC_flex
let ioarg_flex = API.BuiltInPredicate.ioarg_flex
(*let ioarg_flex = API.BuiltInPredicate.ioarg_flex*)
let ioarg_poly s = { ioarg_any with API.Conversion.ty = API.Conversion.TyName s }
end
module Pred = API.BuiltInPredicate
Expand Down Expand Up @@ -367,7 +367,7 @@ let cs_pattern =
K("cs-default","",N,
B Default_cs,
M (fun ~ok ~ko -> function Default_cs -> ok | _ -> ko ()));
K("cs-sort","",A(sort,N),
K("cs-sort","",CA(sort,N),
B (fun s -> Sort_cs (Sorts.family s)),
MS (fun ~ok ~ko p state -> match p with
| Sort_cs Sorts.InSet -> ok Sorts.set state
Expand All @@ -378,18 +378,18 @@ let cs_pattern =
ok u state
| _ -> ko state))
]
} |> CConv.(!<)
}

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


type tc_priority = Computed of int | UserGiven of int
Expand Down Expand Up @@ -2275,13 +2275,13 @@ The different data types stay, since Coq will eventually become
able to handle algebraic universes consistently, making this purging
phase unnecessary.|};
MLData univ;
MLData sort;
MLDataC sort;
MLCode(Pred("coq.sort.leq",
InOut(B.ioarg_flex sort, "S1",
InOut(B.ioarg_flex sort, "S2",
CInOut(B.ioargC_flex sort, "S1",
CInOut(B.ioargC_flex sort, "S2",
Full(global, "constrains S1 <= S2"))),
(fun u1 u2 ~depth { options } _ -> on_global_state "coq.sort.leq"
(fun u1 u2 ~depth { options } _ -> grab_global_env "coq.sort.leq"
(fun state ->
match u1, u2 with
| Data u1, Data u2 ->
Expand All @@ -2295,10 +2295,10 @@ phase unnecessary.|};
DocAbove);
MLCode(Pred("coq.sort.eq",
InOut(B.ioarg_flex sort, "S1",
InOut(B.ioarg_flex sort, "S2",
CInOut(B.ioargC_flex sort, "S1",
CInOut(B.ioargC_flex sort, "S2",
Full(global, "constrains S1 = S2"))),
(fun u1 u2 ~depth { options } _ -> on_global_state "coq.sort.eq"
(fun u1 u2 ~depth { options } _ -> grab_global_env "coq.sort.eq"
(fun state ->
match u1, u2 with
| Data u1, Data u2 ->
Expand All @@ -2312,20 +2312,20 @@ phase unnecessary.|};
DocAbove);
MLCode(Pred("coq.sort.sup",
InOut(B.ioarg_flex sort, "S1",
InOut(B.ioarg_flex sort, "S2",
Full(unit_ctx, "constrains S2 = S1 + 1"))),
CInOut(B.ioargC_flex sort, "S1",
CInOut(B.ioargC_flex sort, "S2",
Full(global, "constrains S2 = S1 + 1"))),
(fun u1 u2 ~depth _ _ state ->
match u1, u2 with
| Data u1, Data u2 -> univ_super state u1 u2, !: u1 +! u2, []
| _ -> err Pp.(str"coq.sort.sup: called with _ as argument"))),
DocAbove);
MLCode(Pred("coq.sort.pts-triple",
InOut(B.ioarg_flex sort, "S1",
InOut(B.ioarg_flex sort, "S2",
Out(sort, "S3",
Full(unit_ctx, "constrains S3 = sort of product with domain in S1 and codomain in S2")))),
CInOut(B.ioargC_flex sort, "S1",
CInOut(B.ioargC_flex sort, "S2",
COut(sort, "S3",
Full(global, "constrains S3 = sort of product with domain in S1 and codomain in S2")))),
(fun u1 u2 _ ~depth _ _ state ->
match u1, u2 with
| Data u1, Data u2 -> let state, u3 = univ_product state u1 u2 in state, !: u1 +! u2 +! u3, []
Expand Down Expand Up @@ -2573,8 +2573,8 @@ declared as cumulative.|};
LPDoc "-- Databases (TC, CS, Coercions) ------------------------------------";
MLData cs_pattern;
MLData cs_instance;
MLDataC cs_pattern;
MLDataC cs_instance;
MLCode(Pred("coq.CS.declare-instance",
In(gref, "GR",
Expand All @@ -2587,16 +2587,16 @@ Supported attributes:
DocAbove);
MLCode(Pred("coq.CS.db",
Out(list cs_instance, "Db",
COut(CConv.(!>>) list cs_instance, "Db",
Read(global,"reads all instances")),
(fun _ ~depth _ _ _ ->
!: (Structures.CSTable.(entries ())))),
DocAbove);
MLCode(Pred("coq.CS.db-for",
In(B.unspec gref, "Proj",
In(B.unspec cs_pattern, "Value",
Out(list cs_instance, "Db",
CIn(B.unspecC cs_pattern, "Value",
COut(CConv.(!>>) list cs_instance, "Db",
Read(global,"reads all instances for a given Projection or canonical Value, or both")))),
(fun proj value _ ~depth _ _ state ->
let env = get_global_env state in
Expand Down Expand Up @@ -3190,7 +3190,7 @@ Universe constraints are put in the constraint store.|})))),
MLCode(Pred("coq.typecheck-ty",
CIn(term, "Ty",
InOut(B.ioarg sort, "U",
CInOut(B.ioargC sort, "U",
InOut(B.ioarg B.diagnostic, "Diagnostic",
Full (proof_context,
{|typchecks a type Ty returning its universe U. If U is provided, then
Expand Down Expand Up @@ -3311,7 +3311,7 @@ Supported attributes:
MLCode(Pred("coq.elaborate-ty-skeleton",
CIn(term_skeleton, "T",
Out(sort, "U",
COut(sort, "U",
COut(term, "E",
InOut(B.ioarg B.diagnostic, "Diagnostic",
Full (proof_context,{|elabotares T expecting it to be a type of sort U.
Expand Down
5 changes: 4 additions & 1 deletion src/coq_elpi_glob_quotation.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -175,8 +175,11 @@ let rec gterm2lp ~depth state x =
let s = API.RawData.mkUnifVar f ~args:[] state in
state, in_elpi_flex_sort s
| GSort(UNamed (None, u)) ->
let ctx, _ = Option.default (upcast @@ mk_coq_context ~options:(default_options ()) state, []) (get_ctx state) in
let env = get_glob_env state in
in_elpi_sort ~depth state (sort_name env (get_sigma state) u)
let state, s, gls = in_elpi_sort ~depth ctx E.no_constraints state (sort_name env (get_sigma state) u) in
assert(gls = []);
state,s
| GSort(_) -> nYI "(glob)HOAS for Type@{i j}"

| GProd(name,_,s,t) ->
Expand Down
3 changes: 2 additions & 1 deletion tests/test_API_env.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -191,7 +191,8 @@ Elpi Query lp:{{
lp:t lp:y true }})
, constructor "K2x" (parameter "y" _ {{nat}} y\ arity {{
lp:t lp:y false }}) ]),
coq.typecheck-indt-decl D ok,
coq.say D,
std.assert-ok! (coq.typecheck-indt-decl D) "illtyped",
coq.env.add-indt D _.
}}.

Expand Down

0 comments on commit a86a913

Please sign in to comment.