Commit Graph

Select branches

Hide Pull Requests

main

Mono Color

• 2af1692bf4 Remove symeq main Danila Fedorin 2024-11-03 17:13:14 -0800
• 0b4a1f2ebd Implement hidden sections Danila Fedorin 2024-11-03 17:13:05 -0800
• c77bb6f900 Add some forward-only arithmetic operations and make rho render as LaTeX Danila Fedorin 2024-09-15 16:33:07 -0700
• e7d3e840b3 Allow input mode code to provide custom error messages Danila Fedorin 2024-09-15 10:21:38 -0700
• a17ea205c7 Clear 'Failed' flag when input changes Danila Fedorin 2024-09-07 22:56:42 -0700
• 2a0db676bc Remove useless inputRules flag Danila Fedorin 2024-09-07 22:54:13 -0700
• a7b3efe56c Tweak API to support syntax errors in custom parsing Danila Fedorin 2024-09-07 22:29:32 -0700
• ec0b05ab51 Make 'language term' just a custom mode Danila Fedorin 2024-09-07 22:23:04 -0700
• bfc21c2928 Add support for custom modes Danila Fedorin 2024-09-07 21:43:02 -0700
• d1fb4bfdc1 Update index.html to work with new setup Danila Fedorin 2024-09-07 21:06:57 -0700
• b6569d8ca0 Allow for customizing the "input mode" toolbar Danila Fedorin 2024-09-07 21:02:15 -0700
• 14b63fccc2 Revert "Reduce gas for proof search" Danila Fedorin 2024-04-20 14:10:18 -0700
• 6a952f8a15 Reduce gas for proof search Danila Fedorin 2024-04-20 14:05:50 -0700
• cd9a048832 Optimize the Elm JS. Danila Fedorin 2023-12-30 20:04:12 -0800
• f35a8d17e8 Add a text for no proofs Danila Fedorin 2023-12-29 00:07:14 -0800
• 98562eca2d Use the same 'literal' term for all object language literals Danila Fedorin 2023-12-26 13:19:15 -0800
• 0b3469b49a Add string and float literals to the object language Danila Fedorin 2023-12-26 13:15:56 -0800
• b828c73e43 Tweak builtin rules to handle floats and more Danila Fedorin 2023-12-26 13:08:24 -0800
• 4c12fee4aa Support parsing float literals in Bergamot Danila Fedorin 2023-12-26 13:08:09 -0800
• 29a95d2659 Add float literals to Bergamot Danila Fedorin 2023-12-26 13:07:52 -0800
• 97fcae9c2c Tweak render rules to handle precedence Danila Fedorin 2023-12-25 18:32:15 -0800
• c192193c57 Add some more builtins to support rendering rules Danila Fedorin 2023-12-25 18:24:55 -0800
• 287562619d Use 'value' for textarea inputs Danila Fedorin 2023-12-25 13:51:44 -0800
• 7d07b2dee9 Put lazy2 back Danila Fedorin 2023-12-25 13:45:40 -0800
• 10d1edbc32 Add error reporting Danila Fedorin 2023-12-25 13:42:20 -0800
• aac1c7f961 Rename some parser functions in ObjectLanguage.elm Danila Fedorin 2023-12-25 11:51:50 -0800
• bc83f0ed53 Add bidirectional inference for int(?x) and str(?x). Danila Fedorin 2023-12-22 21:59:41 -0800
• 12d823e944 Configure prommpts via a Bergamot program, too. Danila Fedorin 2023-12-22 15:58:52 -0800
• 9fd60b4013 Reorganize the UI somewhat and add conclusion-only view Danila Fedorin 2023-12-22 15:22:46 -0800
• aa7fd44a6d Slightly tweak code for proving a term Danila Fedorin 2023-12-22 14:39:52 -0800
• da470f5caa Add an occurss check to avoid infinite terms Danila Fedorin 2023-12-22 14:39:35 -0800
• abd6a848f8 Add support for editing the meta rules Danila Fedorin 2023-12-21 16:57:46 -0800
• 535c714b47 Remove yields and switch to depth-based gas. Danila Fedorin 2023-12-21 16:47:56 -0800
• 363e52ec5e Switch entirely to using rules to render rules. Danila Fedorin 2023-12-21 14:45:04 -0800
• 84c79ddb50 Render sections in widget Danila Fedorin 2023-12-21 14:06:37 -0800
• 678e51f146 Allow implicit sections to have more than one rule Danila Fedorin 2023-12-21 14:06:10 -0800
• 401883c1da Update the object language parser to use 'number' and 'string' Danila Fedorin 2023-12-21 14:05:03 -0800
• fd301806c6 Add sections to the language syntax Danila Fedorin 2023-12-21 13:31:53 -0800
• 18d524a0d2 Avoid checking for out-of-gas on each 'andThen' Danila Fedorin 2023-12-02 23:46:24 -0800
• d6d610c038 Save the current rules I'm using for rendering LaTeX. Danila Fedorin 2023-12-02 00:27:41 -0800
• 11dd5ee9fd Put render rules separately from regular rules Danila Fedorin 2023-12-02 00:25:23 -0800
• 1d3f3fd3f8 Use 'lazy' to speed up re-rendering Danila Fedorin 2023-12-02 00:07:01 -0800
• f964a60412 Perform metavariable substitution from quoting Danila Fedorin 2023-12-02 00:06:33 -0800
• 1fca9171b1 Unify conclusion before instantiating premises to save some time Danila Fedorin 2023-12-01 23:40:29 -0800
• 12fa4dc1fd WIP: Use bergamot to render inference rules. Danila Fedorin 2023-12-01 23:31:43 -0800
• 549527d0cc Add a 'call' primitive Danila Fedorin 2023-12-01 18:15:32 -0800
• 905b760dd7 Fix a few bugs with encoding / decoding strings Danila Fedorin 2023-12-01 18:15:17 -0800
• a1ae15d84c Add a new builtin to identify symbols Danila Fedorin 2023-12-01 16:56:27 -0800
• 012c1b0d0c Extract common utility functions and convert symbols to strings Danila Fedorin 2023-12-01 16:38:46 -0800
• 1e12dc8032 Ensure metavariables aren't re-used in rules and queries Danila Fedorin 2023-12-01 16:35:22 -0800
• f4619672a9 Implement more builtins Danila Fedorin 2023-12-01 16:26:34 -0800
• faa65ff77b Don't encode '\n' for now Danila Fedorin 2023-12-01 16:26:08 -0800
• 66fbfd1962 Add necessary escape characters for LaTeX and pretty printing Danila Fedorin 2023-12-01 16:25:39 -0800
• 22f3937523 Fix a parser bug to parse '1' as IntLit Danila Fedorin 2023-12-01 16:24:19 -0800
• 3232d80376 Add syntax sugar for lists Danila Fedorin 2023-12-01 14:11:40 -0800
• a8f07dd422 Tweak pretty printing of LaTeX Danila Fedorin 2023-12-01 14:09:12 -0800
• e659172320 Add a builtin rule for string concatenation Danila Fedorin 2023-12-01 13:10:51 -0800
• 546265f2e6 Add string literals to the term language Danila Fedorin 2023-12-01 12:55:11 -0800
• 45a04cc59c Add a mode for entering the object language to parse Danila Fedorin 2023-12-01 11:31:38 -0800
• 51c78af138 Add an initial parser for the Bergamot 'object language' Danila Fedorin 2023-11-30 22:44:20 -0800
• d9f9522365 Add a tab to switch between editor and rendered view Danila Fedorin 2023-11-30 21:29:37 -0800
• bb18c8bd8c Tweak the HTML tags generated by Bergamot. Danila Fedorin 2023-11-29 22:20:55 -0800
• 524796d74f More strictly control what goes into elm.nix Danila Fedorin 2023-11-30 04:22:02 +0000
• cd2d6366b0 Add a flake file to build the project Danila Fedorin 2023-11-30 04:02:58 +0000
• a34e143408 Add Nix-specific generated dependencies Danila Fedorin 2023-11-29 19:47:30 -0800
• e1c6e5e83f Use 'gas' instead of yields to limit recursion Danila Fedorin 2023-11-26 21:28:27 -0800
• 9d287a37d5 Add flags for setting rules and query before starting Danila Fedorin 2023-11-26 20:53:31 -0800
• f30752a2c6 Minor tweaks to pretty printing and CSS Danila Fedorin 2023-11-26 20:48:48 -0800
• e0532fb581 Fix the parser and add more syntax pretty printing Danila Fedorin 2023-11-26 20:44:27 -0800
• ff1ea05784 Add yielding to help proof search Danila Fedorin 2023-11-26 17:17:10 -0800
• 4deb7bc556 Minor tweaks to style and rule rendering Danila Fedorin 2023-11-26 16:32:27 -0800
• 33c3f87564 Add some styling (still very early stages) Danila Fedorin 2023-11-26 16:25:23 -0800
• 250dbb4ee8 Add an index.html file that includes the web component Danila Fedorin 2023-11-26 15:54:17 -0800
• acc769e799 Add LaTeX support for rendering rules Danila Fedorin 2023-11-26 15:54:01 -0800
• 7cc5d05e9c Add a way to print the rules as LaTeX Danila Fedorin 2023-11-26 14:34:52 -0800
• e123f24af0 Add support for reifying proof trees Danila Fedorin 2023-11-26 13:14:44 -0800
• a24fbad249 Make Metavariable and UnificationVar newtypes to help type safety Danila Fedorin 2023-11-26 12:58:38 -0800
• 985be53367 Add an interactive 'can this query be satisfied' interface Danila Fedorin 2023-11-26 12:47:05 -0800
• 9f7b59c65d Instantiate the query-to-be-proven as well Danila Fedorin 2023-11-26 12:32:28 -0800
• 2f1cb79013 Clean up the search and proving code somewhat Danila Fedorin 2023-11-26 12:27:44 -0800
• efe0efbee7 Add a (debug) interactive demo Danila Fedorin 2023-11-26 11:58:20 -0800
• 800c96dc7b Add an initial Main.elm file Danila Fedorin 2023-11-26 11:43:38 -0800
• 95c30b6891 Also parse whole programs Danila Fedorin 2023-11-26 11:42:46 -0800
• 295c93e38a Add a parser for the tiny language Danila Fedorin 2023-11-26 11:40:15 -0800
• 6271dd8c2b Add an initial implementation of proof search Danila Fedorin 2023-11-26 00:45:05 -0800
• 7d78db96d6 Add a useful helper function to the instantiation state Danila Fedorin 2023-11-26 00:44:43 -0800
• b13cdea15d Add a few more convenient operations to Search.elm Danila Fedorin 2023-11-26 00:44:24 -0800
• 2cc1012a09 Add an initial 'lazy list' for doing backtracking Danila Fedorin 2023-11-25 23:33:48 -0800
• ed34302627 Add a function to substitute all variables for their values Danila Fedorin 2023-11-25 23:19:36 -0800
• 3269e37ef3 Add some convenience exports to Syntax.elm Danila Fedorin 2023-11-25 23:15:00 -0800
• f4fba66f8b Add instantiating terms of metavariables with variables Danila Fedorin 2023-11-25 23:08:21 -0800
• 824b19123e Fix a bug in unification (lol) Danila Fedorin 2023-11-25 23:08:05 -0800
• a9163c0797 Rename the 'Metavariable' type to 'UnificationVar' Danila Fedorin 2023-11-25 22:53:08 -0800
• bfa9deb0b0 Implement a first draft of unification Danila Fedorin 2023-11-25 22:51:53 -0800
• d0b88ee6df Initial commit Danila Fedorin 2023-11-25 22:51:39 -0800