{-# LANGUAGE NoMonomorphismRestriction #-}
module SimpleEditor.Convert where

import Control.Monad(unless,foldM,ap,mplus)
import Data.List(sortBy)
import Data.Function(on)
import qualified Data.Map as Map
import Text.JSON(makeObj) --encode
import GF.Text.Pretty(render,(<+>))

import qualified Data.ByteString.UTF8 as UTF8(fromString)

import GF.Infra.Option(optionsGFO)
import GF.Infra.Ident(showIdent,ModuleName(..))
import GF.Grammar.Grammar
import GF.Grammar.Printer(ppParams,ppTerm,getAbs,TermPrintQual(..))
import GF.Grammar.Parser(runP,pModDef)
import GF.Grammar.Lexer(Posn(..))
import GF.Data.ErrM
import PGF.Internal(Literal(LStr))

import SimpleEditor.Syntax as S
import SimpleEditor.JSON


parseModule :: (a2, String) -> (a2, JSValue)
parseModule (a2
path,String
source) =
   (a2
patha2 -> JSValue -> (a2, JSValue)
forall a1 a2. JSON a1 => a2 -> a1 -> (a2, JSValue)
.=) (JSValue -> (a2, JSValue)) -> JSValue -> (a2, JSValue)
forall a b. (a -> b) -> a -> b
$
   case P SourceModule -> ByteString -> Either (Posn, String) SourceModule
forall a. P a -> ByteString -> Either (Posn, String) a
runP P SourceModule
pModDef (String -> ByteString
UTF8.fromString String
source) of
     Left (Pn Int
l Int
c,String
msg) ->
         [(String, JSValue)] -> JSValue
makeObj [String
"error"String -> String -> (String, JSValue)
forall a1 a2. JSON a1 => a2 -> a1 -> (a2, JSValue)
.=String
msg, String
"location"String -> String -> (String, JSValue)
forall a1 a2. JSON a1 => a2 -> a1 -> (a2, JSValue)
.= Int -> String
forall a. Show a => a -> String
show Int
lString -> String -> String
forall a. [a] -> [a] -> [a]
++String
":"String -> String -> String
forall a. [a] -> [a] -> [a]
++Int -> String
forall a. Show a => a -> String
show Int
c]
     Right SourceModule
mod -> case SourceModule -> Err Grammar
forall (m :: * -> *). MonadFail m => SourceModule -> m Grammar
convModule SourceModule
mod of
                    Ok Grammar
g -> [(String, JSValue)] -> JSValue
makeObj [String
"converted"String -> Grammar -> (String, JSValue)
forall a1 a2. JSON a1 => a2 -> a1 -> (a2, JSValue)
.=Grammar
g]
                    Bad String
msg -> [(String, JSValue)] -> JSValue
makeObj [String
"parsed"String -> String -> (String, JSValue)
forall a1 a2. JSON a1 => a2 -> a1 -> (a2, JSValue)
.=String
msg]

{-
convAbstractFile path =
    appIOE (fmap encode . convAbstract =<< getSourceModule noOptions path)
-}

convModule :: SourceModule -> m Grammar
convModule m :: SourceModule
m@(ModuleName
modid,ModuleInfo
src) =
  if ModuleInfo -> Bool
isModAbs ModuleInfo
src
  then SourceModule -> m Grammar
forall (m :: * -> *). MonadFail m => SourceModule -> m Grammar
convAbstract SourceModule
m
  else if ModuleInfo -> Bool
isModCnc ModuleInfo
src
       then SourceModule -> m Grammar
forall (m :: * -> *). MonadFail m => SourceModule -> m Grammar
convConcrete SourceModule
m
       else String -> m Grammar
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"An abstract or concrete syntax module was expected"

convAbstract :: SourceModule -> m Grammar
convAbstract (ModuleName
modid,ModuleInfo
src) =
  do Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ModuleInfo -> Bool
isModAbs ModuleInfo
src) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Abstract syntax expected"
     Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ModuleInfo -> Bool
