Typprüfung für System F_w mit CASE und PAIR

Markus Bleicher

Contents

"Rank 2 types break all the standard typing algorithms. We can only do type checking by making rather draconian restrictions." ¹

1  Das Problem

2  Typen und Typsysteme

2.1  Sprache

2.2  Das General Type System Kalkül

2.2.1  Regeln für Kinds

2.2.2  Regeln für Konstruktoren

2.2.3  Regeln für Terme

2.2.4  Und die Abschwächungsregel

2.3  Kalküle

Chapter 1
System F_w und Erweiterungen

1  System F_w

1.1  Sprache und Notation

1.2  Der Kalkül von System F_w

1.3  Terme für F_w im Church style

1.4  Syntaxgeleitete Version des Kalküls

1.5  Äquivalenzbeweis

1.6  Notation: Rang und F_w⁽ⁿ⁾

2  System F_w mit CASE und PAIR³

2.1  Curry Style

2.2  syntaxgeleitete Version

2.3  Äquivalenzbeweis

2.4  Church Style

3  syntaxgeleitete Kalküle

4  annotierte Syntaxbäume

5  Algorithmen und Semi-Algorithmen zur Typprüfung

6  Der Semiunifikations-Algorithmus

6.1  Matching, Semiunifikation, Unifikation

6.2  Der Unifikations-Algorithmus von Huet

6.3  Matching-Algorithmus

7  Ein Algorithmus zur Typgewinnung

8  Hierarchie der betrachteten Probleme

9  Typsysteme von Programmiersprachen

9.1  bidirektionale Typprüfung

9.2  entscheidbare Typsysteme

9.3  Ponder

Chapter 2
Die Implementierung

1  Datentypen und Abstraktion

2  Der Parser

3  Der Pretty-Printer

4  Hilfsfunktionen

5  Der Algorithmus zur vollständigen Annotation

6  Der Typprüfer

7  Beispiele

7.1  Kombinatoren

7.2  Church-Ziffern

7.3  Verschiedenes

7.3.1  Zurückweisung einer Übergeneralisierung

7.3.2  Getypte Kombinatoren S K

7.3.3  Typ von Urzyczyns 22K

7.3.4  Einfache Paarbildung

7.4  Montoniezeugen

Chapter 3
Anhang

1  Die Programme

1.1  Die Datentypen mit show

-- these are datatypes for system F_omega typed lambda expressions with CASE
-- and PAIR rules. All a la Church with Maybe type assignments
-- they can also be used to represent Curry terms
-- $Id: CPFwDatatypes.hs,v 1.12 2002/05/01 18:29:35 markus Exp $

module CPFwDatatypes where

import List(notElem, intersect)
import Maybe(fromJust, isJust)

infix ::: 
infix ::^

-- Exp, Type and Kind extraction
-- smells like a class, but Exp has to be a "real" type, so i don't know how
-- to create one

tm :: Exp->UntypedExp
tm (e ::: _) = e

ty :: Exp->Maybe Type
ty (_ ::: t) = t
jty = fromJust . ty

con :: Type->UnkindedType
con (t ::^ _) = t

kd :: Type->Maybe Kind
kd (_ ::^ k) = k
jkd = fromJust . kd

-- conditional show
cs b br = if b then br else ""

data OpStyle = Base | LeftAss | RightAss | Non | Post | Pre deriving Eq

data Binary = Function | Prod | Sum deriving Eq
instance Show Binary where
  show Function = "->"
  show Prod = "%"
  show Sum = "+"
instance Read Binary where
  readsPrec _ ('-':'>':r) = [(Function, r)]
  readsPrec _ ('%':r) = [(Prod, r)]
  readsPrec _ ('+':r) = [(Sum, r)]
  readsPrec _ _ = []

data LR = L | R deriving (Show, Read, Eq) 

class Show_ a where
  show_ :: Bool -> a -> String

class Prec a where
  prec :: a -> (Int, OpStyle)

-- precProb(T) (not a class because of Haskell limitations)
-- if the precedence of the outer (upper in a parse tree) is higher or equal
-- as the inner and the operator style makes it possible, brackets are
-- neccesary to avoid "stealing"

data UntypedExp
      = Abs Exp Exp
      | Inst Exp Type
      | Gen Type Exp
      | App Exp Exp
      | Var String
      | Case Exp Exp Exp Exp Exp
      | InLR LR Exp
      | Pair Exp Exp
      | Lr LR Exp
     deriving Eq
instance Show UntypedExp where
  show = show_ True -- first arg says whether term is in front of a closing
                    -- bracket to bracket \ . correctly 

instance Prec UntypedExp where
  prec (Abs _ _) = (1000, Pre)
  prec (Gen _ _) = (1000, Pre)
  prec (InLR _ _) = (500, Pre)
  prec (App _ _) = (100, LeftAss)
  prec (Inst _ _) = (100, Post)
  prec (Case _ _ _ _ _) = (700, Post)
  prec (Lr _ _) = (200, Post)
  prec (Var _) = (0, Base)
  prec (Pair _ _) = (0, Base)

precProb ops out (inn ::: t) =
     (fst (prec out) < fst (prec inn)
       && (snd (prec inn) `notElem` (ops `intersect` [Post, Pre])))
  || (fst (prec out) == fst (prec inn) 
       && (snd (prec inn) `notElem` ops)
  || isJust t)

instance Show_ UntypedExp where
  -- dot structures (prefix), lowest prec so no testing neccesary 
  show_ b (Abs v t) =
    let p = precProb [Pre] (Abs v t) t in
    cs (not b) "("++"\\"++show_ False v++"."++
    cs p "("++show_ True t++cs p ")"++cs (not b) ")"
  show_ b (Gen v t) =
    let p = precProb [Pre] (Gen v t) t in
    cs (not b) "("++"/\\"++show_ False v++"."++
    cs p "("++show_ True t++cs p ")"++cs (not b) ")"

  -- prefix
  show_ _ (InLR c e) | precProb [Pre] (InLR c e) e =
    "IN"++show c++" ("++show_ True e++")"
  show_ b (InLR c e) = "IN"++show c++" "++show_ b e

  -- apps
  show_ b (App t1 t2) =
    let lp = precProb [Post, LeftAss] (App t1 t2) t1
        rp = precProb [Pre] (App t1 t2) t2 in
    cs lp "("++show_ lp t1++cs lp ")"++" "++
    cs rp "("++show_ (rp||b) t2++cs rp ")"
  show_ b (Inst t (ty ::^ k)) =
    let lp = precProb [Post, LeftAss] (Inst t (ty ::^ k)) t
        rp = case prec ty of (_, Base) -> False 
                             _ -> True in
    cs lp "("++show_ (lp||b) t++cs lp ")"++" "++
    cs rp "("++show_ (rp||b) (ty ::^ k)++cs rp ")"

  -- postfix
  show_ _ (Case inlr vl tl vr tr) = 
    let p = precProb [Post, LeftAss] (Case inlr vl tl vr tr) inlr in
    cs p "("++ show_ p inlr++cs p ")"++
    "{"++show vl++"."++show_ True tl++", "++
    show vr++"."++show_ True tr++"}"
  show_ b (Lr c e) =
    let p = precProb [Post, LeftAss] (Lr c e) e in
    cs p "("++show_ (b||p) e++cs p ")"++" "++show c

  -- simple cases
  show_ _ (Var v) = v
  show_ _ (Pair t1 t2) = "<"++show_ True t1++", "++show_ True t2++">"

  -- ERROR
  show_ _ _ = "UntypedExp show_: no rule applies."

data UnkindedType
      = TypeVar String
      | TypeBinary Binary Type Type
      | TypeLambda Type Type
      | TypeApp Type Type
      | Forall Type Type
     deriving Eq
instance Show UnkindedType where
  show = show_ True -- first arg says whether term is in front of a closing
                    -- bracket to bracket \ . correctly

instance Prec UnkindedType where
  prec (TypeLambda _ _) = (1000, Pre)
  prec (Forall _ _) = (1000, Pre)
  prec (TypeBinary Function _ _) = (700, RightAss)
  prec (TypeBinary Sum _ _) = (600, LeftAss)
  prec (TypeBinary Prod _ _) = (500, LeftAss)
  prec (TypeApp _ _) = (100, LeftAss)
  prec (TypeVar _) = (0, Base)

precProbT ops out (inn ::^ t) =
     (fst (prec out) < fst (prec inn)
       && (snd (prec inn) `notElem` (ops `intersect` [Post, Pre])))
  || (fst (prec out) == fst (prec inn) 
       && (snd (prec inn) `notElem` ops))

