{- |
module: Factor.Value
description: Expression values
license: MIT

maintainer: Joe Leslie-Hurd <joe@gilith.com>
stability: provisional
portability: portable
-}
module Factor.Value
where

import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set

import Factor.Gfpx (Gfpx)
import qualified Factor.Gfpx as Gfpx
import Factor.Prime (Gfp,Prime)
import qualified Factor.Prime as Prime
import Factor.Term (Term(..),Var)
import qualified Factor.Term as Term
import Factor.Zx (Zx)
import qualified Factor.Zx as Zx

-------------------------------------------------------------------------------
-- Values
-------------------------------------------------------------------------------

data Value =
    ZValue Integer
  | ZxValue Zx Var
  | GfpValue Prime Gfp
  | GfpxValue Prime Gfpx Var
  deriving (Value -> Value -> Bool
(Value -> Value -> Bool) -> (Value -> Value -> Bool) -> Eq Value
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Value -> Value -> Bool
$c/= :: Value -> Value -> Bool
== :: Value -> Value -> Bool
$c== :: Value -> Value -> Bool
Eq,Eq Value
Eq Value
-> (Value -> Value -> Ordering)
-> (Value -> Value -> Bool)
-> (Value -> Value -> Bool)
-> (Value -> Value -> Bool)
-> (Value -> Value -> Bool)
-> (Value -> Value -> Value)
-> (Value -> Value -> Value)
-> Ord Value
Value -> Value -> Bool
Value -> Value -> Ordering
Value -> Value -> Value
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Value -> Value -> Value
$cmin :: Value -> Value -> Value
max :: Value -> Value -> Value
$cmax :: Value -> Value -> Value
>= :: Value -> Value -> Bool
$c>= :: Value -> Value -> Bool
> :: Value -> Value -> Bool
$c> :: Value -> Value -> Bool
<= :: Value -> Value -> Bool
$c<= :: Value -> Value -> Bool
< :: Value -> Value -> Bool
$c< :: Value -> Value -> Bool
compare :: Value -> Value -> Ordering
$ccompare :: Value -> Value -> Ordering
$cp1Ord :: Eq Value
Ord,Int -> Value -> ShowS
[Value] -> ShowS
Value -> String
(Int -> Value -> ShowS)
-> (Value -> String) -> ([Value] -> ShowS) -> Show Value
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Value] -> ShowS
$cshowList :: [Value] -> ShowS
show :: Value -> String
$cshow :: Value -> String
showsPrec :: Int -> Value -> ShowS
$cshowsPrec :: Int -> Value -> ShowS
Show)

free :: Value -> Set Var
free :: Value -> Set String
free (ZxValue Zx
_ String
x) = String -> Set String
forall a. a -> Set a
Set.singleton String
x
free (GfpxValue Prime
_ Gfpx
_ String
x) = String -> Set String
forall a. a -> Set a
Set.singleton String
x
free Value
_ = Set String
forall a. Set a
Set.empty

normalize :: Value -> Value
normalize :: Value -> Value
normalize (ZxValue Zx
f String
_) | Zx -> Bool
Zx.isConstant Zx
f =
    Prime -> Value
ZValue (Zx -> Prime
Zx.constantCoeff Zx
f)
normalize (GfpxValue Prime
p Gfpx
f String
_) | Gfpx -> Bool
Gfpx.isConstant Gfpx
f =
    Prime -> Prime -> Value
GfpValue Prime
p (Gfpx -> Prime
Gfpx.constantCoeff Gfpx
f)
normalize Value
v = Value
v

negate :: Value -> Value
negate :: Value -> Value
negate (ZValue Prime
n) = Prime -> Value
ZValue (-Prime
n)
negate (ZxValue Zx
f String
x) = Zx -> String -> Value
ZxValue (Zx -> Zx
Zx.negate Zx
f) String
x
negate (GfpValue Prime
p Prime
a) = Prime -> Prime -> Value
GfpValue Prime
p (Prime -> Prime -> Prime
Prime.negate Prime
p Prime
a)
negate (GfpxValue Prime
p Gfpx
f String
x) = Prime -> Gfpx -> String -> Value
GfpxValue Prime
p (Prime -> Gfpx -> Gfpx
Gfpx.negate Prime
p Gfpx
f) String
x

