----------------------------------------------------------------------
-- |
-- Module      : TC
-- Maintainer  : AR
-- Stability   : (stable)
-- Portability : (portable)
--
-- > CVS $Date: 2005/10/02 20:50:19 $
-- > CVS $Author: aarne $
-- > CVS $Revision: 1.11 $
--
-- Thierry Coquand's type checking algorithm that creates a trace
-----------------------------------------------------------------------------

module GF.Compile.TypeCheck.TC (
    AExp(..),
    Theory,
    checkExp,
    inferExp,
    checkBranch,
    eqVal,
    whnf
  ) where

import GF.Data.Operations
import GF.Grammar
import GF.Grammar.Predef

import Control.Monad
--import Data.List (sortBy)
import Data.Maybe
import GF.Text.Pretty

data AExp =
     AVr   Ident Val
   | ACn   QIdent Val
   | AType
   | AInt  Int
   | AFloat Double
   | AStr  String
   | AMeta MetaId Val
   | ALet  (Ident,(Val,AExp)) AExp
   | AApp  AExp AExp Val
   | AAbs  Ident Val AExp
   | AProd Ident AExp AExp
-- -- | AEqs  [([Exp],AExp)] --- not used
   | ARecType [ALabelling]
   | AR    [AAssign]
   | AP    AExp Label Val
   | AGlue AExp AExp
   | AData Val
  deriving (AExp -> AExp -> Bool
(AExp -> AExp -> Bool) -> (AExp -> AExp -> Bool) -> Eq AExp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AExp -> AExp -> Bool
$c/= :: AExp -> AExp -> Bool
== :: AExp -> AExp -> Bool
$c== :: AExp -> AExp -> Bool
Eq,Int -> AExp -> ShowS
[AExp] -> ShowS
AExp -> String
(Int -> AExp -> ShowS)
-> (AExp -> String) -> ([AExp] -> ShowS) -> Show AExp
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [AExp] -> ShowS
$cshowList :: [AExp] -> ShowS
show :: AExp -> String
$cshow :: AExp -> String
showsPrec :: Int -> AExp -> ShowS
$cshowsPrec :: Int -> AExp -> ShowS
Show)

type ALabelling = (Label, AExp)
type AAssign = (Label, (Val, AExp))

type Theory = QIdent -> Err Val

lookupConst :: Theory -> QIdent -> Err Val
lookupConst :: Theory -> Theory
lookupConst Theory
th QIdent
f = Theory
th QIdent
f

lookupVar :: Env -> Ident -> Err Val
lookupVar :: Env -> Ident -> Err Val
lookupVar Env
g Ident
x = Err Val -> (Val -> Err Val) -> Maybe Val -> Err Val
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> Err Val
forall a. String -> Err a
Bad (Doc -> String
forall a. Pretty a => a -> String
render (String
"unknown variable" String -> Ident -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Ident
x))) Val -> Err Val
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Val -> Err Val) -> Maybe Val -> Err Val
forall a b. (a -> b) -> a -> b
$ Ident -> Env -> Maybe Val
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Ident
x ((Ident
identW,Env -> Term -> Val
VClos [] (Int -> Term
Meta Int
0))(Ident, Val) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
g)
-- wild card IW: no error produced, ?0 instead.

type TCEnv = (Int,Env,Env)

--emptyTCEnv :: TCEnv
--emptyTCEnv = (0,[],[])

whnf :: Val -> Err Val
whnf :: Val -> Err Val
whnf Val
v = ---- errIn ("whnf" +++ prt v) $ ---- debug
         case Val
v of
  VApp Val
u Val
w -> do
    Val
u' <- Val -> Err Val
whnf Val
u
    Val
w' <- Val -> Err Val
whnf Val
w
    Val -> Val -> Err Val
app Val
u' Val
w'
  VClos Env
env Term
e -> Env -> Term -> Err Val
eval Env
env Term
e
  Val
_ -> Val -> Err Val
forall (m :: * -> *) a. Monad m => a -> m a
return Val
v

app :: Val -> Val -> Err Val
app :: Val -> Val -> Err Val
app Val
u Val
v = case Val
u of
  VClos Env
env (Abs BindType
_ Ident
x Term
e) -> Env -> Term -> Err Val
eval ((Ident
x,Val
v)(Ident, Val) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
env) Term
e
  Val
_ -> Val -> Err Val
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> Err Val) -> Val -> Err Val
forall a b. (a -> b) -> a -> b
$ Val -> Val -> Val
VApp Val
u Val
v

eval :: Env -> Term -> Err Val
eval :: Env -> Term -> Err Val
eval Env
env Term
e = ---- errIn ("eval" +++ prt e +++ "in" +++ prEnv env) $
             case Term
e of
  Vr Ident
x    -> Env -> Ident -> Err Val
lookupVar Env
env Ident
x
  Q QIdent
c   -> Val -> Err Val
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> Err Val) -> Val -> Err Val
forall a b. (a -> b) -> a -> b
$ QIdent -> Val
VCn QIdent
c
  QC QIdent
c  -> Val -> Err Val
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> Err Val) -> Val -> Err Val
forall a b. (a -> b) -> a -> b
$ QIdent -> Val
VCn QIdent
c ---- == Q ?
  Sort Ident
c  -> Val -> Err Val
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> Err Val) -> Val -> Err Val
forall a b. (a -> b) -> a -> b
$ Val
VType --- the only sort is Type
  App Term
f Term
a -> Err (Err Val) -> Err Val
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Err (Err Val) -> Err Val) -> Err (Err Val) -> Err Val
forall a b. (a -> b) -> a -> b
$ (Val -> Val -> Err Val) -> Err Val -> Err Val -> Err (Err Val)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Val -> Val -> Err Val
app (Env -> Term -> Err Val
eval Env
env Term
f) (Env -> Term -> Err Val
eval Env
env Term
a)
  RecType [Labelling]
xs -> do [(Label, Val)]
xs <- (Labelling -> Err (Label, Val))
-> [Labelling] -> Err [(Label, Val)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(Label
l,Term
e) -> Env -> Term -> Err Val
eval Env
env Term
e Err Val -> (Val -> Err (Label, Val)) -> Err (Label, Val)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Val
e -> (Label, Val) -> Err (Label, Val)
forall (m :: * -> *) a. Monad m => a -> m a
return (Label
l,Val
e)) [Labelling]
xs
                   Val -> Err Val
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Label, Val)] -> Val
VRecType [(Label, Val)]
xs)
  Term
