{- |
Module      :  ./Comorphisms/PPolyTyConsHOL2IsaUtils.hs
Description :  translating a HasCASL subset to Isabelle
Copyright   :  (c) C. Maeder, DFKI 2008
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

utility function for translation from HasCASL to Isabelle leaving open how
partial values are interpreted
-}

module Comorphisms.PPolyTyConsHOL2IsaUtils
  ( mapTheory
  , simpForPairs
  , simpForOption
  , typeToks
  , transSentence
  , SimpKind (..)
  , OldSimpKind (..)
  ) where

import HasCASL.As as As
import HasCASL.AsUtils
import HasCASL.Builtin
import HasCASL.DataAna
import HasCASL.Le as Le
import HasCASL.Unify (substGen)

import Isabelle.IsaSign as Isa hiding (qname)
import Isabelle.IsaConsts
import Isabelle.IsaPrint
import Isabelle.Translate

import Common.DocUtils
import Common.Id
import Common.Result
import Common.Utils (isSingleton, number)
import Common.Lib.State
import Common.AS_Annotation
import Common.GlobalAnnotations

import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.List
import Data.Maybe
import Control.Monad (foldM, zipWithM)
import qualified Control.Monad.Fail as Fail

mapTheory :: SimpKind -> Simplifier -> (Env, [Named Le.Sentence])
          -> Result (Isa.Sign, [Named Isa.Sentence])
mapTheory :: SimpKind
-> Simplifier
-> (Env, [Named Sentence])
-> Result (Sign, [Named Sentence])
mapTheory simK :: SimpKind
simK simpF :: Simplifier
simpF (env :: Env
env, sens :: [Named Sentence]
sens) = do
      let tyToks :: Set String
tyToks = Env -> Set String
typeToks Env
env
      Sign
sign <- Env -> Set String -> Result Sign
transSignature Env
env Set String
tyToks
      [Named Sentence]
isens <- (Named Sentence -> Result (Named Sentence))
-> [Named Sentence] -> Result [Named Sentence]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Sentence -> Result Sentence)
-> Named Sentence -> Result (Named Sentence)
forall (m :: * -> *) s t.
Monad m =>
(s -> m t) -> Named s -> m (Named t)
mapNamedM ((Sentence -> Result Sentence)
 -> Named Sentence -> Result (Named Sentence))
-> (Sentence -> Result Sentence)
-> Named Sentence
-> Result (Named Sentence)
forall a b. (a -> b) -> a -> b
$ Env
-> Set String
-> SimpKind
-> Simplifier
-> Sentence
-> Result Sentence
transSentence Env
env Set String
tyToks SimpKind
simK Simplifier
simpF) [Named Sentence]
sens
      (dt :: DomainTab
dt, _, _) <- ((DomainTab, Set String, Set VName)
 -> [DataEntry] -> Result (DomainTab, Set String, Set VName))
-> (DomainTab, Set String, Set VName)
-> [[DataEntry]]
-> Result (DomainTab, Set String, Set VName)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (Env
-> Set String
-> (DomainTab, Set String, Set VName)
-> [DataEntry]
-> Result (DomainTab, Set String, Set VName)
transDataEntries Env
env Set String
tyToks)
         ([], Set String
forall a. Set a
Set.empty, Set VName
forall a. Set a
Set.empty) ([[DataEntry]] -> Result (DomainTab, Set String, Set VName))
-> [[DataEntry]] -> Result (DomainTab, Set String, Set VName)
forall a b. (a -> b) -> a -> b
$ ([DataEntry] -> Bool) -> [[DataEntry]] -> [[DataEntry]]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> ([DataEntry] -> Bool) -> [DataEntry] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [DataEntry] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) ([[DataEntry]] -> [[DataEntry]]) -> [[DataEntry]] -> [[DataEntry]]
forall a b. (a -> b) -> a -> b
$ (Named Sentence -> [DataEntry])
-> [Named Sentence] -> [[DataEntry]]
forall a b. (a -> b) -> [a] -> [b]
map
           (\ ns :: Named Sentence
ns -> case Named Sentence -> Sentence
forall s a. SenAttr s a -> s
sentence Named Sentence
ns of
             DatatypeSen ds :: [DataEntry]
ds -> [DataEntry]
ds
             _ -> []) [Named Sentence]
sens
      (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence])
forall (m :: * -> *) a. Monad m => a -> m a
return ( Sign
sign { domainTab :: DomainTab
domainTab = DomainTab -> DomainTab
forall a. [a] -> [a]
reverse DomainTab
dt }
             , (Named Sentence -> Bool) -> [Named Sentence] -> [Named Sentence]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Sentence -> Sentence -> Bool
forall a. Eq a => a -> a -> Bool
/= Term -> Sentence
mkSen Term
true) (Sentence -> Bool)
-> (Named Sentence -> Sentence) -> Named Sentence -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named Sentence -> Sentence
forall s a. SenAttr s a -> s
sentence) [Named Sentence]
isens)

-- * Signature
baseSign :: BaseSig
baseSign :: BaseSig
baseSign = BaseSig
MainHC_thy

transAssumps :: GlobalAnnos -> Set.Set String -> Assumps -> Result ConstTab
transAssumps :: GlobalAnnos -> Set String -> Assumps -> Result ConstTab
transAssumps ga :: GlobalAnnos
ga toks :: Set String
toks = (ConstTab -> (Id, Set OpInfo) -> Result ConstTab)
-> ConstTab -> [(Id, Set OpInfo)] -> Result ConstTab
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ConstTab -> (Id, Set OpInfo) -> Result ConstTab
insertOps ConstTab
forall k a. Map k a
Map.empty ([(Id, Set OpInfo)] -> Result ConstTab)
-> (Assumps -> [(Id, Set OpInfo)]) -> Assumps -> Result ConstTab
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Assumps -> [(Id, Set OpInfo)]
forall k a. Map k a -> [(k, a)]
Map.toList where
  insertOps :: ConstTab -> (Id, Set OpInfo) -> Result ConstTab
insertOps m :: ConstTab
m (name :: Id
name, ops :: Set OpInfo
ops) =
      let chk :: FunType -> Int
chk = FunType -> Int
isPlainFunType
      in case (OpInfo -> TypeScheme) -> [OpInfo] -> [TypeScheme]
forall a b. (a -> b) -> [a] -> [b]
map OpInfo -> TypeScheme
opType ([OpInfo] -> [TypeScheme]) -> [OpInfo] -> [TypeScheme]
forall a b. (a -> b) -> a -> b
$ Set OpInfo -> [OpInfo]
forall a. Set a -> [a]
Set.toList Set OpInfo
ops of
          [TypeScheme _ op :: Type
op _ ] -> do
              FunType
ty <- Type -> Result FunType
funType Type
op
              ConstTab -> Result ConstTab
forall (m :: * -> *) a. Monad m => a -> m a
return (ConstTab -> Result ConstTab) -> ConstTab -> Result ConstTab
forall a b. (a -> b) -> a -> b
$ VName -> Typ -> ConstTab -> ConstTab
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert
                         (Bool -> GlobalAnnos -> Int -> Id -> BaseSig -> Set String -> VName
mkIsaConstT (Type -> Bool
isPredType Type
op) GlobalAnnos
ga (FunType -> Int
chk FunType
ty)
                          Id
name BaseSig
baseSign Set String
toks) (FunType -> Typ
transPlainFunType FunType
ty) ConstTab
m
          infos :: [TypeScheme]
infos -> (ConstTab -> (TypeScheme, Int) -> Result ConstTab)
-> ConstTab -> [(TypeScheme, Int)] -> Result ConstTab
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ( \ m' :: ConstTab
m' (TypeScheme _ op :: Type
op _, i :: Int
i) -> do
                        FunType
ty <- Type -> Result FunType
funType Type
op
                        ConstTab -> Result ConstTab
forall (m :: * -> *) a. Monad m => a -> m a
return (ConstTab -> Result ConstTab) -> ConstTab -> Result ConstTab
forall a b. (a -> b) -> a -> b
$ VName -> Typ -> ConstTab -> ConstTab
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert
                             (Bool
-> GlobalAnnos
-> Int
-> Id
-> Int
-> BaseSig
-> Set String
-> VName
mkIsaConstIT (Type -> Bool
isPredType Type
op) GlobalAnnos
ga (FunType -> Int
chk FunType
ty)
                              Id
name Int
i BaseSig
baseSign Set String
toks) (FunType -> Typ
transPlainFunType FunType
ty) ConstTab
m'
                         ) ConstTab
m ([(TypeScheme, Int)] -> Result ConstTab)
-> [(TypeScheme, Int)] -> Result ConstTab
forall a b. (a -> b) -> a -> b
$ [TypeScheme] -> [(TypeScheme, Int)]
forall a. [a] -> [(a, Int)]
number [TypeScheme]
infos

-- all possible tokens of mixfix identifiers that must not be used as variables
getAssumpsToks :: Assumps -> Set.Set String
getAssumpsToks :: Assumps -> Set String
getAssumpsToks = (Id -> Set OpInfo -> Set String -> Set String)
-> Set String -> Assumps -> Set String
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (\ i :: Id
i ops :: Set OpInfo
ops s :: Set String
s ->
    Set String -> Set String -> Set String
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set String
s (Set String -> Set String) -> Set String -> Set String
forall a b. (a -> b) -> a -> b
$ [Set String] -> Set String
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions
        ([Set String] -> Set String) -> [Set String] -> Set String
forall a b. (a -> b) -> a -> b
$ ((OpInfo, Int) -> Set String) -> [(OpInfo, Int)] -> [Set String]
forall a b. (a -> b) -> [a] -> [b]
map (\ (_, o :: Int
o) -> Id -> Int -> BaseSig -> Set String
getConstIsaToks Id
i Int
o BaseSig
baseSign)
                     ([(OpInfo, Int)] -> [Set String])
-> [(OpInfo, Int)] -> [Set String]
forall a b. (a -> b) -> a -> b
$ [OpInfo] -> [(OpInfo, Int)]
forall a. [a] -> [(a, Int)]
number ([OpInfo] -> [(OpInfo, Int)]) -> [OpInfo] -> [(OpInfo, Int)]
forall a b. (a -> b) -> a -> b
$ Set OpInfo -> [OpInfo]
forall a. Set a -> [a]
Set.toList Set OpInfo
ops) Set String
forall a. Set a
Set.empty

typeToks :: Env -> Set.Set String
typeToks :: Env -> Set String
typeToks =
    (Id -> String) -> Set Id -> Set String
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Id -> BaseSig -> String
`showIsaTypeT` BaseSig
baseSign) (Set Id -> Set String) -> (Env -> Set Id) -> Env -> Set String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Id TypeInfo -> Set Id
forall k a. Map k a -> Set k
Map.keysSet (Map Id TypeInfo -> Set Id)
-> (Env -> Map Id TypeInfo) -> Env -> Set Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> Map Id TypeInfo
typeMap

transSignature :: Env -> Set.Set String -> Result Isa.Sign
transSignature :: Env -> Set String -> Result Sign
transSignature env :: Env
env toks :: Set String
toks = do
    let extractTypeName :: Id
-> TypeInfo
-> Map String [(IsaClass, [(Typ, Sort)])]
-> Map String [(IsaClass, [(Typ, Sort)])]
extractTypeName tyId :: Id
tyId typeInfo :: TypeInfo
typeInfo m :: Map String [(IsaClass, [(Typ, Sort)])]
m =
            let getTypeArgs :: t -> AnyKind a -> [(Typ, Sort)]
getTypeArgs n :: t
n k :: AnyKind a
k = case AnyKind a
k of
                        ClassKind _ -> []
                        FunKind _ _ r :: AnyKind a
r _ ->
                            (String -> Sort -> Typ
TFree ("'a" String -> String -> String
forall a. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
n) [], Sort
holType)
                                           (Typ, Sort) -> [(Typ, Sort)] -> [(Typ, Sort)]
forall a. a -> [a] -> [a]
: t -> AnyKind a -> [(Typ, Sort)]
getTypeArgs (t
n t -> t -> t
forall a. Num a => a -> a -> a
+ 1) AnyKind a
r
            in String
-> [(IsaClass, [(Typ, Sort)])]
-> Map String [(IsaClass, [(Typ, Sort)])]
-> Map String [(IsaClass, [(Typ, Sort)])]
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Id -> BaseSig -> String
showIsaTypeT Id
tyId BaseSig
baseSign)
                  [(IsaClass
isaTerm, Int -> AnyKind () -> [(Typ, Sort)]
forall t a. (Show t, Num t) => t -> AnyKind a -> [(Typ, Sort)]
getTypeArgs (1 :: Int) (AnyKind () -> [(Typ, Sort)]) -> AnyKind () -> [(Typ, Sort)]
forall a b. (a -> b) -> a -> b
$ TypeInfo -> AnyKind ()
typeKind TypeInfo
typeInfo)] Map String [(IsaClass, [(Typ, Sort)])]
m
    ConstTab
ct <- GlobalAnnos -> Set String -> Assumps -> Result ConstTab
transAssumps (Env -> GlobalAnnos
globAnnos Env
env) Set String
toks (Assumps -> Result ConstTab) -> Assumps -> Result ConstTab
forall a b. (a -> b) -> a -> b
$ Env -> Assumps
assumps Env
env
    Sign -> Result Sign
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign -> Result Sign) -> Sign -> Result Sign
forall a b. (a -> b) -> a -> b
$ Sign
Isa.emptySign
        { baseSig :: BaseSig
baseSig = BaseSig
baseSign
    -- translation of typeconstructors
        , tsig :: TypeSig
tsig = TypeSig
emptyTypeSig
             { arities :: Map String [(IsaClass, [(Typ, Sort)])]
arities = (Id
 -> TypeInfo
 -> Map String [(IsaClass, [(Typ, Sort)])]
 -> Map String [(IsaClass, [(Typ, Sort)])])
-> Map String [(IsaClass, [(Typ, Sort)])]
-> Map Id TypeInfo
-> Map String [(IsaClass, [(Typ, Sort)])]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey Id
-> TypeInfo
-> Map String [(IsaClass, [(Typ, Sort)])]
-> Map String [(IsaClass, [(Typ, Sort)])]
extractTypeName Map String [(IsaClass, [(Typ, Sort)])]
forall k a. Map k a
Map.empty
               (Map Id TypeInfo -> Map String [(IsaClass, [(Typ, Sort)])])
-> Map Id TypeInfo -> Map String [(IsaClass, [(Typ, Sort)])]
forall a b. (a -> b) -> a -> b
$ Env -> Map Id TypeInfo
typeMap Env
env }
        , constTab :: ConstTab
constTab = ConstTab
ct }

-- * translation of a type in an operation declaration

unitTyp :: Typ
unitTyp :: Typ
unitTyp = String -> Sort -> [Typ] -> Typ
Type "unit" Sort
holType []

mkPartialType :: Typ -> Typ
mkPartialType :: Typ -> Typ
mkPartialType arg :: Typ
arg = String -> Sort -> [Typ] -> Typ
Type "partial" [] [Typ
arg]

transFunType :: FunType -> Typ
transFunType :: FunType -> Typ
transFunType fty :: FunType
fty = case FunType
fty of
    UnitType -> Typ
unitTyp
    BoolType -> Typ
boolType
    FunType f :: FunType
f a :: FunType
a -> Typ -> Typ -> Typ
mkFunType (FunType -> Typ
transFunType FunType
f) (Typ -> Typ) -> Typ -> Typ
forall a b. (a -> b) -> a -> b
$ FunType -> Typ
transFunType FunType
a
    PartialVal a :: FunType
a -> Typ -> Typ
mkPartialType (Typ -> Typ) -> Typ -> Typ
forall a b. (a -> b) -> a -> b
$ FunType -> Typ
transFunType FunType
a
    PairType a :: FunType
a b :: FunType
b -> Typ -> Typ -> Typ
prodType (FunType -> Typ
transFunType FunType
a) (Typ -> Typ) -> Typ -> Typ
forall a b. (a -> b) -> a -> b
$ FunType -> Typ
transFunType FunType
b
    TupleType l :: [FunType]
l -> case [FunType]
l of
      [] -> String -> Typ
forall a. HasCallStack => String -> a
error "transFunType"
      _ -> FunType -> Typ
transFunType (FunType -> Typ) -> FunType -> Typ
forall a b. (a -> b) -> a -> b
$ (FunType -> FunType -> FunType) -> [FunType] -> FunType
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 FunType -> FunType -> FunType
PairType [FunType]
l
    ApplType tid :: Id
tid args :: [FunType]
args -> String -> Sort -> [Typ] -> Typ
Type (Id -> BaseSig -> String
showIsaTypeT Id
tid BaseSig
baseSign) []
                       ([Typ] -> Typ) -> [Typ] -> Typ
forall a b. (a -> b) -> a -> b
$ (FunType -> Typ) -> [FunType] -> [Typ]
forall a b. (a -> b) -> [a] -> [b]
map FunType -> Typ
transFunType [FunType]
args
    TypeVar tid :: Id
tid -> String -> Sort -> Typ
TFree (Id -> BaseSig -> String
showIsaTypeT Id
tid BaseSig
baseSign) []

-- compute number of arguments for plain CASL functions
isPlainFunType :: FunType -> Int
isPlainFunType :: FunType -> Int
isPlainFunType fty :: FunType
fty = case FunType
fty of
    FunType f :: FunType
f a :: FunType
a -> case FunType
a of
                     FunType _ _ -> -1
                     _ -> case FunType
f of
                            TupleType l :: [FunType]
