Parse_AS.hs revision c36c47428b2f42fe09eab533acf6be19d6d9f259
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
59d823de481014f68b8b024474bffac150b56e1eWiebke Herding{- Spickzettel f�r's Parsen
cc6df32dd55910aac7de12b30cc5049d96b8f770Wiebke Herding-- Definition aus Logic.hs
cc6df32dd55910aac7de12b30cc5049d96b8f770Wiebke Herdingtype ParseFun a = FilePath -> Int -> Int -> String -> (a,String,Int,Int)
cc6df32dd55910aac7de12b30cc5049d96b8f770Wiebke Herding -- args: filename, line, column, input text
cc6df32dd55910aac7de12b30cc5049d96b8f770Wiebke Herding -- result: value, remaining text, line, column
cc6df32dd55910aac7de12b30cc5049d96b8f770Wiebke HerdingtoParseFun :: GenParser Char st a -> st -> ParseFun a
cc6df32dd55910aac7de12b30cc5049d96b8f770Wiebke Herding-- Klassenfunktion, die meine Instanz implementiert
cc6df32dd55910aac7de12b30cc5049d96b8f770Wiebke Herdingparse_basic_spec :: id -> Maybe(ParseFun basic_spec)
cc6df32dd55910aac7de12b30cc5049d96b8f770Wiebke Herding-- ^ R�ckgabetyp
59d823de481014f68b8b024474bffac150b56e1eWiebke Herding-- aus CASL, kann bleiben
10e8873de4a89035222d077fe80b9fd7b9631473Wiebke HerdingbasicSpec :: AParser BASIC_SPEC
10e8873de4a89035222d077fe80b9fd7b9631473Wiebke HerdingbasicSpec = (fmap Basic_spec $ many1 $
10e8873de4a89035222d077fe80b9fd7b9631473Wiebke Herding try $ annoParser basicItems)
10e8873de4a89035222d077fe80b9fd7b9631473Wiebke Herding <|> try (oBraceT >> cBraceT >> return (Basic_spec []))
59d823de481014f68b8b024474bffac150b56e1eWiebke HerdingbasicItems :: AParser BASIC_ITEMS
59d823de481014f68b8b024474bffac150b56e1eWiebke HerdingbasicItems = fmap Sig_items sigItems
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke Herding <|> dotFormulae -- sp�ter!
59d823de481014f68b8b024474bffac150b56e1eWiebke HerdingsigItems :: AParser SIG_ITEMS
10e8873de4a89035222d077fe80b9fd7b9631473Wiebke HerdingsigItems = propItems
10e8873de4a89035222d077fe80b9fd7b9631473Wiebke HerdingpropItem :: AParser PROP_ITEM
10e8873de4a89035222d077fe80b9fd7b9631473Wiebke HerdingpropItem = do s <- sortId ; -- Props are the same as sorts (in declaration)
10e8873de4a89035222d077fe80b9fd7b9631473Wiebke Herding commaPropDecl s
10e8873de4a89035222d077fe80b9fd7b9631473Wiebke Herding return (Prop_decl [s] [])
10e8873de4a89035222d077fe80b9fd7b9631473Wiebke HerdingpropItems :: AParser SIG_ITEMS
10e8873de4a89035222d077fe80b9fd7b9631473Wiebke HerdingpropItems = itemList propS propItem Prop_items
10e8873de4a89035222d077fe80b9fd7b9631473Wiebke HerdingcommaPropDecl :: Id -> AParser PROP_ITEM
10e8873de4a89035222d077fe80b9fd7b9631473Wiebke HerdingcommaPropDecl s = do c <- anComma
10e8873de4a89035222d077fe80b9fd7b9631473Wiebke Herding (is, cs) <- sortId `separatedBy` anComma
10e8873de4a89035222d077fe80b9fd7b9631473Wiebke Herding let l = s : is
10e8873de4a89035222d077fe80b9fd7b9631473Wiebke Herding p = tokPos c : map tokPos cs in return (Prop_decl l p)
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke HerdingdotFormulae :: AParser BASIC_ITEMS
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke HerdingdotFormulae = do d <- dotT
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke Herding (fs, ds) <- aFormula `separatedBy` dotT
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke Herding (m, an) <- optSemi
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke Herding let ps = map tokPos (d:ds)
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke Herding ns = init fs ++ [appendAnno (last fs) an]
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke Herding Nothing -> return (Axiom_items ns ps)
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke Herding Just t -> return (Axiom_items ns
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke Herding (ps ++ [tokPos t]))
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke HerdingaFormula :: AParser (Annoted FORMULA)
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke HerdingaFormula = bind appendAnno (annoParser formula) lineAnnos
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke Herdingformula :: AParser FORMULA
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke Herdingformula = impFormula []
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke HerdingimpFormula :: [String] -> AParser FORMULA
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke HerdingimpFormula k =
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke Herding do f <- andOrFormula k
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke Herding do c <- implKey
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke Herding (fs, ps) <- andOrFormula k `separatedBy` implKey
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke Herding return (makeImpl (f:fs) (map tokPos (c:ps)))
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke Herding do c <- ifKey
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke Herding (fs, ps) <- andOrFormula k `separatedBy` ifKey
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke Herding return (makeIf (f:fs) (map tokPos (c:ps)))
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke Herding do c <- asKey equivS
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke Herding g <- andOrFormula k
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke Herding return (Equivalence f g [tokPos c])
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke Herding where makeImpl [f,g] p = Implication f g p
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke Herding makeImpl (f:r) (c:p) =
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke Herding Implication f (makeImpl r p) [c]
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke Herding makeImpl _ _ = error "makeImpl got illegal argument"
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke Herding makeIf l p = makeImpl (reverse l) (reverse p)
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke HerdingandOrFormula :: [String] -> AParser FORMULA
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke HerdingandOrFormula k =
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke Herding do f <- primFormula k
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke Herding do c <- andKey
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke Herding (fs, ps) <- primFormula k `separatedBy` andKey
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke Herding return (Conjunction (f:fs) (map tokPos (c:ps)))
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke Herding do c <- orKey
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke Herding (fs, ps) <- primFormula k `separatedBy` orKey
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke Herding return (Disjunction (f:fs) (map tokPos (c:ps)))
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke HerdingimplKey, ifKey :: AParser Token
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke HerdingimplKey = asKey implS
c36c47428b2f42fe09eab533acf6be19d6d9f259Wiebke HerdingifKey = asKey ifS