Formality.fm

// A ideia é que o Formality-Lang compila para o
// Formality-Core para fins de type-checking apenas. O
// Formality-Lang tem coisas tipo ADTs e números, enquanto o
// Formality-Core só tem lambdas e self. Para virar
// JavaScript, a compilação parte do Formality-Lang, de modo
// a poder usar os números e ADTs nele presentes.

import Bits
import IO
import Map
import Nat
import Number
import String
import Unit

// :::::::::::
// :: Utils ::
// :::::::::::

Lazy(A : Type) : Type
  Unit -> A

force(A; x: Lazy(A)) : A
  x(unit)

// ::::::::::
// :: Term ::
// ::::::::::

T Term
| typ
| var(indx: Nat)
| ref(name: String, eras: Bool)
| all(name: String, bind: Term, body: Term, eras: Bool)
| lam(name: String, body: Term, eras: Bool)
| app(func: Term, argm: Term, eras: Bool)
| slf(name: String, type: Term)
| ins(type: Term, expr: Term)
| eli(expr: Term)
| ann(type: Term, expr: Term, done: Bool)

T Def
| def(type: Term, term: Term)

Defs : Type
  Map(Def)

// ::::::::::::::::::
// :: Erased Terms ::
// ::::::::::::::::::

T Eras
| etyp(hash: Number)
| evar(hash: Number, indx: Nat)
| eref(hash: Number, name: String)
| eall(hash: Number, bind: Eras, body: Eras)
| elam(hash: Number, body: Eras)
| eapp(hash: Number, func: Eras, argm: Eras)
| eslf(hash: Number, type: Eras)

hash_of(eras: Eras) : Uint32
  case eras
  | etyp => eras.hash
  | evar => eras.hash
  | eref => eras.hash
  | eall => eras.hash
  | elam => eras.hash
  | eapp => eras.hash
  | eslf => eras.hash

esame(a: Eras, b: Eras) : Bool
  if hash_of(a) === hash_of(b)
  then true
  else false

NUL 0x0 ZER 0x1 SUC 0x2 TYP 0x3
VAR 0x4 REF 0x5 ALL 0x6 LAM 0x7
APP 0x8 SLF 0x9 INS 0xA ELI 0xB
ANN 0xC BTE 0xD BT0 0xE BT1 0xF

hash2(a: Uint32, b: Uint32) : Uint32
  bitmix(a ^ b) >>> 0

hash_nat(n: Nat) : Uint32
  case n
  | zero => hash2(ZER, 0)
  | succ => hash2(SUC, hash_nat(n.pred))

hash_str(str: String) : Uint32
  case str
  | nil  => hash2(ZER, 0)
  | cons => hash2(SUC, hash2(str.head, hash_str(str.tail)))

mk_etyp : Eras
  etyp(hash2(TYP, 0))

mk_evar(indx: Nat) : Eras
  evar(hash2(VAR, hash_nat(indx)), indx)

mk_eref(name: String) : Eras
  eref(hash2(REF, hash_str(name)), name)

mk_eall(bind, body) : Eras
  eall(hash2(ALL, hash2(hash_of(bind), hash_of(body))), bind, body)

mk_elam(body) : Eras
  elam(hash2(LAM, hash_of(body)), body)

mk_eapp(func, argm) : Eras
  eapp(hash2(APP, hash2(hash_of(func), hash_of(argm))), func, argm)

mk_eslf(type) : Eras
  eslf(hash2(SLF, hash_of(type)), type)

erase(term: Term) : Eras
  case term
  | typ => mk_etyp
  | var => mk_evar(term.indx)
  | ref => mk_eref(term.name)
  | all => mk_eall(erase(term.bind), erase(term.body))
  | lam => mk_elam(erase(term.body))
  | app => mk_eapp(erase(term.func), erase(term.argm))
  | slf => mk_eslf(erase(term.type))
  | ins => erase(term.expr)
  | eli => erase(term.expr)
  | ann => erase(term.expr)

// ::::::::::::::::::
// :: Substitution ::
// ::::::::::::::::::

