module Isabelle.IsaImport where

import Text.XML.HaXml.OneOfN
import Text.XML.HaXml.XmlContent (fReadXml, List1 (..))
import Isabelle.IsaExport
import qualified Isabelle.IsaSign as IsaSign
import qualified Isabelle.IsaConsts as IsaConsts
import Data.Maybe (fromMaybe, isJust)

type IsaData = (String, Maybe String, [String], [String],
                [String], [IsaSign.Sentence])

importIsaDataIO :: String ->
 IO [IsaData]
importIsaDataIO :: String -> IO [IsaData]
importIsaDataIO p :: String
p = do
 Export (NonEmpty thys :: [Thy]
thys) <- String -> IO Export
forall a. XmlContent a => String -> IO a
fReadXml String
p
 [IsaData] -> IO [IsaData]
forall (m :: * -> *) a. Monad m => a -> m a
return ([IsaData] -> IO [IsaData]) -> [IsaData] -> IO [IsaData]
forall a b. (a -> b) -> a -> b
$ [Thy] -> [IsaData]
importIsaData [Thy]
thys

importIsaData :: [Thy] -> [IsaData]
importIsaData :: [Thy] -> [IsaData]
importIsaData = (Thy -> IsaData) -> [Thy] -> [IsaData]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Thy a :: Thy_Attrs
a imports :: List1 Import
imports keywords :: [Keyword]
keywords uses :: [UseFile]
uses body :: Body
body) ->
 let imports' :: [String]
imports' = (\ (NonEmpty l :: [Import]
l) -> (Import -> String) -> [Import] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Import -> String
importName [Import]
l) List1 Import
imports
     keywords' :: [String]
keywords' = (Keyword -> String) -> [Keyword] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Keyword -> String
keywordName [Keyword]
keywords
     uses' :: [String]
uses' = (UseFile -> String) -> [UseFile] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map UseFile -> String
useFileName [UseFile]
uses
     body' :: [Sentence]
body' = (Body_ -> Sentence) -> [Body_] -> [Sentence]
forall a b. (a -> b) -> [a] -> [b]
map Body_ -> Sentence
hXmlBody_2IsaSentence ((\ (Body l :: [Body_]
l) -> [Body_]
l) Body
body)
 in (Thy_Attrs -> String
thyName Thy_Attrs
a, Thy_Attrs -> Maybe String
thyHeader Thy_Attrs
a, [String]
imports', [String]
keywords', [String]
uses', [Sentence]
body'))

hXmlBody_2IsaSentence :: Body_ -> IsaSign.Sentence
hXmlBody_2IsaSentence :: Body_ -> Sentence
hXmlBody_2IsaSentence (Body_Locale (Locale a :: Locale_Attrs
a ctxt :: Ctxt
ctxt parents :: [Parent]
parents body :: Body
body)) =
 Locale :: QName -> Ctxt -> [QName] -> [Sentence] -> Sentence
IsaSign.Locale {
  localeName :: QName
IsaSign.localeName = String -> QName
IsaSign.mkQName (String -> QName) -> String -> QName
forall a b. (a -> b) -> a -> b
$ Locale_Attrs -> String
localeName Locale_Attrs
a,
  localeContext :: Ctxt
IsaSign.localeContext = Ctxt -> Ctxt
hXmlCtxt2IsaCtxt Ctxt
ctxt,
  localeParents :: [QName]
IsaSign.localeParents = (Parent -> QName) -> [Parent] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map (String -> QName
IsaSign.mkQName (String -> QName) -> (Parent -> String) -> Parent -> QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Parent -> String
parentName) [Parent]
parents,
  localeBody :: [Sentence]
IsaSign.localeBody = (Body_ -> Sentence) -> [Body_] -> [Sentence]
forall a b. (a -> b) -> [a] -> [b]
map Body_ -> Sentence
hXmlBody_2IsaSentence ((\ (Body l :: [Body_]
l) -> [Body_]
l) Body
body) }
hXmlBody_2IsaSentence (Body_Cls (Cls a :: Cls_Attrs
a ctxt :: Ctxt
ctxt parents :: [Parent]
parents body :: Body
body)) =
 Class :: QName -> Ctxt -> [QName] -> [Sentence] -> Sentence
IsaSign.Class {
  className :: QName
IsaSign.className = String -> QName
IsaSign.mkQName (String -> QName) -> String -> QName
forall a b. (a -> b) -> a -> b
$ Cls_Attrs -> String
clsName Cls_Attrs
a,
  classContext :: Ctxt
IsaSign.classContext = Ctxt -> Ctxt
hXmlCtxt2IsaCtxt Ctxt
ctxt,
  classParents :: [QName]
IsaSign.classParents = (Parent -> QName) -> [Parent] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map (String -> QName
IsaSign.mkQName (String -> QName) -> (Parent -> String) -> Parent -> QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Parent -> String
parentName) [Parent]
parents,
  classBody :: [Sentence]
IsaSign.classBody = (Body_ -> Sentence) -> [Body_] -> [Sentence]
forall a b. (a -> b) -> [a] -> [b]
map Body_ -> Sentence
hXmlBody_2IsaSentence ((\ (Body l :: [Body_]
l) -> [Body_]
l) Body
body) }
hXmlBody_2IsaSentence (Body_TypeSynonym (TypeSynonym a :: TypeSynonym_Attrs
a mx :: Maybe Mixfix
mx (Vars vars :: [TFree]
vars) tp :: OneOf3 TVar TFree Type
tp)) =
 QName -> Maybe Mixfix -> [String] -> Typ -> Sentence
IsaSign.TypeSynonym (String -> QName
IsaSign.mkQName (String -> QName) -> String -> QName
forall a b. (a -> b) -> a -> b
$ TypeSynonym_Attrs -> String
typeSynonymName TypeSynonym_Attrs
a)
                     ((Mixfix -> Mixfix) -> Maybe Mixfix -> Maybe Mixfix
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Mixfix -> Mixfix
hXmlMixfix2IsaMixfix Maybe Mixfix
mx)
                     ((TFree -> String) -> [TFree] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\ (TFree a' :: TFree_Attrs
a' _ ) -> TFree_Attrs -> String
tFreeName TFree_Attrs
a') [TFree]
vars)
                     (OneOf3 TVar TFree Type -> Typ
hXmlOneOf3_2IsaTyp OneOf3 TVar TFree Type
tp)
hXmlBody_2IsaSentence (Body_Datatypes (Datatypes (NonEmpty dts :: [Datatype]
dts))) =
 [Datatype] -> Sentence
IsaSign.Datatypes ((Datatype -> Datatype) -> [Datatype] -> [Datatype]
forall a b. (a -> b) -> [a] -> [b]
map Datatype -> Datatype
hXmlDatatype2IsaDatatype [Datatype]
dts)
hXmlBody_2IsaSentence (Body_Domains (Domains (NonEmpty dts :: [Domain]
dts))) =
 [Domain] -> Sentence
IsaSign.Domains ((Domain -> Domain) -> [Domain] -> [Domain]
forall a b. (a -> b) -> [a] -> [b]
map Domain -> Domain
hXmlDomain2IsaDomain [Domain]
dts)
hXmlBody_2IsaSentence (Body_Consts (Consts (NonEmpty consts :: [ConstDef]
consts))) =
 [(String, Maybe Mixfix, Typ)] -> Sentence
IsaSign.Consts ((ConstDef -> (String, Maybe Mixfix, Typ))
-> [ConstDef] -> [(String, Maybe Mixfix, Typ)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (ConstDef a :: ConstDef_Attrs
a m :: Maybe Mixfix
m t :: OneOf3 TVar TFree Type
t) ->
  (ConstDef_Attrs -> String
constDefName ConstDef_Attrs
a, (Mixfix -> Mixfix) -> Maybe Mixfix -> Maybe Mixfix
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Mixfix -> Mixfix
hXmlMixfix2IsaMixfix Maybe Mixfix
m,
   OneOf3 TVar TFree Type -> Typ
hXmlOneOf3_2IsaTyp OneOf3 TVar TFree Type
t)) [ConstDef]
consts)
hXmlBody_2IsaSentence (Body_Axioms (Axioms (NonEmpty axioms :: [Axiom]
axioms))) =
 [Axiom] -> Sentence
IsaSign.Axioms ((Axiom -> Axiom) -> [Axiom] -> [Axiom]
forall a b. (a -> b) -> [a] -> [b]
map Axiom -> Axiom
hXmlAxiom2IsaAxiom [Axiom]
axioms)
hXmlBody_2IsaSentence (Body_Lemma (Lemma a :: Lemma_Attrs
a ctxt :: Ctxt
ctxt (Proof proof :: String
proof) (NonEmpty s :: [Shows]
s))) =
 Lemma :: Maybe QName -> Ctxt -> Maybe String -> [Props] -> Sentence
IsaSign.Lemma {
  lemmaTarget :: Maybe QName
IsaSign.lemmaTarget = (String -> QName) -> Maybe String -> Maybe QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> QName
IsaSign.mkQName (Lemma_Attrs -> Maybe String
lemmaTarget Lemma_Attrs
a),
  lemmaContext :: Ctxt
IsaSign.lemmaContext = Ctxt -> Ctxt
hXmlCtxt2IsaCtxt Ctxt
ctxt,
  lemmaProof :: Maybe String
IsaSign.lemmaProof = String -> Maybe String
forall a. a -> Maybe a
Just String
proof,
  lemmaProps :: [Props]
IsaSign.lemmaProps = (Shows -> Props) -> [Shows] -> [Props]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Shows a' :: Shows_Attrs
a' (NonEmpty tms :: [AShow]
tms)) ->
   Props :: Maybe QName -> Maybe String -> [Prop] -> Props
IsaSign.Props {
    propsName :: Maybe QName
IsaSign.propsName = if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ Shows_Attrs -> String
showsName Shows_Attrs
a' then Maybe QName
forall a. Maybe a
Nothing
                         else QName -> Maybe QName
forall a. a -> Maybe a
Just (QName -> Maybe QName) -> QName -> Maybe QName
forall a b. (a -> b) -> a -> b
$ String -> QName
IsaSign.mkQName (String -> QName) -> String -> QName
forall a b. (a -> b) -> a -> b
$ Shows_Attrs -> String
showsName Shows_Attrs
a',
    propsArgs :: Maybe String
IsaSign.propsArgs = Shows_Attrs -> Maybe String
showsArgs Shows_Attrs
a',
    props :: [Prop]
IsaSign.props = (AShow -> Prop) -> [AShow] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map (\ (AShow (NonEmpty l :: [OneOf6 Bound Free Var Const App Abs]
l)) ->
                          case (OneOf6 Bound Free Var Const App Abs -> Term)
-> [OneOf6 Bound Free Var Const App Abs] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map ([String] -> OneOf6 Bound Free Var Const App Abs -> Term
hXmlOneOf6_2IsaTerm []) [OneOf6 Bound Free Var Const App Abs]
l of
                           t :: Term
t : tms' :: [Term]
tms' -> Prop :: Term -> [Term] -> Prop
IsaSign.Prop {prop :: Term
IsaSign.prop = Term
t,
                                                   propPats :: [Term]
IsaSign.propPats = [Term]
tms' }
                           _ -> String -> Prop
forall a. HasCallStack => String -> a
error "This should not happen!") [AShow]
tms}) [Shows]
s }
hXmlBody_2IsaSentence (Body_Definition (Definition a :: Definition_Attrs
a m :: Maybe Mixfix
m tp :: OneOf3 TVar TFree Type
tp (NonEmpty tms :: [OneOf6 Bound Free Var Const App Abs]
tms))) =
 Definition :: QName
