{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverlappingInstances #-}

-- Implementation of Hindley Milner algorithm W
-- to system F translation by Ryan Wisnesky, with extensions for Hydra by Joshua Shinavier
-- License: Apache 2.0 https://www.apache.org/licenses/LICENSE-2.0

module Hydra.Inference.AlgorithmW where

import Hydra.Minimal

import Prelude
import Control.Monad.Except
import Control.Monad.State
import Data.List (nub)
import Debug.Trace


natType :: MTy
natType = LiteralType -> MTy
TyLit (LiteralType -> MTy) -> LiteralType -> MTy
forall a b. (a -> b) -> a -> b
$ IntegerType -> LiteralType
LiteralTypeInteger IntegerType
IntegerTypeInt32
constNeg :: Expr
constNeg = Prim -> Expr
Const (Prim -> Expr) -> Prim -> Expr
forall a b. (a -> b) -> a -> b
$ TypedPrimitive -> Prim
TypedPrim (TypedPrimitive -> Prim) -> TypedPrimitive -> Prim
forall a b. (a -> b) -> a -> b
$ Name -> TypSch -> TypedPrimitive
TypedPrimitive (Var -> Name
Name Var
"hydra/lib/math.neg") (TypSch -> TypedPrimitive) -> TypSch -> TypedPrimitive
forall a b. (a -> b) -> a -> b
$ [Var] -> MTy -> TypSch
Forall [] (MTy -> TypSch) -> MTy -> TypSch
forall a b. (a -> b) -> a -> b
$ MTy -> MTy -> MTy
TyFn MTy
natType MTy
natType
-- Note: Hydra has no built-in pred or succ functions, but neg has the expected type
constPred :: Expr
constPred = Expr
constNeg
constSucc :: Expr
constSucc = Expr
constNeg
nat :: Int -> Expr
nat = Prim -> Expr
Const (Prim -> Expr) -> (Int -> Prim) -> Int -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Literal -> Prim
Lit (Literal -> Prim) -> (Int -> Literal) -> Int -> Prim
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Literal
int32
str :: Var -> Expr
str = Prim -> Expr
Const (Prim -> Expr) -> (Var -> Prim) -> Var -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Literal -> Prim
Lit (Literal -> Prim) -> (Var -> Literal) -> Var -> Prim
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Literal
string

-- A typed primitive corresponds to the Hydra primitive of the same name
data TypedPrimitive = TypedPrimitive Name TypSch deriving (TypedPrimitive -> TypedPrimitive -> Bool
(TypedPrimitive -> TypedPrimitive -> Bool)
-> (TypedPrimitive -> TypedPrimitive -> Bool) -> Eq TypedPrimitive
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TypedPrimitive -> TypedPrimitive -> Bool
== :: TypedPrimitive -> TypedPrimitive -> Bool
$c/= :: TypedPrimitive -> TypedPrimitive -> Bool
/= :: TypedPrimitive -> TypedPrimitive -> Bool
Eq)


------------------------
-- STLC

type Var = String

data Prim
 = Lit Literal
 | TypedPrim TypedPrimitive
 | If0
 | Fst | Snd | Pair | TT
 | Nil | Cons | FoldList
 | FF | Inl | Inr | Case | Con Var | Fold Var
 deriving Prim -> Prim -> Bool
(Prim -> Prim -> Bool) -> (Prim -> Prim -> Bool) -> Eq Prim
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Prim -> Prim -> Bool
== :: Prim -> Prim -> Bool
$c/= :: Prim -> Prim -> Bool
/= :: Prim -> Prim -> Bool
Eq

instance Show Prim where
  show :: Prim -> Var
show (Lit Literal
l) = Literal -> Var
forall a. Show a => a -> Var
show Literal
l
  show (TypedPrim (TypedPrimitive Name
name TypSch
_)) = Name -> Var
unName Name
name Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
"()"
  show Prim
FoldList = Var
"fold"
  show Prim
Fst = Var
"fst"
  show Prim
Snd = Var
"snd"
  show Prim
Nil = Var
"nil"
  show Prim
Cons = Var
"cons"
  show Prim
TT = Var
"tt"
  show Prim
FF = Var
"ff"
  show Prim
Inl = Var
"inl"
  show Prim
Inr = Var
"inr"
  show Prim
Case = Var
"case"
  show Prim
If0 = Var
"if0"
  show Prim
Pair = Var
"pair"
  show (Con  Var
n) = Var
n
  show (Fold Var
n) = Var
"fold_" Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
n

data Expr = Const Prim
 | Var Var
 | Tuple [Expr]
 | Proj Int Int Expr
 | Inj Int Int Expr
 | Case' Expr [Expr]
 | App Expr Expr
 | Abs Var Expr
 | Letrec [(Var, Expr)] Expr
 deriving (Expr -> Expr -> Bool
(Expr -> Expr -> Bool) -> (Expr -> Expr -> Bool) -> Eq Expr
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Expr -> Expr -> Bool
== :: Expr -> Expr -> Bool
$c/= :: Expr -> Expr -> Bool
/= :: Expr -> Expr -> Bool
Eq)

instance Show Expr where
  show :: Expr -> Var
show (Case' Expr
t [Expr]
ts) = Var
"case " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> Var
forall a. Show a => a -> Var
show Expr
t Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" of " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
x Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" end"
   where x :: Var
x = (Var -> ShowS) -> Var -> [Var] -> Var
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\Var
p Var
q -> Var
p Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
"\n\t\t" Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
q) Var
"" ([Var] -> Var) -> [Var] -> Var
forall a b. (a -> b) -> a -> b
$ (Expr -> Var) -> [Expr] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> Var
forall a. Show a => a -> Var
show [Expr]
ts
  show (Proj Int
i Int
j Expr
e) = Expr -> Var
forall a. Show a => a -> Var
show Expr
e Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
"." Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Var
forall a. Show a => a -> Var
show Int
i Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" (arity " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Var
forall a. Show a => a -> Var
show Int
j Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
")"
  show (Inj Int
i Int
j Expr
e) = Var
"inj " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Var
forall a. Show a => a -> Var
show Int
i Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" (arity " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Var
forall a. Show a => a -> Var
show Int
j Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
") " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> Var
forall a. Show a => a -> Var
show Expr
e
  show (Tuple [Expr]
ts) = Var
"<" Var -> ShowS
forall a. [a] -> [a] -> [a]
++ [Var] -> Var
forall a. Show a => a -> Var
show ((Expr -> Var) -> [Expr] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> Var
forall a. Show a => a -> Var
show [Expr]
ts) Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
">"
  show (Const Prim
p) = Prim -> Var
forall a. Show a => a -> Var
show Prim
p
  show (Var Var
v) = Var
v
  show (App (App (App Expr
a' Expr
a) Expr
b) Expr
b') = Var
"(" Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> Var
forall a. Show a => a -> Var
show Expr
a' Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> Var
forall a. Show a => a -> Var
show Expr
a Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> Var
forall a. Show a => a -> Var
show Expr
b Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> Var
forall a. Show a => a -> Var
show Expr
b' Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
")"
  show (App (App Expr
a Expr
b) Expr
b') = Var
"(" Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> Var
forall a. Show a => a -> Var
show Expr
a Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> Var
forall a. Show a => a -> Var
show Expr
b Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> Var
forall a. Show a => a -> Var
show Expr
b' Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
")"
  show (App Expr
a Expr
b) = Var
"(" Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> Var
forall a. Show a => a -> Var
show Expr
a Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> Var
forall a. Show a => a -> Var
show Expr
b Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
")"
  show (Abs Var
a Expr
b) = Var
"(\\" Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
a Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
". " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> Var
forall a. Show a => a -> Var
show Expr
b Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
")"
  show (Letrec [(Var, Expr)]
ab Expr
c) = Var
"letrec " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
d Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> Var
forall a. Show a => a -> Var
show Expr
c
    where d :: Var
d = ((Var, Expr) -> ShowS) -> Var -> [(Var, Expr)] -> Var
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Var
p, Expr
q) Var
r -> Var
p Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" = " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> Var
forall a. Show a => a -> Var
show Expr
q Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" \n\t\t" Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
r) Var
"in " [(Var, Expr)]
ab

data MTy = TyVar Var
  | TyLit LiteralType
  | TyList MTy
  | TyFn MTy MTy
  | TyProd MTy MTy
  | TySum MTy MTy
  | TyUnit
  | TyVoid
  | TyTuple [MTy]
  | TyVariant [MTy]
  | TyCon Var [MTy]
 deriving (MTy -> MTy -> Bool
(MTy -> MTy -> Bool) -> (MTy -> MTy -> Bool) -> Eq MTy
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MTy -> MTy -> Bool
== :: MTy -> MTy -> Bool
$c/= :: MTy -> MTy -> Bool
/= :: MTy -> MTy -> Bool
Eq)

instance Show MTy where
  show :: MTy -> Var
show (TyLit LiteralType
lt) = case LiteralType
lt of
    LiteralTypeInteger IntegerType
it -> Int -> ShowS
forall a. Int -> [a] -> [a]
drop (Var -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Var
"IntegerType") ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ IntegerType -> Var
forall a. Show a => a -> Var
show IntegerType
it
    LiteralTypeFloat FloatType
ft -> Int -> ShowS
forall a. Int -> [a] -> [a]
drop (Var -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Var
"FloatType") ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ FloatType -> Var
forall a. Show a => a -> Var
show FloatType
ft
    LiteralType
_ -> Int -> ShowS
forall a. Int -> [a] -> [a]
drop (Var -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Var
"LiteralType") ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ LiteralType -> Var
forall a. Show a => a -> Var
show LiteralType
lt
  show (TyTuple [MTy]
ts) = Var
"(Tuple " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ [Var] -> Var
forall a. Show a => a -> Var
show ((MTy -> Var) -> [MTy] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map MTy -> Var
forall a. Show a => a -> Var
show [MTy]
ts) Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
")"
  show (TyVariant [MTy]
ts) = Var
"(Variant " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ [Var] -> Var
forall a. Show a => a -> Var
show ((MTy -> Var) -> [MTy] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map MTy -> Var
forall a. Show a => a -> Var
show [MTy]
ts) Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
")"
  show (TyVar Var
v) = Var
v
  show (TyList MTy
t) = Var
"(List " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ (MTy -> Var
forall a. Show a => a -> Var
show MTy
t) Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
")"
  show (TyFn MTy
t1 MTy
t2) = Var
"(" Var -> ShowS
forall a. [a] -> [a] -> [a]
++ MTy -> Var
forall a. Show a => a -> Var
show MTy
t1 Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" -> " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ MTy -> Var
forall a. Show a => a -> Var
show MTy
t2 Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
")"
  show (TyProd MTy
t1 MTy
t2) = Var
"(" Var -> ShowS
forall a. [a] -> [a] -> [a]
++ MTy -> Var
forall a. Show a => a -> Var
show MTy
t1 Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" * " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ MTy -> Var
forall a. Show a => a -> Var
show MTy
t2 Var -> ShowS
forall a. [a] -> [a] -> [a]
++  Var
")"
  show (TySum MTy
t1 MTy
t2) = Var
"(" Var -> ShowS
forall a. [a] -> [a] -> [a]
++ MTy -> Var
forall a. Show a => a -> Var
show MTy
t1 Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" + " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ MTy -> Var
forall a. Show a => a -> Var
show MTy
t2 Var -> ShowS
forall a. [a] -> [a] -> [a]
++  Var
")"
  show MTy
TyUnit = Var
"Unit"
  show MTy
TyVoid = Var
"Void"
  show (TyCon Var
c [MTy]
ts) = Var
c Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
ts'
   where ts' :: Var
ts' = (MTy -> ShowS) -> Var -> [MTy] -> Var
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\MTy
p Var
r -> MTy -> Var
forall a. Show a => a -> Var
show MTy
p Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
"" Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
r) Var
"" [MTy]
ts

instance Show TypSch where
  show :: TypSch -> Var
show (Forall [] MTy
t) = MTy -> Var
forall a. Show a => a -> Var
show MTy
t
  show (Forall [Var]
x MTy
t) = Var
"forall " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
d Var -> ShowS
forall a. [a] -> [a] -> [a]
++ MTy -> Var
forall a. Show a => a -> Var
show MTy
t
   where d :: Var
d = (Var -> ShowS) -> Var -> [Var] -> Var
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Var
p Var
q ->  Var
p Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
q) Var
", " [Var]
x

data TypSch = Forall [Var] MTy
 deriving TypSch -> TypSch -> Bool
(TypSch -> TypSch -> Bool)
-> (TypSch -> TypSch -> Bool) -> Eq TypSch
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TypSch -> TypSch -> Bool
== :: TypSch -> TypSch -> Bool
$c/= :: TypSch -> TypSch -> Bool
/= :: TypSch -> TypSch -> Bool
Eq


type ADTs = [(Var, [Var], [(Var, [MTy])])]




------------------------
-- System F

data FExpr = FConst Prim
 | FVar Var
 | FTuple [FExpr]
 | FProj Int FExpr
 | FInj Int [FTy] FExpr
 | FCase FExpr FTy [FExpr]
 | FApp FExpr FExpr
 | FAbs Var FTy FExpr
 | FTyApp FExpr [FTy]
 | FTyAbs [Var] FExpr
 | FLetrec [(Var, FTy, FExpr)] FExpr
 deriving (FExpr -> FExpr -> Bool
(FExpr -> FExpr -> Bool) -> (FExpr -> FExpr -> Bool) -> Eq FExpr
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FExpr -> FExpr -> Bool
== :: FExpr -> FExpr -> Bool
$c/= :: FExpr -> FExpr -> Bool
/= :: FExpr -> FExpr -> Bool
Eq)

instance Show FExpr where
  show :: FExpr -> Var
show (FCase FExpr
t FTy
t' []) = Var
"ff " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FExpr -> Var
forall a. Show a => a -> Var
show FExpr
t Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FTy -> Var
forall a. Show a => a -> Var
show FTy
t' Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" "
  show (FCase FExpr
t FTy
t' [FExpr]
ts) = Var
"case " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FExpr -> Var
forall a. Show a => a -> Var
show FExpr
t Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" of " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ [Var] -> Var
forall a. Show a => a -> Var
show ((FExpr -> Var) -> [FExpr] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map FExpr -> Var
forall a. Show a => a -> Var
show [FExpr]
ts) Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" end"
  show (FProj Int
i FExpr
e) = FExpr -> Var
forall a. Show a => a -> Var
show FExpr
e Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
"." Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Var
forall a. Show a => a -> Var
show Int
i
  show (FInj Int
i [FTy]
j FExpr
e) = Var
"inj " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Var
forall a. Show a => a -> Var
show Int
i Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" (arity " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ [FTy] -> Var
forall a. Show a => a -> Var
show [FTy]
j Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
") " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FExpr -> Var
forall a. Show a => a -> Var
show FExpr
e
  show (FTuple [FExpr]
es) = Var
"<" Var -> ShowS
forall a. [a] -> [a] -> [a]
++ [Var] -> Var
forall a. Show a => a -> Var
show ((FExpr -> Var) -> [FExpr] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map FExpr -> Var
forall a. Show a => a -> Var
show [FExpr]
es) Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
">"
  show (FConst Prim
p) = Prim -> Var
forall a. Show a => a -> Var
show Prim
p
  show (FVar Var
v) = Var
v
  show (FTyApp FExpr
e [FTy]
t) = Var
"(" Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FExpr -> Var
forall a. Show a => a -> Var
show FExpr
e Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ [FTy] -> Var
forall a. Show a => a -> Var
show [FTy]
t Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
")"
  show (FApp (FApp (FApp FExpr
a' FExpr
a) FExpr
b) FExpr
b') = Var
"(" Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FExpr -> Var
forall a. Show a => a -> Var
show FExpr
a' Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FExpr -> Var
forall a. Show a => a -> Var
show FExpr
a Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FExpr -> Var
forall a. Show a => a -> Var
show FExpr
b Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FExpr -> Var
forall a. Show a => a -> Var
show FExpr
b' Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
")"
  show (FApp (FApp FExpr
a FExpr
b) FExpr
b') = Var
"(" Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FExpr -> Var
forall a. Show a => a -> Var
show FExpr
a Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FExpr -> Var
forall a. Show a => a -> Var
show FExpr
b Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FExpr -> Var
forall a. Show a => a -> Var
show FExpr
b' Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
")"
  show (FApp FExpr
a FExpr
b) = Var
"(" Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FExpr -> Var
forall a. Show a => a -> Var
show FExpr
a Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FExpr -> Var
forall a. Show a => a -> Var
show FExpr
b Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
")"
  show (FAbs Var
a FTy
t FExpr
b) = Var
"(\\" Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
a Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
":" Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FTy -> Var
forall a. Show a => a -> Var
show FTy
t Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
". " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FExpr -> Var
forall a. Show a => a -> Var
show FExpr
b Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
")"
  show (FLetrec [(Var, FTy, FExpr)]
ab FExpr
c) = Var
"letrecs " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
d Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FExpr -> Var
forall a. Show a => a -> Var
show FExpr
c
    where d :: Var
d = ((Var, FTy, FExpr) -> ShowS) -> Var -> [(Var, FTy, FExpr)] -> Var
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Var
p, FTy
t, FExpr
q) Var
r -> Var
p Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
":" Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FTy -> Var
forall a. Show a => a -> Var
show FTy
t Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" = " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FExpr -> Var
forall a. Show a => a -> Var
show FExpr
q Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" \n\t\t" Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
r) Var
"in " [(Var, FTy, FExpr)]
ab
  show (FTyAbs [Var]
ab FExpr
c) = Var
"(/\\" Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
d Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FExpr -> Var
forall a. Show a => a -> Var
show FExpr
c Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
")"
    where d :: Var
d = (Var -> ShowS) -> Var -> [Var] -> Var
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Var
p Var
r -> Var
p Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
r) Var
". " [Var]
ab

data FTy = FTyVar Var
  | FTyLit LiteralType
  | FTyList FTy
  | FTyFn FTy FTy
  | FTyProd FTy FTy
  | FTySum FTy FTy
  | FTyUnit
  | FTyVoid
  | FTyTuple [FTy]
  | FTyVariant [FTy]
  | FTyCon Var [FTy]
  | FForall [Var] FTy
 deriving (FTy -> FTy -> Bool
(FTy -> FTy -> Bool) -> (FTy -> FTy -> Bool) -> Eq FTy
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FTy -> FTy -> Bool
== :: FTy -> FTy -> Bool
$c/= :: FTy -> FTy -> Bool
/= :: FTy -> FTy -> Bool
Eq)

instance Show FTy where
  show :: FTy -> Var
show (FTyLit LiteralType
lt) = MTy -> Var
forall a. Show a => a -> Var
show (MTy -> Var) -> MTy -> Var
forall a b. (a -> b) -> a -> b
$ LiteralType -> MTy
TyLit LiteralType
lt
  show (FTyVariant [FTy]
ts) = Var
"(Variant " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ [Var] -> Var
forall a. Show a => a -> Var
show ((FTy -> Var) -> [FTy] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map FTy -> Var
forall a. Show a => a -> Var
show [FTy]
ts) Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
")"
  show (FTyTuple [FTy]
ts) = Var
"(Tuple " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ [Var] -> Var
forall a. Show a => a -> Var
show ((FTy -> Var) -> [FTy] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map FTy -> Var
forall a. Show a => a -> Var
show [FTy]
ts) Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
")"
  show (FTyVar Var
v) = Var
v
  show (FTyList FTy
t) = Var
"(List " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ (FTy -> Var
forall a. Show a => a -> Var
show FTy
t) Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
")"
  show (FTyFn FTy
t1 FTy
t2) = Var
"(" Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FTy -> Var
forall a. Show a => a -> Var
show FTy
t1 Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" -> " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FTy -> Var
forall a. Show a => a -> Var
show FTy
t2 Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
")"
  show (FTyProd FTy
t1 FTy
t2) = Var
"(" Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FTy -> Var
forall a. Show a => a -> Var
show FTy
t1 Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" * " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FTy -> Var
forall a. Show a => a -> Var
show FTy
t2 Var -> ShowS
forall a. [a] -> [a] -> [a]
++  Var
")"
  show (FTySum FTy
t1 FTy
t2) = Var
"(" Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FTy -> Var
forall a. Show a => a -> Var
show FTy
t1 Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" + " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FTy -> Var
forall a. Show a => a -> Var
show FTy
t2 Var -> ShowS
forall a. [a] -> [a] -> [a]
++  Var
")"
  show FTy
FTyUnit = Var
"Unit"
  show FTy