_ -> Val -> Err Val
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> Err Val) -> Val -> Err Val
forall a b. (a -> b) -> a -> b
$ Env -> Term -> Val
VClos Env
env Term
e

eqVal :: Int -> Val -> Val -> Err [(Val,Val)]
eqVal :: Int -> Val -> Val -> Err [(Val, Val)]
eqVal Int
k Val
u1 Val
u2 = ---- errIn (prt u1 +++ "<>" +++ prBracket (show k) +++ prt u2) $
                do
  Val
w1 <- Val -> Err Val
whnf Val
u1
  Val
w2 <- Val -> Err Val
whnf Val
u2
  let v :: Ident -> Val
v = Int -> Ident -> Val
VGen Int
k
  case (Val
w1,Val
w2) of
    (VApp Val
f1 Val
a1, VApp Val
f2 Val
a2) -> ([(Val, Val)] -> [(Val, Val)] -> [(Val, Val)])
-> Err [(Val, Val)] -> Err [(Val, Val)] -> Err [(Val, Val)]
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 [(Val, Val)] -> [(Val, Val)] -> [(Val, Val)]
forall a. [a] -> [a] -> [a]
(++) (Int -> Val -> Val -> Err [(Val, Val)]
eqVal Int
k Val
f1 Val
f2) (Int -> Val -> Val -> Err [(Val, Val)]
eqVal Int
k Val
a1 Val
a2)
    (VClos Env
env1 (Abs BindType
_ Ident
x1 Term
e1), VClos Env
env2 (Abs BindType
_ Ident
x2 Term
e2)) ->
      Int -> Val -> Val -> Err [(Val, Val)]
eqVal (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (Env -> Term -> Val
VClos ((Ident
x1,Ident -> Val
v Ident
x1)(Ident, Val) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
env1) Term
e1) (Env -> Term -> Val
VClos ((Ident
x2,Ident -> Val
v Ident
x1)(Ident, Val) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
env2) Term
e2)
    (VClos Env
env1 (Prod BindType
_ Ident
x1 Term
a1 Term
e1), VClos Env
env2 (Prod BindType
_ Ident
x2 Term
a2 Term
e2)) ->
      ([(Val, Val)] -> [(Val, Val)] -> [(Val, Val)])
-> Err [(Val, Val)] -> Err [(Val, Val)] -> Err [(Val, Val)]
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 [(Val, Val)] -> [(Val, Val)] -> [(Val, Val)]
forall a. [a] -> [a] -> [a]
(++)
        (Int -> Val -> Val -> Err [(Val, Val)]
eqVal Int
k     (Env -> Term -> Val
VClos            Env
env1  Term
a1) (Env -> Term -> Val
VClos            Env
env2  Term
a2))
        (Int -> Val -> Val -> Err [(Val, Val)]
eqVal (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (Env -> Term -> Val
VClos ((Ident
x1,Ident -> Val
v Ident
x1)(Ident, Val) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
env1) Term
e1) (Env -> Term -> Val
VClos ((Ident
x2,Ident -> Val
v Ident
x1)(Ident, Val) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
env2) Term
e2))
    (VGen Int
i Ident
_, VGen Int
j Ident
_) -> [(Val, Val)] -> Err [(Val, Val)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Val
w1,Val
w2) | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
j]
    (VCn (ModuleName
_, Ident
i), VCn (ModuleName
_,Ident
j)) -> [(Val, Val)] -> Err [(Val, Val)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Val
w1,Val
w2) | Ident
i Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
/= Ident
j]
    --- thus ignore qualifications; valid because inheritance cannot
    --- be qualified. Simplifies annotation. AR 17/3/2005
    (Val, Val)
_ -> [(Val, Val)] -> Err [(Val, Val)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Val
w1,Val
w2) | Val
w1 Val -> Val -> Bool
forall a. Eq a => a -> a -> Bool
/= Val
w2]
-- invariant: constraints are in whnf

checkType :: Theory -> TCEnv -> Term -> Err (AExp,[(Val,Val)])
checkType :: Theory -> TCEnv -> Term -> Err (AExp, [(Val, Val)])
checkType Theory
th TCEnv
tenv Term
e = Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val, Val)])
checkExp Theory
th TCEnv
tenv Term
e Val
vType

checkExp :: Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val,Val)])
checkExp :: Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val, Val)])
checkExp Theory
th tenv :: TCEnv
tenv@(Int
k,Env
rho,Env
gamma) Term
e Val
ty = do
  Val
typ <- Val -> Err Val
whnf Val
ty
  let v :: Ident -> Val
v = Int -> Ident -> Val
VGen Int
k
  case Term
e of
    Meta Int
m -> (AExp, [(Val, Val)]) -> Err (AExp, [(Val, Val)])
forall (m :: * -> *) a. Monad m => a -> m a
return ((AExp, [(Val, Val)]) -> Err (AExp, [(Val, Val)]))
-> (AExp, [(Val, Val)]) -> Err (AExp, [(Val, Val)])
forall a b. (a -> b) -> a -> b
$ (Int -> Val -> AExp
AMeta Int
m Val
typ,[])

    Abs BindType
_ Ident
x Term
t -> case Val
typ of
      VClos Env
env (Prod BindType
_ Ident
y Term
a Term
b) -> do
                           Val
