{-# LANGUAGE GADTs, PatternGuards #-}
module Jukebox.Tools.EncodeTypes where

import Jukebox.Tools.Clausify(split, removeEquiv, run, withName)
import Jukebox.Name
import Jukebox.Form hiding (run)
import qualified Jukebox.Form as Form
import Jukebox.Options
import Control.Monad hiding (guard)
import Data.Monoid
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set

data Scheme = Scheme {
  Scheme -> Type -> NameM Function
makeFunction :: Type -> NameM Function,
  Scheme -> (Type -> Bool) -> (Type -> Function) -> Scheme1
scheme1 :: (Type -> Bool) -> (Type -> Function) -> Scheme1
  }

data Scheme1 = Scheme1 {
  Scheme1 -> Bind Form -> Form
forAll :: Bind Form -> Form,
  Scheme1 -> Bind Form -> Form
exists :: Bind Form -> Form,
  Scheme1 -> Term -> Term -> Form
equals :: Term -> Term -> Form,
  Scheme1 -> Function -> NameM Form
funcAxiom :: Function -> NameM Form,
  Scheme1 -> Type -> NameM Form
typeAxiom :: Type -> NameM Form
  }

guard :: Scheme1 -> (Type -> Bool) -> Input Form -> Input Form
guard :: Scheme1 -> (Type -> Bool) -> Input Form -> Input Form
guard Scheme1
scheme Type -> Bool
mono (Input Tag
t Kind
k InputSource
info Form
f) = Tag -> Kind -> InputSource -> Form -> Input Form
forall a. Tag -> Kind -> InputSource -> a -> Input a
Input Tag
t Kind
k InputSource
info (Bool -> Form -> Form
aux (Kind -> Bool
pos Kind
k) Form
f)
  where aux :: Bool -> Form -> Form
aux Bool
pos (ForAll (Bind Set Variable
vs Form
f))
          | Bool
pos = Scheme1 -> Bind Form -> Form
forAll Scheme1
scheme (Set Variable -> Form -> Bind Form
forall a. Set Variable -> a -> Bind a
Bind Set Variable
vs (Bool -> Form -> Form
aux Bool
pos Form
f))
          | Bool
otherwise = Form -> Form
notInwards (Scheme1 -> Bind Form -> Form
exists Scheme1
scheme (Set Variable -> Form -> Bind Form
forall a. Set Variable -> a -> Bind a
Bind Set Variable
vs (Form -> Form
Not (Bool -> Form -> Form
aux Bool
pos Form
f))))
        aux Bool
pos (Exists (Bind Set Variable
vs Form
f))
          | Bool
pos = Scheme1 -> Bind Form -> Form
exists Scheme1
scheme (Set Variable -> Form -> Bind Form
forall a. Set Variable -> a -> Bind a
Bind Set Variable
vs (Bool -> Form -> Form
aux Bool
pos Form
f))
          | Bool
otherwise = Form -> Form
notInwards (Scheme1 -> Bind Form -> Form
forAll Scheme1
scheme (Set Variable -> Form -> Bind Form
forall a. Set Variable -> a -> Bind a
Bind Set Variable
vs (Form -> Form
Not (Bool -> Form -> Form
aux Bool
pos Form
f))))
        aux Bool
_pos (Literal (Pos (Term
t :=: Term
u)))
          | Bool -> Bool
not (Type -> Bool
mono (Term -> Type
forall a. Typed a => a -> Type
typ Term
t)) = Scheme1 -> Term -> Term -> Form
equals Scheme1
scheme Term
t Term
u
        aux Bool
_pos (Literal (Neg (Term
t :=: Term
u)))
          | Bool -> Bool
not (Type -> Bool
mono (Term -> Type
forall a. Typed a => a -> Type
typ Term
t)) = Form -> Form
Not (Scheme1 -> Term -> Term -> Form
equals Scheme1
scheme Term
t Term
u)
        aux Bool
_pos l :: Form
l@Literal{} = Form
l
        aux Bool
pos (Not Form
f) = Form -> Form
Not (Bool -> Form -> Form
aux (Bool -> Bool
not Bool
pos) Form
f)
        aux Bool
pos (And [Form]
fs) = [Form] -> Form
And ((Form -> Form) -> [Form] -> [Form]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Bool -> Form -> Form
aux Bool
pos) [Form]
fs)
        aux Bool
