summaryrefslogtreecommitdiff
path: root/contrib/subtac
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/subtac')
-rw-r--r--contrib/subtac/FixSub.v82
-rw-r--r--contrib/subtac/FunctionalExtensionality.v25
-rw-r--r--contrib/subtac/Subtac.v2
-rw-r--r--contrib/subtac/Utils.v28
-rw-r--r--contrib/subtac/eterm.ml30
-rw-r--r--contrib/subtac/g_subtac.ml451
-rw-r--r--contrib/subtac/subtac.ml17
-rw-r--r--contrib/subtac/subtac_cases.ml1925
-rw-r--r--contrib/subtac/subtac_cases.mli50
-rw-r--r--contrib/subtac/subtac_coercion.ml168
-rw-r--r--contrib/subtac/subtac_command.ml282
-rw-r--r--contrib/subtac/subtac_obligations.ml321
-rw-r--r--contrib/subtac/subtac_obligations.mli17
-rw-r--r--contrib/subtac/subtac_pretyping.ml33
-rw-r--r--contrib/subtac/subtac_pretyping_F.ml13
-rw-r--r--contrib/subtac/subtac_utils.ml373
-rw-r--r--contrib/subtac/subtac_utils.mli20
-rw-r--r--contrib/subtac/test/ListsTest.v141
-rw-r--r--contrib/subtac/test/euclid.v73
19 files changed, 3016 insertions, 635 deletions
diff --git a/contrib/subtac/FixSub.v b/contrib/subtac/FixSub.v
index ded069bf..46121ff1 100644
--- a/contrib/subtac/FixSub.v
+++ b/contrib/subtac/FixSub.v
@@ -1,37 +1,87 @@
Require Import Wf.
+Require Import Coq.subtac.Utils.
Section Well_founded.
-Variable A : Set.
-Variable R : A -> A -> Prop.
-Hypothesis Rwf : well_founded R.
+ Variable A : Type.
+ Variable R : A -> A -> Prop.
+ Hypothesis Rwf : well_founded R.
+
+ Section Acc.
+
+ Variable P : A -> Type.
+
+ Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x.
+
+ Fixpoint Fix_F_sub (x : A) (r : Acc R x) {struct r} : P x :=
+ F_sub x (fun y: { y : A | R y x} => Fix_F_sub (proj1_sig y)
+ (Acc_inv r (proj1_sig y) (proj2_sig y))).
+
+ Definition Fix_sub (x : A) := Fix_F_sub x (Rwf x).
+ End Acc.
+
+ Section FixPoint.
+ Variable P : A -> Type.
+
+ Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x.
+
+ Notation Fix_F := (Fix_F_sub P F_sub) (only parsing). (* alias *)
+
+ Definition Fix (x:A) := Fix_F_sub P F_sub x (Rwf x).
+
+ Hypothesis
+ F_ext :
+ forall (x:A) (f g:forall y:{y:A | R y x}, P (`y)),
+ (forall y:{ y:A | R y x}, f y = g y) -> F_sub x f = F_sub x g.
-Section FixPoint.
-
-Variable P : A -> Set.
+ Lemma Fix_F_eq :
+ forall (x:A) (r:Acc R x),
+ F_sub x (fun (y:{y:A|R y x}) => Fix_F (`y) (Acc_inv r (proj1_sig y) (proj2_sig y))) = Fix_F x r.
+ Proof.
+ destruct r using Acc_inv_dep; auto.
+ Qed.
+
+ Lemma Fix_F_inv : forall (x:A) (r s:Acc R x), Fix_F x r = Fix_F x s.
+ Proof.
+ intro x; induction (Rwf x); intros.
+ rewrite <- (Fix_F_eq x r); rewrite <- (Fix_F_eq x s); intros.
+ apply F_ext; auto.
+ intros.
+ rewrite (proof_irrelevance (Acc R x) r s) ; auto.
+ Qed.
-Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x.
-
-Fixpoint Fix_F_sub (x : A) (r : Acc R x) {struct r} : P x :=
- F_sub x (fun y: { y : A | R y x} => Fix_F_sub (proj1_sig y)
- (Acc_inv r (proj1_sig y) (proj2_sig y))).
+ Lemma Fix_eq : forall x:A, Fix x = F_sub x (fun (y:{y:A|R y x}) => Fix (proj1_sig y)).
+ Proof.
+ intro x; unfold Fix in |- *.
+ rewrite <- (Fix_F_eq ).
+ apply F_ext; intros.
+ apply Fix_F_inv.
+ Qed.
-Definition Fix_sub (x : A) := Fix_F_sub x (Rwf x).
+ Lemma fix_sub_eq :
+ forall x : A,
+ Fix_sub P F_sub x =
+ let f_sub := F_sub in
+ f_sub x (fun {y : A | R y x}=> Fix (`y)).
+ exact Fix_eq.
+ Qed.
-End FixPoint.
+ End FixPoint.
End Well_founded.
+Extraction Inline Fix_F_sub Fix_sub.
+
Require Import Wf_nat.
Require Import Lt.
Section Well_founded_measure.
-Variable A : Set.
+Variable A : Type.
Variable f : A -> nat.
Definition R := fun x y => f x < f y.
Section FixPoint.
-Variable P : A -> Set.
+Variable P : A -> Type.
Variable F_sub : forall x:A, (forall y: { y : A | f y < f x }, P (proj1_sig y)) -> P x.
@@ -44,3 +94,5 @@ Definition Fix_measure_sub (x : A) := Fix_measure_F_sub x (lt_wf (f x)).
End FixPoint.
End Well_founded_measure.
+
+Extraction Inline Fix_measure_F_sub Fix_measure_sub.
diff --git a/contrib/subtac/FunctionalExtensionality.v b/contrib/subtac/FunctionalExtensionality.v
new file mode 100644
index 00000000..1a12ac82
--- /dev/null
+++ b/contrib/subtac/FunctionalExtensionality.v
@@ -0,0 +1,25 @@
+Axiom fun_extensionality : forall A B (f g : A -> B),
+ (forall x, f x = g x) -> f = g.
+
+Axiom fun_extensionality_dep : forall A, forall B : (A -> Type), forall (f g : forall x : A, B x),
+ (forall x, f x = g x) -> f = g.
+
+Hint Resolve fun_extensionality fun_extensionality_dep : subtac.
+
+Require Import Coq.subtac.Utils.
+Require Import Coq.subtac.FixSub.
+
+Lemma fix_sub_eq_ext :
+ forall (A : Set) (R : A -> A -> Prop) (Rwf : well_founded R)
+ (P : A -> Set)
+ (F_sub : forall x : A, (forall {y : A | R y x}, P (`y)) -> P x),
+ forall x : A,
+ Fix_sub A R Rwf P F_sub x =
+ F_sub x (fun {y : A | R y x}=> Fix A R Rwf P F_sub (`y)).
+Proof.
+ intros ; apply Fix_eq ; auto.
+ intros.
+ assert(f = g).
+ apply (fun_extensionality_dep _ _ _ _ H).
+ rewrite H0 ; auto.
+Qed.
diff --git a/contrib/subtac/Subtac.v b/contrib/subtac/Subtac.v
new file mode 100644
index 00000000..9912cd24
--- /dev/null
+++ b/contrib/subtac/Subtac.v
@@ -0,0 +1,2 @@
+Require Export Coq.subtac.Utils.
+Require Export Coq.subtac.FixSub. \ No newline at end of file
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
index 219cd75b..4a2208ce 100644
--- a/contrib/subtac/Utils.v
+++ b/contrib/subtac/Utils.v
@@ -6,6 +6,8 @@ Notation "'fun' { x : A | P } => Q" :=
Notation "( x & ? )" := (@exist _ _ x _) : core_scope.
+Notation " ! " := (False_rect _ _).
+
Definition ex_pi1 (A : Prop) (P : A -> Prop) (t : ex P) : A.
intros.
induction t.
@@ -44,4 +46,30 @@ end.
Ltac destruct_exists := repeat (destruct_one_pair) .
+Ltac subtac_simpl := simpl ; intros ; destruct_exists ; simpl in * ; try subst ; auto with arith.
+
+(* Destructs calls to f in hypothesis or conclusion, useful if f creates a subset object *)
+Ltac destruct_call f :=
+ match goal with
+ | H : ?T |- _ =>
+ match T with
+ context [f ?x ?y ?z] => destruct (f x y z)
+ | context [f ?x ?y] => destruct (f x y)
+ | context [f ?x] => destruct (f x)
+ end
+ | |- ?T =>
+ match T with
+ context [f ?x ?y ?z] => let n := fresh "H" in set (n:=f x y z); destruct n
+ | context [f ?x ?y] => let n := fresh "H" in set (n:=f x y); destruct n
+ | context [f ?x] => let n := fresh "H" in set (n:=f x); destruct n
+ end
+ end.
+
Extraction Inline proj1_sig.
+Extract Inductive unit => "unit" [ "()" ].
+Extract Inductive bool => "bool" [ "true" "false" ].
+Extract Inductive sumbool => "bool" [ "true" "false" ].
+Extract Inductive prod => "pair" [ "" ].
+Extract Inductive sigT => "pair" [ "" ].
+
+Require Export ProofIrrelevance.
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index 790e61a0..1844fea5 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -52,8 +52,8 @@ let subst_evar_constr evs n t =
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 _ -> () );
+(* (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)
*)
@@ -126,7 +126,6 @@ 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");
let evn =
let i = ref (-1) in
List.rev_map (fun (id, ev) -> incr i;
@@ -136,12 +135,9 @@ let eterm_obligations name nclen evm t tycon =
(* Remove existential variables in types and build the corresponding products *)
fold_right
(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 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)
evn []
@@ -152,17 +148,17 @@ let eterm_obligations name nclen evm t tycon =
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);
- trace (str "Term constructed in eterm" ++ spc () ++
- Termops.print_constr_env (Global.env ()) t');
- ignore(iter
- (fun (name, typ, deps) ->
- trace (str "Evar :" ++ spc () ++ str (string_of_id name) ++
- Termops.print_constr_env (Global.env ()) typ))
- evars);
- with _ -> ());
+(* (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(iter *)
+(* (fun (name, typ, deps) -> *)
+(* trace (str "Evar :" ++ spc () ++ str (string_of_id name) ++ *)
+(* Termops.print_constr_env (Global.env ()) typ)) *)
+(* evars); *)
+(* with _ -> ()); *)
Array.of_list (List.rev evars), t'
let mkMetas n =
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index 243cb191..e31326e9 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 9326 2006-10-31 12:57:26Z msozeau $ *)
+(* $Id: g_subtac.ml4 9588 2007-02-02 16:17:13Z herbelin $ *)
(*i camlp4deps: "parsing/grammar.cma" i*)
@@ -37,6 +37,8 @@ struct
let gec s = Gram.Entry.create ("Subtac."^s)
(* types *)
let subtac_gallina_loc : Vernacexpr.vernac_expr located Gram.Entry.e = gec "subtac_gallina_loc"
+
+ let subtac_nameopt : identifier option Gram.Entry.e = gec "subtac_nameopt"
end
open SubtacGram
@@ -46,12 +48,17 @@ open Pcoq
let sigref = mkRefC (Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Init.Specif.sig"))
GEXTEND Gram
- GLOBAL: subtac_gallina_loc Constr.binder_let Constr.binder;
+ GLOBAL: subtac_gallina_loc Constr.binder_let Constr.binder subtac_nameopt;
subtac_gallina_loc:
[ [ g = Vernac.gallina -> loc, g ] ]
;
+ subtac_nameopt:
+ [ [ "ofb"; id=Prim.ident -> Some (id)
+ | -> None ] ]
+ ;
+
Constr.binder_let:
[ [ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" ->
let typ = mkAppC (sigref, [mkLambdaC ([id], t, c)]) in
@@ -60,8 +67,12 @@ GEXTEND Gram
Constr.binder:
[ [ "("; id=Prim.name; ":"; c=Constr.lconstr; "|"; p=Constr.lconstr; ")" ->
- let typ = mkAppC (sigref, [mkLambdaC ([id], c, p)]) in
- ([id], typ) ] ];
+ ([id],mkAppC (sigref, [mkLambdaC ([id], c, p)]))
+ | "("; id=Prim.name; ":"; c=Constr.lconstr; ")" ->
+ ([id],c)
+ | "("; id=Prim.name; lid=LIST1 Prim.name; ":"; c=Constr.lconstr; ")" ->
+ (id::lid,c)
+ ] ];
END
@@ -69,16 +80,42 @@ GEXTEND Gram
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),
- (globwit_subtac_gallina_loc : (Genarg.glevel, Tacexpr.glob_tactic_expr) 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"
+type 'a nameopt_argtype = (identifier option, 'a, 'a) Genarg.abstract_argument_type
+
+let (wit_subtac_nameopt : Genarg.tlevel nameopt_argtype),
+ (globwit_subtac_nameopt : Genarg.glevel nameopt_argtype),
+ (rawwit_subtac_nameopt : Genarg.rlevel nameopt_argtype) =
+ Genarg.create_arg "subtac_nameopt"
+
VERNAC COMMAND EXTEND Subtac
[ "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) ]
+ END
+
+VERNAC COMMAND EXTEND Subtac_Obligations
+| [ "Obligation" integer(num) "of" ident(name) ":" lconstr(t) ] -> [ Subtac_obligations.subtac_obligation (num, Some name, Some t) ]
+| [ "Obligation" integer(num) "of" ident(name) ] -> [ Subtac_obligations.subtac_obligation (num, Some name, None) ]
+| [ "Obligation" integer(num) ":" lconstr(t) ] -> [ Subtac_obligations.subtac_obligation (num, None, Some t) ]
+| [ "Obligation" integer(num) ] -> [ Subtac_obligations.subtac_obligation (num, None, None) ]
+| [ "Next" "Obligation" "of" ident(name) ] -> [ Subtac_obligations.next_obligation (Some name) ]
+| [ "Next" "Obligation" ] -> [ Subtac_obligations.next_obligation None ]
+END
+
+VERNAC COMMAND EXTEND Subtac_Solve_Obligations
| [ "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) ]
+| [ "Admit" "Obligations" "of" ident(name) ] -> [ Subtac_obligations.admit_obligations (Some name) ]
+| [ "Admit" "Obligations" ] -> [ Subtac_obligations.admit_obligations None ]
+ END
+
+VERNAC COMMAND EXTEND Subtac_Set_Solver
+| [ "Obligations" "Tactic" ":=" tactic(t) ] -> [ Subtac_obligations.set_default_tactic (Tacinterp.interp t) ]
+END
+
+VERNAC COMMAND EXTEND Subtac_Show_Obligations
| [ "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 26e8f715..5e46bead 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 9284 2006-10-26 12:06:57Z msozeau $ *)
+(* $Id: subtac.ml 9563 2007-01-31 09:37:18Z msozeau $ *)
open Global
open Pp
@@ -120,6 +120,8 @@ let subtac_end_proof = function
open Pp
open Ppconstr
open Decl_kinds
+open Tacinterp
+open Tacexpr
let start_proof_com env isevars sopt kind (bl,t) hook =
let id = match sopt with
@@ -140,14 +142,27 @@ let start_proof_com env isevars sopt kind (bl,t) hook =
let print_subgoals () = Options.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
+let subtac_utils_path =
+ make_dirpath (List.map id_of_string ["Utils";contrib_name;"Coq"])
+let utils_tac s =
+ lazy(make_kn (MPfile subtac_utils_path) (make_dirpath []) (mk_label s))
+
+let utils_call tac args =
+ TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (utils_tac tac)),args))
+
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_obligations.set_default_tactic
+ (Tacinterp.eval_tactic (utils_call "subtac_simpl" []))
+
+
let subtac (loc, command) =
check_required_library ["Coq";"Init";"Datatypes"];
check_required_library ["Coq";"Init";"Specif"];
+ (* check_required_library ["Coq";"Logic";"JMeq"]; *)
require_library "Coq.subtac.FixSub";
require_library "Coq.subtac.Utils";
let env = Global.env () in
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
new file mode 100644
index 00000000..fbe1ac37
--- /dev/null
+++ b/contrib/subtac/subtac_cases.ml
@@ -0,0 +1,1925 @@
+(************************************************************************)
+(* 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: cases.ml 9399 2006-11-22 16:11:53Z herbelin $ *)
+
+open Util
+open Names
+open Nameops
+open Term
+open Termops
+open Declarations
+open Inductiveops
+open Environ
+open Sign
+open Reductionops
+open Typeops
+open Type_errors
+
+open Rawterm
+open Retyping
+open Pretype_errors
+open Evarutil
+open Evarconv
+
+open Subtac_utils
+
+(* Pattern-matching errors *)
+
+type pattern_matching_error =
+ | BadPattern of constructor * constr
+ | BadConstructor of constructor * inductive
+ | WrongNumargConstructor of constructor * int
+ | WrongNumargInductive of inductive * int
+ | WrongPredicateArity of constr * constr * constr
+ | NeedsInversion of constr * constr
+ | UnusedClause of cases_pattern list
+ | NonExhaustive of cases_pattern list
+ | CannotInferPredicate of (constr * types) array
+
+exception PatternMatchingError of env * pattern_matching_error
+
+let raise_pattern_matching_error (loc,ctx,te) =
+ Stdpp.raise_with_loc loc (PatternMatchingError(ctx,te))
+
+let error_bad_pattern_loc loc cstr ind =
+ raise_pattern_matching_error (loc, Global.env(), BadPattern (cstr,ind))
+
+let error_bad_constructor_loc loc cstr ind =
+ raise_pattern_matching_error (loc, Global.env(), BadConstructor (cstr,ind))
+
+let error_wrong_numarg_constructor_loc loc env c n =
+ raise_pattern_matching_error (loc, env, WrongNumargConstructor(c,n))
+
+let error_wrong_numarg_inductive_loc loc env c n =
+ raise_pattern_matching_error (loc, env, WrongNumargInductive(c,n))
+
+let error_wrong_predicate_arity_loc loc env c n1 n2 =
+ raise_pattern_matching_error (loc, env, WrongPredicateArity (c,n1,n2))
+
+let error_needs_inversion env x t =
+ raise (PatternMatchingError (env, NeedsInversion (x,t)))
+
+module type S = sig
+ val compile_cases :
+ loc ->
+ (type_constraint -> env -> rawconstr -> unsafe_judgment) *
+ Evd.evar_defs ref ->
+ type_constraint ->
+ env -> rawconstr option * tomatch_tuple * cases_clauses ->
+ unsafe_judgment
+end
+
+(************************************************************************)
+(* Pattern-matching compilation (Cases) *)
+(************************************************************************)
+
+(************************************************************************)
+(* Configuration, errors and warnings *)
+
+open Pp
+
+let mssg_may_need_inversion () =
+ str "Found a matching with no clauses on a term unknown to have an empty inductive type"
+
+(* Utils *)
+let make_anonymous_patvars =
+ list_tabulate (fun _ -> PatVar (dummy_loc,Anonymous))
+
+(* Environment management *)
+let push_rels vars env = List.fold_right push_rel vars env
+
+let push_rel_defs =
+ List.fold_right (fun (x,d,t) e -> push_rel (x,Some d,t) e)
+
+(* We have x1:t1...xn:tn,xi':ti,y1..yk |- c and re-generalize
+ over xi:ti to get x1:t1...xn:tn,xi':ti,y1..yk |- c[xi:=xi'] *)
+
+let regeneralize_rel i k j = if j = i+k then k else if j < i+k then j else j
+
+let rec regeneralize_index i k t = match kind_of_term t with
+ | Rel j when j = i+k -> mkRel (k+1)
+ | Rel j when j < i+k -> t
+ | Rel j when j > i+k -> t
+ | _ -> map_constr_with_binders succ (regeneralize_index i) k t
+
+type alias_constr =
+ | DepAlias
+ | NonDepAlias
+
+let mkSpecialLetInJudge j (na,(deppat,nondeppat,d,t)) =
+ { uj_val =
+ (match d with
+ | DepAlias -> mkLetIn (na,deppat,t,j.uj_val)
+ | NonDepAlias ->
+ if (not (dependent (mkRel 1) j.uj_type))
+ or (* A leaf: *) isRel deppat
+ then
+ (* The body of pat is not needed to type j - see *)
+ (* insert_aliases - and both deppat and nondeppat have the *)
+ (* same type, then one can freely substitute one by the other *)
+ subst1 nondeppat j.uj_val
+ else
+ (* The body of pat is not needed to type j but its value *)
+ (* is dependent in the type of j; our choice is to *)
+ (* enforce this dependency *)
+ mkLetIn (na,deppat,t,j.uj_val));
+ uj_type = subst1 deppat j.uj_type }
+
+(**********************************************************************)
+(* Structures used in compiling pattern-matching *)
+
+type rhs =
+ { rhs_env : env;
+ avoid_ids : identifier list;
+ it : rawconstr;
+ }
+
+type equation =
+ { patterns : cases_pattern list;
+ rhs : rhs;
+ alias_stack : name list;
+ eqn_loc : loc;
+ used : bool ref;
+ tag : pattern_source }
+
+type matrix = equation list
+
+(* 1st argument of IsInd is the original ind before extracting the summary *)
+type tomatch_type =
+ | IsInd of types * inductive_type
+ | NotInd of constr option * types
+
+type tomatch_status =
+ | Pushed of ((constr * tomatch_type) * int list)
+ | Alias of (constr * constr * alias_constr * constr)
+ | Abstract of rel_declaration
+
+type tomatch_stack = tomatch_status list
+
+(* The type [predicate_signature] types the terms to match and the rhs:
+
+ - [PrLetIn (names,dep,pred)] types a pushed term ([Pushed]),
+ if dep<>Anonymous, the term is dependent, let n=|names|, if
+ n<>0 then the type of the pushed term is necessarily an
+ inductive with n real arguments. Otherwise, it may be
+ non inductive, or inductive without real arguments, or inductive
+ originating from a subterm in which case real args are not dependent;
+ it accounts for n+1 binders if dep or n binders if not dep
+ - [PrProd] types abstracted term ([Abstract]); it accounts for one binder
+ - [PrCcl] types the right-hand-side
+ - Aliases [Alias] have no trace in [predicate_signature]
+*)
+
+type predicate_signature =
+ | PrLetIn of (name list * name) * predicate_signature
+ | PrProd of predicate_signature
+ | PrCcl of constr
+
+(* We keep a constr for aliases and a cases_pattern for error message *)
+
+type alias_builder =
+ | AliasLeaf
+ | AliasConstructor of constructor
+
+type pattern_history =
+ | Top
+ | MakeAlias of alias_builder * pattern_continuation
+
+and pattern_continuation =
+ | Continuation of int * cases_pattern list * pattern_history
+ | Result of cases_pattern list
+
+let start_history n = Continuation (n, [], Top)
+
+let initial_history = function Continuation (_,[],Top) -> true | _ -> false
+
+let feed_history arg = function
+ | Continuation (n, l, h) when n>=1 ->
+ Continuation (n-1, arg :: l, h)
+ | Continuation (n, _, _) ->
+ anomaly ("Bad number of expected remaining patterns: "^(string_of_int n))
+ | Result _ ->
+ anomaly "Exhausted pattern history"
+
+(* This is for non exhaustive error message *)
+
+let rec rawpattern_of_partial_history args2 = function
+ | Continuation (n, args1, h) ->
+ let args3 = make_anonymous_patvars (n - (List.length args2)) in
+ build_rawpattern (List.rev_append args1 (args2@args3)) h
+ | Result pl -> pl
+
+and build_rawpattern args = function
+ | Top -> args
+ | MakeAlias (AliasLeaf, rh) ->
+ assert (args = []);
+ rawpattern_of_partial_history [PatVar (dummy_loc, Anonymous)] rh
+ | MakeAlias (AliasConstructor pci, rh) ->
+ rawpattern_of_partial_history
+ [PatCstr (dummy_loc, pci, args, Anonymous)] rh
+
+let complete_history = rawpattern_of_partial_history []
+
+(* This is to build glued pattern-matching history and alias bodies *)
+
+let rec simplify_history = function
+ | Continuation (0, l, Top) -> Result (List.rev l)
+ | Continuation (0, l, MakeAlias (f, rh)) ->
+ let pargs = List.rev l in
+ let pat = match f with
+ | AliasConstructor pci ->
+ PatCstr (dummy_loc,pci,pargs,Anonymous)
+ | AliasLeaf ->
+ assert (l = []);
+ PatVar (dummy_loc, Anonymous) in
+ feed_history pat rh
+ | h -> h
+
+(* Builds a continuation expecting [n] arguments and building [ci] applied
+ to this [n] arguments *)
+
+let push_history_pattern n current cont =
+ Continuation (n, [], MakeAlias (current, cont))
+
+(* A pattern-matching problem has the following form:
+
+ env, isevars |- <pred> Cases tomatch of mat end
+
+ where tomatch is some sequence of "instructions" (t1 ... tn)
+
+ and mat is some matrix
+ (p11 ... p1n -> rhs1)
+ ( ... )
+ (pm1 ... pmn -> rhsm)
+
+ Terms to match: there are 3 kinds of instructions
+
+ - "Pushed" terms to match are typed in [env]; these are usually just
+ Rel(n) except for the initial terms given by user and typed in [env]
+ - "Abstract" instructions means an abstraction has to be inserted in the
+ current branch to build (this means a pattern has been detected dependent
+ in another one and generalisation is necessary to ensure well-typing)
+ - "Alias" instructions means an alias has to be inserted (this alias
+ is usually removed at the end, except when its type is not the
+ same as the type of the matched term from which it comes -
+ typically because the inductive types are "real" parameters)
+
+ Right-hand-sides:
+
+ They consist of a raw term to type in an environment specific to the
+ clause they belong to: the names of declarations are those of the
+ variables present in the patterns. Therefore, they come with their
+ own [rhs_env] (actually it is the same as [env] except for the names
+ of variables).
+
+*)
+type pattern_matching_problem =
+ { env : env;
+ isevars : Evd.evar_defs ref;
+ pred : predicate_signature option;
+ tomatch : tomatch_stack;
+ history : pattern_continuation;
+ mat : matrix;
+ caseloc : loc;
+ typing_function: type_constraint -> env -> rawconstr -> unsafe_judgment }
+
+(*--------------------------------------------------------------------------*
+ * A few functions to infer the inductive type from the patterns instead of *
+ * checking that the patterns correspond to the ind. type of the *
+ * destructurated object. Allows type inference of examples like *
+ * match n with O => true | _ => false end *
+ * match x in I with C => true | _ => false end *
+ *--------------------------------------------------------------------------*)
+
+(* Computing the inductive type from the matrix of patterns *)
+
+(* We use the "in I" clause to coerce the terms to match and otherwise
+ use the constructor to know in which type is the matching problem
+
+ Note that insertion of coercions inside nested patterns is done
+ each time the matrix is expanded *)
+
+let rec find_row_ind = function
+ [] -> None
+ | PatVar _ :: l -> find_row_ind l
+ | PatCstr(loc,c,_,_) :: _ -> Some (loc,c)
+
+let inductive_template isevars env tmloc ind =
+ let arsign = get_full_arity_sign env ind in
+ let hole_source = match tmloc with
+ | Some loc -> fun i -> (loc, Evd.TomatchTypeParameter (ind,i))
+ | None -> fun _ -> (dummy_loc, Evd.InternalHole) in
+ let (_,evarl,_) =
+ List.fold_right
+ (fun (na,b,ty) (subst,evarl,n) ->
+ match b with
+ | None ->
+ let ty' = substl subst ty in
+ let e = e_new_evar isevars env ~src:(hole_source n) ty' in
+ (e::subst,e::evarl,n+1)
+ | Some b ->
+ (b::subst,evarl,n+1))
+ arsign ([],[],1) in
+ applist (mkInd ind,List.rev evarl)
+
+
+(************************************************************************)
+(* Utils *)
+
+let mkExistential env ?(src=(dummy_loc,Evd.InternalHole)) isevars =
+ e_new_evar isevars env ~src:src (new_Type ())
+
+let evd_comb2 f isevars x y =
+ let (evd',y) = f !isevars x y in
+ isevars := evd';
+ y
+
+
+module Cases_F(Coercion : Coercion.S) : S = struct
+
+let inh_coerce_to_ind isevars env ty tyi =
+ let expected_typ = inductive_template isevars env None tyi in
+ (* devrait être indifférent d'exiger leq ou pas puisque pour
+ un inductif cela doit être égal *)
+ let _ = e_cumul env isevars expected_typ ty in ()
+
+let unify_tomatch_with_patterns isevars env loc typ pats =
+ match find_row_ind pats with
+ | None -> NotInd (None,typ)
+ | Some (_,(ind,_)) ->
+ inh_coerce_to_ind isevars env typ ind;
+ try IsInd (typ,find_rectype env (Evd.evars_of !isevars) typ)
+ with Not_found -> NotInd (None,typ)
+
+let find_tomatch_tycon isevars env loc = function
+ (* Try if some 'in I ...' is present and can be used as a constraint *)
+ | Some (_,ind,_,_) -> mk_tycon (inductive_template isevars env loc ind)
+ | None -> empty_tycon
+
+let coerce_row typing_fun isevars env pats (tomatch,(_,indopt)) =
+ let loc = Some (loc_of_rawconstr tomatch) in
+ let tycon = find_tomatch_tycon isevars env loc indopt in
+ let j = typing_fun tycon env tomatch in
+ let evd, j = Coercion.inh_coerce_to_base (loc_of_rawconstr tomatch) env !isevars j in
+ isevars := evd;
+ let typ = nf_evar (Evd.evars_of !isevars) j.uj_type in
+ let t =
+ try IsInd (typ,find_rectype env (Evd.evars_of !isevars) typ)
+ with Not_found ->
+ unify_tomatch_with_patterns isevars env loc typ pats in
+ (j.uj_val,t)
+
+let coerce_to_indtype typing_fun isevars env matx tomatchl =
+ let pats = List.map (fun r -> r.patterns) matx in
+ let matx' = match matrix_transpose pats with
+ | [] -> List.map (fun _ -> []) tomatchl (* no patterns at all *)
+ | m -> m in
+ List.map2 (coerce_row typing_fun isevars env) matx' tomatchl
+
+
+
+let adjust_tomatch_to_pattern pb ((current,typ),deps) =
+ (* Ideally, we could find a common inductive type to which both the
+ term to match and the patterns coerce *)
+ (* In practice, we coerce the term to match if it is not already an
+ inductive type and it is not dependent; moreover, we use only
+ the first pattern type and forget about the others *)
+ let typ = match typ with IsInd (t,_) -> t | NotInd (_,t) -> t in
+ let typ =
+ try IsInd (typ,find_rectype pb.env (Evd.evars_of !(pb.isevars)) typ)
+ with Not_found -> NotInd (None,typ) in
+ let tomatch = ((current,typ),deps) in
+ match typ with
+ | NotInd (None,typ) ->
+ let tm1 = List.map (fun eqn -> List.hd eqn.patterns) pb.mat in
+ (match find_row_ind tm1 with
+ | None -> tomatch
+ | Some (_,(ind,_)) ->
+ let indt = inductive_template pb.isevars pb.env None ind in
+ let current =
+ if deps = [] & isEvar typ then
+ (* Don't insert coercions if dependent; only solve evars *)
+ let _ = e_cumul pb.env pb.isevars indt typ in
+ current
+ else
+ (evd_comb2 (Coercion.inh_conv_coerce_to dummy_loc pb.env)
+ pb.isevars (make_judge current typ) (mk_tycon_type indt)).uj_val in
+ let sigma = Evd.evars_of !(pb.isevars) in
+ let typ = IsInd (indt,find_rectype pb.env sigma indt) in
+ ((current,typ),deps))
+ | _ -> tomatch
+
+ (* extract some ind from [t], possibly coercing from constructors in [tm] *)
+let to_mutind env isevars tm c t =
+(* match c with
+ | Some body -> *) NotInd (c,t)
+(* | None -> unify_tomatch_with_patterns isevars env t tm*)
+
+let type_of_tomatch = function
+ | IsInd (t,_) -> t
+ | NotInd (_,t) -> t
+
+let mkDeclTomatch na = function
+ | IsInd (t,_) -> (na,None,t)
+ | NotInd (c,t) -> (na,c,t)
+
+let map_tomatch_type f = function
+ | IsInd (t,ind) -> IsInd (f t,map_inductive_type f ind)
+ | NotInd (c,t) -> NotInd (option_map f c, f t)
+
+let liftn_tomatch_type n depth = map_tomatch_type (liftn n depth)
+let lift_tomatch_type n = liftn_tomatch_type n 1
+
+let lift_tomatch n ((current,typ),info) =
+ ((lift n current,lift_tomatch_type n typ),info)
+
+(**********************************************************************)
+(* Utilities on patterns *)
+
+let current_pattern eqn =
+ match eqn.patterns with
+ | pat::_ -> pat
+ | [] -> anomaly "Empty list of patterns"
+
+let alias_of_pat = function
+ | PatVar (_,name) -> name
+ | PatCstr(_,_,_,name) -> name
+
+let unalias_pat = function
+ | PatVar (c,name) as p ->
+ if name = Anonymous then p else PatVar (c,Anonymous)
+ | PatCstr(a,b,c,name) as p ->
+ if name = Anonymous then p else PatCstr (a,b,c,Anonymous)
+
+let remove_current_pattern eqn =
+ match eqn.patterns with
+ | pat::pats ->
+ { eqn with
+ patterns = pats;
+ alias_stack = alias_of_pat pat :: eqn.alias_stack }
+ | [] -> anomaly "Empty list of patterns"
+
+let prepend_pattern tms eqn = {eqn with patterns = tms@eqn.patterns }
+
+(**********************************************************************)
+(* Dealing with regular and default patterns *)
+let is_regular eqn = eqn.tag = RegularPat
+
+let lower_pattern_status = function
+ | RegularPat -> DefaultPat 0
+ | DefaultPat n -> DefaultPat (n+1)
+
+let pattern_status pats =
+ if array_exists ((=) RegularPat) pats then RegularPat
+ else
+ let min =
+ Array.fold_right
+ (fun pat n -> match pat with
+ | DefaultPat i when i<n -> i
+ | _ -> n)
+ pats 0 in
+ DefaultPat min
+
+(**********************************************************************)
+(* Well-formedness tests *)
+(* Partial check on patterns *)
+
+exception NotAdjustable
+
+let rec adjust_local_defs loc = function
+ | (pat :: pats, (_,None,_) :: decls) ->
+ pat :: adjust_local_defs loc (pats,decls)
+ | (pats, (_,Some _,_) :: decls) ->
+ PatVar (loc, Anonymous) :: adjust_local_defs loc (pats,decls)
+ | [], [] -> []
+ | _ -> raise NotAdjustable
+
+let check_and_adjust_constructor env ind cstrs = function
+ | PatVar _ as pat -> pat
+ | PatCstr (loc,((_,i) as cstr),args,alias) as pat ->
+ (* Check it is constructor of the right type *)
+ let ind' = inductive_of_constructor cstr in
+ if Closure.mind_equiv env ind' ind then
+ (* Check the constructor has the right number of args *)
+ let ci = cstrs.(i-1) in
+ let nb_args_constr = ci.cs_nargs in
+ if List.length args = nb_args_constr then pat
+ else
+ try
+ let args' = adjust_local_defs loc (args, List.rev ci.cs_args)
+ in PatCstr (loc, cstr, args', alias)
+ with NotAdjustable ->
+ error_wrong_numarg_constructor_loc loc (Global.env())
+ cstr nb_args_constr
+ else
+ (* Try to insert a coercion *)
+ try
+ Coercion.inh_pattern_coerce_to loc pat ind' ind
+ with Not_found ->
+ error_bad_constructor_loc loc cstr ind
+
+let check_all_variables typ mat =
+ List.iter
+ (fun eqn -> match current_pattern eqn with
+ | PatVar (_,id) -> ()
+ | PatCstr (loc,cstr_sp,_,_) ->
+ error_bad_pattern_loc loc cstr_sp typ)
+ mat
+
+let check_unused_pattern env eqn =
+ if not !(eqn.used) then
+ raise_pattern_matching_error
+ (eqn.eqn_loc, env, UnusedClause eqn.patterns)
+
+let set_used_pattern eqn = eqn.used := true
+
+let extract_rhs pb =
+ match pb.mat with
+ | [] -> errorlabstrm "build_leaf" (mssg_may_need_inversion())
+ | eqn::_ ->
+ set_used_pattern eqn;
+ eqn.tag, eqn.rhs
+
+(**********************************************************************)
+(* Functions to deal with matrix factorization *)
+
+let occur_in_rhs na rhs =
+ match na with
+ | Anonymous -> false
+ | Name id -> occur_rawconstr id rhs.it
+
+let is_dep_patt eqn = function
+ | PatVar (_,name) -> occur_in_rhs name eqn.rhs
+ | PatCstr _ -> true
+
+let dependencies_in_rhs nargs eqns =
+ if eqns = [] then list_tabulate (fun _ -> false) nargs (* Only "_" patts *)
+ else
+ let deps = List.map (fun (tms,eqn) -> List.map (is_dep_patt eqn) tms) eqns in
+ let columns = matrix_transpose deps in
+ List.map (List.exists ((=) true)) columns
+
+let dependent_decl a = function
+ | (na,None,t) -> dependent a t
+ | (na,Some c,t) -> dependent a t || dependent a c
+
+(* Computing the matrix of dependencies *)
+
+(* We are in context d1...dn |- and [find_dependencies k 1 nextlist]
+ computes for declaration [k+1] in which of declarations in
+ [nextlist] (which corresponds to d(k+2)...dn) it depends;
+ declarations are expressed by index, e.g. in dependency list
+ [n-2;1], [1] points to [dn] and [n-2] to [d3] *)
+
+let rec find_dependency_list k n = function
+ | [] -> []
+ | (used,tdeps,d)::rest ->
+ let deps = find_dependency_list k (n+1) rest in
+ if used && dependent_decl (mkRel n) d
+ then list_add_set (List.length rest + 1) (list_union deps tdeps)
+ else deps
+
+let find_dependencies is_dep_or_cstr_in_rhs d (k,nextlist) =
+ let deps = find_dependency_list k 1 nextlist in
+ if is_dep_or_cstr_in_rhs || deps <> []
+ then (k-1,(true ,deps,d)::nextlist)
+ else (k-1,(false,[] ,d)::nextlist)
+
+let find_dependencies_signature deps_in_rhs typs =
+ let k = List.length deps_in_rhs in
+ let _,l = List.fold_right2 find_dependencies deps_in_rhs typs (k,[]) in
+ List.map (fun (_,deps,_) -> deps) l
+
+(******)
+
+(* A Pushed term to match has just been substituted by some
+ constructor t = (ci x1...xn) and the terms x1 ... xn have been added to
+ match
+
+ - all terms to match and to push (dependent on t by definition)
+ must have (Rel depth) substituted by t and Rel's>depth lifted by n
+ - all pushed terms to match (non dependent on t by definition) must
+ be lifted by n
+
+ We start with depth=1
+*)
+
+let regeneralize_index_tomatch n =
+ let rec genrec depth = function
+ | [] -> []
+ | Pushed ((c,tm),l)::rest ->
+ let c = regeneralize_index n depth c in
+ let tm = map_tomatch_type (regeneralize_index n depth) tm in
+ let l = List.map (regeneralize_rel n depth) l in
+ Pushed ((c,tm),l)::(genrec depth rest)
+ | Alias (c1,c2,d,t)::rest ->
+ Alias (regeneralize_index n depth c1,c2,d,t)::(genrec depth rest)
+ | Abstract d::rest ->
+ Abstract (map_rel_declaration (regeneralize_index n depth) d)
+ ::(genrec (depth+1) rest) in
+ genrec 0
+
+let rec replace_term n c k t =
+ if t = mkRel (n+k) then lift k c
+ else map_constr_with_binders succ (replace_term n c) k t
+
+let replace_tomatch n c =
+ let rec replrec depth = function
+ | [] -> []
+ | Pushed ((b,tm),l)::rest ->
+ let b = replace_term n c depth b in
+ let tm = map_tomatch_type (replace_term n c depth) tm in
+ List.iter (fun i -> if i=n+depth then anomaly "replace_tomatch") l;
+ Pushed ((b,tm),l)::(replrec depth rest)
+ | Alias (c1,c2,d,t)::rest ->
+ Alias (replace_term n c depth c1,c2,d,t)::(replrec depth rest)
+ | Abstract d::rest ->
+ Abstract (map_rel_declaration (replace_term n c depth) d)
+ ::(replrec (depth+1) rest) in
+ replrec 0
+
+let liftn_rel_declaration n k = map_rel_declaration (liftn n k)
+let substnl_rel_declaration sigma k = map_rel_declaration (substnl sigma k)
+
+let rec liftn_tomatch_stack n depth = function
+ | [] -> []
+ | Pushed ((c,tm),l)::rest ->
+ let c = liftn n depth c in
+ let tm = liftn_tomatch_type n depth tm in
+ let l = List.map (fun i -> if i<depth then i else i+n) l in
+ Pushed ((c,tm),l)::(liftn_tomatch_stack n depth rest)
+ | Alias (c1,c2,d,t)::rest ->
+ Alias (liftn n depth c1,liftn n depth c2,d,liftn n depth t)
+ ::(liftn_tomatch_stack n depth rest)
+ | Abstract d::rest ->
+ Abstract (map_rel_declaration (liftn n depth) d)
+ ::(liftn_tomatch_stack n (depth+1) rest)
+
+
+let lift_tomatch_stack n = liftn_tomatch_stack n 1
+
+(* if [current] has type [I(p1...pn u1...um)] and we consider the case
+ of constructor [ci] of type [I(p1...pn u'1...u'm)], then the
+ default variable [name] is expected to have which type?
+ Rem: [current] is [(Rel i)] except perhaps for initial terms to match *)
+
+(************************************************************************)
+(* Some heuristics to get names for variables pushed in pb environment *)
+(* Typical requirement:
+
+ [match y with (S (S x)) => x | x => x end] should be compiled into
+ [match y with O => y | (S n) => match n with O => y | (S x) => x end end]
+
+ and [match y with (S (S n)) => n | n => n end] into
+ [match y with O => y | (S n0) => match n0 with O => y | (S n) => n end end]
+
+ i.e. user names should be preserved and created names should not
+ interfere with user names *)
+
+let merge_name get_name obj = function
+ | Anonymous -> get_name obj
+ | na -> na
+
+let merge_names get_name = List.map2 (merge_name get_name)
+
+let get_names env sign eqns =
+ let names1 = list_tabulate (fun _ -> Anonymous) (List.length sign) in
+ (* If any, we prefer names used in pats, from top to bottom *)
+ let names2 =
+ List.fold_right
+ (fun (pats,eqn) names -> merge_names alias_of_pat pats names)
+ eqns names1 in
+ (* Otherwise, we take names from the parameters of the constructor but
+ avoiding conflicts with user ids *)
+ let allvars =
+ List.fold_left (fun l (_,eqn) -> list_union l eqn.rhs.avoid_ids) [] eqns in
+ let names4,_ =
+ List.fold_left2
+ (fun (l,avoid) d na ->
+ let na =
+ merge_name
+ (fun (na,_,t) -> Name (next_name_away (named_hd env t na) avoid))
+ d na
+ in
+ (na::l,(out_name na)::avoid))
+ ([],allvars) (List.rev sign) names2 in
+ names4
+
+(************************************************************************)
+(* Recovering names for variables pushed to the rhs' environment *)
+
+let recover_alias_names get_name = List.map2 (fun x (_,c,t) ->(get_name x,c,t))
+
+let all_name sign = List.map (fun (n, b, t) -> let n = match n with Name _ -> n | Anonymous -> Name (id_of_string "Anonymous") in
+ (n, b, t)) sign
+
+let push_rels_eqn sign eqn =
+ let sign = all_name sign in
+(* trace (str "push_rels_eqn: " ++ my_print_rel_context eqn.rhs.rhs_env sign ++ str "end"); *)
+(* str " branch is " ++ my_print_constr (fst eqn.rhs.c_orig) (snd eqn.rhs.c_orig)); *)
+(* let rhs = eqn.rhs in *)
+(* let l, c, s, e = *)
+(* List.fold_right *)
+(* (fun (na, c, t) (itlift, it, sign, env) -> *)
+(* (try trace (str "Pushing decl: " ++ pr_rel_decl env (na, c, t) ++ *)
+(* str " lift is " ++ int itlift); *)
+(* with _ -> trace (str "error in push_rels_eqn")); *)
+(* let env' = push_rel (na, c, t) env in *)
+(* match sign with *)
+(* [] -> (itlift, lift 1 it, sign, env') *)
+(* | (na', c, t) :: sign' -> *)
+(* if na' = na then *)
+(* (pred itlift, it, sign', env') *)
+(* else ( *)
+(* trace (str "skipping it"); *)
+(* (itlift, liftn 1 itlift it, sign, env'))) *)
+(* sign (rhs.rhs_lift, rhs.c_it, eqn.rhs.rhs_sign, eqn.rhs.rhs_env) *)
+(* in *)
+ {eqn with rhs = {eqn.rhs with rhs_env = push_rels sign eqn.rhs.rhs_env; } }
+
+let push_rels_eqn_with_names sign eqn =
+ let pats = List.rev (list_firstn (List.length sign) eqn.patterns) in
+ let sign = recover_alias_names alias_of_pat pats sign in
+ push_rels_eqn sign eqn
+
+let build_aliases_context env sigma names allpats pats =
+ (* pats is the list of bodies to push as an alias *)
+ (* They all are defined in env and we turn them into a sign *)
+ (* cuts in sign need to be done in allpats *)
+ let rec insert env sign1 sign2 n newallpats oldallpats = function
+ | (deppat,_,_,_)::pats, Anonymous::names when not (isRel deppat) ->
+ (* Anonymous leaves must be considered named and treated in the *)
+ (* next clause because they may occur in implicit arguments *)
+ insert env sign1 sign2
+ n newallpats (List.map List.tl oldallpats) (pats,names)
+ | (deppat,nondeppat,d,t)::pats, na::names ->
+ let nondeppat = lift n nondeppat in
+ let deppat = lift n deppat in
+ let newallpats =
+ List.map2 (fun l1 l2 -> List.hd l2::l1) newallpats oldallpats in
+ let oldallpats = List.map List.tl oldallpats in
+ let decl = (na,Some deppat,t) in
+ let a = (deppat,nondeppat,d,t) in
+ insert (push_rel decl env) (decl::sign1) ((na,a)::sign2) (n+1)
+ newallpats oldallpats (pats,names)
+ | [], [] -> newallpats, sign1, sign2, env
+ | _ -> anomaly "Inconsistent alias and name lists" in
+ let allpats = List.map (fun x -> [x]) allpats
+ in insert env [] [] 0 (List.map (fun _ -> []) allpats) allpats (pats, names)
+
+let insert_aliases_eqn sign eqnnames alias_rest eqn =
+ let thissign = List.map2 (fun na (_,c,t) -> (na,c,t)) eqnnames sign in
+ push_rels_eqn thissign { eqn with alias_stack = alias_rest; }
+
+
+let insert_aliases env sigma alias eqns =
+ (* Là, y a une faiblesse, si un alias est utilisé dans un cas par *)
+ (* défaut présent mais inutile, ce qui est le cas général, l'alias *)
+ (* est introduit même s'il n'est pas utilisé dans les cas réguliers *)
+ let eqnsnames = List.map (fun eqn -> List.hd eqn.alias_stack) eqns in
+ let alias_rests = List.map (fun eqn -> List.tl eqn.alias_stack) eqns in
+ (* names2 takes the meet of all needed aliases *)
+ let names2 =
+ List.fold_right (merge_name (fun x -> x)) eqnsnames Anonymous in
+ (* Only needed aliases are kept by build_aliases_context *)
+ let eqnsnames, sign1, sign2, env =
+ build_aliases_context env sigma [names2] eqnsnames [alias] in
+ let eqns = list_map3 (insert_aliases_eqn sign1) eqnsnames alias_rests eqns in
+ sign2, env, eqns
+
+(**********************************************************************)
+(* Functions to deal with elimination predicate *)
+
+exception Occur
+let noccur_between_without_evar n m term =
+ let rec occur_rec n c = match kind_of_term c with
+ | Rel p -> if n<=p && p<n+m then raise Occur
+ | Evar (_,cl) -> ()
+ | _ -> iter_constr_with_binders succ occur_rec n c
+ in
+ try occur_rec n term; true with Occur -> false
+
+(* Inferring the predicate *)
+let prepare_unif_pb typ cs =
+ let n = List.length (assums_of_rel_context cs.cs_args) in
+
+ (* We may need to invert ci if its parameters occur in typ *)
+ let typ' =
+ if noccur_between_without_evar 1 n typ then lift (-n) typ
+ else (* TODO4-1 *)
+ error "Unable to infer return clause of this pattern-matching problem" in
+ let args = extended_rel_list (-n) cs.cs_args in
+ let ci = applist (mkConstruct cs.cs_cstr, cs.cs_params@args) in
+
+ (* This is the problem: finding P s.t. cs_args |- (P realargs ci) = typ' *)
+ (Array.map (lift (-n)) cs.cs_concl_realargs, ci, typ')
+
+
+(* Infering the predicate *)
+(*
+The problem to solve is the following:
+
+We match Gamma |- t : I(u01..u0q) against the following constructors:
+
+ Gamma, x11...x1p1 |- C1(x11..x1p1) : I(u11..u1q)
+ ...
+ Gamma, xn1...xnpn |- Cn(xn1..xnp1) : I(un1..unq)
+
+Assume the types in the branches are the following
+
+ Gamma, x11...x1p1 |- branch1 : T1
+ ...
+ Gamma, xn1...xnpn |- branchn : Tn
+
+Assume the type of the global case expression is Gamma |- T
+
+The predicate has the form phi = [y1..yq][z:I(y1..yq)]? and must satisfy
+the following n+1 equations:
+
+ Gamma, x11...x1p1 |- (phi u11..u1q (C1 x11..x1p1)) = T1
+ ...
+ Gamma, xn1...xnpn |- (phi un1..unq (Cn xn1..xnpn)) = Tn
+ Gamma |- (phi u01..u0q t) = T
+
+Some hints:
+
+- Clearly, if xij occurs in Ti, then, a "match z with (Ci xi1..xipi) => ..."
+ should be inserted somewhere in Ti.
+
+- If T is undefined, an easy solution is to insert a "match z with (Ci
+ xi1..xipi) => ..." in front of each Ti
+
+- Otherwise, T1..Tn and T must be step by step unified, if some of them
+ diverge, then try to replace the diverging subterm by one of y1..yq or z.
+
+- The main problem is what to do when an existential variables is encountered
+
+let prepare_unif_pb typ cs =
+ let n = cs.cs_nargs in
+ let _,p = decompose_prod_n n typ in
+ let ci = build_dependent_constructor cs in
+ (* This is the problem: finding P s.t. cs_args |- (P realargs ci) = p *)
+ (n, cs.cs_concl_realargs, ci, p)
+
+let eq_operator_lift k (n,n') = function
+ | OpRel p, OpRel p' when p > k & p' > k ->
+ if p < k+n or p' < k+n' then false else p - n = p' - n'
+ | op, op' -> op = op'
+
+let rec transpose_args n =
+ if n=0 then []
+ else
+ (Array.map (fun l -> List.hd l) lv)::
+ (transpose_args (m-1) (Array.init (fun l -> List.tl l)))
+
+let shift_operator k = function OpLambda _ | OpProd _ -> k+1 | _ -> k
+
+let reloc_operator (k,n) = function OpRel p when p > k ->
+let rec unify_clauses k pv =
+ let pv'= Array.map (fun (n,sign,_,p) -> n,splay_constr (whd_betaiotaevar (push_rels (List.rev sign) env) (Evd.evars_of isevars)) p) pv in
+ let n1,op1 = let (n1,(op1,args1)) = pv'.(0) in n1,op1 in
+ if Array.for_all (fun (ni,(opi,_)) -> eq_operator_lift k (n1,ni) (op1,opi)) pv'
+ then
+ let argvl = transpose_args (List.length args1) pv' in
+ let k' = shift_operator k op1 in
+ let argl = List.map (unify_clauses k') argvl in
+ gather_constr (reloc_operator (k,n1) op1) argl
+*)
+
+let abstract_conclusion typ cs =
+ let n = List.length (assums_of_rel_context cs.cs_args) in
+ let (sign,p) = decompose_prod_n n typ in
+ lam_it p sign
+
+let infer_predicate loc env isevars typs cstrs indf =
+ (* Il faudra substituer les isevars a un certain moment *)
+ if Array.length cstrs = 0 then (* "TODO4-3" *)
+ error "Inference of annotation for empty inductive types not implemented"
+ else
+ (* Empiric normalization: p may depend in a irrelevant way on args of the*)
+ (* cstr as in [c:{_:Alpha & Beta}] match c with (existS a b)=>(a,b) end *)
+ let typs =
+ Array.map (local_strong (whd_betaevar empty_env (Evd.evars_of !isevars))) typs
+ in
+ let eqns = array_map2 prepare_unif_pb typs cstrs in
+ (* First strategy: no dependencies at all *)
+(*
+ let (mis,_) = dest_ind_family indf in
+ let (cclargs,_,typn) = eqns.(mis_nconstr mis -1) in
+*)
+ let (sign,_) = get_arity env indf in
+ let mtyp =
+ if array_exists is_Type typs then
+ (* Heuristic to avoid comparison between non-variables algebric univs*)
+ new_Type ()
+ else
+ mkExistential env ~src:(loc, Evd.CasesType) isevars
+ in
+ if array_for_all (fun (_,_,typ) -> e_cumul env isevars typ mtyp) eqns
+ then
+ (* Non dependent case -> turn it into a (dummy) dependent one *)
+ let sign = (Anonymous,None,build_dependent_inductive env indf)::sign in
+ let pred = it_mkLambda_or_LetIn (lift (List.length sign) mtyp) sign in
+ (true,pred) (* true = dependent -- par défaut *)
+ else
+(*
+ let s = get_sort_of env (evars_of isevars) typs.(0) in
+ let predpred = it_mkLambda_or_LetIn (mkSort s) sign in
+ let caseinfo = make_default_case_info mis in
+ let brs = array_map2 abstract_conclusion typs cstrs in
+ let predbody = mkCase (caseinfo, (nf_betaiota predpred), mkRel 1, brs) in
+ let pred = it_mkLambda_or_LetIn (lift (List.length sign) mtyp) sign in
+*)
+ (* "TODO4-2" *)
+ (* We skip parameters *)
+ let cis =
+ Array.map
+ (fun cs ->
+ applist (mkConstruct cs.cs_cstr, extended_rel_list 0 cs.cs_args))
+ cstrs in
+ let ct = array_map2 (fun ci (_,_,t) -> (ci,t)) cis eqns in
+ raise_pattern_matching_error (loc,env, CannotInferPredicate ct)
+(*
+ (true,pred)
+*)
+
+(* Propagation of user-provided predicate through compilation steps *)
+
+let rec map_predicate f k = function
+ | PrCcl ccl -> PrCcl (f k ccl)
+ | PrProd pred ->
+ PrProd (map_predicate f (k+1) pred)
+ | PrLetIn ((names,dep as tm),pred) ->
+ let k' = List.length names + (if dep<>Anonymous then 1 else 0) in
+ PrLetIn (tm, map_predicate f (k+k') pred)
+
+let rec noccurn_predicate k = function
+ | PrCcl ccl -> noccurn k ccl
+ | PrProd pred -> noccurn_predicate (k+1) pred
+ | PrLetIn ((names,dep),pred) ->
+ let k' = List.length names + (if dep<>Anonymous then 1 else 0) in
+ noccurn_predicate (k+k') pred
+
+let liftn_predicate n = map_predicate (liftn n)
+
+let lift_predicate n = liftn_predicate n 1
+
+let regeneralize_index_predicate n = map_predicate (regeneralize_index n) 0
+
+let substnl_predicate sigma = map_predicate (substnl sigma)
+
+(* This is parallel bindings *)
+let subst_predicate (args,copt) pred =
+ let sigma = match copt with
+ | None -> List.rev args
+ | Some c -> c::(List.rev args) in
+ substnl_predicate sigma 0 pred
+
+let specialize_predicate_var (cur,typ) = function
+ | PrProd _ | PrCcl _ ->
+ anomaly "specialize_predicate_var: a pattern-variable must be pushed"
+ | PrLetIn (([],dep),pred) ->
+ subst_predicate ([],if dep<>Anonymous then Some cur else None) pred
+ | PrLetIn ((_,dep),pred) ->
+ (match typ with
+ | IsInd (_,IndType (_,realargs)) ->
+ subst_predicate (realargs,if dep<>Anonymous then Some cur else None) pred
+ | _ -> anomaly "specialize_predicate_var")
+
+let ungeneralize_predicate = function
+ | PrLetIn _ | PrCcl _ -> anomaly "ungeneralize_predicate: expects a product"
+ | PrProd pred -> pred
+
+(*****************************************************************************)
+(* We have pred = [X:=realargs;x:=c]P typed in Gamma1, x:I(realargs), Gamma2 *)
+(* and we want to abstract P over y:t(x) typed in the same context to get *)
+(* *)
+(* pred' = [X:=realargs;x':=c](y':t(x'))P[y:=y'] *)
+(* *)
+(* We first need to lift t(x) s.t. it is typed in Gamma, X:=rargs, x' *)
+(* then we have to replace x by x' in t(x) and y by y' in P *)
+(*****************************************************************************)
+let generalize_predicate ny d = function
+ | PrLetIn ((names,dep as tm),pred) ->
+ if dep=Anonymous then anomaly "Undetected dependency";
+ let p = List.length names + 1 in
+ let pred = lift_predicate 1 pred in
+ let pred = regeneralize_index_predicate (ny+p+1) pred in
+ PrLetIn (tm, PrProd pred)
+ | PrProd _ | PrCcl _ ->
+ anomaly "generalize_predicate: expects a non trivial pattern"
+
+let rec extract_predicate l = function
+ | pred, Alias (deppat,nondeppat,_,_)::tms ->
+ let tms' = match kind_of_term nondeppat with
+ | Rel i -> replace_tomatch i deppat tms
+ | _ -> (* initial terms are not dependent *) tms in
+ extract_predicate l (pred,tms')
+ | PrProd pred, Abstract d'::tms ->
+ let d' = map_rel_declaration (lift (List.length l)) d' in
+ substl l (mkProd_or_LetIn d' (extract_predicate [] (pred,tms)))
+ | PrLetIn (([],dep),pred), Pushed ((cur,_),_)::tms ->
+ extract_predicate (if dep<>Anonymous then cur::l else l) (pred,tms)
+ | PrLetIn ((_,dep),pred), Pushed ((cur,IsInd (_,(IndType(_,realargs)))),_)::tms ->
+ let l = List.rev realargs@l in
+ extract_predicate (if dep<>Anonymous then cur::l else l) (pred,tms)
+ | PrCcl ccl, [] ->
+ substl l ccl
+ | _ -> anomaly"extract_predicate: predicate inconsistent with terms to match"
+
+let abstract_predicate env sigma indf cur tms = function
+ | (PrProd _ | PrCcl _) -> anomaly "abstract_predicate: must be some LetIn"
+ | PrLetIn ((names,dep),pred) ->
+ let sign = make_arity_signature env true indf in
+ (* n is the number of real args + 1 *)
+ let n = List.length sign in
+ let tms = lift_tomatch_stack n tms in
+ let tms =
+ match kind_of_term cur with
+ | Rel i -> regeneralize_index_tomatch (i+n) tms
+ | _ -> (* Initial case *) tms in
+ (* Depending on whether the predicate is dependent or not, and has real
+ args or not, we lift it to make room for [sign] *)
+ (* Even if not intrinsically dep, we move the predicate into a dep one *)
+ let sign,k =
+ if names = [] & n <> 1 then
+ (* Real args were not considered *)
+ (if dep<>Anonymous then
+ ((let (_,c,t) = List.hd sign in (dep,c,t)::List.tl sign),n-1)
+ else
+ (sign,n))
+ else
+ (* Real args are OK *)
+ (List.map2 (fun na (_,c,t) -> (na,c,t)) (dep::names) sign,
+ if dep<>Anonymous then 0 else 1) in
+ let pred = lift_predicate k pred in
+ let pred = extract_predicate [] (pred,tms) in
+ (true, it_mkLambda_or_LetIn_name env pred sign)
+
+let rec known_dependent = function
+ | None -> false
+ | Some (PrLetIn ((_,dep),_)) -> dep<>Anonymous
+ | Some (PrCcl _) -> false
+ | Some (PrProd _) ->
+ anomaly "known_dependent: can only be used when patterns remain"
+
+(* [expand_arg] is used by [specialize_predicate]
+ it replaces gamma, x1...xn, x1...xk |- pred
+ by gamma, x1...xn, x1...xk-1 |- [X=realargs,xk=xk]pred (if dep) or
+ by gamma, x1...xn, x1...xk-1 |- [X=realargs]pred (if not dep) *)
+
+let expand_arg n alreadydep (na,t) deps (k,pred) =
+ (* current can occur in pred even if the original problem is not dependent *)
+ let dep =
+ if alreadydep<>Anonymous then alreadydep
+ else if deps = [] && noccurn_predicate 1 pred then Anonymous
+ else Name (id_of_string "x") in
+ let pred = if dep<>Anonymous then pred else lift_predicate (-1) pred in
+ (* There is no dependency in realargs for subpattern *)
+ (k-1, PrLetIn (([],dep), pred))
+
+
+(*****************************************************************************)
+(* pred = [X:=realargs;x:=c]P types the following problem: *)
+(* *)
+(* Gamma |- match Pushed(c:I(realargs)) rest with...end: pred *)
+(* *)
+(* where the branch with constructor Ci:(x1:T1)...(xn:Tn)->I(realargsi) *)
+(* is considered. Assume each Ti is some Ii(argsi). *)
+(* We let e=Ci(x1,...,xn) and replace pred by *)
+(* *)
+(* pred' = [X1:=rargs1,x1:=x1']...[Xn:=rargsn,xn:=xn'](P[X:=realargsi;x:=e]) *)
+(* *)
+(* s.t Gamma,x1'..xn' |- match Pushed(x1')..Pushed(xn') rest with..end :pred'*)
+(* *)
+(*****************************************************************************)
+let specialize_predicate tomatchs deps cs = function
+ | (PrProd _ | PrCcl _) ->
+ anomaly "specialize_predicate: a matched pattern must be pushed"
+ | PrLetIn ((names,isdep),pred) ->
+ (* Assume some gamma st: gamma, (X,x:=realargs,copt) |- pred *)
+ let nrealargs = List.length names in
+ let k = nrealargs + (if isdep<>Anonymous then 1 else 0) in
+ (* We adjust pred st: gamma, x1..xn, (X,x:=realargs,copt) |- pred' *)
+ let n = cs.cs_nargs in
+ let pred' = liftn_predicate n (k+1) pred in
+ let argsi = if nrealargs <> 0 then Array.to_list cs.cs_concl_realargs else [] in
+ let copti = if isdep<>Anonymous then Some (build_dependent_constructor cs) else None in
+ (* The substituends argsi, copti are all defined in gamma, x1...xn *)
+ (* We need _parallel_ bindings to get gamma, x1...xn |- pred'' *)
+ let pred'' = subst_predicate (argsi, copti) pred' in
+ (* We adjust pred st: gamma, x1..xn, x1..xn |- pred'' *)
+ let pred''' = liftn_predicate n (n+1) pred'' in
+ (* We finally get gamma,x1..xn |- [X1,x1:=R1,x1]..[Xn,xn:=Rn,xn]pred'''*)
+ snd (List.fold_right2 (expand_arg n isdep) tomatchs deps (n,pred'''))
+
+let find_predicate loc env isevars p typs cstrs current
+ (IndType (indf,realargs)) tms =
+ let (dep,pred) =
+ match p with
+ | Some p -> abstract_predicate env (Evd.evars_of !isevars) indf current tms p
+ | None -> infer_predicate loc env isevars typs cstrs indf in
+ let typ = whd_beta (applist (pred, realargs)) in
+ if dep then
+ (pred, whd_beta (applist (typ, [current])), new_Type ())
+ else
+ (pred, typ, new_Type ())
+
+(************************************************************************)
+(* Sorting equations by constructor *)
+
+type inversion_problem =
+ (* the discriminating arg in some Ind and its order in Ind *)
+ | Incompatible of int * (int * int)
+ | Constraints of (int * constr) list
+
+let solve_constraints constr_info indt =
+ (* TODO *)
+ Constraints []
+
+let rec irrefutable env = function
+ | PatVar (_,name) -> true
+ | PatCstr (_,cstr,args,_) ->
+ let ind = inductive_of_constructor cstr in
+ let (_,mip) = Inductive.lookup_mind_specif env ind in
+ let one_constr = Array.length mip.mind_user_lc = 1 in
+ one_constr & List.for_all (irrefutable env) args
+
+let first_clause_irrefutable env = function
+ | eqn::mat -> List.for_all (irrefutable env) eqn.patterns
+ | _ -> false
+
+let group_equations pb ind current cstrs mat =
+ let mat =
+ if first_clause_irrefutable pb.env mat then [List.hd mat] else mat in
+ let brs = Array.create (Array.length cstrs) [] in
+ let only_default = ref true in
+ let _ =
+ List.fold_right (* To be sure it's from bottom to top *)
+ (fun eqn () ->
+ let rest = remove_current_pattern eqn in
+ let pat = current_pattern eqn in
+ match check_and_adjust_constructor pb.env ind cstrs pat with
+ | PatVar (_,name) ->
+ (* This is a default clause that we expand *)
+ for i=1 to Array.length cstrs do
+ let n = cstrs.(i-1).cs_nargs in
+ let args = make_anonymous_patvars n in
+ let rest = {rest with tag = lower_pattern_status rest.tag } in
+ brs.(i-1) <- (args, rest) :: brs.(i-1)
+ done
+ | PatCstr (loc,((_,i)),args,_) ->
+ (* This is a regular clause *)
+ only_default := false;
+ brs.(i-1) <- (args,rest) :: brs.(i-1)) mat () in
+ (brs,!only_default)
+
+(************************************************************************)
+(* Here starts the pattern-matching compilation algorithm *)
+
+(* Abstracting over dependent subterms to match *)
+let rec generalize_problem pb = function
+ | [] -> pb
+ | i::l ->
+ let d = map_rel_declaration (lift i) (Environ.lookup_rel i pb.env) in
+ let pb' = generalize_problem pb l in
+ let tomatch = lift_tomatch_stack 1 pb'.tomatch in
+ let tomatch = regeneralize_index_tomatch (i+1) tomatch in
+ { pb with
+ tomatch = Abstract d :: tomatch;
+ pred = option_map (generalize_predicate i d) pb'.pred }
+
+(* No more patterns: typing the right-hand-side of equations *)
+let build_leaf pb =
+ let tag, rhs = extract_rhs pb in
+ let tycon = match pb.pred with
+ | None -> anomaly "Predicate not found"
+ | Some (PrCcl typ) -> mk_tycon typ
+ | Some _ -> anomaly "not all parameters of pred have been consumed" in
+ tag, pb.typing_function tycon rhs.rhs_env rhs.it
+
+(* Building the sub-problem when all patterns are variables *)
+let shift_problem (current,t) pb =
+ {pb with
+ tomatch = Alias (current,current,NonDepAlias,type_of_tomatch t)::pb.tomatch;
+ pred = option_map (specialize_predicate_var (current,t)) pb.pred;
+ history = push_history_pattern 0 AliasLeaf pb.history;
+ mat = List.map remove_current_pattern pb.mat }
+
+(* Building the sub-pattern-matching problem for a given branch *)
+let build_branch current deps pb eqns const_info =
+ (* We remember that we descend through a constructor *)
+ let alias_type =
+ if Array.length const_info.cs_concl_realargs = 0
+ & not (known_dependent pb.pred) & deps = []
+ then
+ NonDepAlias
+ else
+ DepAlias
+ in
+ let history =
+ push_history_pattern const_info.cs_nargs
+ (AliasConstructor const_info.cs_cstr)
+ pb.history in
+
+ (* We find matching clauses *)
+ let cs_args = (*assums_of_rel_context*) const_info.cs_args in
+ let names = get_names pb.env cs_args eqns in
+ let submat = List.map (fun (tms,eqn) -> prepend_pattern tms eqn) eqns in
+ if submat = [] then
+ raise_pattern_matching_error
+ (dummy_loc, pb.env, NonExhaustive (complete_history history));
+ let typs = List.map2 (fun (_,c,t) na -> (na,c,t)) cs_args names in
+ let _,typs',_ =
+ List.fold_right
+ (fun (na,c,t as d) (env,typs,tms) ->
+ let tm1 = List.map List.hd tms in
+ let tms = List.map List.tl tms in
+ (push_rel d env, (na,to_mutind env pb.isevars tm1 c t)::typs,tms))
+ typs (pb.env,[],List.map fst eqns) in
+
+ let dep_sign =
+ find_dependencies_signature
+ (dependencies_in_rhs const_info.cs_nargs eqns) (List.rev typs) in
+
+ (* The dependent term to subst in the types of the remaining UnPushed
+ terms is relative to the current context enriched by topushs *)
+ let ci = build_dependent_constructor const_info in
+
+ (* We replace [(mkRel 1)] by its expansion [ci] *)
+ (* and context "Gamma = Gamma1, current, Gamma2" by "Gamma;typs;curalias" *)
+ (* This is done in two steps : first from "Gamma |- tms" *)
+ (* into "Gamma; typs; curalias |- tms" *)
+ let tomatch = lift_tomatch_stack const_info.cs_nargs pb.tomatch in
+
+ let currents =
+ list_map2_i
+ (fun i (na,t) deps -> Pushed ((mkRel i, lift_tomatch_type i t), deps))
+ 1 typs' (List.rev dep_sign) in
+
+ let sign = List.map (fun (na,t) -> mkDeclTomatch na t) typs' in
+ let ind =
+ appvect (
+ applist (mkInd (inductive_of_constructor const_info.cs_cstr),
+ List.map (lift const_info.cs_nargs) const_info.cs_params),
+ const_info.cs_concl_realargs) in
+
+ let cur_alias = lift (List.length sign) current in
+ let currents = Alias (ci,cur_alias,alias_type,ind) :: currents in
+ let env' = push_rels sign pb.env in
+ let pred' = option_map (specialize_predicate (List.rev typs') dep_sign const_info) pb.pred in
+ sign,
+ { pb with
+ env = env';
+ tomatch = List.rev_append currents tomatch;
+ pred = pred';
+ history = history;
+ mat = List.map (push_rels_eqn_with_names sign) submat }
+
+(**********************************************************************
+ INVARIANT:
+
+ pb = { env, subst, tomatch, mat, ...}
+ tomatch = list of Pushed (c:T) or Abstract (na:T) or Alias (c:T)
+
+ "Pushed" terms and types are relative to env
+ "Abstract" types are relative to env enriched by the previous terms to match
+
+*)
+
+(**********************************************************************)
+(* Main compiling descent *)
+let rec compile pb =
+ match pb.tomatch with
+ | (Pushed cur)::rest -> match_current { pb with tomatch = rest } cur
+ | (Alias x)::rest -> compile_alias pb x rest
+ | (Abstract d)::rest -> compile_generalization pb d rest
+ | [] -> build_leaf pb
+
+and match_current pb tomatch =
+ let ((current,typ as ct),deps) = adjust_tomatch_to_pattern pb tomatch in
+ match typ with
+ | NotInd (_,typ) ->
+ check_all_variables typ pb.mat;
+ compile (shift_problem ct pb)
+ | IsInd (_,(IndType(indf,realargs) as indt)) ->
+ let mind,_ = dest_ind_family indf in
+ let cstrs = get_constructors pb.env indf in
+ let eqns,onlydflt = group_equations pb mind current cstrs pb.mat in
+ if (Array.length cstrs <> 0 or pb.mat <> []) & onlydflt then
+ compile (shift_problem ct pb)
+ else
+ let _constraints = Array.map (solve_constraints indt) cstrs in
+
+ (* We generalize over terms depending on current term to match *)
+ let pb = generalize_problem pb deps in
+
+ (* We compile branches *)
+ let brs = array_map2 (compile_branch current deps pb) eqns cstrs in
+
+ (* We build the (elementary) case analysis *)
+ let tags = Array.map (fun (t,_,_) -> t) brs in
+ let brvals = Array.map (fun (_,v,_) -> v) brs in
+ let brtyps = Array.map (fun (_,_,t) -> t) brs in
+ let (pred,typ,s) =
+ find_predicate pb.caseloc pb.env pb.isevars
+ pb.pred brtyps cstrs current indt pb.tomatch in
+ let ci = make_case_info pb.env mind RegularStyle tags in
+ let case = mkCase (ci,nf_betaiota pred,current,brvals) in
+ let inst = List.map mkRel deps in
+ pattern_status tags,
+ { uj_val = applist (case, inst);
+ uj_type = substl inst typ }
+
+and compile_branch current deps pb eqn cstr =
+ let sign, pb = build_branch current deps pb eqn cstr in
+ let tag, j = compile pb in
+ (tag, it_mkLambda_or_LetIn j.uj_val sign, j.uj_type)
+
+and compile_generalization pb d rest =
+ let pb =
+ { pb with
+ env = push_rel d pb.env;
+ tomatch = rest;
+ pred = option_map ungeneralize_predicate pb.pred;
+ mat = List.map (push_rels_eqn [d]) pb.mat } in
+ let patstat,j = compile pb in
+ patstat,
+ { uj_val = mkLambda_or_LetIn d j.uj_val;
+ uj_type = mkProd_or_LetIn d j.uj_type }
+
+and compile_alias pb (deppat,nondeppat,d,t) rest =
+ let history = simplify_history pb.history in
+ let sign, newenv, mat =
+ insert_aliases pb.env (Evd.evars_of !(pb.isevars)) (deppat,nondeppat,d,t) pb.mat in
+ let n = List.length sign in
+
+ (* We had Gamma1; x:current; Gamma2 |- tomatch(x) and we rebind x to get *)
+ (* Gamma1; x:current; Gamma2; typs; x':=curalias |- tomatch(x') *)
+ let tomatch = lift_tomatch_stack n rest in
+ let tomatch = match kind_of_term nondeppat with
+ | Rel i ->
+ if n = 1 then regeneralize_index_tomatch (i+n) tomatch
+ else replace_tomatch i deppat tomatch
+ | _ -> (* initial terms are not dependent *) tomatch in
+
+ let pb =
+ {pb with
+ env = newenv;
+ tomatch = tomatch;
+ pred = option_map (lift_predicate n) pb.pred;
+ history = history;
+ mat = mat } in
+ let patstat,j = compile pb in
+ patstat,
+ List.fold_left mkSpecialLetInJudge j sign
+
+(* pour les alias des initiaux, enrichir les env de ce qu'il faut et
+substituer après par les initiaux *)
+
+(**************************************************************************)
+(* Preparation of the pattern-matching problem *)
+
+(* builds the matrix of equations testing that each eqn has n patterns
+ * and linearizing the _ patterns.
+ * Syntactic correctness has already been done in astterm *)
+let matx_of_eqns env eqns =
+ let build_eqn (loc,ids,lpat,rhs) =
+ let rhs =
+ { rhs_env = env;
+ avoid_ids = ids@(ids_of_named_context (named_context env));
+ it = rhs;
+ } in
+ { patterns = lpat;
+ tag = RegularPat;
+ alias_stack = [];
+ eqn_loc = loc;
+ used = ref false;
+ rhs = rhs }
+ in List.map build_eqn eqns
+
+(************************************************************************)
+(* preparing the elimination predicate if any *)
+
+let build_expected_arity env isevars isdep tomatchl =
+ let cook n = function
+ | _,IsInd (_,IndType(indf,_)) ->
+ let indf' = lift_inductive_family n indf in
+ Some (build_dependent_inductive env indf', fst (get_arity env indf'))
+ | _,NotInd _ -> None
+ in
+ let rec buildrec n env = function
+ | [] -> new_Type ()
+ | tm::ltm ->
+ match cook n tm with
+ | None -> buildrec n env ltm
+ | Some (ty1,aritysign) ->
+ let rec follow n env = function
+ | d::sign ->
+ mkProd_or_LetIn_name env
+ (follow (n+1) (push_rel d env) sign) d
+ | [] ->
+ if isdep then
+ mkProd (Anonymous, ty1,
+ buildrec (n+1)
+ (push_rel_assum (Anonymous, ty1) env)
+ ltm)
+ else buildrec n env ltm
+ in follow n env (List.rev aritysign)
+ in buildrec 0 env tomatchl
+
+let extract_predicate_conclusion isdep tomatchl pred =
+ let cook = function
+ | _,IsInd (_,IndType(_,args)) -> Some (List.length args)
+ | _,NotInd _ -> None in
+ let rec decomp_lam_force n l p =
+ if n=0 then (l,p) else
+ match kind_of_term p with
+ | Lambda (na,_,c) -> decomp_lam_force (n-1) (na::l) c
+ | _ -> (* eta-expansion *)
+ let na = Name (id_of_string "x") in
+ decomp_lam_force (n-1) (na::l) (applist (lift 1 p, [mkRel 1])) in
+ let rec buildrec allnames p = function
+ | [] -> (List.rev allnames,p)
+ | tm::ltm ->
+ match cook tm with
+ | None ->
+ let p =
+ (* adjust to a sign containing the NotInd's *)
+ if isdep then lift 1 p else p in
+ let names = if isdep then [Anonymous] else [] in
+ buildrec (names::allnames) p ltm
+ | Some n ->
+ let n = if isdep then n+1 else n in
+ let names,p = decomp_lam_force n [] p in
+ buildrec (names::allnames) p ltm
+ in buildrec [] pred tomatchl
+
+let set_arity_signature dep n arsign tomatchl pred x =
+ (* avoid is not exhaustive ! *)
+ let rec decomp_lam_force n avoid l p =
+ if n = 0 then (List.rev l,p,avoid) else
+ match p with
+ | RLambda (_,(Name id as na),_,c) ->
+ decomp_lam_force (n-1) (id::avoid) (na::l) c
+ | RLambda (_,(Anonymous as na),_,c) -> decomp_lam_force (n-1) avoid (na::l) c
+ | _ ->
+ let x = next_ident_away (id_of_string "x") avoid in
+ decomp_lam_force (n-1) (x::avoid) (Name x :: l)
+ (* eta-expansion *)
+ (let a = RVar (dummy_loc,x) in
+ match p with
+ | RApp (loc,p,l) -> RApp (loc,p,l@[a])
+ | _ -> (RApp (dummy_loc,p,[a]))) in
+ let rec decomp_block avoid p = function
+ | ([], _) -> x := Some p
+ | ((_,IsInd (_,IndType(indf,realargs)))::l),(y::l') ->
+ let (ind,params) = dest_ind_family indf in
+ let (nal,p,avoid') = decomp_lam_force (List.length realargs) avoid [] p
+ in
+ let na,p,avoid' =
+ if dep then decomp_lam_force 1 avoid' [] p else [Anonymous],p,avoid'
+ in
+ y :=
+ (List.hd na,
+ if List.for_all ((=) Anonymous) nal then
+ None
+ else
+ Some (dummy_loc, ind, (List.map (fun _ -> Anonymous) params)@nal));
+ decomp_block avoid' p (l,l')
+ | (_::l),(y::l') ->
+ y := (Anonymous,None);
+ decomp_block avoid p (l,l')
+ | _ -> anomaly "set_arity_signature"
+ in
+ decomp_block [] pred (tomatchl,arsign)
+
+let prepare_predicate_from_tycon loc dep env isevars tomatchs sign c =
+ let cook (n, l, env, signs) = function
+ | c,IsInd (_,IndType(indf,realargs)) ->
+ let indf' = lift_inductive_family n indf in
+ let sign = make_arity_signature env dep indf' in
+ let p = List.length realargs in
+ if dep then
+ (n + p + 1, c::(List.rev realargs)@l, push_rels sign env,sign::signs)
+ else
+ (n + p, (List.rev realargs)@l, push_rels sign env,sign::signs)
+ | c,NotInd _ ->
+ (n, l, env, []::signs) in
+ let n, allargs, env, signs = List.fold_left cook (0, [], env, []) tomatchs in
+ let names = List.rev (List.map (List.map pi1) signs) in
+ let allargs =
+ List.map (fun c -> lift n (nf_betadeltaiota env (Evd.evars_of !isevars) c)) allargs in
+ let rec build_skeleton env c =
+ (* Don't put into normal form, it has effects on the synthesis of evars *)
+ (* let c = whd_betadeltaiota env (evars_of isevars) c in *)
+ (* We turn all subterms possibly dependent into an evar with maximum ctxt*)
+ if isEvar c or List.exists (eq_constr c) allargs then
+ e_new_evar isevars env ~src:(loc, Evd.CasesType)
+ (Retyping.get_type_of env (Evd.evars_of !isevars) c)
+ else
+ map_constr_with_full_binders push_rel build_skeleton env c
+ in
+ names, build_skeleton env (lift n c)
+
+(* Here, [pred] is assumed to be in the context built from all *)
+(* realargs and terms to match *)
+let build_initial_predicate isdep allnames pred =
+ let nar = List.fold_left (fun n names -> List.length names + n) 0 allnames in
+ let rec buildrec n pred = function
+ | [] -> PrCcl pred
+ | names::lnames ->
+ let names' = if isdep then List.tl names else names in
+ let n' = n + List.length names' in
+ let pred, p, user_p =
+ if isdep then
+ if dependent (mkRel (nar-n')) pred then pred, 1, 1
+ else liftn (-1) (nar-n') pred, 0, 1
+ else pred, 0, 0 in
+ let na =
+ if p=1 then
+ let na = List.hd names in
+ if na = Anonymous then
+ (* peut arriver en raison des evars *)
+ Name (id_of_string "x") (*Hum*)
+ else na
+ else Anonymous in
+ PrLetIn ((names',na), buildrec (n'+user_p) pred lnames)
+ in buildrec 0 pred allnames
+
+let extract_arity_signature env0 tomatchl tmsign =
+ let get_one_sign n tm (na,t) =
+ match tm with
+ | NotInd (bo,typ) ->
+ (match t with
+ | None -> [na,option_map (lift n) bo,lift n typ]
+ | Some (loc,_,_,_) ->
+ user_err_loc (loc,"",
+ str "Unexpected type annotation for a term of non inductive type"))
+ | IsInd (_,IndType(indf,realargs)) ->
+ let indf' = lift_inductive_family n indf in
+ let (ind,params) = dest_ind_family indf' in
+ let nrealargs = List.length realargs in
+ let realnal =
+ match t with
+ | Some (loc,ind',nparams,realnal) ->
+ if ind <> ind' then
+ user_err_loc (loc,"",str "Wrong inductive type");
+ if List.length params <> nparams
+ or nrealargs <> List.length realnal then
+ anomaly "Ill-formed 'in' clause in cases";
+ List.rev realnal
+ | None -> list_tabulate (fun _ -> Anonymous) nrealargs in
+ let arsign = fst (get_arity env0 indf') in
+ (na,None,build_dependent_inductive env0 indf')
+ ::(List.map2 (fun x (_,c,t) ->(x,c,t)) realnal arsign) in
+ let rec buildrec n = function
+ | [],[] -> []
+ | (_,tm)::ltm, x::tmsign ->
+ let l = get_one_sign n tm x in
+ l :: buildrec (n + List.length l) (ltm,tmsign)
+ | _ -> assert false
+ in List.rev (buildrec 0 (tomatchl,tmsign))
+
+let inh_conv_coerce_to_tycon loc env isevars j tycon =
+ match tycon with
+ | Some p ->
+ let (evd',j) = Coercion.inh_conv_coerce_to loc env !isevars j p in
+ isevars := evd';
+ j
+ | None -> j
+
+let out_ind = function IsInd (_, IndType(x, y)) -> (x, y) | _ -> assert(false)
+
+let list_mapi f l =
+ let rec aux n = function
+ [] -> []
+ | hd :: tl -> f n hd :: aux (succ n) tl
+ in aux 0 l
+
+let constr_of_pat env isevars ty pat idents =
+ let rec typ env ty pat idents =
+ trace (str "Typing pattern " ++ Printer.pr_cases_pattern pat ++ str " in env " ++
+ print_env env ++ str" should have type: " ++ my_print_constr env ty);
+ match pat with
+ | PatVar (l,name) ->
+ let name, idents' = match name with
+ Name n -> name, idents
+ | Anonymous ->
+ let n' = next_ident_away_from (id_of_string "wildcard") idents in
+ Name n', n' :: idents
+ in
+(* trace (str "Treating pattern variable " ++ str (string_of_id (id_of_name name))); *)
+ PatVar (l, name), [name, None, ty], mkRel 1, 1, idents'
+ | PatCstr (l,((_, i) as cstr),args,alias) ->
+ let _ind = inductive_of_constructor cstr in
+ let IndType (indf, realargs) = find_rectype env (Evd.evars_of !isevars) ty in
+ let ind, params = dest_ind_family indf in
+ let cstrs = get_constructors env indf in
+ let ci = cstrs.(i-1) in
+ let nb_args_constr = ci.cs_nargs in
+ assert(nb_args_constr = List.length args);
+ let idents' = idents in
+ let patargs, args, sign, env, n, m, idents' =
+ List.fold_right2
+ (fun (na, c, t) ua (patargs, args, sign, env, n, m, idents) ->
+ let pat', sign', arg', n', idents' = typ env (lift (n - m) t) ua idents in
+ let args' = arg' :: List.map (lift n') args in
+ let env' = push_rels sign' env in
+ (pat' :: patargs, args', sign' @ sign, env', n' + n, succ m, idents'))
+ ci.cs_args (List.rev args) ([], [], [], env, 0, 0, idents')
+ in
+ let args = List.rev args in
+ let patargs = List.rev patargs in
+ let pat' = PatCstr (l, cstr, patargs, alias) in
+ let cstr = mkConstruct ci.cs_cstr in
+ let app = applistc cstr (List.map (lift (List.length sign)) params) in
+ let app = applistc app args in
+(* trace (str "New pattern: " ++ Printer.pr_cases_pattern pat'); *)
+(* let alname = if alias <> Anonymous then alias else Name (id_of_string "anon") in *)
+(* let al = alname, Some (mkRel 1), lift 1 ty in *)
+ if alias <> Anonymous then
+ pat', (alias, Some app, ty) :: sign, lift 1 app, n + 1, idents'
+ else pat', sign, app, n, idents'
+ in
+ let pat', sign, y, z, idents = typ env ty pat idents in
+ let c = it_mkProd_or_LetIn y sign in
+ trace (str "Constr_of_pat gives: " ++ my_print_constr env c);
+ pat', (sign, y), idents
+
+let mk_refl typ a = mkApp (Lazy.force eq_refl, [| typ; a |])
+
+let vars_of_ctx =
+ List.rev_map (fun (na, _, t) ->
+ match na with
+ Anonymous -> raise (Invalid_argument "vars_of_ctx")
+ | Name n -> RVar (dummy_loc, n))
+
+(*let build_ineqs eqns pats =
+ List.fold_left
+ (fun (sign, c) eqn ->
+ let acc = fold_left3
+ (fun acc prevpat (ppat_sign, ppat_c, ppat_ty) (pat, pat_c) ->
+ match acc with
+ None -> None
+ | Some (sign,len, c) ->
+ if is_included pat prevpat then
+ let lens = List.length ppat_sign in
+ let acc =
+ (lift_rels lens ppat_sign @ sign,
+ lens + len,
+ mkApp (Lazy.force eq_ind,
+ [| ppat_ty ; ppat_c ;
+ lift (lens + len) pat_c |]) :: c)
+ in Some acc
+ else None)
+ (sign, c) eqn.patterns eqn.c_patterns pats
+ in match acc with
+ None -> (sign, c)
+ | Some (sign, len, c) ->
+ it_mkProd_or_LetIn c sign
+
+ )
+ ([], []) eqns*)
+
+let constrs_of_pats typing_fun tycon env isevars eqns tomatchs =
+ let i = ref 0 in
+ List.fold_left
+ (fun (branches, eqns) eqn ->
+ let _, newpatterns, pats =
+ List.fold_right2 (fun pat (_, ty) (idents, newpatterns, pats) ->
+ let x, y, z = constr_of_pat env isevars (type_of_tomatch ty) pat idents in
+ (z, x :: newpatterns, y :: pats))
+ eqn.patterns tomatchs ([], [], [])
+ in
+ let rhs_rels, signlen =
+ List.fold_left (fun (renv, n) (sign,_) ->
+ ((lift_rel_context n sign) @ renv, List.length sign + n))
+ ([], 0) pats in
+ let eqs, _, _ = List.fold_left2
+ (fun (eqs, n, slen) (sign, c) (tm, ty) ->
+ let len = n + signlen in (* Number of already defined equations + signature *)
+ let csignlen = List.length sign in
+ let slen' = slen - csignlen in (* Lift to get pattern variables signature *)
+ let c = liftn (signlen - slen) signlen c in (* Lift to jump over previous ind signatures for pattern variables outside sign
+ in c (e.g. type arguments of constructors instanciated by variables ) *)
+ let cstr = lift (slen' + n) c in
+(* trace (str "lift " ++ my_print_constr (push_rels sign env) c ++ *)
+(* str " by " ++ int ++ str " to get " ++ *)
+(* my_print_constr (push_rels sign env) cstr); *)
+ let app =
+ mkApp (Lazy.force eq_ind,
+ [| lift len (type_of_tomatch ty); cstr; lift len tm |])
+ in app :: eqs, succ n, slen')
+ ([], 0, signlen) pats tomatchs
+ in
+ let eqs_rels = List.map (fun eq -> Name (id_of_string "H"), None, eq) eqs in
+(* let ineqs = build_ineqs eqns newpatterns in *)
+ let rhs_rels' = eqs_rels @ rhs_rels in
+ let rhs_env = push_rels rhs_rels' env in
+(* (try trace (str "branch env: " ++ print_env rhs_env) *)
+(* with _ -> trace (str "error in print branch env")); *)
+ let tycon = lift_tycon (List.length eqs + signlen) tycon in
+
+ let j = typing_fun tycon rhs_env eqn.rhs.it in
+(* (try trace (str "in env: " ++ my_print_env rhs_env ++ str"," ++ *)
+(* str "Typed branch: " ++ Prettyp.print_judgment rhs_env j); *)
+(* with _ -> *)
+(* trace (str "Error in typed branch pretty printing")); *)
+ let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels'
+ and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in
+ let branch_name = id_of_string ("branch_" ^ (string_of_int !i)) in
+ let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in
+(* (try trace (str "Branch decl: " ++ pr_rel_decl env (Name branch_name, Some bbody, btype)) *)
+(* with _ -> trace (str "Error in branch decl pp")); *)
+ let branch =
+ let bref = RVar (dummy_loc, branch_name) in
+ match vars_of_ctx rhs_rels with
+ [] -> bref
+ | l -> RApp (dummy_loc, bref, l)
+ in
+(* let branch = *)
+(* List.fold_left (fun br (eqH, _, t) -> RLambda (dummy_loc, eqH, RHole (dummy_loc, Evd.InternalHole), br)) branch eqs_rels *)
+(* in *)
+(* (try trace (str "New branch: " ++ Printer.pr_rawconstr branch) *)
+(* with _ -> trace (str "Error in new branch pp")); *)
+ incr i;
+ let rhs = { eqn.rhs with it = branch } in
+ (branch_decl :: branches,
+ { eqn with patterns = newpatterns; rhs = rhs } :: eqns))
+ ([], []) eqns
+
+
+(* liftn_rel_declaration *)
+
+
+(* Builds the predicate. If the predicate is dependent, its context is
+ * made of 1+nrealargs assumptions for each matched term in an inductive
+ * type and 1 assumption for each term not _syntactically_ in an
+ * inductive type.
+
+ * Each matched terms are independently considered dependent or not.
+
+ * A type constraint but no annotation case: it is assumed non dependent.
+ *)
+
+let prepare_predicate_from_tycon loc typing_fun isevars env tomatchs arsign tycon =
+ (* We extract the signature of the arity *)
+(* List.iter *)
+(* (fun arsign -> *)
+(* trace (str "arity signature: " ++ my_print_rel_context env arsign)) *)
+(* arsign; *)
+(* let env = List.fold_right push_rels arsign env in *)
+ let allnames = List.rev (List.map (List.map pi1) arsign) in
+ let nar = List.fold_left (fun n names -> List.length names + n) 0 allnames in
+ let pred = out_some (valcon_of_tycon tycon) in
+ let predcclj, pred, neqs =
+ let _, _, eqs =
+ List.fold_left2
+ (fun (neqs, slift, eqs) ctx (tm,ty) ->
+ let len = List.length ctx in
+ let _name, _, _typ' = List.hd ctx in (* FixMe: Ignoring dependent inductives *)
+ let eq = mkApp (Lazy.force eq_ind,
+ [| lift (neqs + nar) (type_of_tomatch ty);
+ mkRel (neqs + slift);
+ lift (neqs + nar) tm|])
+ in
+ (succ neqs, slift - len, (Anonymous, None, eq) :: eqs))
+ (0, nar, []) (List.rev arsign) tomatchs
+ in
+ let len = List.length eqs in
+ it_mkProd_wo_LetIn (lift (nar + len) pred) eqs, pred, len
+ in
+ let predccl = nf_isevar !isevars predcclj in
+(* let env' = List.fold_right push_rel_context arsign env in *)
+(* trace (str " Env:" ++ my_print_env env' ++ str" Predicate: " ++ my_print_constr env' predccl); *)
+ build_initial_predicate true allnames predccl, pred
+
+let prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs sign tycon rtntyp =
+ (* We extract the signature of the arity *)
+ let arsign = extract_arity_signature env tomatchs sign in
+ let env = List.fold_right push_rels arsign env in
+ let allnames = List.rev (List.map (List.map pi1) arsign) in
+ let predcclj = typing_fun (mk_tycon (new_Type ())) env rtntyp in
+(* let _ = *)
+(* option_map (fun tycon -> *)
+(* isevars := Coercion.inh_conv_coerces_to loc env !isevars predcclj.uj_val *)
+(* (lift_tycon_type (List.length arsign) tycon)) *)
+(* tycon *)
+(* in *)
+ let predccl = (j_nf_isevar !isevars predcclj).uj_val in
+ Some (build_initial_predicate true allnames predccl)
+
+let lift_ctx n ctx =
+ let ctx', _ =
+ List.fold_right (fun (c, t) (ctx, n') -> (liftn n n' c, liftn_tomatch_type n n' t) :: ctx, succ n') ctx ([], 0)
+ in ctx'
+
+(* Turn matched terms into variables. *)
+let abstract_tomatch env tomatchs =
+ let prev, ctx, names =
+ List.fold_left
+ (fun (prev, ctx, names) (c, t) ->
+ let lenctx = List.length ctx in
+ match kind_of_term c with
+ Rel n -> (lift lenctx c, lift_tomatch_type lenctx t) :: prev, ctx, names
+ | _ ->
+ let name = next_ident_away_from (id_of_string "filtered_var") names in
+ (mkRel 1, lift_tomatch_type 1 t) :: lift_ctx 1 prev,
+ (Name name, Some (lift lenctx c), lift lenctx $ type_of_tomatch t) :: ctx,
+ name :: names)
+ ([], [], []) tomatchs
+ in List.rev prev, ctx
+
+(**************************************************************************)
+(* Main entry of the matching compilation *)
+
+let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns)=
+ let tycon0 = tycon in
+ (* We build the matrix of patterns and right-hand-side *)
+ let matx = matx_of_eqns env eqns in
+
+ (* We build the vector of terms to match consistently with the *)
+ (* constructors found in patterns *)
+ let tomatchs = coerce_to_indtype typing_fun isevars env matx tomatchl in
+ let tomatchs, tomatchs_lets = abstract_tomatch env tomatchs in
+ let tomatchs_len = List.length tomatchs_lets in
+ let tycon = lift_tycon tomatchs_len tycon in
+ let env = push_rel_context tomatchs_lets env in
+ match predopt with
+ None ->
+ let lets, matx = constrs_of_pats typing_fun tycon env isevars matx tomatchs in
+ let matx = List.rev matx in
+ let len = List.length lets in
+ let sign =
+ let arsign = extract_arity_signature env tomatchs (List.map snd tomatchl) in
+ List.map (lift_rel_context len) arsign
+ in
+ let env = push_rels lets env in
+ let matx = List.map (fun eqn -> { eqn with rhs = { eqn.rhs with rhs_env = env } }) matx in
+ let tycon = lift_tycon len tycon in
+ let tomatchs = List.map (fun (x, y) -> lift len x, lift_tomatch_type len y) tomatchs in
+ let args = List.map (fun (tm,ty) -> mk_refl (type_of_tomatch ty) tm) tomatchs in
+
+ (* We build the elimination predicate if any and check its consistency *)
+ (* with the type of arguments to match *)
+ let pred, opred = prepare_predicate_from_tycon loc typing_fun isevars env tomatchs sign tycon in
+ (* We push the initial terms to match and push their alias to rhs' envs *)
+ (* names of aliases will be recovered from patterns (hence Anonymous here) *)
+ let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in
+
+ let pb =
+ { env = env;
+ isevars = isevars;
+ pred = Some pred;
+ tomatch = initial_pushed;
+ history = start_history (List.length initial_pushed);
+ mat = matx;
+ caseloc = loc;
+ typing_function = typing_fun } in
+
+ let _, j = compile pb in
+ (* We check for unused patterns *)
+ List.iter (check_unused_pattern env) matx;
+ let ty = out_some (valcon_of_tycon tycon0) in
+ let body = it_mkLambda_or_LetIn (applistc j.uj_val args) lets in
+ let j =
+ { uj_val = it_mkLambda_or_LetIn body tomatchs_lets;
+ uj_type = ty; }
+ in
+ inh_conv_coerce_to_tycon loc env isevars j tycon0
+
+ | Some rtntyp ->
+ (* We build the elimination predicate if any and check its consistency *)
+ (* with the type of arguments to match *)
+ let tmsign = List.map snd tomatchl in
+ let pred = prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs tmsign tycon rtntyp in
+
+ (* We push the initial terms to match and push their alias to rhs' envs *)
+ (* names of aliases will be recovered from patterns (hence Anonymous here) *)
+ let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in
+
+ let pb =
+ { env = env;
+ isevars = isevars;
+ pred = pred;
+ tomatch = initial_pushed;
+ history = start_history (List.length initial_pushed);
+ mat = matx;
+ caseloc = loc;
+ typing_function = typing_fun } in
+
+ let _, j = compile pb in
+ (* We check for unused patterns *)
+ List.iter (check_unused_pattern env) matx;
+ let j = { j with uj_val = it_mkLambda_or_LetIn j.uj_val tomatchs_lets } in
+ inh_conv_coerce_to_tycon loc env isevars j tycon
+
+end
+
diff --git a/contrib/subtac/subtac_cases.mli b/contrib/subtac/subtac_cases.mli
new file mode 100644
index 00000000..9e902126
--- /dev/null
+++ b/contrib/subtac/subtac_cases.mli
@@ -0,0 +1,50 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i $Id: cases.mli 8741 2006-04-26 22:30:32Z herbelin $ i*)
+
+(*i*)
+open Util
+open Names
+open Term
+open Evd
+open Environ
+open Inductiveops
+open Rawterm
+open Evarutil
+(*i*)
+
+type pattern_matching_error =
+ | BadPattern of constructor * constr
+ | BadConstructor of constructor * inductive
+ | WrongNumargConstructor of constructor * int
+ | WrongNumargInductive of inductive * int
+ | WrongPredicateArity of constr * constr * constr
+ | NeedsInversion of constr * constr
+ | UnusedClause of cases_pattern list
+ | NonExhaustive of cases_pattern list
+ | CannotInferPredicate of (constr * types) array
+
+exception PatternMatchingError of env * pattern_matching_error
+
+val error_wrong_numarg_constructor_loc : loc -> env -> constructor -> int -> 'a
+
+val error_wrong_numarg_inductive_loc : loc -> env -> inductive -> int -> 'a
+
+(*s Compilation of pattern-matching. *)
+
+module type S = sig
+ val compile_cases :
+ loc ->
+ (type_constraint -> env -> rawconstr -> unsafe_judgment) * evar_defs ref ->
+ type_constraint ->
+ env -> rawconstr option * tomatch_tuple * cases_clauses ->
+ unsafe_judgment
+end
+
+module Cases_F(C : Coercion.S) : S
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index da5c497c..3613ec4f 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 9284 2006-10-26 12:06:57Z msozeau $ *)
+(* $Id: subtac_coercion.ml 9563 2007-01-31 09:37:18Z msozeau $ *)
open Util
open Names
@@ -53,8 +53,6 @@ module Coercion = struct
| _ -> None
and disc_exist 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
@@ -67,8 +65,6 @@ module Coercion = struct
let disc_proj_exist 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
@@ -108,27 +104,27 @@ module Coercion = struct
: (Term.constr -> Term.constr) option
=
let x = nf_evar (evars_of !isevars) x and y = nf_evar (evars_of !isevars) y in
- (try debug 1 (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 _ -> ());
+(* (try debug 1 (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 =
- (try debug 1 (str "coerce_unify from " ++ (my_print_constr env x) ++
- str " to "++ my_print_constr env y)
- with _ -> ());
+(* (try debug 1 (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;
- (try debug 1 (str "Unified " ++ (my_print_constr env x) ++
- str " and "++ my_print_constr env y);
- with _ -> ());
+(* (try debug 1 (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
- (try debug 1 (str "coerce' from " ++ (my_print_constr env x) ++
- str " to "++ my_print_constr env y);
- with _ -> ());
+(* (try debug 1 (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
@@ -158,11 +154,11 @@ module Coercion = struct
let existS = Lazy.force existS in
let prod = Lazy.force prod in
if len = Array.length l' && len = 2 && i = i'
+ && (i = Term.destInd existS.typ || i = Term.destInd prod.typ)
then
if i = Term.destInd existS.typ
then
begin
- trace (str "In coerce sigma types");
let (a, pb), (a', pb') =
pair_of_array l, pair_of_array l'
in
@@ -185,7 +181,6 @@ module Coercion = struct
let c2 = coerce_unify env' b b' in
match c1, c2 with
None, None ->
- trace (str "No coercion needed");
None
| _, _ ->
Some
@@ -198,9 +193,8 @@ module Coercion = struct
in
mkApp (existS.intro, [| a'; pb'; x ; y |]))
end
- else if i = Term.destInd prod.typ then
+ else
begin
- debug 1 (str "In coerce prod types");
let (a, b), (a', b') =
pair_of_array l, pair_of_array l'
in
@@ -219,14 +213,48 @@ module Coercion = struct
in
mkApp (prod.intro, [| a'; b'; x ; y |]))
end
- else subco ()
- else subco ()
- | _ -> subco ())
+ else
+ (* if len = 1 && len = Array.length l' && i = i' then *)
+(* let argx, argy = l.(0), l'.(0) in *)
+(* let indtyp = Inductiveops.type_of_inductive env i in *)
+(* let argname, argtype, _ = destProd indtyp in *)
+(* let eq = *)
+(* mkApp (Lazy.force eqind, [| argtype; argx; argy |]) *)
+(* in *)
+(* let pred = mkLambda (argname, argtype, *)
+(* mkApp (mkInd i, [| mkRel 1 |])) *)
+(* in *)
+(* let evar = make_existential dummy_loc env isevars eq in *)
+(* Some (fun x -> *)
+(* mkApp (Lazy.force eqrec, *)
+(* [| argtype; argx; pred; x; argy; evar |])) *)
+(* else *)subco ()
+ | x, y when x = y ->
+ let lam_type = Typing.type_of env (evars_of !isevars) c in
+ let rec coerce typ i co =
+ if i < Array.length l then
+ let hdx = l.(i) and hdy = l'.(i) in
+ let (n, eqT, restT) = destProd typ in
+ let pred = mkLambda (n, eqT, mkApp (lift 1 c, [| mkRel 1 |])) in
+ let eq = mkApp (Lazy.force eq_ind, [| eqT; hdx; hdy |]) in
+ let evar = make_existential dummy_loc env isevars eq in
+ let eq_app x = mkApp (Lazy.force eq_rect,
+ [| eqT; hdx; pred; x; hdy; evar|])
+ in
+ coerce (subst1 hdy restT) (succ i) (fun x -> eq_app (co x))
+ else co
+ in
+ if Array.length l = Array.length l' then (
+ trace (str"Inserting coercion at application");
+ Some (coerce lam_type 0 (fun x -> x))
+ ) else subco ()
+ | _ -> subco ())
| _, _ -> subco ()
and subset_coerce env isevars x y =
match disc_subset x with
Some (u, p) ->
+ (* trace (str "Inserting projection "); *)
let c = coerce_unify env u y in
let f x =
app_opt c (mkApp ((Lazy.force sig_).proj1,
@@ -372,13 +400,13 @@ module Coercion = struct
with Reduction.NotConvertible -> raise NoCoercion
let rec inh_conv_coerce_to_fail loc env isevars v t c1 =
- (try
- debug 1 (str "inh_conv_coerce_to_fail called for " ++
- Termops.print_constr_env env t ++ str " and "++ spc () ++
- Termops.print_constr_env env c1 ++ str " with evars: " ++ spc () ++
- Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
- Termops.print_env env);
- with _ -> ());
+(* (try *)
+(* debug 1 (str "inh_conv_coerce_to_fail called for " ++ *)
+(* Termops.print_constr_env env t ++ str " and "++ spc () ++ *)
+(* Termops.print_constr_env env c1 ++ str " with evars: " ++ spc () ++ *)
+(* Subtac_utils.pr_evar_defs isevars ++ str " in env: " ++ spc () ++ *)
+(* Termops.print_env env); *)
+(* with _ -> ()); *)
try (the_conv_x_leq env t c1 isevars, v, t)
with Reduction.NotConvertible ->
(try
@@ -437,14 +465,14 @@ module Coercion = struct
(* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
- let inh_conv_coerce_to loc env isevars cj ((n, t) as tycon) =
- (try
- debug 1 (str "Subtac_coercion.inh_conv_coerce_to called for " ++
- Termops.print_constr_env env cj.uj_type ++ str " and "++ spc () ++
- Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++
- Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
- Termops.print_env env);
- with _ -> ());
+ let inh_conv_coerce_to loc env isevars cj ((n, t) as _tycon) =
+(* (try *)
+(* trace (str "Subtac_coercion.inh_conv_coerce_to called for " ++ *)
+(* Termops.print_constr_env env cj.uj_type ++ str " and "++ spc () ++ *)
+(* Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++ *)
+(* Subtac_utils.pr_evar_defs isevars ++ str " in env: " ++ spc () ++ *)
+(* Termops.print_env env); *)
+(* with _ -> ()); *)
match n with
None ->
let (evd', val', type') =
@@ -462,40 +490,38 @@ module Coercion = struct
| Some (init, cur) ->
(isevars, cj)
- let inh_conv_coerces_to loc env isevars t ((abs, t') as tycon) =
- (try
- debug 1 (str "Subtac_coercion.inh_conv_coerces_to called for " ++
- Termops.print_constr_env env t ++ str " and "++ spc () ++
- Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++
- Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
- Termops.print_env env);
- with _ -> ());
+ let inh_conv_coerces_to loc env isevars t ((abs, t') as _tycon) =
+(* (try *)
+(* trace (str "Subtac_coercion.inh_conv_coerces_to called for " ++ *)
+(* Termops.print_constr_env env t ++ str " and "++ spc () ++ *)
+(* Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++ *)
+(* Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++ *)
+(* Termops.print_env env); *)
+(* with _ -> ()); *)
let nabsinit, nabs =
match abs with
None -> 0, 0
| Some (init, cur) -> init, cur
in
- let (rels, rng) =
(* a little more effort to get products is needed *)
- try decompose_prod_n nabs t
- with _ ->
- trace (str "decompose_prod_n failed");
- raise (Invalid_argument "Subtac_coercion.inh_conv_coerces_to")
- in
- (* The final range free variables must have been replaced by evars, we accept only that evars
- in rng are applied to free vars. *)
- if noccur_with_meta 0 (succ nabsinit) rng then (
- trace (str "No occur between 0 and " ++ int (succ nabsinit));
- let env', t, t' =
- let env' = List.fold_right (fun (n, t) env -> push_rel (n, None, t) env) rels env in
- env', rng, lift nabs t'
- in
- try
- pi1 (try inh_conv_coerce_to_fail loc env' isevars None t t'
- with NoCoercion ->
- coerce_itf loc env' isevars None t t')
- with NoSubtacCoercion ->
- let sigma = evars_of isevars in
- error_cannot_coerce env' sigma (t, t'))
- else isevars
+ try let rels, rng = decompose_prod_n nabs t in
+ (* The final range free variables must have been replaced by evars, we accept only that evars
+ in rng are applied to free vars. *)
+ if noccur_with_meta 0 (succ nabsinit) rng then (
+(* trace (str "No occur between 0 and " ++ int (succ nabsinit)); *)
+ let env', t, t' =
+ let env' = List.fold_right (fun (n, t) env -> push_rel (n, None, t) env) rels env in
+ env', rng, lift nabs t'
+ in
+ try
+ pi1 (try inh_conv_coerce_to_fail loc env' isevars None t t'
+ with NoCoercion ->
+ coerce_itf loc env' isevars None t t')
+ with NoSubtacCoercion ->
+ let sigma = evars_of isevars in
+ error_cannot_coerce env' sigma (t, t'))
+ else isevars
+ with _ -> isevars
+ (* trace (str "decompose_prod_n failed"); *)
+ (* raise (Invalid_argument "Subtac_coercion.inh_conv_coerces_to") *)
end
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index b433af2c..68ab8c46 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -57,7 +57,7 @@ let interp_gen kind isevars env
c =
let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars (Evd.evars_of !isevars) env c in
let c' = Subtac_utils.rewrite_cases env c' in
- (try trace (str "Pretyping " ++ my_print_constr_expr c) with _ -> ());
+(* (try trace (str "Pretyping " ++ my_print_constr_expr c) with _ -> ()); *)
let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in
evar_nf isevars c'
@@ -150,14 +150,6 @@ let collect_non_rec env =
in
searchrec []
-
-let filter_map f l =
- let rec aux acc = function
- hd :: tl -> (match f hd with Some t -> aux (t :: acc) tl
- | None -> aux acc tl)
- | [] -> List.rev acc
- in aux [] l
-
let list_of_local_binders l =
let rec aux acc = function
Topconstr.LocalRawDef (n, c) :: tl -> aux ((n, Some c, None) :: acc) tl
@@ -176,25 +168,29 @@ let rec gen_rels = function
0 -> []
| n -> mkRel n :: gen_rels (pred n)
+let split_args n rel = match list_chop ((List.length rel) - n) rel with
+ (l1, x :: l2) -> l1, x, l2
+ | _ -> assert(false)
+
let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
let sigma = Evd.empty in
let isevars = ref (Evd.create_evar_defs sigma) in
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 "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)
- with _ -> ()
- 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 _ = *)
+(* 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) *)
+(* with _ -> () *)
+ (* in *)
let env', binders_rel = interp_context isevars env bl in
- let after, ((argname, _, argtyp) as arg), before = list_chop_hd (succ n) binders_rel in
+ let after, ((argname, _, argtyp) as arg), before = split_args (succ n) binders_rel in
let before_length, after_length = List.length before, List.length after in
let argid = match argname with Name n -> n | _ -> assert(false) in
let _liftafter = lift_binders 1 after_length after in
@@ -226,15 +222,14 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
in
let argid' = id_of_string (string_of_id argid ^ "'") in
let wfarg len = (Name argid', None,
- mkSubset (Name argid') argtyp
+ mkSubset (Name argid') (lift len 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
let top_env = push_rel_context top_bl env in
- let intern_env = push_rel_context intern_bl env in
+ let _intern_env = push_rel_context intern_bl env in
let top_arity = interp_type isevars top_env arityc in
- (try debug 2 (str "Intern bl: " ++ prr intern_bl) with _ -> ());
let proj = (Lazy.force sig_).Coqlib.proj1 in
let projection =
mkApp (proj, [| argtyp ;
@@ -243,32 +238,32 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
mkRel 1
|])
in
- (try debug 2 (str "Top arity: " ++ my_print_constr top_env top_arity) with _ -> ());
+ (* (try debug 2 (str "Top arity: " ++ my_print_constr top_env top_arity) with _ -> ()); *)
let intern_arity = substnl [projection] after_length top_arity in
- (try debug 2 (str "Top arity after subst: " ++ my_print_constr intern_env intern_arity) with _ -> ());
+(* (try debug 2 (str "Top arity after subst: " ++ my_print_constr intern_env intern_arity) with _ -> ()); *)
let intern_before_env = push_rel_context before env in
let intern_fun_bl = after @ [wfarg 1] in
- (try debug 2 (str "Intern fun bl: " ++ prr intern_fun_bl) with _ -> ());
+(* (try debug 2 (str "Intern fun bl: " ++ prr intern_fun_bl) with _ -> ()); *)
let intern_fun_arity = intern_arity in
- (try debug 2 (str "Intern fun arity: " ++
- my_print_constr intern_env intern_fun_arity) with _ -> ());
+(* (try debug 2 (str "Intern fun arity: " ++ *)
+(* my_print_constr intern_env intern_fun_arity) with _ -> ()); *)
let intern_fun_arity_prod = it_mkProd_or_LetIn intern_fun_arity intern_fun_bl in
let intern_fun_binder = (Name recname, None, intern_fun_arity_prod) in
let fun_bl = after @ (intern_fun_binder :: [arg]) in
- (try debug 2 (str "Fun bl: " ++ pr_rel intern_before_env fun_bl ++ spc ()) with _ -> ());
+(* (try debug 2 (str "Fun bl: " ++ pr_rel intern_before_env fun_bl ++ spc ()) with _ -> ()); *)
let fun_env = push_rel_context fun_bl intern_before_env in
let fun_arity = interp_type isevars fun_env arityc in
let intern_body = interp_casted_constr isevars fun_env body fun_arity in
let intern_body_lam = it_mkLambda_or_LetIn intern_body fun_bl in
- let _ =
- try debug 2 (str "Fun bl: " ++ prr fun_bl ++ spc () ++
- str "Intern bl" ++ prr intern_bl ++ spc () ++
- str "Top bl" ++ prr top_bl ++ spc () ++
- str "Intern arity: " ++ pr intern_arity ++
- str "Top arity: " ++ pr top_arity ++ spc () ++
- str "Intern body " ++ pr intern_body_lam)
- with _ -> ()
- in
+(* let _ = *)
+(* try debug 2 (str "Fun bl: " ++ prr fun_bl ++ spc () ++ *)
+(* str "Intern bl" ++ prr intern_bl ++ spc () ++ *)
+(* str "Top bl" ++ prr top_bl ++ spc () ++ *)
+(* str "Intern arity: " ++ pr intern_arity ++ *)
+(* str "Top arity: " ++ pr top_arity ++ spc () ++ *)
+(* str "Intern body " ++ pr intern_body_lam) *)
+(* with _ -> () *)
+(* in *)
let _impl =
if Impargs.is_implicit_args()
then Impargs.compute_implicits top_env top_arity
@@ -292,53 +287,48 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
let def_appl = applist (fix_def, gen_rels (after_length + 1)) in
let def = it_mkLambda_or_LetIn def_appl binders_rel in
let typ = it_mkProd_or_LetIn top_arity binders_rel in
- debug 2 (str "Constructed def");
- debug 2 (my_print_constr intern_before_env def);
- debug 2 (str "Type: " ++ my_print_constr env typ);
let fullcoqc = Evarutil.nf_isevar !isevars def in
let fullctyp = Evarutil.nf_isevar !isevars typ in
- 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 _ = 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 _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in
+ (* let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in *)
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")
-(*
+ (* (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 _ -> ()); *)
+ Subtac_obligations.add_definition recname evars_def fullctyp evars
+
let build_mutrec l boxed =
- let sigma = Evd.empty
- and env0 = Global.env()
- in
+ let sigma = Evd.empty and env = Global.env () in
+ let nc = named_context env in
+ let nc_len = named_context_length nc in
let lnameargsardef =
- (*List.map (fun (f, d) -> Subtac_interp_fixpoint.rewrite_fixpoint env0 protos (f, d))*)
+ (*List.map (fun (f, d) -> Subtac_interp_fixpoint.rewrite_fixpoint env protos (f, d))*)
l
in
let lrecnames = List.map (fun ((f,_,_,_,_),_) -> f) lnameargsardef
and nv = List.map (fun ((_,n,_,_,_),_) -> n) lnameargsardef
in
(* Build the recursive context and notations for the recursive types *)
- let (rec_sign,rec_impls,arityl) =
+ let (rec_sign,rec_env,rec_impls,arityl) =
List.fold_left
- (fun (env,impls,arl) ((recname, n, bl,arityc,body),_) ->
+ (fun (sign,env,impls,arl) ((recname, n, bl,arityc,body),_) ->
let isevars = ref (Evd.create_evar_defs sigma) in
let arityc = Command.generalize_constr_expr arityc bl in
- let arity = interp_type isevars env0 arityc in
+ let arity = interp_type isevars env arityc in
let impl =
if Impargs.is_implicit_args()
- then Impargs.compute_implicits env0 arity
+ then Impargs.compute_implicits env arity
else [] in
let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in
- (Environ.push_named (recname,None,arity) env, impls', (isevars, None, arity)::arl))
- (env0,[],[]) lnameargsardef in
+ ((recname,None,arity) :: sign, Environ.push_named (recname,None,arity) env, impls', (isevars, None, arity)::arl))
+ ([],env,[],[]) lnameargsardef in
let arityl = List.rev arityl in
let notations =
List.fold_right (fun (_,ntnopt) l -> option_cons ntnopt l)
@@ -357,11 +347,11 @@ let build_mutrec l boxed =
match info with
None ->
let def = abstract_constr_expr def bl in
- isevars, info, interp_casted_constr isevars rec_sign ~impls:([],rec_impls)
+ isevars, info, interp_casted_constr isevars rec_env ~impls:([],rec_impls)
def arity
| Some (n, artyp, wfrel, fun_bl, intern_bl, intern_arity) ->
- let rec_sign = push_rel_context fun_bl rec_sign in
- let cstr = interp_casted_constr isevars rec_sign ~impls:([],rec_impls)
+ let rec_env = push_rel_context fun_bl rec_env in
+ let cstr = interp_casted_constr isevars rec_env ~impls:([],rec_impls)
def intern_arity
in isevars, info, it_mkLambda_or_LetIn cstr fun_bl)
lnameargsardef arityl
@@ -369,162 +359,33 @@ let build_mutrec l boxed =
States.unfreeze fs; raise e in
States.unfreeze fs; def
in
-
let (lnonrec,(namerec,defrec,arrec,nvrec)) =
- collect_non_rec env0 lrecnames recdef arityl nv in
- 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 =
- (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);
- const_entry_opaque = false;
- const_entry_boxed = boxed} in
- let kn = Declare.declare_constant fi (DefinitionEntry ce,IsDefinition Fixpoint)
- in (ConstRef kn)
- in
- (* declare the recursive definitions *)
- let lrefrec = Array.mapi declare namerec in
- Options.if_verbose ppnl (recursive_message lrefrec);
-
-
- (*(* The others are declared as normal definitions *)
- let var_subst id = (id, Constrintern.global_reference id) in
- let _ =
- List.fold_left
- (fun subst (f,def,t) ->
- let ce = { const_entry_body = replace_vars subst def;
- const_entry_type = Some t;
- const_entry_opaque = false;
- const_entry_boxed = boxed } in
- let _ =
- Declare.declare_constant f (DefinitionEntry ce,IsDefinition Definition)
- in
- warning ((string_of_id f)^" is non-recursively defined");
- (var_subst f) :: subst)
- (List.map var_subst (Array.to_list namerec))
- lnonrec
- in*)
- List.iter (fun (df,c,scope) ->
- Metasyntax.add_notation_interpretation df [] c scope) notations
- in
- let declare l =
- let recvec = Array.of_list l
- and arrec = Array.map pi3 arrec
- in declare arrec recvec
- in
+ collect_non_rec env lrecnames recdef arityl nv in
let recdefs = Array.length defrec in
- trace (int recdefs ++ str " recursive definitions");
(* Solve remaining evars *)
let rec collect_evars i acc =
if i < recdefs then
let (isevars, info, def) = defrec.(i) in
- let _ = try trace (str "In solve evars, isevars is: " ++ Evd.pr_evar_defs !isevars) with _ -> () 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 _ = try trace (str "In solve evars, undefined is: " ++ Evd.pr_evar_defs isevars) with _ -> () 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
- (* Generalize by the recursive prototypes *)
+ (* Generalize by the recursive prototypes *)
let def =
- Termops.it_mkNamedLambda_or_LetIn def (Environ.named_context rec_sign)
+ Termops.it_mkNamedLambda_or_LetIn def rec_sign
and typ =
- Termops.it_mkNamedProd_or_LetIn typ (Environ.named_context rec_sign)
+ Termops.it_mkNamedProd_or_LetIn typ 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 =
- { const_entry_body = evars_def;
- const_entry_type = Some evars_typ;
- const_entry_opaque = false;
- const_entry_boxed = boxed} in
- let kn = Declare.declare_constant fi (DefinitionEntry ce,IsDefinition Definition) in
- definition_message fi;
- trace (str (string_of_id fi) ++ str " is defined");*)
- let evar_sum =
- if evars = [] then None
- 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
- (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)
+ let evars, def = Eterm.eterm_obligations id nc_len evm def (Some typ) in
+ collect_evars (succ i) ((id, def, typ, evars) :: acc)
else acc
in
let defs = collect_evars 0 [] in
-
- (* Solve evars then create the definitions *)
- let real_evars =
- filter_map (fun (id, kn, sum) ->
- match sum with Some (sumtac, sumg) -> Some (id, kn, sumg, sumtac) | None -> None)
- defs
- in
- match real_evars with
- [] -> declare (List.rev_map (fun (id, c, _) ->
- snd (decompose_lam_n recdefs c)) defs)
- | l ->
-
- Subtac_utils.and_tac real_evars
- (fun f _ gr ->
- 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
- (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) ->
- let (id, kn, sumg, pi), pis = List.hd pis, List.tl pis in
- let args = Subtac_utils.destruct_ex pi sumg in
- let args =
- List.map (fun c ->
- try Reductionops.whd_betadeltaiota (Global.env ()) Evd.empty c
- with Not_found ->
- trace (str "Not_found while reducing " ++
- my_print_constr (Global.env ()) c);
- c
- ) args
- in
- let _, newdef = decompose_lam_n (recdefs + List.length args) kn in
- let constr = Term.substl (mkRel 1 :: List.rev args) newdef in
- aux pis (constr :: acc) tl)
- | [] -> List.rev acc
- in
- declare (aux pis [] defs)
- with Environ.NotEvaluableConst cer ->
- match cer with
- Environ.NoBody -> trace (str "Constant has no body")
- | Environ.Opaque -> trace (str "Constant is opaque")
- )
-*)
+ Subtac_obligations.add_mutual_definitions (List.rev defs) nvrec
+
let out_n = function
Some n -> n
| None -> 0
@@ -544,8 +405,7 @@ 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 assert(false)
- (*build_mutrec lnameargsardef boxed*)
+ in build_mutrec lnameargsardef boxed
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 7b13b402..d6c1772f 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -12,6 +12,8 @@ open Decl_kinds
open Util
open Evd
+type obligation_info = (Names.identifier * Term.types * Intset.t) array
+
type obligation =
{ obl_name : identifier;
obl_type : types;
@@ -24,15 +26,42 @@ type obligations = (obligation array * int)
type program_info = {
prg_name: identifier;
prg_body: constr;
- prg_type: types;
+ prg_type: constr;
prg_obligations: obligations;
+ prg_deps : identifier list;
+ prg_nvrec : int array;
}
-let evar_of_obligation o = { evar_hyps = Environ.empty_named_context_val ;
+let assumption_message id =
+ Options.if_verbose message ((string_of_id id) ^ " is assumed")
+
+let default_tactic : Proof_type.tactic ref = ref Refiner.tclIDTAC
+
+let set_default_tactic t = default_tactic := t
+
+let evar_of_obligation o = { evar_hyps = Global.named_context_val () ;
evar_concl = o.obl_type ;
evar_body = Evar_empty ;
evar_extra = None }
+let subst_deps obls deps t =
+ Intset.fold
+ (fun x acc ->
+ let xobl = obls.(x) in
+ debug 3 (str "Trying to get body of obligation " ++ int x);
+ let oblb =
+ try out_some xobl.obl_body
+ with _ ->
+ debug 3 (str "Couldn't get body of obligation " ++ int x);
+ assert(false)
+ in
+ Term.subst1 oblb (Term.subst_var xobl.obl_name acc))
+ deps t
+
+let subst_deps_obl obls obl =
+ let t' = subst_deps obls obl.obl_deps obl.obl_type in
+ { obl with obl_type = t' }
+
module ProgMap = Map.Make(struct type t = identifier let compare = compare end)
let map_replace k v m = ProgMap.add k v (ProgMap.remove k m)
@@ -62,21 +91,6 @@ let _ =
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 =
@@ -88,14 +102,72 @@ let terms_of_evar ev =
body, typ
| _ -> assert(false)
+let rec intset_to = function
+ -1 -> Intset.empty
+ | n -> Intset.add n (intset_to (pred n))
+
+let subst_body prg =
+ let obls, _ = prg.prg_obligations in
+ subst_deps obls (intset_to (pred (Array.length obls))) prg.prg_body
+
+let declare_definition prg =
+ let body = subst_body prg in
+ (try trace (str "Declaring: " ++ Ppconstr.pr_id prg.prg_name ++ spc () ++
+ my_print_constr (Global.env()) body);
+ with _ -> ());
+ let ce =
+ { const_entry_body = 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 Pp
+open Ppconstr
+
+let declare_mutual_definition l =
+ let len = List.length l in
+ let namerec = Array.of_list (List.map (fun x -> x.prg_name) l) in
+ let arrec =
+ Array.of_list (List.map (fun x -> snd (decompose_prod_n len x.prg_type)) l)
+ in
+ let recvec =
+ Array.of_list
+ (List.map (fun x ->
+ let subs = (subst_body x) in
+ snd (decompose_lam_n len subs)) l)
+ in
+ let nvrec = (List.hd l).prg_nvrec in
+ let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in
+ let rec declare i fi =
+ (try trace (str "Declaring: " ++ pr_id fi ++ spc () ++
+ my_print_constr (Global.env()) (recvec.(i)));
+ with _ -> ());
+ let ce =
+ { const_entry_body = mkFix ((nvrec,i),recdecls);
+ const_entry_type = Some arrec.(i);
+ const_entry_opaque = false;
+ const_entry_boxed = true} in
+ let kn = Declare.declare_constant fi (DefinitionEntry ce,IsDefinition Fixpoint)
+ in
+ ConstRef kn
+ in
+ let lrefrec = Array.mapi declare namerec in
+ Options.if_verbose ppnl (recursive_message lrefrec)
+
let declare_obligation obl body =
let ce =
{ const_entry_body = body;
const_entry_type = Some obl.obl_type;
- const_entry_opaque = true;
+ const_entry_opaque = false;
const_entry_boxed = false}
in
- let constant = Declare.declare_constant obl.obl_name (DefinitionEntry ce,IsProof Property)
+ 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) }
@@ -113,36 +185,30 @@ let try_tactics obls =
| _ -> 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
+let red = Reductionops.nf_betaiota
+
+let init_prog_info n b t deps nvrec obls =
+ let obls' =
+ Array.mapi
+ (fun i (n, t, d) ->
+ debug 2 (str "Adding obligation " ++ int i ++ str " with deps : " ++ str (string_of_intset d));
+ { obl_name = n ; obl_body = None;
+ obl_type = red t;
+ obl_deps = d })
+ obls
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
+ { prg_name = n ; prg_body = b; prg_type = red t; prg_obligations = (obls', Array.length obls');
+ prg_deps = deps; prg_nvrec = nvrec; }
+
+let pperror cmd = Util.errorlabstrm "Subtac" cmd
+let error s = pperror (str s)
let get_prog name =
let prg_infos = !from_prg in
match name with
- Some n -> ProgMap.find n prg_infos
+ Some n ->
+ (try ProgMap.find n prg_infos
+ with Not_found -> error ("No obligations for program " ^ string_of_id n))
| None ->
(let n = map_cardinal prg_infos in
match n with
@@ -150,57 +216,67 @@ let get_prog name =
| 1 -> map_first prg_infos
| _ -> error "More than one program with unsolved obligations")
+let obligations_solved prg = (snd prg.prg_obligations) = 0
+
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)
+ from_prg := map_replace prg.prg_name prg' !from_prg;
+ if rem > 0 then (
+ Options.if_verbose msgnl (int rem ++ str " obligation(s) remaining");
+ )
else (
- declare_definition prg';
- from_prg := ProgMap.remove prg.prg_name !from_prg
- )
+ Options.if_verbose msgnl (str "No more obligations remaining");
+ match prg'.prg_deps with
+ [] ->
+ declare_definition prg';
+ from_prg := ProgMap.remove prg.prg_name !from_prg
+ | l ->
+ let progs = List.map (fun x -> ProgMap.find x !from_prg) prg'.prg_deps in
+ if List.for_all (fun x -> obligations_solved x) progs then
+ (declare_mutual_definition progs;
+ from_prg := List.fold_left
+ (fun acc x -> ProgMap.remove x.prg_name acc) !from_prg progs))
let is_defined obls x = obls.(x).obl_body <> None
-let deps_remaining obls x =
- let deps = obls.(x).obl_deps in
+let deps_remaining obls deps =
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 solve_obligation prg num =
+ let user_num = succ num in
+ let obls, rem = prg.prg_obligations in
+ let obl = obls.(num) in
+ if obl.obl_body <> None then
+ pperror (str "Obligation" ++ spc () ++ int user_num ++ str "already" ++ spc() ++ str "solved.")
+ else
+ match deps_remaining obls obl.obl_deps with
+ [] ->
+ let obl = subst_deps_obl obls obl in
+ Command.start_proof obl.obl_name 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: " ++
+ Subtac_utils.my_print_constr (Global.env ()) obl.obl_type);
+ Pfedit.by !default_tactic
+ | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
+ ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l))
+
+let subtac_obligation (user_num, name, typ) =
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)))
+ None -> solve_obligation prg num
| Some r -> error "Obligation already solved"
else error (sprintf "Unknown obligation number %i" (succ num))
@@ -217,33 +293,102 @@ let obligations_of_evars evars =
}) evars)
in arr, Array.length arr
+let solve_obligation_by_tac prg obls i tac =
+ let obl = obls.(i) in
+ match obl.obl_body with
+ Some _ -> false
+ | None ->
+ (try
+ if deps_remaining obls obl.obl_deps = [] then
+ let obl = subst_deps_obl obls obl in
+ let t = Subtac_utils.solve_by_tac (evar_of_obligation obl) tac in
+ obls.(i) <- { obl with obl_body = Some t };
+ true
+ else false
+ with _ -> false)
+
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.copy obls in
+ let _ =
+ Array.iteri (fun i x ->
+ if solve_obligation_by_tac prg obls' i tac then
+ decr rem)
+ obls'
+ in
+ update_obls prg obls' !rem
+
+let add_definition n b t obls =
+ Options.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
+ let prg = init_prog_info n b t [] (Array.make 0 0) obls in
+ let obls,_ = prg.prg_obligations in
+ if Array.length obls = 0 then (
+ Options.if_verbose ppnl (str ".");
+ declare_definition prg;
+ from_prg := ProgMap.remove prg.prg_name !from_prg)
+ else (
+ let len = Array.length obls in
+ let _ = Options.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in
+ from_prg := ProgMap.add n prg !from_prg;
+ solve_obligations (Some n) !default_tactic)
+
+let add_mutual_definitions l nvrec =
+ let deps = List.map (fun (n, b, t, obls) -> n) l in
+ let upd = List.fold_left
+ (fun acc (n, b, t, obls) ->
+ let prg = init_prog_info n b t deps nvrec obls in
+ ProgMap.add n prg acc)
+ !from_prg l
+ in
+ from_prg := upd;
+ List.iter (fun x -> solve_obligations (Some x) !default_tactic) deps
+
+let admit_obligations n =
+ let prg = get_prog n in
+ let obls, rem = prg.prg_obligations in
let obls' =
- Array.map (fun x ->
+ Array.mapi (fun i 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)
+ None ->
+ let kn = Declare.declare_constant x.obl_name (ParameterEntry x.obl_type, IsAssumption Conjectural) in
+ assumption_message x.obl_name;
+ { x with obl_body = Some (mkConst kn) }
+ | Some _ -> x)
obls
in
- update_obls prg obls' !rem
+ update_obls prg obls' 0
+exception Found of int
+
+let array_find f arr =
+ try Array.iteri (fun i x -> if f x then raise (Found i)) arr;
+ raise Not_found
+ with Found i -> i
+
+let rec next_obligation n =
+ let prg = get_prog n in
+ let obls, rem = prg.prg_obligations in
+ let i =
+ array_find (fun x -> x.obl_body = None && deps_remaining obls x.obl_deps = [])
+ obls
+ in
+ if solve_obligation_by_tac prg obls i !default_tactic then (
+ update_obls prg obls (pred rem);
+ next_obligation n
+ ) else solve_obligation prg i
+
open Pp
let show_obligations n =
let prg = get_prog n in
+ let n = prg.prg_name 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)
+ None -> msgnl (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++ str "of" ++ spc() ++ str (string_of_id n) ++ str ":" ++ spc () ++
+ my_print_constr (Global.env ()) x.obl_type ++ str "." ++ fnl ())
| Some _ -> ())
obls
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli
index 7d93d57b..3981d4c6 100644
--- a/contrib/subtac/subtac_obligations.mli
+++ b/contrib/subtac/subtac_obligations.mli
@@ -1,10 +1,21 @@
open Util
-val add_entry : Names.identifier -> Term.constr -> Term.types ->
- (Names.identifier * Term.types * Intset.t) array -> unit
+type obligation_info = (Names.identifier * Term.types * Intset.t) array
-val subtac_obligation : int * Names.identifier option -> unit
+val set_default_tactic : Proof_type.tactic -> unit
+
+val add_definition : Names.identifier -> Term.constr -> Term.types ->
+ obligation_info -> unit
+
+val add_mutual_definitions :
+ (Names.identifier * Term.constr * Term.types * obligation_info) list -> int array -> unit
+
+val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr option -> unit
+
+val next_obligation : Names.identifier option -> unit
val solve_obligations : Names.identifier option -> Proof_type.tactic -> unit
val show_obligations : Names.identifier option -> unit
+
+val admit_obligations : Names.identifier option -> unit
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index a243ba34..4d1ac731 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 9326 2006-10-31 12:57:26Z msozeau $ *)
+(* $Id: subtac_pretyping.ml 9563 2007-01-31 09:37:18Z msozeau $ *)
open Global
open Pp
@@ -113,29 +113,23 @@ let env_with_binders env isevars l =
in aux (env, []) l
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 _ = 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 _ = 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 _ = 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 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 _ = try trace (str "Interpreted term: " ++ my_print_constr env_binders coqc ++ spc () ++
- str "Coq type: " ++ my_print_constr env_binders ctyp)
- with _ -> ()
- in
- let _ = try trace (str "Original evar map: " ++ Evd.pr_evar_map (evars ())) with _ -> () in
+(* 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 _ = 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
@@ -143,13 +137,13 @@ 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 _ = 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 _ = 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 _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in
+(* let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in *)
evm, fullcoqc, fullctyp
open Subtac_obligations
@@ -159,5 +153,4 @@ let subtac_proof env isevars id l c tycon =
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
+ add_definition id def coqt evars
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index 46af5886..6244aef3 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 9316 2006-10-29 22:49:11Z herbelin $ *)
+(* $Id: subtac_pretyping_F.ml 9563 2007-01-31 09:37:18Z msozeau $ *)
open Pp
open Util
@@ -40,7 +40,7 @@ open Inductiveops
module SubtacPretyping_F (Coercion : Coercion.S) = struct
- module Cases = Cases.Cases_F(Coercion)
+ module Cases = Subtac_cases.Cases_F(Coercion)
(* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
let allow_anonymous_refs = ref true
@@ -161,7 +161,12 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
(* [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
+ let rec pretype (tycon : type_constraint) env isevars lvar c =
+(* let _ = try Subtac_utils.trace (str "pretype " ++ Subtac_utils.my_print_rawconstr env c ++ *)
+(* str " with tycon " ++ Evarutil.pr_tycon env tycon) *)
+(* with _ -> () *)
+(* in *)
+ match c with
| RRef (loc,ref) ->
inh_conv_coerce_to_tycon loc env isevars
(pretype_ref isevars env ref)
@@ -321,7 +326,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
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
+ 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
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 7b96758a..01dee3e9 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -5,6 +5,8 @@ open Term
open Names
open Util
+let ($) f x = f x
+
(****************************************************************************)
(* Library linking *)
@@ -45,10 +47,23 @@ let build_sig () =
let sig_ = lazy (build_sig ())
-let eqind = lazy (init_constant ["Init"; "Logic"] "eq")
-let eqind_ref = lazy (init_reference ["Init"; "Logic"] "eq")
+let eq_ind = lazy (init_constant ["Init"; "Logic"] "eq")
+let eq_rec = lazy (init_constant ["Init"; "Logic"] "eq_rec")
+let eq_rect = lazy (init_constant ["Init"; "Logic"] "eq_rect")
+let eq_refl = lazy (init_constant ["Init"; "Logic"] "refl_equal")
+let eq_ind_ref = lazy (init_reference ["Init"; "Logic"] "eq")
let refl_equal_ref = lazy (init_reference ["Init"; "Logic"] "refl_equal")
+let eqdep_ind = lazy (init_constant [ "Logic";"Eqdep"] "eq_dep")
+let eqdep_rec = lazy (init_constant ["Logic";"Eqdep"] "eq_dep_rec")
+let eqdep_ind_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep")
+let eqdep_intro_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep_intro")
+
+let jmeq_ind = lazy (init_constant ["Logic";"JMeq"] "JMeq")
+let jmeq_rec = lazy (init_constant ["Logic";"JMeq"] "JMeq_rec")
+let jmeq_ind_ref = lazy (init_reference ["Logic";"JMeq"] "JMeq")
+let jmeq_refl_ref = lazy (init_reference ["Logic";"JMeq"] "JMeq_refl")
+
let ex_ind = lazy (init_constant ["Init"; "Logic"] "ex")
let ex_intro = lazy (init_reference ["Init"; "Logic"] "ex_intro")
@@ -79,6 +94,7 @@ open Pp
let my_print_constr = Termops.print_constr_env
let my_print_constr_expr = Ppconstr.pr_constr_expr
+let my_print_rel_context env ctx = Printer.pr_rel_context env ctx
let my_print_context = Termops.print_rel_context
let my_print_named_context = Termops.print_named_context
let my_print_env = Termops.print_env
@@ -87,7 +103,7 @@ let my_print_evardefs = Evd.pr_evar_defs
let my_print_tycon_type = Evarutil.pr_tycon_type
-let debug_level = 1
+let debug_level = 2
let debug_on = true
@@ -132,8 +148,9 @@ 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
- (try debug 2 (str "Constructed evar " ++ int key ++ str " applied to args: " ++
- print_args env args) with _ -> ());
+ (try trace (str "Constructed evar " ++ int key ++ str " applied to args: " ++
+ print_args env args ++ str " for type: "++
+ my_print_constr env c) with _ -> ());
evar
let make_existential_expr loc env c =
@@ -177,6 +194,12 @@ open Tactics
open Tacticals
let id x = x
+let filter_map f l =
+ let rec aux acc = function
+ hd :: tl -> (match f hd with Some t -> aux (t :: acc) tl
+ | None -> aux acc tl)
+ | [] -> List.rev acc
+ in aux [] l
let build_dependent_sum l =
let rec aux names conttac conttype = function
@@ -279,45 +302,137 @@ let destruct_ex ext ex =
open Rawterm
-
+let rec concatMap f l =
+ match l with
+ hd :: tl -> f hd @ concatMap f tl
+ | [] -> []
+
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 make_discr (loc, po, tml, eqns) =
let mkHole = RHole (dummy_loc, InternalHole) in
- let mkeq c n = RApp (dummy_loc, RRef (dummy_loc, (Lazy.force eqind_ref)),
- [mkHole; c; n])
+
+ let rec vars_of_pat = function
+ RPatVar (loc, n) -> (match n with Anonymous -> [] | Name n -> [n])
+ | RPatCstr (loc, csrt, pats, _) ->
+ concatMap vars_of_pat pats
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
+ let rec constr_of_pat l = function
+ RPatVar (loc, n) ->
+ (match n with
+ Anonymous ->
+ let n = next_name_away_from "x" l in
+ RVar n, (n :: l)
+ | Name n -> RVar n, l)
+ | RPatCstr (loc, csrt, pats, _) ->
+ let (args, vars) =
+ List.fold_left
+ (fun (args, vars) x ->
+ let c, vars = constr_of_pat vars x in
+ c :: args, vars)
+ ([], l) pats
+ in
+ RApp ((RRef (dummy_loc, ConstructRef cstr)), args), vars
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)
+ let rec constr_of_pat l = function
+ RPatVar (loc, n) ->
+ (match n with
+ Anonymous ->
+ let n = next_name_away_from "x" l in
+ RVar n, (n :: l)
+ | Name n -> RVar n, l)
+ | RPatCstr (loc, csrt, pats, _) ->
+ let (args, vars) =
+ List.fold_left
+ (fun (args, vars) x ->
+ let c, vars = constr_of_pat vars x in
+ c :: args, vars)
+ ([], l) pats
+ in
+ RApp ((RRef (dummy_loc, ConstructRef cstr)), args), vars
in
- let eqns =
- List.map (fun (loc, idl, cpl, c) ->
+ let constrs_of_pats v l =
+ List.fold_left
+ (fun (v, acc) x ->
+ let x', v' = constr_of_pat v x in
+ (l', v' :: acc))
+ (v, []) l
+ in
+ let rec pat_of_pat l = function
+ RPatVar (loc, n) ->
+ let n', l = match n with
+ Anonymous ->
+ let n = next_name_away_from "x" l in
+ n, n :: l
+ | Name n -> n, n :: l
+ in
+ RPatVar (loc, Name n'), l
+ | RPatCstr (loc, cstr, pats, (loc, alias)) ->
+ let args, vars, s =
+ List.fold_left (fun (args, vars) x ->
+ let pat', vars = pat_of_pat vars pat in
+ pat' :: args, vars)
+ ([], alias :: l) pats
+ in RPatCstr (loc, cstr, args, (loc, alias)), vars
+ in
+ let pats_of_pats l =
+ List.fold_left
+ (fun (v, acc) x ->
+ let x', v' = pat_of_pat v x in
+ (v', x' :: acc))
+ ([], []) l
+ in
+ let eq_of_pat p used c =
+ let constr, vars' = constr_of_pat used p in
+ let eq = RApp (dummy_loc, RRef (dummy_loc, Lazy.force eqind_ref), [mkHole; constr; c]) in
+ vars', eq
+ in
+ let eqs_of_pats ps used cstrs =
+ List.fold_left2
+ (fun (vars, eqs) pat c ->
+ let (vars', eq) = eq_of_pat pat c in
+ match eqs with
+ None -> Some eq
+ | Some eqs ->
+ Some (RApp (dummy_loc, RRef (dummy_loc, Lazy.force and_ref), [eq, eqs])))
+ (used, None) ps cstrs
+ in
+ let quantify c l =
+ List.fold_left
+ (fun acc name -> RProd (dummy_loc, name, mkHole, acc))
+ c l
+ in
+ let quantpats =
+ List.fold_left
+ (fun (acc, pats) ((loc, idl, cpl, c) as x) ->
+ let vars, cpl = pats_of_pats cpl in
+ let l', constrs = constrs_of_pats vars cpl in
+ let discrs =
+ List.map (fun (_, _, cpl', _) ->
+ let qvars, eqs = eqs_of_pats cpl' l' constrs in
+ let neg = RApp (dummy_loc, RRef (dummy_loc, Lazy.force not_ref), [out_some eqs]) in
+ let pat_ineq = quantify qvars neg in
+
+ )
+ pats in
+
+
+
+
+
+
+
+ (x, pat_ineq))
+ in
+ List.fold_left
+ (fun acc ((loc, idl, cpl, c0) pat) ->
+
+
let c' =
List.fold_left
(fun acc (n, t) ->
@@ -325,27 +440,74 @@ let rewrite_cases_aux (loc, po, tml, eqns) =
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
+ i
+*)
+(* 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 mkeq c n = RApp (dummy_loc, RRef (dummy_loc, (Lazy.force eqdep_ind_ref)), *)
+(* [mkHole; c; mkHole; 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 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'
+(* 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 list_mapi f =
let rec aux i = function
@@ -371,7 +533,7 @@ let rewrite_cases_aux (loc, po, tml, eqns) =
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)),
+ let mkeq c n = RApp (dummy_loc, RRef (dummy_loc, (Lazy.force eq_ind_ref)),
[mkHole; c; n])
in
let eqs_types =
@@ -419,10 +581,10 @@ let rec rewrite_cases c =
| _ -> 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'
+let rewrite_cases env c = 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
@@ -439,16 +601,107 @@ let recursive_message 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
+ debug 1 (str "Goal created");
let ts = Tacmach.mk_pftreestate goal in
+ debug 1 (str "Got pftreestate");
let solved_state = Tacmach.solve_pftreestate t ts in
- let c = Tacmach.extract_pftreestate solved_state in
+ debug 1 (str "Solved goal");
+ let _, l = Tacmach.extract_open_pftreestate solved_state in
+ List.iter (fun (_, x) -> debug 1 (str "left hole of type " ++ my_print_constr (Global.env()) x)) l;
+ let c = Tacmach.extract_pftreestate solved_state in
+ debug 1 (str "Extracted term");
debug 1 (str "Term constructed in solve by tac: " ++ my_print_constr (Global.env ()) c);
c
+ *)
+
+let solve_by_tac evi t =
+ debug 2 (str "Solving goal using tactics: " ++ Evd.pr_evar_info evi);
+ let id = id_of_string "H" in
+ try
+ Pfedit.start_proof id goal_kind evi.evar_hyps evi.evar_concl
+ (fun _ _ -> ());
+ debug 2 (str "Started proof");
+ Pfedit.by (tclCOMPLETE t);
+ let _,(const,_,_) = Pfedit.cook_proof () in
+ Pfedit.delete_current_proof (); const.Entries.const_entry_body
+ with e ->
+ Pfedit.delete_current_proof();
+ raise Exit
let rec string_of_list sep f = function
[] -> ""
| x :: [] -> f x
| x :: ((y :: _) as tl) -> f x ^ sep ^ string_of_list sep f tl
+
+let string_of_intset d =
+ string_of_list "," string_of_int (Intset.elements d)
+
+(**********************************************************)
+(* Pretty-printing *)
+open Printer
+open Ppconstr
+open Nameops
+open Termops
+open Evd
+
+let pr_meta_map evd =
+ let ml = meta_list evd in
+ let pr_name = function
+ Name id -> str"[" ++ pr_id id ++ str"]"
+ | _ -> mt() in
+ let pr_meta_binding = function
+ | (mv,Cltyp (na,b)) ->
+ hov 0
+ (pr_meta mv ++ pr_name na ++ str " : " ++
+ print_constr b.rebus ++ fnl ())
+ | (mv,Clval(na,b,_)) ->
+ hov 0
+ (pr_meta mv ++ pr_name na ++ str " := " ++
+ print_constr b.rebus ++ fnl ())
+ in
+ prlist pr_meta_binding ml
+
+let pr_idl idl = prlist_with_sep pr_spc pr_id idl
+
+let pr_evar_info evi =
+ let phyps =
+ (*pr_idl (List.rev (ids_of_named_context (evar_context evi))) *)
+ Printer.pr_named_context (Global.env()) (evar_context evi)
+ in
+ let pty = print_constr evi.evar_concl in
+ let pb =
+ match evi.evar_body with
+ | Evar_empty -> mt ()
+ | Evar_defined c -> spc() ++ str"=> " ++ print_constr c
+ in
+ hov 2 (str"[" ++ phyps ++ spc () ++ str"|- " ++ pty ++ pb ++ str"]")
+
+let pr_evar_map sigma =
+ h 0
+ (prlist_with_sep pr_fnl
+ (fun (ev,evi) ->
+ h 0 (str(string_of_existential ev)++str"=="++ pr_evar_info evi))
+ (to_list sigma))
+
+let pr_constraints pbs =
+ h 0
+ (prlist_with_sep pr_fnl (fun (pbty,t1,t2) ->
+ print_constr t1 ++ spc() ++
+ str (match pbty with
+ | Reduction.CONV -> "=="
+ | Reduction.CUMUL -> "<=") ++
+ spc() ++ print_constr t2) pbs)
+
+let pr_evar_defs evd =
+ let pp_evm =
+ let evars = evars_of evd in
+ if evars = empty then mt() else
+ str"EVARS:"++brk(0,1)++pr_evar_map evars++fnl() in
+ let pp_met =
+ if meta_list evd = [] then mt() else
+ str"METAS:"++brk(0,1)++pr_meta_map evd in
+ v 0 (pp_evm ++ pp_met)
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index ebfc5123..482640f9 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -12,6 +12,7 @@ open Evarutil
open Names
open Sign
+val ($) : ('a -> 'b) -> 'a -> 'b
val contrib_name : string
val subtac_dir : string list
val fix_sub_module : string
@@ -31,9 +32,19 @@ val proj1_sig_ref : reference
val proj2_sig_ref : reference
val build_sig : unit -> coq_sigma_data
val sig_ : coq_sigma_data lazy_t
-val eqind : constr lazy_t
-val eqind_ref : global_reference lazy_t
+
+val eq_ind : constr lazy_t
+val eq_rec : constr lazy_t
+val eq_rect : constr lazy_t
+val eq_refl : constr lazy_t
+val eq_ind_ref : global_reference lazy_t
val refl_equal_ref : global_reference lazy_t
+
+val eqdep_ind : constr lazy_t
+val eqdep_rec : constr lazy_t
+val eqdep_ind_ref : global_reference lazy_t
+val eqdep_intro_ref : global_reference lazy_t
+
val boolind : constr lazy_t
val sumboolind : constr lazy_t
val natind : constr lazy_t
@@ -48,10 +59,12 @@ val acc : constr lazy_t
val acc_inv : constr lazy_t
val extconstr : constr -> constr_expr
val extsort : sorts -> constr_expr
+
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_rel_context : env -> rel_context -> 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
@@ -98,3 +111,6 @@ 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
+val string_of_intset : Intset.t -> string
+
+val pr_evar_defs : evar_defs -> Pp.std_ppcmds
diff --git a/contrib/subtac/test/ListsTest.v b/contrib/subtac/test/ListsTest.v
index 8429c267..b8d13fe6 100644
--- a/contrib/subtac/test/ListsTest.v
+++ b/contrib/subtac/test/ListsTest.v
@@ -1,95 +1,76 @@
+(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
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.
+Set Implicit Arguments.
+Section Accessors.
+ Variable A : Set.
-Extraction myhd.
-Extraction Inline proj1_sig.
+ Program Definition myhd : forall { l : list A | length l <> 0 }, A :=
+ fun l =>
+ match l with
+ | nil => !
+ | hd :: tl => hd
+ end.
-Program Definition mytail : forall { l : list A | length l <> 0 }, list A :=
- fun l =>
+ Program Definition mytail (l : list A | length l <> 0) : list A :=
match l with
- | nil => _
- | hd :: tl => tl
+ | nil => !
+ | hd :: tl => tl
end.
-Proof.
-destruct l ; simpl ; intro H ; rewrite H in n ; intuition.
-Defined.
-
-Extraction mytail.
-
-Variable a : A.
+End Accessors.
-Program Definition test_hd : A := myhd (cons a nil).
-Proof.
-simpl ; auto.
-Defined.
-
-Extraction test_hd.
+Program Definition test_hd : nat := myhd (cons 1 nil).
+(*Eval compute in test_hd*)
(*Program Definition test_tail : list A := mytail nil.*)
+Section app.
+ Variable A : Set.
+ Program Fixpoint app (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 :: (tl ++ l')
+ end
+ where "x ++ y" := (app x y).
+
+ Next Obligation.
+ intros.
+ destruct_call app ; subtac_simpl.
+ Defined.
+
+ Program Lemma app_id_l : forall l : list A, l = nil ++ l.
+ Proof.
+ simpl ; auto.
+ Qed.
+
+ Program Lemma app_id_r : forall l : list A, l = l ++ nil.
+ Proof.
+ induction l ; simpl ; auto.
+ rewrite <- IHl ; auto.
+ Qed.
+
+End app.
+
+Extraction app.
+
+Section Nth.
+
+ Variable A : Set.
+
+ Program Fixpoint nth (l : list A) (n : nat | n < length l) { struct l } : A :=
+ match n, l with
+ | 0, hd :: _ => hd
+ | S n', _ :: tl => nth tl n'
+ | _, nil => !
+ end.
-
-
-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.
-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.
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+ Next Obligation.
+ Proof.
+ inversion l0.
+ Defined.
+End Nth.
diff --git a/contrib/subtac/test/euclid.v b/contrib/subtac/test/euclid.v
index ba5bdf23..a5a8b85f 100644
--- a/contrib/subtac/test/euclid.v
+++ b/contrib/subtac/test/euclid.v
@@ -1,66 +1,27 @@
-
-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 sig.
-Extract Inductive sig => "" [ "" ].
-Extraction testsig.
-
+Require Import Coq.subtac.Utils.
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} :
+Notation "( x & y )" := (existS _ x y) : core_scope.
+
+Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf lt a} :
{ 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.
+Require Import Omega.
+
+Obligations.
+Solve Obligations using subtac_simpl ; omega.
+
+Next Obligation.
+ assert(x0 * S q' = x0 * q' + x0) by auto with arith ; omega.
+Defined.
-apply minus_eq_add.
-omega.
-auto with arith.
-auto.
-simpl.
-induction b0 ; simpl.
-split ; auto.
-omega.
-exact (euclid a0 Acc_a0 b0).
+Program Definition test_euclid : (prod nat nat) := let (q, r) := euclid 4 2 in (q, q).
-exact (Acc_a).
-auto.
-auto.
-Focus 1.
+Eval lazy beta zeta delta iota in test_euclid.
+Program Definition testsig (a : nat) : { x : nat & { y : nat | x < y } } :=
+ (a & S a).
+Check testsig.
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-05 04:53:26 +0000