a' <- Val -> Err Val
whnf (Val -> Err Val) -> Val -> Err Val
forall a b. (a -> b) -> a -> b
$ Env -> Term -> Val
VClos Env
env Term
a ---
                           (AExp
t',[(Val, Val)]
cs) <- Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val, Val)])
checkExp Theory
th
                                          (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1,(Ident
x,Ident -> Val
v Ident
x)(Ident, Val) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
rho, (Ident
x,Val
a')(Ident, Val) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
gamma) Term
t (Env -> Term -> Val
VClos ((Ident
y,Ident -> Val
v Ident
x)(Ident, Val) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
env) Term
b)
                           (AExp, [(Val, Val)]) -> Err (AExp, [(Val, Val)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Ident -> Val -> AExp -> AExp
AAbs Ident
x Val
a' AExp
t', [(Val, Val)]
cs)
      Val
_ -> String -> Err (AExp, [(Val, Val)])
forall a. String -> Err a
Bad (Doc -> String
forall a. Pretty a => a -> String
render (String
"function type expected for" 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
0 Term
e Doc -> String -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> String
"instead of" Doc -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Int -> Val -> Doc
ppValue TermPrintQual
Unqualified Int
0 Val
typ))

    Let (Ident
x, (Maybe Term
mb_typ, Term
e1)) Term
e2 -> do
      (Val
val,AExp
e1,[(Val, Val)]
cs1) <- case Maybe Term
mb_typ of
                        Just Term
typ -> do (AExp
_,[(Val, Val)]
cs1) <- Theory -> TCEnv -> Term -> Err (AExp, [(Val, Val)])
checkType Theory
th TCEnv
tenv Term
typ
                                       Val
val <- Env -> Term -> Err Val
eval Env
rho Term
typ
                                       (AExp
e1,[(Val, Val)]
cs2) <- Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val, Val)])
checkExp Theory
th TCEnv
tenv Term
e1 Val
val
                                       (Val, AExp, [(Val, Val)]) -> Err (Val, AExp, [(Val, Val)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Val
val,AExp
e1,[(Val, Val)]
cs1[(Val, Val)] -> [(Val, Val)] -> [(Val, Val)]
forall a. [a] -> [a] -> [a]
++[(Val, Val)]
cs2)
                        Maybe Term
Nothing  -> do (AExp
e1,Val
val,[(Val, Val)]
cs) <- Theory -> TCEnv -> Term -> Err (AExp, Val, [(Val, Val)])
inferExp Theory
th TCEnv
tenv Term
e1
                                       (Val, AExp, [(Val, Val)]) -> Err (Val, AExp, [(Val, Val)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Val
val,AExp
e1,[(Val, Val)]
cs)
      (AExp
e2,[(Val, Val)]
cs2) <- Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val, Val)])
checkExp Theory
th (Int
k,Env
rho,(Ident
x,Val
val)(Ident, Val) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
gamma) Term
e2 Val
typ
      (AExp, [(Val, Val)]) -> Err (AExp, [(Val, Val)])
forall (m :: * -> *) a. Monad m => a -> m a
return ((Ident, (Val, AExp)) -> AExp -> AExp
ALet (Ident
x,(Val
val,AExp
e1)) AExp
e2, [(Val, Val)]
cs1[(Val, Val)] -> [(Val, Val)] -> [(Val, Val)]
forall a. [a] -> [a] -> [a]
++[(Val, Val)]
cs2)

    Prod BindType
_ Ident
x Term
a Term
b -> do
      Bool -> String -> Err ()
forall (m :: * -> *). ErrorMonad m => Bool -> String -> m ()
testErr (Val
typ Val -> Val -> Bool
forall a. Eq a => a -> a -> Bool
== Val
vType) String
"expected Type"
      (AExp
a',[(Val, Val)]
csa) <- Theory -> TCEnv -> Term -> Err (AExp, [(Val, Val)])
checkType Theory
th TCEnv
tenv Term
a
      (AExp
b',[(Val, Val)]
csb) <- Theory -> TCEnv -> Term -> Err (AExp, [(Val, Val)])
checkType Theory
th (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1, (Ident
x,Ident -> Val
v Ident
x)(Ident, Val) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
rho, (Ident
x,Env -> Term -> Val
VClos Env
rho Term
a)(Ident, Val) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
gamma) Term
b
      (AExp, [(Val, Val)]) -> Err (AExp, [(Val, Val)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Ident -> AExp -> AExp -> AExp
AProd Ident
x AExp
a' AExp
b', [(Val, Val)]
csa [(Val, Val)] -> [(Val, Val)] -> [(Val, Val)]
forall a. [a] -> [a] -> [a]
++ [(Val, Val)]
csb)

    R [Assign]
xs ->
      case Val
typ of
        VRecType [(Label, Val)]
ys -> do case [Label
l | (Label
l,Val
_) <- [(Label, Val)]
ys, Maybe (Maybe Term, Term) -> Bool
forall a. Maybe a -> Bool
isNothing (Label -> [Assign] -> Maybe (Maybe Term, Term)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Label
l [Assign]
xs)] of
                            [] -> () -> Err ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                            [Label]
ls -> String -> Err ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (Doc -> String
forall a. Pretty a => a -> String
render (String
"no value given for label:" String -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> [Doc] -> Doc
forall a. Pretty a => [a] -> Doc
fsep (Char -> [Label] -> [Doc]
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> [a2] -> [Doc]
punctuate Char
',' [Label]
ls)))
                          [(AAssign, [(Val, Val)])]
r <- (Assign -> Err (AAssign, [(Val, Val)]))
-> [Assign] -> Err [(AAssign, [(Val, Val)])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Theory
-> TCEnv -> [(Label, Val)] -> Assign -> Err (AAssign, [(Val, Val)])
checkAssign Theory
th TCEnv
tenv [(Label, Val)]
ys) [Assign]
xs
                          let ([AAssign]
xs,[[(Val, Val)]]
css) = [(AAssign, [(Val, Val)])] -> ([AAssign], [[(Val, Val)]])
forall a b. [(a, b)] -> ([a], [b])
unzip [(AAssign, [(Val, Val)])]
r
                          (AExp, [(Val, Val)]) -> Err (AExp, [(Val, Val)])
forall (m :: * -> *) a. Monad m => a -> m a
return ([AAssign] -> AExp
AR [AAssign]
xs, [[(Val, Val)]] -> [(Val, Val)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Val, Val)]]
css)
        Val
_           -> String -> Err (AExp, [(Val, Val)])
forall a. String -> Err a
Bad (Doc -> String
forall a. Pretty a => a -> String
render (String
"record type expected for" 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
0 Term
e Doc -> String -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> String
"instead of" Doc -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Int -> Val -> Doc
ppValue TermPrintQual
Unqualified Int
0 Val
typ))

    P Term
r Label
l -> do (AExp
r',[(Val, Val)]
cs) <- Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val, Val)])
checkExp Theory
th TCEnv
tenv Term
r ([(Label, Val)] -> Val
VRecType [(Label
l,Val
typ)])
                (AExp, [(Val, Val)]) -> Err (AExp, [(Val, Val)])
forall (m :: * -> *) a. Monad m => a -> m a
return (AExp -> Label -> Val -> AExp
AP AExp
r' Label
l Val
typ,[(Val, Val)]
cs)

    Glue Term
