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

59 Commits

Author SHA1 Message Date
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
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
Danila Fedorin
bb18c8bd8c Tweak the HTML tags generated by Bergamot. 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-11-29 22:20:55 -08:00
Danila Fedorin
e1c6e5e83f Use 'gas' instead of yields to limit recursion 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-11-26 21:28:27 -08:00
Danila Fedorin
9d287a37d5 Add flags for setting rules and query before starting 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-11-26 20:53:31 -08:00
Danila Fedorin
f30752a2c6 Minor tweaks to pretty printing and CSS 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-11-26 20:48:48 -08:00
Danila Fedorin
e0532fb581 Fix the parser and add more syntax pretty printing 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-11-26 20:44:27 -08:00
Danila Fedorin
ff1ea05784 Add yielding to help proof search 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-11-26 17:17:10 -08:00
Danila Fedorin
4deb7bc556 Minor tweaks to style and rule rendering 2023-11-26 16:32:27 -08:00
Danila Fedorin
33c3f87564 Add some styling (still very early stages) 2023-11-26 16:25:23 -08:00
Danila Fedorin
acc769e799 Add LaTeX support for rendering rules 2023-11-26 15:54:01 -08:00
Danila Fedorin
7cc5d05e9c Add a way to print the rules as LaTeX 2023-11-26 14:34:52 -08:00
Danila Fedorin
e123f24af0 Add support for reifying proof trees 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-11-26 13:14:44 -08:00
Danila Fedorin
a24fbad249 Make Metavariable and UnificationVar newtypes to help type safety 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-11-26 12:58:38 -08:00
Danila Fedorin
985be53367 Add an interactive 'can this query be satisfied' interface 2023-11-26 12:47:05 -08:00
Danila Fedorin
9f7b59c65d Instantiate the query-to-be-proven as well 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-11-26 12:32:28 -08:00
Danila Fedorin
2f1cb79013 Clean up the search and proving code somewhat 2023-11-26 12:27:44 -08:00
Danila Fedorin
efe0efbee7 Add a (debug) interactive demo 2023-11-26 11:58:20 -08:00
Danila Fedorin
800c96dc7b Add an initial Main.elm file 2023-11-26 11:43:38 -08:00
Danila Fedorin
95c30b6891 Also parse whole programs 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-11-26 11:42:46 -08:00
Danila Fedorin
295c93e38a Add a parser for the tiny language 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-11-26 11:40:15 -08:00
Danila Fedorin
6271dd8c2b Add an initial implementation of proof search 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2023-11-26 00:45:05 -08:00