{- |
Module      :  ./LF/Analysis.hs
Description :  Static analysis for the Edinburgh Logical Framework
Copyright   :  (c) Kristina Sojakova, DFKI Bremen 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  k.sojakova@jacobs-university.de
Stability   :  experimental
Portability :  portable
-}
module LF.Analysis where

import LF.AS
import LF.Sign
import LF.Twelf2GR

import Common.ExtSign
import Common.GlobalAnnotations
import Common.AS_Annotation
import Common.Result
import Common.DocUtils

import Data.List
import qualified Data.Map as Map
import qualified Data.Set as Set

import System.IO.Unsafe

sen_type_exp :: EXP
sen_type_exp :: EXP
sen_type_exp = EXP
Type

gen_file :: String
gen_file :: String
gen_file = String
gen_base

gen_sig1 :: String
gen_sig1 :: String
gen_sig1 = String
gen_module

gen_sig2 :: String
gen_sig2 :: String
gen_sig2 = String
gen_module String -> String -> String
forall a. [a] -> [a] -> [a]
++ "'"

gen :: String
gen :: String
gen = "gen_"

genPref :: String -> String
genPref :: String -> String
genPref s :: String
s = String
gen String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s

gen_ax :: String
gen_ax :: String
gen_ax = String -> String
genPref "ax"

numSuf :: String -> Int -> String
numSuf :: String -> Int -> String
numSuf s :: String
s i :: Int
i = String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i

mkSig :: String -> String -> String
mkSig :: String -> String -> String
mkSig n :: String
n cont :: String
cont = "%sig " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ " = {\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cont String -> String -> String
forall a. [a] -> [a] -> [a]
++ "}.\n"

mkIncl :: String -> String
mkIncl :: String -> String
mkIncl n :: String
n = "%include " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ " %open.\n"

mkRead :: String -> String
mkRead :: String -> String
mkRead n :: String
n = "%read \"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\".\n"

getSigItems :: [Annoted BASIC_ITEM] -> [Annoted BASIC_ITEM]
getSigItems :: [Annoted BASIC_ITEM] -> [Annoted BASIC_ITEM]
getSigItems = (Annoted BASIC_ITEM -> Bool)
-> [Annoted BASIC_ITEM] -> [Annoted BASIC_ITEM]
forall a. (a -> Bool) -> [a] -> [a]
filter ( \ (Annoted i :: BASIC_ITEM
i _ _ _) ->
  case BASIC_ITEM
i of
    Decl _ -> Bool
True
    Form _ -> Bool
False )

getSenItems :: [Annoted BASIC_ITEM] -> [Annoted BASIC_ITEM]
getSenItems :: [Annoted BASIC_ITEM] -> [Annoted BASIC_ITEM]
getSenItems = (Annoted BASIC_ITEM -> Bool)
-> [Annoted BASIC_ITEM] -> [Annoted BASIC_ITEM]
forall a. (a -> Bool) -> [a] -> [a]
filter ( \ (Annoted i :: BASIC_ITEM
i _ _ _) ->
  case BASIC_ITEM
i of
    Decl _ -> Bool
False
    Form _ -> Bool
True )

printSigItems :: [Annoted BASIC_ITEM] -> String
printSigItems :: [Annoted BASIC_ITEM] -> String
printSigItems =
  (Annoted BASIC_ITEM -> String) -> [Annoted BASIC_ITEM] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (Annoted i :: BASIC_ITEM
i _ _ _) ->
     case BASIC_ITEM
i of
          Decl d :: String
d -> String
d String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".\n"
          _ -> ""
     )

printSenItems :: String -> [Annoted BASIC_ITEM] -> String
printSenItems :: String -> [Annoted BASIC_ITEM] -> String
printSenItems sen_type :: String
sen_type = String -> Int -> [Annoted BASIC_ITEM] -> String
printSenItemsH String
sen_type 0

printSenItemsH :: String -> Int -> [Annoted BASIC_ITEM] -> String
printSenItemsH :: String -> Int -> [Annoted BASIC_ITEM] -> String
printSenItemsH _ _ [] = ""
printSenItemsH sen_type :: String
sen_type num :: Int
num (i :: Annoted BASIC_ITEM
i : is :: [Annoted BASIC_ITEM]
is) =
  case Annoted BASIC_ITEM
