src/common/entity.cmx src/basic_ag/bagCrg.cmx src/basic_ag/bag.cmx \
src/basic_ag/bagOutput.cmi
src/basic_ag/bagEnvironment.cmi : src/basic_ag/bag.cmx
-src/basic_ag/bagEnvironment.cmo : src/lib/log.cmi src/common/entity.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/bagEnvironment.cmo : src/common/options.cmx src/lib/log.cmi \
+ src/common/entity.cmx src/basic_ag/bag.cmx \
+ src/basic_ag/bagEnvironment.cmi
+src/basic_ag/bagEnvironment.cmx : src/common/options.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/lib/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
let attrs_for_abst id aw =
let id = if !G.alpha <> "" then alpha id else id in
- let main = E.succ aw.E.n_main in
- E.node_attrs ~name:(id, true) ~side:aw.E.n_main ~main ()
+ let main = E.succ aw.E.b_main in
+ E.bind_attrs ~name:(id, true) ~side:aw.E.b_main ~main ()
let attrs_for_decl aw =
- let main = E.succ aw.E.n_main in
- E.node_attrs ~side:aw.E.n_main ~main ()
+ let main = E.succ aw.E.b_main in
+ E.bind_attrs ~side:aw.E.b_main ~main ()
let add_abst cnt id aw w =
- let a = attrs_for_abst id aw in
+ let y = attrs_for_abst id aw in
let l = if !G.infinity then N.infinity else N.two in
- D.EBind (cnt, a, D.Abst (false, l, w))
+ D.EBind (cnt, E.empty_node, y, D.Abst (false, l, w))
-let mk_lref f a i = f a (D.TLRef (a, i))
+let mk_lref f _ y i = f y (D.TLRef (E.empty_node, i))
let id_of_name (id, _, _) =
if !G.alpha <> "" then alpha id else id
| Some qid -> let f qid = f (Some qid) in relax_qid f lst qid
let resolve_gref err f lst qid =
- try let a, cnt = UH.find henv (uri_of_qid qid) in f qid a cnt
+ try let y, cnt = UH.find henv (uri_of_qid qid) in f qid y cnt
with Not_found -> err qid
let resolve_gref_relaxed f lst qid =
let rec err node = relax_opt_qid (get_cnt err f lst) lst node in
get_cnt err f lst lst.node
-let push_abst f a w lenv =
+let push_abst f y w lenv =
let bw = D.Abst (false, N.infinity, w) in
- D.push_bind f a bw lenv
-
-let add_proj at e t = match e with
- | D.ESort -> t
- | D.EBind (D.ESort, a, b) -> D.TBind (E.compose a at, b, t)
- | _ ->
-IFDEF MANAGER OR OBJS THEN
- D.TProj (at, D.set_attrs C.start at e, t)
-ELSE
- D.TProj (at, e, t)
-END
+ D.push_bind f E.empty_node y bw lenv
+
+let add_proj yt e t = match e with
+ | D.ESort -> t
+ | D.EBind (D.ESort, _, y, b) -> D.TBind (E.compose y yt, b, t)
+ | _ ->
+ D.TProj (D.set_attrs C.start yt e, t)
(* this is not tail recursive in the GRef branch *)
-let rec xlate_term f st lst y lenv = function
+let rec xlate_term f st lst z lenv = function
| A.Sort s ->
- let h = if s then 0 else 1 in
- let a = E.node_attrs ~main:(h, 0) () in
- f a (D.TSort (a, h))
+ let k = if s then 0 else 1 in
+ let y = E.bind_attrs ~main:(k, 0) () in
+ f y (D.TSort k)
| A.Appl (v, t) ->
- let f av vv at tt =
- let at = E.compose av at in
- f at (D.TAppl (at, !G.extended, vv, tt))
+ let f vv yt tt =
+ f yt (D.TAppl (!G.extended, vv, tt))
in
- let f av vv = xlate_term (f av vv) st lst y lenv t in
+ let f _ vv = xlate_term (f vv) st lst z lenv t in
xlate_term f st lst false lenv v
| A.Abst (name, w, t) ->
- let f aw ww =
- let aw = attrs_for_abst name aw in
- let f at tt =
- let at = E.compose aw at in
+ let f yw ww =
+ let yw = attrs_for_abst name yw in
+ let f yt tt =
+ let yt = E.compose yw yt in
let l =
- if !G.cc then match y, snd at.E.n_main with
+ if !G.cc then match z, snd yt.E.b_main with
| true, _ -> N.one
| _ , 0 -> N.one
| _ , 1 -> N.unknown st
else N.infinity
in
let b = D.Abst (false, l, ww) in
- f at (D.TBind (at, b, tt))
+ f yt (D.TBind (yt, b, tt))
in
- let f lenv = xlate_term f st lst y lenv t in
- push_abst f aw ww lenv
+ let f lenv = xlate_term f st lst z lenv t in
+ push_abst f yw ww lenv
in
xlate_term f st lst true lenv w
| A.GRef (name, args) ->
let map1 args (id, _) = A.GRef ((id, true, []), []) :: args in
let map2 f arg args =
- let f av v = f (D.EAppl (args, E.shift av, !G.extended, v)) in
+ let f _ v = f (D.EAppl (args, !G.extended, v)) in
xlate_term f st lst false lenv arg
in
- let g qid a cnt =
- let gref = D.TGRef (a, uri_of_qid qid) in
- if cnt = D.ESort then f a gref else
+ let g qid y cnt =
+ let gref = D.TGRef (E.empty_node, uri_of_qid qid) in
+ if cnt = D.ESort then f y gref else
let f = function
- | D.EAppl (D.ESort, av, x, v) ->
- let a = E.compose av a in
- f a (D.TAppl (a, x, v, gref))
- | args ->
-IFDEF MANAGER OR OBJS THEN
- f a (D.TProj (a, D.set_attrs C.start a args, gref))
-ELSE
- f a (D.TProj (a, args, gref))
-END
+ | D.EAppl (D.ESort, x, v) -> f y (D.TAppl (x, v, gref))
+ | args -> f y (D.TProj (args, gref))
in
let f args = C.list_fold_right f map2 args D.ESort in
D.sub_list_strict (D.fold_names f map1 args) cnt args
| A.Decl (name, w) ->
let f lenv =
let f qid =
- let f aw ww =
- let a = attrs_for_decl aw in
- UH.add henv (uri_of_qid qid) (a, lenv);
- let t = add_proj aw lenv ww in
+ let f yw ww =
+ let y = attrs_for_decl yw in
+ UH.add henv (uri_of_qid qid) (y, lenv);
+ let t = add_proj yw lenv ww in
(*
print_newline (); CrgOutput.pp_term print_string t;
*)
- let na = {aw with E.n_apix = lst.line} in
+ let na = E.node_attrs ~apix:lst.line () in
let entity = E.empty_root, na, uri_of_qid qid, E.Abst t in
G.set_current_trace lst.line;
f {lst with line = succ lst.line} entity
let f lenv =
let f qid =
let f _ ww =
- let f av vv =
- UH.add henv (uri_of_qid qid) (av, lenv);
- let t = add_proj av lenv (D.TCast (av, ww, vv)) in
+ let f yv vv =
+ UH.add henv (uri_of_qid qid) (yv, lenv);
+ let t = add_proj yv lenv (D.TCast (ww, vv)) in
(*
print_newline (); CrgOutput.pp_term print_string t;
*)
- let na = {av with E.n_apix = lst.line} in
+ let na = E.node_attrs ~apix:lst.line () 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, E.Abbr t in
G.set_current_trace lst.line;
module E = Entity
type uri = E.uri
-type attrs = E.node_attrs
+type b_attrs = E.bind_attrs
type bind = Void (* exclusion *)
| Abst of term (* abstraction *)
| Abbr of term (* abbreviation *)
-and term = Sort of int (* hierarchy index *)
- | LRef of P.mark (* location *)
- | GRef of uri (* reference *)
- | Cast of term * term (* domain, element *)
- | Appl of term * term (* argument, function *)
- | Bind of attrs * P.mark * bind * term (* name, location, binder, scope *)
+and term = Sort of int (* hierarchy index *)
+ | LRef of P.mark (* location *)
+ | GRef of uri (* reference *)
+ | Cast of term * term (* domain, element *)
+ | Appl of term * term (* argument, function *)
+ | Bind of b_attrs * P.mark * bind * term (* name, location, binder, scope *)
type entity = term E.entity (* attrs, uri, binder *)
-type lenv = (attrs * P.mark * bind) list (* name, location, binder *)
+type lenv = (b_attrs * P.mark * bind) list (* name, location, binder *)
type message = (lenv, term) Log.item list
let appl u t = Appl (u, t)
-let bind a l b t = Bind (a, l, b, t)
+let bind y l b t = Bind (y, l, b, t)
-let bind_abst a l u t = Bind (a, l, Abst u, t)
+let bind_abst y l u t = Bind (y, l, Abst u, t)
-let bind_abbr a l v t = Bind (a, l, Abbr v, t)
+let bind_abbr y l v t = Bind (y, l, Abbr v, t)
(* local environment handling functions *************************************)
let empty_lenv = []
-let push msg f es a l b =
+let push msg f es y l b =
let rec does_not_occur loc = function
| [] -> true
| (_, l, _) :: _ when l = loc -> false
| _ :: es -> does_not_occur l es
in
if not (does_not_occur l es) then failwith msg else
- let c = (a, l, b) :: es in f c
+ let c = (y, l, b) :: es in f c
let append f es1 es2 =
f (List.append es2 es1)
let get err f es i =
let rec aux = function
| [] -> err ()
- | (a, l, b) :: tl -> if l = i then f a b else aux tl
+ | (y, l, b) :: tl -> if l = i then f y b else aux tl
in
aux es
(* internal functions: crg to bag term **************************************)
let rec xlate_term st f c = function
- | D.TSort (_, h) -> f (Z.Sort h)
- | D.TGRef (_, s) -> f (Z.GRef s)
- | D.TLRef (a, i) ->
+ | D.TSort k -> f (Z.Sort k)
+ | D.TGRef (_, s) -> f (Z.GRef s)
+ | D.TLRef (_, i) ->
let _, l, _ = List.nth c i in f (Z.LRef l)
- | D.TCast (_, u, t) ->
+ | D.TCast (u, t) ->
let f tt uu = f (Z.Cast (uu, tt)) in
let f tt = xlate_term st (f tt) c u in
xlate_term st f c t
- | D.TAppl (_, _, v, t) ->
+ | D.TAppl (_, v, t) ->
let f tt vv = f (Z.Appl (vv, tt)) in
let f tt = xlate_term st (f tt) c v in
xlate_term st f c t
- | D.TProj (_, e, t) ->
+ | 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 (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) ->
+ | D.TBind (y, D.Abst (x, n, ws), D.TCast (u, t)) ->
+ xlate_term st f c (D.TCast (D.TBind (y, D.Abst (x, N.minus st n 1, ws), u), D.TBind (y, D.Abst (x, n, ws), t)))
+ | D.TBind (y, b, t) ->
let f cc =
let a, l, b = List.hd cc in
let f tt = f (Z.Bind (a, l, b, tt)) in
xlate_term st f cc t
in
- xlate_bind st f c a b
+ xlate_bind st f c y b
-and xlate_bind st f c a = function
+and xlate_bind st f c y = function
| D.Abst (_, _, w) ->
- let f ww = Z.push "xlate_bind" f c a (P.new_mark ()) (Z.Abst ww) in
+ let f ww = Z.push "xlate_bind" f c y (P.new_mark ()) (Z.Abst ww) in
xlate_term st f c w
| D.Abbr v ->
- let f vv = Z.push "xlate_bind" f c a (P.new_mark ()) (Z.Abbr vv) in
+ let f vv = Z.push "xlate_bind" f c y (P.new_mark ()) (Z.Abbr vv) in
xlate_term st f c v
| D.Void ->
- Z.push "xlate_bind" f c a (P.new_mark ()) Z.Void
+ Z.push "xlate_bind" f c y (P.new_mark ()) Z.Void
(* internal functions: bag to crg term **************************************)
let rec xlate_bk_term f c = function
- | Z.Sort h -> f (D.TSort (E.empty_node, h))
+ | Z.Sort k -> f (D.TSort k)
| Z.GRef s -> f (D.TGRef (E.empty_node, s))
| Z.LRef l ->
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 (E.empty_node, uu, tt)) in
+ let f tt uu = f (D.TCast (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 (E.empty_node, true, uu, tt)) in
+ let f tt uu = f (D.TAppl (true, 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) ->
- let f tt bb = f (D.TBind (a, bb, tt)) in
+ | Z.Bind (y, l, b, t) ->
+ let f tt bb = f (D.TBind (y, bb, tt)) in
let f tt = xlate_bk_bind (f tt) c b in
- let cc = Z.push "xlate_bk_term" C.start c a l b in
+ let cc = Z.push "xlate_bk_term" C.start c y l b in
xlate_bk_term f cc t
and xlate_bk_bind f c = function
module U = NUri
module UH = U.UriHash
module L = Log
+module G = Options
module E = Entity
module Z = Bag
exception ObjectNotFound of Z.message
-let hsize = 7000
+let hsize = 7000
let env = UH.create hsize
(* Internal functions *******************************************************)
-let get_age =
- let age = ref 0 in
- fun () -> incr age; !age
-
let error uri = raise (ObjectNotFound (L.items1 (U.string_of_uri uri)))
(* Interface functions ******************************************************)
-let set_entity f (ra, na, uri, b) =
- let age = get_age () in
- let entry = ra, {na with E.n_apix = age}, uri, b in
- UH.add env uri entry; f entry
+let set_entity f entity =
+IFDEF EXPAND THEN
+ let ra, na, uri, b = entity in
+ let entity0 = if !G.expand then ra, E.node_attrs ~apix:0 (), uri, b else entity in
+ UH.add env uri entity0; f entity
+ELSE
+ let _, _, uri, _ = entity in
+ UH.add env uri entity; f entity
+END
let get_entity f uri =
try f (UH.find env uri) with Not_found -> error uri
KP.fprintf och "{%a}.%a" (pp_term st c) u (pp_term st c) t
| Z.Appl (v, t) ->
KP.fprintf och "(%a).%a" (pp_term st c) v (pp_term st c) t
- | Z.Bind (a, l, Z.Abst w, t) ->
+ | Z.Bind (y, l, Z.Abst w, t) ->
let f cc =
- KP.fprintf och "[%t:%a].%a" (res a l) (pp_term st c) w (pp_term st cc) t
+ KP.fprintf och "[%t:%a].%a" (res y l) (pp_term st c) w (pp_term st cc) t
in
- Z.push "output abst" f c a l (Z.Abst w)
- | Z.Bind (a, l, Z.Abbr v, t) ->
+ Z.push "output abst" f c y l (Z.Abst w)
+ | Z.Bind (y, l, Z.Abbr v, t) ->
let f cc =
- KP.fprintf och "[%t=%a].%a" (res a l) (pp_term st c) v (pp_term st cc) t
+ KP.fprintf och "[%t=%a].%a" (res y l) (pp_term st c) v (pp_term st cc) t
in
- Z.push "output abbr" f c a l (Z.Abbr v)
- | Z.Bind (a, l, Z.Void, t) ->
- let f cc = KP.fprintf och "[%t].%a" (res a l) (pp_term st cc) t in
- Z.push "output void" f c a l Z.Void
+ Z.push "output abbr" f c y l (Z.Abbr v)
+ | Z.Bind (y, l, Z.Void, t) ->
+ let f cc = KP.fprintf och "[%t].%a" (res y l) (pp_term st cc) t in
+ Z.push "output void" f c y l Z.Void
let pp_lenv st och c =
let pp_entry och = function
- | a, l, Z.Abst w ->
- KP.fprintf och "%t : %a\n" (res a l) (pp_term st c) w
- | a, l, Z.Abbr v ->
- KP.fprintf och "%t = %a\n" (res a l) (pp_term st c) v
- | a, l, Z.Void ->
- KP.fprintf och "%t\n" (res a l)
+ | y, l, Z.Abst w ->
+ KP.fprintf och "%t : %a\n" (res y l) (pp_term st c) w
+ | y, l, Z.Abbr v ->
+ KP.fprintf och "%t = %a\n" (res y l) (pp_term st c) v
+ | y, l, Z.Void ->
+ KP.fprintf och "%t\n" (res y l)
in
let iter map och l = List.iter (map och) l in
let f es = KP.fprintf och "%a" (iter pp_entry) (List.rev es) in
| Sort_ of int
| LRef_ of P.mark * Z.term option
| GRef_ of Z.entity
- | Bind_ of Z.attrs * P.mark * Z.term * Z.term
+ | Bind_ of Z.b_attrs * P.mark * Z.term * Z.term
type ho_whd_result =
| Sort of int
let inc m = {m with i = succ m.i}
let unwind_to_term f m t =
- let map f t (a, l, b) = f (Z.Bind (a, l, b, t)) in
+ let map f t (y, l, b) = f (Z.Bind (y, l, b, t)) in
let f mc = C.list_fold_left f map t mc in
Z.contents f m.c
get f c m i
| Z.Cast (_, t) -> whd f c m t
| Z.Appl (v, t) -> whd f c {m with s = v :: m.s} t
- | Z.Bind (a, l, Z.Abst w, t) ->
+ | Z.Bind (y, l, Z.Abst w, t) ->
begin match m.s with
- | [] -> f m (Bind_ (a, l, w, t))
+ | [] -> f m (Bind_ (y, l, w, t))
| v :: tl ->
let nl = P.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)))
+ Z.push "!" f m.c y nl (Z.Abbr (Z.Cast (w, v)))
end
- | Z.Bind (a, l, b, t) ->
+ | Z.Bind (y, l, b, t) ->
let nl = P.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
+ Z.push "!" f m.c y nl b
(* Interface functions ******************************************************)
let u, t = term_of_whdr r1, term_of_whdr r2 in
if !G.ct >= level then log2 st "Now really converting" c u c t;
match r1, r2 with
- | Sort_ h1, Sort_ h2 ->
- if h1 = h2 then f a else f false
- | LRef_ (i1, _), LRef_ (i2, _) ->
+ | Sort_ k1, Sort_ k2 ->
+ if k1 = k2 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.n_apix = a1}, _, E.Abst _),
- GRef_ (_, {E.n_apix = a2}, _, E.Abst _) ->
+ GRef_ (_, {E.n_apix = a2}, _, E.Abst _) ->
if a1 = a2 then are_convertible_stacks f st a c m1 m2 else f false
| GRef_ (_, {E.n_apix = a1}, _, E.Abbr v1),
- GRef_ (_, {E.n_apix = a2}, _, E.Abbr v2) ->
+ GRef_ (_, {E.n_apix = 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) ->
+ | Bind_ (y1, l1, w1, t1), Bind_ (_, l2, w2, t2) ->
let l = P.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
ZS.subst f l l1 t1
in
- let f r = if r then push "!" h c m1 a1 l w1 else f false in
+ let f r = if r then push "!" h c m1 y1 l w1 else f false in
are_convertible f st a c m1 w1 m2 w2
(* we detect the AUT-QE reduction rule for type/prop inclusion *)
- | Sort_ _, Bind_ (a2, l2, w2, t2) when !G.si ->
+ | Sort_ _, Bind_ (y2, l2, w2, t2) when !G.si ->
let m1, m2 = inc m1, inc m2 in
let f c = are_convertible f st a c m1 (term_of_whdr r1) m2 t2 in
- push "nsi" f c m2 a2 l2 w2
- | _ -> f false
+ push "nsi" f c m2 y2 l2 w2
+ | _ -> f false
and aux_rev m2 r2 m1 r1 = aux m1 r1 m2 r2 in
let g m1 r1 = whd (aux m1 r1) c m2 t2 in
if a = false then f false else whd g c m1 t1
let f w' u' = f (S.sh2 w w' u u' t Z.appl) in
let f w' = lref_map (f w') map u in
lref_map f map w
- | Z.Bind (a, l, b, u) ->
- let f b' u' = f (S.sh2 b b' u u' t (Z.bind a l)) in
+ | Z.Bind (y, l, b, u) ->
+ let f b' u' = f (S.sh2 b b' u u' t (Z.bind y l)) in
let f b' = lref_map (f b') map u in
lref_map_bind f map b
| _, _, _, E.Void -> assert false
in
ZE.get_entity f uri
- | Z.Bind (a, l, Z.Abbr v, t) ->
+ | Z.Bind (y, l, Z.Abbr v, t) ->
let f xv xt tt =
- f (S.sh2 v xv t xt x (Z.bind_abbr a l)) (Z.bind_abbr a l xv tt)
+ f (S.sh2 v xv t xt x (Z.bind_abbr y l)) (Z.bind_abbr y l xv tt)
in
let f xv cc = b_type_of err (f xv) st cc t in
- let f xv = Z.push "type abbr" (f xv) c a l (Z.Abbr xv) in
+ let f xv = Z.push "type abbr" (f xv) c y l (Z.Abbr xv) in
let f xv vv = match xv with
| Z.Cast _ -> f xv
| _ -> f (Z.Cast (vv, xv))
in
type_of err f st c v
- | Z.Bind (a, l, Z.Abst u, t) ->
+ | Z.Bind (y, l, Z.Abst u, t) ->
let f xu xt tt =
- f (S.sh2 u xu t xt x (Z.bind_abst a l)) (Z.bind_abst a l xu tt)
+ f (S.sh2 u xu t xt x (Z.bind_abst y l)) (Z.bind_abst y l xu tt)
in
let f xu cc = b_type_of err (f xu) st cc t in
- let f xu _ = Z.push "type abst" (f xu) c a l (Z.Abst xu) in
+ let f xu _ = Z.push "type abst" (f xu) c y l (Z.Abst xu) in
type_of err f st c u
- | Z.Bind (a, l, Z.Void, t) ->
+ | Z.Bind (y, l, Z.Void, t) ->
let f xt tt =
- f (S.sh1 t xt x (Z.bind a l Z.Void)) (Z.bind a l Z.Void tt)
+ f (S.sh1 t xt x (Z.bind y l Z.Void)) (Z.bind y l Z.Void tt)
in
let f cc = b_type_of err f st cc t in
- Z.push "type void" f c a l Z.Void
+ Z.push "type void" f c y l Z.Void
| Z.Appl (v, t) ->
let f xv vv xt tt = function
- | ZR.Abst w ->
+ | ZR.Abst w ->
if !G.ct > level then L.log st ZO.specs level (L.t_items1 "Just scanned" c w);
let f a =
(* L.warn (Printf.sprintf "Convertible: %b" a); *)
else error3 err c xv vv w
in
ZR.are_convertible f st c w vv
- | _ ->
+ | _ ->
error1 err "not a function" c xt
in
let f xv vv xt tt = ZR.ho_whd (f xv vv xt tt) st c tt in
module E = Entity
type uri = E.uri
-type attrs = E.node_attrs
+type n_attrs = E.node_attrs
+type b_attrs = E.bind_attrs
(* x-reduced abstractions are output by RTM only *)
type bind = Void (* *)
| Abst of bool * N.layer * term (* x-reduced?, layer, type *)
| Abbr of term (* body *)
-and term = Sort of attrs * int (* attrs, hierarchy index *)
- | LRef of attrs * int (* attrs, position index *)
- | GRef of attrs * uri (* attrs, reference *)
- | Cast of attrs * term * term (* attrs, type, term *)
- | Appl of attrs * bool * term * term (* attrs, extended?, argument, function *)
- | Bind of attrs * bind * term (* attrs, binder, scope *)
+and term = Sort of int (* hierarchy index *)
+ | LRef of n_attrs * int (* attrs, position index *)
+ | GRef of n_attrs * uri (* attrs, reference *)
+ | Cast of term * term (* type, term *)
+ | Appl of bool * term * term (* extended?, argument, function *)
+ | Bind of b_attrs * bind * term (* attrs, binder, scope *)
type entity = term E.entity (* attrs, uri, binder *)
type lenv = Null
(* Cons: tail, relative local environment, attrs, binder *)
- | Cons of lenv * lenv * attrs * bind
+ | Cons of lenv * lenv * n_attrs * b_attrs * bind
type manager = (N.status -> entity -> bool) * (unit -> unit)
let gref a u = GRef (a, u)
-let cast a u t = Cast (a, u, t)
+let cast u t = Cast (u, t)
-let appl a x u t = Appl (a, x, u, t)
+let appl x u t = Appl (x, u, t)
-let bind a b t = Bind (a, b, t)
+let bind y b t = Bind (y, b, t)
-let bind_abst r n a u t = Bind (a, Abst (r, n, u), t)
+let bind_abst r n y u t = Bind (y, Abst (r, n, u), t)
-let bind_abbr a u t = Bind (a, Abbr u, t)
+let bind_abbr y u t = Bind (y, Abbr u, t)
-let bind_void a t = Bind (a, Void, t)
+let bind_void y t = Bind (y, Void, t)
(* local environment handling functions *************************************)
let empty = Null
-let push e c a b = Cons (e, c, a, b)
+let push e c a y b = Cons (e, c, a, y, b)
-let rec get i = function
- | Null -> empty, empty, E.empty_node, Void
- | Cons (e, c, a, b) when i = 0 -> e, c, a, b
- | Cons (e, _, _, _) -> get (pred i) e
-
-let get e i = get i e
+let rec get e i = match e with
+ | Null -> empty, empty, E.empty_node, E.empty_bind, Void
+ | Cons (e, c, a, y, b) when i = 0 -> e, c, a, y, b
+ | Cons (e, _, _, _, _) -> get e (pred i)
(* 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 c a b) map e x
+ | Null -> f x
+ | Cons (e, c, a, y, b) -> fold_right (map f c a y b) map e x
-let rec mem err f e b = match e with
- | Null -> err ()
- | Cons (e, _, a, _) ->
- if a.E.n_name = b.E.n_name then f () else mem err f e b
+let rec mem err f e y0 = match e with
+ | Null -> err ()
+ | Cons (e, _, _, y, _) ->
+ if y.E.b_name = y0.E.b_name then f () else mem err f e y0
(* internal functions: crg to brg term **************************************)
let rec xlate_term f = function
- | D.TSort (a, l) -> f (B.Sort (a, l))
- | D.TGRef (a, n) -> f (B.GRef (a, n))
- | D.TLRef (a, i) -> f (B.LRef (a, i))
- | D.TCast (a, u, t) ->
- let f tt uu = f (B.Cast (a, uu, tt)) in
+ | D.TSort k -> f (B.Sort k)
+ | D.TGRef (a, n) -> f (B.GRef (a, n))
+ | D.TLRef (a, i) -> f (B.LRef (a, i))
+ | D.TCast (u, t) ->
+ let f tt uu = f (B.Cast (uu, tt)) in
let f tt = xlate_term (f tt) u in
- xlate_term f t
- | D.TAppl (a, x, v, t) ->
- let f tt vv = f (B.Appl (a, x, vv, tt)) in
+ xlate_term f t
+ | D.TAppl (x, v, t) ->
+ let f tt vv = f (B.Appl (x, vv, tt)) in
let f tt = xlate_term (f tt) v in
xlate_term f t
- | D.TProj (_, e, t) ->
+ | D.TProj (e, t) ->
D.shift (xlate_term f) e t
- | D.TBind (a, b, t) ->
- xlate_term (xlate_bind f a b) t
+ | D.TBind (y, b, t) ->
+ xlate_term (xlate_bind f y b) t
-and xlate_bind f a b t = match b with
+and xlate_bind f y b t = match b with
| D.Abst (r, n, w) ->
- let f ww = f (B.Bind (a, B.Abst (r, n, ww), t)) in
+ let f ww = f (B.Bind (y, B.Abst (r, n, ww), t)) in
xlate_term f w
| D.Abbr v ->
- let f vv = f (B.Bind (a, B.Abbr vv, t)) in
+ let f vv = f (B.Bind (y, B.Abbr vv, t)) in
xlate_term f v
| D.Void ->
- f (B.Bind (a, B.Void, t))
+ f (B.Bind (y, B.Void, t))
(* internal functions: brg to crg term **************************************)
let rec xlate_bk_term f = function
- | B.Sort (a, l) -> f (D.TSort (a, l))
- | B.GRef (a, n) -> f (D.TGRef (a, n))
- | B.LRef (a, i) -> f (D.TLRef (a, i))
- | B.Cast (a, u, t) ->
- let f tt uu = f (D.TCast (a, uu, tt)) in
+ | B.Sort k -> f (D.TSort k)
+ | B.GRef (a, n) -> f (D.TGRef (a, n))
+ | B.LRef (a, i) -> f (D.TLRef (a, i))
+ | B.Cast (u, t) ->
+ let f tt uu = f (D.TCast (uu, tt)) in
let f tt = xlate_bk_term (f tt) u in
xlate_bk_term f t
- | B.Appl (a, x, u, t) ->
- let f tt uu = f (D.TAppl (a, x, uu, tt)) in
+ | B.Appl (x, u, t) ->
+ let f tt uu = f (D.TAppl (x, uu, tt)) in
let f tt = xlate_bk_term (f tt) u in
xlate_bk_term f t
- | B.Bind (a, b, t) ->
- let f tt bb = f (D.TBind (a, bb, tt)) in
+ | B.Bind (y, b, t) ->
+ let f tt bb = f (D.TBind (y, bb, tt)) in
let f tt = xlate_bk_bind (f tt) b in
xlate_bk_term f t
let set_entity entity =
IFDEF EXPAND THEN
let ra, na, uri, b = entity in
- let entity0 = if !G.expand then ra, {na with E.n_apix = 0}, uri, b else entity in
+ let entity0 = if !G.expand then ra, E.node_attrs ~apix:0 (), uri, b else entity in
UH.add env uri entity0; entity
ELSE
let _, _, uri, _ = entity in
E.name err f a
let rec out_term st p e och = function
- | B.Sort (_, h) ->
- let sort = if h = 0 then "Type" else if h = 1 then "Prop" else assert false in
+ | B.Sort k ->
+ let sort = if k = 0 then "Type" else if k = 1 then "Prop" else assert false in
KP.fprintf och "%s" sort
| B.LRef (_, i) ->
- let _, _, a, b = B.get e i in
- KP.fprintf och "%a" out_name a
+ let _, _, _, y, b = B.get e i in
+ KP.fprintf och "%a" out_name y
| B.GRef (_, s) ->
KP.fprintf och "%a" out_uri s
- | B.Cast (_, u, t) ->
+ | B.Cast (u, t) ->
KP.fprintf och "(%a : %a)" (out_term st false e) t (out_term st false e) u
- | B.Appl (_, _, v, t) ->
+ | B.Appl (_, v, t) ->
let pt = match t with B.Appl _ -> false | _ -> true in
let op, cp = if p then "(", ")" else "", "" in
KP.fprintf och "%s%a %a%s" op (out_term st pt e) t (out_term st true e) v cp
- | B.Bind (a, B.Abst (r, n, w), t) ->
+ | B.Bind (y, B.Abst (r, n, w), t) ->
let p = true in
let op, cp = if p then "(", ")" else "", "" in
- let a = R.alpha B.mem e a in
- let ee = B.push e B.empty a (B.abst r n w) in
+ let y = R.alpha B.mem e y in
+ let ee = B.push e B.empty E.empty_node y (B.abst r n w) in
let ob, cb = match N.to_string st n with
| "1" -> "forall", ","
| "2" -> "fun", " =>"
| _ -> ok := false; "?", "?"
in
KP.fprintf och "%s%s (%a:%a)%s %a%s"
- op ob out_name a (out_term st false e) w cb (out_term st false ee) t cp
- | B.Bind (a, B.Abbr v, t) ->
+ op ob out_name y (out_term st false e) w cb (out_term st false ee) t cp
+ | B.Bind (y, B.Abbr v, t) ->
let op, cp = if p then "(", ")" else "", "" in
- let a = R.alpha B.mem e a in
- let ee = B.push e B.empty a (B.abbr v) in
+ let y = R.alpha B.mem e y in
+ let ee = B.push e B.empty E.empty_node y (B.abbr v) in
KP.fprintf och "%slet %a := %a in %a%s"
- op out_name a (out_term st false e) v (out_term st false ee) t cp
+ op out_name y (out_term st false e) v (out_term st false ee) t cp
| B.Bind (a, B.Void, t) -> C.err ()
let close_out och () = close_out och
E.name err f a
let rec out_term st p e och = function
- | B.Sort (_, h) ->
- let sort = if h = 0 then "Type[0]" else if h = 1 then "Prop" else assert false in
+ | B.Sort k ->
+ let sort = if k = 0 then "Type[0]" else if k = 1 then "Prop" else assert false in
KP.fprintf och "%s" sort
| B.LRef (_, i) ->
- let _, _, a, b = B.get e i in
- KP.fprintf och "%a" out_name a
+ let _, _, _, y, b = B.get e i in
+ KP.fprintf och "%a" out_name y
| B.GRef (_, s) ->
KP.fprintf och "%a" out_uri s
- | B.Cast (_, u, t) ->
+ | B.Cast (u, t) ->
KP.fprintf och "(%a : %a)" (out_term st false e) t (out_term st false e) u
- | B.Appl (_, _, v, t) ->
+ | B.Appl (_, v, t) ->
let pt = match t with B.Appl _ -> false | _ -> true in
let op, cp = if p then "(", ")" else "", "" in
KP.fprintf och "%s%a %a%s" op (out_term st pt e) t (out_term st true e) v cp
- | B.Bind (a, B.Abst (r, n, w), t) ->
+ | B.Bind (y, B.Abst (r, n, w), t) ->
let op, cp = if p then "(", ")" else "", "" in
- let a = R.alpha B.mem e a in
- let ee = B.push e B.empty a (B.abst r n w) in
- let binder = match N.to_string st n, fst a.E.n_main with
+ let y = R.alpha B.mem e y in
+ let ee = B.push e B.empty E.empty_node y (B.abst r n w) in
+ let binder = match N.to_string st n, fst y.E.b_main with
| "1", 0 -> "Π"
| "1", 1 -> "∀"
| "2", _ -> "λ"
| _ -> ok := false; "?"
in
KP.fprintf och "%s%s%a:%a.%a%s"
- op binder out_name a (out_term st false e) w (out_term st false ee) t cp
- | B.Bind (a, B.Abbr v, t) ->
+ op binder out_name y (out_term st false e) w (out_term st false ee) t cp
+ | B.Bind (y, B.Abbr v, t) ->
let op, cp = if p then "(", ")" else "", "" in
- let a = R.alpha B.mem e a in
- let ee = B.push e B.empty a (B.abbr v) in
+ let y = R.alpha B.mem e y in
+ let ee = B.push e B.empty E.empty_node y (B.abbr v) in
KP.fprintf och "%slet %a ≝ %a in %a%s"
- op out_name a (out_term st false e) v (out_term st false ee) t cp
+ op out_name y (out_term st false e) v (out_term st false ee) t cp
| B.Bind (a, B.Void, t) -> C.err ()
let close_out och () = close_out och
E.name err f a
let rec out_term st e och = function
- | B.Sort (_, h) ->
- let sort = if h = 0 then "k+set" else if h = 1 then "k+prop" else assert false in
+ | B.Sort k ->
+ let sort = if k = 0 then "k+set" else if k = 1 then "k+prop" else assert false in
KP.fprintf och "(sort %s)" sort
| B.LRef (_, i) ->
- let _, _, a, b = B.get e i in
- KP.fprintf och "%a" out_name a
+ let _, _, _, y, b = B.get e i in
+ KP.fprintf och "%a" out_name y
| B.GRef (_, s) ->
KP.fprintf och "%a" out_uri s
- | B.Cast (_, u, t) ->
+ | B.Cast (u, t) ->
KP.fprintf och "(cast %a %a)" (out_term st e) u (out_term st e) t
- | B.Appl (_, x, v, t) ->
+ | B.Appl (x, v, t) ->
let c = if x then "appx" else "appr" in
KP.fprintf och "(%s %a %a)" c (out_term st e) v (out_term st e) t
- | B.Bind (a, B.Abst (r, n, w), t) ->
- let a = R.alpha B.mem e a in
- let ee = B.push e B.empty a (B.abst r n w) in
+ | B.Bind (y, B.Abst (r, n, w), t) ->
+ let y = R.alpha B.mem e y in
+ let ee = B.push e B.empty E.empty_node y (B.abst r n w) in
let c = if r then "prod" else "abst" in
let l = match N.to_string st n with
| "1" -> "l+1"
| _ -> ok := false; "?"
in
KP.fprintf och "(%s %s %a %a\\ %a)"
- c l (out_term st e) w out_name a (out_term st ee) t
- | B.Bind (a, B.Abbr v, t) ->
- let a = R.alpha B.mem e a in
- let ee = B.push e B.empty a (B.abbr v) in
+ c l (out_term st e) w out_name y (out_term st ee) t
+ | B.Bind (y, B.Abbr v, t) ->
+ let y = R.alpha B.mem e y in
+ let ee = B.push e B.empty E.empty_node y (B.abbr v) in
KP.fprintf och "(abbr %a %a\\ %a)"
- (out_term st e) v out_name a (out_term st ee) t
- | B.Bind (a, B.Void, t) ->
- let a = R.alpha B.mem e a in
- let ee = B.push e B.empty a (B.Void) in
- KP.fprintf och "(void %a\\ %a)"
- out_name a (out_term st ee) t
+ (out_term st e) v out_name y (out_term st ee) t
+ | B.Bind (_, B.Void, _) -> C.err ()
(* elpi variant 1 ***********************************************************)
f c
and count_term f c e = function
- | B.Sort _ ->
+ | B.Sort _ ->
f {c with tsorts = succ c.tsorts; nodes = succ c.nodes}
- | B.LRef (_, i) ->
+ | B.LRef (_, i) ->
begin match B.get e i with
- | _, _, _, B.Abst _
- | _, _, _, B.Void ->
+ | _, _, _, _, B.Abst _
+ | _, _, _, _, B.Void ->
f {c with tlrefs = succ c.tlrefs; nodes = succ c.nodes}
- | _, _, _, B.Abbr _ ->
+ | _, _, _, _, B.Abbr _ ->
f {c with tlrefs = succ c.tlrefs; xnodes = succ c.xnodes}
end
- | B.GRef (_, u) ->
+ | B.GRef (_, u) ->
let c =
if Cps.list_mem ~eq:U.eq u c.uris
then {c with nodes = succ c.nodes}
else {c with xnodes = succ c.xnodes}
in
f {c with tgrefs = succ c.tgrefs}
- | B.Cast (_, v, t) ->
+ | B.Cast (v, t) ->
let c = {c with tcasts = succ c.tcasts} in
let f c = count_term f c e t in
count_term f c e v
- | B.Appl (_, _, v, t) ->
+ | B.Appl (_, v, t) ->
let c = {c with tappls = succ c.tappls; nodes = succ c.nodes} in
let f c = count_term f c e t in
count_term f c e v
- | B.Bind (a, b, t) ->
- let f c = count_term f c (B.push e B.empty a b) t in
+ | B.Bind (y, b, t) ->
+ let f c = count_term f c (B.push e B.empty E.empty_node y b) t in
count_term_binder f c e b
let count_entity f c = function
let print_counters f c =
let terms =
- c.tsorts + c.tgrefs + c.tgrefs + c.tcasts + c.tappls + c.tabsts +
+ c.tsorts + c.tlrefs + c.tgrefs + c.tcasts + c.tappls + c.tabsts +
c.tabbrs
in
let items = c.eabsts + c.eabbrs in
KP.fprintf och "%s" (N.to_string st n)
let rec pp_term st e och = function
- | B.Sort (_, h) ->
- let err _ = KP.fprintf och "*%u" h in
+ | B.Sort k ->
+ let err _ = KP.fprintf och "*%u" k in
let f s = KP.fprintf och "%s" s in
- H.string_of_sort err f h
+ H.string_of_sort err f k
| B.LRef (_, i) ->
let err _ = KP.fprintf och "#%u" i in
if !G.indexes then err () else
- let _, _, a, b = B.get e i in
- KP.fprintf och "%a" (name err) a
+ let _, _, _, y, b = B.get e i in
+ KP.fprintf och "%a" (name err) y
| B.GRef (_, s) ->
let u = U.string_of_uri s in
KP.fprintf och "$%s" (if !G.short then KF.basename u else u)
- | B.Cast (_, u, t) ->
+ | B.Cast (u, t) ->
KP.fprintf och "<%a>.%a" (pp_term st e) u (pp_term st e) t
- | B.Appl (_, _, v, t) ->
+ | B.Appl (_, v, t) ->
KP.fprintf och "(%a).%a" (pp_term st e) v (pp_term st e) t
- | B.Bind (a, B.Abst (r, n, w), t) ->
- let a = R.alpha B.mem e a in
- let ee = B.push e B.empty a (B.abst r n w) in
- KP.fprintf och "%a%a[%a:%a].%a" (pp_level st) n pp_reduced r (name C.start) a (pp_term st e) w (pp_term st ee) t
- | B.Bind (a, B.Abbr v, t) ->
- let a = R.alpha B.mem e a in
- let ee = B.push e B.empty a (B.abbr v) in
- KP.fprintf och "[%a=%a].%a" (name C.start) a (pp_term st e) v (pp_term st ee) t
- | B.Bind (a, B.Void, t) ->
- let a = R.alpha B.mem e a in
- let ee = B.push e B.empty a B.Void in
- KP.fprintf och "[%a].%a" (name C.start) a (pp_term st ee) t
+ | B.Bind (y, B.Abst (r, n, w), t) ->
+ let y = R.alpha B.mem e y in
+ let ee = B.push e B.empty E.empty_node y (B.abst r n w) in
+ KP.fprintf och "%a%a[%a:%a].%a" (pp_level st) n pp_reduced r (name C.start) y (pp_term st e) w (pp_term st ee) t
+ | B.Bind (y, B.Abbr v, t) ->
+ let y = R.alpha B.mem e y in
+ let ee = B.push e B.empty E.empty_node y (B.abbr v) in
+ KP.fprintf och "[%a=%a].%a" (name C.start) y (pp_term st e) v (pp_term st ee) t
+ | B.Bind (y, B.Void, t) ->
+ let y = R.alpha B.mem e y in
+ let ee = B.push e B.empty E.empty_node y B.Void in
+ KP.fprintf och "[%a].%a" (name C.start) y (pp_term st ee) t
let pp_lenv st och e =
- 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
+ let pp_entry f c a y b x =
+ let y = R.alpha B.mem e y in
+ let x = B.push x c a y b in
match b with
| B.Abst (_, _, w) ->
- KP.fprintf och "[%a : %a] " (name C.start) a (pp_term st c) w; f x
+ KP.fprintf och "[%a : %a] " (name C.start) y (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
+ KP.fprintf och "[%a = %a] " (name C.start) y (pp_term st c) v; f x
| B.Void ->
- KP.fprintf och "[%a]" (name C.start) a; f x
+ KP.fprintf och "[%a]" (name C.start) y; f x
in
if e = B.empty then KP.fprintf och "%s" "empty" else
B.fold_right ignore pp_entry e B.empty
(* check closure *)
let are_alpha_convertible err f t1 t2 =
let rec aux f = function
- | B.Sort (_, p1), B.Sort (_, p2)
- | B.LRef (_, p1), B.LRef (_, p2) ->
+ | B.Sort p1, B.Sort p2
+ | B.LRef (_, p1), B.LRef (_, p2) ->
if p1 = p2 then f () else err ()
- | B.GRef (_, u1), B.GRef (_, u2) ->
+ | B.GRef (_, u1), B.GRef (_, u2) ->
if U.eq u1 u2 then f () else err ()
- | B.Cast (_, v1, t1), B.Cast (_, v2, t2)
- | B.Appl (_, _, v1, t1), B.Appl (_, _, v2, t2) ->
+ | B.Cast (v1, t1), B.Cast (v2, t2)
+ | B.Appl (_, v1, t1), B.Appl (_, v2, t2) ->
let f _ = aux f (t1, t2) in
aux f (v1, v2)
- | B.Bind (_, b1, t1), B.Bind (_, b2, t2) ->
+ | B.Bind (_, b1, t1), B.Bind (_, b2, t2) ->
let f _ = aux f (t1, t2) in
aux_bind f (b1, b2)
- | _ -> err ()
+ | _ -> err ()
and aux_bind f = function
| B.Abbr v1, B.Abbr v2 -> aux f (v1, v2)
| B.Abst (r1, n1, v1), B.Abst (r2, n2, v2) when r1 = r2 && n1 = n2 -> aux f (v1, v2)
| None -> 0
let get m i =
- let _, c, a, b = B.get m.e i in c, a, b
+ let _, c, a, _, b = B.get m.e i in c, a, b
(* to share *)
let rec step st m r =
if !G.ct >= 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;
match r with
- | B.Sort (a, h) ->
+ | B.Sort k ->
if assert_tstep m false then
- step st (tstep m) (B.Sort (a, H.apply h))
+ step st (tstep m) (B.Sort (H.apply k))
else m, r, None
- | B.GRef (_, uri) ->
- begin match BE.get_entity uri with
+ | B.GRef (_, u) ->
+ begin match BE.get_entity u with
| _, a, _, E.Abbr v ->
- m, B.gref a uri, Some v
+ m, B.gref a u, Some v
| _, _, _, E.Abst w ->
if assert_tstep m true then begin
if !G.summary then O.add ~grt:1 ();
| _, _, B.Void ->
assert false
end
- | B.Cast (_, u, t) ->
+ | B.Cast (u, t) ->
if assert_tstep m false then begin
if !G.summary then O.add ~e:1 ();
step st (tstep m) u
if !G.summary then O.add ~epsilon:1 ();
step st m t
end
- | B.Appl (_, _, v, t) ->
+ | B.Appl (_, v, t) ->
step st {m with s = (m.e, v) :: m.s} t
- | B.Bind (a, B.Abst (false, n, w), t) ->
+ | B.Bind (y, B.Abst (false, n, w), t) ->
let i = tsteps m in
if !G.summary then O.add ~x:i ();
let n = if i = 0 then n else N.minus st n i in
- let r = B.Bind (a, B.Abst (true, n, w), t) in
+ let r = B.Bind (y, B.Abst (true, n, w), t) in
step st m r
- | B.Bind (a, B.Abst (true, n, w), t) ->
+ | B.Bind (y, B.Abst (true, n, w), t) ->
if !G.si || N.is_not_zero st n then begin match m.s with
| [] ->
- m, B.Bind (a, B.Abst (true, n, w), t), None
+ m, B.Bind (y, B.Abst (true, n, w), t), None
| (c, v) :: s ->
if !G.summary then O.add ~beta:1 ~theta:(List.length s) ();
- let v = B.Cast (E.empty_node, w, v) in
- let e = B.push m.e c a (B.abbr v) in
+ let v = B.Cast (w, v) in
+ let e = B.push m.e c E.empty_node y (B.abbr v) in
step st {m with e = e; s = s} t
end else begin
if !G.summary then O.add ~upsilon:1 ();
- let e = B.push m.e m.e a B.Void in (**) (* this is wrong in general *)
+ let e = B.push m.e m.e E.empty_node y B.Void in (**) (* this is wrong in general *)
step st {m with e = e} t
end
- | B.Bind (a, b, t) ->
+ | B.Bind (y, b, t) ->
if !G.summary then O.add ~theta:(List.length m.s) ();
- let e = B.push m.e m.e a b in
+ let e = B.push m.e m.e E.empty_node y b in
step st {m with e = e} t
let assert_iterations m1 m2 =
let reset m ?(e=m.e) n =
{m with e = e; n = n; s = []}
-let push m a b =
+let push m y b =
let a, l = match b with
- | B.Abst _ -> {a with E.n_apix = m.l}, succ m.l
- | _ -> a, m.l
+ | B.Abst _ -> E.node_attrs ~apix:m.l (), succ m.l
+ | _ -> E.empty_node, m.l
in
- let e = B.push m.e m.e a b in
+ let e = B.push m.e m.e a y b in
{m with e = e; l = l}
let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) =
if !G.ct >= level then log2 st "Now converting nfs" m1.e t1 m2.e t2;
match t1, r1, t2, r2 with
- | B.Sort (_, h1), _, B.Sort (_, h2), _ ->
- h1 = h2
+ | B.Sort k1, _, B.Sort k2, _ ->
+ k1 = k2
| B.LRef ({E.n_apix = e1}, _), _,
B.LRef ({E.n_apix = e2}, _), _ ->
if e1 = e2 then ac_stacks st m1 m2 else false
| B.GRef _, Some v1, _, _ ->
if !G.summary then O.add ~gdelta:1 ();
ac_nfs st (step st m1 v1) (m2, t2, r2)
- | B.Bind (a1, (B.Abst (true, n1, w1) as b1), t1), _,
- B.Bind (a2, (B.Abst (true, n2, w2) as b2), t2), _ ->
+ | B.Bind (y1, (B.Abst (true, n1, w1) as b1), t1), _,
+ B.Bind (y2, (B.Abst (true, n2, w2) as b2), t2), _ ->
if ((!G.cc && N.assert_equal st n1 n2) || N.are_equal st n1 n2) &&
ac st (reset m1 zero) w1 (reset m2 zero) w2
- then ac st (push m1 a1 b1) t1 (push m2 a2 b2) t2
+ then ac st (push m1 y1 b1) t1 (push m2 y2 b2) t2
else false
- | B.Sort _, _, B.Bind (a, B.Abst (true, n, _), t), _ ->
+ | B.Sort _, _, B.Bind (y, B.Abst (true, n, _), t), _ ->
if !G.si then
if !G.cc && not (N.assert_zero st n) then false else begin
if !G.summary then O.add ~upsilon:1 ();
- ac st (push m1 a B.Void) t1 (push m2 a B.Void) t end
+ ac st (push m1 y B.Void) t1 (push m2 y B.Void) t end
else false
| _ -> false
let get m i =
assert (m.s = []);
- let _, _, _, b = B.get m.e i in b
+ let _, _, _, _, b = B.get m.e i in b
let xwhd st m n t =
if !G.ct >= level then log1 st "Now scanning" m.e t;
val get: rtm -> int -> Brg.bind
-val push: rtm -> Entity.node_attrs -> Brg.bind -> rtm
+val push: rtm -> Entity.bind_attrs -> Brg.bind -> rtm
val xwhd: Layer.status -> rtm -> int option -> Brg.term -> rtm * Brg.term
| 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.Appl (_, _, u, 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.Abst (r, n, w) -> B.Abst (r, 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
+ | B.Sort _ as t -> t
+ | B.GRef _ as t -> t
| B.LRef (a, i) as t -> if i < d then t else map d a i
- | B.Cast (a, w, v) -> B.Cast (a, iter_term d w, iter_term d v)
- | B.Appl (a, x, w, u) -> B.Appl (a, x, iter_term d w, iter_term d u)
- | B.Bind (a, b, u) -> B.Bind (a, iter_bind d b, iter_term (succ d) u)
+ | B.Cast (w, v) -> B.Cast (iter_term d w, iter_term d v)
+ | B.Appl (x, w, u) -> B.Appl (x, iter_term d w, iter_term d u)
+ | B.Bind (y, b, u) -> B.Bind (y, iter_bind d b, iter_term (succ d) u)
in
iter_term d
error3 err m v w ~mu u
| _ -> assert false (**)
-let rec b_type_of err f st m y =
- if !G.ct >= level then log1 st "Now checking" m y;
- match y with
- | B.Sort (a, h) ->
- let h = H.apply h in f y (B.Sort (a, h))
+let rec b_type_of err f st m z =
+ if !G.ct >= level then log1 st "Now checking" m z;
+ match z with
+ | B.Sort k ->
+ let k = H.apply k in f z (B.Sort k)
| B.LRef (_, i) ->
begin match BR.get m i with
- | B.Abst (_, _, w) ->
- f y (BS.lift (succ i) (0) w)
- | B.Abbr (B.Cast (_, w, _)) ->
- f y (BS.lift (succ i) (0) w)
- | B.Abbr _ -> assert false
- | B.Void ->
- error1 err "reference to excluded variable" m y
+ | B.Abst (_, _, w) ->
+ f z (BS.lift (succ i) (0) w)
+ | B.Abbr (B.Cast (w, _)) ->
+ f z (BS.lift (succ i) (0) w)
+ | B.Abbr _ -> assert false
+ | B.Void ->
+ error1 err "reference to excluded variable" m z
end
- | B.GRef (_, uri) ->
- begin match BE.get_entity uri with
- | _, _, _, E.Abst w -> f y w
- | _, _, _, E.Abbr (B.Cast (_, w, _)) -> f y w
- | _, _, _, E.Abbr _ -> assert false
- | _, _, _, E.Void ->
- error1 err "reference to unknown entry" m y
+ | B.GRef (_, u) ->
+ begin match BE.get_entity u with
+ | _, _, _, E.Abst w -> f z w
+ | _, _, _, E.Abbr (B.Cast (w, _)) -> f z w
+ | _, _, _, E.Abbr _ -> assert false
+ | _, _, _, E.Void ->
+ error1 err "reference to unknown entry" m z
end
- | B.Bind (a, B.Abbr v, t) ->
+ | B.Bind (y, B.Abbr v, t) ->
let f rv rt tt =
- f (S.sh2 v rv t rt y (B.bind_abbr a)) (B.bind_abbr a rv tt)
+ f (S.sh2 v rv t rt z (B.bind_abbr y)) (B.bind_abbr y rv tt)
in
let f rv m = b_type_of err (f rv) st m t in
- let f rv = f rv (BR.push m a (B.abbr rv)) in
+ let f rv = f rv (BR.push m y (B.abbr rv)) in
let f rv vv = match rv with
| B.Cast _ -> f rv
- | _ -> f (B.Cast (E.empty_node, vv, rv))
+ | _ -> f (B.Cast (vv, rv))
in
type_of err f st m v
- | B.Bind (a, B.Abst (r, n, u), t) ->
+ | B.Bind (y, B.Abst (r, n, u), t) ->
let f ru rt tt =
- f (S.sh2 u ru t rt y (B.bind_abst r n a)) (B.bind_abst r (N.minus st n 1) a ru tt)
+ f (S.sh2 u ru t rt z (B.bind_abst r n y)) (B.bind_abst r (N.minus st n 1) y ru tt)
in
let f ru m = b_type_of err (f ru) st m t in
- let f ru _ = f ru (BR.push m a (B.abst r n ru)) in
+ let f ru _ = f ru (BR.push m y (B.abst r n ru)) in
type_of err f st m u
- | B.Bind (a, B.Void, t) ->
+ | B.Bind (y, B.Void, t) ->
let f rt tt =
- f (S.sh1 t rt y (B.bind_void a)) (B.bind_void a tt)
+ f (S.sh1 t rt z (B.bind_void y)) (B.bind_void y tt)
in
- b_type_of err f st (BR.push m a B.Void) t
- | B.Appl (a, x, v, t) ->
+ b_type_of err f st (BR.push m y B.Void) t
+ | B.Appl (x, v, t) ->
let f rv vv rt tt =
- let f _ = f (S.sh2 v rv t rt y (B.appl a x)) (B.appl a x rv tt) in
+ let f _ = f (S.sh2 v rv t rt z (B.appl x)) (B.appl x rv tt) in
assert_applicability err f st m x tt vv rv
in
let f rv vv = b_type_of err (f rv vv) st m t in
type_of err f st m v
- | B.Cast (a, u, t) ->
+ | B.Cast (u, t) ->
let f ru rt tt =
- let f _ = f (S.sh2 u ru t rt y (B.cast a)) ru in
+ let f _ = f (S.sh2 u ru t rt z (B.cast)) ru in
assert_convertibility err f st m ru tt rt
in
let f ru _ = b_type_of err (f ru) st m t in
let f xt tt =
let xt = match xt with
| B.Cast _ -> xt
- | _ -> B.Cast (E.empty_node, tt, xt)
+ | _ -> B.Cast (tt, xt)
in
let e = BE.set_entity (ra, na, uri, E.Abbr xt) in f tt e
in
let uri, t = match e with
| _, _, uri, E.Abst t -> uri, t
| _, _, uri, E.Abbr t -> uri, t
- | _, _, _, E.Void -> assert false
+ | _, _, _, E.Void -> assert false
in
let err msg = err (L.Uri uri :: msg) in
let f () = let _ = BE.set_entity e in f () in
| _, _, _, E.Void ->
error1 err "reference to unknown entry" m y
end
- | B.Bind (a, b, t) ->
- let f () = b_validate err f st (BR.push m a b) t in
+ | B.Bind (y, b, t) ->
+ let f () = b_validate err f st (BR.push m y b) t in
begin match b with
| B.Abst (_, n, u) -> validate err f st m u
| B.Abbr v -> validate err f st m v
| B.Void -> f ()
end
- | B.Appl (_, x, v, t) ->
+ | B.Appl (x, v, t) ->
let f () = assert_applicability err f st m x v t in
let f () = b_validate err f st m t in
validate err f st m v
- | B.Cast (_, u, t) ->
+ | B.Cast (u, t) ->
let f () = assert_convertibility err f st m u t in
let f () = b_validate err f st m t in
validate err f st m u
let rec alpha mem x a =
let err () = a in
- let f () = match a.E.n_name with
+ let f () = match a.E.b_name with
| None -> a
- | Some (token, mode) -> alpha mem x {a with E.n_name = Some (token ^ "_", mode)}
+ | Some (token, mode) -> alpha mem x {a with E.b_name = Some (token ^ "_", mode)}
in
mem err f x a
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-val alpha: ((unit -> Entity.node_attrs) -> (unit -> Entity.node_attrs) ->
- 'a -> Entity.node_attrs -> Entity.node_attrs
+val alpha: ((unit -> Entity.bind_attrs) -> (unit -> Entity.bind_attrs) ->
+ 'a -> Entity.bind_attrs -> Entity.bind_attrs
) ->
- 'a -> Entity.node_attrs -> Entity.node_attrs
+ 'a -> Entity.bind_attrs -> Entity.bind_attrs
| Private (* private global definition *)
type node_attrs = {
- n_name: name option; (* name *)
- n_apix: int; (* additional position index *)
- n_main: arity; (* main arity *)
- n_side: arity; (* side arity *)
+ n_apix: int; (* additional position index *)
+}
+
+type bind_attrs = {
+ b_name: name option; (* name *)
+ b_main: arity; (* main arity *)
+ b_side: arity; (* side arity *)
}
type root_attrs = {
(* helpers ******************************************************************)
-let node_attrs ?name ?(main=(0,0)) ?(side=(0,0)) () = {
- n_apix = 0; n_name = name; n_main = main; n_side = side;
+let node_attrs ?(apix=0) () = {
+ n_apix = apix;
+}
+
+let bind_attrs ?name ?(main=(0,0)) ?(side=(0,0)) () = {
+ b_name = name; b_main = main; b_side = side;
}
let root_attrs ?(meta=[]) ?info () = {
let empty_node = node_attrs ()
+let empty_bind = bind_attrs ()
+
let empty_root = root_attrs ()
let common f (ra, na, u, _) = f ra na u
let succ (sort, degr) = sort, succ degr
-let compose av at = {av with n_main = at.n_main}
+let compose av at = {av with b_main = at.b_main}
-let shift av = {av with n_side = av.n_main}
+let shift av = {av with b_side = av.b_main}
-let rec name err f a = match a.n_name with
+let rec name err f a = match a.b_name with
| Some (n, r) -> f n r
| None -> err ()
type uri = E.uri
type id = E.id
-type attrs = E.node_attrs
+type n_attrs = E.node_attrs
+type b_attrs = E.bind_attrs
-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 * bool * term * term (* attrs, extended?, argument, function *)
- | TBind of attrs * bind * term (* attrs, binder, scope *)
- | TProj of attrs * lenv * term (* attrs, closure, member *)
+type bind = Abst of bool * N.layer * term (* x-reduced?, layer, type *)
+ | Abbr of term (* body *)
+ | Void (* *)
-and lenv = ESort (* top *)
- | EBind of lenv * attrs * bind (* environment, attrs, binder *)
- | EAppl of lenv * attrs * bool * term (* environment, attrs, extended?, argument *)
- | EProj of lenv * attrs * lenv (* environment, attrs, closure *)
+and term = TSort of int (* hierarchy index *)
+ | TLRef of n_attrs * int (* attrs, position indexe *)
+ | TGRef of n_attrs * uri (* attrs, reference *)
+ | TCast of term * term (* domain, element *)
+ | TAppl of bool * term * term (* extended?, argument, function *)
+ | TBind of b_attrs * bind * term (* attrs, binder, scope *)
+ | TProj of lenv * term (* closure, member *)
+
+and lenv = ESort (* top *)
+ | EBind of lenv * n_attrs * b_attrs * bind (* environment, attrs, binder *)
+ | EAppl of lenv * bool * term (* environment, extended?, argument *)
+ | EProj of lenv * lenv (* environment, closure *)
type entity = term E.entity
let empty_lenv = ESort
-let push_bind f a b lenv = f (EBind (lenv, a, b))
+let push_bind f a y b lenv = f (EBind (lenv, a, y, b))
-let push_appl f a x t lenv = f (EAppl (lenv, a, x, t))
+let push_appl f x t lenv = f (EAppl (lenv, x, t))
-let push_proj f a e lenv = f (EProj (lenv, a, e))
+let push_proj f e lenv = f (EProj (lenv, e))
-let add_bind f a b t = f (TBind (a, b, t))
+let add_bind f y b t = f (TBind (y, b, t))
-let add_appl f a x v t = f (TAppl (a, x, v, t))
+let add_appl f x v t = f (TAppl (x, v, t))
-let add_proj f a e t = f (TProj (a, e, t))
+let add_proj f e t = f (TProj (e, t))
let rec shift f c t = match c with
| ESort -> f t
- | EBind (e, a, b) -> add_bind (shift f e) a b t
- | EAppl (e, a, x, v) -> add_appl (shift f e) a x v t
- | EProj (e, a, d) -> add_proj (shift f e) a d t
+ | EBind (e, _, y, b) -> add_bind (shift f e) y b t
+ | EAppl (e, x, v) -> add_appl (shift f e) x v t
+ | EProj (e, d) -> add_proj (shift f e) d t
let rec append f c = function
| ESort -> f c
- | EBind (e, a, b) -> append (push_bind f a b) c e
- | EAppl (e, a, x, t) -> append (push_appl f a x t) c e
- | EProj (e, a, d) -> append (push_proj f a d) c e
+ | EBind (e, a, y, b) -> append (push_bind f a y b) c e
+ | EAppl (e, x, t) -> append (push_appl f x t) c e
+ | EProj (e, d) -> append (push_proj f d) c e
let resolve_lref err f id lenv =
let rec aux i = function
| ESort -> err ()
- | EAppl (tl, _, _, _) -> aux i tl
- | EBind (tl, a, _) ->
- let f id0 _ = if id0 = id then f a i else aux (succ i) tl in
+ | EAppl (tl, _, _) -> aux i tl
+ | EBind (tl, a, y, _) ->
+ let f id0 _ = if id0 = id then f a y i else aux (succ i) tl in
let err () = aux (succ i) tl in
- E.name err f a
- | EProj (tl, _, d) -> append (aux i) tl d
+ E.name err f y
+ | EProj (tl, d) -> append (aux i) tl d
in
aux 0 lenv
let rec get_name err f i = function
- | ESort -> err i
- | EAppl (tl, _, _, _) -> get_name err f i tl
- | EBind (_, a, _) when i = 0 ->
+ | ESort -> err i
+ | EAppl (tl, _, _) -> get_name err f i tl
+ | EBind (_, _, y, _) when i = 0 ->
let err () = err i in
- E.name err f a
- | EBind (tl, _, _) -> get_name err f (pred i) tl
- | EProj (tl, _, e) ->
+ E.name err f y
+ | EBind (tl, _, _, _) -> get_name err f (pred i) tl
+ | EProj (tl, e) ->
let err i = get_name err f i tl in
get_name err f i e
let rec get e i = match e with
- | 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
- | EProj (e, _, d) -> get (append C.start e d) i
+ | ESort -> ESort, E.empty_node, E.empty_bind, Void
+ | EBind (e, a, y, b) when i = 0 -> e, a, y, b
+ | EBind (e, _, _, _) -> get e (pred i)
+ | EAppl (e, _, _) -> get e i
+ | EProj (e, d) -> get (append C.start e d) i
let rec sub_list_strict f e l = match e, l with
- | _, [] -> f e
- | EBind (e, _, Abst _), _ :: tl -> sub_list_strict f e tl
- | _ -> assert false
+ | _, [] -> f e
+ | EBind (e, _, _, Abst _), _ :: tl -> sub_list_strict f e tl
+ | _ -> 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
+ | ESort -> f x
+ | EBind (e, _, {E.b_name = Some n}, Abst _) -> fold_names f map (map x n) e
+ | _ -> assert false
-let rec mem err f e b = match e with
+let rec mem err f e y0 = 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
+ | EBind (e, _, y, _) ->
+ if y.E.b_name = y0.E.b_name then f () else mem err f e y0
+ | EAppl (e, _, _) -> mem err f e y0
+ | EProj (e, d) ->
+ let err () = mem err f e y0 in mem err f d y0
let set_layer f n0 e =
let rec aux f = function
- | ESort -> f ESort
- | EBind (e, a, Abst (r, n, w)) -> aux (push_bind f a (Abst (r, n0, w))) e
- | EBind (e, a, b) -> aux (push_bind f a b) e
- | EAppl (e, a, x, v) -> aux (push_appl f a x 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, y, Abst (r, n, w)) -> aux (push_bind f a y (Abst (r, n0, w))) e
+ | EBind (e, a, y, b) -> aux (push_bind f a y b) e
+ | EAppl (e, x, v) -> aux (push_appl f x v) e
+ | EProj (e, d) -> let f d = aux (push_proj f d) e in aux f d
in
aux f e
-let set_attrs f a0 e =
+let set_attrs f y0 e =
let rec aux f = function
| ESort -> f ESort
- | EBind (e, a, b) ->
- let a = E.compose a a0 in
- aux (push_bind f a b) e
- | EAppl (e, a, x, v) ->
- let a = E.compose a a0 in
- aux (push_appl f a x v) e
- | EProj (e, a, d) ->
- let a = E.compose a a0 in
- let f d = aux (push_proj f a d) e in
+ | EBind (e, a, y, b) ->
+ let y = E.compose y y0 in
+ aux (push_bind f a y b) e
+ | EAppl (e, x, v) ->
+ aux (push_appl f x v) e
+ | EProj (e, d) ->
+ let f d = aux (push_proj f d) e in
aux f d
in
aux f e
}
let rec count_term f c e = function
- | D.TSort _ ->
+ | D.TSort _ ->
f {c with tsorts = succ c.tsorts; nodes = succ c.nodes}
- | D.TLRef (_, i) ->
+ | D.TLRef (_, i) ->
begin match D.get e i with
- | _, _, D.Abbr _ ->
+ | _, _, _, D.Abbr _ ->
f {c with tlrefs = succ c.tlrefs; xnodes = succ c.xnodes}
- | _ ->
+ | _ ->
f {c with tlrefs = succ c.tlrefs; nodes = succ c.nodes}
end
- | D.TGRef (_, u) ->
+ | D.TGRef (_, u) ->
let c =
if C.list_mem ~eq:U.eq u c.uris
then {c with nodes = succ c.nodes}
else {c with xnodes = succ c.xnodes}
in
f {c with tgrefs = succ c.tgrefs}
- | D.TCast (_, v, t) ->
+ | D.TCast (v, t) ->
let c = {c with tcasts = succ c.tcasts} in
let f c = count_term f c e t in
count_term f c e v
- | D.TAppl (_, _, v, t) ->
+ | D.TAppl (_, v, t) ->
let c = {c with tappls = succ c.tappls} in
let f c = count_term f c e t in
count_term f c e v
- | D.TProj (_, d, t) ->
+ | D.TProj (d, t) ->
D.shift (count_term f c e) d t
- | D.TBind (a, b, t) ->
+ | D.TBind (y, b, t) ->
let f c e = count_term f c e t in
- count_binder f c e a b
+ count_binder f c e y b
-and count_binder f c e a b = match b with
+and count_binder f c e y b = match b with
| 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
+ let f c = D.push_bind (f c) E.empty_node y b e in
count_term f c e w
| 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
+ let f c = D.push_bind (f c) E.empty_node y b e in
count_term f c e v
| D.Void ->
let c = {c with tvoids = succ c.tvoids; xnodes = succ c.xnodes} in
- D.push_bind (f c) a b e
+ D.push_bind (f c) E.empty_node y b e
let count_entity f c = function
| _, _, u, E.Abst w ->
(* term/environment pretty printer ******************************************)
-let pp_attrs out a =
+let pp_b_attrs out a =
let f s b = if b then out (KP.sprintf "%s;" s) else out (KP.sprintf "~%s;" s) in
- E.name ignore f a;
+ E.name ignore f a
+
+let pp_n_attrs out 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, 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
+ | D.TSort k -> out (KP.sprintf "*%u" k)
+ | D.TLRef (a, i) -> pp_n_attrs out a; out (KP.sprintf "#%u" i)
+ | D.TGRef (a, u) -> pp_n_attrs out a; out (KP.sprintf "$")
+ | D.TCast (u, t) -> out "<"; pp_term out st u; out ">."; pp_term out st t
+ | D.TAppl (_, u, t) -> out "("; pp_term out st u; out ")."; pp_term out st t
+ | D.TBind (y, u, t) -> pp_b_attrs out y; pp_bind out st u; out "."; pp_term out st t
+ | D.TProj (u, t) -> out "{"; pp_lenv out st u; out "}."; pp_term out st t
and pp_bind out st = function
| D.Abst (r, n, u) ->
and pp_lenv out st = function
| D.ESort -> ()
- | 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 "} "
+ | D.EBind (u, a, y, t) -> pp_lenv out st u; pp_b_attrs out y; pp_n_attrs out a; pp_bind out st t
+ | D.EAppl (u, _, t) -> pp_lenv out st u; out "("; pp_term out st t; out ") "
+ | D.EProj (u, t) -> pp_lenv out st u; out "{"; pp_lenv out st t; out "} "
(* Internal functions *******************************************************)
-let mk_lref f a i = f a (D.TLRef (a, i))
+let mk_lref f a y i = f y (D.TLRef (a, i))
-let mk_gref f a uri = f a (D.TGRef (a, uri))
+let mk_gref f y uri = f y (D.TGRef (E.empty_node, uri))
let get err f e i = match D.get e i with
- | _, _, D.Void -> err ()
- | _, a, _ -> mk_lref f a i
+ | _, _, _, D.Void -> err ()
+ | _, a, y, _ -> mk_lref f a y i
let resolve_gref err f st id =
try
- let a, uri = KH.find henv id in f a uri
+ let y, uri = KH.find henv id in f y uri
with Not_found -> err ()
let name_of_id ?(r=true) id =
CrgOutput.pp_lenv print_string (Layer.initial_status ()) lenv;
Printf.printf "\n";
*)
- | T.Sort h ->
- let a = E.node_attrs ~main:(h, 0) () in
- f a (D.TSort (a, h))
+ | T.Sort k ->
+ let y = E.bind_attrs ~main:(k, 0) () in
+ f y (D.TSort k)
| T.NSrt id ->
let f h = xlate_term f st lenv (T.Sort h) in
H.sort_of_string (xerr "sort not found") f id
let err () = resolve_gref (xerr "global constant not found") (mk_gref f) st id in
D.resolve_lref err (mk_lref f) id lenv
| T.Cast (u, t) ->
- let f uu a tt = f a (D.TCast (a, uu, tt)) in
+ let f uu y tt = f y (D.TCast (uu, tt)) in
let f _ uu = xlate_term (f uu) st lenv t in
xlate_term f st lenv u
| T.Appl (v, t) ->
- let f vv a tt = f a (D.TAppl (a, st.ext, vv, tt)) in
+ let f vv y tt = f y (D.TAppl (st.ext, vv, tt)) in
let f _ vv = xlate_term (f vv) st lenv t in
xlate_term f st lenv v
| T.Proj (bs, t) ->
- let f e a tt = f a (D.TProj (a, e, tt)) in
+ let f e y tt = f y (D.TProj (e, tt)) in
let f (lenv, e) = xlate_term (f e) st lenv t in
C.list_fold_left f (xlate_bind st) (lenv, D.empty_lenv) bs
| T.Inst (t, vs) ->
let map f v e =
- let f _ vv = D.push_appl f E.empty_node st.ext vv e in
+ let f _ vv = D.push_appl f st.ext vv e in
xlate_term f st lenv v
in
- let f e a tt = f a (D.TProj (a, e, tt)) in
+ let f e y tt = f y (D.TProj (e, tt)) in
let f e = xlate_term (f e) st lenv t in
C.list_fold_right f map vs D.empty_lenv
and xlate_bind st f (lenv, e) b =
let f lenv e = f (lenv, e) in
- let f a b lenv = D.push_bind (f lenv) a b e in
- let f a b = D.push_bind (f a b) a b lenv in
+ let f y b lenv = D.push_bind (f lenv) E.empty_node y b e in
+ let f y b = D.push_bind (f y b) E.empty_node y b lenv in
match b with
| 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 (false, n, ww))
+ let f y ww =
+ let y = E.bind_attrs ?name:(name_of_id id) () in
+ f y (D.Abst (false, n, ww))
in
xlate_term f st lenv w
| T.Abbr (id, v) ->
- let f a vv =
- let a = {a with E.n_name = name_of_id id} in
- f a (D.Abbr vv)
+ let f y vv =
+ let y = E.bind_attrs ?name:(name_of_id id) () in
+ f y (D.Abbr vv)
in
xlate_term f st lenv v
| T.Void id ->
- let a = E.node_attrs ?name:(name_of_id id) ~main:(st.sort, 0) () in
- f a D.Void
+ let y = E.bind_attrs ?name:(name_of_id id) ~main:(st.sort, 0) () in
+ f y D.Void
let mk_contents main kind tt =
let ms, b = match kind with
assert (H.set_graph id); err st
| T.Constant (main, kind, id, info, t) ->
let uri = uri_of_id st id st.path in
- let g na tt =
+ let g ya tt =
+ KH.add henv id (ya, uri);
(*
print_newline (); CrgOutput.pp_term print_string tt;
*)
- let na = {na with E.n_apix = st.line} in
- KH.add henv id (na, uri);
let meta, b = mk_contents main kind tt in
+ let na = E.node_attrs ~apix:st.line () in
let ra = E.root_attrs ~meta ~info () in
let entity = ra, na, uri, b in
f {st with line = succ st.line} entity
-
in
xlate_term g st D.empty_lenv t
| T.Generate _ ->
let lenv_iter map_bind map_appl map_proj st e lenv out tab =
let rec aux = function
- | D.ESort -> e
- | D.EBind (e, a, b) ->
+ | D.ESort -> e
+ | D.EBind (e, a, y, 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 st e a b out tab; D.EBind (e, a, b)
- | D.EAppl (e, a, x, v) ->
+ let y = R.alpha D.mem e y in
+ map_bind st e a y b out tab; D.EBind (e, a, y, b)
+ | D.EAppl (e, x, v) ->
let e = aux e in
- map_appl st e a x v out tab; D.EAppl (e, a, x, v)
- | D.EProj (e, a, d) ->
+ map_appl st e x v out tab; D.EAppl (e, x, v)
+ | D.EProj (e, d) ->
let e = aux e in
- map_proj st e a d out tab; D.EProj (e, a, d)
+ map_proj st e d out tab; D.EProj (e, d)
in
ignore (aux lenv)
let rec exp_term st e t out tab = match t with
- | D.TSort (a, h) ->
- let a =
- let err _ = a in
- let f s = {a with E.n_name = Some (s, true)} in
- H.string_of_sort err f h
+ | D.TSort k ->
+ let y =
+ let err _ = E.empty_bind in
+ let f s = E.bind_attrs ~name:(s, true) () in
+ H.string_of_sort err f k
in
- let attrs = [XL.position h; XL.name a] in
+ let attrs = [XL.position k; XL.name y] in
XL.tag XL.sort attrs out tab
- | D.TLRef (a, i) ->
- let a =
- let err _ = a in
- let f n r = {a with E.n_name = Some (n, r)} in
+ | D.TLRef (_, i) ->
+ let y =
+ let err _ = E.empty_bind in
+ let f s r = E.bind_attrs ~name:(s, r) () in
D.get_name err f i e
in
- let attrs = [XL.depth i; XL.name a] in
+ let attrs = [XL.depth i; XL.name y] in
XL.tag XL.lref attrs out tab
- | D.TGRef (a, n) ->
- let a = {a with E.n_name = Some (U.name_of_uri n, true)} in
- let attrs = [XL.uri n; XL.name a] in
+ | D.TGRef (_, n) ->
+ let y = E.bind_attrs ~name:(U.name_of_uri n, true) () in
+ let attrs = [XL.uri n; XL.name y] in
XL.tag XL.gref attrs out tab
- | D.TCast (a, u, t) ->
+ | D.TCast (u, t) ->
let attrs = [] in
XL.tag XL.cast attrs ~contents:(exp_term st e u) out tab;
exp_term st e t out tab
- | D.TAppl (a, x, v, t) ->
+ | D.TAppl (x, v, t) ->
let attrs = [] in
XL.tag (XL.appl x) attrs ~contents:(exp_term st e v) out tab;
exp_term st e t out tab
- | D.TProj (a, lenv, t) ->
+ | D.TProj (lenv, t) ->
let attrs = [] in
XL.tag XL.proj attrs ~contents:(lenv_iter exp_bind exp_appl exp_proj st e lenv) out tab;
- exp_term st (D.push_proj C.start a lenv e) t out tab
- | D.TBind (a, b, t) ->
+ exp_term st (D.push_proj C.start lenv e) t out tab
+ | D.TBind (y, b, t) ->
(* NOTE: the inner binders are alpha-converted first *)
- let a = R.alpha D.mem e a in
- exp_bind st e a b out tab;
- exp_term st (D.push_bind C.start a b e) t out tab
+ let y = R.alpha D.mem e y in
+ exp_bind st e E.empty_node y b out tab;
+ exp_term st (D.push_bind C.start E.empty_node y b e) t out tab
-and exp_appl st e a x v out tab =
+and exp_appl st e x v out tab =
let attrs = [] in
XL.tag (XL.appl x) attrs ~contents:(exp_term st e v) out tab;
-and exp_bind st e a b out tab = match b with
+and exp_bind st e a y b out tab = match b with
| D.Abst (_, n, w) ->
- let attrs = [XL.layer st n; XL.name a] in
+ let attrs = XL.layer st n :: XL.name y :: XL.side y @ XL.main y in
XL.tag XL.abst attrs ~contents:(exp_term st e w) out tab
| D.Abbr v ->
- let attrs = [XL.name a] in
+ let attrs = [XL.name y] in
XL.tag XL.abbr attrs ~contents:(exp_term st e v) out tab
| D.Void ->
- let attrs = [XL.name a] in
+ let attrs = [XL.name y] in
XL.tag XL.void attrs out tab
-and exp_proj st e a lenv out tab =
+and exp_proj st e lenv out tab =
let attrs = [] in
XL.tag XL.proj attrs ~contents:(lenv_iter exp_bind exp_appl exp_proj st e lenv) out tab
"layer", N.to_string st n
let main a =
- let sort, degr = a.E.n_main in
+ let sort, degr = a.E.b_main in
["main-position", string_of_int sort;
"main-degree", string_of_int degr;
]
let side a =
- let sort, degr = a.E.n_side in
+ let sort, degr = a.E.b_side in
["side-position", string_of_int sort;
"side-degree", string_of_int degr;
]
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 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 ba = E.bind_attrs ~name:(U.name_of_uri u, true) () in
+ let attrs = uri u :: name ba :: apix na :: meta ra :: info ra in
let contents = match b with
| E.Abst w -> tag "GDec" attrs ~contents:(pp_term w)
| E.Abbr v -> tag "GDef" attrs ~contents:(pp_term v)
val layer: Layer.status -> Layer.layer -> attr
-val name: Entity.node_attrs -> attr
+val name: Entity.bind_attrs -> attr
-val main: Entity.node_attrs -> attr list
+val main: Entity.bind_attrs -> attr list
-val side: Entity.node_attrs -> attr list
+val side: Entity.bind_attrs -> attr list
val apix: Entity.node_attrs -> attr
projects / helm.git / commitdiff