l -> [FunType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [FunType]
l
                            _ -> 1
    _ -> 0

transPlainFunType :: FunType -> Typ
transPlainFunType :: FunType -> Typ
transPlainFunType fty :: FunType
fty =
    case FunType
fty of
    FunType (TupleType l :: [FunType]
l) a :: FunType
a -> case FunType
a of
        FunType _ _ -> FunType -> Typ
transFunType FunType
fty
        _ -> (FunType -> Typ -> Typ) -> Typ -> [FunType] -> Typ
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Typ -> Typ -> Typ
mkFunType (Typ -> Typ -> Typ) -> (FunType -> Typ) -> FunType -> Typ -> Typ
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FunType -> Typ
transFunType) (FunType -> Typ
transFunType FunType
a) [FunType]
l
    _ -> FunType -> Typ
transFunType FunType
fty

data FunType = UnitType | BoolType
  | FunType FunType FunType
  | PartialVal FunType
  | PairType FunType FunType -- only used to represent tuples as nested pairs
  | TupleType [FunType]
  | ApplType Id [FunType]
  | TypeVar Id
    deriving (FunType -> FunType -> Bool
(FunType -> FunType -> Bool)
-> (FunType -> FunType -> Bool) -> Eq FunType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FunType -> FunType -> Bool
$c/= :: FunType -> FunType -> Bool
== :: FunType -> FunType -> Bool
$c== :: FunType -> FunType -> Bool
Eq, Int -> FunType -> String -> String
[FunType] -> String -> String
FunType -> String
(Int -> FunType -> String -> String)
-> (FunType -> String)
-> ([FunType] -> String -> String)
-> Show FunType
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [FunType] -> String -> String
$cshowList :: [FunType] -> String -> String
show :: FunType -> String
$cshow :: FunType -> String
showsPrec :: Int -> FunType -> String -> String
$cshowsPrec :: Int -> FunType -> String -> String
Show)

isPartialVal :: FunType -> Bool
isPartialVal :: FunType -> Bool
isPartialVal t :: FunType
t = case FunType
t of
    PartialVal _ -> Bool
True
    BoolType -> Bool
True
    _ -> Bool
False

makePartialVal :: FunType -> FunType
makePartialVal :: FunType -> FunType
makePartialVal t :: FunType
t = if FunType -> Bool
isPartialVal FunType
t then FunType
t else case FunType
t of
    UnitType -> FunType
BoolType
    _ -> FunType -> FunType
PartialVal FunType
t

funType :: Type -> Result FunType
funType :: Type -> Result FunType
funType t :: Type
t = case Type -> (Type, [Type])
getTypeAppl Type
t of
   (TypeName tid :: Id
tid _ n :: Int
n, tys :: [Type]
tys)
     | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0 -> do
           [FunType]
ftys <- (Type -> Result FunType) -> [Type] -> Result [FunType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> Result FunType
funType [Type]
tys
           FunType -> Result FunType
forall (m :: * -> *) a. Monad m => a -> m a
return (FunType -> Result FunType) -> FunType -> Result FunType
forall a b. (a -> b) -> a -> b
$ case [FunType]
ftys of
             [] | Id
tid Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
unitTypeId -> FunType
UnitType
             [ty :: FunType
ty] | Id
tid Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
lazyTypeId -> FunType -> FunType
makePartialVal FunType
ty
             [t1 :: FunType
t1, t2 :: FunType
t2] | Id -> Bool
isArrow Id
tid -> FunType -> FunType -> FunType
FunType FunType
t1 (FunType -> FunType) -> FunType -> FunType
forall a b. (a -> b) -> a -> b
$
                  if Id -> Bool
isPartialArrow Id
tid then FunType -> FunType
makePartialVal FunType
t2 else FunType
t2
             (_ : _ : _) | Id -> Bool
isProductId Id
tid -> [FunType] -> FunType
TupleType [FunType]
ftys
             _ -> Id -> [FunType] -> FunType
ApplType Id
tid [FunType]
ftys
     | [Type] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
tys -> FunType -> Result FunType
forall (m :: * -> *) a. Monad m => a -> m a
return (FunType -> Result FunType) -> FunType -> Result FunType
forall a b. (a -> b) -> a -> b
$ Id -> FunType
TypeVar Id
tid
   _ -> String -> Range -> Result FunType
forall a. String -> Range -> Result a
fatal_error "funType: no flat type appl" (Range -> Result FunType) -> Range -> Result FunType
forall a b. (a -> b) -> a -> b
$ Type -> Range
forall a. GetRange a => a -> Range
getRange Type
t

-- * translation of a datatype declaration

transDataEntries :: Env -> Set.Set String
                 -> (DomainTab, Set.Set TName, Set.Set VName) -> [DataEntry]
                 -> Result (DomainTab, Set.Set TName, Set.Set VName)
transDataEntries :: Env
-> Set String
-> (DomainTab, Set String, Set VName)
-> [DataEntry]
-> Result (DomainTab, Set String, Set VName)
transDataEntries env :: Env
env tyToks :: Set String
tyToks t :: (DomainTab, Set String, Set VName)
t@(dt :: DomainTab
dt, tys :: Set String
tys, cs :: Set VName
cs) l :: [DataEntry]
l = do
    let rs :: [Result DomainEntry]
rs = (DataEntry -> Result DomainEntry)
-> [DataEntry] -> [Result DomainEntry]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> Set String -> DataEntry -> Result DomainEntry
transDataEntry Env
env Set String
tyToks) [DataEntry]
l
        ms :: [Maybe DomainEntry]
ms = (Result DomainEntry -> Maybe DomainEntry)
-> [Result DomainEntry] -> [Maybe DomainEntry]
forall a b. (a -> b) -> [a] -> [b]
map Result DomainEntry -> Maybe DomainEntry
forall a. Result a -> Maybe a
maybeResult [Result DomainEntry]
rs
        toWarning :: [Diagnosis] -> [Diagnosis]
toWarning = (Diagnosis -> Diagnosis) -> [Diagnosis] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map ( \ d :: Diagnosis
d -> Diagnosis
d { diagKind :: DiagKind
diagKind = DiagKind
Warning })
    [Diagnosis] -> Result ()
appendDiags ([Diagnosis] -> Result ()) -> [Diagnosis] -> Result ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> [Diagnosis]
toWarning ([Diagnosis] -> [Diagnosis]) -> [Diagnosis] -> [Diagnosis]
forall a b. (a -> b) -> a -> b
$ (Result DomainEntry -> [Diagnosis])
-> [Result DomainEntry] -> [Diagnosis]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Result DomainEntry -> [Diagnosis]
forall a. Result a -> [Diagnosis]
diags [Result DomainEntry]
rs
    if (Maybe DomainEntry -> Bool) -> [Maybe DomainEntry] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Maybe DomainEntry -> Bool
forall a. Maybe a -> Bool
isNothing [Maybe DomainEntry]
ms then (DomainTab, Set String, Set VName)
-> Result (DomainTab, Set String, Set VName)
forall (m :: * -> *) a. Monad m => a -> m a
return (DomainTab, Set String, Set VName)
t
        else do
        let des :: [DomainEntry]
des = [Maybe DomainEntry] -> [DomainEntry]
forall a. [Maybe a] -> [a]
catMaybes [Maybe DomainEntry]
ms
            ntys :: [String]
ntys = (DomainEntry -> String) -> [DomainEntry] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Typ -> String
Isa.typeId (Typ -> String) -> (DomainEntry -> Typ) -> DomainEntry -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DomainEntry -> Typ
forall a b. (a, b) -> a
fst) [DomainEntry]
des
            ncs :: [VName]
ncs = (DomainEntry -> [VName]) -> [DomainEntry] -> [VName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (((VName, [Typ]) -> VName) -> [(VName, [Typ])] -> [VName]
forall a b. (a -> b) -> [a] -> [b]
map (VName, [Typ]) -> VName
forall a b. (a, b) -> a
fst ([(VName, [Typ])] -> [VName])
-> (DomainEntry -> [(VName, [Typ])]) -> DomainEntry -> [VName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DomainEntry -> [(VName, [Typ])]
forall a b. (a, b) -> b
snd) [DomainEntry]
des
            foldF :: String -> (a -> String) -> Set a -> t a -> m (Set a)
foldF str :: String
str cnv :: a -> String
cnv = (Set a -> a -> m (Set a)) -> Set a -> t a -> m (Set a)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ( \ s :: Set a
s i :: a
i ->
                   if a -> Set a -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member a
i Set a
s then
                       String -> m (Set a)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m (Set a)) -> String -> m (Set a)
forall a b. (a -> b) -> a -> b
$ "duplicate " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
cnv a
i
                   else Set a -> m (Set a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set a -> m (Set a)) -> Set a -> m (Set a)
forall a b. (a -> b) -> a -> b
$ a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
Set.insert a
i Set a
s)
            Result d1 :: [Diagnosis]
d1 mrtys :: Maybe (Set String)
mrtys = String
-> (String -> String)
-> Set String
-> [String]
-> Result (Set String)
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Ord a, MonadFail m) =>
String -> (a -> String) -> Set a -> t a -> m (Set a)
foldF "datatype " String -> String
forall a. a -> a
id Set String
tys [String]
ntys
            Result d2 :: [Diagnosis]
d2 mrcs :: Maybe (Set VName)
mrcs = String
-> (VName -> String) -> Set VName -> [VName] -> Result (Set VName)
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Ord a, MonadFail m) =>
String -> (a -> String) -> Set a -> t a -> m (Set a)
foldF "constructor " VName -> String
new Set VName
cs [VName]
ncs
        [Diagnosis] -> Result ()
appendDiags ([Diagnosis] -> Result ()) -> [Diagnosis] -> Result ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> [Diagnosis]
toWarning ([Diagnosis] -> [Diagnosis]) -> [Diagnosis] -> [Diagnosis]
forall a b. (a -> b) -> a -> b
$ [Diagnosis]
d1 [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ [Diagnosis]
d2
        case (Maybe (Set String)
mrtys, Maybe (Set VName)
mrcs) of
          (Just rtys :: Set String
rtys, Just rcs :: Set VName
rcs) -> (DomainTab, Set String, Set VName)
-> Result (DomainTab, Set String, Set VName)
forall (m :: * -> *) a. Monad m => a -> m a
return ([DomainEntry]
des [DomainEntry] -> DomainTab -> DomainTab
forall a. a -> [a] -> [a]
: DomainTab
dt, Set String
rtys, Set VName
rcs)
          _ -> (DomainTab, Set String, Set VName)
-> Result (DomainTab, Set String, Set VName)
forall (m :: * -> *) a. Monad m => a -> m a
return (DomainTab, Set String, Set VName)
t

-- datatype with name (tyId) + args (tyArgs) and alternatives
transDataEntry :: Env -> Set.Set String -> DataEntry -> Result DomainEntry
transDataEntry :: Env -> Set String -> DataEntry -> Result DomainEntry
transDataEntry env :: Env
env tyToks :: Set String
tyToks de :: DataEntry
de@(DataEntry _ _ gk :: GenKind
gk _ _ alts :: Set AltDefn
alts) =
    let dp :: DataPat
dp@(DataPat _ i :: Id
i tyArgs :: [TypeArg]
tyArgs _ _) = DataEntry -> DataPat
toDataPat DataEntry
de
    in case GenKind
gk of
    Le.Free -> do
      [(VName, [Typ])]
nalts <- (AltDefn -> Result (VName, [Typ]))
-> [AltDefn] -> Result [(VName, [Typ])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Env -> Set String -> DataPat -> AltDefn -> Result (VName, [Typ])
transAltDefn Env
env Set String
tyToks DataPat
dp) ([AltDefn] -> Result [(VName, [Typ])])
-> [AltDefn] -> Result [(VName, [Typ])]
forall a b. (a -> b) -> a -> b
$ Set AltDefn -> [AltDefn]
forall a. Set a -> [a]
Set.toList Set AltDefn
alts
      let transDName :: Id -> [TypeArg] -> Typ
transDName ti :: Id
ti = String -> Sort -> [Typ] -> Typ
Type (Id -> BaseSig -> String
showIsaTypeT Id
ti BaseSig
baseSign) []
                             ([Typ] -> Typ) -> ([TypeArg] -> [Typ]) -> [TypeArg] -> Typ
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TypeArg -> Typ) -> [TypeArg] -> [Typ]
forall a b. (a -> b) -> [a] -> [b]
map TypeArg -> Typ
transTypeArg
      DomainEntry -> Result DomainEntry
forall (m :: * -> *) a. Monad m => a -> m a
return (Id -> [TypeArg] -> Typ
transDName Id
i [TypeArg]
tyArgs, [(VName, [Typ])]
nalts)
    _ -> String -> Range -> Result DomainEntry
forall a. String -> Range -> Result a
fatal_error ("not a free type: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
i)
         (Range -> Result DomainEntry) -> Range -> Result DomainEntry
forall a b. (a -> b) -> a -> b
$ Id -> Range
posOfId Id
i

-- arguments of a datatype's typeconstructor
transTypeArg :: TypeArg -> Typ
transTypeArg :: TypeArg -> Typ
transTypeArg ta :: TypeArg
ta = String -> Sort -> Typ
TFree (Id -> BaseSig -> String
showIsaTypeT (TypeArg -> Id
getTypeVar TypeArg
ta) BaseSig
baseSign) []

-- datatype alternatives/constructors
transAltDefn :: Env -> Set.Set String -> DataPat -> AltDefn
             -> Result (VName, [Typ])
transAltDefn :: Env -> Set String -> DataPat -> AltDefn -> Result (VName, [Typ])
transAltDefn env :: Env
env tyToks :: Set String
tyToks dp :: DataPat
dp@(DataPat dm :: IdMap
dm _ _ _ _) alt :: AltDefn
alt = case AltDefn
alt of
  Construct mi :: Maybe Id
