let is_sober c t =
let rec sober_term c g = function
- | C.Rel _
+ | C.Rel i ->
+ if i <= 0 then fun b -> false else g
| C.Sort _
| C.Implicit _ -> g
| C.Const (_, xnss)
| C.LetIn (_, v, ty, t) ->
sober_term c (sober_term c (sober_term c g t) ty) v
| C.Appl []
- | C.Appl [_] -> fun b -> false
+ | C.Appl [_]
+ | C.Appl (C.Appl _ :: _) -> fun b -> false
| C.Appl ts -> sober_terms c g ts
| C.MutCase (_, _, t, v, ts) ->
sober_terms c (sober_term c (sober_term c g t) v) ts
| Some (s, _) -> out (Printf.sprintf "%u[" i); pp_name out s; out "]"
with Failure "nth" -> out (Printf.sprintf "%u[%i]" i (List.length c - i))
-let pp_implict out = function
+let pp_implicit out = function
| None -> out "?"
| Some `Closed -> out "?[Closed]"
| Some `Type -> out "?[Type]"
| Some `Hole -> out "?[Hole]"
+ | Some `Vector -> out "?[...]"
let pp_uri out a =
out (Printf.sprintf "%s<%s>" (UM.name_of_uri a) (UM.string_of_uri a))
let rec pp_term out e c = function
| C.Sort h -> pp_sort out h
| C.Rel i -> pp_rel out c i
- | C.Implicit x -> pp_implict out x
+ | C.Implicit x -> pp_implicit out x
| C.Meta (i, iss) ->
let map = function None -> out "_" | Some v -> pp_term out e c v in
out (Printf.sprintf "?%u" i); xiter out "[" "; " "]" map iss