isCompleteModule ModuleInfo
src) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"A complete abstract syntax expected"
     [String]
extends <- [(ModuleName, MInclude)] -> m [String]
forall (t :: * -> *) (m :: * -> *).
(Traversable t, MonadFail m) =>
t (ModuleName, MInclude) -> m (t String)
convExtends (ModuleInfo -> [(ModuleName, MInclude)]
mextend ModuleInfo
src)
     ([String]
cats0,[Fun]
funs0) <- Map Ident Info -> m ([String], [Fun])
forall (m :: * -> *).
MonadFail m =>
Map Ident Info -> m ([String], [Fun])
convAbsJments (ModuleInfo -> Map Ident Info
jments ModuleInfo
src)
     let cats :: [String]
cats = [String] -> [String]
forall a. [a] -> [a]
reverse [String]
cats0
         funs :: [Fun]
funs = [Fun] -> [Fun]
forall a. [a] -> [a]
reverse [Fun]
funs0
         flags :: [(String, Literal)]
flags = Options -> [(String, Literal)]
optionsGFO (ModuleInfo -> Options
mflags ModuleInfo
src)
         startcat :: String
startcat =
           case String -> [(String, Literal)] -> Maybe Literal
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
"startcat" [(String, Literal)]
flags of
             Just (LStr String
cat) -> String
cat
             Maybe Literal
_               -> String
"-"
     Grammar -> m Grammar
forall (m :: * -> *) a. Monad m => a -> m a
return (Grammar -> m Grammar) -> Grammar -> m Grammar
forall a b. (a -> b) -> a -> b
$ String -> [String] -> Abstract -> [Concrete] -> Grammar
Grammar (ModuleName -> String
convModId ModuleName
modid) [String]
extends (String -> [String] -> [Fun] -> Abstract
Abstract String
startcat [String]
cats [Fun]
funs) []

convExtends :: t (ModuleName, MInclude) -> m (t String)
convExtends = ((ModuleName, MInclude) -> m String)
-> t (ModuleName, MInclude) -> m (t String)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ModuleName, MInclude) -> m String
forall (m :: * -> *).
MonadFail m =>
(ModuleName, MInclude) -> m String
convExtend
convExtend :: (ModuleName, MInclude) -> m String
convExtend (ModuleName
modid,MInclude
MIAll) = String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return (ModuleName -> String
convModId ModuleName
modid)
convExtend (ModuleName, MInclude)
_ = String -> m String
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"unsupported module extension"

convAbsJments :: Map Ident Info -> m ([String], [Fun])
convAbsJments Map Ident Info
jments = (([String], [Fun]) -> (Ident, Info) -> m ([String], [Fun]))
-> ([String], [Fun]) -> [(Ident, Info)] -> m ([String], [Fun])
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ([String], [Fun]) -> (Ident, Info) -> m ([String], [Fun])
forall (m :: * -> *).
MonadFail m =>
([String], [Fun]) -> (Ident, Info) -> m ([String], [Fun])
convAbsJment ([],[]) (Map Ident Info -> [(Ident, Info)]
forall a. Map a Info -> [(a, Info)]
jmentList Map Ident Info
jments)

convAbsJment :: ([String], [Fun]) -> (Ident, Info) -> m ([String], [Fun])
convAbsJment ([String]
cats,[Fun]
funs) (Ident
name,Info
jment) =
  case Info
jment of
    AbsCat Maybe (L Context)
octx -> do Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Context -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Context -> (L Context -> Context) -> Maybe (L Context) -> Context
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] L Context -> Context
forall a. L a -> a
unLoc Maybe (L Context)
octx)) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
                             String -> m ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"category with context"
                      let cat :: String
cat = Ident -> String
convId Ident
name
                      ([String], [Fun]) -> m ([String], [Fun])
