{- |
Module      :  ./HolLight/HolLight2DG.hs
Description :  Import data generated by hol2hets into a DG
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.HolLight2DG where

import Static.GTheory
import Static.DevGraph

import Static.DgUtils
import Static.History
import Static.ComputeTheory

import Logic.Logic
import Logic.Prover
import Logic.ExtSign
import Logic.Grothendieck

import Common.LibName
import Common.Id
import Common.IRI (simpleIdToIRI)
import Common.AS_Annotation
import Common.Result
import Common.Utils
import Common.SAX
import Control.Monad
import Common.Lib.Maybe
import qualified Control.Monad.Fail as Fail
import qualified Data.ByteString.Lazy as L
import Text.XML.Expat.SAX

import HolLight.Sign
import HolLight.Sentence
import HolLight.Term
import HolLight.Logic_HolLight

import HolLight.Helper (names)

import Driver.Options

import Data.Graph.Inductive.Graph
import qualified Data.Map as Map
import Data.Maybe (fromMaybe)

import System.Exit
import System.Directory
import System.FilePath

readTuple :: (Show a, Show b) => MSaxState a -> MSaxState b -> MSaxState (a, b)
readTuple :: MSaxState a -> MSaxState b -> MSaxState (a, b)
readTuple f1 :: MSaxState a
f1 f2 :: MSaxState b
f2 = do
 Bool -> String -> MSaxState String
expectTag Bool
True "tuple"
 a
t1 <- MSaxState a -> String -> MSaxState a
forall a. MSaxState a -> String -> MSaxState a
readWithTag MSaxState a
f1 "fst"
 b
t2 <- MSaxState b -> String -> MSaxState b
forall a. MSaxState a -> String -> MSaxState a
readWithTag MSaxState b
f2 "snd"
 Bool -> String -> MSaxState String
expectTag Bool
False "tuple"
 (a, b) -> MSaxState (a, b)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
t1, b
t2)

readWord :: MSaxState String
readWord :: MSaxState String
readWord = (String -> String) -> MSaxState String -> MSaxState String
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM String -> String
forall a. [a] -> [a]
reverse (MSaxState String -> MSaxState String)
-> MSaxState String -> MSaxState String
forall a b. (a -> b) -> a -> b
$ (String -> MSaxState String) -> String -> MSaxState String
forall (m :: * -> *) a.
Monad m =>
(a -> MaybeT m a) -> a -> MaybeT m a
foldCatchLeft (\ s :: String
s ->
 do
  String
s' <- do
   MSaxState ()
dropSpaces
   SaxEvL
d <- MSaxState SaxEvL
getD
   case SaxEvL
d of
     [] -> String -> MSaxState String
forall a. HasCallStack => String -> a
error "HolLight.readWord"
     h :: SAXEvent String String
h : xs :: SaxEvL
xs -> case SAXEvent String String
h of
       CharacterData s' :: String
s' -> do
         SaxEvL -> MSaxState ()
putD SaxEvL
xs
         String -> MSaxState String
forall (m :: * -> *) a. Monad m => a -> m a
return String
s'
       _ -> String -> MSaxState String
forall a. String -> MSaxState a
debugS (String -> MSaxState String) -> String -> MSaxState String
forall a b. (a -> b) -> a -> b
$ "Expected character data but instead got: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SAXEvent String String -> String
forall a. Show a => a -> String
show SAXEvent String String
h
  String -> MSaxState String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> MSaxState String) -> String -> MSaxState String
