{- |
Module      :  ./Fpl/StatAna.hs
Description :  static basic analysis for FPL
Copyright   :  (c) Christian Maeder, DFKI GmbH 2011
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

basic static analysis for FPL

-}

module Fpl.StatAna
  ( basicFplAnalysis
  , minFplTerm
  , simplifyTermExt
  ) where

import Fpl.As
import Fpl.Sign

import CASL.Sign
import CASL.MixfixParser
import CASL.StaticAna
import CASL.AS_Basic_CASL
import CASL.ShowMixfix
import CASL.Overload
import CASL.Quantification
import CASL.SimplifySen

import Common.AS_Annotation
import Common.DocUtils
import Common.ExtSign
import Common.GlobalAnnotations
import Common.Id
import Common.Lib.State
import Common.Result
import Common.Utils
import qualified Common.Lib.MapSet as MapSet

import Control.Monad
import qualified Control.Monad.Fail as Fail

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

import Data.Maybe

basicFplAnalysis
  :: (FplBasicSpec, FplSign, GlobalAnnos)
  -> Result (FplBasicSpec, ExtSign FplSign Symbol, [Named FplForm])
basicFplAnalysis :: (FplBasicSpec, FplSign, GlobalAnnos)
-> Result (FplBasicSpec, ExtSign FplSign Symbol, [Named FplForm])
basicFplAnalysis (b :: FplBasicSpec
b, s :: FplSign
s, ga :: GlobalAnnos
ga) =
    ((FplBasicSpec, ExtSign FplSign Symbol, [Named FplForm])
 -> (FplBasicSpec, ExtSign FplSign Symbol, [Named FplForm]))
-> Result (FplBasicSpec, ExtSign FplSign Symbol, [Named FplForm])
-> Result (FplBasicSpec, ExtSign FplSign Symbol, [Named FplForm])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ (r :: FplBasicSpec
r, ExtSign t :: FplSign
t syms :: Set Symbol
syms, sens :: [Named FplForm]
sens) ->
       (FplBasicSpec
r, FplSign -> Set Symbol -> ExtSign FplSign Symbol
forall sign symbol. sign -> Set symbol -> ExtSign sign symbol
ExtSign (FplSign -> FplSign
delBuiltins FplSign
t) Set Symbol
syms, [Named FplForm]
sens))
    (Result (FplBasicSpec, ExtSign FplSign Symbol, [Named FplForm])
 -> Result (FplBasicSpec, ExtSign FplSign Symbol, [Named FplForm]))
-> Result (FplBasicSpec, ExtSign FplSign Symbol, [Named FplForm])
-> Result (FplBasicSpec, ExtSign FplSign Symbol, [Named FplForm])
forall a b. (a -> b) -> a -> b
$ Min TermExt SignExt
-> Ana FplExt FplExt () TermExt SignExt
-> Ana () FplExt () TermExt SignExt
-> Mix FplExt () TermExt SignExt
-> (FplBasicSpec, FplSign, GlobalAnnos)
-> Result (FplBasicSpec, ExtSign FplSign Symbol, [Named FplForm])
forall f e b s.
(FormExtension f, TermExtension f) =>
Min f e
-> Ana b b s f e
-> Ana s b s f e
-> Mix b s f e
-> (BASIC_SPEC b s f, Sign f e, GlobalAnnos)
-> Result
     (BASIC_SPEC b s f, ExtSign (Sign f e) Symbol, [Named (FORMULA f)])
basicAnalysis Min TermExt SignExt
minFplTerm Ana FplExt FplExt () TermExt SignExt
anaFplExt ((() -> State FplSign ()) -> Ana () FplExt () TermExt SignExt
forall a b. a -> b -> a
const () -> State FplSign ()
forall (m :: * -> *) a. Monad m => a -> m a
return) Mix FplExt () TermExt SignExt
mixFplAna
    (FplBasicSpec
b, FplSign -> FplSign
addBuiltins FplSign
s, GlobalAnnos
ga)

mixFplAna :: Mix FplExt () TermExt SignExt
mixFplAna :: Mix FplExt () TermExt SignExt
mixFplAna = Mix Any () Any SignExt
forall b s f e. Mix b s f e
emptyMix
    { getBaseIds :: FplExt -> IdSets
getBaseIds = FplExt -> IdSets
fplIds
    , putParen :: TermExt -> TermExt
putParen = TermExt -> TermExt
mapTermExt
    , mixResolve :: MixResolve TermExt
mixResolve = MixResolve TermExt
resolveTermExt
    }

fplIds :: FplExt -> IdSets
fplIds :: FplExt -> IdSets
fplIds fe :: FplExt
fe = case FplExt
fe of
  FplSortItems sis :: [Annoted FplSortItem]
sis _ -> [IdSets] -> IdSets
unite ([IdSets] -> IdSets) -> [IdSets] -> IdSets
forall a b. (a -> b) -> a -> b
$ (Annoted FplSortItem -> IdSets)
-> [Annoted FplSortItem] -> [IdSets]
forall a b. (a -> b) -> [a] -> [b]
map (FplSortItem -> IdSets
fplSortIds (FplSortItem -> IdSets)
-> (Annoted FplSortItem -> FplSortItem)
-> Annoted FplSortItem
-> IdSets
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted FplSortItem -> FplSortItem
forall a. Annoted a -> a
item) [Annoted FplSortItem]
sis
  FplOpItems ois :: [Annoted FplOpItem]
ois _ -> [IdSets] -> IdSets
unite ([IdSets] -> IdSets) -> [IdSets] -> IdSets
forall a b. (a -> b) -> a -> b
$ (Annoted FplOpItem -> IdSets) -> [Annoted FplOpItem] -> [IdSets]
forall a b. (a -> b) -> [a] -> [b]
map (FplOpItem -> IdSets
fplOpIds (FplOpItem -> IdSets)
-> (Annoted FplOpItem -> FplOpItem) -> Annoted FplOpItem -> IdSets
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted FplOpItem -> FplOpItem
forall a. Annoted a -> a
item) [Annoted FplOpItem]
ois

fplSortIds :: FplSortItem -> IdSets
fplSortIds :: FplSortItem -> IdSets
fplSortIds si :: FplSortItem
si = case FplSortItem
si of
  FreeType dt :: DATATYPE_DECL
dt -> (DATATYPE_DECL -> (Set Id, Set Id)
ids_DATATYPE_DECL DATATYPE_DECL
dt, Set Id
forall a. Set a
Set.empty)
  CaslSortItem _ -> IdSets
emptyIdSets

fplOpIds :: FplOpItem -> IdSets
fplOpIds :: FplOpItem -> IdSets
fplOpIds oi :: FplOpItem
oi = let e :: Set a
e = Set a
forall a. Set a
Set.empty in case FplOpItem
oi of
  FunOp (FunDef i :: Id
i (Op_head _ vs :: [VAR_DECL]
vs _ _) _ _) -> let s :: Set Id
s = Id -> Set Id
forall a. a -> Set a
Set.singleton Id
i in
      (if [VAR_DECL] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [VAR_DECL]
vs then (Set Id
s, Set Id
forall a. Set a
e) else (Set Id
forall a. Set a
e, Set Id
s), Set Id
forall a. Set a
e)
  CaslOpItem o :: OP_ITEM TermExt
o -> (OP_ITEM TermExt -> (Set Id, Set Id)
forall f. OP_ITEM f -> (Set Id, Set Id)
ids_OP_ITEM OP_ITEM TermExt
o, Set Id
forall a. Set a
e)

-- | put parens around terms
mapTermExt :: TermExt -> TermExt
mapTermExt :: TermExt -> TermExt
mapTermExt te :: TermExt
te = let rec :: TERM TermExt -> TERM TermExt
rec = (TermExt -> TermExt) -> TERM TermExt -> TERM TermExt
forall f. (f -> f) -> TERM f -> TERM f
mapTerm TermExt -> TermExt
mapTermExt in case TermExt
te of
  FixDef fd :: FunDef
fd -> FunDef -> TermExt
FixDef (FunDef -> TermExt) -> FunDef -> TermExt
forall a b. (a -> b) -> a -> b
$ FunDef -> FunDef
mapFunDef FunDef
fd
  Case o :: TERM TermExt
o l :: [(TERM TermExt, TERM TermExt)]
l r :: Range
r -> TERM TermExt -> [(TERM TermExt, TERM TermExt)] -> Range -> TermExt
Case (TERM TermExt -> TERM TermExt
rec TERM TermExt
o)
    (((TERM TermExt, TERM TermExt) -> (TERM TermExt, TERM TermExt))
-> [(TERM TermExt, TERM TermExt)] -> [(TERM TermExt, TERM TermExt)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (p :: TERM TermExt
p, t :: TERM TermExt
t) -> (TERM TermExt -> TERM TermExt
rec TERM TermExt
p, TERM TermExt -> TERM TermExt
rec TERM TermExt
t)) [(TERM TermExt, TERM TermExt)]
l) Range
r
  Let fd :: FunDef
fd t :: TERM TermExt
t r :: Range
r -> FunDef -> TERM TermExt -> Range -> TermExt
Let (FunDef -> FunDef
mapFunDef FunDef
fd) (TERM TermExt -> TERM TermExt
rec TERM TermExt
t) Range
r
  IfThenElse i :: TERM TermExt
i t :: TERM TermExt
t e :: TERM TermExt
e r :: Range
r -> TERM TermExt -> TERM TermExt -> TERM TermExt -> Range -> TermExt
IfThenElse (TERM TermExt -> TERM TermExt
rec TERM TermExt
i) (TERM TermExt -> TERM TermExt
rec TERM TermExt
t) (TERM TermExt -> TERM TermExt
rec TERM TermExt
e) Range
r
  EqTerm t :: TERM TermExt
t e :: TERM TermExt
e r :: Range
r -> TERM TermExt -> TERM TermExt -> Range -> TermExt
EqTerm (TERM TermExt -> TERM TermExt
rec TERM TermExt
t) (TERM TermExt -> TERM TermExt
rec TERM TermExt
e) Range
r
  BoolTerm t :: TERM TermExt
t -> TERM TermExt -> TermExt
BoolTerm (TERM TermExt -> TERM TermExt
rec TERM TermExt
t)