shift(term: Term, inc: Nat, dep: Nat) : Term
  case term
  | typ =>
    typ
  | var =>
    case nat_compare(term.indx, dep) as cmp
    | less_than    => var(term.indx)
    | equal_to     => var(add(inc, term.indx))
    | greater_than => var(add(inc, term.indx))
  | ref =>
    let name = term.name
    let eras = term.eras
    ref(name, eras)
  | all =>
    let name = term.name
    let bind = shift(term.bind, inc, dep)
    let body = shift(term.body, inc, succ(dep))
    let eras = term.eras
    all(name, bind, body, eras)
  | lam =>
    let name = term.name
    let body = shift(term.body, inc, succ(dep))
    let eras = term.eras
    lam(name, body, eras)
  | app =>
    let func = shift(term.func, inc, dep)
    let argm = shift(term.argm, inc, dep)
    let eras = term.eras
    app(func, argm, eras)
  | slf =>
    let name = term.name
    let type = shift(term.type, inc, succ(dep))
    slf(name, type)
  | ins =>
    let type = shift(term.type, inc, dep)
    let expr = shift(term.expr, inc, dep)
    ins(type, expr)
  | eli =>
    let expr = shift(term.expr, inc, dep)
    eli(expr)
  | ann =>
    let type = shift(term.type, inc, dep)
    let expr = shift(term.expr, inc, dep)
    let done = term.done
    ann(type, expr, done)

subst(term: Term, trm: Term, dep: Nat) : Term
  case term
  | typ =>
    typ
  | var =>
    case nat_compare(term.indx, dep) as cmp
    | less_than    => var(term.indx)
    | equal_to     => trm
    | greater_than => var(pred(term.indx))
  | ref =>
    let name = term.name
    let eras = term.eras
    ref(name, eras)
  | all =>
    let name = term.name
    let bind = subst(term.bind, trm, dep)
    let body = subst(term.body, shift(trm,1n,0n), succ(dep))
    let eras = term.eras
    all(name, bind, body, eras)
  | lam =>
    let name = term.name
    let body = subst(term.body, shift(trm,1n,0n), succ(dep))
    let eras = term.eras
    lam(name, body, eras)
  | app =>
    let func = subst(term.func, trm, dep)
    let argm = subst(term.argm, trm, dep)
    let eras = term.eras
    app(func, argm, eras)
  | slf =>
    let name = term.name
    let type = subst(term.type, shift(trm,1n,0n), succ(dep))
    slf(name, type)
  | ins =>
    let type = subst(term.type, trm, dep)
    let expr = subst(term.expr, trm, dep)
    ins(type, expr)
  | eli =>
    let expr = subst(term.expr, trm, dep)
    eli(expr)
  | ann =>
    let type = subst(term.type, trm, dep)
    let expr = subst(term.expr, trm, dep)
    let done = term.done
    ann(type, expr, done)

subst_many(term: Term, vals: List(Term), inc: Nat, dep: Nat) : Term
  case vals
  | nil =>
    term
  | cons =>
    let sval = shift(vals.head, inc, 0n)
    let sdep = add(dep, inc)
    let term = subst(term, sval, sdep)
    subst_many(term, vals.tail, pred(inc), dep)

// :::::::::::::::::::
// :: Normalization ::
// :::::::::::::::::::

T Hoas
| xtyp
| xvar(indx: Nat)
| xref(name: String, eras: Bool)
| xall(name: String, bind: Hoas, body: Hoas -> Hoas, eras: Bool)
| xlam(name: String, body: Hoas -> Hoas, eras: Bool)
| xapp(func: Hoas, argm: Hoas, eras: Bool)
| xslf(name: String, type: Hoas -> Hoas)
| xins(type: Hoas, expr: Hoas)
| xeli(expr: Hoas)
| xann(type: Hoas, expr: Hoas, done: Bool)