i of
    Annoted (Form f :: String
f) _ _ _ ->
      let lab :: String
lab = Annoted BASIC_ITEM -> String
forall a. Annoted a -> String
getRLabel Annoted BASIC_ITEM
i
          lab' :: String
lab' = if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
lab then String -> Int -> String
numSuf String
gen_ax Int
num else String
lab
          num' :: Int
num' = if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
lab then Int
num Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 else Int
num
          in String
lab' String -> String -> String
forall a. [a] -> [a] -> [a]
++ " : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sen_type String -> String -> String
forall a. [a] -> [a] -> [a]
++ " = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
             String -> Int -> [Annoted BASIC_ITEM] -> String
printSenItemsH String
sen_type Int
num' [Annoted BASIC_ITEM]
is
    _ -> String -> Int -> [Annoted BASIC_ITEM] -> String
printSenItemsH String
sen_type Int
num [Annoted BASIC_ITEM]
is

makeNamedForms :: [(NAME, Sentence)] -> [[Annotation]] -> [Named Sentence]
makeNamedForms :: [(String, EXP)] -> [[Annotation]] -> [Named EXP]
makeNamedForms = ((String, EXP) -> [Annotation] -> Named EXP)
-> [(String, EXP)] -> [[Annotation]] -> [Named EXP]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith ((((String, EXP), [Annotation]) -> Named EXP)
-> (String, EXP) -> [Annotation] -> Named EXP
forall a b c. ((a, b) -> c) -> a -> b -> c
curry ((String, EXP), [Annotation]) -> Named EXP
makeNamedForm)

makeNamedForm :: ((NAME, Sentence), [Annotation]) -> Named Sentence
makeNamedForm :: ((String, EXP), [Annotation]) -> Named EXP
makeNamedForm ((n :: String
n, s :: EXP
s), annos :: [Annotation]
annos) =
  let implies :: Bool
implies = (Annotation -> Bool) -> [Annotation] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Annotation -> Bool
isImplies [Annotation]
annos
      implied :: Bool
implied = (Annotation -> Bool) -> [Annotation] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Annotation -> Bool
isImplied [Annotation]
annos
      isTheorem :: Bool
isTheorem = Bool
implies Bool -> Bool -> Bool
|| Bool
implied
      in (String -> EXP -> Named EXP
forall a s. a -> s -> SenAttr s a
makeNamed String
n EXP
s) {isAxiom :: Bool
isAxiom = Bool -> Bool
not Bool
isTheorem}

getSigFromLibs :: MODULE -> LIBS -> IO Sign
getSigFromLibs :: String -> LIBS -> IO Sign
getSigFromLibs n :: String
n libs :: LIBS
libs = do
  String
lname <- Namespace -> String -> IO String
toLibName Namespace
HETS String
gen_file
  let (sigs :: SIGS
sigs, _) = (SIGS, MORPHS) -> String -> LIBS -> (SIGS, MORPHS)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> (SIGS, MORPHS)
forall a. HasCallStack => String -> a
error String
badLibError) String
lname LIBS
libs
  Sign -> IO Sign
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign -> IO Sign) -> Sign -> IO Sign
forall a b. (a -> b) -> a -> b
$ Sign -> String -> SIGS -> Sign
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Sign
forall a. HasCallStack => String -> a
error (String -> Sign) -> String -> Sign
forall a b. (a -> b) -> a -> b
$ String -> String
badSigError String
n) String
n SIGS
sigs

getUnknownSyms :: [RAW_SYM] -> Sign -> [RAW_SYM]
getUnknownSyms :: [String] -> Sign -> [String]
getUnknownSyms syms :: [String]
syms sig :: Sign
sig =
  [String]
syms [String] -> [String] -> [String]
forall a. Eq a => [a] -> [a] -> [a]
\\ Set String -> [String]
forall a. Set a -> [a]
Set.toList ((Symbol -> String) -> Set Symbol -> Set String
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Symbol -> String
symName (Set Symbol -> Set String) -> Set Symbol -> Set String
forall a b. (a -> b) -> a -> b
$ Sign -> Set Symbol
getLocalSyms Sign
sig)

{- ---------------------------------------------------------------
--------------------------------------------------------------- -}

-- basic analysis for LF
basicAnalysis :: (BASIC_SPEC, Sign, GlobalAnnos) ->
                 Result (BASIC_SPEC, ExtSign Sign Symbol, [Named EXP])
