coinconclusive

/* Copyright © 2023 Anne Redko */
/* Under the MIT License. https://mit-license.org/ */

#include <assert.h>
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <ctype.h>
#include <stdint.h>
#include <stddef.h>

coinconclusive

# by coinconclusive. in public domain.
from __future__ import annotations
from dataclasses import dataclass
from typing import ClassVar

@dataclass
class Lam:
    name: str
    body: Expr
    def __str__(self):

leddoo

// a very minimal instruction set.
// it has just enough operations to implement a recursive
// fibonacci function - what a coincidence :D
// NOTE: in my VM, i don't use an `enum`.
//  this is just for simplicity.
#[derive(Clone, Copy, Debug)]
enum Instruction {
    LoadInt     { dst: u8, value: i16 },
    Copy        { dst: u8, src: u8 },
    Add         { dst: u8, src1: u8, src2: u8 },

AndrasKovacs

{-
At ICFP 2022 I attended a talk given by Tomasz Drab, about this paper:

    "A simple and efficient implementation of strong call by need by an abstract machine"
    https://dl.acm.org/doi/10.1145/3549822

This is right up my alley since I've implemented strong call-by-need evaluation
quite a few times (without ever doing more formal analysis of it) and I'm also
interested in performance improvements. Such evaluation is required in
conversion checking in dependently typed languages.

mb64

(* Compile with:
  $ ocamlfind ocamlc -package angstrom,stdio -linkpkg tychk.ml -o tychk
Example use:
  $ ./tychk <<EOF
  > let f = (fun x -> x) : forall a. a -> a
  > in f f
  > EOF
  input : forall a. a -> a
*)