term_to_hoas(term: Term, vals: List(Hoas)) : Hoas
  case term
  | typ =>
    xtyp
  | var =>
    case at(Hoas; term.indx, vals) as got
    | none => xvar(term.indx)
    | some => got.value
  | ref =>
    let name = term.name
    let eras = term.eras
    xref(name, eras)
  | all =>
    let name = term.name
    let bind = term_to_hoas(term.bind, vals)
    let body = (x) => term_to_hoas(term.body,cons(_ x,vals))
    let eras = term.eras
    xall(name, bind, body, eras)
  | lam =>
    let name = term.name
    let body = (x) => term_to_hoas(term.body,cons(_ x,vals))
    let eras = term.eras
    xlam(name, body, eras)
  | app =>
    let func = term_to_hoas(term.func, vals)
    let argm = term_to_hoas(term.argm, vals)
    let eras = term.eras
    xapp(func, argm, eras)
  | slf =>
    let name = term.name
    let type = (x) => term_to_hoas(term.type, cons(_ x, vals))
    xslf(name, type)
  | ins =>
    let type = term_to_hoas(term.type, vals)
    let expr = term_to_hoas(term.expr, vals)
    xins(type, expr)
  | eli =>
    let expr = term_to_hoas(term.expr, vals)
    xeli(expr)
  | ann =>
    let type = term_to_hoas(term.type, vals)
    let expr = term_to_hoas(term.expr, vals)
    let done = term.done
    xann(type, expr, done)

hoas_to_term(term: Hoas, depth: Nat) : Term
  case term
  | xtyp =>
    typ
  | xvar =>
    case nat_compare(term.indx, depth) as cmp
    | less_than    => var(sub(depth, succ(term.indx)))
    | equal_to     => var(term.indx)
    | greater_than => var(term.indx)
  | xref =>
    let name = term.name
    let eras = term.eras
    ref(name, eras)
  | xall =>
    let name = term.name
    let bind = hoas_to_term(term.bind, depth)
    let body = hoas_to_term(term.body(xvar(depth)), succ(depth))
    let eras = term.eras
    all(name, bind, body, eras)
  | xlam =>
    let name = term.name
    let body = hoas_to_term(term.body(xvar(depth)), succ(depth))
    let eras = term.eras
    lam(name, body, eras)
  | xapp =>
    let func = hoas_to_term(term.func, depth)
    let argm = hoas_to_term(term.argm, depth)
    let eras = term.eras
    app(func, argm, eras)
  | xslf =>
    let name = term.name
    let type = hoas_to_term(term.type(xvar(depth)), succ(depth))
    slf(name, type)
  | xins =>
    let type = hoas_to_term(term.type, depth)
    let expr = hoas_to_term(term.expr, depth)
    ins(type, expr)
  | xeli =>
    let expr = hoas_to_term(term.expr, depth)
    eli(expr)
  | xann =>
    let type = hoas_to_term(term.type, depth)
    let expr = hoas_to_term(term.expr, depth)
    let done = term.done
    ann(type, expr, done)

normalize(term: Hoas, defs: Defs) : Hoas
  case term
  | xtyp =>
    xtyp
  | xvar =>
    xvar(term.indx)
  | xref =>
    let name = term.name
    let eras = term.eras
    case lookup(_ string_to_bits(name), defs) as got
    | none => xref(name, eras)
    | some => case got.value |def
      term_to_hoas(got.value.term, [])
  | xall =>
    let name = term.name
    let bind = normalize(term.bind, defs)
    let body = (x) => normalize(term.body(x), defs)
    let eras = term.eras
    xall(name, bind, body, eras)
  | xlam =>
    let name = term.name
    let body = (x) => normalize(term.body(x), defs)
    let eras = term.eras
    xlam(name, body, eras)
  | xapp =>
    case unit with normalize(term.func, defs) as func : Hoas |unit
    case func
    with term.argm : Hoas
    with term.eras : Bool
    | xtyp => xapp(func, normalize(term.argm, defs), term.eras)
    | xvar => xapp(func, normalize(term.argm, defs), term.eras)
    | xref => xapp(func, normalize(term.argm, defs), term.eras)
    | xall => xapp(func, normalize(term.argm, defs), term.eras)
    | xlam => normalize(func.body(term.argm), defs)
    | xapp => xapp(func, normalize(term.argm, defs), term.eras)
    | xslf => xapp(func, normalize(term.argm, defs), term.eras)
    | xins => xapp(func, normalize(term.argm, defs), term.eras)
    | xeli => xapp(func, normalize(term.argm, defs), term.eras)
    | xann => xapp(func, normalize(term.argm, defs), term.eras)
  | xslf =>
    let name = term.name
    let type = (x) => normalize(term.type(x), defs)
    xslf(name, type)
  | xins =>
    let type = normalize(term.type, defs)
    let expr = normalize(term.expr, defs)
    xins(type, expr)
  | xeli =>
    case unit with normalize(term.expr, defs) as expr : Hoas |unit
    case expr
    | xtyp => xeli(expr)
    | xvar => xeli(expr)
    | xref => xeli(expr)
    | xall => xeli(expr)
    | xlam => xeli(expr)
    | xapp => xeli(expr)
    | xslf => xeli(expr)
    | xins => xeli(expr)
    | xeli => expr
    | xann => xeli(expr)
  | xann =>
    let type = normalize(term.type, defs)
    let expr = normalize(term.expr, defs)
    let done = term.done
    xann(type, expr, done)

