module Day1

let var = int

type ty =
  | TyBool
  | TyArrow of ty * ty

type term =
  | EVar of int
  | ETrue
  | EFalse
  | EIfThenElse of term * term * term
  | ELambda of ty * term
  | EApp of term * term

type value =
  | VTrue
  | VFalse
  | VLambda of ty * term

type evalctx =
  | ECDot
  | ECIfThenElse of evalctx * term * term
  | ECAppL of evalctx * term
  | ECAppR of value * evalctx

type step : term -> term -> Type =
  | StepIfTrue : (e1 : term) -> (e2 : term) -> step (EIfThenElse (ETrue, e1, e2)) e1
  | StepIfFalse : (e1 : term) -> (e2 : term) -> step (EIfThenElse (EFalse, e1, e2)) e2

let ctx = var -> option ty
let empty : ctx = fun _ -> None
let extend (t : ty) (g : ctx) : ctx = fun y -> if y = 0 then Some t else g (y - 1)

noeq type typing : ctx -> term -> ty -> Type =
  | TypeTrue : (ctx : ctx) -> typing ctx ETrue TyBool
  | TypeFalse : (ctx : ctx) -> typing ctx EFalse TyBool
  | TypeIfThenElse : (ctx : ctx) -> (ty : ty)
    -> (c : term) -> (e1 : term) -> (e2 : term)
    -> typing ctx c TyBool
    -> typing ctx e1 ty -> typing ctx e2 ty
    -> typing ctx (EIfThenElse (c, e1, e2)) ty

let vRelation (ty : ty) (term : term) : prop =
  match ty, term with
  | (TyBool, ETrue) -> True
  | (TyBool, EFalse) -> True
  | _ -> False

let irred (term : term) : prop = admit()

let rec stepsToInNSteps (e1 : term) (e2 : term) (n : nat) : prop =
  if n = 0 then False
  else exists e' . (stepsToInNSteps e' e2 (n - 1) /\ (step e1 e'))

// let stepsTo (e1 : term) (e2 : term) : prop =


let eRelation (ty : ty) (term : term) : prop =
  exists e' . irred e' /\ vRelation ty e'

let goodRelation (g : ctx) =
  admit()

let subst (#ctx:ctx) (g : goodRelation ctx) (term : term) =
  admit()

// let typeSoundness (ctx : ctx) (term : term) (ty : ty) : prop =
//   forall (e' : )

let semanticSoundness (ctx : ctx) (term : term) (ty : ty) : prop =
  forall (y : goodRelation ctx) . eRelation ty (subst y term)

let fundamentalProperty (#ctx : ctx) (#term : term) (#ty : ty)
  (_ : typing ctx term ty) : semanticSoundness ctx term ty =
  admit()