-- | Functions for computing the values of terms in the concrete syntax, in
-- | preparation for PMCFG generation.
module GF.Compile.Compute.Concrete
           (GlobalEnv, GLocation, resourceValues, geLoc, geGrammar,
            normalForm,
            Value(..), Bind(..), Env, value2term, eval, vapply
           ) where
import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint

import GF.Grammar hiding (Env, VGen, VApp, VRecType)
import GF.Grammar.Lookup(lookupResDefLoc,allParamValues)
import GF.Grammar.Predef(cPredef,cErrorType,cTok,cStr,cTrace,cPBool)
import GF.Grammar.PatternMatch(matchPattern,measurePatt)
import GF.Grammar.Lockfield(isLockLabel,lockRecType) --unlockRecord,lockLabel
import GF.Compile.Compute.Value hiding (Error)
import GF.Compile.Compute.Predef(predef,predefName,delta)
import GF.Data.Str(Str,glueStr,str2strings,str,sstr,plusStr,strTok)
import GF.Data.Operations(Err,err,errIn,maybeErr,mapPairsM)
import GF.Data.Utilities(mapFst,mapSnd)
import GF.Infra.Option
import Control.Monad(ap,liftM,liftM2) -- ,unless,mplus
import Data.List (findIndex,intersect,nub,elemIndex,(\\)) --,isInfixOf
--import Data.Char (isUpper,toUpper,toLower)
import GF.Text.Pretty
import qualified Data.Map as Map
import Debug.Trace(trace)

-- * Main entry points

normalForm :: GlobalEnv -> L Ident -> Term -> Term
normalForm :: GlobalEnv -> L Ident -> Term -> Term
normalForm (GE Grammar
gr ResourceValues
rv Options
opts L Ident
_) L Ident
loc = (String -> Term) -> (Term -> Term) -> Err Term -> Term
forall b a. (String -> b) -> (a -> b) -> Err a -> b
err (L Ident -> String -> Term
forall a1 a3 a. (Pretty a1, Pretty a3) => L a3 -> a1 -> a
bugloc L Ident
loc) Term -> Term
forall a. a -> a
id (Err Term -> Term) -> (Term -> Err Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GlobalEnv -> Term -> Err Term
nfx (Grammar -> ResourceValues -> Options -> L Ident -> GlobalEnv
GE Grammar
gr ResourceValues
rv Options
opts L Ident
loc)

nfx :: GlobalEnv -> Term -> Err Term
nfx :: GlobalEnv -> Term -> Err Term
nfx env :: GlobalEnv
env@(GE Grammar
_ ResourceValues
_ Options
_ L Ident
loc) Term
t = do
  Value
v <- GlobalEnv -> Env -> Term -> Err Value
eval GlobalEnv
env [] Term
t
  Term -> Err Term
forall (m :: * -> *) a. Monad m => a -> m a
return (L Ident -> [Ident] -> Value -> Term
value2term L Ident
loc [] Value
v)
    -- Old value2term error message:
    -- Left i  -> fail ("variable #"++show i++" is out of scope")

eval :: GlobalEnv -> Env -> Term -> Err Value
eval :: GlobalEnv -> Env -> Term -> Err Value
eval (GE Grammar
gr ResourceValues
rvs Options
opts L Ident
loc) Env
env Term
t = (([Value] -> Value) -> [Value] -> Value
forall a b. (a -> b) -> a -> b
$ (((Ident, Value) -> Value) -> Env -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map (Ident, Value) -> Value
forall a b. (a, b) -> b
snd Env
env)) (([Value] -> Value) -> Value)
-> Err ([Value] -> Value) -> Err Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
# CompleteEnv -> Term -> Err ([Value] -> Value)
value CompleteEnv
cenv Term
t
  where
    cenv :: CompleteEnv
cenv = Grammar
-> ResourceValues -> Options -> L Ident -> [Ident] -> CompleteEnv
CE Grammar
gr ResourceValues
rvs Options
opts L Ident
loc (((Ident, Value) -> Ident) -> Env -> [Ident]
forall a b. (a -> b) -> [a] -> [b]
map (Ident, Value) -> Ident
forall a b. (a, b) -> a
fst Env
env)

--apply env = apply' env

--------------------------------------------------------------------------------

-- * Environments

type ResourceValues = Map.Map ModuleName (Map.Map Ident (Err Value))

data GlobalEnv = GE Grammar ResourceValues Options GLocation
data CompleteEnv = CE {CompleteEnv -> Grammar
srcgr::Grammar,CompleteEnv -> ResourceValues
rvs::ResourceValues,
                       CompleteEnv -> Options
opts::Options,
                       CompleteEnv -> L Ident
gloc::GLocation,CompleteEnv -> [Ident]
local::LocalScope}
type GLocation = L Ident
type LocalScope = [Ident]
type Stack = [Value]
type OpenValue = Stack->Value

geLoc :: GlobalEnv -> L Ident
geLoc     (GE Grammar
_ ResourceValues
_ Options
_ L Ident
loc) = L Ident
loc
geGrammar :: GlobalEnv -> Grammar
geGrammar (GE Grammar
gr ResourceValues
_ Options
_ L Ident
_)  = Grammar
gr

ext :: Ident -> CompleteEnv -> CompleteEnv
ext Ident
b CompleteEnv
env = CompleteEnv
env{local :: [Ident]
local=Ident
bIdent -> [Ident] -> [Ident]
forall a. a -> [a] -> [a]
:CompleteEnv -> [Ident]
local CompleteEnv
env}
extend :: [Ident] -> CompleteEnv -> CompleteEnv
extend [Ident]
bs CompleteEnv
env = CompleteEnv
env{local :: [Ident]
local=[Ident]
bs[Ident] -> [Ident] -> [Ident]
forall a. [a] -> [a] -> [a]
++CompleteEnv -> [Ident]
local CompleteEnv
env}
global :: CompleteEnv -> GlobalEnv
global CompleteEnv
env = Grammar -> ResourceValues -> Options -> L Ident -> GlobalEnv
GE (CompleteEnv -> Grammar
srcgr CompleteEnv
env) (CompleteEnv -> ResourceValues
rvs CompleteEnv
env) (CompleteEnv -> Options
opts CompleteEnv
env) (CompleteEnv -> L Ident
gloc CompleteEnv
env)

var :: CompleteEnv -> Ident -> Err OpenValue
var :: CompleteEnv -> Ident -> Err ([Value] -> Value)
var CompleteEnv
env Ident
x = Err ([Value] -> Value)
-> (Int -> Err ([Value] -> Value))
-> Maybe Int
-> Err ([Value] -> Value)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Err ([Value] -> Value)
forall a. Err a
unbound Int -> Err ([Value] -> Value)
forall (m :: * -> *). Monad m => Int -> m ([Value] -> Value)
pick' (Ident -> [Ident] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex Ident
x (CompleteEnv -> [Ident]
local CompleteEnv
env))
  where
    unbound :: Err a
unbound = String -> Err a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Unknown variable: "String -> String -> String
forall a. [a] -> [a] -> [a]
++Ident -> String
showIdent Ident
x)
    pick' :: Int -> m ([Value] -> Value)
pick' Int
i = ([Value] -> Value) -> m ([Value] -> Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (([Value] -> Value) -> m ([Value] -> Value))
-> ([Value] -> Value) -> m ([Value] -> Value)
forall a b. (a -> b) -> a -> b
$ \ [Value]
vs -> Value -> (Value -> Value) -> Maybe Value -> Value
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Int -> [Value] -> Value
forall a (t :: * -> *) a a. (Show a, Foldable t) => a -> t a -> a
err Int
i [Value]
vs) Value -> Value
forall a. a -> a
ok (Int -> [Value] -> Maybe Value
pick Int
i [Value]
vs)
    err :: a -> t a -> a