instance Show_ UnkindedType where
  show_ _ (TypeVar tv) = tv

  -- brackets if necessary
  show_ b (TypeLambda tv t) =
    cs (not b) "("++"\\"++show_ False tv++"."++show_ True t++cs (not b) ")"
  show_ b (Forall tv t) =
    cs (not b) "("++"&"++show_ False tv++"."++show_ True t++cs (not b) ")" 

  -- binary infix operators + % ->
  show_ b (TypeBinary op t1 t2) =
    let lp = precProbT [Post, LeftAss] (TypeBinary op t1 t2) t1
        rp = precProbT [Pre, RightAss] (TypeBinary op t1 t2) t2 in
    cs lp "("++show_ lp t1++cs lp ")"++show op++
    cs rp "("++show_ (rp||b) t2++cs rp ")"

  -- apps
  show_ b (TypeApp t1 t2) =
    let lp = precProbT [Post, LeftAss] (TypeApp t1 t2) t1
        rp = precProbT [Pre, RightAss] (TypeApp t1 t2) t2 in
    cs lp "("++show_ lp t1++cs lp ")"++" "++
    cs rp "("++show_ (rp||b) t2++cs rp ")"

  -- base types
  show_ _ (TypeVar v) = v

  -- ERROR
  show_ _ _ = error "UnkindedType show_: no rule applies."

data Kind
      = KindProp
      | KindAbs Kind Kind
     deriving Eq
instance Show Kind where
  show KindProp = "*"
  show (KindAbs (KindAbs k11 k12) k2) =
         "("++show (KindAbs k11 k12)++")=>"++show k2
  show (KindAbs k1 k2) = show k1++"=>"++show k2

data Type = UnkindedType ::^ Maybe Kind deriving Eq

instance Show Type where
  show = show_ True
instance Show_ Type where
  show_ b (utype ::^ Nothing) = show_ b utype
  show_ b (utype ::^ Just kind) =
    let br = case prec utype of (_, Base) -> False
                                _ -> True in
    cs br "("++show_ (br||b) utype++cs br ")"++"^"++show kind

data Exp = UntypedExp ::: Maybe Type deriving Eq

instance Show Exp where
  show = show_ True
instance Show_ Exp where
  show_ b (uexp ::: Nothing) = show_ b uexp
  show_ b (uexp ::: Just (t ::^ k)) =
    show_ b uexp++":"++show_ b (t ::^ k)
 

1.2  Der Parser

-- this is a "happy" parser for system F_omega typed lambda
-- expressions with CASE and PAIR rules. All a la Church with
-- Maybe type assignments they can also be used to represent
-- Curry terms
-- $Id: ParseCPFw.y,v 1.12 2002/05/01 18:29:36 markus Exp $

{
module ParseCPFw where
import Char(isAlpha, isAlphaNum, isSpace, isUpper, isLower)
import CPFwDatatypes(Exp(..), Type(..), Kind(..),
                     UntypedExp(..), UnkindedType(..), Binary(..))

}

%name parser Exp
%tokentype { Token }

%token '\\'  { TokenAbs }
       '.'  { TokenDot }
       var  { TokenVar $$ }
       tvar { TokenTypVar $$ }
       ':'  { TokenColon }
       '&'  { TokenForall }
       '/\\' { TokenAlpha }
       '^'  { TokenUp }
       '+' { TokenPlus }
       '%' { TokenTimes }
       '->' { TokenArrow }
       'LR' { TokenLR $$ }
       'INLR' { TokenINLR $$ }
       '*'  { TokenStar }
       '=>' { TokenDoubleArrow }
       '('  { TokenOB }
       ')'  { TokenCB }
       '{'  { TokenCOB }
       '}'  { TokenCCB }
       ','  { TokenComma }
       '<'  { TokenROB }
       '>'  { TokenRCB }

-- precedence: earlier means lower

%nonassoc ':' -- type applicator

-- IN(L|R)
-- \ . lambda
-- /\ . Alpha

-- { } case
-- left: LR, church app, curry app

-- base:
-- Var
-- < , > pair
-- ( ) brackets

%left '%' -- % case type
%left '+' -- + pair type
%right '->' -- type abstractor

%right '=>' -- kind abstractor

%nonassoc '^' -- kind applicator

%monad { P } { thenP } { returnP }
%lexer { monadiclexer } { TokenEOF }

%%

-- EXP RULES

SimpleExp :: { Exp }
        : var { Var $1 ::: Nothing }
        | '<' Exp ',' Exp '>' { Pair $2 $4 ::: Nothing }
        | '(' Exp ')' { $2 }

-- left assoc. and postfix operators
AppExp :: { Exp }
        : SimpleExp { $1 }
        | AppExp SimpleExp { App $1 $2 ::: Nothing }
        | AppExp SimpleType { Inst $1 $2 ::: Nothing }
	| AppExp 'LR' { Lr (read $2) $1 ::: Nothing }
        | AppExp '{' Exp '.' Exp ',' Exp '.' Exp '}'
          {% case ($3, $7) of
             (Var v1 ::: t1, Var v2 ::: t2) ->
               returnP (Case $1 (Var v1 ::: t1) $5 (Var v2 ::: t2) $9
                          ::: Nothing)
             (v1, v2) ->
               failP ("CASE, where "++show v1++" or "++show v2++
                      " are no variables.") 
          }             

-- expression with unbracketed prefix operators
NoBrakExp :: { Exp }
	: AppExp { $1 }
	| AppExp PreExp { App $1 $2 ::: Nothing }
	| PreExp { $1 }

-- prefix operators
PreExp :: { Exp }
	: 'INLR' NoBrakExp  { InLR (read $1) $2 ::: Nothing }
        | '\\' Exp '.' NoBrakExp
          {% case $2 of { Var v ::: t -> returnP (Abs (Var v ::: t)
                                                      $4
                                                    ::: Nothing)
                        ; e -> failP ("Abstraction of "++show e++
                                      "which is no variable.")
                        }
          }
        | '/\\' Type '.' NoBrakExp
          {% case $2 of { TypeVar v ::^ k -> returnP (Gen (TypeVar v ::^ k)
                                                          $4
                                                       ::: Nothing)
                        ; e -> failP ("GEN of "++show e++
                                      "which is no type variable.")
                        }
          }

Exp :: { Exp }
	: NoBrakExp { $1 }
	| Exp ':' Type {% case $1 of
                            uexp ::: Nothing -> returnP (uexp ::: Just $3)
                            _ -> failP "Double typing is not allowed" }


-- TYPE RULES

TypeVar :: { Type }
	: tvar { TypeVar $1 ::^ Nothing }
	| tvar '^' Kind { TypeVar $1 ::^ Just $3 } 

SimpleType :: { Type }
	: TypeVar { $1 }
	| '(' Type ')' { $2 }
	| '(' Type ')' '^' Kind
            {% case $2 of
                 utype ::^ Nothing -> returnP (utype ::^ Just $5)
                 _ -> failP "Double kinding is not allowed" }

AppType :: { Type }
	: AppType SimpleType { TypeApp $1 $2 ::^ Nothing }
	| SimpleType { $1 }

BinType :: { Type }
--	: AppType { $1 }
	: AppType '+' PreType { TypeBinary Sum $1 $3 ::^ Nothing }
	| AppType '%' PreType { TypeBinary Prod $1 $3 ::^ Nothing }
	| AppType '->' PreType { TypeBinary Function $1 $3 ::^ Nothing }

	| BinType '+' PreType { TypeBinary Sum $1 $3 ::^ Nothing }
	| BinType '%' PreType { TypeBinary Prod $1 $3 ::^ Nothing }
	| BinType '->' PreType { TypeBinary Function $1 $3 ::^ Nothing }

	| AppType '+' BinType { TypeBinary Sum $1 $3 ::^ Nothing }
	| AppType '%' BinType { TypeBinary Prod $1 $3 ::^ Nothing }
	| AppType '->' BinType { TypeBinary Function $1 $3 ::^ Nothing }

	| BinType '+' BinType { TypeBinary Sum $1 $3 ::^ Nothing }
	| BinType '%' BinType { TypeBinary Prod $1 $3 ::^ Nothing }
	| BinType '->' BinType { TypeBinary Function $1 $3 ::^ Nothing }

	| AppType '+' AppType { TypeBinary Sum $1 $3 ::^ Nothing }
	| AppType '%' AppType { TypeBinary Prod $1 $3 ::^ Nothing }
	| AppType '->' AppType { TypeBinary Function $1 $3 ::^ Nothing }

	| BinType '+' AppType { TypeBinary Sum $1 $3 ::^ Nothing }
	| BinType '%' AppType { TypeBinary Prod $1 $3 ::^ Nothing }
	| BinType '->' AppType { TypeBinary Function $1 $3 ::^ Nothing }

