text:
module EDSL

--import TypeTrans.AST
import TypeTrans.Transformations
import TypeTrans.Array
import Control.Monad.State

import Data.Vect

data TypeT = TyInt | TyBool | TyFun TypeT TypeT | TyVect Nat TypeT

-- Difference between stream and seq?
data MapVariant = MSeq | MPar | MStream
data FoldVariant = FSeq | FStream | FTree

total
interpType : TypeT -> Type
interpType TyInt = Int
interpType TyBool = Bool
interpType (TyFun i o) = interpType i -> interpType o
interpType (TyVect i t) = Vect i (interpType t)

-- Locate "base"/primitive type e.g. int, bool
--total
--baseType : TypeT -> TypeT
--baseType (TyFun i o) =
--baseType TyVect Nat

using (G : Vect xs TypeT) {

data HasType : Fin n -> Vect n TypeT -> TypeT -> Type where
  Stop : HasType FZ (t :: G) t
  Pop  : HasType k G t -> HasType (FS k) (u :: G) t

data Expr : (Vect xs TypeT) -> TypeT -> Type where
  Var : HasType i G t -> Expr G t
  Val : (x : Int) -> Expr G TyInt
  Map : MapVariant -> Expr G (TyFun a b) -> Expr G (TyVect n a) -> Expr G (TyVect n b)

  -- Treat Composition as Concatonation of multiple Applys in a row
  -- Apply f (Apply g o)  is a composition of f and g, can be used for
  -- map streaming optimisation
  Apply : Expr G (TyFun a b) -> Expr G a -> Expr G b
  --Let : Expr (a :: gam) (Val () :: gam’) (R t) -> Expr gam gam’ t

  FoldL : FoldVariant -> Expr G (TyFun a (TyFun b a)) ->
                          Expr G a  -> Expr G (TyVect n b) -> Expr G a
  FoldR : FoldVariant -> Expr G (TyFun a (TyFun b b)) ->
                          Expr G b  -> Expr G (TyVect n a) -> Expr G b

  -- For Assoc Fold, the function needs to be closed e.g. (a -> a -> a), possibly
  -- ensure given type is a monoid and use the respective monoid function for that type,
  -- using implicit type class instances we can select which monoid we wish to use
  -- e.g. the natural numbers can create a monoid instance for both addition and multiplication
  --FoldAssoc : (Monoid (interpType a)) => FoldVariant -> Expr G a -> Expr G (TyVect n a) -> Expr G a

  Lambda : Expr (a :: G) t -> Expr G (TyFun a t)
  --Compose : Expr G (TyFun a  -> Expr (head a

  Split : (m: Nat) -> Expr G (TyVect n t) ->
                      {default SIsNotZ nz : Not (m = Z)} ->
                      {auto mz : modNatNZ n m nz = Z} ->
                      Expr G (TyVect m (TyVect (divNatNZ n m nz) t))

  Merge : Expr G (TyVect x1 (TyVect x2 t)) -> Expr G (TyVect (x1 * x2) t)
  Op : (interpType a -> interpType b -> interpType c) -> Expr G a -> Expr G b -> Expr G c
  UnOp : (interpType a -> interpType b) -> Expr G a -> Expr G b

-- Idris Interpreter which executes the AST

-- When we produce an expression we need to know which variables are in scope,
-- as well as their types. Env is an environment indexed over the types in scope.
data Env : Vect n TypeT -> Type where
  Nil : Env Nil
  (::) : interpType a -> Env G -> Env (a :: G)

lookup : HasType i G t -> Env G -> interpType t
lookup Stop (x :: xs) = x
lookup (Pop k) (x :: xs) = lookup k xs

interp : Env G -> Expr G t -> interpType t
interp env (Var i) = lookup i env
interp env (Val x) = x
interp env (Apply f s) = (interp env f) (interp env s)
interp env (Lambda body) = \x => interp (x :: env) body
interp env (Map vt f xs) =
  case (interp env xs) of
    [] => Nil
    (y::ys) => (interp env (Apply f (UnOp head xs))) :: (interp env (Map vt f (UnOp tail xs)))

interp env (FoldL vt f x xs) =
  case (interp env xs) of
    [] => interp env x
    (y::ys) => interp env $ FoldL vt f (Apply (Apply f x) $ UnOp head xs) $ UnOp tail xs

interp env (FoldR vt f x xs) =
  case (interp env xs) of
    [] => interp env x
    (y::ys) => interp env $ Apply (Apply f $ UnOp head xs) (FoldR vt f x $ UnOp tail xs)

--interp env (FoldAssoc vt f x xs) = interp env (FoldL vt f x xs)

interp env (Op op x y) = op (interp env x) (interp env y)
interp env (UnOp op x) = op (interp env x)
--interp env (Merge xs) = merge $ interp env xs
--interp env (Split m xs {nz} {mz}) = splitV m {nz} {mz} $ interp env xs

-- Generate All Different Combinations
generate : Env G -> Expr G t -> Expr G t
generate env (Var i) = (Var i)
generate env (Val x) = (Val x)
generate env (Apply f s) = Apply (convertS env f) (convertS env s)
generate env (Lambda body) = Lambda (convertS body)
generate env (Map vt f xs) = ?todo45
--  case (interp env xs) of
--    [] => Nil
--    (y::ys) => (interp env (Apply f (UnOp head xs))) :: (interp env (Map vt f (UnOp tail xs)))
generate env (FoldL vt f x xs) = ?todo57
--  case (interp env xs) of
--    [] => interp env x
--    (y::ys) => interp env $ FoldL vt f (Apply (Apply f x) $ UnOp head xs) $ UnOp tail xs

generate env (FoldR vt f x xs) = ?todo56
--  case (interp env xs) of
--    [] => interp env x
--    (y::ys) => interp env $ Apply (Apply f $ UnOp head xs) (FoldR vt f x $ UnOp tail xs)

--interp env (FoldAssoc vt f x xs) = interp env (FoldL vt f x xs)

interp env (Op op x y) = Op op (generate env x) (generate env y)
interp env (UnOp op x) = UnOp op (generate env x)

mkLam : TTName -> Expr (t::g) t' -> Expr g (TyFun t t')
mkLam _ body = Lambda body

-- Specify structures for DSL
dsl expr
  lambda = mkLam
  variable = Var
  index_first = Stop
  index_next = Pop
  variable = Var

pure : Expr G a -> Expr G a
pure = id

(<$>) : (f : Lazy (Expr G (TyFun a t))) -> Expr G a -> Expr G t
(<$>) f a = Apply f a

-- Examples:
syntax "map" [f] [xs] = Map MSeq f xs
syntax [x] "+" [y] = Op (+) x (Val y)

-- AST for lambda function which adds 3 to a given integer
add3 : Expr G (TyFun TyInt TyInt)
add3 = Lambda (Op (+) (Var Stop) (Val 3))

add3Pretty : Expr G (TyFun TyInt TyInt)
add3Pretty = expr (\x => Op (+) (Val 3) x)

add3Pretty2 : Expr G (TyFun TyInt TyInt)
add3Pretty2 = expr (\x => x + 3)

-- AST for lambda function which adds 2 integers
add : Expr G (TyFun TyInt (TyFun TyInt TyInt))
add = Lambda (Lambda (Op (+) (Var Stop) (Var (Pop Stop))))

addPretty : Expr G (TyFun TyInt (TyFun TyInt TyInt))
addPretty = expr (\x,y => (Op (+) x y))

-- AST for simple mapping over list
mapAdd3 : Expr G (TyFun (TyVect n TyInt) (TyVect n TyInt))
mapAdd3 = Lambda (Map MSeq (add3) (Var Stop))

mapAdd3Pretty : Expr G (TyFun (TyVect n TyInt) (TyVect n TyInt))
mapAdd3Pretty = expr (\xs => map add3 xs)

-- AST for simple merge and mapping
map2dAdd3 : Expr G (TyFun (TyVect m (TyVect n TyInt)) (TyVect (m * n) TyInt))
map2dAdd3 = Lambda (Apply (mapAdd3) (Merge (Var Stop)))

testAdd : Int ->  Expr G (TyFun TyInt TyInt)
testAdd i = Lambda (Op (+) (Var Stop) (Val i))

testAdd' : {n : Nat} -> Vect n t ->  Expr G (TyFun TyInt TyInt)
testAdd' v {n} = Lambda (Op (+) (Var Stop) (Val $ fromNat n))

--splitEx : Expr G (TyFun (TyVect (m * n) TyInt) (TyVect m (TyVect n TyInt)))
--splitEx {m = Z} = ?todo45 --Lambda (Var Stop)
--splitEx {m = S k} {n} = rewrite (modMProof m n) in (Lambda (Split m (Var Stop)))

--AST for merge, map, then split again
--mapAddSplit : Expr G (TyFun (TyVect m (TyVect n TyInt)) (TyVect m (TyVect n TyInt)))
--mapAddSplit {m = Z} = Lambda (Var Stop)
--mapAddSplit {m = S k} = Lambda (Split m $ Apply (mapAdd3) (Merge (Var Stop)))

{-
print2dV : Vect m (Vect n Int) -> IO ()
print2dV xs =
    do print "["
       print2dV' xs

  where print2dV' : Vect m (Vect n Int) -> IO ()
        print2dV' [] = print "]"
        print2dV' (x::[]) = do print x
                               print "]"

        print2dV' (x::xs) = do print x
                               print ", "
                               print2dV' xs

-}

interpStuff : IO ()
interpStuff = do
    print $ interp [] mapAdd3 [1,2,3,4]
    print v2d

    print v3

  where v2d : Vect 3 Int
        v2d = interp [] map2dAdd3 [[1,1,1]]

        v3 : Int
        v3 = interp [] add3 3
}

max_stars_repo_name: RossMeikleham/MSci-Project

max_issues_repo_name: RossMeikleham/MSci-Project

max_forks_repo_name: RossMeikleham/MSci-Project


text:
{--
Copyright 2021 Joel Berkeley

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
--}
||| This module contains general library utilities.
module Util

import Data.Vect

||| All numbers from `0` to `n - 1` inclusive, in increasing order.
|||
||| @n The (exclusive) limit of the range.
export
range : (n : Nat) -> Vect n Nat
range Z = []
range (S n) = snoc (range n) n

ext: idr

max_stars_repo_name: joelberkeley/spidr

max_issues_repo_name: joelberkeley/spidr

max_forks_repo_name: joelberkeley/spidr


text:
module Main

main : IO ()
main = putStrLn "Hello World"

-- [ EOF ]


text:
import Data.Vect
import Data.String
import System.File.Handle
import System.File.Mode
import System.File.ReadWrite

data VectUnknown : Type -> Type where
     MkVect : (len : Nat) -> Vect len a -> VectUnknown a

readVect : IO (len ** Vect len String)
readVect = do x <- getLine
              if (x == "")
                then pure (_ ** [])
                else do (_ ** xs) <- readVect
                        pure (_ ** x :: xs)

printVect : Show a => VectUnknown a -> IO ()
printVect (MkVect len xs) = putStrLn (show xs ++ " (length " ++ show len ++ ")")

zipInputs : IO ()
zipInputs = do putStrLn "Enter first vector (blank line to end):"
               (len1 ** vec1) <- readVect
               putStrLn "Enter second vector (blank line to end):"
               (len2 ** vec2) <- readVect
               case exactLength len1 vec2 of
                    Nothing => putStrLn "Vectors are different lengths"
                    Just vec2 => printLn (zip vec1 vec2)

readToBlank : IO (List String)
readToBlank = do x <- getLine
                 if x == ""
                    then pure ([])
                    else do xs <- readToBlank
                            pure (x :: xs)

||| Read until blank line then
||| Read file name and save entered data to file
readAndSave : IO ()
readAndSave = do putStrLn "Type some lines (blank line to end):"
                 list <- readToBlank
                 putStrLn "Enter file name:"
                 fileName <- getLine
                 Left err <- writeFile fileName (unlines list)
                           | Right () => pure ()
                 printLn err

msg : String -> Maybe FileError -> IO (n ** Vect n String)
msg m err = let m_ = case err of
                          Nothing => m
                          Just err => m ++ ": " ++ (show err)
                     in do putStrLn m_
                           pure (_ ** [])

||| Reads file contents into Vect
||| ex.
|||   :exec readVectFile "test.txt" >>= printLn
readVectFile : (filename : String) -> IO (n ** Vect n String)
readVectFile filename = do Right file <- openFile filename Read
                                       | Left err => msg "Could not open file" (Just err)
                           nextLine file where
                           nextLine : File -> IO (n ** Vect n String)
                           nextLine f = do eof <- fEOF f
                                           if eof then msg "Done reading file" Nothing
                                            else do Right line <- fGetLine f
                                                                | Left err => msg "Could not read line" (Just err)
                                                    (_ ** xs) <- nextLine f
                                                    pure (_ ** line :: xs)

handleErr : FileError -> IO String
handleErr err = pure (show err)

readFileToVect : File -> IO (Either String (n ** Vect n String))
readFileToVect f = do eof <- fEOF f
                      if eof then pure (Right (_ ** []))
                        else do Right line <- fGetLine f
                                                 | Left err => pure (Left (show err))
                                Right (_ ** xs) <- readFileToVect f
                                                 | Left err => pure (Left (show err))
                                pure (Right (_ ** line :: xs))

||| Reads file contents into Vect using withFile
||| Returns either an error message or the Vect of file contents
readVectFile2 : (filename : String) -> IO (Either String (n ** Vect n String))
readVectFile2 filename = do withFile filename Read handleErr readFileToVect


text:
module Data.Surely

%default total
%access public export

||| A `Surely a` represents an input value.
||| It can be exactly the value `a`,
||| or anything which matches the type of `a`.
|||
||| It is similar to `Maybe a`,
||| except that `Anything` is equal to every exact value.
||| That means that `Semantics.inputs` can produce `Change` inputs
||| without specifying a specific input value.
data Surely a
  = Exactly a
  | Anything

toMaybe : Surely a -> Maybe a
toMaybe (Exactly x) = Just x
toMaybe (Anything)  = Nothing

toSurely : Maybe a -> Surely a
toSurely (Just x)  = Exactly x
toSurely (Nothing) = Anything

Eq a => Eq (Surely a) where
  (Exactly x) == (Exactly y) = x == y
  (Anything)  == (Exactly _) = True
  (Exactly _) == (Anything)  = True
  (Anything)  == (Anything)  = True

max_stars_repo_name: mklinik/task-semantics

max_issues_repo_name: mklinik/task-semantics

max_forks_repo_name: mklinik/task-semantics


text:
{-
Copyright 2019, Mokshasoft AB (mokshasoft.com)

This software may be distributed and modified according to the terms of
the BSD 2-Clause license. Note that NO WARRANTY is provided.
See "LICENSE_BSD2.txt" for details.
-}

module StarterWareFree.Utils

%access public export
%default total
%include C "consoleUtils.h"

ConsoleUtilsInit : IO ()
ConsoleUtilsInit =
    foreign FFI_C "ConsoleUtilsInit" (IO ())

ConsoleUtilsSetType : Int -> IO ()
ConsoleUtilsSetType type =
    foreign FFI_C "ConsoleUtilsSetType" (Int -> IO ()) type

ConsoleUtilsPrintf : String -> IO ()
ConsoleUtilsPrintf str =
    foreign FFI_C "ConsoleUtilsPrintf" (String -> IO ()) str

max_stars_repo_name: mokshasoft/starterwarefree-idris-ffi

max_issues_repo_name: mokshasoft/starterwarefree-idris-ffi

max_forks_repo_name: mokshasoft/starterwarefree-idris-ffi


text:
module Compiler.Erlang.Utils.PrimTerm

import Data.List
import Compiler.Erlang.Utils.CompositeString
import Compiler.Erlang.Utils.String

%default total

public export
data PrimTerm
  = PAtom String
  | PChar Char
  | PFloat Double
  | PInteger Integer
  | PTuple (List PrimTerm)
  | PList (List PrimTerm)
  | PCharlist String

export
primTermToCS : PrimTerm -> CompositeString
primTermToCS (PAtom str) = Nested [Str "'", Str (escapeString (unpack str) ""), Str "'"]
primTermToCS (PChar x) = Nested [Str "$", Str (escapeChar x "")]
primTermToCS (PFloat x) = Str (showDouble x)
primTermToCS (PInteger x) = Str (show x)
primTermToCS (PTuple xs) = Nested [Str "{", Nested $ intersperse (Str ",") (assert_total (map primTermToCS xs)), Str "}"]
primTermToCS (PList xs) = Nested [Str "[", Nested $ intersperse (Str ",") (assert_total (map primTermToCS xs)), Str "]"]
primTermToCS (PCharlist str) = Nested [Str "\"", Str (escapeString (unpack str) ""), Str "\""]


text:
%!PS-Adobe-2.0 EPSF-1.2
%%Creator: idraw
%%DocumentFonts: Helvetica
%%Pages: 1
%%BoundingBox: 21 320 330 606
%%EndComments

%%BeginIdrawPrologue
/arrowhead {
0 begin
transform originalCTM itransform
/taily exch def
/tailx exch def
transform originalCTM itransform
/tipy exch def
/tipx exch def
/dy tipy taily sub def
/dx tipx tailx sub def
/angle dx 0 ne dy 0 ne or { dy dx atan } { 90 } ifelse def
gsave
originalCTM setmatrix
tipx tipy translate
angle rotate
newpath
arrowHeight neg arrowWidth 2 div moveto
0 0 lineto
arrowHeight neg arrowWidth 2 div neg lineto
patternNone not {
originalCTM setmatrix
/padtip arrowHeight 2 exp 0.25 arrowWidth 2 exp mul add sqrt brushWidth mul
arrowWidth div def
/padtail brushWidth 2 div def
tipx tipy translate
angle rotate
padtip 0 translate
arrowHeight padtip add padtail add arrowHeight div dup scale
arrowheadpath
ifill
} if
brushNone not {
originalCTM setmatrix
tipx tipy translate
angle rotate
arrowheadpath
istroke
} if
grestore
end
} dup 0 9 dict put def

/arrowheadpath {
newpath
arrowHeight neg arrowWidth 2 div moveto
0 0 lineto
arrowHeight neg arrowWidth 2 div neg lineto
} def

/leftarrow {
0 begin
y exch get /taily exch def
x exch get /tailx exch def
y exch get /tipy exch def
x exch get /tipx exch def
brushLeftArrow { tipx tipy tailx taily arrowhead } if
end
} dup 0 4 dict put def

/rightarrow {
0 begin
y exch get /tipy exch def
x exch get /tipx exch def
y exch get /taily exch def
x exch get /tailx exch def
brushRightArrow { tipx tipy tailx taily arrowhead } if
end
} dup 0 4 dict put def

%%EndIdrawPrologue

/arrowHeight 11 def
/arrowWidth 5 def

/IdrawDict 51 dict def
IdrawDict begin

/reencodeISO {
dup dup findfont dup length dict begin
{ 1 index /FID ne { def }{ pop pop } ifelse } forall
/Encoding ISOLatin1Encoding def
currentdict end definefont
} def

/ISOLatin1Encoding [
/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef
/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef
/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef
/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef
/space/exclam/quotedbl/numbersign/dollar/percent/ampersand/quoteright
/parenleft/parenright/asterisk/plus/comma/minus/period/slash
/zero/one/two/three/four/five/six/seven/eight/nine/colon/semicolon
/less/equal/greater/question/at/A/B/C/D/E/F/G/H/I/J/K/L/M/N
/O/P/Q/R/S/T/U/V/W/X/Y/Z/bracketleft/backslash/bracketright
/asciicircum/underscore/quoteleft/a/b/c/d/e/f/g/h/i/j/k/l/m
/n/o/p/q/r/s/t/u/v/w/x/y/z/braceleft/bar/braceright/asciitilde
/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef
/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef/.notdef
/.notdef/dotlessi/grave/acute/circumflex/tilde/macron/breve
/dotaccent/dieresis/.notdef/ring/cedilla/.notdef/hungarumlaut
/ogonek/caron/space/exclamdown/cent/sterling/currency/yen/brokenbar
/section/dieresis/copyright/ordfeminine/guillemotleft/logicalnot
/hyphen/registered/macron/degree/plusminus/twosuperior/threesuperior
/acute/mu/paragraph/periodcentered/cedilla/onesuperior/ordmasculine
/guillemotright/onequarter/onehalf/threequarters/questiondown
/Agrave/Aacute/Acircumflex/Atilde/Adieresis/Aring/AE/Ccedilla
/Egrave/Eacute/Ecircumflex/Edieresis/Igrave/Iacute/Icircumflex
/Idieresis/Eth/Ntilde/Ograve/Oacute/Ocircumflex/Otilde/Odieresis
/multiply/Oslash/Ugrave/Uacute/Ucircumflex/Udieresis/Yacute
/Thorn/germandbls/agrave/aacute/acircumflex/atilde/adieresis
/aring/ae/ccedilla/egrave/eacute/ecircumflex/edieresis/igrave
/iacute/icircumflex/idieresis/eth/ntilde/ograve/oacute/ocircumflex
/otilde/odieresis/divide/oslash/ugrave/uacute/ucircumflex/udieresis
/yacute/thorn/ydieresis
] def
/Helvetica reencodeISO def

/none null def
/numGraphicParameters 17 def
/stringLimit 65535 def

/Begin {
save
numGraphicParameters dict begin
} def

/End {
end
restore
} def

/SetB {
dup type /nulltype eq {
pop
false /brushRightArrow idef
false /brushLeftArrow idef
true /brushNone idef
} {
/brushDashOffset idef
/brushDashArray idef
0 ne /brushRightArrow idef
0 ne /brushLeftArrow idef
/brushWidth idef
false /brushNone idef
} ifelse
} def

/SetCFg {
/fgblue idef
/fggreen idef
/fgred idef
} def

/SetCBg {
/bgblue idef
/bggreen idef
/bgred idef
} def

/SetF {
/printSize idef
/printFont idef
} def

/SetP {
dup type /nulltype eq {
pop true /patternNone idef
} {
dup -1 eq {
/patternGrayLevel idef
/patternString idef
} {
/patternGrayLevel idef
} ifelse
false /patternNone idef
} ifelse
} def

/BSpl {
0 begin
storexyn
newpath
n 1 gt {
0 0 0 0 0 0 1 1 true subspline
n 2 gt {
0 0 0 0 1 1 2 2 false subspline
1 1 n 3 sub {
/i exch def
i 1 sub dup i dup i 1 add dup i 2 add dup false subspline
} for
n 3 sub dup n 2 sub dup n 1 sub dup 2 copy false subspline
} if
n 2 sub dup n 1 sub dup 2 copy 2 copy false subspline
patternNone not brushLeftArrow not brushRightArrow not and and { ifill } if
brushNone not { istroke } if
0 0 1 1 leftarrow
n 2 sub dup n 1 sub dup rightarrow
} if
end
} dup 0 4 dict put def

/Circ {
newpath
0 360 arc
closepath
patternNone not { ifill } if
brushNone not { istroke } if
} def

/CBSpl {
0 begin
dup 2 gt {
storexyn
newpath
n 1 sub dup 0 0 1 1 2 2 true subspline
1 1 n 3 sub {
/i exch def
i 1 sub dup i dup i 1 add dup i 2 add dup false subspline
} for
n 3 sub dup n 2 sub dup n 1 sub dup 0 0 false subspline
n 2 sub dup n 1 sub dup 0 0 1 1 false subspline
patternNone not { ifill } if
brushNone not { istroke } if
} {
Poly
} ifelse
end
} dup 0 4 dict put def

/Elli {
0 begin
newpath
4 2 roll
translate
scale
0 0 1 0 360 arc
closepath
patternNone not { ifill } if
brushNone not { istroke } if
end
} dup 0 1 dict put def

/Line {
0 begin
2 storexyn
newpath
x 0 get y 0 get moveto
x 1 get y 1 get lineto
brushNone not { istroke } if
0 0 1 1 leftarrow
0 0 1 1 rightarrow
end
} dup 0 4 dict put def

/MLine {
0 begin
storexyn
newpath
n 1 gt {
x 0 get y 0 get moveto
1 1 n 1 sub {
/i exch def
x i get y i get lineto
} for
patternNone not brushLeftArrow not brushRightArrow not and and { ifill } if
brushNone not { istroke } if
0 0 1 1 leftarrow
n 2 sub dup n 1 sub dup rightarrow
} if
end
} dup 0 4 dict put def

/Poly {
3 1 roll
newpath
moveto
-1 add
{ lineto } repeat
closepath
patternNone not { ifill } if
brushNone not { istroke } if
} def

/Rect {
0 begin
/t exch def
/r exch def
/b exch def
/l exch def
newpath
l b moveto
l t lineto
r t lineto
r b lineto
closepath
patternNone not { ifill } if
brushNone not { istroke } if
end
} dup 0 4 dict put def

/Text {
ishow
} def

/idef {
dup where { pop pop pop } { exch def } ifelse
} def

/ifill {
0 begin
gsave
patternGrayLevel -1 ne {
fgred bgred fgred sub patternGrayLevel mul add
fggreen bggreen fggreen sub patternGrayLevel mul add
fgblue bgblue fgblue sub patternGrayLevel mul add setrgbcolor
eofill
} {
eoclip
originalCTM setmatrix
pathbbox /t exch def /r exch def /b exch def /l exch def
/w r l sub ceiling cvi def
/h t b sub ceiling cvi def
/imageByteWidth w 8 div ceiling cvi def
/imageHeight h def
bgred bggreen bgblue setrgbcolor
eofill
fgred fggreen fgblue setrgbcolor
w 0 gt h 0 gt and {
l w add b translate w neg h scale
w h true [w 0 0 h neg 0 h] { patternproc } imagemask
} if
} ifelse
grestore
end
} dup 0 8 dict put def

/istroke {
gsave
brushDashOffset -1 eq {
[] 0 setdash
1 setgray
} {
brushDashArray brushDashOffset setdash
fgred fggreen fgblue setrgbcolor
} ifelse
brushWidth setlinewidth
originalCTM setmatrix
stroke
grestore
} def

/ishow {
0 begin
gsave
fgred fggreen fgblue setrgbcolor
/fontDict printFont printSize scalefont dup setfont def
/descender fontDict begin 0 /FontBBox load 1 get FontMatrix end
transform exch pop def
/vertoffset 1 printSize sub descender sub def {
0 vertoffset moveto show
/vertoffset vertoffset printSize sub def
} forall
grestore
end
} dup 0 3 dict put def
/patternproc {
0 begin
/patternByteLength patternString length def
/patternHeight patternByteLength 8 mul sqrt cvi def
/patternWidth patternHeight def
/patternByteWidth patternWidth 8 idiv def
/imageByteMaxLength imageByteWidth imageHeight mul
stringLimit patternByteWidth sub min def
/imageMaxHeight imageByteMaxLength imageByteWidth idiv patternHeight idiv
patternHeight mul patternHeight max def
/imageHeight imageHeight imageMaxHeight sub store
/imageString imageByteWidth imageMaxHeight mul patternByteWidth add string def
0 1 imageMaxHeight 1 sub {
/y exch def
/patternRow y patternByteWidth mul patternByteLength mod def
/patternRowString patternString patternRow patternByteWidth getinterval def
/imageRow y imageByteWidth mul def
0 patternByteWidth imageByteWidth 1 sub {
/x exch def
imageString imageRow x add patternRowString putinterval
} for
} for
imageString
end
} dup 0 12 dict put def

/min {
dup 3 2 roll dup 4 3 roll lt { exch } if pop
} def

/max {
dup 3 2 roll dup 4 3 roll gt { exch } if pop
} def

/midpoint {
0 begin
/y1 exch def
/x1 exch def
/y0 exch def
/x0 exch def
x0 x1 add 2 div
y0 y1 add 2 div
end
} dup 0 4 dict put def

/thirdpoint {
0 begin
/y1 exch def
/x1 exch def
/y0 exch def
/x0 exch def
x0 2 mul x1 add 3 div
y0 2 mul y1 add 3 div
end
} dup 0 4 dict put def

/subspline {
0 begin
/movetoNeeded exch def
y exch get /y3 exch def
x exch get /x3 exch def
y exch get /y2 exch def
x exch get /x2 exch def
y exch get /y1 exch def
x exch get /x1 exch def
y exch get /y0 exch def
x exch get /x0 exch def
x1 y1 x2 y2 thirdpoint
/p1y exch def
/p1x exch def
x2 y2 x1 y1 thirdpoint
/p2y exch def
/p2x exch def
x1 y1 x0 y0 thirdpoint
p1x p1y midpoint
/p0y exch def
/p0x exch def
x2 y2 x3 y3 thirdpoint
p2x p2y midpoint
/p3y exch def
/p3x exch def
movetoNeeded { p0x p0y moveto } if
p1x p1y p2x p2y p3x p3y curveto
end
} dup 0 17 dict put def

/storexyn {
/n exch def
/y n array def
/x n array def
n 1 sub -1 0 {
/i exch def
y i 3 2 roll put
x i 3 2 roll put
} for
} def

/SSten {
fgred fggreen fgblue setrgbcolor
dup true exch 1 0 0 -1 0 6 -1 roll matrix astore
} def

/FSten {
dup 3 -1 roll dup 4 1 roll exch
newpath
0 0 moveto
dup 0 exch lineto
exch dup 3 1 roll exch lineto
0 lineto
closepath
bgred bggreen bgblue setrgbcolor
eofill
SSten
} def

/Rast {
exch dup 3 1 roll 1 0 0 -1 0 6 -1 roll matrix astore
} def

%%EndProlog

%I Idraw 13 Grid 8 8

%%Page: 1 1

Begin
%I b u
%I cfg u
%I cbg u
%I f u
%I p u
%I t
[ 0.74759 0 0 0.74759 0 0 ] concat
/originalCTM matrix currentmatrix def

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 57 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -17 57 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -1 57 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 31 57 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 15 57 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 47 57 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 63 57 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 79 57 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
2 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 111 57 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 95 57 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 127 57 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 143 57 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 159 57 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 191 57 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 175 57 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 207 57 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 223 57 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 239 57 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 271 57 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 255 57 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 17 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -17 17 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -1 17 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 31 17 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 15 17 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 47 17 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
2 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 63 17 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 79 17 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 111 17 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 95 17 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 127 17 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 -23 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -17 -23 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -1 -23 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 31 -23 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
2 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 15 -23 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 47 -23 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 63 -23 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 79 -23 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 -63 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -17 -63 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -1 -63 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 31 -63 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 15 -63 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 47 -63 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 63 -63 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 79 -63 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 111 -63 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 95 -63 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 127 -63 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 143 -63 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 159 -63 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 175 -63 ] concat
%I
153 727 169 751 Rect
End

