ToSExpr.hs revision d4aed7a2eea6b546c0d9520d85038addb7beb12f
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
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian MaederModule : $Header$
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian MaederDescription : translate CASL to S-Expressions
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian MaederCopyright : (c) C. Maeder, DFKI 2008
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian MaederMaintainer : Christian.Maeder@dfki.de
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian MaederStability : provisional
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian MaederPortability : portable
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maedertranslation of CASL to S-Expressions
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maederimport qualified Data.Map as Map
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maederimport qualified Data.Set as Set
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maederimport qualified Data.List as List
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian MaederpredToSSymbol :: Sign f e -> PRED_SYMB -> SExpr
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian MaederpredToSSymbol sign p = case p of
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder Pred_name _ -> error "predToSSymbol"
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder Qual_pred_name i t _ -> case Map.lookup i $ predMap sign of
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder Nothing -> error "predToSSymbol2"
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder Just s -> case List.elemIndex (toPredType t) $ Set.toList s of
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder Nothing -> error "predToSSymbol3"
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder Just n -> idToSSymbol (n + 1) i
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian MaederopToSSymbol :: Sign f e -> OP_SYMB -> SExpr
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian MaederopToSSymbol sign o = case o of
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder Op_name _ -> error "opToSSymbol"
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder Qual_op_name i (Op_type _ args res _) _ ->
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder case Map.lookup i $ opMap sign of
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder Nothing -> error "opToSSymbol2"
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder (\ r -> opArgs r == args && opRes r == res) $ Set.toList s of
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder Nothing -> error "opToSSymbol3"
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder Just n -> idToSSymbol (n + 1) i
d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian MaedersortToSSymbol :: Id -> SExpr
d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian MaedersortToSSymbol = idToSSymbol 0
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian MaedervarToSSymbol :: Token -> SExpr
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian MaedervarToSSymbol = SSymbol . transToken
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian MaedervarDeclToSExpr :: (VAR, SORT) -> SExpr
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian MaedervarDeclToSExpr (v, s) =
d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maeder SList [SSymbol "vardecl-indet", varToSSymbol v, sortToSSymbol s]
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maedersfail :: String -> Range -> Result a
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maedersfail s r = fatal_error ("unexpected " ++ s) r
a94f7b3982dccd2e01bd87f64de1aeab6edac118Christian MaedersRec :: Bool -> Sign a e -> (f -> Result SExpr)
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder -> Record f (Result SExpr) (Result SExpr)
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian MaedersRec withQuant sign mf = Record
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder { foldQuantification = \ _ q vs r p -> if withQuant then do
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder s <- case q of
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder Unique_existential -> sfail "Unique_existential" p
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder _ -> return $ SSymbol $ case q of
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder Universal -> "all"
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder Existential -> "ex"
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder let vl = SList $ map varDeclToSExpr $ flatVAR_DECLs vs
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder return $ SList [s, vl, f]
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder else sfail "Quantification" p
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder , foldConjunction = \ _ rs _ -> do
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder fs <- sequence rs
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder return $ SList $ SSymbol "and" : fs
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder , foldDisjunction = \ _ rs _ -> do
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder fs <- sequence rs
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder return $ SList $ SSymbol "or" : fs
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder , foldImplication = \ _ r1 r2 b _ -> do
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder return $ SList $ SSymbol "implies" : if b then [f1, f2] else [f2, f1]
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder , foldEquivalence = \ _ r1 r2 _ -> do
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder return $ SList [SSymbol "equiv", f1, f2]
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder , foldNegation = \ _ r _ -> do
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder return $ SList [SSymbol "not", f]
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder , foldTrue_atom = \ _ _ -> return $ SSymbol "true"
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder , foldFalse_atom = \ _ _ -> return $ SSymbol "false"
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder , foldPredication = \ _ p rs _ -> do
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder ts <- sequence rs
e7b0b439ffae08514ac1afc62186d9a87ec6bd59Christian Maeder return $ SList $ SSymbol "papply" : predToSSymbol sign p : ts
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , foldDefinedness = \ _ _ r -> sfail "Definedness" r
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , foldExistl_equation = \ _ _ _ r -> sfail "Existl_equation" r
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder , foldStrong_equation = \ _ r1 r2 _ -> do
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder return $ SList [SSymbol "eq", t1, t2]
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , foldMembership = \ _ _ _ r -> sfail "Membership" r
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , foldMixfix_formula = \ t _ -> sfail "Mixfix_formula" $ getRange t
d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maeder , foldSort_gen_ax = \ _ cs b ->
d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maeder let (srts, ops, _) = recover_Sort_gen_ax cs in
d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maeder return $ SList $ SSymbol ((if b then "freely-" else "") ++ "generated")
d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maeder : (case srts of
d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maeder [s] -> sortToSSymbol s
d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maeder _ -> SList $ map sortToSSymbol srts)
d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maeder : map (opToSSymbol sign) ops
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder , foldExtFORMULA = \ _ f -> mf f
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , foldSimpleId = \ _ t -> sfail "Simple_id" $ tokPos t
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder , foldQual_var = \ _ v _ _ ->
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder return $ SList [SSymbol "varterm", varToSSymbol v]
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder , foldApplication = \ _ o rs _ -> do
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder ts <- sequence rs
e7b0b439ffae08514ac1afc62186d9a87ec6bd59Christian Maeder return $ SList $ SSymbol "fapply" : opToSSymbol sign o : ts
a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder , foldSorted_term = \ _ r _ _ -> r
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , foldCast = \ _ _ _ r -> sfail "Cast" r
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , foldConditional = \ _ _ _ _ r -> sfail "Conditional" r
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , foldMixfix_qual_pred = \ _ p -> sfail "Mixfix_qual_pred" $ getRange p
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , foldMixfix_term = \ (Mixfix_term ts) _ ->
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder sfail "Mixfix_term" $ getRange ts
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , foldMixfix_token = \ _ t -> sfail "Mixfix_token" $ tokPos t
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , foldMixfix_sorted_term = \ _ _ r -> sfail "Mixfix_sorted_term" r
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , foldMixfix_cast = \ _ _ r -> sfail "Mixfix_cast" r
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , foldMixfix_parenthesized = \ _ _ r -> sfail "Mixfix_parenthesized" r
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , foldMixfix_bracketed = \ _ _ r -> sfail "Mixfix_bracketed" r
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder , foldMixfix_braced = \ _ _ r -> sfail "Mixfix_braced" r