{-# 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 String
t Kind
k InputSource
info Form
f) = String -> Kind -> InputSource -> Form -> Input Form
forall a. String -> Kind -> InputSource -> a -> Input a
Input String
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 (Name ::: Type)
vs Form
f))
          | Bool
pos = Scheme1 -> Bind Form -> Form
forAll Scheme1
scheme (Set (Name ::: Type) -> Form -> Bind Form
forall a. Set (Name ::: Type) -> a -> Bind a
Bind Set (Name ::: Type)
vs (Bool -> Form -> Form
aux Bool
pos Form
f))
          | Bool
otherwise = Form -> Form
notInwards (Scheme1 -> Bind Form -> Form
exists Scheme1
scheme (Set (Name ::: Type) -> Form -> Bind Form
forall a. Set (Name ::: Type) -> a -> Bind a
Bind Set (Name ::: Type)
vs (Form -> Form
Not (Bool -> Form -> Form
aux Bool
pos Form
f))))
        aux Bool
pos (Exists (Bind Set (Name ::: Type)
vs Form
f))
          | Bool
pos = Scheme1 -> Bind Form -> Form
exists Scheme1
scheme (Set (Name ::: Type) -> Form -> Bind Form
forall a. Set (Name ::: Type) -> a -> Bind a
Bind Set (Name ::: Type)
vs (Bool -> Form -> Form
aux Bool
pos Form
f))
          | Bool
otherwise = Form -> Form
notInwards (Scheme1 -> Bind Form -> Form
forAll Scheme1
scheme (Set (Name ::: Type) -> Form -> Bind Form
forall a. Set (Name ::: Type) -> a -> Bind a
Bind Set (Name ::: Type)
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 a b. (a -> b) -> [a] -> [b]
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 a b. (a -> b) -> [a] -> [b]
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
_) = String -> Form
forall a. HasCallStack => String -> a
error String
"ToFOF.guard: equiv should have been eliminated"
        aux Bool
_pos (Connective Connective
_ Form
_ Form
_) = String -> Form
forall a. HasCallStack => String -> a
error String
"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 a. [a] -> 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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 -> String -> Function
forall a. HasCallStack => String -> a
error String
"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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 a b. (a -> b -> b) -> b -> [a] -> b
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 a. a -> NameM a
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
$
    [ String -> Kind -> InputSource -> Form -> Input Form
forall a. String -> Kind -> InputSource -> a -> Input a
Input (String
"types" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i) (AxKind -> Kind
Ax AxKind
Axiom) (String -> String -> Problem Form -> InputSource
inference String
"type_axiom" String
"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 String
tag Kind
kind InputSource
_ Form
f) -> do
            let prepare :: Form -> NameM Form
prepare Form
f = ([Form] -> Form) -> NameM [Form] -> NameM Form
forall a b. (a -> b) -> NameM a -> NameM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Form -> Form -> Form) -> Form -> [Form] -> Form
forall a b. (a -> b -> b) -> b -> [a] -> b
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 (String -> M [Form] -> M [Form]
forall a. String -> M a -> M a
withName String
tag (Form -> M [Form]
removeEquiv (Form -> Form
simplify Form
f))))
            case Kind
kind of
              Ax{} ->
                (Form -> Input Form) -> NameM Form -> NameM (Input Form)
