src/lib/log.cmx : src/lib/log.cmi
src/lib/time.cmo : src/lib/log.cmi
src/lib/time.cmx : src/lib/log.cmx
+src/lib/marks.cmi :
+src/lib/marks.cmo : src/lib/marks.cmi
+src/lib/marks.cmx : src/lib/marks.cmi
src/common/options.cmo : src/lib/cps.cmx
src/common/options.cmx : src/lib/cps.cmx
-src/common/marks.cmi :
-src/common/marks.cmo : src/common/marks.cmi
-src/common/marks.cmx : src/common/marks.cmi
src/common/hierarchy.cmi :
src/common/hierarchy.cmo : src/lib/cps.cmx src/common/hierarchy.cmi
src/common/hierarchy.cmx : src/lib/cps.cmx src/common/hierarchy.cmi
src/common/layer.cmi :
-src/common/layer.cmo : src/common/options.cmx src/common/marks.cmi \
+src/common/layer.cmo : src/common/options.cmx src/lib/marks.cmi \
src/lib/log.cmi src/common/layer.cmi
-src/common/layer.cmx : src/common/options.cmx src/common/marks.cmx \
+src/common/layer.cmx : src/common/options.cmx src/lib/marks.cmx \
src/lib/log.cmx src/common/layer.cmi
src/common/entity.cmo : src/common/layer.cmi
src/common/entity.cmx : src/common/layer.cmx
src/complete_rg/crg.cmx : src/common/layer.cmx src/common/entity.cmx \
src/lib/cps.cmx
src/complete_rg/crgOutput.cmi : src/common/layer.cmi src/complete_rg/crg.cmx
-src/complete_rg/crgOutput.cmo : src/common/marks.cmi src/lib/log.cmi \
+src/complete_rg/crgOutput.cmo : src/lib/marks.cmi src/lib/log.cmi \
src/common/layer.cmi src/common/entity.cmx src/complete_rg/crg.cmx \
src/lib/cps.cmx src/complete_rg/crgOutput.cmi
-src/complete_rg/crgOutput.cmx : src/common/marks.cmx src/lib/log.cmx \
+src/complete_rg/crgOutput.cmx : src/lib/marks.cmx src/lib/log.cmx \
src/common/layer.cmx src/common/entity.cmx src/complete_rg/crg.cmx \
src/lib/cps.cmx src/complete_rg/crgOutput.cmi
src/text/txt.cmo : src/common/layer.cmi
src/basic_rg/brgGrafite.cmx : src/common/options.cmx src/common/layer.cmx \
src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \
src/common/alpha.cmx src/basic_rg/brgGrafite.cmi
-src/basic_ag/bag.cmo : src/common/marks.cmi src/lib/log.cmi \
+src/basic_ag/bag.cmo : src/lib/marks.cmi src/lib/log.cmi \
src/common/entity.cmx src/lib/cps.cmx
-src/basic_ag/bag.cmx : src/common/marks.cmx src/lib/log.cmx \
+src/basic_ag/bag.cmx : src/lib/marks.cmx src/lib/log.cmx \
src/common/entity.cmx src/lib/cps.cmx
src/basic_ag/bagCrg.cmi : src/common/layer.cmi src/complete_rg/crg.cmx \
src/basic_ag/bag.cmx
-src/basic_ag/bagCrg.cmo : src/common/marks.cmi src/common/layer.cmi \
+src/basic_ag/bagCrg.cmo : src/lib/marks.cmi src/common/layer.cmi \
src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
src/basic_ag/bag.cmx src/basic_ag/bagCrg.cmi
-src/basic_ag/bagCrg.cmx : src/common/marks.cmx src/common/layer.cmx \
+src/basic_ag/bagCrg.cmx : src/lib/marks.cmx src/common/layer.cmx \
src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
src/basic_ag/bag.cmx src/basic_ag/bagCrg.cmi
src/basic_ag/bagOutput.cmi : src/xml/xmlLibrary.cmi src/lib/log.cmi \
src/common/layer.cmi src/basic_ag/bag.cmx
src/basic_ag/bagOutput.cmo : src/xml/xmlCrg.cmi src/common/options.cmx \
- src/common/marks.cmi src/lib/log.cmi src/common/hierarchy.cmi \
+ src/lib/marks.cmi src/lib/log.cmi src/common/hierarchy.cmi \
src/common/entity.cmx src/basic_ag/bagCrg.cmi src/basic_ag/bag.cmx \
src/basic_ag/bagOutput.cmi
src/basic_ag/bagOutput.cmx : src/xml/xmlCrg.cmx src/common/options.cmx \
- src/common/marks.cmx src/lib/log.cmx src/common/hierarchy.cmx \
+ src/lib/marks.cmx src/lib/log.cmx src/common/hierarchy.cmx \
src/common/entity.cmx src/basic_ag/bagCrg.cmx src/basic_ag/bag.cmx \
src/basic_ag/bagOutput.cmi
src/basic_ag/bagEnvironment.cmi : src/basic_ag/bag.cmx
src/basic_ag/bag.cmx src/basic_ag/bagEnvironment.cmi
src/basic_ag/bagEnvironment.cmx : src/lib/log.cmx src/common/entity.cmx \
src/basic_ag/bag.cmx src/basic_ag/bagEnvironment.cmi
-src/basic_ag/bagSubstitution.cmi : src/common/marks.cmi src/basic_ag/bag.cmx
+src/basic_ag/bagSubstitution.cmi : src/lib/marks.cmi src/basic_ag/bag.cmx
src/basic_ag/bagSubstitution.cmo : src/lib/share.cmx src/basic_ag/bag.cmx \
src/basic_ag/bagSubstitution.cmi
src/basic_ag/bagSubstitution.cmx : src/lib/share.cmx src/basic_ag/bag.cmx \
src/basic_ag/bagSubstitution.cmi
src/basic_ag/bagReduction.cmi : src/common/layer.cmi src/basic_ag/bag.cmx
-src/basic_ag/bagReduction.cmo : src/common/options.cmx src/common/marks.cmi \
+src/basic_ag/bagReduction.cmo : src/common/options.cmx src/lib/marks.cmi \
src/lib/log.cmi src/common/entity.cmx src/lib/cps.cmx \
src/basic_ag/bagSubstitution.cmi src/basic_ag/bagOutput.cmi \
src/basic_ag/bagEnvironment.cmi src/basic_ag/bag.cmx \
src/basic_ag/bagReduction.cmi
-src/basic_ag/bagReduction.cmx : src/common/options.cmx src/common/marks.cmx \
+src/basic_ag/bagReduction.cmx : src/common/options.cmx src/lib/marks.cmx \
src/lib/log.cmx src/common/entity.cmx src/lib/cps.cmx \
src/basic_ag/bagSubstitution.cmx src/basic_ag/bagOutput.cmx \
src/basic_ag/bagEnvironment.cmx src/basic_ag/bag.cmx \
src/toplevel/top.cmo : src/xml/xmlLibrary.cmi src/xml/xmlCrg.cmi \
src/text/txtParser.cmi src/text/txtLexer.cmx src/text/txtCrg.cmi \
src/text/txt.cmx src/lib/time.cmx src/common/output.cmi \
- src/common/options.cmx src/common/marks.cmi src/lib/log.cmi \
+ src/common/options.cmx src/lib/marks.cmi src/lib/log.cmi \
src/common/layer.cmi src/common/hierarchy.cmi src/common/entity.cmx \
src/complete_rg/crgOutput.cmi src/complete_rg/crg.cmx src/lib/cps.cmx \
src/basic_rg/brgUntrusted.cmi src/basic_rg/brgReduction.cmi \
src/toplevel/top.cmx : src/xml/xmlLibrary.cmx src/xml/xmlCrg.cmx \
src/text/txtParser.cmx src/text/txtLexer.cmx src/text/txtCrg.cmx \
src/text/txt.cmx src/lib/time.cmx src/common/output.cmx \
- src/common/options.cmx src/common/marks.cmx src/lib/log.cmx \
+ src/common/options.cmx src/lib/marks.cmx src/lib/log.cmx \
src/common/layer.cmx src/common/hierarchy.cmx src/common/entity.cmx \
src/complete_rg/crgOutput.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
src/basic_rg/brgUntrusted.cmx src/basic_rg/brgReduction.cmx \
CLEAN = etc/log.txt etc/profile.txt
-TAGS = test-si-fast test-si test-si-matita test profile xml-si-crg xml-si matita matitac
+TAGS = test-si-fast test-si test-si-matita test profile xml xml-v3 matita matitac
include Makefile.common
PREAMBLE = ../matita/matita.ma.templ
test-si-fast: $(MAIN).opt etc
- @echo " HELENA -o -q $(INPUTFAST)"
- $(H)./$(MAIN).opt -T 1 -o -q $(O) $(INPUTFAST) > etc/log.txt
+ @echo " HELENA -o -q -1 $(INPUTFAST)"
+ $(H)./$(MAIN).opt -T 1 -o -q -1 $(O) $(INPUTFAST) > etc/log.txt
test-si: $(MAIN).opt etc
@echo " HELENA -d -l -p -o $(INPUT)"
$(H)for T in `seq 31`; do ./$(MAIN).opt -T 1 -o -q $(O) $(INPUTFAST) >> etc/log.txt; done
$(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile-new.txt
-xml-si-crg: $(MAIN).opt etc
- @echo " HELENA -l -o -s 1 -x $(INPUT)"
- $(H)./$(MAIN).opt -O $(XMLDIR) -T 1 -l -o -s 1 -x $(INPUT) > etc/log.txt
+xml: $(MAIN).opt etc
+ @echo " HELENA -l -s 1 -x $(INPUT)"
+ $(H)./$(MAIN).opt -l -o $(INPUT) -X -O $(XMLDIR) -T 1 -l -s 1 -x $(INPUT) > etc/log.txt
-xml-si: $(MAIN).opt etc
- @echo " HELENA -l -o -s 2 -x $(INPUT)"
- $(H)./$(MAIN).opt -O $(XMLDIR) -T 1 -l -o -s 2 -x $(INPUT) > etc/log.txt
+xml-v3: $(MAIN).opt etc
+ @echo " HELENA -l -s 2 -x $(INPUT)"
+ $(H)./$(MAIN).opt -l -o $(INPUT) -X -O $(XMLDIR) -T 1 -l -s 3 -x $(INPUT) > etc/log.txt
matita: matita/$(MA)
@echo " MATITA $(MA)"
path = []; node = None; nodes = []; line = 1; mk_uri = G.get_mk_uri ();
}
-let refresh_status lst = {lst with
- mk_uri = G.get_mk_uri (); line = 1;
-}
+let refresh_status lst = initial_status ()
let crg_of_aut = xlate_entity
(* kernel version: basic, absolute, global *)
(* note : experimental *)
-module J = Marks
+module P = Marks
module E = Entity
type uri = E.uri
| Abbr of term (* abbreviation *)
and term = Sort of int (* hierarchy index *)
- | LRef of J.mark (* location *)
+ | LRef of P.mark (* location *)
| GRef of uri (* reference *)
| Cast of term * term (* domain, element *)
| Appl of term * term (* argument, function *)
- | Bind of attrs * J.mark * bind * term (* name, location, binder, scope *)
+ | Bind of attrs * P.mark * bind * term (* name, location, binder, scope *)
type entity = term E.entity (* attrs, uri, binder *)
-type lenv = (attrs * J.mark * bind) list (* name, location, binder *)
+type lenv = (attrs * P.mark * bind) list (* name, location, binder *)
type message = (lenv, term) Log.item list
V_______________________________________________________________ *)
module C = Cps
-module J = Marks
+module P = Marks
module N = Layer
module E = Entity
module D = Crg
and xlate_bind st f c a = function
| D.Abst (_, w) ->
- let f ww = Z.push "xlate_bind" f c a (J.new_mark ()) (Z.Abst ww) in
+ let f ww = Z.push "xlate_bind" f c a (P.new_mark ()) (Z.Abst ww) in
xlate_term st f c w
| D.Abbr v ->
- let f vv = Z.push "xlate_bind" f c a (J.new_mark ()) (Z.Abbr vv) in
+ let f vv = Z.push "xlate_bind" f c a (P.new_mark ()) (Z.Abbr vv) in
xlate_term st f c v
| D.Void ->
- Z.push "xlate_bind" f c a (J.new_mark ()) Z.Void
+ Z.push "xlate_bind" f c a (P.new_mark ()) Z.Void
(* internal functions: bag to crg term **************************************)
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module P = Printf
+module KP = Printf
module U = NUri
module L = Log
+module P = Marks
module G = Options
-module J = Marks
module H = Hierarchy
module E = Entity
module XD = XmlCrg
c.tabbrs
in
let items = c.eabsts + c.eabbrs in
- let locations = J.marks () in
- L.warn level (P.sprintf "Kernel representation summary (basic_ag)");
- L.warn level (P.sprintf " Total entry items: %7u" items);
- L.warn level (P.sprintf " Declaration items: %7u" c.eabsts);
- L.warn level (P.sprintf " Definition items: %7u" c.eabbrs);
- L.warn level (P.sprintf " Total term items: %7u" terms);
- L.warn level (P.sprintf " Sort items: %7u" c.tsorts);
- L.warn level (P.sprintf " Local reference items: %7u" c.tlrefs);
- L.warn level (P.sprintf " Global reference items: %7u" c.tgrefs);
- L.warn level (P.sprintf " Explicit Cast items: %7u" c.tcasts);
- L.warn level (P.sprintf " Application items: %7u" c.tappls);
- L.warn level (P.sprintf " Abstraction items: %7u" c.tabsts);
- L.warn level (P.sprintf " Abbreviation items: %7u" c.tabbrs);
- L.warn level (P.sprintf " Total binder locations: %7u" locations);
+ let locations = P.marks () in
+ L.warn level (KP.sprintf "Kernel representation summary (basic_ag)");
+ L.warn level (KP.sprintf " Total entry items: %7u" items);
+ L.warn level (KP.sprintf " Declaration items: %7u" c.eabsts);
+ L.warn level (KP.sprintf " Definition items: %7u" c.eabbrs);
+ L.warn level (KP.sprintf " Total term items: %7u" terms);
+ L.warn level (KP.sprintf " Sort items: %7u" c.tsorts);
+ L.warn level (KP.sprintf " Local reference items: %7u" c.tlrefs);
+ L.warn level (KP.sprintf " Global reference items: %7u" c.tgrefs);
+ L.warn level (KP.sprintf " Explicit Cast items: %7u" c.tcasts);
+ L.warn level (KP.sprintf " Application items: %7u" c.tappls);
+ L.warn level (KP.sprintf " Abstraction items: %7u" c.tabsts);
+ L.warn level (KP.sprintf " Abbreviation items: %7u" c.tabbrs);
+ L.warn level (KP.sprintf " Total binder locations: %7u" locations);
f ()
let name err och a =
let f n = function
- | true -> P.fprintf och "%s" n
- | false -> P.fprintf och "-%s" n
+ | true -> KP.fprintf och "%s" n
+ | false -> KP.fprintf och "-%s" n
in
E.name err f a
let res a l och =
- let err () = P.fprintf och "#%s" (J.string_of_mark l) in
+ let err () = KP.fprintf och "#%s" (P.string_of_mark l) in
if !G.indexes then err () else name err och a
let rec pp_term st c och = function
| Z.Sort h ->
- let err () = P.fprintf och "*%u" h in
- let f s = P.fprintf och "%s" s in
+ let err () = KP.fprintf och "*%u" h in
+ let f s = KP.fprintf och "%s" s in
H.string_of_sort err f h
| Z.LRef i ->
- let err () = P.fprintf och "#%s" (J.string_of_mark i) in
+ let err () = KP.fprintf och "#%s" (P.string_of_mark i) in
let f a _ = name err och a in
if !G.indexes then err () else Z.get err f c i
- | Z.GRef s -> P.fprintf och "$%s" (U.string_of_uri s)
+ | Z.GRef s -> KP.fprintf och "$%s" (U.string_of_uri s)
| Z.Cast (u, t) ->
- P.fprintf och "{%a}.%a" (pp_term st c) u (pp_term st c) t
+ KP.fprintf och "{%a}.%a" (pp_term st c) u (pp_term st c) t
| Z.Appl (v, t) ->
- P.fprintf och "(%a).%a" (pp_term st c) v (pp_term st c) t
+ KP.fprintf och "(%a).%a" (pp_term st c) v (pp_term st c) t
| Z.Bind (a, l, Z.Abst w, t) ->
let f cc =
- P.fprintf och "[%t:%a].%a" (res a l) (pp_term st c) w (pp_term st cc) t
+ KP.fprintf och "[%t:%a].%a" (res a l) (pp_term st c) w (pp_term st cc) t
in
Z.push "output abst" f c a l (Z.Abst w)
| Z.Bind (a, l, Z.Abbr v, t) ->
let f cc =
- P.fprintf och "[%t=%a].%a" (res a l) (pp_term st c) v (pp_term st cc) t
+ KP.fprintf och "[%t=%a].%a" (res a l) (pp_term st c) v (pp_term st cc) t
in
Z.push "output abbr" f c a l (Z.Abbr v)
| Z.Bind (a, l, Z.Void, t) ->
- let f cc = P.fprintf och "[%t].%a" (res a l) (pp_term st cc) t in
+ let f cc = KP.fprintf och "[%t].%a" (res a l) (pp_term st cc) t in
Z.push "output void" f c a l Z.Void
let pp_lenv st och c =
let pp_entry och = function
| a, l, Z.Abst w ->
- P.fprintf och "%t : %a\n" (res a l) (pp_term st c) w
+ KP.fprintf och "%t : %a\n" (res a l) (pp_term st c) w
| a, l, Z.Abbr v ->
- P.fprintf och "%t = %a\n" (res a l) (pp_term st c) v
+ KP.fprintf och "%t = %a\n" (res a l) (pp_term st c) v
| a, l, Z.Void ->
- P.fprintf och "%t\n" (res a l)
+ KP.fprintf och "%t\n" (res a l)
in
let iter map och l = List.iter (map och) l in
- let f es = P.fprintf och "%a" (iter pp_entry) (List.rev es) in
+ let f es = KP.fprintf och "%a" (iter pp_entry) (List.rev es) in
Z.contents f c
let specs = {
module U = NUri
module C = Cps
module L = Log
+module P = Marks
module G = Options
-module J = Marks
module E = Entity
module Z = Bag
module ZO = BagOutput
type whd_result =
| Sort_ of int
- | LRef_ of J.mark * Z.term option
+ | LRef_ of P.mark * Z.term option
| GRef_ of Z.entity
- | Bind_ of Z.attrs * J.mark * Z.term * Z.term
+ | Bind_ of Z.attrs * P.mark * Z.term * Z.term
type ho_whd_result =
| Sort of int
begin match m.s with
| [] -> f m (Bind_ (a, l, w, t))
| v :: tl ->
- let nl = J.new_mark () in
+ let nl = P.new_mark () in
let f mc = ZS.subst (whd f c {m with c = mc; s = tl}) nl l t in
Z.push "!" f m.c a nl (Z.Abbr (Z.Cast (w, v)))
end
| Z.Bind (a, l, b, t) ->
- let nl = J.new_mark () in
+ let nl = P.new_mark () in
let f mc = ZS.subst (whd f c {m with c = mc}) nl l t in
Z.push "!" f m.c a nl b
| GRef_ (_, _, _, E.Abbr v1), _ ->
whd (aux_rev m2 r2) c m1 v1
| Bind_ (a1, l1, w1, t1), Bind_ (a2, l2, w2, t2) ->
- let l = J.new_mark () in
+ let l = P.new_mark () in
let h c =
let m1, m2 = inc m1, inc m2 in
let f t1 = ZS.subst (are_convertible f st a c m1 t1 m2) l l2 t2 in
-options marks hierarchy layer entity output alpha
+options hierarchy layer entity output alpha
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module H = Hashtbl
+module KH = Hashtbl
module L = Log
+module P = Marks
module G = Options
-module J = Marks
type value = Inf (* infinite layer *)
| Fin of int (* finite layer *)
- | Ref of J.mark * int (* referred layer, step *)
+ | Ref of P.mark * int (* referred layer, step *)
| Unk (* no layer set *)
type layer = {
mutable b: bool; (* beta allowed? *)
}
-type status = (J.mark, layer) H.t (* environment for layer variables *)
+type status = (P.mark, layer) KH.t (* environment for layer variables *)
(* Internal functions *******************************************************)
let string_of_value k = function
| Inf -> ""
| Fin i -> string_of_int i
- | Ref (k, i) -> "-" ^ J.string_of_mark k ^ "-" ^ string_of_int i
- | Unk -> "-" ^ J.string_of_mark k
+ | Ref (k, i) -> "-" ^ P.string_of_mark k ^ "-" ^ string_of_int i
+ | Unk -> "-" ^ P.string_of_mark k
(* Note: remove assigned variables *)
let pp_table st =
let map k n =
warn (Printf.sprintf "%s: v %s (s:%b b:%b)"
- (J.string_of_mark k) (string_of_value k n.v) n.s n.b
+ (P.string_of_mark k) (string_of_value k n.v) n.s n.b
)
in
- H.iter map st
+ KH.iter map st
let cell s v = {
v = v; s = s; b = false
let dynamic k i = cell false (Ref (k, i))
let find_with_default st default k =
- try H.find st k with Not_found -> H.add st k default; default
+ try KH.find st k with Not_found -> KH.add st k default; default
let find st k =
- try H.find st k with Not_found -> assert false
+ try KH.find st k with Not_found -> assert false
let rec resolve_key_with_default st default k = match find_with_default st default k with
| {v = Ref (k, i)} when i = 0 -> resolve_key_with_default st default k
let resolve_layer st = function
| {v = Ref (k, i)} when i = 0 -> resolve_key st k
- | cell -> J.null_mark, cell
+ | cell -> P.null_mark, cell
let rec generated st h i =
let default = dynamic h i in
- let k = J.new_mark () in
+ let k = P.new_mark () in
let k, n = resolve_key_with_default st default k in
if n.s then generated st h i else begin
- if n <> default then H.replace st k default;
+ if n <> default then KH.replace st k default;
if !G.trace >= level then pp_table st; default
end
let rec aux (k, n) j = match n.v with
| Fin i when i = j -> true
| Fin i ->
- Printf.printf "binder %s is %u but must be %u\n" (J.string_of_mark k) i j; true (**)
+ Printf.printf "binder %s is %u but must be %u\n" (P.string_of_mark k) i j; true (**)
| Inf ->
- Printf.printf "binder %s is infinite but must be %u\n" (J.string_of_mark k) j; true (**)
+ Printf.printf "binder %s is infinite but must be %u\n" (P.string_of_mark k) j; true (**)
| Unk -> n.v <- Fin j; if !G.trace >= level then pp_table st; true
| Ref (k, i) -> n.v <- Fin j; aux (resolve_key st k) (i+j)
in
let k, n = resolve_layer st n in
(* if j = 0 && n.b then begin
- Printf.printf "^Pi reduction on binder %s\n" (J.string_of_mark k); false (**)
+ Printf.printf "^Pi reduction on binder %s\n" (P.string_of_mark k); false (**)
end else *)
aux (k, n) j
let rec aux (k, n) = match n.v with
| Inf -> true
| Fin i ->
- Printf.printf "binder %s is %u but must be infinite\n" (J.string_of_mark k) i; true (**)
+ Printf.printf "binder %s is %u but must be infinite\n" (P.string_of_mark k) i; true (**)
| Unk -> n.v <- Inf; if !G.trace >= level then pp_table st; true
| Ref (k, _) -> n.v <- Inf; aux (resolve_key st k)
in
(* Interface functions ******************************************************)
let initial_status () =
- H.create env_size
+ KH.create env_size
let refresh_status st = st
let rec unknown st =
if !G.trace >= level then warn "UNKNOWN";
let default = empty () in
- let k = J.new_mark () in
+ let k = P.new_mark () in
let k, n = resolve_key_with_default st default k in
if n.s then match n.v with
| Inf
| Fin i when i > j -> cell false (Fin (i - j))
| Fin _ -> cell false zero
| Unk ->
- if k = J.null_mark then assert false else generated st k j
+ if k = P.null_mark then assert false else generated st k j
| Ref (k, i) ->
let k, n = resolve_key st k in
aux k n (i+j)
match n.b, n.v with
| true, _ -> n.b
(* | _ , Fin i when i = 0 ->
- Printf.printf "^Pi reduction on binder %s\n" (J.string_of_mark k); false *) (**)
-(* if n.s && n.v = Fin 1 then Printf.printf "Pi reduction on binder %s\n" (J.string_of_mark k); *)
+ Printf.printf "^Pi reduction on binder %s\n" (P.string_of_mark k); false *) (**)
+(* if n.s && n.v = Fin 1 then Printf.printf "Pi reduction on binder %s\n" (P.string_of_mark k); *)
| _ -> n.b <- true; if !G.trace >= level then pp_table st; n.b
let assert_zero st n = assert_finite st n 0
else false
in begin
if !G.trace >= level then warn "ASSERT EQUAL";
- if b && k1 <> J.null_mark && k2 <> J.null_mark then begin
+ if b && k1 <> P.null_mark && k2 <> P.null_mark then begin
n1.v <- Ref (k2, 0); if !G.trace >= level then pp_table st
end; b end
+++ /dev/null
-(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department, University of Bologna, Italy.
- ||I||
- ||T|| HELM is free software; you can redistribute it and/or
- ||A|| modify it under the terms of the GNU General Public License
- \ / version 2 or (at your option) any later version.
- \ / This software is distributed as is, NO WARRANTY.
- V_______________________________________________________________ *)
-
-type mark = int
-
-let mark = ref 0
-
-(* interface functions ******************************************************)
-
-let marks () = !mark
-
-let new_mark () =
- incr mark; !mark
-
-let null_mark = 0
-
-let string_of_mark i = string_of_int i
-
-let clear_marks () =
- mark := 0
+++ /dev/null
-(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department, University of Bologna, Italy.
- ||I||
- ||T|| HELM is free software; you can redistribute it and/or
- ||A|| modify it under the terms of the GNU General Public License
- \ / version 2 or (at your option) any later version.
- \ / This software is distributed as is, NO WARRANTY.
- V_______________________________________________________________ *)
-
-type mark
-
-val marks: unit -> int
-
-val new_mark: unit -> mark
-
-val null_mark: mark
-
-val string_of_mark: mark -> string
-
-val clear_marks: unit -> unit
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module F = Filename
+module KF = Filename
module C = Cps
type uri_generator = string -> string
-type kernel = Crg | Brg | Bag
+type kernel = V4 | V3 | V0
(* interface functions ******************************************************)
let xdir = ref "" (* directory for XML output *)
-let kernel = ref Brg (* kernel type *)
+let kernel = ref V3 (* kernel type *)
let si = ref false (* use sort inclusion *)
let alpha = ref "" (* prefix of numeric identifiers *)
-let kernel_id () =
- let id = match !kernel with
- | Crg -> "crg"
- | Brg -> "brg"
- | Bag -> "bag"
- in
- let si = if !si then "_si" else "" in
- id ^ si
+let kernel_id () = match !kernel with
+ | V4 -> ""
+ | V3 -> "V3"
+ | V0 -> "V0"
let get_baseuri () =
String.concat "/" ["ld:"; kernel_id (); !cover; "" ]
let get_mk_uri () =
let bu = get_baseuri () in
- fun s -> F.concat bu (s ^ ".ld")
+ fun s -> KF.concat bu (s ^ ".ld")
let clear () =
stage := 3; trace := 0; summary := false;
- xdir := ""; kernel := Brg; si := false; cover := "";
+ xdir := ""; kernel := V3; si := false; cover := "";
expand := false; indexes := false; icm := 0; unquote := false;
debug_parser := false; debug_lexer := false;
ma_dir := ""; ma_preamble := ""
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module P = Printf
+module KP = Printf
module U = NUri
module C = Cps
module L = Log
-module J = Marks
+module P = Marks
module N = Layer
module E = Entity
module D = Crg
in
let items = c.eabsts + c.eabbrs in
let nodes = c.nodes + c.xnodes in
- let marks = J.marks () in
- L.warn level (P.sprintf "Intermediate representation summary (complete_rg)");
- L.warn level (P.sprintf " Total entry items: %7u" items);
- L.warn level (P.sprintf " Declaration items: %7u" c.eabsts);
- L.warn level (P.sprintf " Definition items: %7u" c.eabbrs);
- L.warn level (P.sprintf " Total term items: %7u" terms);
- L.warn level (P.sprintf " Sort items: %7u" c.tsorts);
- L.warn level (P.sprintf " Local reference items: %7u" c.tlrefs);
- L.warn level (P.sprintf " Global reference items: %7u" c.tgrefs);
- L.warn level (P.sprintf " Explicit Cast items: %7u" c.tcasts);
- L.warn level (P.sprintf " Application items: %7u" c.tappls);
- L.warn level (P.sprintf " Abstraction items: %7u" c.tabsts);
- L.warn level (P.sprintf " Abbreviation items: %7u" c.tabbrs);
- L.warn level (P.sprintf " Ambiguous abstractions: %7u" marks);
- L.warn level (P.sprintf " Global Int. Complexity: %7u" c.nodes);
- L.warn level (P.sprintf " + Abbreviation nodes: %7u" nodes);
+ let marks = P.marks () in
+ L.warn level (KP.sprintf "Intermediate representation summary (complete_rg)");
+ L.warn level (KP.sprintf " Total entry items: %7u" items);
+ L.warn level (KP.sprintf " Declaration items: %7u" c.eabsts);
+ L.warn level (KP.sprintf " Definition items: %7u" c.eabbrs);
+ L.warn level (KP.sprintf " Total term items: %7u" terms);
+ L.warn level (KP.sprintf " Sort items: %7u" c.tsorts);
+ L.warn level (KP.sprintf " Local reference items: %7u" c.tlrefs);
+ L.warn level (KP.sprintf " Global reference items: %7u" c.tgrefs);
+ L.warn level (KP.sprintf " Explicit Cast items: %7u" c.tcasts);
+ L.warn level (KP.sprintf " Application items: %7u" c.tappls);
+ L.warn level (KP.sprintf " Abstraction items: %7u" c.tabsts);
+ L.warn level (KP.sprintf " Abbreviation items: %7u" c.tabbrs);
+ L.warn level (KP.sprintf " Ambiguous abstractions: %7u" marks);
+ L.warn level (KP.sprintf " Global Int. Complexity: %7u" c.nodes);
+ L.warn level (KP.sprintf " + Abbreviation nodes: %7u" nodes);
f ()
(* term/environment pretty printer ******************************************)
let pp_attrs out a =
- let f s b = if b then out (P.sprintf "%s;" s) else out (P.sprintf "~%s;" s) in
+ let f s b = if b then out (KP.sprintf "%s;" s) else out (KP.sprintf "~%s;" s) in
E.name ignore f a;
- out (P.sprintf "+%i;" a.E.n_apix)
+ out (KP.sprintf "+%i;" a.E.n_apix)
let rec pp_term out st = function
- | D.TSort (a, l) -> pp_attrs out a; out (P.sprintf "*%u" l)
- | D.TLRef (a, i ) -> pp_attrs out a; out (P.sprintf "#%u" i)
- | D.TGRef (a, u) -> pp_attrs out a; out (P.sprintf "$")
+ | D.TSort (a, l) -> pp_attrs out a; out (KP.sprintf "*%u" l)
+ | D.TLRef (a, i ) -> pp_attrs out a; out (KP.sprintf "#%u" i)
+ | D.TGRef (a, u) -> pp_attrs out a; out (KP.sprintf "$")
| D.TCast (a, x, y) -> pp_attrs out a; out "<"; pp_term out st x; out ">."; pp_term out st y
| D.TAppl (a, x, y) -> pp_attrs out a; out "("; pp_term out st x; out ")."; pp_term out st y
| D.TBind (a, x, y) -> pp_attrs out a; pp_bind out st x; out "."; pp_term out st y
-cps share log time
+cps share log time marks
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+type mark = int
+
+let mark = ref 0
+
+(* interface functions ******************************************************)
+
+let marks () = !mark
+
+let new_mark () =
+ incr mark; !mark
+
+let null_mark = 0
+
+let string_of_mark i = string_of_int i
+
+let clear_marks () =
+ mark := 0
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+type mark
+
+val marks: unit -> int
+
+val new_mark: unit -> mark
+
+val null_mark: mark
+
+val string_of_mark: mark -> string
+
+val clear_marks: unit -> unit
-(* free = F I K M P Q U V W *)
+(* free = F I J M Q U V W *)
+
+module KF = Filename
+module KH = Hashtbl
+module KP = Printf
module U = NUri
module UH = NUri.UriHash
module S = Share
module L = Log
module Y = Time (**)
+module P = Marks
module G = Options
-module J = Marks (**)
module H = Hierarchy
module N = Layer
module E = Entity
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module F = Filename
-module P = Printf
+module KF = Filename
+module KP = Printf
module U = NUri
module C = Cps
module L = Log
module Y = Time
+module P = Marks
module G = Options
-module J = Marks
module H = Hierarchy
module N = Layer
module E = Entity
| CrgEntity of Crg.entity
let print_counters st = function
- | G.Crg -> DO.print_counters C.start st.dc
- | G.Brg -> BO.print_counters C.start st.bc
- | G.Bag -> ZO.print_counters C.start st.zc
+ | G.V4 -> DO.print_counters C.start st.dc
+ | G.V3 -> BO.print_counters C.start st.bc
+ | G.V0 -> ZO.print_counters C.start st.zc
let xlate_entity st entity = match !G.kernel, entity with
- | G.Brg, CrgEntity e ->
+ | G.V3, CrgEntity e ->
let f e = (BrgEntity e) in E.xlate f BD.brg_of_crg e
- | G.Bag, CrgEntity e ->
+ | G.V0, CrgEntity e ->
let f e = (BagEntity e) in E.xlate f (ZD.bag_of_crg st.kst) e
| _, entity -> entity
let pp_progress e =
let f _ na u =
let s = U.string_of_uri u in
- L.warn 2 (P.sprintf "[%u] <%s>" na.E.n_apix s);
+ L.warn 2 (KP.sprintf "[%u] <%s>" na.E.n_apix s);
in
Y.utime_stamp "intermediate";
match e with
| NoEntity
let type_of_input name =
- if F.check_suffix name ".hln" then Text
- else if F.check_suffix name ".aut" then
+ if KF.check_suffix name ".hln" then Text
+ else if KF.check_suffix name ".aut" then
let _ = H.set_sorts 0 ["Set"; "Prop"] in
assert (H.set_graph "Z2");
Automath
else begin
- L.warn level (P.sprintf "Unknown file type: %s" name); exit 2
+ L.warn level (KP.sprintf "Unknown file type: %s" name); exit 2
end
let txt_xl = initial_lexer TxtLexer.token
let print_version () = L.warn level (G.version_string ^ "\n"); exit 0 in
let set_hierarchy s =
if H.set_graph s then () else
- L.warn level (P.sprintf "Unknown type hierarchy: %s" s)
+ L.warn level (KP.sprintf "Unknown type hierarchy: %s" s)
in
let set_kernel = function
- | "brg" -> G.kernel := G.Brg
- | "bag" -> G.kernel := G.Bag
- | s -> L.warn level (P.sprintf "Unknown kernel version: %s" s)
+ | "V3" -> G.kernel := G.V3
+ | "V0" -> G.kernel := G.V0
+ | s -> L.warn level (KP.sprintf "Unknown kernel version: %s" s)
in
let set_trace i =
if !G.trace = 0 && i > 0 then Y.gmtime G.version_string;
version := true
in
let process_file name =
- if !G.trace >= 2 then L.warn 1 (P.sprintf "Processing file: %s" name);
+ if !G.trace >= 2 then L.warn 1 (KP.sprintf "Processing file: %s" name);
if !G.trace >= 2 then Y.utime_stamp "started";
let base_name = Filename.chop_extension (Filename.basename name) in
- let cover = F.concat !root base_name in
- if !G.stage <= 1 then G.kernel := G.Crg;
+ let cover = KF.concat !root base_name in
+ if !G.stage <= 1 then G.kernel := G.V4;
G.cover := cover;
if !G.ma_preamble <> "" then st := {!st with och = Some (BG.open_out base_name)};
- J.clear_marks ();
+ P.clear_marks ();
let sst, input = process (refresh_status !st) name in
st := begin match sst.och with
| None -> sst
if !G.summary then begin
AO.print_counters C.start !st.ac;
if !preprocess then AO.print_process_counters C.start !st.pst;
- if !G.stage >= 1 then print_counters !st G.Crg;
+ if !G.stage >= 1 then print_counters !st G.V4;
if !G.stage >= 2 then print_counters !st !G.kernel;
if !G.stage >= 3 then O.print_reductions ()
end
let help_g = " always expand global definitions" in
let help_h = "<string> set type hierarchy (default: \"Z1\")" in
let help_i = " show local references by index" in
- let help_k = "<string> set kernel version (default: \"brg\")" in
+ let help_k = "<string> set kernel version (default: \"V3\")" in
let help_l = " disambiguate binders level (Automath)" in
let help_m = "<file> export kernel entities (Grafite) setting location of preamble to <file> (default: empty)" in
let help_o = " activate sort inclusion (default: false)" in
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module F = Filename
+module KF = Filename
-module U = NUri
-module C = Cps
-module G = Options
-module H = Hierarchy
-module N = Layer
-module E = Entity
+module U = NUri
+module C = Cps
+module G = Options
+module H = Hierarchy
+module N = Layer
+module E = Entity
(* internal functions *******************************************************)
let ext = ".xml"
-let obj_root = "ENTITY"
+let obj_root = "CONSTANT"
let home = "http://lambdadelta.info/"
-let system = F.concat (F.concat home base) "ld.dtd"
+let system = KF.concat (KF.concat home base) "ld.dtd"
let xmlns = "xmlns", home
let path_of_uri xdir uri =
- let base = F.concat xdir base in
- F.concat base (Str.string_after (U.string_of_uri uri) 3)
+ let base = KF.concat xdir base in
+ KF.concat base (Str.string_after (U.string_of_uri uri) 3)
(* interface functions ******************************************************)
let export_entity pp_term (ra, na, u, b) =
let path = path_of_uri !G.xdir u in
- let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in
+ let _ = Sys.command (Printf.sprintf "mkdir -p %s" (KF.dirname path)) in
let och = open_out (path ^ ext) in
let out = output_string och in
xml out "1.0" "UTF-8"; doctype out obj_root system;
| E.Abbr v -> tag "GDef" attrs ~contents:(pp_term v)
| E.Void -> assert false
in
- let opts = if !G.si then "si" else "" in
let shp = H.string_of_graph () in
- let attrs = [xmlns; "hierarchy", shp; "options", opts] in
+ let attrs = [xmlns; "hierarchy", shp] in
tag obj_root attrs ~contents out 0;
close_out och
BIB = lambdadelta.bib
CONTRIB = lambdadelta_2.tar.gz
-XMLS = brg_si/grundlagen/l/not.ld.xml \
- brg_si/grundlagen/l/et.ld.xml \
- brg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \
- brg_si/grundlagen/l/e/pairis1.ld.xml \
- brg_si/grundlagen/l/e/st/eq/landau/n/327/t25.ld.xml \
- crg_si/grundlagen/l/not.ld.xml \
- crg_si/grundlagen/l/et.ld.xml \
- crg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \
- crg_si/grundlagen/l/e/pairis1.ld.xml \
- crg_si/grundlagen/l/e/st/eq/landau/n/327/t25.ld.xml \
- brg_si/grundlagen/ccs.ldc.xml
+XMLS = grundlagen_2/l/not.ld.xml \
+ grundlagen_2/l/et.ld.xml \
+ grundlagen_2/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \
+ grundlagen_2/l/e/pairis1.ld.xml \
+ grundlagen_2/l/e/st/eq/landau/n/327/t25.ld.xml \
LDWEB = ld_web.xsl ld_web_root.xsl ld_web_library.xsl
<!-- ENVIRONMENT ENTRIES -->
-<!ENTITY % entity '(GDec|GDef)'>
+<!ENTITY % constant '(GDec|GDef)'>
<!ELEMENT GDec %term;>
<!ATTLIST GDec
info CDATA #IMPLIED
>
-<!ELEMENT ENTITY %entity;>
-<!ATTLIST ENTITY
+<!ELEMENT CONSTANT %constant;>
+<!ATTLIST CONSTANT
xmlns CDATA #FIXED "http://lambdadelta.info/"
hierarchy NMTOKEN #REQUIRED
- options NMTOKENS #IMPLIED
>
projects / helm.git / commitdiff