From 3ddad84e0daa6e9552168f7a8ecb101e23c33476 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 15 Apr 2008 13:44:16 +0000 Subject: [PATCH] get_checked_fix -> get_checked_fixes --- helm/software/components/ng_kernel/nCicEnvironment.ml | 7 +++---- .../software/components/ng_kernel/nCicEnvironment.mli | 8 ++++---- helm/software/components/ng_kernel/nCicReduction.ml | 10 ++++++---- helm/software/components/ng_kernel/nCicTypeChecker.ml | 11 ++++++++++- 4 files changed, 23 insertions(+), 13 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml index 1076adbf5..cca0e5cdf 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.ml +++ b/helm/software/components/ng_kernel/nCicEnvironment.ml @@ -68,13 +68,12 @@ let get_checked_fix_or_cofix b = function | NReference.Ref (_, uri, (NReference.Fix (fixno,_)|NReference.CoFix 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 + funcs, att, height | _ ->prerr_endline "get_checked_(co)fix on a non (co)fix 2";assert false) | r -> prerr_endline ("get_checked_(co)fix on " ^ NReference.string_of_reference r); 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_checked_fixes r = get_checked_fix_or_cofix true r;; +let get_checked_cofixes r = get_checked_fix_or_cofix false r;; let get_indty_leftno = function | NReference.Ref (_, uri, NReference.Ind _) diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli index 6f224d527..07bd1b51c 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.mli +++ b/helm/software/components/ng_kernel/nCicEnvironment.mli @@ -39,13 +39,13 @@ val get_checked_indtys: NReference.reference -> bool * int * NCic.inductiveType list * NCic.i_attr * int -val get_checked_fix: +val get_checked_fixes: NReference.reference -> - NCic.relevance * string * NCic.term * NCic.term * NCic.f_attr * int + NCic.inductiveFun list * NCic.f_attr * int -val get_checked_cofix: +val get_checked_cofixes: NReference.reference -> - NCic.relevance * string * NCic.term * NCic.term * NCic.f_attr * int + NCic.inductiveFun list * NCic.f_attr * int val get_indty_leftno: NReference.reference -> int diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index defd12e29..db19c9c96 100644 --- a/helm/software/components/ng_kernel/nCicReduction.ml +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -421,8 +421,8 @@ module Reduction(RS : Strategy) = 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 + (_,_,NReference.Fix (fixno,recindex)) as refer),s) as config -> + let fixes,_, height = NCicEnvironment.get_checked_fixes refer in if delta > height then config else (match try Some (RS.from_stack (List.nth s recindex)) @@ -435,13 +435,15 @@ module Reduction(RS : Strategy) = let new_s = replace recindex s (RS.compute_to_stack ~reduce:aux ~unwind c) in + let _,_,_,_,body = List.nth fixes fixno 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 + | (_,_,NCic.Const(NReference.Ref(_,_,NReference.CoFix c)as refer),s)-> + let cofixes,_,_ = NCicEnvironment.get_checked_cofixes refer in + let _,_,_,_,body = List.nth cofixes c in reduce ~delta:0 ~subst context (0,[],body,s) | config -> config in diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 26e2163ea..690cd5900 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -889,7 +889,8 @@ and eat_lambdas ~subst ~metasenv context n te = and guarded_by_destructors ~subst ~metasenv context recfuns t = let recursor f k t = NCicUtils.fold shift_k k (fun k () -> f k) () t in - let rec aux (context, recfuns, x, safes as k) = function + let rec aux (context, recfuns, x, safes as k) t = + match R.whd ~subst context t with (* TODO: use ~delta:false as mush as poss*) | C.Rel m as t when List.mem_assoc m recfuns -> raise (NotGuarded (lazy (NCicPp.ppterm ~subst ~metasenv ~context t ^ " passed around"))) @@ -910,6 +911,14 @@ and guarded_by_destructors ~subst ~metasenv context recfuns t = raise (NotGuarded (lazy (NCicPp.ppterm ~context ~subst ~metasenv rec_arg ^ " not smaller"))); List.iter (aux k) tl + (* + | C.Appl (C.Const ((Ref.Ref (_,_,Ref.Fix (i,j))) as r)::args) -> + List.iter (aux k) args; + let fixes,_,_ = E.get_checked_fixes r in + let _,_,_,_,bo = List.nth fixes i in + let bo_wout_lam, context = eat_lambdas ~subst ~metasenv context j in + (* debruijna body..... *) assert false +*) | C.Match (Ref.Ref (_,uri,_) as ref,outtype,term,pl) as t -> (match R.whd ~subst context term with | C.Rel m | C.Appl (C.Rel m :: _ ) as t when List.mem m safes || m = x -> -- 2.39.2