summaryrefslogtreecommitdiff
path: root/contrib/subtac
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/subtac')
-rw-r--r--contrib/subtac/Utils.v28
-rw-r--r--contrib/subtac/eterm.ml28
-rw-r--r--contrib/subtac/g_subtac.ml410
-rw-r--r--contrib/subtac/subtac.ml53
-rw-r--r--contrib/subtac/subtac_coercion.ml53
-rw-r--r--contrib/subtac/subtac_command.ml77
-rw-r--r--contrib/subtac/subtac_interp_fixpoint.ml68
-rw-r--r--contrib/subtac/subtac_interp_fixpoint.mli11
-rw-r--r--contrib/subtac/subtac_pretyping.ml23
-rw-r--r--contrib/subtac/subtac_pretyping_F.ml639
-rw-r--r--contrib/subtac/subtac_utils.ml122
-rw-r--r--contrib/subtac/subtac_utils.mli4
-rw-r--r--contrib/subtac/test/ListsTest.v95
-rw-r--r--contrib/subtac/test/Mutind.v7
-rw-r--r--contrib/subtac/test/Test1.v16
-rw-r--r--contrib/subtac/test/euclid.v66
-rw-r--r--contrib/subtac/test/id.v46
-rw-r--r--contrib/subtac/test/rec.v65
18 files changed, 1215 insertions, 196 deletions
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
index 9acb10ae..db10cb2a 100644
--- a/contrib/subtac/Utils.v
+++ b/contrib/subtac/Utils.v
@@ -1,20 +1,17 @@
Set Implicit Arguments.
+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.
+
Definition ex_pi1 (A : Prop) (P : A -> Prop) (t : ex P) : A.
intros.
induction t.
exact x.
Defined.
-Check proj1_sig.
-Lemma subset_simpl : forall (A : Set) (P : A -> Prop)
- (t : sig P), P (proj1_sig t).
-Proof.
-intros.
-induction t.
- simpl ; auto.
-Qed.
-
Lemma ex_pi2 : forall (A : Prop) (P : A -> Prop) (t : ex P),
P (ex_pi1 t).
intros A P.
@@ -23,12 +20,17 @@ simpl.
exact p.
Defined.
+
+Notation "` t" := (proj1_sig t) (at level 100) : core_scope.
Notation "'forall' { x : A | P } , Q" :=
(forall x:{x:A|P}, Q)
(at level 200, x ident, right associativity).
-Notation "'fun' { x : A | P } => Q" :=
- (fun x:{x:A|P} => Q)
- (at level 200, x ident, right associativity).
+Lemma subset_simpl : forall (A : Set) (P : A -> Prop)
+ (t : sig P), P (` t).
+Proof.
+intros.
+induction t.
+ simpl ; auto.
+Qed.
-Notation "( x & y )" := (@existS _ _ x y) : core_scope.
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index 5703c0ef..382ae2d5 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -47,9 +47,9 @@ let subst_evars evs n t =
| Evar (k, args) ->
(try
let index, hyps = evar_info k in
- trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++
- int (List.length hyps) ++ str " hypotheses");
-
+ (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)
@@ -128,7 +128,7 @@ let eterm_term evm t tycon =
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_app
+ and tycon = option_map
(fun typ -> Termops.it_mkProd_wo_LetIn typ anon_evar_bl) tycon
in
let _declare_evar (id, c) =
@@ -140,15 +140,17 @@ let eterm_term evm t tycon =
let id = id_of_string ("Evar" ^ string_of_int id) in
tclTHEN acc (Tactics.assert_tac false (Name id) c)
in
- trace (str "Term given to eterm" ++ spc () ++
- Termops.print_constr_env (Global.env ()) t);
- trace (str "Term constructed in eterm" ++ spc () ++
- Termops.print_constr_env (Global.env ()) t'');
- ignore(option_app
- (fun typ ->
- trace (str "Type :" ++ spc () ++
- Termops.print_constr_env (Global.env ()) typ))
- tycon);
+ (try
+ trace (str "Term given to eterm" ++ spc () ++
+ 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);
+ with _ -> ());
t'', tycon, evar_names
let mkMetas n =
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index c3f2a24d..b56ecc3d 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 8688 2006-04-07 15:08:12Z msozeau $ *)
+(* $Id: g_subtac.ml4 8917 2006-06-07 16:59:05Z herbelin $ *)
(*i camlp4deps: "parsing/grammar.cma" i*)
@@ -49,11 +49,11 @@ GEXTEND Gram
;
END
-type gallina_loc_argtype = (Vernacexpr.vernac_expr located, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type
+type ('a,'b) gallina_loc_argtype = (Vernacexpr.vernac_expr located, 'a, 'b) Genarg.abstract_argument_type
-let (wit_subtac_gallina_loc : gallina_loc_argtype),
- (globwit_subtac_gallina_loc : gallina_loc_argtype),
- (rawwit_subtac_gallina_loc : gallina_loc_argtype) =
+let (wit_subtac_gallina_loc : (Genarg.tlevel, Proof_type.tactic) gallina_loc_argtype),
+ (globwit_subtac_gallina_loc : (Genarg.glevel, Tacexpr.glob_tactic_expr) gallina_loc_argtype),
+ (rawwit_subtac_gallina_loc : (Genarg.rlevel, Tacexpr.raw_tactic_expr) gallina_loc_argtype) =
Genarg.create_arg "subtac_gallina_loc"
VERNAC COMMAND EXTEND Subtac
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index 84b7d39b..cd2e7c43 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 8688 2006-04-07 15:08:12Z msozeau $ *)
+(* $Id: subtac.ml 8889 2006-06-01 20:23:56Z msozeau $ *)
open Global
open Pp
@@ -48,8 +48,10 @@ let subtac_one_fixpoint env isevars (f, decl) =
let ((id, n, bl, typ, body), decl) =
Subtac_interp_fixpoint.rewrite_fixpoint env [] (f, decl)
in
- let _ = trace (str "Working on a single fixpoint rewritten as: " ++ spc () ++
- Ppconstr.pr_constr_expr body)
+ let _ =
+ try trace (str "Working on a single fixpoint rewritten as: " ++ spc () ++
+ Ppconstr.pr_constr_expr body)
+ with _ -> ()
in ((id, n, bl, typ, body), decl)
@@ -115,16 +117,44 @@ let subtac_end_proof = function
*)
+open Pp
+open Ppconstr
+open Decl_kinds
+
+let start_proof_com env isevars sopt kind (bl,t) hook =
+ let id = match sopt with
+ | Some id ->
+ (* We check existence here: it's a bit late at Qed time *)
+ if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
+ errorlabstrm "start_proof" (pr_id id ++ str " already exists");
+ id
+ | None ->
+ next_global_ident_away false (id_of_string "Unnamed_thm")
+ (Pfedit.get_all_proof_names ())
+ in
+ let evm, c, typ =
+ Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr t bl) None
+ in
+ let _ = Typeops.infer_type env c in
+ Command.start_proof id kind c hook
+
+let print_subgoals () = Options.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
+
+let start_proof_and_print env isevars idopt k t hook =
+ start_proof_com env isevars idopt k t hook;
+ print_subgoals ()
+ (*if !pcoq <> None then (out_some !pcoq).start_proof ()*)
+
let subtac (loc, command) =
check_required_library ["Coq";"Init";"Datatypes"];
check_required_library ["Coq";"Init";"Specif"];
require_library "Coq.subtac.FixSub";
require_library "Coq.subtac.Utils";
+ let env = Global.env () in
+ let isevars = ref (create_evar_defs Evd.empty) in
try
match command with
VernacDefinition (defkind, (locid, id), expr, hook) ->
- let env = Global.env () in
- let isevars = ref (create_evar_defs Evd.empty) in
(match expr with
ProveBody (bl, c) ->
let evm, c, ctyp = Subtac_pretyping.subtac_process env isevars id bl c None in
@@ -142,6 +172,19 @@ let subtac (loc, command) =
| VernacFixpoint (l, b) ->
let _ = trace (str "Building fixpoint") in
ignore(Subtac_command.build_recursive l b)
+
+ | VernacStartTheoremProof (thkind, (locid, id), (bl, t), lettop, hook) ->
+ if not(Pfedit.refining ()) then
+ if lettop then
+ errorlabstrm "Subtac_command.StartProof"
+ (str "Let declarations can only be used in proof editing mode");
+ if Lib.is_modtype () then
+ errorlabstrm "Subtac_command.StartProof"
+ (str "Proof editing mode not supported in module types");
+ start_proof_and_print env isevars (Some id) (Global, Proof thkind) (bl,t) hook
+
+
+
(*| VernacEndProof e ->
subtac_end_proof e*)
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 7c8ea2d6..7428e1ed 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 8695 2006-04-10 16:33:52Z msozeau $ *)
+(* $Id: subtac_coercion.ml 8889 2006-06-01 20:23:56Z msozeau $ *)
open Util
open Names
@@ -53,7 +53,8 @@ module Coercion = struct
| _ -> None
and disc_exist env x =
- trace (str "Disc_exist: " ++ my_print_constr env x);
+ (try trace (str "Disc_exist: " ++ my_print_constr env x)
+ with _ -> ());
match kind_of_term x with
| App (c, l) ->
(match kind_of_term c with
@@ -66,7 +67,8 @@ module Coercion = struct
let disc_proj_exist env x =
- trace (str "disc_proj_exist: " ++ my_print_constr env x);
+ (try trace (str "disc_proj_exist: " ++ my_print_constr env x);
+ with _ -> ());
match kind_of_term x with
| App (c, l) ->
(if Term.eq_constr c (Lazy.force sig_).proj1
@@ -97,30 +99,34 @@ module Coercion = struct
app_opt f (mkApp ((Lazy.force sig_).proj1,
[| u; p; x |]))),
ct)
- | None -> (None, t)
+ | None -> (None, v)
in aux t
and coerce loc env isevars (x : Term.constr) (y : Term.constr)
: (Term.constr -> Term.constr) option
=
let x = nf_evar (evars_of !isevars) x and y = nf_evar (evars_of !isevars) y in
- trace (str "Coerce called for " ++ (my_print_constr env x) ++
- str " and "++ my_print_constr env y ++
- str " with evars: " ++ spc () ++
- my_print_evardefs !isevars);
+ (try trace (str "Coerce called for " ++ (my_print_constr env x) ++
+ str " and "++ my_print_constr env y ++
+ str " with evars: " ++ spc () ++
+ my_print_evardefs !isevars);
+ with _ -> ());
let rec coerce_unify env x y =
- trace (str "coerce_unify from " ++ (my_print_constr env x) ++
- str " to "++ my_print_constr env y);
+ (try trace (str "coerce_unify from " ++ (my_print_constr env x) ++
+ str " to "++ my_print_constr env y)
+ with _ -> ());
try
isevars := the_conv_x_leq env x y !isevars;
- trace (str "Unified " ++ (my_print_constr env x) ++
- str " and "++ my_print_constr env y);
+ (try (trace (str "Unified " ++ (my_print_constr env x) ++
+ str " and "++ my_print_constr env y));
+ with _ -> ());
None
with Reduction.NotConvertible -> coerce' env (hnf env isevars x) (hnf env isevars y)
and coerce' env x y : (Term.constr -> Term.constr) option =
let subco () = subset_coerce env isevars x y in
- trace (str "coerce' from " ++ (my_print_constr env x) ++
- str " to "++ my_print_constr env y);
+ (try trace (str "coerce' from " ++ (my_print_constr env x) ++
+ str " to "++ my_print_constr env y);
+ with _ -> ());
match (kind_of_term x, kind_of_term y) with
| Sort s, Sort s' ->
(match s, s' with
@@ -153,7 +159,7 @@ module Coercion = struct
if i = Term.destInd existS.typ
then
begin
- debug 1 (str "In coerce sigma types");
+ trace (str "In coerce sigma types");
let (a, pb), (a', pb') =
pair_of_array l, pair_of_array l'
in
@@ -244,7 +250,7 @@ module Coercion = struct
let coerce_itf loc env isevars v t c1 =
let evars = ref isevars in
let coercion = coerce loc env evars t c1 in
- !evars, option_app (app_opt coercion) v, t
+ !evars, option_map (app_opt coercion) v, t
(* Taken from pretyping/coercion.ml *)
@@ -339,6 +345,13 @@ module Coercion = struct
| _ ->
inh_tosort_force loc env isevars j
+ let inh_coerce_to_base loc env isevars j =
+ let typ = whd_betadeltaiota env (evars_of isevars) j.uj_type in
+ let ct, typ' = mu env isevars typ in
+ isevars, { uj_val = app_opt ct j.uj_val;
+ uj_type = typ' }
+
+
let inh_coerce_to_fail env isevars c1 v t =
let v', t' =
try
@@ -371,7 +384,7 @@ module Coercion = struct
(match kind_of_term (whd_betadeltaiota env (evars_of isevars) t),
kind_of_term (whd_betadeltaiota env (evars_of isevars) c1) with
| Prod (_,t1,t2), Prod (name,u1,u2) ->
- let v' = option_app (whd_betadeltaiota env (evars_of isevars)) v in
+ let v' = option_map (whd_betadeltaiota env (evars_of isevars)) v in
let (evd',b) =
match v' with
Some v' ->
@@ -387,7 +400,7 @@ module Coercion = struct
let env1 = push_rel (x,None,v1) env in
let (evd'', v2', t2') = inh_conv_coerce_to_fail loc env1 evd'
(Some v2) t2 u2 in
- (evd'', option_app (fun v2' -> mkLambda (x, v1, v2')) v2',
+ (evd'', option_map (fun v2' -> mkLambda (x, v1, v2')) v2',
mkProd (x, v1, t2'))
| None ->
(* Mismatch on t1 and u1 or not a lambda: we eta-expand *)
@@ -404,7 +417,7 @@ module Coercion = struct
let (evd'', v2', t2') =
let v2 =
match v with
- Some v -> option_app (fun v1' -> mkApp (lift 1 v, [|v1'|])) v1'
+ Some v -> option_map (fun v1' -> mkApp (lift 1 v, [|v1'|])) v1'
| None -> None
and evd', t2 =
match v1' with
@@ -415,7 +428,7 @@ module Coercion = struct
in
inh_conv_coerce_to_fail loc env1 evd' v2 t2 u2
in
- (evd'', option_app (fun v2' -> mkLambda (name, u1, v2')) v2',
+ (evd'', option_map (fun v2' -> mkLambda (name, u1, v2')) v2',
mkProd (name, u1, t2')))
| _ -> raise NoCoercion))
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 1b92c691..b09228c0 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -55,8 +55,8 @@ let interp_gen kind isevars env
?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[]))
c =
let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars (Evd.evars_of !isevars) env c in
- let c' = Subtac_interp_fixpoint.rewrite_cases env c' in
- msgnl (str "Pretyping " ++ my_print_constr_expr c);
+ let c' = Subtac_utils.rewrite_cases env c' in
+ (try trace (str "Pretyping " ++ my_print_constr_expr c) with _ -> ());
let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in
evar_nf isevars c'
@@ -200,15 +200,18 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in
(Environ.push_named (recname,None,arity) env, impls', (isevars, None, arity)::arl)
| CWfRec r ->
- let _ = trace (str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++
- Ppconstr.pr_binders bl ++ str " : " ++
- Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++
- Ppconstr.pr_constr_expr body)
+ let n = out_some n in
+ let _ =
+ try trace (str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++
+ Ppconstr.pr_binders bl ++ str " : " ++
+ Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++
+ Ppconstr.pr_constr_expr body)
+ with _ -> ()
in
let env', binders_rel = interp_context isevars env0 bl in
let after, ((argname, _, argtyp) as arg), before = list_chop_hd n binders_rel in
let argid = match argname with Name n -> n | _ -> assert(false) in
- let after' = List.map (fun (n, c, t) -> (n, option_app (lift 1) c, lift 1 t)) after in
+ let after' = List.map (fun (n, c, t) -> (n, option_map (lift 1) c, lift 1 t)) after in
let envwf = push_rel_context before env0 in
let wf_rel = interp_constr isevars envwf r in
let accarg_id = id_of_string ("Acc_" ^ string_of_id argid) in
@@ -233,10 +236,11 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
let _ =
let pr c = my_print_constr env c in
let prr = Printer.pr_rel_context env in
- trace (str "Fun bl: " ++ prr fun_bl ++ spc () ++
- str "Intern bl" ++ prr intern_bl ++ spc () ++
- str "Extern bl" ++ prr new_bl ++ spc () ++
- str "Intern arity: " ++ pr intern_arity)
+ try trace (str "Fun bl: " ++ prr fun_bl ++ spc () ++
+ str "Intern bl" ++ prr intern_bl ++ spc () ++
+ str "Extern bl" ++ prr new_bl ++ spc () ++
+ str "Intern arity: " ++ pr intern_arity)
+ with _ -> ()
in
let impl =
if Impargs.is_implicit_args()
@@ -279,14 +283,15 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
let (lnonrec,(namerec,defrec,arrec,nvrec)) =
collect_non_rec env0 lrecnames recdef arityl nv in
- let nvrec' = Array.map fst nvrec in(* ignore rec order *)
+ let nvrec' = Array.map (function (Some n,_) -> n | _ -> 0) nvrec in(* ignore rec order *)
let declare arrec defrec =
let recvec =
Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in
let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in
let rec declare i fi =
- trace (str "Declaring: " ++ pr_id fi ++ spc () ++
- my_print_constr env0 (recvec.(i)));
+ (try trace (str "Declaring: " ++ pr_id fi ++ spc () ++
+ my_print_constr env0 (recvec.(i)));
+ with _ -> ());
let ce =
{ const_entry_body = mkFix ((nvrec',i),recdecls);
const_entry_type = Some arrec.(i);
@@ -331,20 +336,20 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
let rec collect_evars i acc =
if i < recdefs then
let (isevars, info, def) = defrec.(i) in
- let _ = trace (str "In solve evars, isevars is: " ++ Evd.pr_evar_defs !isevars) in
+ let _ = try trace (str "In solve evars, isevars is: " ++ Evd.pr_evar_defs !isevars) with _ -> () in
let def = evar_nf isevars def in
let isevars = Evd.undefined_evars !isevars in
- let _ = trace (str "In solve evars, undefined is: " ++ Evd.pr_evar_defs isevars) in
+ let _ = try trace (str "In solve evars, undefined is: " ++ Evd.pr_evar_defs isevars) with _ -> () in
let evm = Evd.evars_of isevars in
let _, _, typ = arrec.(i) in
let id = namerec.(i) in
- let evars_def, evars_typ, evars = Eterm.eterm_term evm def (Some typ) in
(* Generalize by the recursive prototypes *)
let def =
Termops.it_mkNamedLambda_or_LetIn def (Environ.named_context rec_sign)
and typ =
Termops.it_mkNamedProd_or_LetIn typ (Environ.named_context rec_sign)
in
+ let evars_def, evars_typ, evars = Eterm.eterm_term evm def (Some typ) in
(*let evars_typ = match evars_typ with Some t -> t | None -> assert(false) in*)
(*let fi = id_of_string (string_of_id id ^ "_evars") in*)
(*let ce =
@@ -357,10 +362,16 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
trace (str (string_of_id fi) ++ str " is defined");*)
let evar_sum =
if evars = [] then None
- else
+ else (
+ (try trace (str "Building evars sum for : ");
+ List.iter
+ (fun (n, t) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env0 t))
+ evars;
+ with _ -> ());
let sum = Subtac_utils.build_dependent_sum evars in
- trace (str "Evars sum: " ++ my_print_constr env0 (pi1 sum));
- Some sum
+ (try trace (str "Evars sum: " ++ my_print_constr env0 (snd sum));
+ with _ -> ());
+ Some sum)
in
collect_evars (succ i) ((id, evars_def, evar_sum) :: acc)
else acc
@@ -370,32 +381,34 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
(* Solve evars then create the definitions *)
let real_evars =
filter_map (fun (id, kn, sum) ->
- match sum with Some (sumg, sumtac, _) -> Some (id, kn, sumg, sumtac) | None -> None)
+ match sum with Some (sumtac, sumg) -> Some (id, kn, sumg, sumtac) | None -> None)
defs
in
Subtac_utils.and_tac real_evars
(fun f _ gr ->
- let _ = trace (str "Got a proof of: " ++ pr_global gr) in
+ let _ = trace (str "Got a proof of: " ++ pr_global gr ++
+ str "type: " ++ my_print_constr (Global.env ()) (Global.type_of_global gr)) in
let constant = match gr with Libnames.ConstRef c -> c
| _ -> assert(false)
in
try
(*let value = Environ.constant_value (Global.env ()) constant in*)
let pis = f (mkConst constant) in
- trace (str "Accessors: " ++
- List.fold_right (fun (_, _, _, c) acc -> my_print_constr env0 c ++ spc () ++ acc)
- pis (mt()));
- trace (str "Applied existentials: " ++
- (List.fold_right
- (fun (id, kn, sumg, pi) acc ->
- let args = Subtac_utils.destruct_ex pi sumg in
- my_print_constr env0 (mkApp (kn, Array.of_list args)))
- pis (mt ())));
+ (try (trace (str "Accessors: " ++
+ List.fold_right (fun (_, _, _, c) acc -> my_print_constr env0 c ++ spc () ++ acc)
+ pis (mt()));
+ trace (str "Applied existentials: " ++
+ (List.fold_right
+ (fun (id, kn, sumg, pi) acc ->
+ let args = Subtac_utils.destruct_ex pi sumg in
+ my_print_constr env0 (mkApp (kn, Array.of_list args)))
+ pis (mt ()))))
+ with _ -> ());
let rec aux pis acc = function
(id, kn, sum) :: tl ->
(match sum with
None -> aux pis (kn :: acc) tl
- | Some (sumg, _, _) ->
+ | Some (_, sumg) ->
let (id, kn, sumg, pi), pis = List.hd pis, List.tl pis in
let args = Subtac_utils.destruct_ex pi sumg in
let args =
diff --git a/contrib/subtac/subtac_interp_fixpoint.ml b/contrib/subtac/subtac_interp_fixpoint.ml
index 599dbe39..858fad1a 100644
--- a/contrib/subtac/subtac_interp_fixpoint.ml
+++ b/contrib/subtac/subtac_interp_fixpoint.ml
@@ -110,7 +110,7 @@ let rewrite_fixpoint env l (f, decl) =
let body =
(* cast or we will loose some info at pretyping time as body
is a function *)
- CCast (dummy_loc, body, DEFAULTcast, typ)
+ CCast (dummy_loc, body, CastConv DEFAULTcast, typ)
in
let body' = (* body abstracted by rec call *)
mkLambdaC ([(dummy_loc, Name id)], internal_type, body)
@@ -151,69 +151,3 @@ let rewrite_fixpoint env l (f, decl) =
Ppconstr.pr_constr_expr body')
in (id, (succ n, ro), bl', typ, body'), decl
-let list_mapi f =
- let rec aux i = function
- hd :: tl -> f i hd :: aux (succ i) tl
- | [] -> []
- in aux 0
-
-let rewrite_cases_aux (loc, po, tml, eqns) =
- let tml = list_mapi (fun i (c, (n, opt)) -> c,
- ((match n with
- Name id -> (match c with
- | RVar (_, id') when id = id' ->
- Name (id_of_string (string_of_id id ^ "'"))
- | _ -> n)
- | Anonymous -> Name (id_of_string ("x" ^ string_of_int i))),
- opt)) tml
- in
- let mkHole = RHole (dummy_loc, InternalHole) in
- let mkeq c n = RApp (dummy_loc, RRef (dummy_loc, (Lazy.force eqind_ref)),
- [mkHole; c; n])
- in
- let eqs_types =
- List.map
- (fun (c, (n, _)) ->
- let id = match n with Name id -> id | _ -> assert false in
- let heqid = id_of_string ("Heq" ^ string_of_id id) in
- Name heqid, mkeq c (RVar (dummy_loc, id)))
- tml
- in
- let po =
- List.fold_right
- (fun (n,t) acc ->
- RProd (dummy_loc, Anonymous, t, acc))
- eqs_types (match po with
- Some e -> e
- | None -> mkHole)
- in
- let eqns =
- List.map (fun (loc, idl, cpl, c) ->
- let c' =
- List.fold_left
- (fun acc (n, t) ->
- RLambda (dummy_loc, n, mkHole, acc))
- c eqs_types
- in (loc, idl, cpl, c'))
- eqns
- in
- let mk_refl_equal c = RApp (dummy_loc, RRef (dummy_loc, Lazy.force refl_equal_ref),
- [mkHole; c])
- in
- let refls = List.map (fun (c, _) -> mk_refl_equal c) tml in
- let case = RCases (loc,Some po,tml,eqns) in
- let app = RApp (dummy_loc, case, refls) in
- app
-
-let rec rewrite_cases c =
- match c with
- RCases _ -> let c' = map_rawconstr rewrite_cases c in
- (match c' with
- | RCases (x, y, z, w) -> rewrite_cases_aux (x,y,z,w)
- | _ -> assert(false))
- | _ -> map_rawconstr rewrite_cases c
-
-let rewrite_cases env c =
- let c' = rewrite_cases c in
- let _ = trace (str "Rewrote cases: " ++ spc () ++ my_print_rawconstr env c') in
- c'
diff --git a/contrib/subtac/subtac_interp_fixpoint.mli b/contrib/subtac/subtac_interp_fixpoint.mli
index b0de0641..fafbb2da 100644
--- a/contrib/subtac/subtac_interp_fixpoint.mli
+++ b/contrib/subtac/subtac_interp_fixpoint.mli
@@ -26,14 +26,3 @@ val rewrite_fixpoint :
Topconstr.local_binder list * Topconstr.constr_expr *
Topconstr.constr_expr) *
'c
-val list_mapi : (int -> 'a -> 'b) -> 'a list -> 'b list
-val rewrite_cases_aux :
- Util.loc * Rawterm.rawconstr option *
- (Rawterm.rawconstr *
- (Names.name * (Util.loc * Names.inductive * Names.name list) option))
- list *
- (Util.loc * Names.identifier list * Rawterm.cases_pattern list *
- Rawterm.rawconstr)
- list -> Rawterm.rawconstr
-
-val rewrite_cases : Environ.env -> Rawterm.rawconstr -> Rawterm.rawconstr
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index 104a0a58..261e0c5b 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 8688 2006-04-07 15:08:12Z msozeau $ *)
+(* $Id: subtac_pretyping.ml 8889 2006-06-01 20:23:56Z msozeau $ *)
open Global
open Pp
@@ -39,7 +39,7 @@ open Subtac_errors
open Context
open Eterm
-module Pretyping = Pretyping.Pretyping_F(Subtac_coercion.Coercion)
+module Pretyping = Subtac_pretyping_F.SubtacPretyping_F(Subtac_coercion.Coercion)
open Pretyping
@@ -116,24 +116,26 @@ let subtac_process env isevars id l c tycon =
let evars () = evars_of !isevars in
let _ = trace (str "Creating env with binders") in
let env_binders, binders_rel = env_with_binders env isevars l in
- let _ = trace (str "New env created:" ++ my_print_context env_binders) in
+ let _ = try (trace (str "New env created:" ++ my_print_context env_binders)) with _ -> () in
let tycon =
match tycon with
None -> empty_tycon
| Some t ->
let t = coqintern !isevars env_binders t in
- let _ = trace (str "Internalized specification: " ++ my_print_rawconstr env_binders t) in
+ let _ = try trace (str "Internalized specification: " ++ my_print_rawconstr env_binders t) with _ -> () in
let coqt, ttyp = interp env_binders isevars t empty_tycon in
- let _ = trace (str "Interpreted type: " ++ my_print_constr env_binders coqt) in
+ let _ = try trace (str "Interpreted type: " ++ my_print_constr env_binders coqt) with _ -> () in
mk_tycon coqt
in
let c = coqintern !isevars env_binders c in
- let _ = trace (str "Internalized term: " ++ my_print_rawconstr env c) in
+ let c = Subtac_utils.rewrite_cases env c in
+ let _ = try trace (str "Internalized term: " ++ my_print_rawconstr env c) with _ -> () in
let coqc, ctyp = interp env_binders isevars c tycon in
- let _ = trace (str "Interpreted term: " ++ my_print_constr env_binders coqc ++ spc () ++
+ let _ = try trace (str "Interpreted term: " ++ my_print_constr env_binders coqc ++ spc () ++
str "Coq type: " ++ my_print_constr env_binders ctyp)
+ with _ -> ()
in
- let _ = trace (str "Original evar map: " ++ Evd.pr_evar_map (evars ())) in
+ let _ = try trace (str "Original evar map: " ++ Evd.pr_evar_map (evars ())) with _ -> () in
let fullcoqc = it_mkLambda_or_LetIn coqc binders_rel
and fullctyp = it_mkProd_or_LetIn ctyp binders_rel
@@ -141,10 +143,11 @@ let subtac_process env isevars id l c tycon =
let fullcoqc = Evarutil.nf_evar (evars_of !isevars) fullcoqc in
let fullctyp = Evarutil.nf_evar (evars_of !isevars) fullctyp in
- let _ = trace (str "After evar normalization: " ++ spc () ++
+ let _ = try trace (str "After evar normalization: " ++ spc () ++
str "Coq term: " ++ my_print_constr env fullcoqc ++ spc ()
++ str "Coq type: " ++ my_print_constr env fullctyp)
+ with _ -> ()
in
let evm = non_instanciated_map env isevars in
- let _ = trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) in
+ let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in
evm, fullcoqc, fullctyp
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
new file mode 100644
index 00000000..65952750
--- /dev/null
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -0,0 +1,639 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+
+(* $Id: subtac_pretyping_F.ml 8889 2006-06-01 20:23:56Z msozeau $ *)
+
+open Pp
+open Util
+open Names
+open Sign
+open Evd
+open Term
+open Termops
+open Reductionops
+open Environ
+open Type_errors
+open Typeops
+open Libnames
+open Nameops
+open Classops
+open List
+open Recordops
+open Evarutil
+open Pretype_errors
+open Rawterm
+open Evarconv
+open Pattern
+open Dyn
+open Pretyping
+
+(************************************************************************)
+(* This concerns Cases *)
+open Declarations
+open Inductive
+open Inductiveops
+
+module SubtacPretyping_F (Coercion : Coercion.S) = struct
+
+ module Cases = Cases.Cases_F(Coercion)
+
+ (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
+ let allow_anonymous_refs = ref true
+
+ let evd_comb0 f isevars =
+ let (evd',x) = f !isevars in
+ isevars := evd';
+ x
+
+ let evd_comb1 f isevars x =
+ let (evd',y) = f !isevars x in
+ isevars := evd';
+ y
+
+ let evd_comb2 f isevars x y =
+ let (evd',z) = f !isevars x y in
+ isevars := evd';
+ z
+
+ let evd_comb3 f isevars x y z =
+ let (evd',t) = f !isevars x y z in
+ isevars := evd';
+ t
+
+ let mt_evd = Evd.empty
+
+ let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t)
+
+ (* Utilisé pour inférer le prédicat des Cases *)
+ (* Semble exagérement fort *)
+ (* Faudra préférer une unification entre les types de toutes les clauses *)
+ (* et autoriser des ? à rester dans le résultat de l'unification *)
+
+ let evar_type_fixpoint loc env isevars lna lar vdefj =
+ let lt = Array.length vdefj in
+ if Array.length lar = lt then
+ for i = 0 to lt-1 do
+ if not (e_cumul env isevars (vdefj.(i)).uj_type
+ (lift lt lar.(i))) then
+ error_ill_typed_rec_body_loc loc env (evars_of !isevars)
+ i lna vdefj lar
+ done
+
+ let check_branches_message loc env isevars c (explft,lft) =
+ for i = 0 to Array.length explft - 1 do
+ if not (e_cumul env isevars lft.(i) explft.(i)) then
+ let sigma = evars_of !isevars in
+ error_ill_formed_branch_loc loc env sigma c i lft.(i) explft.(i)
+ done
+
+ (* coerce to tycon if any *)
+ let inh_conv_coerce_to_tycon loc env isevars j = function
+ | None -> j
+ | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) isevars j t
+
+ let push_rels vars env = List.fold_right push_rel vars env
+
+ (*
+ let evar_type_case isevars env ct pt lft p c =
+ let (mind,bty,rslty) = type_case_branches env (evars_of isevars) ct pt p c
+ in check_branches_message isevars env (c,ct) (bty,lft); (mind,rslty)
+ *)
+
+ let strip_meta id = (* For Grammar v7 compatibility *)
+ let s = string_of_id id in
+ if s.[0]='$' then id_of_string (String.sub s 1 (String.length s - 1))
+ else id
+
+ let pretype_id loc env (lvar,unbndltacvars) id =
+ let id = strip_meta id in (* May happen in tactics defined by Grammar *)
+ try
+ let (n,typ) = lookup_rel_id id (rel_context env) in
+ { uj_val = mkRel n; uj_type = type_app (lift n) typ }
+ with Not_found ->
+ try
+ List.assoc id lvar
+ with Not_found ->
+ try
+ let (_,_,typ) = lookup_named id env in
+ { uj_val = mkVar id; uj_type = typ }
+ with Not_found ->
+ try (* To build a nicer ltac error message *)
+ match List.assoc id unbndltacvars with
+ | None -> user_err_loc (loc,"",
+ str "variable " ++ pr_id id ++ str " should be bound to a term")
+ | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0
+ with Not_found ->
+ error_var_not_found_loc loc id
+
+ (* make a dependent predicate from an undependent one *)
+
+ let make_dep_of_undep env (IndType (indf,realargs)) pj =
+ let n = List.length realargs in
+ let rec decomp n p =
+ if n=0 then p else
+ match kind_of_term p with
+ | Lambda (_,_,c) -> decomp (n-1) c
+ | _ -> decomp (n-1) (applist (lift 1 p, [mkRel 1]))
+ in
+ let sign,s = decompose_prod_n n pj.uj_type in
+ let ind = build_dependent_inductive env indf in
+ let s' = mkProd (Anonymous, ind, s) in
+ let ccl = lift 1 (decomp n pj.uj_val) in
+ let ccl' = mkLambda (Anonymous, ind, ccl) in
+ {uj_val=lam_it ccl' sign; uj_type=prod_it s' sign}
+
+ (*************************************************************************)
+ (* Main pretyping function *)
+
+ let pretype_ref isevars env ref =
+ let c = constr_of_global ref in
+ make_judge c (Retyping.get_type_of env Evd.empty c)
+
+ let pretype_sort = function
+ | RProp c -> judge_of_prop_contents c
+ | RType _ -> judge_of_new_Type ()
+
+ (* [pretype tycon env isevars lvar lmeta cstr] attempts to type [cstr] *)
+ (* in environment [env], with existential variables [(evars_of isevars)] and *)
+ (* the type constraint tycon *)
+ let rec pretype (tycon : type_constraint) env isevars lvar = function
+ | RRef (loc,ref) ->
+ inh_conv_coerce_to_tycon loc env isevars
+ (pretype_ref isevars env ref)
+ tycon
+
+ | RVar (loc, id) ->
+ inh_conv_coerce_to_tycon loc env isevars
+ (pretype_id loc env lvar id)
+ tycon
+
+ | REvar (loc, ev, instopt) ->
+ (* Ne faudrait-il pas s'assurer que hyps est bien un
+ sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *)
+ let hyps = evar_context (Evd.find (evars_of !isevars) ev) in
+ let args = match instopt with
+ | None -> instance_from_named_context hyps
+ | Some inst -> failwith "Evar subtitutions not implemented" in
+ let c = mkEvar (ev, args) in
+ let j = (Retyping.get_judgment_of env (evars_of !isevars) c) in
+ inh_conv_coerce_to_tycon loc env isevars j tycon
+
+ | RPatVar (loc,(someta,n)) ->
+ anomaly "Found a pattern variable in a rawterm to type"
+
+ | RHole (loc,k) ->
+ let ty =
+ match tycon with
+ | Some (None, ty) -> ty
+ | None | Some _ ->
+ e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ()) in
+ { uj_val = e_new_evar isevars env ~src:(loc,k) ty; uj_type = ty }
+
+ | RRec (loc,fixkind,names,bl,lar,vdef) ->
+ let rec type_bl env ctxt = function
+ [] -> ctxt
+ | (na,None,ty)::bl ->
+ let ty' = pretype_type empty_valcon env isevars lvar ty in
+ let dcl = (na,None,ty'.utj_val) in
+ type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl
+ | (na,Some bd,ty)::bl ->
+ let ty' = pretype_type empty_valcon env isevars lvar ty in
+ let bd' = pretype (mk_tycon ty'.utj_val) env isevars lvar ty in
+ let dcl = (na,Some bd'.uj_val,ty'.utj_val) in
+ type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl in
+ let ctxtv = Array.map (type_bl env empty_rel_context) bl in
+ let larj =
+ array_map2
+ (fun e ar ->
+ pretype_type empty_valcon (push_rel_context e env) isevars lvar ar)
+ ctxtv lar in
+ let lara = Array.map (fun a -> a.utj_val) larj in
+ let ftys = array_map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in
+ let nbfix = Array.length lar in
+ let names = Array.map (fun id -> Name id) names in
+ (* Note: bodies are not used by push_rec_types, so [||] is safe *)
+ let newenv = push_rec_types (names,ftys,[||]) env in
+ let vdefj =
+ array_map2_i
+ (fun i ctxt def ->
+ (* we lift nbfix times the type in tycon, because of
+ * the nbfix variables pushed to newenv *)
+ let (ctxt,ty) =
+ decompose_prod_n_assum (rel_context_length ctxt)
+ (lift nbfix ftys.(i)) in
+ let nenv = push_rel_context ctxt newenv in
+ let j = pretype (mk_tycon ty) nenv isevars lvar def in
+ { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
+ uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
+ ctxtv vdef in
+ evar_type_fixpoint loc env isevars names ftys vdefj;
+ let fixj = match fixkind with
+ | RFix (vn,i) ->
+ let guard_indexes = Array.mapi
+ (fun i (n,_) -> match n with
+ | Some n -> n
+ | None ->
+ (* Recursive argument was not given by the user : We
+ check that there is only one inductive argument *)
+ let ctx = ctxtv.(i) in
+ let isIndApp t =
+ isInd (fst (decompose_app (strip_head_cast t))) in
+ (* This could be more precise (e.g. do some delta) *)
+ let lb = List.rev_map (fun (_,_,t) -> isIndApp t) ctx in
+ try (list_unique_index true lb) - 1
+ with Not_found ->
+ Util.user_err_loc
+ (loc,"pretype",
+ Pp.str "cannot guess decreasing argument of fix"))
+ vn
+ in
+ let fix = ((guard_indexes, i),(names,ftys,Array.map j_val vdefj)) in
+ (try check_fix env fix with e -> Stdpp.raise_with_loc loc e);
+ make_judge (mkFix fix) ftys.(i)
+ | RCoFix i ->
+ let cofix = (i,(names,ftys,Array.map j_val vdefj)) in
+ (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e);
+ make_judge (mkCoFix cofix) ftys.(i) in
+ inh_conv_coerce_to_tycon loc env isevars fixj tycon
+
+ | RSort (loc,s) ->
+ inh_conv_coerce_to_tycon loc env isevars (pretype_sort s) tycon
+
+ | RApp (loc,f,args) ->
+ let length = List.length args in
+ let ftycon =
+ match tycon with
+ None -> None
+ | Some (None, ty) -> mk_abstr_tycon length ty
+ | Some (Some (init, cur), ty) ->
+ Some (Some (length + init, length + cur), ty)
+ in
+ let fj = pretype ftycon env isevars lvar f in
+ let floc = loc_of_rawconstr f in
+ let rec apply_rec env n resj tycon = function
+ | [] -> resj
+ | c::rest ->
+ let argloc = loc_of_rawconstr c in
+ let resj = evd_comb1 (Coercion.inh_app_fun env) isevars resj in
+ let resty = whd_betadeltaiota env (evars_of !isevars) resj.uj_type in
+ match kind_of_term resty with
+ | Prod (na,c1,c2) ->
+ let hj = pretype (mk_tycon c1) env isevars lvar c in
+ let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in
+ let typ' = nf_isevar !isevars typ in
+ let tycon =
+ option_map
+ (fun (abs, ty) ->
+ match abs with
+ None ->
+ isevars := Coercion.inh_conv_coerces_to loc env !isevars typ'
+ (abs, ty);
+ (abs, ty)
+ | Some (init, cur) ->
+ isevars := Coercion.inh_conv_coerces_to loc env !isevars typ'
+ (abs, ty);
+ (Some (init, pred cur), ty))
+ tycon
+ in
+ apply_rec env (n+1)
+ { uj_val = nf_isevar !isevars value;
+ uj_type = nf_isevar !isevars typ' }
+ (option_map (fun (abs, c) -> abs, nf_isevar !isevars c) tycon) rest
+
+ | _ ->
+ let hj = pretype empty_tycon env isevars lvar c in
+ error_cant_apply_not_functional_loc
+ (join_loc floc argloc) env (evars_of !isevars)
+ resj [hj]
+ in
+ let ftycon = option_map (lift_abstr_tycon_type (-1)) ftycon in
+ 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 ->
+ 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 *)
+ | _ -> resj in
+ inh_conv_coerce_to_tycon loc env isevars resj tycon
+
+ | RLambda(loc,name,c1,c2) ->
+ let (name',dom,rng) = evd_comb1 (split_tycon loc env) isevars tycon in
+ let dom_valcon = valcon_of_tycon dom in
+ let j = pretype_type dom_valcon env isevars lvar c1 in
+ let var = (name,None,j.utj_val) in
+ let j' = pretype rng (push_rel var env) isevars lvar c2 in
+ judge_of_abstraction env name j j'
+
+ | RProd(loc,name,c1,c2) ->
+ let j = pretype_type empty_valcon env isevars lvar c1 in
+ let var = (name,j.utj_val) in
+ let env' = push_rel_assum var env in
+ let j' = pretype_type empty_valcon env' isevars lvar c2 in
+ let resj =
+ try judge_of_product env name j j'
+ with TypeError _ as e -> Stdpp.raise_with_loc loc e in
+ inh_conv_coerce_to_tycon loc env isevars resj tycon
+
+ | RLetIn(loc,name,c1,c2) ->
+ let j = pretype empty_tycon env isevars lvar c1 in
+ let t = refresh_universes j.uj_type in
+ let var = (name,Some j.uj_val,t) in
+ let tycon = lift_tycon 1 tycon in
+ let j' = pretype tycon (push_rel var env) isevars lvar c2 in
+ { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
+ uj_type = subst1 j.uj_val j'.uj_type }
+
+ | RLetTuple (loc,nal,(na,po),c,d) ->
+ let cj = pretype empty_tycon env isevars lvar c in
+ let (IndType (indf,realargs)) =
+ try find_rectype env (evars_of !isevars) cj.uj_type
+ with Not_found ->
+ let cloc = loc_of_rawconstr c in
+ error_case_not_inductive_loc cloc env (evars_of !isevars) cj
+ in
+ let cstrs = get_constructors env indf in
+ if Array.length cstrs <> 1 then
+ user_err_loc (loc,"",str "Destructing let is only for inductive types with one constructor");
+ let cs = cstrs.(0) in
+ if List.length nal <> cs.cs_nargs then
+ user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables");
+ let fsign = List.map2 (fun na (_,c,t) -> (na,c,t))
+ (List.rev nal) cs.cs_args in
+ let env_f = push_rels fsign env in
+ (* Make dependencies from arity signature impossible *)
+ let arsgn =
+ let arsgn,_ = get_arity env indf in
+ if not !allow_anonymous_refs then
+ List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn
+ else arsgn
+ in
+ let psign = (na,None,build_dependent_inductive env indf)::arsgn in
+ let nar = List.length arsgn in
+ (match po with
+ | Some p ->
+ let env_p = push_rels psign env in
+ let pj = pretype_type empty_valcon env_p isevars lvar p in
+ let ccl = nf_evar (evars_of !isevars) pj.utj_val in
+ let psign = make_arity_signature env true indf in (* with names *)
+ let p = it_mkLambda_or_LetIn ccl psign in
+ let inst =
+ (Array.to_list cs.cs_concl_realargs)
+ @[build_dependent_constructor cs] in
+ let lp = lift cs.cs_nargs p in
+ let fty = hnf_lam_applist env (evars_of !isevars) lp inst in
+ let fj = pretype (mk_tycon fty) env_f isevars lvar d in
+ let f = it_mkLambda_or_LetIn fj.uj_val fsign in
+ let v =
+ let mis,_ = dest_ind_family indf in
+ let ci = make_default_case_info env LetStyle mis in
+ mkCase (ci, p, cj.uj_val,[|f|]) in
+ { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl }
+
+ | None ->
+ let tycon = lift_tycon cs.cs_nargs tycon in
+ let fj = pretype tycon env_f isevars lvar d in
+ let f = it_mkLambda_or_LetIn fj.uj_val fsign in
+ let ccl = nf_evar (evars_of !isevars) fj.uj_type in
+ let ccl =
+ if noccur_between 1 cs.cs_nargs ccl then
+ lift (- cs.cs_nargs) ccl
+ else
+ error_cant_find_case_type_loc loc env (evars_of !isevars)
+ cj.uj_val in
+ let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
+ let v =
+ let mis,_ = dest_ind_family indf in
+ let ci = make_default_case_info env LetStyle mis in
+ mkCase (ci, p, cj.uj_val,[|f|] )
+ in
+ { uj_val = v; uj_type = ccl })
+
+ | RIf (loc,c,(na,po),b1,b2) ->
+ let cj = pretype empty_tycon env isevars lvar c in
+ let (IndType (indf,realargs)) =
+ try find_rectype env (evars_of !isevars) cj.uj_type
+ with Not_found ->
+ let cloc = loc_of_rawconstr c in
+ error_case_not_inductive_loc cloc env (evars_of !isevars) cj in
+ let cstrs = get_constructors env indf in
+ if Array.length cstrs <> 2 then
+ user_err_loc (loc,"",
+ str "If is only for inductive types with two constructors");
+
+ let arsgn =
+ let arsgn,_ = get_arity env indf in
+ if not !allow_anonymous_refs then
+ (* Make dependencies from arity signature impossible *)
+ List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn
+ else arsgn
+ in
+ let nar = List.length arsgn in
+ let psign = (na,None,build_dependent_inductive env indf)::arsgn in
+ let pred,p = match po with
+ | Some p ->
+ let env_p = push_rels psign env in
+ let pj = pretype_type empty_valcon env_p isevars lvar p in
+ let ccl = nf_evar (evars_of !isevars) pj.utj_val in
+ let pred = it_mkLambda_or_LetIn ccl psign in
+ let typ = lift (- nar) (beta_applist (pred,[cj.uj_val])) in
+ let jtyp = inh_conv_coerce_to_tycon loc env isevars {uj_val = pred;
+ uj_type = typ} tycon
+ in
+ jtyp.uj_val, jtyp.uj_type
+ | None ->
+ let p = match tycon with
+ | Some (None, ty) -> ty
+ | None | Some _ ->
+ e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ())
+ in
+ it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
+ let pred = nf_evar (evars_of !isevars) pred in
+ let p = nf_evar (evars_of !isevars) p in
+ (* msgnl (str "Pred is: " ++ Termops.print_constr_env env pred);*)
+ let f cs b =
+ let n = rel_context_length cs.cs_args in
+ let pi = lift n pred in (* liftn n 2 pred ? *)
+ let pi = beta_applist (pi, [build_dependent_constructor cs]) in
+ let csgn =
+ if not !allow_anonymous_refs then
+ List.map (fun (_,b,t) -> (Anonymous,b,t)) cs.cs_args
+ else
+ List.map
+ (fun (n, b, t) ->
+ match n with
+ Name _ -> (n, b, t)
+ | Anonymous -> (Name (id_of_string "H"), b, t))
+ cs.cs_args
+ in
+ let env_c = push_rels csgn env in
+(* msgnl (str "Pi is: " ++ Termops.print_constr_env env_c pi); *)
+ let bj = pretype (mk_tycon pi) env_c isevars lvar b in
+ it_mkLambda_or_LetIn bj.uj_val cs.cs_args in
+ let b1 = f cstrs.(0) b1 in
+ let b2 = f cstrs.(1) b2 in
+ let v =
+ let mis,_ = dest_ind_family indf in
+ let ci = make_default_case_info env IfStyle mis in
+ mkCase (ci, pred, cj.uj_val, [|b1;b2|])
+ in
+ { uj_val = v; uj_type = p }
+
+ | RCases (loc,po,tml,eqns) ->
+ Cases.compile_cases loc
+ ((fun vtyc env -> pretype vtyc env isevars lvar),isevars)
+ tycon env (* loc *) (po,tml,eqns)
+
+ | RCast(loc,c,k,t) ->
+ let cj =
+ match k with
+ CastCoerce ->
+ let cj = pretype empty_tycon env isevars lvar c in
+ evd_comb1 (Coercion.inh_coerce_to_base loc env) isevars cj
+ | CastConv k ->
+ let tj = pretype_type empty_valcon env isevars lvar t in
+ let cj = pretype (mk_tycon tj.utj_val) env isevars lvar c in
+ (* User Casts are for helping pretyping, experimentally not to be kept*)
+ (* ... except for Correctness *)
+ let v = mkCast (cj.uj_val, k, tj.utj_val) in
+ { uj_val = v; uj_type = tj.utj_val }
+ in
+ inh_conv_coerce_to_tycon loc env isevars cj tycon
+
+ | RDynamic (loc,d) ->
+ if (tag d) = "constr" then
+ let c = constr_out d in
+ let j = (Retyping.get_judgment_of env (evars_of !isevars) c) in
+ j
+ (*inh_conv_coerce_to_tycon loc env isevars j tycon*)
+ else
+ user_err_loc (loc,"pretype",(str "Not a constr tagged Dynamic"))
+
+ (* [pretype_type valcon env isevars lvar c] coerces [c] into a type *)
+ and pretype_type valcon env isevars lvar = function
+ | RHole loc ->
+ (match valcon with
+ | Some v ->
+ let s =
+ let sigma = evars_of !isevars in
+ let t = Retyping.get_type_of env sigma v in
+ match kind_of_term (whd_betadeltaiota env sigma t) with
+ | Sort s -> s
+ | Evar v when is_Type (existential_type sigma v) ->
+ evd_comb1 (define_evar_as_sort) isevars v
+ | _ -> anomaly "Found a type constraint which is not a type"
+ in
+ { utj_val = v;
+ utj_type = s }
+ | None ->
+ let s = new_Type_sort () in
+ { utj_val = e_new_evar isevars env ~src:loc (mkSort s);
+ utj_type = s})
+ | c ->
+ let j = pretype empty_tycon env isevars lvar c in
+ let loc = loc_of_rawconstr c in
+ let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) isevars j in
+ match valcon with
+ | None -> tj
+ | Some v ->
+ if e_cumul env isevars v tj.utj_val then tj
+ else
+ error_unexpected_type_loc
+ (loc_of_rawconstr c) env (evars_of !isevars) tj.utj_val v
+
+ let pretype_gen isevars env lvar kind c =
+ let c' = match kind with
+ | OfType exptyp ->
+ let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
+ (pretype tycon env isevars lvar c).uj_val
+ | IsType ->
+ (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...
+ *)
+
+ let understand_judgment sigma env c =
+ 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
+ check_evars env sigma isevars (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
+ j
+
+ let understand_judgment_tcc isevars env c =
+ let j = pretype empty_tycon env isevars ([],[]) c in
+ let sigma = evars_of !isevars in
+ let j = j_nf_evar sigma j in
+ j
+
+ (* Raw calls to the unsafe inference machine: boolean says if we must
+ fail on unresolved evars; the unsafe_judgment list allows us to
+ extend env with some bindings *)
+
+ 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
+ if fail_evar then check_evars env sigma isevars c;
+ !isevars, c
+
+ (** Entry points of the high-level type synthesis algorithm *)
+
+ let understand_gen kind sigma env c =
+ snd (ise_pretype_gen true sigma env ([],[]) kind c)
+
+ let understand sigma env ?expected_type:exptyp c =
+ snd (ise_pretype_gen true sigma env ([],[]) (OfType exptyp) c)
+
+ let understand_type sigma env c =
+ snd (ise_pretype_gen true sigma env ([],[]) IsType c)
+
+ let understand_ltac sigma env lvar kind c =
+ ise_pretype_gen false sigma env lvar kind c
+
+ let understand_tcc_evars isevars env kind c =
+ pretype_gen isevars env ([],[]) kind c
+
+ let understand_tcc sigma env ?expected_type:exptyp c =
+ let ev, t = ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c in
+ Evd.evars_of ev, t
+end
+
+module Default : S = SubtacPretyping_F(Coercion.Default)
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 6c165dad..59c858a6 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -57,7 +57,7 @@ let natind = lazy (init_constant ["Init"; "Datatypes"] "nat")
let intind = lazy (init_constant ["ZArith"; "binint"] "Z")
let existSind = lazy (init_constant ["Init"; "Specif"] "sigS")
-let existS = lazy (build_sigma_set ())
+let existS = lazy (build_sigma_type ())
let prod = lazy (build_prod ())
@@ -118,8 +118,8 @@ let print_args env args =
let make_existential loc env isevars c =
let evar = Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark) c in
let (key, args) = destEvar evar in
- debug 2 (str "Constructed evar " ++ int key ++ str " applied to args: " ++
- print_args env args);
+ (try debug 2 (str "Constructed evar " ++ int key ++ str " applied to args: " ++
+ print_args env args) with _ -> ());
evar
let make_existential_expr loc env c =
@@ -160,26 +160,27 @@ open Tactics
open Tacticals
let build_dependent_sum l =
- let rec aux (acc, tac, typ) = function
+ let rec aux (tac, typ) = function
(n, t) :: tl ->
let t' = mkLambda (Name n, t, typ) in
- trace (str ("treating " ^ string_of_id n) ++
- str "assert: " ++ my_print_constr (Global.env ()) t);
+ trace (spc () ++ str ("treating evar " ^ string_of_id n));
+ (try trace (str " assert: " ++ my_print_constr (Global.env ()) t)
+ with _ -> ());
let tac' =
- tclTHEN (assert_tac true (Name n) t)
- (tclTHENLIST
- [intros;
- (tclTHENSEQ
- [tclTRY (constructor_tac (Some 1) 1
- (Rawterm.ImplicitBindings [mkVar n]));
- tac]);
- ])
+ tclTHENS (assert_tac true (Name n) t)
+ ([intros;
+ (tclTHENSEQ
+ [constructor_tac (Some 1) 1
+ (Rawterm.ImplicitBindings [mkVar n]);
+ tac]);
+ ])
in
- aux (mkApp (Lazy.force ex_ind, [| t; t'; |]), tac', t') tl
- | [] -> acc, tac, typ
+ let newt = mkApp (Lazy.force ex_ind, [| t; t'; |]) in
+ aux (tac', newt) tl
+ | [] -> tac, typ
in
match l with
- (_, hd) :: tl -> aux (hd, intros, hd) tl
+ (_, hd) :: tl -> aux (intros, hd) tl
| [] -> raise (Invalid_argument "build_dependent_sum")
open Proof_type
@@ -218,7 +219,8 @@ let and_tac l hook =
let and_proof_id, and_goal, and_tac, and_extract =
match l with
| [] -> raise (Invalid_argument "and_tac: empty list of goals")
- | (hdid, x, hdg, hdt) :: tl -> aux (string_of_id hdid, hdg, hdt, [hdid, x, hdg, (fun c -> c)]) tl
+ | (hdid, x, hdg, hdt) :: tl ->
+ aux (string_of_id hdid, hdg, hdt, [hdid, x, hdg, (fun c -> c)]) tl
in
let and_proofid = id_of_string (and_proof_id ^ "_and_proof") in
Command.start_proof and_proofid goal_kind and_goal
@@ -238,9 +240,91 @@ let destruct_ex ext ex =
try (args.(0), args.(1))
with _ -> assert(false)
in
- (mk_ex_pi1 dom rng acc) :: aux rng (mk_ex_pi2 dom rng acc)
+ let pi1 = (mk_ex_pi1 dom rng acc) in
+ let rng_body =
+ match kind_of_term rng with
+ Lambda (_, _, t) -> subst1 pi1 t
+ | t -> rng
+ in
+ pi1 :: aux rng_body (mk_ex_pi2 dom rng acc)
| _ -> [acc])
| _ -> [acc]
in aux ex ext
+let list_mapi f =
+ let rec aux i = function
+ hd :: tl -> f i hd :: aux (succ i) tl
+ | [] -> []
+ in aux 0
+
+open Rawterm
+
+let rewrite_cases_aux (loc, po, tml, eqns) =
+ let tml' = list_mapi (fun i (c, (n, opt)) -> c,
+ ((match n with
+ Name id -> (match c with
+ | RVar (_, id') when id = id' ->
+ id, (id_of_string (string_of_id id ^ "Heq_id"))
+ | RVar (_, id') ->
+ id', id
+ | _ -> id_of_string (string_of_id id ^ "Heq_id"), id)
+ | Anonymous ->
+ let str = "Heq_id" ^ string_of_int i in
+ id_of_string str, id_of_string (str ^ "'")),
+ opt)) tml
+ in
+ let mkHole = RHole (dummy_loc, InternalHole) in
+ let mkCoerceCast c = RCast (dummy_loc, c, CastCoerce, mkHole) in
+ let mkeq c n = RApp (dummy_loc, RRef (dummy_loc, (Lazy.force eqind_ref)),
+ [mkHole; c; n])
+ in
+ let eqs_types =
+ List.map
+ (fun (c, ((id, id'), _)) ->
+ let heqid = id_of_string ("Heq" ^ string_of_id id) in
+ Name heqid, mkeq (RVar (dummy_loc, id')) c)
+ tml'
+ in
+ let po =
+ List.fold_right
+ (fun (n,t) acc ->
+ RProd (dummy_loc, Anonymous, t, acc))
+ eqs_types (match po with
+ Some e -> e
+ | None -> mkHole)
+ in
+ let eqns =
+ List.map (fun (loc, idl, cpl, c) ->
+ let c' =
+ List.fold_left
+ (fun acc (n, t) ->
+ RLambda (dummy_loc, n, mkHole, acc))
+ c eqs_types
+ in (loc, idl, cpl, c'))
+ eqns
+ in
+ let mk_refl_equal c = RApp (dummy_loc, RRef (dummy_loc, Lazy.force refl_equal_ref),
+ [mkHole; c])
+ in
+ let refls = List.map (fun (c, ((id, _), _)) -> mk_refl_equal (mkCoerceCast c)) tml' in
+ let tml'' = List.map (fun (c, ((id, id'), opt)) -> c, (Name id', opt)) tml' in
+ let case = RCases (loc,Some po,tml'',eqns) in
+ let app = RApp (dummy_loc, case, refls) in
+(* let letapp = List.fold_left (fun acc (c, ((id, id'), opt)) -> RLetIn (dummy_loc, Name id, c, acc)) *)
+(* app tml' *)
+(* in *)
+ app
+
+let rec rewrite_cases c =
+ match c with
+ RCases _ -> let c' = map_rawconstr rewrite_cases c in
+ (match c' with
+ | RCases (x, y, z, w) -> rewrite_cases_aux (x,y,z,w)
+ | _ -> assert(false))
+ | _ -> map_rawconstr rewrite_cases c
+
+let rewrite_cases env c =
+ let c' = rewrite_cases c in
+ let _ = trace (str "Rewrote cases: " ++ spc () ++ my_print_rawconstr env c') in
+ c'
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index 92a995c8..a90f281f 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -78,8 +78,10 @@ val mkProj1 : constr -> constr -> constr -> constr
val mk_ex_pi1 : constr -> constr -> constr -> constr
val mk_ex_pi1 : constr -> constr -> constr -> constr
-val build_dependent_sum : (identifier * types) list -> constr * Proof_type.tactic * types
+val build_dependent_sum : (identifier * types) list -> Proof_type.tactic * types
val and_tac : (identifier * 'a * constr * Proof_type.tactic) list ->
((constr -> (identifier * 'a * constr * constr) list) -> Tacexpr.declaration_hook) -> unit
val destruct_ex : constr -> constr -> constr list
+
+val rewrite_cases : Environ.env -> Rawterm.rawconstr -> Rawterm.rawconstr
diff --git a/contrib/subtac/test/ListsTest.v b/contrib/subtac/test/ListsTest.v
new file mode 100644
index 00000000..a29cd039
--- /dev/null
+++ b/contrib/subtac/test/ListsTest.v
@@ -0,0 +1,95 @@
+Require Import Coq.subtac.Utils.
+Require Import List.
+
+Variable A : Set.
+
+Program Definition myhd : forall { l : list A | length l <> 0 }, A :=
+ fun l =>
+ match l with
+ | nil => _
+ | hd :: tl => hd
+ end.
+Proof.
+ destruct l ; simpl ; intro H ; rewrite <- H in n ; intuition.
+Defined.
+
+
+Extraction myhd.
+Extraction Inline proj1_sig.
+
+Program Definition mytail : forall { l : list A | length l <> 0 }, list A :=
+ fun l =>
+ match l with
+ | nil => _
+ | hd :: tl => tl
+ end.
+Proof.
+destruct l ; simpl ; intro H ; rewrite <- H in n ; intuition.
+Defined.
+
+Extraction mytail.
+
+Variable a : A.
+
+Program Definition test_hd : A := myhd (cons a nil).
+Proof.
+simpl ; auto.
+Defined.
+
+Extraction test_hd.
+
+(*Program Definition test_tail : list A := mytail nil.*)
+
+
+
+
+
+Program Fixpoint append (l : list A) (l' : list A) { struct l } :
+ { r : list A | length r = length l + length l' } :=
+ match l with
+ | nil => l'
+ | hd :: tl => hd :: (append tl l')
+ end.
+simpl.
+subst ; auto.
+simpl ; rewrite (subset_simpl (append tl0 l')).
+simpl ; subst.
+simpl ; auto.
+Defined.
+
+Extraction append.
+
+
+Program Lemma append_app' : forall l : list A, l = append nil l.
+Proof.
+simpl ; auto.
+Qed.
+
+Program Lemma append_app : forall l : list A, l = append l nil.
+Proof.
+intros.
+induction l ; simpl ; auto.
+simpl in IHl.
+rewrite <- IHl.
+reflexivity.
+Qed.
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/contrib/subtac/test/Mutind.v b/contrib/subtac/test/Mutind.v
new file mode 100644
index 00000000..ab200354
--- /dev/null
+++ b/contrib/subtac/test/Mutind.v
@@ -0,0 +1,7 @@
+Fixpoint f (a : nat) : nat := match a with 0 => 0
+| S a' => g a a'
+ end
+with g (a b : nat) { struct b } : nat :=
+ match b with 0 => 0
+ | S b' => f b'
+ end. \ No newline at end of file
diff --git a/contrib/subtac/test/Test1.v b/contrib/subtac/test/Test1.v
new file mode 100644
index 00000000..14b80854
--- /dev/null
+++ b/contrib/subtac/test/Test1.v
@@ -0,0 +1,16 @@
+Program Definition test (a b : nat) : { x : nat | x = a + b } :=
+ ((a + b) : { x : nat | x = a + b }).
+Proof.
+intros.
+reflexivity.
+Qed.
+
+Print test.
+
+Require Import List.
+
+Program hd_opt (l : list nat) : { x : nat | x <> 0 } :=
+ match l with
+ nil => 1
+ | a :: l => a
+ end.
diff --git a/contrib/subtac/test/euclid.v b/contrib/subtac/test/euclid.v
new file mode 100644
index 00000000..481b6708
--- /dev/null
+++ b/contrib/subtac/test/euclid.v
@@ -0,0 +1,66 @@
+
+Notation "( x & y )" := (@existS _ _ x y) : core_scope.
+Unset Printing All.
+
+Definition t := fun (Evar46 : forall a : nat, (fun y : nat => @eq nat a y) a) (a : nat) =>
+@existS nat (fun x : nat => @sig nat (fun y : nat => @eq nat x y)) a
+ (@exist nat (fun y : nat => @eq nat a y) a (Evar46 a)).
+
+Program Definition testsig (a : nat) : { x : nat & { y : nat | x = y } } :=
+ (a & a).
+reflexivity.
+Defined.
+
+Extraction testsig.
+Extraction sigS.
+Extract Inductive sigS => "" [ "" ].
+Extraction testsig.
+
+Require Import Coq.Arith.Compare_dec.
+
+Require Import Omega.
+
+Lemma minus_eq_add : forall x y z w, y <= x -> x - y = y * z + w -> x = y * S z + w.
+intros.
+assert(y * S z = y * z + y).
+auto.
+rewrite H1.
+omega.
+Qed.
+
+Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf a lt} :
+ { q : nat & { r : nat | a = b * q + r /\ r < b } } :=
+ if le_lt_dec b a then let (q', r) := euclid (a - b) b in
+ (S q' & r)
+ else (O & a).
+intro euclid.
+simpl ; intros.
+Print euclid_evars.
+eapply euclid_evars with euclid.
+refine (euclid_evars _ _ _ euclid a Acc_a b).
+; simpl ; intros.
+Show Existentials.
+
+induction b0 ; induction r.
+simpl in H.
+simpl.
+simpl in p0.
+destruct p0.
+split.
+
+apply minus_eq_add.
+omega.
+auto with arith.
+auto.
+simpl.
+induction b0 ; simpl.
+split ; auto.
+omega.
+exact (euclid a0 Acc_a0 b0).
+
+exact (Acc_a).
+auto.
+auto.
+Focus 1.
+
+
diff --git a/contrib/subtac/test/id.v b/contrib/subtac/test/id.v
new file mode 100644
index 00000000..9ae11088
--- /dev/null
+++ b/contrib/subtac/test/id.v
@@ -0,0 +1,46 @@
+Require Coq.Arith.Arith.
+
+Require Import Coq.subtac.Utils.
+Program Fixpoint id (n : nat) : { x : nat | x = n } :=
+ match n with
+ | O => O
+ | S p => S (id p)
+ end.
+intros ; auto.
+
+pose (subset_simpl (id p)).
+simpl in e.
+unfold p0.
+rewrite e.
+auto.
+Defined.
+
+Check id.
+Print id.
+Extraction id.
+
+Axiom le_gt_dec : forall n m, { n <= m } + { n > m }.
+Require Import Omega.
+
+Program Fixpoint id_if (n : nat) { wf n lt }: { x : nat | x = n } :=
+ if le_gt_dec n 0 then 0
+ else S (id_if (pred n)).
+intros.
+auto with arith.
+intros.
+pose (subset_simpl (id_if (pred n))).
+simpl in e.
+rewrite e.
+induction n ; auto with arith.
+Defined.
+
+Print id_if_instance.
+Extraction id_if_instance.
+
+Notation "( x & y )" := (@existS _ _ x y) : core_scope.
+
+Program Definition testsig ( a : nat ) : { x : nat & { y : nat | x = y }} :=
+ (a & a).
+intros.
+auto.
+Qed.
diff --git a/contrib/subtac/test/rec.v b/contrib/subtac/test/rec.v
new file mode 100644
index 00000000..aaefd8cc
--- /dev/null
+++ b/contrib/subtac/test/rec.v
@@ -0,0 +1,65 @@
+Require Import Coq.Arith.Arith.
+Require Import Lt.
+Require Import Omega.
+
+Axiom lt_ge_dec : forall x y : nat, { x < y } + { x >= y }.
+(*Proof.
+ intros.
+ elim (le_lt_dec y x) ; intros ; auto with arith.
+Defined.
+*)
+Require Import Coq.subtac.FixSub.
+Require Import Wf_nat.
+
+Lemma preda_lt_a : forall a, 0 < a -> pred a < a.
+auto with arith.
+Qed.
+
+Program Fixpoint id_struct (a : nat) : nat :=
+ match a with
+ 0 => 0
+ | S n => S (id_struct n)
+ end.
+
+Check struct_rec.
+
+ if (lt_ge_dec O a)
+ then S (wfrec (pred a))
+ else O.
+
+Program Fixpoint wfrec (a : nat) { wf a lt } : nat :=
+ if (lt_ge_dec O a)
+ then S (wfrec (pred a))
+ else O.
+intros.
+apply preda_lt_a ; auto.
+
+Defined.
+
+Extraction wfrec.
+Extraction Inline proj1_sig.
+Extract Inductive bool => "bool" [ "true" "false" ].
+Extract Inductive sumbool => "bool" [ "true" "false" ].
+Extract Inlined Constant lt_ge_dec => "<".
+
+Extraction wfrec.
+Extraction Inline lt_ge_dec le_lt_dec.
+Extraction wfrec.
+
+
+Program Fixpoint structrec (a : nat) { wf a lt } : nat :=
+ match a with
+ S n => S (structrec n)
+ | 0 => 0
+ end.
+intros.
+unfold n0.
+omega.
+Defined.
+
+Print structrec.
+Extraction structrec.
+Extraction structrec.
+
+Definition structrec_fun (a : nat) : nat := structrec a (lt_wf a).
+Print structrec_fun.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 01:38:07 +0000