FTyVoid = Var
"Void"
  show (FForall [Var]
x FTy
t) = Var
"(forall " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
d Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FTy -> Var
forall a. Show a => a -> Var
show FTy
t Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
")"
   where d :: Var
d = (Var -> ShowS) -> Var -> [Var] -> Var
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Var
p Var
q -> Var
p Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
q) Var
", " [Var]
x
  show (FTyCon Var
c [FTy]
ts) = Var
c Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
ts'
   where ts' :: Var
ts' = (FTy -> ShowS) -> Var -> [FTy] -> Var
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\FTy
p Var
r -> FTy -> Var
forall a. Show a => a -> Var
show FTy
p Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
"" Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
r) Var
" " [FTy]
ts

mTyToFTy :: MTy -> FTy
mTyToFTy :: MTy -> FTy
mTyToFTy (TyVar Var
v) = Var -> FTy
FTyVar Var
v
mTyToFTy (TyLit LiteralType
lt) = LiteralType -> FTy
FTyLit LiteralType
lt
mTyToFTy MTy
TyUnit = FTy
FTyUnit
mTyToFTy MTy
TyVoid = FTy
FTyVoid
mTyToFTy (TyList MTy
x) = FTy -> FTy
FTyList (FTy -> FTy) -> FTy -> FTy
forall a b. (a -> b) -> a -> b
$ MTy -> FTy
mTyToFTy MTy
x
mTyToFTy (TyFn MTy
x MTy
y) = FTy -> FTy -> FTy
FTyFn (MTy -> FTy
mTyToFTy MTy
x) (MTy -> FTy
mTyToFTy MTy
y)
mTyToFTy (TyProd MTy
x MTy
y) = FTy -> FTy -> FTy
FTyProd (MTy -> FTy
mTyToFTy MTy
x) (MTy -> FTy
mTyToFTy MTy
y)
mTyToFTy (TySum MTy
x MTy
y) = FTy -> FTy -> FTy
FTySum (MTy -> FTy
mTyToFTy MTy
x) (MTy -> FTy
mTyToFTy MTy
y)
mTyToFTy (TyTuple [MTy]
ts) = [FTy] -> FTy
FTyTuple ((MTy -> FTy) -> [MTy] -> [FTy]
forall a b. (a -> b) -> [a] -> [b]
map MTy -> FTy
mTyToFTy [MTy]
ts)
mTyToFTy (TyVariant [MTy]
ts) = [FTy] -> FTy
FTyVariant ((MTy -> FTy) -> [MTy] -> [FTy]
forall a b. (a -> b) -> [a] -> [b]
map MTy -> FTy
mTyToFTy [MTy]
ts)
mTyToFTy (TyCon Var
c [MTy]
ts) = Var -> [FTy] -> FTy
FTyCon Var
c ([FTy] -> FTy) -> [FTy] -> FTy
forall a b. (a -> b) -> a -> b
$ (MTy -> FTy) -> [MTy] -> [FTy]
forall a b. (a -> b) -> [a] -> [b]
map MTy -> FTy
mTyToFTy [MTy]
ts

tyToFTy :: TypSch -> FTy
tyToFTy :: TypSch -> FTy
tyToFTy (Forall [] MTy
t) = MTy -> FTy
mTyToFTy MTy
t
tyToFTy (Forall [Var]
vs MTy
t) = [Var] -> FTy -> FTy
FForall [Var]
vs (MTy -> FTy
mTyToFTy MTy
t)

--------------------
-- Contexts

type Ctx = [(Var, TypSch)]

class Vars a where
  vars :: a -> [Var]

instance Vars Ctx where
 vars :: Ctx -> [Var]
vars [] = []
 vars ((Var
v,TypSch
t):Ctx
l) = TypSch -> [Var]
forall a. Vars a => a -> [Var]
vars TypSch
t [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ Ctx -> [Var]
forall a. Vars a => a -> [Var]
vars Ctx
l

instance Vars TypSch where
 vars :: TypSch -> [Var]
vars (Forall [Var]
vs MTy
t) = (Var -> Bool) -> [Var] -> [Var]
forall a. (a -> Bool) -> [a] -> [a]
filter (\Var
v -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Var -> [Var] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Var
v [Var]
vs) (MTy -> [Var]
forall a. Vars a => a -> [Var]
vars MTy
t)

instance Vars MTy where
 vars :: MTy -> [Var]
vars (TyVar Var
v) = [Var
v]
 vars (TyLit LiteralType
_) = []
 vars (TyList MTy
t) = MTy -> [Var]
forall a. Vars a => a -> [Var]
vars MTy
t
 vars (TyFn MTy
t1 MTy
t2) = MTy -> [Var]
forall a. Vars a => a -> [Var]
vars MTy
t1 [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ MTy -> [Var]
forall a. Vars a => a -> [Var]
vars MTy
t2
 vars MTy
TyUnit = []
 vars MTy
TyVoid = []
 vars (TyProd MTy
t1 MTy
t2) = MTy -> [Var]
forall a. Vars a => a -> [Var]
vars MTy
t1 [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ MTy -> [Var]
forall a. Vars a => a -> [Var]
vars MTy
t2
 vars (TySum MTy
t1 MTy
t2) = MTy -> [Var]
forall a. Vars a => a -> [Var]
vars MTy
t1 [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ MTy -> [Var]
forall a. Vars a => a -> [Var]
vars MTy
t2
 vars (TyTuple []) = []
 vars (TyTuple (MTy
a:[MTy]
b)) = MTy -> [Var]
forall a. Vars a => a -> [Var]
vars MTy
a [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ MTy -> [Var]
forall a. Vars a => a -> [Var]
vars ([MTy] -> MTy
TyTuple [MTy]
b)
 vars (TyVariant []) = []
 vars (TyVariant (MTy
a:[MTy]
b)) = MTy -> [Var]
forall a. Vars a => a -> [Var]
vars MTy
a [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ MTy -> [Var]
forall a. Vars a => a -> [Var]
vars ([MTy] -> MTy
TyVariant [MTy]
b)
 vars (TyCon Var
_ [MTy]
x) = MTy -> [Var]
forall a. Vars a => a -> [Var]
vars (MTy -> [Var]) -> MTy -> [Var]
forall a b. (a -> b) -> a -> b
$ [MTy] -> MTy
TyVariant [MTy]
x --cheat

replaceTCon :: MTy -> MTy -> MTy -> MTy
replaceTCon :: MTy -> MTy -> MTy -> MTy
replaceTCon MTy
u MTy
s (TyVar Var
x) = Var -> MTy
TyVar Var
x
replaceTCon MTy
u MTy
s (TyLit LiteralType
l) = LiteralType -> MTy
TyLit LiteralType
l
replaceTCon MTy
u MTy
s (TyList MTy
t)  = MTy -> MTy
TyList (MTy -> MTy) -> MTy -> MTy
forall a b. (a -> b) -> a -> b
$ MTy -> MTy -> MTy -> MTy
replaceTCon MTy
u MTy
s MTy
t
replaceTCon MTy
u MTy
s (TyFn MTy
t1 MTy
t2)  = MTy -> MTy -> MTy
TyFn (MTy -> MTy -> MTy -> MTy
replaceTCon MTy
u MTy
s MTy
t1) (MTy -> MTy -> MTy -> MTy
replaceTCon MTy
u MTy
s MTy
t2)
replaceTCon MTy
u MTy
s MTy
TyUnit  = MTy
TyUnit
replaceTCon MTy
u MTy
s MTy
TyVoid  = MTy
TyVoid
replaceTCon MTy
u MTy
s (TyProd MTy
t1 MTy
t2)  = MTy -> MTy -> MTy
TyProd (MTy -> MTy -> MTy -> MTy
replaceTCon MTy
u MTy
s MTy
t1) (MTy -> MTy -> MTy -> MTy
replaceTCon MTy
u MTy
s MTy
t2)
replaceTCon MTy
u MTy
s (TySum MTy
t1 MTy
t2)  = MTy -> MTy -> MTy
TySum (MTy -> MTy -> MTy -> MTy
replaceTCon MTy
u MTy
s MTy
t1) (MTy -> MTy -> MTy -> MTy
replaceTCon MTy
u MTy
s MTy
t2)
replaceTCon MTy
u MTy
s (TyTuple [])  = [MTy] -> MTy
TyTuple []
replaceTCon MTy
u MTy
s (TyTuple (MTy
a:[MTy]
b)) = [MTy] -> MTy
TyTuple ([MTy] -> MTy) -> [MTy] -> MTy
forall a b. (a -> b) -> a -> b
$ (MTy -> MTy -> MTy -> MTy
replaceTCon MTy
u MTy
s MTy
a)MTy -> [MTy] -> [MTy]
forall a. a -> [a] -> [a]
:((MTy -> MTy) -> [MTy] -> [MTy]
forall a b. (a -> b) -> [a] -> [b]
map (MTy -> MTy -> MTy -> MTy
replaceTCon MTy
u MTy
s) [MTy]
b)
replaceTCon MTy
u MTy
s (TyVariant [])  = [MTy] -> MTy
TyVariant []
replaceTCon MTy
u MTy
s (TyVariant (MTy
a:[MTy]
b)) = [MTy] -> MTy
TyVariant ([MTy] -> MTy) -> [MTy] -> MTy
forall a b. (a -> b) -> a -> b
$ (MTy -> MTy -> MTy -> MTy
replaceTCon MTy
u MTy
s MTy
a)MTy -> [MTy] -> [MTy]
forall a. a -> [a] -> [a]
:((MTy -> MTy) -> [MTy] -> [MTy]
forall a b. (a -> b) -> [a] -> [b]
map (MTy -> MTy -> MTy -> MTy
replaceTCon MTy
u MTy
s) [MTy]
b)
replaceTCon MTy
u MTy
s (TyCon Var
t' [MTy]
ts)  | Var -> [MTy] -> MTy
TyCon Var
t' [MTy]
ts MTy -> MTy -> Bool
forall a. Eq a => a -> a -> Bool
== MTy
u = MTy
s
                               | Bool
otherwise = Var -> [MTy] -> MTy
TyCon Var
t' ([MTy] -> MTy) -> [MTy] -> MTy
forall a b. (a -> b) -> a -> b
$ (MTy -> MTy) -> [MTy] -> [MTy]
forall a b. (a -> b) -> [a] -> [b]
map (MTy -> MTy -> MTy -> MTy
replaceTCon MTy
u MTy
s) [MTy]
ts

primTy :: ADTs -> Prim -> Either String TypSch
primTy :: ADTs -> Prim -> Either Var TypSch
primTy ADTs
_ (Lit Literal
l) = TypSch -> Either Var TypSch
forall a b. b -> Either a b
Right (TypSch -> Either Var TypSch) -> TypSch -> Either Var TypSch
forall a b. (a -> b) -> a -> b
$ [Var] -> MTy -> TypSch
Forall [] (MTy -> TypSch) -> MTy -> TypSch
forall a b. (a -> b) -> a -> b
$ LiteralType -> MTy
TyLit (LiteralType -> MTy) -> LiteralType -> MTy
forall a b. (a -> b) -> a -> b
$ Literal -> LiteralType
literalType Literal
l
primTy ADTs
_ (TypedPrim (TypedPrimitive Name
_ TypSch
forall)) = TypSch -> Either Var TypSch
forall a b. b -> Either a b
Right TypSch
forall
primTy [] (Con Var
n) = Var -> Either Var TypSch
forall a. Var -> Either Var a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Var -> Either Var TypSch) -> Var -> Either Var TypSch
forall a b. (a -> b) -> a -> b
$ Var
n Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" not found "
primTy ((Var
a,[Var]
t,[]):ADTs
tl) (Con Var
n) = ADTs -> Prim -> Either Var TypSch
primTy ADTs
tl (Prim -> Either Var TypSch) -> Prim -> Either Var TypSch
forall a b. (a -> b) -> a -> b
$ Var -> Prim
Con Var
n
primTy ((Var
a,[Var]
t,(Var
c,[MTy]
ts):[(Var, [MTy])]
cs):ADTs
tl) (Con Var
n) | Var
c Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
n = TypSch -> Either Var TypSch
forall a. a -> Either Var a
forall (m :: * -> *) a. Monad m => a -> m a
return (TypSch -> Either Var TypSch) -> TypSch -> Either Var TypSch
forall a b. (a -> b) -> a -> b
$ [Var] -> MTy -> TypSch
Forall [Var]
t ([MTy] -> MTy -> MTy
ts' [MTy]
ts (MTy -> MTy) -> MTy -> MTy
forall a b. (a -> b) -> a -> b
$ Var -> [MTy] -> MTy
TyCon Var
a ([MTy] -> MTy) -> [MTy] -> MTy
forall a b. (a -> b) -> a -> b
$ (Var -> MTy) -> [Var] -> [MTy]
forall a b. (a -> b) -> [a] -> [b]
map Var -> MTy
TyVar [Var]
t)
                                    | Bool
otherwise = ADTs -> Prim -> Either Var TypSch
primTy ((Var
a,[Var]
t,[(Var, [MTy])]
cs)(Var, [Var], [(Var, [MTy])]) -> ADTs -> ADTs
forall a. a -> [a] -> [a]
:ADTs
tl) (Prim -> Either Var TypSch) -> Prim -> Either Var TypSch
forall a b. (a -> b) -> a -> b
$ Var -> Prim
Con Var
n
 where ts' :: [MTy] -> MTy -> MTy
ts' [] MTy
x = MTy
x
       ts' (MTy
p:[MTy]
q) MTy
x = MTy -> MTy -> MTy
TyFn MTy
p (MTy -> MTy) -> MTy -> MTy
forall a b. (a -> b) -> a -> b
$ [MTy] -> MTy -> MTy
ts' [MTy]
q MTy
x
primTy [] (Fold Var
n) = Var -> Either Var TypSch
forall a. Var -> Either Var a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Var -> Either Var TypSch) -> Var -> Either Var TypSch
forall a b. (a -> b) -> a -> b
$ Var
n Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" not found "
primTy ((Var
a,[Var]
t,[(Var, [MTy])]
cs):ADTs
tl) (Fold Var
n) | Var
a Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
n = TypSch -> Either Var TypSch
forall a. a -> Either Var a
forall (m :: * -> *) a. Monad m => a -> m a
return (TypSch -> Either Var TypSch) -> TypSch -> Either Var TypSch
forall a b. (a -> b) -> a -> b
$ [Var] -> MTy -> TypSch
Forall (Var
"r"Var -> [Var] -> [Var]
forall a. a -> [a] -> [a]
:[Var]
t) (MTy -> TypSch) -> MTy -> TypSch
forall a b. (a -> b) -> a -> b
$ MTy
elimTy
                              | Bool
otherwise = ADTs -> Prim -> Either Var TypSch
primTy ADTs
tl (Prim -> Either Var TypSch) -> Prim -> Either Var TypSch
forall a b. (a -> b) -> a -> b
$ Var -> Prim
Fold Var
n
 where elimTy :: MTy
elimTy = MTy -> MTy -> MTy
TyFn (Var -> [MTy] -> MTy
TyCon Var
a ([MTy] -> MTy) -> [MTy] -> MTy
forall a b. (a -> b) -> a -> b
$ (Var -> MTy) -> [Var] -> [MTy]
forall a b. (a -> b) -> [a] -> [b]
map Var -> MTy
TyVar [Var]
t) (MTy -> MTy) -> MTy -> MTy
forall a b. (a -> b) -> a -> b
$ MTy -> MTy -> MTy -> MTy
replaceTCon (Var -> [MTy] -> MTy
TyCon Var
a ([MTy] -> MTy) -> [MTy] -> MTy
forall a b. (a -> b) -> a -> b
$ (Var -> MTy) -> [Var] -> [MTy]
forall a b. (a -> b) -> [a] -> [b]
map Var -> MTy
TyVar [Var]
t) (Var -> MTy
TyVar Var
"r") ([(Var, [MTy])] -> MTy
forall {a}. [(a, [MTy])] -> MTy
ts' [(Var, [MTy])]
cs)
       ts' :: [(a, [MTy])] -> MTy
ts' [] = Var -> MTy
TyVar Var
"r"
       ts' ((a
_,[MTy]
ts):[(a, [MTy])]
q)  = MTy -> MTy -> MTy
TyFn ([MTy] -> MTy
ts'' [MTy]
ts) (MTy -> MTy) -> MTy -> MTy
forall a b. (a -> b) -> a -> b
$ [(a, [MTy])] -> MTy
ts' [(a, [MTy])]
q
       ts'' :: [MTy] -> MTy
ts'' [] = Var -> [MTy] -> MTy
TyCon Var
a ([MTy] -> MTy) -> [MTy] -> MTy
forall a b. (a -> b) -> a -> b
$ (Var -> MTy) -> [Var] -> [MTy]
forall a b. (a -> b) -> [a] -> [b]
map Var -> MTy
TyVar [Var]
t
       ts'' (MTy
a:[MTy]
b) = MTy -> MTy -> MTy
TyFn MTy
a (MTy -> MTy) -> MTy -> MTy
forall a b. (a -> b) -> a -> b
$ [MTy] -> MTy
ts'' [MTy]
b
primTy ADTs
_ Prim
Fst = TypSch -> Either Var TypSch
forall a. a -> Either Var a
forall (m :: * -> *) a. Monad m => a -> m a
return (TypSch -> Either Var TypSch) -> TypSch -> Either Var TypSch
forall a b. (a -> b) -> a -> b
$  [Var] -> MTy -> TypSch
Forall [Var
"x", Var
"y"] (MTy -> TypSch) -> MTy -> TypSch
forall a b. (a -> b) -> a -> b
$ (MTy -> MTy -> MTy
TyProd (Var -> MTy
TyVar Var
"x") (Var -> MTy
TyVar Var
"y")) MTy -> MTy -> MTy
`TyFn` (Var -> MTy
TyVar Var
"x")
primTy ADTs
_ Prim
Snd = TypSch -> Either Var TypSch
forall a. a -> Either Var a
forall (m :: * -> *) a. Monad m => a -> m a
return (TypSch -> Either Var TypSch) -> TypSch -> Either Var TypSch
forall a b. (a -> b) -> a -> b
$  [Var] -> MTy -> TypSch
Forall [Var
"x", Var
"y"] (MTy -> TypSch) -> MTy -> TypSch
forall a b. (a -> b) -> a -> b
$ (MTy -> MTy -> MTy
TyProd (Var -> MTy
TyVar Var
"x") (Var -> MTy
TyVar Var
"y")) MTy -> MTy -> MTy
`TyFn` (Var -> MTy
TyVar Var
"y")
primTy ADTs
_ Prim
Nil = TypSch -> Either Var TypSch
forall a. a -> Either Var a
forall (m :: * -> *) a. Monad m => a -> m a
return (TypSch -> Either Var TypSch) -> TypSch -> Either Var TypSch
forall a b. (a -> b) -> a -> b
$  [Var] -> MTy -> TypSch
Forall [Var
"t"] (MTy -> TypSch) -> MTy -> TypSch
forall a b. (a -> b) -> a -> b
$ MTy -> MTy
TyList (Var -> MTy
TyVar Var
"t")
primTy ADTs
_ Prim
Cons = TypSch -> Either Var TypSch
forall a. a -> Either Var a
forall (m :: * -> *) a. Monad m => a -> m a
return (TypSch -> Either Var TypSch) -> TypSch -> Either Var TypSch
forall a b. (a -> b) -> a -> b
$ [Var] -> MTy -> TypSch
Forall [Var
"t"] (MTy -> TypSch) -> MTy -> TypSch
forall a b. (a -> b) -> a -> b
$ MTy -> MTy -> MTy
TyFn (Var -> MTy
TyVar Var
"t") (MTy -> MTy -> MTy
TyFn (MTy -> MTy
TyList (Var -> MTy
TyVar Var
"t")) (MTy -> MTy
TyList (Var -> MTy
TyVar Var
"t")))
primTy ADTs
_ Prim
TT = TypSch -> Either Var TypSch
forall a. a -> Either Var a
forall (m :: * -> *) a. Monad m => a -> m a
return (TypSch -> Either Var TypSch) -> TypSch -> Either Var TypSch
forall a b. (a -> b) -> a -> b
$ [Var] -> MTy -> TypSch
Forall [] MTy
TyUnit
primTy ADTs
_ Prim
FF = TypSch -> Either Var TypSch
forall a. a -> Either Var a
forall (m :: * -> *) a. Monad m => a -> m a
return (TypSch -> Either Var TypSch) -> TypSch -> Either Var TypSch
forall a b. (a -> b) -> a -> b
$ [Var] -> MTy -> TypSch
Forall [Var
"t"] (MTy -> TypSch) -> MTy -> TypSch
forall a b. (a -> b) -> a -> b
$ MTy -> MTy -> MTy
TyFn MTy
TyVoid (Var -> MTy
TyVar Var
"t")
primTy ADTs
_ Prim
Inl = TypSch -> Either Var TypSch
forall a. a -> Either Var a
forall (m :: * -> *) a. Monad m => a -> m a
return (TypSch -> Either Var TypSch) -> TypSch -> Either Var TypSch
forall a b. (a -> b) -> a -> b
$ [Var] -> MTy -> TypSch
Forall [Var
"x", Var
"y"] (MTy -> TypSch) -> MTy -> TypSch
forall a b. (a -> b) -> a -> b
$ (Var -> MTy
TyVar Var
"x") MTy -> MTy -> MTy
`TyFn` (MTy -> MTy -> MTy
TyProd (Var -> MTy
TyVar Var
"x") (Var -> MTy
TyVar Var
"y"))
primTy ADTs
_ Prim
Inr = TypSch -> Either Var TypSch
forall a. a -> Either Var a
forall (m :: * -> *) a. Monad m => a -> m a
return (TypSch -> Either Var TypSch) -> TypSch -> Either Var TypSch
forall a b. (a -> b) -> a -> b
$ [Var] -> MTy -> TypSch
Forall [Var
"x", Var
"y"] (MTy -> TypSch) -> MTy -> TypSch
forall a b. (a -> b) -> a -> b
$ (Var -> MTy
TyVar Var
"y") MTy -> MTy -> MTy
`TyFn` (MTy -> MTy -> MTy
TyProd (Var -> MTy
TyVar Var
"x") (Var -> MTy
TyVar Var
"y"))
primTy ADTs
_ Prim
Pair = TypSch -> Either Var TypSch
forall a. a -> Either Var a
forall (m :: * -> *) a. Monad m => a -> m a
return (TypSch -> Either Var TypSch) -> TypSch -> Either Var TypSch
forall a b. (a -> b) -> a -> b
$ [Var] -> MTy -> TypSch
Forall [Var
"xx", Var
"yy"] (MTy -> TypSch) -> MTy -> TypSch
forall a b. (a -> b) -> a -> b
$ (MTy -> MTy -> MTy
TyFn (Var -> MTy
TyVar Var
"xx") (MTy -> MTy -> MTy
TyFn (Var -> MTy
TyVar Var
"yy") (MTy -> MTy -> MTy
TyProd (Var -> MTy
TyVar Var
"xx") (Var -> MTy
TyVar Var
"yy"))))
primTy ADTs
_ Prim
If0 = TypSch -> Either Var TypSch
forall a. a -> Either Var a
forall (m :: * -> *) a. Monad m => a -> m a
return (TypSch -> Either Var TypSch) -> TypSch -> Either Var TypSch
forall a b. (a -> b) -> a -> b
$ [Var] -> MTy -> TypSch
Forall [] (MTy -> TypSch) -> MTy -> TypSch
forall a b. (a -> b) -> a -> b
$ MTy
natType MTy -> MTy -> MTy
`TyFn` (MTy
natType MTy -> MTy -> MTy
`TyFn` (MTy
natType MTy -> MTy -> MTy
`TyFn` MTy
natType))
primTy ADTs
_ Prim
FoldList = TypSch -> Either Var TypSch
forall a. a -> Either Var a
forall (m :: * -> *) a. Monad m => a -> m a
return (TypSch -> Either Var TypSch) -> TypSch -> Either Var TypSch
forall a b. (a -> b) -> a -> b
$ [Var] -> MTy -> TypSch
Forall [Var
"a", Var
"b"] (MTy -> TypSch) -> MTy -> TypSch
forall a b. (a -> b) -> a -> b
$ MTy
p MTy -> MTy -> MTy
`TyFn` ((Var -> MTy
TyVar Var
"b") MTy -> MTy -> MTy
`TyFn` ((MTy -> MTy
TyList (MTy -> MTy) -> MTy -> MTy
forall a b. (a -> b) -> a -> b
$ Var -> MTy
TyVar Var
"a") MTy -> MTy -> MTy
`TyFn` (Var -> MTy
TyVar Var
"b")))
 where p :: MTy
p = Var -> MTy
TyVar Var
"b" MTy -> MTy -> MTy
`TyFn` (Var -> MTy
TyVar Var
"a" MTy -> MTy -> MTy
`TyFn` Var -> MTy
TyVar Var
"b")
primTy ADTs
_ Prim
Case = TypSch -> Either Var TypSch
forall a. a -> Either Var a
forall (m :: * -> *) a. Monad m => a -> m a
return (TypSch -> Either Var TypSch) -> TypSch -> Either Var TypSch
forall a b. (a -> b) -> a -> b
$ [Var] -> MTy -> TypSch
Forall [Var
"x", Var
"y", Var
"z"] (MTy -> TypSch) -> MTy -> TypSch
forall a b. (a -> b) -> a -> b
$ (MTy -> MTy -> MTy
TySum (Var -> MTy
TyVar Var
"x") (Var -> MTy
TyVar Var
"y")) MTy -> MTy -> MTy
`TyFn` (MTy
l MTy -> MTy -> MTy
`TyFn` (MTy
r MTy -> MTy -> MTy
`TyFn` (Var -> MTy
TyVar Var
"z")))
 where l :: MTy
l = (Var -> MTy
TyVar Var
"x") MTy -> MTy -> MTy
`TyFn` (Var -> MTy
TyVar Var
"z")
       r :: MTy
r = (Var -> MTy
TyVar Var
"y") MTy -> MTy -> MTy
`TyFn` (Var -> MTy
TyVar Var
"z")


-----------------------------
-- Substitution

type Subst = [(Var, MTy)]

idSubst :: Subst
idSubst :: Subst
idSubst = []

o :: Subst -> Subst -> Subst
o :: Subst -> Subst -> Subst
o Subst
f Subst
g = Subst
addExtra Subst -> Subst -> Subst
forall a. [a] -> [a] -> [a]
++ ((Var, MTy) -> (Var, MTy)) -> Subst -> Subst
forall a b. (a -> b) -> [a] -> [b]
map (Var, MTy) -> (Var, MTy)
forall {b} {a}. Substable b => (a, b) -> (a, b)
h Subst
g
 where h :: (a, b) -> (a, b)
h (a
v, b
g') = (a
v, Subst -> b -> b
forall a. Substable a => Subst -> a -> a
subst Subst
f b
g')
       addExtra :: Subst
addExtra = ((Var, MTy) -> Bool) -> Subst -> Subst
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Var
v,MTy
f')-> case Var -> Subst -> Maybe MTy
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Var
v Subst
g of
                                      Just MTy
y  -> Bool
False
                                      Maybe MTy
Nothing -> Bool
True) Subst
f

class Substable a where
  subst :: Subst -> a -> a

instance Substable MTy where
 subst :: Subst -> MTy -> MTy
subst Subst
f (TyLit LiteralType
lt) = LiteralType -> MTy
TyLit LiteralType
lt
 subst Subst
f (TyVariant [MTy]
ts) = [MTy] -> MTy
TyVariant ([MTy] -> MTy) -> [MTy] -> MTy
forall a b. (a -> b) -> a -> b
$ (MTy -> MTy) -> [MTy] -> [MTy]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> MTy -> MTy
forall a. Substable a => Subst -> a -> a
subst Subst
f) [MTy]
ts
 subst Subst