-- | put parens around final term
mapFunDef :: FunDef -> FunDef
mapFunDef :: FunDef -> FunDef
mapFunDef (FunDef o :: Id
o h :: OP_HEAD
h at :: Annoted (TERM TermExt)
at r :: Range
r) =
  Id -> OP_HEAD -> Annoted (TERM TermExt) -> Range -> FunDef
FunDef Id
o OP_HEAD
h ((TERM TermExt -> TERM TermExt)
-> Annoted (TERM TermExt) -> Annoted (TERM TermExt)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((TermExt -> TermExt) -> TERM TermExt -> TERM TermExt
forall f. (f -> f) -> TERM f -> TERM f
mapTerm TermExt -> TermExt
mapTermExt) Annoted (TERM TermExt)
at) Range
r

{- | The is the plugin function for the mixfix analysis. Due to patterns there
may be unknown simple identifiers that are turned to constants and later by
the overload resolution to variables. Obviously, such variables cannot be fed
into the mixfix analysis like all other known variables. -}
resolveTermExt :: MixResolve TermExt
resolveTermExt :: MixResolve TermExt
resolveTermExt ga :: GlobalAnnos
ga ids :: (TokRules, Rules)
ids te :: TermExt
te =
  let recAux :: (TokRules, Rules) -> TERM TermExt -> Result (TERM TermExt)
recAux = (TermExt -> TermExt)
-> MixResolve TermExt -> MixResolve (TERM TermExt)
forall f.
FormExtension f =>
(f -> f) -> MixResolve f -> MixResolve (TERM f)
resolveMixTrm TermExt -> TermExt
mapTermExt MixResolve TermExt
resolveTermExt GlobalAnnos
ga
      rec :: TERM TermExt -> Result (TERM TermExt)
rec = (TokRules, Rules) -> TERM TermExt -> Result (TERM TermExt)
recAux (TokRules, Rules)
ids
  in case TermExt
te of
  FixDef fd :: FunDef
fd -> (FunDef -> TermExt) -> Result FunDef -> Result TermExt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FunDef -> TermExt
FixDef (Result FunDef -> Result TermExt)
-> Result FunDef -> Result TermExt
forall a b. (a -> b) -> a -> b
$ MixResolve FunDef
resolveFunDef GlobalAnnos
ga (TokRules, Rules)
ids FunDef
fd
  Case o :: TERM TermExt
o l :: [(TERM TermExt, TERM TermExt)]
l r :: Range
r -> do
    TERM TermExt
ro <- TERM TermExt -> Result (TERM TermExt)
rec TERM TermExt
o
    -- CHECK: consider pattern variables
    [(TERM TermExt, TERM TermExt)]
rl <- ((TERM TermExt, TERM TermExt)
 -> Result (TERM TermExt, TERM TermExt))
-> [(TERM TermExt, TERM TermExt)]
-> Result [(TERM TermExt, TERM TermExt)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (p :: TERM TermExt
p, t :: TERM TermExt
t) -> (TERM TermExt -> TERM TermExt -> (TERM TermExt, TERM TermExt))
-> Result (TERM TermExt)
-> Result (TERM TermExt)
-> Result (TERM TermExt, TERM TermExt)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (,)
          (TERM TermExt -> Result (TERM TermExt)
rec TERM TermExt
p)
          (Result (TERM TermExt) -> Result (TERM TermExt, TERM TermExt))
-> Result (TERM TermExt) -> Result (TERM TermExt, TERM TermExt)
forall a b. (a -> b) -> a -> b
$ TERM TermExt -> Result (TERM TermExt)
rec TERM TermExt
t) [(TERM TermExt, TERM TermExt)]
l
    TermExt -> Result TermExt
forall (m :: * -> *) a. Monad m => a -> m a
return (TermExt -> Result TermExt) -> TermExt -> Result TermExt
forall a b. (a -> b) -> a -> b
$ TERM TermExt -> [(TERM TermExt, TERM TermExt)] -> Range -> TermExt
Case TERM TermExt
ro [(TERM TermExt, TERM TermExt)]
rl Range
r
  Let fd :: FunDef
fd@(FunDef o :: Id
o _ _ _) t :: TERM TermExt
t r :: Range
r -> do
    FunDef
rfd <- MixResolve FunDef
resolveFunDef GlobalAnnos
ga (TokRules, Rules)
ids FunDef
fd
    TERM TermExt
rt <- (TokRules, Rules) -> TERM TermExt -> Result (TERM TermExt)
recAux (Id -> (TokRules, Rules) -> (TokRules, Rules)
addIdToRules Id
o (TokRules, Rules)
ids) TERM TermExt
t
    TermExt -> Result TermExt
forall (m :: * -> *) a. Monad m => a -> m a
return (TermExt -> Result TermExt) -> TermExt -> Result TermExt
forall a b. (a -> b) -> a -> b
$ FunDef -> TERM TermExt -> Range -> TermExt
Let FunDef
rfd TERM TermExt
rt Range
r
  IfThenElse i :: TERM TermExt
i t :: TERM TermExt
t e :: TERM TermExt
e r :: Range
r -> do
    TERM TermExt
ri <- TERM TermExt -> Result (TERM TermExt)
rec TERM TermExt
i
    TERM TermExt
rt <- TERM TermExt -> Result (TERM TermExt)
rec TERM TermExt
t
    TERM TermExt
re <- TERM TermExt -> Result (TERM TermExt)
rec TERM TermExt
e
    TermExt -> Result TermExt
forall (m :: * -> *) a. Monad m => a -> m a
return (TermExt -> Result TermExt) -> TermExt -> Result TermExt
forall a b. (a -> b) -> a -> b
$ TERM TermExt -> TERM TermExt -> TERM TermExt -> Range -> TermExt
IfThenElse TERM TermExt
ri TERM TermExt
rt TERM TermExt
re Range
r
  EqTerm t :: TERM TermExt
t e :: TERM TermExt
e r :: Range
r -> do
    TERM TermExt
rt <- TERM TermExt -> Result (TERM TermExt)
rec TERM TermExt
t
    TERM TermExt
re <- TERM TermExt -> Result (TERM TermExt)
rec TERM TermExt
e
    TermExt -> Result TermExt
forall (m :: * -> *) a. Monad m => a -> m a
return (TermExt -> Result TermExt) -> TermExt -> Result TermExt
forall a b. (a -> b) -> a -> b
$ TERM TermExt -> TERM TermExt -> Range -> TermExt
EqTerm TERM TermExt
rt TERM TermExt
re Range
r
  BoolTerm t :: TERM TermExt
t -> (TERM TermExt -> TermExt)
-> Result (TERM TermExt) -> Result TermExt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TERM TermExt -> TermExt
BoolTerm (Result (TERM TermExt) -> Result TermExt)
-> Result (TERM TermExt) -> Result TermExt
forall a b. (a -> b) -> a -> b
$ TERM TermExt -> Result (TERM TermExt)
rec TERM TermExt
t

-- | resolve overloading in rhs and assume function to be in the signature
resolveFunDef :: MixResolve FunDef
resolveFunDef :: MixResolve FunDef
resolveFunDef ga :: GlobalAnnos
ga ids :: (TokRules, Rules)
ids (FunDef o :: Id
o h :: OP_HEAD
h@(Op_head _ vs :: [VAR_DECL]
vs _ _) at :: Annoted (TERM TermExt)
at r :: Range
r) = do
  TERM TermExt
nt <- (TermExt -> TermExt)
-> MixResolve TermExt -> MixResolve (TERM TermExt)
forall f.
FormExtension f =>
(f -> f) -> MixResolve f -> MixResolve (TERM f)
resolveMixTrm TermExt -> TermExt
mapTermExt MixResolve TermExt
resolveTermExt GlobalAnnos
ga
    (Id -> (TokRules, Rules) -> (TokRules, Rules)
addIdToRules Id
o ((TokRules, Rules) -> (TokRules, Rules))
-> (TokRules, Rules) -> (TokRules, Rules)
forall a b. (a -> b) -> a -> b
$ Set Token -> (TokRules, Rules) -> (TokRules, Rules)
extendRules ([VAR_DECL] -> Set Token
varDeclTokens [VAR_DECL]
vs) (TokRules, Rules)
ids) (TERM TermExt -> Result (TERM TermExt))
-> TERM TermExt -> Result (TERM TermExt)
forall a b. (a -> b) -> a -> b
$ Annoted (TERM TermExt) -> TERM TermExt
forall a. Annoted a -> a
item Annoted (TERM TermExt)
at
  FunDef -> Result FunDef
forall (m :: * -> *) a. Monad m => a -> m a
return (FunDef -> Result FunDef) -> FunDef -> Result FunDef
forall a b. (a -> b) -> a -> b
$ Id -> OP_HEAD -> Annoted (TERM TermExt) -> Range -> FunDef
FunDef Id
o OP_HEAD
h Annoted (TERM TermExt)
at { item :: TERM TermExt
item = TERM TermExt
nt } Range
r

