linear-logic/Printer.hs at master · andykitchen/linear-logic · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
module Printer where

import Syntax

showsTermOp  prec op d (l, r) = showParen (d > prec) $
      showsTerm (prec+1) l . showString op . showsTerm prec r

showTerm :: Term -> String
showTerm term = showsTerm 0 term ""

showsTerm :: Int -> Term -> ShowS
showsTerm d (Atom s) = showString s

showsTerm d (Not t)  = showParen (d > prec) $
    showsTerm prec t . showString "^"
  where prec = 8

showsTerm d (OfCourse t)  = showParen (d > prec) $
    showString "!" . showsTerm prec t
  where prec = 7

showsTerm d (WhyNot t)  = showParen (d > prec) $
    showString "?" . showsTerm prec t
  where prec = 7


showsTerm d (l :*:  r) = showsTermOp 6 "*"  d (l, r)
showsTerm d (l :$:  r) = showsTermOp 6 "$"  d (l, r)
showsTerm d (l :-@: r) = showsTermOp 2 "  -@  " d (l, r)

showsTerm d (l :&: r) = showsTermOp 4 " & " d (l, r)
showsTerm d (l :+: r) = showsTermOp 4 " + " d (l, r)


showsTerm d Top    = showString "#"
showsTerm d Bottom = showString "%"
showsTerm d One    = showString "1"
showsTerm d Zero   = showString "0"


showTerms ls = showsTerms ls ""

showsTerms []     = id
showsTerms (x:[]) = showsTerm 0 x . showString "."
showsTerms (x:xs) = showsTerm 0 x . showString ".\n" . showsTerms xs