diff options
| -rw-r--r-- | library/wunschzettel.tex | 9 | ||||
| -rw-r--r-- | source/Api.hs | 4 | ||||
| -rw-r--r-- | source/Syntax/Abstract.hs | 7 | ||||
| -rw-r--r-- | source/Syntax/Adapt.hs | 14 | ||||
| -rw-r--r-- | source/Syntax/Concrete.hs | 27 | ||||
| -rw-r--r-- | source/Syntax/Concrete/Keywords.hs | 10 |
6 files changed, 67 insertions, 4 deletions
diff --git a/library/wunschzettel.tex b/library/wunschzettel.tex index b2681fd..74ea899 100644 --- a/library/wunschzettel.tex +++ b/library/wunschzettel.tex @@ -45,6 +45,15 @@ Tupel struct % more proof but now i can use the function f % -------------------------------------------------------- + \begin{equation} + X= + \begin{cases} + 0, & \text{if}\ a=1 \\ + 1, & \text{otherwise} + \end{cases} + \end{equation} + + \end{proof} diff --git a/source/Api.hs b/source/Api.hs index 3fb0ca2..1bdf615 100644 --- a/source/Api.hs +++ b/source/Api.hs @@ -203,7 +203,9 @@ describeToken = \case EndEnv _ -> "end of environment" _ -> "delimiter" - +-- | gloss generates internal represantation of the LaTeX files. +-- First the file will be parsed and therefore checkt for grammer. +-- 'meaning' then transfer the raw parsed grammer to the internal semantics. gloss :: MonadIO io => FilePath -> io ([Internal.Block], Lexicon) gloss file = do (blocks, lexicon) <- parse file diff --git a/source/Syntax/Abstract.hs b/source/Syntax/Abstract.hs index 4aa8623..f775b69 100644 --- a/source/Syntax/Abstract.hs +++ b/source/Syntax/Abstract.hs @@ -369,6 +369,13 @@ data Proof -- ^ Local function definition, e.g. /@Let $f(x) = e$ for $x\\in d$@/. -- The first 'VarSymbol' is the newly defined symbol, the second one is the argument. -- The first 'Expr' is the value, the final variable and expr specify a bound (the domain of the function). + + + + + | DefineFunctionMathy VarSymbol VarSymbol VarSymbol [VarSymbol Expr [VarSymbol] Expr ] 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) -- | An inline justification. diff --git a/source/Syntax/Adapt.hs b/source/Syntax/Adapt.hs index 622946a..96fd76d 100644 --- a/source/Syntax/Adapt.hs +++ b/source/Syntax/Adapt.hs @@ -34,6 +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 signature "signature" pos _ -> [] adaptChunks :: [[Located Token]] -> Lexicon -> Lexicon @@ -85,6 +87,18 @@ abbreviation = do skipUntilNextLexicalEnv pure [lexicalItem m] +signatureIntro :: RE Token [ScannedLexicalItem] --since signiture is a used word of haskell we have to name it diffrentliy +signatureIntro = do + sym (BeginEnv "signature") + few notEndOfLexicalEnvToken + m <- label + few anySym + lexicalItem <- head + few anySym + sym (EndEnv "signature") + skipUntilNextLexicalEnv + pure [lexicalItem m] + label :: RE Token Marker label = msym \case Label m -> Just (Marker m) 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. diff --git a/source/Syntax/Concrete/Keywords.hs b/source/Syntax/Concrete/Keywords.hs index 135cdac..b507e7e 100644 --- a/source/Syntax/Concrete/Keywords.hs +++ b/source/Syntax/Concrete/Keywords.hs @@ -108,7 +108,7 @@ _either = word "either" ? "either" _equipped :: Prod r Text (Located Token) SourcePos _equipped = (word "equipped" <|> word "together") <* word "with" ? "equipped with" _every :: Prod r Text (Located Token) SourcePos -_every = (word "every") ? "every" +_every = word "every" ? "every" _exist :: Prod r Text (Located Token) SourcePos _exist = word "there" <* word "exist" ? "there exist" _exists :: Prod r Text (Located Token) SourcePos @@ -124,7 +124,7 @@ _for = word "for" ? "for" _forAll :: Prod r Text (Located Token) SourcePos _forAll = (word "for" <* word "all") <|> word "all" ? "all" _forEvery :: Prod r Text (Located Token) SourcePos -_forEvery = (word "for" <* word "every") <|> (word "every") ? "for every" +_forEvery = (word "for" <* word "every") <|> word "every" ? "for every" _have :: Prod r Text (Located Token) SourcePos _have = word "we" <* word "have" <* optional (word "that") ? "we have" _if :: Prod r Text (Located Token) SourcePos @@ -220,3 +220,9 @@ _in :: Prod r Text (Located Token) SourcePos _in = symbol "∈" <|> command "in" ? "\\in" _subseteq :: Prod r Text (Located Token) SourcePos _subseteq = command "subseteq" ? "\\subseteq" +_to :: Prod r Text (Located Token) SourcePos +_to = command "to" ? "\\to" +_mapsto :: Prod r Text (Located Token) SourcePos +_mapsto = command "mapsto" ? "\\mapsto" +_ampersand :: Prod r Text (Located Token) SourcePos +_ampersand = symbol "&" ? "&"
\ No newline at end of file |