forall a b. (a -> b) -> NameM a -> NameM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String -> Kind -> InputSource -> Form -> Input Form
forall a. String -> Kind -> InputSource -> a -> Input a
Input String
tag Kind
kind (String -> String -> Problem Form -> InputSource
inference String
"type_encoding" String
"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 a b. (a -> b) -> NameM a -> NameM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String -> Kind -> InputSource -> Form -> Input Form
forall a. String -> Kind -> InputSource -> a -> Input a
Input String
tag Kind
kind (String -> String -> Problem Form -> InputSource
inference String
"type_encoding" String
"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 a b. (a -> b) -> NameM a -> NameM b
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 String
_) = Bool
True
      isNumber (Fixed (Rational Rational
_) Maybe String
_) = Bool
True
      isNumber (Fixed (Real Rational
_) Maybe String
_) = 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 <- String -> NameM Name
forall a. Named a => a -> NameM Name
newName String
""
    Problem Form -> NameM (Problem Form)
forall a. a -> NameM a
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 =
  String -> OptionParser Bool -> OptionParser Bool
forall a. String -> OptionParser a -> OptionParser a
inGroup String
"Options for encoding types" (OptionParser Bool -> OptionParser Bool)
-> OptionParser Bool -> OptionParser Bool
forall a b. (a -> b) -> a -> b
$
  String -> [String] -> Bool -> OptionParser Bool
bool String
"more-axioms"
    [String
"Add extra, redundant typing axioms for function arguments (on by default).",
     String
"Improves performance on provers which use equations as rewrite rules",
     String
"to simplify discovered facts. May harm performance on other provers.",
     String
"Only affects --encoding tags."]
    Bool
True

tags :: Bool -> Scheme
tags :: Bool -> Scheme
tags Bool
moreAxioms = Scheme
  { makeFunction :: Type -> NameM Function
makeFunction = \Type
ty ->
      Name -> [Type] -> Type -> NameM Function
forall a. Named a => a -> [Type] -> Type -> NameM Function
newFunction (String -> Name -> Name
withLabel String
"type_tag" (String -> Name
forall a. Named a => a -> Name
name (String
"to_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Named a => a -> String
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
  { forAll :: Bind Form -> Form
forAll = Bind Form -> Form
ForAll,
    exists :: Bind Form -> Form
exists = \(Bind Set (Name ::: Type)
vs Form
f) ->
       let bound :: Form
bound = (Form -> Form -> Form) -> Form -> [Form] -> Form
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Form -> Form -> Form
(/\) Form
true (((Name ::: Type) -> Form) -> [Name ::: Type] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map (Name ::: Type) -> Form
guard (Set (Name ::: Type) -> [Name ::: Type]
forall a. Set a -> [a]
Set.toList Set (Name ::: Type)
vs))
           guard :: (Name ::: Type) -> Form
guard Name ::: Type
v | Type -> Bool
mono ((Name ::: Type) -> Type
forall a. Typed a => a -> Type
typ Name ::: Type
v) = Form
true
                   | Bool
otherwise = Signed Atomic -> Form
Literal (Atomic -> Signed Atomic
forall a. a -> Signed a
Pos (Type -> Function
fs ((Name ::: Type) -> Type
forall a. Typed a => a -> Type
typ Name ::: Type
v) Function -> [Term] -> Term
:@: [(Name ::: Type) -> Term
Var Name ::: Type
v] Term -> Term -> Atomic
:=: (Name ::: Type) -> Term
Var Name ::: Type
v))
       in Bind Form -> Form
Exists (Set (Name ::: Type) -> Form -> Bind Form
forall a. Set (Name ::: Type) -> a -> Bind a
Bind Set (Name ::: Type)
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 ->
    ((Name ::: Type) -> Term) -> NameM (Name ::: Type) -> NameM Term
forall a b. (a -> b) -> NameM a -> NameM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name ::: Type) -> Term
Var (String -> Type -> NameM (Name ::: Type)
forall a b. Named a => a -> b -> NameM (Name ::: b)
newSymbol String
"X" Type
ty)
  let t :: Term
t = Function
f Function -> [Term] -> Term
:@: [Term]
vs
      at :: Int -> (t -> t) -> [t] -> [t]
at Int
n t -> t
f [t]
xs = Int -> [t] -> [t]
forall a. Int -> [a] -> [a]
take Int
n [t]
xs [t] -> [t] -> [t]
forall a. [a] -> [a] -> [a]
++ [t -> t
f ([t]
xs [t] -> Int -> t
forall a. HasCallStack => [a] -> Int -> a
!! Int
n)] [t] -> [t] -> [t]
forall a. [a] -> [a] -> [a]
++ Int -> [t] -> [t]
forall a. Int -> [a] -> [a]
drop (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) [t]
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. HasCallStack => [a] -> Int -> a
!! Int
n), Function
f Function -> [Term] -> Term
:@: Int -> (Term -> Term) -> [Term] -> [Term]
forall {t}. Int -> (t -> t) -> [t] -> [t]
at Int
n Term -> Term
tag [Term]
vs)
           | Bool
moreAxioms,
             Int
n <- [Int
0..[Term] -> Int
forall a. [a] -> 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 a. a -> NameM a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Form -> Form -> Form) -> Form -> [Form] -> Form
forall a b. (a -> b -> b) -> b -> [a] -> b
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 a. a -> NameM a
forall (m :: * -> *) a. Monad m => a -> m a
return Form
true
  | Bool
otherwise = do
      Term
v <- ((Name ::: Type) -> Term) -> NameM (Name ::: Type) -> NameM Term
forall a b. (a -> b) -> NameM a -> NameM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name ::: Type) -> Term
Var (String -> Type -> NameM (Name ::: Type)
forall a b. Named a => a -> b -> NameM (Name ::: b)
newSymbol String
"X" Type
ty)
      Form -> NameM Form
forall a. a -> NameM a
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
  { makeFunction :: Type -> NameM Function
makeFunction = \Type
ty ->
      Name -> [Type] -> Type -> NameM Function
forall a. Named a => a -> [Type] -> Type -> NameM Function
newFunction (String -> Name -> Name
withLabel String
"type_pred" (String -> Name
forall a. Named a => a -> Name
name (String
"is_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Named a => a -> String
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
  { forAll :: Bind Form -> Form
forAll = \(Bind Set (Name ::: Type)
vs Form
f) ->
       let bound :: Form
bound = (Form -> Form -> Form) -> Form -> [Form] -> Form
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Form -> Form -> Form
(/\) Form
true (((Name ::: Type) -> Form) -> [Name ::: Type] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map (Name ::: Type) -> Form
guard (Set (Name ::: Type) -> [Name ::: Type]
forall a. Set a -> [a]
Set.toList Set (Name ::: Type)
vs))
           guard :: (Name ::: Type) -> Form
guard Name ::: Type
v | Type -> Bool
mono ((Name ::: Type) -> Type
forall a. Typed a => a -> Type
typ Name ::: Type
v) = Form
true
                   | Bool -> Bool
not (Bool -> (Name ::: Type) -> Form -> Bool
forall a. Symbolic a => Bool -> (Name ::: Type) -> a -> Bool
naked Bool
True Name ::: Type
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 ((Name ::: Type) -> Type
forall a. Typed a => a -> Type
typ Name ::: Type
v) Function -> [Term] -> Term
:@: [(Name ::: Type) -> Term
Var Name ::: Type
v])))
       in Bind Form -> Form
ForAll (Set (Name ::: Type) -> Form -> Bind Form
forall a. Set (Name ::: Type) -> a -> Bind a
Bind Set (Name ::: Type)
vs (Form -> Form
simplify (Form -> Form
Not Form
bound) Form -> Form -> Form
\/ Form
f)),
    exists :: Bind Form -> Form
exists = \(Bind Set (Name ::: Type)
vs Form
f) ->
       let bound :: Form
bound = (Form -> Form -> Form) -> Form -> [Form] -> Form
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Form -> Form -> Form
(/\) Form
true (((Name ::: Type) -> Form) -> [Name ::: Type] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map (Name ::: Type) -> Form
guard (Set (Name ::: Type) -> [Name ::: Type]
forall a. Set a -> [a]
Set.toList Set (Name ::: Type)
vs))
           guard :: (Name ::: Type) -> Form
guard Name ::: Type
v | Type -> Bool
mono ((Name ::: Type) -> Type
forall a. Typed a => a -> Type
typ Name ::: Type
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 ((Name ::: Type) -> Type
forall a. Typed a => a -> Type
typ Name ::: Type
v) Function -> [Term] -> Term
:@: [(Name ::: Type) -> Term
Var Name ::: Type
v])))
       in Bind Form -> Form
Exists (Set (Name ::: Type) -> Form -> Bind Form
forall a. Set (Name ::: Type) -> a -> Bind a
Bind Set (Name ::: Type)
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 :: forall a. Symbolic a => Bool -> (Name ::: Type) -> a -> Bool
naked Bool
pos Name ::: Type
v a
f
  | TypeOf a
Form <- a -> TypeOf a
forall a. Symbolic a => a -> TypeOf a
typeOf a
f,
    Not Form
f' <- a
f = Bool -> (Name ::: Type) -> Form -> Bool
forall a. Symbolic a => Bool -> (Name ::: Type) -> a -> Bool
naked (Bool -> Bool
not Bool
pos) Name ::: Type
v Form
f'
  | TypeOf a
Signed <- a -> TypeOf a
forall a. Symbolic a => a -> TypeOf a
typeOf a
f,
    Pos a1
f' <- a
f = Bool -> (Name ::: Type) -> a1 -> Bool
forall a. Symbolic a => Bool -> (Name ::: Type) -> a -> Bool
naked Bool
pos Name ::: Type
v a1
f'
  | TypeOf a
Signed <- a -> TypeOf a
forall a. Symbolic a => a -> TypeOf a
typeOf a
f,
    Neg a1
f' <- a
f = Bool -> (Name ::: Type) -> a1 -> Bool
forall a. Symbolic a => Bool -> (Name ::: Type) -> a -> Bool
naked (Bool -> Bool
not Bool
pos) Name ::: Type
v a1
f'
  | TypeOf a
Atomic <- a -> TypeOf a
forall a. Symbolic a => a -> TypeOf a
typeOf a
f,
    Term
t :=: Term
u <- a
f,
    Bool
pos = Term
t Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== (Name ::: Type) -> Term
Var Name ::: Type
v Bool -> Bool -> Bool
|| Term
u Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== (Name ::: Type) -> Term
Var Name ::: Type
v
  | TypeOf a
Bind_ <- a -> TypeOf a
forall a. Symbolic a => a -> TypeOf a
typeOf a
f,
    Bind Set (Name ::: Type)
vs a1
f' <- a
f = Bool -> Bool
not ((Name ::: Type) -> Set (Name ::: Type) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Name ::: Type
v Set (Name ::: Type)
vs) Bool -> Bool -> Bool
&& Bool -> (Name ::: Type) -> a1 -> Bool
forall a. Symbolic a => Bool -> (Name ::: Type) -> a -> Bool
naked Bool
pos Name ::: Type
v a1
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 -> (Name ::: Type) -> a1 -> Bool
forall a. Symbolic a => Bool -> (Name ::: Type) -> a -> Bool
naked Bool
pos Name ::: Type
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 a. a -> NameM a
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 ->
      ((Name ::: Type) -> Term) -> NameM (Name ::: Type) -> NameM Term
forall a b. (a -> b) -> NameM a -> NameM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name ::: Type) -> Term
Var (String -> Type -> NameM (Name ::: Type)
forall a b. Named a => a -> b -> NameM (Name ::: b)
newSymbol String
"X" Type
ty)
    Form -> NameM Form
forall a. a -> NameM a
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 a. a -> NameM a
forall (m :: * -> *) a. Monad m => a -> m a
return Form
true
  | Bool
otherwise = do
    Term
v <- ((Name ::: Type) -> Term) -> NameM (Name ::: Type) -> NameM Term
forall a b. (a -> b) -> NameM a -> NameM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name ::: Type) -> Term
Var (String -> Type -> NameM (Name ::: Type)
forall a b. Named a => a -> b -> NameM (Name ::: b)
newSymbol String
"X" Type
ty)
    Form -> NameM Form
forall a. a -> NameM a
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]))))))