module E = BagEnvironment
module S = BagSubstitution
-exception TypeError of B.message
-
type machine = {
i: int;
c: B.context;
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 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)
+ L.log O.specs level (L.ct_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
let empty_machine = {i = 0; c = B.empty_context; s = []}
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