forall a b. (a -> b) -> a -> b
$ String -> String
trimLeft (String -> String
forall a. [a] -> [a]
reverse (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String
trimLeft String
s') String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s) []

readStr :: MSaxState String
readStr :: MSaxState String
readStr = MSaxState String -> String -> MSaxState String
forall a. MSaxState a -> String -> MSaxState a
readWithTag MSaxState String
readWord "s"

readInt :: MSaxState Int
readInt :: MSaxState Int
readInt = do
 String
w <- MSaxState String
readWord
 Int -> MSaxState Int
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> MSaxState Int) -> Int -> MSaxState Int
forall a b. (a -> b) -> a -> b
$ Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe (String -> Int
forall a. HasCallStack => String -> a
error "HolLight.readInt") (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ String -> Maybe Int
forall a. Read a => String -> Maybe a
readMaybe String
w

readInt' :: MSaxState Int
readInt' :: MSaxState Int
readInt' = MSaxState Int -> String -> MSaxState Int
forall a. MSaxState a -> String -> MSaxState a
readWithTag MSaxState Int
readInt "i"

readMappedInt :: Map.Map Int a -> MSaxState a
readMappedInt :: Map Int a -> MSaxState a
readMappedInt m :: Map Int a
m = do
 Int
i <- MSaxState Int
readInt
 case Int -> Map Int a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
i Map Int a
m of
  Just a :: a
a -> a -> MSaxState a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
  _ -> String -> MSaxState a
forall a. String -> MSaxState a
debugS (String -> MSaxState a) -> String -> MSaxState a
forall a b. (a -> b) -> a -> b
$ "readMappedInt: Integer " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ " not mapped"

listToTypes :: Map.Map Int HolType -> [Int] -> Maybe [HolType]
listToTypes :: Map Int HolType -> [Int] -> Maybe [HolType]
listToTypes m :: Map Int HolType
m l :: [Int]
l = case [Int]
l of
 x :: Int
x : xs :: [Int]
xs -> case Int -> Map Int HolType -> Maybe HolType
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
x Map Int HolType
m of
  Just t :: HolType
t -> case Map Int HolType -> [Int] -> Maybe [HolType]
listToTypes Map Int HolType
m [Int]
xs of
   Just ts :: [HolType]
ts -> [HolType] -> Maybe [HolType]
forall a. a -> Maybe a
Just (HolType
t HolType -> [HolType] -> [HolType]
forall a. a -> [a] -> [a]
: [HolType]
ts)
   _ -> Maybe [HolType]
forall a. Maybe a
Nothing
  _ -> Maybe [HolType]
forall a. Maybe a
Nothing
 [] -> [HolType] -> Maybe [HolType]
forall a. a -> Maybe a
Just []

readSharedHolType :: Map.Map Int String -> Map.Map Int HolType
                      -> MSaxState (Map.Map Int HolType)
readSharedHolType :: Map Int String -> Map Int HolType -> MSaxState (Map Int HolType)
readSharedHolType sl :: Map Int String
sl m :: Map Int HolType
m = do
 (SaxEvL, DbgData)
d <- MSaxState (SaxEvL, DbgData)
getM
 (b :: Bool
b, t :: String
t) <- MSaxState (Bool, String)
tag
 case (Bool
b, String
t) of
  (True, "TyApp") -> do
   (i :: Int
i, l :: [Int]
l) <- MSaxState Int -> MSaxState [Int] -> MSaxState (Int, [Int])
forall a b.
(Show a, Show b) =>
MSaxState a -> MSaxState b -> MSaxState (a, b)
readTuple MSaxState Int
readInt (MSaxState Int -> MSaxState [Int]
forall (m :: * -> *) a. Monad m => MaybeT m a -> MaybeT m [a]
whileM MSaxState Int
readInt')
   case (Int -> Map Int String -> Maybe String
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
i Map Int String
sl, Map Int HolType -> [Int] -> Maybe [HolType]
listToTypes Map Int HolType
m [Int]
l) of
    (Just s :: String
s, Just l' :: [HolType]
l') -> do
     Bool -> String -> MSaxState String
expectTag Bool
False "TyApp"
     Map Int HolType -> MSaxState (Map Int HolType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Int HolType -> MSaxState (Map Int HolType))
-> Map Int HolType -> MSaxState (Map Int HolType)
forall a b. (a -> b) -> a -> b
$ Int -> HolType -> Map Int HolType -> Map Int HolType
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Map Int HolType -> Int
forall k a. Map k a -> Int
Map.size Map Int HolType
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) (String -> [HolType] -> HolType
TyApp String
s ([HolType] -> HolType) -> [HolType] -> HolType
forall a b. (a -> b) -> a -> b
$ [HolType] -> [HolType]
forall a. [a] -> [a]
reverse [HolType]
l') Map Int HolType
m
    (r1 :: Maybe String
r1, r2 :: Maybe [HolType]
r2) -> String -> MSaxState (Map Int HolType)
forall a. String -> MSaxState a
debugS (String -> MSaxState (Map Int HolType))
-> String -> MSaxState (Map Int HolType)
forall a b. (a -> b) -> a -> b
$ "readSharedHolType: Couldn't build TyApp"
                        String -> String -> String
forall a. [a] -> [a] -> [a]
++ " because the result of the lookup for "
                        String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int, [Int]) -> String
forall a. Show a => a -> String
show (Int
i, [Int]
l) String -> String -> String
forall a. [a] -> [a] -> [a]
++ " was " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Maybe String, Maybe [HolType]) -> String
forall a. Show a => a -> String
show (Maybe String
r1, Maybe [HolType]
r2)
  (True, "TyVar") -> do
   Int
i <- MSaxState Int
readInt
   case Int -> Map Int String -> Maybe String
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
i Map Int String
sl of
    Just s :: String
s -> do
     Bool -> String -> MSaxState String
expectTag Bool
False "TyVar"
     Map Int HolType -> MSaxState (Map Int HolType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Int HolType -> MSaxState (Map Int HolType))
-> Map Int HolType -> MSaxState (Map Int HolType)
forall a b. (a -> b) -> a -> b
$ Int -> HolType -> Map Int HolType -> Map Int HolType
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Map Int HolType -> Int
forall k a. Map k a -> Int
Map.size Map Int HolType
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) (String -> HolType
TyVar String
s) Map Int HolType
m
    _ -> String -> MSaxState (Map Int HolType)
forall a. String -> MSaxState a
debugS (String -> MSaxState (Map Int HolType))
-> String -> MSaxState (Map Int HolType)
forall a b. (a -> b) -> a -> b
$ "readSharedHolType: Couldn't build TyVar"
                  String -> String -> String
forall a. [a] -> [a] -> [a]
++ " because looking up " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
                  String -> String -> String
forall a. [a] -> [a] -> [a]
++ " failed"
  _ -> do
   (SaxEvL, DbgData) -> MSaxState ()
putM (SaxEvL, DbgData)
d
   String -> MSaxState (Map Int HolType)
forall a. String -> MSaxState a
debugS (String -> MSaxState (Map Int HolType))
-> String -> MSaxState (Map Int HolType)
forall a b. (a -> b) -> a -> b
$ "readSharedHolType: Expected a hol type but"
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ " instead got following tag: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Bool, String) -> String
forall a. Show a => a -> String
show (Bool
b, String
t)

readParseType :: MSaxState HolParseType
readParseType :: MSaxState HolParseType
readParseType = do
 (b :: Bool
b, t :: String
t) <- MSaxState (Bool, String)
tag
 case (Bool
b, String
t) of
  (True, "Prefix") -> do
   Bool -> String -> MSaxState String
expectTag Bool
False "Prefix"
   HolParseType -> MSaxState HolParseType
forall (m :: * -> *) a. Monad m => a -> m a
return HolParseType
PrefixT
  (True, "InfixR") -> do
   Int
i <- MSaxState Int
readInt
   Bool -> String -> MSaxState String
expectTag Bool
False "InfixR"
   HolParseType -> MSaxState HolParseType
forall (m :: * -> *) a. Monad m => a -> m a
return (HolParseType -> MSaxState HolParseType)
-> HolParseType -> MSaxState HolParseType
forall a b. (a -> b) -> a -> b
$ Int -> HolParseType
InfixR Int
i
  (True, "InfixL") -> do
   Int
i <- MSaxState Int
readInt
   Bool -> String -> MSaxState String
expectTag Bool
False "InfixL"
   HolParseType -> MSaxState HolParseType
forall (m :: * -> *) a. Monad m => a -> m a
return (HolParseType -> MSaxState HolParseType)
-> HolParseType -> MSaxState HolParseType
forall a b. (a -> b) -> a -> b
$ Int -> HolParseType
InfixL Int
i
  (True, "Normal") -> do
   Bool -> String -> MSaxState String
expectTag Bool
False "Normal"
   HolParseType -> MSaxState HolParseType
forall (m :: * -> *) a. Monad m => a -> m a
return HolParseType
Normal
  (True, "Binder") -> do
   Bool -> String -> MSaxState String
expectTag Bool
False "Binder"
   HolParseType -> MSaxState HolParseType
forall (m :: * -> *) a. Monad m => a -> m a
return HolParseType
Binder
  _ -> String -> MSaxState HolParseType
forall a. String -> MSaxState a
debugS (String -> MSaxState HolParseType)
-> String -> MSaxState HolParseType
forall a b. (a -> b) -> a -> b
$ "readParseType: Expected a parse type but"
                String -> String -> String
forall a. [a] -> [a] -> [a]
++ " instead got following tag: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Bool, String) -> String
forall a. Show a => a -> String
show (Bool
b, String
t)

readTermInfo :: MSaxState HolTermInfo
readTermInfo :: MSaxState HolTermInfo
readTermInfo = do
 HolParseType
p <- MSaxState HolParseType
readParseType
 State (SaxEvL, DbgData) (Maybe HolTermInfo)
-> MSaxState HolTermInfo
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (State (SaxEvL, DbgData) (Maybe HolTermInfo)
 -> MSaxState HolTermInfo)
-> State (SaxEvL, DbgData) (Maybe HolTermInfo)
-> MSaxState HolTermInfo
forall a b. (a -> b) -> a -> b
$ do
  Maybe (String, HolParseType)
v <- MaybeT (State (SaxEvL, DbgData)) (String, HolParseType)
-> State (SaxEvL, DbgData) (Maybe (String, HolParseType))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT (State (SaxEvL, DbgData)) (String, HolParseType)
 -> State (SaxEvL, DbgData) (Maybe (String, HolParseType)))
-> MaybeT (State (SaxEvL, DbgData)) (String, HolParseType)
-> State (SaxEvL, DbgData) (Maybe (String, HolParseType))
forall a b. (a -> b) -> a -> b
$ MSaxState String
-> MSaxState HolParseType
-> MaybeT (State (SaxEvL, DbgData)) (String, HolParseType)
forall a b.
(Show a, Show b) =>
MSaxState a -> MSaxState b -> MSaxState (a, b)
readTuple MSaxState String
readWord MSaxState HolParseType
readParseType
  case Maybe (String, HolParseType)
v of
   Just _ -> Maybe HolTermInfo -> State (SaxEvL, DbgData) (Maybe HolTermInfo)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe HolTermInfo -> State (SaxEvL, DbgData) (Maybe HolTermInfo))
-> Maybe HolTermInfo -> State (SaxEvL, DbgData) (Maybe HolTermInfo)
forall a b. (a -> b) -> a -> b
$ HolTermInfo -> Maybe HolTermInfo
forall a. a -> Maybe a
Just (HolTermInfo -> Maybe HolTermInfo)
-> HolTermInfo -> Maybe HolTermInfo
forall a b. (a -> b) -> a -> b
$ (HolParseType, Maybe (String, HolParseType)) -> HolTermInfo
HolTermInfo (HolParseType
p, Maybe (String, HolParseType)
v)
   _ -> Maybe HolTermInfo -> State (SaxEvL, DbgData) (Maybe HolTermInfo)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe HolTermInfo -> State (SaxEvL, DbgData) (Maybe HolTermInfo))