Begin %I Text
%I cfg Black
0 0 0 SetCFg
%I f -*-helvetica-medium-r-normal--18-*
Helvetica 18 SetF
%I t
[ 1 0 0 1 32 801 ] concat
%I
[
(positions)
] Text
End

Begin %I Text
%I cfg Black
0 0 0 SetCFg
%I f -*-helvetica-medium-r-normal--18-*
Helvetica 18 SetF
%I t
[ 1 0 0 1 42 761.5 ] concat
%I
[
(normals)
] Text
End

Begin %I Text
%I cfg Black
0 0 0 SetCFg
%I f -*-helvetica-medium-r-normal--18-*
Helvetica 18 SetF
%I t
[ 1 0 0 1 56 721 ] concat
%I
[
(colors)
] Text
End

Begin %I Text
%I cfg Black
0 0 0 SetCFg
%I f -*-helvetica-medium-r-normal--18-*
Helvetica 18 SetF
%I t
[ 1 0 0 1 48 692 ] concat
%I
[
(texture )
(coords)
] Text
End

Begin %I Pict
%I b u
%I cfg u
%I cbg u
%I f u
%I p u
%I t
[ 1 0 0 1 -64 32 ] concat

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 111 57 ] concat
%I
185 527 201 543 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 111 41 ] concat
%I
185 527 201 543 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 111 25 ] concat
%I
185 527 201 543 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 111 9 ] concat
%I
185 527 201 543 Rect
End

