Skip to content

Commit

Permalink
Merge pull request #104 from ppedrot/rm-compat-layer
Browse files Browse the repository at this point in the history 
Remove the V82 compatibility layers.
  • Loading branch information
@palmskog
palmskog authored Nov 29, 2021
2 parents 70ab698 + 224ab67 commit 1a856bd
Show file tree
Hide file tree
Showing 2 changed files with 55 additions and 63 deletions.
99 changes: 46 additions & 53 deletions src/coq.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,10 @@ open EConstr
open Names
open Context.Rel.Declaration

open Proofview.Notations

type tactic = unit Proofview.tactic

let mkArrow x y = mkArrow x Sorts.Relevant y
(* The kernel will fix the relevance if needed. Also as an equality
tactic we probably are only called on relevant terms. *)
Expand Down Expand Up @@ -43,18 +47,15 @@ let nowhere =
Locus.concl_occs = Locus.NoOccurrences
}

let tclEVARS sigma gl =
let open Evd in
{ it = [gl.it]; sigma }

let retype c gl =
let sigma, _ = Tacmach.Old.pf_apply Typing.type_of gl c in
tclEVARS sigma gl
let retype c =
Proofview.Goal.enter begin fun gl ->
let sigma, _ = Typing.type_of (Proofview.Goal.env gl) (Proofview.Goal.sigma gl) c in
Proofview.Unsafe.tclEVARS sigma
end