x Term
y -> do [(Val, Val)]
cs1 <- Int -> Val -> Val -> Err [(Val, Val)]
eqVal Int
k Val
valAbsFloat Val
typ
                   (AExp
x,[(Val, Val)]
cs2) <- Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val, Val)])
checkExp Theory
th TCEnv
tenv Term
x Val
typ
                   (AExp
y,[(Val, Val)]
cs3) <- Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val, Val)])
checkExp Theory
th TCEnv
tenv Term
y Val
typ
                   (AExp, [(Val, Val)]) -> Err (AExp, [(Val, Val)])
forall (m :: * -> *) a. Monad m => a -> m a
return (AExp -> AExp -> AExp
AGlue AExp
x AExp
y,[(Val, Val)]
cs1[(Val, Val)] -> [(Val, Val)] -> [(Val, Val)]
forall a. [a] -> [a] -> [a]
++[(Val, Val)]
cs2[(Val, Val)] -> [(Val, Val)] -> [(Val, Val)]
forall a. [a] -> [a] -> [a]
++[(Val, Val)]
cs3)
    Term
_ -> Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val, Val)])
checkInferExp Theory
th TCEnv
tenv Term
e Val
typ

checkInferExp :: Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val,Val)])
checkInferExp :: Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val, Val)])
checkInferExp Theory
th tenv :: TCEnv
tenv@(Int
k,Env
_,Env
_) Term
e Val
typ = do
  (AExp
e',Val
w,[(Val, Val)]
cs1) <- Theory -> TCEnv -> Term -> Err (AExp, Val, [(Val, Val)])
inferExp Theory
th TCEnv
tenv Term
e
  [(Val, Val)]
cs2 <- Int -> Val -> Val -> Err [(Val, Val)]
eqVal Int
k Val
w Val
typ
  (AExp, [(Val, Val)]) -> Err (AExp, [(Val, Val)])
forall (m :: * -> *) a. Monad m => a -> m a
return (AExp
e',[(Val, Val)]
cs1 [(Val, Val)] -> [(Val, Val)] -> [(Val, Val)]
forall a. [a] -> [a] -> [a]
++ [(Val, Val)]
cs2)

inferExp :: Theory -> TCEnv -> Term -> Err (AExp, Val, [(Val,Val)])
inferExp :: Theory -> TCEnv -> Term -> Err (AExp, Val, [(Val, Val)])
inferExp Theory
th tenv :: TCEnv
tenv@(Int
k,Env
rho,Env
gamma) Term
e = case Term
e of
   Vr Ident
x -> (Val -> AExp)
-> Err (Val, [(Val, Val)]) -> Err (AExp, Val, [(Val, Val)])
mkAnnot (Ident -> Val -> AExp
AVr Ident
x) (Err (Val, [(Val, Val)]) -> Err (AExp, Val, [(Val, Val)]))
-> Err (Val, [(Val, Val)]) -> Err (AExp, Val, [(Val, Val)])
forall a b. (a -> b) -> a -> b
$ Err Val -> Err (Val, [(Val, Val)])
noConstr (Err Val -> Err (Val, [(Val, Val)]))
-> Err Val -> Err (Val, [(Val, Val)])
forall a b. (a -> b) -> a -> b
$ Env -> Ident -> Err Val
lookupVar Env
gamma Ident
x
   Q (ModuleName
m,Ident
c) | ModuleName
m ModuleName -> ModuleName -> Bool
forall a. Eq a => a -> a -> Bool
== ModuleName
cPredefAbs Bool -> Bool -> Bool
&& Ident -> Bool
isPredefCat Ident
c
                     -> (AExp, Val, [(Val, Val)]) -> Err (AExp, Val, [(Val, Val)])
forall (m :: * -> *) a. Monad m => a -> m a
return (QIdent -> Val -> AExp
ACn (ModuleName
m,Ident
c) Val
vType, Val
vType, [])
           | Bool
otherwise -> (Val -> AExp)
-> Err (Val, [(Val, Val)]) -> Err (AExp, Val, [(Val, Val)])
mkAnnot (QIdent -> Val -> AExp
ACn (ModuleName
m,Ident
c)) (Err (Val, [(Val, Val)]) -> Err (AExp, Val, [(Val, Val)]))
-> Err (Val, [(Val, Val)]) -> Err (AExp, Val, [(Val, Val)])
forall a b. (a -> b) -> a -> b
$ Err Val -> Err (Val, [(Val, Val)])
noConstr (Err Val -> Err (Val, [(Val, Val)]))
-> Err Val -> Err (Val, [(Val, Val)])
forall a b. (a -> b) -> a -> b
$ Theory -> Theory
lookupConst Theory
th (ModuleName
m,Ident
c)
   QC QIdent
c -> (Val -> AExp)
-> Err (Val, [(Val, Val)]) -> Err (AExp, Val, [(Val, Val)])
mkAnnot (QIdent -> Val -> AExp
ACn QIdent
c) (Err (Val, [(Val, Val)]) -> Err (AExp, Val, [(Val, Val)]))
-> Err (Val, [(Val, Val)]) -> Err (AExp, Val, [(Val, Val)])
forall a b. (a -> b) -> a -> b
$ Err Val -> Err (Val, [(Val, Val)])
noConstr (Err Val -> Err (Val, [(Val, Val)]))
-> Err Val -> Err (Val, [(Val, Val)])
forall a b. (a -> b) -> a -> b
$ Theory -> Theory
lookupConst Theory
th QIdent
c ----
   EInt Int
