let add_abst cnt id aw w =
let id = if !G.alpha <> "" then alpha id else id in
let aw = {aw with E.n_name = Some (id, true); E.n_degr = succ aw.E.n_degr} in
- D.EBind (cnt, aw, D.Abst (N.two, w))
+ D.EBind (cnt, aw, D.Abst (false, N.two, w))
let mk_lref f a i = f a (D.TLRef (a, i))
get_cnt err f lst lst.node
let push_abst f a w lenv =
- let bw = D.Abst (N.infinite, w) in
+ let bw = D.Abst (false, N.infinite, w) in
D.push_bind f a bw lenv
let add_proj e t = match e with
| _ -> assert false
else N.infinite
in
- let b = D.Abst (l, ww) in
+ let b = D.Abst (false, l, ww) in
let at = {at with E.n_name = name} in
f at (D.TBind (at, b, tt))
in
| D.TProj (_, e, t) ->
D.shift (xlate_term st 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 st f c (D.TCast (ac, D.TBind (ab, D.Abst (N.minus st n 1, ws), u), D.TBind (ab, D.Abst (n, ws), t)))
+ | D.TBind (ab, D.Abst (x, n, ws), D.TCast (ac, u, t)) ->
+ xlate_term st f c (D.TCast (ac, D.TBind (ab, D.Abst (x, N.minus st n 1, ws), u), D.TBind (ab, D.Abst (x, n, ws), t)))
| D.TBind (a, b, t) ->
let f cc =
let a, l, b = List.hd cc in
xlate_bind st f c a b
and xlate_bind st f c a = function
- | D.Abst (_, w) ->
+ | D.Abst (_, _, w) ->
let f ww = Z.push "xlate_bind" f c a (P.new_mark ()) (Z.Abst ww) in
xlate_term st f c w
- | D.Abbr v ->
+ | D.Abbr v ->
let f vv = Z.push "xlate_bind" f c a (P.new_mark ()) (Z.Abbr vv) in
xlate_term st f c v
- | D.Void ->
+ | D.Void ->
Z.push "xlate_bind" f c a (P.new_mark ()) Z.Void
(* internal functions: bag to crg term **************************************)
and xlate_bk_bind f c = function
| Z.Abst t ->
- let f tt = f (D.Abst (N.infinite, tt)) in
+ let f tt = f (D.Abst (false, N.infinite, tt)) in
xlate_bk_term f c t
| Z.Abbr t ->
let f tt = f (D.Abbr tt) in
(* used in BrgOutput.pp_lenv *)
let rec fold_right f map e x = match e with
| Null -> f x
- | Cons (e, c, a, b) -> fold_right (map f e c a b) map e x
+ | Cons (e, c, a, b) -> fold_right (map f c a b) map e x
let rec mem err f e b = match e with
| Null -> err ()
| D.TBind (a, b, t) ->
xlate_term (xlate_bind f a b) t
-and xlate_bind f a b x = match b with
- | D.Abst (n, w) ->
- let f ww = f (B.Bind (a, B.Abst (false, n, ww), x)) in
+and xlate_bind f a b t = match b with
+ | D.Abst (x, n, w) ->
+ let f ww = f (B.Bind (a, B.Abst (x, n, ww), t)) in
xlate_term f w
- | D.Abbr v ->
- let f vv = f (B.Bind (a, B.Abbr vv, x)) in
+ | D.Abbr v ->
+ let f vv = f (B.Bind (a, B.Abbr vv, t)) in
xlate_term f v
- | D.Void ->
- f (B.Bind (a, B.Void, x))
+ | D.Void ->
+ f (B.Bind (a, B.Void, t))
(* internal functions: brg to crg term **************************************)
xlate_bk_term f t
and xlate_bk_bind f = function
- | B.Abst (_, n, t) ->
- let f tt = f (D.Abst (n, tt)) in
+ | B.Abst (x, n, t) ->
+ let f tt = f (D.Abst (x, n, tt)) in
xlate_bk_term f t
| B.Abbr t ->
let f tt = f (D.Abbr tt) in
KP.fprintf och "[%a].%a" (name C.start) a (pp_term st ee) t
let pp_lenv st och e =
- let pp_entry f e c a b x = f x (* match b with
- | B.Abst (a, w) ->
- let a = R.alpha B.mem e a in
- KP.fprintf och "%a : %a\n" (name C.start) a (pp_term st e) w; f a
- | B.Abbr (a, v) ->
- let a = R.alpha B.mem e a in
- KP.fprintf och "%a = %a\n" (name C.start) a (pp_term st e) v; f a
- | B.Void a ->
- let a = R.alpha B.mem e a in
- KP.fprintf och "%a\n" (name C.start) a; f a
-*) in
- let e = B.empty in
- if e = B.empty then KP.fprintf och "%s\n" "not shown" else
+ let pp_entry f c a b x =
+ let a = R.alpha B.mem e a in
+ let x = B.push x c a b in
+ match b with
+ | B.Abst (_, _, w) ->
+ KP.fprintf och "[%a : %a] " (name C.start) a (pp_term st c) w; f x
+ | B.Abbr v ->
+ KP.fprintf och "[%a = %a] " (name C.start) a (pp_term st c) v; f x
+ | B.Void ->
+ KP.fprintf och "[%a]" (name C.start) a; f x
+ in
+ if e = B.empty then KP.fprintf och "%s" "empty" else
B.fold_right ignore pp_entry e B.empty
let specs = {
(* to share *)
let rec step st m r =
if !G.trace >= sublevel then
- log1 st (Printf.sprintf "entering R.step: l:%u n:%s" m.l (match m.n with Some n -> string_of_int n | None -> "infinite")) m.e r;
+ log1 st (Printf.sprintf "entering R.step: l=%u, n=%s," m.l (match m.n with Some n -> string_of_int n | None -> "infinite")) m.e r;
match r with
| B.Sort (a, h) ->
if assert_tstep m false then
?(beta=0) ?(theta=0) ?(epsilon=0) ?(ldelta=0) ?(gdelta=0) ?(zeta=0)
?(upsilon=0) ?(lrt=0) ?(grt=0) ?(e=0) ?(x=0) ()
=
-(*
if beta > 0 then L.warn level (KP.sprintf "BETA %u" beta);
if ldelta > 0 then L.warn level (KP.sprintf "EXP %u" ldelta);
if gdelta > 0 then L.warn level (KP.sprintf "EXP %u" gdelta);
if lrt > 0 then L.warn level (KP.sprintf "EXP %u" lrt);
- if grt > 0 then L.warn level (KP.sprintf "EXP %u" grt);
-*)
+ if grt > 0 then L.warn level (KP.sprintf "EXP %u" grt);
reductions := {
beta = !reductions.beta + beta;
zeta = !reductions.zeta + zeta;
type id = E.id
type attrs = E.node_attrs
-type bind = Abst of N.layer * term (* layer, type *)
- | Abbr of term (* body *)
- | Void (* *)
-
-and term = TSort of attrs * int (* attrs, hierarchy index *)
- | TLRef of attrs * int (* attrs, position indexe *)
- | TGRef of attrs * uri (* attrs, reference *)
- | TCast of attrs * term * term (* attrs, domain, element *)
- | TAppl of attrs * term * term (* attrs, argument, function *)
- | TBind of attrs * bind * term (* attrs, binder, scope *)
- | TProj of attrs * lenv * term (* attrs, closure, member *)
-
-and lenv = ESort (* top *)
- | EBind of lenv * attrs * bind (* environment, attrs, binder *)
- | EAppl of lenv * attrs * term (* environment, attrs, argument *)
- | EProj of lenv * attrs * lenv (* environment, attrs, closure *)
+type bind = Abst of bool * N.layer * term (* x-reduced?, layer, type *)
+ | Abbr of term (* body *)
+ | Void (* *)
+
+and term = TSort of attrs * int (* attrs, hierarchy index *)
+ | TLRef of attrs * int (* attrs, position indexe *)
+ | TGRef of attrs * uri (* attrs, reference *)
+ | TCast of attrs * term * term (* attrs, domain, element *)
+ | TAppl of attrs * term * term (* attrs, argument, function *)
+ | TBind of attrs * bind * term (* attrs, binder, scope *)
+ | TProj of attrs * lenv * term (* attrs, closure, member *)
+
+and lenv = ESort (* top *)
+ | EBind of lenv * attrs * bind (* environment, attrs, binder *)
+ | EAppl of lenv * attrs * term (* environment, attrs, argument *)
+ | EProj of lenv * attrs * lenv (* environment, attrs, closure *)
type entity = term E.entity
let replace f n0 e =
let rec aux f = function
- | ESort -> f ESort
- | EBind (e, a, Abst (n, w)) -> aux (push_bind f a (Abst (n0, w))) e
- | EBind (e, a, b) -> aux (push_bind f a b) e
- | EAppl (e, a, v) -> aux (push_appl f a v) e
- | EProj (e, a, d) -> let f d = aux (push_proj f a d) e in aux f d
+ | ESort -> f ESort
+ | EBind (e, a, Abst (x, n, w)) -> aux (push_bind f a (Abst (x, n0, w))) e
+ | EBind (e, a, b) -> aux (push_bind f a b) e
+ | EAppl (e, a, v) -> aux (push_appl f a v) e
+ | EProj (e, a, d) -> let f d = aux (push_proj f a d) e in aux f d
in
aux f e
count_binder f c e a b
and count_binder f c e a b = match b with
- | D.Abst (_, w) ->
+ | D.Abst (_, _, w) ->
let c = {c with tabsts = succ c.tabsts; nodes = succ c.nodes} in
let f c = D.push_bind (f c) a b e in
count_term f c e w
- | D.Abbr v ->
+ | D.Abbr v ->
let c = {c with tabbrs = succ c.tabbrs; xnodes = succ c.xnodes} in
let f c = D.push_bind (f c) a b e in
count_term f c e v
- | D.Void ->
+ | D.Void ->
let c = {c with tvoids = succ c.tvoids; xnodes = succ c.xnodes} in
D.push_bind (f c) a b e
E.name ignore f a;
out (KP.sprintf "+%i;" a.E.n_apix)
+let pp_state out x = if x then out "^"
+
let rec pp_term out st = function
| D.TSort (a, l) -> pp_attrs out a; out (KP.sprintf "*%u" l)
| D.TLRef (a, i ) -> pp_attrs out a; out (KP.sprintf "#%u" i)
| D.TGRef (a, u) -> pp_attrs out a; out (KP.sprintf "$")
- | D.TCast (a, x, y) -> pp_attrs out a; out "<"; pp_term out st x; out ">."; pp_term out st y
- | D.TAppl (a, x, y) -> pp_attrs out a; out "("; pp_term out st x; out ")."; pp_term out st y
- | D.TBind (a, x, y) -> pp_attrs out a; pp_bind out st x; out "."; pp_term out st y
- | D.TProj (a, x, y) -> pp_attrs out a; out "{"; pp_lenv out st x; out "}."; pp_term out st y
+ | D.TCast (a, u, t) -> pp_attrs out a; out "<"; pp_term out st u; out ">."; pp_term out st t
+ | D.TAppl (a, u, t) -> pp_attrs out a; out "("; pp_term out st u; out ")."; pp_term out st t
+ | D.TBind (a, u, t) -> pp_attrs out a; pp_bind out st u; out "."; pp_term out st t
+ | D.TProj (a, u, t) -> pp_attrs out a; out "{"; pp_lenv out st u; out "}."; pp_term out st t
and pp_bind out st = function
- | D.Abst (n, x) ->
- out "[:"; pp_term out st x; out "]"; out (N.to_string st n); out " "
- | D.Abbr x -> out "[="; pp_term out st x; out "] ";
- | D.Void -> out "[] "
+ | D.Abst (x, n, u) ->
+ out "[:"; pp_term out st u; out "]"; pp_state out x; out (N.to_string st n); out " "
+ | D.Abbr u -> out "[="; pp_term out st u; out "] ";
+ | D.Void -> out "[] "
and pp_lenv out st = function
| D.ESort -> ()
- | D.EBind (x, a, y) -> pp_lenv out st x; pp_attrs out a; pp_bind out st y
- | D.EAppl (x, a, y) -> pp_lenv out st x; out "("; pp_term out st y; out ") "
- | D.EProj (x, a, y) -> pp_lenv out st x; out "{"; pp_lenv out st y; out "} "
+ | D.EBind (u, a, t) -> pp_lenv out st u; pp_attrs out a; pp_bind out st t
+ | D.EAppl (u, a, t) -> pp_lenv out st u; out "("; pp_term out st t; out ") "
+ | D.EProj (u, a, t) -> pp_lenv out st u; out "{"; pp_lenv out st t; out "} "
let indent = KT.make (l+l) ' ' in
let pp_item och = function
| Term (c, t) -> KP.fprintf och "%s%a\n" indent (st.pp_term a c) t
- | LEnv c -> KP.fprintf och "%s%a" indent (st.pp_lenv a) c
+ | LEnv c -> KP.fprintf och "%s%a\n" indent (st.pp_lenv a) c
| Warn s -> KP.fprintf och "%s%s\n" indent s
| Uri u -> KP.fprintf och "%s<%s>\n" indent (U.string_of_uri u)
in
| T.Abst (n, id, r, w) ->
let f a ww =
let a = {a with E.n_name = name_of_id ~r id} in
- f a (D.Abst (n, ww))
+ f a (D.Abst (false, n, ww))
in
xlate_term f st lenv w
| T.Abbr (id, v) ->
XL.tag XL.appl attrs ~contents:(exp_term st e v) out tab;
and exp_bind st e a b out tab = match b with
- | D.Abst (n, w) ->
+ | D.Abst (_, n, w) ->
let attrs = [XL.layer st n; XL.name a; XL.kind a] in
XL.tag XL.abst attrs ~contents:(exp_term st e w) out tab
- | D.Abbr v ->
+ | D.Abbr v ->
let attrs = [XL.name a] in
XL.tag XL.abbr attrs ~contents:(exp_term st e v) out tab
- | D.Void ->
+ | D.Void ->
let attrs = [XL.name a] in
XL.tag XL.void attrs out tab
projects / helm.git / commitdiff