src/lib/log.cmx: src/lib/log.cmi
src/lib/time.cmo: src/lib/log.cmi
src/lib/time.cmx: src/lib/log.cmx
+src/common/marks.cmi:
+src/common/marks.cmo: src/common/marks.cmi
+src/common/marks.cmx: src/common/marks.cmi
src/common/hierarchy.cmi:
src/common/hierarchy.cmo: src/lib/cps.cmx src/common/hierarchy.cmi
src/common/hierarchy.cmx: src/lib/cps.cmx src/common/hierarchy.cmi
-src/common/level.cmi:
-src/common/level.cmo: src/common/level.cmi
-src/common/level.cmx: src/common/level.cmi
+src/common/level.cmi: src/common/marks.cmi
+src/common/level.cmo: src/common/marks.cmi src/common/level.cmi
+src/common/level.cmx: src/common/marks.cmx src/common/level.cmi
src/common/entity.cmo: src/common/level.cmi
src/common/entity.cmx: src/common/level.cmx
src/common/options.cmo: src/lib/cps.cmx
src/common/output.cmi
src/common/output.cmx: src/common/options.cmx src/lib/log.cmx \
src/common/output.cmi
-src/common/marks.cmi: src/common/entity.cmx
-src/common/marks.cmo: src/common/entity.cmx src/common/marks.cmi
-src/common/marks.cmx: src/common/entity.cmx src/common/marks.cmi
src/common/alpha.cmi: src/common/entity.cmx
src/common/alpha.cmo: src/common/entity.cmx src/common/alpha.cmi
src/common/alpha.cmx: src/common/entity.cmx src/common/alpha.cmi
-src/common/ccs.cmi: src/common/entity.cmx
+src/common/ccs.cmi:
src/common/ccs.cmo: src/common/options.cmx src/common/entity.cmx \
src/lib/cps.cmx src/common/ccs.cmi
src/common/ccs.cmx: src/common/options.cmx src/common/entity.cmx \
src/complete_rg/crg.cmx: src/common/level.cmx src/common/entity.cmx \
src/lib/cps.cmx
src/complete_rg/crgOutput.cmi: src/complete_rg/crg.cmx
-src/complete_rg/crgOutput.cmo: src/lib/log.cmi src/common/level.cmi \
- src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
- src/complete_rg/crgOutput.cmi
-src/complete_rg/crgOutput.cmx: src/lib/log.cmx src/common/level.cmx \
- src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
- src/complete_rg/crgOutput.cmi
+src/complete_rg/crgOutput.cmo: src/common/marks.cmi src/lib/log.cmi \
+ src/common/level.cmi src/common/entity.cmx src/complete_rg/crg.cmx \
+ src/lib/cps.cmx src/complete_rg/crgOutput.cmi
+src/complete_rg/crgOutput.cmx: src/common/marks.cmx src/lib/log.cmx \
+ src/common/level.cmx src/common/entity.cmx src/complete_rg/crg.cmx \
+ src/lib/cps.cmx src/complete_rg/crgOutput.cmi
src/text/txt.cmo: src/common/level.cmi
src/text/txt.cmx: src/common/level.cmx
src/text/txtParser.cmi: src/text/txt.cmx
src/automath/autLexer.cmx: src/common/options.cmx src/lib/log.cmx \
src/automath/autParser.cmx
src/automath/autCrg.cmi: src/complete_rg/crg.cmx src/automath/aut.cmx
-src/automath/autCrg.cmo: src/common/options.cmx src/common/level.cmi \
- src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
- src/automath/aut.cmx src/automath/autCrg.cmi
-src/automath/autCrg.cmx: src/common/options.cmx src/common/level.cmx \
- src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
- src/automath/aut.cmx src/automath/autCrg.cmi
-src/xml/xmlLibrary.cmi: src/common/level.cmi src/common/entity.cmx \
- src/common/ccs.cmi
+src/automath/autCrg.cmo: src/common/options.cmx src/common/marks.cmi \
+ src/common/level.cmi src/common/entity.cmx src/complete_rg/crg.cmx \
+ src/lib/cps.cmx src/automath/aut.cmx src/automath/autCrg.cmi
+src/automath/autCrg.cmx: src/common/options.cmx src/common/marks.cmx \
+ src/common/level.cmx src/common/entity.cmx src/complete_rg/crg.cmx \
+ src/lib/cps.cmx src/automath/aut.cmx src/automath/autCrg.cmi
+src/xml/xmlLibrary.cmi: src/common/level.cmi src/common/entity.cmx
src/xml/xmlLibrary.cmo: src/common/options.cmx src/common/level.cmi \
src/common/hierarchy.cmi src/common/entity.cmx src/lib/cps.cmx \
src/common/ccs.cmi src/xml/xmlLibrary.cmi
src/basic_rg/brg.cmo: src/common/level.cmi src/common/entity.cmx
src/basic_rg/brg.cmx: src/common/level.cmx src/common/entity.cmx
src/basic_rg/brgCrg.cmi: src/complete_rg/crg.cmx src/basic_rg/brg.cmx
-src/basic_rg/brgCrg.cmo: src/common/marks.cmi src/common/level.cmi \
- src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
- src/basic_rg/brg.cmx src/basic_rg/brgCrg.cmi
-src/basic_rg/brgCrg.cmx: src/common/marks.cmx src/common/level.cmx \
- src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
- src/basic_rg/brg.cmx src/basic_rg/brgCrg.cmi
+src/basic_rg/brgCrg.cmo: src/common/level.cmi src/common/entity.cmx \
+ src/complete_rg/crg.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \
+ src/basic_rg/brgCrg.cmi
+src/basic_rg/brgCrg.cmx: src/common/level.cmx src/common/entity.cmx \
+ src/complete_rg/crg.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \
+ 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/xmlCrg.cmi src/common/options.cmx \
src/basic_rg/brgReduction.cmo: src/common/status.cmx src/lib/share.cmx \
src/common/output.cmi src/common/options.cmx src/lib/log.cmi \
src/common/level.cmi src/common/hierarchy.cmi src/common/entity.cmx \
- src/lib/cps.cmx src/common/ccs.cmi src/basic_rg/brgOutput.cmi \
+ src/common/ccs.cmi src/basic_rg/brgOutput.cmi \
src/basic_rg/brgEnvironment.cmi src/basic_rg/brg.cmx \
src/basic_rg/brgReduction.cmi
src/basic_rg/brgReduction.cmx: src/common/status.cmx src/lib/share.cmx \
src/common/output.cmx src/common/options.cmx src/lib/log.cmx \
src/common/level.cmx src/common/hierarchy.cmx src/common/entity.cmx \
- src/lib/cps.cmx src/common/ccs.cmx src/basic_rg/brgOutput.cmx \
+ src/common/ccs.cmx src/basic_rg/brgOutput.cmx \
src/basic_rg/brgEnvironment.cmx src/basic_rg/brg.cmx \
src/basic_rg/brgReduction.cmi
src/basic_rg/brgValidity.cmi: src/common/status.cmx \
src/basic_rg/brgValidity.cmx src/basic_rg/brgType.cmx \
src/basic_rg/brgReduction.cmx src/basic_rg/brgEnvironment.cmx \
src/basic_rg/brg.cmx src/basic_rg/brgUntrusted.cmi
-src/basic_ag/bag.cmo: src/lib/log.cmi src/common/entity.cmx src/lib/cps.cmx
-src/basic_ag/bag.cmx: src/lib/log.cmx src/common/entity.cmx src/lib/cps.cmx
+src/basic_ag/bag.cmo: src/common/marks.cmi src/lib/log.cmi \
+ src/common/entity.cmx src/lib/cps.cmx
+src/basic_ag/bag.cmx: src/common/marks.cmx src/lib/log.cmx \
+ src/common/entity.cmx src/lib/cps.cmx
src/basic_ag/bagCrg.cmi: src/complete_rg/crg.cmx src/basic_ag/bag.cmx
src/basic_ag/bagCrg.cmo: src/common/marks.cmi src/common/level.cmi \
src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
src/basic_ag/bag.cmx src/basic_ag/bagEnvironment.cmi
src/basic_ag/bagEnvironment.cmx: src/lib/log.cmx src/common/entity.cmx \
src/basic_ag/bag.cmx src/basic_ag/bagEnvironment.cmi
-src/basic_ag/bagSubstitution.cmi: src/basic_ag/bag.cmx
+src/basic_ag/bagSubstitution.cmi: src/common/marks.cmi src/basic_ag/bag.cmx
src/basic_ag/bagSubstitution.cmo: src/lib/share.cmx src/basic_ag/bag.cmx \
src/basic_ag/bagSubstitution.cmi
src/basic_ag/bagSubstitution.cmx: src/lib/share.cmx src/basic_ag/bag.cmx \
include Makefile.common
-XMLDIR = $(HOME)/svn/helm_stable/www/lambdadelta
+XMLDIR = ../../www/lambdadelta
INPUT = examples/grundlagen/grundlagen_2.aut
module K = U.UriHash
module C = Cps
module G = Options
-module E = Entity
+module J = Marks
module N = Level
+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 = E.attrs * D.term list
-
type context_node = qid option (* context node: None = root *)
type status = {
node: context_node; (* current context node *)
nodes: context_node list; (* context node list *)
line: int; (* line number *)
- mk_uri: G.uri_generator; (* uri generator *)
+ mk_uri: G.uri_generator; (* uri generator *)
+ lenv: N.status; (* level environment *)
}
-type resolver = Local of int
- | Global of context
-
let henv_size, hcnt_size = 7000, 4300 (* hash tables initial sizes *)
let henv = K.create henv_size (* optimized global environment *)
let empty_cnt = D.ESort
let add_abst cnt id w =
- D.EBind (cnt, [E.Name (id, true)], D.Abst (N.infinite, w))
+ D.EBind (cnt, E.node_attrs ~name:(id, true) (), D.Abst (N.two, w))
-let mk_lref f i = f (D.TLRef ([], i))
+let mk_lref f a i = f a.E.n_degr (D.TLRef (E.empty_node, i))
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 age, cnt = K.find henv (uri_of_qid qid) in f qid age cnt
- with Not_found -> err qid
+ try let a, cnt = K.find henv (uri_of_qid qid) in f qid a cnt
+ with Not_found -> err qid
let resolve_gref_relaxed f st qid =
(* this is not tail recursive *)
let add_proj e t = match e with
| D.ESort -> t
| D.EBind (D.ESort, a, b) -> D.TBind (a, b, t)
- | _ -> D.TProj ([], e, t)
-
-let lenv_of_cnt cnt = cnt
+ | _ -> D.TProj (E.empty_node, e, t)
(* this is not tail recursive in the GRef branch *)
let rec xlate_term f st lenv = function
- | A.Sort s ->
- let f h = f (D.TSort ([], h)) in
+ | A.Sort s ->
+ let f h = f 0 (D.TSort (E.empty_node, h)) in
if s then f 0 else f 1
| A.Appl (v, t) ->
- let f vv tt = f (D.TAppl ([], vv, tt)) in
- let f vv = xlate_term (f vv) st lenv t in
+ let f vv d tt = f d (D.TAppl (E.empty_node, vv, tt)) in
+ let f _ vv = xlate_term (f vv) st lenv t in
xlate_term f st lenv v
| A.Abst (name, w, t) ->
- let f ww =
- let a = [E.Name (name, true)] in
- let f tt =
- let b = D.Abst (N.infinite, ww) in
- f (D.TBind (a, b, tt))
+ let f d ww =
+ let a = E.node_attrs ~name:(name, true) () in
+ let f d tt =
+ let l = match d with
+ | 0 -> N.one
+ | 1 -> N.unknown st.lenv (J.new_mark ())
+ | 2 -> N.two
+ | _ -> assert false
+ in
+ let b = D.Abst (l, ww) in
+ f d (D.TBind (a, b, tt))
in
let f lenv = xlate_term f st lenv t in
- push_abst f a ww lenv
+ push_abst f {a with E.n_degr = succ d} ww lenv
in
xlate_term f st lenv w
| A.GRef (name, args) ->
- let map1 args a =
- let f id _ = A.GRef ((id, true, []), []) :: args in
- E.name C.err f a
- in
+ let map1 args (id, _) = A.GRef ((id, true, []), []) :: args in
let map2 f arg args =
- let f arg = f (D.EAppl (args, [], arg)) in
+ let f _ arg = f (D.EAppl (args, E.empty_node, arg)) in
xlate_term f st lenv arg
in
- let g qid age cnt =
- let gref = D.TGRef ([age], uri_of_qid qid) in
- if cnt = D.ESort then f gref else
+ let g qid a cnt =
+ let gref = D.TGRef (a, uri_of_qid qid) in
+ if cnt = D.ESort then f a.E.n_degr gref else
let f = function
- | D.EAppl (D.ESort, a, v) -> f (D.TAppl (a, v, gref))
- | args -> f (D.TProj ([], args, gref))
+ | D.EAppl (D.ESort, a, v) -> f a.E.n_degr (D.TAppl (a, v, gref))
+ | args -> f a.E.n_degr (D.TProj (E.empty_node, args, gref))
in
let f args = C.list_fold_right f map2 args D.ESort in
- D.sub_list_strict (D.fold_attrs f map1 args) cnt args
+ D.sub_list_strict (D.fold_names f map1 args) cnt args
in
let g qid = resolve_gref_relaxed g st qid in
let err () = complete_qid g st name in
| A.Block (name, w) ->
let f qid =
let f cnt =
- let f ww =
+ let f _ ww =
K.add hcnt (uri_of_qid qid) (add_abst cnt name ww);
err {st with node = Some qid}
in
in
complete_qid f st (name, true, [])
| A.Decl (name, w) ->
- let f cnt =
- let lenv = lenv_of_cnt cnt in
+ let f lenv =
let f qid =
- let f ww =
- let age = E.Apix st.line in
- K.add henv (uri_of_qid qid) (age, cnt);
+ let f d ww =
+ let a = E.node_attrs ~apix:st.line ~degr:(succ d) () in
+ K.add henv (uri_of_qid qid) (a, lenv);
let t = add_proj lenv ww in
(*
print_newline (); CrgOutput.pp_term print_string t;
*)
- let b = E.Abst (N.infinite, t) in
- let entity = [age], uri_of_qid qid, b in
+ let b = E.Abst t in
+ let entity = E.empty_root, a, uri_of_qid qid, b in
f {st with line = succ st.line} entity
in
xlate_term f st lenv w
in
get_cnt_relaxed f st
| A.Def (name, w, trans, v) ->
- let f cnt =
- let lenv = lenv_of_cnt cnt in
+ let f lenv =
let f qid =
- let f ww =
- let f vv =
- let age = E.Apix st.line in
- K.add henv (uri_of_qid qid) (age, cnt);
- let t = add_proj lenv (D.TCast ([], ww, vv)) in
+ let f _ ww =
+ let f d vv =
+ let na = E.node_attrs ~apix:st.line ~degr:d () in
+ K.add henv (uri_of_qid qid) (na, lenv);
+ let t = add_proj lenv (D.TCast (E.empty_node, ww, vv)) in
(*
print_newline (); CrgOutput.pp_term print_string t;
*)
let b = E.Abbr t in
- let a = age :: if trans then [] else [E.Meta [E.Private]] in
- let entity = a, uri_of_qid qid, b in
+ let ra = if trans then E.empty_root else E.root_attrs ~meta:[E.Private] () in
+ let entity = ra, na, uri_of_qid qid, b in
f {st with line = succ st.line} entity
in
xlate_term f st lenv v
let initial_status () =
K.clear henv; K.clear hcnt; {
- path = []; node = None; nodes = []; line = 1; mk_uri = G.get_mk_uri ()
+ path = []; node = None; nodes = []; line = 1; mk_uri = G.get_mk_uri ();
+ lenv = N.initial_status ();
}
let refresh_status st = {st with
(* kernel version: basic, absolute, global *)
(* note : experimental *)
+module J = Marks
module E = Entity
type uri = E.uri
-type attrs = E.attrs
+type attrs = E.node_attrs
type bind = Void (* exclusion *)
| Abst of term (* abstraction *)
| Abbr of term (* abbreviation *)
-and term = Sort of int (* hierarchy index *)
- | LRef of int (* location *)
- | GRef of uri (* reference *)
- | Cast of term * term (* domain, element *)
- | Appl of term * term (* argument, function *)
- | Bind of attrs * int * bind * term (* name, location, binder, scope *)
+and term = Sort of int (* hierarchy index *)
+ | LRef of J.mark (* location *)
+ | GRef of uri (* reference *)
+ | Cast of term * term (* domain, element *)
+ | Appl of term * term (* argument, function *)
+ | Bind of attrs * J.mark * bind * term (* name, location, binder, scope *)
type entity = term E.entity (* attrs, uri, binder *)
-type lenv = (attrs * int * bind) list (* name, location, binder *)
+type lenv = (attrs * J.mark * bind) list (* name, location, binder *)
type message = (lenv, term) Log.item list
D.shift (xlate_term f c) e t
(* this case should be removed by improving alpha-conversion *)
| D.TBind (ab, D.Abst (n, ws), D.TCast (ac, u, t)) ->
- xlate_term f c (D.TCast (ac, D.TBind (ab, D.Abst (N.pred n, ws), u), D.TBind (ab, D.Abst (n, ws), t)))
+ xlate_term f c (D.TCast (ac, D.TBind (ab, D.Abst (N.minus n 1, ws), u), D.TBind (ab, D.Abst (n, ws), t)))
| D.TBind (a, b, t) ->
let f cc =
let a, l, b = List.hd cc in
and xlate_bind f c a = function
| D.Abst (_, w) ->
- let f ww = Z.push "xlate_bind" f c a (J.new_location ()) (Z.Abst ww) in
+ let f ww = Z.push "xlate_bind" f c a (J.new_mark ()) (Z.Abst ww) in
xlate_term f c w
| D.Abbr v ->
- let f vv = Z.push "xlate_bind" f c a (J.new_location ()) (Z.Abbr vv) in
+ let f vv = Z.push "xlate_bind" f c a (J.new_mark ()) (Z.Abbr vv) in
xlate_term f c v
| D.Void ->
- Z.push "xlate_bind" f c a (J.new_location ()) Z.Void
+ Z.push "xlate_bind" f c a (J.new_mark ()) Z.Void
(* internal functions: bag to crg term **************************************)
let rec xlate_bk_term f c = function
- | Z.Sort h -> f (D.TSort ([], h))
- | Z.GRef s -> f (D.TGRef ([], s))
+ | Z.Sort h -> f (D.TSort (E.empty_node, h))
+ | Z.GRef s -> f (D.TGRef (E.empty_node, s))
| Z.LRef l ->
- let f i = f (D.TLRef ([], i)) in
+ let f i = f (D.TLRef (E.empty_node, i)) in
Z.nth C.err f l c
| Z.Cast (u, t) ->
- let f tt uu = f (D.TCast ([], uu, tt)) in
+ let f tt uu = f (D.TCast (E.empty_node, uu, tt)) in
let f tt = xlate_bk_term (f tt) c u in
xlate_bk_term f c t
| Z.Appl (u, t) ->
- let f tt uu = f (D.TAppl ([], uu, tt)) in
+ let f tt uu = f (D.TAppl (E.empty_node, uu, tt)) in
let f tt = xlate_bk_term (f tt) c u in
xlate_bk_term f c t
| Z.Bind (a, l, b, t) ->
(* Interface functions ******************************************************)
-let set_entity f (a, uri, b) =
+let set_entity f (ra, na, uri, b) =
let age = get_age () in
- let entry = (E.Apix age :: a), uri, b in
+ let entry = ra, {na with E.n_apix = Some age}, uri, b in
K.add env uri entry; f entry
let get_entity f uri =
count_term f c t
let count_entity f c = function
- | _, _, E.Abst (_, w) ->
+ | _, _, _, E.Abst w ->
let c = {c with eabsts = succ c.eabsts} in
count_term f c w
- | _, _, E.Abbr v ->
+ | _, _, _, E.Abbr v ->
let c = {c with eabbrs = succ c.eabbrs} in
count_term f c v
- | _, _, E.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 = J.locations () in
+ let locations = J.marks () in
L.warn level (P.sprintf "Kernel representation summary (basic_ag)");
L.warn level (P.sprintf " Total entry items: %7u" items);
L.warn level (P.sprintf " Declaration items: %7u" c.eabsts);
E.name err f a
let res a l och =
- let err () = P.fprintf och "#%u" l in
+ let err () = P.fprintf och "#%s" (J.to_string l) in
if !G.indexes then err () else name err och a
let rec pp_term c och = function
let f s = P.fprintf och "%s" s in
H.string_of_sort err f h
| Z.LRef i ->
- let err () = P.fprintf och "#%u" i in
+ let err () = P.fprintf och "#%s" (J.to_string i) in
let f a _ = name err och a in
if !G.indexes then err () else Z.get err f c i
| Z.GRef s -> P.fprintf och "$%s" (U.string_of_uri s)
type whd_result =
| Sort_ of int
- | LRef_ of int * Z.term option
+ | LRef_ of J.mark * Z.term option
| GRef_ of Z.entity
- | Bind_ of Z.attrs * int * Z.term * Z.term
+ | Bind_ of Z.attrs * J.mark * Z.term * Z.term
type ho_whd_result =
| Sort of int
let level = 4
let term_of_whdr = function
- | Sort_ h -> Z.Sort h
- | LRef_ (i, _) -> Z.LRef i
- | GRef_ (_, uri, _) -> Z.GRef uri
- | Bind_ (a, l, w, t) -> Z.bind_abst a l w t
+ | Sort_ h -> Z.Sort h
+ | LRef_ (i, _) -> Z.LRef i
+ | GRef_ (_, _, uri, _) -> Z.GRef uri
+ | Bind_ (a, l, w, t) -> Z.bind_abst a l w t
let log1 s c t =
let sc, st = s ^ " in the environment", "the term" in
begin match m.s with
| [] -> f m (Bind_ (a, l, w, t))
| v :: tl ->
- let nl = J.new_location () in
+ let nl = J.new_mark () in
let f mc = ZS.subst (whd f c {m with c = mc; s = tl}) nl l t in
Z.push "!" f m.c a nl (Z.Abbr (Z.Cast (w, v)))
end
| Z.Bind (a, l, b, t) ->
- let nl = J.new_location () in
+ let nl = J.new_mark () in
let f mc = ZS.subst (whd f c {m with c = mc}) nl l t in
Z.push "!" f m.c a nl b
let rec ho_whd f c m x =
(* L.warn "entering R.ho_whd"; *)
let aux m = function
- | Sort_ h -> f (Sort h)
- | Bind_ (_, _, w, _) ->
+ | Sort_ h -> f (Sort h)
+ | 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_ (_, _, E.Abst (_, w)) -> ho_whd f c m w
- | GRef_ (_, _, E.Abbr v) -> ho_whd f c m v
- | LRef_ (_, None) -> assert false
- | GRef_ (_, _, E.Void) -> assert false
+ | LRef_ (_, Some w) -> ho_whd f c m w
+ | 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_ (_, _, _, 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 st a c m1 m2 else f false
- | GRef_ ((E.Apix a1 :: _), _, E.Abst _),
- GRef_ ((E.Apix a2 :: _), _, E.Abst _) ->
+ | GRef_ (_, {E.n_apix = Some a1}, _, E.Abst _),
+ GRef_ (_, {E.n_apix = Some a2}, _, E.Abst _) ->
if a1 = a2 then are_convertible_stacks f st a c m1 m2 else f false
- | GRef_ ((E.Apix a1 :: _), _, E.Abbr v1),
- GRef_ ((E.Apix a2 :: _), _, E.Abbr v2) ->
+ | GRef_ (_, {E.n_apix = Some a1}, _, E.Abbr v1),
+ GRef_ (_, {E.n_apix = Some a2}, _, E.Abbr v2) ->
if a1 = a2 then
let f a =
if a then f a else are_convertible f st 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_ (_, _, E.Abbr v2) ->
+ | _, GRef_ (_, _, _, E.Abbr v2) ->
whd (aux m1 r1) c m2 v2
- | GRef_ (_, _, E.Abbr v1), _ ->
+ | GRef_ (_, _, _, E.Abbr v1), _ ->
whd (aux_rev m2 r2) c m1 v1
| Bind_ (a1, l1, w1, t1), Bind_ (a2, l2, w2, t2) ->
- let l = J.new_location () in
+ let l = J.new_mark () in
let h c =
let m1, m2 = inc m1, inc m2 in
let f t1 = ZS.subst (are_convertible f st a c m1 t1 m2) l l2 t2 in
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-val subst: (Bag.term -> 'a) -> int -> int -> Bag.term -> 'a
+val subst: (Bag.term -> 'a) -> Marks.mark -> Marks.mark -> Bag.term -> 'a
Z.get err0 f c i
| Z.GRef uri ->
let f = function
- | _, _, E.Abst (_, w) -> f x w
- | _, _, E.Abbr (Z.Cast (w, v)) -> f x w
- | _, _, E.Abbr _ -> assert false
- | _, _, E.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
ZE.get_entity f uri
| Z.Bind (a, l, Z.Abbr v, t) ->
(* to share *)
let type_check err f st = function
- | a, uri, E.Abst (n, t) ->
+ | ra, na, uri, E.Abst t ->
let err msg = err (L.Uri uri :: msg) in
- let f xt tt = ZE.set_entity (f tt) (a, uri, E.Abst (n, xt)) in
+ let f xt tt = ZE.set_entity (f tt) (ra, na, uri, E.Abst xt) in
ZT.type_of err f st Z.empty_lenv t
- | a, uri, E.Abbr t ->
+ | ra, na, uri, E.Abbr t ->
let err msg = err (L.Uri uri :: msg) in
- let f xt tt = ZE.set_entity (f tt) (a, uri, E.Abbr xt) in
+ let f xt tt = ZE.set_entity (f tt) (ra, na, uri, E.Abbr xt) in
ZT.type_of err f st Z.empty_lenv t
- | _, _, E.Void -> assert false
+ | _, _, _, E.Void -> assert false
module N = Level
type uri = E.uri
-type attrs = E.attrs
+type attrs = E.node_attrs
type bind = Void (* *)
| Abst of N.level * term (* level, type *)
let push e c a b = Cons (e, c, a, b)
let rec get i = function
- | Null -> Null, Null, [], Void
+ | Null -> Null, Null, E.empty_node, Void
| Cons (e, c, a, b) when i = 0 -> e, c, a, b
| Cons (e, _, _, _) -> get (pred i) e
module C = Cps
module E = Entity
-module J = Marks
module N = Level
module D = Crg
module B = Brg
and xlate_bind f a b x = match b with
| D.Abst (n, w) ->
- let f ww = f (B.Bind (J.new_mark () :: a, B.Abst (n, ww), x)) in
+ let f ww = f (B.Bind (a, B.Abst (n, ww), x)) in
xlate_term f w
| D.Abbr v ->
let f vv = f (B.Bind (a, B.Abbr vv, x)) in
(* decps *)
let set_entity entity =
- let _, uri, _ = entity in
+ let _, _, uri, _ = entity in
K.add env uri entity; entity
let get_entity uri =
- try K.find env uri with Not_found -> [], uri, E.Void
+ try K.find env uri with Not_found -> E.empty_root, E.empty_node, uri, E.Void
count_term_binder f c e b
let count_entity f c = function
- | _, u, E.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
- | _, _, E.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
- | _, _, E.Void -> assert false
+ | _, _, _, E.Void -> assert false
let print_counters f c =
let terms =
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 (E.Name (n, r) :: a) in
+ let f n r = if n = n0 && r = r0 then f a else f {a with E.n_name = Some (n, r)} in
aux f e n0 r0
in
E.name C.err f a
E.name err f a
let pp_level och n =
- if N.is_infinite n then () else P.fprintf och "^%s" (N.to_string n)
+ P.fprintf och "%s" (N.to_string n)
let rec pp_term e och = function
| B.Sort (_, h) ->
V_______________________________________________________________ *)
module U = NUri
-module C = Cps
module W = Share
module L = Log
module H = Hierarchy
else m, x, None
| B.GRef (_, uri) ->
begin match BE.get_entity uri with
- | _, _, E.Abbr v ->
+ | _, _, _, E.Abbr v ->
if st.S.delta then begin
if !G.summary then O.add ~gdelta:1 ();
step st m v
end else
m, x, Some v
- | _, _, E.Abst (_, w) ->
+ | _, _, _, E.Abst w ->
if assert_tstep m true then begin
if !G.summary then O.add ~grt:1 ();
step st (tstep m) w
end else
m, x, None
- | _, _, E.Void ->
+ | _, _, _, E.Void ->
assert false
end
| B.LRef (_, i) ->
let n = N.minus n m.d in
m, B.Bind (a, B.Abst (n, w), t), None
| (c, v) :: s ->
- if N.is_zero n then Q.add_nonzero st.S.cc a;
+(* if N.is_zero n then Q.add_nonzero st.S.cc a; *)
if !G.summary then O.add ~beta:1 ~theta:(List.length s) ();
- let v = if assert_tstep m false then B.Cast ([], w, v) else v in
+ let v = if assert_tstep m false then B.Cast (E.empty_node, w, v) else v in
let e = B.push m.e c a (B.abbr v) in
step st {m with e = e; s = s} t
end
| _ -> false
let push m a b =
- assert (m.s = []);
let a, l = match b with
- | B.Abst _ -> E.Apix m.l :: a, succ m.l
+ | B.Abst _ -> {a with E.n_apix = Some m.l}, succ m.l
| b -> a, m.l
in
let e = B.push m.e m.e a b in
match t1, r1, t2, r2 with
| B.Sort (_, h1), _, B.Sort (_, h2), _ ->
h1 = h2
- | B.LRef (a1, _), _, B.LRef (a2, _), _ ->
- let e1 = E.apix C.err C.start a1 in
- let e2 = E.apix C.err C.start a2 in
+ | B.LRef ({E.n_apix = Some e1}, _), _,
+ B.LRef ({E.n_apix = Some e2}, _), _ ->
if e1 = e2 then ac_stacks st m1 m2 else false
| B.GRef (_, u1), None, B.GRef (_, u2), None ->
if U.eq u1 u2 && assert_iterations m1 m2 then ac_stacks st m1 m2 else false
- | B.GRef (a1, u1), Some v1, B.GRef (a2, u2), Some v2 ->
- let e1 = E.apix C.err C.start a1 in
- let e2 = E.apix C.err C.start a2 in
+ | B.GRef ({E.n_apix = Some e1}, u1), Some v1,
+ B.GRef ({E.n_apix = Some e2}, u2), Some v2 ->
if e1 < e2 then begin
if !G.summary then O.add ~gdelta:1 ();
ac_nfs st (m1, t1, r1) (step st m2 v2)
ac_nfs st (step st m1 v1) (m2, t2, r2)
| B.Bind (a1, (B.Abst (n1, w1) as b1), t1), _,
B.Bind (a2, (B.Abst (n2, w2) as b2), t2), _ ->
- if n1 = n2 then () else Q.add_equal st.S.cc a1 a2;
+(* if n1 = n2 then () else Q.add_equal st.S.cc a1 a2; *)
if ac {st with S.si = false} (reset m1 zero) w1 (reset m2 zero) w2 then
ac st (push m1 a1 b1) t1 (push m2 a2 b2) t2
else false
| B.Sort _, _, B.Bind (a, (B.Abst (n, _) as b), t), _ ->
- if N.is_zero n then () else Q.add_zero st.S.cc a;
+(* if N.is_zero n then () else Q.add_zero st.S.cc a; *)
if !G.summary then O.add ~si:1 ();
ac st (push m1 a b) t1 (push m2 a b) t
| _ -> false
val get: kam -> int -> Brg.bind
-val push: kam -> Entity.attrs -> Brg.bind -> kam
+val push: kam -> Entity.node_attrs -> Brg.bind -> kam
val xwhd: Status.status -> kam -> int option -> Brg.term -> kam * Brg.term
end
| B.GRef (_, uri) ->
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 ->
+ | _, _, _, 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 = 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))
+ | _ -> f (B.Cast (E.empty_node, vv, xv))
in
type_of err f st m v
| B.Bind (a, B.Abst (n, u), t) ->
let f xu xt tt =
- f (W.sh2 u xu t xt x (B.bind_abst n a)) (B.bind_abst (N.pred n) a xu tt)
+ f (W.sh2 u xu t xt x (B.bind_abst n a)) (B.bind_abst (N.minus n 1) a xu tt)
in
let f xu m = b_type_of err (f xu) st m t in
let f xu _ = f xu (BR.push m a (B.abst n xu)) in
(* to share *)
let type_check err f st = function
- | a, uri, E.Abst (n, t) ->
+ | ra, na, uri, E.Abst t ->
let err msg = err (L.Uri uri :: msg) in
let f xt tt =
- let e = BE.set_entity (a, uri, E.Abst (n, xt)) in f tt e
+ let e = BE.set_entity (ra, na, uri, E.Abst xt) in f tt e
in
BT.type_of err f st BR.empty_kam t
- | a, uri, E.Abbr t ->
+ | ra, na, uri, E.Abbr t ->
let err msg = err (L.Uri uri :: msg) in
let f xt tt =
let xt = match xt with
| B.Cast _ -> xt
- | _ -> B.Cast ([], tt, xt)
+ | _ -> B.Cast (E.empty_node, tt, xt)
in
- let e = BE.set_entity (a, uri, E.Abbr xt) in f tt e
+ let e = BE.set_entity (ra, na, uri, E.Abbr xt) in f tt e
in
BT.type_of err f st BR.empty_kam t
- | _, _, E.Void -> assert false
+ | _, _, _, E.Void -> assert false
let validate err f st e =
let uri, t = match e with
- | _, uri, E.Abst (_, t) -> uri, t
- | _, uri, E.Abbr t -> uri, t
- | _, _, E.Void -> assert false
+ | _, _, uri, E.Abst t -> uri, t
+ | _, _, uri, E.Abbr t -> uri, t
+ | _, _, _, E.Void -> assert false
in
let err msg = err (L.Uri uri :: msg) in
let f () = let _ = BE.set_entity e in f () in
end
| B.GRef (_, uri) ->
begin match BE.get_entity uri with
- | _, _, E.Abst _
- | _, _, E.Abbr _ -> f ()
- | _, _, E.Void ->
+ | _, _, _, E.Abst _
+ | _, _, _, E.Abbr _ -> f ()
+ | _, _, _, E.Void ->
error1 err "reference to unknown entry" m x
end
| B.Bind (a, b, t) ->
-hierarchy level entity options output marks alpha ccs status
+marks hierarchy level entity options output alpha ccs status
module E = Entity
-(* internal functions *******************************************************)
-
-let rec rename ns n =
- let token, mode = n in
- let n = token ^ "_", mode in
- if List.mem n ns then rename ns n else n
-
-let alpha_name acc attr =
- let ns, a = acc in
- match attr with
- | E.Name n ->
- if List.mem n ns then
- let n = rename ns n in
- n :: ns, E.Name n :: a
- else
- n :: ns, attr :: a
- | _ -> assert false
-
(* interface functions ******************************************************)
-let alpha ns a =
- let f a names =
- let _, names = List.fold_left alpha_name (ns, []) (List.rev names) in
- List.rev_append a names
+let rec alpha mem x a =
+ let err () = a in
+ let f () = match a.E.n_name with
+ | None -> assert false
+ | Some (token, mode) -> alpha mem x {a with E.n_name = Some (token ^ "_", mode)}
in
- E.get_names f a
+ mem err f x a
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-val alpha: Entity.names -> Entity.attrs -> Entity.attrs
+val alpha: ((unit -> Entity.node_attrs) -> (unit -> Entity.node_attrs) ->
+ 'a -> Entity.node_attrs -> Entity.node_attrs
+ ) ->
+ 'a -> Entity.node_attrs -> Entity.node_attrs
module C = Cps
module E = Entity
module G = Options
-
+(*
type csys = {
buri: E.uri;
mutable tp : int list;
let i = abs (mark xa), abs (mark ia) in
if L.mem i s.tn then () else s.tn <- i :: s.tn
else ()
+*)
\ / version 2 or (at your option) any later version.
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-
+(*
type csys = {
buri: Entity.uri;
mutable tp : int list;
val add_zero: csys -> Entity.attrs -> unit
val add_equal: csys -> Entity.attrs -> Entity.attrs -> unit
+*)
type name = id * bool (* token, real? *)
-type names = name list
-
type meta = Main (* main object *)
| InProp (* inhabitant of a proposition *)
| Progress (* uncompleted object *)
| Private (* private global definition *)
-type attr = Name of name (* name *)
- | Apix of int (* additional position index *)
- | Mark of int (* node marker *)
- | Meta of meta list (* metaliguistic classification *)
- | Info of (string * string) (* metaliguistic annotation: language (defaults to "en-US"), text *)
+type node_attrs = {
+ n_name: name option; (* name *)
+ n_apix: int option; (* additional position index *)
+ n_degr: int; (* degree *)
+ n_real: bool; (* real node? (not generated) *)
+}
-type attrs = attr list (* attributes *)
+type root_attrs = {
+ r_meta: meta list; (* metaliguistic classification *)
+ r_info: (string * string) option; (* metaliguistic annotation: language (defaults to "en-US"), text *)
+}
-type 'term bind = Abst of N.level * 'term (* declaration: level, domain *)
- | Abbr of 'term (* definition: body *)
- | Void (* exclusion *)
+type 'term bind = Abst of 'term (* declaration: domain *)
+ | Abbr of 'term (* definition: body *)
+ | Void (* exclusion *)
-type 'term entity = attrs * uri * 'term bind (* attrs, name, binder *)
+type 'term entity = root_attrs * node_attrs * uri * 'term bind (* attrs, uri, binder *)
(* helpers ******************************************************************)
-let common f (a, u, _) = f a u
-
-let rec name err f = function
- | Name (n, r) :: _ -> f n r
- | _ :: tl -> name err f tl
- | [] -> err ()
-
-let names f map l a =
- let rec aux f i a = function
- | [] -> f a
- | Name (n, r) :: tl -> aux (map f i n r) false a tl
- | _ :: tl -> aux f i a tl
- in
- aux f true a l
-
-let rec get_name err f j = function
- | [] -> err ()
- | Name (n, r) :: _ when j = 0 -> f n r
- | Name _ :: tl -> get_name err f (pred j) tl
- | _ :: tl -> get_name err f j tl
-
-let rec get_names f = function
- | [] -> f [] []
- | Name _ as n :: tl ->
- let f a ns = f a (n :: ns) in get_names f tl
- | e :: tl ->
- let f a = f (e :: a) in get_names f tl
-
-let count_names a =
- let rec aux k = function
- | [] -> k
- | Name _ :: tl -> aux (succ k) tl
- | _ :: tl -> aux k tl
- in
- aux 0 a
-
-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 meta err f = function
- | Meta ms :: _ -> f ms
- | _ :: tl -> meta err f tl
- | [] -> err ()
-
-let rec info err f = function
- | Info (lg, tx) :: _ -> f lg tx
- | _ :: tl -> info 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 rec rev_append_names ns = function
- | [] -> ns
- | Name n :: tl -> rev_append_names (n :: ns) tl
- | _ :: tl -> rev_append_names ns tl
+let node_attrs ?(real=true) ?apix ?name ?(degr=0) () = {
+ n_real = real; n_apix = apix; n_name = name; n_degr = degr;
+}
+
+let root_attrs ?(meta=[]) ?info () = {
+ r_meta = meta; r_info = info;
+}
+
+let empty_node = node_attrs ()
+
+let empty_root = root_attrs ()
+
+let common f (ra, na, u, _) = f ra na u
+
+let rec name err f a = match a.n_name with
+ | Some (n, r) -> f n r
+ | None -> err ()
+
+let rec apix err f a = match a.n_apix with
+ | Some i -> f i
+ | None -> err ()
+
+let rec info err f a = match a.r_info with
+ | Some (lg, tx) -> f lg tx
+ | None -> err ()
let xlate f xlate_term = function
- | a, uri, Abst (n, t) ->
- let f t = f (a, uri, Abst (n, t)) in xlate_term f t
- | a, uri, Abbr t ->
- let f t = f (a, uri, Abbr t) in xlate_term f t
- | _, _, Void ->
+ | ra, na, uri, Abst t ->
+ let f t = f (ra, na, uri, Abst t) in xlate_term f t
+ | ra, na, uri, Abbr t ->
+ let f t = f (ra, na, uri, Abbr t) in xlate_term f t
+ | _, _, _, Void ->
assert false
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-type level = int option
+module H = Hashtbl
+
+module J = Marks
+
+type level = Inf (* infinite *)
+ | Fin of int (* finite *)
+ | Ref of J.mark (* unknown *)
+
+type const = NotZero (* not zero: beta and whnf allowed *)
+
+type contents = Value of level (* defined with this level *)
+ | Const of const list (* undefined with these constraints *)
+
+type status = (J.mark, contents) H.t (* environment for level variables *)
+
+(* Internal functions *******************************************************)
+
+let env_size = 2000
+
+let empty_ref = Const []
+
+let find st k =
+ try H.find st k with Not_found -> H.add st k empty_ref; empty_ref
+
+let rec resolve st k = match find st k with
+ | Value (Ref k) -> resolve st k
+ | cell -> k, cell
(* Interface functions ******************************************************)
-let infinite = None
+let initial_status () =
+ H.create env_size
+
+let infinite = Inf
+
+let zero = Fin 0
-let finite i = Some i
+let one = Fin 1
-let is_zero xi =
- xi = (Some 0)
+let two = Fin 2
-let is_infinite xi =
- xi = None
+let finite i = Fin i
-let succ = function
- | None -> None
- | Some i -> Some (succ i)
+let unknown st k = match resolve st k with
+ | _, Value l -> l
+ | k, Const _ -> Ref k
-let pred = function
- | None -> None
- | Some i when i > 1 -> Some (pred i)
- | _ -> Some 0
+let is_zero l =
+ l = zero
let minus n j = match n with
- | None -> None
- | Some i when i > j -> Some (i - j)
- | _ -> Some 0
+ | Inf -> Inf
+ | Fin i when i > j -> Fin (i - j)
+ | Fin _ -> zero
+ | Ref i -> Inf (* assert false *)
let to_string = function
- | None -> ""
- | Some i -> string_of_int i
+ | Inf -> ""
+ | Fin i -> string_of_int i
+ | Ref k -> "-" ^ J.to_string k
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
+type status
+
type level
+val initial_status: unit -> status
+
val infinite: level
val finite: int -> level
-val is_zero: level -> bool
+val one: level
-val is_infinite: level -> bool
+val two: level
-val succ: level -> level
+val unknown: status -> Marks.mark -> level
-val pred: level -> level
+val is_zero: level -> bool
val minus: level -> int -> level
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module E = Entity
+type mark = int
-let location = ref 0
+let mark = ref 1
(* interface functions ******************************************************)
-let locations () = !location
-
-let new_location () =
- incr location; !location
+let marks () = !mark
let new_mark () =
- E.Mark (new_location ())
+ incr mark; !mark
+
+let to_string i = string_of_int i
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-val locations: unit -> int
+type mark
-val new_location: unit -> int
+val marks: unit -> int
-val new_mark: unit -> Entity.attr
+val new_mark: unit -> mark
+
+val to_string: mark -> string
type status = {
delta: bool; (* global delta-expansion *)
si: bool; (* sort inclusion *)
- cc: Q.csys; (* conversion constraints *)
+(* cc: Q.csys; (* conversion constraints *) *)
}
(* helpers ******************************************************************)
let initial_status () = {
delta = false;
- si = !G.si; cc = Q.init ()
+ si = !G.si; (* cc = Q.init () *)
}
let refresh_status st = {st with
- si = !G.si; cc = Q.init ()
+ si = !G.si; (* cc = Q.init () *)
}
type uri = E.uri
type id = E.id
-type attrs = E.attrs
+type attrs = E.node_attrs
type bind = Abst of N.level * term (* level, type *)
| Abbr of term (* body *)
| ESort -> err ()
| EAppl (tl, _, _) -> aux i tl
| EBind (tl, a, _) ->
- let f id0 _ = if id0 = id then f i else aux (succ i) tl in
+ let f id0 _ = if id0 = id then f a i else aux (succ i) tl in
E.name err f a
| EProj (tl, _, d) -> append (aux i) tl d
in
let err i = get_name err f i tl in
get_name err f i e
-(*
-let push2 err f lenv ?attr ?t () = match lenv, attr, t with
- | EBind (e, a, Abst (n, ws)), Some attr, Some t ->
- f (EBind (e, (attr :: a), Abst (n, t :: ws)))
- | EBind (e, a, Abst (n, ws)), None, Some t ->
- f (EBind (e, a, Abst (n, t :: ws)))
- | EBind (e, a, Abbr vs), Some attr, Some t ->
- f (EBind (e, (attr :: a), Abbr (t :: vs)))
- | EBind (e, a, Abbr vs), None, Some t ->
- f (EBind (e, a, Abbr (t :: vs)))
- | EBind (e, a, Void n), Some attr, None ->
- f (EBind (e, (attr :: a), Void (succ n)))
- | EBind (e, a, Void n), None, None ->
- f (EBind (e, a, Void (succ n)))
- | _ -> err ()
-
-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 E.count_names a > j then f (k + j) else err i
- | EBind (tl, a, _) ->
- aux f (pred i) (k + E.count_names a) tl
- | EProj (tl, _, d) -> aux f i k (eshift C.start tl d)
- in
- aux f i 0 lenv
-*)
-let rec names_of_lenv ns = function
- | ESort -> ns
- | EBind (tl, a, _) -> names_of_lenv (E.rev_append_names ns a) tl
- | EAppl (tl, _, _) -> names_of_lenv ns tl
- | EProj (tl, _, e) -> names_of_lenv (names_of_lenv ns e) tl
-
let rec get e i = match e with
- | ESort -> ESort, [], Void
+ | ESort -> ESort, E.empty_node, Void
| EBind (e, a, b) when i = 0 -> e, a, b
| EBind (e, _, _) -> get e (pred i)
| EAppl (e, _, _) -> get e i
| EBind (e, _, Abst _), _ :: tl -> sub_list_strict f e tl
| _ -> assert false
-let rec fold_attrs f map a0 = function
- | ESort -> f a0
- | EBind (e, a, Abst _) -> fold_attrs f map (map a0 a) e
- | _ -> assert false
+let rec fold_names f map x = function
+ | ESort -> f x
+ | EBind (e, {E.n_name = Some n}, Abst _) -> fold_names f map (map x n) e
+ | _ -> assert false
+
+let rec mem err f e b = match e with
+ | ESort -> err ()
+ | EBind (e, a, _) ->
+ if a.E.n_name = b.E.n_name then f () else mem err f e b
+ | EAppl (e, _, _) -> mem err f e b
+ | EProj (e, _, d) ->
+ let err () = mem err f e b in mem err f d b
module U = NUri
module C = Cps
module L = Log
-module E = Entity
+module J = Marks
module N = Level
+module E = Entity
module D = Crg
(* nodes count **************************************************************)
D.push_bind (f c) a b e
let count_entity f c = function
- | _, u, E.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 D.ESort w
- | _, _, E.Abbr v ->
+ | _, _, _, E.Abbr v ->
let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in
count_term f c D.ESort v
- | _, _, E.Void -> assert false
+ | _, _, _, E.Void -> assert false
let print_counters f c =
let terms =
in
let items = c.eabsts + c.eabbrs in
let nodes = c.nodes + c.xnodes in
+ let marks = J.marks () in
L.warn level (P.sprintf "Intermediate representation summary (complete_rg)");
L.warn level (P.sprintf " Total entry items: %7u" items);
L.warn level (P.sprintf " Declaration items: %7u" c.eabsts);
L.warn level (P.sprintf " Application items: %7u" c.tappls);
L.warn level (P.sprintf " Abstraction items: %7u" c.tabsts);
L.warn level (P.sprintf " Abbreviation items: %7u" c.tabbrs);
+ L.warn level (P.sprintf " Ambiguous abstractions: %7u" marks);
L.warn level (P.sprintf " Global Int. Complexity: %7u" c.nodes);
L.warn level (P.sprintf " + Abbreviation nodes: %7u" nodes);
f ()
(* term/environment pretty printer ******************************************)
let pp_attrs out a =
- let map = function
- | 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 _ -> ()
- | E.Info _ -> ()
- in
- List.iter map a
+ let f s b = if b then out (P.sprintf "%s;" s) else out (P.sprintf "~%s;" s) in
+ E.name ignore f a;
+ let f i = out (P.sprintf "+%i;" i) in
+ E.apix ignore f a
let rec pp_term out = function
| D.TSort (a, l) -> pp_attrs out a; out (P.sprintf "*%u" l)
and pp_bind out = function
| D.Abst (n, x) ->
- out "[:"; pp_term out x; out "]";
- if N.is_infinite n then () else out (N.to_string n)
+ out "[:"; pp_term out x; out "]"; out (N.to_string n)
| D.Abbr x -> out "[="; pp_term out x; out "]";
| D.Void -> out "[]"
module L = Log
module Y = Time (**)
+module J = Marks (**)
module H = Hierarchy
module N = Level
module E = Entity
module G = Options
module O = Output
-module J = Marks (**)
module R = Alpha
module Q = Ccs
module S = Status
let henv = Hashtbl.create henv_size (* optimized global environment *)
(* Internal functions *******************************************************)
-
-let name_of_id ?(r=true) id = E.Name (id, r)
(*
+let name_of_id ?(r=true) id = E.Name (id, r)
+
let mk_lref f i j k = f (D.TLRef ([E.Apix k], i, j))
let mk_gref f uri = f (D.TGRef ([], uri))
| _, entity -> entity
let pp_progress e =
- let f a u =
+ let f _ na u =
let s = U.string_of_uri u in
let err () = L.warn 2 (P.sprintf "<%s>" s) in
let f i = L.warn 2 (P.sprintf "[%u] <%s>" i s) in
- E.apix err f a
+ E.apix err f na
in
match e with
| CrgEntity e -> E.common f e
let lexbuf = Lexing.from_channel ich in
let st = process st lexbuf input in
close_in ich;
- if !G.cc then XL.export_csys st.kst.S.cc;
+(* if !G.cc then XL.export_csys st.kst.S.cc; *)
st, input
let main =
module U = NUri
module C = Cps
module H = Hierarchy
-module Y = Entity
+module E = Entity
module R = Alpha
module XL = XmlLibrary
module D = Crg
| D.ESort -> e
| D.EBind (e, a, b) ->
let e = aux e in
+(* NOTE: the inner binders are alpha-converted first *)
+ let a = R.alpha D.mem e a in
map_bind e a b out tab; D.EBind (e, a, b)
| D.EAppl (e, a, v) ->
let e = aux e in
| D.TSort (a, l) ->
let a =
let err _ = a in
- let f s = Y.Name (s, true) :: a in
+ let f s = {a with E.n_name = Some (s, true)} in
H.string_of_sort err f l
in
let attrs = [XL.position l; XL.name a] in
| D.TLRef (a, i) ->
let a =
let err _ = a in
- let f n r = Y.Name (n, r) :: a in
+ let f n r = {a with E.n_name = Some (n, r)} in
D.get_name err f i e
in
let attrs = [XL.position i; 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 a = {a with E.n_name = Some (U.name_of_uri n, true)} in
let attrs = [XL.uri n; XL.name a; XL.apix a] in
XL.tag XL.gref attrs out tab
| D.TCast (a, u, t) ->
exp_term (D.push_proj C.start a lenv e) t out tab
| D.TBind (a, b, t) ->
(* NOTE: the inner binders are alpha-converted first *)
- let a = R.alpha (D.names_of_lenv [] e) a in
+ let a = R.alpha D.mem e a in
exp_bind e a b out tab;
exp_term (D.push_bind C.start a b e) t out tab
and exp_bind e a b out tab = match b with
| D.Abst (n, w) ->
- let attrs = [XL.level n; XL.name a; XL.mark a] in
+ let attrs = [XL.level n; XL.name a] in
XL.tag XL.abst attrs ~contents:(exp_term e w) out tab
| D.Abbr v ->
let attrs = [XL.name a] in
"uri", U.string_of_uri u
let name a =
- let map f i n r s =
- 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
- E.names f map a ""
+ let err () = "name", "" in
+ let f n r = "name", if r then n else "-" ^ n in
+ E.name err f a
let apix a =
let err () = "age", "" in
let f i = "age", string_of_int i in
E.apix err f a
-let mark a =
- let err () = "mark", "" in
- let f i = "mark", string_of_int i in
- E.mark err f a
-
let level n =
"level", N.to_string n
| E.Progress -> "Progress"
| E.Private -> "Private"
in
- let err () = "meta", "" in
- let f ms = "meta", String.concat " " (List.rev_map map ms) in
- E.meta err f a
+ "meta", String.concat " " (List.rev_map map a.E.r_meta)
let arity l =
"arity", string_of_int (List.length l)
let f lg tx = ["lang", lg; "info", tx] in
E.info err f a
-let export_entity pp_term (a, u, b) =
+let export_entity pp_term (ra, na, u, b) =
let path = path_of_uri !G.xdir u in
let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in
let och = open_out (path ^ ext) in
let out = output_string och in
xml out "1.0" "UTF-8"; doctype out obj_root system;
- let a = E.Name (U.name_of_uri u, true) :: a in
- let attrs = uri u :: name a :: apix a :: meta a :: info a in
+ let na = {na with E.n_name = Some (U.name_of_uri u, true)} in
+ let attrs = uri u :: name na :: apix na :: meta ra :: info ra in
let contents = match b with
- | E.Abst (n, w) -> tag "GDec" (level n :: attrs) ~contents:(pp_term w)
- | E.Abbr v -> tag "GDef" attrs ~contents:(pp_term v)
- | E.Void -> assert false
+ | E.Abst w -> tag "GDec" attrs ~contents:(pp_term w)
+ | E.Abbr v -> tag "GDef" attrs ~contents:(pp_term v)
+ | E.Void -> assert false
in
let opts = if !G.si then "si" else "" in
let shp = H.string_of_graph () in
let nexts = function
| [] -> "next", ""
| l -> "next", String.concat " " (List.rev_map next_map l)
-
+(*
let export_csys s =
let path = path_of_uri !G.xdir s.Q.buri in
let _ = Sys.command (Printf.sprintf "mkdir -p %s" path) in
in
tag ccs_root attrs ~contents out 0;
close_out och
+*)
type pp = och -> int -> unit
val export_entity: ('term -> pp) -> 'term Entity.entity -> unit
-
+(*
val export_csys: Ccs.csys -> unit
-
+*)
val tag: string -> attr list -> ?contents:pp -> pp
val sort: string
val level: Level.level -> attr
-val name: Entity.attrs -> attr
-
-val apix: Entity.attrs -> attr
+val name: Entity.node_attrs -> attr
-val mark: Entity.attrs -> attr
+val apix: Entity.node_attrs -> attr
-val meta: Entity.attrs -> attr
+val meta: Entity.root_attrs -> attr
-val info: Entity.attrs -> attr list
+val info: Entity.root_attrs -> attr list
projects / helm.git / commitdiff