// https://www.fstar-lang.org/tutorial/book/part2/part2_stlc.html

module Hello

open FStar.Exn

type monotype =
  | MTVar of string
  | MTArrow of monotype * monotype
  | MTEmpty
  | MTUnit
  | MTSum of monotype * monotype
  | MTProd of monotype * monotype
  | MTInductive of string * monotype

type polytype =
  | Mono of monotype
  | Forall of string * polytype

type expr =
  | EVar of string
  | EPoly of string * expr
  | ETypeSub
  | ELam of string * monotype * expr
  | EApp of expr * expr
  | EAbort of expr
  | EInl of expr
  | EInr of expr
  | ECase of expr * (string * expr) * (string * expr)
  | EUnit
  | EPair of expr * expr
  | EFst of expr
  | ESnd of expr
  | ERoll of string * monotype * expr
  | EFold of (string * monotype) * monotype * (expr * string * expr)

let rec appearsIn
  (a : string)
  (mono : monotype)
  : prop
=
  match mono with
  | MTEmpty -> False
  | MTUnit -> False
  | MTVar b -> if a = b then True else False
  | MTProd (left, right) -> appearsIn a left \/ appearsIn a right
  | MTSum (left, right) -> appearsIn a left \/ appearsIn a right
  | MTArrow (left, right) -> appearsIn a left \/ appearsIn a right
  | MTInductive (b, t) -> if a = b then False else appearsIn a t

let rec strictlyPositive
  (a : string)
  (mono : monotype)
  : prop
=
  match mono with
  | MTEmpty -> True
  | MTUnit -> True
  | MTVar b -> True
  | MTProd (left, right) -> strictlyPositive a left /\ strictlyPositive a right
  | MTSum (left, right) -> strictlyPositive a left /\ strictlyPositive a right
  | MTArrow (t1, t2) -> ~(appearsIn a t1) /\ strictlyPositive a t2
  | MTInductive (_, t) -> strictlyPositive a t

exception InductiveCase

let rec logNoInductive
  (mono : monotype)
  (a : string)
  : Exn monotype (requires True) (ensures (fun _ -> True))
=
  match mono with
  | MTEmpty -> MTEmpty
  | MTUnit -> MTEmpty
  | MTVar a' -> if a' = a then MTUnit else MTEmpty
  | MTArrow (t1, t2) -> MTProd (t1, logNoInductive t2 a)
  | MTProd (left, right) -> MTSum (logNoInductive left a, logNoInductive right a)
  | MTSum (left, right) -> MTSum (logNoInductive left a, logNoInductive right a)
  | MTInductive (_, _) -> raise InductiveCase

let rec isVal
  (e : expr)
  : prop
=
  match e with
  | EPoly (_, _) -> True
  | ELam (_, _, _) -> True
  | EInl e' -> isVal e'
  | EInr e' -> isVal e'
  | EUnit -> True
  | EPair (e1, e2) -> isVal e1 /\ isVal e2
  | ERoll (_, _, e') -> isVal e'
  | _ -> False

  // | EVar _ -> True
  // | ETypeSub -> True
  // | EApp (_, _) -> True
  // | EAbort _ -> True
  // | ECase (_, _, _) -> True
  // | EFst _ -> True
  // | ESnd _ -> True
  // | EFold (_, _, _) -> True