
   0 | module Idrall.Value
   1 | 
   2 | import Idrall.Expr
   3 | import Idrall.Error
   4 | 
   5 | import Data.List1
   6 | 
   7 | mutual
   8 |   public export
   9 |   Ty : Type
  10 |   Ty = Value
  11 | 
  12 |   -- Values
  13 |   public export
  14 |   data Value
  15 |     = VConst FC U
  16 |     | VVar FC Name Int
  17 |     | VPrimVar FC
  18 |     | VApp FC Value Value
  19 |     | VLambda FC Ty Closure
  20 |     | VHLam FC HLamInfo (Value -> Either Error Value)
  21 |     | VPi FC Ty Closure
  22 |     | VHPi FC Name Value (Value -> Either Error Value)
  23 | 
  24 |     | VBool FC
  25 |     | VBoolLit FC Bool
  26 |     | VBoolAnd FC Value Value
  27 |     | VBoolOr FC Value Value
  28 |     | VBoolEQ FC Value Value
  29 |     | VBoolNE FC Value Value
  30 |     | VBoolIf FC Value Value Value
  31 | 
  32 |     | VNatural FC
  33 |     | VNaturalLit FC Nat
  34 |     | VNaturalBuild FC Value
  35 |     | VNaturalFold FC Value Value Value Value
  36 |     | VNaturalIsZero FC Value
  37 |     | VNaturalEven FC Value
  38 |     | VNaturalOdd FC Value
  39 |     | VNaturalSubtract FC Value Value
  40 |     | VNaturalShow FC Value
  41 |     | VNaturalToInteger FC Value
  42 |     | VNaturalPlus FC Value Value
  43 |     | VNaturalTimes FC Value Value
  44 | 
  45 |     | VInteger FC
  46 |     | VIntegerLit FC Integer
  47 |     | VIntegerShow FC Value
  48 |     | VIntegerNegate FC Value
  49 |     | VIntegerClamp FC Value
  50 |     | VIntegerToDouble FC Value
  51 | 
  52 |     | VDouble FC
  53 |     | VDoubleLit FC Double
  54 |     | VDoubleShow FC Value
  55 | 
  56 |     | VText FC
  57 |     | VTextLit FC VChunks
  58 |     | VTextAppend FC Value Value
  59 |     | VTextShow FC Value
  60 |     | VTextReplace FC Value Value Value
  61 | 
  62 |     | VList FC Ty
  63 |     | VListLit FC (Maybe Ty) (List Value)
  64 |     | VListAppend FC Value Value
  65 |     | VListBuild FC Value Value
  66 |     | VListFold FC Value Value Value Value Value
  67 |     | VListLength FC Value Value
  68 |     | VListHead FC Value Value
  69 |     | VListLast FC Value Value
  70 |     | VListIndexed FC Value Value
  71 |     | VListReverse FC Value Value
  72 | 
  73 |     | VOptional FC Ty
  74 |     | VNone FC Ty
  75 |     | VSome FC Ty
  76 | 
  77 |     | VEquivalent FC Value Value
  78 |     | VAssert FC Value
  79 | 
  80 |     | VRecord FC (SortedMap FieldName Value)
  81 |     | VRecordLit FC (SortedMap FieldName Value)
  82 |     | VUnion FC (SortedMap FieldName (Maybe Value))
  83 |     | VField FC Value FieldName
  84 |     | VCombine FC Value Value
  85 |     | VCombineTypes FC Value Value
  86 |     | VPrefer FC Value Value
  87 |     | VMerge FC Value Value (Maybe Value)
  88 |     | VToMap FC Value (Maybe Value)
  89 |     -- TODO missing VField?
  90 |     | VInject FC (SortedMap FieldName (Maybe Value)) FieldName (Maybe Value) -- TODO proof that key is in SM?
  91 |     | VProject FC (Value) (Either (List FieldName) (Value))
  92 |     | VWith FC Value (List1 FieldName) Value
  93 | 
  94 |   public export
  95 |   data Env
  96 |     = Empty
  97 |     | Skip Env Name
  98 |     | Extend Env Name Value
  99 | 
 100 |   public export
 101 |   data VChunks = MkVChunks (List (String, Value)) String
 102 | 
 103 |   public export
 104 |   record Closure where
 105 |     constructor MkClosure
 106 |     closureName : Name
 107 |     closureEnv : Env
 108 |     closureBody : Expr Void
 109 | 
 110 |   public export
 111 |   data HLamInfo
 112 |     = Prim
 113 |     | Typed String Value
 114 |     | NaturalSubtractZero
 115 | 
 116 | ||| Returns `VHPi "_" a (\_ => Right b)`
 117 | ||| Non-dependent function arrow
 118 | public export
 119 | vFun : Value -> Value -> Value
 120 | vFun a b = VHPi initFC "_" a (\_ => Right b)
 121 | 
 122 | ||| Returns `VHLam Prim f`
 123 | public export
 124 | VPrim : (Value -> Either Error Value) -> Value
 125 | VPrim f = VHLam initFC Prim f
 126 | 
 127 | mutual
 128 |   partial
 129 |   Show HLamInfo where
 130 |     show Prim = "Prim"
 131 |     show (Typed x y) = "(Typed " ++ show x ++ " " ++ show y ++ ")"
 132 |     show NaturalSubtractZero = "NaturalSubtractZero"
 133 | 
 134 |   public export covering
 135 |   Show Env where
 136 |     show Empty = "Empty"
 137 |     show (Skip x y) = "(Skip " ++ show x ++ " " ++ show y ++ ")"
 138 |     show (Extend x y z) = "(Extend " ++ show x ++ " " ++ show y ++ " " ++ show z ++ ")"
 139 | 
 140 |   public export covering
 141 |   Show Closure where
 142 |     show (MkClosure closureName closureEnv closureBody)
 143 |       = "(MkClosure " ++ show closureName ++ " " ++ show closureEnv ++ " " ++ show closureBody ++ ")"
 144 | 
 145 |   public export covering
 146 |   Show VChunks where
 147 |     show (MkVChunks xs x) = "(MkVChunks " ++ show xs ++ " " ++ show x ++ ")"
 148 | 
 149 |   public export covering
 150 |   Show Value where
 151 |     show (VConst fc x) = "(VConst " ++ show x ++ ")"
 152 |     show (VVar fc x i) = "(VVar " ++ show x ++ " " ++ show i ++ ")"
 153 |     show (VPrimVar fc) = "VPrimVar"
 154 |     show (VApp fc x y) = "(VApp " ++ show x ++ " " ++ show y ++ ")"
 155 |     show (VLambda fc x y) = "(VLambda " ++ show x ++ " " ++ show y ++ ")"
 156 |     show (VHLam fc i x) = "(VHLam " ++ show i ++ " " ++ show (x (VPrimVar fc))
 157 |     show (VPi fc x y) = "(VPi " ++ show x ++ " " ++ show y ++ ")"
 158 |     show (VHPi fc i x y) = "(VHPi " ++ show i ++ " " ++ show x ++ show (y (VPrimVar fc))
 159 | 
 160 |     show (VBool fc) = "VBool"
 161 |     show (VBoolLit fc x) = "(VBoolLit " ++ show x ++ ")"
 162 |     show (VBoolAnd fc x y) = "(VBoolAnd " ++ show x ++ " " ++ show y ++ ")"
 163 |     show (VBoolOr fc x y) = "(VBoolOr " ++ show x ++ " " ++ show y ++ ")"
 164 |     show (VBoolEQ fc x y) = "(VBoolEQ " ++ show x ++ " " ++ show y ++ ")"
 165 |     show (VBoolNE fc x y) = "(VBoolNE " ++ show x ++ " " ++ show y ++ ")"
 166 |     show (VBoolIf fc x y z) = "(VBoolNE " ++ show x ++ " " ++ show y ++ " " ++ show y ++ ")"
 167 | 
 168 |     show (VNatural fc) = "VNatural"
 169 |     show (VNaturalLit fc k) = "(VNaturalLit " ++ show k ++ ")"
 170 |     show (VNaturalBuild fc x) = "(VNaturalBuild " ++ show x ++ ")"
 171 |     show (VNaturalFold fc w x y z) =
 172 |       "(VNaturalFold " ++ show w ++ " " ++ show x ++ " " ++ show y ++ " " ++ show z ++ ")"
 173 |     show (VNaturalIsZero fc x) = "(VNaturalIsZero " ++ show x ++ ")"
 174 |     show (VNaturalEven fc x) = "(VNaturalEven " ++ show x ++ ")"
 175 |     show (VNaturalOdd fc x) = "(VNaturalOdd " ++ show x ++ ")"
 176 |     show (VNaturalToInteger fc x) = "(VNaturalToInteger " ++ show x ++ ")"
 177 |     show (VNaturalSubtract fc x y) = "(VNaturalSubtract " ++ show x ++ " " ++ show y ++ ")"
 178 |     show (VNaturalShow fc x) = "(VNaturalShow " ++ show x ++ ")"
 179 |     show (VNaturalPlus fc x y) = "(VNaturalPlus " ++ show x ++ " " ++ show y ++ ")"
 180 |     show (VNaturalTimes fc x y) = "(VNaturalTimes " ++ show x ++ " " ++ show y ++ ")"
 181 | 
 182 |     show (VInteger fc) = "VInteger"
 183 |     show (VIntegerLit fc x) = "(VIntegerLit " ++ show x ++ ")"
 184 |     show (VIntegerShow fc x) = "(VIntegerShow " ++ show x ++ ")"
 185 |     show (VIntegerNegate fc x) = "(VIntegerNegate " ++ show x ++ ")"
 186 |     show (VIntegerClamp fc x) = "(VIntegerClamp " ++ show x ++ ")"
 187 |     show (VIntegerToDouble fc x) = "(VIntegerToDouble " ++ show x ++ ")"
 188 | 
 189 |     show (VDouble fc) = "VDouble"
 190 |     show (VDoubleLit fc k) = "(VDoubleLit " ++ show k ++ ")"
 191 |     show (VDoubleShow fc x) = "(VDoubleShow " ++ show x ++ ")"
 192 | 
 193 |     show (VText fc) = "VText"
 194 |     show (VTextLit fc x) = "(VTextLit " ++ show x ++ ")"
 195 |     show (VTextAppend fc x y) = "(VTextAppend " ++ show x ++ " " ++ show y ++ ")"
 196 |     show (VTextShow fc x) = "(VTextShow " ++ show x ++ ")"
 197 |     show (VTextReplace fc x y z) = "(VTextReplace " ++ show x ++ " " ++ show y ++ " " ++ show z ++ ")"
 198 | 
 199 |     show (VList fc a) = "(VList " ++ show a ++ ")"
 200 |     show (VListLit fc ty vs) = "(VListLit " ++ show ty ++ show vs ++ ")"
 201 |     show (VListAppend fc x y) = "(VListAppend " ++ show x ++ " " ++ show y ++ ")"
 202 |     show (VListBuild fc x y) = "(VListBuild " ++ show x ++ " " ++ show y ++ ")"
 203 |     show (VListFold fc v w x y z) =
 204 |       "(VListFold " ++ show v ++ " " ++ show w ++ " " ++ show x ++ " " ++ show y ++ " " ++ show z ++ ")"
 205 |     show (VListLength fc x y) = "(VListLength " ++ show x ++ " " ++ show y ++ ")"
 206 |     show (VListHead fc x y) = "(VListHead " ++ show x ++ " " ++ show y ++ ")"
 207 |     show (VListLast fc x y) = "(VListLast " ++ show x ++ " " ++ show y ++ ")"
 208 |     show (VListIndexed fc x y) = "(VListIndexed " ++ show x ++ " " ++ show y ++ ")"
 209 |     show (VListReverse fc x y) = "(VListReverse " ++ show x ++ " " ++ show y ++ ")"
 210 | 
 211 |     show (VOptional fc a) = "(VOptional " ++ show a ++ ")"
 212 |     show (VNone fc a) = "(VNone " ++ show a ++ ")"
 213 |     show (VSome fc a) = "(VSome " ++ show a ++ ")"
 214 | 
 215 |     show (VEquivalent fc x y) = "(VEquivalent " ++ show x ++ " " ++ show y ++ ")"
 216 |     show (VAssert fc x) = "(VAssert " ++ show x ++ ")"
 217 | 
 218 |     show (VRecord fc a) = "(VRecord $ " ++ show a ++ ")"
 219 |     show (VRecordLit fc a) = "(VRecordLit $ " ++ show a ++ ")"
 220 |     show (VUnion fc a) = "(VUnion " ++ show a ++ ")"
 221 |     show (VField fc x y) = "(VField " ++ show x ++ " " ++ show y ++ ")"
 222 |     show (VCombine fc x y) = "(VCombine " ++ show x ++ " " ++ show y ++ ")"
 223 |     show (VCombineTypes fc x y) = "(VCombineTypes " ++ show x ++ " " ++ show y ++ ")"
 224 |     show (VPrefer fc x y) = "(VPrefer " ++ show x ++ " " ++ show y ++ ")"
 225 |     show (VMerge fc x y z) = "(VMerge " ++ show x ++ " " ++ show y ++ " " ++ show z ++ ")"
 226 |     show (VToMap fc x y) = "(VToMap " ++ show x ++ " " ++ show y ++ ")"
 227 |     show (VInject fc a k v) = "(VInject " ++ show a ++ " " ++ show k ++ " " ++ show v ++ ")"
 228 |     show (VProject fc x y) = "(VProject " ++ show x ++ " " ++ show y ++ ")"
 229 |     show (VWith fc x ks y) = "(VWith " ++ show x ++ " " ++ show ks ++ " " ++ show y ++ ")"
 230 | 
 231 | public export
 232 | Semigroup VChunks where
 233 |   (<+>) (MkVChunks xys z) (MkVChunks [] z') = MkVChunks xys (z <+> z')
 234 |   (<+>) (MkVChunks xys z) (MkVChunks ((x', y') :: xys') z') = MkVChunks (xys ++ ((z <+> x', y') :: xys')) z'
 235 | 
 236 | public export
 237 | Monoid VChunks where
 238 |   neutral = MkVChunks neutral neutral
 239 | 
 240 | public export
 241 | HasFC Value where
 242 |   getFC (VConst fc x) = fc
 243 |   getFC (VVar fc x y) = fc
 244 |   getFC (VPrimVar fc) = fc
 245 |   getFC (VApp fc x y) = fc
 246 |   getFC (VLambda fc x y) = fc
 247 |   getFC (VHLam fc x f) = fc
 248 |   getFC (VPi fc x y) = fc
 249 |   getFC (VHPi fc x y f) = fc
 250 |   getFC (VBool fc) = fc
 251 |   getFC (VBoolLit fc x) = fc
 252 |   getFC (VBoolAnd fc x y) = fc
 253 |   getFC (VBoolOr fc x y) = fc
 254 |   getFC (VBoolEQ fc x y) = fc
 255 |   getFC (VBoolNE fc x y) = fc
 256 |   getFC (VBoolIf fc x y z) = fc
 257 |   getFC (VNatural fc) = fc
 258 |   getFC (VNaturalLit fc k) = fc
 259 |   getFC (VNaturalBuild fc x) = fc
 260 |   getFC (VNaturalFold fc x y z w) = fc
 261 |   getFC (VNaturalIsZero fc x) = fc
 262 |   getFC (VNaturalEven fc x) = fc
 263 |   getFC (VNaturalOdd fc x) = fc
 264 |   getFC (VNaturalSubtract fc x y) = fc
 265 |   getFC (VNaturalShow fc x) = fc
 266 |   getFC (VNaturalToInteger fc x) = fc
 267 |   getFC (VNaturalPlus fc x y) = fc
 268 |   getFC (VNaturalTimes fc x y) = fc
 269 |   getFC (VInteger fc) = fc
 270 |   getFC (VIntegerLit fc x) = fc
 271 |   getFC (VIntegerShow fc x) = fc
 272 |   getFC (VIntegerNegate fc x) = fc
 273 |   getFC (VIntegerClamp fc x) = fc
 274 |   getFC (VIntegerToDouble fc x) = fc
 275 |   getFC (VDouble fc) = fc
 276 |   getFC (VDoubleLit fc x) = fc
 277 |   getFC (VDoubleShow fc x) = fc
 278 |   getFC (VText fc) = fc
 279 |   getFC (VTextLit fc x) = fc
 280 |   getFC (VTextAppend fc x y) = fc
 281 |   getFC (VTextShow fc x) = fc
 282 |   getFC (VTextReplace fc x y z) = fc
 283 |   getFC (VList fc x) = fc
 284 |   getFC (VListLit fc x xs) = fc
 285 |   getFC (VListAppend fc x y) = fc
 286 |   getFC (VListBuild fc x y) = fc
 287 |   getFC (VListFold fc x y z w v) = fc
 288 |   getFC (VListLength fc x y) = fc
 289 |   getFC (VListHead fc x y) = fc
 290 |   getFC (VListLast fc x y) = fc
 291 |   getFC (VListIndexed fc x y) = fc
 292 |   getFC (VListReverse fc x y) = fc
 293 |   getFC (VOptional fc x) = fc
 294 |   getFC (VNone fc x) = fc
 295 |   getFC (VSome fc x) = fc
 296 |   getFC (VEquivalent fc x y) = fc
 297 |   getFC (VAssert fc x) = fc
 298 |   getFC (VRecord fc x) = fc
 299 |   getFC (VRecordLit fc x) = fc
 300 |   getFC (VUnion fc x) = fc
 301 |   getFC (VField fc x y) = fc
 302 |   getFC (VCombine fc x y) = fc
 303 |   getFC (VCombineTypes fc x y) = fc
 304 |   getFC (VPrefer fc x y) = fc
 305 |   getFC (VMerge fc x y z) = fc
 306 |   getFC (VToMap fc x y) = fc
 307 |   getFC (VInject fc x y z) = fc
 308 |   getFC (VProject fc x y) = fc
 309 |   getFC (VWith fc x xs y) = fc
 310 |