-- types with unbracketed prefix operators
Type :: { Type }
	: PreType { $1 }
	| BinType { $1 }
	| AppType { $1 }
	| AppType PreType { TypeApp $1 $2 ::^ Nothing }

-- prefix operators
PreType :: { Type }
--	: AppType { $1 }
--	| BinType { $1 }
        : '\\' TypeVar '.' PreType { TypeLambda $2 $4 ::^ Nothing }
        | '&' TypeVar '.' PreType { Forall $2 $4 ::^ Nothing }
        | '\\' TypeVar '.' BinType { TypeLambda $2 $4 ::^ Nothing }
        | '&' TypeVar '.' BinType { Forall $2 $4 ::^ Nothing }
        | '\\' TypeVar '.' AppType { TypeLambda $2 $4 ::^ Nothing }
        | '&' TypeVar '.' AppType { Forall $2 $4 ::^ Nothing }

-- KIND RULES

Kind :: { Kind }
	: '*' { KindProp }
	| Kind '=>' Kind { KindAbs $1 $3 }
	| '(' Kind ')' { $2 }

{
data Token
       = TokenAbs
       | TokenAlpha
       | TokenDot
       | TokenVar String
       | TokenTypVar String
       | TokenForall
       | TokenColon
       | TokenUp
       | TokenDoubleArrow
       | TokenStar
       | TokenOB
       | TokenCB
       | TokenPlus
       | TokenTimes
       | TokenArrow
       | TokenCOB
       | TokenCCB
       | TokenComma
       | TokenROB
       | TokenRCB
       | TokenLR String
       | TokenINLR String
       | TokenEOF
       | TokenFail
  deriving (Show, Eq)

-- a type to locate errors

type LineNumber = (Int, Int)
addLineNumber :: LineNumber->LineNumber->LineNumber
addLineNumber (x1,y1) (x2,y2) = (x1+x2, y1+y2)

-- the monad around the lexer to process errors

data ParseResult a = Ok a | Failed (String, LineNumber)

-- parse error handling

happyError :: P a
happyError = failP "Parse Error"

-- failP adds the line number, so i don't need this 
-- getLineNumber :: P LineNumber
-- getLineNumber = \s l -> Ok l

-- the monadic lexer

type P a = String -> LineNumber -> ParseResult a
-- hand-made Monad P, since using a "real" Monad needs a real type, needs a
-- real constructor, creates really ugly functions with lots of meaningless
-- case constructs to eliminate these constructors

returnP :: a -> P a
returnP a = \s l -> Ok a

failP :: String -> P a
failP err = \ _ (x,y) -> Failed (err++" at line "++show y
                                 ++", column "++show x++".", (x,y))

thenP :: P a -> (a -> P b) -> P b
a `thenP` b = \s l -> case a s l of Ok r -> b r s l
                                    Failed err -> Failed err

monadiclexer :: (Token -> P a) -> P a
monadiclexer cont = 
  \s l -> let (token, rest, pos)=lexer s l
          in if (token==TokenFail) then failP "Lexer error" rest pos
                                   else cont token rest pos

-- the real lexer

lexer :: String -> LineNumber -> (Token, String, LineNumber)
lexer [] (x,y) = (TokenEOF, "", (x,y))
lexer (c:cs) (x,y)
      | isSpace c =
          let (t,s, (xp,yp))=lexer cs (x,y)
           in (t,s, (if c=='\n' then (1,yp+1) else (xp+1,yp)))
      | isAlpha c = 
          let (var, rest)=lexLetter (c:cs)
           in (var, rest, (length (c:cs)-length rest+x,y))
lexer ('\\':cs) (x,y) = (TokenAbs, cs, (x+1,y))
lexer ('/':'\\':cs) (x,y) = (TokenAlpha, cs, (x+2,y))
lexer ('.':cs) (x,y) = (TokenDot, cs, (x+1,y))
lexer (':':cs) (x,y) = (TokenColon, cs, (x+1,y))
lexer ('^':cs) (x,y) = (TokenUp, cs, (x+1,y))

lexer ('=':'>':cs) (x,y) = (TokenDoubleArrow, cs, (x+2,y))
lexer ('*':cs) (x,y) = (TokenStar, cs, (x+1,y))
lexer ('&':cs) (x,y) = (TokenForall, cs, (x+1,y))
lexer ('(':cs) (x,y) = (TokenOB, cs, (x+1,y))
lexer (')':cs) (x,y) = (TokenCB, cs, (x+1,y))

lexer ('+':cs) (x,y) = (TokenPlus, cs, (x+1,y))
lexer ('%':cs) (x,y) = (TokenTimes, cs, (x+1,y))
lexer ('-':'>':cs) (x,y) = (TokenArrow, cs, (x+2,y))
lexer ('{':cs) (x,y) = (TokenCOB, cs, (x+1,y))
lexer ('}':cs) (x,y) = (TokenCCB, cs, (x+1,y))
lexer (',':cs) (x,y) = (TokenComma, cs, (x+1,y))
lexer ('<':cs) (x,y) = (TokenROB, cs, (x+1,y))
lexer ('>':cs) (x,y) = (TokenRCB, cs, (x+1,y))


-- no rule applies
lexer s c = (TokenFail, s, c)

lexLetter cs =
  let (var, rest) = span isAlphaNum cs
      token = case var of
        "L" -> TokenLR "L"
        "R" -> TokenLR "R"
        "INL" -> TokenINLR "L"
        "INR" -> TokenINLR "R"

        v:_ | isUpper v -> TokenTypVar var
        v:_ | isLower v -> TokenVar var
  in (token, rest)

-- general functions

parserMonadic :: String -> ParseResult Exp
parserMonadic = \s -> parser s (1,1)

parserShortError :: String -> Exp
parserShortError s = case parser s (1,1) of Ok r -> r
                                            Failed (s,l) -> error s

marklocation s (x,y) =
  let ls=lines s
  in unlines (take y ls++[replicate (x-1) ' '++"^"]++drop y ls)

parserLongError :: String -> Exp
parserLongError s =
  case parser s (1,1) of
    Ok r -> r
    Failed (e,p) -> error (e++"\n"++marklocation s p)
parseCPFw = parserLongError
parse = parserLongError

}

1.3  Pretty-Printer

-- funtions to pretty print lambda terms with types as LaTeX source
-- $Id: PrintExplicit.hs,v 1.5 2002/05/01 18:29:36 markus Exp $

module PrintExplicit where
import ParseTypedLambdaExpressions(Exp(..), Type(..), Kind(..),
                                   UntypedExp(..), UnkindedType(..))

attribute separator string Nothing = string
attribute separator string (Just t) = "("++string++separator++show t++")"

class Explicit a where
  explicit :: a -> String

instance Explicit Exp where
  explicit (Abs v t ::: ty) =
    attribute ":" ("(\\"++explicit v++"."++explicit t++")") ty
  explicit (App t1 t2 ::: ty) =
    attribute ":" ("("++explicit t1++" "++explicit t2++")") ty
  explicit (Var v ::: ty) =
    attribute ":" v ty 

instance Explicit Kind where
  explicit KindProp = "*"
  explicit (KindAbs k1 k2) = "("++explicit k1++"=>"++explicit k2++")"

instance Explicit Type where
  explicit (TypeAbs t1 t2 ::^ k) =
    attribute "^" ("("++explicit t1++"->"++explicit t2++")") k
  explicit (TypeApp t1 t2 ::^ k) =
    attribute "^"  ("("++explicit t1++" "++explicit t2++")") k
  explicit (Forall (TypeVar tv ::^ ktv) t ::^ k) =
    attribute "^" ("(&"++explicit (TypeVar tv ::^ ktv)++"."++explicit t++")") k
  explicit (TypeVar tv ::^ k) =
    attribute "^" tv k

-- funtions to pretty print lambda terms with types as LaTeX source
-- $Id: PrintLaTeX.hs,v 1.8 2002/05/08 02:32:09 markus Exp $

module PrintLaTeX where
import CPFwDatatypes(Exp(..), Type(..), UntypedExp(..), UnkindedType(..),
                     Kind(..),
                     Binary (..),
                     Prec(..), precProb, precProbT, OpStyle(..),
                     cs)

import Char(isAlphaNum)

latexVar v =
  let s=fst $ span isAlphaNum v in if s==v then s else s++"..."
--  let cs=drop 1 (show v) in "\\textrm{ "++take (length cs-1) cs++" }"

class LaTeX a where
  latex :: a -> String
  latex = latex_ True
  latex_ :: Bool -> a -> String