pos (Or [Form]
fs) = [Form] -> Form
Or ((Form -> Form) -> [Form] -> [Form]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Bool -> Form -> Form
aux Bool
pos) [Form]
fs)
        aux Bool
_pos (Equiv Form
_ Form
_) = Tag -> Form
forall a. HasCallStack => Tag -> a
error Tag
"ToFOF.guard: equiv should have been eliminated"
        aux Bool
_pos (Connective Connective
_ Form
_ Form
_) = Tag -> Form
forall a. HasCallStack => Tag -> a
error Tag
"ToFOF.guard: connective should have been eliminated"
        pos :: Kind -> Bool
pos Ax{} = Bool
True
        pos Conj{} = Bool
False

translate, translate1 :: Scheme -> (Type -> Bool) -> Problem Form -> Problem Form
translate1 :: Scheme -> (Type -> Bool) -> Problem Form -> Problem Form
translate1 Scheme
scheme Type -> Bool
mono Problem Form
f = Problem Form
-> (Problem Form -> NameM (Problem Form)) -> Problem Form
forall a b. Symbolic a => a -> (a -> NameM b) -> b
Form.run Problem Form
f ((Problem Form -> NameM (Problem Form)) -> Problem Form)
-> (Problem Form -> NameM (Problem Form)) -> Problem Form
forall a b. (a -> b) -> a -> b
$ \Problem Form
inps -> do
  let tys :: [Type]
tys = Problem Form -> [Type]
forall a. Symbolic a => a -> [Type]
types' Problem Form
inps
      funcs :: [Function]
funcs = Problem Form -> [Function]
forall a. Symbolic a => a -> [Function]
functions Problem Form
inps
      -- Hardly any use adding guards if there's only one type.
      mono' :: Type -> Bool
mono' | [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = Bool -> Type -> Bool
forall a b. a -> b -> a
const Bool
True
            | Bool
otherwise = Type -> Bool
mono
  [Function]
typeFuncs <- (Type -> NameM Function) -> [Type] -> NameM [Function]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Scheme -> Type -> NameM Function
makeFunction Scheme
scheme) [Type]
tys
  let typeMap :: Map Type Function
typeMap = [(Type, Function)] -> Map Type Function
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([Type] -> [Function] -> [(Type, Function)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Type]
tys [Function]
typeFuncs)
      lookupType :: Type -> Function
lookupType Type
ty =
        case Type -> Map Type Function -> Maybe Function
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Type
ty Map Type Function
typeMap of
          Just Function
f -> Function
f
          Maybe Function
Nothing -> Tag -> Function
forall a. HasCallStack => Tag -> a
error Tag
"ToFOF.translate: type not found"
      scheme1' :: Scheme1
scheme1' = Scheme -> (Type -> Bool) -> (Type -> Function) -> Scheme1
scheme1 Scheme
scheme Type -> Bool
mono' Type -> Function
lookupType
  [Form]
funcAxioms <- (Function -> NameM Form) -> [Function] -> NameM [Form]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Scheme1 -> Function -> NameM Form
funcAxiom Scheme1
scheme1') [Function]
funcs
  [Form]
typeAxioms <- (Type -> NameM Form) -> [Type] -> NameM [Form]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Scheme1 -> Type -> NameM Form
typeAxiom Scheme1
scheme1') [Type]
tys
  let axioms :: [Form]
axioms =
        (Form -> Form) -> [Form] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map (Form -> Form
simplify (Form -> Form) -> (Form -> Form) -> Form -> Form
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bind Form -> Form
ForAll (Bind Form -> Form) -> (Form -> Bind Form) -> Form -> Form
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Form -> Bind Form
forall a. Symbolic a => a -> Bind a
bind) ([Form] -> [Form]) -> ([Form] -> [Form]) -> [Form] -> [Form]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Form -> [Form]
split (Form -> [Form]) -> ([Form] -> Form) -> [Form] -> [Form]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Form -> Form
simplify (Form -> Form) -> ([Form] -> Form) -> [Form] -> Form
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Form -> Form -> Form) -> Form -> [Form] -> Form
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Form -> Form -> Form
(/\) Form
true ([Form] -> [Form]) -> [Form] -> [Form]
forall a b. (a -> b) -> a -> b
$
          [Form]
funcAxioms [Form] -> [Form] -> [Form]
forall a. [a] -> [a] -> [a]
++ [Form]
typeAxioms
  Problem Form -> NameM (Problem Form)
