common/library.cmi: common/item.cmx common/hierarchy.cmi
common/library.cmo: lib/nUri.cmi common/hierarchy.cmi common/library.cmi
common/library.cmx: lib/nUri.cmx common/hierarchy.cmx common/library.cmi
-basic_rg/brg.cmo: lib/log.cmi common/item.cmx lib/cps.cmx
-basic_rg/brg.cmx: lib/log.cmx common/item.cmx lib/cps.cmx
+basic_rg/brg.cmo: lib/log.cmi common/item.cmx
+basic_rg/brg.cmx: lib/log.cmx common/item.cmx
basic_rg/brgOutput.cmi: lib/log.cmi common/item.cmx basic_rg/brg.cmx
basic_rg/brgOutput.cmo: common/output.cmi lib/nUri.cmi lib/log.cmi \
common/hierarchy.cmi lib/cps.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi
basic_rg/brgSubstitution.cmi: basic_rg/brg.cmx
basic_rg/brgSubstitution.cmo: basic_rg/brg.cmx basic_rg/brgSubstitution.cmi
basic_rg/brgSubstitution.cmx: basic_rg/brg.cmx basic_rg/brgSubstitution.cmi
-basic_rg/brgReduction.cmi: basic_rg/brg.cmx
+basic_rg/brgReduction.cmi: lib/log.cmi basic_rg/brg.cmx
basic_rg/brgReduction.cmo: common/output.cmi lib/nUri.cmi lib/log.cmi \
- lib/cps.cmx basic_rg/brgSubstitution.cmi basic_rg/brgOutput.cmi \
- basic_rg/brgEnvironment.cmi basic_rg/brg.cmx basic_rg/brgReduction.cmi
+ lib/cps.cmx basic_rg/brgOutput.cmi basic_rg/brgEnvironment.cmi \
+ basic_rg/brg.cmx basic_rg/brgReduction.cmi
basic_rg/brgReduction.cmx: common/output.cmx lib/nUri.cmx lib/log.cmx \
- lib/cps.cmx basic_rg/brgSubstitution.cmx basic_rg/brgOutput.cmx \
- basic_rg/brgEnvironment.cmx basic_rg/brg.cmx basic_rg/brgReduction.cmi
-basic_rg/brgType.cmi: common/hierarchy.cmi basic_rg/brg.cmx
+ lib/cps.cmx basic_rg/brgOutput.cmx basic_rg/brgEnvironment.cmx \
+ basic_rg/brg.cmx basic_rg/brgReduction.cmi
+basic_rg/brgType.cmi: common/hierarchy.cmi basic_rg/brgReduction.cmi \
+ basic_rg/brg.cmx
basic_rg/brgType.cmo: lib/share.cmx lib/nUri.cmi lib/log.cmi \
common/hierarchy.cmi lib/cps.cmx basic_rg/brgSubstitution.cmi \
basic_rg/brgReduction.cmi basic_rg/brgOutput.cmi \
basic_rg/brgEnvironment.cmx basic_rg/brg.cmx basic_rg/brgType.cmi
basic_rg/brgUntrusted.cmi: common/hierarchy.cmi basic_rg/brg.cmx
basic_rg/brgUntrusted.cmo: lib/log.cmi basic_rg/brgType.cmi \
- basic_rg/brgEnvironment.cmi basic_rg/brg.cmx basic_rg/brgUntrusted.cmi
+ basic_rg/brgReduction.cmi basic_rg/brgEnvironment.cmi basic_rg/brg.cmx \
+ basic_rg/brgUntrusted.cmi
basic_rg/brgUntrusted.cmx: lib/log.cmx basic_rg/brgType.cmx \
- basic_rg/brgEnvironment.cmx basic_rg/brg.cmx basic_rg/brgUntrusted.cmi
+ basic_rg/brgReduction.cmx basic_rg/brgEnvironment.cmx basic_rg/brg.cmx \
+ basic_rg/brgUntrusted.cmi
basic_ag/bag.cmo: lib/log.cmi common/item.cmx lib/cps.cmx
basic_ag/bag.cmx: lib/log.cmx common/item.cmx lib/cps.cmx
basic_ag/bagOutput.cmi: lib/log.cmi basic_ag/bag.cmx
type uri = Item.uri
type id = Item.id
+type attr = Name of bool * id (* real?, name *)
+ | Apix of int (* additional position index *)
+
+type attrs = attr list
+
type bind = Void (* exclusion *)
| Abst of term (* abstraction *)
| Abbr of term (* abbreviation *)
| Appl of attrs * term * term (* attrs, argument, function *)
| Bind of attrs * bind * term (* attrs, binder, scope *)
-and attr = Name of bool * id (* real?, name *)
- | Entry of int * bind (* age, binder *)
-
-and attrs = attr list
-
type obj = bind Item.obj (* age, uri, binder *)
type item = bind Item.item
-type context = (attrs * bind) list (* attrs, binder *)
+type context = Null
+(* Cons: tail, relative context, attrs, binder *)
+ | Cons of context * context option * attrs * bind
type message = (context, term) Log.item list
(* context handling functions ***********************************************)
-let empty_context = []
+let empty_context = Null
-let push f es a b =
- let c = (a, b) :: es in f c
+let push f es ?c a b =
+ let es = Cons (es, c, a, b) in f es
-let append f es1 es2 =
- f (List.append es2 es1)
-
-let map f map es =
- Cps.list_map f map es
-
-let contents f es = f es
-
-let get f es i =
- let rec aux e i = function
- | [] -> f e None
- | hd :: tl ->
- if i = 0 then f e (Some hd) else
- let e = match hd with _, Abst _ -> succ e | _ -> e in
- aux e (pred i) tl
+let get err f es i =
+ let rec aux j = function
+ | Null -> err i
+ | Cons (tl, None, a, b) when j = 0 -> f tl a b
+ | Cons (_, Some c, a, b) when j = 0 -> f c a b
+ | Cons (tl, _, _, _) -> aux (pred j) tl
in
- aux 0 i es
-
-let rec name f = function
- | [] -> f None
- | Name (r, n) :: _ -> f (Some (r, n))
- | _ :: tl -> name f tl
+ aux i es
+
+let rec rev_iter f map = function
+ | Null -> f ()
+ | Cons (tl, None, a, b) ->
+ let f () = map f tl a b in rev_iter f map tl
+ | Cons (tl, Some c, a, b) ->
+ let f () = map f c a b in rev_iter f map tl
+
+let rec fold_left f map x = function
+ | Null -> f x
+ | Cons (tl, _, a, b) ->
+ let f x = fold_left f map x tl in
+ map f x a b
+
+let rec name err f = function
+ | [] -> err ()
+ | Name (r, n) :: _ -> f n r
+ | _ :: tl -> name err f tl
+
+let rec apix err f = function
+ | [] -> err ()
+ | Apix i :: _ -> f i
+ | _ :: tl -> apix err f tl
module P = Printf
module F = Format
+module C = Cps
module U = NUri
module L = Log
module H = Hierarchy
| B.Sort _ ->
f {c with tsorts = succ c.tsorts; nodes = succ c.nodes}
| B.LRef (_, i) ->
- let f _ = function
- | None
- | Some (_, B.Abst _) ->
+ let err _ = f {c with tlrefs = succ c.tlrefs; nodes = succ c.nodes} in
+ let f _ _ = function
+ | B.Abst _
+ | B.Void ->
f {c with tlrefs = succ c.tlrefs; nodes = succ c.nodes}
- | Some (_, B.Abbr _)
- | Some (_, B.Void) ->
+ | B.Abbr _ ->
f {c with tlrefs = succ c.tlrefs; xnodes = succ c.xnodes}
in
- B.get f e i
+ B.get err f e i
| B.GRef (_, u) ->
let c =
if Cps.list_mem ~eq:U.eq u c.uris
| (_, _, B.Abbr v) ->
let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in
count_term f c B.empty_context v
- | (_, _, B.Void) ->
- let c = {c with evoids = succ c.evoids; xnodes = succ c.xnodes} in
+ | (_, u, B.Void) ->
+ let c = {c with
+ evoids = succ c.evoids; nodes = succ c.nodes; uris = u :: c.uris
+ } in
f c
let count_item f c = function
(* context/term pretty printing *********************************************)
let id frm a =
- let f = function
- | None -> assert false
- | Some (true, n) -> F.fprintf frm "%s" n
- | Some (false, n) -> F.fprintf frm "^%s" n
+ let err () = assert false in
+ let f n = function
+ | true -> F.fprintf frm "%s" n
+ | false -> F.fprintf frm "^%s" n
in
- B.name f a
+ B.name err f a
let rec pp_term c frm = function
| B.Sort (_, h) ->
in
H.get_sort f h
| B.LRef (_, i) ->
- let f _ = function
- | Some (a, _) -> F.fprintf frm "@[%a@]" id a
- | None -> F.fprintf frm "@[#%u@]" i
- in
- if !O.indexes then f 0 None else B.get f c i
+ let err i = F.fprintf frm "@[#%u@]" i in
+ let f _ a _ = F.fprintf frm "@[%a@]" id a in
+ if !O.indexes then err i else B.get err f c i
| B.GRef (_, s) -> F.fprintf frm "@[$%s@]" (U.string_of_uri s)
| B.Cast (_, u, t) ->
F.fprintf frm "@[{%a}.%a@]" (pp_term c) u (pp_term c) t
B.push f c a B.Void
let pp_context frm c =
- let pp_entry frm = function
- | a, B.Abst w ->
- F.fprintf frm "@,@[%a : %a@]" id a (pp_term c) w
- | a, B.Abbr v ->
- F.fprintf frm "@,@[%a = %a@]" id a (pp_term c) v
- | a, B.Void ->
- F.fprintf frm "@,%a" id a
+ let pp_entry f c a = function
+ | B.Abst w ->
+ F.fprintf frm "@,@[%a : %a@]" id a (pp_term c) w; f ()
+ | B.Abbr v ->
+ F.fprintf frm "@,@[%a = %a@]" id a (pp_term c) v; f ()
+ | B.Void ->
+ F.fprintf frm "@,%a" id a; f ()
in
- let iter map frm l = List.iter (map frm) l in
- let f es = F.fprintf frm "%a" (iter pp_entry) (List.rev es) in
- B.contents f c
+ B.rev_iter C.start pp_entry c
let specs = {
L.pp_term = pp_term; L.pp_context = pp_context
(* term xml printing ********************************************************)
let id frm a =
- let f = function
- | None -> ()
- | Some (true, s) -> F.fprintf frm " name=%S" s
- | Some (false, n) -> F.fprintf frm " name=%S" ("^" ^ n)
+ let f s = function
+ | true -> F.fprintf frm " name=%S" s
+ | false -> F.fprintf frm " name=%S" ("^" ^ s)
in
- B.name f a
+ B.name C.start f a
let rec exp_term frm = function
| B.Sort (a, l) ->
module B = Brg
module O = BrgOutput
module E = BrgEnvironment
-module S = BrgSubstitution
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 *******************************************************)
in
raise (TypeError (L.ct_items3 sc c st1 t1 st2 t2 st3 t3))
-let empty_machine c = {
- c = c; s = []
-}
+let err () = assert false
let get f m i =
- let f e = function
- | Some (_, b) -> f e b
- | None -> error0 i
- in
- B.get f m.c i
-
-let lift_stack f s =
- let map f (v, i) = f (v, succ i) in
- Cps.list_map f map s
-
-let push f m a b =
- assert (m.s = []);
- f {m with c = (a, b) :: m.c}
+ B.get error0 f m.c i
(* to share *)
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 ->
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 ->
P.add ~ldelta:1 ();
- step f ~delta ~rt m v
+ step f ~delta ~rt {m with c = c} v
| B.Abst w when rt ->
P.add ~lrt:1 ();
- step f ~delta ~rt m w
+ 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
+ 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) ->
P.add ~tau:1 ();
step f ~delta ~rt m t
| B.Appl (_, v, t) ->
- step f ~delta ~rt {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 ->
- P.add ~beta:1 ~upsilon:(List.length tl) ();
- let f c s = step f ~delta ~rt {c = c; s = s} t in
- let f c = lift_stack (f c) tl in
- let f v = B.push f m.c a (B.Abbr v (* (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) ->
+ | B.Bind (a, b, t) ->
P.add ~upsilon:(List.length m.s) ();
- let f s c = step f ~delta ~rt {c = c; s = s} t in
- let f s = B.push (f s) m.c a b in
- lift_stack f m.s
-
-(* Interface functions ******************************************************)
+ let f c = step f ~delta ~rt {m with c = c} t in
+ B.push f m.c ~c:m.c a b
let domain f m t =
let f r = L.unbox level; f r in
- let f m = function
+ 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" m.c t;
step f ~delta:true ~rt:true m t
-let rec ac_nfs f ~si r m1 u m2 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 u, t with
- | B.Sort (_, h1), B.Sort (_, h2) ->
+ 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 _) :: _, i1),
- B.LRef (B.Entry (e2, B.Abst _) :: _, i2) ->
- P.add ~zeta:(i1+i2-e1-e2) ();
- if e1 = e2 then ac_stacks f ~si r m1 m2 else f false
- | B.GRef (B.Entry (e1, B.Abst _) :: _, _),
- B.GRef (B.Entry (e2, B.Abst _) :: _, _) ->
+ | Some (e1, B.Abst _), _, Some (e2, B.Abst _), _ ->
if e1 = e2 then ac_stacks f ~si r m1 m2 else f false
- | B.GRef (B.Entry (e1, B.Abbr v1) :: _, _),
- B.GRef (B.Entry (e2, B.Abbr v2) :: _, _) ->
+ | Some (e1, B.Abbr v1), _, Some (e2, B.Abbr v2), _ ->
if e1 = e2 then
let f r =
if r then f r
ac_stacks f ~si r m1 m2
else if e1 < e2 then begin
P.add ~gdelta:1 ();
- step (ac_nfs f ~si r m1 u) m2 v2
+ step (ac_nfs f ~si r m1 a1 u) m2 v2
end else begin
P.add ~gdelta:1 ();
- step (ac_nfs_rev f ~si r m2 t) m1 v1
+ step (ac_nfs_rev f ~si r m2 a2 t) m1 v1
end
- | _, B.GRef (B.Entry (_, B.Abbr v2) :: _, _) ->
+ | _, _, Some (_, B.Abbr v2), _ ->
P.add ~gdelta:1 ();
- step (ac_nfs f ~si r m1 u) m2 v2
- | B.GRef (B.Entry (_, B.Abbr v1) :: _, _), _ ->
+ 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 t) m1 v1
- | B.Bind (a1, (B.Abst w1 as b1), t1),
- B.Bind (a2, (B.Abst w2 as b2), t2) ->
+ 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 m1 w1 m2 w2
- | B.Sort _, B.Bind (a, b, t) when si ->
+ | _, 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 m2 t m1 u = ac_nfs f ~si r 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 m1 t1 m2 t2 =
(* L.warn "entering R.are_convertible"; *)
- let g m1 t1 = step (ac_nfs f ~si r m1 t1) m2 t2 in
+ 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 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 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 assert_conversion f ?(si=false) ?(rt=false) c u w v =
+let empty_machine = {
+ c = B.empty_context; s = []; i = 0
+}
+
+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
- let mw = empty_machine c in
let f mu u =
let f = function
| true -> f ()
- | false -> error3 c v w u
+ | false -> error3 mw.c v w u
in
- L.box level; log2 "Now converting" c u c w;
+ 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
exception TypeError of Brg.message
+type machine
+
+val empty_machine: machine
+
+val get: (Brg.attrs -> Brg.bind -> 'a) -> machine -> int -> 'a
+
+val push: (machine -> 'a) -> machine -> Brg.attrs -> Brg.bind -> 'a
+
(* arguments: expected type, inferred type, typed term *)
val assert_conversion:
(unit -> 'a) -> ?si:bool -> ?rt:bool ->
- Brg.context -> Brg.term -> Brg.term -> Brg.term -> 'a
+ machine -> Brg.term -> Brg.term -> Brg.term -> 'a
+
+val message1:
+ string -> machine -> Brg.term -> (Brg.context, Brg.term) Log.message
let level = 4
-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 log1 s m t =
+ let s = s ^ " the term" in
+ L.log O.specs level (R.message1 s m t)
-let error1 st c t =
- let sc = "In the context" in
- raise (R.TypeError (L.ct_items1 sc c st t))
+let error1 s m t =
+ raise (R.TypeError (R.message1 s m t))
(* Interface functions ******************************************************)
-let rec b_type_of f ~si g c x =
- log1 "Now checking" c x;
+let rec b_type_of f ~si g m x =
+ log1 "Now checking" m x;
match x with
| B.Sort (a, h) ->
let f h = f x (B.Sort (a, h)) in H.apply f g h
| B.LRef (_, i) ->
let f _ = function
- | Some (_, B.Abst w) ->
+ | B.Abst w ->
S.lift (f x) (succ i) (0) w
- | Some (_, B.Abbr (B.Cast (_, w, _))) ->
+ | B.Abbr (B.Cast (_, w, _)) ->
S.lift (f x) (succ i) (0) w
- | Some (_, B.Abbr _) -> assert false
- | Some (_, B.Void) ->
- error1 "reference to excluded variable" c x
- | None ->
- error1 "variable not found" c x
+ | B.Abbr _ -> assert false
+ | B.Void ->
+ error1 "reference to excluded variable" m x
in
- B.get f c i
+ R.get f m i
| B.GRef (_, uri) ->
let f = function
| _, _, B.Abst w -> f x w
| _, _, B.Abbr (B.Cast (_, w, _)) -> f x w
| _, _, B.Abbr _ -> assert false
| _, _, B.Void ->
- error1 "reference to excluded object" c x
+ error1 "reference to excluded object" m x
in
E.get_obj f uri
| B.Bind (a, B.Abbr v, t) ->
let f xv xt tt =
f (A.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt)
in
- let f xv cc = b_type_of (f xv) ~si g cc t in
- let f xv = B.push (f xv) c a (B.Abbr xv) in
+ let f xv m = b_type_of (f xv) ~si g m t in
+ let f xv = R.push (f xv) m a (B.Abbr xv) in
let f xv vv = match xv with
| B.Cast _ -> f xv
- | _ -> assert false (* f (B.Cast ([], vv, xv)) *)
+ | _ -> f (B.Cast ([], vv, xv))
in
- type_of f ~si g c v
+ type_of f ~si g m v
| B.Bind (a, B.Abst u, t) ->
let f xu xt tt =
f (A.sh2 u xu t xt x (B.bind_abst a)) (B.bind_abst a xu tt)
in
- let f xu cc = b_type_of (f xu) ~si g cc t in
- let f xu _ = B.push (f xu) c a (B.Abst xu) in
- type_of f ~si g c u
+ let f xu m = b_type_of (f xu) ~si g m t in
+ let f xu _ = R.push (f xu) m a (B.Abst xu) in
+ type_of f ~si g m u
| B.Bind (a, B.Void, t) ->
let f xt tt =
f (A.sh1 t xt x (B.bind a B.Void)) (B.bind a B.Void tt)
in
- let f cc = b_type_of f ~si g cc t in
- B.push f c a B.Void
+ let f m = b_type_of f ~si g m t in
+ R.push f m a B.Void
| B.Appl (a, v, t) ->
let f xv vv xt tt =
let f () = f (A.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt) in
- R.assert_conversion f ~si ~rt:true c tt vv xv
+ R.assert_conversion f ~si ~rt:true m tt vv xv
in
- let f xv vv = b_type_of (f xv vv) ~si g c t in
- type_of f ~si g c v
+ let f xv vv = b_type_of (f xv vv) ~si g m t in
+ type_of f ~si g m v
| B.Cast (a, u, t) ->
let f xu xt tt =
let f () = f (A.sh2 u xu t xt x (B.cast a)) xu in
- R.assert_conversion f ~si c xu tt xt
+ R.assert_conversion f ~si m xu tt xt
in
- let f xu _ = b_type_of (f xu) ~si g c t in
- type_of f ~si g c u
+ let f xu _ = b_type_of (f xu) ~si g m t in
+ type_of f ~si g m u
-and type_of f ?(si=false) g c x =
+and type_of f ?(si=false) g m x =
let f t u = L.unbox level; f t u in
- L.box level; b_type_of f ~si g c x
+ L.box level; b_type_of f ~si g m x
val type_of:
(Brg.term -> Brg.term -> 'a) -> ?si:bool ->
- Hierarchy.graph -> Brg.context -> Brg.term -> 'a
+ Hierarchy.graph -> BrgReduction.machine -> Brg.term -> 'a
module L = Log
module B = Brg
module E = BrgEnvironment
+module R = BrgReduction
module T = BrgType
(* Interface functions ******************************************************)
| Some (e, uri, B.Abst t) ->
let f tt obj = f (Some tt) (Some obj) in
let f xt tt = E.set_obj (f tt) (e, uri, B.Abst xt) in
- L.loc := e; T.type_of f ~si g B.empty_context t
+ L.loc := e; T.type_of f ~si g R.empty_machine t
| Some (e, uri, B.Abbr t) ->
let f tt obj = f (Some tt) (Some obj) in
let f xt tt = E.set_obj (f tt) (e, uri, B.Abbr xt) in
- L.loc := e; T.type_of f ~si g B.empty_context t
+ L.loc := e; T.type_of f ~si g R.empty_machine t
| Some (e, uri, B.Void) ->
let f obj = f None (Some obj) in
L.loc := e; E.set_obj f (e, uri, B.Void)
| String of string
| Loc
+type ('a, 'b) message = ('a, 'b) item list
+
type ('a, 'b) specs = {
pp_term : 'a -> F.formatter -> 'b -> unit;
pp_context: F.formatter -> 'a -> unit
| String of string
| Loc
+type ('a, 'b) message = ('a, 'b) item list
+
type ('a, 'b) specs = {
pp_term : 'a -> Format.formatter -> 'b -> unit;
pp_context: Format.formatter -> 'a -> unit
val flush_err: unit -> unit
-val log: ('a, 'b) specs -> int -> ('a, 'b) item list -> unit
+val log: ('a, 'b) specs -> int -> ('a, 'b) message -> unit
-val error: ('a, 'b) specs -> ('a, 'b) item list -> unit
+val error: ('a, 'b) specs -> ('a, 'b) message -> unit
-val items1: string -> ('a, 'b) item list
+val items1: string -> ('a, 'b) message
-val t_items1: string -> 'a -> 'b -> ('a, 'b) item list
+val t_items1: string -> 'a -> 'b -> ('a, 'b) message
val ct_items1:
- string -> 'a -> string -> 'b -> ('a, 'b) item list
+ string -> 'a -> string -> 'b -> ('a, 'b) message
val ct_items2:
string -> 'a -> string -> 'b -> string -> 'a -> string -> 'b ->
- ('a, 'b) item list
+ ('a, 'b) message
val ct_items3:
string -> 'a -> string -> 'b -> string -> 'b -> string -> 'b ->
- ('a, 'b) item list
+ ('a, 'b) message
C.list_fold_right f map pars B.empty_context
let unwind_to_xlate_term f c t =
- let map f t (a, b) = f (B.bind a b t) in
- let f t = C.list_fold_left f map t c in
+ let map f t a b = f (B.bind a b t) in
+ let f t = B.fold_left f map t c in
xlate_term c f t
let xlate_entry f = function
projects / helm.git / commitdiff