diff options
Diffstat (limited to 'source')
| -rw-r--r-- | source/Api.hs | 1 | ||||
| -rw-r--r-- | source/Checking.hs | 22 | ||||
| -rw-r--r-- | source/CommandLine.hs | 5 | ||||
| -rw-r--r-- | source/Meaning.hs | 14 | ||||
| -rw-r--r-- | source/Syntax/Abstract.hs | 6 | ||||
| -rw-r--r-- | source/Syntax/Concrete.hs | 29 | ||||
| -rw-r--r-- | source/Syntax/Internal.hs | 43 | ||||
| -rw-r--r-- | source/Syntax/Token.hs | 13 |
8 files changed, 82 insertions, 51 deletions
diff --git a/source/Api.hs b/source/Api.hs index 1bdf615..866115d 100644 --- a/source/Api.hs +++ b/source/Api.hs @@ -67,7 +67,6 @@ import Text.Megaparsec hiding (parse, Token) import UnliftIO import UnliftIO.Directory import UnliftIO.Environment -import Syntax.Abstract (Formula) -- | Follow all @\\import@ statements recursively and build a theory graph from them. -- The @\\import@ statements should be on their own separate line and precede all diff --git a/source/Checking.hs b/source/Checking.hs index 8bc38a4..a33edc2 100644 --- a/source/Checking.hs +++ b/source/Checking.hs @@ -539,17 +539,17 @@ checkProof = \case , Asm (relationNoun (TermVar funVar)) ] checkProof continue - Calc calc continue -> do - checkCalc calc - assume [Asm (calcResult calc)] + Calc quant calc continue -> do + checkCalc quant calc + assume [Asm (calcResult quant calc)] checkProof continue DefineFunctionLocal funVar argVar domVar ranExpr definitions continue -> do - -- We have f: X \to Y and x \mapsto ... + -- We have f: X \to Y and x \mapsto ... -- definition is a nonempty list of (expresssion e, formula phi) -- such that f(x) = e if phi(x) -- since we do a case deduction in the definition there has to be a check that, -- our domains in the case are a disjunct union of dom(f) - assume + assume [Asm (TermOp DomSymbol [TermVar funVar] `Equals` TermVar domVar) ,Asm (rightUniqueAdj (TermVar funVar)) ,Asm (relationNoun (TermVar funVar))] @@ -578,7 +578,7 @@ localFunctionGoal xs = makeXor $ map snd $ NonEmpty.toList xs -- -- For x \mapsto expr(x,ys,cs) , if formula(x,ys) ; here cs are just global constants -- -> \forall x,ys: ( formula(x,ys) => expr(x,ys,cs)) - + functionSubdomianExpression :: VarSymbol -> VarSymbol -> VarSymbol -> Set VarSymbol -> [(Term, Formula)] -> [Asm] functionSubdomianExpression f a d s (x:xs) = singleFunctionSubdomianExpression f a d s x : functionSubdomianExpression f a d s xs @@ -588,15 +588,15 @@ singleFunctionSubdomianExpression :: VarSymbol -> VarSymbol -> VarSymbol -> Set singleFunctionSubdomianExpression funVar argVar domVar fixedV (expr, frm) = let -- boundVar = Set.toList (freeVars expr) in -- let def = makeForall (argVar:boundVar) (((TermVar argVar `IsElementOf` TermVar domVar) `And` frm) `Implies` TermOp ApplySymbol [TermVar funVar, TermVar argVar] `Equals` expr) - boundVar = fixedV in + boundVar = fixedV in let def = forallClosure boundVar (((TermVar argVar `IsElementOf` TermVar domVar) `And` frm) `Implies` (TermOp ApplySymbol [TermVar funVar, TermVar argVar] `Equals` expr)) in Asm def - -checkCalc :: Calc -> Checking -checkCalc calc = locally do - let tasks = calculation calc + +checkCalc :: CalcQuantifier -> Calc -> Checking +checkCalc quant calc = locally do + let tasks = calculation quant calc forM_ tasks tell where tell = \case diff --git a/source/CommandLine.hs b/source/CommandLine.hs index b8c170e..3502b9a 100644 --- a/source/CommandLine.hs +++ b/source/CommandLine.hs @@ -18,7 +18,6 @@ import UnliftIO import UnliftIO.Directory import UnliftIO.Environment (lookupEnv) import System.FilePath.Posix -import qualified Tptp.UnsortedFirstOrder as Syntax.Internal runCommandLine :: IO () runCommandLine = do @@ -94,7 +93,7 @@ run = do Text.putStrLn task Text.putStrLn err Text.putStrLn tptp - + WithFailList -> liftIO case result of VerificationSuccess -> putStrLn "\ESC[32mVerification successful.\ESC[0m" VerificationFailure [] -> error "Empty verification fail" @@ -187,4 +186,4 @@ withMegalodonParser = flag' WithMegalodon (long "megalodon" <> help "Export to M withFailListParser :: Parser WithFailList withFailListParser = flag' WithFailList (long "list_fails" <> help "Will list all unproven task with possible reason of failure.") - <|> pure WithoutFailList -- Default to using the cache.
\ No newline at end of file + <|> pure WithoutFailList -- Default to using the cache. diff --git a/source/Meaning.hs b/source/Meaning.hs index 9b4bc45..3822221 100644 --- a/source/Meaning.hs +++ b/source/Meaning.hs @@ -605,14 +605,22 @@ glossProof = \case if domVar == argVar then Sem.DefineFunction funVar argVar <$> glossExpr valueExpr <*> glossExpr domExpr <*> glossProof proof else error "mismatched variables in function definition." - + Raw.DefineFunctionLocal funVar domVar ranExpr funVar2 argVar definitions proof -> do if funVar == funVar2 then Sem.DefineFunctionLocal funVar argVar domVar <$> glossExpr ranExpr <*> (glossLocalFunctionExprDef `each` definitions) <*> glossProof proof else error "missmatched function names" - Raw.Calc calc proof -> - Sem.Calc <$> glossCalc calc <*> glossProof proof + Raw.Calc calcQuant calc proof -> + Sem.Calc <$> glossCalcQuantifier calcQuant <*> glossCalc calc <*> glossProof proof +glossCalcQuantifier :: Maybe Raw.CalcQuantifier -> Gloss Sem.CalcQuantifier +glossCalcQuantifier Nothing = pure Sem.CalcUnquantified +glossCalcQuantifier (Just (Raw.CalcQuantifier xs bound maySuchThat)) = do + bound' <- glossBound bound + maySuchThat' <- glossStmt `each` maySuchThat + let maySuchThat'' = case (bound', maySuchThat') of + _ -> Nothing + pure (Sem.CalcForall xs maySuchThat'') glossLocalFunctionExprDef :: (Raw.Expr, Raw.Formula) -> Gloss (Sem.Term, Sem.Formula) glossLocalFunctionExprDef (definingExpression, localDomain) = do diff --git a/source/Syntax/Abstract.hs b/source/Syntax/Abstract.hs index c8d5dac..23da652 100644 --- a/source/Syntax/Abstract.hs +++ b/source/Syntax/Abstract.hs @@ -338,6 +338,10 @@ data Defn | DefnOp SymbolPattern Expr deriving (Show, Eq, Ord) +data CalcQuantifier + = CalcQuantifier (NonEmpty VarSymbol) Bound (Maybe Stmt) + deriving (Show, Eq, Ord) + data Proof = Omitted | Qed Justification @@ -351,7 +355,7 @@ data Proof | Assume Stmt Proof | FixSymbolic (NonEmpty VarSymbol) Bound Proof | FixSuchThat (NonEmpty VarSymbol) Stmt Proof - | Calc Calc Proof + | Calc (Maybe CalcQuantifier) Calc Proof -- ^ Simplify goals that are implications or disjunctions. | TakeVar (NonEmpty VarSymbol) Bound Stmt Justification Proof | TakeNoun (NounPhrase []) Justification Proof diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs index 9b947b0..383f348 100644 --- a/source/Syntax/Concrete.hs +++ b/source/Syntax/Concrete.hs @@ -211,7 +211,6 @@ grammar lexicon@Lexicon{..} = mdo suchStmt <- rule $ _suchThat *> stmt <* optional _comma - -- Symbolic quantifications with or without generalized bounds. symbolicForall <- rule $ SymbolicForall <$> ((_forAll <|> _forEvery) *> beginMath *> varSymbols) @@ -327,9 +326,16 @@ grammar lexicon@Lexicon{..} = mdo let alignedIff = symbol "&" *> command "iff" <?> "\"&\\iff\"" biconditionalItem <- rule $ (,) <$> (alignedIff *> formula) <*> explanation - biconditionals <- rule $ Biconditionals <$> formula <*> (many1 biconditionalItem) + biconditionals <- rule $ Biconditionals <$> formula <*> (many1 biconditionalItem) <* optional _dot + - calc <- rule $ Calc <$> align (equations <|> biconditionals) <*> proof + calcQuantifier <- rule $ CalcQuantifier <$> + ((_forAll <|> _forEvery) *> beginMath *> varSymbols) + <*> maybeBounded <* endMath + <*> optional suchStmt + <* optional _have + + calc <- rule $ Calc <$> optional calcQuantifier <*> align (equations <|> biconditionals) <*> proof caseOf <- rule $ command "caseOf" *> token InvisibleBraceL *> stmt <* _dot <* token InvisibleBraceR byCases <- rule $ ByCase <$> env_ "byCase" (many1_ (Case <$> caseOf <*> proof)) @@ -349,39 +355,40 @@ grammar lexicon@Lexicon{..} = mdo subclaim <- rule $ Subclaim <$> (_show *> stmt <* _dot) <*> env_ "subproof" proof <*> proof have <- rule $ Have <$> optional (_since *> stmt <* _comma <* _have) <* optional _haveIntro <*> stmt <*> justification <* _dot <*> proof + define <- rule $ Define <$> (_let *> beginMath *> varSymbol <* _eq) <*> expr <* endMath <* _dot <*> proof defineFunction <- rule $ DefineFunction <$> (_let *> beginMath *> varSymbol) <*> paren varSymbol <* _eq <*> expr <* endMath <* _for <* beginMath <*> varSymbol <* _in <*> expr <* endMath <* _dot <*> proof - - -- Define $f $\fromTo{X}{Y} such that, + + -- Define $f $\fromTo{X}{Y} such that, -- Define function $f: X \to Y$, -- \begin{align} - -- &x \mapsto 3*x &, + -- &x \mapsto 3*x &, -- &x \mapsto 4*k &, \forall k \in \N. x \in \Set{k} -- \end{align} - -- + -- -- Follwing is the definition right now. -- Define function $f: X \to Y$ such that, -- \begin{cases} -- 1 & \text{if } x \in \mathbb{Q}\\ -- 0 & \text{if } x \in \mathbb{R}\setminus\mathbb{Q} - -- 3 & \text{else} + -- 3 & \text{else} -- \end{cases} functionDefineCase <- rule $ (,) <$> (optional _ampersand *> expr) <*> (_ampersand *> text _if *> formula) - defineFunctionLocal <- rule $ DefineFunctionLocal + defineFunctionLocal <- rule $ DefineFunctionLocal <$> (_define *> beginMath *> varSymbol) -- Define $ f <*> (_colon *> varSymbol) -- : 'var' \to 'var' - <*> (_to *> expr <* endMath <* _suchThat) + <*> (_to *> expr <* endMath <* _suchThat) -- <*> (_suchThat *> align (many1 ((_ampersand *> varSymbol <* _mapsto) <*> exprApp <*> (_ampersand *> formula)))) -- <*> (_suchThat *> align (many1 (varSymbol <* exprApp <* formula))) <*> (beginMath *> varSymbol) <*> (paren varSymbol <* _eq ) - <*> cases (many1 functionDefineCase) <* endMath <* optional _dot + <*> cases (many1 functionDefineCase) <* endMath <* optional _dot <*> proof diff --git a/source/Syntax/Internal.hs b/source/Syntax/Internal.hs index 6a53aa6..f185025 100644 --- a/source/Syntax/Internal.hs +++ b/source/Syntax/Internal.hs @@ -329,7 +329,7 @@ makeIff :: [ExprOf a] -> ExprOf a makeIff = \case [] -> Bottom es -> List.foldl1' Iff es - + makeXor :: [ExprOf a] -> ExprOf a makeXor = \case [] -> Bottom @@ -404,6 +404,10 @@ data IntroRule = IntroRule } deriving (Show, Eq, Ord) +data CalcQuantifier + = CalcForall (NonEmpty VarSymbol) (Maybe Formula) + | CalcUnquantified + deriving (Show, Eq, Ord) data Proof = Omitted @@ -435,7 +439,7 @@ data Proof | Have Formula Justification Proof -- ^ An affirmation, e.g.: /@We have \<stmt\> by \<ref\>@/. -- - | Calc Calc Proof + | Calc CalcQuantifier Calc Proof | Subclaim Formula Proof Proof -- ^ A claim is a sublemma with its own proof: -- @@ -474,25 +478,32 @@ deriving instance Show Calc deriving instance Eq Calc deriving instance Ord Calc -calcResult :: Calc -> ExprOf VarSymbol -calcResult = \case - Equation e eqns -> e `Equals` fst (NonEmpty.last eqns) - Biconditionals phi phis -> phi `Iff` fst (NonEmpty.last phis) +calcQuant :: CalcQuantifier -> (Formula -> Formula) +calcQuant = \case + CalcUnquantified -> id + CalcForall xs maySuchThat -> case maySuchThat of + Nothing -> makeForall xs + Just suchThat -> \phi -> makeForall xs (suchThat `Implies` phi) + +calcResult :: CalcQuantifier -> Calc -> ExprOf VarSymbol +calcResult quant = \case + Equation e eqns -> calcQuant quant (e `Equals` fst (NonEmpty.last eqns)) + Biconditionals phi phis -> calcQuant quant (phi `Iff` fst (NonEmpty.last phis)) -calculation :: Calc -> [(ExprOf VarSymbol, Justification)] -calculation = \case - Equation e1 eqns@((e2, jst) :| _) -> (e1 `Equals` e2, jst) : collectEquations (toList eqns) - Biconditionals p1 ps@((p2, jst) :| _) -> (p1 `Iff` p2, jst) : collectBiconditionals (toList ps) +calculation :: CalcQuantifier -> Calc -> [(ExprOf VarSymbol, Justification)] +calculation quant = \case + Equation e1 eqns@((e2, jst) :| _) -> (calcQuant quant (e1 `Equals` e2), jst) : collectEquations quant (toList eqns) + Biconditionals p1 ps@((p2, jst) :| _) -> (calcQuant quant (p1 `Iff` p2), jst) : collectBiconditionals quant (toList ps) -collectEquations :: [(ExprOf a, b)] -> [(ExprOf a, b)] -collectEquations = \case - (e1, _) : eqns'@((e2, jst) : _) -> (e1 `Equals` e2, jst) : collectEquations eqns' +collectEquations :: CalcQuantifier -> [(Formula, j)] -> [(Formula, j)] +collectEquations quant = \case + (e1, _) : eqns'@((e2, jst) : _) -> (calcQuant quant (e1 `Equals` e2), jst) : collectEquations quant eqns' _ -> [] -collectBiconditionals :: [(ExprOf a, b)] -> [(ExprOf a, b)] -collectBiconditionals = \case - (p1, _) : ps@((p2, jst) : _) -> (p1 `Iff` p2, jst) : collectEquations ps +collectBiconditionals :: CalcQuantifier -> [(Formula, j)] -> [(Formula, j)] +collectBiconditionals quant = \case + (p1, _) : ps@((p2, jst) : _) -> (calcQuant quant (p1 `Iff` p2), jst) : collectBiconditionals quant ps _ -> [] diff --git a/source/Syntax/Token.hs b/source/Syntax/Token.hs index 53e1e6a..2dad049 100644 --- a/source/Syntax/Token.hs +++ b/source/Syntax/Token.hs @@ -321,14 +321,17 @@ var = guardM isMathMode *> lexeme (fmap Variable var') where var' = do alphabeticPart <- letter <|> bb <|> greek - variationPart <- subscriptNumber <|> ticked <|> pure "" + variationPart <- subscript <|> ticked <|> pure "" pure (alphabeticPart <> variationPart) - subscriptNumber :: Lexer Text - subscriptNumber = do + subscript :: Lexer Text + subscript = do Char.char '_' - n <- some Char.digitChar - pure (Text.pack n) + unbraced <|> braced <|> text + where + unbraced = Text.singleton <$> Char.alphaNumChar + braced = Text.pack <$> (Char.char '{' *> many Char.alphaNumChar <* Char.char '}') + text = Char.string "\\text" *> braced -- for rendering the subscript in roman type -- Temporary hack to fit the TPTP format. ticked :: Lexer Text |