f (TyTuple [MTy]
ts) = [MTy] -> MTy
TyTuple ([MTy] -> MTy) -> [MTy] -> MTy
forall a b. (a -> b) -> a -> b
$ (MTy -> MTy) -> [MTy] -> [MTy]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> MTy -> MTy
forall a. Substable a => Subst -> a -> a
subst Subst
f) [MTy]
ts
 subst Subst
f MTy
TyUnit = MTy
TyUnit
 subst Subst
f MTy
TyVoid = MTy
TyVoid
 subst Subst
f (TyList MTy
t) = MTy -> MTy
TyList (MTy -> MTy) -> MTy -> MTy
forall a b. (a -> b) -> a -> b
$ Subst -> MTy -> MTy
forall a. Substable a => Subst -> a -> a
subst Subst
f MTy
t
 subst Subst
f (TyFn MTy
t1 MTy
t2) = MTy -> MTy -> MTy
TyFn (Subst -> MTy -> MTy
forall a. Substable a => Subst -> a -> a
subst Subst
f MTy
t1) (Subst -> MTy -> MTy
forall a. Substable a => Subst -> a -> a
subst Subst
f MTy
t2)
 subst Subst
f (TyProd MTy
t1 MTy
t2) = MTy -> MTy -> MTy
TyProd  (Subst -> MTy -> MTy
forall a. Substable a => Subst -> a -> a
subst Subst
f MTy
t1) (Subst -> MTy -> MTy
forall a. Substable a => Subst -> a -> a
subst Subst
f MTy
t2)
 subst Subst
f (TySum MTy
t1 MTy
t2) = MTy -> MTy -> MTy
TySum  (Subst -> MTy -> MTy
forall a. Substable a => Subst -> a -> a
subst Subst
f MTy
t1) (Subst -> MTy -> MTy
forall a. Substable a => Subst -> a -> a
subst Subst
f MTy
t2)
 subst Subst
f (TyVar Var
v) = case Var -> Subst -> Maybe MTy
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Var
v Subst
f of
                      Maybe MTy
Nothing -> Var -> MTy
TyVar Var
v
                      Just MTy
y -> MTy
y
 subst Subst
f (TyCon Var
v [MTy]
ts) = Var -> [MTy] -> MTy
TyCon Var
v ([MTy] -> MTy) -> [MTy] -> MTy
forall a b. (a -> b) -> a -> b
$ (MTy -> MTy) -> [MTy] -> [MTy]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> MTy -> MTy
forall a. Substable a => Subst -> a -> a
subst Subst
f) [MTy]
ts

instance Substable FTy where
 subst :: Subst -> FTy -> FTy
subst Subst
f (FTyLit LiteralType
lt) = LiteralType -> FTy
FTyLit LiteralType
lt
 subst Subst
f (FTyVariant [FTy]
ts) = [FTy] -> FTy
FTyVariant ([FTy] -> FTy) -> [FTy] -> FTy
forall a b. (a -> b) -> a -> b
$ (FTy -> FTy) -> [FTy] -> [FTy]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> FTy -> FTy
forall a. Substable a => Subst -> a -> a
subst Subst
f) [FTy]
ts
 subst Subst
f (FTyTuple [FTy]
ts) = [FTy] -> FTy
FTyTuple ([FTy] -> FTy) -> [FTy] -> FTy
forall a b. (a -> b) -> a -> b
$ (FTy -> FTy) -> [FTy] -> [FTy]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> FTy -> FTy
forall a. Substable a => Subst -> a -> a
subst Subst
f) [FTy]
ts
 subst Subst
f FTy
FTyUnit = FTy
FTyUnit
 subst Subst
f FTy
FTyVoid = FTy
FTyVoid
 subst Subst
f (FTyList FTy
t) = FTy -> FTy
FTyList (FTy -> FTy) -> FTy -> FTy
forall a b. (a -> b) -> a -> b
$ Subst -> FTy -> FTy
forall a. Substable a => Subst -> a -> a
subst Subst
f FTy
t
 subst Subst
f (FTyFn FTy
t1 FTy
t2) = FTy -> FTy -> FTy
FTyFn (Subst -> FTy -> FTy
forall a. Substable a => Subst -> a -> a
subst Subst
f FTy
t1) (Subst -> FTy -> FTy
forall a. Substable a => Subst -> a -> a
subst Subst
f FTy
t2)
 subst Subst
f (FTyProd FTy
t1 FTy
t2) = FTy -> FTy -> FTy
FTyProd  (Subst -> FTy -> FTy
forall a. Substable a => Subst -> a -> a
subst Subst
f FTy
t1) (Subst -> FTy -> FTy
forall a. Substable a => Subst -> a -> a
subst Subst
f FTy
t2)
 subst Subst
f (FTySum FTy
t1 FTy
t2) = FTy -> FTy -> FTy
FTySum  (Subst -> FTy -> FTy
forall a. Substable a => Subst -> a -> a
subst Subst
f FTy
t1) (Subst -> FTy -> FTy
forall a. Substable a => Subst -> a -> a
subst Subst
f FTy
t2)
 subst Subst
f (FTyVar Var
v) = case Var -> Subst -> Maybe MTy
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Var
v Subst
f of
                        Maybe MTy
Nothing -> Var -> FTy
FTyVar Var
v
                        Just MTy
y -> MTy -> FTy
mTyToFTy MTy
y
 subst Subst
f (FForall [Var]
vs FTy
t) = [Var] -> FTy -> FTy
FForall [Var]
vs (FTy -> FTy) -> FTy -> FTy
forall a b. (a -> b) -> a -> b
$ Subst -> FTy -> FTy
forall a. Substable a => Subst -> a -> a
subst Subst
phi' FTy
t
  where phi' :: Subst
phi' = ((Var, MTy) -> Bool) -> Subst -> Subst
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Var
v,MTy
f')-> Bool -> Bool
not (Var -> [Var] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Var
v [Var]
vs)) Subst
f
 subst Subst
f (FTyCon Var
v [FTy]
ts) = Var -> [FTy] -> FTy
FTyCon Var
v ([FTy] -> FTy) -> [FTy] -> FTy
forall a b. (a -> b) -> a -> b
$ (FTy -> FTy) -> [FTy] -> [FTy]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> FTy -> FTy
forall a. Substable a => Subst -> a -> a
subst Subst
f) [FTy]
ts

instance Substable TypSch where
 subst :: Subst -> TypSch -> TypSch
subst Subst
f (Forall [Var]
vs MTy
t) = [Var] -> MTy -> TypSch
Forall [Var]
vs (MTy -> TypSch) -> MTy -> TypSch
forall a b. (a -> b) -> a -> b
$ Subst -> MTy -> MTy
forall a. Substable a => Subst -> a -> a
subst Subst
f' MTy
t
   where f' :: Subst
f' = ((Var, MTy) -> Bool) -> Subst -> Subst
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Var
v,MTy
t')-> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Var -> [Var] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Var
v [Var]
vs) Subst
f

instance Substable Ctx where
 subst :: Subst -> Ctx -> Ctx
subst Subst
phi Ctx
g = ((Var, TypSch) -> (Var, TypSch)) -> Ctx -> Ctx
forall a b. (a -> b) -> [a] -> [b]
map (\(Var
k,TypSch
v)->(Var
k, Subst -> TypSch -> TypSch
forall a. Substable a => Subst -> a -> a
subst Subst
phi TypSch
v)) Ctx
g

instance Substable FExpr where
 subst :: Subst -> FExpr -> FExpr
subst Subst
phi (FInj Int
i [FTy]
js FExpr
e) = Int -> [FTy] -> FExpr -> FExpr
FInj Int
i ((FTy -> FTy) -> [FTy] -> [FTy]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> FTy -> FTy
forall a. Substable a => Subst -> a -> a
subst Subst
phi) [FTy]
js) (FExpr -> FExpr) -> FExpr -> FExpr
forall a b. (a -> b) -> a -> b
$ Subst -> FExpr -> FExpr
forall a. Substable a => Subst -> a -> a
subst Subst
phi FExpr
e
 subst Subst
phi (FProj Int
i FExpr
e) = Int -> FExpr -> FExpr
FProj Int
i (FExpr -> FExpr) -> FExpr -> FExpr
forall a b. (a -> b) -> a -> b
$ Subst -> FExpr -> FExpr
forall a. Substable a => Subst -> a -> a
subst Subst
phi FExpr
e
 subst Subst
phi (FTuple [FExpr]
es) = [FExpr] -> FExpr
FTuple ([FExpr] -> FExpr) -> [FExpr] -> FExpr
forall a b. (a -> b) -> a -> b
$ (FExpr -> FExpr) -> [FExpr] -> [FExpr]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> FExpr -> FExpr
forall a. Substable a => Subst -> a -> a
subst Subst
phi) [FExpr]
es
 subst Subst
phi (FCase FExpr
e FTy
t [FExpr]
es) = FExpr -> FTy -> [FExpr] -> FExpr
FCase (Subst -> FExpr -> FExpr
forall a. Substable a => Subst -> a -> a
subst Subst
phi FExpr
e) (Subst -> FTy -> FTy
forall a. Substable a => Subst -> a -> a
subst Subst
phi FTy
t) ([FExpr] -> FExpr) -> [FExpr] -> FExpr
forall a b. (a -> b) -> a -> b
$ (FExpr -> FExpr) -> [FExpr] -> [FExpr]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> FExpr -> FExpr
forall a. Substable a => Subst -> a -> a
subst Subst
phi) [FExpr]
es
 subst Subst
phi (FConst Prim
p) = Prim -> FExpr
FConst Prim
p
 subst Subst
phi (FVar Var
p) = Var -> FExpr
FVar Var
p
 subst Subst
phi (FApp FExpr
p FExpr
q) = FExpr -> FExpr -> FExpr
FApp (Subst -> FExpr -> FExpr
forall a. Substable a => Subst -> a -> a
subst Subst
phi FExpr
p) (Subst -> FExpr -> FExpr
forall a. Substable a => Subst -> a -> a
subst Subst
phi FExpr
q)
 subst Subst
phi (FAbs Var
p FTy
t FExpr
q) = Var -> FTy -> FExpr -> FExpr
FAbs Var
p (Subst -> FTy -> FTy
forall a. Substable a => Subst -> a -> a
subst Subst
phi FTy
t) (Subst -> FExpr -> FExpr
forall a. Substable a => Subst -> a -> a
subst Subst
phi FExpr
q)
 subst Subst
phi (FTyApp FExpr
p [FTy]
q) = FExpr -> [FTy] -> FExpr
FTyApp (Subst -> FExpr -> FExpr
forall a. Substable a => Subst -> a -> a
subst Subst
phi FExpr
p) ((FTy -> FTy) -> [FTy] -> [FTy]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> FTy -> FTy
forall a. Substable a => Subst -> a -> a
subst Subst
phi) [FTy]
q)
 subst Subst
phi (FTyAbs [Var]
vs FExpr
p) = [Var] -> FExpr -> FExpr
FTyAbs [Var]
vs (Subst -> FExpr -> FExpr
forall a. Substable a => Subst -> a -> a
subst Subst
phi' FExpr
p)
  where phi' :: Subst
phi' = ((Var, MTy) -> Bool) -> Subst -> Subst
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Var
v,MTy
f')-> Bool -> Bool
not (Var -> [Var] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Var
v [Var]
vs)) Subst
phi
 subst Subst
phi (FLetrec [(Var, FTy, FExpr)]
vs FExpr
p) = [(Var, FTy, FExpr)] -> FExpr -> FExpr
FLetrec (((Var, FTy, FExpr) -> (Var, FTy, FExpr))
-> [(Var, FTy, FExpr)] -> [(Var, FTy, FExpr)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Var
k,FTy
t,FExpr
v)->(Var
k,Subst -> FTy -> FTy
forall a. Substable a => Subst -> a -> a
subst Subst
phi FTy
t, Subst -> FExpr -> FExpr
forall a. Substable a => Subst -> a -> a
subst Subst
phi FExpr
v)) [(Var, FTy, FExpr)]
vs) (Subst -> FExpr -> FExpr
forall a. Substable a => Subst -> a -> a
subst Subst
phi FExpr
p)