basicAnalysis :: (BASIC_SPEC, Sign, GlobalAnnos)
-> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named EXP])
basicAnalysis (bs :: BASIC_SPEC
bs@(Basic_spec items :: [Annoted BASIC_ITEM]
items), initsig :: Sign
initsig, _) = do
  let (sig :: Sign
sig, sens :: [(String, EXP)]
sens) = IO (Sign, [(String, EXP)]) -> (Sign, [(String, EXP)])
forall a. IO a -> a
unsafePerformIO (IO (Sign, [(String, EXP)]) -> (Sign, [(String, EXP)]))
-> IO (Sign, [(String, EXP)]) -> (Sign, [(String, EXP)])
forall a b. (a -> b) -> a -> b
$ Sign -> [Annoted BASIC_ITEM] -> IO (Sign, [(String, EXP)])
makeSigSen Sign
initsig [Annoted BASIC_ITEM]
items
  let syms :: Set Symbol
syms = Sign -> Set Symbol
getSymbols Sign
sig
  let fs :: [Named EXP]
fs = [(String, EXP)] -> [[Annotation]] -> [Named EXP]
makeNamedForms [(String, EXP)]
sens ([[Annotation]] -> [Named EXP]) -> [[Annotation]] -> [Named EXP]
forall a b. (a -> b) -> a -> b
$ (Annoted BASIC_ITEM -> [Annotation])
-> [Annoted BASIC_ITEM] -> [[Annotation]]
forall a b. (a -> b) -> [a] -> [b]
map Annoted BASIC_ITEM -> [Annotation]
forall a. Annoted a -> [Annotation]
r_annos ([Annoted BASIC_ITEM] -> [[Annotation]])
-> [Annoted BASIC_ITEM] -> [[Annotation]]
forall a b. (a -> b) -> a -> b
$ [Annoted BASIC_ITEM] -> [Annoted BASIC_ITEM]
getSenItems [Annoted BASIC_ITEM]
items
  (BASIC_SPEC, ExtSign Sign Symbol, [Named EXP])
-> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named EXP])
forall (m :: * -> *) a. Monad m => a -> m a
return (BASIC_SPEC
bs, Sign -> Set Symbol -> ExtSign Sign Symbol
forall sign symbol. sign -> Set symbol -> ExtSign sign symbol
ExtSign Sign
sig Set Symbol
syms, [Named EXP]
fs)

-- constructs the signatures and sentences
makeSigSen :: Sign -> [Annoted BASIC_ITEM] -> IO (Sign, [(NAME, Sentence)])
makeSigSen :: Sign -> [Annoted BASIC_ITEM] -> IO (Sign, [(String, EXP)])
makeSigSen sig :: Sign
sig items :: [Annoted BASIC_ITEM]
items = do
  -- make a Twelf file
  let sen_type :: String
sen_type = Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ EXP -> Doc
forall a. Pretty a => a -> Doc
pretty EXP
sen_type_exp
  let cont1 :: String
cont1 = if [DEF] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Sign -> [DEF]
getDefs Sign
sig) then "" else Doc -> String
forall a. Show a => a -> String
show (Sign -> Doc
forall a. Pretty a => a -> Doc
pretty Sign
sig) String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n"
  let cont2 :: String
cont2 = [Annoted BASIC_ITEM] -> String
printSigItems ([Annoted BASIC_ITEM] -> String) -> [Annoted BASIC_ITEM] -> String
forall a b. (a -> b) -> a -> b
$ [Annoted BASIC_ITEM] -> [Annoted BASIC_ITEM]
getSigItems [Annoted BASIC_ITEM]
items
  let cont3 :: String
cont3 = String -> [Annoted BASIC_ITEM] -> String
printSenItems String
sen_type ([Annoted BASIC_ITEM] -> String) -> [Annoted BASIC_ITEM] -> String
forall a b. (a -> b) -> a -> b
$ [Annoted BASIC_ITEM] -> [Annoted BASIC_ITEM]
getSenItems [Annoted BASIC_ITEM]
items
  let s1 :: String