forall (m :: * -> *) a. Monad m => a -> m a
return (Problem Form -> NameM (Problem Form))
-> Problem Form -> NameM (Problem Form)
forall a b. (a -> b) -> a -> b
$
    [ Tag -> Kind -> InputSource -> Form -> Input Form
forall a. Tag -> Kind -> InputSource -> a -> Input a
Input (Tag
"types" Tag -> Tag -> Tag
forall a. [a] -> [a] -> [a]
++ Integer -> Tag
forall a. Show a => a -> Tag
show Integer
i) (AxKind -> Kind
Ax AxKind
Axiom) (Tag -> Tag -> Problem Form -> InputSource
Inference Tag
"type_axiom" Tag
"esa" []) Form
axiom | (Form
axiom, Integer
i) <- [Form] -> [Integer] -> [(Form, Integer)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Form]
axioms [Integer
1..] ] Problem Form -> Problem Form -> Problem Form
forall a. [a] -> [a] -> [a]
++
    (Input Form -> Input Form) -> Problem Form -> Problem Form
forall a b. (a -> b) -> [a] -> [b]
map (Scheme1 -> (Type -> Bool) -> Input Form -> Input Form
guard Scheme1
scheme1' Type -> Bool
mono') Problem Form
inps

translate :: Scheme -> (Type -> Bool) -> Problem Form -> Problem Form
translate Scheme
scheme Type -> Bool
mono Problem Form
f =
  let f' :: Problem Form
f' =
        Problem Form
-> (Problem Form -> NameM (Problem Form)) -> Problem Form
forall a b. Symbolic a => a -> (a -> NameM b) -> b
Form.run Problem Form
f ((Problem Form -> NameM (Problem Form)) -> Problem Form)
-> (Problem Form -> NameM (Problem Form)) -> Problem Form
forall a b. (a -> b) -> a -> b
$ \Problem Form
inps -> do
          Problem Form
-> (Input Form -> NameM (Input Form)) -> NameM (Problem Form)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM Problem Form
inps ((Input Form -> NameM (Input Form)) -> NameM (Problem Form))
-> (Input Form -> NameM (Input Form)) -> NameM (Problem Form)
forall a b. (a -> b) -> a -> b
$ \inp :: Input Form
inp@(Input Tag
tag Kind
kind InputSource
_ Form
f) -> do
            let prepare :: Form -> NameM Form
prepare Form
f = ([Form] -> Form) -> NameM [Form] -> NameM Form
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Form -> Form -> Form) -> Form -> [Form] -> Form
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Form -> Form -> Form
(/\) Form
true) (M [Form] -> NameM [Form]
forall a. M a -> NameM a
run (Tag -> M [Form] -> M [Form]
forall a. Tag -> M a -> M a
withName Tag
tag (Form -> M [Form]
removeEquiv (Form -> Form
simplify Form
f))))
            case Kind
kind of
              Ax{} ->
                (Form -> Input Form) -> NameM Form -> NameM (Input Form)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Tag -> Kind -> InputSource -> Form -> Input Form
forall a. Tag -> Kind -> InputSource -> a -> Input a
Input Tag
tag Kind
kind (Tag -> Tag -> Problem Form -> InputSource
Inference Tag
"type_encoding" Tag
"esa" [Input Form
inp])) (NameM Form -> NameM (Input Form))
-> NameM Form -> NameM (Input Form)
forall a b. (a -> b) -> a -> b
$
                  Form -> NameM Form
prepare Form
f
              Conj{} ->
                (Form -> Input Form) -> NameM Form -> NameM (Input Form)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Tag -> Kind -> InputSource -> Form -> Input Form
forall a. Tag -> Kind -> InputSource -> a -> Input a
Input Tag
tag Kind
kind (Tag -> Tag -> Problem Form -> InputSource
Inference Tag
"type_encoding" Tag
"esa" [Input Form
inp])) (NameM Form -> NameM (Input Form))
-> NameM Form -> NameM (Input Form)
forall a b. (a -> b) -> a -> b
$
                (Form -> Form) -> NameM Form -> NameM Form
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Form -> Form
notInwards (NameM Form -> NameM Form) -> NameM Form -> NameM Form
forall a b. (a -> b) -> a -> b
$ Form -> NameM Form
prepare (Form -> NameM Form) -> Form -> NameM Form
forall a b. (a -> b) -> a -> b
$ Form -> Form
nt Form
f
      trType :: Type -> Type
