> module Token(tokenise) where
> import Core_datatype
> import Kernel
> import Type_defs
> endofline = "\n\f\r"
> whitespace = " \t" ++ endofline
> a_symbol = "!#$&*-+=~<>?/\\.:|@"
> singlechrs = ",;\"`\'(){}[]\176\185"
> binder = "\208\211\236\177\178\229\196"
> ifx_binder = "\183\184\167\182\187"
> ifx_op = "\179\180=\172:"
> reserved = [ "empty", "signature", "extend", "combine", "with", "sharing" ,
> "++", "=", "(", ")", "@", "operator", ";", ":", "\189",
> "datatype", "|", "case", "of", "\167", "recurse", "end",
> "typed", "fn", "rec", "if", "then", "else", "let", "in",
> "\168", "\169", "{", "}", "[", "]", "\208", "\211", "\236",
> "\229", "\177", "\178", ".", ",", "\181", "\179", "\180",
> "\182", "\172", "\183", "\184", "\185", "\176", "BinL",
> "BinR", "Pre", "Post", "\196", "\187" ]
> tokenise :: String -> [Token]
> tokenise string
> = denull ( scan' string "" )
> denull :: [Token] -> [Token]
> denull ( Clr "" : tkl ) = denull tkl
> denull ( Clr tk : tkl )
> = tag rev_tk : denull tkl
> where
> tag | rev_tk `elem` reserved = Rvd
> | otherwise = Clr
> rev_tk = reverse tk
> denull ( Rvd tk : tkl ) = error " optimise to trap some reserved earlier and reduce length of reserved set"
> denull ( Scan_Err mess : _ ) = [ Scan_Err mess ]
> denull ( tk : tkl ) = tk : denull tkl
> denull [] = []
> denull x = error ( show x )
> scan' ( a : x ) current
> | a `elem` binder = Clr current : ( Bdr ( mk_bdr a ) : scan' x "" )
> | a `elem` ifx_binder = Clr current : ( IfxBdr [a] : scan' x "" )
> | a `elem` ifx_op = Clr current : ( IfxOp [a] : scan' x "" )
> | single a = Clr current : ( Clr [a] : scan' x "" )
> | a `elem` a_symbol = Clr current : symbol_scan x [a]
> | a `elem` whitespace = Clr current : scan' x ""
> | alphanum' a = scan' x ( a : current )
> | a == '%' = Clr current : scan' ( discard x ) ""
> | a == '^' = super_scan x ( '^' : current )
> | otherwise = [ Scan_Err "\nInvalid character\n" ]
> scan' [] current = [ Clr current ]
> symbol_scan :: String -> String -> [Token]
> symbol_scan ( a : x ) current
> | a `elem` a_symbol = symbol_scan x ( a : current )
> | a == '^' = super_scan x ( a : current )
> | otherwise = Clr current : scan' ( a : x ) ""
> symbol_scan [] current = [ Clr current ]
> super_scan _ "^" = [ Scan_Err "\nAttempt to superscript invalid string\n"]
> super_scan ( a : x ) current
> | alphanum a || a `elem` a_symbol
> = Clr ( a : current ) : scan' x ""
> | otherwise = [ Scan_Err "\nInvalid superscript character\n" ]
> super_scan [] _ = [ Scan_Err "\nEmpty superscript\n" ]
> alphanum' ch = alphanum ch || ch == '_'
> alphanum ch
> = ( ch >= 'A' && ch <= 'Z' ) ||
> ( ch >= 'a' && ch <= 'z' ) ||
> ( ch >= '0' && ch <= '9' )
> single ch
> = ch `elem` singlechrs || ch > '\DEL'
> discard :: String -> String
> discard ( ch : x )
> | ch `elem` endofline = x
> | otherwise = discard x
> discard [] = ""
> mk_bdr :: Char -> Binder_conn
> {-
> mk_bdr x | fromEnum x == 208 = Pi
> mk_bdr x | fromEnum x == 211 = Sigma
> mk_bdr x | fromEnum x == 236 = Lambda
> mk_bdr x | fromEnum x == 177 = Forall
> mk_bdr x | fromEnum x == 178 = Exists
> mk_bdr x | fromEnum x == 229 = Choose
> -}
> mk_bdr '\208' = Pi
> mk_bdr '\211' = Sigma
> mk_bdr '\236' = Lambda
> mk_bdr '\177' = Forall
> mk_bdr '\178' = Exists
> mk_bdr '\229' = Choose
> mk_bdr '\196' = Delta
> mk_bdr oth = error ( "Mk_bdr: " ++ [oth])
token display function used in debugging messages
> disp_tk :: Token -> String
> disp_tk ( Rvd str ) = str
> disp_tk ( Clr str ) = str
|
