-
-(* raw cic prettyprinter ****************************************************)
-
-let xiter out so ss sc map l =
- let rec aux = function
- | hd :: tl when tl <> [] -> map hd; out ss; aux tl
- | hd :: tl -> map hd; aux tl
- | [] -> ()
- in
- out so; aux l; out sc
-
-let abst s w = Some (s, C.Decl w)
-
-let abbr s v w = Some (s, C.Def (v, w))
-
-let pp_sort out = function
- | C.Type _ -> out "\Type"
- | C.Prop -> out "\Prop"
- | C.CProp _ -> out "\CProp"
- | C.Set -> out "\Set"
-
-let pp_name out = function
- | C.Name s -> out s
- | C.Anonymous -> out "_"
-
-let pp_rel out c i =
- 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))
-
-let pp_implict out = function
- | None -> out "?"
- | Some `Closed -> out "?[Closed]"
- | Some `Type -> out "?[Type]"
- | Some `Hole -> out "?[Hole]"
-
-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.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
- | C.Var (a, xss) ->
- pp_uri out a; pp_xss out e c xss
- | C.Const (a, xss) ->
- pp_uri out a; pp_xss out e c xss
- | C.MutInd (a, m, xss) ->
- pp_uri out a; out (Printf.sprintf "/%u" m);
- pp_xss out e c xss
- | C.MutConstruct (a, m, n, xss) ->
- pp_uri out a; out (Printf.sprintf "/%u/%u" m n);
- pp_xss out e c xss
- | C.Cast (v, w) ->
- out "type "; pp_term out e c w; out " contains "; pp_term out e c v
- | C.Appl vs ->
- xiter out "(" " @ " ")" (pp_term out e c) vs
- | C.MutCase (a, m, w, v, vs) ->
- out "match "; pp_term out e c v;
- out " of "; pp_uri out a; out (Printf.sprintf "/%u" m);
- out " to "; pp_term out e c w;
- xiter out " cases " " | " "" (pp_term out e c) vs
- | C.Prod (s, w, t) ->
- out "forall "; pp_name out s; out " of "; pp_term out e c w;
- out " in "; pp_term out e (abst s w :: c) t
- | C.Lambda (s, w, t) ->
- out "fun "; pp_name out s; out " of "; pp_term out e c w;
- out " in "; pp_term out e (abst s w :: c) t
- | C.LetIn (s, v, w, t) ->
- out "let "; pp_name out s;
- out " def "; pp_term out e c v; out " of "; pp_term out e c w;
- out " in "; pp_term out e (abbr s v w :: c) t
- | C.Fix (i, fs) ->
- let map c (s, _, w, v) = abbr (C.Name s) v w :: c in
- let c' = List.fold_left map c fs in
- let map (s, i, w, v) =
- out (Printf.sprintf "%s[%u] def " s i); pp_term out e c' v;
- out " of "; pp_term out e c w;
- in
- xiter out "let rec " " and " " in " map fs; pp_rel out c' (succ i)
- | C.CoFix (i, fs) ->
- let map c (s, w, v) = abbr (C.Name s) v w :: c in
- let c' = List.fold_left map c fs in
- let map (s, w, v) =
- out s; pp_term out e c' v;
- out " of "; pp_term out e c w;
- in
- xiter out "let corec " " and " " in " map fs; pp_rel out c' (succ i)
-
-and pp_xss out e c xss =
- let map (a, v) = pp_uri out a; out " <- "; pp_term out e c v in
- xiter out "[" "; " "]" map xss