X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fbasic_rg%2FbrgReduction.ml;h=4a1667862d373d63f057ec592053bf09196adf07;hb=f983656c56d37a50536e50a319114dbfa592c9a0;hp=8ad752bada79e9a85688362c2f8a6b26064d2e5f;hpb=dcdee4ca839dac671924a95f0ada71faf06a8be4;p=helm.git

diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.ml b/helm/software/lambda-delta/basic_rg/brgReduction.ml
index 8ad752bad..4a1667862 100644
--- a/helm/software/lambda-delta/basic_rg/brgReduction.ml
+++ b/helm/software/lambda-delta/basic_rg/brgReduction.ml
@@ -12,193 +12,200 @@
 module U = NUri
 module C = Cps
 module L = Log
+module P = Output
 module B = Brg
 module O = BrgOutput
 module E = BrgEnvironment
-module S = BrgSubstitution
 
-exception LRefNotFound of B.message
+exception TypeError of B.message
 
 type machine = {
    c: B.context;
-   s: (B.term * int) list
+   s: (B.context * B.term) list;
+   i: int
 }
 
 (* Internal functions *******************************************************)
 
-let reductions = ref O.initial_reductions
-
 let level = 5
 
-let error i = raise (LRefNotFound (L.items1 (string_of_int i)))
-
 let log1 s c t =
    let sc, st = s ^ " in the context", "the term" in
    L.log O.specs level (L.ct_items1 sc c st t)
 
-let log2 s c u t =
-   let sc, su, st = s ^ " in the context", "the term", "and the term" in
-   L.log O.specs level (L.ct_items2 sc c su u st t)
+let log2 s cu u ct t =
+   let s1, s2, s3 = s ^ " in the context", "the term", "and in the context" in
+   L.log O.specs level (L.ct_items2 s1 cu s2 u s3 ct s2 t)
 
-let empty_machine = {
-   c = B.empty_context; s = []
-}
+let error0 i = 
+   let s = Printf.sprintf "local reference not found %u" i in
+   raise (TypeError (L.items1 s))
+
+let error1 st c t =
+   let sc = "In the context" in
+   raise (TypeError (L.ct_items1 sc c st t))
 
-let get f c m i =
-   let f e = function
-      | Some (_, b) -> f e b
-      | None        -> error i
+let error3 c t1 t2 t3 =
+   let sc, st1, st2, st3 = 
+      "In the context", "the term", "is of type", "but must be of type"
    in
-   let f c = B.get f c i in
-   B.append f c m.c
+   raise (TypeError (L.ct_items3 sc c st1 t1 st2 t2 st3 t3))
 
-let lift_stack f s =
-   let map f (v, i) = f (v, succ i) in
-   Cps.list_map f map s
+let err () = assert false
 
-let unwind_to_term f m t =
-   let map f t (a, b) = f (B.Bind (a, b, t)) in
-   let f mc = C.list_fold_left f map t mc in
-   assert (m.s = []);
-   B.contents f m.c
-
-let push f m a b = 
-   assert (m.s = []);
-   f {m with c = (a, b) :: m.c}
+let get f m i =
+   B.get error0 f m.c i
 
 (* to share *)
-let rec step f ?(delta=false) ?(sty=false) c m x = 
+let rec step f ?(delta=false) ?(rt=false) m x = 
 (*   L.warn "entering R.step"; *)
    match x with
-   | B.Sort _                -> f m x
+   | B.Sort _                -> f m None x
    | B.GRef (a, uri)         ->
       let f = function
          | _, _, B.Abbr v when delta ->
-            reductions := O.add ~gdelta:1 !reductions;
-	    step f ~delta ~sty c m v
-         | _, _, B.Abst w when sty   ->
-	    step f ~delta ~sty c m w	 
+            P.add ~gdelta:1 ();
+	    step f ~delta ~rt m v
+         | _, _, B.Abst w when rt   ->
+            P.add ~grt:1 ();
+	    step f ~delta ~rt m w	 
 	 | e, _, b                   ->
-	    f m (B.GRef (B.Entry (e, b) :: a, uri))
+	    f m (Some (e, b)) x
       in
       E.get_obj f uri
    | B.LRef (a, i)           ->
-      let f e = function
+      let f c a = function
 	 | B.Abbr v          ->
-	    reductions := O.add ~ldelta:1 !reductions;
-	    step f ~delta ~sty c m v
-	 | B.Abst w when sty ->
-            step f ~delta ~sty c m w
+	    P.add ~ldelta:1 ();
+	    step f ~delta ~rt {m with c = c} v
+	 | B.Abst w when rt ->
+            P.add ~lrt:1 ();
+            step f ~delta ~rt {m with c = c} w
+	 | B.Void            ->
+	    f {m with c = c} None x
 	 | b                 ->
-	    f m (B.LRef (B.Entry (e, b) :: a, i))
-      in
-      let f e = S.lift_bind (f e) (succ i) (0) in 
-      get f c m i
+	    let f e = f {m with c = c} (Some (e, b)) x in 
+	    B.apix err f a
+      in 
+      get f m i
    | B.Cast (_, _, t)        ->