-> Maybe Mixfix
-> Maybe String
-> Typ
-> [Term]
-> Term
-> Sentence
IsaSign.Definition {
  definitionName :: QName
IsaSign.definitionName = String -> QName
IsaSign.mkQName (String -> QName) -> String -> QName
forall a b. (a -> b) -> a -> b
$ Definition_Attrs -> String
definitionName Definition_Attrs
a,
  definitionMixfix :: Maybe Mixfix
IsaSign.definitionMixfix = (Mixfix -> Mixfix) -> Maybe Mixfix -> Maybe Mixfix
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Mixfix -> Mixfix
hXmlMixfix2IsaMixfix Maybe Mixfix
m,
  definitionTarget :: Maybe String
IsaSign.definitionTarget = Definition_Attrs -> Maybe String
definitionTarget Definition_Attrs
a,
  definitionType :: Typ
IsaSign.definitionType = OneOf3 TVar TFree Type -> Typ
hXmlOneOf3_2IsaTyp OneOf3 TVar TFree Type
tp,
  definitionVars :: [Term]
IsaSign.definitionVars = (OneOf6 Bound Free Var Const App Abs -> Term)
-> [OneOf6 Bound Free Var Const App Abs] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map ([String] -> OneOf6 Bound Free Var Const App Abs -> Term
hXmlOneOf6_2IsaTerm []) ([OneOf6 Bound Free Var Const App Abs] -> [Term])
-> [OneOf6 Bound Free Var Const App Abs] -> [Term]
forall a b. (a -> b) -> a -> b
$ [OneOf6 Bound Free Var Const App Abs]
-> [OneOf6 Bound Free Var Const App Abs]
forall a. [a] -> [a]
init [OneOf6 Bound Free Var Const App Abs]
tms,
  definitionTerm :: Term
IsaSign.definitionTerm = [String] -> OneOf6 Bound Free Var Const App Abs -> Term
hXmlOneOf6_2IsaTerm [] (OneOf6 Bound Free Var Const App Abs -> Term)
-> OneOf6 Bound Free Var Const App Abs -> Term
forall a b. (a -> b) -> a -> b
$ [OneOf6 Bound Free Var Const App Abs]
-> OneOf6 Bound Free Var Const App Abs
forall a. [a] -> a
last [OneOf6 Bound Free Var Const App Abs]
tms }
hXmlBody_2IsaSentence (Body_Funs (Funs a :: Funs_Attrs
a (NonEmpty funs :: [Fun]
funs))) =
 Fun :: Maybe QName
