IsabelleTerm.hs

module IsabelleTerm where
import IsabelleType
import Mixfix

type Pattern = Term

-- LCF terms in HOLCF
data Term
  = HVar String
  | HAbs [String] Term -- should probably be [Pattern]
  | HAbsTuple [String] Term
  | HApp Term Term
  | HInfix Term String Term
  | HTuple [Term]
  | HList [Term]
  | HLet [HMatch] Term
  | HIte Term Term Term -- if-then-else
  | HInt Integer
  | HCase Term [HAlt]
  | HConstrain Term Type
  | HMixfix String [Int] Int [Term]

data HAlt = HAlt Pattern Term

head_of_Term :: Term -> String
head_of_Term (HApp t _) = head_of_Term t
head_of_Term (HInfix _ s _) = s
head_of_Term (HVar s) = s

-- hIte = HMixfix "If _ then _ else _ fi" [0,0,0] 60
hApps t ts = foldl HApp t ts
hCon c ts = hApps (HVar c) ts

isHVar (HVar _) = True
isHVar _ = False

hAbs (HVar x) (HAbs xs t) = HAbs (x:xs) t
hAbs (HVar x) t = HAbs [x] t
hAbs (HTuple ts) t | all isHVar ts = HAbsTuple (map (\(HVar x) -> x) ts) t
hAbs p t = error ("hAbs: illegal pattern " ++ show p)

hAbss ps t = foldr hAbs t ps

nomatch = HVar "UU"

data HMatch
  = HMatch Pattern Term

head_of_HMatch :: HMatch -> String
head_of_HMatch (HMatch lhs rhs) = head_of_Term lhs

data HMatches
  = HMatches [HMatch]

head_of_HMatches :: HMatches -> String
head_of_HMatches (HMatches (m:ms)) = head_of_HMatch m

data FixrecDecl
  = FixrecDecl [HMatches]

------------------------------------------------------------

instance Show Term where
  showsPrec p x = case x of
    HVar s -> showString s
    HAbs xs t -> mixfix "LAM _. _"
                    [showSpaceSep (map showString xs), showsPrec 10 t] 10 p
    HAbsTuple xs t -> mixfix "LAM <_>. _"
                    [showCommaSep (map showString xs), showsPrec 10 t] 10 p
    HApp t t' -> mixfix "_$_" [showsPrec 999 t, showsPrec 1000 t'] 999 p
    HInfix t o t' -> mixfix "_ `_ _" [showsPrec 900 t, showString o, showsPrec 900 t'] 0 p
    HTuple ts -> showSpace . showAngles (showCommaSep (map shows ts))
    HList [] -> showString "[:]"
    HList ts -> showLR "[:" ":]" (showCommaSep (map shows ts))
    HIte b x y -> mixfix "If _ then _ else _ fi" [shows b, shows x, shows y] 60 p
    HInt n -> shows n -- mixfix "Def _" [shows n] 999 p
    HMixfix s ps p0 ts -> mixfix s (zipWith ($) (map showsPrec ps) ts) p0 p
    HCase t alts ->
            mixfix "case _ of _" [shows t, showBarSep (map shows alts)] 10 p
    HConstrain x t -> mixfix "_::_" [showsPrec 4 x, shows t] 3 p

instance Show HAlt where
  showsPrec p (HAlt lhs rhs) = mixfix "_ => _" [shows lhs, shows rhs] 10 p

instance Show HMatch where
  showsPrec p (HMatch lhs rhs) = mixfix "_ = _" [showsPrec 50 lhs, showsPrec 51 rhs] 50 p

instance Show HMatches where
  showsPrec p (HMatches ms) = showAll (map (showLR "  \"" "\"\n" . shows) ms)

instance Show FixrecDecl where
  showsPrec _ (FixrecDecl blocks) =
    showString "fixrec\n" . (showSep (showString "and\n") (map shows blocks))