reduce(term: Term, defs: Defs) : Term
  hoas_to_term(normalize(term_to_hoas(term, []), defs), 0n)

// :::::::::::::::::
// :: Stringifier ::
// :::::::::::::::::

show.go(term: Term, names: List(String)) : Concat(Char)
  case term
  | typ =>
    let type = list_to_concat(Char; "Type")
    (x) => type(x)
  | var =>
    (x) => case at(String; term.indx, names) as got
      | none =>
        let numb = nat_to_number(term.indx)
        let str0 = list_to_concat(Char; "#")
        let str1 = list_to_concat(Char; number_to_string(10, numb))
        str0(str1(x))
      | some =>
        list_to_concat(Char; got.value, x)
  | ref =>
    let name = list_to_concat(Char; term.name)
    (x) => name(x)
  | all =>
    let pun0 = list_to_concat(Char; "(")
    let name = list_to_concat(Char; term.name)
    let pun1 = list_to_concat(Char; " : ")
    let bind = show.go(term.bind, names)
    let pun2 = list_to_concat(Char; ") -> ")
    let body = show.go(term.body, cons(String; term.name, names))
    (x) => pun0(name(pun1(bind(pun2(body(x))))))
  | lam =>
    let pun0 = list_to_concat(Char; "(")
    let name = list_to_concat(Char; term.name)
    let pun1 = list_to_concat(Char; ") => ")
    let body = show.go(term.body, cons(String; term.name, names))
    (x) => pun0(name(pun1(body(x))))
  | app =>
    let pun0 = list_to_concat(Char; "(")
    let func = show.go(term.func, names)
    let pun1 = list_to_concat(Char; ")(")
    let argm = show.go(term.argm, names)
    let pun2 = list_to_concat(Char; ")")
    (x) => pun0(func(pun1(argm(pun2(x)))))
  | slf =>
    let pun0 = list_to_concat(Char; "type{")
    let name = list_to_concat(Char; term.name)
    let pun1 = list_to_concat(Char; "} ")
    //let type = show.go(term.type, names)
    let type = show.go(term.type, cons(String; term.name, names))
    (x) => pun0(name(pun1(type(x))))
  | ins =>
    let pun0 = list_to_concat(Char; "inst{")
    let type = show.go(term.type, names)
    let pun1 = list_to_concat(Char; "}");
    let expr = show.go(term.expr, names)
    (x) => pun0(type(pun1(expr(x))))
  | eli =>
    let pun0 = list_to_concat(Char; "elim{")
    let expr = show.go(term.expr, names)
    let pun1 = list_to_concat(Char; "}")
    (x) => pun0(expr(pun1(x)))
  | ann =>
    let type = show.go(term.type, names)
    let pun0 = list_to_concat(Char; " :: ")
    let expr = show.go(term.expr, names)
    (x) => type(pun0(expr(x)))
  : Concat(Char)
  
show(term: Term) : String
  show.go(term, [], [])

//show_defs.go(defs: Defs) : String
  //let els = map_elements(_ defs)
  //let cons = (term, str) =>
    //let name = list_to_concat(Char; show(head))
    //let 
  //fold(Def; String; 
  //| none => nil(_)
  //| some => 
  //case defs
  //| none => nil(_)
  //| some => case 
  
// ::::::::::::
// :: Parser ::
// ::::::::::::

// The parser below would be prettier with monads, but it
// avoids that in order to increase performance to the
// theoretical maximum, and decrease the dependency.

Parsed : Type
  Maybe(Pair(String, Term))

Vars : Type
  List(String)

