From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 28 May 2002 17:37:10 +0000 (+0000)
Subject: * Bug fixed: syntactic equality for CIC term (which was used in the Fold tactic)
X-Git-Tag: V_0_3_0_debian_8~68
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=a86e50c2f080bd288d1a37b27fd4d0ea3044c5df

* Bug fixed: syntactic equality for CIC term (which was used in the Fold tactic)
  is not the structural equality of Ocaml (i.e. '=') because of cooking
  numbers that can differ denoting the very same term. So a new function
  syntactic_equality has been added to proofEngineReduction.ml and it is now
  used for Fold.
---

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 695ef7a7f..f33c69e35 100644
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -749,8 +749,10 @@ let fold term =
    (* the type of one metavariable. So we replace it everywhere.   *)
    (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
    (*CSC: che si guadagni nulla in fatto di efficienza.    *) 
-   let replace = ProofEngineReduction.replace
-    ~equality:(=) ~what:term' ~with_what:term
+   let replace =
+    ProofEngineReduction.replace
+     ~equality:(ProofEngineReduction.syntactic_equality)
+     ~what:term' ~with_what:term
    in
     let ty' = replace ty in
     let context' =
diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml
index 7d4a79960..460c8d726 100644
--- a/helm/gTopLevel/proofEngineReduction.ml
+++ b/helm/gTopLevel/proofEngineReduction.ml
@@ -45,6 +45,64 @@ exception ReferenceToInductiveDefinition;;
 exception WrongUriToInductiveDefinition;;
 exception RelToHiddenHypothesis;;
 
+(* syntactic_equality up to cookingsno for uris *)
+(* (which is often syntactically irrilevant)    *)
+let rec syntactic_equality t t' =
+ let module C = Cic in
+  if t = t' then true
+  else
+   match t,t' with
+      C.Rel _, C.Rel _
+    | C.Var _, C.Var _
+    | C.Meta _, C.Meta _
+    | C.Sort _, C.Sort _
+    | C.Implicit, C.Implicit -> false (* we already know that t != t' *)
+    | C.Cast (te,ty), C.Cast (te',ty') ->
+       syntactic_equality te te' &&
+        syntactic_equality ty ty'
+    | C.Prod (n,s,t), C.Prod (n',s',t') ->
+       n = n' &&
+        syntactic_equality s s' &&
+         syntactic_equality t t'
+    | C.Lambda (n,s,t), C.Lambda (n',s',t') ->
+       n = n' &&
+        syntactic_equality s s' &&
+         syntactic_equality t t'
+    | C.LetIn (n,s,t), C.LetIn(n',s',t') ->
+       n = n' &&
+        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,_), C.Const (uri',_) -> UriManager.eq uri uri'
+    | C.Abst _, C.Abst _ -> assert false
+    | C.MutInd (uri,_,i), C.MutInd (uri',_,i') ->
+       UriManager.eq uri uri' && i = i'
+    | C.MutConstruct (uri,_,i,j), C.MutConstruct (uri',_,i',j') ->
+       UriManager.eq uri uri' && i = i' && j = j'
+    | 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 (name,i,ty,bo) (name',i',ty',bo') ->
+           b && name = name' && 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 (name,ty,bo) (name',ty',bo') ->
+           b && name = name' &&
+            syntactic_equality ty ty' &&
+             syntactic_equality bo bo') true fl fl'
+    | _,_ -> false
+;;
+
 (* "textual" replacement of a subterm with another one *)
 let replace ~equality ~what ~with_what ~where =
  let module C = Cic in