let is_generated obj = List.exists ((=) `Generated) (attributes_of_obj obj)
-let arity_of_composed_coercion obj =
- let attrs = attributes_of_obj obj in
- try
- let tag=List.find (function `Class (`Coercion _) -> true|_->false) attrs in
- match tag with
- | `Class (`Coercion n) -> n
- | _-> assert false
- with Not_found -> 0
-;;
-
let projections_of_record obj uri =
let attrs = attributes_of_obj obj in
try
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
try match List.nth c (pred i) with
| None -> out (Printf.sprintf "%u[?]" i)
| Some (s, _) -> out (Printf.sprintf "%u[" i); pp_name out s; out "]"
- with Failure "nth" -> out (Printf.sprintf "%u[%u]" i (List.length c - i))
+ 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
let map (a, v) = pp_uri out a; out " <- "; pp_term out e c v in
xiter out "[" "; " "]" map xss
-and pp_attrs out attrs =
+let pp_int out i =
+ out (Printf.sprintf "%u" i)
+
+let pp_attrs out attrs =
let map = function
| _ -> ()
in
let pp_pars out pars =
xiter out " (" ", " ")\n" (pp_uri out) pars
+let pp_point out point =
+ if point then out "ind " else out "coind "
+
+let pp_constructor out (s, w) =
+ out s; out " of "; pp_term out [] [] w
+
+let pp_definition out (s, point, w, ts) =
+ out "let "; pp_point out point; out s; out " of "; pp_term out [] [] w;
+ xiter out "\ndef " "\nor " "" (pp_constructor out) ts
+
let pp_obj out = function
- | C.Constant (s, None, u, pars, attrs) ->
+ | C.Constant (s, None, u, pars, attrs) ->
out "fun "; pp_attrs out attrs; out s; pp_pars out pars;
out " of "; pp_term out [] [] u
- | C.Constant (s, Some t, u, pars, attrs) ->
+ | C.Constant (s, Some t, u, pars, attrs) ->
out "let "; pp_attrs out attrs; out s; pp_pars out pars;
out " def "; pp_term out [] [] t; out " of "; pp_term out [] [] u
- | C.Variable (s, None, u, pars, attrs) ->
- out "Local declaration"
- | C.Variable (s, Some t, u, pars, attrs) ->
- out "Local definition"
- | C.CurrentProof (s, e, t, u, pars, attrs) ->
+ | C.Variable (s, None, u, pars, attrs) ->
+ out "local fun "; pp_attrs out attrs; out s; pp_pars out pars;
+ out " of "; pp_term out [] [] u
+ | C.Variable (s, Some t, u, pars, attrs) ->
+ out "local let "; pp_attrs out attrs; out s; pp_pars out pars;
+ out " def "; pp_term out [] [] t; out " of "; pp_term out [] [] u
+ | C.InductiveDefinition (us, pars, lpsno, attrs) ->
+ out "Inductive "; pp_attrs out attrs; pp_int out lpsno; pp_pars out pars;
+ xiter out "" "\n" "" (pp_definition out) us
+ | C.CurrentProof (s, e, t, u, pars, attrs) ->
out "Current Proof"
- | C.InductiveDefinition (us, pars, lpno, attrs) ->
- out "Inductive Definition"
-
+