alpha equivalence test factorized and moved to CicUtil

diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml
index 08727be1cfde78d6c773dcc76177ff679351dbcd..fb99090e98b76df165c3cbd8244ee17fb70c1601 100644 (file)
--- a/components/acic_procedural/acic2Procedural.ml
+++ b/components/acic_procedural/acic2Procedural.ml
@@ -35,7 +35,6 @@ module A    = Cic2acic
 module Ut   = CicUtil
 module E    = CicEnvironment
 module PEH  = ProofEngineHelpers
-module PER  = ProofEngineReduction
 module Pp   = CicPp
 
 module Cl   = ProceduralClassify
@@ -155,6 +154,14 @@ try
    ty
 with e -> failwith (msg ^ ": " ^ Printexc.to_string e)
 
+let get_entry st id =
+   let rec aux = function
+      | []                                        -> assert false
+      | Some (C.Name name, e) :: _ when name = id -> e
+      | _ :: tl                                   -> aux tl
+   in
+   aux st.context
+   
 (* proof construction *******************************************************)
 
 let unused_premise = "UNUSED"
@@ -174,14 +181,20 @@ let mk_exp_args hd tl classes =
 
 let convert st ?name v = 
    match get_inner_types st v with
-      | None          -> []
-      | Some (st, et) ->
-         let cst, cet = cic st, cic et in
-        if PER.alpha_equivalence cst cet then [] else 
+      | None            -> []
+      | Some (sty, ety) ->
+         let csty, cety = cic sty, cic ety in
+        if Ut.alpha_equivalence csty cety then [] else 
         let e = Cn.mk_pattern 0 (T.mk_arel 1 "") in
         match name with
-           | None    -> [T.Change (st, et, None, e, "")]
-           | Some id -> [T.Change (st, et, Some (id, id), e, ""); T.ClearBody (id, "")]
+           | None    -> [T.Change (sty, ety, None, e, "")]
+           | Some id -> 
+               begin match get_entry st id with
+                 | C.Def _  -> [T.ClearBody (id, "")]
+                 | C.Decl w -> 
+                    if Ut.alpha_equivalence csty w then [] 
+                    else [T.Change (sty, ety, Some (id, id), e, "")] 
+              end
 
 let get_intro = function 
    | C.Anonymous -> unused_premise
@@ -193,7 +206,7 @@ let mk_intros st script =
    T.Intros (Some count, List.rev st.intros, "") :: script
 
 let mk_arg st = function
-   | C.ARel (_, _, _, name) as what -> [] (* convert st ~name what *)
+   | C.ARel (_, _, _, name) as what -> convert st ~name what
    | _                              -> []
 
 let mk_fwd_rewrite st dtext name tl direction =   
@@ -233,7 +246,7 @@ and proc_letin st what name v t =
                  let qs = [[T.Id ""]; proc_proof (next st) v] in
                  [T.Branch (qs, ""); T.Cut (intro, ity, dtext)]
            in
-           C.Decl (get_type "TC1" st v), rqv
+           C.Decl (cic ity), rqv
         | None          ->
            C.Def (cic v, None), [T.LetIn (intro, v, dtext)]
       in

diff --git a/components/cic/cicUtil.ml b/components/cic/cicUtil.ml
index 496452a87bf75f02efaa3344a3742f4592d29406..d79c233dfa100ad96a61a37e4ee8788190332563 100644 (file)
--- a/components/cic/cicUtil.ml
+++ b/components/cic/cicUtil.ml
@@ -25,7 +25,7 @@
 
 (* $Id$ *)
 
-open Printf
+module C = Cic
 
 exception Meta_not_found of int
 exception Subst_not_found of int
@@ -109,30 +109,30 @@ in
 
 let rec is_meta_closed =
   function
