- basic_rg: architectural bug fix

[helm.git] / helm / software / lambda-delta / basic_rg / brgType.ml

diff --git a/helm/software/lambda-delta/basic_rg/brgType.ml b/helm/software/lambda-delta/basic_rg/brgType.ml
index 60b5b75bcc54d540a5d063e8d9aaba1aac9b38b4..fd240994543168287d2c42353561d664d36c3171 100644 (file)
--- a/helm/software/lambda-delta/basic_rg/brgType.ml
+++ b/helm/software/lambda-delta/basic_rg/brgType.ml
@@ -15,46 +15,48 @@ module O = BrgOutput
 module E = BrgEnvironment
 module R = BrgReduction
 
-exception TypeError of (R.context, B.term) Log.item list
+exception TypeError of B.message
 
 (* Internal functions *******************************************************)
 
+let level = 4
+
 let error1 s c t =
    raise (TypeError (L.ct_items1 s c t))
 
 let error2 s1 c1 t1 s2 c2 t2 =
    raise (TypeError (L.ct_items2 s1 c1 t1 s2 c2 t2))
 
-let are_convertible f c t1 t2 =
-   L.log O.specs 4 (L.ct_items2 "Now converting" c t1 "and" c t2);
-   R.are_convertible f c t1 t2
-
 (* Interface functions ******************************************************)
 
 let rec type_of f g c x = 
-   L.log O.specs 5 (L.ct_items1 "now checking" c x);
+   L.log O.specs level (L.ct_items1 "now checking" c x);
    match x with
    | B.Sort h                 -> f (B.Sort (g h))
    | B.LRef i                 ->
       let f = function
-         | B.Abst w               -> f w
-        | B.Abbr (B.Cast (w, v)) -> f w
-        | B.Abbr _               -> assert false
-        | B.Void                 -> assert false
+         | Some (_, B.Abst w)               -> f w
+        | Some (_, B.Abbr (B.Cast (w, v))) -> f w
+        | Some (_, B.Abbr _)               -> assert false
+        | Some (_, B.Void)                 -> 
+           error1 "reference to excluded variable" c x
+         | None                             ->
+           error1 "variable not found" c x      
       in
-      R.get f c i
+      B.get f c i
    | B.GRef uri               ->
       let f = function
          | _, _, B.Abst w               -> f w
         | _, _, B.Abbr (B.Cast (w, v)) -> f w
         | _, _, B.Abbr _               -> assert false
-        | _, _, B.Void                 -> assert false
+        | _, _, B.Void                 ->
+           error1 "reference to excluded object" c x
       in
       E.get_obj f uri
    | B.Bind (id, B.Abbr u, t) ->
       let f tt = f (B.Bind (id, B.Abbr u, tt)) in
       let f cc = type_of f g cc t in
-      let f u = R.push f c (B.Abbr u) in
+      let f u = B.push f c id (B.Abbr u) in
       let f uu = match u with 
         | B.Cast _ -> f u
          | _        -> f (B.Cast (uu, u))
@@ -63,21 +65,22 @@ let rec type_of f g c x =
    | B.Bind (id, B.Abst u, t) ->
       let f tt = f (B.Bind (id, B.Abst u, tt)) in
       let f cc = type_of f g cc t in
-      let f _ = R.push f c (B.Abst u) in
+      let f _ = B.push f c id (B.Abst u) in
       type_of f g c u
    | B.Bind (id, B.Void, t)   ->
       let f tt = f (B.Bind (id, B.Void, tt)) in
       let f cc = type_of f g cc t in
-      R.push f c B.Void
+      B.push f c id B.Void
    | B.Appl (v, t)            ->
       let f tt cc = function
          | R.Sort _ -> error1 "not a function" c t
         | R.Abst w -> 
+            L.log O.specs (succ level) (L.ct_items1 "Just scanned" cc w);
            let f b =
               if b then f (B.Appl (v, tt)) else
               error2 "the term" c v "must be of type" cc w
            in
-           type_of (are_convertible f cc w) g c v
+           type_of (R.are_convertible f cc w) g c v
       in
       let f tt = R.ho_whd (f tt) c t in
       type_of f g c t 
@@ -86,5 +89,5 @@ let rec type_of f g c x =
          if b then f u else
         error2 "the term" c t "must be of type" c u
       in
-      let f _ = type_of (are_convertible f c u) g c t in
+      let f _ = type_of (R.are_convertible f c u) g c t in
       type_of f g c u