diff options
Diffstat (limited to 'source')
| -rw-r--r-- | source/Checking.hs | 13 | ||||
| -rw-r--r-- | source/Meaning.hs | 4 | ||||
| -rw-r--r-- | source/Syntax/Abstract.hs | 2 | ||||
| -rw-r--r-- | source/Syntax/Adapt.hs | 4 | ||||
| -rw-r--r-- | source/Syntax/Concrete.hs | 13 | ||||
| -rw-r--r-- | source/Syntax/Internal.hs | 2 | ||||
| -rw-r--r-- | source/Syntax/Token.hs | 17 |
7 files changed, 36 insertions, 19 deletions
diff --git a/source/Checking.hs b/source/Checking.hs index 817c477..6d55ee1 100644 --- a/source/Checking.hs +++ b/source/Checking.hs @@ -543,7 +543,7 @@ checkProof = \case checkCalc calc assume [Asm (calcResult calc)] checkProof continue - DefineFunctionMathy funVar domVar ranVar argVar definitions continue -> do + DefineFunctionMathy funVar argVar domVar ranExpr definitions continue -> do -- 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) @@ -558,8 +558,8 @@ checkProof = \case setGoals [makeForall [argVar] ((TermVar argVar `IsElementOf` TermVar domVar) `Iff` subdomainConjuctionLocalFunction argVar definitions )] -- check the disjunct union tellTasks - assume [Asm (makeForall [argVar] ((TermVar argVar `IsElementOf` TermVar domVar) `Implies` (TermOp ApplySymbol [TermVar funVar, TermVar argVar] `IsElementOf` TermVar ranVar)))] -- function f from \dom(f) \to \ran(f) - assume (functionSubdomianExpression funVar argVar definitions) --behavior on the subdomians + assume [Asm (makeForall [argVar] ((TermVar argVar `IsElementOf` TermVar domVar) `Implies` (TermOp ApplySymbol [TermVar funVar, TermVar argVar] `IsElementOf` ranExpr)))] -- function f from \dom(f) \to \ran(f) + assume (functionSubdomianExpression funVar argVar (NonEmpty.toList definitions)) --behavior on the subdomians setGoals goals checkProof continue @@ -571,9 +571,10 @@ subdomainConjuctionLocalFunction argVar defintions = in TermVar argVar `IsElementOf` makeConjunction stmts -functionSubdomianExpression :: VarSymbol -> VarSymbol -> NonEmpty (Term, Formula) -> [Asm] -functionSubdomianExpression f a nxs = case nxs of - x:|xs -> singleFunctionSubdomianExpression f a x : functionSubdomianExpression f a (NonEmpty.fromList xs) +functionSubdomianExpression :: VarSymbol -> VarSymbol -> [(Term, Formula)] -> [Asm] +functionSubdomianExpression f a (x:xs) = singleFunctionSubdomianExpression f a x : functionSubdomianExpression f a xs +functionSubdomianExpression _ _ [] = [] + singleFunctionSubdomianExpression :: VarSymbol -> VarSymbol -> (Term, Formula) -> Asm diff --git a/source/Meaning.hs b/source/Meaning.hs index ab98c9a..4a21fa3 100644 --- a/source/Meaning.hs +++ b/source/Meaning.hs @@ -606,9 +606,9 @@ glossProof = \case then Sem.DefineFunction funVar argVar <$> glossExpr valueExpr <*> glossExpr domExpr <*> glossProof proof else error "mismatched variables in function definition." - Raw.DefineFunctionMathy funVar domVar ranVar funVar2 argVar definitions proof -> do + Raw.DefineFunctionMathy funVar domVar ranExpr funVar2 argVar definitions proof -> do if funVar == funVar2 - then Sem.DefineFunctionMathy funVar domVar ranVar argVar <$> (glossLocalFunctionExprDef `each` definitions) <*> glossProof proof + then Sem.DefineFunctionMathy 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 diff --git a/source/Syntax/Abstract.hs b/source/Syntax/Abstract.hs index 6372c87..13691e7 100644 --- a/source/Syntax/Abstract.hs +++ b/source/Syntax/Abstract.hs @@ -373,7 +373,7 @@ data Proof - | DefineFunctionMathy VarSymbol VarSymbol VarSymbol VarSymbol VarSymbol (NonEmpty (Expr, Formula)) Proof + | DefineFunctionMathy VarSymbol VarSymbol Expr VarSymbol VarSymbol (NonEmpty (Expr, Formula)) Proof -- ^ Local function definition, but in this case we give the domain and target an the rules for $xs$ in some sub domains. -- deriving (Show, Eq, Ord) diff --git a/source/Syntax/Adapt.hs b/source/Syntax/Adapt.hs index 3cff497..4b43bc6 100644 --- a/source/Syntax/Adapt.hs +++ b/source/Syntax/Adapt.hs @@ -34,8 +34,8 @@ scanChunk ltoks = matchOrErr struct "struct definition" pos Located{startPos = pos, unLocated = (BeginEnv "inductive")} :_ -> matchOrErr inductive "inductive definition" pos - Located{startPos = pos, unLocated = (BeginEnv "signature")} :_ -> - matchOrErr signatureIntro "signature" pos + --Located{startPos = pos, unLocated = (BeginEnv "signature")} :_ -> + -- matchOrErr signatureIntro "signature" pos _ -> [] adaptChunks :: [[Located Token]] -> Lexicon -> Lexicon diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs index 69280c1..fe08fec 100644 --- a/source/Syntax/Concrete.hs +++ b/source/Syntax/Concrete.hs @@ -373,16 +373,16 @@ grammar lexicon@Lexicon{..} = mdo -- 3 & \text{else} -- \end{cases} - functionDefineCase <- rule $ (,) <$> expr <*> (_ampersand *> formula) + functionDefineCase <- rule $ (,) <$> (_ampersand *> (expr <|> exprVar )) <*> (_comma *> formula) defineFunctionMathy <- rule $ DefineFunctionMathy <$> (_define *> beginMath *> varSymbol) -- Define $ f <*> (_colon *> varSymbol) -- : 'var' \to 'var' - <*> (_to *> varSymbol <* endMath <* _suchThat) + <*> (_to *> expr <* endMath <* _suchThat) -- <*> (_suchThat *> align (many1 ((_ampersand *> varSymbol <* _mapsto) <*> exprApp <*> (_ampersand *> formula)))) -- <*> (_suchThat *> align (many1 (varSymbol <* exprApp <* formula))) - <*> varSymbol <*> varSymbol <* symbol "=" - <*> many1 functionDefineCase - <*> proof + <*> (beginMath *> varSymbol) <*> (paren varSymbol <* _eq <* endMath) + <*> cases (many1 functionDefineCase) + <*> proof @@ -644,6 +644,9 @@ group body = token InvisibleBraceL *> body <* token InvisibleBraceR <?> "\"{...} align :: Prod r Text (Located Token) a -> Prod r Text (Located Token) a align body = begin "align*" *> body <* end "align*" +cases :: Prod r Text (Located Token) a -> Prod r Text (Located Token) a +cases body = begin "cases" *> body <* end "cases" + maybeVarToken :: Located Token -> Maybe VarSymbol maybeVarToken ltok = case unLocated ltok of diff --git a/source/Syntax/Internal.hs b/source/Syntax/Internal.hs index 0e3361d..7046161 100644 --- a/source/Syntax/Internal.hs +++ b/source/Syntax/Internal.hs @@ -436,7 +436,7 @@ data Proof | Define VarSymbol Term Proof | DefineFunction VarSymbol VarSymbol Term Term Proof - | DefineFunctionMathy VarSymbol VarSymbol VarSymbol VarSymbol (NonEmpty (Term, Formula)) Proof + | DefineFunctionMathy VarSymbol VarSymbol VarSymbol Term (NonEmpty (Term, Formula)) Proof deriving instance Show Proof deriving instance Eq Proof diff --git a/source/Syntax/Token.hs b/source/Syntax/Token.hs index cb3f4cb..52da86a 100644 --- a/source/Syntax/Token.hs +++ b/source/Syntax/Token.hs @@ -189,6 +189,7 @@ toks = whitespace *> goNormal id <* eof Nothing -> pure (f []) Just t@Located{unLocated = BeginEnv "math"} -> goMath (f . (t:)) Just t@Located{unLocated = BeginEnv "align*"} -> goMath (f . (t:)) + Just t@Located{unLocated = BeginEnv "cases"} -> goMath (f . (t:)) Just t -> goNormal (f . (t:)) goText f = do r <- optional textToken @@ -204,6 +205,7 @@ toks = whitespace *> goNormal id <* eof Nothing -> pure (f []) Just t@Located{unLocated = EndEnv "math"} -> goNormal (f . (t:)) Just t@Located{unLocated = EndEnv "align*"} -> goNormal (f . (t:)) + Just t@Located{unLocated = EndEnv "cases"} -> goNormal (f . (t:)) Just t@Located{unLocated = BeginEnv "text"} -> goText (f . (t:)) Just t@Located{unLocated = BeginEnv "explanation"} -> goText (f . (t:)) Just t -> goMath (f . (t:)) @@ -219,12 +221,12 @@ toks = whitespace *> goNormal id <* eof -- | Parses a single normal mode token. tok :: Lexer (Located Token) tok = - word <|> var <|> symbol <|> mathBegin <|> alignBegin <|> begin <|> end <|> opening <|> closing <|> label <|> ref <|> command + word <|> var <|> symbol <|> mathBegin <|> alignBegin <|> casesBegin <|> begin <|> end <|> opening <|> closing <|> label <|> ref <|> command -- | Parses a single math mode token. mathToken :: Lexer (Located Token) mathToken = - var <|> symbol <|> number <|> begin <|> alignEnd <|> end <|> opening <|> closing <|> beginText <|> beginExplanation <|> mathEnd <|> command + var <|> symbol <|> number <|> begin <|> alignEnd <|> casesEnd <|> end <|> opening <|> closing <|> beginText <|> beginExplanation <|> mathEnd <|> command beginText :: Lexer (Located Token) beginText = lexeme do @@ -277,6 +279,11 @@ alignBegin = guardM isTextMode *> lexeme do setMathMode pure (BeginEnv "align*") +casesBegin :: Lexer (Located Token) +casesBegin = guardM isTextMode *> lexeme do + Char.string "\\begin{cases}" + setMathMode + pure (BeginEnv "cases") -- | Parses a single end math token. mathEnd :: Lexer (Located Token) @@ -291,6 +298,12 @@ alignEnd = guardM isMathMode *> lexeme do setTextMode pure (EndEnv "align*") +casesEnd :: Lexer (Located Token) +casesEnd = guardM isMathMode *> lexeme do + Char.string "\\end{cases}" + setTextMode + pure (EndEnv "cases") + -- | Parses a word. Words are returned casefolded, since we want to ignore their case later on. word :: Lexer (Located Token) |