qexat

jekyll: a hyper-declarative, statically-typed programming language around environment manipulation

# x is introduced to the environment
{ ..?e } → { x := 3 ; ..?e }
# y too ; ?e is not the same row variable as the one above
{ ..?e } → { y := 5 ; ..?e }
# matching the current context on one that contains an x and a y
# which allows us to add them to introduce y
{ x ; y ; ..?e } → { z := x + y ; ..?e } 

qexat

let ( or ) option default = Option.value option ~default

module Int = struct
  include Int

  let compare i1 i2 =
    let as_int = compare i1 i2 in
    if as_int > 0 then `Greater else if as_int < 0 then `Less else `Equal
  ;;

qexat

type inhabited = Inhabited

module Hole = struct
  (* Discriminator for Done *)
  type 'ty value = Value of 'ty

  (* Discriminator for Falling *)
  type nonterm = Nonterm

  type 'value t =

qexat

#!/usr/bin/env -S neige run

extend Nat with module
  # This version does not care about a leading zero
  let parse_decimal_digits : String -> List Nat =
    let tailrec string acc =
      match string with
      | "" -> acc
      | ('0' .. '9' as first) :: rest ->
        let digit = Char.code_point_of first - Char.digit_offset in

qexat

# ruff: noqa: S101, PLR6301, RUF002
"""
Cursed implementation of `is_odd`.

It relies on two interesting properties. Firstly, the set formed
by the difference of consecutive squares is the odd members of
ℕ - let's call this set ℕ_odd.
Secondly, the negative integers are symmetric to their positive
counterparts with respect to oddness. Differently put, negating
a number preserves the fact that it is odd.

qexat

(* we start by setting up a global scope.
   `setup` is a special function that handles all we need behind
   the scenes. `$global` is a macro that gets substituted with
   the scope ID from the meta-environment mapping (ID -> scope) *)
$global -> setup ()

(* `let` is an applicative statement that handles intro and
   substitution in the specified scope *)
let($global) n := 3

qexat

public Nat -> type
  | O : Nat
  | S : Nat -> Nat

public successor -> fun (n : Nat) : Nat => S n
public predecessor -> fun (S n : Nat) : Nat => n

public n + m ->
  split n, m into
  | _, O -> n

qexat

{-# LANGUAGE MonoLocalBinds #-}

module Main where

class Relation r a b

class Relation r a a => Reflexivity r a where
  reflexivity :: r a a

class Relation r a b => Symmetry r a b where

qexat

module Ptr = struct
  type 'a t

  external create : 'a -> 'a t = "%makemutable"
  external get_value : 'a t -> 'a = "%field0"
  external of_ref : 'a ref -> 'a t = "%identity"

  let of_int : int -> 'a t = function
    | i -> Obj.magic (i / 2)
  ;;

qexat

module Char = struct
  include Char

  let is_alpha : t -> bool = function
    | 'A' .. 'Z' | 'a' .. 'z' | '_' -> true
    | _ -> false
  ;;

  let is_digit : t -> bool = function
    | '0' .. '9' -> true