X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicReduction.ml;h=1815ceedfcf5c87e9d387068ffbfb039c76763ff;hb=32d3f10c1904d450ce8ea3525230acc6980a5601;hp=7dbe379e4144f77801abfd6631cfdeaec547391d;hpb=002d456397be2f0046bb50356e80816f7296647d;p=helm.git diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index 7dbe379e4..1815ceedf 100644 --- a/helm/software/components/ng_kernel/nCicReduction.ml +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -15,6 +15,8 @@ module C = NCic module Ref = NReference module E = NCicEnvironment +exception AssertFailure of string Lazy.t;; + module type Strategy = sig type stack_term type env_term @@ -114,7 +116,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,13 +158,15 @@ 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 ;; @@ -253,7 +259,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 +274,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 +284,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 +341,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 +356,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 +401,19 @@ 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); +;; + +(* if n < 0, then splits all prods from an arity, returning a sort *) +let rec split_prods ~subst context n te = + match (n, R.whd ~subst context te) with + | (0, _) -> context,te + | (n, C.Sort _) when n <= 0 -> context,te + | (n, C.Prod (name,so,ta)) -> + split_prods ~subst ((name,(C.Decl so))::context) (n - 1) ta + | (_, _) -> raise (AssertFailure (lazy "split_prods")) +;; + (* vim:set foldmethod=marker: *)