diff options
author | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
commit | cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch) | |
tree | b7832bd5d412a5a5d69cb36ae2ded62c71124c22 /contrib/subtac | |
parent | 113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff) |
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'contrib/subtac')
-rw-r--r-- | contrib/subtac/equations.ml4 | 1149 | ||||
-rw-r--r-- | contrib/subtac/eterm.ml | 121 | ||||
-rw-r--r-- | contrib/subtac/eterm.mli | 22 | ||||
-rw-r--r-- | contrib/subtac/g_subtac.ml4 | 16 | ||||
-rw-r--r-- | contrib/subtac/subtac.ml | 38 | ||||
-rw-r--r-- | contrib/subtac/subtac_cases.ml | 4 | ||||
-rw-r--r-- | contrib/subtac/subtac_classes.ml | 159 | ||||
-rw-r--r-- | contrib/subtac/subtac_classes.mli | 10 | ||||
-rw-r--r-- | contrib/subtac/subtac_coercion.ml | 59 | ||||
-rw-r--r-- | contrib/subtac/subtac_coercion.mli | 3 | ||||
-rw-r--r-- | contrib/subtac/subtac_command.ml | 6 | ||||
-rw-r--r-- | contrib/subtac/subtac_obligations.ml | 246 | ||||
-rw-r--r-- | contrib/subtac/subtac_obligations.mli | 19 | ||||
-rw-r--r-- | contrib/subtac/subtac_pretyping.ml | 4 | ||||
-rw-r--r-- | contrib/subtac/subtac_pretyping_F.ml | 23 | ||||
-rw-r--r-- | contrib/subtac/subtac_utils.ml | 7 | ||||
-rw-r--r-- | contrib/subtac/subtac_utils.mli | 3 |
17 files changed, 1552 insertions, 337 deletions
diff --git a/contrib/subtac/equations.ml4 b/contrib/subtac/equations.ml4 new file mode 100644 index 00000000..9d120019 --- /dev/null +++ b/contrib/subtac/equations.ml4 @@ -0,0 +1,1149 @@ +(* -*- 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: subtac_cases.ml 11198 2008-07-01 17:03:43Z msozeau $ *) + +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.extended_locate qid with + | TrueGlobal ref -> true + | SyntacticDef kn -> true + +let is_global id = + try + locate_reference (make_short_qualid 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 (Evd.evars_of !isevar) varsctx, + nf_env_evar (Evd.evars_of !isevar) env', + rev_map (nf_evar (Evd.evars_of !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 (Evd.evars_of !isevar) sign in + let arity = nf_evar (Evd.evars_of !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 (Evd.evars_of !isevar) sign in + let arity = nf_evar (Evd.evars_of !isevar) arity in + let prob = (i, sign, arity) in + let fixenv = nf_env_evar (Evd.evars_of !isevar) fixenv in + let fixdecls = nf_rel_context_evar (Evd.evars_of !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 (Evd.evars_of 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/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml index 9bfb33ea..00a69bba 100644 --- a/contrib/subtac/eterm.ml +++ b/contrib/subtac/eterm.ml @@ -1,3 +1,4 @@ +(* -*- compile-command: "make -C ../.. bin/coqtop.byte" -*- *) (** - Get types of existentials ; - Flatten dependency tree (prefix order) ; @@ -6,12 +7,14 @@ *) open Term +open Sign open Names open Evd open List open Pp open Util open Subtac_utils +open Proof_type let trace s = if !Flags.debug then (msgnl s; msgerr s) @@ -20,15 +23,27 @@ let trace s = let succfix (depth, fixrels) = (succ depth, List.map succ fixrels) +type oblinfo = + { ev_name: int * identifier; + ev_hyps: named_context; + ev_status: obligation_definition_status; + ev_chop: int option; + ev_loc: Util.loc; + ev_typ: types; + ev_tac: Tacexpr.raw_tactic_expr 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 seen = ref Intset.empty in let transparent = ref Idset.empty in let evar_info id = List.assoc id evs in let rec substrec (depth, fixrels) c = match kind_of_term c with | Evar (k, args) -> - let (id, idstr), hyps, chop, _, _, _ = + let { ev_name = (id, idstr) ; + ev_hyps = hyps ; ev_chop = chop } = try evar_info k with Not_found -> anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found") @@ -46,17 +61,13 @@ let subst_evar_constr evs n t = let rec aux hyps args acc = match hyps, args with ((_, None, _) :: tlh), (c :: tla) -> - aux tlh tla ((map_constr_with_binders succfix substrec (depth, fixrels) c) :: acc) + aux tlh tla ((substrec (depth, fixrels) c) :: acc) | ((_, Some _, _) :: tlh), (_ :: tla) -> aux tlh tla acc | [], [] -> acc | _, _ -> acc (*failwith "subst_evars: invalid argument"*) in aux hyps args [] in - (try trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (List.length args) ++ str "arguments," ++ - int (List.length hyps) ++ str " hypotheses" ++ spc () ++ - pp_list (fun x -> my_print_constr (Global.env ()) x) args); - with _ -> ()); 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) @@ -93,8 +104,8 @@ let etype_of_evar evs hyps concl = let trans' = Idset.union trans trans' in (match copt with Some c -> - if noccurn 1 rest then lift (-1) rest, s', trans' - else +(* if noccurn 1 rest then lift (-1) rest, s', trans' *) +(* else *) let c', s'', trans'' = subst_evar_constr evs n c in let c' = subst_vars acc 0 c' in mkNamedProd_or_LetIn (id, Some c', t'') rest, @@ -121,15 +132,34 @@ let rec chop_product n t = | Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None | _ -> None -let eterm_obligations env name isevars evm fs t ty = - (* 'Serialize' the evars, we assume that the types of the existentials - refer to previous existentials in the list only *) - trace (str " In eterm: isevars: " ++ my_print_evardefs isevars); - trace (str "Term given to eterm" ++ spc () ++ - Termops.print_constr_env (Global.env ()) t); +let evar_dependencies evm ev = + let one_step deps = + Intset.fold (fun ev s -> + let evi = Evd.find evm ev in + Intset.union (Evarutil.evars_of_evar_info evi) s) + deps deps + in + let rec aux deps = + let deps' = one_step deps in + if Intset.equal deps deps' then deps + else aux deps' + 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 = + (* 'Serialize' the evars *) let nc = Environ.named_context env in let nc_len = Sign.named_context_length nc in let evl = List.rev (to_list evm) in + let evl = List.map (fun (id, ev) -> (id, ev, evar_dependencies evm id)) evl in + let sevl = sort_dependencies evl in + let evl = List.map (fun (id, ev, _) -> id, ev) sevl in let evn = let i = ref (-1) in List.rev_map (fun (id, ev) -> incr i; @@ -146,20 +176,29 @@ let eterm_obligations env name isevars evm fs t ty = let evtyp, deps, transp = etype_of_evar l hyps ev.evar_concl in let evtyp, hyps, chop = match chop_product fs evtyp with - Some t -> - (try - trace (str "Choped a product: " ++ spc () ++ - Termops.print_constr_env (Global.env ()) evtyp ++ str " to " ++ spc () ++ - Termops.print_constr_env (Global.env ()) t); - with _ -> ()); - t, trunc_named_context fs hyps, fs - | None -> evtyp, hyps, 0 + | Some t -> t, trunc_named_context fs hyps, fs + | None -> evtyp, hyps, 0 in let loc, k = evar_source id isevars in - let opacity = match k with QuestionMark o -> o | _ -> true in - let opaque = if not opacity || chop <> fs then None else Some chop in - let y' = (id, ((n, nstr), hyps, opaque, loc, evtyp, deps)) in - y' :: l) + let status = match k with QuestionMark o -> Some o | _ -> status in + let status, chop = match status with + | Some (Define true as stat) -> + if chop <> fs then Define false, None + else stat, Some chop + | Some s -> s, None + | None -> Define true, None + in + let tac = match ev.evar_extra with + | Some t -> + if Dyn.tag t = "tactic" then + Some (Tacinterp.globTacticIn (Tacinterp.tactic_out t)) + else None + | None -> None + in + let info = { ev_name = (n, nstr); + ev_hyps = hyps; ev_status = status; ev_chop = chop; + ev_loc = loc; ev_typ = evtyp ; ev_deps = deps; ev_tac = tac } + in (id, info) :: l) evn [] in let t', _, transparent = (* Substitute evar refs in the term by variables *) @@ -167,28 +206,16 @@ let eterm_obligations env name isevars evm fs t ty = in let ty, _, _ = subst_evar_constr evts 0 ty in let evars = - List.map (fun (_, ((_, name), _, opaque, loc, typ, deps)) -> - name, typ, loc, not (opaque = None) && not (Idset.mem name transparent), deps) evts - in - (try - trace (str "Term constructed in eterm" ++ spc () ++ - Termops.print_constr_env (Global.env ()) t'); - ignore(iter - (fun (name, typ, _, _, deps) -> - trace (str "Evar :" ++ spc () ++ str (string_of_id name) ++ - Termops.print_constr_env (Global.env ()) typ)) - evars); - with _ -> ()); - Array.of_list (List.rev evars), t', ty + List.map (fun (_, info) -> + let { ev_name = (_, name); ev_status = status; + ev_loc = loc; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info + in + let status = match status with + | 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 let mkMetas n = list_tabulate (fun _ -> Evarutil.mk_new_meta ()) n -(* let eterm evm t (tycon : types option) = *) -(* let t, tycon, evs = eterm_term evm t tycon in *) -(* match tycon with *) -(* Some typ -> Tactics.apply_term (mkCast (t, DEFAULTcast, typ)) [] *) -(* | None -> Tactics.apply_term t (mkMetas (List.length evs)) *) - -(* open Tacmach *) - let etermtac (evm, t) = assert(false) (*eterm evm t None *) diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli index 007e327c..19e8ffe8 100644 --- a/contrib/subtac/eterm.mli +++ b/contrib/subtac/eterm.mli @@ -6,23 +6,27 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: eterm.mli 10889 2008-05-06 14:05:20Z msozeau $ i*) +(*i $Id: eterm.mli 11576 2008-11-10 19:13:15Z msozeau $ i*) open Environ open Tacmach open Term open Evd open Names open Util +open Tacinterp val mkMetas : int -> constr list -(* val eterm_term : evar_map -> constr -> types option -> constr * types option * (identifier * types) list *) - -(* 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 -> constr -> types -> - (identifier * types * loc * bool * Intset.t) array * constr * types - (* Obl. name, type as product, location of the original evar, - opacity (true = opaque) and dependencies as indexes into the array *) +val evar_dependencies : evar_map -> int -> Intset.t +val sort_dependencies : (int * evar_info * Intset.t) list -> (int * evar_info * Intset.t) list + +(* 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, + status and dependencies as indexes into the array *) val etermtac : open_constr -> tactic diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4 index 4cf5336d..7194d435 100644 --- a/contrib/subtac/g_subtac.ml4 +++ b/contrib/subtac/g_subtac.ml4 @@ -14,7 +14,7 @@ Syntax for the subtac terms and types. Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliâtre *) -(* $Id: g_subtac.ml4 11282 2008-07-28 11:51:53Z msozeau $ *) +(* $Id: g_subtac.ml4 11576 2008-11-10 19:13:15Z msozeau $ *) open Flags @@ -112,25 +112,25 @@ END VERNAC COMMAND EXTEND Subtac_Solve_Obligation | [ "Solve" "Obligation" integer(num) "of" ident(name) "using" tactic(t) ] -> - [ Subtac_obligations.try_solve_obligation num (Some name) (Tacinterp.interp t) ] + [ Subtac_obligations.try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) ] | [ "Solve" "Obligation" integer(num) "using" tactic(t) ] -> - [ Subtac_obligations.try_solve_obligation num None (Tacinterp.interp t) ] + [ Subtac_obligations.try_solve_obligation num None (Some (Tacinterp.interp t)) ] END VERNAC COMMAND EXTEND Subtac_Solve_Obligations | [ "Solve" "Obligations" "of" ident(name) "using" tactic(t) ] -> - [ Subtac_obligations.try_solve_obligations (Some name) (Tacinterp.interp t) ] + [ Subtac_obligations.try_solve_obligations (Some name) (Some (Tacinterp.interp t)) ] | [ "Solve" "Obligations" "using" tactic(t) ] -> - [ Subtac_obligations.try_solve_obligations None (Tacinterp.interp t) ] + [ Subtac_obligations.try_solve_obligations None (Some (Tacinterp.interp t)) ] | [ "Solve" "Obligations" ] -> - [ Subtac_obligations.try_solve_obligations None (Subtac_obligations.default_tactic ()) ] + [ Subtac_obligations.try_solve_obligations None None ] END VERNAC COMMAND EXTEND Subtac_Solve_All_Obligations | [ "Solve" "All" "Obligations" "using" tactic(t) ] -> - [ Subtac_obligations.solve_all_obligations (Tacinterp.interp t) ] + [ Subtac_obligations.solve_all_obligations (Some (Tacinterp.interp t)) ] | [ "Solve" "All" "Obligations" ] -> - [ Subtac_obligations.solve_all_obligations (Subtac_obligations.default_tactic ()) ] + [ Subtac_obligations.solve_all_obligations None ] END VERNAC COMMAND EXTEND Subtac_Admit_Obligations diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml index 7bfa107b..ba00fce5 100644 --- a/contrib/subtac/subtac.ml +++ b/contrib/subtac/subtac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: subtac.ml 11800 2009-01-18 18:34:15Z msozeau $ *) open Global open Pp @@ -52,16 +52,14 @@ 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 c typ in - (** Make all obligations transparent so that real dependencies can be sorted out by the user *) - let obls = Array.map (fun (id, t, l, op, d) -> (id, t, l, false, d)) obls 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()) - (match cst with ConstRef kn -> kn | _ -> assert false) - | _ -> - errorlabstrm "start_proof" - (str "The statement obligations could not be resolved automatically, " ++ spc () ++ - str "write a statement definition first.") + Subtac_obligations.Defined cst -> constant_value (Global.env()) + (match cst with ConstRef kn -> kn | _ -> assert false) + | _ -> + errorlabstrm "start_proof" + (str "The statement obligations could not be resolved automatically, " ++ spc () ++ + str "write a statement definition first.") else let _ = Typeops.infer_type env c in c @@ -106,12 +104,9 @@ let declare_assumption env isevars idl is_coe k bl c nl = errorlabstrm "Command.Assumption" (str "Cannot declare an assumption while in proof editing mode.") -let dump_definition (loc, id) s = - Flags.dump_string (Printf.sprintf "%s %d %s\n" s (fst (unloc loc)) (string_of_id id)) - let dump_constraint ty ((loc, n), _, _) = match n with - | Name id -> dump_definition (loc, id) ty + | Name id -> Dumpglob.dump_definition (loc, id) false ty | Anonymous -> () let dump_variable lid = () @@ -119,9 +114,9 @@ let dump_variable lid = () let vernac_assumption env isevars kind l nl = let global = fst kind = Global in List.iter (fun (is_coe,(idl,c)) -> - if !Flags.dump then + if Dumpglob.dump () then List.iter (fun lid -> - if global then dump_definition lid "ax" + if global then Dumpglob.dump_definition lid (not global) "ax" else dump_variable lid) idl; declare_assumption env isevars idl is_coe kind [] c nl) l @@ -139,7 +134,7 @@ let subtac (loc, command) = match command with | VernacDefinition (defkind, (_, id as lid), expr, hook) -> check_fresh lid; - dump_definition lid "def"; + Dumpglob.dump_definition lid false "def"; (match expr with | ProveBody (bl, t) -> if Lib.is_modtype () then @@ -152,12 +147,12 @@ let subtac (loc, command) = | VernacFixpoint (l, b) -> List.iter (fun ((lid, _, _, _, _), _) -> check_fresh lid; - dump_definition lid "fix") l; + Dumpglob.dump_definition lid false "fix") l; let _ = trace (str "Building fixpoint") in ignore(Subtac_command.build_recursive l b) | VernacStartTheoremProof (thkind, [Some id, (bl, t)], lettop, hook) -> - if !Flags.dump then dump_definition id "prf"; + Dumpglob.dump_definition id false "prf"; if not(Pfedit.refining ()) then if lettop then errorlabstrm "Subtac_command.StartProof" @@ -172,11 +167,12 @@ let subtac (loc, command) = vernac_assumption env isevars stre l nl | VernacInstance (glob, sup, is, props, pri) -> - if !Flags.dump then dump_constraint "inst" is; + dump_constraint "inst" is; ignore(Subtac_classes.new_instance ~global:glob sup is props pri) | VernacCoFixpoint (l, b) -> - List.iter (fun ((lid, _, _, _), _) -> dump_definition lid "cofix") l; + if Dumpglob.dump () then + List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "cofix") l; ignore(Subtac_command.build_corecursive l b) (*| VernacEndProof e -> diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml index 04bf54d3..094226ff 100644 --- a/contrib/subtac/subtac_cases.ml +++ b/contrib/subtac/subtac_cases.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac_cases.ml 11282 2008-07-28 11:51:53Z msozeau $ *) +(* $Id: subtac_cases.ml 11576 2008-11-10 19:13:15Z msozeau $ *) open Cases open Util @@ -1572,7 +1572,7 @@ let mk_JMeq typ x typ' y = mkApp (Lazy.force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |]) let mk_JMeq_refl typ x = mkApp (Lazy.force Subtac_utils.jmeq_refl, [| typ; x |]) -let hole = RHole (dummy_loc, Evd.QuestionMark true) +let hole = RHole (dummy_loc, Evd.QuestionMark (Evd.Define true)) let context_of_arsign l = let (x, _) = List.fold_right diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml index 9a5539e2..0d44a0c0 100644 --- a/contrib/subtac/subtac_classes.ml +++ b/contrib/subtac/subtac_classes.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: subtac_classes.ml 11282 2008-07-28 11:51:53Z msozeau $ i*) +(*i $Id: subtac_classes.ml 11800 2009-01-18 18:34:15Z msozeau $ i*) open Pretyping open Evd @@ -92,104 +92,103 @@ let type_class_instance_params isevars env id n ctx inst subst = let substitution_of_constrs ctx cstrs = List.fold_right2 (fun c (na, _, _) acc -> (na, c) :: acc) cstrs ctx [] -let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Classes.default_on_free_vars) pri = +let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) pri = let env = Global.env() in let isevars = ref (Evd.create_evar_defs Evd.empty) in - let bound = Implicit_quantifiers.ids_of_list (Termops.ids_of_context env) in - let bound, fvs = Implicit_quantifiers.free_vars_of_binders ~bound [] ctx in let tclass = match bk with - | Implicit -> - let loc, id, par = Implicit_quantifiers.destClassAppExpl cl in - let k = class_info (Nametab.global id) in - let applen = List.fold_left (fun acc (x, y) -> if y = None then succ acc else acc) 0 par in - let needlen = List.fold_left (fun acc (x, y) -> if x = None then succ acc else acc) 0 k.cl_context in - if needlen <> applen then - Classes.mismatched_params env (List.map fst par) (List.map snd k.cl_context); - let pars, _ = Implicit_quantifiers.combine_params Idset.empty (* need no avoid *) - (fun avoid (clname, (id, _, t)) -> - match clname with - Some (cl, b) -> - let t = - if b then - let _k = class_info cl in - CHole (Util.dummy_loc, Some Evd.InternalHole) (* (Evd.ImplicitArg (IndRef k.cl_impl, (1, None)))) *) - else CHole (Util.dummy_loc, None) - in t, avoid - | None -> failwith ("new instance: under-applied typeclass")) - par (List.rev k.cl_context) - in Topconstr.CAppExpl (loc, (None, id), pars) - + | Implicit -> + Implicit_quantifiers.implicit_application Idset.empty (* need no avoid *) + ~allow_partial:false (fun avoid (clname, (id, _, t)) -> + match clname with + | Some (cl, b) -> + let t = + if b then + let _k = class_info cl in + CHole (Util.dummy_loc, Some Evd.InternalHole) + else CHole (Util.dummy_loc, None) + in t, avoid + | None -> failwith ("new instance: under-applied typeclass")) + cl | Explicit -> cl in - let ctx_bound = Idset.union bound (Implicit_quantifiers.ids_of_list fvs) in - let gen_ids = Implicit_quantifiers.free_vars_of_constr_expr ~bound:ctx_bound tclass [] in - let bound = Idset.union (Implicit_quantifiers.ids_of_list gen_ids) ctx_bound in - on_free_vars (List.rev (gen_ids @ fvs)); - let gen_ctx = Implicit_quantifiers.binder_list_of_ids gen_ids in - let ctx, avoid = Classes.name_typeclass_binders bound ctx in - let ctx = List.append ctx (List.rev gen_ctx) in + let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in let k, ctx', imps, subst = let c = Command.generalize_constr_expr tclass ctx in let c', imps = interp_type_evars_impls ~evdref:isevars env c in let ctx, c = Sign.decompose_prod_assum c' in - let cl, args = Typeclasses.dest_class_app c in - cl, ctx, imps, (List.rev (Array.to_list args)) + let cl, args = Typeclasses.dest_class_app (push_rel_context ctx env) c in + cl, ctx, imps, (List.rev args) in let id = match snd instid with - Name id -> - let sp = Lib.make_path id in - if Nametab.exists_cci sp then - errorlabstrm "new_instance" (Nameops.pr_id id ++ Pp.str " already exists"); - id - | Anonymous -> - let i = Nameops.add_suffix (Classes.id_of_class k) "_instance_0" in - Termops.next_global_ident_away false i (Termops.ids_of_context env) + | Name id -> + let sp = Lib.make_path id in + if Nametab.exists_cci sp then + errorlabstrm "new_instance" (Nameops.pr_id id ++ Pp.str " already exists"); + id + | Anonymous -> + let i = Nameops.add_suffix (Classes.id_of_class k) "_instance_0" in + Termops.next_global_ident_away false i (Termops.ids_of_context env) in let env' = push_rel_context ctx' env in isevars := Evarutil.nf_evar_defs !isevars; isevars := resolve_typeclasses ~onlyargs:false ~fail:true env' !isevars; let sigma = Evd.evars_of !isevars in - let substctx = List.map (Evarutil.nf_evar sigma) subst in - let subst, _propsctx = + let subst = List.map (Evarutil.nf_evar sigma) subst in + let subst = let props = - List.map (fun (x, l, d) -> - x, Topconstr.abstract_constr_expr d (Classes.binders_of_lidents l)) - props + match props with + | CRecord (loc, _, fs) -> + if List.length fs > List.length k.cl_props then + Classes.mismatched_props env' (List.map snd fs) k.cl_props; + fs + | _ -> + if List.length k.cl_props <> 1 then + errorlabstrm "new_instance" (Pp.str "Expected a definition for the instance body") + else [(dummy_loc, Nameops.out_name (pi1 (List.hd k.cl_props))), props] in - if List.length props > List.length k.cl_props then - Classes.mismatched_props env' (List.map snd props) k.cl_props; - let props, rest = - List.fold_left - (fun (props, rest) (id,_,_) -> - try - let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in - let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in - Constrintern.add_glob loc (ConstRef (List.assoc mid k.cl_projs)); - c :: props, rest' - with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest) - ([], props) k.cl_props - in - if rest <> [] then - unbound_method env' k.cl_impl (fst (List.hd rest)) - else - type_ctx_instance isevars env' k.cl_props props substctx + match k.cl_props with + | [(na,b,ty)] -> + let term = match props with [] -> CHole (Util.dummy_loc, None) | [(_,f)] -> f | _ -> assert false in + let ty' = substl subst ty in + let c = interp_casted_constr_evars isevars env' term ty' in + c :: subst + | _ -> + let props, rest = + List.fold_left + (fun (props, rest) (id,_,_) -> + try + let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in + let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in + Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) (List.assoc mid k.cl_projs); + c :: props, rest' + with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest) + ([], props) k.cl_props + in + if rest <> [] then + unbound_method env' k.cl_impl (fst (List.hd rest)) + else + fst (type_ctx_instance isevars env' k.cl_props props subst) + in + let subst = List.fold_left2 + (fun subst' s (_, b, _) -> if b = None then s :: subst' else subst') + [] subst (k.cl_props @ snd k.cl_context) in - let inst_constr, ty_constr = instance_constructor k (List.rev subst) in - isevars := Evarutil.nf_evar_defs !isevars; - let term = Evarutil.nf_isevar !isevars (it_mkLambda_or_LetIn inst_constr ctx') - and termtype = Evarutil.nf_isevar !isevars (it_mkProd_or_LetIn ty_constr ctx') + let inst_constr, ty_constr = instance_constructor k subst in + isevars := Evarutil.nf_evar_defs !isevars; + let term = Evarutil.nf_isevar !isevars (it_mkLambda_or_LetIn inst_constr ctx') + and termtype = Evarutil.nf_isevar !isevars (it_mkProd_or_LetIn ty_constr ctx') + in + isevars := undefined_evars !isevars; + Evarutil.check_evars env Evd.empty !isevars termtype; + let hook gr = + let cst = match gr with ConstRef kn -> kn | _ -> assert false in + let inst = Typeclasses.new_instance k pri global cst in + Impargs.declare_manual_implicits false gr ~enriching:false imps; + Typeclasses.add_instance inst in - isevars := undefined_evars !isevars; - Evarutil.check_evars env Evd.empty !isevars termtype; - let hook gr = - let cst = match gr with ConstRef kn -> kn | _ -> assert false in - let inst = Typeclasses.new_instance k pri global cst in - Impargs.declare_manual_implicits false gr false imps; - Typeclasses.add_instance inst - in - let evm = Subtac_utils.evars_of_term (Evd.evars_of !isevars) Evd.empty term in - let obls, constr, typ = Eterm.eterm_obligations env id !isevars evm 0 term termtype in - ignore(Subtac_obligations.add_definition id constr typ ~kind:(Global,false,Instance) ~hook obls); - id + let evm = Subtac_utils.evars_of_term (Evd.evars_of !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 + diff --git a/contrib/subtac/subtac_classes.mli b/contrib/subtac/subtac_classes.mli index afb0d38d..96a51027 100644 --- a/contrib/subtac/subtac_classes.mli +++ b/contrib/subtac/subtac_classes.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: subtac_classes.mli 11282 2008-07-28 11:51:53Z msozeau $ i*) +(*i $Id: subtac_classes.mli 11709 2008-12-20 11:42:15Z msozeau $ i*) (*i*) open Names @@ -34,9 +34,9 @@ val type_ctx_instance : Evd.evar_defs ref -> val new_instance : ?global:bool -> - Topconstr.local_binder list -> + local_binder list -> typeclass_constraint -> - binder_def_list -> - ?on_free_vars:(identifier list -> unit) -> + constr_expr -> + ?generalize:bool -> int option -> - identifier + identifier * Subtac_obligations.progress diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml index 4d8f868f..1bbbfbb1 100644 --- a/contrib/subtac/subtac_coercion.ml +++ b/contrib/subtac/subtac_coercion.ml @@ -6,7 +6,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac_coercion.ml 11343 2008-09-01 20:55:13Z herbelin $ *) +(* $Id: subtac_coercion.ml 11576 2008-11-10 19:13:15Z msozeau $ *) open Util open Names @@ -33,37 +33,36 @@ open Pp let pair_of_array a = (a.(0), a.(1)) let make_name s = Name (id_of_string s) +let rec disc_subset x = + match kind_of_term x with + | App (c, l) -> + (match kind_of_term c with + Ind i -> + let len = Array.length l in + let sig_ = Lazy.force sig_ in + if len = 2 && i = Term.destInd sig_.typ + then + let (a, b) = pair_of_array l in + Some (a, b) + else None + | _ -> None) + | _ -> None + +and disc_exist env x = + match kind_of_term x with + | App (c, l) -> + (match kind_of_term c with + Construct c -> + if c = Term.destConstruct (Lazy.force sig_).intro + then Some (l.(0), l.(1), l.(2), l.(3)) + else None + | _ -> None) + | _ -> None + module Coercion = struct - + exception NoSubtacCoercion - - let rec disc_subset x = - match kind_of_term x with - | App (c, l) -> - (match kind_of_term c with - Ind i -> - let len = Array.length l in - let sig_ = Lazy.force sig_ in - if len = 2 && i = Term.destInd sig_.typ - then - let (a, b) = pair_of_array l in - Some (a, b) - else None - | _ -> None) - | _ -> None - - and disc_exist env x = - match kind_of_term x with - | App (c, l) -> - (match kind_of_term c with - Construct c -> - if c = Term.destConstruct (Lazy.force sig_).intro - then Some (l.(0), l.(1), l.(2), l.(3)) - else None - | _ -> None) - | _ -> None - - + let disc_proj_exist env x = match kind_of_term x with | App (c, l) -> diff --git a/contrib/subtac/subtac_coercion.mli b/contrib/subtac/subtac_coercion.mli index 53a8d213..5678c10e 100644 --- a/contrib/subtac/subtac_coercion.mli +++ b/contrib/subtac/subtac_coercion.mli @@ -1 +1,4 @@ +open Term +val disc_subset : types -> (types * types) option + module Coercion : Coercion.S diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index a2f54b02..4876b065 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -99,7 +99,7 @@ let interp_binder sigma env na t = SPretyping.pretype_gen sigma env ([], []) IsType (locate_if_isevar (loc_of_rawconstr t) na t) let interp_context_evars evdref env params = - let bl = Constrintern.intern_context (Evd.evars_of !evdref) env params in + let bl = Constrintern.intern_context false (Evd.evars_of !evdref) env params in let (env, par, _, impls) = List.fold_left (fun (env,params,n,impls) (na, k, b, t) -> @@ -284,7 +284,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = mkApp (constr_of_global (Lazy.force fix_sub_ref), [| argtyp ; wf_rel ; - make_existential dummy_loc ~opaque:false env isevars wf_proof ; + make_existential dummy_loc ~opaque:(Define false) env isevars wf_proof ; lift lift_cst prop ; lift lift_cst intern_body_lam |]) | Some f -> @@ -385,7 +385,7 @@ let interp_recursive fixkind l boxed = let env_rec = push_named_context rec_sign env in (* Get interpretation metadatas *) - let impls = Command.compute_interning_datas env [] fixnames fixtypes fiximps in + let impls = Command.compute_interning_datas env Constrintern.Recursive [] fixnames fixtypes fiximps in let notations = List.fold_right Option.List.cons ntnl [] in (* Interp bodies with rollback because temp use of notations/implicit *) diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index a393e2c9..cc1e2dde 100644 --- a/contrib/subtac/subtac_obligations.ml +++ b/contrib/subtac/subtac_obligations.ml @@ -1,7 +1,9 @@ +(* -*- compile-command: "make -C ../.. bin/coqtop.byte" -*- *) open Printf open Pp open Subtac_utils open Command +open Environ open Term open Names @@ -13,9 +15,11 @@ open Decl_kinds open Util open Evd open Declare +open Proof_type type definition_hook = global_reference -> unit +let ppwarn cmd = Pp.warn (str"Program:" ++ cmd) let pperror cmd = Util.errorlabstrm "Program" cmd let error s = pperror (str s) @@ -25,15 +29,17 @@ let explain_no_obligations = function Some ident -> str "No obligations for program " ++ str (string_of_id ident) | None -> str "No obligations remaining" -type obligation_info = (Names.identifier * Term.types * loc * bool * Intset.t) array - +type obligation_info = (Names.identifier * Term.types * loc * obligation_definition_status * Intset.t + * Tacexpr.raw_tactic_expr option) array + type obligation = { obl_name : identifier; obl_type : types; obl_location : loc; obl_body : constr option; - obl_opaque : bool; + obl_status : obligation_definition_status; obl_deps : Intset.t; + obl_tac : Tacexpr.raw_tactic_expr option; } type obligations = (obligation array * int) @@ -79,22 +85,29 @@ let _ = let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type -let subst_deps obls deps t = - Intset.fold - (fun x acc -> - let xobl = obls.(x) in - debug 3 (str "Trying to get body of obligation " ++ int x); - let oblb = - try Option.get xobl.obl_body - with _ -> - debug 3 (str "Couldn't get body of obligation " ++ int x); - assert(false) - in - Term.subst1 oblb (Term.subst_var xobl.obl_name acc)) - deps t - +let get_obligation_body expand obl = + let c = Option.get obl.obl_body in + if expand && obl.obl_status = Expand then + match kind_of_term c with + | Const c -> constant_value (Global.env ()) c + | _ -> c + else c + +let subst_deps expand obls deps t = + let subst = + Intset.fold + (fun x acc -> + let xobl = obls.(x) in + let oblb = + try get_obligation_body expand xobl + with _ -> assert(false) + in (xobl.obl_name, oblb) :: acc) + deps [] + in(* Termops.it_mkNamedProd_or_LetIn t subst *) + Term.replace_vars subst t + let subst_deps_obl obls obl = - let t' = subst_deps obls obl.obl_deps obl.obl_type in + let t' = subst_deps false 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) @@ -150,14 +163,14 @@ let rec intset_to = function -1 -> Intset.empty | n -> Intset.add n (intset_to (pred n)) -let subst_body prg = +let subst_body expand prg = let obls, _ = prg.prg_obligations in let ints = intset_to (pred (Array.length obls)) in - subst_deps obls ints prg.prg_body, - subst_deps obls ints (Termops.refresh_universes prg.prg_type) + subst_deps expand obls ints prg.prg_body, + subst_deps expand obls ints (Termops.refresh_universes prg.prg_type) let declare_definition prg = - let body, typ = subst_body prg in + let body, typ = subst_body false 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); @@ -188,7 +201,7 @@ let declare_definition prg = in let gr = ConstRef c in if Impargs.is_implicit_args () || prg.prg_implicits <> [] then - Impargs.declare_manual_implicits false gr (Impargs.is_implicit_args ()) prg.prg_implicits; + Impargs.declare_manual_implicits false gr prg.prg_implicits; print_message (Subtac_utils.definition_message prg.prg_name); prg.prg_hook gr; gr @@ -216,14 +229,18 @@ let compute_possible_guardness_evidences (n,_) fixbody fixtype = let ctx = fst (Sign.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 fixdefs, fixtypes, fiximps = list_split3 (List.map (fun x -> - let subs, typ = (subst_body x) in + let subs, typ = (subst_body false x) in snd (decompose_lam_n len subs), snd (decompose_prod_n len typ), x.prg_implicits) l) in +(* let fixdefs = List.map reduce_fix fixdefs in *) let fixkind = Option.get (List.hd l).prg_fixkind in let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in @@ -248,41 +265,33 @@ let declare_mutual_definition l = (match List.hd kns with ConstRef kn -> kn | _ -> assert false) let declare_obligation obl body = - let ce = - { const_entry_body = body; - const_entry_type = Some obl.obl_type; - const_entry_opaque = if get_proofs_transparency () then false else obl.obl_opaque; - const_entry_boxed = false} - in - let constant = Declare.declare_constant obl.obl_name - (DefinitionEntry ce,IsProof Property) - in - print_message (Subtac_utils.definition_message obl.obl_name); - { obl with obl_body = Some (mkConst constant) } - -let try_tactics obls = - Array.map - (fun obl -> - match obl.obl_body with - None -> - (try - let ev = evar_of_obligation obl in - let c = Subtac_utils.solve_by_tac ev Auto.default_full_auto in - declare_obligation obl c - with _ -> obl) - | _ -> obl) - obls - + match obl.obl_status with + | Expand -> { obl with obl_body = Some body } + | Define opaque -> + 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} + in + let constant = Declare.declare_constant obl.obl_name + (DefinitionEntry ce,IsProof Property) + in + print_message (Subtac_utils.definition_message obl.obl_name); + { obl with obl_body = Some (mkConst constant) } + let red = Reductionops.nf_betaiota 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) -> + (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_opaque = o; - obl_deps = d }) + obl_location = l; obl_type = red t; obl_status = o; + obl_deps = d; obl_tac = tac }) obls in { prg_name = n ; prg_body = b; prg_type = red t; prg_obligations = (obls', Array.length obls'); @@ -369,22 +378,16 @@ let has_dependencies obls n = !res let kind_of_opacity o = - if o then Subtac_utils.goal_proof_kind - else Subtac_utils.goal_kind - -let obligations_of_evars evars = - let arr = - Array.of_list - (List.map - (fun (n, t) -> - { obl_name = n; - obl_type = t; - obl_location = dummy_loc; - obl_body = None; - obl_opaque = false; - obl_deps = Intset.empty; - }) evars) - in arr, Array.length arr + match o with + | Define false | Expand -> Subtac_utils.goal_kind + | _ -> Subtac_utils.goal_proof_kind + +let not_transp_msg = + str "Obligation should be transparent but was declared opaque." ++ spc () ++ + str"Use 'Defined' instead." + +let warn_not_transp () = ppwarn not_transp_msg +let error_not_transp () = pperror not_transp_msg let rec solve_obligation prg num = let user_num = succ num in @@ -394,26 +397,37 @@ let rec solve_obligation prg num = pperror (str "Obligation" ++ spc () ++ int user_num ++ str "already" ++ spc() ++ str "solved.") else match deps_remaining obls obl.obl_deps with - [] -> - let obl = subst_deps_obl obls obl in - Command.start_proof obl.obl_name (kind_of_opacity obl.obl_opaque) obl.obl_type - (fun strength gr -> - debug 2 (str "Proof of obligation " ++ int user_num ++ str " finished"); - let obl = { obl with obl_body = Some (Libnames.constr_of_global gr) } in - let obls = Array.copy obls in - let _ = obls.(num) <- obl in - match update_obls prg obls (pred rem) with - | Remain n when n > 0 -> - if has_dependencies obls num then - ignore(auto_solve_obligations (Some prg.prg_name)) - | _ -> ()); - trace (str "Started obligation " ++ int user_num ++ str " proof: " ++ - Subtac_utils.my_print_constr (Global.env ()) obl.obl_type); - Pfedit.by !default_tactic; - Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) () - | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) " - ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l)) - + | [] -> + let obl = subst_deps_obl obls obl in + Command.start_proof obl.obl_name (kind_of_opacity obl.obl_status) obl.obl_type + (fun strength gr -> + let cst = match gr with ConstRef cst -> cst | _ -> assert false in + let obl = + let transparent = evaluable_constant cst (Global.env ()) in + let body = + match obl.obl_status with + | Expand -> + if not transparent then error_not_transp () + else constant_value (Global.env ()) cst + | 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 + let obls = Array.copy obls in + let _ = obls.(num) <- obl in + match update_obls prg obls (pred rem) with + | Remain n when n > 0 -> + if has_dependencies obls num then + ignore(auto_solve_obligations (Some prg.prg_name) None) + | _ -> ()); + trace (str "Started obligation " ++ int user_num ++ str " proof: " ++ + Subtac_utils.my_print_constr (Global.env ()) obl.obl_type); + Pfedit.by !default_tactic; + Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) () + | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) " + ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l)) + and subtac_obligation (user_num, name, typ) = let num = pred user_num in let prg = get_prog_err name in @@ -434,12 +448,17 @@ and solve_obligation_by_tac prg obls i tac = (try if deps_remaining obls obl.obl_deps = [] then let obl = subst_deps_obl obls obl in + let tac = + match tac with + | Some t -> t + | None -> + match obl.obl_tac with + | Some t -> Tacinterp.interp t + | None -> !default_tactic + in let t = Subtac_utils.solve_by_tac (evar_of_obligation obl) tac in - if obl.obl_opaque then - obls.(i) <- declare_obligation obl t - else - obls.(i) <- { obl with obl_body = Some t }; - true + obls.(i) <- declare_obligation obl t; + true else false with | Stdpp.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s))) @@ -473,34 +492,40 @@ and try_solve_obligation n prg tac = let obls' = Array.copy obls in if solve_obligation_by_tac prg obls' n tac then ignore(update_obls prg obls' (pred rem)); - + and try_solve_obligations n tac = try ignore (solve_obligations n tac) with NoObligations _ -> () -and auto_solve_obligations n : progress = +and auto_solve_obligations n tac : progress = Flags.if_verbose msgnl (str "Solving obligations automatically..."); - try solve_obligations n !default_tactic with NoObligations _ -> Dependent + 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 n = prg.prg_name in let obls, rem = prg.prg_obligations in + let showed = ref 5 in if msg then msgnl (int rem ++ str " obligation(s) remaining: "); Array.iteri (fun i x -> match x.obl_body with - None -> msgnl (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++ str "of" ++ spc() ++ str (string_of_id n) ++ str ":" ++ spc () ++ - my_print_constr (Global.env ()) x.obl_type ++ str "." ++ fnl ()) - | Some _ -> ()) + | None -> + if !showed > 0 then ( + decr showed; + msgnl (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++ + str "of" ++ spc() ++ str (string_of_id n) ++ str ":" ++ spc () ++ + hov 1 (my_print_constr (Global.env ()) x.obl_type ++ str "." ++ fnl ()))) + | Some _ -> ()) obls - + let show_term n = let prg = get_prog_err n in let n = prg.prg_name in - msgnl (str (string_of_id n) ++ spc () ++ str":" ++ spc () ++ my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl () + msgnl (str (string_of_id n) ++ spc () ++ str":" ++ spc () ++ + 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) ?(hook=fun x -> ()) obls = +let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic ?(hook=fun x -> ()) 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 obls,_ = prg.prg_obligations in @@ -513,12 +538,12 @@ let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?(hook= let len = Array.length obls in let _ = Flags.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in from_prg := ProgMap.add n prg !from_prg; - let res = auto_solve_obligations (Some n) in + let res = auto_solve_obligations (Some n) tactic in match res with - | Remain rem when rem < 5 -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res - | _ -> res) + | Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res + | _ -> res) -let add_mutual_definitions l ?(kind=Global,false,Definition) notations fixkind = +let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) notations fixkind = 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) -> @@ -531,8 +556,9 @@ let add_mutual_definitions l ?(kind=Global,false,Definition) notations fixkind = List.fold_left (fun finished x -> if finished then finished else - match auto_solve_obligations (Some x) with - Defined _ -> (* If one definition is turned into a constant, the whole block is defined. *) true + let res = auto_solve_obligations (Some x) tactic in + match res with + | Defined _ -> (* If one definition is turned into a constant, the whole block is defined. *) true | _ -> false) false deps in () @@ -562,8 +588,8 @@ let next_obligation n = let prg = get_prog_err n in let obls, rem = prg.prg_obligations in let i = - array_find (fun x -> x.obl_body = None && deps_remaining obls x.obl_deps = []) - obls + try array_find (fun x -> x.obl_body = None && deps_remaining obls x.obl_deps = []) obls + with Not_found -> anomaly "Could not find a solvable obligation." in solve_obligation prg i let default_tactic () = !default_tactic diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli index 6d13e3bd..60c0a413 100644 --- a/contrib/subtac/subtac_obligations.mli +++ b/contrib/subtac/subtac_obligations.mli @@ -1,9 +1,14 @@ open Names open Util open Libnames +open Evd +open Proof_type -type obligation_info = (Names.identifier * Term.types * loc * bool * Intset.t) array - (* ident, type, location, opaque or transparent, dependencies *) +type obligation_info = + (identifier * Term.types * loc * + obligation_definition_status * Intset.t * Tacexpr.raw_tactic_expr 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 *) @@ -21,6 +26,7 @@ type definition_hook = global_reference -> unit val add_definition : Names.identifier -> Term.constr -> Term.types -> ?implicits:(Topconstr.explicitation * (bool * bool)) list -> ?kind:Decl_kinds.definition_kind -> + ?tactic:Proof_type.tactic -> ?hook:definition_hook -> obligation_info -> progress type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list @@ -28,6 +34,7 @@ type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) val add_mutual_definitions : (Names.identifier * Term.constr * Term.types * (Topconstr.explicitation * (bool * bool)) list * obligation_info) list -> + ?tactic:Proof_type.tactic -> ?kind:Decl_kinds.definition_kind -> notations -> Command.fixpoint_kind -> unit @@ -36,14 +43,14 @@ val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr op val next_obligation : Names.identifier option -> unit -val solve_obligations : Names.identifier option -> Proof_type.tactic -> progress +val solve_obligations : Names.identifier option -> Proof_type.tactic option -> progress (* Number of remaining obligations to be solved for this program *) -val solve_all_obligations : Proof_type.tactic -> unit +val solve_all_obligations : Proof_type.tactic option -> unit -val try_solve_obligation : int -> Names.identifier option -> Proof_type.tactic -> unit +val try_solve_obligation : int -> Names.identifier option -> Proof_type.tactic option -> unit -val try_solve_obligations : Names.identifier option -> Proof_type.tactic -> unit +val try_solve_obligations : Names.identifier option -> Proof_type.tactic option -> unit val show_obligations : ?msg:bool -> Names.identifier option -> unit diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml index ad76bdeb..07a75720 100644 --- a/contrib/subtac/subtac_pretyping.ml +++ b/contrib/subtac/subtac_pretyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac_pretyping.ml 11282 2008-07-28 11:51:53Z msozeau $ *) +(* $Id: subtac_pretyping.ml 11574 2008-11-10 13:45:05Z msozeau $ *) open Global open Pp @@ -73,7 +73,7 @@ let interp env isevars c tycon = let _ = isevars := Evarutil.nf_evar_defs !isevars in let evd,_ = consider_remaining_unif_problems env !isevars in (* let unevd = undefined_evars evd in *) - let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env evd in + let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:true ~fail:true env evd in let evm = evars_of unevd' in isevars := unevd'; nf_evar evm j.uj_val, nf_evar evm j.uj_type diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml index 559b6ac1..00d37f35 100644 --- a/contrib/subtac/subtac_pretyping_F.ml +++ b/contrib/subtac/subtac_pretyping_F.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac_pretyping_F.ml 11282 2008-07-28 11:51:53Z msozeau $ *) +(* $Id: subtac_pretyping_F.ml 11576 2008-11-10 19:13:15Z msozeau $ *) open Pp open Util @@ -276,14 +276,19 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct | RApp (loc,f,args) -> let length = List.length args in - let ftycon = - if length > 0 then - match tycon with - | None -> None - | Some (None, ty) -> mk_abstr_tycon length ty - | Some (Some (init, cur), ty) -> - Some (Some (length + init, length + cur), ty) - else tycon + let ftycon = + let ty = + if length > 0 then + match tycon with + | None -> None + | Some (None, ty) -> mk_abstr_tycon length ty + | Some (Some (init, cur), ty) -> + Some (Some (length + init, length + cur), ty) + else tycon + in + match ty with + | Some (_, t) when Subtac_coercion.disc_subset t = None -> ty + | _ -> None in let fj = pretype ftycon env isevars lvar f in let floc = loc_of_rawconstr f in diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml index bae2731a..cdbc4023 100644 --- a/contrib/subtac/subtac_utils.ml +++ b/contrib/subtac/subtac_utils.ml @@ -159,7 +159,7 @@ let app_opt c e = let print_args env args = Array.fold_right (fun a acc -> my_print_constr env a ++ spc () ++ acc) args (str "") -let make_existential loc ?(opaque = true) env isevars c = +let make_existential loc ?(opaque = Define true) env isevars c = let evar = Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark opaque) c in let (key, args) = destEvar evar in (try trace (str "Constructed evar " ++ int key ++ str " applied to args: " ++ @@ -232,7 +232,7 @@ let build_dependent_sum l = trace (spc () ++ str ("treating evar " ^ string_of_id n)); (try trace (str " assert: " ++ my_print_constr (Global.env ()) hyptype) with _ -> ()); - let tac = assert_tac true (Name n) hyptype in + let tac = assert_tac (Name n) hyptype in let conttac = (fun cont -> conttac @@ -369,7 +369,7 @@ let solve_by_tac evi t = Pfedit.start_proof id goal_kind evi.evar_hyps evi.evar_concl (fun _ _ -> ()); Pfedit.by (tclCOMPLETE t); - let _,(const,_,_) = Pfedit.cook_proof ignore in + let _,(const,_,_,_) = Pfedit.cook_proof ignore in Pfedit.delete_current_proof (); const.Entries.const_entry_body with e -> Pfedit.delete_current_proof(); @@ -470,4 +470,3 @@ let tactics_tac s = let tactics_call tac args = TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (tactics_tac tac)),args)) - diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli index 49335211..964f668f 100644 --- a/contrib/subtac/subtac_utils.mli +++ b/contrib/subtac/subtac_utils.mli @@ -83,7 +83,8 @@ val wf_relations : (constr, constr lazy_t) Hashtbl.t type binders = local_binder list val app_opt : ('a -> 'a) option -> 'a -> 'a val print_args : env -> constr array -> std_ppcmds -val make_existential : loc -> ?opaque:bool -> env -> evar_defs ref -> types -> constr +val make_existential : loc -> ?opaque:obligation_definition_status -> + env -> evar_defs ref -> types -> constr val make_existential_expr : loc -> 'a -> 'b -> constr_expr val string_of_hole_kind : hole_kind -> string val evars_of_term : evar_map -> evar_map -> constr -> evar_map |