From ea41b1f6e212334924a8de4b2ff53b2586de9c4b Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 12 Nov 2009 19:15:43 +0000 Subject: [PATCH 1/1] some interfaces improved --- helm/software/lambda-delta/basic_ag/bagType.ml | 2 +- .../lambda-delta/basic_rg/brgReduction.ml | 16 ++++++++-------- .../lambda-delta/basic_rg/brgSubstitution.ml | 15 ++++++++++++++- helm/software/lambda-delta/basic_rg/brgType.ml | 2 +- helm/software/lambda-delta/common/hierarchy.ml | 8 ++++---- helm/software/lambda-delta/common/hierarchy.mli | 6 +++--- helm/software/lambda-delta/common/library.ml | 2 +- helm/software/lambda-delta/common/output.ml | 5 ++++- helm/software/lambda-delta/common/output.mli | 2 ++ helm/software/lambda-delta/toplevel/top.ml | 2 +- 10 files changed, 39 insertions(+), 21 deletions(-) diff --git a/helm/software/lambda-delta/basic_ag/bagType.ml b/helm/software/lambda-delta/basic_ag/bagType.ml index 30d8ac48b..dbf1bd4eb 100644 --- a/helm/software/lambda-delta/basic_ag/bagType.ml +++ b/helm/software/lambda-delta/basic_ag/bagType.ml @@ -51,7 +51,7 @@ let rec b_type_of f ~si g c x = log1 "Now checking" c x; match x with | B.Sort h -> - let f h = f x (B.Sort h) in H.apply f g h + let h = H.apply g h in f x (B.Sort h) | B.LRef i -> let f = function | Some (_, B.Abst w) -> f x w diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.ml b/helm/software/lambda-delta/basic_rg/brgReduction.ml index 1ae73652d..5dff4647b 100644 --- a/helm/software/lambda-delta/basic_rg/brgReduction.ml +++ b/helm/software/lambda-delta/basic_rg/brgReduction.ml @@ -20,9 +20,9 @@ module O = BrgOutput module E = BrgEnvironment type kam = { - e: B.lenv; - s: (B.lenv * B.term) list; - i: int + e: B.lenv; (* environment *) + s: (B.lenv * B.term) list; (* stack *) + d: int (* depth *) } (* Internal functions *******************************************************) @@ -122,12 +122,12 @@ let rec step st m x = let push m a b = assert (m.s = []); - let a, i = match b with - | B.Abst _ -> Y.Apix m.i :: a, succ m.i - | b -> a, m.i + let a, d = match b with + | B.Abst _ -> Y.Apix m.d :: a, succ m.d + | b -> a, m.d in let e = B.push m.e m.e a b in - {m with e = e; i = i} + {m with e = e; d = d} let rec ac_nfs st (m1, r1, u) (m2, r2, t) = log2 "Now converting nfs" m1.e u m2.e t; @@ -180,7 +180,7 @@ and ac_stacks st m1 m2 = (* Interface functions ******************************************************) let empty_kam = { - e = B.empty; s = []; i = 0 + e = B.empty; s = []; d = 0 } let get m i = diff --git a/helm/software/lambda-delta/basic_rg/brgSubstitution.ml b/helm/software/lambda-delta/basic_rg/brgSubstitution.ml index 40859b2d5..5c9d91a8b 100644 --- a/helm/software/lambda-delta/basic_rg/brgSubstitution.ml +++ b/helm/software/lambda-delta/basic_rg/brgSubstitution.ml @@ -10,6 +10,17 @@ V_______________________________________________________________ *) module B = Brg +(* module O = Output *) + +let rec icm a = function + | B.Sort _ + | B.LRef _ + | B.GRef _ -> succ a + | B.Bind (_, B.Void, t) -> icm (succ a) t + | B.Cast (_, u, t) -> icm (icm a u) t + | B.Appl (_, u, t) + | B.Bind (_, B.Abst u, t) + | B.Bind (_, B.Abbr u, t) -> icm (icm (succ a) u) t let iter map d = let rec iter_bind d = function @@ -30,4 +41,6 @@ let lift_map h _ a i = if i + h >= 0 then B.LRef (a, i + h) else assert false let lift h d t = - if h = 0 then t else iter (lift_map h) d t + if h = 0 then t else begin +(* O.icm := succ (* icm *) !O.icm (*t*); *) iter (lift_map h) d t + end diff --git a/helm/software/lambda-delta/basic_rg/brgType.ml b/helm/software/lambda-delta/basic_rg/brgType.ml index 79949a3a7..728e3ff41 100644 --- a/helm/software/lambda-delta/basic_rg/brgType.ml +++ b/helm/software/lambda-delta/basic_rg/brgType.ml @@ -66,7 +66,7 @@ let rec b_type_of err f st 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 + let h = H.apply g h in f x (B.Sort (a, h)) | B.LRef (_, i) -> begin match R.get m i with | B.Abst w -> diff --git a/helm/software/lambda-delta/common/hierarchy.ml b/helm/software/lambda-delta/common/hierarchy.ml index e00cfc72c..f8a58dc0f 100644 --- a/helm/software/lambda-delta/common/hierarchy.ml +++ b/helm/software/lambda-delta/common/hierarchy.ml @@ -25,15 +25,15 @@ let set_sort h s = (* Interface functions ******************************************************) -let set_sorts f ss i = - f (List.fold_left set_sort i ss) +let set_sorts ss i = + List.fold_left set_sort i ss let get_sort err f h = try f (H.find sort h) with Not_found -> err () -let string_of_graph f (s, _) = f s +let string_of_graph (s, _) = s -let apply f (_, g) h = f (g h) +let apply (_, g) h = (g h) let graph_of_string err f s = try diff --git a/helm/software/lambda-delta/common/hierarchy.mli b/helm/software/lambda-delta/common/hierarchy.mli index a0790321c..19e943054 100644 --- a/helm/software/lambda-delta/common/hierarchy.mli +++ b/helm/software/lambda-delta/common/hierarchy.mli @@ -11,12 +11,12 @@ type graph -val set_sorts: (int -> 'a) -> string list -> int -> 'a +val set_sorts: string list -> int -> int val get_sort: (unit -> 'a) -> (string -> 'a) -> int -> 'a val graph_of_string: (unit -> 'a) -> (graph -> 'a) -> string -> 'a -val string_of_graph: (string -> 'a) -> graph -> 'a +val string_of_graph: graph -> string -val apply: (int -> 'a) -> graph -> int -> 'a +val apply: graph -> int -> int diff --git a/helm/software/lambda-delta/common/library.ml b/helm/software/lambda-delta/common/library.ml index 61af97921..94ee60bd3 100644 --- a/helm/software/lambda-delta/common/library.ml +++ b/helm/software/lambda-delta/common/library.ml @@ -119,7 +119,7 @@ let export_entity pp_term si g (a, u, b) = | Y.Void -> assert false in let opts = if si then "si" else "" in - let shp = H.string_of_graph C.start g in + let shp = H.string_of_graph g in let attrs = ["hierarchy", shp; "options", opts] in tag root attrs ~contents out 0; close_out och diff --git a/helm/software/lambda-delta/common/output.ml b/helm/software/lambda-delta/common/output.ml index 6dd526bfb..c2e43d460 100644 --- a/helm/software/lambda-delta/common/output.ml +++ b/helm/software/lambda-delta/common/output.ml @@ -12,6 +12,8 @@ module P = Printf module L = Log +let icm = ref 0 + type reductions = { beta : int; zeta : int; @@ -67,6 +69,7 @@ let print_reductions () = L.warn (P.sprintf " Reference typing: %7u" rt); L.warn (P.sprintf " Local: %7u" r.lrt); L.warn (P.sprintf " Global: %7u" r.grt); - L.warn (P.sprintf " Sort inclusion: %7u" r.si) + L.warn (P.sprintf " Sort inclusion: %7u" r.si); + L.warn (P.sprintf " Relocated nodes (icm): %7u" !icm) let indexes = ref false diff --git a/helm/software/lambda-delta/common/output.mli b/helm/software/lambda-delta/common/output.mli index 812531585..679346a19 100644 --- a/helm/software/lambda-delta/common/output.mli +++ b/helm/software/lambda-delta/common/output.mli @@ -11,6 +11,8 @@ val indexes: bool ref +val icm: int ref + val clear_reductions: unit -> unit val add: diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index 1bab9136b..dff0bbe10 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -257,7 +257,7 @@ try let help_u = " activate sort inclusion" in let help_x = " export kernel entities (XML)" in L.box 0; L.box_err (); - H.set_sorts ignore ["Set"; "Prop"] 0; + let _ = H.set_sorts ["Set"; "Prop"] 0 in at_exit exit; Arg.parse [ ("-S", Arg.Int set_summary, help_S); -- 2.39.2