bishabosha

//> using scala "3.3.0"

import scala.util.boundary, boundary.break

object Loops:

  type ExitToken = Unit { type Exit }
  type ContinueToken = Unit { type Continue }

  type Exit = boundary.Label[ExitToken]

aradarbel10

{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# HLINT ignore "Use list comprehension" #-}

import Data.IORef ( IORef, newIORef, readIORef, writeIORef )
import GHC.IO ( unsafePerformIO )
import Control.Applicative ( Alternative(..) )
import Control.Monad ( when )
import Debug.Trace

aradarbel10

(* language definition *)
type nom = string
type bop = Add | Sub | Mul

type typ =
| Int | Arrow of typ * typ | Meta of meta
and meta = meta_state ref
and meta_state =
| Solved of typ
| Unsolved of nom (* keep name for pretty printing *)

AndrasKovacs

{-# language BlockArguments, LambdaCase, Strict, UnicodeSyntax #-}

{-|
Minimal dependent lambda caluclus with:
  - HOAS-only representation
  - Lossless printing
  - Bidirectional checking
  - Efficient evaluation & conversion checking

Inspired by https://gist.github.com/Hirrolot/27e6b02a051df333811a23b97c375196

AndrasKovacs

{-# OPTIONS --prop --without-K --show-irrelevant --safe #-}

{-
Challenge:
- Define a deeply embedded faithfully represented syntax of a dependently typed
  TT in Agda.
- Use an Agda fragment which has canonicity. This means that the combination of
  indexed inductive types & cubical equality is not allowed!
- Prove consistency.

zehnpaard

module D = Effect.Deep

type 'a expr = ..
type _ Effect.t += Extension : 'a expr -> 'a Effect.t

(* Base Interpreter *)
type 'a expr +=
| Int : int -> int expr
| Add : int expr * int expr -> int expr
| Sub : int expr * int expr -> int expr

hirrolot

module type Form = sig
  type ('env, 'a) meaning

  val vz : ('a * 'env, 'a) meaning
  val vs : ('env, 'a) meaning -> ('b * 'env, 'a) meaning
  val lam : ('a * 'env, 'b) meaning -> ('env, 'a -> 'b) meaning

  val appl :
    ('env, 'a -> 'b) meaning -> ('env, 'a) meaning -> ('env, 'b) meaning
end

hirrolot

module type Form = sig
  type 'a meaning

  val lam : ('a meaning -> 'b meaning) -> ('a -> 'b) meaning
  val appl : ('a -> 'b) meaning -> 'a meaning -> 'b meaning
end

(* Evaluate a given term. *)
module Eval = struct
  type 'a meaning = 'a

hirrolot

let rec eval = function
  | `Appl (m, n) -> (
      let n' = eval n in
      match eval m with `Lam f -> eval (f n') | m' -> `Appl (m', n'))
  | (`Lam _ | `Var _) as t -> t

let sprintf = Printf.sprintf

(* Print a given term using De Bruijn levels. *)
let rec pp lvl = function

RiscInside

-- One argument operations with strict evaluation strategy
inductive UnOp : Type :=
  | ufst                                     : UnOp -- first element of the pair
  | usnd                                     : UnOp -- second element of the pair
  | umkl                                     : UnOp -- left constructor of either type
  | umkr                                     : UnOp -- right constructor of either type
  deriving DecidableEq

open UnOp