From: Enrico Tassi Date: Wed, 13 Feb 2008 15:35:43 +0000 (+0000) Subject: substituion and lifting implemented X-Git-Tag: make_still_working~5609 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cf3c2f9d76c0483afc91ad89c0ae2517081ce912;p=helm.git substituion and lifting implemented --- diff --git a/helm/software/components/ng_kernel/.depend b/helm/software/components/ng_kernel/.depend index 5fb3278ed..801551b32 100644 --- a/helm/software/components/ng_kernel/.depend +++ b/helm/software/components/ng_kernel/.depend @@ -1,9 +1,12 @@ -nCicEnvironment.cmi: nReference.cmi nCic.cmo +nCicEnvironment.cmi: nUri.cmi nCic.cmo nCicTypeChecker.cmi: nCic.cmo nReference.cmi: nUri.cmi oCic2NCic.cmi: nCic.cmo -nCicEnvironment.cmo: oCic2NCic.cmi nReference.cmi nCicEnvironment.cmi -nCicEnvironment.cmx: oCic2NCic.cmx nReference.cmx nCicEnvironment.cmi +nCicSubstitution.cmi: nCic.cmo +nCic.cmo: nUri.cmi nReference.cmi +nCic.cmx: nUri.cmx nReference.cmx +nCicEnvironment.cmo: oCic2NCic.cmi nUri.cmi nCicEnvironment.cmi +nCicEnvironment.cmx: oCic2NCic.cmx nUri.cmx nCicEnvironment.cmi nCicTypeChecker.cmo: nCicTypeChecker.cmi nCicTypeChecker.cmx: nCicTypeChecker.cmi nReference.cmo: nUri.cmi nReference.cmi @@ -14,3 +17,5 @@ oCic2NCic.cmo: oCic2NCic.cmi oCic2NCic.cmx: oCic2NCic.cmi nUri.cmo: nUri.cmi nUri.cmx: nUri.cmi +nCicSubstitution.cmo: nCic.cmo nCicSubstitution.cmi +nCicSubstitution.cmx: nCic.cmx nCicSubstitution.cmi diff --git a/helm/software/components/ng_kernel/Makefile b/helm/software/components/ng_kernel/Makefile index 65c0ab906..3604530df 100644 --- a/helm/software/components/ng_kernel/Makefile +++ b/helm/software/components/ng_kernel/Makefile @@ -2,11 +2,12 @@ PACKAGE = ng_kernel PREDICATES = INTERFACE_FILES = \ - nCicEnvironment.mli nCicTypeChecker.mli nReference.mli oCicTypeChecker.mli oCic2NCic.mli nUri.mli + nCicEnvironment.mli nCicTypeChecker.mli nReference.mli oCicTypeChecker.mli oCic2NCic.mli nUri.mli nCicSubstitution.mli IMPLEMENTATION_FILES = \ nCic.ml $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = EXTRA_OBJECTS_TO_CLEAN = +OCAMLOPTIONS += -w Ae include ../../Makefile.defs include ../Makefile.common diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml index 19a8a227b..961c84cfa 100644 --- a/helm/software/components/ng_kernel/nCic.ml +++ b/helm/software/components/ng_kernel/nCic.ml @@ -29,8 +29,10 @@ type sort = Prop | Set | Type of int | CProp type implicit_annotation = [ `Closed | `Type | `Hole | `Term ] -type local_context = int * (term list) option (* shift (0 -> no shift), - subst (None means id) *) +type lc_kind = Irl of int | Ctx of term list + +and local_context = int * lc_kind (* shift (0 -> no shift), + subst (None means id) *) and term = | Rel of int (* DeBruijn index, 1 based *) | Meta of int * local_context diff --git a/helm/software/components/ng_kernel/nCicSubstitution.ml b/helm/software/components/ng_kernel/nCicSubstitution.ml new file mode 100644 index 000000000..48e96709c --- /dev/null +++ b/helm/software/components/ng_kernel/nCicSubstitution.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$ *) + +let debug_print = fun _ -> ();; + +(* to be moved in cic util *) +let expand_local_context = function + | NCic.Irl len -> + let rec aux acc = function + | 0 -> acc + | n -> aux (NCic.Rel n::acc) (n-1) + in + aux [] len + | NCic.Ctx lctx -> lctx +;; + +let lift_from k n = + let rec liftaux k = function + | NCic.Const _ + | NCic.Sort _ as t -> t + | NCic.Rel m -> + if m < k then NCic.Rel m + else NCic.Rel (m + n) + | NCic.Meta (i,(m,l)) when k <= m -> NCic.Meta (i,(m+n,l)) + | NCic.Meta (_,(m,NCic.Irl l)) as t when k > l + m -> t + | NCic.Meta (i,(m,l)) -> + let lctx = expand_local_context l in + NCic.Meta (i, (m, NCic.Ctx (List.map (liftaux (k-m)) lctx))) + | NCic.Implicit _ -> (* was the identity *) assert false + | NCic.Prod (n,s,t) -> NCic.Prod (n, liftaux k s, liftaux (k+1) t) + | NCic.Lambda (n,s,t) -> NCic.Lambda (n, liftaux k s, liftaux (k+1) t) + | NCic.LetIn (n,ty,te,t) -> + NCic.LetIn (n, liftaux k ty, liftaux k te, liftaux (k+1) t) + | NCic.Appl l -> NCic.Appl (List.map (liftaux k) l) + | NCic.Match (r,outty,t,pl) -> + NCic.Match (r,liftaux k outty,liftaux k t, List.map (liftaux k) pl) + in + liftaux k +;; + +let lift ?(from=1) n t = + if n = 0 then t + else lift_from from n t +;; + +(* subst t1 t2 *) +(* substitutes [t1] for [Rel 1] in [t2] *) +(* if avoid_beta_redexes is true (default: false) no new beta redexes *) +(* are generated. WARNING: the substitution can diverge when t2 is not *) +(* well typed and avoid_beta_redexes is true. *) +let rec psubst ?(avoid_beta_redexes=false) delift lift_args args = + let nargs = List.length args in + let rec substaux k = function + | NCic.Rel n as t -> + (match n with + | n when n >= (k+nargs) -> if delift then NCic.Rel (n - nargs) else t + | n when n < k -> t + | n (* k <= n < k+nargs *) -> + (try lift (k+lift_args) (List.nth args (n-k)) + with Failure _ -> assert false)) + | NCic.Meta (_,(m,_)) as t when m >= k + nargs - 1 -> t + | NCic.Meta (_,(m,NCic.Irl l)) as t when k > l + m -> t + | NCic.Meta (i,(m,l)) -> + let lctx = expand_local_context l in + (* 1-nargs < k-m, when <= 0 is still reasonable because we will + * substitute args[ k-m ... k-m+nargs-1 > 0 ] *) + NCic.Meta (i,(m, NCic.Ctx (List.map (substaux (k-m)) lctx))) + | NCic.Sort _ as t -> t + | NCic.Implicit _ -> assert false (* was identity *) + | NCic.Prod (n,s,t) -> NCic.Prod (n, substaux k s, substaux (k + 1) t) + | NCic.Lambda (n,s,t) -> NCic.Lambda (n, substaux k s, substaux (k + 1) t) + | NCic.LetIn (n,ty,te,t) -> + NCic.LetIn (n, substaux k ty, substaux k te, substaux (k + 1) t) + | NCic.Appl (he::tl) -> + (* Invariant: no Appl applied to another Appl *) + let rec avoid he = function + | [] -> he + | arg::tl as args-> + (match he with + | NCic.Appl l -> NCic.Appl (l@args) + | NCic.Lambda (_,_,bo) when avoid_beta_redexes -> + avoid (psubst ~avoid_beta_redexes true 0 [arg] bo) tl + | _ as he -> NCic.Appl (he::args)) + in + let tl = List.map (substaux k) tl in + avoid (substaux k he) tl + | NCic.Appl _ -> assert false + | NCic.Const _ as t -> t + | NCic.Match (r,outt,t,pl) -> + NCic.Match (r,substaux k outt, substaux k t, List.map (substaux k) pl) + in + substaux 1 +;; + +let subst ?avoid_beta_redexes arg = psubst ?avoid_beta_redexes true 0 [arg];; + +(* subst_meta (n, Some [t_1 ; ... ; t_n]) t *) +(* returns the term [t] where [Rel i] is substituted with [t_i] lifted by n *) +(* [t_i] is lifted as usual when it crosses an abstraction *) +(* subst_meta (n, Non) t -> lift n t *) +let subst_meta = function + | m, NCic.Irl _ + | m, NCic.Ctx [] -> lift m + | m, NCic.Ctx l -> psubst false m l +;; diff --git a/helm/software/components/ng_kernel/nCicSubstitution.mli b/helm/software/components/ng_kernel/nCicSubstitution.mli new file mode 100644 index 000000000..30a6c7451 --- /dev/null +++ b/helm/software/components/ng_kernel/nCicSubstitution.mli @@ -0,0 +1,45 @@ +(* 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/. + *) + +(* lift n t *) +(* lifts [t] of [n] *) +(* [from] default 1, lifts only indexes >= [from] *) +(* NOTE: the opposite function (delift_rels) is defined in CicMetaSubst *) +(* since it needs to restrict the metavariables in case of failure *) +val lift : ?from:int -> int -> NCic.term -> NCic.term + +(* subst t1 t2 *) +(* substitutes [t1] for [Rel 1] in [t2] *) +(* if avoid_beta_redexes is true (default: false) no new beta redexes *) +(* are generated. WARNING: the substitution can diverge when t2 is not *) +(* well typed and avoid_beta_redexes is true. *) +val subst : ?avoid_beta_redexes:bool -> NCic.term -> NCic.term -> NCic.term + +(* subst_meta (n, Ctx [t_1 ; ... ; t_n]) t *) +(* returns the term [t] where [Rel i] is substituted with [t_i] lifted by n *) +(* [t_i] is lifted as usual when it crosses an abstraction *) +(* subst_meta (n, Irl _) t -> lift n t *) +val subst_meta : NCic.local_context -> NCic.term -> NCic.term +