| term, None -> pp_term (* ~pp_parens:false *) term
| term, Some typ -> "(" ^ pp_term (* ~pp_parens:false *) term ^ ": " ^ pp_term typ ^ ")"
-let rec pp_term ?(pp_parens = true) t =
+let rec pp_term (status : #NCic.status) ?(pp_parens = true) t =
+ let pp_term = pp_term status in
let t_pp =
match t with
| Ast.AttributedTerm (attr, term) when debug_printing ->
sprintf " in %s%s" ty
(match debug_printing, href_opt with
| true, Some uri ->
- sprintf "(i.e.%s)" (UriManager.string_of_uri uri)
+ sprintf "(i.e.%s)" (NReference.string_of_reference uri)
| _ -> ""))
(match typ with None -> "" | Some t -> sprintf " return %s" (pp_term t))
- (pp_patterns patterns)
+ (pp_patterns status patterns)
| Ast.Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term ~pp_parens:true t1) (pp_term ~pp_parens:true t2)
| Ast.LetIn ((var,t2), t1, t3) ->
(* let t2 = match t2 with None -> Ast.Implicit | Some t -> t in *)
| Ast.Ident (name, Some []) | Ast.Ident (name, None)
| Ast.Uri (name, Some []) | Ast.Uri (name, None) -> name
| Ast.NRef nref -> NReference.string_of_reference nref
- | Ast.NCic cic -> NCicPp.ppterm ~metasenv:[] ~context:[] ~subst:[] cic
+ | Ast.NCic cic -> status#ppterm ~metasenv:[] ~context:[] ~subst:[] cic
| Ast.Ident (name, Some substs)
| Ast.Uri (name, Some substs) ->
- sprintf "%s \\subst [%s]" name (pp_substs substs)
+ sprintf "%s \\subst [%s]" name (pp_substs status substs)
| Ast.Implicit `Vector -> "…"
| Ast.Implicit `JustOne -> "?"
| Ast.Implicit (`Tagged name) -> "?"^name
| Ast.Num (num, _) -> num
| Ast.Sort `Set -> "Set"
| Ast.Sort `Prop -> "Prop"
- | Ast.Sort (`Type _) -> "Type"
- | Ast.Sort (`CProp _)-> "CProp"
| Ast.Sort (`NType s)-> "Type[" ^ s ^ "]"
| Ast.Sort (`NCProp s)-> "CProp[" ^ s ^ "]"
| Ast.Symbol (name, _) -> "'" ^ name
| Ast.UserInput -> "%"
| Ast.Literal l -> pp_literal l
- | Ast.Layout l -> pp_layout l
- | Ast.Magic m -> pp_magic m
+ | Ast.Layout l -> pp_layout status l
+ | Ast.Magic m -> pp_magic status m
| Ast.Variable v -> pp_variable v
in
match pp_parens, t with
| true, Ast.Ident (_, None) -> t_pp
| _ -> sprintf "(%s)" t_pp
-and pp_subst (name, term) = sprintf "%s \\Assign %s" name (pp_term term)
-and pp_substs substs = String.concat "; " (List.map pp_subst substs)
+and pp_subst status (name, term) =
+ sprintf "%s \\Assign %s" name (pp_term status term)
+and pp_substs status substs = String.concat "; " (List.map (pp_subst status) substs)
-and pp_pattern =
+and pp_pattern status =
function
Ast.Pattern (head, href, vars), term ->
let head_pp =
head ^
(match debug_printing, href with
- | true, Some uri -> sprintf "(i.e.%s)" (UriManager.string_of_uri uri)
+ | true, Some uri -> sprintf "(i.e.%s)" (NReference.string_of_reference uri)
| _ -> "")
in
sprintf "%s \\Rightarrow %s"
| [] -> head_pp
| _ ->
sprintf "(%s %s)" head_pp
- (String.concat " " (List.map (pp_capture_variable pp_term) vars)))
- (pp_term term)
+ (String.concat " " (List.map (pp_capture_variable (pp_term status)) vars)))
+ (pp_term status term)
| Ast.Wildcard, term ->
- sprintf "_ \\Rightarrow %s" (pp_term term)
+ sprintf "_ \\Rightarrow %s" (pp_term status term)
-and pp_patterns patterns =
- sprintf "[%s]" (String.concat " | " (List.map pp_pattern patterns))
+and pp_patterns status patterns =
+ sprintf "[%s]" (String.concat " | " (List.map (pp_pattern status) patterns))
and pp_box_spec (kind, spacing, indent) =
let int_of_bool b = if b then 1 else 0 in
in
sprintf "%sBOX%d%d" kind_string (int_of_bool spacing) (int_of_bool indent)
-and pp_layout = function
+and pp_layout status =
+ let pp_term = pp_term status in
+ function
| Ast.Sub (t1, t2) -> sprintf "%s \\SUB %s" (pp_term t1) (pp_term t2)
| Ast.Sup (t1, t2) -> sprintf "%s \\SUP %s" (pp_term t1) (pp_term t2)
| Ast.Below (t1, t2) -> sprintf "%s \\BELOW %s" (pp_term t1) (pp_term t2)
(String.concat " " (List.map (fun (k,v) -> k^"="^v) l))
(String.concat " " (List.map pp_term terms))
-and pp_magic = function
+and pp_magic status =
+ let pp_term = pp_term status in
+ function
| Ast.List0 (t, sep_opt) ->
sprintf "list0 %s%s" (pp_term t) (pp_sep_opt sep_opt)
| Ast.List1 (t, sep_opt) ->
| Ast.FreshVar n -> "fresh " ^ n
let _pp_term = ref (pp_term ~pp_parens:false)
-let pp_term t = !_pp_term t
+let pp_term status t = !_pp_term (status :> NCic.status) t
let set_pp_term f = _pp_term := f
let pp_params pp_term = function
| [] -> ""
| params -> " " ^ String.concat " " (List.map (pp_capture_variable pp_term) params)
-let pp_flavour = function
- | `Definition -> "definition"
- | `MutualDefinition -> assert false
- | `Fact -> "fact"
- | `Goal -> "goal"
- | `Lemma -> "lemma"
- | `Remark -> "remark"
- | `Theorem -> "theorem"
- | `Variant -> "variant"
- | `Axiom -> "axiom"
-
let pp_fields pp_term fields =
(if fields <> [] then "\n" else "") ^
String.concat ";\n"
(pp_term typ) (pp_constructors constructors)
in
fst_typ_pp ^ String.concat "" (List.map pp_type tl))
- | Ast.Theorem (`MutualDefinition, name, typ, body,_) ->
- sprintf "<<pretty printing of mutual definitions not implemented yet>>"
| Ast.Theorem (flavour, name, typ, body,_) ->
sprintf "%s %s:\n %s\n%s"
- (pp_flavour flavour)
+ (NCicPp.string_of_flavour flavour)
name
(pp_term typ)
(match body with
"record " ^ name ^ " " ^ pp_params pp_term params ^ ": " ^ pp_term ty ^
" \\def {" ^ pp_fields pp_term fields ^ "\n}"
-let rec pp_value = function
- | Env.TermValue t -> sprintf "$%s$" (pp_term t)
- | Env.StringValue s -> sprintf "\"%s\"" s
+let rec pp_value (status: #NCic.status) = function
+ | Env.TermValue t -> sprintf "$%s$" (pp_term status t)
+ | Env.StringValue (Env.Ident s) -> sprintf "\"%s\"" s
+ | Env.StringValue (Env.Var s) -> sprintf "\"${ident %s}\"" s
| Env.NumValue n -> n
- | Env.OptValue (Some v) -> "Some " ^ pp_value v
+ | Env.OptValue (Some v) -> "Some " ^ pp_value status v
| Env.OptValue None -> "None"
- | Env.ListValue l -> sprintf "[%s]" (String.concat "; " (List.map pp_value l))
+ | Env.ListValue l -> sprintf "[%s]" (String.concat "; " (List.map (pp_value status) l))
let rec pp_value_type =
function
| Env.OptType t -> "Maybe " ^ pp_value_type t
| Env.ListType l -> "List " ^ pp_value_type l
-let pp_env env =
+let pp_env status env =
String.concat "; "
(List.map
(fun (name, (ty, value)) ->
- sprintf "%s : %s = %s" name (pp_value_type ty) (pp_value value))
+ sprintf "%s : %s = %s" name (pp_value_type ty) (pp_value status value))
env)
let rec pp_cic_appl_pattern = function
- | Ast.UriPattern uri -> UriManager.string_of_uri uri
| Ast.NRefPattern nref -> NReference.string_of_reference nref
| Ast.VarPattern name -> name
| Ast.ImplicitPattern -> "?"