instance LaTeX UntypedExp where
  -- dot structures (prefix), lowest prec so no testing neccesary
  latex_ b (Abs v t) =
    let p = precProb [Pre] (Abs v t) t in
    cs (not b) "("++"\\lambda "++latex_ False v++"."++
    cs p "("++latex_ True t++cs p ")"++cs (not b) ")"
  latex_ b (Gen v t) =
    let p = precProb [Pre] (Gen v t) t in
    cs (not b) "("++"\\Lambda "++latex_ False v++"."++
    cs p "("++latex_ True t++cs p ")"++cs (not b) ")"

  -- prefix
  latex_ _ (InLR c e) | precProb [Pre] (InLR c e) e =
    "IN"++show c++" ("++latex_ True e++")"
  latex_ b (InLR c e) = "IN"++show c++" "++latex_ b e

  -- apps
  latex_ b (App t1 t2) =
    let lp = precProb [Post, LeftAss] (App t1 t2) t1
        rp = precProb [Pre] (App t1 t2) t2 in
    cs lp "("++latex_ lp t1++cs lp ")"++" "++
    cs rp "("++latex_ (rp||b) t2++cs rp ")"
  latex_ b (Inst t (ty ::^ k)) =
    let lp = precProb [Post, LeftAss] (Inst t (ty ::^ k)) t
        rp = case prec ty of (_, Base) -> False
                             _ -> True in
    cs lp "("++latex_ (lp||b) t++cs lp ")"++" "++
    cs rp "("++latex_ (rp||b) (ty ::^ k)++cs rp ")"

  -- postfix
  latex_ _ (Case inlr vl tl vr tr) =
    let p = precProb [Post, LeftAss] (Case inlr vl tl vr tr) inlr in
    cs p "("++ latex_ p inlr++cs p ")"++
    "( "++show vl++" . "++latex_ True tl++" , "++
    show vr++" . "++latex_ True tr++" )"
{- latex is unable to typeset bracketed expressions reasonable
    cs p "("++ latex_ p inlr++cs p ")"++
    "\\left( "++show vl++". \\right. "++latex_ True tl++", "++
    show vr++" . \\left. "++latex_ True tr++" \\right)"
-}
  latex_ b (Lr c e) =
    let p = precProb [Post, LeftAss] (Lr c e) e in
    cs p "("++latex_ (b||p) e++cs p ")"++" "++show c

  -- simple cases
  latex_ _ (Var v) = latexVar v
  latex_ _ (Pair t1 t2) = " < "++latex_ True t1++", "++
                          latex_ True t2++" > "
{- latex is unable to typeset bracketed expressions reasonable
  latex_ _ (Pair t1 t2) = " \\left< "++latex_ True t1++", \\right. \\left. "++
                          latex_ True t2++" \\right> "
-}

  -- ERROR
  latex_ _ _ = "UntypedExp latex_: no rule applies."

instance LaTeX Exp where
  latex_ b (e ::: Nothing) = latex_ b e
  latex_ b (e ::: Just t) = latex_ b e++":"++latex_ b t

instance LaTeX Kind where
  latex_ _ KindProp = "*"
  latex_ _ (KindAbs (KindAbs k11 k12) k2) = 
    "("++latex (KindAbs k11 k12)++") \\Rightarrow "++latex k2
  latex_ _ (KindAbs k1 k2) = latex k1++" \\Rightarrow "++latex k2

instance LaTeX Binary where
  latex_ _ Sum = " + "
  latex_ _ Prod = " \\times "
  latex_ _ Function = " \\rightarrow "

instance LaTeX UnkindedType where
  latex_ _ (TypeVar tv) = latexVar tv

  -- brackets if necessary
  latex_ b (TypeLambda tv t) =
    cs (not b) "("++" \\lambda "++latex_ False tv++"."++latex_ True t++cs (not b) ")"
  latex_ b (Forall tv t) =
    cs (not b) "("++" \\forall "++latex_ False tv++"."++latex_ True t++cs (not b) ")"

  -- binary infix operators + % ->
  latex_ b (TypeBinary op t1 t2) =
    let lp = precProbT [Post, LeftAss] (TypeBinary op t1 t2) t1
        rp = precProbT [Pre, RightAss] (TypeBinary op t1 t2) t2 in
    cs lp "("++latex_ lp t1++cs lp ")"++latex op++
    cs rp "("++latex_ (rp||b) t2++cs rp ")"

  -- apps
  latex_ b (TypeApp t1 t2) =
    let lp = precProbT [Post, LeftAss] (TypeApp t1 t2) t1
        rp = precProbT [Pre, RightAss] (TypeApp t1 t2) t2 in
    cs lp "("++latex_ lp t1++cs lp ")"++" "++
    cs rp "("++latex_ (rp||b) t2++cs rp ")"

  -- base types
  latex_ _ (TypeVar tv) = latexVar tv

  -- ERROR
  latex_ _ _ = error "UnkindedType latex_: no rule applies."

instance LaTeX Type where
  latex_ b (t ::^ Nothing) = latex_ b t
  latex_ b (TypeVar v ::^ Just k) = latex_ b (TypeVar v)++"^{"++latex k++"}"
  latex_ b (t ::^ Just k) = "("++latex_ True t++")^{"++latex k++"}"

1.4  Die Verarbeitung der Bäume

-- Implementing funtions for lambda terms with types
-- $Id: ProcessCPFw.hs,v 1.18 2002/05/07 20:09:44 markus Exp $

module ProcessCPFw where
import CPFwDatatypes(Exp(..), Type(..), UntypedExp(..), UnkindedType(..),
                     Kind(..), Binary(..), LR(..), ty, jty, con, kd, jkd)

import List(union, unionBy, intersect, (\\), elemIndex, delete, nubBy, nub,
            find)
import Maybe(mapMaybe, fromJust, isNothing, isJust, maybeToList,
             catMaybes, fromMaybe)
import Char(isDigit)
import Monad(liftM2, mplus)

-- class Lambda with methods to ease the implementation of methods from the
-- lambda calculus theory

class Eq a=>Lambda a where
  -- a more uniform representation of trees with bound variables:
  -- a list of pairs of a bound variable (or Nothing if nothing is bound) and
  -- the term it is abstracted out
  destr :: a->[(Maybe a, a)]
  constr :: a->[(Maybe a, a)]->a
  errorvar :: String -> a
  sameType :: a->a->Bool
  rmType :: a->a
  freshenVar :: a->a
  isLambda :: a->Bool
  isApp :: a->Bool
  redEx :: a->Maybe a

  match :: [a] -> a -> a -> a
  annotateType :: [a] -> a -> a
  annotateInner :: [a] -> a -> a

-- comparing two types using alpha equality
infix 4 ==+
(==+) :: (Lambda a)=>a->a->Bool

a ==+ b = let l=alphaUnify (destr a) (destr b) 
              join (b1, l1) (b2, l2) = (b1&&b2, l1++l2)
              alphaUnify :: (Lambda a)=>[(Maybe a, a)] -> [(Maybe a, a)] -> (Bool, [(Maybe a, a)])
              alphaUnify [] [] = (True, [])
              alphaUnify ((Nothing, tl):rl) ((Nothing, tr):rr) =
                 join (tl ==+ tr, [(Nothing, tl)]) (alphaUnify rl rr)
              alphaUnify ((vl, tl):rl) ((vr, tr):rr) =
                 join (tl ==+ snd (alpha (vr, tr) (fromJust vl)), [(vl, tl)]) (alphaUnify rl rr)
              alphaUnify _ _ = (False, [])
          in fst l && constr a (snd l) == constr b (snd l)