i -> (AExp, Val, [(Val, Val)]) -> Err (AExp, Val, [(Val, Val)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> AExp
AInt Int
i, Val
valAbsInt, [])
   EFloat Double
i -> (AExp, Val, [(Val, Val)]) -> Err (AExp, Val, [(Val, Val)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Double -> AExp
AFloat Double
i, Val
valAbsFloat, [])
   K String
i -> (AExp, Val, [(Val, Val)]) -> Err (AExp, Val, [(Val, Val)])
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> AExp
AStr String
i, Val
valAbsString, [])
   Sort Ident
_ -> (AExp, Val, [(Val, Val)]) -> Err (AExp, Val, [(Val, Val)])
forall (m :: * -> *) a. Monad m => a -> m a
return (AExp
AType, Val
vType, [])
   RecType [Labelling]
xs -> do [(ALabelling, [(Val, Val)])]
r <- (Labelling -> Err (ALabelling, [(Val, Val)]))
-> [Labelling] -> Err [(ALabelling, [(Val, Val)])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Theory -> TCEnv -> Labelling -> Err (ALabelling, [(Val, Val)])
checkLabelling Theory
th TCEnv
tenv) [Labelling]
xs
                    let ([ALabelling]
xs,[[(Val, Val)]]
css) = [(ALabelling, [(Val, Val)])] -> ([ALabelling], [[(Val, Val)]])
forall a b. [(a, b)] -> ([a], [b])
unzip [(ALabelling, [(Val, Val)])]
r
                    (AExp, Val, [(Val, Val)]) -> Err (AExp, Val, [(Val, Val)])
forall (m :: * -> *) a. Monad m => a -> m a
return ([ALabelling] -> AExp
ARecType [ALabelling]
xs, Val
vType, [[(Val, Val)]] -> [(Val, Val)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Val, Val)]]
css)
   Let (Ident
x, (Maybe Term
mb_typ, Term
e1)) Term
e2 -> do
    (Val
val1,AExp
e1,[(Val, Val)]
cs1) <- case Maybe Term
mb_typ of
                       Just Term
typ -> do (AExp
_,[(Val, Val)]
cs1) <- Theory -> TCEnv -> Term -> Err (AExp, [(Val, Val)])
checkType Theory
th TCEnv
tenv Term
typ
                                      Val
val <- Env -> Term -> Err Val
eval Env
rho Term
typ
                                      (AExp
e1,[(Val, Val)]
cs2) <- Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val, Val)])
checkExp Theory
th TCEnv
tenv Term
e1 Val
val
                                      (Val, AExp, [(Val, Val)]) -> Err (Val, AExp, [(Val, Val)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Val
val,AExp
e1,[(Val, Val)]
cs1[(Val, Val)] -> [(Val, Val)] -> [(Val, Val)]
forall a. [a] -> [a] -> [a]
++[(Val, Val)]
cs2)
                       Maybe Term
Nothing  -> do (AExp
e1,Val
val,[(Val, Val)]
cs) <- Theory -> TCEnv -> Term -> Err (AExp, Val, [(Val, Val)])
inferExp Theory
th TCEnv
tenv Term
e1
                                      (Val, AExp, [(Val, Val)]) -> Err (Val, AExp, [(Val, Val)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Val
val,AExp
e1,[(Val, Val)]
cs)
    (AExp
e2,Val
val2,[(Val, Val)]
cs2) <- Theory -> TCEnv -> Term -> Err (AExp, Val, [(Val, Val)])
inferExp Theory
th (Int
k,Env
rho,(Ident
x,Val
val1)(Ident, Val) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
gamma) Term
e2
    (AExp, Val, [(Val, Val)]) -> Err (AExp, Val, [(Val, Val)])
forall (m :: * -> *) a. Monad m => a -> m a
return ((Ident, (Val, AExp)) -> AExp -> AExp
ALet (Ident
x,(Val
val1,AExp
e1)) AExp
e2, Val
val2, [(Val, Val)]
cs1[(Val, Val)] -> [(Val, Val)] -> [(Val, Val)]
forall a. [a] -> [a] -> [a]
++[(Val, Val)]
cs2)
   App Term
f Term
t -> do
    (AExp
f',Val
w,[(Val, Val)]
csf) <- Theory -> TCEnv -> Term -> Err (AExp, Val, [(Val, Val)])
inferExp Theory
th TCEnv
tenv Term
f
    Val
typ <- Val -> Err Val
whnf Val
w
    case Val
typ of
      VClos Env
env (Prod BindType
_ Ident
x Term
a Term
b) -> do
        (AExp
a',[(Val, Val)]
csa) <- Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val, Val)])
checkExp Theory
th TCEnv
tenv Term
t (Env -> Term -> Val
VClos Env
env Term
a)
        Val
b' <- Val -> Err Val
whnf (Val -> Err Val) -> Val -> Err Val
forall a b. (a -> b) -> a -> b
$ Env -> Term -> Val
VClos ((Ident
x,Env -> Term -> Val
VClos Env
rho Term
t)(Ident, Val) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
env) Term
b
        (AExp, Val, [(Val, Val)]) -> Err (AExp, Val, [(Val, Val)])
forall (m :: * -> *) a. Monad m => a -> m a
return ((AExp, Val, [(Val, Val)]) -> Err (AExp, Val, [(Val, Val)]))
-> (AExp, Val, [(Val, Val)]) -> Err (AExp, Val, [(Val, Val)])
forall a b. (a -> b) -> a -> b
$ (AExp -> AExp -> Val -> AExp
AApp AExp
f' AExp
a' Val
b', Val
b', [(Val, Val)]
csf [(Val, Val)] -> [(Val, Val)] -> [(Val, Val)]
forall a. [a] -> [a] -> [a]
++ [(Val, Val)]
csa)
      Val
_ -> String -> Err (AExp, Val, [(Val, Val)])
forall a. String -> Err a
Bad (Doc -> String
forall a. Pretty a => a -> String
render (String
"Prod expected for function" 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
0 Term
f Doc -> String -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> String
"instead of" Doc -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Int -> Val -> Doc
ppValue TermPrintQual
Unqualified Int
0 Val
typ))
   Term
_ -> String -> Err (AExp, Val, [(Val, Val)])
forall a. String -> Err a
Bad (Doc -> String
forall a. Pretty a => a -> String
render (String
"cannot infer type of expression" 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
0 Term
e))

checkLabelling :: Theory -> TCEnv -> Labelling -> Err (ALabelling, [(Val,Val)])
checkLabelling :: Theory -> TCEnv -> Labelling -> Err (ALabelling, [(Val, Val)])
checkLabelling Theory
th TCEnv
tenv (Label
lbl,Term
typ) = do
  (AExp
atyp,[(Val, Val)]
cs) <- Theory -> TCEnv -> Term -> Err (AExp, [(Val, Val)])
checkType Theory
th TCEnv
tenv Term
typ
  (ALabelling, [(Val, Val)]) -> Err (ALabelling, [(Val, Val)])
forall (m :: * -> *) a. Monad m => a -> m a
return ((Label
lbl,AExp
atyp),[(Val, Val)]
cs)

