debian release -3

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

diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml
index 7d4a799601dad71082943a92b5685480996b60da..87cf24c2158be45bf601d879c4bfc2690315ec84 100644 (file)
--- a/helm/gTopLevel/proofEngineReduction.ml
+++ b/helm/gTopLevel/proofEngineReduction.ml
@@ -1,4 +1,4 @@
-(* Copyright (C) 2000, HELM Team.
+(* Copyright (C) 2002, HELM Team.
  * 
  * This file is part of HELM, an Hypertextual, Electronic
  * Library of Mathematics, developed at the Computer Science
@@ -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
@@ -276,7 +331,6 @@ let reduce context =
 
 exception WrongShape;;
 exception AlreadySimplified;;
-exception WhatShouldIDo;;
 
 (*CSC: I fear it is still weaker than Coq's one. For example, Coq is *)
 (*CSCS: able to simpl (foo (S n) (S n)) to (foo (S O) n) where       *)
@@ -365,7 +419,8 @@ let simpl context =
                          (* superfluous                                       *)
                          aux (he::rev_constant_args) tl (S.subst he t)
                     end
-                 | C.LetIn (_,_,_) -> raise WhatShouldIDo (*CSC: ?????????? *)
+                 | C.LetIn (_,s,t) ->
+                    aux rev_constant_args l (S.subst s t)
                  | C.Fix (i,fl) as t ->
                     let tys =
                      List.map (function (name,_,ty,_) ->
@@ -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