Everything-I-Know-About-Types
/
bergamot-elm
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
84 Commits 1 Branch 0 Tags 225 KiB
Commit Graph

84 Commits

Author SHA1 Message Date
Danila Fedorin 14b63fccc2 Revert "Reduce gas for proof search" 
This reverts commit 6a952f8a15.
 2024-04-20 14:10:18 -07:00
Danila Fedorin 6a952f8a15 Reduce gas for proof search 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2024-04-20 14:05:50 -07:00
Danila Fedorin cd9a048832 Optimize the Elm JS. 2023-12-30 20:04:12 -08:00
Danila Fedorin f35a8d17e8 Add a text for no proofs 2023-12-29 00:07:14 -08:00
Danila Fedorin 98562eca2d Use the same 'literal' term for all object language literals 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-26 13:19:15 -08:00
Danila Fedorin 0b3469b49a Add string and float literals to the object language 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-26 13:15:56 -08:00
Danila Fedorin b828c73e43 Tweak builtin rules to handle floats and more 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-26 13:08:24 -08:00
Danila Fedorin 4c12fee4aa Support parsing float literals in Bergamot 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-26 13:08:09 -08:00
Danila Fedorin 29a95d2659 Add float literals to Bergamot 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-26 13:07:52 -08:00
Danila Fedorin 97fcae9c2c Tweak render rules to handle precedence 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-25 18:32:15 -08:00
Danila Fedorin c192193c57 Add some more builtins to support rendering rules 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-25 18:24:55 -08:00
Danila Fedorin 287562619d Use 'value' for textarea inputs 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-25 13:51:44 -08:00
Danila Fedorin 7d07b2dee9 Put lazy2 back 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-25 13:45:40 -08:00
Danila Fedorin 10d1edbc32 Add error reporting 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-25 13:42:20 -08:00
Danila Fedorin aac1c7f961 Rename some parser functions in ObjectLanguage.elm 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-25 11:51:50 -08:00
Danila Fedorin bc83f0ed53 Add bidirectional inference for `int(?x)` and `str(?x)`. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-22 21:59:41 -08:00
Danila Fedorin 12d823e944 Configure prommpts via a Bergamot program, too. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-22 15:58:52 -08:00
Danila Fedorin 9fd60b4013 Reorganize the UI somewhat and add conclusion-only view 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-22 15:22:46 -08:00
Danila Fedorin aa7fd44a6d Slightly tweak code for proving a term 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-22 14:39:52 -08:00
Danila Fedorin da470f5caa Add an occurss check to avoid infinite terms 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-22 14:39:35 -08:00
Danila Fedorin abd6a848f8 Add support for editing the meta rules 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-21 16:57:46 -08:00
Danila Fedorin 535c714b47 Remove yields and switch to depth-based gas. 
This considerably speeds up forward inference, but we do get lost when
trying to prove more difficult things, or doing backwards search.

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-21 16:47:56 -08:00
Danila Fedorin 363e52ec5e Switch entirely to using rules to render rules. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-21 14:45:04 -08:00
Danila Fedorin 84c79ddb50 Render sections in widget 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-21 14:06:37 -08:00
Danila Fedorin 678e51f146 Allow implicit sections to have more than one rule 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-21 14:06:10 -08:00
Danila Fedorin 401883c1da Update the object language parser to use 'number' and 'string' 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-21 14:05:03 -08:00
Danila Fedorin fd301806c6 Add sections to the language syntax 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-21 13:31:53 -08:00
Danila Fedorin 18d524a0d2 Avoid checking for out-of-gas on each 'andThen' 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-02 23:46:24 -08:00
Danila Fedorin d6d610c038 Save the current rules I'm using for rendering LaTeX. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-02 00:27:41 -08:00
Danila Fedorin 11dd5ee9fd Put render rules separately from regular rules 
This should let us hide them from the user and maybe speed up rendering

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-02 00:25:23 -08:00
Danila Fedorin 1d3f3fd3f8 Use 'lazy' to speed up re-rendering 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-02 00:07:01 -08:00
Danila Fedorin f964a60412 Perform metavariable substitution from quoting 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-02 00:06:33 -08:00
Danila Fedorin 1fca9171b1 Unify conclusion before instantiating premises to save some time 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-01 23:40:29 -08:00
Danila Fedorin 12fa4dc1fd WIP: Use bergamot to render inference rules. 
Not the proof trees yet, but it should be about the same.
 2023-12-01 23:31:43 -08:00
Danila Fedorin 549527d0cc Add a 'call' primitive 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-01 18:15:32 -08:00
Danila Fedorin 905b760dd7 Fix a few bugs with encoding / decoding strings 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-01 18:15:17 -08:00
Danila Fedorin a1ae15d84c Add a new builtin to identify symbols 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-01 16:56:27 -08:00
Danila Fedorin 012c1b0d0c Extract common utility functions and convert symbols to strings 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-01 16:40:39 -08:00
Danila Fedorin 1e12dc8032 Ensure metavariables aren't re-used in rules and queries 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-01 16:35:22 -08:00
Danila Fedorin f4619672a9 Implement more builtins 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-01 16:26:34 -08:00
Danila Fedorin faa65ff77b Don't encode '\n' for now 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-01 16:26:08 -08:00
Danila Fedorin 66fbfd1962 Add necessary escape characters for LaTeX and pretty printing 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-01 16:25:39 -08:00
Danila Fedorin 22f3937523 Fix a parser bug to parse '1' as IntLit 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-01 16:24:19 -08:00
Danila Fedorin 3232d80376 Add syntax sugar for lists 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-01 14:11:40 -08:00
Danila Fedorin a8f07dd422 Tweak pretty printing of LaTeX 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-01 14:09:12 -08:00
Danila Fedorin e659172320 Add a builtin rule for string concatenation 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-01 13:10:51 -08:00
Danila Fedorin 546265f2e6 Add string literals to the term language 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-01 12:55:11 -08:00
Danila Fedorin 45a04cc59c Add a mode for entering the object language to parse 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-12-01 11:31:38 -08:00
Danila Fedorin 51c78af138 Add an initial parser for the Bergamot 'object language' 2023-11-30 22:44:20 -08:00
Danila Fedorin d9f9522365 Add a tab to switch between editor and rendered view 2023-11-30 21:29:37 -08:00