hets/HasCASL/Ast.hs

	Ast.hs revision 03b3c9dc9de5716538a9b04ae9bd8f36e22660e3


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
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
module Ast where

import Id
import Lexer
import Maybe
import Parsec
import ParseType
import ParseTerm
import Type
import Term
import Token

type SortId = Id
type OpId = Id
type VarId = Id

barChar = '|'
sortStr = "sort"

type Axiom = Term

data BasicItems = SigItems SigItems
		| FreeDatatypeItems [DatatypeDecl]
                | SortGen [SigItems]
		| VarItems [VarDecl]
		| LocalVarDecl [VarDecl] [Axiom]
		| Axioms [Axiom]

data SigItems = SortItems Keyword [SortItem]
	      | OpItems Keyword [OpItem]
	      |	DatatypeItems [DatatypeDecl]
              deriving (Show)

data SortItem = SubsortDecl [SortId] (Maybe Type)
	      | IsoDecl [SortId]
	      |	SubsortDefn SortId VarId Type Term
	      | AnnotatedSortItem SortItem [Anno]

showSortItem (SubsortDecl l Nothing) = showCommaList l
showSortItem (SubsortDecl l (Just t)) =
    showCommaList l . showSignStr lessStr . showSign t

showSortItem (IsoDecl l) =
    showSepList (showSignStr equalStr) showSign l

showSortItem (AnnotatedSortItem s _) = shows s
showSortItem (SubsortDefn s _ _ e) =
    shows s. showSignStr equalStr . shows e

instance Show SortItem where
    showsPrec _ = showSortItem

assocStr = "assoc"
commStr = "comm"
idemStr = "idem"
unitStr = "unit"

data OpAttr = AssocOpAttr | CommOpAttr | IdemOpAttr | UnitOpAttr Term

instance Show OpAttr where
     showsPrec _ AssocOpAttr = showString assocStr
     showsPrec _ CommOpAttr = showString commStr
     showsPrec _ IdemOpAttr = showString idemStr
     showsPrec _ (UnitOpAttr t) = showSignStr unitStr . shows t
     showList = showString . concat . map (\a -> ',' : show a)

data OpItem = OpItem [OpId] Type [OpAttr] (Maybe Term) [Anno]
	    deriving (Show)

data Component = Component Decl deriving (Show)

-- full function type (in Decl) of constructor
data Alternative = Construct Decl [Component]
		 | Subsorts [SortId]
		   deriving (Show)

data DatatypeDecl = DatatypeDecl SortId [Alternative] deriving (Show)

class Annotatable a where
    annotate :: a -> [Anno] -> a

instance Annotatable OpItem where
    annotate (OpItem os t as def _) l = OpItem os t as def l

instance Annotatable SortItem where
    annotate (AnnotatedSortItem s _) l = AnnotatedSortItem s l
    annotate s l = AnnotatedSortItem s l

commaSortDecl :: SortId -> Parser SortItem
commaSortDecl s = do { l <- comma >> (sortId `sepBy1` comma)
		     ; let l' = s : l in
		       subSortDecl l'
		       <|> return (SubsortDecl l' Nothing)
		     }

isoDecl :: SortId -> Parser SortItem
isoDecl s = do { e <- equal
               ; subSortDefn s
		 <|>
		 (do { l <- sortId `sepBy1` equal
		     ; return (IsoDecl (s:l))
		     })
	       }

subSortDefn :: SortId -> Parser SortItem
subSortDefn s = do { o <- oBrace
		   ; v <- varId
		   ; t <- colon >>= funType
		   ; dot <|> bar
		   ; e <- parseTerm
		   ; cBrace
		   ; let f = Binding SupersortVar [Decl (Symb [v] t) o []] e
		     in return (SubsortDefn s v t f)
		   }

subSortDecl :: [SortId] -> Parser SortItem
subSortDecl l = do { s <- lessSign >>= funType
		   ; return (SubsortDecl l (Just s))
		   }

sortItem :: Parser SortItem
sortItem = do { s <- sortId
	      ; subSortDecl [s]
		<|>
		commaSortDecl s
		<|>
                isoDecl s
		<|>
		return (SubsortDecl [s] Nothing)
	      }

sortItems = do { key <- pluralKeyword sortStr
	       ; l <- itemAux sortItem
	       ; return (SortItems key l)
	       }

pluralKeyword s = makeToken (string s <++> option "" (string "s"))

optSemi = bind (\ x y -> (x, y)) (option Nothing (fmap Just semi)) ann

dot = toKey [dotChar] <|> toKey middleDotStr <?> "dot"
bar = toKey [barChar]
equal = toKey equalStr

isStartKeyword s = s `elem` [dotChar]:middleDotStr:casl_reserved_words

lookAheadItemKeyword :: a -> Parser a
lookAheadItemKeyword a =
    do { c <- lookAhead (many (oneOf (['0'..'9'] ++ "'" ++ caslLetters))
			 <|> many (oneOf signChars))
       ; if isStartKeyword c then return a else unexpected c
       }

itemAux :: Annotatable a => (Parser a) -> Parser [a]
itemAux itemParser =
    do { i <- itemParser
       ; (m, an) <- optSemi
       ; let i' = if null an then i else annotate i an
	 in case m of Nothing -> return [i']
                      Just _ -> try (lookAheadItemKeyword [i'])
	                        <|>
	                        do { l <- itemAux itemParser
				   ; return (i':l)
				   }
       }