End %I eop

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 89 ] concat
%I
201 479 217 543 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -65 89 ] concat
%I
201 479 217 543 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -81 89 ] concat
%I
201 479 217 543 Rect
End

Begin %I Pict
%I b u
%I cfg u
%I cbg u
%I f u
%I p u
%I t
[ 1 0 0 1 -40 32 ] concat

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 39 57 ] concat
%I
201 479 217 543 Rect
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 57 ] concat
%I
273 527 289 527 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 57 ] concat
%I
273 511 289 511 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 57 ] concat
%I
273 495 289 495 Line
%I 1
End

End %I eop

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 89 ] concat
%I
153 527 169 527 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 89 ] concat
%I
153 511 169 511 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 89 ] concat
%I
153 495 169 495 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 89 ] concat
%I
169 495 185 495 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 89 ] concat
%I
169 511 185 511 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 89 ] concat
%I
169 527 185 527 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 89 ] concat
%I
201 527 217 527 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 89 ] concat
%I
209 511 217 511 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 89 ] concat
%I
209 511 201 511 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 89 ] concat
%I
201 495 217 495 Line
%I 1
End

Begin %I Pict
%I b u
%I cfg u
%I cbg u
%I f u
%I p u
%I t
[ 1 0 0 1 -24 32 ] concat

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 39 57 ] concat
%I
201 479 217 543 Rect
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 57 ] concat
%I
273 527 289 527 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 57 ] concat
%I
273 511 289 511 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 57 ] concat
%I
273 495 289 495 Line
%I 1
End

End %I eop

Begin %I Pict
%I b u
%I cfg u
%I cbg u
%I f u
%I p u
%I t
[ 1 0 0 1 -56 32 ] concat

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 39 57 ] concat
%I
201 479 217 543 Rect
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 57 ] concat
%I
273 527 289 527 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 57 ] concat
%I
273 511 289 511 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 57 ] concat
%I
273 495 289 495 Line
%I 1
End

End %I eop

Begin %I Pict
%I b u
%I cfg u
%I cbg u
%I f u
%I p u
%I t
[ 1 0 0 1 -88 32 ] concat

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 39 57 ] concat
%I
201 479 217 543 Rect
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 57 ] concat
%I
273 527 289 527 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 57 ] concat
%I
273 511 289 511 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 57 ] concat
%I
273 495 289 495 Line
%I 1
End

