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
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
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 =
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.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)
| 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)))
--- /dev/null
+(* 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
+;;
+
--- /dev/null
+(* 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
+
projects / helm.git / commitdiff