-> Maybe HolTermInfo -> State (SaxEvL, DbgData) (Maybe HolTermInfo)
forall a b. (a -> b) -> a -> b
$ HolTermInfo -> Maybe HolTermInfo
forall a. a -> Maybe a
Just (HolTermInfo -> Maybe HolTermInfo)
-> HolTermInfo -> Maybe HolTermInfo
forall a b. (a -> b) -> a -> b
$ (HolParseType, Maybe (String, HolParseType)) -> HolTermInfo
HolTermInfo (HolParseType
p, Maybe (String, HolParseType)
forall a. Maybe a
Nothing)

readSharedHolTerm :: Map.Map Int HolType -> Map.Map Int String
                      -> Map.Map Int Term -> MSaxState (Map.Map Int Term)
readSharedHolTerm :: Map Int HolType
-> Map Int String -> Map Int Term -> MSaxState (Map Int Term)
readSharedHolTerm ts :: Map Int HolType
ts sl :: Map Int String
sl m :: Map Int Term
m = do
 (SaxEvL, DbgData)
d <- MSaxState (SaxEvL, DbgData)
getM
 (b :: Bool
b, tg :: String
tg) <- MSaxState (Bool, String)
tag
 case (Bool
b, String
tg) of
  (True, "Var") -> do
   (n :: Int
n, t :: Int
t) <- MSaxState Int -> MSaxState Int -> MSaxState (Int, Int)
forall a b.
(Show a, Show b) =>
MSaxState a -> MSaxState b -> MSaxState (a, b)
readTuple MSaxState Int
readInt MSaxState Int
readInt
   HolTermInfo
ti <- MSaxState HolTermInfo
readTermInfo
   case (Int -> Map Int String -> Maybe String
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
n Map Int String
sl, Int -> Map Int HolType -> Maybe HolType
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
t Map Int HolType
ts) of
    (Just name :: String
name, Just tp :: HolType
tp) -> do
     Bool -> String -> MSaxState String
expectTag Bool
False "Var"
     Map Int Term -> MSaxState (Map Int Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Int Term -> MSaxState (Map Int Term))
-> Map Int Term -> MSaxState (Map Int Term)
forall a b. (a -> b) -> a -> b
$ Int -> Term -> Map Int Term -> Map Int Term
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Map Int Term -> Int
forall k a. Map k a -> Int
Map.size Map Int Term
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) (String -> HolType -> HolTermInfo -> Term
Var String
name HolType
tp HolTermInfo
ti) Map Int Term
m
    (r1 :: Maybe String
r1, r2 :: Maybe HolType
r2) -> String -> MSaxState (Map Int Term)
forall a. String -> MSaxState a
debugS (String -> MSaxState (Map Int Term))
-> String -> MSaxState (Map Int Term)
forall a b. (a -> b) -> a -> b
$ "readSharedHolTerm: Couldn't build Var"
                  String -> String -> String
forall a. [a] -> [a] -> [a]
++ " because the result of the lookup for "
                  String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int, Int) -> String
forall a. Show a => a -> String
show (Int
n, Int
t) String -> String -> String
forall a. [a] -> [a] -> [a]
++ " was " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Maybe String, Maybe HolType) -> String
forall a. Show a => a -> String
show (Maybe String
r1, Maybe HolType
r2)
  (True, "Const") -> do
   (n :: Int
n, t :: Int
t) <- MSaxState Int -> MSaxState Int -> MSaxState (Int, Int)
forall a b.
(Show a, Show b) =>
MSaxState a -> MSaxState b -> MSaxState (a, b)
readTuple MSaxState Int
readInt MSaxState Int
readInt
   HolTermInfo
ti <- MSaxState HolTermInfo
readTermInfo
   case (Int -> Map Int String -> Maybe String
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
n Map Int String
sl, Int -> Map Int HolType -> Maybe HolType
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
t Map Int HolType
ts) of
    (Just name :: String
name, Just tp :: HolType
tp) -> do
     Bool -> String -> MSaxState String
expectTag Bool
False "Const"
     Map Int Term -> MSaxState (Map Int Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Int Term -> MSaxState (Map Int Term))
-> Map Int Term -> MSaxState (Map Int Term)
forall a b. (a -> b) -> a -> b
$ Int -> Term -> Map Int Term -> Map Int Term
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Map Int Term -> Int
forall k a. Map k a -> Int
Map.size Map Int Term
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) (String -> HolType -> HolTermInfo -> Term
Const String
name HolType
tp HolTermInfo
ti) Map Int Term
m
    (r1 :: Maybe String
r1, r2 :: Maybe HolType
r2) -> String -> MSaxState (Map Int Term)
forall a. String -> MSaxState a
debugS (String -> MSaxState (Map Int Term))
-> String -> MSaxState (Map Int Term)
forall a b. (a -> b) -> a -> b
$ "readSharedHolTerm: Couldn't build Const"
                  String -> String -> String
forall a. [a] -> [a] -> [a]
++ " because the result of the lookup for "
                  String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int, Int) -> String
forall a. Show a => a -> String
show (Int
n, Int
t) String -> String -> String
forall a. [a] -> [a] -> [a]
++ " was " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Maybe String, Maybe HolType) -> String
forall a. Show a => a -> String
show (Maybe String
r1, Maybe HolType
r2)
  (True, "Comb") -> do
   (t1 :: Int
t1, t2 :: Int
t2) <- MSaxState Int -> MSaxState Int -> MSaxState (Int, Int)
forall a b.
(Show a, Show b) =>
MSaxState a -> MSaxState b -> MSaxState (a, b)
readTuple MSaxState Int
readInt MSaxState Int
readInt
   case (Int -> Map Int Term -> Maybe Term
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
t1 Map Int Term
m, Int -> Map Int Term -> Maybe Term
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
t2 Map Int Term
m) of
    (Just t1' :: Term
t1', Just t2' :: Term
t2') -> do
     Bool -> String -> MSaxState String
expectTag Bool
False "Comb"
     Map Int Term -> MSaxState (Map Int Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Int Term -> MSaxState (Map Int Term))
-> Map Int Term -> MSaxState (Map Int Term)
forall a b. (a -> b) -> a -> b
$ Int -> Term -> Map Int Term -> Map Int Term
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Map Int Term -> Int
forall k a. Map k a -> Int
Map.size Map Int Term
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) (Term -> Term -> Term
Comb Term
t1' Term
t2') Map Int Term
m
    (r1 :: Maybe Term
r1, r2 :: Maybe Term
r2) -> String -> MSaxState (Map Int Term)
forall a. String -> MSaxState a
debugS (String -> MSaxState (Map Int Term))
-> String -> MSaxState (Map Int Term)
forall a b. (a -> b) -> a -> b
$ "readSharedHolTerm: Couldn't build Comb"
                  String -> String -> String
forall a. [a] -> [a] -> [a]
++ " because the result of the lookup for "
                  String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int, Int) -> String