-- | get constructors for input sort
getConstrs :: FplSign -> SORT -> OpMap
getConstrs :: FplSign -> Id -> OpMap
getConstrs sign :: FplSign
sign resSort :: Id
resSort = (Set OpType -> Set OpType) -> OpMap -> OpMap
forall a b c. Ord a => (Set b -> Set c) -> MapSet a b -> MapSet a c
MapSet.mapSet
  ((OpType -> Bool) -> Set OpType -> Set OpType
forall a. (a -> Bool) -> Set a -> Set a
Set.filter ((OpType -> Bool) -> Set OpType -> Set OpType)
-> (OpType -> Bool) -> Set OpType -> Set OpType
forall a b. (a -> b) -> a -> b
$ FplSign -> Id -> Id -> Bool
forall f e. Sign f e -> Id -> Id -> Bool
leqSort FplSign
sign Id
resSort (Id -> Bool) -> (OpType -> Id) -> OpType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpType -> Id
opRes) (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ SignExt -> OpMap
constr (SignExt -> OpMap) -> SignExt -> OpMap
forall a b. (a -> b) -> a -> b
$ FplSign -> SignExt
forall f e. Sign f e -> e
extendedInfo FplSign
sign

{- | This functions tries to recognize variables in case-patterns (application
terms) after overload resolution.  A current limitation is that a unique sort
is needed as input that is taken from the term between @case@ and @of@. -}
resolvePattern :: FplSign -> (SORT, FplTerm) -> Result ([VAR_DECL], FplTerm)
resolvePattern :: FplSign -> (Id, TERM TermExt) -> Result ([VAR_DECL], TERM TermExt)
resolvePattern sign :: FplSign
sign (resSort :: Id
resSort, term :: TERM TermExt
term) =
  let err :: [Char] -> m a
err msg :: [Char]
msg = [Char] -> m a
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
Fail.fail ([Char] -> m a) -> [Char] -> m a
forall a b. (a -> b) -> a -> b
$ [Char]
msg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ " " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ TERM TermExt -> [Char] -> [Char]
forall a. Pretty a => a -> [Char] -> [Char]
showDoc TERM TermExt
term "" in
  case TERM TermExt
term of
  Application opSym :: OP_SYMB
opSym args :: [TERM TermExt]
args p :: Range
p ->
    let ide :: Id
ide@(Id ts :: [Token]
ts _ _) = OP_SYMB -> Id
opSymbName OP_SYMB
opSym in
    case (OpType -> Bool) -> [OpType] -> [OpType]
forall a. (a -> Bool) -> [a] -> [a]
filter ( \ oTy :: OpType
oTy -> [Id] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (OpType -> [Id]
opArgs OpType
oTy) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [TERM TermExt] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TERM TermExt]
args
                    Bool -> Bool -> Bool
&& case OP_SYMB
opSym of
                         Qual_op_name _ symTy :: OP_TYPE
symTy _ ->
                             FplSign -> OpType -> OpType -> Bool
forall f e. Sign f e -> OpType -> OpType -> Bool
leqF FplSign
sign OpType
oTy (OpType -> Bool) -> OpType -> Bool
forall a b. (a -> b) -> a -> b
$ OP_TYPE -> OpType
toOpType OP_TYPE
symTy
                         _ -> Bool
True
                    )
         ([OpType] -> [OpType]) -> [OpType] -> [OpType]
forall a b. (a -> b) -> a -> b
$ Set OpType -> [OpType]
forall a. Set a -> [a]
Set.toList (Set OpType -> [OpType]) -> Set OpType -> [OpType]
forall a b. (a -> b) -> a -> b
$ Id -> OpMap -> Set OpType
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup Id
ide (OpMap -> Set OpType) -> OpMap -> Set OpType
forall a b. (a -> b) -> a -> b
$ FplSign -> Id -> OpMap
getConstrs FplSign
sign Id
resSort of
      [] -> if [TERM TermExt] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TERM TermExt]
args Bool -> Bool -> Bool
&& Id -> Bool
isSimpleId Id
ide then
                let v :: VAR_DECL
v = [Token] -> Id -> Range -> VAR_DECL
Var_decl [[Token] -> Token
forall a. [a] -> a
head [Token]
ts] Id
resSort (Range -> VAR_DECL) -> Range -> VAR_DECL
forall a b. (a -> b) -> a -> b
$ Id -> Range
posOfId Id
ide
                in ([VAR_DECL], TERM TermExt) -> Result ([VAR_DECL], TERM TermExt)
forall (m :: * -> *) a. Monad m => a -> m a
return ([VAR_DECL
v], VAR_DECL -> TERM TermExt
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
v)
            else [Char] -> Result ([VAR_DECL], TERM TermExt)
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
err "unresolved pattern"
      [OpType k :: OpKind
k as :: [Id]
as r :: Id
r] -> do
        [([VAR_DECL], TERM TermExt)]
l <- ((Id, TERM TermExt) -> Result ([VAR_DECL], TERM TermExt))
-> [(Id, TERM TermExt)] -> Result [([VAR_DECL], TERM TermExt)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (FplSign -> (Id, TERM TermExt) -> Result ([VAR_DECL], TERM TermExt)
resolvePattern FplSign
sign) ([(Id, TERM TermExt)] -> Result [([VAR_DECL], TERM TermExt)])
-> [(Id, TERM TermExt)] -> Result [([VAR_DECL], TERM TermExt)]
forall a b. (a -> b) -> a -> b
$ [Id] -> [TERM TermExt] -> [(Id, TERM TermExt)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Id]
as [TERM TermExt]
args
        ([VAR_DECL], TERM TermExt) -> Result ([VAR_DECL], TERM TermExt)
forall (m :: * -> *) a. Monad m => a -> m a
return ((([VAR_DECL], TERM TermExt) -> [VAR_DECL])
-> [([VAR_DECL], TERM TermExt)] -> [VAR_DECL]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([VAR_DECL], TERM TermExt) -> [VAR_DECL]
forall a b. (a, b) -> a
fst [([VAR_DECL], TERM TermExt)]
l,
          OP_SYMB -> [TERM TermExt] -> Range -> TERM TermExt
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application (Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name Id
ide (OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
k [Id]
as Id
r Range
p) Range
p) ((([VAR_DECL], TERM TermExt) -> TERM TermExt)
-> [([VAR_DECL], TERM TermExt)] -> [TERM TermExt]
forall a b. (a -> b) -> [a] -> [b]
map ([VAR_DECL], TERM TermExt) -> TERM TermExt
forall a b. (a, b) -> b
snd [([VAR_DECL], TERM TermExt)]
l) Range
p)
      _ -> [Char] -> Result ([VAR_DECL], TERM TermExt)
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
err "ambiguous pattern"
  Qual_var v :: Token
v s :: Id
s r :: Range
r -> if FplSign -> Id -> Id -> Bool
forall f e. Sign f e -> Id -> Id -> Bool
leqSort FplSign
sign Id
s Id
resSort then
      ([VAR_DECL], TERM TermExt) -> Result ([VAR_DECL], TERM TermExt)
forall (m :: * -> *) a. Monad m => a -> m a
return ([[Token] -> Id -> Range -> VAR_DECL
Var_decl [Token
v] Id
s Range
r], TERM TermExt
term)
    else [Char] -> Result ([VAR_DECL], TERM TermExt)
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
err "wrong type of pattern variable"
  Sorted_term t :: TERM TermExt
t s :: Id
s r :: Range
r -> if FplSign -> Id -> Id -> Bool
forall f e. Sign f e -> Id -> Id -> Bool
leqSort FplSign
sign Id
s Id
resSort then do
      (vs :: [VAR_DECL]
vs, nt :: TERM TermExt
nt) <- FplSign -> (Id, TERM TermExt) -> Result ([VAR_DECL], TERM TermExt)
resolvePattern FplSign
sign (Id
s, TERM TermExt
t)
      ([VAR_DECL], TERM TermExt) -> Result ([VAR_DECL], TERM TermExt)
forall (m :: * -> *) a. Monad m => a -> m a
return ([VAR_DECL]
vs, TERM TermExt -> Id -> Range -> TERM TermExt
forall f. TERM f -> Id -> Range -> TERM f
Sorted_term TERM TermExt
nt Id
s Range
r)
    else [Char] -> Result ([VAR_DECL], TERM TermExt)
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
err "wrong typed pattern"
  _ -> [Char] -> Result ([VAR_DECL], TERM TermExt)
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
err "unexpected pattern"

addFunToSign :: FunDef -> State FplSign ()
addFunToSign :: FunDef -> State FplSign ()
addFunToSign (FunDef o :: Id
o h :: OP_HEAD
h _ _) =
  State FplSign ()
-> (OP_TYPE -> State FplSign ())
-> Maybe OP_TYPE
-> State FplSign ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> State FplSign ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (\ ty :: OP_TYPE
ty -> Annoted Id -> OpType -> Id -> State FplSign ()
forall a f e. Annoted a -> OpType -> Id -> State (Sign f e) ()
addOp (Id -> Annoted Id
forall a. a -> Annoted a
emptyAnno Id
o) (OP_TYPE -> OpType
toOpType OP_TYPE
ty) Id
o)
  (Maybe OP_TYPE -> State FplSign ())
-> Maybe OP_TYPE -> State FplSign ()
forall a b. (a -> b) -> a -> b
$ OP_HEAD -> Maybe OP_TYPE
headToType OP_HEAD
h

letVars :: FunDef -> [VAR_DECL]
letVars :: FunDef -> [VAR_DECL]
letVars (FunDef o :: Id
o (Op_head _ vs :: [VAR_DECL]
vs ms :: Maybe Id
ms _) at :: Annoted (TERM TermExt)
at ps :: Range
ps) =
     [ [Token] -> Id -> Range -> VAR_DECL
Var_decl [Id -> Token
idToSimpleId Id
o] (TERM TermExt -> Id
forall f. TermExtension f => f -> Id
sortOfTerm (TERM TermExt -> Id) -> TERM TermExt -> Id
forall a b. (a -> b) -> a -> b
$ Annoted (TERM TermExt) -> TERM TermExt
forall a. Annoted a -> a
item Annoted (TERM TermExt)
at) Range
ps
     | Id -> Bool
isSimpleId Id
o Bool -> Bool -> Bool
&& Maybe Id -> Bool
forall a. Maybe a -> Bool
isNothing Maybe Id
ms Bool -> Bool -> Bool
&& [VAR_DECL] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [VAR_DECL]
vs ]

addFunVar :: FunDef -> State FplSign ()
addFunVar :: FunDef -> State FplSign ()
addFunVar = (VAR_DECL -> State FplSign ()) -> [VAR_DECL] -> State FplSign ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ VAR_DECL -> State FplSign ()
forall f e. VAR_DECL -> State (Sign f e) ()
addVars ([VAR_DECL] -> State FplSign ())
-> (FunDef -> [VAR_DECL]) -> FunDef -> State FplSign ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FunDef -> [VAR_DECL]
letVars

{- | perform overload resolution after mixfix analysis. The type of patterns
is deduced from the top term. Overlapping or exhaustive patterns are not
recognized yet. -}
minFplTerm :: Min TermExt SignExt
minFplTerm :: Min TermExt SignExt
minFplTerm sig :: FplSign
sig te :: TermExt
te = case TermExt
te of
  FixDef fd :: FunDef
fd -> (FunDef -> TermExt) -> Result FunDef -> Result TermExt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FunDef -> TermExt
FixDef (Result FunDef -> Result TermExt)
-> Result FunDef -> Result TermExt
forall a b. (a -> b) -> a -> b
$ FplSign -> FunDef -> Result FunDef
minFunDef FplSign
sig FunDef
fd
  Case o :: TERM TermExt
o l :: [(TERM TermExt, TERM TermExt)]
l r :: Range
r -> do
    TERM TermExt
ro <- Min TermExt SignExt
-> FplSign -> TERM TermExt -> Result (TERM TermExt)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> TERM f -> Result (TERM f)
oneExpTerm Min TermExt SignExt
minFplTerm FplSign
sig TERM TermExt
o
    -- assume unique type of top-level term for now
    let s :: Id
s = TERM TermExt -> Id
forall f. TermExtension f => f -> Id
sortOfTerm TERM TermExt
ro
    [(TERM TermExt, [[TERM TermExt]])]
rl <- ((TERM TermExt, TERM TermExt)
 -> Result (TERM TermExt, [[TERM TermExt]]))
-> [(TERM TermExt, TERM TermExt)]
-> Result [(TERM TermExt, [[TERM TermExt]])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (p :: TERM TermExt
p, t :: TERM TermExt
t) -> do
          (vs :: [VAR_DECL]
vs, np :: TERM TermExt
np) <- FplSign -> (Id, TERM TermExt) -> Result ([VAR_DECL], TERM TermExt)
resolvePattern FplSign
sig (Id
s, TERM TermExt
p)
          [Diagnosis] -> Result ()
appendDiags ([Diagnosis] -> Result ()) -> [Diagnosis] -> Result ()
forall a b. (a -> b) -> a -> b
$ [Token] -> [Diagnosis]
forall a. (Pretty a, GetRange a, Ord a) => [a] -> [Diagnosis]
checkUniqueness ([Token] -> [Diagnosis])
-> ([(Token, Id)] -> [Token]) -> [(Token, Id)] -> [Diagnosis]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Token, Id) -> Token) -> [(Token, Id)] -> [Token]
forall a b. (a -> b) -> [a] -> [b]
map (Token, Id) -> Token
forall a b. (a, b) -> a
fst ([(Token, Id)] -> [Diagnosis]) -> [(Token, Id)] -> [Diagnosis]
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> [(Token, Id)]
flatVAR_DECLs [VAR_DECL]
vs
          let newSign :: FplSign
