summaryrefslogtreecommitdiff
path: root/source/Megalodon.hs
diff options
context:
space:
mode:
Diffstat (limited to 'source/Megalodon.hs')
-rw-r--r--source/Megalodon.hs98
1 files changed, 48 insertions, 50 deletions
diff --git a/source/Megalodon.hs b/source/Megalodon.hs
index 8f63915..df192c0 100644
--- a/source/Megalodon.hs
+++ b/source/Megalodon.hs
@@ -2,21 +2,19 @@ module Megalodon where
import Base hiding (null)
import Syntax.Internal
-import Syntax.Lexicon
import Checking (makeReplacementIff)
import Report.Location
import Bound.Scope
import Bound.Var
-import Data.Map.Strict qualified as Map
import Data.List.NonEmpty qualified as NonEmpty
import TextBuilder
import Data.List qualified as List
import Data.Text qualified as Text
-encodeBlocks :: Lexicon -> [Block] -> Text
-encodeBlocks lexi blocks = TextBuilder.toText (preamble <> buildBlocks lexi blocks)
+encodeBlocks :: [Block] -> Text
+encodeBlocks blocks = TextBuilder.toText (preamble <> buildBlocks blocks)
closure :: [ExprOf VarSymbol] -> ExprOf VarSymbol -> Formula
closure asms stmt = contraction (forallClosure mempty (makeConjunction asms `Implies` stmt))
@@ -25,44 +23,44 @@ unAsm :: Asm -> Formula
unAsm (Asm phi) = phi
unAsm (AsmStruct x sp) = TermSymbol Nowhere (SymbolPredicate (PredicateNounStruct sp)) [TermVar x]
-buildBlocks :: Lexicon -> [Block] -> TextBuilder
-buildBlocks lexi = \case
+buildBlocks :: [Block] -> TextBuilder
+buildBlocks = \case
BlockAxiom _pos lbl (Axiom asms stmt) : blocks ->
let phi = closure (unAsm <$> asms) stmt
- in text "Fact " <> buildMarker lbl <> text " : " <> buildFormula lexi phi <> text ".\nAdmitted.\n" <> buildBlocks lexi blocks
+ in text "Fact " <> buildMarker lbl <> text " : " <> buildFormula phi <> text ".\nAdmitted.\n" <> buildBlocks blocks
BlockLemma _pos lbl (Lemma asms stmt) : BlockProof _ _ _ : blocks ->
let phi = closure (unAsm <$> asms) stmt
- in text "Theorem " <> buildMarker lbl <> text " : " <> buildFormula lexi phi <> text ".\nAdmitted.\n" <> buildBlocks lexi blocks
+ in text "Theorem " <> buildMarker lbl <> text " : " <> buildFormula phi <> text ".\nAdmitted.\n" <> buildBlocks blocks
BlockLemma _pos lbl (Lemma asms stmt) : blocks ->
let phi = closure (unAsm <$> asms) stmt
- in text "Theorem " <> buildMarker lbl <> text " : " <> buildFormula lexi phi <> text ".\nAdmitted.\n" <> buildBlocks lexi blocks
+ in text "Theorem " <> buildMarker lbl <> text " : " <> buildFormula phi <> text ".\nAdmitted.\n" <> buildBlocks blocks
BlockDefn _pos _lbl defn : blocks->
- buildDefn lexi defn <> buildBlocks lexi blocks
+ buildDefn defn <> buildBlocks blocks
BlockAbbr _pos _lbl abbr : blocks->
- buildAbbr lexi abbr <> buildBlocks lexi blocks
+ buildAbbr abbr <> buildBlocks blocks
[] ->
mempty
block : _ ->
_TODO ("builBlocks" <> show block)
-buildDefn :: Lexicon -> Defn -> TextBuilder
-buildDefn lexi = \case
+buildDefn :: Defn -> TextBuilder
+buildDefn = \case
DefnPredicate [] predi xs phi ->
- "Definition " <> buildSymbol lexi (SymbolPredicate predi) <> " := " <>
- "fun " <> buildVarSymbols xs <> ": set => " <> buildFormula lexi phi <> ".\n"
+ "Definition " <> buildSymbol (SymbolPredicate predi) <> " := " <>
+ "fun " <> buildVarSymbols xs <> ": set => " <> buildFormula phi <> ".\n"
DefnFun [] f xs phi ->
- "Definition " <> buildSymbol lexi (SymbolFun f) <> " := " <>
- buildSetFunIfNonEmpty (buildVarSymbols xs) (buildFormula lexi phi) <> ".\n"
+ "Definition " <> buildSymbol (SymbolFun f) <> " := " <>
+ buildSetFunIfNonEmpty (buildVarSymbols xs) (buildFormula phi) <> ".\n"
DefnOp f xs phi ->
- "Definition " <> buildSymbol lexi (SymbolMixfix f) <> " := " <>
- buildSetFunIfNonEmpty (buildVarSymbols xs) (buildFormula lexi phi) <> ".\n"
+ "Definition " <> buildSymbol (SymbolMixfix f) <> " := " <>
+ buildSetFunIfNonEmpty (buildVarSymbols xs) (buildFormula phi) <> ".\n"
_ ->
error "assumptions in definition, deprecated"
-buildAbbr :: Lexicon -> Abbreviation -> TextBuilder
-buildAbbr lexi (Abbreviation f body) =
- "Definition " <> buildSymbol lexi f <> " := " <>
- buildSetFunIfNonEmpty buildBindings' (buildFormula lexi ((instantiate (TermVar . FreshVar) (fmap absurd body)))) <> ".\n"
+buildAbbr :: Abbreviation -> TextBuilder
+buildAbbr (Abbreviation f body) =
+ "Definition " <> buildSymbol f <> " := " <>
+ buildSetFunIfNonEmpty buildBindings' (buildFormula ((instantiate (TermVar . FreshVar) (fmap absurd body)))) <> ".\n"
where
buildBindings' :: TextBuilder
buildBindings' = intercalate (char ' ') (buildVarSymbol . FreshVar <$> List.sort (List.nub (bindings body)))
@@ -70,62 +68,62 @@ buildAbbr lexi (Abbreviation f body) =
buildSetFunIfNonEmpty :: TextBuilder -> TextBuilder -> TextBuilder
buildSetFunIfNonEmpty xs b = if isEmpty xs then b else "fun " <> xs <> " : set => " <> b
-buildFormula :: Lexicon -> Formula -> TextBuilder
-buildFormula lexi = \case
+buildFormula :: Formula -> TextBuilder
+buildFormula = \case
TermVar x -> buildVarSymbol x
-- We handle eq in a special manner to avoid having to specify the type of the equality.
TermSymbol _pos f [x,y] | isEqSymbol f ->
- char '(' <> buildFormula lexi x <> text " = " <> buildFormula lexi y <> char ')'
+ char '(' <> buildFormula x <> text " = " <> buildFormula y <> char ')'
TermSymbol _pos f [x,y] | isDiseqSymbol f ->
- char '(' <> buildFormula lexi x <> text " <> " <> buildFormula lexi y <> char ')'
+ char '(' <> buildFormula x <> text " <> " <> buildFormula y <> char ')'
TermSymbol _pos f es ->
- let es' = buildSymbol lexi f : (buildFormula lexi <$> es)
+ let es' = buildSymbol f : (buildFormula <$> es)
in char '(' <> intercalate (char ' ') es' <> char ')'
Apply e es ->
- let es' = NonEmpty.cons (buildFormula lexi e) (buildFormula lexi <$> es)
+ let es' = NonEmpty.cons (buildFormula e) (buildFormula <$> es)
in char '(' <> intercalate (char ' ') es' <> char ')'
- Not _pos e -> text "~(" <> buildFormula lexi e <> char ')'
+ Not _pos e -> text "~(" <> buildFormula e <> char ')'
Connected conn e1 e2 ->
- char '(' <> buildConn conn (buildFormula lexi e1) (buildFormula lexi e2) <> char ')'
+ char '(' <> buildConn conn (buildFormula e1) (buildFormula e2) <> char ')'
Quantified quant body ->
- char '(' <> buildQuant quant <> char ' ' <> buildBindings body <> text ",(" <> buildFormula lexi (instantiate TermVar body) <> text "))"
+ char '(' <> buildQuant quant <> char ' ' <> buildBindings body <> text ",(" <> buildFormula (instantiate TermVar body) <> text "))"
TermSep x bound phi ->
- char '{' <> buildVarSymbol x <> " :e (" <> buildFormula lexi bound <> text ")|" <> buildFormula lexi (instantiate1 (TermVar x) phi) <> char '}'
+ char '{' <> buildVarSymbol x <> " :e (" <> buildFormula bound <> text ")|" <> buildFormula (instantiate1 (TermVar x) phi) <> char '}'
ReplacePred y x xB body ->
let x' = buildVarSymbol x
y' = buildVarSymbol y
fromReplacementVar = \case
ReplacementDomVar -> TermVar x
ReplacementRangeVar -> TermVar y
- body' = buildFormula lexi (instantiate fromReplacementVar body)
- in "let MkReplFun := fun " <> x' <> " : set => (Eps_i (fun " <> y' <> "=>" <> body' <> ")) in {MkReplFun " <> x' <> "|" <> x' <> " :e (" <> buildFormula lexi xB <> ")}"
+ body' = buildFormula (instantiate fromReplacementVar body)
+ in "let MkReplFun := fun " <> x' <> " : set => (Eps_i (fun " <> y' <> "=>" <> body' <> ")) in {MkReplFun " <> x' <> "|" <> x' <> " :e (" <> buildFormula xB <> ")}"
ReplaceFun ((x, xB) :| []) lhs cond ->
let x' = buildVarSymbol x
- xB' = "(" <> buildFormula lexi xB <> ")" -- parens probably not needed
- lhs' = "(fun " <> x' <> " => " <> buildFormula lexi (instantiate TermVar lhs) <> ")"
- cond' = "(fun " <> x' <> " => " <> buildFormula lexi (instantiate TermVar cond) <> ")"
+ xB' = "(" <> buildFormula xB <> ")" -- parens probably not needed
+ lhs' = "(fun " <> x' <> " => " <> buildFormula (instantiate TermVar lhs) <> ")"
+ cond' = "(fun " <> x' <> " => " <> buildFormula (instantiate TermVar cond) <> ")"
-- Using "ReplSep : set->(set->prop)->(set->set)->set"
in "ReplSep " <> xB' <> cond' <> lhs'
ReplaceFun ((x, xB) :| (y, yB) : []) lhs cond ->
let x' = buildVarSymbol x
- xB' = "(" <> buildFormula lexi xB <> ")"
+ xB' = "(" <> buildFormula xB <> ")"
y' = buildVarSymbol y
- yB' = "(fun dummyVar => " <> buildFormula lexi yB <> ")"
- lhs' = "(fun " <> x' <> " " <> y' <> " => " <> buildFormula lexi (instantiate TermVar lhs) <> ")"
- cond' = "(fun " <> x' <> " " <> y' <> " => " <> buildFormula lexi (instantiate TermVar cond) <> ")"
+ yB' = "(fun dummyVar => " <> buildFormula yB <> ")"
+ lhs' = "(fun " <> x' <> " " <> y' <> " => " <> buildFormula (instantiate TermVar lhs) <> ")"
+ cond' = "(fun " <> x' <> " " <> y' <> " => " <> buildFormula (instantiate TermVar cond) <> ")"
-- Using "ReplSep2 : set -> (set -> set) -> (set -> set -> prop) -> (set -> set -> set) -> set"
in "ReplSep2 " <> xB' <> yB' <> cond' <> lhs'
ReplaceFun bounds lhs cond ->
-- Silly placeholder translation for now
let iff = makeReplacementIff (TermVar (F "frs")) bounds lhs cond
- in "Eps_i (fun frs : set => " <> buildFormula lexi iff <> ")"
+ in "Eps_i (fun frs : set => " <> buildFormula iff <> ")"
Lambda _ -> text "TODO_buildFormula_Lambda"
PropositionalConstant IsTop -> "True"
PropositionalConstant IsBottom -> "False"
TermSymbolStruct f me ->
let f' = buildMarker (Marker (unStructSymbol f))
e = me ?? error "unannotated struct op"
- in char '(' <> f' <> buildFormula lexi e <> char ')'
+ in char '(' <> f' <> buildFormula e <> char ')'
buildMarker :: Marker -> TextBuilder
buildMarker (Marker m)= text m
@@ -138,10 +136,10 @@ buildQuant = \case
buildBindings :: Scope VarSymbol ExprOf a -> TextBuilder
buildBindings body = intercalate (char ' ') (buildVarSymbol <$> List.nub (bindings body))
-buildBounds :: Lexicon -> NonEmpty (VarSymbol, ExprOf VarSymbol) -> TextBuilder
-buildBounds l (bound :| bounds) = foldr (\b bs -> buildBound b <> "/\\ " <> bs) (buildBound bound) bounds
+buildBounds :: NonEmpty (VarSymbol, ExprOf VarSymbol) -> TextBuilder
+buildBounds (bound :| bounds) = foldr (\b bs -> buildBound b <> "/\\ " <> bs) (buildBound bound) bounds
where
- buildBound (y, yB) = buildVarSymbol y <> " :e (" <> buildFormula l yB <> ")"
+ buildBound (y, yB) = buildVarSymbol y <> " :e (" <> buildFormula yB <> ")"
buildConn :: Connective -> (TextBuilder -> TextBuilder -> TextBuilder)
buildConn conn = \p q -> case conn of
@@ -160,9 +158,9 @@ buildVarSymbol = \case
buildVarSymbols :: (Functor t, Foldable t) => t VarSymbol -> TextBuilder
buildVarSymbols xs = intercalate (char ' ') (fmap buildVarSymbol xs)
-buildSymbol :: Lexicon -> Symbol -> TextBuilder
-buildSymbol _ (SymbolInteger i) = decimal i
-buildSymbol lexi symb = fromRightMarker case symb of
+buildSymbol :: Symbol -> TextBuilder
+buildSymbol (SymbolInteger i) = decimal i
+buildSymbol symb = fromRightMarker case symb of
SymbolMixfix f ->
Right (mixfixMarker f)
SymbolFun f -> Right (lexicalItemSgPlMarker f)
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-07 15:51:51 +0000