subst' :: [(Var,FTy)] -> FTy -> FTy
subst' :: [(Var, FTy)] -> FTy -> FTy
subst' [(Var, FTy)]
f (FTyLit LiteralType
lt) = LiteralType -> FTy
FTyLit LiteralType
lt
subst' [(Var, FTy)]
f (FTyTuple [FTy]
ts) = [FTy] -> FTy
FTyTuple ([FTy] -> FTy) -> [FTy] -> FTy
forall a b. (a -> b) -> a -> b
$ ((FTy -> FTy) -> [FTy] -> [FTy]
forall a b. (a -> b) -> [a] -> [b]
map ((FTy -> FTy) -> [FTy] -> [FTy]) -> (FTy -> FTy) -> [FTy] -> [FTy]
forall a b. (a -> b) -> a -> b
$ [(Var, FTy)] -> FTy -> FTy
subst' [(Var, FTy)]
f) [FTy]
ts
subst' [(Var, FTy)]
f (FTyVariant [FTy]
ts) = [FTy] -> FTy
FTyVariant ([FTy] -> FTy) -> [FTy] -> FTy
forall a b. (a -> b) -> a -> b
$ ((FTy -> FTy) -> [FTy] -> [FTy]
forall a b. (a -> b) -> [a] -> [b]
map ((FTy -> FTy) -> [FTy] -> [FTy]) -> (FTy -> FTy) -> [FTy] -> [FTy]
forall a b. (a -> b) -> a -> b
$ [(Var, FTy)] -> FTy -> FTy
subst' [(Var, FTy)]
f) [FTy]
ts
subst' [(Var, FTy)]
f FTy
FTyUnit = FTy
FTyUnit
subst' [(Var, FTy)]
f FTy
FTyVoid = FTy
FTyVoid
subst' [(Var, FTy)]
f (FTyList FTy
t) = FTy -> FTy
FTyList (FTy -> FTy) -> FTy -> FTy
forall a b. (a -> b) -> a -> b
$ [(Var, FTy)] -> FTy -> FTy
subst' [(Var, FTy)]
f FTy
t
subst' [(Var, FTy)]
f (FTyFn FTy
t1 FTy
t2) = FTy -> FTy -> FTy
FTyFn ([(Var, FTy)] -> FTy -> FTy
subst' [(Var, FTy)]
f FTy
t1) ([(Var, FTy)] -> FTy -> FTy
subst' [(Var, FTy)]
f FTy
t2)
subst' [(Var, FTy)]
f (FTyProd FTy
t1 FTy
t2) = FTy -> FTy -> FTy
FTyProd  ([(Var, FTy)] -> FTy -> FTy
subst' [(Var, FTy)]
f FTy
t1) ([(Var, FTy)] -> FTy -> FTy
subst' [(Var, FTy)]
f FTy
t2)
subst' [(Var, FTy)]
f (FTySum FTy
t1 FTy
t2) = FTy -> FTy -> FTy
FTySum  ([(Var, FTy)] -> FTy -> FTy
subst' [(Var, FTy)]
f FTy
t1) ([(Var, FTy)] -> FTy -> FTy
subst' [(Var, FTy)]
f FTy
t2)
subst' [(Var, FTy)]
f (FTyVar Var
v) = case Var -> [(Var, FTy)] -> Maybe FTy
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Var
v [(Var, FTy)]
f of
                        Maybe FTy
Nothing -> Var -> FTy
FTyVar Var
v
                        Just FTy
y -> FTy
y
subst' [(Var, FTy)]
f (FForall [Var]
vs FTy
t) = [Var] -> FTy -> FTy
FForall [Var]
vs (FTy -> FTy) -> FTy -> FTy
forall a b. (a -> b) -> a -> b
$ [(Var, FTy)] -> FTy -> FTy
subst' [(Var, FTy)]
f' FTy
t
 where f' :: [(Var, FTy)]
f' = ((Var, FTy) -> Bool) -> [(Var, FTy)] -> [(Var, FTy)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Var
v,FTy
f')-> Bool -> Bool
not (Var -> [Var] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Var
v [Var]
vs)) [(Var, FTy)]
f
subst' [(Var, FTy)]
f (FTyCon Var
v [FTy]
ts) = Var -> [FTy] -> FTy
FTyCon Var
v ([FTy] -> FTy) -> [FTy] -> FTy
forall a b. (a -> b) -> a -> b
$ (FTy -> FTy) -> [FTy] -> [FTy]
forall a b. (a -> b) -> [a] -> [b]
map ([(Var, FTy)] -> FTy -> FTy
subst' [(Var, FTy)]
f) [FTy]
ts

instance Show Ctx where
  show :: Ctx -> Var
show [] = Var
""
  show ((Var
k,TypSch
v):Ctx
t) = Var
k Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
":" Var -> ShowS
forall a. [a] -> [a] -> [a]
++ TypSch -> Var
forall a. Show a => a -> Var
show TypSch
v Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Ctx -> Var
forall a. Show a => a -> Var
show Ctx
t

------------------------------------
-- Type checking for F

open :: [Var] -> [FTy] -> FTy -> Either String FTy
open :: [Var] -> [FTy] -> FTy -> Either Var FTy
open [Var]
vs [FTy]
ts FTy
e | [Var] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
vs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [FTy] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [FTy]
ts = FTy -> Either Var FTy
forall a. a -> Either Var a
forall (m :: * -> *) a. Monad m => a -> m a
return (FTy -> Either Var FTy) -> FTy -> Either Var FTy
forall a b. (a -> b) -> a -> b
$ [(Var, FTy)] -> FTy -> FTy
subst' ([Var] -> [FTy] -> [(Var, FTy)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
vs [FTy]
ts) FTy
e
             | Bool
otherwise = Var -> Either Var FTy
forall a. Var -> Either Var a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError Var
"Cannot open"

typeOf :: ADTs -> [Var] -> [(Var,FTy)] -> FExpr -> Either String FTy
typeOf :: ADTs -> [Var] -> [(Var, FTy)] -> FExpr -> Either Var FTy
typeOf ADTs
adts [Var]
tvs [(Var, FTy)]
g (FCase FExpr
e FTy
r [FExpr]
es) = do { [FTy]
ts <- (FExpr -> Either Var FTy) -> [FExpr] -> Either Var [FTy]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (ADTs -> [Var] -> [(Var, FTy)] -> FExpr -> Either Var FTy
typeOf ADTs
adts [Var]
tvs [(Var, FTy)]
g) [FExpr]
es
                                      ; FTy
t <- ADTs -> [Var] -> [(Var, FTy)] -> FExpr -> Either Var FTy
typeOf ADTs
adts [Var]
tvs [(Var, FTy)]
g FExpr
e
                                      ; case FTy
t of
                                         FTyVariant [FTy]
ts' -> if [FTy] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [FTy]
ts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [FTy] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [FTy]
ts'
                                                           then do { ((FTy, FTy) -> Either Var ()) -> [(FTy, FTy)] -> Either Var [()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (FTy, FTy) -> Either Var ()
forall {m :: * -> *}. Monad m => (FTy, FTy) -> m ()
f ([(FTy, FTy)] -> Either Var [()])
-> [(FTy, FTy)] -> Either Var [()]
forall a b. (a -> b) -> a -> b
$ [FTy] -> [FTy] -> [(FTy, FTy)]
forall a b. [a] -> [b] -> [(a, b)]
zip [FTy]
ts [FTy]
ts'
                                                                   ; FTy -> Either Var FTy
forall a. a -> Either Var a
forall (m :: * -> *) a. Monad m => a -> m a
return FTy
r }
                                                           else Var -> Either Var FTy
forall a. Var -> Either Var a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Var -> Either Var FTy) -> Var -> Either Var FTy
forall a b. (a -> b) -> a -> b
$ Var
"bad number of cases "
                                         FTy
z -> Var -> Either Var FTy
forall a. Var -> Either Var a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Var -> Either Var FTy) -> Var -> Either Var FTy
forall a b. (a -> b) -> a -> b
$ FTy -> Var
forall a. Show a => a -> Var
show FTy
z Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" is not a variant"}
 where f :: (FTy, FTy) -> m ()
f ((FTyFn FTy
a FTy
b), FTy
exp) | FTy
a FTy -> FTy -> Bool
forall a. Eq a => a -> a -> Bool
== FTy
exp Bool -> Bool -> Bool
&& FTy
b FTy -> FTy -> Bool
forall a. Eq a => a -> a -> Bool
== FTy
r = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
typeOf ADTs
adts [Var]
tvs [(Var, FTy)]
g (FInj Int
i [FTy]
ts FExpr
e) = do { FTy
t <- ADTs -> [Var] -> [(Var, FTy)] -> FExpr -> Either Var FTy
typeOf ADTs
adts [Var]
tvs [(Var, FTy)]
g FExpr
e
                                     ; if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= [FTy] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [FTy]
ts
                                       then Var -> Either Var FTy
forall a. Var -> Either Var a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Var -> Either Var FTy) -> Var -> Either Var FTy
forall a b. (a -> b) -> a -> b
$ Var
"bad inj index " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Var
forall a. Show a => a -> Var
show Int
i Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" on " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FExpr -> Var
forall a. Show a => a -> Var
show FExpr
e
                                       else if [FTy]
ts [FTy] -> Int -> FTy
forall a. HasCallStack => [a] -> Int -> a
!! Int
i FTy -> FTy -> Bool
forall a. Eq a => a -> a -> Bool
== FTy
t
                                            then FTy -> Either Var FTy
forall a. a -> Either Var a
forall (m :: * -> *) a. Monad m => a -> m a
return (FTy -> Either Var FTy) -> FTy -> Either Var FTy
forall a b. (a -> b) -> a -> b
$ [FTy] -> FTy
FTyVariant [FTy]
ts
                                            else Var -> Either Var FTy
forall a. Var -> Either Var a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Var -> Either Var FTy) -> Var -> Either Var FTy
forall a b. (a -> b) -> a -> b
$ Var
"injection type mismatch " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FExpr -> Var
forall a. Show a => a -> Var
show (Int -> [FTy] -> FExpr -> FExpr
FInj Int
i [FTy]
ts FExpr
e) Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
", " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FTy -> Var
forall a. Show a => a -> Var
show ([FTy]
ts [FTy] -> Int -> FTy
forall a. HasCallStack => [a] -> Int -> a
!! Int
i) Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" <> " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FTy -> Var
forall a. Show a => a -> Var
show FTy
t }
typeOf ADTs
adts [Var]
tvs [(Var, FTy)]
g (FProj Int
i FExpr
e) = do { FTy
t <- ADTs -> [Var] -> [(Var, FTy)] -> FExpr -> Either Var FTy
typeOf ADTs
adts [Var]
tvs [(Var, FTy)]
g FExpr
e
                                   ; case FTy
t of
                                      FTyTuple [FTy]
ts -> if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= [FTy] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [FTy]
ts
                                                     then Var -> Either Var FTy
forall a. Var -> Either Var a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Var -> Either Var FTy) -> Var -> Either Var FTy
forall a b. (a -> b) -> a -> b
$ Var
"bad proj index " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Var
forall a. Show a => a -> Var
show Int
i Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" on " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FExpr -> Var
forall a. Show a => a -> Var
show FExpr
e
                                                     else FTy -> Either Var FTy
forall a. a -> Either Var a
forall (m :: * -> *) a. Monad m => a -> m a
return (FTy -> Either Var FTy) -> FTy -> Either Var FTy
forall a b. (a -> b) -> a -> b
$ [FTy]
ts [FTy] -> Int -> FTy
forall a. HasCallStack => [a] -> Int -> a
!! Int
i
                                      FTy
z -> Var -> Either Var FTy
forall a. Var -> Either Var a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Var -> Either Var FTy) -> Var -> Either Var FTy
forall a b. (a -> b) -> a -> b
$ FTy -> Var
forall a. Show a => a -> Var
show FTy
z Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" is not a tuple type" }
typeOf ADTs
adts [Var]
tvs [(Var, FTy)]
g (FTuple [FExpr]
es) = do { [FTy]
ts <- (FExpr -> Either Var FTy) -> [FExpr] -> Either Var [FTy]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (ADTs -> [Var] -> [(Var, FTy)] -> FExpr -> Either Var FTy
typeOf ADTs
adts [Var]
tvs [(Var, FTy)]
g) [FExpr]
es
                                   ; FTy -> Either Var FTy
forall a. a -> Either Var a
forall (m :: * -> *) a. Monad m => a -> m a
return (FTy -> Either Var FTy) -> FTy -> Either Var FTy
forall a b. (a -> b) -> a -> b
$ [FTy] -> FTy
FTyTuple [FTy]
ts }
typeOf ADTs
adts [Var]
tvs [(Var, FTy)]
g (FVar Var
x) = case Var -> [(Var, FTy)] -> Maybe FTy
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Var
x [(Var, FTy)]
g of
  Maybe FTy
Nothing -> Var -> Either Var FTy
forall a. Var -> Either Var a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Var -> Either Var FTy) -> Var -> Either Var FTy
forall a b. (a -> b) -> a -> b
$ Var
"unbound var: " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
x
  Just FTy
y -> FTy -> Either Var FTy
forall a. a -> Either Var a
forall (m :: * -> *) a. Monad m => a -> m a
return FTy
y
typeOf ADTs
adts [Var]
tvs [(Var, FTy)]
g (FConst Prim
p) = do { TypSch
t <- ADTs -> Prim -> Either Var TypSch
primTy ADTs
adts Prim
p ; FTy -> Either Var FTy
forall a. a -> Either Var a
forall (m :: * -> *) a. Monad m => a -> m a
return (FTy -> Either Var FTy) -> FTy -> Either Var FTy
forall a b. (a -> b) -> a -> b
$ TypSch -> FTy
tyToFTy TypSch
t }
typeOf ADTs
adts [Var]
tvs [(Var, FTy)]
g (FApp FExpr
a FExpr
b) = do { FTy
t1 <- ADTs -> [Var] -> [(Var, FTy)] -> FExpr -> Either Var FTy
typeOf ADTs
adts [Var]
tvs [(Var, FTy)]
g FExpr
a
                                  ; FTy
t2 <- ADTs -> [Var] -> [(Var, FTy)] -> FExpr -> Either Var FTy
typeOf ADTs
adts [Var]
tvs [(Var, FTy)]
g FExpr
b
                                  ; case FTy
t1 of
                                      FTyFn FTy
p FTy
q -> if FTy
p FTy -> FTy -> Bool
forall a. Eq a => a -> a -> Bool
== FTy
t2
                                                   then FTy -> Either Var FTy
forall a. a -> Either Var a
forall (m :: * -> *) a. Monad m => a -> m a
return FTy
q
                                                   else Var -> Either Var FTy
forall a. Var -> Either Var a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Var -> Either Var FTy) -> Var -> Either Var FTy
forall a b. (a -> b) -> a -> b
$ Var
"In " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ (FExpr -> Var
forall a. Show a => a -> Var
show (FExpr -> Var) -> FExpr -> Var
forall a b. (a -> b) -> a -> b
$ FExpr -> FExpr -> FExpr
FApp FExpr
a FExpr
b) Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" expected " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FTy -> Var
forall a. Show a => a -> Var
show FTy
p Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" given " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FTy -> Var
forall a. Show a => a -> Var
show FTy
t2
                                      FTy
v -> Var -> Either Var FTy
forall a. Var -> Either Var a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Var -> Either Var FTy) -> Var -> Either Var FTy
forall a b. (a -> b) -> a -> b
$ Var
"In " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FExpr -> Var
forall a. Show a => a -> Var
show (FExpr -> FExpr -> FExpr
FApp FExpr
a FExpr
b) Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" not a fn type: " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FTy -> Var
forall a. Show a => a -> Var
show FTy
v }
typeOf ADTs
adts [Var]
tvs [(Var, FTy)]
g (FAbs Var
x FTy
t FExpr
e) = do { FTy
t1 <- ADTs -> [Var] -> [(Var, FTy)] -> FExpr -> Either Var FTy
typeOf ADTs
adts [Var]
tvs ((Var
x,FTy
t)(Var, FTy) -> [(Var, FTy)] -> [(Var, FTy)]
forall a. a -> [a] -> [a]
:[(Var, FTy)]
g) FExpr
e
                                    ; FTy -> Either Var FTy
forall a. a -> Either Var a
forall (m :: * -> *) a. Monad m => a -> m a
return (FTy -> Either Var FTy) -> FTy -> Either Var FTy
forall a b. (a -> b) -> a -> b
$ FTy
t FTy -> FTy -> FTy
`FTyFn` FTy
t1 }
typeOf ADTs
adts [Var]
tvs [(Var, FTy)]
g (FTyAbs [Var]
vs FExpr
e) = do { FTy
t1 <- ADTs -> [Var] -> [(Var, FTy)] -> FExpr -> Either Var FTy
typeOf ADTs
adts ([Var]
vs[Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++[Var]
tvs) [(Var, FTy)]
g FExpr
e
                                     ; FTy -> Either Var FTy
forall a. a -> Either Var a
forall (m :: * -> *) a. Monad m => a -> m a
return (FTy -> Either Var FTy) -> FTy -> Either Var FTy
forall a b. (a -> b) -> a -> b
$ [Var] -> FTy -> FTy
FForall [Var]
vs FTy
t1 }
typeOf ADTs
adts [Var]
tvs [(Var, FTy)]
g (FTyApp FExpr
e [FTy]
ts) = do { FTy
t1 <- ADTs -> [Var] -> [(Var, FTy)] -> FExpr -> Either Var FTy
typeOf ADTs
adts [Var]
tvs [(Var, FTy)]
g FExpr
e
                                     ; case FTy
t1 of
                                        FForall [Var]
vs FTy
t -> [Var] -> [FTy] -> FTy -> Either Var FTy
open [Var]
vs [FTy]
ts FTy
t
                                        FTy
v -> Var -> Either Var FTy
forall a. Var -> Either Var a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Var -> Either Var FTy) -> Var -> Either Var FTy
forall a b. (a -> b) -> a -> b
$ Var
"not a forall type: " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FTy -> Var
forall a. Show a => a -> Var
show FTy
v }
typeOf ADTs
adts [Var]
tvs [(Var, FTy)]
g (FLetrec [(Var, FTy, FExpr)]
es FExpr
e) = do { let g' :: [(Var, FTy)]
g' = ((Var, FTy, FExpr) -> (Var, FTy))
-> [(Var, FTy, FExpr)] -> [(Var, FTy)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Var
k,FTy
t,FExpr
e)->(Var
k,FTy
t)) [(Var, FTy, FExpr)]
es
                                      ; [FTy]
est <- ((Var, FTy, FExpr) -> Either Var FTy)
-> [(Var, FTy, FExpr)] -> Either Var [FTy]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\(Var
_,FTy
_,FExpr
v)->ADTs -> [Var] -> [(Var, FTy)] -> FExpr -> Either Var FTy
typeOf ADTs
adts [Var]
tvs ([(Var, FTy)]
g'[(Var, FTy)] -> [(Var, FTy)] -> [(Var, FTy)]
forall a. [a] -> [a] -> [a]
++[(Var, FTy)]
g) FExpr
v) [(Var, FTy, FExpr)]
es
                                      ; if [FTy]
est [FTy] -> [FTy] -> Bool
forall a. Eq a => a -> a -> Bool
== (([Var], [FTy]) -> [FTy]
forall a b. (a, b) -> b
snd (([Var], [FTy]) -> [FTy]) -> ([Var], [FTy]) -> [FTy]
forall a b. (a -> b) -> a -> b
$ [(Var, FTy)] -> ([Var], [FTy])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Var, FTy)]
g')
                                        then ADTs -> [Var] -> [(Var, FTy)] -> FExpr -> Either Var FTy
typeOf ADTs
adts [Var]
tvs [(Var, FTy)]
g' FExpr
e
                                        else Var -> Either Var FTy
forall a. Var -> Either Var a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Var -> Either Var FTy) -> Var -> Either Var FTy
forall a b. (a -> b) -> a -> b
$ Var
"Disagree: " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ [FTy] -> Var
forall a. Show a => a -> Var
show [FTy]
est Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" and " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ ([FTy] -> Var
forall a. Show a => a -> Var
show ([FTy] -> Var) -> [FTy] -> Var
forall a b. (a -> b) -> a -> b
$ ([Var], [FTy]) -> [FTy]
forall a b. (a, b) -> b
snd (([Var], [FTy]) -> [FTy]) -> ([Var], [FTy]) -> [FTy]
forall a b. (a -> b) -> a -> b
$ [(Var, FTy)] -> ([Var], [FTy])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Var, FTy)]
g') }


-----------------------------
-- Unification

mgu :: MTy -> MTy -> E Subst
mgu :: MTy -> MTy -> E Subst
mgu (TyLit LiteralType
lt1) (TyLit LiteralType
lt2) = if LiteralType
lt1 LiteralType -> LiteralType -> Bool
forall a. Eq a => a -> a -> Bool
== LiteralType
lt2
  then Subst -> E Subst
forall a. a -> ExceptT Var (State ([Var], Integer)) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
  else Var -> E Subst
