
   0 | module Data.List.Suffix.Result
   1 | 
   2 | import Data.Bool.Rewrite
   3 | import public Data.List.Suffix
   4 | 
   5 | %default total
   6 | 
   7 | ||| Result of consuming and converting a (possibly strict) prefix
   8 | ||| of a list of tokens.
   9 | |||
  10 | ||| This comes with a non-erased proof about the number of tokens
  11 | ||| consumed, which can be used to for instance 
  12 | ||| calculate the bounds of a lexeme. Likewise, the error specifies
  13 | ||| a start and end suffix for calculating proper bounds in case
  14 | ||| of an error.
  15 | |||
  16 | ||| Use this for writing simple, high-performance tokenizers, which
  17 | ||| (in the case of strict results) are guaranteed to terminate.
  18 | ||| See module `Text.Lex.Manual` for
  19 | ||| utilities for consuming and converting prefixes
  20 | ||| of tokens, but for a nicer interface, consider using `Text.Lex.Tokenizer`
  21 | ||| (at the cost of a drop in performance).
  22 | |||
  23 | ||| @ strict : True if a strict prefix of the list of tokens has
  24 | |||            been consumed.
  25 | ||| @ t      : the type of token consumed.
  26 | ||| @ ts     : the original list of tokens
  27 | ||| @ e      : the error type in case of a failure
  28 | ||| @ a      : the result type
  29 | public export
  30 | data Result :
  31 |      (strict : Bool)
  32 |   -> (t : Type)
  33 |   -> List t
  34 |   -> (e,a : Type)
  35 |   -> Type where
  36 | 
  37 |   Succ :
  38 |        {0 b : Bool}
  39 |     -> {0 t,e,a : Type}
  40 |     -> {0 ts : List t}
  41 |     -> (val : a)
  42 |     -> (xs : List t)
  43 |     -> {auto p : Suffix b xs ts}
  44 |     -> Result b t ts e a
  45 | 
  46 |   Fail :
  47 |        {0 b : Bool}
  48 |     -> {0 t,e,a : Type}
  49 |     -> {ts,stopStart : List t}
  50 |     -> (start : Suffix False stopStart ts)
  51 |     -> (0 errEnd : List t)
  52 |     -> {auto end : Suffix False errEnd stopStart}
  53 |     -> (reason : e)
  54 |     -> Result b t ts e a
  55 | 
  56 | ||| Alias for `Succ`, which takes the proof as an
  57 | ||| explicit argument
  58 | public export %inline
  59 | succ : 
  60 |        {0 b : Bool}
  61 |     -> {0 t,e,a : Type}
  62 |     -> {0 ts : List t}
  63 |     -> (val : a)
  64 |     -> {xs : List t}
  65 |     -> Suffix b xs ts
  66 |     -> Result b t ts e a
  67 | succ val _ = Succ val xs
  68 | 
  69 | public export
  70 | Functor (Result b t ts e) where
  71 |   map f (Succ v xs)    = Succ (f v) xs
  72 |   map _ (Fail st ee r) = Fail st ee r
  73 | 
  74 | --------------------------------------------------------------------------------
  75 | --          Conversions
  76 | --------------------------------------------------------------------------------
  77 | 
  78 | public export %inline
  79 | swapOr : {0 x,y : _} -> Result (x || y) t ts e a -> Result (y || x) t ts e a
  80 | swapOr = swapOr (\k => Result k t ts e a)
  81 | 
  82 | public export %inline
  83 | orSame : {0 x : _} -> Result (x || x) t ts e a -> Result x t ts e a
  84 | orSame = orSame (\k => Result k t ts e a)
  85 | 
  86 | public export %inline
  87 | orTrue : {0 x : _} -> Result (x || True) t ts e a -> Result True t ts e a
  88 | orTrue = orTrue (\k => Result k t ts e a)
  89 | 
  90 | public export %inline
  91 | orFalse : {0 x : _} -> Result (x || False) t ts e a -> Result x t ts e a
  92 | orFalse = orFalse (\k => Result k t ts e a)
  93 | 
  94 | public export %inline
  95 | swapAnd : {0 x,y : _} -> Result (x && y) t ts e a -> Result (y && x) t ts e a
  96 | swapAnd = swapAnd (\k => Result k t ts e a)
  97 | 
  98 | public export %inline
  99 | andSame : {0 x : _} -> Result (x && x) t ts e a -> Result x t ts e a
 100 | andSame = andSame (\k => Result k t ts e a)
 101 | 
 102 | public export %inline
 103 | andTrue : {0 x : _} -> Result (x && True) t ts e a -> Result x t ts e a
 104 | andTrue = andTrue (\k => Result k t ts e a)
 105 | 
 106 | public export %inline
 107 | andFalse : {0 x : _} -> Result (x && False) t ts e a -> Result False t ts e a
 108 | andFalse = andFalse (\k => Result k t ts e a)
 109 | 
 110 | public export %inline
 111 | weaken : {0 x : _} -> Result x t ts e a -> Result False t ts e a
 112 | weaken (Succ val xs @{p}) = Succ val xs @{weaken p}
 113 | weaken (Fail x y err) = Fail x y err
 114 | 
 115 | public export %inline
 116 | weakens : {0 x : _} -> Result True t ts e a -> Result x t ts e a
 117 | weakens (Succ val xs @{p}) = Succ val xs @{weakens p}
 118 | weakens (Fail x y err) = Fail x y err
 119 | 
 120 | public export %inline
 121 | and1 : {0 x : _} -> Result x t ts e a -> Result (x && y) t ts e a
 122 | and1 (Succ val xs @{p}) = Succ val xs @{and1 p}
 123 | and1 (Fail x y err) = Fail x y err
 124 | 
 125 | public export %inline
 126 | and2 : {0 x : _} -> Result x t ts e a -> Result (y && x) t ts e a
 127 | and2 r = swapAnd $ and1 r
 128 | 
 129 | public export %inline
 130 | trans :
 131 |      {ys : _}
 132 |   -> Result b1 t xs e a
 133 |   -> Suffix b2 xs ys
 134 |   -> Result (b1 || b2) t ys e a
 135 | trans (Succ val ts @{p}) q = Succ val ts @{trans p q}
 136 | trans (Fail {stopStart} x y err) q =
 137 |   Fail {stopStart} (weaken $ trans x q) y err
 138 | 
 139 | public export %inline
 140 | succT :
 141 |       {ys : _}
 142 |   ->  Result b1 t xs e a
 143 |   -> {auto p : Suffix True xs ys}
 144 |   -> Result True t ys e a
 145 | succT r = swapOr $ trans r p
 146 | 
 147 | public export %inline
 148 | succF :
 149 |       {ys : _}
 150 |   ->  Result b1 t xs e a
 151 |   -> {auto p : Suffix True xs ys}
 152 |   -> Result False t ys e a
 153 | succF r = weaken $ trans r p
 154 |