diff options
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) |