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/common/entity.cmx: src/common/options.cmx
+src/common/level.cmi:
+src/common/level.cmo: src/common/level.cmi
+src/common/level.cmx: src/common/level.cmi
+src/common/entity.cmo: src/common/options.cmx src/common/level.cmi
+src/common/entity.cmx: src/common/options.cmx src/common/level.cmx
src/common/marks.cmo: src/common/entity.cmx
src/common/marks.cmx: src/common/entity.cmx
src/common/alpha.cmi: src/common/entity.cmx
src/common/alpha.cmo: src/common/entity.cmx src/common/alpha.cmi
src/common/alpha.cmx: src/common/entity.cmx src/common/alpha.cmi
-src/text/txt.cmo:
-src/text/txt.cmx:
+src/text/txt.cmo: src/common/level.cmi
+src/text/txt.cmx: src/common/level.cmx
src/text/txtParser.cmi: src/text/txt.cmx
src/text/txtParser.cmo: src/text/txt.cmx src/common/options.cmx \
- src/text/txtParser.cmi
+ src/common/level.cmi src/text/txtParser.cmi
src/text/txtParser.cmx: src/text/txt.cmx src/common/options.cmx \
- src/text/txtParser.cmi
+ src/common/level.cmx src/text/txtParser.cmi
src/text/txtLexer.cmo: src/text/txtParser.cmi src/common/options.cmx \
src/lib/log.cmi
src/text/txtLexer.cmx: src/text/txtParser.cmx src/common/options.cmx \
src/basic_ag/bagUntrusted.cmx: src/lib/log.cmx src/common/entity.cmx \
src/basic_ag/bagType.cmx src/basic_ag/bagEnvironment.cmx \
src/basic_ag/bag.cmx src/basic_ag/bagUntrusted.cmi
-src/complete_rg/crg.cmo: src/common/entity.cmx
-src/complete_rg/crg.cmx: src/common/entity.cmx
+src/complete_rg/crg.cmo: src/common/level.cmi src/common/entity.cmx
+src/complete_rg/crg.cmx: src/common/level.cmx src/common/entity.cmx
src/complete_rg/crgOutput.cmi: src/complete_rg/crg.cmx
-src/complete_rg/crgOutput.cmo: src/common/hierarchy.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/hierarchy.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/level.cmi src/common/hierarchy.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/level.cmx src/common/hierarchy.cmx \
+ src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
+ src/complete_rg/crgOutput.cmi
src/complete_rg/crgTxt.cmi: src/text/txt.cmx src/complete_rg/crg.cmx
src/complete_rg/crgTxt.cmo: src/text/txtTxt.cmi src/text/txt.cmx \
src/common/options.cmx src/common/hierarchy.cmi src/common/entity.cmx \
src/common/options.cmx src/common/hierarchy.cmx src/common/entity.cmx \
src/complete_rg/crg.cmx src/lib/cps.cmx src/complete_rg/crgTxt.cmi
src/complete_rg/crgAut.cmi: src/complete_rg/crg.cmx src/automath/aut.cmx
-src/complete_rg/crgAut.cmo: src/common/options.cmx src/common/entity.cmx \
- src/complete_rg/crg.cmx src/lib/cps.cmx src/automath/aut.cmx \
- src/complete_rg/crgAut.cmi
-src/complete_rg/crgAut.cmx: src/common/options.cmx src/common/entity.cmx \
- src/complete_rg/crg.cmx src/lib/cps.cmx src/automath/aut.cmx \
- src/complete_rg/crgAut.cmi
-src/xml/xmlLibrary.cmi: src/common/entity.cmx
-src/xml/xmlLibrary.cmo: src/common/hierarchy.cmi src/common/entity.cmx \
- src/lib/cps.cmx src/xml/xmlLibrary.cmi
-src/xml/xmlLibrary.cmx: src/common/hierarchy.cmx src/common/entity.cmx \
- src/lib/cps.cmx src/xml/xmlLibrary.cmi
+src/complete_rg/crgAut.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/complete_rg/crgAut.cmi
+src/complete_rg/crgAut.cmx: src/common/options.cmx src/common/level.cmx \
+ src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
+ src/automath/aut.cmx src/complete_rg/crgAut.cmi
+src/xml/xmlLibrary.cmi: src/common/level.cmi src/common/entity.cmx
+src/xml/xmlLibrary.cmo: src/common/level.cmi src/common/hierarchy.cmi \
+ src/common/entity.cmx src/lib/cps.cmx src/xml/xmlLibrary.cmi
+src/xml/xmlLibrary.cmx: src/common/level.cmx src/common/hierarchy.cmx \
+ src/common/entity.cmx src/lib/cps.cmx src/xml/xmlLibrary.cmi
src/xml/xmlCrg.cmi: src/xml/xmlLibrary.cmi src/complete_rg/crg.cmx
src/xml/xmlCrg.cmo: src/xml/xmlLibrary.cmi src/common/hierarchy.cmi \
src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
src/xml/xmlCrg.cmx: src/xml/xmlLibrary.cmx src/common/hierarchy.cmx \
src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
src/common/alpha.cmx src/xml/xmlCrg.cmi
-src/basic_rg/brg.cmo: src/common/entity.cmx
-src/basic_rg/brg.cmx: src/common/entity.cmx
+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.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.cmx: src/common/marks.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/marks.cmx 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/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/lib/log.cmi src/common/hierarchy.cmi src/common/entity.cmx \
- src/lib/cps.cmx src/basic_rg/brgCrg.cmi src/basic_rg/brg.cmx \
- src/basic_rg/brgOutput.cmi
+ src/lib/log.cmi src/common/level.cmi src/common/hierarchy.cmi \
+ src/common/entity.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/brgCrg.cmx src/basic_rg/brg.cmx \
- src/basic_rg/brgOutput.cmi
+ src/lib/log.cmx src/common/level.cmx src/common/hierarchy.cmx \
+ src/common/entity.cmx 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.cmi: src/lib/log.cmi src/common/entity.cmx \
src/basic_rg/brgReduction.cmi src/basic_rg/brg.cmx
src/basic_rg/brgType.cmo: src/lib/share.cmx src/lib/log.cmi \
- src/common/hierarchy.cmi src/common/entity.cmx src/lib/cps.cmx \
- src/basic_rg/brgSubstitution.cmi src/basic_rg/brgReduction.cmi \
- src/basic_rg/brgEnvironment.cmi src/basic_rg/brg.cmx \
- src/basic_rg/brgType.cmi
+ src/common/level.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/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/brgEnvironment.cmx src/basic_rg/brg.cmx \
- src/basic_rg/brgType.cmi
+ src/common/level.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/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 \
src/common/entity.cmx src/lib/cps.cmx src/toplevel/metaOutput.cmi
src/toplevel/metaAut.cmi: src/toplevel/meta.cmx src/automath/aut.cmx
src/toplevel/metaAut.cmo: src/common/options.cmx src/toplevel/meta.cmx \
- src/common/entity.cmx src/lib/cps.cmx src/automath/aut.cmx \
- src/toplevel/metaAut.cmi
+ src/common/level.cmi src/common/entity.cmx src/lib/cps.cmx \
+ src/automath/aut.cmx src/toplevel/metaAut.cmi
src/toplevel/metaAut.cmx: src/common/options.cmx src/toplevel/meta.cmx \
- src/common/entity.cmx src/lib/cps.cmx src/automath/aut.cmx \
- src/toplevel/metaAut.cmi
+ src/common/level.cmx src/common/entity.cmx src/lib/cps.cmx \
+ src/automath/aut.cmx src/toplevel/metaAut.cmi
src/toplevel/metaBag.cmi: src/toplevel/meta.cmx src/basic_ag/bag.cmx
src/toplevel/metaBag.cmo: src/toplevel/meta.cmx src/lib/cps.cmx \
src/basic_ag/bag.cmx src/toplevel/metaBag.cmi
src/toplevel/metaBag.cmx: src/toplevel/meta.cmx src/lib/cps.cmx \
src/basic_ag/bag.cmx src/toplevel/metaBag.cmi
src/toplevel/metaBrg.cmi: src/toplevel/meta.cmx src/basic_rg/brg.cmx
-src/toplevel/metaBrg.cmo: src/toplevel/meta.cmx src/common/entity.cmx \
- src/lib/cps.cmx src/basic_rg/brg.cmx src/toplevel/metaBrg.cmi
-src/toplevel/metaBrg.cmx: src/toplevel/meta.cmx src/common/entity.cmx \
- src/lib/cps.cmx src/basic_rg/brg.cmx src/toplevel/metaBrg.cmi
+src/toplevel/metaBrg.cmo: src/toplevel/meta.cmx src/common/level.cmi \
+ src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \
+ src/toplevel/metaBrg.cmi
+src/toplevel/metaBrg.cmx: src/toplevel/meta.cmx src/common/level.cmx \
+ src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \
+ src/toplevel/metaBrg.cmi
src/toplevel/top.cmo: src/xml/xmlLibrary.cmi src/xml/xmlCrg.cmi \
src/text/txtParser.cmi src/text/txtLexer.cmx src/text/txt.cmx \
src/lib/time.cmx src/common/output.cmi src/common/options.cmx \
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 =
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
Z.get f c i
| Z.GRef uri ->
let f = function
- | _, _, E.Abst w -> f x w
+ | _, _, E.Abst (_, w) -> f x w
| _, _, E.Abbr (Z.Cast (w, v)) -> f x w
| _, _, E.Abbr _ -> assert false
| _, _, E.Void -> assert false
(* to share *)
let type_check f st = function
- | a, uri, E.Abst t ->
- let f xt tt = ZE.set_entity (f tt) (a, uri, E.Abst xt) in
+ | a, uri, E.Abst (n, t) ->
+ let f xt tt = ZE.set_entity (f tt) (a, uri, E.Abst (n, xt)) in
L.loc := U.string_of_uri uri; ZT.type_of f st Z.empty_lenv t
- | a, uri, E.Abbr 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
+ | _, _, E.Void -> assert false
(* note : ufficial basic lambda-delta *)
module E = Entity
+module N = Level
type uri = E.uri
type id = E.id
type attrs = E.attrs
-type bind = Void (* *)
- | Abst of term (* type *)
- | Abbr of term (* body *)
+type bind = Void (* *)
+ | Abst of N.level * term (* level, type *)
+ | Abbr of term (* body *)
and term = Sort of attrs * int (* attrs, hierarchy index *)
| LRef of attrs * int (* attrs, position index *)
(* Currified constructors ***************************************************)
-let abst w = Abst w
+let abst n w = Abst (n, w)
let abbr v = Abbr v
let bind a b t = Bind (a, b, t)
-let bind_abst a u t = Bind (a, Abst u, t)
+let bind_abst n a u t = Bind (a, Abst (n, u), t)
let bind_abbr a v t = Bind (a, Abbr v, t)
module C = Cps
module E = Entity
module J = Marks
+module N = Level
module D = Crg
module B = Brg
| D.TProj (a, e, t) ->
let f tt = f (lenv_fold_left xlate_bind xlate_proj tt e) in
xlate_term f t
- | D.TBind (ab, D.Abst ws, D.TCast (ac, u, t)) ->
- xlate_term f (D.TCast (ac, D.TBind (ab, D.Abst ws, u), D.TBind (ab, D.Abst ws, t)))
+ | D.TBind (ab, D.Abst (n, ws), D.TCast (ac, u, t)) ->
+ xlate_term f (D.TCast (ac, D.TBind (ab, D.Abst (N.pred n, ws), u), D.TBind (ab, D.Abst (n, ws), t)))
| D.TBind (a, b, t) ->
let f tt = f (xlate_bind tt a b) in xlate_term f t
let f a ns = a, ns in
let a, ns = E.get_names f a in
match b with
- | D.Abst ws ->
+ | D.Abst (m, ws) ->
let map x n w =
- let f ww = B.Bind (n :: J.new_mark () :: a, B.Abst ww, x) in
+ let f ww = B.Bind (n :: J.new_mark () :: a, B.Abst (m, ww), x) in
xlate_term f w
in
List.fold_left2 map x ns ws
- | D.Abbr vs ->
+ | D.Abbr vs ->
let map x n v =
let f vv = B.Bind (n :: a, B.Abbr vv, x) in
xlate_term f v
in
List.fold_left2 map x ns vs
- | D.Void _ ->
+ | D.Void _ ->
let map x n = B.Bind (n :: a, B.Void, x) in
List.fold_left map x ns
xlate_bk_bind f b
and xlate_bk_bind f = function
- | B.Abst t ->
- let f tt = f (D.Abst [tt]) in
+ | B.Abst (n, t) ->
+ let f tt = f (D.Abst (n, [tt])) in
xlate_bk_term f t
- | B.Abbr t ->
+ | B.Abbr t ->
let f tt = f (D.Abbr [tt]) in
xlate_bk_term f t
- | B.Void -> f (D.Void 1)
+ | B.Void -> f (D.Void 1)
(* interface functions ******************************************************)
module G = Options
module E = Entity
module H = Hierarchy
+module N = Level
module XD = XmlCrg
module B = Brg
module BD = BrgCrg
}
let rec count_term_binder f c e = function
- | B.Abst w ->
+ | B.Abst (_, w) ->
let c = {c with tabsts = succ c.tabsts; nodes = succ c.nodes} in
count_term f c e w
- | B.Abbr v ->
+ | B.Abbr v ->
let c = {c with tabbrs = succ c.tabbrs; xnodes = succ c.xnodes} in
count_term f c e v
- | B.Void ->
+ | B.Void ->
let c = {c with tvoids = succ c.tvoids; xnodes = succ c.xnodes} in
f c
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 =
let name err frm a =
let f n = function
| true -> F.fprintf frm "%s" n
- | false -> F.fprintf frm "^%s" n
+ | false -> F.fprintf frm "-%s" n
in
E.name err f a
+let pp_level frm n =
+ if N.is_infinite n then () else F.fprintf frm "^%s" (N.to_string n)
+
let rec pp_term e frm = function
| B.Sort (_, h) ->
let err _ = F.fprintf frm "@[*%u@]" h in
F.fprintf frm "@[{%a}.%a@]" (pp_term e) u (pp_term e) t
| B.Appl (_, v, t) ->
F.fprintf frm "@[(%a).%a@]" (pp_term e) v (pp_term e) t
- | B.Bind (a, B.Abst w, t) ->
+ | B.Bind (a, B.Abst (n, w), t) ->
let f a =
- let ee = B.push e B.empty a (B.abst w) in
- F.fprintf frm "@[[%a:%a].%a@]" (name C.err) a (pp_term e) w (pp_term ee) t
+ let ee = B.push e B.empty a (B.abst n w) in
+ F.fprintf frm "@[[%a:%a]%a.%a@]" (name C.err) a (pp_term e) w pp_level n (pp_term ee) t
in
rename f e a
| B.Bind (a, B.Abbr v, t) ->
aux_bind f (b1, b2)
| _ -> err ()
and aux_bind f = function
- | B.Abbr v1, B.Abbr v2
- | B.Abst v1, B.Abst v2 -> aux f (v1, v2)
- | B.Void, B.Void -> f ()
- | _ -> err ()
+ | B.Abbr v1, B.Abbr v2 -> aux f (v1, v2)
+ | B.Abst (n1, v1), B.Abst (n2, v2) when n1 = n2 -> aux f (v1, v2)
+ | B.Void, B.Void -> f ()
+ | _ -> err ()
in
if S.eq t1 t2 then f () else aux f (t1, t2)
let rec step st m x =
(* L.warn "entering R.step"; *)
match x with
- | B.Sort _ -> m, None, x
- | B.GRef (_, uri) ->
+ | B.Sort _ -> m, None, x
+ | B.GRef (_, uri) ->
begin match BE.get_entity uri with
- | _, _, E.Abbr v when st.E.delta ->
+ | _, _, E.Abbr v when st.E.delta ->
O.add ~gdelta:1 (); step st m v
- | _, _, E.Abst w when st.E.rt ->
+ | _, _, E.Abst (_, w) when st.E.rt ->
O.add ~grt:1 (); step st m w
- | a, _, E.Abbr v ->
+ | a, _, E.Abbr v ->
let e = E.apix C.err C.start a in
m, Some (e, a, B.Abbr v), x
- | a, _, E.Abst w ->
+ | a, _, E.Abst (n, w) ->
let e = E.apix C.err C.start a in
- m, Some (e, a, B.Abst w), x
- | _, _, E.Void -> assert false
+ m, Some (e, a, B.Abst (n, w)), x
+ | _, _, E.Void -> assert false
end
- | B.LRef (_, i) ->
+ | B.LRef (_, i) ->
begin match get m i with
- | c, _, B.Abbr v ->
+ | c, _, B.Abbr v ->
O.add ~ldelta:1 ();
step st {m with e = c} v
- | c, _, B.Abst w when st.E.rt ->
+ | c, _, B.Abst (_, w) when st.E.rt ->
O.add ~lrt:1 ();
step st {m with e = c} w
- | c, _, B.Void ->
+ | c, _, B.Void ->
assert false
- | c, a, (B.Abst _ as b) ->
+ | c, a, (B.Abst _ as b) ->
let e = E.apix C.err C.start a in
{m with e = c}, Some (e, a, b), x
end
- | B.Cast (_, _, t) ->
+ | B.Cast (_, _, t) ->
O.add ~tau:1 ();
step st m t
- | B.Appl (_, v, t) ->
+ | B.Appl (_, v, t) ->
step st {m with s = (m.e, v) :: m.s} t
- | B.Bind (a, B.Abst w, t) ->
+ | B.Bind (a, B.Abst (n, w), t) ->
begin match m.s with
| [] -> m, None, x
| (c, v) :: s ->
| Some (_, _, B.Abbr v1), _, _, _ ->
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 E.si = false} m1 w1 m2 w2 then
+ | _, B.Bind (a1, (B.Abst (n1, w1) as b1), t1),
+ _, B.Bind (a2, (B.Abst (n2, w2) as b2), t2) ->
+ if (* n1 = n2 && *) ac {st with E.si = false} m1 w1 m2 w2 then
ac st (push m1 a1 b1) t1 (push m2 a2 b2) t2
else false
| _, B.Sort _, _, B.Bind (a, b, t) when st.E.si ->
let rec icm a = function
| B.Sort _
| B.LRef _
- | B.GRef _ -> succ a
- | B.Bind (_, B.Void, t) -> icm (succ a) t
- | B.Cast (_, u, t) -> icm (icm a u) t
+ | B.GRef _ -> succ a
+ | B.Bind (_, B.Void, t) -> icm (succ a) t
+ | B.Cast (_, u, t) -> icm (icm a u) t
| B.Appl (_, u, t)
- | B.Bind (_, B.Abst u, t)
- | B.Bind (_, B.Abbr u, t) -> icm (icm (succ a) u) t
+ | B.Bind (_, B.Abst (_, u), t)
+ | B.Bind (_, B.Abbr u, t) -> icm (icm (succ a) u) t
let iter map d =
let rec iter_bind d = function
- | B.Void -> B.Void
- | B.Abst w -> B.Abst (iter_term d w)
- | B.Abbr v -> B.Abbr (iter_term d v)
+ | B.Void -> B.Void
+ | B.Abst (n, w) -> B.Abst (n, iter_term d w)
+ | B.Abbr v -> B.Abbr (iter_term d v)
and iter_term d = function
| B.Sort _ as t -> t
| B.GRef _ as t -> t
module L = Log
module H = Hierarchy
module E = Entity
+module N = Level
module B = Brg
module BE = BrgEnvironment
module BS = BrgSubstitution
let assert_applicability err f st m u w v =
match BR.xwhd st m u with
- | _, B.Sort _ -> error1 err "not a function type" m u
- | mu, B.Bind (_, B.Abst u, _) ->
+ | _, B.Sort _ ->
+ error1 err "not a function type" m u
+ | mu, B.Bind (_, B.Abst (_, u), _) ->
if BR.are_convertible st mu u m w then f () else
error3 err m v w ~mu u
- | _ -> assert false (**)
+ | _ -> assert false (**)
let rec b_type_of err f st m x =
log1 "Now checking" m x;
let h = H.apply h in f x (B.Sort (a, h))
| B.LRef (_, i) ->
begin match BR.get m i with
- | B.Abst w ->
+ | B.Abst (_, w) ->
f x (BS.lift (succ i) (0) w)
| B.Abbr (B.Cast (_, w, _)) ->
f x (BS.lift (succ i) (0) w)
end
| B.GRef (_, uri) ->
begin match BE.get_entity uri with
- | _, _, E.Abst w -> f x w
+ | _, _, E.Abst (_, w) -> f x w
| _, _, E.Abbr (B.Cast (_, w, _)) -> f x w
| _, _, E.Abbr _ -> assert false
| _, _, E.Void ->
| _ -> f (B.Cast ([], vv, xv))
in
type_of err f st m v
- | B.Bind (a, B.Abst u, t) ->
+ | B.Bind (a, B.Abst (n, u), t) ->
let f xu xt tt =
- f (S.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 n a)) (B.bind_abst (N.pred n) a xu tt)
in
let f xu m = b_type_of err (f xu) st m t in
- let f xu _ = f xu (BR.push m a (B.abst xu)) in
+ let f xu _ = f xu (BR.push m a (B.abst n xu)) in
type_of err f st m u
| B.Bind (a, B.Void, t) ->
let f xt tt =
(* to share *)
let type_check err f st = function
- | a, uri, E.Abst t ->
+ | a, uri, E.Abst (n, t) ->
let f xt tt =
- let e = BE.set_entity (a, uri, E.Abst xt) in f tt e
+ let e = BE.set_entity (a, uri, E.Abst (n, xt)) in f tt e
in
L.loc := U.string_of_uri uri; BT.type_of err f st BR.empty_kam t
- | a, uri, E.Abbr t ->
+ | a, uri, E.Abbr t ->
let f xt tt =
let xt = match xt with
| B.Cast _ -> xt
let e = BE.set_entity (a, uri, E.Abbr xt) in f tt e
in
L.loc := U.string_of_uri uri; BT.type_of err f st BR.empty_kam t
- | _, _, E.Void -> assert false
+ | _, _, E.Void -> assert false
-options hierarchy output entity marks alpha
+options hierarchy output level entity marks alpha
module U = NUri
module G = Options
+module N = Level
type uri = U.uri
type attrs = attr list (* attributes *)
-type 'term bind = Abst of 'term (* declaration: domain *)
- | Abbr of 'term (* definition: body *)
- | Void (* exclusion *)
+type 'term bind = Abst of N.level * 'term (* declaration: level, domain *)
+ | Abbr of 'term (* definition: body *)
+ | Void (* exclusion *)
type 'term entity = attrs * uri * 'term bind (* attrs, name, binder *)
| _ :: tl -> rev_append_names ns tl
let xlate f xlate_term = function
- | a, uri, Abst t ->
- let f t = f (a, uri, Abst t) in xlate_term f t
- | a, uri, Abbr t ->
+ | 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 ->
+ | _, _, Void ->
assert false
let initial_status () = {
(* note : fragment of complete lambda-delta serving as abstract layer *)
module E = Entity
+module N = Level
type uri = E.uri
type id = E.id
type attrs = E.attrs
-type bind = Abst of term list (* domains *)
- | Abbr of term list (* bodies *)
- | Void of int (* number of exclusions *)
+type bind = Abst of N.level * term list (* level, domains *)
+ | Abbr of term list (* bodies *)
+ | Void of int (* number of exclusions *)
and term = TSort of attrs * int (* attrs, hierarchy index *)
| TLRef of attrs * int * int (* attrs, position indexes *)
let push_proj f lenv a e = f (EProj (lenv, a, e))
let push2 err f lenv attr ?t () = match lenv, t with
- | EBind (e, a, Abst ws), Some t -> f (EBind (e, (attr :: a), Abst (t :: ws)))
- | EBind (e, a, Abbr vs), Some t -> f (EBind (e, (attr :: a), Abbr (t :: vs)))
- | EBind (e, a, Void n), None -> f (EBind (e, (attr :: a), Void (succ n)))
+ | EBind (e, a, Abst (n, ws)), Some t ->
+ f (EBind (e, (attr :: a), Abst (n, t :: ws)))
+ | EBind (e, a, Abbr vs), Some t ->
+ f (EBind (e, (attr :: a), Abbr (t :: vs)))
+ | EBind (e, a, Void n), None ->
+ f (EBind (e, (attr :: a), Void (succ n)))
| _ -> err ()
(* this id not tail recursive *)
let resolve_lref err f id lenv =
let rec aux f i k = function
| ESort -> err ()
- | EBind (tl, _, Abst [])
+ | 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
+ | EBind (tl, a, b) ->
+ let err kk = aux f (succ i) (k + kk) tl in
let f j = f i j (k + j) in
E.resolve err f id a
| EProj _ -> assert false (* TODO *)
let rec get_name err f i j = function
| ESort -> err i
- | EBind (tl, _, Abst [])
+ | EBind (tl, _, Abst (_, []))
| EBind (tl, _, Abbr [])
| EBind (tl, _, Void 0) -> get_name err f i j tl
| EBind (_, a, _) when i = 0 ->
let get_index err f i j lenv =
let rec aux f i k = function
| ESort -> err i
- | EBind (tl, _, Abst [])
+ | EBind (tl, _, Abst (_, []))
| EBind (tl, _, Abbr [])
| EBind (tl, _, Void 0) -> aux f i k tl
| EBind (_, a, _) when i = 0 ->
module C = Cps
module G = Options
module E = Entity
+module N = Level
module A = Aut
module D = Crg
(* Internal functions *******************************************************)
-let empty_cnt = [], []
+let empty_cnt = [], [], []
-let add_abst (a, ws) id w =
- E.Name (id, true) :: a, w :: ws
+let add_abst (a, ws, ns) id w n =
+ E.Name (id, true) :: a, w :: ws, N.succ n :: ns
-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 ([E.Apix k], i, j))
+let mk_lref f n i j k = f n (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 = K.find henv (uri_of_qid qid) in f qid cnt
+ try let n, cnt = K.find henv (uri_of_qid qid) in f n qid cnt
with Not_found -> err qid
let resolve_gref_relaxed f st qid =
resolve_gref err f st qid
let get_cnt err f st = function
- | None -> f empty_cnt
+ | None -> f empty_cnt
| Some qid as node ->
try let cnt = K.find hcnt (uri_of_qid qid) in f cnt
with Not_found -> err node
let rec err node = relax_opt_qid (get_cnt err f st) st node in
get_cnt err f st st.node
+(****************************************************************************)
+
+let push_abst f (lenv, ns) a n w =
+ let bw = D.Abst (N.infinite, [w]) in
+ let f lenv = f (lenv, N.succ n :: ns) in
+ D.push_bind f lenv a bw
+
+let resolve_lref err f id (lenv, ns) =
+ let f i j k = f (List.nth ns k) i j k in
+ D.resolve_lref err f id lenv
+
+let lenv_of_cnt (a, ws, ns) =
+ D.push_bind C.start D.empty_lenv a (D.Abst (N.infinite, ws)), ns
+
(* 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
+ let f h = f (N.finite 0) (D.TSort ([], 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 n tt = f n (D.TAppl ([], [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, b = [E.Name (name, true)], (D.Abst [ww]) in
- let f tt = f (D.TBind (a, b, tt)) in
+ let f nw ww =
+ let a = [E.Name (name, true)] in
+ let f nt tt =
+ let b = D.Abst (nt, [ww]) in
+ f nt (D.TBind (a, b, tt))
+ in
let f lenv = xlate_term f st lenv t in
- D.push_bind f lenv a b
+ push_abst f lenv a nw ww
in
xlate_term f st lenv w
| A.GRef (name, args) ->
| E.Name (id, _) -> f (A.GRef ((id, true, []), []))
| _ -> C.err ()
in
- let map2 f = xlate_term f st lenv in
- let g qid (a, _) =
+ let map2 f t =
+ let f _ tt = f tt in xlate_term f st lenv t
+ in
+ let g n qid (a, _, _) =
let gref = D.TGRef ([], uri_of_qid qid) in
match args, a with
- | [], [] -> f gref
- | _ ->
- let f args = f (D.TAppl ([], args, gref)) in
- let f args = f (List.rev_map (map2 C.start) args) in
+ | [], [] -> f n gref
+ | _ ->
+ let f args = f n (D.TAppl ([], args, gref)) in
+ let f args = C.list_rev_map f map2 args in
let f a = C.list_rev_map_append f map1 a ~tail:args in
C.list_sub_strict f a args
in
let g qid = resolve_gref_relaxed g st qid in
let err () = complete_qid g st name in
- D.resolve_lref err (mk_lref f) (id_of_name name) lenv
+ resolve_lref err (mk_lref f) (id_of_name name) lenv
let xlate_entity err f st = function
| A.Section (Some (_, name)) ->
let f qid =
let f cnt =
let lenv = lenv_of_cnt cnt in
- let ww = xlate_term C.start st lenv w in
- K.add hcnt (uri_of_qid qid) (add_abst cnt name ww);
- err {st with node = Some qid}
+ let f nw ww =
+ K.add hcnt (uri_of_qid qid) (add_abst cnt name ww nw);
+ err {st with node = Some qid}
+ in
+ xlate_term f st lenv w
in
get_cnt_relaxed f st
in
complete_qid f st (name, true, [])
| A.Decl (name, w) ->
let f cnt =
- let a, ws = cnt in
+ let a, ws, _ = cnt in
let lenv = lenv_of_cnt cnt in
let f qid =
- let ww = xlate_term C.start st lenv w in
- K.add henv (uri_of_qid qid) cnt;
- let t = match ws with
- | [] -> ww
- | _ -> D.TBind (a, D.Abst ws, ww)
- in
+ let f nw ww =
+ K.add henv (uri_of_qid qid) (N.succ nw, cnt);
+ let t = match ws with
+ | [] -> ww
+ | _ -> D.TBind (a, D.Abst (N.infinite, ws), ww)
+ in
(*
print_newline (); CrgOutput.pp_term print_string t;
*)
- 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
+ let b = E.Abst (N.infinite, t) in
+ let entity = [E.Mark st.line], uri_of_qid qid, b in
+ f {st with line = succ st.line} entity
+ in
+ xlate_term f st lenv w
in
complete_qid f st (name, true, [])
in
get_cnt_relaxed f st
| A.Def (name, w, trans, v) ->
let f cnt =
- let a, ws = cnt in
+ let a, ws, _ = cnt in
let lenv = lenv_of_cnt cnt in
let f qid =
- let ww = xlate_term C.start st lenv w in
- let vv = xlate_term C.start st lenv v in
- 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))
- in
+ let f nw ww =
+ let f nv vv =
+ assert (nv = N.succ nw); (**)
+ K.add henv (uri_of_qid qid) (nv, cnt);
+ let t = match ws with
+ | [] -> D.TCast ([], ww, vv)
+ | _ -> D.TBind (a, D.Abst (N.infinite, ws), D.TCast ([], ww, vv))
+ in
(*
print_newline (); CrgOutput.pp_term print_string t;
*)
- 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
+ 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
+ xlate_term f st lenv v
+ in
+ xlate_term f st lenv w
in
complete_qid f st (name, true, [])
in
module C = Cps
module H = Hierarchy
module E = Entity
+module N = Level
module D = Crg
(****************************************************************************)
out bg; aux vs; out (eg ^ ".")
and pp_bind out = function
- | D.Abst x -> pp_terms "[:" "]" out x
- | D.Abbr x -> pp_terms "[=" "]" out x
- | D.Void x -> out (P.sprintf "[%u]" x)
+ | D.Abst (n, x) when N.is_infinite n -> pp_terms "[:" "]" out x
+ | D.Abst (n, x) ->
+ pp_terms "[:" (P.sprintf "]^%s" (N.to_string n)) out x
+ | D.Abbr x -> pp_terms "[=" "]" out x
+ | D.Void x -> out (P.sprintf "[%u]" x)
let rec pp_lenv out = function
| D.ESort -> ()
let rec xlate_term f st lenv = function
| T.Inst _
- | T.Impl _ -> assert false
- | T.Sort h ->
+ | T.Impl _ -> assert false
+ | T.Sort h ->
f (D.TSort ([], h))
- | T.NSrt id ->
+ | T.NSrt id ->
let f h = f (D.TSort ([], h)) in
H.sort_of_string C.err f id
- | T.LRef (i, j) ->
+ | T.LRef (i, j) ->
D.get_index C.err (mk_lref f i j) i j lenv
- | T.NRef id ->
+ | T.NRef id ->
let err () = resolve_gref C.err (mk_gref f) st id in
D.resolve_lref err (mk_lref f) id lenv
- | T.Cast (u, t) ->
+ | T.Cast (u, t) ->
let f uu tt = f (D.TCast ([], uu, tt)) in
let f uu = xlate_term (f uu) st lenv t in
xlate_term f st lenv u
- | T.Appl (vs, t) ->
+ | T.Appl (vs, t) ->
let map f = xlate_term f st lenv in
let f vvs tt = f (D.TAppl ([], vvs, tt)) in
let f vvs = xlate_term (f vvs) st lenv t in
C.list_map f map vs
- | T.Bind (b, t) ->
+ | T.Bind (n, b, t) ->
let abst_map (lenv, a, wws) (id, r, w) =
let attr = name_of_id ~r id in
let ww = xlate_term C.start st lenv w in
in
let lenv, aa, bb = match b with
| T.Abst xws ->
- let lenv = D.push_bind C.start lenv [] (D.Abst []) in
+ let lenv = D.push_bind C.start lenv [] (D.Abst (n, [])) in
let lenv, aa, wws = List.fold_left abst_map (lenv, [], []) xws in
- lenv, aa, D.Abst wws
+ lenv, aa, D.Abst (n, wws)
| T.Abbr xvs ->
let lenv = D.push_bind C.start lenv [] (D.Abbr []) in
let lenv, aa, vvs = List.fold_left abbr_map (lenv, [], []) xvs in
let xlate_term f st lenv t =
TT.contract (xlate_term f st lenv) t
-let mk_contents tt = function
- | T.Decl -> [], E.Abst tt
- | T.Ax -> [], E.Abst tt
+let mk_contents n tt = function
+ | T.Decl -> [], E.Abst (n, tt)
+ | T.Ax -> [], E.Abst (n, tt)
+ | T.Cong -> [], E.Abst (n, tt)
| T.Def -> [], E.Abbr tt
| T.Th -> [], E.Abbr tt
{st with sort = H.set_sorts ix [s]}
in
err (List.fold_left map st sorts)
- | T.Graph id ->
+ | T.Graph id ->
assert (H.set_graph id); err st
- | T.Entity (kind, id, meta, t) ->
+ | T.Entity (kind, n, id, meta, t) ->
let uri = uri_of_id st id st.path in
Hashtbl.add henv id uri;
let tt = xlate_term C.start st D.empty_lenv t in
(*
print_newline (); CrgOutput.pp_term print_string tt;
*)
- let a, b = mk_contents tt kind in
+ let a, b = mk_contents n tt kind 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 _ ->
+ | T.Generate _ ->
err st
(* Interface functions ******************************************************)
-(* free = F I N P Q U V W *)
+(* free = F I P Q U V W *)
module U = NUri
module K = NUri.UriHash
module E = entity
module J = marks (**)
module R = alpha
+module N = level
module T = txt
module TP = txtParser
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
+module N = Level
+
type ix = int (* index *)
type id = string (* identifier *)
type kind = Decl (* generic declaration *)
| Ax (* axiom *)
+ | Cong (* conjecture *)
| Def (* generic definition *)
| Th (* theorem *)
-type bind = Abst of (id * bool * term) list (* name, real?, domain *)
- | Abbr of (id * term) list (* name, bodies *)
- | Void of id list (* names *)
-
-and term = Sort of ix (* level *)
- | NSrt of id (* named level *)
- | LRef of ix * ix (* index, offset *)
- | NRef of id (* name *)
- | Cast of term * term (* domain, element *)
- | Appl of term list * term (* arguments, function *)
- | Bind of bind * term (* binder, scope *)
- | Inst of term * term list (* function, arguments *)
- | Impl of bool * id * term * term (* strong?, label, source, target *)
-
-type command = Require of id list (* required files: names *)
- | Graph of id (* hierarchy graph: name *)
- | Sorts of (int option * id) list (* sorts: index, name *)
- | 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 *)
+type bind =
+(* name, real?, domain *)
+ | Abst of (id * bool * term) list
+(* name, bodies *)
+ | Abbr of (id * term) list
+(* names *)
+ | Void of id list
+
+and term =
+(* level *)
+ | Sort of ix
+(* named level *)
+ | NSrt of id
+(* index, offset *)
+ | LRef of ix * ix
+(* name *)
+ | NRef of id
+(* domain, element *)
+ | Cast of term * term
+(* arguments, function *)
+ | Appl of term list * term
+(* level, binder, scope *)
+ | Bind of N.level * bind * term
+(* function, arguments *)
+ | Inst of term * term list
+(* level, strong?, label, source, target *)
+ | Impl of N.level * bool * id * term * term
+
+type command =
+(* required files: names *)
+ | Require of id list
+(* hierarchy graph: name *)
+ | Graph of id
+(* sorts: index, name *)
+ | Sorts of (int option * id) list
+(* section: Some id = open, None = close last *)
+ | Section of id option
+(* entity: class, name, description, contents *)
+ | Entity of kind * N.level * id * desc * term
+(* predefined generated entity: arguments *)
+ | Generate of term list
| "\\graph" { out "GRAPH"; TP.GRAPH }
| "\\decl" { out "DECL"; TP.DECL }
| "\\ax" { out "AX"; TP.AX }
+ | "\\cong" { out "CONG"; TP.CONG }
| "\\def" { out "DEF"; TP.DEF }
| "\\th" { out "TH"; TP.TH }
| "\\generate" { out "GEN"; TP.GEN }
| "~" { out "TE"; TP.TE }
| "->" { out "WTO"; TP.WTO }
| "=>" { out "STO"; TP.STO }
+ | "^" { out "CT"; TP.CT }
| eof { out "EOF"; TP.EOF }
%{
module G = Options
+ module N = Level
module T = Txt
let _ = Parsing.set_trace !G.debug_parser
%}
%token <int> IX
%token <string> ID STR
- %token OP CP OB CB OA CA FS CN CM EQ STAR HASH PLUS TE WTO STO
- %token GRAPH DECL AX DEF TH GEN REQ OPEN CLOSE SORTS EOF
+ %token OP CP OB CB OA CA FS CN CM EQ STAR HASH PLUS TE WTO STO CT
+ %token GRAPH DECL AX CONG DEF TH GEN REQ OPEN CLOSE SORTS EOF
%start entry
%type <Txt.command option> entry
| sort { [$1] }
| sort CM sorts { $1 :: $3 }
;
+ level:
+ | { N.infinite }
+ | CT IX { N.finite $2}
+ ;
abst:
| ID CN term { $1, true, $3 }
| atom OP terms CP { T.Inst ($1, $3) }
;
term:
- | atom { $1 }
- | OA term CA fs term { T.Cast ($2, $5) }
- | OP term CP fs term { T.Appl ([$2], $5) }
- | OP terms CP fs term { T.Appl ($2, $5) }
- | OB binder CB fs term { T.Bind ($2, $5) }
- | term WTO term { T.Impl (false, "", $1, $3) }
- | ID TE term WTO term { T.Impl (false, $1, $3, $5) }
- | term STO term { T.Impl (true, "", $1, $3) }
- | ID TE term STO term { T.Impl (true, $1, $3, $5) }
- | OP term CP { $2 }
+ | atom { $1 }
+ | OA term CA fs term { T.Cast ($2, $5) }
+ | OP term CP fs term { T.Appl ([$2], $5) }
+ | OP terms CP fs term { T.Appl ($2, $5) }
+ | OB binder CB level fs term { T.Bind ($4, $2, $6) }
+ | term WTO level term { T.Impl ($3, false, "", $1, $4) }
+ | ID TE term WTO level term { T.Impl ($5, false, $1, $3, $6) }
+ | term STO level term { T.Impl ($3, true, "", $1, $4) }
+ | ID TE term STO level term { T.Impl ($5, true, $1, $3, $6) }
+ | OP term CP { $2 }
;
terms:
| term CM term { [$1; $3] }
decl:
| DECL { T.Decl }
| AX { T.Ax }
+ | CONG { T.Cong }
;
def:
| DEF { T.Def }
;
xentity:
| GRAPH ID
- { T.Graph $2 }
- | decl comment ID CN term
- { T.Entity ($1, $3, $2, $5) }
- | def comment ID EQ term
- { T.Entity ($1, $3, $2, $5) }
- | def comment ID EQ term CN term
- { T.Entity ($1, $3, $2, T.Cast ($7, $5)) }
+ { T.Graph $2 }
+ | decl level comment ID CN term
+ { T.Entity ($1, $2, $4, $3, $6) }
+ | def level comment ID EQ term
+ { T.Entity ($1, $2, $4, $3, $6) }
+ | def level comment ID EQ term CN term
+ { T.Entity ($1, $2, $4, $3, T.Cast ($8, $6)) }
| GEN term
- { T.Generate [$2] }
+ { T.Generate [$2] }
| GEN terms
- { T.Generate $2 }
+ { T.Generate $2 }
| REQ ids
- { T.Require $2 }
+ { T.Require $2 }
| OPEN ID
- { T.Section (Some $2) }
+ { T.Section (Some $2) }
| CLOSE
- { T.Section None }
+ { T.Section None }
| SORTS sorts
- { T.Sorts $2 }
+ { T.Sorts $2 }
;
start:
| GRAPH {} | decl {} | def {} | GEN {} |
| T.Inst (t, vs) ->
let tt = T.Appl (List.rev vs, t) in
contract f tt
- | T.Impl (false, id, w, t) ->
- let tt = T.Bind (T.Abst [id, false, w], t) in
+ | T.Impl (n, false, id, w, t) ->
+ let tt = T.Bind (n, T.Abst [id, false, w], t) in
contract f tt
- | T.Impl (true, id, w, t) ->
+ | T.Impl (n, true, id, w, t) ->
let f = function
- | T.Bind (T.Abst [xw], T.Bind (T.Abst xws, tt)) ->
- f (T.Bind (T.Abst (xw :: xws), tt))
+ | T.Bind (n, T.Abst [xw], T.Bind (_, T.Abst xws, tt)) ->
+ f (T.Bind (n, T.Abst (xw :: xws), tt))
| tt -> f tt
in
- let tt = T.Impl (false, id, w, t) in
+ let tt = T.Impl (n, false, id, w, t) in
contract f tt
| T.Sort _
| T.NSrt _
let f tt vvs = f (T.Appl (vvs, tt)) in
let f tt = C.list_map (f tt) contract vs in
contract f t
- | T.Bind (b, t) ->
- let f tt bb = f (T.Bind (bb, tt)) in
+ | T.Bind (n, b, t) ->
+ let f tt bb = f (T.Bind (n, bb, tt)) in
let f tt = contract_binder (f tt) b in
contract f t
module C = Cps
module G = Options
module E = Entity
+module N = Level
module M = Meta
module A = Aut
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, E.Abst entry in
+ let entity = a, uri_of_qid qid, E.Abst (N.infinite, entry) in
f {st with line = succ st.line} entity
in
xlate_term f st pars w
module C = Cps
module E = Entity
+module N = Level
module B = Brg
module M = Meta
| M.Abst (id, w, t) ->
let f w =
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
+ let f t = f (B.Bind (a, B.Abst (N.infinite, w), t)) in
+ xlate_term (B.push c B.empty a (B.Abst (N.infinite, w))) f t
in
xlate_term c f w
let xlate_pars f pars =
let map f (id, w) c =
let a = [E.Name (id, true)] in
- let f w = f (B.push c B.empty a (B.Abst w)) in
+ let f w = f (B.push c B.empty a (B.Abst (N.infinite, w))) in
xlate_term c f w
in
C.list_fold_right f map pars B.empty
| Some v -> count_term f c v
let count_entity f c = function
- | _, u, E.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
- | _, _, E.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
- | _, _, E.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
if !preprocess then process_input f st entity else f st entity
let process_nostreaming st lexbuf input =
+ let id x = x in
let rec aux1 book = match entity_of_input lexbuf input with
| NoEntity -> List.rev book
- | e -> aux1 (e :: book)
+ | e -> aux1 (id e :: book)
in
let rec aux2 st = function
| [] -> st
in
aux2 st (aux1 [])
-let rec process_streaming st lexbuf input = match entity_of_input lexbuf input with
- | NoEntity -> st
- | e -> process_streaming (process_0 st e) lexbuf input
+let process_streaming st lexbuf input =
+ let rec aux st = match entity_of_input lexbuf input with
+ | NoEntity -> st
+ | e -> aux (process_0 st e)
+ in
+ aux st
(****************************************************************************)
let main =
try
- let version_string = "Helena 0.8.1 M - August 2010" in
+ let version_string = "Helena 0.8.1 M - October 2010" in
let print_version () = L.warn (version_string ^ "\n"); exit 0 in
let set_hierarchy s =
if H.set_graph s then () else
let f a ns = a, ns in
let a, ns = Y.get_names f a in
match b with
- | D.Abst ws ->
- let e = D.push_bind C.start e a (D.Abst []) in
- let attrs = [XL.name ns; XL.mark a; XL.arity (List.length ws)] in
+ | D.Abst (n, ws) ->
+ let e = D.push_bind C.start e a (D.Abst (n, ws)) in
+ let attrs = [XL.level n; XL.name ns; XL.mark a; XL.arity (List.length ws)] in
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
+ | D.Abbr vs ->
+ let e = D.push_bind C.start e a (D.Abbr vs) in
let attrs = [XL.name ns; XL.mark a; XL.arity (List.length vs)] in
XL.tag XL.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab
- | D.Void n ->
+ | D.Void n ->
let attrs = [XL.name a; XL.mark a; XL.arity n] in
XL.tag XL.void attrs out tab
module C = Cps
module H = Hierarchy
module E = Entity
+module N = Level
(* internal functions *******************************************************)
let f i = "mark", string_of_int i in
E.mark err f a
+let level n =
+ "level", N.to_string n
+
(* TODO: the string s must be quoted *)
let meta a =
let err () = "meta", "" 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
- | E.Abst w -> tag "ABST" attrs ~contents:(pp_term w)
- | E.Abbr v -> tag "ABBR" attrs ~contents:(pp_term v)
- | E.Void -> assert false
+ | E.Abst (n, w) -> tag "ABST" (level n :: 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
val arity: int -> attr
+val level: Level.level -> attr
+
val name: Entity.attrs -> attr
val mark: Entity.attrs -> attr
projects / helm.git / commitdiff