kana-sama

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

kana-sama

% hpack; cabal run --ghc-options "-O2"
benchmarking strict
time                 115.7 μs   (114.9 μs .. 116.5 μs)
                     0.999 R²   (0.998 R² .. 0.999 R²)
mean                 118.8 μs   (116.9 μs .. 121.0 μs)
std dev              6.537 μs   (5.279 μs .. 7.705 μs)
variance introduced by outliers: 56% (severely inflated)

benchmarking lazy
time                 529.3 μs   (523.9 μs .. 535.1 μs)

kana-sama

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}

kana-sama

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE LambdaCase #-}

import Data.Void
import Text.Megaparsec hiding (Token)
import Text.Read (reads)

data Token
  = TokParenL
  | TokParenR

kana-sama

From mathcomp Require Import all_ssreflect.


(* Expr lang *)

Inductive expr : Type :=
| Const of nat
| Plus of expr & expr
| Minus of expr & expr
| Mult of expr & expr.

kana-sama

use num_derive::FromPrimitive;
use num_traits::FromPrimitive;
use std::collections::HashMap;

use Instruction::*;
#[derive(FromPrimitive, Clone, Debug)]
enum Instruction {
  // stack
  LIT,
  DROP,

kana-sama

// builtin
type ns_the<a, b extends a> = b
type at<a, b extends keyof a> = a[b]
type array<a> = a[]
type merge<a, b> = Omit<a, keyof b> & b

// source:
/*
def plus_map : array(array(number)) :=
  [[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50], [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50], [2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50], [3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50], [4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20

kana-sama

type ok<value, rest> = [value, rest];
type fail = [];
type fix_intersection<a> = { [key in keyof a]: a[key] }

type parse_substring<sub extends string, s1> =
  s1 extends `${sub}${infer s2}` ?
  ok<null, s2> : fail;

type space = " " | "\n";
type parse_space<s1> =

kana-sama

declare type Space = " " | "\n" | "\t";
declare type LetterL = "a" | "b" | "c" | "d" | "e" | "f" | "g" | "h" | "i" | "j" | "k" | "l" | "m" | "n" | "o" | "p" | "q" | "r" | "s" | "t" | "u" | "v" | "w" | "x" | "y" | "z";
declare type Letter = LetterL | Uppercase<LetterL>;
declare type Digit = "0" | "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9";
declare type Alphanumeric = Letter | Digit;
declare type Trim<S> = S extends `${Space}${infer S}` ? Trim<S> : S extends `${infer S}${Space}` ? Trim<S> : S;
declare type ParseIdent2<S, OS> = S extends `${Alphanumeric}${infer X}` ? ParseIdent2<X, OS> : S extends "" ? OS : never;
declare type ParseIdent<S> = S extends `${Letter}${infer X}` ? ParseIdent2<X, S> : never;
declare type ParseIfaceProperty<S> = S extends `${infer Name}: ${infer Type}` ? {
    ok: true;

kana-sama

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}