forall a. Show a => a -> String
show (Int
t1, Int
t2) String -> String -> String
forall a. [a] -> [a] -> [a]
++ " was " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Maybe Term, Maybe Term) -> String
forall a. Show a => a -> String
show (Maybe Term
r1, Maybe Term
r2)
  (True, "Abs") -> do
   (t1 :: Int
t1, t2 :: Int
t2) <- MSaxState Int -> MSaxState Int -> MSaxState (Int, Int)
forall a b.
(Show a, Show b) =>
MSaxState a -> MSaxState b -> MSaxState (a, b)
readTuple MSaxState Int
readInt MSaxState Int
readInt
   case (Int -> Map Int Term -> Maybe Term
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
t1 Map Int Term
m, Int -> Map Int Term -> Maybe Term
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
t2 Map Int Term
m) of
    (Just t1' :: Term
t1', Just t2' :: Term
t2') -> do
     Bool -> String -> MSaxState String
expectTag Bool
False "Abs"
     Map Int Term -> MSaxState (Map Int Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Int Term -> MSaxState (Map Int Term))
-> Map Int Term -> MSaxState (Map Int Term)
forall a b. (a -> b) -> a -> b
$ Int -> Term -> Map Int Term -> Map Int Term
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Map Int Term -> Int
forall k a. Map k a -> Int
Map.size Map Int Term
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) (Term -> Term -> Term
Abs Term
t1' Term
t2') Map Int Term
m
    (r1 :: Maybe Term
r1, r2 :: Maybe Term
r2) -> String -> MSaxState (Map Int Term)
forall a. String -> MSaxState a
debugS (String -> MSaxState (Map Int Term))
-> String -> MSaxState (Map Int Term)
forall a b. (a -> b) -> a -> b
$ "readSharedHoLTerm: Couldn't build Abs"
                  String -> String -> String
forall a. [a] -> [a] -> [a]
++ " because the result of the lookup for "
                  String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int, Int) -> String
forall a. Show a => a -> String
show (Int
t1, Int
t2) String -> String -> String
forall a. [a] -> [a] -> [a]
++ " was " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Maybe Term, Maybe Term) -> String
forall a. Show a => a -> String
show (Maybe Term
r1, Maybe Term
r2)
  _ -> do
   (SaxEvL, DbgData) -> MSaxState ()
putM (SaxEvL, DbgData)
d
   String -> MSaxState (Map Int Term)
forall a. String -> MSaxState a
debugS (String -> MSaxState (Map Int Term))
-> String -> MSaxState (Map Int Term)
forall a b. (a -> b) -> a -> b
$ "readSharedHolTerm: Expected a hol term but"
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ " instead got following tag: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Bool, String) -> String
forall a. Show a => a -> String
show (Bool
b, String
tg)

importData :: HetcatsOpts -> FilePath
  -> IO ([(String, [(String, Term)])], [(String, String)])
importData :: HetcatsOpts
-> String -> IO ([(String, [(String, Term)])], [(String, String)])
importData opts :: HetcatsOpts
opts fp' :: String
fp' = do
  String
fp <- String -> IO String
canonicalizePath String
fp'
  let image :: String
image = "hol_light.dmtcp"
      dmtcpBin :: String
dmtcpBin = "dmtcp_restart"
  String
tmpImage <- String -> String -> IO String
getTempFile "" String
image
  String
imageFile <- (String -> String) -> IO String -> IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String -> String -> String
</> String
image) (IO String -> IO String) -> IO String -> IO String
forall a b. (a -> b) -> a -> b
$ String -> String -> IO String
getEnvDef
   "HETS_HOLLIGHT_TOOLS" "HolLight/OcamlTools/"
  -- for dmtcp we need an image owned by the current user
  String -> String -> IO ()
copyFile String
imageFile String
tmpImage
  Bool
e2 <- String -> IO Bool
doesFileExist String
imageFile
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
e2 (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
image String -> String -> String
forall a. [a] -> [a] -> [a]
++ " not found"
  String
tempFile <- String -> String -> IO String
getTempFile "" (String -> String
takeBaseName String
fp)
  (ex :: ExitCode
ex, sout :: String
sout, err :: String
err) <- String -> [String] -> String -> IO (ExitCode, String, String)
executeProcess String
dmtcpBin [String
tmpImage]
    (String -> IO (ExitCode, String, String))
-> String -> IO (ExitCode, String, String)
forall a b. (a -> b) -> a -> b
$ "use_file " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
fp String -> String -> String
forall a. [a] -> [a] -> [a]
++ ";;\n"
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ "inject_hol_include " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
fp String -> String -> String
forall a. [a] -> [a] -> [a]
++ ";;\n"
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ "export_libs (get_libs()) " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
tempFile String -> String -> String
forall a. [a] -> [a] -> [a]
++ ";;\n"
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ "exit 0;;\n"
  String -> IO ()
removeFile String
tmpImage
  ByteString
s <- String -> IO ByteString
L.readFile String
tempFile
  case ExitCode
ex of
   ExitFailure _ -> do
     String -> IO ()
removeFile String
tempFile
     String -> IO ([(String, [(String, Term)])], [(String, String)])
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> IO ([(String, [(String, Term)])], [(String, String)]))
-> String -> IO ([(String, [(String, Term)])], [(String, String)])
forall a b. (a -> b) -> a -> b
$ "HolLight.importData: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
err
   ExitSuccess -> do
    HetcatsOpts -> Int -> String -> IO ()
putIfVerbose HetcatsOpts
opts 5 String
sout
    let e :: ([a], [a])
e = ([], [])
    (r :: ([(String, [(String, Term)])], [(String, String)])
r, evl :: String
evl, msgs :: Maybe [String]
msgs) <- (([(String, [(String, Term)])], [(String, String)]), String,
 Maybe [String])
-> IO
     (([(String, [(String, Term)])], [(String, String)]), String,
      Maybe [String])
forall (m :: * -> *) a. Monad m => a -> m a
return ((([(String, [(String, Term)])], [(String, String)]), String,
  Maybe [String])
 -> IO
      (([(String, [(String, Term)])], [(String, String)]), String,
       Maybe [String]))
-> (([(String, [(String, Term)])], [(String, String)]), String,
    Maybe [String])
-> IO
     (([(String, [(String, Term)])], [(String, String)]), String,
      Maybe [String])
forall a b. (a -> b) -> a -> b
$ case MSaxState ([(String, [(String, Term)])], [(String, String)])
-> SaxEvL
-> Bool
-> (Maybe ([(String, [(String, Term)])], [(String, String)]),
    (SaxEvL, DbgData))