// If `b` is successful, return it. Otherwise, try `a`.
try(a: Lazy(Parsed), b: Parsed) : Parsed
  case b
  with unit : Unit
  |none case force(_ a) as a
    |none none(_)
    |some some(_ a.value)
  |some some(_ b.value)

// Drops some characters from code
drop(amount: Nat, code: String) : String
  case amount |zero code |succ
  case code   |nil  code |cons
  drop(amount.pred, code.tail)

// Is this character allowed in names?
is_name_char(chr: Char) : Number
  ((chr > 47) && (chr < 58))  || // 0-9
  ((chr > 64) && (chr < 91))  || // A-Z 
  ((chr > 96) && (chr < 123)) || // a-z
  (chr === 95)                   // _ 

// Is this character a space?
is_space_char(chr: Char) : Number
  (chr === ' ') || (chr === 10)

// Removes leadig spaces
skip_spaces(code: String) : String
  case code |nil nil(_) |cons
  if is_space_char(code.head) then
    skip_spaces(code.tail)
  else
    code

// Are there non-space characters on this line?
line_has_chars(code: String) : Number
  case code |nil 0 |cons
  if (code.head === ' ') then
    line_has_chars(code.tail)
  else if (code.head === 10) then
    0
  else
    1

// Matches an exact string, returns the remaining code
consume(value: String, code: String) : Maybe(String)
  let code = skip_spaces(code)
  case value |nil some(_ code) |cons
  case code  |nil none(_)      |cons
  if code.head === value.head then
    consume(value.tail, code.tail)
  else
    none(_)

// Parses name characters
parse_name.go(code: String) : Pair(String, String)
  case code |nil #[code, nil(_)] |cons
  if is_name_char(code.head) then
    get #[code, name] = parse_name.go(code.tail)
    #[code, cons(Char; code.head, name)]
  else
    #[code, nil(Char;)]

parse_name(code: String) : Pair(String, String)
  parse_name.go(skip_spaces(code))

// Parses a grouping `(...)`
parse_grp(code: String, vars: Vars) : Parsed
  // Parses `(`
  case consume("(",code) as got
  |none => none(_)
  |some => let code = got.value

  // Parses term
  case parse_term(code,vars) as got
  |none => none(_)
  |some => get #[code,term] = got.value

  // Parses `)`
  case consume(")",code) as got
  |none => none(_)
  |some => let code = got.value

  some(_ pair(__ code, term))

// Parses `(x:A)->B`
parse_all(code: String, vars: Vars) : Parsed
  // Parses `(`
  case consume("(",code) as got
  |none => none(_)
  |some => let code = got.value

  // Parses variable name
  get #[code, name] = parse_name(code)

  // Parses `:`
  case consume(":",code) as got
  |none => none(_)
  |some => let code = got.value

  // Parses variable type
  case parse_term(code, vars) as got
  |none => none(_)
  |some => get #[code, type] = got.value

  // Parses erasure
  get #[code,eras] =
    case consume(";",code) as got
    |none => #[code, false]
    |some => #[got.value, true]

  // Parses `)`
  case consume(")",code) as got
  |none => none(_)
  |some => let code = got.value

  // Parses `->`
  case consume("->",code) as got
  |none => none(_)
  |some => let code = got.value

  // Parses body
  case parse_term(code, cons(_ name, vars)) as got
  |none => none(_)
  |some => get #[code, body] = got.value

  // Result
  some(_ pair(__ code, all(name, type, body, eras)))

// Parses `(x:A)=>B`
parse_lam(code: String, vars: Vars) : Parsed
  // Parses `(`
  case consume("(",code) as got
  |none => none(_)
  |some => let code = got.value

  // Parses variable name
  get #[code, name] = parse_name(code)

  // Parses erasure
  get #[code,eras] =
    case consume(";",code) as got
    |none => #[code, false]
    |some => #[got.value, true]

  // Parses `)`
  case consume(")",code) as got
  |none => none(_)
  |some => let code = got.value

  // Parses `->`
  case consume("=>",code) as got
  |none => none(_)
  |some => let code = got.value

  // Parses body
  case parse_term(code, cons(_ name, vars)) as got
  |none => none(_)
  |some => get #[code, body] = got.value

  // Result
  some(_ pair(__ code, lam(name, body, eras)))