newSign = State FplSign () -> FplSign -> FplSign
forall s a. State s a -> s -> s
execState ((VAR_DECL -> State FplSign ()) -> [VAR_DECL] -> State FplSign ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ VAR_DECL -> State FplSign ()
forall f e. VAR_DECL -> State (Sign f e) ()
addVars [VAR_DECL]
vs) FplSign
sig
          [[TERM TermExt]]
rt <- Min TermExt SignExt
-> FplSign -> TERM TermExt -> Result [[TERM TermExt]]
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> TERM f -> Result [[TERM f]]
minExpTerm Min TermExt SignExt
minFplTerm FplSign
newSign TERM TermExt
t
          (TERM TermExt, [[TERM TermExt]])
-> Result (TERM TermExt, [[TERM TermExt]])
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM TermExt
np, [[TERM TermExt]]
rt)) [(TERM TermExt, TERM TermExt)]
l
    let (ps :: [TERM TermExt]
ps, tts :: [[[TERM TermExt]]]
tts) = [(TERM TermExt, [[TERM TermExt]])]
-> ([TERM TermExt], [[[TERM TermExt]]])
forall a b. [(a, b)] -> ([a], [b])
unzip [(TERM TermExt, [[TERM TermExt]])]
rl
        cSupers :: [f] -> Bool
cSupers tl :: [f]
tl = case [f]
tl of
          [] -> Bool
True
          hd :: f
hd : rt :: [f]
rt -> (f -> Bool) -> [f] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> FplSign -> Id -> Id -> Bool
forall f e. Bool -> Sign f e -> Id -> Id -> Bool
haveCommonSupersorts Bool
True FplSign
sig
             (f -> Id
forall f. TermExtension f => f -> Id
sortOfTerm f
hd) (Id -> Bool) -> (f -> Id) -> f -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f -> Id
forall f. TermExtension f => f -> Id
sortOfTerm) [f]
rt Bool -> Bool -> Bool
&& [f] -> Bool
cSupers [f]
rt
    [TERM TermExt]
nts <- [Char]
-> GlobalAnnos
-> [TERM TermExt]
-> [[[TERM TermExt]]]
-> Range
-> Result [TERM TermExt]
forall f.
Pretty f =>
[Char] -> GlobalAnnos -> f -> [[f]] -> Range -> Result f
isUnambiguous "" (FplSign -> GlobalAnnos
forall f e. Sign f e -> GlobalAnnos
globAnnos FplSign
sig) (((TERM TermExt, TERM TermExt) -> TERM TermExt)
-> [(TERM TermExt, TERM TermExt)] -> [TERM TermExt]
forall a b. (a -> b) -> [a] -> [b]
map (TERM TermExt, TERM TermExt) -> TERM TermExt
forall a b. (a, b) -> b
snd [(TERM TermExt, TERM TermExt)]
l)
      (([[TERM TermExt]] -> [[TERM TermExt]])
-> [[[TERM TermExt]]] -> [[[TERM TermExt]]]
forall a b. (a -> b) -> [a] -> [b]
map (([TERM TermExt] -> Bool) -> [[TERM TermExt]] -> [[TERM TermExt]]
forall a. (a -> Bool) -> [a] -> [a]
filter [TERM TermExt] -> Bool
forall f. TermExtension f => [f] -> Bool
cSupers ([[TERM TermExt]] -> [[TERM TermExt]])
-> ([[TERM TermExt]] -> [[TERM TermExt]])
-> [[TERM TermExt]]
-> [[TERM TermExt]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[TERM TermExt]] -> [[TERM TermExt]]
forall a. [[a]] -> [[a]]
combine) ([[[TERM TermExt]]] -> [[[TERM TermExt]]])
-> [[[TERM TermExt]]] -> [[[TERM TermExt]]]
forall a b. (a -> b) -> a -> b
$ [[[TERM TermExt]]] -> [[[TERM TermExt]]]
forall a. [[a]] -> [[a]]
combine [[[TERM TermExt]]]
tts) Range
r
    let nl :: [(TERM TermExt, TERM TermExt)]
nl = [TERM TermExt] -> [TERM TermExt] -> [(TERM TermExt, TERM TermExt)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TERM TermExt]
ps [TERM TermExt]
nts
        minSort :: Set Id -> Set Id
minSort sl :: Set Id
sl = if Set Id -> Bool
forall a. Set a -> Bool
Set.null Set Id
sl then Set Id
forall a. Set a
Set.empty else
           let (hd :: Id
hd, rt :: Set Id
rt) = Set Id -> (Id, Set Id)
forall a. Set a -> (a, Set a)
Set.deleteFindMin Set Id
sl
           in [Set Id] -> Set Id
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Id] -> Set Id) -> (Set Id -> [Set Id]) -> Set Id -> Set Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Id -> Set Id) -> [Id] -> [Set Id]
forall a b. (a -> b) -> [a] -> [b]
map ([Id] -> Set Id
forall a. Ord a => [a] -> Set a
Set.fromList ([Id] -> Set Id) -> (Id -> [Id]) -> Id -> Set Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FplSign -> Id -> Id -> [Id]
forall f e. Sign f e -> Id -> Id -> [Id]
minimalSupers FplSign
sig Id
hd)
                    ([Id] -> [Set Id]) -> (Set Id -> [Id]) -> Set Id -> [Set Id]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Id -> [Id]
