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
|
----------------------------------------------------------------------
-- |
-- Module : AppPredefined
-- Maintainer : AR
-- Stability : (stable)
-- Portability : (portable)
--
-- > CVS $Date: 2005/02/18 19:21:12 $
-- > CVS $Author: peb $
-- > CVS $Revision: 1.9 $
--
-- Predefined function type signatures and definitions.
-----------------------------------------------------------------------------
module AppPredefined (isInPredefined, typPredefined, appPredefined
) where
import Operations
import Grammar
import Ident
import Macros
import PrGrammar (prt,prt_,prtBad)
---- import PGrammar (pTrm)
-- predefined function type signatures and definitions. AR 12/3/2003.
isInPredefined :: Ident -> Bool
isInPredefined = err (const True) (const False) . typPredefined
typPredefined :: Ident -> Err Type
typPredefined c@(IC f) = case f of
"Int" -> return typePType
"Ints" -> return $ mkFunType [cnPredef "Int"] typePType
"PBool" -> return typePType
"PFalse" -> return $ cnPredef "PBool"
"PTrue" -> return $ cnPredef "PBool"
"dp" -> return $ mkFunType [cnPredef "Int",typeTok] typeTok
"drop" -> return $ mkFunType [cnPredef "Int",typeTok] typeTok
"eqInt" -> return $ mkFunType [cnPredef "Int",cnPredef "Int"] (cnPredef "PBool")
"lessInt"-> return $ mkFunType [cnPredef "Int",cnPredef "Int"] (cnPredef "PBool")
"eqStr" -> return $ mkFunType [typeTok,typeTok] (cnPredef "PBool")
"length" -> return $ mkFunType [typeTok] (cnPredef "Int")
"occur" -> return $ mkFunType [typeTok,typeTok] (cnPredef "PBool")
"plus" -> return $ mkFunType [cnPredef "Int",cnPredef "Int"] (cnPredef "Int")
---- "read" -> (P : Type) -> Tok -> P
"show" -> return $ mkProd -- (P : PType) -> P -> Tok
([(zIdent "P",typePType),(wildIdent,Vr (zIdent "P"))],typeStr,[])
"toStr" -> return $ mkProd -- (L : Type) -> L -> Str
([(zIdent "L",typeType),(wildIdent,Vr (zIdent "L"))],typeStr,[])
"take" -> return $ mkFunType [cnPredef "Int",typeTok] typeTok
"tk" -> return $ mkFunType [cnPredef "Int",typeTok] typeTok
_ -> prtBad "unknown in Predef:" c
typPredefined c = prtBad "unknown in Predef:" c
appPredefined :: Term -> Term
appPredefined t = case t of
App f x -> case f of
-- one-place functions
Q (IC "Predef") (IC f) -> case (f, appPredefined x) of
("length", K s) -> EInt $ length s
_ -> t
-- two-place functions
App (Q (IC "Predef") (IC f)) z -> case (f, appPredefined z, appPredefined x) of
("drop", EInt i, K s) -> K (drop i s)
("take", EInt i, K s) -> K (take i s)
("tk", EInt i, K s) -> K (take (max 0 (length s - i)) s)
("dp", EInt i, K s) -> K (drop (max 0 (length s - i)) s)
("eqStr",K s, K t) -> if s == t then predefTrue else predefFalse
("occur",K s, K t) -> if substring s t then predefTrue else predefFalse
("eqInt",EInt i, EInt j) -> if i==j then predefTrue else predefFalse
("lessInt",EInt i, EInt j) -> if i<j then predefTrue else predefFalse
("plus", EInt i, EInt j) -> EInt $ i+j
("show", _, t) -> foldr C Empty $ map K $ words $ prt t
("read", _, K s) -> str2tag s --- because of K, only works for atomic tags
("toStr", _, t) -> trm2str t
_ -> t
_ -> t
_ -> t
-- read makes variables into constants
str2tag :: String -> Term
str2tag s = case s of
---- '\'' : cs -> mkCn $ pTrm $ init cs
_ -> Cn $ IC s ---
where
mkCn t = case t of
Vr i -> Cn i
App c a -> App (mkCn c) (mkCn a)
_ -> t
predefTrue = Q (IC "Predef") (IC "PTrue")
predefFalse = Q (IC "Predef") (IC "PFalse")
substring :: String -> String -> Bool
substring s t = case (s,t) of
(c:cs, d:ds) -> (c == d && substring cs ds) || substring s ds
([],_) -> True
_ -> False
trm2str :: Term -> Term
trm2str t = case t of
R ((_,(_,s)):_) -> trm2str s
T _ ((_,s):_) -> trm2str s
TSh _ ((_,s):_) -> trm2str s
V _ (s:_) -> trm2str s
C _ _ -> t
K _ -> t
Empty -> t
_ -> K $ "ERROR_toStr_" ++ prt_ t --- eliminated by type checker
|
