X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicReduction.ml;h=2b1d4119b51b4ec6d7b9206d289a704d2d4bc383;hb=e02c6eaf8d50025c3be8bbf6988ab8b2a37b40da;hp=a7dfc50fad582819e0a62a2d97c076e8b51d9db9;hpb=05adc7f9da7d66a14fd4417911e9f22b9bf9583f;p=helm.git diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index a7dfc50fa..2b1d4119b 100644 --- a/helm/software/components/ng_kernel/nCicReduction.ml +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -114,7 +114,9 @@ module Reduction(RS : Strategy) = struct aux (k, e, he, tl' @ s) | (_, _, C.Const (Ref.Ref (_,Ref.Def height) as refer), s) as config -> - if delta >= height then config, false else + if delta >= height then + config, false + else let _,_,body,_,_,_ = NCicEnvironment.get_checked_def refer in aux (0, [], body, s) | (_, _, C.Const (Ref.Ref (_, @@ -154,18 +156,20 @@ module Reduction(RS : Strategy) = struct c | config -> config in - (match decofix (fst (reduce ~delta:0 ~subst context (k,e,term,[]))) with + let match_head = k,e,term,[] in + let reduced,_ = reduce ~delta:0 ~subst context match_head in + (match decofix reduced with | (_, _, C.Const (Ref.Ref (_,Ref.Con (_,j,_))),[]) -> aux (k, e, List.nth pl (j-1), s) | (_, _, C.Const (Ref.Ref (_,Ref.Con (_,j,lno))), s')-> let _,params = HExtlib.split_nth lno s' in aux (k, e, List.nth pl (j-1), params@s) - | _ -> config,true) + | _ -> config, true) in aux ;; - let whd ?(delta=0) ?(subst=[]) context t = + let whd ?(delta=0) ~subst context t = unwind (fst (reduce ~delta ~subst context (0, [], t, []))) ;; @@ -253,7 +257,7 @@ let are_convertible ~metasenv ~subst = in (try HExtlib.list_forall_default3_var - (fun t1 t2 b -> not b || aux test_eq_only context t1 t2 ) + (fun t1 t2 b -> not b || aux true context t1 t2 ) tl1 tl2 true relevance with Invalid_argument _ -> false | HExtlib.FailureAt fail -> @@ -268,7 +272,7 @@ let are_convertible ~metasenv ~subst = let _,tl2 = HExtlib.split_nth (fail+1) tl2 in try HExtlib.list_forall_default3 - (fun t1 t2 b -> not b || aux test_eq_only context t1 t2) + (fun t1 t2 b -> not b || aux true context t1 t2) tl1 tl2 true relevance with Invalid_argument _ -> false else false) @@ -278,7 +282,7 @@ let are_convertible ~metasenv ~subst = let relevance = !get_relevance ~metasenv ~subst context hd1 tl1 in (try HExtlib.list_forall_default3 - (fun t1 t2 b -> not b || aux test_eq_only context t1 t2) + (fun t1 t2 b -> not b || aux true context t1 t2) tl1 tl2 true relevance with Invalid_argument _ -> false) @@ -335,7 +339,7 @@ let are_convertible ~metasenv ~subst = R.reduce ~delta ~subst context m1, R.reduce ~delta ~subst context m2 in - let rec convert_machines + let rec convert_machines test_eq_only ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2), norm2 as m2) = (alpha_eq test_eq_only @@ -350,33 +354,41 @@ let are_convertible ~metasenv ~subst = not b || let t1 = RS.from_stack t1 in let t2 = RS.from_stack t2 in - convert_machines (put_in_whd t1 t2)) s1 s2 true relevance + convert_machines true (put_in_whd t1 t2)) s1 s2 true relevance with Invalid_argument _ -> false) || - (not (norm1 && norm2) && convert_machines (small_delta_step m1 m2)) + (not (norm1 && norm2) && convert_machines test_eq_only (small_delta_step m1 m2)) in - convert_machines (put_in_whd (0,[],t1,[]) (0,[],t2,[])) + convert_machines test_eq_only (put_in_whd (0,[],t1,[]) (0,[],t2,[])) in aux false ;; -let rec head_beta_reduce ?(delta=max_int) ?(upto=(-1)) t l = +let rec head_beta_reduce ~delta ~upto ~subst t l = match upto, t, l with | 0, C.Appl l1, _ -> C.Appl (l1 @ l) | 0, t, [] -> t | 0, t, _ -> C.Appl (t::l) - | _, C.Appl (hd::tl), _ -> head_beta_reduce ~delta ~upto hd (tl @ l) + | _, C.Meta (n,ctx), _ -> + (try + let _,_, term,_ = NCicUtils.lookup_subst n subst in + head_beta_reduce ~delta ~upto ~subst + (NCicSubstitution.subst_meta ctx term) l + with NCicUtils.Subst_not_found _ -> if l = [] then t else C.Appl (t::l)) + | _, C.Appl (hd::tl), _ -> head_beta_reduce ~delta ~upto ~subst hd (tl @ l) | _, C.Lambda(_,_,bo), arg::tl -> let bo = NCicSubstitution.subst arg bo in - head_beta_reduce ~delta ~upto:(upto - 1) bo tl + head_beta_reduce ~delta ~upto:(upto - 1) ~subst bo tl | _, C.Const (Ref.Ref (_, Ref.Def height) as re), _ when delta <= height -> let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def re in - head_beta_reduce ~upto ~delta bo l + head_beta_reduce ~upto ~delta ~subst bo l | _, t, [] -> t | _, t, _ -> C.Appl (t::l) ;; -let head_beta_reduce ?delta ?upto t = head_beta_reduce ?delta ?upto t [];; +let head_beta_reduce ?(delta=max_int) ?(upto= -1) ?(subst=[]) t = + head_beta_reduce ~delta ~upto ~subst t [] +;; type stack_item = RS.stack_term type environment_item = RS.env_term @@ -387,4 +399,12 @@ let reduce_machine = R.reduce let from_stack = RS.from_stack let unwind = R.unwind +let _ = + NCicUtils.set_head_beta_reduce (fun ~upto t -> head_beta_reduce ~upto t); + NCicPp.set_head_beta_reduce (fun ~upto t -> head_beta_reduce ~upto t); +;; + + + + (* vim:set foldmethod=marker: *)