(* Natural Deductions *)
(* Version 1: Compact representation *)
(* Proof checking alternates bottom-up and top-down *)
(* Author: Frank Pfenning *)

signature ND2 =
sig

  (* Annotated proof terms *)
  (* Divided into introduction and elimination forms *)
  (* Note the special status of Case and Abort *)

  datatype ITerm =			(* I ::=        *)
    Pair of ITerm * ITerm		(*      <I1,I2> *)
  | Unit				(*    | <>      *)
  | Lam of string * ITerm		(*    | \u. I   *)
  | Inl of ITerm			(*    | inl I   *)
  | Inr of ITerm			(*    | inr I   *)
  | Case of ETerm * (string * ITerm) * (string * ITerm)
					(*    | case E of inl u1 => I1
                                                        | inr u2 => I2 *)
  | Abort of ETerm			(*    | abort E *)
  | Elim of ETerm			(*    | E       *)
  and ETerm =				(* E ::=        *)
    Var of string			(*      u       *)
  | Fst of ETerm			(*    | fst E   *)
  | Snd of ETerm			(*    | snd E   *)
  | App of ETerm * ITerm		(*    | E I     *)
  | Intro of ITerm * P.Prop		(*    | I : A   *)

  exception Invalid of string

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

end;  (* signature ND2 *)

structure ND2 :> ND2 =
struct

  (* Annotated proof terms *)
  (* Divided into introduction and elimination forms *)
  (* Note the special status of Case and Abort *)

  datatype ITerm =			(* I ::=        *)
    Pair of ITerm * ITerm		(*      <I1,I2> *)
  | Unit				(*    | <>      *)
  | Lam of string * ITerm		(*    | \u. I   *)
  | Inl of ITerm			(*    | inl I   *)
  | Inr of ITerm			(*    | inr I   *)
  | Case of ETerm * (string * ITerm) * (string * ITerm)
					(*    | case E of inl u1 => I1
                                                        | inr u2 => I2 *)
  | Abort of ETerm			(*    | abort E *)
  | Elim of ETerm			(*    | E       *)
  and ETerm =				(* E ::=        *)
    Var of string			(*      u       *)
  | Fst of ETerm			(*    | fst E   *)
  | Snd of ETerm			(*    | snd E   *)
  | App of ETerm * ITerm		(*    | E I     *)
  | Intro of ITerm * P.Prop		(*    | I : A   *)

  exception Invalid of string
  fun check (G, Pair(I1, I2), P.And(A1, A2)) =
        (check (G, I1, A1); check (G, I2, A2))
    | check (G, Unit, True) = ()
    | check (G, Lam(x, I), P.Implies (A, B)) =
	check (C.Decl (G, (x, A)), I, B)
    | check (G, Inl(I), P.Or(A, B)) = check (G, I, A)
    | check (G, Inr(I), P.Or(A, B)) = check (G, I, B)
    | check (G, Case(E, (x1, I1), (x2, I2)), C) =
	(case syn (G, E)
	   of P.Or (A, B) => (check (C.Decl (G, (x1, A)), I1, C);
			    check (C.Decl (G, (x2, B)), I2, C))
            | _ => raise Invalid ("Case subject does not have sum type"))
    | check (G, Abort(E), C) =
	(case syn (G, E)
	   of P.False => ()
            | _ => raise Invalid ("Abort subject does not have void type"))
    | check (G, Elim(E), C) =
      if P.eq (syn (G, E), C) then ()
      else raise Invalid("Mismatch between expected and synthesized type")
    | check _ =
	raise Invalid ("Introduction term does not match expected type")

  and syn (G, Var(u)) =
      (case C.lookup (G, u)
         of SOME(A) => A
          | NONE => raise Invalid("Undeclared variable " ^ u))
    | syn (G, Fst(E)) =
      (case syn (G, E)
         of P.And (A, B) => A
          | _ => raise Invalid("Argument to Fst not product"))
    | syn (G, Snd(E)) =
      (case syn (G, E)
	 of P.And (A, B) => B
	  | _ => raise Invalid("Argument to Snd not product"))
    | syn (G, App(E, I)) =
      (case syn (G, E)
         of P.Implies (A, B) => (check (G, I, A); B)
          | _ => raise Invalid("First argument to App not function"))
    | syn (G, Intro(I, A)) =
      (check (G, I, A); A)

end;  (* structure ND2 *)