(* Printing of functional proof terms *) (* Author: Carsten Schuermann *) functor TomegaPrint (structure IntSyn' : INTSYN structure Tomega' : TOMEGA sharing Tomega'.IntSyn = IntSyn' structure Normalize : NORMALIZE sharing Normalize.IntSyn = IntSyn' sharing Normalize.Tomega = Tomega' structure Formatter : FORMATTER structure Names : NAMES sharing Names.IntSyn = IntSyn' structure Print : PRINT sharing Print.Formatter = Formatter sharing Print.IntSyn = IntSyn') : TOMEGAPRINT = struct structure IntSyn = IntSyn' structure Tomega = Tomega' structure Formatter = Formatter local structure I = IntSyn' structure T = Tomega' structure Fmt = Formatter structure P = Print (* Invariant: The proof term must satisfy the following conditions: * proof term must have the structure Rec. Lam ... Lam Case And Lam ... Lam Case ... And Lam ... Lam Case and the body of every case must be of the form (Let Decs in Case ... or Inx ... Inx Unit) * where Decs are always of the form New ... New App .. App Split .. Split Empty *) (* formatCtxBlock (G, (G1, s1)) = (G', s', fmts') Invariant: If |- G ctx and G |- G1 ctx and G2 |- s1 : G then G' = G2, G1 [s1] and G' |- s' : G, G1 and fmts is a format list of G1[s1] *) fun formatCtxBlock (G, (I.Null, s)) = (G, s, nil) | formatCtxBlock (G, (I.Decl (I.Null, D), s)) = let val D' = I.decSub (D, s) val fmt = P.formatDec (G, D') in (I.Decl (G, D'), I.dot1 s, [fmt]) end | formatCtxBlock (G, (I.Decl (G', D), s)) = let val (G'', s'', fmts) = formatCtxBlock (G, (G', s)) val D'' = I.decSub (D, s'') val fmt = P.formatDec (G'', D'') in (I.Decl (G'', D''), I.dot1 s'', fmts @ [Fmt.String ",", Fmt.Break, fmt]) end (* formatFor' (G, (F, s)) = fmts' Invariant: If |- G ctx and G |- s : Psi' and Psi' |- F formula then fmts' is a list of formats for F *) fun formatFor' (Psi, T.All (D, F)) = (case D of T.UDec D => let val G = T.coerceCtx Psi val D' = Names.decName (G, D) in [Fmt.String "All {", P.formatDec (G, D'), Fmt.String "}", Fmt.Break] @ formatFor' (I.Decl (Psi, T.UDec D'), F) end) | formatFor' (Psi, T.Ex (D, F)) = let val G = T.coerceCtx Psi val D' = Names.decName (G, D) in [Fmt.String "Ex [", P.formatDec (G, D'), Fmt.String "]", Fmt.Break] @ formatFor' (I.Decl (Psi, T.UDec D'), F) end | formatFor' (Psi, T.And (F1, F2)) = [Fmt.String "(", Fmt.HVbox (formatFor' (Psi, F1)), Fmt.String ")", Fmt.Break, Fmt.String "/\\", Fmt.Space, Fmt.String "(", Fmt.HVbox (formatFor' (Psi, F1)), Fmt.String ")"] | formatFor' (Psi, T.True) = [Fmt.String "True"] fun formatFor (G, F) = Fmt.HVbox (formatFor' (G, Normalize.normalizeFor (F, T.id))) fun forToString (Psi, F) = Fmt.makestring_fmt (formatFor (Psi, F)) (* formatPrg (Psi, P) names = fmt' Invariant: If |- Psi ctx and Psi; . |- P = rec x. (P1, P2, .. Pn) in F and names is a list of n names, then fmt' is the pretty printed format of P *) (* fun nameLookup index = List.nth (names, index) *) (* decName (G, LD) = LD' Invariant: If G1 |- LD lfdec then LD' = LD modulo new non-conficting variable names. *) fun decName (G, T.UDec D) = T.UDec (Names.decName (G, D)) | decName (G, T.PDec (NONE, F))= T.PDec (SOME "xx", F) (* needs to be integrated with Names *) | decName (G, D) = D (* (* numberOfSplits Ds = n' Invariant: If Psi, Delta |- Ds :: Psi', Delta' then n'= |Psi'| - |Psi| *) fun numberOfSplits Ds = let fun numberOfSplits' (T.Empty, n) = n | numberOfSplits' (T.New (_, Ds), n) = numberOfSplits' (Ds, n) | numberOfSplits' (T.App (_, Ds), n) = numberOfSplits' (Ds, n) | numberOfSplits' (T.Lemma (_, Ds), n) = numberOfSplits' (Ds, n) | numberOfSplits' (T.Split (_, Ds), n) = numberOfSplits' (Ds, n+1) | numberOfSplits' (T.Left (_, Ds), n) = numberOfSplits' (Ds, n) | numberOfSplits' (T.Right (_, Ds), n) = numberOfSplits' (Ds, n) in numberOfSplits' (Ds, 0) end *) (* psiName (Psi1, s, Psi2, l) = Psi1' Invariant: If |- Psi1 ctx and |- Psi1' ctx and |- Psi2 ctx and Psi2 = Psi2', Psi2'' and Psi1 |- s : Psi2 and |Psi2''| = l then Psi1' = Psi1 modulo variable naming and for all x in Psi2 s.t. s(x) = x in Psi1' *) fun psiName (Psi1, s, Psi2, l) = let fun nameDec (D as I.Dec (SOME _, _), name) = D | nameDec (I.Dec (NONE, V), name) = I.Dec (SOME name, V) fun namePsi (I.Decl (Psi, T.UDec D), 1, name) = I.Decl (Psi, T.UDec (nameDec (D, name))) | namePsi (I.Decl (Psi, LD as T.UDec D), n, name) = I.Decl (namePsi (Psi, n-1, name), LD) and nameG (Psi, I.Null, n, name, k) = (k n, I.Null) | nameG (Psi, I.Decl (G, D), 1, name, k) = (Psi, I.Decl (G, nameDec (D, name))) | nameG (Psi, I.Decl (G, D), n, name, k) = let val (Psi', G') = nameG (Psi, G, n-1, name, k) in (Psi', I.Decl (G', D)) end fun ignore (s, 0) = s | ignore (T.Dot (_, s), k) = ignore (s, k-1) | ignore (T.Shift n, k) = ignore (T.Dot (T.Idx (n+1), T.Shift (n+1)), k-1) fun copyNames (T.Shift n, G as I.Decl _) Psi1= copyNames (T.Dot (T.Idx (n+1), T.Shift (n+1)), G) Psi1 | copyNames (T.Dot (T.Exp _, s), I.Decl (G, _)) Psi1= copyNames (s, G) Psi1 | copyNames (T.Dot (T.Idx k, s), I.Decl (G, T.UDec (I.Dec (NONE, _)))) Psi1 = copyNames (s, G) Psi1 | copyNames (T.Dot (T.Idx k, s), I.Decl (G, T.UDec (I.Dec (SOME name, _)))) Psi1 = let val Psi1' = namePsi (Psi1, k, name) in copyNames (s, G) Psi1' end | copyNames (T.Dot (T.Prg k, s), I.Decl (G, T.PDec (NONE, _))) Psi1 = copyNames (s, G) Psi1 | copyNames (T.Dot (T.Prg k, s), I.Decl (G, T.PDec (SOME name, _))) Psi1 = copyNames (s, G) Psi1 | copyNames (T.Shift _, I.Null) Psi1 = Psi1 fun psiName' (I.Null) = I.Null | psiName' (I.Decl (Psi, D)) = let val Psi' = psiName' Psi in I.Decl (Psi', decName (T.coerceCtx Psi', D)) end in psiName' ((* copyNames (ignore (s, l), Psi2) *) Psi1) end (* (* merge (G1, G2) = G' Invariant: G' = G1, G2 *) fun merge (G1, I.Null) = G1 | merge (G1, I.Decl (G2, D)) = I.Decl (merge (G1, G2), D) (* formatCtx (Psi, G) = fmt' Invariant: If |- Psi ctx and Psi |- G ctx then fmt' is a pretty print format of G *) fun formatCtx (Psi, G) = let val G0 = T.makectx Psi fun formatCtx' (I.Null) = nil | formatCtx' (I.Decl (I.Null, I.Dec (SOME name, V))) = [Fmt.String name, Fmt.String ":", Print.formatExp (G0, V)] | formatCtx' (I.Decl (G, I.Dec (SOME name, V))) = (formatCtx' G) @ [Fmt.String ",", Fmt.Break, Fmt.String name, Fmt.String ":", Print.formatExp (merge (G0, G), V)] in Fmt.Hbox (Fmt.String "|" :: (formatCtx' G @ [Fmt.String "|"])) end (* formatTuple (Psi, P) = fmt' Invariant: If |- Psi ctx and Psi; Delta |- P = Inx (M1, Inx ... (Mn, Unit)) then fmt' is a pretty print format of (M1, .., Mn) *) fun formatTuple (Psi, P) = let fun formatTuple' (T.Unit) = nil | formatTuple' (T.Inx (M, T.Unit)) = [Print.formatExp (T.makectx Psi, M)] | formatTuple' (T.Inx (M, P')) = (Print.formatExp (T.makectx Psi, M) :: Fmt.String "," :: Fmt.Break :: formatTuple' P') in case P of (T.Inx (_, T.Unit)) => Fmt.Hbox (formatTuple' P) | _ => Fmt.HVbox0 1 1 1 (Fmt.String "(" :: (formatTuple' P @ [Fmt.String ")"])) end (* formatSplitArgs (Psi, L) = fmt' Invariant: If |- Psi ctx and L = (M1, .., Mn) and Psi |- Mk:Ak for all 1<=k<=n then fmt' is a pretty print format of (M1, .., Mn) *) fun formatSplitArgs (Psi, L) = let fun formatSplitArgs' (nil) = nil | formatSplitArgs' (M :: nil) = [Print.formatExp (T.makectx Psi, M)] | formatSplitArgs' (M :: L) = (Print.formatExp (T.makectx Psi, M) :: Fmt.String "," :: Fmt.Break :: formatSplitArgs' L) in if List.length L = 1 then Fmt.Hbox (formatSplitArgs' L) else Fmt.HVbox0 1 1 1 (Fmt.String "(" :: (formatSplitArgs' L @ [Fmt.String ")"])) end (* formatDecs1 (Psi, Ds, s, L) = L' Invariant: If |- Psi ctx and Psi; Delta |- Ds : Psi'; Delta' and Psi' = x1:A1 .. xn:An and Psi'' |- s : Psi and for i<=n L = (M1 .. Mi) s.t Psi'' |- Mi : Ai then L' extends L s.t. L = (M1 .. Mn) for all i <=n Psi'' |- Mi : Ai (and Mi is a splitting of a the result of an inductive call) *) fun formatDecs1 (Psi, T.Split (xx, Ds), I.Dot (Ft, s1), L) = formatDecs1 (Psi, Ds, s1, frontToExp (Ft) :: L) | formatDecs1 (Psi, T.Empty, s1, L) = L | formatDecs1 (Psi, Ds, I.Shift n, L) = formatDecs1 (Psi, Ds, I.Dot (I.Idx (n+1), I.Shift (n+1)), L) (* formatDecs0 (Psi, Ds) = (Ds', S') Invariant: If |- Psi ctx and Psi ; Delta |- Ds : Psi', Delta' and Ds = App M1 ... App Mn Ds' (where Ds' starts with Split) then S' = (M1, M2 .. Mn) and Psi1, Delta1 |- Ds' : Psi1', Delta1' (for some Psi1, Delta1, Psi1', Delta1') *) fun formatDecs0 (Psi, T.App ((xx, M), Ds)) = let val (Ds', S) = formatDecs0 (Psi, Ds) in (Ds', I.App (M, S)) end | formatDecs0 (Psi, Ds) = (Ds, I.Nil) (* formatDecs (index, Psi, Ds, (Psi1, s1)) = fmt' Invariant: If |- Psi ctx and Psi; Delta |- Ds : Psi'; Delta' and Psi1 |- s1 : Psi, Psi' then fmt' is a pretty print format of Ds *) fun formatDecs (index, Psi, Ds as T.App ((xx, _), P), (Psi1, s1)) = let val (Ds', S) = formatDecs0 (Psi, Ds) val L' = formatDecs1 (Psi, Ds', s1, nil) val name = nameLookup index in Fmt.Hbox [formatSplitArgs (Psi1, L'), Fmt.Space, Fmt.String "=", Fmt.Break, Fmt.HVbox (Fmt.String name :: Fmt.Break :: Print.formatSpine (T.makectx Psi, S))] end | formatDecs (index, Psi, T.New (B as T.CtxBlock (_, G), Ds), (Psi1, s1)) = let val B' = ctxBlockName (T.makectx Psi, B) val fmt = formatDecs (index, I.Decl (Psi, T.Block B'), Ds, (Psi1, s1)) in Fmt.Vbox [formatCtx (Psi, G), Fmt.Break, fmt] end | formatDecs (index, Psi, T.Lemma (lemma, Ds), (Psi1, s1)) = let val (Ds', S) = formatDecs0 (Psi, Ds) val L' = formatDecs1 (Psi, Ds', s1, nil) val (T.LemmaDec (names, _, _)) = T.lemmaLookup lemma in Fmt.Hbox [formatSplitArgs (Psi1, L'), Fmt.Space, Fmt.String "=", Fmt.Break, Fmt.HVbox (Fmt.String (List.nth (names, index)) :: Fmt.Break :: Print.formatSpine (T.makectx Psi, S))] end | formatDecs (index, Psi, T.Left (_, Ds), (Psi1, s1)) = let val fmt = formatDecs (index, Psi, Ds, (Psi1, s1)) in fmt end | formatDecs (index, Psi, T.Right (_, Ds), (Psi1, s1)) = let val fmt = formatDecs (index+1, Psi, Ds, (Psi1, s1)) in fmt end *) (* fmtSpine (G, d, l, (S, s)) = fmts format spine S[s] at printing depth d, printing length l, in printing context G which approximates G', where G' |- S[s] is valid *) fun fmtSpine (Psi, T.Nil) = [] | fmtSpine (Psi, T.AppExp (U, S)) = (* Print.formatExp (T.coerceCtx Psi, U) *) Fmt.HVbox (Print.formatSpine (T.coerceCtx Psi, I.App (U, I.Nil))) :: fmtSpine' (Psi, S) | fmtSpine (Psi, T.AppPrg (P, S)) = formatPrg3 (Psi, P) :: fmtSpine' (Psi, S) and fmtSpine' (Psi, T.Nil) = [] | fmtSpine' (Psi, S) = Fmt.Break :: fmtSpine (Psi, S) (* (* frontToExp (Ft) = U' Invariant: G |- Ft = U' : V for a G, V *) and frontToExp (T.Idx k) = I.Root (I.BVar k, I.Nil) | frontToExp (T.Exp (U)) = U | frontToExp (T.Prg (T.PairExp (U, _))) = U (* this is a patch -cs works only with one exists quantifier we cannot use LF spines, we need to use tomega spines. Next step program printer for tomega spines Then change this code. *) *) (* argsToSpine (Psi1, s, S) = S' Invariant: If Psi1 |- s = M1 . M2 .. Mn. ^|Psi1|: Psi2 and Psi1 |- S : V1 > {Psi2} V2 then Psi1 |- S' : V1 > V2 and S' = S, M1 .. Mn where then Fmts is a list of arguments *) and argsToSpine (s, 0, S) = S | argsToSpine (T.Shift (n), k, S) = argsToSpine (T.Dot (T.Idx (n+1), T.Shift (n+1)), k, S) | argsToSpine (T.Dot (T.Idx n, s), k, S) = argsToSpine (s, k-1, T.AppExp (I.Root (I.BVar n, I.Nil), S)) | argsToSpine (T.Dot (T.Exp (U), s), k, S) = argsToSpine (s, k-1, T.AppExp (U, S)) | argsToSpine (T.Dot (T.Prg P, s), k, S) = argsToSpine (s, k-1, T.AppPrg (P, S)) (* Idx will always be expanded into Expressions and never into programs is this a problem? -- cs *) (* formatTuple (Psi, P) = fmt' Invariant: If |- Psi ctx and Psi; Delta |- P = Inx (M1, Inx ... (Mn, Unit)) then fmt' is a pretty print format of (M1, .., Mn) *) and formatTuple (Psi, P) = let fun formatTuple' (T.Unit) = nil | formatTuple' (T.PairExp (M, T.Unit)) = [Print.formatExp (T.coerceCtx Psi, M)] | formatTuple' (T.PairExp (M, P')) = (Print.formatExp (T.coerceCtx Psi, M) :: Fmt.String "," :: Fmt.Break :: formatTuple' P') in case P of (T.PairExp (_, T.Unit)) => Fmt.Hbox (formatTuple' P) | _ => Fmt.HVbox0 1 1 1 (Fmt.String "(" :: (formatTuple' P @ [Fmt.String ")"])) end and formatRoot (Psi, T.Var (k), S) = let val T.PDec (SOME name, _) = I.ctxLookup (Psi, k) val Fspine = fmtSpine (Psi, S) in Fmt.Hbox [Fmt.Space, Fmt.HVbox (Fmt.String name :: Fmt.Break :: Fspine)] end | formatRoot (Psi, T.Const (l), S) = let val T.ValDec (name, _, _) = T.lemmaLookup l val Fspine = fmtSpine (Psi, S) in Fmt.Hbox [Fmt.Space, Fmt.HVbox (Fmt.String name :: Fmt.Break :: Fspine)] end (* formatPrg3 (Psi, P) = fmt Invariant: If |- Psi ctx and Psi; Delta |- P :: F and P = let .. in .. end | <..,..> | <> then fmt is a pretty print of P *) and formatPrg3 (Psi, T.Unit) = Fmt.String "<>" (* formatTuple (Psi, P) *) | formatPrg3 (Psi, T.PairExp (U, P)) = Fmt.HVbox [Fmt.String "<", Print.formatExp (T.coerceCtx Psi, U), Fmt.String ",", Fmt.Break, formatPrg3 (Psi, P), Fmt.String ">"] (* formatTuple (Psi, P) *) | formatPrg3 (Psi, P as T.Let _) = formatLet (Psi, P, nil) | formatPrg3 (Psi, P as T.Root (H, S)) = formatRoot (Psi, H, S) | formatPrg3 (Psi, P as T.New (T.Lam (T.UDec (I.BDec (l, (c, s))), _))) = formatNew (Psi, P, nil) | formatPrg3 _ = Fmt.String "missing case" and formatNew (Psi, T.New (T.Lam (T.UDec (D as I.BDec (l, (c, s))), P)), fmts) = let val G = T.coerceCtx Psi val D' = Names.decName (G, D) in formatNew (I.Decl (Psi, T.UDec D'), P, Fmt.Break :: Fmt.HVbox [Fmt.String "struct", Fmt.Space, Print.formatDec (G, D')] :: fmts) end | formatNew (Psi, P, fmts) = Fmt.Vbox0 0 1 ([Fmt.String "new", Fmt.Vbox0 0 1 (fmts), Fmt.Break, Fmt.String "in", Fmt.Break, Fmt.Spaces 2, formatPrg3 (Psi, P), Fmt.Break, Fmt.String "end"]) (* formatLet (Psi, P, fmts) = fmts' Invariant: If |- Psi ctx and Psi; Delta |- P = Let . Case P' :: F and fmts is a list of pretty print formats of P then fmts' extends fmts and fmts also includes a pretty print format for P' *) and formatLet (Psi, T.Let (D, P1, T.Case (T.Cases ((Psi1, s1, P2 as T.Let _) :: nil))), fmts) = let val Psi1' = psiName (Psi1, s1, Psi, 1) val F1 = Fmt.HVbox [formatPrg3 (Psi, P1)] val S = argsToSpine (s1, 1, T.Nil) (* was I.ctxLength Psi - max --cs *) (* val Fspine = Print.formatSpine (T.coerceCtx Psi1, S) *) val Fspine = fmtSpine (Psi1, S) val Fpattern = Fmt.HVbox [Fmt.Hbox (Fspine)] val Fbody = Fmt.HVbox [F1] val fmt = Fmt.HVbox [Fmt.HVbox [Fmt.String "val", Fmt.Space, Fpattern, Fmt.Space, Fmt.String "="], Fmt.Break, Fbody] in formatLet (Psi1', P2, fmts @ [Fmt.Break, fmt]) end | formatLet (Psi, T.Let (D, P1, T.Case (T.Cases ((Psi1, s1, P2) :: nil))), fmts) = let val Psi1' = psiName (Psi1, s1, Psi, 1) val F1 = Fmt.HVbox [formatPrg3 (Psi, P1)] val S = argsToSpine (s1, 1, T.Nil) (* was I.ctxLength Psi - max --cs *) (* val Fspine = Print.formatSpine (T.coerceCtx Psi1, S) *) val Fspine = fmtSpine (Psi1, S) val Fpattern = Fmt.HVbox [Fmt.Hbox (Fspine)] val Fbody = Fmt.HVbox [F1] val fmt = Fmt.HVbox [Fmt.HVbox [Fmt.String "val", Fmt.Space, Fpattern, Fmt.Space, Fmt.String "="], Fmt.Break, Fbody] (* val fmt = (* formatDecs (0, Psi, Ds, (Psi1', s1)) *) Fmt.Hbox [Fmt.String " ..." , Fmt.Space, Fmt.String "=", Fmt.Break, F1] *) in Fmt.Vbox0 0 1 ([Fmt.String "let", Fmt.Vbox0 0 1 (fmts @ [Fmt.Break, fmt]), Fmt.Break, Fmt.String "in", Fmt.Break, Fmt.Spaces 2, formatPrg3 (Psi1', P2), Fmt.Break, Fmt.String "end"]) end (* formatHead (index, Psi1, s, Psi2) = fmt' Invariant: If Psi1 |- s : Psi2 then fmt is a format of the entire head where index represents the function name and s the spine. *) fun formatHead ((max, index), Psi', s, Psi) = let val T.PDec (SOME name, _) = I.ctxLookup (Psi, index) val S = argsToSpine (s, I.ctxLength Psi - max, T.Nil) (* val Fspine = Print.formatSpine (T.coerceCtx Psi', S) *) val Fspine = fmtSpine (Psi', S) in Fmt.Hbox [Fmt.Space, Fmt.HVbox (Fmt.String name :: Fmt.Break :: Fspine)] end (* formatPrg2 ((max, index), Psi, L) = fmts' Invariant: If |- Psi ctx and Psi |- L a list of cases then fmts' list of pretty print formats of L *) fun formatPrg2 ((max, index), Psi, nil) = nil | formatPrg2 ((max, index), Psi, (Psi', s, P) :: nil) = let val Psi'' = psiName (Psi', s, Psi, 0) val fhead = if index = I.ctxLength Psi then "fun" else "and" in [Fmt.HVbox0 1 5 1 [Fmt.String fhead, formatHead ((max, index), Psi'', s, Psi), Fmt.Space, Fmt.String "=", Fmt.Break, formatPrg3 (Psi'', P)], Fmt.Break] end | formatPrg2 ((max, index), Psi, (Psi', s, P) :: O) = let val Psi'' = psiName (Psi', s, Psi, 0) in formatPrg2 ((max, index), Psi, O) @ [Fmt.HVbox0 1 5 1 [Fmt.String " |", formatHead ((max, index), Psi'', s, Psi), Fmt.Space, Fmt.String "=", Fmt.Break, formatPrg3 (Psi'', P)], Fmt.Break] end fun formatPrg11 ((max, index), Psi, T.Lam (D, P)) = formatPrg11 ((max, index+1), I.Decl (Psi, decName (T.coerceCtx Psi, D)), P) | formatPrg11 ((max, index), Psi, T.Case (T.Cases Os)) = formatPrg2 ((max, index), Psi, Os) (* formatPrg1 ((max, index), Psi, P) = fmts' Invariant: If |- Psi ctx and Psi; . |- P :: F and P is either a Lam .. | Case ... | Pair ... then fmts' is alist of pretty print formats of P *) fun formatPrg1 ((max, index), Psi, T.PairPrg (P1, P2)) = formatPrg1 ((max, index), Psi, P1) @ formatPrg1 ((max, index-1), Psi, P2) | formatPrg1 ((max, index), Psi, P) = formatPrg11 ((max, index), Psi, P) (* formatPrg0 (Psi, P) = fmt' If |- Psi ctx and Psi; . |- P :: F then fmt' is a pretty print format of P *) fun formatPrg0 (T.Rec (T.PDec (SOME _, F), T.Case (T.Cases [(Psi, t, P)]))) = let val max = I.ctxLength Psi (* number of ih. *) in Fmt.Vbox0 0 1 (formatPrg1 ((max, max), Psi, P)) end fun formatFun Args = (Names.varReset I.Null; formatPrg0 Args) (* fun formatLemmaDec (T.LemmaDec (names, P, F)) = Fmt.Vbox0 0 1 [formatFor (I.Null, F) names, Fmt.Break, formatPrg (I.Null, P) names] *) fun funToString Args = Fmt.makestring_fmt (formatFun Args) fun prgToString Args = Fmt.makestring_fmt (formatPrg3 Args) (* fun lemmaDecToString Args = Fmt.makestring_fmt (formatLemmaDec Args) *) (* fun prgToString Args names = "not yet implemented " *) in val formatFor = formatFor val forToString = forToString val formatFun = formatFun val formatPrg = formatPrg3 (* val formatLemmaDec = formatLemmaDec *) val prgToString = prgToString val funToString = funToString (* val lemmaDecToString = lemmaDecToString *) end end; (* signature FUNPRINT *)