src/common/output.cmi
src/common/output.cmx: src/common/options.cmx src/lib/log.cmx \
src/common/output.cmi
-src/common/entity.cmo: src/common/options.cmx src/automath/aut.cmx
-src/common/entity.cmx: src/common/options.cmx src/automath/aut.cmx
+src/common/entity.cmo: src/common/options.cmx
+src/common/entity.cmx: src/common/options.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/text/txtTxt.cmi: src/text/txt.cmx
src/text/txtTxt.cmo: src/text/txt.cmx src/lib/cps.cmx src/text/txtTxt.cmi
src/text/txtTxt.cmx: src/text/txt.cmx src/lib/cps.cmx src/text/txtTxt.cmi
-src/automath/aut.cmo:
-src/automath/aut.cmx:
+src/automath/aut.cmo: src/common/entity.cmx
+src/automath/aut.cmx: src/common/entity.cmx
src/automath/autProcess.cmi: src/automath/aut.cmx
src/automath/autProcess.cmo: src/automath/aut.cmx src/automath/autProcess.cmi
src/automath/autProcess.cmx: src/automath/aut.cmx src/automath/autProcess.cmi
src/basic_rg/brgCrg.cmi
src/basic_rg/brgOutput.cmi: src/xml/xmlLibrary.cmi src/lib/log.cmi \
src/basic_rg/brg.cmx
-src/basic_rg/brgOutput.cmo: src/xml/xmlLibrary.cmi src/common/options.cmx \
+src/basic_rg/brgOutput.cmo: src/xml/xmlCrg.cmi src/common/options.cmx \
src/lib/log.cmi src/common/hierarchy.cmi src/common/entity.cmx \
- src/lib/cps.cmx src/basic_rg/brg.cmx src/basic_rg/brgOutput.cmi
-src/basic_rg/brgOutput.cmx: src/xml/xmlLibrary.cmx src/common/options.cmx \
+ src/lib/cps.cmx src/basic_rg/brgCrg.cmi src/basic_rg/brg.cmx \
+ src/basic_rg/brgOutput.cmi
+src/basic_rg/brgOutput.cmx: src/xml/xmlCrg.cmx src/common/options.cmx \
src/lib/log.cmx src/common/hierarchy.cmx src/common/entity.cmx \
- src/lib/cps.cmx src/basic_rg/brg.cmx src/basic_rg/brgOutput.cmi
+ src/lib/cps.cmx src/basic_rg/brgCrg.cmx src/basic_rg/brg.cmx \
+ src/basic_rg/brgOutput.cmi
src/basic_rg/brgEnvironment.cmi: src/basic_rg/brg.cmx
src/basic_rg/brgEnvironment.cmo: src/common/entity.cmx src/basic_rg/brg.cmx \
src/basic_rg/brgEnvironment.cmi
src/basic_rg/brgType.cmo: src/lib/share.cmx src/lib/log.cmi \
src/common/hierarchy.cmi src/common/entity.cmx src/lib/cps.cmx \
src/basic_rg/brgSubstitution.cmi src/basic_rg/brgReduction.cmi \
- src/basic_rg/brgOutput.cmi src/basic_rg/brgEnvironment.cmi \
- src/basic_rg/brg.cmx src/basic_rg/brgType.cmi
+ src/basic_rg/brgEnvironment.cmi src/basic_rg/brg.cmx \
+ src/basic_rg/brgType.cmi
src/basic_rg/brgType.cmx: src/lib/share.cmx src/lib/log.cmx \
src/common/hierarchy.cmx src/common/entity.cmx src/lib/cps.cmx \
src/basic_rg/brgSubstitution.cmx src/basic_rg/brgReduction.cmx \
- src/basic_rg/brgOutput.cmx src/basic_rg/brgEnvironment.cmx \
- src/basic_rg/brg.cmx src/basic_rg/brgType.cmi
+ 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/brg.cmx
src/basic_rg/brgUntrusted.cmo: src/lib/log.cmi src/common/entity.cmx \
$(H)$(OCAMLDEP) $^ > .depend.opt
clean:
- @echo " CLEAN"
+ @echo " CLEAN . $(SRC)"
$(H)find -name "*~" | xargs $(RM) $(CLEAN)
lint: $(XMLS)
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-type id = string (* identifier *)
+module E = Entity
+
+type id = E.id
type qid = id * bool * id list (* qualified identifier: name, local?, path *)
V_______________________________________________________________ *)
{
- module L = Log
- module O = Options
- module P = AutParser
+ module L = Log
+ module G = Options
+ module AP = AutParser
- let out s = if !O.debug_lexer then L.warn s else ()
+ let out s = if !G.debug_lexer then L.warn s else ()
(* This turns an Automath identifier into an XML nmtoken *)
let quote id =
| SPC { token lexbuf }
| LC { line_comment lexbuf; token lexbuf }
| OC { block_comment lexbuf; token lexbuf }
- | "_E" { out "E"; P.E }
- | "'_E'" { out "E"; P.E }
- | "---" { out "EB"; P.EB }
- | "'eb'" { out "EB"; P.EB }
- | "EB" { out "EB"; P.EB }
- | "--" { out "EXIT"; P.EXIT }
- | "PN" { out "PN"; P.PN }
- | "'pn'" { out "PN"; P.PN }
- | "PRIM" { out "PN"; P.PN }
- | "'prim'" { out "PN"; P.PN }
- | "???" { out "PN"; P.PN }
- | "PROP" { out "PROP"; P.PROP }
- | "'prop'" { out "PROP"; P.PROP }
- | "TYPE" { out "TYPE"; P.TYPE }
- | "'type'" { out "TYPE"; P.TYPE }
+ | "_E" { out "E"; AP.E }
+ | "'_E'" { out "E"; AP.E }
+ | "---" { out "EB"; AP.EB }
+ | "'eb'" { out "EB"; AP.EB }
+ | "EB" { out "EB"; AP.EB }
+ | "--" { out "EXIT"; AP.EXIT }
+ | "PN" { out "PN"; AP.PN }
+ | "'pn'" { out "PN"; AP.PN }
+ | "PRIM" { out "PN"; AP.PN }
+ | "'prim'" { out "PN"; AP.PN }
+ | "???" { out "PN"; AP.PN }
+ | "PROP" { out "PROP"; AP.PROP }
+ | "'prop'" { out "PROP"; AP.PROP }
+ | "TYPE" { out "TYPE"; AP.TYPE }
+ | "'type'" { out "TYPE"; AP.TYPE }
| ID { out "ID";
let s = Lexing.lexeme lexbuf in
- if !O.unquote then P.IDENT s else P.IDENT (quote s)
+ if !G.unquote then AP.IDENT s else AP.IDENT (quote s)
}
- | ":=" { out "DEF"; P.DEF }
- | "(" { out "OP"; P.OP }
- | ")" { out "CP"; P.CP }
- | "[" { out "OB"; P.OB }
- | "]" { out "CB"; P.CB }
- | "<" { out "OA"; P.OA }
- | ">" { out "CA"; P.CA }
- | "@" { out "AT"; P.AT }
- | "~" { out "TD"; P.TD }
- | "\"" { out "QT"; P.QT }
- | ":" { out "CN"; P.CN }
- | "," { out "CM"; P.CM }
- | ";" { out "SC"; P.SC }
- | "." { out "FS"; P.FS }
- | "+" { out "PLUS"; P.PLUS }
- | "-" { out "MINUS"; P.MINUS }
- | "*" { out "TIMES"; P.TIMES }
- | "=" { out "DEF"; P.DEF }
- | eof { out "EOF"; P.EOF }
+ | ":=" { out "DEF"; AP.DEF }
+ | "(" { out "OP"; AP.OP }
+ | ")" { out "CP"; AP.CP }
+ | "[" { out "OB"; AP.OB }
+ | "]" { out "CB"; AP.CB }
+ | "<" { out "OA"; AP.OA }
+ | ">" { out "CA"; AP.CA }
+ | "@" { out "AT"; AP.AT }
+ | "~" { out "TD"; AP.TD }
+ | "\"" { out "QT"; AP.QT }
+ | ":" { out "CN"; AP.CN }
+ | "," { out "CM"; AP.CM }
+ | ";" { out "SC"; AP.SC }
+ | "." { out "FS"; AP.FS }
+ | "+" { out "PLUS"; AP.PLUS }
+ | "-" { out "MINUS"; AP.MINUS }
+ | "*" { out "TIMES"; AP.TIMES }
+ | "=" { out "DEF"; AP.DEF }
+ | eof { out "EOF"; AP.EOF }
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module P = Printf
-module C = Cps
-module L = Log
-module A = Aut
-module R = AutProcess
+module P = Printf
+module C = Cps
+module L = Log
+module A = Aut
+module AA = AutProcess
type counters = {
sections: int;
L.warn (P.sprintf " Implicit after global: %7u" iag);
f ()
in
- R.get_counters f c
+ AA.get_counters f c
*/
%{
- module O = Options
+ module G = Options
module A = Aut
- let _ = Parsing.set_trace !O.debug_parser
+ let _ = Parsing.set_trace !G.debug_parser
%}
%token <int> NUM
%token <string> IDENT
(* kernel version: basic, absolute, global *)
(* note : experimental *)
-type uri = Entity.uri
-type id = Entity.id
+module E = Entity
+
+type uri = E.uri
+type id = E.id
type bind = Void (* exclusion *)
| Abst of term (* abstraction *)
| Appl of term * term (* argument, function *)
| Bind of int * id * bind * term (* location, name, binder, scope *)
-type entity = term Entity.entity (* attrs, uri, binder *)
+type entity = term E.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
+module K = U.UriHash
+module E = Entity
+module Z = Bag
-exception ObjectNotFound of B.message
+exception ObjectNotFound of Z.message
let hsize = 7000
-let env = H.create hsize
+let env = K.create hsize
(* Internal functions *******************************************************)
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 entry = (E.Apix age :: a), uri, b in
+ K.add env uri entry; f entry
let get_entity f uri =
- try f (H.find env uri) with Not_found -> error uri
+ try f (K.find env uri) with Not_found -> error uri
module F = Format
module U = NUri
module L = Log
-module O = Options
-module Y = Entity
+module G = Options
+module E = Entity
module H = Hierarchy
-module B = Bag
+module Z = Bag
type counters = {
eabsts: int;
}
let rec count_term_binder f c = function
- | B.Abst w ->
+ | Z.Abst w ->
let c = {c with tabsts = succ c.tabsts} in
count_term f c w
- | B.Abbr v ->
+ | Z.Abbr v ->
let c = {c with tabbrs = succ c.tabbrs} in
count_term f c v
- | B.Void -> f c
+ | Z.Void -> f c
and count_term f c = function
- | B.Sort _ ->
+ | Z.Sort _ ->
f {c with tsorts = succ c.tsorts}
- | B.LRef _ ->
+ | Z.LRef _ ->
f {c with tlrefs = succ c.tlrefs}
- | B.GRef _ ->
+ | Z.GRef _ ->
f {c with tgrefs = succ c.tgrefs}
- | B.Cast (v, t) ->
+ | Z.Cast (v, t) ->
let c = {c with tcasts = succ c.tcasts} in
let f c = count_term f c t in
count_term f c v
- | B.Appl (v, t) ->
+ | Z.Appl (v, t) ->
let c = {c with tappls = succ c.tappls} in
let f c = count_term f c t in
count_term f c v
- | B.Bind (_, _, b, t) ->
+ | Z.Bind (_, _, b, t) ->
let f c = count_term_binder f c b in
count_term f c t
let count_entity f c = function
- | _, _, Y.Abst w ->
+ | _, _, E.Abst w ->
let c = {c with eabsts = succ c.eabsts} in
count_term f c w
- | _, _, Y.Abbr v ->
+ | _, _, E.Abbr v ->
let c = {c with eabbrs = succ c.eabbrs} in
count_term f c v
- | _, _, Y.Void -> assert false
+ | _, _, E.Void -> assert false
let print_counters f c =
let terms =
c.tabbrs
in
let items = c.eabsts + c.eabbrs in
- let locations = B.locations () in
+ let locations = Z.locations () in
L.warn (P.sprintf " Kernel representation summary (basic_ag)");
L.warn (P.sprintf " Total entry items: %7u" items);
L.warn (P.sprintf " Declaration items: %7u" c.eabsts);
f ()
let res l id =
- if !O.indexes then P.sprintf "#%u" l else id
+ if !G.indexes then P.sprintf "#%u" l else id
let rec pp_term c frm = function
- | B.Sort h ->
+ | Z.Sort h ->
let err () = F.fprintf frm "@[*%u@]" h in
let f s = F.fprintf frm "@[%s@]" s in
H.string_of_sort err f h
- | B.LRef i ->
+ | Z.LRef i ->
let f = function
| Some (id, _) -> F.fprintf frm "@[%s@]" id
| None -> F.fprintf frm "@[#%u@]" i
in
- if !O.indexes then f None else B.get f c i
- | B.GRef s -> F.fprintf frm "@[$%s@]" (U.string_of_uri s)
- | B.Cast (u, t) ->
+ if !G.indexes then f None else Z.get f c i
+ | Z.GRef s -> F.fprintf frm "@[$%s@]" (U.string_of_uri s)
+ | Z.Cast (u, t) ->
F.fprintf frm "@[{%a}.%a@]" (pp_term c) u (pp_term c) t
- | B.Appl (v, t) ->
+ | Z.Appl (v, t) ->
F.fprintf frm "@[(%a).%a@]" (pp_term c) v (pp_term c) t
- | B.Bind (l, id, B.Abst w, t) ->
+ | Z.Bind (l, id, Z.Abst w, t) ->
let f cc =
F.fprintf frm "@[[%s:%a].%a@]" (res l id) (pp_term c) w (pp_term cc) t
in
- B.push "output abst" f c l id (B.Abst w)
- | B.Bind (l, id, B.Abbr v, t) ->
+ Z.push "output abst" f c l id (Z.Abst w)
+ | Z.Bind (l, id, Z.Abbr v, t) ->
let f cc =
F.fprintf frm "@[[%s=%a].%a@]" (res l id) (pp_term c) v (pp_term cc) t
in
- B.push "output abbr" f c l id (B.Abbr v)
- | B.Bind (l, id, B.Void, t) ->
+ Z.push "output abbr" f c l id (Z.Abbr v)
+ | Z.Bind (l, id, Z.Void, t) ->
let f cc = F.fprintf frm "@[[%s].%a@]" (res l id) (pp_term cc) t in
- B.push "output void" f c l id B.Void
+ Z.push "output void" f c l id Z.Void
let pp_lenv frm c =
let pp_entry frm = function
- | l, id, B.Abst w ->
+ | l, id, Z.Abst w ->
F.fprintf frm "@,@[%s : %a@]" (res l id) (pp_term c) w
- | l, id, B.Abbr v ->
+ | l, id, Z.Abbr v ->
F.fprintf frm "@,@[%s = %a@]" (res l id) (pp_term c) v
- | l, id, B.Void ->
+ | l, id, Z.Void ->
F.fprintf frm "@,%s" (res l id)
in
let iter map frm l = List.iter (map frm) l in
let f es = F.fprintf frm "%a" (iter pp_entry) (List.rev es) in
- B.contents f c
+ Z.contents f c
let specs = {
L.pp_term = pp_term; L.pp_lenv = pp_lenv
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module U = NUri
-module C = Cps
-module L = Log
-module Y = Entity
-module B = Bag
-module O = BagOutput
-module E = BagEnvironment
-module S = BagSubstitution
+module U = NUri
+module C = Cps
+module L = Log
+module E = Entity
+module Z = Bag
+module ZO = BagOutput
+module ZE = BagEnvironment
+module ZS = BagSubstitution
type machine = {
i: int;
- c: B.lenv;
- s: B.term list
+ c: Z.lenv;
+ s: Z.term list
}
type whd_result =
| Sort_ of int
- | LRef_ of int * B.term option
- | GRef_ of B.entity
- | Bind_ of int * B.id * B.term * B.term
+ | LRef_ of int * Z.term option
+ | GRef_ of Z.entity
+ | Bind_ of int * Z.id * Z.term * Z.term
type ho_whd_result =
| Sort of int
- | Abst of B.term
+ | Abst of Z.term
(* Internal functions *******************************************************)
let term_of_whdr = function
- | Sort_ h -> B.Sort h
- | LRef_ (i, _) -> B.LRef i
- | GRef_ (_, uri, _) -> B.GRef uri
- | Bind_ (l, id, w, t) -> B.bind_abst l id w t
+ | Sort_ h -> Z.Sort h
+ | LRef_ (i, _) -> Z.LRef i
+ | GRef_ (_, uri, _) -> Z.GRef uri
+ | Bind_ (l, id, w, t) -> Z.bind_abst l id w t
let level = 5
let log1 s c t =
let sc, st = s ^ " in the environment", "the term" in
- L.log O.specs level (L.et_items1 sc c st t)
+ L.log ZO.specs level (L.et_items1 sc c st t)
let log2 s cu u ct t =
let s1, s2, s3 = s ^ " in the environment", "the term", "and in the environment" in
- L.log O.specs level (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
+ L.log ZO.specs level (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
-let empty_machine = {i = 0; c = B.empty_lenv; s = []}
+let empty_machine = {i = 0; c = Z.empty_lenv; s = []}
let inc m = {m with i = succ m.i}
let unwind_to_term f m t =
- let map f t (l, id, b) = f (B.Bind (l, id, b, t)) in
+ let map f t (l, id, b) = f (Z.Bind (l, id, b, t)) in
let f mc = C.list_fold_left f map t mc in
- B.contents f m.c
+ Z.contents f m.c
let unwind_stack f m =
let map f v = unwind_to_term f m v in
| Some (_, b) -> f b
| None -> assert false
in
- let f c = B.get f c i in
- B.append f c m.c
+ let f c = Z.get f c i in
+ Z.append f c m.c
let push msg f c m l id w =
assert (m.s = []);
- let f w = B.push msg f c l id (B.Abst w) in
+ let f w = Z.push msg f c l id (Z.Abst w) in
unwind_to_term f m w
(* to share *)
let rec whd f c m x =
(* L.warn "entering R.whd"; *)
match x with
- | B.Sort h -> f m (Sort_ h)
- | B.GRef uri ->
+ | Z.Sort h -> f m (Sort_ h)
+ | Z.GRef uri ->
let f entry = f m (GRef_ entry) in
- E.get_entity f uri
- | B.LRef i ->
+ ZE.get_entity f uri
+ | Z.LRef i ->
let f = function
- | B.Void -> f m (LRef_ (i, None))
- | B.Abst t -> f m (LRef_ (i, Some t))
- | B.Abbr t -> whd f c m t
+ | Z.Void -> f m (LRef_ (i, None))
+ | Z.Abst t -> f m (LRef_ (i, Some t))
+ | Z.Abbr t -> whd f c m t
in
get f c m i
- | B.Cast (_, t) -> whd f c m t
- | B.Appl (v, t) -> whd f c {m with s = v :: m.s} t
- | B.Bind (l, id, B.Abst w, t) ->
+ | Z.Cast (_, t) -> whd f c m t
+ | Z.Appl (v, t) -> whd f c {m with s = v :: m.s} t
+ | Z.Bind (l, id, Z.Abst w, t) ->
begin match m.s with
| [] -> f m (Bind_ (l, id, w, t))
| v :: tl ->
- let nl = B.new_location () in
- let f mc = S.subst (whd f c {m with c = mc; s = tl}) nl l t in
- B.push "!" f m.c nl id (B.Abbr (B.Cast (w, v)))
+ let nl = Z.new_location () in
+ let f mc = ZS.subst (whd f c {m with c = mc; s = tl}) nl l t in
+ Z.push "!" f m.c nl id (Z.Abbr (Z.Cast (w, v)))
end
- | B.Bind (l, id, b, t) ->
- let nl = B.new_location () in
- let f mc = S.subst (whd f c {m with c = mc}) nl l t in
- B.push "!" f m.c nl id b
+ | Z.Bind (l, id, b, t) ->
+ let nl = Z.new_location () in
+ let f mc = ZS.subst (whd f c {m with c = mc}) nl l t in
+ Z.push "!" f m.c nl id b
(* Interface functions ******************************************************)
| 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_ (_, _, Y.Abst w) -> ho_whd f c m w
- | GRef_ (_, _, Y.Abbr v) -> ho_whd f c m v
+ | GRef_ (_, _, E.Abst w) -> ho_whd f c m w
+ | GRef_ (_, _, E.Abbr v) -> ho_whd f c m v
| LRef_ (_, None) -> assert false
- | GRef_ (_, _, Y.Void) -> assert false
+ | GRef_ (_, _, E.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_ ((Y.Apix a1 :: _), _, Y.Abst _),
- GRef_ ((Y.Apix a2 :: _), _, Y.Abst _) ->
+ | GRef_ ((E.Apix a1 :: _), _, E.Abst _),
+ GRef_ ((E.Apix a2 :: _), _, E.Abst _) ->
if a1 = a2 then are_convertible_stacks f ~si a c m1 m2 else f false
- | GRef_ ((Y.Apix a1 :: _), _, Y.Abbr v1),
- GRef_ ((Y.Apix a2 :: _), _, Y.Abbr v2) ->
+ | GRef_ ((E.Apix a1 :: _), _, E.Abbr v1),
+ GRef_ ((E.Apix a2 :: _), _, E.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_ (_, _, Y.Abbr v2) ->
+ | _, GRef_ (_, _, E.Abbr v2) ->
whd (aux m1 r1) c m2 v2
- | GRef_ (_, _, Y.Abbr v1), _ ->
+ | GRef_ (_, _, E.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
+ let l = Z.new_location () in
let h c =
let m1, m2 = inc m1, inc m2 in
- let f t1 = S.subst (are_convertible f ~si a c m1 t1 m2) l l2 t2 in
- S.subst f l l1 t1
+ let f t1 = ZS.subst (are_convertible f ~si a c m1 t1 m2) l l2 t2 in
+ ZS.subst f l l1 t1
in
let f r = if r then push "!" h c m1 l id1 w1 else f false in
are_convertible f ~si a c m1 w1 m2 w2
V_______________________________________________________________ *)
module S = Share
-module B = Bag
+module Z = Bag
(* Internal functions *******************************************************)
let rec lref_map_bind f map b = match b with
- | B.Abbr v ->
- let f v' = f (S.sh1 v v' b B.abbr) in
+ | Z.Abbr v ->
+ let f v' = f (S.sh1 v v' b Z.abbr) in
lref_map f map v
- | B.Abst w ->
- let f w' = f (S.sh1 w w' b B.abst) in
+ | Z.Abst w ->
+ let f w' = f (S.sh1 w w' b Z.abst) in
lref_map f map w
- | B.Void -> f b
+ | Z.Void -> f b
and lref_map f map t = match t with
- | B.LRef i ->
- let ii = map i in f (S.sh1 i ii t B.lref)
- | B.GRef _ -> f t
- | B.Sort _ -> f t
- | B.Cast (w, u) ->
- let f w' u' = f (S.sh2 w w' u u' t B.cast) in
+ | Z.LRef i ->
+ let ii = map i in f (S.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' = lref_map (f w') map u in
lref_map f map w
- | B.Appl (w, u) ->
- let f w' u' = f (S.sh2 w w' u u' t B.appl) in
+ | Z.Appl (w, u) ->
+ let f w' u' = f (S.sh2 w w' u u' t Z.appl) in
let f w' = lref_map (f w') map u in
lref_map f map w
- | B.Bind (l, id, b, u) ->
- let f b' u' = f (S.sh2 b b' u u' t (B.bind l id)) in
+ | 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' = lref_map (f b') map u in
lref_map_bind f map b
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module U = NUri
-module C = Cps
-module S = Share
-module L = Log
-module Y = Entity
-module H = Hierarchy
-module B = Bag
-module O = BagOutput
-module E = BagEnvironment
-module R = BagReduction
+module U = NUri
+module C = Cps
+module S = Share
+module L = Log
+module E = Entity
+module H = Hierarchy
+module Z = Bag
+module ZO = BagOutput
+module ZE = BagEnvironment
+module ZR = BagReduction
-exception TypeError of B.message
+exception TypeError of Z.message
(* Internal functions *******************************************************)
let log1 s c t =
let sc, st = s ^ " in the envireonment", "the term" in
- L.log O.specs level (L.et_items1 sc c st t)
+ L.log ZO.specs level (L.et_items1 sc c st t)
let error1 st c t =
let sc = "In the envireonment" in
raise (TypeError (L.et_items3 sc c st1 t1 st2 t2 st3 t3))
let mk_gref u l =
- let map t v = B.Appl (v, t) in
- List.fold_left map (B.GRef u) l
+ let map t v = Z.Appl (v, t) in
+ List.fold_left map (Z.GRef u) l
(* Interface functions ******************************************************)
(* L.warn "Entering T.b_type_of"; *)
log1 "Now checking" c x;
match x with
- | B.Sort h ->
- let h = H.apply h in f x (B.Sort h)
- | B.LRef i ->
+ | Z.Sort h ->
+ let h = H.apply h in f x (Z.Sort h)
+ | Z.LRef i ->
let f = function
- | Some (_, B.Abst w) -> f x w
- | Some (_, B.Abbr (B.Cast (w, v))) -> f x w
- | Some (_, B.Abbr _) -> assert false
- | Some (_, B.Void) ->
+ | Some (_, Z.Abst w) -> f x w
+ | Some (_, Z.Abbr (Z.Cast (w, v))) -> f x w
+ | Some (_, Z.Abbr _) -> assert false
+ | Some (_, Z.Void) ->
error1 "reference to excluded variable" c x
| None ->
error1 "variable not found" c x
in
- B.get f c i
- | B.GRef uri ->
+ Z.get f c i
+ | Z.GRef uri ->
let f = function
- | _, _, Y.Abst w -> f x w
- | _, _, Y.Abbr (B.Cast (w, v)) -> f x w
- | _, _, Y.Abbr _ -> assert false
- | _, _, Y.Void -> assert false
+ | _, _, E.Abst w -> f x w
+ | _, _, E.Abbr (Z.Cast (w, v)) -> f x w
+ | _, _, E.Abbr _ -> assert false
+ | _, _, E.Void -> assert false
in
- E.get_entity f uri
- | B.Bind (l, id, B.Abbr v, t) ->
+ 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 (B.bind_abbr l id)) (B.bind_abbr l id xv tt)
+ f (S.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 = B.push "type abbr" (f xv) c l id (B.Abbr xv) in
+ let f xv = Z.push "type abbr" (f xv) c l id (Z.Abbr xv) in
let f xv vv = match xv with
- | B.Cast _ -> f xv
- | _ -> f (B.Cast (vv, xv))
+ | Z.Cast _ -> f xv
+ | _ -> f (Z.Cast (vv, xv))
in
type_of f st c v
- | B.Bind (l, id, B.Abst u, t) ->
+ | Z.Bind (l, id, Z.Abst u, t) ->
let f xu xt tt =
- f (S.sh2 u xu t xt x (B.bind_abst l id)) (B.bind_abst l id xu tt)
+ f (S.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 _ = B.push "type abst" (f xu) c l id (B.Abst xu) in
+ let f xu _ = Z.push "type abst" (f xu) c l id (Z.Abst xu) in
type_of f st c u
- | B.Bind (l, id, B.Void, t) ->
+ | Z.Bind (l, id, Z.Void, t) ->
let f xt tt =
- f (S.sh1 t xt x (B.bind l id B.Void)) (B.bind l id B.Void tt)
+ f (S.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
- B.push "type void" f c l id B.Void
- | B.Appl (v, t) ->
+ Z.push "type void" f c l id Z.Void
+ | Z.Appl (v, t) ->
let f xv vv xt tt = function
- | R.Abst w ->
+ | ZR.Abst w ->
L.box (succ level);
- L.log O.specs (succ level) (L.t_items1 "Just scanned" c w);
+ L.log ZO.specs (succ level) (L.t_items1 "Just scanned" c w);
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 B.appl) (B.appl xv tt)
+ if a then f (S.sh2 v xv t xt x Z.appl) (Z.appl xv tt)
else error3 c xv vv w
in
- R.are_convertible f ~si:st.Y.si c w vv
+ ZR.are_convertible f ~si:st.E.si c w vv
| _ ->
error1 "not a function" c xt
in
- let f xv vv xt tt = R.ho_whd (f xv vv xt tt) c tt in
+ let f xv vv xt tt = ZR.ho_whd (f xv vv xt tt) c tt in
let f xv vv = b_type_of (f xv vv) st c t in
type_of f st c v
- | B.Cast (u, t) ->
+ | 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 B.cast) xu else error3 c xt tt xu
+ if a then f (S.sh2 u xu t xt x Z.cast) xu else error3 c xt tt xu
in
- let f xu xt tt = R.are_convertible (f xu xt tt) ~si:st.Y.si c xu tt in
+ let f xu xt tt = ZR.are_convertible (f xu xt tt) ~si:st.E.si c xu tt in
let f xu _ = b_type_of (f xu) st c t in
type_of f st c u
\ / 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
+module U = NUri
+module L = Log
+module E = Entity
+module Z = Bag
+module ZE = BagEnvironment
+module ZT = BagType
(* Interface functions ******************************************************)
(* to share *)
let type_check f st = function
- | 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 st 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 st B.empty_lenv t
- | _, _, Y.Void -> assert false
+ | a, uri, E.Abst t ->
+ let f xt tt = ZE.set_entity (f tt) (a, uri, E.Abst xt) in
+ L.loc := U.string_of_uri uri; ZT.type_of f st Z.empty_lenv t
+ | a, uri, E.Abbr t ->
+ let f xt tt = ZE.set_entity (f tt) (a, uri, E.Abbr xt) in
+ L.loc := U.string_of_uri uri; ZT.type_of f st Z.empty_lenv t
+ | _, _, E.Void -> assert false
(* kernel version: basic, relative, global *)
(* note : ufficial basic lambda-delta *)
-type uri = Entity.uri
-type id = Entity.id
-type attrs = Entity.attrs
+module E = Entity
+
+type uri = E.uri
+type id = E.id
+type attrs = E.attrs
type bind = Void (* *)
| Abst of term (* type *)
| Appl of attrs * term * term (* attrs, argument, function *)
| Bind of attrs * bind * term (* attrs, binder, scope *)
-type entity = term Entity.entity (* attrs, uri, binder *)
+type entity = term E.entity (* attrs, uri, binder *)
type lenv = Null
(* Cons: tail, relative local environment, attrs, binder *)
V_______________________________________________________________ *)
module C = Cps
-module Y = Entity
-module M = Marks
+module E = Entity
+module J = Marks
module D = Crg
module B = Brg
let rec xlate_term f = function
| D.TSort (a, l) -> f (B.Sort (a, l))
| D.TGRef (a, n) -> f (B.GRef (a, n))
- | D.TLRef (a, _, _) -> let f i = f (B.LRef (a, i)) in Y.apix C.err f a
+ | D.TLRef (a, _, _) -> let f i = f (B.LRef (a, i)) in E.apix C.err f a
| D.TCast (a, u, t) ->
let f uu tt = f (B.Cast (a, uu, tt)) in
let f uu = xlate_term (f uu) t in
and xlate_bind x a b =
let f a ns = a, ns in
- let a, ns = Y.get_names f a in
+ let a, ns = E.get_names f a in
match b with
| D.Abst ws ->
let map x n w =
- let f ww = B.Bind (n :: M.new_mark () :: a, B.Abst ww, x) in
+ let f ww = B.Bind (n :: J.new_mark () :: a, B.Abst ww, x) in
xlate_term f w
in
List.fold_left2 map x ns ws
V_______________________________________________________________ *)
module U = NUri
-module H = U.UriHash
-module Y = Entity
+module K = U.UriHash
+module E = Entity
module B = Brg
let hsize = 7000
-let env = H.create hsize
+let env = K.create hsize
(* Internal functions *******************************************************)
(* decps *)
let set_entity (a, uri, b) =
let age = get_age () in
- let entity = (Y.Apix age :: a), uri, b in
- H.add env uri entity; entity
+ let entity = (E.Apix age :: a), uri, b in
+ K.add env uri entity; entity
let get_entity uri =
- try H.find env uri with Not_found -> [], uri, Y.Void
+ try K.find env uri with Not_found -> [], uri, E.Void
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module P = Printf
-module F = Format
-module C = Cps
-module U = NUri
-module L = Log
-module O = Options
-module Y = Entity
-module X = XmlLibrary
-module H = Hierarchy
-module B = Brg
+module P = Printf
+module F = Format
+module C = Cps
+module U = NUri
+module L = Log
+module G = Options
+module E = Entity
+module H = Hierarchy
+module XD = XmlCrg
+module B = Brg
+module BD = BrgCrg
(* nodes count **************************************************************)
count_term_binder f c e b
let count_entity f c = function
- | _, u, Y.Abst w ->
+ | _, u, E.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 w
- | _, _, Y.Abbr v ->
+ | _, _, E.Abbr v ->
let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in
count_term f c B.empty v
- | _, _, Y.Void -> assert false
+ | _, _, E.Void -> assert false
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 e
in
- Y.name C.err f a
+ E.name C.err f a
let rename f e a =
let rec aux f e n r =
does_not_occur f n r e
in
let f n0 r0 =
- let f n r = if n = n0 && r = r0 then f a else f (Y.Name (n, r) :: a) in
+ let f n r = if n = n0 && r = r0 then f a else f (E.Name (n, r) :: a) in
aux f e n0 r0
in
- Y.name C.err f a
+ E.name C.err f a
(* lenv/term pretty printing ************************************************)
| true -> F.fprintf frm "%s" n
| false -> F.fprintf frm "^%s" n
in
- Y.name err f a
+ E.name err f a
let rec pp_term e frm = function
| B.Sort (_, h) ->
H.string_of_sort err f h
| B.LRef (_, i) ->
let err _ = F.fprintf frm "@[#%u@]" i in
- if !O.indexes then err () else
+ if !G.indexes then err () else
let _, _, a, b = B.get e i in
F.fprintf frm "@[%a@]" (name err) a
| B.GRef (_, s) ->
(* term xml printing ********************************************************)
-let rec exp_term e t out tab = match t with
- | B.Sort (a, l) ->
- let a =
- let err _ = a in
- let f s = Y.Name (s, true) :: a in
- H.string_of_sort err f l
- in
- let attrs = [X.position l; X.name a] in
- X.tag X.sort attrs out tab
- | B.LRef (a, i) ->
- let a =
- let err _ = a in
- let f n r = Y.Name (n, r) :: a in
- let _, _, a, b = B.get e i in
- Y.name err f a
- in
- let attrs = [X.position i; X.name a] in
- X.tag X.lref attrs out tab
- | B.GRef (a, n) ->
- let a = Y.Name (U.name_of_uri n, true) :: a in
- let attrs = [X.uri n; X.name a] in
- X.tag X.gref attrs out tab
- | B.Cast (a, u, t) ->
- let attrs = [] in
- X.tag X.cast attrs ~contents:(exp_term e u) out tab;
- exp_term e t out tab
- | B.Appl (a, v, t) ->
- let attrs = [] in
- X.tag X.appl attrs ~contents:(exp_term e v) out tab;
- exp_term e t out tab
- | B.Bind (a, b, t) ->
- let a = rename C.start e a in
- exp_bind e a b out tab;
- exp_term (B.push e B.empty a b) t out tab
-
-and exp_bind e a b out tab = match b with
- | B.Abst w ->
- let attrs = [X.name a; X.mark a] in
- X.tag X.abst attrs ~contents:(exp_term e w) out tab
- | B.Abbr v ->
- let attrs = [X.name a; X.mark a] in
- X.tag X.abbr attrs ~contents:(exp_term e v) out tab
- | B.Void ->
- let attrs = [X.name a; X.mark a] in
- X.tag X.void attrs out tab
-
-let export_term = exp_term B.empty
+let export_term =
+ BD.crg_of_brg XD.export_term
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module U = NUri
-module C = Cps
-module S = Share
-module L = Log
-module Y = Entity
-module P = Output
-module B = Brg
-module O = BrgOutput
-module E = BrgEnvironment
+module U = NUri
+module C = Cps
+module S = Share
+module L = Log
+module E = Entity
+module O = Output
+module B = Brg
+module BO = BrgOutput
+module BE = BrgEnvironment
type kam = {
e: B.lenv; (* environment *)
let log1 s c t =
let sc, st = s ^ " in the environment", "the term" in
- L.log O.specs level (L.et_items1 sc c st t)
+ L.log BO.specs level (L.et_items1 sc c st t)
let log2 s cu u ct t =
let s1, s2, s3 = s ^ " in the environment", "the term", "and in the environment" in
- L.log O.specs level (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
+ L.log BO.specs level (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
let rec list_and map = function
| hd1 :: tl1, hd2 :: tl2 ->
match x with
| B.Sort _ -> m, None, x
| B.GRef (_, uri) ->
- begin match E.get_entity uri with
- | _, _, Y.Abbr v when st.Y.delta ->
- P.add ~gdelta:1 (); step st m v
- | _, _, Y.Abst w when st.Y.rt ->
- P.add ~grt:1 (); step st m w
- | a, _, Y.Abbr v ->
- let e = Y.apix C.err C.start a in
+ begin match BE.get_entity uri with
+ | _, _, E.Abbr v when st.E.delta ->
+ O.add ~gdelta:1 (); step st m v
+ | _, _, E.Abst w when st.E.rt ->
+ O.add ~grt:1 (); step st m w
+ | a, _, E.Abbr v ->
+ let e = E.apix C.err C.start a in
m, Some (e, a, B.Abbr v), x
- | a, _, Y.Abst w ->
- let e = Y.apix C.err C.start a in
+ | a, _, E.Abst w ->
+ let e = E.apix C.err C.start a in
m, Some (e, a, B.Abst w), x
- | _, _, Y.Void -> assert false
+ | _, _, E.Void -> assert false
end
| B.LRef (_, i) ->
begin match get m i with
| c, _, B.Abbr v ->
- P.add ~ldelta:1 ();
+ O.add ~ldelta:1 ();
step st {m with e = c} v
- | c, _, B.Abst w when st.Y.rt ->
- P.add ~lrt:1 ();
+ | c, _, B.Abst w when st.E.rt ->
+ O.add ~lrt:1 ();
step st {m with e = c} w
| c, _, B.Void ->
assert false
| c, a, (B.Abst _ as b) ->
- let e = Y.apix C.err C.start a in
+ let e = E.apix C.err C.start a in
{m with e = c}, Some (e, a, b), x
end
| B.Cast (_, _, t) ->
- P.add ~tau:1 ();
+ O.add ~tau:1 ();
step st m t
| B.Appl (_, v, t) ->
step st {m with s = (m.e, v) :: m.s} t
begin match m.s with
| [] -> m, None, x
| (c, v) :: s ->
- P.add ~beta:1 ~upsilon:(List.length s) ();
+ 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
| B.Bind (a, b, t) ->
- P.add ~upsilon:(List.length m.s) ();
+ O.add ~upsilon:(List.length m.s) ();
let e = B.push m.e m.e a b in
step st {m with e = e} t
let push m a b =
assert (m.s = []);
let a, d = match b with
- | B.Abst _ -> Y.Apix m.d :: a, succ m.d
+ | B.Abst _ -> E.Apix m.d :: a, succ m.d
| b -> a, m.d
in
let e = B.push m.e m.e a b in
| Some (e1, _, B.Abbr v1), _, Some (e2, _, B.Abbr v2), _ ->
if e1 = e2 then
if ac_stacks st m1 m2 then true else begin
- P.add ~gdelta:2 (); ac st m1 v1 m2 v2
+ O.add ~gdelta:2 (); ac st m1 v1 m2 v2
end
else if e1 < e2 then begin
- P.add ~gdelta:1 ();
+ O.add ~gdelta:1 ();
ac_nfs st (m1, r1, u) (step st m2 v2)
end else begin
- P.add ~gdelta:1 ();
+ O.add ~gdelta:1 ();
ac_nfs st (step st m1 v1) (m2, r2, t)
end
| _, _, Some (_, _, B.Abbr v2), _ ->
- P.add ~gdelta:1 ();
+ O.add ~gdelta:1 ();
ac_nfs st (m1, r1, u) (step st m2 v2)
| Some (_, _, B.Abbr v1), _, _, _ ->
- P.add ~gdelta:1 ();
+ O.add ~gdelta:1 ();
ac_nfs st (step st m1 v1) (m2, r2, t)
| _, B.Bind (a1, (B.Abst w1 as b1), t1),
_, B.Bind (a2, (B.Abst w2 as b2), t2) ->
- if ac {st with Y.si = false} m1 w1 m2 w2 then
+ if ac {st with E.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.Y.si ->
- P.add ~si:1 ();
+ | _, B.Sort _, _, B.Bind (a, b, t) when st.E.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 Y.si = false} m1 v1 m2 v2
+ ac {st with E.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 Y.delta = true; Y.rt = true} m t in
+ let m, _, t = step {st with E.delta = true; E.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 Y.delta = st.Y.expand; Y.rt = false} mu u mw w in
+ let r = ac {st with E.delta = st.E.expand; E.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 () *)
(* error reporting **********************************************************)
-let pp_term m frm t = O.specs.L.pp_term m.e frm t
+let pp_term m frm t = BO.specs.L.pp_term m.e frm t
-let pp_lenv frm m = O.specs.L.pp_lenv frm m.e
+let pp_lenv frm m = BO.specs.L.pp_lenv frm m.e
let specs = {
L.pp_term = pp_term; L.pp_lenv = pp_lenv
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module U = NUri
-module C = Cps
-module A = Share
-module L = Log
-module H = Hierarchy
-module Y = Entity
-module B = Brg
-module O = BrgOutput
-module E = BrgEnvironment
-module S = BrgSubstitution
-module R = BrgReduction
+module U = NUri
+module C = Cps
+module S = Share
+module L = Log
+module H = Hierarchy
+module E = Entity
+module B = Brg
+module BE = BrgEnvironment
+module BS = BrgSubstitution
+module BR = BrgReduction
-type message = (R.kam, B.term) Log.message
+type message = (BR.kam, B.term) Log.message
(* Internal functions *******************************************************)
let log1 s m t =
let s = s ^ " the term" in
- L.log R.specs level (message1 s m t)
+ L.log BR.specs level (message1 s m t)
let error1 err s m t =
err (message1 s m t)
err (message3 m t1 t2 ?mu t3)
let assert_convertibility err f st m u w v =
- if R.are_convertible st m u m w then f () else
+ if BR.are_convertible st m u m w then f () else
error3 err m v w u
let assert_applicability err f st m u w v =
- match R.xwhd st m u with
+ match BR.xwhd st m u with
| _, B.Sort _ -> error1 err "not a function type" m u
| mu, B.Bind (_, B.Abst u, _) ->
- if R.are_convertible st mu u m w then f () else
+ if BR.are_convertible st mu u m w then f () else
error3 err m v w ~mu u
| _ -> assert false (**)
| B.Sort (a, h) ->
let h = H.apply h in f x (B.Sort (a, h))
| B.LRef (_, i) ->
- begin match R.get m i with
+ begin match BR.get m i with
| B.Abst w ->
- f x (S.lift (succ i) (0) w)
+ f x (BS.lift (succ i) (0) w)
| B.Abbr (B.Cast (_, w, _)) ->
- f x (S.lift (succ i) (0) w)
+ f x (BS.lift (succ i) (0) w)
| B.Abbr _ -> assert false
| B.Void ->
error1 err "reference to excluded variable" m x
end
| B.GRef (_, uri) ->
- begin match E.get_entity uri with
- | _, _, Y.Abst w -> f x w
- | _, _, Y.Abbr (B.Cast (_, w, _)) -> f x w
- | _, _, Y.Abbr _ -> assert false
- | _, _, Y.Void ->
+ begin match BE.get_entity uri with
+ | _, _, E.Abst w -> f x w
+ | _, _, E.Abbr (B.Cast (_, w, _)) -> f x w
+ | _, _, E.Abbr _ -> assert false
+ | _, _, E.Void ->
error1 err "reference to unknown entry" m x
end
| B.Bind (a, B.Abbr 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)
+ f (S.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 (R.push m a (B.abbr xv)) in
+ let f xv = f xv (BR.push m a (B.abbr xv)) in
let f xv vv = match xv with
| B.Cast _ -> f xv
| _ -> f (B.Cast ([], vv, xv))
type_of err f st m v
| B.Bind (a, B.Abst u, t) ->
let f xu xt tt =
- f (A.sh2 u xu t xt x (B.bind_abst a)) (B.bind_abst a xu tt)
+ f (S.sh2 u xu t xt x (B.bind_abst a)) (B.bind_abst a xu tt)
in
let f xu m = b_type_of err (f xu) st m t in
- let f xu _ = f xu (R.push m a (B.abst xu)) in
+ let f xu _ = f xu (BR.push m a (B.abst xu)) in
type_of err f st m u
| B.Bind (a, B.Void, t) ->
let f xt tt =
- f (A.sh1 t xt x (B.bind_void a)) (B.bind_void a tt)
+ f (S.sh1 t xt x (B.bind_void a)) (B.bind_void a tt)
in
- b_type_of err f st (R.push m a B.Void) t
+ 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 (A.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt) in
+ let f _ = f (S.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 (A.sh2 u xu t xt x (B.cast a)) xu in
+ let f _ = f (S.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
\ / 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
-module T = BrgType
+module U = NUri
+module L = Log
+module E = Entity
+module B = Brg
+module BE = BrgEnvironment
+module BR = BrgReduction
+module BT = BrgType
(* Interface functions ******************************************************)
(* to share *)
let type_check err f st = function
- | a, uri, Y.Abst t ->
+ | a, uri, E.Abst t ->
let f xt tt =
- let e = E.set_entity (a, uri, Y.Abst xt) in f tt e
+ let e = BE.set_entity (a, uri, E.Abst xt) in f tt e
in
- L.loc := U.string_of_uri uri; T.type_of err f st R.empty_kam t
- | a, uri, Y.Abbr t ->
+ L.loc := U.string_of_uri uri; BT.type_of err f st BR.empty_kam t
+ | a, uri, E.Abbr t ->
let f xt tt =
let xt = match xt with
| B.Cast _ -> xt
| _ -> B.Cast ([], tt, xt)
in
- let e = E.set_entity (a, uri, Y.Abbr xt) in f tt e
+ let e = BE.set_entity (a, uri, E.Abbr xt) in f tt e
in
- L.loc := U.string_of_uri uri; T.type_of err f st R.empty_kam t
- | _, _, Y.Void -> assert false
+ L.loc := U.string_of_uri uri; BT.type_of err f st BR.empty_kam t
+ | _, _, E.Void -> assert false
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module Y = Entity
+module E = Entity
(* internal functions *******************************************************)
let alpha_name acc attr =
let ns, a = acc in
match attr with
- | Y.Name n ->
+ | E.Name n ->
if List.mem n ns then
let n = rename ns n in
- n :: ns, Y.Name n :: a
+ n :: ns, E.Name n :: a
else
n :: ns, attr :: a
| _ -> assert false
let _, names = List.fold_left alpha_name (ns, []) (List.rev names) in
List.rev_append a names
in
- Y.get_names f a
+ E.get_names f a
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module O = Options
+module U = NUri
+module G = Options
+
+type uri = U.uri
+
+type id = string (* identifier *)
-type uri = NUri.uri
-type id = Aut.id
type name = id * bool (* token, real? *)
type names = name list
assert false
let initial_status () = {
- delta = false; rt = false; si = !O.si; expand = !O.expand
+ delta = false; rt = false; si = !G.si; expand = !G.expand
}
let refresh_status st = {st with
- si = !O.si; expand = !O.expand
+ si = !G.si; expand = !G.expand
}
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module H = Hashtbl
-module S = Scanf
+module K = Hashtbl
+module P = Scanf
module C = Cps
type graph = string * (int -> int)
let sorts = 3
-let sort = H.create sorts
+let sort = K.create sorts
let default_graph = "Z1"
(* Internal functions *******************************************************)
let set_sort h s =
- H.add sort h s; succ h
+ K.add sort h s; succ h
let graph_of_string err f s =
try
- let x = S.sscanf s "Z%u" C.start in
+ let x = P.sscanf s "Z%u" C.start in
if x > 0 then f (s, fun h -> x + h) else err ()
with
- S.Scan_failure _ | Failure _ | End_of_file -> err ()
+ P.Scan_failure _ | Failure _ | End_of_file -> err ()
let graph = ref (graph_of_string C.err C.start default_graph)
List.fold_left set_sort i ss
let string_of_sort err f h =
- try f (H.find sort h) with Not_found -> err ()
+ try f (K.find sort h) with Not_found -> err ()
let sort_of_string err f s =
let map h n = function
| None when n = s -> Some h
| xh -> xh
in
- match H.fold map sort None with
+ match K.fold map sort None with
| None -> err ()
| Some h -> f h
graph_of_string err f s
let clear () =
- H.clear sort; graph := graph_of_string C.err C.start default_graph
+ K.clear sort; graph := graph_of_string C.err C.start default_graph
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module Y = Entity
+module E = Entity
(* interface functions ******************************************************)
fun () -> incr location; !location
let new_mark () =
- Y.Mark (new_location ())
+ E.Mark (new_location ())
module P = Printf
module L = Log
-module O = Options
+module G = Options
type reductions = {
beta : int;
L.warn (P.sprintf " Local: %7u" r.lrt);
L.warn (P.sprintf " Global: %7u" r.grt);
L.warn (P.sprintf " Sort inclusion: %7u" r.si);
- L.warn (P.sprintf " Relocated nodes (icm): %7u" !O.icm)
+ L.warn (P.sprintf " Relocated nodes (icm): %7u" !G.icm)
(* kernel version: complete, relative, global *)
(* note : fragment of complete lambda-delta serving as abstract layer *)
-module Y = Entity
+module E = Entity
-type uri = Y.uri
-type id = Y.id
-type attrs = Y.attrs
+type uri = E.uri
+type id = E.id
+type attrs = E.attrs
type bind = Abst of term list (* domains *)
| Abbr of term list (* bodies *)
| EProj of lenv * attrs * lenv (* environment, attrs, closure *)
| EBind of lenv * attrs * bind (* environment, attrs, binder *)
-type entity = term Y.entity
+type entity = term E.entity
(* helpers ******************************************************************)
let resolve_lref err f id lenv =
let rec aux f i k = function
| ESort -> err ()
+ | EBind (tl, _, Abst [])
+ | EBind (tl, _, Abbr [])
+ | EBind (tl, _, Void 0) -> aux f i k tl
| EBind (tl, a, _) ->
let err kk = aux f (succ i) (k + kk) tl in
let f j = f i j (k + j) in
- Y.resolve err f id a
+ E.resolve err f id a
| EProj _ -> assert false (* TODO *)
in
aux f 0 0 lenv
let rec get_name err f i j = function
| ESort -> err i
+ | EBind (tl, _, Abst [])
+ | EBind (tl, _, Abbr [])
+ | EBind (tl, _, Void 0) -> get_name err f i j tl
| EBind (_, a, _) when i = 0 ->
let err () = err i in
- Y.get_name err f j a
+ E.get_name err f j a
| EBind (tl, _, _) ->
get_name err f (pred i) j tl
| EProj (tl, _, e) ->
let get_index err f i j lenv =
let rec aux f i k = function
| ESort -> err i
+ | EBind (tl, _, Abst [])
+ | EBind (tl, _, Abbr [])
+ | EBind (tl, _, Void 0) -> aux f i k tl
| EBind (_, a, _) when i = 0 ->
- if Y.count_names a > j then f (k + j) else err i
+ if E.count_names a > j then f (k + j) else err i
| EBind (tl, a, _) ->
- aux f (pred i) (k + Y.count_names a) tl
+ aux f (pred i) (k + E.count_names a) tl
| EProj _ -> assert false (* TODO *)
in
aux f i 0 lenv
let rec names_of_lenv ns = function
| ESort -> ns
- | EBind (tl, a, _) -> names_of_lenv (Y.rev_append_names ns a) tl
+ | EBind (tl, a, _) -> names_of_lenv (E.rev_append_names ns a) tl
| EProj (tl, _, e) -> names_of_lenv (names_of_lenv ns e) tl
V_______________________________________________________________ *)
module U = NUri
-module H = U.UriHash
+module K = U.UriHash
module C = Cps
-module O = Options
-module Y = Entity
+module G = Options
+module E = Entity
module A = Aut
module D = Crg
(* qualified identifier: uri, name, qualifiers *)
type qid = D.uri * D.id * D.id list
-type context = Y.attrs * D.term list
+type context = E.attrs * D.term list
type context_node = qid option (* context node: None = root *)
node: context_node; (* current context node *)
nodes: context_node list; (* context node list *)
line: int; (* line number *)
- mk_uri:O.uri_generator (* uri generator *)
+ mk_uri:G.uri_generator (* uri generator *)
}
type resolver = Local of int
let henv_size, hcnt_size = 7000, 4300 (* hash tables initial sizes *)
-let henv = H.create henv_size (* optimized global environment *)
+let henv = K.create henv_size (* optimized global environment *)
-let hcnt = H.create hcnt_size (* optimized context *)
+let hcnt = K.create hcnt_size (* optimized context *)
(* Internal functions *******************************************************)
let empty_cnt = [], []
let add_abst (a, ws) id w =
- Y.Name (id, true) :: a, w :: ws
+ E.Name (id, true) :: a, w :: ws
let lenv_of_cnt (a, ws) =
D.push_bind C.start D.empty_lenv a (D.Abst ws)
-let mk_lref f i j k = f (D.TLRef ([Y.Apix k], i, j))
+let mk_lref f i j k = f (D.TLRef ([E.Apix k], i, j))
let id_of_name (id, _, _) = id
| Some qid -> let f qid = f (Some qid) in relax_qid f st qid
let resolve_gref err f st qid =
- try let cnt = H.find henv (uri_of_qid qid) in f qid cnt
+ try let cnt = K.find henv (uri_of_qid qid) in f qid cnt
with Not_found -> err qid
let resolve_gref_relaxed f st qid =
let get_cnt err f st = function
| None -> f empty_cnt
| Some qid as node ->
- try let cnt = H.find hcnt (uri_of_qid qid) in f cnt
+ try let cnt = K.find hcnt (uri_of_qid qid) in f cnt
with Not_found -> err node
let get_cnt_relaxed f st =
xlate_term f st lenv v
| A.Abst (name, w, t) ->
let f ww =
- let a, b = [Y.Name (name, true)], (D.Abst [ww]) in
+ let a, b = [E.Name (name, true)], (D.Abst [ww]) in
let f tt = f (D.TBind (a, b, tt)) in
let f lenv = xlate_term f st lenv t in
D.push_bind f lenv a b
xlate_term f st lenv w
| A.GRef (name, args) ->
let map1 f = function
- | Y.Name (id, _) -> f (A.GRef ((id, true, []), []))
+ | E.Name (id, _) -> f (A.GRef ((id, true, []), []))
| _ -> C.err ()
in
let map2 f = xlate_term f st lenv in
let f cnt =
let lenv = lenv_of_cnt cnt in
let ww = xlate_term C.start st lenv w in
- H.add hcnt (uri_of_qid qid) (add_abst cnt name ww);
+ K.add hcnt (uri_of_qid qid) (add_abst cnt name ww);
err {st with node = Some qid}
in
get_cnt_relaxed f st
let lenv = lenv_of_cnt cnt in
let f qid =
let ww = xlate_term C.start st lenv w in
- H.add henv (uri_of_qid qid) cnt;
+ K.add henv (uri_of_qid qid) cnt;
let t = match ws with
| [] -> ww
| _ -> D.TBind (a, D.Abst ws, ww)
(*
print_newline (); CrgOutput.pp_term print_string t;
*)
- let b = Y.Abst t in
- let entity = [Y.Mark st.line], uri_of_qid qid, b in
+ let b = E.Abst t in
+ let entity = [E.Mark st.line], uri_of_qid qid, b in
f {st with line = succ st.line} entity
in
complete_qid f st (name, true, [])
let f qid =
let ww = xlate_term C.start st lenv w in
let vv = xlate_term C.start st lenv v in
- H.add henv (uri_of_qid qid) cnt;
+ K.add henv (uri_of_qid qid) cnt;
let t = match ws with
| [] -> D.TCast ([], ww, vv)
| _ -> D.TBind (a, D.Abst ws, D.TCast ([], ww, vv))
(*
print_newline (); CrgOutput.pp_term print_string t;
*)
- let b = Y.Abbr t in
- let a = Y.Mark st.line :: if trans then [] else [Y.Priv] in
+ let b = E.Abbr t in
+ let a = E.Mark st.line :: if trans then [] else [E.Priv] in
let entity = a, uri_of_qid qid, b in
f {st with line = succ st.line} entity
in
(* Interface functions ******************************************************)
let initial_status () =
- H.clear henv; H.clear hcnt; {
- path = []; node = None; nodes = []; line = 1; mk_uri = O.get_mk_uri ()
+ K.clear henv; K.clear hcnt; {
+ path = []; node = None; nodes = []; line = 1; mk_uri = G.get_mk_uri ()
}
let refresh_status st = {st with
- mk_uri = O.get_mk_uri ()
+ mk_uri = G.get_mk_uri ()
}
let crg_of_aut = xlate_entity
module U = NUri
module C = Cps
module H = Hierarchy
-module Y = Entity
+module E = Entity
module D = Crg
(****************************************************************************)
let pp_attrs out a =
let map = function
- | Y.Name (s, true) -> out (P.sprintf "%s;" s)
- | Y.Name (s, false) -> out (P.sprintf "~%s;" s)
- | Y.Apix i -> out (P.sprintf "+%i;" i)
- | Y.Mark i -> out (P.sprintf "@%i;" i)
- | Y.Meta s -> out (P.sprintf "\"%s\";" s)
- | Y.Priv -> out (P.sprintf "%s;" "~")
+ | E.Name (s, true) -> out (P.sprintf "%s;" s)
+ | E.Name (s, false) -> out (P.sprintf "~%s;" s)
+ | E.Apix i -> out (P.sprintf "+%i;" i)
+ | E.Mark i -> out (P.sprintf "@%i;" i)
+ | E.Meta s -> out (P.sprintf "\"%s\";" s)
+ | E.Priv -> out (P.sprintf "%s;" "~")
in
List.iter map a
module U = NUri
module H = Hierarchy
module C = Cps
-module O = Options
-module Y = Entity
+module G = Options
+module E = Entity
module T = Txt
module TT = TxtTxt
module D = Crg
path : T.id list; (* current section path *)
line : int; (* line number *)
sort : int; (* first default sort index *)
- mk_uri: O.uri_generator (* uri generator *)
+ mk_uri: G.uri_generator (* uri generator *)
}
let henv_size = 7000 (* hash tables initial size *)
(* Internal functions *******************************************************)
-let name_of_id ?(r=true) id = Y.Name (id, r)
+let name_of_id ?(r=true) id = E.Name (id, r)
-let mk_lref f i j k = f (D.TLRef ([Y.Apix k], i, j))
+let mk_lref f i j k = f (D.TLRef ([E.Apix k], i, j))
let mk_gref f uri = f (D.TGRef ([], uri))
TT.contract (xlate_term f st lenv) t
let mk_contents tt = function
- | T.Decl -> [], Y.Abst tt
- | T.Ax -> [], Y.Abst tt
- | T.Def -> [], Y.Abbr tt
- | T.Th -> [], Y.Abbr tt
+ | T.Decl -> [], E.Abst tt
+ | T.Ax -> [], E.Abst tt
+ | T.Def -> [], E.Abbr tt
+ | T.Th -> [], E.Abbr tt
let xlate_entity err f gen st = function
| T.Require _ ->
print_newline (); CrgOutput.pp_term print_string tt;
*)
let a, b = mk_contents tt kind in
- let a = if meta <> "" then Y.Meta meta :: a else a in
- let entity = Y.Mark st.line :: a, uri, b in
+ let a = if meta <> "" then E.Meta meta :: a else a in
+ let entity = E.Mark st.line :: a, uri, b in
f {st with line = succ st.line} entity
| T.Generate _ ->
err st
let initial_status () =
Hashtbl.clear henv; {
- path = []; line = 1; sort = 0; mk_uri = O.get_mk_uri ()
+ path = []; line = 1; sort = 0; mk_uri = G.get_mk_uri ()
}
let refresh_status st = {st with
- mk_uri = O.get_mk_uri ()
+ mk_uri = G.get_mk_uri ()
}
let crg_of_txt = xlate_entity
--- /dev/null
+(* free = F I N P Q U V W *)
+
+module U = NUri
+module K = NUri.UriHash
+
+module C = cps
+module S = share
+module L = log
+module Y = time (**)
+
+module G = options
+module H = hierarchy
+module O = output
+module E = entity
+module J = marks (**)
+module R = alpha
+
+module T = txt
+module TP = txtParser
+module TL = txtLexer
+module TT = txtTxt
+
+module A = aut
+module AA = autProcess
+module AO = autOutput
+module AP = autParser
+module AL = autLexer
+
+module Z = bag
+module ZO = bagOutput
+module ZE = bagEnvironment
+module ZS = bagSubstitution
+module ZR = bagReduction
+module ZT = bagType
+module ZU = bagUntrusted
+
+module D = crg
+module DO = crgOutput
+module TD = crgTxt
+module AD = crgAut
+
+module XL = xmlLibrary
+module XD = xmlCrg
+
+module B = brg
+module BD = brgCrg
+module BO = brgOutput
+module BE = brgEnvironment
+module BS = brgSubstitution
+module BR = brgReduction
+module BT = brgType
+module BU = brgUntrusted
+
+module M = meta
+module MO = metaOutput
+module ML = metaLibrary
+module MA = metaAut
+module MZ = metaBag
+module MB = metaBrg
+(*
+ top
+*)
| Section of id option (* section: Some id = open, None = close last *)
| Entity of kind * id * desc * term (* entity: class, name, description, contents *)
| Generate of term list (* predefined generated entity: arguments *)
-
V_______________________________________________________________ *)
{
- module L = Log
- module O = Options
- module P = TxtParser
+ module L = Log
+ module G = Options
+ module TP = TxtParser
- let out s = if !O.debug_lexer then L.warn s else ()
+ let out s = if !G.debug_lexer then L.warn s else ()
}
let BS = "\\"
| BS QT { "\"" ^ qstring lexbuf }
| _ as c { String.make 1 c ^ qstring lexbuf }
and token = parse
- | SPC { token lexbuf }
- | OC { block_comment lexbuf; token lexbuf }
- | ID as id { out ("ID " ^ id); P.ID id }
- | IX as ix { out ("IX " ^ ix); P.IX (int_of_string ix) }
- | QT { let s = qstring lexbuf in out ("STR " ^ s); P.STR s }
- | "\\graph" { out "GRAPH"; P.GRAPH }
- | "\\decl" { out "DECL"; P.DECL }
- | "\\ax" { out "AX"; P.AX }
- | "\\def" { out "DEF"; P.DEF }
- | "\\th" { out "TH"; P.TH }
- | "\\generate" { out "GEN"; P.GEN }
- | "\\require" { out "REQ"; P.REQ }
- | "\\open" { out "OPEN"; P.OPEN }
- | "\\close" { out "CLOSE"; P.CLOSE }
- | "\\sorts" { out "SORTS"; P.SORTS }
- | "(" { out "OP"; P.OP }
- | ")" { out "CP"; P.CP }
- | "[" { out "OB"; P.OB }
- | "]" { out "CB"; P.CB }
- | "<" { out "OA"; P.OA }
- | ">" { out "CA"; P.CA }
- | "." { out "FS"; P.FS }
- | ":" { out "CN"; P.CN }
- | "," { out "CM"; P.CM }
- | "=" { out "EQ"; P.EQ }
- | "*" { out "STAR"; P.STAR }
- | "#" { out "HASH"; P.HASH }
- | "+" { out "PLUS"; P.PLUS }
- | "~" { out "TE"; P.TE }
- | "->" { out "WTO"; P.WTO }
- | "=>" { out "STO"; P.STO }
- | eof { out "EOF"; P.EOF }
+ | SPC { token lexbuf }
+ | OC { block_comment lexbuf; token lexbuf }
+ | ID as id { out ("ID " ^ id); TP.ID id }
+ | IX as ix { out ("IX " ^ ix); TP.IX (int_of_string ix) }
+ | QT { let s = qstring lexbuf in out ("STR " ^ s); TP.STR s }
+ | "\\graph" { out "GRAPH"; TP.GRAPH }
+ | "\\decl" { out "DECL"; TP.DECL }
+ | "\\ax" { out "AX"; TP.AX }
+ | "\\def" { out "DEF"; TP.DEF }
+ | "\\th" { out "TH"; TP.TH }
+ | "\\generate" { out "GEN"; TP.GEN }
+ | "\\require" { out "REQ"; TP.REQ }
+ | "\\open" { out "OPEN"; TP.OPEN }
+ | "\\close" { out "CLOSE"; TP.CLOSE }
+ | "\\sorts" { out "SORTS"; TP.SORTS }
+ | "(" { out "OP"; TP.OP }
+ | ")" { out "CP"; TP.CP }
+ | "[" { out "OB"; TP.OB }
+ | "]" { out "CB"; TP.CB }
+ | "<" { out "OA"; TP.OA }
+ | ">" { out "CA"; TP.CA }
+ | "." { out "FS"; TP.FS }
+ | ":" { out "CN"; TP.CN }
+ | "," { out "CM"; TP.CM }
+ | "=" { out "EQ"; TP.EQ }
+ | "*" { out "STAR"; TP.STAR }
+ | "#" { out "HASH"; TP.HASH }
+ | "+" { out "PLUS"; TP.PLUS }
+ | "~" { out "TE"; TP.TE }
+ | "->" { out "WTO"; TP.WTO }
+ | "=>" { out "STO"; TP.STO }
+ | eof { out "EOF"; TP.EOF }
*/
%{
- module O = Options
+ module G = Options
module T = Txt
- let _ = Parsing.set_trace !O.debug_parser
+ let _ = Parsing.set_trace !G.debug_parser
%}
%token <int> IX
%token <string> ID STR
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-type uri = Entity.uri
-type id = Entity.id
+module E = Entity
+
+type uri = E.uri
+type id = E.id
type term = Sort of bool (* sorts: true = TYPE, false = PROP *)
| LRef of int * int (* local reference: local environment length, de bruijn index *)
type entry = pars * term * term option (* parameters, domain, body *)
-type entity = entry Entity.entity
+type entity = entry E.entity
V_______________________________________________________________ *)
module U = NUri
-module H = U.UriHash
+module K = U.UriHash
module C = Cps
-module O = Options
-module Y = Entity
+module G = Options
+module E = Entity
module M = Meta
module A = Aut
let henv_size, hcnt_size = 7000, 4300 (* hash tables initial sizes *)
-let henv = H.create henv_size (* optimized global environment *)
+let henv = K.create henv_size (* optimized global environment *)
-let hcnt = H.create hcnt_size (* optimized context *)
+let hcnt = K.create hcnt_size (* optimized context *)
(* Internal functions *******************************************************)
resolve_lref f st l lenv id
let resolve_gref f st qid =
- try let args = H.find henv (uri_of_qid qid) in f qid (Some args)
+ try let args = K.find henv (uri_of_qid qid) in f qid (Some args)
with Not_found -> f qid None
let resolve_gref_relaxed f st qid =
let get_pars f st = function
| None -> f [] None
| Some qid as node ->
- try let pars = H.find hcnt (uri_of_qid qid) in f pars None
+ try let pars = K.find hcnt (uri_of_qid qid) in f pars None
with Not_found -> f [] (Some node)
let get_pars_relaxed f st =
let f qid =
let f pars =
let f ww =
- H.add hcnt (uri_of_qid qid) ((name, ww) :: pars);
+ K.add hcnt (uri_of_qid qid) ((name, ww) :: pars);
err {st with node = Some qid}
in
xlate_term f st pars w
let f pars =
let f qid =
let f ww =
- H.add henv (uri_of_qid qid) pars;
- let a = [Y.Mark st.line] in
+ K.add henv (uri_of_qid qid) pars;
+ let a = [E.Mark st.line] in
let entry = pars, ww, None in
- let entity = a, uri_of_qid qid, Y.Abst entry in
+ let entity = a, uri_of_qid qid, E.Abst entry in
f {st with line = succ st.line} entity
in
xlate_term f st pars w
let f pars =
let f qid =
let f ww vv =
- H.add henv (uri_of_qid qid) pars;
- let a = Y.Mark st.line :: if trans then [] else [Y.Priv] in
+ K.add henv (uri_of_qid qid) pars;
+ let a = E.Mark st.line :: if trans then [] else [E.Priv] in
let entry = pars, ww, Some vv in
- let entity = a, uri_of_qid qid, Y.Abbr entry in
+ let entity = a, uri_of_qid qid, E.Abbr entry in
f {st with line = succ st.line} entity
in
let f ww = xlate_term (f ww) st pars v in
(* Interface functions ******************************************************)
let initial_status () =
- H.clear henv; H.clear hcnt; {
- path = []; node = None; nodes = []; line = 1; cover = !O.cover
+ K.clear henv; K.clear hcnt; {
+ path = []; node = None; nodes = []; line = 1; cover = !G.cover
}
let refresh_status st = {st with
- cover = !O.cover
+ cover = !G.cover
}
let meta_of_aut = xlate_entity
V_______________________________________________________________ *)
module C = Cps
-module B = Bag
+module Z = Bag
module M = Meta
(* Internal functions *******************************************************)
let rec xlate_term c f = function
| M.Sort s ->
- let f h = f (B.Sort h) in
+ let f h = f (Z.Sort h) in
if s then f 0 else f 1
| M.LRef (_, i) ->
let l, _, _ = List.nth c i in
- f (B.LRef l)
+ f (Z.LRef l)
| M.GRef (_, uri, vs) ->
- let map f t v = f (B.appl v t) in
- let f vs = C.list_fold_left f map (B.GRef uri) vs in
+ let map f t v = f (Z.appl v t) in
+ let f vs = C.list_fold_left f map (Z.GRef uri) vs in
C.list_map f (xlate_term c) vs
| M.Appl (v, t) ->
- let f v t = f (B.Appl (v, t)) in
+ let f v t = f (Z.Appl (v, t)) in
let f v = xlate_term c (f v) t in
xlate_term c f v
| M.Abst (id, w, t) ->
let f w =
- let l = B.new_location () in
- let f t = f (B.Bind (l, id, B.Abst w, t)) in
+ let l = Z.new_location () in
+ let f t = f (Z.Bind (l, id, Z.Abst w, t)) in
let f c = xlate_term c f t in
- B.push "meta" f c l id (B.Abst w)
+ Z.push "meta" f c l id (Z.Abst w)
in
xlate_term c f w
let xlate_pars f pars =
let map f (id, w) c =
- let l = B.new_location () in
- let f w = B.push "meta" f c l id (B.Abst w) in
+ let l = Z.new_location () in
+ let f w = Z.push "meta" f c l id (Z.Abst w) in
xlate_term c f w
in
- C.list_fold_right f map pars B.empty_lenv
+ C.list_fold_right f map pars Z.empty_lenv
let unwind_to_xlate_term f c t =
- let map f t (l, id, b) = f (B.bind l id b t) in
+ let map f t (l, id, b) = f (Z.bind l id b t) in
let f t = C.list_fold_left f map t c in
xlate_term c f t
let f c = unwind_to_xlate_term f c u in
xlate_pars f pars
| pars, u, Some t ->
- let f u t = f (B.Cast (u, t)) in
+ let f u t = f (Z.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
V_______________________________________________________________ *)
module C = Cps
-module Y = Entity
+module E = Entity
module B = Brg
module M = Meta
xlate_term c f v
| M.Abst (id, w, t) ->
let f w =
- let a = [Y.Name (id, true)] in
+ let a = [E.Name (id, true)] in
let f t = f (B.Bind (a, B.Abst w, t)) in
xlate_term (B.push c B.empty a (B.Abst w)) f t
in
let xlate_pars f pars =
let map f (id, w) c =
- let a = [Y.Name (id, true)] in
+ let a = [E.Name (id, true)] in
let f w = f (B.push c B.empty a (B.Abst w)) in
xlate_term c f w
in
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module F = Format
-module O = MetaOutput
+module F = Format
+module MO = MetaOutput
type out_channel = Pervasives.out_channel * F.formatter
f (och, frm)
let write_entity f (_, frm) entity =
- O.pp_entity f frm entity
+ MO.pp_entity f frm entity
let close_out f (och, _) =
close_out och; f ()
module U = NUri
module C = Cps
module L = Log
-module Y = Entity
+module E = Entity
module M = Meta
type counters = {
| Some v -> count_term f c v
let count_entity f c = function
- | _, u, Y.Abst (pars, w, xv) ->
+ | _, u, E.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
- | _, _, Y.Abbr (pars, w, xv) ->
+ | _, _, E.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_xterm f c xv in
let f c = count_term f c w in
Cps.list_fold_left f count_par c pars
- | _, _, Y.Void -> assert false
+ | _, _, E.Void -> assert false
let print_counters f c =
let terms = c.tsorts + c.tlrefs + c.tgrefs + c.tappls + c.tabsts in
let pp_transparent frm a =
let err () = F.fprintf frm "%s" "=" in
let f () = F.fprintf frm "%s" "~" in
- Y.priv err f a
+ E.priv err f a
let pp_list pp opend sep closed frm l =
let rec aux frm = function
| Some t -> F.fprintf frm "%a%a" pp_transparent a pp_term t
let pp_entity frm = function
- | a, uri, Y.Abst (pars, u, body)
- | a, uri, Y.Abbr (pars, u, body) ->
+ | a, uri, E.Abst (pars, u, body)
+ | a, uri, E.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)
+ (E.mark C.err C.start a) (U.string_of_uri uri)
pp_pars pars (pp_body a) body pp_term u
- | _, _, Y.Void -> assert false
+ | _, _, E.Void -> assert false
let pp_entity f frm entity =
pp_entity frm entity; f ()
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module F = Filename
-module P = Printf
-module U = NUri
-module C = Cps
-module L = Log
-module T = Time
-module O = Options
-module H = Hierarchy
-module Op = Output
-module Y = Entity
-module XL = XmlLibrary
-module XCrg = XmlCrg
-module AL = AutLexer
-module AP = AutProcess
-module AO = AutOutput
-module DT = CrgTxt
-module DA = CrgAut
-module MA = MetaAut
-module MO = MetaOutput
-module ML = MetaLibrary
-module MBrg = MetaBrg
-module BrgC = BrgCrg
-module BrgO = BrgOutput
-module BrgR = BrgReduction
-module BrgU = BrgUntrusted
-module MBag = MetaBag
-module BagO = BagOutput
-module BagT = BagType
-module BagU = BagUntrusted
+module F = Filename
+module P = Printf
+module U = NUri
+module C = Cps
+module L = Log
+module Y = Time
+module G = Options
+module H = Hierarchy
+module O = Output
+module E = Entity
+module XL = XmlLibrary
+module XD = XmlCrg
+module AA = AutProcess
+module AO = AutOutput
+module TD = CrgTxt
+module AD = CrgAut
+module MA = MetaAut
+module MO = MetaOutput
+module ML = MetaLibrary
+module MB = MetaBrg
+module BD = BrgCrg
+module BO = BrgOutput
+module BR = BrgReduction
+module BU = BrgUntrusted
+module MZ = MetaBag
+module ZO = BagOutput
+module ZT = BagType
+module ZU = BagUntrusted
type status = {
- ast : AP.status;
- dst : DA.status;
+ ast : AA.status;
+ dst : AD.status;
mst : MA.status;
- tst : DT.status;
+ tst : TD.status;
ac : AO.counters;
mc : MO.counters;
- brgc: BrgO.counters;
- bagc: BagO.counters;
- kst : Y.status
+ brgc: BO.counters;
+ bagc: ZO.counters;
+ kst : E.status
}
let flush_all () = L.flush 0; L.flush_err ()
let bag_error s msg =
- L.error BagO.specs (L.Warn s :: L.Loc :: msg); flush_all ()
+ L.error ZO.specs (L.Warn s :: L.Loc :: msg); flush_all ()
let brg_error s msg =
- L.error BrgR.specs (L.Warn s :: L.Loc :: msg); flush_all ()
+ L.error BR.specs (L.Warn s :: L.Loc :: msg); flush_all ()
let initial_status () = {
ac = AO.initial_counters;
mc = MO.initial_counters;
- brgc = BrgO.initial_counters;
- bagc = BagO.initial_counters;
+ brgc = BO.initial_counters;
+ bagc = ZO.initial_counters;
mst = MA.initial_status ();
- dst = DA.initial_status ();
- tst = DT.initial_status ();
- ast = AP.initial_status ();
- kst = Y.initial_status ()
+ dst = AD.initial_status ();
+ tst = TD.initial_status ();
+ ast = AA.initial_status ();
+ kst = E.initial_status ()
}
let refresh_status st = {st with
mst = MA.refresh_status st.mst;
- dst = DA.refresh_status st.dst;
- tst = DT.refresh_status st.tst;
- kst = Y.refresh_status st.kst
+ dst = AD.refresh_status st.dst;
+ tst = TD.refresh_status st.tst;
+ kst = E.refresh_status st.kst
}
(* kernel related ***********************************************************)
let kernel = ref Brg
let print_counters st = match !kernel with
- | Brg -> BrgO.print_counters C.start st.brgc
- | Bag -> BagO.print_counters C.start st.bagc
+ | Brg -> BO.print_counters C.start st.brgc
+ | Bag -> ZO.print_counters C.start st.bagc
let xlate_entity entity = match !kernel, entity with
| Brg, CrgEntity e ->
- let f e = (BrgEntity e) in Y.xlate f BrgC.brg_of_crg e
+ let f e = (BrgEntity e) in E.xlate f BD.brg_of_crg e
| Brg, MetaEntity e ->
- let f e = (BrgEntity e) in Y.xlate f MBrg.brg_of_meta e
+ let f e = (BrgEntity e) in E.xlate f MB.brg_of_meta e
| Bag, MetaEntity e ->
- let f e = (BagEntity e) in Y.xlate f MBag.bag_of_meta e
+ let f e = (BagEntity e) in E.xlate f MZ.bag_of_meta e
| _, entity -> entity
let pp_progress e =
let s = U.string_of_uri u in
let err () = L.warn (P.sprintf "%s" s) in
let f i = L.warn (P.sprintf "[%u] %s" i s) in
- Y.mark err f a
+ E.mark err f a
in
match e with
- | CrgEntity e -> Y.common f e
- | BrgEntity e -> Y.common f e
- | BagEntity e -> Y.common f e
- | MetaEntity e -> Y.common f e
+ | CrgEntity e -> E.common f e
+ | BrgEntity e -> E.common f e
+ | BagEntity e -> E.common f e
+ | MetaEntity e -> E.common f e
let count_entity st = function
| MetaEntity e -> {st with mc = MO.count_entity C.start st.mc e}
- | BrgEntity e -> {st with brgc = BrgO.count_entity C.start st.brgc e}
- | BagEntity e -> {st with bagc = BagO.count_entity C.start st.bagc e}
+ | BrgEntity e -> {st with brgc = BO.count_entity C.start st.brgc e}
+ | BagEntity e -> {st with bagc = ZO.count_entity C.start st.bagc e}
| _ -> st
let export_entity si xdir moch = function
- | CrgEntity e -> XL.export_entity XCrg.export_term si xdir e
- | BrgEntity e -> XL.export_entity BrgO.export_term si xdir e
+ | CrgEntity e -> XL.export_entity XD.export_term si xdir e
+ | BrgEntity e -> XL.export_entity BO.export_term si xdir e
| MetaEntity e ->
begin match moch with
| None -> ()
let brg_err msg = brg_error "Type Error" msg; failwith "Interrupted" in
let ok _ _ = st in
match k with
- | BrgEntity entity -> BrgU.type_check brg_err ok st.kst entity
- | BagEntity entity -> BagU.type_check ok st.kst entity
+ | BrgEntity entity -> BU.type_check brg_err ok st.kst entity
+ | BagEntity entity -> ZU.type_check ok st.kst entity
| CrgEntity _
| MetaEntity _ -> st
let process_input f st = function
| AutEntity e ->
let f ast e = f {st with ast = ast} (AutEntity e) in
- AP.process_command f st.ast e
+ AA.process_command f st.ast e
| xe -> f st xe
let count_input st = function
let process_2 st entity =
let st = if !L.level > 2 then count_entity st entity else st in
- if !export <> "" then export_entity !O.si !export !moch entity;
+ if !export <> "" then export_entity !G.si !export !moch 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 !O.si !export !moch entity;
+ if !export <> "" && !stage = 1 then export_entity !G.si !export !moch entity;
if !stage > 1 then process_2 st (xlate_entity entity) else st
let process_0 st entity =
| AutEntity e, false ->
let err dst = {st with dst = dst} in
let g dst e = process_1 {st with dst = dst} (CrgEntity e) in
- DA.crg_of_aut err g st.dst e
+ AD.crg_of_aut err g st.dst e
| TxtEntity e, _ ->
let crr tst = {st with tst = tst} in
let d tst e = process_1 {st with tst = tst} (CrgEntity e) in
- DT.crg_of_txt crr d gen_text st.tst e
+ TD.crg_of_txt crr d gen_text st.tst e
| NoEntity, _ -> assert false
in
let st = if !L.level > 2 then count_input st entity else st in
stage := 3; moch := None; meta := false; progress := false;
preprocess := false; root := ""; cc := false; export := "";
old := false; kernel := Brg; st := initial_status ();
- L.clear (); O.clear (); H.clear (); Op.clear_reductions ();
+ L.clear (); G.clear (); H.clear (); O.clear_reductions ();
streaming := false;
in
let process_file name =
- if !L.level > 0 then T.gmtime version_string;
+ if !L.level > 0 then Y.gmtime version_string;
if !L.level > 1 then
L.warn (P.sprintf "Processing file: %s" name);
- if !L.level > 0 then T.utime_stamp "started";
+ if !L.level > 0 then Y.utime_stamp "started";
let base_name = Filename.chop_extension (Filename.basename name) in
if !meta then set_meta_file base_name;
let mk_uri =
| Bag -> Bag.mk_uri
in
let cover = F.concat !root base_name in
- O.mk_uri := mk_uri; O.cover := cover;
+ G.mk_uri := mk_uri; G.cover := cover;
let sst, input = process (refresh_status !st) name in
st := sst;
- if !L.level > 0 then T.utime_stamp "processed";
+ if !L.level > 0 then Y.utime_stamp "processed";
if !L.level > 2 then begin
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 > 2 then Op.print_reductions ()
+ if !stage > 2 then O.print_reductions ()
end
in
let exit () =
close !moch;
- if !L.level > 0 then T.utime_stamp "at exit";
+ if !L.level > 0 then Y.utime_stamp "at exit";
flush_all ()
in
let help =
L.box 0; L.box_err ();
at_exit exit;
Arg.parse [
- ("-L", Arg.Set O.debug_lexer, help_L);
- ("-P", Arg.Set O.debug_parser, help_P);
+ ("-L", Arg.Set G.debug_lexer, help_L);
+ ("-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);
- ("-g", Arg.Set O.expand, help_g);
+ ("-g", Arg.Set G.expand, help_g);
("-h", Arg.String set_hierarchy, help_h);
- ("-i", Arg.Set O.indexes, help_i);
+ ("-i", Arg.Set G.indexes, help_i);
("-j", Arg.Set progress, help_j);
("-k", Arg.String set_kernel, help_k);
("-m", Arg.Set meta, help_m);
("-o", Arg.Set old, help_o);
("-p", Arg.Set preprocess, help_p);
- ("-q", Arg.Set O.unquote, help_q);
+ ("-q", Arg.Set G.unquote, help_q);
("-r", Arg.String set_root, help_r);
("-s", Arg.Int set_stage, help_s);
- ("-u", Arg.Set O.si, help_u);
+ ("-u", Arg.Set G.si, help_u);
("-x", Arg.String set_xdir, help_x);
("-1", Arg.Set streaming, help_1);
] process_file help;
-with BagT.TypeError msg -> bag_error "Type Error" msg
+with ZT.TypeError msg -> bag_error "Type Error" msg
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module U = NUri
-module C = Cps
-module H = Hierarchy
-module Y = Entity
-module A = Alpha
-module X = XmlLibrary
-module D = Crg
+module U = NUri
+module C = Cps
+module H = Hierarchy
+module Y = Entity
+module R = Alpha
+module XL = XmlLibrary
+module D = Crg
(* internal functions *******************************************************)
let f s = Y.Name (s, true) :: a in
H.string_of_sort err f l
in
- let attrs = [X.position l; X.name a] in
- X.tag X.sort attrs out tab
+ let attrs = [XL.position l; XL.name a] in
+ XL.tag XL.sort attrs out tab
| D.TLRef (a, i, j) ->
let a =
let err _ = a in
let f n r = Y.Name (n, r) :: a in
D.get_name err f i j e
in
- let attrs = [X.position i; X.offset j; X.name a] in
- X.tag X.lref attrs out tab
+ let attrs = [XL.position i; XL.offset j; XL.name a] in
+ XL.tag XL.lref attrs out tab
| D.TGRef (a, n) ->
let a = Y.Name (U.name_of_uri n, true) :: a in
- let attrs = [X.uri n; X.name a] in
- X.tag X.gref attrs out tab
+ let attrs = [XL.uri n; XL.name a] in
+ XL.tag XL.gref attrs out tab
| D.TCast (a, u, t) ->
let attrs = [] in
- X.tag X.cast attrs ~contents:(exp_term e u) out tab;
+ 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 = [X.arity (List.length vs)] in
- X.tag X.appl attrs ~contents:(list_iter (exp_term e) vs) out tab;
+ let attrs = [XL.arity (List.length 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) ->
let attrs = [] in
- X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab;
+ XL.tag XL.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab;
exp_term (D.push_proj C.start e a lenv) t out tab
| D.TBind (a, b, t) ->
(* NOTE: the inner binders are alpha-converted first *)
-(* so undesirable renamings might occur *)
-(* EX: we rename [x][x]x to [x][x_]x_ *)
-(* whereas [x_][x]x would be more desirable *)
- let a = A.alpha (D.names_of_lenv [] e) a in
+ let a = R.alpha (D.names_of_lenv [] e) a in
exp_bind e a b out tab;
exp_term (D.push_bind C.start e a b) t out tab
match b with
| D.Abst ws ->
let e = D.push_bind C.start e a (D.Abst []) in
- let attrs = [X.name ns; X.mark a; X.arity (List.length ws)] in
- X.tag X.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab
+ let attrs = [XL.name ns; XL.mark a; XL.arity (List.length 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 []) in
- let attrs = [X.name ns; X.mark a; X.arity (List.length vs)] in
- X.tag X.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab
+ let attrs = [XL.name ns; XL.mark a; XL.arity (List.length vs)] in
+ XL.tag XL.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab
| D.Void n ->
- let attrs = [X.name a; X.mark a; X.arity n] in
- X.tag X.void attrs out tab
+ 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 =
let attrs = [] in
- X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab
+ XL.tag XL.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab
(* interface functions ******************************************************)
module U = NUri
module C = Cps
module H = Hierarchy
-module Y = Entity
+module E = Entity
(* internal functions *******************************************************)
let name a =
let map f i n r s =
- let n = if r then n else "^" ^ n in
+ let n = if r then n else "-" ^ n in
let spc = if i then "" else " " in
f (s ^ n ^ spc)
in
let f s = "name", s in
- Y.names f map a ""
+ E.names f map a ""
let mark a =
let err () = "mark", "" in
let f i = "mark", string_of_int i in
- Y.mark err f a
+ E.mark err f a
(* TODO: the string s must be quoted *)
let meta a =
let err () = "meta", "" in
let f s = "meta", s in
- Y.meta err f a
+ E.meta err f a
let export_entity pp_term si xdir (a, u, b) =
let path = path_of_uri xdir u in
let och = open_out (path ^ obj_ext) in
let out = output_string och in
xml out "1.0" "UTF-8"; doctype out root system;
- let a = Y.Name (U.name_of_uri u, true) :: a in
+ 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
- | Y.Abst w -> tag "ABST" attrs ~contents:(pp_term w)
- | Y.Abbr v -> tag "ABBR" attrs ~contents:(pp_term v)
- | Y.Void -> assert false
+ | E.Abst w -> tag "ABST" attrs ~contents:(pp_term w)
+ | E.Abbr v -> tag "ABBR" attrs ~contents:(pp_term v)
+ | E.Void -> assert false
in
let opts = if si then "si" else "" in
let shp = H.string_of_graph () in
<!ELEMENT Sort EMPTY>
<!ATTLIST Sort
- position NMTOKEN #REQUIRED
- name NMTOKENS #IMPLIED
- mark NMTOKENS #IMPLIED
- meta CDATA #IMPLIED
+ position NMTOKEN #REQUIRED
+ name NMTOKEN #IMPLIED
+ mark NMTOKEN #IMPLIED
+ meta CDATA #IMPLIED
>
<!ELEMENT LRef EMPTY>
<!ATTLIST LRef
- position NMTOKEN #REQUIRED
- name NMTOKENS #IMPLIED
- mark NMTOKENS #IMPLIED
- meta CDATA #IMPLIED
+ position NMTOKEN #REQUIRED
+ name NMTOKEN #IMPLIED
+ mark NMTOKEN #IMPLIED
+ meta CDATA #IMPLIED
>
<!ELEMENT GRef EMPTY>
<!ATTLIST GRef
- uri CDATA #REQUIRED
- name NMTOKENS #IMPLIED
- mark NMTOKENS #IMPLIED
- meta CDATA #IMPLIED
+ uri CDATA #REQUIRED
+ name NMTOKEN #IMPLIED
+ mark NMTOKEN #IMPLIED
+ meta CDATA #IMPLIED
>
<!ELEMENT Cast %term;>
<!ATTLIST Cast
- name NMTOKENS #IMPLIED
- arity NMTOKENS #IMPLIED
- mark NMTOKENS #IMPLIED
- meta CDATA #IMPLIED
+ arity NMTOKEN #IMPLIED
+ mark NMTOKEN #IMPLIED
+ meta CDATA #IMPLIED
>
<!ELEMENT Appl %term;>
<!ATTLIST Appl
- name NMTOKENS #IMPLIED
- arity NMTOKENS #IMPLIED
- mark NMTOKENS #IMPLIED
- meta CDATA #IMPLIED
+ arity NMTOKEN #IMPLIED
+ mark NMTOKEN #IMPLIED
+ meta CDATA #IMPLIED
>
<!ELEMENT Abst %term;>
<!ATTLIST Abst
name NMTOKENS #IMPLIED
- arity NMTOKENS #IMPLIED
- mark NMTOKENS #IMPLIED
+ arity NMTOKEN #IMPLIED
+ mark NMTOKEN #IMPLIED
meta CDATA #IMPLIED
>
<!ELEMENT Abbr %term;>
<!ATTLIST Abbr
name NMTOKENS #IMPLIED
- arity NMTOKENS #IMPLIED
- mark NMTOKENS #IMPLIED
+ arity NMTOKEN #IMPLIED
+ mark NMTOKEN #IMPLIED
meta CDATA #IMPLIED
>
<!ELEMENT Void EMPTY>
<!ATTLIST Void
name NMTOKENS #IMPLIED
- arity NMTOKENS #IMPLIED
- mark NMTOKENS #IMPLIED
+ arity NMTOKEN #IMPLIED
+ mark NMTOKEN #IMPLIED
meta CDATA #IMPLIED
>
<!ELEMENT ABST %term;>
<!ATTLIST ABST
- uri CDATA #REQUIRED
- name NMTOKENS #IMPLIED
- mark NMTOKENS #IMPLIED
- meta CDATA #IMPLIED
+ uri CDATA #REQUIRED
+ name NMTOKEN #IMPLIED
+ mark NMTOKEN #IMPLIED
+ meta CDATA #IMPLIED
>
<!ELEMENT ABBR %term;>
<!ATTLIST ABBR
- uri CDATA #REQUIRED
- name NMTOKENS #IMPLIED
- mark NMTOKENS #IMPLIED
- meta CDATA #IMPLIED
+ uri CDATA #REQUIRED
+ name NMTOKEN #IMPLIED
+ mark NMTOKEN #IMPLIED
+ meta CDATA #IMPLIED
>
<!-- ROOT -->
projects / helm.git / commitdiff