forall a.
MSaxState a -> SaxEvL -> Bool -> (Maybe a, (SaxEvL, DbgData))
runMSaxState (do
     Bool -> String -> MSaxState String
expectTag Bool
True "HolExport"
     [String]
sl <- MSaxState String -> String -> MSaxState [String]
forall a. Show a => MSaxState a -> String -> MSaxState [a]
readL MSaxState String
readStr "Strings"
     let strings :: Map Int String
strings = [(Int, String)] -> Map Int String
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([Int] -> [String] -> [(Int, String)]
forall a b. [a] -> [b] -> [(a, b)]
zip [1 ..] [String]
sl)
     Map Int HolType
hol_types <- (Map Int HolType -> MSaxState (Map Int HolType))
-> Map Int HolType -> String -> MSaxState (Map Int HolType)
forall a.
Show a =>
(a -> MSaxState a) -> a -> String -> MSaxState a
foldS (Map Int String -> Map Int HolType -> MSaxState (Map Int HolType)
readSharedHolType Map Int String
strings)
                   Map Int HolType
forall k a. Map k a
Map.empty "SharedHolTypes"
     Map Int Term
hol_terms <- (Map Int Term -> MSaxState (Map Int Term))
-> Map Int Term -> String -> MSaxState (Map Int Term)
forall a.
Show a =>
(a -> MSaxState a) -> a -> String -> MSaxState a
foldS (Map Int HolType
-> Map Int String -> Map Int Term -> MSaxState (Map Int Term)
readSharedHolTerm Map Int HolType
hol_types Map Int String
strings)
                   Map Int Term
forall k a. Map k a
Map.empty "SharedHolTerms"
     [(String, [(String, Term)])]
libs <- MSaxState (String, [(String, Term)])
-> String -> MSaxState [(String, [(String, Term)])]
forall a. Show a => MSaxState a -> String -> MSaxState [a]
readL (MSaxState String
-> MSaxState [(String, Term)]
-> MSaxState (String, [(String, Term)])
forall a b.
(Show a, Show b) =>
MSaxState a -> MSaxState b -> MSaxState (a, b)
readTuple MSaxState String
readWord
                    (MaybeT (State (SaxEvL, DbgData)) (String, Term)
-> MSaxState [(String, Term)]
forall (m :: * -> *) a. Monad m => MaybeT m a -> MaybeT m [a]
whileM (MSaxState String
-> MSaxState Term
-> MaybeT (State (SaxEvL, DbgData)) (String, Term)
forall a b.
(Show a, Show b) =>
MSaxState a -> MSaxState b -> MSaxState (a, b)
readTuple MSaxState String
readWord
                             (Map Int Term -> MSaxState Term
forall a. Map Int a -> MSaxState a
readMappedInt Map Int Term
hol_terms)))) "Libs"
     [(String, String)]
liblinks <- MSaxState (String, String)
-> String -> MSaxState [(String, String)]
forall a. Show a => MSaxState a -> String -> MSaxState [a]
readL (MSaxState String -> MSaxState String -> MSaxState (String, String)
forall a b.
(Show a, Show b) =>
MSaxState a -> MSaxState b -> MSaxState (a, b)
readTuple MSaxState String
readWord MSaxState String
readWord) "LibLinks"
     ([(String, [(String, Term)])], [(String, String)])
-> MSaxState ([(String, [(String, Term)])], [(String, String)])
forall (m :: * -> *) a. Monad m => a -> m a
return ([(String, [(String, Term)])]
libs, [(String, String)]
liblinks)) (ByteString -> SaxEvL
parsexml ByteString
s) (HetcatsOpts -> Int
verbose HetcatsOpts
opts Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 6) of
      (de :: Maybe ([(String, [(String, Term)])], [(String, String)])
de, msgs :: (SaxEvL, DbgData)
msgs) -> (([(String, [(String, Term)])], [(String, String)])
-> Maybe ([(String, [(String, Term)])], [(String, String)])
-> ([(String, [(String, Term)])], [(String, String)])
forall a. a -> Maybe a -> a
fromMaybe ([(String, [(String, Term)])], [(String, String)])
forall a a. ([a], [a])
e Maybe ([(String, [(String, Term)])], [(String, String)])
de, "Next 5 items: "
       String -> String -> String
forall a. [a] -> [a] -> [a]
++ SaxEvL -> String
forall a. Show a => a -> String
show (Int -> SaxEvL -> SaxEvL
forall a. Int -> [a] -> [a]
take 5 (SaxEvL -> SaxEvL) -> SaxEvL -> SaxEvL
forall a b. (a -> b) -> a -> b
$ (SaxEvL, DbgData) -> SaxEvL
forall a b. (a, b) -> a
fst (SaxEvL, DbgData)
msgs), DbgData -> Maybe [String]
forall a b. (a, b) -> a
fst (DbgData -> Maybe [String]) -> DbgData -> Maybe [String]
forall a b. (a -> b) -> a -> b
$ (SaxEvL, DbgData) -> DbgData
forall a b. (a, b) -> b
snd (SaxEvL, DbgData)
msgs)
    case Maybe [String]
msgs of
      Just ms :: [String]
ms -> HetcatsOpts -> Int -> String -> IO ()
putIfVerbose HetcatsOpts
opts 6 (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> [String]
forall a. [a] -> [a]
reverse [String]
ms) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
evl
      Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    String -> IO ()
removeFile String
tempFile
    ([(String, [(String, Term)])], [(String, String)])
-> IO ([(String, [(String, Term)])], [(String, String)])
forall (m :: * -> *) a. Monad m => a -> m a
return ([(String, [(String, Term)])], [(String, String)])
r

getTypes :: Map.Map String Int -> HolType -> Map.Map String Int
getTypes :: Map String Int -> HolType -> Map String Int
getTypes m :: Map String Int
m t :: HolType
t = case HolType
t of
 TyVar _ -> Map String Int
m
 TyApp s :: String
s ts :: [HolType]
ts -> let m' :: Map String Int
m' = (Map String Int -> HolType -> Map String Int)
-> Map String Int -> [HolType] -> Map String Int
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Map String Int -> HolType -> Map String Int
getTypes Map String Int
m [HolType]
ts in
                     String -> Int -> Map String Int -> Map String Int
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
s ([HolType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [HolType]
ts) Map String Int
m'

mergeTypesOps :: (Map.Map String Int, Map.Map String HolType)
                 -> (Map.Map String Int, Map.Map String HolType)
                 -> (Map.Map String Int, Map.Map String HolType)
mergeTypesOps :: (Map String Int, Map String HolType)
-> (Map String Int, Map String HolType)
-> (Map String Int, Map String HolType)
mergeTypesOps (ts1 :: Map String Int
ts1, ops1 :: Map String HolType
ops1) (ts2 :: Map String Int
ts2, ops2 :: Map String HolType
ops2) =
 (Map String Int
ts1 Map String Int -> Map String Int -> Map String Int
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` Map String Int
ts2, Map String HolType
ops1 Map String HolType -> Map String HolType -> Map String HolType
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` Map String HolType
ops2)

getOps :: Term
           -> (Map.Map String Int, Map.Map String HolType)
getOps :: Term -> (Map String Int, Map String HolType)
getOps tm :: Term
tm = case Term
tm of
 Var _ t :: HolType
t _ -> let ts :: Map String Int
ts = Map String Int -> HolType -> Map String Int
getTypes Map String Int
forall k a. Map k a
Map.empty HolType
t
                     in (Map String Int
ts, Map String HolType
forall k a. Map k a
Map.empty)
 Const s :: String
s t :: HolType
t _ -> let ts :: Map String Int
ts = Map String Int -> HolType -> Map String Int
getTypes Map String Int
forall k a. Map k a
Map.empty HolType
t
                     in (Map String Int
ts, String -> HolType -> Map String HolType -> Map String HolType
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
s HolType
t Map String HolType
forall k a. Map k a
Map.empty)
 Comb t1 :: Term
t1 t2 :: Term
t2 -> (Map String Int, Map String HolType)
-> (Map String Int, Map String HolType)
-> (Map String Int, Map String HolType)
mergeTypesOps
                  (Term -> (Map String Int, Map String HolType)
getOps Term
t1)
                  (Term -> (Map String Int, Map String HolType)
getOps Term
t2)
 Abs t1 :: Term
t1 t2 :: Term
t2 -> (Map String Int, Map String HolType)
-> (Map String Int, Map String HolType)
-> (Map String Int, Map String HolType)
mergeTypesOps
                  (Term -> (Map String Int, Map String HolType)
getOps Term
t1)
                  (Term -> (Map String Int, Map String HolType)
getOps Term
t2)

calcSig :: [(String, Term)] -> Sign
calcSig :: [(String, Term)] -> Sign
calcSig tm :: [(String, Term)]
tm = let (ts :: Map String Int
ts, os :: Map String HolType
os) = ((Map String Int, Map String HolType)
 -> (String, Term) -> (Map String Int, Map String HolType))
-> (Map String Int, Map String HolType)
-> [(String, Term)]
-> (Map String Int, Map String HolType)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl
                      (\ p :: (Map String Int, Map String HolType)
p (_, t :: Term
t) -> ((Map String Int, Map String HolType)
-> (Map String Int, Map String HolType)
-> (Map String Int, Map String HolType)
mergeTypesOps (Term -> (Map String Int, Map String HolType)
getOps Term
t) (Map String Int, Map String HolType)
p))
                      (Map String Int
forall k a. Map k a
Map.empty, Map String HolType
forall k a. Map k a
Map.empty) [(String, Term)]
tm
                 in Sign :: Map String Int -> Map String HolType -> Sign
Sign {
                   types :: Map String Int
types = Map String Int
ts
                  , ops :: Map String HolType
ops = Map String HolType
os }

sigDepends :: Sign -> Sign -> Bool
sigDepends :: Sign -> Sign -> Bool
sigDepends s1 :: Sign
s1 s2 :: Sign
s2 = (Map String Int -> Int
forall k a. Map k a -> Int
Map.size (Map String Int -> Map String Int -> Map String Int
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.intersection (Sign -> Map String Int
types Sign
s1) (Sign -> Map String Int
types Sign
s2)) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= 0) Bool -> Bool -> Bool
||
                   (Map String HolType -> Int
forall k a. Map k a -> Int
Map.size (Map String HolType -> Map String HolType -> Map String HolType
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.intersection (Sign -> Map String HolType
ops Sign
s1) (Sign -> Map String HolType
ops Sign
s2)) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= 0)

prettifyTypeVarsTp :: HolType -> Map.Map String String
                      -> (HolType, Map.Map String String)
prettifyTypeVarsTp :: HolType -> Map String String -> (HolType, Map String String)
prettifyTypeVarsTp (TyVar s :: String
s) m :: Map String String
m = case String -> Map String String -> Maybe String
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
s Map String String
m of
 Just s' :: String
s' -> (String -> HolType
TyVar String
s', Map String String
m)
 Nothing -> let s' :: String