s1 = String -> String -> String
mkSig String
gen_sig1 (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
cont1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cont2
  let s2 :: String
s2 = String -> String -> String
mkSig String
gen_sig2 (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String
mkIncl String
gen_sig1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cont3
  let contents :: String
contents = String
s1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s2
  String -> String -> IO ()
writeFile String
gen_file String
contents

  -- run Twelf on the created file
  LIBS
libs <- Namespace -> String -> IO LIBS
twelf2SigMor Namespace
HETS String
gen_file

  -- construct the signature and sentences
  Sign
sig1 <- String -> LIBS -> IO Sign
getSigFromLibs String
gen_sig1 LIBS
libs
  Sign
sig2 <- String -> LIBS -> IO Sign
getSigFromLibs String
gen_sig2 LIBS
libs
  let sens :: [(String, EXP)]
sens = Sign -> [(String, EXP)]
getSens Sign
sig2
  (Sign, [(String, EXP)]) -> IO (Sign, [(String, EXP)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign
sig1, [(String, EXP)]
sens)

getSens :: Sign -> [(NAME, Sentence)]
getSens :: Sign -> [(String, EXP)]
getSens sig :: Sign
sig =
  (DEF -> (String, EXP)) -> [DEF] -> [(String, EXP)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Def s :: Symbol
s _ v :: Maybe EXP
v) ->
         case Maybe EXP
v of
           Nothing -> String -> (String, EXP)
forall a. HasCallStack => String -> a
error (String -> (String, EXP)) -> String -> (String, EXP)
forall a b. (a -> b) -> a -> b
$ String -> String
badValError (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ Symbol -> String
symName Symbol
s
           Just v' :: EXP
v' -> (Symbol -> String
symName Symbol
s, EXP
v')
      ) ([DEF] -> [(String, EXP)]) -> [DEF] -> [(String, EXP)]
forall a b. (a -> b) -> a -> b
$ Sign -> [DEF]
getLocalDefs Sign
sig

{- ---------------------------------------------------------------
--------------------------------------------------------------- -}

-- symbol analysis for LF
symbAnalysis :: [SYMB_ITEMS] -> Result [RAW_SYM]
symbAnalysis :: [SYMB_ITEMS] -> Result [String]
symbAnalysis ss :: [SYMB_ITEMS]
ss = [Diagnosis] -> Maybe [String] -> Result [String]
forall a. [Diagnosis] -> Maybe a -> Result a
Result [] (Maybe [String] -> Result [String])
-> Maybe [String] -> Result [String]
forall a b. (a -> b) -> a -> b
$ [String] -> Maybe [String]
forall a. a -> Maybe a
Just ([String] -> Maybe [String]) -> [String] -> Maybe [String]
forall a b. (a -> b) -> a -> b
$ (SYMB_ITEMS -> [String]) -> [SYMB_ITEMS] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (Symb_items s :: [String]
s) -> [String]
s) [SYMB_ITEMS]
ss

-- symbol map analysis for LF
symbMapAnalysis :: [SYMB_MAP_ITEMS] -> Result (Map.Map RAW_SYM RAW_SYM)
symbMapAnalysis :: [SYMB_MAP_ITEMS] -> Result (Map String String)
symbMapAnalysis ss :: [SYMB_MAP_ITEMS]
ss = [Diagnosis]
-> Maybe (Map String String) -> Result (Map String String)
forall a. [Diagnosis] -> Maybe a -> Result a
Result [] (Maybe (Map String String) -> Result (Map String String))
-> Maybe (Map String String) -> Result (Map String String)
forall a b. (a -> b) -> a -> b
$ Map String String -> Maybe (Map String String)
forall a. a -> Maybe a
Just (Map String String -> Maybe (Map String String))
-> Map String String -> Maybe (Map String String)
forall a b. (a -> b) -> a -> b
$
  (Map String String -> SYMB_MAP_ITEMS -> Map String String)
-> Map String String -> [SYMB_MAP_ITEMS] -> Map String String
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ m :: Map String String
m s :: SYMB_MAP_ITEMS
s -> Map String String -> Map String String -> Map String String
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map String String
m (SYMB_MAP_ITEMS -> Map String String
makeSymbMap SYMB_MAP_ITEMS
s)) Map String String
forall k a. Map k a
Map.empty [SYMB_MAP_ITEMS]
ss

makeSymbMap :: SYMB_MAP_ITEMS -> Map.Map RAW_SYM RAW_SYM
makeSymbMap :: SYMB_MAP_ITEMS -> Map String String
makeSymbMap (Symb_map_items ss :: [SYMB_OR_MAP]
ss) =
   (Map String String -> SYMB_OR_MAP -> Map String String)
-> Map String String -> [SYMB_OR_MAP] -> Map String String
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ m :: Map String String
m s :: SYMB_OR_MAP
s -> case SYMB_OR_MAP
s of
                     Symb s1 :: String
s1 -> String -> String -> Map String String -> Map String String
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
s1 String
s1 Map String String
m
                     Symb_map s1 :: String
s1 s2 :: String
s2 -> String -> String -> Map String String -> Map String String
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
s1 String
s2 Map String String
m
         ) Map String String
