From 25fba20748a951f7061188cc5fabece8f5ac97b9 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 3 Dec 2008 19:24:54 +0000 Subject: [PATCH] improved interface for brgEnvironment --- helm/software/lambda-delta/basic_rg/brg.ml | 4 ++-- helm/software/lambda-delta/basic_rg/brgEnvironment.ml | 11 +++++++---- .../software/lambda-delta/basic_rg/brgEnvironment.mli | 4 ++-- helm/software/lambda-delta/basic_rg/brgOutput.ml | 6 +++--- helm/software/lambda-delta/toplevel/metaBrg.ml | 8 ++++---- 5 files changed, 18 insertions(+), 15 deletions(-) diff --git a/helm/software/lambda-delta/basic_rg/brg.ml b/helm/software/lambda-delta/basic_rg/brg.ml index eaaeb6e60..45777ead4 100644 --- a/helm/software/lambda-delta/basic_rg/brg.ml +++ b/helm/software/lambda-delta/basic_rg/brg.ml @@ -21,6 +21,6 @@ type term = Sort of int (* hierarchy index *) | Appl of term * term (* argument, function *) | Bind of id * bind * term * term (* name, binder, content, scope *) -type obj = bind * term (* binder, contents *) +type obj = int * uri * bind * term (* age, uri, binder, contents *) -type item = (obj * uri) option (* uri, object *) +type item = obj option diff --git a/helm/software/lambda-delta/basic_rg/brgEnvironment.ml b/helm/software/lambda-delta/basic_rg/brgEnvironment.ml index f1561516d..b0cb9596e 100644 --- a/helm/software/lambda-delta/basic_rg/brgEnvironment.ml +++ b/helm/software/lambda-delta/basic_rg/brgEnvironment.ml @@ -17,14 +17,17 @@ exception ObjectNotFound of string Lazy.t let hsize = 7000 let env = H.create hsize +let entry = ref 0 (* Internal functions *******************************************************) (* Interface functions ******************************************************) -let set_obj f obj uri = - H.add env uri obj; f obj uri - +let set_obj f obj = + let _, uri, b, t = obj in + let obj = !entry, uri, b, t in + incr entry; H.add env uri obj; f obj + let get_obj f uri = - try f (H.find env uri) uri + try f (H.find env uri) with Not_found -> raise (ObjectNotFound (lazy (U.string_of_uri uri))) diff --git a/helm/software/lambda-delta/basic_rg/brgEnvironment.mli b/helm/software/lambda-delta/basic_rg/brgEnvironment.mli index a6fec6db0..ddf55d7a4 100644 --- a/helm/software/lambda-delta/basic_rg/brgEnvironment.mli +++ b/helm/software/lambda-delta/basic_rg/brgEnvironment.mli @@ -11,6 +11,6 @@ exception ObjectNotFound of string Lazy.t -val set_obj: (Brg.obj -> NUri.uri -> 'a) -> Brg.obj -> NUri.uri -> 'a +val set_obj: (Brg.obj -> 'a) -> Brg.obj -> 'a -val get_obj: (Brg.obj -> NUri.uri -> 'a) -> NUri.uri -> 'a +val get_obj: (Brg.obj -> 'a) -> NUri.uri -> 'a diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml index dcefefa2e..e29b3f495 100644 --- a/helm/software/lambda-delta/basic_rg/brgOutput.ml +++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml @@ -58,13 +58,13 @@ let count_obj_binder f c = function | B.Abst -> f {c with eabsts = succ c.eabsts} | B.Abbr -> f {c with eabbrs = succ c.eabbrs} -let count_obj f c (b, t) = +let count_obj f c (_, _, b, t) = let f c = count_obj_binder f c b in count_term f c t let count_item f c = function - | Some (obj, _) -> count_obj f c obj - | None -> f c + | Some obj -> count_obj f c obj + | None -> f c let print_counters f c = let terms = diff --git a/helm/software/lambda-delta/toplevel/metaBrg.ml b/helm/software/lambda-delta/toplevel/metaBrg.ml index 7c7adce7e..4088c2982 100644 --- a/helm/software/lambda-delta/toplevel/metaBrg.ml +++ b/helm/software/lambda-delta/toplevel/metaBrg.ml @@ -45,12 +45,12 @@ let xlate_pars f (id, w) = xlate_term f w let xlate_entry f = function - | _, pars, uri, u, None -> - let f u = f ((B.Abst, u), uri) in + | e, pars, uri, u, None -> + let f u = f (e, uri, B.Abst, u) in let f pars = map_fold_left f xlate_term map_pars u pars in Cps.list_rev_map f xlate_pars pars - | _, pars, uri, u, Some (_, t) -> - let f u t = f ((B.Abbr, (B.Cast (u, t))), uri) in + | e, pars, uri, u, Some (_, t) -> + let f u t = f (e, uri, B.Abbr, (B.Cast (u, t))) in let f pars u = map_fold_left (f u) xlate_term map_pars t pars in let f pars = map_fold_left (f pars) xlate_term map_pars u pars in Cps.list_rev_map f xlate_pars pars -- 2.39.2