s' = '\'' Char -> String -> String
forall a. a -> [a] -> [a]
: ([String]
names [String] -> Int -> String
forall a. [a] -> Int -> a
!! Map String String -> Int
forall k a. Map k a -> Int
Map.size Map String String
m)
            in (String -> HolType
TyVar String
s', String -> String -> Map String String -> Map String String
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
s String
s' Map String String
m)
prettifyTypeVarsTp (TyApp s :: String
s ts :: [HolType]
ts) m :: Map String String
m =
 let (ts' :: [HolType]
ts', m' :: Map String String
m') = (([HolType], Map String String)
 -> HolType -> ([HolType], Map String String))
-> ([HolType], Map String String)
-> [HolType]
-> ([HolType], Map String String)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ (ts'' :: [HolType]
ts'', m'' :: Map String String
m'') t :: HolType
t ->
      let (t' :: HolType
t', m''' :: Map String String
m''') = HolType -> Map String String -> (HolType, Map String String)
prettifyTypeVarsTp HolType
t Map String String
m''
      in (HolType
t' HolType -> [HolType] -> [HolType]
forall a. a -> [a] -> [a]
: [HolType]
ts'', Map String String
m''')) ([], Map String String
m) [HolType]
ts
 in (String -> [HolType] -> HolType
TyApp String
s [HolType]
ts', Map String String
m')

prettifyTypeVarsTm :: Term -> Map.Map String String
                      -> (Term, Map.Map String String)
prettifyTypeVarsTm :: Term -> Map String String -> (Term, Map String String)
prettifyTypeVarsTm (Const s :: String
s t :: HolType
t p :: HolTermInfo
p) _ =
 let (t1 :: HolType
t1, m1 :: Map String String
m1) = HolType -> Map String String -> (HolType, Map String String)
prettifyTypeVarsTp HolType
t Map String String
forall k a. Map k a
Map.empty
 in (String -> HolType -> HolTermInfo -> Term
Const String
s HolType
t1 HolTermInfo
p, Map String String
m1)
prettifyTypeVarsTm (Comb tm1 :: Term
tm1 tm2 :: Term
tm2) m :: Map String String
m =
 let (tm1' :: Term
tm1', m1 :: Map String String
m1) = Term -> Map String String -> (Term, Map String String)
prettifyTypeVarsTm Term
tm1 Map String String
m
     (tm2' :: Term
tm2', m2 :: Map String String
m2) = Term -> Map String String -> (Term, Map String String)
prettifyTypeVarsTm Term
tm2 Map String String
m1
 in (Term -> Term -> Term
Comb Term
tm1' Term
tm2', Map String String
m2)
prettifyTypeVarsTm (Abs tm1 :: Term
tm1 tm2 :: Term
tm2) m :: Map String String
m =
 let (tm1' :: Term
tm1', m1 :: Map String String
m1) = Term -> Map String String -> (Term, Map String String)
prettifyTypeVarsTm Term
tm1 Map String String
m
     (tm2' :: Term
tm2', m2 :: Map String String
m2) = Term -> Map String String -> (Term, Map String String)
prettifyTypeVarsTm Term
tm2 Map String String
m1
 in (Term -> Term -> Term
Abs Term
tm1' Term
tm2', Map String String
m2)
prettifyTypeVarsTm t :: Term
t m :: Map String String
m = (Term
t, Map String String
m)

prettifyTypeVars :: ([(String, [(String, Term)])], [(String, String)]) ->
                    ([(String, [(String, Term)])], [(String, String)])
prettifyTypeVars :: ([(String, [(String, Term)])], [(String, String)])
-> ([(String, [(String, Term)])], [(String, String)])
prettifyTypeVars (libs :: [(String, [(String, Term)])]
libs, lnks :: [(String, String)]
lnks) =
 let libs' :: [(String, [(String, Term)])]
libs' = ((String, [(String, Term)]) -> (String, [(String, Term)]))
-> [(String, [(String, Term)])] -> [(String, [(String, Term)])]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: String
s, terms :: [(String, Term)]
terms) ->
      let terms' :: [(String, Term)]
terms' = ([(String, Term)] -> (String, Term) -> [(String, Term)])
-> [(String, Term)] -> [(String, Term)] -> [(String, Term)]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ tms :: [(String, Term)]
tms (ts :: String
ts, t :: Term
t) ->
            let (t' :: Term
t', _) = Term -> Map String String -> (Term, Map String String)
prettifyTypeVarsTm Term
t Map String String
forall k a. Map k a
Map.empty
            in ((String
ts, Term
t') (String, Term) -> [(String, Term)] -> [(String, Term)]
forall a. a -> [a] -> [a]
: [(String, Term)]
tms))
             [] [(String, Term)]
terms
      in (String
s, [(String, Term)]
terms')
      ) [(String, [(String, Term)])]
libs
 in ([(String, [(String, Term)])]
libs', [(String, String)]
lnks)

treeLevels :: [(String, String)] -> Map.Map Int [(String, String)]
treeLevels :: [(String, String)] -> Map Int [(String, String)]
treeLevels l :: [(String, String)]
l =
 let lk :: [(String, (Int, String))]
lk = ((String, String)
 -> [(String, (Int, String))] -> [(String, (Int, String))])
-> [(String, (Int, String))]
-> [(String, String)]
-> [(String, (Int, String))]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (imp :: String
imp, t :: String
t) l' :: [(String, (Int, String))]
l' ->
      case String -> [(String, (Int, String))] -> Maybe (Int, String)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
t [(String, (Int, String))]
l' of
       Just (p :: Int
p, _) -> (String
imp, (Int
p Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1, String
t)) (String, (Int, String))
-> [(String, (Int, String))] -> [(String, (Int, String))]
forall a. a -> [a] -> [a]
: [(String, (Int, String))]
l'
       Nothing -> (String
imp, (1, String
t)) (String, (Int, String))
-> [(String, (Int, String))] -> [(String, (Int, String))]
forall a. a -> [a] -> [a]
: (String
t, (0, "")) (String, (Int, String))
-> [(String, (Int, String))] -> [(String, (Int, String))]
forall a. a -> [a] -> [a]
: [(String, (Int, String))]
l') [] [(String, String)]
l
 in (Map Int [(String, String)]
 -> (String, (Int, String)) -> Map Int [(String, String)])
-> Map Int [(String, String)]
-> [(String, (Int, String))]
-> Map Int [(String, String)]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ m :: Map Int [(String, String)]
m (imp :: String
imp, (p :: Int
p, t :: String
t)) ->
  let s :: [(String, String)]
s = [(String, String)]
-> Int -> Map Int [(String, String)] -> [(String, String)]
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault [] Int
p Map Int [(String, String)]
m
  in Int
-> [(String, String)]
-> Map Int [(String, String)]
-> Map Int [(String, String)]
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Int
p ((String
imp, String
t) (String, String) -> [(String, String)] -> [(String, String)]
forall a. a -> [a] -> [a]
: [(String, String)]
s) Map Int [(String, String)]
m) Map Int [(String, String)]
forall k a. Map k a
Map.empty [(String, (Int, String))]
lk

