X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngineReduction.ml;h=bb724fc758d2736c40a7c199b60898501fe4308a;hb=a4df9661e15509e5da6ed9c57e3ab6a27a440c3f;hp=7d4a799601dad71082943a92b5685480996b60da;hpb=ee35bf33520d92753899985329cc4bfee141b808;p=helm.git

diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml
index 7d4a79960..bb724fc75 100644
--- 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,69 @@ exception ReferenceToInductiveDefinition;;
 exception WrongUriToInductiveDefinition;;
 exception RelToHiddenHypothesis;;
 
+(* syntactic_equality up to cookingsno for uris *)
+(* (which is often syntactically irrilevant)    *)
+let syntactic_equality ~alpha_equivalence =
+ let module C = Cic in
+  let rec aux t t' =
+   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') ->
+        aux te te' && aux ty ty'
+     | C.Prod (n,s,t), C.Prod (n',s',t') ->
+        (alpha_equivalence || n = n') && aux s s' && aux t t'
+     | C.Lambda (n,s,t), C.Lambda (n',s',t') ->
+        (alpha_equivalence || n = n') && aux s s' && aux t t'
+     | C.LetIn (n,s,t), C.LetIn(n',s',t') ->
+        (alpha_equivalence || n = n') && 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,_), 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' &&
+         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 (name,i,ty,bo) (name',i',ty',bo') ->
+             b && (alpha_equivalence || name = name') && 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 (name,ty,bo) (name',ty',bo') ->
+             b && (alpha_equivalence || name = name') &&
+              aux ty ty' && aux bo bo') true fl fl'
+         with
+          Invalid_argument _ -> false)
+     | _,_ -> false
+ in
+  aux
+;;
+
 (* "textual" replacement of a subterm with another one *)
 let replace ~equality ~what ~with_what ~where =
  let module C = Cic in
@@ -66,7 +129,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) ->
@@ -90,6 +152,71 @@ let replace ~equality ~what ~with_what ~where =
    aux where
 ;;
 
+(* replaces in a term a term with another one. *)
+(* Lifting are performed as usual.             *)
+let replace_lifting ~equality ~what ~with_what ~where =
+ let rec substaux k what =
+  let module C = Cic in
+  let module S = CicSubstitution in
+   function
+      t when (equality t what) -> S.lift (k-1) with_what
+    | C.Rel n as t -> t
+    | C.Var _ as t  -> t
+    | C.Meta (i, l) as t -> 
+       let l' =
+        List.map
+         (function
+             None -> None
+           | Some t -> Some (substaux k what t)
+         ) l
+       in
+        C.Meta(i,l')
+    | C.Sort _ as t -> t
+    | C.Implicit as t -> t
+    | C.Cast (te,ty) -> C.Cast (substaux k what te, substaux k what ty)
+    | C.Prod (n,s,t) ->
+       C.Prod (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t)
+    | C.Lambda (n,s,t) ->
+       C.Lambda (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t)
+    | C.LetIn (n,s,t) ->
+       C.LetIn (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t)
+    | C.Appl (he::tl) ->
+       (* Invariant: no Appl applied to another Appl *)
+       let tl' = List.map (substaux k what) tl in
+        begin
+         match substaux k what he with
+            C.Appl l -> C.Appl (l@tl')
+          | _ as he' -> C.Appl (he'::tl')
+        end
+    | C.Appl _ -> assert false
+    | C.Const _ as t -> t
+    | C.MutInd _ as t -> t
+    | C.MutConstruct _ as t -> t
+    | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
+       C.MutCase (sp,cookingsno,i,substaux k what outt, substaux k what t,
+        List.map (substaux k what) pl)
+    | C.Fix (i,fl) ->
+       let len = List.length fl in
+       let substitutedfl =
+        List.map
+         (fun (name,i,ty,bo) ->
+           (name, i, substaux k what ty, substaux (k+len) (S.lift len what) bo))
+          fl
+       in
+        C.Fix (i, substitutedfl)
+    | C.CoFix (i,fl) ->
+       let len = List.length fl in
+       let substitutedfl =
+        List.map
+         (fun (name,ty,bo) ->
+           (name, substaux k what ty, substaux (k+len) (S.lift len what) bo))
+          fl
+       in
+        C.CoFix (i, substitutedfl)
+ in
+  substaux 1 what where
+;;
+
 (* Takes a well-typed term and fully reduces it. *)
 (*CSC: It does not perform reduction in a Case *)
 let reduce context =
@@ -145,7 +272,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 +333,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 +402,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 +490,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 +551,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 +610,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