checkAssign :: Theory -> TCEnv -> [(Label,Val)] -> Assign -> Err (AAssign, [(Val,Val)])
checkAssign :: Theory
-> TCEnv -> [(Label, Val)] -> Assign -> Err (AAssign, [(Val, Val)])
checkAssign Theory
th tenv :: TCEnv
tenv@(Int
k,Env
rho,Env
gamma) [(Label, Val)]
typs (Label
lbl,(Just Term
typ,Term
exp)) = do
  (AExp
atyp,[(Val, Val)]
cs1) <- Theory -> TCEnv -> Term -> Err (AExp, [(Val, Val)])
checkType Theory
th TCEnv
tenv Term
typ
  Val
val <- Env -> Term -> Err Val
eval Env
rho Term
typ
  [(Val, Val)]
cs2 <- case Label -> [(Label, Val)] -> Maybe Val
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Label
lbl [(Label, Val)]
typs of
           Maybe Val
Nothing   -> [(Val, Val)] -> Err [(Val, Val)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
           Just Val
val0 -> Int -> Val -> Val -> Err [(Val, Val)]
eqVal Int
k Val
val Val
val0
  (AExp
aexp,[(Val, Val)]
cs3) <- Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val, Val)])
checkExp Theory
th TCEnv
tenv Term
exp Val
val
  (AAssign, [(Val, Val)]) -> Err (AAssign, [(Val, Val)])
forall (m :: * -> *) a. Monad m => a -> m a
return ((Label
lbl,(Val
val,AExp
aexp)),[(Val, Val)]
cs1[(Val, Val)] -> [(Val, Val)] -> [(Val, Val)]
forall a. [a] -> [a] -> [a]
++[(Val, Val)]
cs2[(Val, Val)] -> [(Val, Val)] -> [(Val, Val)]
forall a. [a] -> [a] -> [a]
++[(Val, Val)]
cs3)
checkAssign Theory
th tenv :: TCEnv
tenv@(Int
k,Env
rho,Env
gamma) [(Label, Val)]
typs (Label
lbl,(Maybe Term
Nothing,Term
exp)) = do
  case Label -> [(Label, Val)] -> Maybe Val
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Label
lbl [(Label, Val)]
typs of
    Maybe Val
Nothing  -> do (AExp
aexp,Val
val,[(Val, Val)]
cs) <- Theory -> TCEnv -> Term -> Err (AExp, Val, [(Val, Val)])
inferExp Theory
th TCEnv
tenv Term
exp
                   (AAssign, [(Val, Val)]) -> Err (AAssign, [(Val, Val)])
forall (m :: * -> *) a. Monad m => a -> m a
return ((Label
lbl,(Val
val,AExp
aexp)),[(Val, Val)]
cs)
    Just Val
val -> do (AExp
aexp,[(Val, Val)]
cs) <- Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val, Val)])
checkExp Theory
th TCEnv
tenv Term
exp Val
val
                   (AAssign, [(Val, Val)]) -> Err (AAssign, [(Val, Val)])
forall (m :: * -> *) a. Monad m => a -> m a
return ((Label
lbl,(Val
val,AExp
aexp)),[(Val, Val)]
cs)

checkBranch :: Theory -> TCEnv -> Equation -> Val -> Err (([Term],AExp),[(Val,Val)])
checkBranch :: Theory
-> TCEnv -> Equation -> Val -> Err (([Term], AExp), [(Val, Val)])
checkBranch Theory
th TCEnv
tenv b :: Equation
b@([Patt]
ps,Term
t) Val
ty = String
-> Err (([Term], AExp), [(Val, Val)])
-> Err (([Term], AExp), [(Val, Val)])
forall (m :: * -> *) a. ErrorMonad m => String -> m a -> m a
errIn (String
"branch" String -> ShowS
+++ Equation -> String
forall a. Show a => a -> String
show Equation
b) (Err (([Term], AExp), [(Val, Val)])
 -> Err (([Term], AExp), [(Val, Val)]))
-> Err (([Term], AExp), [(Val, Val)])
-> Err (([Term], AExp), [(Val, Val)])
forall a b. (a -> b) -> a -> b
$
                                  TCEnv -> [Term] -> Val -> Err (([Term], AExp), [(Val, Val)])
chB TCEnv
tenv' [Term]
ps' Val
ty
 where

  ([Term]
ps',Int
_,Env
rho2,Int
k') = Int -> [Patt] -> ([Term], Int, Env, Int)
forall (t :: * -> *).
Foldable t =>
Int -> t Patt -> ([Term], Int, Env, Int)
ps2ts Int
k [Patt]
ps
  tenv' :: TCEnv
tenv' = (Int
k, Env
rho2Env -> Env -> Env
forall a. [a] -> [a] -> [a]
++Env
rho, Env
gamma) ---- k' ?
  (Int
k,Env
rho,Env
gamma) = TCEnv
tenv

  chB :: TCEnv -> [Term] -> Val -> Err (([Term], AExp), [(Val, Val)])
chB tenv :: TCEnv
tenv@(Int
k,Env
rho,Env
gamma) [Term]
ps Val
ty = case [Term]
ps of
    Term
p:[Term]
ps2 -> do
      Val
typ <- Val -> Err Val
whnf Val
ty
      case Val
typ of
        VClos Env
env (Prod BindType
_ Ident
y Term
a Term
b) -> do
          Val
a' <- Val -> Err Val
whnf (Val -> Err Val) -> Val -> Err Val
forall a b. (a -> b) -> a -> b
$ Env -> Term -> Val
VClos Env
env Term
a
          (Val
p', Env
sigma, Env
binds, [(Val, Val)]
cs1) <- TCEnv -> Term -> Ident -> Val -> Err (Val, Env, Env, [(Val, Val)])
forall p.
TCEnv -> Term -> p -> Val -> Err (Val, Env, Env, [(Val, Val)])
checkP TCEnv
tenv Term
p Ident
y Val
a'
          let tenv' :: TCEnv
