jake-87

type t =
  | Int of int
  | Name of string
  | Let of string * t * t
  | Add of t * t
  | Ref of t option ref

(* iffy *)
let rec pp i x =
  print_string (String.make i ' ');

jake-87

open import Relation.Binary.PropositionalEquality
open import Data.Nat renaming (ℕ to Nat)
open import Data.Fin hiding (_≤_; _≟_)
open import Data.Empty
open import Data.Unit hiding (_≟_)
open import Data.Sum
open import Data.Vec
open import Data.Product renaming (proj₁ to fst; proj₂ to snd)
open import Relation.Nullary.Negation
open import Data.Bool hiding (_≤_; _≟_)

jake-87

open import Relation.Binary.PropositionalEquality
open import Data.Nat renaming (ℕ to Nat)
open import Data.Fin
open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Vec
open import Data.Product
open import Relation.Nullary.Negation
open import Data.Bool

jake-87

#include <math.h>
#include <stdio.h>
#include <stdlib.h>

#define pi 3.141592653589793
#define solar_mass (4 * pi * pi)
#define days_per_year 365.24

struct planet {
  double x, y, z;

jake-87

open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Data.Bool
open import Relation.Nullary.Negation
open import Data.Sum
open import Data.Empty

postulate LEM : ∀ {ℓ} (A : Set ℓ)  → A ⊎ (¬ A)
postulate funext : ∀ {ℓ} {A B : Set ℓ} {f g : A → B} → (∀ x → f x ≡ g x) → f ≡ g

jake-87

V2:

theory Isabelle_little_compiler
  imports Main
begin

datatype lang = 
  Lit nat
  | Plus lang lang

jake-87

{-# LANGUAGE StrictData, OverloadedStrings #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_GHC -Wno-unused-matches -Wno-unused-top-binds #-}
{-# OPTIONS_GHC -Wno-unused-imports -Wno-name-shadowing #-}
{-# LANGUAGE PartialTypeSignatures #-}
import Data.STRef
import Control.Monad.ST
import Text.Show.Functions
import Control.Monad.Except
import Control.Monad.Trans.Class

jake-87

let rand =
  let x = ref 10 in
  fun () ->
  x := (!x * 27527 + 27791) mod 41231;
  !x

type tree =
  | Leaf
  | Branch of int * tree * tree

jake-87

open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Nat.Properties 
open import Data.Maybe
open import Data.Fin
open import Relation.Nullary.Decidable
open import Data.Product

data Con : ℕ → Set
data Tm : ℕ → Set

jake-87