-      reductions := O.add ~tau:1 !reductions;
-      step f ~delta ~sty c m t
+      P.add ~tau:1 ();
+      step f ~delta ~rt m t
    | B.Appl (_, v, t)        ->
-      step f ~delta ~sty c {m with s = (v, 0) :: m.s} t   
-   | B.Bind (a, B.Abst w, t) -> 
+      step f ~delta ~rt {m with s = (m.c, v) :: m.s} t   
+   | B.Bind (a, B.Abst w, t) ->
       begin match m.s with
-         | []           -> f m x
-	 | (v, h) :: tl -> 
-            reductions := O.add ~beta:1 !reductions;
-	    let f mc = step f ~delta ~sty c {c = mc; s = tl} t in
-	    let f v = B.push f m.c a (B.Abbr (B.Cast ([], w, v))) in
-	    S.lift f h (0) v
+         | []          -> f m None x
+	 | (c, v) :: s ->
+            P.add ~beta:1 ~upsilon:(List.length s) ();
+	    let f c = step f ~delta ~rt {m with c = c; s = s} t in 
+	    B.push f m.c ~c a (B.Abbr v) (* (B.Cast ([], w, v)) *)
       end
-   | B.Bind (a, b, t)        -> 
-      reductions := O.add ~upsilon:(List.length m.s) !reductions;
-      let f sc mc = step f ~delta ~sty c {c = mc; s = sc} t in
-      let f sc = B.push (f sc) m.c a b in
-      lift_stack f m.s
+   | B.Bind (a, b, t)        ->
+      P.add ~upsilon:(List.length m.s) ();
+      let f c = step f ~delta ~rt {m with c = c} t in
+      B.push f m.c ~c:m.c a b
 
-(* Interface functions ******************************************************)
-   
-let domain f c t =
+let domain f m t =
    let f r = L.unbox level; f r in
-   let f m = function
-      | B.Bind (_, B.Abst w, _) ->
-         let f w = f (Some w) in unwind_to_term f m w
-      | x                       -> f None
+   let f m _ = function
+      | B.Bind (_, B.Abst w, _) -> f m w
+      | _                       -> error1 "not a function" m.c t
    in
-   L.box level; log1 "Now scanning" c t;
-   step f ~delta:true ~sty:true c empty_machine t
-
-let rec ac_nfs f ~si r c m1 u m2 t =
-(*   L.warn "entering R.are_convertible_aux"; *)
-   log2 "Now converting nfs" c u t;
-   match u, t with
-      | B.Sort (_, h1), B.Sort (_, h2)             ->
+   L.box level; log1 "Now scanning" m.c t;
+   step f ~delta:true ~rt:true m t
+
+let push f m a b = 
+   assert (m.s = []);
+   let a, i = match b with
+      | B.Abst _ -> B.Apix m.i :: a, succ m.i
+      | _        -> a, m.i
+   in
+   let f c = f {m with c = c; i = i} in
+   B.push f m.c ~c:m.c a b
+
+let rec ac_nfs f ~si r m1 a1 u m2 a2 t =
+   log2 "Now converting nfs" m1.c u m2.c t;
+   match a1, u, a2, t with
+      | _, B.Sort (_, h1), 
+        _, B.Sort (_, h2)                                ->
          if h1 = h2 then f r else f false 
-      | B.LRef (B.Entry (e1, B.Abst _) :: _, _), 
-        B.LRef (B.Entry (e2, B.Abst _) :: _, _)    ->
-	 if e1 = e2 then ac_stacks f ~si r c m1 m2 else f false
-      | B.GRef (B.Entry (e1, B.Abst _) :: _, _), 
-        B.GRef (B.Entry (e2, B.Abst _) :: _, _)    ->
-	 if e1 = e2 then ac_stacks f ~si r c m1 m2 else f false
-      | B.GRef (B.Entry (e1, B.Abbr v1) :: _, _), 
-        B.GRef (B.Entry (e2, B.Abbr v2) :: _, _)   ->
+      | Some (e1, B.Abst _), _, Some (e2, B.Abst _), _   ->
+	 if e1 = e2 then ac_stacks f ~si r m1 m2 else f false
+      | Some (e1, B.Abbr v1), _, Some (e2, B.Abbr v2), _ ->
          if e1 = e2 then
 	    let f r = 
 	       if r then f r 
 	       else begin  
-                  reductions := O.add ~gdelta:2 !reductions;
-	          ac f ~si true c m1 v1 m2 v2
+                  P.add ~gdelta:2 ();
+	          ac f ~si true m1 v1 m2 v2
 	       end
 	    in
-	    ac_stacks f ~si r c m1 m2
+	    ac_stacks f ~si r m1 m2
 	 else if e1 < e2 then begin 
-            reductions := O.add ~gdelta:1 !reductions;
-	    step (ac_nfs f ~si r c m1 u) c m2 v2
+            P.add ~gdelta:1 ();
+	    step (ac_nfs f ~si r m1 a1 u) m2 v2
 	 end else begin