tenv' = (Env -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Env
binds, Env
sigma Env -> Env -> Env
forall a. [a] -> [a] -> [a]
++ Env
rho, Env
binds Env -> Env -> Env
forall a. [a] -> [a] -> [a]
++ Env
gamma)
          (([Term]
ps',AExp
exp),[(Val, Val)]
cs2) <- TCEnv -> [Term] -> Val -> Err (([Term], AExp), [(Val, Val)])
chB TCEnv
tenv' [Term]
ps2 (Env -> Term -> Val
VClos ((Ident
y,Val
p')(Ident, Val) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
env) Term
b)
          (([Term], AExp), [(Val, Val)])
-> Err (([Term], AExp), [(Val, Val)])
forall (m :: * -> *) a. Monad m => a -> m a
return ((Term
pTerm -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:[Term]
ps',AExp
exp), [(Val, Val)]
cs1 [(Val, Val)] -> [(Val, Val)] -> [(Val, Val)]
forall a. [a] -> [a] -> [a]
++ [(Val, Val)]
cs2) -- don't change the patt
        Val
_ -> String -> Err (([Term], AExp), [(Val, Val)])
forall a. String -> Err a
Bad (Doc -> String
forall a. Pretty a => a -> String
render (String
"Product expected for definiens" 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
0 Term
t Doc -> String -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> String
"instead of" Doc -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Int -> Val -> Doc
ppValue TermPrintQual
Unqualified Int
0 Val
typ))
    [] -> do
      (AExp
e,[(Val, Val)]
cs) <- Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val, Val)])
checkExp Theory
th TCEnv
tenv Term
t Val
ty
      (([Term], AExp), [(Val, Val)])
-> Err (([Term], AExp), [(Val, Val)])
forall (m :: * -> *) a. Monad m => a -> m a
return (([],AExp
e),[(Val, Val)]
cs)
  checkP :: TCEnv -> Term -> p -> Val -> Err (Val, Env, Env, [(Val, Val)])
checkP env :: TCEnv
env@(Int
k,Env
rho,Env
gamma) Term
t p
x Val
a = do
     (Env
delta,[(Val, Val)]
cs) <- Theory -> TCEnv -> Term -> Val -> Err (Env, [(Val, Val)])
checkPatt Theory
th TCEnv
env Term
t Val
a
     let sigma :: Env