trType Type
O = Type
O
      trType Type
_ = Type
indType
      quoteNumbers :: b -> Name -> Name
quoteNumbers b
tagName Name
name
        | Name -> Bool
isNumber Name
name = Name
name Name -> [b] -> Name
forall a b. (Named a, Named b) => a -> [b] -> Name
`variant` [b
tagName]
        | Bool
otherwise = Name
name
      isNumber :: Name -> Bool
isNumber (Fixed (Integer Integer
_) Maybe Tag
_) = Bool
True
      isNumber (Fixed (Rational Rational
_) Maybe Tag
_) = Bool
True
      isNumber (Fixed (Real Rational
_) Maybe Tag
_) = Bool
True
      isNumber Name
_ = Bool
False

  in Problem Form
-> (Problem Form -> NameM (Problem Form)) -> Problem Form
forall a b. Symbolic a => a -> (a -> NameM b) -> b
Form.run (Scheme -> (Type -> Bool) -> Problem Form -> Problem Form
translate1 Scheme
scheme Type -> Bool
mono Problem Form
f') ((Problem Form -> NameM (Problem Form)) -> Problem Form)
-> (Problem Form -> NameM (Problem Form)) -> Problem Form
forall a b. (a -> b) -> a -> b
$ \Problem Form
form -> do
    Name
name <- Tag -> NameM Name
forall a. Named a => a -> NameM Name
newName Tag
""
    Problem Form -> NameM (Problem Form)
forall (m :: * -> *) a. Monad m => a -> m a
return (Problem Form -> NameM (Problem Form))
-> Problem Form -> NameM (Problem Form)
forall a b. (a -> b) -> a -> b
$ (Name -> Name) -> Problem Form -> Problem Form
forall a. Symbolic a => (Name -> Name) -> a -> a
mapName (Name -> Name -> Name
forall b. Named b => b -> Name -> Name
quoteNumbers Name
name) (Problem Form -> Problem Form) -> Problem Form -> Problem Form
forall a b. (a -> b) -> a -> b
$ (Type -> Type) -> Problem Form -> Problem Form
forall a. Symbolic a => (Type -> Type) -> a -> a
mapType Type -> Type
trType Problem Form
form

-- Typing functions.

tagsFlags :: OptionParser Bool
tagsFlags :: OptionParser Bool
tagsFlags =
  Tag -> OptionParser Bool -> OptionParser Bool
forall a. Tag -> OptionParser a -> OptionParser a
inGroup Tag
"Options for encoding types" (OptionParser Bool -> OptionParser Bool)
-> OptionParser Bool -> OptionParser Bool
forall a b. (a -> b) -> a -> b
$
  Tag -> [Tag] -> Bool -> OptionParser Bool
bool Tag
"more-axioms"
    [Tag
"Add extra, redundant typing axioms for function arguments (on by default).",
     Tag
"Improves performance on provers which use equations as rewrite rules",
     Tag
"to simplify discovered facts. May harm performance on other provers.",
     Tag
"Only affects --encoding tags."]
    Bool
True

tags :: Bool -> Scheme
tags :: Bool -> Scheme
tags Bool
moreAxioms = Scheme :: (Type -> NameM Function)
-> ((Type -> Bool) -> (Type -> Function) -> Scheme1) -> Scheme
Scheme
  { makeFunction :: Type -> NameM Function
makeFunction = \Type
ty ->
      Name -> [Type] -> Type -> NameM Function
forall a. Named a => a -> [Type] -> Type -> NameM Function
newFunction (Tag -> Name -> Name
withLabel Tag
"type_tag" (Tag -> Name
forall a. Named a => a -> Name
name (Tag
"to_" Tag -> Tag -> Tag
forall a. [a] -> [a] -> [a]
++ Type -> Tag
forall a. Named a => a -> Tag
base Type
ty))) [Type
ty] Type
ty,
    scheme1 :: (Type -> Bool) -> (Type -> Function) -> Scheme1
scheme1 = Bool -> (Type -> Bool) -> (Type -> Function) -> Scheme1
tags1 Bool
moreAxioms }

tags1 :: Bool -> (Type -> Bool) -> (Type -> Function) -> Scheme1
tags1 :: Bool -> (Type -> Bool) -> (Type -> Function) -> Scheme1
tags1 Bool
moreAxioms Type -> Bool
mono Type -> Function
fs = Scheme1 :: (Bind Form -> Form)
-> (Bind Form -> Form)
-> (Term -> Term -> Form)
-> (Function -> NameM Form)
-> (Type -> NameM Form)
-> Scheme1
Scheme1
  { forAll :: Bind Form -> Form
forAll = Bind Form -> Form
ForAll,
    exists :: Bind Form -> Form
exists = \(Bind Set Variable
vs Form
f) ->
       let bound :: Form
bound = (Form -> Form -> Form) -> Form -> [Form] -> Form
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Form -> Form -> Form
(/\) Form
true ((Variable -> Form) -> [Variable] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map Variable -> Form
guard (Set Variable -> [Variable]
forall a. Set a -> [a]
Set.toList Set Variable
vs))
           guard :: Variable -> Form
guard Variable
v | Type -> Bool
mono (Variable -> Type
forall a. Typed a => a -> Type
typ Variable
v) = Form
true
                   | Bool
otherwise = Signed Atomic -> Form
Literal (Atomic -> Signed Atomic
forall a. a -> Signed a
Pos (Type -> Function
fs (Variable -> Type
forall a. Typed a => a -> Type
typ Variable
v) Function -> [Term] -> Term
:@: [Variable -> Term
Var Variable
v] Term -> Term -> Atomic
:=: Variable -> Term
Var Variable
v))
       in Bind Form -> Form
Exists (Set Variable -> Form -> Bind Form
forall a. Set Variable -> a -> Bind a
Bind Set Variable
vs (Form -> Form
simplify Form
bound Form -> Form -> Form
/\ Form
f)),
    equals :: Term -> Term -> Form
equals =
      \Term
t Term
u ->
        let protect :: Term -> Term
protect t :: Term
t@Var{} = Type -> Function
fs (Term -> Type
forall a. Typed a => a -> Type
typ Term
t) Function -> [Term] -> Term
:@: [Term
t]
            protect Term
t = Term
t
        in Signed Atomic -> Form
Literal (Atomic -> Signed Atomic
forall a. a -> Signed a
Pos (Term -> Term
protect Term
t Term -> Term -> Atomic
:=: Term -> Term
protect Term
u)),
    funcAxiom :: Function -> NameM Form
funcAxiom = Bool
-> (Type -> Bool) -> (Type -> Function) -> Function -> NameM Form
tagsAxiom Bool
moreAxioms Type -> Bool
mono Type -> Function
fs,
    typeAxiom :: Type -> NameM Form
typeAxiom = \Type
ty -> if Bool
moreAxioms then Bool
-> (Type -> Bool) -> (Type -> Function) -> Function -> NameM Form
tagsAxiom Bool
False Type -> Bool
mono Type -> Function
fs (Type -> Function
fs Type
ty) else (Type -> Bool) -> Type -> Function -> NameM Form
tagsExists Type -> Bool
mono Type
ty (Type -> Function
fs Type
ty) }

tagsAxiom :: Bool -> (Type -> Bool) -> (Type -> Function) -> Function -> NameM Form
tagsAxiom :: Bool
-> (Type -> Bool) -> (Type -> Function) -> Function -> NameM Form
tagsAxiom Bool
moreAxioms Type -> Bool
mono Type -> Function
fs f :: Function
f@(Name
_ ::: FunType [Type]
args Type
_res) = do
  [Term]
vs <- [Type] -> (Type -> NameM Term) -> NameM [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Type]
args ((Type -> NameM Term) -> NameM [Term])
-> (Type -> NameM Term) -> NameM [Term]
forall a b. (a -> b) -> a -> b
$ \Type
ty ->
    (Variable -> Term) -> NameM Variable -> NameM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Variable -> Term
Var (Tag -> Type -> NameM Variable
forall a b. Named a => a -> b -> NameM (Name ::: b)
newSymbol Tag
"X" Type
ty)
  let t :: Term
t = Function
f Function -> [Term] -> Term
:@: [Term]
vs
      at :: Int -> (a -> a) -> [a] -> [a]
at Int
n a -> a
f [a]
xs = Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take Int
n [a]
xs [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a -> a
f ([a]
xs [a] -> Int -> a
forall a. [a] -> Int -> a
!! Int
n)] [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
drop (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) [a]
xs
      tag :: Term -> Term
tag Term
t = Type -> Function
fs (Term -> Type
forall a. Typed a => a -> Type
typ Term
t) Function -> [Term] -> Term
:@: [Term
t]
      equate :: (Type, Term) -> Form
equate (Type
ty, Term
t') | Type -> Bool
mono Type
ty = Form
true
                      | Bool
otherwise = Term
t Term -> Term -> Form
`eq` Term
t'
      Term
t eq :: Term -> Term -> Form
`eq` Term
u | Term -> Type
forall a. Typed a => a -> Type
typ Term
t Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
O = Signed Atomic -> Form
Literal (Atomic -> Signed Atomic
forall a. a -> Signed a
Pos (Term -> Atomic
Tru Term
t)) Form -> Form -> Form
`Equiv` Signed Atomic -> Form
Literal (Atomic -> Signed Atomic
forall a. a -> Signed a
Pos (Term -> Atomic
Tru Term
u))
               | Bool
otherwise = Signed Atomic -> Form
Literal (Atomic -> Signed Atomic
forall a. a -> Signed a
Pos (Term
t Term -> Term -> Atomic
:=: Term
u))
      ts :: [(Type, Term)]
ts = (Term -> Type
forall a. Typed a => a -> Type
typ Term
t, Term -> Term
tag Term
t)(Type, Term) -> [(Type, Term)] -> [(Type, Term)]
forall a. a -> [a] -> [a]
:
           [ (Term -> Type
forall a. Typed a => a -> Type
typ ([Term]
vs [Term] -> Int -> Term
forall a. [a] -> Int -> a
!! Int
n), Function
f Function -> [Term] -> Term
:@: Int -> (Term -> Term) -> [Term] -> [Term]
forall a. Int -> (a -> a) -> [a] -> [a]
at Int
n Term -> Term
tag [Term]
vs)
           | Bool
moreAxioms,
             Int
n <- [Int
0..[Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
vsInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1] ]
  Form -> NameM Form
forall (m :: * -> *) a. Monad m => a -> m a
return ((Form -> Form -> Form) -> Form -> [Form] -> Form
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Form -> Form -> Form
(/\) Form
true (((Type, Term) -> Form) -> [(Type, Term)] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map (Type, Term) -> Form
equate [(Type, Term)]
ts))

tagsExists :: (Type -> Bool) -> Type -> Function -> NameM Form
tagsExists :: (Type -> Bool) -> Type -> Function -> NameM Form
tagsExists Type -> Bool
mono Type
ty Function
f
  | Type -> Bool
mono Type
ty = Form -> NameM Form
forall (m :: * -> *) a. Monad m => a -> m a
return Form
true
  | Bool
otherwise = do
      Term
v <- (Variable -> Term) -> NameM Variable -> NameM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Variable -> Term
Var (Tag -> Type -> NameM Variable
forall a b. Named a => a -> b -> NameM (Name ::: b)
newSymbol Tag
"X" Type
ty)
      Form -> NameM Form
forall (m :: * -> *) a. Monad m => a -> m a
return (Bind Form -> Form
Exists (Form -> Bind Form
forall a. Symbolic a => a -> Bind a
bind (Signed Atomic -> Form
Literal (Atomic -> Signed Atomic
forall a. a -> Signed a
Pos (Function
f Function -> [Term] -> Term
:@: [Term
v] Term -> Term -> Atomic
:=: Term
v)))))

-- Typing predicates.

guards :: Scheme
guards :: Scheme
guards = Scheme :: (Type -> NameM Function)
-> ((Type -> Bool) -> (Type -> Function) -> Scheme1) -> Scheme
Scheme
  { makeFunction :: Type -> NameM Function
makeFunction = \Type
ty ->
      Name -> [Type] -> Type -> NameM Function
forall a. Named a => a -> [Type] -> Type -> NameM Function
newFunction (Tag -> Name -> Name
withLabel Tag
"type_pred" (Tag -> Name
forall a. Named a => a -> Name
name (Tag
"is_" Tag -> Tag -> Tag
forall a. [a] -> [a] -> [a]
++ Type -> Tag
forall a. Named a => a -> Tag
base Type
ty))) [Type
ty] Type
O,
    scheme1 :: (Type -> Bool) -> (Type -> Function) -> Scheme1
scheme1 = (Type -> Bool) -> (Type -> Function) -> Scheme1
guards1 }

guards1 :: (Type -> Bool) -> (Type -> Function) -> Scheme1
guards1 :: (Type -> Bool) -> (Type -> Function) -> Scheme1
guards1 Type -> Bool
mono Type -> Function
ps = Scheme1 :: (Bind Form -> Form)
-> (Bind Form -> Form)
-> (Term -> Term -> Form)
-> (Function -> NameM Form)
-> (Type -> NameM Form)
-> Scheme1
Scheme1
  { forAll :: Bind Form -> Form
forAll = \(Bind Set Variable
vs Form
f) ->
       let bound :: Form
bound = (Form -> Form -> Form) -> Form -> [Form] -> Form
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Form -> Form -> Form
(/\) Form
true ((Variable -> Form) -> [Variable] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map Variable -> Form
guard (Set Variable -> [Variable]
forall a. Set a -> [a]
Set.toList Set Variable
vs))
           guard :: Variable -> Form
guard Variable
v | Type -> Bool
mono (Variable -> Type
forall a. Typed a => a -> Type
typ Variable
v) = Form
true
                   | Bool -> Bool
not (Bool -> Variable -> Form -> Bool
forall a. Symbolic a => Bool -> Variable -> a -> Bool
naked Bool
True Variable
v Form
f) = Form
true
                   | Bool
otherwise = Signed Atomic -> Form
Literal (Atomic -> Signed Atomic
forall a. a -> Signed a
Pos (Term -> Atomic
Tru (Type -> Function
ps (Variable -> Type
forall a. Typed a => a -> Type
typ Variable
v) Function -> [Term] -> Term
:@: [Variable -> Term
Var Variable
v])))
       in Bind Form -> Form
ForAll (Set Variable -> Form -> Bind Form
forall a. Set Variable -> a -> Bind a
Bind Set Variable
vs (Form -> Form
simplify (Form -> Form
Not Form
bound) Form -> Form -> Form
\/ Form
f)),
    exists :: Bind Form -> Form
exists = \(Bind Set Variable
vs Form
f) ->
       let bound :: Form
bound = (Form -> Form -> Form) -> Form -> [Form] -> Form
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Form -> Form -> Form
(/\) Form
true ((Variable -> Form) -> [Variable] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map Variable -> Form
guard (Set Variable -> [Variable]
forall a. Set a -> [a]
Set.toList Set Variable
vs))
           guard :: Variable -> Form
guard Variable
v | Type -> Bool
mono (Variable -> Type
forall a. Typed a => a -> Type
typ Variable
v) = Form
true
--                   | not (naked True v f) = true
                   | Bool
otherwise = Signed Atomic -> Form
Literal (Atomic -> Signed Atomic
forall a. a -> Signed a
Pos (Term -> Atomic
Tru (Type -> Function
ps (Variable -> Type
forall a. Typed a => a -> Type
typ Variable
v) Function -> [Term] -> Term
:@: [Variable -> Term
Var Variable
v])))
       in Bind Form -> Form
Exists (Set Variable -> Form -> Bind Form
forall a. Set Variable -> a -> Bind a
Bind Set Variable
vs (Form -> Form
simplify Form
bound Form -> Form -> Form
/\ Form
f)),
    equals :: Term -> Term -> Form
equals = \Term
t Term
u -> Signed Atomic -> Form
Literal (Atomic -> Signed Atomic
forall a. a -> Signed a
Pos (Term
t Term -> Term -> Atomic
:=: Term
u)),
    funcAxiom :: Function -> NameM Form
funcAxiom = (Type -> Bool) -> (Type -> Function) -> Function -> NameM Form
guardsAxiom Type -> Bool
mono Type -> Function
ps,
    typeAxiom :: Type -> NameM Form
typeAxiom = (Type -> Bool) -> (Type -> Function) -> Type -> NameM Form
guardsTypeAxiom Type -> Bool
mono Type -> Function
ps }

naked :: Symbolic a => Bool -> Variable -> a -> Bool
naked :: Bool -> Variable -> a -> Bool
naked Bool
pos Variable
v a
f
  | TypeOf a
Form <- a -> TypeOf a
forall a. Symbolic a => a -> TypeOf a
typeOf a
f,
    Not f' <- a
f = Bool -> Variable -> Form -> Bool
forall a. Symbolic a => Bool -> Variable -> a -> Bool
naked (Bool -> Bool
not Bool
pos) Variable
v Form
f'
  | TypeOf a
Signed <- a -> TypeOf a
forall a. Symbolic a => a -> TypeOf a
typeOf a
f,
    Pos f' <- a
f = Bool -> Variable -> a -> Bool
forall a. Symbolic a => Bool -> Variable -> a -> Bool
naked Bool
pos Variable
v a
f'
  | TypeOf a
Signed <- a -> TypeOf a
forall a. Symbolic a => a -> TypeOf a
typeOf a
f,
    Neg f' <- a
f = Bool -> Variable -> a -> Bool
forall a. Symbolic a => Bool -> Variable -> a -> Bool
naked (Bool -> Bool
not Bool
pos) Variable
v a
f'
  | TypeOf a
Atomic <- a -> TypeOf a
forall a. Symbolic a => a -> TypeOf a
typeOf a
f,
    t :=: u <- a
f,
    Bool
pos = Term
t Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Variable -> Term
Var Variable
v Bool -> Bool -> Bool
|| Term
u Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Variable -> Term
Var Variable
v
  | TypeOf a
Bind_ <- a -> TypeOf a
forall a. Symbolic a => a -> TypeOf a
typeOf a
f,
    Bind vs f' <- a
f = Bool -> Bool
not (Variable -> Set Variable -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Variable
v Set Variable
vs) Bool -> Bool -> Bool
&& Bool -> Variable -> a -> Bool
forall a. Symbolic a => Bool -> Variable -> a -> Bool
naked Bool
pos Variable
v a
f'
  | Bool
otherwise = Any -> Bool
getAny ((forall a1. Symbolic a1 => a1 -> Any) -> a -> Any
forall a b.
(Symbolic a, Monoid b) =>
(forall a1. Symbolic a1 => a1 -> b) -> a -> b
collect (Bool -> Any
Any (Bool -> Any) -> (a1 -> Bool) -> a1 -> Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Variable -> a1 -> Bool
forall a. Symbolic a => Bool -> Variable -> a -> Bool
naked Bool
pos Variable
v) a
f)

guardsAxiom :: (Type -> Bool) -> (Type -> Function) -> Function -> NameM Form
guardsAxiom :: (Type -> Bool) -> (Type -> Function) -> Function -> NameM Form
guardsAxiom Type -> Bool
mono Type -> Function
ps f :: Function
f@(Name
_ ::: FunType [Type]
args Type
res)
  | Type -> Bool
mono Type
res = Form -> NameM Form
forall (m :: * -> *) a. Monad m => a -> m a
return Form
true
  | Bool
otherwise = do
    [Term]
vs <- [Type] -> (Type -> NameM Term) -> NameM [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Type]
args ((Type -> NameM Term) -> NameM [Term])
-> (Type -> NameM Term) -> NameM [Term]
forall a b. (a -> b) -> a -> b
$ \Type
ty ->
      (Variable -> Term) -> NameM Variable -> NameM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Variable -> Term
Var (Tag -> Type -> NameM Variable
forall a b. Named a => a -> b -> NameM (Name ::: b)
newSymbol Tag
"X" Type
ty)
    Form -> NameM Form
forall (m :: * -> *) a. Monad m => a -> m a
return (Signed Atomic -> Form
Literal (Atomic -> Signed Atomic
forall a. a -> Signed a
Pos (Term -> Atomic
Tru (Type -> Function
ps Type
res Function -> [Term] -> Term
:@: [Function
f Function -> [Term] -> Term
:@: [Term]
vs]))))

guardsTypeAxiom :: (Type -> Bool) -> (Type -> Function) -> Type -> NameM Form
guardsTypeAxiom :: (Type -> Bool) -> (Type -> Function) -> Type -> NameM Form
guardsTypeAxiom Type -> Bool
mono Type -> Function
ps Type
ty
  | Type -> Bool
mono Type
ty = Form -> NameM Form
forall (m :: * -> *) a. Monad m => a -> m a
return Form
true
  | Bool
otherwise = do
    Term
v <- (Variable -> Term) -> NameM Variable -> NameM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Variable -> Term
Var (Tag -> Type -> NameM Variable
forall a b. Named a => a -> b -> NameM (Name ::: b)
newSymbol Tag
"X" Type
ty)
    Form -> NameM Form
forall (m :: * -> *) a. Monad m => a -> m a
return (Bind Form -> Form
Exists (Form -> Bind Form
forall a. Symbolic a => a -> Bind a
bind (Signed Atomic -> Form
Literal (Atomic -> Signed Atomic
forall a. a -> Signed a
Pos (Term -> Atomic
Tru (Type -> Function
ps Type
ty Function -> [Term] -> Term
:@: [Term
v]))))))