CLEAN = etc/log.txt
-TAGS = test test-si test-si-fast hal xml-si-drg xml-si-old
+TAGS = test test-si test-si-fast hal xml-si-drg xml-si-old profile
XMLS = xml/brg/grundlagen/l/not.ld.xml xml/brg/grundlagen/l/et.ld.xml \
xml/brg/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \
@echo " HELENA -o -r -u $(INPUT)"
$(H)./$(MAIN).opt -o -r -u -S 1 $(O) $(INPUT) > etc/log.txt
+profile: $(MAIN).opt
+ @echo " HELENA -r -u $(INPUT) (30 TIMES)"
+ $(H)for T in `seq 30`; do ./$(MAIN).opt -r -u -S 1 $(O) automath/grundlagen.aut >> etc/log.txt; done
+ $(H)grep "at exit" etc/log.txt | sort | uniq | less
+
hal: $(MAIN).opt
@echo " HELENA -o -x -m $(INPUT)"
$(H)./$(MAIN).opt -o -x -m -s 1 -S 1 $(INPUT) > etc/log.txt
type id = Entity.id
type attrs = Entity.attrs
-type bind = Void of attrs (* attrs *)
- | Abst of attrs * term (* attrs, type *)
- | Abbr of attrs * term (* attrs, body *)
+type bind = Void (* *)
+ | Abst of term (* 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 * term * term (* attrs, argument, function *)
- | Bind of bind * term (* binder, scope *)
+ | Bind of attrs * bind * term (* attrs, binder, scope *)
type entity = term Entity.entity (* attrs, uri, binder *)
type lenv = Null
-(* Cons: tail, relative local environment, binder *)
- | Cons of lenv * lenv option * bind
+(* Cons: tail, relative local environment, attrs, binder *)
+ | Cons of lenv * lenv * attrs * bind
(* helpers ******************************************************************)
(* Currified constructors ***************************************************)
-let abst a w = Abst (a, w)
+let abst w = Abst w
-let abbr a v = Abbr (a, v)
+let abbr v = Abbr v
let lref a i = LRef (a, i)
let appl a u t = Appl (a, u, t)
-let bind b t = Bind (b, t)
+let bind a b t = Bind (a, b, t)
-let bind_abst a u t = Bind (Abst (a, u), t)
+let bind_abst a u t = Bind (a, Abst u, t)
-let bind_abbr a v t = Bind (Abbr (a, v), t)
+let bind_abbr a v t = Bind (a, Abbr v, t)
+
+let bind_void a t = Bind (a, Void, t)
(* local environment handling functions *************************************)
-let empty_lenv = Null
+let empty = Null
+
+let push e c a b = Cons (e, c, a, b)
-let push es ?c b = Cons (es, c, b)
+let rec get i = function
+ | Null -> Null, Null, [], Void
+ | Cons (e, c, a, b) when i = 0 -> e, c, a, b
+ | Cons (e, _, _, _) -> get (pred i) e
-let get err f es i =
- let rec aux j = function
- | Null -> err ()
- | Cons (tl, None, b) when j = 0 -> f tl b
- | Cons (_, Some c, b) when j = 0 -> f c b
- | Cons (tl, _, _) -> aux (pred j) tl
- in
- aux i es
+let get e i = get i e
-(* check closure *)
-let rec rev_iter f map = function
- | Null -> f ()
- | Cons (tl, None, b) ->
- let f _ = map f tl b in rev_iter f map tl
- | Cons (tl, Some c, b) ->
- let f _ = map f c b in rev_iter f map tl
+(* 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
+(* used in MetaBrg.unwind_to_xlate_term *)
let rec fold_left map x = function
- | Null -> x
- | Cons (tl, _, b) -> fold_left map (map x b) tl
+ | Null -> x
+ | Cons (e, _, a, b) -> fold_left map (map x a b) e
}
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
| B.Sort _ ->
f {c with tsorts = succ c.tsorts; nodes = succ c.nodes}
| B.LRef (_, i) ->
- let err _ = f {c with tlrefs = succ c.tlrefs; nodes = succ c.nodes} in
- let f _ = function
- | B.Abst _
- | B.Void _ ->
+ begin match B.get e i with
+ | _, _, _, 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}
- in
- B.get err f e i
+ end
| B.GRef (_, u) ->
let c =
if Cps.list_mem ~eq:U.eq u c.uris
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 (b, t) ->
- let f c = count_term f c (B.push e b) t in
+ | B.Bind (a, b, t) ->
+ let f c = count_term f c (B.push e B.empty a b) t in
count_term_binder f c e b
let count_entity f c = function
let c = {c with
eabsts = succ c.eabsts; nodes = succ c.nodes; uris = u :: c.uris
} in
- count_term f c B.empty_lenv w
+ count_term f c B.empty w
| _, _, Y.Abbr v ->
let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in
- count_term f c B.empty_lenv v
- | _, _, Y.Void -> assert false
+ count_term f c B.empty v
+ | _, _, Y.Void -> assert false
let print_counters f c =
let terms =
(* supplementary annotation *************************************************)
-let attrs_of_binder f = function
- | B.Abst (a, _)
- | B.Abbr (a, _)
- | B.Void a -> f a
-
let rec does_not_occur f n r = function
- | B.Null -> f true
- | B.Cons (c, _, b) ->
+ | B.Null -> f true
+ | B.Cons (e, _, a, _) ->
let f n1 r1 =
- if n1 = n && r1 = r then f false else does_not_occur f n r c
+ if n1 = n && r1 = r then f false else does_not_occur f n r e
in
- attrs_of_binder (Y.name C.err f) b
+ Y.name C.err f a
-let rename f c a =
- let rec aux f c n r =
+let rename f e a =
+ let rec aux f e n r =
let f = function
| true -> f n r
- | false -> aux f c (n ^ "'") r
+ | false -> aux f e (n ^ "'") r
in
- does_not_occur f n r c
+ does_not_occur f n r e
in
let f n0 r0 =
let f n r = if n = n0 && r = r0 then f a else f (Y.Name (n, r) :: a) in
- aux f c n0 r0
+ aux f e n0 r0
in
Y.name C.err f a
-let rename_bind f c = function
- | B.Abst (a, w) -> let f a = f (B.abst a w) in rename f c a
- | B.Abbr (a, v) -> let f a = f (B.abbr a v) in rename f c a
- | B.Void a -> let f a = f (B.Void a) in rename f c a
-
(* lenv/term pretty printing ************************************************)
-let name frm a =
+let name err frm a =
let f n = function
| true -> F.fprintf frm "%s" n
| false -> F.fprintf frm "^%s" n
in
- Y.name C.err f a
+ Y.name err f a
-let rec pp_term c frm = function
- | B.Sort (_, h) ->
+let rec pp_term e frm = function
+ | B.Sort (_, h) ->
let err _ = F.fprintf frm "@[*%u@]" h in
let f s = F.fprintf frm "@[%s@]" s in
H.get_sort err f h
- | B.LRef (_, i) ->
+ | B.LRef (_, i) ->
let err _ = F.fprintf frm "@[#%u@]" i in
- let f _ = function
- | B.Abst (a, _)
- | B.Abbr (a, _)
- | B.Void a -> F.fprintf frm "@[%a@]" name a
- in
- if !O.indexes then err () else B.get err f c i
- | B.GRef (_, s) ->
+ if !O.indexes then err () else
+ let _, _, a, b = B.get e i in
+ F.fprintf frm "@[%a@]" (name err) a
+ | B.GRef (_, s) ->
F.fprintf frm "@[$%s@]" (U.string_of_uri s)
- | B.Cast (_, u, t) ->
- F.fprintf frm "@[{%a}.%a@]" (pp_term c) u (pp_term c) t
- | B.Appl (_, v, t) ->
- F.fprintf frm "@[(%a).%a@]" (pp_term c) v (pp_term c) t
- | B.Bind (B.Abst (a, w), t) ->
+ | B.Cast (_, u, t) ->
+ 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) ->
let f a =
- let cc = B.push c (B.abst a w) in
- F.fprintf frm "@[[%a:%a].%a@]" name a (pp_term c) w (pp_term cc) t
+ 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
in
- rename f c a
- | B.Bind (B.Abbr (a, v), t) ->
+ rename f e a
+ | B.Bind (a, B.Abbr v, t) ->
let f a =
- let cc = B.push c (B.abbr a v) in
- F.fprintf frm "@[[%a=%a].%a@]" name a (pp_term c) v (pp_term cc) t
+ let ee = B.push e B.empty a (B.abbr v) in
+ F.fprintf frm "@[[%a=%a].%a@]" (name C.err) a (pp_term e) v (pp_term ee) t
in
- rename f c a
- | B.Bind (B.Void a, t) ->
+ rename f e a
+ | B.Bind (a, B.Void, t) ->
let f a =
- let cc = B.push c (B.Void a) in
- F.fprintf frm "@[[%a].%a@]" name a (pp_term cc) t
+ let ee = B.push e B.empty a B.Void in
+ F.fprintf frm "@[[%a].%a@]" (name C.err) a (pp_term ee) t
in
- rename f c a
+ rename f e a
-let pp_lenv frm c =
- let pp_entry f c = function
+let pp_lenv frm e =
+ let pp_entry f e c a b x = f x (*match b with
| B.Abst (a, w) ->
- let f a = F.fprintf frm "@,@[%a : %a@]" name a (pp_term c) w; f () in
- rename f c a
+ let f a = F.fprintf frm "@,@[%a : %a@]" (name C.err) a (pp_term e) w; f a in
+ rename f x a
| B.Abbr (a, v) ->
- let f a = F.fprintf frm "@,@[%a = %a@]" name a (pp_term c) v; f () in
+ let f a = F.fprintf frm "@,@[%a = %a@]" (name C.err) a (pp_term e) v; f a in
rename f c a
| B.Void a ->
- let f a = F.fprintf frm "@,%a" name a; f () in
+ let f a = F.fprintf frm "@,%a" (name C.err) a; f a in
rename f c a
- in
- B.rev_iter C.start pp_entry c
+*) in
+ B.fold_right ignore pp_entry e B.empty
let specs = {
L.pp_term = pp_term; L.pp_lenv = pp_lenv
X.tag X.sort attrs out tab
| B.LRef (a, i) ->
let a =
- let err _ = a in
+ let err _ = a in
let f n r = Y.Name (n, r) :: a in
- let f _ b = attrs_of_binder (Y.name err f) b in
- B.get err f e i
+ let _, _, a, b = B.get e i in
+ Y.name err f a
in
let attrs = [X.position i; X.name a] in
X.tag X.lref attrs out tab
let attrs = [] in
X.tag X.appl attrs ~contents:(exp_term e v) out tab;
exp_term e t out tab
- | B.Bind (b, t) ->
- let b = rename_bind C.start e b in
- exp_bind e b out tab;
- exp_term (B.push e b) t out tab
+ | B.Bind (a, b, t) ->
+ let a = rename C.start e a in
+ exp_bind e a b out tab;
+ exp_term (B.push e B.empty a b) t out tab
-and exp_bind e b out tab = match b with
- | B.Abst (a, w) ->
+and exp_bind e a b out tab = match b with
+ | B.Abst w ->
let attrs = [X.name a; X.mark a] in
X.tag X.abst attrs ~contents:(exp_term e w) out tab
- | B.Abbr (a, v) ->
+ | B.Abbr v ->
let attrs = [X.name a; X.mark a] in
X.tag X.abbr attrs ~contents:(exp_term e v) out tab
- | B.Void a ->
+ | B.Void ->
let attrs = [X.name a; X.mark a] in
X.tag X.void attrs out tab
-let export_term = exp_term B.empty_lenv
+let export_term = exp_term B.empty
module E = BrgEnvironment
type kam = {
- c: B.lenv;
+ e: B.lenv;
s: (B.lenv * B.term) list;
i: int
}
| 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 ()
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 ()
+ | B.Abbr v1, B.Abbr v2
+ | B.Abst v1, B.Abst v2 -> aux f (v1, v2)
+ | B.Void, B.Void -> f ()
| _ -> err ()
in
if S.eq t1 t2 then f () else aux f (t1, t2)
let get m i =
- let f c b = c, b in
- B.get C.err f m.c i
+ let _, c, a, b = B.get m.e i in c, a, b
(* to share *)
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 E.get_entity uri with
| _, _, Y.Abbr v when st.Y.delta ->
P.add ~gdelta:1 (); step st m v
P.add ~grt:1 (); step st m w
| a, _, Y.Abbr v ->
let e = Y.apix C.err C.start a in
- m, Some (e, B.Abbr (a, v)), x
+ m, Some (e, a, B.Abbr v), x
| a, _, Y.Abst w ->
let e = Y.apix C.err C.start a in
- m, Some (e, B.Abst (a, w)), x
+ m, Some (e, a, B.Abst w), x
| _, _, Y.Void -> assert false
end
- | B.LRef (_, i) ->
+ | B.LRef (_, i) ->
begin match get m i with
- | c, B.Abbr (_, v) ->
+ | c, _, B.Abbr v ->
P.add ~ldelta:1 ();
- step st {m with c = c} v
- | c, B.Abst (_, w) when st.Y.rt ->
+ step st {m with e = c} v
+ | c, _, B.Abst w when st.Y.rt ->
P.add ~lrt:1 ();
- step st {m with c = c} w
- | c, B.Void _ ->
+ step st {m with e = c} w
+ | c, _, B.Void ->
assert false
- | c, (B.Abst (a, _) as b) ->
+ | c, a, (B.Abst _ as b) ->
let e = Y.apix C.err C.start a in
- {m with c = c}, Some (e, b), x
+ {m with e = c}, Some (e, a, b), x
end
- | B.Cast (_, _, t) ->
+ | B.Cast (_, _, t) ->
P.add ~tau:1 ();
step st m t
- | B.Appl (_, v, t) ->
- step st {m with s = (m.c, v) :: m.s} t
- | B.Bind (B.Abst (a, w), t) ->
+ | B.Appl (_, v, t) ->
+ step st {m with s = (m.e, v) :: m.s} t
+ | B.Bind (a, B.Abst w, t) ->
begin match m.s with
| [] -> m, None, x
| (c, v) :: s ->
P.add ~beta:1 ~upsilon:(List.length s) ();
- let c = B.push m.c ~c (B.abbr a v) (* (B.Cast ([], w, v)) *) in
- step st {m with c = c; s = s} t
+ let e = B.push m.e c a (B.abbr v) (* (B.Cast ([], w, v)) *) in
+ step st {m with e = e; s = s} t
end
- | B.Bind (b, t) ->
+ | B.Bind (a, b, t) ->
P.add ~upsilon:(List.length m.s) ();
- let c = B.push m.c ~c:m.c b in
- step st {m with c = c} t
+ let e = B.push m.e m.e a b in
+ step st {m with e = e} t
-let push m b =
+let push m a b =
assert (m.s = []);
- let b, i = match b with
- | B.Abst (a, w) -> B.abst (Y.Apix m.i :: a) w, succ m.i
- | b -> b, m.i
+ let a, i = match b with
+ | B.Abst _ -> Y.Apix m.i :: a, succ m.i
+ | b -> a, m.i
in
- let c = B.push m.c ~c:m.c b in
- {m with c = c; i = i}
+ let e = B.push m.e m.e a b in
+ {m with e = e; i = i}
-let rec ac_nfs st (m1, a1, u) (m2, a2, t) =
- log2 "Now converting nfs" m1.c u m2.c t;
- match a1, u, a2, t with
- | _, B.Sort (_, h1), _, B.Sort (_, h2) ->
+let rec ac_nfs st (m1, r1, u) (m2, r2, t) =
+ log2 "Now converting nfs" m1.e u m2.e t;
+ match r1, u, r2, t with
+ | _, B.Sort (_, h1), _, B.Sort (_, h2) ->
h1 = h2
- | Some (e1, B.Abst _), _, Some (e2, B.Abst _), _ ->
+ | Some (e1, _, B.Abst _), _, Some (e2, _, B.Abst _), _ ->
if e1 = e2 then ac_stacks st m1 m2 else false
- | Some (e1, B.Abbr (_, v1)), _, Some (e2, B.Abbr (_, v2)), _ ->
+ | Some (e1, _, B.Abbr v1), _, Some (e2, _, B.Abbr v2), _ ->
if e1 = e2 then
if ac_stacks st m1 m2 then true else begin
P.add ~gdelta:2 (); ac st m1 v1 m2 v2
end
else if e1 < e2 then begin
P.add ~gdelta:1 ();
- ac_nfs st (m1, a1, u) (step st m2 v2)
+ ac_nfs st (m1, r1, u) (step st m2 v2)
end else begin
P.add ~gdelta:1 ();
- ac_nfs st (step st m1 v1) (m2, a2, t)
+ ac_nfs st (step st m1 v1) (m2, r2, t)
end
- | _, _, Some (_, B.Abbr (_, v2)), _ ->
+ | _, _, Some (_, _, B.Abbr v2), _ ->
P.add ~gdelta:1 ();
- ac_nfs st (m1, a1, u) (step st m2 v2)
- | Some (_, B.Abbr (_, v1)), _, _, _ ->
+ ac_nfs st (m1, r1, u) (step st m2 v2)
+ | Some (_, _, B.Abbr v1), _, _, _ ->
P.add ~gdelta:1 ();
- ac_nfs st (step st m1 v1) (m2, a2, t)
- | _, B.Bind ((B.Abst (_, w1) as b1), t1),
- _, B.Bind ((B.Abst (_, w2) as b2), t2) ->
+ ac_nfs st (step st m1 v1) (m2, r2, t)
+ | _, B.Bind (a1, (B.Abst w1 as b1), t1),
+ _, B.Bind (a2, (B.Abst w2 as b2), t2) ->
if ac {st with Y.si = false} m1 w1 m2 w2 then
- ac st (push m1 b1) t1 (push m2 b2) t2
+ ac st (push m1 a1 b1) t1 (push m2 a2 b2) t2
else false
- | _, B.Sort _, _, B.Bind (b, t) when st.Y.si ->
+ | _, B.Sort _, _, B.Bind (a, b, t) when st.Y.si ->
P.add ~si:1 ();
- ac st (push m1 b) u (push m2 b) t
- | _ -> false
+ ac st (push m1 a b) u (push m2 a b) t
+ | _ -> false
and ac st m1 t1 m2 t2 =
(* L.warn "entering R.are_convertible"; *)
(* L.warn "entering R.are_convertible_stacks"; *)
(* if List.length m1.s <> List.length m2.s then false else *)
let map (c1, v1) (c2, v2) =
- let m1, m2 = {m1 with c = c1; s = []}, {m2 with c = c2; s = []} in
+ let m1, m2 = {m1 with e = c1; s = []}, {m2 with e = c2; s = []} in
ac {st with Y.si = false} m1 v1 m2 v2
in
list_and map (m1.s, m2.s)
(* Interface functions ******************************************************)
let empty_kam = {
- c = B.empty_lenv; s = []; i = 0
+ e = B.empty; s = []; i = 0
}
-let get err f m i =
+let get m i =
assert (m.s = []);
- let f c = f in
- B.get err f m.c i
+ let _, _, _, b = B.get m.e i in b
let xwhd st m t =
- L.box level; log1 "Now scanning" m.c t;
+ L.box level; log1 "Now scanning" m.e t;
let m, _, t = step {st with Y.delta = true; Y.rt = true} m t in
L.unbox level; m, t
let are_convertible st mu u mw w =
- L.box level; log2 "Now converting" mu.c u mw.c w;
+ L.box level; log2 "Now converting" mu.e u mw.e w;
let r = ac {st with Y.delta = false; Y.rt = false} mu u mw w in
L.unbox level; r
(* let err _ = in
(* error reporting **********************************************************)
-let pp_term m frm t = O.specs.L.pp_term m.c frm t
+let pp_term m frm t = O.specs.L.pp_term m.e frm t
-let pp_lenv frm m = O.specs.L.pp_lenv frm m.c
+let pp_lenv frm m = O.specs.L.pp_lenv frm m.e
let specs = {
L.pp_term = pp_term; L.pp_lenv = pp_lenv
val empty_kam: kam
-val get: (unit -> 'a) -> (Brg.bind -> 'a) -> kam -> int -> 'a
+val get: kam -> int -> Brg.bind
-val push: kam -> Brg.bind -> kam
+val push: kam -> Entity.attrs -> Brg.bind -> kam
val xwhd: Entity.status -> kam -> Brg.term -> kam * Brg.term
let iter map d =
let rec iter_bind d = function
- | B.Void _ as b -> b
- | B.Abst (a, w) -> B.Abst (a, iter_term d w)
- | B.Abbr (a, v) -> B.Abbr (a, iter_term d v)
+ | B.Void -> B.Void
+ | B.Abst w -> B.Abst (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.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, w, u) -> B.Appl (a, iter_term d w, iter_term d u)
- | B.Bind (b, u) -> B.Bind (iter_bind d b, iter_term (succ d) u)
+ | B.Bind (a, b, u) -> B.Bind (a, iter_bind d b, iter_term (succ d) u)
in
iter_term d
let lift h d t =
if h = 0 then t else iter (lift_map h) d t
-
-let lift_bind h d = function
- | B.Void _ as b -> b
- | B.Abst (a, w) -> B.abst a (lift h d w)
- | B.Abbr (a, v) -> B.abbr a (lift h d v)
let assert_applicability err f st m u w v =
match R.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 R.are_convertible st mu u m w then f () else
error3 err m v w ~mu u
| _ -> assert false (**)
let rec b_type_of err f st g m x =
log1 "Now checking" m x;
match x with
- | B.Sort (a, h) ->
+ | B.Sort (a, h) ->
let f h = f x (B.Sort (a, h)) in H.apply f g h
- | B.LRef (_, i) ->
- let f = function
- | B.Abst (_, w) ->
+ | B.LRef (_, i) ->
+ begin match R.get m i with
+ | B.Abst w ->
f x (S.lift (succ i) (0) w)
- | B.Abbr (_, B.Cast (_, w, _)) ->
+ | B.Abbr (B.Cast (_, w, _)) ->
f x (S.lift (succ i) (0) w)
- | B.Abbr _ -> assert false
- | B.Void _ ->
+ | B.Abbr _ -> assert false
+ | B.Void ->
error1 err "reference to excluded variable" m x
- in
- let err _ = error1 err "reference to unknown variable" m x in
- R.get err f m i
- | B.GRef (_, uri) ->
+ end
+ | B.GRef (_, uri) ->
begin match E.get_entity uri with
| _, _, Y.Abst w -> f x w
| _, _, Y.Abbr (B.Cast (_, w, _)) -> f x w
| _, _, Y.Void ->
error1 err "reference to unknown entry" m x
end
- | B.Bind (B.Abbr (a, v), t) ->
+ | B.Bind (a, B.Abbr v, t) ->
let f xv xt tt =
f (A.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt)
in
let f xv m = b_type_of err (f xv) st g m t in
- let f xv = f xv (R.push m (B.abbr a xv)) in
+ let f xv = f xv (R.push m a (B.abbr xv)) in
let f xv vv = match xv with
| B.Cast _ -> f xv
| _ -> f (B.Cast ([], vv, xv))
in
type_of err f st g m v
- | B.Bind (B.Abst (a, u), t) ->
+ | B.Bind (a, B.Abst u, t) ->
let f xu xt tt =
f (A.sh2 u xu t xt x (B.bind_abst a)) (B.bind_abst a xu tt)
in
let f xu m = b_type_of err (f xu) st g m t in
- let f xu _ = f xu (R.push m (B.abst a xu)) in
+ let f xu _ = f xu (R.push m a (B.abst xu)) in
type_of err f st g m u
- | B.Bind (B.Void a as b, t) ->
+ | B.Bind (a, B.Void, t) ->
let f xt tt =
- f (A.sh1 t xt x (B.bind b)) (B.bind b tt)
+ f (A.sh1 t xt x (B.bind_void a)) (B.bind_void a tt)
in
- b_type_of err f st g (R.push m b) t
+ b_type_of err f st g (R.push m a B.Void) t
- | B.Appl (a, v, t) ->
+ | B.Appl (a, v, t) ->
let f xv vv xt tt =
let f _ = f (A.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt) in
assert_applicability err f st m tt vv xv
in
let f xv vv = b_type_of err (f xv vv) st g m t in
type_of err f st g m v
- | B.Cast (a, u, t) ->
+ | B.Cast (a, u, t) ->
let f xu xt tt =
let f _ = f (A.sh2 u xu t xt x (B.cast a)) xu in
assert_convertibility err f st m xu tt xt
match b with
| D.Abst ws ->
let map x n w =
- let f ww = B.Bind (B.Abst (n :: a, ww), x) in xlate_term f w
+ let f ww = B.Bind (n :: a, B.Abst ww, x) in xlate_term f w
in
List.fold_left2 map x ns ws
| D.Abbr vs ->
let map x n v =
- let f vv = B.Bind (B.Abbr (n :: a, vv), x) in xlate_term f 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 _ ->
- let map x n = B.Bind (B.Void (n :: a), x) in
+ let map x n = B.Bind (n :: a, B.Void, x) in
List.fold_left map x ns
and xlate_proj x _ e =
| M.Abst (id, w, t) ->
let f w =
let a = [Y.Name (id, true)] in
- let f t = f (B.Bind (B.abst a w, t)) in
- xlate_term (B.push c (B.abst a w)) f t
+ let f t = f (B.Bind (a, B.Abst w, t)) in
+ xlate_term (B.push c B.empty a (B.Abst w)) f t
in
xlate_term c f w
let xlate_pars f pars =
let map f (id, w) c =
let a = [Y.Name (id, true)] in
- let f w = f (B.push c (B.abst a w)) in
+ let f w = f (B.push c B.empty a (B.Abst w)) in
xlate_term c f w
in
- C.list_fold_right f map pars B.empty_lenv
+ C.list_fold_right f map pars B.empty
let unwind_to_xlate_term f c t =
- let map t b = B.bind b t in
+ let map t a b = B.bind a b t in
let f t = f (B.fold_left map t c) in
xlate_term c f t
projects / helm.git / commitdiff