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#18938 (EConstr.ERelevance) #621

Merged
merged 1 commit into from
Apr 23, 2024
Merged

Adapt to coq/coq#18938 (EConstr.ERelevance) #621

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
4 changes: 2 additions & 2 deletions apps/coercion/src/coq_elpi_coercion_hook.mlg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,8 +15,8 @@ let elpi_coercion_hook program env sigma ~flags v ~inferred ~expected =
match expected with
| Coercion.Type t -> (env, sigma, t, false)
| Coercion.Product -> begin let (sigma, (source, _)) = Evarutil.new_type_evar env sigma Evd.univ_flexible in
let (sigma, (target, _)) = let env = EConstr.push_rel (Context.Rel.Declaration.LocalAssum (Context.annotR (Names.Name (Namegen.default_dependent_ident)) , source)) env in Evarutil.new_type_evar env sigma Evd.univ_flexible in
(env, sigma, EConstr.mkProd (Context.annotR (Names.Name (Namegen.default_type_ident)), source, target), true) end
let (sigma, (target, _)) = let env = EConstr.push_rel (Context.Rel.Declaration.LocalAssum (EConstr.annotR (Names.Name (Namegen.default_dependent_ident)) , source)) env in Evarutil.new_type_evar env sigma Evd.univ_flexible in
(env, sigma, EConstr.mkProd (EConstr.annotR (Names.Name (Namegen.default_type_ident)), source, target), true) end
| Coercion.Sort -> let (sigma, t) = Evarutil.new_Type sigma in (env, sigma, t, true) in
let sigma, goal = Evarutil.new_evar env sigma expected in
let goal_evar, _ = EConstr.destEvar sigma goal in
Expand Down
6 changes: 4 additions & 2 deletions apps/tc/src/coq_elpi_class_tactics_hacked.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -465,9 +465,10 @@ module Search = struct
let (dir, onlyc, sign', cached_modes, cached_hints) = !autogoal_cache in
let cwd = Lib.cwd () in
let eq c1 c2 = EConstr.eq_constr sigma c1 c2 in
let eqr r1 r2 = ERelevance.equal sigma r1 r2 in
if DirPath.equal cwd dir &&
(onlyc == only_classes) &&
Context.Named.equal eq sign sign' &&
Context.Named.equal eqr eq sign sign' &&
cached_modes == modes
then cached_hints
else
Expand Down Expand Up @@ -730,8 +731,9 @@ module Search = struct
pr_ev sigma' (Proofview.Goal.goal gl'))
in
let eq c1 c2 = EConstr.eq_constr sigma' c1 c2 in
let eqr r1 r2 = ERelevance.equal sigma' r1 r2 in
let hints' =
if b && not (Context.Named.equal eq (Goal.hyps gl') (Goal.hyps gl))
if b && not (Context.Named.equal eqr eq (Goal.hyps gl') (Goal.hyps gl))
then
let st = Hint_db.transparent_state info.search_hints in
let modes = Hint_db.modes info.search_hints in
Expand Down
23 changes: 12 additions & 11 deletions src/coq_elpi_HOAS.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ module EC = EConstr
open Names
module G = GlobRef
open Coq_elpi_utils
module ERelevance = EC.ERelevance

(* ************************************************************************ *)
(* ****************** HOAS of Coq terms and goals ************************* *)
Expand Down Expand Up @@ -409,14 +410,14 @@ fun ~depth dbl name ~names ->
| Name.Name id when Id.Set.mem id names -> Name.Name (mk_fresh dbl)
| Name.Name id as x -> x

let in_coq_annot ~depth t = Context.make_annot (in_coq_name ~depth t) Sorts.Relevant
let in_coq_annot ~depth t = Context.make_annot (in_coq_name ~depth t) ERelevance.relevant

let in_coq_fresh_annot_name ~depth ~coq_ctx dbl t =
Context.make_annot (in_coq_fresh ~id_only:false ~depth ~names:coq_ctx.names dbl t) Sorts.Relevant
Context.make_annot (in_coq_fresh ~id_only:false ~depth ~names:coq_ctx.names dbl t) ERelevance.relevant

let in_coq_fresh_annot_id ~depth ~names dbl t =
let get_name = function Name.Name x -> x | Name.Anonymous -> assert false in
Context.make_annot (in_coq_fresh ~id_only:true ~depth ~names dbl t |> get_name) Sorts.Relevant
Context.make_annot (in_coq_fresh ~id_only:true ~depth ~names dbl t |> get_name) ERelevance.relevant

let unspec2opt = function Elpi.Builtin.Given x -> Some x | Elpi.Builtin.Unspec -> None
let opt2unspec = function Some x -> Elpi.Builtin.Given x | None -> Elpi.Builtin.Unspec
Expand Down Expand Up @@ -1324,7 +1325,7 @@ let rec constr2lp coq_ctx ~calldepth ~depth state t =
| C.Cast (t,_,ty0) ->
let state, t = aux ~depth env state t in
let state, ty = aux ~depth env state ty0 in
let env = EConstr.push_rel Context.Rel.Declaration.(LocalAssum(Context.make_annot Anonymous Sorts.Relevant,ty0)) env in
let env = EConstr.push_rel Context.Rel.Declaration.(LocalAssum(Context.make_annot Anonymous EConstr.ERelevance.relevant,ty0)) env in
let state, self = aux ~depth:(depth+1) env state (EC.mkRel 1) in
state, in_elpi_let Names.Name.Anonymous t ty self
| C.Prod(n,s0,t) ->
Expand Down Expand Up @@ -1900,7 +1901,7 @@ and lp2constr ~calldepth syntactic_constraints coq_ctx ~depth state ?(on_ty=fals
let state, i, gl1 = aux ~depth state i in
let state, xs, gl2 = API.Utils.map_acc (aux ~depth ~on_ty:false) state xs in
(* TODO handle relevance *)
state, EC.mkApp (EC.mkProj (p,Relevant,i),Array.of_list xs), gls @ gl1 @ gl2
state, EC.mkApp (EC.mkProj (p,ERelevance.relevant,i),Array.of_list xs), gls @ gl1 @ gl2
| _ -> err Pp.(str"not a primitive projection:" ++ str (E.Constants.show c))
end
| x, _ ->
Expand Down Expand Up @@ -1949,15 +1950,15 @@ and lp2constr ~calldepth syntactic_constraints coq_ctx ~depth state ?(on_ty=fals
begin match ind with
| `SomeInd ind ->
let ci = Inductiveops.make_case_info (get_global_env state) ind C.RegularStyle in
state, EC.mkCase (EConstr.contract_case (get_global_env state) sigma (ci,(rt,Relevant),C.NoInvert,t,Array.of_list bt)), gl1 @ gl2 @ gl3
state, EC.mkCase (EConstr.contract_case (get_global_env state) sigma (ci,(rt,ERelevance.relevant),C.NoInvert,t,Array.of_list bt)), gl1 @ gl2 @ gl3
| `None -> CErrors.anomaly Pp.(str "non dependent match on unknown, non singleton, inductive")
| `SomeTerm (n,rt) ->
let ci = default_case_info () in
let b =
match bt with
| [t] -> [||], t
| _ -> assert false in
state, EConstr.mkCase (ci,EConstr.EInstance.empty,[||],(([|n|],rt),Relevant),Constr.NoInvert,t,[|b|]), gl1 @ gl2 @ gl3
state, EConstr.mkCase (ci,EConstr.EInstance.empty,[||],(([|n|],rt),ERelevance.relevant),Constr.NoInvert,t,[|b|]), gl1 @ gl2 @ gl3
end

(* fix *)
Expand Down Expand Up @@ -2861,7 +2862,7 @@ let lp2inductive_entry ~depth coq_ctx constraints state t =
poly_cumul_udecl_variance_of_options state coq_ctx.options in
let the_type =
let open Context.Rel.Declaration in
LocalAssum(Context.nameR itname, EConstr.it_mkProd_or_LetIn arity (nuparams @ params)) in
LocalAssum(EConstr.nameR itname, EConstr.it_mkProd_or_LetIn arity (nuparams @ params)) in
let env_ar_params = (Global.env ()) |> EC.push_rel the_type |> EC.push_rel_context (nuparams @ params) in
let arityconcl =
match Reductionops.sort_of_arity env_ar_params sigma arity with
Expand Down Expand Up @@ -3061,7 +3062,7 @@ let under_coq2elpi_relctx ~calldepth state (ctx : 'a ctx_entry list) ~coq_ctx ~m
gls := gls_ty @ !gls;
let hyp = mk_decl ~depth name ~ty in
let hyps = { ctx_entry = hyp ; depth = depth } :: hyps in
let e = Context.Rel.Declaration.LocalAssum (Context.annotR name, typ) in
let e = Context.Rel.Declaration.LocalAssum (EConstr.annotR name, typ) in
let coq_ctx = push_coq_ctx_local depth e coq_ctx in
let state, rest = aux ~depth:(depth+1) coq_ctx hyps state rest in
mk_ctx_item ~depth name extra ty rest state
Expand Down Expand Up @@ -3128,15 +3129,15 @@ let hoas_ind2lp ~depth coq_ctx state { params; decl } =
let i = i + 1 in (* init is 0 based, rels are 1 base *)
if i = arityno + paramsno + 1 then
let ind = EC.mkRel (arityno + 1) in
iter paramsno ind (fun x -> EConstr.mkLambda (Context.anonR,EConstr.mkProp,EConstr.Vars.lift 1 x))
iter paramsno ind (fun x -> EConstr.mkLambda (EConstr.anonR,EConstr.mkProp,EConstr.Vars.lift 1 x))
else if i > arityno then EC.mkRel(i+1)
else EC.mkRel i) in
let reloc ctx_len t =
let t = EC.Vars.substl (subst ctx_len) t in
Reductionops.nf_beta (Global.env()) sigma t in

let state, arity, gls1 = embed_arity ~depth coq_ctx state (nuparams,typ) in
let coq_ctx = push_coq_ctx_local depth (Context.Rel.Declaration.LocalAssum(Context.anonR,EConstr.mkProp)) coq_ctx in
let coq_ctx = push_coq_ctx_local depth (Context.Rel.Declaration.LocalAssum(EConstr.anonR,EConstr.mkProp)) coq_ctx in
let depth = depth+1 in
let embed_constructor state { id; arity; typ } =
let alen = List.length arity in
Expand Down
2 changes: 1 addition & 1 deletion src/coq_elpi_utils.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ exception LtacFail of int * Pp.t
val ltac_fail_err : ?loc:Elpi.API.Ast.Loc.t -> int -> Pp.t -> 'a
val nYI : string -> 'a
val safe_destApp : Evd.evar_map ->
EConstr.t -> (EConstr.t,EConstr.types,EConstr.ESorts.t, EConstr.EInstance.t) Constr.kind_of_term * EConstr.t array
EConstr.t -> (EConstr.t,EConstr.types,EConstr.ESorts.t, EConstr.EInstance.t, EConstr.ERelevance.t) Constr.kind_of_term * EConstr.t array
val mkGHole : Glob_term.glob_constr
val pp2string : (Format.formatter -> 'a -> unit) -> 'a -> string
val mkApp : depth:int -> Elpi.API.RawData.term -> Elpi.API.RawData.term list -> Elpi.API.RawData.term
Expand Down
Loading