add :: Value -> Value -> Value
add :: Value -> Value -> Value
add Value
v Value
w = Value -> Value
normalize (Value -> Value) -> Value -> Value
forall a b. (a -> b) -> a -> b
$
    case Value -> Value -> (Value, Value)
align Value
v Value
w of
      (ZValue Prime
m, ZValue Prime
n) -> Prime -> Value
ZValue (Prime
m Prime -> Prime -> Prime
forall a. Num a => a -> a -> a
+ Prime
n)
      (ZxValue Zx
f String
x, ZValue Prime
n) -> Zx -> String -> Value
ZxValue (Zx -> Zx -> Zx
Zx.add Zx
f (Prime -> Zx
Zx.constant Prime
n)) String
x
      (ZValue Prime
m, ZxValue Zx
g String
x) -> Zx -> String -> Value
ZxValue (Zx -> Zx -> Zx
Zx.add (Prime -> Zx
Zx.constant Prime
m) Zx
g) String
x
      (ZxValue Zx
f String
x, ZxValue Zx
g String
_) -> Zx -> String -> Value
ZxValue (Zx -> Zx -> Zx
Zx.add Zx
f Zx
g) String
x
      (GfpValue Prime
p Prime
a, GfpValue Prime
_ Prime
b) -> Prime -> Prime -> Value
GfpValue Prime
p (Prime -> Prime -> Prime -> Prime
Prime.add Prime
p Prime
a Prime
b)
      (GfpxValue Prime
p Gfpx
f String
x, GfpValue Prime
_ Prime
b) -> Prime -> Gfpx -> String -> Value
GfpxValue Prime
p (Prime -> Gfpx -> Gfpx -> Gfpx
Gfpx.add Prime
p Gfpx
f (Prime -> Gfpx
Gfpx.constant Prime
b)) String
x
      (GfpValue Prime
p Prime
a, GfpxValue Prime
_ Gfpx
g String
x) -> Prime -> Gfpx -> String -> Value
GfpxValue Prime
p (Prime -> Gfpx -> Gfpx -> Gfpx
Gfpx.add Prime
p (Prime -> Gfpx
Gfpx.constant Prime
a) Gfpx
g) String
x
      (GfpxValue Prime
p Gfpx
f String
x, GfpxValue Prime
_ Gfpx
g String
_) -> Prime -> Gfpx -> String -> Value
GfpxValue Prime
p (Prime -> Gfpx -> Gfpx -> Gfpx
Gfpx.add Prime
p Gfpx
f Gfpx
g) String
x
      (Value, Value)
_ -> String -> Value
forall a. HasCallStack => String -> a
error (String -> Value) -> String -> Value
forall a b. (a -> b) -> a -> b
$ String
"cannot add values " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" and " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
w

subtract :: Value -> Value -> Value
subtract :: Value -> Value -> Value
subtract Value
v Value
w = Value -> Value
normalize (Value -> Value) -> Value -> Value
forall a b. (a -> b) -> a -> b
$
    case Value -> Value -> (Value, Value)