End %I eop

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 95 89 ] concat
%I
201 479 217 543 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 63 89 ] concat
%I
201 479 217 543 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 47 89 ] concat
%I
201 479 217 543 Rect
End

Begin %I Pict
%I b u
%I cfg u
%I cbg u
%I f u
%I p u
%I t
[ 1 0 0 1 88 32 ] concat

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 39 57 ] concat
%I
201 479 217 543 Rect
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 57 ] concat
%I
273 527 289 527 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 57 ] concat
%I
273 511 289 511 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 57 ] concat
%I
273 495 289 495 Line
%I 1
End

End %I eop

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 95 89 ] concat
%I
153 527 169 527 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 95 89 ] concat
%I
153 511 169 511 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 95 89 ] concat
%I
153 495 169 495 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 95 89 ] concat
%I
169 495 185 495 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 95 89 ] concat
%I
169 511 185 511 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 95 89 ] concat
%I
169 527 185 527 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 95 89 ] concat
%I
201 527 217 527 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 95 89 ] concat
%I
209 511 217 511 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 95 89 ] concat
%I
209 511 201 511 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 95 89 ] concat
%I
201 495 217 495 Line
%I 1
End

Begin %I Pict
%I b u
%I cfg u
%I cbg u
%I f u
%I p u
%I t
[ 1 0 0 1 104 32 ] concat

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 39 57 ] concat
%I
201 479 217 543 Rect
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 57 ] concat
%I
273 527 289 527 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 57 ] concat
%I
273 511 289 511 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 57 ] concat
%I
273 495 289 495 Line
%I 1
End

End %I eop

Begin %I Pict
%I b u
%I cfg u
%I cbg u
%I f u
%I p u
%I t
[ 1 0 0 1 72 32 ] concat

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 39 57 ] concat
%I
201 479 217 543 Rect
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 57 ] concat
%I
273 527 289 527 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 57 ] concat
%I
273 511 289 511 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 57 ] concat
%I
273 495 289 495 Line
%I 1
End

End %I eop

Begin %I Pict
%I b u
%I cfg u
%I cbg u
%I f u
%I p u
%I t
[ 1 0 0 1 40 32 ] concat

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 39 57 ] concat
%I
201 479 217 543 Rect
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 57 ] concat
%I
273 527 289 527 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 57 ] concat
%I
273 511 289 511 Line
%I 1
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 57 ] concat
%I
273 495 289 495 Line
%I 1
End

End %I eop

Begin %I Text
%I cfg Black
0 0 0 SetCFg
%I f -*-helvetica-medium-r-normal--18-*
Helvetica 18 SetF
%I t
[ 1 0 0 1 40 609 ] concat
%I
[
(vertices)
] Text
End

Begin %I Text
%I cfg Black
0 0 0 SetCFg
%I f -*-helvetica-medium-r-normal--14-*
Helvetica 14 SetF
%I t
[ 1 0 0 1 235 581 ] concat
%I
[
(-1)
] Text
End

Begin %I Elli
%I b 65535
2 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 0.5 -0 -0 0.5 143 369.5 ] concat
%I
193 446 3 3 Elli
End

Begin %I Elli
%I b 65535
2 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 0.5 -0 -0 0.5 144 401 ] concat
%I
193 446 3 3 Elli
End

Begin %I Elli
%I b 65535
2 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 0.5 -0 -0 0.5 143.5 385 ] concat
%I
193 446 3 3 Elli
End

Begin %I BSpl
%I b 65535
1 0 1 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
%I p
0 SetP
%I t
[ 0.25 -0 -0 0.25 134.25 529 ] concat
%I 6
423 380
487 380
679 412
807 796
673 1058
553 1064
6 BSpl
%I 4
End

Begin %I BSpl
%I b 65535
1 0 1 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
%I p
0 SetP
%I t
[ 0.25 -0 -0 0.25 134.25 529 ] concat
%I 5
423 316
647 348
647 732
519 860
361 904
5 BSpl
%I 4
End

Begin %I BSpl
%I b 65535
1 0 1 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
%I p
0 SetP
%I t
[ 0.25 -0 -0 0.25 134.25 529 ] concat
%I 6
423 252
487 252
743 412
551 636
327 700
169 744
6 BSpl
%I 4
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -33 -215 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -17 -215 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 -1 -215 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 31 -215 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 15 -215 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 1 -0 -0 1 47 -215 ] concat
%I
153 727 169 751 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 0.5 -0 -0 0.5 23.5 411 ] concat
%I
193 122 449 170 Rect
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 0.5 -0 -0 0.5 23.5 411 ] concat
%I
193 42 289 90 Rect
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 0.5 -0 -0 0.5 23.5 411 ] concat
%I
257 170 257 122 Line
%I 2
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 0.5 -0 -0 0.5 23.5 411 ] concat
%I
321 170 321 122 Line
%I 2
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 0.5 -0 -0 0.5 23.5 411 ] concat
%I
385 170 385 122 Line
%I 2
End

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 0.5 -0 -0 0.5 71.5 411 ] concat
%I
193 42 289 90 Rect
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 0.5 -0 -0 0.5 23.5 411 ] concat
%I
225 170 225 122 Line
%I 2
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 0.5 -0 -0 0.5 23.5 411 ] concat
%I
289 170 289 122 Line
%I 2
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 0.5 -0 -0 0.5 23.5 411 ] concat
%I
353 170 353 122 Line
%I 2
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 0.5 -0 -0 0.5 23.5 411 ] concat
%I
417 170 417 122 Line
%I 2
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 0.5 -0 -0 0.5 23.5 411 ] concat
%I
225 74 225 90 Line
%I 2
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 0.5 -0 -0 0.5 23.5 411 ] concat
%I
225 90 225 42 Line
%I 2
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 0.5 -0 -0 0.5 23.5 411 ] concat
%I
257 90 257 42 Line
%I 2
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 0.5 -0 -0 0.5 23.5 411 ] concat
%I
321 90 321 42 Line
%I 2
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 0.5 -0 -0 0.5 23.5 411 ] concat
%I
353 90 353 42 Line
%I 2
End

Begin %I Pict
%I b u
%I cfg u
%I cbg u
%I f u
%I p u
%I t
[ 1 0 0 1 40 -8 ] concat

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 0.5 -0 -0 0.5 79.5 419 ] concat
%I
193 42 289 90 Rect
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 0.5 -0 -0 0.5 31.5 419 ] concat
%I
321 90 321 42 Line
%I 2
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 0.5 -0 -0 0.5 31.5 419 ] concat
%I
353 90 353 42 Line
%I 2
End

End %I eop

Begin %I Pict
%I b u
%I cfg u
%I cbg u
%I f u
%I p u
%I t
[ 1 0 0 1 88 -8 ] concat

Begin %I Rect
%I b 65535
1 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 0.5 -0 -0 0.5 79.5 419 ] concat
%I
193 42 289 90 Rect
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 0.5 -0 -0 0.5 31.5 419 ] concat
%I
321 90 321 42 Line
%I 2
End

Begin %I Line
%I b 65535
1 0 0 [] 0 SetB
%I cfg LtGray
0.762951 0.762951 0.762951 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 0.5 -0 -0 0.5 31.5 419 ] concat
%I
353 90 353 42 Line
%I 2
End

End %I eop

Begin %I Rect
%I b 65535
2 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 0.5 -0 -0 0.5 23.5 411 ] concat
%I
417 314 449 442 Rect
End

Begin %I Rect
%I b 65535
2 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 0.5 -0 -0 0.5 23.5 411 ] concat
%I
321 202 353 250 Rect
End

Begin %I Rect
%I b 65535
2 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 0.5 -0 -0 0.5 23.5 411 ] concat
%I
385 122 449 170 Rect
End

Begin %I Rect
%I b 65535
2 0 0 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
none SetP %I p n
%I t
[ 0.5 -0 -0 0.5 23.5 411 ] concat
%I
481 42 577 90 Rect
End

Begin %I BSpl
%I b 65535
1 0 1 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
%I p
0 SetP
%I t
[ 0.25 -0 -0 0.25 108.75 422.5 ] concat
%I 4
335 400
219 456
201 522
205 577
4 BSpl
%I 4
End

Begin %I BSpl
%I b 65535
1 0 1 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
%I p
0 SetP
%I t
[ 0.25 -0 -0 0.25 108.75 422.5 ] concat
%I 5
779 84
883 203
928 347
906 518
845 579
5 BSpl
%I 4
End

Begin %I BSpl
%I b 65535
1 0 1 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
%I p
0 SetP
%I t
[ 0.25 -0 -0 0.25 108.75 422.5 ] concat
%I 4
718 86
820 257
834 473
782 579
4 BSpl
%I 4
End

Begin %I BSpl
%I b 65535
1 0 1 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
%I p
0 SetP
%I t
[ 0.25 -0 -0 0.25 108.75 422.5 ] concat
%I 4
523 246
667 328
752 447
783 577
4 BSpl
%I 4
End

Begin %I BSpl
%I b 65535
1 0 1 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
%I p
0 SetP
%I t
[ 0.25 -0 -0 0.25 108.75 422.5 ] concat
%I 4
653 87
752 261
720 499
658 579
4 BSpl
%I 4
End

Begin %I BSpl
%I b 65535
1 0 1 [] 0 SetB
%I cfg Black
0 0 0 SetCFg
%I cbg White
1 1 1 SetCBg
%I p
0 SetP
%I t
[ 0.25 -0 -0 0.25 108.75 422.5 ] concat
%I 4
463 244
577 338
663 434
658 575
4 BSpl
%I 4
End

Begin %I Text
%I cfg Black
0 0 0 SetCFg
%I f -*-helvetica-medium-r-normal--18-*
Helvetica 18 SetF
%I t
[ 1 0 0 1 54.5 530.5 ] concat
%I
[
(points)
] Text
End

Begin %I Text
%I cfg Black
0 0 0 SetCFg
%I f -*-helvetica-medium-r-normal--18-*
Helvetica 18 SetF
%I t
[ 1 0 0 1 66.5 491 ] concat
%I
[
(lines)
] Text
End

Begin %I Text
%I cfg Black
0 0 0 SetCFg
%I f -*-helvetica-medium-r-normal--18-*
Helvetica 18 SetF
%I t
[ 1 0 0 1 35.5 452.5 ] concat
%I
[
(triangles)
] Text
End

End %I eop

showpage

%%Trailer

end


text:
module Graphics.Rendering.Gl

import Data.Fin
import Graphics.Util.Mesh
import Graphics.Util.Transforms
import public Graphics.Rendering.Gl.Types
import public Graphics.Rendering.Gl.Buffers
import public Graphics.Rendering.Gl.Gl41
import Data.Matrix
import Data.Vect
import Control.Algebra

%include C "GL/glew.h"
%include C "gl_idris.h"
%link C "gl_idris.o"

%access public export

-- GLEW

||| initialises the GL function pointers
export
glewInit : IO Int
glewInit = foreign FFI_C "idr_init_glew" (IO Int)

-- ----------------------------------------------------------------- [ Helpers ]

