{- |
Module      :  ./HolLight/Helper.hs
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 :: [String]
names =
 let
  nextName :: String -> String
nextName [] = "a"
  nextName (x :: Char
x : xs :: String
xs) = if Char -> Int
Char.ord Char
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 122
                     then 'a' Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String
nextName String
xs
                     else Int -> Char
Char.chr (Char -> Int
Char.ord Char
x Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) Char -> String -> String
forall a. a -> [a] -> [a]
: String
xs
 in (String -> String) -> String -> [String]
forall a. (a -> a) -> a -> [a]
iterate (String -> String
forall a. [a] -> [a]
reverse (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
nextName (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
forall a. [a] -> [a]
reverse) "a"

freeName :: [String] -> String
freeName :: [String] -> String
freeName ns :: [String]
ns = [String] -> String
forall a. [a] -> a
head ((String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ x :: String
x -> case (String -> Bool) -> [String] -> Maybe String
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
x) [String]
ns
                              of Nothing -> Bool
True
                                 _ -> Bool
False) [String]
names)

fromRight :: Either t t1 -> t1
fromRight :: Either t t1 -> t1
fromRight e :: Either t t1
e = case Either t t1
e of
  Right t :: t1
t -> t1
t
  Left _ -> String -> t1
forall a. HasCallStack => String -> a
error "fromRight"

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

ppPrintType :: HolType -> Doc
ppPrintType :: HolType -> Doc
ppPrintType = Int -> HolType -> Doc
sot 0

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

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

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

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

isVar :: Term -> Bool
isVar :: Term -> Bool
isVar v :: Term
v = Maybe (String, HolType) -> Bool
forall a. Maybe a -> Bool
isJust (Term -> Maybe (String, HolType)
destVar Term
v)

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

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

variant :: [Term] -> Term -> Maybe Term
variant :: [Term] -> Term -> Maybe Term
variant avoid :: [Term]
avoid v :: Term
v = if Bool -> Bool
not ((Term -> Bool) -> [Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Term -> Term -> Bool
vfreeIn Term
v) [Term]
avoid) then Term -> Maybe Term
forall a. a -> Maybe a
Just Term
v
                  else case Term
v of
                         Var s :: String
s ty :: HolType
ty p :: HolTermInfo
p -> [Term] -> Term -> Maybe Term
variant [Term]
avoid (String -> HolType -> HolTermInfo -> Term
Var (String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ "'") HolType
ty HolTermInfo
p)
                         _ -> Maybe Term
forall a. Maybe a
Nothing

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

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

isComb :: Term -> Bool
isComb :: Term -> Bool
isComb c :: Term
c = Maybe (Term, Term) -> Bool
forall a. Maybe a -> Bool
isJust (Term -> Maybe (Term, Term)
destComb Term
c)

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

isConst :: Term -> Bool
isConst :: Term -> Bool
isConst c :: Term
c = Maybe (String, HolType) -> Bool
forall a. Maybe a -> Bool
isJust (Term -> Maybe (String, HolType)
destConst Term
c)

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

isAbs :: Term -> Bool
isAbs :: Term -> Bool
isAbs a :: Term
a = Maybe (Term, Term) -> Bool
forall a. Maybe a -> Bool
isJust (Term -> Maybe (Term, Term)
destAbs Term
a)

rator :: Term -> Maybe Term
rator :: Term -> Maybe Term
rator tm :: Term
tm = ((Term, Term) -> Term) -> Maybe (Term, Term) -> Maybe Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Term, Term) -> Term
forall a b. (a, b) -> a
fst (Term -> Maybe (Term, Term)
destComb Term
tm)

rand :: Term -> Maybe Term
rand :: Term -> Maybe Term
rand tm :: Term
tm = ((Term, Term) -> Term) -> Maybe (Term, Term) -> Maybe Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Term, Term) -> Term
forall a b. (a, b) -> b
snd (Term -> Maybe (Term, Term)
destComb Term
tm)

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

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

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

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

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

typeSubst :: [(HolType, HolType)] -> HolType -> HolType
typeSubst :: [(HolType, HolType)] -> HolType -> HolType
typeSubst i :: [(HolType, HolType)]
i ty :: HolType
ty = case HolType
ty of
  TyApp tycon :: String
tycon args :: [HolType]
args -> let args' :: [HolType]
args' = (HolType -> HolType) -> [HolType] -> [HolType]
forall a b. (a -> b) -> [a] -> [b]
map ([(HolType, HolType)] -> HolType -> HolType
typeSubst [(HolType, HolType)]
i) [HolType]
args
                      in if [HolType]
args' [HolType] -> [HolType] -> Bool
forall a. Eq a => a -> a -> Bool
== [HolType]
args then HolType
ty else String -> [HolType] -> HolType
TyApp String
tycon [HolType]
args'
  _ -> HolType -> [(HolType, HolType)] -> HolType -> HolType
forall t1 t. Eq t1 => t1 -> [(t, t1)] -> t -> t
revAssocd HolType
ty [(HolType, HolType)]
i HolType
ty

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

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

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

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

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

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

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

stripExists :: Term -> ([Term], Term)
stripExists :: Term -> ([Term], Term)
stripExists = (Term -> Maybe (Term, Term)) -> Term -> ([Term], Term)
forall t a. (t -> Maybe (a, t)) -> t -> ([a], t)
splitlist Term -> Maybe (Term, Term)
destExists

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

stripForall :: Term -> ([Term], Term)
stripForall :: Term -> ([Term], Term)
stripForall = (Term -> Maybe (Term, Term)) -> Term -> ([Term], Term)
forall t a. (t -> Maybe (a, t)) -> t -> ([a], t)
splitlist Term -> Maybe (Term, Term)
destForall

stripComb :: Term -> (Term, [Term])
stripComb :: Term -> (Term, [Term])
stripComb = (Term -> Maybe (Term, Term)) -> Term -> (Term, [Term])
forall t t1. (t -> Maybe (t, t1)) -> t -> (t, [t1])
revSplitlist Term -> Maybe (Term, Term)
destComb

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

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

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

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

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

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

isGabs :: Term -> Bool
isGabs :: Term -> Bool
isGabs tm :: Term
tm = Maybe (Term, Term) -> Bool
forall a. Maybe a -> Bool
isJust (Term -> Maybe (Term, Term)
destGabs Term
tm)

stripGabs :: Term -> ([Term], Term)
stripGabs :: Term -> ([Term], Term)
stripGabs = (Term -> Maybe (Term, Term)) -> Term -> ([Term], Term)
forall t a. (t -> Maybe (a, t)) -> t -> ([a], t)
splitlist Term -> Maybe (Term, Term)
destGabs

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

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

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

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

destBinary :: Term -> Term -> Maybe (Term, Term)
destBinary :: Term -> Term -> Maybe (Term, Term)
destBinary c :: Term
c tm :: Term
tm = case Term -> Maybe (Term, Term)
destComb Term
tm of -- original name: DEST_BINARY
  Just (il :: Term
il, r :: Term
r) -> case Term -> Maybe (Term, Term)
destComb Term
il of
    Just (i :: Term
i, l :: Term
l) -> if (Term
i Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
c) Bool -> Bool -> Bool
||
      (Term -> Bool
isConst Term
i Bool -> Bool -> Bool
&& Term -> Bool
isConst Term
c Bool -> Bool -> Bool
&&
       ((String, Maybe HolParseType) -> String
forall a b. (a, b) -> a
fst ((String, Term) -> (String, Maybe HolParseType)
reverseInterface ((String, HolType) -> String
forall a b. (a, b) -> a
fst (Maybe (String, HolType) -> (String, HolType)
forall a. HasCallStack => Maybe a -> a
fromJust (Term -> Maybe (String, HolType)
destConst Term
i)), Term
i))
       String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== (String, Maybe HolParseType) -> String
forall a b. (a, b) -> a
fst ((String, Term) -> (String, Maybe HolParseType)
reverseInterface ((String, HolType) -> String
forall a b. (a, b) -> a
fst (Maybe (String, HolType) -> (String, HolType)
forall a. HasCallStack => Maybe a -> a
fromJust (Term -> Maybe (String, HolType)
destConst Term
c)), Term
i))))
      then (Term, Term) -> Maybe (Term, Term)
forall a. a -> Maybe a
Just (Term
l, Term
r)
      else Maybe (Term, Term)
forall a. Maybe a
Nothing
    _ -> Maybe (Term, Term)
forall a. Maybe a
Nothing
  _ -> Maybe (Term, Term)
forall a. Maybe a
Nothing

powerof10 :: Integer -> Bool
powerof10 :: Integer -> Bool
powerof10 n :: Integer
n = (10 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div Integer
n 10) Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
n

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

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

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

destClause :: Term -> Maybe [Term]
destClause :: Term -> Maybe [Term]
destClause tm :: Term
tm = case (Term -> ([Term], Term)) -> Maybe Term -> Maybe ([Term], Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> ([Term], Term)
stripExists (Maybe Term -> (Term -> Maybe Term) -> Maybe Term -> Maybe Term
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Maybe Term
forall a. Maybe a
Nothing Term -> Maybe Term
body (Term -> Maybe Term
body Term
tm)) of
  Just (_, pbod :: Term
pbod) -> let (s :: Term
s, args :: [Term]
args) = Term -> (Term, [Term])
stripComb Term
pbod
                   in case (Term -> String
nameOf Term
s, [Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args) of
                     ("_UNGUARDED_PATTERN", 2) ->
                       case (Term -> Maybe Term
randRator ([Term] -> Term
forall a. [a] -> a
head [Term]
args),
                             Term -> Maybe Term
randRator ([Term]
args [Term] -> Int -> Term
forall a. [a] -> Int -> a
!! 1)) of
                         (Just _1 :: Term
_1, Just _2 :: Term
_2) -> [Term] -> Maybe [Term]
forall a. a -> Maybe a
Just [Term
_1, Term
_2]
                         _ -> Maybe [Term]
forall a. Maybe a
Nothing
                     ("_GUARDED_PATTERN", 3) ->
                       case (Term -> Maybe Term
randRator ([Term] -> Term
forall a. [a] -> a
head [Term]
args),
                             Term -> Maybe Term
randRator ([Term]
args [Term] -> Int -> Term
forall a. [a] -> Int -> a
!! 2)) of
                         (Just _1 :: Term
_1, Just _3 :: Term
_3) -> [Term] -> Maybe [Term]
forall a. a -> Maybe a
Just [Term
_1, [Term]
args [Term] -> Int -> Term
forall a. [a] -> Int -> a
!! 1, Term
_3]
                         _ -> Maybe [Term]
forall a. Maybe a
Nothing
                     _ -> Maybe [Term]
forall a. Maybe a
Nothing
  _ -> Maybe [Term]
forall a. Maybe a
Nothing

destClauses :: Term -> Maybe [[Term]]
destClauses :: Term -> Maybe [[Term]]
destClauses tm :: Term
tm = let (s :: Term
s, args :: [Term]
args) = Term -> (Term, [Term])
stripComb Term
tm
                  in if Term -> String
nameOf Term
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "_SEQPATTERN" Bool -> Bool -> Bool
&& [Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 2
                     then case Term -> Maybe [[Term]]
destClauses ([Term]
args [Term] -> Int -> Term
forall a. [a] -> Int -> a
!! 1) of
                       Just cs :: [[Term]]
cs -> case Term -> Maybe [Term]
destClause ([Term] -> Term
forall a. [a] -> a
head [Term]
args) of
                         Just c :: [Term]
c -> [[Term]] -> Maybe [[Term]]
forall a. a -> Maybe a
Just ([Term]
c [Term] -> [[Term]] -> [[Term]]
forall a. a -> [a] -> [a]
: [[Term]]
cs)
                         _ -> Maybe [[Term]]
forall a. Maybe a
Nothing
                       _ -> Maybe [[Term]]
forall a. Maybe a
Nothing
                     else case Term -> Maybe [Term]
destClause Term
tm of
                       Just c :: [Term]
c -> [[Term]] -> Maybe [[Term]]
forall a. a -> Maybe a
Just [[Term]
c]
                       _ -> Maybe [[Term]]
forall a. Maybe a
Nothing

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

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

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

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