forall k a. Map k a
Map.empty [SYMB_OR_MAP]
ss

{- ---------------------------------------------------------------
--------------------------------------------------------------- -}

-- converts a mapping of raw symbols to a mapping of symbols
renamMapAnalysis :: Map.Map RAW_SYM RAW_SYM -> Sign -> Map.Map Symbol Symbol
renamMapAnalysis :: Map String String -> Sign -> Map Symbol Symbol
renamMapAnalysis m :: Map String String
m sig :: Sign
sig =
  let syms1 :: [String]
syms1 = [String] -> Sign -> [String]
getUnknownSyms (Map String String -> [String]
forall k a. Map k a -> [k]
Map.keys Map String String
m) Sign
sig
      syms2 :: [String]
syms2 = (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (String -> Bool) -> String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Bool
isSym) ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ Map String String -> [String]
forall k a. Map k a -> [a]
Map.elems Map String String
m
      syms :: [String]
syms = [String]
syms1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
syms2
      in if Bool -> Bool
not ([String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
syms) then String -> Map Symbol Symbol
forall a. HasCallStack => String -> a
error (String -> Map Symbol Symbol) -> String -> Map Symbol Symbol
forall a b. (a -> b) -> a -> b
$ [String] -> String
badSymsError [String]
syms else
            [(Symbol, Symbol)] -> Map Symbol Symbol
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Symbol, Symbol)] -> Map Symbol Symbol)
-> [(Symbol, Symbol)] -> Map Symbol Symbol
forall a b. (a -> b) -> a -> b
$ ((String, String) -> (Symbol, Symbol))
-> [(String, String)] -> [(Symbol, Symbol)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (k :: String
k, v :: String
v) -> (String -> Symbol
toSym String
k, String -> Symbol
toSym String
v)) ([(String, String)] -> [(Symbol, Symbol)])
-> [(String, String)] -> [(Symbol, Symbol)]
forall a b. (a -> b) -> a -> b
$ Map String String -> [(String, String)]
forall k a. Map k a -> [(k, a)]
Map.toList Map String String
m

{- converts a mapping of raw symbols to a mapping of symbols to expressions
   annotated with their type -}
translMapAnalysis :: Map.Map RAW_SYM RAW_SYM -> Sign -> Sign ->
                     Map.Map Symbol (EXP, EXP)
translMapAnalysis :: Map String String -> Sign -> Sign -> Map Symbol (EXP, EXP)
translMapAnalysis m :: Map String String
m sig1 :: Sign
sig1 sig2 :: Sign
sig2 =
  let syms :: [String]
syms = [String] -> Sign -> [String]
getUnknownSyms (Map String String -> [String]
forall k a. Map k a -> [k]
Map.keys Map String String
m) Sign
sig1
      in if Bool -> Bool
