X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicReduction.ml;h=2b1d4119b51b4ec6d7b9206d289a704d2d4bc383;hb=ffdd3ddd6ce10a5fa0729ab407647bd46c44b9d8;hp=015ba007a311a8fb6491c84c58034215d92b6173;hpb=a981b42002f822aa49a41b3889a76b9438b093bb;p=helm.git diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index 015ba007a..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, []))) ;; @@ -180,12 +184,12 @@ let whd = R.whd let (===) x y = Pervasives.compare x y = 0 ;; -let get_relevance = ref (fun ~subst:_ _ _ -> assert false);; +let get_relevance = ref (fun ~metasenv:_ ~subst:_ _ _ -> assert false);; let set_get_relevance f = get_relevance := f;; (* t1, t2 must be well-typed *) -let are_convertible ?(subst=[]) = +let are_convertible ~metasenv ~subst = let rec aux test_eq_only context t1 t2 = let alpha_eq test_eq_only t1 t2 = if t1 === t2 then @@ -221,7 +225,12 @@ let are_convertible ?(subst=[]) = (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2)) l1 l2 - with Invalid_argument _ -> assert false) -> true + with Invalid_argument "List.for_all2" -> + prerr_endline ("Meta " ^ string_of_int n1 ^ + " occurrs with local contexts of different lenght\n"^ + NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^ + NCicPp.ppterm ~metasenv ~subst ~context t2); + assert false) -> true | C.Meta (n1,l1), _ -> (try @@ -248,11 +257,12 @@ let are_convertible ?(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 -> - let relevance = !get_relevance ~subst context hd1 tl1 in + let relevance = + !get_relevance ~metasenv ~subst context hd1 tl1 in let _,relevance = HExtlib.split_nth fail relevance in let b,relevance = (match relevance with | [] -> assert false @@ -262,17 +272,17 @@ let are_convertible ?(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) | (C.Appl (hd1::tl1), C.Appl (hd2::tl2)) -> aux test_eq_only context hd1 hd2 && - let relevance = !get_relevance ~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 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) @@ -329,7 +339,7 @@ let are_convertible ?(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 @@ -344,33 +354,41 @@ let are_convertible ?(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 @@ -381,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: *)