forall a. Var -> ExceptT Var (State ([Var], Integer)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Var -> E Subst) -> Var -> E Subst
forall a b. (a -> b) -> a -> b
$ Var
"Cannot unify literal types " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ LiteralType -> Var
forall a. Show a => a -> Var
show LiteralType
lt1 Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" and " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ LiteralType -> Var
forall a. Show a => a -> Var
show LiteralType
lt2
mgu (TyVariant [MTy]
ts1) (TyVariant [MTy]
ts2) | [MTy] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [MTy]
ts1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [MTy] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [MTy]
ts2 = [MTy] -> [MTy] -> E Subst
mgu' [MTy]
ts1 [MTy]
ts2
                                    | Bool
otherwise = Var -> E Subst
forall a. Var -> ExceptT Var (State ([Var], Integer)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Var -> E Subst) -> Var -> E Subst
forall a b. (a -> b) -> a -> b
$ Var
"cannot unify " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ [MTy] -> Var
forall a. Show a => a -> Var
show [MTy]
ts1 Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" with " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ [MTy] -> Var
forall a. Show a => a -> Var
show [MTy]
ts2
mgu (TyTuple [MTy]
ts1) (TyTuple [MTy]
ts2) | [MTy] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [MTy]
ts1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [MTy] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [MTy]
ts2 = [MTy] -> [MTy] -> E Subst
mgu' [MTy]
ts1 [MTy]
ts2
                                | Bool
otherwise = Var -> E Subst
forall a. Var -> ExceptT Var (State ([Var], Integer)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Var -> E Subst) -> Var -> E Subst
forall a b. (a -> b) -> a -> b
$ Var
"cannot unify " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ [MTy] -> Var
forall a. Show a => a -> Var
show [MTy]
ts1 Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" with " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ [MTy] -> Var
forall a. Show a => a -> Var
show [MTy]
ts2
mgu (TyList MTy
a) (TyList MTy
b) = MTy -> MTy -> E Subst
mgu MTy
a MTy
b
mgu MTy
TyUnit MTy
TyUnit = Subst -> E Subst
forall a. a -> ExceptT Var (State ([Var], Integer)) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
mgu MTy
TyVoid MTy
TyVoid = Subst -> E Subst
forall a. a -> ExceptT Var (State ([Var], Integer)) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
mgu (TyCon Var
a [MTy]
as) (TyCon Var
b [MTy]
bs) | Var
a Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
b Bool -> Bool -> Bool
&& [MTy] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [MTy]
as Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [MTy] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [MTy]
bs = [MTy] -> [MTy] -> E Subst
mgu' [MTy]
as [MTy]
bs
                              | Bool
otherwise = Var -> E Subst
forall a. Var -> ExceptT Var (State ([Var], Integer)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Var -> E Subst) -> Var -> E Subst
forall a b. (a -> b) -> a -> b
$ Var
"cannot unify " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> Var
show Var
a Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" with " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> Var
show Var
b
mgu (TyProd MTy
a MTy
b) (TyProd MTy
a' MTy
b') = do { Subst
s <- MTy -> MTy -> E Subst
mgu MTy
a MTy
a' ; Subst
s' <- MTy -> MTy -> E Subst
mgu (Subst -> MTy -> MTy
forall a. Substable a => Subst -> a -> a
subst Subst
s MTy
b) (Subst -> MTy -> MTy
forall a. Substable a => Subst -> a -> a
subst Subst
s MTy
b'); Subst -> E Subst
forall a. a -> ExceptT Var (State ([Var], Integer)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst -> E Subst) -> Subst -> E Subst
forall a b. (a -> b) -> a -> b
$ Subst
s' Subst -> Subst -> Subst
`o` Subst
s }
mgu (TySum  MTy
a MTy
b) (TySum  MTy
a' MTy
b') = do { Subst
s <- MTy -> MTy -> E Subst
mgu MTy
a MTy
a' ; Subst
s' <- MTy -> MTy -> E Subst
mgu (Subst -> MTy -> MTy
forall a. Substable a => Subst -> a -> a
subst Subst
s MTy
b) (Subst -> MTy -> MTy
forall a. Substable a => Subst -> a -> a
subst Subst
s MTy
b'); Subst -> E Subst
forall a. a -> ExceptT Var (State ([Var], Integer)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst -> E Subst) -> Subst -> E Subst
forall a b. (a -> b) -> a -> b
$ Subst
s' Subst -> Subst -> Subst
`o` Subst
s }
mgu (TyFn   MTy
a MTy
b) (TyFn   MTy
a' MTy
b') = do { Subst
s <- MTy -> MTy -> E Subst
mgu MTy
a MTy
a' ; Subst
s' <- MTy -> MTy -> E Subst
mgu (Subst -> MTy -> MTy
forall a. Substable a => Subst -> a -> a
subst Subst
s MTy
b) (Subst -> MTy -> MTy
forall a. Substable a => Subst -> a -> a
subst Subst
s MTy
b'); Subst -> E Subst
forall a. a -> ExceptT Var (State ([Var], Integer)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst -> E Subst) -> Subst -> E Subst
forall a b. (a -> b) -> a -> b
$ Subst
s' Subst -> Subst -> Subst
`o` Subst
s }
mgu (TyVar Var
a) (TyVar Var
b) | Var
a Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
b = Subst -> E Subst
forall a. a -> ExceptT Var (State ([Var], Integer)) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
mgu (TyVar Var
a) MTy
b = do { Var -> MTy -> E ()
occurs Var
a MTy
b; Subst -> E Subst
forall a. a -> ExceptT Var (State ([Var], Integer)) a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Var
a, MTy
b)] }
mgu MTy
a (TyVar Var
b) = MTy -> MTy -> E Subst
mgu (Var -> MTy
TyVar Var
b) MTy
a
mgu MTy
a MTy
b = Var -> E Subst
forall a. Var -> ExceptT Var (State ([Var], Integer)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Var -> E Subst) -> Var -> E Subst
forall a b. (a -> b) -> a -> b
$ Var
"cannot unify " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ MTy -> Var
forall a. Show a => a -> Var
show MTy
a Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" with " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ MTy -> Var
forall a. Show a => a -> Var
show MTy
b

mgu' :: [MTy] -> [MTy] -> E Subst
mgu' :: [MTy] -> [MTy] -> E Subst
mgu' [] [] = Subst -> E Subst
forall a. a -> ExceptT Var (State ([Var], Integer)) a
forall (m :: * -> *) a. Monad m => a -> m a
return Subst
idSubst
mgu' (MTy
a:[MTy]
as) (MTy
b:[MTy]
bs) = do { Subst
f <- MTy -> MTy -> E Subst
mgu MTy
a MTy
b; Subst
s <- [MTy] -> [MTy] -> E Subst
mgu' ((MTy -> MTy) -> [MTy] -> [MTy]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> MTy -> MTy
forall a. Substable a => Subst -> a -> a
subst Subst
f) [MTy]
as) ((MTy -> MTy) -> [MTy] -> [MTy]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> MTy -> MTy
forall a. Substable a => Subst -> a -> a
subst Subst
f) [MTy]
bs); Subst -> E Subst
forall a. a -> ExceptT Var (State ([Var], Integer)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst -> E Subst) -> Subst -> E Subst
forall a b. (a -> b) -> a -> b
$ Subst
s Subst -> Subst -> Subst
`o` Subst
f }

occurs :: Var -> MTy -> E ()
occurs :: Var -> MTy -> E ()
occurs Var
v (TyLit LiteralType
_) = () -> E ()
forall a. a -> ExceptT Var (State ([Var], Integer)) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
occurs Var
v (TyCon Var
_ [MTy]
ts) = (MTy -> E ()) -> [MTy] -> E ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Var -> MTy -> E ()
occurs Var
v) [MTy]
ts
occurs Var
v (TyTuple [MTy]
ts) = (MTy -> E ()) -> [MTy] -> E ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Var -> MTy -> E ()
occurs Var
v) [MTy]
ts
occurs Var
v (TyVariant [MTy]
ts) = (MTy -> E ()) -> [MTy] -> E ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Var -> MTy -> E ()
occurs Var
v) [MTy]
ts
occurs Var
v (TyList MTy
l) = Var -> MTy -> E ()
occurs Var
v MTy
l
occurs Var
v MTy
TyUnit = () -> E ()
forall a. a -> ExceptT Var (State ([Var], Integer)) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
occurs Var
v MTy
TyVoid = () -> E ()
forall a. a -> ExceptT Var (State ([Var], Integer)) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
occurs Var
v (TyFn   MTy
a MTy
b) = do { Var -> MTy -> E ()
occurs Var
v MTy
a; Var -> MTy -> E ()
occurs Var
v MTy
b }
occurs Var
v (TyProd MTy
a MTy
b) = do { Var -> MTy -> E ()
occurs Var
v MTy
a; Var -> MTy -> E ()
occurs Var
v MTy
b }
occurs Var
v (TySum  MTy
a MTy
b) = do { Var -> MTy -> E ()
occurs Var
v MTy
a; Var -> MTy -> E ()
occurs Var
v MTy
b }
occurs Var
v (TyVar Var
v') | Var
v Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
v' = Var -> E ()
forall a. Var -> ExceptT Var (State ([Var], Integer)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Var -> E ()) -> Var -> E ()
forall a b. (a -> b) -> a -> b
$ Var
"occurs check failed"
                    | Bool
otherwise = () -> E ()
forall a. a -> ExceptT Var (State ([Var], Integer)) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-----------------------------
-- Algorithm W

type E = ExceptT String (State ([String],Integer))
type M a = E (Subst, a)

log0 :: Int -> String -> E ()
log0 :: Int -> Var -> E ()
log0 Int
i Var
x = do { ([Var]
l, Integer
s) <- ExceptT Var (State ([Var], Integer)) ([Var], Integer)
forall s (m :: * -> *). MonadState s m => m s
get; ([Var], Integer) -> E ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((Var
x'Var -> ShowS
forall a. [a] -> [a] -> [a]
++Var
x)Var -> [Var] -> [Var]
forall a. a -> [a] -> [a]
:[Var]
l, Integer
s); }
 where x' :: Var
x' = (Var -> Int -> Var) -> Var -> [Int] -> Var
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\Var
p Int
q -> Var
"\t" Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
p) Var
"" [Int
0..Int
i]

