{- |
Module      :  $Header$
Description :  Helper functions for dealing with terms
                (mainly for pretty printing which is
                 directly adapted from hollight)
Copyright   :  (c) Jonathan von Schroeder, DFKI GmbH 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  jonathan.von_schroeder@dfki.de
Stability   :  experimental
Portability :  portable

-}

module HolLight.Helper where

import Data.Maybe (fromJust, isJust, catMaybes)
import HolLight.Term
import Data.List (union, (\\), find)
import Common.Doc
import Data.Char as Char

names :: [String]
names =
 let
  nextName [] = "a"
  nextName (x : xs) = if Char.ord x >= 122
                     then 'a' : nextName xs
                     else Char.chr (Char.ord x + 1) : xs
 in iterate (reverse . nextName . reverse) "a"

freeName :: [String] -> String
freeName ns = head (filter (\ x -> case find (== x) ns
                              of Nothing -> True
                                 _ -> False) names)

fromRight :: Either t t1 -> t1
fromRight e = case e of
  Right t -> t
  Left _ -> error "fromRight"

isPrefix :: Term -> Bool
isPrefix tm = case tm of
  Var _ _ (HolTermInfo (PrefixT, _)) -> True
  Const _ _ (HolTermInfo (PrefixT, _)) -> True
  _ -> False

ppPrintType :: HolType -> Doc
ppPrintType = sot 0

