ssube
/
agulator
1
0
Fork 0
Code

switch split char to semicolon, remove some debug lines

This commit is contained in:
Sean Sube 2022-09-28 17:32:35 -05:00
parent 065885f0d0
commit 0ecc7467fe
3 changed files with 16 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
Calc.agda
View File

@ -17,5 +17,6 @@ open import Parse
open import Util
main : Main
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")))))
-- 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")))))

21
Parse.agda
View File

@ -6,6 +6,8 @@ open import Agda.Builtin.Maybe
open import Agda.Builtin.Nat
open import Agda.Builtin.String
import Data.List using (_++_)
open import Expr
open import Util
@ -25,11 +27,14 @@ 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
digits : List Char
digits = primStringToList "0123456789"
-- parse a single character into a typed token
parseChar : Char → Token
parseChar '0' = Digit 0
parseChar '1' = Digit 1
@ -47,6 +52,7 @@ parseChar '+' = Oper '+'
parseChar ' ' = Skip ' '
parseChar _ = Term
-- parse a number from a list of characters
parseNat : Maybe Nat → List Char → Result Nat
parseNat a [] = emit a []
parseNat a (x ∷ xs) with parseChar x
@ -54,9 +60,6 @@ parseNat a (x ∷ xs) with parseChar x
... | Skip c = parseNat a xs
... | _ = emit nothing xs
digits : List Char
digits = primStringToList "0123456789"
takeNat : List Char → Result Nat
takeNat s with takeCons digits s
... | emit nothing rem₁ = emit nothing rem₁
@ -69,10 +72,8 @@ 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?
-- we know operators are a single char, so xs must be empty, but anything left there should be attached to rem?
... | Oper o = emit (just (Oper o)) (Data.List._++_ xs rem)
... | _ = emit nothing s
data BinExpr : Set where
bin : Token → Token → Token → BinExpr
@ -85,13 +86,11 @@ 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)
takeLine s = map takeBin (split (';' ∷ []) s)

6
Util.agda
View File

@ -84,6 +84,6 @@ 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
go acc acl delims (x ∷ xs) with findCharIndex 0 x delims
... | nothing = go (x ∷ acc) acl delims xs
... | _ = go [] (acc ∷ acl) delims xs