summaryrefslogtreecommitdiff
path: root/contrib/cc/cctac.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/cc/cctac.ml')
-rw-r--r--contrib/cc/cctac.ml145
1 files changed, 99 insertions, 46 deletions
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 23:04:41 +0000