]> matita.cs.unibo.it Git - helm.git/commitdiff
added a duplicated implementation of replace lifting
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 6 Sep 2007 13:01:59 +0000 (13:01 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 6 Sep 2007 13:01:59 +0000 (13:01 +0000)
components/cic_unification/.depend
components/cic_unification/.depend.opt
components/cic_unification/Makefile
components/cic_unification/cicReplace.ml [new file with mode: 0644]
components/cic_unification/cicReplace.mli [new file with mode: 0644]

index 9fa71a619a828de5d7bde8e188e7cbadf907de9b..a7b23ceb4e8ba6ae3fdc2fa8352ce69acbde78b0 100644 (file)
@@ -8,7 +8,9 @@ coercGraph.cmo: termUtil.cmi cicMkImplicit.cmi coercGraph.cmi
 coercGraph.cmx: termUtil.cmx cicMkImplicit.cmx coercGraph.cmi 
 cicUnification.cmo: coercGraph.cmi cicMetaSubst.cmi cicUnification.cmi 
 cicUnification.cmx: coercGraph.cmx cicMetaSubst.cmx cicUnification.cmi 
-cicRefine.cmo: coercGraph.cmi cicUnification.cmi cicMkImplicit.cmi \
-    cicMetaSubst.cmi cicRefine.cmi 
-cicRefine.cmx: coercGraph.cmx cicUnification.cmx cicMkImplicit.cmx \
-    cicMetaSubst.cmx cicRefine.cmi 
+cicReplace.cmo: cicReplace.cmi 
+cicReplace.cmx: cicReplace.cmi 
+cicRefine.cmo: coercGraph.cmi cicUnification.cmi cicReplace.cmi \
+    cicMkImplicit.cmi cicMetaSubst.cmi cicRefine.cmi 
+cicRefine.cmx: coercGraph.cmx cicUnification.cmx cicReplace.cmx \
+    cicMkImplicit.cmx cicMetaSubst.cmx cicRefine.cmi 
index 9fa71a619a828de5d7bde8e188e7cbadf907de9b..a7b23ceb4e8ba6ae3fdc2fa8352ce69acbde78b0 100644 (file)
@@ -8,7 +8,9 @@ coercGraph.cmo: termUtil.cmi cicMkImplicit.cmi coercGraph.cmi
 coercGraph.cmx: termUtil.cmx cicMkImplicit.cmx coercGraph.cmi 
 cicUnification.cmo: coercGraph.cmi cicMetaSubst.cmi cicUnification.cmi 
 cicUnification.cmx: coercGraph.cmx cicMetaSubst.cmx cicUnification.cmi 
-cicRefine.cmo: coercGraph.cmi cicUnification.cmi cicMkImplicit.cmi \
-    cicMetaSubst.cmi cicRefine.cmi 
-cicRefine.cmx: coercGraph.cmx cicUnification.cmx cicMkImplicit.cmx \
-    cicMetaSubst.cmx cicRefine.cmi 
+cicReplace.cmo: cicReplace.cmi 
+cicReplace.cmx: cicReplace.cmi 
+cicRefine.cmo: coercGraph.cmi cicUnification.cmi cicReplace.cmi \
+    cicMkImplicit.cmi cicMetaSubst.cmi cicRefine.cmi 
+cicRefine.cmx: coercGraph.cmx cicUnification.cmx cicReplace.cmx \
+    cicMkImplicit.cmx cicMetaSubst.cmx cicRefine.cmi 
index d0c259b2799cd3692a7e7810ea6553dd649aa3a1..ad87356d14d939f506b8552fbf994f2cb0a3b06b 100644 (file)
@@ -7,6 +7,7 @@ INTERFACE_FILES = \
        termUtil.mli \
        coercGraph.mli \
        cicUnification.mli \
+       cicReplace.mli \
        cicRefine.mli
 IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
 EXTRA_OBJECTS_TO_INSTALL =
diff --git a/components/cic_unification/cicReplace.ml b/components/cic_unification/cicReplace.ml
new file mode 100644 (file)
index 0000000..7f53e1e
--- /dev/null
@@ -0,0 +1,129 @@
+(* Copyright (C) 2000, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* $Id: cicRefine.ml 7618 2007-09-05 10:07:39Z sacerdot $ *)
+
+exception WhatAndWithWhatDoNotHaveTheSameLength;;
+
+module C = Cic
+module S = CicSubstitution
+
+let replace_lifting ~equality ~context ~what ~with_what ~where =
+  let find_image ctx what t =
+   let rec find_image_aux =
+    function
+       [],[] -> raise Not_found
+     | what::tl1,with_what::tl2 ->
+        if equality ctx what t then with_what else find_image_aux (tl1,tl2)
+     | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
+   in
+    find_image_aux (what,with_what)
+  in
+  let add_ctx ctx n s = (Some (n, Cic.Decl s))::ctx in
+  let add_ctx1 ctx n s = (Some (n, Cic.Def (s,None)))::ctx in
+  let rec substaux k ctx what t =
+   try
+    S.lift (k-1) (find_image ctx what t)
+   with Not_found ->
+    match t with
+      C.Rel n as t -> t
+    | C.Var (uri,exp_named_subst) ->
+       let exp_named_subst' =
+        List.map (function (uri,t) -> uri,substaux k ctx what t) exp_named_subst
+       in
+        C.Var (uri,exp_named_subst')
+    | C.Meta (i, l) -> 
+       let l' =
+        List.map
+         (function
+             None -> None
+           | Some t -> Some (substaux k ctx 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 ctx what te, substaux k ctx what ty)
+    | C.Prod (n,s,t) ->
+       C.Prod
+        (n, substaux k ctx what s, substaux (k + 1) (add_ctx ctx n s) (List.map (S.lift 1) what) t)
+    | C.Lambda (n,s,t) ->
+       C.Lambda
+        (n, substaux k ctx what s, substaux (k + 1) (add_ctx ctx n s) (List.map (S.lift 1) what) t)
+    | C.LetIn (n,s,t) ->
+       C.LetIn
+        (n, substaux k ctx what s, substaux (k + 1) (add_ctx1 ctx n s) (List.map (S.lift 1) what) t)
+    | C.Appl (he::tl) ->
+       (* Invariant: no Appl applied to another Appl *)
+       let tl' = List.map (substaux k ctx what) tl in
+        begin
+         match substaux k ctx what he with
+            C.Appl l -> C.Appl (l@tl')
+          | _ as he' -> C.Appl (he'::tl')
+        end
+    | C.Appl _ -> assert false
+    | C.Const (uri,exp_named_subst) ->
+       let exp_named_subst' =
+        List.map (function (uri,t) -> uri,substaux k ctx what t) exp_named_subst
+       in
+       C.Const (uri,exp_named_subst')
+    | C.MutInd (uri,i,exp_named_subst) ->
+       let exp_named_subst' =
+        List.map (function (uri,t) -> uri,substaux k ctx what t) exp_named_subst
+       in
+        C.MutInd (uri,i,exp_named_subst')
+    | C.MutConstruct (uri,i,j,exp_named_subst) ->
+       let exp_named_subst' =
+        List.map (function (uri,t) -> uri,substaux k ctx what t) exp_named_subst
+       in
+        C.MutConstruct (uri,i,j,exp_named_subst')
+    | C.MutCase (sp,i,outt,t,pl) ->
+       C.MutCase (sp,i,substaux k ctx what outt, substaux k ctx what t,
+        List.map (substaux k ctx what) pl)
+    | C.Fix (i,fl) ->
+       let len = List.length fl in
+       let substitutedfl =
+        List.map
+         (fun (name,i,ty,bo) -> (* WRONG CTX *)
+           (name, i, substaux k ctx what ty,
+             substaux (k+len) ctx (List.map (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) -> (* WRONG CTX *)
+           (name, substaux k ctx what ty,
+             substaux (k+len) ctx (List.map (S.lift len) what) bo)
+         ) fl
+       in
+        C.CoFix (i, substitutedfl)
+ in
+  substaux 1 context what where
+;;
+
+
diff --git a/components/cic_unification/cicReplace.mli b/components/cic_unification/cicReplace.mli
new file mode 100644 (file)
index 0000000..c2f9aaf
--- /dev/null
@@ -0,0 +1,34 @@
+(* Copyright (C) 2000, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* $Id: cicRefine.ml 7618 2007-09-05 10:07:39Z sacerdot $ *)
+
+exception WhatAndWithWhatDoNotHaveTheSameLength
+
+
+val replace_lifting :
+  equality:(Cic.context -> Cic.term -> Cic.term -> bool) ->
+  context:Cic.context ->
+  what:Cic.term list -> with_what:Cic.term list -> where:Cic.term -> Cic.term