forall (m :: * -> *) a. Monad m => a -> m a
return (String
catString -> [String] -> [String]
forall a. a -> [a] -> [a]
:[String]
cats,[Fun]
funs)
    AbsFun (Just L Type
lt) Maybe Int
_ Maybe [L Equation]
oeqns Maybe Bool
_ -> do Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([L Equation] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([L Equation]
-> ([L Equation] -> [L Equation])
-> Maybe [L Equation]
-> [L Equation]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] [L Equation] -> [L Equation]
forall a. a -> a
id Maybe [L Equation]
oeqns)) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
                                            String -> m ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"function with equations"
                                     let f :: String
f = Ident -> String
convId Ident
name
                                     [String]
typ <- Type -> m [String]
forall (m :: * -> *). MonadFail m => Type -> m [String]
convType (L Type -> Type
forall a. L a -> a
unLoc L Type
lt)
                                     let fun :: Fun
fun = String -> [String] -> Fun
Fun String
f [String]
typ
                                     ([String], [Fun]) -> m ([String], [Fun])
forall (m :: * -> *) a. Monad m => a -> m a
return ([String]
cats,Fun
funFun -> [Fun] -> [Fun]
forall a. a -> [a] -> [a]
:[Fun]
funs)
    Info
_ -> String -> m ([String], [Fun])
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> m ([String], [Fun])) -> String -> m ([String], [Fun])
forall a b. (a -> b) -> a -> b
$ String
"unsupported judgement form: "String -> String -> String
forall a. [a] -> [a] -> [a]
++Info -> String
forall a. Show a => a -> String
show Info
jment

convType :: Type -> m [String]
convType (Prod BindType
_ Ident
_ Type
t1 Type
t2) = (:) (String -> [String] -> [String])
-> m String -> m ([String] -> [String])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Type -> m String
forall (m :: * -> *). MonadFail m => Type -> m String
convSimpleType Type
t1 m ([String] -> [String]) -> m [String] -> m [String]
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
`ap` Type -> m [String]
convType Type
t2
convType Type
t = (String -> [String] -> [String]
forall a. a -> [a] -> [a]
:[]) (String -> [String]) -> m String -> m [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Type -> m String
forall (m :: * -> *). MonadFail m => Type -> m String
convSimpleType Type
t


convSimpleType :: Type -> m String
convSimpleType (Vr Ident
id) = String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return (Ident -> String
convId Ident
id)
convSimpleType Type
t = String -> m String
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"unsupported type"

convId :: Ident -> String
convId = Ident -> String
showIdent
convModId :: ModuleName -> String
convModId (MN Ident
m) = Ident -> String
convId Ident
m

convConcrete :: SourceModule -> m Grammar
convConcrete (ModuleName
modid,ModuleInfo
src) =
  do Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ModuleInfo -> Bool
isModCnc ModuleInfo
src) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Concrete syntax expected"
     Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ModuleInfo -> Bool
isCompleteModule ModuleInfo
src) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"A complete concrete syntax expected"
     [String]
extends <- [(ModuleName, MInclude)] -> m [String]
forall (t :: * -> *) (m :: * -> *).
(Traversable t, MonadFail m) =>
t (ModuleName, MInclude) -> m (t String)
convExtends (ModuleInfo -> [(ModuleName, MInclude)]
mextend ModuleInfo
src)
     [String]
opens <- [OpenSpec] -> m [String]
forall (t :: * -> *) (m :: * -> *).
(Traversable t, MonadFail m) =>
t OpenSpec -> m (t String)
convOpens (ModuleInfo -> [OpenSpec]
mopens ModuleInfo
src)
     [CncJment]
js <- Map Ident Info -> m [CncJment]
forall (m :: * -> *). MonadFail m => Map Ident Info -> m [CncJment]
convCncJments (ModuleInfo -> Map Ident Info
jments ModuleInfo
src)
     let ps :: [Param]
ps  = [Param
p  | Pa Param
p <-[CncJment]
js]
         lcs :: [Lincat]
lcs = [Lincat
lc | LC Lincat
lc<-[CncJment]
js]
         os :: [Oper]
