From 8a4c83c6341976f2bb70eb44a0c70f2aa95ad3ea Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 8 Sep 2009 20:39:31 +0000 Subject: [PATCH] some renaming and some interfaces improved --- helm/software/lambda-delta/.depend.opt | 4 ++-- helm/software/lambda-delta/basic_ag/bag.ml | 8 +++---- .../lambda-delta/basic_ag/bagOutput.ml | 4 ++-- .../lambda-delta/basic_ag/bagOutput.mli | 2 +- .../lambda-delta/basic_ag/bagReduction.ml | 12 +++++----- .../lambda-delta/basic_ag/bagReduction.mli | 4 ++-- .../software/lambda-delta/basic_ag/bagType.ml | 12 +++++----- .../lambda-delta/basic_ag/bagType.mli | 2 +- .../lambda-delta/basic_ag/bagUntrusted.ml | 4 ++-- helm/software/lambda-delta/basic_rg/brg.ml | 10 ++++---- .../lambda-delta/basic_rg/brgOutput.ml | 12 +++++----- .../lambda-delta/basic_rg/brgOutput.mli | 2 +- .../lambda-delta/basic_rg/brgReduction.ml | 18 +++++++------- .../software/lambda-delta/basic_rg/brgType.ml | 10 ++++---- helm/software/lambda-delta/lib/log.ml | 24 +++++++++---------- helm/software/lambda-delta/lib/log.mli | 12 +++++----- helm/software/lambda-delta/toplevel/meta.ml | 8 +++---- .../software/lambda-delta/toplevel/metaBag.ml | 2 +- .../software/lambda-delta/toplevel/metaBrg.ml | 2 +- 19 files changed, 76 insertions(+), 76 deletions(-) diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index 6524ef593..692e237c6 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -113,8 +113,8 @@ basic_ag/bagUntrusted.cmo: lib/log.cmi basic_ag/bagType.cmi \ basic_ag/bagEnvironment.cmi basic_ag/bag.cmx basic_ag/bagUntrusted.cmi basic_ag/bagUntrusted.cmx: lib/log.cmx basic_ag/bagType.cmx \ basic_ag/bagEnvironment.cmx basic_ag/bag.cmx basic_ag/bagUntrusted.cmi -toplevel/meta.cmo: lib/nUri.cmi automath/aut.cmx -toplevel/meta.cmx: lib/nUri.cmx automath/aut.cmx +toplevel/meta.cmo: common/item.cmx +toplevel/meta.cmx: common/item.cmx toplevel/metaOutput.cmi: toplevel/meta.cmx toplevel/metaOutput.cmo: lib/nUri.cmi toplevel/meta.cmx lib/log.cmi \ lib/cps.cmx toplevel/metaOutput.cmi diff --git a/helm/software/lambda-delta/basic_ag/bag.ml b/helm/software/lambda-delta/basic_ag/bag.ml index 65a93ab18..32a9b0c5b 100644 --- a/helm/software/lambda-delta/basic_ag/bag.ml +++ b/helm/software/lambda-delta/basic_ag/bag.ml @@ -30,9 +30,9 @@ type obj = bind Item.obj (* age, uri, binder *) type item = bind Item.item -type context = (int * id * bind) list (* location, name, binder *) +type lenv = (int * id * bind) list (* location, name, binder *) -type message = (context, term) Log.item list +type message = (lenv, term) Log.item list (* Currified constructors ***************************************************) @@ -60,9 +60,9 @@ let new_location () = let loc = !location in incr location; loc let locations () = !location -(* context handling functions ***********************************************) +(* local environment handling functions *************************************) -let empty_context = [] +let empty_lenv = [] let push msg f es l id b = let rec does_not_occur loc = function diff --git a/helm/software/lambda-delta/basic_ag/bagOutput.ml b/helm/software/lambda-delta/basic_ag/bagOutput.ml index c315b1ec7..d6633bcd8 100644 --- a/helm/software/lambda-delta/basic_ag/bagOutput.ml +++ b/helm/software/lambda-delta/basic_ag/bagOutput.ml @@ -133,7 +133,7 @@ let rec pp_term c frm = function let f cc = F.fprintf frm "@[[%s].%a@]" (res l id) (pp_term cc) t in B.push "output void" f c l id B.Void -let pp_context frm c = +let pp_lenv frm c = let pp_entry frm = function | l, id, B.Abst w -> F.fprintf frm "@,@[%s : %a@]" (res l id) (pp_term c) w @@ -147,5 +147,5 @@ let pp_context frm c = B.contents f c let specs = { - L.pp_term = pp_term; L.pp_context = pp_context + L.pp_term = pp_term; L.pp_lenv = pp_lenv } diff --git a/helm/software/lambda-delta/basic_ag/bagOutput.mli b/helm/software/lambda-delta/basic_ag/bagOutput.mli index e176227d9..58c63f110 100644 --- a/helm/software/lambda-delta/basic_ag/bagOutput.mli +++ b/helm/software/lambda-delta/basic_ag/bagOutput.mli @@ -17,4 +17,4 @@ val count_item: (counters -> 'a) -> counters -> Bag.item -> 'a val print_counters: (unit -> 'a) -> counters -> 'a -val specs: (Bag.context, Bag.term) Log.specs +val specs: (Bag.lenv, Bag.term) Log.specs diff --git a/helm/software/lambda-delta/basic_ag/bagReduction.ml b/helm/software/lambda-delta/basic_ag/bagReduction.ml index c2de019cd..3aa576a86 100644 --- a/helm/software/lambda-delta/basic_ag/bagReduction.ml +++ b/helm/software/lambda-delta/basic_ag/bagReduction.ml @@ -19,7 +19,7 @@ module S = BagSubstitution type machine = { i: int; - c: B.context; + c: B.lenv; s: B.term list } @@ -44,14 +44,14 @@ let term_of_whdr = function let level = 5 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 ~sc2:s3 ~c2: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} diff --git a/helm/software/lambda-delta/basic_ag/bagReduction.mli b/helm/software/lambda-delta/basic_ag/bagReduction.mli index c9918704d..8f32faa0e 100644 --- a/helm/software/lambda-delta/basic_ag/bagReduction.mli +++ b/helm/software/lambda-delta/basic_ag/bagReduction.mli @@ -14,7 +14,7 @@ type ho_whd_result = | Abst of Bag.term val ho_whd: - (ho_whd_result -> 'a) -> Bag.context -> Bag.term -> 'a + (ho_whd_result -> 'a) -> Bag.lenv -> Bag.term -> 'a val are_convertible: - (bool -> 'a) -> ?si:bool -> Bag.context -> Bag.term -> Bag.term -> 'a + (bool -> 'a) -> ?si:bool -> Bag.lenv -> Bag.term -> Bag.term -> 'a diff --git a/helm/software/lambda-delta/basic_ag/bagType.ml b/helm/software/lambda-delta/basic_ag/bagType.ml index 02c831994..6adcc4087 100644 --- a/helm/software/lambda-delta/basic_ag/bagType.ml +++ b/helm/software/lambda-delta/basic_ag/bagType.ml @@ -26,18 +26,18 @@ exception TypeError of B.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 sc, st = s ^ " in the envireonment", "the term" in + L.log O.specs level (L.et_items1 sc c st t) let error1 st c t = - let sc = "In the context" in - raise (TypeError (L.ct_items1 sc c st t)) + let sc = "In the envireonment" in + raise (TypeError (L.et_items1 sc c st t)) let error3 c t1 t2 t3 = let sc, st1, st2, st3 = - "In the context", "the term", "is of type", "but must be of type" + "In the envireonment", "the term", "is of type", "but must be of type" in - raise (TypeError (L.ct_items3 sc c st1 t1 st2 t2 st3 t3)) + raise (TypeError (L.et_items3 sc c st1 t1 st2 t2 st3 t3)) let mk_gref u l = let map t v = B.Appl (v, t) in diff --git a/helm/software/lambda-delta/basic_ag/bagType.mli b/helm/software/lambda-delta/basic_ag/bagType.mli index 37f92875d..d44b1cfe2 100644 --- a/helm/software/lambda-delta/basic_ag/bagType.mli +++ b/helm/software/lambda-delta/basic_ag/bagType.mli @@ -13,4 +13,4 @@ exception TypeError of Bag.message val type_of: (Bag.term -> Bag.term -> 'a) -> ?si:bool -> - Hierarchy.graph -> Bag.context -> Bag.term -> 'a + Hierarchy.graph -> Bag.lenv -> Bag.term -> 'a diff --git a/helm/software/lambda-delta/basic_ag/bagUntrusted.ml b/helm/software/lambda-delta/basic_ag/bagUntrusted.ml index e588caa49..69112d2ff 100644 --- a/helm/software/lambda-delta/basic_ag/bagUntrusted.ml +++ b/helm/software/lambda-delta/basic_ag/bagUntrusted.ml @@ -22,11 +22,11 @@ let type_check f ?(si=false) g = function | Some (a, uri, B.Abst t) -> let f tt obj = f (Some tt) (Some obj) in let f xt tt = E.set_obj (f tt) (a, uri, B.Abst xt) in - L.loc := a; T.type_of f ~si g B.empty_context t + L.loc := a; T.type_of f ~si g B.empty_lenv t | Some (a, uri, B.Abbr t) -> let f tt obj = f (Some tt) (Some obj) in let f xt tt = E.set_obj (f tt) (a, uri, B.Abbr xt) in - L.loc := a; T.type_of f ~si g B.empty_context t + L.loc := a; T.type_of f ~si g B.empty_lenv t | Some (a, uri, B.Void) -> let f obj = f None (Some obj) in L.loc := a; E.set_obj f (a, uri, B.Void) diff --git a/helm/software/lambda-delta/basic_rg/brg.ml b/helm/software/lambda-delta/basic_rg/brg.ml index 6a9f9fd20..52ec4728f 100644 --- a/helm/software/lambda-delta/basic_rg/brg.ml +++ b/helm/software/lambda-delta/basic_rg/brg.ml @@ -35,9 +35,9 @@ type obj = bind Item.obj (* age, uri, binder *) type item = bind Item.item -type context = Null -(* Cons: tail, relative context, binder *) - | Cons of context * context option * bind +type lenv = Null +(* Cons: tail, relative local environment, binder *) + | Cons of lenv * lenv option * bind (* Currified constructors ***************************************************) @@ -57,9 +57,9 @@ let bind_abst a u t = Bind (Abst (a, u), t) let bind_abbr a v t = Bind (Abbr (a, v), t) -(* context handling functions ***********************************************) +(* local environment handling functions *************************************) -let empty_context = Null +let empty_lenv = Null let push f es ?c b = let es = Cons (es, c, b) in f es diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml index eec76f620..47005ec6d 100644 --- a/helm/software/lambda-delta/basic_rg/brgOutput.ml +++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml @@ -93,10 +93,10 @@ let count_obj f c = function let c = {c with eabsts = succ c.eabsts; nodes = succ c.nodes; uris = u :: c.uris } in - count_term f c B.empty_context w + count_term f c B.empty_lenv w | (_, _, B.Abbr (_, v)) -> let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in - count_term f c B.empty_context v + count_term f c B.empty_lenv v | (_, u, B.Void _) -> let c = {c with evoids = succ c.evoids; nodes = succ c.nodes; uris = u :: c.uris @@ -164,7 +164,7 @@ let rename_bind f c = function | B.Abbr (a, v) -> let f a = f (B.abbr a v) in rename f c a | B.Void a -> let f a = f (B.Void a) in rename f c a -(* context/term pretty printing *********************************************) +(* lenv/term pretty printing ************************************************) let id frm a = let f n = function @@ -209,7 +209,7 @@ let rec pp_term c frm = function let f a = B.push (f a) c (B.Void a) in rename f c a -let pp_context frm c = +let pp_lenv frm c = let pp_entry f c = function | B.Abst (a, w) -> let f a = F.fprintf frm "@,@[%a : %a@]" id a (pp_term c) w; f () in @@ -224,7 +224,7 @@ let pp_context frm c = B.rev_iter C.start pp_entry c let specs = { - L.pp_term = pp_term; L.pp_context = pp_context + L.pp_term = pp_term; L.pp_lenv = pp_lenv } (* term xml printing ********************************************************) @@ -290,4 +290,4 @@ let exp_obj c frm = function F.fprintf frm "" str id a let export_obj frm obj = - F.fprintf frm "@,@[ %a@]@," (exp_obj B.empty_context) obj + F.fprintf frm "@,@[ %a@]@," (exp_obj B.empty_lenv) obj diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.mli b/helm/software/lambda-delta/basic_rg/brgOutput.mli index 138a29a9c..9a3b58b4a 100644 --- a/helm/software/lambda-delta/basic_rg/brgOutput.mli +++ b/helm/software/lambda-delta/basic_rg/brgOutput.mli @@ -17,6 +17,6 @@ val count_item: (counters -> 'a) -> counters -> Brg.item -> 'a val print_counters: (unit -> 'a) -> counters -> 'a -val specs: (Brg.context, Brg.term) Log.specs +val specs: (Brg.lenv, Brg.term) Log.specs val export_obj: Format.formatter -> Brg.bind Item.obj -> unit diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.ml b/helm/software/lambda-delta/basic_rg/brgReduction.ml index c8d8ddde9..71a0d1639 100644 --- a/helm/software/lambda-delta/basic_rg/brgReduction.ml +++ b/helm/software/lambda-delta/basic_rg/brgReduction.ml @@ -19,8 +19,8 @@ module O = BrgOutput module E = BrgEnvironment type machine = { - c: B.context; - s: (B.context * B.term) list; + c: B.lenv; + s: (B.lenv * B.term) list; i: int } @@ -29,12 +29,12 @@ type machine = { let level = 5 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 ~sc2:s3 ~c2: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 are_alpha_convertible err f t1 t2 = let rec aux f = function @@ -177,7 +177,7 @@ and ac_stacks err f m1 m2 = (* Interface functions ******************************************************) let empty_machine = { - c = B.empty_context; s = []; i = 0 + c = B.empty_lenv; s = []; i = 0 } let get err f m i = @@ -200,8 +200,8 @@ let are_convertible err f ?(si=false) mu u mw w = let pp_term m frm t = O.specs.L.pp_term m.c frm t -let pp_context frm m = O.specs.L.pp_context frm m.c +let pp_lenv frm m = O.specs.L.pp_lenv frm m.c let specs = { - L.pp_term = pp_term; L.pp_context = pp_context + L.pp_term = pp_term; L.pp_lenv = pp_lenv } diff --git a/helm/software/lambda-delta/basic_rg/brgType.ml b/helm/software/lambda-delta/basic_rg/brgType.ml index d2d6706b8..b26d1b439 100644 --- a/helm/software/lambda-delta/basic_rg/brgType.ml +++ b/helm/software/lambda-delta/basic_rg/brgType.ml @@ -29,7 +29,7 @@ exception TypeError of message let level = 4 let message1 st1 m t1 = - L.ct_items1 "In the context" m st1 t1 + L.et_items1 "In the environment" m st1 t1 let log1 s m t = let s = s ^ " the term" in @@ -39,14 +39,14 @@ let error1 s m t = raise (TypeError (message1 s m t)) let message3 m t1 t2 ?mu t3 = - let sm, st1, st2 = "In the context", "the term", "is of type" in + let sm, st1, st2 = "In the environment", "the term", "is of type" in match mu with | Some mu -> - let smu, st3 = "but in the context", "it must be of type" in - L.ct_items3 sm m st1 t1 st2 t2 ~sc3:smu ~c3:mu st3 t3 + let smu, st3 = "but in the environment", "it must be of type" in + L.et_items3 sm m st1 t1 st2 t2 ~sc3:smu ~c3:mu st3 t3 | None -> let st3 = "but it must be of type" in - L.ct_items3 sm m st1 t1 st2 t2 st3 t3 + L.et_items3 sm m st1 t1 st2 t2 st3 t3 let error3 m t1 t2 ?mu t3 = raise (TypeError (message3 m t1 t2 ?mu t3)) diff --git a/helm/software/lambda-delta/lib/log.ml b/helm/software/lambda-delta/lib/log.ml index 2d3f07517..e50fa254d 100644 --- a/helm/software/lambda-delta/lib/log.ml +++ b/helm/software/lambda-delta/lib/log.ml @@ -14,7 +14,7 @@ module F = Format module C = Cps type ('a, 'b) item = Term of 'a * 'b - | Context of 'a + | LEnv of 'a | Warn of string | String of string | Loc @@ -22,8 +22,8 @@ type ('a, 'b) item = Term of 'a * 'b 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 + pp_term: 'a -> F.formatter -> 'b -> unit; + pp_lenv: F.formatter -> 'a -> unit } let level = ref 0 @@ -39,7 +39,7 @@ let err = F.err_formatter let pp_items frm st l items = let pp_item frm = function | Term (c, t) -> F.fprintf frm "@,%a" (st.pp_term c) t - | Context c -> F.fprintf frm "%a" st.pp_context c + | LEnv c -> F.fprintf frm "%a" st.pp_lenv c | Warn s -> F.fprintf frm "@,%s" s | String s -> F.fprintf frm "%s " s | Loc -> F.fprintf frm " (line %u)" !loc @@ -70,23 +70,23 @@ let items1 s = [Warn s] let t_items1 st c t = [Warn st; Term (c, t)] -let ct_items1 sc c st t = - [Warn sc; Context c; Warn st; Term (c, t)] +let et_items1 sc c st t = + [Warn sc; LEnv c; Warn st; Term (c, t)] -let ct_items2 sc1 c1 st1 t1 ?sc2 ?c2 st2 t2 = +let et_items2 sc1 c1 st1 t1 ?sc2 ?c2 st2 t2 = let tl = match sc2, c2 with - | Some sc2, Some c2 -> ct_items1 sc2 c2 st2 t2 + | Some sc2, Some c2 -> et_items1 sc2 c2 st2 t2 | None, None -> t_items1 st2 c1 t2 | _ -> assert false in - ct_items1 sc1 c1 st1 t1 @ tl + et_items1 sc1 c1 st1 t1 @ tl -let ct_items3 sc1 c1 st1 t1 ?sc2 ?c2 st2 t2 ?sc3 ?c3 st3 t3 = +let et_items3 sc1 c1 st1 t1 ?sc2 ?c2 st2 t2 ?sc3 ?c3 st3 t3 = let tl = match sc3, c3 with - | Some sc3, Some c3 -> ct_items1 sc3 c3 st3 t3 + | Some sc3, Some c3 -> et_items1 sc3 c3 st3 t3 | None, None -> t_items1 st3 c1 t3 | _ -> assert false in - ct_items2 sc1 c1 st1 t1 ?sc2 ?c2 st2 t2 @ tl + et_items2 sc1 c1 st1 t1 ?sc2 ?c2 st2 t2 @ tl let warn msg = F.fprintf std "@,%s" msg diff --git a/helm/software/lambda-delta/lib/log.mli b/helm/software/lambda-delta/lib/log.mli index 0de107325..3e093575a 100644 --- a/helm/software/lambda-delta/lib/log.mli +++ b/helm/software/lambda-delta/lib/log.mli @@ -10,7 +10,7 @@ V_______________________________________________________________ *) type ('a, 'b) item = Term of 'a * 'b - | Context of 'a + | LEnv of 'a | Warn of string | String of string | Loc @@ -18,8 +18,8 @@ type ('a, 'b) item = Term of 'a * 'b 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 + pp_term: 'a -> Format.formatter -> 'b -> unit; + pp_lenv: Format.formatter -> 'a -> unit } val loc: int ref @@ -46,15 +46,15 @@ val items1: string -> ('a, 'b) message val t_items1: string -> 'a -> 'b -> ('a, 'b) message -val ct_items1: +val et_items1: string -> 'a -> string -> 'b -> ('a, 'b) message -val ct_items2: +val et_items2: string -> 'a -> string -> 'b -> ?sc2:string -> ?c2:'a -> string -> 'b -> ('a, 'b) message -val ct_items3: +val et_items3: string -> 'a -> string -> 'b -> ?sc2:string -> ?c2:'a -> string -> 'b -> ?sc3:string -> ?c3:'a -> string -> 'b -> diff --git a/helm/software/lambda-delta/toplevel/meta.ml b/helm/software/lambda-delta/toplevel/meta.ml index 5b3895e79..a7af17273 100644 --- a/helm/software/lambda-delta/toplevel/meta.ml +++ b/helm/software/lambda-delta/toplevel/meta.ml @@ -9,13 +9,13 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -type uri = NUri.uri +type uri = Item.uri -type id = Aut.id +type id = Item.id type term = Sort of bool (* sorts: true = TYPE, false = PROP *) - | LRef of int * int (* local reference: context length, de bruijn index *) - | GRef of int * uri * term list (* global reference: context length, name, arguments *) + | LRef of int * int (* local reference: local environment length, de bruijn index *) + | GRef of int * uri * term list (* global reference: local environment length, name, arguments *) | Appl of term * term (* application: argument, function *) | Abst of id * term * term (* abstraction: name, type, scope *) diff --git a/helm/software/lambda-delta/toplevel/metaBag.ml b/helm/software/lambda-delta/toplevel/metaBag.ml index 4f909bdca..e0dbf53ae 100644 --- a/helm/software/lambda-delta/toplevel/metaBag.ml +++ b/helm/software/lambda-delta/toplevel/metaBag.ml @@ -45,7 +45,7 @@ let xlate_pars f pars = let f w = B.push "meta" f c l id (B.Abst w) in xlate_term c f w in - C.list_fold_right f map pars B.empty_context + C.list_fold_right f map pars B.empty_lenv let unwind_to_xlate_term f c t = let map f t (l, id, b) = f (B.bind l id b t) in diff --git a/helm/software/lambda-delta/toplevel/metaBrg.ml b/helm/software/lambda-delta/toplevel/metaBrg.ml index 4c5696cea..9b0ae73db 100644 --- a/helm/software/lambda-delta/toplevel/metaBrg.ml +++ b/helm/software/lambda-delta/toplevel/metaBrg.ml @@ -44,7 +44,7 @@ let xlate_pars f pars = let f w = B.push f c (B.abst a w) in xlate_term c f w in - C.list_fold_right f map pars B.empty_context + C.list_fold_right f map pars B.empty_lenv let unwind_to_xlate_term f c t = let map f t b = f (B.bind b t) in -- 2.39.2