common/entity.cmo: lib/nUri.cmi automath/aut.cmx
common/entity.cmx: lib/nUri.cmx automath/aut.cmx
common/library.cmi: common/hierarchy.cmi common/entity.cmx
-common/library.cmo: lib/nUri.cmi common/hierarchy.cmi common/library.cmi
-common/library.cmx: lib/nUri.cmx common/hierarchy.cmx common/library.cmi
+common/library.cmo: lib/nUri.cmi common/hierarchy.cmi common/entity.cmx \
+ lib/cps.cmx common/library.cmi
+common/library.cmx: lib/nUri.cmx common/hierarchy.cmx common/entity.cmx \
+ lib/cps.cmx common/library.cmi
basic_ag/bag.cmo: lib/log.cmi common/entity.cmx lib/cps.cmx
basic_ag/bag.cmx: lib/log.cmx common/entity.cmx lib/cps.cmx
basic_ag/bagOutput.cmi: lib/log.cmi basic_ag/bag.cmx
basic_ag/bagOutput.cmo: common/output.cmi lib/nUri.cmi lib/log.cmi \
- common/hierarchy.cmi basic_ag/bag.cmx basic_ag/bagOutput.cmi
+ common/hierarchy.cmi common/entity.cmx basic_ag/bag.cmx \
+ basic_ag/bagOutput.cmi
basic_ag/bagOutput.cmx: common/output.cmx lib/nUri.cmx lib/log.cmx \
- common/hierarchy.cmx basic_ag/bag.cmx basic_ag/bagOutput.cmi
+ common/hierarchy.cmx common/entity.cmx basic_ag/bag.cmx \
+ basic_ag/bagOutput.cmi
basic_ag/bagEnvironment.cmi: basic_ag/bag.cmx
-basic_ag/bagEnvironment.cmo: lib/nUri.cmi lib/log.cmi basic_ag/bag.cmx \
- basic_ag/bagEnvironment.cmi
-basic_ag/bagEnvironment.cmx: lib/nUri.cmx lib/log.cmx basic_ag/bag.cmx \
- basic_ag/bagEnvironment.cmi
+basic_ag/bagEnvironment.cmo: lib/nUri.cmi lib/log.cmi common/entity.cmx \
+ basic_ag/bag.cmx basic_ag/bagEnvironment.cmi
+basic_ag/bagEnvironment.cmx: lib/nUri.cmx lib/log.cmx common/entity.cmx \
+ basic_ag/bag.cmx basic_ag/bagEnvironment.cmi
basic_ag/bagSubstitution.cmi: basic_ag/bag.cmx
basic_ag/bagSubstitution.cmo: lib/share.cmx basic_ag/bag.cmx \
basic_ag/bagSubstitution.cmi
basic_ag/bagSubstitution.cmx: lib/share.cmx basic_ag/bag.cmx \
basic_ag/bagSubstitution.cmi
basic_ag/bagReduction.cmi: basic_ag/bag.cmx
-basic_ag/bagReduction.cmo: lib/nUri.cmi lib/log.cmi lib/cps.cmx \
- basic_ag/bagSubstitution.cmi basic_ag/bagOutput.cmi \
+basic_ag/bagReduction.cmo: lib/nUri.cmi lib/log.cmi common/entity.cmx \
+ lib/cps.cmx basic_ag/bagSubstitution.cmi basic_ag/bagOutput.cmi \
basic_ag/bagEnvironment.cmi basic_ag/bag.cmx basic_ag/bagReduction.cmi
-basic_ag/bagReduction.cmx: lib/nUri.cmx lib/log.cmx lib/cps.cmx \
- basic_ag/bagSubstitution.cmx basic_ag/bagOutput.cmx \
+basic_ag/bagReduction.cmx: lib/nUri.cmx lib/log.cmx common/entity.cmx \
+ lib/cps.cmx basic_ag/bagSubstitution.cmx basic_ag/bagOutput.cmx \
basic_ag/bagEnvironment.cmx basic_ag/bag.cmx basic_ag/bagReduction.cmi
basic_ag/bagType.cmi: common/hierarchy.cmi basic_ag/bag.cmx
basic_ag/bagType.cmo: lib/share.cmx lib/nUri.cmi lib/log.cmi \
- common/hierarchy.cmi lib/cps.cmx basic_ag/bagReduction.cmi \
- basic_ag/bagOutput.cmi basic_ag/bagEnvironment.cmi basic_ag/bag.cmx \
- basic_ag/bagType.cmi
+ common/hierarchy.cmi common/entity.cmx lib/cps.cmx \
+ basic_ag/bagReduction.cmi basic_ag/bagOutput.cmi \
+ basic_ag/bagEnvironment.cmi basic_ag/bag.cmx basic_ag/bagType.cmi
basic_ag/bagType.cmx: lib/share.cmx lib/nUri.cmx lib/log.cmx \
- common/hierarchy.cmx lib/cps.cmx basic_ag/bagReduction.cmx \
- basic_ag/bagOutput.cmx basic_ag/bagEnvironment.cmx basic_ag/bag.cmx \
- basic_ag/bagType.cmi
+ common/hierarchy.cmx common/entity.cmx lib/cps.cmx \
+ basic_ag/bagReduction.cmx basic_ag/bagOutput.cmx \
+ basic_ag/bagEnvironment.cmx basic_ag/bag.cmx basic_ag/bagType.cmi
basic_ag/bagUntrusted.cmi: common/hierarchy.cmi basic_ag/bag.cmx
-basic_ag/bagUntrusted.cmo: lib/log.cmi basic_ag/bagType.cmi \
- basic_ag/bagEnvironment.cmi basic_ag/bag.cmx basic_ag/bagUntrusted.cmi
-basic_ag/bagUntrusted.cmx: lib/log.cmx basic_ag/bagType.cmx \
- basic_ag/bagEnvironment.cmx basic_ag/bag.cmx basic_ag/bagUntrusted.cmi
+basic_ag/bagUntrusted.cmo: lib/nUri.cmi lib/log.cmi common/entity.cmx \
+ basic_ag/bagType.cmi basic_ag/bagEnvironment.cmi basic_ag/bag.cmx \
+ basic_ag/bagUntrusted.cmi
+basic_ag/bagUntrusted.cmx: lib/nUri.cmx lib/log.cmx common/entity.cmx \
+ basic_ag/bagType.cmx basic_ag/bagEnvironment.cmx basic_ag/bag.cmx \
+ basic_ag/bagUntrusted.cmi
basic_rg/brg.cmo: common/entity.cmx
basic_rg/brg.cmx: common/entity.cmx
-basic_rg/brgOutput.cmi: lib/log.cmi common/entity.cmx basic_rg/brg.cmx
+basic_rg/brgOutput.cmi: lib/log.cmi basic_rg/brg.cmx
basic_rg/brgOutput.cmo: common/output.cmi lib/nUri.cmi lib/log.cmi \
- common/hierarchy.cmi lib/cps.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi
+ common/library.cmi common/hierarchy.cmi common/entity.cmx lib/cps.cmx \
+ basic_rg/brg.cmx basic_rg/brgOutput.cmi
basic_rg/brgOutput.cmx: common/output.cmx lib/nUri.cmx lib/log.cmx \
- common/hierarchy.cmx lib/cps.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi
+ common/library.cmx common/hierarchy.cmx common/entity.cmx lib/cps.cmx \
+ basic_rg/brg.cmx basic_rg/brgOutput.cmi
basic_rg/brgEnvironment.cmi: basic_rg/brg.cmx
-basic_rg/brgEnvironment.cmo: lib/nUri.cmi basic_rg/brg.cmx \
+basic_rg/brgEnvironment.cmo: lib/nUri.cmi common/entity.cmx basic_rg/brg.cmx \
basic_rg/brgEnvironment.cmi
-basic_rg/brgEnvironment.cmx: lib/nUri.cmx basic_rg/brg.cmx \
+basic_rg/brgEnvironment.cmx: lib/nUri.cmx common/entity.cmx basic_rg/brg.cmx \
basic_rg/brgEnvironment.cmi
basic_rg/brgSubstitution.cmi: basic_rg/brg.cmx
basic_rg/brgSubstitution.cmo: basic_rg/brg.cmx basic_rg/brgSubstitution.cmi
basic_rg/brgSubstitution.cmx: basic_rg/brg.cmx basic_rg/brgSubstitution.cmi
basic_rg/brgReduction.cmi: lib/log.cmi basic_rg/brg.cmx
basic_rg/brgReduction.cmo: lib/share.cmx common/output.cmi lib/nUri.cmi \
- lib/log.cmi lib/cps.cmx basic_rg/brgOutput.cmi \
+ lib/log.cmi common/entity.cmx lib/cps.cmx basic_rg/brgOutput.cmi \
basic_rg/brgEnvironment.cmi basic_rg/brg.cmx basic_rg/brgReduction.cmi
basic_rg/brgReduction.cmx: lib/share.cmx common/output.cmx lib/nUri.cmx \
- lib/log.cmx lib/cps.cmx basic_rg/brgOutput.cmx \
+ lib/log.cmx common/entity.cmx lib/cps.cmx basic_rg/brgOutput.cmx \
basic_rg/brgEnvironment.cmx basic_rg/brg.cmx basic_rg/brgReduction.cmi
basic_rg/brgType.cmi: lib/log.cmi common/hierarchy.cmi \
basic_rg/brgReduction.cmi basic_rg/brg.cmx
basic_rg/brgType.cmo: lib/share.cmx lib/nUri.cmi lib/log.cmi \
- common/hierarchy.cmi lib/cps.cmx basic_rg/brgSubstitution.cmi \
- basic_rg/brgReduction.cmi basic_rg/brgOutput.cmi \
- basic_rg/brgEnvironment.cmi basic_rg/brg.cmx basic_rg/brgType.cmi
+ common/hierarchy.cmi common/entity.cmx lib/cps.cmx \
+ basic_rg/brgSubstitution.cmi basic_rg/brgReduction.cmi \
+ basic_rg/brgOutput.cmi basic_rg/brgEnvironment.cmi basic_rg/brg.cmx \
+ basic_rg/brgType.cmi
basic_rg/brgType.cmx: lib/share.cmx lib/nUri.cmx lib/log.cmx \
- common/hierarchy.cmx lib/cps.cmx basic_rg/brgSubstitution.cmx \
- basic_rg/brgReduction.cmx basic_rg/brgOutput.cmx \
- basic_rg/brgEnvironment.cmx basic_rg/brg.cmx basic_rg/brgType.cmi
+ common/hierarchy.cmx common/entity.cmx lib/cps.cmx \
+ basic_rg/brgSubstitution.cmx basic_rg/brgReduction.cmx \
+ basic_rg/brgOutput.cmx basic_rg/brgEnvironment.cmx basic_rg/brg.cmx \
+ basic_rg/brgType.cmi
basic_rg/brgUntrusted.cmi: common/hierarchy.cmi basic_rg/brgType.cmi \
basic_rg/brg.cmx
-basic_rg/brgUntrusted.cmo: lib/log.cmi basic_rg/brgType.cmi \
- basic_rg/brgReduction.cmi basic_rg/brgEnvironment.cmi basic_rg/brg.cmx \
- basic_rg/brgUntrusted.cmi
-basic_rg/brgUntrusted.cmx: lib/log.cmx basic_rg/brgType.cmx \
- basic_rg/brgReduction.cmx basic_rg/brgEnvironment.cmx basic_rg/brg.cmx \
- basic_rg/brgUntrusted.cmi
+basic_rg/brgUntrusted.cmo: lib/nUri.cmi lib/log.cmi common/entity.cmx \
+ basic_rg/brgType.cmi basic_rg/brgReduction.cmi \
+ basic_rg/brgEnvironment.cmi basic_rg/brg.cmx basic_rg/brgUntrusted.cmi
+basic_rg/brgUntrusted.cmx: lib/nUri.cmx lib/log.cmx common/entity.cmx \
+ basic_rg/brgType.cmx basic_rg/brgReduction.cmx \
+ basic_rg/brgEnvironment.cmx basic_rg/brg.cmx basic_rg/brgUntrusted.cmi
dual_rg/drg.cmo: common/entity.cmx
dual_rg/drg.cmx: common/entity.cmx
+dual_rg/drgOutput.cmi: common/library.cmi dual_rg/drg.cmx
+dual_rg/drgOutput.cmo: common/library.cmi dual_rg/drg.cmx \
+ dual_rg/drgOutput.cmi
+dual_rg/drgOutput.cmx: common/library.cmx dual_rg/drg.cmx \
+ dual_rg/drgOutput.cmi
dual_rg/drgAut.cmi: common/entity.cmx dual_rg/drg.cmx automath/aut.cmx
dual_rg/drgAut.cmo: lib/nUri.cmi common/entity.cmx dual_rg/drg.cmx \
lib/cps.cmx automath/aut.cmx dual_rg/drgAut.cmi
toplevel/meta.cmx: common/entity.cmx
toplevel/metaOutput.cmi: toplevel/meta.cmx
toplevel/metaOutput.cmo: lib/nUri.cmi toplevel/meta.cmx lib/log.cmi \
- lib/cps.cmx toplevel/metaOutput.cmi
+ common/entity.cmx lib/cps.cmx toplevel/metaOutput.cmi
toplevel/metaOutput.cmx: lib/nUri.cmx toplevel/meta.cmx lib/log.cmx \
- lib/cps.cmx toplevel/metaOutput.cmi
+ common/entity.cmx lib/cps.cmx toplevel/metaOutput.cmi
toplevel/metaLibrary.cmi: toplevel/meta.cmx
toplevel/metaLibrary.cmo: toplevel/metaOutput.cmi toplevel/metaLibrary.cmi
toplevel/metaLibrary.cmx: toplevel/metaOutput.cmx toplevel/metaLibrary.cmi
toplevel/metaAut.cmi: toplevel/meta.cmx automath/aut.cmx
-toplevel/metaAut.cmo: lib/nUri.cmi toplevel/meta.cmx lib/cps.cmx \
- automath/aut.cmx toplevel/metaAut.cmi
-toplevel/metaAut.cmx: lib/nUri.cmx toplevel/meta.cmx lib/cps.cmx \
- automath/aut.cmx toplevel/metaAut.cmi
+toplevel/metaAut.cmo: lib/nUri.cmi toplevel/meta.cmx common/entity.cmx \
+ lib/cps.cmx automath/aut.cmx toplevel/metaAut.cmi
+toplevel/metaAut.cmx: lib/nUri.cmx toplevel/meta.cmx common/entity.cmx \
+ lib/cps.cmx automath/aut.cmx toplevel/metaAut.cmi
toplevel/metaBag.cmi: toplevel/meta.cmx basic_ag/bag.cmx
toplevel/metaBag.cmo: toplevel/meta.cmx lib/cps.cmx basic_ag/bag.cmx \
toplevel/metaBag.cmi
toplevel/metaBag.cmx: toplevel/meta.cmx lib/cps.cmx basic_ag/bag.cmx \
toplevel/metaBag.cmi
toplevel/metaBrg.cmi: toplevel/meta.cmx basic_rg/brg.cmx
-toplevel/metaBrg.cmo: toplevel/meta.cmx lib/cps.cmx basic_rg/brg.cmx \
- toplevel/metaBrg.cmi
-toplevel/metaBrg.cmx: toplevel/meta.cmx lib/cps.cmx basic_rg/brg.cmx \
- toplevel/metaBrg.cmi
+toplevel/metaBrg.cmo: toplevel/meta.cmx common/entity.cmx lib/cps.cmx \
+ basic_rg/brg.cmx toplevel/metaBrg.cmi
+toplevel/metaBrg.cmx: toplevel/meta.cmx common/entity.cmx lib/cps.cmx \
+ basic_rg/brg.cmx toplevel/metaBrg.cmi
toplevel/top.cmo: lib/time.cmx common/output.cmi lib/nUri.cmi \
toplevel/metaOutput.cmi toplevel/metaLibrary.cmi toplevel/metaBrg.cmi \
toplevel/metaBag.cmi toplevel/metaAut.cmi lib/log.cmi common/library.cmi \
- common/hierarchy.cmi lib/cps.cmx basic_rg/brgUntrusted.cmi \
- basic_rg/brgReduction.cmi basic_rg/brgOutput.cmi basic_rg/brg.cmx \
- basic_ag/bagUntrusted.cmi basic_ag/bagType.cmi basic_ag/bagOutput.cmi \
- basic_ag/bag.cmx automath/autProcess.cmi automath/autParser.cmi \
- automath/autOutput.cmi automath/autLexer.cmx
+ common/hierarchy.cmi common/entity.cmx lib/cps.cmx \
+ basic_rg/brgUntrusted.cmi basic_rg/brgReduction.cmi \
+ basic_rg/brgOutput.cmi basic_rg/brg.cmx basic_ag/bagUntrusted.cmi \
+ basic_ag/bagType.cmi basic_ag/bagOutput.cmi basic_ag/bag.cmx \
+ automath/autProcess.cmi automath/autParser.cmi automath/autOutput.cmi \
+ automath/autLexer.cmx
toplevel/top.cmx: lib/time.cmx common/output.cmx lib/nUri.cmx \
toplevel/metaOutput.cmx toplevel/metaLibrary.cmx toplevel/metaBrg.cmx \
toplevel/metaBag.cmx toplevel/metaAut.cmx lib/log.cmx common/library.cmx \
- common/hierarchy.cmx lib/cps.cmx basic_rg/brgUntrusted.cmx \
- basic_rg/brgReduction.cmx basic_rg/brgOutput.cmx basic_rg/brg.cmx \
- basic_ag/bagUntrusted.cmx basic_ag/bagType.cmx basic_ag/bagOutput.cmx \
- basic_ag/bag.cmx automath/autProcess.cmx automath/autParser.cmx \
- automath/autOutput.cmx automath/autLexer.cmx
+ common/hierarchy.cmx common/entity.cmx lib/cps.cmx \
+ basic_rg/brgUntrusted.cmx basic_rg/brgReduction.cmx \
+ basic_rg/brgOutput.cmx basic_rg/brg.cmx basic_ag/bagUntrusted.cmx \
+ basic_ag/bagType.cmx basic_ag/bagOutput.cmx basic_ag/bag.cmx \
+ automath/autProcess.cmx automath/autParser.cmx automath/autOutput.cmx \
+ automath/autLexer.cmx
INPUT-ORIG = automath/grundlagen-orig.aut
test: $(MAIN).opt
- @echo " HELENA -a -r $(INPUT)"
- $(H)./$(MAIN).opt -a -r -S 3 $(O) $(INPUT) > etc/log.txt
+ @echo " HELENA -p -r $(INPUT)"
+ $(H)./$(MAIN).opt -p -r -S 3 $(O) $(INPUT) > etc/log.txt
test-si: $(MAIN).opt
- @echo " HELENA -a -r -u $(INPUT)"
- $(H)./$(MAIN).opt -a -r -u -S 3 $(O) $(INPUT) > etc/log.txt
+ @echo " HELENA -p -r -u $(INPUT)"
+ $(H)./$(MAIN).opt -p -r -u -S 3 $(O) $(INPUT) > etc/log.txt
test-si-fast: $(MAIN).opt
@echo " HELENA -r -u $(INPUT)"
OCAMLYACC = ocamlyacc -v
XMLLINT = xmllint --noout
XSLT = xsltproc
-TAR = tar -czf $(MAIN:%=%.tgz)
+TAR = tar -czf etc/$(MAIN:%=%.tgz)
define DIR_TEMPLATE
MODULES += $$(addprefix $(1)/,$$(shell cat $(1)/Make))
| Appl of term * term (* argument, function *)
| Bind of int * id * bind * term (* location, name, binder, scope *)
-type entry = bind Entity.entry (* age, uri, binder *)
-
-type entity = bind Entity.entity
+type entity = term Entity.entity (* attrs, uri, binder *)
type lenv = (int * id * bind) list (* location, name, binder *)
module U = NUri
module L = Log
module H = U.UriHash
+module Y = Entity
module B = Bag
exception ObjectNotFound of B.message
let hsize = 7000
let env = H.create hsize
-let age = ref 1
(* Internal functions *******************************************************)
+let get_age =
+ let age = ref 0 in
+ fun () -> incr age; !age
+
let error uri = raise (ObjectNotFound (L.items1 (U.string_of_uri uri)))
(* Interface functions ******************************************************)
-let set_entry f entry =
- let _, uri, b = entry in
- let entry = !age, uri, b in
- incr age; H.add env uri entry; f entry
+let set_entity f (a, uri, b) =
+ let age = get_age () in
+ let entry = (Y.Apix age :: a), uri, b in
+ H.add env uri entry; f entry
-let get_entry f uri =
+let get_entity f uri =
try f (H.find env uri) with Not_found -> error uri
exception ObjectNotFound of Bag.message
-val set_entry: (Bag.entry -> 'a) -> Bag.entry -> 'a
+val set_entity: (Bag.entity -> 'a) -> Bag.entity -> 'a
-val get_entry: (Bag.entry -> 'a) -> Bag.uri -> 'a
+val get_entity: (Bag.entity -> 'a) -> Bag.uri -> 'a
module F = Format
module U = NUri
module L = Log
+module Y = Entity
module H = Hierarchy
module O = Output
module B = Bag
let f c = count_term_binder f c b in
count_term f c t
-let count_entry_binder f c = function
- | B.Abst w ->
+let count_entity f c = function
+ | _, _, Y.Abst w ->
let c = {c with eabsts = succ c.eabsts} in
count_term f c w
- | B.Abbr v ->
+ | _, _, Y.Abbr v ->
let c = {c with eabbrs = succ c.eabbrs} in
count_term f c v
- | B.Void -> f c
-
-let count_entry f c (_, _, b) =
- count_entry_binder f c b
-
-let count_entity f c = function
- | Some entry -> count_entry f c entry
- | None -> f c
let print_counters f c =
let terms =
module U = NUri
module C = Cps
module L = Log
+module Y = Entity
module B = Bag
module O = BagOutput
module E = BagEnvironment
type whd_result =
| Sort_ of int
| LRef_ of int * B.term option
- | GRef_ of B.entry
+ | GRef_ of B.entity
| Bind_ of int * B.id * B.term * B.term
type ho_whd_result =
| B.Sort h -> f m (Sort_ h)
| B.GRef uri ->
let f entry = f m (GRef_ entry) in
- E.get_entry f uri
+ E.get_entity f uri
| B.LRef i ->
let f = function
| B.Void -> f m (LRef_ (i, None))
| Bind_ (_, _, w, _) ->
let f w = f (Abst w) in unwind_to_term f m w
| LRef_ (_, Some w) -> ho_whd f c m w
- | GRef_ (_, _, B.Abst w) -> ho_whd f c m w
- | GRef_ (_, _, B.Abbr v) -> ho_whd f c m v
+ | GRef_ (_, _, Y.Abst w) -> ho_whd f c m w
+ | GRef_ (_, _, Y.Abbr v) -> ho_whd f c m v
| LRef_ (_, None) -> assert false
- | GRef_ (_, _, B.Void) -> assert false
in
whd aux c m x
if h1 = h2 then f a else f false
| LRef_ (i1, _), LRef_ (i2, _) ->
if i1 = i2 then are_convertible_stacks f ~si a c m1 m2 else f false
- | GRef_ (a1, _, B.Abst _), GRef_ (a2, _, B.Abst _) ->
+ | GRef_ ((Y.Apix a1 :: _), _, Y.Abst _),
+ GRef_ ((Y.Apix a2 :: _), _, Y.Abst _) ->
if a1 = a2 then are_convertible_stacks f ~si a c m1 m2 else f false
- | GRef_ (a1, _, B.Abbr v1), GRef_ (a2, _, B.Abbr v2) ->
+ | GRef_ ((Y.Apix a1 :: _), _, Y.Abbr v1),
+ GRef_ ((Y.Apix a2 :: _), _, Y.Abbr v2) ->
if a1 = a2 then
let f a =
if a then f a else are_convertible f ~si true c m1 v1 m2 v2
else
if a1 < a2 then whd (aux m1 r1) c m2 v2 else
whd (aux_rev m2 r2) c m1 v1
- | _, GRef_ (_, _, B.Abbr v2) ->
+ | _, GRef_ (_, _, Y.Abbr v2) ->
whd (aux m1 r1) c m2 v2
- | GRef_ (_, _, B.Abbr v1), _ ->
+ | GRef_ (_, _, Y.Abbr v1), _ ->
whd (aux_rev m2 r2) c m1 v1
| Bind_ (l1, id1, w1, t1), Bind_ (l2, id2, w2, t2) ->
let l = B.new_location () in
module C = Cps
module S = Share
module L = Log
+module Y = Entity
module H = Hierarchy
module B = Bag
module O = BagOutput
B.get f c i
| B.GRef uri ->
let f = function
- | _, _, B.Abst w -> f x w
- | _, _, B.Abbr (B.Cast (w, v)) -> f x w
- | _, _, B.Abbr _ -> assert false
- | _, _, B.Void ->
- error1 "reference to excluded entry" c x
+ | _, _, Y.Abst w -> f x w
+ | _, _, Y.Abbr (B.Cast (w, v)) -> f x w
+ | _, _, Y.Abbr _ -> assert false
in
- E.get_entry f uri
+ E.get_entity f uri
| B.Bind (l, id, B.Abbr v, t) ->
let f xv xt tt =
f (S.sh2 v xv t xt x (B.bind_abbr l id)) (B.bind_abbr l id xv tt)
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
+module U = NUri
module L = Log
+module Y = Entity
module B = Bag
module E = BagEnvironment
module T = BagType
(* to share *)
let type_check f ?(si=false) g = function
- | None -> f None None
- | Some (a, uri, B.Abst t) ->
- let f tt entry = f (Some tt) (Some entry) in
- let f xt tt = E.set_entry (f tt) (a, uri, B.Abst xt) in
- L.loc := a; T.type_of f ~si g B.empty_lenv t
- | Some (a, uri, B.Abbr t) ->
- let f tt entry = f (Some tt) (Some entry) in
- let f xt tt = E.set_entry (f tt) (a, uri, B.Abbr xt) in
- L.loc := a; T.type_of f ~si g B.empty_lenv t
- | Some (a, uri, B.Void) ->
- let f entry = f None (Some entry) in
- L.loc := a; E.set_entry f (a, uri, B.Void)
+ | a, uri, Y.Abst t ->
+ let f xt tt = E.set_entity (f tt) (a, uri, Y.Abst xt) in
+ L.loc := U.string_of_uri uri; T.type_of f ~si g B.empty_lenv t
+ | a, uri, Y.Abbr t ->
+ let f xt tt = E.set_entity (f tt) (a, uri, Y.Abbr xt) in
+ L.loc := U.string_of_uri uri; T.type_of f ~si g B.empty_lenv t
V_______________________________________________________________ *)
val type_check:
- (Bag.term option -> Bag.entity -> 'a) -> ?si:bool ->
+ (Bag.term -> Bag.entity -> 'a) -> ?si:bool ->
Hierarchy.graph -> Bag.entity -> 'a
type uri = Entity.uri
type id = Entity.id
-
-type attr = Name of bool * id (* real?, name *)
- | Apix of int (* additional position index *)
-
-type attrs = attr list
+type attrs = Entity.attrs
type bind = Void of attrs (* attrs *)
| Abst of attrs * term (* attrs, type *)
| Appl of attrs * term * term (* attrs, argument, function *)
| Bind of bind * term (* binder, scope *)
-type entry = bind Entity.entry (* age, uri, binder *)
-
-type entity = bind Entity.entity
+type entity = term Entity.entity (* attrs, uri, binder *)
type lenv = Null
(* Cons: tail, relative local environment, binder *)
| Cons (tl, _, b) ->
let f x = fold_left f map x tl in
map f x b
-
-let rec name err f = function
- | [] -> err ()
- | Name (r, n) :: _ -> f n r
- | _ :: tl -> name err f tl
-
-let rec apix err f = function
- | [] -> err ()
- | Apix i :: _ -> f i
- | _ :: tl -> apix err f tl
module U = NUri
module H = U.UriHash
+module Y = Entity
module B = Brg
let hsize = 7000
let env = H.create hsize
-let age = ref 1
(* Internal functions *******************************************************)
+let get_age =
+ let age = ref 0 in
+ fun () -> incr age; !age
+
(* Interface functions ******************************************************)
-let set_entry f entry =
- let _, uri, b = entry in
- let entry = !age, uri, b in
- incr age; H.add env uri entry; f entry
+let set_entity f (a, uri, b) =
+ let age = get_age () in
+ let entity = (Y.Apix age :: a), uri, b in
+ H.add env uri entity; f entity
-let get_entry err f uri =
+let get_entity err f uri =
try f (H.find env uri) with Not_found -> err ()
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-val set_entry: (Brg.entry -> 'a) -> Brg.entry -> 'a
+val set_entity: (Brg.entity -> 'a) -> Brg.entity -> 'a
-val get_entry: (unit -> 'a) -> (Brg.entry -> 'a) -> Brg.uri -> 'a
+val get_entity: (unit -> 'a) -> (Brg.entity -> 'a) -> Brg.uri -> 'a
module C = Cps
module U = NUri
module L = Log
+module Y = Entity
+module X = Library
module H = Hierarchy
module O = Output
module B = Brg
let f c = B.push (f c) e b in
count_term_binder f c e b
-let count_entry f c = function
- | (_, u, B.Abst (_, w)) ->
+let count_entity f c = function
+ | _, u, Y.Abst w ->
let c = {c with
eabsts = succ c.eabsts; nodes = succ c.nodes; uris = u :: c.uris
} in
count_term f c B.empty_lenv w
- | (_, _, B.Abbr (_, v)) ->
+ | _, _, Y.Abbr v ->
let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in
count_term f c B.empty_lenv v
- | (_, u, B.Void _) ->
- let c = {c with
- evoids = succ c.evoids; nodes = succ c.nodes; uris = u :: c.uris
- } in
- f c
-
-let count_entity f c = function
- | Some entry -> count_entry f c entry
- | None -> f c
let print_counters f c =
let terms =
let f n1 r1 =
if n1 = n && r1 = r then f false else does_not_occur f n r c
in
- attrs_of_binder (B.name C.err f) b
+ attrs_of_binder (Y.name C.err f) b
let rename f c a =
let rec aux f c n r =
does_not_occur f n r c
in
let f n0 r0 =
- let f n r = if n = n0 && r = r0 then f a else f (B.Name (r, n) :: a) in
+ let f n r = if n = n0 && r = r0 then f a else f (Y.Name (n, r) :: a) in
aux f c n0 r0
in
- B.name C.err f a
+ Y.name C.err f a
let rename_bind f c = function
| B.Abst (a, w) -> let f a = f (B.abst a w) in rename f c a
(* lenv/term pretty printing ************************************************)
-let id frm a =
+let name frm a =
let f n = function
| true -> F.fprintf frm "%s" n
| false -> F.fprintf frm "^%s" n
in
- B.name C.err f a
+ Y.name C.err f a
let rec pp_term c frm = function
| B.Sort (_, h) ->
let f _ = function
| B.Abst (a, _)
| B.Abbr (a, _)
- | B.Void a -> F.fprintf frm "@[%a@]" id a
+ | B.Void a -> F.fprintf frm "@[%a@]" name a
in
if !O.indexes then err () else B.get err f c i
| B.GRef (_, s) ->
F.fprintf frm "@[(%a).%a@]" (pp_term c) v (pp_term c) t
| B.Bind (B.Abst (a, w), t) ->
let f a cc =
- F.fprintf frm "@[[%a:%a].%a@]" id a (pp_term c) w (pp_term cc) t
+ F.fprintf frm "@[[%a:%a].%a@]" name a (pp_term c) w (pp_term cc) t
in
let f a = B.push (f a) c (B.abst a w) in
rename f c a
| B.Bind (B.Abbr (a, v), t) ->
let f a cc =
- F.fprintf frm "@[[%a=%a].%a@]" id a (pp_term c) v (pp_term cc) t
+ F.fprintf frm "@[[%a=%a].%a@]" name a (pp_term c) v (pp_term cc) t
in
let f a = B.push (f a) c (B.abbr a v) in
rename f c a
| B.Bind (B.Void a, t) ->
- let f a cc = F.fprintf frm "@[[%a].%a@]" id a (pp_term cc) t in
+ let f a cc = F.fprintf frm "@[[%a].%a@]" name a (pp_term cc) t in
let f a = B.push (f a) c (B.Void a) in
rename f c a
let pp_lenv frm c =
let pp_entry f c = function
| B.Abst (a, w) ->
- let f a = F.fprintf frm "@,@[%a : %a@]" id a (pp_term c) w; f () in
+ let f a = F.fprintf frm "@,@[%a : %a@]" name a (pp_term c) w; f () in
rename f c a
| B.Abbr (a, v) ->
- let f a = F.fprintf frm "@,@[%a = %a@]" id a (pp_term c) v; f () in
+ let f a = F.fprintf frm "@,@[%a = %a@]" name a (pp_term c) v; f () in
rename f c a
| B.Void a ->
- let f a = F.fprintf frm "@,%a" id a; f () in
+ let f a = F.fprintf frm "@,%a" name a; f () in
rename f c a
in
B.rev_iter C.start pp_entry c
(* term xml printing ********************************************************)
-let id frm a =
- let f s = function
- | true -> F.fprintf frm " name=%S" s
- | false -> F.fprintf frm " name=%S" ("^" ^ s)
- in
- B.name C.start f a
-
let rec exp_term c frm = function
| B.Sort (a, l) ->
let a =
let err _ = a in
- let f s = B.Name (true, s) :: a in
+ let f s = Y.Name (s, true) :: a in
H.get_sort err f l
in
- F.fprintf frm "<Sort position=%S%a/>" (string_of_int l) id a
+ F.fprintf frm "<Sort position=%S%a/>" (string_of_int l) X.old_name a
| B.LRef (a, i) ->
let a =
let err _ = a in
- let f n r = B.Name (r, n) :: a in
- let f _ b = attrs_of_binder (B.name err f) b in
+ let f n r = Y.Name (n, r) :: a in
+ let f _ b = attrs_of_binder (Y.name err f) b in
B.get err f c i
in
- F.fprintf frm "<LRef position=%S%a/>" (string_of_int i) id a
+ F.fprintf frm "<LRef position=%S%a/>" (string_of_int i) X.old_name a
| B.GRef (a, u) ->
- let a = B.Name (true, U.name_of_uri u) :: a in
- F.fprintf frm "<GRef uri=%S%a/>" (U.string_of_uri u) id a
+ let a = Y.Name (U.name_of_uri u, true) :: a in
+ F.fprintf frm "<GRef uri=%S%a/>" (U.string_of_uri u) X.old_name a
| B.Cast (a, w, t) ->
- F.fprintf frm "<Cast%a>%a</Cast>@,%a" id a (exp_boxed c) w (exp_term c) t
+ F.fprintf frm "<Cast%a>%a</Cast>@,%a" X.old_name a (exp_boxed c) w (exp_term c) t
| B.Appl (a, v, t) ->
- F.fprintf frm "<Appl%a>%a</Appl>@,%a" id a (exp_boxed c) v (exp_term c) t
+ F.fprintf frm "<Appl%a>%a</Appl>@,%a" X.old_name a (exp_boxed c) v (exp_term c) t
| B.Bind (b, t) ->
let f b cc = F.fprintf frm "%a@,%a" (exp_bind c) b (exp_term cc) t in
let f b = B.push (f b) c b in
and exp_bind c frm = function
| B.Abst (a, w) ->
- F.fprintf frm "<Abst%a>%a</Abst>" id a (exp_boxed c) w
+ F.fprintf frm "<Abst%a>%a</Abst>" X.old_name a (exp_boxed c) w
| B.Abbr (a, v) ->
- F.fprintf frm "<Abbr%a/>%a</Abbr>" id a (exp_boxed c) v
+ F.fprintf frm "<Abbr%a/>%a</Abbr>" X.old_name a (exp_boxed c) v
| B.Void a ->
- F.fprintf frm "<Void%a/>" id a
-
-let exp_entry c frm = function
- | _, u, B.Abst (a, w) ->
- let str = U.string_of_uri u in
- let a = B.Name (true, U.name_of_uri u) :: a in
- F.fprintf frm "<ABST uri=%S%a>%a</ABST>" str id a (exp_boxed c) w
- | _, u, B.Abbr (a, v) ->
- let str = U.string_of_uri u in
- let a = B.Name (true, U.name_of_uri u) :: a in
- F.fprintf frm "<ABBR uri=%S%a>%a</ABBR>" str id a (exp_boxed c) v
- | _, u, B.Void a ->
- let str = U.string_of_uri u in
- let a = B.Name (true, U.name_of_uri u) :: a in
- F.fprintf frm "<VOID uri=%S%a/>" str id a
+ F.fprintf frm "<Void%a/>" X.old_name a
-let export_entry frm entry =
- F.fprintf frm "@,@[<v3> %a@]@," (exp_entry B.empty_lenv) entry
+let export_term frm t =
+ F.fprintf frm "%a" (exp_boxed B.empty_lenv) t
val specs: (Brg.lenv, Brg.term) Log.specs
-val export_entry: Format.formatter -> Brg.bind Entity.entry -> unit
+val export_term: Format.formatter -> Brg.term -> unit
module C = Cps
module S = Share
module L = Log
+module Y = Entity
module P = Output
module B = Brg
module O = BrgOutput
| B.Sort _ -> f m None x
| B.GRef (_, uri) ->
let f = function
- | _, _, B.Abbr (_, v) when delta ->
+ | _, _, Y.Abbr v when delta ->
P.add ~gdelta:1 (); step f ~delta ~rt m v
- | _, _, B.Abst (_, w) when rt ->
+ | _, _, Y.Abst w when rt ->
P.add ~grt:1 (); step f ~delta ~rt m w
- | _, _, B.Void _ ->
- assert false
- | e, _, b ->
- f m (Some (e, b)) x
+ | a, _, Y.Abbr v ->
+ let f e = f m (Some (e, B.Abbr (a, v))) x in
+ Y.apix C.err f a
+ | a, _, Y.Abst w ->
+ let f e = f m (Some (e, B.Abst (a, w))) x in
+ Y.apix C.err f a
in
- E.get_entry C.err f uri
+ E.get_entity C.err f uri
| B.LRef (_, i) ->
let f c = function
| B.Abbr (_, v) ->
assert false
| B.Abst (a, _) as b ->
let f e = f {m with c = c} (Some (e, b)) x in
- B.apix C.err f a
+ Y.apix C.err f a
in
get C.err f m i
| B.Cast (_, _, t) ->
let push f m b =
assert (m.s = []);
let b, i = match b with
- | B.Abst (a, w) -> B.abst (B.Apix m.i :: a) w, succ m.i
+ | B.Abst (a, w) -> B.abst (Y.Apix m.i :: a) w, succ m.i
| b -> b, m.i
in
let f c = f {m with c = c; i = i} in
module A = Share
module L = Log
module H = Hierarchy
+module Y = Entity
module B = Brg
module O = BrgOutput
module E = BrgEnvironment
R.get err f m i
| B.GRef (_, uri) ->
let f = function
- | _, _, B.Abst (_, w) -> f x w
- | _, _, B.Abbr (_, B.Cast (_, w, _)) -> f x w
- | _, _, B.Abbr _ -> assert false
- | _, _, B.Void _ ->
- error1 err "reference to excluded entry" m x
+ | _, _, Y.Abst w -> f x w
+ | _, _, Y.Abbr (B.Cast (_, w, _)) -> f x w
+ | _, _, Y.Abbr _ -> assert false
in
let err _ = error1 err "reference to unknown entry" m x in
- E.get_entry err f uri
+ E.get_entity err f uri
| B.Bind (B.Abbr (a, v), t) ->
let f xv xt tt =
f (A.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt)
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
+module U = NUri
module L = Log
+module Y = Entity
module B = Brg
module E = BrgEnvironment
module R = BrgReduction
(* to share *)
let type_check err f ?(si=false) g = function
- | None -> f None None
- | Some (e, uri, B.Abst (a, t)) ->
- let f tt entry = f (Some tt) (Some entry) in
- let f xt tt = E.set_entry (f tt) (e, uri, B.abst a xt) in
- L.loc := e; T.type_of err f ~si g R.empty_kam t
- | Some (e, uri, B.Abbr (a, t)) ->
- let f tt entry = f (Some tt) (Some entry) in
- let f xt tt = E.set_entry (f tt) (e, uri, B.abbr a xt) in
- L.loc := e; T.type_of err f ~si g R.empty_kam t
- | Some (e, uri, (B.Void _ as b)) ->
- let f entry = f None (Some entry) in
- L.loc := e; E.set_entry f (e, uri, b)
+ | a, uri, Y.Abst t ->
+ let f xt tt = E.set_entity (f tt) (a, uri, Y.Abst xt) in
+ L.loc := U.string_of_uri uri; T.type_of err f ~si g R.empty_kam t
+ | a, uri, Y.Abbr t ->
+ let f xt tt = E.set_entity (f tt) (a, uri, Y.Abbr xt) in
+ L.loc := U.string_of_uri uri; T.type_of err f ~si g R.empty_kam t
V_______________________________________________________________ *)
val type_check:
- (BrgType.message -> 'a) -> (Brg.term option -> Brg.entity -> 'a) ->
+ (BrgType.message -> 'a) -> (Brg.term -> Brg.entity -> 'a) ->
?si:bool -> Hierarchy.graph -> Brg.entity -> 'a
type uri = NUri.uri
type id = Aut.id
-type 'bind entry = int * uri * 'bind (* age, uri, binder *)
+type attr = Name of id * bool (* name, real? *)
+ | Apix of int (* additional position index *)
+ | Mark of int (* node marker *)
+ | Priv (* private global definition *)
-type 'bind entity = 'bind entry option
+type attrs = attr list (* attributes *)
+
+type 'term bind = Abst of 'term (* declaration: domain *)
+ | Abbr of 'term (* definition: body *)
+
+type 'term entity = attrs * uri * 'term bind (* attrs, name, binder *)
type 'a uri_generator = (string -> 'a) -> string -> 'a
+
+(* helpers ******************************************************************)
+
+let rec name err f = function
+ | Name (n, r) :: _ -> f n r
+ | _ :: tl -> name err f tl
+ | [] -> err ()
+
+let rec apix err f = function
+ | Apix i :: _ -> f i
+ | _ :: tl -> apix err f tl
+ | [] -> err ()
+
+let rec mark err f = function
+ | Mark i :: _ -> f i
+ | _ :: tl -> mark err f tl
+ | [] -> err ()
+
+let rec priv err f = function
+ | Priv :: _ -> f ()
+ | _ :: tl -> priv err f tl
+ | [] -> err ()
+
+let resolve err f name a =
+ let rec aux i = function
+ | Name (n, true) :: _ when n = name -> f i
+ | _ :: tl -> aux (succ i) tl
+ | [] -> err i
+ in
+ aux 0 a
+
+let xlate f xlate_term = function
+ | a, uri, Abst t ->
+ let f t = f (a, uri, Abst t) in xlate_term f t
+ | a, uri, Abbr t ->
+ let f t = f (a, uri, Abbr t) in xlate_term f t
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module F = Filename
+module F = Format
+module N = Filename
module U = NUri
+module C = Cps
module H = Hierarchy
-
-type 'a out = (unit -> 'a) -> string -> 'a
+module Y = Entity
(* internal functions *******************************************************)
let obj_ext = ".xml"
+let root = "ENTITY"
+
let system = "http://helm.cs.unibo.it/lambda-delta/" ^ base ^ "/ld.dtd"
let path_of_uri uri =
- F.concat base (Str.string_after (U.string_of_uri uri) 3)
+ N.concat base (Str.string_after (U.string_of_uri uri) 3)
let pp_head frm =
- Format.fprintf frm "<?xml version=%S encoding=%S?>@,@," "1.0" "UTF-8"
+ F.fprintf frm "<?xml version=%S encoding=%S?>@,@," "1.0" "UTF-8"
let pp_doctype frm =
- Format.fprintf frm "<!DOCTYPE ENTRY SYSTEM %S>@,@," system
+ F.fprintf frm "<!DOCTYPE ENTITY SYSTEM %S>@,@," system
-let open_entry si g frm =
+let open_entity si g frm =
let opts = if si then "si" else "" in
let f shp =
- Format.fprintf frm "<ENTRY hierarchy=%S options=%S>" shp opts
+ F.fprintf frm "<ENTITY hierarchy=%S options=%S>" shp opts
in
H.string_of_graph f g
-let close_entry frm =
- Format.fprintf frm "</ENTRY>"
+let close_entity frm =
+ F.fprintf frm "</ENTITY>"
+
+let name frm a =
+ let f s = function
+ | true -> F.fprintf frm " name=%S" s
+ | false -> F.fprintf frm " name=%S" ("^" ^ s)
+ in
+ Y.name C.start f a
+
+let pp_entity pp_term frm = function
+ | a, u, Y.Abst w ->
+ let str = U.string_of_uri u in
+ let a = Y.Name (U.name_of_uri u, true) :: a in
+ F.fprintf frm "<ABST uri=%S%a>%a</ABST>" str name a pp_term w
+ | a, u, Y.Abbr v ->
+ let str = U.string_of_uri u in
+ let a = Y.Name (U.name_of_uri u, true) :: a in
+ F.fprintf frm "<ABBR uri=%S%a>%a</ABBR>" str name a pp_term v
+
+let pp_boxed pp_term frm entity =
+ F.fprintf frm "@,@[<v3> %a@]@," (pp_entity pp_term) entity
(* interface functions ******************************************************)
-let old_export_entity export_entry si g = function
- | Some entry ->
- let _, uri, bind = entry in
- let path = path_of_uri uri in
- let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in
- let och = open_out (path ^ obj_ext) in
- let frm = Format.formatter_of_out_channel och in
- Format.pp_set_margin frm max_int;
- Format.fprintf frm "@[<v>%t%t%t%a%t@]@."
- pp_head pp_doctype (open_entry si g) export_entry entry close_entry;
- close_out och
- | None -> ()
+let old_export_entity pp_term si g entity =
+ let _, uri, _ = entity in
+ let path = path_of_uri uri in
+ let _ = Sys.command (Printf.sprintf "mkdir -p %s" (N.dirname path)) in
+ let och = open_out (path ^ obj_ext) in
+ let frm = F.formatter_of_out_channel och in
+ F.pp_set_margin frm max_int;
+ F.fprintf frm "@[<v>%t%t%t%a%t@]@."
+ pp_head pp_doctype
+ (open_entity si g) (pp_boxed pp_term) entity close_entity;
+ close_out och
+
+let old_name = name
(****************************************************************************)
-(*
-let export_entity export_entry si g = function
- | Some entry ->
- let _, uri, bind = entry in
- let path = path_of_uri root uri in
- let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in
- let och = open_out (path ^ obj_ext) in
- let out f s = output_string och s; f () in
- let f () = close_out och in
-
- Format.fprintf frm "@[<v>%t%t%t%a%t@]@."
- pp_head pp_doctype (open_entry si g) export_entry entry close_entry;
- close_out och
- | None -> ()
-*)
+
+type och = string -> unit
+
+type attr = string * string
+
+type 'a pp = (och -> int -> 'a) -> och -> int -> 'a
+
+let attribute out (name, contents) =
+ if contents <> "" then begin
+ out " "; out name; out "=\""; out contents; out "\""
+ end
+
+let xml out version encoding =
+ out "<?xml";
+ attribute out ("version", version);
+ attribute out ("encoding", encoding);
+ out "?>\n\n"
+
+let doctype out root system =
+ out "<!DOCTYPE "; out root; out " SYSTEM \""; out system; out "\">\n\n"
+
+let tag tag attrs ?contents f out indent =
+ let spc = String.make indent ' ' in
+ out spc; out "<"; out "tag"; List.iter (attribute out) attrs;
+ match contents with
+ | None -> out "/>\n"; f out indent
+ | Some cont ->
+ let f _ _ = out spc; out "</"; out tag; out ">\n"; f out indent in
+ cont f out (indent + 3)
+
+let sort = "Sort"
+
+let lref = "LRef"
+
+let gref = "GRef"
+
+let cast = "Cast"
+
+let appl = "Appl"
+
+let proj = "Proj"
+
+let abst = "Abst"
+
+let abbr = "Abbr"
+
+let void = "Void"
+
+let position i =
+ "position", string_of_int i
+
+let offset j =
+ let contents = if j > 0 then string_of_int j else "" in
+ "offset", contents
+
+let uri u =
+ "uri", U.string_of_uri u
+
+let arity n =
+ let contents = if n > 1 then string_of_int n else "" in
+ "arity", contents
+
+let name a =
+ let err () = "name", "" in
+ let f s = function
+ | true -> "name", s
+ | false -> "name", ("^" ^ s)
+ in
+ Y.name err f a
+
+let mark a =
+ let err () = "mark", "" in
+ let f i = "mark", string_of_int i in
+ Y.mark err f a
+
+let export_entity f pp_term si g (a, uri, b) =
+ let path = path_of_uri uri in
+ let _ = Sys.command (Printf.sprintf "mkdir -p %s" (N.dirname path)) in
+ let och = open_out (path ^ obj_ext) in
+ let out = output_string och in
+ let f _ _ = close_out och; f () in
+ xml out "1.0" "UTF-8"; doctype out root system;
+ let str = U.string_of_uri uri in
+ let a = Y.Name (U.name_of_uri uri, true) :: a in
+ let attrs = ["uri", str; name a] in
+ let contents = match b with
+ | Y.Abst w -> tag "ABST" attrs ~contents:(pp_term w)
+ | Y.Abbr v -> tag "ABBR" attrs ~contents:(pp_term v)
+ in
+ let opts = if si then "si" else "" in
+ let shp = H.string_of_graph C.start g in
+ let attrs = ["hierarchy", shp; "options", opts] in
+ tag root attrs ~contents f out 0;
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-type 'a out = (unit -> 'a) -> string -> 'a
-(*
+type och = string -> unit
+
+type attr = string * string
+
+type 'a pp = (och -> int -> 'a) -> och -> int -> 'a
+
val export_entity:
- ('a och -> string -> 'bind Entity.entry -> 'a) ->
- string -> bool -> Hierarchy.graph -> 'bind Entity.entity -> 'a
-*)
+ (unit ->'a) -> ('term -> 'a pp) ->
+ bool -> Hierarchy.graph -> 'term Entity.entity -> 'a
+
+val tag: string -> attr list -> ?contents:'a pp -> 'a pp
+
+val sort: string
+
+val lref: string
+
+val gref: string
+
+val cast: string
+
+val appl: string
+
+val proj: string
+
+val abst: string
+
+val abbr: string
+
+val void: string
+
+val position: int -> attr
+
+val offset: int -> attr
+
+val uri: Entity.uri -> attr
+
+val arity: int -> attr
+
+val name: Entity.attrs -> attr
+
+val mark: Entity.attrs -> attr
+
val old_export_entity:
- (Format.formatter -> 'bind Entity.entry -> unit) ->
- bool -> Hierarchy.graph -> 'bind Entity.entity -> unit
+ (Format.formatter -> 'term -> unit) ->
+ bool -> Hierarchy.graph -> 'term Entity.entity -> unit
+
+val old_name: Format.formatter -> Entity.attrs -> unit
-drg drgAut
+drg drgOutput drgAut
type uri = Entity.uri
type id = Entity.id
+type attrs = Entity.attrs
-type attr = Name of id * bool (* name, real? *)
- | Priv (* private global definition *)
-
-type attrs = attr list (* attributes *)
-
-type bind = Abst of attrs * term (* attrs, domain *)
- | Abbr of attrs * term (* attrs, body *)
- | Void of attrs (* attrs *)
+type bind = Abst of term list (* domains *)
+ | Abbr of term list (* bodies *)
+ | Void of int (* number of exclusions *)
and term = Sort of attrs * int (* attrs, hierarchy index *)
- | LRef of attrs * int (* attrs, position index *)
+ | LRef of attrs * int * int (* attrs, position indexes *)
| GRef of attrs * uri (* attrs, reference *)
| Cast of attrs * term * term (* attrs, domain, element *)
| Appl of attrs * term list * term (* attrs, arguments, function *)
- | Bind of lenv * term (* closure, scope *)
-
-and lenv = bind list (* local environment *)
+ | Proj of attrs * lenv * term (* attrs, closure, member *)
+ | Bind of attrs * bind * term (* attrs, binder, scope *)
-type entry = bind Entity.entry (* age, uri, binder *)
+and lenv = Null
+ | Cons of lenv * attrs * bind (* closure, attrs, binder *)
-type entity = bind Entity.entity
+type entity = term Entity.entity
(* helpers ******************************************************************)
let str = String.concat "/" ["ld:"; "drg"; root; s ^ ".ld"] in
f str
-let rec name_of err f = function
- | Name (n, r) :: _ -> f n r
- | _ :: tl -> name_of err f tl
- | [] -> err ()
+let empty_lenv = Null
-let name_of_binder err f = function
- | Abst (a, _) -> name_of err f a
- | Abbr (a, _) -> name_of err f a
- | Void a -> name_of err f a
+let push f lenv a b = f (Cons (lenv, a, b))
let resolve_lref err f id lenv =
- let rec aux f i = function
- | [] -> err ()
- | b :: tl ->
- let err () = aux f (succ i) tl in
- let f name _ = if name = id then f i else err () in
- name_of_binder err f b
+ let rec aux f i k = function
+ | Null -> err ()
+ | Cons (tl, a, _) ->
+ let err kk = aux f (succ i) (k + kk) tl in
+ let f j = f i j k in
+ Entity.resolve err f id a
in
- aux f 0 lenv
+ aux f 0 0 lenv
module U = NUri
module H = U.UriHash
module C = Cps
-module E = Entity
+module Y = Entity
module A = Aut
module D = Drg
(* qualified identifier: uri, name, qualifiers *)
type qid = D.uri * D.id * D.id list
-type environment = D.lenv H.t
+type context = Y.attrs * D.term list
+
+type environment = context H.t
type context_node = qid option (* context node: None = root *)
-type 'b status = {
+type 'a status = {
henv: environment; (* optimized global environment *)
path: D.id list; (* current section path *)
hcnt: environment; (* optimized context *)
node: context_node; (* current context node *)
nodes: context_node list; (* context node list *)
line: int; (* line number *)
- mk_uri:'b E.uri_generator (* uri generator *)
+ mk_uri:'a Y.uri_generator (* uri generator *)
}
type resolver = Local of int
- | Global of D.lenv
+ | Global of context
-let hsize = 7000 (* hash tables initial size *)
+let henv_size, hcnt_size = 7000, 4300 (* hash tables initial sizes *)
(* Internal functions *******************************************************)
-let initial_status size mk_uri = {
+let initial_status mk_uri = {
path = []; node = None; nodes = []; line = 1; mk_uri = mk_uri;
- henv = H.create size; hcnt = H.create size
+ henv = H.create henv_size; hcnt = H.create hcnt_size
}
-let mk_lref f i = f (D.LRef ([], i))
+let empty_cnt = [], []
+
+let add_abst (a, ws) id w =
+ Y.Name (id, true) :: a, w :: ws
+
+let lenv_of_cnt (a, ws) =
+ D.push C.start D.empty_lenv a (D.Abst ws)
-let mk_abst id w = D.Abst ([D.Name (id, true)], w)
+let mk_lref f i j k = f (D.LRef ([Y.Apix k], i, j))
let id_of_name (id, _, _) = id
resolve_gref err f st qid
let get_cnt err f st = function
- | None -> f []
+ | None -> f empty_cnt
| Some qid as node ->
try let cnt = H.find st.hcnt (uri_of_qid qid) in f cnt
with Not_found -> err node
xlate_term f st lenv v
| A.Abst (name, w, t) ->
let f ww =
- let b = mk_abst name ww in
- let f tt = f (D.Bind ([b], tt)) in
- xlate_term f st (b :: lenv) t
+ let a, b = [Y.Name (name, true)], (D.Abst [ww]) in
+ let f tt = f (D.Bind (a, b, tt)) in
+ let f lenv = xlate_term f st lenv t in
+ D.push f lenv a b
in
xlate_term f st lenv w
| A.GRef (name, args) ->
- let g qid cnt =
+ let g qid (a, _) =
let map1 f = xlate_term f st lenv in
- let map2 f b =
- let f id _ = D.resolve_lref Cps.err (mk_lref f) id lenv in
- D.name_of_binder C.err f b
+ let map2 f = function
+ | Y.Name (id, _) -> D.resolve_lref Cps.err (mk_lref f) id lenv
+ | _ -> assert false
in
let f tail =
let f args = f (D.Appl ([], args, D.GRef ([], uri_of_qid qid))) in
- let f cnt = C.list_rev_map_append f map2 cnt ~tail in
- C.list_sub_strict f cnt args
+ let f a = C.list_rev_map_append f map2 a ~tail in
+ C.list_sub_strict f a args
in
C.list_map f map1 args
in
let err () = complete_qid g st name in
D.resolve_lref err (mk_lref f) (id_of_name name) lenv
-let xlate_entity f st = function
+let xlate_entity err f st = function
| A.Section (Some (_, name)) ->
- f {st with path = name :: st.path; nodes = st.node :: st.nodes} None
+ err {st with path = name :: st.path; nodes = st.node :: st.nodes}
| A.Section None ->
begin match st.path, st.nodes with
| _ :: ptl, nhd :: ntl ->
- f {st with path = ptl; node = nhd; nodes = ntl} None
+ err {st with path = ptl; node = nhd; nodes = ntl}
| _ -> assert false
end
| A.Context None ->
- f {st with node = None} None
+ err {st with node = None}
| A.Context (Some name) ->
- let f name = f {st with node = Some name} None in
+ let f name = err {st with node = Some name} in
complete_qid f st name
| A.Block (name, w) ->
let f qid =
let f cnt =
+ let lenv = lenv_of_cnt cnt in
let f ww =
- H.add st.hcnt (uri_of_qid qid) (mk_abst name ww :: cnt);
- f {st with node = Some qid} None
+ H.add st.hcnt (uri_of_qid qid) (add_abst cnt name ww);
+ err {st with node = Some qid}
in
- xlate_term f st cnt w
+ xlate_term f st lenv w
in
get_cnt_relaxed f st
in
complete_qid f st (name, true, [])
| A.Decl (name, w) ->
- let f cnt =
- let f qid =
+ let f cnt =
+ let a, ws = cnt in
+ let lenv = lenv_of_cnt cnt in
+ let f qid =
let f ww =
- let b = D.Abst ([], D.Bind (cnt, ww)) in
- let entry = st.line, uri_of_qid qid, b in
- H.add st.henv (uri_of_qid qid) cnt;
- f {st with line = succ st.line} (Some entry)
+ H.add st.henv (uri_of_qid qid) cnt;
+ let b = Y.Abst (D.Bind (a, D.Abst ws, ww)) in
+ let entity = [Y.Mark st.line], uri_of_qid qid, b in
+ f {st with line = succ st.line} entity
in
- xlate_term f st cnt w
+ xlate_term f st lenv w
in
complete_qid f st (name, true, [])
in
get_cnt_relaxed f st
| A.Def (name, w, trans, v) ->
let f cnt =
+ let a, ws = cnt in
+ let lenv = lenv_of_cnt cnt in
let f qid =
let f ww vv =
- let a = if trans then [] else [D.Priv] in
- let b = D.Abbr (a, D.Bind (cnt, D.Cast ([], ww, vv))) in
- let entry = st.line, uri_of_qid qid, b in
H.add st.henv (uri_of_qid qid) cnt;
- f {st with line = succ st.line} (Some entry)
+ let b = Y.Abbr (D.Bind (a, D.Abst ws, D.Cast ([], ww, vv))) in
+ let a =
+ if trans then [Y.Mark st.line] else [Y.Mark st.line; Y.Priv]
+ in
+ let entity = a, uri_of_qid qid, b in
+ f {st with line = succ st.line} entity
in
- let f ww = xlate_term (f ww) st cnt v in
- xlate_term f st cnt w
+ let f ww = xlate_term (f ww) st lenv v in
+ xlate_term f st lenv w
in
complete_qid f st (name, true, [])
in
(* Interface functions ******************************************************)
let initial_status mk_uri =
- initial_status hsize mk_uri
+ initial_status mk_uri
let drg_of_aut = xlate_entity
val initial_status: 'a Entity.uri_generator -> 'a status
-val drg_of_aut: ('a status -> Drg.entity -> 'a) ->
+val drg_of_aut: ('a status -> 'a) -> ('a status -> Drg.entity -> 'a) ->
'a status -> Aut.entity -> 'a
--- /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 X = Library
+module D = Drg
+
+let rec list_iter map l f = match l with
+ | [] -> f
+ | hd :: tl -> map hd (list_iter map tl f)
+
+let rec lenv_iter map l f = match l with
+ | D.Null -> f
+ | D.Cons (lenv, a, b) -> lenv_iter map lenv (map a b f)
+
+let rec exp_term t f = match t with
+ | D.Sort (a, h) ->
+ let attrs = [X.position h; X.name a] in
+ X.tag X.sort attrs f
+ | D.LRef (a, i, j) ->
+ let attrs = [X.position i; X.offset j; X.name a] in
+ X.tag X.lref attrs f
+ | D.GRef (a, n) ->
+ let attrs = [X.uri n; X.name a] in
+ X.tag X.gref attrs f
+ | D.Cast (a, u, t) ->
+ let attrs = [] in
+ X.tag X.cast attrs (exp_term t f) ~contents:(exp_term u)
+ | D.Appl (a, vs, t) ->
+ let attrs = [X.arity (List.length vs)] in
+ X.tag X.appl attrs (exp_term t f) ~contents:(list_iter exp_term vs)
+ | D.Proj (a, lenv, t) ->
+ let attrs = [] in
+ X.tag X.proj attrs (exp_term t f) ~contents:(lenv_iter exp_lenv lenv)
+ | D.Bind (a, b, t) ->
+ exp_lenv a b (exp_term t f)
+
+and exp_lenv a b f = match b with
+ | D.Abst ws ->
+ let attrs = [X.name a; X.mark a; X.arity (List.length ws)] in
+ X.tag X.abst attrs f ~contents:(list_iter exp_term ws)
+ | D.Abbr vs ->
+ let attrs = [X.name a; X.mark a; X.arity (List.length vs)] in
+ X.tag X.abbr attrs f ~contents:(list_iter exp_term vs)
+ | D.Void n ->
+ let attrs = [X.name a; X.mark a; X.arity n] in
+ X.tag X.void attrs f
+
+let export_term = exp_term
--- /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_______________________________________________________________ *)
+
+val export_term: Drg.term -> 'a Library.pp
let level = ref 0
-let loc = ref 0
+let loc = ref "unknown location"
(* Internal functions *******************************************************)
| LEnv c -> F.fprintf frm "%a" st.pp_lenv c
| Warn s -> F.fprintf frm "@,%s" s
| String s -> F.fprintf frm "%s " s
- | Loc -> F.fprintf frm " (line %u)" !loc
+ | Loc -> F.fprintf frm " <%s>" !loc
in
let iter map frm l = List.iter (map frm) l in
if !level >= l then F.fprintf frm "%a" (iter pp_item) items
pp_lenv: Format.formatter -> 'a -> unit
}
-val loc: int ref
+val loc: string ref
val level: int ref
V_______________________________________________________________ *)
type uri = Entity.uri
-
type id = Entity.id
type term = Sort of bool (* sorts: true = TYPE, false = PROP *)
type pars = (id * term) list (* parameter declarations: name, type *)
-(* entry: line number, parameters, name, domain, (transparent?, body) *)
-type entry = int * pars * uri * term * (bool * term) option
+type entry = pars * term * term option (* parameters, domain, body *)
-type entity = entry option
+type entity = entry Entity.entity
module U = NUri
module H = U.UriHash
+module C = Cps
+module Y = Entity
module M = Meta
module A = Aut
(* qualified identifier: uri, name, qualifiers *)
-type qid = U.uri * M.id * M.id list
+type qid = M.uri * M.id * M.id list
type environment = M.pars H.t
type resolver = Local of int
| Global of M.pars
-let hsize = 7000 (* hash tables initial size *)
+let henv_size, hcnt_size = 7000, 4300 (* hash tables initial sizes *)
(* Internal functions *******************************************************)
-let initial_status size cover = {
+let initial_status cover = {
path = []; node = None; nodes = []; line = 1; cover = cover;
- henv = H.create size; hcnt = H.create size
+ henv = H.create henv_size; hcnt = H.create hcnt_size
}
let id_of_name (id, _, _) = id
let complete_qid f st (id, is_local, qs) =
let f qs = f (mk_qid st id qs) in
- let f path = Cps.list_rev_append f path ~tail:qs in
+ let f path = C.list_rev_append f path ~tail:qs in
let rec skip f = function
| phd :: ptl, qshd :: _ when phd = qshd -> f ptl
| _ :: ptl, _ :: _ -> skip f (ptl, qs)
let relax_qid f st (_, id, path) =
let f path = f (mk_qid st id path) in
let f = function
- | _ :: tl -> Cps.list_rev f tl
+ | _ :: tl -> C.list_rev f tl
| [] -> assert false
in
- Cps.list_rev f path
+ C.list_rev f path
let relax_opt_qid f st = function
| None -> f None
let map2 f (id, _) = resolve_lref_strict f st l lenv id in
let f tail =
let f args = f (M.GRef (l, uri_of_qid qid, args)) in
- let f defs = Cps.list_rev_map_append f map2 defs ~tail in
- Cps.list_sub_strict f defs args
+ let f defs = C.list_rev_map_append f map2 defs ~tail in
+ C.list_sub_strict f defs args
in
- Cps.list_map f map1 args
+ C.list_map f map1 args
in
let g qid = resolve_gref_relaxed g st qid in
let f = function
in
resolve_lref f st l lenv (id_of_name name)
-let xlate_entity f st = function
+let xlate_entity err f st = function
| A.Section (Some (_, name)) ->
- f {st with path = name :: st.path; nodes = st.node :: st.nodes} None
+ err {st with path = name :: st.path; nodes = st.node :: st.nodes}
| A.Section None ->
begin match st.path, st.nodes with
| _ :: ptl, nhd :: ntl ->
- f {st with path = ptl; node = nhd; nodes = ntl} None
+ err {st with path = ptl; node = nhd; nodes = ntl}
| _ -> assert false
end
| A.Context None ->
- f {st with node = None} None
+ err {st with node = None}
| A.Context (Some name) ->
- let f name = f {st with node = Some name} None in
+ let f name = err {st with node = Some name} in
complete_qid f st name
| A.Block (name, w) ->
let f qid =
let f pars =
let f ww =
H.add st.hcnt (uri_of_qid qid) ((name, ww) :: pars);
- f {st with node = Some qid} None
+ err {st with node = Some qid}
in
xlate_term f st pars w
in
let f pars =
let f qid =
let f ww =
- let entry = (st.line, pars, uri_of_qid qid, ww, None) in
H.add st.henv (uri_of_qid qid) pars;
- f {st with line = succ st.line} (Some entry)
+ let a = [Y.Mark st.line] in
+ let entry = pars, ww, None in
+ let entity = a, uri_of_qid qid, Y.Abst entry in
+ f {st with line = succ st.line} entity
in
xlate_term f st pars w
in
let f pars =
let f qid =
let f ww vv =
- let entry = (st.line, pars, uri_of_qid qid, ww, Some (trans, vv)) in
H.add st.henv (uri_of_qid qid) pars;
- f {st with line = succ st.line} (Some entry)
+ let a = Y.Mark st.line :: if trans then [] else [Y.Priv] in
+ let entry = pars, ww, Some vv in
+ let entity = a, uri_of_qid qid, Y.Abbr entry in
+ f {st with line = succ st.line} entity
in
let f ww = xlate_term (f ww) st pars v in
xlate_term f st pars w
(* Interface functions ******************************************************)
let initial_status ?(cover="") () =
- initial_status hsize cover
+ initial_status cover
let meta_of_aut = xlate_entity
val initial_status: ?cover:string -> unit -> status
-val meta_of_aut: (status -> Meta.entity -> 'a) -> status -> Aut.entity -> 'a
+val meta_of_aut:
+ (status -> 'a) -> (status -> Meta.entity -> 'a) ->
+ status -> Aut.entity -> 'a
let f t = C.list_fold_left f map t c in
xlate_term c f t
-let xlate_entry f = function
- | e, pars, uri, u, None ->
- let f u = f (e, uri, B.Abst u) in
+let xlate_entry f = function
+ | pars, u, None ->
let f c = unwind_to_xlate_term f c u in
xlate_pars f pars
- | e, pars, uri, u, Some (_, t) ->
- let f u t = f (e, uri, B.Abbr (B.Cast (u, t))) in
+ | pars, u, Some t ->
+ let f u t = f (B.Cast (u, t)) in
let f c u = unwind_to_xlate_term (f u) c t in
let f c = unwind_to_xlate_term (f c) c u in
xlate_pars f pars
-
-let xlate_entity f = function
- | None -> f None
- | Some e -> let f e = f (Some e) in xlate_entry f e
-
+
(* Interface functions ******************************************************)
-let bag_of_meta = xlate_entity
+let bag_of_meta = xlate_entry
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-val bag_of_meta: (Bag.entity -> 'a) -> Meta.entity -> 'a
+val bag_of_meta: (Bag.term -> 'a) -> Meta.entry -> 'a
V_______________________________________________________________ *)
module C = Cps
+module Y = Entity
module B = Brg
module M = Meta
xlate_term c f v
| M.Abst (id, w, t) ->
let f w =
- let a = [B.Name (true, id)] in
+ let a = [Y.Name (id, true)] in
let f t = f (B.Bind (B.abst a w, t)) in
let f c = xlate_term c f t in
B.push f c (B.abst a w)
let xlate_pars f pars =
let map f (id, w) c =
- let a = [B.Name (true, id)] in
+ let a = [Y.Name (id, true)] in
let f w = B.push f c (B.abst a w) in
xlate_term c f w
in
xlate_term c f t
let xlate_entry f = function
- | e, pars, uri, u, None ->
- let f u = f (e, uri, B.abst [] u) in
+ | pars, u, None ->
let f c = unwind_to_xlate_term f c u in
xlate_pars f pars
- | e, pars, uri, u, Some (_, t) ->
- let f u t = f (e, uri, B.abbr [] (B.Cast ([], u, t))) in
+ | pars, u, Some t ->
+ let f u t = f (B.Cast ([], u, t)) in
let f c u = unwind_to_xlate_term (f u) c t in
let f c = unwind_to_xlate_term (f c) c u in
xlate_pars f pars
-let xlate_entity f = function
- | None -> f None
- | Some e -> let f e = f (Some e) in xlate_entry f e
-
(* Interface functions ******************************************************)
-let brg_of_meta = xlate_entity
+let brg_of_meta = xlate_entry
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-val brg_of_meta: (Brg.entity -> 'a) -> Meta.entity -> 'a
+val brg_of_meta: (Brg.term -> 'a) -> Meta.entry -> 'a
module P = Printf
module F = Format
module U = NUri
+module C = Cps
module L = Log
+module Y = Entity
module M = Meta
type counters = {
let count_par f c (_, w) = count_term f c w
-let count_entry f c = function
- | _, pars, u, w, None ->
+let count_xterm f c = function
+ | None -> f c
+ | Some v -> count_term f c v
+
+let count_entity f c = function
+ | _, u, Y.Abst (pars, w, xv) ->
let c = {c with eabsts = succ c.eabsts} in
let c = {c with pabsts = c.pabsts + List.length pars} in
let c = {c with uris = u :: c.uris; nodes = succ c.nodes + List.length pars} in
+ let f c = count_xterm f c xv in
let f c = count_term f c w in
Cps.list_fold_left f count_par c pars
- | _, pars, _, w, Some (_, v) ->
+ | _, _, Y.Abbr (pars, w, xv) ->
let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in
let c = {c with pabsts = c.pabsts + List.length pars} in
let c = {c with nodes = c.nodes + List.length pars} in
- let f c = count_term f c v in
+ let f c = count_xterm f c xv in
let f c = count_term f c w in
Cps.list_fold_left f count_par c pars
-let count_entity f c = function
- | Some e -> count_entry f c e
- | None -> f c
-
let print_counters f c =
let terms = c.tsorts + c.tlrefs + c.tgrefs + c.tappls + c.tabsts in
let pars = c.pabsts + c.pappls in
| true -> "Type"
| false -> "Prop"
-let string_of_transparent = function
- | true -> "="
- | false -> "~"
+let pp_transparent frm a =
+ let err () = F.fprintf frm "%s" "=" in
+ let f () = F.fprintf frm "%s" "~" in
+ Y.priv err f a
let pp_list pp opend sep closed frm l =
let rec aux frm = function
F.fprintf frm "@[[%s:%a].%a@]" id pp_term w pp_term t
let pp_par frm (id, w) =
- F.fprintf frm "%s:%a" id pp_term w
+ F.fprintf frm "%s:%a" id pp_term w
let pp_pars = pp_rev_list pp_par "[" "," "]"
-let pp_body frm = function
- | None -> ()
- | Some (trans, t) ->
- F.fprintf frm "%s%a" (string_of_transparent trans) pp_term t
+let pp_body a frm = function
+ | None -> ()
+ | Some t -> F.fprintf frm "%a%a" pp_transparent a pp_term t
-let pp_entry frm (l, pars, uri, u, body) =
- F.fprintf frm "@[%u@@%s%a%a:%a@]@\n%!"
- l (U.string_of_uri uri) pp_pars pars pp_body body pp_term u
+let pp_entity frm = function
+ | a, uri, Y.Abst (pars, u, body)
+ | a, uri, Y.Abbr (pars, u, body) ->
+ F.fprintf frm "@[%u@@%s%a%a:%a@]@\n%!"
+ (Y.mark C.err C.start a) (U.string_of_uri uri)
+ pp_pars pars (pp_body a) body pp_term u
-let pp_entity f frm = function
- | Some entry -> pp_entry frm entry; f ()
- | None -> f ()
+let pp_entity f frm entity =
+ pp_entity frm entity; f ()
module T = Time
module H = Hierarchy
module O = Output
+module Y = Entity
+module X = Library
module AP = AutProcess
module AO = AutOutput
module MA = MetaAut
module MO = MetaOutput
module ML = MetaLibrary
module MBrg = MetaBrg
-module G = Library
module BrgO = BrgOutput
module BrgR = BrgReduction
module BrgU = BrgUntrusted
let kernel_of_meta f st entity = match !kernel with
| Brg ->
let f entity = f st (BrgEntity entity) in
- MBrg.brg_of_meta f entity
+ Y.xlate f MBrg.brg_of_meta entity
| Bag ->
let f entity = f st (BagEntity entity) in
- MBag.bag_of_meta f entity
+ Y.xlate f MBag.bag_of_meta entity
let count_entity st = function
| BrgEntity entity -> {st with brgc = count BrgO.count_entity st.brgc entity}
| BagEntity entity -> {st with bagc = count BagO.count_entity st.bagc entity}
let export_entity si g = function
- | BrgEntity entity -> G.old_export_entity BrgO.export_entry si g entity
- | BagEntity _ -> ()
+ | BrgEntity entity -> X.old_export_entity BrgO.export_term si g entity
+ | BagEntity _ -> ()
let type_check f st si g k =
let brg_err msg = brg_error "Type Error" msg; failwith "Interrupted" in
- let f _ = function
- | None -> f st None
- | Some (i, u, _) -> f st (Some (i, u))
- in
+ let f _ (a, u, _) = f st a u in
match k with
| BrgEntity entity -> BrgU.type_check brg_err f ~si g entity
| BagEntity entity -> BagU.type_check f ~si g entity
close_in ich;
if !L.level > 0 then T.utime_stamp "parsed";
let rec aux st = function
- | [] -> st
+ | [] -> st
| entity :: tl ->
(* stage 3 *)
- let f st = function
- | None -> st
- | Some (i, u) ->
- if !progress then
- L.warn (P.sprintf "[%u] %s" i (U.string_of_uri u));
- st
+ let f st a u =
+ if !progress then
+ let s = U.string_of_uri u in
+ let err () = L.warn (P.sprintf "%s" s); st in
+ let f i = L.warn (P.sprintf "[%u] %s" i s); st in
+ Y.mark err f a
+ else
+ st
in
(* stage 2 *)
let f st entity =
in
(* stage 0 *)
let st = {st with ac = count AO.count_entity st.ac entity} in
+ let err st mst = {st with mst = mst} in
let f st entity =
let st =
- if !stage > 0 then MA.meta_of_aut (f st) st.mst entity else st
+ if !stage > 0 then
+ MA.meta_of_aut (err st) (f st) st.mst entity
+ else st
in
aux st tl
in
projects / helm.git / commitdiff