gistfile1.hs

{-# OPTIONS_GHC -XViewPatterns #-}

module Derivation
    where

import Control.Monad.Error

-- import AbstractTree
-- Stump definition of Expr
data Expr = Variable String Int | Type | Kind deriving (Eq)

data DerivationRule =
      AxiomRule
    | StartRule
    | WeakeningRule
    | ApplicationRule
    | AbstractionRule
    | ConversionRule
    | SpecificRule

-- Derivation name assumptions gamma a T
data Derivation = Derivation DerivationRule [Derivation] [Expr] Expr Expr

-- Get conclusion of a derivation.  
conc (Derivation _ _ gamma expr typ) = (gamma, expr, typ)

typeOrKind = (`elem` [Type, Kind])

wellformed :: Derivation -> Either Derivation ()

wellformed (Derivation AxiomRule [] [] Type Kind) = return ()

wellformed (Derivation StartRule
            [ d@(conc -> (gamma, typeA, s)) ]
            ((== typeA:gamma) -> True)
            (Variable _ 0)
            ((== typeA) -> True)) = wellformed d

wellformed (Derivation WeakeningRule
            [ d1@(conc -> (gamma, typeA, typeB)),
              d2@(conc -> (((== gamma) -> True), typeC, (typeOrKind -> True))) ]
            ((== typeC:gamma) -> True)
            ((== typeA) -> True)
            ((== typeB) -> True)) = do wellformed d1
                                       wellformed d2

{- 
-- This is the old version of the above rule.
all_eq :: (Eq a) => [a] -> Bool
all_eq [] = True
all_eq (x:xs) = all ((==) x) xs

wellformed (Derivation WeakeningRule
                [ d1@(Derivation _ _ gamma typeA typeB)
                , d2@(Derivation _ _ gamma' typeC' s)]
                (typeC:gamma'') typeA' typeB')
    | all_eq [gamma, gamma', gamma''] &&
      all_eq [typeA, typeA'] &&
      all_eq [typeB, typeB'] &&
      all_eq [typeC, typeC'] &&
      s `elem` [Type, Kind] = do
        wellformed d1
        wellformed d2

-}