(* Printing implementation *)
functor NatDed(structure Timers : TIMERS
structure ProofTerm : PROOF_TERM) :> NAT_DED =
struct
structure ProofTerm = ProofTerm
and N = ProofTerm
structure C = CSyn
structure G = Global
structure Pr = Pretty
infixr ^^
val (op ^^) = Pr.^^
(* The kinds of ND rules that we support *)
datatype Rule =
Hyp (* hypothesis introduction *)
| Axiom of string (* axiom *)
| Lemma of string
| Theorem of string
| By of int list (* for combining steps *)
| TrueI (* true introduction *)
| FE of int
| AndI of int * int (* conjunction intro *)
| AndE_L of int (* conj-elim left *)
| AndE_R of int (* conj-elim right *)
| ImpI of int * int (* implication intro *)
| ImpE of int * int (* inplication elim *)
| OrI_L of int (* disj-intro left *)
| OrI_R of int (* disj-intro right *)
| OrE of int * int * int * int * int (* disj-elimination *)
| NotI of int * int (* negation-introduction *)
| NotE of int * int (* negation-elimination *)
| ForallI of int * string (* generalisation *)
| ForallE of int * C.CTerm (* universal instantiation *)
| ExistsI of int * C.CTerm (* existential introduction *)
| ExistsE of int * int * int * string (* existential elimination *)
type natded = (int list * C.CForm * Rule) list
exception Error
open Ctx
(* app G v = (F, L) iff (F, L) is bound to v in G *)
fun app Null x = raise Error
| app (Decl (G, (x, FL))) v = if x = v then FL else app G v
(* the list of line numbers of hypotheses inside the conPr.text *)
fun hyps Null = []
| hyps (Decl (G, (x, (F, L)))) = (! L) :: (hyps G)
(* convert a proof-term and a CForm to a natural deduction of type natded *)
fun toNat (K, P, F) =
let
val line = ref 1
fun newline () = ! line before line := !line + 1 (* generate new line nos *)
fun makeEmpty Null = Null
| makeEmpty (Decl (G, (u, F))) =
let
val n = newline ()
in
Decl (makeEmpty G, (u, (F, ref n)))
end
fun fillErUp Null = []
| fillErUp (Decl (G, (u, (F, l)))) = ([], F, Axiom u) :: (fillErUp G)
(* I am extremely annoyed that globals doesn't allow us to check what KIND of
knowledge u is -- axiom, lemma, or theorem. But I don't have time to change it.
What was the rationale behind hiding this information??? - Chad *)
val K = makeEmpty K
(* output (G, I, F) = (L, n) *)
(* un-numbered list of lines in the intro of F with certificate I *)
(* n = line number where F is introduced *)
fun output (G, N.Pair (I1, I2), F as C.And (A, B)) =
let
val (L1, n1) = output (G, I1, A)
val (L2, n2) = output (G, I2, B)
in
((hyps G, F, AndI (n1, n2)) :: (L2 @ L1), newline ())
end
| output (G, N.Unit, C.True) = ([(hyps G, C.True, TrueI)], newline ())
| output (G, N.Lam (u, I), F as C.Implies (A, B)) =
let
val n1 = newline () (* for the hypothesis *)
val G' = Decl (G, (u, (A, ref n1)))
val (L2, n2) = output (G', I, B)
in
(((hyps G, F, ImpI (n1, n2)) :: L2) @ [(hyps G', A, Hyp)], newline ())
end
| output (G, N.Inl I, F as C.Or (A, B)) =
let
val (L, n) = output (G, I, A)
in
((hyps G, F, OrI_L n) :: L, newline ())
end
| output (G, N.Inr I, F as C.Or (A, B)) =
let
val (L, n) = output (G, I, B)
in
((hyps G, F, OrI_R n) :: L, newline ())
end
| output (G, N.Case (E, (u1, I1), (u2, I2)), F) =
let
val (L1, n1, F1 as C.Or (A, B)) = output' (G, E)
val n2 = newline ()
val (L3, n3) = output (Decl (G, (u1, (A, ref n2))), I1, F)
val n4 = newline ()
val (L5, n5) = output (Decl (G, (u2, (B, ref n4))), I2, F)
in
([(hyps G, F, OrE (n1, n2, n3, n4, n5))] @
L5 @
[(n4 :: (hyps G), B, Hyp)] @
L3 @
[(n2 :: (hyps G), A, Hyp)] @
L1, newline ())
end
| output (G, N.Abort E, F) =
let
val (L, n, F') = output' (G, E)
in
case F of
C.False => (line := !line - 1; (L, newline ()))
| _ => ((hyps G, F, FE n) :: L, newline ())
end
| output (G, N.Elim E, F) =
let
val (L, n, _) = output' (G, E)
in
(L, n)
end
| output (G, I, F) =
(TextIO.print ((Pr.toString 40 (N.toDoc I)) ^ " : " ^ (Pr.toString 40 (C.formToDoc F)));
raise Domain)
(* output (G, E) = (L, n, F) *)
(* L un-numbered list of lines in the intro of F with certificate I *)
(* n = line where E is eliminated *)
(* F = principal type of E *)
and output' (G, N.Var u) =
let
val (F, L) = app G u handle Error => app K u
in
([], ! L, F)
end
| output' (G, N.Fst E) =
let
val (L, n, F) = output' (G, E)
in
case F of
C.And (A, B) => ((hyps G, A, AndE_L n) :: L, newline (), A)
| _ => raise Error
end
| output' (G, N.Snd E) =
let
val (L, n, F) = output' (G, E)
in
case F of
C.And (A, B) => ((hyps G, B, AndE_R n) :: L, newline (), B)
| _ => raise Error
end
| output' (G, N.App (E, I)) =
let
val (L1, n1, F as C.Implies (A, B)) = output' (G, E)
val (L2, n2) = output (G, I, A)
in
((hyps G, B, ImpE (n1, n2)) :: (L2 @ L1), newline (), B)
end
| output' (G, N.Intro (I, F)) =
let
val (L, n) = output (G, I, F)
in
(L, n, F)
end
val (L, _) = output (Null, P, F)
in
(fillErUp K) @ (rev L)
(* rev L *)
(* because it is faster to generate the list *)
(* in reverse order (cons vs append) *)
end
(* Convert a list of strings into a new string delimited by commas *)
fun listify' [] s = s
| listify' [n] s = s ^ Int.toString n
| listify' (h :: t) s = listify' t (s ^ Int.toString h ^ ", ")
and listify l = listify' l ""
(* Get the name of a rule *)
fun ruleString Hyp = "Hyp"
| ruleString (Axiom s) = "Know " ^ s (* Currently (unfortunately) we're using "Axiom" for every kind of knowledge. - Chad. *)
| ruleString (Lemma s) = "Lemma " ^ s
| ruleString (Theorem s) = "Thm " ^ s
| ruleString (By nl) = "By: " ^ listify nl
| ruleString TrueI = "TI"
| ruleString (AndI (n1, n2)) = "&I: " ^ listify [n1, n2]
| ruleString (AndE_L n) = "&E_L: " ^ Int.toString n
| ruleString (AndE_R n) = "&E_R: " ^ Int.toString n
| ruleString (ImpI (n1, n2)) = "=>I: " ^ listify [n1, n2]
| ruleString (OrI_L n) = "vI_L: " ^ Int.toString n
| ruleString (OrI_R n) = "vI_R: " ^ Int.toString n
| ruleString (OrE (n1, n2, n3, n4, n5)) = "vE: " ^ listify [n1, n2, n3, n4, n5]
| ruleString (FE n) = "FE: " ^ Int.toString n
| ruleString (ImpE (n1, n2)) = "=>E: " ^ listify [n1, n2]
| ruleString (NotI (n1, n2)) = "~I: " ^ listify [n1, n2]
| ruleString (NotE (n1, n2)) = "~E: " ^ listify [n1, n2]
| ruleString (ForallI (n, x)) = "Gen: " ^ x ^ ", " ^ Int.toString n
| ruleString (ForallE (n, t)) = "UI: " ^ Int.toString n ^ ", " ^ Pr.toString 100 (C.termToDoc t)
| ruleString (ExistsI (n, t)) = "EGen: " ^ Int.toString n ^ ", " ^ Pr.toString 100 (C.termToDoc t)
| ruleString (ExistsE (n1, n2, n3, x)) = "Choose: " ^ x ^ ", " ^ listify [n1, n2, n3]
fun prettyNat (nl, nh) (n, (il, F, R)) =
let
val ils = (StringCvt.padRight #" " nh (listify il)) ^ " |- "
val ns = StringCvt.padLeft #" " nl ("(" ^ Int.toString n ^ ")")
val left = ns ^ " " ^ ils
val lefts = String.size left
val firsttwo = Pretty.agrp (Pretty.text left ^^
Pretty.nest lefts (Pretty.break ^^ C.formToDoc F))
in
(firsttwo, ruleString R)
end
(* pretty print a natural deduction by making sure that the line does not *)
(* exceed lw characters. nl and nh are the widths of the line number and *)
(* hypothesis "areas" of a line. n is the line number, il is the list of *)
(* hypotheses, F is the formula that is pretty-printed, and R is the rule *)
(* corresponding to the formula *)
(* fun prettyNat (nl, nh, lw) (n, (il, F, R)) =
let
val ils = (StringCvt.padRight #" " nh (listify il)) ^ " |- "
val ns = StringCvt.padLeft #" " nl ("(" ^ Int.toString n ^ ")")
val left = ns ^ " " ^ ils
val lefts = String.size left
val right = " " ^ ruleString R
val mid = lw - lefts - String.size right
val firsttwo = Pr.agrp (Pr.text left ^^ Pr.nest lefts (Pr.break ^^ (C.formToDoc F)))
val lines =
List.rev (String.tokens (fn x => x = #"\n") (Pr.toString (lefts + mid) firsttwo))
val withright =
((StringCvt.padRight #" " (lefts + mid) (hd lines)) ^ right) :: (tl lines)
in
foldl (fn (x, s) => x ^ "\n" ^ s) "" withright
end *)
fun toDoc lines =
let
fun digs n =
if n < 10 then 1 else if n < 100 then 2 else if n < 1000 then 3 else 4
fun listdigs [] = 0
| listdigs [n] = digs n
| listdigs (n :: ns) = digs n + 2 + listdigs ns
val maxH = foldl (fn ((x, _, _), y) => Int.max (listdigs x, y)) 0 lines
(* max number of digits in line number *)
val nl = digs (List.length lines)
fun number n [] = []
| number n (h :: t) = (n, h) :: (number (n + 1) t)
in
List.map (fn x => prettyNat (nl + 2, maxH) x) (number 1 lines)
end
val toDoc = Timers.time Timers.printing toDoc
end (* functor NatDed *)