align Value
v Value
w of
      (ZValue Prime
m, ZValue Prime
n) -> Prime -> Value
ZValue (Prime
m Prime -> Prime -> Prime
forall a. Num a => a -> a -> a
- Prime
n)
      (ZxValue Zx
f String
x, ZValue Prime
n) -> Zx -> String -> Value
ZxValue (Zx -> Zx -> Zx
Zx.subtract Zx
f (Prime -> Zx
Zx.constant Prime
n)) String
x
      (ZValue Prime
m, ZxValue Zx
g String
x) -> Zx -> String -> Value
ZxValue (Zx -> Zx -> Zx
Zx.subtract (Prime -> Zx
Zx.constant Prime
m) Zx
g) String
x
      (ZxValue Zx
f String
x, ZxValue Zx
g String
_) -> Zx -> String -> Value
ZxValue (Zx -> Zx -> Zx
Zx.subtract Zx
f Zx
g) String
x
      (GfpValue Prime
p Prime
a, GfpValue Prime
_ Prime
b) -> Prime -> Prime -> Value
GfpValue Prime
p (Prime -> Prime -> Prime -> Prime
Prime.subtract Prime
p Prime
a Prime
b)
      (GfpxValue Prime
p Gfpx
f String
x, GfpValue Prime
_ Prime
b) -> Prime -> Gfpx -> String -> Value
GfpxValue Prime
p (Prime -> Gfpx -> Gfpx -> Gfpx
Gfpx.subtract Prime
p Gfpx
f (Prime -> Gfpx
Gfpx.constant Prime
b)) String
x
      (GfpValue Prime
p Prime
a, GfpxValue Prime
_ Gfpx
g String
x) -> Prime -> Gfpx -> String -> Value
GfpxValue Prime
p (Prime -> Gfpx -> Gfpx -> Gfpx
Gfpx.subtract Prime
p (Prime -> Gfpx
Gfpx.constant Prime
a) Gfpx
g) String
x
      (GfpxValue Prime
p Gfpx
f String
x, GfpxValue Prime
_ Gfpx
g String
_) -> Prime -> Gfpx -> String -> Value
GfpxValue Prime
p (Prime -> Gfpx -> Gfpx -> Gfpx
Gfpx.subtract Prime
p Gfpx
f Gfpx
g) String
x
      (Value, Value)
_ -> String -> Value
forall a. HasCallStack => String -> a
error (String -> Value) -> String -> Value
forall a b. (a -> b) -> a -> b
$ String
"cannot subtract values " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" and " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
w

multiply :: Value -> Value -> Value
multiply :: Value -> Value -> Value
multiply Value
v Value
w = Value -> Value
normalize (Value -> Value) -> Value -> Value
forall a b. (a -> b) -> a -> b
$
    case Value -> Value -> (Value, Value)
align Value
v Value
w of
      (ZValue Prime
m, ZValue Prime
n) -> Prime -> Value
ZValue (Prime
m Prime -> Prime -> Prime
forall a. Num a => a -> a -> a
* Prime
n)
      (ZxValue Zx
f String
x, ZValue Prime
n) -> Zx -> String -> Value
ZxValue (Zx -> Zx -> Zx
Zx.multiply Zx
f (Prime -> Zx
Zx.constant Prime
n)) String
x
      (ZValue Prime
m, ZxValue Zx
g String
x) -> Zx -> String -> Value
ZxValue (Zx -> Zx -> Zx
Zx.multiply (Prime -> Zx
Zx.constant Prime
m) Zx
g) String
x
      (ZxValue Zx
f String
x, ZxValue Zx
g String
_) -> Zx -> String -> Value
ZxValue (Zx -> Zx -> Zx
Zx.multiply Zx
f Zx
g) String
x
      (GfpValue Prime
p Prime
a, GfpValue Prime
_ Prime
b) -> Prime -> Prime -> Value
GfpValue Prime
p (Prime -> Prime -> Prime -> Prime
Prime.multiply Prime
p Prime
a Prime
b)
      (GfpxValue Prime
p Gfpx
f String
x, GfpValue Prime
_ Prime
b) -> Prime -> Gfpx -> String -> Value
GfpxValue Prime
p (Prime -> Gfpx -> Gfpx -> Gfpx
Gfpx.multiply Prime
p Gfpx
f (Prime -> Gfpx
Gfpx.constant Prime
b)) String
x
      (GfpValue Prime
p Prime
a, GfpxValue Prime
_ Gfpx
g String
x) -> Prime -> Gfpx -> String -> Value
GfpxValue Prime
p (Prime -> Gfpx -> Gfpx -> Gfpx
Gfpx.multiply Prime
p (Prime -> Gfpx
Gfpx.constant Prime
a) Gfpx
g) String
x
      (GfpxValue Prime
p Gfpx
f String
x, GfpxValue Prime
_ Gfpx
g String
_) -> Prime -> Gfpx -> String -> Value
GfpxValue Prime
p (Prime -> Gfpx -> Gfpx -> Gfpx
Gfpx.multiply Prime
p Gfpx
f Gfpx
g) String
x
      (Value, Value)