// Parses `Type`
parse_typ(code: String, vars: Vars) : Parsed
  case consume("Type",code) as got
  |none => none(_)
  |some => some(_ pair(__ got.value, typ))

// Parses variables
parse_var(code: String, vars: Vars) : Parsed
  get #[code,name] = parse_name(code)
  case find_index(_ string.equal(name), vars) as found
  |none =>
    case name |nil none(_) |cons
    some(_ pair(__ code, ref(name, false)))
  |some =>
    some(_ pair(__ code, var(found.value)))

// Parses a self type
parse_slf(code: String, vars: Vars) : Parsed
  case consume("type{",code) as got
  |none => none(_)
  |some => let code = got.value

  get #[code,name] = parse_name(code)

  case consume("}",code) as got
  |none => none(_)
  |some => let code = got.value

  case parse_term(code, cons(_ name, vars)) as got
  |none => none(_)
  |some => get #[code,body] = got.value

  some(_ pair(__ code, slf(name, body)))

// Parses a self instantiation
parse_ins(code: String, vars: Vars) : Parsed
  case consume("inst{",code) as got
  |none => none(_)
  |some => let code = got.value

  case parse_term(code,vars) as got
  |none => none(_)
  |some => get #[code,type] = got.value

  case consume("}",code) as got
  |none => none(_)
  |some => let code = got.value

  case parse_term(code,vars) as got
  |none => none(_)
  |some => get #[code,expr] = got.value 

  some(_ pair(__ code, ins(type, expr)))

// Parses a self elimination
parse_eli(code: String, vars: Vars) : Parsed
  case consume("elim{",code) as got
  |none => none(_)
  |some => let code = got.value

  case parse_term(code,vars) as got
  |none => none(_)
  |some => get #[code,expr] = got.value

  some(_ pair(__ code, eli(expr)))

// Parses application
parse_app(code: String, func: Term, vars: Vars) : Parsed
  // Parses `(`
  case consume("(",code) as got
  |none => none(_)
  |some => let code = got.value

  // Parses argument
  case parse_term(code, vars) as got
  |none => none(_)
  |some => get #[code,argm] = got.value

  // Parses `)`
  case consume(")",code) as got
  |none => none(_)
  |some => let code = got.value

  some(_ pair(__ code, app(func, argm, false)))

// Postfix parses
// Attempts each one repeatedly, until all fail
parse_postfix(code: String, term: Term, vars: Vars) : Parsed
  if line_has_chars(code) then
    let parsed = none(_)
    let parsed = try((x)=>parse_app(code, term, vars), parsed)
    case parsed
    |none some(_ pair(__ code, term))
    |some get #[code,term] = parsed.value
    parse_postfix(code, term, vars)
  else
    some(_ pair(__ code, term))

// Parses terms
parse_term(code: String, vars: Vars) : Parsed
  let parsed = none(_)
  let parsed = try((x)=>parse_all(code, vars), parsed)
  let parsed = try((x)=>parse_lam(code, vars), parsed)
  let parsed = try((x)=>parse_grp(code, vars), parsed)
  let parsed = try((x)=>parse_typ(code, vars), parsed)
  let parsed = try((x)=>parse_slf(code, vars), parsed)
  let parsed = try((x)=>parse_ins(code, vars), parsed)
  let parsed = try((x)=>parse_eli(code, vars), parsed)
  let parsed = try((x)=>parse_var(code, vars), parsed)
  case parsed |none none(_) |some
  get #[code, term] = parsed.value
  parse_postfix(code, term, vars)

// Parses a term, drops leftover code
parsed_term(code: String) : Maybe(Term)
  case parse_term(code, []) as parsed
  | none => none(_)
  | some => case parsed.value |pair some(_ parsed.value.snd)

// Parses defs
parse_defs.go(code: String, defs: Defs) : Defs
  get #[code,name] = parse_name(code)
  case name
  with defs : Defs
  | nil  => defs
  | cons =>
    let name = cons(_ name.head, name.tail)
    case consume(":",code) as got
    with defs : Defs
    |none => defs
    |some => let code = got.value
    case parse_term(code, []) as got
    with defs : Defs
    |none => defs
    |some => get #[code,type] = got.value
    case parse_term(code, []) as got
    with defs : Defs
    |none => defs
    |some => get #[code,term] = got.value
    let bits = string_to_bits(name)
    let defs = insert(_ bits, def(type,term), defs)
    parse_defs.go(code, defs)