-> Bool
-> Maybe String
-> Bool
-> Bool
-> [(String, Maybe Mixfix, Typ, [([Term], Term)])]
-> Sentence
IsaSign.Fun {
  funTarget :: Maybe QName
IsaSign.funTarget = (String -> QName) -> Maybe String -> Maybe QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> QName
IsaSign.mkQName (Maybe String -> Maybe QName) -> Maybe String -> Maybe QName
forall a b. (a -> b) -> a -> b
$ Funs_Attrs -> Maybe String
funsTarget Funs_Attrs
a,
  funSequential :: Bool
IsaSign.funSequential = Maybe String -> Bool
forall a. Maybe a -> Bool
isJust (Maybe String -> Bool) -> Maybe String -> Bool
forall a b. (a -> b) -> a -> b
$ Funs_Attrs -> Maybe String
funsSequential Funs_Attrs
a,
  funDefault :: Maybe String
IsaSign.funDefault = Funs_Attrs -> Maybe String
funsDefault Funs_Attrs
a,
  funDomintros :: Bool
IsaSign.funDomintros = Maybe String -> Bool
forall a. Maybe a -> Bool
isJust (Maybe String -> Bool) -> Maybe String -> Bool
forall a b. (a -> b) -> a -> b
$ Funs_Attrs -> Maybe String
funsDomintros Funs_Attrs
a,
  funPartials :: Bool
IsaSign.funPartials = Maybe String -> Bool
forall a. Maybe a -> Bool
isJust (Maybe String -> Bool) -> Maybe String -> Bool
forall a b. (a -> b) -> a -> b
$ Funs_Attrs -> Maybe String
funsPartials Funs_Attrs
a,
  funEquations :: [(String, Maybe Mixfix, Typ, [([Term], Term)])]
IsaSign.funEquations = (Fun -> (String, Maybe Mixfix, Typ, [([Term], Term)]))
-> [Fun] -> [(String, Maybe Mixfix, Typ, [([Term], Term)])]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Fun a' :: Fun_Attrs
a' mx :: Maybe Mixfix
mx tp :: OneOf3 TVar TFree Type
tp (NonEmpty eqs :: [Equation]
eqs)) ->
   (Fun_Attrs -> String
funName Fun_Attrs
a', (Mixfix -> Mixfix) -> Maybe Mixfix -> Maybe Mixfix
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Mixfix -> Mixfix
hXmlMixfix2IsaMixfix Maybe Mixfix
mx,
    OneOf3 TVar TFree Type -> Typ
hXmlOneOf3_2IsaTyp OneOf3 TVar TFree Type
tp, (Equation -> ([Term], Term)) -> [Equation] -> [([Term], Term)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Equation (NonEmpty tms :: [OneOf6 Bound Free Var Const App Abs]
tms)) ->
         let tms' :: [Term]
tms' = (OneOf6 Bound Free Var Const App Abs -> Term)
-> [OneOf6 Bound Free Var Const App Abs] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map ([String] -> OneOf6 Bound Free Var Const App Abs -> Term
hXmlOneOf6_2IsaTerm []) [OneOf6 Bound Free Var Const App Abs]
tms
         in ([Term] -> [Term]
forall a. [a] -> [a]
init [Term]
tms', [Term] -> Term
forall a. [a] -> a
last [Term]
tms')) [Equation]
eqs)) [Fun]
funs }
hXmlBody_2IsaSentence (Body_Primrec (Primrec a :: Primrec_Attrs
a (NonEmpty funs :: [Fun]
funs))) =
 Primrec :: Maybe QName
-> [(String, Maybe Mixfix, Typ, [([Term], Term)])] -> Sentence
IsaSign.Primrec {
  primrecTarget :: Maybe QName
IsaSign.primrecTarget = (String -> QName) -> Maybe String -> Maybe QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> QName
IsaSign.mkQName (Maybe String -> Maybe QName) -> Maybe String -> Maybe QName
forall a b. (a -> b) -> a -> b
$ Primrec_Attrs -> Maybe String
primrecTarget Primrec_Attrs
a,
  primrecEquations :: [(String, Maybe Mixfix, Typ, [([Term], Term)])]
IsaSign.primrecEquations = (Fun -> (String, Maybe Mixfix, Typ, [([Term], Term)]))
-> [Fun] -> [(String, Maybe Mixfix, Typ, [([Term], Term)])]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Fun a' :: Fun_Attrs
a' mx :: Maybe Mixfix
mx tp :: OneOf3 TVar TFree Type
tp (NonEmpty eqs :: [Equation]
eqs)) ->
   (Fun_Attrs -> String
funName Fun_Attrs
a', (Mixfix -> Mixfix) -> Maybe Mixfix -> Maybe Mixfix
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Mixfix -> Mixfix
hXmlMixfix2IsaMixfix Maybe Mixfix
mx,
    OneOf3 TVar TFree Type -> Typ
hXmlOneOf3_2IsaTyp OneOf3 TVar TFree Type
tp, (Equation -> ([Term], Term)) -> [Equation] -> [([Term], Term)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Equation (NonEmpty tms :: [OneOf6 Bound Free Var Const App Abs]
tms)) ->
         let tms' :: [Term]
tms' = (OneOf6 Bound Free Var Const App Abs -> Term)
-> [OneOf6 Bound Free Var Const App Abs] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map ([String] -> OneOf6 Bound Free Var Const App Abs -> Term
hXmlOneOf6_2IsaTerm []) [OneOf6 Bound Free Var Const App Abs]
tms
         in ([Term] -> [Term]
forall a. [a] -> [a]
init [Term]
tms', [Term] -> Term
forall a. [a] -> a
last [Term]
tms')) [Equation]
eqs)) [Fun]
funs }
hXmlBody_2IsaSentence (Body_Fixrec (Fixrec (NonEmpty fs :: [FixrecFun]
fs))) =
 [(String, Maybe Mixfix, Typ, [FixrecEquation])] -> Sentence
IsaSign.Fixrec ([(String, Maybe Mixfix, Typ, [FixrecEquation])] -> Sentence)
-> [(String, Maybe Mixfix, Typ, [FixrecEquation])] -> Sentence
forall a b. (a -> b) -> a -> b
$ (FixrecFun -> (String, Maybe Mixfix, Typ, [FixrecEquation]))
-> [FixrecFun] -> [(String, Maybe Mixfix, Typ, [FixrecEquation])]
forall a b. (a -> b) -> [a] -> [b]
map (\ (FixrecFun a :: FixrecFun_Attrs
a mx :: Maybe Mixfix
mx tp :: OneOf3 TVar TFree Type
tp (NonEmpty eqs :: [FixrecEquation]
eqs)) ->
  (FixrecFun_Attrs -> String
fixrecFunName FixrecFun_Attrs
a, (Mixfix -> Mixfix) -> Maybe Mixfix -> Maybe Mixfix
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Mixfix -> Mixfix
hXmlMixfix2IsaMixfix Maybe Mixfix
mx,
   OneOf3 TVar TFree Type -> Typ
hXmlOneOf3_2IsaTyp OneOf3 TVar TFree Type
tp, (FixrecEquation -> FixrecEquation)
-> [FixrecEquation] -> [FixrecEquation]
forall a b. (a -> b) -> [a] -> [b]
map FixrecEquation -> FixrecEquation
hXmlFixrecEquation2IsaFixrecEquation [FixrecEquation]
eqs)) [FixrecFun]
fs
hXmlBody_2IsaSentence (Body_Instantiation
 (Instantiation a :: Instantiation_Attrs
a arity :: Arity
arity body :: Body
body)) =
 Instantiation :: String -> (Sort, [Sort]) -> [Sentence] -> Sentence
