diff options
Diffstat (limited to 'source/Syntax/Concrete.hs')
| -rw-r--r-- | source/Syntax/Concrete.hs | 27 |
1 files changed, 26 insertions, 1 deletions
diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs index b51b738..51cc013 100644 --- a/source/Syntax/Concrete.hs +++ b/source/Syntax/Concrete.hs @@ -351,8 +351,23 @@ grammar lexicon@Lexicon{..} = mdo 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 + - proof <- rule $ asum [byContradiction, byCases, bySetInduction, byOrdInduction, calc, subclaim, assume, fix, take, have, suffices, define, defineFunction, qed] + + -- Define $f $\fromTo{X}{Y} such that, + -- Define function $f: X \to Y$, + -- \begin{align} + -- &x \mapsto 3*x &, + -- &x \mapsto 4*k+x &, + -- \end{align} + -- + defineFunctionMathy <- rule $ DefineFunctionMathy + <$> (_define *> beginMath *> varSymbol) -- Define $ f + <*> _colon *> varSymbol <*> _to *> varSymbol -- : 'var' \to 'var' + <*> localFunctionDefinitionAlign + + + proof <- rule $ asum [byContradiction, byCases, bySetInduction, byOrdInduction, calc, subclaim, assume, fix, take, have, suffices, define, defineFunction, defineFunctionMathy, qed] blockAxiom <- rule $ uncurry3 BlockAxiom <$> envPos "axiom" axiom @@ -435,7 +450,17 @@ enumeratedMarked1 :: Prod r Text (Located Token) a -> Prod r Text (Located Token enumeratedMarked1 p = begin "enumerate" *> many1 ((,) <$> (command "item" *> label) <*> p) <* end "enumerate" <?> "\"\\begin{enumerate}\\item\\label{...}...\"" +-- &x \mapsto 'someexpr' &, for x +localFunctionDefinitionAlign :: Prod r Text (Located Token) a -> Prod r Text (Located Token) (Marker, a) +localFunctionDefinitionAlign p = begin "align" *> many1 funDefExp <* end "align" + <?> "\"\\begin{algin} &x \\mapsto x+2 , x \\in X \\ \\end{algin}\"" + + +funDefExp :: Prod r Text (Located Token) a -> Prod r Text (Located Token) [(Marker, a)] +funDefExp p = NonEmpty.toList <$> ( _ampersand *> varSymbol <*> funDefExpRange <*> (_ampersand *> varSymbol <* _in) <*> varSymbol) -- the last var should be a expression +funDefRange :: Prod r Text (Located Token) a -> Prod r Text (Located Token) (NonEmpty (Marker, a)) +funDefRange p = _mapsto *> varSymbol -- TODO: this Var has to be changed to a expression -- This function could be rewritten, so that it can be used directly in the grammar, -- instead of with specialized variants. |