diff options
Diffstat (limited to 'source/Encoding.hs')
| -rw-r--r-- | source/Encoding.hs | 159 |
1 files changed, 159 insertions, 0 deletions
diff --git a/source/Encoding.hs b/source/Encoding.hs new file mode 100644 index 0000000..e3a65f2 --- /dev/null +++ b/source/Encoding.hs @@ -0,0 +1,159 @@ +module Encoding where + + +import Base +import Syntax.Internal +import Syntax.Lexicon +import Tptp.UnsortedFirstOrder qualified as Tptp + +import Data.Text qualified as Text +import Bound +import Bound.Scope + + +encodeTask :: Lexicon -> Task -> Tptp.Task +encodeTask l (Task _isByContradiction hypos m conjecture) = Tptp.Task (conjecture' : hypos') + where + conjecture' = encodeConjecture l m conjecture + hypos' = encodeHypos l hypos + + +encodeConjecture :: Lexicon -> Marker -> Formula -> Tptp.AnnotatedFormula +encodeConjecture l (Marker str) f = Tptp.AnnotatedFormula (Tptp.NameAtomicWord (Tptp.AtomicWord str)) Tptp.Conjecture (encodeExpr l f) + +-- NOTE: E's SInE will only filter out axioms and leave hypotheses fixed. +encodeHypos :: Lexicon -> [(Marker, Formula)] -> [Tptp.AnnotatedFormula] +encodeHypos l phis = [makeHypo m (encodeExpr l phi) | (m, phi) <- phis] + where + makeHypo :: Marker -> Tptp.Expr -> Tptp.AnnotatedFormula + makeHypo (Marker str) f' = Tptp.AnnotatedFormula (Tptp.NameAtomicWord (Tptp.AtomicWord str)) Tptp.Axiom f' + +encodeWithRole :: Tptp.Role -> Lexicon -> [(Marker, Formula)] -> [Tptp.AnnotatedFormula] +encodeWithRole role l phis = [makeHypo m (encodeExpr l phi) | (m, phi) <- phis] + where + makeHypo :: Marker -> Tptp.Expr -> Tptp.AnnotatedFormula + makeHypo (Marker str) f' = Tptp.AnnotatedFormula (Tptp.NameAtomicWord (Tptp.AtomicWord str)) role f' + + +encodeExpr :: Lexicon -> Expr -> Tptp.Expr +encodeExpr l = go . (fmap encodeFreeVar) + where + go :: ExprOf Tptp.Expr -> Tptp.Expr + go = \case + e1 `Equals` e2 -> + Tptp.Eq (go e1) (go e2) + e1 `NotEquals` e2 -> + Tptp.NotEq (go e1) (go e2) + Atomic p es -> + let p' = encodePredicate l p + es' = go <$> toList es + in Tptp.Apply p' es' + PropositionalConstant IsBottom -> + Tptp.Bottom + PropositionalConstant IsTop -> + Tptp.Top + Not f -> + Tptp.Not (go f) + Connected Conjunction f1 f2 -> + Tptp.Conn Tptp.And (go f1) (go f2) + Connected Disjunction f1 f2 -> + Tptp.Conn Tptp.Or (go f1) (go f2) + Connected Implication f1 f2 -> + Tptp.Conn Tptp.Imply (go f1) (go f2) + Connected Equivalence f1 f2 -> + Tptp.Conn Tptp.Iff (go f1) (go f2) + Connected NegatedDisjunction f1 f2 -> + Tptp.Not (Tptp.Conn Tptp.Or (go f1) (go f2)) + Connected ExclusiveOr f1 f2 -> + Tptp.Not (Tptp.Conn Tptp.Iff (go f1) (go f2)) + Quantified quant scope -> + let phi = instantiate instantiator scope + xs = [encodeBoundVar x | x <- nubOrd (bindings scope)] + phi' = go phi + quant' = encodeQuant quant + in case xs of + [] -> phi' + y:ys -> Tptp.Quantified quant' (y:|ys) phi' + TermVar v -> + v + Apply e es -> case e of + TermVar (Tptp.Const x) -> Tptp.Apply x (go <$> toList es) + _ -> error ("encodeExpr: complex term as head of applicaition: " <> show e) + TermSymbol symb es -> + Tptp.Apply (encodeSymbol l symb) (go <$> es) + e@ReplaceFun{} -> + error ("Precondition failed in encodeTerm, cannot encode terms with comprehensions directly: " <> show e) + e@ReplacePred{} -> + error ("Precondition failed in encodeTerm, cannot encode terms with comprehensions directly: " <> show e) + e@TermSep{} -> + error ("Precondition failed in encodeTerm, cannot encode terms with comprehensions directly: " <> show e) + e@Iota{} -> + error ("Precondition failed in encodeTerm, cannot encode terms with descriptors directly: " <> show e) + TermSymbolStruct symb e -> case e of + Just e' -> + Tptp.Apply (Tptp.AtomicWord ("s__" <> (unStructSymbol symb))) [go e'] + Nothing -> + error ("encodeExpr.go (precondition failed): unannotated struct symbol" <> show symb) + _ -> error "encodeExpr.go: missing case" + + +instantiator :: VarSymbol -> ExprOf Tptp.Expr +instantiator bv = TermVar (Tptp.Var (encodeBoundVar bv)) + + + +encodeQuant :: Quantifier -> Tptp.Quantifier +encodeQuant Universally = Tptp.Forall +encodeQuant Existentially = Tptp.Exists + + + + +encodeSymbol :: Lexicon -> Symbol -> Tptp.AtomicWord +encodeSymbol l symb = atomicWordFromRightMarker case symb of + SymbolMixfix op -> + lookupOp op (lexiconMixfix l) + SymbolFun fun -> + lookupLexicalItem fun (lexiconFuns l) + SymbolInteger n -> + Right (Marker (Text.pack (show n))) + SymbolPredicate _ -> + error "IMPOSSIBLE: predicates should already be translated" + + +encodePredicate :: Lexicon -> Predicate -> Tptp.AtomicWord +encodePredicate l p = atomicWordFromRightMarker case p of + PredicateAdj adj -> + lookupLexicalItem adj (lexiconAdjs l) + PredicateVerb verb -> + lookupLexicalItem verb (lexiconVerbs l) + PredicateNoun noun -> + lookupLexicalItem noun (lexiconNouns l) + PredicateRelation rel -> + lookupLexicalItem rel (lexiconRelationSymbols l) + PredicateNounStruct noun -> + lookupLexicalItem noun (lexiconStructNouns l) + PredicateSymbol symb -> + Right (Marker symb) + + +atomicWordFromRightMarker :: Either String Marker -> Tptp.AtomicWord +atomicWordFromRightMarker = \case + Right (Marker m) -> Tptp.AtomicWord m + Left a -> error ("symbol not in lexicon" <> a) + +encodeFreeVar :: VarSymbol -> Tptp.Expr +encodeFreeVar fv = Tptp.Const fv' + where + fv' = Tptp.AtomicWord case fv of + NamedVar x -> Text.cons 'f' x + FreshVar n -> Text.cons 'y' (Text.pack (show n)) + + +-- | Tptp variables must be "upper words", starting with an uppercase letter +-- and continuing with alphanumeric characters. We prefix all variables +-- with "X" to make them easy to decode. +encodeBoundVar :: VarSymbol -> Tptp.Variable +encodeBoundVar bv = Tptp.Variable $ Text.cons 'X' case bv of + NamedVar x -> x + FreshVar n -> Text.pack (show n) |