| from lark import Lark, Transformer, v_args | |
| # 1. Define the grammar for second order logic using ASCII characters | |
| grammar = """ | |
| start: formula | |
| ?expr: arith_expr | |
| | bool_expr | |
| ?arith_expr: term |
A simple boolean language with definitions implemented over Sexp.t
Conclusions:
sexp_of_t and t_of_sexp functions.!!!! from manual !!!!
@TODO: FIX THIS!
| <html> | |
| <head> | |
| <link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/bootstrap@5.2.3/dist/css/bootstrap.min.css" integrity="sha384-rbsA2VBKQhggwzxH7pPCaAqO46MgnOM80zW1RWuH61DGLwZJEdK2Kadq2F9CUG65" crossorigin="anonymous"> | |
| <script src="https://cdn.jsdelivr.net/npm/bootstrap@5.2.3/dist/js/bootstrap.bundle.min.js" integrity="sha384-kenU1KFdBIe4zVF0s0G1M5b4hcpxyD9F7jL+jjXkk+Q2h455rYXK/7HAuoJl+0I4" crossorigin="anonymous"></script> | |
| </head> | |
| <body> | |
| <script> | |
| function html(text, ...values) { | |
| const html = text.flatMap((text, i) => { | |
| return [text, values[i]?.outerHTML || values[i]] |
| from typing import ParamSpec, TypeVar, Callable, reveal_type | |
| T = TypeVar("T") | |
| P = ParamSpec("P") | |
| def tco(f: Callable[P, T]) -> Callable[P, T]: | |
| unwind = False |
| from typing import * | |
| from typing_extensions import ParamSpec | |
| A = TypeVar("A") | |
| B = TypeVar("B") | |
| C = TypeVar("C") | |
| D = TypeVar("D") | |
| E = TypeVar("E") | |
| F = TypeVar("F") | |
| G = TypeVar("G") |
| class Calcparser | |
| prechigh | |
| left '*' '/' | |
| left '+' '-' | |
| preclow | |
| options no_result_var | |
| rule | |
| target: expr |
| open Format | |
| type term = | |
| | Var of int | |
| | Lamb of term | |
| | App of term * term | |
| let rec shift i depth = function | |
| | Var x when x < depth -> Var x | |
| | Var x -> Var (x + i) |
| open Printf | |
| let (%) = Int.logor | |
| let (<<) = Int.shift_left | |
| let (>>) = Int.shift_right | |
| let (&) = Int.logand | |
| let utf_8_bytes_of_unicode i = | |
| if i <= 0x007F | |
| then |
| (** | |
| * Closed Terms Lambda Caulcus with De Bruijn Indexes | |
| * ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ | |
| *) | |
| open Format | |
| type term = | |
| | Var of int | |
| | Lamb of int * term |
| import sys | |
| from functools import partial | |
| class Pipe: | |
| def __init__(self, f, *args, **kwargs): | |
| self.f = f | |
| self.args = args | |
| self.kwargs = kwargs | |
| def __call__(self, replacement): | |
| args = [arg if arg is not Ellipsis else replacement |