not ([String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
syms) then String -> Map Symbol (EXP, EXP)
forall a. HasCallStack => String -> a
error (String -> Map Symbol (EXP, EXP))
-> String -> Map Symbol (EXP, EXP)
forall a b. (a -> b) -> a -> b
$ [String] -> String
badSymsError [String]
syms else
         IO (Map Symbol (EXP, EXP)) -> Map Symbol (EXP, EXP)
forall a. IO a -> a
unsafePerformIO (IO (Map Symbol (EXP, EXP)) -> Map Symbol (EXP, EXP))
-> IO (Map Symbol (EXP, EXP)) -> Map Symbol (EXP, EXP)
forall a b. (a -> b) -> a -> b
$ Map String String -> Sign -> IO (Map Symbol (EXP, EXP))
codAnalysis Map String String
m Sign
sig2

codAnalysis :: Map.Map RAW_SYM RAW_SYM -> Sign -> IO (Map.Map Symbol (EXP, EXP))
codAnalysis :: Map String String -> Sign -> IO (Map Symbol (EXP, EXP))
codAnalysis m :: Map String String
m sig2 :: Sign
sig2 = do
  -- make a Twelf file
  let cont1 :: String
cont1 = Doc -> String
forall a. Show a => a -> String
show (Sign -> Doc
forall a. Pretty a => a -> Doc
pretty Sign
sig2) String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n"
  let cont2 :: String
cont2 = ((String, String) -> String) -> [(String, String)] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (k :: String
k, v :: String
v) -> String -> String
genPref String
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ " = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".\n") ([(String, String)] -> String) -> [(String, String)] -> String
forall a b. (a -> b) -> a -> b
$
                 Map String String -> [(String, String)]
forall k a. Map k a -> [(k, a)]
Map.toList Map String String
m
  let s1 :: String
s1 = String -> String -> String
mkSig String
gen_sig1 String
cont1
  let s2 :: String
s2 = String -> String -> String
mkSig String
gen_sig2 (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String
mkIncl String
gen_sig1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cont2
  let contents :: String
contents = String
s1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s2
  String -> String -> IO ()
writeFile String
gen_file String
contents

  -- run Twelf on the created file
  LIBS
libs <- Namespace -> String -> IO LIBS
twelf2SigMor Namespace
HETS String
gen_file

  -- construct the mapping
  Sign
sig' <- String -> LIBS -> IO Sign
getSigFromLibs String
gen_sig2 LIBS
libs
  Map Symbol (EXP, EXP) -> IO (Map Symbol (EXP, EXP))
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Symbol (EXP, EXP) -> IO (Map Symbol (EXP, EXP)))
-> Map Symbol (EXP, EXP) -> IO (Map Symbol (EXP, EXP))
forall a b. (a -> b) -> a -> b
$ Sign -> Map Symbol (EXP, EXP)
getMap Sign
sig'

getMap :: Sign -> Map.Map Symbol (EXP, EXP)
getMap :: Sign -> Map Symbol (EXP, EXP)
getMap sig :: Sign
sig = [(Symbol, (EXP, EXP))] -> Map Symbol (EXP, EXP)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Symbol, (EXP, EXP))] -> Map Symbol (EXP, EXP))
-> [(Symbol, (EXP, EXP))] -> Map Symbol (EXP, EXP)
forall a b. (a -> b) -> a -> b
$ (DEF -> (Symbol, (EXP, EXP))) -> [DEF] -> [(Symbol, (EXP, EXP))]
forall a b. (a -> b) -> [a] -> [b]
map
    (\ (Def s :: Symbol
s t :: EXP
t v :: Maybe EXP
v) ->
       case Maybe EXP
v of
         Nothing -> String -> (Symbol, (EXP, EXP))
forall a. HasCallStack => String -> a
error (String -> (Symbol, (EXP, EXP))) -> String -> (Symbol, (EXP, EXP))
forall a b. (a -> b) -> a -> b
$ String -> String
badValError (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ Symbol -> String
symName Symbol
s
         Just v' :: EXP
v' -> let Just n :: String
n = String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix String
gen (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ Symbol -> String
symName Symbol
s
                        in (String -> Symbol
toSym String
n, (EXP
v', EXP
t))
    ) ([DEF] -> [(Symbol, (EXP, EXP))])
-> [DEF] -> [(Symbol, (EXP, EXP))]
forall a b. (a -> b) -> a -> b
$ Sign -> [DEF]
getLocalDefs Sign
sig

{- -------------------------------------------------------------------------
------------------------------------------------------------------------- -}

-- ERROR MESSAGES
badLibError :: String
badLibError :: String
badLibError = "Library " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
gen_file String -> String -> String
forall a. [a] -> [a] -> [a]
++ " not found."

badSigError :: MODULE -> String
badSigError :: String -> String
badSigError n :: String
n = "Signature " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ " not found."

badSymsError :: [String] -> String
badSymsError :: [String] -> String
badSymsError ss :: [String]
ss = "Symbols " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. Show a => a -> String
show [String]
ss String -> String -> String
forall a. [a] -> [a] -> [a]
++
  " are unknown or are not locally accessible."

badValError :: String -> String
badValError :: String -> String
badValError s :: String
s = "Symbol " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ "does not have a value."