IsaSign.Instantiation {
  instantiationType :: String
IsaSign.instantiationType = Instantiation_Attrs -> String
instantiationType Instantiation_Attrs
a,
  instantiationArity :: (Sort, [Sort])
IsaSign.instantiationArity = (\ (Arity a1 :: Sort
a1 a2 :: [Sort]
a2) -> (Sort -> Sort
hXmlSort2IsaSort Sort
a1,
   (Sort -> Sort) -> [Sort] -> [Sort]
forall a b. (a -> b) -> [a] -> [b]
map Sort -> Sort
hXmlSort2IsaSort [Sort]
a2)) Arity
arity,
  instantiationBody :: [Sentence]
IsaSign.instantiationBody =
   (Body_ -> Sentence) -> [Body_] -> [Sentence]
forall a b. (a -> b) -> [a] -> [b]
map Body_ -> Sentence
hXmlBody_2IsaSentence ((\ (Body l :: [Body_]
l) -> [Body_]
l) Body
body) }
hXmlBody_2IsaSentence (Body_Instance (Instance a :: Instance_Attrs
a (Proof proof :: String
proof) h :: Maybe (Vars, Arity)
h)) =
 case (Instance_Attrs -> Maybe String
instanceClass Instance_Attrs
a, Instance_Attrs -> Maybe String
instanceRel Instance_Attrs
a, Instance_Attrs -> Maybe String
instanceClass1 Instance_Attrs
a, Maybe (Vars, Arity)
h) of
  (Just c :: String
c, Just rel :: String
rel, Just c1 :: String
c1, _) -> InstanceSubclass :: String -> String -> String -> String -> Sentence
IsaSign.InstanceSubclass {
   instanceClass :: String
IsaSign.instanceClass = String
c,
   instanceRel :: String
IsaSign.instanceRel = String
rel,
   instanceClass1 :: String
IsaSign.instanceClass1 = String
c1,
   instanceProof :: String
IsaSign.instanceProof = String
proof }
  (_, _, _, Just (Vars vars :: [TFree]
vars, Arity a1 :: Sort
a1 a2 :: [Sort]
a2)) -> InstanceArity :: [String] -> (Sort, [Sort]) -> String -> Sentence
IsaSign.InstanceArity {
              instanceTypes :: [String]
IsaSign.instanceTypes = (TFree -> String) -> [TFree] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\ (TFree a' :: TFree_Attrs
a' _ ) -> TFree_Attrs -> String
tFreeName TFree_Attrs
a') [TFree]
vars,
              instanceArity :: (Sort, [Sort])
IsaSign.instanceArity = (Sort -> Sort
hXmlSort2IsaSort Sort
a1,
                                       (Sort -> Sort) -> [Sort] -> [Sort]
forall a b. (a -> b) -> [a] -> [b]
map Sort -> Sort
hXmlSort2IsaSort [Sort]
a2),
              instanceProof :: String
IsaSign.instanceProof = String
proof }
  _ -> String -> Sentence
IsaSign.InstanceProof String
proof
hXmlBody_2IsaSentence (Body_Subclass (Subclass a :: Subclass_Attrs
a (Proof proof :: String
proof))) =
 Subclass :: String -> Maybe QName -> String -> Sentence
IsaSign.Subclass {
  subclassClass :: String
IsaSign.subclassClass = Subclass_Attrs -> String
subclassClass Subclass_Attrs
a,
  subclassTarget :: Maybe QName
IsaSign.subclassTarget = (String -> QName) -> Maybe String -> Maybe QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> QName
IsaSign.mkQName (Maybe String -> Maybe QName) -> Maybe String -> Maybe QName
forall a b. (a -> b) -> a -> b
$ Subclass_Attrs -> Maybe String
subclassTarget Subclass_Attrs
a,
  subclassProof :: String
IsaSign.subclassProof = String
proof }
hXmlBody_2IsaSentence (Body_Typedef (Typedef a :: Typedef_Attrs
a mx :: Maybe Mixfix
mx (Proof proof :: String
proof) tm :: OneOf6 Bound Free Var Const App Abs
tm vs :: [TFree]
vs)) =
 Typedef :: QName
-> [(String, Sort)]
-> Maybe Mixfix
-> Maybe (QName, QName)
-> Term
-> String
-> Sentence
IsaSign.Typedef {
  typedefName :: QName
IsaSign.typedefName = String -> QName
IsaSign.mkQName (String -> QName) -> String -> QName
forall a b. (a -> b) -> a -> b
$ Typedef_Attrs -> String
typedefType Typedef_Attrs
a,
  typedefVars :: [(String, Sort)]
IsaSign.typedefVars = (TFree -> (String, Sort)) -> [TFree] -> [(String, Sort)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (TFree a' :: TFree_Attrs
a' s :: [Class]
s) -> (TFree_Attrs -> String
tFreeName TFree_Attrs
a',
   (Class -> IsaClass) -> [Class] -> Sort
forall a b. (a -> b) -> [a] -> [b]
map Class -> IsaClass
hXmlClass2IsaClass [Class]
s)) [TFree]
vs,
  typedefMixfix :: Maybe Mixfix
IsaSign.typedefMixfix = (Mixfix -> Mixfix) -> Maybe Mixfix -> Maybe Mixfix
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Mixfix -> Mixfix
hXmlMixfix2IsaMixfix Maybe Mixfix
mx,
  typedefMorphisms :: Maybe (QName, QName)
IsaSign.typedefMorphisms = case (Typedef_Attrs -> Maybe String
typedefM1 Typedef_Attrs
a, Typedef_Attrs -> Maybe String
typedefM2 Typedef_Attrs
a) of
   (Just m1 :: String
m1, Just m2 :: String
m2) -> (QName, QName) -> Maybe (QName, QName)
forall a. a -> Maybe a
Just (String -> QName
IsaSign.mkQName String
m1, String -> QName
IsaSign.mkQName String
m2)
   _ -> Maybe (QName, QName)
forall a. Maybe a
Nothing,
  typedefTerm :: Term
IsaSign.typedefTerm = [String] -> OneOf6 Bound Free Var Const App Abs -> Term
hXmlOneOf6_2IsaTerm [] OneOf6 Bound Free Var Const App Abs
tm,
  typedefProof :: String
IsaSign.typedefProof = String
proof }
hXmlBody_2IsaSentence (Body_Defs (Defs a :: Defs_Attrs
a (NonEmpty defs :: [Def]
defs))) =
 Defs :: Bool -> Bool -> [DefEquation] -> Sentence
IsaSign.Defs {
  defsUnchecked :: Bool
IsaSign.defsUnchecked = Maybe String -> Bool
forall a. Maybe a -> Bool
isJust (Maybe String -> Bool) -> Maybe String -> Bool
forall a b. (a -> b) -> a -> b
$ Defs_Attrs -> Maybe String
defsUnchecked Defs_Attrs
a,
  defsOverloaded :: Bool
IsaSign.defsOverloaded = Maybe String -> Bool
forall a. Maybe a -> Bool
isJust (Maybe String -> Bool) -> Maybe String -> Bool
forall a b. (a -> b) -> a -> b
$ Defs_Attrs -> Maybe String
defsOverloaded Defs_Attrs
a,
  defsEquations :: [DefEquation]
IsaSign.defsEquations = (Def -> DefEquation) -> [Def] -> [DefEquation]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Def a' :: Def_Attrs
a' tp :: OneOf3 TVar TFree Type
tp tm :: OneOf6 Bound Free Var Const App Abs
tm) ->
   DefEquation :: QName -> String -> Typ -> Term -> String -> DefEquation
IsaSign.DefEquation {
    defEquationName :: QName
IsaSign.defEquationName = String -> QName
IsaSign.mkQName (String -> QName) -> String -> QName
forall a b. (a -> b) -> a -> b
$ Def_Attrs -> String
defName Def_Attrs
a',
    defEquationConst :: String
IsaSign.defEquationConst = Def_Attrs -> String
defConst Def_Attrs
a',
    defEquationConstType :: Typ
IsaSign.defEquationConstType = OneOf3 TVar TFree Type -> Typ
hXmlOneOf3_2IsaTyp OneOf3 TVar TFree Type
tp,
    defEquationTerm :: Term
IsaSign.defEquationTerm = [String] -> OneOf6 Bound Free Var Const App Abs -> Term
hXmlOneOf6_2IsaTerm [] OneOf6 Bound Free Var Const App Abs
tm,
    defEquationArgs :: String
IsaSign.defEquationArgs = Def_Attrs -> String
defArgs Def_Attrs
a' }) [Def]
defs }

hXmlCtxt2IsaCtxt :: Ctxt -> IsaSign.Ctxt
hXmlCtxt2IsaCtxt :: Ctxt -> Ctxt
hXmlCtxt2IsaCtxt (Ctxt ctxt :: [OneOf2 Fixes Assumes]
ctxt) =
 let (fixes :: [(String, Maybe Mixfix, Typ)]
fixes, assumes :: [(String, Term)]
assumes) = (([(String, Maybe Mixfix, Typ)], [(String, Term)])
 -> OneOf2 Fixes Assumes
 -> ([(String, Maybe Mixfix, Typ)], [(String, Term)]))
-> ([(String, Maybe Mixfix, Typ)], [(String, Term)])
-> [OneOf2 Fixes Assumes]
-> ([(String, Maybe Mixfix, Typ)], [(String, Term)])
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ (fixes' :: [(String, Maybe Mixfix, Typ)]
fixes', assumes' :: [(String, Term)]
assumes') c :: OneOf2 Fixes Assumes
c ->
      case OneOf2 Fixes Assumes
c of
       OneOf2 (Fixes f :: [Fix]
f) -> ([(String, Maybe Mixfix, Typ)]
fixes' [(String, Maybe Mixfix, Typ)]
-> [(String, Maybe Mixfix, Typ)] -> [(String, Maybe Mixfix, Typ)]
forall a. [a] -> [a] -> [a]
++ (Fix -> (String, Maybe Mixfix, Typ))
-> [Fix] -> [(String, Maybe Mixfix, Typ)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Fix a :: Fix_Attrs
a t :: OneOf3 TVar TFree Type
t mx :: Maybe Mixfix
mx) ->
        (Fix_Attrs -> String
fixName Fix_Attrs
a, (Mixfix -> Mixfix) -> Maybe Mixfix -> Maybe Mixfix
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Mixfix -> Mixfix
hXmlMixfix2IsaMixfix Maybe Mixfix
mx,
         OneOf3 TVar TFree Type -> Typ
hXmlOneOf3_2IsaTyp OneOf3 TVar TFree Type
t)) [Fix]
f, [(String, Term)]
assumes')
       TwoOf2 (Assumes a :: [Assumption]
a) -> ([(String, Maybe Mixfix, Typ)]
fixes', [(String, Term)]
assumes' [(String, Term)] -> [(String, Term)] -> [(String, Term)]
forall a. [a] -> [a] -> [a]
++ (Assumption -> (String, Term)) -> [Assumption] -> [(String, Term)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Assumption a' :: Assumption_Attrs
a' tm :: OneOf6 Bound Free Var Const App Abs
tm) ->
        (Assumption_Attrs -> String
assumptionName Assumption_Attrs
a', [String] -> OneOf6 Bound Free Var Const App Abs -> Term
hXmlOneOf6_2IsaTerm [] OneOf6 Bound Free Var Const App Abs
tm)) [Assumption]
a)) ([], []) [OneOf2 Fixes Assumes]
ctxt
 in Ctxt :: [(String, Maybe Mixfix, Typ)] -> [(String, Term)] -> Ctxt
