summaryrefslogtreecommitdiff
path: root/contrib/subtac
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/subtac')
-rw-r--r--contrib/subtac/Utils.v3
-rw-r--r--contrib/subtac/eterm.ml148
-rw-r--r--contrib/subtac/eterm.mli8
-rw-r--r--contrib/subtac/g_subtac.ml430
-rw-r--r--contrib/subtac/subtac.ml54
-rw-r--r--contrib/subtac/subtac_coercion.ml7
-rw-r--r--contrib/subtac/subtac_command.ml107
-rw-r--r--contrib/subtac/subtac_command.mli1
-rw-r--r--contrib/subtac/subtac_obligations.ml249
-rw-r--r--contrib/subtac/subtac_obligations.mli10
-rw-r--r--contrib/subtac/subtac_pretyping.ml12
-rw-r--r--contrib/subtac/subtac_pretyping.mli3
-rw-r--r--contrib/subtac/subtac_pretyping_F.ml45
-rw-r--r--contrib/subtac/subtac_utils.ml72
-rw-r--r--contrib/subtac/subtac_utils.mli10
-rw-r--r--contrib/subtac/test/ListDep.v86
16 files changed, 612 insertions, 233 deletions
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
index b1694d7c..219cd75b 100644
--- a/contrib/subtac/Utils.v
+++ b/contrib/subtac/Utils.v
@@ -4,7 +4,7 @@ Notation "'fun' { x : A | P } => Q" :=
(fun x:{x:A|P} => Q)
(at level 200, x ident, right associativity).
-Notation "( x & y )" := (@existS _ _ x y) : core_scope.
+Notation "( x & ? )" := (@exist _ _ x _) : core_scope.
Definition ex_pi1 (A : Prop) (P : A -> Prop) (t : ex P) : A.
intros.
@@ -44,3 +44,4 @@ end.
Ltac destruct_exists := repeat (destruct_one_pair) .
+Extraction Inline proj1_sig.
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index 859f9013..790e61a0 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -32,47 +32,48 @@ let list_assoc_index x l =
| [] -> raise Not_found
in aux 0 l
+
(** Substitute evar references in t using De Bruijn indices,
where n binders were passed through. *)
-let subst_evars evs n t =
+let subst_evar_constr evs n t =
+ let seen = ref Intset.empty in
let evar_info id =
let rec aux i = function
- (k, h, v) :: tl ->
- trace (str "Searching for " ++ int id ++ str " found: " ++ int k);
- if k = id then (i, h, v) else aux (succ i) tl
+ (k, x) :: tl ->
+ if k = id then x else aux (succ i) tl
| [] -> raise Not_found
- in
- let (idx, hyps, v) = aux 0 evs in
- n + idx + 1, hyps
+ in aux 0 evs
in
let rec substrec depth c = match kind_of_term c with
| Evar (k, args) ->
- (let index, hyps =
- try evar_info k
- with Not_found ->
- anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found")
- in
- (try trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++
- int (List.length hyps) ++ str " hypotheses"); with _ -> () );
- let ex = mkRel (index + depth) in
- (* Evar arguments are created in inverse order,
- and we must not apply to defined ones (i.e. LetIn's)
- *)
- let args =
- let rec aux hyps args acc =
+ let (id, idstr), hyps, _, _ =
+ try evar_info k
+ with Not_found ->
+ anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found")
+ in
+ seen := Intset.add id !seen;
+ (try trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++
+ int (List.length hyps) ++ str " hypotheses"); with _ -> () );
+ (* Evar arguments are created in inverse order,
+ and we must not apply to defined ones (i.e. LetIn's)
+ *)
+ let args =
+ let rec aux hyps args acc =
match hyps, args with
((_, None, _) :: tlh), (c :: tla) ->
aux tlh tla ((map_constr_with_binders succ substrec depth c) :: acc)
| ((_, Some _, _) :: tlh), (_ :: tla) ->
aux tlh tla acc
| [], [] -> acc
- | _, _ -> failwith "subst_evars: invalid argument"
+ | _, _ -> acc (*failwith "subst_evars: invalid argument"*)
in aux hyps (Array.to_list args) []
in
- mkApp (ex, Array.of_list args))
+ mkApp (mkVar idstr, Array.of_list args)
| _ -> map_constr_with_binders succ substrec depth c
in
- substrec 0 t
+ let t' = substrec 0 t in
+ t', !seen
+
(** Substitute variable references in t using De Bruijn indices,
where n binders were passed through. *)
@@ -89,73 +90,80 @@ let subst_vars acc n t =
(** Rewrite type of an evar ([ H1 : t1, ... Hn : tn |- concl ])
to a product : forall H1 : t1, ..., forall Hn : tn, concl.
- Changes evars and hypothesis references to De Bruijn indices.
+ Changes evars and hypothesis references to variable references.
*)
let etype_of_evar evs ev hyps =
let rec aux acc n = function
(id, copt, t) :: tl ->
- let t' = subst_evars evs n t in
+ let t', s = subst_evar_constr evs n t in
let t'' = subst_vars acc 0 t' in
- mkNamedProd_or_LetIn (id, copt, t'') (aux (id :: acc) (succ n) tl)
+ let copt', s =
+ match copt with
+ Some c ->
+ let c', s' = subst_evar_constr evs n c in
+ Some c', Intset.union s s'
+ | None -> None, s
+ in
+ let copt' = option_map (subst_vars acc 0) copt' in
+ let rest, s' = aux (id :: acc) (succ n) tl in
+ mkNamedProd_or_LetIn (id, copt', t'') rest, Intset.union s' s
| [] ->
- let t' = subst_evars evs n ev.evar_concl in
- subst_vars acc 0 t'
+ let t', s = subst_evar_constr evs n ev.evar_concl in
+ subst_vars acc 0 t', s
in aux [] 0 (rev hyps)
open Tacticals
-let eterm_term evm t tycon =
+let rec take n l =
+ if n = 0 then [] else List.hd l :: take (pred n) (List.tl l)
+
+let trunc_named_context n ctx =
+ let len = List.length ctx in
+ take (len - n) ctx
+
+let eterm_obligations name nclen evm t tycon =
(* 'Serialize' the evars, we assume that the types of the existentials
refer to previous existentials in the list only *)
let evl = List.rev (to_list evm) in
- trace (str "Eterm, transformed to list");
+ trace (str "Eterm, transformed to list");
+ let evn =
+ let i = ref (-1) in
+ List.rev_map (fun (id, ev) -> incr i;
+ (id, (!i, id_of_string (string_of_id name ^ "_obligation_" ^ string_of_int (succ !i))), ev)) evl
+ in
let evts =
(* Remove existential variables in types and build the corresponding products *)
fold_right
- (fun (id, ev) l ->
+ (fun (id, (n, nstr), ev) l ->
trace (str "Eterm: " ++ str "treating evar: " ++ int id);
let hyps = Environ.named_context_of_val ev.evar_hyps in
- let y' = (id, hyps, etype_of_evar l ev hyps) in
+ let hyps = trunc_named_context nclen hyps in
+ trace (str "Named context is: " ++ Printer.pr_named_context (Global.env ()) hyps);
+ let evtyp, deps = etype_of_evar l ev hyps in
+ trace (str "Evar " ++ str (string_of_int n) ++ str "'s type is: " ++ Termops.print_constr_env (Global.env ()) evtyp);
+ let y' = (id, ((n, nstr), hyps, evtyp, deps)) in
y' :: l)
- evl []
+ evn []
in
- let t' = (* Substitute evar refs in the term by De Bruijn indices *)
- subst_evars evts 0 t
- in
- let evar_names =
- List.map (fun (id, _, c) -> (id_of_string ("Evar" ^ string_of_int id)), c) evts
- in
- let evar_bl =
- List.map (fun (id, c) -> Name id, None, c) evar_names
- in
- let anon_evar_bl = List.map (fun (_, x, y) -> (Anonymous, x, y)) evar_bl in
- (* Generalize over the existential variables *)
- let t'' = Termops.it_mkLambda_or_LetIn t' evar_bl
- and tycon = option_map
- (fun typ -> Termops.it_mkProd_wo_LetIn typ anon_evar_bl) tycon
- in
- let _declare_evar (id, c) =
- let id = id_of_string ("Evar" ^ string_of_int id) in
- ignore(Declare.declare_variable id (Names.empty_dirpath, Declare.SectionLocalAssum c,
- Decl_kinds.IsAssumption Decl_kinds.Definitional))
+ let t', _ = (* Substitute evar refs in the term by variables *)
+ subst_evar_constr evts 0 t
in
- let _declare_assert acc (id, c) =
- let id = id_of_string ("Evar" ^ string_of_int id) in
- tclTHEN acc (Tactics.assert_tac false (Name id) c)
+ let evars =
+ List.map (fun (_, ((_, name), _, typ, deps)) -> name, typ, deps) evts
in
(try
trace (str "Term given to eterm" ++ spc () ++
- Termops.print_constr_env (Global.env ()) t);
+ Termops.print_constr_env (Global.env ()) t);
trace (str "Term constructed in eterm" ++ spc () ++
- Termops.print_constr_env (Global.env ()) t'');
- ignore(option_map
- (fun typ ->
- trace (str "Type :" ++ spc () ++
- Termops.print_constr_env (Global.env ()) typ))
- tycon);
+ 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 _ -> ());
- t'', tycon, evar_names
+ Array.of_list (List.rev evars), t'
let mkMetas n =
let rec aux i acc =
@@ -163,12 +171,12 @@ let mkMetas n =
else acc
in aux 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))
+(* 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
+(* open Tacmach *)
-let etermtac (evm, t) = eterm evm t None
+let etermtac (evm, t) = assert(false) (*eterm evm t None *)
diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli
index fbe2ac1d..3a571ee1 100644
--- a/contrib/subtac/eterm.mli
+++ b/contrib/subtac/eterm.mli
@@ -6,15 +6,19 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: eterm.mli 8688 2006-04-07 15:08:12Z msozeau $ i*)
+(*i $Id: eterm.mli 9326 2006-10-31 12:57:26Z msozeau $ i*)
open Tacmach
open Term
open Evd
open Names
+open Util
val mkMetas : int -> constr list
-val eterm_term : evar_map -> constr -> types option -> constr * types option * (identifier * types) list
+(* val eterm_term : evar_map -> constr -> types option -> constr * types option * (identifier * types) list *)
+
+val eterm_obligations : identifier -> int -> evar_map -> constr -> types option ->
+ (identifier * types * Intset.t) array * constr (* Obl. name, type as product 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 b56ecc3d..243cb191 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -10,7 +10,7 @@
Syntax for the subtac terms and types.
Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliātre *)
-(* $Id: g_subtac.ml4 8917 2006-06-07 16:59:05Z herbelin $ *)
+(* $Id: g_subtac.ml4 9326 2006-10-31 12:57:26Z msozeau $ *)
(*i camlp4deps: "parsing/grammar.cma" i*)
@@ -30,6 +30,7 @@ open Topconstr
module Gram = Pcoq.Gram
module Vernac = Pcoq.Vernac_
+module Tactic = Pcoq.Tactic
module SubtacGram =
struct
@@ -40,15 +41,31 @@ end
open SubtacGram
open Util
+open Pcoq
+
+let sigref = mkRefC (Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Init.Specif.sig"))
GEXTEND Gram
- GLOBAL: subtac_gallina_loc;
+ GLOBAL: subtac_gallina_loc Constr.binder_let Constr.binder;
subtac_gallina_loc:
[ [ g = Vernac.gallina -> loc, g ] ]
;
+
+ Constr.binder_let:
+ [ [ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" ->
+ let typ = mkAppC (sigref, [mkLambdaC ([id], t, c)]) in
+ LocalRawAssum ([id], typ)
+ ] ];
+
+ Constr.binder:
+ [ [ "("; id=Prim.name; ":"; c=Constr.lconstr; "|"; p=Constr.lconstr; ")" ->
+ let typ = mkAppC (sigref, [mkLambdaC ([id], c, p)]) in
+ ([id], typ) ] ];
+
END
+
type ('a,'b) gallina_loc_argtype = (Vernacexpr.vernac_expr located, 'a, 'b) Genarg.abstract_argument_type
let (wit_subtac_gallina_loc : (Genarg.tlevel, Proof_type.tactic) gallina_loc_argtype),
@@ -57,6 +74,11 @@ let (wit_subtac_gallina_loc : (Genarg.tlevel, Proof_type.tactic) gallina_loc_arg
Genarg.create_arg "subtac_gallina_loc"
VERNAC COMMAND EXTEND Subtac
-[ "Program" subtac_gallina_loc(g) ] ->
- [ Subtac.subtac g ]
+[ "Program" subtac_gallina_loc(g) ] -> [ Subtac.subtac g ]
+| [ "Obligation" integer(num) "of" ident(name) ] -> [ Subtac_obligations.subtac_obligation (num, Some name) ]
+| [ "Obligation" integer(num) ] -> [ Subtac_obligations.subtac_obligation (num, None) ]
+| [ "Solve" "Obligations" "of" ident(name) "using" tactic(t) ] -> [ Subtac_obligations.solve_obligations (Some name) (Tacinterp.interp t) ]
+| [ "Solve" "Obligations" "using" tactic(t) ] -> [ Subtac_obligations.solve_obligations None (Tacinterp.interp t) ]
+| [ "Obligations" "of" ident(name) ] -> [ Subtac_obligations.show_obligations (Some name) ]
+| [ "Obligations" ] -> [ Subtac_obligations.show_obligations None ]
END
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index ffb16a19..26e8f715 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 8964 2006-06-20 13:52:21Z msozeau $ *)
+(* $Id: subtac.ml 9284 2006-10-26 12:06:57Z msozeau $ *)
open Global
open Pp
@@ -156,19 +156,19 @@ let subtac (loc, command) =
match command with
VernacDefinition (defkind, (locid, id), expr, hook) ->
(match expr with
- ProveBody (bl, c) ->
- let evm, c, ctyp = Subtac_pretyping.subtac_process env isevars id bl c None in
- trace (str "Starting proof");
- Command.start_proof id goal_kind c hook;
- trace (str "Started proof");
+ ProveBody (bl, c) -> Subtac_pretyping.subtac_proof env isevars id bl c None
+(* let evm, c, ctyp = in *)
+(* trace (str "Starting proof"); *)
+(* Command.start_proof id goal_kind c hook; *)
+(* trace (str "Started proof"); *)
| DefineBody (bl, _, c, tycon) ->
- let evm, c, ctyp = Subtac_pretyping.subtac_process env isevars id bl c tycon in
- let tac = Eterm.etermtac (evm, c) in
- trace (str "Starting proof");
- Command.start_proof id goal_kind ctyp hook;
- trace (str "Started proof");
- Pfedit.by tac)
+ Subtac_pretyping.subtac_proof env isevars id bl c tycon
+ (* let tac = Eterm.etermtac (evm, c) in *)
+ (* trace (str "Starting proof"); *)
+ (* Command.start_proof id goal_kind ctyp hook; *)
+ (* trace (str "Started proof"); *)
+ (* Pfedit.by tac) *))
| VernacFixpoint (l, b) ->
let _ = trace (str "Building fixpoint") in
ignore(Subtac_command.build_recursive l b)
@@ -223,24 +223,30 @@ let subtac (loc, command) =
++ x ++ spc () ++ str "and" ++ spc () ++ y
in msg_warning cmds
- | Type_errors.TypeError (env, e) ->
- debug 2 (Himsg.explain_type_error env e)
+ | Type_errors.TypeError (env, exn) as e ->
+ debug 2 (Himsg.explain_type_error env exn);
+ raise e
- | Pretype_errors.PretypeError (env, e) ->
- debug 2 (Himsg.explain_pretype_error env e)
+ | Pretype_errors.PretypeError (env, exn) as e ->
+ debug 2 (Himsg.explain_pretype_error env exn);
+ raise e
- | Stdpp.Exc_located (loc, e) ->
+ | (Stdpp.Exc_located (loc, e')) as e ->
debug 2 (str "Parsing exception: ");
- (match e with
- | Type_errors.TypeError (env, e) ->
- debug 2 (Himsg.explain_type_error env e)
+ (match e' with
+ | Type_errors.TypeError (env, exn) ->
+ debug 2 (Himsg.explain_type_error env exn);
+ raise e
- | Pretype_errors.PretypeError (env, e) ->
- debug 2 (Himsg.explain_pretype_error env e)
+ | Pretype_errors.PretypeError (env, exn) ->
+ debug 2 (Himsg.explain_pretype_error env exn);
+ raise e
- | e -> msg_warning (str "Unexplained exception: " ++ Cerrors.explain_exn e))
+ | e'' -> msg_warning (str "Unexpected exception: " ++ Cerrors.explain_exn e'');
+ raise e)
| e ->
- msg_warning (str "Uncatched exception: " ++ Cerrors.explain_exn e)
+ msg_warning (str "Uncatched exception: " ++ Cerrors.explain_exn e);
+ raise e
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 78c3c70b..da5c497c 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -5,7 +5,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: subtac_coercion.ml 8964 2006-06-20 13:52:21Z msozeau $ *)
+(* $Id: subtac_coercion.ml 9284 2006-10-26 12:06:57Z msozeau $ *)
open Util
open Names
@@ -91,7 +91,9 @@ module Coercion = struct
let hnf env isevars c = whd_betadeltaiota env (evars_of !isevars) c
let rec mu env isevars t =
+ let isevars = ref isevars in
let rec aux v =
+ let v = hnf env isevars v in
match disc_subset v with
Some (u, p) ->
let f, ct = aux u in
@@ -135,8 +137,9 @@ module Coercion = struct
| Type x, Type y when x = y -> None (* false *)
| _ -> subco ())
| Prod (name, a, b), Prod (name', a', b') ->
- let c1 = coerce_unify env a' a in
+ let name' = Name (Nameops.next_ident_away (id_of_string "x") (Termops.ids_of_context env)) in
let env' = push_rel (name', None, a') env in
+ let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in
let c2 = coerce_unify env' b b' in
(match c1, c2 with
None, None -> failwith "subtac.coerce': Should have detected equivalence earlier"
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index c738d7a6..b433af2c 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -43,6 +43,7 @@ open Notation
module SPretyping = Subtac_pretyping.Pretyping
open Subtac_utils
open Pretyping
+open Subtac_obligations
(*********************************************************************)
(* Functions to parse and interpret constructions *)
@@ -149,15 +150,6 @@ let collect_non_rec env =
in
searchrec []
-let definition_message id =
- Options.if_verbose message ((string_of_id id) ^ " is defined")
-
-let recursive_message v =
- match Array.length v with
- | 0 -> error "no recursive definition"
- | 1 -> (Printer.pr_global v.(0) ++ str " is recursively defined")
- | _ -> hov 0 (prvect_with_sep pr_coma Printer.pr_global v ++
- spc () ++ str "are recursively defined")
let filter_map f l =
let rec aux acc = function
@@ -190,9 +182,12 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
let env = Global.env() in
let pr c = my_print_constr env c in
let prr = Printer.pr_rel_context env in
+ let prn = Printer.pr_named_context env in
let pr_rel env = Printer.pr_rel_context env in
+ let nc = named_context env in
+ let nc_len = named_context_length nc in
let _ =
- try debug 2 (str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++
+ try debug 2 (str "In named context: " ++ prn (named_context env) ++ str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++
Ppconstr.pr_binders bl ++ str " : " ++
Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++
Ppconstr.pr_constr_expr body)
@@ -204,25 +199,35 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
let argid = match argname with Name n -> n | _ -> assert(false) in
let _liftafter = lift_binders 1 after_length after in
let envwf = push_rel_context before env in
- let wf_rel, measure_fn =
- let rconstr = interp_constr isevars envwf r in
- if measure then
- let lt_rel = constr_of_global (Lazy.force lt_ref) in
- let name s = Name (id_of_string s) in
- mkLambda (name "x", argtyp,
- mkLambda (name "y", argtyp,
- mkApp (lt_rel,
- [| mkApp (rconstr, [| mkRel 2 |]) ;
- mkApp (rconstr, [| mkRel 1 |]) |]))),
- Some rconstr
- else rconstr, None
+ let wf_rel, wf_rel_fun, measure_fn =
+ let rconstr_body, rconstr =
+ let app = mkAppC (r, [mkIdentC (id_of_name argname)]) in
+ let env = push_rel_context [arg] envwf in
+ let capp = interp_constr isevars env app in
+ capp, mkLambda (argname, argtyp, capp)
+ in
+ if measure then
+ let lt_rel = constr_of_global (Lazy.force lt_ref) in
+ let name s = Name (id_of_string s) in
+ let wf_rel_fun =
+ (fun x y ->
+ mkApp (lt_rel, [| subst1 x rconstr_body;
+ subst1 y rconstr_body |]))
+ in
+ let wf_rel =
+ mkLambda (name "x", argtyp,
+ mkLambda (name "y", lift 1 argtyp,
+ wf_rel_fun (mkRel 2) (mkRel 1)))
+ in
+ wf_rel, wf_rel_fun , Some rconstr
+ else rconstr, (fun x y -> mkApp (rconstr, [|x; y|])), None
in
let wf_proof = mkApp (Lazy.force well_founded, [| argtyp ; wf_rel |])
in
let argid' = id_of_string (string_of_id argid ^ "'") in
let wfarg len = (Name argid', None,
- mkSubset (Name argid') argtyp
- (mkApp (wf_rel, [|mkRel 1; mkRel (len + 1)|])))
+ mkSubset (Name argid') argtyp
+ (wf_rel_fun (mkRel 1) (mkRel (len + 1))))
in
let top_bl = after @ (arg :: before) in
let intern_bl = after @ (wfarg 1 :: arg :: before) in
@@ -234,7 +239,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
let projection =
mkApp (proj, [| argtyp ;
(mkLambda (Name argid', argtyp,
- (mkApp (wf_rel, [|mkRel 1; mkRel 3|])))) ;
+ (wf_rel_fun (mkRel 1) (mkRel 3)))) ;
mkRel 1
|])
in
@@ -299,40 +304,16 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
in
let evm = non_instanciated_map env isevars in
let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in
- let evars_def, evars_typ, evars = Eterm.eterm_term evm fullcoqc (Some fullctyp) in
- let evars_typ = out_some evars_typ in
- (try trace (str "Building evars sum for : ");
- List.iter
- (fun (n, t) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env t))
- evars;
- with _ -> ());
- let (sum_tac, sumg) = Subtac_utils.build_dependent_sum evars in
- (try trace (str "Evars sum: " ++ my_print_constr env sumg);
- trace (str "Evars type: " ++ my_print_constr env evars_typ);
- with _ -> ());
- let proofid = id_of_string (string_of_id recname ^ "_evars_proof") in
- Command.start_proof proofid goal_proof_kind sumg
- (fun strength gr ->
- debug 2 (str "Proof finished");
- let def = constr_of_global gr in
- let args = Subtac_utils.destruct_ex def sumg in
- let _, newdef = decompose_lam_n (List.length args) evars_def in
- let constr = Term.substl (List.rev args) newdef in
- debug 2 (str "Applied existentials : " ++ my_print_constr env constr);
- let ce =
- { const_entry_body = constr;
- const_entry_type = Some fullctyp;
- const_entry_opaque = false;
- const_entry_boxed = boxed}
- in
- let _constant = Declare.declare_constant
- recname (DefinitionEntry ce,IsDefinition Definition)
- in
- definition_message recname);
- trace (str "Started existentials proof");
- Pfedit.by sum_tac;
- trace (str "Applied sum tac")
-
+ let evars, evars_def = Eterm.eterm_obligations recname nc_len evm fullcoqc (Some fullctyp) in
+ (try trace (str "Generated obligations : ");
+ Array.iter
+ (fun (n, t, _) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env t))
+ evars;
+ with _ -> ());
+ trace (str "Adding to obligations list");
+ Subtac_obligations.add_entry recname evars_def fullctyp evars;
+ trace (str "Added to obligations list")
+(*
let build_mutrec l boxed =
let sigma = Evd.empty
and env0 = Global.env()
@@ -543,7 +524,7 @@ let build_mutrec l boxed =
Environ.NoBody -> trace (str "Constant has no body")
| Environ.Opaque -> trace (str "Constant is opaque")
)
-
+*)
let out_n = function
Some n -> n
| None -> 0
@@ -563,8 +544,8 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
errorlabstrm "Subtac_command.build_recursive"
(str "Well-founded fixpoints not allowed in mutually recursive blocks"))
lnameargsardef
- in
- build_mutrec lnameargsardef boxed;
- assert(false)
+ in assert(false)
+ (*build_mutrec lnameargsardef boxed*)
+
diff --git a/contrib/subtac/subtac_command.mli b/contrib/subtac/subtac_command.mli
index 90ffb892..846e06cf 100644
--- a/contrib/subtac/subtac_command.mli
+++ b/contrib/subtac/subtac_command.mli
@@ -37,7 +37,6 @@ val interp_constr_judgment :
env ->
constr_expr -> unsafe_judgment
val list_chop_hd : int -> 'a list -> 'a list * 'a * 'a list
-val recursive_message : global_reference array -> std_ppcmds
val build_recursive :
(fixpoint_expr * decl_notation) list -> bool -> unit
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
new file mode 100644
index 00000000..7b13b402
--- /dev/null
+++ b/contrib/subtac/subtac_obligations.ml
@@ -0,0 +1,249 @@
+open Printf
+open Pp
+open Subtac_utils
+
+open Term
+open Names
+open Libnames
+open Summary
+open Libobject
+open Entries
+open Decl_kinds
+open Util
+open Evd
+
+type obligation =
+ { obl_name : identifier;
+ obl_type : types;
+ obl_body : constr option;
+ obl_deps : Intset.t;
+ }
+
+type obligations = (obligation array * int)
+
+type program_info = {
+ prg_name: identifier;
+ prg_body: constr;
+ prg_type: types;
+ prg_obligations: obligations;
+}
+
+let evar_of_obligation o = { evar_hyps = Environ.empty_named_context_val ;
+ evar_concl = o.obl_type ;
+ evar_body = Evar_empty ;
+ evar_extra = None }
+
+module ProgMap = Map.Make(struct type t = identifier let compare = compare end)
+
+let map_replace k v m = ProgMap.add k v (ProgMap.remove k m)
+
+let map_cardinal m =
+ let i = ref 0 in
+ ProgMap.iter (fun _ _ -> incr i) m;
+ !i
+
+exception Found of program_info
+
+let map_first m =
+ try
+ ProgMap.iter (fun _ v -> raise (Found v)) m;
+ assert(false)
+ with Found x -> x
+
+let from_prg : program_info ProgMap.t ref = ref ProgMap.empty
+
+let _ =
+ Summary.declare_summary "program-tcc-table"
+ { Summary.freeze_function = (fun () -> !from_prg);
+ Summary.unfreeze_function =
+ (fun v -> from_prg := v);
+ Summary.init_function =
+ (fun () -> from_prg := ProgMap.empty);
+ Summary.survive_module = false;
+ Summary.survive_section = false }
+
+let declare_definition prg =
+(* let obls_constrs =
+ Array.fold_right (fun x acc -> (out_some x.obl_evar.evar_body) :: acc) (fst prg.prg_obligations) []
+ in*)
+ let ce =
+ { const_entry_body = prg.prg_body;
+ const_entry_type = Some prg.prg_type;
+ const_entry_opaque = false;
+ const_entry_boxed = false}
+ in
+ let _constant = Declare.declare_constant
+ prg.prg_name (DefinitionEntry ce,IsDefinition Definition)
+ in
+ Subtac_utils.definition_message prg.prg_name
+
+open Evd
+
+let terms_of_evar ev =
+ match ev.evar_body with
+ Evar_defined b ->
+ let nc = Environ.named_context_of_val ev.evar_hyps in
+ let body = Termops.it_mkNamedLambda_or_LetIn b nc in
+ let typ = Termops.it_mkNamedProd_or_LetIn ev.evar_concl nc in
+ body, typ
+ | _ -> assert(false)
+
+let declare_obligation obl body =
+ let ce =
+ { const_entry_body = body;
+ const_entry_type = Some obl.obl_type;
+ const_entry_opaque = true;
+ const_entry_boxed = false}
+ in
+ let constant = Declare.declare_constant obl.obl_name (DefinitionEntry ce,IsProof Property)
+ in
+ 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
+
+let add_entry n b t obls =
+ Options.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
+ let init_obls e =
+ Array.map
+ (fun (n, t, d) ->
+ { obl_name = n ; obl_body = None; obl_type = t; obl_deps = d })
+ e
+ in
+ if Array.length obls = 0 then (
+ Options.if_verbose ppnl (str ".");
+ declare_definition { prg_name = n ; prg_body = b ; prg_type = t ; prg_obligations = ([||], 0) } )
+ else (
+ let len = Array.length obls in
+ let _ = Options.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in
+ let obls = init_obls obls in
+ let rem = Array.fold_left (fun acc obl -> if obl.obl_body = None then succ acc else acc) 0 obls in
+ let prg = { prg_name = n ; prg_body = b ; prg_type = t ; prg_obligations = (obls, rem) } in
+ if rem < len then
+ Options.if_verbose ppnl (int rem ++ str " obligation(s) remaining.");
+ if rem = 0 then
+ declare_definition prg
+ else
+ from_prg := ProgMap.add n prg !from_prg)
+
+let error s = Util.error s
+
+let get_prog name =
+ let prg_infos = !from_prg in
+ match name with
+ Some n -> ProgMap.find n prg_infos
+ | None ->
+ (let n = map_cardinal prg_infos in
+ match n with
+ 0 -> error "No obligations remaining"
+ | 1 -> map_first prg_infos
+ | _ -> error "More than one program with unsolved obligations")
+
+let update_obls prg obls rem =
+ let prg' = { prg with prg_obligations = (obls, rem) } in
+ if rem > 1 then (
+ debug 2 (int rem ++ str " obligations remaining");
+ from_prg := map_replace prg.prg_name prg' !from_prg)
+ else (
+ declare_definition prg';
+ from_prg := ProgMap.remove prg.prg_name !from_prg
+ )
+
+let is_defined obls x = obls.(x).obl_body <> None
+
+let deps_remaining obls x =
+ let deps = obls.(x).obl_deps in
+ Intset.fold
+ (fun x acc ->
+ if is_defined obls x then acc
+ else x :: acc)
+ deps []
+
+let subst_deps obls obl =
+ let t' =
+ Intset.fold
+ (fun x acc ->
+ let xobl = obls.(x) in
+ let oblb = out_some xobl.obl_body in
+ Term.subst1 oblb (Term.subst_var xobl.obl_name acc))
+ obl.obl_deps obl.obl_type
+ in { obl with obl_type = t' }
+
+let subtac_obligation (user_num, name) =
+ let num = pred user_num in
+ let prg = get_prog name in
+ let obls, rem = prg.prg_obligations in
+ if num < Array.length obls then
+ let obl = obls.(num) in
+ match obl.obl_body with
+ None ->
+ (match deps_remaining obls num with
+ [] ->
+ let obl = subst_deps obls obl in
+ Command.start_proof obl.obl_name Subtac_utils.goal_proof_kind 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
+ update_obls prg obls (pred rem));
+ trace (str "Started obligation " ++ int user_num ++ str " proof")
+ | l -> msgnl (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
+ ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l)))
+ | Some r -> error "Obligation already solved"
+ else error (sprintf "Unknown obligation number %i" (succ num))
+
+
+let obligations_of_evars evars =
+ let arr =
+ Array.of_list
+ (List.map
+ (fun (n, t) ->
+ { obl_name = n;
+ obl_type = t;
+ obl_body = None;
+ obl_deps = Intset.empty;
+ }) evars)
+ in arr, Array.length arr
+
+let solve_obligations n tac =
+ let prg = get_prog n in
+ let obls, rem = prg.prg_obligations in
+ let rem = ref rem in
+ let obls' =
+ Array.map (fun x ->
+ match x.obl_body with
+ Some _ -> x
+ | None ->
+ try
+ let t = Subtac_utils.solve_by_tac (evar_of_obligation x) tac in
+ decr rem;
+ { x with obl_body = Some t }
+ with _ -> x)
+ obls
+ in
+ update_obls prg obls' !rem
+
+open Pp
+let show_obligations n =
+ let prg = get_prog n in
+ let obls, rem = prg.prg_obligations in
+ msgnl (int rem ++ str " obligation(s) remaining: ");
+ Array.iteri (fun i x ->
+ match x.obl_body with
+ None -> msgnl (int (succ i) ++ str " : " ++ spc () ++
+ my_print_constr (Global.env ()) x.obl_type)
+ | Some _ -> ())
+ obls
+
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli
new file mode 100644
index 00000000..7d93d57b
--- /dev/null
+++ b/contrib/subtac/subtac_obligations.mli
@@ -0,0 +1,10 @@
+open Util
+
+val add_entry : Names.identifier -> Term.constr -> Term.types ->
+ (Names.identifier * Term.types * Intset.t) array -> unit
+
+val subtac_obligation : int * Names.identifier option -> unit
+
+val solve_obligations : Names.identifier option -> Proof_type.tactic -> unit
+
+val show_obligations : Names.identifier option -> unit
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index 261e0c5b..a243ba34 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 8889 2006-06-01 20:23:56Z msozeau $ *)
+(* $Id: subtac_pretyping.ml 9326 2006-10-31 12:57:26Z msozeau $ *)
open Global
open Pp
@@ -151,3 +151,13 @@ let subtac_process env isevars id l c tycon =
let evm = non_instanciated_map env isevars in
let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in
evm, fullcoqc, fullctyp
+
+open Subtac_obligations
+
+let subtac_proof env isevars id l c tycon =
+ let nc = named_context env in
+ let nc_len = named_context_length nc in
+ let evm, coqc, coqt = subtac_process env isevars id l c tycon in
+ let evars, def = Eterm.eterm_obligations id nc_len evm coqc (Some coqt) in
+ trace (str "Adding to obligations list");
+ add_entry id def coqt evars
diff --git a/contrib/subtac/subtac_pretyping.mli b/contrib/subtac/subtac_pretyping.mli
index 97e56ecb..b62a8766 100644
--- a/contrib/subtac/subtac_pretyping.mli
+++ b/contrib/subtac/subtac_pretyping.mli
@@ -10,3 +10,6 @@ module Pretyping : Pretyping.S
val subtac_process : env -> evar_defs ref -> identifier -> local_binder list ->
constr_expr -> constr_expr option -> evar_map * constr * types
+
+val subtac_proof : env -> evar_defs ref -> identifier -> local_binder list ->
+ constr_expr -> constr_expr option -> unit
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index 65952750..46af5886 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: subtac_pretyping_F.ml 8889 2006-06-01 20:23:56Z msozeau $ *)
+(* $Id: subtac_pretyping_F.ml 9316 2006-10-29 22:49:11Z herbelin $ *)
open Pp
open Util
@@ -315,12 +315,11 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj ftycon args) in
let resj =
match kind_of_term resj.uj_val with
- | App (f,args) when isInd f ->
+ | App (f,args) when isInd f or isConst f ->
let sigma = evars_of !isevars in
- let t = Retyping.type_of_inductive_knowing_parameters env sigma (destInd f) args in
- let s = snd (splay_arity env sigma t) in
- on_judgment_type (set_inductive_level env s) resj
- (* Rem: no need to send sigma: no head evar, it's an arity *)
+ let c = mkApp (f,Array.map (whd_evar sigma) args) in
+ let t = Retyping.get_type_of env sigma c in
+ make_judge c t
| _ -> resj in
inh_conv_coerce_to_tycon loc env isevars resj tycon
@@ -557,35 +556,6 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
(pretype_type empty_valcon env isevars lvar c).utj_val in
nf_evar (evars_of !isevars) c'
- (* [check_evars] fails if some unresolved evar remains *)
- (* it assumes that the defined existentials have already been substituted
- (should be done in unsafe_infer and unsafe_infer_type) *)
-
- let check_evars env initial_sigma isevars c =
- let sigma = evars_of !isevars in
- let rec proc_rec c =
- match kind_of_term c with
- | Evar (ev,args) ->
- assert (Evd.mem sigma ev);
- if not (Evd.mem initial_sigma ev) then
- let (loc,k) = evar_source ev !isevars in
- error_unsolvable_implicit loc env sigma k
- | _ -> iter_constr proc_rec c
- in
- proc_rec c(*;
- let (_,pbs) = get_conv_pbs !isevars (fun _ -> true) in
- if pbs <> [] then begin
- pperrnl
- (str"TYPING OF "++Termops.print_constr_env env c++fnl()++
- prlist_with_sep fnl
- (fun (pb,c1,c2) ->
- Termops.print_constr c1 ++
- (if pb=Reduction.CUMUL then str " <="++ spc()
- else str" =="++spc()) ++
- Termops.print_constr c2)
- pbs ++ fnl())
- end*)
-
(* TODO: comment faire remonter l'information si le typage a resolu des
variables du sigma original. il faudrait que la fonction de typage
retourne aussi le nouveau sigma...
@@ -595,6 +565,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let isevars = ref (create_evar_defs sigma) in
let j = pretype empty_tycon env isevars ([],[]) c in
let j = j_nf_evar (evars_of !isevars) j in
+ let isevars,_ = consider_remaining_unif_problems env !isevars in
check_evars env sigma isevars (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
j
@@ -611,8 +582,10 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let ise_pretype_gen fail_evar sigma env lvar kind c =
let isevars = ref (Evd.create_evar_defs sigma) in
let c = pretype_gen isevars env lvar kind c in
+ let isevars,_ = consider_remaining_unif_problems env !isevars in
+ let c = nf_evar (evars_of isevars) c in
if fail_evar then check_evars env sigma isevars c;
- !isevars, c
+ isevars, c
(** Entry points of the high-level type synthesis algorithm *)
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index d4db7c27..7b96758a 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -80,25 +80,34 @@ open Pp
let my_print_constr = Termops.print_constr_env
let my_print_constr_expr = Ppconstr.pr_constr_expr
let my_print_context = Termops.print_rel_context
+let my_print_named_context = Termops.print_named_context
let my_print_env = Termops.print_env
let my_print_rawconstr = Printer.pr_rawconstr_env
let my_print_evardefs = Evd.pr_evar_defs
let my_print_tycon_type = Evarutil.pr_tycon_type
-let debug_level = 2
+let debug_level = 1
+
+let debug_on = true
let debug n s =
- if !Options.debug && n >= debug_level then
- msgnl s
+ if debug_on then
+ if !Options.debug && n >= debug_level then
+ msgnl s
+ else ()
else ()
let debug_msg n s =
- if !Options.debug && n >= debug_level then s
+ if debug_on then
+ if !Options.debug && n >= debug_level then s
+ else mt ()
else mt ()
let trace s =
- if !Options.debug && debug_level > 0 then msgnl s
+ if debug_on then
+ if !Options.debug && debug_level > 0 then msgnl s
+ else ()
else ()
let wf_relations = Hashtbl.create 10
@@ -167,30 +176,6 @@ let goal_fix_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Fixp
open Tactics
open Tacticals
-let build_dependent_sum l =
- let rec aux (tac, typ) = function
- (n, t) :: tl ->
- let t' = mkLambda (Name n, t, typ) in
- trace (spc () ++ str ("treating evar " ^ string_of_id n));
- (try trace (str " assert: " ++ my_print_constr (Global.env ()) t)
- with _ -> ());
- let tac' =
- tclTHENS (assert_tac true (Name n) t)
- ([intros;
- (tclTHENSEQ
- [constructor_tac (Some 1) 1
- (Rawterm.ImplicitBindings [mkVar n]);
- tac]);
- ])
- in
- let newt = mkApp (Lazy.force ex_ind, [| t; t'; |]) in
- aux (tac', newt) tl
- | [] -> tac, typ
- in
- match l with
- (_, hd) :: tl -> aux (intros, hd) tl
- | [] -> raise (Invalid_argument "build_dependent_sum")
-
let id x = x
let build_dependent_sum l =
@@ -438,3 +423,32 @@ let rewrite_cases env c =
let c' = rewrite_cases c in
let _ = trace (str "Rewrote cases: " ++ spc () ++ my_print_rawconstr env c') in
c'
+
+let id_of_name = function
+ Name n -> n
+ | Anonymous -> raise (Invalid_argument "id_of_name")
+
+let definition_message id =
+ Options.if_verbose message ((string_of_id id) ^ " is defined")
+
+let recursive_message v =
+ match Array.length v with
+ | 0 -> error "no recursive definition"
+ | 1 -> (Printer.pr_global v.(0) ++ str " is recursively defined")
+ | _ -> hov 0 (prvect_with_sep pr_coma Printer.pr_global v ++
+ spc () ++ str "are recursively defined")
+
+(* Solve an obligation using tactics, return the corresponding proof term *)
+let solve_by_tac ev t =
+ debug 1 (str "Solving goal using tactics: " ++ Evd.pr_evar_info ev);
+ let goal = Proof_trees.mk_goal ev.evar_hyps ev.evar_concl None in
+ let ts = Tacmach.mk_pftreestate goal in
+ let solved_state = Tacmach.solve_pftreestate t ts in
+ let c = Tacmach.extract_pftreestate solved_state in
+ debug 1 (str "Term constructed in solve by tac: " ++ my_print_constr (Global.env ()) c);
+ c
+
+let rec string_of_list sep f = function
+ [] -> ""
+ | x :: [] -> f x
+ | x :: ((y :: _) as tl) -> f x ^ sep ^ string_of_list sep f tl
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index 4a7e8177..ebfc5123 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -10,6 +10,7 @@ open Rawterm
open Util
open Evarutil
open Names
+open Sign
val contrib_name : string
val subtac_dir : string list
@@ -51,6 +52,7 @@ val my_print_constr : env -> constr -> std_ppcmds
val my_print_constr_expr : constr_expr -> std_ppcmds
val my_print_evardefs : evar_defs -> std_ppcmds
val my_print_context : env -> std_ppcmds
+val my_print_named_context : env -> std_ppcmds
val my_print_env : env -> std_ppcmds
val my_print_rawconstr : env -> rawconstr -> std_ppcmds
val my_print_tycon_type : env -> type_constraint_type -> std_ppcmds
@@ -88,3 +90,11 @@ val and_tac : (identifier * 'a * constr * Proof_type.tactic) list ->
val destruct_ex : constr -> constr -> constr list
val rewrite_cases : Environ.env -> Rawterm.rawconstr -> Rawterm.rawconstr
+val id_of_name : name -> identifier
+
+val definition_message : identifier -> unit
+val recursive_message : global_reference array -> std_ppcmds
+
+val solve_by_tac : evar_info -> Tacmach.tactic -> constr
+
+val string_of_list : string -> ('a -> string) -> 'a list -> string
diff --git a/contrib/subtac/test/ListDep.v b/contrib/subtac/test/ListDep.v
new file mode 100644
index 00000000..7ab720f6
--- /dev/null
+++ b/contrib/subtac/test/ListDep.v
@@ -0,0 +1,86 @@
+Require Import List.
+Require Import Coq.subtac.Utils.
+
+Set Implicit Arguments.
+
+Definition sub_list (A : Set) (l' l : list A) := (forall v, In v l' -> In v l) /\ length l' <= length l.
+
+Lemma sub_list_tl : forall A : Set, forall x (l l' : list A), sub_list (x :: l) l' -> sub_list l l'.
+Proof.
+ intros.
+ inversion H.
+ split.
+ intros.
+ apply H0.
+ auto with datatypes.
+ auto with arith.
+Qed.
+
+Section Map_DependentRecursor.
+ Variable U V : Set.
+ Variable l : list U.
+ Variable f : { x : U | In x l } -> V.
+
+ Program Fixpoint map_rec ( l' : list U | sub_list l' l )
+ { measure l' length } : { r : list V | length r = length l' } :=
+ match l' with
+ nil => nil
+ | cons x tl => let tl' := map_rec tl in
+ f x :: tl'
+ end.
+
+ Obligation 1.
+ intros.
+ destruct tl' ; simpl ; simpl in e.
+ subst x0 tl0.
+ rewrite <- Heql'.
+ rewrite e.
+ auto.
+ Qed.
+
+ Obligation 2.
+ simpl.
+ intros.
+ destruct l'.
+ simpl in Heql'.
+ destruct x0 ; simpl ; try discriminate.
+ inversion Heql'.
+ inversion s.
+ apply H.
+ auto with datatypes.
+ Qed.
+
+
+ Obligation 3 of map_rec.
+ simpl.
+ intros.
+ rewrite <- Heql'.
+ simpl ; auto with arith.
+ Qed.
+
+ Obligation 4.
+ simpl.
+ intros.
+ destruct l'.
+ simpl in Heql'.
+ destruct x0 ; simpl ; try discriminate.
+ inversion Heql'.
+ subst x tl.
+ apply sub_list_tl with u ; auto.
+ Qed.
+
+ Obligation 5.
+ intros.
+ rewrite <- Heql' ; auto.
+ Qed.
+
+ Program Definition map : list V := map_rec l.
+ Obligation 1.
+ split ; auto.
+ Qed.
+
+End Map_DependentRecursor.
+
+Extraction map.
+Extraction map_rec.
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 22:35:04 +0000