forall a. Set a -> [a]
Set.toList (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Id -> Set Id -> Set Id
forall a. Ord a => a -> Set a -> Set a
Set.insert Id
hd (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Set Id -> Set Id
minSort Set Id
rt
        mSort :: Set Id
mSort = Set Id -> Set Id
minSort (Set Id -> Set Id) -> ([Id] -> Set Id) -> [Id] -> Set Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Id] -> Set Id
forall a. Ord a => [a] -> Set a
Set.fromList ([Id] -> Set Id) -> [Id] -> Set Id
forall a b. (a -> b) -> a -> b
$ (TERM TermExt -> Id) -> [TERM TermExt] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map TERM TermExt -> Id
forall f. TermExtension f => f -> Id
sortOfTerm [TERM TermExt]
nts
    case Set Id -> [Id]
forall a. Set a -> [a]
Set.toList Set Id
mSort of
      [tSort :: Id
tSort] -> do
         [(TERM TermExt, TERM TermExt)]
fl <- ((TERM TermExt, TERM TermExt)
 -> Result (TERM TermExt, TERM TermExt))
-> [(TERM TermExt, TERM TermExt)]
-> Result [(TERM TermExt, TERM TermExt)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (p :: TERM TermExt
p, t :: TERM TermExt
t) -> do
            let pvs :: VarSet
pvs = FplSign -> TERM TermExt -> VarSet
forall f e. TermExtension f => Sign f e -> TERM f -> VarSet
freeTermVars FplSign
sig TERM TermExt
p
                tvs :: VarSet
tvs = FplSign -> TERM TermExt -> VarSet
forall f e. TermExtension f => Sign f e -> TERM f -> VarSet
freeTermVars FplSign
sig TERM TermExt
t
                unused :: VarSet
unused = VarSet -> VarSet -> VarSet
forall a. Ord a => Set a -> Set a -> Set a
Set.difference VarSet
pvs VarSet
tvs
            Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (VarSet -> Bool
forall a. Set a -> Bool
Set.null VarSet
unused) (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$
              [Diagnosis] -> Result ()
appendDiags ([Diagnosis] -> Result ()) -> [Diagnosis] -> Result ()
forall a b. (a -> b) -> a -> b
$ ((Token, Id) -> Diagnosis) -> [(Token, Id)] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map (DiagKind -> [Char] -> (Token, Id) -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Warning "unused pattern variables")
                     ([(Token, Id)] -> [Diagnosis]) -> [(Token, Id)] -> [Diagnosis]
forall a b. (a -> b) -> a -> b
$ VarSet -> [(Token, Id)]
forall a. Set a -> [a]
Set.toList VarSet
unused
            (TERM TermExt, TERM TermExt) -> Result (TERM TermExt, TERM TermExt)
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM TermExt
p, FplSign -> TERM TermExt -> Id -> Range -> TERM TermExt
forall f e.
TermExtension f =>
Sign f e -> TERM f -> Id -> Range -> TERM f
mkSorted FplSign
sig TERM TermExt
t Id
tSort Range
r)) [(TERM TermExt, TERM TermExt)]
nl
         TermExt -> Result TermExt
forall (m :: * -> *) a. Monad m => a -> m a
return (TermExt -> Result TermExt) -> TermExt -> Result TermExt
forall a b. (a -> b) -> a -> b
$ TERM TermExt -> [(TERM TermExt, TERM TermExt)] -> Range -> TermExt
Case TERM TermExt
ro [(TERM TermExt, TERM TermExt)]
fl Range
r
      sl :: [Id]
sl -> [Char] -> Range -> Result TermExt
forall a b. (GetRange a, Pretty a) => [Char] -> a -> Result b
mkError ("no common supersort for case terms: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Id] -> [Char]
forall a. Show a => a -> [Char]
show [Id]
sl) Range
r
  Let fd :: FunDef
fd t :: TERM TermExt
t r :: Range
r -> do
    let newSign :: FplSign
newSign = State FplSign () -> FplSign -> FplSign
forall s a. State s a -> s -> s
execState (FunDef -> State FplSign ()
addFunToSign FunDef
fd) FplSign
sig
    FunDef
rfd <- FplSign -> FunDef -> Result FunDef
minFunDef FplSign
newSign FunDef
fd
    let sign2 :: FplSign
sign2 = State FplSign () -> FplSign -> FplSign
forall s a. State s a -> s -> s
execState (FunDef -> State FplSign ()
addFunVar FunDef
rfd) FplSign
newSign
    TERM TermExt
rt <- Min TermExt SignExt
-> FplSign -> TERM TermExt -> Result (TERM TermExt)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> TERM f -> Result (TERM f)
oneExpTerm Min TermExt SignExt
minFplTerm FplSign
sign2 TERM TermExt
t
    TermExt -> Result TermExt
forall (m :: * -> *) a. Monad m => a -> m a
return (TermExt -> Result TermExt) -> TermExt -> Result TermExt
forall a b. (a -> b) -> a -> b
$ FunDef -> TERM TermExt -> Range -> TermExt
Let FunDef
rfd TERM TermExt
rt Range
r
  IfThenElse i :: TERM TermExt
i t :: TERM TermExt
t e :: TERM TermExt
e r :: Range
r -> do
    TERM TermExt
ri <- Min TermExt SignExt
-> FplSign -> TERM TermExt -> Result (TERM TermExt)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> TERM f -> Result (TERM f)
oneExpTerm Min TermExt SignExt
minFplTerm FplSign
sig (TERM TermExt -> Result (TERM TermExt))
-> TERM TermExt -> Result (TERM TermExt)
forall a b. (a -> b) -> a -> b
$ TERM TermExt -> Id -> Range -> TERM TermExt
forall f. TERM f -> Id -> Range -> TERM f
Sorted_term TERM TermExt
i Id
boolSort Range
r
    Equation rt :: TERM TermExt
rt Strong re :: TERM TermExt
re _ <-
        Min TermExt SignExt
-> FplSign
-> (TERM TermExt -> TERM TermExt -> Range -> FplForm)
-> TERM TermExt
-> TERM TermExt
-> Range
-> Result FplForm
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> Sign f e
-> (TERM f -> TERM f -> Range -> FORMULA f)
-> TERM f
-> TERM f
-> Range
-> Result (FORMULA f)
minExpFORMULAeq Min TermExt SignExt
minFplTerm FplSign
sig (TERM TermExt -> Equality -> TERM TermExt -> Range -> FplForm
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
`Equation` Equality
Strong) TERM TermExt
t TERM TermExt
e Range
r
    TermExt -> Result TermExt
forall (m :: * -> *) a. Monad m => a -> m a
return (TermExt -> Result TermExt) -> TermExt -> Result TermExt
forall a b. (a -> b) -> a -> b
$ TERM TermExt -> TERM TermExt -> TERM TermExt -> Range -> TermExt
IfThenElse TERM TermExt
ri TERM TermExt
rt TERM TermExt
re Range
r
  EqTerm t :: TERM TermExt
t e :: TERM TermExt
e r :: Range
r -> do
    Equation rt :: TERM TermExt
rt Strong re :: TERM TermExt
re _ <-
        Min TermExt SignExt
-> FplSign
-> (TERM TermExt -> TERM TermExt -> Range -> FplForm)
-> TERM TermExt
-> TERM TermExt
-> Range
-> Result FplForm
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> Sign f e
-> (TERM f -> TERM f -> Range -> FORMULA f)
-> TERM f
-> TERM f
-> Range
-> Result (FORMULA f)
minExpFORMULAeq Min TermExt SignExt
minFplTerm FplSign
sig (TERM TermExt -> Equality -> TERM TermExt -> Range -> FplForm
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
`Equation` Equality
Strong) TERM TermExt
t TERM TermExt
e Range
r
    TermExt -> Result TermExt
forall (m :: * -> *) a. Monad m => a -> m a
return (TermExt -> Result TermExt) -> TermExt -> Result TermExt
forall a b. (a -> b) -> a -> b
$ TERM TermExt -> TERM TermExt -> Range -> TermExt
EqTerm TERM TermExt
rt TERM TermExt
re Range
r
  BoolTerm t :: TERM TermExt
t -> (TERM TermExt -> TermExt)
-> Result (TERM TermExt) -> Result TermExt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TERM TermExt -> TermExt
BoolTerm (Result (TERM TermExt) -> Result TermExt)
-> Result (TERM TermExt) -> Result TermExt
forall a b. (a -> b) -> a -> b
$ Min TermExt SignExt
-> FplSign -> TERM TermExt -> Result (TERM TermExt)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> TERM f -> Result (TERM f)
oneExpTerm Min TermExt SignExt
minFplTerm FplSign
sig TERM TermExt
t

-- | type check rhs and assume function to be in the signature
minFunDef :: Sign TermExt SignExt -> FunDef -> Result FunDef
minFunDef :: FplSign -> FunDef -> Result FunDef
minFunDef sig :: FplSign
sig fd :: FunDef
fd@(FunDef o :: Id
o h :: OP_HEAD
h@(Op_head _ vs :: [VAR_DECL]
vs ms :: Maybe Id
ms _) at :: Annoted (TERM TermExt)
at r :: Range
r) = do
  let newSign :: FplSign
newSign = State FplSign () -> FplSign -> FplSign
forall s a. State s a -> s -> s
execState ((VAR_DECL -> State FplSign ()) -> [VAR_DECL] -> State FplSign ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ VAR_DECL -> State FplSign ()
forall f e. VAR_DECL -> State (Sign f e) ()
addVars [VAR_DECL]
vs State FplSign () -> State FplSign () -> State FplSign ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FunDef -> State FplSign ()
addFunToSign FunDef
fd) FplSign
sig
      varSign :: Sign f SignExt
varSign = State (Sign f SignExt) () -> Sign f SignExt -> Sign f SignExt
forall s a. State s a -> s -> s
execState ((VAR_DECL -> State (Sign f SignExt) ())
-> [VAR_DECL] -> State (Sign f SignExt) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ VAR_DECL -> State (Sign f SignExt) ()
forall f e. VAR_DECL -> State (Sign f e) ()
addVars [VAR_DECL]
vs) (Sign f SignExt -> Sign f SignExt)
-> Sign f SignExt -> Sign f SignExt
forall a b. (a -> b) -> a -> b
$ SignExt -> Sign f SignExt
forall e f. e -> Sign f e
emptySign SignExt
emptyFplSign
      t :: TERM TermExt
t = Annoted (TERM TermExt) -> TERM TermExt
forall a. Annoted a -> a
item Annoted (TERM TermExt)
at
  TERM TermExt
nt <- Min TermExt SignExt
-> FplSign -> TERM TermExt -> Result (TERM TermExt)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> TERM f -> Result (TERM f)
oneExpTerm Min TermExt SignExt
minFplTerm FplSign
newSign (TERM TermExt -> Result (TERM TermExt))
-> TERM TermExt -> Result (TERM TermExt)
forall a b. (a -> b) -> a -> b
$ TERM TermExt -> (Id -> TERM TermExt) -> Maybe Id -> TERM TermExt
forall b a. b -> (a -> b) -> Maybe a -> b
maybe TERM TermExt
t (\ s :: Id
s -> TERM TermExt -> Id -> Range -> TERM TermExt
forall f. TERM f -> Id -> Range -> TERM f
Sorted_term TERM TermExt
t Id
s Range
r) Maybe Id
ms
  [Diagnosis] -> Result ()
appendDiags ([Diagnosis] -> Result ()) -> [Diagnosis] -> Result ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Sign Any SignExt -> VarSet -> [Diagnosis]
forall f e. [Char] -> Sign f e -> VarSet -> [Diagnosis]
warnUnusedVars " function " Sign Any SignExt
forall f. Sign f SignExt
varSign (VarSet -> [Diagnosis]) -> VarSet -> [Diagnosis]
forall a b. (a -> b) -> a -> b
$ FplSign -> TERM TermExt -> VarSet
forall f e. TermExtension f => Sign f e -> TERM f -> VarSet
freeTermVars FplSign
newSign TERM TermExt
nt
  FunDef -> Result FunDef
forall (m :: * -> *) a. Monad m => a -> m a
return (FunDef -> Result FunDef) -> FunDef -> Result FunDef
forall a b. (a -> b) -> a -> b
$ Id -> OP_HEAD -> Annoted (TERM TermExt) -> Range -> FunDef
FunDef Id
o OP_HEAD
h Annoted (TERM TermExt)
at { item :: TERM TermExt
item = TERM TermExt
nt } Range
r

getDDSorts :: [Annoted FplSortItem] -> [SORT]
getDDSorts :: [Annoted FplSortItem] -> [Id]
getDDSorts = ([Id] -> Annoted FplSortItem -> [Id])
-> [Id] -> [Annoted FplSortItem] -> [Id]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ l :: [Id]
l si :: Annoted FplSortItem
si -> case Annoted FplSortItem -> FplSortItem
forall a. Annoted a -> a
item Annoted FplSortItem
si of
  FreeType (Datatype_decl s :: Id
s _ _) -> Id
s Id -> [Id] -> [Id]
forall a. a -> [a] -> [a]
: [Id]
l
  CaslSortItem _ -> [Id]
l) []

