summaryrefslogtreecommitdiff
path: root/contrib/subtac
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/subtac')
-rw-r--r--contrib/subtac/equations.ml41149
-rw-r--r--contrib/subtac/eterm.ml121
-rw-r--r--contrib/subtac/eterm.mli22
-rw-r--r--contrib/subtac/g_subtac.ml416
-rw-r--r--contrib/subtac/subtac.ml38
-rw-r--r--contrib/subtac/subtac_cases.ml4
-rw-r--r--contrib/subtac/subtac_classes.ml159
-rw-r--r--contrib/subtac/subtac_classes.mli10
-rw-r--r--contrib/subtac/subtac_coercion.ml59
-rw-r--r--contrib/subtac/subtac_coercion.mli3
-rw-r--r--contrib/subtac/subtac_command.ml6
-rw-r--r--contrib/subtac/subtac_obligations.ml246
-rw-r--r--contrib/subtac/subtac_obligations.mli19
-rw-r--r--contrib/subtac/subtac_pretyping.ml4
-rw-r--r--contrib/subtac/subtac_pretyping_F.ml23
-rw-r--r--contrib/subtac/subtac_utils.ml7
-rw-r--r--contrib/subtac/subtac_utils.mli3
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 06:39:00 +0000