Links und Funktionen
Sprachumschaltung

Navigationspfad
Sie sind hier: Startseite / Lehre / SS 2014 / Programmierung und Modellierung / ProMo Material / Vorlage H8-3 (Unifikation)


Inhaltsbereich

Vorlage H8-3 (Unifikation)

Dateivorlage zu Aufgabe H8-3 (Unifikation 2) Bearbeiten Sie nur die mit "-- TODO" markierte Stelle! Sie dürfen auch neue Hilfsfunktion definieren, und alle vorhandenen Funktion nutzen; Sie dürfen aber nicht vorhandene Definitionen, Hilfsfunktion oder importierten Module abändern!

Haskell source code icon H8-3_Vorlage.hs — Haskell source code, 3 KB (3640 bytes)

Dateiinhalt

import Data.List
import qualified Data.Map as Map

data TTyp = TVar Identifier
          | TInt | TBool 
          | TArrow TTyp TTyp
  deriving (Eq) -- Show-Instanz weiter unten von Hand deklariert

type Identifier = String  
  
type TEq  = (TTyp,TTyp) -- Eine Typgleichung


-- !!! NUR UNTERHALB DIESER ZEILE EDITIEREN !!! --
------------------------------------------------  
  
unify :: [TEq]  -> TSub
unify = -- TODO: implementieren Sie diese Funktion gemäß Vorlesungsfolie 08-S.48!
  error "Teilnehmer hat unify leider noch nicht implementiert!"

------------------------------------------------  
-- !!! NUR OBERHALB DIESER ZEILE EDITIEREN !!! --
-- Hilfsfunktionen:

hasTVar :: Identifier -> TTyp -> Bool    -- Prüft ob Typvariable im Typ vorkommt
hasTVar var = has
  where -- Abkürzung "has", um nicht bei jedem rekursiven Aufruf jedes mal var übergeben zu müssen
    has :: TTyp -> Bool
    has (TVar v1)      = v1 == var
    has (TArrow t1 t2) = has t1 || has t2
    has _othertype     = False
    
--------------------------------
-- All About Typesubstitutions

newtype TSub = TSub (Map.Map Identifier TTyp) -- Eine Typsubstitution
  -- newtype, damit wir eigene Show-Instanz definieren können, ansonsten würde type reichen


idSub :: TSub
idSub = TSub $ Map.empty

makeSub :: (Identifier, TTyp) -> TSub
makeSub = TSub . uncurry Map.singleton 

composeSubs :: TSub -> TSub -> TSub
composeSubs (TSub s1) (TSub s2) = TSub $ Map.union (Map.map (applySub $ TSub s2) s1) s2 
-- proper merging of overlapping substitution
-- s1 is applied first, then s2 is applied

applySub :: TSub -> TTyp -> TTyp
applySub (TSub sigma) = applySigma 
  where 
    applySigma t1@(TVar v1)   = Map.findWithDefault t1 v1 sigma 
    applySigma (TArrow t1 t2) = TArrow (applySigma t1) (applySigma t2)    
    applySigma othertype      = othertype

applySub2Equation :: TSub -> TEq -> TEq
applySub2Equation sigma (t1,t2) = (s t1, s t2)
  where s = applySub sigma
  
    
------------------------------------      
-- Beispiele zum Testen, z.B. mit:
-- > unify aufg1
-- 
alpha, beta, gamma, delta :: TTyp  
alpha = TVar "a"
beta  = TVar "b"
gamma = TVar "c"
delta = TVar "d"
  
aufg0, aufg1, aufg2, aufg3, aufg4, aufg5, aufg6 :: [TEq]  

aufg0 = [(alpha,TBool),(beta,TInt),(alpha,gamma)]

aufg1 = [(alpha `TArrow` beta, TBool `TArrow` beta)]

aufg2 =  [(alpha,beta),(beta,gamma)]

aufg3 = [(t1,t2)]
 where
   t1 = TArrow TInt  $ TArrow alpha beta
   t2 = TArrow alpha $ TArrow beta  TInt
   
aufg4 = [(t1,t2)] -- zirkulär
 where
   t1 = alpha `TArrow` (alpha `TArrow` TInt)
   t2 = (TInt `TArrow` beta) `TArrow` beta
   
aufg5 =  [(t1,t2)]
 where
   t1 = alpha `TArrow` (alpha `TArrow` TBool)
   t2 = (TBool `TArrow` beta) `TArrow` gamma
   
aufg6 =  [(t1,t2)] -- Typfehler
 where
   t1 = TInt `TArrow` alpha
   t2 = alpha `TArrow` TBool
  
-----------------------------------------------
-- Anzeige von TTyp und TSub


instance Show TTyp where -- etwas hübschere Show-Instanz als die automatisch generierte
{--- Herkömmliche Variante:
  show (TVar v)       = v
  show (TInt)         = "Int"
  show (TBool)        = "Bool"  
  show (TArrow t1 t2) = "(" ++ (show t1) ++ ") -> " ++ (show t2)  
  --
  -- Mit intelligenter Klammerung: 
-}
  showsPrec _ (TVar v)         = showString v
  showsPrec _ (TInt)           = showString "Int"
  showsPrec _ (TBool)          = showString "Bool" 
  showsPrec n (t1 `TArrow` t2) = showParen (n>0) $ (showsPrec 1 t1) . showString " -> " . showsPrec 0 t2  

instance Show TSub where
  show (TSub sigma) = '[':subs ++ "]"
    where subs = intercalate ", " $ map (\(v,t) -> show t ++ '/':v) $ Map.assocs sigma 
  

Artikelaktionen


Funktionsleiste