diff --git a/Calc.agda b/Calc.agda
index a9c594b..b78bd50 100644
--- a/Calc.agda
+++ b/Calc.agda
@@ -5,14 +5,17 @@
 module Calc where
 
 open import Agda.Builtin.Char
+open import Agda.Builtin.Maybe
 open import Agda.Builtin.Nat
 open import Agda.Builtin.String
 
 open import Data.Nat.Show
 open import IO
 
+open import Expr
 open import Parse
 open import Util
 
 main : Main
-main = run (putStrLn (showMaybe show (takeNat "123a456")))
\ No newline at end of file
+main = run (getLine >>= λ c → putStrLn (showResult show (evalBin (takeBin (primStringToList c)))))
+-- main = run (getLine >>= λ c → putStrLn (showList (showResult show) (map evalBin (takeLine (primStringToList c))))) -- "123+415\n1+2\n")))))
\ No newline at end of file
diff --git a/Expr.agda b/Expr.agda
index fcd863b..53c751a 100644
--- a/Expr.agda
+++ b/Expr.agda
@@ -1,6 +1,14 @@
-data BinExpr : Set where
-  binE : Token → Token → Token → BinExpr
+module Expr where
 
-evalBin : BinExpr → Maybe Nat
-evalBin (binE (Oper '+') (Digit a) (Digit b)) = just (a + b)
-evalBin (binE _ _ _) = nothing
+open import Agda.Builtin.Char
+open import Agda.Builtin.List
+open import Agda.Builtin.Maybe
+open import Agda.Builtin.Nat
+open import Agda.Builtin.String
+
+data Token : Set where
+  Digit : Nat → Token
+  Delim : Char → Token
+  Oper : Char → Token
+  Skip : Char → Token
+  Term : Token
diff --git a/Parse.agda b/Parse.agda
index be8db5c..f7cee2f 100644
--- a/Parse.agda
+++ b/Parse.agda
@@ -6,13 +6,29 @@ open import Agda.Builtin.Maybe
 open import Agda.Builtin.Nat
 open import Agda.Builtin.String
 
+open import Expr
 open import Util
 
-data Token : Set where
-  Digit : Nat → Token
-  Delim : Char → Token
-  Oper : Char → Token
-  Term : Token
+record Result (A : Set) : Set where
+  constructor emit
+  field
+    res : Maybe A
+    rem : List Char
+
+showResult : {A : Set} → (A → String) → Result A → String
+showResult f (emit (just r) _) = primStringAppend "result: " (f r)
+showResult f (emit nothing rem) = primStringAppend "remainder: " (primStringFromList rem)
+
+-- take consecutive occurences of a character set
+takeCons : List Char → List Char → Result (List Char)
+takeCons [] r = emit nothing r
+takeCons _ [] = emit nothing []
+takeCons cs (x ∷ xs) with (findCharIndex 0 x cs)
+...                     | nothing = emit nothing (x ∷ xs)
+-- ...                     | just n = x ∷ (takeCons cs xs)
+...                     | just n with (takeCons cs xs)
+...                                 | emit nothing rem = emit (just (x ∷ [])) xs
+...                                 | emit (just res) rem = emit (just (x ∷ res)) rem
 
 parseChar : Char → Token
 parseChar '0' = Digit 0
@@ -28,39 +44,54 @@ parseChar '9' = Digit 9
 parseChar ',' = Delim ','
 parseChar '=' = Oper '='
 parseChar '+' = Oper '+'
+parseChar ' ' = Skip ' '
 parseChar _   = Term
 
-parseNat : Nat → List Char → Nat
-parseNat a [] = a
+parseNat : Maybe Nat → List Char → Result Nat
+parseNat a [] = emit a []
 parseNat a (x ∷ xs) with parseChar x
-...                     | Digit n = parseNat ((a * 10) + n) xs
-...                     | _ = a
+...                     | Digit n = parseNat (just (((default 0 a) * 10) + n)) xs
+...                     | Skip c = parseNat a xs
+...                     | _ = emit nothing xs
 
 digits : List Char
 digits = primStringToList "0123456789"
 
-takeNat : String → Maybe Nat
-takeNat s with takeCons digits (primStringToList s)
-...            | [] = nothing
-...            | xs = just (parseNat 0 xs)
+takeNat : List Char → Result Nat
+takeNat s with takeCons digits s
+...            | emit nothing rem₁ = emit nothing rem₁
+...            | emit (just xs) rem₁ with parseNat nothing xs
+...                                     | emit nothing rem₂ = emit nothing rem₁
+...                                     | emit (just n) rem₂ = emit (just n) rem₁
 
