- siimplifified RTM (one register less) now counts x-steps.

[helm.git] / helm / software / helena / src / basic_rg / brgType.ml

diff --git a/helm/software/helena/src/basic_rg/brgType.ml b/helm/software/helena/src/basic_rg/brgType.ml
index fd06282fe886f5e922350fef0f87d56201bb5cc7..929dcbce85457955f7d7c4b9e9d8bda1141d9b79 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgType.ml
+++ b/helm/software/helena/src/basic_rg/brgType.ml
@@ -57,76 +57,75 @@ let assert_convertibility err f st m u w v =
 
 let assert_applicability err f st m u w v =
    match BR.xwhd st m None u with 
-      | _, B.Sort _                      ->
+      | _, B.Sort _                            ->
          error1 err "not a function type" m u
-      | mu, B.Bind (_, B.Abst (n, u), _) -> 
+      | mu, B.Bind (_, B.Abst (true, n, u), _) -> 
          if !G.cc && not (N.assert_not_zero st n) then error1 err "not a function type" m u else 
          if BR.are_convertible st mu zero u m zero w then f () else
         error3 err m v w ~mu u
-      | _                                -> assert false (**)
+      | _                                      -> assert false (**)
 
-let rec b_type_of err f st m x =
-   if !G.trace >= level then log1 st "Now checking" m x;
-   match x with
-   | B.Sort (a, h)           ->
-      let h = H.apply h in f x (B.Sort (a, h)) 
-   | B.LRef (_, i)           ->
+let rec b_type_of err f st m r =
+   if !G.trace >= level then log1 st "Now checking" m r;
+   match r with
+   | B.Sort (a, h)                   ->
+      let h = H.apply h in f r (B.Sort (a, h)) 
+   | B.LRef (_, i)                   ->
       begin match BR.get m i with
-         | B.Abst (_, w)     ->
-           f x (BS.lift (succ i) (0) w)
+         | B.Abst (_, _, w)          ->
+           f r (BS.lift (succ i) (0) w)
         | B.Abbr (B.Cast (_, w, _)) -> 
-           f x (BS.lift (succ i) (0) w)
+           f r (BS.lift (succ i) (0) w)
         | B.Abbr _                  -> assert false
         | B.Void                    -> 
-           error1 err "reference to excluded variable" m x
+           error1 err "reference to excluded variable" m r
       end
-   | B.GRef (_, uri)         ->
+   | B.GRef (_, uri)                 ->
       begin match BE.get_entity uri with
-         | _, _, _, E.Abst w                  -> f x w
-        | _, _, _, E.Abbr (B.Cast (_, w, _)) -> f x w
+         | _, _, _, E.Abst w                  -> f r w
+        | _, _, _, E.Abbr (B.Cast (_, w, _)) -> f r w
         | _, _, _, E.Abbr _                  -> assert false
         | _, _, _, E.Void                    ->
-            error1 err "reference to unknown entry" m x
+            error1 err "reference to unknown entry" m r
       end
-   | B.Bind (a, B.Abbr v, t) ->
-      let f xv xt tt =
-         f (S.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt)
+   | B.Bind (a, B.Abbr v, t)         ->
+      let f rv rt tt =
+         f (S.sh2 v rv t rt r (B.bind_abbr a)) (B.bind_abbr a rv tt)
       in
-      let f xv m = b_type_of err (f xv) st m t in
-      let f xv = f xv (BR.push m a (B.abbr xv)) in
-      let f xv vv = match xv with 
-        | B.Cast _ -> f xv
-         | _        -> f (B.Cast (E.empty_node, vv, xv))
+      let f rv m = b_type_of err (f rv) st m t in
+      let f rv = f rv (BR.push m a (B.abbr rv)) in
+      let f rv vv = match rv with 
+        | B.Cast _ -> f rv
+         | _        -> f (B.Cast (E.empty_node, vv, rv))
       in
       type_of err f st m v
-   | B.Bind (a, B.Abst (n, u), t) ->
-      let f xu xt tt =
-        f (S.sh2 u xu t xt x (B.bind_abst n a)) (B.bind_abst (N.minus st n 1) a xu tt)
+   | B.Bind (a, B.Abst (x, n, u), t) ->
+      let f ru rt tt =
+        f (S.sh2 u ru t rt r (B.bind_abst x n a)) (B.bind_abst x (N.minus st n 1) a ru tt)
       in
-      let f xu m = b_type_of err (f xu) st m t in
-      let f xu _ = f xu (BR.push m a (B.abst n xu)) in
+      let f ru m = b_type_of err (f ru) st m t in
+      let f ru _ = f ru (BR.push m a (B.abst x n ru)) in
       type_of err f st m u
-   | B.Bind (a, B.Void, t)   ->
-      let f xt tt = 
-         f (S.sh1 t xt x (B.bind_void a)) (B.bind_void a tt)
+   | B.Bind (a, B.Void, t)           ->
+      let f rt tt = 
+         f (S.sh1 t rt r (B.bind_void a)) (B.bind_void a tt)
       in
       b_type_of err f st (BR.push m a B.Void) t
-         
-   | B.Appl (a, v, t)        ->
-      let f xv vv xt tt = 
-         let f _ = f (S.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt) in
-         assert_applicability err f st m tt vv xv
+   | B.Appl (a, v, t)                ->
+      let f rv vv rt tt = 
+         let f _ = f (S.sh2 v rv t rt r (B.appl a)) (B.appl a rv tt) in
+         assert_applicability err f st m tt vv rv
       in
-      let f xv vv = b_type_of err (f xv vv) st m t in
+      let f rv vv = b_type_of err (f rv vv) st m t in
       type_of err f st m v
-   | B.Cast (a, u, t)        ->
-      let f xu xt tt =  
-        let f _ = f (S.sh2 u xu t xt x (B.cast a)) xu in
-         assert_convertibility err f st m xu tt xt
+   | B.Cast (a, u, t)                ->
+      let f ru rt tt =  
+        let f _ = f (S.sh2 u ru t rt r (B.cast a)) ru in
+         assert_convertibility err f st m ru tt rt
       in
-      let f xu _ = b_type_of err (f xu) st m t in
+      let f ru _ = b_type_of err (f ru) st m t in
       type_of err f st m u
 
 (* Interface functions ******************************************************)
 
-and type_of err f st m x = b_type_of err f st m x
+and type_of err f st m r = b_type_of err f st m r