_ -> String -> Value
forall a. HasCallStack => String -> a
error (String -> Value) -> String -> Value
forall a b. (a -> b) -> a -> b
$ String
"cannot multiply values " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" and " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
w

exp :: Value -> Value -> Value
exp :: Value -> Value -> Value
exp (ZValue Prime
m) (ZValue Prime
n) = Prime -> Value
ZValue (Prime
m Prime -> Prime -> Prime
forall a b. (Num a, Integral b) => a -> b -> a
^ Prime
n)
exp (ZxValue Zx
f String
x) (ZValue Prime
n) = Value -> Value
normalize (Value -> Value) -> Value -> Value
forall a b. (a -> b) -> a -> b
$ Zx -> String -> Value
ZxValue (Zx -> Prime -> Zx
Zx.exp Zx
f Prime
n) String
x
exp (GfpValue Prime
p Prime
a) (ZValue Prime
n) = Prime -> Prime -> Value
GfpValue Prime
p (Prime -> Prime -> Prime -> Prime
Prime.exp Prime
p Prime
a Prime
n)
exp (GfpxValue Prime
p Gfpx
f String
x) (ZValue Prime
n) = Value -> Value
normalize (Value -> Value) -> Value -> Value
forall a b. (a -> b) -> a -> b
$ Prime -> Gfpx -> String -> Value
GfpxValue Prime
p (Prime -> Gfpx -> Prime -> Gfpx
Gfpx.exp Prime
p Gfpx
f Prime
n) String
x
exp Value
v Value
w = String -> Value
forall a. HasCallStack => String -> a
error (String -> Value) -> String -> Value
forall a b. (a -> b) -> a -> b
$ String
"cannot exponentiate values " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" and " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
w

fromTerm :: Term -> Value
fromTerm :: Term -> Value
fromTerm = Env -> Context -> Term -> Value
interpret Env
emptyEnv Context
ZContext

toTerm :: Value -> Term
toTerm :: Value -> Term
toTerm (ZValue Prime
n) = Prime -> Term
IntegerTerm Prime
n
toTerm (ZxValue Zx
f String
x) = String -> Zx -> Term
Zx.toTerm String
x Zx
f
toTerm (GfpValue Prime
p Prime
a) = Prime -> Prime -> Term
Term.fromGfp Prime
p Prime
a
toTerm (GfpxValue Prime
p Gfpx
f String
x) = Prime -> String -> Gfpx -> Term
Gfpx.toTerm Prime
p String
x Gfpx
f

toString :: Value -> String
toString :: Value -> String
toString = Term -> String
Term.toString (Term -> String) -> (Value -> Term) -> Value -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Term
toTerm

-------------------------------------------------------------------------------
-- Interpretation environments
-------------------------------------------------------------------------------

type Env = Map Var Value

emptyEnv :: Env
emptyEnv :: Env
emptyEnv = Env
forall k a. Map k a
Map.empty

lookupEnv :: Env -> Var -> Value
lookupEnv :: Env -> String -> Value
lookupEnv Env
e String
x =
    case String -> Env -> Maybe Value
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
x Env
e of
      Just Value
v -> Value
v
      Maybe Value
Nothing -> Zx -> String -> Value
ZxValue Zx
Zx.variable String
x

extendEnv :: Env -> Var -> Value -> Env
extendEnv :: Env -> String -> Value -> Env
extendEnv Env
e String
x Value
v = String -> Value -> Env -> Env
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
x Value
v Env
e

-------------------------------------------------------------------------------
-- Interpretation contexts
-------------------------------------------------------------------------------

