happyfellow-one

import Mathlib

inductive Operation | add | sub | mul | div
  deriving DecidableEq

def Operation.parse (input : String) : Option Operation :=
  match input with
  | "+" => .some .add | "-" => .some .sub
  | "*" => .some .mul | "/" => .some .div
  | _ => .none

happyfellow-one

def calc_rpn (program : List String) (stack : List Int) : List Int :=
  match program, stack with
  | "+" :: rest, op1 :: op2 :: stack => calc_rpn rest ((op2 + op1) :: stack)
  | "-" :: rest, op1 :: op2 :: stack => calc_rpn rest ((op2 - op1) :: stack)
  | "*" :: rest, op1 :: op2 :: stack => calc_rpn rest ((op2 * op1) :: stack)
  | "/" :: rest, op1 :: op2 :: stack => calc_rpn rest ((op2 / op1) :: stack)
  | another :: rest, stack => calc_rpn rest (another.toNat! :: stack)
  | [], stack => stack

def rpn (program : String) : Option Int :=

happyfellow-one

open Core

(* First version: the type of diffs is a function from an enumeration
   of all record fields to a potential difference. It's a GADT type,
   which allows us to return correclty typed results.

   All thanks to ppx_typed_fields! *)

type order = {
  id: int;

happyfellow-one

type order = {
  id: int;
  name: string;
  price: int;
  is_quote: bool;
  items: string list;
}

type 'a diff = Same | Different of { left: 'a; right: 'a }

happyfellow-one

open Core

type ('result, 'input, 'output) gen =
  | Done of 'result
  | Input of ('input -> ('result, 'input, 'output) gen)
  | Output of ('output * ('result, 'input, 'output) gen)

let rec gen_bind x f =
  match x with
  | Done x -> f x