instance Lambda Exp where

  destr (Var v ::: ty) =
    []
  destr (Abs (Var v ::: ty) tm ::: t) =
    [(Just (Var v ::: ty), tm)]
  destr (Inst e ty ::: t) =
    [(Nothing, e)]
  destr (Gen v e ::: t) =
    [(Nothing, e)]
  destr (App e1 e2 ::: t) =
    [(Nothing, e1), (Nothing, e2)]
  destr (Case e (Var v1 ::: ty1) t1 (Var v2 ::: ty2) t2 ::: t) =
    [(Nothing, e), (Just (Var v1 ::: ty1), t1), (Just (Var v2 ::: ty2), t2)]
  destr (InLR lr e ::: t) =
    [(Nothing, e)]
  destr (Pair e1 e2 ::: t) =
    [(Nothing, e1), (Nothing, e2)]
  destr (Lr lr e ::: t) =
    [(Nothing, e)]
  destr a = error ("destr: no rule applies to "++show a++".")

  constr (Var v ::: ty) [] = 
    (Var v ::: ty)
  constr (Abs _ _ ::: t) [(Just (Var v ::: ty), tm)] = 
    Abs (Var v ::: ty) tm ::: t
  constr (Inst _ ty ::: t) [(Nothing, e)]  = 
    Inst e ty ::: t
  constr (Gen v _ ::: t) [(Nothing, e)]  = 
    Gen v e ::: t
  constr (App _ _ ::: t) [(Nothing, e1), (Nothing, e2)]  = 
    App e1 e2 ::: t
  constr (Case _ _ _ _ _ ::: t)
         [(Nothing, e), (Just (Var v1 ::: ty1), t1), (Just (Var v2 ::: ty2), t2)]  = 
    Case e (Var v1 ::: ty1) t1 (Var v2 ::: ty2) t2 ::: t
  constr (InLR lr _ ::: t) [(Nothing, e)]  = 
    InLR lr e ::: t
  constr (Pair _ _ ::: t) [(Nothing, e1), (Nothing, e2)]  = 
    Pair e1 e2 ::: t
  constr (Lr lr _ ::: t) [(Nothing, e)]  = 
    Lr lr e ::: t
  constr a b = errorvar ("constr: no rule applies to wrap "++show a++" around "++
                         show b++".")

  errorvar s = Var s ::: Nothing

  freshenVar (Var v ::: typ) =
    let (n,r)=span isDigit (reverse v)
    in Var (reverse r++show (read ("0"++(reverse n)) + 1)) ::: typ 

  sameType e1 e2 = ty e1 == ty e2

  rmType (tm ::: _) = tm ::: Nothing

  isLambda (Abs _ _ ::: _) = True
  isLambda _ = False

  isApp (App _ _ ::: _) = True
  isApp _ = False

  redEx (App (Abs v t ::: atyp) t2 ::: typ) =
    Just (subst [(v, t2)] t)
  redEx (Case (InLR lr r ::: intyp) vl tl vr tr ::: typ) =
    let lrf=if lr==L then fst else snd
    in Just (subst [(lrf (vl,vr), r)] (lrf (tl, tr)))
  redEx (Lr lr (Pair t1 t2 ::: ptyp) ::: typ) =
    Just (if lr==L then t1 else t2)
  redEx _ = Nothing

  match env (e1 ::: Nothing) (e2 ::: t2) =
    (e2 ::: fmap (annotateFull_ (freetv env)) t2)
  match env (e1 ::: t1) (e2 ::: t2) | matchingT (betaReduction $ fromJust t1)
                                            (betaReduction $ fromJust t2) =
    (e2 ::: fmap (annotateFull_ (freetv env).betaReduction) t2)
  match _ (e1 ::: t1) (e2 ::: t2) =
    errorvar ("Can not match "++show (e1 ::: fmap betaReduction t1)++
              " with "++show (e2 ::: fmap betaReduction t2)++".")
  
  annotateInner env (Inst e t ::: typ) =
    case jty e of
      Forall v r ::^ Just KindProp ->
        match env (Inst e t ::: typ)
              (Inst e t ::: Just (subst [(v,t)] r))
      _ -> errorvar ("Can not INST a type "++show t++" without a & "++
                     "at the front of "++show (jty e)++".") 
  annotateInner env (Abs v e ::: typ) =
    match env (Abs v e ::: typ)
          (Abs v e ::: Just (TypeBinary Function
                                        (typeToProp (jty v))
                                        (typeToProp (jty e))
                               ::^ Just KindProp))
  annotateInner env (Gen t e ::: typ) =
    case ty e of
      Nothing -> errorvar ("Untyped term in Lambda (/\\): "++show e++".")
      Just tye -> match env (Gen t e ::: typ)
                            (Gen t e ::: Just (Forall t (typeToProp tye)
                                                 ::^ Just KindProp))  
  annotateInner env (App e1 e2 ::: typ) =
    case jty e1 of
      TypeBinary Function v t ::^ k ->
        if v==jty e2 then match env (App e1 e2 ::: typ)
                                (App e1 e2 ::: Just t)
                     else errorvar ("Cannot apply "++show e1++" $ "++show e2++
                                    ". Type mismatch.")
      _ -> errorvar ("Cannot apply "++show e1++" $ "++show e2++". No APP type.")
  annotateInner env (Lr lr e ::: typ) = 
    case jty e of
      TypeBinary Prod tl tr ::^ Just KindProp ->
        match env (Lr lr e ::: typ)
              (Lr lr e ::: Just (case lr of L -> tl; R -> tr)) 
      t -> errorvar ("Can not LR a type "++show t++" which is not a product.") 
  annotateInner env (Pair e1 e2 ::: typ) =
    match env (Pair e1 e2 ::: typ)
          (Pair e1 e2 ::: Just (TypeBinary Prod (jty e1)
                                                (jty e2)
                                  ::^ Just KindProp))
  annotateInner env (Case ei v1 e1 v2 e2 ::: typ) =
    case jty ei of
      TypeBinary Sum tl tr ::^ k ->
        if k /= Just KindProp then errorvar "Case disjunction not of type *." else
        if tl /= jty v1 then errorvar "Case type mismatch in left argument." else
        if tr /= jty v2 then errorvar "Case type mismatch in right argument." else
        if ty e1 /= ty e2 then errorvar "Case type mismatch in fuction arguments." else
          match env (Case ei v1 e1 v2 e2 ::: typ) (Case ei v1 e1 v2 e2 ::: ty e1)
      t -> errorvar ("Can not Case an expression with a type "++show t++
                     " which is not a sum.")
  annotateInner env (InLR lr e ::: typ) = 
    case typ of
      Nothing -> errorvar ("Can not type a InLR "++show (InLR lr e ::: typ)++
                           " without annotation.")
      Just (TypeBinary Sum lt rt ::^ k) ->
        match env (InLR lr e ::: typ)
              (InLR lr e ::: Just (case lr of L -> TypeBinary Sum (jty e) rt
                                              R -> TypeBinary Sum lt (jty e)
                                     ::^ toProp k))
      Just t -> errorvar ("Type "++show t++"doesn't match InLR "++
                          show (InLR lr e ::: typ)++".")

  annotateInner env e = errorvar("annotateInner: Can not annotate "++
                                 show e++" under env "++show env++".")

  annotateType env (e ::: Just t) =
    e ::: Just (annotateFull_ (freetv env) t) -- annotate variable binders
  annotateType env te =
    errorvar ("annotateType(Exp): cannot annotate empty type in: "++
              show te++".")

instance Lambda Type where

  destr (TypeVar v ::^ ty) =
    []
  destr (TypeLambda (TypeVar v ::^ ty) tm ::^ t) =
    [(Just (TypeVar v ::^ ty), tm)]
  destr (Forall (TypeVar v ::^ ty) tm ::^ t) =
    [(Just (TypeVar v ::^ ty), tm)]
  destr (TypeApp e1 e2 ::^ t) =
    [(Nothing, e1), (Nothing, e2)]
  destr (TypeBinary _ e1 e2 ::^ t) =
    [(Nothing, e1), (Nothing, e2)]
  destr a = error ("destr: no rule applies to "++show a++".")

  constr (TypeVar v ::^ ty) [] = 
    TypeVar v ::^ ty
  constr (TypeLambda _ _ ::^ t) [(Just (TypeVar v ::^ ty), tm)] = 
    TypeLambda (TypeVar v ::^ ty) tm ::^ t
  constr (Forall _ _ ::^ t) [(Just (TypeVar v ::^ ty), tm)] = 
    Forall (TypeVar v ::^ ty) tm ::^ t
  constr (TypeApp _ _ ::^ t) [(Nothing, e1), (Nothing, e2)]  = 
    TypeApp e1 e2 ::^ t
  constr (TypeBinary k _ _ ::^ t) [(Nothing, e1), (Nothing, e2)]  = 
    TypeBinary k e1 e2 ::^ t
  constr a b = errorvar ("constr: no rule applies to wrap "++show a++" around "++
                         show b++".")

  errorvar s = TypeVar s ::^ Nothing

  freshenVar (TypeVar v ::^ k) =
    let (n,r)=span isDigit (reverse v)
    in TypeVar (reverse r++show (read ("0"++(reverse n)) + 1)) ::^ k 

  sameType e1 e2 = kd e1 == kd e2

  rmType (tm ::^ _) = tm ::^ Nothing

  isLambda (TypeLambda _ _ ::^ _) = True
  isLambda _ = False

  isApp (TypeApp _ _ ::^ _) = True
  isApp _ = False

  redEx (TypeApp (TypeLambda v t ::^ ak) t2 ::^ tk) =
    Just (subst [(v, t2)] t)
  redEx _ = Nothing

  match _ (e1 ::^ Nothing) (e2 ::^ Nothing) =
    errorvar ("Can not match "++show e1++" with "++show e2++
              " having both no kinds.")
  match _ (e1 ::^ Nothing) (e2 ::^ t2) = (e2 ::^ t2)
  match _ (e1 ::^ t1) (e2 ::^ t2) | t1 == t2 = (e2 ::^ t2)
  match _ e1 e2 =
    errorvar ("Can not match "++show e1++" with "++show e2++".")
 
  annotateInner env (TypeBinary q lt rt ::^ k) =
    match env (TypeBinary q lt rt ::^ k)
          (TypeBinary q (typeToProp lt) (typeToProp rt) ::^ toProp k)
  annotateInner env (Forall v t ::^ k) =
    match env (Forall v t ::^ k)
          (Forall v (typeToProp t) ::^ toProp k)
  annotateInner env (TypeLambda v t ::^ k) =
    match env (TypeLambda v t ::^ k)
          (TypeLambda v t ::^ Just (KindAbs (jkd v) (jkd t)))
  annotateInner env (TypeApp t1 t2 ::^ k) =
    case jkd t1 of
      KindAbs k1 k2 | k1 == jkd t2 -> 
        match env (TypeApp t1 t2 ::^ k)
              (TypeApp t1 t2 ::^ Just k2)
      kw -> errorvar ("Kind mismatch TypeApp: "++show kw++" $ "++
                      show (jkd t2)++".")

  annotateInner env t = errorvar ("annotateInner: no rule applies. "++show t++".")

  annotateType tenv t = annotateFull_ [] t -- used for variable binders

