From b7387e01fb1ce2745a6df6ffc254dba7d13d35ac Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 13 Feb 2008 15:42:28 +0000 Subject: [PATCH] reorganization of sources --- helm/software/components/ng_kernel/.depend | 7 +++- helm/software/components/ng_kernel/Makefile | 2 +- .../components/ng_kernel/nCicSubstitution.ml | 15 +------- .../components/ng_kernel/nCicUtils.ml | 37 +++++++++++++++++++ .../components/ng_kernel/nCicUtils.mli | 29 +++++++++++++++ 5 files changed, 74 insertions(+), 16 deletions(-) create mode 100644 helm/software/components/ng_kernel/nCicUtils.ml create mode 100644 helm/software/components/ng_kernel/nCicUtils.mli diff --git a/helm/software/components/ng_kernel/.depend b/helm/software/components/ng_kernel/.depend index 801551b32..96e415f0c 100644 --- a/helm/software/components/ng_kernel/.depend +++ b/helm/software/components/ng_kernel/.depend @@ -3,6 +3,7 @@ nCicTypeChecker.cmi: nCic.cmo nReference.cmi: nUri.cmi oCic2NCic.cmi: nCic.cmo nCicSubstitution.cmi: nCic.cmo +nCicUtils.cmi: nCic.cmo nCic.cmo: nUri.cmi nReference.cmi nCic.cmx: nUri.cmx nReference.cmx nCicEnvironment.cmo: oCic2NCic.cmi nUri.cmi nCicEnvironment.cmi @@ -17,5 +18,7 @@ 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 +nCicSubstitution.cmo: nCicUtils.cmi nCic.cmo nCicSubstitution.cmi +nCicSubstitution.cmx: nCicUtils.cmx nCic.cmx nCicSubstitution.cmi +nCicUtils.cmo: nCic.cmo nCicUtils.cmi +nCicUtils.cmx: nCic.cmx nCicUtils.cmi diff --git a/helm/software/components/ng_kernel/Makefile b/helm/software/components/ng_kernel/Makefile index 3604530df..69f294925 100644 --- a/helm/software/components/ng_kernel/Makefile +++ b/helm/software/components/ng_kernel/Makefile @@ -2,7 +2,7 @@ PACKAGE = ng_kernel PREDICATES = INTERFACE_FILES = \ - nCicEnvironment.mli nCicTypeChecker.mli nReference.mli oCicTypeChecker.mli oCic2NCic.mli nUri.mli nCicSubstitution.mli + nCicEnvironment.mli nCicTypeChecker.mli nReference.mli oCicTypeChecker.mli oCic2NCic.mli nUri.mli nCicSubstitution.mli nCicUtils.mli IMPLEMENTATION_FILES = \ nCic.ml $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = diff --git a/helm/software/components/ng_kernel/nCicSubstitution.ml b/helm/software/components/ng_kernel/nCicSubstitution.ml index 48e96709c..67bada949 100644 --- a/helm/software/components/ng_kernel/nCicSubstitution.ml +++ b/helm/software/components/ng_kernel/nCicSubstitution.ml @@ -27,17 +27,6 @@ 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 _ @@ -48,7 +37,7 @@ let lift_from k 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 + let lctx = NCicUtils.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) @@ -85,7 +74,7 @@ let rec psubst ?(avoid_beta_redexes=false) delift lift_args args = | 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 + let lctx = NCicUtils.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))) diff --git a/helm/software/components/ng_kernel/nCicUtils.ml b/helm/software/components/ng_kernel/nCicUtils.ml new file mode 100644 index 000000000..2a9aaf0a5 --- /dev/null +++ b/helm/software/components/ng_kernel/nCicUtils.ml @@ -0,0 +1,37 @@ +(* 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: nCicSubstitution.ml 8135 2008-02-13 15:35:43Z tassi $ *) + +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 +;; + diff --git a/helm/software/components/ng_kernel/nCicUtils.mli b/helm/software/components/ng_kernel/nCicUtils.mli new file mode 100644 index 000000000..45c444ac4 --- /dev/null +++ b/helm/software/components/ng_kernel/nCicUtils.mli @@ -0,0 +1,29 @@ +(* 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: nCicSubstitution.ml 8135 2008-02-13 15:35:43Z tassi $ *) + +val expand_local_context : NCic.lc_kind -> NCic.term list + -- 2.39.2