err a
i t a
vs = String -> a
forall a2 a. Pretty a2 => a2 -> a
bug (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"Stack problem: "String -> String -> String
forall a. [a] -> [a] -> [a]
++Ident -> String
showIdent Ident
xString -> String -> String
forall a. [a] -> [a] -> [a]
++String
": "
                    String -> String -> String
forall a. [a] -> [a] -> [a]
++[String] -> String
unwords ((Ident -> String) -> [Ident] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Ident -> String
showIdent (CompleteEnv -> [Ident]
local CompleteEnv
env))
                    String -> String -> String
forall a. [a] -> [a] -> [a]
++String
" => "String -> String -> String
forall a. [a] -> [a] -> [a]
++(a, Int) -> String
forall a. Show a => a -> String
show (a
i,t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
vs)
    ok :: p -> p
ok p
v = --trace ("var "++show x++" = "++show v) $
           p
v

pick :: Int -> Stack -> Maybe Value
pick :: Int -> [Value] -> Maybe Value
pick Int
0 (Value
v:[Value]
_) = Value -> Maybe Value
forall a. a -> Maybe a
Just Value
v
pick Int
i (Value
_:[Value]
vs) = Int -> [Value] -> Maybe Value
pick (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [Value]
vs
pick Int
i [Value]
vs = Maybe Value
forall a. Maybe a
Nothing -- bug $ "pick "++show (i,vs)

resource :: CompleteEnv -> (ModuleName, Ident) -> Err Value
resource CompleteEnv
env (ModuleName
m,Ident
c) =
--  err bug id $
    if Ident -> Bool
isPredefCat Ident
c
    then CompleteEnv -> Term -> Err Value
value0 CompleteEnv
env (Term -> Err Value) -> Err Term -> Err Value
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Ident -> Term -> Err Term
forall (m :: * -> *). ErrorMonad m => Ident -> Term -> m Term
lockRecType Ident
c Term
defLinType -- hmm
    else Err Value
-> (Err Value -> Err Value) -> Maybe (Err Value) -> Err Value
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Err Value
forall a. Err a
e Err Value -> Err Value
forall a. a -> a
id (Maybe (Err Value) -> Err Value) -> Maybe (Err Value) -> Err Value
forall a b. (a -> b) -> a -> b
$ Ident -> Map Ident (Err Value) -> Maybe (Err Value)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Ident
c (Map Ident (Err Value) -> Maybe (Err Value))
-> Maybe (Map Ident (Err Value)) -> Maybe (Err Value)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ModuleName -> ResourceValues -> Maybe (Map Ident (Err Value))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ModuleName
m (CompleteEnv -> ResourceValues
rvs CompleteEnv
env)
  where e :: Err a
e = String -> Err a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Err a) -> String -> Err a
forall a b. (a -> b) -> a -> b
$ String
"Not found: "String -> String -> String
forall a. [a] -> [a] -> [a]
++ModuleName -> String
forall a. Pretty a => a -> String
render ModuleName
mString -> String -> String
forall a. [a] -> [a] -> [a]
++String
"."String -> String -> String
forall a. [a] -> [a] -> [a]
++Ident -> String
showIdent Ident
c

-- | Convert operators once, not every time they are looked up
resourceValues :: Options -> SourceGrammar -> GlobalEnv
resourceValues :: Options -> Grammar -> GlobalEnv
resourceValues Options
opts Grammar
gr = GlobalEnv
env
  where
    env :: GlobalEnv
env = Grammar -> ResourceValues -> Options -> L Ident -> GlobalEnv
GE Grammar
gr ResourceValues
rvs Options
opts (Location -> Ident -> L Ident
forall a. Location -> a -> L a
L Location
NoLoc Ident
identW)
    rvs :: ResourceValues
rvs = (ModuleName -> ModuleInfo -> Map Ident (Err Value))
-> Map ModuleName ModuleInfo -> ResourceValues
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey ModuleName -> ModuleInfo -> Map Ident (Err Value)
moduleResources (Grammar -> Map ModuleName ModuleInfo
moduleMap Grammar
gr)
    moduleResources :: ModuleName -> ModuleInfo -> Map Ident (Err Value)
moduleResources ModuleName
m = (Ident -> Info -> Err Value)
-> Map Ident Info -> Map Ident (Err Value)
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey (ModuleName -> Ident -> Info -> Err Value
moduleResource ModuleName
m) (Map Ident Info -> Map Ident (Err Value))
-> (ModuleInfo -> Map Ident Info)
-> ModuleInfo
-> Map Ident (Err Value)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleInfo -> Map Ident Info
jments
    moduleResource :: ModuleName -> Ident -> Info -> Err Value
moduleResource ModuleName
m Ident
c Info
_info = do L Location
l Term
t <- Grammar -> (ModuleName, Ident) -> Err (L Term)
forall (f :: * -> *).
ErrorMonad f =>
Grammar -> (ModuleName, Ident) -> f (L Term)
lookupResDefLoc Grammar
gr (ModuleName
m,Ident
c)
                                  let loc :: L Ident
loc = Location -> Ident -> L Ident
forall a. Location -> a -> L a
L Location
l Ident
c
                                      qloc :: L Term
qloc = Location -> Term -> L Term
forall a. Location -> a -> L a
L Location
l ((ModuleName, Ident) -> Term
Q (ModuleName
m,Ident
c))
                                  GlobalEnv -> Env -> Term -> Err Value
eval (Grammar -> ResourceValues -> Options -> L Ident -> GlobalEnv
GE Grammar
gr ResourceValues
rvs Options
opts L Ident
loc) [] (L Term -> Term -> Term
traceRes L Term
qloc Term
t)

    traceRes :: L Term -> Term -> Term
traceRes = if (Flags -> Bool) -> Options -> Bool
forall a. (Flags -> a) -> Options -> a
flag Flags -> Bool
optTrace Options
opts
               then L Term -> Term -> Term
traceResource
               else (Term -> Term) -> L Term -> Term -> Term
forall a b. a -> b -> a
const Term -> Term
forall a. a -> a
id

-- * Tracing

-- | Insert a call to the trace function under the top-level lambdas
traceResource :: L Term -> Term -> Term
traceResource (L Location
l Term
q) Term
t =
  case Term -> ([(BindType, Ident)], Term)
termFormCnc Term
t of
    ([(BindType, Ident)]
abs,Term
body) -> [(BindType, Ident)] -> Term -> Term
mkAbs [(BindType, Ident)]
abs (Term -> [Term] -> Term
mkApp Term
traceQ [Term
args,Term
body])
      where
        args :: Term
args = [Assign] -> Term
R ([Assign] -> Term) -> [Assign] -> Term
forall a b. (a -> b) -> a -> b
$ [Term] -> [Assign]
tuple2record (String -> Term
K String
lstrTerm -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:[Ident -> Term
Vr Ident
x|(BindType
bt,Ident
x)<-[(BindType, Ident)]
abs,BindType
btBindType -> BindType -> Bool
forall a. Eq a => a -> a -> Bool
==BindType
Explicit])
        lstr :: String
lstr = Doc -> String
forall a. Pretty a => a -> String
render (Location
lLocation -> String -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<>String
":"Doc -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<>TermPrintQual -> Integer -> Term -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Term -> Doc
ppTerm TermPrintQual
Qualified Integer
0 Term
q)
        traceQ :: Term
traceQ = (ModuleName, Ident) -> Term
Q (ModuleName
cPredef,Ident
cTrace)

-- * Computing values

-- | Computing the value of a top-level term
value0 :: CompleteEnv -> Term -> Err Value
value0 :: CompleteEnv -> Term -> Err Value
value0 CompleteEnv
env = GlobalEnv -> Env -> Term -> Err Value
eval (CompleteEnv -> GlobalEnv
global CompleteEnv
env) []

-- | Computing the value of a term
value :: CompleteEnv -> Term -> Err OpenValue
value :: CompleteEnv -> Term -> Err ([Value] -> Value)
value CompleteEnv
env Term
t0 =
  -- Each terms is traversed only once by this function, using only statically
  -- available information. Notably, the values of lambda bound variables
  -- will be unknown during the term traversal phase.
  -- The result is an OpenValue, which is a function that may be applied many
  -- times to different dynamic values, but without the term traversal overhead
  -- and without recomputing other statically known information.
  -- For this to work, there should be no recursive calls under lambdas here.
  -- Whenever we need to construct the OpenValue function with an explicit
  -- lambda, we have to lift the recursive calls outside the lambda.
  -- (See e.g. the rules for Let, Prod and Abs)
{-
  trace (render $ text "value"<+>sep [ppL (gloc env)<>text ":",
                                      brackets (fsep (map ppIdent (local env))),
                                      ppTerm Unqualified 10 t0]) $
--}
  String -> Err ([Value] -> Value) -> Err ([Value] -> Value)
forall (m :: * -> *) a. ErrorMonad m => String -> m a -> m a
errIn (Term -> String
forall a. Pretty a => a -> String
render Term
t0) (Err ([Value] -> Value) -> Err ([Value] -> Value))
-> Err ([Value] -> Value) -> Err ([Value] -> Value)
forall a b. (a -> b) -> a -> b
$
  case Term
t0 of
    Vr Ident
x   -> CompleteEnv -> Ident -> Err ([Value] -> Value)
var CompleteEnv
env Ident
x
    Q x :: (ModuleName, Ident)
x@(ModuleName
m,Ident
f)
      | ModuleName
m ModuleName -> ModuleName -> Bool
forall a. Eq a => a -> a -> Bool
== ModuleName
cPredef -> if Ident
fIdent -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
==Ident
cErrorType                -- to be removed
                        then let p :: Ident
p = String -> Ident
identS String
"P"
                             in Value -> [Value] -> Value
forall a b. a -> b -> a
const (Value -> [Value] -> Value) -> Err Value -> Err ([Value] -> Value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
# CompleteEnv -> Term -> Err Value
value0 CompleteEnv
env (Context -> Term -> [Term] -> Term
mkProd [(BindType
Implicit,Ident
p,Term
typeType)] (Ident -> Term
Vr Ident
p) [])
                        else if Ident
fIdent -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
==Ident
cPBool
                               then Value -> [Value] -> Value
forall a b. a -> b -> a
const (Value -> [Value] -> Value) -> Err Value -> Err ([Value] -> Value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
# CompleteEnv -> (ModuleName, Ident) -> Err Value
resource CompleteEnv
env (ModuleName, Ident)
x
                               else Value -> [Value] -> Value
forall a b. a -> b -> a
const (Value -> [Value] -> Value)
-> (Predefined -> Value) -> Predefined -> [Value] -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Predefined -> [Value] -> Value) -> [Value] -> Predefined -> Value
forall a b c. (a -> b -> c) -> b -> a -> c
flip Predefined -> [Value] -> Value
VApp [] (Predefined -> [Value] -> Value)
-> Err Predefined -> Err ([Value] -> Value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
# Ident -> Err Predefined
forall (m :: * -> *). MonadFail m => Ident -> m Predefined
predef Ident
f
      | Bool
otherwise    -> Value -> [Value] -> Value
forall a b. a -> b -> a
const (Value -> [Value] -> Value) -> Err Value -> Err ([Value] -> Value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
# CompleteEnv -> (ModuleName, Ident) -> Err Value
resource CompleteEnv
env (ModuleName, Ident)
x --valueResDef (fst env) x
    QC (ModuleName, Ident)
x   -> ([Value] -> Value) -> Err ([Value] -> Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (([Value] -> Value) -> Err ([Value] -> Value))
-> ([Value] -> Value) -> Err ([Value] -> Value)
forall a b. (a -> b) -> a -> b
$ Value -> [Value] -> Value
forall a b. a -> b -> a
const ((ModuleName, Ident) -> [Value] -> Value
VCApp (ModuleName, Ident)
x [])
    App Term
e1 Term
e2 -> CompleteEnv -> Term -> [[Value] -> Value] -> Err ([Value] -> Value)
apply' CompleteEnv
env Term
e1 ([[Value] -> Value] -> Err ([Value] -> Value))
-> (([Value] -> Value) -> [[Value] -> Value])
-> ([Value] -> Value)
-> Err ([Value] -> Value)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (([Value] -> Value) -> [[Value] -> Value] -> [[Value] -> Value]
forall a. a -> [a] -> [a]
:[]) (([Value] -> Value) -> Err ([Value] -> Value))
-> Err ([Value] -> Value) -> Err ([Value] -> Value)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< CompleteEnv -> Term -> Err ([Value] -> Value)
value CompleteEnv
env Term
e2
    Let (Ident
x,(Maybe Term
oty,Term
t)) Term
body -> do [Value] -> Value
vb <- CompleteEnv -> Term -> Err ([Value] -> Value)
value (Ident -> CompleteEnv -> CompleteEnv
ext Ident
x CompleteEnv
env) Term
body
                               [Value] -> Value
vt <- CompleteEnv -> Term -> Err ([Value] -> Value)
value CompleteEnv
env Term
t
                               ([Value] -> Value) -> Err ([Value] -> Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (([Value] -> Value) -> Err ([Value] -> Value))
-> ([Value] -> Value) -> Err ([Value] -> Value)
forall a b. (a -> b) -> a -> b
$ \ [Value]
vs -> [Value] -> Value
vb ([Value] -> Value
vt [Value]
vsValue -> [Value] -> [Value]
forall a. a -> [a] -> [a]
:[Value]
vs)
    Meta Int
i -> ([Value] -> Value) -> Err ([Value] -> Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (([Value] -> Value) -> Err ([Value] -> Value))
-> ([Value] -> Value) -> Err ([Value] -> Value)
forall a b. (a -> b) -> a -> b
$ \ [Value]
vs -> Int -> Env -> [Value] -> Value
VMeta Int
i ([Ident] -> [Value] -> Env
forall a b. [a] -> [b] -> [(a, b)]
zip (CompleteEnv -> [Ident]
local CompleteEnv
env) [Value]
vs) []
    Prod BindType
bt Ident
x Term
t1 Term
t2 ->
       do [Value] -> Value
vt1 <- CompleteEnv -> Term -> Err ([Value] -> Value)
value CompleteEnv
env Term
t1
          [Value] -> Value
vt2 <- CompleteEnv -> Term -> Err ([Value] -> Value)
value (Ident -> CompleteEnv -> CompleteEnv
ext Ident
x CompleteEnv
env) Term
t2
          ([Value] -> Value) -> Err ([Value] -> Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (([Value] -> Value) -> Err ([Value] -> Value))
-> ([Value] -> Value) -> Err ([Value] -> Value)
forall a b. (a -> b) -> a -> b
$ \ [Value]
vs -> BindType -> Value -> Ident -> Binding -> Value
VProd BindType
bt ([Value] -> Value
vt1 [Value]
vs) Ident
x (Binding -> Value) -> Binding -> Value
forall a b. (a -> b) -> a -> b
$ (Value -> Value) -> Binding
forall a. (a -> Value) -> Bind a
Bind ((Value -> Value) -> Binding) -> (Value -> Value) -> Binding
forall a b. (a -> b) -> a -> b
$ \ Value
vx -> [Value] -> Value
vt2 (Value
vxValue -> [Value] -> [Value]
forall a. a -> [a] -> [a]
:[Value]
vs)
    Abs BindType
bt Ident
x Term
t -> do [Value] -> Value
vt <- CompleteEnv -> Term -> Err ([Value] -> Value)
value (Ident -> CompleteEnv -> CompleteEnv
ext Ident
x CompleteEnv
env) Term
t
                     ([Value] -> Value) -> Err ([Value] -> Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (([Value] -> Value) -> Err ([Value] -> Value))
-> ([Value] -> Value) -> Err ([Value] -> Value)
forall a b. (a -> b) -> a -> b
$ BindType -> Ident -> Binding -> Value
VAbs BindType
bt Ident
x (Binding -> Value) -> ([Value] -> Binding) -> [Value] -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Value -> Value) -> Binding
forall a. (a -> Value) -> Bind a
Bind ((Value -> Value) -> Binding)
-> ([Value] -> Value -> Value) -> [Value] -> Binding
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \ [Value]
vs Value
vx -> [Value] -> Value
vt (Value
vxValue -> [Value] -> [Value]
forall a. a -> [a] -> [a]
:[Value]
vs)
    EInt Int
n -> ([Value] -> Value) -> Err ([Value] -> Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (([Value] -> Value) -> Err ([Value] -> Value))
-> ([Value] -> Value) -> Err ([Value] -> Value)
forall a b. (a -> b) -> a -> b
$ Value -> [Value] -> Value
forall a b. a -> b -> a
const (Int -> Value
VInt Int
n)
    EFloat Double
f -> ([Value] -> Value) -> Err ([Value] -> Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (([Value] -> Value) -> Err ([Value] -> Value))
-> ([Value] -> Value) -> Err ([Value] -> Value)
forall a b. (a -> b) -> a -> b
$ Value -> [Value] -> Value
forall a b. a -> b -> a
const (Double -> Value
VFloat Double
f)
    K String
s -> ([Value] -> Value) -> Err ([Value] -> Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (([Value] -> Value) -> Err ([Value] -> Value))
-> ([Value] -> Value) -> Err ([Value] -> Value)
forall a b. (a -> b) -> a -> b
$ Value -> [Value] -> Value
forall a b. a -> b -> a
const (String -> Value
VString String
s)
    Term
Empty -> ([Value] -> Value) -> Err ([Value] -> Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (([Value] -> Value) -> Err ([Value] -> Value))
-> ([Value] -> Value) -> Err ([Value] -> Value)
forall a b. (a -> b) -> a -> b
$ Value -> [Value] -> Value
forall a b. a -> b -> a
const (String -> Value
VString String
"")
    Sort Ident
s | Ident
s Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
cTok -> ([Value] -> Value) -> Err ([Value] -> Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (([Value] -> Value) -> Err ([Value] -> Value))
-> ([Value] -> Value) -> Err ([Value] -> Value)
forall a b. (a -> b) -> a -> b
$ Value -> [Value] -> Value
forall a b. a -> b -> a
const (Ident -> Value
VSort Ident
cStr)        -- to be removed
           | Bool
otherwise -> ([Value] -> Value) -> Err ([Value] -> Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (([Value] -> Value) -> Err ([Value] -> Value))
-> ([Value] -> Value) -> Err ([Value] -> Value)
forall a b. (a -> b) -> a -> b
$ Value -> [Value] -> Value
forall a b. a -> b -> a
const (Ident -> Value
VSort Ident
s)
    ImplArg Term
t -> (Value -> Value
VImplArg(Value -> Value) -> ([Value] -> Value) -> [Value] -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) (([Value] -> Value) -> [Value] -> Value)
-> Err ([Value] -> Value) -> Err ([Value] -> Value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
# CompleteEnv -> Term -> Err ([Value] -> Value)
value CompleteEnv
env Term
t
    Table Term
p Term
res -> (Value -> Value -> Value)
-> ([Value] -> Value) -> ([Value] -> Value) -> [Value] -> Value
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Value -> Value -> Value
VTblType (([Value] -> Value) -> ([Value] -> Value) -> [Value] -> Value)
-> Err ([Value] -> Value)
-> Err (([Value] -> Value) -> [Value] -> Value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
# CompleteEnv -> Term -> Err ([Value] -> Value)
value CompleteEnv
env Term
p Err (([Value] -> Value) -> [Value] -> Value)
-> Err ([Value] -> Value) -> Err ([Value] -> Value)
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
<# CompleteEnv -> Term -> Err ([Value] -> Value)
value CompleteEnv
env Term
res
    RecType [Labelling]
rs -> do [(Label, [Value] -> Value)]
lovs <- (Term -> Err ([Value] -> Value))
-> [Labelling] -> Err [(Label, [Value] -> Value)]
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> [(a, b)] -> m [(a, c)]
mapPairsM (CompleteEnv -> Term -> Err ([Value] -> Value)
value CompleteEnv
env) [Labelling]
rs
                     ([Value] -> Value) -> Err ([Value] -> Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (([Value] -> Value) -> Err ([Value] -> Value))
-> ([Value] -> Value) -> Err ([Value] -> Value)
forall a b. (a -> b) -> a -> b
$ \[Value]
vs->[(Label, Value)] -> Value
VRecType ([(Label, Value)] -> Value) -> [(Label, Value)] -> Value
forall a b. (a -> b) -> a -> b
$ (([Value] -> Value) -> Value)
-> [(Label, [Value] -> Value)] -> [(Label, Value)]
forall b b' a. (b -> b') -> [(a, b)] -> [(a, b')]
mapSnd (([Value] -> Value) -> [Value] -> Value
forall a b. (a -> b) -> a -> b
$[Value]
vs) [(Label, [Value] -> Value)]
lovs
    t :: Term
t@(ExtR Term
t1 Term
t2) -> ((Term -> (Value, Value) -> Value
extR Term
t((Value, Value) -> Value)
-> ([Value] -> (Value, Value)) -> [Value] -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
.)(([Value] -> (Value, Value)) -> [Value] -> Value)
-> (([Value] -> Value, [Value] -> Value)
    -> [Value] -> (Value, Value))
-> ([Value] -> Value, [Value] -> Value)
-> [Value]
-> Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
# (([Value] -> Value) -> [Value] -> Value)
-> ([Value] -> Value, [Value] -> Value)
-> [Value]
-> (Value, Value)
forall (m :: * -> *) t a.
Monad m =>
(t -> m a) -> (t, t) -> m (a, a)
both ([Value] -> Value) -> [Value] -> Value
forall a. a -> a
id) (([Value] -> Value, [Value] -> Value) -> [Value] -> Value)
-> Err ([Value] -> Value, [Value] -> Value)
-> Err ([Value] -> Value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
# (Term -> Err ([Value] -> Value))
-> (Term, Term) -> Err ([Value] -> Value, [Value] -> Value)
forall (m :: * -> *) t a.
Monad m =>
(t -> m a) -> (t, t) -> m (a, a)
both (CompleteEnv -> Term -> Err ([Value] -> Value)
value CompleteEnv
env) (Term
t1,Term
t2)
    FV [Term]
ts   -> (([Value] -> Value
vfv ([Value] -> Value) -> ([Value] -> [Value]) -> [Value] -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) (([Value] -> [Value]) -> [Value] -> Value)
-> ([[Value] -> Value] -> [Value] -> [Value])
-> [[Value] -> Value]
-> [Value]
-> Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
# [[Value] -> Value] -> [Value] -> [Value]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence) ([[Value] -> Value] -> [Value] -> Value)
-> Err [[Value] -> Value] -> Err ([Value] -> Value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
# (Term -> Err ([Value] -> Value))
-> [Term] -> Err [[Value] -> Value]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (CompleteEnv -> Term -> Err ([Value] -> Value)
value CompleteEnv
env) [Term]
ts
    R [Assign]
as    -> do [(Label, [Value] -> Value)]
lovs <- ((Maybe Term, Term) -> Err ([Value] -> Value))
-> [Assign] -> Err [(Label, [Value] -> Value)]
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> [(a, b)] -> m [(a, c)]
mapPairsM (CompleteEnv -> Term -> Err ([Value] -> Value)
value CompleteEnv
env(Term -> Err ([Value] -> Value))
-> ((Maybe Term, Term) -> Term)
-> (Maybe Term, Term)
-> Err ([Value] -> Value)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Maybe Term, Term) -> Term
forall a b. (a, b) -> b
snd) [Assign]
as
                  ([Value] -> Value) -> Err ([Value] -> Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (([Value] -> Value) -> Err ([Value] -> Value))
-> ([Value] -> Value) -> Err ([Value] -> Value)
forall a b. (a -> b) -> a -> b
$ \ [Value]
vs->[(Label, Value)] -> Value
VRec ([(Label, Value)] -> Value) -> [(Label, Value)] -> Value
forall a b. (a -> b) -> a -> b
$ (([Value] -> Value) -> Value)
-> [(Label, [Value] -> Value)] -> [(Label, Value)]
forall b b' a. (b -> b') -> [(a, b)] -> [(a, b')]
mapSnd (([Value] -> Value) -> [Value] -> Value
forall a b. (a -> b) -> a -> b
$[Value]
vs) [(Label, [Value] -> Value)]
lovs
    T TInfo
i [Case]
cs  -> CompleteEnv -> TInfo -> [Case] -> Err ([Value] -> Value)
valueTable CompleteEnv
env TInfo
i [Case]
cs
    V Term
ty [Term]
ts -> do [Value]
pvs <- CompleteEnv -> Term -> Err [Value]
paramValues CompleteEnv
env Term
ty
                  ((Term -> [Value] -> [Value] -> Value
VV Term
ty [Value]
pvs ([Value] -> Value) -> ([Value] -> [Value]) -> [Value] -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) (([Value] -> [Value]) -> [Value] -> Value)
-> ([[Value] -> Value] -> [Value] -> [Value])
-> [[Value] -> Value]
-> [Value]
-> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Value] -> Value] -> [Value] -> [Value]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence) ([[Value] -> Value] -> [Value] -> Value)
-> Err [[Value] -> Value] -> Err ([Value] -> Value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
# (Term -> Err ([Value] -> Value))
-> [Term] -> Err [[Value] -> Value]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (CompleteEnv -> Term -> Err ([Value] -> Value)
value CompleteEnv
env) [Term]
ts
    C Term
t1 Term
t2 -> ((((Value, Value) -> Value) -> (Value, Value) -> Value
ok2p (Value, Value) -> Value
vconcat((Value, Value) -> Value)
-> ([Value] -> (Value, Value)) -> [Value] -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) (([Value] -> (Value, Value)) -> [Value] -> Value)
-> (([Value] -> Value, [Value] -> Value)
    -> [Value] -> (Value, Value))
-> ([Value] -> Value, [Value] -> Value)
-> [Value]
-> Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
# (([Value] -> Value) -> [Value] -> Value)
-> ([Value] -> Value, [Value] -> Value)
-> [Value]
-> (Value, Value)
forall (m :: * -> *) t a.
Monad m =>
(t -> m a) -> (t, t) -> m (a, a)
both ([Value] -> Value) -> [Value] -> Value
forall a. a -> a
id) (([Value] -> Value, [Value] -> Value) -> [Value] -> Value)
-> Err ([Value] -> Value, [Value] -> Value)
-> Err ([Value] -> Value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
# (Term -> Err ([Value] -> Value))
-> (Term, Term) -> Err ([Value] -> Value, [Value] -> Value)
forall (m :: * -> *) t a.
Monad m =>
(t -> m a) -> (t, t) -> m (a, a)
both (CompleteEnv -> Term -> Err ([Value] -> Value)
value CompleteEnv
env) (Term
t1,Term
t2)
    S Term
t1 Term
t2 -> ((CompleteEnv -> (Value, Value) -> Value
select CompleteEnv
env((Value, Value) -> Value)
-> ([Value] -> (Value, Value)) -> [Value] -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) (([Value] -> (Value, Value)) -> [Value] -> Value)
-> (([Value] -> Value, [Value] -> Value)
    -> [Value] -> (Value, Value))
-> ([Value] -> Value, [Value] -> Value)
-> [Value]
-> Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
# (([Value] -> Value) -> [Value] -> Value)
-> ([Value] -> Value, [Value] -> Value)
-> [Value]
-> (Value, Value)
forall (m :: * -> *) t a.
Monad m =>
(t -> m a) -> (t, t) -> m (a, a)
both ([Value] -> Value) -> [Value] -> Value
forall a. a -> a
id) (([Value] -> Value, [Value] -> Value) -> [Value] -> Value)
-> Err ([Value] -> Value, [Value] -> Value)
-> Err ([Value] -> Value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
# (Term -> Err ([Value] -> Value))
-> (Term, Term) -> Err ([Value] -> Value, [Value] -> Value)
forall (m :: * -> *) t a.
Monad m =>
(t -> m a) -> (t, t) -> m (a, a)
both (CompleteEnv -> Term -> Err ([Value] -> Value)
value CompleteEnv
env) (Term
t1,Term
t2)
    P Term
t Label
l   -> --maybe (bug $ "project "++show l++" from "++show v) id $
               do [Value] -> Value
ov <- CompleteEnv -> Term -> Err ([Value] -> Value)
value CompleteEnv
env Term
t
                  ([Value] -> Value) -> Err ([Value] -> Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (([Value] -> Value) -> Err ([Value] -> Value))
-> ([Value] -> Value) -> Err ([Value] -> Value)
forall a b. (a -> b) -> a -> b
$ \ [Value]
vs -> let v :: Value
v = [Value] -> Value
ov [Value]
vs
                                   in Value -> (Value -> Value) -> Maybe Value -> Value
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Value -> Label -> Value
VP Value
v Label
l) Value -> Value
forall a. a -> a
id (Label -> Value -> Maybe Value
proj Label
l Value
v)
    Alts Term
t [(Term, Term)]
tts -> (\[Value] -> Value
v [([Value] -> Value, [Value] -> Value)]
vts -> Value -> [(Value, Value)] -> Value
VAlts (Value -> [(Value, Value)] -> Value)
-> ([Value] -> Value) -> [Value] -> [(Value, Value)] -> Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
# [Value] -> Value
v ([Value] -> [(Value, Value)] -> Value)
-> ([Value] -> [(Value, Value)]) -> [Value] -> Value
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
<# (([Value] -> Value, [Value] -> Value) -> [Value] -> (Value, Value))
-> [([Value] -> Value, [Value] -> Value)]
-> [Value]
-> [(Value, Value)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((([Value] -> Value) -> [Value] -> Value)
-> ([Value] -> Value, [Value] -> Value)
-> [Value]
-> (Value, Value)
forall (m :: * -> *) t a.
Monad m =>
(t -> m a) -> (t, t) -> m (a, a)
both ([Value] -> Value) -> [Value] -> Value
forall a. a -> a
id) [([Value] -> Value, [Value] -> Value)]
vts) (([Value] -> Value)
 -> [([Value] -> Value, [Value] -> Value)] -> [Value] -> Value)
-> Err ([Value] -> Value)
-> Err ([([Value] -> Value, [Value] -> Value)] -> [Value] -> Value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
# CompleteEnv -> Term -> Err ([Value] -> Value)
value CompleteEnv
env Term
t Err ([([Value] -> Value, [Value] -> Value)] -> [Value] -> Value)
-> Err [([Value] -> Value, [Value] -> Value)]
-> Err ([Value] -> Value)
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
<# ((Term, Term) -> Err ([Value] -> Value, [Value] -> Value))
-> [(Term, Term)] -> Err [([Value] -> Value, [Value] -> Value)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Term -> Err ([Value] -> Value))
-> (Term, Term) -> Err ([Value] -> Value, [Value] -> Value)
forall (m :: * -> *) t a.
Monad m =>
(t -> m a) -> (t, t) -> m (a, a)
both (CompleteEnv -> Term -> Err ([Value] -> Value)
value CompleteEnv
env)) [(Term, Term)]
tts
    Strs [Term]
ts    -> (([Value] -> Value
VStrs([Value] -> Value) -> ([Value] -> [Value]) -> [Value] -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) (([Value] -> [Value]) -> [Value] -> Value)
-> ([[Value] -> Value] -> [Value] -> [Value])
-> [[Value] -> Value]
-> [Value]
-> Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
# [[Value] -> Value] -> [Value] -> [Value]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence) ([[Value] -> Value] -> [Value] -> Value)
-> Err [[Value] -> Value] -> Err ([Value] -> Value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
# (Term -> Err ([Value] -> Value))
-> [Term] -> Err [[Value] -> Value]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (CompleteEnv -> Term -> Err ([Value] -> Value)
value CompleteEnv
env) [Term]
ts
    Glue Term
t1 Term
t2 -> ((((Value, Value) -> Value) -> (Value, Value) -> Value
ok2p (CompleteEnv -> (Value, Value) -> Value
glue CompleteEnv
env)((Value, Value) -> Value)
-> ([Value] -> (Value, Value)) -> [Value] -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) (([Value] -> (Value, Value)) -> [Value] -> Value)
-> (([Value] -> Value, [Value] -> Value)
    -> [Value] -> (Value, Value))
-> ([Value] -> Value, [Value] -> Value)
-> [Value]
-> Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
# (([Value] -> Value) -> [Value] -> Value)
-> ([Value] -> Value, [Value] -> Value)
-> [Value]
-> (Value, Value)
forall (m :: * -> *) t a.
Monad m =>
(t -> m a) -> (t, t) -> m (a, a)
both ([Value] -> Value) -> [Value] -> Value
forall a. a -> a
id) (([Value] -> Value, [Value] -> Value) -> [Value] -> Value)
-> Err ([Value] -> Value, [Value] -> Value)
-> Err ([Value] -> Value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
# (Term -> Err ([Value] -> Value))
-> (Term, Term) -> Err ([Value] -> Value, [Value] -> Value)
forall (m :: * -> *) t a.
Monad m =>
(t -> m a) -> (t, t) -> m (a, a)
both (CompleteEnv -> Term -> Err ([Value] -> Value)
value CompleteEnv
env) (Term
t1,Term
t2)
    ELin Ident
c Term
r -> (L Ident -> Ident -> Value -> Value
forall p p p. p -> p -> p -> p
unlockVRec (CompleteEnv -> L Ident
gloc CompleteEnv
env) Ident
c(Value -> Value) -> ([Value] -> Value) -> [Value] -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) (([Value] -> Value) -> [Value] -> Value)
-> Err ([Value] -> Value) -> Err ([Value] -> Value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
# CompleteEnv -> Term -> Err ([Value] -> Value)
value CompleteEnv
env Term
r
    EPatt Patt
p  -> ([Value] -> Value) -> Err ([Value] -> Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (([Value] -> Value) -> Err ([Value] -> Value))
-> ([Value] -> Value) -> Err ([Value] -> Value)
forall a b. (a -> b) -> a -> b
$ Value -> [Value] -> Value
forall a b. a -> b -> a
const (Patt -> Value
VPatt Patt
p) -- hmm
    EPattType Term
ty -> do [Value] -> Value
vt <- CompleteEnv -> Term -> Err ([Value] -> Value)
value CompleteEnv
env Term
ty
                       ([Value] -> Value) -> Err ([Value] -> Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Value
VPattType (Value -> Value) -> ([Value] -> Value) -> [Value] -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Value] -> Value
vt)
    Typed Term
t Term
ty -> CompleteEnv -> Term -> Err ([Value] -> Value)
value CompleteEnv
env Term
t
    Term
t -> String -> Err ([Value] -> Value)
forall (m :: * -> *) a. MonadFail m => String -> m a
fail(String -> Err ([Value] -> Value))
-> (Doc -> String) -> Doc -> Err ([Value] -> Value)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Doc -> String
forall a. Pretty a => a -> String
render (Doc -> Err ([Value] -> Value)) -> Doc -> Err ([Value] -> Value)
forall a b. (a -> b) -> a -> b
$ String
"value"String -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+>TermPrintQual -> Integer -> Term -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Term -> Doc
ppTerm TermPrintQual
Unqualified Integer
10 Term
t Doc -> String -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$ Term -> String
forall a. Show a => a -> String
show Term
t

vconcat :: (Value, Value) -> Value
vconcat vv :: (Value, Value)
vv@(Value
v1,Value
v2) =
    case (Value, Value)
vv of
      (VString String
"",Value
_) -> Value
v2
      (Value
_,VString String
"") -> Value
v1
      (VApp Predefined
NonExist [Value]
_,Value
_) -> Value
v1
      (Value
_,VApp Predefined
NonExist [Value]
_) -> Value
v2
      (Value, Value)
_ -> Value -> Value -> Value
VC Value
v1 Value
v2

proj :: Label -> Value -> Maybe Value
proj Label
l Value
v | Label -> Bool
isLockLabel Label
l = Value -> Maybe Value
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Label, Value)] -> Value
VRec [])
                ---- a workaround 18/2/2005: take this away and find the reason
                ---- why earlier compilation destroys the lock field
proj Label
l Value
v =
    case Value
v of
      VFV [Value]
vs -> ([Value] -> Value) -> Maybe [Value] -> Maybe Value
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [Value] -> Value
vfv ((Value -> Maybe Value) -> [Value] -> Maybe [Value]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Label -> Value -> Maybe Value
proj Label
l) [Value]
vs)
      VRec [(Label, Value)]
rs -> Label -> [(Label, Value)] -> Maybe Value
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Label
l [(Label, Value)]
rs
--    VExtR v1 v2 -> proj l v2 `mplus` proj l v1 -- hmm
      VS (VV Term
pty [Value]
pvs [Value]
rs) Value
v2 -> (Value -> Value -> Value) -> Value -> Value -> Value
forall a b c. (a -> b -> c) -> b -> a -> c
flip Value -> Value -> Value
VS Value
v2 (Value -> Value) -> ([Value] -> Value) -> [Value] -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> [Value] -> [Value] -> Value
VV Term
pty [Value]
pvs ([Value] -> Value) -> Maybe [Value] -> Maybe Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
# (Value -> Maybe Value) -> [Value] -> Maybe [Value]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Label -> Value -> Maybe Value
proj Label
l) [Value]
rs
      Value
_ -> Value -> Maybe Value
forall (m :: * -> *) a. Monad m => a -> m a
return ((Value -> Label -> Value) -> Value -> Label -> Value
forall t. (Value -> t -> Value) -> Value -> t -> Value
ok1 Value -> Label -> Value
VP Value
v Label
l)

ok1 :: (Value -> t -> Value) -> Value -> t -> Value
ok1 Value -> t -> Value
f v1 :: Value
v1@(VError {}) t
_ = Value
v1
ok1 Value -> t -> Value
f Value
v1 t
v2 = Value -> t -> Value
f Value
v1 t
v2

ok2 :: (Value -> Value -> Value) -> Value -> Value -> Value
ok2 Value -> Value -> Value
f v1 :: Value
v1@(VError {}) Value
_ = Value
v1
ok2 Value -> Value -> Value
f Value
_ v2 :: Value
v2@(VError {}) = Value
v2
ok2 Value -> Value -> Value
f Value
v1 Value
v2 = Value -> Value -> Value
f Value
v1 Value
v2

ok2p :: ((Value, Value) -> Value) -> (Value, Value) -> Value
ok2p (Value, Value) -> Value
f (v1 :: Value
v1@VError {},Value
_) = Value
v1
ok2p (Value, Value) -> Value
f (Value
_,v2 :: Value
v2@VError {}) = Value
v2
ok2p (Value, Value) -> Value
f (Value, Value)
vv = (Value, Value) -> Value
f (Value, Value)
vv

unlockVRec :: p -> p -> p -> p
unlockVRec p
loc p
c0 p
v0 = p
v0
{-
unlockVRec loc c0 v0 = unlockVRec' c0 v0
  where
    unlockVRec' ::Ident -> Value -> Value
    unlockVRec' c v =
        case v of
    --    VClosure env t -> err bug (VClosure env) (unlockRecord c t)
          VAbs bt x (Bind f) -> VAbs bt x (Bind $ \ v -> unlockVRec' c (f v))
          VRec rs        -> plusVRec rs lock
    --    _              -> VExtR v (VRec lock) -- hmm
          _              -> {-trace (render $ ppL loc $ "unlock non-record "++show v0)-} v -- hmm
    --    _              -> bugloc loc $ "unlock non-record "++show v0
      where
        lock = [(lockLabel c,VRec [])]
-}

-- suspicious, but backwards compatible
plusVRec :: [(Label, Value)] -> [(Label, Value)] -> Value
plusVRec [(Label, Value)]
rs1 [(Label, Value)]
rs2 = [(Label, Value)] -> Value
VRec ([(Label
l,Value
v)|(Label
l,Value
v)<-[(Label, Value)]
rs1,Label
l Label -> [Label] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Label]
ls2] [(Label, Value)] -> [(Label, Value)] -> [(Label, Value)]
forall a. [a] -> [a] -> [a]
++ [(Label, Value)]
rs2)
  where ls2 :: [Label]
ls2 = ((Label, Value) -> Label) -> [(Label, Value)] -> [Label]
forall a b. (a -> b) -> [a] -> [b]
map (Label, Value) -> Label
forall a b. (a, b) -> a
fst [(Label, Value)]
rs2

extR :: Term -> (Value, Value) -> Value
extR Term
t (Value, Value)
vv =
    case (Value, Value)
vv of
      (VFV [Value]
vs,Value
v2) -> [Value] -> Value
vfv [Term -> (Value, Value) -> Value
extR Term
t (Value
v1,Value
v2)|Value
v1<-[Value]
vs]
      (Value
v1,VFV [Value]
vs) -> [Value] -> Value
vfv [Term -> (Value, Value) -> Value
extR Term
t (Value
v1,Value
v2)|Value
v2<-[Value]
vs]
      (VRecType [(Label, Value)]
rs1, VRecType [(Label, Value)]
rs2) ->
          case [Label] -> [Label] -> [Label]
forall a. Eq a => [a] -> [a] -> [a]
intersect (((Label, Value) -> Label) -> [(Label, Value)] -> [Label]
forall a b. (a -> b) -> [a] -> [b]
map (Label, Value) -> Label
forall a b. (a, b) -> a
fst [(Label, Value)]
rs1) (((Label, Value) -> Label) -> [(Label, Value)] -> [Label]
forall a b. (a -> b) -> [a] -> [b]
map (Label, Value) -> Label
forall a b. (a, b) -> a
fst [(Label, Value)]
rs2) of
            [] -> [(Label, Value)] -> Value
VRecType ([(Label, Value)]
rs1 [(Label, Value)] -> [(Label, Value)] -> [(Label, Value)]
forall a. [a] -> [a] -> [a]
++ [(Label, Value)]
rs2)
            [Label]
ls -> Doc -> Value
forall a2 a. Pretty a2 => a2 -> a
error (Doc -> Value) -> Doc -> Value
forall a b. (a -> b) -> a -> b
$ String
"clash"String -> String -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+>[Label] -> String
forall a. Show a => a -> String
show [Label]
ls
      (VRec     [(Label, Value)]
rs1, VRec     [(Label, Value)]
rs2) -> [(Label, Value)] -> [(Label, Value)] -> Value
plusVRec [(Label, Value)]
rs1 [(Label, Value)]
rs2
      (Value
v1          , VRec [(Label
l,Value
_)]) | Label -> Bool
isLockLabel Label
l -> Value
v1 -- hmm
      (VS (VV Term
t [Value]
pvs [Value]
vs) Value
s,Value
v2) -> Value -> Value -> Value
VS (Term -> [Value] -> [Value] -> Value
VV Term
t [Value]
pvs [Term -> (Value, Value) -> Value
extR Term
t (Value
v1,Value
v2)|Value
v1<-[Value]
vs]) Value
s
--    (v1,v2) -> ok2 VExtR v1 v2 -- hmm
      (Value
v1,Value
v2) -> Doc -> Value
forall a2 a. Pretty a2 => a2 -> a
error (Doc -> Value) -> Doc -> Value
forall a b. (a -> b) -> a -> b
$ String
"not records" String -> String -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$ Value -> String
forall a. Show a => a -> String
show Value
v1 Doc -> String -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$ Value -> String
forall a. Show a => a -> String
show Value
v2
  where
    error :: a2 -> a
error a2
explain = Doc -> a
forall a2 a. Pretty a2 => a2 -> a
ppbug (Doc -> a) -> Doc -> a
forall a b. (a -> b) -> a -> b
$ String
"The term" String -> Term -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Term
t
                            Doc -> String -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> String
"is not reducible" Doc -> a2 -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
$$ a2
explain

glue :: CompleteEnv -> (Value, Value) -> Value
glue CompleteEnv
env (Value
v1,Value
v2) = Value -> Value -> Value
glu Value
v1 Value
v2
  where
    glu :: Value -> Value -> Value
glu Value
v1 Value
v2 =
        case (Value
v1,Value
v2) of
          (VFV [Value]
vs,Value
v2) -> [Value] -> Value
vfv [Value -> Value -> Value
glu Value
v1 Value
v2|Value
v1<-[Value]
vs]
          (Value
v1,VFV [Value]
vs) -> [Value] -> Value
vfv [Value -> Value -> Value
glu Value
v1 Value
v2|Value
v2<-[Value]
vs]
          (VString String
s1,VString String
s2) -> String -> Value
VString (String
s1String -> String -> String
forall a. [a] -> [a] -> [a]
++String
s2)
          (Value
v1,VAlts Value
d [(Value, Value)]
vs) -> Value -> [(Value, Value)] -> Value
VAlts (Value -> Value
glx Value
d) [(Value -> Value
glx Value
v,Value
c) | (Value
v,Value
c) <- [(Value, Value)]
vs]
             where glx :: Value -> Value
glx Value
v2 = Value -> Value -> Value
glu Value
v1 Value
v2
          (v1 :: Value
v1@(VAlts {}),Value
v2) ->
           --err (const (ok2 VGlue v1 v2)) id $
             (String -> Value) -> (Value -> Value) -> Err Value -> Value
forall b a. (String -> b) -> (a -> b) -> Err a -> b
err String -> Value
forall a2 a. Pretty a2 => a2 -> a
bug Value -> Value
forall a. a -> a
id (Err Value -> Value) -> Err Value -> Value
forall a b. (a -> b) -> a -> b
$
             do [Str]
y' <- Value -> Err [Str]
strsFromValue Value
v2
                [Str]
x' <- Value -> Err [Str]
strsFromValue Value
v1
                Value -> Err Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Err Value) -> Value -> Err Value
forall a b. (a -> b) -> a -> b
$ [Value] -> Value
vfv [(Value -> Value -> Value) -> [Value] -> Value
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Value -> Value -> Value
VC ((String -> Value) -> [String] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map String -> Value
VString (Str -> [String]
str2strings (Str -> Str -> Str
glueStr Str
v Str
u))) | Str
v <- [Str]
x', Str
u <- [Str]
y']
          (VC Value
va Value
vb,Value
v2) -> Value -> Value -> Value
VC Value
va (Value -> Value -> Value
glu Value
vb Value
v2)
          (Value
v1,VC Value
va Value
vb) -> Value -> Value -> Value
VC (Value -> Value -> Value
glu Value
v1 Value
va) Value
vb
          (VS (VV Term
ty [Value]
pvs [Value]
vs) Value
vb,Value
v2) -> Value -> Value -> Value
VS (Term -> [Value] -> [Value] -> Value
VV Term
ty [Value]
pvs [Value -> Value -> Value
glu Value
v Value
v2|Value
v<-[Value]
vs]) Value
vb
          (Value
v1,VS (VV Term
ty [Value]
pvs [Value]
vs) Value
vb) -> Value -> Value -> Value
VS (Term -> [Value] -> [Value] -> Value
VV Term
ty [Value]
pvs [Value -> Value -> Value
glu Value
v1 Value
v|Value
v<-[Value]
vs]) Value
vb
          (v1 :: Value
v1@(VApp Predefined
NonExist [Value]
_),Value
_) -> Value
v1
          (Value
_,v2 :: Value
v2@(VApp Predefined
NonExist [Value]
_)) -> Value
v2
--        (v1,v2) -> ok2 VGlue v1 v2
          (Value
v1,Value
v2) -> if (Flags -> Bool) -> Options -> Bool
forall a. (Flags -> a) -> Options -> a
flag Flags -> Bool
optPlusAsBind (CompleteEnv -> Options
opts CompleteEnv
env)
                       then Value -> Value -> Value
VC Value
v1 (Value -> Value -> Value
VC (Predefined -> [Value] -> Value
VApp Predefined
BIND []) Value
v2)
                       else let loc :: L Ident
loc  = CompleteEnv -> L Ident
gloc CompleteEnv
env
                                vt :: Value -> Term
vt Value
v = L Ident -> [Ident] -> Value -> Term
value2term L Ident
loc (CompleteEnv -> [Ident]
local CompleteEnv
env) Value
v
                                        -- Old value2term error message:
                                        --  Left i  -> Error ('#':show i)
                                originalMsg :: String
originalMsg = Doc -> String
forall a. Pretty a => a -> String
render (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ L Ident -> Doc -> Doc
forall a1 a3. (Pretty a1, Pretty a3) => L a3 -> a1 -> Doc
ppL L Ident
loc (String -> Int -> Term -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> Int -> a2 -> Doc
hang String
"unsupported token gluing" Int
4
                                                               (Term -> Term -> Term
Glue (Value -> Term
vt Value
v1) (Value -> Term
vt Value
v2)))
                                term :: String
term = Doc -> String
forall a. Pretty a => a -> String
render (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ Term -> Doc
forall a. Pretty a => a -> Doc
pp  (Term -> Doc) -> Term -> Doc
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
Glue (Value -> Term
vt Value
v1) (Value -> Term
vt Value
v2)
                            in String -> Value
forall a. HasCallStack => String -> a
error (String -> Value) -> String -> Value
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
                                [String
originalMsg
                                ,String
""
                                ,String
"There was a problem in the expression `"String -> String -> String
forall a. [a] -> [a] -> [a]
++String
termString -> String -> String
forall a. [a] -> [a] -> [a]
++String
"`, either:"
                                ,String
"1) You are trying to use + on runtime arguments, possibly via an oper."
                                ,String
"2) One of the arguments in `"String -> String -> String
forall a. [a] -> [a] -> [a]
++String
termString -> String -> String
forall a. [a] -> [a] -> [a]
++String
"` is a bound variable from pattern matching a string, but the cases are non-exhaustive."
                                ,String
"For more help see https://github.com/GrammaticalFramework/gf-core/tree/master/doc/errors/gluing.md"
                                ]


-- | to get a string from a value that represents a sequence of terminals
strsFromValue :: Value -> Err [Str]
strsFromValue :: Value -> Err [Str]
strsFromValue Value
t = case Value
t of
  VString String
s   -> [Str] -> Err [Str]
forall (m :: * -> *) a. Monad m => a -> m a
return [String -> Str
str String
s]
  VC Value
s Value
t -> do
    [Str]
s' <- Value -> Err [Str]
strsFromValue Value
s
    [Str]
t' <- Value -> Err [Str]
strsFromValue Value
t
    [Str] -> Err [Str]
forall (m :: * -> *) a. Monad m => a -> m a
return [Str -> Str -> Str
plusStr Str
x Str
y | Str
x <- [Str]
s', Str
y <- [Str]
t']
{-
  VGlue s t -> do
    s' <- strsFromValue s
    t' <- strsFromValue t
    return [glueStr x y | x <- s', y <- t']
-}
  VAlts Value
d [(Value, Value)]
vs -> do
    [Str]
d0 <- Value -> Err [Str]
strsFromValue Value
d
    [[Str]]
v0 <- ((Value, Value) -> Err [Str]) -> [(Value, Value)] -> Err [[Str]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Value -> Err [Str]
strsFromValue (Value -> Err [Str])
-> ((Value, Value) -> Value) -> (Value, Value) -> Err [Str]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Value, Value) -> Value
forall a b. (a, b) -> a
fst) [(Value, Value)]
vs
    [[Str]]
c0 <- ((Value, Value) -> Err [Str]) -> [(Value, Value)] -> Err [[Str]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Value -> Err [Str]
strsFromValue (Value -> Err [Str])
-> ((Value, Value) -> Value) -> (Value, Value) -> Err [Str]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Value, Value) -> Value
forall a b. (a, b) -> b
snd) [(Value, Value)]
vs
  --let vs' = zip v0 c0
    [Str] -> Err [Str]
forall (m :: * -> *) a. Monad m => a -> m a
return [[String] -> [([String], [String])] -> Str
strTok (Str -> [String]
str2strings Str
def) [([String], [String])]
vars |
              Str
def  <- [Str]
d0,
              [([String], [String])]
vars <- [[(Str -> [String]
str2strings Str
v, (Str -> String) -> [Str] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Str -> String
sstr [Str]
c) | (Str
v,[Str]
c) <- [Str] -> [[Str]] -> [(Str, [Str])]
forall a b. [a] -> [b] -> [(a, b)]
zip [Str]
vv [[Str]]
c0] |
                                                          [Str]
vv <- [[Str]] -> [[Str]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [[Str]]
v0]
           ]
  VFV [Value]
ts -> [[Str]] -> [Str]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Str]] -> [Str]) -> Err [[Str]] -> Err [Str]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
# (Value -> Err [Str]) -> [Value] -> Err [[Str]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Value -> Err [Str]
strsFromValue [Value]
ts
  VStrs [Value]
ts -> [[Str]] -> [Str]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Str]] -> [Str]) -> Err [[Str]] -> Err [Str]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
# (Value -> Err [Str]) -> [Value] -> Err [[Str]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Value -> Err [Str]
strsFromValue [Value]
ts

  Value
_ -> String -> Err [Str]
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"cannot get Str from value " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
t)

vfv :: [Value] -> Value
vfv [Value]
vs = case [Value] -> [Value]
forall a. Eq a => [a] -> [a]
nub [Value]
vs of
           [Value
v] -> Value
v
           [Value]
vs -> [Value] -> Value
VFV [Value]
vs

select :: CompleteEnv -> (Value, Value) -> Value
select CompleteEnv
env (Value, Value)
vv =
    case (Value, Value)
vv of
      (Value
v1,VFV [Value]
vs) -> [Value] -> Value
vfv [CompleteEnv -> (Value, Value) -> Value
select CompleteEnv
env (Value
v1,Value
v2)|Value
v2<-[Value]
vs]
      (VFV [Value]
vs,Value
v2) -> [Value] -> Value
vfv [CompleteEnv -> (Value, Value) -> Value
select CompleteEnv
env (Value
v1,Value
v2)|Value
v1<-[Value]
vs]
      (v1 :: Value
v1@(VV Term
pty [Value]
vs [Value]
rs),Value
v2) ->
         (String -> Value) -> (Value -> Value) -> Err Value -> Value
forall b a. (String -> b) -> (a -> b) -> Err a -> b
err (Value -> String -> Value
forall a b. a -> b -> a
const (Value -> Value -> Value
VS Value
v1 Value
v2)) Value -> Value
forall a. a -> a
id (Err Value -> Value) -> Err Value -> Value
forall a b. (a -> b) -> a -> b
$
         do --ats <- allParamValues (srcgr env) pty
            --let vs = map (value0 env) ats
            Int
i <- String -> Maybe Int -> Err Int
forall (m :: * -> *) a. ErrorMonad m => String -> Maybe a -> m a
maybeErr String
"no match" (Maybe Int -> Err Int) -> Maybe Int -> Err Int
forall a b. (a -> b) -> a -> b
$ (Value -> Bool) -> [Value] -> Maybe Int
forall a. (a -> Bool) -> [a] -> Maybe Int
findIndex (Value -> Value -> Bool
forall a. Eq a => a -> a -> Bool
==Value
v2) [Value]
vs
            Value -> Err Value
forall (m :: * -> *) a. Monad m => a -> m a
return (L Ident -> String -> [Value] -> Int -> Value
forall a3 a. Pretty a3 => L a3 -> String -> [a] -> Int -> a
ix (CompleteEnv -> L Ident
gloc CompleteEnv
env) String
"select" [Value]
rs Int
i)
      (VT Bool
_ Value
_ [(Patt
PW,Bind Env -> Value
b)],Value
_) -> {-trace "eliminate wild card table" $-} Env -> Value
b []
      (v1 :: Value
v1@(VT Bool
_ Value
_ [(Patt, Bind Env)]
cs),Value
v2) ->
                 (String -> Value)
-> ((Bind Env, Substitution) -> Value)
-> Err (Bind Env, Substitution)
-> Value
forall b a. (String -> b) -> (a -> b) -> Err a -> b
err (\String
_->(Value -> Value -> Value) -> Value -> Value -> Value
ok2 Value -> Value -> Value
VS Value
v1 Value
v2) ((String -> Value) -> (Value -> Value) -> Err Value -> Value
forall b a. (String -> b) -> (a -> b) -> Err a -> b
err String -> Value
forall a2 a. Pretty a2 => a2 -> a
bug Value -> Value
forall a. a -> a
id (Err Value -> Value)
-> ((Bind Env, Substitution) -> Err Value)
-> (Bind Env, Substitution)
-> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompleteEnv -> (Bind Env, Substitution) -> Err Value
valueMatch CompleteEnv
env) (Err (Bind Env, Substitution) -> Value)
-> Err (Bind Env, Substitution) -> Value
forall a b. (a -> b) -> a -> b
$
                 L Ident
-> [(Patt, Bind Env)] -> Value -> Err (Bind Env, Substitution)
forall (m :: * -> *) rhs.
MonadFail m =>
L Ident -> [(Patt, rhs)] -> Value -> m (rhs, Substitution)
match (CompleteEnv -> L Ident
gloc CompleteEnv
env) [(Patt, Bind Env)]
cs Value
v2
      (VS (VV Term
pty [Value]
pvs [Value]
rs) Value
v12,Value
v2) -> Value -> Value -> Value
VS (Term -> [Value] -> [Value] -> Value
VV Term
pty [Value]
pvs [CompleteEnv -> (Value, Value) -> Value
select CompleteEnv
env (Value
v11,Value
v2)|Value
v11<-[Value]
rs]) Value
v12
      (Value
v1,Value
v2) -> (Value -> Value -> Value) -> Value -> Value -> Value
ok2 Value -> Value -> Value
VS Value
v1 Value
v2

match :: L Ident -> [(Patt, rhs)] -> Value -> m (rhs, Substitution)
match L Ident
loc [(Patt, rhs)]
cs Value
v =
  (String -> m (rhs, Substitution))
-> ((rhs, Substitution) -> m (rhs, Substitution))
-> Err (rhs, Substitution)
-> m (rhs, Substitution)
forall b a. (String -> b) -> (a -> b) -> Err a -> b
err String -> m (rhs, Substitution)
forall a. String -> m a
bad (rhs, Substitution) -> m (rhs, Substitution)
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Patt, rhs)] -> Term -> Err (rhs, Substitution)
forall (m :: * -> *) rhs.
ErrorMonad m =>
[(Patt, rhs)] -> Term -> m (rhs, Substitution)
matchPattern [(Patt, rhs)]
cs (L Ident -> [Ident] -> Value -> Term
value2term L Ident
loc [] Value
v))
    -- Old value2term error message:
    -- Left i  -> bad ("variable #"++show i++" is out of scope")
  where
    bad :: String -> m a
bad = String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> m a) -> (String -> String) -> String -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
"In pattern matching: "String -> String -> String
forall a. [a] -> [a] -> [a]
++)

valueMatch :: CompleteEnv -> (Bind Env,Substitution) -> Err Value
valueMatch :: CompleteEnv -> (Bind Env, Substitution) -> Err Value
valueMatch CompleteEnv
env (Bind Env -> Value
f,Substitution
env') = Env -> Value
f (Env -> Value) -> Err Env -> Err Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
# (Term -> Err Value) -> Substitution -> Err Env
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> [(a, b)] -> m [(a, c)]
mapPairsM (CompleteEnv -> Term -> Err Value
value0 CompleteEnv
env) Substitution
env'

valueTable :: CompleteEnv -> TInfo -> [Case] -> Err OpenValue
valueTable :: CompleteEnv -> TInfo -> [Case] -> Err ([Value] -> Value)
valueTable CompleteEnv
env TInfo
i [Case]
cs =
    case TInfo
i of
      TComp Term
ty -> do [Value]
pvs <- CompleteEnv -> Term -> Err [Value]
paramValues CompleteEnv
env Term
ty
                     ((Term -> [Value] -> [Value] -> Value
VV Term
ty [Value]
pvs ([Value] -> Value) -> ([Value] -> [Value]) -> [Value] -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) (([Value] -> [Value]) -> [Value] -> Value)
-> ([[Value] -> Value] -> [Value] -> [Value])
-> [[Value] -> Value]
-> [Value]
-> Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
# [[Value] -> Value] -> [Value] -> [Value]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence) ([[Value] -> Value] -> [Value] -> Value)
-> Err [[Value] -> Value] -> Err ([Value] -> Value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
# (Case -> Err ([Value] -> Value))
-> [Case] -> Err [[Value] -> Value]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (CompleteEnv -> Term -> Err ([Value] -> Value)
value CompleteEnv
env(Term -> Err ([Value] -> Value))
-> (Case -> Term) -> Case -> Err ([Value] -> Value)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Case -> Term
forall a b. (a, b) -> b
snd) [Case]
cs
      TInfo
_ -> do Term
ty <- TInfo -> Err Term
getTableType TInfo
i
              [(Patt, [Value] -> Bind Env)]
cs' <- (Case -> Err (Patt, [Value] -> Bind Env))
-> [Case] -> Err [(Patt, [Value] -> Bind Env)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Case -> Err (Patt, [Value] -> Bind Env)
valueCase [Case]
cs
              (String -> Err ([Value] -> Value))
-> (([Value] -> Value) -> Err ([Value] -> Value))
-> Err ([Value] -> Value)
-> Err ([Value] -> Value)
forall b a. (String -> b) -> (a -> b) -> Err a -> b
err ([(Patt, [Value] -> Bind Env)]
-> Term -> String -> Err ([Value] -> Value)
forall p.
[(Patt, [Value] -> Bind Env)]
-> Term -> p -> Err ([Value] -> Value)
dynamic [(Patt, [Value] -> Bind Env)]
cs' Term
ty) ([Value] -> Value) -> Err ([Value] -> Value)
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Patt, [Value] -> Bind Env)] -> Term -> Err ([Value] -> Value)
forall a. [(Patt, a -> Bind Env)] -> Term -> Err (a -> Value)
convert [(Patt, [Value] -> Bind Env)]
cs' Term
ty)
  where
    dynamic :: [(Patt, [Value] -> Bind Env)]
-> Term -> p -> Err ([Value] -> Value)
dynamic [(Patt, [Value] -> Bind Env)]
cs' Term
ty p
_ = [(Patt, [Value] -> Bind Env)]
-> ([Value] -> Value) -> [Value] -> Value
forall a. [(Patt, a -> Bind Env)] -> (a -> Value) -> a -> Value
cases [(Patt, [Value] -> Bind Env)]
cs' (([Value] -> Value) -> [Value] -> Value)
-> Err ([Value] -> Value) -> Err ([Value] -> Value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
# CompleteEnv -> Term -> Err ([Value] -> Value)
value CompleteEnv
env Term
ty

    cases :: [(Patt, a -> Bind Env)] -> (a -> Value) -> a -> Value
cases [(Patt, a -> Bind Env)]
cs' a -> Value
vty a
vs = (String -> Value)
-> ((a -> Value) -> Value) -> Err (a -> Value) -> Value
forall b a. (String -> b) -> (a -> b) -> Err a -> b
err String -> Value
forall p. p -> Value
keep ((a -> Value) -> a -> Value
forall a b. (a -> b) -> a -> b
$a
vs) ([(Patt, a -> Bind Env)] -> Value -> Err (a -> Value)
forall a. [(Patt, a -> Bind Env)] -> Value -> Err (a -> Value)
convertv [(Patt, a -> Bind Env)]
cs' (a -> Value
vty a
vs))
      where
        keep :: p -> Value
keep p
msg = --trace (msg++"\n"++render (ppTerm Unqualified 0 (T i cs))) $
                   Bool -> Value -> [(Patt, Bind Env)] -> Value
VT Bool
wild (a -> Value
vty a
vs) (((a -> Bind Env) -> Bind Env)
-> [(Patt, a -> Bind Env)] -> [(Patt, Bind Env)]
forall b b' a. (b -> b') -> [(a, b)] -> [(a, b')]
mapSnd ((a -> Bind Env) -> a -> Bind Env
forall a b. (a -> b) -> a -> b
$a
vs) [(Patt, a -> Bind Env)]
cs')

    wild :: Bool
wild = case TInfo
i of TWild Term
_ -> Bool
True; TInfo
_ -> Bool
False

    convertv :: [(Patt, a -> Bind Env)] -> Value -> Err (a -> Value)
convertv [(Patt, a -> Bind Env)]
cs' Value
vty =
      [(Patt, a -> Bind Env)]
-> ((Term, [Term]), [Value]) -> Err (a -> Value)
forall (m :: * -> *) a.
ErrorMonad m =>
[(Patt, a -> Bind Env)]
-> ((Term, [Term]), [Value]) -> m (a -> Value)
convert' [(Patt, a -> Bind Env)]
cs' (((Term, [Term]), [Value]) -> Err (a -> Value))
-> Err ((Term, [Term]), [Value]) -> Err (a -> Value)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< CompleteEnv -> Term -> Err ((Term, [Term]), [Value])
paramValues'' CompleteEnv
env (L Ident -> [Ident] -> Value -> Term
value2term (CompleteEnv -> L Ident
gloc CompleteEnv
env) [] Value
vty)
        -- Old value2term error message: Left i    -> fail ("variable #"++show i++" is out of scope")

    convert :: [(Patt, a -> Bind Env)] -> Term -> Err (a -> Value)
convert [(Patt, a -> Bind Env)]
cs' Term
ty = [(Patt, a -> Bind Env)]
-> ((Term, [Term]), [Value]) -> Err (a -> Value)
forall (m :: * -> *) a.
ErrorMonad m =>
[(Patt, a -> Bind Env)]
-> ((Term, [Term]), [Value]) -> m (a -> Value)
convert' [(Patt, a -> Bind Env)]
cs' (((Term, [Term]), [Value]) -> Err (a -> Value))
-> Err ((Term, [Term]), [Value]) -> Err (a -> Value)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< CompleteEnv -> Term -> Err ((Term, [Term]), [Value])
paramValues' CompleteEnv
env Term
ty

    convert' :: [(Patt, a -> Bind Env)]
-> ((Term, [Term]), [Value]) -> m (a -> Value)
convert' [(Patt, a -> Bind Env)]
cs' ((Term
pty,[Term]
vs),[Value]
pvs) =
      do [(a -> Bind Env, Substitution)]
sts  <- (Term -> m (a -> Bind Env, Substitution))
-> [Term] -> m [(a -> Bind Env, Substitution)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([(Patt, a -> Bind Env)] -> Term -> m (a -> Bind Env, Substitution)
forall (m :: * -> *) rhs.
ErrorMonad m =>
[(Patt, rhs)] -> Term -> m (rhs, Substitution)
matchPattern [(Patt, a -> Bind Env)]
cs') [Term]
vs
         (a -> Value) -> m (a -> Value)
forall (m :: * -> *) a. Monad m => a -> m a
return ((a -> Value) -> m (a -> Value)) -> (a -> Value) -> m (a -> Value)
forall a b. (a -> b) -> a -> b
$ \ a
vs -> Term -> [Value] -> [Value] -> Value
VV Term
pty [Value]
pvs ([Value] -> Value) -> [Value] -> Value
forall a b. (a -> b) -> a -> b
$ ((Bind Env, Substitution) -> Value)
-> [(Bind Env, Substitution)] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map ((String -> Value) -> (Value -> Value) -> Err Value -> Value
forall b a. (String -> b) -> (a -> b) -> Err a -> b
err String -> Value
forall a2 a. Pretty a2 => a2 -> a
bug Value -> Value
forall a. a -> a
id (Err Value -> Value)
-> ((Bind Env, Substitution) -> Err Value)
-> (Bind Env, Substitution)
-> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompleteEnv -> (Bind Env, Substitution) -> Err Value
valueMatch CompleteEnv
env)
                                           (((a -> Bind Env) -> Bind Env)
-> [(a -> Bind Env, Substitution)] -> [(Bind Env, Substitution)]
forall a a' b. (a -> a') -> [(a, b)] -> [(a', b)]
mapFst ((a -> Bind Env) -> a -> Bind Env
forall a b. (a -> b) -> a -> b
$a
vs) [(a -> Bind Env, Substitution)]
sts)

    valueCase :: Case -> Err (Patt, [Value] -> Bind Env)
valueCase (Patt
p,Term
t) = do Patt
p' <- Patt -> Patt
measurePatt (Patt -> Patt) -> Err Patt -> Err Patt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
# Patt -> Err Patt
inlinePattMacro Patt
p
                         [Ident]
pvs <- Patt -> Err [Ident]
forall (m :: * -> *). MonadFail m => Patt -> m [Ident]
linPattVars Patt
p'
                         [Value] -> Value
vt <- CompleteEnv -> Term -> Err ([Value] -> Value)
value ([Ident] -> CompleteEnv -> CompleteEnv
extend [Ident]
pvs CompleteEnv
env) Term
t
                         (Patt, [Value] -> Bind Env) -> Err (Patt, [Value] -> Bind Env)
forall (m :: * -> *) a. Monad m => a -> m a
return (Patt
p',\[Value]
vs-> (Env -> Value) -> Bind Env
forall a. (a -> Value) -> Bind a
Bind ((Env -> Value) -> Bind Env) -> (Env -> Value) -> Bind Env
forall a b. (a -> b) -> a -> b
$ \Env
bs-> [Value] -> Value
vt (Patt -> Env -> [Ident] -> [Value] -> [Value]
forall a. Show a => a -> Env -> [Ident] -> [Value] -> [Value]
push' Patt
p' Env
bs [Ident]
pvs [Value]
vs))

    inlinePattMacro :: Patt -> Err Patt
inlinePattMacro Patt
p =
        case Patt
p of
          PM (ModuleName, Ident)
qc -> do Value
r <- CompleteEnv -> (ModuleName, Ident) -> Err Value
resource CompleteEnv
env (ModuleName, Ident)
qc
                      case Value
r of
                        VPatt Patt
p' -> Patt -> Err Patt
inlinePattMacro Patt
p'
                        Value
_ -> Doc -> Err Patt
forall a2 a. Pretty a2 => a2 -> a
ppbug (Doc -> Err Patt) -> Doc -> Err Patt
forall a b. (a -> b) -> a -> b
$ String -> Int -> String -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> Int -> a2 -> Doc
hang String
"Expected pattern macro:" Int
4
                                          (Value -> String
forall a. Show a => a -> String
show Value
r)
          Patt
_ -> (Patt -> Err Patt) -> Patt -> Err Patt
forall (m :: * -> *). Monad m => (Patt -> m Patt) -> Patt -> m Patt
composPattOp Patt -> Err Patt
inlinePattMacro Patt
p


paramValues :: CompleteEnv -> Term -> Err [Value]
paramValues CompleteEnv
env Term
ty = ((Term, [Term]), [Value]) -> [Value]
forall a b. (a, b) -> b
snd (((Term, [Term]), [Value]) -> [Value])
-> Err ((Term, [Term]), [Value]) -> Err [Value]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
# CompleteEnv -> Term -> Err ((Term, [Term]), [Value])
paramValues' CompleteEnv
env Term
ty

paramValues' :: CompleteEnv -> Term -> Err ((Term, [Term]), [Value])
paramValues' CompleteEnv
env Term
ty = CompleteEnv -> Term -> Err ((Term, [Term]), [Value])
paramValues'' CompleteEnv
env (Term -> Err ((Term, [Term]), [Value]))
-> Err Term -> Err ((Term, [Term]), [Value])
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< GlobalEnv -> Term -> Err Term
nfx (CompleteEnv -> GlobalEnv
global CompleteEnv
env) Term
ty

paramValues'' :: CompleteEnv -> Term -> Err ((Term, [Term]), [Value])
paramValues'' CompleteEnv
env Term
pty = do [Term]
ats <- Grammar -> Term -> Err [Term]
forall (m :: * -> *). ErrorMonad m => Grammar -> Term -> m [Term]
allParamValues (CompleteEnv -> Grammar
srcgr CompleteEnv
env) Term
pty
                           [Value]
pvs <- (Term -> Err Value) -> [Term] -> Err [Value]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (GlobalEnv -> Env -> Term -> Err Value
eval (CompleteEnv -> GlobalEnv
global CompleteEnv
env) []) [Term]
ats
                           ((Term, [Term]), [Value]) -> Err ((Term, [Term]), [Value])
forall (m :: * -> *) a. Monad m => a -> m a
return ((Term
pty,[Term]
ats),[Value]
pvs)

push' :: a -> Env -> [Ident] -> [Value] -> [Value]
push' a
p Env
bs [Ident]
xs = if Env -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Env
bsInt -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/=[Ident] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Ident]
xs
                then String -> [Value] -> [Value]
forall a2 a. Pretty a2 => a2 -> a
bug (String -> [Value] -> [Value]) -> String -> [Value] -> [Value]
forall a b. (a -> b) -> a -> b
$ String
"push "String -> String -> String
forall a. [a] -> [a] -> [a]
++(a, Env, [Ident]) -> String
forall a. Show a => a -> String
show (a
p,Env
bs,[Ident]
xs)
                else Env -> [Ident] -> [Value] -> [Value]
push Env
bs [Ident]
xs

push :: Env -> LocalScope -> Stack -> Stack
push :: Env -> [Ident] -> [Value] -> [Value]
push Env
bs [] [Value]
vs = [Value]
vs
push Env
bs (Ident
x:[Ident]
xs) [Value]
vs = Value -> (Value -> Value) -> Maybe Value -> Value
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Value
forall a. a
err Value -> Value
forall a. a -> a
id (Ident -> Env -> Maybe Value
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Ident
x Env
bs)Value -> [Value] -> [Value]
forall a. a -> [a] -> [a]
:Env -> [Ident] -> [Value] -> [Value]
push Env
bs [Ident]
xs [Value]
vs
  where  err :: a
err = String -> a
forall a2 a. Pretty a2 => a2 -> a
bug (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"Unbound pattern variable "String -> String -> String
forall a. [a] -> [a] -> [a]
++Ident -> String
showIdent Ident
x

apply' :: CompleteEnv -> Term -> [OpenValue] -> Err OpenValue
apply' :: CompleteEnv -> Term -> [[Value] -> Value] -> Err ([Value] -> Value)
apply' CompleteEnv
env Term
t [] = CompleteEnv -> Term -> Err ([Value] -> Value)
value CompleteEnv
env Term
t
apply' CompleteEnv
env Term
t [[Value] -> Value]
vs =
  case Term
t of
    QC (ModuleName, Ident)
x                   -> ([Value] -> Value) -> Err ([Value] -> Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (([Value] -> Value) -> Err ([Value] -> Value))
-> ([Value] -> Value) -> Err ([Value] -> Value)
forall a b. (a -> b) -> a -> b
$ \ [Value]
svs -> (ModuleName, Ident) -> [Value] -> Value
VCApp (ModuleName, Ident)
x ((([Value] -> Value) -> Value) -> [[Value] -> Value] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map (([Value] -> Value) -> [Value] -> Value
forall a b. (a -> b) -> a -> b
$[Value]
svs) [[Value] -> Value]
vs)
{-
    Q x@(m,f) | m==cPredef -> return $
                              let constr = --trace ("predef "++show x) .
                                           VApp x
                              in \ svs -> maybe constr id (Map.lookup f predefs)
                                          $ map ($svs) vs
              | otherwise  -> do r <- resource env x
                                 return $ \ svs -> vapply (gloc env) r (map ($svs) vs)
-}
    App Term
t1 Term
t2              -> CompleteEnv -> Term -> [[Value] -> Value] -> Err ([Value] -> Value)
apply' CompleteEnv
env Term
t1 ([[Value] -> Value] -> Err ([Value] -> Value))
-> (([Value] -> Value) -> [[Value] -> Value])
-> ([Value] -> Value)
-> Err ([Value] -> Value)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (([Value] -> Value) -> [[Value] -> Value] -> [[Value] -> Value]
forall a. a -> [a] -> [a]
:[[Value] -> Value]
vs) (([Value] -> Value) -> Err ([Value] -> Value))
-> Err ([Value] -> Value) -> Err ([Value] -> Value)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< CompleteEnv -> Term -> Err ([Value] -> Value)
value CompleteEnv
env Term
t2
    Term
_                      -> do [Value] -> Value
fv <- CompleteEnv -> Term -> Err ([Value] -> Value)
value CompleteEnv
env Term
t
                                 ([Value] -> Value) -> Err ([Value] -> Value)
forall (m :: * -> *) a. Monad m => a -> m a
return (([Value] -> Value) -> Err ([Value] -> Value))
-> ([Value] -> Value) -> Err ([Value] -> Value)
forall a b. (a -> b) -> a -> b
$ \ [Value]
svs -> L Ident -> Value -> [Value] -> Value
vapply (CompleteEnv -> L Ident
gloc CompleteEnv
env) ([Value] -> Value
fv [Value]
svs) ((([Value] -> Value) -> Value) -> [[Value] -> Value] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map (([Value] -> Value) -> [Value] -> Value
forall a b. (a -> b) -> a -> b
$[Value]
svs) [[Value] -> Value]
vs)

vapply :: GLocation -> Value -> [Value] -> Value
vapply :: L Ident -> Value -> [Value] -> Value
vapply L Ident
loc Value
v [] = Value
v
vapply L Ident
loc Value
v [Value]
vs =
  case Value
v of
    VError {} -> Value
v
--  VClosure env (Abs b x t) -> beta gr env b x t vs
    VAbs BindType
bt Ident
_ (Bind Value -> Value
f) -> L Ident -> BindType -> (Value -> Value) -> [Value] -> Value
vbeta L Ident
loc BindType
bt Value -> Value
f [Value]
vs
    VApp Predefined
pre [Value]
vs1 -> Predefined -> [Value] -> Value
delta' Predefined
pre ([Value]
vs1[Value] -> [Value] -> [Value]
forall a. [a] -> [a] -> [a]
++[Value]
vs)
      where
        delta' :: Predefined -> [Value] -> Value
delta' Predefined
Trace (Value
v1:Value
v2:[Value]
vs) = let vr :: Value
vr = L Ident -> Value -> [Value] -> Value
vapply L Ident
loc Value
v2 [Value]
vs
                                  in L Ident -> Value -> Value -> Value
forall p. p -> Value -> Value -> Value
vtrace L Ident
loc Value
v1 Value
vr
        delta' Predefined
pre [Value]
vs = (String -> Value) -> ([Value] -> Value) -> Err [Value] -> Value
forall b a. (String -> b) -> (a -> b) -> Err a -> b
err String -> Value
forall c. String -> c
msg [Value] -> Value
vfv (Err [Value] -> Value) -> Err [Value] -> Value
forall a b. (a -> b) -> a -> b
$ ([Value] -> Err Value) -> [[Value]] -> Err [Value]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Predefined -> [Value] -> Err Value
delta Predefined
pre) ([Value] -> [[Value]]
varyList [Value]
vs)
        --msg = const (VApp pre (vs1++vs))
        msg :: String -> c
msg = String -> c
forall a2 a. Pretty a2 => a2 -> a
bug (String -> c) -> (String -> String) -> String -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((String
"Applying Predef."String -> String -> String
forall a. [a] -> [a] -> [a]
++Ident -> String
showIdent (Predefined -> Ident
predefName Predefined
pre)String -> String -> String
forall a. [a] -> [a] -> [a]
++String
": ")String -> String -> String
forall a. [a] -> [a] -> [a]
++)
    VS (VV Term
t [Value]
pvs [Value]
fs) Value
s -> Value -> Value -> Value
VS (Term -> [Value] -> [Value] -> Value
VV Term
t [Value]
pvs [L Ident -> Value -> [Value] -> Value
vapply L Ident
loc Value
f [Value]
vs|Value
f<-[Value]
fs]) Value
s
    VFV [Value]
fs -> [Value] -> Value
vfv [L Ident -> Value -> [Value] -> Value
vapply L Ident
loc Value
f [Value]
vs|Value
f<-[Value]
fs]
    VCApp (ModuleName, Ident)
f [Value]
vs0 -> (ModuleName, Ident) -> [Value] -> Value
VCApp (ModuleName, Ident)
f ([Value]
vs0[Value] -> [Value] -> [Value]
forall a. [a] -> [a] -> [a]
++[Value]
vs)
    VMeta Int
i Env
env [Value]
vs0 -> Int -> Env -> [Value] -> Value
VMeta Int
i Env
env ([Value]
vs0[Value] -> [Value] -> [Value]
forall a. [a] -> [a] -> [a]
++[Value]
vs)
    VGen Int
i [Value]
vs0 -> Int -> [Value] -> Value
VGen Int
i ([Value]
vs0[Value] -> [Value] -> [Value]
forall a. [a] -> [a] -> [a]
++[Value]
vs)
    Value
v -> String -> Value
forall a2 a. Pretty a2 => a2 -> a
bug (String -> Value) -> String -> Value
forall a b. (a -> b) -> a -> b
$ String
"vapply "String -> String -> String
forall a. [a] -> [a] -> [a]
++Value -> String
forall a. Show a => a -> String
show Value
vString -> String -> String
forall a. [a] -> [a] -> [a]
++String
" "String -> String -> String
forall a. [a] -> [a] -> [a]
++[Value] -> String
forall a. Show a => a -> String
show [Value]
vs

vbeta :: L Ident -> BindType -> (Value -> Value) -> [Value] -> Value
vbeta L Ident
loc BindType
bt Value -> Value
f (Value
v:[Value]
vs) =
  case (BindType
bt,Value
v) of
    (BindType
Implicit,VImplArg Value
v) -> Value -> Value
ap Value
v
    (BindType
Explicit,         Value
v) -> Value -> Value
ap Value
v
  where
    ap :: Value -> Value
ap (VFV [Value]
avs) = [Value] -> Value
vfv [L Ident -> Value -> [Value] -> Value
vapply L Ident
loc (Value -> Value
f Value
v) [Value]
vs|Value
v<-[Value]
avs]
    ap Value
v         = L Ident -> Value -> [Value] -> Value
vapply L Ident
loc (Value -> Value
f Value
v) [Value]
vs

vary :: Value -> [Value]
vary (VFV [Value]
vs) = [Value]
vs
vary Value
v = [Value
v]
varyList :: [Value] -> [[Value]]
varyList = (Value -> [Value]) -> [Value] -> [[Value]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Value -> [Value]
vary

{-
beta env b x t (v:vs) =
  case (b,v) of
    (Implicit,VImplArg v) -> apply' (ext (x,v) env) t vs
    (Explicit,         v) -> apply' (ext (x,v) env) t vs
-}

vtrace :: p -> Value -> Value -> Value
vtrace p
loc Value
arg Value
res = String -> Value -> Value
forall a. String -> a -> a
trace (Doc -> String
forall a. Pretty a => a -> String
render (Doc -> Int -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> Int -> a2 -> Doc
hang (Value -> Doc
pv Value
arg) Int
4 (String
"->"String -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+>Value -> Doc
pv Value
res))) Value
res
  where
    pv :: Value -> Doc
pv Value
v = case Value
v of
             VRec ((Label, Value)
f:[(Label, Value)]
as) -> Doc -> Int -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> Int -> a2 -> Doc
hang ((Label, Value) -> Doc
forall a. (a, Value) -> Doc
pf (Label, Value)
f) Int
4 ([Doc] -> Doc
forall a. Pretty a => [a] -> Doc
fsep (((Label, Value) -> Doc) -> [(Label, Value)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Label, Value) -> Doc
forall a. (a, Value) -> Doc
pa [(Label, Value)]
as))
             Value
_ -> Value -> Doc
ppV Value
v
    pf :: (a, Value) -> Doc
pf (a
_,VString String
n) = String -> Doc
forall a. Pretty a => a -> Doc
pp String
n
    pf (a
_,Value
v) = Value -> Doc
ppV Value
v
    pa :: (a, Value) -> Doc
pa (a
_,Value
v) = Value -> Doc
ppV Value
v
    ppV :: Value -> Doc
ppV Value
v = TermPrintQual -> Integer -> Term -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Term -> Doc
ppTerm TermPrintQual
Unqualified Integer
10 (Bool -> p -> [Ident] -> Value -> Term
forall p. Bool -> p -> [Ident] -> Value -> Term
value2term' Bool
True p
loc [] Value
v)
              -- Old value2term error message:
              -- Left i  -> "variable #" <> pp i <+> "is out of scope"

-- | Convert a value back to a term
value2term :: GLocation -> [Ident] -> Value -> Term
value2term :: L Ident -> [Ident] -> Value -> Term
value2term = Bool -> L Ident -> [Ident] -> Value -> Term
forall p. Bool -> p -> [Ident] -> Value -> Term
value2term' Bool
False

value2term' :: Bool -> p -> [Ident] -> Value -> Term
value2term' :: Bool -> p -> [Ident] -> Value -> Term
value2term' Bool
stop p
loc [Ident]
xs Value
v0 =
  case Value
v0 of
    VApp Predefined
pre [Value]
vs    -> Term -> [Value] -> Term
applyMany ((ModuleName, Ident) -> Term
Q (ModuleName
cPredef,Predefined -> Ident
predefName Predefined
pre)) [Value]
vs
    VCApp (ModuleName, Ident)
f [Value]
vs     -> Term -> [Value] -> Term
applyMany ((ModuleName, Ident) -> Term
QC (ModuleName, Ident)
f)                       [Value]
vs
    VGen Int
j [Value]
vs      -> Term -> [Value] -> Term
applyMany (Int -> Term
var Int
j)                      [Value]
vs
    VMeta Int
j Env
env [Value]
vs -> Term -> [Value] -> Term
applyMany (Int -> Term
Meta Int
j)                     [Value]
vs
    VProd BindType
bt Value
v Ident
x Binding
f -> BindType -> Ident -> Term -> Term -> Term
Prod BindType
bt Ident
x (Value -> Term
v2t Value
v)  (Ident -> Binding -> Term
v2t' Ident
x Binding
f)
    VAbs  BindType
bt   Ident
x Binding
f -> BindType -> Ident -> Term -> Term
Abs  BindType
bt Ident
x          (Ident -> Binding -> Term
v2t' Ident
x Binding
f)
    VInt Int
n         -> Int -> Term
EInt Int
n
    VFloat Double
f       -> Double -> Term
EFloat Double
f
    VString String
s      -> if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
s then Term
Empty else String -> Term
K String
s
    VSort Ident
s        -> Ident -> Term
Sort Ident
s
    VImplArg Value
v     -> Term -> Term
ImplArg (Value -> Term
v2t Value
v)
    VTblType Value
p Value
res -> Term -> Term -> Term
Table (Value -> Term
v2t Value
p) (Value -> Term
v2t Value
res)
    VRecType [(Label, Value)]
rs    -> [Labelling] -> Term
RecType [(Label
l, Value -> Term
v2t Value
v) | (Label
l,Value
v) <- [(Label, Value)]
rs]
    VRec [(Label, Value)]
as        -> [Assign] -> Term
R       [(Label
l, (Maybe Term
forall a. Maybe a
Nothing, Value -> Term
v2t Value
v)) | (Label
l,Value
v) <- [(Label, Value)]
as]
    VV Term
t [Value]
_ [Value]
vs      -> Term -> [Term] -> Term
V Term
t     ((Value -> Term) -> [Value] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Value -> Term
v2t [Value]
vs)
    VT Bool
wild Value
v [(Patt, Bind Env)]
cs   -> TInfo -> [Case] -> Term
T ((if Bool
wild then Term -> TInfo
TWild else Term -> TInfo
TTyped) (Value -> Term
v2t Value
v)) (((Patt, Bind Env) -> Case) -> [(Patt, Bind Env)] -> [Case]
forall a b. (a -> b) -> [a] -> [b]
map (Patt, Bind Env) -> Case
nfcase [(Patt, Bind Env)]
cs)
    VFV [Value]
vs         -> [Term] -> Term
FV ((Value -> Term) -> [Value] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Value -> Term
v2t [Value]
vs)
    VC Value
v1 Value
v2       -> Term -> Term -> Term
C (Value -> Term
v2t Value
v1) (Value -> Term
v2t Value
v2)
    VS Value
v1 Value
v2       -> Term -> Term -> Term
S (Value -> Term
v2t Value
v1) (Value -> Term
v2t Value
v2)
    VP Value
v Label
l         -> Term -> Label -> Term
P (Value -> Term
v2t Value
v) Label
l
    VPatt Patt
p        -> Patt -> Term
EPatt Patt
p
    VPattType Value
v    -> Term -> Term
EPattType (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Value -> Term
v2t Value
v
    VAlts Value
v [(Value, Value)]
vvs    -> Term -> [(Term, Term)] -> Term
Alts (Value -> Term
v2t Value
v) [(Value -> Term
v2t Value
x, Value -> Term
v2t Value
y) | (Value
x,Value
y) <- [(Value, Value)]
vvs]
    VStrs [Value]
vs       -> [Term] -> Term
Strs ((Value -> Term) -> [Value] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Value -> Term
v2t [Value]
vs)
--  VGlue v1 v2    -> Glue (v2t v1) (v2t v2)
--  VExtR v1 v2    -> ExtR (v2t v1) (v2t v2)
    VError String
err     -> String -> Term
Error String
err
  where
    applyMany :: Term -> [Value] -> Term
applyMany Term
f [Value]
vs = (Term -> Term -> Term) -> Term -> [Term] -> Term
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Term -> Term -> Term
App Term
f ((Value -> Term) -> [Value] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Value -> Term
v2t [Value]
vs)
    v2t :: Value -> Term
v2t = [Ident] -> Value -> Term
v2txs [Ident]
xs
    v2txs :: [Ident] -> Value -> Term
v2txs = Bool -> p -> [Ident] -> Value -> Term
forall p. Bool -> p -> [Ident] -> Value -> Term
value2term' Bool
stop p
loc
    v2t' :: Ident -> Binding -> Term
v2t' Ident
x Binding
f = [Ident] -> Value -> Term
v2txs (Ident
xIdent -> [Ident] -> [Ident]
forall a. a -> [a] -> [a]
:[Ident]
xs) (Binding -> Value -> Value
forall a. Bind a -> a -> Value
bind Binding
f ([Ident] -> Value
forall (t :: * -> *) a. Foldable t => t a -> Value
gen [Ident]
xs))

    var :: Int -> Term
var Int
j
      | Int
jInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<[Ident] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Ident]
xs = Ident -> Term
Vr ([Ident] -> [Ident]
forall a. [a] -> [a]
reverse [Ident]
xs [Ident] -> Int -> Ident
forall a. [a] -> Int -> a
!! Int
j)
      | Bool
otherwise   = String -> Term
forall a. HasCallStack => String -> a
error (String
"variable #"String -> String -> String
forall a. [a] -> [a] -> [a]
++Int -> String
forall a. Show a => a -> String
show Int
jString -> String -> String
forall a. [a] -> [a] -> [a]
++String
" is out of scope")


    pushs :: t a -> ([(a, Value)], [a]) -> ([(a, Value)], [a])
pushs t a
xs ([(a, Value)], [a])
e = (a -> ([(a, Value)], [a]) -> ([(a, Value)], [a]))
-> ([(a, Value)], [a]) -> t a -> ([(a, Value)], [a])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> ([(a, Value)], [a]) -> ([(a, Value)], [a])
forall a. a -> ([(a, Value)], [a]) -> ([(a, Value)], [a])
push ([(a, Value)], [a])
e t a
xs
    push :: a -> ([(a, Value)], [a]) -> ([(a, Value)], [a])
push a
x ([(a, Value)]
env,[a]
xs) = ((a
x,[a] -> Value
forall (t :: * -> *) a. Foldable t => t a -> Value
gen [a]
xs)(a, Value) -> [(a, Value)] -> [(a, Value)]
forall a. a -> [a] -> [a]
:[(a, Value)]
env,a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
xs)
    gen :: t a -> Value
gen t a
xs = Int -> [Value] -> Value
VGen (t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
xs) []

    nfcase :: (Patt, Bind Env) -> Case
nfcase (Patt
p,Bind Env
f) = (,) Patt
p ([Ident] -> Value -> Term
v2txs [Ident]
xs' (Bind Env -> Env -> Value
forall a. Bind a -> a -> Value
bind Bind Env
f Env
env'))
      where (Env
env',[Ident]
xs') = [Ident] -> (Env, [Ident]) -> (Env, [Ident])
forall (t :: * -> *) a.
Foldable t =>
t a -> ([(a, Value)], [a]) -> ([(a, Value)], [a])
pushs (Patt -> [Ident]
pattVars Patt
p) ([],[Ident]
xs)

    bind :: Bind a -> a -> Value
bind (Bind a -> Value
f) a
x = if Bool
stop
                      then Ident -> Value
VSort (String -> Ident
identS String
"...") -- hmm
                      else a -> Value
f a
x


linPattVars :: Patt -> m [Ident]
linPattVars Patt
p =
    if [Ident] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ident]
dups
    then [Ident] -> m [Ident]
forall (m :: * -> *) a. Monad m => a -> m a
return [Ident]
pvs
    else String -> m [Ident]
forall (m :: * -> *) a. MonadFail m => String -> m a
fail(String -> m [Ident]) -> (Doc -> String) -> Doc -> m [Ident]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Doc -> String
forall a. Pretty a => a -> String
render (Doc -> m [Ident]) -> Doc -> m [Ident]
forall a b. (a -> b) -> a -> b
$ String -> Int -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> Int -> a2 -> Doc
hang String
"Pattern is not linear. All variable names on the left-hand side must be distinct." Int
4 (TermPrintQual -> Integer -> Patt -> Doc
forall a. (Num a, Ord a) => TermPrintQual -> a -> Patt -> Doc
ppPatt TermPrintQual
Unqualified Integer
0 Patt
p)
  where
    allpvs :: [Ident]
allpvs = Patt -> [Ident]
allPattVars Patt
p
    pvs :: [Ident]
pvs = [Ident] -> [Ident]
forall a. Eq a => [a] -> [a]
nub [Ident]
allpvs
    dups :: [Ident]
dups = [Ident]
allpvs [Ident] -> [Ident] -> [Ident]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Ident]
pvs

pattVars :: Patt -> [Ident]
pattVars = [Ident] -> [Ident]
forall a. Eq a => [a] -> [a]
nub ([Ident] -> [Ident]) -> (Patt -> [Ident]) -> Patt -> [Ident]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Patt -> [Ident]
allPattVars
allPattVars :: Patt -> [Ident]
allPattVars Patt
p =
    case Patt
p of
      PV Ident
i    -> [Ident
i]
      PAs Ident
i Patt
p -> Ident
iIdent -> [Ident] -> [Ident]
forall a. a -> [a] -> [a]
:Patt -> [Ident]
allPattVars Patt
p
      Patt
_       -> (Patt -> [Ident]) -> Patt -> [Ident]
forall a. (Patt -> [a]) -> Patt -> [a]
collectPattOp Patt -> [Ident]
allPattVars Patt
p

---
ix :: L a3 -> String -> [a] -> Int -> a
ix L a3
loc String
fn [a]
xs Int
i =
    if Int
iInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<Int
n
    then [a]
xs [a] -> Int -> a
forall a. [a] -> Int -> a
!! Int
i
    else L a3 -> String -> a
forall a1 a3 a. (Pretty a1, Pretty a3) => L a3 -> a1 -> a
bugloc L a3
loc (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"(!!): index too large in "String -> String -> String
forall a. [a] -> [a] -> [a]
++String
fnString -> String -> String
forall a. [a] -> [a] -> [a]
++String
", "String -> String -> String
forall a. [a] -> [a] -> [a]
++Int -> String
forall a. Show a => a -> String
show Int
iString -> String -> String
forall a. [a] -> [a] -> [a]
++String
"<"String -> String -> String
forall a. [a] -> [a] -> [a]
++Int -> String
forall a. Show a => a -> String
show Int
n
  where n :: Int
n = [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs

infixl 1 #,<# --,@@

a -> b
f # :: (a -> b) -> f a -> f b
# f a
x = (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f f a
x
m (a -> b)
mf <# :: m (a -> b) -> m a -> m b
<# m a
mx  = m (a -> b) -> m a -> m b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap m (a -> b)
mf m a
mx
--m1 @@ m2 = (m1 =<<) . m2

both :: (t -> m a) -> (t, t) -> m (a, a)
both t -> m a
f (t
x,t
y) = (,) (a -> a -> (a, a)) -> m a -> m (a -> (a, a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
# t -> m a
f t
x m (a -> (a, a)) -> m a -> m (a, a)
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
<# t -> m a
f t
y

bugloc :: L a3 -> a1 -> a
bugloc L a3
loc a1
s = Doc -> a
forall a2 a. Pretty a2 => a2 -> a
ppbug (Doc -> a) -> Doc -> a
forall a b. (a -> b) -> a -> b
$ L a3 -> a1 -> Doc
forall a1 a3. (Pretty a1, Pretty a3) => L a3 -> a1 -> Doc
ppL L a3
loc a1
s

bug :: a2 -> a
bug a2
msg = a2 -> a
forall a2 a. Pretty a2 => a2 -> a
ppbug a2
msg
ppbug :: a2 -> a
ppbug a2
doc = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Pretty a => a -> String
render (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ String -> Int -> a2 -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> Int -> a2 -> Doc
hang String
"Internal error in Compute.Concrete:" Int
4 a2
doc