-
Notifications
You must be signed in to change notification settings - Fork 19
/
Copy pathParse_AS_Basic.hs
132 lines (111 loc) · 4.19 KB
/
Parse_AS_Basic.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
{- |
Module : $Header$
Description : Parsing CASL's SIG-ITEMS, BASIC-ITEMS and BASIC-SPEC
Copyright : (c) Christian Maeder, Uni Bremen 2002-2004
License : GPLv2 or higher, see LICENSE.txt
Maintainer : Christian.Maeder@dfki.de
Stability : provisional
Portability : portable
Parser for CASL basic specifications (SIG-ITEMS, BASIC-ITEMS, BASIC-SPEC)
Follows Sect. II:3.1 of the CASL Reference Manual.
-}
{-
http://www.cofi.info/Documents/CASL/Summary/
from 25 March 2001
C.2.1 Basic Specifications with Subsorts
-}
module CASL.Parse_AS_Basic where
import Common.AS_Annotation
import Common.AnnoState
import Common.Id
import Common.Keywords
import Common.Lexer
import Common.GlobalAnnotations (PrefixMap)
import CASL.AS_Basic_CASL
import CASL.Formula
import CASL.SortItem
import CASL.OpItem
import Text.ParserCombinators.Parsec
-- * signature items
sortItems, typeItems, opItems, predItems, sigItems
:: (AParsable s, TermParser f) => [String] -> AParser st (SIG_ITEMS s f)
sortItems ks = itemList ks esortS sortItem (Sort_items PossiblyEmptySorts)
<|> itemList ks sortS sortItem (Sort_items NonEmptySorts)
typeItems ks = itemList ks typeS datatype (Datatype_items NonEmptySorts)
<|> itemList ks etypeS datatype (Datatype_items PossiblyEmptySorts)
opItems ks = itemList ks opS opItem Op_items
predItems ks = itemList ks predS predItem Pred_items
sigItems ks = fmap Ext_SIG_ITEMS aparser <|>
sortItems ks <|> opItems ks <|> predItems ks <|> typeItems ks
-- * helpers
datatypeToFreetype :: (AParsable b, AParsable s, TermParser f) =>
SIG_ITEMS s f -> Range -> BASIC_ITEMS b s f
datatypeToFreetype d pos =
case d of
Datatype_items sk ts ps -> Free_datatype sk ts (pos `appRange` ps)
_ -> error "datatypeToFreetype"
axiomToLocalVarAxioms :: (AParsable b, AParsable s, TermParser f) =>
BASIC_ITEMS b s f -> [Annotation] -> [VAR_DECL] -> Range
-> BASIC_ITEMS b s f
axiomToLocalVarAxioms ai a vs posl =
case ai of
Axiom_items (Annoted ft qs as rs : fs) ds ->
let aft = Annoted ft qs (a ++ as) rs
in Local_var_axioms vs (aft : fs) (posl `appRange` ds)
_ -> error "axiomToLocalVarAxioms"
-- * basic items
basicItems :: (AParsable b, AParsable s, TermParser f) =>
[String] -> AParser st (BASIC_ITEMS b s f)
basicItems ks = fmap Ext_BASIC_ITEMS aparser <|> fmap Sig_items (sigItems ks)
<|> do
f <- asKey freeS
ti <- typeItems ks
return (datatypeToFreetype ti (tokPos f))
<|> do
g <- asKey generatedS
do t <- typeItems ks
return (Sort_gen [Annoted t nullRange [] []] $ tokPos g)
<|> do
o <- oBraceT
is <- annosParser (sigItems ks)
c <- cBraceT
a <- lineAnnos
return (Sort_gen (init is ++ [appendAnno (last is) a])
(toRange g [o] c))
<|> do
v <- pluralKeyword varS
(vs, ps) <- varItems ks
return (Var_items vs (catRange (v : ps)))
<|> do
f <- forallT
(vs, ps) <- varDecls ks
a <- annos
ai <- dotFormulae True ks
return (axiomToLocalVarAxioms ai a vs $ catRange (f : ps))
<|> dotFormulae True ks
<|> itemList ks axiomS formula Axiom_items
varItems :: [String] -> AParser st ([VAR_DECL], [Token])
varItems ks =
do v <- varDecl ks
do s <- trySemiOrComma
do tryItemEnd (ks ++ startKeyword)
return ([v], [s])
<|> do
(vs, ts) <- varItems ks
return (v : vs, s : ts)
<|> return ([v], [])
dotFormulae :: (AParsable b, AParsable s, TermParser f) =>
Bool -> [String] -> AParser st (BASIC_ITEMS b s f)
dotFormulae requireDot ks =
do d <- (if requireDot then id else option $ mkSimpleId ".") dotT
(fs, ds) <- aFormula ks `separatedBy` dotT
(m, an) <- optSemi
let ps = catRange (d : ds)
ns = init fs ++ [appendAnno (last fs) an]
return $ Axiom_items ns (ps `appRange` catRange m)
aFormula :: TermParser f => [String] -> AParser st (Annoted (FORMULA f))
aFormula = allAnnoParser . formula
-- * basic spec
basicSpec :: (TermParser f, AParsable s, AParsable b) =>
[String] -> PrefixMap -> AParser st (BASIC_SPEC b s f)
basicSpec bi _ = (fmap Basic_spec . annosParser . basicItems) bi