// Parses defs
parse_defs(code: String) : Defs
  parse_defs.go(code, empty(_))

// ::::::::::::::
// :: Equality ::
// ::::::::::::::

identical(a: Term, b: Term) : Bool
  case a
  | typ =>
    case b
    | typ => true
    | var => false
    | ref => false
    | all => false
    | lam => false
    | app => false
    | slf => false
    | ins => false
    | eli => false
    | ann => false
  | var =>
    case b
    | typ => false
    | var => nat_equal(a.indx, b.indx) 
    | ref => false
    | all => false
    | lam => false
    | app => false
    | slf => false
    | ins => false
    | eli => false
    | ann => false
  | ref =>
    case b
    | typ => false
    | var => false
    | ref => string_equal(a.name,b.name)
    | all => false
    | lam => false
    | app => false
    | slf => false
    | ins => false
    | eli => false
    | ann => false
  | all =>
    case b
    | typ => false
    | var => false
    | ref => false
    | all => and(equal(a.bind,b.bind),equal(a.body,b.body))
    | lam => false
    | app => false
    | slf => false
    | ins => false
    | eli => false
    | ann => false
  | lam =>
    case b
    | typ => false
    | var => false
    | ref => false
    | all => false
    | lam => and(equal(a.body,b.body))
    | app => false
    | slf => false
    | ins => false
    | eli => false
    | ann => false
  | app =>
    case b
    | typ => false
    | var => false
    | ref => false
    | all => false
    | lam => false
    | app => and(equal(a.func,b.func),equal(a.argm,b.argm))
    | slf => false
    | ins => false
    | eli => false
    | ann => false
  | slf =>
    case b
    | typ => false
    | var => false
    | ref => false
    | all => false
    | lam => false
    | app => false
    | slf => equal(a.type,b.type)
    | ins => false
    | eli => false
    | ann => false
  | ins =>
    case b
    | typ => false
    | var => false
    | ref => false
    | all => false
    | lam => false
    | app => false
    | slf => false
    | ins => and(equal(a.type,b.type),equal(a.expr,b.expr))
    | eli => false
    | ann => false
  | eli =>
    case b
    | typ => false
    | var => false
    | ref => false
    | all => false
    | lam => false
    | app => false
    | slf => false
    | ins => false
    | eli => equal(a.expr,b.expr)
    | ann => false
  | ann =>
    case b
    | typ => false
    | var => false
    | ref => false
    | all => false
    | lam => false
    | app => false
    | slf => false
    | ins => false
    | eli => false
    | ann => equal(a.expr,b.expr)
  
// :::::::::::::::::::
// :: Type-Checking ::
// :::::::::::::::::::

Context : Type
  List(Term)

ctx.get(ctx: Context, i: Nat) : Maybe(Term)
  case at(_ i, ctx) as got
  | none => none(_) 
  | some => some(_ shift(got.value, succ(i), 0n))

ctx.nil : Context
  nil(_)

ctx.ext(ctx: Context, term: Term) : Context
  cons(_ term, ctx)

