NCicReduction.reduce_machine returns a boolean stating if the machine is in normal...

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index bd7cbc842b1ad79bea25b565bd7b25faedf99168..015ba007a311a8fb6491c84c58034215d92b6173 100644 (file)
--- 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 4828fbc2b5e8b56d804be26c6d0f90f4325c15c5..c80da989d73c3bc53e29477de4df5e9b48e2e66d 100644 (file)
--- 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 d0f6a2e8692f5c64d84ef44779817dfb733af925..8f9604a8524817acdbc1489a7613b43239981310 100644 (file)
--- 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 bfa8fff4758db1c620b7e5cc0fd40832f113a1b0..d34e3efcc00abb6a485ecafe1de844b8ea9f902d 100644 (file)
--- 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