-      Cic.Rel _ -> true
-    | Cic.Meta _ -> false
-    | Cic.Sort _ -> true
-    | Cic.Implicit _ -> assert false
-    | Cic.Cast (te,ty) -> is_meta_closed te && is_meta_closed ty
-    | Cic.Prod (name,so,dest) -> is_meta_closed so && is_meta_closed dest
-    | Cic.Lambda (_,so,dest) -> is_meta_closed so && is_meta_closed dest
-    | Cic.LetIn (_,so,dest) -> is_meta_closed so && is_meta_closed dest
-    | Cic.Appl l ->
+      C.Rel _ -> true
+    | C.Meta _ -> false
+    | C.Sort _ -> true
+    | C.Implicit _ -> assert false
+    | C.Cast (te,ty) -> is_meta_closed te && is_meta_closed ty
+    | C.Prod (name,so,dest) -> is_meta_closed so && is_meta_closed dest
+    | C.Lambda (_,so,dest) -> is_meta_closed so && is_meta_closed dest
+    | C.LetIn (_,so,dest) -> is_meta_closed so && is_meta_closed dest
+    | C.Appl l ->
        not (List.exists (fun x -> not (is_meta_closed x)) l)
-    | Cic.Var (_,exp_named_subst)
-    | Cic.Const (_,exp_named_subst)
-    | Cic.MutInd (_,_,exp_named_subst)
-    | Cic.MutConstruct (_,_,_,exp_named_subst) ->
+    | C.Var (_,exp_named_subst)
+    | C.Const (_,exp_named_subst)
+    | C.MutInd (_,_,exp_named_subst)
+    | C.MutConstruct (_,_,_,exp_named_subst) ->
        not (List.exists (fun (_,x) -> not (is_meta_closed x)) exp_named_subst)
-    | Cic.MutCase (_,_,out,te,pl) ->
+    | C.MutCase (_,_,out,te,pl) ->
        is_meta_closed out && is_meta_closed te &&
         not (List.exists (fun x -> not (is_meta_closed x)) pl)
-    | Cic.Fix (_,fl) ->
+    | C.Fix (_,fl) ->
         not (List.exists 
               (fun (_,_,ty,bo) -> 
                   not (is_meta_closed ty) || not (is_meta_closed bo)) 
               fl)