makeNamedSentence :: String -> Term -> Named Sentence
makeNamedSentence :: String -> Term -> Named Sentence
makeNamedSentence n :: String
n t :: Term
t = String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed String
n Sentence :: Term -> Maybe HolProof -> Sentence
Sentence { term :: Term
term = Term
t, proof :: Maybe HolProof
proof = Maybe HolProof
forall a. Maybe a
Nothing }

_insNodeDG :: Sign -> [Named Sentence] -> FilePath -> String
              -> (DGraph, Map.Map String
               (String, Data.Graph.Inductive.Graph.Node, DGNodeLab))
              -> (DGraph, Map.Map String
               (String, Data.Graph.Inductive.Graph.Node, DGNodeLab))
_insNodeDG :: Sign
-> [Named Sentence]
-> String
-> String
-> (DGraph, Map String (String, Int, DGNodeLab))
-> (DGraph, Map String (String, Int, DGNodeLab))
_insNodeDG sig :: Sign
sig sens :: [Named Sentence]
sens path :: String
path n :: String
n (dg :: DGraph
dg, m :: Map String (String, Int, DGNodeLab)
m) =
 let gt :: G_theory
gt = HolLight
-> Maybe IRI
-> ExtSign Sign ()
-> SigId
-> ThSens Sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
G_theory HolLight
HolLight Maybe IRI
forall a. Maybe a
Nothing (HolLight -> Sign -> ExtSign Sign ()
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sign -> ExtSign sign symbol
makeExtSign HolLight
HolLight Sign
sig) SigId
startSigId
           ([Named Sentence] -> ThSens Sentence (AnyComorphism, BasicProof)
forall a b. Ord a => [Named a] -> ThSens a b
toThSens [Named Sentence]
sens) ThId
startThId
     n' :: String
n' = (String, String) -> String
forall a b. (a, b) -> b
snd (String -> (String, String)
System.FilePath.splitFileName String
n)
     labelK :: DGNodeLab