matchingT (e1 ::^ Nothing) (e2 ::^ t2) = True
matchingT (e1 ::^ t1) (e2 ::^ t2) =
  t1 == t2 {- && all (\(a,b)->matchingT a b)  (zip  ((map snd (destr e1)))
                                                 (map snd (destr e2))) -}

freetv [] = []
freetv (e:es) = freevar (jty e)++freetv es

isVar :: Lambda a => a->Bool
isVar = null . destr

isBinder t = (do (b,_)<-destr t; maybeToList b) /= []

var :: Lambda a=>a->[a]
var e =
  if isVar e then [e]
             else nubBy sameName (do (b,t)<-destr e 
                                     unionBy sameName (maybeToList b) (var t))

freevar :: Lambda a=>a->[a]
freevar e =
  if isVar e then [e]
             else nubBy sameName
                        (do (b,t)<-destr e
                            (filter (\v->Just (rmType v) /= fmap rmType b)
                                    (freevar t)))

boundvar :: Lambda a=>a->[a]
boundvar e = nubBy sameName  (do (b,t)<-destr e 
                                 unionBy sameName (maybeToList b) (boundvar t))

-- subterms

directSubterms :: Lambda a=>a->[a]
directSubterms exp = map snd $ destr exp

subterms :: Lambda a=>a->[a]
subterms exp = subterms_ [exp] where 
                 subterms_ [] =[]
                 subterms_ (t:ts) = t:subterms_ (directSubterms t++ts)

-- no capture avoidance
capsubst :: Lambda a=>[(a, a)]->a->a
capsubst s e | isVar e = case e `lookup` s of Nothing -> e
                                              Just v -> v
capsubst s e = constr e (do (b,t)<-destr e 
                            let n=case b of Just v -> (filter ((v==).fst) s)
                                            Nothing -> s
                            [(b, capsubst s t)])

-- change names of bound variables
alpha :: Lambda a => (Maybe a, a) -> a -> (Maybe a, a)
alpha (Just vold, t) vnew 
  | not (sameType vold vnew) = error ("alpha subsitutes only "++
                                      "variables of the same type.")
  | not (isVar vnew) = error ("alpha needs a new variable as "++
                              "second argument.")
  | vnew `elem` freevar t\\[vold] = error "alpha name clash."
  | True = (Just vnew, capsubst [(vold, vnew)] t)
alpha _ _ = error ("alpha: needs a Just binder pair as "++
                   "first and a new variable as second argument.")

subst :: Lambda a => [(a, a)] -> a -> a -- [(variable, term to insert)], target ->result
                                        -- parallel substitution of variables

subst s t | isVar t = fromMaybe t (t `lookup` s)
subst s t =
  constr t (do (mv, tm)<-destr t
               case mv of Nothing -> [(Nothing, subst s tm)]
                          Just v -> if (freevar t `intersect` map fst s) /= []
                                       -- no substitution, no capture
                                       && (v `elem` (do (sv,st)<-s; sv:freevar st))
                                       -- capture danger
                                    then -- rename
                                      let fv=freshenVar v
                                          asub=alpha (mv, tm) fv
                                      in destr (subst s (constr t [asub]))
                                    else [(mv, subst s tm)]

           )

-- betaReduce :: Lambda a => a -> Maybe a

betaReduce t | isApp t && (isLambda (snd (destr t !! 0))) = 
  let arg=snd (destr t !! 1)
      [(Just var, fct)]=destr (snd (destr t !! 0))
  in (Just (subst [(var, arg)] fct))

-- betaReduce t = error ("BLOCK error: "++show t)

betaReduce t | isVar t = Nothing

betaReduce t =  fmap (constr t) (leftmost (destr t)) where
--  leftmost :: Lambda a => [(Maybe a, a)]->Maybe [(Maybe a, a)]
  leftmost [] = Nothing 
  leftmost (p:ps) = case betaReduce (snd p) of
    Nothing -> fmap (p:) (leftmost ps)
    Just nt -> Just ((fst p, nt):ps)


-- reduce using all reduction rules avaliable in the calculus of "Lambda"
-- this is governed by the redEx Lambda class method

fullReduce :: Lambda a => a -> Maybe a
fullReduce t | isJust (redEx t) = redEx t
fullReduce t = fmap (constr t) (leftmost (destr t)) where
  leftmost [] = Nothing 
  leftmost (p:ps) =
    case fullReduce (snd p) of
      Nothing -> fmap (p:) (leftmost ps)
      Just nt -> Just ((fst p, nt):ps)

-- reduce until no reduction applies or term stops changing
reduction :: Lambda a => (a->Maybe a)->a->a 
reduction r t =
  case r t of Nothing -> t 
              Just nt -> if t==nt then t
                                  else reduction r nt 

betaReduction :: Lambda a => a -> a
betaReduction = reduction betaReduce

fullReduction :: Lambda a => a -> a
fullReduction = reduction fullReduce

-- a history of recorded reductions

historyReduction r t =
  case r t of Nothing -> [] 
              Just nt -> if t==nt then []
                                  else nt:historyReduction r nt 

historyBetaReduction t = t:historyReduction betaReduce t

historyFullReduction t = t:historyReduction fullReduce t

-- helper

noType t = sameType t (rmType t)
sameName v1 v2 = rmType v1 == rmType v2
addVar v l = if noType v then [errorvar ("Cannot add untyped variable "++show v++
                                         " to "++show l++".")]
                         else nubBy sameName (v:l)

freetypevarInEnv env =
  nub (do _ ::: t<-env
          case t of 
            Nothing -> [errorvar ("freetypevarInEnv: "++
                                  show env++" contains untyped elements.")]
            Just typ -> let fv=freevar (con typ ::^ toProp (kd typ)) in
                        if any noType fv
                          then [errorvar ("freetypevarInEnv: "++show env++
                                          " contains unkinded type variables.")]
                          else fv
      )

toProp Nothing = Just KindProp
toProp (Just KindProp) = Just KindProp
toProp k = error ("toProp: Can not convert kind "++show k++" to kind Prop.")

rmProp Nothing = Nothing
rmProp (Just KindProp) = Nothing
rmProp k = error ("rmProp: Kind "++show k++" is no Prop.")

typeToProp (t ::^ k) = t ::^ toProp k

-- strips

strip t | isVar t = rmType t
strip t = rmType ((constr t) (do (v,st)<-destr t
                                 [(fmap rmType v, strip st)]))

stripChurch t = stripChurch_ [] t

stripChurch_ env t | isVar t =
  if t `elem` env then rmType t
                  else t -- stripType t
stripChurch_ env t = 
    rmType ((constr t)
      (do (v, st)<-destr t  
          case v of
            Just var -> [(Just (stripChurch_ [] var),
                         stripChurch_ (addVar var env) st)]
            Nothing -> [(v, stripChurch_ env st)])
    )

-- annotate

-- annotateFull annotates all inner nodes on a tree with annotated leafes
-- using a bottom up algorithm
annotateFull :: (Lambda a, Show a) => a -> a
annotateFull t = annotateFull_ (freevar t) t

annotateFull_ :: (Lambda a, Show a) => [a] -> a -> a
annotateFull_ env t | any noType env =
  errorvar ("annotateFull_: all variables in environment "++
            show env++" have to be typed. Problem:"++
            show (filter noType env)++".")
