dhilst

(**
 *      Closed Terms Lambda Caulcus with De Bruijn Indexes 
 *      ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 *)

open Format

type term = 
  | Var of int
  | Lamb of int * term

dhilst

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

dhilst

from typing import *
import ast
from dataclasses import dataclass

@dataclass(frozen=True)
class FuncSig:
    name : str
    args : list[str]
    ret: str

dhilst

open Printf

type term = F of string * (term list) | V of string

let rec subst term ((name, replacement) as sub) =
  match term, name with 
  | V x, V y when String.equal x y -> replacement
  | V x, V y when not (String.equal x y) -> term
  | F (x, args), V y -> F (x, List.map (fun arg -> subst arg sub) args)
  | _, _ -> assert false

dhilst

(* A possibly correct unification algorithm implementaion *)
open Printf

type term = F of string * (term list) | V of string

let rec subst subs = function
  | V x -> List.fold_left (fun acc (s, t) -> if x = s then t else V x) (V x) subs 
  | F (x, args) ->
    F (x, 
       List.map (fun arg -> subst subs arg) args)

dhilst

from ast import (
    NodeTransformer,
    arguments,
    arg,
    Lambda,
    parse,
    In,
    Call,
    Expression,
    fix_missing_locations,

dhilst

def gen(start, f):
    return lambda: (start, gen(f(start), f))

def inc(a):
    return a + 1

g = gen(0, inc)
while True:
    x, g = g()
    print(x)

dhilst

--- cpdt/src/DataStruct.v	2020-02-02 12:46:14.000000000 -0300
+++ cpdt-8.13/src/DataStruct.v	2021-12-05 11:05:01.000000000 -0300
@@ -117,8 +117,8 @@
 (* end thide *)
 End ilist.
 
-Arguments Nil [A].
-Arguments First [n].
+Arguments Nil {A}.
+Arguments First {n}.

dhilst

from ast import *


class LetVisitor(NodeTransformer):
    def visit_Call(self, node):

        self.generic_visit(node)

        if (
            type(node.func) is Call

dhilst

(* this is the commutativity on Nat.add (the builtin + in Coq) that only simplifies
   from the left *)
Theorem add_comm : forall (n m : nat), n + m = m + n.
  assert (plus_0_r : forall (n' : nat), n' + 0 = n').
  { induction n'. reflexivity. simpl. rewrite IHn'. reflexivity. }
  induction n, m; try reflexivity; simpl; try rewrite plus_0_r; try reflexivity.
  - rewrite IHn. simpl.
    assert (plus_m_Sn : forall (o p : nat), o + S p = S (o + p)).
    { induction o; intros; simpl; try reflexivity. rewrite IHo. reflexivity. }
    rewrite plus_m_Sn. reflexivity.