labelK = NodeName -> DGNodeInfo -> G_theory -> DGNodeLab
newInfoNodeLab
      (IRI -> NodeName
makeName (SIMPLE_ID -> IRI
simpleIdToIRI (SIMPLE_ID -> IRI) -> SIMPLE_ID -> IRI
forall a b. (a -> b) -> a -> b
$ String -> SIMPLE_ID
mkSimpleId String
n'))
      (DGOrigin -> DGNodeInfo
newNodeInfo DGOrigin
DGEmpty)
      G_theory
gt
     k :: Int
k = DGraph -> Int
getNewNodeDG DGraph
dg
     m' :: Map String (String, Int, DGNodeLab)
m' = String
-> (String, Int, DGNodeLab)
-> Map String (String, Int, DGNodeLab)
-> Map String (String, Int, DGNodeLab)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
n (String
n, Int
k, DGNodeLab
labelK) Map String (String, Int, DGNodeLab)
m
     insN :: [DGChange]
insN = [LNode DGNodeLab -> DGChange
InsertNode (Int
k, DGNodeLab
labelK)]
     newDG :: DGraph
newDG = DGraph -> [DGChange] -> DGraph
changesDGH DGraph
dg [DGChange]
insN
     labCh :: [DGChange]
labCh = [DGNodeLab -> LNode DGNodeLab -> DGChange
SetNodeLab DGNodeLab
labelK (Int
k, DGNodeLab
labelK
      { globalTheory :: Maybe G_theory
globalTheory = LibEnv -> LibName -> DGraph -> LNode DGNodeLab -> Maybe G_theory
computeLabelTheory LibEnv
forall k a. Map k a
Map.empty (String -> LibName
emptyLibName
            (String -> String
System.FilePath.takeBaseName String
path)) DGraph
newDG
        (Int
k, DGNodeLab
labelK) })]
     newDG1 :: DGraph
newDG1 = DGraph -> [DGChange] -> DGraph
changesDGH DGraph
newDG [DGChange]
labCh in (DGraph
newDG1, Map String (String, Int, DGNodeLab)
m')

anaHolLightFile :: HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
anaHolLightFile :: HetcatsOpts -> String -> IO (Maybe (LibName, LibEnv))
anaHolLightFile opts :: HetcatsOpts
opts path :: String
path = do
 (libs_ :: [(String, [(String, Term)])]
libs_, lnks_ :: [(String, String)]
lnks_) <- HetcatsOpts
-> String -> IO ([(String, [(String, Term)])], [(String, String)])
importData HetcatsOpts
opts String
path
 let (libs :: [(String, [(String, Term)])]
libs, lnks :: [(String, String)]
lnks) = ([(String, [(String, Term)])], [(String, String)])
-> ([(String, [(String, Term)])], [(String, String)])
prettifyTypeVars ([(String, [(String, Term)])]
libs_, [(String, String)]
lnks_)
 let h :: Map Int [(String, String)]
h = [(String, String)] -> Map Int [(String, String)]
treeLevels [(String, String)]
lnks
 let fixLinks :: Map b Sign -> [(b, b)] -> [(b, b)]
fixLinks m :: Map b Sign
m l :: [(b, b)]
l =
      case [(b, b)]
l of
       (l1 :: (b, b)
l1 : l2 :: (b, b)
l2 : l' :: [(b, b)]
l') ->
        if (b, b) -> b
forall a b. (a, b) -> b
snd (b, b)
l1 b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== (b, b) -> b
forall a b. (a, b) -> b
snd (b, b)
l2 Bool -> Bool -> Bool
&& Sign -> Sign -> Bool
sigDepends
         (Sign -> b -> Map b Sign -> Sign
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Sign
emptySig ((b, b) -> b
forall a b. (a, b) -> a
fst (b, b)
l1) Map b Sign
m)
         (Sign -> b -> Map b Sign -> Sign
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Sign
emptySig ((b, b) -> b
forall a b. (a, b) -> a
fst (b, b)
l2) Map b Sign
m) then
          ((b, b) -> b
forall a b. (a, b) -> a
fst (b, b)
l1, (b, b) -> b
forall a b. (a, b) -> a
fst (b, b)
l2) (b, b) -> [(b, b)] -> [(b, b)]
forall a. a -> [a] -> [a]
: Map b Sign -> [(b, b)] -> [(b, b)]
fixLinks Map b Sign
m ((b, b)
l2 (b, b) -> [(b, b)] -> [(b, b)]
forall a. a -> [a] -> [a]
: [(b, b)]
l')
        else (b, b)
l1 (b, b) -> [(b, b)] -> [(b, b)]
forall a. a -> [a] -> [a]
: (b, b)
l2 (b, b) -> [(b, b)] -> [(b, b)]
forall a. a -> [a] -> [a]
: Map b Sign -> [(b, b)] -> [(b, b)]
fixLinks Map b Sign
m [(b, b)]
l'
       l' :: [(b, b)]
l' -> [(b, b)]
l'
 let uniteSigs :: Map String Sign -> [(String, String)] -> Map String Sign
uniteSigs = (Map String Sign -> (String, String) -> Map String Sign)
-> Map String Sign -> [(String, String)] -> Map String Sign
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ m' :: Map String Sign
m' (s :: String
s, t :: String
t) ->
                  case Result Sign -> Maybe Sign
forall a. Result a -> Maybe a
resultToMaybe
                    (Sign -> Sign -> Result Sign
sigUnion (Sign -> String -> Map String Sign -> Sign
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Sign
emptySig String
s Map String Sign
m')
                    (Sign -> String -> Map String Sign -> Sign
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Sign
emptySig String
t Map String Sign
m')) of
                   Nothing -> Map String Sign
m'
                   Just new_tsig :: Sign
new_tsig -> String -> Sign -> Map String Sign -> Map String Sign
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
t Sign
new_tsig Map String Sign
m')
 let m :: Map String Sign
m = (Map String Sign -> (String, [(String, Term)]) -> Map String Sign)
-> Map String Sign
-> [(String, [(String, Term)])]
-> Map String Sign
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ m' :: Map String Sign
m' (s :: String
s, l :: [(String, Term)]
l) -> String -> Sign -> Map String Sign -> Map String Sign
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
s ([(String, Term)] -> Sign
calcSig [(String, Term)]
l) Map String Sign
m') Map String Sign
forall k a. Map k a
Map.empty [(String, [(String, Term)])]
libs
 let (m' :: Map String Sign
m', lnks' :: [(String, String)]
lnks') = (Int
 -> (Map String Sign, [(String, String)])
 -> (Map String Sign, [(String, String)]))
-> (Map String Sign, [(String, String)])
-> [Int]
-> (Map String Sign, [(String, String)])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ lvl :: Int
lvl (m'' :: Map String Sign
m'', lnks_loc :: [(String, String)]
lnks_loc) ->
                    let lvl' :: [(String, String)]
lvl' = [(String, String)]
-> Int -> Map Int [(String, String)] -> [(String, String)]
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault [] Int
lvl Map Int [(String, String)]
h
                        lnks_next :: [(String, String)]
lnks_next = Map String Sign -> [(String, String)] -> [(String, String)]
forall b. Ord b => Map b Sign -> [(b, b)] -> [(b, b)]
fixLinks Map String Sign
m'' ([(String, String)] -> [(String, String)]
forall a. [a] -> [a]
reverse [(String, String)]
lvl')
{- we'd probably need to take care of dependencies on previously
imported files not imported by the file imported last -}
                    in (Map String Sign -> [(String, String)] -> Map String Sign
uniteSigs Map String Sign
m'' [(String, String)]
lnks_next, [(String, String)]
lnks_next [(String, String)] -> [(String, String)] -> [(String, String)]
forall a. [a] -> [a] -> [a]
++ [(String, String)]
lnks_loc)
                   ) (Map String Sign
m, []) [0 .. (Map Int [(String, String)] -> Int
forall k a. Map k a -> Int
Map.size Map Int [(String, String)]
h Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1)]
 let (dg' :: DGraph
dg', node_m :: Map String (String, Int, DGNodeLab)
node_m) = ((String, [(String, Term)])
 -> (DGraph, Map String (String, Int, DGNodeLab))
 -> (DGraph, Map String (String, Int, DGNodeLab)))
-> (DGraph, Map String (String, Int, DGNodeLab))
-> [(String, [(String, Term)])]
-> (DGraph, Map String (String, Int, DGNodeLab))
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (lname :: String
lname, lterms :: [(String, Term)]
lterms) (dg :: DGraph
dg, node_m' :: Map String (String, Int, DGNodeLab)
node_m') ->
           let sig :: Sign
sig = Sign -> String -> Map String Sign -> Sign
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Sign
emptySig String
lname Map String Sign
m'
               sens :: [Named Sentence]
sens = ((String, Term) -> Named Sentence)
-> [(String, Term)] -> [Named Sentence]
forall a b. (a -> b) -> [a] -> [b]
map ((String -> Term -> Named Sentence)
-> (String, Term) -> Named Sentence
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry String -> Term -> Named Sentence
makeNamedSentence) [(String, Term)]
lterms in
           Sign
-> [Named Sentence]
-> String
-> String
-> (DGraph, Map String (String, Int, DGNodeLab))
-> (DGraph, Map String (String, Int, DGNodeLab))
_insNodeDG Sign
sig [Named Sentence]
sens String
path String
lname (DGraph
dg, Map String (String, Int, DGNodeLab)
node_m')) (DGraph
emptyDG, Map String (String, Int, DGNodeLab)
forall k a. Map k a
Map.empty) [(String, [(String, Term)])]
libs
     dg'' :: DGraph
dg'' = ((String, String) -> DGraph -> DGraph)
-> DGraph -> [(String, String)] -> DGraph
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (source :: String
source, target :: String
target) dg :: DGraph
dg ->
      case String
-> Map String (String, Int, DGNodeLab)
-> Maybe (String, Int, DGNodeLab)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
source Map String (String, Int, DGNodeLab)
node_m of
       Just (n :: String
n, k :: Int
k, _) ->
        case String
-> Map String (String, Int, DGNodeLab)
-> Maybe (String, Int, DGNodeLab)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
target Map String (String, Int, DGNodeLab)
node_m of
         Just (n1 :: String
n1, k1 :: Int
k1, _) ->
          let sig :: Sign
sig = Sign -> String -> Map String Sign -> Sign
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Sign
emptySig String
n Map String Sign
m'
              sig1 :: Sign
sig1 = Sign -> String -> Map String Sign -> Sign
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Sign
emptySig String
n1 Map String Sign
m'
          in case Result HolLightMorphism -> Maybe HolLightMorphism
forall a. Result a -> Maybe a
resultToMaybe (Result HolLightMorphism -> Maybe HolLightMorphism)
-> Result HolLightMorphism -> Maybe HolLightMorphism
forall a b. (a -> b) -> a -> b
$
               HolLight -> Sign -> Sign -> Result HolLightMorphism
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign -> sign -> Result morphism
subsig_inclusion HolLight
HolLight Sign
sig Sign
sig1 of
              Nothing -> DGraph
dg
              Just incl :: HolLightMorphism
incl ->
               let inclM :: GMorphism
inclM = G_morphism -> GMorphism
gEmbed (G_morphism -> GMorphism) -> G_morphism -> GMorphism
forall a b. (a -> b) -> a -> b
$ HolLight -> HolLightMorphism -> G_morphism
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> morphism -> G_morphism
mkG_morphism HolLight
HolLight HolLightMorphism
incl
                   insE :: [DGChange]
insE = [LEdge DGLinkLab -> DGChange
InsertEdge (Int
k, Int
k1, GMorphism -> DGLinkOrigin -> DGLinkLab
globDefLink GMorphism
inclM DGLinkOrigin
DGLinkImports)]
               in DGraph -> [DGChange] -> DGraph
changesDGH DGraph
dg [DGChange]
insE
         Nothing -> DGraph
dg
       Nothing -> DGraph
dg) DGraph
dg' [(String, String)]
lnks'
     le :: LibEnv
le = LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (String -> LibName
emptyLibName
            (String -> String
System.FilePath.takeBaseName String
path))
           DGraph
dg'' LibEnv
forall k a. Map k a
Map.empty
 Maybe (LibName, LibEnv) -> IO (Maybe (LibName, LibEnv))
forall (m :: * -> *) a. Monad m => a -> m a
return ((LibName, LibEnv) -> Maybe (LibName, LibEnv)
forall a. a -> Maybe a
Just (String -> LibName
emptyLibName
  (String -> String
System.FilePath.takeBaseName String
path),
  LibEnv -> LibEnv
computeLibEnvTheories LibEnv
le))