anaFplExt :: Ana FplExt FplExt () TermExt SignExt
anaFplExt :: Ana FplExt FplExt () TermExt SignExt
anaFplExt mix :: Mix FplExt () TermExt SignExt
mix fe :: FplExt
fe = case FplExt
fe of
  FplSortItems ais :: [Annoted FplSortItem]
ais r :: Range
r -> do
    (Id -> State FplSign ()) -> [Id] -> State FplSign ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ s :: Id
s -> SortsKind -> Annoted Id -> Id -> State FplSign ()
forall a f e. SortsKind -> Annoted a -> Id -> State (Sign f e) ()
addSort SortsKind
NonEmptySorts (Id -> Annoted Id
forall a. a -> Annoted a
emptyAnno Id
s) Id
s)
      ([Id] -> State FplSign ()) -> [Id] -> State FplSign ()
forall a b. (a -> b) -> a -> b
$ [Annoted FplSortItem] -> [Id]
getDDSorts [Annoted FplSortItem]
ais
    [Annoted FplSortItem]
ns <- (FplSortItem -> State FplSign FplSortItem)
-> [Annoted FplSortItem] -> State FplSign [Annoted FplSortItem]
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> [Annoted a] -> m [Annoted b]
mapAnM (Ana FplSortItem FplExt () TermExt SignExt
anaFplSortItem Mix FplExt () TermExt SignExt
mix) [Annoted FplSortItem]
ais
    State FplSign ()
forall f e. State (Sign f e) ()
closeSubsortRel
    FplExt -> State FplSign FplExt
forall (m :: * -> *) a. Monad m => a -> m a
return (FplExt -> State FplSign FplExt) -> FplExt -> State FplSign FplExt
forall a b. (a -> b) -> a -> b
$ [Annoted FplSortItem] -> Range -> FplExt
FplSortItems [Annoted FplSortItem]
ns Range
r
  FplOpItems ais :: [Annoted FplOpItem]
ais r :: Range
r -> do
    [Annoted FplOpItem]
ns <- (FplOpItem -> State FplSign FplOpItem)
-> [Annoted FplOpItem] -> State FplSign [Annoted FplOpItem]
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> [Annoted a] -> m [Annoted b]
mapAnM (Ana FplOpItem FplExt () TermExt SignExt
anaFplOpItem Mix FplExt () TermExt SignExt
mix) [Annoted FplOpItem]
ais
    FplExt -> State FplSign FplExt
forall (m :: * -> *) a. Monad m => a -> m a
return (FplExt -> State FplSign FplExt) -> FplExt -> State FplSign FplExt
forall a b. (a -> b) -> a -> b
$ [Annoted FplOpItem] -> Range -> FplExt
FplOpItems [Annoted FplOpItem]
ns Range
r

anaFplSortItem :: Ana FplSortItem FplExt () TermExt SignExt
anaFplSortItem :: Ana FplSortItem FplExt () TermExt SignExt
anaFplSortItem mix :: Mix FplExt () TermExt SignExt
mix si :: FplSortItem
si = case FplSortItem
si of
  FreeType dt :: DATATYPE_DECL
dt@(Datatype_decl s :: Id
s aalts :: [Annoted ALTERNATIVE]
aalts _) -> do
    GenKind -> DATATYPE_DECL -> State FplSign [Component]
forall f e.
GenKind -> DATATYPE_DECL -> State (Sign f e) [Component]
ana_DATATYPE_DECL GenKind
Free DATATYPE_DECL
dt
    FplSign
sign <- State FplSign FplSign
forall s. State s s
get
    let cm :: OpMap
cm = FplSign -> Id -> OpMap
getConstrs FplSign
sign Id
s
    (SignExt -> Result SignExt) -> State FplSign ()