sigma = [(Ident
x, Int -> Ident -> Val
VGen Int
i Ident
x) | ((Ident
x,Val
_),Int
i) <- Env -> [Int] -> [((Ident, Val), Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip Env
delta [Int
k..]]
     (Val, Env, Env, [(Val, Val)]) -> Err (Val, Env, Env, [(Val, Val)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Env -> Term -> Val
VClos Env
sigma Term
t, Env
sigma, Env
delta, [(Val, Val)]
cs)

  ps2ts :: Int -> t Patt -> ([Term], Int, Env, Int)
ps2ts Int
k = (Patt -> ([Term], Int, Env, Int) -> ([Term], Int, Env, Int))
-> ([Term], Int, Env, Int) -> t Patt -> ([Term], Int, Env, Int)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Patt -> ([Term], Int, Env, Int) -> ([Term], Int, Env, Int)
p2t ([],Int
0,[],Int
k)
  p2t :: Patt -> ([Term], Int, Env, Int) -> ([Term], Int, Env, Int)
p2t Patt
p ([Term]
ps,Int
i,Env
g,Int
k) = case Patt
p of
     Patt
PW      -> (Int -> Term
Meta Int
i Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
ps, Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1,Env
g,Int
k)
     PV Ident
x    -> (Ident -> Term
Vr Ident
x   Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
ps, Int
i, Ident -> Int -> Env -> Env
upd Ident
x Int
k Env
g,Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
     PAs Ident
x Patt
p -> Patt -> ([Term], Int, Env, Int) -> ([Term], Int, Env, Int)
p2t Patt
p ([Term]
ps,Int
i,Env
g,Int
k)
     PString String
s -> (String -> Term
K String
s Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
ps, Int
i, Env
g, Int
k)
     PInt Int
n -> (Int -> Term
EInt Int
n Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
ps, Int
i, Env
g, Int
k)
     PFloat Double
n -> (Double -> Term
EFloat Double
n Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
ps, Int
i, Env
g, Int
k)
     PP QIdent
c [Patt]
xs -> (Term -> [Term] -> Term
mkApp (QIdent -> Term
Q QIdent
c) [Term]
xss Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
ps, Int
j, Env
g',Int
k')
                    where ([Term]
xss,Int
j,Env
g',Int
k') = (Patt -> ([Term], Int, Env, Int) -> ([Term], Int, Env, Int))
-> ([Term], Int, Env, Int) -> [Patt] -> ([Term], Int, Env, Int)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Patt -> ([Term], Int, Env, Int) -> ([Term], Int, Env, Int)
p2t ([],Int
i,Env
g,Int
k) [Patt]
xs
     PImplArg Patt
p -> Patt -> ([Term], Int, Env, Int) -> ([Term], Int, Env, Int)
p2t Patt
p ([Term]
ps,Int
i,Env
g,Int
k)
     PTilde Term
t -> (Term
t Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
ps, Int
i, Env
g, Int
k)
     Patt
_ -> String -> ([Term], Int, Env, Int)
forall a. HasCallStack => String -> a
error (String -> ([Term], Int, Env, Int))
-> String -> ([Term], Int, Env, Int)
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Pretty a => a -> String
render (String
"undefined p2t case" String -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Integer -> Patt -> Doc
forall a. (Num a, Ord a) => TermPrintQual -> a -> Patt -> Doc
ppPatt TermPrintQual
Unqualified Integer
0 Patt
p Doc -> String -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> String
"in checkBranch")

  upd :: Ident -> Int -> Env -> Env
upd Ident
x Int
k Env
g = (Ident
x, Int -> Ident -> Val
VGen Int
k Ident
x) (Ident, Val) -> Env -> Env
forall a. a -> [a] -> [a]
: Env
g --- hack to recognize pattern variables


checkPatt :: Theory -> TCEnv -> Term -> Val -> Err (Binds,[(Val,Val)])
checkPatt :: Theory -> TCEnv -> Term -> Val -> Err (Env, [(Val, Val)])
checkPatt Theory
th TCEnv
tenv Term
exp Val
val = do
  (AExp
aexp,Val
_,[(Val, Val)]
cs) <- TCEnv -> Term -> Val -> Err (AExp, Val, [(Val, Val)])
forall a c a. (a, Env, c) -> Term -> Val -> Err (AExp, Val, [a])
checkExpP TCEnv
tenv Term
exp Val
val
  let binds :: Env
binds = AExp -> Env
extrBinds AExp
aexp
  (Env, [(Val, Val)]) -> Err (Env, [(Val, Val)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Env
binds,[(Val, Val)]
cs)
 where
   extrBinds :: AExp -> Env
extrBinds AExp
aexp = case AExp
aexp of
     AVr Ident
i Val
v    -> [(Ident
i,Val
v)]
     AApp AExp
f AExp
a Val
_ -> AExp -> Env
extrBinds AExp
f Env -> Env -> Env
forall a. [a] -> [a] -> [a]
++ AExp -> Env
extrBinds AExp
a
     AExp
_ -> [] -- no other cases are possible

--- ad hoc, to find types of variables
   checkExpP :: (a, Env, c) -> Term -> Val -> Err (AExp, Val, [a])
checkExpP tenv :: (a, Env, c)
tenv@(a
k,Env
rho,c
gamma) Term
exp Val
val = case Term
exp of
     Meta Int
m -> (AExp, Val, [a]) -> Err (AExp, Val, [a])
forall (m :: * -> *) a. Monad m => a -> m a
return ((AExp, Val, [a]) -> Err (AExp, Val, [a]))
-> (AExp, Val, [a]) -> Err (AExp, Val, [a])
forall a b. (a -> b) -> a -> b
$ (Int -> Val -> AExp
AMeta Int
m Val
val, Val
val, [])
     Vr Ident
x   -> (AExp, Val, [a]) -> Err (AExp, Val, [a])
forall (m :: * -> *) a. Monad m => a -> m a
return ((AExp, Val, [a]) -> Err (AExp, Val, [a]))
-> (AExp, Val, [a]) -> Err (AExp, Val, [a])
forall a b. (a -> b) -> a -> b
$ (Ident -> Val -> AExp
AVr   Ident
x Val
val, Val
val, [])
     EInt Int
i -> (AExp, Val, [a]) -> Err (AExp, Val, [a])
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> AExp
AInt Int
i, Val
valAbsInt, [])
     EFloat Double
i -> (AExp, Val, [a]) -> Err (AExp, Val, [a])
forall (m :: * -> *) a. Monad m => a -> m a
return (Double -> AExp
AFloat Double
i, Val
valAbsFloat, [])
     K String
s    -> (AExp, Val, [a]) -> Err (AExp, Val, [a])
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> AExp
AStr String
s, Val
valAbsString, [])

     Q QIdent
c  -> do
       Val
typ <- Theory -> Theory
lookupConst Theory
th QIdent
c
       (AExp, Val, [a]) -> Err (AExp, Val, [a])
forall (m :: * -> *) a. Monad m => a -> m a
return ((AExp, Val, [a]) -> Err (AExp, Val, [a]))
-> (AExp, Val, [a]) -> Err (AExp, Val, [a])
forall a b. (a -> b) -> a -> b
$ (QIdent -> Val -> AExp
ACn QIdent
c Val
typ, Val
typ, [])
     QC QIdent
c  -> do
       Val
typ <- Theory -> Theory
lookupConst Theory
th QIdent
c
       (AExp, Val, [a]) -> Err (AExp, Val, [a])
forall (m :: * -> *) a. Monad m => a -> m a
return ((AExp, Val, [a]) -> Err (AExp, Val, [a]))
-> (AExp, Val, [a]) -> Err (AExp, Val, [a])
forall a b. (a -> b) -> a -> b
$ (QIdent -> Val -> AExp
ACn QIdent
c Val
typ, Val
typ, []) ----
     App Term
f Term
t -> do
       (AExp
f',Val
w,[a]
csf) <- (a, Env, c) -> Term -> Val -> Err (AExp, Val, [a])
checkExpP (a, Env, c)
tenv Term
f Val
val
       Val
typ <- Val -> Err Val
whnf Val
w
       case Val
typ of
         VClos Env
env (Prod BindType
_ Ident
x Term
a Term
b) -> do
           (AExp
a',Val
_,[a]
csa) <- (a, Env, c) -> Term -> Val -> Err (AExp, Val, [a])
checkExpP (a, Env, c)
tenv Term
t (Env -> Term -> Val
VClos Env
env Term
a)
           Val
b' <- Val -> Err Val
whnf (Val -> Err Val) -> Val -> Err Val
forall a b. (a -> b) -> a -> b
$ Env -> Term -> Val
VClos ((Ident
x,Env -> Term -> Val
VClos Env
rho Term
t)(Ident, Val) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
env) Term
b
           (AExp, Val, [a]) -> Err (AExp, Val, [a])
forall (m :: * -> *) a. Monad m => a -> m a
return ((AExp, Val, [a]) -> Err (AExp, Val, [a]))
-> (AExp, Val, [a]) -> Err (AExp, Val, [a])
forall a b. (a -> b) -> a -> b
$ (AExp -> AExp -> Val -> AExp
AApp AExp
f' AExp
a' Val
b', Val
b', [a]
csf [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
csa)
         Val
_ -> String -> Err (AExp, Val, [a])
forall a. String -> Err a
Bad (Doc -> String
forall a. Pretty a => a -> String
render (String
"Prod expected for function" 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
0 Term
f Doc -> String -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> String
"instead of" Doc -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> TermPrintQual -> Int -> Val -> Doc
ppValue TermPrintQual
Unqualified Int
0 Val
typ))
     Term
_ -> String -> Err (AExp, Val, [a])
forall a. String -> Err a
Bad (Doc -> String
forall a. Pretty a => a -> String
render (String
"cannot typecheck pattern" 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
0 Term
exp))

-- auxiliaries

noConstr :: Err Val -> Err (Val,[(Val,Val)])
noConstr :: Err Val -> Err (Val, [(Val, Val)])
noConstr Err Val
er = Err Val
er Err Val
-> (Val -> Err (Val, [(Val, Val)])) -> Err (Val, [(Val, Val)])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Val
v -> (Val, [(Val, Val)]) -> Err (Val, [(Val, Val)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Val
v,[]))

mkAnnot :: (Val -> AExp) -> Err (Val,[(Val,Val)]) -> Err (AExp,Val,[(Val,Val)])
mkAnnot :: (Val -> AExp)
-> Err (Val, [(Val, Val)]) -> Err (AExp, Val, [(Val, Val)])
mkAnnot Val -> AExp
a Err (Val, [(Val, Val)])
ti = do
  (Val
v,[(Val, Val)]
cs) <- Err (Val, [(Val, Val)])
ti
  (AExp, Val, [(Val, Val)]) -> Err (AExp, Val, [(Val, Val)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> AExp
a Val
v, Val
v, [(Val, Val)]
cs)