src/lib/log.cmx: src/lib/cps.cmx src/lib/log.cmi
src/lib/time.cmo: src/lib/log.cmi
src/lib/time.cmx: src/lib/log.cmx
-src/common/options.cmo: src/lib/cps.cmx
-src/common/options.cmx: src/lib/cps.cmx
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/level.cmi:
+src/common/level.cmo: src/common/level.cmi
+src/common/level.cmx: src/common/level.cmi
+src/common/entity.cmo: src/common/level.cmi
+src/common/entity.cmx: src/common/level.cmx
+src/common/options.cmo: src/lib/cps.cmx
+src/common/options.cmx: src/lib/cps.cmx
src/common/output.cmi:
src/common/output.cmo: src/common/options.cmx src/lib/log.cmi \
src/common/output.cmi
src/common/output.cmx: src/common/options.cmx src/lib/log.cmx \
src/common/output.cmi
-src/common/level.cmi:
-src/common/level.cmo: src/common/level.cmi
-src/common/level.cmx: src/common/level.cmi
-src/common/entity.cmo: src/common/options.cmx src/common/level.cmi
-src/common/entity.cmx: src/common/options.cmx src/common/level.cmx
src/common/marks.cmo: src/common/entity.cmx
src/common/marks.cmx: src/common/entity.cmx
src/common/alpha.cmi: src/common/entity.cmx
src/common/alpha.cmo: src/common/entity.cmx src/common/alpha.cmi
src/common/alpha.cmx: src/common/entity.cmx src/common/alpha.cmi
+src/common/ccs.cmi: src/common/entity.cmx
+src/common/ccs.cmo: src/common/options.cmx src/common/entity.cmx \
+ src/lib/cps.cmx src/common/ccs.cmi
+src/common/ccs.cmx: src/common/options.cmx src/common/entity.cmx \
+ src/lib/cps.cmx src/common/ccs.cmi
+src/common/status.cmo: src/common/options.cmx src/common/ccs.cmi
+src/common/status.cmx: src/common/options.cmx src/common/ccs.cmx
src/text/txt.cmo: src/common/level.cmi
src/text/txt.cmx: src/common/level.cmx
src/text/txtParser.cmi: src/text/txt.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/basic_ag/bagReduction.cmi
-src/basic_ag/bagType.cmi: src/common/entity.cmx src/basic_ag/bag.cmx
-src/basic_ag/bagType.cmo: src/lib/share.cmx src/lib/log.cmi \
- src/common/hierarchy.cmi src/common/entity.cmx src/lib/cps.cmx \
- src/basic_ag/bagReduction.cmi src/basic_ag/bagOutput.cmi \
+src/basic_ag/bagType.cmi: src/common/status.cmx src/basic_ag/bag.cmx
+src/basic_ag/bagType.cmo: src/common/status.cmx src/lib/share.cmx \
+ src/lib/log.cmi src/common/hierarchy.cmi src/common/entity.cmx \
+ src/lib/cps.cmx src/basic_ag/bagReduction.cmi src/basic_ag/bagOutput.cmi \
src/basic_ag/bagEnvironment.cmi src/basic_ag/bag.cmx \
src/basic_ag/bagType.cmi
-src/basic_ag/bagType.cmx: src/lib/share.cmx src/lib/log.cmx \
- src/common/hierarchy.cmx src/common/entity.cmx src/lib/cps.cmx \
- src/basic_ag/bagReduction.cmx src/basic_ag/bagOutput.cmx \
+src/basic_ag/bagType.cmx: src/common/status.cmx src/lib/share.cmx \
+ src/lib/log.cmx src/common/hierarchy.cmx src/common/entity.cmx \
+ src/lib/cps.cmx src/basic_ag/bagReduction.cmx src/basic_ag/bagOutput.cmx \
src/basic_ag/bagEnvironment.cmx src/basic_ag/bag.cmx \
src/basic_ag/bagType.cmi
-src/basic_ag/bagUntrusted.cmi: src/common/entity.cmx src/basic_ag/bag.cmx
+src/basic_ag/bagUntrusted.cmi: src/common/status.cmx src/basic_ag/bag.cmx
src/basic_ag/bagUntrusted.cmo: src/lib/log.cmi src/common/entity.cmx \
src/basic_ag/bagType.cmi src/basic_ag/bagEnvironment.cmi \
src/basic_ag/bag.cmx src/basic_ag/bagUntrusted.cmi
src/complete_rg/crgAut.cmx: src/common/options.cmx src/common/level.cmx \
src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
src/automath/aut.cmx src/complete_rg/crgAut.cmi
-src/xml/xmlLibrary.cmi: src/common/level.cmi src/common/entity.cmx
-src/xml/xmlLibrary.cmo: src/common/level.cmi src/common/hierarchy.cmi \
- src/common/entity.cmx src/lib/cps.cmx src/xml/xmlLibrary.cmi
-src/xml/xmlLibrary.cmx: src/common/level.cmx src/common/hierarchy.cmx \
- src/common/entity.cmx src/lib/cps.cmx src/xml/xmlLibrary.cmi
+src/xml/xmlLibrary.cmi: src/common/level.cmi src/common/entity.cmx \
+ src/common/ccs.cmi
+src/xml/xmlLibrary.cmo: src/common/options.cmx src/common/level.cmi \
+ src/common/hierarchy.cmi src/common/entity.cmx src/lib/cps.cmx \
+ src/common/ccs.cmi src/xml/xmlLibrary.cmi
+src/xml/xmlLibrary.cmx: src/common/options.cmx src/common/level.cmx \
+ src/common/hierarchy.cmx src/common/entity.cmx src/lib/cps.cmx \
+ src/common/ccs.cmx src/xml/xmlLibrary.cmi
src/xml/xmlCrg.cmi: src/xml/xmlLibrary.cmi src/complete_rg/crg.cmx
src/xml/xmlCrg.cmo: src/xml/xmlLibrary.cmi src/common/hierarchy.cmi \
src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
src/basic_rg/brgSubstitution.cmi
src/basic_rg/brgSubstitution.cmx: src/basic_rg/brg.cmx \
src/basic_rg/brgSubstitution.cmi
-src/basic_rg/brgReduction.cmi: src/lib/log.cmi src/common/entity.cmx \
- src/basic_rg/brg.cmx
-src/basic_rg/brgReduction.cmo: src/lib/share.cmx src/common/output.cmi \
- src/lib/log.cmi src/common/entity.cmx src/lib/cps.cmx \
+src/basic_rg/brgReduction.cmi: src/common/status.cmx src/lib/log.cmi \
+ src/common/entity.cmx src/basic_rg/brg.cmx
+src/basic_rg/brgReduction.cmo: src/common/status.cmx src/lib/share.cmx \
+ src/common/output.cmi src/lib/log.cmi src/common/level.cmi \
+ src/common/entity.cmx src/lib/cps.cmx src/common/ccs.cmi \
src/basic_rg/brgOutput.cmi src/basic_rg/brgEnvironment.cmi \
src/basic_rg/brg.cmx src/basic_rg/brgReduction.cmi
-src/basic_rg/brgReduction.cmx: src/lib/share.cmx src/common/output.cmx \
- src/lib/log.cmx src/common/entity.cmx src/lib/cps.cmx \
+src/basic_rg/brgReduction.cmx: src/common/status.cmx src/lib/share.cmx \
+ src/common/output.cmx src/lib/log.cmx src/common/level.cmx \
+ src/common/entity.cmx src/lib/cps.cmx src/common/ccs.cmx \
src/basic_rg/brgOutput.cmx src/basic_rg/brgEnvironment.cmx \
src/basic_rg/brg.cmx src/basic_rg/brgReduction.cmi
-src/basic_rg/brgType.cmi: src/lib/log.cmi src/common/entity.cmx \
+src/basic_rg/brgType.cmi: src/common/status.cmx src/lib/log.cmi \
src/basic_rg/brgReduction.cmi src/basic_rg/brg.cmx
src/basic_rg/brgType.cmo: src/lib/share.cmx src/lib/log.cmi \
src/common/level.cmi src/common/hierarchy.cmi src/common/entity.cmx \
src/lib/cps.cmx src/basic_rg/brgSubstitution.cmx \
src/basic_rg/brgReduction.cmx src/basic_rg/brgEnvironment.cmx \
src/basic_rg/brg.cmx src/basic_rg/brgType.cmi
-src/basic_rg/brgUntrusted.cmi: src/common/entity.cmx src/basic_rg/brgType.cmi \
+src/basic_rg/brgUntrusted.cmi: src/common/status.cmx src/basic_rg/brgType.cmi \
src/basic_rg/brg.cmx
src/basic_rg/brgUntrusted.cmo: src/lib/log.cmi src/common/entity.cmx \
src/basic_rg/brgType.cmi src/basic_rg/brgReduction.cmi \
src/toplevel/metaBrg.cmi
src/toplevel/top.cmo: src/xml/xmlLibrary.cmi src/xml/xmlCrg.cmi \
src/text/txtParser.cmi src/text/txtLexer.cmx src/text/txt.cmx \
- src/lib/time.cmx src/common/output.cmi src/common/options.cmx \
- src/toplevel/metaOutput.cmi src/toplevel/metaBrg.cmi \
- src/toplevel/metaBag.cmi src/toplevel/metaAut.cmi src/toplevel/meta.cmx \
- src/lib/log.cmi src/common/hierarchy.cmi src/common/entity.cmx \
- src/complete_rg/crgTxt.cmi src/complete_rg/crgAut.cmi \
- src/complete_rg/crg.cmx src/lib/cps.cmx src/basic_rg/brgUntrusted.cmi \
- src/basic_rg/brgReduction.cmi src/basic_rg/brgOutput.cmi \
- src/basic_rg/brgCrg.cmi src/basic_rg/brg.cmx \
+ src/lib/time.cmx src/common/status.cmx src/common/output.cmi \
+ src/common/options.cmx src/toplevel/metaOutput.cmi \
+ src/toplevel/metaBrg.cmi src/toplevel/metaBag.cmi \
+ src/toplevel/metaAut.cmi src/toplevel/meta.cmx src/lib/log.cmi \
+ src/common/hierarchy.cmi src/common/entity.cmx src/complete_rg/crgTxt.cmi \
+ src/complete_rg/crgAut.cmi src/complete_rg/crg.cmx src/lib/cps.cmx \
+ src/basic_rg/brgUntrusted.cmi src/basic_rg/brgReduction.cmi \
+ src/basic_rg/brgOutput.cmi src/basic_rg/brgCrg.cmi src/basic_rg/brg.cmx \
src/basic_ag/bagUntrusted.cmi src/basic_ag/bagType.cmi \
src/basic_ag/bagOutput.cmi src/basic_ag/bag.cmx \
src/automath/autProcess.cmi src/automath/autParser.cmi \
src/automath/autOutput.cmi src/automath/autLexer.cmx src/automath/aut.cmx
src/toplevel/top.cmx: src/xml/xmlLibrary.cmx src/xml/xmlCrg.cmx \
src/text/txtParser.cmx src/text/txtLexer.cmx src/text/txt.cmx \
- src/lib/time.cmx src/common/output.cmx src/common/options.cmx \
- src/toplevel/metaOutput.cmx src/toplevel/metaBrg.cmx \
- src/toplevel/metaBag.cmx src/toplevel/metaAut.cmx src/toplevel/meta.cmx \
- src/lib/log.cmx src/common/hierarchy.cmx src/common/entity.cmx \
- src/complete_rg/crgTxt.cmx src/complete_rg/crgAut.cmx \
- src/complete_rg/crg.cmx src/lib/cps.cmx src/basic_rg/brgUntrusted.cmx \
- src/basic_rg/brgReduction.cmx src/basic_rg/brgOutput.cmx \
- src/basic_rg/brgCrg.cmx src/basic_rg/brg.cmx \
+ src/lib/time.cmx src/common/status.cmx src/common/output.cmx \
+ src/common/options.cmx src/toplevel/metaOutput.cmx \
+ src/toplevel/metaBrg.cmx src/toplevel/metaBag.cmx \
+ src/toplevel/metaAut.cmx src/toplevel/meta.cmx src/lib/log.cmx \
+ src/common/hierarchy.cmx src/common/entity.cmx src/complete_rg/crgTxt.cmx \
+ src/complete_rg/crgAut.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
+ src/basic_rg/brgUntrusted.cmx src/basic_rg/brgReduction.cmx \
+ src/basic_rg/brgOutput.cmx src/basic_rg/brgCrg.cmx src/basic_rg/brg.cmx \
src/basic_ag/bagUntrusted.cmx src/basic_ag/bagType.cmx \
src/basic_ag/bagOutput.cmx src/basic_ag/bag.cmx \
src/automath/autProcess.cmx src/automath/autParser.cmx \
TAGS = test-si test-si-fast hal xml-si-crg xml-si profile
+XMLLINTLOCAL = --nonet --path xml --dtdvalid ld.dtd
+
XMLS = xml/brg-si/grundlagen/l/not.ld.xml \
xml/brg-si/grundlagen/l/et.ld.xml \
xml/brg-si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \
xml/crg-si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \
xml/crg-si/grundlagen/l/e/pairis1.ld.xml
-include Makefile.common
+LOCALXMLS = xml/brg-si/grundlagen/ccs.ldc.xml
-HOME = .
+include Makefile.common
INPUT = examples/grundlagen/grundlagen.aut
test-si: $(MAIN).opt etc
- @echo " HELENA -p -u $(INPUT)"
- $(H)./$(MAIN).opt -p -u -S 3 $(O) $(INPUT) > etc/log.txt
+ @echo " HELENA -p -u -c $(INPUT)"
+ $(H)./$(MAIN).opt -p -u -c -S 3 $(O) $(INPUT) > etc/log.txt
test-si-fast: $(MAIN).opt etc
@echo " HELENA -u -q $(INPUT)"
xml-si: $(MAIN).opt etc
@echo " HELENA -u -x -s 2 $(INPUT)"
- $(H)./$(MAIN).opt -u -x $(HOME) -s 2 -S 1 $(INPUT) > etc/log.txt
+ $(H)./$(MAIN).opt -u -x -s 2 -S 1 $(INPUT) > etc/log.txt
xml-si-crg: $(MAIN).opt etc
@echo " HELENA -u -x -s 1 $(INPUT)"
- $(H)./$(MAIN).opt -u -x $(HOME) -s 1 -S 1 $(INPUT) > etc/log.txt
+ $(H)./$(MAIN).opt -u -x -s 1 -S 1 $(INPUT) > etc/log.txt
etc:
@echo " MKDIR etc"
xml-si-old: $(MAIN).opt etc
@echo " HELENA -o -u -x -s 2 $(INPUT)"
- $(H)./$(MAIN).opt -o -u -x $(HOME) -s 2 -S 1 $(INPUT) > etc/log.txt
+ $(H)./$(MAIN).opt -o -u -x -s 2 -S 1 $(INPUT) > etc/log.txt
OCAMLLEX = ocamllex.opt
OCAMLYACC = ocamlyacc -v
XMLLINT = xmllint --noout
+
+
XSLT = xsltproc
#TAR = tar -czf etc/$(MAIN:%=%.tgz)
@echo XMLLINT --valid
$(H)$(XMLLINT) --valid $^
+lint-xml-local: $(LOCALXMLS)
+ @echo XMLLINT --valid
+ $(H)$(XMLLINT) $(XMLLINTLOCAL) --valid $^
+
#tgz: clean
# @echo " TAR -czf $(MAIN:%=%.tgz) . $(DIRECTORIES)"
# $(H)find -name "Make*" | xargs $(TAR) $(KEEP)
type message = (lenv, term) Log.item list
-(* helpers ******************************************************************)
-
-let mk_uri si root s =
- let kernel = if si then "bag-si" else "bag" in
- String.concat "/" ["ld:"; kernel; root; s ^ ".ld"]
-
(* Currified constructors ***************************************************)
let abst w = Abst w
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module S = Share
+module W = Share
module Z = Bag
(* Internal functions *******************************************************)
let rec lref_map_bind f map b = match b with
| Z.Abbr v ->
- let f v' = f (S.sh1 v v' b Z.abbr) in
+ let f v' = f (W.sh1 v v' b Z.abbr) in
lref_map f map v
| Z.Abst w ->
- let f w' = f (S.sh1 w w' b Z.abst) in
+ let f w' = f (W.sh1 w w' b Z.abst) in
lref_map f map w
| Z.Void -> f b
and lref_map f map t = match t with
| Z.LRef i ->
- let ii = map i in f (S.sh1 i ii t Z.lref)
+ let ii = map i in f (W.sh1 i ii t Z.lref)
| Z.GRef _ -> f t
| Z.Sort _ -> f t
| Z.Cast (w, u) ->
- let f w' u' = f (S.sh2 w w' u u' t Z.cast) in
+ let f w' u' = f (W.sh2 w w' u u' t Z.cast) in
let f w' = lref_map (f w') map u in
lref_map f map w
| Z.Appl (w, u) ->
- let f w' u' = f (S.sh2 w w' u u' t Z.appl) in
+ let f w' u' = f (W.sh2 w w' u u' t Z.appl) in
let f w' = lref_map (f w') map u in
lref_map f map w
| Z.Bind (l, id, b, u) ->
- let f b' u' = f (S.sh2 b b' u u' t (Z.bind l id)) in
+ let f b' u' = f (W.sh2 b b' u u' t (Z.bind l id)) in
let f b' = lref_map (f b') map u in
lref_map_bind f map b
module U = NUri
module C = Cps
-module S = Share
+module W = Share
module L = Log
module E = Entity
module H = Hierarchy
+module S = Status
module Z = Bag
module ZO = BagOutput
module ZE = BagEnvironment
ZE.get_entity f uri
| Z.Bind (l, id, Z.Abbr v, t) ->
let f xv xt tt =
- f (S.sh2 v xv t xt x (Z.bind_abbr l id)) (Z.bind_abbr l id xv tt)
+ f (W.sh2 v xv t xt x (Z.bind_abbr l id)) (Z.bind_abbr l id xv tt)
in
let f xv cc = b_type_of (f xv) st cc t in
let f xv = Z.push "type abbr" (f xv) c l id (Z.Abbr xv) in
type_of f st c v
| Z.Bind (l, id, Z.Abst u, t) ->
let f xu xt tt =
- f (S.sh2 u xu t xt x (Z.bind_abst l id)) (Z.bind_abst l id xu tt)
+ f (W.sh2 u xu t xt x (Z.bind_abst l id)) (Z.bind_abst l id xu tt)
in
let f xu cc = b_type_of (f xu) st cc t in
let f xu _ = Z.push "type abst" (f xu) c l id (Z.Abst xu) in
type_of f st c u
| Z.Bind (l, id, Z.Void, t) ->
let f xt tt =
- f (S.sh1 t xt x (Z.bind l id Z.Void)) (Z.bind l id Z.Void tt)
+ f (W.sh1 t xt x (Z.bind l id Z.Void)) (Z.bind l id Z.Void tt)
in
let f cc = b_type_of f st cc t in
Z.push "type void" f c l id Z.Void
L.unbox (succ level);
let f a =
(* L.warn (Printf.sprintf "Convertible: %b" a); *)
- if a then f (S.sh2 v xv t xt x Z.appl) (Z.appl xv tt)
+ if a then f (W.sh2 v xv t xt x Z.appl) (Z.appl xv tt)
else error3 c xv vv w
in
- ZR.are_convertible f ~si:st.E.si c w vv
+ ZR.are_convertible f ~si:st.S.si c w vv
| _ ->
error1 "not a function" c xt
in
| Z.Cast (u, t) ->
let f xu xt tt a =
(* L.warn (Printf.sprintf "Convertible: %b" a); *)
- if a then f (S.sh2 u xu t xt x Z.cast) xu else error3 c xt tt xu
+ if a then f (W.sh2 u xu t xt x Z.cast) xu else error3 c xt tt xu
in
- let f xu xt tt = ZR.are_convertible (f xu xt tt) ~si:st.E.si c xu tt in
+ let f xu xt tt = ZR.are_convertible (f xu xt tt) ~si:st.S.si c xu tt in
let f xu _ = b_type_of (f xu) st c t in
type_of f st c u
val type_of:
(Bag.term -> Bag.term -> 'a) ->
- Entity.status -> Bag.lenv -> Bag.term -> 'a
+ Status.status -> Bag.lenv -> Bag.term -> 'a
V_______________________________________________________________ *)
val type_check:
- (Bag.term -> Bag.entity -> 'a) -> Entity.status -> Bag.entity -> 'a
+ (Bag.term -> Bag.entity -> 'a) -> Status.status -> Bag.entity -> 'a
(* Cons: tail, relative local environment, attrs, binder *)
| Cons of lenv * lenv * attrs * bind
-(* helpers ******************************************************************)
-
-let mk_uri si root s =
- let kernel = if si then "brg-si" else "brg" in
- String.concat "/" ["ld:"; kernel; root; s ^ ".ld"]
-
(* Currified constructors ***************************************************)
let abst n w = Abst (n, w)
module U = NUri
module C = Cps
-module S = Share
+module W = Share
module L = Log
module E = Entity
+module N = Level
module O = Output
+module Q = Ccs
+module S = Status
module B = Brg
module BO = BrgOutput
module BE = BrgEnvironment
| B.Void, B.Void -> f ()
| _ -> err ()
in
- if S.eq t1 t2 then f () else aux f (t1, t2)
+ if W.eq t1 t2 then f () else aux f (t1, t2)
let get m i =
let _, c, a, b = B.get m.e i in c, a, b
| B.Sort _ -> m, None, x
| B.GRef (_, uri) ->
begin match BE.get_entity uri with
- | _, _, E.Abbr v when st.E.delta ->
+ | _, _, E.Abbr v when st.S.delta ->
O.add ~gdelta:1 (); step st m v
- | _, _, E.Abst (_, w) when st.E.rt ->
+ | _, _, E.Abst (_, w) when st.S.rt ->
O.add ~grt:1 (); step st m w
| a, _, E.Abbr v ->
let e = E.apix C.err C.start a in
| c, _, B.Abbr v ->
O.add ~ldelta:1 ();
step st {m with e = c} v
- | c, _, B.Abst (_, w) when st.E.rt ->
+ | c, _, B.Abst (_, w) when st.S.rt ->
O.add ~lrt:1 ();
step st {m with e = c} w
| c, _, B.Void ->
begin match m.s with
| [] -> m, None, x
| (c, v) :: s ->
- O.add ~beta:1 ~upsilon:(List.length s) ();
+ if N.is_zero n then Q.add_infinite st.S.cc a;
+ O.add ~beta:1 ~upsilon:(List.length s) ();
let e = B.push m.e c a (B.abbr v) (* (B.Cast ([], w, v)) *) in
step st {m with e = e; s = s} t
end
ac_nfs st (step st m1 v1) (m2, r2, t)
| _, B.Bind (a1, (B.Abst (n1, w1) as b1), t1),
_, B.Bind (a2, (B.Abst (n2, w2) as b2), t2) ->
- if (* n1 = n2 && *) ac {st with E.si = false} m1 w1 m2 w2 then
+ if n1 = n2 && ac {st with S.si = false} m1 w1 m2 w2 then
ac st (push m1 a1 b1) t1 (push m2 a2 b2) t2
else false
- | _, B.Sort _, _, B.Bind (a, b, t) when st.E.si ->
+ | _, B.Sort _, _, B.Bind (a, (B.Abst (n, _) as b), t)
+ when N.is_zero n && st.S.si ->
O.add ~si:1 ();
ac st (push m1 a b) u (push m2 a b) t
| _ -> false
if List.length m1.s <> List.length m2.s then false else
let map (c1, v1) (c2, v2) =
let m1, m2 = {m1 with e = c1; s = []}, {m2 with e = c2; s = []} in
- ac {st with E.si = false} m1 v1 m2 v2
+ ac {st with S.si = false} m1 v1 m2 v2
in
list_and map (m1.s, m2.s)
let xwhd st m t =
L.box level; log1 "Now scanning" m.e t;
- let m, _, t = step {st with E.delta = true; E.rt = true} m t in
+ let m, _, t = step {st with S.delta = true; S.rt = true} m t in
L.unbox level; m, t
let are_convertible st mu u mw w =
L.box level; log2 "Now converting" mu.e u mw.e w;
- let r = ac {st with E.delta = st.E.expand; E.rt = false} mu u mw w in
+ let r = ac {st with S.delta = st.S.expand; S.rt = false} mu u mw w in
L.unbox level; r
(* let err _ = in
- if S.eq mu mw then are_alpha_convertible err f u w else err () *)
+ if W.eq mu mw then are_alpha_convertible err f u w else err () *)
(* error reporting **********************************************************)
val push: kam -> Entity.attrs -> Brg.bind -> kam
-val xwhd: Entity.status -> kam -> Brg.term -> kam * Brg.term
+val xwhd: Status.status -> kam -> Brg.term -> kam * Brg.term
(* arguments: expected type, inferred type *)
val are_convertible:
- Entity.status -> kam -> Brg.term -> kam -> Brg.term -> bool
+ Status.status -> kam -> Brg.term -> kam -> Brg.term -> bool
val specs: (kam, Brg.term) Log.specs
module U = NUri
module C = Cps
-module S = Share
+module W = Share
module L = Log
module H = Hierarchy
module E = Entity
end
| B.Bind (a, B.Abbr v, t) ->
let f xv xt tt =
- f (S.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt)
+ f (W.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt)
in
let f xv m = b_type_of err (f xv) st m t in
let f xv = f xv (BR.push m a (B.abbr xv)) in
type_of err f st m v
| B.Bind (a, B.Abst (n, u), t) ->
let f xu xt tt =
- f (S.sh2 u xu t xt x (B.bind_abst n a)) (B.bind_abst (N.pred n) a xu tt)
+ f (W.sh2 u xu t xt x (B.bind_abst n a)) (B.bind_abst (N.pred n) a xu tt)
in
let f xu m = b_type_of err (f xu) st m t in
let f xu _ = f xu (BR.push m a (B.abst n xu)) in
type_of err f st m u
| B.Bind (a, B.Void, t) ->
let f xt tt =
- f (S.sh1 t xt x (B.bind_void a)) (B.bind_void a tt)
+ f (W.sh1 t xt x (B.bind_void a)) (B.bind_void a tt)
in
b_type_of err f st (BR.push m a B.Void) t
| B.Appl (a, v, t) ->
let f xv vv xt tt =
- let f _ = f (S.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt) in
+ let f _ = f (W.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt) in
assert_applicability err f st m tt vv xv
in
let f xv vv = b_type_of err (f xv vv) st m t in
type_of err f st m v
| B.Cast (a, u, t) ->
let f xu xt tt =
- let f _ = f (S.sh2 u xu t xt x (B.cast a)) xu in
+ let f _ = f (W.sh2 u xu t xt x (B.cast a)) xu in
assert_convertibility err f st m xu tt xt
in
let f xu _ = b_type_of err (f xu) st m t in
val type_of:
(message -> 'a) -> (Brg.term -> Brg.term -> 'a) ->
- Entity.status -> BrgReduction.kam -> Brg.term -> 'a
+ Status.status -> BrgReduction.kam -> Brg.term -> 'a
val type_check:
(BrgType.message -> 'a) -> (Brg.term -> Brg.entity -> 'a) ->
- Entity.status -> Brg.entity -> 'a
+ Status.status -> Brg.entity -> 'a
-options hierarchy output level entity marks alpha
+hierarchy level entity options output marks alpha ccs status
--- /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_______________________________________________________________ *)
+
+module L = List
+module U = NUri
+module C = Cps
+module E = Entity
+module G = Options
+
+type csys = {
+ uri: E.uri;
+ mutable is : int list
+}
+
+let mark a = E.mark C.err C.start a
+
+(* interface functions ******************************************************)
+
+let init () = {
+ uri = U.uri_of_string (G.get_baseuri ());
+ is = [];
+}
+
+let add_infinite s a =
+ if !G.si && !G.cc then
+ let i = abs (mark a) in
+ if L.mem i s.is then () else s.is <- i :: s.is
+ else ()
--- /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 csys = {
+ uri: Entity.uri;
+ mutable is : int list
+}
+
+val init: unit -> csys
+
+val add_infinite: csys -> Entity.attrs -> unit
V_______________________________________________________________ *)
module U = NUri
-module G = Options
module N = Level
type uri = U.uri
type 'term entity = attrs * uri * 'term bind (* attrs, name, binder *)
-type status = {
- delta: bool; (* global delta-expansion *)
- rt: bool; (* reference typing *)
- si: bool; (* sort inclusion *)
- expand: bool (* always expand global definitions *)
-}
-
(* helpers ******************************************************************)
let common f (a, u, _) = f a u
let f t = f (a, uri, Abbr t) in xlate_term f t
| _, _, Void ->
assert false
-
-let initial_status () = {
- delta = false; rt = false; si = !G.si; expand = !G.expand
-}
-
-let refresh_status st = {st with
- si = !G.si; expand = !G.expand
-}
-
type uri_generator = string -> string
+type kernel = Crg | Brg | Bag
+
(* interface functions ******************************************************)
-let indexes = ref false (* show de Bruijn indexes *)
+let xdir = ref ""
-let expand = ref false (* always expand global definitions *)
+let kernel = ref Brg
let si = ref false (* use sort inclusion *)
-let unquote = ref false (* do not quote identifiers when lexing *)
+let cover = ref "" (* initial uri segment *)
+
+let cc = ref false (* activate conversion constraints *)
+
+let expand = ref false (* always expand global definitions *)
+
+let indexes = ref false (* show de Bruijn indexes *)
let icm = ref 0 (* complexity measure of relocated terms *)
-let cover = ref "" (* initial uri segment *)
+let unquote = ref false (* do not quote identifiers when lexing *)
let debug_parser = ref false (* output parser debug information *)
let debug_lexer = ref false (* output lexer debug information *)
-let mk_uri = ref (fun _ _ -> C.err : bool -> string -> uri_generator)
+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 get_baseuri () =
+ String.concat "/" ["ld:"; kernel_id (); !cover ]
let get_mk_uri () =
- !mk_uri !si !cover
+ let bu = get_baseuri () in
+ fun s -> bu ^ "/" ^ s ^ ".ld"
let clear () =
- expand := false; si := false; cover := ""; indexes := false; icm := 0;
- debug_parser := false; debug_lexer := false;
- mk_uri := fun _ _ -> C.err
+ xdir := ""; kernel := Brg; si := false; cover := "";
+ expand := false; indexes := false; icm := 0; unquote := false;
+ debug_parser := false; debug_lexer := false
--- /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_______________________________________________________________ *)
+
+module G = Options
+module Q = Ccs
+
+type status = {
+ delta: bool; (* global delta-expansion *)
+ rt: bool; (* reference typing *)
+ si: bool; (* sort inclusion *)
+ expand: bool; (* always expand global definitions *)
+ cc: Q.csys; (* conversion constraints *)
+}
+
+(* helpers ******************************************************************)
+
+let initial_status () = {
+ delta = false; rt = false;
+ si = !G.si; expand = !G.expand; cc = Q.init ()
+}
+
+let refresh_status st = {st with
+ si = !G.si; expand = !G.expand; cc = Q.init ()
+}
+
(* helpers ******************************************************************)
-let mk_uri si root s =
- let kernel = if si then "crg-si" else "crg" in
- String.concat "/" ["ld:"; kernel; root; s ^ ".ld"]
-
let empty_lenv = ESort
let push_bind f lenv a b = f (EBind (lenv, a, b))
-(* free = F I P Q U V W *)
+(* free = F I P U V *)
module U = NUri
module K = NUri.UriHash
module C = cps
-module S = share
+module W = share (**)
module L = log
module Y = time (**)
-module G = options
module H = hierarchy
-module O = output
+module N = level
module E = entity
+module G = options
+module O = output
module J = marks (**)
module R = alpha
-module N = level
+module Q = ccs
+module S = status
module T = txt
module TP = txtParser
contract f tt
| T.Impl (n, true, id, w, t) ->
let f = function
- | T.Bind (n, T.Abst [xw], T.Bind (_, T.Abst xws, tt)) ->
+ | T.Bind (_, T.Abst [xw], T.Bind (n, T.Abst xws, tt)) ->
f (T.Bind (n, T.Abst (xw :: xws), tt))
| tt -> f tt
in
module H = Hierarchy
module O = Output
module E = Entity
+module S = Status
module XL = XmlLibrary
module XD = XmlCrg
module AA = AutProcess
mc : MO.counters;
brgc: BO.counters;
bagc: ZO.counters;
- kst : E.status
+ kst : S.status
}
let flush_all () = L.flush 0; L.flush_err ()
dst = AD.initial_status ();
tst = TD.initial_status ();
ast = AA.initial_status ();
- kst = E.initial_status ()
+ kst = S.initial_status ()
}
let refresh_status st = {st with
mst = MA.refresh_status st.mst;
dst = AD.refresh_status st.dst;
tst = TD.refresh_status st.tst;
- kst = E.refresh_status st.kst
+ kst = S.refresh_status st.kst
}
(* kernel related ***********************************************************)
-type kernel = Brg | Bag
-
type kernel_entity = BrgEntity of Brg.entity
| BagEntity of Bag.entity
| CrgEntity of Crg.entity
| MetaEntity of Meta.entity
-let kernel = ref Brg
-
-let print_counters st = match !kernel with
- | Brg -> BO.print_counters C.start st.brgc
- | Bag -> ZO.print_counters C.start st.bagc
+let print_counters st = function
+ | G.Brg -> BO.print_counters C.start st.brgc
+ | G.Bag -> ZO.print_counters C.start st.bagc
+ | G.Crg -> ()
-let xlate_entity entity = match !kernel, entity with
- | Brg, CrgEntity e ->
+let xlate_entity entity = match !G.kernel, entity with
+ | G.Brg, CrgEntity e ->
let f e = (BrgEntity e) in E.xlate f BD.brg_of_crg e
- | Brg, MetaEntity e ->
+ | G.Brg, MetaEntity e ->
let f e = (BrgEntity e) in E.xlate f MB.brg_of_meta e
- | Bag, MetaEntity e ->
+ | G.Bag, MetaEntity e ->
let f e = (BagEntity e) in E.xlate f MZ.bag_of_meta e
| _, entity -> entity
| BagEntity e -> {st with bagc = ZO.count_entity C.start st.bagc e}
| _ -> st
-let export_entity si xdir = function
- | CrgEntity e -> XL.export_entity XD.export_term si xdir e
- | BrgEntity e -> XL.export_entity BO.export_term si xdir e
+let export_entity = function
+ | CrgEntity e -> XL.export_entity XD.export_term e
+ | BrgEntity e -> XL.export_entity BO.export_term e
| MetaEntity _
| BagEntity _ -> ()
let progress = ref false
let preprocess = ref false
let root = ref ""
-let cc = ref false
-let export = ref ""
+let export = ref false
let old = ref false
let st = ref (initial_status ())
let streaming = ref false (* parsing style (temporary) *)
let process_2 st entity =
let st = if !L.level > 2 then count_entity st entity else st in
- if !export <> "" then export_entity !G.si !export entity;
+ if !export then export_entity entity;
if !stage > 2 then type_check st entity else st
let process_1 st entity =
if !progress then pp_progress entity;
let st = if !L.level > 2 then count_entity st entity else st in
- if !export <> "" && !stage = 1 then export_entity !G.si !export entity;
+ if !export && !stage = 1 then export_entity entity;
if !stage > 1 then process_2 st (xlate_entity entity) else st
let process_0 st entity =
let ich = open_in name in
let lexbuf = Lexing.from_channel ich in
let st = process st lexbuf input in
- close_in ich; st, input
+ close_in ich;
+ if !stage > 2 && !G.cc && !G.si then XL.export_csys st.kst.S.cc;
+ st, input
let main =
try
L.warn (P.sprintf "Unknown type hierarchy: %s" s)
in
let set_kernel = function
- | "brg" -> kernel := Brg
- | "bag" -> kernel := Bag
+ | "brg" -> G.kernel := G.Brg
+ | "bag" -> G.kernel := G.Bag
| s -> L.warn (P.sprintf "Unknown kernel version: %s" s)
in
let set_summary i = L.level := i in
let set_stage i = stage := i in
- let set_xdir s = export := s in
+ let set_xdir s = G.xdir := s in
let set_root s = root := s in
let clear_options () =
- stage := 3; progress := false; old := false;
- preprocess := false; root := ""; cc := false; export := "";
- kernel := Brg; st := initial_status ();
+ progress := false; old := false; export := false; preprocess := false;
+ stage := 3; root := "";
+ st := initial_status ();
L.clear (); G.clear (); H.clear (); O.clear_reductions ();
streaming := false;
in
L.warn (P.sprintf "Processing file: %s" name);
if !L.level > 0 then Y.utime_stamp "started";
let base_name = Filename.chop_extension (Filename.basename name) in
- let mk_uri =
- if !stage < 2 then Crg.mk_uri else
- match !kernel with
- | Brg -> Brg.mk_uri
- | Bag -> Bag.mk_uri
- in
let cover = F.concat !root base_name in
- G.mk_uri := mk_uri; G.cover := cover;
+ if !stage < 2 then G.kernel := G.Crg;
+ G.cover := cover;
let sst, input = process (refresh_status !st) name in
st := sst;
if !L.level > 0 then Y.utime_stamp "processed";
AO.print_counters C.start !st.ac;
if !preprocess then AO.print_process_counters C.start !st.ast;
if !stage > 0 then MO.print_counters C.start !st.mc;
- if !stage > 1 then print_counters !st;
+ if !stage > 1 then print_counters !st !G.kernel;
if !stage > 2 then O.print_reductions ()
end
in
flush_all ()
in
let help =
- "Usage: helena [ -LPVXcgijopqu1 | -Ss <number> | -x <dir> | -hkr <string> ]* [ <file> ]*\n\n" ^
+ "Usage: helena [ -LPVXcgijopqux1 | -Ss <number> | -O <dir> | -hkr <string> ]* [ <file> ]*\n\n" ^
"Summary levels: 0 just errors (default), 1 time stamps, 2 processed file names, \
3 data information, 4 typing information, 5 reduction information\n\n" ^
"Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n"
in
let help_L = " show lexer debug information" in
+ let help_O = "<dir> set location of output directory (XML) to <dir> (default: current directory)" in
let help_P = " show parser debug information" in
let help_S = "<number> set summary level (see above)" in
let help_V = " show version information" in
let help_X = " clear options" in
- let help_c = " output conversion constraints" in
+ let help_c = " read/write conversion constraints" in
let help_g = " always expand global definitions" in
- let help_h = "<string> set type hierarchy (default: Z1)" in
+ let help_h = "<string> set type hierarchy (default: \"Z1\")" in
let help_i = " show local references by index" in
let help_j = " show URI of processed kernel objects" in
- let help_k = "<string> set kernel version (default: brg)" in
+ let help_k = "<string> set kernel version (default: \"brg\")" in
let help_o = " use old abstract language instead of crg" in
let help_p = " preprocess source" in
let help_q = " disable quotation of identifiers" in
- let help_r = "<string> set initial segment of URI hierarchy" in
+ let help_r = "<string> set initial segment of URI hierarchy (default: empty)" in
let help_s = "<number> set translation stage (see above)" in
let help_u = " activate sort inclusion" in
- let help_x = "<dir> export kernel entities (XML) to <dir>" in
+ let help_x = " export kernel entities (XML)" in
let help_1 = " parse files with streaming policy" in
L.box 0; L.box_err ();
at_exit exit;
Arg.parse [
("-L", Arg.Set G.debug_lexer, help_L);
+ ("-O", Arg.String set_xdir, help_O);
("-P", Arg.Set G.debug_parser, help_P);
("-S", Arg.Int set_summary, help_S);
("-V", Arg.Unit print_version, help_V);
("-X", Arg.Unit clear_options, help_X);
- ("-c", Arg.Set cc, help_c);
+ ("-c", Arg.Set G.cc, help_c);
("-g", Arg.Set G.expand, help_g);
("-h", Arg.String set_hierarchy, help_h);
("-i", Arg.Set G.indexes, help_i);
("-r", Arg.String set_root, help_r);
("-s", Arg.Int set_stage, help_s);
("-u", Arg.Set G.si, help_u);
- ("-x", Arg.String set_xdir, help_x);
+ ("-x", Arg.Set export, help_x);
("-1", Arg.Set streaming, help_1);
] process_file help;
with ZT.TypeError msg -> bag_error "Type Error" msg
XL.tag XL.cast attrs ~contents:(exp_term e u) out tab;
exp_term e t out tab
| D.TAppl (a, vs, t) ->
- let attrs = [XL.arity (List.length vs)] in
+ let attrs = [XL.arity vs] in
XL.tag XL.appl attrs ~contents:(list_iter (exp_term e) vs) out tab;
exp_term e t out tab
| D.TProj (a, lenv, t) ->
match b with
| D.Abst (n, ws) ->
let e = D.push_bind C.start e a (D.Abst (n, ws)) in
- let attrs = [XL.level n; XL.name ns; XL.mark a; XL.arity (List.length ws)] in
+ let attrs = [XL.level n; XL.name ns; XL.mark a; XL.arity ws] in
XL.tag XL.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab
| D.Abbr vs ->
let e = D.push_bind C.start e a (D.Abbr vs) in
- let attrs = [XL.name ns; XL.mark a; XL.arity (List.length vs)] in
+ let attrs = [XL.name ns; XL.mark a; XL.arity vs] in
XL.tag XL.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab
| D.Void n ->
- let attrs = [XL.name a; XL.mark a; XL.arity n] in
+ let attrs = [XL.name a; XL.mark a; XL.arity ~n []] in
XL.tag XL.void attrs out tab
and exp_eproj e a lenv out tab =
module U = NUri
module C = Cps
module H = Hierarchy
+module G = Options
module E = Entity
module N = Level
+module Q = Ccs
(* internal functions *******************************************************)
let base = "xml"
-let obj_ext = ".xml"
+let ext = ".xml"
-let root = "ENTITY"
+let obj_root = "ENTITY"
+
+let ccs_name = "ccs.ldc"
+
+let ccs_root = "CCS"
let system = "http://helm.cs.unibo.it/lambda-delta/" ^ base ^ "/ld.dtd"
let uri u =
"uri", U.string_of_uri u
-let arity n =
+let arity ?n l =
+ let n = match n with
+ | None -> List.length l
+ | Some n -> n
+ in
let contents = if n > 1 then string_of_int n else "" in
"arity", contents
let f s = "meta", s in
E.meta err f a
-let export_entity pp_term si xdir (a, u, b) =
- let path = path_of_uri xdir u in
+let export_entity pp_term (a, u, b) =
+ let path = path_of_uri !G.xdir u in
let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in
- let och = open_out (path ^ obj_ext) in
+ let och = open_out (path ^ ext) in
let out = output_string och in
- xml out "1.0" "UTF-8"; doctype out root system;
+ xml out "1.0" "UTF-8"; doctype out obj_root system;
let a = E.Name (U.name_of_uri u, true) :: a in
let attrs = [uri u; name a; mark a; meta a] in
let contents = match b with
| E.Abbr v -> tag "ABBR" attrs ~contents:(pp_term v)
| E.Void -> assert false
in
- let opts = if si then "si" else "" in
+ let opts = if !G.si then "si" else "" in
let shp = H.string_of_graph () in
let attrs = ["hierarchy", shp; "options", opts] in
- tag root attrs ~contents out 0;
+ tag obj_root attrs ~contents out 0;
+ close_out och
+
+let marks = function
+ | [] -> "mark", ""
+ | l -> "mark", String.concat " " (List.rev_map string_of_int l)
+
+let export_csys s =
+ let path = path_of_uri !G.xdir s.Q.uri in
+ let _ = Sys.command (Printf.sprintf "mkdir -p %s" path) in
+ let name = F.concat path (ccs_name ^ ext) in
+ let och = open_out name in
+ let out = output_string och in
+ xml out "1.0" "UTF-8"; doctype out ccs_root system;
+ let attrs = [uri s.Q.uri] in
+ let contents = tag "ToInfinity" [arity s.Q.is; marks s.Q.is] in
+ tag ccs_root attrs ~contents out 0;
close_out och
type pp = och -> int -> unit
-val export_entity:
- ('term -> pp) -> bool -> string -> 'term Entity.entity -> unit
+val export_entity: ('term -> pp) -> 'term Entity.entity -> unit
+
+val export_csys: Ccs.csys -> unit
val tag: string -> attr list -> ?contents:pp -> pp
val uri: Entity.uri -> attr
-val arity: int -> attr
+val arity: ?n:int -> 'a list -> attr
val level: Level.level -> attr
meta CDATA #IMPLIED
>
-<!-- ROOT -->
-
<!ELEMENT ENTITY %entity;>
<!ATTLIST ENTITY
hierarchy NMTOKEN #REQUIRED
options NMTOKENS #IMPLIED
>
+
+<!-- CONVERSION CONSTRAINT SYSTEM -->
+
+<!ENTITY % ccs '(ToInfinity)'>
+
+<!ELEMENT ToInfinity EMPTY>
+<!ATTLIST ToInfinity
+ arity NMTOKEN #IMPLIED
+ mark NMTOKENS #IMPLIED
+>
+
+<!ELEMENT CCS %ccs;>
+<!ATTLIST CCS
+ uri CDATA #REQUIRED
+>
projects / helm.git / commitdiff