forall e f. (e -> Result e) -> State (Sign f e) ()
updateExtInfo ((SignExt -> Result SignExt) -> State FplSign ())
-> (SignExt -> Result SignExt) -> State FplSign ()
forall a b. (a -> b) -> a -> b
$ \ cs :: SignExt
cs -> (SignExt -> Annoted ALTERNATIVE -> Result SignExt)
-> SignExt -> [Annoted ALTERNATIVE] -> Result SignExt
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM
      (\ e :: SignExt
e aa :: Annoted ALTERNATIVE
aa -> let a :: ALTERNATIVE
a = Annoted ALTERNATIVE -> ALTERNATIVE
forall a. Annoted a -> a
item Annoted ALTERNATIVE
aa in if ALTERNATIVE -> Bool
isConsAlt ALTERNATIVE
a then do
            let (c :: Id
c, ty :: OpType
ty, _) = Id -> ALTERNATIVE -> (Id, OpType, [COMPONENTS])
getConsType Id
s ALTERNATIVE
a
            Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (OpMap -> Bool
forall a b. MapSet a b -> Bool
MapSet.null OpMap
cm)
              (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ if OpType -> Set OpType -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (OpType -> OpType
mkPartial OpType
ty)
                    (Set OpType -> Bool) -> Set OpType -> Bool
forall a b. (a -> b) -> a -> b
$ Set OpType -> Set OpType
makePartial (Set OpType -> Set OpType) -> Set OpType -> Set OpType
forall a b. (a -> b) -> a -> b
$ Id -> OpMap -> Set OpType
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup Id
c OpMap
cm
                then [Diagnosis] -> Result ()
appendDiags [DiagKind -> [Char] -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Warning "repeated constructor" Id
c]
                else [Char] -> Id -> Result ()
forall a b. (GetRange a, Pretty a) => [Char] -> a -> Result b
mkError "illegal new constructor" Id
c
            SignExt -> Result SignExt
forall (m :: * -> *) a. Monad m => a -> m a
return SignExt
e { constr :: OpMap
constr = Id -> OpType -> OpMap -> OpMap
addOpTo Id
c OpType
ty (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ SignExt -> OpMap
constr SignExt
e }
      else [Char] -> ALTERNATIVE -> Result SignExt
forall a b. (GetRange a, Pretty a) => [Char] -> a -> Result b
mkError "unexpected subsort embedding" ALTERNATIVE
a) SignExt
cs [Annoted ALTERNATIVE]
aalts
    FplSortItem -> State FplSign FplSortItem
forall (m :: * -> *) a. Monad m => a -> m a
return FplSortItem
si
  CaslSortItem s :: SORT_ITEM TermExt
s -> (Annoted (SORT_ITEM TermExt) -> FplSortItem)
-> State FplSign (Annoted (SORT_ITEM TermExt))
-> State FplSign FplSortItem
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (SORT_ITEM TermExt -> FplSortItem
CaslSortItem (SORT_ITEM TermExt -> FplSortItem)
-> (Annoted (SORT_ITEM TermExt) -> SORT_ITEM TermExt)
-> Annoted (SORT_ITEM TermExt)
-> FplSortItem
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted (SORT_ITEM TermExt) -> SORT_ITEM TermExt
forall a. Annoted a -> a
item)
    (State FplSign (Annoted (SORT_ITEM TermExt))
 -> State FplSign FplSortItem)
-> State FplSign (Annoted (SORT_ITEM TermExt))
-> State FplSign FplSortItem
forall a b. (a -> b) -> a -> b
$ Min TermExt SignExt
-> Mix FplExt () TermExt SignExt
-> SortsKind
-> Annoted (SORT_ITEM TermExt)
-> State FplSign (Annoted (SORT_ITEM TermExt))
forall f e b s.
(FormExtension f, TermExtension f) =>
Min f e
-> Mix b s f e
-> SortsKind
-> Annoted (SORT_ITEM f)
-> State (Sign f e) (Annoted (SORT_ITEM f))
ana_SORT_ITEM Min TermExt SignExt
minFplTerm Mix FplExt () TermExt SignExt
mix SortsKind
NonEmptySorts (Annoted (SORT_ITEM TermExt)
 -> State FplSign (Annoted (SORT_ITEM TermExt)))
-> Annoted (SORT_ITEM TermExt)
-> State FplSign (Annoted (SORT_ITEM TermExt))
forall a b. (a -> b) -> a -> b
$ SORT_ITEM TermExt -> Annoted (SORT_ITEM TermExt)
forall a. a -> Annoted a
emptyAnno SORT_ITEM TermExt
s

anaFplOpItem :: Ana FplOpItem FplExt () TermExt SignExt
anaFplOpItem :: Ana FplOpItem FplExt () TermExt SignExt
anaFplOpItem mix :: Mix FplExt () TermExt SignExt
mix oi :: FplOpItem
oi = case FplOpItem
oi of
  FunOp fd :: FunDef
fd@(FunDef i :: Id
i oh :: OP_HEAD
oh@(Op_head _ vs :: [VAR_DECL]
vs r :: Maybe Id
r _) at :: Annoted (TERM TermExt)
at ps :: Range
ps) -> do
    let mty :: Maybe OP_TYPE
mty = OP_HEAD -> Maybe OP_TYPE
headToType OP_HEAD
oh
        lb :: [Char]
lb = Annoted (TERM TermExt) -> [Char]
forall a. Annoted a -> [Char]
getRLabel Annoted (TERM TermExt)
at
    FunDef -> State FplSign ()
addFunToSign FunDef
fd
    FplSign
e <- State FplSign FplSign
forall s. State s s
get -- save
    FplSign -> State FplSign ()
forall s. s -> State s ()
put FplSign
e { varMap :: Map Token Id
varMap = Map Token Id
forall k a. Map k a
Map.empty }
    (VAR_DECL -> State FplSign ()) -> [VAR_DECL] -> State FplSign ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ VAR_DECL -> State FplSign ()
forall f e. VAR_DECL -> State (Sign f e) ()
addVars [VAR_DECL]
vs
    FplSign
sign <- State FplSign FplSign
forall s. State s s
get
    FplSign -> State FplSign ()
forall s. s -> State s ()
put FplSign
e -- restore
    let Result ds :: [Diagnosis]
ds mt :: Maybe (TERM TermExt, TERM TermExt)
mt = Min TermExt SignExt
-> Mix FplExt () TermExt SignExt
-> FplSign
-> Maybe Id
-> Range
-> TERM TermExt
-> Result (TERM TermExt, TERM TermExt)
forall f e b s.
(FormExtension f, TermExtension f) =>
Min f e
-> Mix b s f e
-> Sign f e
-> Maybe Id
-> Range
-> TERM f
-> Result (TERM f, TERM f)
anaTerm Min TermExt SignExt
minFplTerm Mix FplExt () TermExt SignExt
mix FplSign
sign Maybe Id
r Range
ps (TERM TermExt -> Result (TERM TermExt, TERM TermExt))
-> TERM TermExt -> Result (TERM TermExt, TERM TermExt)
forall a b. (a -> b) -> a -> b
$ Annoted (TERM TermExt) -> TERM TermExt
forall a. Annoted a -> a
item Annoted (TERM TermExt)
at
    [Diagnosis] -> State FplSign ()
forall f e. [Diagnosis] -> State (Sign f e) ()
addDiags [Diagnosis]
ds
    case Maybe (TERM TermExt, TERM TermExt)
mt of
      Nothing -> FplOpItem -> State FplSign FplOpItem
forall (m :: * -> *) a. Monad m => a -> m a
return
        (FplOpItem -> State FplSign FplOpItem)
-> FplOpItem -> State FplSign FplOpItem
forall a b. (a -> b) -> a -> b
$ FplOpItem -> (OP_TYPE -> FplOpItem) -> Maybe OP_TYPE -> FplOpItem
forall b a. b -> (a -> b) -> Maybe a -> b
maybe FplOpItem
oi (\ ty :: OP_TYPE
ty -> OP_ITEM TermExt -> FplOpItem
CaslOpItem (OP_ITEM TermExt -> FplOpItem) -> OP_ITEM TermExt -> FplOpItem
forall a b. (a -> b) -> a -> b
$ [Id] -> OP_TYPE -> [OP_ATTR TermExt] -> Range -> OP_ITEM TermExt
forall f. [Id] -> OP_TYPE -> [OP_ATTR f] -> Range -> OP_ITEM f
Op_decl [Id
i] OP_TYPE
ty [] Range
ps) Maybe OP_TYPE
mty
      Just (resT :: TERM TermExt
resT, anaT :: TERM TermExt
anaT) -> do
        [Named FplForm] -> State FplSign ()
forall f e. [Named (FORMULA f)] -> State (Sign f e) ()
addSentences
          [([Char] -> FplForm -> Named FplForm
forall a s. a -> s -> SenAttr s a
makeNamed [Char]
lb (FplForm -> Named FplForm) -> FplForm -> Named FplForm
forall a b. (a -> b) -> a -> b
$ TermExt -> FplForm
forall f. f -> FORMULA f
ExtFORMULA (TermExt -> FplForm) -> TermExt -> FplForm
forall a b. (a -> b) -> a -> b
$ FunDef -> TermExt
FixDef
           (FunDef -> TermExt) -> FunDef -> TermExt
forall a b. (a -> b) -> a -> b
$ Id -> OP_HEAD -> Annoted (TERM TermExt) -> Range -> FunDef
FunDef Id
i OP_HEAD
oh Annoted (TERM TermExt)
at { item :: TERM TermExt
item = TERM TermExt
anaT } Range
ps)
           { isAxiom :: Bool
isAxiom = Annoted (TERM TermExt) -> Bool
forall a. Annoted a -> Bool
notImplied Annoted (TERM TermExt)
at, isDef :: Bool
isDef = Bool
True }]
        FplOpItem -> State FplSign FplOpItem
forall (m :: * -> *) a. Monad m => a -> m a
return (FplOpItem -> State FplSign FplOpItem)
-> FplOpItem -> State FplSign FplOpItem
forall a b. (a -> b) -> a -> b
$ FunDef -> FplOpItem
FunOp (FunDef -> FplOpItem) -> FunDef -> FplOpItem
forall a b. (a -> b) -> a -> b
$ Id -> OP_HEAD -> Annoted (TERM TermExt) -> Range -> FunDef
FunDef Id
i OP_HEAD
oh Annoted (TERM TermExt)
at { item :: TERM TermExt
item = TERM TermExt
resT } Range
ps
  CaslOpItem o :: OP_ITEM TermExt
o -> (Annoted (OP_ITEM TermExt) -> FplOpItem)
-> State FplSign (Annoted (OP_ITEM TermExt))
-> State FplSign FplOpItem
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (OP_ITEM TermExt -> FplOpItem
CaslOpItem (OP_ITEM TermExt -> FplOpItem)
-> (Annoted (OP_ITEM TermExt) -> OP_ITEM TermExt)
-> Annoted (OP_ITEM TermExt)
-> FplOpItem
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted (OP_ITEM TermExt) -> OP_ITEM TermExt
forall a. Annoted a -> a
item)
    (State FplSign (Annoted (OP_ITEM TermExt))
 -> State FplSign FplOpItem)
-> State FplSign (Annoted (OP_ITEM TermExt))
-> State FplSign FplOpItem
forall a b. (a -> b) -> a -> b
$ Min TermExt SignExt
-> Mix FplExt () TermExt SignExt
-> Annoted (OP_ITEM TermExt)
-> State FplSign (Annoted (OP_ITEM TermExt))
forall f e b s.
(FormExtension f, TermExtension f) =>
Min f e
-> Mix b s f e
-> Annoted (OP_ITEM f)
-> State (Sign f e) (Annoted (OP_ITEM f))
ana_OP_ITEM Min TermExt SignExt
minFplTerm Mix FplExt () TermExt SignExt
mix (OP_ITEM TermExt -> Annoted (OP_ITEM TermExt)
forall a. a -> Annoted a
emptyAnno OP_ITEM TermExt
o)

freeFunDefVars :: Sign TermExt e -> FunDef -> VarSet
freeFunDefVars :: Sign TermExt e -> FunDef -> VarSet
freeFunDefVars s :: Sign TermExt e
s (FunDef _ (Op_head _ vs :: [VAR_DECL]
vs _ _) at :: Annoted (TERM TermExt)
at _) = VarSet -> VarSet -> VarSet
forall a. Ord a => Set a -> Set a -> Set a
Set.difference
  (Sign TermExt e -> TERM TermExt -> VarSet
forall f e. TermExtension f => Sign f e -> TERM f -> VarSet
freeTermVars Sign TermExt e
s (TERM TermExt -> VarSet) -> TERM TermExt -> VarSet
forall a b. (a -> b) -> a -> b
$ Annoted (TERM TermExt) -> TERM TermExt
forall a. Annoted a -> a
item Annoted (TERM TermExt)
at) (VarSet -> VarSet) -> VarSet -> VarSet
forall a b. (a -> b) -> a -> b
$ [(Token, Id)] -> VarSet
forall a. Ord a => [a] -> Set a
Set.fromList ([(Token, Id)] -> VarSet) -> [(Token, Id)] -> VarSet
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> [(Token, Id)]
flatVAR_DECLs [VAR_DECL]
vs

instance TermExtension TermExt where
  freeVarsOfExt :: Sign TermExt e -> TermExt -> VarSet
freeVarsOfExt s :: Sign TermExt e
s te :: TermExt
te = case TermExt
te of
    FixDef fd :: FunDef
fd -> Sign TermExt e -> FunDef -> VarSet
forall e. Sign TermExt e -> FunDef -> VarSet
freeFunDefVars Sign TermExt e
s FunDef
fd
    Case o :: TERM TermExt
o l :: [(TERM TermExt, TERM TermExt)]
l _ -> [VarSet] -> VarSet
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([VarSet] -> VarSet) -> [VarSet] -> VarSet
forall a b. (a -> b) -> a -> b
$ Sign TermExt e -> TERM TermExt -> VarSet
forall f e. TermExtension f => Sign f e -> TERM f -> VarSet
freeTermVars Sign TermExt e
s TERM TermExt
o
      VarSet -> [VarSet] -> [VarSet]
forall a. a -> [a] -> [a]
: ((TERM TermExt, TERM TermExt) -> VarSet)
-> [(TERM TermExt, TERM TermExt)] -> [VarSet]
forall a b. (a -> b) -> [a] -> [b]
map (\ (p :: TERM TermExt
p, t :: TERM TermExt
t) -> VarSet -> VarSet -> VarSet
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (Sign TermExt e -> TERM TermExt -> VarSet
forall f e. TermExtension f => Sign f e -> TERM f -> VarSet
freeTermVars Sign TermExt e
s TERM TermExt
t) (VarSet -> VarSet) -> VarSet -> VarSet
forall a b. (a -> b) -> a -> b
$ Sign TermExt e -> TERM TermExt -> VarSet
forall f e. TermExtension f => Sign f e -> TERM f -> VarSet
freeTermVars Sign TermExt e
s TERM TermExt
p) [(TERM TermExt, TERM TermExt)]
l
    Let fd :: FunDef
fd t :: TERM TermExt
t _ -> VarSet -> VarSet -> VarSet
forall a. Ord a => Set a -> Set a -> Set a
Set.difference
      (VarSet -> VarSet -> VarSet
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Sign TermExt e -> FunDef -> VarSet
forall e. Sign TermExt e -> FunDef -> VarSet
freeFunDefVars Sign TermExt e
s FunDef
fd) (VarSet -> VarSet) -> VarSet -> VarSet
forall a b. (a -> b) -> a -> b
$ Sign TermExt e -> TERM TermExt -> VarSet
forall f e. TermExtension f => Sign f e -> TERM f -> VarSet
freeTermVars Sign TermExt e
s TERM TermExt
t)
      (VarSet -> VarSet) -> VarSet -> VarSet
forall a b. (a -> b) -> a -> b
$ [(Token, Id)] -> VarSet
forall a. Ord a => [a] -> Set a
Set.fromList ([(Token, Id)] -> VarSet) -> [(Token, Id)] -> VarSet
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> [(Token, Id)]
flatVAR_DECLs ([VAR_DECL] -> [(Token, Id)]) -> [VAR_DECL] -> [(Token, Id)]
forall a b. (a -> b) -> a -> b
$ FunDef -> [VAR_DECL]
letVars FunDef
fd
    IfThenElse f :: TERM TermExt
f t :: TERM TermExt
t e :: TERM TermExt
e _ -> [VarSet] -> VarSet
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([VarSet] -> VarSet) -> [VarSet] -> VarSet
forall a b. (a -> b) -> a -> b
$ (TERM TermExt -> VarSet) -> [TERM TermExt] -> [VarSet]
forall a b. (a -> b) -> [a] -> [b]
map (Sign TermExt e -> TERM TermExt -> VarSet
forall f e. TermExtension f => Sign f e -> TERM f -> VarSet
freeTermVars Sign TermExt e
s) [TERM TermExt
f, TERM TermExt
t, TERM TermExt
e]
    EqTerm t :: TERM TermExt
t e :: TERM TermExt
e _ -> [VarSet] -> VarSet
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([VarSet] -> VarSet) -> [VarSet] -> VarSet
forall a b. (a -> b) -> a -> b
$ (TERM TermExt -> VarSet) -> [TERM TermExt] -> [VarSet]
forall a b. (a -> b) -> [a] -> [b]
map (Sign TermExt e -> TERM TermExt -> VarSet
forall f e. TermExtension f => Sign f e -> TERM f -> VarSet
freeTermVars Sign TermExt e
s) [TERM TermExt
t, TERM TermExt
e]
    BoolTerm t :: TERM TermExt
t -> Sign TermExt e -> TERM TermExt -> VarSet
forall f e. TermExtension f => Sign f e -> TERM f -> VarSet
freeTermVars Sign TermExt e
s TERM TermExt
t

  optTermSort :: TermExt -> Maybe Id
optTermSort te :: TermExt
te = case TermExt
te of
      Case _ ((_, t :: TERM TermExt
t) : _) _ -> TERM TermExt -> Maybe Id
forall f. TermExtension f => f -> Maybe Id
optTermSort TERM TermExt
t
      Let _ t :: TERM TermExt
t _ -> TERM TermExt -> Maybe Id
forall f. TermExtension f => f -> Maybe Id
optTermSort TERM TermExt
t
      IfThenElse _ t :: TERM TermExt
t _ _ -> TERM TermExt -> Maybe Id
forall f. TermExtension f => f -> Maybe Id
optTermSort TERM TermExt
t
      EqTerm {} -> Id -> Maybe Id
forall a. a -> Maybe a
Just Id
boolSort
      BoolTerm t :: TERM TermExt
t -> TERM TermExt -> Maybe Id
forall f. TermExtension f => f -> Maybe Id
optTermSort TERM TermExt
t
      _ -> Maybe Id
forall a. Maybe a
Nothing -- all others are formulas
  termToFormula :: TERM TermExt -> Result FplForm
termToFormula t :: TERM TermExt
t = let s :: Id
s = TERM TermExt -> Id
forall f. TermExtension f => f -> Id
sortOfTerm TERM TermExt
t in
        if Id
s Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
boolSort
        then FplForm -> Result FplForm
forall (m :: * -> *) a. Monad m => a -> m a
return (FplForm -> Result FplForm) -> FplForm -> Result FplForm
forall a b. (a -> b) -> a -> b
$ TermExt -> FplForm
forall f. f -> FORMULA f
ExtFORMULA (TermExt -> FplForm) -> TermExt -> FplForm
forall a b. (a -> b) -> a -> b
$ TERM TermExt -> TermExt
BoolTerm TERM TermExt
t
        else [Char] -> Result FplForm
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
Fail.fail ([Char] -> Result FplForm) -> [Char] -> Result FplForm
forall a b. (a -> b) -> a -> b
$ "expected boolean term but found sort: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Id -> [Char]
forall a. Show a => a -> [Char]
show Id
s

simplifyTermExt :: FplSign -> TermExt -> TermExt
simplifyTermExt :: FplSign -> TermExt -> TermExt
simplifyTermExt s :: FplSign
s te :: TermExt
te = let rec :: FplSign -> TERM TermExt -> TERM TermExt
rec = Min TermExt SignExt
-> (FplSign -> TermExt -> TermExt)
-> FplSign
-> TERM TermExt
-> TERM TermExt
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> (Sign f e -> f -> f) -> Sign f e -> TERM f -> TERM f
simplifyTerm Min TermExt SignExt
minFplTerm FplSign -> TermExt -> TermExt
simplifyTermExt in
  case TermExt
te of
    FixDef fd :: FunDef
fd -> FunDef -> TermExt
FixDef (FunDef -> TermExt) -> FunDef -> TermExt
forall a b. (a -> b) -> a -> b
$ FplSign -> FunDef -> FunDef
simplifyFunDef FplSign
s FunDef
fd
    Case o :: TERM TermExt
o l :: [(TERM TermExt, TERM TermExt)]
l r :: Range
r -> TERM TermExt -> [(TERM TermExt, TERM TermExt)] -> Range -> TermExt
Case (FplSign -> TERM TermExt -> TERM TermExt
rec FplSign
s TERM TermExt
o)
      (((TERM TermExt, TERM TermExt) -> (TERM TermExt, TERM TermExt))
-> [(TERM TermExt, TERM TermExt)] -> [(TERM TermExt, TERM TermExt)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (p :: TERM TermExt
p, t :: TERM TermExt
t) -> let
                vs :: VarSet
vs = FplSign -> TERM TermExt -> VarSet
forall f e. TermExtension f => Sign f e -> TERM f -> VarSet
freeTermVars FplSign
s TERM TermExt
p
                newSign :: FplSign
newSign = State FplSign () -> FplSign -> FplSign
forall s a. State s a -> s -> s
execState
                  (((Token, Id) -> State FplSign ())
-> [(Token, Id)] -> State FplSign ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((Token -> Id -> State FplSign ())
-> (Token, Id) -> State FplSign ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((Token -> Id -> State FplSign ())
 -> (Token, Id) -> State FplSign ())
-> (Token -> Id -> State FplSign ())
-> (Token, Id)
-> State FplSign ()
forall a b. (a -> b) -> a -> b
$ (Id -> Token -> State FplSign ())
-> Token -> Id -> State FplSign ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip Id -> Token -> State FplSign ()
forall f e. Id -> Token -> State (Sign f e) ()
addVar) ([(Token, Id)] -> State FplSign ())
-> [(Token, Id)] -> State FplSign ()
forall a b. (a -> b) -> a -> b
$ VarSet -> [(Token, Id)]
forall a. Set a -> [a]
Set.toList VarSet
vs) FplSign
s
                in (FplSign -> TERM TermExt -> TERM TermExt
rec FplSign
newSign TERM TermExt
p, FplSign -> TERM TermExt -> TERM TermExt
rec FplSign
newSign TERM TermExt
t)) [(TERM TermExt, TERM TermExt)]
l) Range
r
    Let fd :: FunDef
fd t :: TERM TermExt
t r :: Range
r ->
      let newSign :: FplSign
newSign = State FplSign () -> FplSign -> FplSign
forall s a. State s a -> s -> s
execState (FunDef -> State FplSign ()
addFunToSign FunDef
fd) FplSign
s
          sign2 :: FplSign
sign2 = State FplSign () -> FplSign -> FplSign
forall s a. State s a -> s -> s
execState (FunDef -> State FplSign ()
addFunVar FunDef
fd) FplSign
newSign
      in FunDef -> TERM TermExt -> Range -> TermExt
Let (FplSign -> FunDef -> FunDef
simplifyFunDef FplSign
newSign FunDef
fd)
            (FplSign -> TERM TermExt -> TERM TermExt
rec FplSign
sign2 TERM TermExt
t) Range
r
    IfThenElse f :: TERM TermExt
f t :: TERM TermExt
t e :: TERM TermExt
e r :: Range
r -> TERM TermExt -> TERM TermExt -> TERM TermExt -> Range -> TermExt
IfThenElse (FplSign -> TERM TermExt -> TERM TermExt
rec FplSign
s TERM TermExt
f) (FplSign -> TERM TermExt -> TERM TermExt
rec FplSign
s TERM TermExt
t) (FplSign -> TERM TermExt -> TERM TermExt
rec FplSign
s TERM TermExt
e) Range
r
    EqTerm t :: TERM TermExt
t e :: TERM TermExt
e r :: Range
r -> TERM TermExt -> TERM TermExt -> Range -> TermExt
EqTerm (FplSign -> TERM TermExt -> TERM TermExt
rec FplSign
s TERM TermExt
t) (FplSign -> TERM TermExt -> TERM TermExt
rec FplSign
s TERM TermExt
e) Range
r
    BoolTerm t :: TERM TermExt
t -> TERM TermExt -> TermExt
BoolTerm (FplSign -> TERM TermExt -> TERM TermExt
rec FplSign
s TERM TermExt
t)

simplifyFunDef :: FplSign -> FunDef -> FunDef
simplifyFunDef :: FplSign -> FunDef -> FunDef
simplifyFunDef sig :: FplSign
sig fd :: FunDef
fd@(FunDef o :: Id
o h :: OP_HEAD
h@(Op_head _ vs :: [VAR_DECL]
vs _ _) at :: Annoted (TERM TermExt)
at r :: Range
r) =
   let newSign :: FplSign
newSign = State FplSign () -> FplSign -> FplSign
forall s a. State s a -> s -> s
execState ((VAR_DECL -> State FplSign ()) -> [VAR_DECL] -> State FplSign ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ VAR_DECL -> State FplSign ()
forall f e. VAR_DECL -> State (Sign f e) ()
addVars [VAR_DECL]
vs State FplSign () -> State FplSign () -> State FplSign ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FunDef -> State FplSign ()
addFunToSign FunDef
fd) FplSign
sig
   in Id -> OP_HEAD -> Annoted (TERM TermExt) -> Range -> FunDef
FunDef Id
o OP_HEAD
h ((TERM TermExt -> TERM TermExt)
-> Annoted (TERM TermExt) -> Annoted (TERM TermExt)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Min TermExt SignExt
-> (FplSign -> TermExt -> TermExt)
-> FplSign
-> TERM TermExt
-> TERM TermExt
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> (Sign f e -> f -> f) -> Sign f e -> TERM f -> TERM f
simplifyTerm Min TermExt SignExt
minFplTerm FplSign -> TermExt -> TermExt
simplifyTermExt FplSign
newSign) Annoted (TERM TermExt)
at) Range
r