data Context =
    ZContext
  | GfpContext Prime
  deriving (Context -> Context -> Bool
(Context -> Context -> Bool)
-> (Context -> Context -> Bool) -> Eq Context
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Context -> Context -> Bool
$c/= :: Context -> Context -> Bool
== :: Context -> Context -> Bool
$c== :: Context -> Context -> Bool
Eq,Eq Context
Eq Context
-> (Context -> Context -> Ordering)
-> (Context -> Context -> Bool)
-> (Context -> Context -> Bool)
-> (Context -> Context -> Bool)
-> (Context -> Context -> Bool)
-> (Context -> Context -> Context)
-> (Context -> Context -> Context)
-> Ord Context
Context -> Context -> Bool
Context -> Context -> Ordering
Context -> Context -> Context
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Context -> Context -> Context
$cmin :: Context -> Context -> Context
max :: Context -> Context -> Context
$cmax :: Context -> Context -> Context
>= :: Context -> Context -> Bool
$c>= :: Context -> Context -> Bool
> :: Context -> Context -> Bool
$c> :: Context -> Context -> Bool
<= :: Context -> Context -> Bool
$c<= :: Context -> Context -> Bool
< :: Context -> Context -> Bool
$c< :: Context -> Context -> Bool
compare :: Context -> Context -> Ordering
$ccompare :: Context -> Context -> Ordering
$cp1Ord :: Eq Context
Ord,Int -> Context -> ShowS
[Context] -> ShowS
Context -> String
(Int -> Context -> ShowS)
-> (Context -> String) -> ([Context] -> ShowS) -> Show Context
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Context] -> ShowS
$cshowList :: [Context] -> ShowS
show :: Context -> String
$cshow :: Context -> String
showsPrec :: Int -> Context -> ShowS
$cshowsPrec :: Int -> Context -> ShowS
Show)

combineContext :: Context -> Context -> Context
combineContext :: Context -> Context -> Context
combineContext Context
ZContext Context
c = Context
c
combineContext (GfpContext Prime
p) (GfpContext Prime
q) | Prime
p Prime -> Prime -> Bool
forall a. Eq a => a -> a -> Bool
/= Prime
q =
    String -> Context
forall a. HasCallStack => String -> a
error (String -> Context) -> String -> Context
forall a b. (a -> b) -> a -> b
$ String
"cannot combine expressions (mod " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Prime -> String
forall a. Show a => a -> String
show Prime
p String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")" String -> ShowS
forall a. [a] -> [a] -> [a]
++
            String
" and (mod " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Prime -> String
forall a. Show a => a -> String
show Prime
q String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
combineContext Context
c Context
_ = Context
c

modContext :: Value -> Context
modContext :: Value -> Context
modContext (ZValue Prime
p) = Prime -> Context
GfpContext Prime
p
modContext Value
v = String -> Context
forall a. HasCallStack => String -> a
error (String -> Context) -> String -> Context
forall a b. (a -> b) -> a -> b
$ String
"cannot calculate modulo value " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
v

-------------------------------------------------------------------------------
-- Interpreting expressions
-------------------------------------------------------------------------------

context :: Value -> Context
context :: Value -> Context
context (ZValue Prime
_) = Context
ZContext
context (ZxValue Zx
_ String
_) = Context
ZContext
context (GfpValue Prime
p Prime
_) = Prime -> Context
GfpContext Prime
p
context (GfpxValue Prime
p Gfpx
_ String
_) = Prime -> Context
GfpContext Prime
p

reduceInContext :: Context -> Value -> Value
reduceInContext :: Context -> Value -> Value
reduceInContext (GfpContext Prime
p) (ZValue Prime
n) =
    Prime -> Prime -> Value
GfpValue Prime
p (Prime -> Prime -> Prime
Prime.fromInteger Prime
p Prime
n)
reduceInContext (GfpContext Prime
p) (ZxValue Zx
f String
x) =
    Value -> Value
normalize (Prime -> Gfpx -> String -> Value
GfpxValue Prime
p (Prime -> Zx -> Gfpx
Gfpx.fromZx Prime
p Zx
f) String
x)
reduceInContext Context
_ Value
v = Value
v

