aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--ide/coq.ml1
-rw-r--r--lib/util.ml8
-rw-r--r--lib/util.mli1
-rw-r--r--parsing/g_vernac.ml42
-rw-r--r--parsing/ppvernac.ml5
-rw-r--r--parsing/prettyp.ml2
-rw-r--r--parsing/printer.ml6
-rw-r--r--plugins/dp/dp_plugin.mllib1
-rw-r--r--plugins/funind/merge.ml7
-rw-r--r--plugins/interface/xlate.ml4
-rw-r--r--plugins/subtac/equations.ml41149
-rw-r--r--plugins/subtac/eterm.ml68
-rw-r--r--plugins/subtac/eterm.mli16
-rw-r--r--plugins/subtac/g_eterm.ml427
-rw-r--r--plugins/subtac/subtac.ml6
-rw-r--r--plugins/subtac/subtac_classes.ml9
-rw-r--r--plugins/subtac/subtac_command.ml41
-rw-r--r--plugins/subtac/subtac_obligations.ml155
-rw-r--r--plugins/subtac/subtac_obligations.mli14
-rw-r--r--plugins/subtac/subtac_plugin.mllib2
-rw-r--r--plugins/subtac/subtac_pretyping.ml4
-rw-r--r--plugins/subtac/subtac_utils.ml9
-rw-r--r--plugins/subtac/subtac_utils.mli1
-rw-r--r--pretyping/coercion.ml2
-rw-r--r--pretyping/evarutil.ml7
-rw-r--r--pretyping/evarutil.mli3
-rw-r--r--pretyping/typeclasses.ml87
-rw-r--r--pretyping/typeclasses.mli17
-rw-r--r--pretyping/unification.ml47
-rw-r--r--tactics/auto.ml38
-rw-r--r--tactics/auto.mli2
-rw-r--r--tactics/autorewrite.ml8
-rw-r--r--tactics/class_tactics.ml4194
-rw-r--r--tactics/eauto.ml4100
-rw-r--r--tactics/eauto.mli2
-rw-r--r--tactics/extratactics.ml418
-rw-r--r--tactics/rewrite.ml411
-rw-r--r--tactics/tactics.ml275
-rw-r--r--tactics/tactics.mli3
-rw-r--r--test-suite/success/Equations.v321
-rw-r--r--test-suite/success/dependentind.v6
-rw-r--r--theories/Program/Equality.v339
-rw-r--r--theories/Program/Subset.v2
-rw-r--r--theories/Program/Syntax.v7
-rw-r--r--theories/Program/Tactics.v21
-rw-r--r--theories/Wellfounded/Transitive_Closure.v4
-rw-r--r--tools/coqdoc/coqdoc.sty2
-rw-r--r--tools/coqdoc/cpretty.mll3
-rw-r--r--toplevel/autoinstance.ml2
-rw-r--r--toplevel/classes.ml48
-rw-r--r--toplevel/classes.mli12
-rw-r--r--toplevel/record.ml12
-rw-r--r--toplevel/toplevel.mllib2
-rw-r--r--toplevel/vernacentries.ml5
-rw-r--r--toplevel/vernacexpr.ml3
55 files changed, 986 insertions, 2155 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index 11d8a3061..b9257de84 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -238,6 +238,7 @@ let rec attribute_of_vernac_command = function
| VernacInstance _ -> []
| VernacContext _ -> []
| VernacDeclareInstance _ -> []
+ | VernacDeclareClass _ -> []
(* Solving *)
| VernacSolve _ -> [SolveCommand]
diff --git a/lib/util.ml b/lib/util.ml
index 2815af014..794f1a6ac 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -1012,6 +1012,14 @@ let array_for_all_i f i v =
let rec allrec i n = n = Array.length v || f i v.(n) && allrec (i+1) (n+1) in
allrec i 0
+exception Found of int
+
+let array_find_i (pred: int -> 'a -> bool) (arr: 'a array) : int option =
+ try
+ for i=0 to Array.length arr - 1 do if pred i (arr.(i)) then raise (Found i) done;
+ None
+ with Found i -> Some i
+
let array_hd v =
match Array.length v with
| 0 -> failwith "array_hd"
diff --git a/lib/util.mli b/lib/util.mli
index 4e2bb6d33..6ab9ce7c4 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -216,6 +216,7 @@ val array_for_all3 : ('a -> 'b -> 'c -> bool) ->
val array_for_all4 : ('a -> 'b -> 'c -> 'd -> bool) ->
'a array -> 'b array -> 'c array -> 'd array -> bool
val array_for_all_i : (int -> 'a -> bool) -> int -> 'a array -> bool
+val array_find_i : (int -> 'a -> bool) -> 'a array -> int option
val array_hd : 'a array -> 'a
val array_tl : 'a array -> 'a array
val array_last : 'a array -> 'a
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 7494ffd7c..2fd822636 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -538,6 +538,8 @@ GEXTEND Gram
| IDENT "Existing"; IDENT "Instance"; is = identref -> VernacDeclareInstance is
+ | IDENT "Existing"; IDENT "Class"; is = identref -> VernacDeclareClass is
+
(* Implicit *)
| IDENT "Implicit"; IDENT "Arguments"; qid = smart_global;
pos = OPT [ "["; l = LIST0 implicit_name; "]" ->
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 8a8248bf4..6449add92 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -741,7 +741,10 @@ let rec pr_vernac = function
| VernacDeclareInstance id ->
- hov 1 (str"Instance" ++ spc () ++ pr_lident id)
+ hov 1 (str"Existing" ++ spc () ++ str"Instance" ++ spc () ++ pr_lident id)
+
+ | VernacDeclareClass id ->
+ hov 1 (str"Existing" ++ spc () ++ str"Class" ++ spc () ++ pr_lident id)
(* Modules and Module Types *)
| VernacDefineModule (export,m,bl,ty,bd) ->
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index f96a94fb4..b7e218719 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -786,7 +786,7 @@ let print_typeclasses () =
let pr_instance env i =
(* gallina_print_constant_with_infos i.is_impl *)
(* lighter *)
- print_ref false (ConstRef (instance_impl i))
+ print_ref false (instance_impl i)
let print_all_instances () =
let env = Global.env () in
diff --git a/parsing/printer.ml b/parsing/printer.ml
index eacad74c4..d9dced791 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -540,9 +540,9 @@ let cmap_to_list m = Cmap.fold (fun k v acc -> v :: acc) m []
open Typeclasses
-let pr_instance i =
- pr_global (ConstRef (instance_impl i))
-
+let pr_instance i =
+ pr_global (instance_impl i)
+
let pr_instance_gmap insts =
prlist_with_sep fnl (fun (gr, insts) ->
prlist_with_sep fnl pr_instance (cmap_to_list insts))
diff --git a/plugins/dp/dp_plugin.mllib b/plugins/dp/dp_plugin.mllib
index adb9721a1..63252d6a2 100644
--- a/plugins/dp/dp_plugin.mllib
+++ b/plugins/dp/dp_plugin.mllib
@@ -1,6 +1,5 @@
Dp_why
Dp_zenon
Dp
-Dp_gappa
G_dp
Dp_plugin_mod
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 3538f6342..8aeff61e6 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -151,11 +151,6 @@ let showind (id:identifier) =
exception Found of int
(* Array scanning *)
-let array_find (arr: 'a array) (pred: int -> 'a -> bool): int option =
- try
- for i=0 to Array.length arr - 1 do if pred i (arr.(i)) then raise (Found i) done;
- None
- with Found i -> Some i
let array_prfx (arr: 'a array) (pred: int -> 'a -> bool): int =
try
@@ -941,7 +936,7 @@ let merge (id1:identifier) (id2:identifier) (args1:identifier array)
as above: vars may be linked inside args2?? *)
Array.mapi
(fun i c ->
- match array_find args1 (fun i x -> x=c) with
+ match array_find_i (fun i x -> x=c) args1 with
| Some j -> Linked j
| None -> Unlinked)
args2 in
diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml
index 627cd517c..261bb0029 100644
--- a/plugins/interface/xlate.ml
+++ b/plugins/interface/xlate.ml
@@ -2145,8 +2145,8 @@ let rec xlate_vernac =
CT_coercion (local_opt, id_opt, xlate_ident id1,
xlate_class id2, xlate_class id3)
- (* Type Classes *)
- | VernacDeclareInstance _|VernacContext _|
+ (* Type Classes *)
+ | VernacDeclareInstance _ | VernacDeclareClass _ | VernacContext _ |
VernacInstance (_, _, _, _, _) ->
xlate_error "TODO: Type Classes commands"
diff --git a/plugins/subtac/equations.ml4 b/plugins/subtac/equations.ml4
deleted file mode 100644
index ca4445cc2..000000000
--- a/plugins/subtac/equations.ml4
+++ /dev/null
@@ -1,1149 +0,0 @@
-(* -*- compile-command: "make -C ../.. bin/coqtop.byte" -*- *)
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(*i camlp4deps: "parsing/grammar.cma" i*)
-(*i camlp4use: "pa_extend.cmo" i*)
-
-(* $Id$ *)
-
-open Cases
-open Util
-open Names
-open Nameops
-open Term
-open Termops
-open Declarations
-open Inductiveops
-open Environ
-open Sign
-open Reductionops
-open Typeops
-open Type_errors
-
-open Rawterm
-open Retyping
-open Pretype_errors
-open Evarutil
-open Evarconv
-open List
-open Libnames
-
-type pat =
- | PRel of int
- | PCstr of constructor * pat list
- | PInac of constr
-
-let coq_inacc = lazy (Coqlib.gen_constant "equations" ["Program";"Equality"] "inaccessible_pattern")
-
-let mkInac env c =
- mkApp (Lazy.force coq_inacc, [| Typing.type_of env Evd.empty c ; c |])
-
-let rec constr_of_pat ?(inacc=true) env = function
- | PRel i -> mkRel i
- | PCstr (c, p) ->
- let c' = mkConstruct c in
- mkApp (c', Array.of_list (constrs_of_pats ~inacc env p))
- | PInac r ->
- if inacc then try mkInac env r with _ -> r else r
-
-and constrs_of_pats ?(inacc=true) env l = map (constr_of_pat ~inacc env) l
-
-let rec pat_vars = function
- | PRel i -> Intset.singleton i
- | PCstr (c, p) -> pats_vars p
- | PInac _ -> Intset.empty
-
-and pats_vars l =
- fold_left (fun vars p ->
- let pvars = pat_vars p in
- let inter = Intset.inter pvars vars in
- if inter = Intset.empty then
- Intset.union pvars vars
- else error ("Non-linear pattern: variable " ^
- string_of_int (Intset.choose inter) ^ " appears twice"))
- Intset.empty l
-
-let rec pats_of_constrs l = map pat_of_constr l
-and pat_of_constr c =
- match kind_of_term c with
- | Rel i -> PRel i
- | App (f, [| a ; c |]) when eq_constr f (Lazy.force coq_inacc) ->
- PInac c
- | App (f, args) when isConstruct f ->
- PCstr (destConstruct f, pats_of_constrs (Array.to_list args))
- | Construct f -> PCstr (f, [])
- | _ -> PInac c
-
-let inaccs_of_constrs l = map (fun x -> PInac x) l
-
-exception Conflict
-
-let rec pmatch p c =
- match p, c with
- | PRel i, t -> [i, t]
- | PCstr (c, pl), PCstr (c', pl') when c = c' -> pmatches pl pl'
- | PInac _, _ -> []
- | _, PInac _ -> []
- | _, _ -> raise Conflict
-
-and pmatches pl l =
- match pl, l with
- | [], [] -> []
- | hd :: tl, hd' :: tl' ->
- pmatch hd hd' @ pmatches tl tl'
- | _ -> raise Conflict
-
-let pattern_matches pl l = try Some (pmatches pl l) with Conflict -> None
-
-let rec pinclude p c =
- match p, c with
- | PRel i, t -> true
- | PCstr (c, pl), PCstr (c', pl') when c = c' -> pincludes pl pl'
- | PInac _, _ -> true
- | _, PInac _ -> true
- | _, _ -> false
-
-and pincludes pl l =
- match pl, l with
- | [], [] -> true
- | hd :: tl, hd' :: tl' ->
- pinclude hd hd' && pincludes tl tl'
- | _ -> false
-
-let pattern_includes pl l = pincludes pl l
-
-(** Specialize by a substitution. *)
-
-let subst_tele s = replace_vars (List.map (fun (id, _, t) -> id, t) s)
-
-let subst_rel_subst k s c =
- let rec aux depth c =
- match kind_of_term c with
- | Rel n ->
- let k = n - depth in
- if k >= 0 then
- try lift depth (snd (assoc k s))
- with Not_found -> c
- else c
- | _ -> map_constr_with_binders succ aux depth c
- in aux k c
-
-let subst_context s ctx =
- let (_, ctx') = fold_right
- (fun (id, b, t) (k, ctx') ->
- (succ k, (id, Option.map (subst_rel_subst k s) b, subst_rel_subst k s t) :: ctx'))
- ctx (0, [])
- in ctx'
-
-let subst_rel_context k cstr ctx =
- let (_, ctx') = fold_right
- (fun (id, b, t) (k, ctx') ->
- (succ k, (id, Option.map (substnl [cstr] k) b, substnl [cstr] k t) :: ctx'))
- ctx (k, [])
- in ctx'
-
-let rec lift_pat n k p =
- match p with
- | PRel i ->
- if i >= k then PRel (i + n)
- else p
- | PCstr(c, pl) -> PCstr (c, lift_pats n k pl)
- | PInac r -> PInac (liftn n k r)
-
-and lift_pats n k = map (lift_pat n k)
-
-let rec subst_pat env k t p =
- match p with
- | PRel i ->
- if i = k then t
- else if i > k then PRel (pred i)
- else p
- | PCstr(c, pl) ->
- PCstr (c, subst_pats env k t pl)
- | PInac r -> PInac (substnl [constr_of_pat ~inacc:false env t] (pred k) r)
-
-and subst_pats env k t = map (subst_pat env k t)
-
-let rec specialize s p =
- match p with
- | PRel i ->
- if mem_assoc i s then
- let b, t = assoc i s in
- if b then PInac t
- else PRel (destRel t)
- else p
- | PCstr(c, pl) ->
- PCstr (c, specialize_pats s pl)
- | PInac r -> PInac (specialize_constr s r)
-
-and specialize_constr s c = subst_rel_subst 0 s c
-and specialize_pats s = map (specialize s)
-
-let specialize_patterns = function
- | [] -> fun p -> p
- | s -> specialize_pats s
-
-let specialize_rel_context s ctx =
- snd (fold_right (fun (n, b, t) (k, ctx) ->
- (succ k, (n, Option.map (subst_rel_subst k s) b, subst_rel_subst k s t) :: ctx))
- ctx (0, []))
-
-let lift_contextn n k sign =
- let rec liftrec k = function
- | (na,c,t)::sign ->
- (na,Option.map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign)
- | [] -> []
- in
- liftrec (rel_context_length sign + k) sign
-
-type program =
- signature * clause list
-
-and signature = identifier * rel_context * constr
-
-and clause = lhs * (constr, int) rhs
-
-and lhs = rel_context * identifier * pat list
-
-and ('a, 'b) rhs =
- | Program of 'a
- | Empty of 'b
-
-type splitting =
- | Compute of clause
- | Split of lhs * int * inductive_family *
- unification_result array * splitting option array
-
-and unification_result =
- rel_context * int * constr * pat * substitution option
-
-and substitution = (int * (bool * constr)) list
-
-type problem = identifier * lhs
-
-let rels_of_tele tele = rel_list 0 (List.length tele)
-
-let patvars_of_tele tele = map (fun c -> PRel (destRel c)) (rels_of_tele tele)
-
-let split_solves split prob =
- match split with
- | Compute (lhs, rhs) -> lhs = prob
- | Split (lhs, id, indf, us, ls) -> lhs = prob
-
-let ids_of_constr c =
- let rec aux vars c =
- match kind_of_term c with
- | Var id -> Idset.add id vars
- | _ -> fold_constr aux vars c
- in aux Idset.empty c
-
-let ids_of_constrs =
- fold_left (fun acc x -> Idset.union (ids_of_constr x) acc) Idset.empty
-
-let idset_of_list =
- fold_left (fun s x -> Idset.add x s) Idset.empty
-
-let intset_of_list =
- fold_left (fun s x -> Intset.add x s) Intset.empty
-
-let solves split (delta, id, pats as prob) =
- split_solves split prob &&
- Intset.equal (pats_vars pats) (intset_of_list (map destRel (rels_of_tele delta)))
-
-let check_judgment ctx c t =
- ignore(Typing.check (push_rel_context ctx (Global.env ())) Evd.empty c t); true
-
-let check_context env ctx =
- fold_right
- (fun (_, _, t as decl) env ->
- ignore(Typing.sort_of env Evd.empty t); push_rel decl env)
- ctx env
-
-let split_context n c =
- let after, before = list_chop n c in
- match before with
- | hd :: tl -> after, hd, tl
- | [] -> raise (Invalid_argument "split_context")
-
-let split_tele n (ctx : rel_context) =
- let rec aux after n l =
- match n, l with
- | 0, decl :: before -> before, decl, List.rev after
- | n, decl :: before -> aux (decl :: after) (pred n) before
- | _ -> raise (Invalid_argument "split_tele")
- in aux [] n ctx
-
-let rec add_var_subst env subst n c =
- if mem_assoc n subst then
- let t = assoc n subst in
- if eq_constr t c then subst
- else unify env subst t c
- else
- let rel = mkRel n in
- if rel = c then subst
- else if dependent rel c then raise Conflict
- else (n, c) :: subst
-
-and unify env subst x y =
- match kind_of_term x, kind_of_term y with
- | Rel n, _ -> add_var_subst env subst n y
- | _, Rel n -> add_var_subst env subst n x
- | App (c, l), App (c', l') when eq_constr c c' ->
- unify_constrs env subst (Array.to_list l) (Array.to_list l')
- | _, _ -> if eq_constr x y then subst else raise Conflict
-
-and unify_constrs (env : env) subst l l' =
- if List.length l = List.length l' then
- fold_left2 (unify env) subst l l'
- else raise Conflict
-
-let fold_rel_context_with_binders f ctx init =
- snd (List.fold_right (fun decl (depth, acc) ->
- (succ depth, f depth decl acc)) ctx (0, init))
-
-let dependent_rel_context (ctx : rel_context) k =
- fold_rel_context_with_binders
- (fun depth (n,b,t) acc ->
- let r = mkRel (depth + k) in
- acc || dependent r t ||
- (match b with
- | Some b -> dependent r b
- | None -> false))
- ctx false
-
-let liftn_between n k p c =
- let rec aux depth c = match kind_of_term c with
- | Rel i ->
- if i <= depth then c
- else if i-depth > p then c
- else mkRel (i - n)
- | _ -> map_constr_with_binders succ aux depth c
- in aux k c
-
-let liftn_rel_context n k sign =
- let rec liftrec k = function
- | (na,c,t)::sign ->
- (na,Option.map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign)
- | [] -> []
- in
- liftrec (k + rel_context_length sign) sign
-
-let substnl_rel_context n l =
- map_rel_context_with_binders (fun k -> substnl l (n+k-1))
-
-let reduce_rel_context (ctx : rel_context) (subst : (int * (bool * constr)) list) =
- let _, s, ctx' =
- fold_left (fun (k, s, ctx') (n, b, t as decl) ->
- match b with
- | None -> (succ k, mkRel k :: s, ctx' @ [decl])
- | Some t -> (k, lift (pred k) t :: map (substnl [t] (pred k)) s, subst_rel_context 0 t ctx'))
- (1, [], []) ctx
- in
- let s = rev s in
- let s' = map (fun (korig, (b, knew)) -> korig, (b, substl s knew)) subst in
- s', ctx'
-
-(* Compute the transitive closure of the dependency relation for a term in a context *)
-
-let rec dependencies_of_rel ctx k =
- let (n,b,t) = nth ctx (pred k) in
- let b = Option.map (lift k) b and t = lift k t in
- let bdeps = match b with Some b -> dependencies_of_term ctx b | None -> Intset.empty in
- Intset.union (Intset.singleton k) (Intset.union bdeps (dependencies_of_term ctx t))
-
-and dependencies_of_term ctx t =
- let rels = free_rels t in
- Intset.fold (fun i -> Intset.union (dependencies_of_rel ctx i)) rels Intset.empty
-
-let subst_telescope k cstr ctx =
- let (_, ctx') = fold_left
- (fun (k, ctx') (id, b, t) ->
- (succ k, (id, Option.map (substnl [cstr] k) b, substnl [cstr] k t) :: ctx'))
- (k, []) ctx
- in rev ctx'
-
-let lift_telescope n k sign =
- let rec liftrec k = function
- | (na,c,t)::sign ->
- (na,Option.map (liftn n k) c,liftn n k t)::(liftrec (succ k) sign)
- | [] -> []
- in liftrec k sign
-
-type ('a,'b) either = Inl of 'a | Inr of 'b
-
-let strengthen (ctx : rel_context) (t : constr) : rel_context * rel_context * (int * (int, int) either) list =
- let rels = dependencies_of_term ctx t in
- let len = length ctx in
- let nbdeps = Intset.cardinal rels in
- let lifting = len - nbdeps in (* Number of variables not linked to t *)
- let rec aux k n acc m rest s = function
- | decl :: ctx' ->
- if Intset.mem k rels then
- let rest' = subst_telescope 0 (mkRel (nbdeps + lifting - pred m)) rest in
- aux (succ k) (succ n) (decl :: acc) m rest' ((k, Inl n) :: s) ctx'
- else aux (succ k) n (subst_telescope 0 mkProp acc) (succ m) (decl :: rest) ((k, Inr m) :: s) ctx'
- | [] -> rev acc, rev rest, s
- in aux 1 1 [] 1 [] [] ctx
-
-let merge_subst (ctx', rest, s) =
- let lenrest = length rest in
- map (function (k, Inl x) -> (k, (false, mkRel (x + lenrest))) | (k, Inr x) -> k, (false, mkRel x)) s
-
-(* let simplify_subst s = *)
-(* fold_left (fun s (k, t) -> *)
-(* match kind_of_term t with *)
-(* | Rel n when n = k -> s *)
-(* | _ -> (k, t) :: s) *)
-(* [] s *)
-
-let compose_subst s' s =
- map (fun (k, (b, t)) -> (k, (b, specialize_constr s' t))) s
-
-let substitute_in_ctx n c ctx =
- let rec aux k after = function
- | [] -> []
- | (name, b, t as decl) :: before ->
- if k = n then rev after @ (name, Some c, t) :: before
- else aux (succ k) (decl :: after) before
- in aux 1 [] ctx
-
-let rec reduce_subst (ctx : rel_context) (substacc : (int * (bool * constr)) list) (cursubst : (int * (bool * constr)) list) =
- match cursubst with
- | [] -> ctx, substacc
- | (k, (b, t)) :: rest ->
- if t = mkRel k then reduce_subst ctx substacc rest
- else if noccur_between 1 k t then
- (* The term to substitute refers only to previous variables. *)
- let t' = lift (-k) t in
- let ctx' = substitute_in_ctx k t' ctx in
- reduce_subst ctx' substacc rest
- else (* The term refers to variables declared after [k], so we have
- to move these dependencies before [k]. *)
- let (minctx, ctxrest, subst as str) = strengthen ctx t in
- match assoc k subst with
- | Inl _ -> error "Occurs check in substituted_context"
- | Inr k' ->
- let s = merge_subst str in
- let ctx' = ctxrest @ minctx in
- let rest' =
- let substsubst (k', (b, t')) =
- match kind_of_term (snd (assoc k' s)) with
- | Rel k'' -> (k'', (b, specialize_constr s t'))
- | _ -> error "Non-variable substituted for variable by strenghtening"
- in map substsubst ((k, (b, t)) :: rest)
- in
- reduce_subst ctx' (compose_subst s substacc) rest' (* (compose_subst s ((k, (b, t)) :: rest)) *)
-
-
-let substituted_context (subst : (int * constr) list) (ctx : rel_context) =
- let _, subst =
- fold_left (fun (k, s) _ ->
- try let t = assoc k subst in
- (succ k, (k, (true, t)) :: s)
- with Not_found ->
- (succ k, ((k, (false, mkRel k)) :: s)))
- (1, []) ctx
- in
- let ctx', subst' = reduce_subst ctx subst subst in
- reduce_rel_context ctx' subst'
-
-let unify_type before ty =
- try
- let envb = push_rel_context before (Global.env()) in
- let IndType (indf, args) = find_rectype envb Evd.empty ty in
- let ind, params = dest_ind_family indf in
- let vs = map (Reduction.whd_betadeltaiota envb) args in
- let cstrs = Inductiveops.arities_of_constructors envb ind in
- let cstrs =
- Array.mapi (fun i ty ->
- let ty = prod_applist ty params in
- let ctx, ty = decompose_prod_assum ty in
- let ctx, ids =
- let ids = ids_of_rel_context ctx in
- fold_right (fun (n, b, t as decl) (acc, ids) ->
- match n with Name _ -> (decl :: acc), ids
- | Anonymous -> let id = next_name_away Anonymous ids in
- ((Name id, b, t) :: acc), (id :: ids))
- ctx ([], ids)
- in
- let env' = push_rel_context ctx (Global.env ()) in
- let IndType (indf, args) = find_rectype env' Evd.empty ty in
- let ind, params = dest_ind_family indf in
- let constr = applist (mkConstruct (ind, succ i), params @ rels_of_tele ctx) in
- let constrpat = PCstr ((ind, succ i), inaccs_of_constrs params @ patvars_of_tele ctx) in
- env', ctx, constr, constrpat, (* params @ *)args)
- cstrs
- in
- let res =
- Array.map (fun (env', ctxc, c, cpat, us) ->
- let _beforelen = length before and ctxclen = length ctxc in
- let fullctx = ctxc @ before in
- try
- let fullenv = push_rel_context fullctx (Global.env ()) in
- let vs' = map (lift ctxclen) vs in
- let subst = unify_constrs fullenv [] vs' us in
- let subst', ctx' = substituted_context subst fullctx in
- (ctx', ctxclen, c, cpat, Some subst')
- with Conflict ->
- (fullctx, ctxclen, c, cpat, None)) cstrs
- in Some (res, indf)
- with Not_found -> (* not an inductive type *)
- None
-
-let rec id_of_rel n l =
- match n, l with
- | 0, (Name id, _, _) :: tl -> id
- | n, _ :: tl -> id_of_rel (pred n) tl
- | _, _ -> raise (Invalid_argument "id_of_rel")
-
-let constrs_of_lhs ?(inacc=true) env (ctx, _, pats) =
- constrs_of_pats ~inacc (push_rel_context ctx env) pats
-
-let rec valid_splitting (f, delta, t, pats) tree =
- split_solves tree (delta, f, pats) &&
- valid_splitting_tree (f, delta, t) tree
-
-and valid_splitting_tree (f, delta, t) = function
- | Compute (lhs, Program rhs) ->
- let subst = constrs_of_lhs ~inacc:false (Global.env ()) lhs in
- ignore(check_judgment (pi1 lhs) rhs (substl subst t)); true
-
- | Compute ((ctx, id, lhs), Empty split) ->
- let before, (x, _, ty), after = split_context split ctx in
- let unify =
- match unify_type before ty with
- | Some (unify, _) -> unify
- | None -> assert false
- in
- array_for_all (fun (_, _, _, _, x) -> x = None) unify
-
- | Split ((ctx, id, lhs), rel, indf, unifs, ls) ->
- let before, (id, _, ty), after = split_tele (pred rel) ctx in
- let unify, indf' = Option.get (unify_type before ty) in
- assert(indf = indf');
- if not (array_exists (fun (_, _, _, _, x) -> x <> None) unify) then false
- else
- let ok, splits =
- Array.fold_left (fun (ok, splits as acc) (ctx', ctxlen, cstr, cstrpat, subst) ->
- match subst with
- | None -> acc
- | Some subst ->
-(* let env' = push_rel_context ctx' (Global.env ()) in *)
-(* let ctx_correct = *)
-(* ignore(check_context env' (subst_context subst ctxc)); *)
-(* ignore(check_context env' (subst_context subst before)); *)
-(* true *)
-(* in *)
- let newdelta =
- subst_context subst (subst_rel_context 0 cstr
- (lift_contextn ctxlen 0 after)) @ before in
- let liftpats = lift_pats ctxlen rel lhs in
- let newpats = specialize_patterns subst (subst_pats (Global.env ()) rel cstrpat liftpats) in
- (ok, (f, newdelta, newpats) :: splits))
- (true, []) unify
- in
- let subst = List.map2 (fun (id, _, _) x -> out_name id, x) delta
- (constrs_of_pats ~inacc:false (Global.env ()) lhs)
- in
- let t' = replace_vars subst t in
- ok && for_all
- (fun (f, delta', pats') ->
- array_exists (function None -> false | Some tree -> valid_splitting (f, delta', t', pats') tree) ls) splits
-
-let valid_tree (f, delta, t) tree =
- valid_splitting (f, delta, t, patvars_of_tele delta) tree
-
-let is_constructor c =
- match kind_of_term (fst (decompose_app c)) with
- | Construct _ -> true
- | _ -> false
-
-let find_split (_, _, curpats : lhs) (_, _, patcs : lhs) =
- let rec find_split_pat curpat patc =
- match patc with
- | PRel _ -> None
- | PCstr (f, args) ->
- (match curpat with
- | PCstr (f', args') when f = f' -> (* Already split at this level, continue *)
- find_split_pats args' args
- | PRel i -> (* Split on i *) Some i
- | PInac c when isRel c -> Some (destRel c)
- | _ -> None)
- | PInac _ -> None
-
- and find_split_pats curpats patcs =
- assert(List.length curpats = List.length patcs);
- fold_left2 (fun acc ->
- match acc with
- | None -> find_split_pat | _ -> fun _ _ -> acc)
- None curpats patcs
- in find_split_pats curpats patcs
-
-open Pp
-open Termops
-
-let pr_constr_pat env c =
- let pr = print_constr_env env c in
- match kind_of_term c with
- | App _ -> str "(" ++ pr ++ str ")"
- | _ -> pr
-
-let pr_pat env c =
- try
- let patc = constr_of_pat env c in
- try pr_constr_pat env patc with _ -> str"pr_constr_pat raised an exception"
- with _ -> str"constr_of_pat raised an exception"
-
-let pr_context env c =
- let pr_decl (id,b,_) =
- let bstr = match b with Some b -> str ":=" ++ spc () ++ print_constr_env env b | None -> mt() in
- let idstr = match id with Name id -> pr_id id | Anonymous -> str"_" in
- idstr ++ bstr
- in
- prlist_with_sep pr_spc pr_decl (List.rev c)
-(* Printer.pr_rel_context env c *)
-
-let pr_lhs env (delta, f, patcs) =
- let env = push_rel_context delta env in
- let ctx = pr_context env delta in
- (if delta = [] then ctx else str "[" ++ ctx ++ str "]" ++ spc ())
- ++ pr_id f ++ spc () ++ prlist_with_sep spc (pr_pat env) patcs
-
-let pr_rhs env = function
- | Empty var -> spc () ++ str ":=!" ++ spc () ++ print_constr_env env (mkRel var)
- | Program rhs -> spc () ++ str ":=" ++ spc () ++ print_constr_env env rhs
-
-let pr_clause env (lhs, rhs) =
- pr_lhs env lhs ++
- (let env' = push_rel_context (pi1 lhs) env in
- pr_rhs env' rhs)
-
-(* let pr_splitting env = function *)
-(* | Compute cl -> str "Compute " ++ pr_clause env cl *)
-(* | Split (lhs, n, indf, results, splits) -> *)
-
-(* let pr_unification_result (ctx, n, c, pat, subst) = *)
-
-(* unification_result array * splitting option array *)
-
-let pr_clauses env =
- prlist_with_sep fnl (pr_clause env)
-
-let lhs_includes (delta, _, patcs : lhs) (delta', _, patcs' : lhs) =
- pattern_includes patcs patcs'
-
-let lhs_matches (delta, _, patcs : lhs) (delta', _, patcs' : lhs) =
- pattern_matches patcs patcs'
-
-let rec split_on env var (delta, f, curpats as lhs) clauses =
- let before, (id, _, ty), after = split_tele (pred var) delta in
- let unify, indf =
- match unify_type before ty with
- | Some r -> r
- | None -> assert false (* We decided... so it better be inductive *)
- in
- let clauses = ref clauses in
- let splits =
- Array.map (fun (ctx', ctxlen, cstr, cstrpat, s) ->
- match s with
- | None -> None
- | Some s ->
- (* ctx' |- s cstr, s cstrpat *)
- let newdelta =
- subst_context s (subst_rel_context 0 cstr
- (lift_contextn ctxlen 1 after)) @ ctx' in
- let liftpats =
- (* delta |- curpats -> before; ctxc; id; after |- liftpats *)
- lift_pats ctxlen (succ var) curpats
- in
- let liftpat = (* before; ctxc |- cstrpat -> before; ctxc; after |- liftpat *)
- lift_pat (pred var) 1 cstrpat
- in
- let substpat = (* before; ctxc; after |- liftpats[id:=liftpat] *)
- subst_pats env var liftpat liftpats
- in
- let lifts = (* before; ctxc |- s : newdelta ->
- before; ctxc; after |- lifts : newdelta ; after *)
- map (fun (k,(b,x)) -> (pred var + k, (b, lift (pred var) x))) s
- in
- let newpats = specialize_patterns lifts substpat in
- let newlhs = (newdelta, f, newpats) in
- let matching, rest =
- fold_right (fun (lhs, rhs as clause) (matching, rest) ->
- if lhs_includes newlhs lhs then
- (clause :: matching, rest)
- else (matching, clause :: rest))
- !clauses ([], [])
- in
- clauses := rest;
- if matching = [] then (
- (* Try finding a splittable variable *)
- let (id, _) =
- fold_right (fun (id, _, ty as decl) (accid, ctx) ->
- match accid with
- | Some _ -> (accid, ctx)
- | None ->
- match unify_type ctx ty with
- | Some (unify, indf) ->
- if array_for_all (fun (_, _, _, _, x) -> x = None) unify then
- (Some id, ctx)
- else (None, decl :: ctx)
- | None -> (None, decl :: ctx))
- newdelta (None, [])
- in
- match id with
- | None ->
- errorlabstrm "deppat"
- (str "Non-exhaustive pattern-matching, no clause found for:" ++ fnl () ++
- pr_lhs env newlhs)
- | Some id ->
- Some (Compute (newlhs, Empty (fst (lookup_rel_id (out_name id) newdelta))))
- ) else (
- let splitting = make_split_aux env newlhs matching in
- Some splitting))
- unify
- in
-(* if !clauses <> [] then *)
-(* errorlabstrm "deppat" *)
-(* (str "Impossible clauses:" ++ fnl () ++ pr_clauses env !clauses); *)
- Split (lhs, var, indf, unify, splits)
-
-and make_split_aux env lhs clauses =
- let split =
- fold_left (fun acc (lhs', rhs) ->
- match acc with
- | None -> find_split lhs lhs'
- | _ -> acc) None clauses
- in
- match split with
- | Some var -> split_on env var lhs clauses
- | None ->
- (match clauses with
- | [] -> error "No clauses left"
- | [(lhs', rhs)] ->
- (* No need to split anymore, fix the environments so that they are correctly aligned. *)
- (match lhs_matches lhs' lhs with
- | Some s ->
- let s = map (fun (x, p) -> x, (true, constr_of_pat ~inacc:false env p)) s in
- let rhs' = match rhs with
- | Program c -> Program (specialize_constr s c)
- | Empty i -> Empty (destRel (snd (assoc i s)))
- in Compute ((pi1 lhs, pi2 lhs, specialize_patterns s (pi3 lhs')), rhs')
- | None -> anomaly "Non-matching clauses at a leaf of the splitting tree")
- | _ ->
- errorlabstrm "make_split_aux"
- (str "Overlapping clauses:" ++ fnl () ++ pr_clauses env clauses))
-
-let make_split env (f, delta, t) clauses =
- make_split_aux env (delta, f, patvars_of_tele delta) clauses
-
-open Evd
-open Evarutil
-
-let lift_substitution n s = map (fun (k, x) -> (k + n, x)) s
-let map_substitution s t = map (subst_rel_subst 0 s) t
-
-let term_of_tree status isevar env (i, delta, ty) ann tree =
-(* let envrec = match ann with *)
-(* | None -> [] *)
-(* | Some (loc, i) -> *)
-(* let (n, t) = lookup_rel_id i delta in *)
-(* let t' = lift n t in *)
-
-
-(* in *)
- let rec aux = function
- | Compute ((ctx, _, pats as lhs), Program rhs) ->
- let ty' = substl (rev (constrs_of_lhs ~inacc:false env lhs)) ty in
- let body = it_mkLambda_or_LetIn rhs ctx and typ = it_mkProd_or_LetIn ty' ctx in
- mkCast(body, DEFAULTcast, typ), typ
-
- | Compute ((ctx, _, pats as lhs), Empty split) ->
- let ty' = substl (rev (constrs_of_lhs ~inacc:false env lhs)) ty in
- let split = (Name (id_of_string "split"),
- Some (Class_tactics.coq_nat_of_int (1 + (length ctx - split))),
- Lazy.force Class_tactics.coq_nat)
- in
- let ty' = it_mkProd_or_LetIn ty' ctx in
- let let_ty' = mkLambda_or_LetIn split (lift 1 ty') in
- let term = e_new_evar isevar env ~src:(dummy_loc, QuestionMark (Define true)) let_ty' in
- term, ty'
-
- | Split ((ctx, _, pats as lhs), rel, indf, unif, sp) ->
- let before, decl, after = split_tele (pred rel) ctx in
- let ty' = substl (rev (constrs_of_lhs ~inacc:false env lhs)) ty in
- let branches =
- array_map2 (fun (ctx', ctxlen, cstr, cstrpat, subst) split ->
- match split with
- | Some s -> aux s
- | None ->
- (* dead code, inversion will find a proof of False by splitting on the rel'th hyp *)
- Class_tactics.coq_nat_of_int rel, Lazy.force Class_tactics.coq_nat)
- unif sp
- in
- let branches_ctx =
- Array.mapi (fun i (br, brt) -> (id_of_string ("m_" ^ string_of_int i), Some br, brt))
- branches
- in
- let n, branches_lets =
- Array.fold_left (fun (n, lets) (id, b, t) ->
- (succ n, (Name id, Option.map (lift n) b, lift n t) :: lets))
- (0, []) branches_ctx
- in
- let liftctx = lift_contextn (Array.length branches) 0 ctx in
- let case =
- let ty = it_mkProd_or_LetIn ty' liftctx in
- let ty = it_mkLambda_or_LetIn ty branches_lets in
- let nbbranches = (Name (id_of_string "branches"),
- Some (Class_tactics.coq_nat_of_int (length branches_lets)),
- Lazy.force Class_tactics.coq_nat)
- in
- let nbdiscr = (Name (id_of_string "target"),
- Some (Class_tactics.coq_nat_of_int (length before)),
- Lazy.force Class_tactics.coq_nat)
- in
- let ty = it_mkLambda_or_LetIn (lift 2 ty) [nbbranches;nbdiscr] in
- let term = e_new_evar isevar env ~src:(dummy_loc, QuestionMark status) ty in
- term
- in
- let casetyp = it_mkProd_or_LetIn ty' ctx in
- mkCast(case, DEFAULTcast, casetyp), casetyp
-
- in aux tree
-
-open Topconstr
-open Constrintern
-open Decl_kinds
-
-type equation = constr_expr * (constr_expr, identifier located) rhs
-
-let locate_reference qid =
- match Nametab.locate_extended qid with
- | TrueGlobal ref -> true
- | SynDef kn -> true
-
-let is_global id =
- try
- locate_reference (qualid_of_ident id)
- with Not_found ->
- false
-
-let is_freevar ids env x =
- try
- if Idset.mem x ids then false
- else
- try ignore(Environ.lookup_named x env) ; false
- with _ -> not (is_global x)
- with _ -> true
-
-let ids_of_patc c ?(bound=Idset.empty) l =
- let found id bdvars l =
- if not (is_freevar bdvars (Global.env ()) (snd id)) then l
- else if List.exists (fun (_, id') -> id' = snd id) l then l
- else id :: l
- in
- let rec aux bdvars l c = match c with
- | CRef (Ident lid) -> found lid bdvars l
- | CNotation (_, "{ _ : _ | _ }", ((CRef (Ident (_, id))) :: _,[])) when not (Idset.mem id bdvars) ->
- fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux (Idset.add id bdvars) l c
- | c -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c
- in aux bound l c
-
-let interp_pats i isevar env impls pat sign recu =
- let bound = Idset.singleton i in
- let vars = ids_of_patc pat ~bound [] in
- let varsctx, env' =
- fold_right (fun (loc, id) (ctx, env) ->
- let decl =
- let ty = e_new_evar isevar env ~src:(loc, BinderType (Name id)) (new_Type ()) in
- (Name id, None, ty)
- in
- decl::ctx, push_rel decl env)
- vars ([], env)
- in
- let pats =
- let patenv = match recu with None -> env' | Some ty -> push_named (i, None, ty) env' in
- let patt, _ = interp_constr_evars_impls ~evdref:isevar patenv ~impls:([],[]) pat in
- match kind_of_term patt with
- | App (m, args) ->
- if not (eq_constr m (mkRel (succ (length varsctx)))) then
- user_err_loc (constr_loc pat, "interp_pats",
- str "Expecting a pattern for " ++ pr_id i)
- else Array.to_list args
- | _ -> user_err_loc (constr_loc pat, "interp_pats",
- str "Error parsing pattern: unnexpected left-hand side")
- in
- isevar := nf_evar_defs !isevar;
- (nf_rel_context_evar ( !isevar) varsctx,
- nf_env_evar ( !isevar) env',
- rev_map (nf_evar ( !isevar)) pats)
-
-let interp_eqn i isevar env impls sign arity recu (pats, rhs) =
- let ctx, env', patcs = interp_pats i isevar env impls pats sign recu in
- let rhs' = match rhs with
- | Program p ->
- let ty = nf_isevar !isevar (substl patcs arity) in
- Program (interp_casted_constr_evars isevar env' ~impls p ty)
- | Empty lid -> Empty (fst (lookup_rel_id (snd lid) ctx))
- in ((ctx, i, pats_of_constrs (rev patcs)), rhs')
-
-open Entries
-
-open Tacmach
-open Tacexpr
-open Tactics
-open Tacticals
-
-let contrib_tactics_path =
- make_dirpath (List.map id_of_string ["Equality";"Program";"Coq"])
-
-let tactics_tac s =
- make_kn (MPfile contrib_tactics_path) (make_dirpath []) (mk_label s)
-
-let equations_tac = lazy
- (Tacinterp.eval_tactic
- (TacArg(TacCall(dummy_loc,
- ArgArg(dummy_loc, tactics_tac "equations"), []))))
-
-let define_by_eqs with_comp i (l,ann) t nt eqs =
- let env = Global.env () in
- let isevar = ref (create_evar_defs Evd.empty) in
- let (env', sign), impls = interp_context_evars isevar env l in
- let arity = interp_type_evars isevar env' t in
- let sign = nf_rel_context_evar ( !isevar) sign in
- let arity = nf_evar ( !isevar) arity in
- let arity =
- if with_comp then
- let compid = add_suffix i "_comp" in
- let ce =
- { const_entry_body = it_mkLambda_or_LetIn arity sign;
- const_entry_type = None;
- const_entry_opaque = false;
- const_entry_boxed = false}
- in
- let c =
- Declare.declare_constant compid (DefinitionEntry ce, IsDefinition Definition)
- in mkApp (mkConst c, rel_vect 0 (length sign))
- else arity
- in
- let env = Global.env () in
- let ty = it_mkProd_or_LetIn arity sign in
- let data = Command.compute_interning_datas env Constrintern.Recursive [] [i] [ty] [impls] in
- let fixdecls = [(Name i, None, ty)] in
- let fixenv = push_rel_context fixdecls env in
- let equations =
- States.with_heavy_rollback (fun () ->
- Option.iter (Command.declare_interning_data data) nt;
- map (interp_eqn i isevar fixenv data sign arity None) eqs) ()
- in
- let sign = nf_rel_context_evar ( !isevar) sign in
- let arity = nf_evar ( !isevar) arity in
- let prob = (i, sign, arity) in
- let fixenv = nf_env_evar ( !isevar) fixenv in
- let fixdecls = nf_rel_context_evar ( !isevar) fixdecls in
- (* let ce = check_evars fixenv Evd.empty !isevar in *)
- (* List.iter (function (_, _, Program rhs) -> ce rhs | _ -> ()) equations; *)
- let is_recursive, env' =
- let occur_eqn ((ctx, _, _), rhs) =
- match rhs with
- | Program c -> dependent (mkRel (succ (length ctx))) c
- | _ -> false
- in if exists occur_eqn equations then true, fixenv else false, env
- in
- let split = make_split env' prob equations in
- (* if valid_tree prob split then *)
- let status = (* if is_recursive then Expand else *) Define false in
- let t, ty = term_of_tree status isevar env' prob ann split in
- let undef = undefined_evars !isevar in
- let t, ty = if is_recursive then
- (it_mkLambda_or_LetIn t fixdecls, it_mkProd_or_LetIn ty fixdecls)
- else t, ty
- in
- let obls, t', ty' =
- Eterm.eterm_obligations env i !isevar ( undef) 0 ~status t ty
- in
- if is_recursive then
- ignore(Subtac_obligations.add_mutual_definitions [(i, t', ty', impls, obls)] []
- ~tactic:(Lazy.force equations_tac)
- (Command.IsFixpoint [None, CStructRec]))
- else
- ignore(Subtac_obligations.add_definition
- ~implicits:impls i t' ty' ~tactic:(Lazy.force equations_tac) obls)
-
-module Gram = Pcoq.Gram
-module Vernac = Pcoq.Vernac_
-module Tactic = Pcoq.Tactic
-
-module DeppatGram =
-struct
- let gec s = Gram.Entry.create ("Deppat."^s)
-
- let deppat_equations : equation list Gram.Entry.e = gec "deppat_equations"
-
- let binders_let2 : (local_binder list * (identifier located option * recursion_order_expr)) Gram.Entry.e = gec "binders_let2"
-
-(* let where_decl : decl_notation Gram.Entry.e = gec "where_decl" *)
-
-end
-
-open Rawterm
-open DeppatGram
-open Util
-open Pcoq
-open Prim
-open Constr
-open G_vernac
-
-GEXTEND Gram
- GLOBAL: (* deppat_gallina_loc *) deppat_equations binders_let2;
-
- deppat_equations:
- [ [ l = LIST1 equation SEP ";" -> l ] ]
- ;
-
- binders_let2:
- [ [ l = binders_let_fixannot -> l ] ]
- ;
-
- equation:
- [ [ c = Constr.lconstr; r=rhs -> (c, r) ] ]
- ;
-
- rhs:
- [ [ ":=!"; id = identref -> Empty id
- |":="; c = Constr.lconstr -> Program c
- ] ]
- ;
-
- END
-
-type 'a deppat_equations_argtype = (equation list, 'a) Genarg.abstract_argument_type
-
-let (wit_deppat_equations : Genarg.tlevel deppat_equations_argtype),
- (globwit_deppat_equations : Genarg.glevel deppat_equations_argtype),
- (rawwit_deppat_equations : Genarg.rlevel deppat_equations_argtype) =
- Genarg.create_arg "deppat_equations"
-
-type 'a binders_let2_argtype = (local_binder list * (identifier located option * recursion_order_expr), 'a) Genarg.abstract_argument_type
-
-let (wit_binders_let2 : Genarg.tlevel binders_let2_argtype),
- (globwit_binders_let2 : Genarg.glevel binders_let2_argtype),
- (rawwit_binders_let2 : Genarg.rlevel binders_let2_argtype) =
- Genarg.create_arg "binders_let2"
-
-type 'a decl_notation_argtype = (Vernacexpr.decl_notation, 'a) Genarg.abstract_argument_type
-
-let (wit_decl_notation : Genarg.tlevel decl_notation_argtype),
- (globwit_decl_notation : Genarg.glevel decl_notation_argtype),
- (rawwit_decl_notation : Genarg.rlevel decl_notation_argtype) =
- Genarg.create_arg "decl_notation"
-
-let equations wc i l t nt eqs =
- try define_by_eqs wc i l t nt eqs
- with e -> msg (Cerrors.explain_exn e)
-
-VERNAC COMMAND EXTEND Define_equations
-| [ "Equations" ident(i) binders_let2(l) ":" lconstr(t) ":=" deppat_equations(eqs)
- decl_notation(nt) ] ->
- [ equations true i l t nt eqs ]
- END
-
-VERNAC COMMAND EXTEND Define_equations2
-| [ "Equations_nocomp" ident(i) binders_let2(l) ":" lconstr(t) ":=" deppat_equations(eqs)
- decl_notation(nt) ] ->
- [ equations false i l t nt eqs ]
-END
-
-let rec int_of_coq_nat c =
- match kind_of_term c with
- | App (f, [| arg |]) -> succ (int_of_coq_nat arg)
- | _ -> 0
-
-let solve_equations_goal destruct_tac tac gl =
- let concl = pf_concl gl in
- let targetn, branchesn, targ, brs, b =
- match kind_of_term concl with
- | LetIn (Name target, targ, _, b) ->
- (match kind_of_term b with
- | LetIn (Name branches, brs, _, b) ->
- target, branches, int_of_coq_nat targ, int_of_coq_nat brs, b
- | _ -> error "Unnexpected goal")
- | _ -> error "Unnexpected goal"
- in
- let branches, b =
- let rec aux n c =
- if n = 0 then [], c
- else match kind_of_term c with
- | LetIn (Name id, br, brt, b) ->
- let rest, b = aux (pred n) b in
- (id, br, brt) :: rest, b
- | _ -> error "Unnexpected goal"
- in aux brs b
- in
- let ids = targetn :: branchesn :: map pi1 branches in
- let cleantac = tclTHEN (intros_using ids) (thin ids) in
- let dotac = tclDO (succ targ) intro in
- let subtacs =
- tclTHENS destruct_tac
- (map (fun (id, br, brt) -> tclTHEN (letin_tac None (Name id) br (Some brt) onConcl) tac) branches)
- in tclTHENLIST [cleantac ; dotac ; subtacs] gl
-
-TACTIC EXTEND solve_equations
- [ "solve_equations" tactic(destruct) tactic(tac) ] -> [ solve_equations_goal (snd destruct) (snd tac) ]
- END
-
-let coq_eq = Lazy.lazy_from_fun Coqlib.build_coq_eq
-let coq_eq_refl = lazy ((Coqlib.build_coq_eq_data ()).Coqlib.refl)
-
-let coq_heq = lazy (Coqlib.coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq")
-let coq_heq_refl = lazy (Coqlib.coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq_refl")
-
-let specialize_hyp id gl =
- let env = pf_env gl in
- let ty = pf_get_hyp_typ gl id in
- let evars = ref (create_evar_defs (project gl)) in
- let rec aux in_eqs acc ty =
- match kind_of_term ty with
- | Prod (_, t, b) ->
- (match kind_of_term t with
- | App (eq, [| eqty; x; y |]) when eq_constr eq (Lazy.force coq_eq) ->
- let pt = mkApp (Lazy.force coq_eq, [| eqty; x; x |]) in
- let p = mkApp (Lazy.force coq_eq_refl, [| eqty; x |]) in
- if e_conv env evars pt t then
- aux true (mkApp (acc, [| p |])) (subst1 p b)
- else error "Unconvertible members of an homogeneous equality"
- | App (heq, [| eqty; x; eqty'; y |]) when eq_constr heq (Lazy.force coq_heq) ->
- let pt = mkApp (Lazy.force coq_heq, [| eqty; x; eqty; x |]) in
- let p = mkApp (Lazy.force coq_heq_refl, [| eqty; x |]) in
- if e_conv env evars pt t then
- aux true (mkApp (acc, [| p |])) (subst1 p b)
- else error "Unconvertible members of an heterogeneous equality"
- | _ ->
- if in_eqs then acc, in_eqs, ty
- else
- let e = e_new_evar evars env t in
- aux false (mkApp (acc, [| e |])) (subst1 e b))
- | t -> acc, in_eqs, ty
- in
- try
- let acc, worked, ty = aux false (mkVar id) ty in
- let ty = Evarutil.nf_isevar !evars ty in
- if worked then
- tclTHENFIRST
- (fun g -> Tacmach.internal_cut true id ty g)
- (exact_no_check (Evarutil.nf_isevar !evars acc)) gl
- else tclFAIL 0 (str "Nothing to do in hypothesis " ++ pr_id id) gl
- with e -> tclFAIL 0 (Cerrors.explain_exn e) gl
-
-TACTIC EXTEND specialize_hyp
-[ "specialize_hypothesis" constr(c) ] -> [
- match kind_of_term c with
- | Var id -> specialize_hyp id
- | _ -> tclFAIL 0 (str "Not an hypothesis") ]
-END
diff --git a/plugins/subtac/eterm.ml b/plugins/subtac/eterm.ml
index 3c947e29c..d9b73109a 100644
--- a/plugins/subtac/eterm.ml
+++ b/plugins/subtac/eterm.ml
@@ -1,4 +1,4 @@
-(* -*- compile-command: "make -C ../.. bin/coqtop.byte" -*- *)
+(* -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *)
(**
- Get types of existentials ;
- Flatten dependency tree (prefix order) ;
@@ -30,13 +30,13 @@ type oblinfo =
ev_chop: int option;
ev_loc: Util.loc;
ev_typ: types;
- ev_tac: Tacexpr.raw_tactic_expr option;
+ ev_tac: tactic option;
ev_deps: Intset.t }
(** Substitute evar references in t using De Bruijn indices,
where n binders were passed through. *)
-let subst_evar_constr evs n t =
+let subst_evar_constr evs n idf t =
let seen = ref Intset.empty in
let transparent = ref Idset.empty in
let evar_info id = List.assoc id evs in
@@ -70,7 +70,7 @@ let subst_evar_constr evs n t =
in
if List.exists (fun x -> match kind_of_term x with Rel n -> List.mem n fixrels | _ -> false) args then
transparent := Idset.add idstr !transparent;
- mkApp (mkVar idstr, Array.of_list args)
+ mkApp (idf idstr, Array.of_list args)
| Fix _ ->
map_constr_with_binders succfix substrec (depth, 1 :: fixrels) c
| _ -> map_constr_with_binders succfix substrec (depth, fixrels) c
@@ -96,14 +96,14 @@ let subst_vars acc n t =
let etype_of_evar evs hyps concl =
let rec aux acc n = function
(id, copt, t) :: tl ->
- let t', s, trans = subst_evar_constr evs n t in
+ let t', s, trans = subst_evar_constr evs n mkVar t in
let t'' = subst_vars acc 0 t' in
let rest, s', trans' = aux (id :: acc) (succ n) tl in
let s' = Intset.union s s' in
let trans' = Idset.union trans trans' in
(match copt with
- Some c ->
- let c', s'', trans'' = subst_evar_constr evs n c in
+ Some c ->
+ let c', s'', trans'' = subst_evar_constr evs n mkVar c in
let c' = subst_vars acc 0 c' in
mkNamedProd_or_LetIn (id, Some c', t'') rest,
Intset.union s'' s',
@@ -111,7 +111,7 @@ let etype_of_evar evs hyps concl =
| None ->
mkNamedProd_or_LetIn (id, None, t'') rest, s', trans')
| [] ->
- let t', s, trans = subst_evar_constr evs n concl in
+ let t', s, trans = subst_evar_constr evs n mkVar concl in
subst_vars acc 0 t', s, trans
in aux [] 0 (rev hyps)
@@ -143,13 +143,33 @@ let evar_dependencies evm ev =
in aux (Intset.singleton ev)
let sort_dependencies evl =
- List.sort (fun (_, _, deps) (_, _, deps') ->
- if Intset.subset deps deps' then (* deps' depends on deps *) -1
- else if Intset.subset deps' deps then 1
- else Intset.compare deps deps')
- evl
-
-let eterm_obligations env name isevars evm fs ?status t ty =
+ let one_step deps ine oute =
+ List.fold_left (fun (ine, oute, acc) (id, _, deps' as d) ->
+ if not (Intset.mem id deps) then
+ if Intset.subset deps' (Intset.add id deps) then
+ (d :: ine, oute, Intset.add id acc)
+ else (ine, d :: oute, acc)
+ else (ine, oute, acc))
+ (ine, [], deps) oute
+ in
+ let rec aux deps evsin evsout =
+ let (evsin, evsout, deps') = one_step deps evsin evsout in
+ if evsout = [] then List.rev evsin
+ else aux deps' evsin evsout
+ in aux Intset.empty [] evl
+
+let map_evar_body f = function
+ | Evar_empty -> Evar_empty
+ | Evar_defined c -> Evar_defined (f c)
+
+open Environ
+
+let map_evar_info f evi =
+ { evi with evar_hyps = val_of_named_context (map_named_context f (named_context_of_val evi.evar_hyps));
+ evar_concl = f evi.evar_concl;
+ evar_body = map_evar_body f evi.evar_body }
+
+let eterm_obligations env name isevars evm fs ?status t ty =
(* 'Serialize' the evars *)
let nc = Environ.named_context env in
let nc_len = Sign.named_context_length nc in
@@ -188,7 +208,8 @@ let eterm_obligations env name isevars evm fs ?status t ty =
let tac = match ev.evar_extra with
| Some t ->
if Dyn.tag t = "tactic" then
- Some (Tacinterp.globTacticIn (Tacinterp.tactic_out t))
+ Some (Tacinterp.interp
+ (Tacinterp.globTacticIn (Tacinterp.tactic_out t)))
else None
| None -> None
in
@@ -199,11 +220,11 @@ let eterm_obligations env name isevars evm fs ?status t ty =
evn []
in
let t', _, transparent = (* Substitute evar refs in the term by variables *)
- subst_evar_constr evts 0 t
+ subst_evar_constr evts 0 mkVar t
in
- let ty, _, _ = subst_evar_constr evts 0 ty in
- let evars =
- List.map (fun (_, info) ->
+ let ty, _, _ = subst_evar_constr evts 0 mkVar ty in
+ let evars =
+ List.map (fun (ev, info) ->
let { ev_name = (_, name); ev_status = status;
ev_loc = loc; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info
in
@@ -211,8 +232,9 @@ let eterm_obligations env name isevars evm fs ?status t ty =
| Define true when Idset.mem name transparent -> Define false
| _ -> status
in name, typ, loc, status, deps, tac) evts
- in Array.of_list (List.rev evars), t', ty
+ in
+ let evnames = List.map (fun (ev, info) -> ev, snd info.ev_name) evts in
+ let evmap f c = pi1 (subst_evar_constr evts 0 f c) in
+ Array.of_list (List.rev evars), (evnames, evmap), t', ty
let mkMetas n = list_tabulate (fun _ -> Evarutil.mk_new_meta ()) n
-
-let etermtac (evm, t) = assert(false) (*eterm evm t None *)
diff --git a/plugins/subtac/eterm.mli b/plugins/subtac/eterm.mli
index 1d1c51266..f45dfa1cc 100644
--- a/plugins/subtac/eterm.mli
+++ b/plugins/subtac/eterm.mli
@@ -22,11 +22,13 @@ val sort_dependencies : (int * evar_info * Intset.t) list -> (int * evar_info *
(* env, id, evars, number of function prototypes to try to clear from
evars contexts, object and type *)
-val eterm_obligations : env -> identifier -> evar_defs -> evar_map -> int ->
- ?status:obligation_definition_status -> constr -> types ->
- (identifier * types * loc * obligation_definition_status * Intset.t *
- Tacexpr.raw_tactic_expr option) array * constr * types
- (* Obl. name, type as product, location of the original evar, associated tactic,
+val eterm_obligations : env -> identifier -> evar_defs -> evar_map -> int ->
+ ?status:obligation_definition_status -> constr -> types ->
+ (identifier * types * loc * obligation_definition_status * Intset.t *
+ tactic option) array
+ (* Existential key, obl. name, type as product, location of the original evar, associated tactic,
status and dependencies as indexes into the array *)
-
-val etermtac : open_constr -> tactic
+ * ((existential_key * identifier) list * ((identifier -> constr) -> constr -> constr)) * constr * types
+ (* Translations from existential identifiers to obligation identifiers
+ and for terms with existentials to closed terms, given a
+ translation from obligation identifiers to constrs, new term, new type *)
diff --git a/plugins/subtac/g_eterm.ml4 b/plugins/subtac/g_eterm.ml4
deleted file mode 100644
index 53ce5b8d6..000000000
--- a/plugins/subtac/g_eterm.ml4
+++ /dev/null
@@ -1,27 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-(**************************************************************************)
-(* *)
-(* Omega: a solver of quantifier-free problems in Presburger Arithmetic *)
-(* *)
-(* Pierre Crégut (CNET, Lannion, France) *)
-(* *)
-(**************************************************************************)
-
-(*i camlp4deps: "parsing/grammar.cma" i*)
-
-(* $Id$ *)
-
-open Eterm
-
-TACTIC EXTEND eterm
- [ "eterm" ] -> [
- (fun gl ->
- let evm = Tacmach.project gl and t = Tacmach.pf_concl gl in
- Eterm.etermtac (evm, t) gl) ]
-END
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 97a929809..85b55f36c 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -51,9 +51,9 @@ open Tacexpr
let solve_tccs_in_type env id isevars evm c typ =
if not (evm = Evd.empty) then
let stmt_id = Nameops.add_suffix id "_stmt" in
- let obls, c', t' = eterm_obligations env stmt_id !isevars evm 0 ~status:Expand c typ in
- match Subtac_obligations.add_definition stmt_id c' typ obls with
- | Subtac_obligations.Defined cst -> constant_value (Global.env())
+ let obls, _, c', t' = eterm_obligations env stmt_id !isevars evm 0 ~status:Expand c typ in
+ match Subtac_obligations.add_definition stmt_id ~term:c' typ obls with
+ | Subtac_obligations.Defined cst -> constant_value (Global.env())
(match cst with ConstRef kn -> kn | _ -> assert false)
| _ ->
errorlabstrm "start_proof"
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index 93b65cd00..211d71a88 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -184,11 +184,10 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
Evarutil.check_evars env Evd.empty !isevars termtype;
let hook vis gr =
let cst = match gr with ConstRef kn -> kn | _ -> assert false in
- let inst = Typeclasses.new_instance k pri global cst in
+ let inst = Typeclasses.new_instance k pri global (ConstRef cst) in
Impargs.declare_manual_implicits false gr ~enriching:false imps;
Typeclasses.add_instance inst
in
- let evm = Subtac_utils.evars_of_term ( !isevars) Evd.empty term in
- let obls, constr, typ = Eterm.eterm_obligations env id !isevars evm 0 term termtype in
- id, Subtac_obligations.add_definition id constr typ ~kind:(Global,false,Instance) ~hook obls
-
+ let evm = Subtac_utils.evars_of_term !isevars Evd.empty term in
+ let obls, _, constr, typ = Eterm.eterm_obligations env id !isevars evm 0 term termtype in
+ id, Subtac_obligations.add_definition id ~term:constr typ ~kind:(Global,false,Instance) ~hook obls
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index 937f7d065..2a31d4e18 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -234,11 +234,6 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
let argtyp, letbinders, make = telescope binders_rel in
let argname = id_of_string "recarg" in
let arg = (Name argname, None, argtyp) in
- let wrapper x =
- if List.length binders_rel > 1 then
- it_mkLambda_or_LetIn (mkApp (x, [|make|])) binders_rel
- else x
- in
let binders = letbinders @ [arg] in
let binders_env = push_rel_context binders_rel env in
let rel = interp_constr isevars env r in
@@ -310,22 +305,46 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
in
let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in
let prop = mkLambda (Name argname, argtyp, top_arity_let) in
- let fix_def =
+ let def =
mkApp (constr_of_global (Lazy.force fix_sub_ref),
[| argtyp ; wf_rel ;
make_existential dummy_loc ~opaque:(Define false) env isevars wf_proof ;
prop ; intern_body_lam |])
in
- let def = wrapper fix_def in
- let typ = it_mkProd_or_LetIn top_arity binders_rel in
+ let hook, recname, typ =
+ if List.length binders_rel > 1 then
+ let name = add_suffix recname "_func" in
+ let hook l gr =
+ let body = it_mkLambda_or_LetIn (mkApp (constr_of_global gr, [|make|])) binders_rel in
+ let ty = it_mkProd_or_LetIn top_arity binders_rel in
+ let ce =
+ { const_entry_body = body;
+ const_entry_type = Some ty;
+ const_entry_opaque = false;
+ const_entry_boxed = false}
+ in
+ let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
+ let gr = ConstRef c in
+ if Impargs.is_implicit_args () || impls <> [] then
+ Impargs.declare_manual_implicits false gr impls
+ in
+ let typ = it_mkProd_or_LetIn top_arity binders in
+ hook, name, typ
+ else
+ let typ = it_mkProd_or_LetIn top_arity binders_rel in
+ let hook l gr =
+ if Impargs.is_implicit_args () || impls <> [] then
+ Impargs.declare_manual_implicits false gr impls
+ in hook, recname, typ
+ in
let _ = isevars := Evarutil.nf_evar_defs !isevars in
let fullcoqc = Evarutil.nf_isevar !isevars def in
let fullctyp = Evarutil.nf_isevar !isevars typ in
let evm = evars_of_term !isevars Evd.empty fullctyp in
let evm = evars_of_term !isevars evm fullcoqc in
let evm = non_instanciated_map env isevars evm in
- let evars, evars_def, evars_typ = Eterm.eterm_obligations env recname !isevars evm 0 fullcoqc fullctyp in
- Subtac_obligations.add_definition recname evars_def evars_typ ~implicits:impls evars
+ let evars, _, evars_def, evars_typ = Eterm.eterm_obligations env recname !isevars evm 0 fullcoqc fullctyp in
+ Subtac_obligations.add_definition recname ~term:evars_def evars_typ evars ~hook
let nf_evar_context isevars ctx =
List.map (fun (n, b, t) ->
@@ -454,7 +473,7 @@ let interp_recursive fixkind l boxed =
in
let evm' = Subtac_utils.evars_of_term evm Evd.empty def in
let evm' = Subtac_utils.evars_of_term evm evm' typ in
- let evars, def, typ = Eterm.eterm_obligations env id isevars evm' recdefs def typ in
+ let evars, _, def, typ = Eterm.eterm_obligations env id isevars evm' recdefs def typ in
(id, def, typ, imps, evars)
in
let defs = list_map4 collect_evars fixnames fixdefs fixtypes fiximps in
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index f617c1008..9b0b39cf8 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -21,6 +21,9 @@ let ppwarn cmd = Pp.warn (str"Program:" ++ cmd)
let pperror cmd = Util.errorlabstrm "Program" cmd
let error s = pperror (str s)
+let reduce =
+ Reductionops.clos_norm_flags Closure.betaiotazeta (Global.env ()) Evd.empty
+
exception NoObligations of identifier option
let explain_no_obligations = function
@@ -28,17 +31,17 @@ let explain_no_obligations = function
| None -> str "No obligations remaining"
type obligation_info = (Names.identifier * Term.types * loc * obligation_definition_status * Intset.t
- * Tacexpr.raw_tactic_expr option) array
+ * tactic option) array
type obligation =
- { obl_name : identifier;
- obl_type : types;
- obl_location : loc;
- obl_body : constr option;
- obl_status : obligation_definition_status;
- obl_deps : Intset.t;
- obl_tac : Tacexpr.raw_tactic_expr option;
- }
+ { obl_name : identifier;
+ obl_type : types;
+ obl_location : loc;
+ obl_body : constr option;
+ obl_status : obligation_definition_status;
+ obl_deps : Intset.t;
+ obl_tac : tactic option;
+ }
type obligations = (obligation array * int)
@@ -105,7 +108,7 @@ let subst_deps expand obls deps t =
Term.replace_vars subst t
let subst_deps_obl obls obl =
- let t' = subst_deps false obls obl.obl_deps obl.obl_type in
+ let t' = subst_deps true obls obl.obl_deps obl.obl_type in
{ obl with obl_type = t' }
module ProgMap = Map.Make(struct type t = identifier let compare = compare end)
@@ -148,15 +151,14 @@ let _ =
let progmap_union = ProgMap.fold ProgMap.add
-let cache (_, (infos, tac)) =
- from_prg := infos;
+let cache (_, tac) =
set_default_tactic tac
-let load (_, (_, tac)) =
+let load (_, tac) =
set_default_tactic tac
-let subst (s, (infos, tac)) =
- (infos, Tacinterp.subst_tactic s tac)
+let subst (s, tac) =
+ Tacinterp.subst_tactic s tac
let (input,output) =
declare_object
@@ -164,17 +166,16 @@ let (input,output) =
cache_function = cache;
load_function = (fun _ -> load);
open_function = (fun _ -> load);
- classify_function = (fun (infos, tac) ->
- if not (ProgMap.is_empty infos) then
+ classify_function = (fun tac ->
+ if not (ProgMap.is_empty !from_prg) then
errorlabstrm "Program" (str "Unsolved obligations when closing module:" ++ spc () ++
prlist_with_sep spc (fun x -> Nameops.pr_id x)
- (map_keys infos));
- Substitute (ProgMap.empty, tac));
+ (map_keys !from_prg));
+ Substitute tac);
subst_function = subst}
let update_state () =
-(* msgnl (str "Updating obligations info"); *)
- Lib.add_anonymous_leaf (input (!from_prg, !default_tactic_expr))
+ Lib.add_anonymous_leaf (input !default_tactic_expr)
let set_default_tactic t =
set_default_tactic t; update_state ()
@@ -195,7 +196,7 @@ let subst_body expand prg =
subst_deps expand obls ints (Termops.refresh_universes prg.prg_type)
let declare_definition prg =
- let body, typ = subst_body false prg in
+ let body, typ = subst_body true prg in
(try trace (str "Declaring: " ++ Ppconstr.pr_id prg.prg_name ++ spc () ++
my_print_constr (Global.env()) body ++ str " : " ++
my_print_constr (Global.env()) prg.prg_type);
@@ -229,8 +230,8 @@ let declare_definition prg =
if Impargs.is_implicit_args () || prg.prg_implicits <> [] then
Impargs.declare_manual_implicits false gr prg.prg_implicits;
print_message (Subtac_utils.definition_message prg.prg_name);
- prg.prg_hook local gr;
progmap_remove prg; update_state ();
+ prg.prg_hook local gr;
gr
open Pp
@@ -256,17 +257,16 @@ let compute_possible_guardness_evidences (n,_) fixbody fixtype =
let ctx = fst (decompose_prod_n_assum m fixtype) in
list_map_i (fun i _ -> i) 0 ctx
-let reduce_fix =
- Reductionops.clos_norm_flags Closure.betaiotazeta (Global.env ()) Evd.empty
-
let declare_mutual_definition l =
let len = List.length l in
let first = List.hd l in
let fixdefs, fixtypes, fiximps =
list_split3
- (List.map (fun x ->
- let subs, typ = (subst_body false x) in
- (strip_lam_n len subs), snd (decompose_prod_n len typ), x.prg_implicits) l)
+ (List.map (fun x ->
+ let subs, typ = (subst_body true x) in
+ let term = snd (Reductionops.splay_lam_n (Global.env ()) Evd.empty len subs) in
+ let typ = snd (Reductionops.splay_prod_n (Global.env ()) Evd.empty len typ) in
+ reduce term, reduce typ, x.prg_implicits) l)
in
(* let fixdefs = List.map reduce_fix fixdefs in *)
let fixkind = Option.get first.prg_fixkind in
@@ -295,36 +295,48 @@ let declare_mutual_definition l =
first.prg_hook local gr;
List.iter progmap_remove l;
update_state (); kn
-
-let declare_obligation obl body =
+
+let declare_obligation prg obl body =
+ let body = reduce body in
+ let ty = reduce obl.obl_type in
match obl.obl_status with
| Expand -> { obl with obl_body = Some body }
| Define opaque ->
- let ce =
+ let opaque = if get_proofs_transparency () then false else opaque in
+ let ce =
{ const_entry_body = body;
- const_entry_type = Some obl.obl_type;
- const_entry_opaque =
- (if get_proofs_transparency () then false
- else opaque) ;
- const_entry_boxed = false}
+ const_entry_type = Some ty;
+ const_entry_opaque = opaque;
+ const_entry_boxed = false}
in
let constant = Declare.declare_constant obl.obl_name
(DefinitionEntry ce,IsProof Property)
in
+ if not opaque then
+ Auto.add_hints false [string_of_id prg.prg_name]
+ (Auto.HintsUnfoldEntry [EvalConstRef constant]);
print_message (Subtac_utils.definition_message obl.obl_name);
{ obl with obl_body = Some (mkConst constant) }
let red = Reductionops.nf_betaiota Evd.empty
let init_prog_info n b t deps fixkind notations obls impls kind hook =
- let obls' =
- Array.mapi
- (fun i (n, t, l, o, d, tac) ->
- debug 2 (str "Adding obligation " ++ int i ++ str " with deps : " ++ str (string_of_intset d));
- { obl_name = n ; obl_body = None;
- obl_location = l; obl_type = red t; obl_status = o;
- obl_deps = d; obl_tac = tac })
- obls
+ let obls', b =
+ match b with
+ | None ->
+ assert(obls = [||]);
+ let n = Nameops.add_suffix n "_obligation" in
+ [| { obl_name = n; obl_body = None;
+ obl_location = dummy_loc; obl_type = t;
+ obl_status = Expand; obl_deps = Intset.empty; obl_tac = None } |],
+ mkVar n
+ | Some b ->
+ Array.mapi
+ (fun i (n, t, l, o, d, tac) ->
+ { obl_name = n ; obl_body = None;
+ obl_location = l; obl_type = red t; obl_status = o;
+ obl_deps = d; obl_tac = tac })
+ obls, b
in
{ prg_name = n ; prg_body = b; prg_type = red t; prg_obligations = (obls', Array.length obls');
prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ;
@@ -348,6 +360,9 @@ let get_prog_err n =
let obligations_solved prg = (snd prg.prg_obligations) = 0
+let all_programs () =
+ ProgMap.fold (fun k p l -> p :: l) !from_prg []
+
type progress =
| Remain of int
| Dependent
@@ -364,13 +379,14 @@ let obligations_message rem =
let update_obls prg obls rem =
let prg' = { prg with prg_obligations = (obls, rem) } in
- from_prg := map_replace prg.prg_name prg' !from_prg;
+ from_prg := map_replace prg.prg_name prg' !from_prg; update_state ();
obligations_message rem;
if rem > 0 then Remain rem
else (
match prg'.prg_deps with
| [] ->
let kn = declare_definition prg' in
+ progmap_remove prg';
Defined kn
| l ->
let progs = List.map (fun x -> ProgMap.find x !from_prg) prg'.prg_deps in
@@ -432,7 +448,11 @@ let rec solve_obligation prg num =
| Define opaque ->
if not opaque && not transparent then error_not_transp ()
else Libnames.constr_of_global gr
- in { obl with obl_body = Some body }
+ in
+ if transparent then
+ Auto.add_hints true [string_of_id prg.prg_name]
+ (Auto.HintsUnfoldEntry [EvalConstRef cst]);
+ { obl with obl_body = Some body }
in
let obls = Array.copy obls in
let _ = obls.(num) <- obl in
@@ -476,11 +496,11 @@ and solve_obligation_by_tac prg obls i tac =
| Some t -> t
| None ->
match obl.obl_tac with
- | Some t -> Tacinterp.interp t
+ | Some t -> t
| None -> !default_tactic
in
let t = Subtac_utils.solve_by_tac (evar_of_obligation obl) tac in
- obls.(i) <- declare_obligation obl t;
+ obls.(i) <- declare_obligation prg obl t;
true
else false
with
@@ -524,8 +544,7 @@ and auto_solve_obligations n tac : progress =
try solve_prg_obligations (get_prog_err n) tac with NoObligations _ -> Dependent
open Pp
-let show_obligations ?(msg=true) n =
- let prg = get_prog_err n in
+let show_obligations_of_prg ?(msg=true) prg =
let n = prg.prg_name in
let obls, rem = prg.prg_obligations in
let showed = ref 5 in
@@ -541,6 +560,14 @@ let show_obligations ?(msg=true) n =
| Some _ -> ())
obls
+let show_obligations ?(msg=true) n =
+ let progs = match n with
+ | None -> all_programs ()
+ | Some n ->
+ try [ProgMap.find n !from_prg]
+ with Not_found -> raise (NoObligations (Some n))
+ in List.iter (show_obligations_of_prg ~msg) progs
+
let show_term n =
let prg = get_prog_err n in
let n = prg.prg_name in
@@ -548,14 +575,13 @@ let show_term n =
my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
++ my_print_constr (Global.env ()) prg.prg_body)
-let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic ?(hook=fun _ _ -> ()) obls =
+let add_definition n ?term t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic ?(hook=fun _ _ -> ()) obls =
Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
- let prg = init_prog_info n b t [] None [] obls implicits kind hook in
+ let prg = init_prog_info n term t [] None [] obls implicits kind hook in
let obls,_ = prg.prg_obligations in
if Array.length obls = 0 then (
Flags.if_verbose ppnl (str ".");
let cst = declare_definition prg in
- from_prg := ProgMap.remove prg.prg_name !from_prg;
Defined cst)
else (
let len = Array.length obls in
@@ -570,7 +596,7 @@ let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) ?(hook=fun
let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
let upd = List.fold_left
(fun acc (n, b, t, imps, obls) ->
- let prg = init_prog_info n b t deps (Some fixkind) notations obls imps kind hook in
+ let prg = init_prog_info n (Some b) t deps (Some fixkind) notations obls imps kind hook in
ProgMap.add n prg acc)
!from_prg l
in
@@ -589,14 +615,17 @@ let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) ?(hook=fun
let admit_obligations n =
let prg = get_prog_err n in
let obls, rem = prg.prg_obligations in
- Array.iteri (fun i x ->
- match x.obl_body with
- None ->
- let x = subst_deps_obl obls x in
- let kn = Declare.declare_constant x.obl_name (ParameterEntry (x.obl_type,false), IsAssumption Conjectural) in
- assumption_message x.obl_name;
- obls.(i) <- { x with obl_body = Some (mkConst kn) }
- | Some _ -> ())
+ Array.iteri
+ (fun i x ->
+ match x.obl_body with
+ | None ->
+ let x = subst_deps_obl obls x in
+ let kn = Declare.declare_constant x.obl_name (ParameterEntry (x.obl_type,false),
+ IsAssumption Conjectural)
+ in
+ assumption_message x.obl_name;
+ obls.(i) <- { x with obl_body = Some (mkConst kn) }
+ | Some _ -> ())
obls;
ignore(update_obls prg obls 0)
diff --git a/plugins/subtac/subtac_obligations.mli b/plugins/subtac/subtac_obligations.mli
index 80d5b9465..04e2371af 100644
--- a/plugins/subtac/subtac_obligations.mli
+++ b/plugins/subtac/subtac_obligations.mli
@@ -6,26 +6,26 @@ open Proof_type
type obligation_info =
(identifier * Term.types * loc *
- obligation_definition_status * Intset.t * Tacexpr.raw_tactic_expr option) array
+ obligation_definition_status * Intset.t * tactic option) array
(* ident, type, location, (opaque or transparent, expand or define),
dependencies, tactic to solve it *)
type progress = (* Resolution status of a program *)
- | Remain of int (* n obligations remaining *)
- | Dependent (* Dependent on other definitions *)
- | Defined of global_reference (* Defined as id *)
-
+ | Remain of int (* n obligations remaining *)
+ | Dependent (* Dependent on other definitions *)
+ | Defined of global_reference (* Defined as id *)
+
val set_default_tactic : Tacexpr.glob_tactic_expr -> unit
val default_tactic : unit -> Proof_type.tactic
val set_proofs_transparency : bool -> unit (* true = All transparent, false = Opaque if possible *)
val get_proofs_transparency : unit -> bool
-val add_definition : Names.identifier -> Term.constr -> Term.types ->
+val add_definition : Names.identifier -> ?term:Term.constr -> Term.types ->
?implicits:(Topconstr.explicitation * (bool * bool * bool)) list ->
?kind:Decl_kinds.definition_kind ->
?tactic:Proof_type.tactic ->
- ?hook:Tacexpr.declaration_hook -> obligation_info -> progress
+ ?hook:(Tacexpr.declaration_hook) -> obligation_info -> progress
type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list
diff --git a/plugins/subtac/subtac_plugin.mllib b/plugins/subtac/subtac_plugin.mllib
index 394a4b30f..a4b9d67e0 100644
--- a/plugins/subtac/subtac_plugin.mllib
+++ b/plugins/subtac/subtac_plugin.mllib
@@ -1,6 +1,5 @@
Subtac_utils
Eterm
-G_eterm
Subtac_errors
Subtac_coercion
Subtac_obligations
@@ -11,5 +10,4 @@ Subtac_command
Subtac_classes
Subtac
G_subtac
-Equations
Subtac_plugin_mod
diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml
index 845710540..11a9fa9f5 100644
--- a/plugins/subtac/subtac_pretyping.ml
+++ b/plugins/subtac/subtac_pretyping.ml
@@ -133,5 +133,5 @@ let subtac_proof kind hook env isevars id bl c tycon =
let evm, coqc, coqt, imps = subtac_process env isevars id bl c tycon in
let evm' = Subtac_utils.evars_of_term evm Evd.empty coqc in
let evm' = Subtac_utils.evars_of_term evm evm' coqt in
- let evars, def, ty = Eterm.eterm_obligations env id !isevars evm' 0 coqc coqt in
- add_definition id def ty ~implicits:imps ~kind ~hook evars
+ let evars, _, def, ty = Eterm.eterm_obligations env id !isevars evm' 0 coqc coqt in
+ add_definition id ~term:def ty ~implicits:imps ~kind ~hook evars
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index 288d3854f..fbe40525b 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -50,6 +50,10 @@ let build_sig () =
let sig_ = lazy (build_sig ())
let fix_proto = lazy (init_constant tactics_module "fix_proto")
+let fix_proto_ref () =
+ match Nametab.global (make_ref "Program.Tactics.fix_proto") with
+ | ConstRef c -> c
+ | _ -> assert false
let eq_ind = lazy (init_constant ["Init"; "Logic"] "eq")
let eq_rec = lazy (init_constant ["Init"; "Logic"] "eq_rec")
@@ -374,7 +378,10 @@ let solve_by_tac evi t =
(fun _ _ -> ());
Pfedit.by (tclCOMPLETE t);
let _,(const,_,_,_) = Pfedit.cook_proof ignore in
- Pfedit.delete_current_proof (); const.Entries.const_entry_body
+ Pfedit.delete_current_proof ();
+ Inductiveops.control_only_guard (Global.env ())
+ const.Entries.const_entry_body;
+ const.Entries.const_entry_body
with e ->
Pfedit.delete_current_proof();
raise e
diff --git a/plugins/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli
index e7ee6c748..81f263cc2 100644
--- a/plugins/subtac/subtac_utils.mli
+++ b/plugins/subtac/subtac_utils.mli
@@ -35,6 +35,7 @@ val build_sig : unit -> coq_sigma_data
val sig_ : coq_sigma_data lazy_t
val fix_proto : constr lazy_t
+val fix_proto_ref : unit -> constant
val eq_ind : constr lazy_t
val eq_rec : constr lazy_t
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 586ad716d..2f5099c1a 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -79,7 +79,7 @@ module Default = struct
| [] -> { uj_val = applist (j_val funj,argl);
uj_type = typ }
| h::restl ->
- (* On devrait pouvoir s'arranger pour qu'on n'ait pas à faire hnf_constr *)
+ (* On devrait pouvoir s'arranger pour qu'on n'ait pas à faire hnf_constr *)
match kind_of_term (whd_betadeltaiota env Evd.empty typ) with
| Prod (_,c1,c2) ->
(* Typage garanti par l'appel à app_coercion*)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 8d19feea4..0fe691358 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1231,8 +1231,11 @@ let check_evars env initial_sigma evd c =
assert (Evd.mem sigma evk);
if not (Evd.mem initial_sigma evk) then
let (loc,k) = evar_source evk evd in
- let evi = nf_evar_info sigma (Evd.find sigma evk) in
- error_unsolvable_implicit loc env sigma evi k None
+ (match k with
+ | ImplicitArg (gr, (i, id), false) -> ()
+ | _ ->
+ let evi = nf_evar_info sigma (Evd.find sigma evk) in
+ error_unsolvable_implicit loc env sigma evi k None)
| _ -> iter_constr proc_rec c
in proc_rec c
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index dc212c9ca..883a64b9a 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -191,3 +191,6 @@ exception ClearDependencyError of identifier * clear_dependency_error
val clear_hyps_in_evi : evar_defs ref -> named_context_val -> types ->
identifier list -> named_context_val * types
+
+val push_rel_context_to_named_context : Environ.env -> types ->
+ named_context_val * types * constr list
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index ceaf25be0..38fca2f19 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -24,6 +24,17 @@ open Typeclasses_errors
open Libobject
(*i*)
+
+let add_instance_hint_ref = ref (fun id pri -> assert false)
+let register_add_instance_hint =
+ (:=) add_instance_hint_ref
+let add_instance_hint id = !add_instance_hint_ref id
+
+let set_typeclass_transparency_ref = ref (fun id pri -> assert false)
+let register_set_typeclass_transparency =
+ (:=) set_typeclass_transparency_ref
+let set_typeclass_transparency gr c = !set_typeclass_transparency_ref gr c
+
let mismatched_params env n m = mismatched_ctx_inst env Parameters n m
(* let mismatched_defs env n m = mismatched_ctx_inst env Definitions n m *)
let mismatched_props env n m = mismatched_ctx_inst env Properties n m
@@ -54,10 +65,10 @@ type instance = {
-1 for discard, 0 for none, mutable to avoid redeclarations
when multiple rebuild_object happen. *)
is_global: int;
- is_impl: constant;
+ is_impl: global_reference;
}
-type instances = (global_reference, instance Cmap.t) Gmap.t
+type instances = (global_reference, (global_reference, instance) Gmap.t) Gmap.t
let instance_impl is = is.is_impl
@@ -95,11 +106,6 @@ let _ =
Summary.unfreeze_function = unfreeze;
Summary.init_function = init }
-let add_instance_hint_ref = ref (fun id pri -> assert false)
-let register_add_instance_hint =
- (:=) add_instance_hint_ref
-let add_instance_hint id = !add_instance_hint_ref id
-
(*
* classes persistent object
*)
@@ -177,11 +183,11 @@ let add_class cl =
* instances persistent object
*)
-let load_instance (_,inst) =
- let insts =
- try Gmap.find inst.is_class !instances
- with Not_found -> Cmap.empty in
- let insts = Cmap.add inst.is_impl inst insts in
+let load_instance (_,inst) =
+ let insts =
+ try Gmap.find inst.is_class !instances
+ with Not_found -> Gmap.empty in
+ let insts = Gmap.add inst.is_impl inst insts in
instances := Gmap.add inst.is_class insts !instances
let cache_instance = load_instance
@@ -189,7 +195,7 @@ let cache_instance = load_instance
let subst_instance (subst,inst) =
{ inst with
is_class = fst (subst_global subst inst.is_class);
- is_impl = fst (Mod_subst.subst_con subst inst.is_impl) }
+ is_impl = fst (subst_global subst inst.is_impl) }
let discharge_instance (_,inst) =
if inst.is_global <= 0 then None
@@ -197,7 +203,7 @@ let discharge_instance (_,inst) =
{ inst with
is_global = pred inst.is_global;
is_class = Lib.discharge_global inst.is_class;
- is_impl = Lib.discharge_con inst.is_impl }
+ is_impl = Lib.discharge_global inst.is_impl }
let rebuild_instance inst =
add_instance_hint inst.is_impl inst.is_pri;
@@ -222,6 +228,36 @@ let add_instance i =
Lib.add_anonymous_leaf (instance_input i);
add_instance_hint i.is_impl i.is_pri
+open Declarations
+
+let add_constant_class cst =
+ let ty = Typeops.type_of_constant (Global.env ()) cst in
+ let ctx, arity = decompose_prod_assum ty in
+ let tc =
+ { cl_impl = ConstRef cst;
+ cl_context = ([], ctx);
+ cl_props = [(Anonymous, None, arity)];
+ cl_projs = []
+ }
+ in add_class tc;
+ set_typeclass_transparency (EvalConstRef cst) false
+
+let add_inductive_class ind =
+ let mind, oneind = Global.lookup_inductive ind in
+ let k =
+ let ty = Inductive.type_of_inductive_knowing_parameters
+ (push_rel_context oneind.mind_arity_ctxt (Global.env ()))
+ oneind (Termops.rel_vect 1 (List.length oneind.mind_arity_ctxt))
+ in
+ { cl_impl = IndRef ind;
+ cl_context = [], oneind.mind_arity_ctxt;
+ cl_props = [Anonymous, None, ty];
+ cl_projs = [] }
+ in add_class k;
+ Array.iteri (fun i _ ->
+ add_instance (new_instance k None true (ConstructRef (ind, succ i))))
+ oneind.mind_consnames
+
(*
* interface functions
*)
@@ -243,25 +279,24 @@ let typeclasses () = Gmap.fold (fun _ l c -> l :: c) !classes []
let cmapl_add x y m =
try
let l = Gmap.find x m in
- Gmap.add x (Cmap.add y.is_impl y l) m
+ Gmap.add x (Gmap.add y.is_impl y l) m
with Not_found ->
- Gmap.add x (Cmap.add y.is_impl y Cmap.empty) m
+ Gmap.add x (Gmap.add y.is_impl y Gmap.empty) m
-let cmap_elements c = Cmap.fold (fun k v acc -> v :: acc) c []
+let cmap_elements c = Gmap.fold (fun k v acc -> v :: acc) c []
let instances_of c =
try cmap_elements (Gmap.find c.cl_impl !instances) with Not_found -> []
-let all_instances () =
- Gmap.fold (fun k v acc ->
- Cmap.fold (fun k v acc -> v :: acc) v acc)
+let all_instances () =
+ Gmap.fold (fun k v acc ->
+ Gmap.fold (fun k v acc -> v :: acc) v acc)
!instances []
-let instances r =
- let cl = class_info r in instances_of cl
-
-
-let is_class gr =
+let instances r =
+ let cl = class_info r in instances_of cl
+
+let is_class gr =
Gmap.fold (fun k v acc -> acc || v.cl_impl = gr) !classes false
let is_instance = function
@@ -273,6 +308,8 @@ let is_instance = function
(match Decls.variable_kind v with
| IsDefinition Instance -> true
| _ -> false)
+ | ConstructRef (ind,_) ->
+ is_class (IndRef ind)
| _ -> false
let is_implicit_arg k =
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index c9ee9adf0..19ec47cf4 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -49,7 +49,11 @@ val all_instances : unit -> instance list
val add_class : typeclass -> unit
-val new_instance : typeclass -> int option -> bool -> constant -> instance
+val add_constant_class : constant -> unit
+
+val add_inductive_class : inductive -> unit
+
+val new_instance : typeclass -> int option -> bool -> global_reference -> instance
val add_instance : instance -> unit
val class_info : global_reference -> typeclass (* raises a UserError if not a class *)
@@ -60,8 +64,8 @@ val dest_class_app : env -> constr -> typeclass * constr list
(* Just return None if not a class *)
val class_of_constr : constr -> typeclass option
-
-val instance_impl : instance -> constant
+
+val instance_impl : instance -> global_reference
val is_class : global_reference -> bool
val is_instance : global_reference -> bool
@@ -86,8 +90,11 @@ val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool ->
env -> evar_defs -> evar_defs
val resolve_one_typeclass : env -> evar_map -> types -> open_constr
-val register_add_instance_hint : (constant -> int option -> unit) -> unit
-val add_instance_hint : constant -> int option -> unit
+val register_set_typeclass_transparency : (evaluable_global_reference -> bool -> unit) -> unit
+val set_typeclass_transparency : evaluable_global_reference -> bool -> unit
+
+val register_add_instance_hint : (global_reference -> int option -> unit) -> unit
+val add_instance_hint : global_reference -> int option -> unit
val solve_instanciations_problem : (env -> evar_defs -> bool -> bool -> bool -> evar_defs) ref
val solve_instanciation_problem : (env -> evar_map -> types -> open_constr) ref
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e8d95a798..a3e63541f 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -27,6 +27,18 @@ open Retyping
open Coercion.Default
open Recordops
+let occur_meta_or_undefined_evar evd c =
+ let rec occrec c = match kind_of_term c with
+ | Meta _ -> raise Occur
+ | Evar (ev,args) ->
+ (match evar_body (Evd.find evd ev) with
+ | Evar_defined c ->
+ occrec c; Array.iter occrec args
+ | Evar_empty -> raise Occur)
+ | Sort s when is_sort_variable evd s -> raise Occur
+ | _ -> iter_constr occrec c
+ in try occrec c; false with Occur | Not_found -> true
+
(* if lname_typ is [xn,An;..;x1,A1] and l is a list of terms,
gives [x1:A1]..[xn:An]c' such that c converts to ([x1:A1]..[xn:An]c' l) *)
@@ -192,15 +204,16 @@ let oracle_order env cf1 cf2 =
let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flags m n =
let trivial_unify curenv pb (sigma,metasubst,_) m n =
let subst = if flags.use_metas_eagerly then metasubst else ms in
- match subst_defined_metas subst m with
- | Some m1 ->
- if (match flags.modulo_conv_on_closed_terms with
- Some flags ->
+ match subst_defined_metas subst m, subst_defined_metas subst n with
+ | Some m1, Some n1 ->
+ let evd = (create_evar_defs sigma) in
+ if (occur_meta_or_undefined_evar evd m1 || occur_meta_or_undefined_evar evd n1)
+ then false
+ else if (match flags.modulo_conv_on_closed_terms with
+ | Some flags ->
is_trans_fconv (conv_pb_of pb) flags env sigma m1 n
- | None -> false) then true else
- if (not (is_ground_term (create_evar_defs sigma) m1))
- || occur_meta_or_existential n then false else
- error_cannot_unify curenv sigma (m, n)
+ | None -> false) then true
+ else error_cannot_unify curenv sigma (m, n)
| _ -> false in
let rec unirec_rec (curenv,nb as curenvnb) pb b ((sigma,metasubst,evarsubst) as substn) curm curn =
let cM = Evarutil.whd_castappevar sigma curm
@@ -370,22 +383,20 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
unirec_rec curenvnb pb b substn c1 (applist (c,(List.rev ks)))
in
- if (if occur_meta m then false else
- if (match flags.modulo_conv_on_closed_terms with
- Some flags ->
- is_trans_fconv (conv_pb_of cv_pb) flags env sigma m n
- | None -> constr_cmp (conv_pb_of cv_pb) m n) then true else
- if (not (is_ground_term (create_evar_defs sigma) m))
- || occur_meta_or_existential n then false else
- if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with
+ let evd = create_evar_defs sigma in
+ if (if occur_meta_or_undefined_evar evd m || occur_meta_or_undefined_evar evd n then false
+ else if (match flags.modulo_conv_on_closed_terms with
+ | Some flags ->
+ is_trans_fconv (conv_pb_of cv_pb) flags env sigma m n
+ | None -> constr_cmp (conv_pb_of cv_pb) m n) then true
+ else if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with
| Some (cv_id, cv_k), (dl_id, dl_k) ->
Idpred.subset dl_id cv_id && Cpred.subset dl_k cv_k
| None,(dl_id, dl_k) ->
Idpred.is_empty dl_id && Cpred.is_empty dl_k)
then error_cannot_unify env sigma (m, n) else false)
then subst
- else
- unirec_rec (env,0) cv_pb conv_at_top subst m n
+ else unirec_rec (env,0) cv_pb conv_at_top subst m n
let unify_0 env sigma = unify_0_with_initial_metas (sigma,[],[]) true env
diff --git a/tactics/auto.ml b/tactics/auto.ml
index dd11e1ef0..5de89baa6 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -123,6 +123,7 @@ module Hint_db = struct
type t = {
hintdb_state : Names.transparent_state;
+ hintdb_unfolds : Idset.t * Cset.t;
use_dn : bool;
hintdb_map : search_entry Constr_map.t;
(* A list of unindexed entries starting with an unfoldable constant
@@ -131,6 +132,7 @@ module Hint_db = struct
}
let empty st use_dn = { hintdb_state = st;
+ hintdb_unfolds = (Idset.empty, Cset.empty);
use_dn = use_dn;
hintdb_map = Constr_map.empty;
hintdb_nopat = [] }
@@ -179,14 +181,17 @@ module Hint_db = struct
List.fold_left (fun db (gr,v) -> addkv gr v db) db' db.hintdb_nopat
let add_one (k,v) db =
- let st',rebuild =
+ let st',db,rebuild =
match v.code with
| Unfold_nth egr ->
- let (ids,csts) = db.hintdb_state in
- (match egr with
- | EvalVarRef id -> (Idpred.add id ids, csts)
- | EvalConstRef cst -> (ids, Cpred.add cst csts)), true
- | _ -> db.hintdb_state, false
+ let addunf (ids,csts) (ids',csts') =
+ match egr with
+ | EvalVarRef id -> (Idpred.add id ids, csts), (Idset.add id ids', csts')
+ | EvalConstRef cst -> (ids, Cpred.add cst csts), (ids', Cset.add cst csts')
+ in
+ let state, unfs = addunf db.hintdb_state db.hintdb_unfolds in
+ state, { db with hintdb_unfolds = unfs }, true
+ | _ -> db.hintdb_state, db, false
in
let db = if db.use_dn && rebuild then rebuild_db st' db else db
in addkv k v db
@@ -203,6 +208,8 @@ module Hint_db = struct
if db.use_dn then rebuild_db st db
else { db with hintdb_state = st }
+ let unfolds db = db.hintdb_unfolds
+
let use_dn db = db.use_dn
end
@@ -356,17 +363,18 @@ open Vernacexpr
(* If the database does not exist, it is created *)
(* TODO: should a warning be printed in this case ?? *)
-let add_hint dbname hintlist =
- try
- let db = searchtable_map dbname in
- let db' = Hint_db.add_list hintlist db in
+
+let get_db dbname =
+ try searchtable_map dbname
+ with Not_found -> Hint_db.empty empty_transparent_state false
+
+let add_hint dbname hintlist =
+ let db = get_db dbname in
+ let db' = Hint_db.add_list hintlist db in
searchtable_add (dbname,db')
- with Not_found ->
- let db = Hint_db.add_list hintlist (Hint_db.empty empty_transparent_state false) in
- searchtable_add (dbname,db)
let add_transparency dbname grs b =
- let db = searchtable_map dbname in
+ let db = get_db dbname in
let st = Hint_db.transparent_state db in
let st' =
List.fold_left (fun (ids, csts) gr ->
@@ -882,7 +890,7 @@ and tac_of_hint db_list local_db concl (flags, {pat=p; code=t}) =
tclTHEN
(unify_resolve_gen flags (term,cl))
(trivial_fail_db (flags <> None) db_list local_db)
- | Unfold_nth c -> unfold_in_concl [all_occurrences,c]
+ | Unfold_nth c -> tclPROGRESS (unfold_in_concl [all_occurrences,c])
| Extern tacast -> conclPattern concl p tacast
and trivial_resolve mod_delta db_list local_db cl =
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 83ad60bc3..fe59dc1e1 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -63,6 +63,8 @@ module Hint_db :
val use_dn : t -> bool
val transparent_state : t -> transparent_state
val set_transparent_state : t -> transparent_state -> t
+
+ val unfolds : t -> Idset.t * Cset.t
end
type hint_db_name = string
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index db0bbd867..0b69eebbd 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -247,7 +247,9 @@ type hypinfo = {
}
let evd_convertible env evd x y =
- try ignore(Evarconv.the_conv_x env x y evd); true
+ try
+ ignore(Unification.w_unify true env Reduction.CONV x y evd); true
+ (* try ignore(Evarconv.the_conv_x env x y evd); true *)
with _ -> false
let decompose_applied_relation metas env sigma c ctype left2right =
@@ -269,8 +271,8 @@ let decompose_applied_relation metas env sigma c ctype left2right =
let ty1, ty2 =
Typing.mtype_of env eqclause.evd c1, Typing.mtype_of env eqclause.evd c2
in
- if not (evd_convertible env eqclause.evd ty1 ty2) then None
- else
+(* if not (evd_convertible env eqclause.evd ty1 ty2) then None *)
+(* else *)
Some { hyp_cl=eqclause; hyp_prf=(Clenv.clenv_value eqclause); hyp_ty = ty;
hyp_car=ty1; hyp_rel=mkApp (equiv, Array.of_list others);
hyp_l2r=left2right; hyp_left=c1; hyp_right=c2; }
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 94b2eff38..40eaec65c 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -89,13 +89,10 @@ let intersects s t =
open Auto
-let e_give_exact flags c gl =
- let t1 = (pf_type_of gl c) and t2 = pf_concl gl in
- if occur_existential t1 or occur_existential t2 then
- tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) gl
- else exact_check c gl
-(* let t1 = (pf_type_of gl c) in *)
-(* tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) gl *)
+let e_give_exact flags c gl =
+ let t1 = (pf_type_of gl c) in
+ tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) gl
+
let assumption flags id = e_give_exact flags (mkVar id)
open Unification
@@ -129,12 +126,12 @@ END
let unify_e_resolve flags (c,clenv) gls =
let clenv' = connect_clenv gls clenv in
let clenv' = clenv_unique_resolver false ~flags clenv' gls in
- Clenvtac.clenv_refine true ~with_classes:false clenv' gls
+ tclPROGRESS (Clenvtac.clenv_refine true ~with_classes:false clenv') gls
let unify_resolve flags (c,clenv) gls =
let clenv' = connect_clenv gls clenv in
let clenv' = clenv_unique_resolver false ~flags clenv' gls in
- Clenvtac.clenv_refine false ~with_classes:false clenv' gls
+ tclPROGRESS (Clenvtac.clenv_refine false ~with_classes:false clenv') gls
(** Hack to properly solve dependent evars that are typeclasses *)
@@ -151,9 +148,9 @@ let rec e_trivial_fail_db db_list local_db goal =
let hintl = make_resolve_hyp (pf_env g') (project g') d in
(e_trivial_fail_db db_list
(Hint_db.add_list hintl local_db) g'))) ::
- (List.map pi1 (e_trivial_resolve db_list local_db (pf_concl goal)) )
- in
- tclFIRST (List.map tclCOMPLETE tacl) goal
+ (List.map (fun (x,_,_,_) -> x) (e_trivial_resolve db_list local_db (pf_concl goal)))
+ in
+ tclFIRST (List.map tclCOMPLETE tacl) goal
and e_my_find_search db_list local_db hdc concl =
let hdc = head_of_constr_reference hdc in
@@ -178,12 +175,13 @@ and e_my_find_search db_list local_db hdc concl =
| Res_pf_THEN_trivial_fail (term,cl) ->
tclTHEN (unify_e_resolve flags (term,cl))
(e_trivial_fail_db db_list local_db)
- | Unfold_nth c -> unfold_in_concl [all_occurrences,c]
+ | Unfold_nth c -> tclWEAK_PROGRESS (unfold_in_concl [all_occurrences,c])
| Extern tacast -> conclPattern concl p tacast
in
- (tac,b,pr_autotactic t)
- in
- List.map tac_of_hint hintl
+ match t with
+ | Extern _ -> (tac,b,true,pr_autotactic t)
+ | _ -> (tac,b,false,pr_autotactic t)
+ in List.map tac_of_hint hintl
and e_trivial_resolve db_list local_db gl =
try
@@ -228,7 +226,7 @@ type validation = evar_map -> proof_tree list -> proof_tree
let pr_depth l = prlist_with_sep (fun () -> str ".") pr_int (List.rev l)
-type autoinfo = { hints : Auto.hint_db; auto_depth: int list; auto_last_tac: std_ppcmds }
+type autoinfo = { hints : Auto.hint_db; only_classes: bool; auto_depth: int list; auto_last_tac: std_ppcmds }
type autogoal = goal * autoinfo
type 'ans fk = unit -> 'ans
type ('a,'ans) sk = 'a -> 'ans fk -> 'ans
@@ -238,6 +236,26 @@ type auto_result = autogoal list sigma * validation
type atac = auto_result tac
+let make_resolve_hyp env sigma st flags only_classes pri (id, _, cty) =
+ let cty = Evarutil.nf_evar sigma cty in
+ let keep = not only_classes ||
+ let ctx, ar = decompose_prod cty in
+ match kind_of_term (fst (decompose_app ar)) with
+ | Const c -> is_class (ConstRef c)
+ | Ind i -> is_class (IndRef i)
+ | _ -> false
+ in
+ if keep then let c = mkVar id in
+ map_succeed
+ (fun f -> try f (c,cty) with UserError _ -> failwith "")
+ [make_exact_entry pri; make_apply_entry env sigma flags pri]
+ else []
+
+let make_autogoal_hints only_classes ?(st=full_transparent_state) g =
+ let sign = pf_hyps g in
+ let hintlist = list_map_append (pf_apply make_resolve_hyp g st (true,false,false) only_classes None) sign in
+ Hint_db.add_list hintlist (Hint_db.empty st true)
+
let lift_tactic tac (f : goal list sigma -> autoinfo -> autogoal list sigma) : 'a tac =
{ skft = fun sk fk {it = gl,hints; sigma=s} ->
let res = try Some (tac {it=gl; sigma=s}) with e when catchable e -> None in
@@ -251,7 +269,8 @@ let intro_tac : atac =
let gls' =
List.map (fun g' ->
let env = evar_env g' in
- let hint = make_resolve_hyp env s (List.hd (evar_context g')) in
+ let hint = make_resolve_hyp env s (Hint_db.transparent_state info.hints)
+ (true,false,false) info.only_classes None (List.hd (evar_context g')) in
let ldb = Hint_db.add_list hint info.hints in
(g', { info with hints = ldb; auto_last_tac = str"intro" })) gls
in {it = gls'; sigma = s})
@@ -261,7 +280,7 @@ let id_tac : atac =
sk ({it = [gl]; sigma = s}, fun _ pfs -> List.hd pfs) fk }
(* Ordering of states is lexicographic on the number of remaining goals. *)
-let compare (pri, _, (res, _)) (pri', _, (res', _)) =
+let compare (pri, _, _, (res, _)) (pri', _, _, (res', _)) =
let nbgoals s =
List.length (sig_it s) + nb_empty_evars (sig_sig s)
in
@@ -277,17 +296,17 @@ let solve_tac (x : 'a tac) : 'a tac =
let hints_tac hints =
{ skft = fun sk fk {it = gl,info; sigma = s} ->
-(* if !typeclasses_debug then msgnl (str"depth=" ++ int info.auto_depth ++ str": " ++ info.auto_last_tac *)
-(* ++ spc () ++ str "->" ++ spc () ++ pr_ev s gl); *)
- let possible_resolve ((lgls,v) as res, pri, pp) =
- (pri, pp, res)
+ let possible_resolve ((lgls,v) as res, pri, b, pp) =
+ (pri, pp, b, res)
in
+ let ({it = normalized; sigma = s}, valid) = tclNORMEVAR {it = gl; sigma = s} in
+ let gl = List.hd normalized in
let tacs =
let concl = Evarutil.nf_evar s gl.evar_concl in
let poss = e_possible_resolve hints info.hints concl in
let l =
- Util.list_map_append (fun (tac, pri, pptac) ->
- try [tac {it = gl; sigma = s}, pri, pptac] with e when catchable e -> [])
+ Util.list_map_append (fun (tac, pri, b, pptac) ->
+ try [(tclTHEN tclNORMEVAR tac) {it = gl; sigma = s}, pri, b, pptac] with e when catchable e -> [])
poss
in
if l = [] && !typeclasses_debug then
@@ -298,16 +317,24 @@ let hints_tac hints =
in
let tacs = List.sort compare tacs in
let rec aux i = function
- | (_, pp, ({it = gls; sigma = s}, v)) :: tl ->
+ | (_, pp, b, ({it = gls; sigma = s}, v)) :: tl ->
if !typeclasses_debug then msgnl (pr_depth (i :: info.auto_depth) ++ str": " ++ pp
++ str" on" ++ spc () ++ pr_ev s gl);
let fk =
(fun () -> (* if !typeclasses_debug then msgnl (str"backtracked after " ++ pp); *)
aux (succ i) tl)
in
- let glsv = {it = list_map_i (fun j g -> g,
- { info with auto_depth = j :: i :: info.auto_depth;
- auto_last_tac = pp }) 1 gls; sigma = s}, fun _ -> v in
+ let gls' = list_map_i (fun j g ->
+ let info =
+ { info with auto_depth = j :: i :: info.auto_depth; auto_last_tac = pp;
+ hints =
+ if b && g.evar_hyps <> gl.evar_hyps
+ then make_autogoal_hints info.only_classes
+ ~st:(Hint_db.transparent_state info.hints) {it = g; sigma = s}
+ else info.hints }
+ in g, info) 1 gls in
+ let glsvalid _ pfs = valid [v pfs] in
+ let glsv = {it = gls'; sigma = s}, glsvalid in
sk glsv fk
| [] -> fk ()
in aux 1 tacs }
@@ -351,42 +378,13 @@ let run_list_tac (t : 'a tac) p goals (gl : autogoal list sigma) : run_list_res
let rec fix (t : 'a tac) : 'a tac =
then_tac t { skft = fun sk fk -> (fix t).skft sk fk }
-
-(* A special one for getting everything into a dnet. *)
-
-let is_transparent_gr (ids, csts) = function
- | VarRef id -> Idpred.mem id ids
- | ConstRef cst -> Cpred.mem cst csts
- | IndRef _ | ConstructRef _ -> false
-
-let make_resolve_hyp env sigma st flags pri (id, _, cty) =
- let cty = Evarutil.nf_evar sigma cty in
- let ctx, ar = decompose_prod cty in
- let keep =
- match kind_of_term (fst (decompose_app ar)) with
- | Const c -> is_class (ConstRef c)
- | Ind i -> is_class (IndRef i)
- | _ -> false
- in
- if keep then let c = mkVar id in
- map_succeed
- (fun f -> f (c,cty))
- [make_exact_entry pri; make_apply_entry env sigma flags pri]
- else []
-
-let make_autogoal ?(st=full_transparent_state) g =
- let sign = pf_hyps g in
- let hintlist = list_map_append (pf_apply make_resolve_hyp g st (true,false,false) None) sign in
- let st = List.fold_left (fun (ids, csts) (n, b, t) ->
- (if b <> None then Idpred.add else Idpred.remove) n ids, csts)
- st sign
- in
- let hints = Hint_db.add_list hintlist (Hint_db.empty st true) in
- (g.it, { hints = hints ; auto_depth = []; auto_last_tac = mt() })
-
-let make_autogoals ?(st=full_transparent_state) gs evm' =
- { it = list_map_i (fun i g ->
- let (gl, auto) = make_autogoal ~st {it = snd g; sigma = evm'} in
+let make_autogoal ?(only_classes=true) ?(st=full_transparent_state) g =
+ let hints = make_autogoal_hints only_classes ~st g in
+ (g.it, { hints = hints ; only_classes = only_classes; auto_depth = []; auto_last_tac = mt() })
+
+let make_autogoals ?(only_classes=true) ?(st=full_transparent_state) gs evm' =
+ { it = list_map_i (fun i g ->
+ let (gl, auto) = make_autogoal ~only_classes ~st {it = snd g; sigma = evm'} in
(gl, { auto with auto_depth = [i]})) 1 gs; sigma = evm' }
let get_result r =
@@ -395,20 +393,20 @@ let get_result r =
| Some ((gls, v), fk) ->
try ignore(v (sig_sig gls) []); assert(false)
with Found evm' -> Some (evm', fk)
-
-let run_on_evars ?(st=full_transparent_state) p evm tac =
+
+let run_on_evars ?(only_classes=true) ?(st=full_transparent_state) p evm tac =
match evars_to_goals p evm with
| None -> None (* This happens only because there's no evar having p *)
| Some (goals, evm') ->
- let res = run_list_tac tac p goals (make_autogoals ~st goals evm') in
+ let res = run_list_tac tac p goals (make_autogoals ~only_classes ~st goals evm') in
match get_result res with
| None -> raise Not_found
| Some (evm', fk) -> Some (Evd.evars_reset_evd evm' evm, fk)
-
+
let eauto_tac hints = fix (or_tac intro_tac (hints_tac hints))
-
-let eauto hints g =
- let gl = { it = make_autogoal ~st:(Hint_db.transparent_state (List.hd hints)) g; sigma = project g } in
+
+let eauto ?(only_classes=true) ?st hints g =
+ let gl = { it = make_autogoal ~only_classes ?st g; sigma = project g } in
match run_tac (eauto_tac hints) gl with
| None -> raise Not_found
| Some ({it = goals; sigma = s}, valid) ->
@@ -477,6 +475,27 @@ let select_evars evs evm =
if Intset.mem ev evs then Evd.add acc ev evi else acc)
evm Evd.empty
+let is_inference_forced p ev evd =
+ try
+ let evi = Evd.find evd ev in
+ if evi.evar_body = Evar_empty then
+ if Typeclasses.is_resolvable evi
+ && snd (p ev evi)
+ then
+ let (loc, k) = evar_source ev evd in
+ match k with
+ | ImplicitArg (_, _, b) -> b
+ | QuestionMark _ -> false
+ | _ -> true
+ else true
+ else false
+ with Not_found -> true
+
+let is_optional p comp evd =
+ Intset.fold (fun ev acc ->
+ acc && not (is_inference_forced p ev evd))
+ comp true
+
let resolve_all_evars debug m env p oevd do_split fail =
let split = if do_split then split_evars oevd else [Intset.empty] in
let p = if do_split then
@@ -506,10 +525,10 @@ let resolve_all_evars debug m env p oevd do_split fail =
| comp :: comps ->
let res = try aux (p comp) evd with Not_found -> None in
match res with
- | None ->
- if fail then
+ | None ->
+ if fail && (not do_split || not (is_optional (p comp evd) comp evd)) then
+ (* Unable to satisfy the constraints. *)
let evd = Evarutil.nf_evars evd in
- (* Unable to satisfy the constraints. *)
let evm = if do_split then select_evars comp evd else evd in
let _, ev = Evd.fold
(fun ev evi (b,acc) ->
@@ -540,19 +559,20 @@ let _ =
Typeclasses.solve_instanciations_problem :=
solve_inst false true default_eauto_depth
+let set_transparency cl b =
+ List.iter (fun r ->
+ let gr = Smartlocate.global_with_alias r in
+ let ev = Tacred.evaluable_of_global_reference (Global.env ()) gr in
+ Classes.set_typeclass_transparency ev b) cl
VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings
| [ "Typeclasses" "Transparent" reference_list(cl) ] -> [
- add_hints false [typeclasses_db]
- (interp_hints (Vernacexpr.HintsTransparency (cl, true)))
- ]
+ set_transparency cl true ]
END
VERNAC COMMAND EXTEND Typeclasses_Rigid_Settings
| [ "Typeclasses" "Opaque" reference_list(cl) ] -> [
- add_hints false [typeclasses_db]
- (interp_hints (Vernacexpr.HintsTransparency (cl, false)))
- ]
+ set_transparency cl false ]
END
open Genarg
@@ -596,10 +616,16 @@ VERNAC COMMAND EXTEND Typeclasses_Settings
]
END
+let typeclasses_eauto ?(st=full_transparent_state) dbs gl =
+ try
+ let dbs = list_map_filter (fun db -> try Some (Auto.searchtable_map db) with _ -> None) dbs in
+ let st = match dbs with [x] -> Hint_db.transparent_state x | _ -> st in
+ eauto ~only_classes:false ~st dbs gl
+ with Not_found -> tclFAIL 0 (str" typeclasses eauto failed") gl
+
TACTIC EXTEND typeclasses_eauto
-| [ "typeclasses" "eauto" ] -> [ fun gl ->
- try eauto [Auto.searchtable_map typeclasses_db] gl
- with Not_found -> tclFAIL 0 (str" typeclasses eauto failed") gl ]
+| [ "typeclasses" "eauto" "with" ne_preident_list(l) ] -> [ typeclasses_eauto l ]
+| [ "typeclasses" "eauto" ] -> [ typeclasses_eauto [typeclasses_db] ]
END
let _ = Classes.refine_ref := Refine.refine
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 25efd5a05..17361f2e6 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -394,6 +394,18 @@ TACTIC EXTEND dfs_eauto
[ gen_eauto false (true, make_depth p) lems db ]
END
+let cons a l = a :: l
+
+let autounfold db cl =
+ let unfolds = List.concat (List.map (fun dbname ->
+ let db = try searchtable_map dbname
+ with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname)
+ in
+ let (ids, csts) = Hint_db.unfolds db in
+ Cset.fold (fun cst -> cons (all_occurrences, EvalConstRef cst)) csts
+ (Idset.fold (fun id -> cons (all_occurrences, EvalVarRef id)) ids [])) db)
+ in unfold_option unfolds cl
+
let autosimpl db cl =
let unfold_of_elts constr (b, elts) =
if not b then
@@ -407,9 +419,86 @@ let autosimpl db cl =
unfold_of_elts (fun x -> EvalVarRef x) (Idpred.elements ids)) db)
in unfold_option unfolds cl
-TACTIC EXTEND autosimpl
-| [ "autosimpl" hintbases(db) ] ->
- [ autosimpl (match db with None -> ["core"] | Some x -> "core"::x) None ]
+TACTIC EXTEND autounfold
+| [ "autounfold" hintbases(db) "in" hyp(id) ] ->
+ [ autounfold (match db with None -> ["core"] | Some x -> "core"::x) (Some (id, InHyp)) ]
+| [ "autounfold" hintbases(db) ] ->
+ [ autounfold (match db with None -> ["core"] | Some x -> "core"::x) None ]
+ END
+
+let unfold_head env (ids, csts) c =
+ let rec aux c =
+ match kind_of_term c with
+ | Var id when Idset.mem id ids ->
+ (match Environ.named_body id env with
+ | Some b -> true, b
+ | None -> false, c)
+ | Const cst when Cset.mem cst csts ->
+ true, Environ.constant_value env cst
+ | App (f, args) ->
+ (match aux f with
+ | true, f' -> true, Reductionops.whd_betaiota Evd.empty (mkApp (f', args))
+ | false, _ ->
+ let done_, args' =
+ array_fold_left_i (fun i (done_, acc) arg ->
+ if done_ then done_, arg :: acc
+ else match aux arg with
+ | true, arg' -> true, arg' :: acc
+ | false, arg' -> false, arg :: acc)
+ (false, []) args
+ in
+ if done_ then true, mkApp (f, Array.of_list (List.rev args'))
+ else false, c)
+ | _ ->
+ let done_ = ref false in
+ let c' = map_constr (fun c ->
+ if !done_ then c else
+ let x, c' = aux c in
+ done_ := x; c') c
+ in !done_, c'
+ in aux c
+
+let autounfold_one db cl gl =
+ let st =
+ List.fold_left (fun (i,c) dbname ->
+ let db = try searchtable_map dbname
+ with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname)
+ in
+ let (ids, csts) = Hint_db.unfolds db in
+ (Idset.union ids i, Cset.union csts c)) (Idset.empty, Cset.empty) db
+ in
+ let did, c' = unfold_head (pf_env gl) st (match cl with Some (id, _) -> pf_get_hyp_typ gl id | None -> pf_concl gl) in
+ if did then
+ match cl with
+ | Some hyp -> change_in_hyp None c' hyp gl
+ | None -> convert_concl_no_check c' DEFAULTcast gl
+ else tclFAIL 0 (str "Nothing to unfold") gl
+
+(* Cset.fold (fun cst -> cons (all_occurrences, EvalConstRef cst)) csts *)
+(* (Idset.fold (fun id -> cons (all_occurrences, EvalVarRef id)) ids [])) db) *)
+(* in unfold_option unfolds cl *)
+
+(* let db = try searchtable_map dbname *)
+(* with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname) *)
+(* in *)
+(* let (ids, csts) = Hint_db.unfolds db in *)
+(* Cset.fold (fun cst -> tclORELSE (unfold_option [(occ, EvalVarRef id)] cst)) csts *)
+(* (Idset.fold (fun id -> tclORELSE (unfold_option [(occ, EvalVarRef id)] cl) ids acc))) *)
+(* (tclFAIL 0 (mt())) db *)
+
+TACTIC EXTEND autounfold_one
+| [ "autounfold_one" hintbases(db) "in" hyp(id) ] ->
+ [ autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) (Some (id, InHyp)) ]
+| [ "autounfold_one" hintbases(db) ] ->
+ [ autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) None ]
+ END
+
+TACTIC EXTEND autounfoldify
+| [ "autounfoldify" constr(x) ] -> [
+ let db = match kind_of_term x with
+ | Const c -> string_of_label (con_label c)
+ | _ -> assert false
+ in autounfold ["core";db] None ]
END
TACTIC EXTEND unify
@@ -417,3 +506,8 @@ TACTIC EXTEND unify
| ["unify" constr(x) constr(y) "with" preident(base) ] -> [
unify ~state:(Hint_db.transparent_state (searchtable_map base)) x y ]
END
+
+
+TACTIC EXTEND convert_concl_no_check
+| ["convert_concl_no_check" constr(x) ] -> [ convert_concl_no_check x DEFAULTcast ]
+END
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 7359d070e..b708949e0 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -35,3 +35,5 @@ val eauto_with_bases :
bool ->
bool * int ->
Term.constr list -> Auto.hint_db list -> Proof_type.tactic
+
+val autounfold : hint_db_name list -> Tacticals.goal_location -> tactic
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 58ab6dfa0..de5445310 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -478,10 +478,24 @@ END
(* sozeau: abs/gen for induction on instantiated dependent inductives, using "Ford" induction as
defined by Conor McBride *)
TACTIC EXTEND generalize_eqs
-| ["generalize_eqs" hyp(id) ] -> [ abstract_generalize id ~generalize_vars:false ]
+| ["generalize_eqs" hyp(id) ] -> [ abstract_generalize ~generalize_vars:false id ]
+END
+TACTIC EXTEND dep_generalize_eqs
+| ["dependent" "generalize_eqs" hyp(id) ] -> [ abstract_generalize ~generalize_vars:false ~force_dep:true id ]
END
TACTIC EXTEND generalize_eqs_vars
-| ["generalize_eqs_vars" hyp(id) ] -> [ abstract_generalize id ~generalize_vars:true ]
+| ["generalize_eqs_vars" hyp(id) ] -> [ abstract_generalize ~generalize_vars:true id ]
+END
+TACTIC EXTEND dep_generalize_eqs_vars
+| ["dependent" "generalize_eqs_vars" hyp(id) ] -> [ abstract_generalize ~force_dep:true ~generalize_vars:true id ]
+END
+
+(** Tactic to automatically simplify hypotheses of the form [Π Δ, x_i = t_i -> T]
+ where [t_i] is closed w.r.t. Δ. Such hypotheses are automatically generated
+ during dependent induction. *)
+
+TACTIC EXTEND specialize_hyp
+[ "specialize_hypothesis" hyp(id) ] -> [ specialize_hypothesis id ]
END
TACTIC EXTEND dependent_pattern
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 0884b3462..07de95d8e 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -201,8 +201,8 @@ let build_signature evars env m (cstrs : 'a option list) (finalcstr : 'a option)
if obj = None then evars, mkProd(na, ty, b), arg', (ty, None) :: cstrs
else error "build_signature: no constraint can apply on a dependent argument"
else
- let (evars, b', arg, cstrs) = aux env evars (subst1 mkProp b) cstrs in
let ty = Reductionops.nf_betaiota (fst evars) ty in
+ let (evars, b', arg, cstrs) = aux env evars (subst1 mkProp b) cstrs in
let evars, relty = mk_relty evars env ty obj in
let newarg = mkApp (Lazy.force respectful, [| ty ; b' ; relty ; arg |]) in
evars, mkProd(na, ty, b), newarg, (ty, Some relty) :: cstrs
@@ -1279,8 +1279,8 @@ let add_morphism_infer glob m n =
let cst = Declare.declare_internal_constant instance_id
(Entries.ParameterEntry (instance,false), Decl_kinds.IsAssumption Decl_kinds.Logical)
in
- add_instance (Typeclasses.new_instance (Lazy.force proper_class) None glob cst);
- declare_projection n instance_id (ConstRef cst)
+ add_instance (Typeclasses.new_instance (Lazy.force proper_class) None glob (ConstRef cst));
+ declare_projection n instance_id (ConstRef cst)
else
let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
Flags.silently
@@ -1289,7 +1289,7 @@ let add_morphism_infer glob m n =
(fun _ -> function
Libnames.ConstRef cst ->
add_instance (Typeclasses.new_instance (Lazy.force proper_class) None
- glob cst);
+ glob (ConstRef cst));
declare_projection n instance_id (ConstRef cst)
| _ -> assert false);
Pfedit.by (Tacinterp.interp <:tactic< Coq.Classes.SetoidTactics.add_morphism_tactic>>)) ();
@@ -1306,8 +1306,7 @@ let add_morphism glob binders m s n =
in
let tac = Tacinterp.interp <:tactic<add_morphism_tactic>> in
ignore(new_instance ~global:glob binders instance (CRecord (dummy_loc,None,[]))
- ~generalize:false ~tac
- ~hook:(fun cst -> declare_projection n instance_id (ConstRef cst)) None)
+ ~generalize:false ~tac ~hook:(declare_projection n instance_id) None)
VERNAC COMMAND EXTEND AddSetoid1
[ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f99da0247..a740d7bb2 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -648,8 +648,8 @@ let cut c gl =
let cut_intro t = tclTHENFIRST (cut t) intro
-(* cut_replacing échoue si l'hypothèse à remplacer apparaît dans le
- but, ou dans une autre hypothèse *)
+(* cut_replacing échoue si l'hypothèse à remplacer apparaît dans le
+ but, ou dans une autre hypothèse *)
let cut_replacing id t tac =
tclTHENLAST (internal_cut_rev_replace id t)
(tac (refine_no_check (mkVar id)))
@@ -1427,14 +1427,14 @@ let generalized_name c t ids cl = function
constante dont on aurait pu prendre directement le nom *)
named_hd (Global.env()) t Anonymous
-let generalize_goal gl i ((occs,c),na) cl =
+let generalize_goal gl i ((occs,c,b),na) cl =
let t = pf_type_of gl c in
let decls,cl = decompose_prod_n_assum i cl in
let dummy_prod = it_mkProd_or_LetIn mkProp decls in
let newdecls,_ = decompose_prod_n_assum i (subst_term c dummy_prod) in
let cl' = subst_term_occ occs c (it_mkProd_or_LetIn cl newdecls) in
let na = generalized_name c t (pf_ids_of_hyps gl) cl' na in
- mkProd (na,t,cl')
+ mkProd_or_LetIn (na,b,t) cl'
let generalize_dep c gl =
let env = pf_env gl in
@@ -1457,28 +1457,40 @@ let generalize_dep c gl =
| _ -> tothin
in
let cl' = it_mkNamedProd_or_LetIn (pf_concl gl) to_quantify in
- let cl'' = generalize_goal gl 0 ((all_occurrences,c),Anonymous) cl' in
+ let cl'' = generalize_goal gl 0 ((all_occurrences,c,None),Anonymous) cl' in
let args = Array.to_list (instance_from_named_context to_quantify_rev) in
tclTHEN
(apply_type cl'' (c::args))
(thin (List.rev tothin'))
gl
-let generalize_gen lconstr gl =
+let generalize_gen_let lconstr gl =
let newcl =
list_fold_right_i (generalize_goal gl) 0 lconstr (pf_concl gl) in
- apply_type newcl (List.map (fun ((_,c),_) -> c) lconstr) gl
+ apply_type newcl (list_map_filter (fun ((_,c,b),_) ->
+ if b = None then Some c else None) lconstr) gl
+let generalize_gen lconstr =
+ generalize_gen_let (List.map (fun ((occs,c),na) ->
+ (occs,c,None),na) lconstr)
+
let generalize l =
- generalize_gen (List.map (fun c -> ((all_occurrences,c),Anonymous)) l)
+ generalize_gen_let (List.map (fun c -> ((all_occurrences,c,None),Anonymous)) l)
-let revert hyps gl =
- tclTHEN (generalize (List.map mkVar hyps)) (clear hyps) gl
+let pf_get_hyp_val gl id =
+ let (_, b, _) = pf_get_hyp gl id in
+ b
+
+let revert hyps gl =
+ let lconstr = List.map (fun id ->
+ ((all_occurrences, mkVar id, pf_get_hyp_val gl id), Anonymous))
+ hyps
+ in tclTHEN (generalize_gen_let lconstr) (clear hyps) gl
(* Faudra-t-il une version avec plusieurs args de generalize_dep ?
-Cela peut-être troublant de faire "Generalize Dependent H n" dans
-"n:nat; H:n=n |- P(n)" et d'échouer parce que H a disparu après la
-généralisation dépendante par n.
+Cela peut-être troublant de faire "Generalize Dependent H n" dans
+"n:nat; H:n=n |- P(n)" et d'échouer parce que H a disparu après la
+généralisation dépendante par n.
let quantify lconstr =
List.fold_right
@@ -1487,9 +1499,9 @@ let quantify lconstr =
tclIDTAC
*)
-(* A dependent cut rule à la sequent calculus
+(* A dependent cut rule à la sequent calculus
------------------------------------------
- Sera simplifiable le jour où il y aura un let in primitif dans constr
+ Sera simplifiable le jour où il y aura un let in primitif dans constr
[letin_tac b na c (occ_hyp,occ_ccl) gl] transforms
[...x1:T1(c),...,x2:T2(c),... |- G(c)] into
@@ -1816,11 +1828,11 @@ let induct_discharge destopt avoid' tac (avoid,ra) names gl =
in
peel_tac ra names no_move gl
-(* - le recalcul de indtyp à chaque itération de atomize_one est pour ne pas
- s'embêter à regarder si un letin_tac ne fait pas des
+(* - le recalcul de indtyp à chaque itération de atomize_one est pour ne pas
+ s'embêter à regarder si un letin_tac ne fait pas des
substitutions aussi sur l'argument voisin *)
-(* Marche pas... faut prendre en compte l'occurrence précise... *)
+(* Marche pas... faut prendre en compte l'occurrence précise... *)
let atomize_param_of_ind (indref,nparams,_) hyp0 gl =
let tmptyp0 = pf_get_hyp_typ gl hyp0 in
@@ -1828,7 +1840,7 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 gl =
let prods, indtyp = decompose_prod typ0 in
let argl = snd (decompose_app indtyp) in
let params = list_firstn nparams argl in
- (* le gl est important pour ne pas préévaluer *)
+ (* le gl est important pour ne pas préévaluer *)
let rec atomize_one i avoid gl =
if i<>nparams then
let tmptyp0 = pf_get_hyp_typ gl hyp0 in
@@ -2116,31 +2128,25 @@ let error_ind_scheme s =
let s = if s <> "" then s^" " else s in
error ("Cannot recognize "^s^"an induction scheme.")
-let mkEq t x y =
- mkApp (build_coq_eq (), [| t; x; y |])
+let coq_eq = Lazy.lazy_from_fun Coqlib.build_coq_eq
+let coq_eq_refl = lazy ((Coqlib.build_coq_eq_data ()).Coqlib.refl)
-let mkRefl t x =
- mkApp ((build_coq_eq_data ()).refl, [| t; x |])
+let coq_heq = lazy (Coqlib.coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq")
+let coq_heq_refl = lazy (Coqlib.coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq_refl")
-let mkHEq t x u y =
- mkApp (coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq",
- [| t; x; u; y |])
+let mkEq t x y =
+ mkApp (Lazy.force coq_eq, [| refresh_universes_strict t; x; y |])
+
+let mkRefl t x =
+ mkApp (Lazy.force coq_eq_refl, [| refresh_universes_strict t; x |])
+let mkHEq t x u y =
+ mkApp (Lazy.force coq_heq,
+ [| refresh_universes_strict t; x; refresh_universes_strict u; y |])
+
let mkHRefl t x =
- mkApp (coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq_refl",
- [| t; x |])
-
-(* let id = lazy (coq_constant "mkHEq" ["Init";"Datatypes"] "id") *)
-
-(* let mkHEq t x u y = *)
-(* let ty = new_Type () in *)
-(* mkApp (coq_constant "mkHEq" ["Logic";"EqdepFacts"] "eq_dep", *)
-(* [| ty; mkApp (Lazy.force id, [|ty|]); t; x; u; y |]) *)
-
-(* let mkHRefl t x = *)
-(* let ty = new_Type () in *)
-(* mkApp (coq_constant "mkHEq" ["Logic";"EqdepFacts"] "eq_dep_intro", *)
-(* [| ty; mkApp (Lazy.force id, [|ty|]); t; x |]) *)
+ mkApp (Lazy.force coq_heq_refl,
+ [| refresh_universes_strict t; x |])
let lift_togethern n l =
let l', _ =
@@ -2157,8 +2163,8 @@ let lift_list l = List.map (lift 1) l
let ids_of_constr vars c =
let rec aux vars c =
match kind_of_term c with
- | Var id -> if List.mem id vars then vars else id :: vars
- | App (f, args) ->
+ | Var id -> Idset.add id vars
+ | App (f, args) ->
(match kind_of_term f with
| Construct (ind,_)
| Ind ind ->
@@ -2168,6 +2174,16 @@ let ids_of_constr vars c =
| _ -> fold_constr aux vars c)
| _ -> fold_constr aux vars c
in aux vars c
+
+let decompose_indapp f args =
+ match kind_of_term f with
+ | Construct (ind,_)
+ | Ind ind ->
+ let (mib,mip) = Global.lookup_inductive ind in
+ let first = mib.Declarations.mind_nparams_rec in
+ let pars, args = array_chop first args in
+ mkApp (f, pars), args
+ | _ -> f, args
let mk_term_eq env sigma ty t ty' t' =
if Reductionops.is_conv env sigma ty ty' then
@@ -2203,24 +2219,52 @@ let make_abstract_generalize gl id concl dep ctx c eqs args refls =
let appeqs = mkApp (instc, Array.of_list refls) in
(* Finaly, apply the reflexivity proof for the original hyp, to get a term of type gl again. *)
mkApp (appeqs, abshypt)
-
-let abstract_args gl id =
+
+let deps_of_var id env =
+ Environ.fold_named_context
+ (fun _ (n,b,t) (acc : Idset.t) ->
+ if Option.cata (occur_var env id) false b || occur_var env id t then
+ Idset.add n acc
+ else acc)
+ env ~init:Idset.empty
+
+let idset_of_list =
+ List.fold_left (fun s x -> Idset.add x s) Idset.empty
+
+let hyps_of_vars env sign nogen hyps =
+ if Idset.is_empty hyps then []
+ else
+ let (_,lh) =
+ Sign.fold_named_context_reverse
+ (fun (hs,hl) (x,_,_ as d) ->
+ if Idset.mem x nogen then (hs,hl)
+ else if Idset.mem x hs then (hs,x::hl)
+ else
+ let xvars = global_vars_set_of_decl env d in
+ if not (Idset.equal (Idset.diff xvars hs) Idset.empty) then
+ (Idset.add x hs, x :: hl)
+ else (hs, hl))
+ ~init:(hyps,[])
+ sign
+ in lh
+
+let abstract_args gl generalize_vars dep id =
let c = pf_get_hyp_typ gl id in
let sigma = project gl in
let env = pf_env gl in
let concl = pf_concl gl in
- let dep = dependent (mkVar id) concl in
+ let dep = dep || dependent (mkVar id) concl in
let avoid = ref [] in
let get_id name =
let id = fresh_id !avoid (match name with Name n -> n | Anonymous -> id_of_string "gen_x") gl in
avoid := id :: !avoid; id
in
- match kind_of_term c with
- App (f, args) ->
+ match kind_of_term c with
+ | App (f, args) ->
(* Build application generalized w.r.t. the argument plus the necessary eqs.
From env |- c : forall G, T and args : G we build
(T[G'], G' : ctx, env ; G' |- args' : G, eqs := G'_i = G_i, refls : G' = G, vars to generalize)
-
+
eqs are not lifted w.r.t. each other yet. (* will be needed when going to dependent indexes *)
*)
let aux (prod, ctx, ctxenv, c, args, eqs, refls, vars, env) arg =
@@ -2232,8 +2276,9 @@ let abstract_args gl id =
let liftargty = lift (List.length ctx) argty in
let convertible = Reductionops.is_conv_leq ctxenv sigma liftargty ty in
match kind_of_term arg with
-(* | Var _ | Rel _ | Ind _ when convertible -> *)
-(* (subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls, vars, env) *)
+(* | Var id -> *)
+(* let deps = deps_of_var id env in *)
+(* (subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls, Idset.union deps vars, env) *)
| _ ->
let name = get_id name in
let decl = (Name name, None, ty) in
@@ -2249,53 +2294,109 @@ let abstract_args gl id =
in
let eqs = eq :: lift_list eqs in
let refls = refl :: refls in
- let vars = ids_of_constr vars arg in
- (arity, ctx, push_rel decl ctxenv, c', args, eqs, refls, vars, env)
+ let argvars = ids_of_constr vars arg in
+ (arity, ctx, push_rel decl ctxenv, c', args, eqs, refls, Idset.union argvars vars, env)
+ in
+ let f', args' = decompose_indapp f args in
+ let dogen, f', args' =
+ if not (array_distinct args) then true, f', args'
+ else
+ match array_find_i (fun i x -> not (isVar x)) args' with
+ | None -> false, f', args'
+ | Some nonvar ->
+ let before, after = array_chop nonvar args' in
+ true, mkApp (f', before), after
in
- let f, args =
- match kind_of_term f with
- | Construct (ind,_)
- | Ind ind ->
- let (mib,mip) = Global.lookup_inductive ind in
- let first = mib.Declarations.mind_nparams in
- let pars, args = array_chop first args in
- mkApp (f, pars), args
- | _ -> f, args
- in
- (match args with [||] -> None
- | _ ->
- let arity, ctx, ctxenv, c', args, eqs, refls, vars, env =
- Array.fold_left aux (pf_type_of gl f,[],env,f,[],[],[],[],env) args
- in
- let args, refls = List.rev args, List.rev refls in
- Some (make_abstract_generalize gl id concl dep ctx c' eqs args refls,
- dep, succ (List.length ctx), vars))
+ if dogen then
+ let arity, ctx, ctxenv, c', args, eqs, refls, vars, env =
+ Array.fold_left aux (pf_type_of gl f',[],env,f',[],[],[],Idset.empty,env) args'
+ in
+ let args, refls = List.rev args, List.rev refls in
+ let vars =
+ if generalize_vars then
+ let nogen = Idset.add id Idset.empty in
+ hyps_of_vars (pf_env gl) (pf_hyps gl) nogen vars
+ else []
+ in
+ Some (make_abstract_generalize gl id concl dep ctx c' eqs args refls,
+ dep, succ (List.length ctx), vars)
+ else None
| _ -> None
-let abstract_generalize id ?(generalize_vars=true) gl =
+let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id gl =
Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
let oldid = pf_get_new_id id gl in
- let newc = abstract_args gl id in
+ let newc = abstract_args gl generalize_vars force_dep id in
match newc with
- | None -> tclIDTAC gl
- | Some (newc, dep, n, vars) ->
- let tac =
- if dep then
- tclTHENLIST [refine newc; rename_hyp [(id, oldid)]; tclDO n intro;
- generalize_dep (mkVar oldid)]
- else
- tclTHENLIST [refine newc; clear [id]; tclDO n intro]
- in
- if generalize_vars then tclTHEN tac
- (tclFIRST [revert (List.rev vars) ;
- tclMAP (fun id -> tclTRY (generalize_dep (mkVar id))) vars]) gl
- else tac gl
+ | None -> tclIDTAC gl
+ | Some (newc, dep, n, vars) ->
+ let tac =
+ if dep then
+ tclTHENLIST [refine newc; rename_hyp [(id, oldid)]; tclDO n intro;
+ generalize_dep (mkVar oldid)]
+ else
+ tclTHENLIST [refine newc; clear [id]; tclDO n intro]
+ in
+ if vars = [] then tac gl
+ else tclTHEN tac
+ (fun gl -> tclFIRST [revert vars ;
+ tclMAP (fun id -> tclTRY (generalize_dep (mkVar id))) vars] gl) gl
+
+let specialize_hypothesis id gl =
+ let env = pf_env gl in
+ let ty = pf_get_hyp_typ gl id in
+ let evars = ref (create_evar_defs (project gl)) in
+ let unif env evars c1 c2 = Evarconv.e_conv env evars c2 c1 in
+ let rec aux in_eqs ctx acc ty =
+ match kind_of_term ty with
+ | Prod (na, t, b) ->
+ (match kind_of_term t with
+ | App (eq, [| eqty; x; y |]) when eq_constr eq (Lazy.force coq_eq) ->
+ let c = if noccur_between 1 (List.length ctx) x then y else x in
+ let pt = mkApp (Lazy.force coq_eq, [| eqty; c; c |]) in
+ let p = mkApp (Lazy.force coq_eq_refl, [| eqty; c |]) in
+ if unif (push_rel_context ctx env) evars pt t then
+ aux true ctx (mkApp (acc, [| p |])) (subst1 p b)
+ else acc, in_eqs, ctx, ty
+ | App (heq, [| eqty; x; eqty'; y |]) when eq_constr heq (Lazy.force coq_heq) ->
+ let eqt, c = if noccur_between 1 (List.length ctx) x then eqty', y else eqty, x in
+ let pt = mkApp (Lazy.force coq_heq, [| eqt; c; eqt; c |]) in
+ let p = mkApp (Lazy.force coq_heq_refl, [| eqt; c |]) in
+ if unif (push_rel_context ctx env) evars pt t then
+ aux true ctx (mkApp (acc, [| p |])) (subst1 p b)
+ else acc, in_eqs, ctx, ty
+ | _ ->
+ if in_eqs then acc, in_eqs, ctx, ty
+ else
+ let e = e_new_evar evars (push_rel_context ctx env) t in
+ aux false ((na, Some e, t) :: ctx) (mkApp (lift 1 acc, [| mkRel 1 |])) b)
+ | t -> acc, in_eqs, ctx, ty
+ in
+ let acc, worked, ctx, ty = aux false [] (mkVar id) ty in
+ let ctx' = nf_rel_context_evar !evars ctx in
+ let ctx'' = List.map (fun (n,b,t as decl) ->
+ match b with
+ | Some k when isEvar k -> (n,None,t)
+ | b -> decl) ctx'
+ in
+ let ty' = it_mkProd_or_LetIn ty ctx'' in
+ let acc' = it_mkLambda_or_LetIn acc ctx'' in
+ let ty' = Tacred.whd_simpl env !evars ty'
+ and acc' = Tacred.whd_simpl env !evars acc' in
+ let ty' = Evarutil.nf_isevar !evars ty' in
+ if worked then
+ tclTHENFIRST (Tacmach.internal_cut true id ty')
+ (exact_no_check (refresh_universes_strict acc')) gl
+ else tclFAIL 0 (str "Nothing to do in hypothesis " ++ pr_id id) gl
+
let dependent_pattern c gl =
let cty = pf_type_of gl c in
let deps =
match kind_of_term cty with
- | App (f, args) -> Array.to_list args
+ | App (f, args) ->
+ let f', args' = decompose_indapp f args in
+ Array.to_list args'
| _ -> []
in
let varname c = match kind_of_term c with
@@ -2500,7 +2601,7 @@ let compute_elim_sig ?elimc elimt =
let compute_scheme_signature scheme names_info ind_type_guess =
let f,l = decompose_app scheme.concl in
- (* Vérifier que les arguments de Qi sont bien les xi. *)
+ (* Vérifier que les arguments de Qi sont bien les xi. *)
match scheme.indarg with
| Some (_,Some _,_) -> error "Strange letin, cannot recognize an induction scheme."
| None -> (* Non standard scheme *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index cedcbf7ca..7d65ab752 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -375,7 +375,8 @@ val tclABSTRACT : identifier option -> tactic -> tactic
val admit_as_an_axiom : tactic
-val abstract_generalize : identifier -> ?generalize_vars:bool -> tactic
+val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> identifier -> tactic
+val specialize_hypothesis : identifier -> tactic
val dependent_pattern : constr -> tactic
diff --git a/test-suite/success/Equations.v b/test-suite/success/Equations.v
deleted file mode 100644
index d6e17f30d..000000000
--- a/test-suite/success/Equations.v
+++ /dev/null
@@ -1,321 +0,0 @@
-Require Import Program.
-
-Equations neg (b : bool) : bool :=
-neg true := false ;
-neg false := true.
-
-Eval compute in neg.
-
-Require Import Coq.Lists.List.
-
-Equations head A (default : A) (l : list A) : A :=
-head A default nil := default ;
-head A default (cons a v) := a.
-
-Eval compute in head.
-
-Equations tail {A} (l : list A) : (list A) :=
-tail A nil := nil ;
-tail A (cons a v) := v.
-
-Eval compute in @tail.
-
-Eval compute in (tail (cons 1 nil)).
-
-Reserved Notation " x ++ y " (at level 60, right associativity).
-
-Equations app' {A} (l l' : list A) : (list A) :=
-app' A nil l := l ;
-app' A (cons a v) l := cons a (app' v l).
-
-Equations app (l l' : list nat) : list nat :=
- [] ++ l := l ;
- (a :: v) ++ l := a :: (v ++ l)
-
-where " x ++ y " := (app x y).
-
-Eval compute in @app'.
-
-Equations zip' {A} (f : A -> A -> A) (l l' : list A) : (list A) :=
-zip' A f nil nil := nil ;
-zip' A f (cons a v) (cons b w) := cons (f a b) (zip' f v w) ;
-zip' A f nil (cons b w) := nil ;
-zip' A f (cons a v) nil := nil.
-
-
-Eval compute in @zip'.
-
-Equations zip'' {A} (f : A -> A -> A) (l l' : list A) (def : list A) : (list A) :=
-zip'' A f nil nil def := nil ;
-zip'' A f (cons a v) (cons b w) def := cons (f a b) (zip'' f v w def) ;
-zip'' A f nil (cons b w) def := def ;
-zip'' A f (cons a v) nil def := def.
-
-Eval compute in @zip''.
-
-Inductive fin : nat -> Set :=
-| fz : Π {n}, fin (S n)
-| fs : Π {n}, fin n -> fin (S n).
-
-Inductive finle : Π (n : nat) (x : fin n) (y : fin n), Prop :=
-| leqz : Π {n j}, finle (S n) fz j
-| leqs : Π {n i j}, finle n i j -> finle (S n) (fs i) (fs j).
-
-Scheme finle_ind_dep := Induction for finle Sort Prop.
-
-Instance finle_ind_pack n x y : DependentEliminationPackage (finle n x y) :=
- { elim_type := _ ; elim := finle_ind_dep }.
-
-Implicit Arguments finle [[n]].
-
-Require Import Bvector.
-
-Implicit Arguments Vnil [[A]].
-Implicit Arguments Vcons [[A] [n]].
-
-Equations vhead {A n} (v : vector A (S n)) : A :=
-vhead A n (Vcons a v) := a.
-
-Equations vmap {A B} (f : A -> B) {n} (v : vector A n) : (vector B n) :=
-vmap A B f 0 Vnil := Vnil ;
-vmap A B f (S n) (Vcons a v) := Vcons (f a) (vmap f v).
-
-Eval compute in (vmap id (@Vnil nat)).
-Eval compute in (vmap id (@Vcons nat 2 _ Vnil)).
-Eval compute in @vmap.
-
-Equations Below_nat (P : nat -> Type) (n : nat) : Type :=
-Below_nat P 0 := unit ;
-Below_nat P (S n) := prod (P n) (Below_nat P n).
-
-Equations below_nat (P : nat -> Type) n (step : Π (n : nat), Below_nat P n -> P n) : Below_nat P n :=
-below_nat P 0 step := tt ;
-below_nat P (S n) step := let rest := below_nat P n step in
- (step n rest, rest).
-
-Class BelowPack (A : Type) :=
- { Below : Type ; below : Below }.
-
-Instance nat_BelowPack : BelowPack nat :=
- { Below := Π P n step, Below_nat P n ;
- below := λ P n step, below_nat P n (step P) }.
-
-Definition rec_nat (P : nat -> Type) n (step : Π n, Below_nat P n -> P n) : P n :=
- step n (below_nat P n step).
-
-Fixpoint Below_vector (P : Π A n, vector A n -> Type) A n (v : vector A n) : Type :=
- match v with Vnil => unit | Vcons a n' v' => prod (P A n' v') (Below_vector P A n' v') end.
-
-Equations below_vector (P : Π A n, vector A n -> Type) A n (v : vector A n)
- (step : Π A n (v : vector A n), Below_vector P A n v -> P A n v) : Below_vector P A n v :=
-below_vector P A ?(0) Vnil step := tt ;
-below_vector P A ?(S n) (Vcons a v) step :=
- let rest := below_vector P A n v step in
- (step A n v rest, rest).
-
-Instance vector_BelowPack : BelowPack (Π A n, vector A n) :=
- { Below := Π P A n v step, Below_vector P A n v ;
- below := λ P A n v step, below_vector P A n v (step P) }.
-
-Instance vector_noargs_BelowPack A n : BelowPack (vector A n) :=
- { Below := Π P v step, Below_vector P A n v ;
- below := λ P v step, below_vector P A n v (step P) }.
-
-Definition rec_vector (P : Π A n, vector A n -> Type) A n v
- (step : Π A n (v : vector A n), Below_vector P A n v -> P A n v) : P A n v :=
- step A n v (below_vector P A n v step).
-
-Class Recursor (A : Type) (BP : BelowPack A) :=
- { rec_type : Π x : A, Type ; rec : Π x : A, rec_type x }.
-
-Instance nat_Recursor : Recursor nat nat_BelowPack :=
- { rec_type := λ n, Π P step, P n ;
- rec := λ n P step, rec_nat P n (step P) }.
-
-(* Instance vect_Recursor : Recursor (Π A n, vector A n) vector_BelowPack := *)
-(* rec_type := Π (P : Π A n, vector A n -> Type) step A n v, P A n v; *)
-(* rec := λ P step A n v, rec_vector P A n v step. *)
-
-Instance vect_Recursor_noargs A n : Recursor (vector A n) (vector_noargs_BelowPack A n) :=
- { rec_type := λ v, Π (P : Π A n, vector A n -> Type) step, P A n v;
- rec := λ v P step, rec_vector P A n v step }.
-
-Implicit Arguments Below_vector [P A n].
-
-Notation " x ~= y " := (@JMeq _ x _ y) (at level 70, no associativity).
-
-(** Won't pass the guardness check which diverges anyway. *)
-
-(* Equations trans {n} {i j k : fin n} (p : finle i j) (q : finle j k) : finle i k := *)
-(* trans ?(S n) ?(fz) ?(j) ?(k) leqz q := leqz ; *)
-(* trans ?(S n) ?(fs i) ?(fs j) ?(fs k) (leqs p) (leqs q) := leqs (trans p q). *)
-
-(* Lemma trans_eq1 n (j k : fin (S n)) (q : finle j k) : trans leqz q = leqz. *)
-(* Proof. intros. simplify_equations ; reflexivity. Qed. *)
-
-(* Lemma trans_eq2 n i j k p q : @trans (S n) (fs i) (fs j) (fs k) (leqs p) (leqs q) = leqs (trans p q). *)
-(* Proof. intros. simplify_equations ; reflexivity. Qed. *)
-
-Section Image.
- Context {S T : Type}.
- Variable f : S -> T.
-
- Inductive Imf : T -> Type := imf (s : S) : Imf (f s).
-
- Equations inv (t : T) (im : Imf t) : S :=
- inv (f s) (imf s) := s.
-
-End Image.
-
-Section Univ.
-
- Inductive univ : Set :=
- | ubool | unat | uarrow (from:univ) (to:univ).
-
- Equations interp (u : univ) : Type :=
- interp ubool := bool ; interp unat := nat ;
- interp (uarrow from to) := interp from -> interp to.
-
- Equations foo (u : univ) (el : interp u) : interp u :=
- foo ubool true := false ;
- foo ubool false := true ;
- foo unat t := t ;
- foo (uarrow from to) f := id ∘ f.
-
- Eval lazy beta delta [ foo foo_obligation_1 foo_obligation_2 ] iota zeta in foo.
-
-End Univ.
-
-Eval compute in (foo ubool false).
-Eval compute in (foo (uarrow ubool ubool) negb).
-Eval compute in (foo (uarrow ubool ubool) id).
-
-Inductive foobar : Set := bar | baz.
-
-Equations bla (f : foobar) : bool :=
-bla bar := true ;
-bla baz := false.
-
-Eval simpl in bla.
-Print refl_equal.
-
-Notation "'refl'" := (@refl_equal _ _).
-
-Equations K {A} (x : A) (P : x = x -> Type) (p : P (refl_equal x)) (p : x = x) : P p :=
-K A x P p refl := p.
-
-Equations eq_sym {A} (x y : A) (H : x = y) : y = x :=
-eq_sym A x x refl := refl.
-
-Equations eq_trans {A} (x y z : A) (p : x = y) (q : y = z) : x = z :=
-eq_trans A x x x refl refl := refl.
-
-Lemma eq_trans_eq A x : @eq_trans A x x x refl refl = refl.
-Proof. reflexivity. Qed.
-
-Equations nth {A} {n} (v : vector A n) (f : fin n) : A :=
-nth A (S n) (Vcons a v) fz := a ;
-nth A (S n) (Vcons a v) (fs f) := nth v f.
-
-Equations tabulate {A} {n} (f : fin n -> A) : vector A n :=
-tabulate A 0 f := Vnil ;
-tabulate A (S n) f := Vcons (f fz) (tabulate (f ∘ fs)).
-
-Equations vlast {A} {n} (v : vector A (S n)) : A :=
-vlast A 0 (Vcons a Vnil) := a ;
-vlast A (S n) (Vcons a (n:=S n) v) := vlast v.
-
-Print Assumptions vlast.
-
-Equations vlast' {A} {n} (v : vector A (S n)) : A :=
-vlast' A ?(0) (Vcons a Vnil) := a ;
-vlast' A ?(S n) (Vcons a (n:=S n) v) := vlast' v.
-
-Lemma vlast_equation1 A (a : A) : vlast' (Vcons a Vnil) = a.
-Proof. intros. simplify_equations. reflexivity. Qed.
-
-Lemma vlast_equation2 A n a v : @vlast' A (S n) (Vcons a v) = vlast' v.
-Proof. intros. simplify_equations ; reflexivity. Qed.
-
-Print Assumptions vlast'.
-Print Assumptions nth.
-Print Assumptions tabulate.
-
-Extraction vlast.
-Extraction vlast'.
-
-Equations vliat {A} {n} (v : vector A (S n)) : vector A n :=
-vliat A 0 (Vcons a Vnil) := Vnil ;
-vliat A (S n) (Vcons a v) := Vcons a (vliat v).
-
-Eval compute in (vliat (Vcons 2 (Vcons 5 (Vcons 4 Vnil)))).
-
-Equations vapp' {A} {n m} (v : vector A n) (w : vector A m) : vector A (n + m) :=
-vapp' A ?(0) m Vnil w := w ;
-vapp' A ?(S n) m (Vcons a v) w := Vcons a (vapp' v w).
-
-Eval compute in @vapp'.
-
-Fixpoint vapp {A n m} (v : vector A n) (w : vector A m) : vector A (n + m) :=
- match v with
- | Vnil => w
- | Vcons a n' v' => Vcons a (vapp v' w)
- end.
-
-Lemma JMeq_Vcons_inj A n m a (x : vector A n) (y : vector A m) : n = m -> JMeq x y -> JMeq (Vcons a x) (Vcons a y).
-Proof. intros until y. simplify_dep_elim. reflexivity. Qed.
-
-Equations NoConfusion_fin (P : Prop) {n : nat} (x y : fin n) : Prop :=
-NoConfusion_fin P (S n) fz fz := P -> P ;
-NoConfusion_fin P (S n) fz (fs y) := P ;
-NoConfusion_fin P (S n) (fs x) fz := P ;
-NoConfusion_fin P (S n) (fs x) (fs y) := (x = y -> P) -> P.
-
-Eval compute in NoConfusion_fin.
-Eval compute in NoConfusion_fin_comp.
-
-Print Assumptions NoConfusion_fin.
-
-Eval compute in (fun P n => NoConfusion_fin P (n:=S n) fz fz).
-
-(* Equations noConfusion_fin P (n : nat) (x y : fin n) (H : x = y) : NoConfusion_fin P x y := *)
-(* noConfusion_fin P (S n) fz fz refl := λ p _, p ; *)
-(* noConfusion_fin P (S n) (fs x) (fs x) refl := λ p : x = x -> P, p refl. *)
-
-Equations_nocomp NoConfusion_vect (P : Prop) {A n} (x y : vector A n) : Prop :=
-NoConfusion_vect P A 0 Vnil Vnil := P -> P ;
-NoConfusion_vect P A (S n) (Vcons a x) (Vcons b y) := (a = b -> x = y -> P) -> P.
-
-Equations noConfusion_vect (P : Prop) A n (x y : vector A n) (H : x = y) : NoConfusion_vect P x y :=
-noConfusion_vect P A 0 Vnil Vnil refl := λ p, p ;
-noConfusion_vect P A (S n) (Vcons a v) (Vcons a v) refl := λ p : a = a -> v = v -> P, p refl refl.
-
-(* Instance fin_noconf n : NoConfusionPackage (fin n) := *)
-(* NoConfusion := λ P, Π x y, x = y -> NoConfusion_fin P x y ; *)
-(* noConfusion := λ P x y, noConfusion_fin P n x y. *)
-
-Instance vect_noconf A n : NoConfusionPackage (vector A n) :=
- { NoConfusion := λ P, Π x y, x = y -> NoConfusion_vect P x y ;
- noConfusion := λ P x y, noConfusion_vect P A n x y }.
-
-Equations fog {n} (f : fin n) : nat :=
-fog (S n) fz := 0 ; fog (S n) (fs f) := S (fog f).
-
-Inductive Split {X : Set}{m n : nat} : vector X (m + n) -> Set :=
- append : Π (xs : vector X m)(ys : vector X n), Split (vapp xs ys).
-
-Implicit Arguments Split [[X]].
-
-Equations_nocomp split {X : Set}(m n : nat) (xs : vector X (m + n)) : Split m n xs :=
-split X 0 n xs := append Vnil xs ;
-split X (S m) n (Vcons x xs) :=
- let 'append xs' ys' in Split _ _ vec := split m n xs return Split (S m) n (Vcons x vec) in
- append (Vcons x xs') ys'.
-
-Eval compute in (split 0 1 (vapp Vnil (Vcons 2 Vnil))).
-Eval compute in (split _ _ (vapp (Vcons 3 Vnil) (Vcons 2 Vnil))).
-
-Extraction Inline split_obligation_1 split_obligation_2.
-Recursive Extraction split.
-
-Eval compute in @split.
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v
index 54bfaa35c..f308bdfd9 100644
--- a/test-suite/success/dependentind.v
+++ b/test-suite/success/dependentind.v
@@ -1,4 +1,4 @@
-Require Import Coq.Program.Program.
+Require Import Coq.Program.Program Coq.Program.Equations.
Variable A : Set.
@@ -77,7 +77,7 @@ Proof with simpl in * ; eqns ; eauto with lambda.
destruct Δ as [|Δ τ'']...
apply abs.
- specialize (IHterm (Δ, τ'', τ0) Γ)...
+ specialize (IHterm Γ (Δ, τ'', τ0) τ'0)...
intro. eapply app...
Defined.
@@ -98,7 +98,7 @@ Proof with simpl in * ; eqns ; eauto.
apply weak...
apply abs...
- specialize (IHterm (Δ, τ0))...
+ specialize (IHterm Γ (Δ, τ0))...
eapply app...
Defined.
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 0c77a1325..76dc09b26 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -1,4 +1,3 @@
-(* -*- coding: utf-8 -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -16,13 +15,31 @@ Require Export JMeq.
Require Import Coq.Program.Tactics.
+Ltac is_ground_goal :=
+ match goal with
+ |- ?T => is_ground T
+ end.
+
+(** Try to find a contradiction. *)
+
+Hint Extern 10 => is_ground_goal ; progress (elimtype False).
+
+(** We will use the [block] definition to separate the goal from the
+ equalities generated by the tactic. *)
+
+Definition block {A : Type} (a : A) := a.
+
+Ltac block_goal := match goal with [ |- ?T ] => change (block T) end.
+Ltac unblock_goal := unfold block in *.
+
(** Notation for heterogenous equality. *)
-Notation " [ x : X ] = [ y : Y ] " := (@JMeq X x Y y) (at level 0, X at next level, Y at next level).
+Notation " x ~= y " := (@JMeq _ x _ y) (at level 70, no associativity).
-(** Notation for the single element of [x = x] *)
+(** Notation for the single element of [x = x] and [x ~= x]. *)
-Notation "'refl'" := (@refl_equal _ _).
+Implicit Arguments eq_refl [[A] [x]].
+Implicit Arguments JMeq_refl [[A] [x]].
(** Do something on an heterogeneous equality appearing in the context. *)
@@ -77,7 +94,7 @@ Ltac elim_eq_rect :=
end
end.
-(** Rewrite using uniqueness of indentity proofs [H = refl_equal X]. *)
+(** Rewrite using uniqueness of indentity proofs [H = eq_refl]. *)
Ltac simpl_uip :=
match goal with
@@ -152,8 +169,21 @@ Ltac clear_eq_proofs :=
Hint Rewrite <- eq_rect_eq : refl_id.
-(** The refl_id database should be populated with lemmas of the form
- [coerce_* t (refl_equal _) = t]. *)
+(** The [refl_id] database should be populated with lemmas of the form
+ [coerce_* t eq_refl = t]. *)
+
+Lemma JMeq_eq_refl {A} (x : A) : JMeq_eq (@JMeq_refl _ x) = eq_refl.
+Proof. intros. apply proof_irrelevance. Qed.
+
+Lemma UIP_refl_refl : Π A (x : A),
+ Eqdep.EqdepTheory.UIP_refl A x eq_refl = eq_refl.
+Proof. intros. apply UIP_refl. Qed.
+
+Lemma inj_pairT2_refl : Π A (x : A) (P : A -> Type) (p : P x),
+ Eqdep.EqdepTheory.inj_pairT2 A P x p p eq_refl = eq_refl.
+Proof. intros. apply UIP_refl. Qed.
+
+Hint Rewrite @JMeq_eq_refl @UIP_refl_refl @inj_pairT2_refl : refl_id.
Ltac rewrite_refl_id := autorewrite with refl_id.
@@ -189,45 +219,12 @@ Ltac simplify_eqs :=
(** A tactic that tries to remove trivial equality guards in induction hypotheses coming
from [dependent induction]/[generalize_eqs] invocations. *)
-Ltac simpl_IH_eq H :=
- match type of H with
- | @JMeq _ ?x _ _ -> _ =>
- refine_hyp (H (JMeq_refl x))
- | _ -> @JMeq _ ?x _ _ -> _ =>
- refine_hyp (H _ (JMeq_refl x))
- | _ -> _ -> @JMeq _ ?x _ _ -> _ =>
- refine_hyp (H _ _ (JMeq_refl x))
- | _ -> _ -> _ -> @JMeq _ ?x _ _ -> _ =>
- refine_hyp (H _ _ _ (JMeq_refl x))
- | _ -> _ -> _ -> _ -> @JMeq _ ?x _ _ -> _ =>
- refine_hyp (H _ _ _ _ (JMeq_refl x))
- | _ -> _ -> _ -> _ -> _ -> @JMeq _ ?x _ _ -> _ =>
- refine_hyp (H _ _ _ _ _ (JMeq_refl x))
- | ?x = _ -> _ =>
- refine_hyp (H (refl_equal x))
- | _ -> ?x = _ -> _ =>
- refine_hyp (H _ (refl_equal x))
- | _ -> _ -> ?x = _ -> _ =>
- refine_hyp (H _ _ (refl_equal x))
- | _ -> _ -> _ -> ?x = _ -> _ =>
- refine_hyp (H _ _ _ (refl_equal x))
- | _ -> _ -> _ -> _ -> ?x = _ -> _ =>
- refine_hyp (H _ _ _ _ (refl_equal x))
- | _ -> _ -> _ -> _ -> _ -> ?x = _ -> _ =>
- refine_hyp (H _ _ _ _ _ (refl_equal x))
- end.
-
-Ltac simpl_IH_eqs H := repeat simpl_IH_eq H.
-
-Ltac do_simpl_IHs_eqs :=
+Ltac simplify_IH_hyps := repeat
match goal with
- | [ H : context [ @JMeq _ _ _ _ -> _ ] |- _ ] => progress (simpl_IH_eqs H)
- | [ H : context [ _ = _ -> _ ] |- _ ] => progress (simpl_IH_eqs H)
+ | [ hyp : _ |- _ ] => specialize_hypothesis hyp
end.
-Ltac simpl_IHs_eqs := repeat do_simpl_IHs_eqs.
-
-(** We split substitution tactics in the two directions depending on which
+(** We split substitution tactics in the two directions depending on which
names we want to keep corresponding to the generalization performed by the
[generalize_eqs] tactic. *)
@@ -250,33 +247,16 @@ Ltac inject_right H :=
Ltac autoinjections_left := repeat autoinjection ltac:inject_left.
Ltac autoinjections_right := repeat autoinjection ltac:inject_right.
-Ltac simpl_depind := subst_no_fail ; autoinjections ; try discriminates ;
- simpl_JMeq ; simpl_existTs ; simpl_IHs_eqs.
-
-Ltac simpl_depind_l := subst_left_no_fail ; autoinjections_left ; try discriminates ;
- simpl_JMeq ; simpl_existTs ; simpl_IHs_eqs.
+Ltac simpl_depind := subst_no_fail ; autoinjections ; try discriminates ;
+ simpl_JMeq ; simpl_existTs ; simplify_IH_hyps.
-Ltac simpl_depind_r := subst_right_no_fail ; autoinjections_right ; try discriminates ;
- simpl_JMeq ; simpl_existTs ; simpl_IHs_eqs.
+Ltac simpl_depind_l := subst_left_no_fail ; autoinjections_left ; try discriminates ;
+ simpl_JMeq ; simpl_existTs ; simplify_IH_hyps.
-(** Support for the [Equations] command.
- These tactics implement the necessary machinery to solve goals produced by the
- [Equations] command relative to dependent pattern-matching.
- It is completely inspired from the "Eliminating Dependent Pattern-Matching" paper by
- Goguen, McBride and McKinna. *)
+Ltac simpl_depind_r := subst_right_no_fail ; autoinjections_right ; try discriminates ;
+ simpl_JMeq ; simpl_existTs ; simplify_IH_hyps.
-
-(** The NoConfusionPackage class provides a method for making progress on proving a property
- [P] implied by an equality on an inductive type [I]. The type of [noConfusion] for a given
- [P] should be of the form [ Π Δ, (x y : I Δ) (x = y) -> NoConfusion P x y ], where
- [NoConfusion P x y] for constructor-headed [x] and [y] will give a formula ending in [P].
- This gives a general method for simplifying by discrimination or injectivity of constructors.
-
- Some actual instances are defined later in the file using the more primitive [discriminate] and
- [injection] tactics on which we can always fall back.
- *)
-
-Class NoConfusionPackage (I : Type) := { NoConfusion : Π P : Prop, Type ; noConfusion : Π P, NoConfusion P }.
+Ltac blocked t := block_goal ; t ; unblock_goal.
(** The [DependentEliminationPackage] provides the default dependent elimination principle to
be used by the [equations] resolver. It is especially useful to register the dependent elimination
@@ -299,18 +279,6 @@ Ltac elim_tac tac p :=
Ltac elim_case p := elim_tac ltac:(fun p el => destruct p using el) p.
Ltac elim_ind p := elim_tac ltac:(fun p el => induction p using el) p.
-(** The [BelowPackage] class provides the definition of a [Below] predicate for some datatype,
- allowing to talk about course-of-value recursion on it. *)
-
-Class BelowPackage (A : Type) := {
- Below : A -> Type ;
- below : Π (a : A), Below a }.
-
-(** The [Recursor] class defines a recursor on a type, based on some definition of [Below]. *)
-
-Class Recursor (A : Type) (BP : BelowPackage A) :=
- { rec_type : A -> Type ; rec : Π (a : A), rec_type a }.
-
(** Lemmas used by the simplifier, mainly rephrasings of [eq_rect], [eq_ind]. *)
Lemma solution_left : Π A (B : A -> Type) (t : A), B t -> (Π x, x = t -> B x).
@@ -332,25 +300,16 @@ Proof. intros. apply X. apply inj_pair2. exact H. Defined.
Lemma simplification_existT1 : Π A (P : A -> Type) B (p q : A) (x : P p) (y : P q),
(p = q -> existT P p x = existT P q y -> B) -> (existT P p x = existT P q y -> B).
Proof. intros. injection H. intros ; auto. Defined.
-
-Lemma simplification_K : Π A (x : A) (B : x = x -> Type), B (refl_equal x) -> (Π p : x = x, B p).
+
+Lemma simplification_K : Π A (x : A) (B : x = x -> Type), B eq_refl -> (Π p : x = x, B p).
Proof. intros. rewrite (UIP_refl A). assumption. Defined.
-(** Simply unfold as much as possible. *)
-
-Ltac unfold_equations :=
- unfold solution_left, solution_right, deletion, simplification_heq,
- simplification_existT1, simplification_existT2, eq_rect_r, eq_rec, eq_ind.
-
-(** The tactic [simplify_equations] is to be used when a program generated using [Equations]
- is in the goal. It simplifies it as much as possible, possibly using [K] if needed. *)
+(** This hint database and the following tactic can be used with [autounfold] to
+ unfold everything to [eq_rect]s. *)
-Ltac simplify_equations := repeat (unfold_equations ; simplify_eqs).
-
-(** We will use the [block_induction] definition to separate the goal from the
- equalities generated by the tactic. *)
-
-Definition block_dep_elim {A : Type} (a : A) := a.
+Hint Unfold solution_left solution_right deletion simplification_heq
+ simplification_existT1 simplification_existT2 simplification_K
+ eq_rect_r eq_rec eq_ind : dep_elim.
(** Using these we can make a simplifier that will perform the unification
steps needed to put the goal in normalised form (provided there are only
@@ -366,19 +325,18 @@ Ltac simplify_one_dep_elim_term c :=
refine (simplification_existT1 _ _ _ _ _ _ _ _)
| ?x = ?y -> _ => (* variables case *)
(let hyp := fresh in intros hyp ;
- move hyp before x ;
- generalize dependent x ; refine (solution_left _ _ _ _) ; intros until 0) ||
+ move hyp before x ; revert_until hyp ; generalize dependent x ;
+ refine (solution_left _ _ _ _)(* ; intros until 0 *)) ||
(let hyp := fresh in intros hyp ;
- move hyp before y ;
- generalize dependent y ; refine (solution_right _ _ _ _) ; intros until 0)
- | @eq ?A ?t ?u -> ?P => apply (noConfusion (I:=A) P)
+ move hyp before y ; revert_until hyp ; generalize dependent y ;
+ refine (solution_right _ _ _ _)(* ; intros until 0 *))
| ?f ?x = ?g ?y -> _ => let H := fresh in progress (intros H ; injection H ; clear H)
| ?t = ?u -> _ => let hyp := fresh in
intros hyp ; exfalso ; discriminate
| ?x = ?y -> _ => let hyp := fresh in
intros hyp ; (try (clear hyp ; (* If non dependent, don't clear it! *) fail 1)) ;
case hyp ; clear hyp
- | block_dep_elim ?T => fail 1 (* Do not put any part of the rhs in the hyps *)
+ | block ?T => fail 1 (* Do not put any part of the rhs in the hyps *)
| forall x, _ => intro x || (let H := fresh x in rename x into H ; intro x) (* Try to keep original names *)
| _ => intro
end.
@@ -393,161 +351,91 @@ Ltac simplify_one_dep_elim :=
Ltac simplify_dep_elim := repeat simplify_one_dep_elim.
-(** To dependent elimination on some hyp. *)
-
-Ltac depelim id :=
- generalize_eqs id ; destruct id ; simplify_dep_elim.
-
(** Do dependent elimination of the last hypothesis, but not simplifying yet
(used internally). *)
Ltac destruct_last :=
on_last_hyp ltac:(fun id => simpl in id ; generalize_eqs id ; destruct id).
-(** The rest is support tactics for the [Equations] command. *)
-
-(** Notation for inaccessible patterns. *)
-
-Definition inaccessible_pattern {A : Type} (t : A) := t.
-
-Notation "?( t )" := (inaccessible_pattern t).
-
-(** To handle sections, we need to separate the context in two parts:
- variables introduced by the section and the rest. We introduce a dummy variable
- between them to indicate that. *)
-
-CoInductive end_of_section := the_end_of_the_section.
-
-Ltac set_eos := let eos := fresh "eos" in
- assert (eos:=the_end_of_the_section).
-
-(** We have a specialized [reverse_local] tactic to reverse the goal until the begining of the
- section variables *)
-
-Ltac reverse_local :=
- match goal with
- | [ H : ?T |- _ ] =>
- match T with
- | end_of_section => idtac | _ => revert H ; reverse_local end
- | _ => idtac
- end.
-
-(** Do as much as possible to apply a method, trying to get the arguments right.
- !!Unsafe!! We use [auto] for the [_nocomp] variant of [Equations], in which case some
- non-dependent arguments of the method can remain after [apply]. *)
-
-Ltac simpl_intros m := ((apply m || refine m) ; auto) || (intro ; simpl_intros m).
-
-(** Hopefully the first branch suffices. *)
-
-Ltac try_intros m :=
- solve [ intros ; unfold block_dep_elim ; refine m || apply m ] ||
- solve [ unfold block_dep_elim ; simpl_intros m ].
-
-(** To solve a goal by inversion on a particular target. *)
-
-Ltac solve_empty target :=
- do_nat target intro ; exfalso ; destruct_last ; simplify_dep_elim.
-
-Ltac simplify_method tac := repeat (tac || simplify_one_dep_elim) ; reverse_local.
+Ltac introduce p := first [
+ match p with _ => (* Already there, generalize dependent hyps *)
+ generalize dependent p ; intros p
+ end
+ | intros until p | intros until 1 | intros ].
-(** Solving a method call: we can solve it by splitting on an empty family member
- or we must refine the goal until the body can be applied. *)
+Ltac do_case p := introduce p ; (destruct p || elim_case p || (case p ; clear p)).
+Ltac do_ind p := introduce p ; (induction p || elim_ind p).
-Ltac solve_method rec :=
- match goal with
- | [ H := ?body : nat |- _ ] => subst H ; clear ; abstract (simplify_method idtac ; solve_empty body)
- | [ H := [ ?body ] : ?T |- _ ] => clear H ; simplify_method ltac:(exact body) ; rec ; try_intros (body:T)
- end.
+(** The following tactics allow to do induction on an already instantiated inductive predicate
+ by first generalizing it and adding the proper equalities to the context, in a maner similar to
+ the BasicElim tactic of "Elimination with a motive" by Conor McBride. *)
-(** Impossible cases, by splitting on a given target. *)
+(** The [do_depelim] higher-order tactic takes an elimination tactic as argument and an hypothesis
+ and starts a dependent elimination using this tactic. *)
-Ltac solve_split :=
+Ltac is_introduced H :=
match goal with
- | [ |- let split := ?x : nat in _ ] => clear ; abstract (intros _ ; solve_empty x)
+ | [ H' : _ |- _ ] => match H' with H => idtac end
end.
-(** If defining recursive functions, the prototypes come first. *)
+Tactic Notation "intro_block" hyp(H) :=
+ (is_introduced H ; block_goal ; revert_until H) ||
+ (let H' := fresh H in intros until H' ; block_goal) || (intros ; block_goal).
-Ltac intro_prototypes :=
- match goal with
- | [ |- Π x : _, _ ] => intro ; intro_prototypes
- | _ => idtac
- end.
+Tactic Notation "intro_block_id" ident(H) :=
+ (is_introduced H ; block_goal ; revert_until H) ||
+ (let H' := fresh H in intros until H' ; block_goal) || (intros ; block_goal).
-Ltac introduce p := first [
- match p with _ => (* Already there, generalize dependent hyps *)
- generalize dependent p ; intros p
- end
- | intros until p | intros ].
+Ltac simpl_dep_elim := simplify_dep_elim ; simplify_IH_hyps ; unblock_goal.
-Ltac do_case p := introduce p ; (destruct p || elim_case p || (case p ; clear p)).
-Ltac do_ind p := introduce p ; (induction p || elim_ind p).
+Ltac do_intros H :=
+ (try intros until H) ; (intro_block_id H || intro_block H).
-Ltac dep_elimify := match goal with [ |- ?T ] => change (block_dep_elim T) end.
+Ltac do_depelim_nosimpl tac H := do_intros H ; generalize_eqs H ; tac H.
-Ltac un_dep_elimify := unfold block_dep_elim in *.
+Ltac do_depelim tac H := do_depelim_nosimpl tac H ; simpl_dep_elim.
-Ltac case_last := dep_elimify ;
- on_last_hyp ltac:(fun p =>
- let ty := type of p in
- match ty with
- | ?x = ?x => revert p ; refine (simplification_K _ x _ _)
- | ?x = ?y => revert p
- | _ => simpl in p ; generalize_eqs p ; do_case p
- end).
+Ltac do_depind tac H :=
+ (try intros until H) ; intro_block H ;
+ generalize_eqs_vars H ; tac H ; simplify_dep_elim ; simplify_IH_hyps ; unblock_goal.
-Ltac nonrec_equations :=
- solve [solve_equations (case_last) (solve_method idtac)] || solve [ solve_split ]
- || fail "Unnexpected equations goal".
+(** To dependent elimination on some hyp. *)
-Ltac recursive_equations :=
- solve [solve_equations (case_last) (solve_method ltac:intro)] || solve [ solve_split ]
- || fail "Unnexpected recursive equations goal".
+Ltac depelim id := do_depelim ltac:(fun hyp => do_case hyp) id.
-(** The [equations] tactic is the toplevel tactic for solving goals generated
- by [Equations]. *)
+(** Used internally. *)
-Ltac equations := set_eos ;
- match goal with
- | [ |- Π x : _, _ ] => intro ; recursive_equations
- | _ => nonrec_equations
- end.
-
-(** The following tactics allow to do induction on an already instantiated inductive predicate
- by first generalizing it and adding the proper equalities to the context, in a maner similar to
- the BasicElim tactic of "Elimination with a motive" by Conor McBride. *)
+Ltac depelim_nosimpl id := do_depelim_nosimpl ltac:(fun hyp => do_case hyp) id.
-(** The [do_depind] higher-order tactic takes an induction tactic as argument and an hypothesis
- and starts a dependent induction using this tactic. *)
+(** To dependent induction on some hyp. *)
-Ltac do_depind tac H :=
- (try intros until H) ; dep_elimify ; generalize_eqs_vars H ; tac H ; simplify_dep_elim ; un_dep_elimify.
+Ltac depind id := do_depind ltac:(fun hyp => do_ind hyp) id.
(** A variant where generalized variables should be given by the user. *)
-Ltac do_depind' tac H :=
- (try intros until H) ; dep_elimify ; generalize_eqs H ; tac H ; simplify_dep_elim ; un_dep_elimify.
+Ltac do_depelim' tac H :=
+ (try intros until H) ; block_goal ; generalize_eqs H ; tac H ; simplify_dep_elim ;
+ simplify_IH_hyps ; unblock_goal.
(** Calls [destruct] on the generalized hypothesis, results should be similar to inversion.
By default, we don't try to generalize the hyp by its variable indices. *)
-Tactic Notation "dependent" "destruction" ident(H) :=
- do_depind' ltac:(fun hyp => do_case hyp) H.
+Tactic Notation "dependent" "destruction" ident(H) :=
+ do_depelim' ltac:(fun hyp => do_case hyp) H.
-Tactic Notation "dependent" "destruction" ident(H) "using" constr(c) :=
- do_depind' ltac:(fun hyp => destruct hyp using c) H.
+Tactic Notation "dependent" "destruction" ident(H) "using" constr(c) :=
+ do_depelim' ltac:(fun hyp => destruct hyp using c) H.
-(** This tactic also generalizes the goal by the given variables before the induction. *)
+(** This tactic also generalizes the goal by the given variables before the elimination. *)
-Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) :=
- do_depind' ltac:(fun hyp => revert l ; do_case hyp) H.
+Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) :=
+ do_depelim' ltac:(fun hyp => revert l ; do_case hyp) H.
-Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) :=
- do_depind' ltac:(fun hyp => revert l ; destruct hyp using c) H.
+Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) :=
+ do_depelim' ltac:(fun hyp => revert l ; destruct hyp using c) H.
-(** Then we have wrappers for usual calls to induction. One can customize the induction tactic by
- writting another wrapper calling do_depind. We suppose the hyp has to be generalized before
+(** Then we have wrappers for usual calls to induction. One can customize the induction tactic by
+ writting another wrapper calling do_depelim. We suppose the hyp has to be generalized before
calling [induction]. *)
Tactic Notation "dependent" "induction" ident(H) :=
@@ -558,13 +446,8 @@ Tactic Notation "dependent" "induction" ident(H) "using" constr(c) :=
(** This tactic also generalizes the goal by the given variables before the induction. *)
-Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) :=
- do_depind' ltac:(fun hyp => generalize l ; clear l ; do_ind hyp) H.
-
-Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) :=
- do_depind' ltac:(fun hyp => generalize l ; clear l ; induction hyp using c) H.
+Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) :=
+ do_depelim' ltac:(fun hyp => generalize l ; clear l ; do_ind hyp) H.
-Ltac simplify_IH_hyps := repeat
- match goal with
- | [ hyp : _ |- _ ] => specialize_hypothesis hyp
- end. \ No newline at end of file
+Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) :=
+ do_depelim' ltac:(fun hyp => generalize l ; clear l ; induction hyp using c) H.
diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v
index a6aa4d524..89f477d8f 100644
--- a/theories/Program/Subset.v
+++ b/theories/Program/Subset.v
@@ -82,7 +82,7 @@ Qed.
in tactics. *)
Definition match_eq (A B : Type) (x : A) (fn : forall (y : A | y = x), B) : B :=
- fn (exist _ x (refl_equal x)).
+ fn (exist _ x eq_refl).
(* This is what we want to be able to do: replace the originaly matched object by a new,
propositionally equal one. If [fn] works on [x] it should work on any [y | y = x]. *)
diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v
index aff2da946..2064977fe 100644
--- a/theories/Program/Syntax.v
+++ b/theories/Program/Syntax.v
@@ -46,6 +46,13 @@ Notation " [ ] " := nil : list_scope.
Notation " [ x ] " := (cons x nil) : list_scope.
Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope.
+(** Implicit arguments for vectors. *)
+
+Require Import Bvector.
+
+Implicit Arguments Vnil [[A]].
+Implicit Arguments Vcons [[A] [n]].
+
(** Treating n-ary exists *)
Notation " 'exists' x y , p" := (ex (fun x => (ex (fun y => p))))
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index 881297955..b3b08e067 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -43,7 +43,7 @@ Ltac do_nat n tac :=
(** Do something on the last hypothesis, or fail *)
Ltac on_last_hyp tac :=
- match goal with [ H : _ |- _ ] => tac H || fail 1 end.
+ match goal with [ H : _ |- _ ] => first [ tac H | fail 1 ] end.
(** Destructs one pair, without care regarding naming. *)
@@ -105,6 +105,15 @@ Ltac revert_last :=
Ltac reverse := repeat revert_last.
+(** Reverse everything up to hypothesis id (not included). *)
+
+Ltac revert_until id :=
+ on_last_hyp ltac:(fun id' =>
+ match id' with
+ | id => idtac
+ | _ => revert id' ; revert_until id
+ end).
+
(** Clear duplicated hypotheses *)
Ltac clear_dup :=
@@ -121,6 +130,16 @@ Ltac clear_dup :=
Ltac clear_dups := repeat clear_dup.
+(** Try to clear everything except some hyp *)
+
+Ltac clear_except hyp :=
+ repeat match goal with [ H : _ |- _ ] =>
+ match H with
+ | hyp => fail 1
+ | _ => clear H
+ end
+ end.
+
(** A non-failing subst that substitutes as much as possible. *)
Ltac subst_no_fail :=
diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v
index bce32af48..c999b58ee 100644
--- a/theories/Wellfounded/Transitive_Closure.v
+++ b/theories/Wellfounded/Transitive_Closure.v
@@ -29,7 +29,7 @@ Section Wf_Transitive_Closure.
intros y H2.
induction H2; auto with sets.
apply Acc_inv with y; auto with sets.
- Qed.
+ Defined.
Hint Resolve Acc_clos_trans.
@@ -42,6 +42,6 @@ Section Wf_Transitive_Closure.
Theorem wf_clos_trans : well_founded R -> well_founded trans_clos.
Proof.
unfold well_founded in |- *; auto with sets.
- Qed.
+ Defined.
End Wf_Transitive_Closure.
diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty
index ba1173bee..b50b755f6 100644
--- a/tools/coqdoc/coqdoc.sty
+++ b/tools/coqdoc/coqdoc.sty
@@ -110,7 +110,7 @@
\newcommand{\coqref}[2]{#2}
\newcommand{\texorpdfstring}[2]{#1}
\newcommand{\identref}[2]{\textsf{#2}}
- \newcommand{\coqlibrary}[2]{\cleardoublepage\chapter{#1\coqdoccst{#2}}}
+ \newcommand{\coqlibrary}[3]{\cleardoublepage\chapter{#2\coqdoccst{#3}}}
\fi
\usepackage{xr}
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index d92b34e25..2820b9a88 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -256,6 +256,9 @@ let firstchar =
'\194' '\185' |
(* utf-8 latin 1 supplement *)
'\195' ['\128'-'\191'] |
+ (* utf-8 letterlike symbols *)
+ (* '\206' ([ '\145' - '\183'] | '\187') | *)
+ (* '\xCF' [ '\x00' - '\xCE' ] | *)
(* utf-8 letterlike symbols *)
'\206' ('\160' | [ '\177'-'\183'] | '\187') |
'\226' ('\130' [ '\128'-'\137' ] (* subscripts *)
diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
index cc174ebac..f4ea23215 100644
--- a/toplevel/autoinstance.ml
+++ b/toplevel/autoinstance.ml
@@ -200,7 +200,7 @@ let declare_class_instance gr ctx params =
try
let cst = Declare.declare_constant ident
(ce,Decl_kinds.IsDefinition Decl_kinds.Instance) in
- Typeclasses.add_instance (Typeclasses.new_instance cl (Some 100) true cst);
+ Typeclasses.add_instance (Typeclasses.new_instance cl (Some 100) true (ConstRef cst));
new_instance_message ident typ def
with e -> msgnl (str"Error defining instance := "++pr_constr def++str" : "++pr_constr typ++str" "++Cerrors.explain_exn e)
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index c5b54df33..7fdd6bd7e 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -34,26 +34,36 @@ open Entries
let typeclasses_db = "typeclass_instances"
+let set_typeclass_transparency c b =
+ Auto.add_hints false [typeclasses_db]
+ (Auto.HintsTransparencyEntry ([c], b))
+
let _ =
Typeclasses.register_add_instance_hint
(fun inst pri ->
Flags.silently (fun () ->
Auto.add_hints false [typeclasses_db]
(Auto.HintsResolveEntry
- [pri, false, mkConst inst])) ())
-
-let declare_instance_cst glob con =
- let instance = Typeops.type_of_constant (Global.env ()) con in
+ [pri, false, constr_of_global inst])) ());
+ Typeclasses.register_set_typeclass_transparency set_typeclass_transparency
+
+let declare_class glob idl =
+ match global (Ident idl) with
+ | ConstRef x -> Typeclasses.add_constant_class x
+ | IndRef x -> Typeclasses.add_inductive_class x
+ | _ -> user_err_loc (fst idl, "declare_class",
+ Pp.str"Unsupported class type, only constants and inductives are allowed")
+
+let declare_instance_cst glob c =
+ let instance = Typing.type_of (Global.env ()) Evd.empty (constr_of_global c) in
let _, r = decompose_prod_assum instance in
match class_of_constr r with
- | Some tc -> add_instance (new_instance tc None glob con)
+ | Some tc -> add_instance (new_instance tc None glob c)
| None -> errorlabstrm "" (Pp.strbrk "Constant does not build instances of a declared type class.")
let declare_instance glob idl =
- let con =
- try (match global (Ident idl) with
- | ConstRef x -> x
- | _ -> raise Not_found)
+ let con =
+ try global (Ident idl)
with _ -> error "Instance definition not found."
in declare_instance_cst glob con
@@ -104,7 +114,7 @@ let ($$) g f = fun x -> g (f x)
let instance_hook k pri global imps ?hook cst =
let inst = Typeclasses.new_instance k pri global cst in
- Impargs.maybe_declare_manual_implicits false (ConstRef cst) ~enriching:false imps;
+ Impargs.maybe_declare_manual_implicits false cst ~enriching:false imps;
Typeclasses.add_instance inst;
(match hook with Some h -> h cst | None -> ())
@@ -120,11 +130,11 @@ let declare_instance_constant k pri global imps ?hook id term termtype =
in
let kn = Declare.declare_constant id cdecl in
Flags.if_verbose Command.definition_message id;
- instance_hook k pri global imps ?hook kn;
+ instance_hook k pri global imps ?hook (ConstRef kn);
id
let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
- ?(tac:Proof_type.tactic option) ?(hook:(Names.constant -> unit) option) pri =
+ ?(tac:Proof_type.tactic option) ?(hook:(global_reference -> unit) option) pri =
let env = Global.env() in
let evars = ref Evd.empty in
let tclass, ids =
@@ -177,7 +187,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
Evarutil.check_evars env Evd.empty !evars termtype;
let cst = Declare.declare_internal_constant id
(Entries.ParameterEntry (termtype,false), Decl_kinds.IsAssumption Decl_kinds.Logical)
- in instance_hook k None false imps ?hook cst; id
+ in instance_hook k None false imps ?hook (ConstRef cst); id
end
else
begin
@@ -238,10 +248,10 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
evars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env !evars;
let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
Flags.silently (fun () ->
- Command.start_proof id kind termtype
- (fun _ -> function ConstRef cst -> instance_hook k pri global imps ?hook cst
- | _ -> assert false);
- if props <> [] then Pfedit.by (!refine_ref (evm, term))
+ Command.start_proof id kind termtype (fun _ -> instance_hook k pri global imps ?hook);
+ if props <> [] then
+ Pfedit.by (* (Refiner.tclTHEN (Refiner.tclEVARS ( !isevars)) *)
+ (!refine_ref (evm, term))
else if Flags.is_auto_intros () then
Pfedit.by (Refiner.tclDO len Tactics.intro);
(match tac with Some tac -> Pfedit.by tac | None -> ())) ();
@@ -249,7 +259,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
id
end
end
-
+
let named_of_rel_context l =
let acc, ctx =
List.fold_right
@@ -285,7 +295,7 @@ let context ?(hook=fun _ -> ()) l =
in
match class_of_constr t with
| Some tc ->
- add_instance (Typeclasses.new_instance tc None false cst);
+ add_instance (Typeclasses.new_instance tc None false (ConstRef cst));
hook (ConstRef cst)
| None -> ()
else (
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 7a8e9a923..5953c14f9 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -29,6 +29,10 @@ val mismatched_params : env -> constr_expr list -> rel_context -> 'a
val mismatched_props : env -> constr_expr list -> rel_context -> 'a
+(* Post-hoc class declaration. *)
+
+val declare_class : bool -> identifier located -> unit
+
(* Instance declaration *)
val declare_instance : bool -> identifier located -> unit
@@ -38,7 +42,7 @@ val declare_instance_constant :
int option -> (* priority *)
bool -> (* globality *)
Impargs.manual_explicitation list -> (* implicits *)
- ?hook:(Names.constant -> unit) ->
+ ?hook:(Libnames.global_reference -> unit) ->
identifier -> (* name *)
Term.constr -> (* body *)
Term.types -> (* type *)
@@ -51,10 +55,14 @@ val new_instance :
constr_expr ->
?generalize:bool ->
?tac:Proof_type.tactic ->
- ?hook:(constant -> unit) ->
+ ?hook:(Libnames.global_reference -> unit) ->
int option ->
identifier
+(* Setting opacity *)
+
+val set_typeclass_transparency : evaluable_global_reference -> bool -> unit
+
(* For generation on names based on classes only *)
val id_of_class : typeclass -> identifier
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 152ae5b70..e11a3b373 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -287,20 +287,14 @@ let implicits_of_context ctx =
in ExplByPos (i, explname), (true, true, true))
1 (List.rev (Anonymous :: (List.map pi1 ctx)))
-let typeclasses_db = "typeclass_instances"
-
-let qualid_of_con c =
+let qualid_of_con c =
Qualid (dummy_loc, shortest_qualid_of_global Idset.empty (ConstRef c))
-let set_rigid c =
- Auto.add_hints false [typeclasses_db]
- (Auto.HintsTransparencyEntry ([EvalConstRef c], false))
-
let declare_instance_cst glob con =
let instance = Typeops.type_of_constant (Global.env ()) con in
let _, r = decompose_prod_assum instance in
match class_of_constr r with
- | Some tc -> add_instance (new_instance tc None glob con)
+ | Some tc -> add_instance (new_instance tc None glob (ConstRef con))
| None -> errorlabstrm "" (Pp.strbrk "Constant does not build instances of a declared type class.")
let declare_class finite def infer id idbuild paramimpls params arity fieldimpls fields
@@ -340,7 +334,7 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
let cref = ConstRef cst in
Impargs.declare_manual_implicits false cref paramimpls;
Impargs.declare_manual_implicits false (ConstRef proj_cst) (List.hd fieldimpls);
- set_rigid cst; (* set_rigid proj_cst; *)
+ Classes.set_typeclass_transparency (EvalConstRef cst) false;
if infer then Evd.fold (fun ev evi _ -> Recordops.declare_method (ConstRef cst) ev sign) sign ();
cref, [proj_name, Some proj_cst]
| _ ->
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index 13b27d5ab..1d20106a5 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -8,9 +8,9 @@ Libtypes
Search
Autoinstance
Command
+Classes
Record
Ppvernac
-Classes
Vernacinterp
Mltop
Vernacentries
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 70feb6ceb..d2a9153fe 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -620,6 +620,10 @@ let vernac_declare_instance id =
Dumpglob.dump_definition id false "inst";
Classes.declare_instance false id
+let vernac_declare_class id =
+ Dumpglob.dump_definition id false "class";
+ Classes.declare_class false id
+
(***********)
(* Solving *)
let vernac_solve n tcom b =
@@ -1338,6 +1342,7 @@ let interp c = match c with
| VernacInstance (glob, sup, inst, props, pri) -> vernac_instance glob sup inst props pri
| VernacContext sup -> vernac_context sup
| VernacDeclareInstance id -> vernac_declare_instance id
+ | VernacDeclareClass id -> vernac_declare_class id
(* Solving *)
| VernacSolve (n,tac,b) -> vernac_solve n tac b
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 2e73767c5..9bcdd402d 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -251,6 +251,9 @@ type vernac_expr =
| VernacDeclareInstance of
lident (* instance name *)
+ | VernacDeclareClass of
+ lident (* inductive or definition name *)
+
(* Modules and Module Types *)
| VernacDeclareModule of bool option * lident *
module_binder list * (module_type_ast * bool)