// Type-checks a term
typecheck(
  term : Term,
  type : Maybe(Term),
  defs : Defs,
  ctx  : Context
) : Maybe(Term)
  // TODO: weak reduce intead
  let type = case type
    | none => none(_)
    | some => some(_ reduce(type.value,defs))

  // Pattern matches term
  case term

  // Type of Types
  | typ =>
    some(_ typ)

  // Variables
  | var =>
    ctx.get(ctx, term.indx)

  // Reference
  | ref => 
    case lookup(_ string_to_bits(term.name), defs) as got
    | none =>
      none(_)
    | some =>
      case got.value
      | def => some(_ got.value.type)

  // Function Type (Universal Quantification)
  | all =>
    let bind_chk = typecheck(term.bind, some(_ typ), defs, ctx)
    let ext_ctx  = ctx.ext(ctx, term.bind)
    let body_chk = typecheck(term.body, some(_ typ), defs, ext_ctx)
    case bind_chk
    | none =>
      none(_)
    | some =>
      let bind_typ = bind_chk.value
      case body_chk
      | none =>
        none(_)
      | some =>
        let body_typ = body_chk.value
        some(_ typ)

  // Function Value (Lambda)
  | lam =>
    case type
    | none => none(_)
    | some => case type.value as type
    | typ => none(_)
    | var => none(_)
    | ref => none(_)
    | all =>
      let ext_ctx = ctx.ext(ctx, type.bind)
      let body_chk = typecheck(term.body, some(_ type.body), defs, ext_ctx)
      case body_chk
      | none =>
        none(_)
      | some =>
        let body_typ = body_chk.value
        let term_typ = all(term.name, type.bind, body_typ, term.eras)
        some(_ term_typ)
    | lam => none(_)
    | app => none(_)
    | slf => none(_)
    | ins => none(_)
    | eli => none(_)
    | ann => none(_)

  // Function Elimination (application)
  | app =>
    let func_chk = typecheck(term.func, none(_), defs, ctx)
    case func_chk
    | none => none(_)
    | some =>
      let func_typ = func_chk.value
      case func_typ
      | typ => none(_)
      | var => none(_)
      | ref => none(_)
      | all =>
        let argm_chk = typecheck(term.argm, some(_ func_typ.bind), defs, ctx)
        case argm_chk
        | none => none(_)
        | some =>
          let argm_typ = argm_chk.value
          let term_typ = subst(func_typ.body, term.argm, 0n)
          some(_ term_typ)
      | lam => none(_)
      | app => none(_)
      | slf => none(_)
      | ins => none(_)
      | eli => none(_)
      | ann => none(_)

  // Self Type
  | slf =>
    let ex_ctx = ctx.ext(ctx, term)
    let type_chk = typecheck(term.type, some(_ typ), defs, ex_ctx)
    case type_chk
    | none =>
      none(_)
    | some =>
      some(_ typ)

  // Self Value
  | ins =>
    case term.type
    | typ => none(_)
    | var => none(_)
    | ref => none(_)
    | all => none(_)
    | lam => none(_)
    | app => none(_)
    | slf =>
      let self_typ = subst(term.type.type, ann(term.type, term, true), 0n)
      let expr_chk = typecheck(term.expr, some(_ self_typ), defs, ctx)
      case expr_chk
      | none =>
        none(_)
      | some =>
        some(_ term.type)
    | ins => none(_)
    | eli => none(_)
    | ann => none(_)

  // Self Elimination
  | eli =>
    let expr_chk = typecheck(term.expr, none(_), defs, ctx)
    case expr_chk
    | none =>
      none(_)
    | some => 
      case expr_chk.value as expr_t
      | typ => none(_)
      | var => none(_)
      | ref => none(_)
      | all => none(_)
      | lam => none(_)
      | app => none(_)
      | slf => some(_ subst(expr_t.type, term.expr, 0n))
      | ins => none(_)
      | eli => none(_)
      | ann => none(_)

  // Annotation
  | ann => some(_ term.type)

// ::::::::::
// :: Test ::
// ::::::::::

main
  let defs = parse_defs("
    Nat : Type
      (A: Type) -> (z : A) -> (s : (x:A) -> A) -> A
      
    zero : (A: Type) -> (z : A) -> (s : (x:A) -> A) -> A
      (A) => (z) => (s) => z

    succ : (n : Nat) -> Nat
      (n) => (A) => (z) => (s) => s(n(A)(z)(s))

    mul : (a : Nat) -> (b : Nat) -> Nat
      (a) => (b) => (A) => (z) => (s) => a(A)(z)((x) => b(A)(x)(s))

    main : Nat
      mul(succ(succ(zero)))(succ(succ(zero)))
  ")

  case lookup(_ string_to_bits("main"), defs) as got
  | none => print("Def not found.")
  | some => case got.value |def do {
    let type = got.value.type
    let term = got.value.term

    case typecheck(term, some(_ type), defs, []) as term_t
    | none => do {
      print("Type error.")
      print(show(term))
      print(show(reduce(term,defs)))
    }
    | some => do {
      print("[Term]")
      print(show(term))
      print("")
      print("[Norm]")
      print(show(reduce(term,defs)))
      print("")
      print("[Type]")
      print(show(term_t.value))
    }
  }