diff --git a/CTT.hs b/CTT.hs --- a/CTT.hs +++ b/CTT.hs @@ -273,7 +273,6 @@ instance Show Val where show = showVal - fstVal, sndVal, unSquare :: Val -> Val fstVal (VPair _ a _) = a fstVal x = error $ "error fstVal: " ++ show x @@ -392,10 +391,10 @@ showTer :: Ter -> String showTer U = "U" -showTer (Var x) = "x" +showTer (Var x) = x showTer (App e0 e1) = showTer e0 <+> showTer1 e1 showTer (Pi e0 e1) = "Pi" <+> showTers [e0,e1] -showTer (Lam x e) = "\\" ++ x ++ "->" <+> showTer e +showTer (Lam x e) = "\\" ++ x <+> "->" <+> showTer e showTer (LSum (_,str) _) = str showTer (Branch (n,str) _) = str ++ show n showTer (Undef (n,str)) = str ++ show n @@ -430,7 +429,6 @@ showTer1 (Con c []) = c showTer1 (Var x) = x showTer1 u = parens $ showTer u - showVal :: Val -> String showVal VU = "U" diff --git a/Concrete.hs b/Concrete.hs --- a/Concrete.hs +++ b/Concrete.hs @@ -185,7 +185,6 @@ checkDef (n,d) = throwError ("Mismatching names in " ++ show n ++ " and " ++ show d) - resolveMutual :: [Def] -> Resolver A.Def resolveMutual defs = do tdecls' <- mapM resolveTDecl tdecls @@ -200,4 +199,3 @@ isTDecl _ = False resolveTDecl (DefTDecl n e) = do e' <- resolveExp e return (unIdent n, e') - diff --git a/Eval.hs b/Eval.hs --- a/Eval.hs +++ b/Eval.hs diff --git a/Exp.cf b/Exp.cf --- a/Exp.cf +++ b/Exp.cf @@ -3,7 +3,7 @@ comment "--" ; comment "{-" "-}" ; -layout "where", "let", "of", "split" ; +layout "where", "let", "of", "split" ; -- , "mutual" ; layout stop "in" ; -- Do not use layout toplevel as it makes pExp fail! @@ -15,9 +15,12 @@ Def. Def ::= AIdent [Arg] "=" ExpWhere ; DefTDecl. Def ::= AIdent ":" Exp ; DefData. Def ::= "data" AIdent [Arg] "=" [Sum] ; --- TODO: Mutual not working. --- NB: No iterated mutuals allowed! --- DefMutual. Def ::= "mutual" "{" [Def] "}" "end" ; + +-- Anders: This is kind of an ugly way to get mutual to work, but at least it +-- works, I guess there is a bug in bnfc when handling layout blocks and lists +-- TODO: Bug report? +-- DefMutual. Def ::= Def "mutual" "{" [Def] "}" ; +-- Mutual. Def ::= "mutual" "{" [Def] "}" ; separator Def ";" ; diff --git a/Main.hs b/Main.hs --- a/Main.hs +++ b/Main.hs @@ -3,14 +3,15 @@ import Control.Monad.Trans.Reader import Control.Monad.Error import Data.List +import System.Directory import System.Environment +import System.Console.GetOpt import System.Console.Haskeline -import System.Directory import Exp.Lex import Exp.Par import Exp.Print -import Exp.Abs +import Exp.Abs hiding (NoArg) import Exp.Layout import Exp.ErrM import MTTtoCTT @@ -21,6 +22,19 @@ type Interpreter a = InputT IO a +-- Flag handling +data Flag = Debug + deriving (Eq,Show) + +options :: [OptDescr Flag] +options = [ Option "d" ["debug"] (NoArg Debug) "Run in debugging mode" ] + +parseOpts :: [String] -> IO ([Flag],[String]) +parseOpts argv = case getOpt Permute options argv of + (o,n,[]) -> return (o,n) + (_,_,errs) -> ioError (userError (concat errs ++ usageInfo header options)) + where header = "Usage: cubical [OPTION...] [FILES...]" + defaultPrompt :: String defaultPrompt = "> " @@ -33,26 +47,40 @@ putStrLn $ "\n[Linearized tree]\n\n" ++ printTree tree main :: IO () -main = getArgs >>= runInputT defaultSettings . runInterpreter +main = do + args <- getArgs + (flags,files) <- parseOpts args + runInputT defaultSettings $ runInterpreter (Debug `elem` flags) files --- (not ok,loaded,already loaded defs) -> to load -> (newnotok, newloaded, newdefs) -imports :: ([String],[String],[Def]) -> String-> Interpreter ([String],[String],[Def]) +-- (not ok,loaded,already loaded defs) -> to load -> (newnotok, newloaded, newdefs) +imports :: ([String],[String],[Def]) -> String -> Interpreter ([String],[String],[Def]) imports st@(notok,loaded,defs) f - | f `elem` notok = fail ("Looping imports in " ++ f) + | f `elem` notok = do + outputStrLn $ "Looping imports in " ++ f + return ([],[],[]) | f `elem` loaded = return st | otherwise = do - s <- lift $ readFile f - let ts = lexer s - case pModule ts of - Bad s -> fail $ "Parse Failed in file " ++ show f ++ "\n" ++ show s - Ok mod@(Module _ imps defs') -> do - let imps' = [ unIdent s ++ ".cub" | Import s <- imps ] - (notok1,loaded1,def1) <- foldM imports (f:notok,loaded,defs) imps' - outputStrLn $ "Parsed file " ++ show f ++ " successfully!" - return (notok,f:loaded1,def1 ++ defs') + b <- lift $ doesFileExist f + if not b + then do + outputStrLn ("The file " ++ f ++ " does not exist") + return ([],[],[]) + else do + s <- lift $ readFile f + let ts = lexer s + case pModule ts of + Bad s -> do + outputStrLn $ "Parse Failed in file " ++ show f ++ "\n" ++ show s + return ([],[],[]) + Ok mod@(Module _ imps defs') -> do + let imps' = [ unIdent s ++ ".cub" | Import s <- imps ] + (notok1,loaded1,def1) <- foldM imports (f:notok,loaded,defs) imps' + outputStrLn $ "Parsed file " ++ show f ++ " successfully!" + return (notok,f:loaded1,def1 ++ defs') -runInterpreter :: [FilePath] -> Interpreter () -runInterpreter fs = case fs of +-- The Bool is intended to be whether or not to run in debug mode +runInterpreter :: Bool -> [FilePath] -> Interpreter () +runInterpreter b fs = case fs of [f] -> do -- parse and type-check files (_,_,defs) <- imports ([],[],[]) f @@ -60,14 +88,19 @@ let cs = concat [ [ unIdent n | Sum n _ <- lbls] | DefData _ _ lbls <- defs ] let res = runResolver (local (insertConstrs cs) (resolveDefs defs)) case res of - Left err -> outputStrLn $ "Resolver failed: " ++ err + Left err -> do + outputStrLn $ "Resolver failed: " ++ err + loop [] A.tEmpty Right adefs -> case A.runDefs A.tEmpty adefs of - Left err -> outputStrLn $ "Type checking failed: " ++ err + Left err -> do + outputStrLn $ "Type checking failed: " ++ err + loop [] A.tEmpty Right tenv -> do outputStrLn "File loaded." loop cs tenv - _ -> do outputStrLn $ "Exactly one file expected: " ++ show fs - loop [] A.tEmpty + _ -> do + outputStrLn $ "Exactly one file expected: " ++ show fs + loop [] A.tEmpty where loop :: [String] -> A.TEnv -> Interpreter () loop cs tenv@(A.TEnv _ rho _) = do @@ -75,8 +108,8 @@ case input of Nothing -> outputStrLn help >> loop cs tenv Just ":q" -> return () - Just ":r" -> runInterpreter fs - Just (':':'l':' ':str) -> runInterpreter (words str) + Just ":r" -> runInterpreter b fs + Just (':':'l':' ':str) -> runInterpreter b (words str) Just (':':'c':'d':' ':str) -> lift (setCurrentDirectory str) >> loop cs tenv Just ":h" -> outputStrLn help >> loop cs tenv Just str -> let ts = lexer str in diff --git a/Makefile b/Makefile --- a/Makefile +++ b/Makefile @@ -1,11 +1,11 @@ all: - ghc --make -O2 -o cubigle Main.hs + ghc --make -O2 -o cubical Main.hs bnfc: bnfc -d Exp.cf happy -gca Exp/Par.y alex -g Exp/Lex.x ghc --make Exp/Test.hs -o Exp/Test clean: - rm -f *.log *.aux *.hi *.o cubigle + rm -f *.log *.aux *.hi *.o cubical cd Exp && rm -f ParExp.y LexExp.x LexhExp.hs \ ParExp.hs PrintExp.hs AbsExp.hs *.o *.hi diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -13,13 +13,21 @@ `cabal install` -To only build cubical do +To only build (not install) cubical do `cabal configure` `cabal build` +Alternatively one can also use the Makefile to build the system by typing: + `make bnfc && make` + +However this requires that the following Haskell packages are installed: + + mtl, haskeline, directory, BNFC, alex, happy + + USAGE ----- @@ -89,13 +97,15 @@ * let/where: `let D in e` where D is a list of definitions an alternative syntax is `e where D` +* `undefined` like in Haskell + The syntax allows Landin's offside rule similar to Haskell. The basic (untyped) language has a direct simple denotational -semantics Type theory works with the total part of this language (it +semantics. Type theory works with the total part of this language (it is possible to define totality at the denotational semantics level). Our evaluator works in a nominal version of this semantics. The -type-checker assumes that we work in this total part, in particular, +type-checker assumes that we work in this total part, however, there is no termination check. @@ -106,11 +116,11 @@ which can be thought of as varying over the unit interval [0,1]. A path connecting a0 and a1 in the direction x is a value p(x) such that p(0) = a0 and p(1) = a1. An element in the identity type a0 = a1 is -then of the form p(x) where the name x is bound. An identity proof +then of the form \p(x) where the name x is bound. An identity proof in an identity type will then be interpreted as a "square" of the form -p(x,y). See examples/hedberg.cub and the example test3 (in the +\\p(x,y). See examples/hedberg.cub and the example test3 (in the current implementation directions/names are represented by numbers). - + Operationally, a type is explained by giving what are its Kan filling operation. For instance, we have to explain what are the Kan filling for the dependent product. @@ -211,7 +221,7 @@ * Voevodsky's home page on univalent foundation - * HoTT book + * HoTT book * Type Theory in Color, J.P. Bernardy, G. Moulin diff --git a/Setup.hs b/Setup.hs --- a/Setup.hs +++ b/Setup.hs @@ -1,8 +1,22 @@ +import Control.Monad import Distribution.Simple +import System.Directory import System.Process import System.Exit + +main :: IO () main = do - ret <- system "bnfc -d Exp.cf" - case ret of - ExitSuccess -> defaultMain - ExitFailure n -> error $ "bnfc command not found or error" ++ show n + b <- doesDirectoryExist "Exp" + -- run bnfc if the Exp directory does not exist + when (not b) bnfc + t1 <- getModificationTime "Exp.cf" + t2 <- getModificationTime "Exp" + -- run bnfc if Exp.cf has been modified + when (t1 > t2) bnfc + defaultMain + where + bnfc = do + ret <- system "bnfc -d Exp.cf" + case ret of + ExitSuccess -> defaultMain + ExitFailure n -> error $ "bnfc command not found or error" ++ show n diff --git a/cubical.cabal b/cubical.cabal --- a/cubical.cabal +++ b/cubical.cabal @@ -1,5 +1,5 @@ name: cubical -version: 0.1.0 +version: 0.1.1 synopsis: Implementation of Univalence in Cubical Sets description: Cubical implements an experimental simple type checker for type theory with univalence with an evaluator for closed terms. diff --git a/dist/build/cubical/cubical-tmp/Exp/Lex.hs b/dist/build/cubical/cubical-tmp/Exp/Lex.hs deleted file mode 100644 --- a/dist/build/cubical/cubical-tmp/Exp/Lex.hs +++ /dev/null @@ -1,351 +0,0 @@ -{-# LANGUAGE CPP,MagicHash #-} -{-# LINE 3 "Exp/Lex.x" #-} - -{-# OPTIONS -fno-warn-incomplete-patterns #-} -module Exp.Lex where - - - -import qualified Data.Bits -import Data.Word (Word8) - -#if __GLASGOW_HASKELL__ >= 603 -#include "ghcconfig.h" -#elif defined(__GLASGOW_HASKELL__) -#include "config.h" -#endif -#if __GLASGOW_HASKELL__ >= 503 -import Data.Array -import Data.Char (ord) -import Data.Array.Base (unsafeAt) -#else -import Array -import Char (ord) -#endif -#if __GLASGOW_HASKELL__ >= 503 -import GHC.Exts -#else -import GlaExts -#endif -alex_base :: AlexAddr -alex_base = AlexA# "\xf8\xff\xff\xff\xd9\xff\xff\xff\x49\x00\x00\x00\x1c\x01\x00\x00\x9c\x01\x00\x00\x6f\x02\x00\x00\xef\x02\x00\x00\xef\x03\x00\x00\xb7\xff\xff\xff\x00\x00\x00\x00\xe0\x03\x00\x00\x00\x00\x00\x00\x8b\x00\x00\x00\x1d\x02\x00\x00\xe0\x04\x00\x00\xa0\x04\x00\x00\x00\x00\x00\x00\x96\x05\x00\x00\x69\x06\x00\x00\x00\x00\x00\x00\xfe\xff\xff\xff\xdf\xff\xff\xff\x00\x00\x00\x00\x42\x07\x00\x00"# - -alex_table :: AlexAddr -alex_table = AlexA# "\x00\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x11\x00\x14\x00\x14\x00\x14\x00\x14\x00\x14\x00\x05\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x16\x00\x14\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x14\x00\x00\x00\x16\x00\x16\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x16\x00\x16\x00\x00\x00\x16\x00\x00\x00\x00\x00\x00\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x00\x00\x16\x00\x00\x00\x00\x00\x16\x00\x00\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x15\x00\x16\x00\x16\x00\x03\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x00\x00\x00\x00\x00\x00\x00\x00\x0d\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x13\x00\x00\x00\x00\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x07\x00\x08\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x02\x00\x0f\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x12\x00\x00\x00\x00\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x07\x00\x08\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x0e\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x02\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x00\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x00\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x07\x00\x08\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x04\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x0c\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x0e\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x0f\x00\x04\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0c\x00\x06\x00\x09\x00\x09\x00\x09\x00\x0a\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x02\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x07\x00\x08\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x17\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x00\x00\x00\x00\x00\x00\x00\x00\x17\x00\x00\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x17\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0d\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"# - -alex_check :: AlexAddr -alex_check = AlexA# "\xff\xff\x09\x00\x0a\x00\x0b\x00\x0c\x00\x0d\x00\x2d\x00\x09\x00\x0a\x00\x0b\x00\x0c\x00\x0d\x00\x2d\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x3e\x00\x20\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x20\x00\xff\xff\x28\x00\x29\x00\xff\xff\xff\xff\xff\xff\x2d\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x3a\x00\x3b\x00\xff\xff\x3d\x00\xff\xff\xff\xff\xff\xff\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\xff\xff\x5c\x00\xff\xff\xff\xff\x5f\x00\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\x7b\x00\x7c\x00\x7d\x00\x2d\x00\xc0\x00\xc1\x00\xc2\x00\xc3\x00\xc4\x00\xc5\x00\xc6\x00\xc7\x00\xc8\x00\xc9\x00\xca\x00\xcb\x00\xcc\x00\xcd\x00\xce\x00\xcf\x00\xd0\x00\xd1\x00\xd2\x00\xd3\x00\xd4\x00\xd5\x00\xd6\x00\xd7\x00\xd8\x00\xd9\x00\xda\x00\xdb\x00\xdc\x00\xdd\x00\xde\x00\xdf\x00\xe0\x00\xe1\x00\xe2\x00\xe3\x00\xe4\x00\xe5\x00\xe6\x00\xe7\x00\xe8\x00\xe9\x00\xea\x00\xeb\x00\xec\x00\xed\x00\xee\x00\xef\x00\xf0\x00\xf1\x00\xf2\x00\xf3\x00\xf4\x00\xf5\x00\xf6\x00\xf7\x00\xf8\x00\xf9\x00\xfa\x00\xfb\x00\xfc\x00\xfd\x00\xfe\x00\xff\x00\xff\xff\xff\xff\xff\xff\xff\xff\xc3\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x7d\x00\xff\xff\xff\xff\x80\x00\x81\x00\x82\x00\x83\x00\x84\x00\x85\x00\x86\x00\x87\x00\x88\x00\x89\x00\x8a\x00\x8b\x00\x8c\x00\x8d\x00\x8e\x00\x8f\x00\x90\x00\x91\x00\x92\x00\x93\x00\x94\x00\x95\x00\x96\x00\x97\x00\x98\x00\x99\x00\x9a\x00\x9b\x00\x9c\x00\x9d\x00\x9e\x00\x9f\x00\xa0\x00\xa1\x00\xa2\x00\xa3\x00\xa4\x00\xa5\x00\xa6\x00\xa7\x00\xa8\x00\xa9\x00\xaa\x00\xab\x00\xac\x00\xad\x00\xae\x00\xaf\x00\xb0\x00\xb1\x00\xb2\x00\xb3\x00\xb4\x00\xb5\x00\xb6\x00\xb7\x00\xb8\x00\xb9\x00\xba\x00\xbb\x00\xbc\x00\xbd\x00\xbe\x00\xbf\x00\xc0\x00\xc1\x00\xc2\x00\xc3\x00\xc4\x00\xc5\x00\xc6\x00\xc7\x00\xc8\x00\xc9\x00\xca\x00\xcb\x00\xcc\x00\xcd\x00\xce\x00\xcf\x00\xd0\x00\xd1\x00\xd2\x00\xd3\x00\xd4\x00\xd5\x00\xd6\x00\xd7\x00\xd8\x00\xd9\x00\xda\x00\xdb\x00\xdc\x00\xdd\x00\xde\x00\xdf\x00\xe0\x00\xe1\x00\xe2\x00\xe3\x00\xe4\x00\xe5\x00\xe6\x00\xe7\x00\xe8\x00\xe9\x00\xea\x00\xeb\x00\xec\x00\xed\x00\xee\x00\xef\x00\xf0\x00\xf1\x00\xf2\x00\xf3\x00\xf4\x00\xf5\x00\xf6\x00\xf7\x00\xf8\x00\xf9\x00\xfa\x00\xfb\x00\xfc\x00\xfd\x00\xfe\x00\xff\x00\x2d\x00\xbf\x00\xc0\x00\xc1\x00\xc2\x00\xc3\x00\xc4\x00\xc5\x00\xc6\x00\xc7\x00\xc8\x00\xc9\x00\xca\x00\xcb\x00\xcc\x00\xcd\x00\xce\x00\xcf\x00\xd0\x00\xd1\x00\xd2\x00\xd3\x00\xd4\x00\xd5\x00\xd6\x00\xd7\x00\xd8\x00\xd9\x00\xda\x00\xdb\x00\xdc\x00\xdd\x00\xde\x00\xdf\x00\xe0\x00\xe1\x00\xe2\x00\xe3\x00\xe4\x00\xe5\x00\xe6\x00\xe7\x00\xe8\x00\xe9\x00\xea\x00\xeb\x00\xec\x00\xed\x00\xee\x00\xef\x00\xf0\x00\xf1\x00\xf2\x00\xf3\x00\xf4\x00\xf5\x00\xf6\x00\xf7\x00\xf8\x00\xf9\x00\xfa\x00\xfb\x00\xfc\x00\xfd\x00\xfe\x00\xff\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x7d\x00\xff\xff\xff\xff\x80\x00\x81\x00\x82\x00\x83\x00\x84\x00\x85\x00\x86\x00\x87\x00\x88\x00\x89\x00\x8a\x00\x8b\x00\x8c\x00\x8d\x00\x8e\x00\x8f\x00\x90\x00\x91\x00\x92\x00\x93\x00\x94\x00\x95\x00\x96\x00\x97\x00\x98\x00\x99\x00\x9a\x00\x9b\x00\x9c\x00\x9d\x00\x9e\x00\x9f\x00\xa0\x00\xa1\x00\xa2\x00\xa3\x00\xa4\x00\xa5\x00\xa6\x00\xa7\x00\xa8\x00\xa9\x00\xaa\x00\xab\x00\xac\x00\xad\x00\xae\x00\xaf\x00\xb0\x00\xb1\x00\xb2\x00\xb3\x00\xb4\x00\xb5\x00\xb6\x00\xb7\x00\xb8\x00\xb9\x00\xba\x00\xbb\x00\xbc\x00\xbd\x00\xbe\x00\xbf\x00\xc0\x00\xc1\x00\xc2\x00\xc3\x00\xc4\x00\xc5\x00\xc6\x00\xc7\x00\xc8\x00\xc9\x00\xca\x00\xcb\x00\xcc\x00\xcd\x00\xce\x00\xcf\x00\xd0\x00\xd1\x00\xd2\x00\xd3\x00\xd4\x00\xd5\x00\xd6\x00\xd7\x00\xd8\x00\xd9\x00\xda\x00\xdb\x00\xdc\x00\xdd\x00\xde\x00\xdf\x00\xe0\x00\xe1\x00\xe2\x00\xe3\x00\xe4\x00\xe5\x00\xe6\x00\xe7\x00\xe8\x00\xe9\x00\xea\x00\xeb\x00\xec\x00\xed\x00\xee\x00\xef\x00\xf0\x00\xf1\x00\xf2\x00\xf3\x00\xf4\x00\xf5\x00\xf6\x00\xf7\x00\xf8\x00\xf9\x00\xfa\x00\xfb\x00\xfc\x00\xfd\x00\xfe\x00\xff\x00\x80\x00\x81\x00\x82\x00\x83\x00\x84\x00\x85\x00\x86\x00\x87\x00\x88\x00\x89\x00\x8a\x00\x8b\x00\x8c\x00\x8d\x00\x8e\x00\x8f\x00\x90\x00\x91\x00\x92\x00\x93\x00\x94\x00\x95\x00\x96\x00\x97\x00\x98\x00\x99\x00\x9a\x00\x9b\x00\x9c\x00\x9d\x00\x9e\x00\x9f\x00\xa0\x00\xa1\x00\xa2\x00\xa3\x00\xa4\x00\xa5\x00\xa6\x00\xa7\x00\xa8\x00\xa9\x00\xaa\x00\xab\x00\xac\x00\xad\x00\xae\x00\xaf\x00\xb0\x00\xb1\x00\xb2\x00\xb3\x00\xb4\x00\xb5\x00\xb6\x00\xb7\x00\xb8\x00\xb9\x00\xba\x00\xbb\x00\xbc\x00\xbd\x00\xbe\x00\xbf\x00\xc0\x00\xc1\x00\xc2\x00\xc3\x00\xc4\x00\xc5\x00\xc6\x00\xc7\x00\xc8\x00\xc9\x00\xca\x00\xcb\x00\xcc\x00\xcd\x00\xce\x00\xcf\x00\xd0\x00\xd1\x00\xd2\x00\xd3\x00\xd4\x00\xd5\x00\xd6\x00\xd7\x00\xd8\x00\xd9\x00\xda\x00\xdb\x00\xdc\x00\xdd\x00\xde\x00\xdf\x00\xe0\x00\xe1\x00\xe2\x00\xe3\x00\xe4\x00\xe5\x00\xe6\x00\xe7\x00\xe8\x00\xe9\x00\xea\x00\xeb\x00\xec\x00\xed\x00\xee\x00\xef\x00\xf0\x00\xf1\x00\xf2\x00\xf3\x00\xf4\x00\xf5\x00\xf6\x00\xf7\x00\xf8\x00\xf9\x00\xfa\x00\xfb\x00\xfc\x00\xfd\x00\xfe\x00\xff\x00\x2d\x00\x80\x00\x81\x00\x82\x00\x83\x00\x84\x00\x85\x00\x86\x00\x87\x00\x88\x00\x89\x00\x8a\x00\x8b\x00\x8c\x00\x8d\x00\x8e\x00\x8f\x00\x90\x00\x91\x00\x92\x00\x93\x00\x94\x00\x95\x00\x96\x00\xff\xff\x98\x00\x99\x00\x9a\x00\x9b\x00\x9c\x00\x9d\x00\x9e\x00\x9f\x00\xa0\x00\xa1\x00\xa2\x00\xa3\x00\xa4\x00\xa5\x00\xa6\x00\xa7\x00\xa8\x00\xa9\x00\xaa\x00\xab\x00\xac\x00\xad\x00\xae\x00\xaf\x00\xb0\x00\xb1\x00\xb2\x00\xb3\x00\xb4\x00\xb5\x00\xb6\x00\xff\xff\xb8\x00\xb9\x00\xba\x00\xbb\x00\xbc\x00\xbd\x00\xbe\x00\xbf\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x80\x00\x81\x00\x82\x00\x83\x00\x84\x00\x85\x00\x86\x00\x87\x00\x88\x00\x89\x00\x8a\x00\x8b\x00\x8c\x00\x8d\x00\x8e\x00\x8f\x00\x90\x00\x91\x00\x92\x00\x93\x00\x94\x00\x95\x00\x96\x00\x97\x00\x98\x00\x99\x00\x9a\x00\x9b\x00\x9c\x00\x9d\x00\x9e\x00\x9f\x00\xa0\x00\xa1\x00\xa2\x00\xa3\x00\xa4\x00\xa5\x00\xa6\x00\xa7\x00\xa8\x00\xa9\x00\xaa\x00\xab\x00\xac\x00\xad\x00\xae\x00\xaf\x00\xb0\x00\xb1\x00\xb2\x00\xb3\x00\xb4\x00\xb5\x00\xb6\x00\xb7\x00\xb8\x00\xb9\x00\xba\x00\xbb\x00\xbc\x00\xbd\x00\xbe\x00\xbf\x00\xc0\x00\xc1\x00\xc2\x00\xc3\x00\xc4\x00\xc5\x00\xc6\x00\xc7\x00\xc8\x00\xc9\x00\xca\x00\xcb\x00\xcc\x00\xcd\x00\xce\x00\xcf\x00\xd0\x00\xd1\x00\xd2\x00\xd3\x00\xd4\x00\xd5\x00\xd6\x00\xd7\x00\xd8\x00\xd9\x00\xda\x00\xdb\x00\xdc\x00\xdd\x00\xde\x00\xdf\x00\xe0\x00\xe1\x00\xe2\x00\xe3\x00\xe4\x00\xe5\x00\xe6\x00\xe7\x00\xe8\x00\xe9\x00\xea\x00\xeb\x00\xec\x00\xed\x00\xee\x00\xef\x00\xf0\x00\xf1\x00\xf2\x00\xf3\x00\xf4\x00\xf5\x00\xf6\x00\xf7\x00\xf8\x00\xf9\x00\xfa\x00\xfb\x00\xfc\x00\xfd\x00\xfe\x00\xff\x00\x80\x00\x81\x00\x82\x00\x83\x00\x84\x00\x85\x00\x86\x00\x87\x00\x88\x00\x89\x00\x8a\x00\x8b\x00\x8c\x00\x8d\x00\x8e\x00\x8f\x00\x90\x00\x91\x00\x92\x00\x93\x00\x94\x00\x95\x00\x96\x00\x97\x00\x98\x00\x99\x00\x9a\x00\x9b\x00\x9c\x00\x9d\x00\x9e\x00\x9f\x00\xa0\x00\xa1\x00\xa2\x00\xa3\x00\xa4\x00\xa5\x00\xa6\x00\xa7\x00\xa8\x00\xa9\x00\xaa\x00\xab\x00\xac\x00\xad\x00\xae\x00\xaf\x00\xb0\x00\xb1\x00\xb2\x00\xb3\x00\xb4\x00\xb5\x00\xb6\x00\xb7\x00\xb8\x00\xb9\x00\xba\x00\xbb\x00\xbc\x00\xbd\x00\xbe\x00\xbf\x00\xc0\x00\xc1\x00\xc2\x00\xc3\x00\xc4\x00\xc5\x00\xc6\x00\xc7\x00\xc8\x00\xc9\x00\xca\x00\xcb\x00\xcc\x00\xcd\x00\xce\x00\xcf\x00\xd0\x00\xd1\x00\xd2\x00\xd3\x00\xd4\x00\xd5\x00\xd6\x00\xd7\x00\xd8\x00\xd9\x00\xda\x00\xdb\x00\xdc\x00\xdd\x00\xde\x00\xdf\x00\xe0\x00\xe1\x00\xe2\x00\xe3\x00\xe4\x00\xe5\x00\xe6\x00\xe7\x00\xe8\x00\xe9\x00\xea\x00\xeb\x00\xec\x00\xed\x00\xee\x00\xef\x00\xf0\x00\xf1\x00\xf2\x00\xf3\x00\xf4\x00\xf5\x00\xf6\x00\xf7\x00\xf8\x00\xf9\x00\xfa\x00\xfb\x00\xfc\x00\xfd\x00\xfe\x00\xff\x00\x00\x00\x01\x00\x02\x00\x03\x00\x04\x00\x05\x00\x06\x00\x07\x00\x08\x00\x09\x00\x0a\x00\x0b\x00\x0c\x00\x0d\x00\x0e\x00\x0f\x00\x10\x00\x11\x00\x12\x00\x13\x00\x14\x00\x15\x00\x16\x00\x17\x00\x18\x00\x19\x00\x1a\x00\x1b\x00\x1c\x00\x1d\x00\x1e\x00\x1f\x00\x20\x00\x21\x00\x22\x00\x23\x00\x24\x00\x25\x00\x26\x00\x27\x00\x28\x00\x29\x00\x2a\x00\x2b\x00\x2c\x00\x2d\x00\x2e\x00\x2f\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\x3a\x00\x3b\x00\x3c\x00\x3d\x00\x3e\x00\x3f\x00\x40\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\x5b\x00\x5c\x00\x5d\x00\x5e\x00\x5f\x00\x60\x00\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\x7b\x00\x7c\x00\x7d\x00\x7e\x00\x7f\x00\x8f\x00\x90\x00\x91\x00\x92\x00\x93\x00\x94\x00\x95\x00\x96\x00\x97\x00\x98\x00\x99\x00\x9a\x00\x9b\x00\x9c\x00\x9d\x00\x9e\x00\x9f\x00\xa0\x00\xa1\x00\xa2\x00\xa3\x00\xa4\x00\xa5\x00\xa6\x00\xa7\x00\xa8\x00\xa9\x00\xaa\x00\xab\x00\xac\x00\xad\x00\xae\x00\xaf\x00\xb0\x00\xb1\x00\xb2\x00\xb3\x00\xb4\x00\xb5\x00\xb6\x00\xb7\x00\xb8\x00\xb9\x00\xba\x00\xbb\x00\xbc\x00\xbd\x00\xbe\x00\xbf\x00\xc0\x00\xc1\x00\xc2\x00\xc3\x00\xc4\x00\xc5\x00\xc6\x00\xc7\x00\xc8\x00\xc9\x00\xca\x00\xcb\x00\xcc\x00\xcd\x00\xce\x00\xcf\x00\xd0\x00\xd1\x00\xd2\x00\xd3\x00\xd4\x00\xd5\x00\xd6\x00\xd7\x00\xd8\x00\xd9\x00\xda\x00\xdb\x00\xdc\x00\xdd\x00\xde\x00\xdf\x00\xe0\x00\xe1\x00\xe2\x00\xe3\x00\xe4\x00\xe5\x00\xe6\x00\xe7\x00\xe8\x00\xe9\x00\xea\x00\xeb\x00\xec\x00\xed\x00\xee\x00\xef\x00\xf0\x00\xf1\x00\xf2\x00\xf3\x00\xf4\x00\xf5\x00\xf6\x00\xf7\x00\xf8\x00\xf9\x00\xfa\x00\xfb\x00\xfc\x00\xfd\x00\xfe\x00\xff\x00\x00\x00\x01\x00\x02\x00\x03\x00\x04\x00\x05\x00\x06\x00\x07\x00\x08\x00\x09\x00\x0a\x00\x0b\x00\x0c\x00\x0d\x00\x0e\x00\x0f\x00\x10\x00\x11\x00\x12\x00\x13\x00\x14\x00\x15\x00\x16\x00\x17\x00\x18\x00\x19\x00\x1a\x00\x1b\x00\x1c\x00\x1d\x00\x1e\x00\x1f\x00\x20\x00\x21\x00\x22\x00\x23\x00\x24\x00\x25\x00\x26\x00\x27\x00\x28\x00\x29\x00\x2a\x00\x2b\x00\x2c\x00\x2d\x00\x2e\x00\x2f\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\x3a\x00\x3b\x00\x3c\x00\x3d\x00\x3e\x00\x3f\x00\x40\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\x5b\x00\x5c\x00\x5d\x00\x5e\x00\x5f\x00\x60\x00\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\x7b\x00\x7c\x00\x7d\x00\x7e\x00\x7f\x00\xc0\x00\xc1\x00\xc2\x00\xc3\x00\xc4\x00\xc5\x00\xc6\x00\xc7\x00\xc8\x00\xc9\x00\xca\x00\xcb\x00\xcc\x00\xcd\x00\xce\x00\xcf\x00\xd0\x00\xd1\x00\xd2\x00\xd3\x00\xd4\x00\xd5\x00\xd6\x00\xd7\x00\xd8\x00\xd9\x00\xda\x00\xdb\x00\xdc\x00\xdd\x00\xde\x00\xdf\x00\xe0\x00\xe1\x00\xe2\x00\xe3\x00\xe4\x00\xe5\x00\xe6\x00\xe7\x00\xe8\x00\xe9\x00\xea\x00\xeb\x00\xec\x00\xed\x00\xee\x00\xef\x00\xf0\x00\xf1\x00\xf2\x00\xf3\x00\xf4\x00\xf5\x00\xf6\x00\xf7\x00\xf8\x00\xf9\x00\xfa\x00\xfb\x00\xfc\x00\xfd\x00\xfe\x00\xff\x00\x0a\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x80\x00\x81\x00\x82\x00\x83\x00\x84\x00\x85\x00\x86\x00\x87\x00\x88\x00\x89\x00\x8a\x00\x8b\x00\x8c\x00\x8d\x00\x8e\x00\x8f\x00\x90\x00\x91\x00\x92\x00\x93\x00\x94\x00\x95\x00\x96\x00\x97\x00\x98\x00\x99\x00\x9a\x00\x9b\x00\x9c\x00\x9d\x00\x9e\x00\x9f\x00\xa0\x00\xa1\x00\xa2\x00\xa3\x00\xa4\x00\xa5\x00\xa6\x00\xa7\x00\xa8\x00\xa9\x00\xaa\x00\xab\x00\xac\x00\xad\x00\xae\x00\xaf\x00\xb0\x00\xb1\x00\xb2\x00\xb3\x00\xb4\x00\xb5\x00\xb6\x00\xb7\x00\xb8\x00\xb9\x00\xba\x00\xbb\x00\xbc\x00\xbd\x00\xbe\x00\xbf\x00\xc0\x00\xc1\x00\xc2\x00\xc3\x00\xc4\x00\xc5\x00\xc6\x00\xc7\x00\xc8\x00\xc9\x00\xca\x00\xcb\x00\xcc\x00\xcd\x00\xce\x00\xcf\x00\xd0\x00\xd1\x00\xd2\x00\xd3\x00\xd4\x00\xd5\x00\xd6\x00\xd7\x00\xd8\x00\xd9\x00\xda\x00\xdb\x00\xdc\x00\xdd\x00\xde\x00\xdf\x00\xe0\x00\xe1\x00\xe2\x00\xe3\x00\xe4\x00\xe5\x00\xe6\x00\xe7\x00\xe8\x00\xe9\x00\xea\x00\xeb\x00\xec\x00\xed\x00\xee\x00\xef\x00\xf0\x00\xf1\x00\xf2\x00\xf3\x00\xf4\x00\xf5\x00\xf6\x00\xf7\x00\xf8\x00\xf9\x00\xfa\x00\xfb\x00\xfc\x00\xfd\x00\xfe\x00\xff\x00\x2d\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x80\x00\x81\x00\x82\x00\x83\x00\x84\x00\x85\x00\x86\x00\x87\x00\x88\x00\x89\x00\x8a\x00\x8b\x00\x8c\x00\x8d\x00\x8e\x00\x8f\x00\x90\x00\x91\x00\x92\x00\x93\x00\x94\x00\x95\x00\x96\x00\x97\x00\x98\x00\x99\x00\x9a\x00\x9b\x00\x9c\x00\x9d\x00\x9e\x00\x9f\x00\xa0\x00\xa1\x00\xa2\x00\xa3\x00\xa4\x00\xa5\x00\xa6\x00\xa7\x00\xa8\x00\xa9\x00\xaa\x00\xab\x00\xac\x00\xad\x00\xae\x00\xaf\x00\xb0\x00\xb1\x00\xb2\x00\xb3\x00\xb4\x00\xb5\x00\xb6\x00\xb7\x00\xb8\x00\xb9\x00\xba\x00\xbb\x00\xbc\x00\xbd\x00\xbe\x00\xbf\x00\xc0\x00\xc1\x00\xc2\x00\xc3\x00\xc4\x00\xc5\x00\xc6\x00\xc7\x00\xc8\x00\xc9\x00\xca\x00\xcb\x00\xcc\x00\xcd\x00\xce\x00\xcf\x00\xd0\x00\xd1\x00\xd2\x00\xd3\x00\xd4\x00\xd5\x00\xd6\x00\xd7\x00\xd8\x00\xd9\x00\xda\x00\xdb\x00\xdc\x00\xdd\x00\xde\x00\xdf\x00\xe0\x00\xe1\x00\xe2\x00\xe3\x00\xe4\x00\xe5\x00\xe6\x00\xe7\x00\xe8\x00\xe9\x00\xea\x00\xeb\x00\xec\x00\xed\x00\xee\x00\xef\x00\xf0\x00\xf1\x00\xf2\x00\xf3\x00\xf4\x00\xf5\x00\xf6\x00\xf7\x00\xf8\x00\xf9\x00\xfa\x00\xfb\x00\xfc\x00\xfd\x00\xfe\x00\xff\x00\x27\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\xff\xff\xff\xff\xff\xff\xff\xff\x5f\x00\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xc3\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff"# - -alex_deflt :: AlexAddr -alex_deflt = AlexA# "\xff\xff\xff\xff\x05\x00\x05\x00\xff\xff\x05\x00\xff\xff\x05\x00\x05\x00\x0b\x00\x0b\x00\x10\x00\x10\x00\xff\xff\x11\x00\x11\x00\x11\x00\x11\x00\x05\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff"# - -alex_accept = listArray (0::Int,23) [AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccSkip,AlexAccSkip,AlexAccSkip,AlexAccSkip,AlexAcc (alex_action_3),AlexAcc (alex_action_3),AlexAcc (alex_action_4)] -{-# LINE 38 "Exp/Lex.x" #-} - - -tok f p s = f p s - -share :: String -> String -share = id - -data Tok = - TS !String !Int -- reserved words and symbols - | TL !String -- string literals - | TI !String -- integer literals - | TV !String -- identifiers - | TD !String -- double precision float literals - | TC !String -- character literals - | T_AIdent !String - - deriving (Eq,Show,Ord) - -data Token = - PT Posn Tok - | Err Posn - deriving (Eq,Show,Ord) - -tokenPos (PT (Pn _ l _) _ :_) = "line " ++ show l -tokenPos (Err (Pn _ l _) :_) = "line " ++ show l -tokenPos _ = "end of file" - -tokenPosn (PT p _) = p -tokenPosn (Err p) = p -tokenLineCol = posLineCol . tokenPosn -posLineCol (Pn _ l c) = (l,c) -mkPosToken t@(PT p _) = (posLineCol p, prToken t) - -prToken t = case t of - PT _ (TS s _) -> s - PT _ (TL s) -> s - PT _ (TI s) -> s - PT _ (TV s) -> s - PT _ (TD s) -> s - PT _ (TC s) -> s - PT _ (T_AIdent s) -> s - - -data BTree = N | B String Tok BTree BTree deriving (Show) - -eitherResIdent :: (String -> Tok) -> String -> Tok -eitherResIdent tv s = treeFind resWords - where - treeFind N = tv s - treeFind (B a t left right) | s < a = treeFind left - | s > a = treeFind right - | s == a = t - -resWords = b "data" 11 (b "=" 6 (b "->" 3 (b ")" 2 (b "(" 1 N N) N) (b ";" 5 (b ":" 4 N N) N)) (b "\\" 9 (b "U" 8 (b "PN" 7 N N) N) (b "_" 10 N N))) (b "undefined" 17 (b "let" 14 (b "in" 13 (b "import" 12 N N) N) (b "split" 16 (b "module" 15 N N) N)) (b "|" 20 (b "{" 19 (b "where" 18 N N) N) (b "}" 21 N N))) - where b s n = let bs = id s - in B bs (TS bs n) - -unescapeInitTail :: String -> String -unescapeInitTail = id . unesc . tail . id where - unesc s = case s of - '\\':c:cs | elem c ['\"', '\\', '\''] -> c : unesc cs - '\\':'n':cs -> '\n' : unesc cs - '\\':'t':cs -> '\t' : unesc cs - '"':[] -> [] - c:cs -> c : unesc cs - _ -> [] - -------------------------------------------------------------------- --- Alex wrapper code. --- A modified "posn" wrapper. -------------------------------------------------------------------- - -data Posn = Pn !Int !Int !Int - deriving (Eq, Show,Ord) - -alexStartPos :: Posn -alexStartPos = Pn 0 1 1 - -alexMove :: Posn -> Char -> Posn -alexMove (Pn a l c) '\t' = Pn (a+1) l (((c+7) `div` 8)*8+1) -alexMove (Pn a l c) '\n' = Pn (a+1) (l+1) 1 -alexMove (Pn a l c) _ = Pn (a+1) l (c+1) - -type Byte = Word8 - -type AlexInput = (Posn, -- current position, - Char, -- previous char - [Byte], -- pending bytes on the current char - String) -- current input string - -tokens :: String -> [Token] -tokens str = go (alexStartPos, '\n', [], str) - where - go :: AlexInput -> [Token] - go inp@(pos, _, _, str) = - case alexScan inp 0 of - AlexEOF -> [] - AlexError (pos, _, _, _) -> [Err pos] - AlexSkip inp' len -> go inp' - AlexToken inp' len act -> act pos (take len str) : (go inp') - -alexGetByte :: AlexInput -> Maybe (Byte,AlexInput) -alexGetByte (p, c, (b:bs), s) = Just (b, (p, c, bs, s)) -alexGetByte (p, _, [], s) = - case s of - [] -> Nothing - (c:s) -> - let p' = alexMove p c - (b:bs) = utf8Encode c - in p' `seq` Just (b, (p', c, bs, s)) - -alexInputPrevChar :: AlexInput -> Char -alexInputPrevChar (p, c, bs, s) = c - - -- | Encode a Haskell String to a list of Word8 values, in UTF8 format. -utf8Encode :: Char -> [Word8] -utf8Encode = map fromIntegral . go . ord - where - go oc - | oc <= 0x7f = [oc] - - | oc <= 0x7ff = [ 0xc0 + (oc `Data.Bits.shiftR` 6) - , 0x80 + oc Data.Bits..&. 0x3f - ] - - | oc <= 0xffff = [ 0xe0 + (oc `Data.Bits.shiftR` 12) - , 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f) - , 0x80 + oc Data.Bits..&. 0x3f - ] - | otherwise = [ 0xf0 + (oc `Data.Bits.shiftR` 18) - , 0x80 + ((oc `Data.Bits.shiftR` 12) Data.Bits..&. 0x3f) - , 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f) - , 0x80 + oc Data.Bits..&. 0x3f - ] - -alex_action_3 = tok (\p s -> PT p (eitherResIdent (TV . share) s)) -alex_action_4 = tok (\p s -> PT p (eitherResIdent (T_AIdent . share) s)) -alex_action_5 = tok (\p s -> PT p (eitherResIdent (TV . share) s)) -{-# LINE 1 "templates/GenericTemplate.hs" #-} -{-# LINE 1 "templates/GenericTemplate.hs" #-} -{-# LINE 1 "" #-} -{-# LINE 1 "templates/GenericTemplate.hs" #-} --- ----------------------------------------------------------------------------- --- ALEX TEMPLATE --- --- This code is in the PUBLIC DOMAIN; you may copy it freely and use --- it for any purpose whatsoever. - --- ----------------------------------------------------------------------------- --- INTERNALS and main scanner engine - -{-# LINE 35 "templates/GenericTemplate.hs" #-} - -{-# LINE 45 "templates/GenericTemplate.hs" #-} - - -data AlexAddr = AlexA# Addr# - -#if __GLASGOW_HASKELL__ < 503 -uncheckedShiftL# = shiftL# -#endif - -{-# INLINE alexIndexInt16OffAddr #-} -alexIndexInt16OffAddr (AlexA# arr) off = -#ifdef WORDS_BIGENDIAN - narrow16Int# i - where - i = word2Int# ((high `uncheckedShiftL#` 8#) `or#` low) - high = int2Word# (ord# (indexCharOffAddr# arr (off' +# 1#))) - low = int2Word# (ord# (indexCharOffAddr# arr off')) - off' = off *# 2# -#else - indexInt16OffAddr# arr off -#endif - - - - - -{-# INLINE alexIndexInt32OffAddr #-} -alexIndexInt32OffAddr (AlexA# arr) off = -#ifdef WORDS_BIGENDIAN - narrow32Int# i - where - i = word2Int# ((b3 `uncheckedShiftL#` 24#) `or#` - (b2 `uncheckedShiftL#` 16#) `or#` - (b1 `uncheckedShiftL#` 8#) `or#` b0) - b3 = int2Word# (ord# (indexCharOffAddr# arr (off' +# 3#))) - b2 = int2Word# (ord# (indexCharOffAddr# arr (off' +# 2#))) - b1 = int2Word# (ord# (indexCharOffAddr# arr (off' +# 1#))) - b0 = int2Word# (ord# (indexCharOffAddr# arr off')) - off' = off *# 4# -#else - indexInt32OffAddr# arr off -#endif - - - - - -#if __GLASGOW_HASKELL__ < 503 -quickIndex arr i = arr ! i -#else --- GHC >= 503, unsafeAt is available from Data.Array.Base. -quickIndex = unsafeAt -#endif - - - - --- ----------------------------------------------------------------------------- --- Main lexing routines - -data AlexReturn a - = AlexEOF - | AlexError !AlexInput - | AlexSkip !AlexInput !Int - | AlexToken !AlexInput !Int a - --- alexScan :: AlexInput -> StartCode -> AlexReturn a -alexScan input (I# (sc)) - = alexScanUser undefined input (I# (sc)) - -alexScanUser user input (I# (sc)) - = case alex_scan_tkn user input 0# input sc AlexNone of - (AlexNone, input') -> - case alexGetByte input of - Nothing -> - - - - AlexEOF - Just _ -> - - - - AlexError input' - - (AlexLastSkip input'' len, _) -> - - - - AlexSkip input'' len - - (AlexLastAcc k input''' len, _) -> - - - - AlexToken input''' len k - - --- Push the input through the DFA, remembering the most recent accepting --- state it encountered. - -alex_scan_tkn user orig_input len input s last_acc = - input `seq` -- strict in the input - let - new_acc = (check_accs (alex_accept `quickIndex` (I# (s)))) - in - new_acc `seq` - case alexGetByte input of - Nothing -> (new_acc, input) - Just (c, new_input) -> - - - - case fromIntegral c of { (I# (ord_c)) -> - let - base = alexIndexInt32OffAddr alex_base s - offset = (base +# ord_c) - check = alexIndexInt16OffAddr alex_check offset - - new_s = if (offset >=# 0#) && (check ==# ord_c) - then alexIndexInt16OffAddr alex_table offset - else alexIndexInt16OffAddr alex_deflt s - in - case new_s of - -1# -> (new_acc, input) - -- on an error, we want to keep the input *before* the - -- character that failed, not after. - _ -> alex_scan_tkn user orig_input (if c < 0x80 || c >= 0xC0 then (len +# 1#) else len) - -- note that the length is increased ONLY if this is the 1st byte in a char encoding) - new_input new_s new_acc - } - where - check_accs (AlexAccNone) = last_acc - check_accs (AlexAcc a ) = AlexLastAcc a input (I# (len)) - check_accs (AlexAccSkip) = AlexLastSkip input (I# (len)) -{-# LINE 191 "templates/GenericTemplate.hs" #-} - -data AlexLastAcc a - = AlexNone - | AlexLastAcc a !AlexInput !Int - | AlexLastSkip !AlexInput !Int - -instance Functor AlexLastAcc where - fmap f AlexNone = AlexNone - fmap f (AlexLastAcc x y z) = AlexLastAcc (f x) y z - fmap f (AlexLastSkip x y) = AlexLastSkip x y - -data AlexAcc a user - = AlexAccNone - | AlexAcc a - | AlexAccSkip -{-# LINE 235 "templates/GenericTemplate.hs" #-} - --- used by wrappers -iUnbox (I# (i)) = i diff --git a/dist/build/cubical/cubical-tmp/Exp/Par.hs b/dist/build/cubical/cubical-tmp/Exp/Par.hs deleted file mode 100644 --- a/dist/build/cubical/cubical-tmp/Exp/Par.hs +++ /dev/null @@ -1,985 +0,0 @@ -{-# OPTIONS_GHC -w #-} -{-# OPTIONS -fglasgow-exts -cpp #-} -{-# OPTIONS_GHC -fno-warn-incomplete-patterns -fno-warn-overlapping-patterns #-} -module Exp.Par where -import Exp.Abs -import Exp.Lex -import Exp.ErrM -import qualified Data.Array as Happy_Data_Array -import qualified GHC.Exts as Happy_GHC_Exts - --- parser produced by Happy Version 1.18.8 - -newtype HappyAbsSyn = HappyAbsSyn HappyAny -#if __GLASGOW_HASKELL__ >= 607 -type HappyAny = Happy_GHC_Exts.Any -#else -type HappyAny = forall a . a -#endif -happyIn5 :: (AIdent) -> (HappyAbsSyn ) -happyIn5 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyIn5 #-} -happyOut5 :: (HappyAbsSyn ) -> (AIdent) -happyOut5 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyOut5 #-} -happyIn6 :: (Module) -> (HappyAbsSyn ) -happyIn6 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyIn6 #-} -happyOut6 :: (HappyAbsSyn ) -> (Module) -happyOut6 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyOut6 #-} -happyIn7 :: (Imp) -> (HappyAbsSyn ) -happyIn7 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyIn7 #-} -happyOut7 :: (HappyAbsSyn ) -> (Imp) -happyOut7 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyOut7 #-} -happyIn8 :: ([Imp]) -> (HappyAbsSyn ) -happyIn8 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyIn8 #-} -happyOut8 :: (HappyAbsSyn ) -> ([Imp]) -happyOut8 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyOut8 #-} -happyIn9 :: (Def) -> (HappyAbsSyn ) -happyIn9 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyIn9 #-} -happyOut9 :: (HappyAbsSyn ) -> (Def) -happyOut9 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyOut9 #-} -happyIn10 :: ([Def]) -> (HappyAbsSyn ) -happyIn10 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyIn10 #-} -happyOut10 :: (HappyAbsSyn ) -> ([Def]) -happyOut10 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyOut10 #-} -happyIn11 :: (ExpWhere) -> (HappyAbsSyn ) -happyIn11 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyIn11 #-} -happyOut11 :: (HappyAbsSyn ) -> (ExpWhere) -happyOut11 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyOut11 #-} -happyIn12 :: (Exp) -> (HappyAbsSyn ) -happyIn12 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyIn12 #-} -happyOut12 :: (HappyAbsSyn ) -> (Exp) -happyOut12 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyOut12 #-} -happyIn13 :: (Exp) -> (HappyAbsSyn ) -happyIn13 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyIn13 #-} -happyOut13 :: (HappyAbsSyn ) -> (Exp) -happyOut13 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyOut13 #-} -happyIn14 :: (Exp) -> (HappyAbsSyn ) -happyIn14 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyIn14 #-} -happyOut14 :: (HappyAbsSyn ) -> (Exp) -happyOut14 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyOut14 #-} -happyIn15 :: (Exp) -> (HappyAbsSyn ) -happyIn15 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyIn15 #-} -happyOut15 :: (HappyAbsSyn ) -> (Exp) -happyOut15 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyOut15 #-} -happyIn16 :: (Binder) -> (HappyAbsSyn ) -happyIn16 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyIn16 #-} -happyOut16 :: (HappyAbsSyn ) -> (Binder) -happyOut16 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyOut16 #-} -happyIn17 :: ([Binder]) -> (HappyAbsSyn ) -happyIn17 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyIn17 #-} -happyOut17 :: (HappyAbsSyn ) -> ([Binder]) -happyOut17 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyOut17 #-} -happyIn18 :: (Arg) -> (HappyAbsSyn ) -happyIn18 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyIn18 #-} -happyOut18 :: (HappyAbsSyn ) -> (Arg) -happyOut18 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyOut18 #-} -happyIn19 :: ([Arg]) -> (HappyAbsSyn ) -happyIn19 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyIn19 #-} -happyOut19 :: (HappyAbsSyn ) -> ([Arg]) -happyOut19 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyOut19 #-} -happyIn20 :: (Branch) -> (HappyAbsSyn ) -happyIn20 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyIn20 #-} -happyOut20 :: (HappyAbsSyn ) -> (Branch) -happyOut20 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyOut20 #-} -happyIn21 :: ([Branch]) -> (HappyAbsSyn ) -happyIn21 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyIn21 #-} -happyOut21 :: (HappyAbsSyn ) -> ([Branch]) -happyOut21 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyOut21 #-} -happyIn22 :: (Sum) -> (HappyAbsSyn ) -happyIn22 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyIn22 #-} -happyOut22 :: (HappyAbsSyn ) -> (Sum) -happyOut22 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyOut22 #-} -happyIn23 :: ([Sum]) -> (HappyAbsSyn ) -happyIn23 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyIn23 #-} -happyOut23 :: (HappyAbsSyn ) -> ([Sum]) -happyOut23 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyOut23 #-} -happyIn24 :: (VDecl) -> (HappyAbsSyn ) -happyIn24 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyIn24 #-} -happyOut24 :: (HappyAbsSyn ) -> (VDecl) -happyOut24 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyOut24 #-} -happyIn25 :: ([VDecl]) -> (HappyAbsSyn ) -happyIn25 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyIn25 #-} -happyOut25 :: (HappyAbsSyn ) -> ([VDecl]) -happyOut25 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyOut25 #-} -happyIn26 :: (PiDecl) -> (HappyAbsSyn ) -happyIn26 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyIn26 #-} -happyOut26 :: (HappyAbsSyn ) -> (PiDecl) -happyOut26 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyOut26 #-} -happyIn27 :: ([PiDecl]) -> (HappyAbsSyn ) -happyIn27 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyIn27 #-} -happyOut27 :: (HappyAbsSyn ) -> ([PiDecl]) -happyOut27 x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyOut27 #-} -happyInTok :: (Token) -> (HappyAbsSyn ) -happyInTok x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyInTok #-} -happyOutTok :: (HappyAbsSyn ) -> (Token) -happyOutTok x = Happy_GHC_Exts.unsafeCoerce# x -{-# INLINE happyOutTok #-} - - -happyActOffsets :: HappyAddr -happyActOffsets = HappyA# "\xd7\x00\xca\x00\xce\x00\x00\x00\x00\x00\xc9\x00\x00\x00\xdb\x00\x00\x00\x00\x00\xde\x00\xcd\x00\xca\x00\x00\x00\x00\x00\x4b\x00\x00\x00\xc4\x00\xbb\x00\x00\x00\xb7\x00\xc3\x00\xba\x00\xaf\x00\x18\x00\x4b\x00\xc1\x00\x00\x00\x41\x00\x9c\x00\x00\x00\xca\x00\x00\x00\xca\x00\x9c\x00\x00\x00\xbd\x00\xb9\x00\x00\x00\x00\x00\xca\x00\xca\x00\x00\x00\xb8\x00\xae\x00\x8c\x00\x98\x00\x00\x00\xa0\x00\x89\x00\x8d\x00\x8a\x00\x00\x00\x7d\x00\x0a\x00\x00\x00\x84\x00\x18\x00\x3a\x00\xca\x00\x00\x00\x8b\x00\x00\x00\x00\x00\x00\x00\xca\x00\x00\x00\xca\x00\x37\x00\xca\x00\x00\x00\x81\x00\x18\x00\x78\x00\x00\x00\x61\x00\x77\x00\x00\x00\x6f\x00\x68\x00\x00\x00\x00\x00\x00\x00\x5f\x00\x00\x00\x6a\x00\x00\x00\x00\x00\x18\x00\x5b\x00\x65\x00\x00\x00\x4b\x00\x00\x00\x59\x00\x00\x00\x60\x00\xca\x00\x6b\x00\x00\x00\x00\x00"# - -happyGotoOffsets :: HappyAddr -happyGotoOffsets = HappyA# "\x64\x00\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x53\x00\x00\x00\x00\x00\xed\xff\x00\x00\x92\x00\x00\x00\x00\x00\xdd\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x63\x00\x00\x00\x26\x00\xb0\x00\xb6\x00\x00\x00\x00\x00\x00\x00\xc0\x00\x00\x00\x82\x00\x00\x00\x72\x00\xb1\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x62\x00\x52\x00\x00\x00\x48\x00\x00\x00\x00\x00\x54\x00\x40\x00\x00\x00\x00\x00\x00\x00\x31\x00\x00\x00\x21\x00\x51\x00\x38\x00\x00\x00\x90\x00\x51\x00\x42\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x12\x00\x00\x00\x32\x00\x51\x00\x01\x00\x00\x00\x00\x00\x80\x00\x3e\x00\x00\x00\x00\x00\x03\x00\x00\x00\x00\x00\x13\x00\x00\x00\x00\x00\x19\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x70\x00\x0c\x00\x02\x00\x00\x00\x04\x00\x00\x00\x00\x00\x00\x00\x00\x00\x22\x00\x00\x00\x00\x00\x00\x00"# - -happyDefActions :: HappyAddr -happyDefActions = HappyA# "\x00\x00\x00\x00\x00\x00\xfd\xff\xde\xff\x00\x00\xec\xff\xe9\xff\xe7\xff\xe6\xff\xce\xff\x00\x00\x00\x00\xe3\xff\xe5\xff\x00\x00\xdd\xff\x00\x00\x00\x00\xe4\xff\x00\x00\x00\x00\x00\x00\xd9\xff\xf4\xff\xe0\xff\x00\x00\xe1\xff\x00\x00\x00\x00\xcd\xff\x00\x00\xe8\xff\x00\x00\x00\x00\xeb\xff\x00\x00\x00\x00\xea\xff\xe2\xff\x00\x00\x00\x00\xdf\xff\xdc\xff\xf3\xff\x00\x00\x00\x00\xdc\xff\xd8\xff\x00\x00\x00\x00\xfa\xff\xed\xff\xd9\xff\x00\x00\xdc\xff\x00\x00\xf4\xff\x00\x00\x00\x00\xee\xff\x00\x00\xcf\xff\xf6\xff\xdb\xff\x00\x00\xf2\xff\x00\x00\x00\x00\x00\x00\xd7\xff\xf9\xff\xf4\xff\x00\x00\xfb\xff\x00\x00\xfa\xff\xda\xff\xf0\xff\xd5\xff\xef\xff\xf7\xff\xd1\xff\xd4\xff\xf5\xff\x00\x00\xf8\xff\xfc\xff\xf4\xff\xd5\xff\xd6\xff\xd0\xff\x00\x00\xd3\xff\x00\x00\xf1\xff\x00\x00\x00\x00\x00\x00\xd2\xff"# - -happyCheck :: HappyAddr -happyCheck = HappyA# "\xff\xff\x00\x00\x15\x00\x16\x00\x00\x00\x02\x00\x03\x00\x06\x00\x07\x00\x08\x00\x09\x00\x0a\x00\x00\x00\x03\x00\x0d\x00\x0b\x00\x0c\x00\x0d\x00\x00\x00\x00\x00\x0a\x00\x13\x00\x15\x00\x16\x00\x06\x00\x07\x00\x08\x00\x09\x00\x0a\x00\x11\x00\x12\x00\x0d\x00\x16\x00\x00\x00\x00\x00\x0b\x00\x11\x00\x12\x00\x00\x00\x15\x00\x16\x00\x07\x00\x08\x00\x09\x00\x0a\x00\x14\x00\x16\x00\x0d\x00\x0f\x00\x10\x00\x00\x00\x02\x00\x03\x00\x0f\x00\x10\x00\x15\x00\x16\x00\x07\x00\x08\x00\x09\x00\x0a\x00\x06\x00\x00\x00\x0d\x00\x06\x00\x0a\x00\x00\x00\x02\x00\x0a\x00\x04\x00\x0e\x00\x15\x00\x16\x00\x07\x00\x08\x00\x09\x00\x0a\x00\x16\x00\x0e\x00\x0d\x00\x16\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0a\x00\x0e\x00\x15\x00\x16\x00\x07\x00\x08\x00\x09\x00\x0a\x00\x0a\x00\x0d\x00\x0d\x00\x0d\x00\x16\x00\x00\x00\x00\x00\x04\x00\x01\x00\x01\x00\x15\x00\x16\x00\x07\x00\x08\x00\x09\x00\x0a\x00\x02\x00\x15\x00\x0d\x00\x00\x00\x16\x00\x00\x00\x14\x00\x04\x00\x05\x00\x15\x00\x15\x00\x16\x00\x07\x00\x08\x00\x09\x00\x0a\x00\x13\x00\x16\x00\x0d\x00\x00\x00\x12\x00\x00\x00\x0c\x00\x04\x00\x05\x00\x05\x00\x15\x00\x16\x00\x07\x00\x08\x00\x09\x00\x0a\x00\x02\x00\x16\x00\x0d\x00\x00\x00\x0d\x00\x00\x00\x16\x00\x04\x00\x05\x00\x0c\x00\x15\x00\x16\x00\x07\x00\x08\x00\x09\x00\x0a\x00\x01\x00\x15\x00\x0d\x00\x13\x00\x15\x00\x00\x00\x07\x00\x08\x00\x05\x00\x0a\x00\x15\x00\x16\x00\x07\x00\x08\x00\x09\x00\x0a\x00\x11\x00\x16\x00\x0d\x00\x00\x00\x00\x00\x16\x00\x05\x00\x04\x00\x05\x00\x00\x00\x15\x00\x16\x00\x08\x00\x09\x00\x0a\x00\x04\x00\x04\x00\x0d\x00\x02\x00\x00\x00\x0b\x00\x0c\x00\x0d\x00\x03\x00\x16\x00\x15\x00\x16\x00\x08\x00\x09\x00\x0a\x00\x01\x00\x12\x00\x0d\x00\x13\x00\x18\x00\x03\x00\x07\x00\x08\x00\x09\x00\x0a\x00\x15\x00\x16\x00\x13\x00\x0e\x00\x16\x00\x10\x00\x11\x00\x01\x00\x00\x00\x03\x00\x01\x00\x16\x00\x18\x00\x07\x00\x08\x00\x16\x00\x0a\x00\x0f\x00\xff\xff\x0b\x00\x0c\x00\x0d\x00\xff\xff\x11\x00\xff\xff\xff\xff\xff\xff\xff\xff\x16\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff"# - -happyTable :: HappyAddr -happyTable = HappyA# "\x00\x00\x04\x00\x0a\x00\x1e\x00\x04\x00\x47\x00\x56\x00\x4d\x00\x4e\x00\x06\x00\x07\x00\x08\x00\x52\x00\x46\x00\x09\x00\x19\x00\x60\x00\x1b\x00\x04\x00\x52\x00\x11\x00\x5b\x00\x0a\x00\x0b\x00\x51\x00\x4e\x00\x06\x00\x07\x00\x08\x00\x53\x00\x5d\x00\x09\x00\x04\x00\x2f\x00\x04\x00\x2f\x00\x53\x00\x54\x00\x2f\x00\x0a\x00\x0b\x00\x62\x00\x06\x00\x07\x00\x08\x00\x5a\x00\x04\x00\x09\x00\x30\x00\x46\x00\x04\x00\x47\x00\x48\x00\x30\x00\x31\x00\x0a\x00\x0b\x00\x50\x00\x06\x00\x07\x00\x08\x00\x50\x00\x4a\x00\x09\x00\x42\x00\x11\x00\x04\x00\x28\x00\x11\x00\x29\x00\x44\x00\x0a\x00\x0b\x00\x3f\x00\x06\x00\x07\x00\x08\x00\x04\x00\x36\x00\x09\x00\x04\x00\x04\x00\x04\x00\x04\x00\x37\x00\x11\x00\x3a\x00\x0a\x00\x0b\x00\x3c\x00\x06\x00\x07\x00\x08\x00\x20\x00\x40\x00\x09\x00\x09\x00\x04\x00\x04\x00\x16\x00\x62\x00\x14\x00\x5d\x00\x0a\x00\x0b\x00\x3d\x00\x06\x00\x07\x00\x08\x00\x64\x00\x60\x00\x09\x00\x2b\x00\x04\x00\x04\x00\x5a\x00\x2c\x00\x5e\x00\x58\x00\x0a\x00\x0b\x00\x24\x00\x06\x00\x07\x00\x08\x00\x59\x00\x04\x00\x09\x00\x2b\x00\x56\x00\x04\x00\x4a\x00\x2c\x00\x4b\x00\x4d\x00\x0a\x00\x0b\x00\x25\x00\x06\x00\x07\x00\x08\x00\x3f\x00\x04\x00\x09\x00\x2b\x00\x44\x00\x04\x00\x04\x00\x2c\x00\x42\x00\x4a\x00\x0a\x00\x0b\x00\x1c\x00\x06\x00\x07\x00\x08\x00\x0d\x00\x35\x00\x09\x00\x34\x00\x39\x00\x04\x00\x0e\x00\x0f\x00\x36\x00\x11\x00\x0a\x00\x0b\x00\x05\x00\x06\x00\x07\x00\x08\x00\x14\x00\x04\x00\x09\x00\x2b\x00\x04\x00\x04\x00\x3a\x00\x2c\x00\x2d\x00\x04\x00\x0a\x00\x0b\x00\x23\x00\x07\x00\x08\x00\x3c\x00\x29\x00\x09\x00\x28\x00\x04\x00\x19\x00\x2a\x00\x1b\x00\x2a\x00\x04\x00\x0a\x00\x0b\x00\x26\x00\x07\x00\x08\x00\x0d\x00\x33\x00\x09\x00\x18\x00\xff\xff\x1e\x00\x0e\x00\x0f\x00\x10\x00\x11\x00\x0a\x00\x0b\x00\x19\x00\x12\x00\x04\x00\x13\x00\x14\x00\x22\x00\x04\x00\x23\x00\x20\x00\x04\x00\xff\xff\x0e\x00\x0f\x00\x04\x00\x11\x00\x16\x00\x00\x00\x19\x00\x1a\x00\x1b\x00\x00\x00\x14\x00\x00\x00\x00\x00\x00\x00\x00\x00\x04\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"# - -happyReduceArr = Happy_Data_Array.array (2, 50) [ - (2 , happyReduce_2), - (3 , happyReduce_3), - (4 , happyReduce_4), - (5 , happyReduce_5), - (6 , happyReduce_6), - (7 , happyReduce_7), - (8 , happyReduce_8), - (9 , happyReduce_9), - (10 , happyReduce_10), - (11 , happyReduce_11), - (12 , happyReduce_12), - (13 , happyReduce_13), - (14 , happyReduce_14), - (15 , happyReduce_15), - (16 , happyReduce_16), - (17 , happyReduce_17), - (18 , happyReduce_18), - (19 , happyReduce_19), - (20 , happyReduce_20), - (21 , happyReduce_21), - (22 , happyReduce_22), - (23 , happyReduce_23), - (24 , happyReduce_24), - (25 , happyReduce_25), - (26 , happyReduce_26), - (27 , happyReduce_27), - (28 , happyReduce_28), - (29 , happyReduce_29), - (30 , happyReduce_30), - (31 , happyReduce_31), - (32 , happyReduce_32), - (33 , happyReduce_33), - (34 , happyReduce_34), - (35 , happyReduce_35), - (36 , happyReduce_36), - (37 , happyReduce_37), - (38 , happyReduce_38), - (39 , happyReduce_39), - (40 , happyReduce_40), - (41 , happyReduce_41), - (42 , happyReduce_42), - (43 , happyReduce_43), - (44 , happyReduce_44), - (45 , happyReduce_45), - (46 , happyReduce_46), - (47 , happyReduce_47), - (48 , happyReduce_48), - (49 , happyReduce_49), - (50 , happyReduce_50) - ] - -happy_n_terms = 25 :: Int -happy_n_nonterms = 23 :: Int - -happyReduce_2 = happySpecReduce_1 0# happyReduction_2 -happyReduction_2 happy_x_1 - = case happyOutTok happy_x_1 of { happy_var_1 -> - happyIn5 - (AIdent (mkPosToken happy_var_1) - )} - -happyReduce_3 = happyReduce 7# 1# happyReduction_3 -happyReduction_3 (happy_x_7 `HappyStk` - happy_x_6 `HappyStk` - happy_x_5 `HappyStk` - happy_x_4 `HappyStk` - happy_x_3 `HappyStk` - happy_x_2 `HappyStk` - happy_x_1 `HappyStk` - happyRest) - = case happyOut5 happy_x_2 of { happy_var_2 -> - case happyOut8 happy_x_5 of { happy_var_5 -> - case happyOut10 happy_x_6 of { happy_var_6 -> - happyIn6 - (Module happy_var_2 happy_var_5 happy_var_6 - ) `HappyStk` happyRest}}} - -happyReduce_4 = happySpecReduce_2 2# happyReduction_4 -happyReduction_4 happy_x_2 - happy_x_1 - = case happyOut5 happy_x_2 of { happy_var_2 -> - happyIn7 - (Import happy_var_2 - )} - -happyReduce_5 = happySpecReduce_0 3# happyReduction_5 -happyReduction_5 = happyIn8 - ([] - ) - -happyReduce_6 = happySpecReduce_1 3# happyReduction_6 -happyReduction_6 happy_x_1 - = case happyOut7 happy_x_1 of { happy_var_1 -> - happyIn8 - ((:[]) happy_var_1 - )} - -happyReduce_7 = happySpecReduce_3 3# happyReduction_7 -happyReduction_7 happy_x_3 - happy_x_2 - happy_x_1 - = case happyOut7 happy_x_1 of { happy_var_1 -> - case happyOut8 happy_x_3 of { happy_var_3 -> - happyIn8 - ((:) happy_var_1 happy_var_3 - )}} - -happyReduce_8 = happyReduce 4# 4# happyReduction_8 -happyReduction_8 (happy_x_4 `HappyStk` - happy_x_3 `HappyStk` - happy_x_2 `HappyStk` - happy_x_1 `HappyStk` - happyRest) - = case happyOut5 happy_x_1 of { happy_var_1 -> - case happyOut19 happy_x_2 of { happy_var_2 -> - case happyOut11 happy_x_4 of { happy_var_4 -> - happyIn9 - (Def happy_var_1 (reverse happy_var_2) happy_var_4 - ) `HappyStk` happyRest}}} - -happyReduce_9 = happySpecReduce_3 4# happyReduction_9 -happyReduction_9 happy_x_3 - happy_x_2 - happy_x_1 - = case happyOut5 happy_x_1 of { happy_var_1 -> - case happyOut12 happy_x_3 of { happy_var_3 -> - happyIn9 - (DefTDecl happy_var_1 happy_var_3 - )}} - -happyReduce_10 = happyReduce 5# 4# happyReduction_10 -happyReduction_10 (happy_x_5 `HappyStk` - happy_x_4 `HappyStk` - happy_x_3 `HappyStk` - happy_x_2 `HappyStk` - happy_x_1 `HappyStk` - happyRest) - = case happyOut5 happy_x_2 of { happy_var_2 -> - case happyOut19 happy_x_3 of { happy_var_3 -> - case happyOut23 happy_x_5 of { happy_var_5 -> - happyIn9 - (DefData happy_var_2 (reverse happy_var_3) happy_var_5 - ) `HappyStk` happyRest}}} - -happyReduce_11 = happySpecReduce_0 5# happyReduction_11 -happyReduction_11 = happyIn10 - ([] - ) - -happyReduce_12 = happySpecReduce_1 5# happyReduction_12 -happyReduction_12 happy_x_1 - = case happyOut9 happy_x_1 of { happy_var_1 -> - happyIn10 - ((:[]) happy_var_1 - )} - -happyReduce_13 = happySpecReduce_3 5# happyReduction_13 -happyReduction_13 happy_x_3 - happy_x_2 - happy_x_1 - = case happyOut9 happy_x_1 of { happy_var_1 -> - case happyOut10 happy_x_3 of { happy_var_3 -> - happyIn10 - ((:) happy_var_1 happy_var_3 - )}} - -happyReduce_14 = happyReduce 5# 6# happyReduction_14 -happyReduction_14 (happy_x_5 `HappyStk` - happy_x_4 `HappyStk` - happy_x_3 `HappyStk` - happy_x_2 `HappyStk` - happy_x_1 `HappyStk` - happyRest) - = case happyOut12 happy_x_1 of { happy_var_1 -> - case happyOut10 happy_x_4 of { happy_var_4 -> - happyIn11 - (Where happy_var_1 happy_var_4 - ) `HappyStk` happyRest}} - -happyReduce_15 = happySpecReduce_1 6# happyReduction_15 -happyReduction_15 happy_x_1 - = case happyOut12 happy_x_1 of { happy_var_1 -> - happyIn11 - (NoWhere happy_var_1 - )} - -happyReduce_16 = happyReduce 6# 7# happyReduction_16 -happyReduction_16 (happy_x_6 `HappyStk` - happy_x_5 `HappyStk` - happy_x_4 `HappyStk` - happy_x_3 `HappyStk` - happy_x_2 `HappyStk` - happy_x_1 `HappyStk` - happyRest) - = case happyOut10 happy_x_3 of { happy_var_3 -> - case happyOut12 happy_x_6 of { happy_var_6 -> - happyIn12 - (Let happy_var_3 happy_var_6 - ) `HappyStk` happyRest}} - -happyReduce_17 = happyReduce 4# 7# happyReduction_17 -happyReduction_17 (happy_x_4 `HappyStk` - happy_x_3 `HappyStk` - happy_x_2 `HappyStk` - happy_x_1 `HappyStk` - happyRest) - = case happyOut17 happy_x_2 of { happy_var_2 -> - case happyOut12 happy_x_4 of { happy_var_4 -> - happyIn12 - (Lam happy_var_2 happy_var_4 - ) `HappyStk` happyRest}} - -happyReduce_18 = happyReduce 4# 7# happyReduction_18 -happyReduction_18 (happy_x_4 `HappyStk` - happy_x_3 `HappyStk` - happy_x_2 `HappyStk` - happy_x_1 `HappyStk` - happyRest) - = case happyOut21 happy_x_3 of { happy_var_3 -> - happyIn12 - (Split happy_var_3 - ) `HappyStk` happyRest} - -happyReduce_19 = happySpecReduce_1 7# happyReduction_19 -happyReduction_19 happy_x_1 - = case happyOut13 happy_x_1 of { happy_var_1 -> - happyIn12 - (happy_var_1 - )} - -happyReduce_20 = happySpecReduce_3 8# happyReduction_20 -happyReduction_20 happy_x_3 - happy_x_2 - happy_x_1 - = case happyOut14 happy_x_1 of { happy_var_1 -> - case happyOut13 happy_x_3 of { happy_var_3 -> - happyIn13 - (Fun happy_var_1 happy_var_3 - )}} - -happyReduce_21 = happySpecReduce_3 8# happyReduction_21 -happyReduction_21 happy_x_3 - happy_x_2 - happy_x_1 - = case happyOut27 happy_x_1 of { happy_var_1 -> - case happyOut13 happy_x_3 of { happy_var_3 -> - happyIn13 - (Pi happy_var_1 happy_var_3 - )}} - -happyReduce_22 = happySpecReduce_1 8# happyReduction_22 -happyReduction_22 happy_x_1 - = case happyOut14 happy_x_1 of { happy_var_1 -> - happyIn13 - (happy_var_1 - )} - -happyReduce_23 = happySpecReduce_2 9# happyReduction_23 -happyReduction_23 happy_x_2 - happy_x_1 - = case happyOut14 happy_x_1 of { happy_var_1 -> - case happyOut15 happy_x_2 of { happy_var_2 -> - happyIn14 - (App happy_var_1 happy_var_2 - )}} - -happyReduce_24 = happySpecReduce_1 9# happyReduction_24 -happyReduction_24 happy_x_1 - = case happyOut15 happy_x_1 of { happy_var_1 -> - happyIn14 - (happy_var_1 - )} - -happyReduce_25 = happySpecReduce_1 10# happyReduction_25 -happyReduction_25 happy_x_1 - = case happyOut18 happy_x_1 of { happy_var_1 -> - happyIn15 - (Var happy_var_1 - )} - -happyReduce_26 = happySpecReduce_1 10# happyReduction_26 -happyReduction_26 happy_x_1 - = happyIn15 - (U - ) - -happyReduce_27 = happySpecReduce_1 10# happyReduction_27 -happyReduction_27 happy_x_1 - = happyIn15 - (Undef - ) - -happyReduce_28 = happySpecReduce_1 10# happyReduction_28 -happyReduction_28 happy_x_1 - = happyIn15 - (PN - ) - -happyReduce_29 = happySpecReduce_3 10# happyReduction_29 -happyReduction_29 happy_x_3 - happy_x_2 - happy_x_1 - = case happyOut12 happy_x_2 of { happy_var_2 -> - happyIn15 - (happy_var_2 - )} - -happyReduce_30 = happySpecReduce_1 11# happyReduction_30 -happyReduction_30 happy_x_1 - = case happyOut18 happy_x_1 of { happy_var_1 -> - happyIn16 - (Binder happy_var_1 - )} - -happyReduce_31 = happySpecReduce_1 12# happyReduction_31 -happyReduction_31 happy_x_1 - = case happyOut16 happy_x_1 of { happy_var_1 -> - happyIn17 - ((:[]) happy_var_1 - )} - -happyReduce_32 = happySpecReduce_2 12# happyReduction_32 -happyReduction_32 happy_x_2 - happy_x_1 - = case happyOut16 happy_x_1 of { happy_var_1 -> - case happyOut17 happy_x_2 of { happy_var_2 -> - happyIn17 - ((:) happy_var_1 happy_var_2 - )}} - -happyReduce_33 = happySpecReduce_1 13# happyReduction_33 -happyReduction_33 happy_x_1 - = case happyOut5 happy_x_1 of { happy_var_1 -> - happyIn18 - (Arg happy_var_1 - )} - -happyReduce_34 = happySpecReduce_1 13# happyReduction_34 -happyReduction_34 happy_x_1 - = happyIn18 - (NoArg - ) - -happyReduce_35 = happySpecReduce_0 14# happyReduction_35 -happyReduction_35 = happyIn19 - ([] - ) - -happyReduce_36 = happySpecReduce_2 14# happyReduction_36 -happyReduction_36 happy_x_2 - happy_x_1 - = case happyOut19 happy_x_1 of { happy_var_1 -> - case happyOut18 happy_x_2 of { happy_var_2 -> - happyIn19 - (flip (:) happy_var_1 happy_var_2 - )}} - -happyReduce_37 = happyReduce 4# 15# happyReduction_37 -happyReduction_37 (happy_x_4 `HappyStk` - happy_x_3 `HappyStk` - happy_x_2 `HappyStk` - happy_x_1 `HappyStk` - happyRest) - = case happyOut5 happy_x_1 of { happy_var_1 -> - case happyOut19 happy_x_2 of { happy_var_2 -> - case happyOut11 happy_x_4 of { happy_var_4 -> - happyIn20 - (Branch happy_var_1 (reverse happy_var_2) happy_var_4 - ) `HappyStk` happyRest}}} - -happyReduce_38 = happySpecReduce_0 16# happyReduction_38 -happyReduction_38 = happyIn21 - ([] - ) - -happyReduce_39 = happySpecReduce_1 16# happyReduction_39 -happyReduction_39 happy_x_1 - = case happyOut20 happy_x_1 of { happy_var_1 -> - happyIn21 - ((:[]) happy_var_1 - )} - -happyReduce_40 = happySpecReduce_3 16# happyReduction_40 -happyReduction_40 happy_x_3 - happy_x_2 - happy_x_1 - = case happyOut20 happy_x_1 of { happy_var_1 -> - case happyOut21 happy_x_3 of { happy_var_3 -> - happyIn21 - ((:) happy_var_1 happy_var_3 - )}} - -happyReduce_41 = happySpecReduce_2 17# happyReduction_41 -happyReduction_41 happy_x_2 - happy_x_1 - = case happyOut5 happy_x_1 of { happy_var_1 -> - case happyOut25 happy_x_2 of { happy_var_2 -> - happyIn22 - (Sum happy_var_1 (reverse happy_var_2) - )}} - -happyReduce_42 = happySpecReduce_0 18# happyReduction_42 -happyReduction_42 = happyIn23 - ([] - ) - -happyReduce_43 = happySpecReduce_1 18# happyReduction_43 -happyReduction_43 happy_x_1 - = case happyOut22 happy_x_1 of { happy_var_1 -> - happyIn23 - ((:[]) happy_var_1 - )} - -happyReduce_44 = happySpecReduce_3 18# happyReduction_44 -happyReduction_44 happy_x_3 - happy_x_2 - happy_x_1 - = case happyOut22 happy_x_1 of { happy_var_1 -> - case happyOut23 happy_x_3 of { happy_var_3 -> - happyIn23 - ((:) happy_var_1 happy_var_3 - )}} - -happyReduce_45 = happyReduce 5# 19# happyReduction_45 -happyReduction_45 (happy_x_5 `HappyStk` - happy_x_4 `HappyStk` - happy_x_3 `HappyStk` - happy_x_2 `HappyStk` - happy_x_1 `HappyStk` - happyRest) - = case happyOut17 happy_x_2 of { happy_var_2 -> - case happyOut12 happy_x_4 of { happy_var_4 -> - happyIn24 - (VDecl happy_var_2 happy_var_4 - ) `HappyStk` happyRest}} - -happyReduce_46 = happySpecReduce_0 20# happyReduction_46 -happyReduction_46 = happyIn25 - ([] - ) - -happyReduce_47 = happySpecReduce_2 20# happyReduction_47 -happyReduction_47 happy_x_2 - happy_x_1 - = case happyOut25 happy_x_1 of { happy_var_1 -> - case happyOut24 happy_x_2 of { happy_var_2 -> - happyIn25 - (flip (:) happy_var_1 happy_var_2 - )}} - -happyReduce_48 = happyReduce 5# 21# happyReduction_48 -happyReduction_48 (happy_x_5 `HappyStk` - happy_x_4 `HappyStk` - happy_x_3 `HappyStk` - happy_x_2 `HappyStk` - happy_x_1 `HappyStk` - happyRest) - = case happyOut12 happy_x_2 of { happy_var_2 -> - case happyOut12 happy_x_4 of { happy_var_4 -> - happyIn26 - (PiDecl happy_var_2 happy_var_4 - ) `HappyStk` happyRest}} - -happyReduce_49 = happySpecReduce_1 22# happyReduction_49 -happyReduction_49 happy_x_1 - = case happyOut26 happy_x_1 of { happy_var_1 -> - happyIn27 - ((:[]) happy_var_1 - )} - -happyReduce_50 = happySpecReduce_2 22# happyReduction_50 -happyReduction_50 happy_x_2 - happy_x_1 - = case happyOut26 happy_x_1 of { happy_var_1 -> - case happyOut27 happy_x_2 of { happy_var_2 -> - happyIn27 - ((:) happy_var_1 happy_var_2 - )}} - -happyNewToken action sts stk [] = - happyDoAction 24# notHappyAtAll action sts stk [] - -happyNewToken action sts stk (tk:tks) = - let cont i = happyDoAction i tk action sts stk tks in - case tk of { - PT _ (TS _ 1) -> cont 1#; - PT _ (TS _ 2) -> cont 2#; - PT _ (TS _ 3) -> cont 3#; - PT _ (TS _ 4) -> cont 4#; - PT _ (TS _ 5) -> cont 5#; - PT _ (TS _ 6) -> cont 6#; - PT _ (TS _ 7) -> cont 7#; - PT _ (TS _ 8) -> cont 8#; - PT _ (TS _ 9) -> cont 9#; - PT _ (TS _ 10) -> cont 10#; - PT _ (TS _ 11) -> cont 11#; - PT _ (TS _ 12) -> cont 12#; - PT _ (TS _ 13) -> cont 13#; - PT _ (TS _ 14) -> cont 14#; - PT _ (TS _ 15) -> cont 15#; - PT _ (TS _ 16) -> cont 16#; - PT _ (TS _ 17) -> cont 17#; - PT _ (TS _ 18) -> cont 18#; - PT _ (TS _ 19) -> cont 19#; - PT _ (TS _ 20) -> cont 20#; - PT _ (TS _ 21) -> cont 21#; - PT _ (T_AIdent _) -> cont 22#; - _ -> cont 23#; - _ -> happyError' (tk:tks) - } - -happyError_ 24# tk tks = happyError' tks -happyError_ _ tk tks = happyError' (tk:tks) - -happyThen :: () => Err a -> (a -> Err b) -> Err b -happyThen = (thenM) -happyReturn :: () => a -> Err a -happyReturn = (returnM) -happyThen1 m k tks = (thenM) m (\a -> k a tks) -happyReturn1 :: () => a -> b -> Err a -happyReturn1 = \a tks -> (returnM) a -happyError' :: () => [(Token)] -> Err a -happyError' = happyError - -pModule tks = happySomeParser where - happySomeParser = happyThen (happyParse 0# tks) (\x -> happyReturn (happyOut6 x)) - -pExp tks = happySomeParser where - happySomeParser = happyThen (happyParse 1# tks) (\x -> happyReturn (happyOut12 x)) - -happySeq = happyDontSeq - - -returnM :: a -> Err a -returnM = return - -thenM :: Err a -> (a -> Err b) -> Err b -thenM = (>>=) - -happyError :: [Token] -> Err a -happyError ts = - Bad $ "syntax error at " ++ tokenPos ts ++ - case ts of - [] -> [] - [Err _] -> " due to lexer error" - _ -> " before " ++ unwords (map (id . prToken) (take 4 ts)) - -myLexer = tokens -{-# LINE 1 "templates/GenericTemplate.hs" #-} -{-# LINE 1 "templates/GenericTemplate.hs" #-} -{-# LINE 1 "" #-} -{-# LINE 1 "" #-} -{-# LINE 1 "templates/GenericTemplate.hs" #-} --- Id: GenericTemplate.hs,v 1.26 2005/01/14 14:47:22 simonmar Exp - -{-# LINE 30 "templates/GenericTemplate.hs" #-} - - -data Happy_IntList = HappyCons Happy_GHC_Exts.Int# Happy_IntList - - - - - -{-# LINE 51 "templates/GenericTemplate.hs" #-} - -{-# LINE 61 "templates/GenericTemplate.hs" #-} - -{-# LINE 70 "templates/GenericTemplate.hs" #-} - -infixr 9 `HappyStk` -data HappyStk a = HappyStk a (HappyStk a) - ------------------------------------------------------------------------------ --- starting the parse - -happyParse start_state = happyNewToken start_state notHappyAtAll notHappyAtAll - ------------------------------------------------------------------------------ --- Accepting the parse - --- If the current token is 0#, it means we've just accepted a partial --- parse (a %partial parser). We must ignore the saved token on the top of --- the stack in this case. -happyAccept 0# tk st sts (_ `HappyStk` ans `HappyStk` _) = - happyReturn1 ans -happyAccept j tk st sts (HappyStk ans _) = - (happyTcHack j (happyTcHack st)) (happyReturn1 ans) - ------------------------------------------------------------------------------ --- Arrays only: do the next action - - - -happyDoAction i tk st - = {- nothing -} - - - case action of - 0# -> {- nothing -} - happyFail i tk st - -1# -> {- nothing -} - happyAccept i tk st - n | (n Happy_GHC_Exts.<# (0# :: Happy_GHC_Exts.Int#)) -> {- nothing -} - - (happyReduceArr Happy_Data_Array.! rule) i tk st - where rule = (Happy_GHC_Exts.I# ((Happy_GHC_Exts.negateInt# ((n Happy_GHC_Exts.+# (1# :: Happy_GHC_Exts.Int#)))))) - n -> {- nothing -} - - - happyShift new_state i tk st - where (new_state) = (n Happy_GHC_Exts.-# (1# :: Happy_GHC_Exts.Int#)) - where (off) = indexShortOffAddr happyActOffsets st - (off_i) = (off Happy_GHC_Exts.+# i) - check = if (off_i Happy_GHC_Exts.>=# (0# :: Happy_GHC_Exts.Int#)) - then (indexShortOffAddr happyCheck off_i Happy_GHC_Exts.==# i) - else False - (action) - | check = indexShortOffAddr happyTable off_i - | otherwise = indexShortOffAddr happyDefActions st - -{-# LINE 130 "templates/GenericTemplate.hs" #-} - - -indexShortOffAddr (HappyA# arr) off = - Happy_GHC_Exts.narrow16Int# i - where - i = Happy_GHC_Exts.word2Int# (Happy_GHC_Exts.or# (Happy_GHC_Exts.uncheckedShiftL# high 8#) low) - high = Happy_GHC_Exts.int2Word# (Happy_GHC_Exts.ord# (Happy_GHC_Exts.indexCharOffAddr# arr (off' Happy_GHC_Exts.+# 1#))) - low = Happy_GHC_Exts.int2Word# (Happy_GHC_Exts.ord# (Happy_GHC_Exts.indexCharOffAddr# arr off')) - off' = off Happy_GHC_Exts.*# 2# - - - - - -data HappyAddr = HappyA# Happy_GHC_Exts.Addr# - - - - ------------------------------------------------------------------------------ --- HappyState data type (not arrays) - -{-# LINE 163 "templates/GenericTemplate.hs" #-} - ------------------------------------------------------------------------------ --- Shifting a token - -happyShift new_state 0# tk st sts stk@(x `HappyStk` _) = - let (i) = (case Happy_GHC_Exts.unsafeCoerce# x of { (Happy_GHC_Exts.I# (i)) -> i }) in --- trace "shifting the error token" $ - happyDoAction i tk new_state (HappyCons (st) (sts)) (stk) - -happyShift new_state i tk st sts stk = - happyNewToken new_state (HappyCons (st) (sts)) ((happyInTok (tk))`HappyStk`stk) - --- happyReduce is specialised for the common cases. - -happySpecReduce_0 i fn 0# tk st sts stk - = happyFail 0# tk st sts stk -happySpecReduce_0 nt fn j tk st@((action)) sts stk - = happyGoto nt j tk st (HappyCons (st) (sts)) (fn `HappyStk` stk) - -happySpecReduce_1 i fn 0# tk st sts stk - = happyFail 0# tk st sts stk -happySpecReduce_1 nt fn j tk _ sts@((HappyCons (st@(action)) (_))) (v1`HappyStk`stk') - = let r = fn v1 in - happySeq r (happyGoto nt j tk st sts (r `HappyStk` stk')) - -happySpecReduce_2 i fn 0# tk st sts stk - = happyFail 0# tk st sts stk -happySpecReduce_2 nt fn j tk _ (HappyCons (_) (sts@((HappyCons (st@(action)) (_))))) (v1`HappyStk`v2`HappyStk`stk') - = let r = fn v1 v2 in - happySeq r (happyGoto nt j tk st sts (r `HappyStk` stk')) - -happySpecReduce_3 i fn 0# tk st sts stk - = happyFail 0# tk st sts stk -happySpecReduce_3 nt fn j tk _ (HappyCons (_) ((HappyCons (_) (sts@((HappyCons (st@(action)) (_))))))) (v1`HappyStk`v2`HappyStk`v3`HappyStk`stk') - = let r = fn v1 v2 v3 in - happySeq r (happyGoto nt j tk st sts (r `HappyStk` stk')) - -happyReduce k i fn 0# tk st sts stk - = happyFail 0# tk st sts stk -happyReduce k nt fn j tk st sts stk - = case happyDrop (k Happy_GHC_Exts.-# (1# :: Happy_GHC_Exts.Int#)) sts of - sts1@((HappyCons (st1@(action)) (_))) -> - let r = fn stk in -- it doesn't hurt to always seq here... - happyDoSeq r (happyGoto nt j tk st1 sts1 r) - -happyMonadReduce k nt fn 0# tk st sts stk - = happyFail 0# tk st sts stk -happyMonadReduce k nt fn j tk st sts stk = - happyThen1 (fn stk tk) (\r -> happyGoto nt j tk st1 sts1 (r `HappyStk` drop_stk)) - where (sts1@((HappyCons (st1@(action)) (_)))) = happyDrop k (HappyCons (st) (sts)) - drop_stk = happyDropStk k stk - -happyMonad2Reduce k nt fn 0# tk st sts stk - = happyFail 0# tk st sts stk -happyMonad2Reduce k nt fn j tk st sts stk = - happyThen1 (fn stk tk) (\r -> happyNewToken new_state sts1 (r `HappyStk` drop_stk)) - where (sts1@((HappyCons (st1@(action)) (_)))) = happyDrop k (HappyCons (st) (sts)) - drop_stk = happyDropStk k stk - - (off) = indexShortOffAddr happyGotoOffsets st1 - (off_i) = (off Happy_GHC_Exts.+# nt) - (new_state) = indexShortOffAddr happyTable off_i - - - - -happyDrop 0# l = l -happyDrop n (HappyCons (_) (t)) = happyDrop (n Happy_GHC_Exts.-# (1# :: Happy_GHC_Exts.Int#)) t - -happyDropStk 0# l = l -happyDropStk n (x `HappyStk` xs) = happyDropStk (n Happy_GHC_Exts.-# (1#::Happy_GHC_Exts.Int#)) xs - ------------------------------------------------------------------------------ --- Moving to a new state after a reduction - - -happyGoto nt j tk st = - {- nothing -} - happyDoAction j tk new_state - where (off) = indexShortOffAddr happyGotoOffsets st - (off_i) = (off Happy_GHC_Exts.+# nt) - (new_state) = indexShortOffAddr happyTable off_i - - - - ------------------------------------------------------------------------------ --- Error recovery (0# is the error token) - --- parse error if we are in recovery and we fail again -happyFail 0# tk old_st _ stk@(x `HappyStk` _) = - let (i) = (case Happy_GHC_Exts.unsafeCoerce# x of { (Happy_GHC_Exts.I# (i)) -> i }) in --- trace "failing" $ - happyError_ i tk - -{- We don't need state discarding for our restricted implementation of - "error". In fact, it can cause some bogus parses, so I've disabled it - for now --SDM - --- discard a state -happyFail 0# tk old_st (HappyCons ((action)) (sts)) - (saved_tok `HappyStk` _ `HappyStk` stk) = --- trace ("discarding state, depth " ++ show (length stk)) $ - happyDoAction 0# tk action sts ((saved_tok`HappyStk`stk)) --} - --- Enter error recovery: generate an error token, --- save the old token and carry on. -happyFail i tk (action) sts stk = --- trace "entering error recovery" $ - happyDoAction 0# tk action sts ( (Happy_GHC_Exts.unsafeCoerce# (Happy_GHC_Exts.I# (i))) `HappyStk` stk) - --- Internal happy errors: - -notHappyAtAll :: a -notHappyAtAll = error "Internal Happy error\n" - ------------------------------------------------------------------------------ --- Hack to get the typechecker to accept our action functions - - -happyTcHack :: Happy_GHC_Exts.Int# -> a -> a -happyTcHack x y = y -{-# INLINE happyTcHack #-} - - ------------------------------------------------------------------------------ --- Seq-ing. If the --strict flag is given, then Happy emits --- happySeq = happyDoSeq --- otherwise it emits --- happySeq = happyDontSeq - -happyDoSeq, happyDontSeq :: a -> b -> b -happyDoSeq a b = a `seq` b -happyDontSeq a b = b - ------------------------------------------------------------------------------ --- Don't inline any functions from the template. GHC has a nasty habit --- of deciding to inline happyGoto everywhere, which increases the size of --- the generated parser quite a bit. - - -{-# NOINLINE happyDoAction #-} -{-# NOINLINE happyTable #-} -{-# NOINLINE happyCheck #-} -{-# NOINLINE happyActOffsets #-} -{-# NOINLINE happyGotoOffsets #-} -{-# NOINLINE happyDefActions #-} - -{-# NOINLINE happyShift #-} -{-# NOINLINE happySpecReduce_0 #-} -{-# NOINLINE happySpecReduce_1 #-} -{-# NOINLINE happySpecReduce_2 #-} -{-# NOINLINE happySpecReduce_3 #-} -{-# NOINLINE happyReduce #-} -{-# NOINLINE happyMonadReduce #-} -{-# NOINLINE happyGoto #-} -{-# NOINLINE happyFail #-} - --- end of Happy Template. diff --git a/examples/BoolEqBool.cub b/examples/BoolEqBool.cub --- a/examples/BoolEqBool.cub +++ b/examples/BoolEqBool.cub @@ -86,20 +86,14 @@ transid : Bool -> Bool transid = transun Bool Bool eqBoolBool (\x -> x) -True : Bool -True = true - -False : Bool -False = false - testT : Bool -testT = transid True +testT = transid true testT' : Bool -testT' = transun Bool Bool (refl U Bool) (\x -> x) True +testT' = transun Bool Bool (refl U Bool) (\x -> x) true testF : Bool -testF = transid False +testF = transid false monoidAndBool : monoid Bool monoidAndBool = pair (true) andBool @@ -111,16 +105,16 @@ opBool2 = opm Bool mBool2 testTF : Bool -testTF = opBool2 True False +testTF = opBool2 true false testFT : Bool -testFT = opBool2 False True +testFT = opBool2 false true testFF : Bool -testFF = opBool2 False False +testFF = opBool2 false false testTT : Bool -testTT = opBool2 True True +testTT = opBool2 true true -- Bool tests: @@ -134,14 +128,13 @@ opBool3 = opm Bool mBool3 testTF3 : Bool -testTF3 = opBool3 True False +testTF3 = opBool3 true false testFT3 : Bool -testFT3 = opBool3 False True +testFT3 = opBool3 false true testFF3 : Bool -testFF3 = opBool3 False False +testFF3 = opBool3 false false testTT3 : Bool -testTT3 = opBool3 True True - +testTT3 = opBool3 true true diff --git a/examples/commutative.cub b/examples/commutative.cub deleted file mode 100644 --- a/examples/commutative.cub +++ /dev/null @@ -1,6 +0,0 @@ -module weq where - -import univ - -com : U -> U -com = pair (A -> A -> A) ( diff --git a/examples/curry.cub b/examples/curry.cub new file mode 100644 --- /dev/null +++ b/examples/curry.cub @@ -0,0 +1,99 @@ +module curry where + +import swap + +curry : (A B C:U) -> ((and A B) -> C) -> A -> B -> C +curry A B C f a b = f (pair a b) + +uncurry : (A B C:U) -> (A -> B -> C) -> (and A B) -> C +uncurry A B C g = split + pair a b -> g a b + +secCurry : (A B C :U) (f : (and A B) -> C) + -> Id ((and A B) -> C) (uncurry A B C (curry A B C f)) f +secCurry A B C f = funExt (and A B) (\ _ -> C) (uncurry A B C (curry A B C f)) f rem + where + rem : (z:and A B) -> Id C (uncurry A B C (curry A B C f) z) (f z) + rem = split + pair a b -> refl C (f (pair a b)) + +retCurry : (A B C :U) (g : A -> B -> C) + -> Id (A -> B -> C) (curry A B C (uncurry A B C g)) g +retCurry A B C g = funExt A (\ _ -> B -> C) (curry A B C (uncurry A B C g)) g rem + where + rem : (a:A) -> Id (B -> C) (curry A B C (uncurry A B C g) a) (g a) + rem a = funExt B (\ _ -> C) (curry A B C (uncurry A B C g) a) (g a) rem1 + where + rem1 : (b:B) -> Id C (curry A B C (uncurry A B C g) a b) (g a b) + rem1 b = refl C (g a b) + + +eqCurry : (A B C : U) -> Id U ((and A B) -> C) (A -> B -> C) +eqCurry A B C = isEquivEq ((and A B) -> C) (A -> B -> C) (curry A B C) rem + where + rem : isEquiv ((and A B) -> C) (A -> B -> C) (curry A B C) + rem = gradLemma ((and A B) -> C) (A -> B -> C) + (curry A B C) (uncurry A B C) (retCurry A B C) (secCurry A B C) + +typFst : U +typFst = (X Y:U) -> (and X Y) -> X + +typFst1 : U +typFst1 = (X Y:U) -> X -> Y -> X + + +eqTest : Id U typFst typFst1 +eqTest = eqPi U (\ X -> Pi U (\ Y -> (and X Y) -> X)) (\ X -> Pi U (\ Y -> X -> Y -> X)) rem + where + rem : (X:U) -> Id U (Pi U (\ Y -> (and X Y) -> X)) (Pi U (\ Y -> X -> Y -> X)) + rem X = eqPi U (\ Y -> (and X Y) -> X) (\ Y -> X -> Y -> X) rem1 + where + rem1 : (Y:U) -> Id U ((and X Y) -> X) (X -> Y -> X) + rem1 Y = eqCurry X Y X + +eqTestInv : Id U typFst1 typFst +eqTestInv = inv U ((X Y:U) -> (and X Y) -> X) ((X Y:U) -> X -> Y -> X) eqTest + +test : N +test = + transport typFst typFst1 + eqTest (\ X Y -> (fst X (\ _ -> Y))) N Bool zero true + +test1 : N +test1 = + transport typFst typFst1 + eqTest (\ X Y -> (fst X (\ _ -> Y))) N Bool (suc zero) false + +test2 : N +test2 = + transport typFst1 typFst + eqTestInv (\ X Y a b -> a) N Bool (pair zero true) + +-- more test for the equality in U + +eqTest2 : Id U typFst typFst +eqTest2 = comp U typFst typFst1 typFst eqTest eqTestInv + +eqTest3 : Id U typFst typFst1 +eqTest3 = comp U typFst typFst typFst1 eqTest2 eqTest + +eqTest4 : Id U typFst typFst +eqTest4 = comp U typFst typFst1 typFst eqTest3 (inv U typFst typFst1 eqTest3) + +test4 : N +test4 = + transport typFst typFst + eqTest2 (\ X Y -> (fst X (\ _ -> Y))) N Bool (pair (suc zero) false) + +test5 : N +test5 = + transport typFst typFst1 + eqTest3 (\ X Y -> (fst X (\ _ -> Y))) N Bool (suc zero) false + +test6 : N +test6 = + transport typFst typFst + eqTest4 (\ X Y -> (fst X (\ _ -> Y))) N Bool (pair (suc zero) false) + + + diff --git a/examples/equivTotal.cub b/examples/equivTotal.cub --- a/examples/equivTotal.cub +++ b/examples/equivTotal.cub @@ -10,14 +10,6 @@ Q : singl A a -> U Q z = P (fst A (\ x -> Id A x a) z) -lem1Sub : (A:U) (P: A -> U) (a:A) -> Id U (fiber (Sigma A P) A (fst A P) a) (P a) -lem1Sub A P a = - comp U (fiber (Sigma A P) A (fst A P) a) (Sigma (singl A a) (\ z -> P (fst A (\ x -> Id A x a) z))) (P a) - (lem2Sub A P a) (lem3Sub A P a) - -retsub : (A:U) -> (P : subset2 A) -> Id (subset2 A) (sub12 A (sub21 A P)) P -retsub A P = funExt A (\ _ -> U) (fiber (Sigma A P) A (fst A P)) P (lem1Sub A P) - -- a corollary of equivalence allTransp : (A B : U) -> hasSection (Id U A B) (Equiv A B) (IdToEquiv A B) @@ -60,6 +52,65 @@ liftTot : (A:U) (P Q : A -> U) (g : (x:A) -> P x -> Q x) -> Sigma A P -> Sigma A Q liftTot A P Q g = split pair a u -> pair a (g a u) + +lem3Sub : (A:U) (P: A -> U) (a:A) -> Id U (Sigma (singl A a) (\ z -> P (fst A (\ x -> Id A x a) z))) (P a) +lem3Sub A P a = lemContrSig (singl A a) (singContr A a) Q (pair a (refl A a)) + where + Q : singl A a -> U + Q z = P (fst A (\ x -> Id A x a) z) + + +lem2Sub : (A:U) (P: A -> U) (a:A) -> Id U (fiber (Sigma A P) A (fst A P) a) + (Sigma (Sigma A (\ x -> Id A x a)) (\ z -> P (fst A (\ x -> Id A x a) z))) +lem2Sub A P a = isoId F T f g sfg rfg + where + T : U + T = Sigma (Sigma A (\ x -> Id A x a)) (\ z -> P (fst A (\ x -> Id A x a) z)) + + F : U + F = fiber (Sigma A P) A (fst A P) a + + f : F -> T + f = split + pair z p -> rem z p + where rem : (z : Sigma A P) (p : Id A (fst A P z) a) -> T + rem = split + pair x u -> \ p -> pair (pair x p) u + + g : T -> F + g = split + pair z u -> rem z u + where rem : (z: Sigma A (\x -> Id A x a)) -> (u: P (fst A (\ x -> Id A x a) z)) -> fiber (Sigma A P) A (fst A P) a + rem = split + pair x p -> \ u -> pair (pair x u) p + + rfg : (v :F) -> Id F (g (f v)) v + rfg = split + pair z p -> rem z p + where rem : (z : Sigma A P) (p : Id A (fst A P z) a) -> Id (fiber (Sigma A P) A (fst A P) a) (g (f (pair z p))) (pair z p) + rem = split + pair x u -> \ p -> refl F (pair (pair x u) p) + + sfg : (v:T) -> Id T (f (g v)) v + sfg = split + pair z u -> rem z u + where rem : (z: Sigma A (\x -> Id A x a)) -> (u: P (fst A (\ x -> Id A x a) z)) -> Id T (f (g (pair z u))) (pair z u) + rem = split + pair x p -> \ u -> refl T (pair (pair x p) u) + +lem1Sub : (A:U) (P: A -> U) (a:A) -> Id U (fiber (Sigma A P) A (fst A P) a) (P a) +lem1Sub A P a = + comp U (fiber (Sigma A P) A (fst A P) a) (Sigma (singl A a) (\ z -> P (fst A (\ x -> Id A x a) z))) (P a) + (lem2Sub A P a) (lem3Sub A P a) + +-- retsub : (A:U) -> (P : subset2 A) -> Id (subset2 A) (sub12 A (sub21 A P)) P +-- retsub A P = funExt A (\ _ -> U) (fiber (Sigma A P) A (fst A P)) P (lem1Sub A P) + + + + + + equivTot : (A:U) (P Q : A -> U) (g : (x:A) -> P x -> Q x) -> isEquiv (Sigma A P) (Sigma A Q) (liftTot A P Q g) -> (a:A) -> Id U (P a) (Q a) diff --git a/examples/finite.cub b/examples/finite.cub new file mode 100644 --- /dev/null +++ b/examples/finite.cub @@ -0,0 +1,272 @@ +module finite where + +-- definition of finite sets and cardinality + +import description +import function +import gradLemma +import Kraus + +step : U -> U +step X = or Unit X + +incSt : (X:U) -> X -> step X +incSt X x = inr x + +injSt : (X:U) -> injective X (step X) (incSt X) +injSt X x0 x1 h = subst (step X) T (inr x0) (inr x1) h (refl X x0) + where + T : step X -> U + T = split + inl _ -> N0 + inr x -> Id X x0 x + +incUnSt : (X:U) -> Unit -> step X +incUnSt X x = inl x + +inlNotinr : (A B:U) (a:A) (b:B) -> neg (Id (or A B) (inl a) (inr b)) +inlNotinr A B a b h = subst (or A B) T (inl a) (inr b) h tt + where + T : or A B -> U + T = split + inl _ -> Unit + inr _ -> N0 + +inrNotinl : (A B:U) (a:A) (b:B) -> neg (Id (or A B) (inr b) (inl a)) +inrNotinl A B a b h = subst (or A B) T (inr b) (inl a) h tt + where + T : or A B -> U + T = split + inl _ -> N0 + inr _ -> Unit + +decSt : (X:U) -> discrete X -> discrete (step X) +decSt X dX = + split + inl a -> split + inl a1 -> inl (cong Unit (step X) (incUnSt X) a a1 (propUnit a a1)) + inr b -> inr (inlNotinr Unit X a b) + inr b -> split + inl a -> inr (inrNotinl Unit X a b) + inr b1 -> rem (dX b b1) + where rem : dec (Id X b b1) -> dec (Id (step X) (inr b) (inr b1)) + rem = split + inl p -> inl (cong X (step X) (incSt X) b b1 p) + inr h -> inr (\ p -> h (injSt X b b1 p)) + +stFin : N -> U +stFin = split + zero -> N0 + suc n -> step (stFin n) + +lemN0 : (X:U) -> Id U (or X N0) X +lemN0 X = isEquivEq (or X N0) X f ef + where + f : or X N0 -> X + f = split + inl x -> x + inr y -> efq X y + + g : X -> or X N0 + g x = inl x + + sfg : (z:or X N0) -> Id (or X N0) (g (f z)) z + sfg = split + inl x -> refl (or X N0) (inl x) + inr y -> efq (Id (or X N0) (g (f (inr y))) (inr y)) y + + rfg : (x:X) -> Id X (f (g x)) x + rfg x = refl X x + + ef : isEquiv (or X N0) X f + ef = gradLemma (or X N0) X f g rfg sfg + + + +N0Dec : discrete N0 +N0Dec = \ x y -> efq (dec (Id N0 x y)) x + + +finDec : (n:N) -> discrete (stFin n) +finDec = split + zero -> N0Dec + suc m -> decSt (stFin m) (finDec m) + +unitDec : discrete Unit +unitDec = split + tt -> split + tt -> inl (refl Unit tt) + + +isolated : (A:U) -> A -> U +isolated A a = (x:A) -> dec (Id A a x) + +-- take away one element + +takeAway : (A:U) -> A -> U +takeAway A a = Sigma A (\ x -> neg (Id A a x)) + +tAway : ptU -> U +tAway = split + pair A a -> takeAway A a + +botEl : (n:N) -> stFin (suc n) +botEl n = inl tt + +eqTkA : (n:N) -> Id U (takeAway (stFin (suc n)) (botEl n)) (stFin n) +eqTkA n = isEquivEq tS (stFin n) f equivf + where + stS : U + stS = stFin (suc n) + + bn : stS + bn = botEl n + + tS : U + tS = takeAway stS bn + + faux : (x:stS) -> neg (Id stS bn x) -> stFin n + faux = split + inl u -> \ h -> efq (stFin n) (h rem) + where rem : Id stS bn (inl u) + rem = cong Unit stS (incUnSt (stFin n)) tt u (propUnit tt u) + inr z -> \ _ -> z + + f : tS -> stFin n + f = split + pair x p -> faux x p + + lem : (x:stFin n) -> neg (Id stS bn (inr x)) + lem x = inlNotinr Unit (stFin n) tt x + + g : stFin n -> tS + g x = pair (inr x) (lem x) + + T : stS -> U + T x = neg (Id stS bn x) + + lem1 : (u:Unit) -> Id stS bn (inl u) + lem1 u = cong Unit stS (incUnSt (stFin n)) tt u (propUnit tt u) + + lem2 : propFam stS T + lem2 = \ x -> propNeg (Id stS bn x) + + sfg : (x:stFin n) -> Id (stFin n) (f (g x)) x + sfg x = refl (stFin n) x + + rfg : (z:tS) -> Id tS (g (f z)) z + rfg = split + pair x p -> rem x p + where rem : (x:stS) -> (p : T x) -> Id tS (g (f (pair x p))) (pair x p) + rem = split + inl u -> \ h -> efq (Id tS (g (f (pair (inl u) h))) (pair (inl u) h)) (h (lem1 u)) + inr z -> \ h -> eqPropFam stS T lem2 + (pair (inr z) (lem (faux (inr z) h))) (pair (inr z) h) (refl stS (inr z)) + + equivf : isEquiv tS (stFin n) f + equivf = gradLemma tS (stFin n) f g sfg rfg + +-- Pointed set with one isolated element + +hasPointIso : U -> U +hasPointIso A = Sigma A (isolated A) +ptBot : N -> ptU +ptBot n = pair (stFin (suc n)) (botEl n) + +corEqTkA : (n:N) -> Id U (tAway (ptBot n)) (stFin n) +corEqTkA = eqTkA + +mkPtU : (n:N) (x:stFin (suc n)) -> ptU +mkPtU n x = pair (stFin (suc n)) x + +homogSt : (n:N) (x:stFin (suc n)) -> Id ptU (mkPtU n x) (ptBot n) +homogSt n x = undefined + +cor1EqTkA : (n:N) (x:stFin (suc n)) -> Id U (tAway (mkPtU n x)) (stFin n) +cor1EqTkA n x = + substInv ptU (\ z -> Id U (tAway z) (stFin n)) (mkPtU n x) (ptBot n) (homogSt n x) (corEqTkA n) + +lemInjSt : (n m:N) -> Id U (stFin (suc n)) (stFin (suc m)) -> Id U (stFin n) (stFin m) +lemInjSt n m h = lem5 + where + P : U -> U + P X = (x:X) -> Id U (takeAway X x) (stFin n) + + lem1 : P (stFin (suc n)) + lem1 = cor1EqTkA n + + lem2 : P (stFin (suc m)) + lem2 = subst U P (stFin (suc n)) (stFin (suc m)) h lem1 + + Am : U + Am = takeAway (stFin (suc m)) (botEl m) + + lem3 : Id U Am (stFin m) + lem3 = cor1EqTkA m (botEl m) + + lem4 : Id U Am (stFin n) + lem4 = lem2 (botEl m) + + lem5 : Id U (stFin n) (stFin m) + lem5 = comp U (stFin n) Am (stFin m) (inv U Am (stFin n) lem4) lem3 + +lem1InjSt : (n:N) -> neg (Id U N0 (stFin (suc n))) +lem1InjSt n h = transportInv N0 (stFin (suc n)) h (botEl n) + +lem2InjSt : (n:N) -> neg (Id U (stFin (suc n)) N0) +lem2InjSt n h = transport (stFin (suc n)) N0 h (botEl n) + +lemInj : injective N U stFin +lemInj = split + zero -> split + zero -> \ _ -> refl N zero + suc m -> \ h -> efq (Id N zero (suc m)) (lem1InjSt m h) + suc n -> split + zero -> \ h -> efq (Id N (suc n) zero) (lem2InjSt n h) + suc m -> \ h -> cong N N (\ x -> suc x) n m (lemInj n m (lemInjSt n m h)) + +eqsT : U -> N -> U +eqsT X n = inh (Id U (stFin n) X) + +finite : U -> U +finite X = exists N (eqsT X) + +lemEqsT : (X:U) (n m:N) -> eqsT X n -> eqsT X m -> Id N n m +lemEqsT X n m = rem2 + where + G : U + G = Id N n m + + pG : prop G + pG = NIsSet n m + + rem : Id U (stFin n) X -> Id U (stFin m) X -> G + rem ln lm = lemInj n m (comp U (stFin n) X (stFin m) ln (inv U (stFin m) X lm)) + + rem1 : Id U (stFin n) X -> eqsT X m -> G + rem1 ln = inhrec (Id U (stFin m) X) G pG (rem ln) + + rem2 : eqsT X n -> eqsT X m -> G + rem2 hn hm = inhrec (Id U (stFin n) X) G pG (\ l -> rem1 l hm) hn + +propEqsT : (X:U) -> prop (Sigma N (eqsT X)) +propEqsT X = propSig N (eqsT X) (\ n -> squash (Id U (stFin n) X)) rem + where rem : atmostOne N (eqsT X) + rem = lemEqsT X + +cardFin : (X:U) -> finite X -> Sigma N (eqsT X) +cardFin X = inhrec (Sigma N (eqsT X)) (Sigma N (eqsT X)) (propEqsT X) (\ h -> h) + +-- Unit is finite + +finUnit : finite Unit +finUnit = inc (Sigma N (eqsT Unit)) rem + where rem : Sigma N (eqsT Unit) + rem = pair (suc zero) (inc (Id U (stFin (suc zero)) Unit) (lemN0 Unit)) + + rem1 : Id U (stFin (suc zero)) Unit + rem1 = lemN0 Unit + +test : N +test = fst N (eqsT Unit) (cardFin Unit finUnit) + diff --git a/examples/set.cub b/examples/set.cub --- a/examples/set.cub +++ b/examples/set.cub @@ -52,3 +52,13 @@ test2 : Id (Id Unit tt tt) (refl Unit tt) (refl Unit tt) test2 = lemunit tt tt (refl Unit tt) (refl Unit tt) +-- to be a set is a proposition + +setIsProp : (A:U) -> prop (set A) +setIsProp A = propPi A (\ x0 -> (x1:A) -> prop (Id A x0 x1)) rem + where rem : (x0:A) -> prop (Pi A (\ x1 -> prop (Id A x0 x1))) + rem x0 = propPi A (\ x1 -> prop (Id A x0 x1)) rem1 + where rem1 : (x1:A) -> prop (prop (Id A x0 x1)) + rem1 x1 = propIsProp (Id A x0 x1) + +-- propIsProp : (A : U) -> prop (prop A) diff --git a/examples/subset.cub b/examples/subset.cub --- a/examples/subset.cub +++ b/examples/subset.cub @@ -1,6 +1,8 @@ module subset where import univalence +import equivTotal +import elimEquiv -- a non trivial equivalence: two different ways to represent subsets -- this is not finished @@ -21,41 +23,144 @@ sub21 : (A:U) -> subset2 A -> subset1 A sub21 A P = pair (Sigma A P) (fst A P) -lem2Sub : (A:U) (P: A -> U) (a:A) -> Id U (fiber (Sigma A P) A (fst A P) a) - (Sigma (Sigma A (\ x -> Id A x a)) (\ z -> P (fst A (\ x -> Id A x a) z))) -lem2Sub A P a = isoId F T f g sfg rfg +retsub : (A:U) -> (P : subset2 A) -> Id (subset2 A) (sub12 A (sub21 A P)) P +retsub A P = funExt A (\ _ -> U) (fiber (Sigma A P) A (fst A P)) P (lem1Sub A P) + + +-- in the other direction we use a corollary of equivalence + +eqSigmaEquiv : (A B :U) (f:A -> B) -> isEquiv A B f -> (Q:B -> U) -> Id U (Sigma A (\ x -> Q (f x))) (Sigma B Q) +eqSigmaEquiv A = elimIsEquiv A C rem where - T : U - T = Sigma (Sigma A (\ x -> Id A x a)) (\ z -> P (fst A (\ x -> Id A x a) z)) + C : (B:U) -> (A->B) -> U + C B f = (Q:B->U) -> Id U (Sigma A (\ y -> Q (f y))) (Sigma B Q) - F : U - F = fiber (Sigma A P) A (fst A P) a + rem : (Q:A->U) -> Id U (Sigma A (\ y -> Q y)) (Sigma A Q) + rem Q = cong (A -> U) U (Sigma A) (\ y -> Q y) Q (funExt A (\ _ -> U) (\ y -> Q y) Q(\ y -> refl U (Q y))) - f : F -> T - f = split - pair z p -> rem z p - where rem : (z : Sigma A P) (p : Id A (fst A P z) a) -> T - rem = split - pair x u -> \ p -> pair (pair x p) u +-- but actually this is not this consequence that we need - g : T -> F - g = split - pair z u -> rem z u - where rem : (z: Sigma A (\x -> Id A x a)) -> (u: P (fst A (\ x -> Id A x a) z)) -> fiber (Sigma A P) A (fst A P) a - rem = split - pair x p -> \ u -> pair (pair x u) p +lemSecSub : (A X Y:U)(g:X->Y) -> isEquiv X Y g -> (f:Y -> A) -> + Id (subset1 A) (pair Y f) (pair X (\ y -> f (g y))) +lemSecSub A X = elimIsEquiv X P rem + where + P : (Y:U) -> (X->Y) -> U + P Y g = (f:Y -> A) -> Id (subset1 A) (pair Y f) (pair X (\ y -> f (g y))) - rfg : (v :F) -> Id F (g (f v)) v - rfg = split - pair z p -> rem z p - where rem : (z : Sigma A P) (p : Id A (fst A P z) a) -> Id (fiber (Sigma A P) A (fst A P) a) (g (f (pair z p))) (pair z p) - rem = split - pair x u -> \ p -> refl F (pair (pair x u) p) + rem : (f:X -> A) -> Id (subset1 A) (pair X f) (pair X (\ y -> f y)) + rem f = cong (X->A) (subset1 A) (\ h -> pair X h) f (\ y -> f y) + (funExt X (\ _ -> A) f (\ y -> f y) (\ y -> refl A (f y))) - sfg : (v:T) -> Id T (f (g v)) v - sfg = split - pair z u -> rem z u - where rem : (z: Sigma A (\x -> Id A x a)) -> (u: P (fst A (\ x -> Id A x a) z)) -> Id T (f (g (pair z u))) (pair z u) - rem = split - pair x p -> \ u -> refl T (pair (pair x p) u) +lem2SecSub : (A X:U) (f:X -> A) -> isEquiv X (Sigma A (fiber X A f)) (\ x -> pair (f x) (pair x (refl A (f x)))) +lem2SecSub A X f = rem2 + where + F : A -> U + F = fiber X A f + Y : U + Y = Sigma A F + + h : Y -> A + h = fst A F + + g : X -> Y + g x = pair (f x) (pair x (refl A (f x))) + + h : Y -> X + h = split + pair a xp -> fst X (\ x -> Id A (f x) a) xp + + Z : U + Z = Sigma X (\ x -> Sigma A (\ a -> Id A (f x) a)) + + sw1 : Y -> Z + sw1 = split + pair a xp -> asw1 xp + where asw1 : Sigma X (\ x -> Id A (f x) a) -> Z + asw1 = split + pair x p -> pair x (pair a p) + + sw2 : Z -> Y + sw2 = split + pair x ap -> asw2 ap + where asw2 : Sigma A (\ a -> Id A (f x) a) -> Y + asw2 = split + pair a p -> pair a (pair x p) + + lemsw : (y:Y) -> Id Y (sw2 (sw1 y)) y + lemsw = split + pair a xp -> lemsw1 xp + where lemsw1 : (xp : Sigma X (\ x -> Id A (f x) a)) -> Id Y (sw2 (sw1 (pair a xp))) (pair a xp) + lemsw1 = split + pair x p -> refl Y (pair a (pair x p)) + + sgh : (x:X) -> Id X (h (g x)) x + sgh x = refl X x + + rgh : (y:Y) -> Id Y (g (h y)) y + rgh = split + pair a xp -> lem xp + where + lem : (xp : Sigma X (\ x -> Id A (f x) a)) -> Id Y (g (h (pair a xp))) (pair a xp) + lem = split + pair x p -> lem1 + where + C : (v u:A) -> Id A v u -> U + C v u q = Id (Sigma A (\ w -> Id A v w)) (pair v (refl A v)) (pair u q) + + lem5 : (v:A) -> C v v (refl A v) + lem5 v = refl (Sigma A (\ w -> Id A v w)) (pair v (refl A v)) + + lem4 : (v u:A) (q: Id A v u) -> C v u q + lem4 v = J A v (C v) (lem5 v) + + lem3 : Id (Sigma A (\ u -> Id A (f x) u)) (pair (f x) (refl A (f x))) (pair a p) + lem3 = lem4 (f x) a p + + lem2 : Id Z (pair x (pair (f x) (refl A (f x)))) (pair x (pair a p)) + lem2 = cong (Sigma A (\ a -> Id A (f x) a)) + (Sigma X (\ x -> Sigma A (\ a -> Id A (f x) a))) + (\ z -> pair x z) + (pair (f x) (refl A (f x))) (pair a p) lem3 + + lem1 : Id Y (pair (f x) (pair x (refl A (f x)))) (pair a (pair x p)) + lem1 = cong Z Y sw2 (pair x (pair (f x) (refl A (f x)))) (pair x (pair a p)) lem2 + + rem2 : isEquiv X Y g + rem2 = gradLemma X Y g h rgh sgh + + +secsub : (A:U) -> (z : subset1 A) -> Id (subset1 A) (sub21 A (sub12 A z)) z +secsub A = + split + pair X f -> rem + where + F : A -> U + F = fiber X A f + + Y : U + Y = Sigma A F + + h : Y -> A + h = fst A F + + g : X -> Y + g x = pair (f x) (pair x (refl A (f x))) + + rem2 : isEquiv X Y (\ x -> g x) + rem2 = lem2SecSub A X f + + rem1 : Id (subset1 A) (pair Y h) (pair X (\ x -> f x)) + rem1 = lemSecSub A X Y g rem2 h + + rem3 : Id (subset1 A) (pair X (\ x -> f x)) (pair X f) + rem3 = cong (X->A) (subset1 A) (\ h -> pair X h) + (\ x -> f x) f (funExt X (\ _ -> A) (\ x-> f x) f (\x -> refl A (f x))) + + rem : Id (subset1 A) (pair Y h) (pair X f) + rem = comp (subset1 A) (pair Y h) (pair X (\ x -> f x)) (pair X f) rem1 rem3 + +thmSubset : (A:U) -> Id U (subset1 A) (subset2 A) +thmSubset A = isEquivEq (subset1 A) (subset2 A) (sub12 A) rem + where rem : isEquiv (subset1 A) (subset2 A) (sub12 A) + rem = gradLemma (subset1 A) (subset2 A) (sub12 A) (sub21 A) (retsub A) (secsub A) diff --git a/examples/test.cub b/examples/test.cub new file mode 100644 --- /dev/null +++ b/examples/test.cub @@ -0,0 +1,21 @@ +module test where + +Id : (A : U) (a b : A) -> U +Id = PN + +refl : (A : U) (a : A) -> Id A a a +refl = PN + +Bool : U +data Bool = true | false + +orBool : Bool -> Bool -> Bool +orBool = split + true -> \x -> true + false -> \x -> x + +id : Bool -> Bool +id x = x + +test : Id Bool true (orBool true false) +test = refl Bool true