From a981b42002f822aa49a41b3889a76b9438b093bb Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 13 Oct 2008 14:02:54 +0000 Subject: [PATCH] NCicReduction.reduce_machine returns a boolean stating if the machine is in normal form --- .../components/ng_kernel/nCicReduction.ml | 95 +++++++++++-------- .../components/ng_kernel/nCicReduction.mli | 3 +- .../software/components/ng_refiner/esempio.ma | 9 +- .../components/ng_refiner/nCicUnification.ml | 43 ++++----- 4 files changed, 83 insertions(+), 67 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index bd7cbc842..015ba007a 100644 --- a/helm/software/components/ng_kernel/nCicReduction.ml +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -20,7 +20,7 @@ module type Strategy = sig type env_term type config = int * env_term list * C.term * stack_term list val to_env : - reduce: (config -> config) -> unwind: (config -> C.term) -> + reduce: (config -> config * bool) -> unwind: (config -> C.term) -> config -> env_term val from_stack : stack_term -> config val from_stack_list_for_unwind : @@ -29,13 +29,13 @@ module type Strategy = sig val from_env_for_unwind : unwind: (config -> C.term) -> env_term -> C.term val stack_to_env : - reduce: (config -> config) -> unwind: (config -> C.term) -> + reduce: (config -> config * bool) -> unwind: (config -> C.term) -> stack_term -> env_term val compute_to_env : - reduce: (config -> config) -> unwind: (config -> C.term) -> + reduce: (config -> config * bool) -> unwind: (config -> C.term) -> int -> env_term list -> C.term -> env_term val compute_to_stack : - reduce: (config -> config) -> unwind: (config -> C.term) -> + reduce: (config -> config * bool) -> unwind: (config -> C.term) -> config -> stack_term end ;; @@ -44,7 +44,7 @@ module CallByValueByNameForUnwind' = 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 (reduce c),lazy (unwind c) + let to_env ~reduce ~unwind c = lazy (fst (reduce c)),lazy (unwind c) let from_stack (c,_) = Lazy.force c let from_stack_list_for_unwind ~unwind:_ l = List.map (function (_,c) -> Lazy.force c) l @@ -52,9 +52,9 @@ module CallByValueByNameForUnwind' = struct 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 (reduce (k,e,t,[])), lazy (unwind (k,e,t,[])) + lazy (fst (reduce (k,e,t,[]))), lazy (unwind (k,e,t,[])) let compute_to_stack ~reduce ~unwind config = - lazy (reduce config), lazy (unwind config) + lazy (fst (reduce config)), lazy (unwind config) end ;; @@ -82,7 +82,7 @@ module Reduction(RS : Strategy) = struct | _,_ -> assert false ;; - let rec reduce ~delta ?(subst = []) context : config -> config = + 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 @@ -91,16 +91,16 @@ module Reduction(RS : Strategy) = struct let x= try Some (List.nth context (n - 1 - k)) with Failure _ -> None in (match x with | Some(_,C.Def(x,_)) -> aux (0,[],NCicSubstitution.lift (n - k) x,s) - | _ -> config) + | _ -> config, true) | (k, e, C.Meta (n,l), s) as config -> (try let _,_, term,_ = NCicUtils.lookup_subst n subst in aux (k, e, NCicSubstitution.subst_meta l term,s) - with NCicUtils.Subst_not_found _ -> config) + with NCicUtils.Subst_not_found _ -> config, true) | (_, _, C.Implicit _, _) -> assert false | (_, _, C.Sort _, _) | (_, _, C.Prod _, _) - | (_, _, C.Lambda _, []) as config -> config + | (_, _, 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) | (k, e, C.LetIn (_,_,m,t), s) -> @@ -114,50 +114,59 @@ 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 else + if delta >= height then config, false else let _,_,body,_,_,_ = NCicEnvironment.get_checked_def refer in aux (0, [], body, s) | (_, _, C.Const (Ref.Ref (_, - (Ref.Decl|Ref.Ind _|Ref.Con _|Ref.CoFix _))), _) as config -> config - | (_, _, C.Const (Ref.Ref - (_,Ref.Fix (fixno,recindex,height)) as refer),s) as config -> - if delta >= height then config else + (Ref.Decl|Ref.Ind _|Ref.Con _|Ref.CoFix _))), _) as config -> + config, true + | (_, _, (C.Const (Ref.Ref + (_,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)) with Failure _ -> None with - | None -> config + | None -> config, true | Some recparam -> let fixes,_,_ = NCicEnvironment.get_checked_fixes_or_cofixes refer in match reduce ~delta:0 ~subst context recparam with - | (_,_,C.Const (Ref.Ref (_,Ref.Con _)), _) as c -> + | (_,_,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) + 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) in let _,_,_,_,body = List.nth fixes fixno in aux (0, [], body, new_s) - | _ -> config) + | _ -> config, true) | (k, e, C.Match (_,_,term,pl),s) as config -> let decofix = function | (_,_,C.Const(Ref.Ref(_,Ref.CoFix c)as refer),s)-> - let cofixes,_,_ = NCicEnvironment.get_checked_fixes_or_cofixes refer in + let cofixes,_,_ = + NCicEnvironment.get_checked_fixes_or_cofixes refer in let _,_,_,_,body = List.nth cofixes c in - reduce ~delta:0 ~subst context (0,[],body,s) + let c,_ = reduce ~delta:0 ~subst context (0,[],body,s) in + c | config -> config in - (match decofix (reduce ~delta:0 ~subst context (k,e,term,[])) with + (match decofix (fst (reduce ~delta:0 ~subst context (k,e,term,[]))) 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) + | _ -> config,true) in aux ;; let whd ?(delta=0) ?(subst=[]) context t = - unwind (reduce ~delta ~subst context (0, [], t, [])) + unwind (fst (reduce ~delta ~subst context (0, [], t, []))) ;; end @@ -301,15 +310,28 @@ let are_convertible ?(subst=[]) = | C.Appl(C.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h | _ -> 0 in - let small_delta_step (_,_,t1,_ as m1) (_,_,t2,_ as m2) = - let h1 = height_of t1 in - let h2 = height_of t2 in - let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in - R.reduce ~delta ~subst context m1, - R.reduce ~delta ~subst context m2, - delta + let put_in_whd m1 m2 = + R.reduce ~delta:max_int ~subst context m1, + R.reduce ~delta:max_int ~subst context m2 + in + let small_delta_step + ((_,_,t1,_ as m1), norm1 as x1) ((_,_,t2,_ as m2), norm2 as x2) + = + assert(not (norm1 && norm2)); + if norm1 then + x1, R.reduce ~delta:(height_of t2 -1) ~subst context m2 + else if norm2 then + R.reduce ~delta:(height_of t1 -1) ~subst context m1, x2 + else + let h1 = height_of t1 in + let h2 = height_of t2 in + let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in + R.reduce ~delta ~subst context m1, + R.reduce ~delta ~subst context m2 in - let rec convert_machines ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),delta) = + let rec convert_machines + ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2), norm2 as m2) + = (alpha_eq test_eq_only (R.unwind (k1,e1,t1,[])) (R.unwind (k2,e2,t2,[])) && let relevance = @@ -322,14 +344,11 @@ let are_convertible ?(subst=[]) = not b || let t1 = RS.from_stack t1 in let t2 = RS.from_stack t2 in - convert_machines (small_delta_step t1 t2)) s1 s2 true relevance + convert_machines (put_in_whd t1 t2)) s1 s2 true relevance with Invalid_argument _ -> false) || - (delta > 0 && - let delta = delta - 1 in - let red = R.reduce ~delta ~subst context in - convert_machines (red m1,red m2,delta)) + (not (norm1 && norm2) && convert_machines (small_delta_step m1 m2)) in - convert_machines (small_delta_step (0,[],t1,[]) (0,[],t2,[])) + convert_machines (put_in_whd (0,[],t1,[]) (0,[],t2,[])) in aux false ;; diff --git a/helm/software/components/ng_kernel/nCicReduction.mli b/helm/software/components/ng_kernel/nCicReduction.mli index 4828fbc2b..c80da989d 100644 --- a/helm/software/components/ng_kernel/nCicReduction.mli +++ b/helm/software/components/ng_kernel/nCicReduction.mli @@ -36,7 +36,8 @@ type environment_item type machine = int * environment_item list * NCic.term * stack_item list val reduce_machine : - delta:int -> ?subst:NCic.substitution -> NCic.context -> machine -> machine + delta:int -> ?subst:NCic.substitution -> NCic.context -> machine -> + machine * bool val from_stack : stack_item -> machine val unwind : machine -> NCic.term diff --git a/helm/software/components/ng_refiner/esempio.ma b/helm/software/components/ng_refiner/esempio.ma index d0f6a2e86..8f9604a85 100644 --- a/helm/software/components/ng_refiner/esempio.ma +++ b/helm/software/components/ng_refiner/esempio.ma @@ -17,6 +17,13 @@ include "nat/plus.ma". definition hole : ∀A:Type.A → A ≝ λA.λx.x. definition id : ∀A:Type.A → A ≝ λA.λx.x. +(* Common case in dama, reduction with metas +inductive list : Type := nil : list | cons : nat -> list -> list. +let rec len l := match l with [ nil => O | cons _ l => S (len l) ]. +axiom lt : nat -> nat -> Prop. +axiom foo : ∀x. Not (lt (hole ? x) (hole ? O)) = (lt x (len nil) -> False). +*) + (* meta1 Vs meta2 with different contexts axiom foo: ∀P:Type.∀f:P→P→Prop.∀x:P. @@ -49,7 +56,7 @@ axiom foo: *) alias num (instance 0) = "natural number". -axiom foo: (12+12) = (12+11). +axiom foo: (100+111) = (100+110). (id ?(id ?(id ?(id ? (100+100))))) = diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index bfa8fff47..d34e3efcc 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -385,35 +385,26 @@ and unify test_eq_only metasenv subst context t1 t2 = in let put_in_whd m1 m2 = NCicReduction.reduce_machine ~delta:max_int ~subst context m1, - NCicReduction.reduce_machine ~delta:max_int ~subst context m2, - false (* not in normal form *) + NCicReduction.reduce_machine ~delta:max_int ~subst context m2 in - let small_delta_step (_,_,t1,_ as m1) (_,_,t2,_ as m2) = + let small_delta_step + ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2) + = + assert (not (norm1 && norm2)); + if norm1 then + x1,NCicReduction.reduce_machine ~delta:(height_of t2 -1) ~subst context m2 + else if norm2 then + NCicReduction.reduce_machine ~delta:(height_of t1 -1) ~subst context m1,x2 + else let h1 = height_of t1 in let h2 = height_of t2 in - let delta = - if flexible [t1] then max 0 (h2 - 1) else - if flexible [t2] then max 0 (h1 - 1) else - if h1 = h2 then max 0 (h1 -1) else min h1 h2 - in - pp (lazy("DELTA STEP TO: " ^ string_of_int delta)); - let m1' = NCicReduction.reduce_machine ~delta ~subst context m1 in - let m2' = NCicReduction.reduce_machine ~delta ~subst context m2 in - if (m1' == m1 && m2' == m2 && delta > 0) then - (* if we have as heads a Fix of height n>m>0 and another term of height - * m, we set delta = m. The Fix may or may not reduce, depending on its - * rec argument. if no reduction was performed we decrease delta to m-1 - * to reduce the other term *) - let delta = delta - 1 in - pp (lazy("DELTA STEP TO: " ^ string_of_int delta)); - let m1' = NCicReduction.reduce_machine ~delta ~subst context m1 in - let m2' = NCicReduction.reduce_machine ~delta ~subst context m2 in - m1', m2', (m1 == m1' && m2 == m2') (* || delta = 0 *) - else m1', m2', (m1 == m1' && m2 == m2') (* delta = 0 *) + let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in + NCicReduction.reduce_machine ~delta ~subst context m1, + NCicReduction.reduce_machine ~delta ~subst context m2 in let rec unif_machines metasenv subst = function - | ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),are_normal) -> + | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) -> (* (*D*) inside 'M'; try let rc = *) (* pp (lazy((if are_normal then "*" else " ") ^ " " ^ @@ -447,10 +438,8 @@ and unify test_eq_only metasenv subst context t1 t2 = (NCicReduction.unwind (k2,e2,t2,List.rev l2)) in try check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst) - with UnificationFailure _ | Uncertain _ when not are_normal -> - let m1,m2,normal as small = small_delta_step m1 m2 in - if not normal then unif_machines metasenv subst small - else raise (UnificationFailure (lazy "TEST x")) + with UnificationFailure _ | Uncertain _ when not (norm1 && norm2) -> + unif_machines metasenv subst (small_delta_step m1 m2) (* (*D*) in outside(); rc with exn -> outside (); raise exn *) in try fo_unif test_eq_only metasenv subst t1 t2 -- 2.39.2