soc :: String -> Bool -> [Doc] -> Doc
soc sep' flag ss = if null ss then empty
  else let s = foldr1 (\ s1 s2 -> hcat [s1, text sep', s2]) ss
       in if flag then parens s else s

sot :: Int -> HolType -> Doc
sot pr ty = case (destVartype ty, destType ty) of
  -- exactly one of these is not Nothing
  (Just vtype, _) -> text vtype
  (_, Just t) -> case t of
    (con, []) -> text con
    ("fun", [ty1, ty2]) -> soc "->" (pr > 0) [sot 1 ty1, sot 0 ty2]
    ("sum", [ty1, ty2]) -> soc "+" (pr > 2) [sot 3 ty1, sot 2 ty2]
    ("prod", [ty1, ty2]) -> soc "#" (pr > 4) [sot 5 ty1, sot 4 ty2]
    ("cart", [ty1, ty2]) -> soc "^" (pr > 6) [sot 6 ty1, sot 7 ty2]
    (con, args) -> hcat [soc "," True (map (sot 0) args), text con]
  _ -> empty -- doesn't happen

-- lib.ml
revAssocd :: Eq t1 => t1 -> [(t, t1)] -> t -> t
revAssocd a l d = case l of
  [] -> d
  (x, y) : t -> if y == a then x
                       else revAssocd a t d

-- fusion.ml
destVar :: Term -> Maybe (String, HolType)
destVar v = case v of
  Var s ty _ -> Just (s, ty)
  _ -> Nothing

isVar :: Term -> Bool
isVar v = isJust (destVar v)

frees :: Term -> [Term]
frees tm = case tm of
  Var {} -> [tm]
  Const {} -> []
  Abs bv bod -> frees bod \\ [bv]
  Comb s t -> frees s `union` frees t

vfreeIn :: Term -> Term -> Bool
vfreeIn v tm = case tm of
  Abs bv bod -> v /= bv && vfreeIn v bod
  Comb s t -> vfreeIn v s || vfreeIn v t
  _ -> tm == v

variant :: [Term] -> Term -> Maybe Term
variant avoid v = if not (any (vfreeIn v) avoid) then Just v
                  else case v of
                         Var s ty p -> variant avoid (Var (s ++ "'") ty p)
                         _ -> Nothing

vsubst :: [(Term, Term)] -> Term -> Maybe Term
vsubst =
  let vsubst' ilist tm = case tm of
                           Var {} -> Just $ revAssocd tm ilist tm
                           Const {} -> Just tm
                           Comb s t -> case (vsubst' ilist s, vsubst ilist t) of
                             (Just s', Just t') -> Just $ if s' == s && t' == t
                                                  then tm
                                                  else Comb s' t'
                             _ -> Nothing
                           Abs v s -> let ilist' = filter (\ (_, x) -> x /= v)
                                                          ilist
                             in if null ilist' then Just tm
                                else case vsubst ilist' s of
                                  Just s' | s' == s -> Just tm
                                          | any (\ (t, x) -> vfreeIn v t
                                                            && vfreeIn x s)
                                                ilist' ->
                                            case variant [s'] v of
                                                Just v' -> case vsubst
                                                 ((v', v) : ilist') s of
                                                  Just t' ->
                                                   Just (Abs v' t')
                                                  _ -> Nothing
                                                _ -> Nothing
                                          | otherwise -> Just (Abs v s')
                                  _ -> Nothing
  in \ theta ->
    if null theta then Just else
    if all (\ (t, x) -> case (typeOf t, destVar x) of
                         (Just t', Just (_, x')) -> t' == x'
                         _ -> False) theta then vsubst' theta
    else const Nothing

destComb :: Term -> Maybe (Term, Term)
destComb c = case c of
  Comb f x -> Just (f, x)
  _ -> Nothing

isComb :: Term -> Bool
isComb c = isJust (destComb c)

destConst :: Term -> Maybe (String, HolType)
destConst c = case c of
  Const s ty _ -> Just (s, ty)
  _ -> Nothing

isConst :: Term -> Bool
isConst c = isJust (destConst c)

destAbs :: Term -> Maybe (Term, Term)
destAbs a = case a of
  Abs v b -> Just (v, b)
  _ -> Nothing

isAbs :: Term -> Bool
isAbs a = isJust (destAbs a)

rator :: Term -> Maybe Term
rator tm = fmap fst (destComb tm)

rand :: Term -> Maybe Term
rand tm = fmap snd (destComb tm)

splitlist :: (t -> Maybe (a, t)) -> t -> ([a], t)
splitlist dest x = case dest x of
  Just (l, r) -> let (ls, res) = splitlist dest r
                in (l : ls, res)
  _ -> ([], x)

revSplitlist :: (t -> Maybe (t, t1)) -> t -> (t, [t1])
revSplitlist dest x =
  let rsplist ls x' = case dest x' of
                       Just (l, r) -> rsplist (r : ls) l
                       _ -> (x', ls)
  in rsplist [] x

typeOf :: Term -> Maybe HolType
typeOf tm = case tm of
  Var _ ty _ -> Just ty
  Const _ ty _ -> Just ty
  Comb s _ -> case typeOf s of
                Just t -> case destType t of
                            Just (_, _ : x1 : _) -> Just x1
                            _ -> Nothing
                _ -> Nothing
  Abs (Var _ ty _) t -> case typeOf t of
                         Just t' -> Just (TyApp "fun" [ty, t'])
                         _ -> Nothing
  _ -> Nothing

destType :: HolType -> Maybe (String, [HolType])
destType a = case a of
  TyApp s ty -> Just (s, ty)
  _ -> Nothing

destVartype :: HolType -> Maybe String
destVartype t = case t of
  TyVar s -> Just s
  _ -> Nothing

typeSubst :: [(HolType, HolType)] -> HolType -> HolType
typeSubst i ty = case ty of
  TyApp tycon args -> let args' = map (typeSubst i) args
                      in if args' == args then ty else TyApp tycon args'
  _ -> revAssocd ty i ty

mkEq :: (Term, Term) -> Maybe Term
mkEq (l, r) = case (typeOf l, mkConst ("=", [])) of
               (Just ty, Just eq) -> case inst [(ty, TyVar "A")] eq of
                                Right eq_tm -> case mkComb (eq_tm, l) of
                                  Just m1 -> mkComb (m1, r)
                                  _ -> Nothing
                                _ -> Nothing
               _ -> Nothing

inst :: [(HolType, HolType)] -> Term -> Either Term Term
inst =
  let inst' env tyin tm = case tm of
                            Var n ty at -> let ty' = typeSubst tyin ty
                              in let tm' = if ty' == ty then tm
                                           else Var n ty' at
                                 in if revAssocd tm' env tm == tm
                                    then Right tm'
                                    else Left tm'
                            Const c ty at -> let ty' = typeSubst tyin ty
                              in Right $ if ty' == ty
                                 then tm
                                 else Const c ty' at
                            Comb f x -> case (inst' env tyin f,
                                              inst' env tyin x) of
                                          (Right f', Right x') ->
                                           Right $ if f' == f && x' == x
                                                   then tm else Comb f' x'
                                          (Left c, _) -> Left c
                                          (_, Left c) -> Left c
                            Abs y t -> case inst' [] tyin y of
                              Right y' -> let env' = (y, y') : env
                                in case inst' env' tyin t of
                                     Right t' ->
                                      Right $ if y' == y && t' == t
                                       then tm else Abs y' t'
                                     Left w' -> if w' /= y'
                                       then Left w'
                                       else let ifrees = map (fromRight .
                                                               inst' [] tyin)
                                                              (frees t) in
                                             case variant ifrees y' of
                                               Just y'' ->
                                                case (destVar y'', destVar y) of
                                                 (Just (v1, _), Just (_, v2)) ->
                                                  let z = Var v1 v2
                                                           (HolTermInfo
                                                           (Normal, Nothing))
                                                  in case vsubst [(z, y)] t of
                                                      Just s -> inst' env tyin
                                                       (Abs z s)
                                                      _ -> Left w'
                                                 _ -> Left w'
                                               _ -> Left w'
                              _ -> Left tm
  in (\ tyin -> if null tyin then Right else inst' [] tyin)

mkComb :: (Term, Term) -> Maybe Term
mkComb (f, a) = case typeOf f of
  Just (TyApp "fun" [ty, _]) -> case typeOf a of
    Just t -> if ty == t then Just (Comb f a) else Nothing
    _ -> Nothing
  _ -> Nothing

eqType :: HolType
eqType = TyApp "fun" [
  TyVar "A",
  TyApp "fun" [
    TyVar "A",
    TyApp "bool" []
  ]]

mkConst :: (String, [(HolType, HolType)]) -> Maybe Term
mkConst (name, theta) = if name == "="
                        then Just (Const name
                                   (typeSubst theta eqType)
                                   (HolTermInfo (InfixR 12, Nothing)))
                        else Nothing

-- basics.ml
destBinder :: String -> Term -> Maybe (Term, Term)
destBinder s tm = case tm of
  Comb (Const s' _ _) (Abs x t) ->
    if s' == s then Just (x, t)
    else Nothing
  _ -> Nothing

destExists :: Term -> Maybe (Term, Term)
destExists = destBinder "?"

stripExists :: Term -> ([Term], Term)
stripExists = splitlist destExists

destForall :: Term -> Maybe (Term, Term)
destForall = destBinder "!"

stripForall :: Term -> ([Term], Term)
stripForall = splitlist destForall

stripComb :: Term -> (Term, [Term])
stripComb = revSplitlist destComb

body :: Term -> Maybe Term
body tm = case destAbs tm of
  Just (_, ret) -> Just ret
  _ -> Nothing

destNumeral :: Term -> Maybe Integer
destNumeral tm' =
  let dest_num tm = case destConst tm of
                      Just ("_0", _) -> Just (toInteger (0 :: Int))
                      _ -> case destComb tm of
                             Just (l, r) -> case dest_num r of
                                             Just i ->
                                               let n = toInteger (2 :: Int) * i
                                               in case destConst l of
                                                    Just ("BIT0", _) -> Just n
                                                    Just ("BIT1", _) -> Just (n
                                                      + toInteger (1 :: Int))
                                                    _ -> Nothing
                                             _ -> Nothing
                             _ -> Nothing
  in case destComb tm' of
       Just (l, r) -> case destConst l of
                     Just ("NUMERAL", _) -> dest_num r
                     _ -> Nothing
       _ -> Nothing

destBinary' :: String -> Term -> Maybe (Term, Term)
destBinary' s tm = case tm of
  Comb (Comb (Const s' _ _) l) r -> if s' == s then Just (l, r)
                                  else Nothing
  _ -> Nothing

destCons :: Term -> Maybe (Term, Term)
destCons = destBinary' "CONS"

destList :: Term -> Maybe [Term]
destList tm = let (tms, nil) = splitlist destCons tm
               in case destConst nil of
                    Just ("NIL", _) -> Just tms
                    _ -> Nothing

destGabs :: Term -> Maybe (Term, Term)
destGabs tm =
  let dest_geq = destBinary' "GEQ"
  in if isAbs tm then destAbs tm
     else case destComb tm of
            Just (l, r) -> case destConst l of
                            Just ("GABS", _) -> case body r of
                              Just b -> case dest_geq (snd (stripForall b)) of
                                Just (ltm, rtm) -> case rand ltm of
                                  Just r' -> Just (r', rtm)
                                  _ -> Nothing
                                _ -> Nothing
                              _ -> Nothing
                            _ -> Nothing
            _ -> Nothing

isGabs :: Term -> Bool
isGabs tm = isJust (destGabs tm)

stripGabs :: Term -> ([Term], Term)
stripGabs = splitlist destGabs

destFunTy :: HolType -> Maybe (HolType, HolType)
destFunTy ty = case ty of
  TyApp "fun" [ty1, ty2] -> Just (ty1, ty2)
  _ -> Nothing

destLet :: Term -> Maybe ([(Term, Term)], Term)
destLet tm = let (l, aargs) = stripComb tm
              in case (aargs, destConst l) of
                   (a : as, Just ("LET", _)) ->
                     let (vars, lebod) = stripGabs a
                     in let eqs = zip vars as
                        in case destComb lebod of
                             Just (le, bod) -> case destConst le of
                              Just ("LET_END", _) -> Just (eqs, bod)
                              _ -> Nothing
                             _ -> Nothing
                   _ -> Nothing

-- printer.ml
nameOf :: Term -> String
nameOf tm = case tm of
  Var x _ _ -> x
  Const x _ _ -> x
  _ -> ""

-- printer.ml - pp_print_term
reverseInterface :: (String, Term) -> (String, Maybe HolParseType)
reverseInterface (s, tm) = case tm of
  Var _ _ ti -> case ti of
    HolTermInfo (_, Just (s'', pt)) -> (s'', Just pt)
    _ -> (s, Nothing)
  Const _ _ ti -> case ti of
    HolTermInfo (_, Just (s'', pt)) -> (s'', Just pt)
    _ -> (s, Nothing)
  _ -> (s, Nothing)

destBinary :: Term -> Term -> Maybe (Term, Term)
destBinary c tm = case destComb tm of -- original name: DEST_BINARY
  Just (il, r) -> case destComb il of
    Just (i, l) -> if (i == c) ||
      (isConst i && isConst c &&
       (fst (reverseInterface (fst (fromJust (destConst i)), i))
       == fst (reverseInterface (fst (fromJust (destConst c)), i))))
      then Just (l, r)
      else Nothing
    _ -> Nothing
  _ -> Nothing

powerof10 :: Integer -> Bool
powerof10 n = (10 * div n 10) == n

boolOfTerm :: Term -> Maybe Bool
boolOfTerm t = case t of
  Const "T" _ _ -> Just True
  Const "F" _ _ -> Just False
  _ -> Nothing

codeOfTerm :: Num b => Term -> Maybe b
codeOfTerm t =
  let (f, tms) = stripComb t in
  if not (isConst f && fst (fromJust (destConst f)) == "ASCII")
     || length tms /= 8
  then Nothing
  else let bools = map boolOfTerm (reverse tms)
       in if notElem Nothing bools then
          Just (foldr (\ b f' -> if b then 1 + 2 * f' else 2 * f')
                0 (catMaybes bools))
          else Nothing

randRator :: Term -> Maybe Term
randRator v = case rator v of
  Just v1 -> rand v1
  _ -> Nothing

destClause :: Term -> Maybe [Term]
destClause tm = case fmap stripExists (maybe Nothing body (body tm)) of
  Just (_, pbod) -> let (s, args) = stripComb pbod
                   in case (nameOf s, length args) of
                     ("_UNGUARDED_PATTERN", 2) ->
                       case (randRator (head args),
                             randRator (args !! 1)) of
                         (Just _1, Just _2) -> Just [_1, _2]
                         _ -> Nothing
                     ("_GUARDED_PATTERN", 3) ->
                       case (randRator (head args),
                             randRator (args !! 2)) of
                         (Just _1, Just _3) -> Just [_1, args !! 1, _3]
                         _ -> Nothing
                     _ -> Nothing
  _ -> Nothing

destClauses :: Term -> Maybe [[Term]]
destClauses tm = let (s, args) = stripComb tm
                  in if nameOf s == "_SEQPATTERN" && length args == 2
                     then case destClauses (args !! 1) of
                       Just cs -> case destClause (head args) of
                         Just c -> Just (c : cs)
                         _ -> Nothing
                       _ -> Nothing
                     else case destClause tm of
                       Just c -> Just [c]
                       _ -> Nothing

aright :: Term -> Bool
aright tm = case tm of
  Var _ _ (HolTermInfo (InfixR _, _)) -> True
  Const _ _ (HolTermInfo (InfixR _, _)) -> True
  _ -> False

getPrec :: Term -> Int
getPrec tm = case tm of
  Var _ _ (HolTermInfo (InfixR i, _)) -> i
  Const _ _ (HolTermInfo (InfixR i, _)) -> i
  _ -> 0

parsesAsBinder :: Term -> Bool
parsesAsBinder tm = case tm of
  Var _ _ (HolTermInfo (Binder, _)) -> True
  Const _ _ (HolTermInfo (Binder, _)) -> True
  _ -> False

canGetInfixStatus :: Term -> Bool
canGetInfixStatus tm = case tm of
  Var _ _ (HolTermInfo (InfixR _, _)) -> True
  Var _ _ (HolTermInfo (InfixL _, _)) -> True
  Const _ _ (HolTermInfo (InfixR _, _)) -> True
  Const _ _ (HolTermInfo (InfixL _, _)) -> True
  _ -> False
