#r "FSharp.Dependent.dll"
open FSharp.Dependent
open System

let three = Nat<3>.value
let eight = Nat<8>.value

let eleven = three + eight
// let err = three - eight
// error FS0001: internal error: Exception of type 'Microsoft.FSharp.Compiler.ConstraintSolver+LocallyAbortOperationThatFailsToResolveOverload' was thrown.

let xs = 1 ^+ 2 ^+ 3 ^+ 4 ^+ VNil
let ys = Vect.init three id |> Vect.map ((+) 5)

let zs = Vect.append xs ys
zs |> Vect.item Nat<5>.value |> printfn "%i" // 6
// zs |> Vect.item eleven |> printfn "%i"
// error FS0001: internal error: Exception of type 'Microsoft.FSharp.Compiler.ConstraintSolver+LocallyAbortOperationThatFailsToResolveOverload' was thrown.

1 ^+ Vect.empty |> Vect.head |> printfn "%i" // 1
// Vect.empty |> Vect.head |> printfn "%i"
// error FS0001: Type mismatch. Expecting a
//    'Vect<Z,'a> -> 'b'
// but given a
//    'Vect<Z,'c> -> 'c'
// This expression was expected to have type
//    'S<'a>'
// but here has type
//    'Z'

let inline randomLessThan n =
  let rand = Random().Next(0, natVal n - 1)
  rand |> RuntimeNat.LTE <| pred n // existential quantifier simulation

zs |> Vect.item (randomLessThan zs.length) |> printfn "%i"

let inline pleaseGiveMeLessThan limit x =
  Constraint.LTETerm(x, pred limit); // this does nothing in term-level but adds a constraint in type level, here abuses F#'s constraint solver!
  printfn "I'm happy with %i." (natVal x)

zs.length |> pleaseGiveMeLessThan eleven // I'm happy with 7.

let inline winwin x = randomLessThan x |> pleaseGiveMeLessThan x

winwin eight

let (>>=) x f = Option.bind f x
let readNat name =
  printf "%s > " name;
  Console.ReadLine() |> Number.tryParse |> Option.map SomeNat

readNat "input length" >>= mapSomeNat (fun (len: S<SomeNatVariable<"length">>) ->
    let xs = Vect.init len (fun seed -> Random(seed).Next(0,100))
    while true do
      readNat "input index" >>= mapSomeNat (fun (x: RangedNat<Z, SomeNatVariable<"length">>) ->
          xs |> Vect.item x |> printfn "xs[%i] = %i" (natVal x)
        ) |> Option.defaultWith (fun () -> printfn "index is out of range!")
    done
  )