
  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 : List Type -> Type where
 12 |   FIni : FState [Formula]
 13 |   FEl  : FState [Elem,Formula]
 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 t         = dput FEl $ el::t
 34 |   onelem el FEl  (e::f::t) = dput FEl $ el::insertElem e f::t
 35 | 
 36 |   onnat : Integer -> StateAct q FState FSz
 37 |   onnat n FEl (e::f::t) = dput FIni $ insert e (cast n) f::t
 38 |   onnat n p t           = dput p t
 39 | 
 40 | el : Steps q FSz SK
 41 | el = vals symbol (\el => \(sk # t) => dact (onelem el) t) values
 42 | 
 43 | formulaTrans : Lex1 q FSz SK
 44 | formulaTrans =
 45 |   lex1
 46 |     [ entry FIni $ dfa el
 47 |     , entry FEl  $ dfa (conv decimal (dact . onnat . decimal) :: el)
 48 |     ]
 49 | 
 50 | formulaErr : Arr32 FSz (SK q -> F1 q (BoundedErr Void))
 51 | formulaErr = errs []
 52 | 
 53 | formulaEOI : Index FSz -> SK q -> F1 q (Either (BoundedErr Void) Formula)
 54 | formulaEOI v sk t =
 55 |   case read1 sk.stack_ t of
 56 |     (FIni:>(f::_))   # t => Right f # t
 57 |     (FEl:>(e::f::_)) # t => Right (insertElem e f) # t
 58 | 
 59 | public export
 60 | formula : P1 q (BoundedErr Void) Formula
 61 | formula =
 62 |   P (cast FIni) (init $ FIni:>[neutral]) 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 |