IsaSign.Ctxt {
  fixes :: [(String, Maybe Mixfix, Typ)]
IsaSign.fixes = [(String, Maybe Mixfix, Typ)]
fixes,
  assumes :: [(String, Term)]
IsaSign.assumes = [(String, Term)]
assumes }

hXmlMixfix2IsaMixfix :: Mixfix -> IsaSign.Mixfix
hXmlMixfix2IsaMixfix :: Mixfix -> Mixfix
hXmlMixfix2IsaMixfix (Mixfix a :: Mixfix_Attrs
a symbs :: [OneOf4 Arg AString Break Block]
symbs) = Mixfix :: Int -> Int -> String -> [MixfixTemplate] -> Mixfix
IsaSign.Mixfix {
 mixfixNargs :: Int
IsaSign.mixfixNargs = String -> Int
forall a. Read a => String -> a
read (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ Mixfix_Attrs -> String
mixfixNargs Mixfix_Attrs
a,
 mixfixPrio :: Int
IsaSign.mixfixPrio = String -> Int
forall a. Read a => String -> a
read (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ Mixfix_Attrs -> String
mixfixPrio Mixfix_Attrs
a,
 mixfixPretty :: String
IsaSign.mixfixPretty = Mixfix_Attrs -> String
mixfixPretty Mixfix_Attrs
a,
 mixfixTemplate :: [MixfixTemplate]
IsaSign.mixfixTemplate = (OneOf4 Arg AString Break Block -> MixfixTemplate)
-> [OneOf4 Arg AString Break Block] -> [MixfixTemplate]
forall a b. (a -> b) -> [a] -> [b]
map OneOf4 Arg AString Break Block -> MixfixTemplate
hXmlOneOf4_2IsaMixfixTemplate [OneOf4 Arg AString Break Block]
symbs }

hXmlOneOf4_2IsaMixfixTemplate :: OneOf4 Arg AString Break Block ->
                                 IsaSign.MixfixTemplate
hXmlOneOf4_2IsaMixfixTemplate :: OneOf4 Arg AString Break Block -> MixfixTemplate
hXmlOneOf4_2IsaMixfixTemplate (OneOf4 a :: Arg
a) =
 Int -> MixfixTemplate
IsaSign.Arg (String -> Int
forall a. Read a => String -> a
read (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ Arg -> String
argPrio Arg
a)
hXmlOneOf4_2IsaMixfixTemplate (TwoOf4 a :: AString
a) =
 String -> MixfixTemplate
IsaSign.Str (AString -> String
stringVal AString
a)
hXmlOneOf4_2IsaMixfixTemplate (ThreeOf4 a :: Break
a) =
 Int -> MixfixTemplate
IsaSign.Break (String -> Int
forall a. Read a => String -> a
read (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ Break -> String
breakPrio Break
a)
hXmlOneOf4_2IsaMixfixTemplate (FourOf4 (Block a :: Block_Attrs
a as :: [OneOf4 Arg AString Break Block]
as)) =
 Int -> [MixfixTemplate] -> MixfixTemplate
IsaSign.Block (String -> Int
forall a. Read a => String -> a
read (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ Block_Attrs -> String
blockPrio Block_Attrs
a) ((OneOf4 Arg AString Break Block -> MixfixTemplate)
-> [OneOf4 Arg AString Break Block] -> [MixfixTemplate]
forall a b. (a -> b) -> [a] -> [b]
map OneOf4 Arg AString Break Block -> MixfixTemplate
hXmlOneOf4_2IsaMixfixTemplate [OneOf4 Arg AString Break Block]
as)

hXmlDatatype2IsaDatatype :: Datatype -> IsaSign.Datatype
hXmlDatatype2IsaDatatype :: Datatype -> Datatype
hXmlDatatype2IsaDatatype (Datatype a :: Datatype_Attrs
a mx :: Maybe Mixfix
mx (NonEmpty cs :: [Constructor]
cs) vars :: [TFree]
vars) =
 Datatype :: QName -> [Typ] -> Maybe Mixfix -> [DatatypeConstructor] -> Datatype
IsaSign.Datatype {
  datatypeName :: QName
IsaSign.datatypeName = String -> QName
IsaSign.mkQName (String -> QName) -> String -> QName
forall a b. (a -> b) -> a -> b
$ Datatype_Attrs -> String
datatypeName Datatype_Attrs
a,
  datatypeTVars :: [Typ]
IsaSign.datatypeTVars = (TFree -> Typ) -> [TFree] -> [Typ]
forall a b. (a -> b) -> [a] -> [b]
map TFree -> Typ
hXmlTFree2IsaTyp [TFree]
vars,
  datatypeMixfix :: Maybe Mixfix
IsaSign.datatypeMixfix = (Mixfix -> Mixfix) -> Maybe Mixfix -> Maybe Mixfix
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Mixfix -> Mixfix
hXmlMixfix2IsaMixfix Maybe Mixfix
mx,
  datatypeConstructors :: [DatatypeConstructor]
IsaSign.datatypeConstructors = (Constructor -> DatatypeConstructor)
-> [Constructor] -> [DatatypeConstructor]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Constructor a' :: Constructor_Attrs
a' mx' :: Maybe Mixfix
mx' tp :: OneOf3 TVar TFree Type
tp tps :: [OneOf3 TVar TFree Type]
tps) ->
   case Constructor_Attrs -> Maybe String
constructorName Constructor_Attrs
a' of
    Just name :: String
name ->
     DatatypeConstructor :: QName -> Typ -> Maybe Mixfix -> [Typ] -> DatatypeConstructor
IsaSign.DatatypeConstructor {
       constructorName :: QName
IsaSign.constructorName = String -> QName
IsaSign.mkQName String
name,
       constructorType :: Typ
IsaSign.constructorType = OneOf3 TVar TFree Type -> Typ
hXmlOneOf3_2IsaTyp OneOf3 TVar TFree Type
tp,
       constructorMixfix :: Maybe Mixfix
IsaSign.constructorMixfix = (Mixfix -> Mixfix) -> Maybe Mixfix -> Maybe Mixfix
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Mixfix -> Mixfix
hXmlMixfix2IsaMixfix Maybe Mixfix
mx',
       constructorArgs :: [Typ]
IsaSign.constructorArgs = (OneOf3 TVar TFree Type -> Typ)
-> [OneOf3 TVar TFree Type] -> [Typ]
forall a b. (a -> b) -> [a] -> [b]
map OneOf3 TVar TFree Type -> Typ
hXmlOneOf3_2IsaTyp [OneOf3 TVar TFree Type]
tps }
    Nothing ->
     DatatypeNoConstructor :: [Typ] -> DatatypeConstructor
IsaSign.DatatypeNoConstructor {
      constructorArgs :: [Typ]
IsaSign.constructorArgs = (OneOf3 TVar TFree Type -> Typ)
-> [OneOf3 TVar TFree Type] -> [Typ]
forall a b. (a -> b) -> [a] -> [b]
map OneOf3 TVar TFree Type -> Typ
hXmlOneOf3_2IsaTyp (OneOf3 TVar TFree Type
tp OneOf3 TVar TFree Type
-> [OneOf3 TVar TFree Type] -> [OneOf3 TVar TFree Type]
forall a. a -> [a] -> [a]
: [OneOf3 TVar TFree Type]
tps) }) [Constructor]
cs }

hXmlDomain2IsaDomain :: Domain -> IsaSign.Domain
hXmlDomain2IsaDomain :: Domain -> Domain
hXmlDomain2IsaDomain (Domain a :: Domain_Attrs
a mx :: Maybe Mixfix
mx vars :: [TFree]
vars (NonEmpty cs :: [DomainConstructor]
cs)) =
 Domain :: QName -> [Typ] -> Maybe Mixfix -> [DomainConstructor] -> Domain
IsaSign.Domain {
  domainName :: QName
IsaSign.domainName = String -> QName
IsaSign.mkQName (String -> QName) -> String -> QName
forall a b. (a -> b) -> a -> b
$ Domain_Attrs -> String
domainName Domain_Attrs
a,
  domainTVars :: [Typ]
IsaSign.domainTVars = (TFree -> Typ) -> [TFree] -> [Typ]
forall a b. (a -> b) -> [a] -> [b]
map TFree -> Typ
hXmlTFree2IsaTyp [TFree]
vars,
  domainMixfix :: Maybe Mixfix
IsaSign.domainMixfix = (Mixfix -> Mixfix) -> Maybe Mixfix -> Maybe Mixfix
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Mixfix -> Mixfix
hXmlMixfix2IsaMixfix Maybe Mixfix
mx,
  domainConstructors :: [DomainConstructor]
IsaSign.domainConstructors = (DomainConstructor -> DomainConstructor)
-> [DomainConstructor] -> [DomainConstructor]
forall a b. (a -> b) -> [a] -> [b]
map (\ (DomainConstructor a' :: DomainConstructor_Attrs
a' tp :: OneOf3 TVar TFree Type
tp args :: [DomainConstructorArg]
args) ->
   DomainConstructor :: QName -> Typ -> [DomainConstructorArg] -> DomainConstructor
IsaSign.DomainConstructor {
    domainConstructorName :: QName
IsaSign.domainConstructorName = String -> QName
IsaSign.mkQName (String -> QName) -> String -> QName
forall a b. (a -> b) -> a -> b
$ DomainConstructor_Attrs -> String
domainConstructorName DomainConstructor_Attrs
a',
    domainConstructorType :: Typ
IsaSign.domainConstructorType = OneOf3 TVar TFree Type -> Typ
hXmlOneOf3_2IsaTyp OneOf3 TVar TFree Type
tp,
    domainConstructorArgs :: [DomainConstructorArg]
IsaSign.domainConstructorArgs = (DomainConstructorArg -> DomainConstructorArg)
-> [DomainConstructorArg] -> [DomainConstructorArg]
forall a b. (a -> b) -> [a] -> [b]
map (\ (DomainConstructorArg a'' :: DomainConstructorArg_Attrs
a'' tp' :: OneOf3 TVar TFree Type
tp') ->
     DomainConstructorArg :: Maybe QName -> Typ -> Bool -> DomainConstructorArg
IsaSign.DomainConstructorArg {
      domainConstructorArgSel :: Maybe QName
IsaSign.domainConstructorArgSel = (String -> QName) -> Maybe String -> Maybe QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> QName
IsaSign.mkQName (Maybe String -> Maybe QName) -> Maybe String -> Maybe QName
forall a b. (a -> b) -> a -> b
$
                                         DomainConstructorArg_Attrs -> Maybe String
domainConstructorArgName DomainConstructorArg_Attrs
a'',
      domainConstructorArgType :: Typ
IsaSign.domainConstructorArgType = OneOf3 TVar TFree Type -> Typ
hXmlOneOf3_2IsaTyp OneOf3 TVar TFree Type
tp',
      domainConstructorArgLazy :: Bool
IsaSign.domainConstructorArgLazy = Maybe String -> Bool
forall a. Maybe a -> Bool
isJust (Maybe String -> Bool) -> Maybe String -> Bool
forall a b. (a -> b) -> a -> b
$ DomainConstructorArg_Attrs -> Maybe String
domainConstructorArgLazy DomainConstructorArg_Attrs
a''})
     [DomainConstructorArg]
args } ) [DomainConstructor]
cs}

hXmlFixrecEquation2IsaFixrecEquation :: FixrecEquation -> IsaSign.FixrecEquation
hXmlFixrecEquation2IsaFixrecEquation :: FixrecEquation -> FixrecEquation
hXmlFixrecEquation2IsaFixrecEquation (FixrecEquation a :: FixrecEquation_Attrs
a (Premises ps :: [OneOf6 Bound Free Var Const App Abs]
ps)
 (NonEmpty tms :: [OneOf6 Bound Free Var Const App Abs]
tms)) = FixrecEquation :: Bool -> [Term] -> [Term] -> Term -> FixrecEquation
IsaSign.FixrecEquation {
  fixrecEquationUnchecked :: Bool
IsaSign.fixrecEquationUnchecked = Maybe String -> Bool
forall a. Maybe a -> Bool
isJust (Maybe String -> Bool) -> Maybe String -> Bool
forall a b. (a -> b) -> a -> b
$ FixrecEquation_Attrs -> Maybe String
fixrecEquationUnchecked FixrecEquation_Attrs
a,
  fixrecEquationPremises :: [Term]
IsaSign.fixrecEquationPremises = (OneOf6 Bound Free Var Const App Abs -> Term)
-> [OneOf6 Bound Free Var Const App Abs] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map ([String] -> OneOf6 Bound Free Var Const App Abs -> Term
hXmlOneOf6_2IsaTerm []) [OneOf6 Bound Free Var Const App Abs]
ps,
  fixrecEquationPatterns :: [Term]
IsaSign.fixrecEquationPatterns = (OneOf6 Bound Free Var Const App Abs -> Term)
-> [OneOf6 Bound Free Var Const App Abs] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map ([String] -> OneOf6 Bound Free Var Const App Abs -> Term
hXmlOneOf6_2IsaTerm []) ([OneOf6 Bound Free Var Const App Abs] -> [Term])
-> [OneOf6 Bound Free Var Const App Abs] -> [Term]
forall a b. (a -> b) -> a -> b
$ [OneOf6 Bound Free Var Const App Abs]
-> [OneOf6 Bound Free Var Const App Abs]
forall a. [a] -> [a]
init [OneOf6 Bound Free Var Const App Abs]
tms,
  fixrecEquationTerm :: Term
IsaSign.fixrecEquationTerm = [String] -> OneOf6 Bound Free Var Const App Abs -> Term
hXmlOneOf6_2IsaTerm [] (OneOf6 Bound Free Var Const App Abs -> Term)
-> OneOf6 Bound Free Var Const App Abs -> Term
forall a b. (a -> b) -> a -> b
$ [OneOf6 Bound Free Var Const App Abs]
-> OneOf6 Bound Free Var Const App Abs
forall a. [a] -> a
last [OneOf6 Bound Free Var Const App Abs]
tms }

hXmlAxiom2IsaAxiom :: Axiom -> IsaSign.Axiom
hXmlAxiom2IsaAxiom :: Axiom -> Axiom
hXmlAxiom2IsaAxiom (Axiom a :: Axiom_Attrs
a tm :: OneOf6 Bound Free Var Const App Abs
tm) =
 Axiom :: QName -> String -> Term -> Axiom
IsaSign.Axiom {
  axiomName :: QName
IsaSign.axiomName = String -> QName
IsaSign.mkQName (String -> QName) -> String -> QName
forall a b. (a -> b) -> a -> b
$ Axiom_Attrs -> String
axiomName Axiom_Attrs
a,
  axiomArgs :: String
IsaSign.axiomArgs = Axiom_Attrs -> String
axiomArgs Axiom_Attrs
a,
  axiomTerm :: Term
IsaSign.axiomTerm = [String] -> OneOf6 Bound Free Var Const App Abs -> Term
hXmlOneOf6_2IsaTerm [] OneOf6 Bound Free Var Const App Abs
tm }

hXmlClass2IsaClass :: Class -> IsaSign.IsaClass
hXmlClass2IsaClass :: Class -> IsaClass
hXmlClass2IsaClass = String -> IsaClass
IsaSign.IsaClass (String -> IsaClass) -> (Class -> String) -> Class -> IsaClass
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Class -> String
className

hXmlSort2IsaSort :: Sort -> IsaSign.Sort
hXmlSort2IsaSort :: Sort -> Sort
hXmlSort2IsaSort (Sort (NonEmpty cls :: [Class]
cls)) = (Class -> IsaClass) -> [Class] -> Sort
forall a b. (a -> b) -> [a] -> [b]
map Class -> IsaClass
hXmlClass2IsaClass [Class]
cls

hXmlType2IsaTyp :: Type -> IsaSign.Typ
hXmlType2IsaTyp :: Type -> Typ
hXmlType2IsaTyp (Type attrs :: Type_Attrs
attrs tps :: [OneOf3 TVar TFree Type]
tps) =
 String -> Sort -> [Typ] -> Typ
IsaSign.Type (Type_Attrs -> String
typeName Type_Attrs
attrs) Sort
IsaConsts.holType ((OneOf3 TVar TFree Type -> Typ)
-> [OneOf3 TVar TFree Type] -> [Typ]
forall a b. (a -> b) -> [a] -> [b]
map OneOf3 TVar TFree Type -> Typ
hXmlOneOf3_2IsaTyp [OneOf3 TVar TFree Type]
tps)

hXmlTFree2IsaTyp :: TFree -> IsaSign.Typ
hXmlTFree2IsaTyp :: TFree -> Typ
hXmlTFree2IsaTyp (TFree attrs :: TFree_Attrs
attrs cls :: [Class]
cls) =
 String -> Sort -> Typ
IsaSign.TFree (TFree_Attrs -> String
tFreeName TFree_Attrs
attrs)
  ((Class -> IsaClass) -> [Class] -> Sort
forall a b. (a -> b) -> [a] -> [b]
map Class -> IsaClass
hXmlClass2IsaClass [Class]
cls)

hXmlOneOf3_2IsaTyp :: OneOf3 TVar TFree Type -> IsaSign.Typ
hXmlOneOf3_2IsaTyp :: OneOf3 TVar TFree Type -> Typ
hXmlOneOf3_2IsaTyp (OneOf3 (TVar a :: TVar_Attrs
a cls :: [Class]
cls)) =
 Indexname -> Sort -> Typ
IsaSign.TVar (String -> Int -> Indexname
IsaSign.Indexname (TVar_Attrs -> String
tVarName TVar_Attrs
a)
    (String -> Int
forall a. Read a => String -> a
read (String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe "0" (TVar_Attrs -> Maybe String
tVarIndex TVar_Attrs
a)) :: Int))
  ((Class -> IsaClass) -> [Class] -> Sort
forall a b. (a -> b) -> [a] -> [b]
map Class -> IsaClass
hXmlClass2IsaClass [Class]
cls)
hXmlOneOf3_2IsaTyp (TwoOf3 f :: TFree
f) = TFree -> Typ
hXmlTFree2IsaTyp TFree
f
hXmlOneOf3_2IsaTyp (ThreeOf3 t :: Type
t) = Type -> Typ
hXmlType2IsaTyp Type
t

hXmlOneOf6_2IsaTerm :: [String] -> OneOf6 Bound Free Var Const App Abs ->
                       IsaSign.Term
hXmlOneOf6_2IsaTerm :: [String] -> OneOf6 Bound Free Var Const App Abs -> Term
hXmlOneOf6_2IsaTerm l :: [String]
l o :: OneOf6 Bound Free Var Const App Abs
o = case OneOf6 Bound Free Var Const App Abs
o of
  (OneOf6 (Bound bindex :: String
bindex)) ->
    let idx :: Int
idx = String -> Int
forall a. Read a => String -> a
read String
bindex :: Int
    in VName -> Term
IsaSign.Free (VName -> Term) -> (String -> VName) -> String -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> VName
IsaConsts.mkVName (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ ([String]
l [String] -> Int -> String
forall a. [a] -> Int -> a
!! Int
idx)
  (TwoOf6 f :: Free
f) -> case Free
f of
                 FreeTVar a :: Free_Attrs
a _ -> Free_Attrs -> Term
free Free_Attrs
a
                 FreeTFree a :: Free_Attrs
a _ -> Free_Attrs -> Term
free Free_Attrs
a
                 FreeType a :: Free_Attrs
a _ -> Free_Attrs -> Term
free Free_Attrs
a
   where free :: Free_Attrs -> Term
free = VName -> Term
IsaSign.Free (VName -> Term) -> (Free_Attrs -> VName) -> Free_Attrs -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> VName
IsaConsts.mkVName (String -> VName) -> (Free_Attrs -> String) -> Free_Attrs -> VName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Free_Attrs -> String
freeName
  (ThreeOf6 v :: Var
v) ->
   let vattrs :: Var_Attrs
vattrs = case Var
v of
                 VarTVar d :: Var_Attrs
d _ -> Var_Attrs
d
                 VarTFree d :: Var_Attrs
d _ -> Var_Attrs
d
                 VarType d :: Var_Attrs
d _ -> Var_Attrs
d
   in VName -> Term
IsaSign.Free (VName -> Term) -> (Var_Attrs -> VName) -> Var_Attrs -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> VName
IsaConsts.mkVName (String -> VName) -> (Var_Attrs -> String) -> Var_Attrs -> VName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var_Attrs -> String
varName (Var_Attrs -> Term) -> Var_Attrs -> Term
forall a b. (a -> b) -> a -> b
$ Var_Attrs
vattrs
  (FourOf6 c :: Const
c) -> Const -> Term
hXmlConst2IsaTerm Const
c
  (FiveOf6 a :: App
a) -> [String] -> App -> Term
hXmlApp2IsaTerm [String]
l App
a
  (SixOf6 a :: Abs
a) -> [String] -> Abs -> Term
hXmlAbs2IsaTerm [String]
l Abs
a

hXmlConst2IsaTerm :: Const -> IsaSign.Term
hXmlConst2IsaTerm :: Const -> Term
hXmlConst2IsaTerm (Const a :: Const_Attrs
a t :: OneOf3 TVar TFree Type
t) =
 let vname :: VName
vname = VName :: String -> Maybe AltSyntax -> VName
IsaSign.VName {
      new :: String
IsaSign.new = Const_Attrs -> String
constName Const_Attrs
a,
      altSyn :: Maybe AltSyntax
IsaSign.altSyn = Maybe AltSyntax
forall a. Maybe a
Nothing }
 in VName -> DTyp -> Term
IsaSign.Const VName
vname (DTyp -> Term) -> DTyp -> Term
forall a b. (a -> b) -> a -> b
$ Typ -> TAttr -> Maybe Int -> DTyp
IsaSign.Hide
     (OneOf3 TVar TFree Type -> Typ
hXmlOneOf3_2IsaTyp OneOf3 TVar TFree Type
t) TAttr
IsaSign.NA Maybe Int
forall a. Maybe a
Nothing

hXmlApp2IsaTerm :: [String] -> App -> IsaSign.Term
hXmlApp2IsaTerm :: [String] -> App -> Term
hXmlApp2IsaTerm l :: [String]
l (App f1 :: OneOf6 Bound Free Var Const App Abs
f1 f2 :: OneOf6 Bound Free Var Const App Abs
f2) = Term -> Term -> Continuity -> Term
IsaSign.App ([String] -> OneOf6 Bound Free Var Const App Abs -> Term
hXmlOneOf6_2IsaTerm [String]
l OneOf6 Bound Free Var Const App Abs
f1)
                                          ([String] -> OneOf6 Bound Free Var Const App Abs -> Term
hXmlOneOf6_2IsaTerm [String]
l OneOf6 Bound Free Var Const App Abs
f2)
                                          Continuity
IsaSign.NotCont

hXmlAbs2IsaTerm :: [String] -> Abs -> IsaSign.Term
hXmlAbs2IsaTerm :: [String] -> Abs -> Term
hXmlAbs2IsaTerm l :: [String]
l (Abs attrs :: Abs_Attrs
attrs t :: OneOf3 TVar TFree Type
t f :: OneOf6 Bound Free Var Const App Abs
f) = Term -> Term -> Continuity -> Term
IsaSign.Abs
 (VName -> DTyp -> Term
IsaSign.Const (String -> VName
IsaConsts.mkVName (String -> VName) -> (Abs_Attrs -> String) -> Abs_Attrs -> VName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Abs_Attrs -> String
absVname (Abs_Attrs -> VName) -> Abs_Attrs -> VName
forall a b. (a -> b) -> a -> b
$ Abs_Attrs
attrs)
              (DTyp -> Term) -> DTyp -> Term
forall a b. (a -> b) -> a -> b
$ Typ -> TAttr -> Maybe Int -> DTyp
IsaSign.Disp (OneOf3 TVar TFree Type -> Typ
hXmlOneOf3_2IsaTyp OneOf3 TVar TFree Type
t)
                             TAttr
IsaSign.NA
                             Maybe Int
forall a. Maybe a
Nothing)
 ([String] -> OneOf6 Bound Free Var Const App Abs -> Term
hXmlOneOf6_2IsaTerm (Abs_Attrs -> String
absVname Abs_Attrs
attrs String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
l) OneOf6 Bound Free Var Const App Abs
f)
 Continuity
IsaSign.NotCont