annotateFull_ env t | isVar t && noType t =
  case t `lookup` (zip (map rmType env) env) of
    Nothing -> errorvar ("annotateFull_: (here) free variable "++show t++
                         " not found in environment: "++show env++".")
    Just v -> v
annotateFull_ env t | isVar t =
  case find (sameName t) env of
    Nothing -> if rmType t == t
                 then errorvar ("annotateFull_: free variables must"++
                                "be annotated. Env: "++show env++
                                " Var: "++show t++".")
                 else t
    Just envvar -> if rmType t == t || envvar == t
                     then envvar
                     else errorvar ("annotateFull_: inner variable "++
                                    "not correctly annotated. EnvVar: "++
                                    show envvar++" Var: "++show t++".")

annotateFull_ env t =
  annotateInner env (constr t
    (do (v,st)<-destr t
        case v of
          Nothing -> [(v, annotateFull_ env st)]
          Just var -> if (noType var)
                         then [(Nothing,
                                errorvar ("annotateFull_: need annotated "++
                                          "abstracted variables. Problem"++show v++
                                          " in "++show t++"."))]
                         else let varan = annotateType env var in
                              [(Just varan,
                                annotateFull_ (addVar varan env) st)]
    ))

annotateChurch :: (Lambda a, Show a)=>a -> a
annotateChurch = stripChurch . annotateFull

-- general type checking function

createType :: Exp -> [Type] -> Type
createType (Abs v _ ::: _) [t] =
  TypeBinary Function (jty v) t ::^ Just KindProp
createType (Inst _ t ::: _) [Forall v r ::^ Just KindProp] =
  betaReduction $ subst [(v,t)] r
createType (Gen v e ::: _) [t] =
  if v `elem` (freetv (freevar e))
    then errorvar ("\nERROR: Illegal Generalisation. TVar:"++
                   show v++" free in "++show e++".\n"++
                   "freevar e: "++show (freevar e)++"\n"++
                   "freetv (freevar e): "++show(freetv (freevar e))++"\n---\n")
    else Forall v t ::^ Just KindProp
createType (App _ _ ::: _) [TypeBinary Function t1 t2  ::^ Just KindProp, t3] =
  t2 -- t1 == t3 not checked
createType (Var _ ::: t) [] =
  fromJust t
createType (Case c vl el vr er ::: t) [tc,tel,ter] =
  ter -- not checked:
      -- con (jty c) == TypeBinary Sum (jty vl) (jty vr) &&
      -- jty el == jty er
createType (InLR lr _ ::: Just (TypeBinary Sum tl tr  ::^ Just KindProp)) [te] =
  case lr of L-> TypeBinary Sum te tr  ::^ Just KindProp
             R-> TypeBinary Sum tl te  ::^ Just KindProp
createType (Pair e1 e2 ::: t) [t1,t2] =
  TypeBinary Prod t1 t2 ::^ Just KindProp
createType (Lr lr _ ::: t) [TypeBinary Prod tl tr ::^ Just KindProp] =
  case lr of L->tl; R->tr
createType e ts = errorvar ("ERROR: Can not create type. No rule applies for "++
                            show (e, ts)) -- ERROR

checkType exp = map checkType_ (subterms exp)

checkType_ e = matchType e (jty e) ((createType e) (map jty (directSubterms e)))

matchType e t1 t2 = (e, t1, t2, t1 ==+ t2)

-- check whether a Church term is completely and correctly annotated

checkChurch :: Exp -> Maybe String -- Nothing means OK, Just Error

checkChurch (Abs e1 e2 ::: t) =
  checkChurch e1 `mplus` checkChurch e2 `mplus`   
    if (TypeBinary Function (jty e1) (jty e2) == con (fromJust t))
      then Just ("Abs mismatch:"++show (jty e1)++"->"++
                 show(jty e2)++"!="++show (con (fromJust t))++".")
      else Nothing
checkChurch (Inst e t ::: ot) =
  checkChurch e  `mplus` 
    case jty e of
    Forall v r ::^ Just KindProp ->
      if Just (betaReduction $ subst [(v,t)] r) == ot
        then Nothing
        else Just "INST type mismatch"
    n ->
      Just ("Can't INST a type "++show n++
            "which is not a Forall.")
checkChurch (Gen v e ::: t) = 
  checkChurch e `mplus`
  if con (fromJust t) == Forall v (jty e)
    then Nothing
    else Just "Gen fail."
checkChurch (App e1 e2 ::: t) =
  checkChurch e1 `mplus` checkChurch e2 `mplus`
  if (TypeBinary Function (jty e2) (fromJust t) == con (jty e1))
    then Nothing
    else Just "App fail."
checkChurch (Var s ::: t) = Nothing -- use an environment?
checkChurch (Case c vl el vr er ::: t) = 
  checkChurch c `mplus` checkChurch vl `mplus` checkChurch el
  `mplus`  checkChurch vr `mplus`  checkChurch er `mplus` 
  if con (jty c) == TypeBinary Sum (jty vl) (jty vr) &&
     jty el == jty er && jty er == fromJust t
  then Nothing
  else Just "Case fail."
checkChurch (InLR lr e ::: t) =
  checkChurch e `mplus`  
  case con (fromJust t) of
    TypeBinary Sum tl tr ->
      if (case lr of L->tl; R->tr) == jty e
        then Nothing
        else Just "InLR fail."
    n -> Just ("Type of InLR has to be a Sum.")
checkChurch (Pair e1 e2 ::: t) =
  checkChurch e1 `mplus` checkChurch e2 `mplus`  
  if TypeBinary Prod (jty e1) (jty e2) == con (fromJust t) 
    then Nothing
    else Just "Pair fail."
checkChurch (Lr lr e ::: t) =
  checkChurch e `mplus` 
  case con (jty e) of
    TypeBinary Prod tl tr ->
      if (case lr of L->tl; R->tr) == fromJust t
        then Nothing
        else Just "LR fail."
    n -> Just ("LR application needs a Prod type:"++show n++".")

1.5  Die Beispiele

-- Examples to test the type checker
-- $Id: Examples.hs,v 1.21 2002/05/07 21:26:29 markus Exp $

module Examples where

import CPFwDatatypes(Exp(..), Type(..), UntypedExp(..), UnkindedType(..),
                     Kind(..))
import ParseCPFw(parse)

import ProcessCPFw 

--import PrintExplicit(Explicit(..))
import PrintLaTeX(LaTeX(..))

import Maybe(fromMaybe)

-- adapted show for lists

brshow :: Show a => [a] -> String
brshow [] = "[]"
brshow (e:es) = "["++foldl (\s e->s++",\n "++show e) (show e) es++"\n]"

-- combinators s,k,i from combinator logic
s = parse("\\x.\\y.\\z.(x z)(y z)")
k = parse("\\x.\\y.x")
i = parse("\\x.x")

skk = (((s `App` k) ::: Nothing) 
           `App` k) ::: Nothing

-- Church numerals
church :: Int->Exp
church n = parse("\\f.\\x."++church_ n)
church_ :: Int->String
church_ 0 = "x"
church_ n = "f("++church_ (n-1)++")"

tchurch n = parse("(\\f:(A^*->A^*)^*.\\x:A^*."++tchurch_ n
                        ++"):((A^*->A^*)^*->(A^*->A^*)^*)^*")
tchurch_ :: Int->String
tchurch_ 0 = "(x:A^*)"
tchurch_ n = "((f:(A^*->A^*)^*)"++tchurch_ (n-1)++":A^*)"

-- Urzyczyn's 2-chains
urzy n = ((urzy_ n) `App` k) ::: Nothing
urzy_ 0 = church 2
urzy_ n = ((urzy_ (n-1)) `App` (church 2)) ::: Nothing

-- Urzyczyn's 22K p. 338

typedtwotwok="("++show (church 2)++")("++show (church 2)++
  ":&B.(&A.A->(B A))->(&A.A->(B(B A)))"++")("++show k++")"

tyttk = parse typedtwotwok

typedtwotwotwok= "("++show (church 2)++")("++show (church 2)++
  ":&C.(&B.(&A.A->B A)->(&A.A->C B A))->"++
  "(&B.(&A.A->(B A))->(&A.A->(C (C B) A)))"++
  ")("++show (church 2)++")("++show k++")"

tytttk = parse typedtwotwotwok

churchttk = "(\\f:&B^*=>*.(&A^*.A^*->B A^*)->&A^*.A^*->B (B A^*)."++
            "\\x:&A^*.A^*->B^*=>* A^*.((f B^*=>*) x))" {- ++
            "(\\f:A^*->B^*=>* A^*.\\x:A^*.f (f x)"++
            ":&B^*=>*.(&A^*.A^*->B A^*)->&A^*.A^*->B (B A^*)) \\x.\\y.x" -}

typed22k = parse churchttk