(* similar to retype above. No Idea when/why this is needed, I smell some ugly hack.
Apparently, it has to do with the need to recompute universe constrains if we just compose terms *)
let tclRETYPE c=
let open Proofview.Notations in
let open Proofview in
tclEVARMAP >>= fun sigma ->
Proofview.Goal.enter (fun goal ->
Expand All @@ -65,11 +66,13 @@ let tclRETYPE c=

(** {1 Tacticals} *)

let tclTIME msg tac = fun gl ->
let tclTIME msg tac =
Proofview.Goal.enter begin fun gl ->
let u = Sys.time () in
let r = tac gl in
tac >>= fun r ->
let _ = Feedback.msg_notice (Pp.str (Printf.sprintf "%s:%fs" msg (Sys.time ()-. u))) in
r
Proofview.tclUNIT r
end

let tclDEBUG msg =
let open Proofview in
Expand All @@ -95,16 +98,16 @@ let show_proof pstate : unit =
let cps_mk_letin
(name:string)
(c: constr)
(k : constr -> Proofview.V82.tac)
: Proofview.V82.tac =
fun goal ->
(k : constr -> tactic)
: tactic =
Proofview.Goal.enter begin fun goal ->
let name = (Id.of_string name) in
let name = Tactics.fresh_id_in_env Id.Set.empty name (Tacmach.Old.pf_env goal) in
let letin = (Proofview.V82.of_tactic (Tactics.letin_tac None (Name name) c None nowhere)) in
Tacticals.Old.tclTHENLIST [retype c; letin; (k (mkVar name))] goal
let name = Tactics.fresh_id_in_env Id.Set.empty name (Tacmach.pf_env goal) in
let letin = Tactics.letin_tac None (Name name) c None nowhere in
Tacticals.tclTHENLIST [retype c; letin; (k (mkVar name))]
end

let mk_letin (name:string) (c: constr) : constr Proofview.tactic =
let open Proofview.Notations in
let open Proofview in
let name = (Id.of_string name) in
Proofview.Goal.enter_one (fun goal ->
Expand All @@ -116,34 +119,24 @@ let mk_letin (name:string) (c: constr) : constr Proofview.tactic =
)
(** {1 General functions} *)

type goal_sigma = Goal.goal Evd.sigma
let goal_update (goal : goal_sigma) evar_map : goal_sigma =
let it = Tacmach.Old.sig_it goal in
Tacmach.Old.re_sig it evar_map

let resolve_one_typeclass goal ty : constr*goal_sigma=
let env = Tacmach.Old.pf_env goal in
let evar_map = Tacmach.Old.project goal in
let em,c = Typeclasses.resolve_one_typeclass env evar_map ty in
c, (goal_update goal em)

let cps_resolve_one_typeclass ?error : types -> (constr -> Proofview.V82.tac) -> Proofview.V82.tac = fun t k goal ->
Tacmach.Old.pf_apply
(fun env em -> let em ,c =
try Typeclasses.resolve_one_typeclass env em t
with Not_found ->
begin match error with
| None -> CErrors.anomaly (Pp.str "Cannot resolve a typeclass : please report")
| Some x -> CErrors.user_err x
end
in
Tacticals.Old.tclTHENLIST [tclEVARS em; k c] goal
) goal


let nf_evar goal c : constr=
let evar_map = Tacmach.Old.project goal in
Evarutil.nf_evar evar_map c
let resolve_one_typeclass env sigma ty : constr * Evd.evar_map =
let sigma, c = Typeclasses.resolve_one_typeclass env sigma ty in
c, sigma

let cps_resolve_one_typeclass ?error : types -> (constr -> tactic) -> tactic = fun t k ->
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let em = Proofview.Goal.sigma gl in
let em, c =
try Typeclasses.resolve_one_typeclass env em t
with Not_found ->
begin match error with
| None -> CErrors.anomaly (Pp.str "Cannot resolve a typeclass : please report")
| Some x -> CErrors.user_err x
end
in
Tacticals.tclTHENLIST [Proofview.Unsafe.tclEVARS em; k c]
end

(* TODO: refactor following similar functions*)

Expand Down Expand Up @@ -283,12 +276,12 @@ module Equivalence = struct
equivalence : constr;
}
let make ty eq equivalence = {carrier = ty; eq = eq; equivalence = equivalence}
let infer goal ty eq =
let infer env sigma ty eq =
let ask = Classes.mk_equivalence ty eq in
let equivalence , goal = resolve_one_typeclass goal ask in
make ty eq equivalence, goal
let from_relation goal rlt =
infer goal (rlt.Relation.carrier) (rlt.Relation.r)
let equivalence, sigma = resolve_one_typeclass env sigma ask in
make ty eq equivalence, sigma
let from_relation env sigma rlt =
infer env sigma (rlt.Relation.carrier) (rlt.Relation.r)
let to_relation t =
{Relation.carrier = t.carrier; Relation.r = t.eq}
let split t =
Expand Down Expand Up @@ -518,8 +511,8 @@ let build
(* let build_with_evar
* (h : hypinfo)
* (subst : (int *constr) list)
* (k :constr -> Proofview.V82.tac)
* : Proofview.V82.tac
* (k :constr -> tactic)
* : tactic
* = fun goal ->
* Tacmach.pf_apply
* (fun env em ->
Expand Down
19 changes: 9 additions & 10 deletions src/coq.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,8 @@
*)

type tactic = unit Proofview.tactic

(** {2 Getting Coq terms from the environment} *)
type lazy_ref = Names.GlobRef.t Lazy.t

Expand All @@ -32,18 +34,15 @@ val find_global : string -> lazy_ref

(** {2 General purpose functions} *)

type goal_sigma = Goal.goal Evd.sigma
val resolve_one_typeclass : Goal.goal Evd.sigma -> EConstr.types -> EConstr.constr * goal_sigma
val cps_resolve_one_typeclass: ?error:Pp.t -> EConstr.types -> (EConstr.constr -> Proofview.V82.tac) -> Proofview.V82.tac
val nf_evar : goal_sigma -> EConstr.constr -> EConstr.constr
val cps_resolve_one_typeclass: ?error:Pp.t -> EConstr.types -> (EConstr.constr -> tactic) -> tactic
val evar_binary: Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.constr
val evar_relation: Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.constr

(** [cps_mk_letin name v] binds the constr [v] using a letin tactic *)
val cps_mk_letin : string -> EConstr.constr -> ( EConstr.constr -> Proofview.V82.tac) -> Proofview.V82.tac
val cps_mk_letin : string -> EConstr.constr -> ( EConstr.constr -> tactic) -> tactic
val mk_letin : string -> EConstr.constr -> EConstr.constr Proofview.tactic

val retype : EConstr.constr -> Proofview.V82.tac
val retype : EConstr.constr -> tactic
val tclRETYPE : EConstr.constr -> unit Proofview.tactic

val decomp_term : Evd.evar_map -> EConstr.constr -> (EConstr.constr , EConstr.types, EConstr.ESorts.t, EConstr.EInstance.t) Constr.kind_of_term
Expand Down Expand Up @@ -114,8 +113,8 @@ module Equivalence : sig
equivalence : EConstr.constr;
}
val make : EConstr.constr -> EConstr.constr -> EConstr.constr -> t
val infer : goal_sigma -> EConstr.constr -> EConstr.constr -> t * goal_sigma
val from_relation : goal_sigma -> Relation.t -> t * goal_sigma
val infer : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> t * Evd.evar_map
val from_relation : Environ.env -> Evd.evar_map -> Relation.t -> t * Evd.evar_map
val to_relation : t -> Relation.t
val split : t -> EConstr.constr * EConstr.constr * EConstr.constr
end
Expand All @@ -127,7 +126,7 @@ val match_as_equation : ?context:EConstr.rel_context -> Environ.env -> Evd.evar
(** {2 Some tacticials} *)

(** time the execution of a tactic *)
val tclTIME : string -> Proofview.V82.tac -> Proofview.V82.tac
val tclTIME : string -> tactic -> tactic

(** emit debug messages to see which tactics are failing *)
val tclDEBUG : string -> unit Proofview.tactic
Expand Down Expand Up @@ -198,7 +197,7 @@ val get_hypinfo : Environ.env -> Evd.evar_map -> ?check_type:(EConstr.types -> b
val build : hypinfo -> (int * EConstr.constr) list -> EConstr.constr

(** build the constr to rewrite, in CPS style, with evars *)
(* val build_with_evar : hypinfo -> (int * EConstr.constr) list -> (EConstr.constr -> Proofview.V82.tac) -> Proofview.V82.tac *)
(* val build_with_evar : hypinfo -> (int * EConstr.constr) list -> (EConstr.constr -> tactic) -> tactic *)

(** [rewrite ?abort hypinfo subst] builds the rewriting tactic
associated with the given [subst] and [hypinfo].
Expand Down

0 comments on commit 1a856bd

Please sign in to comment.