Move unused files to ATTIC (not committed)

.gitignore

@@ -1,2 +1,2 @@
 build/
-*.*~
+*.*~ATTIC

src/Derive.idr

@@ -1,46 +0,0 @@
-module Derive
-
-import public Language.Reflection
--- import public Language.Elab.Syntax
--- import public Language.Elab.Types
-
--- Is base not in scope?
--- import public Deriving.Common
-
-%language ElabReflection
-
-getType1 : Name -> Elab (Name,TTImp)
-getType1 name = do
-  [rval] <- getType name 
-    | [] => fail "can't get fullname for \{show name}"
-    | _  => fail "ambiguous name \{show name}"
-  pure rval
-
-
-fullName : Name -> Elab Name
-fullName name = do
-  [(qname,_)] <- getType name 
-    | [] => fail "can't get fullname for \{show name}"
-    | _  => fail "ambiguous name \{show name}"
-  pure qname
-
-export
-deriveShow : Name -> Elab ()
-deriveShow name = do
-    myGoal <- goal
-    logMsg "foo" 1 $ "my goal is \{show myGoal}"
-    fname <- fullName name
-    logMsg "foo" 1 $ "woo \{show fname}"
-    cons <- getCons fname
-    logMsg "foo" 1 $ "cons \{show cons}"
-    for_ cons $ \name => do
-      logMsg "foo" 1 $ "getType1 \{show name}"
-      (_,type) <- getType1 name
-      logTerm "foo" 1 (show name) type
-      -- type doesn't really matter, we need the explicit arity and the base name
-      
-
-
-    pure ()
-
-

src/Lib/Grammar.idr

@@ -1,45 +0,0 @@
-module Lib.Grammar
-
--- Derived from Parser/Core.idr - revisit later when we want to be stack safe
--- For simplicity (for now), it drops consumed flag from the type, which I think was
--- there for totality checking.  May want it back someday.
-
-data Grammar : (state : Type) -> (tok : Type) -> Type -> Type where
-  EOF : Grammar state tok ()
-  Empty : a -> Grammar state tok a
-  Fail : String -> Grammar state tok a
-  Commit : Grammar state tok ()
-  Alt : Grammar state tok ty -> Lazy (Grammar state tok ty) -> Grammar state tok ty
-  Seq : Grammar state tok a -> (a -> Grammar state tok b) -> Grammar state tok b
-
-Functor (Grammar state tok) where
-  map f (Fail str) = Fail str
-  map f (Alt x y) = Alt (map f x) (map f y)
-  map f (Seq x g) = ?todo_4
-  map f (Empty v) = Empty (f v)
-  -- Empty / EOF
-  map f p = Seq p (Empty . f)
-  
-Applicative (Grammar state tok) where
-  pure a = Empty a
-  x <*> y = ?hole3
-
-Alternative (Grammar state tok) where 
-  empty = ?hole2
-  (<|>) = Alt
-
-Monad (Grammar state tok) where
-  (>>=) = Seq
-
-ParseError : Type
-
-data ParseResult : Type -> Type -> Type -> Type where
-  Failure : (commit : Bool) -> List ParseError -> ParseResult state tok ty
-
-doParse : Semigroup state =>
-          state ->
-          (commit : Bool) ->
-          Grammar state tok ty ->
-          List tok ->
-          ParseResult state tok ty
-doParse = ?todo

src/Lib/Layout.idr

@@ -1,48 +0,0 @@
-module Lib.Layout
-
-import Lib.Token
-import Text.Lexer
-
--- Dunno if I'll do layout or pass col, but here it is:
-
-intro : List String
-intro = [ "where", "let", "of" ]
-
-Position : Type
-Position = (Int,Int)
-
-isIntro : BTok -> Bool
-isIntro t = elem (value t) intro
-
-export
-layout : List BTok -> List BTok
-layout = go [] []
-  where
-    lbrace = irrelevantBounds (Tok LBrace "{")
-    semi = irrelevantBounds (Tok Semi ";")
-    rbrace = irrelevantBounds (Tok RBrace "}")
-
-    -- go' does start of block
-    go' : List BTok -> List Position -> List BTok -> List BTok
-
-    -- go does semi and end of block, we require "in" to be on separate, outdented line if not the same line as let
-    go : List BTok -> List Position -> List BTok -> List BTok
-    go acc lvls [] = reverse acc
-    go acc [] ts = go' acc [] ts
-    go acc lvls@(lvl::rest) toks@(t :: ts) =
-      let (sr,sc) = start t in
-      if      snd lvl >  sc then go (rbrace :: acc) rest toks
-      else if snd lvl == sc then go' (semi :: acc) lvls toks
-      else if value t == "in" && sr == fst lvl then go' (rbrace :: acc) rest toks
-      else go' acc lvls toks
-    
-    -- handle start of block
-    go' acc lvls [] = reverse acc
-    go' acc lvls (t::ts) = case isIntro t of
-      False => go (t::acc) lvls ts
-      True => case ts of
-          t'::ts' => go (t' :: lbrace :: t :: acc) (start t' :: lvls) ts'
-          []      => go (rbrace :: lbrace :: t :: acc) lvls ts
-
-      
-      

