| Z.Sort h ->
let h = H.apply h in f x (Z.Sort h)
| Z.LRef i ->
- let f = function
- | Some (_, Z.Abst w) -> f x w
- | Some (_, Z.Abbr (Z.Cast (w, v))) -> f x w
- | Some (_, Z.Abbr _) -> assert false
- | Some (_, Z.Void) ->
- error1 "reference to excluded variable" c x
- | None ->
- error1 "variable not found" c x
+ let err () = error1 "variable not found" c x in
+ let f _ = function
+ | Z.Abst w -> f x w
+ | Z.Abbr (Z.Cast (w, v)) -> f x w
+ | Z.Abbr _ -> assert false
+ | Z.Void -> error1 "reference to excluded variable" c x
in
- Z.get f c i
+ Z.get err f c i
| Z.GRef uri ->
let f = function
| _, _, E.Abst (_, w) -> f x w
| _, _, E.Void -> assert false
in
ZE.get_entity f uri
- | Z.Bind (l, id, Z.Abbr v, t) ->
+ | Z.Bind (a, l, Z.Abbr v, t) ->
let f xv xt tt =
- f (W.sh2 v xv t xt x (Z.bind_abbr l id)) (Z.bind_abbr l id xv tt)
+ f (W.sh2 v xv t xt x (Z.bind_abbr a l)) (Z.bind_abbr a l xv tt)
in
let f xv cc = b_type_of (f xv) st cc t in
- let f xv = Z.push "type abbr" (f xv) c l id (Z.Abbr xv) in
+ let f xv = Z.push "type abbr" (f xv) c a l (Z.Abbr xv) in
let f xv vv = match xv with
| Z.Cast _ -> f xv
| _ -> f (Z.Cast (vv, xv))
in
type_of f st c v
- | Z.Bind (l, id, Z.Abst u, t) ->
+ | Z.Bind (a, l, Z.Abst u, t) ->
let f xu xt tt =
- f (W.sh2 u xu t xt x (Z.bind_abst l id)) (Z.bind_abst l id xu tt)
+ f (W.sh2 u xu t xt x (Z.bind_abst a l)) (Z.bind_abst a l xu tt)
in
let f xu cc = b_type_of (f xu) st cc t in
- let f xu _ = Z.push "type abst" (f xu) c l id (Z.Abst xu) in
+ let f xu _ = Z.push "type abst" (f xu) c a l (Z.Abst xu) in
type_of f st c u
- | Z.Bind (l, id, Z.Void, t) ->
+ | Z.Bind (a, l, Z.Void, t) ->
let f xt tt =
- f (W.sh1 t xt x (Z.bind l id Z.Void)) (Z.bind l id Z.Void tt)
+ f (W.sh1 t xt x (Z.bind a l Z.Void)) (Z.bind a l Z.Void tt)
in
let f cc = b_type_of f st cc t in
- Z.push "type void" f c l id Z.Void
+ Z.push "type void" f c a l Z.Void
| Z.Appl (v, t) ->
let f xv vv xt tt = function
| ZR.Abst w ->