diff options
Diffstat (limited to 'contrib/subtac')
26 files changed, 1448 insertions, 1336 deletions
diff --git a/contrib/subtac/FixSub.v b/contrib/subtac/FixSub.v index 46121ff1..f047b729 100644 --- a/contrib/subtac/FixSub.v +++ b/contrib/subtac/FixSub.v @@ -1,6 +1,8 @@ Require Import Wf. Require Import Coq.subtac.Utils. +(** Reformulation of the Wellfounded module using subsets where possible. *) + Section Well_founded. Variable A : Type. Variable R : A -> A -> Prop. @@ -75,23 +77,70 @@ Require Import Wf_nat. Require Import Lt. Section Well_founded_measure. -Variable A : Type. -Variable f : A -> nat. -Definition R := fun x y => f x < f y. + Variable A : Type. + Variable m : A -> nat. + + Section Acc. + + Variable P : A -> Type. + + Variable F_sub : forall x:A, (forall y: { y : A | m y < m x }, P (proj1_sig y)) -> P x. + + Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (m x)) {struct r} : P x := + F_sub x (fun y: { y : A | m y < m x} => Fix_measure_F_sub (proj1_sig y) + (Acc_inv r (m (proj1_sig y)) (proj2_sig y))). + + Definition Fix_measure_sub (x : A) := Fix_measure_F_sub x (lt_wf (m x)). + + End Acc. -Section FixPoint. + Section FixPoint. + Variable P : A -> Type. + + Variable F_sub : forall x:A, (forall y: { y : A | m y < m x }, P (proj1_sig y)) -> P x. + + Notation Fix_F := (Fix_measure_F_sub P F_sub) (only parsing). (* alias *) + + Definition Fix_measure (x:A) := Fix_measure_F_sub P F_sub x (lt_wf (m x)). + + Hypothesis + F_ext : + forall (x:A) (f g:forall y:{y:A | m y < m x}, P (`y)), + (forall y:{ y:A | m y < m x}, f y = g y) -> F_sub x f = F_sub x g. -Variable P : A -> Type. + Lemma Fix_measure_F_eq : + forall (x:A) (r:Acc lt (m x)), + F_sub x (fun (y:{y:A|m y < m x}) => Fix_F (`y) (Acc_inv r (m (proj1_sig y)) (proj2_sig y))) = Fix_F x r. + Proof. + intros x. + set (y := m x). + unfold Fix_measure_F_sub. + intros r ; case r ; auto. + Qed. + + Lemma Fix_measure_F_inv : forall (x:A) (r s:Acc lt (m x)), Fix_F x r = Fix_F x s. + Proof. + intros x r s. + rewrite (proof_irrelevance (Acc lt (m x)) r s) ; auto. + Qed. -Variable F_sub : forall x:A, (forall y: { y : A | f y < f x }, P (proj1_sig y)) -> P x. - -Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (f x)) {struct r} : P x := - F_sub x (fun y: { y : A | f y < f x} => Fix_measure_F_sub (proj1_sig y) - (Acc_inv r (f (proj1_sig y)) (proj2_sig y))). + Lemma Fix_measure_eq : forall x:A, Fix_measure x = F_sub x (fun (y:{y:A| m y < m x}) => Fix_measure (proj1_sig y)). + Proof. + intro x; unfold Fix_measure in |- *. + rewrite <- (Fix_measure_F_eq ). + apply F_ext; intros. + apply Fix_measure_F_inv. + Qed. -Definition Fix_measure_sub (x : A) := Fix_measure_F_sub x (lt_wf (f x)). + Lemma fix_measure_sub_eq : + forall x : A, + Fix_measure_sub P F_sub x = + let f_sub := F_sub in + f_sub x (fun {y : A | m y < m x}=> Fix_measure (`y)). + exact Fix_measure_eq. + Qed. -End FixPoint. + End FixPoint. End Well_founded_measure. diff --git a/contrib/subtac/FunctionalExtensionality.v b/contrib/subtac/FunctionalExtensionality.v index 1a12ac82..4610f346 100644 --- a/contrib/subtac/FunctionalExtensionality.v +++ b/contrib/subtac/FunctionalExtensionality.v @@ -1,3 +1,11 @@ +Lemma equal_f : forall A B : Type, forall (f g : A -> B), + f = g -> forall x, f x = g x. +Proof. + intros. + rewrite H. + auto. +Qed. + Axiom fun_extensionality : forall A B (f g : A -> B), (forall x, f x = g x) -> f = g. @@ -23,3 +31,17 @@ Proof. apply (fun_extensionality_dep _ _ _ _ H). rewrite H0 ; auto. Qed. + +Lemma fix_sub_measure_eq_ext : + forall (A : Type) (f : A -> nat) (P : A -> Type) + (F_sub : forall x : A, (forall {y : A | f y < f x}, P (`y)) -> P x), + forall x : A, + Fix_measure_sub A f P F_sub x = + F_sub x (fun {y : A | f y < f x}=> Fix_measure_sub A f P F_sub (`y)). +Proof. + intros ; apply Fix_measure_eq ; auto. + intros. + assert(f0 = g). + apply (fun_extensionality_dep _ _ _ _ H). + rewrite H0 ; auto. +Qed. diff --git a/contrib/subtac/Heq.v b/contrib/subtac/Heq.v new file mode 100644 index 00000000..f2b216d9 --- /dev/null +++ b/contrib/subtac/Heq.v @@ -0,0 +1,34 @@ +Require Export JMeq. + +(** Notation for heterogenous equality. *) + +Notation " [ x : X ] = [ y : Y ] " := (@JMeq X x Y y) (at level 0, X at next level, Y at next level). + +(** Do something on an heterogeneous equality appearing in the context. *) + +Ltac on_JMeq tac := + match goal with + | [ H : @JMeq ?x ?X ?y ?Y |- _ ] => tac H + end. + +(** Try to apply [JMeq_eq] to get back a regular equality when the two types are equal. *) + +Ltac simpl_one_JMeq := + on_JMeq + ltac:(fun H => let H' := fresh "H" in + assert (H' := JMeq_eq H) ; clear H ; rename H' into H). + +(** Repeat it for every possible hypothesis. *) + +Ltac simpl_JMeq := repeat simpl_one_JMeq. + +(** Just simplify an h.eq. without clearing it. *) + +Ltac simpl_one_dep_JMeq := + on_JMeq + ltac:(fun H => let H' := fresh "H" in + assert (H' := JMeq_eq H)). + + + + diff --git a/contrib/subtac/SubtacTactics.v b/contrib/subtac/SubtacTactics.v new file mode 100644 index 00000000..a00234dd --- /dev/null +++ b/contrib/subtac/SubtacTactics.v @@ -0,0 +1,158 @@ +Ltac induction_with_subterm c H := + let x := fresh "x" in + let y := fresh "y" in + (remember c as x ; rewrite <- y in H ; induction H ; subst). + +Ltac induction_on_subterm c := + let x := fresh "x" in + let y := fresh "y" in + (set(x := c) ; assert(y:x = c) by reflexivity ; clearbody x ; induction x ; inversion y ; try subst ; + clear y). + +Ltac induction_with_subterms c c' H := + let x := fresh "x" in + let y := fresh "y" in + let z := fresh "z" in + let w := fresh "w" in + (set(x := c) ; assert(y:x = c) by reflexivity ; + set(z := c') ; assert(w:z = c') by reflexivity ; + rewrite <- y in H ; rewrite <- w in H ; + induction H ; subst). + + +Ltac destruct_one_pair := + match goal with + | [H : (_ /\ _) |- _] => destruct H + | [H : prod _ _ |- _] => destruct H + end. + +Ltac destruct_pairs := repeat (destruct_one_pair). + +Ltac destruct_one_ex := + let tac H := let ph := fresh "H" in destruct H as [H ph] in + match goal with + | [H : (ex _) |- _] => tac H + | [H : (sig ?P) |- _ ] => tac H + | [H : (ex2 _) |- _] => tac H + end. + +Ltac destruct_exists := repeat (destruct_one_ex). + +Tactic Notation "destruct" "exist" ident(t) ident(Ht) := destruct t as [t Ht]. + +Tactic Notation "destruct" "or" ident(H) := destruct H as [H|H]. + +Tactic Notation "contradiction" "by" constr(t) := + let H := fresh in assert t as H by auto with * ; contradiction. + +Ltac discriminates := + match goal with + | [ H : ?x <> ?x |- _ ] => elim H ; reflexivity + | _ => discriminate + end. + +Ltac destruct_conjs := repeat (destruct_one_pair || destruct_one_ex). + +Ltac on_last_hyp tac := + match goal with + [ H : _ |- _ ] => tac H + end. + +Tactic Notation "on_last_hyp" tactic(t) := on_last_hyp t. + +Ltac revert_last := + match goal with + [ H : _ |- _ ] => revert H + end. + +Ltac reverse := repeat revert_last. + +Ltac on_call f tac := + match goal with + | H : ?T |- _ => + match T with + | context [f ?x ?y ?z ?w ?v ?u] => tac (f x y z w v u) + | context [f ?x ?y ?z ?w ?v] => tac (f x y z w v) + | context [f ?x ?y ?z ?w] => tac (f x y z w) + | context [f ?x ?y ?z] => tac (f x y z) + | context [f ?x ?y] => tac (f x y) + | context [f ?x] => tac (f x) + end + | |- ?T => + match T with + | context [f ?x ?y ?z ?w ?v ?u] => tac (f x y z w v u) + | context [f ?x ?y ?z ?w ?v] => tac (f x y z w v) + | context [f ?x ?y ?z ?w] => tac (f x y z w) + | context [f ?x ?y ?z] => tac (f x y z) + | context [f ?x ?y] => tac (f x y) + | context [f ?x] => tac (f x) + end + end. + +(* Destructs calls to f in hypothesis or conclusion, useful if f creates a subset object *) +Ltac destruct_call f := + let tac t := destruct t in on_call f tac. + +Ltac destruct_call_as f l := + let tac t := destruct t as l in on_call f tac. + +Tactic Notation "destruct_call" constr(f) := destruct_call f. +Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) := destruct_call_as f l. + +Ltac myinjection := + let tac H := inversion H ; subst ; clear H in + match goal with + | [ H : ?f ?a = ?f' ?a' |- _ ] => tac H + | [ H : ?f ?a ?b = ?f' ?a' ?b' |- _ ] => tac H + | [ H : ?f ?a ?b ?c = ?f' ?a' ?b' ?c' |- _ ] => tac H + | [ H : ?f ?a ?b ?c ?d= ?f' ?a' ?b' ?c' ?d' |- _ ] => tac H + | [ H : ?f ?a ?b ?c ?d ?e= ?f' ?a' ?b' ?c' ?d' ?e' |- _ ] => tac H + | [ H : ?f ?a ?b ?c ?d ?e ?g= ?f' ?a' ?b' ?c' ?d' ?e' ?g' |- _ ] => tac H + | [ H : ?f ?a ?b ?c ?d ?e ?g ?h= ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' |- _ ] => tac H + | [ H : ?f ?a ?b ?c ?d ?e ?g ?h ?i = ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' ?i' |- _ ] => tac H + | [ H : ?f ?a ?b ?c ?d ?e ?g ?h ?i ?j = ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' ?i' ?j' |- _ ] => tac H + | _ => idtac + end. + +Ltac destruct_nondep H := let H0 := fresh "H" in assert(H0 := H); destruct H0. + +Ltac bang := + match goal with + | |- ?x => + match x with + | context [False_rect _ ?p] => elim p + end + end. + +Require Import Eqdep. + +Ltac elim_eq_rect := + match goal with + | [ |- ?t ] => + match t with + | context [ @eq_rect _ _ _ _ _ ?p ] => + let P := fresh "P" in + set (P := p); simpl in P ; + try ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P)) + | context [ @eq_rect _ _ _ _ _ ?p _ ] => + let P := fresh "P" in + set (P := p); simpl in P ; + try ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P)) + end + end. + +Ltac real_elim_eq_rect := + match goal with + | [ |- ?t ] => + match t with + | context [ @eq_rect _ _ _ _ _ ?p ] => + let P := fresh "P" in + set (P := p); simpl in P ; + ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P)) + | context [ @eq_rect _ _ _ _ _ ?p _ ] => + let P := fresh "P" in + set (P := p); simpl in P ; + ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P)) + end + end. +
\ No newline at end of file diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v index 4a2208ce..76f49dd3 100644 --- a/contrib/subtac/Utils.v +++ b/contrib/subtac/Utils.v @@ -1,75 +1,65 @@ +Require Export Coq.subtac.SubtacTactics. + Set Implicit Arguments. -Notation "'fun' { x : A | P } => Q" := - (fun x:{x:A|P} => Q) - (at level 200, x ident, right associativity). +(** Wrap a proposition inside a subset. *) -Notation "( x & ? )" := (@exist _ _ x _) : core_scope. +Notation " {{ x }} " := (tt : { y : unit | x }). + +(** A simpler notation for subsets defined on a cartesian product. *) + +Notation "{ ( x , y ) : A | P }" := + (sig (fun anonymous : A => let (x,y) := anonymous in P)) + (x ident, y ident) : type_scope. + +(** Generates an obligation to prove False. *) Notation " ! " := (False_rect _ _). -Definition ex_pi1 (A : Prop) (P : A -> Prop) (t : ex P) : A. -intros. -induction t. -exact x. -Defined. +(** Abbreviation for first projection and hiding of proofs of subset objects. *) + +Notation " ` t " := (proj1_sig t) (at level 10) : core_scope. +Notation "( x & ? )" := (@exist _ _ x _) : core_scope. + +(** Coerces objects to their support before comparing them. *) -Lemma ex_pi2 : forall (A : Prop) (P : A -> Prop) (t : ex P), - P (ex_pi1 t). -intros A P. -dependent inversion t. -simpl. -exact p. -Defined. +Notation " x '`=' y " := ((x :>) = (y :>)) (at level 70). +(** Quantifying over subsets. *) + +Notation "'fun' { x : A | P } => Q" := + (fun x:{x:A|P} => Q) + (at level 200, x ident, right associativity). -Notation "` t" := (proj1_sig t) (at level 100) : core_scope. Notation "'forall' { x : A | P } , Q" := (forall x:{x:A|P}, Q) (at level 200, x ident, right associativity). -Lemma subset_simpl : forall (A : Set) (P : A -> Prop) - (t : sig P), P (` t). -Proof. -intros. -induction t. - simpl ; auto. -Qed. - -Ltac destruct_one_pair := - match goal with - | [H : (ex _) |- _] => destruct H - | [H : (ex2 _) |- _] => destruct H - | [H : (sig _) |- _] => destruct H - | [H : (_ /\ _) |- _] => destruct H -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. +Require Import Coq.Bool.Sumbool. + +(** Construct a dependent disjunction from a boolean. *) + +Notation "'dec'" := (sumbool_of_bool) (at level 0). +(** The notations [in_right] and [in_left] construct objects of a dependent disjunction. *) + +Notation in_right := (@right _ _ _). +Notation in_left := (@left _ _ _). + +(** Default simplification tactic. *) + +Ltac subtac_simpl := simpl ; intros ; destruct_conjs ; simpl in * ; try subst ; + try (solve [ red ; intros ; discriminate ]) ; auto with *. + +(** Extraction directives *) 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" [ "" ]. +(* Extract Inductive prod "'a" "'b" => " 'a * 'b " [ "(,)" ]. *) +(* Extract Inductive sigT => "prod" [ "" ]. *) Require Export ProofIrrelevance. +Require Export Coq.subtac.Heq. + +Delimit Scope program_scope with program. diff --git a/contrib/subtac/context.ml b/contrib/subtac/context.ml deleted file mode 100644 index 236b0ea5..00000000 --- a/contrib/subtac/context.ml +++ /dev/null @@ -1,35 +0,0 @@ -open Term -open Names - -type t = rel_declaration list (* name, optional coq interp, algorithmic type *) - -let assoc n t = - let _, term, typ = List.find (fun (x, _, _) -> x = n) t in - term, typ - -let assoc_and_index x l = - let rec aux i = function - (y, term, typ) :: tl -> if x = y then i, term, typ else aux (succ i) tl - | [] -> raise Not_found - in aux 0 l - -let id_of_name = function - Name id -> id - | Anonymous -> raise (Invalid_argument "id_of_name") -(* - -let subst_ctx ctx c = - let rec aux ((ctx, n, c) as acc) = function - (name, None, typ) :: tl -> - aux (((id_of_name name, None, rel_to_vars ctx typ) :: ctx), - pred n, c) tl - | (name, Some term, typ) :: tl -> - let t' = Term.substnl [term] n c in - aux (ctx, n, t') tl - | [] -> acc - in - let (x, _, z) = aux ([], pred (List.length ctx), c) (List.rev ctx) in - (x, rel_to_vars x z) -*) - -let subst_env env c = (env, c) diff --git a/contrib/subtac/context.mli b/contrib/subtac/context.mli deleted file mode 100644 index 671d6f36..00000000 --- a/contrib/subtac/context.mli +++ /dev/null @@ -1,5 +0,0 @@ -type t = Term.rel_declaration list -val assoc : 'a -> ('a * 'b * 'c) list -> 'b * 'c -val assoc_and_index : 'a -> ('a * 'b * 'c) list -> int * 'b * 'c -val id_of_name : Names.name -> Names.identifier -val subst_env : 'a -> 'b -> 'a * 'b diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml index 1844fea5..2a84fdd0 100644 --- a/contrib/subtac/eterm.ml +++ b/contrib/subtac/eterm.ml @@ -11,52 +11,33 @@ open Evd open List open Pp open Util +open Subtac_utils -let reverse_array arr = - Array.of_list (List.rev (Array.to_list arr)) - let trace s = if !Options.debug then (msgnl s; msgerr s) else () -(** Utilities to find indices in lists *) -let list_index x l = - let rec aux i = function - k :: tl -> if k = x then i else aux (succ i) tl - | [] -> raise Not_found - in aux 0 l - -let list_assoc_index x l = - let rec aux i = function - (k, _, v) :: tl -> if k = x then i else aux (succ i) tl - | [] -> raise Not_found - in aux 0 l - - (** Substitute evar references in t using De Bruijn indices, where n binders were passed through. *) let subst_evar_constr evs n t = let seen = ref Intset.empty in - let evar_info id = - let rec aux i = function - (k, x) :: tl -> - if k = id then x else aux (succ i) tl - | [] -> raise Not_found - in aux 0 evs - in + let evar_info id = List.assoc id evs in let rec substrec depth c = match kind_of_term c with | Evar (k, args) -> - let (id, idstr), hyps, _, _ = + let (id, idstr), hyps, chop, _, _ = try evar_info k with Not_found -> anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found") in seen := Intset.add id !seen; -(* (try trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++ *) -(* int (List.length hyps) ++ str " hypotheses"); with _ -> () ); *) (* Evar arguments are created in inverse order, and we must not apply to defined ones (i.e. LetIn's) *) + let args = + let n = match chop with None -> 0 | Some c -> c in + let (l, r) = list_chop n (List.rev (Array.to_list args)) in + List.rev r + in let args = let rec aux hyps args acc = match hyps, args with @@ -66,9 +47,13 @@ let subst_evar_constr evs n t = aux tlh tla acc | [], [] -> acc | _, _ -> acc (*failwith "subst_evars: invalid argument"*) - in aux hyps (Array.to_list args) [] - in - mkApp (mkVar idstr, Array.of_list args) + in aux hyps args [] + in + (try trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (List.length args) ++ str "arguments," ++ + int (List.length hyps) ++ str " hypotheses" ++ spc () ++ + pp_list (fun x -> my_print_constr (Global.env ()) x) args); + with _ -> ()); + mkApp (mkVar idstr, Array.of_list args) | _ -> map_constr_with_binders succ substrec depth c in let t' = substrec 0 t in @@ -78,10 +63,7 @@ let subst_evar_constr evs n t = (** Substitute variable references in t using De Bruijn indices, where n binders were passed through. *) let subst_vars acc n t = - let var_index id = - let idx = list_index id acc in - idx + 1 - in + let var_index id = Util.list_index id acc in let rec substrec depth c = match kind_of_term c with | Var v -> (try mkRel (depth + (var_index v)) with Not_found -> c) | _ -> map_constr_with_binders succ substrec depth c @@ -89,47 +71,58 @@ let subst_vars acc n t = substrec 0 t (** Rewrite type of an evar ([ H1 : t1, ... Hn : tn |- concl ]) - to a product : forall H1 : t1, ..., forall Hn : tn, concl. + to a product : forall H1 : t1, ..., forall Hn : tn, concl. Changes evars and hypothesis references to variable references. + A little optimization: don't include unnecessary let-ins and their dependencies. *) -let etype_of_evar evs ev hyps = +let etype_of_evar evs hyps concl = let rec aux acc n = function (id, copt, t) :: tl -> let t', s = subst_evar_constr evs n t in let t'' = subst_vars acc 0 t' in - let copt', s = - match copt with + let rest, s' = aux (id :: acc) (succ n) tl in + let s' = Intset.union s s' in + (match copt with Some c -> - let c', s' = subst_evar_constr evs n c in - Some c', Intset.union s s' - | None -> None, s - in - let copt' = option_map (subst_vars acc 0) copt' in - let rest, s' = aux (id :: acc) (succ n) tl in - mkNamedProd_or_LetIn (id, copt', t'') rest, Intset.union s' s + if noccurn 1 rest then lift (-1) rest, s' + else + let c', s'' = subst_evar_constr evs n c in + let c' = subst_vars acc 0 c' in + mkNamedProd_or_LetIn (id, Some c', t'') rest, Intset.union s'' s' + | None -> + mkNamedProd_or_LetIn (id, None, t'') rest, s') | [] -> - let t', s = subst_evar_constr evs n ev.evar_concl in + let t', s = subst_evar_constr evs n concl in subst_vars acc 0 t', s in aux [] 0 (rev hyps) open Tacticals -let rec take n l = - if n = 0 then [] else List.hd l :: take (pred n) (List.tl l) - let trunc_named_context n ctx = let len = List.length ctx in - take (len - n) ctx + list_firstn (len - n) ctx -let eterm_obligations name nclen evm t tycon = +let rec chop_product n t = + if n = 0 then Some t + else + match kind_of_term t with + | Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None + | _ -> None + +let eterm_obligations name nclen isevars evm fs t tycon = (* 'Serialize' the evars, we assume that the types of the existentials refer to previous existentials in the list only *) + trace (str " In eterm: isevars: " ++ my_print_evardefs isevars); + trace (str "Term given to eterm" ++ spc () ++ + Termops.print_constr_env (Global.env ()) t); let evl = List.rev (to_list evm) in let evn = let i = ref (-1) in List.rev_map (fun (id, ev) -> incr i; - (id, (!i, id_of_string (string_of_id name ^ "_obligation_" ^ string_of_int (succ !i))), ev)) evl + (id, (!i, id_of_string + (string_of_id name ^ "_obligation_" ^ string_of_int (succ !i))), + ev)) evl in let evts = (* Remove existential variables in types and build the corresponding products *) @@ -137,8 +130,22 @@ let eterm_obligations name nclen evm t tycon = (fun (id, (n, nstr), ev) l -> let hyps = Environ.named_context_of_val ev.evar_hyps in let hyps = trunc_named_context nclen hyps in - let evtyp, deps = etype_of_evar l ev hyps in - let y' = (id, ((n, nstr), hyps, evtyp, deps)) in + let evtyp, deps = etype_of_evar l hyps ev.evar_concl in + let evtyp, hyps, chop = + match chop_product fs evtyp with + Some t -> + (try + trace (str "Choped a product: " ++ spc () ++ + Termops.print_constr_env (Global.env ()) evtyp ++ str " to " ++ spc () ++ + Termops.print_constr_env (Global.env ()) t); + with _ -> ()); + t, trunc_named_context fs hyps, fs + | None -> evtyp, hyps, 0 + in + let loc, k = evar_source id isevars in + let opacity = match k with QuestionMark o -> o | _ -> true in + let opaque = if not opacity || chop <> fs then None else Some chop in + let y' = (id, ((n, nstr), hyps, opaque, evtyp, deps)) in y' :: l) evn [] in @@ -146,26 +153,20 @@ let eterm_obligations name nclen evm t tycon = subst_evar_constr evts 0 t in let evars = - List.map (fun (_, ((_, name), _, typ, deps)) -> name, typ, deps) evts + List.map (fun (_, ((_, name), _, opaque, typ, deps)) -> name, typ, not (opaque = None), 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 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 = - let rec aux i acc = - if i > 0 then aux (pred i) (Evarutil.mk_new_meta () :: acc) - else acc - in aux n [] +let mkMetas n = list_tabulate (fun _ -> Evarutil.mk_new_meta ()) n (* let eterm evm t (tycon : types option) = *) (* let t, tycon, evs = eterm_term evm t tycon in *) diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli index 3a571ee1..76994c06 100644 --- a/contrib/subtac/eterm.mli +++ b/contrib/subtac/eterm.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: eterm.mli 9326 2006-10-31 12:57:26Z msozeau $ i*) +(*i $Id: eterm.mli 9976 2007-07-12 11:58:30Z msozeau $ i*) open Tacmach open Term @@ -18,7 +18,10 @@ val mkMetas : int -> constr list (* val eterm_term : evar_map -> constr -> types option -> constr * types option * (identifier * types) list *) -val eterm_obligations : identifier -> int -> evar_map -> constr -> types option -> - (identifier * types * Intset.t) array * constr (* Obl. name, type as product and dependencies as indexes into the array *) +(* id, named context length, evars, number of + function prototypes to try to clear from evars contexts, object and optional type *) +val eterm_obligations : identifier -> int -> evar_defs -> evar_map -> int -> constr -> types option -> + (identifier * types * bool * Intset.t) array * constr + (* Obl. name, type as product, opacity (true = opaque) and dependencies as indexes into the array *) val etermtac : open_constr -> tactic diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4 index e31326e9..43a3bec4 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 9588 2007-02-02 16:17:13Z herbelin $ *) +(* $Id: g_subtac.ml4 9976 2007-07-12 11:58:30Z msozeau $ *) (*i camlp4deps: "parsing/grammar.cma" i*) @@ -104,15 +104,36 @@ VERNAC COMMAND EXTEND Subtac_Obligations | [ "Next" "Obligation" ] -> [ Subtac_obligations.next_obligation None ] END +VERNAC COMMAND EXTEND Subtac_Solve_Obligation +| [ "Solve" "Obligation" integer(num) "of" ident(name) "using" tactic(t) ] -> + [ Subtac_obligations.try_solve_obligation num (Some name) (Tacinterp.interp t) ] +| [ "Solve" "Obligation" integer(num) "using" tactic(t) ] -> + [ Subtac_obligations.try_solve_obligation num None (Tacinterp.interp t) ] + 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) ] +| [ "Solve" "Obligations" "of" ident(name) "using" tactic(t) ] -> + [ Subtac_obligations.try_solve_obligations (Some name) (Tacinterp.interp t) ] +| [ "Solve" "Obligations" "using" tactic(t) ] -> + [ Subtac_obligations.try_solve_obligations None (Tacinterp.interp t) ] +| [ "Solve" "Obligations" ] -> + [ Subtac_obligations.try_solve_obligations None (Subtac_obligations.default_tactic ()) ] + END + +VERNAC COMMAND EXTEND Subtac_Solve_All_Obligations +| [ "Solve" "All" "Obligations" "using" tactic(t) ] -> + [ Subtac_obligations.solve_all_obligations (Tacinterp.interp t) ] +| [ "Solve" "All" "Obligations" ] -> + [ Subtac_obligations.solve_all_obligations (Subtac_obligations.default_tactic ()) ] + END + +VERNAC COMMAND EXTEND Subtac_Admit_Obligations | [ "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) ] +| [ "Obligations" "Tactic" ":=" tactic(t) ] -> [ Subtac_obligations.set_default_tactic (Tacinterp.glob_tactic t) ] END VERNAC COMMAND EXTEND Subtac_Show_Obligations diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml index 5e46bead..8bc310d5 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 9563 2007-01-31 09:37:18Z msozeau $ *) +(* $Id: subtac.ml 9976 2007-07-12 11:58:30Z msozeau $ *) open Global open Pp @@ -37,85 +37,11 @@ open Subtac_utils open Coqlib open Printer open Subtac_errors -open Context open Eterm let require_library dirpath = let qualid = (dummy_loc, qualid_of_dirpath (dirpath_of_string dirpath)) in Library.require_library [qualid] None -(* -let subtac_one_fixpoint env isevars (f, decl) = - let ((id, n, bl, typ, body), decl) = - Subtac_interp_fixpoint.rewrite_fixpoint env [] (f, decl) - in - let _ = - try trace (str "Working on a single fixpoint rewritten as: " ++ spc () ++ - Ppconstr.pr_constr_expr body) - with _ -> () - in ((id, n, bl, typ, body), decl) -*) - -let subtac_fixpoint isevars l = - (* TODO: Copy command.build_recursive *) - () -(* -let save id const (locality,kind) hook = - let {const_entry_body = pft; - const_entry_type = tpo; - const_entry_opaque = opacity } = const in - let l,r = match locality with - | Local when Lib.sections_are_opened () -> - let k = logical_kind_of_goal_kind kind in - let c = SectionLocalDef (pft, tpo, opacity) in - let _ = declare_variable id (Lib.cwd(), c, k) in - (Local, VarRef id) - | Local -> - let k = logical_kind_of_goal_kind kind in - let kn = declare_constant id (DefinitionEntry const, k) in - (Global, ConstRef kn) - | Global -> - let k = logical_kind_of_goal_kind kind in - let kn = declare_constant id (DefinitionEntry const, k) in - (Global, ConstRef kn) in - Pfedit.delete_current_proof (); - hook l r; - definition_message id - -let save_named opacity = - let id,(const,persistence,hook) = Pfedit.cook_proof () in - let const = { const with const_entry_opaque = opacity } in - save id const persistence hook - -let check_anonymity id save_ident = - if atompart_of_id id <> "Unnamed_thm" then - error "This command can only be used for unnamed theorem" -(* - message("Overriding name "^(string_of_id id)^" and using "^save_ident) -*) - -let save_anonymous opacity save_ident = - let id,(const,persistence,hook) = Pfedit.cook_proof () in - let const = { const with const_entry_opaque = opacity } in - check_anonymity id save_ident; - save save_ident const persistence hook - -let save_anonymous_with_strength kind opacity save_ident = - let id,(const,_,hook) = Pfedit.cook_proof () in - let const = { const with const_entry_opaque = opacity } in - check_anonymity id save_ident; - (* we consider that non opaque behaves as local for discharge *) - save save_ident const (Global, Proof kind) hook - -let subtac_end_proof = function - | Admitted -> admit () - | Proved (is_opaque,idopt) -> - if_verbose show_script (); - match idopt with - | None -> save_named is_opaque - | Some ((_,id),None) -> save_anonymous is_opaque id - | Some ((_,id),Some kind) -> save_anonymous_with_strength kind is_opaque id - - *) open Pp open Ppconstr @@ -142,48 +68,45 @@ 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 _ = Detyping.set_detype_anonymous (fun loc n -> RVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n))) + +let assumption_message id = + Options.if_verbose message ((string_of_id id) ^ " is assumed") -let _ = Subtac_obligations.set_default_tactic - (Tacinterp.eval_tactic (utils_call "subtac_simpl" [])) +let declare_assumption env isevars idl is_coe k bl c = + if not (Pfedit.refining ()) then + let evm, c, typ = + Subtac_pretyping.subtac_process env isevars (snd (List.hd idl)) [] (Command.generalize_constr_expr c bl) None + in + List.iter (Command.declare_one_assumption is_coe k c) idl + else + errorlabstrm "Command.Assumption" + (str "Cannot declare an assumption while in proof editing mode.") + +let vernac_assumption env isevars kind l = + List.iter (fun (is_coe,(idl,c)) -> declare_assumption env isevars idl is_coe kind [] c) l let subtac (loc, command) = check_required_library ["Coq";"Init";"Datatypes"]; check_required_library ["Coq";"Init";"Specif"]; - (* check_required_library ["Coq";"Logic";"JMeq"]; *) +(* check_required_library ["Coq";"Logic";"JMeq"]; *) require_library "Coq.subtac.FixSub"; require_library "Coq.subtac.Utils"; + require_library "Coq.Logic.JMeq"; let env = Global.env () in let isevars = ref (create_evar_defs Evd.empty) in try - match command with + match command with VernacDefinition (defkind, (locid, id), expr, hook) -> (match expr with ProveBody (bl, c) -> Subtac_pretyping.subtac_proof env isevars id bl c None -(* let evm, c, ctyp = in *) -(* trace (str "Starting proof"); *) -(* Command.start_proof id goal_kind c hook; *) -(* trace (str "Started proof"); *) - | DefineBody (bl, _, c, tycon) -> - Subtac_pretyping.subtac_proof env isevars id bl c tycon - (* let tac = Eterm.etermtac (evm, c) in *) - (* trace (str "Starting proof"); *) - (* Command.start_proof id goal_kind ctyp hook; *) - (* trace (str "Started proof"); *) - (* Pfedit.by tac) *)) + Subtac_pretyping.subtac_proof env isevars id bl c tycon) | VernacFixpoint (l, b) -> let _ = trace (str "Building fixpoint") in ignore(Subtac_command.build_recursive l b) @@ -199,6 +122,8 @@ let subtac (loc, command) = start_proof_and_print env isevars (Some id) (Global, Proof thkind) (bl,t) hook + | VernacAssumption (stre,l) -> + vernac_assumption env isevars stre l (*| VernacEndProof e -> subtac_end_proof e*) @@ -237,6 +162,10 @@ let subtac (loc, command) = str "Uncoercible terms:" ++ spc () ++ x ++ spc () ++ str "and" ++ spc () ++ y in msg_warning cmds + + | Cases.PatternMatchingError (env, exn) as e -> + debug 2 (Himsg.explain_pattern_matching_error env exn); + raise e | Type_errors.TypeError (env, exn) as e -> debug 2 (Himsg.explain_type_error env exn); diff --git a/contrib/subtac/subtac.mli b/contrib/subtac/subtac.mli index 25922782..b51150aa 100644 --- a/contrib/subtac/subtac.mli +++ b/contrib/subtac/subtac.mli @@ -1,3 +1,2 @@ val require_library : string -> unit -val subtac_fixpoint : 'a -> 'b -> unit val subtac : Util.loc * Vernacexpr.vernac_expr -> unit diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml index fbe1ac37..04cad7c0 100644 --- a/contrib/subtac/subtac_cases.ml +++ b/contrib/subtac/subtac_cases.ml @@ -8,6 +8,7 @@ (* $Id: cases.ml 9399 2006-11-22 16:11:53Z herbelin $ *) +open Cases open Util open Names open Nameops @@ -29,52 +30,6 @@ 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) *) (************************************************************************) @@ -1500,7 +1455,7 @@ let set_arity_signature dep n arsign tomatchl pred x = in decomp_block [] pred (tomatchl,arsign) -let prepare_predicate_from_tycon loc dep env isevars tomatchs sign c = +let oldprepare_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 @@ -1587,6 +1542,39 @@ let extract_arity_signature env0 tomatchl tmsign = | _ -> assert false in List.rev (buildrec 0 (tomatchl,tmsign)) +let extract_arity_signatures env0 tomatchl tmsign = + let get_one_sign tm (na,t) = + match tm with + | NotInd (bo,typ) -> + (match t with + | None -> [na,bo,typ] + | Some (loc,_,_,_) -> + user_err_loc (loc,"", + str "Unexpected type annotation for a term of non inductive type")) + | IsInd (_,IndType(indf,realargs)) -> + 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) + ::(try List.map2 (fun x (_,c,t) ->(x,c,t)) realnal arsign with _ -> assert false) in + let rec buildrec = function + | [],[] -> [] + | (_,tm)::ltm, x::tmsign -> + let l = get_one_sign tm x in + l :: buildrec (ltm,tmsign) + | _ -> assert false + in List.rev (buildrec (tomatchl,tmsign)) + let inh_conv_coerce_to_tycon loc env isevars j tycon = match tycon with | Some p -> @@ -1596,44 +1584,80 @@ let inh_conv_coerce_to_tycon loc env isevars j tycon = | 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 = + +let string_of_name name = + match name with + | Anonymous -> "anonymous" + | Name n -> string_of_id n + +let id_of_name n = id_of_string (string_of_name n) + +let make_prime_id name = + let str = string_of_name name in + id_of_string str, id_of_string (str ^ "'") + +let prime avoid name = + let previd, id = make_prime_id name in + previd, next_ident_away_from id avoid + +let make_prime avoid prevname = + let previd, id = prime !avoid prevname in + avoid := id :: !avoid; + previd, id + +let eq_id avoid id = + let hid = id_of_string ("Heq_" ^ string_of_id id) in + let hid' = next_ident_away_from hid avoid in + hid' + +let mk_eq typ x y = mkApp (Lazy.force eq_ind, [| typ; x ; y |]) +let mk_eq_refl typ x = mkApp (Lazy.force eq_refl, [| typ; x |]) +let mk_JMeq typ x typ' y = mkApp (Lazy.force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |]) +let mk_JMeq_refl typ x = mkApp (Lazy.force Subtac_utils.jmeq_refl, [| typ; x |]) + +let hole = RHole (dummy_loc, Evd.QuestionMark true) + +let context_of_arsign l = + let (x, _) = List.fold_right + (fun c (x, n) -> + (lift_rel_context n c @ x, List.length c + n)) + l ([], 0) + in x + +let constr_of_pat env isevars arsign pat avoid = + let rec typ env (ty, realargs) pat avoid = 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 + trace (str "Treating pattern variable " ++ str (string_of_id (id_of_name name))); + let name, avoid = match name with + Name n -> name, avoid | Anonymous -> - let n' = next_ident_away_from (id_of_string "wildcard") idents in - Name n', n' :: idents + let previd, id = prime avoid (Name (id_of_string "wildcard")) in + Name id, id :: avoid in -(* trace (str "Treating pattern variable " ++ str (string_of_id (id_of_name name))); *) - PatVar (l, name), [name, None, ty], mkRel 1, 1, idents' + trace (str "Treated pattern variable " ++ str (string_of_id (id_of_name name))); + PatVar (l, name), [name, None, ty] @ realargs, mkRel 1, ty, (List.map (fun x -> mkRel 1) realargs), 1, avoid | 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 cind = inductive_of_constructor cstr in + let IndType (indf, _) = find_rectype env (Evd.evars_of !isevars) (lift (-(List.length realargs)) ty) in let ind, params = dest_ind_family indf in + if ind <> cind then error_bad_constructor_loc l cstr ind; 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' = + let patargs, args, sign, env, n, m, avoid = 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 + (fun (na, c, t) ua (patargs, args, sign, env, n, m, avoid) -> + let pat', sign', arg', typ', argtypargs, n', avoid = + typ env (lift (n - m) t, []) ua avoid + 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') + (pat' :: patargs, args', sign' @ sign, env', n' + n, succ m, avoid)) + ci.cs_args (List.rev args) ([], [], [], env, 0, 0, avoid) in let args = List.rev args in let patargs = List.rev patargs in @@ -1641,120 +1665,244 @@ let constr_of_pat env isevars ty pat idents = 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' + trace (str "Getting type of app: " ++ my_print_constr env app); + let apptype = Retyping.get_type_of env (Evd.evars_of !isevars) app in + trace (str "Family and args of apptype: " ++ my_print_constr env apptype); + let IndType (indf, realargs) = find_rectype env (Evd.evars_of !isevars) apptype in + trace (str "Got Family and args of apptype: " ++ my_print_constr env apptype); + match alias with + Anonymous -> + pat', sign, app, apptype, realargs, n, avoid + | Name id -> + let sign = (alias, None, lift m ty) :: sign in + let avoid = id :: avoid in + let sign, i, avoid = + try + let env = push_rels sign env in + isevars := the_conv_x_leq (push_rels sign env) (lift (succ m) ty) (lift 1 apptype) !isevars; + trace (str "convertible types for alias : " ++ my_print_constr env (lift (succ m) ty) + ++ my_print_constr env (lift 1 apptype)); + let eq_t = mk_eq (lift (succ m) ty) + (mkRel 1) (* alias *) + (lift 1 app) (* aliased term *) + in + let neq = eq_id avoid id in + (Name neq, Some (mkRel 0), eq_t) :: sign, 2, neq :: avoid + with Reduction.NotConvertible -> sign, 1, avoid + in + (* Mark the equality as a hole *) + pat', sign, lift i app, lift i apptype, realargs, n + i, avoid 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 tycon, arity = mk_tycon_from_sign env isevars arsign arity in *) + let pat', sign, patc, patty, args, z, avoid = typ env (pi3 (List.hd arsign), List.tl arsign) pat avoid in + let c = it_mkProd_or_LetIn patc sign in + trace (str "arity signature is : " ++ my_print_rel_context env arsign); + trace (str "signature is : " ++ my_print_rel_context env sign); + trace (str "patty, args are : " ++ my_print_constr env (applistc patty args)); + trace (str "Constr_of_pat gives: " ++ my_print_constr env c); + trace (str "with args: " ++ pp_list (my_print_constr (push_rels sign env)) args); + pat', (sign, patc, (pi3 (List.hd arsign), args), pat'), avoid + + +(* shadows functional version *) +let eq_id avoid id = + let hid = id_of_string ("Heq_" ^ string_of_id id) in + let hid' = next_ident_away_from hid !avoid in + avoid := hid' :: !avoid; + hid' + +let rels_of_patsign = + List.map (fun ((na, b, t) as x) -> + match b with + | Some t' when kind_of_term t' = Rel 0 -> (na, None, t) + | _ -> x) + +let vars_of_ctx ctx = + let _, y = + List.fold_right (fun (na, b, t) (prev, vars) -> + match b with + | Some t' when kind_of_term t' = Rel 0 -> + prev, + (RApp (dummy_loc, + (RRef (dummy_loc, Lazy.force refl_ref)), [hole; RVar (dummy_loc, prev)])) :: vars + | _ -> + match na with + Anonymous -> raise (Invalid_argument "vars_of_ctx") + | Name n -> n, RVar (dummy_loc, n) :: vars) + ctx (id_of_string "vars_of_ctx: error", []) + in List.rev y + +let rec is_included x y = + match x, y with + | PatVar _, _ -> true + | _, PatVar _ -> true + | PatCstr (l, (_, i), args, alias), PatCstr (l', (_, i'), args', alias') -> + if i = i' then List.for_all2 is_included args args' + else false + +(* liftsign is the current pattern's signature length *) +let build_ineqs prevpatterns pats liftsign = + let _tomatchs = List.length pats in + let diffs = + List.fold_left + (fun c eqnpats -> + let acc = List.fold_left2 + (fun acc (ppat_sign, ppat_c, (ppat_ty, ppat_tyargs), ppat) + (curpat_sign, curpat_c, (curpat_ty, curpat_tyargs), curpat) -> + match acc with + None -> None + | Some (sign, len, n, c) -> (* FixMe: do not work with ppat_args *) + if is_included curpat ppat then + (* Length of previous pattern's signature *) + let lens = List.length ppat_sign in + (* Accumulated length of previous pattern's signatures *) + let len' = lens + len in + trace (str "Lifting " ++ my_print_constr Environ.empty_env curpat_c ++ str " by " + ++ int len'); + let acc = + ((* Jump over previous prevpat signs *) + lift_rel_context len ppat_sign @ sign, + len', + succ n, (* nth pattern *) + mkApp (Lazy.force eq_ind, + [| lift (lens + liftsign) ppat_ty ; + liftn liftsign (succ lens) ppat_c ; + lift len' curpat_c |]) :: + List.map + (fun t -> + liftn (List.length curpat_sign) (succ len') (* Jump over the curpat signature *) + (lift lens t (* Jump over this prevpat signature *))) c) + in Some acc + else None) + (Some ([], 0, 0, [])) eqnpats pats + in match acc with + None -> c + | Some (sign, len, _, c') -> + let conj = it_mkProd_or_LetIn (mk_not (mk_conj c')) + (lift_rel_context liftsign sign) + in + conj :: c) + [] prevpatterns + in match diffs with [] -> None + | _ -> Some (mk_conj diffs) + +let subst_rel_context k ctx subst = + let (_, ctx') = + List.fold_right + (fun (n, b, t) (k, acc) -> + (succ k, (n, option_map (substnl subst k) b, substnl subst k t) :: acc)) + ctx (k, []) + in ctx' + +let lift_rel_contextn n k sign = + let rec liftrec k = function + | (na,c,t)::sign -> + (na,option_map (liftn n k) c,type_app (liftn n k) t) + ::(liftrec (k-1) sign) + | [] -> [] + in + liftrec (rel_context_length sign + k) sign + +let constrs_of_pats typing_fun tycon env isevars eqns tomatchs sign neqs eqs arity = 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 (x, y, z) = + List.fold_left + (fun (branches, eqns, prevpatterns) eqn -> + let _, newpatterns, pats = + List.fold_left2 + (fun (idents, newpatterns, pats) pat arsign -> + let pat', cpat, idents = constr_of_pat env isevars arsign pat idents in + (idents, pat' :: newpatterns, cpat :: pats)) + ([], [], []) eqn.patterns sign + in + let newpatterns = List.rev newpatterns and pats = List.rev pats in + let rhs_rels, pats, signlen = + List.fold_left + (fun (renv, pats, n) (sign,c, (s, args), p) -> + (* Recombine signatures and terms of all of the row's patterns *) +(* trace (str "treating pattern:" ++ my_print_constr Environ.empty_env c); *) + let sign' = lift_rel_context n sign in + let len = List.length sign' in + (sign' @ renv, + (* lift to get outside of previous pattern's signatures. *) + (sign', liftn n (succ len) c, (s, List.map (liftn n (succ len)) args), p) :: pats, + len + n)) + ([], [], 0) pats in + let pats, _ = List.fold_left + (* lift to get outside of past patterns to get terms in the combined environment. *) + (fun (pats, n) (sign, c, (s, args), p) -> + let len = List.length sign in + ((rels_of_patsign sign, lift n c, (s, List.map (lift n) args), p) :: pats, len + n)) + ([], 0) pats + in + let rhs_rels' = rels_of_patsign rhs_rels in + let _signenv = push_rel_context rhs_rels' env in +(* trace (str "Env with signature is: " ++ my_print_env _signenv); *) + let ineqs = build_ineqs prevpatterns pats signlen in + let eqs_rels = + let eqs = (*List.concat (List.rev eqs)*) context_of_arsign eqs in + let args, nargs = + List.fold_right (fun (sign, c, (_, args), _) (allargs,n) -> +(* trace (str "treating arg:" ++ my_print_constr Environ.empty_env c); *) + (args @ c :: allargs, List.length args + succ n)) + pats ([], 0) + in + let args = List.rev args in +(* trace (str " equalities " ++ my_print_rel_context Environ.empty_env eqs); *) +(* trace (str " args " ++ pp_list (my_print_constr _signenv) args); *) + (* Make room for substitution of prime arguments by constr patterns *) + let eqs' = lift_rel_contextn signlen nargs eqs in + let eqs'' = subst_rel_context 0 eqs' args in +(* trace (str " new equalities " ++ my_print_rel_context Environ.empty_env eqs'); *) +(* trace (str " subtituted equalities " ++ my_print_rel_context _signenv eqs''); *) + eqs'' + in + let rhs_rels', lift_ineqs = + match ineqs with + None -> eqs_rels @ rhs_rels', 0 + | Some ineqs -> + (* let _ = trace (str"Generated inequalities: " ++ my_print_constr env ineqs) in *) + lift_rel_context 1 eqs_rels @ ((Anonymous, None, ineqs) :: rhs_rels'), 1 + 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_rels + lift_ineqs + 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")); *) + (* (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) + 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 - + let branch = match ineqs with + Some _ -> RApp (dummy_loc, branch, [ hole ]) + | None -> branch + 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, + pats :: prevpatterns)) + ([], [], []) eqns + in x, y + (* liftn_rel_declaration *) @@ -1769,52 +1917,28 @@ let constrs_of_pats typing_fun tycon env isevars eqns tomatchs = * 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 +(* (try List.iter *) +(* (fun arsign -> *) +(* trace (str "arity signature: " ++ my_print_rel_context env arsign)) *) +(* arsign; *) +(* with _ -> trace (str "error in arity signature printing")); *) 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) + match rtntyp with + | Some rtntyp -> + let predcclj = typing_fun (mk_tycon (new_Type ())) env rtntyp in + let predccl = (j_nf_isevar !isevars predcclj).uj_val in + Some (build_initial_predicate true allnames predccl) + | None -> + match valcon_of_tycon tycon with + | Some ty -> + let names,pred = + oldprepare_predicate_from_tycon loc false env isevars tomatchs sign ty + in Some (build_initial_predicate true names pred) + | None -> None let lift_ctx n ctx = let ctx', _ = @@ -1837,70 +1961,240 @@ let abstract_tomatch env tomatchs = ([], [], []) tomatchs in List.rev prev, ctx +let is_dependent_ind = function + IsInd (_, IndType (indf, args)) when List.length args > 0 -> true + | _ -> false + +let build_dependent_signature env evars avoid tomatchs arsign = + let avoid = ref avoid in + let arsign = List.rev arsign 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 eqs, neqs, refls, slift, arsign' = + List.fold_left2 + (fun (eqs, neqs, refl_args, slift, arsigns) (tm, ty) arsign -> + (* The accumulator: + previous eqs, + number of previous eqs, + lift to get outside eqs and in the introduced variables ('as' and 'in'), + new arity signatures + *) + match ty with + IsInd (ty, IndType (indf, args)) when List.length args > 0 -> + (* Build the arity signature following the names in matched terms as much as possible *) + let argsign = List.tl arsign in (* arguments in inverse application order *) + let (appn, appb, appt) as _appsign = List.hd arsign in (* The matched argument *) +(* let _ = trace (str "Working on dependent arg: " ++ my_print_rel_context *) +(* (push_rel_context argsign env) [_appsign]) *) +(* in *) + let argsign = List.rev argsign in (* arguments in application order *) + let env', nargeqs, argeqs, refl_args, slift, argsign' = + List.fold_left2 + (fun (env, nargeqs, argeqs, refl_args, slift, argsign') arg (name, b, t) -> +(* trace (str "Matching indexes: " ++ my_print_constr env arg ++ *) +(* str " and " ++ my_print_rel_context env [(name,b,t)]); *) + let argt = Retyping.get_type_of env evars arg in + let eq, refl_arg = + if Reductionops.is_conv env evars argt t then + (mk_eq (lift (nargeqs + slift) argt) + (mkRel (nargeqs + slift)) + (lift (nargeqs + nar) arg), + mk_eq_refl argt arg) + else + (mk_JMeq (lift (nargeqs + slift) appt) + (mkRel (nargeqs + slift)) + (lift (nargeqs + nar) argt) + (lift (nargeqs + nar) arg), + mk_JMeq_refl argt arg) + in + let previd, id = + let name = + match kind_of_term arg with + Rel n -> pi1 (lookup_rel n (rel_context env)) + | _ -> name + in + make_prime avoid name + in + (env, succ nargeqs, + (Name (eq_id avoid previd), None, eq) :: argeqs, + refl_arg :: refl_args, + pred slift, + (Name id, b, t) :: argsign')) + (env, 0, [], [], slift, []) args argsign + in +(* trace (str "neqs: " ++ int neqs ++ spc () ++ *) +(* str "nargeqs: " ++ int nargeqs ++spc () ++ *) +(* str "slift: " ++ int slift ++spc () ++ *) +(* str "nar: " ++ int nar); *) + let eq = mk_JMeq + (lift (nargeqs + slift) appt) + (mkRel (nargeqs + slift)) + (lift (nargeqs + nar) ty) + (lift (nargeqs + nar) tm) + in + let refl_eq = mk_JMeq_refl ty tm in + let previd, id = make_prime avoid appn in + (((Name (eq_id avoid previd), None, eq) :: argeqs) :: eqs, + succ nargeqs, + refl_eq :: refl_args, + pred slift, + (((Name id, appb, appt) :: argsign') :: arsigns)) + + | _ -> + (* Non dependent inductive or not inductive, just use a regular equality *) + let (name, b, typ) = match arsign with [x] -> x | _ -> assert(false) in + let previd, id = make_prime avoid name in + let arsign' = (Name id, b, typ) in +(* let _ = trace (str "Working on arg: " ++ my_print_rel_context *) +(* env [arsign']) *) +(* in *) + let tomatch_ty = type_of_tomatch ty in + let eq = + mk_eq (lift nar tomatch_ty) + (mkRel slift) (lift nar tm) +(* mk_eq (lift (neqs + nar) tomatch_ty) *) +(* (mkRel (neqs + slift)) (lift (neqs + nar) tm) *) + in + ([(Name (eq_id avoid previd), None, eq)] :: eqs, succ neqs, + (mk_eq_refl tomatch_ty tm) :: refl_args, + pred slift, (arsign' :: []) :: arsigns)) + ([], 0, [], nar, []) tomatchs arsign + in + let arsign'' = List.rev arsign' in + assert(slift = 0); (* we must have folded over all elements of the arity signature *) +(* begin try *) +(* List.iter *) +(* (fun arsign -> *) +(* trace (str "old arity signature: " ++ my_print_rel_context env arsign)) *) +(* arsign; *) + List.iter + (fun c -> + trace (str "new arity signature: " ++ my_print_rel_context env c)) + (arsign''); +(* with _ -> trace (str "error in arity signature printing") *) +(* end; *) + let env' = push_rel_context (context_of_arsign arsign') env in + let _eqsenv = push_rel_context (context_of_arsign eqs) env' in + (try trace (str "Where env with eqs is: " ++ my_print_env _eqsenv); + trace (str "args: " ++ List.fold_left (fun acc x -> acc ++ my_print_constr env x) + (mt()) refls) + with _ -> trace (str "error in equalities signature printing")); + arsign'', allnames, nar, eqs, neqs, refls + +(* let len = List.length eqs in *) +(* it_mkProd_wo_LetIn (lift (nar + len) pred) eqs, pred, len *) + + (**************************************************************************) (* 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 +let liftn_rel_context n k sign = + let rec liftrec k = function + | (na,c,t)::sign -> + (na,option_map (liftn n k) c,type_app (liftn n k) t) + ::(liftrec (k-1) sign) + | [] -> [] + in + liftrec (k + rel_context_length sign) sign + +let nf_evars_env evar_defs (env : env) : env = + let nf t = nf_isevar evar_defs t in + let env0 : env = reset_context env in + let f e (na, b, t) e' : env = + Environ.push_named (na, option_map nf b, nf t) e' + in + let env' = Environ.fold_named_context f ~init:env0 env in + Environ.fold_rel_context (fun e (na, b, t) e' -> Environ.push_rel (na, option_map nf b, nf t) e') + ~init:env' env + +let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns) = (* 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 +(* isevars := nf_evar_defs !isevars; *) +(* let env = nf_evars_env !isevars (env : env) in *) +(* trace (str "Evars : " ++ my_print_evardefs !isevars); *) +(* trace (str "Env : " ++ my_print_env env); *) + 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 - + let _isdep = List.exists (fun (x, y) -> is_dependent_ind y) tomatchs in + if predopt = None then + let len = List.length eqns in + let sign, allnames, signlen, eqs, neqs, args = + (* The arity signature *) + let arsign = extract_arity_signatures env tomatchs (List.map snd tomatchl) in + (* Build the dependent arity signature, the equalities which makes + the first part of the predicate and their instantiations. *) + trace (str "Arity signatures : " ++ my_print_rel_context env (context_of_arsign arsign)); + let avoid = [] in + build_dependent_signature env (Evd.evars_of !isevars) avoid tomatchs arsign + + in + let tycon_constr = + match valcon_of_tycon tycon with + | None -> mkExistential env isevars + | Some t -> t + in + let lets, matx = + (* Type the rhs under the assumption of equations *) + constrs_of_pats typing_fun tycon env isevars matx tomatchs sign neqs + (eqs : rel_context list) (lift (signlen + neqs) tycon_constr) in + + let matx = List.rev matx in + let _ = assert(len = List.length lets) 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 tomatchs = List.map (fun (x, y) -> lift len x, lift_tomatch_type len y) tomatchs in + let args = List.rev_map (lift len) args in + let sign = List.map (lift_rel_context len) sign in + let pred = it_mkProd_wo_LetIn (lift (signlen + neqs) tycon_constr) + (context_of_arsign eqs) in + + let pred = liftn len (succ signlen) pred in +(* it_mkProd_wo_LetIn (lift (len + signlen + neqs) tycon_constr) (liftn_rel_context len signlen eqs) in*) + (* We build the elimination predicate if any and check its consistency *) + (* with the type of arguments to match *) + let _signenv = List.fold_right push_rels sign env in +(* trace (str "Using predicate: " ++ my_print_constr signenv pred ++ str " in env: " ++ my_print_env signenv ++ str " len is " ++ int len); *) + + let pred = + (* prepare_predicate_from_tycon loc typing_fun isevars env tomatchs eqs allnames signlen sign tycon in *) + build_initial_predicate true allnames pred 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 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 = lift (-tomatchs_len) (nf_isevar !isevars tycon_constr); } + in j +(* inh_conv_coerce_to_tycon loc env isevars j tycon0 *) + else + (* 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 predopt 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 diff --git a/contrib/subtac/subtac_cases.mli b/contrib/subtac/subtac_cases.mli index 9e902126..02fe016d 100644 --- a/contrib/subtac/subtac_cases.mli +++ b/contrib/subtac/subtac_cases.mli @@ -19,32 +19,5 @@ 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 +(*s Compilation of pattern-matching, subtac style. *) +module Cases_F(C : Coercion.S) : Cases.S diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml index 3613ec4f..c764443f 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 9563 2007-01-31 09:37:18Z msozeau $ *) +(* $Id: subtac_coercion.ml 9976 2007-07-12 11:58:30Z msozeau $ *) open Util open Names @@ -26,7 +26,6 @@ open Subtac_utils open Coqlib open Printer open Subtac_errors -open Context open Eterm open Pp @@ -86,6 +85,13 @@ module Coercion = struct let hnf env isevars c = whd_betadeltaiota env (evars_of !isevars) c + let lift_args n sign = + let rec liftrec k = function + | t::sign -> liftn n k t :: (liftrec (k-1) sign) + | [] -> [] + in + liftrec (List.length sign) sign + let rec mu env isevars t = let isevars = ref isevars in let rec aux v = @@ -113,15 +119,41 @@ module Coercion = struct (* (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 _ -> ()); *) - None - with Reduction.NotConvertible -> coerce' env (hnf env isevars x) (hnf env isevars y) + let x = hnf env isevars x and y = hnf env isevars y in + 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 _ -> ()); *) + None + with Reduction.NotConvertible -> coerce' env x y and coerce' env x y : (Term.constr -> Term.constr) option = let subco () = subset_coerce env isevars x y in + let rec coerce_application typ c c' l l' = + let len = Array.length l in + let rec aux tele typ i co = + if i < len then + let hdx = l.(i) and hdy = l'.(i) in + try isevars := the_conv_x_leq env hdx hdy !isevars; + let (n, eqT, restT) = destProd typ in + aux (hdx :: tele) (subst1 hdy restT) (succ i) co + with Reduction.NotConvertible -> + let (n, eqT, restT) = destProd typ in + let restargs = lift_args 1 + (List.rev (Array.to_list (Array.sub l (succ i) (len - (succ i))))) + in + let args = List.rev (restargs @ mkRel 1 :: lift_args 1 tele) in + let pred = mkLambda (n, eqT, applistc (lift 1 c) args) in + let eq = mkApp (Lazy.force eq_ind, [| eqT; hdx; hdy |]) in +(* let jmeq = mkApp (Lazy.force jmeq_ind, [| eqT; hdx; eqT; 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 + trace (str"Inserting coercion at application"); + aux (hdy :: tele) (subst1 hdy restT) (succ i) (fun x -> eq_app (co x)) + else co + in aux [] typ 0 (fun x -> x) + in (* (try debug 1 (str "coerce' from " ++ (my_print_constr env x) ++ *) (* str " to "++ my_print_constr env y); *) (* with _ -> ()); *) @@ -214,40 +246,25 @@ module Coercion = struct mkApp (prod.intro, [| a'; b'; x ; y |])) end 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 () + if i = i' && len = Array.length l' then + let evm = evars_of !isevars in + let typ = Typing.type_of env evm c in + (try subco () + with NoSubtacCoercion -> + +(* if not (is_arity env evm typ) then *) + Some (coerce_application typ c c' l l')) +(* else subco () *) + 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 () + if Array.length l = Array.length l' then + let evm = evars_of !isevars in + let lam_type = Typing.type_of env evm c in +(* if not (is_arity env evm lam_type) then ( *) + Some (coerce_application lam_type c c' l l') +(* ) else subco () *) + else subco () | _ -> subco ()) | _, _ -> subco () diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index 68ab8c46..86139039 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -56,7 +56,6 @@ let interp_gen kind isevars env ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[])) c = let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars (Evd.evars_of !isevars) env c in - let c' = Subtac_utils.rewrite_cases env c' in (* (try trace (str "Pretyping " ++ my_print_constr_expr c) with _ -> ()); *) let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in evar_nf isevars c' @@ -178,10 +177,10 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = let env = Global.env() in let nc = named_context env in let nc_len = named_context_length nc 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 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 " : " ++ *) @@ -193,40 +192,42 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = 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 + let liftafter = lift_binders 1 after_length after in let envwf = push_rel_context before env in let wf_rel, wf_rel_fun, measure_fn = let rconstr_body, rconstr = let app = mkAppC (r, [mkIdentC (id_of_name argname)]) in let env = push_rel_context [arg] envwf in let capp = interp_constr isevars env app in - capp, mkLambda (argname, argtyp, capp) + capp, mkLambda (argname, argtyp, capp) in + trace (str"rconstr_body: " ++ pr rconstr_body); if measure then let lt_rel = constr_of_global (Lazy.force lt_ref) in let name s = Name (id_of_string s) in - let wf_rel_fun = - (fun x y -> - mkApp (lt_rel, [| subst1 x rconstr_body; - subst1 y rconstr_body |])) - in + let wf_rel_fun lift x y = (* lift to before_env *) + trace (str"lifter rconstr_body:" ++ pr (liftn lift 2 rconstr_body)); + mkApp (lt_rel, [| subst1 x (liftn lift 2 rconstr_body); + subst1 y (liftn lift 2 rconstr_body) |]) + in let wf_rel = mkLambda (name "x", argtyp, mkLambda (name "y", lift 1 argtyp, - wf_rel_fun (mkRel 2) (mkRel 1))) + wf_rel_fun 0 (mkRel 2) (mkRel 1))) in wf_rel, wf_rel_fun , Some rconstr - else rconstr, (fun x y -> mkApp (rconstr, [|x; y|])), None + else rconstr, (fun lift x y -> mkApp (rconstr, [|x; y|])), None in let wf_proof = mkApp (Lazy.force well_founded, [| argtyp ; wf_rel |]) in let argid' = id_of_string (string_of_id argid ^ "'") in - let wfarg len = (Name argid', None, + let wfarg len = (Name argid', None, mkSubset (Name argid') (lift len argtyp) - (wf_rel_fun (mkRel 1) (mkRel (len + 1)))) + (wf_rel_fun (succ len) (mkRel 1) (mkRel (len + 1)))) in let top_bl = after @ (arg :: before) in - let intern_bl = after @ (wfarg 1 :: arg :: before) in + let intern_bl = liftafter @ (wfarg 1 :: arg :: before) in + (try trace (str "Intern bl: " ++ prr intern_bl) with _ -> ()); let top_env = push_rel_context top_bl env in let _intern_env = push_rel_context intern_bl env in let top_arity = interp_type isevars top_env arityc in @@ -234,36 +235,45 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = let projection = mkApp (proj, [| argtyp ; (mkLambda (Name argid', argtyp, - (wf_rel_fun (mkRel 1) (mkRel 3)))) ; + (wf_rel_fun 1 (mkRel 1) (mkRel 3)))) ; mkRel 1 |]) in - (* (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 _ -> ()); *) + let intern_arity = it_mkProd_or_LetIn top_arity after in + (try trace (str "After length: " ++ int after_length ++ str "Top env: " ++ prr top_bl ++ spc () ++ str "Top arity: " ++ my_print_constr top_env top_arity); + trace (str "Before lifting arity: " ++ my_print_constr env top_arity) with _ -> ()); + (* Top arity is in top_env = after :: arg :: before *) +(* let intern_arity' = liftn 1 (succ after_length) top_arity in (\* arity in after :: wfarg :: arg :: before *\) *) +(* (try trace (str "projection: " "After lifting arity: " ++ my_print_constr env intern_arity' ++ spc ()); *) +(* trace (str "Intern env: " ++ prr intern_bl ++ str "intern_arity': " ++ my_print_constr _intern_env intern_arity') with _ -> ()); *) + let intern_arity = substl [projection] intern_arity in (* substitute the projection of wfarg for arg *) + (try trace (str "Top arity after subst: " ++ my_print_constr (Global.env ()) intern_arity) with _ -> ()); +(* let intern_arity = liftn 1 (succ after_length) intern_arity in (\* back in after :: wfarg :: arg :: before (ie, jump over arg) *\) *) +(* (try trace (str "Top arity after subst and lift: " ++ my_print_constr (Global.env ()) intern_arity) with _ -> ()); *) let intern_before_env = push_rel_context before env in - let intern_fun_bl = after @ [wfarg 1] in +(* let intern_fun_bl = liftafter @ [wfarg 1] in (\* FixMe dependencies *\) *) (* (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 _ -> ()); *) - let intern_fun_arity_prod = it_mkProd_or_LetIn intern_fun_arity intern_fun_bl in + (try trace (str "Intern arity: " ++ + my_print_constr _intern_env intern_arity) with _ -> ()); + let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfarg 1] in + (try trace (str "Intern fun arity product: " ++ + my_print_constr (push_rel_context [arg] intern_before_env) intern_fun_arity_prod) with _ -> ()); let intern_fun_binder = (Name recname, None, intern_fun_arity_prod) in - let fun_bl = after @ (intern_fun_binder :: [arg]) in + let fun_bl = liftafter @ (intern_fun_binder :: [arg]) in (* (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 () ++ *) + let _ = + try trace ((* 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 *) + with _ -> () + in let _impl = if Impargs.is_implicit_args() then Impargs.compute_implicits top_env top_arity @@ -276,13 +286,16 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = mkApp (constr_of_reference (Lazy.force fix_sub_ref), [| argtyp ; wf_rel ; - make_existential dummy_loc intern_before_env isevars wf_proof ; + make_existential dummy_loc ~opaque:false intern_before_env isevars wf_proof ; prop ; intern_body_lam |]) | Some f -> - mkApp (constr_of_reference (Lazy.force fix_measure_sub_ref), - [| argtyp ; f ; prop ; - intern_body_lam |]) + lift (succ after_length) + (mkApp (constr_of_reference (Lazy.force fix_measure_sub_ref), + [| argtyp ; + f ; + prop ; + intern_body_lam |])) in let def_appl = applist (fix_def, gen_rels (after_length + 1)) in let def = it_mkLambda_or_LetIn def_appl binders_rel in @@ -294,15 +307,22 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = (* ++ str "Coq type: " ++ my_print_constr env fullctyp) *) (* with _ -> () *) (* in *) - let evm = non_instanciated_map env isevars in + let evm = evars_of_term (Evd.evars_of !isevars) Evd.empty fullctyp in + let evm = evars_of_term (Evd.evars_of !isevars) evm fullcoqc in + let evm = non_instanciated_map env isevars evm 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 + let evars, evars_def = Eterm.eterm_obligations recname nc_len !isevars evm 0 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 _ -> ()); *) Subtac_obligations.add_definition recname evars_def fullctyp evars + +let nf_evar_context isevars ctx = + List.map (fun (n, b, t) -> + (n, option_map (Evarutil.nf_isevar isevars) b, Evarutil.nf_isevar isevars t)) ctx let build_mutrec l boxed = let sigma = Evd.empty and env = Global.env () in @@ -368,10 +388,13 @@ let build_mutrec l boxed = let (isevars, info, def) = defrec.(i) 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 x, y, typ = arrec.(i) in + let typ = evar_nf isevars typ in + arrec.(i) <- (x, y, typ); + let rec_sign = nf_evar_context !isevars rec_sign 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 evm = Evd.evars_of isevars in - let _, _, typ = arrec.(i) in let id = namerec.(i) in (* Generalize by the recursive prototypes *) let def = @@ -379,7 +402,7 @@ let build_mutrec l boxed = and typ = Termops.it_mkNamedProd_or_LetIn typ rec_sign in - let evars, def = Eterm.eterm_obligations id nc_len evm def (Some typ) in + let evars, def = Eterm.eterm_obligations id nc_len isevars evm recdefs def (Some typ) in collect_evars (succ i) ((id, def, typ, evars) :: acc) else acc in diff --git a/contrib/subtac/subtac_interp_fixpoint.ml b/contrib/subtac/subtac_interp_fixpoint.ml deleted file mode 100644 index bb35833f..00000000 --- a/contrib/subtac/subtac_interp_fixpoint.ml +++ /dev/null @@ -1,154 +0,0 @@ -open Global -open Pp -open Util -open Names -open Sign -open Evd -open Term -open Termops -open Reductionops -open Environ -open Type_errors -open Typeops -open Libnames -open Classops -open List -open Recordops -open Evarutil -open Pretype_errors -open Rawterm -open Evarconv -open Pattern -open Dyn -open Topconstr - -open Subtac_coercion -open Subtac_utils -open Coqlib -open Printer -open Subtac_errors -open Context -open Eterm - - -let mkAppExplC (f, args) = CAppExpl (dummy_loc, (None, f), args) - -let mkSubset name typ prop = - mkAppExplC (sig_ref, - [ typ; mkLambdaC ([name], typ, prop) ]) - -let mkProj1 u p x = - mkAppExplC (proj1_sig_ref, [ u; p; x ]) - -let mkProj2 u p x = - mkAppExplC (proj2_sig_ref, [ u; p; x ]) - -let list_of_local_binders l = - let rec aux acc = function - Topconstr.LocalRawDef (n, c) :: tl -> aux ((n, c) :: acc) tl - | Topconstr.LocalRawAssum (nl, c) :: tl -> - aux (List.fold_left (fun acc n -> (n, c) :: acc) acc nl) tl - | [] -> List.rev acc - in aux [] l - -let abstract_constr_expr_bl abs c bl = - List.fold_right (fun (n, t) c -> abs ([n], t, c)) bl c - -let pr_binder_list b = - List.fold_right (fun ((loc, name), t) acc -> Nameops.pr_name name ++ str " : " ++ - Ppconstr.pr_constr_expr t ++ spc () ++ acc) b (mt ()) - - -let rec rewrite_rec_calls l c = c -(* -let rewrite_fixpoint env l (f, decl) = - let (id, (n, ro), bl, typ, body) = f in - let body = rewrite_rec_calls l body in - match ro with - CStructRec -> ((id, (n, ro), bl, typ, body), decl) - | CWfRec wfrel -> - let bls = list_of_local_binders bl in - let _ = trace (str "Rewriting fixpoint: " ++ Ppconstr.pr_id id ++ - Ppconstr.pr_binders bl ++ str " : " ++ - Ppconstr.pr_constr_expr typ ++ str " := " ++ spc () ++ - Ppconstr.pr_constr_expr body) - in - let before, after = list_chop n bls in - let _ = trace (str "Binders before the recursion arg: " ++ spc () ++ - pr_binder_list before ++ str "; after the recursion arg: " ++ - pr_binder_list after) - in - let ((locn, name) as lnid, ntyp), after = match after with - hd :: tl -> hd, tl - | _ -> assert(false) (* Rec arg must be in after *) - in - let nid = match name with - Name id -> id - | Anonymous -> assert(false) (* Rec arg _must_ be named *) - in - let _wfproof = - let _wf_rel = mkAppExplC (well_founded_ref, [ntyp; wfrel]) in - (*make_existential_expr dummy_loc before wf_rel*) - mkRefC lt_wf_ref - in - let nid', accproofid = - let nid = string_of_id nid in - id_of_string (nid ^ "'"), id_of_string ("Acc_" ^ nid) - in - let lnid', laccproofid = (dummy_loc, Name nid'), (dummy_loc, Name accproofid) in - let wf_prop = (mkAppC (wfrel, [ mkIdentC nid'; mkIdentC nid ])) in - let lam_wf_prop = mkLambdaC ([lnid'], ntyp, wf_prop) in - let typnid' = mkSubset lnid' ntyp wf_prop in - let internal_type = - abstract_constr_expr_bl mkProdC - (mkProdC ([lnid'], typnid', - mkLetInC (lnid, mkProj1 ntyp lam_wf_prop (mkIdentC nid'), - abstract_constr_expr_bl mkProdC typ after))) - before - in - let body' = - let body = - (* cast or we will loose some info at pretyping time as body - is a function *) - CCast (dummy_loc, body, CastConv DEFAULTcast, typ) - in - let body' = (* body abstracted by rec call *) - mkLambdaC ([(dummy_loc, Name id)], internal_type, body) - in - mkAppC (body', - [mkLambdaC - ([lnid'], typnid', - mkAppC (mkIdentC id, - [mkProj1 ntyp lam_wf_prop (mkIdentC nid'); - (mkAppExplC (acc_inv_ref, - [ ntyp; wfrel; - mkIdentC nid; - mkIdentC accproofid; - mkProj1 ntyp lam_wf_prop (mkIdentC nid'); - mkProj2 ntyp lam_wf_prop (mkIdentC nid') ])) ]))]) - in - let acctyp = mkAppExplC (acc_ref, [ ntyp; wfrel; mkIdentC nid ]) in - let bl' = - let rec aux acc = function - Topconstr.LocalRawDef _ as x :: tl -> - aux (x :: acc) tl - | Topconstr.LocalRawAssum (bl, typ) as assum :: tl -> - let rec aux' bl' = function - ((loc, name') as x) :: tl -> - if name' = name then - (if tl = [] then [] else [LocalRawAssum (tl, typ)]) @ - LocalRawAssum ([(dummy_loc, Name accproofid)], acctyp) :: - [LocalRawAssum (List.rev (x :: bl'), typ)] - else aux' (x :: bl') tl - | [] -> [assum] - in aux (aux' [] bl @ acc) tl - | [] -> List.rev acc - in aux [] bl - in - let _ = trace (str "Rewrote fixpoint: " ++ Ppconstr.pr_id id ++ - Ppconstr.pr_binders bl' ++ str " : " ++ - Ppconstr.pr_constr_expr typ ++ str " := " ++ spc () ++ - Ppconstr.pr_constr_expr body') - in (id, (succ n, ro), bl', typ, body'), decl - -*) diff --git a/contrib/subtac/subtac_interp_fixpoint.mli b/contrib/subtac/subtac_interp_fixpoint.mli deleted file mode 100644 index 149e7580..00000000 --- a/contrib/subtac/subtac_interp_fixpoint.mli +++ /dev/null @@ -1,17 +0,0 @@ -val mkAppExplC : - Libnames.reference * Topconstr.constr_expr list -> Topconstr.constr_expr -val mkSubset : - Names.name Util.located -> - Topconstr.constr_expr -> Topconstr.constr_expr -> Topconstr.constr_expr -val mkProj1 : - Topconstr.constr_expr -> - Topconstr.constr_expr -> Topconstr.constr_expr -> Topconstr.constr_expr -val mkProj2 : - Topconstr.constr_expr -> - Topconstr.constr_expr -> Topconstr.constr_expr -> Topconstr.constr_expr -val list_of_local_binders : - Topconstr.local_binder list -> - (Names.name Util.located * Topconstr.constr_expr) list -val pr_binder_list : - (('a * Names.name) * Topconstr.constr_expr) list -> Pp.std_ppcmds -val rewrite_rec_calls : 'a -> 'b -> 'b diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index d6c1772f..d182f7cd 100644 --- a/contrib/subtac/subtac_obligations.ml +++ b/contrib/subtac/subtac_obligations.ml @@ -1,3 +1,4 @@ +(* -*- default-directory: "~/research/coq/trunk/" -*- *) open Printf open Pp open Subtac_utils @@ -12,12 +13,22 @@ open Decl_kinds open Util open Evd -type obligation_info = (Names.identifier * Term.types * Intset.t) array +let pperror cmd = Util.errorlabstrm "Subtac" cmd +let error s = pperror (str s) + +exception NoObligations of identifier option + +let explain_no_obligations = function + Some ident -> str "No obligations for program " ++ str (string_of_id ident) + | None -> str "No obligations remaining" + +type obligation_info = (Names.identifier * Term.types * bool * Intset.t) array type obligation = { obl_name : identifier; obl_type : types; obl_body : constr option; + obl_opaque : bool; obl_deps : Intset.t; } @@ -36,8 +47,9 @@ 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 default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref (Obj.magic ()) -let set_default_tactic t = default_tactic := t +let set_default_tactic t = default_tactic_expr := t; default_tactic := Tacinterp.eval_tactic t let evar_of_obligation o = { evar_hyps = Global.named_context_val () ; evar_concl = o.obl_type ; @@ -81,26 +93,35 @@ let map_first m = let from_prg : program_info ProgMap.t ref = ref ProgMap.empty +let freeze () = !from_prg, !default_tactic_expr +let unfreeze (v, t) = from_prg := v; set_default_tactic t +let init () = + from_prg := ProgMap.empty; set_default_tactic (Subtac_utils.utils_call "subtac_simpl" []) + let _ = Summary.declare_summary "program-tcc-table" - { Summary.freeze_function = (fun () -> !from_prg); - Summary.unfreeze_function = - (fun v -> from_prg := v); - Summary.init_function = - (fun () -> from_prg := ProgMap.empty); + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = init; Summary.survive_module = false; Summary.survive_section = false } -open Evd +let progmap_union = ProgMap.fold ProgMap.add -let terms_of_evar ev = - match ev.evar_body with - Evar_defined b -> - let nc = Environ.named_context_of_val ev.evar_hyps in - let body = Termops.it_mkNamedLambda_or_LetIn b nc in - let typ = Termops.it_mkNamedProd_or_LetIn ev.evar_concl nc in - body, typ - | _ -> assert(false) +let cache (_, (infos, tac)) = + from_prg := infos; + default_tactic_expr := tac + +let (input,output) = + declare_object + { (default_object "Program state") with + cache_function = cache; + load_function = (fun _ -> cache); + open_function = (fun _ -> cache); + classify_function = (fun _ -> Dispose); + export_function = (fun x -> Some x) } + +open Evd let rec intset_to = function -1 -> Intset.empty @@ -113,7 +134,8 @@ let subst_body prg = 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); + my_print_constr (Global.env()) body ++ str " : " ++ + my_print_constr (Global.env()) prg.prg_type); with _ -> ()); let ce = { const_entry_body = body; @@ -163,7 +185,7 @@ let declare_obligation obl body = let ce = { const_entry_body = body; const_entry_type = Some obl.obl_type; - const_entry_opaque = false; + const_entry_opaque = obl.obl_opaque; const_entry_boxed = false} in let constant = Declare.declare_constant obl.obl_name @@ -190,42 +212,53 @@ let red = Reductionops.nf_betaiota let init_prog_info n b t deps nvrec obls = let obls' = Array.mapi - (fun i (n, t, d) -> + (fun i (n, t, o, 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_type = red t; obl_opaque = o; obl_deps = d }) obls in { 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 -> (try ProgMap.find n prg_infos - with Not_found -> error ("No obligations for program " ^ string_of_id n)) + with Not_found -> raise (NoObligations (Some n))) | None -> (let n = map_cardinal prg_infos in match n with - 0 -> error "No obligations remaining" + 0 -> raise (NoObligations None) | 1 -> map_first prg_infos | _ -> error "More than one program with unsolved obligations") +let get_prog_err n = + try get_prog n with NoObligations id -> pperror (explain_no_obligations id) + let obligations_solved prg = (snd prg.prg_obligations) = 0 +let update_state s = +(* msgnl (str "Updating obligations info"); *) + Lib.add_anonymous_leaf (input s) + +let obligations_message rem = + if rem > 0 then + if rem = 1 then + Options.if_verbose msgnl (int rem ++ str " obligation remaining") + else + Options.if_verbose msgnl (int rem ++ str " obligations remaining") + else + Options.if_verbose msgnl (str "No more obligations remaining") + let update_obls prg obls rem = let prg' = { prg with prg_obligations = (obls, rem) } in from_prg := map_replace prg.prg_name prg' !from_prg; - if rem > 0 then ( - Options.if_verbose msgnl (int rem ++ str " obligation(s) remaining"); - ) + obligations_message rem; + if rem > 0 then () else ( - Options.if_verbose msgnl (str "No more obligations remaining"); match prg'.prg_deps with [] -> declare_definition prg'; @@ -235,7 +268,10 @@ let update_obls prg obls rem = 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)) + (fun acc x -> + ProgMap.remove x.prg_name acc) !from_prg progs)); + update_state (!from_prg, !default_tactic_expr); + rem let is_defined obls x = obls.(x).obl_body <> None @@ -246,7 +282,24 @@ let deps_remaining obls deps = else x :: acc) deps [] -let solve_obligation prg num = +let kind_of_opacity o = + if o then Subtac_utils.goal_proof_kind + else Subtac_utils.goal_kind + +let obligations_of_evars evars = + let arr = + Array.of_list + (List.map + (fun (n, t) -> + { obl_name = n; + obl_type = t; + obl_body = None; + obl_opaque = false; + obl_deps = Intset.empty; + }) evars) + in arr, Array.length arr + +let rec solve_obligation prg num = let user_num = succ num in let obls, rem = prg.prg_obligations in let obl = obls.(num) in @@ -256,22 +309,23 @@ let solve_obligation prg num = 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 + Command.start_proof obl.obl_name (kind_of_opacity obl.obl_opaque) obl.obl_type (fun strength gr -> debug 2 (str "Proof of obligation " ++ int user_num ++ str " finished"); let obl = { obl with obl_body = Some (Libnames.constr_of_global gr) } in let obls = Array.copy obls in let _ = obls.(num) <- obl in - update_obls prg obls (pred rem)); + if update_obls prg obls (pred rem) <> 0 then + auto_solve_obligations (Some prg.prg_name)); trace (str "Started obligation " ++ int user_num ++ str " proof: " ++ Subtac_utils.my_print_constr (Global.env ()) obl.obl_type); Pfedit.by !default_tactic | 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) = +and subtac_obligation (user_num, name, typ) = let num = pred user_num in - let prg = get_prog name in + let prg = get_prog_err name in let obls, rem = prg.prg_obligations in if num < Array.length obls then let obl = obls.(num) in @@ -280,20 +334,8 @@ let subtac_obligation (user_num, name, typ) = | Some r -> error "Obligation already solved" else error (sprintf "Unknown obligation number %i" (succ num)) - -let obligations_of_evars evars = - let arr = - Array.of_list - (List.map - (fun (n, t) -> - { obl_name = n; - obl_type = t; - obl_body = None; - obl_deps = Intset.empty; - }) evars) - in arr, Array.length arr - -let solve_obligation_by_tac prg obls i tac = + +and solve_obligation_by_tac prg obls i tac = let obl = obls.(i) in match obl.obl_body with Some _ -> false @@ -302,13 +344,15 @@ let solve_obligation_by_tac prg obls i tac = 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 }; + if obl.obl_opaque then + obls.(i) <- declare_obligation obl t + else + obls.(i) <- { obl with obl_body = Some t }; true else false with _ -> false) -let solve_obligations n tac = - let prg = get_prog n in +and solve_prg_obligations prg tac = let obls, rem = prg.prg_obligations in let rem = ref rem in let obls' = Array.copy obls in @@ -320,6 +364,27 @@ let solve_obligations n tac = in update_obls prg obls' !rem +and solve_obligations n tac = + let prg = get_prog_err n in + solve_prg_obligations prg tac + +and solve_all_obligations tac = + ProgMap.iter (fun k v -> ignore(solve_prg_obligations v tac)) !from_prg + +and try_solve_obligation n prg tac = + let prg = get_prog prg in + let obls, rem = prg.prg_obligations in + let obls' = Array.copy obls in + if solve_obligation_by_tac prg obls' n tac then + ignore(update_obls prg obls' (pred rem)); + +and try_solve_obligations n tac = + try ignore (solve_obligations n tac) with NoObligations _ -> () + +and auto_solve_obligations n : unit = + Options.if_verbose msgnl (str "Solving obligations automatically..."); + try_solve_obligations n !default_tactic + 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 @@ -332,7 +397,7 @@ let add_definition n b t obls = 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) + auto_solve_obligations (Some n)) let add_mutual_definitions l nvrec = let deps = List.map (fun (n, b, t, obls) -> n) l in @@ -343,22 +408,21 @@ let add_mutual_definitions l nvrec = !from_prg l in from_prg := upd; - List.iter (fun x -> solve_obligations (Some x) !default_tactic) deps + List.iter (fun x -> auto_solve_obligations (Some x)) deps let admit_obligations n = - let prg = get_prog n in + let prg = get_prog_err n in let obls, rem = prg.prg_obligations in - let obls' = - Array.mapi (fun i x -> + Array.iteri (fun i x -> match x.obl_body with 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' 0 + let x = subst_deps_obl obls x in + let kn = Declare.declare_constant x.obl_name (ParameterEntry x.obl_type, IsAssumption Conjectural) in + assumption_message x.obl_name; + obls.(i) <- { x with obl_body = Some (mkConst kn) } + | Some _ -> ()) + obls; + ignore(update_obls prg obls 0) exception Found of int @@ -367,21 +431,17 @@ let array_find f arr = raise Not_found with Found i -> i -let rec next_obligation n = - let prg = get_prog n in +let next_obligation n = + let prg = get_prog_err n in let obls, rem = prg.prg_obligations in let i = array_find (fun x -> x.obl_body = None && deps_remaining obls x.obl_deps = []) obls - 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 + in solve_obligation prg i open Pp let show_obligations n = - let prg = get_prog n in + let prg = get_prog_err n in let n = prg.prg_name in let obls, rem = prg.prg_obligations in msgnl (int rem ++ str " obligation(s) remaining: "); @@ -392,3 +452,4 @@ let show_obligations n = | Some _ -> ()) obls +let default_tactic () = !default_tactic diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli index 3981d4c6..f015b80b 100644 --- a/contrib/subtac/subtac_obligations.mli +++ b/contrib/subtac/subtac_obligations.mli @@ -1,8 +1,10 @@ open Util -type obligation_info = (Names.identifier * Term.types * Intset.t) array +type obligation_info = (Names.identifier * Term.types * bool * Intset.t) array + (* ident, type, opaque or transparent, dependencies *) -val set_default_tactic : Proof_type.tactic -> unit +val set_default_tactic : Tacexpr.glob_tactic_expr -> unit +val default_tactic : unit -> Proof_type.tactic val add_definition : Names.identifier -> Term.constr -> Term.types -> obligation_info -> unit @@ -14,8 +16,20 @@ val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr op val next_obligation : Names.identifier option -> unit -val solve_obligations : Names.identifier option -> Proof_type.tactic -> unit +val solve_obligations : Names.identifier option -> Proof_type.tactic -> int +(* Number of remaining obligations to be solved for this program *) + +val solve_all_obligations : Proof_type.tactic -> unit + +val try_solve_obligation : int -> Names.identifier option -> Proof_type.tactic -> unit + +val try_solve_obligations : Names.identifier option -> Proof_type.tactic -> unit val show_obligations : Names.identifier option -> unit val admit_obligations : Names.identifier option -> unit + +exception NoObligations of Names.identifier option + +val explain_no_obligations : Names.identifier option -> Pp.std_ppcmds + diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml index 4d1ac731..cce9a358 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 9563 2007-01-31 09:37:18Z msozeau $ *) +(* $Id: subtac_pretyping.ml 9976 2007-07-12 11:58:30Z msozeau $ *) open Global open Pp @@ -36,7 +36,6 @@ open Subtac_utils open Coqlib open Printer open Subtac_errors -open Context open Eterm module Pretyping = Subtac_pretyping_F.SubtacPretyping_F(Subtac_coercion.Coercion) @@ -89,18 +88,18 @@ let list_split_at index l = open Vernacexpr -let coqintern evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_constr (evars_of evd) env -let coqinterp evd env : Topconstr.constr_expr -> Term.constr = Constrintern.interp_constr (evars_of evd) env +let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_constr (evars_of evd) env +let coqintern_type evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_type (evars_of evd) env let env_with_binders env isevars l = let rec aux ((env, rels) as acc) = function Topconstr.LocalRawDef ((loc, name), def) :: tl -> - let rawdef = coqintern !isevars env def in + let rawdef = coqintern_constr !isevars env def in let coqdef, deftyp = interp env isevars rawdef empty_tycon in let reldecl = (name, Some coqdef, deftyp) in aux (push_rel reldecl env, reldecl :: rels) tl | Topconstr.LocalRawAssum (bl, typ) :: tl -> - let rawtyp = coqintern !isevars env typ in + let rawtyp = coqintern_type !isevars env typ in let coqtyp, typtyp = interp env isevars rawtyp empty_tycon in let acc = List.fold_left (fun (env, rels) (loc, name) -> @@ -113,36 +112,37 @@ let env_with_binders env isevars l = in aux (env, []) l let subtac_process env isevars id l c tycon = - let env_binders, binders_rel = env_with_binders env isevars l in + let c = Command.abstract_constr_expr c l in +(* let env_binders, binders_rel = env_with_binders env isevars l in *) let tycon = match tycon with None -> empty_tycon | Some t -> - let t = coqintern !isevars env_binders t in - let coqt, ttyp = interp env_binders isevars t empty_tycon in + let t = Command.generalize_constr_expr t l in + let t = coqintern_type !isevars env t in + let coqt, ttyp = interp env isevars t empty_tycon in mk_tycon coqt in - let c = coqintern !isevars env_binders c in - let c = Subtac_utils.rewrite_cases env c 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 _ -> () *) + let c = coqintern_constr !isevars env c in + let coqc, ctyp = interp env isevars c tycon in +(* let _ = try trace (str "Interpreted term: " ++ my_print_constr env coqc ++ spc () ++ *) +(* str "Coq type: " ++ my_print_constr env ctyp) *) +(* with _ -> () *) (* in *) -(* let _ = try trace (str "Original evar map: " ++ Evd.pr_evar_map (evars ())) with _ -> () in *) +(* let _ = try trace (str "Original evar map: " ++ Evd.pr_evar_map (evars_of !isevars)) with _ -> () in *) - let fullcoqc = it_mkLambda_or_LetIn coqc binders_rel - and fullctyp = it_mkProd_or_LetIn ctyp binders_rel - in - 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 _ -> () *) +(* let fullcoqc = it_mkLambda_or_LetIn coqc binders_rel *) +(* and fullctyp = it_mkProd_or_LetIn ctyp binders_rel *) (* in *) - let evm = non_instanciated_map env isevars in + let fullcoqc = Evarutil.nf_evar (evars_of !isevars) coqc in + let fullctyp = Evarutil.nf_evar (evars_of !isevars) ctyp in +(* let evm = evars_of_term (evars_of !isevars) Evd.empty fullctyp in *) +(* let evm = evars_of_term (evars_of !isevars) evm fullcoqc in *) +(* let _ = try trace (str "After evar normalization remain: " ++ spc () ++ *) +(* Evd.pr_evar_map evm) *) +(* with _ -> () *) +(* in *) + let evm = non_instanciated_map env isevars (evars_of !isevars) in (* let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in *) evm, fullcoqc, fullctyp @@ -152,5 +152,5 @@ let subtac_proof env isevars id l c tycon = let nc = named_context env in let nc_len = named_context_length nc in let evm, coqc, coqt = subtac_process env isevars id l c tycon in - let evars, def = Eterm.eterm_obligations id nc_len evm coqc (Some coqt) in + let evars, def = Eterm.eterm_obligations id nc_len !isevars evm 0 coqc (Some coqt) in add_definition id def coqt evars diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml index 6244aef3..53eec0b6 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 9563 2007-01-31 09:37:18Z msozeau $ *) +(* $Id: subtac_pretyping_F.ml 9976 2007-07-12 11:58:30Z msozeau $ *) open Pp open Util @@ -93,7 +93,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct (* coerce to tycon if any *) let inh_conv_coerce_to_tycon loc env isevars j = function - | None -> j + | None -> j_nf_isevar !isevars j | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) isevars j t let push_rels vars env = List.fold_right push_rel vars env @@ -364,21 +364,21 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct error_case_not_inductive_loc cloc env (evars_of !isevars) cj in let cstrs = get_constructors env indf in - if Array.length cstrs <> 1 then - user_err_loc (loc,"",str "Destructing let is only for inductive types with one constructor"); - let cs = cstrs.(0) in - if List.length nal <> cs.cs_nargs then - user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables"); - let fsign = List.map2 (fun na (_,c,t) -> (na,c,t)) - (List.rev nal) cs.cs_args in - let env_f = push_rels fsign env in - (* Make dependencies from arity signature impossible *) - let arsgn = - let arsgn,_ = get_arity env indf in - if not !allow_anonymous_refs then - List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn - else arsgn - in + if Array.length cstrs <> 1 then + user_err_loc (loc,"",str "Destructing let is only for inductive types with one constructor"); + let cs = cstrs.(0) in + if List.length nal <> cs.cs_nargs then + user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables"); + let fsign = List.map2 (fun na (_,c,t) -> (na,c,t)) + (List.rev nal) cs.cs_args in + let env_f = push_rels fsign env in + (* Make dependencies from arity signature impossible *) + let arsgn = + let arsgn,_ = get_arity env indf in + if not !allow_anonymous_refs then + List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn + else arsgn + in let psign = (na,None,build_dependent_inductive env indf)::arsgn in let nar = List.length arsgn in (match po with @@ -495,13 +495,13 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct ((fun vtyc env -> pretype vtyc env isevars lvar),isevars) tycon env (* loc *) (po,tml,eqns) - | RCast(loc,c,k,t) -> + | RCast(loc,c,k) -> let cj = match k with CastCoerce -> let cj = pretype empty_tycon env isevars lvar c in evd_comb1 (Coercion.inh_coerce_to_base loc env) isevars cj - | CastConv k -> + | CastConv (k,t) -> let tj = pretype_type empty_valcon env isevars lvar t in let cj = pretype (mk_tycon tj.utj_val) env isevars lvar c in (* User Casts are for helping pretyping, experimentally not to be kept*) diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml index 01dee3e9..28fe6352 100644 --- a/contrib/subtac/subtac_utils.ml +++ b/contrib/subtac/subtac_utils.ml @@ -32,6 +32,7 @@ let fix_sub_ref = make_ref ["subtac";"FixSub"] "Fix_sub" let fix_measure_sub_ref = make_ref ["subtac";"FixSub"] "Fix_measure_sub" let lt_ref = make_ref ["Init";"Peano"] "lt" let lt_wf_ref = make_ref ["Wf_nat"] "lt_wf" +let refl_ref = make_ref ["Init";"Logic"] "refl_equal" let make_ref s = Qualid (dummy_loc, qualid_of_string s) let sig_ref = make_ref "Init.Specif.sig" @@ -54,6 +55,10 @@ 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 not_ref = lazy (init_constant ["Init"; "Logic"] "not") + +let and_typ = lazy (Coqlib.build_coq_and ()) + 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") @@ -61,8 +66,7 @@ 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 jmeq_refl = lazy (init_constant ["Logic";"JMeq"] "JMeq_refl") let ex_ind = lazy (init_constant ["Init"; "Logic"] "ex") let ex_intro = lazy (init_reference ["Init"; "Logic"] "ex_intro") @@ -126,6 +130,10 @@ let trace s = else () else () +let rec pp_list f = function + [] -> mt() + | x :: y -> f x ++ spc () ++ pp_list f y + let wf_relations = Hashtbl.create 10 let std_relations () = @@ -145,8 +153,8 @@ let app_opt c e = let print_args env args = Array.fold_right (fun a acc -> my_print_constr env a ++ spc () ++ acc) args (str "") -let make_existential loc env isevars c = - let evar = Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark) c in +let make_existential loc ?(opaque = true) env isevars c = + let evar = Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark opaque) c in let (key, args) = destEvar evar in (try trace (str "Constructed evar " ++ int key ++ str " applied to args: " ++ print_args env args ++ str " for type: "++ @@ -162,25 +170,33 @@ let make_existential_expr loc env c = let string_of_hole_kind = function | ImplicitArg _ -> "ImplicitArg" | BinderType _ -> "BinderType" - | QuestionMark -> "QuestionMark" + | QuestionMark _ -> "QuestionMark" | CasesType -> "CasesType" | InternalHole -> "InternalHole" | TomatchTypeParameter _ -> "TomatchTypeParameter" - -let non_instanciated_map env evd = - let evm = evars_of !evd in - List.fold_left - (fun evm (key, evi) -> - let (loc,k) = evar_source key !evd in - debug 2 (str "evar " ++ int key ++ str " has kind " ++ - str (string_of_hole_kind k)); - match k with - QuestionMark -> Evd.add evm key evi - | _ -> + +let evars_of_term evc init c = + let rec evrec acc c = + match kind_of_term c with + | Evar (n, _) when Evd.mem evc n -> Evd.add acc n (Evd.find evc n) + | Evar (n, _) -> assert(false) + | _ -> fold_constr evrec acc c + in + evrec init c + +let non_instanciated_map env evd evm = + List.fold_left + (fun evm (key, evi) -> + let (loc,k) = evar_source key !evd in + debug 2 (str "evar " ++ int key ++ str " has kind " ++ + str (string_of_hole_kind k)); + match k with + QuestionMark _ -> Evd.add evm key evi + | _ -> debug 2 (str " and is an implicit"); Pretype_errors.error_unsolvable_implicit loc env evm k) - Evd.empty (Evarutil.non_instantiated evm) - + Evd.empty (Evarutil.non_instantiated evm) + let global_kind = Decl_kinds.IsDefinition Decl_kinds.Definition let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition @@ -247,11 +263,30 @@ let mk_ex_pi1 a b c = let mk_ex_pi2 a b c = mkApp (Lazy.force ex_pi2, [| a; b; c |]) - let mkSubset name typ prop = mkApp ((Lazy.force sig_).typ, [| typ; mkLambda (name, typ, prop) |]) +let mk_eq typ x y = mkApp (Lazy.force eq_ind, [| typ; x ; y |]) +let mk_eq_refl typ x = mkApp (Lazy.force eq_refl, [| typ; x |]) +let mk_JMeq typ x typ' y = mkApp (Lazy.force jmeq_ind, [| typ; x ; typ'; y |]) +let mk_JMeq_refl typ x = mkApp (Lazy.force jmeq_refl, [| typ; x |]) + +let unsafe_fold_right f = function + hd :: tl -> List.fold_right f tl hd + | [] -> raise (Invalid_argument "unsafe_fold_right") + +let mk_conj l = + let conj_typ = Lazy.force and_typ in + unsafe_fold_right + (fun c conj -> + mkApp (conj_typ, [| c ; conj |])) + l + +let mk_not c = + let notc = Lazy.force not_ref in + mkApp (notc, [| c |]) + let and_tac l hook = let andc = Coqlib.build_coq_and () in let rec aux ((accid, goal, tac, extract) as acc) = function @@ -301,291 +336,7 @@ let destruct_ex ext ex = in aux ex ext 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 make_discr (loc, po, tml, eqns) = - let mkHole = RHole (dummy_loc, InternalHole) in - - 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 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 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 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) -> - RLambda (dummy_loc, n, mkHole, acc)) - c eqs_types - in (loc, idl, cpl, c')) - eqns - 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 list_mapi f = - let rec aux i = function - hd :: tl -> f i hd :: aux (succ i) tl - | [] -> [] - in aux 0 - -open Rawterm - -let rewrite_cases_aux (loc, po, tml, eqns) = - let tml' = list_mapi (fun i (c, (n, opt)) -> c, - ((match n with - Name id -> (match c with - | RVar (_, id') when id = id' -> - id, (id_of_string (string_of_id id ^ "Heq_id")) - | RVar (_, id') -> - id', id - | _ -> id_of_string (string_of_id id ^ "Heq_id"), id) - | Anonymous -> - let str = "Heq_id" ^ string_of_int i in - id_of_string str, id_of_string (str ^ "'")), - opt)) tml - in - let mkHole = RHole (dummy_loc, InternalHole) in - let mkCoerceCast c = RCast (dummy_loc, c, CastCoerce, mkHole) in - let mkeq c n = RApp (dummy_loc, RRef (dummy_loc, (Lazy.force eq_ind_ref)), - [mkHole; c; n]) - in - let eqs_types = - List.map - (fun (c, ((id, id'), _)) -> - let heqid = id_of_string ("Heq" ^ string_of_id id) in - Name heqid, mkeq (RVar (dummy_loc, id')) c) - tml' - in - let po = - List.fold_right - (fun (n,t) acc -> - RProd (dummy_loc, Anonymous, t, acc)) - eqs_types (match po with - Some e -> e - | None -> mkHole) - in - let eqns = - List.map (fun (loc, idl, cpl, c) -> - let c' = - List.fold_left - (fun acc (n, t) -> - RLambda (dummy_loc, n, mkHole, acc)) - c eqs_types - in (loc, idl, cpl, c')) - eqns - in - let mk_refl_equal c = RApp (dummy_loc, RRef (dummy_loc, Lazy.force refl_equal_ref), - [mkHole; c]) - in - let refls = List.map (fun (c, ((id, _), _)) -> mk_refl_equal (mkCoerceCast c)) tml' in - let tml'' = List.map (fun (c, ((id, id'), opt)) -> c, (Name id', opt)) tml' in - let case = RCases (loc,Some po,tml'',eqns) in - let app = RApp (dummy_loc, case, refls) in -(* let letapp = List.fold_left (fun acc (c, ((id, id'), opt)) -> RLetIn (dummy_loc, Name id, c, acc)) *) -(* app tml' *) -(* in *) - app - -let rec rewrite_cases c = - match c with - RCases _ -> let c' = map_rawconstr rewrite_cases c in - (match c' with - | RCases (x, y, z, w) -> rewrite_cases_aux (x,y,z,w) - | _ -> assert(false)) - | _ -> map_rawconstr rewrite_cases c - -let rewrite_cases env c = c -(* let c' = rewrite_cases c in *) -(* let _ = trace (str "Rewrote cases: " ++ spc () ++ my_print_rawconstr env c') in *) -(* c' *) - let id_of_name = function Name n -> n | Anonymous -> raise (Invalid_argument "id_of_name") @@ -601,23 +352,6 @@ 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 - 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 @@ -705,3 +439,12 @@ let pr_evar_defs evd = if meta_list evd = [] then mt() else str"METAS:"++brk(0,1)++pr_meta_map evd in v 0 (pp_evm ++ pp_met) + +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)) + diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli index 482640f9..5a5dd427 100644 --- a/contrib/subtac/subtac_utils.mli +++ b/contrib/subtac/subtac_utils.mli @@ -27,6 +27,7 @@ val fix_sub_ref : global_reference lazy_t val fix_measure_sub_ref : global_reference lazy_t val lt_ref : global_reference lazy_t val lt_wf_ref : global_reference lazy_t +val refl_ref : global_reference lazy_t val sig_ref : reference val proj1_sig_ref : reference val proj2_sig_ref : reference @@ -37,13 +38,16 @@ 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 not_ref : constr lazy_t +val and_typ : constr 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 jmeq_ind : constr lazy_t +val jmeq_rec : constr lazy_t +val jmeq_refl : constr lazy_t val boolind : constr lazy_t val sumboolind : constr lazy_t @@ -79,10 +83,11 @@ val wf_relations : (constr, constr lazy_t) Hashtbl.t type binders = local_binder list val app_opt : ('a -> 'a) option -> 'a -> 'a val print_args : env -> constr array -> std_ppcmds -val make_existential : loc -> env -> evar_defs ref -> types -> constr +val make_existential : loc -> ?opaque:bool -> env -> evar_defs ref -> types -> constr val make_existential_expr : loc -> 'a -> 'b -> constr_expr val string_of_hole_kind : hole_kind -> string -val non_instanciated_map : env -> evar_defs ref -> evar_map +val evars_of_term : evar_map -> evar_map -> constr -> evar_map +val non_instanciated_map : env -> evar_defs ref -> evar_map -> evar_map val global_kind : logical_kind val goal_kind : locality_flag * goal_object_kind val global_proof_kind : logical_kind @@ -95,6 +100,12 @@ val mkProj1 : constr -> constr -> constr -> constr val mkProj1 : constr -> constr -> constr -> constr val mk_ex_pi1 : constr -> constr -> constr -> constr val mk_ex_pi1 : constr -> constr -> constr -> constr +val mk_eq : types -> constr -> constr -> types +val mk_eq_refl : types -> constr -> constr +val mk_JMeq : types -> constr-> types -> constr -> types +val mk_JMeq_refl : types -> constr -> constr +val mk_conj : types list -> types +val mk_not : types -> types val build_dependent_sum : (identifier * types) list -> Proof_type.tactic * types val and_tac : (identifier * 'a * constr * Proof_type.tactic) list -> @@ -102,7 +113,6 @@ val and_tac : (identifier * 'a * constr * Proof_type.tactic) list -> val destruct_ex : constr -> constr -> constr list -val rewrite_cases : Environ.env -> Rawterm.rawconstr -> Rawterm.rawconstr val id_of_name : name -> identifier val definition_message : identifier -> unit @@ -114,3 +124,7 @@ 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 + +val utils_call : string -> Tacexpr.glob_tactic_arg list -> Tacexpr.glob_tactic_expr + +val pp_list : ('a -> Pp.std_ppcmds) -> 'a list -> Pp.std_ppcmds diff --git a/contrib/subtac/test/ListDep.v b/contrib/subtac/test/ListDep.v index 7ab720f6..97cef9a5 100644 --- a/contrib/subtac/test/ListDep.v +++ b/contrib/subtac/test/ListDep.v @@ -1,3 +1,4 @@ +(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *) Require Import List. Require Import Coq.subtac.Utils. @@ -21,63 +22,25 @@ Section Map_DependentRecursor. Variable l : list U. Variable f : { x : U | In x l } -> V. + Obligations Tactic := unfold sub_list in * ; + subtac_simpl ; intuition. + Program Fixpoint map_rec ( l' : list U | sub_list l' l ) - { measure l' length } : { r : list V | length r = length l' } := + { measure length l' } : { r : list V | length r = length l' } := match l' with nil => nil | cons x tl => let tl' := map_rec tl in f x :: tl' end. - Obligation 1. - intros. - destruct tl' ; simpl ; simpl in e. - subst x0 tl0. - rewrite <- Heql'. - rewrite e. - auto. - Qed. - - Obligation 2. - simpl. - intros. - destruct l'. - simpl in Heql'. - destruct x0 ; simpl ; try discriminate. - inversion Heql'. - inversion s. - apply H. - auto with datatypes. - Qed. - - - Obligation 3 of map_rec. - simpl. - intros. - rewrite <- Heql'. + Next Obligation. + destruct_call map_rec. + simpl in *. + subst l'. simpl ; auto with arith. - Qed. - - Obligation 4. - simpl. - intros. - destruct l'. - simpl in Heql'. - destruct x0 ; simpl ; try discriminate. - inversion Heql'. - subst x tl. - apply sub_list_tl with u ; auto. - Qed. - - Obligation 5. - intros. - rewrite <- Heql' ; auto. - Qed. - - Program Definition map : list V := map_rec l. - Obligation 1. - split ; auto. - Qed. + Qed. + + Program Definition map : list V := map_rec l. End Map_DependentRecursor. diff --git a/contrib/subtac/test/ListsTest.v b/contrib/subtac/test/ListsTest.v index b8d13fe6..3ceea173 100644 --- a/contrib/subtac/test/ListsTest.v +++ b/contrib/subtac/test/ListsTest.v @@ -70,7 +70,22 @@ Section Nth. Next Obligation. Proof. - inversion l0. + intros. + inversion H. Defined. + + Program Fixpoint nth' (l : list A) (n : nat | n < length l) { struct l } : A := + match l, n with + | hd :: _, 0 => hd + | _ :: tl, S n' => nth' tl n' + | nil, _ => ! + end. + + Next Obligation. + Proof. + intros. + inversion H. + Defined. + End Nth. |