summaryrefslogtreecommitdiff
path: root/utils/ext-core
diff options
context:
space:
mode:
Diffstat (limited to 'utils/ext-core')
-rw-r--r--utils/ext-core/Check.hs421
-rw-r--r--utils/ext-core/Core.hs150
-rw-r--r--utils/ext-core/Driver.hs86
-rw-r--r--utils/ext-core/Env.hs44
-rw-r--r--utils/ext-core/Interp.hs450
-rw-r--r--utils/ext-core/Lex.hs92
-rw-r--r--utils/ext-core/ParseGlue.hs65
-rw-r--r--utils/ext-core/Parser.y230
-rw-r--r--utils/ext-core/Prep.hs151
-rw-r--r--utils/ext-core/Prims.hs834
-rw-r--r--utils/ext-core/Printer.hs163
-rw-r--r--utils/ext-core/README9
12 files changed, 2695 insertions, 0 deletions
diff --git a/utils/ext-core/Check.hs b/utils/ext-core/Check.hs
new file mode 100644
index 0000000000..a9a3eac8f4
--- /dev/null
+++ b/utils/ext-core/Check.hs
@@ -0,0 +1,421 @@
+module Check where
+
+import Monad
+import Core
+import Printer
+import List
+import Env
+
+{- Checking is done in a simple error monad. In addition to
+ allowing errors to be captured, this makes it easy to guarantee
+ that checking itself has been completed for an entire module. -}
+
+data CheckResult a = OkC a | FailC String
+
+instance Monad CheckResult where
+ OkC a >>= k = k a
+ FailC s >>= k = fail s
+ return = OkC
+ fail = FailC
+
+require :: Bool -> String -> CheckResult ()
+require False s = fail s
+require True _ = return ()
+
+requireM :: CheckResult Bool -> String -> CheckResult ()
+requireM cond s =
+ do b <- cond
+ require b s
+
+{- Environments. -}
+type Tvenv = Env Tvar Kind -- type variables (local only)
+type Tcenv = Env Tcon Kind -- type constructors
+type Tsenv = Env Tcon ([Tvar],Ty) -- type synonyms
+type Cenv = Env Dcon Ty -- data constructors
+type Venv = Env Var Ty -- values
+type Menv = Env Mname Envs -- modules
+data Envs = Envs {tcenv_::Tcenv,tsenv_::Tsenv,cenv_::Cenv,venv_::Venv} -- all the exportable envs
+
+{- Extend an environment, checking for illegal shadowing of identifiers. -}
+extendM :: (Ord a, Show a) => Env a b -> (a,b) -> CheckResult (Env a b)
+extendM env (k,d) =
+ case elookup env k of
+ Just _ -> fail ("multiply-defined identifier: " ++ show k)
+ Nothing -> return (eextend env (k,d))
+
+lookupM :: (Ord a, Show a) => Env a b -> a -> CheckResult b
+lookupM env k =
+ case elookup env k of
+ Just v -> return v
+ Nothing -> fail ("undefined identifier: " ++ show k)
+
+{- Main entry point. -}
+checkModule :: Menv -> Module -> CheckResult Menv
+checkModule globalEnv (Module mn tdefs vdefgs) =
+ do (tcenv,tsenv) <- foldM checkTdef0 (eempty,eempty) tdefs
+ cenv <- foldM (checkTdef tcenv) eempty tdefs
+ (e_venv,l_venv) <- foldM (checkVdefg True (tcenv,tsenv,eempty,cenv)) (eempty,eempty) vdefgs
+ return (eextend globalEnv (mn,Envs{tcenv_=tcenv,tsenv_=tsenv,cenv_=cenv,venv_=e_venv}))
+ where
+
+ checkTdef0 :: (Tcenv,Tsenv) -> Tdef -> CheckResult (Tcenv,Tsenv)
+ checkTdef0 (tcenv,tsenv) tdef = ch tdef
+ where
+ ch (Data (m,c) tbs _) =
+ do require (m == mn) ("wrong module name in data type declaration:\n" ++ show tdef)
+ tcenv' <- extendM tcenv (c,k)
+ return (tcenv',tsenv)
+ where k = foldr Karrow Klifted (map snd tbs)
+ ch (Newtype (m,c) tbs rhs) =
+ do require (m == mn) ("wrong module name in newtype declaration:\n" ++ show tdef)
+ tcenv' <- extendM tcenv (c,k)
+ tsenv' <- case rhs of
+ Nothing -> return tsenv
+ Just rep -> extendM tsenv (c,(map fst tbs,rep))
+ return (tcenv', tsenv')
+ where k = foldr Karrow Klifted (map snd tbs)
+
+ checkTdef :: Tcenv -> Cenv -> Tdef -> CheckResult Cenv
+ checkTdef tcenv cenv = ch
+ where
+ ch (Data (_,c) utbs cdefs) =
+ do cbinds <- mapM checkCdef cdefs
+ foldM extendM cenv cbinds
+ where checkCdef (cdef@(Constr (m,dcon) etbs ts)) =
+ do require (m == mn) ("wrong module name in constructor declaration:\n" ++ show cdef)
+ tvenv <- foldM extendM eempty tbs
+ ks <- mapM (checkTy (tcenv,tvenv)) ts
+ mapM_ (\k -> require (baseKind k)
+ ("higher-order kind in:\n" ++ show cdef ++ "\n" ++
+ "kind: " ++ show k) ) ks
+ return (dcon,t)
+ where tbs = utbs ++ etbs
+ t = foldr Tforall
+ (foldr tArrow
+ (foldl Tapp (Tcon (mn,c))
+ (map (Tvar . fst) utbs)) ts) tbs
+ ch (tdef@(Newtype c tbs (Just t))) =
+ do tvenv <- foldM extendM eempty tbs
+ k <- checkTy (tcenv,tvenv) t
+ require (k==Klifted) ("bad kind:\n" ++ show tdef)
+ return cenv
+ ch (tdef@(Newtype c tbs Nothing)) =
+ {- should only occur for recursive Newtypes -}
+ return cenv
+
+
+ checkVdefg :: Bool -> (Tcenv,Tsenv,Tvenv,Cenv) -> (Venv,Venv) -> Vdefg -> CheckResult (Venv,Venv)
+ checkVdefg top_level (tcenv,tsenv,tvenv,cenv) (e_venv,l_venv) vdefg =
+ case vdefg of
+ Rec vdefs ->
+ do e_venv' <- foldM extendM e_venv e_vts
+ l_venv' <- foldM extendM l_venv l_vts
+ let env' = (tcenv,tsenv,tvenv,cenv,e_venv',l_venv')
+ mapM_ (\ (vdef@(Vdef ((m,v),t,e))) ->
+ do require (m == "" || m == mn) ("wrong module name in value definition:\n" ++ show vdef)
+ k <- checkTy (tcenv,tvenv) t
+ require (k==Klifted) ("unlifted kind in:\n" ++ show vdef)
+ t' <- checkExp env' e
+ requireM (equalTy tsenv t t')
+ ("declared type doesn't match expression type in:\n" ++ show vdef ++ "\n" ++
+ "declared type: " ++ show t ++ "\n" ++
+ "expression type: " ++ show t')) vdefs
+ return (e_venv',l_venv')
+ where e_vts = [ (v,t) | Vdef ((m,v),t,_) <- vdefs, m /= "" ]
+ l_vts = [ (v,t) | Vdef (("",v),t,_) <- vdefs]
+ Nonrec (vdef@(Vdef ((m,v),t,e))) ->
+ do require (m == "" || m == mn) ("wrong module name in value definition:\n" ++ show vdef)
+ k <- checkTy (tcenv,tvenv) t
+ require (k /= Kopen) ("open kind in:\n" ++ show vdef)
+ require ((not top_level) || (k /= Kunlifted)) ("top-level unlifted kind in:\n" ++ show vdef)
+ t' <- checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) e
+ requireM (equalTy tsenv t t')
+ ("declared type doesn't match expression type in:\n" ++ show vdef ++ "\n" ++
+ "declared type: " ++ show t ++ "\n" ++
+ "expression type: " ++ show t')
+ if m == "" then
+ do l_venv' <- extendM l_venv (v,t)
+ return (e_venv,l_venv')
+ else
+ do e_venv' <- extendM e_venv (v,t)
+ return (e_venv',l_venv)
+
+ checkExp :: (Tcenv,Tsenv,Tvenv,Cenv,Venv,Venv) -> Exp -> CheckResult Ty
+ checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) = ch
+ where
+ ch e0 =
+ case e0 of
+ Var qv ->
+ qlookupM venv_ e_venv l_venv qv
+ Dcon qc ->
+ qlookupM cenv_ cenv eempty qc
+ Lit l ->
+ checkLit l
+ Appt e t ->
+ do t' <- ch e
+ k' <- checkTy (tcenv,tvenv) t
+ case t' of
+ Tforall (tv,k) t0 ->
+ do require (k' <= k)
+ ("kind doesn't match at type application in:\n" ++ show e0 ++ "\n" ++
+ "operator kind: " ++ show k ++ "\n" ++
+ "operand kind: " ++ show k')
+ return (substl [tv] [t] t0)
+ _ -> fail ("bad operator type in type application:\n" ++ show e0 ++ "\n" ++
+ "operator type: " ++ show t')
+ App e1 e2 ->
+ do t1 <- ch e1
+ t2 <- ch e2
+ case t1 of
+ Tapp(Tapp(Tcon tc) t') t0 | tc == tcArrow ->
+ do requireM (equalTy tsenv t2 t')
+ ("type doesn't match at application in:\n" ++ show e0 ++ "\n" ++
+ "operator type: " ++ show t' ++ "\n" ++
+ "operand type: " ++ show t2)
+ return t0
+ _ -> fail ("bad operator type at application in:\n" ++ show e0 ++ "\n" ++
+ "operator type: " ++ show t1)
+ Lam (Tb tb) e ->
+ do tvenv' <- extendM tvenv tb
+ t <- checkExp (tcenv,tsenv,tvenv',cenv,e_venv,l_venv) e
+ return (Tforall tb t)
+ Lam (Vb (vb@(_,vt))) e ->
+ do k <- checkTy (tcenv,tvenv) vt
+ require (baseKind k)
+ ("higher-order kind in:\n" ++ show e0 ++ "\n" ++
+ "kind: " ++ show k)
+ l_venv' <- extendM l_venv vb
+ t <- checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv') e
+ require (not (isUtupleTy vt)) ("lambda-bound unboxed tuple in:\n" ++ show e0)
+ return (tArrow vt t)
+ Let vdefg e ->
+ do (e_venv',l_venv') <- checkVdefg False (tcenv,tsenv,tvenv,cenv) (e_venv,l_venv) vdefg
+ checkExp (tcenv,tsenv,tvenv,cenv,e_venv',l_venv') e
+ Case e (v,t) alts ->
+ do t' <- ch e
+ checkTy (tcenv,tvenv) t
+ requireM (equalTy tsenv t t')
+ ("scrutinee declared type doesn't match expression type in:\n" ++ show e0 ++ "\n" ++
+ "declared type: " ++ show t ++ "\n" ++
+ "expression type: " ++ show t')
+ case (reverse alts) of
+ (Acon c _ _ _):as ->
+ let ok ((Acon c _ _ _):as) cs = do require (notElem c cs)
+ ("duplicate alternative in case:\n" ++ show e0)
+ ok as (c:cs)
+ ok ((Alit _ _):_) _ = fail ("invalid alternative in constructor case:\n" ++ show e0)
+ ok [Adefault _] _ = return ()
+ ok (Adefault _:_) _ = fail ("misplaced default alternative in case:\n" ++ show e0)
+ ok [] _ = return ()
+ in ok as [c]
+ (Alit l _):as ->
+ let ok ((Acon _ _ _ _):_) _ = fail ("invalid alternative in literal case:\n" ++ show e0)
+ ok ((Alit l _):as) ls = do require (notElem l ls)
+ ("duplicate alternative in case:\n" ++ show e0)
+ ok as (l:ls)
+ ok [Adefault _] _ = return ()
+ ok (Adefault _:_) _ = fail ("misplaced default alternative in case:\n" ++ show e0)
+ ok [] _ = fail ("missing default alternative in literal case:\n" ++ show e0)
+ in ok as [l]
+ [Adefault _] -> return ()
+ [] -> fail ("no alternatives in case:\n" ++ show e0)
+ l_venv' <- extendM l_venv (v,t)
+ t:ts <- mapM (checkAlt (tcenv,tsenv,tvenv,cenv,e_venv,l_venv') t) alts
+ bs <- mapM (equalTy tsenv t) ts
+ require (and bs)
+ ("alternative types don't match in:\n" ++ show e0 ++ "\n" ++
+ "types: " ++ show (t:ts))
+ return t
+ Coerce t e ->
+ do ch e
+ checkTy (tcenv,tvenv) t
+ return t
+ Note s e ->
+ ch e
+ External _ t ->
+ do checkTy (tcenv,eempty) t {- external types must be closed -}
+ return t
+
+ checkAlt :: (Tcenv,Tsenv,Tvenv,Cenv,Venv,Venv) -> Ty -> Alt -> CheckResult Ty
+ checkAlt (env@(tcenv,tsenv,tvenv,cenv,e_venv,l_venv)) t0 = ch
+ where
+ ch a0 =
+ case a0 of
+ Acon qc etbs vbs e ->
+ do let uts = f t0
+ where f (Tapp t0 t) = f t0 ++ [t]
+ f _ = []
+ ct <- qlookupM cenv_ cenv eempty qc
+ let (tbs,ct_args0,ct_res0) = splitTy ct
+ {- get universals -}
+ let (utbs,etbs') = splitAt (length uts) tbs
+ let utvs = map fst utbs
+ {- check existentials -}
+ let (etvs,eks) = unzip etbs
+ let (etvs',eks') = unzip etbs'
+ require (eks == eks')
+ ("existential kinds don't match in:\n" ++ show a0 ++ "\n" ++
+ "kinds declared in data constructor: " ++ show eks ++
+ "kinds declared in case alternative: " ++ show eks')
+ tvenv' <- foldM extendM tvenv etbs
+ {- check term variables -}
+ let vts = map snd vbs
+ mapM_ (\vt -> require ((not . isUtupleTy) vt)
+ ("pattern-bound unboxed tuple in:\n" ++ show a0 ++ "\n" ++
+ "pattern type: " ++ show vt)) vts
+ vks <- mapM (checkTy (tcenv,tvenv')) vts
+ mapM_ (\vk -> require (baseKind vk)
+ ("higher-order kind in:\n" ++ show a0 ++ "\n" ++
+ "kind: " ++ show vk)) vks
+ let (ct_res:ct_args) = map (substl (utvs++etvs') (uts++(map Tvar etvs))) (ct_res0:ct_args0)
+ zipWithM_
+ (\ct_arg vt ->
+ requireM (equalTy tsenv ct_arg vt)
+ ("pattern variable type doesn't match constructor argument type in:\n" ++ show a0 ++ "\n" ++
+ "pattern variable type: " ++ show ct_arg ++ "\n" ++
+ "constructor argument type: " ++ show vt)) ct_args vts
+ requireM (equalTy tsenv ct_res t0)
+ ("pattern constructor type doesn't match scrutinee type in:\n" ++ show a0 ++ "\n" ++
+ "pattern constructor type: " ++ show ct_res ++ "\n" ++
+ "scrutinee type: " ++ show t0)
+ l_venv' <- foldM extendM l_venv vbs
+ t <- checkExp (tcenv,tsenv,tvenv',cenv,e_venv,l_venv') e
+ checkTy (tcenv,tvenv) t {- check that existentials don't escape in result type -}
+ return t
+ Alit l e ->
+ do t <- checkLit l
+ requireM (equalTy tsenv t t0)
+ ("pattern type doesn't match scrutinee type in:\n" ++ show a0 ++ "\n" ++
+ "pattern type: " ++ show t ++ "\n" ++
+ "scrutinee type: " ++ show t0)
+ checkExp env e
+ Adefault e ->
+ checkExp env e
+
+ checkTy :: (Tcenv,Tvenv) -> Ty -> CheckResult Kind
+ checkTy (tcenv,tvenv) = ch
+ where
+ ch (Tvar tv) = lookupM tvenv tv
+ ch (Tcon qtc) = qlookupM tcenv_ tcenv eempty qtc
+ ch (t@(Tapp t1 t2)) =
+ do k1 <- ch t1
+ k2 <- ch t2
+ case k1 of
+ Karrow k11 k12 ->
+ do require (k2 <= k11)
+ ("kinds don't match in type application: " ++ show t ++ "\n" ++
+ "operator kind: " ++ show k11 ++ "\n" ++
+ "operand kind: " ++ show k2)
+ return k12
+ _ -> fail ("applied type has non-arrow kind: " ++ show t)
+ ch (Tforall tb t) =
+ do tvenv' <- extendM tvenv tb
+ checkTy (tcenv,tvenv') t
+
+ {- Type equality modulo newtype synonyms. -}
+ equalTy :: Tsenv -> Ty -> Ty -> CheckResult Bool
+ equalTy tsenv t1 t2 =
+ do t1' <- expand t1
+ t2' <- expand t2
+ return (t1' == t2')
+ where expand (Tvar v) = return (Tvar v)
+ expand (Tcon qtc) = return (Tcon qtc)
+ expand (Tapp t1 t2) =
+ do t2' <- expand t2
+ expapp t1 [t2']
+ expand (Tforall tb t) =
+ do t' <- expand t
+ return (Tforall tb t')
+ expapp (t@(Tcon (m,tc))) ts =
+ do env <- mlookupM tsenv_ tsenv eempty m
+ case elookup env tc of
+ Just (formals,rhs) | (length formals) == (length ts) -> return (substl formals ts rhs)
+ _ -> return (foldl Tapp t ts)
+ expapp (Tapp t1 t2) ts =
+ do t2' <- expand t2
+ expapp t1 (t2':ts)
+ expapp t ts =
+ do t' <- expand t
+ return (foldl Tapp t' ts)
+
+
+ mlookupM :: (Envs -> Env a b) -> Env a b -> Env a b -> Mname -> CheckResult (Env a b)
+ mlookupM selector external_env local_env m =
+ if m == "" then
+ return local_env
+ else if m == mn then
+ return external_env
+ else
+ case elookup globalEnv m of
+ Just env' -> return (selector env')
+ Nothing -> fail ("undefined module name: " ++ show m)
+
+ qlookupM :: (Ord a, Show a) => (Envs -> Env a b) -> Env a b -> Env a b -> (Mname,a) -> CheckResult b
+ qlookupM selector external_env local_env (m,k) =
+ do env <- mlookupM selector external_env local_env m
+ lookupM env k
+
+
+checkLit :: Lit -> CheckResult Ty
+checkLit lit =
+ case lit of
+ Lint _ t ->
+ do {- require (elem t [tIntzh, {- tInt32zh,tInt64zh, -} tWordzh, {- tWord32zh,tWord64zh, -} tAddrzh, tCharzh])
+ ("invalid int literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) -}
+ return t
+ Lrational _ t ->
+ do {- require (elem t [tFloatzh,tDoublezh])
+ ("invalid rational literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) -}
+ return t
+ Lchar _ t ->
+ do {- require (t == tCharzh)
+ ("invalid char literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) -}
+ return t
+ Lstring _ t ->
+ do {- require (t == tAddrzh)
+ ("invalid string literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) -}
+ return t
+
+{- Utilities -}
+
+{- Split off tbs, arguments and result of a (possibly abstracted) arrow type -}
+splitTy :: Ty -> ([Tbind],[Ty],Ty)
+splitTy (Tforall tb t) = (tb:tbs,ts,tr)
+ where (tbs,ts,tr) = splitTy t
+splitTy (Tapp(Tapp(Tcon tc) t0) t) | tc == tcArrow = (tbs,t0:ts,tr)
+ where (tbs,ts,tr) = splitTy t
+splitTy t = ([],[],t)
+
+
+{- Simultaneous substitution on types for type variables,
+ renaming as neceessary to avoid capture.
+ No checks for correct kindedness. -}
+substl :: [Tvar] -> [Ty] -> Ty -> Ty
+substl tvs ts t = f (zip tvs ts) t
+ where
+ f env t0 =
+ case t0 of
+ Tcon _ -> t0
+ Tvar v -> case lookup v env of
+ Just t1 -> t1
+ Nothing -> t0
+ Tapp t1 t2 -> Tapp (f env t1) (f env t2)
+ Tforall (t,k) t1 ->
+ if t `elem` free then
+ Tforall (t',k) (f ((t,Tvar t'):env) t1)
+ else
+ Tforall (t,k) (f (filter ((/=t).fst) env) t1)
+ where free = foldr union [] (map (freeTvars.snd) env)
+ t' = freshTvar free
+
+{- Return free tvars in a type -}
+freeTvars :: Ty -> [Tvar]
+freeTvars (Tcon _) = []
+freeTvars (Tvar v) = [v]
+freeTvars (Tapp t1 t2) = (freeTvars t1) `union` (freeTvars t2)
+freeTvars (Tforall (t,_) t1) = delete t (freeTvars t1)
+
+{- Return any tvar *not* in the argument list. -}
+freshTvar :: [Tvar] -> Tvar
+freshTvar tvs = maximum ("":tvs) ++ "x" -- one simple way!
+
diff --git a/utils/ext-core/Core.hs b/utils/ext-core/Core.hs
new file mode 100644
index 0000000000..2f94f80b3e
--- /dev/null
+++ b/utils/ext-core/Core.hs
@@ -0,0 +1,150 @@
+module Core where
+
+import List (elemIndex)
+
+data Module
+ = Module Mname [Tdef] [Vdefg]
+
+data Tdef
+ = Data (Qual Tcon) [Tbind] [Cdef]
+ | Newtype (Qual Tcon) [Tbind] (Maybe Ty)
+
+data Cdef
+ = Constr (Qual Dcon) [Tbind] [Ty]
+
+data Vdefg
+ = Rec [Vdef]
+ | Nonrec Vdef
+
+newtype Vdef = Vdef (Qual Var,Ty,Exp)
+
+data Exp
+ = Var (Qual Var)
+ | Dcon (Qual Dcon)
+ | Lit Lit
+ | App Exp Exp
+ | Appt Exp Ty
+ | Lam Bind Exp
+ | Let Vdefg Exp
+ | Case Exp Vbind [Alt] {- non-empty list -}
+ | Coerce Ty Exp
+ | Note String Exp
+ | External String Ty
+
+data Bind
+ = Vb Vbind
+ | Tb Tbind
+
+data Alt
+ = Acon (Qual Dcon) [Tbind] [Vbind] Exp
+ | Alit Lit Exp
+ | Adefault Exp
+
+type Vbind = (Var,Ty)
+type Tbind = (Tvar,Kind)
+
+data Ty
+ = Tvar Tvar
+ | Tcon (Qual Tcon)
+ | Tapp Ty Ty
+ | Tforall Tbind Ty
+
+data Kind
+ = Klifted
+ | Kunlifted
+ | Kopen
+ | Karrow Kind Kind
+ deriving (Eq)
+
+data Lit
+ = Lint Integer Ty
+ | Lrational Rational Ty
+ | Lchar Char Ty
+ | Lstring String Ty
+ deriving (Eq) -- with nearlyEqualTy
+
+type Mname = Id
+type Var = Id
+type Tvar = Id
+type Tcon = Id
+type Dcon = Id
+
+type Qual t = (Mname,t)
+
+type Id = String
+
+{- Doesn't expand out fully applied newtype synonyms
+ (for which an environment is needed). -}
+nearlyEqualTy t1 t2 = eqTy [] [] t1 t2
+ where eqTy e1 e2 (Tvar v1) (Tvar v2) =
+ case (elemIndex v1 e1,elemIndex v2 e2) of
+ (Just i1, Just i2) -> i1 == i2
+ (Nothing, Nothing) -> v1 == v2
+ _ -> False
+ eqTy e1 e2 (Tcon c1) (Tcon c2) = c1 == c2
+ eqTy e1 e2 (Tapp t1a t1b) (Tapp t2a t2b) =
+ eqTy e1 e2 t1a t2a && eqTy e1 e2 t1b t2b
+ eqTy e1 e2 (Tforall (tv1,tk1) t1) (Tforall (tv2,tk2) t2) =
+ tk1 == tk2 && eqTy (tv1:e1) (tv2:e2) t1 t2
+ eqTy _ _ _ _ = False
+instance Eq Ty where (==) = nearlyEqualTy
+
+
+subKindOf :: Kind -> Kind -> Bool
+_ `subKindOf` Kopen = True
+k1 `subKindOf` k2 = k1 == k2 -- doesn't worry about higher kinds
+
+instance Ord Kind where (<=) = subKindOf
+
+baseKind :: Kind -> Bool
+baseKind (Karrow _ _ ) = False
+baseKind _ = True
+
+primMname = "PrelGHC"
+
+tcArrow :: Qual Tcon
+tcArrow = (primMname, "ZLzmzgZR")
+
+tArrow :: Ty -> Ty -> Ty
+tArrow t1 t2 = Tapp (Tapp (Tcon tcArrow) t1) t2
+
+ktArrow :: Kind
+ktArrow = Karrow Kopen (Karrow Kopen Klifted)
+
+{- Unboxed tuples -}
+
+maxUtuple :: Int
+maxUtuple = 100
+
+tcUtuple :: Int -> Qual Tcon
+tcUtuple n = (primMname,"Z"++ (show n) ++ "H")
+
+ktUtuple :: Int -> Kind
+ktUtuple n = foldr Karrow Kunlifted (replicate n Kopen)
+
+tUtuple :: [Ty] -> Ty
+tUtuple ts = foldl Tapp (Tcon (tcUtuple (length ts))) ts
+
+isUtupleTy :: Ty -> Bool
+isUtupleTy (Tapp t _) = isUtupleTy t
+isUtupleTy (Tcon tc) = tc `elem` [tcUtuple n | n <- [1..maxUtuple]]
+isUtupleTy _ = False
+
+dcUtuple :: Int -> Qual Dcon
+dcUtuple n = (primMname,"ZdwZ" ++ (show n) ++ "H")
+
+isUtupleDc :: Qual Dcon -> Bool
+isUtupleDc dc = dc `elem` [dcUtuple n | n <- [1..maxUtuple]]
+
+dcUtupleTy :: Int -> Ty
+dcUtupleTy n =
+ foldr ( \tv t -> Tforall (tv,Kopen) t)
+ (foldr ( \tv t -> tArrow (Tvar tv) t)
+ (tUtuple (map Tvar tvs)) tvs)
+ tvs
+ where tvs = map ( \i -> ("a" ++ (show i))) [1..n]
+
+utuple :: [Ty] -> [Exp] -> Exp
+utuple ts es = foldl App (foldl Appt (Dcon (dcUtuple (length es))) ts) es
+
+
diff --git a/utils/ext-core/Driver.hs b/utils/ext-core/Driver.hs
new file mode 100644
index 0000000000..2328eca22a
--- /dev/null
+++ b/utils/ext-core/Driver.hs
@@ -0,0 +1,86 @@
+{- A simple driver that loads, typechecks, prepares, re-typechecks, and interprets the
+ GHC standard Prelude modules and an application module called Main.
+
+ Note that, if compiled under GHC, this requires a very large heap to run!
+-}
+
+import Monad
+import Core
+import Printer
+import Parser
+import Lex
+import ParseGlue
+import Env
+import Prims
+import Check
+import Prep
+import Interp
+
+process (senv,modules) f =
+ do putStrLn ("Processing " ++ f)
+ s <- readFile f
+ case parse s 1 of
+ OkP m -> do putStrLn "Parse succeeded"
+ {- writeFile (f ++ ".parsed") (show m) -}
+ case checkModule senv m of
+ OkC senv' ->
+ do putStrLn "Check succeeded"
+ let m' = prepModule senv' m
+ {- writeFile (f ++ ".prepped") (show m') -}
+ case checkModule senv m' of
+ OkC senv'' ->
+ do putStrLn "Recheck succeeded"
+ return (senv'',modules ++ [m'])
+ FailC s ->
+ do putStrLn ("Recheck failed: " ++ s)
+ error "quit"
+ FailC s ->
+ do putStrLn ("Check failed: " ++ s)
+ error "quit"
+ FailP s -> do putStrLn ("Parse failed: " ++ s)
+ error "quit"
+
+main = do (_,modules) <- foldM process (initialEnv,[]) flist
+ let result = evalProgram modules
+ putStrLn ("Result = " ++ show result)
+ putStrLn "All done"
+ where flist = ["PrelBase.hcr",
+ "PrelMaybe.hcr",
+ "PrelTup.hcr",
+ "PrelList.hcr",
+ "PrelShow.hcr",
+ "PrelEnum.hcr",
+ "PrelNum.hcr",
+ "PrelST.hcr",
+ "PrelArr.hcr",
+ "PrelDynamic.hcr",
+ "PrelReal.hcr",
+ "PrelFloat.hcr",
+ "PrelRead.hcr",
+ "PrelIOBase.hcr",
+ "PrelException.hcr",
+ "PrelErr.hcr",
+ "PrelConc.hcr",
+ "PrelPtr.hcr",
+ "PrelByteArr.hcr",
+ "PrelPack.hcr",
+ "PrelBits.hcr",
+ "PrelWord.hcr",
+ "PrelInt.hcr",
+ "PrelCTypes.hcr",
+ "PrelStable.hcr",
+ "PrelCTypesISO.hcr",
+ "Monad.hcr",
+ "PrelStorable.hcr",
+ "PrelMarshalAlloc.hcr",
+ "PrelMarshalUtils.hcr",
+ "PrelMarshalArray.hcr",
+ "PrelCString.hcr",
+ "PrelMarshalError.hcr",
+ "PrelCError.hcr",
+ "PrelPosix.hcr",
+ "PrelHandle.hcr",
+ "PrelIO.hcr",
+ "Prelude.hcr",
+ "Main.hcr" ]
+
diff --git a/utils/ext-core/Env.hs b/utils/ext-core/Env.hs
new file mode 100644
index 0000000000..6f6973c558
--- /dev/null
+++ b/utils/ext-core/Env.hs
@@ -0,0 +1,44 @@
+{- Environments.
+ Uses lists for simplicity and to make the semantics clear.
+ A real implementation should use balanced trees or hash tables.
+-}
+
+module Env (Env,
+ eempty,
+ elookup,
+ eextend,
+ edomain,
+ efromlist,
+ efilter,
+ eremove)
+where
+
+import List
+
+data Env a b = Env [(a,b)]
+ deriving (Show)
+
+eempty :: Env a b
+eempty = Env []
+
+{- In case of duplicates, returns most recently added entry. -}
+elookup :: (Eq a) => Env a b -> a -> Maybe b
+elookup (Env l) k = lookup k l
+
+{- May hide existing entries. -}
+eextend :: Env a b -> (a,b) -> Env a b
+eextend (Env l) (k,d) = Env ((k,d):l)
+
+edomain :: (Eq a) => Env a b -> [a]
+edomain (Env l) = nub (map fst l)
+
+{- In case of duplicates, first entry hides others. -}
+efromlist :: [(a,b)] -> Env a b
+efromlist l = Env l
+
+eremove :: (Eq a) => Env a b -> a -> Env a b
+eremove (Env l) k = Env (filter ((/= k).fst) l)
+
+efilter :: Env a b -> (a -> Bool) -> Env a b
+efilter (Env l) p = Env (filter (p.fst) l)
+
diff --git a/utils/ext-core/Interp.hs b/utils/ext-core/Interp.hs
new file mode 100644
index 0000000000..1988ae9cf3
--- /dev/null
+++ b/utils/ext-core/Interp.hs
@@ -0,0 +1,450 @@
+{-
+Interprets the subset of well-typed Core programs for which
+ (a) All constructor and primop applications are saturated
+ (b) All non-trivial expressions of unlifted kind ('#') are
+ scrutinized in a Case expression.
+
+This is by no means a "minimal" interpreter, in the sense that considerably
+simpler machinary could be used to run programs and get the right answers.
+However, it attempts to mirror the intended use of various Core constructs,
+particularly with respect to heap usage. So considerations such as unboxed
+tuples, sharing, trimming, black-holing, etc. are all covered.
+The only major omission is garbage collection.
+
+Just a sampling of primitive types and operators are included.
+-}
+
+module Interp where
+
+import Core
+import Printer
+import Monad
+import Env
+import List
+import Char
+import Prims
+
+data HeapValue =
+ Hconstr Dcon [Value] -- constructed value (note: no qualifier needed!)
+ | Hclos Venv Var Exp -- function closure
+ | Hthunk Venv Exp -- unevaluated thunk
+ deriving (Show)
+
+type Ptr = Int
+
+data Value =
+ Vheap Ptr -- heap pointer (boxed)
+ | Vimm PrimValue -- immediate primitive value (unboxed)
+ | Vutuple [Value] -- unboxed tuples
+ deriving (Show)
+
+type Venv = Env Var Value -- values of vars
+
+data PrimValue = -- values of the (unboxed) primitive types
+ PCharzh Integer -- actually 31-bit unsigned
+ | PIntzh Integer -- actually WORD_SIZE_IN_BITS-bit signed
+ | PWordzh Integer -- actually WORD_SIZE_IN_BITS-bit unsigned
+ | PAddrzh Integer -- actually native pointer size
+ | PFloatzh Rational -- actually 32-bit
+ | PDoublezh Rational -- actually 64-bit
+-- etc., etc.
+ deriving (Eq,Show)
+
+type Menv = Env Mname Venv -- modules
+
+initialGlobalEnv :: Menv
+initialGlobalEnv =
+ efromlist
+ [(primMname,efromlist [("realWorldzh",Vimm (PIntzh 0))])]
+
+{- Heap management. -}
+{- Nothing is said about garbage collection. -}
+
+data Heap = Heap Ptr (Env Ptr HeapValue) -- last cell allocated; environment of allocated cells
+ deriving (Show)
+
+hallocate :: Heap -> HeapValue -> (Heap,Ptr)
+hallocate (Heap last contents) v =
+ let next = last+1
+ in (Heap next (eextend contents (next,v)),next)
+
+hupdate :: Heap -> Ptr -> HeapValue -> Heap
+hupdate (Heap last contents) p v =
+ Heap last (eextend contents (p,v))
+
+hlookup:: Heap -> Ptr -> HeapValue
+hlookup (Heap _ contents) p =
+ case elookup contents p of
+ Just v -> v
+ Nothing -> error "Missing heap entry (black hole?)"
+
+hremove :: Heap -> Ptr -> Heap
+hremove (Heap last contents) p =
+ Heap last (eremove contents p)
+
+hempty :: Heap
+hempty = Heap 0 eempty
+
+{- The evaluation monad manages the heap and the possiblity
+ of exceptions. -}
+
+type Exn = Value
+
+newtype Eval a = Eval (Heap -> (Heap,Either a Exn))
+
+instance Monad Eval where
+ (Eval m) >>= k = Eval (
+ \h -> case m h of
+ (h',Left x) -> case k x of
+ Eval k' -> k' h'
+ (h',Right exn) -> (h',Right exn))
+ return x = Eval (\h -> (h,Left x))
+
+hallocateE :: HeapValue -> Eval Ptr
+hallocateE v = Eval (\ h ->
+ let (h',p) = hallocate h v
+ in (h', Left p))
+
+hupdateE :: Ptr -> HeapValue -> Eval ()
+hupdateE p v = Eval (\h -> (hupdate h p v,Left ()))
+
+hlookupE :: Ptr -> Eval HeapValue
+hlookupE p = Eval (\h -> (h,Left (hlookup h p)))
+
+hremoveE :: Ptr -> Eval ()
+hremoveE p = Eval (\h -> (hremove h p, Left ()))
+
+raiseE :: Exn -> Eval a
+raiseE exn = Eval (\h -> (h,Right exn))
+
+catchE :: Eval a -> (Exn -> Eval a) -> Eval a
+catchE (Eval m) f = Eval
+ (\h -> case m h of
+ (h',Left x) -> (h',Left x)
+ (h',Right exn) ->
+ case f exn of
+ Eval f' -> f' h')
+
+runE :: Eval a -> a
+runE (Eval f) =
+ case f hempty of
+ (_,Left v) -> v
+ (_,Right exn) -> error ("evaluation failed with uncaught exception: " ++ show exn)
+
+
+{- Main entry point -}
+evalProgram :: [Module] -> Value
+evalProgram modules =
+ runE(
+ do globalEnv <- foldM evalModule initialGlobalEnv modules
+ Vutuple [_,v] <- evalExp globalEnv eempty (App (Var ("Main","main")) (Var (primMname,"realWorldzh")))
+ return v)
+
+{- Environments:
+
+Evaluating a module just fills an environment with suspensions for all
+the external top-level values; it doesn't actually do any evaluation
+or look anything up.
+
+By the time we actually evaluate an expression, all external values from
+all modules will be in globalEnv. So evaluation just maintains an environment
+of non-external values (top-level or local). In particular, only non-external
+values end up in closures (all other values are accessible from globalEnv.)
+
+Throughout:
+
+- globalEnv contains external values (all top-level) from all modules seen so far.
+
+In evalModule:
+
+- e_venv contains external values (all top-level) seen so far in current module
+- l_venv contains non-external values (top-level or local)
+ seen so far in current module.
+In evalExp:
+
+- env contains non-external values (top-level or local) seen so far
+ in current expression.
+-}
+
+
+evalModule :: Menv -> Module -> Eval Menv
+evalModule globalEnv (Module mn tdefs vdefgs) =
+ do (e_venv,l_venv) <- foldM evalVdef (eempty,eempty) vdefgs
+ return (eextend globalEnv (mn,e_venv))
+ where
+ evalVdef :: (Venv,Venv) -> Vdefg -> Eval (Venv,Venv)
+ evalVdef (e_env,l_env) (Nonrec(Vdef((m,x),t,e))) =
+ do p <- hallocateE (suspendExp l_env e)
+ let heaps =
+ if m == "" then
+ (e_env,eextend l_env (x,Vheap p))
+ else
+ (eextend e_env (x,Vheap p),l_env)
+ return heaps
+ evalVdef (e_env,l_env) (Rec vdefs) =
+ do l_vs0 <- mapM preallocate l_xs
+ let l_env' = foldl eextend l_env (zip l_xs l_vs0)
+ let l_hs = map (suspendExp l_env') l_es
+ mapM_ reallocate (zip l_vs0 l_hs)
+ let e_hs = map (suspendExp l_env') e_es
+ e_vs <- mapM allocate e_hs
+ let e_env' = foldl eextend e_env (zip e_xs e_vs)
+ return (e_env',l_env')
+ where
+ (l_xs,l_es) = unzip [(x,e) | Vdef(("",x),_,e) <- vdefs]
+ (e_xs,e_es) = unzip [(x,e) | Vdef((m,x),_,e) <- vdefs, m /= ""]
+ preallocate _ =
+ do p <- hallocateE undefined
+ return (Vheap p)
+ reallocate (Vheap p0,h) =
+ hupdateE p0 h
+ allocate h =
+ do p <- hallocateE h
+ return (Vheap p)
+
+ suspendExp:: Venv -> Exp -> HeapValue
+ suspendExp env (Lam (Vb(x,_)) e) = Hclos env' x e
+ where env' = thin env (delete x (freevarsExp e))
+ suspendExp env e = Hthunk env' e
+ where env' = thin env (freevarsExp e)
+
+
+evalExp :: Menv -> Venv -> Exp -> Eval Value
+evalExp globalEnv env (Var qv) =
+ let v = qlookup globalEnv env qv
+ in case v of
+ Vheap p ->
+ do z <- hlookupE p -- can fail due to black-holing
+ case z of
+ Hthunk env' e ->
+ do hremoveE p -- black-hole
+ w@(Vheap p') <- evalExp globalEnv env' e -- result is guaranteed to be boxed!
+ h <- hlookupE p'
+ hupdateE p h
+ return w
+ _ -> return v -- return pointer to Hclos or Hconstr
+ _ -> return v -- return Vimm or Vutuple
+evalExp globalEnv env (Lit l) = return (Vimm (evalLit l))
+evalExp globalEnv env (Dcon (_,c)) =
+ do p <- hallocateE (Hconstr c [])
+ return (Vheap p)
+
+evalExp globalEnv env (App e1 e2) = evalApp env e1 [e2]
+ where
+ evalApp :: Venv -> Exp -> [Exp] -> Eval Value
+ evalApp env (App e1 e2) es = evalApp env e1 (e2:es)
+ evalApp env (op @(Dcon (qdc@(m,c)))) es =
+ do vs <- suspendExps globalEnv env es
+ if isUtupleDc qdc then
+ return (Vutuple vs)
+ else
+ {- allocate a thunk -}
+ do p <- hallocateE (Hconstr c vs)
+ return (Vheap p)
+ evalApp env (op @ (Var(m,p))) es | m == primMname =
+ do vs <- evalExps globalEnv env es
+ case (p,vs) of
+ ("raisezh",[exn]) -> raiseE exn
+ ("catchzh",[body,handler,rws]) ->
+ catchE (apply body [rws])
+ (\exn -> apply handler [exn,rws])
+ _ -> evalPrimop p vs
+ evalApp env (External s _) es =
+ do vs <- evalExps globalEnv env es
+ evalExternal s vs
+ evalApp env (Appt e _) es = evalApp env e es
+ evalApp env (Lam (Tb _) e) es = evalApp env e es
+ evalApp env (Coerce _ e) es = evalApp env e es
+ evalApp env (Note _ e) es = evalApp env e es
+ evalApp env e es =
+ {- e must now evaluate to a closure -}
+ do vs <- suspendExps globalEnv env es
+ vop <- evalExp globalEnv env e
+ apply vop vs
+
+ apply :: Value -> [Value] -> Eval Value
+ apply vop [] = return vop
+ apply (Vheap p) (v:vs) =
+ do Hclos env' x b <- hlookupE p
+ v' <- evalExp globalEnv (eextend env' (x,v)) b
+ apply v' vs
+
+
+evalExp globalEnv env (Appt e _) = evalExp globalEnv env e
+evalExp globalEnv env (Lam (Vb(x,_)) e) =
+ do p <- hallocateE (Hclos env' x e)
+ return (Vheap p)
+ where env' = thin env (delete x (freevarsExp e))
+evalExp globalEnv env (Lam _ e) = evalExp globalEnv env e
+evalExp globalEnv env (Let vdef e) =
+ do env' <- evalVdef globalEnv env vdef
+ evalExp globalEnv env' e
+ where
+ evalVdef :: Menv -> Venv -> Vdefg -> Eval Venv
+ evalVdef globalEnv env (Nonrec(Vdef((m,x),t,e))) =
+ do v <- suspendExp globalEnv env e
+ return (eextend env (x,v))
+ evalVdef globalEnv env (Rec vdefs) =
+ do vs0 <- mapM preallocate xs
+ let env' = foldl eextend env (zip xs vs0)
+ vs <- suspendExps globalEnv env' es
+ mapM_ reallocate (zip vs0 vs)
+ return env'
+ where
+ (xs,es) = unzip [(x,e) | Vdef((_,x),_,e) <- vdefs]
+ preallocate _ =
+ do p <- hallocateE (Hconstr "UGH" [])
+ return (Vheap p)
+ reallocate (Vheap p0,Vheap p) =
+ do h <- hlookupE p
+ hupdateE p0 h
+
+evalExp globalEnv env (Case e (x,_) alts) =
+ do z <- evalExp globalEnv env e
+ let env' = eextend env (x,z)
+ case z of
+ Vheap p ->
+ do h <- hlookupE p -- can fail due to black-holing
+ case h of
+ Hconstr dcon vs -> evalDcAlt env' dcon vs (reverse alts)
+ _ -> evalDefaultAlt env' alts
+ Vutuple vs ->
+ evalUtupleAlt env' vs (reverse alts)
+ Vimm pv ->
+ evalLitAlt env' pv (reverse alts)
+ where
+ evalDcAlt :: Venv -> Dcon -> [Value] -> [Alt] -> Eval Value
+ evalDcAlt env dcon vs alts =
+ f alts
+ where
+ f ((Acon (_,dcon') _ xs e):as) =
+ if dcon == dcon' then
+ evalExp globalEnv (foldl eextend env (zip (map fst xs) vs)) e
+ else f as
+ f [Adefault e] =
+ evalExp globalEnv env e
+ f _ = error "impossible Case-evalDcAlt"
+
+ evalUtupleAlt :: Venv -> [Value] -> [Alt] -> Eval Value
+ evalUtupleAlt env vs [Acon _ _ xs e] =
+ evalExp globalEnv (foldl eextend env (zip (map fst xs) vs)) e
+
+ evalLitAlt :: Venv -> PrimValue -> [Alt] -> Eval Value
+ evalLitAlt env pv alts =
+ f alts
+ where
+ f ((Alit lit e):as) =
+ let pv' = evalLit lit
+ in if pv == pv' then
+ evalExp globalEnv env e
+ else f as
+ f [Adefault e] =
+ evalExp globalEnv env e
+ f _ = error "impossible Case-evalLitAlt"
+
+ evalDefaultAlt :: Venv -> [Alt] -> Eval Value
+ evalDefaultAlt env [Adefault e] = evalExp globalEnv env e
+
+evalExp globalEnv env (Coerce _ e) = evalExp globalEnv env e
+evalExp globalEnv env (Note _ e) = evalExp globalEnv env e
+evalExp globalEnv env (External s t) = evalExternal s []
+
+evalExps :: Menv -> Venv -> [Exp] -> Eval [Value]
+evalExps globalEnv env = mapM (evalExp globalEnv env)
+
+suspendExp:: Menv -> Venv -> Exp -> Eval Value
+suspendExp globalEnv env (Var qv) = return (qlookup globalEnv env qv)
+suspendExp globalEnv env (Lit l) = return (Vimm (evalLit l))
+suspendExp globalEnv env (Lam (Vb(x,_)) e) =
+ do p <- hallocateE (Hclos env' x e)
+ return (Vheap p)
+ where env' = thin env (delete x (freevarsExp e))
+suspendExp globalEnv env (Lam _ e) = suspendExp globalEnv env e
+suspendExp globalEnv env (Appt e _) = suspendExp globalEnv env e
+suspendExp globalEnv env (Coerce _ e) = suspendExp globalEnv env e
+suspendExp globalEnv env (Note _ e) = suspendExp globalEnv env e
+suspendExp globalEnv env (External s _) = evalExternal s []
+suspendExp globalEnv env e =
+ do p <- hallocateE (Hthunk env' e)
+ return (Vheap p)
+ where env' = thin env (freevarsExp e)
+
+suspendExps :: Menv -> Venv -> [Exp] -> Eval [Value]
+suspendExps globalEnv env = mapM (suspendExp globalEnv env)
+
+mlookup :: Menv -> Venv -> Mname -> Venv
+mlookup _ env "" = env
+mlookup globalEnv _ m =
+ case elookup globalEnv m of
+ Just env' -> env'
+ Nothing -> error ("undefined module name: " ++ m)
+
+qlookup :: Menv -> Venv -> (Mname,Var) -> Value
+qlookup globalEnv env (m,k) =
+ case elookup (mlookup globalEnv env m) k of
+ Just v -> v
+ Nothing -> error ("undefined identifier: " ++ show m ++ "." ++ show k)
+
+evalPrimop :: Var -> [Value] -> Eval Value
+evalPrimop "zpzh" [Vimm (PIntzh i1),Vimm (PIntzh i2)] = return (Vimm (PIntzh (i1+i2)))
+evalPrimop "zmzh" [Vimm (PIntzh i1),Vimm (PIntzh i2)] = return (Vimm (PIntzh (i1-i2)))
+evalPrimop "ztzh" [Vimm (PIntzh i1),Vimm (PIntzh i2)] = return (Vimm (PIntzh (i1*i2)))
+evalPrimop "zgzh" [Vimm (PIntzh i1),Vimm (PIntzh i2)] = mkBool (i1 > i2)
+evalPrimop "remIntzh" [Vimm (PIntzh i1),Vimm (PIntzh i2)] = return (Vimm (PIntzh (i1 `rem` i2)))
+-- etc.
+evalPrimop p vs = error ("undefined primop: " ++ p)
+
+evalExternal :: String -> [Value] -> Eval Value
+-- etc.
+evalExternal s vs = error "evalExternal undefined for now" -- etc.,etc.
+
+evalLit :: Lit -> PrimValue
+evalLit l =
+ case l of
+ Lint i (Tcon(_,"Intzh")) -> PIntzh i
+ Lint i (Tcon(_,"Wordzh")) -> PWordzh i
+ Lint i (Tcon(_,"Addrzh")) -> PAddrzh i
+ Lint i (Tcon(_,"Charzh")) -> PCharzh i
+ Lrational r (Tcon(_,"Floatzh")) -> PFloatzh r
+ Lrational r (Tcon(_,"Doublezh")) -> PDoublezh r
+ Lchar c (Tcon(_,"Charzh")) -> PCharzh (toEnum (ord c))
+ Lstring s (Tcon(_,"Addrzh")) -> PAddrzh 0 -- should really be address of non-heap copy of C-format string s
+
+{- Utilities -}
+
+mkBool True =
+ do p <- hallocateE (Hconstr "ZdwTrue" [])
+ return (Vheap p)
+mkBool False =
+ do p <- hallocateE (Hconstr "ZdwFalse" [])
+ return (Vheap p)
+
+thin env vars = efilter env (`elem` vars)
+
+{- Return the free non-external variables in an expression. -}
+
+freevarsExp :: Exp -> [Var]
+freevarsExp (Var ("",v)) = [v]
+freevarsExp (Var qv) = []
+freevarsExp (Dcon _) = []
+freevarsExp (Lit _) = []
+freevarsExp (App e1 e2) = freevarsExp e1 `union` freevarsExp e2
+freevarsExp (Appt e t) = freevarsExp e
+freevarsExp (Lam (Vb(v,_)) e) = delete v (freevarsExp e)
+freevarsExp (Lam _ e) = freevarsExp e
+freevarsExp (Let vdefg e) = freevarsVdefg vdefg `union` freevarsExp e
+ where freevarsVdefg (Rec vdefs) = (foldl union [] (map freevarsExp es)) \\ vs
+ where (vs,es) = unzip [(v,e) | Vdef((_,v),_,e) <- vdefs]
+ freevarsVdefg (Nonrec (Vdef (_,_,e))) = freevarsExp e
+freevarsExp (Case e (v,_) as) = freevarsExp e `union` [v] `union` freevarsAlts as
+ where freevarsAlts alts = foldl union [] (map freevarsAlt alts)
+ freevarsAlt (Acon _ _ vbs e) = freevarsExp e \\ (map fst vbs)
+ freevarsAlt (Alit _ e) = freevarsExp e
+ freevarsAlt (Adefault e) = freevarsExp e
+freevarsExp (Coerce _ e) = freevarsExp e
+freevarsExp (Note _ e) = freevarsExp e
+freevarsExp (External _ _) = []
+
+
+
+
diff --git a/utils/ext-core/Lex.hs b/utils/ext-core/Lex.hs
new file mode 100644
index 0000000000..ad9d2eb00f
--- /dev/null
+++ b/utils/ext-core/Lex.hs
@@ -0,0 +1,92 @@
+module Lex where
+
+import ParseGlue
+import Ratio
+import Char
+
+isNameChar c = isAlpha c || isDigit c || (c == '_') || (c == '\'')
+isKeywordChar c = isAlpha c || (c == '_')
+
+lexer :: (Token -> P a) -> P a
+lexer cont [] = cont TKEOF []
+lexer cont ('\n':cs) = \line -> lexer cont cs (line+1)
+lexer cont ('-':'>':cs) = cont TKrarrow cs
+lexer cont (c:cs)
+ | isSpace c = lexer cont cs
+ | isLower c || (c == '_') = lexName cont TKname (c:cs)
+ | isUpper c = lexName cont TKcname (c:cs)
+ | isDigit c || (c == '-') = lexNum cont (c:cs)
+lexer cont ('%':cs) = lexKeyword cont cs
+lexer cont ('\'':cs) = lexChar cont cs
+lexer cont ('\"':cs) = lexString [] cont cs
+lexer cont ('#':cs) = cont TKhash cs
+lexer cont ('(':cs) = cont TKoparen cs
+lexer cont (')':cs) = cont TKcparen cs
+lexer cont ('{':cs) = cont TKobrace cs
+lexer cont ('}':cs) = cont TKcbrace cs
+lexer cont ('=':cs) = cont TKeq cs
+lexer cont (':':':':cs) = cont TKcoloncolon cs
+lexer cont ('*':cs) = cont TKstar cs
+lexer cont ('.':cs) = cont TKdot cs
+lexer cont ('\\':cs) = cont TKlambda cs
+lexer cont ('/':'\\':cs) = cont TKbiglambda cs
+lexer cont ('@':cs) = cont TKat cs
+lexer cont ('?':cs) = cont TKquestion cs
+lexer cont (';':cs) = cont TKsemicolon cs
+lexer cont (c:cs) = failP "invalid character" [c]
+
+lexChar cont ('\\':'x':h1:h0:'\'':cs)
+ | isHexEscape [h1,h0] = cont (TKchar (hexToChar h1 h0)) cs
+lexChar cont ('\\':cs) = failP "invalid char character" ('\\':(take 10 cs))
+lexChar cont ('\'':cs) = failP "invalid char character" ['\'']
+lexChar cont ('\"':cs) = failP "invalid char character" ['\"']
+lexChar cont (c:'\'':cs) = cont (TKchar c) cs
+
+lexString s cont ('\\':'x':h1:h0:cs)
+ | isHexEscape [h1,h0] = lexString (s++[hexToChar h1 h0]) cont cs
+lexString s cont ('\\':cs) = failP "invalid string character" ['\\']
+lexString s cont ('\'':cs) = failP "invalid string character" ['\'']
+lexString s cont ('\"':cs) = cont (TKstring s) cs
+lexString s cont (c:cs) = lexString (s++[c]) cont cs
+
+isHexEscape = all (\c -> isHexDigit c && (isDigit c || isLower c))
+
+hexToChar h1 h0 =
+ chr(
+ (digitToInt h1) * 16 +
+ (digitToInt h0))
+
+
+lexNum cont cs =
+ case cs of
+ ('-':cs) -> f (-1) cs
+ _ -> f 1 cs
+ where f sgn cs =
+ case span isDigit cs of
+ (digits,'.':c:rest) | isDigit c ->
+ cont (TKrational (numer % denom)) rest'
+ where (fpart,rest') = span isDigit (c:rest)
+ denom = 10^(length fpart)
+ numer = sgn * ((read digits) * denom + (read fpart))
+ (digits,rest) -> cont (TKinteger (sgn * (read digits))) rest
+
+lexName cont cstr cs = cont (cstr name) rest
+ where (name,rest) = span isNameChar cs
+
+lexKeyword cont cs =
+ case span isKeywordChar cs of
+ ("module",rest) -> cont TKmodule rest
+ ("data",rest) -> cont TKdata rest
+ ("newtype",rest) -> cont TKnewtype rest
+ ("forall",rest) -> cont TKforall rest
+ ("rec",rest) -> cont TKrec rest
+ ("let",rest) -> cont TKlet rest
+ ("in",rest) -> cont TKin rest
+ ("case",rest) -> cont TKcase rest
+ ("of",rest) -> cont TKof rest
+ ("coerce",rest) -> cont TKcoerce rest
+ ("note",rest) -> cont TKnote rest
+ ("external",rest) -> cont TKexternal rest
+ ("_",rest) -> cont TKwild rest
+ _ -> failP "invalid keyword" ('%':cs)
+
diff --git a/utils/ext-core/ParseGlue.hs b/utils/ext-core/ParseGlue.hs
new file mode 100644
index 0000000000..3dde0c3d75
--- /dev/null
+++ b/utils/ext-core/ParseGlue.hs
@@ -0,0 +1,65 @@
+module ParseGlue where
+
+data ParseResult a = OkP a | FailP String
+type P a = String -> Int -> ParseResult a
+
+thenP :: P a -> (a -> P b) -> P b
+m `thenP` k = \ s l ->
+ case m s l of
+ OkP a -> k a s l
+ FailP s -> FailP s
+
+returnP :: a -> P a
+returnP m _ _ = OkP m
+
+failP :: String -> P a
+failP s s' _ = FailP (s ++ ":" ++ s')
+
+data Token =
+ TKmodule
+ | TKdata
+ | TKnewtype
+ | TKforall
+ | TKrec
+ | TKlet
+ | TKin
+ | TKcase
+ | TKof
+ | TKcoerce
+ | TKnote
+ | TKexternal
+ | TKwild
+ | TKoparen
+ | TKcparen
+ | TKobrace
+ | TKcbrace
+ | TKhash
+ | TKeq
+ | TKcoloncolon
+ | TKstar
+ | TKrarrow
+ | TKlambda
+ | TKbiglambda
+ | TKat
+ | TKdot
+ | TKquestion
+ | TKsemicolon
+ | TKname String
+ | TKcname String
+ | TKinteger Integer
+ | TKrational Rational
+ | TKstring String
+ | TKchar Char
+ | TKEOF
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/utils/ext-core/Parser.y b/utils/ext-core/Parser.y
new file mode 100644
index 0000000000..1e1c6a3592
--- /dev/null
+++ b/utils/ext-core/Parser.y
@@ -0,0 +1,230 @@
+{
+module Parser ( parse ) where
+
+import Core
+import ParseGlue
+import Lex
+
+}
+
+%name parse
+%tokentype { Token }
+
+%token
+ '%module' { TKmodule }
+ '%data' { TKdata }
+ '%newtype' { TKnewtype }
+ '%forall' { TKforall }
+ '%rec' { TKrec }
+ '%let' { TKlet }
+ '%in' { TKin }
+ '%case' { TKcase }
+ '%of' { TKof }
+ '%coerce' { TKcoerce }
+ '%note' { TKnote }
+ '%external' { TKexternal }
+ '%_' { TKwild }
+ '(' { TKoparen }
+ ')' { TKcparen }
+ '{' { TKobrace }
+ '}' { TKcbrace }
+ '#' { TKhash}
+ '=' { TKeq }
+ '::' { TKcoloncolon }
+ '*' { TKstar }
+ '->' { TKrarrow }
+ '\\' { TKlambda}
+ '@' { TKat }
+ '.' { TKdot }
+ '?' { TKquestion}
+ ';' { TKsemicolon }
+ NAME { TKname $$ }
+ CNAME { TKcname $$ }
+ INTEGER { TKinteger $$ }
+ RATIONAL { TKrational $$ }
+ STRING { TKstring $$ }
+ CHAR { TKchar $$ }
+
+%monad { P } { thenP } { returnP }
+%lexer { lexer } { TKEOF }
+
+%%
+
+module :: { Module }
+ : '%module' mname tdefs vdefgs
+ { Module $2 $3 $4 }
+
+tdefs :: { [Tdef] }
+ : {- empty -} {[]}
+ | tdef ';' tdefs {$1:$3}
+
+tdef :: { Tdef }
+ : '%data' qcname tbinds '=' '{' cons1 '}'
+ { Data $2 $3 $6 }
+ | '%newtype' qcname tbinds trep
+ { Newtype $2 $3 $4 }
+
+trep :: { Maybe Ty }
+ : {- empty -} {Nothing}
+ | '=' ty { Just $2 }
+
+tbind :: { Tbind }
+ : name { ($1,Klifted) }
+ | '(' name '::' akind ')'
+ { ($2,$4) }
+
+tbinds :: { [Tbind] }
+ : {- empty -} { [] }
+ | tbind tbinds { $1:$2 }
+
+
+vbind :: { Vbind }
+ : '(' name '::' ty')' { ($2,$4) }
+
+vbinds :: { [Vbind] }
+ : {-empty -} { [] }
+ | vbind vbinds { $1:$2 }
+
+bind :: { Bind }
+ : '@' tbind { Tb $2 }
+ | vbind { Vb $1 }
+
+binds1 :: { [Bind] }
+ : bind { [$1] }
+ | bind binds1 { $1:$2 }
+
+attbinds :: { [Tbind] }
+ : {- empty -} { [] }
+ | '@' tbind attbinds
+ { $2:$3 }
+
+akind :: { Kind }
+ : '*' {Klifted}
+ | '#' {Kunlifted}
+ | '?' {Kopen}
+ | '(' kind ')' { $2 }
+
+kind :: { Kind }
+ : akind { $1 }
+ | akind '->' kind
+ { Karrow $1 $3 }
+
+cons1 :: { [Cdef] }
+ : con { [$1] }
+ | con ';' cons1 { $1:$3 }
+
+con :: { Cdef }
+ : qcname attbinds atys
+ { Constr $1 $2 $3 }
+
+atys :: { [Ty] }
+ : {- empty -} { [] }
+ | aty atys { $1:$2 }
+
+aty :: { Ty }
+ : name { Tvar $1 }
+ | qcname { Tcon $1 }
+ | '(' ty ')' { $2 }
+
+
+bty :: { Ty }
+ : aty { $1 }
+ | bty aty { Tapp $1 $2 }
+
+ty :: { Ty }
+ : bty {$1}
+ | bty '->' ty
+ { tArrow $1 $3 }
+ | '%forall' tbinds '.' ty
+ { foldr Tforall $4 $2 }
+
+vdefgs :: { [Vdefg] }
+ : {- empty -} { [] }
+ | vdefg ';' vdefgs {$1:$3 }
+
+vdefg :: { Vdefg }
+ : '%rec' '{' vdefs1 '}'
+ { Rec $3 }
+ | vdef { Nonrec $1}
+
+vdefs1 :: { [Vdef] }
+ : vdef { [$1] }
+ | vdef ';' vdefs1 { $1:$3 }
+
+vdef :: { Vdef }
+ : qname '::' ty '=' exp
+ { Vdef ($1,$3,$5) }
+
+aexp :: { Exp }
+ : qname { Var $1 }
+ | qcname { Dcon $1 }
+ | lit { Lit $1 }
+ | '(' exp ')' { $2 }
+
+fexp :: { Exp }
+ : fexp aexp { App $1 $2 }
+ | fexp '@' aty { Appt $1 $3 }
+ | aexp { $1 }
+
+exp :: { Exp }
+ : fexp { $1 }
+ | '\\' binds1 '->' exp
+ { foldr Lam $4 $2 }
+ | '%let' vdefg '%in' exp
+ { Let $2 $4 }
+ | '%case' aexp '%of' vbind '{' alts1 '}'
+ { Case $2 $4 $6 }
+ | '%coerce' aty exp
+ { Coerce $2 $3 }
+ | '%note' STRING exp
+ { Note $2 $3 }
+ | '%external' STRING aty
+ { External $2 $3 }
+
+alts1 :: { [Alt] }
+ : alt { [$1] }
+ | alt ';' alts1 { $1:$3 }
+
+alt :: { Alt }
+ : qcname attbinds vbinds '->' exp
+ { Acon $1 $2 $3 $5 }
+ | lit '->' exp
+ { Alit $1 $3 }
+ | '%_' '->' exp
+ { Adefault $3 }
+
+lit :: { Lit }
+ : '(' INTEGER '::' aty ')'
+ { Lint $2 $4 }
+ | '(' RATIONAL '::' aty ')'
+ { Lrational $2 $4 }
+ | '(' CHAR '::' aty ')'
+ { Lchar $2 $4 }
+ | '(' STRING '::' aty ')'
+ { Lstring $2 $4 }
+
+name :: { Id }
+ : NAME { $1 }
+
+cname :: { Id }
+ : CNAME { $1 }
+
+mname :: { Id }
+ : CNAME { $1 }
+
+qname :: { (Id,Id) }
+ : name { ("",$1) }
+ | mname '.' name
+ { ($1,$3) }
+
+qcname :: { (Id,Id) }
+ : mname '.' cname
+ { ($1,$3) }
+
+
+{
+
+happyError :: P a
+happyError s l = failP (show l ++ ": Parse error\n") (take 100 s) l
+
+}
diff --git a/utils/ext-core/Prep.hs b/utils/ext-core/Prep.hs
new file mode 100644
index 0000000000..ee65eaaba2
--- /dev/null
+++ b/utils/ext-core/Prep.hs
@@ -0,0 +1,151 @@
+{-
+Preprocess a module to normalize it in the following ways:
+ (1) Saturate all constructor and primop applications.
+ (2) Arrange that any non-trivial expression of unlifted kind ('#')
+ is turned into the scrutinee of a Case.
+After these preprocessing steps, Core can be interpreted (or given an operational semantics)
+ ignoring type information almost completely.
+-}
+
+
+module Prep where
+
+import Prims
+import Core
+import Printer
+import Env
+import Check
+
+primArgTys :: Env Var [Ty]
+primArgTys = efromlist (map f Prims.primVals)
+ where f (v,t) = (v,atys)
+ where (_,atys,_) = splitTy t
+
+prepModule :: Menv -> Module -> Module
+prepModule globalEnv (Module mn tdefs vdefgs) =
+ Module mn tdefs vdefgs'
+ where
+ (_,vdefgs') = foldl prepTopVdefg (eempty,[]) vdefgs
+
+ prepTopVdefg (venv,vdefgs) vdefg = (venv',vdefgs ++ [vdefg'])
+ where (venv',vdefg') = prepVdefg (venv,eempty) vdefg
+
+ prepVdefg (env@(venv,_)) (Nonrec(Vdef(("",x),t,e))) =
+ (eextend venv (x,t), Nonrec(Vdef(("",x),t,prepExp env e)))
+ prepVdefg (env@(venv,_)) (Nonrec(Vdef(qx,t,e))) =
+ (venv, Nonrec(Vdef(qx,t,prepExp env e)))
+ prepVdefg (venv,tvenv) (Rec vdefs) =
+ (venv',Rec [Vdef(qx,t,prepExp (venv',tvenv) e) | Vdef(qx,t,e) <- vdefs])
+ where venv' = foldl eextend venv [(x,t) | Vdef(("",x),t,_) <- vdefs]
+
+ prepExp env (Var qv) = Var qv
+ prepExp env (Dcon qdc) = Dcon qdc
+ prepExp env (Lit l) = Lit l
+ prepExp env e@(App _ _) = unwindApp env e []
+ prepExp env e@(Appt _ _) = unwindApp env e []
+ prepExp (venv,tvenv) (Lam (Vb vb) e) = Lam (Vb vb) (prepExp (eextend venv vb,tvenv) e)
+ prepExp (venv,tvenv) (Lam (Tb tb) e) = Lam (Tb tb) (prepExp (venv,eextend tvenv tb) e)
+ prepExp env@(venv,tvenv) (Let (Nonrec(Vdef(("",x),t,b))) e) | kindof tvenv t == Kunlifted && suspends b =
+ Case (prepExp env b) (x,t) [Adefault (prepExp (eextend venv (x,t),tvenv) e)]
+ prepExp (venv,tvenv) (Let vdefg e) = Let vdefg' (prepExp (venv',tvenv) e)
+ where (venv',vdefg') = prepVdefg (venv,tvenv) vdefg
+ prepExp env@(venv,tvenv) (Case e vb alts) = Case (prepExp env e) vb (map (prepAlt (eextend venv vb,tvenv)) alts)
+ prepExp env (Coerce t e) = Coerce t (prepExp env e)
+ prepExp env (Note s e) = Note s (prepExp env e)
+ prepExp env (External s t) = External s t
+
+ prepAlt (venv,tvenv) (Acon qdc tbs vbs e) = Acon qdc tbs vbs (prepExp (foldl eextend venv vbs,foldl eextend tvenv tbs) e)
+ prepAlt env (Alit l e) = Alit l (prepExp env e)
+ prepAlt env (Adefault e) = Adefault (prepExp env e)
+
+
+ unwindApp env (App e1 e2) as = unwindApp env e1 (Left e2:as)
+ unwindApp env (Appt e t) as = unwindApp env e (Right t:as)
+ unwindApp env (op@(Dcon qdc)) as =
+ etaExpand (drop n atys) (rewindApp env op as)
+ where (tbs,atys0,_) = splitTy (qlookup cenv_ eempty qdc)
+ atys = map (substl (map fst tbs) ts) atys0
+ ts = [t | Right t <- as]
+ n = length [e | Left e <- as]
+ unwindApp env (op@(Var(m,p))) as | m == primMname =
+ etaExpand (drop n atys) (rewindApp env op as)
+ where Just atys = elookup primArgTys p
+ n = length [e | Left e <- as]
+ unwindApp env op as = rewindApp env op as
+
+
+ etaExpand ts e = foldl g e [('$':(show i),t) | (i,t) <- zip [1..] ts]
+ where g e (v,t) = Lam (Vb(v,t)) (App e (Var ("",v)))
+
+ rewindApp env e [] = e
+ rewindApp env@(venv,tvenv) e1 (Left e2:as) | kindof tvenv t == Kunlifted && suspends e2 =
+ Case (prepExp env' e2) (v,t)
+ [Adefault (rewindApp env' (App e1 (Var ("",v))) as)]
+ where v = freshVar venv
+ t = typeofExp env e2
+ env' = (eextend venv (v,t),tvenv)
+ rewindApp env e1 (Left e2:as) = rewindApp env (App e1 (prepExp env e2)) as
+ rewindApp env e (Right t:as) = rewindApp env (Appt e t) as
+
+ freshVar venv = maximum ("":edomain venv) ++ "x" -- one simple way!
+
+ typeofExp :: (Venv,Tvenv) -> Exp -> Ty
+ typeofExp (venv,_) (Var qv) = qlookup venv_ venv qv
+ typeofExp env (Dcon qdc) = qlookup cenv_ eempty qdc
+ typeofExp env (Lit l) = typeofLit l
+ where typeofLit (Lint _ t) = t
+ typeofLit (Lrational _ t) = t
+ typeofLit (Lchar _ t) = t
+ typeofLit (Lstring _ t) = t
+ typeofExp env (App e1 e2) = t
+ where (Tapp(Tapp _ t0) t) = typeofExp env e1
+ typeofExp env (Appt e t) = substl [tv] [t] t'
+ where (Tforall (tv,_) t') = typeofExp env e
+ typeofExp (venv,tvenv) (Lam (Vb(v,t)) e) = tArrow t (typeofExp (eextend venv (v,t),tvenv) e)
+ typeofExp (venv,tvenv) (Lam (Tb tb) e) = Tforall tb (typeofExp (venv,eextend tvenv tb) e)
+ typeofExp (venv,tvenv) (Let vdefg e) = typeofExp (venv',tvenv) e
+ where venv' = case vdefg of
+ Nonrec (Vdef((_,x),t,_)) -> eextend venv (x,t)
+ Rec vdefs -> foldl eextend venv [(x,t) | Vdef((_,x),t,_) <- vdefs]
+ typeofExp (venv,tvenv) (Case _ vb (alt:_)) = typeofAlt (eextend venv vb,tvenv) alt
+ where typeofAlt (venv,tvenv) (Acon _ tbs vbs e) = typeofExp (foldl eextend venv vbs,foldl eextend tvenv tbs) e
+ typeofAlt env (Alit _ e) = typeofExp env e
+ typeofAlt env (Adefault e) = typeofExp env e
+ typeofExp env (Coerce t _) = t
+ typeofExp env (Note _ e) = typeofExp env e
+ typeofExp env (External _ t) = t
+
+ {- Return false for those expressions for which Interp.suspendExp buidds a thunk. -}
+ suspends (Var _) = False
+ suspends (Lit _) = False
+ suspends (Lam (Vb _) _) = False
+ suspends (Lam _ e) = suspends e
+ suspends (Appt e _) = suspends e
+ suspends (Coerce _ e) = suspends e
+ suspends (Note _ e) = suspends e
+ suspends (External _ _) = False
+ suspends _ = True
+
+ kindof :: Tvenv -> Ty -> Kind
+ kindof tvenv (Tvar tv) =
+ case elookup tvenv tv of
+ Just k -> k
+ Nothing -> error ("impossible Tyvar " ++ show tv)
+ kindof tvenv (Tcon qtc) = qlookup tcenv_ eempty qtc
+ kindof tvenv (Tapp t1 t2) = k2
+ where Karrow _ k2 = kindof tvenv t1
+ kindof tvenv (Tforall _ t) = kindof tvenv t
+
+ mlookup :: (Envs -> Env a b) -> Env a b -> Mname -> Env a b
+ mlookup _ local_env "" = local_env
+ mlookup selector _ m =
+ case elookup globalEnv m of
+ Just env -> selector env
+ Nothing -> error ("undefined module name: " ++ m)
+
+ qlookup :: (Ord a, Show a) => (Envs -> Env a b) -> Env a b -> (Mname,a) -> b
+ qlookup selector local_env (m,k) =
+ case elookup (mlookup selector local_env m) k of
+ Just v -> v
+ Nothing -> error ("undefined identifier: " ++ show k)
+
diff --git a/utils/ext-core/Prims.hs b/utils/ext-core/Prims.hs
new file mode 100644
index 0000000000..fd6e827c39
--- /dev/null
+++ b/utils/ext-core/Prims.hs
@@ -0,0 +1,834 @@
+{- This module really should be auto-generated from the master primops.txt file.
+ It is roughly correct (but may be slightly incomplete) wrt/ GHC5.02. -}
+
+module Prims where
+
+import Core
+import Env
+import Check
+
+initialEnv :: Menv
+initialEnv = efromlist [(primMname,primEnv),
+ ("PrelErr",errorEnv)]
+
+primEnv :: Envs
+primEnv = Envs {tcenv_=efromlist primTcs,
+ tsenv_=eempty,
+ cenv_=efromlist primDcs,
+ venv_=efromlist primVals}
+
+errorEnv :: Envs
+errorEnv = Envs {tcenv_=eempty,
+ tsenv_=eempty,
+ cenv_=eempty,
+ venv_=efromlist errorVals}
+
+{- Components of static environment -}
+
+primTcs :: [(Tcon,Kind)]
+primTcs =
+ map (\ ((m,tc),k) -> (tc,k))
+ ([(tcArrow,ktArrow),
+ (tcAddrzh,ktAddrzh),
+ (tcCharzh,ktCharzh),
+ (tcDoublezh,ktDoublezh),
+ (tcFloatzh,ktFloatzh),
+ (tcIntzh,ktIntzh),
+ (tcInt32zh,ktInt32zh),
+ (tcInt64zh,ktInt64zh),
+ (tcWordzh,ktWordzh),
+ (tcWord32zh,ktWord32zh),
+ (tcWord64zh,ktWord64zh),
+ (tcRealWorld, ktRealWorld),
+ (tcStatezh, ktStatezh),
+ (tcArrayzh,ktArrayzh),
+ (tcByteArrayzh,ktByteArrayzh),
+ (tcMutableArrayzh,ktMutableArrayzh),
+ (tcMutableByteArrayzh,ktMutableByteArrayzh),
+ (tcMutVarzh,ktMutVarzh),
+ (tcMVarzh,ktMVarzh),
+ (tcWeakzh,ktWeakzh),
+ (tcForeignObjzh, ktForeignObjzh),
+ (tcStablePtrzh, ktStablePtrzh),
+ (tcThreadIdzh, ktThreadIdzh),
+ (tcZCTCCallable, ktZCTCCallable),
+ (tcZCTCReturnable, ktZCTCReturnable)]
+ ++ [(tcUtuple n, ktUtuple n) | n <- [1..maxUtuple]])
+
+
+primDcs :: [(Dcon,Ty)]
+primDcs = map (\ ((m,c),t) -> (c,t))
+ [(dcUtuple n, dcUtupleTy n) | n <- [1..maxUtuple]]
+
+primVals :: [(Var,Ty)]
+primVals =
+ opsAddrzh ++
+ opsCharzh ++
+ opsDoublezh ++
+ opsFloatzh ++
+ opsIntzh ++
+ opsInt32zh ++
+ opsInt64zh ++
+ opsIntegerzh ++
+ opsWordzh ++
+ opsWord32zh ++
+ opsWord64zh ++
+ opsSized ++
+ opsArray ++
+ opsMutVarzh ++
+ opsState ++
+ opsExn ++
+ opsMVar ++
+ opsWeak ++
+ opsForeignObjzh ++
+ opsStablePtrzh ++
+ opsConc ++
+ opsMisc
+
+
+dcUtuples :: [(Qual Dcon,Ty)]
+dcUtuples = map ( \n -> (dcUtuple n, typ n)) [1..100]
+ where typ n = foldr ( \tv t -> Tforall (tv,Kopen) t)
+ (foldr ( \tv t -> tArrow (Tvar tv) t)
+ (tUtuple (map Tvar tvs)) tvs) tvs
+ where tvs = map ( \i -> ("a" ++ (show i))) [1..n]
+
+
+{- Addrzh -}
+
+tcAddrzh = (primMname,"Addrzh")
+tAddrzh = Tcon tcAddrzh
+ktAddrzh = Kunlifted
+
+opsAddrzh = [
+ ("gtAddrzh",tcompare tAddrzh),
+ ("geAddrzh",tcompare tAddrzh),
+ ("eqAddrzh",tcompare tAddrzh),
+ ("neAddrzh",tcompare tAddrzh),
+ ("ltAddrzh",tcompare tAddrzh),
+ ("leAddrzh",tcompare tAddrzh),
+ ("nullAddrzh", tAddrzh),
+ ("plusAddrzh", tArrow tAddrzh (tArrow tIntzh tAddrzh)),
+ ("minusAddrzh", tArrow tAddrzh (tArrow tAddrzh tIntzh)),
+ ("remAddrzh", tArrow tAddrzh (tArrow tIntzh tIntzh))]
+
+{- Charzh -}
+
+tcCharzh = (primMname,"Charzh")
+tCharzh = Tcon tcCharzh
+ktCharzh = Kunlifted
+
+opsCharzh = [
+ ("gtCharzh", tcompare tCharzh),
+ ("geCharzh", tcompare tCharzh),
+ ("eqCharzh", tcompare tCharzh),
+ ("neCharzh", tcompare tCharzh),
+ ("ltCharzh", tcompare tCharzh),
+ ("leCharzh", tcompare tCharzh),
+ ("ordzh", tArrow tCharzh tIntzh)]
+
+
+{- Doublezh -}
+
+tcDoublezh = (primMname, "Doublezh")
+tDoublezh = Tcon tcDoublezh
+ktDoublezh = Kunlifted
+
+opsDoublezh = [
+ ("zgzhzh", tcompare tDoublezh),
+ ("zgzezhzh", tcompare tDoublezh),
+ ("zezezhzh", tcompare tDoublezh),
+ ("zszezhzh", tcompare tDoublezh),
+ ("zlzhzh", tcompare tDoublezh),
+ ("zlzezhzh", tcompare tDoublezh),
+ ("zpzhzh", tdyadic tDoublezh),
+ ("zmzhzh", tdyadic tDoublezh),
+ ("ztzhzh", tdyadic tDoublezh),
+ ("zszhzh", tdyadic tDoublezh),
+ ("negateDoublezh", tmonadic tDoublezh),
+ ("double2Intzh", tArrow tDoublezh tIntzh),
+ ("double2Floatzh", tArrow tDoublezh tFloatzh),
+ ("expDoublezh", tmonadic tDoublezh),
+ ("logDoublezh", tmonadic tDoublezh),
+ ("sqrtDoublezh", tmonadic tDoublezh),
+ ("sinDoublezh", tmonadic tDoublezh),
+ ("cosDoublezh", tmonadic tDoublezh),
+ ("tanDoublezh", tmonadic tDoublezh),
+ ("asinDoublezh", tmonadic tDoublezh),
+ ("acosDoublezh", tmonadic tDoublezh),
+ ("atanDoublezh", tmonadic tDoublezh),
+ ("sinhDoublezh", tmonadic tDoublezh),
+ ("coshDoublezh", tmonadic tDoublezh),
+ ("tanhDoublezh", tmonadic tDoublezh),
+ ("ztztzhzh", tdyadic tDoublezh),
+ ("decodeDoublezh", tArrow tDoublezh (tUtuple[tIntzh,tIntzh,tByteArrayzh]))]
+
+
+{- Floatzh -}
+
+tcFloatzh = (primMname, "Floatzh")
+tFloatzh = Tcon tcFloatzh
+ktFloatzh = Kunlifted
+
+opsFloatzh = [
+ ("gtFloatzh", tcompare tFloatzh),
+ ("geFloatzh", tcompare tFloatzh),
+ ("eqFloatzh", tcompare tFloatzh),
+ ("neFloatzh", tcompare tFloatzh),
+ ("ltFloatzh", tcompare tFloatzh),
+ ("leFloatzh", tcompare tFloatzh),
+ ("plusFloatzh", tdyadic tFloatzh),
+ ("minusFloatzh", tdyadic tFloatzh),
+ ("timesFloatzh", tdyadic tFloatzh),
+ ("divideFloatzh", tdyadic tFloatzh),
+ ("negateFloatzh", tmonadic tFloatzh),
+ ("float2Intzh", tArrow tFloatzh tIntzh),
+ ("expFloatzh", tmonadic tFloatzh),
+ ("logFloatzh", tmonadic tFloatzh),
+ ("sqrtFloatzh", tmonadic tFloatzh),
+ ("sinFloatzh", tmonadic tFloatzh),
+ ("cosFloatzh", tmonadic tFloatzh),
+ ("tanFloatzh", tmonadic tFloatzh),
+ ("asinFloatzh", tmonadic tFloatzh),
+ ("acosFloatzh", tmonadic tFloatzh),
+ ("atanFloatzh", tmonadic tFloatzh),
+ ("sinhFloatzh", tmonadic tFloatzh),
+ ("coshFloatzh", tmonadic tFloatzh),
+ ("tanhFloatzh", tmonadic tFloatzh),
+ ("powerFloatzh", tdyadic tFloatzh),
+ ("float2Doublezh", tArrow tFloatzh tDoublezh),
+ ("decodeFloatzh", tArrow tFloatzh (tUtuple[tIntzh,tIntzh,tByteArrayzh]))]
+
+
+{- Intzh -}
+
+tcIntzh = (primMname,"Intzh")
+tIntzh = Tcon tcIntzh
+ktIntzh = Kunlifted
+
+opsIntzh = [
+ ("zpzh", tdyadic tIntzh),
+ ("zmzh", tdyadic tIntzh),
+ ("ztzh", tdyadic tIntzh),
+ ("quotIntzh", tdyadic tIntzh),
+ ("remIntzh", tdyadic tIntzh),
+ ("gcdIntzh", tdyadic tIntzh),
+ ("negateIntzh", tmonadic tIntzh),
+ ("addIntCzh", tArrow tIntzh (tArrow tIntzh (tUtuple [tIntzh, tIntzh]))),
+ ("subIntCzh", tArrow tIntzh (tArrow tIntzh (tUtuple [tIntzh, tIntzh]))),
+ ("mulIntCzh", tArrow tIntzh (tArrow tIntzh (tUtuple [tIntzh, tIntzh]))),
+ ("zgzh", tcompare tIntzh),
+ ("zgzezh", tcompare tIntzh),
+ ("zezezh", tcompare tIntzh),
+ ("zszezh", tcompare tIntzh),
+ ("zlzh", tcompare tIntzh),
+ ("zlzezh", tcompare tIntzh),
+ ("chrzh", tArrow tIntzh tCharzh),
+ ("int2Wordzh", tArrow tIntzh tWordzh),
+ ("int2Floatzh", tArrow tIntzh tFloatzh),
+ ("int2Doublezh", tArrow tIntzh tDoublezh),
+ ("intToInt32zh", tArrow tIntzh tInt32zh),
+ ("int2Integerzh", tArrow tIntzh tIntegerzhRes),
+ ("iShiftLzh", tdyadic tIntzh),
+ ("iShiftRAzh", tdyadic tIntzh),
+ ("iShiftRLh", tdyadic tIntzh)]
+
+
+{- Int32zh -}
+
+tcInt32zh = (primMname,"Int32zh")
+tInt32zh = Tcon tcInt32zh
+ktInt32zh = Kunlifted
+
+opsInt32zh = [
+ ("int32ToIntzh", tArrow tInt32zh tIntzh),
+ ("int32ToIntegerzh", tArrow tInt32zh tIntegerzhRes)]
+
+
+{- Int64zh -}
+
+tcInt64zh = (primMname,"Int64zh")
+tInt64zh = Tcon tcInt64zh
+ktInt64zh = Kunlifted
+
+opsInt64zh = [
+ ("int64ToIntegerzh", tArrow tInt64zh tIntegerzhRes)]
+
+{- Integerzh -}
+
+-- not actuallly a primitive type
+tIntegerzhRes = tUtuple [tIntzh, tByteArrayzh]
+tIntegerzhTo t = tArrow tIntzh (tArrow tByteArrayzh t)
+tdyadicIntegerzh = tIntegerzhTo (tIntegerzhTo tIntegerzhRes)
+
+opsIntegerzh = [
+ ("plusIntegerzh", tdyadicIntegerzh),
+ ("minusIntegerzh", tdyadicIntegerzh),
+ ("timesIntegerzh", tdyadicIntegerzh),
+ ("gcdIntegerzh", tdyadicIntegerzh),
+ ("gcdIntegerIntzh", tIntegerzhTo (tArrow tIntzh tIntzh)),
+ ("divExactIntegerzh", tdyadicIntegerzh),
+ ("quotIntegerzh", tdyadicIntegerzh),
+ ("remIntegerzh", tdyadicIntegerzh),
+ ("cmpIntegerzh", tIntegerzhTo (tIntegerzhTo tIntzh)),
+ ("cmpIntegerIntzh", tIntegerzhTo (tArrow tIntzh tIntzh)),
+ ("quotRemIntegerzh", tIntegerzhTo (tIntegerzhTo (tUtuple [tIntzh,tByteArrayzh,tIntzh,tByteArrayzh]))),
+ ("divModIntegerzh", tIntegerzhTo (tIntegerzhTo (tUtuple [tIntzh,tByteArrayzh,tIntzh,tByteArrayzh]))),
+ ("integer2Intzh", tIntegerzhTo tIntzh),
+ ("integer2Wordzh", tIntegerzhTo tWordzh),
+ ("integerToInt32zh", tIntegerzhTo tInt32zh),
+ ("integerToWord32zh", tIntegerzhTo tWord32zh),
+ ("integerToInt64zh", tIntegerzhTo tInt64zh),
+ ("integerToWord64zh", tIntegerzhTo tWord64zh),
+ ("andIntegerzh", tdyadicIntegerzh),
+ ("orIntegerzh", tdyadicIntegerzh),
+ ("xorIntegerzh", tdyadicIntegerzh),
+ ("complementIntegerzh", tIntegerzhTo tIntegerzhRes)]
+
+
+
+{- Wordzh -}
+
+tcWordzh = (primMname,"Wordzh")
+tWordzh = Tcon tcWordzh
+ktWordzh = Kunlifted
+
+opsWordzh = [
+ ("plusWordzh", tdyadic tWordzh),
+ ("minusWordzh", tdyadic tWordzh),
+ ("timesWordzh", tdyadic tWordzh),
+ ("quotWordzh", tdyadic tWordzh),
+ ("remWordzh", tdyadic tWordzh),
+ ("andzh", tdyadic tWordzh),
+ ("orzh", tdyadic tWordzh),
+ ("xorzh", tdyadic tWordzh),
+ ("notzh", tmonadic tWordzh),
+ ("shiftLzh", tArrow tWordzh (tArrow tIntzh tWordzh)),
+ ("shiftRLzh", tArrow tWordzh (tArrow tIntzh tWordzh)),
+ ("word2Intzh", tArrow tWordzh tIntzh),
+ ("wordToWord32zh", tArrow tWordzh tWord32zh),
+ ("word2Integerzh", tArrow tWordzh tIntegerzhRes),
+ ("gtWordzh", tcompare tWordzh),
+ ("geWordzh", tcompare tWordzh),
+ ("eqWordzh", tcompare tWordzh),
+ ("neWordzh", tcompare tWordzh),
+ ("ltWordzh", tcompare tWordzh),
+ ("leWordzh", tcompare tWordzh)]
+
+{- Word32zh -}
+
+tcWord32zh = (primMname,"Word32zh")
+tWord32zh = Tcon tcWord32zh
+ktWord32zh = Kunlifted
+
+opsWord32zh = [
+ ("word32ToWordzh", tArrow tWord32zh tWordzh),
+ ("word32ToIntegerzh", tArrow tWord32zh tIntegerzhRes)]
+
+{- Word64zh -}
+
+tcWord64zh = (primMname,"Word64zh")
+tWord64zh = Tcon tcWord64zh
+ktWord64zh = Kunlifted
+
+opsWord64zh = [
+ ("word64ToIntegerzh", tArrow tWord64zh tIntegerzhRes)]
+
+{- Explicitly sized Intzh and Wordzh -}
+
+opsSized = [
+ ("narrow8Intzh", tmonadic tIntzh),
+ ("narrow16Intzh", tmonadic tIntzh),
+ ("narrow32Intzh", tmonadic tIntzh),
+ ("narrow8Wordzh", tmonadic tWordzh),
+ ("narrow16Wordzh", tmonadic tWordzh),
+ ("narrow32Wordzh", tmonadic tWordzh)]
+
+{- Arrays -}
+
+tcArrayzh = (primMname,"Arrayzh")
+tArrayzh t = Tapp (Tcon tcArrayzh) t
+ktArrayzh = Karrow Klifted Kunlifted
+
+tcByteArrayzh = (primMname,"ByteArrayzh")
+tByteArrayzh = Tcon tcByteArrayzh
+ktByteArrayzh = Kunlifted
+
+tcMutableArrayzh = (primMname,"MutableArrayzh")
+tMutableArrayzh s t = Tapp (Tapp (Tcon tcMutableArrayzh) s) t
+ktMutableArrayzh = Karrow Klifted (Karrow Klifted Kunlifted)
+
+tcMutableByteArrayzh = (primMname,"MutableByteArrayzh")
+tMutableByteArrayzh s = Tapp (Tcon tcMutableByteArrayzh) s
+ktMutableByteArrayzh = Karrow Klifted Kunlifted
+
+opsArray = [
+ ("newArrayzh", Tforall ("a",Klifted)
+ (Tforall ("s",Klifted)
+ (tArrow tIntzh
+ (tArrow (Tvar "a")
+ (tArrow (tStatezh (Tvar "s"))
+ (tUtuple [tStatezh (Tvar "s"),tMutableArrayzh (Tvar "s") (Tvar "a")])))))),
+ ("newByteArrayzh", Tforall ("s",Klifted)
+ (tArrow tIntzh
+ (tArrow (tStatezh (Tvar "s"))
+ (tUtuple [tStatezh (Tvar "s"),tMutableByteArrayzh (Tvar "s")])))),
+ ("newPinnedByteArrayzh", Tforall ("s",Klifted)
+ (tArrow tIntzh
+ (tArrow (tStatezh (Tvar "s"))
+ (tUtuple [tStatezh (Tvar "s"),tMutableByteArrayzh (Tvar "s")])))),
+ ("byteArrayContentszh", tArrow tByteArrayzh tAddrzh),
+ ("indexCharArrayzh", tArrow tByteArrayzh (tArrow tIntzh tCharzh)),
+ ("indexWideCharArrayzh", tArrow tByteArrayzh (tArrow tIntzh tCharzh)),
+ ("indexIntArrayzh", tArrow tByteArrayzh (tArrow tIntzh tIntzh)),
+ ("indexWordArrayzh", tArrow tByteArrayzh (tArrow tIntzh tWordzh)),
+ ("indexAddrArrayzh", tArrow tByteArrayzh (tArrow tIntzh tAddrzh)),
+ ("indexFloatArrayzh", tArrow tByteArrayzh (tArrow tIntzh tFloatzh)),
+ ("indexDoubleArrayzh", tArrow tByteArrayzh (tArrow tIntzh tDoublezh)),
+ ("indexStablePtrArrayzh", Tforall ("a",Klifted) (tArrow tByteArrayzh (tArrow tIntzh (tStablePtrzh (Tvar "a"))))),
+ ("indexInt8Arrayzh", tArrow tByteArrayzh (tArrow tIntzh tIntzh)),
+ ("indexInt16Arrayzh", tArrow tByteArrayzh (tArrow tIntzh tIntzh)),
+ ("indexInt32Arrayzh", tArrow tByteArrayzh (tArrow tIntzh tInt32zh)),
+ ("indexInt64Arrayzh", tArrow tByteArrayzh (tArrow tIntzh tInt64zh)),
+ ("indexWord8Arrayzh", tArrow tByteArrayzh (tArrow tIntzh tWordzh)),
+ ("indexWord16Arrayzh", tArrow tByteArrayzh (tArrow tIntzh tWordzh)),
+ ("indexWord32Arrayzh", tArrow tByteArrayzh (tArrow tIntzh tWord32zh)),
+ ("indexWord64Arrayzh", tArrow tByteArrayzh (tArrow tIntzh tWord64zh)),
+ ("readCharArrayzh", tReadMutableByteArrayzh tCharzh),
+ ("readWideCharArrayzh", tReadMutableByteArrayzh tCharzh),
+ ("readIntArrayzh", tReadMutableByteArrayzh tIntzh),
+ ("readWordArrayzh", tReadMutableByteArrayzh tWordzh),
+ ("readAddrArrayzh", tReadMutableByteArrayzh tAddrzh),
+ ("readFloatArrayzh", tReadMutableByteArrayzh tFloatzh),
+ ("readDoubleArrayzh", tReadMutableByteArrayzh tDoublezh),
+ ("readStablePtrArrayzh", Tforall ("s",Klifted)
+ (Tforall ("a",Klifted)
+ (tArrow (tMutableByteArrayzh (Tvar "s"))
+ (tArrow tIntzh
+ (tArrow (tStatezh (Tvar "s"))
+ (tUtuple [tStatezh (Tvar "s"),tStablePtrzh (Tvar "a")])))))),
+ ("readInt8Arrayzh", tReadMutableByteArrayzh tIntzh),
+ ("readInt16Arrayzh", tReadMutableByteArrayzh tIntzh),
+ ("readInt32Arrayzh", tReadMutableByteArrayzh tInt32zh),
+ ("readInt64Arrayzh", tReadMutableByteArrayzh tInt64zh),
+ ("readWord8Arrayzh", tReadMutableByteArrayzh tWordzh),
+ ("readWord16Arrayzh", tReadMutableByteArrayzh tWordzh),
+ ("readWord32Arrayzh", tReadMutableByteArrayzh tWord32zh),
+ ("readWord64Arrayzh", tReadMutableByteArrayzh tWord64zh),
+
+ ("writeCharArrayzh", tWriteMutableByteArrayzh tCharzh),
+ ("writeWideCharArrayzh", tWriteMutableByteArrayzh tCharzh),
+ ("writeIntArrayzh", tWriteMutableByteArrayzh tIntzh),
+ ("writeWordArrayzh", tWriteMutableByteArrayzh tWordzh),
+ ("writeAddrArrayzh", tWriteMutableByteArrayzh tAddrzh),
+ ("writeFloatArrayzh", tWriteMutableByteArrayzh tFloatzh),
+ ("writeDoubleArrayzh", tWriteMutableByteArrayzh tDoublezh),
+ ("writeStablePtrArrayzh", Tforall ("s",Klifted)
+ (Tforall ("a",Klifted)
+ (tArrow (tMutableByteArrayzh (Tvar "s"))
+ (tArrow tIntzh
+ (tArrow (tStablePtrzh (Tvar "a"))
+ (tArrow (tStatezh (Tvar "s"))
+ (tStatezh (Tvar "s")))))))),
+ ("writeInt8Arrayzh", tWriteMutableByteArrayzh tIntzh),
+ ("writeInt16Arrayzh", tWriteMutableByteArrayzh tIntzh),
+ ("writeInt32Arrayzh", tWriteMutableByteArrayzh tIntzh),
+ ("writeInt64Arrayzh", tWriteMutableByteArrayzh tInt64zh),
+ ("writeWord8Arrayzh", tWriteMutableByteArrayzh tWordzh),
+ ("writeWord16Arrayzh", tWriteMutableByteArrayzh tWordzh),
+ ("writeWord32Arrayzh", tWriteMutableByteArrayzh tWord32zh),
+ ("writeWord64Arrayzh", tWriteMutableByteArrayzh tWord64zh),
+
+ ("indexCharOffAddrzh", tArrow tAddrzh (tArrow tIntzh tCharzh)),
+ ("indexWideCharOffAddrzh", tArrow tAddrzh (tArrow tIntzh tCharzh)),
+ ("indexIntOffAddrzh", tArrow tAddrzh (tArrow tIntzh tIntzh)),
+ ("indexWordOffAddrzh", tArrow tAddrzh (tArrow tIntzh tWordzh)),
+ ("indexAddrOffAddrzh", tArrow tAddrzh (tArrow tIntzh tAddrzh)),
+ ("indexFloatOffAddrzh", tArrow tAddrzh (tArrow tIntzh tFloatzh)),
+ ("indexDoubleOffAddrzh", tArrow tAddrzh (tArrow tIntzh tDoublezh)),
+ ("indexStablePtrOffAddrzh", Tforall ("a",Klifted) (tArrow tAddrzh (tArrow tIntzh (tStablePtrzh (Tvar "a"))))),
+ ("indexInt8OffAddrzh", tArrow tAddrzh (tArrow tIntzh tIntzh)),
+ ("indexInt16OffAddrzh", tArrow tAddrzh (tArrow tIntzh tIntzh)),
+ ("indexInt32OffAddrzh", tArrow tAddrzh (tArrow tIntzh tInt32zh)),
+ ("indexInt64OffAddrzh", tArrow tAddrzh (tArrow tIntzh tInt64zh)),
+ ("indexWord8OffAddrzh", tArrow tAddrzh (tArrow tIntzh tWordzh)),
+ ("indexWord16OffAddrzh", tArrow tAddrzh (tArrow tIntzh tWordzh)),
+ ("indexWord32ffAddrzh", tArrow tAddrzh (tArrow tIntzh tWord32zh)),
+ ("indexWord64OffAddrzh", tArrow tAddrzh (tArrow tIntzh tWord64zh)),
+
+ ("indexCharOffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tCharzh)),
+ ("indexWideCharOffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tCharzh)),
+ ("indexIntOffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tIntzh)),
+ ("indexWordOffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tWordzh)),
+ ("indexAddrOffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tAddrzh)),
+ ("indexFloatOffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tFloatzh)),
+ ("indexDoubleOffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tDoublezh)),
+ ("indexStablePtrOffForeignObjzh", Tforall ("a",Klifted) (tArrow tForeignObjzh (tArrow tIntzh (tStablePtrzh (Tvar "a"))))),
+ ("indexInt8OffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tIntzh)),
+ ("indexInt16OffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tIntzh)),
+ ("indexInt32OffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tInt32zh)),
+ ("indexInt64OffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tInt64zh)),
+ ("indexWord8OffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tWordzh)),
+ ("indexWord16OffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tWordzh)),
+ ("indexWord32ffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tWord32zh)),
+ ("indexWord64OffForeignObjzh", tArrow tForeignObjzh (tArrow tIntzh tWord64zh)),
+
+ ("readCharOffAddrzh", tReadOffAddrzh tCharzh),
+ ("readWideCharOffAddrzh", tReadOffAddrzh tCharzh),
+ ("readIntOffAddrzh", tReadOffAddrzh tIntzh),
+ ("readWordOffAddrzh", tReadOffAddrzh tWordzh),
+ ("readAddrOffAddrzh", tReadOffAddrzh tAddrzh),
+ ("readFloatOffAddrzh", tReadOffAddrzh tFloatzh),
+ ("readDoubleOffAddrzh", tReadOffAddrzh tDoublezh),
+ ("readStablePtrOffAddrzh", Tforall ("s",Klifted)
+ (Tforall ("a",Klifted)
+ (tArrow tAddrzh
+ (tArrow tIntzh
+ (tArrow (tStatezh (Tvar "s"))
+ (tUtuple [tStatezh (Tvar "s"),tStablePtrzh (Tvar "a")])))))),
+ ("readInt8OffAddrzh", tReadOffAddrzh tIntzh),
+ ("readInt16OffAddrzh", tReadOffAddrzh tIntzh),
+ ("readInt32OffAddrzh", tReadOffAddrzh tInt32zh),
+ ("readInt64OffAddrzh", tReadOffAddrzh tInt64zh),
+ ("readWord8OffAddrzh", tReadOffAddrzh tWordzh),
+ ("readWord16OffAddrzh", tReadOffAddrzh tWordzh),
+ ("readWord32OffAddrzh", tReadOffAddrzh tWord32zh),
+ ("readWord64OffAddrzh", tReadOffAddrzh tWord64zh),
+
+ ("writeCharOffAddrzh", tWriteOffAddrzh tCharzh),
+ ("writeWideCharOffAddrzh", tWriteOffAddrzh tCharzh),
+ ("writeIntOffAddrzh", tWriteOffAddrzh tIntzh),
+ ("writeWordOffAddrzh", tWriteOffAddrzh tWordzh),
+ ("writeAddrOffAddrzh", tWriteOffAddrzh tAddrzh),
+ ("writeFloatOffAddrzh", tWriteOffAddrzh tFloatzh),
+ ("writeDoubleOffAddrzh", tWriteOffAddrzh tDoublezh),
+ ("writeStablePtrOffAddrzh", Tforall ("a",Klifted) (tWriteOffAddrzh (tStablePtrzh (Tvar "a")))),
+ ("writeInt8OffAddrzh", tWriteOffAddrzh tIntzh),
+ ("writeInt16OffAddrzh", tWriteOffAddrzh tIntzh),
+ ("writeInt32OffAddrzh", tWriteOffAddrzh tInt32zh),
+ ("writeInt64OffAddrzh", tWriteOffAddrzh tInt64zh),
+ ("writeWord8OffAddrzh", tWriteOffAddrzh tWordzh),
+ ("writeWord16OffAddrzh", tWriteOffAddrzh tWordzh),
+ ("writeWord32OffAddrzh", tWriteOffAddrzh tWord32zh),
+ ("writeWord64OffAddrzh", tWriteOffAddrzh tWord64zh),
+
+ ("sameMutableArrayzh", Tforall ("s",Klifted)
+ (Tforall ("a",Klifted)
+ (tArrow (tMutableArrayzh (Tvar "s") (Tvar "a"))
+ (tArrow (tMutableArrayzh (Tvar "s") (Tvar "a"))
+ tBool)))),
+ ("sameMutableByteArrayzh", Tforall ("s",Klifted)
+ (tArrow (tMutableByteArrayzh (Tvar "s"))
+ (tArrow (tMutableByteArrayzh (Tvar "s"))
+ tBool))),
+ ("readArrayzh",Tforall ("s",Klifted)
+ (Tforall ("a",Klifted)
+ (tArrow (tMutableArrayzh (Tvar "s") (Tvar "a"))
+ (tArrow tIntzh
+ (tArrow (tStatezh (Tvar "s"))
+ (tUtuple[tStatezh (Tvar "s"), Tvar "a"])))))),
+ ("writeArrayzh",Tforall ("s",Klifted)
+ (Tforall ("a",Klifted)
+ (tArrow (tMutableArrayzh (Tvar "s") (Tvar "a"))
+ (tArrow tIntzh
+ (tArrow (Tvar "a")
+ (tArrow (tStatezh (Tvar "s"))
+ (tStatezh (Tvar "s")))))))),
+ ("indexArrayzh", Tforall ("a",Klifted)
+ (tArrow (tArrayzh (Tvar "a"))
+ (tArrow tIntzh
+ (tUtuple[Tvar "a"])))),
+ ("unsafeFreezzeArrayzh",Tforall ("s",Klifted)
+ (Tforall ("a",Klifted)
+ (tArrow (tMutableArrayzh (Tvar "s") (Tvar "a"))
+ (tArrow (tStatezh (Tvar "s"))
+ (tUtuple[tStatezh (Tvar "s"),tArrayzh (Tvar "a")]))))),
+ ("unsafeFreezzeByteArrayzh",Tforall ("s",Klifted)
+ (tArrow (tMutableByteArrayzh (Tvar "s"))
+ (tArrow (tStatezh (Tvar "s"))
+ (tUtuple[tStatezh (Tvar "s"),tByteArrayzh])))),
+ ("unsafeThawArrayzh",Tforall ("a",Klifted)
+ (Tforall ("s",Klifted)
+ (tArrow (tArrayzh (Tvar "a"))
+ (tArrow (tStatezh (Tvar "s"))
+ (tUtuple[tStatezh (Tvar "s"),tMutableArrayzh (Tvar "s") (Tvar "a")]))))),
+ ("sizzeofByteArrayzh", tArrow tByteArrayzh tIntzh),
+ ("sizzeofMutableByteArrayzh", Tforall ("s",Klifted) (tArrow (tMutableByteArrayzh (Tvar "s")) tIntzh))]
+ where
+ tReadMutableByteArrayzh t =
+ Tforall ("s",Klifted)
+ (tArrow (tMutableByteArrayzh (Tvar "s"))
+ (tArrow tIntzh
+ (tArrow (tStatezh (Tvar "s"))
+ (tUtuple [tStatezh (Tvar "s"),t]))))
+
+ tWriteMutableByteArrayzh t =
+ Tforall ("s",Klifted)
+ (tArrow (tMutableByteArrayzh (Tvar "s"))
+ (tArrow tIntzh
+ (tArrow t
+ (tArrow (tStatezh (Tvar "s"))
+ (tStatezh (Tvar "s"))))))
+
+ tReadOffAddrzh t =
+ Tforall ("s",Klifted)
+ (tArrow tAddrzh
+ (tArrow tIntzh
+ (tArrow (tStatezh (Tvar "s"))
+ (tUtuple [tStatezh (Tvar "s"),t]))))
+
+
+ tWriteOffAddrzh t =
+ Tforall ("s",Klifted)
+ (tArrow tAddrzh
+ (tArrow tIntzh
+ (tArrow t
+ (tArrow (tStatezh (Tvar "s"))
+ (tStatezh (Tvar "s"))))))
+
+{- MutVars -}
+
+tcMutVarzh = (primMname,"MutVarzh")
+tMutVarzh s t = Tapp (Tapp (Tcon tcMutVarzh) s) t
+ktMutVarzh = Karrow Klifted (Karrow Klifted Kunlifted)
+
+opsMutVarzh = [
+ ("newMutVarzh", Tforall ("a",Klifted)
+ (Tforall ("s",Klifted)
+ (tArrow (Tvar "a") (tArrow (tStatezh (Tvar "s"))
+ (tUtuple [tStatezh (Tvar "s"),
+ tMutVarzh (Tvar "s") (Tvar "a")]))))),
+ ("readMutVarzh", Tforall ("s",Klifted)
+ (Tforall ("a",Klifted)
+ (tArrow (tMutVarzh (Tvar "s")(Tvar "a"))
+ (tArrow (tStatezh (Tvar "s"))
+ (tUtuple [tStatezh (Tvar "s"), Tvar "a"]))))),
+ ("writeMutVarzh", Tforall ("s",Klifted)
+ (Tforall ("a",Klifted)
+ (tArrow (tMutVarzh (Tvar "s") (Tvar "a"))
+ (tArrow (Tvar "a")
+ (tArrow (tStatezh (Tvar "s"))
+ (tStatezh (Tvar "s"))))))),
+ ("sameMutVarzh", Tforall ("s",Klifted)
+ (Tforall ("a",Klifted)
+ (tArrow (tMutVarzh (Tvar "s") (Tvar "a"))
+ (tArrow (tMutVarzh (Tvar "s") (Tvar "a"))
+ tBool))))]
+
+{- Real world and state. -}
+
+tcRealWorld = (primMname,"RealWorld")
+tRealWorld = Tcon tcRealWorld
+ktRealWorld = Klifted
+
+tcStatezh = (primMname, "Statezh")
+tStatezh t = Tapp (Tcon tcStatezh) t
+ktStatezh = Karrow Klifted Kunlifted
+
+tRWS = tStatezh tRealWorld
+
+opsState = [
+ ("realWorldzh", tRWS)]
+
+{- Exceptions -}
+
+-- no primitive type
+opsExn = [
+ ("catchzh",
+ let t' = tArrow tRWS (tUtuple [tRWS, Tvar "a"]) in
+ Tforall ("a",Klifted)
+ (Tforall ("b",Klifted)
+ (tArrow t'
+ (tArrow (tArrow (Tvar "b") t')
+ t')))),
+ ("raisezh", Tforall ("a",Klifted)
+ (Tforall ("b",Klifted)
+ (tArrow (Tvar "a") (Tvar "b")))),
+ ("blockAsyncExceptionszh", Tforall ("a",Klifted)
+ (tArrow (tArrow tRWS (tUtuple[tRWS,Tvar "a"]))
+ (tArrow tRWS (tUtuple[tRWS,Tvar "a"])))),
+ ("unblockAsyncExceptionszh", Tforall ("a",Klifted)
+ (tArrow (tArrow tRWS (tUtuple[tRWS,Tvar "a"]))
+ (tArrow tRWS (tUtuple[tRWS,Tvar "a"]))))]
+
+{- Mvars -}
+
+tcMVarzh = (primMname, "MVarzh")
+tMVarzh s t = Tapp (Tapp (Tcon tcMVarzh) s) t
+ktMVarzh = Karrow Klifted (Karrow Klifted Kunlifted)
+
+opsMVar = [
+ ("newMVarzh", Tforall ("s",Klifted)
+ (Tforall ("a",Klifted)
+ (tArrow (tStatezh (Tvar "s"))
+ (tUtuple[tStatezh (Tvar "s"),tMVarzh (Tvar "s") (Tvar "a")])))),
+ ("takeMVarzh", Tforall ("s",Klifted)
+ (Tforall ("a",Klifted)
+ (tArrow (tMVarzh (Tvar "s") (Tvar "a"))
+ (tArrow (tStatezh (Tvar "s"))
+ (tUtuple[tStatezh (Tvar "s"),Tvar "a"]))))),
+ ("tryTakeMVarzh", Tforall ("s",Klifted)
+ (Tforall ("a",Klifted)
+ (tArrow (tMVarzh (Tvar "s") (Tvar "a"))
+ (tArrow (tStatezh (Tvar "s"))
+ (tUtuple[tStatezh (Tvar "s"),tIntzh,Tvar "a"]))))),
+ ("putMVarzh", Tforall ("s",Klifted)
+ (Tforall ("a",Klifted)
+ (tArrow (tMVarzh (Tvar "s") (Tvar "a"))
+ (tArrow (Tvar "a")
+ (tArrow (tStatezh (Tvar "s"))
+ (tStatezh (Tvar "s"))))))),
+ ("tryPutMVarzh", Tforall ("s",Klifted)
+ (Tforall ("a",Klifted)
+ (tArrow (tMVarzh (Tvar "s") (Tvar "a"))
+ (tArrow (Tvar "a")
+ (tArrow (tStatezh (Tvar "s"))
+ (tUtuple [tStatezh (Tvar "s"), tIntzh])))))),
+ ("sameMVarzh", Tforall ("s",Klifted)
+ (Tforall ("a",Klifted)
+ (tArrow (tMVarzh (Tvar "s") (Tvar "a"))
+ (tArrow (tMVarzh (Tvar "s") (Tvar "a"))
+ tBool)))),
+ ("isEmptyMVarzh", Tforall ("s",Klifted)
+ (Tforall ("a",Klifted)
+ (tArrow (tMVarzh (Tvar "s") (Tvar "a"))
+ (tArrow (tStatezh (Tvar "s"))
+ (tUtuple[tStatezh (Tvar "s"),tIntzh])))))]
+
+
+{- Weak Objects -}
+
+tcWeakzh = (primMname, "Weakzh")
+tWeakzh t = Tapp (Tcon tcWeakzh) t
+ktWeakzh = Karrow Klifted Kunlifted
+
+opsWeak = [
+ ("mkWeakzh", Tforall ("o",Kopen)
+ (Tforall ("b",Klifted)
+ (Tforall ("c",Klifted)
+ (tArrow (Tvar "o")
+ (tArrow (Tvar "b")
+ (tArrow (Tvar "c")
+ (tArrow tRWS (tUtuple[tRWS, tWeakzh (Tvar "b")])))))))),
+ ("deRefWeakzh", Tforall ("a",Klifted)
+ (tArrow (tWeakzh (Tvar "a"))
+ (tArrow tRWS (tUtuple[tRWS, tIntzh, Tvar "a"])))),
+ ("finalizeWeakzh", Tforall ("a",Klifted)
+ (tArrow (tWeakzh (Tvar "a"))
+ (tArrow tRWS
+ (tUtuple[tRWS,tIntzh,
+ tArrow tRWS (tUtuple[tRWS, tUnit])]))))]
+
+
+{- Foreign Objects -}
+
+tcForeignObjzh = (primMname, "ForeignObjzh")
+tForeignObjzh = Tcon tcForeignObjzh
+ktForeignObjzh = Kunlifted
+
+opsForeignObjzh = [
+ ("mkForeignObjzh", tArrow tAddrzh
+ (tArrow tRWS (tUtuple [tRWS,tForeignObjzh]))),
+ ("writeForeignObjzh", Tforall ("s",Klifted)
+ (tArrow tForeignObjzh
+ (tArrow tAddrzh
+ (tArrow (tStatezh (Tvar "s")) (tStatezh (Tvar "s")))))),
+ ("foreignObjToAddrzh", tArrow tForeignObjzh tAddrzh),
+ ("touchzh", Tforall ("o",Kopen)
+ (tArrow (Tvar "o")
+ (tArrow tRWS tRWS)))]
+
+
+{- Stable Pointers (but not names) -}
+
+tcStablePtrzh = (primMname, "StablePtrzh")
+tStablePtrzh t = Tapp (Tcon tcStablePtrzh) t
+ktStablePtrzh = Karrow Klifted Kunlifted
+
+opsStablePtrzh = [
+ ("makeStablePtrzh", Tforall ("a",Klifted)
+ (tArrow (Tvar "a")
+ (tArrow tRWS (tUtuple[tRWS,tStablePtrzh (Tvar "a")])))),
+ ("deRefStablePtrzh", Tforall ("a",Klifted)
+ (tArrow (tStablePtrzh (Tvar "a"))
+ (tArrow tRWS (tUtuple[tRWS,Tvar "a"])))),
+ ("eqStablePtrzh", Tforall ("a",Klifted)
+ (tArrow (tStablePtrzh (Tvar "a"))
+ (tArrow (tStablePtrzh (Tvar "a")) tIntzh)))]
+
+{- Concurrency operations -}
+
+tcThreadIdzh = (primMname,"ThreadIdzh")
+tThreadIdzh = Tcon tcThreadIdzh
+ktThreadIdzh = Kunlifted
+
+opsConc = [
+ ("seqzh", Tforall ("a",Klifted)
+ (tArrow (Tvar "a") tIntzh)),
+ ("parzh", Tforall ("a",Klifted)
+ (tArrow (Tvar "a") tIntzh)),
+ ("delayzh", Tforall ("s",Klifted)
+ (tArrow tIntzh (tArrow (tStatezh (Tvar "s")) (tStatezh (Tvar "s"))))),
+ ("waitReadzh", Tforall ("s",Klifted)
+ (tArrow tIntzh (tArrow (tStatezh (Tvar "s")) (tStatezh (Tvar "s"))))),
+ ("waitWritezh", Tforall ("s",Klifted)
+ (tArrow tIntzh (tArrow (tStatezh (Tvar "s")) (tStatezh (Tvar "s"))))),
+ ("forkzh", Tforall ("a",Klifted)
+ (tArrow (Tvar "a")
+ (tArrow tRWS (tUtuple[tRWS,tThreadIdzh])))),
+ ("killThreadzh", Tforall ("a",Klifted)
+ (tArrow tThreadIdzh
+ (tArrow (Tvar "a")
+ (tArrow tRWS tRWS)))),
+ ("yieldzh", tArrow tRWS tRWS),
+ ("myThreadIdzh", tArrow tRWS (tUtuple[tRWS, tThreadIdzh]))]
+
+{- Miscellaneous operations -}
+
+opsMisc = [
+ ("dataToTagzh", Tforall ("a",Klifted)
+ (tArrow (Tvar "a") tIntzh)),
+ ("tagToEnumzh", Tforall ("a",Klifted)
+ (tArrow tIntzh (Tvar "a"))),
+ ("unsafeCoercezh", Tforall ("a",Kopen)
+ (Tforall ("b",Kopen)
+ (tArrow (Tvar "a") (Tvar "b")))) -- maybe unneeded
+ ]
+
+{- CCallable and CReturnable.
+ We just define the type constructors for the dictionaries
+ corresponding to these pseudo-classes. -}
+
+tcZCTCCallable = (primMname,"ZCTCCallable")
+ktZCTCCallable = Karrow Kopen Klifted -- ??
+tcZCTCReturnable = (primMname,"ZCTCReturnable")
+ktZCTCReturnable = Karrow Kopen Klifted -- ??
+
+{- Non-primitive, but mentioned in the types of primitives. -}
+
+tcUnit = ("PrelBase","Unit")
+tUnit = Tcon tcUnit
+ktUnit = Klifted
+tcBool = ("PrelBase","Bool")
+tBool = Tcon tcBool
+ktBool = Klifted
+
+{- Properly defined in PrelError, but needed in many modules before that. -}
+errorVals = [
+ ("error", Tforall ("a",Kopen) (tArrow tString (Tvar "a"))),
+ ("irrefutPatError", Tforall ("a",Kopen) (tArrow tString (Tvar "a"))),
+ ("patError", Tforall ("a",Kopen) (tArrow tString (Tvar "a")))]
+
+tcChar = ("PrelBase","Char")
+tChar = Tcon tcChar
+ktChar = Klifted
+tcList = ("PrelBase","ZMZN")
+tList t = Tapp (Tcon tcList) t
+ktList = Karrow Klifted Klifted
+tString = tList tChar
+
+{- Utilities for building types -}
+tmonadic t = tArrow t t
+tdyadic t = tArrow t (tArrow t t)
+tcompare t = tArrow t (tArrow t tBool)
+
diff --git a/utils/ext-core/Printer.hs b/utils/ext-core/Printer.hs
new file mode 100644
index 0000000000..ded48aadc2
--- /dev/null
+++ b/utils/ext-core/Printer.hs
@@ -0,0 +1,163 @@
+module Printer where
+
+import Pretty
+import Core
+import Char
+import Numeric (fromRat)
+
+instance Show Module where
+ showsPrec d m = shows (pmodule m)
+
+instance Show Tdef where
+ showsPrec d t = shows (ptdef t)
+
+instance Show Cdef where
+ showsPrec d c = shows (pcdef c)
+
+instance Show Vdefg where
+ showsPrec d v = shows (pvdefg v)
+
+instance Show Vdef where
+ showsPrec d v = shows (pvdef v)
+
+instance Show Exp where
+ showsPrec d e = shows (pexp e)
+
+instance Show Alt where
+ showsPrec d a = shows (palt a)
+
+instance Show Ty where
+ showsPrec d t = shows (pty t)
+
+instance Show Kind where
+ showsPrec d k = shows (pkind k)
+
+instance Show Lit where
+ showsPrec d l = shows (plit l)
+
+
+indent = nest 2
+
+pmodule (Module mname tdefs vdefgs) =
+ (text "%module" <+> text mname)
+ $$ indent ((vcat (map ((<> char ';') . ptdef) tdefs))
+ $$ (vcat (map ((<> char ';') . pvdefg) vdefgs)))
+
+ptdef (Data qtcon tbinds cdefs) =
+ (text "%data" <+> pqname qtcon <+> (hsep (map ptbind tbinds)) <+> char '=')
+ $$ indent (braces ((vcat (punctuate (char ';') (map pcdef cdefs)))))
+
+ptdef (Newtype qtcon tbinds tyopt ) =
+ text "%newtype" <+> pqname qtcon <+> (hsep (map ptbind tbinds)) <+>
+ (case tyopt of
+ Just ty -> char '=' <+> pty ty
+ Nothing -> empty)
+
+pcdef (Constr qdcon tbinds tys) =
+ (pqname qdcon) <+> (sep [hsep (map pattbind tbinds),sep (map paty tys)])
+
+pname id = text id
+
+pqname ("",id) = pname id
+pqname (m,id) = pname m <> char '.' <> pname id
+
+ptbind (t,Klifted) = pname t
+ptbind (t,k) = parens (pname t <> text "::" <> pkind k)
+
+pattbind (t,k) = char '@' <> ptbind (t,k)
+
+pakind (Klifted) = char '*'
+pakind (Kunlifted) = char '#'
+pakind (Kopen) = char '?'
+pakind k = parens (pkind k)
+
+pkind (Karrow k1 k2) = parens (pakind k1 <> text "->" <> pkind k2)
+pkind k = pakind k
+
+paty (Tvar n) = pname n
+paty (Tcon c) = pqname c
+paty t = parens (pty t)
+
+pbty (Tapp(Tapp(Tcon tc) t1) t2) | tc == tcArrow = parens(fsep [pbty t1, text "->",pty t2])
+pbty (Tapp t1 t2) = pappty t1 [t2]
+pbty t = paty t
+
+pty (Tapp(Tapp(Tcon tc) t1) t2) | tc == tcArrow = fsep [pbty t1, text "->",pty t2]
+pty (Tforall tb t) = text "%forall" <+> pforall [tb] t
+pty t = pbty t
+
+pappty (Tapp t1 t2) ts = pappty t1 (t2:ts)
+pappty t ts = sep (map paty (t:ts))
+
+pforall tbs (Tforall tb t) = pforall (tbs ++ [tb]) t
+pforall tbs t = hsep (map ptbind tbs) <+> char '.' <+> pty t
+
+pvdefg (Rec vdefs) = text "%rec" $$ braces (indent (vcat (punctuate (char ';') (map pvdef vdefs))))
+pvdefg (Nonrec vdef) = pvdef vdef
+
+pvdef (Vdef (qv,t,e)) = sep [pqname qv <+> text "::" <+> pty t <+> char '=',
+ indent (pexp e)]
+
+paexp (Var x) = pqname x
+paexp (Dcon x) = pqname x
+paexp (Lit l) = plit l
+paexp e = parens(pexp e)
+
+plamexp bs (Lam b e) = plamexp (bs ++ [b]) e
+plamexp bs e = sep [sep (map pbind bs) <+> text "->",
+ indent (pexp e)]
+
+pbind (Tb tb) = char '@' <+> ptbind tb
+pbind (Vb vb) = pvbind vb
+
+pfexp (App e1 e2) = pappexp e1 [Left e2]
+pfexp (Appt e t) = pappexp e [Right t]
+pfexp e = paexp e
+
+pappexp (App e1 e2) as = pappexp e1 (Left e2:as)
+pappexp (Appt e t) as = pappexp e (Right t:as)
+pappexp e as = fsep (paexp e : map pa as)
+ where pa (Left e) = paexp e
+ pa (Right t) = char '@' <+> paty t
+
+pexp (Lam b e) = char '\\' <+> plamexp [b] e
+pexp (Let vd e) = (text "%let" <+> pvdefg vd) $$ (text "%in" <+> pexp e)
+pexp (Case e vb alts) = sep [text "%case" <+> paexp e,
+ text "%of" <+> pvbind vb]
+ $$ (indent (braces (vcat (punctuate (char ';') (map palt alts)))))
+pexp (Coerce t e) = (text "%coerce" <+> paty t) $$ pexp e
+pexp (Note s e) = (text "%note" <+> pstring s) $$ pexp e
+pexp (External n t) = (text "%extcall" <+> pstring n) $$ paty t
+pexp e = pfexp e
+
+
+pvbind (x,t) = parens(pname x <> text "::" <> pty t)
+
+palt (Acon c tbs vbs e) =
+ sep [pqname c,
+ sep (map pattbind tbs),
+ sep (map pvbind vbs) <+> text "->"]
+ $$ indent (pexp e)
+palt (Alit l e) =
+ (plit l <+> text "->")
+ $$ indent (pexp e)
+palt (Adefault e) =
+ (text "%_ ->")
+ $$ indent (pexp e)
+
+plit (Lint i t) = parens (integer i <> text "::" <> pty t)
+plit (Lrational r t) = parens (text (show (fromRat r)) <> text "::" <> pty t)
+plit (Lchar c t) = parens (text ("\'" ++ escape [c] ++ "\'") <> text "::" <> pty t)
+plit (Lstring s t) = parens (pstring s <> text "::" <> pty t)
+
+pstring s = doubleQuotes(text (escape s))
+
+escape s = foldr f [] (map ord s)
+ where
+ f cv rest | (cv < 0x20 || cv > 0x7e || cv == 0x22 || cv == 0x27 || cv == 0x5c) =
+ '\\':'x':h1:h0:rest
+ where (q1,r1) = quotRem cv 16
+ h1 = intToDigit q1
+ h0 = intToDigit r1
+ f cv rest = (chr cv):rest
+
diff --git a/utils/ext-core/README b/utils/ext-core/README
new file mode 100644
index 0000000000..7ec8adf09a
--- /dev/null
+++ b/utils/ext-core/README
@@ -0,0 +1,9 @@
+A set of example programs for handling external core format.
+
+In particular, typechecker and interpreter give a precise semantics.
+
+All can be built using, e.g.,
+
+happy -o Parser.hs Parser.y
+ghc --make -package text -fglasgow-exts -o Driver Driver.hs
+