From 0ec61cd3d3fe2bf43b75fc94800af0c23cfa8c3b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 18 Feb 2008 16:31:32 +0000 Subject: [PATCH] some bits of reduction, reusing psubst --- helm/software/components/ng_kernel/.depend | 8 +- helm/software/components/ng_kernel/Makefile | 2 +- helm/software/components/ng_kernel/nCic.ml | 5 +- .../components/ng_kernel/nCicEnvironment.ml | 31 + .../components/ng_kernel/nCicEnvironment.mli | 16 +- .../components/ng_kernel/nCicReduction.ml | 964 ++++++++++++++++++ .../components/ng_kernel/nCicReduction.mli | 46 + .../components/ng_kernel/nCicSubstitution.ml | 22 +- .../components/ng_kernel/nCicSubstitution.mli | 14 + .../components/ng_kernel/nCicUtils.ml | 7 + .../components/ng_kernel/nCicUtils.mli | 4 + 11 files changed, 1107 insertions(+), 12 deletions(-) create mode 100644 helm/software/components/ng_kernel/nCicReduction.ml create mode 100644 helm/software/components/ng_kernel/nCicReduction.mli diff --git a/helm/software/components/ng_kernel/.depend b/helm/software/components/ng_kernel/.depend index 96e415f0c..c56514948 100644 --- a/helm/software/components/ng_kernel/.depend +++ b/helm/software/components/ng_kernel/.depend @@ -14,11 +14,15 @@ nReference.cmo: nUri.cmi nReference.cmi nReference.cmx: nUri.cmx nReference.cmi oCicTypeChecker.cmo: oCic2NCic.cmi nCicTypeChecker.cmi oCicTypeChecker.cmi oCicTypeChecker.cmx: oCic2NCic.cmx nCicTypeChecker.cmx oCicTypeChecker.cmi -oCic2NCic.cmo: oCic2NCic.cmi -oCic2NCic.cmx: oCic2NCic.cmi +oCic2NCic.cmo: nUri.cmi nCic.cmo oCic2NCic.cmi +oCic2NCic.cmx: nUri.cmx nCic.cmx oCic2NCic.cmi nUri.cmo: nUri.cmi nUri.cmx: nUri.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 +nCicReduction.cmo: nReference.cmi nCicSubstitution.cmi nCicEnvironment.cmi \ + nCic.cmo nCicReduction.cmi +nCicReduction.cmx: nReference.cmx nCicSubstitution.cmx nCicEnvironment.cmx \ + nCic.cmx nCicReduction.cmi diff --git a/helm/software/components/ng_kernel/Makefile b/helm/software/components/ng_kernel/Makefile index 69f294925..3bc7f1a19 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 nCicUtils.mli + nCicEnvironment.mli nCicTypeChecker.mli nReference.mli oCicTypeChecker.mli oCic2NCic.mli nUri.mli nCicSubstitution.mli nCicUtils.mli nCicReduction.mli IMPLEMENTATION_FILES = \ nCic.ml $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml index 639bab2b6..08726422e 100644 --- a/helm/software/components/ng_kernel/nCic.ml +++ b/helm/software/components/ng_kernel/nCic.ml @@ -63,7 +63,9 @@ type conjecture = int * string option * context * term type metasenv = conjecture list -type substitution = (int * (string option * context * term * term)) list +type subst_entry = string option * context * term * term + +type substitution = (int * subst_entry) list (******************************** OBJECTS **********************************) @@ -109,4 +111,5 @@ type obj_kind = | Inductive of bool * int * inductiveType list * i_attr (* (co)inductive, leftno, types *) + (* the int must be 0 if the object has no body *) type obj = NUri.uri * int * metasenv * substitution * obj_kind diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml index 37cebe647..e10aba973 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.ml +++ b/helm/software/components/ng_kernel/nCicEnvironment.ml @@ -11,3 +11,34 @@ let get_checked_obj u = NUri.UriHash.add cache u no; no ;; + +let get_checked_def = function + | NReference.Ref (_, uri, NReference.Def) -> + (match get_checked_obj uri with + | _,height,_,_, NCic.Constant (rlv,name,Some bo,ty,att) -> + rlv,name,bo,ty,att,height + | _,_,_,_, NCic.Constant (_,_,None,_,_) -> + prerr_endline "get_checked_def on an axiom"; assert false + | _ -> prerr_endline "get_checked_def on a non def 2"; assert false) + | _ -> prerr_endline "get_checked_def on a non def"; assert false +;; + +let get_checked_fix_or_cofix b = function + | NReference.Ref (_, uri, NReference.Fix (fixno,_)) -> + (match get_checked_obj uri with + | _,height,_,_, NCic.Fixpoint (is_fix,funcs,att) when is_fix = b -> + let rlv, name, _, ty, bo = List.nth funcs fixno in + rlv, name, bo, ty, att, height + | _ ->prerr_endline "get_checked_(co)fix on a non (co)fix 2";assert false) + | _ -> prerr_endline "get_checked_(co)fix on a non (co)fix"; assert false +;; +let get_checked_fix r = get_checked_fix_or_cofix true r;; +let get_checked_cofix r = get_checked_fix_or_cofix false r;; + +let get_indty_leftno = function + | NReference.Ref (_, uri, NReference.Ind _) + | NReference.Ref (_, uri, NReference.Con _) -> + (match get_checked_obj uri with + | _,_,_,_, NCic.Inductive (_,left,_,_) -> left + | _ ->prerr_endline "get_indty_leftno called on a non ind 2";assert false) + | _ -> prerr_endline "get_indty_leftno called on a non indty";assert false diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli index 765198439..225a4aea2 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.mli +++ b/helm/software/components/ng_kernel/nCicEnvironment.mli @@ -26,6 +26,20 @@ (* NG: minimal wrapper on the old cicEnvironment, should provide only the * functions strictly necessary to the typechecking algorithm *) -val get_checked_obj : NUri.uri -> NCic.obj +val get_checked_obj: NUri.uri -> NCic.obj + +val get_checked_def: + NReference.reference -> + NCic.relevance * string * NCic.term * NCic.term * NCic.c_attr * int + +val get_checked_fix: + NReference.reference -> + NCic.relevance * string * NCic.term * NCic.term * NCic.f_attr * int + +val get_checked_cofix: + NReference.reference -> + NCic.relevance * string * NCic.term * NCic.term * NCic.f_attr * int + +val get_indty_leftno: NReference.reference -> int (* EOF *) diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml new file mode 100644 index 000000000..37472875e --- /dev/null +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -0,0 +1,964 @@ +(* 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$ *) + +(* TODO unify exceptions *) + +exception WrongUriToInductiveDefinition;; +exception Impossible of int;; +exception ReferenceToConstant;; +exception ReferenceToVariable;; +exception ReferenceToCurrentProof;; +exception ReferenceToInductiveDefinition;; + +let debug = false +let profile = false +let debug_print s = if debug then prerr_endline (Lazy.force s) + +let fdebug = ref 1;; +let debug t env s = + let rec debug_aux t i = + let module C = Cic in + let module U = UriManager in + CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i + in + if !fdebug = 0 then + debug_print (lazy (s ^ "\n" ^ List.fold_right debug_aux (t::env) "")) +;; + +module type Strategy = + sig + type stack_term + type env_term + type config = int * env_term list * NCic.term * stack_term list + val to_env : + reduce: (config -> config) -> + unwind: (config -> NCic.term) -> + config -> env_term + val from_stack : stack_term -> config + val from_stack_list_for_unwind : + unwind: (config -> NCic.term) -> + stack_term list -> NCic.term list + val from_env : env_term -> config + val from_env_for_unwind : + unwind: (config -> NCic.term) -> + env_term -> NCic.term + val stack_to_env : + reduce: (config -> config) -> + unwind: (config -> NCic.term) -> + stack_term -> env_term + val compute_to_env : + reduce: (config -> config) -> + unwind: (config -> NCic.term) -> + int -> env_term list -> + NCic.term -> env_term + val compute_to_stack : + reduce: (config -> config) -> + unwind: (config -> NCic.term) -> + config -> stack_term + end +;; + +(* +module CallByValueByNameForUnwind = + struct + type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list + and stack_term = config + and env_term = config * config (* cbv, cbn *) + and ens_term = config * config (* cbv, cbn *) + + let to_env c = c,c + let to_ens c = c,c + let from_stack config = config + let from_stack_list_for_unwind ~unwind l = List.map unwind l + let from_env (c,_) = c + let from_ens (c,_) = c + let from_env_for_unwind ~unwind (_,c) = unwind c + let from_ens_for_unwind ~unwind (_,c) = unwind c + let stack_to_env ~reduce ~unwind config = reduce config, (0,[],[],unwind config,[]) + let compute_to_env ~reduce ~unwind k e ens t = (k,e,ens,t,[]), (k,e,ens,t,[]) + let compute_to_stack ~reduce ~unwind config = config + end +;; +*) + +module CallByValueByNameForUnwind' = + struct + type config = int * env_term list * NCic.term * stack_term list + and stack_term = config lazy_t * NCic.term lazy_t (* cbv, cbn *) + and env_term = config lazy_t * NCic.term lazy_t (* cbv, cbn *) + let to_env ~reduce ~unwind c = lazy (reduce c),lazy (unwind c) + let from_stack (c,_) = Lazy.force c + let from_stack_list_for_unwind ~unwind:_ l = + List.map (function (_,c) -> Lazy.force c) l + let from_env (c,_) = Lazy.force c + let from_env_for_unwind ~unwind:_ (_,c) = Lazy.force c + let stack_to_env ~reduce:_ ~unwind:_ config = config + let compute_to_env ~reduce ~unwind k e t = + lazy (reduce (k,e,t,[])), lazy (unwind (k,e,t,[])) + let compute_to_stack ~reduce ~unwind config = + lazy (reduce config), lazy (unwind config) + end +;; + + +(* Old Machine +module CallByNameStrategy = + struct + type stack_term = Cic.term + type env_term = Cic.term + type ens_term = Cic.term + type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list + let to_env v = v + let to_ens v = v + let from_stack ~unwind v = v + let from_stack_list ~unwind l = l + let from_env v = v + let from_ens v = v + let from_env_for_unwind ~unwind v = v + let from_ens_for_unwind ~unwind v = v + let stack_to_env ~reduce ~unwind v = v + let compute_to_stack ~reduce ~unwind k e ens t = unwind k e ens t + let compute_to_env ~reduce ~unwind k e ens t = unwind k e ens t + end +;; + +module CallByNameStrategy = + struct + type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list + and stack_term = config + and env_term = config + and ens_term = config + + let to_env c = c + let to_ens c = c + let from_stack config = config + let from_stack_list_for_unwind ~unwind l = List.map unwind l + let from_env c = c + let from_ens c = c + let from_env_for_unwind ~unwind c = unwind c + let from_ens_for_unwind ~unwind c = unwind c + let stack_to_env ~reduce ~unwind config = 0,[],[],unwind config,[] + let compute_to_env ~reduce ~unwind k e ens t = k,e,ens,t,[] + let compute_to_stack ~reduce ~unwind config = config + end +;; + +module CallByValueStrategy = + struct + type stack_term = Cic.term + type env_term = Cic.term + type ens_term = Cic.term + type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list + let to_env v = v + let to_ens v = v + let from_stack ~unwind v = v + let from_stack_list ~unwind l = l + let from_env v = v + let from_ens v = v + let from_env_for_unwind ~unwind v = v + let from_ens_for_unwind ~unwind v = v + let stack_to_env ~reduce ~unwind v = v + let compute_to_stack ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[]) + let compute_to_env ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[]) + end +;; + +module CallByValueStrategyByNameOnConstants = + struct + type stack_term = Cic.term + type env_term = Cic.term + type ens_term = Cic.term + type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list + let to_env v = v + let to_ens v = v + let from_stack ~unwind v = v + let from_stack_list ~unwind l = l + let from_env v = v + let from_ens v = v + let from_env_for_unwind ~unwind v = v + let from_ens_for_unwind ~unwind v = v + let stack_to_env ~reduce ~unwind v = v + let compute_to_stack ~reduce ~unwind k e ens = + function + Cic.Const _ as t -> unwind k e ens t + | t -> reduce (k,e,ens,t,[]) + let compute_to_env ~reduce ~unwind k e ens = + function + Cic.Const _ as t -> unwind k e ens t + | t -> reduce (k,e,ens,t,[]) + end +;; + +module LazyCallByValueStrategy = + struct + type stack_term = Cic.term lazy_t + type env_term = Cic.term lazy_t + type ens_term = Cic.term lazy_t + type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list + let to_env v = lazy v + let to_ens v = lazy v + let from_stack ~unwind v = Lazy.force v + let from_stack_list ~unwind l = List.map (from_stack ~unwind) l + let from_env v = Lazy.force v + let from_ens v = Lazy.force v + let from_env_for_unwind ~unwind v = Lazy.force v + let from_ens_for_unwind ~unwind v = Lazy.force v + let stack_to_env ~reduce ~unwind v = v + let compute_to_stack ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[])) + let compute_to_env ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[])) + end +;; + +module LazyCallByValueStrategyByNameOnConstants = + struct + type stack_term = Cic.term lazy_t + type env_term = Cic.term lazy_t + type ens_term = Cic.term lazy_t + type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list + let to_env v = lazy v + let to_ens v = lazy v + let from_stack ~unwind v = Lazy.force v + let from_stack_list ~unwind l = List.map (from_stack ~unwind) l + let from_env v = Lazy.force v + let from_ens v = Lazy.force v + let from_env_for_unwind ~unwind v = Lazy.force v + let from_ens_for_unwind ~unwind v = Lazy.force v + let stack_to_env ~reduce ~unwind v = v + let compute_to_stack ~reduce ~unwind k e ens t = + lazy ( + match t with + Cic.Const _ as t -> unwind k e ens t + | t -> reduce (k,e,ens,t,[])) + let compute_to_env ~reduce ~unwind k e ens t = + lazy ( + match t with + Cic.Const _ as t -> unwind k e ens t + | t -> reduce (k,e,ens,t,[])) + end +;; + +module LazyCallByNameStrategy = + struct + type stack_term = Cic.term lazy_t + type env_term = Cic.term lazy_t + type ens_term = Cic.term lazy_t + type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list + let to_env v = lazy v + let to_ens v = lazy v + let from_stack ~unwind v = Lazy.force v + let from_stack_list ~unwind l = List.map (from_stack ~unwind) l + let from_env v = Lazy.force v + let from_ens v = Lazy.force v + let from_env_for_unwind ~unwind v = Lazy.force v + let from_ens_for_unwind ~unwind v = Lazy.force v + let stack_to_env ~reduce ~unwind v = v + let compute_to_stack ~reduce ~unwind k e ens t = lazy (unwind k e ens t) + let compute_to_env ~reduce ~unwind k e ens t = lazy (unwind k e ens t) + end +;; + +module + LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns += + struct + type stack_term = reduce:bool -> Cic.term + type env_term = reduce:bool -> Cic.term + type ens_term = reduce:bool -> Cic.term + type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list + let to_env v = + let value = lazy v in + fun ~reduce -> Lazy.force value + let to_ens v = + let value = lazy v in + fun ~reduce -> Lazy.force value + let from_stack ~unwind v = (v ~reduce:false) + let from_stack_list ~unwind l = List.map (from_stack ~unwind) l + let from_env v = (v ~reduce:true) + let from_ens v = (v ~reduce:true) + let from_env_for_unwind ~unwind v = (v ~reduce:true) + let from_ens_for_unwind ~unwind v = (v ~reduce:true) + let stack_to_env ~reduce ~unwind v = v + let compute_to_stack ~reduce ~unwind k e ens t = + let svalue = + lazy ( + match t with + Cic.Const _ as t -> unwind k e ens t + | t -> reduce (k,e,ens,t,[]) + ) in + let lvalue = + lazy (unwind k e ens t) + in + fun ~reduce -> + if reduce then Lazy.force svalue else Lazy.force lvalue + let compute_to_env ~reduce ~unwind k e ens t = + let svalue = + lazy ( + match t with + Cic.Const _ as t -> unwind k e ens t + | t -> reduce (k,e,ens,t,[]) + ) in + let lvalue = + lazy (unwind k e ens t) + in + fun ~reduce -> + if reduce then Lazy.force svalue else Lazy.force lvalue + end +;; + +module ClosuresOnStackByValueFromEnvOrEnsStrategy = + struct + type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list + and stack_term = config + and env_term = config + and ens_term = config + + let to_env config = config + let to_ens config = config + let from_stack config = config + let from_stack_list_for_unwind ~unwind l = List.map unwind l + let from_env v = v + let from_ens v = v + let from_env_for_unwind ~unwind config = unwind config + let from_ens_for_unwind ~unwind config = unwind config + let stack_to_env ~reduce ~unwind config = reduce config + let compute_to_env ~reduce ~unwind k e ens t = (k,e,ens,t,[]) + let compute_to_stack ~reduce ~unwind config = config + end +;; + +module ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy = + struct + type stack_term = + int * Cic.term list * Cic.term Cic.explicit_named_substitution * Cic.term + type env_term = Cic.term + type ens_term = Cic.term + type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list + let to_env v = v + let to_ens v = v + let from_stack ~unwind (k,e,ens,t) = unwind k e ens t + let from_stack_list ~unwind l = List.map (from_stack ~unwind) l + let from_env v = v + let from_ens v = v + let from_env_for_unwind ~unwind v = v + let from_ens_for_unwind ~unwind v = v + let stack_to_env ~reduce ~unwind (k,e,ens,t) = + match t with + Cic.Const _ as t -> unwind k e ens t + | t -> reduce (k,e,ens,t,[]) + let compute_to_env ~reduce ~unwind k e ens t = + unwind k e ens t + let compute_to_stack ~reduce ~unwind k e ens t = (k,e,ens,t) + end +;; + +*) + +module Reduction(RS : Strategy) = + struct + type env = RS.env_term list + type stack = RS.stack_term list + type config = int * env * NCic.term * stack + + let rec unwind (k,e,t,s) = + let t = + if k = 0 then t + else + NCicSubstitution.psubst ~avoid_beta_redexes:true + true 0 (RS.from_env_for_unwind ~unwind) e t + in + if s = [] then t + else NCic.Appl(t::(RS.from_stack_list_for_unwind ~unwind s)) + ;; + + let list_nth l n = try List.nth l n with Failure _ -> assert false;; + let rec replace i s t = + match i,s with + | 0,_::tl -> t::tl + | n,he::tl -> he::(replace (n - 1) tl t) + | _,_ -> assert false + ;; + + let rec reduce ~delta ?(subst = []) context : config -> config = + let rec aux = function + | k, e, NCic.Rel n, s when n <= k -> + let k',e',t',s' = RS.from_env (list_nth e (n-1)) in + aux (k',e',t',s'@s) + | k, _, NCic.Rel n, s as config (* when n > k *) -> + (match List.nth context (n - 1 - k) with + | (_,NCic.Decl _) -> config + | (_,NCic.Def (x,_)) -> aux (0,[],NCicSubstitution.lift (n - k) x,s)) + | (k, e, NCic.Meta (n,l), s) as config -> + (try + let _,_, term,_ = NCicUtils.lookup_subst n subst in + aux (k, e, NCicSubstitution.subst_meta l term,s) + with NCicUtils.Subst_not_found _ -> config) + | (_, _, NCic.Sort _, _) as config -> config + | (_, _, NCic.Implicit _, _) -> assert false + | (_, _, NCic.Prod _, _) as config -> config + | (_, _, NCic.Lambda _, []) as config -> config + | (k, e, NCic.Lambda (_,_,t), p::s) -> + aux (k+1, (RS.stack_to_env ~reduce:aux ~unwind p)::e, t,s) + | (k, e, NCic.LetIn (_,_,m,t), s) -> + let m' = RS.compute_to_env ~reduce:aux ~unwind k e m in + aux (k+1, m'::e, t, s) + | (_, _, NCic.Appl [], _) -> assert false + | (k, e, NCic.Appl (he::tl), s) -> + let tl' = + List.map (fun t->RS.compute_to_stack ~reduce:aux ~unwind (k,e,t,[])) tl + in + aux (k, e, he, tl' @ s) + | (_, _, NCic.Const(NReference.Ref (_,_,NReference.Def) as refer), s) as config -> + let _,_,body,_,_,height = NCicEnvironment.get_checked_def refer in + if delta >= height then config else aux (0, [], body, s) + | (_, _, NCic.Const (NReference.Ref + (_,_,NReference.Fix (_,recindex)) as refer),s) as config -> + let _,_,body,_, _, height = NCicEnvironment.get_checked_fix refer in + if delta >= height then config else + (match + try Some (RS.from_stack (List.nth s recindex)) + with Failure _ -> None + with + | None -> config + | Some recparam -> + match reduce ~delta:0 ~subst context recparam with + | (_,_,NCic.Const (NReference.Ref (_,_,NReference.Con _)), _) as c -> + let new_s = + replace recindex s (RS.compute_to_stack ~reduce:aux ~unwind c) + in + aux (0, [], body, new_s) + | _ -> config) + | (_, _, NCic.Const _, _) as config -> config + | (k, e, NCic.Match (_,_,term,pl),s) as config -> + let decofix = function + | (_,_,NCic.Const(NReference.Ref(_,_,NReference.CoFix _)as refer),s)-> + let _,_,body,_,_,_ = NCicEnvironment.get_checked_cofix refer in + reduce ~delta:0 ~subst context (0,[],body,s) + | config -> config + in + (match decofix (reduce ~delta:0 ~subst context (k,e,term,[])) with + | (_, _, NCic.Const (NReference.Ref (_,_,NReference.Con (_,j))),[]) -> + aux (k, e, List.nth pl (j-1), s) + | (_, _, NCic.Const + (NReference.Ref (_,_,NReference.Con (_,j)) as refer), s') -> + let leftno = NCicEnvironment.get_indty_leftno refer in + let _,params = HExtlib.split_nth leftno s' in + aux (k, e, List.nth pl (j-1), params@s) + | _ -> config) + in + aux + ;; + + let whd ?(delta=0) ?(subst=[]) context t = + unwind (reduce ~delta ~subst context (0, [], t, [])) + ;; + + end +;; + + +(* ROTTO = rompe l'unificazione poiche' riduce gli argomenti di un'applicazione + senza ridurre la testa +module R = Reduction CallByNameStrategy;; OK 56.368s +module R = Reduction CallByValueStrategy;; ROTTO +module R = Reduction CallByValueStrategyByNameOnConstants;; ROTTO +module R = Reduction LazyCallByValueStrategy;; ROTTO +module R = Reduction LazyCallByValueStrategyByNameOnConstants;; ROTTO +module R = Reduction LazyCallByNameStrategy;; OK 0m56.398s +module R = Reduction + LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns;; + OK 59.058s +module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;; OK 58.583s +module R = Reduction + ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;; OK 58.094s +module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s +*) +(*module R = Reduction(CallByValueByNameForUnwind);;*) +module RS = CallByValueByNameForUnwind';; +(*module R = Reduction(CallByNameStrategy);;*) +(*module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;*) + +(* +module R = Reduction(RS);; +module U = UriManager;; + +let whd = R.whd +*) + +(* +let whd = + let profiler_whd = HExtlib.profile ~enable:profile "are_convertible.whd" in + fun ?(delta=true) ?(subst=[]) context t -> + profiler_whd.HExtlib.profile (whd ~delta ~subst context) t +*) + +(* + + (* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then + * fallbacks to structural equality *) +let (===) x y = + Pervasives.compare x y = 0 + +(* t1, t2 must be well-typed *) +let are_convertible whd ?(subst=[]) ?(metasenv=[]) = + let heuristic = ref true in + let rec aux test_equality_only context t1 t2 ugraph = + let rec aux2 test_equality_only t1 t2 ugraph = + + (* this trivial euristic cuts down the total time of about five times ;-) *) + (* this because most of the time t1 and t2 are "sintactically" the same *) + if t1 === t2 then + true,ugraph + else + begin + let module C = Cic in + match (t1,t2) with + (C.Rel n1, C.Rel n2) -> (n1 = n2),ugraph + | (C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2)) -> + if U.eq uri1 uri2 then + (try + List.fold_right2 + (fun (uri1,x) (uri2,y) (b,ugraph) -> + let b',ugraph' = aux test_equality_only context x y ugraph in + (U.eq uri1 uri2 && b' && b),ugraph' + ) exp_named_subst1 exp_named_subst2 (true,ugraph) + with + Invalid_argument _ -> false,ugraph + ) + else + false,ugraph + | (C.Meta (n1,l1), C.Meta (n2,l2)) -> + if n1 = n2 then + let b2, ugraph1 = + let l1 = CicUtil.clean_up_local_context subst metasenv n1 l1 in + let l2 = CicUtil.clean_up_local_context subst metasenv n2 l2 in + List.fold_left2 + (fun (b,ugraph) t1 t2 -> + if b then + match t1,t2 with + None,_ + | _,None -> true,ugraph + | Some t1',Some t2' -> + aux test_equality_only context t1' t2' ugraph + else + false,ugraph + ) (true,ugraph) l1 l2 + in + if b2 then true,ugraph1 else false,ugraph + else + false,ugraph + | C.Meta (n1,l1), _ -> + (try + let _,term,_ = NCicUtils.lookup_subst n1 subst in + let term' = CicSubstitution.subst_meta l1 term in +(* +prerr_endline ("%?: " ^ CicPp.ppterm t1 ^ " <==> " ^ CicPp.ppterm t2); +prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t2); +*) + aux test_equality_only context term' t2 ugraph + with CicUtil.Subst_not_found _ -> false,ugraph) + | _, C.Meta (n2,l2) -> + (try + let _,term,_ = CicUtil.lookup_subst n2 subst in + let term' = CicSubstitution.subst_meta l2 term in +(* +prerr_endline ("%?: " ^ CicPp.ppterm t1 ^ " <==> " ^ CicPp.ppterm t2); +prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1); +*) + aux test_equality_only context t1 term' ugraph + with CicUtil.Subst_not_found _ -> false,ugraph) + (* TASSI: CONSTRAINTS *) + | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only -> + (try + true,(CicUniv.add_eq t2 t1 ugraph) + with CicUniv.UniverseInconsistency _ -> false,ugraph) + | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> + (try + true,(CicUniv.add_ge t2 t1 ugraph) + with CicUniv.UniverseInconsistency _ -> false,ugraph) + | (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph + | (C.Sort s1, C.Sort s2) -> (s1 = s2),ugraph + | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) -> + let b',ugraph' = aux true context s1 s2 ugraph in + if b' then + aux test_equality_only ((Some (name1, (C.Decl s1)))::context) + t1 t2 ugraph' + else + false,ugraph + | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) -> + let b',ugraph' = aux test_equality_only context s1 s2 ugraph in + if b' then + aux test_equality_only ((Some (name1, (C.Decl s1)))::context) + t1 t2 ugraph' + else + false,ugraph + | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) -> + let b',ugraph' = aux test_equality_only context s1 s2 ugraph in + if b' then + aux test_equality_only + ((Some (name1, (C.Def (s1,None))))::context) t1 t2 ugraph' + else + false,ugraph + | (C.Appl l1, C.Appl l2) -> + (try + List.fold_right2 + (fun x y (b,ugraph) -> + if b then + aux test_equality_only context x y ugraph + else + false,ugraph) l1 l2 (true,ugraph) + with + Invalid_argument _ -> false,ugraph + ) + | (C.Const (uri1,exp_named_subst1), C.Const (uri2,exp_named_subst2)) -> + let b' = U.eq uri1 uri2 in + if b' then + (try + List.fold_right2 + (fun (uri1,x) (uri2,y) (b,ugraph) -> + if b && U.eq uri1 uri2 then + aux test_equality_only context x y ugraph + else + false,ugraph + ) exp_named_subst1 exp_named_subst2 (true,ugraph) + with + Invalid_argument _ -> false,ugraph + ) + else + false,ugraph + | (C.MutInd (uri1,i1,exp_named_subst1), + C.MutInd (uri2,i2,exp_named_subst2) + ) -> + let b' = U.eq uri1 uri2 && i1 = i2 in + if b' then + (try + List.fold_right2 + (fun (uri1,x) (uri2,y) (b,ugraph) -> + if b && U.eq uri1 uri2 then + aux test_equality_only context x y ugraph + else + false,ugraph + ) exp_named_subst1 exp_named_subst2 (true,ugraph) + with + Invalid_argument _ -> false,ugraph + ) + else + false,ugraph + | (C.MutConstruct (uri1,i1,j1,exp_named_subst1), + C.MutConstruct (uri2,i2,j2,exp_named_subst2) + ) -> + let b' = U.eq uri1 uri2 && i1 = i2 && j1 = j2 in + if b' then + (try + List.fold_right2 + (fun (uri1,x) (uri2,y) (b,ugraph) -> + if b && U.eq uri1 uri2 then + aux test_equality_only context x y ugraph + else + false,ugraph + ) exp_named_subst1 exp_named_subst2 (true,ugraph) + with + Invalid_argument _ -> false,ugraph + ) + else + false,ugraph + | (C.MutCase (uri1,i1,outtype1,term1,pl1), + C.MutCase (uri2,i2,outtype2,term2,pl2)) -> + let b' = U.eq uri1 uri2 && i1 = i2 in + if b' then + let b'',ugraph''=aux test_equality_only context + outtype1 outtype2 ugraph in + if b'' then + let b''',ugraph'''= aux test_equality_only context + term1 term2 ugraph'' in + List.fold_right2 + (fun x y (b,ugraph) -> + if b then + aux test_equality_only context x y ugraph + else + false,ugraph) + pl1 pl2 (b''',ugraph''') + else + false,ugraph + else + false,ugraph + | (C.Fix (i1,fl1), C.Fix (i2,fl2)) -> + let tys,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl1 + in + if i1 = i2 then + List.fold_right2 + (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) (b,ugraph) -> + if b && recindex1 = recindex2 then + let b',ugraph' = aux test_equality_only context ty1 ty2 + ugraph in + if b' then + aux test_equality_only (tys@context) bo1 bo2 ugraph' + else + false,ugraph + else + false,ugraph) + fl1 fl2 (true,ugraph) + else + false,ugraph + | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) -> + let tys,_ = + List.fold_left + (fun (types,len) (n,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl1 + in + if i1 = i2 then + List.fold_right2 + (fun (_,ty1,bo1) (_,ty2,bo2) (b,ugraph) -> + if b then + let b',ugraph' = aux test_equality_only context ty1 ty2 + ugraph in + if b' then + aux test_equality_only (tys@context) bo1 bo2 ugraph' + else + false,ugraph + else + false,ugraph) + fl1 fl2 (true,ugraph) + else + false,ugraph + | C.Cast (bo,_),t -> aux2 test_equality_only bo t ugraph + | t,C.Cast (bo,_) -> aux2 test_equality_only t bo ugraph + | (C.Implicit _, _) | (_, C.Implicit _) -> assert false + | (_,_) -> false,ugraph + end + in + let res = + if !heuristic then + aux2 test_equality_only t1 t2 ugraph + else + false,ugraph + in + if fst res = true then + res + else +begin +(*if !heuristic then prerr_endline ("NON FACILE: " ^ CicPp.ppterm t1 ^ " <===> " ^ CicPp.ppterm t2);*) + (* heuristic := false; *) + debug t1 [t2] "PREWHD"; +(*prerr_endline ("PREWHD: " ^ CicPp.ppterm t1 ^ " <===> " ^ CicPp.ppterm t2);*) +(* +prerr_endline ("PREWHD: " ^ CicPp.ppterm t1 ^ " <===> " ^ CicPp.ppterm t2); + let t1' = whd ?delta:(Some true) ?subst:(Some subst) context t1 in + let t2' = whd ?delta:(Some true) ?subst:(Some subst) context t2 in + debug t1' [t2'] "POSTWHD"; +*) +let rec convert_machines ugraph = + function + [] -> true,ugraph + | ((k1,env1,ens1,h1,s1),(k2,env2,ens2,h2,s2))::tl -> + let (b,ugraph) as res = + aux2 test_equality_only + (R.unwind (k1,env1,ens1,h1,[])) (R.unwind (k2,env2,ens2,h2,[])) ugraph + in + if b then + let problems = + try + Some + (List.combine + (List.map + (fun si-> R.reduce ~delta:false ~subst context(RS.from_stack si)) + s1) + (List.map + (fun si-> R.reduce ~delta:false ~subst context(RS.from_stack si)) + s2) + @ tl) + with + Invalid_argument _ -> None + in + match problems with + None -> false,ugraph + | Some problems -> convert_machines ugraph problems + else + res +in + convert_machines ugraph + [R.reduce ~delta:true ~subst context (0,[],[],t1,[]), + R.reduce ~delta:true ~subst context (0,[],[],t2,[])] +(*prerr_endline ("POSTWH: " ^ CicPp.ppterm t1' ^ " <===> " ^ CicPp.ppterm t2');*) +(* + aux2 test_equality_only t1' t2' ugraph +*) +end + in + aux false (*c t1 t2 ugraph *) +;; +*) + +(* DEBUGGING ONLY +let whd ?(delta=true) ?(subst=[]) context t = + let res = whd ~delta ~subst context t in + let rescsc = CicReductionNaif.whd ~delta ~subst context t in + if not (fst (are_convertible CicReductionNaif.whd ~subst context res rescsc CicUniv.empty_ugraph)) then + begin + debug_print (lazy ("PRIMA: " ^ CicPp.ppterm t)) ; + flush stderr ; + debug_print (lazy ("DOPO: " ^ CicPp.ppterm res)) ; + flush stderr ; + debug_print (lazy ("CSC: " ^ CicPp.ppterm rescsc)) ; + flush stderr ; +fdebug := 0 ; +let _ = are_convertible CicReductionNaif.whd ~subst context res rescsc CicUniv.empty_ugraph in + assert false ; + end + else + res +;; +*) + +(* +let are_convertible = are_convertible whd + +let whd = R.whd +*) + +(* +let profiler_other_whd = HExtlib.profile ~enable:profile "~are_convertible.whd" +let whd ?(delta=true) ?(subst=[]) context t = + let foo () = + whd ~delta ~subst context t + in + profiler_other_whd.HExtlib.profile foo () +*) + +(* +let rec normalize ?(delta=true) ?(subst=[]) ctx term = + let module C = Cic in + let t = whd ~delta ~subst ctx term in + let aux = normalize ~delta ~subst in + let decl name t = Some (name, C.Decl t) in + match t with + | C.Rel n -> t + | C.Var (uri,exp_named_subst) -> + C.Var (uri, List.map (fun (n,t) -> n,aux ctx t) exp_named_subst) + | C.Meta (i,l) -> + C.Meta (i,List.map (function Some t -> Some (aux ctx t) | None -> None) l) + | C.Sort _ -> t + | C.Implicit _ -> t + | C.Cast (te,ty) -> C.Cast (aux ctx te, aux ctx ty) + | C.Prod (n,s,t) -> + let s' = aux ctx s in + C.Prod (n, s', aux ((decl n s')::ctx) t) + | C.Lambda (n,s,t) -> + let s' = aux ctx s in + C.Lambda (n, s', aux ((decl n s')::ctx) t) + | C.LetIn (n,s,t) -> + (* the term is already in weak head normal form *) + assert false + | C.Appl (h::l) -> C.Appl (h::(List.map (aux ctx) l)) + | C.Appl [] -> assert false + | C.Const (uri,exp_named_subst) -> + C.Const (uri, List.map (fun (n,t) -> n,aux ctx t) exp_named_subst) + | C.MutInd (uri,typeno,exp_named_subst) -> + C.MutInd (uri,typeno, List.map (fun (n,t) -> n,aux ctx t) exp_named_subst) + | C.MutConstruct (uri,typeno,consno,exp_named_subst) -> + C.MutConstruct (uri, typeno, consno, + List.map (fun (n,t) -> n,aux ctx t) exp_named_subst) + | C.MutCase (sp,i,outt,t,pl) -> + C.MutCase (sp,i, aux ctx outt, aux ctx t, List.map (aux ctx) pl) +(*CSC: to be completed, I suppose *) + | C.Fix _ -> t + | C.CoFix _ -> t +*) + +(* +let normalize ?delta ?subst ctx term = +(* prerr_endline ("NORMALIZE:" ^ CicPp.ppterm term); *) + let t = normalize ?delta ?subst ctx term in +(* prerr_endline ("NORMALIZED:" ^ CicPp.ppterm t); *) + t +*) + +(* performs an head beta/cast reduction +let rec head_beta_reduce ?(delta=false) ?(upto=(-1)) t = + match upto with + 0 -> t + | n -> + match t with + (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) -> + let he'' = CicSubstitution.subst he' t in + if tl' = [] then + he'' + else + let he''' = + match he'' with + Cic.Appl l -> Cic.Appl (l@tl') + | _ -> Cic.Appl (he''::tl') + in + head_beta_reduce ~delta ~upto:(upto - 1) he''' + | Cic.Cast (te,_) -> head_beta_reduce ~delta ~upto te + | Cic.Appl (Cic.Const (uri,ens)::tl) as t when delta=true -> + let bo = + match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with + Cic.Constant (_,bo,_,_,_) -> bo + | Cic.Variable _ -> raise ReferenceToVariable + | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo + | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition + in + (match bo with + None -> t + | Some bo -> + head_beta_reduce ~upto + ~delta (Cic.Appl ((CicSubstitution.subst_vars ens bo)::tl))) + | Cic.Const (uri,ens) as t when delta=true -> + let bo = + match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with + Cic.Constant (_,bo,_,_,_) -> bo + | Cic.Variable _ -> raise ReferenceToVariable + | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo + | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition + in + (match bo with + None -> t + | Some bo -> + head_beta_reduce ~delta ~upto (CicSubstitution.subst_vars ens bo)) + | t -> t +*) +(* +let are_convertible ?subst ?metasenv context t1 t2 ugraph = + let before = Unix.gettimeofday () in + let res = are_convertible ?subst ?metasenv context t1 t2 ugraph in + let after = Unix.gettimeofday () in + let diff = after -. before in + if diff > 0.1 then + begin + let nc = List.map (function None -> None | Some (n,_) -> Some n) context in + prerr_endline + ("\n#(" ^ string_of_float diff ^ "):\n" ^ CicPp.pp t1 nc ^ "\n<=>\n" ^ CicPp.pp t2 nc); + end; + res +*) diff --git a/helm/software/components/ng_kernel/nCicReduction.mli b/helm/software/components/ng_kernel/nCicReduction.mli new file mode 100644 index 000000000..328924c79 --- /dev/null +++ b/helm/software/components/ng_kernel/nCicReduction.mli @@ -0,0 +1,46 @@ +(* 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/. + *) + +exception WrongUriToInductiveDefinition +exception ReferenceToConstant +exception ReferenceToVariable +exception ReferenceToCurrentProof +exception ReferenceToInductiveDefinition +(* +val fdebug : int ref +val whd : + ?delta:bool -> ?subst:Cic.substitution -> Cic.context -> Cic.term -> Cic.term +val are_convertible : + ?subst:Cic.substitution -> ?metasenv:Cic.metasenv -> + Cic.context -> Cic.term -> Cic.term -> CicUniv.universe_graph -> + bool * CicUniv.universe_graph +val normalize: + ?delta:bool -> ?subst:Cic.substitution -> Cic.context -> Cic.term -> Cic.term + +(* performs head beta/(delta)/cast reduction; the default is to not perform + delta reduction; if provided, ~upto is the maximum number of beta redexes + reduced *) +val head_beta_reduce: ?delta:bool -> ?upto:int -> Cic.term -> Cic.term +*) diff --git a/helm/software/components/ng_kernel/nCicSubstitution.ml b/helm/software/components/ng_kernel/nCicSubstitution.ml index 4f5e25ecc..1439544b3 100644 --- a/helm/software/components/ng_kernel/nCicSubstitution.ml +++ b/helm/software/components/ng_kernel/nCicSubstitution.ml @@ -61,7 +61,9 @@ let lift ?(from=1) n t = (* 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 = +(* map_arg is ReductionStrategy.from_env_for_unwind when psubst is *) +(* used to implement nCicReduction.unwind' *) +let rec psubst ?(avoid_beta_redexes=false) delift lift_args map_arg args = let nargs = List.length args in let rec substaux k = function | NCic.Sort _ @@ -71,10 +73,12 @@ let rec psubst ?(avoid_beta_redexes=false) delift lift_args args = | 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)) + (try lift (k+lift_args) (map_arg (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)) as t when m >= k + nargs - 1 -> + if delift then NCic.Meta (i,(m-nargs,l)) else t + | NCic.Meta (i,(m,(NCic.Irl l as irl))) as t when k > l + m -> + if delift then NCic.Meta (i,(m-nargs,irl)) else t | NCic.Meta (i,(m,l)) -> let lctx = NCicUtils.expand_local_context l in (* 1-nargs < k-m, when <= 0 is still reasonable because we will @@ -93,7 +97,10 @@ let rec psubst ?(avoid_beta_redexes=false) delift lift_args 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 + (* map_arg is here \x.x, Obj magic is needed because + * we don't have polymorphic recursion w/o records *) + avoid (psubst + ~avoid_beta_redexes true 0 Obj.magic [Obj.magic arg] bo) tl | _ as he -> NCic.Appl (he::args)) in let tl = List.map (substaux k) tl in @@ -105,7 +112,8 @@ let rec psubst ?(avoid_beta_redexes=false) delift lift_args args = substaux 1 ;; -let subst ?avoid_beta_redexes arg = psubst ?avoid_beta_redexes true 0 [arg];; +let subst ?avoid_beta_redexes arg = + psubst ?avoid_beta_redexes true 0 (fun x -> x)[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 *) @@ -114,5 +122,5 @@ let subst ?avoid_beta_redexes arg = psubst ?avoid_beta_redexes true 0 [arg];; let subst_meta = function | m, NCic.Irl _ | m, NCic.Ctx [] -> lift m - | m, NCic.Ctx l -> psubst false m l + | m, NCic.Ctx l -> psubst false m (fun x -> x) l ;; diff --git a/helm/software/components/ng_kernel/nCicSubstitution.mli b/helm/software/components/ng_kernel/nCicSubstitution.mli index 30a6c7451..158f53fdc 100644 --- a/helm/software/components/ng_kernel/nCicSubstitution.mli +++ b/helm/software/components/ng_kernel/nCicSubstitution.mli @@ -37,6 +37,20 @@ val lift : ?from:int -> int -> NCic.term -> NCic.term (* well typed and avoid_beta_redexes is true. *) val subst : ?avoid_beta_redexes:bool -> NCic.term -> NCic.term -> NCic.term +(* psubst [avoid] [delift] [lift_args] [t] [map_arg] [args] + * [avoid] : do not leave newly created beta-redexes, default false + * [delift] : perform delifting + * [t] : term to fill in + * [lift_args] : lift argument after map_arg is applied + * [args] : stuff to substitute + * [map_arg] : map the argument to obtain a term + * the function is ReductionStrategy.from_env_for_unwind when psubst is + * used to implement nCicReduction.unwind' *) +val psubst : + ?avoid_beta_redexes:bool -> bool -> int -> + ('a -> NCic.term) -> 'a list -> 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 *) diff --git a/helm/software/components/ng_kernel/nCicUtils.ml b/helm/software/components/ng_kernel/nCicUtils.ml index 2a9aaf0a5..965f1cf2b 100644 --- a/helm/software/components/ng_kernel/nCicUtils.ml +++ b/helm/software/components/ng_kernel/nCicUtils.ml @@ -35,3 +35,10 @@ let expand_local_context = function | NCic.Ctx lctx -> lctx ;; +exception Subst_not_found of int + +let lookup_subst n subst = + try + List.assoc n subst + with Not_found -> raise (Subst_not_found n) + diff --git a/helm/software/components/ng_kernel/nCicUtils.mli b/helm/software/components/ng_kernel/nCicUtils.mli index 45c444ac4..6af6ac8f0 100644 --- a/helm/software/components/ng_kernel/nCicUtils.mli +++ b/helm/software/components/ng_kernel/nCicUtils.mli @@ -25,5 +25,9 @@ (* $Id: nCicSubstitution.ml 8135 2008-02-13 15:35:43Z tassi $ *) +exception Subst_not_found of int + val expand_local_context : NCic.lc_kind -> NCic.term list +val lookup_subst: int -> NCic.substitution -> NCic.subst_entry + -- 2.39.2