-parseList₂ : String → List Nat
-parseList₂ s with primStringToList s
-...             | [] = []
-...             | (x ∷ xs) with parseChar x
-...                           | Digit n = n ∷ []
-...                           | _ = []
+takeOper : List Char → Result Token
+takeOper s with takeCons ('+' ∷ []) s
+...           | emit nothing rem = emit nothing rem
+...           | emit (just []) rem = emit nothing rem
+...           | emit (just (x ∷ xs)) rem with parseChar x
+...                                         | Oper o = emit (just (Oper o)) rem -- todo: what about xs?
+...                                         | _ = emit nothing rem -- todo: loop here?
 
--- old stuff...
+-- we know operators are a single char, so xs must be empty, but anything left there should be attached to rem?
 
-parseList : Nat → List Char → List Nat
-parseList a [] = a ∷ []
-parseList a (x ∷ xs) with parseChar x
-...                     | Digit n = parseList ((a * 10) + n) xs
-...                     | Delim s = a ∷ parseList 0 xs
-...                     | Oper o = [] -- ignore for now
-...                     | Term = []
+data BinExpr : Set where
+  bin : Token → Token → Token → BinExpr
 
-parseExpr : String → List Nat
-parseExpr "" = []
-parseExpr x = parseList 0 (primStringToList x)
+evalBin : Result BinExpr → Result Nat
+evalBin (emit nothing rem) = emit nothing rem
+evalBin (emit (just (bin (Oper '+') (Digit a) (Digit b))) rem) = emit (just (a + b)) rem
+evalBin (emit (just (bin _ _ _)) rem) = emit nothing rem
+
+takeBin : List Char → Result BinExpr
+takeBin s with takeNat s
+...           | emit nothing rem₁ = emit nothing s
+-- ...           | emit (just res₁) rem₁ = emit (just (bin (Oper '+') (Digit res₁) (Digit res₁))) rem₁
+...           | emit (just res₁) rem₁ with takeOper rem₁
+...                                       | emit nothing rem₃ = emit nothing rem₁
+-- ...                                       | emit (just oper) rem₂ = emit (just (bin oper (Digit res₁) (Digit res₁))) rem₁
+...                                       | emit (just oper) rem₃ with takeNat rem₃
+...                                                                   | emit nothing rem₄ = emit nothing rem₁
+...                                                                   | emit (just res₄) rem₄ = emit (just (bin oper (Digit res₁) (Digit res₄))) rem₄
+
+takeLine : List Char → List (Result BinExpr)
+takeLine s = map takeBin (split ('\n' ∷ []) s)
diff --git a/Util.agda b/Util.agda
index f6d4c59..69e6ceb 100644
--- a/Util.agda
+++ b/Util.agda
@@ -2,11 +2,18 @@ module Util where
 
 open import Agda.Builtin.Bool
 open import Agda.Builtin.Char
+open import Agda.Builtin.Equality
 open import Agda.Builtin.List
 open import Agda.Builtin.Maybe
 open import Agda.Builtin.Nat
 open import Agda.Builtin.String
 
+-- given some default value and a Maybe, definitely return one of them
+default : {V : Set} → V → Maybe V → V
+default n nothing = n
+default n (just m) = m
+
+-- return the same thing, for functions that need a noop fn
 ident : {V : Set} → V → V
 ident x = x
 
@@ -66,10 +73,17 @@ showMaybe : {V : Set} → (V → String) → Maybe V → String
 showMaybe f nothing = "nothing"
 showMaybe f (just v) = f v
 
--- take consecutive occurences of a character set
-takeCons : List Char → List Char → List Char
-takeCons [] _ = []
-takeCons _ [] = []
-takeCons cs (x ∷ xs) with (findCharIndex 0 x cs)
-...                     | nothing = []
-...                     | just n = x ∷ (takeCons cs xs)
+-- findAny : { A : Set } → Nat → A → List A → Nat
+-- findAny n t [] = n
+-- findAny n t (x ∷ xs) with (t ≡ x)
+-- ...                     | refl = n
+-- ...                     | _ = findAny (suc n) t xs
+
+split : List Char → List Char → List (List Char)
+split = go [] []
+  where
+    go : List Char → List (List Char) → List Char → List Char → List (List Char)
+    go acc acl delims [] = acl
+    go acc acl delims (x ∷ xs) with (primCharEquality x '\n')
+    ...                           | true = go [] (acc ∷ acl) delims xs
+    ...                           | false = go (x ∷ acc) acl delims xs
\ No newline at end of file