aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/dp/dp_plugin.mllib1
-rw-r--r--plugins/funind/merge.ml7
-rw-r--r--plugins/interface/xlate.ml4
-rw-r--r--plugins/subtac/equations.ml41149
-rw-r--r--plugins/subtac/eterm.ml68
-rw-r--r--plugins/subtac/eterm.mli16
-rw-r--r--plugins/subtac/g_eterm.ml427
-rw-r--r--plugins/subtac/subtac.ml6
-rw-r--r--plugins/subtac/subtac_classes.ml9
-rw-r--r--plugins/subtac/subtac_command.ml41
-rw-r--r--plugins/subtac/subtac_obligations.ml155
-rw-r--r--plugins/subtac/subtac_obligations.mli14
-rw-r--r--plugins/subtac/subtac_plugin.mllib2
-rw-r--r--plugins/subtac/subtac_pretyping.ml4
-rw-r--r--plugins/subtac/subtac_utils.ml9
-rw-r--r--plugins/subtac/subtac_utils.mli1
16 files changed, 204 insertions, 1309 deletions
diff --git a/plugins/dp/dp_plugin.mllib b/plugins/dp/dp_plugin.mllib
index adb9721a19..63252d6a23 100644
--- a/plugins/dp/dp_plugin.mllib
+++ b/plugins/dp/dp_plugin.mllib
@@ -1,6 +1,5 @@
Dp_why
Dp_zenon
Dp
-Dp_gappa
G_dp
Dp_plugin_mod
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 3538f63426..8aeff61e6a 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -151,11 +151,6 @@ let showind (id:identifier) =
exception Found of int
(* Array scanning *)
-let array_find (arr: 'a array) (pred: int -> 'a -> bool): int option =
- try
- for i=0 to Array.length arr - 1 do if pred i (arr.(i)) then raise (Found i) done;
- None
- with Found i -> Some i
let array_prfx (arr: 'a array) (pred: int -> 'a -> bool): int =
try
@@ -941,7 +936,7 @@ let merge (id1:identifier) (id2:identifier) (args1:identifier array)
as above: vars may be linked inside args2?? *)
Array.mapi
(fun i c ->
- match array_find args1 (fun i x -> x=c) with
+ match array_find_i (fun i x -> x=c) args1 with
| Some j -> Linked j
| None -> Unlinked)
args2 in
diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml
index 627cd517c3..261bb0029c 100644
--- a/plugins/interface/xlate.ml
+++ b/plugins/interface/xlate.ml
@@ -2145,8 +2145,8 @@ let rec xlate_vernac =
CT_coercion (local_opt, id_opt, xlate_ident id1,
xlate_class id2, xlate_class id3)
- (* Type Classes *)
- | VernacDeclareInstance _|VernacContext _|
+ (* Type Classes *)
+ | VernacDeclareInstance _ | VernacDeclareClass _ | VernacContext _ |
VernacInstance (_, _, _, _, _) ->
xlate_error "TODO: Type Classes commands"
diff --git a/plugins/subtac/equations.ml4 b/plugins/subtac/equations.ml4
deleted file mode 100644
index ca4445cc2e..0000000000
--- a/plugins/subtac/equations.ml4
+++ /dev/null
@@ -1,1149 +0,0 @@
-(* -*- compile-command: "make -C ../.. bin/coqtop.byte" -*- *)
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(*i camlp4deps: "parsing/grammar.cma" i*)
-(*i camlp4use: "pa_extend.cmo" i*)
-
-(* $Id$ *)
-
-open Cases
-open Util
-open Names
-open Nameops
-open Term
-open Termops
-open Declarations
-open Inductiveops
-open Environ
-open Sign
-open Reductionops
-open Typeops
-open Type_errors
-
-open Rawterm
-open Retyping
-open Pretype_errors
-open Evarutil
-open Evarconv
-open List
-open Libnames
-
-type pat =
- | PRel of int
- | PCstr of constructor * pat list
- | PInac of constr
-
-let coq_inacc = lazy (Coqlib.gen_constant "equations" ["Program";"Equality"] "inaccessible_pattern")
-
-let mkInac env c =
- mkApp (Lazy.force coq_inacc, [| Typing.type_of env Evd.empty c ; c |])
-
-let rec constr_of_pat ?(inacc=true) env = function
- | PRel i -> mkRel i
- | PCstr (c, p) ->
- let c' = mkConstruct c in
- mkApp (c', Array.of_list (constrs_of_pats ~inacc env p))
- | PInac r ->
- if inacc then try mkInac env r with _ -> r else r
-
-and constrs_of_pats ?(inacc=true) env l = map (constr_of_pat ~inacc env) l
-
-let rec pat_vars = function
- | PRel i -> Intset.singleton i
- | PCstr (c, p) -> pats_vars p
- | PInac _ -> Intset.empty
-
-and pats_vars l =
- fold_left (fun vars p ->
- let pvars = pat_vars p in
- let inter = Intset.inter pvars vars in
- if inter = Intset.empty then
- Intset.union pvars vars
- else error ("Non-linear pattern: variable " ^
- string_of_int (Intset.choose inter) ^ " appears twice"))
- Intset.empty l
-
-let rec pats_of_constrs l = map pat_of_constr l
-and pat_of_constr c =
- match kind_of_term c with
- | Rel i -> PRel i
- | App (f, [| a ; c |]) when eq_constr f (Lazy.force coq_inacc) ->
- PInac c
- | App (f, args) when isConstruct f ->
- PCstr (destConstruct f, pats_of_constrs (Array.to_list args))
- | Construct f -> PCstr (f, [])
- | _ -> PInac c
-
-let inaccs_of_constrs l = map (fun x -> PInac x) l
-
-exception Conflict
-
-let rec pmatch p c =
- match p, c with
- | PRel i, t -> [i, t]
- | PCstr (c, pl), PCstr (c', pl') when c = c' -> pmatches pl pl'
- | PInac _, _ -> []
- | _, PInac _ -> []
- | _, _ -> raise Conflict
-
-and pmatches pl l =
- match pl, l with
- | [], [] -> []
- | hd :: tl, hd' :: tl' ->
- pmatch hd hd' @ pmatches tl tl'
- | _ -> raise Conflict
-
-let pattern_matches pl l = try Some (pmatches pl l) with Conflict -> None
-
-let rec pinclude p c =
- match p, c with
- | PRel i, t -> true
- | PCstr (c, pl), PCstr (c', pl') when c = c' -> pincludes pl pl'
- | PInac _, _ -> true
- | _, PInac _ -> true
- | _, _ -> false
-
-and pincludes pl l =
- match pl, l with
- | [], [] -> true
- | hd :: tl, hd' :: tl' ->
- pinclude hd hd' && pincludes tl tl'
- | _ -> false
-
-let pattern_includes pl l = pincludes pl l
-
-(** Specialize by a substitution. *)
-
-let subst_tele s = replace_vars (List.map (fun (id, _, t) -> id, t) s)
-
-let subst_rel_subst k s c =
- let rec aux depth c =
- match kind_of_term c with
- | Rel n ->
- let k = n - depth in
- if k >= 0 then
- try lift depth (snd (assoc k s))
- with Not_found -> c
- else c
- | _ -> map_constr_with_binders succ aux depth c
- in aux k c
-
-let subst_context s ctx =
- let (_, ctx') = fold_right
- (fun (id, b, t) (k, ctx') ->
- (succ k, (id, Option.map (subst_rel_subst k s) b, subst_rel_subst k s t) :: ctx'))
- ctx (0, [])
- in ctx'
-
-let subst_rel_context k cstr ctx =
- let (_, ctx') = fold_right
- (fun (id, b, t) (k, ctx') ->
- (succ k, (id, Option.map (substnl [cstr] k) b, substnl [cstr] k t) :: ctx'))
- ctx (k, [])
- in ctx'
-
-let rec lift_pat n k p =
- match p with
- | PRel i ->
- if i >= k then PRel (i + n)
- else p
- | PCstr(c, pl) -> PCstr (c, lift_pats n k pl)
- | PInac r -> PInac (liftn n k r)
-
-and lift_pats n k = map (lift_pat n k)
-
-let rec subst_pat env k t p =
- match p with
- | PRel i ->
- if i = k then t
- else if i > k then PRel (pred i)
- else p
- | PCstr(c, pl) ->
- PCstr (c, subst_pats env k t pl)
- | PInac r -> PInac (substnl [constr_of_pat ~inacc:false env t] (pred k) r)
-
-and subst_pats env k t = map (subst_pat env k t)
-
-let rec specialize s p =
- match p with
- | PRel i ->
- if mem_assoc i s then
- let b, t = assoc i s in
- if b then PInac t
- else PRel (destRel t)
- else p
- | PCstr(c, pl) ->
- PCstr (c, specialize_pats s pl)
- | PInac r -> PInac (specialize_constr s r)
-
-and specialize_constr s c = subst_rel_subst 0 s c
-and specialize_pats s = map (specialize s)
-
-let specialize_patterns = function
- | [] -> fun p -> p
- | s -> specialize_pats s
-
-let specialize_rel_context s ctx =
- snd (fold_right (fun (n, b, t) (k, ctx) ->
- (succ k, (n, Option.map (subst_rel_subst k s) b, subst_rel_subst k s t) :: ctx))
- ctx (0, []))
-
-let lift_contextn n k sign =
- let rec liftrec k = function
- | (na,c,t)::sign ->
- (na,Option.map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign)
- | [] -> []
- in
- liftrec (rel_context_length sign + k) sign
-
-type program =
- signature * clause list
-
-and signature = identifier * rel_context * constr
-
-and clause = lhs * (constr, int) rhs
-
-and lhs = rel_context * identifier * pat list
-
-and ('a, 'b) rhs =
- | Program of 'a
- | Empty of 'b
-
-type splitting =
- | Compute of clause
- | Split of lhs * int * inductive_family *
- unification_result array * splitting option array
-
-and unification_result =
- rel_context * int * constr * pat * substitution option
-
-and substitution = (int * (bool * constr)) list
-
-type problem = identifier * lhs
-
-let rels_of_tele tele = rel_list 0 (List.length tele)
-
-let patvars_of_tele tele = map (fun c -> PRel (destRel c)) (rels_of_tele tele)
-
-let split_solves split prob =
- match split with
- | Compute (lhs, rhs) -> lhs = prob
- | Split (lhs, id, indf, us, ls) -> lhs = prob
-
-let ids_of_constr c =
- let rec aux vars c =
- match kind_of_term c with
- | Var id -> Idset.add id vars
- | _ -> fold_constr aux vars c
- in aux Idset.empty c
-
-let ids_of_constrs =
- fold_left (fun acc x -> Idset.union (ids_of_constr x) acc) Idset.empty
-
-let idset_of_list =
- fold_left (fun s x -> Idset.add x s) Idset.empty
-
-let intset_of_list =
- fold_left (fun s x -> Intset.add x s) Intset.empty
-
-let solves split (delta, id, pats as prob) =
- split_solves split prob &&
- Intset.equal (pats_vars pats) (intset_of_list (map destRel (rels_of_tele delta)))
-
-let check_judgment ctx c t =
- ignore(Typing.check (push_rel_context ctx (Global.env ())) Evd.empty c t); true
-
-let check_context env ctx =
- fold_right
- (fun (_, _, t as decl) env ->
- ignore(Typing.sort_of env Evd.empty t); push_rel decl env)
- ctx env
-
-let split_context n c =
- let after, before = list_chop n c in
- match before with
- | hd :: tl -> after, hd, tl
- | [] -> raise (Invalid_argument "split_context")
-
-let split_tele n (ctx : rel_context) =
- let rec aux after n l =
- match n, l with
- | 0, decl :: before -> before, decl, List.rev after
- | n, decl :: before -> aux (decl :: after) (pred n) before
- | _ -> raise (Invalid_argument "split_tele")
- in aux [] n ctx
-
-let rec add_var_subst env subst n c =
- if mem_assoc n subst then
- let t = assoc n subst in
- if eq_constr t c then subst
- else unify env subst t c
- else
- let rel = mkRel n in
- if rel = c then subst
- else if dependent rel c then raise Conflict
- else (n, c) :: subst
-
-and unify env subst x y =
- match kind_of_term x, kind_of_term y with
- | Rel n, _ -> add_var_subst env subst n y
- | _, Rel n -> add_var_subst env subst n x
- | App (c, l), App (c', l') when eq_constr c c' ->
- unify_constrs env subst (Array.to_list l) (Array.to_list l')
- | _, _ -> if eq_constr x y then subst else raise Conflict
-
-and unify_constrs (env : env) subst l l' =
- if List.length l = List.length l' then
- fold_left2 (unify env) subst l l'
- else raise Conflict
-
-let fold_rel_context_with_binders f ctx init =
- snd (List.fold_right (fun decl (depth, acc) ->
- (succ depth, f depth decl acc)) ctx (0, init))
-
-let dependent_rel_context (ctx : rel_context) k =
- fold_rel_context_with_binders
- (fun depth (n,b,t) acc ->
- let r = mkRel (depth + k) in
- acc || dependent r t ||
- (match b with
- | Some b -> dependent r b
- | None -> false))
- ctx false
-
-let liftn_between n k p c =
- let rec aux depth c = match kind_of_term c with
- | Rel i ->
- if i <= depth then c
- else if i-depth > p then c
- else mkRel (i - n)
- | _ -> map_constr_with_binders succ aux depth c
- in aux k c
-
-let liftn_rel_context n k sign =
- let rec liftrec k = function
- | (na,c,t)::sign ->
- (na,Option.map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign)
- | [] -> []
- in
- liftrec (k + rel_context_length sign) sign
-
-let substnl_rel_context n l =
- map_rel_context_with_binders (fun k -> substnl l (n+k-1))
-
-let reduce_rel_context (ctx : rel_context) (subst : (int * (bool * constr)) list) =
- let _, s, ctx' =
- fold_left (fun (k, s, ctx') (n, b, t as decl) ->
- match b with
- | None -> (succ k, mkRel k :: s, ctx' @ [decl])
- | Some t -> (k, lift (pred k) t :: map (substnl [t] (pred k)) s, subst_rel_context 0 t ctx'))
- (1, [], []) ctx
- in
- let s = rev s in
- let s' = map (fun (korig, (b, knew)) -> korig, (b, substl s knew)) subst in
- s', ctx'
-
-(* Compute the transitive closure of the dependency relation for a term in a context *)
-
-let rec dependencies_of_rel ctx k =
- let (n,b,t) = nth ctx (pred k) in
- let b = Option.map (lift k) b and t = lift k t in
- let bdeps = match b with Some b -> dependencies_of_term ctx b | None -> Intset.empty in
- Intset.union (Intset.singleton k) (Intset.union bdeps (dependencies_of_term ctx t))
-
-and dependencies_of_term ctx t =
- let rels = free_rels t in
- Intset.fold (fun i -> Intset.union (dependencies_of_rel ctx i)) rels Intset.empty
-
-let subst_telescope k cstr ctx =
- let (_, ctx') = fold_left
- (fun (k, ctx') (id, b, t) ->
- (succ k, (id, Option.map (substnl [cstr] k) b, substnl [cstr] k t) :: ctx'))
- (k, []) ctx
- in rev ctx'
-
-let lift_telescope n k sign =
- let rec liftrec k = function
- | (na,c,t)::sign ->
- (na,Option.map (liftn n k) c,liftn n k t)::(liftrec (succ k) sign)
- | [] -> []
- in liftrec k sign
-
-type ('a,'b) either = Inl of 'a | Inr of 'b
-
-let strengthen (ctx : rel_context) (t : constr) : rel_context * rel_context * (int * (int, int) either) list =
- let rels = dependencies_of_term ctx t in
- let len = length ctx in
- let nbdeps = Intset.cardinal rels in
- let lifting = len - nbdeps in (* Number of variables not linked to t *)
- let rec aux k n acc m rest s = function
- | decl :: ctx' ->
- if Intset.mem k rels then
- let rest' = subst_telescope 0 (mkRel (nbdeps + lifting - pred m)) rest in
- aux (succ k) (succ n) (decl :: acc) m rest' ((k, Inl n) :: s) ctx'
- else aux (succ k) n (subst_telescope 0 mkProp acc) (succ m) (decl :: rest) ((k, Inr m) :: s) ctx'
- | [] -> rev acc, rev rest, s
- in aux 1 1 [] 1 [] [] ctx
-
-let merge_subst (ctx', rest, s) =
- let lenrest = length rest in
- map (function (k, Inl x) -> (k, (false, mkRel (x + lenrest))) | (k, Inr x) -> k, (false, mkRel x)) s
-
-(* let simplify_subst s = *)
-(* fold_left (fun s (k, t) -> *)
-(* match kind_of_term t with *)
-(* | Rel n when n = k -> s *)
-(* | _ -> (k, t) :: s) *)
-(* [] s *)
-
-let compose_subst s' s =
- map (fun (k, (b, t)) -> (k, (b, specialize_constr s' t))) s
-
-let substitute_in_ctx n c ctx =
- let rec aux k after = function
- | [] -> []
- | (name, b, t as decl) :: before ->
- if k = n then rev after @ (name, Some c, t) :: before
- else aux (succ k) (decl :: after) before
- in aux 1 [] ctx
-
-let rec reduce_subst (ctx : rel_context) (substacc : (int * (bool * constr)) list) (cursubst : (int * (bool * constr)) list) =
- match cursubst with
- | [] -> ctx, substacc
- | (k, (b, t)) :: rest ->
- if t = mkRel k then reduce_subst ctx substacc rest
- else if noccur_between 1 k t then
- (* The term to substitute refers only to previous variables. *)
- let t' = lift (-k) t in
- let ctx' = substitute_in_ctx k t' ctx in
- reduce_subst ctx' substacc rest
- else (* The term refers to variables declared after [k], so we have
- to move these dependencies before [k]. *)
- let (minctx, ctxrest, subst as str) = strengthen ctx t in
- match assoc k subst with
- | Inl _ -> error "Occurs check in substituted_context"
- | Inr k' ->
- let s = merge_subst str in
- let ctx' = ctxrest @ minctx in
- let rest' =
- let substsubst (k', (b, t')) =
- match kind_of_term (snd (assoc k' s)) with
- | Rel k'' -> (k'', (b, specialize_constr s t'))
- | _ -> error "Non-variable substituted for variable by strenghtening"
- in map substsubst ((k, (b, t)) :: rest)
- in
- reduce_subst ctx' (compose_subst s substacc) rest' (* (compose_subst s ((k, (b, t)) :: rest)) *)
-
-
-let substituted_context (subst : (int * constr) list) (ctx : rel_context) =
- let _, subst =
- fold_left (fun (k, s) _ ->
- try let t = assoc k subst in
- (succ k, (k, (true, t)) :: s)
- with Not_found ->
- (succ k, ((k, (false, mkRel k)) :: s)))
- (1, []) ctx
- in
- let ctx', subst' = reduce_subst ctx subst subst in
- reduce_rel_context ctx' subst'
-
-let unify_type before ty =
- try
- let envb = push_rel_context before (Global.env()) in
- let IndType (indf, args) = find_rectype envb Evd.empty ty in
- let ind, params = dest_ind_family indf in
- let vs = map (Reduction.whd_betadeltaiota envb) args in
- let cstrs = Inductiveops.arities_of_constructors envb ind in
- let cstrs =
- Array.mapi (fun i ty ->
- let ty = prod_applist ty params in
- let ctx, ty = decompose_prod_assum ty in
- let ctx, ids =
- let ids = ids_of_rel_context ctx in
- fold_right (fun (n, b, t as decl) (acc, ids) ->
- match n with Name _ -> (decl :: acc), ids
- | Anonymous -> let id = next_name_away Anonymous ids in
- ((Name id, b, t) :: acc), (id :: ids))
- ctx ([], ids)
- in
- let env' = push_rel_context ctx (Global.env ()) in
- let IndType (indf, args) = find_rectype env' Evd.empty ty in
- let ind, params = dest_ind_family indf in
- let constr = applist (mkConstruct (ind, succ i), params @ rels_of_tele ctx) in
- let constrpat = PCstr ((ind, succ i), inaccs_of_constrs params @ patvars_of_tele ctx) in
- env', ctx, constr, constrpat, (* params @ *)args)
- cstrs
- in
- let res =
- Array.map (fun (env', ctxc, c, cpat, us) ->
- let _beforelen = length before and ctxclen = length ctxc in
- let fullctx = ctxc @ before in
- try
- let fullenv = push_rel_context fullctx (Global.env ()) in
- let vs' = map (lift ctxclen) vs in
- let subst = unify_constrs fullenv [] vs' us in
- let subst', ctx' = substituted_context subst fullctx in
- (ctx', ctxclen, c, cpat, Some subst')
- with Conflict ->
- (fullctx, ctxclen, c, cpat, None)) cstrs
- in Some (res, indf)
- with Not_found -> (* not an inductive type *)
- None
-
-let rec id_of_rel n l =
- match n, l with
- | 0, (Name id, _, _) :: tl -> id
- | n, _ :: tl -> id_of_rel (pred n) tl
- | _, _ -> raise (Invalid_argument "id_of_rel")
-
-let constrs_of_lhs ?(inacc=true) env (ctx, _, pats) =
- constrs_of_pats ~inacc (push_rel_context ctx env) pats
-
-let rec valid_splitting (f, delta, t, pats) tree =
- split_solves tree (delta, f, pats) &&
- valid_splitting_tree (f, delta, t) tree
-
-and valid_splitting_tree (f, delta, t) = function
- | Compute (lhs, Program rhs) ->
- let subst = constrs_of_lhs ~inacc:false (Global.env ()) lhs in
- ignore(check_judgment (pi1 lhs) rhs (substl subst t)); true
-
- | Compute ((ctx, id, lhs), Empty split) ->
- let before, (x, _, ty), after = split_context split ctx in
- let unify =
- match unify_type before ty with
- | Some (unify, _) -> unify
- | None -> assert false
- in
- array_for_all (fun (_, _, _, _, x) -> x = None) unify
-
- | Split ((ctx, id, lhs), rel, indf, unifs, ls) ->
- let before, (id, _, ty), after = split_tele (pred rel) ctx in
- let unify, indf' = Option.get (unify_type before ty) in
- assert(indf = indf');
- if not (array_exists (fun (_, _, _, _, x) -> x <> None) unify) then false
- else
- let ok, splits =
- Array.fold_left (fun (ok, splits as acc) (ctx', ctxlen, cstr, cstrpat, subst) ->
- match subst with
- | None -> acc
- | Some subst ->
-(* let env' = push_rel_context ctx' (Global.env ()) in *)
-(* let ctx_correct = *)
-(* ignore(check_context env' (subst_context subst ctxc)); *)
-(* ignore(check_context env' (subst_context subst before)); *)
-(* true *)
-(* in *)
- let newdelta =
- subst_context subst (subst_rel_context 0 cstr
- (lift_contextn ctxlen 0 after)) @ before in
- let liftpats = lift_pats ctxlen rel lhs in
- let newpats = specialize_patterns subst (subst_pats (Global.env ()) rel cstrpat liftpats) in
- (ok, (f, newdelta, newpats) :: splits))
- (true, []) unify
- in
- let subst = List.map2 (fun (id, _, _) x -> out_name id, x) delta
- (constrs_of_pats ~inacc:false (Global.env ()) lhs)
- in
- let t' = replace_vars subst t in
- ok && for_all
- (fun (f, delta', pats') ->
- array_exists (function None -> false | Some tree -> valid_splitting (f, delta', t', pats') tree) ls) splits
-
-let valid_tree (f, delta, t) tree =
- valid_splitting (f, delta, t, patvars_of_tele delta) tree
-
-let is_constructor c =
- match kind_of_term (fst (decompose_app c)) with
- | Construct _ -> true
- | _ -> false
-
-let find_split (_, _, curpats : lhs) (_, _, patcs : lhs) =
- let rec find_split_pat curpat patc =
- match patc with
- | PRel _ -> None
- | PCstr (f, args) ->
- (match curpat with
- | PCstr (f', args') when f = f' -> (* Already split at this level, continue *)
- find_split_pats args' args
- | PRel i -> (* Split on i *) Some i
- | PInac c when isRel c -> Some (destRel c)
- | _ -> None)
- | PInac _ -> None
-
- and find_split_pats curpats patcs =
- assert(List.length curpats = List.length patcs);
- fold_left2 (fun acc ->
- match acc with
- | None -> find_split_pat | _ -> fun _ _ -> acc)
- None curpats patcs
- in find_split_pats curpats patcs
-
-open Pp
-open Termops
-
-let pr_constr_pat env c =
- let pr = print_constr_env env c in
- match kind_of_term c with
- | App _ -> str "(" ++ pr ++ str ")"
- | _ -> pr
-
-let pr_pat env c =
- try
- let patc = constr_of_pat env c in
- try pr_constr_pat env patc with _ -> str"pr_constr_pat raised an exception"
- with _ -> str"constr_of_pat raised an exception"
-
-let pr_context env c =
- let pr_decl (id,b,_) =
- let bstr = match b with Some b -> str ":=" ++ spc () ++ print_constr_env env b | None -> mt() in
- let idstr = match id with Name id -> pr_id id | Anonymous -> str"_" in
- idstr ++ bstr
- in
- prlist_with_sep pr_spc pr_decl (List.rev c)
-(* Printer.pr_rel_context env c *)
-
-let pr_lhs env (delta, f, patcs) =
- let env = push_rel_context delta env in
- let ctx = pr_context env delta in
- (if delta = [] then ctx else str "[" ++ ctx ++ str "]" ++ spc ())
- ++ pr_id f ++ spc () ++ prlist_with_sep spc (pr_pat env) patcs
-
-let pr_rhs env = function
- | Empty var -> spc () ++ str ":=!" ++ spc () ++ print_constr_env env (mkRel var)
- | Program rhs -> spc () ++ str ":=" ++ spc () ++ print_constr_env env rhs
-
-let pr_clause env (lhs, rhs) =
- pr_lhs env lhs ++
- (let env' = push_rel_context (pi1 lhs) env in
- pr_rhs env' rhs)
-
-(* let pr_splitting env = function *)
-(* | Compute cl -> str "Compute " ++ pr_clause env cl *)
-(* | Split (lhs, n, indf, results, splits) -> *)
-
-(* let pr_unification_result (ctx, n, c, pat, subst) = *)
-
-(* unification_result array * splitting option array *)
-
-let pr_clauses env =
- prlist_with_sep fnl (pr_clause env)
-
-let lhs_includes (delta, _, patcs : lhs) (delta', _, patcs' : lhs) =
- pattern_includes patcs patcs'
-
-let lhs_matches (delta, _, patcs : lhs) (delta', _, patcs' : lhs) =
- pattern_matches patcs patcs'
-
-let rec split_on env var (delta, f, curpats as lhs) clauses =
- let before, (id, _, ty), after = split_tele (pred var) delta in
- let unify, indf =
- match unify_type before ty with
- | Some r -> r
- | None -> assert false (* We decided... so it better be inductive *)
- in
- let clauses = ref clauses in
- let splits =
- Array.map (fun (ctx', ctxlen, cstr, cstrpat, s) ->
- match s with
- | None -> None
- | Some s ->
- (* ctx' |- s cstr, s cstrpat *)
- let newdelta =
- subst_context s (subst_rel_context 0 cstr
- (lift_contextn ctxlen 1 after)) @ ctx' in
- let liftpats =
- (* delta |- curpats -> before; ctxc; id; after |- liftpats *)
- lift_pats ctxlen (succ var) curpats
- in
- let liftpat = (* before; ctxc |- cstrpat -> before; ctxc; after |- liftpat *)
- lift_pat (pred var) 1 cstrpat
- in
- let substpat = (* before; ctxc; after |- liftpats[id:=liftpat] *)
- subst_pats env var liftpat liftpats
- in
- let lifts = (* before; ctxc |- s : newdelta ->
- before; ctxc; after |- lifts : newdelta ; after *)
- map (fun (k,(b,x)) -> (pred var + k, (b, lift (pred var) x))) s
- in
- let newpats = specialize_patterns lifts substpat in
- let newlhs = (newdelta, f, newpats) in
- let matching, rest =
- fold_right (fun (lhs, rhs as clause) (matching, rest) ->
- if lhs_includes newlhs lhs then
- (clause :: matching, rest)
- else (matching, clause :: rest))
- !clauses ([], [])
- in
- clauses := rest;
- if matching = [] then (
- (* Try finding a splittable variable *)
- let (id, _) =
- fold_right (fun (id, _, ty as decl) (accid, ctx) ->
- match accid with
- | Some _ -> (accid, ctx)
- | None ->
- match unify_type ctx ty with
- | Some (unify, indf) ->
- if array_for_all (fun (_, _, _, _, x) -> x = None) unify then
- (Some id, ctx)
- else (None, decl :: ctx)
- | None -> (None, decl :: ctx))
- newdelta (None, [])
- in
- match id with
- | None ->
- errorlabstrm "deppat"
- (str "Non-exhaustive pattern-matching, no clause found for:" ++ fnl () ++
- pr_lhs env newlhs)
- | Some id ->
- Some (Compute (newlhs, Empty (fst (lookup_rel_id (out_name id) newdelta))))
- ) else (
- let splitting = make_split_aux env newlhs matching in
- Some splitting))
- unify
- in
-(* if !clauses <> [] then *)
-(* errorlabstrm "deppat" *)
-(* (str "Impossible clauses:" ++ fnl () ++ pr_clauses env !clauses); *)
- Split (lhs, var, indf, unify, splits)
-
-and make_split_aux env lhs clauses =
- let split =
- fold_left (fun acc (lhs', rhs) ->
- match acc with
- | None -> find_split lhs lhs'
- | _ -> acc) None clauses
- in
- match split with
- | Some var -> split_on env var lhs clauses
- | None ->
- (match clauses with
- | [] -> error "No clauses left"
- | [(lhs', rhs)] ->
- (* No need to split anymore, fix the environments so that they are correctly aligned. *)
- (match lhs_matches lhs' lhs with
- | Some s ->
- let s = map (fun (x, p) -> x, (true, constr_of_pat ~inacc:false env p)) s in
- let rhs' = match rhs with
- | Program c -> Program (specialize_constr s c)
- | Empty i -> Empty (destRel (snd (assoc i s)))
- in Compute ((pi1 lhs, pi2 lhs, specialize_patterns s (pi3 lhs')), rhs')
- | None -> anomaly "Non-matching clauses at a leaf of the splitting tree")
- | _ ->
- errorlabstrm "make_split_aux"
- (str "Overlapping clauses:" ++ fnl () ++ pr_clauses env clauses))
-
-let make_split env (f, delta, t) clauses =
- make_split_aux env (delta, f, patvars_of_tele delta) clauses
-
-open Evd
-open Evarutil
-
-let lift_substitution n s = map (fun (k, x) -> (k + n, x)) s
-let map_substitution s t = map (subst_rel_subst 0 s) t
-
-let term_of_tree status isevar env (i, delta, ty) ann tree =
-(* let envrec = match ann with *)
-(* | None -> [] *)
-(* | Some (loc, i) -> *)
-(* let (n, t) = lookup_rel_id i delta in *)
-(* let t' = lift n t in *)
-
-
-(* in *)
- let rec aux = function
- | Compute ((ctx, _, pats as lhs), Program rhs) ->
- let ty' = substl (rev (constrs_of_lhs ~inacc:false env lhs)) ty in
- let body = it_mkLambda_or_LetIn rhs ctx and typ = it_mkProd_or_LetIn ty' ctx in
- mkCast(body, DEFAULTcast, typ), typ
-
- | Compute ((ctx, _, pats as lhs), Empty split) ->
- let ty' = substl (rev (constrs_of_lhs ~inacc:false env lhs)) ty in
- let split = (Name (id_of_string "split"),
- Some (Class_tactics.coq_nat_of_int (1 + (length ctx - split))),
- Lazy.force Class_tactics.coq_nat)
- in
- let ty' = it_mkProd_or_LetIn ty' ctx in
- let let_ty' = mkLambda_or_LetIn split (lift 1 ty') in
- let term = e_new_evar isevar env ~src:(dummy_loc, QuestionMark (Define true)) let_ty' in
- term, ty'
-
- | Split ((ctx, _, pats as lhs), rel, indf, unif, sp) ->
- let before, decl, after = split_tele (pred rel) ctx in
- let ty' = substl (rev (constrs_of_lhs ~inacc:false env lhs)) ty in
- let branches =
- array_map2 (fun (ctx', ctxlen, cstr, cstrpat, subst) split ->
- match split with
- | Some s -> aux s
- | None ->
- (* dead code, inversion will find a proof of False by splitting on the rel'th hyp *)
- Class_tactics.coq_nat_of_int rel, Lazy.force Class_tactics.coq_nat)
- unif sp
- in
- let branches_ctx =
- Array.mapi (fun i (br, brt) -> (id_of_string ("m_" ^ string_of_int i), Some br, brt))
- branches
- in
- let n, branches_lets =
- Array.fold_left (fun (n, lets) (id, b, t) ->
- (succ n, (Name id, Option.map (lift n) b, lift n t) :: lets))
- (0, []) branches_ctx
- in
- let liftctx = lift_contextn (Array.length branches) 0 ctx in
- let case =
- let ty = it_mkProd_or_LetIn ty' liftctx in
- let ty = it_mkLambda_or_LetIn ty branches_lets in
- let nbbranches = (Name (id_of_string "branches"),
- Some (Class_tactics.coq_nat_of_int (length branches_lets)),
- Lazy.force Class_tactics.coq_nat)
- in
- let nbdiscr = (Name (id_of_string "target"),
- Some (Class_tactics.coq_nat_of_int (length before)),
- Lazy.force Class_tactics.coq_nat)
- in
- let ty = it_mkLambda_or_LetIn (lift 2 ty) [nbbranches;nbdiscr] in
- let term = e_new_evar isevar env ~src:(dummy_loc, QuestionMark status) ty in
- term
- in
- let casetyp = it_mkProd_or_LetIn ty' ctx in
- mkCast(case, DEFAULTcast, casetyp), casetyp
-
- in aux tree
-
-open Topconstr
-open Constrintern
-open Decl_kinds
-
-type equation = constr_expr * (constr_expr, identifier located) rhs
-
-let locate_reference qid =
- match Nametab.locate_extended qid with
- | TrueGlobal ref -> true
- | SynDef kn -> true
-
-let is_global id =
- try
- locate_reference (qualid_of_ident id)
- with Not_found ->
- false
-
-let is_freevar ids env x =
- try
- if Idset.mem x ids then false
- else
- try ignore(Environ.lookup_named x env) ; false
- with _ -> not (is_global x)
- with _ -> true
-
-let ids_of_patc c ?(bound=Idset.empty) l =
- let found id bdvars l =
- if not (is_freevar bdvars (Global.env ()) (snd id)) then l
- else if List.exists (fun (_, id') -> id' = snd id) l then l
- else id :: l
- in
- let rec aux bdvars l c = match c with
- | CRef (Ident lid) -> found lid bdvars l
- | CNotation (_, "{ _ : _ | _ }", ((CRef (Ident (_, id))) :: _,[])) when not (Idset.mem id bdvars) ->
- fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux (Idset.add id bdvars) l c
- | c -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c
- in aux bound l c
-
-let interp_pats i isevar env impls pat sign recu =
- let bound = Idset.singleton i in
- let vars = ids_of_patc pat ~bound [] in
- let varsctx, env' =
- fold_right (fun (loc, id) (ctx, env) ->
- let decl =
- let ty = e_new_evar isevar env ~src:(loc, BinderType (Name id)) (new_Type ()) in
- (Name id, None, ty)
- in
- decl::ctx, push_rel decl env)
- vars ([], env)
- in
- let pats =
- let patenv = match recu with None -> env' | Some ty -> push_named (i, None, ty) env' in
- let patt, _ = interp_constr_evars_impls ~evdref:isevar patenv ~impls:([],[]) pat in
- match kind_of_term patt with
- | App (m, args) ->
- if not (eq_constr m (mkRel (succ (length varsctx)))) then
- user_err_loc (constr_loc pat, "interp_pats",
- str "Expecting a pattern for " ++ pr_id i)
- else Array.to_list args
- | _ -> user_err_loc (constr_loc pat, "interp_pats",
- str "Error parsing pattern: unnexpected left-hand side")
- in
- isevar := nf_evar_defs !isevar;
- (nf_rel_context_evar ( !isevar) varsctx,
- nf_env_evar ( !isevar) env',
- rev_map (nf_evar ( !isevar)) pats)
-
-let interp_eqn i isevar env impls sign arity recu (pats, rhs) =
- let ctx, env', patcs = interp_pats i isevar env impls pats sign recu in
- let rhs' = match rhs with
- | Program p ->
- let ty = nf_isevar !isevar (substl patcs arity) in
- Program (interp_casted_constr_evars isevar env' ~impls p ty)
- | Empty lid -> Empty (fst (lookup_rel_id (snd lid) ctx))
- in ((ctx, i, pats_of_constrs (rev patcs)), rhs')
-
-open Entries
-
-open Tacmach
-open Tacexpr
-open Tactics
-open Tacticals
-
-let contrib_tactics_path =
- make_dirpath (List.map id_of_string ["Equality";"Program";"Coq"])
-
-let tactics_tac s =
- make_kn (MPfile contrib_tactics_path) (make_dirpath []) (mk_label s)
-
-let equations_tac = lazy
- (Tacinterp.eval_tactic
- (TacArg(TacCall(dummy_loc,
- ArgArg(dummy_loc, tactics_tac "equations"), []))))
-
-let define_by_eqs with_comp i (l,ann) t nt eqs =
- let env = Global.env () in
- let isevar = ref (create_evar_defs Evd.empty) in
- let (env', sign), impls = interp_context_evars isevar env l in
- let arity = interp_type_evars isevar env' t in
- let sign = nf_rel_context_evar ( !isevar) sign in
- let arity = nf_evar ( !isevar) arity in
- let arity =
- if with_comp then
- let compid = add_suffix i "_comp" in
- let ce =
- { const_entry_body = it_mkLambda_or_LetIn arity sign;
- const_entry_type = None;
- const_entry_opaque = false;
- const_entry_boxed = false}
- in
- let c =
- Declare.declare_constant compid (DefinitionEntry ce, IsDefinition Definition)
- in mkApp (mkConst c, rel_vect 0 (length sign))
- else arity
- in
- let env = Global.env () in
- let ty = it_mkProd_or_LetIn arity sign in
- let data = Command.compute_interning_datas env Constrintern.Recursive [] [i] [ty] [impls] in
- let fixdecls = [(Name i, None, ty)] in
- let fixenv = push_rel_context fixdecls env in
- let equations =
- States.with_heavy_rollback (fun () ->
- Option.iter (Command.declare_interning_data data) nt;
- map (interp_eqn i isevar fixenv data sign arity None) eqs) ()
- in
- let sign = nf_rel_context_evar ( !isevar) sign in
- let arity = nf_evar ( !isevar) arity in
- let prob = (i, sign, arity) in
- let fixenv = nf_env_evar ( !isevar) fixenv in
- let fixdecls = nf_rel_context_evar ( !isevar) fixdecls in
- (* let ce = check_evars fixenv Evd.empty !isevar in *)
- (* List.iter (function (_, _, Program rhs) -> ce rhs | _ -> ()) equations; *)
- let is_recursive, env' =
- let occur_eqn ((ctx, _, _), rhs) =
- match rhs with
- | Program c -> dependent (mkRel (succ (length ctx))) c
- | _ -> false
- in if exists occur_eqn equations then true, fixenv else false, env
- in
- let split = make_split env' prob equations in
- (* if valid_tree prob split then *)
- let status = (* if is_recursive then Expand else *) Define false in
- let t, ty = term_of_tree status isevar env' prob ann split in
- let undef = undefined_evars !isevar in
- let t, ty = if is_recursive then
- (it_mkLambda_or_LetIn t fixdecls, it_mkProd_or_LetIn ty fixdecls)
- else t, ty
- in
- let obls, t', ty' =
- Eterm.eterm_obligations env i !isevar ( undef) 0 ~status t ty
- in
- if is_recursive then
- ignore(Subtac_obligations.add_mutual_definitions [(i, t', ty', impls, obls)] []
- ~tactic:(Lazy.force equations_tac)
- (Command.IsFixpoint [None, CStructRec]))
- else
- ignore(Subtac_obligations.add_definition
- ~implicits:impls i t' ty' ~tactic:(Lazy.force equations_tac) obls)
-
-module Gram = Pcoq.Gram
-module Vernac = Pcoq.Vernac_
-module Tactic = Pcoq.Tactic
-
-module DeppatGram =
-struct
- let gec s = Gram.Entry.create ("Deppat."^s)
-
- let deppat_equations : equation list Gram.Entry.e = gec "deppat_equations"
-
- let binders_let2 : (local_binder list * (identifier located option * recursion_order_expr)) Gram.Entry.e = gec "binders_let2"
-
-(* let where_decl : decl_notation Gram.Entry.e = gec "where_decl" *)
-
-end
-
-open Rawterm
-open DeppatGram
-open Util
-open Pcoq
-open Prim
-open Constr
-open G_vernac
-
-GEXTEND Gram
- GLOBAL: (* deppat_gallina_loc *) deppat_equations binders_let2;
-
- deppat_equations:
- [ [ l = LIST1 equation SEP ";" -> l ] ]
- ;
-
- binders_let2:
- [ [ l = binders_let_fixannot -> l ] ]
- ;
-
- equation:
- [ [ c = Constr.lconstr; r=rhs -> (c, r) ] ]
- ;
-
- rhs:
- [ [ ":=!"; id = identref -> Empty id
- |":="; c = Constr.lconstr -> Program c
- ] ]
- ;
-
- END
-
-type 'a deppat_equations_argtype = (equation list, 'a) Genarg.abstract_argument_type
-
-let (wit_deppat_equations : Genarg.tlevel deppat_equations_argtype),
- (globwit_deppat_equations : Genarg.glevel deppat_equations_argtype),
- (rawwit_deppat_equations : Genarg.rlevel deppat_equations_argtype) =
- Genarg.create_arg "deppat_equations"
-
-type 'a binders_let2_argtype = (local_binder list * (identifier located option * recursion_order_expr), 'a) Genarg.abstract_argument_type
-
-let (wit_binders_let2 : Genarg.tlevel binders_let2_argtype),
- (globwit_binders_let2 : Genarg.glevel binders_let2_argtype),
- (rawwit_binders_let2 : Genarg.rlevel binders_let2_argtype) =
- Genarg.create_arg "binders_let2"
-
-type 'a decl_notation_argtype = (Vernacexpr.decl_notation, 'a) Genarg.abstract_argument_type
-
-let (wit_decl_notation : Genarg.tlevel decl_notation_argtype),
- (globwit_decl_notation : Genarg.glevel decl_notation_argtype),
- (rawwit_decl_notation : Genarg.rlevel decl_notation_argtype) =
- Genarg.create_arg "decl_notation"
-
-let equations wc i l t nt eqs =
- try define_by_eqs wc i l t nt eqs
- with e -> msg (Cerrors.explain_exn e)
-
-VERNAC COMMAND EXTEND Define_equations
-| [ "Equations" ident(i) binders_let2(l) ":" lconstr(t) ":=" deppat_equations(eqs)
- decl_notation(nt) ] ->
- [ equations true i l t nt eqs ]
- END
-
-VERNAC COMMAND EXTEND Define_equations2
-| [ "Equations_nocomp" ident(i) binders_let2(l) ":" lconstr(t) ":=" deppat_equations(eqs)
- decl_notation(nt) ] ->
- [ equations false i l t nt eqs ]
-END
-
-let rec int_of_coq_nat c =
- match kind_of_term c with
- | App (f, [| arg |]) -> succ (int_of_coq_nat arg)
- | _ -> 0
-
-let solve_equations_goal destruct_tac tac gl =
- let concl = pf_concl gl in
- let targetn, branchesn, targ, brs, b =
- match kind_of_term concl with
- | LetIn (Name target, targ, _, b) ->
- (match kind_of_term b with
- | LetIn (Name branches, brs, _, b) ->
- target, branches, int_of_coq_nat targ, int_of_coq_nat brs, b
- | _ -> error "Unnexpected goal")
- | _ -> error "Unnexpected goal"
- in
- let branches, b =
- let rec aux n c =
- if n = 0 then [], c
- else match kind_of_term c with
- | LetIn (Name id, br, brt, b) ->
- let rest, b = aux (pred n) b in
- (id, br, brt) :: rest, b
- | _ -> error "Unnexpected goal"
- in aux brs b
- in
- let ids = targetn :: branchesn :: map pi1 branches in
- let cleantac = tclTHEN (intros_using ids) (thin ids) in
- let dotac = tclDO (succ targ) intro in
- let subtacs =
- tclTHENS destruct_tac
- (map (fun (id, br, brt) -> tclTHEN (letin_tac None (Name id) br (Some brt) onConcl) tac) branches)
- in tclTHENLIST [cleantac ; dotac ; subtacs] gl
-
-TACTIC EXTEND solve_equations
- [ "solve_equations" tactic(destruct) tactic(tac) ] -> [ solve_equations_goal (snd destruct) (snd tac) ]
- END
-
-let coq_eq = Lazy.lazy_from_fun Coqlib.build_coq_eq
-let coq_eq_refl = lazy ((Coqlib.build_coq_eq_data ()).Coqlib.refl)
-
-let coq_heq = lazy (Coqlib.coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq")
-let coq_heq_refl = lazy (Coqlib.coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq_refl")
-
-let specialize_hyp id gl =
- let env = pf_env gl in
- let ty = pf_get_hyp_typ gl id in
- let evars = ref (create_evar_defs (project gl)) in
- let rec aux in_eqs acc ty =
- match kind_of_term ty with
- | Prod (_, t, b) ->
- (match kind_of_term t with
- | App (eq, [| eqty; x; y |]) when eq_constr eq (Lazy.force coq_eq) ->
- let pt = mkApp (Lazy.force coq_eq, [| eqty; x; x |]) in
- let p = mkApp (Lazy.force coq_eq_refl, [| eqty; x |]) in
- if e_conv env evars pt t then
- aux true (mkApp (acc, [| p |])) (subst1 p b)
- else error "Unconvertible members of an homogeneous equality"
- | App (heq, [| eqty; x; eqty'; y |]) when eq_constr heq (Lazy.force coq_heq) ->
- let pt = mkApp (Lazy.force coq_heq, [| eqty; x; eqty; x |]) in
- let p = mkApp (Lazy.force coq_heq_refl, [| eqty; x |]) in
- if e_conv env evars pt t then
- aux true (mkApp (acc, [| p |])) (subst1 p b)
- else error "Unconvertible members of an heterogeneous equality"
- | _ ->
- if in_eqs then acc, in_eqs, ty
- else
- let e = e_new_evar evars env t in
- aux false (mkApp (acc, [| e |])) (subst1 e b))
- | t -> acc, in_eqs, ty
- in
- try
- let acc, worked, ty = aux false (mkVar id) ty in
- let ty = Evarutil.nf_isevar !evars ty in
- if worked then
- tclTHENFIRST
- (fun g -> Tacmach.internal_cut true id ty g)
- (exact_no_check (Evarutil.nf_isevar !evars acc)) gl
- else tclFAIL 0 (str "Nothing to do in hypothesis " ++ pr_id id) gl
- with e -> tclFAIL 0 (Cerrors.explain_exn e) gl
-
-TACTIC EXTEND specialize_hyp
-[ "specialize_hypothesis" constr(c) ] -> [
- match kind_of_term c with
- | Var id -> specialize_hyp id
- | _ -> tclFAIL 0 (str "Not an hypothesis") ]
-END
diff --git a/plugins/subtac/eterm.ml b/plugins/subtac/eterm.ml
index 3c947e29cf..d9b73109a2 100644
--- a/plugins/subtac/eterm.ml
+++ b/plugins/subtac/eterm.ml
@@ -1,4 +1,4 @@
-(* -*- compile-command: "make -C ../.. bin/coqtop.byte" -*- *)
+(* -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *)
(**
- Get types of existentials ;
- Flatten dependency tree (prefix order) ;
@@ -30,13 +30,13 @@ type oblinfo =
ev_chop: int option;
ev_loc: Util.loc;
ev_typ: types;
- ev_tac: Tacexpr.raw_tactic_expr option;
+ ev_tac: tactic option;
ev_deps: Intset.t }
(** Substitute evar references in t using De Bruijn indices,
where n binders were passed through. *)
-let subst_evar_constr evs n t =
+let subst_evar_constr evs n idf t =
let seen = ref Intset.empty in
let transparent = ref Idset.empty in
let evar_info id = List.assoc id evs in
@@ -70,7 +70,7 @@ let subst_evar_constr evs n t =
in
if List.exists (fun x -> match kind_of_term x with Rel n -> List.mem n fixrels | _ -> false) args then
transparent := Idset.add idstr !transparent;
- mkApp (mkVar idstr, Array.of_list args)
+ mkApp (idf idstr, Array.of_list args)
| Fix _ ->
map_constr_with_binders succfix substrec (depth, 1 :: fixrels) c
| _ -> map_constr_with_binders succfix substrec (depth, fixrels) c
@@ -96,14 +96,14 @@ let subst_vars acc n t =
let etype_of_evar evs hyps concl =
let rec aux acc n = function
(id, copt, t) :: tl ->
- let t', s, trans = subst_evar_constr evs n t in
+ let t', s, trans = subst_evar_constr evs n mkVar t in
let t'' = subst_vars acc 0 t' in
let rest, s', trans' = aux (id :: acc) (succ n) tl in
let s' = Intset.union s s' in
let trans' = Idset.union trans trans' in
(match copt with
- Some c ->
- let c', s'', trans'' = subst_evar_constr evs n c in
+ Some c ->
+ let c', s'', trans'' = subst_evar_constr evs n mkVar c in
let c' = subst_vars acc 0 c' in
mkNamedProd_or_LetIn (id, Some c', t'') rest,
Intset.union s'' s',
@@ -111,7 +111,7 @@ let etype_of_evar evs hyps concl =
| None ->
mkNamedProd_or_LetIn (id, None, t'') rest, s', trans')
| [] ->
- let t', s, trans = subst_evar_constr evs n concl in
+ let t', s, trans = subst_evar_constr evs n mkVar concl in
subst_vars acc 0 t', s, trans
in aux [] 0 (rev hyps)
@@ -143,13 +143,33 @@ let evar_dependencies evm ev =
in aux (Intset.singleton ev)
let sort_dependencies evl =
- List.sort (fun (_, _, deps) (_, _, deps') ->
- if Intset.subset deps deps' then (* deps' depends on deps *) -1
- else if Intset.subset deps' deps then 1
- else Intset.compare deps deps')
- evl
-
-let eterm_obligations env name isevars evm fs ?status t ty =
+ let one_step deps ine oute =
+ List.fold_left (fun (ine, oute, acc) (id, _, deps' as d) ->
+ if not (Intset.mem id deps) then
+ if Intset.subset deps' (Intset.add id deps) then
+ (d :: ine, oute, Intset.add id acc)
+ else (ine, d :: oute, acc)
+ else (ine, oute, acc))
+ (ine, [], deps) oute
+ in
+ let rec aux deps evsin evsout =
+ let (evsin, evsout, deps') = one_step deps evsin evsout in
+ if evsout = [] then List.rev evsin
+ else aux deps' evsin evsout
+ in aux Intset.empty [] evl
+
+let map_evar_body f = function
+ | Evar_empty -> Evar_empty
+ | Evar_defined c -> Evar_defined (f c)
+
+open Environ
+
+let map_evar_info f evi =
+ { evi with evar_hyps = val_of_named_context (map_named_context f (named_context_of_val evi.evar_hyps));
+ evar_concl = f evi.evar_concl;
+ evar_body = map_evar_body f evi.evar_body }
+
+let eterm_obligations env name isevars evm fs ?status t ty =
(* 'Serialize' the evars *)
let nc = Environ.named_context env in
let nc_len = Sign.named_context_length nc in
@@ -188,7 +208,8 @@ let eterm_obligations env name isevars evm fs ?status t ty =
let tac = match ev.evar_extra with
| Some t ->
if Dyn.tag t = "tactic" then
- Some (Tacinterp.globTacticIn (Tacinterp.tactic_out t))
+ Some (Tacinterp.interp
+ (Tacinterp.globTacticIn (Tacinterp.tactic_out t)))
else None
| None -> None
in
@@ -199,11 +220,11 @@ let eterm_obligations env name isevars evm fs ?status t ty =
evn []
in
let t', _, transparent = (* Substitute evar refs in the term by variables *)
- subst_evar_constr evts 0 t
+ subst_evar_constr evts 0 mkVar t
in
- let ty, _, _ = subst_evar_constr evts 0 ty in
- let evars =
- List.map (fun (_, info) ->
+ let ty, _, _ = subst_evar_constr evts 0 mkVar ty in
+ let evars =
+ List.map (fun (ev, info) ->
let { ev_name = (_, name); ev_status = status;
ev_loc = loc; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info
in
@@ -211,8 +232,9 @@ let eterm_obligations env name isevars evm fs ?status t ty =
| Define true when Idset.mem name transparent -> Define false
| _ -> status
in name, typ, loc, status, deps, tac) evts
- in Array.of_list (List.rev evars), t', ty
+ in
+ let evnames = List.map (fun (ev, info) -> ev, snd info.ev_name) evts in
+ let evmap f c = pi1 (subst_evar_constr evts 0 f c) in
+ Array.of_list (List.rev evars), (evnames, evmap), t', ty
let mkMetas n = list_tabulate (fun _ -> Evarutil.mk_new_meta ()) n
-
-let etermtac (evm, t) = assert(false) (*eterm evm t None *)
diff --git a/plugins/subtac/eterm.mli b/plugins/subtac/eterm.mli
index 1d1c512662..f45dfa1cce 100644
--- a/plugins/subtac/eterm.mli
+++ b/plugins/subtac/eterm.mli
@@ -22,11 +22,13 @@ val sort_dependencies : (int * evar_info * Intset.t) list -> (int * evar_info *
(* env, id, evars, number of function prototypes to try to clear from
evars contexts, object and type *)
-val eterm_obligations : env -> identifier -> evar_defs -> evar_map -> int ->
- ?status:obligation_definition_status -> constr -> types ->
- (identifier * types * loc * obligation_definition_status * Intset.t *
- Tacexpr.raw_tactic_expr option) array * constr * types
- (* Obl. name, type as product, location of the original evar, associated tactic,
+val eterm_obligations : env -> identifier -> evar_defs -> evar_map -> int ->
+ ?status:obligation_definition_status -> constr -> types ->
+ (identifier * types * loc * obligation_definition_status * Intset.t *
+ tactic option) array
+ (* Existential key, obl. name, type as product, location of the original evar, associated tactic,
status and dependencies as indexes into the array *)
-
-val etermtac : open_constr -> tactic
+ * ((existential_key * identifier) list * ((identifier -> constr) -> constr -> constr)) * constr * types
+ (* Translations from existential identifiers to obligation identifiers
+ and for terms with existentials to closed terms, given a
+ translation from obligation identifiers to constrs, new term, new type *)
diff --git a/plugins/subtac/g_eterm.ml4 b/plugins/subtac/g_eterm.ml4
deleted file mode 100644
index 53ce5b8d64..0000000000
--- a/plugins/subtac/g_eterm.ml4
+++ /dev/null
@@ -1,27 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-(**************************************************************************)
-(* *)
-(* Omega: a solver of quantifier-free problems in Presburger Arithmetic *)
-(* *)
-(* Pierre Crégut (CNET, Lannion, France) *)
-(* *)
-(**************************************************************************)
-
-(*i camlp4deps: "parsing/grammar.cma" i*)
-
-(* $Id$ *)
-
-open Eterm
-
-TACTIC EXTEND eterm
- [ "eterm" ] -> [
- (fun gl ->
- let evm = Tacmach.project gl and t = Tacmach.pf_concl gl in
- Eterm.etermtac (evm, t) gl) ]
-END
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 97a9298092..85b55f36c4 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -51,9 +51,9 @@ open Tacexpr
let solve_tccs_in_type env id isevars evm c typ =
if not (evm = Evd.empty) then
let stmt_id = Nameops.add_suffix id "_stmt" in
- let obls, c', t' = eterm_obligations env stmt_id !isevars evm 0 ~status:Expand c typ in
- match Subtac_obligations.add_definition stmt_id c' typ obls with
- | Subtac_obligations.Defined cst -> constant_value (Global.env())
+ let obls, _, c', t' = eterm_obligations env stmt_id !isevars evm 0 ~status:Expand c typ in
+ match Subtac_obligations.add_definition stmt_id ~term:c' typ obls with
+ | Subtac_obligations.Defined cst -> constant_value (Global.env())
(match cst with ConstRef kn -> kn | _ -> assert false)
| _ ->
errorlabstrm "start_proof"
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index 93b65cd000..211d71a881 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -184,11 +184,10 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
Evarutil.check_evars env Evd.empty !isevars termtype;
let hook vis gr =
let cst = match gr with ConstRef kn -> kn | _ -> assert false in
- let inst = Typeclasses.new_instance k pri global cst in
+ let inst = Typeclasses.new_instance k pri global (ConstRef cst) in
Impargs.declare_manual_implicits false gr ~enriching:false imps;
Typeclasses.add_instance inst
in
- let evm = Subtac_utils.evars_of_term ( !isevars) Evd.empty term in
- let obls, constr, typ = Eterm.eterm_obligations env id !isevars evm 0 term termtype in
- id, Subtac_obligations.add_definition id constr typ ~kind:(Global,false,Instance) ~hook obls
-
+ let evm = Subtac_utils.evars_of_term !isevars Evd.empty term in
+ let obls, _, constr, typ = Eterm.eterm_obligations env id !isevars evm 0 term termtype in
+ id, Subtac_obligations.add_definition id ~term:constr typ ~kind:(Global,false,Instance) ~hook obls
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index 937f7d0650..2a31d4e18d 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -234,11 +234,6 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
let argtyp, letbinders, make = telescope binders_rel in
let argname = id_of_string "recarg" in
let arg = (Name argname, None, argtyp) in
- let wrapper x =
- if List.length binders_rel > 1 then
- it_mkLambda_or_LetIn (mkApp (x, [|make|])) binders_rel
- else x
- in
let binders = letbinders @ [arg] in
let binders_env = push_rel_context binders_rel env in
let rel = interp_constr isevars env r in
@@ -310,22 +305,46 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
in
let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in
let prop = mkLambda (Name argname, argtyp, top_arity_let) in
- let fix_def =
+ let def =
mkApp (constr_of_global (Lazy.force fix_sub_ref),
[| argtyp ; wf_rel ;
make_existential dummy_loc ~opaque:(Define false) env isevars wf_proof ;
prop ; intern_body_lam |])
in
- let def = wrapper fix_def in
- let typ = it_mkProd_or_LetIn top_arity binders_rel in
+ let hook, recname, typ =
+ if List.length binders_rel > 1 then
+ let name = add_suffix recname "_func" in
+ let hook l gr =
+ let body = it_mkLambda_or_LetIn (mkApp (constr_of_global gr, [|make|])) binders_rel in
+ let ty = it_mkProd_or_LetIn top_arity binders_rel in
+ let ce =
+ { const_entry_body = body;
+ const_entry_type = Some ty;
+ const_entry_opaque = false;
+ const_entry_boxed = false}
+ in
+ let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
+ let gr = ConstRef c in
+ if Impargs.is_implicit_args () || impls <> [] then
+ Impargs.declare_manual_implicits false gr impls
+ in
+ let typ = it_mkProd_or_LetIn top_arity binders in
+ hook, name, typ
+ else
+ let typ = it_mkProd_or_LetIn top_arity binders_rel in
+ let hook l gr =
+ if Impargs.is_implicit_args () || impls <> [] then
+ Impargs.declare_manual_implicits false gr impls
+ in hook, recname, typ
+ in
let _ = isevars := Evarutil.nf_evar_defs !isevars in
let fullcoqc = Evarutil.nf_isevar !isevars def in
let fullctyp = Evarutil.nf_isevar !isevars typ in
let evm = evars_of_term !isevars Evd.empty fullctyp in
let evm = evars_of_term !isevars evm fullcoqc in
let evm = non_instanciated_map env isevars evm in
- let evars, evars_def, evars_typ = Eterm.eterm_obligations env recname !isevars evm 0 fullcoqc fullctyp in
- Subtac_obligations.add_definition recname evars_def evars_typ ~implicits:impls evars
+ let evars, _, evars_def, evars_typ = Eterm.eterm_obligations env recname !isevars evm 0 fullcoqc fullctyp in
+ Subtac_obligations.add_definition recname ~term:evars_def evars_typ evars ~hook
let nf_evar_context isevars ctx =
List.map (fun (n, b, t) ->
@@ -454,7 +473,7 @@ let interp_recursive fixkind l boxed =
in
let evm' = Subtac_utils.evars_of_term evm Evd.empty def in
let evm' = Subtac_utils.evars_of_term evm evm' typ in
- let evars, def, typ = Eterm.eterm_obligations env id isevars evm' recdefs def typ in
+ let evars, _, def, typ = Eterm.eterm_obligations env id isevars evm' recdefs def typ in
(id, def, typ, imps, evars)
in
let defs = list_map4 collect_evars fixnames fixdefs fixtypes fiximps in
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index f617c1008d..9b0b39cf82 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -21,6 +21,9 @@ let ppwarn cmd = Pp.warn (str"Program:" ++ cmd)
let pperror cmd = Util.errorlabstrm "Program" cmd
let error s = pperror (str s)
+let reduce =
+ Reductionops.clos_norm_flags Closure.betaiotazeta (Global.env ()) Evd.empty
+
exception NoObligations of identifier option
let explain_no_obligations = function
@@ -28,17 +31,17 @@ let explain_no_obligations = function
| None -> str "No obligations remaining"
type obligation_info = (Names.identifier * Term.types * loc * obligation_definition_status * Intset.t
- * Tacexpr.raw_tactic_expr option) array
+ * tactic option) array
type obligation =
- { obl_name : identifier;
- obl_type : types;
- obl_location : loc;
- obl_body : constr option;
- obl_status : obligation_definition_status;
- obl_deps : Intset.t;
- obl_tac : Tacexpr.raw_tactic_expr option;
- }
+ { obl_name : identifier;
+ obl_type : types;
+ obl_location : loc;
+ obl_body : constr option;
+ obl_status : obligation_definition_status;
+ obl_deps : Intset.t;
+ obl_tac : tactic option;
+ }
type obligations = (obligation array * int)
@@ -105,7 +108,7 @@ let subst_deps expand obls deps t =
Term.replace_vars subst t
let subst_deps_obl obls obl =
- let t' = subst_deps false obls obl.obl_deps obl.obl_type in
+ let t' = subst_deps true obls obl.obl_deps obl.obl_type in
{ obl with obl_type = t' }
module ProgMap = Map.Make(struct type t = identifier let compare = compare end)
@@ -148,15 +151,14 @@ let _ =
let progmap_union = ProgMap.fold ProgMap.add
-let cache (_, (infos, tac)) =
- from_prg := infos;
+let cache (_, tac) =
set_default_tactic tac
-let load (_, (_, tac)) =
+let load (_, tac) =
set_default_tactic tac
-let subst (s, (infos, tac)) =
- (infos, Tacinterp.subst_tactic s tac)
+let subst (s, tac) =
+ Tacinterp.subst_tactic s tac
let (input,output) =
declare_object
@@ -164,17 +166,16 @@ let (input,output) =
cache_function = cache;
load_function = (fun _ -> load);
open_function = (fun _ -> load);
- classify_function = (fun (infos, tac) ->
- if not (ProgMap.is_empty infos) then
+ classify_function = (fun tac ->
+ if not (ProgMap.is_empty !from_prg) then
errorlabstrm "Program" (str "Unsolved obligations when closing module:" ++ spc () ++
prlist_with_sep spc (fun x -> Nameops.pr_id x)
- (map_keys infos));
- Substitute (ProgMap.empty, tac));
+ (map_keys !from_prg));
+ Substitute tac);
subst_function = subst}
let update_state () =
-(* msgnl (str "Updating obligations info"); *)
- Lib.add_anonymous_leaf (input (!from_prg, !default_tactic_expr))
+ Lib.add_anonymous_leaf (input !default_tactic_expr)
let set_default_tactic t =
set_default_tactic t; update_state ()
@@ -195,7 +196,7 @@ let subst_body expand prg =
subst_deps expand obls ints (Termops.refresh_universes prg.prg_type)
let declare_definition prg =
- let body, typ = subst_body false prg in
+ let body, typ = subst_body true prg in
(try trace (str "Declaring: " ++ Ppconstr.pr_id prg.prg_name ++ spc () ++
my_print_constr (Global.env()) body ++ str " : " ++
my_print_constr (Global.env()) prg.prg_type);
@@ -229,8 +230,8 @@ let declare_definition prg =
if Impargs.is_implicit_args () || prg.prg_implicits <> [] then
Impargs.declare_manual_implicits false gr prg.prg_implicits;
print_message (Subtac_utils.definition_message prg.prg_name);
- prg.prg_hook local gr;
progmap_remove prg; update_state ();
+ prg.prg_hook local gr;
gr
open Pp
@@ -256,17 +257,16 @@ let compute_possible_guardness_evidences (n,_) fixbody fixtype =
let ctx = fst (decompose_prod_n_assum m fixtype) in
list_map_i (fun i _ -> i) 0 ctx
-let reduce_fix =
- Reductionops.clos_norm_flags Closure.betaiotazeta (Global.env ()) Evd.empty
-
let declare_mutual_definition l =
let len = List.length l in
let first = List.hd l in
let fixdefs, fixtypes, fiximps =
list_split3
- (List.map (fun x ->
- let subs, typ = (subst_body false x) in
- (strip_lam_n len subs), snd (decompose_prod_n len typ), x.prg_implicits) l)
+ (List.map (fun x ->
+ let subs, typ = (subst_body true x) in
+ let term = snd (Reductionops.splay_lam_n (Global.env ()) Evd.empty len subs) in
+ let typ = snd (Reductionops.splay_prod_n (Global.env ()) Evd.empty len typ) in
+ reduce term, reduce typ, x.prg_implicits) l)
in
(* let fixdefs = List.map reduce_fix fixdefs in *)
let fixkind = Option.get first.prg_fixkind in
@@ -295,36 +295,48 @@ let declare_mutual_definition l =
first.prg_hook local gr;
List.iter progmap_remove l;
update_state (); kn
-
-let declare_obligation obl body =
+
+let declare_obligation prg obl body =
+ let body = reduce body in
+ let ty = reduce obl.obl_type in
match obl.obl_status with
| Expand -> { obl with obl_body = Some body }
| Define opaque ->
- let ce =
+ let opaque = if get_proofs_transparency () then false else opaque in
+ let ce =
{ const_entry_body = body;
- const_entry_type = Some obl.obl_type;
- const_entry_opaque =
- (if get_proofs_transparency () then false
- else opaque) ;
- const_entry_boxed = false}
+ const_entry_type = Some ty;
+ const_entry_opaque = opaque;
+ const_entry_boxed = false}
in
let constant = Declare.declare_constant obl.obl_name
(DefinitionEntry ce,IsProof Property)
in
+ if not opaque then
+ Auto.add_hints false [string_of_id prg.prg_name]
+ (Auto.HintsUnfoldEntry [EvalConstRef constant]);
print_message (Subtac_utils.definition_message obl.obl_name);
{ obl with obl_body = Some (mkConst constant) }
let red = Reductionops.nf_betaiota Evd.empty
let init_prog_info n b t deps fixkind notations obls impls kind hook =
- let obls' =
- Array.mapi
- (fun i (n, t, l, o, d, tac) ->
- debug 2 (str "Adding obligation " ++ int i ++ str " with deps : " ++ str (string_of_intset d));
- { obl_name = n ; obl_body = None;
- obl_location = l; obl_type = red t; obl_status = o;
- obl_deps = d; obl_tac = tac })
- obls
+ let obls', b =
+ match b with
+ | None ->
+ assert(obls = [||]);
+ let n = Nameops.add_suffix n "_obligation" in
+ [| { obl_name = n; obl_body = None;
+ obl_location = dummy_loc; obl_type = t;
+ obl_status = Expand; obl_deps = Intset.empty; obl_tac = None } |],
+ mkVar n
+ | Some b ->
+ Array.mapi
+ (fun i (n, t, l, o, d, tac) ->
+ { obl_name = n ; obl_body = None;
+ obl_location = l; obl_type = red t; obl_status = o;
+ obl_deps = d; obl_tac = tac })
+ obls, b
in
{ prg_name = n ; prg_body = b; prg_type = red t; prg_obligations = (obls', Array.length obls');
prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ;
@@ -348,6 +360,9 @@ let get_prog_err n =
let obligations_solved prg = (snd prg.prg_obligations) = 0
+let all_programs () =
+ ProgMap.fold (fun k p l -> p :: l) !from_prg []
+
type progress =
| Remain of int
| Dependent
@@ -364,13 +379,14 @@ let obligations_message rem =
let update_obls prg obls rem =
let prg' = { prg with prg_obligations = (obls, rem) } in
- from_prg := map_replace prg.prg_name prg' !from_prg;
+ from_prg := map_replace prg.prg_name prg' !from_prg; update_state ();
obligations_message rem;
if rem > 0 then Remain rem
else (
match prg'.prg_deps with
| [] ->
let kn = declare_definition prg' in
+ progmap_remove prg';
Defined kn
| l ->
let progs = List.map (fun x -> ProgMap.find x !from_prg) prg'.prg_deps in
@@ -432,7 +448,11 @@ let rec solve_obligation prg num =
| Define opaque ->
if not opaque && not transparent then error_not_transp ()
else Libnames.constr_of_global gr
- in { obl with obl_body = Some body }
+ in
+ if transparent then
+ Auto.add_hints true [string_of_id prg.prg_name]
+ (Auto.HintsUnfoldEntry [EvalConstRef cst]);
+ { obl with obl_body = Some body }
in
let obls = Array.copy obls in
let _ = obls.(num) <- obl in
@@ -476,11 +496,11 @@ and solve_obligation_by_tac prg obls i tac =
| Some t -> t
| None ->
match obl.obl_tac with
- | Some t -> Tacinterp.interp t
+ | Some t -> t
| None -> !default_tactic
in
let t = Subtac_utils.solve_by_tac (evar_of_obligation obl) tac in
- obls.(i) <- declare_obligation obl t;
+ obls.(i) <- declare_obligation prg obl t;
true
else false
with
@@ -524,8 +544,7 @@ and auto_solve_obligations n tac : progress =
try solve_prg_obligations (get_prog_err n) tac with NoObligations _ -> Dependent
open Pp
-let show_obligations ?(msg=true) n =
- let prg = get_prog_err n in
+let show_obligations_of_prg ?(msg=true) prg =
let n = prg.prg_name in
let obls, rem = prg.prg_obligations in
let showed = ref 5 in
@@ -541,6 +560,14 @@ let show_obligations ?(msg=true) n =
| Some _ -> ())
obls
+let show_obligations ?(msg=true) n =
+ let progs = match n with
+ | None -> all_programs ()
+ | Some n ->
+ try [ProgMap.find n !from_prg]
+ with Not_found -> raise (NoObligations (Some n))
+ in List.iter (show_obligations_of_prg ~msg) progs
+
let show_term n =
let prg = get_prog_err n in
let n = prg.prg_name in
@@ -548,14 +575,13 @@ let show_term n =
my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
++ my_print_constr (Global.env ()) prg.prg_body)
-let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic ?(hook=fun _ _ -> ()) obls =
+let add_definition n ?term t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic ?(hook=fun _ _ -> ()) obls =
Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
- let prg = init_prog_info n b t [] None [] obls implicits kind hook in
+ let prg = init_prog_info n term t [] None [] obls implicits kind hook in
let obls,_ = prg.prg_obligations in
if Array.length obls = 0 then (
Flags.if_verbose ppnl (str ".");
let cst = declare_definition prg in
- from_prg := ProgMap.remove prg.prg_name !from_prg;
Defined cst)
else (
let len = Array.length obls in
@@ -570,7 +596,7 @@ let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) ?(hook=fun
let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
let upd = List.fold_left
(fun acc (n, b, t, imps, obls) ->
- let prg = init_prog_info n b t deps (Some fixkind) notations obls imps kind hook in
+ let prg = init_prog_info n (Some b) t deps (Some fixkind) notations obls imps kind hook in
ProgMap.add n prg acc)
!from_prg l
in
@@ -589,14 +615,17 @@ let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) ?(hook=fun
let admit_obligations n =
let prg = get_prog_err n in
let obls, rem = prg.prg_obligations in
- Array.iteri (fun i x ->
- match x.obl_body with
- None ->
- let x = subst_deps_obl obls x in
- let kn = Declare.declare_constant x.obl_name (ParameterEntry (x.obl_type,false), IsAssumption Conjectural) in
- assumption_message x.obl_name;
- obls.(i) <- { x with obl_body = Some (mkConst kn) }
- | Some _ -> ())
+ Array.iteri
+ (fun i x ->
+ match x.obl_body with
+ | None ->
+ let x = subst_deps_obl obls x in
+ let kn = Declare.declare_constant x.obl_name (ParameterEntry (x.obl_type,false),
+ IsAssumption Conjectural)
+ in
+ assumption_message x.obl_name;
+ obls.(i) <- { x with obl_body = Some (mkConst kn) }
+ | Some _ -> ())
obls;
ignore(update_obls prg obls 0)
diff --git a/plugins/subtac/subtac_obligations.mli b/plugins/subtac/subtac_obligations.mli
index 80d5b9465c..04e2371af7 100644
--- a/plugins/subtac/subtac_obligations.mli
+++ b/plugins/subtac/subtac_obligations.mli
@@ -6,26 +6,26 @@ open Proof_type
type obligation_info =
(identifier * Term.types * loc *
- obligation_definition_status * Intset.t * Tacexpr.raw_tactic_expr option) array
+ obligation_definition_status * Intset.t * tactic option) array
(* ident, type, location, (opaque or transparent, expand or define),
dependencies, tactic to solve it *)
type progress = (* Resolution status of a program *)
- | Remain of int (* n obligations remaining *)
- | Dependent (* Dependent on other definitions *)
- | Defined of global_reference (* Defined as id *)
-
+ | Remain of int (* n obligations remaining *)
+ | Dependent (* Dependent on other definitions *)
+ | Defined of global_reference (* Defined as id *)
+
val set_default_tactic : Tacexpr.glob_tactic_expr -> unit
val default_tactic : unit -> Proof_type.tactic
val set_proofs_transparency : bool -> unit (* true = All transparent, false = Opaque if possible *)
val get_proofs_transparency : unit -> bool
-val add_definition : Names.identifier -> Term.constr -> Term.types ->
+val add_definition : Names.identifier -> ?term:Term.constr -> Term.types ->
?implicits:(Topconstr.explicitation * (bool * bool * bool)) list ->
?kind:Decl_kinds.definition_kind ->
?tactic:Proof_type.tactic ->
- ?hook:Tacexpr.declaration_hook -> obligation_info -> progress
+ ?hook:(Tacexpr.declaration_hook) -> obligation_info -> progress
type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list
diff --git a/plugins/subtac/subtac_plugin.mllib b/plugins/subtac/subtac_plugin.mllib
index 394a4b30fc..a4b9d67e01 100644
--- a/plugins/subtac/subtac_plugin.mllib
+++ b/plugins/subtac/subtac_plugin.mllib
@@ -1,6 +1,5 @@
Subtac_utils
Eterm
-G_eterm
Subtac_errors
Subtac_coercion
Subtac_obligations
@@ -11,5 +10,4 @@ Subtac_command
Subtac_classes
Subtac
G_subtac
-Equations
Subtac_plugin_mod
diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml
index 8457105407..11a9fa9f53 100644
--- a/plugins/subtac/subtac_pretyping.ml
+++ b/plugins/subtac/subtac_pretyping.ml
@@ -133,5 +133,5 @@ let subtac_proof kind hook env isevars id bl c tycon =
let evm, coqc, coqt, imps = subtac_process env isevars id bl c tycon in
let evm' = Subtac_utils.evars_of_term evm Evd.empty coqc in
let evm' = Subtac_utils.evars_of_term evm evm' coqt in
- let evars, def, ty = Eterm.eterm_obligations env id !isevars evm' 0 coqc coqt in
- add_definition id def ty ~implicits:imps ~kind ~hook evars
+ let evars, _, def, ty = Eterm.eterm_obligations env id !isevars evm' 0 coqc coqt in
+ add_definition id ~term:def ty ~implicits:imps ~kind ~hook evars
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index 288d3854fd..fbe40525bd 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -50,6 +50,10 @@ let build_sig () =
let sig_ = lazy (build_sig ())
let fix_proto = lazy (init_constant tactics_module "fix_proto")
+let fix_proto_ref () =
+ match Nametab.global (make_ref "Program.Tactics.fix_proto") with
+ | ConstRef c -> c
+ | _ -> assert false
let eq_ind = lazy (init_constant ["Init"; "Logic"] "eq")
let eq_rec = lazy (init_constant ["Init"; "Logic"] "eq_rec")
@@ -374,7 +378,10 @@ let solve_by_tac evi t =
(fun _ _ -> ());
Pfedit.by (tclCOMPLETE t);
let _,(const,_,_,_) = Pfedit.cook_proof ignore in
- Pfedit.delete_current_proof (); const.Entries.const_entry_body
+ Pfedit.delete_current_proof ();
+ Inductiveops.control_only_guard (Global.env ())
+ const.Entries.const_entry_body;
+ const.Entries.const_entry_body
with e ->
Pfedit.delete_current_proof();
raise e
diff --git a/plugins/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli
index e7ee6c7483..81f263cc2b 100644
--- a/plugins/subtac/subtac_utils.mli
+++ b/plugins/subtac/subtac_utils.mli
@@ -35,6 +35,7 @@ val build_sig : unit -> coq_sigma_data
val sig_ : coq_sigma_data lazy_t
val fix_proto : constr lazy_t
+val fix_proto_ref : unit -> constant
val eq_ind : constr lazy_t
val eq_rec : constr lazy_t
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:04:25 +0000