(* proofs in natural deduction (a.k.a, positive unit resolution) format, headers.
   Copyright (C) 2003 Jean Goubault-Larrecq and LSV, CNRS UMR 8643 & ENS Cachan.

   This file is part of h1.

   h1 is free software; you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation; either version 2, or (at your option)
   any later version.

   h1 is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with h1; see the file COPYING.  If not, write to
   the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
*)

open "proof_aux_h";

(* We only deal with definite gclauses.
 A gclause GCLAUSE ([a1, ..., an], [a]) with free variables X1, ..., Xk
 (as given by gclause_vars) is seen as the formula:
 forall X1, ..., Xk . a1 -> ... -> an -> a.
 Some of these gclauses C also serve as constants c inhabiting the type C.
 This is the case for input clauses, i.e., the ones in the <definitions>
 and <approximation> sections.
 *)

datatype pfc_kind = PFC_SPLIT_DEF (* a splitting definition, e.g.
				   #ne(A&B) :- A(X), B(X). *)
       | PFC_ABBRV_DEF (* an abbreviation definition, e.g.
			#q1 (X1) :- knows key(prv,X1). *)
       | PFC_DEF (* a clause in the <definitions> section. *)
       | PFC_INPUT (* a clause in the <approximation> section. *)
       | PFC_AXIOM of string (* some well-known logical axiom. *)
	 ;

type qclause = string list * string gclause; (* ([X1, ..., Xk], c)
					      denotes forall X1, ..., Xk . c;
					      the quantification over X1, ..., Xk
					      is made explicit; all
					      variables free in c are quantified upon. *)

datatype pfabs = PF_L0 of pfc (* a genuine proof. *)
       | PF_L1 of string term -> pfabs (* lambda X1 . pf : a lambda-abstraction on first-order vars. *)
       | PF_L2 of pfc -> pfabs (* lambda H1 . pf: second-order lambda-abstraction. *)
and pfc = PFC of pfc_kind * qclause * string term list * pfc list
(* pf = PFC (kind, c, [t1, ..., tk], [pf1, ..., pfn])
 where c = GCLAUSE ([a1, ..., an], [a]) with free variables X1, ..., Xk
 (as given by gclause_vars),
 and pf1 : a1 sigma, ..., pfn : an sigma,
 sigma = [X1:=t1, ..., Xn:=tn],
 is a proof of a sigma.
 *);

extern val pfc_apply_1 : pfabs * string term -> pfabs;
	   (* apply a proof abstraction on a first-order term. *)
extern val pfc_apply_l_1 : pfabs * string term list -> pfabs;
	   (* apply a proof abstraction on a list of first-order terms. *)
extern val pfc_apply_2 : pfabs * pfc -> pfabs;
	   (* apply a proof abstraction on a concrete proof. *)
extern val pfc_apply_l_2 : pfabs * pfc list -> pfabs;
	   (* apply a proof abstraction on a list of concrete proofs. *)

extern val pfc_from_clause : pfc_kind * string gclause -> pfabs;
	   (* generate a proof of the clause in input.
	    It is assumed that the clause itself is an axiom that we
	    may use.  In other words,
	    we compile clauses from <definitions> or <approximation> sections as follows.
	    Given the clause c = forall X1, ..., Xk . a1 -> ... -> an -> a,
	    we compile it as
	    lambda X1, ..., Xk . lambda H1:a1 . ... . lambda Hn : an .
	    c X1 ... Xk H1 ... Hn
	    *)

exception PfcSplitDefEvt;
extern val pfc_split_def : string gclause -> pfabs;
(* Compile input clause as a splitting definition;
 raise PfcSplitDefEvt if not a valid splitting definition clause. *)
(* We compile splitting definitions, e.g., #ne(A&B) :- A(X), B(X)., as:
 lambda X . lambda H1:A(X) . lambda H2:B(X) .
   c X H1 H2
 where c = PFC_SPLIT_DEF, ([X], c) is the constant of type forall X . #ne(A&B) :- A(X), B(X).
*)

exception PfcSplitUseEvt;
extern val pfc_split_use : pfabs * string gclause * string gclause -> pfabs;
(* Given pfa, c1, c2, where pfa is a proof of c1,
 and c2 is obtained by epsilon-splitting of c1,
 generate a proof abstraction of c2.
 Raise PfcSplitUseEvt if not logically correct. *)

exception PfcSplitSplitEvt;
extern val pfc_split_split : pfabs * string gclause * string gclause -> pfabs;
(* Given pfa, c1, c2, where pfa is a proof of c1,
 and c2 is obtained by split-splitting of c1,
 generate a proof abstraction of c2.
 Split-splitting is the rule that allows one to derive, say, ne(P&R) from ne(P&Q&R).
 Raise PfcSplitSplitEvt if not logically correct. *)

exception PfcInterDefEvt;
extern val pfc_inter_def : string gclause -> pfabs;
(* Compile input clause as intersection definition;
 raise PfcInterDefEvt if not a valid intersection definition clause. *)
(* We compile intersection definitions, e.g., __inter_P_Q(X) :- P(X), Q(X), as:
 lambda X . lambda H1:P(X) . lambda H2:Q(X) .
     c X H1 H2
  where c = PFC_ABBRV_DEF, ([X], c) is the constant of type
 forall X . __inter_P_Q(X) :- P(X), Q(X).
 This is very similar to pfc_split_def.
 *)

exception PfcInterUseEvt;
extern val pfc_inter_use : pfabs * string gclause * string gclause -> pfabs;
(* Given pfa, c1, c2, where pfa is a proof of c1,
 and c2 is obtained by replacing epsilon-blocks B(X) of c1 by
 single intersection predicates __inter_B(X),
 generate a proof abstraction of c2.
 Raise PfcInterUseEvt if not logically correct.
 Very similar to pfc_inter_use.
*)

exception PfcAbbrvDefEvt;
extern val pfc_abbrv_def : (string -m> string gclause) ref
	   * string gclause
	   -> pfabs;
(* Given (table, c), return a proof of c by P_ABBRV_DEF,
 where c is of the form #q<n> (X1,...,Xn) :- body.
 Similar to pfc_split_def, except we cannot get the definition of
 #q<n> from its name.  So we update table to this end,
 and consult it to verify that definitions are not changed from
 one instance to another.
 We also check that X1, ..., Xn contains all the variables in body.
 Otherwise PfcAbbrvDefEvt is raised (this is raised normally if
 this is not a valid definition).
*)

exception PfcAbbrvUseEvt;
extern val pfc_abbrv_use : (string -m> string gclause) ref
	   * pfabs * string gclause * string gclause
	   -> pfabs;
(* Similar to pfc_split_use, but for #q<n> symbols.
 Relies on first, table argument to get the definition of #q<n>
 symbols. *)

(* Given a proof pf (of type pfabs) of clause c, and a substitution sigma,
 produce a proof of c.sigma, and the clause c.sigma itself. *)
extern val pfc_apply_subst : pfabs * string gclause * (string -m> string term)
	   -> pfabs * string gclause;

exception PfcResolveEvt;
extern val pfc_resolve : (pfabs * string gclause) * (pfabs * string gclause) list
	   * string gclause * string term
	   -> pfabs;
(* pfc_resolve ((pf0, c0), prems, c, default_term):
 Given a list (pf0,c0)::prems of (pfi, ci) where each pfi is a proof of ci,
 and a clause c, produce a proof of the resolvent.
 c0 is the main premise.  default_term is any ground term, needed
 to show that the type of terms is not empty (typically "*" $ nil).
 *)

exception PfcSortSimplifyEvt;
extern val pfc_sort_simplify : (pfabs * string gclause) * (pfabs * string gclause) list
	   * string gclause * string term
	   -> pfabs;
(* pfc_sort_simplify ((pf0, c0), prems, c, default_term):
 Given a list (pf0,c0)::prems of (pfi, ci) where each pfi is a proof of ci,
 and a clause c, produce a proof of the resolvent.
 c0 is the main premise.  default_term is any ground term, needed
 to show that the type of terms is not empty (typically "*" $ nil).
 Although this looks like pfc_resolve,
 several resolution steps can be performed by pfc_sort_simplify
 in sequence; on the other hand, pfc_sort_simplify can only be required
 to prove c from c0 when c is a subclause of c0, i.e., c0 = c \/ c' for
 some c'.  The idea is that the extra atoms from c' can be deduced from
 those of c plus the clauses ci, using only propositional reasoning.
 Raises PfcSortSimplifyEvt if proof cannot be reconstructed.
 *)

exception PfcWeakenPosEvt;
extern val pfc_weaken_pos : pfabs * string gclause * string gclause -> pfabs;
(* pfc_weaken_pos (pfa, c, c');
 Given a proof pfa of c, a Horn clause,
 returns a proof of c', which is a disjunction of c with additional
 positive atoms.
*)

exception PfcMakeNatdedEvt of string;
extern val make_natded : string gclause set * string gclause set * deduction_tree
	   * (string -m> string gclause) ref
	   -> string gclause -> pfabs;
(* make_natded (definitions, approximation, deductions, abbrv_table) c
 produces a proof of clause c from definitions,approximation,deductions.
 Raises PfcMakeNatdedEvt msg, where msg is an error msg,
 if verification failed. *)
