cubical 0.1.0 → 0.1.1
raw patch · 19 files changed
+711/−1446 lines, 19 filessetup-changed
Files
- CTT.hs +2/−4
- Concrete.hs +0/−2
- Eval.hs +0/−0
- Exp.cf +7/−4
- Main.hs +56/−23
- Makefile +2/−2
- README.md +17/−7
- Setup.hs +18/−4
- cubical.cabal +1/−1
- dist/build/cubical/cubical-tmp/Exp/Lex.hs +0/−351
- dist/build/cubical/cubical-tmp/Exp/Par.hs +0/−985
- examples/BoolEqBool.cub +11/−18
- examples/commutative.cub +0/−6
- examples/curry.cub +99/−0
- examples/equivTotal.cub +59/−8
- examples/finite.cub +272/−0
- examples/set.cub +10/−0
- examples/subset.cub +136/−31
- examples/test.cub +21/−0
CTT.hs view
@@ -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"
Concrete.hs view
@@ -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')-
Eval.hs view
Exp.cf view
@@ -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 ";" ;
Main.hs view
@@ -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
Makefile view
@@ -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
README.md view
@@ -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 <x>p(x) where the name x is bound. An identity proof +then of the form \<x\>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 -<x><y>p(x,y). See examples/hedberg.cub and the example test3 (in the +\<x\>\<y\>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
Setup.hs view
@@ -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
cubical.cabal view
@@ -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.
− dist/build/cubical/cubical-tmp/Exp/Lex.hs
@@ -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 "<command-line>" #-}-{-# 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
− dist/build/cubical/cubical-tmp/Exp/Par.hs
@@ -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 "<built-in>" #-}-{-# LINE 1 "<command-line>" #-}-{-# 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.
examples/BoolEqBool.cub view
@@ -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
− examples/commutative.cub
@@ -1,6 +0,0 @@-module weq where - -import univ - -com : U -> U -com = pair (A -> A -> A) (
+ examples/curry.cub view
@@ -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)+++
examples/equivTotal.cub view
@@ -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)
+ examples/finite.cub view
@@ -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)+
examples/set.cub view
@@ -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)
examples/subset.cub view
@@ -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)
+ examples/test.cub view
@@ -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