-- test my betareduction "be id!"
beid = betaReduction skk

-- type tests

typeds = parse ("(\\x:X^*.(\\y:Y^*.(\\z:Z^*."
                     ++"((x:X^*) (z:Z^*))"
                     ++"(y z))))"
                     ++":((X^*->Y^*)^*->Z^*)^*")
typedk = parse "(\\x:X^*.\\y:Y^*.x):(X->Y->X)^*"
typedi = parse "\\x:X^*.(x:X^*):(X^*->X^*)^*"
typedx = parse "x:X^*"

-- crap

-- t = ((i `App` k) ::: Nothing)
kk = (k `App` k) ::: Nothing
app = parse("x y")
x = parse("x")
y = parse("y")
abstr = parse("\\x.y")
cti = parse("/\\A^*.\\x:A.x") -- kinding of Lambda vars is not sufficient

ts="\\x:Z^*->Y^*->X^*.\\y:Z^*->Y^*.\\z:Z^*.(x z)(y z)"
tk="\\x:Xk^*.\\y:Yk^*.x"
tskk=parse("("++ts++")"++" ("++tk++") "++tk)

tsk=parse("(/\\Z^*./\\Y^*./\\X^*."++ts++
          ") Xk^* Yk^* Xk^*"++" ("++tk++")") -- ++tk)

-- check annotation in abstraction expressions

aexp = parse "\\x:A^*->A^*.x"

-- illegal generalisation 

wrongfa = parse "/\\ A^*. (x:A^*)"

-- Matthes

moniso = "(\\F.&Am.&A.(Am->A) -> F Am -> F A)"
monisoan = "(\\F^*=>*.&Am^*.&A^*.(Am->A) -> F Am -> F A)"

monanti = "(\\F.&Am.&A.(Am->A) -> F A -> F Am)"
monantian = "(\\F^*=>*.&Am^*.&A^*.(Am->A) -> F A -> F Am)"

--mi = parse ("x:"++moniso)
--ma = parse ("x:"++monanti)

-- 1.2

prmi = moniso++"\\A.B"
prmian = monisoan++"\\A^*.B^*"

prma = monanti++"\\A.B"
prmaan = monantian++"\\A^*.B^*"

proofproj = parse "/\\ B^*. /\\ Am^*. /\\ A^*. \\ f:Am^*->A^*. \\ x:B^*. x"

-- 1.3
idmi = moniso++"\\A.A"
idmian = monisoan++"\\A^*.A"

proofidmi = parse ("/\\Am./\\A.\\f:Am->A.\\x:Am^*.f x"++":"++idmi)
proofidmian = parse ("/\\Am^*./\\A^*.\\f:(Am->A)^*.\\x:Am^*.f x"++
                     ":"++idmian)
proofidmian2 = parse ("/\\Am^*./\\A^*.\\f:(Am^*->A^*)^*.\\x:Am^*.f x"++
                     ":"++idmian)

-- 1.4
{-
proofsumpresisotone =  parse $ "/\\F./\\G."++
                     "\\x:"++monisoan++"F."++
                     "\\y:"++monisoan++"G."++
                     "/\\Am./\\A."++
                     "\\f:Am->A."++
                     "\\z:F Am % G Am."++
                     "z{x1:F Am.INL(x Am A f x1): G A + F A, "++
                     "  y1:G Am.INL(y Am A f y1): G A + F A}"++
                     ":&F.&G.("++monisoan++"F)->"++
                     "("++monisoan++"G)->(\\A.F A + G A)"

proofprodpresisotone = parse $ "/\\F^*=>*./\\G^*=>*."++
                     "\\x:"++monisoan++"F^*=>*."++
                     "\\y:"++monisoan++"G^*=>*."++
                     "/\\Am^*./\\A^*."++
                     "\\f:Am^*->A^*."++
                     "\\z:F^*=>* Am^* % G^*=>* Am^*."++
                     "<x, y>"++ -- "<x Am^* A^* f (z L), y Am^* A^* f (z R)>"++
                     ":&F^*=>*.&G^*=>*.("++monisoan++"F^*=>*)->"++
                     "("++monisoan++"G^*=>*)->(\\A^*.F A % G A)"
proofprodpresisotone2 = parse $
                     "/\\F^*./\\G^*."++
                     "\\x:"++monisoan++"F^*=>*.x " --  ++
                     "\\y:"++monisoan++"G."++
                     "/\\Am./\\A."++
                     "\\f:Am->A."++
                     "\\z:F Am % G Am."++
                     "<x Am A f (z L), y Am A f (z R)>"  ++
                     ":&F.&G.("++monisoan++"F)->"++
                     "("++monisoan++"G)->(\\A.F A % G A)"
-}

-- 1.5

-- 1.6

-- 1.7

-- 1.8

-- mail

proofpair = parse "\\ x:A^*.<x,x>"
prooffapair = parse "/\\ A^*. \\ x:A^*.<x,x>"

proofsum = parse "\\ x:A^*.(INL x:A+B^*)"
prooffasum = parse "/\\ A^*. \\ x:A^*.(INL x:A+B^*)"

proofsumiso = parse $ "(/\\ A^*. /\\ B^*. \\ f:A^*->B^*. \\ c:A^*+A^*. "++
                      "(INL (c{cl:A^*.f cl:B^*, cr:A^*.f cr:B^*}):B^*+B^*)"++
                      "):("++monisoan++")\\X^*.X + X"
proofprodiso = parse $
  "/\\ A^*. /\\ B^*. \\ f:A^*->B^*. \\ p:A^*%A^*. <f(p L),f(p R)>"++
  ":("++monisoan++")\\X^*.X % X"

1.6  Das Makefile

GHC=ghc
HUGS=hugs
HAPPY=/usr/src/happy-1.10/happy/src/happy.sh
RM=rm
PERL=perl
MAKE=make

DEBUG=
GHC_OPTS=-package lang -package net

TEXS=KS.tex HistorySKK.tex ChurchNumerals.tex UrzyChains.tex \
     MonotonicityWitnesses.tex Tabular.tex SimplePair.tex \
     ProofProjIsIsotone.tex ProofSumIsIsotone.tex \
     ProofPairingIsIsotone.tex ProofIdentityIsIsotone.tex \
     WrongForall.tex TypedSK.tex Proof22KIsTypable.tex \
     ProofProdPresIsotone.tex ProofSumPresIsotone.tex

MAINS=Parser CPFwCGI

.PHONY: all
all: ${TEXS} ${MAINS}

.PHONY: ${MAINS} ${basename ${TEXS}}
${MAINS} ${basename ${TEXS}}: %: %.hs
	EXIT=(1 1); \
	until test "$${EXIT[1]}" == "0"; do \
	  ${GHC} ${GHC_OPTS} --make $< -o $@ 2>&1 \
	  | ${PERL} -p \
	            -e 'BEGIN {$$remade=0;}' \
	            -e "if (/(can't find module )\`(.*)'$$/ || " \
	            -e '    /^(Skipping  |Compiling ).*\( (.*)\.hs\, .* \)$$/ )' \
                    -e '  {if (system "${MAKE} -q $$2.hs")' \
                    -e '    {if (!system "${MAKE} $$2.hs") {$$remade=1}}}' \
	            -e 'END {exit $$remade;}'; \
	  EXIT=($${PIPESTATUS[*]}); \
	done; \
	exit $${EXIT[0]}

%.hs: %.y
	${HAPPY} -a ${DEBUG} $< -o $@

%.info: %.y
	${HAPPY} -a -i $< 

${TEXS}: %.tex: %
	./$< > $@

.PHONY: tar
tar:
	cvs checkout -d /tmp/fopra/ fopra
	WD=$$(pwd); cd /tmp/; tar -cvjf $$WD/fopra.tar.bz2 fopra/
	rm -fr /tmp/fopra

.PHONY: GHCVersion.tex
GHCVersion.tex:
	( echo "{\tt " ; ${GHC} --version ; echo " }" ) > $@

.PHONY: HugsVersion.tex
HugsVersion.tex:
	( echo "{\tt " ; \
	  (echo ":version" | ${HUGS} 2>/dev/null | perl -n \
	       -e 'if (/^Prelude> -- (Hugs Version .+)$$/) {print $$1 }'); \
	  echo " }" ) > $@

.PHONY: clean
clean:
	${RM} -f *.o
	${RM} -f *.hi
	${RM} -f ParseCPFw.hs
	${RM} -f ParseCPFw.info
	${RM} -f ${TEXS}
	${RM} -f ${basename ${TEXS}}
	${RM} -f ${MAINS}
	${RM} -f GHCVersion.tex
	${RM} -f HugsVersion.tex
	${RM} -f fopra.tar.bz2

Footnotes: