module HaskHOL.Core.Basics.Nets
( Net
, netEmpty
, netEnter
, netLookup
, netMerge
) where
import HaskHOL.Core.Lib
import HaskHOL.Core.Kernel
import HaskHOL.Core.State
import HaskHOL.Core.Basics (genVar, stripComb)
setInsert :: Ord a => a -> [a] -> [a]
setInsert a xs = fromMaybe xs $ sinsert a xs
where sinsert :: Ord a => a -> [a] -> Maybe [a]
sinsert x [] = Just [x]
sinsert x l@(h:t)
| h == x = Nothing
| x < h = Just (x:l)
| otherwise = do t' <- sinsert x t
return (h:t')
setMerge :: Ord a => [a] -> [a] -> [a]
setMerge [] l2 = l2
setMerge l1 [] = l1
setMerge l1@(h1:t1) l2@(h2:t2)
| h1 == h2 = h1 : setMerge t1 t2
| h1 < h2 = h1 : setMerge t1 l2
| otherwise = h2 : setMerge l1 t2
data TermLabel
= VNet
| LCNet String Int
| CNet String Int
| LNet Int
| LTyAbs
| LTyComb
deriving (Eq, Show)
data Net a = NetNode [(TermLabel, Net a)] [a] deriving Show
netEmpty :: Net a
netEmpty = NetNode [] []
labelToStore :: [HOLTerm] -> HOLTerm -> HOL cls thry (TermLabel, [HOLTerm])
labelToStore lconsts tm =
let (op, args) = stripComb tm in
case view op of
(Const x _ _) -> return (CNet x (length args), args)
(Abs bv bod) ->
do bod' <- if bv `elem` lconsts
then do v <- genVar $ typeOf bv
return $! varSubst [(bv, v)] bod
else return bod
return (LNet (length args), bod':args)
(TyAbs _ t) -> return (LTyAbs, [t])
(TyComb t _) -> return (LTyComb, [t])
(Var x _) -> return $! if op `elem` lconsts
then (LCNet x (length args), args)
else (VNet, [])
_ -> error "labelToStore: stripComb broken"
netUpdate :: Ord a => [HOLTerm] -> (a, [HOLTerm], Net a) -> HOL cls thry (Net a)
netUpdate _ (b, [], NetNode edges tips) =
return . NetNode edges $ setInsert b tips
netUpdate lconsts (b, tm:rtms, NetNode edges tips) =
do (label, ntms) <- labelToStore lconsts tm
let (child, others) = case remove (\ (x, _) -> x == label) edges of
Just edges' -> (snd `ffComb` id) edges'
Nothing -> (netEmpty, edges)
newChild <- netUpdate lconsts (b, ntms++rtms, child)
return $! NetNode ((label, newChild):others) tips
netEnter :: Ord a => [HOLTerm] -> (HOLTerm, a) -> Net a -> HOL cls thry (Net a)
netEnter lconsts (tm, b) net = netUpdate lconsts (b, [tm], net)
labelForLookup :: HOLTerm -> (TermLabel, [HOLTerm])
labelForLookup tm =
let (op, args) = stripComb tm in
case view op of
(Const x _ _ ) -> (CNet x (length args), args)
(Abs _ bod) -> (LNet (length args), bod:args)
(TyAbs _ t) -> (LTyAbs, [t])
(TyComb t _) -> (LTyComb, [t])
(Var x _) -> (LCNet x (length args), args)
_ -> error "labelForLookup: stripComb broken"
follow :: ([HOLTerm], Net a) -> [a]
follow ([], NetNode _ tips) = tips
follow (tm:rtms, NetNode edges _) =
let (label, ntms) = labelForLookup tm
collection = case lookup label edges of
Just child -> follow (ntms++rtms, child)
Nothing -> [] in
if label == VNet then collection
else case lookup VNet edges of
Just vn -> collection ++ follow (rtms, vn)
Nothing -> collection
netLookup :: HOLTerm -> Net a -> [a]
netLookup tm net = follow ([tm], net)
netMerge :: Ord a => Net a -> Net a -> Net a
netMerge (NetNode l1 data1) (NetNode l2 data2) =
NetNode (foldr addNode (foldr addNode [] l1) l2) $ setMerge data1 data2
where addNode :: Ord a => (TermLabel, Net a) -> [(TermLabel, Net a)] ->
[(TermLabel, Net a)]
addNode p@(lab, net) l =
case remove (\ (x, _) -> x == lab) l of
Just ((lab', net'), rest) ->
(lab', netMerge net net'):rest
Nothing -> p:l
deriveLiftMany [''TermLabel, ''Net]