-    | Cic.CoFix (_,fl) ->
+    | C.CoFix (_,fl) ->
         not (List.exists 
               (fun (_,ty,bo) -> 
                   not (is_meta_closed ty) || not (is_meta_closed bo)) 
@@ -146,18 +146,18 @@ let term_of_uri uri =
   let s = UriManager.string_of_uri uri in
   try
     (if UriManager.uri_is_con uri then
-      Cic.Const (uri, [])
+      C.Const (uri, [])
     else if UriManager.uri_is_var uri then
-      Cic.Var (uri, [])
+      C.Var (uri, [])
     else if not (Str.string_match xpointer_RE s 0) then
       raise (UriManager.IllFormedUri s)
     else
       let (baseuri,xpointer) = (Str.matched_group 1 s, Str.matched_group 2 s) in
       let baseuri = UriManager.uri_of_string baseuri in
       (match Str.split slash_RE xpointer with
-      | [_; tyno] -> Cic.MutInd (baseuri, int_of_string tyno - 1, [])
+      | [_; tyno] -> C.MutInd (baseuri, int_of_string tyno - 1, [])
       | [_; tyno; consno] ->
-          Cic.MutConstruct
+          C.MutConstruct
             (baseuri, int_of_string tyno - 1, int_of_string consno, [])
       | _ -> raise Exit))
   with
@@ -166,14 +166,14 @@ let term_of_uri uri =
   | Not_found -> raise (UriManager.IllFormedUri s)
 
 let uri_of_term = function
-  | Cic.Const (uri, _)
-  | Cic.Var (uri, _) -> uri
-  | Cic.MutInd (baseuri, tyno, _) ->
+  | C.Const (uri, _)
+  | C.Var (uri, _) -> uri
+  | C.MutInd (baseuri, tyno, _) ->
      UriManager.uri_of_string
-      (sprintf "%s#xpointer(1/%d)" (UriManager.string_of_uri baseuri) (tyno+1))
-  | Cic.MutConstruct (baseuri, tyno, consno, _) ->
+      (Printf.sprintf "%s#xpointer(1/%d)" (UriManager.string_of_uri baseuri) (tyno+1))
+  | C.MutConstruct (baseuri, tyno, consno, _) ->
      UriManager.uri_of_string
-      (sprintf "%s#xpointer(1/%d/%d)" (UriManager.string_of_uri baseuri)
+      (Printf.sprintf "%s#xpointer(1/%d/%d)" (UriManager.string_of_uri baseuri)
         (tyno + 1) consno)
   | _ -> raise (Invalid_argument "uri_of_term")
 
@@ -181,32 +181,32 @@ let uri_of_term = function
 (*
 let pack terms =
   List.fold_right
-    (fun term acc -> Cic.Prod (Cic.Anonymous, term, acc))
-    terms (Cic.Sort (Cic.Type (CicUniv.fresh ())))
+    (fun term acc -> C.Prod (C.Anonymous, term, acc))
+    terms (C.Sort (C.Type (CicUniv.fresh ())))
 
 let rec unpack = function
-  | Cic.Prod (Cic.Anonymous, term, Cic.Sort (Cic.Type _)) -> [term]
-  | Cic.Prod (Cic.Anonymous, term, tgt) -> term :: unpack tgt
+  | C.Prod (C.Anonymous, term, C.Sort (C.Type _)) -> [term]
+  | C.Prod (C.Anonymous, term, tgt) -> term :: unpack tgt
   | _ -> assert false
 *)
 
 let rec strip_prods n = function
   | t when n = 0 -> t
-  | Cic.Prod (_, _, tgt) when n > 0 -> strip_prods (n-1) tgt
+  | C.Prod (_, _, tgt) when n > 0 -> strip_prods (n-1) tgt
   | _ -> failwith "not enough prods"
 
 let params_of_obj = function
-  | Cic.Constant (_, _, _, params, _)
-  | Cic.Variable (_, _, _, params, _)
-  | Cic.CurrentProof (_, _, _, _, params, _)
-  | Cic.InductiveDefinition (_, params, _, _) ->
+  | C.Constant (_, _, _, params, _)
+  | C.Variable (_, _, _, params, _)
+  | C.CurrentProof (_, _, _, _, params, _)
+  | C.InductiveDefinition (_, params, _, _) ->
       params
 
 let attributes_of_obj = function
-  | Cic.Constant (_, _, _, _, attributes)
-  | Cic.Variable (_, _, _, _, attributes)
-  | Cic.CurrentProof (_, _, _, _, _, attributes)
-  | Cic.InductiveDefinition (_, _, _, attributes) ->
+  | C.Constant (_, _, _, _, attributes)
+  | C.Variable (_, _, _, _, attributes)
+  | C.CurrentProof (_, _, _, _, _, attributes)
+  | C.InductiveDefinition (_, _, _, attributes) ->
       attributes
 
 let is_generated obj = List.exists ((=) `Generated) (attributes_of_obj obj)
@@ -238,26 +238,26 @@ let projections_of_record obj uri =
 let rec mk_rels howmany from =
   match howmany with 
   | 0 -> []
-  | _ -> (Cic.Rel (howmany + from)) :: (mk_rels (howmany-1) from)
+  | _ -> (C.Rel (howmany + from)) :: (mk_rels (howmany-1) from)
 
 let id_of_annterm =
   function
-  | Cic.ARel (id,_,_,_)
-  | Cic.AVar (id,_,_)
-  | Cic.AMeta (id,_,_)
-  | Cic.ASort (id,_)
-  | Cic.AImplicit (id,_)
-  | Cic.ACast (id,_,_)
-  | Cic.AProd (id,_,_,_)
-  | Cic.ALambda (id,_,_,_)
-  | Cic.ALetIn (id,_,_,_)
-  | Cic.AAppl (id,_)
-  | Cic.AConst (id,_,_)
-  | Cic.AMutInd (id,_,_,_)
-  | Cic.AMutConstruct (id,_,_,_,_)
-  | Cic.AMutCase (id,_,_,_,_,_)
-  | Cic.AFix (id,_,_)
-  | Cic.ACoFix (id,_,_) -> id
+  | C.ARel (id,_,_,_)
+  | C.AVar (id,_,_)
+  | C.AMeta (id,_,_)
+  | C.ASort (id,_)
+  | C.AImplicit (id,_)
+  | C.ACast (id,_,_)
+  | C.AProd (id,_,_,_)
+  | C.ALambda (id,_,_,_)
+  | C.ALetIn (id,_,_,_)
+  | C.AAppl (id,_)
+  | C.AConst (id,_,_)
+  | C.AMutInd (id,_,_,_)
+  | C.AMutConstruct (id,_,_,_,_)
+  | C.AMutCase (id,_,_,_,_,_)
+  | C.AFix (id,_,_)
+  | C.ACoFix (id,_,_) -> id
 
 
 let rec rehash_term =
@@ -392,25 +392,25 @@ let rehash_obj =
      C.InductiveDefinition (tl', params', paramsno, attrs)
 
 let rec metas_of_term = function
-  | Cic.Meta (i, c) -> [i,c]
-  | Cic.Var (_, ens) 
-  | Cic.Const (_, ens) 
-  | Cic.MutInd (_, _, ens) 
-  | Cic.MutConstruct (_, _, _, ens) ->
+  | C.Meta (i, c) -> [i,c]
+  | C.Var (_, ens) 
+  | C.Const (_, ens) 
+  | C.MutInd (_, _, ens) 
+  | C.MutConstruct (_, _, _, ens) ->
       List.flatten (List.map (fun (u, t) -> metas_of_term t) ens)
-  | Cic.Cast (s, t)
-  | Cic.Prod (_, s, t)
-  | Cic.Lambda (_, s, t)
-  | Cic.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t)
-  | Cic.Appl l -> List.flatten (List.map metas_of_term l)
-  | Cic.MutCase (uri, i, s, t, l) ->
+  | C.Cast (s, t)
+  | C.Prod (_, s, t)
+  | C.Lambda (_, s, t)
+  | C.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t)
+  | C.Appl l -> List.flatten (List.map metas_of_term l)
+  | C.MutCase (uri, i, s, t, l) ->
       (metas_of_term s) @ (metas_of_term t) @
         (List.flatten (List.map metas_of_term l))
-  | Cic.Fix (i, il) ->
+  | C.Fix (i, il) ->
       List.flatten
         (List.map (fun (s, i, t1, t2) ->
                      (metas_of_term t1) @ (metas_of_term t2)) il)
-  | Cic.CoFix (i, il) ->
+  | C.CoFix (i, il) ->
       List.flatten
         (List.map (fun (s, t1, t2) ->
                      (metas_of_term t1) @ (metas_of_term t2)) il)
@@ -418,41 +418,41 @@ let rec metas_of_term = function
 ;;      
 
 module MetaOT = struct
-  type t = int * Cic.term option list
+  type t = int * C.term option list
   let compare = Pervasives.compare
 end
 
 module S = Set.Make(MetaOT)
 
 let rec metas_of_term_set = function
-  | Cic.Meta (i, c) -> S.singleton (i,c)
-  | Cic.Var (_, ens) 
-  | Cic.Const (_, ens) 
-  | Cic.MutInd (_, _, ens) 
-  | Cic.MutConstruct (_, _, _, ens) ->
+  | C.Meta (i, c) -> S.singleton (i,c)
+  | C.Var (_, ens) 
+  | C.Const (_, ens) 
+  | C.MutInd (_, _, ens) 
+  | C.MutConstruct (_, _, _, ens) ->
       List.fold_left 
         (fun s (_,t) -> S.union s (metas_of_term_set t)) 
         S.empty ens
-  | Cic.Cast (s, t)
-  | Cic.Prod (_, s, t)
-  | Cic.Lambda (_, s, t)
-  | Cic.LetIn (_, s, t) -> S.union (metas_of_term_set s) (metas_of_term_set t)
-  | Cic.Appl l -> 
+  | C.Cast (s, t)
+  | C.Prod (_, s, t)
+  | C.Lambda (_, s, t)
+  | C.LetIn (_, s, t) -> S.union (metas_of_term_set s) (metas_of_term_set t)
+  | C.Appl l -> 
       List.fold_left 
         (fun s t -> S.union s (metas_of_term_set t)) 
         S.empty l
-  | Cic.MutCase (uri, i, s, t, l) ->
+  | C.MutCase (uri, i, s, t, l) ->
       S.union 
         (S.union (metas_of_term_set s)  (metas_of_term_set t))
         (List.fold_left 
           (fun s t -> S.union s (metas_of_term_set t)) 
           S.empty l)
-  | Cic.Fix (_, il) ->
+  | C.Fix (_, il) ->
       (List.fold_left 
         (fun s (_,_,t1,t2) -> 
           S.union s (S.union (metas_of_term_set t1) (metas_of_term_set t2))))
         S.empty il
-  | Cic.CoFix (i, il) ->
+  | C.CoFix (i, il) ->
       (List.fold_left 
         (fun s (_,t1,t2) -> 
           S.union s (S.union (metas_of_term_set t1) (metas_of_term_set t2))))
@@ -465,3 +465,75 @@ let metas_of_term_set t =
   S.elements s
 ;;
 
+(* syntactic_equality up to the                 *)
+(* distinction between fake dependent products  *)
+(* and non-dependent products, alfa-conversion  *)
+let alpha_equivalence =
+  let rec aux t t' =
+   if t = t' then true
+   else
+    match t,t' with
+       C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2) ->
+        UriManager.eq uri1 uri2 &&
+         aux_exp_named_subst exp_named_subst1 exp_named_subst2
+     | C.Cast (te,ty), C.Cast (te',ty') ->
+        aux te te' && aux ty ty'
+     | C.Prod (_,s,t), C.Prod (_,s',t') ->
+        aux s s' && aux t t'
+     | C.Lambda (_,s,t), C.Lambda (_,s',t') ->
+        aux s s' && aux t t'
+     | C.LetIn (_,s,t), C.LetIn(_,s',t') ->
+        aux s s' && aux t t'
+     | C.Appl l, C.Appl l' ->
+        (try
+          List.fold_left2
+           (fun b t1 t2 -> b && aux t1 t2) true l l'
+         with
+          Invalid_argument _ -> false)
+     | C.Const (uri,exp_named_subst1), C.Const (uri',exp_named_subst2) ->
+        UriManager.eq uri uri' &&
+         aux_exp_named_subst exp_named_subst1 exp_named_subst2
+     | C.MutInd (uri,i,exp_named_subst1), C.MutInd (uri',i',exp_named_subst2) ->
+        UriManager.eq uri uri' && i = i' &&
+         aux_exp_named_subst exp_named_subst1 exp_named_subst2
+     | C.MutConstruct (uri,i,j,exp_named_subst1),
+       C.MutConstruct (uri',i',j',exp_named_subst2) ->
+        UriManager.eq uri uri' && i = i' && j = j' &&
+         aux_exp_named_subst exp_named_subst1 exp_named_subst2
+     | C.MutCase (sp,i,outt,t,pl), C.MutCase (sp',i',outt',t',pl') ->
+        UriManager.eq sp sp' && i = i' &&
+         aux outt outt' && aux t t' &&
+          (try
+            List.fold_left2
+             (fun b t1 t2 -> b && aux t1 t2) true pl pl'
+           with
+            Invalid_argument _ -> false)
+     | C.Fix (i,fl), C.Fix (i',fl') ->
+        i = i' &&
+        (try
+          List.fold_left2
+           (fun b (_,i,ty,bo) (_,i',ty',bo') ->
+             b && i = i' && aux ty ty' && aux bo bo'
+           ) true fl fl'
+         with
+          Invalid_argument _ -> false)
+     | C.CoFix (i,fl), C.CoFix (i',fl') ->
+        i = i' &&
+        (try
+          List.fold_left2
+           (fun b (_,ty,bo) (_,ty',bo') ->
+             b && aux ty ty' && aux bo bo'
+           ) true fl fl'
+         with
+          Invalid_argument _ -> false)
+     | _,_ -> false (* we already know that t != t' *)
+  and aux_exp_named_subst exp_named_subst1 exp_named_subst2 =
+   try
+     List.fold_left2
+      (fun b (uri1,t1) (uri2,t2) ->
+        b && UriManager.eq uri1 uri2 && aux t1 t2
+      ) true exp_named_subst1 exp_named_subst2
+    with
+     Invalid_argument _ -> false
+  in
+   aux

diff --git a/components/cic/cicUtil.mli b/components/cic/cicUtil.mli
index 9b1fecf0c25de2218a593884d8f92d9fbd4f17b5..de8c020952ac0262d774ef6c7ad2fff39d5d543a 100644 (file)
--- a/components/cic/cicUtil.mli
+++ b/components/cic/cicUtil.mli
@@ -65,3 +65,4 @@ val mk_rels : int -> int -> Cic.term list
 val rehash_term: Cic.term -> Cic.term
 val rehash_obj: Cic.obj -> Cic.obj
 
+val alpha_equivalence: Cic.term -> Cic.term -> bool

diff --git a/components/cic_acic/doubleTypeInference.ml b/components/cic_acic/doubleTypeInference.ml
index 1ea800a6b9307ec13065fe6d5c853f01a1090ba8..ca5848369c8f735bf410d5308daa67dfe7c9c72a 100644 (file)
--- a/components/cic_acic/doubleTypeInference.ml
+++ b/components/cic_acic/doubleTypeInference.ml
@@ -33,6 +33,8 @@ exception WrongUriToMutualInductiveDefinitions of string;;
 exception ListTooShort;;
 exception RelToHiddenHypothesis;;
 
+(*CSC: must alfa-conversion be considered or not? *)
+
 let xxx_type_of_aux' m c t =
  try 
    Some (fst (CicTypeChecker.type_of_aux' m c t CicUniv.empty_ugraph))
@@ -163,75 +165,6 @@ let rec beta_reduce =
         C.CoFix (i,fl')
 ;;
 
-(* syntactic_equality up to the                 *)
-(* distinction between fake dependent products  *)
-(* and non-dependent products, alfa-conversion  *)
-(*CSC: must alfa-conversion be considered or not? *)
-let syntactic_equality t t' =
- let module C = Cic in
- let rec syntactic_equality t t' =
-  if t = t' then true
-  else
-   match t, t' with
-      C.Var (uri,exp_named_subst), C.Var (uri',exp_named_subst') ->
-       UriManager.eq uri uri' &&
-        syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
-    | C.Cast (te,ty), C.Cast (te',ty') ->
-       syntactic_equality te te' &&
-        syntactic_equality ty ty'
-    | C.Prod (_,s,t), C.Prod (_,s',t') ->
-       syntactic_equality s s' &&
-        syntactic_equality t t'
-    | C.Lambda (_,s,t), C.Lambda (_,s',t') ->
-       syntactic_equality s s' &&
-        syntactic_equality t t'
-    | C.LetIn (_,s,t), C.LetIn(_,s',t') ->
-       syntactic_equality s s' &&
-        syntactic_equality t t'
-    | C.Appl l, C.Appl l' ->
-       List.fold_left2 (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l'
-    | C.Const (uri,exp_named_subst), C.Const (uri',exp_named_subst') ->
-       UriManager.eq uri uri' &&
-        syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
-    | C.MutInd (uri,i,exp_named_subst), C.MutInd (uri',i',exp_named_subst') ->
-       UriManager.eq uri uri' && i = i' &&
-        syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
-    | C.MutConstruct (uri,i,j,exp_named_subst),
-      C.MutConstruct (uri',i',j',exp_named_subst') ->
-       UriManager.eq uri uri' && i = i' && j = j' &&
-        syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
-    | C.MutCase (sp,i,outt,t,pl), C.MutCase (sp',i',outt',t',pl') ->
-       UriManager.eq sp sp' && i = i' &&
-        syntactic_equality outt outt' &&
-         syntactic_equality t t' &&
-          List.fold_left2
-           (fun b t1 t2 -> b && syntactic_equality t1 t2) true pl pl'
-    | C.Fix (i,fl), C.Fix (i',fl') ->
-       i = i' &&
-        List.fold_left2
-         (fun b (_,i,ty,bo) (_,i',ty',bo') ->
-           b && i = i' &&
-            syntactic_equality ty ty' &&
-             syntactic_equality bo bo') true fl fl'
-    | C.CoFix (i,fl), C.CoFix (i',fl') ->
-       i = i' &&
-        List.fold_left2
-         (fun b (_,ty,bo) (_,ty',bo') ->
-           b &&
-            syntactic_equality ty ty' &&
-             syntactic_equality bo bo') true fl fl'
-    | _, _ -> false (* we already know that t != t' *)
- and syntactic_equality_exp_named_subst exp_named_subst1 exp_named_subst2 =
-  List.fold_left2
-   (fun b (_,t1) (_,t2) -> b && syntactic_equality t1 t2) true
-   exp_named_subst1 exp_named_subst2
- in
-  try
-   syntactic_equality t t'
-  with
-   _ -> false
-;;
-
 let rec split l n =
  match (l,n) with
     (l,0) -> ([], l)
@@ -621,7 +554,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
          None ->
           (* No expected type *)
           {synthesized = synthesized' ; expected = None}, synthesized
-       | Some ty when syntactic_equality synthesized' ty ->
+       | Some ty when CicUtil.alpha_equivalence synthesized' ty ->
           (* The expected type is synthactically equal to *)
           (* the synthesized type. Let's forget it.       *)
           {synthesized = synthesized' ; expected = None}, synthesized

diff --git a/components/tactics/inversion.ml b/components/tactics/inversion.ml
index d80814fc363da2945b236a42381ba67e2e8b03bd..5f8a9a37f91ab400b8574cea9f0afe7e1960f2ea 100644 (file)
--- a/components/tactics/inversion.ml
+++ b/components/tactics/inversion.ml
@@ -123,7 +123,7 @@ let rec foo_prod nright right_param_tys rightparameters l2 base_rel goalty
      (CicSubstitution.lift 1 termty)
      isSetType (CicSubstitution.lift 1 term))
    | [] -> ProofEngineReduction.replace_lifting 
-    ~equality:(ProofEngineReduction.alpha_equivalence)
+    ~equality:(CicUtil.alpha_equivalence)
     ~what: (if isSetType
      then (rightparameters_ @ [term] ) 
      else (rightparameters_ ) )
@@ -151,7 +151,7 @@ let rec foo_lambda nright right_param_tys nright_ right_param_tys_
    | [] when isSetType -> Cic.Lambda (
     (Cic.Name ("lambda" ^ (string_of_int nright))),
     (ProofEngineReduction.replace_lifting
-     ~equality:(ProofEngineReduction.alpha_equivalence)
+     ~equality:(CicUtil.alpha_equivalence)
      ~what: (rightparameters_ ) 
      ~with_what: (List.map (CicSubstitution.lift (-1)) created_vars)
      ~where:termty), (* type of H with replaced right parameters *)

diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml
index 07723ea9fe9483fd18afda332169373a7a8f6666..5310fea7e09a6638bb7b5181053748ac3fba0160 100644 (file)
--- a/components/tactics/primitiveTactics.ml
+++ b/components/tactics/primitiveTactics.ml
@@ -701,7 +701,7 @@ let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_nam
     let n_lambdas = n_right_args + 1 in
     let lifted_ty = CicSubstitution.lift n_lambdas ty in
     let replace = ProofEngineReduction.replace_lifting
-       ~equality:(ProofEngineReduction.alpha_equivalence)
+       ~equality:(CicUtil.alpha_equivalence)
     in
     let captured_ty = 
       let what = 

diff --git a/components/tactics/proofEngineReduction.ml b/components/tactics/proofEngineReduction.ml
index f72ec4679842b9888bed5b07b9e92bc48fd50b28..b55b92b9339da1e211acf65c7340511d480356d8 100644 (file)
--- a/components/tactics/proofEngineReduction.ml
+++ b/components/tactics/proofEngineReduction.ml
@@ -49,77 +49,6 @@ exception RelToHiddenHypothesis;;
 module C = Cic
 module S = CicSubstitution
 
-let alpha_equivalence =
-  let rec aux t t' =
-   if t = t' then true
-   else
-    match t,t' with
-       C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2) ->
-        UriManager.eq uri1 uri2 &&
-         aux_exp_named_subst exp_named_subst1 exp_named_subst2
-     | C.Cast (te,ty), C.Cast (te',ty') ->
-        aux te te' && aux ty ty'
-     | C.Prod (_,s,t), C.Prod (_,s',t') ->
-        aux s s' && aux t t'
-     | C.Lambda (_,s,t), C.Lambda (_,s',t') ->
-        aux s s' && aux t t'
-     | C.LetIn (_,s,t), C.LetIn(_,s',t') ->
-        aux s s' && aux t t'
-     | C.Appl l, C.Appl l' ->
-        (try
-          List.fold_left2
-           (fun b t1 t2 -> b && aux t1 t2) true l l'
-         with
-          Invalid_argument _ -> false)
-     | C.Const (uri,exp_named_subst1), C.Const (uri',exp_named_subst2) ->
-        UriManager.eq uri uri' &&
-         aux_exp_named_subst exp_named_subst1 exp_named_subst2
-     | C.MutInd (uri,i,exp_named_subst1), C.MutInd (uri',i',exp_named_subst2) ->
-        UriManager.eq uri uri' && i = i' &&
-         aux_exp_named_subst exp_named_subst1 exp_named_subst2
-     | C.MutConstruct (uri,i,j,exp_named_subst1),
-       C.MutConstruct (uri',i',j',exp_named_subst2) ->
-        UriManager.eq uri uri' && i = i' && j = j' &&
-         aux_exp_named_subst exp_named_subst1 exp_named_subst2
-     | C.MutCase (sp,i,outt,t,pl), C.MutCase (sp',i',outt',t',pl') ->
-        UriManager.eq sp sp' && i = i' &&
-         aux outt outt' && aux t t' &&
-          (try
-            List.fold_left2
-             (fun b t1 t2 -> b && aux t1 t2) true pl pl'
-           with
-            Invalid_argument _ -> false)
-     | C.Fix (i,fl), C.Fix (i',fl') ->
-        i = i' &&
-        (try
-          List.fold_left2
-           (fun b (_,i,ty,bo) (_,i',ty',bo') ->
-             b && i = i' && aux ty ty' && aux bo bo'
-           ) true fl fl'
-         with
-          Invalid_argument _ -> false)
-     | C.CoFix (i,fl), C.CoFix (i',fl') ->
-        i = i' &&
-        (try
-          List.fold_left2
-           (fun b (_,ty,bo) (_,ty',bo') ->
-             b && aux ty ty' && aux bo bo'
-           ) true fl fl'
-         with
-          Invalid_argument _ -> false)
-     | _,_ -> false (* we already know that t != t' *)
-  and aux_exp_named_subst exp_named_subst1 exp_named_subst2 =
-   try
-     List.fold_left2
-      (fun b (uri1,t1) (uri2,t2) ->
-        b && UriManager.eq uri1 uri2 && aux t1 t2
-      ) true exp_named_subst1 exp_named_subst2
-    with
-     Invalid_argument _ -> false
-  in
-   aux
-;;
-
 exception WhatAndWithWhatDoNotHaveTheSameLength;;
 
 (* Replaces "textually" in "where" every term in "what" with the corresponding

diff --git a/components/tactics/proofEngineReduction.mli b/components/tactics/proofEngineReduction.mli
index 78f4b7f4c4e8024550fa91dd05a8ae91db2356a6..2d04d39596ea4149042189b2187ffb1245928ebd 100644 (file)
--- a/components/tactics/proofEngineReduction.mli
+++ b/components/tactics/proofEngineReduction.mli
@@ -34,8 +34,6 @@ exception WrongShape
 exception AlreadySimplified
 exception WhatAndWithWhatDoNotHaveTheSameLength;;
 
-val alpha_equivalence: Cic.term -> Cic.term -> bool
-
 (* Replaces "textually" in "where" every term in "what" with the corresponding
    term in "with_what". The terms in "what" ARE NOT lifted when binders are
    crossed. The terms in "with_what" ARE NOT lifted when binders are crossed.