importIntoContext :: Context -> Value -> Value
importIntoContext :: Context -> Value -> Value
importIntoContext Context
c Value
v = Context -> Value -> Value
reduceInContext (Context -> Context -> Context
combineContext Context
c (Value -> Context
context Value
v)) Value
v

align :: Value -> Value -> (Value,Value)
align :: Value -> Value -> (Value, Value)
align Value
v Value
w =
    if Set String -> Int
forall a. Set a -> Int
Set.size Set String
xs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1 then (Value
v',Value
w')
    else String -> (Value, Value)
forall a. HasCallStack => String -> a
error (String -> (Value, Value)) -> String -> (Value, Value)
forall a b. (a -> b) -> a -> b
$ String
"more than one free variable in values " String -> ShowS
forall a. [a] -> [a] -> [a]
++
                 Value -> String
forall a. Show a => a -> String
show Value
v' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" and " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
w'
  where
    xs :: Set String
xs = Set String -> Set String -> Set String
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Value -> Set String
free Value
v') (Value -> Set String
free Value
w')
    v' :: Value
v' = Context -> Value -> Value
reduceInContext Context
c Value
v
    w' :: Value
w' = Context -> Value -> Value
reduceInContext Context
c Value
w
    c :: Context
c = Context -> Context -> Context
combineContext (Value -> Context
context Value
v) (Value -> Context
context Value
w)

interpret :: Env -> Context -> Term -> Value
interpret :: Env -> Context -> Term -> Value
interpret Env
_ Context
c (IntegerTerm Prime
n) = Context -> Value -> Value
importIntoContext Context
c (Prime -> Value
ZValue Prime
n)
interpret Env
e Context
c (NegateTerm Term
t) = Value -> Value
Factor.Value.negate (Env -> Context -> Term -> Value
interpret Env
e Context
c Term
t)
interpret Env
e Context
c (AddTerm Term
t Term
u) = Value -> Value -> Value
add (Env -> Context -> Term -> Value
interpret Env
e Context
c Term
t) (Env -> Context -> Term -> Value
interpret Env
e Context
c Term
u)
interpret Env
e Context
c (SubtractTerm Term
t Term
u) = Value -> Value -> Value
Factor.Value.subtract (Env -> Context -> Term -> Value
interpret Env
e Context
c Term
t) (Env -> Context -> Term -> Value
interpret Env
e Context
c Term
u)
interpret Env
e Context
c (MultiplyTerm Term
t Term
u) = Value -> Value -> Value
multiply (Env -> Context -> Term -> Value
interpret Env
e Context
c Term
t) (Env -> Context -> Term -> Value
interpret Env
e Context
c Term
u)
interpret Env
e Context
c (ExpTerm Term
t Term
u) = Value -> Value -> Value
Factor.Value.exp (Env -> Context -> Term -> Value
interpret Env
e Context
c Term
t) (Env -> Context -> Term -> Value
interpret Env
e Context
ZContext Term
u)
interpret Env
e Context
c (VarTerm String
x) = Context -> Value -> Value
importIntoContext Context
c (Env -> String -> Value
lookupEnv Env
e String
x)
interpret Env
e Context
c (ModTerm Term
t Term
u) = Env -> Context -> Term -> Value
interpret Env
e Context
c' Term
t
  where c' :: Context
c' = Context -> Context -> Context
combineContext Context
c (Value -> Context
modContext (Env -> Context -> Term -> Value
interpret Env
e Context
ZContext Term
u))
interpret Env
e Context
c (LetTerm String
x Term
t Term
u) = Env -> Context -> Term -> Value
interpret Env
e' Context
c Term
u
  where e' :: Env
e' = Env -> String -> Value -> Env
extendEnv Env
e String
x (Env -> Context -> Term -> Value
interpret Env
e Context
c Term
t)
interpret Env
_ Context
_ Term
tm = String -> Value
forall a. HasCallStack => String -> a
error (String -> Value) -> String -> Value
forall a b. (a -> b) -> a -> b
$ String
"cannot interpret " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
tm