summaryrefslogtreecommitdiff
path: root/contrib/cc
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/cc')
-rw-r--r--contrib/cc/ccalgo.ml307
-rw-r--r--contrib/cc/ccalgo.mli19
-rw-r--r--contrib/cc/ccproof.ml2
-rw-r--r--contrib/cc/ccproof.mli2
-rw-r--r--contrib/cc/cctac.ml145
-rw-r--r--contrib/cc/cctac.mli4
-rw-r--r--contrib/cc/g_congruence.ml410
7 files changed, 330 insertions, 159 deletions
diff --git a/contrib/cc/ccalgo.ml b/contrib/cc/ccalgo.ml
index 8bdae54b..e67797e4 100644
--- a/contrib/cc/ccalgo.ml
+++ b/contrib/cc/ccalgo.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ccalgo.ml 9151 2006-09-19 13:32:22Z corbinea $ *)
+(* $Id: ccalgo.ml 10579 2008-02-21 13:54:00Z corbinea $ *)
(* This file implements the basic congruence-closure algorithm by *)
(* Downey,Sethi and Tarjan. *)
@@ -16,13 +16,16 @@ open Pp
open Goptions
open Names
open Term
+open Tacmach
+open Evd
+open Proof_type
let init_size=5
let cc_verbose=ref false
-let debug msg (stdpp:std_ppcmds) =
- if !cc_verbose then msg stdpp
+let debug f x =
+ if !cc_verbose then f x
let _=
let gdopt=
@@ -97,7 +100,8 @@ type cinfo=
type term=
Symb of constr
- | Eps
+ | Product of sorts_family * sorts_family
+ | Eps of identifier
| Appli of term*term
| Constructor of cinfo (* constructor arity + nhyps *)
@@ -122,14 +126,19 @@ type equality = rule eq
type disequality = from eq
+type patt_kind =
+ Normal
+ | Trivial of types
+ | Creates_variables
+
type quant_eq =
{qe_hyp_id: identifier;
qe_pol: bool;
qe_nvars:int;
qe_lhs: ccpattern;
- qe_lhs_valid:bool;
+ qe_lhs_valid:patt_kind;
qe_rhs: ccpattern;
- qe_rhs_valid:bool}
+ qe_rhs_valid:patt_kind}
let swap eq : equality =
let swap_rule=match eq.rule with
@@ -145,10 +154,11 @@ type inductive_status =
| Total of (int * pa_constructor)
type representative=
- {mutable nfathers:int;
+ {mutable weight:int;
mutable lfathers:Intset.t;
mutable fathers:Intset.t;
mutable inductive_status: inductive_status;
+ class_type : Term.types;
mutable functions: Intset.t PafMap.t;
mutable constructors: int PacMap.t} (*pac -> term = app(constr,t) *)
@@ -179,9 +189,11 @@ type state =
mutable diseq: disequality list;
mutable quant: quant_eq list;
mutable pa_classes: Intset.t;
- q_history: (constr,unit) Hashtbl.t;
+ q_history: (identifier,int array) Hashtbl.t;
mutable rew_depth:int;
- mutable changed:bool}
+ mutable changed:bool;
+ by_type: (types,Intset.t) Hashtbl.t;
+ mutable gls:Proof_type.goal Tacmach.sigma}
let dummy_node =
{clas=Eqto(min_int,{lhs=min_int;rhs=min_int;rule=Congruence});
@@ -189,7 +201,7 @@ let dummy_node =
vertex=Leaf;
term=Symb (mkRel min_int)}
-let empty depth:state =
+let empty depth gls:state =
{uf=
{max_size=init_size;
size=0;
@@ -206,7 +218,9 @@ let empty depth:state =
pa_classes=Intset.empty;
q_history=Hashtbl.create init_size;
rew_depth=depth;
- changed=false}
+ by_type=Hashtbl.create init_size;
+ changed=false;
+ gls=gls}
let forest state = state.uf
@@ -233,7 +247,7 @@ let get_constructor_info uf i=
| _ -> anomaly "get_constructor: not a constructor"
let size uf i=
- (get_representative uf i).nfathers
+ (get_representative uf i).weight
let axioms uf = uf.axioms
@@ -241,13 +255,13 @@ let epsilons uf = uf.epsilons
let add_lfather uf i t=
let r=get_representative uf i in
- r.nfathers<-r.nfathers+1;
+ r.weight<-r.weight+1;
r.lfathers<-Intset.add t r.lfathers;
r.fathers <-Intset.add t r.fathers
let add_rfather uf i t=
let r=get_representative uf i in
- r.nfathers<-r.nfathers+1;
+ r.weight<-r.weight+1;
r.fathers <-Intset.add t r.fathers
exception Discriminable of int * pa_constructor * int * pa_constructor
@@ -295,19 +309,29 @@ let next uf=
uf.size<-nsize;
size
-let new_representative ()=
- {nfathers=0;
+let new_representative typ =
+ {weight=0;
lfathers=Intset.empty;
fathers=Intset.empty;
inductive_status=Unknown;
+ class_type=typ;
functions=PafMap.empty;
constructors=PacMap.empty}
(* rebuild a constr from an applicative term *)
+let _A_ = Name (id_of_string "A")
+let _B_ = Name (id_of_string "A")
+let _body_ = mkProd(Anonymous,mkRel 2,mkRel 2)
+
+let cc_product s1 s2 =
+ mkLambda(_A_,mkSort(Termops.new_sort_in_family s1),
+ mkLambda(_B_,mkSort(Termops.new_sort_in_family s2),_body_))
+
let rec constr_of_term = function
Symb s->s
- | Eps -> anomaly "epsilon constant has no value"
+ | Product(s1,s2) -> cc_product s1 s2
+ | Eps id -> mkVar id
| Constructor cinfo -> mkConstruct cinfo.ci_constr
| Appli (s1,s2)->
make_app [(constr_of_term s2)] s1
@@ -330,24 +354,31 @@ let rec inst_pattern subst = function
(fun spat f -> Appli (f,inst_pattern subst spat))
args t
+let pr_idx_term state i = str "[" ++ int i ++ str ":=" ++
+ Termops.print_constr (constr_of_term (term state.uf i)) ++ str "]"
+
+let pr_term t = str "[" ++
+ Termops.print_constr (constr_of_term t) ++ str "]"
+
let rec add_term state t=
let uf=state.uf in
try Hashtbl.find uf.syms t with
Not_found ->
let b=next uf in
+ let typ = pf_type_of state.gls (constr_of_term t) in
let new_node=
match t with
- Symb _ ->
+ Symb _ | Product (_,_) ->
let paf =
{fsym=b;
fnargs=0} in
Queue.add (b,Fmark paf) state.marks;
- {clas= Rep (new_representative ());
+ {clas= Rep (new_representative typ);
cpath= -1;
vertex= Leaf;
term= t}
- | Eps ->
- {clas= Rep (new_representative ());
+ | Eps id ->
+ {clas= Rep (new_representative typ);
cpath= -1;
vertex= Leaf;
term= t}
@@ -356,7 +387,7 @@ let rec add_term state t=
add_lfather uf (find uf i1) b;
add_rfather uf (find uf i2) b;
state.terms<-Intset.add b state.terms;
- {clas= Rep (new_representative ());
+ {clas= Rep (new_representative typ);
cpath= -1;
vertex= Node(i1,i2);
term= t}
@@ -370,13 +401,17 @@ let rec add_term state t=
arity= cinfo.ci_arity;
args=[]} in
Queue.add (b,Cmark pac) state.marks;
- {clas=Rep (new_representative ());
+ {clas=Rep (new_representative typ);
cpath= -1;
vertex=Leaf;
term=t}
in
uf.map.(b)<-new_node;
Hashtbl.add uf.syms t b;
+ Hashtbl.replace state.by_type typ
+ (Intset.add b
+ (try Hashtbl.find state.by_type typ with
+ Not_found -> Intset.empty));
b
let add_equality state c s t=
@@ -400,32 +435,53 @@ let add_quant state id pol (nvars,valid1,patt1,valid2,patt2) =
qe_rhs= patt2;
qe_rhs_valid=valid2}::state.quant
+let is_redundant state id args =
+ try
+ let norm_args = Array.map (find state.uf) args in
+ let prev_args = Hashtbl.find_all state.q_history id in
+ List.exists
+ (fun old_args ->
+ Util.array_for_all2 (fun i j -> i = find state.uf j)
+ norm_args old_args)
+ prev_args
+ with Not_found -> false
+
let add_inst state (inst,int_subst) =
- if state.rew_depth > 0 then
- let subst = build_subst (forest state) int_subst in
- let prfhead= mkVar inst.qe_hyp_id in
- let args = Array.map constr_of_term subst in
- let _ = array_rev args in (* highest deBruijn index first *)
- let prf= mkApp(prfhead,args) in
- try Hashtbl.find state.q_history prf
- with Not_found ->
- (* this instance is new, we can go on *)
- let s = inst_pattern subst inst.qe_lhs
- and t = inst_pattern subst inst.qe_rhs in
- state.changed<-true;
- state.rew_depth<-pred state.rew_depth;
- if inst.qe_pol then
- begin
- debug msgnl
- (str "adding new equality, depth="++ int state.rew_depth);
- add_equality state prf s t
- end
- else
- begin
- debug msgnl (str "adding new disequality, depth="++
- int state.rew_depth);
- add_disequality state (Hyp prf) s t
- end
+ check_for_interrupt ();
+ if state.rew_depth > 0 then
+ if is_redundant state inst.qe_hyp_id int_subst then
+ debug msgnl (str "discarding redundant (dis)equality")
+ else
+ begin
+ Hashtbl.add state.q_history inst.qe_hyp_id int_subst;
+ let subst = build_subst (forest state) int_subst in
+ let prfhead= mkVar inst.qe_hyp_id in
+ let args = Array.map constr_of_term subst in
+ let _ = array_rev args in (* highest deBruijn index first *)
+ let prf= mkApp(prfhead,args) in
+ let s = inst_pattern subst inst.qe_lhs
+ and t = inst_pattern subst inst.qe_rhs in
+ state.changed<-true;
+ state.rew_depth<-pred state.rew_depth;
+ if inst.qe_pol then
+ begin
+ debug (fun () ->
+ msgnl
+ (str "Adding new equality, depth="++ int state.rew_depth);
+ msgnl (str " [" ++ Termops.print_constr prf ++ str " : " ++
+ pr_term s ++ str " == " ++ pr_term t ++ str "]")) ();
+ add_equality state prf s t
+ end
+ else
+ begin
+ debug (fun () ->
+ msgnl
+ (str "Adding new disequality, depth="++ int state.rew_depth);
+ msgnl (str " [" ++ Termops.print_constr prf ++ str " : " ++
+ pr_term s ++ str " <> " ++ pr_term t ++ str "]")) ();
+ add_disequality state (Hyp prf) s t
+ end
+ end
let link uf i j eq = (* links i -> j *)
let node=uf.map.(i) in
@@ -448,12 +504,17 @@ let join_path uf i j=
min_path (down_path uf i [],down_path uf j [])
let union state i1 i2 eq=
- debug msgnl (str "Linking " ++ int i1 ++ str " and " ++ int i2 ++ str ".");
+ debug (fun () -> msgnl (str "Linking " ++ pr_idx_term state i1 ++
+ str " and " ++ pr_idx_term state i2 ++ str ".")) ();
let r1= get_representative state.uf i1
and r2= get_representative state.uf i2 in
link state.uf i1 i2 eq;
+ Hashtbl.replace state.by_type r1.class_type
+ (Intset.remove i1
+ (try Hashtbl.find state.by_type r1.class_type with
+ Not_found -> Intset.empty));
let f= Intset.union r1.fathers r2.fathers in
- r2.nfathers<-Intset.cardinal f;
+ r2.weight<-Intset.cardinal f;
r2.fathers<-f;
r2.lfathers<-Intset.union r1.lfathers r2.lfathers;
ST.delete_set state.sigtable r1.fathers;
@@ -483,8 +544,9 @@ let union state i1 i2 eq=
| _,_ -> ()
let merge eq state = (* merge and no-merge *)
- debug msgnl
- (str "Merging " ++ int eq.lhs ++ str " and " ++ int eq.rhs ++ str ".");
+ debug (fun () -> msgnl
+ (str "Merging " ++ pr_idx_term state eq.lhs ++
+ str " and " ++ pr_idx_term state eq.rhs ++ str ".")) ();
let uf=state.uf in
let i=find uf eq.lhs
and j=find uf eq.rhs in
@@ -495,8 +557,8 @@ let merge eq state = (* merge and no-merge *)
union state j i (swap eq)
let update t state = (* update 1 and 2 *)
- debug msgnl
- (str "Updating term " ++ int t ++ str ".");
+ debug (fun () -> msgnl
+ (str "Updating term " ++ pr_idx_term state t ++ str ".")) ();
let (i,j) as sign = signature state.uf t in
let (u,v) = subterms state.uf t in
let rep = get_representative state.uf i in
@@ -556,8 +618,8 @@ let process_constructor_mark t i rep pac state =
end
let process_mark t m state =
- debug msgnl
- (str "Processing mark for term " ++ int t ++ str ".");
+ debug (fun () -> msgnl
+ (str "Processing mark for term " ++ pr_idx_term state t ++ str ".")) ();
let i=find state.uf t in
let rep=get_representative state.uf i in
match m with
@@ -573,9 +635,9 @@ let check_disequalities state =
let uf=state.uf in
let rec check_aux = function
dis::q ->
- debug msg
- (str "Checking if " ++ int dis.lhs ++ str " = " ++
- int dis.rhs ++ str " ... ");
+ debug (fun () -> msg
+ (str "Checking if " ++ pr_idx_term state dis.lhs ++ str " = " ++
+ pr_idx_term state dis.rhs ++ str " ... ")) ();
if find uf dis.lhs=find uf dis.rhs then
begin debug msgnl (str "Yes");Some dis end
else
@@ -601,16 +663,35 @@ let one_step state =
update t state;
true
with Not_found -> false
-
+
+let __eps__ = id_of_string "_eps_"
+
+let new_state_var typ state =
+ let id = pf_get_new_id __eps__ state.gls in
+ state.gls<-
+ {state.gls with it =
+ {state.gls.it with evar_hyps =
+ Environ.push_named_context_val (id,None,typ)
+ state.gls.it.evar_hyps}};
+ id
let complete_one_class state i=
match (get_representative state.uf i).inductive_status with
Partial pac ->
- let rec app t n =
+ let rec app t typ n =
if n<=0 then t else
- app (Appli(t,Eps)) (n-1) in
+ let _,etyp,rest= destProd typ in
+ let id = new_state_var etyp state in
+ app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in
+ let _c = pf_type_of state.gls
+ (constr_of_term (term state.uf pac.cnode)) in
+ let _args =
+ List.map (fun i -> constr_of_term (term state.uf i))
+ pac.args in
+ let typ = prod_applist _c (List.rev _args) in
+ let ct = app (term state.uf i) typ pac.arity in
state.uf.epsilons <- pac :: state.uf.epsilons;
- ignore (add_term state (app (term state.uf i) pac.arity))
+ ignore (add_term state ct)
| _ -> anomaly "wrong incomplete class"
let complete state =
@@ -624,18 +705,18 @@ type matching_problem =
let make_fun_table state =
let uf= state.uf in
let funtab=ref PafMap.empty in
- for cl=0 to pred uf.size do
- match uf.map.(cl).clas with
- Rep rep ->
- PafMap.iter
- (fun paf _ ->
- let elem =
- try PafMap.find paf !funtab
- with Not_found -> Intset.empty in
- funtab:= PafMap.add paf (Intset.add cl elem) !funtab)
- rep.functions
- | _ -> ()
- done;
+ Array.iteri
+ (fun i inode -> if i < uf.size then
+ match inode.clas with
+ Rep rep ->
+ PafMap.iter
+ (fun paf _ ->
+ let elem =
+ try PafMap.find paf !funtab
+ with Not_found -> Intset.empty in
+ funtab:= PafMap.add paf (Intset.add i elem) !funtab)
+ rep.functions
+ | _ -> ()) state.uf.map;
!funtab
@@ -656,6 +737,7 @@ let rec do_match state res pb_stack =
else
if mp.mp_subst.(pred i) = cl then
Stack.push {mp with mp_stack=remains} pb_stack
+ else (* mismatch for non-linear variable in pattern *) ()
| PApp (f,[]) ->
begin
try let j=Hashtbl.find uf.syms f in
@@ -665,19 +747,19 @@ let rec do_match state res pb_stack =
end
| PApp(f, ((last_arg::rem_args) as args)) ->
try
- let j=Hashtbl.find uf.syms f in
+ let j=Hashtbl.find uf.syms f in
let paf={fsym=j;fnargs=List.length args} in
let rep=get_representative uf cl in
let good_terms = PafMap.find paf rep.functions in
let aux i =
- let (s,t) = ST.rev_query i state.sigtable in
+ let (s,t) = signature state.uf i in
Stack.push
{mp with
mp_subst=Array.copy mp.mp_subst;
mp_stack=
(PApp(f,rem_args),s) ::
(last_arg,t) :: remains} pb_stack in
- Intset.iter aux good_terms
+ Intset.iter aux good_terms
with Not_found -> ()
let paf_of_patt syms = function
@@ -692,28 +774,50 @@ let init_pb_stack state =
let funtab = make_fun_table state in
let aux inst =
begin
- if inst.qe_lhs_valid then
- try
- let paf= paf_of_patt syms inst.qe_lhs in
- let good_classes = PafMap.find paf funtab in
- Intset.iter (fun i ->
- Stack.push
- {mp_subst = Array.make inst.qe_nvars (-1);
- mp_inst=inst;
- mp_stack=[inst.qe_lhs,i]} pb_stack) good_classes
- with Not_found -> ()
+ let good_classes =
+ match inst.qe_lhs_valid with
+ Creates_variables -> Intset.empty
+ | Normal ->
+ begin
+ try
+ let paf= paf_of_patt syms inst.qe_lhs in
+ PafMap.find paf funtab
+ with Not_found -> Intset.empty
+ end
+ | Trivial typ ->
+ begin
+ try
+ Hashtbl.find state.by_type typ
+ with Not_found -> Intset.empty
+ end in
+ Intset.iter (fun i ->
+ Stack.push
+ {mp_subst = Array.make inst.qe_nvars (-1);
+ mp_inst=inst;
+ mp_stack=[inst.qe_lhs,i]} pb_stack) good_classes
end;
begin
- if inst.qe_rhs_valid then
- try
- let paf= paf_of_patt syms inst.qe_rhs in
- let good_classes = PafMap.find paf funtab in
- Intset.iter (fun i ->
- Stack.push
- {mp_subst = Array.make inst.qe_nvars (-1);
- mp_inst=inst;
- mp_stack=[inst.qe_rhs,i]} pb_stack) good_classes
- with Not_found -> ()
+ let good_classes =
+ match inst.qe_rhs_valid with
+ Creates_variables -> Intset.empty
+ | Normal ->
+ begin
+ try
+ let paf= paf_of_patt syms inst.qe_rhs in
+ PafMap.find paf funtab
+ with Not_found -> Intset.empty
+ end
+ | Trivial typ ->
+ begin
+ try
+ Hashtbl.find state.by_type typ
+ with Not_found -> Intset.empty
+ end in
+ Intset.iter (fun i ->
+ Stack.push
+ {mp_subst = Array.make inst.qe_nvars (-1);
+ mp_inst=inst;
+ mp_stack=[inst.qe_rhs,i]} pb_stack) good_classes
end in
List.iter aux state.quant;
pb_stack
@@ -724,7 +828,8 @@ let find_instances state =
let _ =
debug msgnl (str "Running E-matching algorithm ... ");
try
- while true do
+ while true do
+ check_for_interrupt ();
do_match state res pb_stack
done;
anomaly "get out of here !"
@@ -734,7 +839,9 @@ let find_instances state =
let rec execute first_run state =
debug msgnl (str "Executing ... ");
try
- while one_step state do ()
+ while
+ check_for_interrupt ();
+ one_step state do ()
done;
match check_disequalities state with
None ->
diff --git a/contrib/cc/ccalgo.mli b/contrib/cc/ccalgo.mli
index 05a5c4d1..cdc0065e 100644
--- a/contrib/cc/ccalgo.mli
+++ b/contrib/cc/ccalgo.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ccalgo.mli 9151 2006-09-19 13:32:22Z corbinea $ *)
+(* $Id: ccalgo.mli 10579 2008-02-21 13:54:00Z corbinea $ *)
open Util
open Term
@@ -19,10 +19,16 @@ type cinfo =
type term =
Symb of constr
- | Eps
+ | Product of sorts_family * sorts_family
+ | Eps of identifier
| Appli of term*term
| Constructor of cinfo (* constructor arity + nhyps *)
+type patt_kind =
+ Normal
+ | Trivial of types
+ | Creates_variables
+
type ccpattern =
PApp of term * ccpattern list
| PVar of int
@@ -70,7 +76,7 @@ val axioms : forest -> (constr, term * term) Hashtbl.t
val epsilons : forest -> pa_constructor list
-val empty : int -> state
+val empty : int -> Proof_type.goal Tacmach.sigma -> state
val add_term : state -> term -> int
@@ -79,8 +85,7 @@ val add_equality : state -> constr -> term -> term -> unit
val add_disequality : state -> from -> term -> term -> unit
val add_quant : state -> identifier -> bool ->
- int * bool * ccpattern * bool * ccpattern -> unit
-
+ int * patt_kind * ccpattern * patt_kind * ccpattern -> unit
val tail_pac : pa_constructor -> pa_constructor
@@ -102,9 +107,9 @@ type quant_eq=
qe_pol: bool;
qe_nvars:int;
qe_lhs: ccpattern;
- qe_lhs_valid:bool;
+ qe_lhs_valid:patt_kind;
qe_rhs: ccpattern;
- qe_rhs_valid:bool}
+ qe_rhs_valid:patt_kind}
type pa_fun=
diff --git a/contrib/cc/ccproof.ml b/contrib/cc/ccproof.ml
index d336f599..a459b18f 100644
--- a/contrib/cc/ccproof.ml
+++ b/contrib/cc/ccproof.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ccproof.ml 9856 2007-05-24 14:05:40Z corbinea $ *)
+(* $Id: ccproof.ml 9857 2007-05-24 14:21:08Z corbinea $ *)
(* This file uses the (non-compressed) union-find structure to generate *)
(* proof-trees that will be transformed into proof-terms in cctac.ml4 *)
diff --git a/contrib/cc/ccproof.mli b/contrib/cc/ccproof.mli
index 572b2c53..0eb97efe 100644
--- a/contrib/cc/ccproof.mli
+++ b/contrib/cc/ccproof.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ccproof.mli 9856 2007-05-24 14:05:40Z corbinea $ *)
+(* $Id: ccproof.mli 9857 2007-05-24 14:21:08Z corbinea $ *)
open Ccalgo
open Names
diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml
index dc0dec0e..871d7521 100644
--- a/contrib/cc/cctac.ml
+++ b/contrib/cc/cctac.ml
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: cctac.ml 10121 2007-09-14 09:45:40Z corbinea $ *)
+(* $Id: cctac.ml 10670 2008-03-14 19:30:48Z letouzey $ *)
(* This file is the interface between the c-c algorithm and Coq *)
@@ -24,6 +24,7 @@ open Termops
open Tacmach
open Tactics
open Tacticals
+open Typing
open Ccalgo
open Tacinterp
open Ccproof
@@ -49,6 +50,8 @@ let _False = constant ["Init";"Logic"] "False"
(* decompose member of equality in an applicative format *)
+let sf_of env sigma c = family_of_sort (destSort (type_of env sigma c))
+
let whd env=
let infos=Closure.create_clos_infos Closure.betaiotazeta env in
(fun t -> Closure.whd_val infos (Closure.inject t))
@@ -57,12 +60,19 @@ let whd_delta env=
let infos=Closure.create_clos_infos Closure.betadeltaiota env in
(fun t -> Closure.whd_val infos (Closure.inject t))
-let rec decompose_term env t=
+let rec decompose_term env sigma t=
match kind_of_term (whd env t) with
App (f,args)->
- let tf=decompose_term env f in
- let targs=Array.map (decompose_term env) args in
+ let tf=decompose_term env sigma f in
+ let targs=Array.map (decompose_term env sigma) args in
Array.fold_left (fun s t->Appli (s,t)) tf targs
+ | Prod (_,a,_b) when not (dependent (mkRel 1) _b) ->
+ let b = pop _b in
+ let sort_b = sf_of env sigma b in
+ let sort_a = sf_of env sigma a in
+ Appli(Appli(Product (sort_a,sort_b) ,
+ decompose_term env sigma a),
+ decompose_term env sigma b)
| Construct c->
let (oib,_)=Global.lookup_inductive (fst c) in
let nargs=mis_constructor_nargs_env env c in
@@ -73,95 +83,111 @@ let rec decompose_term env t=
(* decompose equality in members and type *)
-let atom_of_constr env term =
+let atom_of_constr env sigma term =
let wh = (whd_delta env term) in
let kot = kind_of_term wh in
match kot with
App (f,args)->
if eq_constr f (Lazy.force _eq) && (Array.length args)=3
then `Eq (args.(0),
- decompose_term env args.(1),
- decompose_term env args.(2))
- else `Other (decompose_term env term)
- | _ -> `Other (decompose_term env term)
+ decompose_term env sigma args.(1),
+ decompose_term env sigma args.(2))
+ else `Other (decompose_term env sigma term)
+ | _ -> `Other (decompose_term env sigma term)
-let rec pattern_of_constr env c =
+let rec pattern_of_constr env sigma c =
match kind_of_term (whd env c) with
App (f,args)->
- let pf = decompose_term env f in
+ let pf = decompose_term env sigma f in
let pargs,lrels = List.split
- (array_map_to_list (pattern_of_constr env) args) in
+ (array_map_to_list (pattern_of_constr env sigma) args) in
PApp (pf,List.rev pargs),
- List.fold_left Intset.union Intset.empty lrels
+ List.fold_left Intset.union Intset.empty lrels
+ | Prod (_,a,_b) when not (dependent (mkRel 1) _b) ->
+ let b =pop _b in
+ let pa,sa = pattern_of_constr env sigma a in
+ let pb,sb = pattern_of_constr env sigma (pop b) in
+ let sort_b = sf_of env sigma b in
+ let sort_a = sf_of env sigma a in
+ PApp(Product (sort_a,sort_b),
+ [pa;pb]),(Intset.union sa sb)
| Rel i -> PVar i,Intset.singleton i
| _ ->
- let pf = decompose_term env c in
+ let pf = decompose_term env sigma c in
PApp (pf,[]),Intset.empty
let non_trivial = function
PVar _ -> false
| _ -> true
-let patterns_of_constr env nrels term=
+let patterns_of_constr env sigma nrels term=
let f,args=
try destApp (whd_delta env term) with _ -> raise Not_found in
if eq_constr f (Lazy.force _eq) && (Array.length args)=3
then
- let patt1,rels1 = pattern_of_constr env args.(1)
- and patt2,rels2 = pattern_of_constr env args.(2) in
- let valid1 = (Intset.cardinal rels1 = nrels && non_trivial patt1)
- and valid2 = (Intset.cardinal rels2 = nrels && non_trivial patt2) in
- if valid1 || valid2 then
+ let patt1,rels1 = pattern_of_constr env sigma args.(1)
+ and patt2,rels2 = pattern_of_constr env sigma args.(2) in
+ let valid1 =
+ if Intset.cardinal rels1 <> nrels then Creates_variables
+ else if non_trivial patt1 then Normal
+ else Trivial args.(0)
+ and valid2 =
+ if Intset.cardinal rels2 <> nrels then Creates_variables
+ else if non_trivial patt2 then Normal
+ else Trivial args.(0) in
+ if valid1 <> Creates_variables
+ || valid2 <> Creates_variables then
nrels,valid1,patt1,valid2,patt2
else raise Not_found
else raise Not_found
-let rec quantified_atom_of_constr env nrels term =
+let rec quantified_atom_of_constr env sigma nrels term =
match kind_of_term (whd_delta env term) with
Prod (_,atom,ff) ->
if eq_constr ff (Lazy.force _False) then
- let patts=patterns_of_constr env nrels atom in
+ let patts=patterns_of_constr env sigma nrels atom in
`Nrule patts
else
- quantified_atom_of_constr env (succ nrels) ff
+ quantified_atom_of_constr env sigma (succ nrels) ff
| _ ->
- let patts=patterns_of_constr env nrels term in
+ let patts=patterns_of_constr env sigma nrels term in
`Rule patts
-let litteral_of_constr env term=
+let litteral_of_constr env sigma term=
match kind_of_term (whd_delta env term) with
| Prod (_,atom,ff) ->
if eq_constr ff (Lazy.force _False) then
- match (atom_of_constr env atom) with
+ match (atom_of_constr env sigma atom) with
`Eq(t,a,b) -> `Neq(t,a,b)
| `Other(p) -> `Nother(p)
else
begin
try
- quantified_atom_of_constr env 1 ff
+ quantified_atom_of_constr env sigma 1 ff
with Not_found ->
- `Other (decompose_term env term)
+ `Other (decompose_term env sigma term)
end
| _ ->
- atom_of_constr env term
+ atom_of_constr env sigma term
(* store all equalities from the context *)
let rec make_prb gls depth additionnal_terms =
let env=pf_env gls in
- let state = empty depth in
+ let sigma=sig_sig gls in
+ let state = empty depth gls in
let pos_hyps = ref [] in
let neg_hyps =ref [] in
List.iter
(fun c ->
- let t = decompose_term env c in
+ let t = decompose_term env sigma c in
ignore (add_term state t)) additionnal_terms;
List.iter
(fun (id,_,e) ->
begin
let cid=mkVar id in
- match litteral_of_constr env e with
+ match litteral_of_constr env sigma e with
`Eq (t,a,b) -> add_equality state cid a b
| `Neq (t,a,b) -> add_disequality state (Hyp cid) a b
| `Other ph ->
@@ -180,7 +206,7 @@ let rec make_prb gls depth additionnal_terms =
| `Nrule patts -> add_quant state id false patts
end) (Environ.named_context_of_val gls.it.evar_hyps);
begin
- match atom_of_constr env gls.it.evar_concl with
+ match atom_of_constr env sigma gls.it.evar_concl with
`Eq (t,a,b) -> add_disequality state Goal a b
| `Other g ->
List.iter
@@ -209,7 +235,7 @@ let build_projection intype outtype (cstr:constructor) special default gls=
let branches=Array.init lp branch in
let casee=mkRel 1 in
let pred=mkLambda(Anonymous,intype,outtype) in
- let case_info=make_default_case_info (pf_env gls) RegularStyle ind in
+ let case_info=make_case_info (pf_env gls) ind RegularStyle in
let body= mkCase(case_info, pred, casee, branches) in
let id=pf_get_new_id (id_of_string "t") gls in
mkLambda(Name id,intype,body)
@@ -224,19 +250,19 @@ let rec proof_tac p gls =
| SymAx c ->
let l=constr_of_term p.p_lhs and
r=constr_of_term p.p_rhs in
- let typ = pf_type_of gls l in
+ let typ = refresh_universes (pf_type_of gls l) in
exact_check
(mkApp(Lazy.force _sym_eq,[|typ;r;l;c|])) gls
| Refl t ->
let lr = constr_of_term t in
- let typ = pf_type_of gls lr in
+ let typ = refresh_universes (pf_type_of gls lr) in
exact_check
(mkApp(Lazy.force _refl_equal,[|typ;constr_of_term t|])) gls
| Trans (p1,p2)->
let t1 = constr_of_term p1.p_lhs and
t2 = constr_of_term p1.p_rhs and
t3 = constr_of_term p2.p_rhs in
- let typ = pf_type_of gls t2 in
+ let typ = refresh_universes (pf_type_of gls t2) in
let prf =
mkApp(Lazy.force _trans_eq,[|typ;t1;t2;t3;_M 1;_M 2|]) in
tclTHENS (refine prf) [(proof_tac p1);(proof_tac p2)] gls
@@ -245,16 +271,17 @@ let rec proof_tac p gls =
and tx1=constr_of_term p2.p_lhs
and tf2=constr_of_term p1.p_rhs
and tx2=constr_of_term p2.p_rhs in
- let typf = pf_type_of gls tf1 in
- let typx = pf_type_of gls tx1 in
- let typfx = pf_type_of gls (mkApp (tf1,[|tx1|])) in
+ let typf = refresh_universes (pf_type_of gls tf1) in
+ let typx = refresh_universes (pf_type_of gls tx1) in
+ let typfx = refresh_universes (pf_type_of gls (mkApp (tf1,[|tx1|]))) in
let id = pf_get_new_id (id_of_string "f") gls in
let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
let lemma1 =
mkApp(Lazy.force _f_equal,
[|typf;typfx;appx1;tf1;tf2;_M 1|]) in
let lemma2=
- mkApp(Lazy.force _f_equal,[|typx;typfx;tf2;tx1;tx2;_M 1|]) in
+ mkApp(Lazy.force _f_equal,
+ [|typx;typfx;tf2;tx1;tx2;_M 1|]) in
let prf =
mkApp(Lazy.force _trans_eq,
[|typfx;
@@ -274,8 +301,8 @@ let rec proof_tac p gls =
let ti=constr_of_term prf.p_lhs in
let tj=constr_of_term prf.p_rhs in
let default=constr_of_term p.p_lhs in
- let intype=pf_type_of gls ti in
- let outtype=pf_type_of gls default in
+ let intype=refresh_universes (pf_type_of gls ti) in
+ let outtype=refresh_universes (pf_type_of gls default) in
let special=mkRel (1+nargs-argind) in
let proj=build_projection intype outtype cstr special default gls in
let injt=
@@ -284,7 +311,7 @@ let rec proof_tac p gls =
let refute_tac c t1 t2 p gls =
let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
- let intype=pf_type_of gls tt1 in
+ let intype=refresh_universes (pf_type_of gls tt1) in
let neweq=
mkApp(Lazy.force _eq,
[|intype;tt1;tt2|]) in
@@ -295,7 +322,7 @@ let refute_tac c t1 t2 p gls =
let convert_to_goal_tac c t1 t2 p gls =
let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
- let sort=pf_type_of gls tt2 in
+ let sort=refresh_universes (pf_type_of gls tt2) in
let neweq=mkApp(Lazy.force _eq,[|sort;tt1;tt2|]) in
let e=pf_get_new_id (id_of_string "e") gls in
let x=pf_get_new_id (id_of_string "X") gls in
@@ -315,7 +342,7 @@ let convert_to_hyp_tac c1 t1 c2 t2 p gls =
let discriminate_tac cstr p gls =
let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in
- let intype=pf_type_of gls t1 in
+ let intype=refresh_universes (pf_type_of gls t1) in
let concl=pf_concl gls in
let outsort=mkType (new_univ ()) in
let xid=pf_get_new_id (id_of_string "X") gls in
@@ -403,3 +430,29 @@ let congruence_tac depth l =
tclORELSE
(tclTHEN (tclREPEAT introf) (cc_tactic depth l))
cc_fail
+
+(* The [f_equal] tactic.
+
+ It mimics the use of lemmas [f_equal], [f_equal2], etc.
+ This isn't particularly related with congruence, apart from
+ the fact that congruence is called internally.
+*)
+
+let f_equal gl =
+ let cut_eq c1 c2 =
+ let ty = refresh_universes (pf_type_of gl c1) in
+ tclTHENTRY
+ (Tactics.cut (mkApp (Lazy.force _eq, [|ty; c1; c2|]))) reflexivity
+ in
+ try match kind_of_term (pf_concl gl) with
+ | App (r,[|_;t;t'|]) when eq_constr r (Lazy.force _eq) ->
+ begin match kind_of_term t, kind_of_term t' with
+ | App (f,v), App (f',v') when Array.length v = Array.length v' ->
+ let rec cuts i =
+ if i < 0 then tclTRY (congruence_tac 1000 [])
+ else tclTHENFIRST (cut_eq v.(i) v'.(i)) (cuts (i-1))
+ in cuts (Array.length v - 1) gl
+ | _ -> tclIDTAC gl
+ end
+ | _ -> tclIDTAC gl
+ with Type_errors.TypeError _ -> tclIDTAC gl
diff --git a/contrib/cc/cctac.mli b/contrib/cc/cctac.mli
index ffc4b9c4..57ad0558 100644
--- a/contrib/cc/cctac.mli
+++ b/contrib/cc/cctac.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: cctac.mli 10121 2007-09-14 09:45:40Z corbinea $ *)
+(* $Id: cctac.mli 10637 2008-03-07 23:52:56Z letouzey $ *)
open Term
open Proof_type
@@ -18,3 +18,5 @@ val cc_tactic : int -> constr list -> tactic
val cc_fail : tactic
val congruence_tac : int -> constr list -> tactic
+
+val f_equal : tactic
diff --git a/contrib/cc/g_congruence.ml4 b/contrib/cc/g_congruence.ml4
index 693aebb4..9877e6fc 100644
--- a/contrib/cc/g_congruence.ml4
+++ b/contrib/cc/g_congruence.ml4
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: g_congruence.ml4 9151 2006-09-19 13:32:22Z corbinea $ *)
+(* $Id: g_congruence.ml4 10637 2008-03-07 23:52:56Z letouzey $ *)
open Cctac
open Tactics
@@ -17,9 +17,13 @@ open Tacticals
(* Tactic registration *)
TACTIC EXTEND cc
- [ "congruence" ] -> [ congruence_tac 0 [] ]
+ [ "congruence" ] -> [ congruence_tac 1000 [] ]
|[ "congruence" integer(n) ] -> [ congruence_tac n [] ]
- |[ "congruence" "with" ne_constr_list(l) ] -> [ congruence_tac 0 l ]
+ |[ "congruence" "with" ne_constr_list(l) ] -> [ congruence_tac 1000 l ]
|[ "congruence" integer(n) "with" ne_constr_list(l) ] ->
[ congruence_tac n l ]
END
+
+TACTIC EXTEND f_equal
+ [ "f_equal" ] -> [ f_equal ]
+END
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 06:03:16 +0000