(* Theorems *)
(* Author: Carsten Schuermann *)
(* Modified: Brigitte Pientka *)

functor ThmSyn ((*! structure IntSyn : INTSYN !*)
		(*! structure ModeSyn' : MODESYN !*)
		(*! sharing ModeSyn'.IntSyn = IntSyn !*)
		structure Abstract : ABSTRACT
		(*! sharing Abstract.IntSyn = IntSyn !*)
		structure Whnf : WHNF
		(*! sharing Whnf.IntSyn = IntSyn !*)
		(*! structure Paths' : PATHS !*)
		  )
  : THMSYN =
struct
  (*! structure IntSyn = IntSyn !*)
  (*! structure ModeSyn = ModeSyn' *)
  (*! structure Paths = Paths' !*)
  exception Error of string
  fun error (r, msg) = raise Error (Paths.wrap (r, msg))


  type Param = string option

  datatype Order =
    Varg of string list
  | Lex of Order list
  | Simul of Order list

  (* -bp *)
  datatype Predicate = Less | Leq | Eq

  datatype RedOrder = 
      RedOrder of Predicate * Order * Order

  datatype Callpats =
    Callpats of (IntSyn.cid * Param list) list 

  (* Termination declaration *)
  datatype TDecl = 
    TDecl of (Order * Callpats)

  (* -bp *)
  (* Reduction declaration *)
  datatype RDecl = 
    RDecl of (RedOrder * Callpats)

  (* Tabled declaration *)
  datatype TabledDecl = 
    TabledDecl of IntSyn.cid

  (* KeepTable declaration *)
  datatype KeepTableDecl = 
    KeepTableDecl of IntSyn.cid

  (* Theorem declaration *)
  datatype ThDecl =
    ThDecl of (IntSyn.Dec IntSyn.Ctx * IntSyn.Dec IntSyn.Ctx) list
              * IntSyn.Dec IntSyn.Ctx * ModeSyn.Mode IntSyn.Ctx * int

  (* Proof declaration *)
  datatype PDecl = 
    PDecl of int * TDecl

  (* World declaration *)
(*  datatype WDecl = 
    WDecl of (IntSyn.Dec IntSyn.Ctx * 
	      IntSyn.Dec IntSyn.Ctx) list * Callpats *)
  datatype WDecl = 
    WDecl of IDs.Qid list * Callpats

  local

    structure I = IntSyn
    structure M = ModeSyn

    (* theoremDecToConDec (name, T) = D' 
     
       Invariant:
       If   name is the name of a theorem 
       and  T is the declaration of a theorem 
       then D' is a constant type declaration of this theorem
    *)

    fun theoremDecToConDec ((name, ThDecl (GBs, G, MG, i)), r) = 
	let 
	  (* theoremToConDec' G V = V'

	     Invariant:
	     If   G = V1 .. Vn
	     and  G |- V : kind
	     then V' = {V1} .. {Vn} V 
	     and  . |-  V' : kind
	  *)

	  fun theoremToConDec' (I.Null, V) = V
	    | theoremToConDec' (I.Decl (G, D), V) =
		if Abstract.closedDec (G, (D, I.id))
		  then theoremToConDec' (G, Abstract.piDepend ((Whnf.normalizeDec (D, I.id), 
								I.Maybe), V))
		else error (r, "Free variables in theorem declaration")
	in
	  (GBs, I.ConDec ([name], nil, i, I.Normal, theoremToConDec' (G, I.Uni (I.Type)), I.Kind))
	end
   

    (* theoremDecToModeSpine (name, T) = mS' 
     
       Invariant:
       If   name is the name of a theorem 
       and  T is the declaration of a theorem 
       then mS' is a mode spine reflecting the 
	 quantifier information for the theorem
    *)

    fun theoremDecToModeSpine ((name,  ThDecl (GBs, G, MG, i)), r) = 
      let 
	fun theoremToModeSpine' (I.Null, I.Null, mS) = mS
	  | theoremToModeSpine' (I.Decl (G, I.Dec (I.VarInfo(x,_,_,_), _)), I.Decl (MG, m), mS) =
	      theoremToModeSpine' (G, MG, M.Mapp (M.Marg (m, x), mS))
      in
        theoremToModeSpine' (G, MG, M.Mnil)
      end

  in
    val theoremDecToConDec = theoremDecToConDec
    val theoremDecToModeSpine = theoremDecToModeSpine 
  end (* local *)

end; (* functor ThmSyn *)