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
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 *******************************************************)
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;
(* Interface functions ******************************************************)
let empty_kam = {
- e = B.empty; s = []; i = 0
+ e = B.empty; s = []; d = 0
}
let get m i =
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
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
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 ->
(* 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
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
| 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
module P = Printf
module L = Log
+let icm = ref 0
+
type reductions = {
beta : int;
zeta : int;
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
val indexes: bool ref
+val icm: int ref
+
val clear_reductions: unit -> unit
val add:
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);
projects / helm.git / commitdiff