os  = [Oper
o  | Op Oper
o <-[CncJment]
js]
         ls :: [Lin]
ls  = [Lin
l  | Li Lin
l <-[CncJment]
js]
         langcode :: String
langcode = String
"" -- !!!
         conc :: Concrete
conc = String
-> [String] -> [Param] -> [Lincat] -> [Oper] -> [Lin] -> Concrete
Concrete String
langcode [String]
opens [Param]
ps [Lincat]
lcs [Oper]
os [Lin]
ls
         abs :: Abstract
abs = String -> [String] -> [Fun] -> Abstract
Abstract String
"-" [] [] -- dummy
     Grammar -> m Grammar
forall (m :: * -> *) a. Monad m => a -> m a
return (Grammar -> m Grammar) -> Grammar -> m Grammar
forall a b. (a -> b) -> a -> b
$ String -> [String] -> Abstract -> [Concrete] -> Grammar
Grammar (ModuleName -> String
convModId ModuleName
modid) [String]
extends Abstract
abs [Concrete
conc]

convOpens :: t OpenSpec -> m (t String)
convOpens = (OpenSpec -> m String) -> t OpenSpec -> m (t String)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM OpenSpec -> m String
forall (m :: * -> *). MonadFail m => OpenSpec -> m String
convOpen

convOpen :: OpenSpec -> m String
convOpen OpenSpec
o =
  case OpenSpec
o of
    OSimple ModuleName
id -> String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return (ModuleName -> String
convModId ModuleName
id)
    OpenSpec
_ -> String -> m String
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"unsupported module open"


data CncJment = Pa S.Param | LC Lincat | Op Oper | Li Lin | Ignored

convCncJments :: Map Ident Info -> m [CncJment]
convCncJments = ((Ident, Info) -> m CncJment) -> [(Ident, Info)] -> m [CncJment]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Ident, Info) -> m CncJment
forall (m :: * -> *). MonadFail m => (Ident, Info) -> m CncJment
convCncJment ([(Ident, Info)] -> m [CncJment])
-> (Map Ident Info -> [(Ident, Info)])
-> Map Ident Info
-> m [CncJment]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Ident Info -> [(Ident, Info)]
forall a. Map a Info -> [(a, Info)]
jmentList

convCncJment :: (Ident, Info) -> m CncJment
convCncJment (Ident
name,Info
jment) =
  case Info
jment of
    ResParam Maybe (L [Param])
ops Maybe [Type]
_ ->
      CncJment -> m CncJment
forall (m :: * -> *) a. Monad m => a -> m a
return (CncJment -> m CncJment) -> CncJment -> m CncJment
forall a b. (a -> b) -> a -> b
$ Param -> CncJment
Pa (Param -> CncJment) -> Param -> CncJment
forall a b. (a -> b) -> a -> b
$ String -> String -> Param
Param String
i (String -> (L [Param] -> String) -> Maybe (L [Param]) -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" (Doc -> String
forall a. Pretty a => a -> String
render (Doc -> String) -> (L [Param] -> Doc) -> L [Param] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermPrintQual -> [Param] -> Doc
forall a1 a.
Pretty a1 =>
TermPrintQual -> [(a1, [(a, Ident, Type)])] -> Doc
ppParams TermPrintQual
q ([Param] -> Doc) -> (L [Param] -> [Param]) -> L [Param] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. L [Param] -> [Param]
forall a. L a -> a
unLoc) Maybe (L [Param])
ops)
    ResValue L Type
_ -> CncJment -> m CncJment
forall (m :: * -> *) a. Monad m => a -> m a
return CncJment
Ignored
    CncCat (Just (L Location
_ Type
typ)) Maybe (L Type)
Nothing Maybe (L Type)
Nothing Maybe (L Type)
pprn Maybe PMCFG
_ -> -- ignores printname !!
      CncJment -> m CncJment