mi origTs :: [Type]
origTs p :: Partiality
p _ -> let ts :: [Type]
ts = (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (IdMap -> Type -> Type
mapType IdMap
dm) [Type]
origTs in
    case Maybe Id
mi of
    Just opId :: Id
opId -> case Partiality
p of
      Total -> do
        let sc :: TypeScheme
sc = DataPat -> Partiality -> [Type] -> TypeScheme
getConstrScheme DataPat
dp Partiality
p [Type]
origTs
        [FunType]
nts <- (Type -> Result FunType) -> [Type] -> Result [FunType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> Result FunType
funType [Type]
ts
        -- extract overloaded opId number
        (VName, [Typ]) -> Result (VName, [Typ])
forall (m :: * -> *) a. Monad m => a -> m a
return (Env -> Set String -> Id -> TypeScheme -> VName
transOpId Env
env Set String
tyToks Id
opId TypeScheme
sc, case [FunType]
nts of
                [TupleType l :: [FunType]
l] -> (FunType -> Typ) -> [FunType] -> [Typ]
forall a b. (a -> b) -> [a] -> [b]
map FunType -> Typ
transFunType [FunType]
l
                _ -> (FunType -> Typ) -> [FunType] -> [Typ]
forall a b. (a -> b) -> [a] -> [b]
map FunType -> Typ
transFunType [FunType]
nts)
      Partial -> String -> Id -> Result (VName, [Typ])
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "not a total constructor" Id
opId
    Nothing -> String -> [Type] -> Result (VName, [Typ])
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "no support for data subtypes" [Type]
ts

-- * Formulas

-- variables
transVar :: Set.Set String -> Id -> VName
transVar :: Set String -> Id -> VName
transVar toks :: Set String
toks v :: Id
v = let
    s :: String
s = Id -> BaseSig -> String
showIsaConstT Id
v BaseSig
baseSign
    renVar :: String -> String
renVar t :: String
t = if String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member String
t Set String
toks then String -> String
renVar (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ "X_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t else String
t
    in String -> VName
mkVName (String -> VName) -> String -> VName
forall a b. (a -> b) -> a -> b
$ String -> String
renVar String
s

mkTypedConst :: VName -> FunType -> Isa.Term
mkTypedConst :: VName -> FunType -> Term
mkTypedConst v :: VName
v fTy :: FunType
fTy = VName -> DTyp -> Term
Isa.Const VName
v (DTyp -> Term) -> DTyp -> Term
forall a b. (a -> b) -> a -> b
$ Typ -> TAttr -> Maybe Int -> DTyp
Disp (FunType -> Typ
transFunType FunType
fTy) TAttr
NA Maybe Int
forall a. Maybe a
Nothing

transTypedVar :: Set.Set String -> VarDecl -> Result Isa.Term
transTypedVar :: Set String -> VarDecl -> Result Term
transTypedVar toks :: Set String
toks (VarDecl var :: Id
var ty :: Type
ty _ _) = do
    FunType
fTy <- Type -> Result FunType
funType Type
ty
    Term -> Result Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Result Term) -> Term -> Result Term
forall a b. (a -> b) -> a -> b
$ VName -> FunType -> Term
mkTypedConst (Set String -> Id -> VName
transVar Set String
toks Id
var) FunType
fTy

mkSimplifiedSen :: OldSimpKind -> Simplifier -> Isa.Term -> Isa.Sentence
mkSimplifiedSen :: OldSimpKind -> Simplifier -> Term -> Sentence
mkSimplifiedSen simK :: OldSimpKind
simK simpF :: Simplifier
simpF t :: Term
t = Term -> Sentence
mkSen (Term -> Sentence) -> Term -> Sentence
forall a b. (a -> b) -> a -> b
$ State Int Term -> Int -> Term
forall s a. State s a -> s -> a
evalState (OldSimpKind -> Simplifier -> Term -> State Int Term
simplify OldSimpKind
simK Simplifier
simpF Term
t) 0

isTrue :: Isa.Term -> Bool
isTrue :: Term -> Bool
isTrue t :: Term
t = case Term
t of
  Const n :: VName
n _ -> VName -> String
new VName
n String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
cTrue
  _ -> Bool
False

mkBinConj :: Isa.Term -> Isa.Term -> Isa.Term
mkBinConj :: Term -> Term -> Term
mkBinConj t1 :: Term
t1 t2 :: Term
t2 = case Term -> Bool
isTrue of
  isT :: Term -> Bool
isT | Term -> Bool
isT Term
t1 -> Term
t2
      | Term -> Bool
isT Term
t2 -> Term
t1
  _ -> Term -> Term -> Term
binConj Term
t1 Term
t2

data OldSimpKind = NoSimpLift | Lift2Restrict | Lift2Case deriving OldSimpKind -> OldSimpKind -> Bool
(OldSimpKind -> OldSimpKind -> Bool)
-> (OldSimpKind -> OldSimpKind -> Bool) -> Eq OldSimpKind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: OldSimpKind -> OldSimpKind -> Bool
$c/= :: OldSimpKind -> OldSimpKind -> Bool
== :: OldSimpKind -> OldSimpKind -> Bool
$c== :: OldSimpKind -> OldSimpKind -> Bool
Eq

data SimpKind = New | Old OldSimpKind deriving SimpKind -> SimpKind -> Bool
(SimpKind -> SimpKind -> Bool)
-> (SimpKind -> SimpKind -> Bool) -> Eq SimpKind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SimpKind -> SimpKind -> Bool
$c/= :: SimpKind -> SimpKind -> Bool
== :: SimpKind -> SimpKind -> Bool
$c== :: SimpKind -> SimpKind -> Bool
Eq

transSentence :: Env -> Set.Set String -> SimpKind -> Simplifier -> Le.Sentence
              -> Result Isa.Sentence
transSentence :: Env
-> Set String
-> SimpKind
-> Simplifier
-> Sentence
-> Result Sentence
transSentence sign :: Env
sign tyToks :: Set String
tyToks simK :: SimpKind
simK simpF :: Simplifier
simpF s :: Sentence
s = case Sentence
s of
    Le.Formula trm :: Term
trm -> do
      ITC ty :: FunType
ty t :: Term
t cs :: Cond
cs <- Env
-> Set String
-> Bool
-> Set String
-> Set VarDecl
-> Term
-> Result IsaTermCond
transTerm Env
sign Set String
tyToks (SimpKind
simK SimpKind -> SimpKind -> Bool
forall a. Eq a => a -> a -> Bool
== SimpKind
New)
        (Assumps -> Set String
getAssumpsToks (Assumps -> Set String) -> Assumps -> Set String
forall a b. (a -> b) -> a -> b
$ Env -> Assumps
assumps Env
sign) Set VarDecl
forall a. Set a
Set.empty Term
trm
      let et :: Term
et = case FunType
ty of
                 PartialVal UnitType -> Term -> Term -> Term
mkTermAppl Term
defOp Term
t
                 _ -> Term
t
          bt :: Term
bt = if Term -> Bool
isTrue Term
et then Cond -> Term
cond2bool Cond
cs else
                   Term -> Term -> Term
mkTermAppl (Cond -> Term
integrateCondInBool Cond
cs) Term
et
          st :: Sentence
st = OldSimpKind -> Simplifier -> Term -> Sentence
mkSimplifiedSen (case SimpKind
simK of
                Old osim :: OldSimpKind
osim -> OldSimpKind
osim
                New -> OldSimpKind
NoSimpLift) Simplifier
simpF Term
bt
      case FunType
ty of
        BoolType -> Sentence -> Result Sentence
forall (m :: * -> *) a. Monad m => a -> m a
return Sentence
st
        PartialVal _ -> Sentence -> Result Sentence
forall (m :: * -> *) a. Monad m => a -> m a
return Sentence
st
        FunType _ _ -> String -> Result Sentence
forall a. HasCallStack => String -> a
error "transSentence: FunType"
        PairType _ _ -> String -> Result Sentence
forall a. HasCallStack => String -> a
error "transSentence: PairType"
        TupleType _ -> String -> Result Sentence
forall a. HasCallStack => String -> a
error "transSentence: TupleType"
        ApplType _ _ -> String -> Result Sentence
forall a. HasCallStack => String -> a
error "transSentence: ApplType"
        _ -> Sentence -> Result Sentence
forall (m :: * -> *) a. Monad m => a -> m a
return (Sentence -> Result Sentence) -> Sentence -> Result Sentence
forall a b. (a -> b) -> a -> b
$ Term -> Sentence
mkSen Term
true
    DatatypeSen ls :: [DataEntry]
ls -> if (DataEntry -> Bool) -> [DataEntry] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\ (DataEntry _ _ gk :: GenKind
gk _ _ _) -> GenKind
gk GenKind -> GenKind -> Bool
forall a. Eq a => a -> a -> Bool
== GenKind
Generated) [DataEntry]
ls
      then Env
-> Set String
-> SimpKind
-> Simplifier
-> Sentence
-> Result Sentence
transSentence Env
sign Set String
tyToks SimpKind
simK Simplifier
simpF (Sentence -> Result Sentence)
-> (Term -> Sentence) -> Term -> Result Sentence
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sentence
Le.Formula
               (Term -> Result Sentence) -> Term -> Result Sentence
forall a b. (a -> b) -> a -> b
$ [DataEntry] -> Term
inductionScheme [DataEntry]
ls
      else Sentence -> Result Sentence
forall (m :: * -> *) a. Monad m => a -> m a
return (Sentence -> Result Sentence) -> Sentence -> Result Sentence
forall a b. (a -> b) -> a -> b
$ Term -> Sentence
mkSen Term
true
    ProgEqSen _ _ (ProgEq _ _ r :: Range
r) -> Sentence -> String -> Range -> Result Sentence
forall a. a -> String -> Range -> Result a
warning (Term -> Sentence
mkSen Term
true)
        "translation of sentence not implemented" Range
r

-- disambiguate operation names
transOpId :: Env -> Set.Set String -> Id -> TypeScheme -> VName
transOpId :: Env -> Set String -> Id -> TypeScheme -> VName
transOpId sign :: Env
sign tyToks :: Set String
tyToks op :: Id
op ts :: TypeScheme
ts@(TypeScheme _ ty :: Type
ty _) =
    let ga :: GlobalAnnos
ga = Env -> GlobalAnnos
globAnnos Env
sign
        Result _ mty :: Maybe FunType
mty = Type -> Result FunType
funType Type
ty
    in case Maybe FunType
mty of
         Nothing -> String -> VName
forall a. HasCallStack => String -> a
error "transOpId"
         Just fty :: FunType
fty ->
           let args :: Int
args = FunType -> Int
isPlainFunType FunType
fty
           in VName -> Maybe VName -> VName
forall a. a -> Maybe a -> a
fromMaybe (String -> VName
forall a. HasCallStack => String -> a
error (String -> VName) -> String -> VName
forall a b. (a -> b) -> a -> b
$ "transOpId " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
op) (Maybe VName -> VName) -> Maybe VName -> VName
forall a b. (a -> b) -> a -> b
$ do
           Set OpInfo
ops <- Id -> Assumps -> Maybe (Set OpInfo)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
op (Env -> Assumps
assumps Env
sign)
           if Set OpInfo -> Bool
forall a. Set a -> Bool
isSingleton Set OpInfo
ops then VName -> Maybe VName
forall (m :: * -> *) a. Monad m => a -> m a
return (VName -> Maybe VName) -> VName -> Maybe VName
forall a b. (a -> b) -> a -> b
$
              Bool -> GlobalAnnos -> Int -> Id -> BaseSig -> Set String -> VName
mkIsaConstT (Type -> Bool
isPredType Type
ty) GlobalAnnos
ga Int
args Id
op BaseSig
baseSign Set String
tyToks
             else do
                 Int
i <- TypeScheme -> [TypeScheme] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex TypeScheme
ts ([TypeScheme] -> Maybe Int) -> [TypeScheme] -> Maybe Int
forall a b. (a -> b) -> a -> b
$ (OpInfo -> TypeScheme) -> [OpInfo] -> [TypeScheme]
forall a b. (a -> b) -> [a] -> [b]
map OpInfo -> TypeScheme
opType ([OpInfo] -> [TypeScheme]) -> [OpInfo] -> [TypeScheme]
forall a b. (a -> b) -> a -> b
$ Set OpInfo -> [OpInfo]
forall a. Set a -> [a]
Set.toList Set OpInfo
ops
                 VName -> Maybe VName
forall (m :: * -> *) a. Monad m => a -> m a
return (VName -> Maybe VName) -> VName -> Maybe VName
forall a b. (a -> b) -> a -> b
$ Bool
-> GlobalAnnos
-> Int
-> Id
-> Int
-> BaseSig
-> Set String
-> VName
mkIsaConstIT (Type -> Bool
isPredType Type
ty)
                        GlobalAnnos
ga Int
args Id
op (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) BaseSig
baseSign Set String
tyToks

transLetEq :: Env -> Set.Set String -> Bool -> Set.Set String
    -> Set.Set VarDecl -> ProgEq -> Result ((As.Term, Isa.Term), IsaTermCond)
transLetEq :: Env
-> Set String
-> Bool
-> Set String
-> Set VarDecl
-> ProgEq
-> Result ((Term, Term), IsaTermCond)
transLetEq sign :: Env
sign tyToks :: Set String
tyToks collectConds :: Bool
collectConds toks :: Set String
toks pVars :: Set VarDecl
pVars (ProgEq pat :: Term
pat trm :: Term
trm r :: Range
r) = do
    (_, op :: Term
op) <- Env -> Set String -> Set String -> Term -> Result (FunType, Term)
transPattern Env
sign Set String
tyToks Set String
toks Term
pat
    p :: IsaTermCond
p@(ITC ty :: FunType
ty _ _) <- Env
-> Set String
-> Bool
-> Set String
-> Set VarDecl
-> Term
-> Result IsaTermCond
transTerm Env
sign Set String
tyToks Bool
collectConds Set String
toks Set VarDecl
pVars Term
trm
    if FunType -> Bool
isPartialVal FunType
ty Bool -> Bool -> Bool
&& Bool -> Bool
not (Term -> Bool
isQualVar Term
pat) then String -> Range -> Result ((Term, Term), IsaTermCond)
forall a. String -> Range -> Result a
fatal_error
           ("rhs must not be partial for a tuple currently: "
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Term
trm "") Range
r
       else ((Term, Term), IsaTermCond) -> Result ((Term, Term), IsaTermCond)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Term
pat, Term
op), IsaTermCond
p)

transLetEqs :: Env -> Set.Set String -> Bool -> Set.Set String
            -> Set.Set VarDecl -> [ProgEq]
            -> Result (Set.Set VarDecl, [(Isa.Term, IsaTermCond)])
transLetEqs :: Env
-> Set String
-> Bool
-> Set String
-> Set VarDecl
-> [ProgEq]
-> Result (Set VarDecl, [(Term, IsaTermCond)])
transLetEqs sign :: Env
sign tyToks :: Set String
tyToks collectConds :: Bool
collectConds toks :: Set String
toks pVars :: Set VarDecl
pVars es :: [ProgEq]
es = case [ProgEq]
es of
    [] -> (Set VarDecl, [(Term, IsaTermCond)])