||| upload a list of doubles to the GPU into an array buffer
export
loadDoubleData : BufferUsageARB -> List Double -> IO ()
loadDoubleData usage data' = do
  ds <- sizeofDouble
  ptr <- doublesToBuffer data'
  glBufferData GL_ARRAY_BUFFER (ds * (cast $ length data')) ptr usage
  free ptr
  pure ()

toList' : Vect n (Vect m a) -> List a
toList' [] = []
toList' (x :: xs) = (toList x) ++ toList' xs

-- ----------------------------------------------------------------- [ Simple API ]

||| location of a texture on the GPU
export
record Texture where
  constructor MkTexture
  textureLocation: Int

||| locations of a shading program
export
record Shader where
  constructor MkShader
  ||| location of the shader program
  program: Int
  ||| locations of all shaders for this program. minimum of two shaders is required (vertex and fragment shader)
  shaders: Vect (S (S n)) Int

||| create a shader from a pair of a shader type an a string containing the shader source
createShader : (GLenum, String) -> IO Int
createShader (shaderType, shaderSource) = do
  shaderLoc <- glCreateShader shaderType
  glShaderSource shaderLoc 1 [shaderSource] [(cast $ length shaderSource)]
  glCompileShader shaderLoc
  pure shaderLoc

||| creates and returns a shader program
||| @ shaderSpec a list of pairs of shader type and shader source
export
createShaders : (shaderSpec: Vect (S (S n)) (GLenum, String)) -> IO Shader
createShaders shaderSpec = do
  locs <- traverse createShader shaderSpec
  programLoc <- glCreateProgram
  traverse (glAttachShader programLoc) locs
  glLinkProgram programLoc
  glUseProgram 0
  pure $ MkShader programLoc locs

||| deletes the shader program
export
deleteShaders : Shader -> IO ()
deleteShaders (MkShader programLoc shaderLocs) = do
  glUseProgram 0
  traverse (glDetachShader programLoc) shaderLocs
  traverse glDeleteShader shaderLocs
  glDeleteProgram programLoc
  pure ()

||| the model on the GPU
|||
||| the minumum information needed is the location of the vertex array object (VAO)
||| and the locations of the vertex buffer objects (VBO)
||| textures are optional
export
data Model : Type where
  ||| creates a textured model
  ||| @ vao the location of the vertex array object
  ||| @ vbos the locations of the vertex buffer objects
  ||| @ indices the number of indices
  ||| @ textures locations of the textures for the model
  TexturedModel : (vao: Int) ->
                  (vbos: Vect (S n) Int) ->
                  (indices: Int) ->
                  (textures: Vect m Texture) -> Model

||| creates a model from a mesh and some texture locations
||| @ m the mesh. should be uv unwrapped
||| @ textures texture locations we need to bind when using the model
export
createModel : (m: Mesh) -> (textures: (Vect n Texture)) -> IO Model
createModel (UvMesh positions normals uvs indices) textures = do
  (vaoLoc :: _) <- glGenVertexArrays 1

  glBindVertexArray vaoLoc
  (positionBuffer :: normalBuffer :: uvBuffer :: indexBuffer :: _) <- glGenBuffers 4

  glBindBuffer GL_ARRAY_BUFFER positionBuffer
  loadDoubleData GL_STATIC_DRAW (toList' positions)
  glEnableVertexAttribArray 0
  glVertexAttribPointer 0 3 GL_DOUBLE GL_FALSE 0 prim__null

  glBindBuffer GL_ARRAY_BUFFER normalBuffer
  loadDoubleData GL_STATIC_DRAW (toList' normals)
  glEnableVertexAttribArray 1
  glVertexAttribPointer 1 3 GL_DOUBLE GL_FALSE 0 prim__null

  glBindBuffer GL_ARRAY_BUFFER uvBuffer
  loadDoubleData GL_STATIC_DRAW (toList' uvs)
  glEnableVertexAttribArray 2
  glVertexAttribPointer 2 2 GL_DOUBLE GL_FALSE 0 prim__null

  is <- sizeofInt
  glBindBuffer GL_ELEMENT_ARRAY_BUFFER indexBuffer
  ptr <- intsToBuffer indices
  glBufferData GL_ELEMENT_ARRAY_BUFFER (is * (cast $ length indices)) ptr GL_STATIC_DRAW
  free ptr

  glDisableVertexAttribArray 2 -- uvs
  glDisableVertexAttribArray 1 -- normals
  glDisableVertexAttribArray 0 -- positions

  glBindVertexArray 0

  pure $ TexturedModel vaoLoc [positionBuffer, normalBuffer, uvBuffer, indexBuffer] (cast $ length indices) textures

export
deleteModel : Model -> IO ()
deleteModel (TexturedModel vao vbos _ _) = do
  glDisableVertexAttribArray 2 -- uvs
  glDisableVertexAttribArray 1 -- normals
  glDisableVertexAttribArray 0 -- positions

  glBindBuffer GL_ARRAY_BUFFER 0
  glBindBuffer GL_ELEMENT_ARRAY_BUFFER 0

  glDeleteBuffers (cast $ length vbos) $ toList vbos

  glBindVertexArray 0

  glDeleteVertexArrays 1 [vao]
  pure ()

||| data type for entities.
||| an entity is like an instance of a model. it consists of the model an instance
||| specific data like location, rotation, etc.
|||
export
data Entity : Type -> Type where
  ||| a simple entity: model, shader, texture and instance data
  ||| @ model the model ('class') of the entity
  ||| @ shader shader program to use
  ||| @ position 3D position of the entity
  ||| @ rotation 3D rotation of the entity
  ||| @ location uniform location of the transform matrix in the shader program
  ||| @ val arbtitrary data
  SimpleEntity :  (model: Model)
               -> (shader: Shader)
               -> (position: Vec3)
               -> (rotation: Vect 3 Angle)
               -> (location: Int)
               -> (val: a)
               -> Entity a

export
render : Entity a -> (prepare: a -> IO ()) -> IO ()
render (SimpleEntity (TexturedModel vao _ numIndices textures) (MkShader prog _) entityPosition rotation location val) prepare = do
  glBindVertexArray vao
  glEnableVertexAttribArray 0
  glEnableVertexAttribArray 1
  glEnableVertexAttribArray 2

  glUseProgram prog

  prepare val

  traverse (\t => glBindTexture GL_TEXTURE_2D (textureLocation t)) textures

  glDrawElements GL_TRIANGLES numIndices GL_UNSIGNED_INT prim__null

  glDisableVertexAttribArray 2 -- uvs
  glDisableVertexAttribArray 1 -- normals
  glDisableVertexAttribArray 0 -- positions

  glBindVertexArray 0
  pure ()

||| load a png file to the currently bound texture
export
glLoadPNGTexture : Int -> Int -> String -> IO Int
glLoadPNGTexture target level filename = foreign FFI_C "png_texture" (Int -> Int -> String -> IO Int) target level filename

export
loadTexture : String -> Fin 30 -> IO Texture
loadTexture filename index = do
  putStrLn $ "Loading " ++ filename ++ " to texture unit " ++ (show $ finToNat index)
  glActiveTexture (GL_TEXTURE0 + (cast $ finToNat index))
  (texture :: _) <- glGenTextures 1
  glBindTexture GL_TEXTURE_2D texture

  ret <- glLoadPNGTexture (toGlInt Graphics.Rendering.Gl.GL41.TextureTarget.GL_TEXTURE_2D) 0 filename

  -- the texture is bound ... so we can set some params
  glTexParameteri GL_TEXTURE_2D GL_TEXTURE_WRAP_S GL_CLAMP_TO_EDGE
  glTexParameteri GL_TEXTURE_2D GL_TEXTURE_WRAP_T GL_CLAMP_TO_EDGE
  glTexParameteri GL_TEXTURE_2D GL_TEXTURE_MIN_FILTER GL_LINEAR
  glTexParameteri GL_TEXTURE_2D GL_TEXTURE_MAG_FILTER GL_LINEAR
  pure $ MkTexture texture

export
deleteTextures : List Texture -> IO ()
deleteTextures xs = glDeleteTextures (cast $ length xs) $ map textureLocation xs

-- ----------------------------------------------------------------- [ Helper ]

export
printShaderLog : Int -> IO ()
printShaderLog id = foreign FFI_C "printShaderLog" (Int -> IO()) id

export
glGetInfo : IO String
glGetInfo = do vendor   <- glGetString GL_VENDOR
               renderer <- glGetString GL_RENDERER
               version  <- glGetString GL_VERSION
               pure $ foldl1 (++) (the (List String) ["Vendor = ", vendor, "\nRenderer = ", renderer, "\nVersion = ", version, "\n"])

max_stars_repo_name: xiphiness/gl-idris

max_issues_repo_name: xiphiness/gl-idris

max_forks_repo_name: xiphiness/gl-idris


text:
module Test

import Mult

thing : Nat -> Nat
thing x = mult x (plus x x)


text:
module Examples

import Linear.Equality
import Linear.Types
import Data.Fin
import Data.Nat
import QPF
import QCont

-- Example 12
namespace ListAsQCont

  ListCont : Type -> Type
  ListCont = F Nat Fin

  MaybeCont : Type -> Type
  MaybeCont = F Bool (\b => if b then I else Fin 0)

  Just : x -<> MaybeCont x
  Just x = True # (\Star => x)

  Nothing : (Fin 0 -<> x) -<> MaybeCont x
  Nothing f = False # f

  head : ListCont x -<> MaybeCont x
  head (0 # f) = Nothing f
  head (S n # f) = Just (f 0)

-- Example 21
namespace NatAsQPF

  NatF : Desc
  NatF = Sum' (Const' I) Id'

  N : Type
  N = W NatF

  Zero : N
  Zero = Con (Inl Star)

  Suc : N -> N
  Suc n = Con (Inr n)

  elim : (0 p : N -> Type) -> p Zero -> ((0 n : N) -> p n -<> p (Suc n)) ->
         (1 n : N) -> p n
  elim p p0 ps = induction {p = p} f where
    f : (1 w : Sigma0 (qpf NatF N) (lift NatF p)) -> p (Con (fst w))
    f (_ # (Inl (Star # (Refl # (Star # Refl))))) = p0
    f (_ # (Inr (b # (Refl # ih)))) = ps b ih

-- Example 22
namespace BinTreeAsQPF
  parameters (a : Type)

    BtF : Desc
    BtF = Sum' (Const' a) (Prod' Id' Id')

    Tree : Type
    Tree = W BtF

    Leaf : a -<> Tree
    Leaf x = Con (Inl x)

    Node : Tree -<> Tree -<> Tree
    Node l r = Con (Inr (l # r))

    elim : (0 p : Tree -> Type) ->
           (pl : (1 x : a) -> p (Leaf x)) ->
           (pn : (0 l : Tree) -> (0 r : Tree) -> p l -<> p r -<> p (Node l r)) ->
           (1 t : Tree) -> p t
    elim p pl pn = induction {p = p} f where
      f : (1 w : Sigma0 (qpf BtF Tree) (lift BtF p)) -> p (Con (fst w))
      f (_ # Inl (x # (Refl # (x # Refl)))) = pl x
      f (x # Inr (w # (q # (ihl # ihr)))) = replace1 (\ y => p (Con y)) (eq x w q) (pn _ _ ihl ihr)
        where
        eq : (0 x : Sum a (LPair (W (Sum' (Const' a) (Prod' Id' Id'))) (W (Sum' (Const' a) (Prod' Id' Id'))))) ->
             (0 w : LPair (W (Sum' (Const' a) (Prod' Id' Id'))) (W (Sum' (Const' a) (Prod' Id' Id')))) ->
             (1 q : x = Inr w) -> Inr (fst w # snd w) = x
        eq (Inr (w1 # w2)) (w1 # w2) Refl = Refl

max_stars_repo_name: g-nakov/quantitative-poly

max_issues_repo_name: g-nakov/quantitative-poly

max_forks_repo_name: g-nakov/quantitative-poly


text:
||| Spec: https://webassembly.github.io/spec/core/syntax/values.html#floating-point
module WebAssembly.Structure.Values.FloatingPoint

import Decidable.Equality

-- Definition

||| Unsigned Integer 32 Bit
||| Notice: WebAssembly's 32-bit floats are over-approximated by Idris' (64-bit) doubles
public export
F32 : Type
F32 = Double

||| Signed Interer 32 Bit
public export
F64 : Type
F64 = Double

-- Equality

||| Decidable syntactic equality
||| Usage: decEq @{F32DecEq} a b
public export
[F32DecEq] DecEq F32 where
  decEq x y =
    case x == y of -- Blocks if x or y not concrete
      True => Yes primitiveEq
      False => No primitiveNotEq
    where
      primitiveEq : x = y
      primitiveEq = believe_me (Refl {x})
      primitiveNotEq : x = y -> Void
      primitiveNotEq prf = believe_me {b = Void} ()

||| Decidable syntactic equality
||| Usage: decEq @{F64DecEq} a b
public export
[F64DecEq] DecEq F64 where
  decEq x y =
    case x == y of -- Blocks if x or y not concrete
      True => Yes primitiveEq
      False => No primitiveNotEq
    where
      primitiveEq : x = y
      primitiveEq = believe_me (Refl {x})
      primitiveNotEq : x = y -> Void
      primitiveNotEq prf = believe_me {b = Void} ()

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
module ParserCombinator

%access public export

record Pos where
    constructor MkPos
    line, column : Int

Show Pos where
    show (MkPos line col) = "(line " ++ (show line) ++ ", column " ++ (show col) ++ ")"

data Error = MkError String

Show Error where
    show (MkError err) = err

data ParseResult a = ParseError Error String Pos | ParseSuccess a String Pos

Show a => Show (ParseResult a) where
    show (ParseError err _ pos) = "Error " ++ (show pos) ++ ": " ++ (show err)
    show (ParseSuccess a _ _) = show a

data Parser : Type -> Type where
    MkParser : (String -> Pos -> ParseResult a) -> Parser a

parse' : Parser a -> String -> Pos -> ParseResult a
parse' (MkParser p) inp pos = p inp pos

Functor Parser where
    map f m1 = MkParser $ \inp, pos =>
        case parse' m1 inp pos of
            ParseError err s2 pos => ParseError err s2 pos
            ParseSuccess a rest pos => ParseSuccess (f a) rest pos

mutual
    Applicative Parser where
        pure a = MkParser $ \inp, pos => ParseSuccess a inp pos
        af <*> ax = do
            f <- af
            x <- ax
            pure (f x)

    Monad Parser where
        p >>= f = MkParser $ \inp, pos =>
            case parse' p inp pos of
                ParseError err _ pos' => ParseError err inp pos'
                ParseSuccess a rest pos' => parse' (f a) rest pos'

failure : String -> Parser a
failure err = MkParser $ \inp, pos => ParseError (MkError err) inp pos

-- TODO: USE THIS!
-- TODO: RENAME PROBABLY!
failWith : String -> Parser a -> Parser a
failWith err p =
    MkParser $ \inp, pos =>
        case parse' p inp pos of
            ParseError _ inp' pos' => ParseError (MkError err) inp' pos'
            ok@(ParseSuccess _ _ _) => ok

nextPos : Char -> Pos -> Pos
nextPos c pos =
    if c == '\n'
    then record { line $= (+ 1), column $= (const 0) } pos
    else record { column $= (+ 1) } pos

item : Parser Char
item =
    MkParser $ \inp, pos =>
        case inp of
            "" => ParseError (MkError "'Item' run on empty input") "" pos
            s =>
                let c = (strHead s)
                in ParseSuccess c (strTail s) (nextPos c pos)

(<|>) : Parser a -> Parser a -> Parser a
p <|> q =
    MkParser $ \inp, pos =>
        case parse' p inp pos of
            ParseError _ _ _ => parse' q inp pos
            ParseSuccess a rest pos' => ParseSuccess a rest pos'

mutual
    many1 : Parser a -> Parser (List a)
    many1 p = do
        v <- p
        vs <- many' p
        pure (v :: vs)

    many' : Parser a -> Parser (List a)
    many' p = many1 p <|> pure []

skipMany : Parser a -> Parser ()
skipMany p = do
    many' p
    pure ()

skipMany1 : Parser a -> Parser ()
skipMany1 p = do
    many1 p
    pure ()

skipUntil : Parser t -> Parser a -> Parser ()
skipUntil end p = scan
    where
    scan =
        do end
           pure ()
        <|>
        do p
           scan
           pure ()

try : Parser a -> Parser a
try p =
    MkParser $ \inp, pos =>
        case parse' p inp pos of
            ParseError err _ pos' => ParseError err inp pos'
            ParseSuccess a rest pos' => ParseSuccess a rest pos'

sat : (Char -> Bool) -> Parser Char
sat p = do
    x <- item
    if p x
    then pure x
    else failure $ "Condition not satisfied for: `" ++ (singleton x) ++ "`"

rej : (Char -> Bool) -> Parser Char
rej p = do
    x <- item
    if not (p x)
    then pure x
    else failure $ "Rejection condition not satisfied for: `" ++ (singleton x) ++ "`"

char : Char -> Parser Char
char x = sat (== x)

oneOf : String -> Parser Char
oneOf "" = item *> failure "Empty input to 'OneOf'"
oneOf s = (try (char (strHead s))) <|> oneOf (strTail s)

noneOf : String -> Parser Char
noneOf s =
    do
        c <- item
        go c s
    where
        go c "" = pure c
        go c s = do
            if c == strHead s
            then failure $ "Rejection condition not satisfied for: `" ++ (singleton c) ++ "`"
            else go c (strTail s)

sepBy : Parser a -> Parser b -> Parser (List a)
sepBy p sep = separated <|> pure []
    where
        separated = do
            x <- p
            xs <- many' (sep *> p)
            pure (x :: xs)

endBy : Parser a -> Parser b -> Parser (List a)
endBy p sep =
  many' $ do
    x <- p
    sep
    pure x

digit : Parser Char
digit = sat isDigit

hexDigit : Parser Char
hexDigit = digit <|> oneOf "ABCDEFabcdef"

octDigit : Parser Char
octDigit = oneOf "01234567"

binDigit : Parser Char
binDigit = oneOf "01"

lower : Parser Char
lower = sat isLower

upper : Parser Char
upper = sat isUpper

letter : Parser Char
letter = sat isAlpha

alphanum : Parser Char
alphanum = sat isAlphaNum

space : Parser Char
space = sat isSpace

spaces : Parser ()
spaces = skipMany1 space

string : String -> Parser String
string "" = pure ""
string s = do
    char (strHead s)
    string (strTail s)
    pure s

eof : Parser ()
eof = MkParser $ \inp, pos =>
    case inp of
        "" => ParseSuccess () inp pos
        s => ParseError (MkError "Not end of file") s (nextPos (strHead s) pos)

parse : Parser a -> String -> ParseResult a
parse p inp = parse' p inp (MkPos 1 0)

max_stars_repo_name: ebenpack/lidrisp

max_issues_repo_name: ebenpack/lidrisp

max_forks_repo_name: ebenpack/lidrisp


text:
-- ------------------------------------------------------------ [ Abstract.idr ]
-- Module    : Abstract.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]

||| TODO List using abstract interpretation
module GRL.Test.DSML.OldTODO

import GRL.Lang.GLang

||| Specify Task.
data Task : (GLang ELEM) -> Type where
  MkTask : (t:String) -> Task (mkGoal t)
  MkSub  : (t:String) -> Task (mkGoal t)

||| Specify action
data Action : (GLang ELEM) -> Type where
  MkAction : (t:String) -> (s:SValue)
          -> Action (mkSatTask t s)

||| Specify task relation.
data ActsOn : (GLang INTENT) -> Type where
  MkActsOn : (c : CValue) -> Action x -> Task y
          -> ActsOn (mkImpacts c x y)

||| Specify sub task
data HasSubTask : (GLang STRUCT) -> Type where
  LinkTasks : Task x -> Task y
           -> HasSubTask (mkAnd x [y])

||| The todo list
data TODO : GModel -> Type where
  MkList : DList (GLang ELEM)   (\x => Task       x) es
        -> DList (GLang ELEM)   (\x => Action     x) as
        -> DList (GLang INTENT) (\x => ActsOn     x) is
        -> DList (GLang STRUCT) (\x => HasSubTask x) ss
        -> TODO (insertMany ss $ insertMany is $ insertMany as $ insertMany es emptyModel)

-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: jfdm/idris-grl

max_issues_repo_name: jfdm/idris-grl

max_forks_repo_name: jfdm/idris-grl


text:
data Bar = MkBar
data Baz = MkBaz

strangeId : a -> a
strangeId {a=Nat} x = x+1
strangeId x = x

foo : (0 x : Type) -> String
foo Nat = "Nat"
foo Bool = "Bool"
foo (List x) = "List of " ++ foo x
foo Int = "Int"
foo Type = "Type"
foo _ = "Something else"


text:
import Data.List1
import Data.Nat
import Data.String.Parser

import System.File

data SnailfishNum = Regular Nat | Pair SnailfishNum SnailfishNum

Show SnailfishNum where
  show (Regular k) = show k
  show (Pair x y) = "[" ++ show x ++ "," ++ show y ++ "]"

data ReduceResult = None | Done | Add Nat Nat | AddL Nat | AddR Nat

Input : Type
Input = List1 SnailfishNum

pairParser : Parser a -> Parser (a, a)
pairParser p = do fst <- p
                  skip $ char ','
                  snd <- p
                  pure (fst, snd)

numParser : Parser SnailfishNum
numParser = (char '[' *> (uncurry Pair <$> pairParser numParser) <* char ']') <|>
            Regular <$> natural

parser : Parser Input
parser = do Just l <- fromList <$> some (numParser <* spaces)
              | Nothing => fail "empty list"
            pure l

reduce : SnailfishNum -> SnailfishNum
reduce n = case explode 0 n of
                (r, None) => case split r of
                                  (r, True) => reduce r
                                  (r, False) => r
                (r, _   ) => reduce r
  where
    split : SnailfishNum -> (SnailfishNum, Bool)
    split (Regular k) =
      if k > 9
         then (Pair (Regular $ divNatNZ k 2 SIsNonZero) (Regular $ divCeilNZ k 2 SIsNonZero), True)
         else (Regular k, False)
    split (Pair x y) = case split x of
                            (z, True) => (Pair z y, True)
                            (z, False) => let (w, b) = split y in
                                              (Pair z w, b)

    addLeftMost : Nat -> SnailfishNum -> SnailfishNum
    addLeftMost n (Regular k) = Regular $ n + k
    addLeftMost n (Pair x y) = Pair (addLeftMost n x) y

    addRightMost : Nat -> SnailfishNum -> SnailfishNum
    addRightMost n (Regular k) = Regular $ n + k
    addRightMost n (Pair x y) = Pair x (addRightMost n y)

    explode : Nat -> SnailfishNum -> (SnailfishNum, ReduceResult)
    explode _ (Regular k) = (Regular k, None)
    explode 4 (Pair (Regular k) (Regular j)) = (Regular 0, Add k j)
    explode d (Pair x y) = case explode (min (d + 1) 4) x of
                                (z, Done) => (Pair z y, Done)
                                (z, (Add k j)) => (Pair z (addLeftMost j y), AddL k)
                                (z, (AddL k)) => (Pair z y, AddL k)
                                (z, (AddR j)) => (Pair z (addLeftMost j y), Done)
                                (z, None) => case explode (min (d + 1) 4) y of
                                                  (w, (Add k j)) => (Pair (addRightMost k z) w, AddR j)
                                                  (w, (AddL k)) => (Pair (addRightMost k z) w, Done)
                                                  (w, r) => (Pair z w, r)

add : SnailfishNum -> SnailfishNum -> SnailfishNum
add n1 n2 = reduce $ Pair n1 n2

magnitude : SnailfishNum -> Nat
magnitude (Regular n) = n
magnitude (Pair x y) = 3 * (magnitude x) + 2 * (magnitude y)

part1 : Input -> IO String
part1 = pure . show . magnitude . foldl1 add

part2 : Input -> IO String
part2 a = pure $ show $ foldl1 max $ (\n1 => foldl1 max $ (\n2 => (magnitude $ add n1 n2)) <$> a) <$> a

main : IO ()
main = do Right input <- readFile "input.txt"
            | Left err => printLn err
          Right (a, _) <- pure $ parse parser input
            | Left err => printLn err
          part1 a >>= putStrLn
          part2 a >>= putStrLn


text:
module FiniteMap

%default total
%access private

public export
interface FiniteMap (m : Type -> Type -> Type) k where
  empty : m k a
  bind : k -> a -> m k a -> m k a
  lookup : k -> m k a -> Maybe a


text:
module Data.List.Extras

import Data.List.Views

%default total
%access export

foldrM :  Monad m => (func : elem -> acc -> m acc) -> (init : acc) -> (input : List elem) -> m acc
foldrM func init input with (snocList input)
    foldrM _ init [] | Empty = pure init
    foldrM func init (xs ++ [x]) | Snoc rec = foldrM func !(func x init) xs | rec

mapM : Monad m => (func : elem -> m r) -> (input : List elem) -> m (List r)
mapM func = foldrM (\x, acc => liftA (:: acc) (func x)) []

max_stars_repo_name: jheiling/idris-extras

max_issues_repo_name: jheiling/idris-extras

max_forks_repo_name: jheiling/idris-extras


text:
module Linear

import public Linear.Epsilon
import public Linear.Metric
import public Linear.Vect

max_stars_repo_name: yurrriq/idris-linear

max_issues_repo_name: yurrriq/idris-linear

max_forks_repo_name: yurrriq/idris-linear


text:
-- ----------------------------------------------------------------- [ IOR.idr ]
-- Module    : IOR.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]

||| Testing IOR contribution evaluation
module GRL.Test.Decomposition

import GRL.Lang.GLang
import GRL.Eval

import GRL.Test.Utils

%default total

-- -------------------------------------------------------- [ Model Definition ]

conn : GOAL
conn = mkGoal "Connection"

lan : TASK
lan = mkTask "LAN"

wireless : TASK
wireless = mkTask "Wireless"

internet : TASK
internet = mkTask "Internet"

modelIOR : GModel
modelIOR = emptyModel
   \= conn \= lan \= wireless \= internet
   \= conn |= [lan,wireless,internet]

modelAND : GModel
modelAND = emptyModel
   \= conn \= lan \= wireless \= internet
   \= conn &= [lan,wireless,internet]

-- ---------------------------------------------------------- [ IOR Strategies ]

or_a : Strategy
or_a = buildStrategy [(lan, NONE), (wireless, WEAKSATIS), (internet, WEAKDEN)]

or_a' : Strategy
or_a' = buildStrategy [(conn,WEAKSATIS), (lan, NONE), (wireless, WEAKSATIS), (internet, WEAKDEN)]

or_b : Strategy
or_b = buildStrategy [(lan, WEAKDEN), (wireless, WEAKDEN), (internet, WEAKDEN)]

or_b' : Strategy
or_b' = buildStrategy [(conn,WEAKDEN), (lan, WEAKDEN), (wireless, WEAKDEN), (internet, WEAKDEN)]

or_c : Strategy
or_c = buildStrategy [(lan, CONFLICT), (wireless, WEAKSATIS), (internet, WEAKDEN)]

or_c' : Strategy
or_c' = buildStrategy [(conn,UNDECIDED), (lan, CONFLICT), (wireless, WEAKSATIS), (internet, WEAKDEN)]

or_d : Strategy
or_d = buildStrategy [(lan, CONFLICT), (wireless, SATISFIED), (internet, WEAKDEN)]

or_d' : Strategy
or_d' = buildStrategy [(conn,SATISFIED), (lan, CONFLICT), (wireless, SATISFIED), (internet, WEAKDEN)]

-- ---------------------------------------------------------- [ AND Strategies ]

and_a : Strategy
and_a = buildStrategy [(lan, NONE), (wireless, WEAKSATIS), (internet, WEAKDEN)]

and_a' : Strategy
and_a' = buildStrategy [(conn, WEAKDEN), (lan, NONE), (wireless, WEAKSATIS), (internet, WEAKDEN)]

and_b : Strategy
and_b = buildStrategy [(lan, SATISFIED), (wireless, SATISFIED), (internet, SATISFIED)]

and_b' : Strategy
and_b' = buildStrategy [(conn,SATISFIED), (lan, SATISFIED), (wireless, SATISFIED), (internet, SATISFIED)]

and_c : Strategy
and_c = buildStrategy [(lan, CONFLICT), (wireless, WEAKSATIS), (internet, WEAKDEN)]

and_c' : Strategy
and_c' = buildStrategy [(conn,UNDECIDED), (lan, CONFLICT), (wireless, WEAKSATIS), (internet, WEAKDEN)]

and_d : Strategy
and_d = buildStrategy [(lan, CONFLICT), (wireless, WEAKSATIS), (internet, DENIED)]

and_d' : Strategy
and_d' = buildStrategy [(conn,DENIED), (lan, CONFLICT), (wireless, WEAKSATIS), (internet, DENIED)]

-- -------------------------------------------------------------------- [ Test ]

export partial
runTest : IO ()
runTest = do
  putStrLn "--> Decomposition Tests"
  printLn $ True == and [ WEAKDEN   == getDecompAnd [WEAKDEN,WEAKSATIS,NONE]
                        , SATISFIED == getDecompAnd [SATISFIED,SATISFIED,SATISFIED]
                        , UNDECIDED == getDecompAnd [WEAKDEN,WEAKSATIS,CONFLICT]
                        , DENIED    == getDecompAnd [DENIED,WEAKSATIS,CONFLICT]
                        ]

  printLn $ True == and [ WEAKSATIS == getDecompIOR [WEAKDEN,WEAKSATIS,NONE]
                        , WEAKDEN   == getDecompIOR [WEAKDEN,WEAKDEN,WEAKDEN]
                        , UNDECIDED == getDecompIOR [WEAKDEN,WEAKSATIS,CONFLICT]
                        , SATISFIED == getDecompIOR [WEAKDEN,SATISFIED,CONFLICT]
                        ]

  putStrLn "--> IOR"

  putStrLn "Strategy A:"
  doTest modelIOR or_a or_a'

  putStrLn "Strategy B:"
  doTest modelIOR or_b or_b'

  putStrLn "Strategy C:"
  doTest modelIOR or_c or_c'

  putStrLn "Strategy D:"
  doTest modelIOR or_d or_d'

  putStrLn "--> AND"

  putStrLn "Strategy A:"
  doTest modelAND and_a and_a'

  putStrLn "Strategy B:"
  doTest modelAND and_b and_b'

  putStrLn "Strategy C:"
  doTest modelAND and_c and_c'

  putStrLn "Strategy D:"
  doTest modelAND and_d and_d'

-- --------------------------------------------------------------------- [ EOF ]


text:
module Example.Qtt.Zero

import Control.Monad.State

import Data.List
import Data.List.Quantifiers

import Data.Maybe

import Syntax.WithProof

%default total

-------------------------
--- Bounded arguments ---
-------------------------

namespace BoundedArgumentW

  total
  head : (l : List a) -> NonEmpty l => a
  head (x::_) = x

namespace BoundedArgumentW_auto

  total
  head : (l : List a) -> {auto _ : NonEmpty l} -> a
  head (x::_) = x

namespace BoundedArgument0_auto

  total
  head : (l : List a) -> {auto 0 _ : NonEmpty l} -> a
  head (x::_) = x

namespace BoundedArgument0

  total
  head : (l : List a) -> (0 _ : NonEmpty l) => a
  head (x::_) = x

------------------------------------
--- Meta-parameters in the "the" ---
------------------------------------

namespace TheUsage

  f : (MonadState Int m, MonadState Nat m, Monad m) => m Integer
  f = put (the Int 0) *> natToInteger <$> get

  Monad m => MonadState a (StateT (a, b) m) where
    get = Builtin.fst <$> get
    put x = put (x, !(snd <$> get))

  Monad m => MonadState b (StateT (a, b) m) where
    get = snd <$> get
    put x = put (!(Builtin.fst <$> get), x)

  f_mono : State (Int, Nat) Integer
  f_mono = f

  f_run : ((Int, Nat), Integer)
  f_run = runState (1, 2) f

---------------------------
--- Proof-carrying code ---
---------------------------

namespace SubsetAsLib

  data Subset : (type : Type)
             -> (pred : type -> Type)
             -> Type
    where
      Element : (value : type)
             -> (0 prf : pred value)
             -> Subset type pred

namespace SubsetAsRecord

  public export
  record Subset type pred where
    constructor Element
    value : type
    0 prf : pred value

namespace FiltersDPair

  filt : (p : a -> Bool) -> List a -> List (x : a ** p x = True)
  filt p [] = []
  filt p (x::xs) = case @@ p x of
    (True  ** prf) => (x ** prf) :: filt p xs
    (False ** _)   => filt p xs

namespace FiltersSubset

  filt : (p : a -> Bool) -> List a -> List $ Subset a (\x => p x = True)
  filt p [] = []
  filt p (x::xs) = case @@ p x of
    (True  ** prf) => Element x prf :: filt p xs
    (False ** _)   => filt p xs

-----------------------
--- Match on erased ---
-----------------------

pushIn : (xs : List a) -> (0 _ : All p xs) -> List $ Subset a p
pushIn []      []      = []
pushIn (x::xs) (p::ps) = Element x p :: pushIn xs ps

---------------------
--- Parametricity ---
---------------------

namespace WithoutAsq

  id : a -> a
  id x = x

namespace WithForall

  id : forall a. a -> a
  id x = x

namespace WithWType

  id : {a : Type} -> a -> a
  id x = x

  nonid : {a : Type} -> a -> a
  nonid {a=Int}    x = x + 1
  nonid {a=String} x = x ++ "a"
  nonid x = x

namespace With0Type

  id : {0 a : Type} -> a -> a
  id x = x

--------------------------------------
--- Need to not to have at runtime ---
--------------------------------------

namespace NotAtRuntime

  -- data Nat = Z | S Nat

  namespace Hiding

    data BNat : Nat -> Type where
      BZ : BNat 0
      B0 : BNat n -> BNat (2*n)
      B1 : BNat n -> BNat (1 + 2*n)

    (+) : BNat n -> BNat m -> BNat (n + m)

    toNat' : {n : Nat} -> BNat n -> Subset Nat (\k => k = n)
    toNat' x = Element n Refl

    toNat : BNat n -> Subset Nat (\k => k = n)
    toNat BZ     = Element 0 Refl
    toNat (B0 x) = let Element s prf = toNat x in
                   Element (2*s) rewrite prf in Refl
    toNat (B1 x) = let Element s prf = toNat x in
                   Element (1 + 2*s) rewrite prf in Refl

  namespace Exposing

    data BNat : Nat -> Type where
      BZ : BNat 0
      B0 : {n : Nat} -> BNat n -> BNat (2*n)
      B1 : {n : Nat} -> BNat n -> BNat (1 + 2*n)

    toNat : BNat n -> Subset Nat (\k => k = n)
    toNat BZ         = Element 0 Refl
    toNat (B0 {n} _) = Element (2*n) Refl
    toNat (B1 {n} _) = Element (1 + 2*n) Refl

max_stars_repo_name: buzden/code-in-lectures

max_issues_repo_name: buzden/code-in-lectures

max_forks_repo_name: buzden/code-in-lectures


text:
-- ----------------------------------------------------------- [ Chapter11.idr ]
-- Module      : Exercises.Chapter11
-- Description : Solutions to the Chapter 11 exercises in Edwin Brady's
--               book, "Type-Driven Development with Idris."
-- --------------------------------------------------------------------- [ EOH ]
module Exercises.Chapter11

import Data.Primitives.Views
import Test

%access  export
%default total

-- ------------------------------------------------------- [ Exercise 11.1.7.1 ]

everyOther : Stream a -> Stream a
everyOther (_ :: x :: xs) = x :: everyOther xs

-- ------------------------------------------------------ [ Exercises 11.1.7.2 ]

||| Generic infinite lists
data InfList : (elem : Type) -> Type where
  ||| An infinite list, consisting of a head element and an infinite list.
  (::) : (x : elem) -> (xs : Inf (InfList elem)) -> InfList elem

%name InfList xs, ys, zs

countFrom : Integer -> InfList Integer
countFrom x = x :: countFrom (x + 1)

getPrefix : (count : Nat) -> InfList a -> List a
getPrefix  Z    _  = []
getPrefix (S k) (x :: xs) = x :: getPrefix k xs

implementation Functor InfList where
  map f (x :: xs) = f x :: map f xs -- FIXME: Delay is implicit, right?

-- ------------------------------------------------------- [ Exercise 11.1.7.3 ]

randoms : Int -> Stream Int
randoms seed = let seed' = 1664525 * seed + 1013904223 in
                  (seed' `shiftR` 2) :: randoms seed'

{-
mutual
  even : Nat -> Bool
  even  Z    = True
  even (S k) = odd k

  odd : Nat -> Bool
  odd  Z    = False
  odd (S k) = even k
-}

||| The faces of a coin, heads or tails.
data Face = Heads | Tails

implementation Eq Face where
  (==) Heads Heads = True
  (==) Tails Tails = True
  (==) _     _     = False

syntax [test] "?" [t] ":" [e] = if test then t else e;

private
getFace : Int -> Face
getFace x with (divides x 2)
  getFace (_ + rem) | (DivBy _) = (rem == 1) ? Tails : Heads

coinFlips : (count : Nat) -> Stream Int -> List Face
coinFlips  Z     _        = []
coinFlips (S k) (x :: xs) = getFace x :: coinFlips k xs

-- ------------------------------------------------------- [ Exercise 11.1.7.4 ]

private
squareRootApprox : (number, approx : Double) -> Stream Double
squareRootApprox number approx =
  let next = (approx + (number / approx)) / 2
  in  approx :: squareRootApprox number next

-- ------------------------------------------------------- [ Exercise 11.1.7.5 ]

squareRootBound : (max : Nat) -> (number, bound : Double)
               -> (approxs : Stream Double)
               -> Double
squareRootBound  Z    _      _     (x :: _)  = x
squareRootBound (S k) number bound (x :: xs) =
  if bound > abs (x * x)
    then x
    else squareRootBound k number bound xs

squareRoot : (number : Double) -> Double
squareRoot number = squareRootBound 100 number 0.00000000001
                      (squareRootApprox number number)

-- ------------------------------------------------------------------- [ InfIO ]

namespace InfIO
  data InfIO : Type where
       Do    : IO a -> (a -> Inf InfIO) -> InfIO

  (>>=) : IO a -> (a -> Inf InfIO) -> InfIO
  (>>=) = Do

data Fuel = Dry | More (Lazy Fuel)

tank : Nat -> Fuel
tank  Z    = Dry
tank (S k) = More (tank k)

partial
forever : Fuel
forever = More forever

run : Fuel -> InfIO -> IO ()
run  Dry         _       = putStrLn "Out of fuel"
run (More fuel) (Do c f) = do res <- c
                              run fuel (f res)

-- --------------------------------------------------------- [ Exercise 11.2.7 ]

totalREPL : (prompt : String) -> (action : String -> String) -> InfIO
totalREPL prompt action
  = do putStr prompt
       input <- getLine
       putStr (action input)
       totalREPL prompt action

-- ------------------------------------------ [ 11.3.2 Domain Specific Comands ]

data Command  : Type -> Type where
     PutStr   : String -> Command ()
     PutStrLn : String -> Command ()
     GetLine  : Command String

     Pure     : ty -> Command ty
     Bind     : Command a -> (a -> Command b) -> Command b

-- ------------------------------------------------------- [ Exercise 11.3.4.2 ]
     ReadFile  : (filepath : String) -> Command (Either FileError String)
     WriteFile : (filepath, contents : String) -> Command (Either FileError ())

namespace CommandDo
  (>>=) : Command a -> (a -> Command b) -> Command b
  (>>=) = Bind

runCommand : Command a -> IO a
runCommand (PutStr   str) = putStr str
runCommand (PutStrLn str) = putStrLn str
runCommand  GetLine       = getLine
runCommand (Pure val)     = pure val
runCommand (Bind c f)     = runCommand c >>= runCommand . f
runCommand (ReadFile  filepath)          = readFile filepath
runCommand (WriteFile filepath contents) = writeFile filepath contents

data ConsoleIO : Type -> Type where
     Quit      : a -> ConsoleIO a
     Do        : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b

namespace ConsoleDo
  (>>=) : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b
  (>>=) = Do

  run : Fuel -> ConsoleIO a -> IO (Maybe a)
  run       fuel  (Quit val) = do pure (Just val)
  run (More fuel) (Do c f)   = do res <- runCommand c
                                  run fuel (f res)
  run  Dry         p         = pure Nothing

  run_ : Fuel -> ConsoleIO a -> IO ()
  run_       fuel  (Quit val) = pure ()
  run_ (More fuel) (Do c f)   = do res <- runCommand c
                                   run_ fuel (f res)
  run_  Dry         p         = pure ()

  partial
  runForever : ConsoleIO a -> IO (Maybe a)
  runForever = run forever

  partial
  runForever_ : ConsoleIO a -> IO ()
  runForever_ = run_ forever

-- ---------------------------------------------- [ 11.3.3 Sequencing Commands ]

data Input = Answer Int
           | QuitCmd

readInput : (prompt : String) -> Command Input
readInput prompt = do PutStr prompt
                      answer <- GetLine
                      if toLower answer == "quit"
                         then Pure QuitCmd
                         else Pure (Answer (cast answer))

-- ------------------------------------------------------- [ Exercise 11.3.4.1 ]

record QuizState where
  constructor MkQuizState
  score, attempts : Nat

implementation Show QuizState where
  show (MkQuizState score attempts)
    = show score ++ " / " ++ show attempts

private
arithInputs : (seed : Int) -> Stream Int
arithInputs seed = map bound (randoms seed)
  where
    bound : Int -> Int
    bound num with (divides num 12)
      bound ((12 * div) + rem) | (DivBy prf) = abs rem + 1

mutual
  correct : Stream Int -> QuizState -> ConsoleIO QuizState
  correct nums state
    = do PutStrLn "Correct!"
         quiz nums (record { score $= (+ 1) } state)

  wrong : Stream Int -> Int -> QuizState -> ConsoleIO QuizState
  wrong nums answer state
    = do PutStrLn $ "Wrong, the answer is: " ++ show answer
         quiz nums state

  quiz : Stream Int -> QuizState -> ConsoleIO QuizState
  quiz (num1 :: num2 :: nums) state
    = do PutStrLn $ "Score so far: " ++ show state
         input <- readInput $ show num1 ++ " * " ++ show num2 ++ "? "
         case input of
              Answer answer =>
                let newState = record { attempts $= (+ 1) } state
                    correctAnswer = num1 * num2 in
                if answer == correctAnswer
                   then correct nums newState
                   else wrong nums correctAnswer newState
              QuitCmd =>
                Quit state

-- ------------------------------------------------------- [ Exercise 11.3.4.3 ]

mutual
  ||| Read the contents of a file and print it to stdout with a trailing
  ||| newline. Print an error message if filename is not a normal file.
  cat : (filename : String) -> ConsoleIO ()
  cat filename
    = do Right contents <- ReadFile filename
           | Left err => do PutStrLn (show err)
                            shell
         PutStrLn contents
         shell

  ||| Read the contents of a source file and write it to a destination file.
  ||| Print an error message if anything goes wrong.
  ||| @ source a source filepath, must be a normal file
  ||| @ destination a destination filepath, must be writable
  copy : (source, destination : String) -> ConsoleIO ()
  copy source destination
    = do Right contents <- ReadFile source
           | Left err => do PutStrLn (show err)
                            shell
         Right () <- WriteFile destination contents
           | Left err => do PutStrLn (show err)
                            shell
         shell

  ||| Print a warning about an invalid command.
  ||| @ command a string that represents an invalid command
  invalidCommand : (command : String) -> ConsoleIO ()
  invalidCommand command
    = do PutStrLn ("Invalid command: " ++ command)
         shell

  ||| Quit the shell.
  exit : ConsoleIO ()
  exit = Quit ()

  ||| Run a limited, interactive shell.
  ||| Supported commands:
  |||   - cat [filename]
  |||   - copy [source] [destination]
  |||   - exit
  shell : ConsoleIO ()
  shell = do PutStr "> "
             input <- GetLine
             case words input of
                  ["exit"] => exit
                  ["cat", filepath] => cat filepath
                  ["copy", source, destination] => copy source destination
                  _ => invalidCommand input

-- ------------------------------------------------------------------- [ Tests ]

testEveryOther : IO ()
testEveryOther = assertEq [2,4..20] $ take 10 (everyOther [1..])

testInfListFunctor : IO ()
testInfListFunctor = assertEq [2,4..20] $ getPrefix 10 (map (*2) (countFrom 1))

testCoinFlips : IO ()
testCoinFlips = assertEq [Tails,Heads,Tails,Tails,Heads,Tails] $
                         coinFlips 6 (randoms 12345)

testSquareRootApprox1 : IO ()
testSquareRootApprox1 = assertEq [10.0,5.5,3.659090909090909] $
                                 take 3 (squareRootApprox 10 10)

testSquareRootApprox2 : IO ()
testSquareRootApprox2 = assertEq [25.0,14.5,10.698275862068964] $
                                 take 3 (squareRootApprox 100 25)

testSquareRoot1 : IO ()
testSquareRoot1 = assertEq 2.449489742783178 (squareRoot 6)

testSquareRoot2 : IO ()
testSquareRoot2 = assertEq 50.0 (squareRoot 2500)

testSquareRoot3 : IO ()
testSquareRoot3 = assertEq 50.009999000199954 (squareRoot 2501)

-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: yurrriq/tdd-with-idris

max_issues_repo_name: yurrriq/tdd-with-idris

max_forks_repo_name: yurrriq/tdd-with-idris


text:
module TypFunktionen

NatOderString : Bool -> Type
NatOderString False = Nat
NatOderString True = String

natOrString : (b:Bool) -> NatOderString b
natOrString False = 42
natOrString True = "Frage"

toString : (b:Bool) -> NatOderString b -> String
toString False n = show n
toString True s = s