From 002d456397be2f0046bb50356e80816f7296647d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 5 Dec 2008 18:16:01 +0000 Subject: [PATCH] a few missing ~subst added to whd --- .../components/ng_disambiguation/nCicDisambiguate.ml | 2 +- helm/software/components/ng_kernel/nCicReduction.ml | 2 +- helm/software/components/ng_kernel/nCicReduction.mli | 2 +- .../software/components/ng_kernel/nCicTypeChecker.ml | 12 ++++++------ helm/software/components/ng_refiner/nCicCoercion.ml | 10 +++++----- helm/software/components/ng_refiner/nCicMetaSubst.ml | 4 ++-- .../software/components/ng_refiner/nCicMetaSubst.mli | 3 ++- helm/software/components/ng_refiner/nCicRefiner.ml | 2 +- 8 files changed, 19 insertions(+), 18 deletions(-) diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index 4092e7ae0..7f9ab1b6e 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -187,7 +187,7 @@ let interpretate_term List.nth itl indtyp_no with _ -> assert false in let rec count_prod t = - match NCicReduction.whd [] t with + match NCicReduction.whd ~subst:[] [] t with NCic.Prod (_, _, t) -> 1 + (count_prod t) | _ -> 0 in diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index a7dfc50fa..7dbe379e4 100644 --- a/helm/software/components/ng_kernel/nCicReduction.ml +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -165,7 +165,7 @@ module Reduction(RS : Strategy) = struct aux ;; - let whd ?(delta=0) ?(subst=[]) context t = + let whd ?(delta=0) ~subst context t = unwind (fst (reduce ~delta ~subst context (0, [], t, []))) ;; diff --git a/helm/software/components/ng_kernel/nCicReduction.mli b/helm/software/components/ng_kernel/nCicReduction.mli index 696723bf6..006dba9d4 100644 --- a/helm/software/components/ng_kernel/nCicReduction.mli +++ b/helm/software/components/ng_kernel/nCicReduction.mli @@ -12,7 +12,7 @@ (* $Id$ *) val whd : - ?delta:int -> ?subst:NCic.substitution -> + ?delta:int -> subst:NCic.substitution -> NCic.context -> NCic.term -> NCic.term diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index da130c555..c09b036b6 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -235,7 +235,7 @@ let check_homogeneous_call ~subst context indparamsno n uri reduct tl = (fun k x -> if k = 0 then 0 else - match R.whd context x with + match R.whd ~subst context x with | C.Rel m when m = n - (indparamsno - k) -> k - 1 | _ -> raise (TypeCheckerFailure (lazy ("Argument "^string_of_int (indparamsno - k + 1) ^ " (of " ^ @@ -268,7 +268,7 @@ let rec weakly_positive ~subst context n nn uri indparamsno posuri te = are skipped because we already know that are_all_occurrences_positive of uri in te. *) let rec aux context n nn te = - match R.whd context te with + match R.whd ~subst context te with | t when t = dummy -> true | C.Appl (te::rargs) when te = dummy -> List.for_all (does_not_occur ~subst context n nn) rargs @@ -286,7 +286,7 @@ let rec weakly_positive ~subst context n nn uri indparamsno posuri te = aux context n nn (subst_inductive_type_with_dummy () te) and strictly_positive ~subst context n nn indparamsno posuri te = - match R.whd context te with + match R.whd ~subst context te with | t when does_not_occur ~subst context n nn t -> true | C.Rel _ when indparamsno = 0 -> true | C.Appl ((C.Rel m)::tl) as reduct when m > n && m <= nn -> @@ -314,7 +314,7 @@ and strictly_positive ~subst context n nn indparamsno posuri te = (* the inductive type indexes are s.t. n < x <= nn *) and are_all_occurrences_positive ~subst context uri indparamsno i n nn te = - match R.whd context te with + match R.whd ~subst context te with | C.Appl ((C.Rel m)::tl) as reduct when m = i -> check_homogeneous_call ~subst context indparamsno n uri reduct tl; List.for_all (does_not_occur ~subst context n nn) tl @@ -714,7 +714,7 @@ and is_non_recursive_singleton ~subst (Ref.Ref (uri,_)) iname ity cty = and is_non_informative ~metasenv ~subst paramsno c = let rec aux context c = - match R.whd context c with + match R.whd ~subst context c with | C.Prod (n,so,de) -> let s = typeof ~metasenv ~subst context so in s = C.Sort C.Prop && aux ((n,(C.Decl so))::context) de @@ -1001,7 +1001,7 @@ and guarded_by_constructors ~subst ~metasenv context t indURI indlen nn = aux context 0 nn false t and recursive_args ~subst ~metasenv context n nn te = - match R.whd context te with + match R.whd ~subst context te with | C.Rel _ | C.Appl _ | C.Const _ -> [] | C.Prod (name,so,de) -> (not (does_not_occur ~subst context n nn so)) :: diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml index 2fc29d597..b8f31c805 100644 --- a/helm/software/components/ng_refiner/nCicCoercion.ml +++ b/helm/software/components/ng_refiner/nCicCoercion.ml @@ -40,7 +40,8 @@ let db () = let arity = match tgt with | CoercDb.Fun i -> i | _ -> 0 in let src, tgt = let cty = NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] c in - match NCicMetaSubst.saturate ~delta:max_int [] [] cty (arity+1) + match + NCicMetaSubst.saturate ~delta:max_int [] [] [] cty (arity+1) with | NCic.Prod (_, src, tgt),_,_ -> src, NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) tgt @@ -58,8 +59,7 @@ let db () = (DB.empty,DB.empty) (CoercDb.to_list ()) ;; -(* XXX saturate takes no subst!!!! *) -let look_for_coercion (db_src,db_tgt) metasenv _subst context infty expty = +let look_for_coercion (db_src,db_tgt) metasenv subst context infty expty = let set_src = DB.retrieve_unifiables db_src infty in let set_tgt = DB.retrieve_unifiables db_tgt expty in let candidates = CoercionSet.inter set_src set_tgt in @@ -68,11 +68,11 @@ let look_for_coercion (db_src,db_tgt) metasenv _subst context infty expty = (fun (t,arity,arg) -> let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t in let ty, metasenv, args = - NCicMetaSubst.saturate ~delta:max_int metasenv context ty arity + NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty arity in prerr_endline ( NCicPp.ppterm ~metasenv ~subst:[] ~context:[] ty ^ " --- " ^ - NCicPp.ppterm ~metasenv ~subst:_subst ~context + NCicPp.ppterm ~metasenv ~subst ~context (NCicUntrusted.mk_appl t args) ^ " --- " ^ string_of_int (List.length args) ^ " == " ^ string_of_int arg); metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg) diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index 5e72d90c7..6a0406747 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.ml +++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml @@ -363,7 +363,7 @@ let mk_meta ?name metasenv context ty = mk_meta name (newmeta ()) metasenv context ty ;; -let saturate ?(delta=0) metasenv context ty goal_arity = +let saturate ?(delta=0) metasenv subst context ty goal_arity = assert (goal_arity >= 0); let rec aux metasenv = function | NCic.Prod (name,s,t) -> @@ -377,7 +377,7 @@ let saturate ?(delta=0) metasenv context ty goal_arity = else t, metasenv1, arg::args, pno+1 | ty -> - match NCicReduction.whd context ty ~delta with + match NCicReduction.whd ~subst context ty ~delta with | NCic.Prod _ as ty -> aux metasenv ty | ty -> ty, metasenv, [], 0 in diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.mli b/helm/software/components/ng_refiner/nCicMetaSubst.mli index 21ac5c3cc..1d7b6729e 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.mli +++ b/helm/software/components/ng_refiner/nCicMetaSubst.mli @@ -61,6 +61,7 @@ val mk_meta: (* returns the resulting type, the metasenv and the arguments *) val saturate: - ?delta:int -> NCic.metasenv -> NCic.context -> NCic.term -> int -> + ?delta:int -> NCic.metasenv -> NCic.substitution -> + NCic.context -> NCic.term -> int -> NCic.term * NCic.metasenv * NCic.term list diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index e9d0e97fd..7ea11f312 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -225,7 +225,7 @@ let rec typeof let _, _, arity, cl = List.nth itl tyno in let constructorsno = List.length cl in let _, metasenv, args = - NCicMetaSubst.saturate metasenv context arity 0 in + NCicMetaSubst.saturate metasenv subst context arity 0 in let ind = if args = [] then C.Const r else C.Appl (C.Const r::args) in let metasenv, subst, term, _ = typeof_aux metasenv subst context (Some ind) term in -- 2.39.2