-	    reductions := O.add ~gdelta:1 !reductions;
-	    step (ac_nfs_rev f ~si r c m2 t) c m1 v1
+	    P.add ~gdelta:1 ();
+	    step (ac_nfs_rev f ~si r m2 a2 t) m1 v1
          end
-      | _, B.GRef (B.Entry (_, B.Abbr v2) :: _, _) ->
-         reductions := O.add ~gdelta:1 !reductions;
-         step (ac_nfs f ~si r c m1 u) c m2 v2      
-      | B.GRef (B.Entry (_, B.Abbr v1) :: _, _), _ ->
-         reductions := O.add ~gdelta:1 !reductions;
-	 step (ac_nfs_rev f ~si r c m2 t) c m1 v1            
-      | B.Bind (a1, (B.Abst w1 as b1), t1), 
-        B.Bind (a2, (B.Abst w2 as b2), t2)         ->
-	 let g m1 m2 = ac f ~si r c m1 t1 m2 t2 in
+      | _, _, Some (_, B.Abbr v2), _                     ->
+         P.add ~gdelta:1 ();
+         step (ac_nfs f ~si r m1 a1 u) m2 v2      
+      | Some (_, B.Abbr v1), _, _, _                     ->
+         P.add ~gdelta:1 ();
+	 step (ac_nfs_rev f ~si r m2 a2 t) m1 v1            
+      | _, B.Bind (a1, (B.Abst w1 as b1), t1), 
+        _, B.Bind (a2, (B.Abst w2 as b2), t2)            ->
+	 let g m1 m2 = ac f ~si r m1 t1 m2 t2 in
          let g m1 = push (g m1) m2 a2 b2 in 
 	 let f r = if r then push g m1 a1 b1 else f false in
-	 ac f ~si r c m1 w1 m2 w2      
-      | B.Sort _, B.Bind (a, b, t) when si         ->
-	 let f m1 m2 = ac f ~si r c m1 u m2 t in
+	 ac f ~si r m1 w1 m2 w2      
+      | _, B.Sort _, _, B.Bind (a, b, t) when si         ->
+	 P.add ~si:1 ();
+	 let f m1 m2 = ac f ~si r m1 u m2 t in
 	 let f m1 = push (f m1) m2 a b in
 	 push f m1 a b
-      | _                                          -> f false
+      | _                                                -> f false
 
-and ac_nfs_rev f ~si r c m2 t m1 u = ac_nfs f ~si r c m1 u m2 t
+and ac_nfs_rev f ~si r m2 a2 t m1 a1 u = ac_nfs f ~si r m1 a1 u m2 a2 t
 
-and ac f ~si r c m1 t1 m2 t2 =
+and ac f ~si r m1 t1 m2 t2 =
 (*   L.warn "entering R.are_convertible"; *)
-   let g m1 t1 = step (ac_nfs f ~si r c m1 t1) c m2 t2 in 
-   if r = false then f false else step g c m1 t1
+   let g m1 a1 t1 = step (ac_nfs f ~si r m1 a1 t1) m2 t2 in 
+   if r = false then f false else step g m1 t1
 
-and ac_stacks f ~si r c m1 m2 =
+and ac_stacks f ~si r m1 m2 =
 (*   L.warn "entering R.are_convertible_stacks"; *)
-   let mm1, mm2 = {m1 with s = []}, {m2 with s = []} in
-   let map f r (v1, h1) (v2, h2) =
-      let f v1 = S.lift (ac f ~si r c mm1 v1 mm2) h2 (0) v2 in
-      S.lift f h1 (0) v1
+   if List.length m1.s <> List.length m2.s then f false else
+   let map f r (c1, v1) (c2, v2) =
+      let m1, m2 = {m1 with c = c1; s = []}, {m2 with c = c2; s = []} in
+      ac f ~si r m1 v1 m2 v2
    in
-   if List.length m1.s <> List.length m2.s then 
-      begin 
-(*         L.warn (Printf.sprintf "Different lengths: %u %u"
-	    (List.length m1.s) (List.length m2.s) 
-	 ); *)
-	 f false
-      end
-   else
-      C.list_fold_left2 f map r m1.s m2.s
+   C.list_fold_left2 f map r m1.s m2.s
+
+(* Interface functions ******************************************************)
+
+let empty_machine = { 
+   c = B.empty_context; s = []; i = 0
+}
 
-let are_convertible f ?(si=false) c u t = 
+let get f m i =
+   assert (m.s = []);
+   let f c = f in
+   get f m i
+
+let assert_conversion f ?(si=false) ?(rt=false) mw u w v = 
    let f b = L.unbox level; f b in
-   L.box level; log2 "Now converting" c u t;
-   ac f ~si true c empty_machine u empty_machine t
+   let f mu u =
+      let f = function
+         | true  -> f ()
+         | false -> error3 mw.c v w u
+      in
+      L.box level; log2 "Now converting" mu.c u mw.c w;
+      ac f ~si true mu u mw w
+   in
+   if rt then domain f mw u else f mw u
+
+let message1 st m t =
+   L.ct_items1 "In the context" m.c st t