fresh :: E MTy
fresh :: E MTy
fresh = do { ([Var]
l,Integer
s) <- ExceptT Var (State ([Var], Integer)) ([Var], Integer)
forall s (m :: * -> *). MonadState s m => m s
get; ([Var], Integer) -> E ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ([Var]
l, Integer
s Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1); MTy -> E MTy
forall a. a -> ExceptT Var (State ([Var], Integer)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (MTy -> E MTy) -> MTy -> E MTy
forall a b. (a -> b) -> a -> b
$ Var -> MTy
TyVar (Var -> MTy) -> Var -> MTy
forall a b. (a -> b) -> a -> b
$ Var
"v" Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> Var
forall a. Show a => a -> Var
show Integer
s }

inst :: TypSch -> E (MTy,[MTy])
inst :: TypSch -> E (MTy, [MTy])
inst (Forall [Var]
vs MTy
ty) = do { [MTy]
vs' <- (Var -> E MTy)
-> [Var] -> ExceptT Var (State ([Var], Integer)) [MTy]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\Var
_->E MTy
fresh) [Var]
vs; (MTy, [MTy]) -> E (MTy, [MTy])
forall a. a -> ExceptT Var (State ([Var], Integer)) a
forall (m :: * -> *) a. Monad m => a -> m a
return ((MTy, [MTy]) -> E (MTy, [MTy])) -> (MTy, [MTy]) -> E (MTy, [MTy])
forall a b. (a -> b) -> a -> b
$ (Subst -> MTy -> MTy
forall a. Substable a => Subst -> a -> a
subst ([Var] -> [MTy] -> Subst
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
vs [MTy]
vs') MTy
ty,  [MTy]
vs') }

gen :: Ctx -> MTy -> (TypSch, [Var])
gen :: Ctx -> MTy -> (TypSch, [Var])
gen Ctx
g MTy
t = ([Var] -> MTy -> TypSch
Forall [Var]
vs MTy
t , [Var]
vs)
 where vs :: [Var]
vs = [Var] -> [Var]
forall a. Eq a => [a] -> [a]
nub ([Var] -> [Var]) -> [Var] -> [Var]
forall a b. (a -> b) -> a -> b
$ (Var -> Bool) -> [Var] -> [Var]
forall a. (a -> Bool) -> [a] -> [a]
filter (\Var
v -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Var -> [Var] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Var
v (Ctx -> [Var]
forall a. Vars a => a -> [Var]
vars Ctx
g)) (MTy -> [Var]
forall a. Vars a => a -> [Var]
vars MTy
t)

fTyApp :: FExpr -> [FTy] -> FExpr
fTyApp FExpr
x [] = FExpr
x
fTyApp FExpr
x [FTy]
y = FExpr -> [FTy] -> FExpr
FTyApp FExpr
x [FTy]
y

fTyAbs :: [Var] -> FExpr -> FExpr
fTyAbs [] FExpr
x = FExpr
x
fTyAbs [Var]
x FExpr
y = [Var] -> FExpr -> FExpr
FTyAbs [Var]
x FExpr
y

replace :: [b] -> (a, b) -> [b]
replace [] (a, b)
_ = []
replace (b
_:[b]
xs) (a
0,b
a) = b
ab -> [b] -> [b]
forall a. a -> [a] -> [a]
:[b]
xs
replace (b
x:[b]
xs) (a
n,b
a) =
  if a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
0
    then (b
xb -> [b] -> [b]
forall a. a -> [a] -> [a]
:[b]
xs)
    else b
xb -> [b] -> [b]
forall a. a -> [a] -> [a]
: [b] -> (a, b) -> [b]
replace [b]
xs (a
na -> a -> a
forall a. Num a => a -> a -> a
-a
1,b
a)

checkAgainstF :: ADTs -> Ctx -> MTy -> FExpr -> E ()
checkAgainstF :: ADTs -> Ctx -> MTy -> FExpr -> E ()
checkAgainstF ADTs
adts Ctx
g MTy
t FExpr
e = case (ADTs -> [Var] -> [(Var, FTy)] -> FExpr -> Either Var FTy
typeOf ADTs
adts [] [(Var, FTy)]
g' FExpr
e) of
                              Left Var
err -> Var -> E ()
forall a. Var -> ExceptT Var (State ([Var], Integer)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError  (Var -> E ()) -> Var -> E ()
forall a b. (a -> b) -> a -> b
$ Var
"\t" Var -> ShowS
forall a. [a] -> [a] -> [a]
++  Var
"err: " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
err
                              Right FTy
tt -> if FTy
tt FTy -> FTy -> Bool
forall a. Eq a => a -> a -> Bool
== MTy -> FTy
mTyToFTy MTy
t
                                          then () -> E ()
forall a. a -> ExceptT Var (State ([Var], Integer)) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                                          else Var -> E ()
forall a. Var -> ExceptT Var (State ([Var], Integer)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Var -> E ()) -> Var -> E ()
forall a b. (a -> b) -> a -> b
$ Ctx -> Var
forall a. Show a => a -> Var
show Ctx
g Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
"|- " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FExpr -> Var
forall a. Show a => a -> Var
show FExpr
e Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
": " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FTy -> Var
forall a. Show a => a -> Var
show FTy
tt Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" != " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ MTy -> Var
forall a. Show a => a -> Var
show MTy
t
 where g' :: [(Var, FTy)]
g' = ((Var, TypSch) -> (Var, FTy)) -> Ctx -> [(Var, FTy)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Var
k,TypSch
v)->(Var
k, TypSch -> FTy
tyToFTy TypSch
v)) Ctx
g

w :: Int -> ADTs -> Ctx -> Expr -> M (MTy, FExpr)
w :: Int -> ADTs -> Ctx -> Expr -> M (MTy, FExpr)
w Int
l ADTs
adts Ctx
g (Case' Expr
e [Expr]
es') = do { MTy
t <- E MTy
fresh
                            ; [MTy]
bs' <- (Expr -> E MTy)
-> [Expr] -> ExceptT Var (State ([Var], Integer)) [MTy]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\Expr
_->E MTy
fresh) [Expr]
es'
                            ; let bs :: [MTy]
bs = (MTy -> MTy) -> [MTy] -> [MTy]
forall a b. (a -> b) -> [a] -> [b]
map (\MTy
k-> MTy -> MTy -> MTy
TyFn MTy
k MTy
t) [MTy]
bs'
                            ; (Subst
phi , ([MTy]
ts, [FExpr]
es)) <- Int
-> Ctx
-> [Expr]
-> ExceptT Var (State ([Var], Integer)) (Subst, ([MTy], [FExpr]))
w' (Int
lInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Ctx
g [Expr]
es'
                            ; Subst
m1 <- [MTy] -> [MTy] -> E Subst
mgu' [MTy]
bs [MTy]
ts
                            ; (Subst
phi', (MTy
t', FExpr
e')) <- Int -> ADTs -> Ctx -> Expr -> M (MTy, FExpr)
w  (Int
lInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ADTs
adts (Subst -> Ctx -> Ctx
forall a. Substable a => Subst -> a -> a
subst (Subst
m1 Subst -> Subst -> Subst
`o` Subst
phi) Ctx
g) Expr
e
                            ; Subst
m2 <- MTy -> MTy -> E Subst
mgu (Subst -> MTy -> MTy
forall a. Substable a => Subst -> a -> a
subst (Subst
m1 Subst -> Subst -> Subst
`o` Subst
phi) MTy
t') (Subst -> MTy -> MTy
forall a. Substable a => Subst -> a -> a
subst (Subst
m1 Subst -> Subst -> Subst
`o` Subst
phi' Subst -> Subst -> Subst
`o` Subst
phi) (MTy -> MTy) -> MTy -> MTy
forall a b. (a -> b) -> a -> b
$ [MTy] -> MTy
TyVariant [MTy]
bs')
                            ; let ret :: FExpr
ret = FExpr -> FTy -> [FExpr] -> FExpr
FCase (Subst -> FExpr -> FExpr
forall a. Substable a => Subst -> a -> a
subst (Subst
m2 ) FExpr
e') (MTy -> FTy
mTyToFTy MTy
ret_t) ((FExpr -> FExpr) -> [FExpr] -> [FExpr]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> FExpr -> FExpr
forall a. Substable a => Subst -> a -> a
subst (Subst -> FExpr -> FExpr) -> Subst -> FExpr -> FExpr
forall a b. (a -> b) -> a -> b
$ Subst
m2 Subst -> Subst -> Subst
`o` Subst
phi' Subst -> Subst -> Subst
`o` Subst
m1) [FExpr]
es)
                                  ret_t :: MTy
ret_t = Subst -> MTy -> MTy
forall a. Substable a => Subst -> a -> a
subst Subst
ret_subst MTy
t
                                  ret_subst :: Subst
ret_subst = Subst
m2 Subst -> Subst -> Subst
`o` Subst
phi' Subst -> Subst -> Subst
`o` Subst
m1 Subst -> Subst -> Subst
`o` Subst
phi
                            ; ADTs -> Ctx -> MTy -> FExpr -> E ()
checkAgainstF ADTs
adts (Subst -> Ctx -> Ctx
forall a. Substable a => Subst -> a -> a
subst Subst
ret_subst Ctx
g) MTy
ret_t FExpr
ret
                            ; (Subst, (MTy, FExpr)) -> M (MTy, FExpr)
forall a. a -> ExceptT Var (State ([Var], Integer)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
ret_subst, (MTy
ret_t, FExpr
ret)) }
 where w' :: Int
-> Ctx
-> [Expr]
-> ExceptT Var (State ([Var], Integer)) (Subst, ([MTy], [FExpr]))
w' Int
l Ctx
g [] = (Subst, ([MTy], [FExpr]))
-> ExceptT Var (State ([Var], Integer)) (Subst, ([MTy], [FExpr]))
forall a. a -> ExceptT Var (State ([Var], Integer)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
idSubst, ([], []))
       w' Int
l Ctx
g (Expr
e:[Expr]
tl) = do { (Subst
u,(MTy
u', FExpr
j)) <- Int -> ADTs -> Ctx -> Expr -> M (MTy, FExpr)
w Int
l ADTs
adts Ctx
g Expr
e
                        ; (Subst
r,([MTy]
r', [FExpr]
h)) <- Int
-> Ctx
-> [Expr]
-> ExceptT Var (State ([Var], Integer)) (Subst, ([MTy], [FExpr]))
w' Int
l (Subst -> Ctx -> Ctx
forall a. Substable a => Subst -> a -> a
subst Subst
u Ctx
g ) [Expr]
tl
                        ; (Subst, ([MTy], [FExpr]))
-> ExceptT Var (State ([Var], Integer)) (Subst, ([MTy], [FExpr]))
forall a. a -> ExceptT Var (State ([Var], Integer)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
r Subst -> Subst -> Subst
`o` Subst
u, ((Subst -> MTy -> MTy
forall a. Substable a => Subst -> a -> a
subst Subst
r MTy
u')MTy -> [MTy] -> [MTy]
forall a. a -> [a] -> [a]
:[MTy]
r', (Subst -> FExpr -> FExpr
forall a. Substable a => Subst -> a -> a
subst Subst
r FExpr
j)FExpr -> [FExpr] -> [FExpr]
forall a. a -> [a] -> [a]
:[FExpr]
h)) }
w Int
l ADTs
adts Ctx
g (Inj Int
i Int
j Expr
e) = do {
                     ; (Subst
s0, (MTy
t0, FExpr
a)) <- Int -> ADTs -> Ctx -> Expr -> M (MTy, FExpr)
w (Int
lInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ADTs
adts Ctx
g Expr
e
                     ; [MTy]
t'' <- (Int -> E MTy)
-> [Int] -> ExceptT Var (State ([Var], Integer)) [MTy]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\Int
_->E MTy
fresh) [Int
1..Int
j]
                     ; let t' :: [MTy]
t' = [MTy] -> (Int, MTy) -> [MTy]
forall {a} {b}. (Num a, Ord a) => [b] -> (a, b) -> [b]
replace [MTy]
t'' (Int
i, MTy
t0)
                     ; let ret :: FExpr
ret = Int -> [FTy] -> FExpr -> FExpr
FInj Int
i ((MTy -> FTy) -> [MTy] -> [FTy]
forall a b. (a -> b) -> [a] -> [b]
map (MTy -> FTy
mTyToFTy) [MTy]
t') FExpr
a
                           ret_t :: MTy
ret_t = [MTy] -> MTy
TyVariant [MTy]
t'
                           ret_subst :: Subst
ret_subst = Subst
s0
                     ; Int -> Var -> E ()
log0 Int
l (Var -> E ()) -> Var -> E ()
forall a b. (a -> b) -> a -> b
$ Var
"INJ " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Ctx -> Var
forall a. Show a => a -> Var
show (Subst -> Ctx -> Ctx
forall a. Substable a => Subst -> a -> a
subst Subst
ret_subst Ctx
g) Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
"|- " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ (FExpr -> Var
forall a. Show a => a -> Var
show (FExpr -> Var) -> FExpr -> Var
forall a b. (a -> b) -> a -> b
$ FExpr
ret) Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" : " Var -> ShowS
forall a. [a] -> [a] -> [a]
++  MTy -> Var
forall a. Show a => a -> Var
show MTy
ret_t
                     ; ADTs -> Ctx -> MTy -> FExpr -> E ()
checkAgainstF ADTs
adts (Subst -> Ctx -> Ctx
forall a. Substable a => Subst -> a -> a
subst Subst
ret_subst Ctx
g) MTy
ret_t FExpr
ret
                     ; (Subst, (MTy, FExpr)) -> M (MTy, FExpr)
forall a. a -> ExceptT Var (State ([Var], Integer)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
ret_subst, (MTy
ret_t, FExpr
ret)) }
w Int
l ADTs
adts Ctx
g (Proj Int
i Int
j Expr
e) = do {
                     ; (Subst
s0, (MTy
t0, FExpr
a)) <- Int -> ADTs -> Ctx -> Expr -> M (MTy, FExpr)
w (Int
lInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ADTs
adts Ctx
g Expr
e
                     ; [MTy]
t' <- (Int -> E MTy)
-> [Int] -> ExceptT Var (State ([Var], Integer)) [MTy]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\Int
_->E MTy
fresh) [Int
1..Int
j]
                     ; Subst
s2 <-  MTy
t0 MTy -> MTy -> E Subst
`mgu` ([MTy] -> MTy
TyTuple [MTy]
t')
                     ; let ret :: FExpr
ret = Int -> FExpr -> FExpr
FProj Int
i (Subst -> FExpr -> FExpr
forall a. Substable a => Subst -> a -> a
subst Subst
s2 FExpr
a)
                           ret_t :: MTy
ret_t = Subst -> MTy -> MTy
forall a. Substable a => Subst -> a -> a
subst Subst
s2 ([MTy]
t' [MTy] -> Int -> MTy
forall a. HasCallStack => [a] -> Int -> a
!! Int
i)
                           ret_subst :: Subst
ret_subst = Subst
s2 Subst -> Subst -> Subst
`o` Subst
s0
                     ; Int -> Var -> E ()
log0 Int
l (Var -> E ()) -> Var -> E ()
forall a b. (a -> b) -> a -> b
$ Var
"PROJ " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Ctx -> Var
forall a. Show a => a -> Var
show (Subst -> Ctx -> Ctx
forall a. Substable a => Subst -> a -> a
subst Subst
ret_subst Ctx
g) Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
"|- " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ (FExpr -> Var
forall a. Show a => a -> Var
show (FExpr -> Var) -> FExpr -> Var
forall a b. (a -> b) -> a -> b
$ FExpr
ret) Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" : " Var -> ShowS
forall a. [a] -> [a] -> [a]
++  MTy -> Var
forall a. Show a => a -> Var
show MTy
ret_t
                     ; ADTs -> Ctx -> MTy -> FExpr -> E ()
checkAgainstF ADTs
adts (Subst -> Ctx -> Ctx
forall a. Substable a => Subst -> a -> a
subst Subst
ret_subst Ctx
g) MTy
ret_t FExpr
ret
                     ; (Subst, (MTy, FExpr)) -> M (MTy, FExpr)
forall a. a -> ExceptT Var (State ([Var], Integer)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
ret_subst, (MTy
ret_t, FExpr
ret)) }
w Int
l ADTs
adts Ctx
g (Tuple [Expr]
es') = do { (Subst
phi, ([MTy]
ts, [FExpr]
es)) <- Int
-> Ctx
-> [Expr]
-> ExceptT Var (State ([Var], Integer)) (Subst, ([MTy], [FExpr]))
w' (Int
lInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Ctx
g [Expr]
es'
                            ; let ret :: FExpr
ret = [FExpr] -> FExpr
FTuple [FExpr]
es
                                  ret_t :: MTy
ret_t = [MTy] -> MTy
TyTuple [MTy]
ts
                                  ret_subst :: Subst
ret_subst = Subst
phi
                            ; Int -> Var -> E ()
log0 Int
l (Var -> E ()) -> Var -> E ()
forall a b. (a -> b) -> a -> b
$ Var
"TUPLE " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Ctx -> Var
forall a. Show a => a -> Var
show (Subst -> Ctx -> Ctx
forall a. Substable a => Subst -> a -> a
subst Subst
ret_subst Ctx
g) Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
"|- " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ (FExpr -> Var
forall a. Show a => a -> Var
show (FExpr -> Var) -> FExpr -> Var
forall a b. (a -> b) -> a -> b
$ FExpr
ret) Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" : " Var -> ShowS
forall a. [a] -> [a] -> [a]
++  MTy -> Var
forall a. Show a => a -> Var
show MTy
ret_t
                            ; ADTs -> Ctx -> MTy -> FExpr -> E ()
checkAgainstF ADTs
adts (Subst -> Ctx -> Ctx
forall a. Substable a => Subst -> a -> a
subst Subst
ret_subst Ctx
g) MTy
ret_t FExpr
ret
                            ; (Subst, (MTy, FExpr)) -> M (MTy, FExpr)
forall a. a -> ExceptT Var (State ([Var], Integer)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
ret_subst, (MTy
ret_t, FExpr
ret)) }
 where w' :: Int
-> Ctx
-> [Expr]
-> ExceptT Var (State ([Var], Integer)) (Subst, ([MTy], [FExpr]))
w' Int
l Ctx
g [] = (Subst, ([MTy], [FExpr]))
-> ExceptT Var (State ([Var], Integer)) (Subst, ([MTy], [FExpr]))
forall a. a -> ExceptT Var (State ([Var], Integer)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
idSubst, ([], []))
       w' Int
l Ctx
g (Expr
e:[Expr]
tl) = do { (Subst
u,(MTy
u', FExpr
j)) <- Int -> ADTs -> Ctx -> Expr -> M (MTy, FExpr)
w Int
l ADTs
adts Ctx
g Expr
e
                        ; (Subst
r,([MTy]
r', [FExpr]
h)) <- Int
-> Ctx
-> [Expr]
-> ExceptT Var (State ([Var], Integer)) (Subst, ([MTy], [FExpr]))
w' Int
l (Subst -> Ctx -> Ctx
forall a. Substable a => Subst -> a -> a
subst Subst
u Ctx
g ) [Expr]
tl
                        ; (Subst, ([MTy], [FExpr]))
-> ExceptT Var (State ([Var], Integer)) (Subst, ([MTy], [FExpr]))
forall a. a -> ExceptT Var (State ([Var], Integer)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
r Subst -> Subst -> Subst
`o` Subst
u, ((Subst -> MTy -> MTy
forall a. Substable a => Subst -> a -> a
subst Subst
r MTy
u')MTy -> [MTy] -> [MTy]
forall a. a -> [a] -> [a]
:[MTy]
r', (Subst -> FExpr -> FExpr
forall a. Substable a => Subst -> a -> a
subst Subst
r FExpr
j)FExpr -> [FExpr] -> [FExpr]
forall a. a -> [a] -> [a]
:[FExpr]
h)) }
w Int
l ADTs
adts Ctx
g (Const Prim
p) = do { case ADTs -> Prim -> Either Var TypSch
primTy ADTs
adts Prim
p of
                              Left Var
er -> Var -> M (MTy, FExpr)
forall a. Var -> ExceptT Var (State ([Var], Integer)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError Var
er
                              Right TypSch
t -> do { (MTy
ret_t, [MTy]
vs) <- TypSch -> E (MTy, [MTy])
inst TypSch
t
                        ; let ret :: FExpr
ret = FExpr -> [FTy] -> FExpr
fTyApp (Prim -> FExpr
FConst Prim
p) ([FTy] -> FExpr) -> [FTy] -> FExpr
forall a b. (a -> b) -> a -> b
$ (MTy -> FTy) -> [MTy] -> [FTy]
forall a b. (a -> b) -> [a] -> [b]
map MTy -> FTy
mTyToFTy [MTy]
vs
                          ; Int -> Var -> E ()
log0 Int
l (Var -> E ()) -> Var -> E ()
forall a b. (a -> b) -> a -> b
$ Var
"CONST " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Ctx -> Var
forall a. Show a => a -> Var
show Ctx
g Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
"|- " Var -> ShowS
forall a. [a] -> [a] -> [a]
++  FExpr -> Var
forall a. Show a => a -> Var
show FExpr
ret Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" : " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ MTy -> Var
forall a. Show a => a -> Var
show MTy
ret_t
                        ; ADTs -> Ctx -> MTy -> FExpr -> E ()
checkAgainstF ADTs
adts Ctx
g MTy
ret_t FExpr
ret
                        ; (Subst, (MTy, FExpr)) -> M (MTy, FExpr)
forall a. a -> ExceptT Var (State ([Var], Integer)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
idSubst, (MTy
ret_t, FExpr
ret)) } }
w Int
l ADTs
adts Ctx
g (Var Var
x) = case Var -> Ctx -> Maybe TypSch
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Var
x Ctx
g of
                Maybe TypSch
Nothing -> Var -> M (MTy, FExpr)
forall a. Var -> ExceptT Var (State ([Var], Integer)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Var -> M (MTy, FExpr)) -> Var -> M (MTy, FExpr)
forall a b. (a -> b) -> a -> b
$ Var
"Unknown var: " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ (ShowS
forall a. Show a => a -> Var
show Var
x)
                Just TypSch
s -> do { (MTy
ret_t, [MTy]
vs) <- TypSch -> E (MTy, [MTy])
inst TypSch
s
                             ; let ret :: FExpr
ret = FExpr -> [FTy] -> FExpr
fTyApp (Var -> FExpr
FVar Var
x) ([FTy] -> FExpr) -> [FTy] -> FExpr
forall a b. (a -> b) -> a -> b
$ (MTy -> FTy) -> [MTy] -> [FTy]
forall a b. (a -> b) -> [a] -> [b]
map MTy -> FTy
mTyToFTy [MTy]
vs
                             ; Int -> Var -> E ()
log0 Int
l (Var -> E ()) -> Var -> E ()
forall a b. (a -> b) -> a -> b
$ Var
"VAR " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Ctx -> Var
forall a. Show a => a -> Var
show Ctx
g Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
"|- " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FExpr -> Var
forall a. Show a => a -> Var
show FExpr
ret Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" : " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ MTy -> Var
forall a. Show a => a -> Var
show MTy
ret_t
                             ; ADTs -> Ctx -> MTy -> FExpr -> E ()
checkAgainstF ADTs
adts Ctx
g MTy
ret_t FExpr
ret
                             ; (Subst, (MTy, FExpr)) -> M (MTy, FExpr)
forall a. a -> ExceptT Var (State ([Var], Integer)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
idSubst, (MTy
ret_t, FExpr
ret)) }
w Int
l ADTs
adts Ctx
g (App Expr
e0 Expr
e1) = do {
                     ; (Subst
s0, (MTy
t0, FExpr
a)) <- Int -> ADTs -> Ctx -> Expr -> M (MTy, FExpr)
w (Int
lInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ADTs
adts Ctx
g Expr
e0
                     ; (Subst
s1, (MTy
t1, FExpr
b)) <- Int -> ADTs -> Ctx -> Expr -> M (MTy, FExpr)
w (Int
lInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ADTs
adts (Subst -> Ctx -> Ctx
forall a. Substable a => Subst -> a -> a
subst Subst
s0 Ctx
g) Expr
e1
                     ; MTy
t' <- E MTy
fresh
                     ; Subst
s2 <-  (Subst -> MTy -> MTy
forall a. Substable a => Subst -> a -> a
subst Subst
s1 MTy
t0) MTy -> MTy -> E Subst
`mgu` (MTy
t1 MTy -> MTy -> MTy
`TyFn` MTy
t')
                     ; let ret :: FExpr
ret = FExpr -> FExpr -> FExpr
FApp (Subst -> FExpr -> FExpr
forall a. Substable a => Subst -> a -> a
subst (Subst
s2 Subst -> Subst -> Subst
`o` Subst
s1) FExpr
a) (Subst -> FExpr -> FExpr
forall a. Substable a => Subst -> a -> a
subst Subst
s2 FExpr
b)
                           ret_t :: MTy
ret_t = Subst -> MTy -> MTy
forall a. Substable a => Subst -> a -> a
subst Subst
s2 MTy
t'
                           ret_subst :: Subst
ret_subst = Subst
s2 Subst -> Subst -> Subst
`o` (Subst
s1 Subst -> Subst -> Subst
`o` Subst
s0);
                     ; Int -> Var -> E ()
log0 Int
l (Var -> E ()) -> Var -> E ()
forall a b. (a -> b) -> a -> b
$ Var
"APP " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Ctx -> Var
forall a. Show a => a -> Var
show (Subst -> Ctx -> Ctx
forall a. Substable a => Subst -> a -> a
subst Subst
ret_subst Ctx
g) Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
"|- " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FExpr -> Var
forall a. Show a => a -> Var
show FExpr
ret Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" : " Var -> ShowS
forall a. [a] -> [a] -> [a]
++  MTy -> Var
forall a. Show a => a -> Var
show MTy
ret_t
                     ; ADTs -> Ctx -> MTy -> FExpr -> E ()
checkAgainstF ADTs
adts (Subst -> Ctx -> Ctx
forall a. Substable a => Subst -> a -> a
subst Subst
ret_subst Ctx
g) MTy
ret_t FExpr
ret
                     ; (Subst, (MTy, FExpr)) -> M (MTy, FExpr)
forall a. a -> ExceptT Var (State ([Var], Integer)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
ret_subst, (MTy
ret_t, FExpr
ret)) }
w Int
l ADTs
adts Ctx
g (Abs Var
x Expr
e) = do {
                        ; MTy
t  <- E MTy
fresh
                        ; (Subst
ret_subst, (MTy
t', FExpr
a)) <- Int -> ADTs -> Ctx -> Expr -> M (MTy, FExpr)
w (Int
lInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ADTs
adts ((Var
x, ([Var] -> MTy -> TypSch
Forall [] MTy
t))(Var, TypSch) -> Ctx -> Ctx
forall a. a -> [a] -> [a]
:Ctx
g) Expr
e
                        ; let ret :: FExpr
ret = Var -> FTy -> FExpr -> FExpr
FAbs Var
x (MTy -> FTy
mTyToFTy (MTy -> FTy) -> MTy -> FTy
forall a b. (a -> b) -> a -> b
$ Subst -> MTy -> MTy
forall a. Substable a => Subst -> a -> a
subst Subst
ret_subst MTy
t) FExpr
a
                              ret_t :: MTy
ret_t = MTy -> MTy -> MTy
TyFn (Subst -> MTy -> MTy
forall a. Substable a => Subst -> a -> a
subst Subst
ret_subst MTy
t) MTy
t'
                        ; Int -> Var -> E ()
log0 Int
l (Var -> E ()) -> Var -> E ()
forall a b. (a -> b) -> a -> b
$ Var
"ABS " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Ctx -> Var
forall a. Show a => a -> Var
show (Subst -> Ctx -> Ctx
forall a. Substable a => Subst -> a -> a
subst Subst
ret_subst Ctx
g) Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
"|- \\" Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
x Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
". " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FExpr -> Var
forall a. Show a => a -> Var
show FExpr
ret Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" : " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ MTy -> Var
forall a. Show a => a -> Var
show MTy
ret_t
                        ; ADTs -> Ctx -> MTy -> FExpr -> E ()
checkAgainstF ADTs
adts (Subst -> Ctx -> Ctx
forall a. Substable a => Subst -> a -> a
subst Subst
ret_subst Ctx
g) MTy
ret_t FExpr
ret
                        ; (Subst, (MTy, FExpr)) -> M (MTy, FExpr)
forall a. a -> ExceptT Var (State ([Var], Integer)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
ret_subst, (MTy
ret_t, FExpr
ret)) }
w Int
l ADTs
adts Ctx
g (Letrec [(Var, Expr)]
xe0 Expr
e1) = do {
                         ; Subst
t0s <- ((Var, Expr) -> ExceptT Var (State ([Var], Integer)) (Var, MTy))
-> [(Var, Expr)] -> E Subst
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\(Var
k,Expr
v) -> do { MTy
f <- E MTy
fresh; (Var, MTy) -> ExceptT Var (State ([Var], Integer)) (Var, MTy)
forall a. a -> ExceptT Var (State ([Var], Integer)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Var
k, MTy
f) }) [(Var, Expr)]
xe0
                         ; let g' :: Ctx
g' = ((Var, MTy) -> (Var, TypSch)) -> Subst -> Ctx
forall a b. (a -> b) -> [a] -> [b]
map (\(Var
k,MTy
v) -> (Var
k, [Var] -> MTy -> TypSch
Forall [] MTy
v)) Subst
t0s Ctx -> Ctx -> Ctx
forall a. [a] -> [a] -> [a]
++ Ctx
g
                         ; (Subst
s0, ([MTy]
ts,[FExpr]
e0XS)) <- Int
-> Ctx
-> [(Var, Expr)]
-> ExceptT Var (State ([Var], Integer)) (Subst, ([MTy], [FExpr]))
forall {a}.
Int
-> Ctx
-> [(a, Expr)]
-> ExceptT Var (State ([Var], Integer)) (Subst, ([MTy], [FExpr]))
w' (Int
lInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Ctx
g' [(Var, Expr)]
xe0
                         ; Subst
s' <- [MTy] -> [MTy] -> E Subst
mgu' (((Var, MTy) -> MTy) -> Subst -> [MTy]
forall a b. (a -> b) -> [a] -> [b]
map (\(Var
_,MTy
v) -> Subst -> MTy -> MTy
forall a. Substable a => Subst -> a -> a
subst Subst
s0 MTy
v) Subst
t0s) [MTy]
ts
                         ; let g'' :: Ctx
g'' = Subst -> Ctx -> Ctx
forall a. Substable a => Subst -> a -> a
subst (Subst
s' Subst -> Subst -> Subst
`o` Subst
s0) Ctx
g'
                               g''' :: Ctx
g'''  = ((Var, MTy) -> (Var, TypSch)) -> Subst -> Ctx
forall a b. (a -> b) -> [a] -> [b]
map (\(Var
k,MTy
t) -> (Var
k, (TypSch, [Var]) -> TypSch
forall a b. (a, b) -> a
fst ((TypSch, [Var]) -> TypSch) -> (TypSch, [Var]) -> TypSch
forall a b. (a -> b) -> a -> b
$ Ctx -> MTy -> (TypSch, [Var])
gen Ctx
g (Subst -> MTy -> MTy
forall a. Substable a => Subst -> a -> a
subst Subst
s' MTy
t))) (Subst -> Ctx) -> Subst -> Ctx
forall a b. (a -> b) -> a -> b
$ [Var] -> [MTy] -> Subst
forall a b. [a] -> [b] -> [(a, b)]
zip (([Var], [Expr]) -> [Var]
forall a b. (a, b) -> a
fst (([Var], [Expr]) -> [Var]) -> ([Var], [Expr]) -> [Var]
forall a b. (a -> b) -> a -> b
$ [(Var, Expr)] -> ([Var], [Expr])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Var, Expr)]
xe0) [MTy]
ts
                         ; (Subst
s1, (MTy
t',FExpr
e1X)) <- Int -> ADTs -> Ctx -> Expr -> M (MTy, FExpr)
w (Int
lInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ADTs
adts (Ctx
g''') Expr
e1
                         ; let g''X :: [(Var, (TypSch, [Var]))]
g''X = ((Var, MTy) -> (Var, (TypSch, [Var])))
-> Subst -> [(Var, (TypSch, [Var]))]
forall a b. (a -> b) -> [a] -> [b]
map (\(Var
k,MTy
t) -> (Var
k, Ctx -> MTy -> (TypSch, [Var])
gen Ctx
g (Subst -> MTy -> MTy
forall a. Substable a => Subst -> a -> a
subst (Subst
s') MTy
t))) (Subst -> [(Var, (TypSch, [Var]))])
-> Subst -> [(Var, (TypSch, [Var]))]
forall a b. (a -> b) -> a -> b
$ [Var] -> [MTy] -> Subst
forall a b. [a] -> [b] -> [(a, b)]
zip (([Var], [Expr]) -> [Var]
forall a b. (a, b) -> a
fst (([Var], [Expr]) -> [Var]) -> ([Var], [Expr]) -> [Var]
forall a b. (a -> b) -> a -> b
$ [(Var, Expr)] -> ([Var], [Expr])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Var, Expr)]
xe0) [MTy]
ts
                               e0Xs :: [FExpr]
e0Xs = (FExpr -> FExpr) -> [FExpr] -> [FExpr]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> FExpr -> FExpr
forall a. Substable a => Subst -> a -> a
subst (Subst
s1 Subst -> Subst -> Subst
`o` Subst
s')) [FExpr]
e0XS
                               mmm :: [(Var, FExpr)]
mmm = (((Var, (TypSch, [Var])), FExpr) -> (Var, FExpr))
-> [((Var, (TypSch, [Var])), FExpr)] -> [(Var, FExpr)]
forall a b. (a -> b) -> [a] -> [b]
map (\((Var
x,(TypSch
ww,[Var]
ww2)),FExpr
e0X)->(Var
x, (FExpr -> [FTy] -> FExpr
fTyApp (Var -> FExpr
FVar Var
x) ([FTy] -> FExpr) -> [FTy] -> FExpr
forall a b. (a -> b) -> a -> b
$ (Var -> FTy) -> [Var] -> [FTy]
forall a b. (a -> b) -> [a] -> [b]
map Var -> FTy
FTyVar [Var]
ww2))) ([((Var, (TypSch, [Var])), FExpr)] -> [(Var, FExpr)])
-> [((Var, (TypSch, [Var])), FExpr)] -> [(Var, FExpr)]
forall a b. (a -> b) -> a -> b
$  [(Var, (TypSch, [Var]))]
-> [FExpr] -> [((Var, (TypSch, [Var])), FExpr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Var, (TypSch, [Var]))]
g''X [FExpr]
e0Xs
                               e0X's :: [(Var, TypSch, [Var], FExpr)]
e0X's =  (((Var, (TypSch, [Var])), FExpr) -> (Var, TypSch, [Var], FExpr))
-> [((Var, (TypSch, [Var])), FExpr)]
-> [(Var, TypSch, [Var], FExpr)]
forall a b. (a -> b) -> [a] -> [b]
map (\((Var
x,(TypSch
ww,[Var]
ww2)),FExpr
e0X)->(Var
x,TypSch
ww,[Var]
ww2, [(Var, FExpr)] -> FExpr -> FExpr
subst'' [(Var, FExpr)]
mmm FExpr
e0X)) ([((Var, (TypSch, [Var])), FExpr)]
 -> [(Var, TypSch, [Var], FExpr)])
-> [((Var, (TypSch, [Var])), FExpr)]
-> [(Var, TypSch, [Var], FExpr)]
forall a b. (a -> b) -> a -> b
$ [(Var, (TypSch, [Var]))]
-> [FExpr] -> [((Var, (TypSch, [Var])), FExpr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Var, (TypSch, [Var]))]
g''X [FExpr]
e0Xs
                               e0X''s :: [(Var, TypSch, [Var], FExpr)]
e0X''s = ((Var, TypSch, [Var], FExpr) -> (Var, TypSch, [Var], FExpr))
-> [(Var, TypSch, [Var], FExpr)] -> [(Var, TypSch, [Var], FExpr)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Var
x,TypSch
ww,[Var]
ww2,FExpr
e) -> (Var
x,TypSch
ww,[Var]
ww2,[Var] -> FExpr -> FExpr
fTyAbs [Var]
ww2 FExpr
e)) [(Var, TypSch, [Var], FExpr)]
e0X's
                               bs :: [(Var, FTy, FExpr)]
bs = ((Var, TypSch, [Var], FExpr) -> (Var, FTy, FExpr))
-> [(Var, TypSch, [Var], FExpr)] -> [(Var, FTy, FExpr)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Var
x,TypSch
ww,[Var]
ww2,FExpr
e0X'') -> (Var
x, Subst -> FTy -> FTy
forall a. Substable a => Subst -> a -> a
subst Subst
s1 (FTy -> FTy) -> FTy -> FTy
forall a b. (a -> b) -> a -> b
$ TypSch -> FTy
tyToFTy TypSch
ww, Subst -> FExpr -> FExpr
forall a. Substable a => Subst -> a -> a
subst (Subst
s' Subst -> Subst -> Subst
`o` Subst
s1) FExpr
e0X'')) [(Var, TypSch, [Var], FExpr)]
e0X''s
                               ret :: FExpr
ret = [(Var, FTy, FExpr)] -> FExpr -> FExpr
FLetrec [(Var, FTy, FExpr)]
bs FExpr
e1X
                               ret_t :: MTy
ret_t = MTy
t'
                               ret_subst :: Subst
ret_subst = Subst
s1 Subst -> Subst -> Subst
`o` Subst
s' Subst -> Subst -> Subst
`o` Subst
s0
                        ; Int -> Var -> E ()
log0 Int
l (Var -> E ()) -> Var -> E ()
forall a b. (a -> b) -> a -> b
$ Var
"LETREC " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Ctx -> Var
forall a. Show a => a -> Var
show (Subst -> Ctx -> Ctx
forall a. Substable a => Subst -> a -> a
subst Subst
ret_subst Ctx
g) Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
"|- " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FExpr -> Var
forall a. Show a => a -> Var
show FExpr
ret Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
" : " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ MTy -> Var
forall a. Show a => a -> Var
show MTy
ret_t
                        ; ADTs -> Ctx -> MTy -> FExpr -> E ()
checkAgainstF ADTs
adts (Subst -> Ctx -> Ctx
forall a. Substable a => Subst -> a -> a
subst Subst
ret_subst Ctx
g) MTy
ret_t FExpr
ret
                        ; (Subst, (MTy, FExpr)) -> M (MTy, FExpr)
forall a. a -> ExceptT Var (State ([Var], Integer)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
ret_subst, (MTy
ret_t, FExpr
ret)) }
 where w' :: Int
-> Ctx
-> [(a, Expr)]
-> ExceptT Var (State ([Var], Integer)) (Subst, ([MTy], [FExpr]))
w' Int
l Ctx
g [] = (Subst, ([MTy], [FExpr]))
-> ExceptT Var (State ([Var], Integer)) (Subst, ([MTy], [FExpr]))
forall a. a -> ExceptT Var (State ([Var], Integer)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
idSubst, ([], []))
       w' Int
l Ctx
g  ((a
k,Expr
v):[(a, Expr)]
tl) = do { (Subst
u,(MTy
u', FExpr
j)) <- Int -> ADTs -> Ctx -> Expr -> M (MTy, FExpr)
w Int
l ADTs
adts Ctx
g Expr
v
                             ; (Subst
r,([MTy]
r', [FExpr]
h)) <- Int
-> Ctx
-> [(a, Expr)]
-> ExceptT Var (State ([Var], Integer)) (Subst, ([MTy], [FExpr]))
w' Int
l (Subst -> Ctx -> Ctx
forall a. Substable a => Subst -> a -> a
subst Subst
u Ctx
g ) [(a, Expr)]
tl
                             ; (Subst, ([MTy], [FExpr]))
-> ExceptT Var (State ([Var], Integer)) (Subst, ([MTy], [FExpr]))
forall a. a -> ExceptT Var (State ([Var], Integer)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
r Subst -> Subst -> Subst
`o` Subst
u, ((Subst -> MTy -> MTy
forall a. Substable a => Subst -> a -> a
subst Subst
r MTy
u')MTy -> [MTy] -> [MTy]
forall a. a -> [a] -> [a]
:[MTy]
r', (Subst -> FExpr -> FExpr
forall a. Substable a => Subst -> a -> a
subst Subst
r FExpr
j)FExpr -> [FExpr] -> [FExpr]
forall a. a -> [a] -> [a]
:[FExpr]
h)) }


subst'' :: [(Var, FExpr)] -> FExpr -> FExpr
subst'' :: [(Var, FExpr)] -> FExpr -> FExpr
subst'' [(Var, FExpr)]
phi (FTuple [FExpr]
es) = [FExpr] -> FExpr
FTuple ([FExpr] -> FExpr) -> [FExpr] -> FExpr
forall a b. (a -> b) -> a -> b
$ (FExpr -> FExpr) -> [FExpr] -> [FExpr]
forall a b. (a -> b) -> [a] -> [b]
map ([(Var, FExpr)] -> FExpr -> FExpr
subst'' [(Var, FExpr)]
phi) [FExpr]
es
subst'' [(Var, FExpr)]
phi (FConst Prim
c) = Prim -> FExpr
FConst Prim
c
subst'' [(Var, FExpr)]
phi (FVar Var
v') = case Var -> [(Var, FExpr)] -> Maybe FExpr
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Var
v' [(Var, FExpr)]
phi of
                         Just FExpr
y -> FExpr
y
                         Maybe FExpr
Nothing -> Var -> FExpr
FVar Var
v'
subst'' [(Var, FExpr)]
phi (FApp FExpr
a FExpr
b) = FExpr -> FExpr -> FExpr
FApp ([(Var, FExpr)] -> FExpr -> FExpr
subst'' [(Var, FExpr)]
phi FExpr
a) ([(Var, FExpr)] -> FExpr -> FExpr
subst'' [(Var, FExpr)]
phi FExpr
b)
subst'' [(Var, FExpr)]
phi (FAbs Var
v' FTy
a FExpr
b) = Var -> FTy -> FExpr -> FExpr
FAbs Var
v' FTy
a (FExpr -> FExpr) -> FExpr -> FExpr
forall a b. (a -> b) -> a -> b
$ [(Var, FExpr)] -> FExpr -> FExpr
subst'' [(Var, FExpr)]
phi' FExpr
b
 where phi' :: [(Var, FExpr)]
phi' = ((Var, FExpr) -> Bool) -> [(Var, FExpr)] -> [(Var, FExpr)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Var
k,FExpr
v) -> Bool -> Bool
not (Var
k Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
v')) [(Var, FExpr)]
phi
subst'' [(Var, FExpr)]
phi (FTyApp FExpr
a [FTy]
ts) = FExpr -> [FTy] -> FExpr
FTyApp ([(Var, FExpr)] -> FExpr -> FExpr
subst'' [(Var, FExpr)]
phi FExpr
a) [FTy]
ts
subst'' [(Var, FExpr)]
phi (FTyAbs [Var]
vs FExpr
a) = [Var] -> FExpr -> FExpr
FTyAbs [Var]
vs (FExpr -> FExpr) -> FExpr -> FExpr
forall a b. (a -> b) -> a -> b
$ [(Var, FExpr)] -> FExpr -> FExpr
subst'' [(Var, FExpr)]
phi FExpr
a
subst'' [(Var, FExpr)]
phi (FLetrec [(Var, FTy, FExpr)]
es FExpr
e) = [(Var, FTy, FExpr)] -> FExpr -> FExpr
FLetrec (((Var, FTy, FExpr) -> (Var, FTy, FExpr))
-> [(Var, FTy, FExpr)] -> [(Var, FTy, FExpr)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Var
k,FTy
t,FExpr
f)->(Var
k,FTy
t,[(Var, FExpr)] -> FExpr -> FExpr
subst'' [(Var, FExpr)]
phi' FExpr
f)) [(Var, FTy, FExpr)]
es) ([(Var, FExpr)] -> FExpr -> FExpr
subst'' [(Var, FExpr)]
phi' FExpr
e)
 where phi' :: [(Var, FExpr)]
phi' = ((Var, FExpr) -> Bool) -> [(Var, FExpr)] -> [(Var, FExpr)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Var
k,FExpr
v) -> Bool -> Bool
not (Var -> [Var] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Var
k [Var]
ns)) [(Var, FExpr)]
phi
       ([Var]
ns,[FTy]
ts,[FExpr]
es') = [(Var, FTy, FExpr)] -> ([Var], [FTy], [FExpr])
forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 [(Var, FTy, FExpr)]
es

----------------------------------------
-- Main

theAdts :: ADTs
theAdts = ADTs
forall {a}. [(Var, [a], [(Var, [MTy])])]
theAdtsJosh ADTs -> ADTs -> ADTs
forall a. [a] -> [a] -> [a]
++ [(Var
"List", [Var
"t"], [(Var
"Nil", []), (Var
"Cons", [Var -> MTy
TyVar Var
"t", Var -> [MTy] -> MTy
TyCon Var
"List" [Var -> MTy
TyVar Var
"t"]])])]

theAdtsJosh :: [(Var, [a], [(Var, [MTy])])]
theAdtsJosh = [(Var
"LatLon1", [], [(Var
"MkLatLon1", [MTy
natType, MTy
natType])]),
               (Var
"LatLon2", [], [(Var
"MkLatLon2", [MTy
natType, MTy
natType])])]
{--  data LatLon1 = MkLatOn1 Nat Nat where lat1 (MkLatLon1 a) = a and lon1 (MkLatLon1 b) = b and also data LatLon2 = MkLatOn2 Nat Nat where lat2 (MkLatLon2 a ) = a and lon2 (MkLatLon2  b) = --}

testJoshAdt :: Expr
testJoshAdt = [(Var, Expr)] -> Expr -> Expr
Letrec [(Var
"lat1", Expr
lat1)] Expr
body
 where body :: Expr
body = Expr -> Expr -> Expr
App (Expr -> Expr -> Expr
App (Prim -> Expr
Const (Prim -> Expr) -> Prim -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Prim
Con Var
"MkLatLon1") (Int -> Expr
nat Int
0)) (Int -> Expr
nat Int
1)
       lat1 :: Expr
lat1 = Var -> Expr -> Expr
Abs Var
"z" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
App (Expr -> Expr -> Expr
App (Prim -> Expr
Const (Prim -> Expr) -> Prim -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Prim
Fold Var
"LatLon1") (Var -> Expr
Var Var
"z")) (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr -> Expr
Abs Var
"p" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr -> Expr
Abs Var
"q" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ (Var -> Expr
Var Var
"p")

testJoshAdt' :: Expr
testJoshAdt' = [(Var, Expr)] -> Expr -> Expr
Letrec [(Var
"lat1", Expr
lat1)] (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
App (Var -> Expr
Var Var
"lat1") Expr
body
 where body :: Expr
body = Expr -> Expr -> Expr
App (Expr -> Expr -> Expr
App (Prim -> Expr
Const (Prim -> Expr) -> Prim -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Prim
Con Var
"MkLatLon1") (Int -> Expr
nat Int
0)) (Int -> Expr
nat Int
1)
       lat1 :: Expr
lat1 = Var -> Expr -> Expr
Abs Var
"z" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
App (Expr -> Expr -> Expr
App (Prim -> Expr
Const (Prim -> Expr) -> Prim -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Prim
Fold Var
"LatLon1") (Var -> Expr
Var Var
"z")) (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr -> Expr
Abs Var
"p" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr -> Expr
Abs Var
"q" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ (Var -> Expr
Var Var
"p")

tests :: [Expr]
tests = [Expr
testJoshAdt, Expr
testJoshAdt'] -- testVariant2, testTuple2, testVariant, testTuple, test_j_0, test_j_0' , testJ,  test4, testk, testC, testA, test0, test1, testB, test2, test3a, test5, test6]

testk :: Expr
testk = [(Var, Expr)] -> Expr -> Expr
Letrec [(Var
"f", Expr
f), (Var
"g", Expr
g)] Expr
b
 where b :: Expr
b = [Expr] -> Expr
Tuple [(Var -> Expr
Var Var
"f"), (Var -> Expr
Var Var
"g")]
       f :: Expr
f = Var -> Expr -> Expr
Abs Var
"x" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr -> Expr
Abs Var
"y" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
App (Expr -> Expr -> Expr
App (Var -> Expr
Var Var
"g") (Int -> Expr
nat Int
0)) (Var -> Expr
Var Var
"x")
       g :: Expr
g = Var -> Expr -> Expr
Abs Var
"u" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr -> Expr
Abs Var
"v" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
App (Expr -> Expr -> Expr
App (Var -> Expr
Var Var
"f") (Var -> Expr
Var Var
"v")) (Int -> Expr
nat Int
0)

testJ :: Expr
testJ = Var -> Expr -> Expr -> Expr
letrec' Var
"f" Expr
i Expr
b
 where i :: Expr
i = Var -> Expr -> Expr
Abs Var
"x" (Var -> Expr
Var Var
"x")
       b :: Expr
b = Var -> Expr
Var Var
"f"

testAdt :: Expr
testAdt = Var -> Expr -> Expr
Abs Var
"z" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
App (Expr -> Expr -> Expr
App (Expr -> Expr -> Expr
App (Prim -> Expr
Const (Prim -> Expr) -> Prim -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Prim
Fold Var
"List") (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr
Var Var
"z") (Prim -> Expr
Const (Prim -> Expr) -> Prim -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Prim
Con Var
"Nil")) (Prim -> Expr
Const (Prim -> Expr) -> Prim -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Prim
Con Var
"Cons")

testOne :: Expr -> IO ()
testOne Expr
t = do { Var -> IO ()
putStrLn (Var -> IO ()) -> Var -> IO ()
forall a b. (a -> b) -> a -> b
$ Var
"Untyped input: "
               ; Var -> IO ()
putStrLn (Var -> IO ()) -> Var -> IO ()
forall a b. (a -> b) -> a -> b
$ Var
"\t" Var -> ShowS
forall a. [a] -> [a] -> [a]
++  Expr -> Var
forall a. Show a => a -> Var
show Expr
t
               ; let out :: (Either Var (Subst, (MTy, FExpr)), ([Var], Integer))
out = State ([Var], Integer) (Either Var (Subst, (MTy, FExpr)))
-> ([Var], Integer)
-> (Either Var (Subst, (MTy, FExpr)), ([Var], Integer))
forall s a. State s a -> s -> (a, s)
runState (M (MTy, FExpr)
-> State ([Var], Integer) (Either Var (Subst, (MTy, FExpr)))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (Int -> ADTs -> Ctx -> Expr -> M (MTy, FExpr)
w Int
0 ADTs
theAdts [] Expr
t)) ([],Integer
0)
               ; case (Either Var (Subst, (MTy, FExpr)), ([Var], Integer))
-> Either Var (Subst, (MTy, FExpr))
forall a b. (a, b) -> a
fst (Either Var (Subst, (MTy, FExpr)), ([Var], Integer))
out of
                   Left  Var
e -> do { Var -> IO ()
putStrLn (Var -> IO ()) -> Var -> IO ()
forall a b. (a -> b) -> a -> b
$ Var
"\t" Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
"err: " Var -> ShowS
forall a. [a] -> [a] -> [a]
++ Var
e
                                 ; Var -> IO ()
putStrLn (Var -> IO ()) -> Var -> IO ()
forall a b. (a -> b) -> a -> b
$ Var
"\nLog:"
                                 ; (Var -> IO ()) -> [Var] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Var -> IO ()
putStrLn) ([Var] -> IO ()) -> [Var] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Var] -> [Var]
forall a. [a] -> [a]
reverse ([Var] -> [Var]) -> [Var] -> [Var]
forall a b. (a -> b) -> a -> b
$ ([Var], Integer) -> [Var]
forall a b. (a, b) -> a
fst (([Var], Integer) -> [Var]) -> ([Var], Integer) -> [Var]
forall a b. (a -> b) -> a -> b
$ (Either Var (Subst, (MTy, FExpr)), ([Var], Integer))
-> ([Var], Integer)
forall a b. (a, b) -> b
snd (Either Var (Subst, (MTy, FExpr)), ([Var], Integer))
out }
                   Right (Subst
s, (MTy
ty, FExpr
f)) -> do { Var -> IO ()
putStrLn (Var -> IO ()) -> Var -> IO ()
forall a b. (a -> b) -> a -> b
$ Var
"\nType inferred by Hindley-Milner: "
                                            ; Var -> IO ()
putStrLn (Var -> IO ()) -> Var -> IO ()
forall a b. (a -> b) -> a -> b
$ Var
"\t" Var -> ShowS
forall a. [a] -> [a] -> [a]
++ MTy -> Var
forall a. Show a => a -> Var
show MTy
ty
                                            ; Var -> IO ()
putStrLn Var
"\nSystem F translation: "
                                            ; Var -> IO ()
putStrLn (Var -> IO ()) -> Var -> IO ()
forall a b. (a -> b) -> a -> b
$ Var
"\t" Var -> ShowS
forall a. [a] -> [a] -> [a]
++ FExpr -> Var
forall a. Show a => a -> Var
show FExpr
f
                                            -- ; putStrLn "\nLog: "
                                            -- ; mapM_ (putStrLn) $ reverse $ fst $ snd out
                                            }
               ; Var -> IO ()
putStrLn Var
""
               ; Var -> IO ()
putStrLn Var
"------------------------"
               ; Var -> IO ()
putStrLn Var
""  }

main :: IO [()]
main = (Expr -> IO ()) -> [Expr] -> IO [()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Expr -> IO ()
testOne [Expr]
tests

letrec' :: Var -> Expr -> Expr -> Expr
letrec' Var
x Expr
e Expr
f = [(Var, Expr)] -> Expr -> Expr
Letrec [(Var
x,Expr
e)] Expr
f

testVariant :: Expr
testVariant :: Expr
testVariant = Var -> Expr -> Expr
Abs Var
"z" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> [Expr] -> Expr
Case' (Var -> Expr
Var Var
"z") [Expr
f,Expr
g]
 where f :: Expr
f = Var -> Expr -> Expr
Abs Var
"x" {-- $ Inj 0 2 --} (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr
Var Var
"x"
       g :: Expr
g = Var -> Expr -> Expr
Abs Var
"y" {-- $ Inj 1 2 --} (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr
Var Var
"y"
      -- t = Variant [f, g]

testVariant2 :: Expr
testVariant2 :: Expr
testVariant2 = Var -> Expr -> Expr
Abs Var
"z" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> [Expr] -> Expr
Case' (Var -> Expr
Var Var
"z") [Expr
f,Expr
g]
 where f :: Expr
f = Var -> Expr -> Expr
Abs Var
"x" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Expr -> Expr
Inj Int
0 Int
2 (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr
Var Var
"x"
       g :: Expr
g = Var -> Expr -> Expr
Abs Var
"y" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Expr -> Expr
Inj Int
1 Int
2 (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr
Var Var
"y"
      -- t = Variant [f, g]

testTuple2 :: Expr
testTuple2 :: Expr
testTuple2 = Var -> Expr -> Expr
Abs Var
"z" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ [Expr] -> Expr
Tuple [(Int -> Int -> Expr -> Expr
Proj Int
0 Int
2 (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr
Var Var
"z"), (Int -> Int -> Expr -> Expr
Proj Int
1 Int
2 (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr
Var Var
"z")]

testTuple :: Expr
testTuple :: Expr
testTuple = [(Var, Expr)] -> Expr -> Expr
Letrec [(Var
"t", Expr
t)] (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ [Expr] -> Expr
Tuple [Int -> Int -> Expr -> Expr
Proj Int
1 Int
2 (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr
Var Var
"t", Int -> Int -> Expr -> Expr
Proj Int
0 Int
2 (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr
Var Var
"t"]
 where f :: Expr
f = Var -> Expr
str Var
"alice"
       g :: Expr
g = Int -> Expr
nat Int
0
       t :: Expr
t = [Expr] -> Expr
Tuple [Expr
f, Expr
g]


testA :: Expr
testA :: Expr
testA =  Var -> Expr -> Expr -> Expr
letrec' Var
"f" ( (Var -> Expr -> Expr
Abs Var
"x" (Var -> Expr
Var Var
"x"))) (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
App (Var -> Expr
Var Var
"f")  (Int -> Expr
nat Int
0)
 where sng0 :: Expr
sng0 = Expr -> Expr -> Expr
App (Var -> Expr
Var Var
"sng") (Int -> Expr
nat Int
0)
       sngAlice :: Expr
sngAlice = Expr -> Expr -> Expr
App (Var -> Expr
Var Var
"sng") (Var -> Expr
str Var
"alice")
       body :: Expr
body = (Var -> Expr
Var Var
"sng")

test0 :: Expr
test0 :: Expr
test0 =  Var -> Expr -> Expr -> Expr
letrec' Var
"f" (Expr -> Expr -> Expr
App (Var -> Expr -> Expr
Abs Var
"x" (Var -> Expr
Var Var
"x")) (Int -> Expr
nat Int
0)) (Var -> Expr
Var Var
"f")
 where sng0 :: Expr
sng0 = Expr -> Expr -> Expr
App (Var -> Expr
Var Var
"sng") (Int -> Expr
nat Int
0)
       sngAlice :: Expr
sngAlice = Expr -> Expr -> Expr
App (Var -> Expr
Var Var
"sng") (Var -> Expr
str Var
"alice")


testB :: Expr
testB :: Expr
testB = Var -> Expr -> Expr -> Expr
letrec' Var
"sng" (Var -> Expr -> Expr
Abs Var
"x" (Expr -> Expr -> Expr
App (Expr -> Expr -> Expr
App (Prim -> Expr
Const Prim
Cons) (Var -> Expr
Var Var
"x")) (Prim -> Expr
Const Prim
Nil))) Expr
body
 where
       body :: Expr
body = (Var -> Expr
Var Var
"sng")

test1 :: Expr
test1 :: Expr
test1 = Var -> Expr -> Expr -> Expr
letrec' Var
"sng" (Var -> Expr -> Expr
Abs Var
"x" (Expr -> Expr -> Expr
App (Expr -> Expr -> Expr
App (Prim -> Expr
Const Prim
Cons) (Var -> Expr
Var Var
"x")) (Prim -> Expr
Const Prim
Nil))) Expr
body
 where sng0 :: Expr
sng0 = Expr -> Expr -> Expr
App (Var -> Expr
Var Var
"sng") (Int -> Expr
nat Int
0)
       sngAlice :: Expr
sngAlice = Expr -> Expr -> Expr
App (Var -> Expr
Var Var
"sng") (Var -> Expr
str Var
"alice")
       body :: Expr
body = Expr -> Expr -> Expr
App (Expr -> Expr -> Expr
App (Prim -> Expr
Const Prim
Pair) Expr
sng0) Expr
sngAlice

test2 :: Expr
test2 :: Expr
test2 = Var -> Expr -> Expr -> Expr
letrec' Var
"+" (Var -> Expr -> Expr
Abs Var
"x" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr -> Expr
Abs Var
"y" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr
recCall) Expr
twoPlusOne
 where
   recCall :: Expr
recCall = Expr -> Expr -> Expr
App Expr
constSucc (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
App (Expr -> Expr -> Expr
App (Var -> Expr
Var Var
"+") (Expr -> Expr -> Expr
App Expr
constPred (Var -> Expr
Var Var
"x"))) (Var -> Expr
Var Var
"y")
   ifz :: Expr -> Expr -> Expr -> Expr
ifz Expr
x Expr
y Expr
z = Expr -> Expr -> Expr
App (Expr -> Expr -> Expr
App (Expr -> Expr -> Expr
App (Prim -> Expr
Const Prim
If0) Expr
x) Expr
y) Expr
z
   twoPlusOne :: Expr
twoPlusOne = Expr -> Expr -> Expr
App (Expr -> Expr -> Expr
App (Var -> Expr
Var Var
"+") Expr
two) Expr
one
   two :: Expr
two = Expr -> Expr -> Expr
App Expr
constSucc Expr
one
   one :: Expr
one = Expr -> Expr -> Expr
App Expr
constSucc (Int -> Expr
nat Int
0)

testC :: Expr
testC :: Expr
testC = Var -> Expr -> Expr -> Expr
letrec' Var
"+" (Var -> Expr -> Expr
Abs Var
"x" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr -> Expr
Abs Var
"y" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr
recCall) (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr
twoPlusOne
 where
   recCall :: Expr
recCall = Expr -> Expr -> Expr
App Expr
constSucc (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
App (Expr -> Expr -> Expr
App (Var -> Expr
Var Var
"+") (Expr -> Expr -> Expr
App Expr
constPred (Var -> Expr
Var Var
"x"))) ( (Var -> Expr
Var Var
"y"))
   ifz :: Expr -> Expr -> Expr -> Expr
ifz Expr
x Expr
y Expr
z = Expr -> Expr -> Expr
App (Expr -> Expr -> Expr
App (Expr -> Expr -> Expr
App (Prim -> Expr
Const Prim
If0) Expr
x) Expr
y) Expr
z
   twoPlusOne :: Expr
twoPlusOne = Expr -> Expr -> Expr
App (Expr -> Expr -> Expr
App (Var -> Expr
Var Var
"+") Expr
two) Expr
one
   two :: Expr
two = Expr -> Expr -> Expr
App Expr
constSucc Expr
one
   one :: Expr
one = Expr -> Expr -> Expr
App Expr
constSucc (Int -> Expr
nat Int
0)

test3 :: Expr
test3 :: Expr
test3 = Var -> Expr -> Expr -> Expr
letrec' Var
"f" Expr
f Expr
x
 where x :: Expr
x =  (Var -> Expr
Var Var
"f")
       f :: Expr
f = Var -> Expr -> Expr
Abs Var
"x" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr -> Expr
Abs Var
"y" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
App (Expr -> Expr -> Expr
App (Var -> Expr
Var Var
"f") (Int -> Expr
nat Int
0)) (Var -> Expr
Var Var
"x")

test3a :: Expr
test3a :: Expr
test3a = [(Var, Expr)] -> Expr -> Expr
Letrec [(Var
"f", Expr
f), (Var
"g", Expr
g)] Expr
x
 where x :: Expr
x =  Expr -> Expr -> Expr
App (Expr -> Expr -> Expr
App (Prim -> Expr
Const (Prim -> Expr) -> Prim -> Expr
forall a b. (a -> b) -> a -> b
$ Prim
Pair) (Var -> Expr
Var Var
"f")) (Var -> Expr
Var Var
"g")
       f :: Expr
f = Var -> Expr -> Expr
Abs Var
"x" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr -> Expr
Abs Var
"y" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
App (Expr -> Expr -> Expr
App (Var -> Expr
Var Var
"f") (Int -> Expr
nat Int
0)) (Var -> Expr
Var Var
"x")
       g :: Expr
g = Var -> Expr -> Expr
Abs Var
"xx" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr -> Expr
Abs Var
"yy" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
App (Expr -> Expr -> Expr
App (Var -> Expr
Var Var
"g") (Int -> Expr
nat Int
0)) (Var -> Expr
Var Var
"xx")

test4 :: Expr
test4 :: Expr
test4 = [(Var, Expr)] -> Expr -> Expr
Letrec [(Var
"f", Expr
f), (Var
"g", Expr
g)] Expr
b
 where b :: Expr
b = Expr -> Expr -> Expr
App (Expr -> Expr -> Expr
App (Prim -> Expr
Const Prim
Pair) (Var -> Expr
Var Var
"f")) (Var -> Expr
Var Var
"g")
       f :: Expr
f = Var -> Expr -> Expr
Abs Var
"x" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr -> Expr
Abs Var
"y" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
App (Expr -> Expr -> Expr
App (Var -> Expr
Var Var
"g") (Int -> Expr
nat Int
0)) (Var -> Expr
Var Var
"x")
       g :: Expr
g = Var -> Expr -> Expr
Abs Var
"u" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr -> Expr
Abs Var
"v" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
App (Expr -> Expr -> Expr
App (Var -> Expr
Var Var
"f") (Var -> Expr
Var Var
"v")) (Int -> Expr
nat Int
0)

test5 :: Expr
test5 :: Expr
test5 = [(Var, Expr)] -> Expr -> Expr
Letrec [(Var
"f", Expr
f), (Var
"g", Expr
g)] Expr
b
 where b :: Expr
b = Expr -> Expr -> Expr
App (Expr -> Expr -> Expr
App (Prim -> Expr
Const Prim
Pair) (Var -> Expr
Var Var
"f")) (Var -> Expr
Var Var
"g")
       f :: Expr
f = Var -> Expr -> Expr
Abs Var
"x" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr -> Expr
Abs Var
"y" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
App (Expr -> Expr -> Expr
App (Var -> Expr
Var Var
"g") (Int -> Expr
nat Int
0)) (Int -> Expr
nat Int
0)
       g :: Expr
g = Var -> Expr -> Expr
Abs Var
"u" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr -> Expr
Abs Var
"v" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
App (Expr -> Expr -> Expr
App (Var -> Expr
Var Var
"f") (Var -> Expr
Var Var
"v")) (Int -> Expr
nat Int
0)


test6 :: Expr
test6 :: Expr
test6 = [(Var, Expr)] -> Expr -> Expr
Letrec [(Var
"f", Expr
f), (Var
"g", Expr
g)] Expr
b
 where b :: Expr
b = Expr -> Expr -> Expr
App (Expr -> Expr -> Expr
App (Prim -> Expr
Const Prim
Pair) (Var -> Expr
Var Var
"f")) (Var -> Expr
Var Var
"g")
       f :: Expr
f = Var -> Expr -> Expr
Abs Var
"x" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr -> Expr
Abs Var
"y" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
App (Expr -> Expr -> Expr
App (Var -> Expr
Var Var
"g") (Int -> Expr
nat Int
0)) (Var -> Expr
Var Var
"x")
       g :: Expr
g = Var -> Expr -> Expr
Abs Var
"u" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr -> Expr
Abs Var
"v" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
App (Expr -> Expr -> Expr
App (Var -> Expr
Var Var
"f") (Int -> Expr
nat Int
0)) (Int -> Expr
nat Int
0)


Expr
x @@ :: Expr -> Expr -> Expr
@@ Expr
y = Expr -> Expr -> Expr
App Expr
x Expr
y
zero :: Expr
zero = Int -> Expr
nat Int
0

test_j_o_haskell :: a -> a -> [([a], [a])]
test_j_o_haskell = a -> a -> [([a], [a])]
forall {a} {a}. a -> a -> [([a], [a])]
f
  where
    sng :: a -> [a]
sng = \a
x -> [a
x]
    f :: a -> a -> [([a], [a])]
f = \a
x a
y -> (a -> [a]
forall {a}. a -> [a]
sng a
x, a -> [a]
forall {a}. a -> [a]
sng a
y)([a], [a]) -> [([a], [a])] -> [([a], [a])]
forall a. a -> [a] -> [a]
: []
    g :: p -> a -> [([Integer], [a])]
g = \p
x a
y -> Integer -> a -> [([Integer], [a])]
forall {a} {a}. a -> a -> [([a], [a])]
f Integer
0 a
y

-- @joshsh's additional test cases
test_j_0 :: Expr
test_j_0 :: Expr
test_j_0 = [(Var, Expr)] -> Expr -> Expr
Letrec [(Var
"singleton", Expr
singleton), (Var
"f", Expr
f), (Var
"g", Expr
g)] (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr
Var Var
"f"
  where
    singleton :: Expr
singleton = Var -> Expr -> Expr
Abs Var
"x" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Prim -> Expr
Const Prim
Cons Expr -> Expr -> Expr
@@ Var -> Expr
Var Var
"x" Expr -> Expr -> Expr
@@ Prim -> Expr
Const Prim
Nil
    f :: Expr
f = Var -> Expr -> Expr
Abs Var
"x" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr -> Expr
Abs Var
"y" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Prim -> Expr
Const Prim
Cons
      Expr -> Expr -> Expr
@@ (Prim -> Expr
Const Prim
Pair
        Expr -> Expr -> Expr
@@ (Var -> Expr
Var Var
"singleton" Expr -> Expr -> Expr
@@ Var -> Expr
Var Var
"x")
        Expr -> Expr -> Expr
@@ (Var -> Expr
Var Var
"singleton" Expr -> Expr -> Expr
@@ Var -> Expr
Var Var
"y"))
      Expr -> Expr -> Expr
@@ (Var -> Expr
Var Var
"g" Expr -> Expr -> Expr
@@ Var -> Expr
Var Var
"x" Expr -> Expr -> Expr
@@ Var -> Expr
Var Var
"y")
    g :: Expr
g = Var -> Expr -> Expr
Abs Var
"x" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr -> Expr
Abs Var
"y" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr
Var Var
"f" Expr -> Expr -> Expr
@@ Expr
zero Expr -> Expr -> Expr
@@ Var -> Expr
Var Var
"y"

test_j_0' :: Expr
test_j_0' :: Expr
test_j_0' = [(Var, Expr)] -> Expr -> Expr
Letrec [(Var
"singleton", Expr
singleton)] (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$
 [(Var, Expr)] -> Expr -> Expr
Letrec [(Var
"f", Expr
f), (Var
"g", Expr
g)] (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr
Var Var
"f"
  where
    singleton :: Expr
singleton = Var -> Expr -> Expr
Abs Var
"x" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Prim -> Expr
Const Prim
Cons Expr -> Expr -> Expr
@@ Var -> Expr
Var Var
"x" Expr -> Expr -> Expr
@@ Prim -> Expr
Const Prim
Nil
    f :: Expr
f = Var -> Expr -> Expr
Abs Var
"x" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr -> Expr
Abs Var
"y" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Prim -> Expr
Const Prim
Cons
      Expr -> Expr -> Expr
@@ (Prim -> Expr
Const Prim
Pair
        Expr -> Expr -> Expr
@@ (Var -> Expr
Var Var
"singleton" Expr -> Expr -> Expr
@@ Var -> Expr
Var Var
"x")
        Expr -> Expr -> Expr
@@ (Var -> Expr
Var Var
"singleton" Expr -> Expr -> Expr
@@ Var -> Expr
Var Var
"y"))
      Expr -> Expr -> Expr
@@ (Var -> Expr
Var Var
"g" Expr -> Expr -> Expr
@@ Var -> Expr
Var Var
"x" Expr -> Expr -> Expr
@@ Var -> Expr
Var Var
"y")
    g :: Expr
g = Var -> Expr -> Expr
Abs Var
"x" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr -> Expr
Abs Var
"y" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr
Var Var
"f" Expr -> Expr -> Expr
@@ Expr
zero Expr -> Expr -> Expr
@@ Var -> Expr
Var Var
"y"

--test_j_0 :: Expr
--test_j_0 = Let "id" i $ f
  --where
   -- i = Abs "z" $ Var "z"
   -- f = Abs "p0" $
     --  (Const Pair)
       -- @@ (Var "id" @@ Var "p0")
       -- @@ (Var "p0")