- bug fixed: some liftings were missing in the implementation of rewrite

- new feature: rewrite now works up to alpha-equivalence

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index d2725ff158fb49ee3445e1a615d7d4e0d0aa27d4..c46973e2cbeffab6cffc4a95224136ffb4603d07 100644 (file)
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -57,7 +57,8 @@ let rewrite_tac ~term:equality ~status:(proof,goal) =
      let t1' = CicSubstitution.lift 1 t1 in
      let gty'' =
       ProofEngineReduction.replace_lifting
-       ~equality:ProofEngineReduction.syntactic_equality
+       ~equality:
+        (ProofEngineReduction.syntactic_equality ~alpha_equivalence:true)
        ~what:t1' ~with_what:(C.Rel 1) ~where:gty'
      in
       C.Lambda (C.Name "dummy_for_rewrite", ty, gty'')

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 3c37b3ed268b67e2a57d62b00902cd8608b67d95..cbfe18e7360d497fdf2a65cc2fe4e5bde307b8cd 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -1466,7 +1466,7 @@ class rendering_window output proofw (label : GMisc.label) =
   GButton.button ~label:"Fourier"
    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
  let rewriteb =
-  GButton.button ~label:"Rewrite"
+  GButton.button ~label:"Rewrite ->"
    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
  let outputhtml =
   GHtml.xmhtml

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 0885f3037ffdcc1dfb9493ec1214f22f09b77022..64d68a37e53adc2aa635bd2b77fd31dea6c254c1 100644 (file)
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -224,7 +224,8 @@ let fold term =
    (*CSC: che si guadagni nulla in fatto di efficienza.    *) 
    let replace =
     ProofEngineReduction.replace
-     ~equality:(ProofEngineReduction.syntactic_equality)
+     ~equality:
+      (ProofEngineReduction.syntactic_equality ~alpha_equivalence:false)
      ~what:term' ~with_what:term
    in
     let ty' = replace ty in

diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml
index 442873cecb17dba0f22aa7f66049025132a800ae..bb724fc758d2736c40a7c199b60898501fe4308a 100644 (file)
--- a/helm/gTopLevel/proofEngineReduction.ml
+++ b/helm/gTopLevel/proofEngineReduction.ml
@@ -47,72 +47,65 @@ exception RelToHiddenHypothesis;;
 
 (* syntactic_equality up to cookingsno for uris *)
 (* (which is often syntactically irrilevant)    *)
-let rec syntactic_equality t t' =
+let syntactic_equality ~alpha_equivalence =
  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' ->
-       (try
-         List.fold_left2
-          (fun b t1 t2 -> b && syntactic_equality 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' &&
-        syntactic_equality outt outt' &&
-         syntactic_equality t t' &&
+  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 && syntactic_equality t1 t2) true pl pl'
+             (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 && name = name' && i = i' &&
-             syntactic_equality ty ty' &&
-              syntactic_equality 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 && name = name' &&
-             syntactic_equality ty ty' &&
-              syntactic_equality bo bo') true fl fl'
-        with
-         Invalid_argument _ -> false)
-    | _,_ -> 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 *)
@@ -162,33 +155,36 @@ let replace ~equality ~what ~with_what ~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 =
+ let rec substaux k what =
   let module C = Cic in
+  let module S = CicSubstitution in
    function
-(*CSC: Possibile bug: debbo liftare di k what? *)
-      t when (equality t what) -> CicSubstitution.lift (k-1) with_what
-    | C.Rel n as t -> t (*CSC: ??? BUG ? *)
+      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 t)
+           | 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 te, substaux k ty)
-    | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
-    | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
-    | C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) 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) tl in
+       let tl' = List.map (substaux k what) tl in
         begin
-         match substaux k he with
+         match substaux k what he with
             C.Appl l -> C.Appl (l@tl')
           | _ as he' -> C.Appl (he'::tl')
         end
@@ -197,13 +193,14 @@ let replace_lifting ~equality ~what ~with_what ~where =
     | 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 outt, substaux k t,
-        List.map (substaux k) 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 ty, substaux (k+len) bo))
+         (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)
@@ -211,12 +208,13 @@ let replace_lifting ~equality ~what ~with_what ~where =
        let len = List.length fl in
        let substitutedfl =
         List.map
-         (fun (name,ty,bo) -> (name, substaux k ty, substaux (k+len) bo))
+         (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 where
+  substaux 1 what where
 ;;
 
 (* Takes a well-typed term and fully reduces it. *)

diff --git a/helm/gTopLevel/proofEngineReduction.mli b/helm/gTopLevel/proofEngineReduction.mli
index e2d96f40b9d64e6a25ed914c6d031ea9600cfaf3..aa0a3a6489394056178b20314c04162bc816efbe 100644 (file)
--- a/helm/gTopLevel/proofEngineReduction.mli
+++ b/helm/gTopLevel/proofEngineReduction.mli
@@ -34,12 +34,12 @@ exception RelToHiddenHypothesis
 exception WrongShape
 exception AlreadySimplified
 
-val syntactic_equality : Cic.term -> Cic.term -> bool
+val syntactic_equality : alpha_equivalence:bool -> Cic.term -> Cic.term -> bool
 val replace :
   equality:(Cic.term -> 'a -> bool) ->
   what:'a -> with_what:Cic.term -> where:Cic.term -> Cic.term
 val replace_lifting :
-  equality:(Cic.term -> 'a -> bool) ->
-  what:'a -> with_what:Cic.term -> where:Cic.term -> Cic.term
+  equality:(Cic.term -> Cic.term -> bool) ->
+  what:Cic.term -> with_what:Cic.term -> where:Cic.term -> Cic.term
 val reduce : Cic.context -> Cic.term -> Cic.term
 val simpl : Cic.context -> Cic.term -> Cic.term