some interfaces improved

[helm.git] / helm / software / lambda-delta / basic_ag / bagReduction.ml

diff --git a/helm/software/lambda-delta/basic_ag/bagReduction.ml b/helm/software/lambda-delta/basic_ag/bagReduction.ml
index 4e147ae6d247f5fb6b34faddd07ab598098a8e9b..b7eb88f6395ee4f3fd0a5dbb24f4d6d9450b8907 100644 (file)
--- a/helm/software/lambda-delta/basic_ag/bagReduction.ml
+++ b/helm/software/lambda-delta/basic_ag/bagReduction.ml
@@ -12,23 +12,22 @@
 module U = NUri
 module C = Cps
 module L = Log
+module Y = Entity
 module B = Bag
 module O = BagOutput
 module E = BagEnvironment
 module S = BagSubstitution
 
-exception TypeError of B.message
-
 type machine = {
    i: int;
-   c: B.context;
+   c: B.lenv;
    s: B.term list
 }
 
 type whd_result =
    | Sort_ of int
    | LRef_ of int * B.term option
-   | GRef_ of B.obj
+   | GRef_ of B.entity
    | Bind_ of int * B.id * B.term * B.term
 
 type ho_whd_result =
@@ -45,19 +44,15 @@ let term_of_whdr = function
 
 let level = 5
 
-let error i = 
-   let s = Printf.sprintf "local reference not found %u" i in
-   raise (TypeError (L.items1 s))
-
 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 sc, st = s ^ " in the environment", "the term" in
+   L.log O.specs level (L.et_items1 sc c 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 s1, s2, s3 = s ^ " in the environment", "the term", "and in the environment" in
+   L.log O.specs level (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
 
-let empty_machine = {i = 0; c = B.empty_context; s = []}
+let empty_machine = {i = 0; c = B.empty_lenv; s = []}
 
 let inc m = {m with i = succ m.i}
 
@@ -73,7 +68,7 @@ let unwind_stack f m =
 let get f c m i =
    let f = function
       | Some (_, b) -> f b
-      | None        -> error i
+      | None        -> assert false
    in
    let f c = B.get f c i in
    B.append f c m.c
@@ -89,8 +84,8 @@ let rec whd f c m x =
    match x with
    | B.Sort h                    -> f m (Sort_ h)
    | B.GRef uri                  ->
-      let f obj = f m (GRef_ obj) in
-      E.get_obj f uri
+      let f entry = f m (GRef_ entry) in
+      E.get_entity f uri
    | B.LRef i                    ->
       let f = function
          | B.Void   -> f m (LRef_ (i, None))
@@ -122,10 +117,10 @@ let rec ho_whd f c m x =
       | Bind_ (_, _, w, _)     -> 
          let f w = f (Abst w) in unwind_to_term f m w
       | LRef_ (_, Some w)      -> ho_whd f c m w
-      | GRef_ (_, _, B.Abst w) -> ho_whd f c m w  
-      | GRef_ (_, _, B.Abbr v) -> ho_whd f c m v
+      | GRef_ (_, _, Y.Abst w) -> ho_whd f c m w  
+      | GRef_ (_, _, Y.Abbr v) -> ho_whd f c m v
       | LRef_ (_, None)        -> assert false
-      | GRef_ (_, _, B.Void)   -> assert false
+      | GRef_ (_, _, Y.Void)   -> assert false
    in
    whd aux c m x
    
@@ -145,9 +140,11 @@ let rec are_convertible f ~si a c m1 t1 m2 t2 =
          if h1 = h2 then f a else f false 
       | LRef_ (i1, _), LRef_ (i2, _)                       ->
          if i1 = i2 then are_convertible_stacks f ~si a c m1 m2 else f false
-      | GRef_ (a1, _, B.Abst _), GRef_ (a2, _, B.Abst _)   ->
+      | GRef_ ((Y.Apix a1 :: _), _, Y.Abst _), 
+        GRef_ ((Y.Apix a2 :: _), _, Y.Abst _)              ->
          if a1 = a2 then are_convertible_stacks f ~si a c m1 m2 else f false
-      | GRef_ (a1, _, B.Abbr v1), GRef_ (a2, _, B.Abbr v2) ->
+      | GRef_ ((Y.Apix a1 :: _), _, Y.Abbr v1), 
+        GRef_ ((Y.Apix a2 :: _), _, Y.Abbr v2)             ->
          if a1 = a2 then
            let f a = 
               if a then f a else are_convertible f ~si true c m1 v1 m2 v2
@@ -156,9 +153,9 @@ let rec are_convertible f ~si a c m1 t1 m2 t2 =
         else
         if a1 < a2 then whd (aux m1 r1) c m2 v2 else
         whd (aux_rev m2 r2) c m1 v1
-      | _, GRef_ (_, _, B.Abbr v2)                         ->
+      | _, GRef_ (_, _, Y.Abbr v2)                         ->
          whd (aux m1 r1) c m2 v2
-      | GRef_ (_, _, B.Abbr v1), _                         ->
+      | GRef_ (_, _, Y.Abbr v1), _                         ->
         whd (aux_rev m2 r2) c m1 v1      
       | Bind_ (l1, id1, w1, t1), Bind_ (l2, id2, w2, t2)   ->
           let l = B.new_location () in