From 6ca04b596642894449012de8ec6d2f3f784f5868 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 6 Sep 2007 13:01:59 +0000 Subject: [PATCH] added a duplicated implementation of replace lifting --- .../components/cic_unification/.depend | 10 +- .../components/cic_unification/.depend.opt | 10 +- .../components/cic_unification/Makefile | 1 + .../components/cic_unification/cicReplace.ml | 129 ++++++++++++++++++ .../components/cic_unification/cicReplace.mli | 34 +++++ 5 files changed, 176 insertions(+), 8 deletions(-) create mode 100644 helm/software/components/cic_unification/cicReplace.ml create mode 100644 helm/software/components/cic_unification/cicReplace.mli diff --git a/helm/software/components/cic_unification/.depend b/helm/software/components/cic_unification/.depend index 9fa71a619..a7b23ceb4 100644 --- a/helm/software/components/cic_unification/.depend +++ b/helm/software/components/cic_unification/.depend @@ -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 diff --git a/helm/software/components/cic_unification/.depend.opt b/helm/software/components/cic_unification/.depend.opt index 9fa71a619..a7b23ceb4 100644 --- a/helm/software/components/cic_unification/.depend.opt +++ b/helm/software/components/cic_unification/.depend.opt @@ -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 diff --git a/helm/software/components/cic_unification/Makefile b/helm/software/components/cic_unification/Makefile index d0c259b27..ad87356d1 100644 --- a/helm/software/components/cic_unification/Makefile +++ b/helm/software/components/cic_unification/Makefile @@ -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/helm/software/components/cic_unification/cicReplace.ml b/helm/software/components/cic_unification/cicReplace.ml new file mode 100644 index 000000000..7f53e1ee5 --- /dev/null +++ b/helm/software/components/cic_unification/cicReplace.ml @@ -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/helm/software/components/cic_unification/cicReplace.mli b/helm/software/components/cic_unification/cicReplace.mli new file mode 100644 index 000000000..c2f9aaff3 --- /dev/null +++ b/helm/software/components/cic_unification/cicReplace.mli @@ -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 -- 2.39.2