src/Lib/Lexer2.idr

@@ -1,56 +0,0 @@
-module Lib.Lexer2
-
-data UToken
-  = Ident String
-  | Let
-  | In
-  | Data
-  | Where
-  | Forall
-  | Case
-  | Of
-  | Underscore
-  | Operator String
-  | Equals
-  | Dot
-  | Colon
-  | Pipe
-  | RightArrow
-  | FatArrow
-  | Number Int
-  | Lambda
-  | LeftParen
-  | RightParen
-  | LeftBrace
-  | RightBrace
-  | Error
-
--- we can skip this if we keep the text...
-
-Show UToken where
-  show = \case
-    Ident name => name
-    Let => "let"
-    In => "in"
-    Data => "data"
-    Where => "where"
-    Forall => "forall"
-    Case => "case"
-    Of => "of"
-    Underscore => "_"
-    Operator name => name
-    Equals => ?rhs_10
-    Dot => ?rhs_11
-    Colon => ?rhs_12
-    Pipe => ?rhs_13
-    RightArrow => ?rhs_14
-    FatArrow => ?rhs_15
-    Number i => show i
-    Lambda => ?rhs_17
-    LeftParen => ?rhs_18
-    RightParen => ?rhs_19
-    LeftBrace => ?rhs_20
-    RightBrace => ?rhs_21
-    Error => ?rhs_22
-
-

src/Lib/Test.idr

@@ -1,23 +0,0 @@
-import Text.Lexer
-
-data Kind = Ignore | Ident | Oper | Number
-
-ignore : WithBounds (Token Kind) -> Bool
-ignore (MkBounded (Tok Ignore _) _ _) = True
-ignore _ = False
-
-tmap : TokenMap (Token Kind)
-tmap = [
-  (alpha <+> many alphaNum, Tok Ident),
-  (some digit, Tok Number),
-  (some symbol, Tok Oper),
-  (spaces, Tok Ignore)
-]
-
-show : WithBounds (Token Kind) -> String
-show t@(MkBounded (Tok _ v) _ _) = "\{show $ start t} \{show v}"
-
-main : IO ()
-main = do
-  let toks = filter (not . ignore) $ fst $ lex tmap  "let x = 1\n    y = 2\n in x + y"
-  traverse_ (putStrLn . show) toks

src/Lib/Tok2.idr

@@ -1,55 +0,0 @@
-module Lib.Tok2
-
-import Text.Bounded
-
-data Kind 
-  = Ident 
-  | Keyword 
-  | Oper 
-  | Number 
-  | Symbol
-  | Arrow
-  | Ignore
-  | EOF
-
-data Token = Tok Kind String
-
-Show Kind where
-  show Ident   = "Ident"
-  show Keyword = "Keyword"
-  show Oper    = "Oper"
-  show Number  = "Number"
-  show Symbol  = "Symbol"
-  show Arrow   = "Arrow"
-  show Ignore  = "Ignore"
-  show EOF = "EOF"
-
-Show Token where show (Tok k v) = "<\{show k}:\{show v}>"
-
-keywords : List String
-keywords = ["let", "in", "where", "case"]
-
-specialOps : List String
-specialOps = ["->", ":"]
-
-checkKW : String -> Token
-checkKW s = if elem s keywords then Tok Keyword s else Tok Ident s
-
-opkind : String -> Kind
-opkind "->" = Arrow
-opkind _    = Oper
-
-isOpChar : Char -> Bool
-isOpChar c = c `elem` (unpack ":!#$%&*+./<=>?@\\^|-~")
-
-nextToken : Int -> Int -> List Char -> Maybe (Token, (Int, Int, List Char))
-nextToken row col xs = case xs of
-  []  => Nothing
-  (' ' :: cs) =>  nextToken row (col + 1) cs
-  (c :: cs)   =>
-    if isDigit c then getTok (Tok Number) isDigit [c] cs
-    else if isOpChar c then getTok else ?Foo
-  where
-    getTok : (String -> Token) -> (Char -> Bool) -> List Char -> List Char -> Maybe (Token, (Int, Int, List Char))
-
-

