updated for the new version of mathQL.ml

[helm.git] / helm / gTopLevel / proofEngineReduction.ml

diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml
index 7d4a799601dad71082943a92b5685480996b60da..941a701a920df3b6424fa504efbfecd89e076ab2 100644 (file)
--- a/helm/gTopLevel/proofEngineReduction.ml
+++ b/helm/gTopLevel/proofEngineReduction.ml
@@ -45,6 +45,63 @@ 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.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
@@ -66,7 +123,6 @@ let replace ~equality ~what ~with_what ~where =
            (C.Appl l')::tl -> C.Appl (l'@tl)
          | l' -> C.Appl l')
     | C.Const _ as t -> t
-    | C.Abst _ as t -> t
     | C.MutInd _ as t -> t
     | C.MutConstruct _ as t -> t
     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
@@ -145,7 +201,6 @@ let reduce context =
          | C.CurrentProof (_,_,body,_) -> reduceaux context l body
          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
        )
-    | C.Abst _ as t -> t (*CSC l should be empty ????? *)
     | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
     | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
     | C.MutCase (mutind,cookingsno,i,outtype,term,pl) ->
@@ -207,7 +262,7 @@ let reduce context =
                  eat_first (num_to_eat,tl)
               in
                reduceaux context (ts@l) (List.nth pl (j-1))
-         | C.Abst _ | C.Cast _ | C.Implicit ->
+         | C.Cast _ | C.Implicit ->
             raise (Impossible 2) (* we don't trust our whd ;-) *)
          | _ ->
            let outtype' = reduceaux context [] outtype in
@@ -425,7 +480,6 @@ let simpl context =
          | C.CurrentProof (_,_,body,_) -> reduceaux context l body
          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
        )
-    | C.Abst _ as t -> t (*CSC l should be empty ????? *)
     | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
     | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
     | C.MutCase (mutind,cookingsno,i,outtype,term,pl) ->
@@ -485,7 +539,7 @@ let simpl context =
                  eat_first (num_to_eat,tl)
               in
                reduceaux context (ts@l) (List.nth pl (j-1))
-         | C.Abst _ | C.Cast _ | C.Implicit ->
+         | C.Cast _ | C.Implicit ->
             raise (Impossible 2) (* we don't trust our whd ;-) *)
          | _ ->
            let outtype' = reduceaux context [] outtype in