
  0 | module Text.Lex.Formula
  1 | 
  2 | import Chem
  3 | import Data.Finite
  4 | import Derive.Prelude
  5 | import Text.ILex
  6 | import Text.ILex.DStack
  7 | 
  8 | %default total
  9 | %language ElabReflection
 10 | 
 11 | data FState : SnocList Type -> Type where
 12 |   FIni : FState [<Formula]
 13 |   FEl  : FState [<Formula,Elem]
 14 | 
 15 | %runElab deriveIndexed "FState" [Show,ConIndex]
 16 | 
 17 | FSz : Bits32
 18 | FSz = 1 + cast (conIndexFState $ FEl)
 19 | 
 20 | inBoundsFState : (s : FState ts) -> (cast (conIndexFState s) < FSz) === True
 21 | 
 22 | export %inline
 23 | Cast (FState ts) (Index FSz) where
 24 |   cast v = I (cast $ conIndexFState v) @{mkLT $ inBoundsFState v}
 25 | 
 26 | 0 SK : Type -> Type
 27 | SK = DStack FState Void
 28 | 
 29 | parameters {auto sk : SK q}
 30 | 
 31 |   %inline
 32 |   onelem : Elem -> StateAct q FState FSz
 33 |   onelem el FIni sx         = dput FEl $ sx:<el
 34 |   onelem el FEl  (sx:<f:<e) = dput FEl $ sx:<insertElem e f:<el
 35 | 
 36 |   onnat : Integer -> StateAct q FState FSz
 37 |   onnat n FEl (sx:<f:<e) = dput FIni $ sx :< insert e (cast n) f
 38 |   onnat n p   sx         = dput p sx
 39 | 
 40 | el : Steps q FSz SK
 41 | el = vals symbol (\el,_ => dact (onelem el)) values
 42 | 
 43 | formulaTrans : Lex1 q FSz SK
 44 | formulaTrans =
 45 |   lex1
 46 |     [ entry FIni $ dfa el
 47 |     , entry FEl  $ dfa (bytes decimal (dact . onnat . decimal) :: el)
 48 |     ]
 49 | 
 50 | formulaErr : Arr32 FSz (SK q -> F1 q (BBErr Void))
 51 | formulaErr = errs []
 52 | 
 53 | formulaEOI : Index FSz -> SK q -> F1 q (Either (BBErr Void) Formula)
 54 | formulaEOI v sk t =
 55 |   case read1 sk.stack_ t of
 56 |     (_:<f:>FIni)   # t => Right f # t
 57 |     (_:<f:<e:>FEl) # t => Right (insertElem e f) # t
 58 | 
 59 | public export
 60 | formula : P1 q (BBErr Void) Formula
 61 | formula =
 62 |   P (cast FIni) (init $ [<neutral]:>FIni) formulaTrans
 63 |     (\_ => (Nothing #)) formulaErr formulaEOI
 64 | 
 65 | inBoundsFState FIni = Refl
 66 | inBoundsFState FEl  = Refl
 67 | 
 68 | export %inline
 69 | parseFormula : String -> Either (ParseError Void) Formula
 70 | parseFormula = parseString formula Virtual
 71 | 
 72 | testFormula : String -> IO ()
 73 | testFormula s =
 74 |   case parseFormula s of
 75 |     Left x  => putStrLn "\{x}"
 76 |     Right f => printLn f
 77 |