From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 12 Nov 2009 19:15:43 +0000 (+0000)
Subject: some interfaces improved
X-Git-Tag: make_still_working~3210
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ea41b1f6e212334924a8de4b2ff53b2586de9c4b;p=helm.git

some interfaces improved
---

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);