X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicReduction.ml;h=432ea9a45bd4c79e599181da2db0cd9038a06463;hb=9aaaba04fbd198881aaee42cfc41fdb75db1eeaa;hp=2e13a5304b23b5adca91ef71dcb9c7d2f4349781;hpb=c6ec0dc44c2e592c7b1323304052bc1a523e7c22;p=helm.git diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index 2e13a5304..432ea9a45 100644 --- a/helm/software/components/ng_kernel/nCicReduction.ml +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -22,41 +22,56 @@ module type Strategy = sig type env_term type config = int * env_term list * C.term * stack_term list val to_env : - reduce: (config -> config * bool) -> unwind: (config -> C.term) -> + reduce: (delta:int -> config -> config * bool) -> + unwind: (config -> C.term) -> config -> env_term - val from_stack : stack_term -> config + val from_stack : delta:int -> stack_term -> config val from_stack_list_for_unwind : - unwind: (config -> C.term) -> stack_term list -> C.term list - val from_env : env_term -> config + unwind: (config -> C.term) -> stack_term list -> C.term list + val from_env : delta:int -> env_term -> config val from_env_for_unwind : - unwind: (config -> C.term) -> env_term -> C.term + unwind: (config -> C.term) -> env_term -> C.term val stack_to_env : - reduce: (config -> config * bool) -> unwind: (config -> C.term) -> + reduce: (delta:int -> config -> config * bool) -> + unwind: (config -> C.term) -> stack_term -> env_term val compute_to_env : - reduce: (config -> config * bool) -> unwind: (config -> C.term) -> + reduce: (delta:int -> config -> config * bool) -> + unwind: (config -> C.term) -> int -> env_term list -> C.term -> env_term val compute_to_stack : - reduce: (config -> config * bool) -> unwind: (config -> C.term) -> + reduce: (delta:int -> config -> config * bool) -> + unwind: (config -> C.term) -> config -> stack_term end ;; -module CallByValueByNameForUnwind' = struct +module CallByValueByNameForUnwind' : Strategy = struct type config = int * env_term list * C.term * stack_term list - and stack_term = config lazy_t * C.term lazy_t (* cbv, cbn *) - and env_term = config lazy_t * C.term lazy_t (* cbv, cbn *) - let to_env ~reduce ~unwind c = lazy (fst (reduce c)),lazy (unwind c) - let from_stack (c,_) = Lazy.force c + and stack_term = + config Lazy.t * (int -> config) * C.term Lazy.t + and env_term = + config Lazy.t (* cbneed ~delta:0 *) + * (int -> config) (* cbvalue ~delta *) + * C.term Lazy.t (* cbname ~delta:max_int *) + let to_env ~reduce ~unwind c = + lazy (fst (reduce ~delta:0 c)), + (fun delta -> fst (reduce ~delta c)), + lazy (unwind c) + let from_stack ~delta (c0,c,_) = if delta = 0 then Lazy.force c0 else c delta 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 + List.map (fun (_,_,c) -> Lazy.force c) l + let from_env ~delta (c0,c,_) = if delta = 0 then Lazy.force c0 else c delta + 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 (fst (reduce (k,e,t,[]))), lazy (unwind (k,e,t,[])) + lazy (fst (reduce ~delta:0 (k,e,t,[]))), + (fun delta -> fst (reduce ~delta (k,e,t,[]))), + lazy (unwind (k,e,t,[])) let compute_to_stack ~reduce ~unwind config = - lazy (fst (reduce config)), lazy (unwind config) + lazy (fst (reduce ~delta:0 config)), + (fun delta -> fst (reduce ~delta config)), + lazy (unwind config) end ;; @@ -87,7 +102,7 @@ module Reduction(RS : Strategy) = struct let rec reduce ~delta ?(subst = []) context : config -> config * bool = let rec aux = function | k, e, C.Rel n, s when n <= k -> - let k',e',t',s' = RS.from_env (list_nth e (n-1)) in + let k',e',t',s' = RS.from_env ~delta (list_nth e (n-1)) in aux (k',e',t',s'@s) | k, _, C.Rel n, s as config (* when n > k *) -> let x= try Some (List.nth context (n - 1 - k)) with Failure _ -> None in @@ -104,14 +119,15 @@ module Reduction(RS : Strategy) = struct | (_, _, C.Prod _, _) | (_, _, C.Lambda _, []) as config -> config, true | (k, e, C.Lambda (_,_,t), p::s) -> - aux (k+1, (RS.stack_to_env ~reduce:aux ~unwind p)::e, t,s) + aux (k+1, (RS.stack_to_env ~reduce:(reduce ~subst context) ~unwind p)::e, t,s) | (k, e, C.LetIn (_,_,m,t), s) -> - let m' = RS.compute_to_env ~reduce:aux ~unwind k e m in + let m' = RS.compute_to_env ~reduce:(reduce ~subst context) ~unwind k e m in aux (k+1, m'::e, t, s) | (_, _, C.Appl ([]|[_]), _) -> assert false | (k, e, C.Appl (he::tl), s) -> let tl' = - List.map (fun t->RS.compute_to_stack ~reduce:aux ~unwind (k,e,t,[])) tl + List.map (fun t->RS.compute_to_stack + ~reduce:(reduce ~subst context) ~unwind (k,e,t,[])) tl in aux (k, e, he, tl' @ s) | (_, _, C.Const @@ -128,7 +144,7 @@ module Reduction(RS : Strategy) = struct (_,Ref.Fix (fixno,recindex,height)) as refer) as head),s) as config -> (* if delta >= height then config else *) (match - try Some (RS.from_stack (List.nth s recindex)) + try Some (RS.from_stack ~delta (List.nth s recindex)) with Failure _ -> None with | None -> config, true @@ -138,12 +154,14 @@ module Reduction(RS : Strategy) = struct | (_,_,C.Const (Ref.Ref (_,Ref.Con _)), _) as c, _ when delta >= height -> let new_s = - replace recindex s (RS.compute_to_stack ~reduce:aux ~unwind c) + replace recindex s (RS.compute_to_stack ~reduce:(reduce ~subst + context) ~unwind c) in (0, [], head, new_s), false | (_,_,C.Const (Ref.Ref (_,Ref.Con _)), _) as c, _ -> let new_s = - replace recindex s (RS.compute_to_stack ~reduce:aux ~unwind c) + replace recindex s (RS.compute_to_stack ~reduce:(reduce ~subst + context) ~unwind c) in let _,_,_,_,body = List.nth fixes fixno in aux (0, [], body, new_s) @@ -281,7 +299,7 @@ let alpha_eq ~test_lambda_source aux test_eq_only metasenv subst context t1 t2 = | (C.Appl (hd1::tl1), C.Appl (hd2::tl2)) -> aux test_eq_only context hd1 hd2 && - let relevance = !get_relevance ~metasenv ~subst context hd1 tl1 in + let relevance = !get_relevance ~metasenv ~subst context hd1 tl1 in (try HExtlib.list_forall_default3 (fun t1 t2 b -> not b || aux true context t1 t2) @@ -361,8 +379,8 @@ let are_convertible ~metasenv ~subst = HExtlib.list_forall_default3 (fun t1 t2 b -> not b || - let t1 = RS.from_stack t1 in - let t2 = RS.from_stack t2 in + let t1 = RS.from_stack ~delta:max_int t1 in + let t2 = RS.from_stack ~delta:max_int t2 in convert_machines true (put_in_whd t1 t2)) s1 s2 true relevance with Invalid_argument _ -> false) || (not (norm1 && norm2) && convert_machines test_eq_only (small_delta_step m1 m2))