forall (m :: * -> *) a. Monad m => a -> m a
return (CncJment -> m CncJment) -> CncJment -> m CncJment
forall a b. (a -> b) -> a -> b
$ Lincat -> CncJment
LC (Lincat -> CncJment) -> Lincat -> CncJment
forall a b. (a -> b) -> a -> b
$ String -> String -> Lincat
Lincat String
i (Doc -> String
forall a. Pretty a => a -> String
render (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
q Integer
0 Type
typ)
    ResOper Maybe (L Type)
oltyp (Just L Type
lterm) -> CncJment -> m CncJment
forall (m :: * -> *) a. Monad m => a -> m a
return (CncJment -> m CncJment) -> CncJment -> m CncJment
forall a b. (a -> b) -> a -> b
$ Oper -> CncJment
Op (Oper -> CncJment) -> Oper -> CncJment
forall a b. (a -> b) -> a -> b
$ String -> String -> Oper
Oper String
lhs String
rhs
      where
        lhs :: String
lhs = String
iString -> String -> String
forall a. [a] -> [a] -> [a]
++String -> (L Type -> String) -> Maybe (L Type) -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" ((String
" : "String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> (L Type -> String) -> L Type -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> String
forall a. Pretty a => a -> String
render (Doc -> String) -> (L Type -> Doc) -> L Type -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
q Integer
0 (Type -> Doc) -> (L Type -> Type) -> L Type -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. L Type -> Type
forall a. L a -> a
unLoc) Maybe (L Type)
oltyp
        rhs :: String
rhs = Doc -> String
forall a. Pretty a => a -> String
render (String
" ="String -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+>TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
q Integer
0 (L Type -> Type
forall a. L a -> a
unLoc L Type
lterm))
    ResOverload [] [(L Type, L Type)]
defs -> CncJment -> m CncJment
forall (m :: * -> *) a. Monad m => a -> m a
return (CncJment -> m CncJment) -> CncJment -> m CncJment
forall a b. (a -> b) -> a -> b
$ Oper -> CncJment
Op (Oper -> CncJment) -> Oper -> CncJment
forall a b. (a -> b) -> a -> b
$ String -> String -> Oper
Oper String
lhs String
rhs
      where
        lhs :: String
lhs = String
i
        rhs :: String