-> Result (Set VarDecl, [(Term, IsaTermCond)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Set VarDecl
pVars, [])
    e :: ProgEq
e : r :: [ProgEq]
r -> do
      ((pat :: Term
pat, op :: Term
op), pt :: IsaTermCond
pt@(ITC ty :: FunType
ty _ _)) <-
        Env
-> Set String
-> Bool
-> Set String
-> Set VarDecl
-> ProgEq
-> Result ((Term, Term), IsaTermCond)
transLetEq Env
sign Set String
tyToks Bool
collectConds Set String
toks Set VarDecl
pVars ProgEq
e
      (newPVars :: Set VarDecl
newPVars, newEs :: [(Term, IsaTermCond)]
newEs) <- Env
-> Set String
-> Bool
-> Set String
-> Set VarDecl
-> [ProgEq]
-> Result (Set VarDecl, [(Term, IsaTermCond)])
transLetEqs Env
sign Set String
tyToks Bool
collectConds Set String
toks
        (if FunType -> Bool
isPartialVal FunType
ty then VarDecl -> Set VarDecl -> Set VarDecl
forall a. Ord a => a -> Set a -> Set a
Set.insert (Term -> VarDecl
getQualVar Term
pat) Set VarDecl
pVars else Set VarDecl
pVars) [ProgEq]
r
      (Set VarDecl, [(Term, IsaTermCond)])
-> Result (Set VarDecl, [(Term, IsaTermCond)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Set VarDecl
newPVars, (Term
op, IsaTermCond
pt) (Term, IsaTermCond)
-> [(Term, IsaTermCond)] -> [(Term, IsaTermCond)]
forall a. a -> [a] -> [a]
: [(Term, IsaTermCond)]
newEs)

isQualVar :: As.Term -> Bool
isQualVar :: Term -> Bool
isQualVar trm :: Term
trm = case Term
trm of
    QualVar (VarDecl {}) -> Bool
True
    TypedTerm t :: Term
t _ _ _ -> Term -> Bool
isQualVar Term
t
    _ -> Bool
False

getQualVar :: As.Term -> VarDecl
getQualVar :: Term -> VarDecl
getQualVar trm :: Term
trm = case Term
trm of
    QualVar vd :: VarDecl
vd -> VarDecl
vd
    TypedTerm t :: Term
t _ _ _ -> Term -> VarDecl
getQualVar Term
t
    _ -> String -> VarDecl
forall a. HasCallStack => String -> a
error "getQualVar"

ifImplOp :: Isa.Term
ifImplOp :: Term
ifImplOp = String -> Term
conDouble "ifImplOp"

unitOp :: Isa.Term
unitOp :: Term
unitOp = [Term] -> Continuity -> Term
Tuplex [] Continuity
NotCont

noneOp :: Isa.Term
noneOp :: Term
noneOp = String -> Term
conDouble "undefinedOp"

whenElseOp :: Isa.Term
whenElseOp :: Term
whenElseOp = String -> Term
conDouble "whenElseOp"

resOp :: Isa.Term
resOp :: Term
resOp = String -> Term
conDouble "resOp"

makeTotal :: Isa.Term
makeTotal :: Term
makeTotal = String -> Term
conDouble "makeTotal"

uncurryOpS :: String
uncurryOpS :: String
uncurryOpS = "uncurryOp"

curryOpS :: String
curryOpS :: String
curryOpS = "curryOp"

uncurryOp :: Isa.Term
uncurryOp :: Term
uncurryOp = String -> Term
conDouble String
uncurryOpS

curryOp :: Isa.Term
curryOp :: Term
curryOp = String -> Term
conDouble String
curryOpS

for :: Int -> (a -> a) -> a -> a
for :: Int -> (a -> a) -> a -> a
for n :: Int
n f :: a -> a
f a :: a
a = if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 0 then a
a else Int -> (a -> a) -> a -> a
forall a. Int -> (a -> a) -> a -> a
for (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) a -> a
f (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$ a -> a
f a
a

data IsaTermCond = ITC FunType Isa.Term Cond

data Cond = None
  | Cond Isa.Term
  | CondList [Cond]
  | PairCond Cond Cond

instance Show Cond where
  show :: Cond -> String
show c :: Cond
c = case Cond
c of
    None -> "none"
    Cond t :: Term
t -> Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ Term -> Doc
printTerm Term
t
    CondList l :: [Cond]
l -> String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate " & " ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (Cond -> String) -> [Cond] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Cond -> String
forall a. Show a => a -> String
show [Cond]
l
    PairCond p1 :: Cond
p1 p2 :: Cond
p2 -> '(' Char -> String -> String
forall a. a -> [a] -> [a]
: Cond -> String -> String
forall a. Show a => a -> String -> String
shows Cond
p1 ", " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Cond -> String -> String
forall a. Show a => a -> String -> String
shows Cond
p2 ")"

joinCond :: Cond -> Cond -> Cond
joinCond :: Cond -> Cond -> Cond
joinCond c1 :: Cond
c1 c2 :: Cond
c2 = let
  toCs :: Cond -> [Cond]
toCs c :: Cond
c = case Cond
c of
          CondList cs :: [Cond]
cs -> [Cond]
cs
          None -> []
          _ -> [Cond
c]
  in case Cond -> [Cond]
toCs Cond
c1 [Cond] -> [Cond] -> [Cond]
forall a. [a] -> [a] -> [a]
++ Cond -> [Cond]
toCs Cond
c2 of
       [] -> Cond
None
       [s :: Cond
s] -> Cond
s
       cs :: [Cond]
cs -> [Cond] -> Cond
CondList [Cond]
cs

pairCond :: Cond -> Cond -> Cond
pairCond :: Cond -> Cond -> Cond
pairCond c1 :: Cond
c1 c2 :: Cond
c2 = case (Cond
c1, Cond
c2) of
  (None, None) -> Cond
None
  _ -> Cond -> Cond -> Cond
PairCond Cond
c1 Cond
c2

condToList :: Cond -> [Isa.Term]
condToList :: Cond -> [Term]
condToList c :: Cond
c = case Cond
c of
  None -> []
  Cond t :: Term
t -> [Term
t]
  CondList cs :: [Cond]
cs -> (Cond -> [Term]) -> [Cond] -> [Term]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Cond -> [Term]
condToList [Cond]
cs
  PairCond c1 :: Cond
c1 c2 :: Cond
c2 -> Cond -> [Term]
condToList Cond
c1 [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ Cond -> [Term]
condToList Cond
c2

{- pass tokens that must not be used as variable names and pass those
variables that are partial because they have been computed in a
let-term. -}
transTerm :: Env -> Set.Set String -> Bool -> Set.Set String
          -> Set.Set VarDecl -> As.Term -> Result IsaTermCond
transTerm :: Env
-> Set String
-> Bool
-> Set String
-> Set VarDecl
-> Term
-> Result IsaTermCond
transTerm sign :: Env
sign tyToks :: Set String
tyToks collectConds :: Bool
collectConds toks :: Set String
toks pVars :: Set VarDecl
pVars trm :: Term
trm = case Term
trm of
    QualVar vd :: VarDecl
vd@(VarDecl v :: Id
v t :: Type
t _ _) -> do
        FunType
fTy <- Type -> Result FunType
funType Type
t
        let vt :: Term
vt = VName -> Term
con (VName -> Term) -> VName -> Term
forall a b. (a -> b) -> a -> b
$ Set String -> Id -> VName
transVar Set String
toks Id
v
        IsaTermCond -> Result IsaTermCond
forall (m :: * -> *) a. Monad m => a -> m a
return (IsaTermCond -> Result IsaTermCond)
-> IsaTermCond -> Result IsaTermCond
forall a b. (a -> b) -> a -> b
$ if VarDecl -> Set VarDecl -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member VarDecl
vd Set VarDecl
pVars then FunType -> Term -> Cond -> IsaTermCond
ITC (FunType -> FunType
makePartialVal FunType
fTy) Term
vt Cond
None
          else FunType -> Term -> Cond -> IsaTermCond
ITC FunType
fTy Term
vt Cond
None
    QualOp _ (PolyId opId :: Id
opId _ _) ts :: TypeScheme
ts@(TypeScheme targs :: [TypeArg]
targs ty :: Type
ty _) insts :: [Type]
insts _ _ -> do
        FunType
fTy <- Type -> Result FunType
funType Type
ty
        FunType
instfTy <- Type -> Result FunType
funType (Type -> Result FunType) -> Type -> Result FunType
forall a b. (a -> b) -> a -> b
$ Subst -> Type -> Type
substGen (if [Type] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
insts then Subst
forall k a. Map k a
Map.empty else
                    [(Int, Type)] -> Subst
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Int, Type)] -> Subst) -> [(Int, Type)] -> Subst
forall a b. (a -> b) -> a -> b
$ (TypeArg -> Type -> (Int, Type))
-> [TypeArg] -> [Type] -> [(Int, Type)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ (TypeArg _ _ _ _ i :: Int
i _ _) t :: Type
t
                                                -> (Int
i, Type
t)) [TypeArg]
targs [Type]
insts) Type
ty
        let cf :: Term -> Term
cf = Term -> Term -> Term
mkTermAppl (Cond -> ConvFun -> Term
convFun Cond
None (ConvFun -> Term) -> ConvFun -> Term
forall a b. (a -> b) -> a -> b
$ FunType -> FunType -> ConvFun
instType FunType
fTy FunType
instfTy)
            unCurry :: VName -> IsaTermCond
unCurry f :: VName
f = let rf :: Term
rf = Term -> Term -> Term
termAppl Term
uncurryOp (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ VName -> Term
con VName
f in
              FunType -> Term -> Cond -> IsaTermCond
ITC FunType
fTy Term
rf Cond
None
        IsaTermCond -> Result IsaTermCond
forall (m :: * -> *) a. Monad m => a -> m a
return (IsaTermCond -> Result IsaTermCond)
-> IsaTermCond -> Result IsaTermCond
forall a b. (a -> b) -> a -> b
$ case (Id
opId Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
==) of
          is :: Id -> Bool
is | Id -> Bool
is Id
trueId -> FunType -> Term -> Cond -> IsaTermCond
ITC FunType
fTy Term
true Cond
None
              | Id -> Bool
is Id
falseId -> FunType -> Term -> Cond -> IsaTermCond
ITC FunType
fTy Term
false Cond
None
              | Id -> Bool
is Id
botId -> case FunType
instfTy of
                  PartialVal t :: FunType
t -> FunType -> Term -> Cond -> IsaTermCond
ITC FunType
t (Term -> Term -> Term
termAppl Term
makeTotal Term
noneOp) (Cond -> IsaTermCond) -> Cond -> IsaTermCond
forall a b. (a -> b) -> a -> b
$ Term -> Cond
Cond Term
false
                  _ -> FunType -> Term -> Cond -> IsaTermCond
ITC FunType
instfTy (Term -> Term
cf Term
noneOp) Cond
None
              | Id -> Bool
is Id
andId -> VName -> IsaTermCond
unCurry VName
conjV
              | Id -> Bool
is Id
orId -> VName -> IsaTermCond
unCurry VName
disjV
              | Id -> Bool
is Id
implId -> VName -> IsaTermCond
unCurry VName
implV
              | Id -> Bool
is Id
infixIf -> FunType -> Term -> Cond -> IsaTermCond
ITC FunType
fTy Term
ifImplOp Cond
None
              | Id -> Bool
is Id
eqvId -> VName -> IsaTermCond
unCurry VName
eqV
              | Id -> Bool
is Id
exEq -> let
                  ef :: Term
ef = Term -> Term
cf (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
termAppl Term
uncurryOp Term
existEqualOp
                  in FunType -> Term -> Cond -> IsaTermCond
ITC FunType
instfTy Term
ef Cond
None
              | Id -> Bool
is Id
eqId -> let
                  ef :: Term
ef = Term -> Term
cf (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
termAppl Term
uncurryOp (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ VName -> Term
con VName
eqV
                  in FunType -> Term -> Cond -> IsaTermCond
ITC FunType
instfTy Term
ef Cond
None
              | Id -> Bool
is Id
notId -> FunType -> Term -> Cond -> IsaTermCond
ITC FunType
fTy Term
notOp Cond
None
              | Id -> Bool
is Id
defId -> FunType -> Term -> Cond -> IsaTermCond
ITC FunType
instfTy (Term -> Term
cf Term
defOp) Cond
None
              | Id -> Bool
is Id
whenElse -> FunType -> Term -> Cond -> IsaTermCond
ITC FunType
instfTy (Term -> Term
cf Term
whenElseOp) Cond
None
              | Id -> Bool
is Id
resId -> FunType -> Term -> Cond -> IsaTermCond
ITC FunType
instfTy (Term -> Term
cf Term
resOp) Cond
None
          _ -> let
                  isaId :: VName
isaId = Env -> Set String -> Id -> TypeScheme -> VName
transOpId Env
sign Set String
tyToks Id
opId TypeScheme
ts
                  ef :: Term
ef = Term -> Term
cf (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Int -> (Term -> Term) -> Term -> Term
forall a. Int -> (a -> a) -> a -> a
for (FunType -> Int
isPlainFunType FunType
fTy Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) (Term -> Term -> Term
termAppl Term
uncurryOp)
                             (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ if Id -> [Id] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Id
opId [Id
injName, Id
projName] then
                                   VName -> FunType -> Term
mkTypedConst VName
isaId FunType
instfTy
                               else VName -> Term
con VName
isaId
                  in FunType -> Term -> Cond -> IsaTermCond
ITC FunType
instfTy Term
ef Cond
None
    QuantifiedTerm quan :: Quantifier
quan varDecls :: [GenVarDecl]
varDecls phi :: Term
phi _ -> do
        let qname :: String
qname = case Quantifier
quan of
                      Universal -> String
allS
                      Existential -> String
exS
                      Unique -> String
ex1S
            quantify :: Term -> GenVarDecl -> Result Term
quantify phi' :: Term
phi' gvd :: GenVarDecl
gvd = case GenVarDecl
gvd of
                GenVarDecl vd :: VarDecl
vd -> do
                    Term
vt <- Set String -> VarDecl -> Result Term
transTypedVar Set String
toks VarDecl
vd
                    Term -> Result Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Result Term) -> Term -> Result Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
termAppl (String -> Term
conDouble String
qname) (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Continuity -> Term
Abs Term
vt Term
phi' Continuity
NotCont
                GenTypeVarDecl _ -> Term -> Result Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
phi'
        ITC ty :: FunType
ty psi :: Term
psi cs :: Cond
cs <- (IsaTermCond -> IsaTermCond)
-> Result IsaTermCond -> Result IsaTermCond
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap IsaTermCond -> IsaTermCond
integrateCond
          (Result IsaTermCond -> Result IsaTermCond)
-> Result IsaTermCond -> Result IsaTermCond
forall a b. (a -> b) -> a -> b
$ Env
-> Set String
-> Bool
-> Set String
-> Set VarDecl
-> Term
-> Result IsaTermCond
transTerm Env
sign Set String
tyToks Bool
collectConds Set String
toks Set VarDecl
pVars Term
phi
        Term
psiR <- (Term -> GenVarDecl -> Result Term)
-> Term -> [GenVarDecl] -> Result Term
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Term -> GenVarDecl -> Result Term
quantify Term
psi ([GenVarDecl] -> Result Term) -> [GenVarDecl] -> Result Term
forall a b. (a -> b) -> a -> b
$ [GenVarDecl] -> [GenVarDecl]
forall a. [a] -> [a]
reverse [GenVarDecl]
varDecls
        IsaTermCond -> Result IsaTermCond
forall (m :: * -> *) a. Monad m => a -> m a
return (IsaTermCond -> Result IsaTermCond)
-> IsaTermCond -> Result IsaTermCond
forall a b. (a -> b) -> a -> b
$ FunType -> Term -> Cond -> IsaTermCond
ITC FunType
ty Term
psiR Cond
cs
    TypedTerm t :: Term
t _q :: TypeQual
_q _ty :: Type
_ty _ -> Env
-> Set String
-> Bool
-> Set String
-> Set VarDecl
-> Term
-> Result IsaTermCond
transTerm Env
sign Set String
tyToks Bool
collectConds Set String
toks Set VarDecl
pVars Term
t
    LambdaTerm pats :: [Term]
pats q :: Partiality
q body :: Term
body r :: Range
r -> do
        p :: IsaTermCond
p@(ITC ty :: FunType
ty _ ncs :: Cond
ncs) <- Env
-> Set String
-> Bool
-> Set String
-> Set VarDecl
-> Term
-> Result IsaTermCond
transTerm Env
sign Set String
tyToks Bool
collectConds Set String
toks Set VarDecl
pVars Term
body
        [Diagnosis] -> Result ()
appendDiags ([Diagnosis] -> Result ()) -> [Diagnosis] -> Result ()
forall a b. (a -> b) -> a -> b
$ case Partiality
q of
            Partial -> []
            Total -> [DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Warning
              ("partial lambda body in total abstraction: "
               String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Term
body "") Range
r
                  | FunType -> Bool
isPartialVal FunType
ty Bool -> Bool -> Bool
|| Bool -> Bool
not (Term -> Bool
isTrue (Term -> Bool) -> Term -> Bool
forall a b. (a -> b) -> a -> b
$ Cond -> Term
cond2bool Cond
ncs) ]
        (IsaTermCond -> Term -> Result IsaTermCond)
-> IsaTermCond -> [Term] -> Result IsaTermCond
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (Env
-> Set String
-> Set String
-> IsaTermCond
-> Term
-> Result IsaTermCond
abstraction Env
sign Set String
tyToks Set String
toks) (IsaTermCond -> IsaTermCond
integrateCond IsaTermCond
p)
          ([Term] -> Result IsaTermCond) -> [Term] -> Result IsaTermCond
forall a b. (a -> b) -> a -> b
$ [Term] -> [Term]
forall a. [a] -> [a]
reverse [Term]
pats
    LetTerm As.Let peqs :: [ProgEq]
peqs body :: Term
body _ -> do
        (nPVars :: Set VarDecl
nPVars, nEqs :: [(Term, IsaTermCond)]
nEqs) <-
            Env
-> Set String
-> Bool
-> Set String
-> Set VarDecl
-> [ProgEq]
-> Result (Set VarDecl, [(Term, IsaTermCond)])
transLetEqs Env
sign Set String
tyToks Bool
collectConds Set String
toks Set VarDecl
pVars [ProgEq]
peqs
        ITC bTy :: FunType
bTy bTrm :: Term
bTrm defCs :: Cond
defCs <-
          Env
-> Set String
-> Bool
-> Set String
-> Set VarDecl
-> Term
-> Result IsaTermCond
transTerm Env
sign Set String
tyToks Bool
collectConds Set String
toks Set VarDecl
nPVars Term
body
        let pEs :: [(Term, Term)]
pEs = ((Term, IsaTermCond) -> (Term, Term))
-> [(Term, IsaTermCond)] -> [(Term, Term)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (p :: Term
p, ITC _ t :: Term
t _) -> (Term
p, Term
t)) [(Term, IsaTermCond)]
nEqs
            cs :: Cond
cs = (Cond -> Cond -> Cond) -> Cond -> [Cond] -> Cond
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Cond -> Cond -> Cond
joinCond Cond
None ([Cond] -> Cond) -> [Cond] -> Cond
forall a b. (a -> b) -> a -> b
$ ((Term, IsaTermCond) -> Cond) -> [(Term, IsaTermCond)] -> [Cond]
forall a b. (a -> b) -> [a] -> [b]
map (\ (_, ITC _ _ c :: Cond
c) -> Cond
c) [(Term, IsaTermCond)]
nEqs
        IsaTermCond -> Result IsaTermCond
forall (m :: * -> *) a. Monad m => a -> m a
return (IsaTermCond -> Result IsaTermCond)
-> IsaTermCond -> Result IsaTermCond
forall a b. (a -> b) -> a -> b
$ FunType -> Term -> Cond -> IsaTermCond
ITC FunType
bTy ([(Term, Term)] -> Term -> Term
mkLetAppl [(Term, Term)]
pEs Term
bTrm) (Cond -> IsaTermCond) -> Cond -> IsaTermCond
forall a b. (a -> b) -> a -> b
$ Cond -> Cond -> Cond
joinCond Cond
cs Cond
defCs
    TupleTerm ts :: [Term]
ts@(_ : _) _ -> do
        [IsaTermCond]
nTs <- (Term -> Result IsaTermCond) -> [Term] -> Result [IsaTermCond]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Env
-> Set String
-> Bool
-> Set String
-> Set VarDecl
-> Term
-> Result IsaTermCond
transTerm Env
sign Set String
tyToks Bool
collectConds Set String
toks Set VarDecl
pVars) [Term]
ts
        IsaTermCond -> Result IsaTermCond
forall (m :: * -> *) a. Monad m => a -> m a
return (IsaTermCond -> Result IsaTermCond)
-> IsaTermCond -> Result IsaTermCond
forall a b. (a -> b) -> a -> b
$ (IsaTermCond -> IsaTermCond -> IsaTermCond)
-> [IsaTermCond] -> IsaTermCond
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 ( \ (ITC s :: FunType
s p :: Term
p cs :: Cond
cs) (ITC t :: FunType
t e :: Term
e cr :: Cond
cr) ->
          FunType -> Term -> Cond -> IsaTermCond
ITC (FunType -> FunType -> FunType
PairType FunType
s FunType
t) ([Term] -> Continuity -> Term
Tuplex [Term
p, Term
e] Continuity
NotCont) (Cond -> IsaTermCond) -> Cond -> IsaTermCond
forall a b. (a -> b) -> a -> b
$ Cond -> Cond -> Cond
pairCond Cond
cs Cond
cr) [IsaTermCond]
nTs
    TupleTerm [] _ -> IsaTermCond -> Result IsaTermCond
forall (m :: * -> *) a. Monad m => a -> m a
return (IsaTermCond -> Result IsaTermCond)
-> IsaTermCond -> Result IsaTermCond
forall a b. (a -> b) -> a -> b
$ FunType -> Term -> Cond -> IsaTermCond
ITC FunType
UnitType Term
unitOp Cond
None
    ApplTerm t1 :: Term
t1 t2 :: Term
t2 _ -> Env
-> Set String
-> Bool
-> Set String
-> Set VarDecl
-> Term
-> Term
-> Result IsaTermCond
mkApp Env
sign Set String
tyToks Bool
collectConds Set String
toks Set VarDecl
pVars Term
t1 Term
t2
    _ -> String -> Range -> Result IsaTermCond
forall a. String -> Range -> Result a
fatal_error ("cannot translate term: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Term
trm "")
         (Range -> Result IsaTermCond) -> Range -> Result IsaTermCond
forall a b. (a -> b) -> a -> b
$ Term -> Range
forall a. GetRange a => a -> Range
getRange Term
trm

integrateCond :: IsaTermCond -> IsaTermCond
integrateCond :: IsaTermCond -> IsaTermCond
integrateCond (ITC ty :: FunType
ty trm :: Term
trm cs :: Cond
cs) = if Term -> Bool
isTrue (Term -> Bool) -> Term -> Bool
forall a b. (a -> b) -> a -> b
$ Cond -> Term
cond2bool Cond
cs then
  FunType -> Term -> Cond -> IsaTermCond
ITC FunType
ty Term
trm Cond
None
  else case FunType
ty of
    PartialVal _ -> FunType -> Term -> Cond -> IsaTermCond
ITC FunType
ty (Term -> Term -> Term
mkTermAppl (Cond -> Term
integrateCondInPartial Cond
cs) Term
trm) Cond
None
    BoolType -> FunType -> Term -> Cond -> IsaTermCond
ITC FunType
ty (Term -> Term -> Term
mkTermAppl (Cond -> Term
integrateCondInBool Cond
cs) Term
trm) Cond
None
    UnitType -> FunType -> Term -> Cond -> IsaTermCond
ITC FunType
BoolType (Cond -> Term
cond2bool Cond
cs) Cond
None
    _ -> FunType -> Term -> Cond -> IsaTermCond
ITC (FunType -> FunType
makePartialVal FunType
ty)
         (Term -> Term -> Term
mkTermAppl (Cond -> Term
integrateCondInTotal Cond
cs) Term
trm) Cond
None
    -- return partial result type

instType :: FunType -> FunType -> ConvFun
instType :: FunType -> FunType -> ConvFun
instType f1 :: FunType
f1 f2 :: FunType
f2 = case (FunType
f1, FunType
f2) of
    (TupleType l1 :: [FunType]
l1, _) -> FunType -> FunType -> ConvFun
instType ((FunType -> FunType -> FunType) -> [FunType] -> FunType
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 FunType -> FunType -> FunType
PairType [FunType]
l1) FunType
f2
    (_, TupleType l2 :: [FunType]
l2) -> FunType -> FunType -> ConvFun
instType FunType
f1 (FunType -> ConvFun) -> FunType -> ConvFun
forall a b. (a -> b) -> a -> b
$ (FunType -> FunType -> FunType) -> [FunType] -> FunType
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 FunType -> FunType -> FunType
PairType [FunType]
l2
    (PartialVal (TypeVar _), BoolType) -> Bool -> ConvFun
Partial2bool Bool
True
    (PairType a :: FunType
a c :: FunType
c, PairType b :: FunType
b d :: FunType
d) ->
        let c2 :: ConvFun
c2 = FunType -> FunType -> ConvFun
instType FunType
c FunType
d
            c1 :: ConvFun
c1 = FunType -> FunType -> ConvFun
instType FunType
a FunType
b
        in ConvFun -> ConvFun -> ConvFun
mkCompFun (MapFun -> ConvFun -> ConvFun
mkMapFun MapFun
MapSnd ConvFun
c2) (ConvFun -> ConvFun) -> ConvFun -> ConvFun
forall a b. (a -> b) -> a -> b
$ MapFun -> ConvFun -> ConvFun
mkMapFun MapFun
MapFst ConvFun
c1
    (FunType a :: FunType
a c :: FunType
c, FunType b :: FunType
b d :: FunType
d) ->
         let c2 :: ConvFun
c2 = FunType -> FunType -> ConvFun
instType FunType
c FunType
d
             c1 :: ConvFun
c1 = FunType -> FunType -> ConvFun
instType FunType
a FunType
b
        in ConvFun -> ConvFun -> ConvFun
mkCompFun (ConvFun -> ConvFun
mkResFun ConvFun
c2) (ConvFun -> ConvFun) -> ConvFun -> ConvFun
forall a b. (a -> b) -> a -> b
$ ConvFun -> ConvFun
mkArgFun (ConvFun -> ConvFun) -> ConvFun -> ConvFun
forall a b. (a -> b) -> a -> b
$ ConvFun -> ConvFun
invertConv ConvFun
c1
    _ -> ConvFun
IdOp

invertConv :: ConvFun -> ConvFun
invertConv :: ConvFun -> ConvFun
invertConv c :: ConvFun
c = case ConvFun
c of
    Partial2bool _ -> Bool -> ConvFun
Bool2partial Bool
False
    Bool2partial _ -> Bool -> ConvFun
Partial2bool Bool
False
    Unit2bool _ -> ConvFun
Bool2unit
    Bool2unit -> Bool -> ConvFun
Unit2bool Bool
False
    MkPartial _ -> ConvFun
MkTotal
    MkTotal -> Bool -> ConvFun
MkPartial Bool
False
    MapFun mv :: MapFun
mv cf :: ConvFun
cf -> MapFun -> ConvFun -> ConvFun
mkMapFun MapFun
mv (ConvFun -> ConvFun) -> ConvFun -> ConvFun
forall a b. (a -> b) -> a -> b
$ ConvFun -> ConvFun
invertConv ConvFun
cf
    ResFun cf :: ConvFun
cf -> ConvFun -> ConvFun
mkResFun (ConvFun -> ConvFun) -> ConvFun -> ConvFun
forall a b. (a -> b) -> a -> b
$ ConvFun -> ConvFun
invertConv ConvFun
cf
    ArgFun cf :: ConvFun
cf -> ConvFun -> ConvFun
mkArgFun (ConvFun -> ConvFun) -> ConvFun -> ConvFun
forall a b. (a -> b) -> a -> b
$ ConvFun -> ConvFun
invertConv ConvFun
cf
    CompFun c1 :: ConvFun
c1 c2 :: ConvFun
c2 -> ConvFun -> ConvFun -> ConvFun
mkCompFun (ConvFun -> ConvFun
invertConv ConvFun
c2) (ConvFun -> ConvFun
invertConv ConvFun
c1)
    _ -> ConvFun
IdOp

data MapFun = MapFst | MapSnd | MapPartial deriving Int -> MapFun -> String -> String
[MapFun] -> String -> String
MapFun -> String
(Int -> MapFun -> String -> String)
-> (MapFun -> String)
-> ([MapFun] -> String -> String)
-> Show MapFun
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [MapFun] -> String -> String
$cshowList :: [MapFun] -> String -> String
show :: MapFun -> String
$cshow :: MapFun -> String
showsPrec :: Int -> MapFun -> String -> String
$cshowsPrec :: Int -> MapFun -> String -> String
Show

data LiftFun = LiftFst | LiftSnd deriving Int -> LiftFun -> String -> String
[LiftFun] -> String -> String
LiftFun -> String
(Int -> LiftFun -> String -> String)
-> (LiftFun -> String)
-> ([LiftFun] -> String -> String)
-> Show LiftFun
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [LiftFun] -> String -> String
$cshowList :: [LiftFun] -> String -> String
show :: LiftFun -> String
$cshow :: LiftFun -> String
showsPrec :: Int -> LiftFun -> String -> String
$cshowsPrec :: Int -> LiftFun -> String -> String
Show

{- the additional Bool indicates condition integration
   Bool2bool and Partial2partial must be mapped to IdOp
   if the conditions should be ignored.
   Bool2Unit and MkTotal can propagate out conditions -}
data ConvFun =
    IdOp
  | Bool2partial Bool
  | Partial2bool Bool
  | Bool2bool
  | Unit2bool Bool
  | Bool2unit
  | Partial2partial
  | MkPartial Bool
  | MkTotal
  | CompFun ConvFun ConvFun
  | MapFun MapFun ConvFun
  | LiftFun LiftFun ConvFun
  | LiftUnit FunType
  | LiftPartial FunType
  | ResFun ConvFun
  | ArgFun ConvFun
    deriving Int -> ConvFun -> String -> String
[ConvFun] -> String -> String
ConvFun -> String
(Int -> ConvFun -> String -> String)
-> (ConvFun -> String)
-> ([ConvFun] -> String -> String)
-> Show ConvFun
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [ConvFun] -> String -> String
$cshowList :: [ConvFun] -> String -> String
show :: ConvFun -> String
$cshow :: ConvFun -> String
showsPrec :: Int -> ConvFun -> String -> String
$cshowsPrec :: Int -> ConvFun -> String -> String
Show

isNotIdOp :: ConvFun -> Bool
isNotIdOp :: ConvFun -> Bool
isNotIdOp f :: ConvFun
f = case ConvFun
f of
    IdOp -> Bool
False
    _ -> Bool
True

mkCompFun :: ConvFun -> ConvFun -> ConvFun
mkCompFun :: ConvFun -> ConvFun -> ConvFun
mkCompFun f1 :: ConvFun
f1 f2 :: ConvFun
f2 = case ConvFun
f1 of
    IdOp -> ConvFun
f2
    _ -> case ConvFun
f2 of
           IdOp -> ConvFun
f1
           _ -> ConvFun -> ConvFun -> ConvFun
CompFun ConvFun
f1 ConvFun
f2

mkMapFun :: MapFun -> ConvFun -> ConvFun
mkMapFun :: MapFun -> ConvFun -> ConvFun
mkMapFun m :: MapFun
m f :: ConvFun
f = case ConvFun
f of
    IdOp -> ConvFun
IdOp
    _ -> MapFun -> ConvFun -> ConvFun
MapFun MapFun
m ConvFun
f

mkLiftFun :: LiftFun -> ConvFun -> ConvFun
mkLiftFun :: LiftFun -> ConvFun -> ConvFun
mkLiftFun lv :: LiftFun
lv c :: ConvFun
c = case ConvFun
c of
    IdOp -> ConvFun
IdOp
    _ -> LiftFun -> ConvFun -> ConvFun
LiftFun LiftFun
lv ConvFun
c

mapFun :: MapFun -> Isa.Term
mapFun :: MapFun -> Term
mapFun mf :: MapFun
mf = case MapFun
mf of
    MapFst -> Term
mapFst
    MapSnd -> Term
mapSnd
    MapPartial -> Term
mapPartial

compOp :: Isa.Term
compOp :: Term
compOp = VName -> Term
con VName
compV

convFun :: Cond -> ConvFun -> Isa.Term
convFun :: Cond -> ConvFun -> Term
convFun cnd :: Cond
cnd cvf :: ConvFun
cvf = case ConvFun
cvf of
    IdOp -> Term
idOp
    Bool2partial b :: Bool
b -> if Bool
b
      then Term -> Term -> Term
metaComp Term
bool2partial (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Cond -> Term
integrateCondInBool Cond
cnd
      else Term
bool2partial
    Partial2bool b :: Bool
b -> if Bool
b
      then Term -> Term -> Term
metaComp (Cond -> Term
integrateCondInBool Cond
cnd) Term
defOp
      else Term
defOp
    Bool2bool -> Cond -> Term
integrateCondInBool Cond
cnd
    Unit2bool b :: Bool
b -> if Bool
b
      then Term -> Term -> Term
metaComp (Cond -> Term
integrateCondInBool Cond
cnd) Term
constTrue else Term
constTrue
    Bool2unit -> Term
constNil
    Partial2partial -> Cond -> Term
integrateCondInPartial Cond
cnd
    MkPartial b :: Bool
b -> if Bool
b
      then Cond -> Term
integrateCondInTotal Cond
cnd
      else Term
mkPartial
    MkTotal -> Term
makeTotal
    LiftUnit rTy :: FunType
rTy -> case FunType
rTy of
       UnitType -> Term
liftUnit2unit
       BoolType -> Term
liftUnit2bool
       PartialVal _ -> Term
liftUnit2partial
       _ -> Term
liftUnit
    LiftPartial rTy :: FunType
rTy ->
        case FunType
rTy of
            UnitType -> Term
lift2unit
            BoolType -> Term
lift2bool
            PartialVal _ -> Term
lift2partial
            _ -> Term
mapPartial
    CompFun f1 :: ConvFun
f1 f2 :: ConvFun
f2 -> Term -> Term -> Term
metaComp (Cond -> ConvFun -> Term
convFun Cond
cnd ConvFun
f1) (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Cond -> ConvFun -> Term
convFun Cond
cnd ConvFun
f2
    MapFun mf :: MapFun
mf cv :: ConvFun
cv -> Term -> Term -> Term
mkTermAppl (MapFun -> Term
mapFun MapFun
mf) (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Cond -> ConvFun -> Term
convFun Cond
cnd ConvFun
cv
    LiftFun lf :: LiftFun
lf cv :: ConvFun
cv -> let ccv :: Term
ccv = Cond -> ConvFun -> Term
convFun Cond
cnd ConvFun
cv in case LiftFun
lf of
        LiftFst -> Term -> Term -> Term
metaComp (Term -> Term -> Term
metaComp Term
uncurryOp Term
flipOp)
                   (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
metaComp (Term -> Term -> Term
metaComp (Term -> Term -> Term
mkTermAppl Term
compOp Term
ccv) Term
flipOp)
                   Term
curryOp
        LiftSnd -> Term -> Term -> Term
metaComp Term
uncurryOp (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
metaComp (Term -> Term -> Term
mkTermAppl Term
compOp Term
ccv)
                   Term
curryOp
    ArgFun cv :: ConvFun
cv -> Term -> Term -> Term
mkTermAppl (Term -> Term -> Term
termAppl Term
flipOp Term
compOp) (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Cond -> ConvFun -> Term
convFun Cond
cnd ConvFun
cv
    ResFun cv :: ConvFun
cv -> Term -> Term -> Term
mkTermAppl Term
compOp (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Cond -> ConvFun -> Term
convFun Cond
cnd ConvFun
cv

mapFst, mapSnd, mapPartial, idOp, bool2partial, constNil, constTrue,
    liftUnit2unit, liftUnit2bool, liftUnit2partial, liftUnit, lift2unit,
    lift2bool, lift2partial, mkPartial, restrict :: Isa.Term

mapFst :: Term
mapFst = String -> Term
conDouble "mapFst"
mapSnd :: Term
mapSnd = String -> Term
conDouble "mapSnd"
mapPartial :: Term
mapPartial = String -> Term
conDouble "mapPartial"
idOp :: Term
idOp = String -> Term
conDouble "id"
bool2partial :: Term
bool2partial = String -> Term
conDouble "bool2partial"
constNil :: Term
constNil = String -> Term
conDouble "constNil"
constTrue :: Term
constTrue = String -> Term
conDouble "constTrue"
liftUnit2unit :: Term
liftUnit2unit = String -> Term
conDouble "liftUnit2unit"
liftUnit2bool :: Term
liftUnit2bool = String -> Term
conDouble "liftUnit2bool"
liftUnit2partial :: Term
liftUnit2partial = String -> Term
conDouble "liftUnit2partial"
liftUnit :: Term
liftUnit = String -> Term
conDouble "liftUnit"
lift2unit :: Term
lift2unit = String -> Term
conDouble "lift2unit"
lift2bool :: Term
lift2bool = String -> Term
conDouble "lift2bool"
lift2partial :: Term
lift2partial = String -> Term
conDouble "lift2partial"
mkPartial :: Term
mkPartial = String -> Term
conDouble "makePartial"
restrict :: Term
restrict = String -> Term
conDouble "restrictOp"

existEqualOp :: Isa.Term
existEqualOp :: Term
existEqualOp =
  VName -> Term
con (VName -> Term) -> VName -> Term
forall a b. (a -> b) -> a -> b
$ String -> Maybe AltSyntax -> VName
VName "existEqualOp" (Maybe AltSyntax -> VName) -> Maybe AltSyntax -> VName
forall a b. (a -> b) -> a -> b
$ AltSyntax -> Maybe AltSyntax
forall a. a -> Maybe a
Just (AltSyntax -> Maybe AltSyntax) -> AltSyntax -> Maybe AltSyntax
forall a b. (a -> b) -> a -> b
$ String -> [Int] -> Int -> AltSyntax
AltSyntax "(_ =e=/ _)" [50, 51] 50

integrateCondInBool :: Cond -> Isa.Term
integrateCondInBool :: Cond -> Term
integrateCondInBool c :: Cond
c = let b :: Term
b = Cond -> Term
cond2bool Cond
c in
  if Term -> Bool
isTrue Term
b then Term
idOp else Term -> Term -> Term
mkTermAppl (VName -> Term
con VName
conjV) Term
b

integrateCondInPartial :: Cond -> Isa.Term
integrateCondInPartial :: Cond -> Term
integrateCondInPartial c :: Cond
c = let b :: Term
b = Cond -> Term
cond2bool Cond
c in
  if Term -> Bool
isTrue Term
b then Term
idOp else
  Term -> Term -> Term
mkTermAppl (Term -> Term -> Term
mkTermAppl Term
flipOp Term
restrict) Term
b

metaComp :: Isa.Term -> Isa.Term -> Isa.Term
metaComp :: Term -> Term -> Term
metaComp = Term -> Term -> Term
mkTermAppl (Term -> Term -> Term) -> (Term -> Term) -> Term -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Term -> Term
mkTermAppl Term
compOp

integrateCondInTotal :: Cond -> Isa.Term
integrateCondInTotal :: Cond -> Term
integrateCondInTotal c :: Cond
c = Term -> Term -> Term
metaComp (Cond -> Term
integrateCondInPartial Cond
c) Term
mkPartial

addCond :: Isa.Term -> Cond -> Cond
addCond :: Term -> Cond -> Cond
addCond = Cond -> Cond -> Cond
joinCond (Cond -> Cond -> Cond) -> (Term -> Cond) -> Term -> Cond -> Cond
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Cond
Cond

cond2bool :: Cond -> Isa.Term
cond2bool :: Cond -> Term
cond2bool c :: Cond
c = case [Term] -> [Term]
forall a. Eq a => [a] -> [a]
nub ([Term] -> [Term]) -> [Term] -> [Term]
forall a b. (a -> b) -> a -> b
$ Cond -> [Term]
condToList Cond
c of
  [] -> Term
true
  ncs :: [Term]
ncs -> (Term -> Term -> Term) -> [Term] -> Term
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Term -> Term -> Term
mkBinConj [Term]
ncs

{- adjust actual argument to expected argument type of function
considering a definedness conditions -}
adjustArgType :: FunType -> FunType -> Result ConvFun
adjustArgType :: FunType -> FunType -> Result ConvFun
adjustArgType aTy :: FunType
aTy ty :: FunType
ty = case (FunType
aTy, FunType
ty) of
    (TupleType l :: [FunType]
l, _) -> FunType -> FunType -> Result ConvFun
adjustArgType ((FunType -> FunType -> FunType) -> [FunType] -> FunType
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 FunType -> FunType -> FunType
PairType [FunType]
l) FunType
ty
    (_, TupleType l :: [FunType]
l) -> FunType -> FunType -> Result ConvFun
adjustArgType FunType
aTy (FunType -> Result ConvFun) -> FunType -> Result ConvFun
forall a b. (a -> b) -> a -> b
$ (FunType -> FunType -> FunType) -> [FunType] -> FunType
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 FunType -> FunType -> FunType
PairType [FunType]
l
    (BoolType, BoolType) -> ConvFun -> Result ConvFun
forall (m :: * -> *) a. Monad m => a -> m a
return ConvFun
Bool2bool
    (UnitType, UnitType) -> ConvFun -> Result ConvFun
forall (m :: * -> *) a. Monad m => a -> m a
return ConvFun
IdOp
    (PartialVal UnitType, BoolType) -> ConvFun -> Result ConvFun
forall (m :: * -> *) a. Monad m => a -> m a
return (ConvFun -> Result ConvFun) -> ConvFun -> Result ConvFun
forall a b. (a -> b) -> a -> b
$ Bool -> ConvFun
Bool2partial Bool
True
    (BoolType, PartialVal UnitType) -> ConvFun -> Result ConvFun
forall (m :: * -> *) a. Monad m => a -> m a
return (ConvFun -> Result ConvFun) -> ConvFun -> Result ConvFun
forall a b. (a -> b) -> a -> b
$ Bool -> ConvFun
Partial2bool Bool
True
    (UnitType, BoolType) -> ConvFun -> Result ConvFun
forall (m :: * -> *) a. Monad m => a -> m a
return ConvFun
Bool2unit
    (BoolType, UnitType) -> ConvFun -> Result ConvFun
forall (m :: * -> *) a. Monad m => a -> m a
return (ConvFun -> Result ConvFun) -> ConvFun -> Result ConvFun
forall a b. (a -> b) -> a -> b
$ Bool -> ConvFun
Unit2bool Bool
True
    (PartialVal a :: FunType
a, PartialVal b :: FunType
b) -> do
        ConvFun
c <- FunType -> FunType -> Result ConvFun
adjustArgType FunType
a FunType
b
        ConvFun -> Result ConvFun
forall (m :: * -> *) a. Monad m => a -> m a
return (ConvFun -> Result ConvFun) -> ConvFun -> Result ConvFun
forall a b. (a -> b) -> a -> b
$ ConvFun -> ConvFun -> ConvFun
mkCompFun ConvFun
Partial2partial ConvFun
c
    (a :: FunType
a, PartialVal b :: FunType
b) -> do
        ConvFun
c <- FunType -> FunType -> Result ConvFun
adjustArgType FunType
a FunType
b
        ConvFun -> Result ConvFun
forall (m :: * -> *) a. Monad m => a -> m a
return (ConvFun -> Result ConvFun) -> ConvFun -> Result ConvFun
forall a b. (a -> b) -> a -> b
$ ConvFun -> ConvFun -> ConvFun
mkCompFun ConvFun
MkTotal ConvFun
c
    (PartialVal a :: FunType
a, b :: FunType
b) -> do
        ConvFun
c <- FunType -> FunType -> Result ConvFun
adjustArgType FunType
a FunType
b
        ConvFun -> Result ConvFun
forall (m :: * -> *) a. Monad m => a -> m a
return (ConvFun -> Result ConvFun) -> ConvFun -> Result ConvFun
forall a b. (a -> b) -> a -> b
$ ConvFun -> ConvFun -> ConvFun
mkCompFun (Bool -> ConvFun
MkPartial Bool
True) ConvFun
c
    (PairType e1 :: FunType
e1 e2 :: FunType
e2, PairType a1 :: FunType
a1 a2 :: FunType
a2) -> do
        ConvFun
c1 <- FunType -> FunType -> Result ConvFun
adjustArgType FunType
e1 FunType
a1
        ConvFun
c2 <- FunType -> FunType -> Result ConvFun
adjustArgType FunType
e2 FunType
a2
        ConvFun -> Result ConvFun
forall (m :: * -> *) a. Monad m => a -> m a
return (ConvFun -> Result ConvFun)
-> (ConvFun -> ConvFun) -> ConvFun -> Result ConvFun
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConvFun -> ConvFun -> ConvFun
mkCompFun (MapFun -> ConvFun -> ConvFun
mkMapFun MapFun
MapSnd ConvFun
c2) (ConvFun -> Result ConvFun) -> ConvFun -> Result ConvFun
forall a b. (a -> b) -> a -> b
$ MapFun -> ConvFun -> ConvFun
mkMapFun MapFun
MapFst ConvFun
c1
    (FunType a :: FunType
a b :: FunType
b, FunType c :: FunType
c d :: FunType
d) -> do
        ConvFun
aC <- FunType -> FunType -> Result ConvFun
adjustArgType FunType
a FunType
c -- function a -> c (a fixed)
        ConvFun
dC <- FunType -> FunType -> Result ConvFun
adjustArgType FunType
b FunType
d -- function d -> b (b fixed)

        {- (d -> b) o (c -> d) o (a -> c) :: a -> b
        do not integrate cond treatment via invertConv . invertConv -}
        ConvFun -> Result ConvFun
forall (m :: * -> *) a. Monad m => a -> m a
return (ConvFun -> Result ConvFun)
-> (ConvFun -> ConvFun) -> ConvFun -> Result ConvFun
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConvFun -> ConvFun -> ConvFun
mkCompFun (ConvFun -> ConvFun
mkResFun (ConvFun -> ConvFun) -> (ConvFun -> ConvFun) -> ConvFun -> ConvFun
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConvFun -> ConvFun
invertConv (ConvFun -> ConvFun) -> ConvFun -> ConvFun
forall a b. (a -> b) -> a -> b
$ ConvFun -> ConvFun
invertConv ConvFun
dC)
          (ConvFun -> ConvFun) -> (ConvFun -> ConvFun) -> ConvFun -> ConvFun
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConvFun -> ConvFun
mkArgFun (ConvFun -> Result ConvFun) -> ConvFun -> Result ConvFun
forall a b. (a -> b) -> a -> b
$ ConvFun -> ConvFun
invertConv ConvFun
aC
    (TypeVar _, _) -> ConvFun -> Result ConvFun
forall (m :: * -> *) a. Monad m => a -> m a
return ConvFun
IdOp
    (_, TypeVar _) -> ConvFun -> Result ConvFun
forall (m :: * -> *) a. Monad m => a -> m a
return ConvFun
IdOp
    (ApplType i1 :: Id
i1 l1 :: [FunType]
l1, ApplType i2 :: Id
i2 l2 :: [FunType]
l2) | Id
i1 Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
i2 Bool -> Bool -> Bool
&& [FunType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [FunType]
l1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [FunType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [FunType]
l2 -> do
      [ConvFun]
l <- (FunType -> FunType -> Result ConvFun)
-> [FunType] -> [FunType] -> Result [ConvFun]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM FunType -> FunType -> Result ConvFun
adjustArgType [FunType]
l1 [FunType]
l2
      if (ConvFun -> Bool) -> [ConvFun] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (ConvFun -> Bool
isNotIdOp (ConvFun -> Bool) -> (ConvFun -> ConvFun) -> ConvFun -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConvFun -> ConvFun
invertConv) [ConvFun]
l
        then String -> Result ConvFun
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "cannot adjust type application"
        else ConvFun -> Result ConvFun
forall (m :: * -> *) a. Monad m => a -> m a
return ConvFun
IdOp
    _ -> String -> Result ConvFun
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result ConvFun) -> String -> Result ConvFun
forall a b. (a -> b) -> a -> b
$ "cannot adjust argument type\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (FunType, FunType) -> String
forall a. Show a => a -> String
show (FunType
aTy, FunType
ty)

unpackOp :: Isa.Term -> Bool -> Bool -> FunType -> ConvFun -> Isa.Term
unpackOp :: Term -> Bool -> Bool -> FunType -> ConvFun -> Term
unpackOp fTrm :: Term
fTrm isPf :: Bool
isPf pfTy :: Bool
pfTy ft :: FunType
ft fConv :: ConvFun
fConv = let isaF :: Term
isaF = Cond -> ConvFun -> Term
convFun Cond
None ConvFun
fConv in
  if Bool
isPf then Term -> Term -> Term
mkTermAppl
  (Term -> Term -> Term
mkTermAppl (String -> Term
conDouble (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ case if Bool
pfTy then FunType -> FunType
makePartialVal FunType
ft else FunType
ft of
    UnitType -> "unpack2bool"
    BoolType -> "unpackBool"
    PartialVal _ -> "unpackPartial"
    _ -> "unpack2partial") Term
isaF) Term
fTrm
  else Term -> Term -> Term
mkTermAppl Term
isaF Term
fTrm

-- True means function type result was partial
adjustMkApplOrig :: Isa.Term -> Cond -> Bool -> FunType -> FunType
                 -> IsaTermCond -> Result IsaTermCond
adjustMkApplOrig :: Term
-> Cond
-> Bool
-> FunType
-> FunType
-> IsaTermCond
-> Result IsaTermCond
adjustMkApplOrig fTrm :: Term
fTrm fCs :: Cond
fCs isPf :: Bool
isPf aTy :: FunType
aTy rTy :: FunType
rTy (ITC ty :: FunType
ty aTrm :: Term
aTrm aCs :: Cond
aCs) = do
  ((pfTy :: Bool
pfTy, fConv :: ConvFun
fConv), (_, aConv :: ConvFun
aConv)) <- FunType
-> FunType
-> FunType
-> Result ((Bool, ConvFun), (FunType, ConvFun))
adjustTypes FunType
aTy FunType
rTy FunType
ty
  IsaTermCond -> Result IsaTermCond
forall (m :: * -> *) a. Monad m => a -> m a
return (IsaTermCond -> Result IsaTermCond)
-> (Cond -> IsaTermCond) -> Cond -> Result IsaTermCond
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FunType -> Term -> Cond -> IsaTermCond
ITC (if Bool
isPf Bool -> Bool -> Bool
|| Bool
pfTy then FunType -> FunType
makePartialVal FunType
rTy else FunType
rTy)
    (Term -> Term -> Term
mkTermAppl (Term -> Bool -> Bool -> FunType -> ConvFun -> Term
unpackOp Term
fTrm Bool
isPf Bool
pfTy FunType
rTy ConvFun
fConv)
    (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
mkTermAppl (Cond -> ConvFun -> Term
convFun Cond
None ConvFun
aConv) Term
aTrm) (Cond -> Result IsaTermCond) -> Cond -> Result IsaTermCond
forall a b. (a -> b) -> a -> b
$ Cond -> Cond -> Cond
joinCond Cond
fCs Cond
aCs

-- True means require result type to be partial
adjustTypes :: FunType -> FunType -> FunType
            -> Result ((Bool, ConvFun), (FunType, ConvFun))
adjustTypes :: FunType
-> FunType
-> FunType
-> Result ((Bool, ConvFun), (FunType, ConvFun))
adjustTypes aTy :: FunType
aTy rTy :: FunType
rTy ty :: FunType
ty = case (FunType
aTy, FunType
ty) of
    (TupleType l :: [FunType]
l, _) -> FunType
-> FunType
-> FunType
-> Result ((Bool, ConvFun), (FunType, ConvFun))
adjustTypes ((FunType -> FunType -> FunType) -> [FunType] -> FunType
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 FunType -> FunType -> FunType
PairType [FunType]
l) FunType
rTy FunType
ty
    (_, TupleType l :: [FunType]
l) -> FunType
-> FunType
-> FunType
-> Result ((Bool, ConvFun), (FunType, ConvFun))
adjustTypes FunType
aTy FunType
rTy (FunType -> Result ((Bool, ConvFun), (FunType, ConvFun)))
-> FunType -> Result ((Bool, ConvFun), (FunType, ConvFun))
forall a b. (a -> b) -> a -> b
$ (FunType -> FunType -> FunType) -> [FunType] -> FunType
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 FunType -> FunType -> FunType
PairType [FunType]
l
    (BoolType, BoolType) -> ((Bool, ConvFun), (FunType, ConvFun))
-> Result ((Bool, ConvFun), (FunType, ConvFun))
forall (m :: * -> *) a. Monad m => a -> m a
return ((Bool
False, ConvFun
IdOp), (FunType
ty, ConvFun
IdOp))
    (UnitType, UnitType) -> ((Bool, ConvFun), (FunType, ConvFun))
-> Result ((Bool, ConvFun), (FunType, ConvFun))
forall (m :: * -> *) a. Monad m => a -> m a
return ((Bool
False, ConvFun
IdOp), (FunType
ty, ConvFun
IdOp))
    (PartialVal _, BoolType) ->
        ((Bool, ConvFun), (FunType, ConvFun))
-> Result ((Bool, ConvFun), (FunType, ConvFun))
forall (m :: * -> *) a. Monad m => a -> m a
return ((Bool
False, ConvFun
IdOp), (FunType
aTy, Bool -> ConvFun
Bool2partial Bool
False))
    (BoolType, PartialVal _) ->
        ((Bool, ConvFun), (FunType, ConvFun))
-> Result ((Bool, ConvFun), (FunType, ConvFun))
forall (m :: * -> *) a. Monad m => a -> m a
return ((Bool
False, ConvFun
IdOp), (FunType
aTy, Bool -> ConvFun
Partial2bool Bool
False))
    (_, BoolType) -> ((Bool, ConvFun), (FunType, ConvFun))
-> Result ((Bool, ConvFun), (FunType, ConvFun))
forall (m :: * -> *) a. Monad m => a -> m a
return ((Bool
True, FunType -> ConvFun
LiftUnit FunType
rTy), (FunType
ty, ConvFun
IdOp))
    (BoolType, _) -> ((Bool, ConvFun), (FunType, ConvFun))
-> Result ((Bool, ConvFun), (FunType, ConvFun))
forall (m :: * -> *) a. Monad m => a -> m a
return ((Bool
False, ConvFun
IdOp), (FunType
aTy, Bool -> ConvFun
Unit2bool Bool
False))
    (PartialVal a :: FunType
a, PartialVal b :: FunType
b) -> do
        q :: ((Bool, ConvFun), (FunType, ConvFun))
q@(fp :: (Bool, ConvFun)
fp, (argTy :: FunType
argTy, aTrm :: ConvFun
aTrm)) <- FunType
-> FunType
-> FunType
-> Result ((Bool, ConvFun), (FunType, ConvFun))
adjustTypes FunType
a FunType
rTy FunType
b
        ((Bool, ConvFun), (FunType, ConvFun))
-> Result ((Bool, ConvFun), (FunType, ConvFun))
forall (m :: * -> *) a. Monad m => a -> m a
return (((Bool, ConvFun), (FunType, ConvFun))
 -> Result ((Bool, ConvFun), (FunType, ConvFun)))
-> ((Bool, ConvFun), (FunType, ConvFun))
-> Result ((Bool, ConvFun), (FunType, ConvFun))
forall a b. (a -> b) -> a -> b
$ case FunType
argTy of
            PartialVal _ -> ((Bool, ConvFun), (FunType, ConvFun))
q
            _ -> ((Bool, ConvFun)
fp, (FunType -> FunType
PartialVal FunType
argTy, MapFun -> ConvFun -> ConvFun
mkMapFun MapFun
MapPartial ConvFun
aTrm))
    (a :: FunType
a, PartialVal b :: FunType
b) -> do
        q :: ((Bool, ConvFun), (FunType, ConvFun))
q@(_, ap :: (FunType, ConvFun)
ap@(argTy :: FunType
argTy, _)) <- FunType
-> FunType
-> FunType
-> Result ((Bool, ConvFun), (FunType, ConvFun))
adjustTypes FunType
a FunType
rTy FunType
b
        ((Bool, ConvFun), (FunType, ConvFun))
-> Result ((Bool, ConvFun), (FunType, ConvFun))
forall (m :: * -> *) a. Monad m => a -> m a
return (((Bool, ConvFun), (FunType, ConvFun))
 -> Result ((Bool, ConvFun), (FunType, ConvFun)))
-> ((Bool, ConvFun), (FunType, ConvFun))
-> Result ((Bool, ConvFun), (FunType, ConvFun))
forall a b. (a -> b) -> a -> b
$ case FunType
argTy of
            PartialVal _ -> ((Bool, ConvFun), (FunType, ConvFun))
q
            _ -> ((Bool
True, FunType -> ConvFun
LiftPartial FunType
rTy), (FunType, ConvFun)
ap)
    (PartialVal a :: FunType
a, b :: FunType
b) -> do
        q :: ((Bool, ConvFun), (FunType, ConvFun))
q@(fp :: (Bool, ConvFun)
fp, (argTy :: FunType
argTy, aTrm :: ConvFun
aTrm)) <- FunType
-> FunType
-> FunType
-> Result ((Bool, ConvFun), (FunType, ConvFun))
adjustTypes FunType
a FunType
rTy FunType
b
        ((Bool, ConvFun), (FunType, ConvFun))
-> Result ((Bool, ConvFun), (FunType, ConvFun))
forall (m :: * -> *) a. Monad m => a -> m a
return (((Bool, ConvFun), (FunType, ConvFun))
 -> Result ((Bool, ConvFun), (FunType, ConvFun)))
-> ((Bool, ConvFun), (FunType, ConvFun))
-> Result ((Bool, ConvFun), (FunType, ConvFun))
forall a b. (a -> b) -> a -> b
$ case FunType
argTy of
            PartialVal _ -> ((Bool, ConvFun), (FunType, ConvFun))
q
            _ -> ((Bool, ConvFun)
fp, (FunType -> FunType
PartialVal FunType
argTy, ConvFun -> ConvFun -> ConvFun
mkCompFun (Bool -> ConvFun
MkPartial Bool
False) ConvFun
aTrm))
    (PairType a :: FunType
a c :: FunType
c, PairType b :: FunType
b d :: FunType
d) -> do
        ((res2Ty :: Bool
res2Ty, f2 :: ConvFun
f2), (arg2Ty :: FunType
arg2Ty, a2 :: ConvFun
a2)) <- FunType
-> FunType
-> FunType
-> Result ((Bool, ConvFun), (FunType, ConvFun))
adjustTypes FunType
c FunType
rTy FunType
d
        ((res1Ty :: Bool
res1Ty, f1 :: ConvFun
f1), (arg1Ty :: FunType
arg1Ty, a1 :: ConvFun
a1)) <- FunType
-> FunType
-> FunType
-> Result ((Bool, ConvFun), (FunType, ConvFun))
adjustTypes FunType
a
                (if Bool
res2Ty then FunType -> FunType
makePartialVal FunType
rTy else FunType
rTy) FunType
b
        ((Bool, ConvFun), (FunType, ConvFun))
-> Result ((Bool, ConvFun), (FunType, ConvFun))
forall (m :: * -> *) a. Monad m => a -> m a
return ((Bool
res1Ty Bool -> Bool -> Bool
|| Bool
res2Ty,
             ConvFun -> ConvFun -> ConvFun
mkCompFun (LiftFun -> ConvFun -> ConvFun
mkLiftFun LiftFun
LiftFst ConvFun
f1) (ConvFun -> ConvFun) -> ConvFun -> ConvFun
forall a b. (a -> b) -> a -> b
$ LiftFun -> ConvFun -> ConvFun
mkLiftFun LiftFun
LiftSnd ConvFun
f2),
                  (FunType -> FunType -> FunType
PairType FunType
arg1Ty FunType
arg2Ty,
                   ConvFun -> ConvFun -> ConvFun
mkCompFun (MapFun -> ConvFun -> ConvFun
mkMapFun MapFun
MapSnd ConvFun
a2) (ConvFun -> ConvFun) -> ConvFun -> ConvFun
forall a b. (a -> b) -> a -> b
$ MapFun -> ConvFun -> ConvFun
mkMapFun MapFun
MapFst ConvFun
a1))
    (FunType a :: FunType
a c :: FunType
c, FunType b :: FunType
b d :: FunType
d) -> do
        ((_, aF :: ConvFun
aF), (aT :: FunType
aT, aC :: ConvFun
aC)) <- FunType
-> FunType
-> FunType
-> Result ((Bool, ConvFun), (FunType, ConvFun))
adjustTypes FunType
b FunType
c FunType
a
        ((cB :: Bool
cB, cF :: ConvFun
cF), (dT :: FunType
dT, dC :: ConvFun
dC)) <- FunType
-> FunType
-> FunType
-> Result ((Bool, ConvFun), (FunType, ConvFun))
adjustTypes FunType
c FunType
rTy FunType
d
        if Bool
cB Bool -> Bool -> Bool
|| ConvFun -> Bool
isNotIdOp ConvFun
cF
          then String -> Result ((Bool, ConvFun), (FunType, ConvFun))
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "cannot adjust result types of function type"
          else ((Bool, ConvFun), (FunType, ConvFun))
-> Result ((Bool, ConvFun), (FunType, ConvFun))
forall (m :: * -> *) a. Monad m => a -> m a
return ((Bool
False, ConvFun
IdOp), (FunType -> FunType -> FunType
FunType FunType
aT FunType
dT,
                 ConvFun -> ConvFun -> ConvFun
mkCompFun ConvFun
aF (ConvFun -> ConvFun) -> ConvFun -> ConvFun
forall a b. (a -> b) -> a -> b
$ ConvFun -> ConvFun -> ConvFun
mkCompFun (ConvFun -> ConvFun
mkResFun ConvFun
dC) (ConvFun -> ConvFun) -> ConvFun -> ConvFun
forall a b. (a -> b) -> a -> b
$ ConvFun -> ConvFun
mkArgFun ConvFun
aC))
    (TypeVar _, _) -> ((Bool, ConvFun), (FunType, ConvFun))
-> Result ((Bool, ConvFun), (FunType, ConvFun))
forall (m :: * -> *) a. Monad m => a -> m a
return ((Bool
False, ConvFun
IdOp), (FunType
ty, ConvFun
IdOp))
    (_, TypeVar _) -> ((Bool, ConvFun), (FunType, ConvFun))
-> Result ((Bool, ConvFun), (FunType, ConvFun))
forall (m :: * -> *) a. Monad m => a -> m a
return ((Bool
False, ConvFun
IdOp), (FunType
aTy, ConvFun
IdOp))
    (ApplType i1 :: Id
i1 l1 :: [FunType]
l1, ApplType i2 :: Id
i2 l2 :: [FunType]
l2) | Id
i1 Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
i2 Bool -> Bool -> Bool
&& [FunType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [FunType]
l1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [FunType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [FunType]
l2 -> do
      [((Bool, ConvFun), (FunType, ConvFun))]
l <- ((FunType, FunType)
 -> Result ((Bool, ConvFun), (FunType, ConvFun)))
-> [(FunType, FunType)]
-> Result [((Bool, ConvFun), (FunType, ConvFun))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (a :: FunType
a, b :: FunType
b) -> FunType
-> FunType
-> FunType
-> Result ((Bool, ConvFun), (FunType, ConvFun))
adjustTypes FunType
a FunType
rTy FunType
b) ([(FunType, FunType)]
 -> Result [((Bool, ConvFun), (FunType, ConvFun))])
-> [(FunType, FunType)]
-> Result [((Bool, ConvFun), (FunType, ConvFun))]
forall a b. (a -> b) -> a -> b
$ [FunType] -> [FunType] -> [(FunType, FunType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [FunType]
l1 [FunType]
l2
      if (((Bool, ConvFun), (FunType, ConvFun)) -> Bool)
-> [((Bool, ConvFun), (FunType, ConvFun))] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Bool, ConvFun) -> Bool
forall a b. (a, b) -> a
fst ((Bool, ConvFun) -> Bool)
-> (((Bool, ConvFun), (FunType, ConvFun)) -> (Bool, ConvFun))
-> ((Bool, ConvFun), (FunType, ConvFun))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Bool, ConvFun), (FunType, ConvFun)) -> (Bool, ConvFun)
forall a b. (a, b) -> a
fst) [((Bool, ConvFun), (FunType, ConvFun))]
l Bool -> Bool -> Bool
|| (((Bool, ConvFun), (FunType, ConvFun)) -> Bool)
-> [((Bool, ConvFun), (FunType, ConvFun))] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (ConvFun -> Bool
isNotIdOp (ConvFun -> Bool)
-> (((Bool, ConvFun), (FunType, ConvFun)) -> ConvFun)
-> ((Bool, ConvFun), (FunType, ConvFun))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FunType, ConvFun) -> ConvFun
forall a b. (a, b) -> b
snd ((FunType, ConvFun) -> ConvFun)
-> (((Bool, ConvFun), (FunType, ConvFun)) -> (FunType, ConvFun))
-> ((Bool, ConvFun), (FunType, ConvFun))
-> ConvFun
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Bool, ConvFun), (FunType, ConvFun)) -> (FunType, ConvFun)
forall a b. (a, b) -> b
snd) [((Bool, ConvFun), (FunType, ConvFun))]
l
        then String -> Result ((Bool, ConvFun), (FunType, ConvFun))
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "cannot adjust type application"
        else ((Bool, ConvFun), (FunType, ConvFun))
-> Result ((Bool, ConvFun), (FunType, ConvFun))
forall (m :: * -> *) a. Monad m => a -> m a
return ((Bool
False, ConvFun
IdOp), (Id -> [FunType] -> FunType
ApplType Id
i1 ([FunType] -> FunType) -> [FunType] -> FunType
forall a b. (a -> b) -> a -> b
$ (((Bool, ConvFun), (FunType, ConvFun)) -> FunType)
-> [((Bool, ConvFun), (FunType, ConvFun))] -> [FunType]
forall a b. (a -> b) -> [a] -> [b]
map ((FunType, ConvFun) -> FunType
forall a b. (a, b) -> a
fst ((FunType, ConvFun) -> FunType)
-> (((Bool, ConvFun), (FunType, ConvFun)) -> (FunType, ConvFun))
-> ((Bool, ConvFun), (FunType, ConvFun))
-> FunType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Bool, ConvFun), (FunType, ConvFun)) -> (FunType, ConvFun)
forall a b. (a, b) -> b
snd) [((Bool, ConvFun), (FunType, ConvFun))]
l, ConvFun
IdOp))
    _ -> String -> Result ((Bool, ConvFun), (FunType, ConvFun))
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result ((Bool, ConvFun), (FunType, ConvFun)))
-> String -> Result ((Bool, ConvFun), (FunType, ConvFun))
forall a b. (a -> b) -> a -> b
$ "cannot adjust types\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (FunType, FunType) -> String
forall a. Show a => a -> String
show (FunType
aTy, FunType
ty)

adjustMkAppl :: Isa.Term -> Cond -> Bool -> FunType -> FunType
             -> IsaTermCond -> Result IsaTermCond
adjustMkAppl :: Term
-> Cond
-> Bool
-> FunType
-> FunType
-> IsaTermCond
-> Result IsaTermCond
adjustMkAppl fTrm :: Term
fTrm fCs :: Cond
fCs isPf :: Bool
isPf aTy :: FunType
aTy rTy :: FunType
rTy (ITC ty :: FunType
ty aTrm :: Term
aTrm aCs :: Cond
aCs) = do
    ConvFun
aConv <- FunType -> FunType -> Result ConvFun
adjustArgType FunType
aTy FunType
ty
    let (natrm :: Term
natrm, nacs :: Cond
nacs) = ConvFun -> (Term, Cond) -> (Term, Cond)
applConv ConvFun
aConv (Term
aTrm, Cond
aCs)
        (nftrm :: Term
nftrm, nfcs :: Cond
nfcs) = if Bool
isPf
          then (Term -> Term -> Term
mkTermAppl Term
makeTotal Term
fTrm, Term -> Cond -> Cond
addCond (Term -> Term -> Term
mkTermAppl Term
defOp Term
fTrm) Cond
fCs)
          else (Term
fTrm, Cond
fCs)
    IsaTermCond -> Result IsaTermCond
forall (m :: * -> *) a. Monad m => a -> m a
return (IsaTermCond -> Result IsaTermCond)
-> IsaTermCond -> Result IsaTermCond
forall a b. (a -> b) -> a -> b
$ FunType -> Term -> Cond -> IsaTermCond
ITC FunType
rTy (Term -> Term -> Term
mkTermAppl Term
nftrm Term
natrm) (Cond -> IsaTermCond) -> Cond -> IsaTermCond
forall a b. (a -> b) -> a -> b
$ Cond -> Cond -> Cond
joinCond Cond
nfcs Cond
nacs

applConv :: ConvFun -> (Isa.Term, Cond) -> (Isa.Term, Cond)
applConv :: ConvFun -> (Term, Cond) -> (Term, Cond)
applConv cnv :: ConvFun
cnv (t :: Term
t, c :: Cond
c) = let
  rt :: Term
rt = Term -> Term -> Term
mkTermAppl (Cond -> ConvFun -> Term
convFun Cond
c ConvFun
cnv) Term
t
  r :: (Term, Cond)
r = (Term
rt, Cond
c)
  rb :: (Term, Cond)
rb = (Term
rt, Cond
None)
  in case ConvFun
cnv of
    IdOp -> (Term
t, Cond
c)
    Bool2partial b :: Bool
b -> if Bool
b then (Term, Cond)
rb else (Term, Cond)
r
    Partial2bool b :: Bool
b -> if Bool
b then (Term, Cond)
rb else (Term, Cond)
r
    Bool2bool -> (Term, Cond)
rb
    Unit2bool b :: Bool
b -> if Bool
b then (Term, Cond)
rb else (Term, Cond)
r
    Bool2unit -> (Term
rt, Term -> Cond -> Cond
addCond Term
t Cond
c)
    Partial2partial -> (Term, Cond)
rb
    MkPartial b :: Bool
b -> if Bool
b then (Term, Cond)
rb else (Term, Cond)
r
    MkTotal -> (Term
rt, Term -> Cond -> Cond
addCond (Term -> Term -> Term
mkTermAppl Term
defOp Term
t) Cond
c)
    CompFun f1 :: ConvFun
f1 f2 :: ConvFun
f2 -> ConvFun -> (Term, Cond) -> (Term, Cond)
applConv ConvFun
f1 ((Term, Cond) -> (Term, Cond)) -> (Term, Cond) -> (Term, Cond)
forall a b. (a -> b) -> a -> b
$ ConvFun -> (Term, Cond) -> (Term, Cond)
applConv ConvFun
f2 (Term
t, Cond
c)
    MapFun mf :: MapFun
mf cv :: ConvFun
cv -> case Term
t of
      Tuplex [t1 :: Term
t1, t2 :: Term
t2] _ -> let
        (c1 :: Cond
c1, c2 :: Cond
c2) = case Cond
c of
          PairCond p1 :: Cond
p1 p2 :: Cond
p2 -> (Cond
p1, Cond
p2)
          _ -> (Cond
c, Cond
c)
        in case MapFun
mf of
        MapFst -> let
          (nt1 :: Term
nt1, nc1 :: Cond
nc1) = ConvFun -> (Term, Cond) -> (Term, Cond)
applConv ConvFun
cv (Term
t1, Cond
c1)
          in ([Term] -> Continuity -> Term
Tuplex [Term
nt1, Term
t2] Continuity
NotCont, Cond -> Cond -> Cond
PairCond Cond
nc1 Cond
c2)
        MapSnd -> let
          (nt2 :: Term
nt2, nc2 :: Cond
nc2) = ConvFun -> (Term, Cond) -> (Term, Cond)
applConv ConvFun
cv (Term
t2, Cond
c2)
          in ([Term] -> Continuity -> Term
Tuplex [Term
t1, Term
nt2] Continuity
NotCont, Cond -> Cond -> Cond
PairCond Cond
c1 Cond
nc2)
        MapPartial -> (Term, Cond)
r
      _ -> (Term, Cond)
r
    _ -> (Term, Cond)
r

mkArgFun :: ConvFun -> ConvFun
mkArgFun :: ConvFun -> ConvFun
mkArgFun c :: ConvFun
c = case ConvFun
c of
    IdOp -> ConvFun
c
    Bool2bool -> ConvFun
c
    Partial2partial -> ConvFun
c
    _ -> ConvFun -> ConvFun
ArgFun ConvFun
c

mkResFun :: ConvFun -> ConvFun
mkResFun :: ConvFun -> ConvFun
mkResFun c :: ConvFun
c = case ConvFun
c of
    IdOp -> ConvFun
c
    Bool2bool -> ConvFun
c
    Partial2partial -> ConvFun
c
    _ -> ConvFun -> ConvFun
ResFun ConvFun
c

isEquallyLifted :: Isa.Term -> Isa.Term -> Maybe (Isa.Term, Isa.Term, Isa.Term)
isEquallyLifted :: Term -> Term -> Maybe (Term, Term, Term)
isEquallyLifted l :: Term
l r :: Term
r = case (Term
l, Term
r) of
    (App ft :: Term
ft@(Const f :: VName
f _) la :: Term
la _,
     App (Const g :: VName
g _) ra :: Term
ra _)
        | VName
f VName -> VName -> Bool
forall a. Eq a => a -> a -> Bool
== VName
g Bool -> Bool -> Bool
&& String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (VName -> String
new VName
f) ["makePartial", "bool2partial"]
            -> (Term, Term, Term) -> Maybe (Term, Term, Term)
forall a. a -> Maybe a
Just (Term
ft, Term
la, Term
ra)
    _ -> Maybe (Term, Term, Term)
forall a. Maybe a
Nothing

isLifted :: Isa.Term -> Bool
isLifted :: Term -> Bool
isLifted t :: Term
t = case Term
t of
    App (Const f :: VName
f _) _ _ | VName -> String
new VName
f String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "makePartial" -> Bool
True
    _ -> Bool
False

splitArg :: Isa.Term -> (Isa.Term, Isa.Term)
splitArg :: Term -> (Term, Term)
splitArg arg :: Term
arg = case Term
arg of
  App (App (Const n :: VName
n _) p :: Term
p _) b :: Term
b _ | VName -> String
new VName
n String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "restrictOp" ->
      case Term
p of
        App (Const pp :: VName
pp _) t :: Term
t _ | VName -> String
new VName
pp String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "makePartial"
            -> (Term
b, Term
t)
        _ -> (Term -> Term -> Term
mkBinConj Term
b (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
mkTermAppl Term
defOp Term
p, Term -> Term -> Term
mkTermAppl Term
makeTotal Term
p)
  _ -> (Term -> Term -> Term
mkTermAppl Term
defOp Term
arg, Term -> Term -> Term
mkTermAppl Term
makeTotal Term
arg)

flipS :: String
flipS :: String
flipS = "flip"

flipOp :: Isa.Term
flipOp :: Term
flipOp = String -> Term
conDouble String
flipS

mkTermAppl :: Isa.Term -> Isa.Term -> Isa.Term
mkTermAppl :: Term -> Term -> Term
mkTermAppl fun :: Term
fun arg :: Term
arg = case (Term
fun, Term
arg) of
      (App (Const uc :: VName
uc _) b :: Term
b _, Tuplex [l :: Term
l, r :: Term
r] _) | VName -> String
new VName
uc String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
uncurryOpS ->
        let res :: Term
res = Term -> Term -> Term
mkTermAppl (Term -> Term -> Term
mkTermAppl Term
b Term
l) Term
r in case Term
b of
          Const bin :: VName
bin _ | String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (VName -> String
new VName
bin) [String
eq, "existEqualOp"] ->
            case Term -> Term -> Maybe (Term, Term, Term)
isEquallyLifted Term
l Term
r of
              Just (_, la :: Term
la, ra :: Term
ra) -> Term -> Term -> Term
mkTermAppl (Term -> Term -> Term
mkTermAppl (VName -> Term
con VName
eqV) Term
la) Term
ra
              _ -> if Term -> Bool
isLifted Term
l Bool -> Bool -> Bool
|| Term -> Bool
isLifted Term
r
                   then Term -> Term -> Term
mkTermAppl (Term -> Term -> Term
mkTermAppl (VName -> Term
con VName
eqV) Term
l) Term
r
                   else let
                     (lb :: Term
lb, lt :: Term
lt) = Term -> (Term, Term)
splitArg Term
l
                     (rb :: Term
rb, rt :: Term
rt) = Term -> (Term, Term)
splitArg Term
r
                   in if VName -> String
new VName
bin String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "existEqualOp" then
                      Term -> Term -> Term
mkBinConj Term
lb (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
mkBinConj Term
rb
                      (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
mkTermAppl (Term -> Term -> Term
mkTermAppl (VName -> Term
con VName
eqV) Term
lt) Term
rt
                      else Term
res
          _ -> Term
res
      (App (Const mp :: VName
mp _) f :: Term
f _, Tuplex [a :: Term
a, b :: Term
b] c :: Continuity
c)
          | VName -> String
new VName
mp String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "mapFst" -> [Term] -> Continuity -> Term
Tuplex [Term -> Term -> Term
mkTermAppl Term
f Term
a, Term
b] Continuity
c
          | VName -> String
new VName
mp String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "mapSnd" -> [Term] -> Continuity -> Term
Tuplex [Term
a, Term -> Term -> Term
mkTermAppl Term
f Term
b] Continuity
c
      (Const mp :: VName
mp _, Tuplex [a :: Term
a, b :: Term
b] _)
          | VName -> String
new VName
mp String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "ifImplOp" -> Term -> Term -> Term
binImpl Term
b Term
a
      (Const mp :: VName
mp _, Tuplex [Tuplex [a :: Term
a, b :: Term
b] _, c :: Term
c] d :: Continuity
d)
          | VName -> String
new VName
mp String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "whenElseOp" -> case Term -> Term -> Maybe (Term, Term, Term)
isEquallyLifted Term
a Term
c of
              Just (f :: Term
f, na :: Term
na, nc :: Term
nc) -> Term -> Term -> Term
mkTermAppl Term
f (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term -> Continuity -> Term
If Term
b Term
na Term
nc Continuity
d
              Nothing -> Term -> Term -> Term -> Continuity -> Term
If Term
b Term
a Term
c Continuity
d
      (App (Const mp :: VName
mp _) f :: Term
f _, App (Const mp2 :: VName
mp2 _) arg2 :: Term
arg2 _)
          | VName -> String
new VName
mp String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "mapPartial" Bool -> Bool -> Bool
&& VName -> String
new VName
mp2 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "makePartial" ->
             Term -> Term -> Term
mkTermAppl Term
mkPartial (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
mkTermAppl Term
f Term
arg2
      (App (Const mp :: VName
mp _) f :: Term
f c :: Continuity
c, _)
          | VName -> String
new VName
mp String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "liftUnit2bool" -> let af :: Term
af = Term -> Term -> Term
mkTermAppl Term
f Term
unitOp in
             case Term
arg of
               Const ma :: VName
ma _ | Term -> Bool
isTrue Term
arg -> Term
af
                          | VName -> String
new VName
ma String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
cFalse -> Term
false
               _ -> Term -> Term -> Term -> Continuity -> Term
If Term
arg Term
af Term
false Continuity
c
          | VName -> String
new VName
mp String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "liftUnit2partial" -> let af :: Term
af = Term -> Term -> Term
mkTermAppl Term
f Term
unitOp in
             case Term
arg of
               Const ma :: VName
ma _ | Term -> Bool
isTrue Term
arg -> Term
af
                          | VName -> String
new VName
ma String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
cFalse -> Term
noneOp
               _ -> Term -> Term -> Term -> Continuity -> Term
If Term
arg Term
af Term
noneOp Continuity
c
      (App (Const mp :: VName
mp _) _ _, _)
          | VName -> String
new VName
mp String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "liftUnit2unit" -> Term
arg
          | VName -> String
new VName
mp String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "lift2unit" -> Term -> Term -> Term
mkTermAppl Term
defOp Term
arg
      (App (App (Const cmp :: VName
cmp _) f :: Term
f _) g :: Term
g c :: Continuity
c, _)
          | VName -> String
new VName
cmp String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
compS -> Term -> Term -> Term
mkTermAppl Term
f (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
mkTermAppl Term
g Term
arg
          | VName -> String
new VName
cmp String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
curryOpS -> Term -> Term -> Term
mkTermAppl Term
f (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ [Term] -> Continuity -> Term
Tuplex [Term
g, Term
arg] Continuity
c
          | VName -> String
new VName
cmp String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
flipS -> Term -> Term -> Term
mkTermAppl (Term -> Term -> Term
mkTermAppl Term
f Term
arg) Term
g
      (Const d :: VName
d _, App (Const sm :: VName
sm _) a :: Term
a _)
          | VName -> String
new VName
d String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
defOpS Bool -> Bool -> Bool
&& VName -> String
new VName
sm String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "makePartial" -> Term
true
          | VName -> String
new VName
d String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
defOpS Bool -> Bool -> Bool
&& VName -> String
new VName
sm String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "bool2partial"
            Bool -> Bool -> Bool
|| VName -> String
new VName
d String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "bool2partial" Bool -> Bool -> Bool
&& VName -> String
new VName
sm String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
defOpS -> Term
a
          | VName -> String
new VName
d String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
curryOpS Bool -> Bool -> Bool
&& VName -> String
new VName
sm String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
uncurryOpS -> Term
a
      (Const i :: VName
i _, _)
          | VName -> String
new VName
i String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "bool2partial" ->
              let tc :: Term
tc = Term -> Term -> Term
mkTermAppl Term
mkPartial Term
unitOp
              in case Term
arg of
                    Const j :: VName
j _ | Term -> Bool
isTrue Term
arg -> Term
tc
                              | VName -> String
new VName
j String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
cFalse -> Term
noneOp
                    _ -> Term -> Term -> Term
termAppl Term
fun Term
arg -- If arg tc noneOp NotCont
          | VName -> String
new VName
i String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "id" -> Term
arg
          | VName -> String
new VName
i String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "constTrue" -> Term
true
          | VName -> String
new VName
i String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "constNil" -> Term
unitOp
      (Const i :: VName
i _, Tuplex [] _)
          | VName -> String
new VName
i String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
defOpS -> Term
false
      _ -> Term -> Term -> Term
termAppl Term
fun Term
arg

freshIndex :: State Int Int
freshIndex :: State Int Int
freshIndex = do
  Int
i <- State Int Int
forall s. State s s
get
  Int -> State Int ()
forall s. s -> State s ()
put (Int -> State Int ()) -> Int -> State Int ()
forall a b. (a -> b) -> a -> b
$ Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1
  Int -> State Int Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
i

type Simplifier = VName
  -> Isa.Term -- variable
  -> Isa.Term -- simplified application to variable
  -> Isa.Term -- simplified argument
  -> State Int Isa.Term

simpForOption :: Simplifier
simpForOption :: Simplifier
simpForOption l :: VName
l v :: Term
v nF :: Term
nF nArg :: Term
nArg =
  Term -> State Int Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> State Int Term) -> Term -> State Int Term
forall a b. (a -> b) -> a -> b
$ Term -> [(Term, Term)] -> Term
Case Term
nArg
   [ (String -> Term
conDouble "None", if VName -> String
new VName
l String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "lift2bool" then Term
false else Term
noneOp)
   , (Term -> Term -> Term
termAppl Term
conSome Term
v,
      if VName -> String
new VName
l String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "mapPartial" then Term -> Term -> Term
mkTermAppl Term
mkPartial Term
nF else Term
nF)]

mkLetAppl :: [(Isa.Term, Isa.Term)] -> Isa.Term -> Isa.Term
mkLetAppl :: [(Term, Term)] -> Term -> Term
mkLetAppl eqs :: [(Term, Term)]
eqs inTrm :: Term
inTrm = case Term
inTrm of
  App (Const mp :: VName
mp _) arg :: Term
arg _ | VName -> String
new VName
mp String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "makePartial" ->
    Term -> Term -> Term
mkTermAppl Term
mkPartial (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ [(Term, Term)] -> Term -> Term
Isa.Let [(Term, Term)]
eqs Term
arg
  _ -> [(Term, Term)] -> Term -> Term
Isa.Let [(Term, Term)]
eqs Term
inTrm

simpForPairs :: Simplifier
simpForPairs :: Simplifier
simpForPairs l :: VName
l v2 :: Term
v2 nF :: Term
nF nArg :: Term
nArg = do
  Int
n <- State Int Int
freshIndex
  let v1 :: Term
v1 = String -> Term
mkFree (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ "Xb" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n
  Term -> State Int Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> State Int Term) -> Term -> State Int Term
forall a b. (a -> b) -> a -> b
$ [(Term, Term)] -> Term -> Term
mkLetAppl [([Term] -> Continuity -> Term
Tuplex [Term
v1, Term
v2] Continuity
NotCont, Term
nArg)] (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$
     Term -> Term -> Term -> Continuity -> Term
If Term
v1 (if VName -> String
new VName
l String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "mapPartial" then Term -> Term -> Term
mkTermAppl Term
mkPartial Term
nF else Term
nF)
            (if VName -> String
new VName
l String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "lift2bool" then Term
false else Term
noneOp) Continuity
NotCont

simplify :: OldSimpKind -> Simplifier -> Isa.Term -> State Int Isa.Term
simplify :: OldSimpKind -> Simplifier -> Term -> State Int Term
simplify simK :: OldSimpKind
simK simpF :: Simplifier
simpF trm :: Term
trm = case Term
trm of
    App (App (Const l :: VName
l _) f :: Term
f _) arg :: Term
arg _
      | OldSimpKind
simK OldSimpKind -> OldSimpKind -> Bool
forall a. Eq a => a -> a -> Bool
/= OldSimpKind
NoSimpLift Bool -> Bool -> Bool
&& String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (VName -> String
new VName
l)
        ["lift2bool", "lift2partial", "mapPartial"] -> do
     Term
nArg <- OldSimpKind -> Simplifier -> Term -> State Int Term
simplify OldSimpKind
simK Simplifier
simpF Term
arg
     let lf :: String
lf = VName -> String
new VName
l
         res :: Bool
res = OldSimpKind
simK OldSimpKind -> OldSimpKind -> Bool
forall a. Eq a => a -> a -> Bool
== OldSimpKind
Lift2Restrict
     if Bool
res Bool -> Bool -> Bool
&& String
lf String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "lift2partial" then Term -> State Int Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> State Int Term)
-> (Term -> Term) -> Term -> State Int Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Term -> Term
mkTermAppl
         (Term -> Term -> Term
mkTermAppl Term
restrict (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Term -> Term
mkTermAppl Term
f (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
mkTermAppl Term
makeTotal Term
nArg)
         (Term -> State Int Term) -> Term -> State Int Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
mkTermAppl Term
defOp Term
nArg
         else if Bool
res Bool -> Bool -> Bool
&& String
lf String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "mapPartial" then Term -> State Int Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> State Int Term)
-> (Term -> Term) -> Term -> State Int Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Term -> Term
mkTermAppl
          (Term -> Term -> Term
mkTermAppl Term
restrict (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Term -> Term
mkTermAppl Term
mkPartial
                   (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Term -> Term
mkTermAppl Term
f (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
mkTermAppl Term
makeTotal Term
nArg)
          (Term -> State Int Term) -> Term -> State Int Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
mkTermAppl Term
defOp Term
nArg
         else do
      Int
n <- State Int Int
freshIndex
      let pvar :: Term
pvar = String -> Term
mkFree (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ "Xc" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n
      Term
nF <- OldSimpKind -> Simplifier -> Term -> State Int Term
simplify OldSimpKind
simK Simplifier
simpF (Term -> State Int Term) -> Term -> State Int Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
mkTermAppl Term
f Term
pvar
      Simplifier
simpF VName
l Term
pvar Term
nF Term
nArg
    App f :: Term
f arg :: Term
arg c :: Continuity
c -> do
        Term
nF <- OldSimpKind -> Simplifier -> Term -> State Int Term
simplify OldSimpKind
simK Simplifier
simpF Term
f
        Term
nArg <- OldSimpKind -> Simplifier -> Term -> State Int Term
simplify OldSimpKind
simK Simplifier
simpF Term
arg
        Term -> State Int Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> State Int Term) -> Term -> State Int Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Continuity -> Term
App Term
nF Term
nArg Continuity
c
    Abs v :: Term
v t :: Term
t c :: Continuity
c -> do
        Term
nT <- OldSimpKind -> Simplifier -> Term -> State Int Term
simplify OldSimpKind
simK Simplifier
simpF Term
t
        Term -> State Int Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> State Int Term) -> Term -> State Int Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Continuity -> Term
Abs Term
v Term
nT Continuity
c
    _ -> Term -> State Int Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
trm

mkApp :: Env -> Set.Set String -> Bool -> Set.Set String
      -> Set.Set VarDecl -> As.Term -> As.Term -> Result IsaTermCond
mkApp :: Env
-> Set String
-> Bool
-> Set String
-> Set VarDecl
-> Term
-> Term
-> Result IsaTermCond
mkApp sign :: Env
sign tyToks :: Set String
tyToks collectConds :: Bool
collectConds toks :: Set String
toks pVars :: Set VarDecl
pVars f :: Term
f arg :: Term
arg = do
    fTr :: IsaTermCond
fTr@(ITC fTy :: FunType
fTy fTrm :: Term
fTrm fCs :: Cond
fCs) <-
        Env
-> Set String
-> Bool
-> Set String
-> Set VarDecl
-> Term
-> Result IsaTermCond
transTerm Env
sign Set String
tyToks Bool
collectConds Set String
toks Set VarDecl
pVars Term
f
    IsaTermCond
aTr <- Env
-> Set String
-> Bool
-> Set String
-> Set VarDecl
-> Term
-> Result IsaTermCond
transTerm Env
sign Set String
tyToks Bool
collectConds Set String
toks Set VarDecl
pVars Term
arg
    let pv :: Result IsaTermCond
pv = case Term
arg of -- dummy application of a unit argument
          TupleTerm [] _ -> IsaTermCond -> Result IsaTermCond
forall (m :: * -> *) a. Monad m => a -> m a
return IsaTermCond
fTr
          _ -> String -> Term -> Result IsaTermCond
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "wrong function type" Term
f
        adjstAppl :: Term
-> Cond
-> Bool
-> FunType
-> FunType
-> IsaTermCond
-> Result IsaTermCond
adjstAppl = if Bool
collectConds then Term
-> Cond
-> Bool
-> FunType
-> FunType
-> IsaTermCond
-> Result IsaTermCond
adjustMkAppl else Term
-> Cond
-> Bool
-> FunType
-> FunType
-> IsaTermCond
-> Result IsaTermCond
adjustMkApplOrig
    Range -> Result IsaTermCond -> Result IsaTermCond
forall a. Range -> Result a -> Result a
adjustPos ([Term] -> Range
forall a. GetRange a => a -> Range
getRange [Term
f, Term
arg]) (Result IsaTermCond -> Result IsaTermCond)
-> Result IsaTermCond -> Result IsaTermCond
forall a b. (a -> b) -> a -> b
$ case FunType
fTy of
         FunType a :: FunType
a r :: FunType
r -> Term
-> Cond
-> Bool
-> FunType
-> FunType
-> IsaTermCond
-> Result IsaTermCond
adjstAppl Term
fTrm Cond
fCs Bool
False FunType
a FunType
r IsaTermCond
aTr
         PartialVal (FunType a :: FunType
a r :: FunType
r) -> Term
-> Cond
-> Bool
-> FunType
-> FunType
-> IsaTermCond
-> Result IsaTermCond
adjstAppl Term
fTrm Cond
fCs Bool
True FunType
a FunType
r IsaTermCond
aTr
         PartialVal _ -> Result IsaTermCond
pv
         BoolType -> Result IsaTermCond
pv
         _ -> String -> Term -> Result IsaTermCond
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "not a function type" Term
f

-- * translation of lambda abstractions

isPatternType :: As.Term -> Bool
isPatternType :: Term -> Bool
isPatternType trm :: Term
trm = case Term
trm of
    QualVar (VarDecl {}) -> Bool
True
    TypedTerm t :: Term
t _ _ _ -> Term -> Bool
isPatternType Term
t
    TupleTerm ts :: [Term]
ts _ -> (Term -> Bool) -> [Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Term -> Bool
isPatternType [Term]
ts
    _ -> Bool
False

transPattern :: Env -> Set.Set String -> Set.Set String -> As.Term
             -> Result (FunType, Isa.Term)
transPattern :: Env -> Set String -> Set String -> Term -> Result (FunType, Term)
transPattern sign :: Env
sign tyToks :: Set String
tyToks toks :: Set String
toks pat :: Term
pat = do
    ITC ty :: FunType
ty trm :: Term
trm cs :: Cond
cs <- Env
-> Set String
-> Bool
-> Set String
-> Set VarDecl
-> Term
-> Result IsaTermCond
transTerm Env
sign Set String
tyToks Bool
False Set String
toks Set VarDecl
forall a. Set a
Set.empty Term
pat
    case Term
pat of
      TupleTerm [] _ -> (FunType, Term) -> Result (FunType, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (FunType
ty, String -> Term
mkFree "_")
      _ -> if Bool -> Bool
not (Term -> Bool
isPatternType Term
pat) Bool -> Bool -> Bool
|| FunType -> Bool
isPartialVal FunType
ty
              Bool -> Bool -> Bool
|| case Cond
cs of
                   None -> Bool
False
                   _ -> Bool
True then
        String -> Range -> Result (FunType, Term)
forall a. String -> Range -> Result a
fatal_error ("illegal pattern for Isabelle: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Term
pat "")
             (Range -> Result (FunType, Term))
-> Range -> Result (FunType, Term)
forall a b. (a -> b) -> a -> b
$ Term -> Range
forall a. GetRange a => a -> Range
getRange Term
pat
       else (FunType, Term) -> Result (FunType, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (FunType
ty, Term
trm)

-- form Abs(pattern term)
abstraction :: Env -> Set.Set String -> Set.Set String
            -> IsaTermCond -> As.Term -> Result IsaTermCond
abstraction :: Env
-> Set String
-> Set String
-> IsaTermCond
-> Term
-> Result IsaTermCond
abstraction sign :: Env
sign tyToks :: Set String
tyToks toks :: Set String
toks (ITC ty :: FunType
ty body :: Term
body cs :: Cond
cs) pat :: Term
pat = do
    (pTy :: FunType
pTy, nPat :: Term
nPat) <- Env -> Set String -> Set String -> Term -> Result (FunType, Term)
transPattern Env
sign Set String
tyToks Set String
toks Term
pat
    IsaTermCond -> Result IsaTermCond
forall (m :: * -> *) a. Monad m => a -> m a
return (IsaTermCond -> Result IsaTermCond)
-> IsaTermCond -> Result IsaTermCond
forall a b. (a -> b) -> a -> b
$ FunType -> Term -> Cond -> IsaTermCond
ITC (FunType -> FunType -> FunType
FunType FunType
pTy FunType
ty) (Term -> Term -> Continuity -> Term
Abs Term
nPat Term
body Continuity
NotCont) Cond
cs