(* 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 *)