-
Notifications
You must be signed in to change notification settings - Fork 2
/
Basics.hs
144 lines (98 loc) · 2.95 KB
/
Basics.hs
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
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
{-# LANGUAGE OverloadedStrings, GeneralizedNewtypeDeriving #-}
module Basics
(module Data.Monoid, (<>),
module Control.Applicative,
Irr(..),
Sort(..),
Ident, Identifier(..), DisplayContext,
Position, dummyPosition, identPosition,
isDummyId, modId, synthId, dummyId, idString,
Binder(..), arrow, colon, cross, appl, comm,
Lattice(..), above,
module Cubes) where
import Display
import qualified RawSyntax as A
import RawSyntax (Identifier(..))
import Control.Applicative
import Data.Monoid hiding ((<>))
import Data.Sequence (Seq)
import Cubes
-----------
-- Irr
newtype Irr a = Irr {fromIrr :: a}
deriving (Show,Monoid)
instance Eq (Irr a) where
x == y = True
instance Pretty x => Pretty (Irr x) where
pretty (Irr x) = pretty x
--------------
-- Ident
instance Pretty Identifier where
pretty (Identifier (_,x)) = text x
instance Monoid Identifier where
Identifier (p,t1) `mappend` Identifier (_,t2) = Identifier (p, t1 <> t2)
mempty = Identifier (fromIrr dummyPosition,"")
type Ident = Irr Identifier
isDummyIdS ('_':x) = True
isDummyIdS _ = False
isDummyId (Irr (Identifier (_,xs))) = isDummyIdS xs
synthId :: String -> Ident
synthId x = Irr (Identifier (fromIrr dummyPosition,x))
dummyId = synthId "_"
idString :: Ident -> String
idString (Irr (Identifier (_,name))) = name
type DisplayContext = Seq Ident
----------------
-- Position
type Position = (Int,Int)
identPosition (Irr (Identifier (p,_))) = Irr p
dummyPosition = Irr (0,0)
modId :: (String -> String) -> Ident -> Ident
modId f (Irr (Identifier (pos ,x))) = (Irr (Identifier (pos,f x)))
-------
-----------
-- Sort
instance Lattice Int where -- Lattice is a misnomer here.
x ⊔ (-1) = (-1)
x ⊔ y = max x y
data Binder = Pred | Regu
deriving (Ord,Eq,Show)
class Lattice a where
(⊔) :: a -> a -> a
-- instance Ord Sort where
-- compare (Sort x) (Sort y) = compare x y
data Sort = Sort {sortLevel :: Int,
sortDimension :: Int}
deriving (Eq)
instance Lattice Sort where
Sort x m ⊔ Sort y n = Sort (x ⊔ y) (min m n)
instance Show Sort where
show s = render (pretty s)
instance Pretty Binder where
pretty = colon
instance Pretty Sort where
pretty (Sort s d) = showLev <> showDim
where showDim = case d of
0 -> mempty
_ -> superscriptPretty d
showLev = case s of
(-1) -> "□"
0 -> star
l -> star <> subscriptPretty l
above (Sort s n) = Sort (s+1) n
star = "∗" -- ⋆★*∗
arrow, colon, cross, comm, appl :: Binder -> Doc
arrow Pred = "⇛"
arrow Regu = "→"
-- ⟴
colon Regu = text ":"
colon Pred = text "::"
-- :⋮∷∴∵
cross Regu = "×"
cross Pred = "⋇"
-- ⊗⊠
-- ⚔⤬⤫⨯
comm Pred = "⍮"
comm Regu = ","
appl Regu = ""
appl Pred = "· "