src/Lib/Tokenizer2.idr

@@ -1,78 +0,0 @@
-module Lib.Tokenizer2
-
--- Starting to write from-scratch tokenizer to flatten out the data a little.
-
-data Position = Pos Int Int
-
-inc : Position -> Position
-inc (Pos l c) = Pos l (c + 1)
-
-
-public export
-data Kind 
-  = Ident 
-  | Keyword 
-  | Oper 
-  | Comment
-  | Number 
-  | Symbol
-  | Arrow
-  -- virtual stuff deprecated?
-  | LBrace
-  | Semi
-  | RBrace
-  | EOF
-
-data Token = Tok Int Int Kind String
-
-data Lexer
-  = Match (Char -> Bool)
-  | Seq Lexer 
-
-keywords : List String
-keywords = ["let", "in", "where", "case", "of", "data"]
-
-specialOps : List String
-specialOps = ["->", ":"]
-
--- checkKW : String -> Token Kind
--- checkKW s = if elem s keywords then Tok Keyword s else Tok Ident s
-
-opkind : String -> Kind
-opkind "->" = Arrow
-opkind _    = Oper
-
-isOpChar : Char -> Bool
-isOpChar c = c `elem` (unpack ":!#$%&*+./<=>?@\\^|-~")
-
--- opChar : Lexer
--- opChar = pred isOpChar
-
-token : Int -> Int -> List Char -> (Token, List Char)
-token l c cs = case cs of
-  [] => (Tok l c EOF "",[])
-  ('-' :: '-' :: cs) => scan (/= '\n') ['-','-'] l (c+2) cs
-  _ => ?fixme
-
-  where
-    scan : (Char -> Bool) -> (List Char) -> Int -> Int -> List Char -> (Token,List Char)
-
-
--- match could be a Maybe thing and use the maybe Alt impl.
--- Not sure what shape I want here.  Maybe a straight up Character Parser and drop tokenization.
-
--- rawTokens : Tokenizer (Token Kind)
--- rawTokens
---    =  match (alpha <+> many alphaNum) checkKW
---   <|> match (some digit) (Tok Number)
---   <|> match (some opChar) (\s => Tok (opkind s) s)
---   <|> match (lineComment (exact "--")) (Tok Space)
---   <|> match symbol (Tok Symbol)
---   <|> match spaces (Tok Space)
-
-
--- export
--- tokenise : String -> List BTok
--- tokenise = filter notSpace . fst . lex rawTokens 
-
-

src/Main.idr

@@ -2,7 +2,7 @@ module Main
 
 import Data.String
 import Lib.Tokenizer
-import Lib.Layout
+-- import Lib.Layout
 import Lib.Token
 import Lib.Parser.Impl
 import Lib.Parser

src/Syntax.idr

@@ -1,15 +1,6 @@
 module Syntax
 
 import Data.String
-import Derive
-
--- Good enough start, lets parse
--- This is informed by pi-forall and others and is somewhat low level
--- %language ElabReflection
--- %logging "foo" 19
-
-%hide Name
-%hide Decl
 
 Name = String
 
@@ -127,9 +118,7 @@ Show Plicity where
 
 covering
 Show Term where
-  show (Ann t ty) = "Ann" ++ " " ++ show t ++ " " ++ show ty
   show Wildcard = "Wildcard"
-  
   show (Var name) = foo ["Var", show name]
   show (Ann t ty) = foo [ "Ann", show t, show ty]
   show (Lit x) = foo [ "Lit", show x]
@@ -138,6 +127,5 @@ Show Term where
   show (App x y) = foo [ "App", show x, show y]
   show (Lam x y) = foo [ "Lam", show x, show y]
   show (Case x xs) = foo [ "Case", show x, show xs]
-  
   show (ParseError str) = foo [ "ParseError", "str"]
-  show _ = "woo"
+