(* Natural Deductions *)
(* Version 1: Valid proof terms have unique type *)
(* Proof checking proceeds bottom-up *)
(* Author: Frank Pfenning *)

signature ND1 =
sig

  (* Proof terms *)
  datatype Term =			(* M ::=          *)
    Var of string			(*      u         *)
  | Pair of Term * Term			(*    | <M1,M2>   *)
  | Fst of Term				(*    | fst M     *)
  | Snd of Term				(*    | snd M     *)
  | Unit				(*    | <>        *)
  | Lam of (string * P.Prop) * Term	(*    | \u:A. M   *)
  | App of Term * Term			(*    | M1 M2     *)
  | Inl of P.Prop * Term		(*    | inl^A M   *)
  | Inr of P.Prop * Term		(*    | inr^A M   *)
  | Case of Term * (string * Term) * (string * Term)
                                        (*    | case M of inl u1 => M1
                                                        | inr u2 => M2 *)
  | Abort of P.Prop * Term		(*    | abort^A M *)

  exception Invalid of string

  (* check (G, M, A) = () if G |- M : A, raises Invalid otherwise *)
  (* syn (G, M) = A       if G |- M : A, raises Invalid if no such A exists *)
  val check : P.Prop C.Ctx * Term * P.Prop -> unit
  val syn : P.Prop C.Ctx * Term -> P.Prop

end;  (* signature ND1 *)

structure ND1 :> ND1 =
struct

  (* Proof terms *)
  datatype Term =			(* M ::=          *)
    Var of string			(*      u         *)
  | Pair of Term * Term			(*    | <M1,M2>   *)
  | Fst of Term				(*    | fst M     *)
  | Snd of Term				(*    | snd M     *)
  | Unit				(*    | <>        *)
  | Lam of (string * P.Prop) * Term	(*    | \u:A. M   *)
  | App of Term * Term			(*    | M1 M2     *)
  | Inl of P.Prop * Term		(*    | inl^A M   *)
  | Inr of P.Prop * Term		(*    | inr^A M   *)
  | Case of Term * (string * Term) * (string * Term)
                                        (*    | case M of inl u1 => M1
                                                        | inr u2 => M2 *)
  | Abort of P.Prop * Term		(*    | abort^A M *)


  exception Invalid of string

  (* check (G, M, A) = () if G |- M : A, raises Invalid otherwise *)
  (* syn (G, M) = A       if G |- M : A, raises Invalid if no such A exists *)
  fun check (G, M, A) =
      if P.eq (syn (G, M), A) then ()
      else raise Invalid("Mismatch between expected and synthesized type")

  and syn (G, Var(u)) =
      (case C.lookup (G, u)
         of SOME(A) => A
          | NONE => raise Invalid("Undeclared variable " ^ u))
    | syn (G, Pair(M1, M2)) = P.And(syn (G, M1), syn (G, M2))
    | syn (G, Fst(M)) =
      (case syn (G, M)
         of P.And(A, B) => A
          | _ => raise Invalid("Argument to Fst not product"))
    | syn (G, Snd(M)) =
      (case syn (G, M)
	 of P.And(A, B) => B
	  | _ => raise Invalid("Argument to Snd not product"))
    | syn (G, Unit) = P.True
    | syn (G, Lam((u, A), M)) = P.Implies(A, syn (C.Decl (G, (u, A)), M))
    | syn (G, App(M1, M2)) =
      (case syn (G, M1)
         of P.Implies(A, B) => (check (G, M2, A); B)
          | _ => raise Invalid("First argument to App not function"))
    | syn (G, Inl(B, M)) = P.Or(syn (G, M), B)
    | syn (G, Inr(A, M)) = P.Or(A, syn (G, M))
    | syn (G, Case(M, (u1, N1), (u2, N2))) =
      (case syn (G, M)
	 of P.Or(A, B) =>
	    let
	      val C1 = syn (C.Decl(G, (u1, A)), N1)
	      val C2 = syn (C.Decl(G, (u2, B)), N2)
	    in
	      if P.eq (C1, C2) then C1
	      else raise Invalid("Branches of Case have different type")
	    end
	  | _ => raise Invalid("First argument to Case not a sum"))
    | syn (G, Abort(C, M)) =
      (case syn (G, M)
	 of P.False => C
          | _ => raise Invalid("Argument to Abort not void"))

end;  (* structure ND1 *)