rhs = Doc -> String
forall a. Pretty a => a -> String
render (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ String
" = overload"String -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+>TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
q Integer
0 Type
r
        r :: Type
r =  [Assign] -> Type
R [(Label
lab,(Type -> Maybe Type
forall a. a -> Maybe a
Just Type
ty,Type
fu)) | (L Location
_ Type
ty,L Location
_ Type
fu) <-[(L Type, L Type)]
defs]
        lab :: Label
lab = Ident -> Label
ident2label Ident
name
    CncFun Maybe (Ident, Context, Type)
_ (Just L Type
ldef) Maybe (L Type)
pprn Maybe PMCFG
_ -> -- ignores printname !!
      do let ([(BindType, Ident)]
xs,Type
e') = Type -> ([(BindType, Ident)], Type)
getAbs (L Type -> Type
forall a. L a -> a
unLoc L Type
ldef)
             lin :: String
lin = Doc -> String
forall a. Pretty a => a -> String
render (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ TermPrintQual -> Integer -> Type -> Doc
forall t. (Ord t, Num t) => TermPrintQual -> t -> Type -> Doc
ppTerm TermPrintQual
q Integer
0 Type
e'
         [String]
args <- ((BindType, Ident) -> m String)
-> [(BindType, Ident)] -> m [String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (BindType, Ident) -> m String
forall (m :: * -> *). MonadFail m => (BindType, Ident) -> m String
convBind [(BindType, Ident)]
xs
         CncJment -> m CncJment
forall (m :: * -> *) a. Monad m => a -> m a
return (CncJment -> m CncJment) -> CncJment -> m CncJment
forall a b. (a -> b) -> a -> b
$ Lin -> CncJment
Li (Lin -> CncJment) -> Lin -> CncJment
forall a b. (a -> b) -> a -> b
$ String -> [String] -> String -> Lin
Lin String
i [String]
args String
lin
    Info
_ -> String -> m CncJment
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> m CncJment) -> String -> m CncJment
forall a b. (a -> b) -> a -> b
$ String
"unsupported judgement form: "String -> String -> String
forall a. [a] -> [a] -> [a]
++Info -> String
forall a. Show a => a -> String
show Info
jment
  where
    i :: String
i = Ident -> String
convId Ident
name
    q :: TermPrintQual
q = TermPrintQual
Unqualified

convBind :: (BindType, Ident) -> m String
convBind (BindType
Explicit,Ident
v) = String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> m String) -> String -> m String
forall a b. (a -> b) -> a -> b
$ Ident -> String
convId Ident
v
convBind (BindType
Implicit,Ident
v) = String -> m String
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"implicit binding not supported"

jmentList :: Map a Info -> [(a, Info)]
jmentList = ((a, Info) -> (a, Info) -> Ordering) -> [(a, Info)] -> [(a, Info)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Maybe Location -> Maybe Location -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Maybe Location -> Maybe Location -> Ordering)
-> ((a, Info) -> Maybe Location)
-> (a, Info)
-> (a, Info)
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Info -> Maybe Location
jmentLocation(Info -> Maybe Location)
-> ((a, Info) -> Info) -> (a, Info) -> Maybe Location
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(a, Info) -> Info
forall a b. (a, b) -> b
snd)) ([(a, Info)] -> [(a, Info)])
-> (Map a Info -> [(a, Info)]) -> Map a Info -> [(a, Info)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map a Info -> [(a, Info)]
forall k a. Map k a -> [(k, a)]
Map.toList

jmentLocation :: Info -> Maybe Location
jmentLocation Info
jment =
  case Info
jment of
    AbsCat Maybe (L Context)
ctxt      -> (L Context -> Location) -> Maybe (L Context) -> Maybe Location
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap L Context -> Location
forall a. L a -> Location
loc Maybe (L Context)
ctxt
    AbsFun Maybe (L Type)
ty Maybe Int
_ Maybe [L Equation]
_ Maybe Bool
_  -> (L Type -> Location) -> Maybe (L Type) -> Maybe Location
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap L Type -> Location
forall a. L a -> Location
loc Maybe (L Type)
ty
    ResParam Maybe (L [Param])
ops Maybe [Type]
_   -> (L [Param] -> Location) -> Maybe (L [Param]) -> Maybe Location
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap L [Param] -> Location
forall a. L a -> Location
loc Maybe (L [Param])
ops
    CncCat Maybe (L Type)
ty Maybe (L Type)
_ Maybe (L Type)
_ Maybe (L Type)
_ Maybe PMCFG
_ ->(L Type -> Location) -> Maybe (L Type) -> Maybe Location
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap L Type -> Location
forall a. L a -> Location
loc Maybe (L Type)
ty
    ResOper Maybe (L Type)
ty Maybe (L Type)
rhs   -> (L Type -> Location) -> Maybe (L Type) -> Maybe Location
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap L Type -> Location
forall a. L a -> Location
loc Maybe (L Type)
rhs Maybe Location -> Maybe Location -> Maybe Location
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` (L Type -> Location) -> Maybe (L Type) -> Maybe Location
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap L Type -> Location
forall a. L a -> Location
loc Maybe (L Type)
ty
    CncFun Maybe (Ident, Context, Type)
_ Maybe (L Type)
rhs Maybe (L Type)
_ Maybe PMCFG
_ -> (L Type -> Location) -> Maybe (L Type) -> Maybe Location
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap L Type -> Location
forall a. L a -> Location
loc Maybe (L Type)
rhs
    Info
_ -> Maybe Location
forall a. Maybe a
Nothing


loc :: L a -> Location
loc (L Location
l a
_) = Location
l