(* proofs in natural deduction (a.k.a, positive unit resolution) format.
   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 "natded_h";
open "ne_h";
open "intersym_h";
open "rel_h";
open "sort_h";

exception PfcApply1;

fun pfc_apply_1 (PF_L1 f, t) = f t
  | pfc_apply_1 arg = raise PfcApply1;

fun pfc_apply_l_1 (pfa, nil) = pfa
  | pfc_apply_l_1 (pfa, t::ts) =
    pfc_apply_l_1 (pfc_apply_1 (pfa, t), ts)

exception PfcApply2;

fun pfc_apply_2 (PF_L2 f, pfc) = f pfc
  | pfc_apply_2 arg = raise PfcApply2;

fun pfc_apply_l_2 (pfa, nil) = pfa
  | pfc_apply_l_2 (pfa, t::ts) =
    pfc_apply_l_2 (pfc_apply_2 (pfa, t), ts)

val Xsort = sort (op strless);

exception PfcFromClause;

fun pfc_from_clause (kind, c as GCLAUSE (neg, _)) =
    let val Xs = Xsort (gclause_vars c)
	fun do_from_clause_1 (neg, accneg, sigma) =
	    case neg of
		A :: rest => PF_L2 (fn pf =>
				       do_from_clause_1 (rest, pf::accneg, sigma))
	      | _ => PF_L0 (PFC (kind, (Xs, c),
				 [?sigma X
				 | X in list Xs] handle MapGet => raise PfcFromClause,
				   rev accneg))
	fun do_from_clause (Xs, sigma) =
	    case Xs of
		X :: rest => PF_L1 (fn t =>
				       do_from_clause (rest, sigma ++ {X => t}))
	      | _ => do_from_clause_1 (neg, nil, sigma)
    in
	do_from_clause (Xs, {})
    end;

fun pfc_split_def (c as GCLAUSE (neg, [ne $ nil])) =
    (let val ql = ne_of ne
	 val ql' = {P
		   | P $ _ in list neg}
     in
	 if ql=ql'
	     then case gclause_vars c of
		      {X} => let val qc = ([X], c)
				 fun do_split_def (nil, acc, t) =
				     PF_L0 (PFC (PFC_SPLIT_DEF, qc, [t], rev acc))
				   | do_split_def (_ :: neg, acc, t) =
				     PF_L2 (fn pfA =>
					       do_split_def (neg, pfA :: acc, t))
			     in
				 iterate
				   (case H of
					_ $ [V _] => ()
				      | _ => raise PfcSplitDefEvt)
				 | H in list neg
				 end;
				 PF_L1 (fn t => do_split_def (neg, nil, t))
			     end
		    | _ => raise PfcSplitDefEvt
	 else raise PfcSplitDefEvt
     end handle NeOf => raise PfcSplitDefEvt)
  | pfc_split_def c = raise PfcSplitDefEvt;

exception PfcSplitUse;
exception PfcSplitUse1Evt;

fun pfc_split_use (pfa, c1 as GCLAUSE (neg1, pos1), c as GCLAUSE (neg, pos)) =
    if pos=pos1
	then let val negs = elems neg
		 val negs1 = elems neg1
		 val qs = negs \ negs1
		 val splitBs = union_rel {(case A of
					       P $ [V X] =>
					       {X => {P}}
					     | _ => raise PfcSplitUseEvt)
					 | A in set negs1 \ negs}
		 val invBs = invrel splitBs (* maps blocks to sets of variables *)
		 val other_vars = union {tvars t | t in list pos} U
		     union {tvars t | t in set negs & negs1}
		 val qsx = {(case q of
				 ne $ nil =>
				 (ne_of ne handle NeOf => raise PfcSplitUseEvt)
			       | _ => raise PfcSplitUseEvt)
			   | q in set qs}
		     (* qsx is set of blocks corresponding to ne atoms in goal clause c. *)
		 val vars_c1 = Xsort (gclause_vars c1)
		 fun do_split_use_1 (neg, accneg, sigma) =
		     case neg of
			 A :: rest =>
			 if A inset qs
			     then (let val ne $ nil = A
				       val qs = ne_of ne
				       val Xs = ?invBs qs
				   in
				       PF_L2 (fn pfA =>
						 (* Now A is ne(P&Q) [say], and pfA should
						  be a proof of the form
						  split_def (ne(P&Q) :- P(X), Q(X),
						  t, proof-of-P(t), proof-of-Q(t))
						  *)
						 case pfA of
						     PFC (PFC_SPLIT_DEF, ([_],
									    GCLAUSE (sneg, _)),
							  [t], pfs) =>
						     let val pfmap = {P => pf
								     || P $ _ in list sneg and
									pf in list pfs}
							     handle ParSweep => raise PfcSplitUse
						     in
							 do_split_use_1 (rest,
									 accneg ++ {P $ [V X] =>
										     ?pfmap P
										   | P in set qs and
										     X in set Xs},
									 sigma ++ {X => t
										  | X in set Xs})
							 handle MapGet => raise PfcSplitUse
						     end
						   | _ => raise PfcSplitUse)
				   end handle Bind => raise PfcSplitUse
					    | NeOf => raise PfcSplitUse
					    | MapGet => raise PfcSplitUse)
			 else PF_L2 (fn pfA =>
					do_split_use_1 (rest, accneg ++ {A => pfA}, sigma))
		       | _ => pfc_apply_l_2 (pfc_apply_l_1 (pfa,
							    [?sigma X
							    | X in list vars_c1]
							      handle MapGet => raise PfcSplitUse),
					     [?accneg A
					     | A in list neg1]
					       handle MapGet => raise PfcSplitUse)
		 fun do_split_use (vars_c, sigma) =
		     case vars_c of
			 X :: rest =>
			 PF_L1 (fn t =>
				   do_split_use (rest, sigma ++ {X => t}))
		       | _ => do_split_use_1 (neg, {}, sigma)
	     in
		 if other_vars intersects splitBs orelse dom invBs<>qsx
		     then raise PfcSplitUseEvt
		 else do_split_use (Xsort (gclause_vars c), {})
	     end
    else raise PfcSplitUseEvt;

exception PfcSplitSplit;

fun pfc_split_split (pfa, GCLAUSE (nil, [q $ nil]), GCLAUSE (nil, [q' $ nil])) =
    (let val qs = ne_of q
	 val qs' = ne_of q'
     in
	 if qs' subset qs
	     then case pfa of
		      PF_L0 (PFC (PFC_SPLIT_DEF, ([X], GCLAUSE (neg, [_])), [t], pfs)) =>
		      let val pfmap = {A => pf
				      || A in list neg and
					 pf in list pfs} handle ParSweep => raise PfcSplitSplit
			  val neg' = [A
				     | A as P $ _ in list neg
					 such that P inset qs']
		      in
			  PF_L0 (PFC (PFC_SPLIT_DEF, ([X], GCLAUSE (neg', [q' $ nil])),
				      [t],
					[?pfmap A
					| A in list neg'] handle MapGet => raise PfcSplitSplit
					  ))
		      end
		    | _ => raise PfcSplitSplit
	 else raise PfcSplitSplitEvt
     end handle NeOf => raise PfcSplitSplitEvt)
  | pfc_split_split arg = raise PfcSplitSplitEvt;

fun pfc_inter_def (c as GCLAUSE (neg, [f $ [V x]])) =
    let val B = block_of_inter f
	val B' = {P
		 | P $ _ in list neg}
    in
	if B=B'
	    then case gclause_vars c of
		     {X} => let val qc = ([X], c)
				fun do_inter_def (nil, acc, t) =
				    PF_L0 (PFC (PFC_ABBRV_DEF, qc, [t], rev acc))
				  | do_inter_def (_ :: neg, acc, t) =
				    PF_L2 (fn pfA =>
					      do_inter_def (neg, pfA :: acc, t))
			    in
				iterate
				  (case H of
				       _ $ [V _] => ()
				     | _ => raise PfcInterDefEvt)
				| H in list neg
				end;
				PF_L1 (fn t => do_inter_def (neg, nil, t))
			    end
		   | _ => raise PfcInterDefEvt
	else raise PfcInterDefEvt
    end
  | pfc_inter_def c = raise PfcInterDefEvt;

exception PfcInterUse;

fun pfc_inter_use (pfa, c1 as GCLAUSE (neg1, pos1), c as GCLAUSE (neg, pos)) =
    if pos=pos1
	then let val negs = elems neg
		 val negs1 = elems neg1
		 val Bs = negs \ negs1
		 val interBs = union_rel {(case A of
					       P $ [V X] =>
					       {X => {P}}
					     | _ => raise PfcInterUseEvt)
					 | A in set negs1 \ negs}
		 val invBs = invrel interBs (* maps blocks to sets of variables *)
		 val other_vars = union {tvars t | t in list pos} U
		     union {tvars t | t in set negs & negs1}
		 val Bsx = {(case B of
				 P $ [V _] =>
				 block_of_inter P
			       | _ => raise PfcInterUseEvt)
			   | B in set Bs}
		     (* Bsx is set of blocks corresponding to intersection atoms
		      in goal clause c. *)
		 val vars_c1 = Xsort (gclause_vars c1)
		 fun do_inter_use_1 (neg, accneg, sigma) =
		     case neg of
			 A :: rest =>
			 if A inset Bs
			     then (let val P $ [V _] = A
				       val B = block_of_inter P
				       val Xs = ?invBs B
				   in
				       PF_L2 (fn pfA =>
						 (* Now A is __inter_P_Q (X) [say], and pfA should
						  be a proof of the form
						  abbrv_def (__inter_P_Q(X) :- P(X),Q(X),
						  t, proof-of-P(t), proof-of-Q(t))
						  *)
						 case pfA of
						     PFC (PFC_ABBRV_DEF, ([_],
									    GCLAUSE (sneg, _)),
							  [t], pfs) =>
						     let val pfmap = {P => pf
								     || P $ _ in list sneg and
									pf in list pfs}
							     handle ParSweep => raise PfcInterUse
						     in
							 do_inter_use_1 (rest,
									 accneg ++ {P $ [V X] =>
										    ?pfmap P
										   | P in set B and
										     X in set Xs},
									 sigma ++ {X => t
										  | X in set Xs})
							 handle MapGet => raise PfcInterUse
						     end
						   | _ => raise PfcInterUse)
				   end handle Bind => raise PfcInterUse
					    | MapGet => raise PfcInterUse)
			 else PF_L2 (fn pfA =>
					do_inter_use_1 (rest, accneg ++ {A => pfA}, sigma))
		       | _ => pfc_apply_l_2 (pfc_apply_l_1 (pfa,
							    [?sigma X
							    | X in list vars_c1]
							    handle MapGet => raise PfcInterUse),
					     [?accneg A
					     | A in list neg1]
					     handle MapGet => raise PfcInterUse)
		 fun do_inter_use (vars_c, sigma) =
		     case vars_c of
			 X :: rest =>
			 PF_L1 (fn t =>
				   do_inter_use (rest, sigma ++ {X => t}))
		       | _ => do_inter_use_1 (neg, {}, sigma)
	     in
		 if other_vars intersects interBs orelse dom invBs<>Bsx
		     then raise PfcInterUseEvt
		 else do_inter_use (Xsort (gclause_vars c), {})
	     end
    else raise PfcInterUseEvt;

exception PfcAbbrvDef;

local
    val nfa = re_make_nfa [(re_parse "^#q", fn _ => ())]
in
    fun matches_abbrv P =
	case nfa_run (nfa, P) of
	    SOME _ => true
	  | _ => false
end;

fun pfc_abbrv_def (table, c as GCLAUSE (neg, [a as (abbrv $ args)])) =
    (if abbrv inset !table
	 then let val c' = ?(!table) abbrv
	      in
		  if c=c'
		      then ()
		  else raise PfcAbbrvDefEvt
	      end
     else ();
	 if matches_abbrv abbrv
	     then let val vars = gclause_vars c
		      val varl = Xsort vars
		  in
		      if vars=tvars a
			  then let val qc = (varl, c)
				   fun do_abbrv_def_1 (nil, acc, sigma) =
				       PF_L0 (PFC (PFC_ABBRV_DEF, qc,
						   [?sigma x | x in list varl]
						   handle MapGet => raise PfcAbbrvDef,
						   rev acc))
				     | do_abbrv_def_1 (_ :: neg, acc, sigma) =
				       PF_L2 (fn pfA =>
						 do_abbrv_def_1 (neg, pfA :: acc, sigma))
				   fun do_abbrv_def (varsl, sigma) =
				       case varsl of
					   X :: rest =>
					   PF_L1 (fn t =>
						     do_abbrv_def (rest, sigma ++ {X => t}))
					 | _ => do_abbrv_def_1 (neg, nil, sigma)
				   val pfa = do_abbrv_def (varl, {})
			       in
				   table := !table ++ {abbrv => c};
				   pfa
			       end
		      else raise PfcAbbrvDefEvt
		  end
	 else raise PfcAbbrvDefEvt
	     )
  | pfc_abbrv_def _ = raise PfcAbbrvDefEvt;

exception PfcAbbrvUse;
exception PfcAbbrvUseNotInTable;
exception GetRenaming;

fun get_renaming (V x, t as V y, sigma) =
    if x inset sigma
	then let val t' = ?sigma x
	     in
		 if t=t'
		     then sigma
		 else raise GetRenaming
	     end
    else sigma ++ {x => t}
  | get_renaming (f $ l, f' $ l', ren) =
    if f=f'
	then get_renaming_l (l, l', ren)
    else raise GetRenaming
  | get_renaming _ = raise GetRenaming
and get_renaming_l (nil, nil, sigma) = sigma
  | get_renaming_l (t::l, t' :: l', sigma) =
    get_renaming_l (l, l', get_renaming (t, t', sigma))
  | get_renaming_l _ = raise GetRenaming;

fun pfc_abbrv_use (table, pfa, c1 as GCLAUSE (neg1, pos1), c as GCLAUSE (neg, pos)) =
    if pos=pos1
	then let val t = !table
		 val negs = elems neg
		 val negs1 = elems neg1
		 val abbrvs = negs \ negs1
		 val abbrv_syms = {if abbrv inset t
				       then abbrv
				   else raise PfcAbbrvUseNotInTable
				  | abbrv $ _ in set abbrvs}
		 val vars_c1 = Xsort (gclause_vars c1)
		 fun do_abbrv_use_1 (neg, accneg, sigma) =
		     case neg of
			 (A as AP $ Aargl) :: rest =>
			 if A inset abbrvs
			     then (let val defA = ?t AP
				   in
				       PF_L2 (fn pfA =>
						 (* Now A is #q<n> (t1..tn) [say],
						  the definition of A is:
						  def = (#q<n> (X1..Xn) :- B(X1..Xn)),
						  and pfA should be a proof of the form
						  abbrv_def (def, [t1..tn],
						  proof-of-B(t1..tn)
						  *)
						  case pfA of
						      PFC (PFC_ABBRV_DEF,
							   (_, defA' as GCLAUSE (sneg, [a'])),
							   argl, pfs) =>
						      if defA=defA'
							  then let val ren =
								       get_renaming (a', A, {})
								   val tren = tsubst ren
								   val pfmap =
								       {tren B => pf
								       || B in list sneg and
									  pf in list pfs}
								       handle ParSweep =>
								       raise PfcAbbrvUse
							       in
								   do_abbrv_use_1 (rest,
										   accneg ++
										   pfmap,
										   sigma
										   )
								   handle MapGet =>
								   raise PfcAbbrvUse
							       end
						      else raise PfcAbbrvUse
						    | _ => raise PfcAbbrvUse)
				   end)
			 else PF_L2 (fn pfA =>
					do_abbrv_use_1 (rest, accneg ++ {A => pfA}, sigma))
		       | _ => pfc_apply_l_2 (pfc_apply_l_1 (pfa,
							    [?sigma X
							    | X in list vars_c1]
							    handle MapGet => raise PfcAbbrvUse),
					     [?accneg A
					     | A in list neg1]
					     handle MapGet => raise PfcAbbrvUse)
		 fun do_abbrv_use (vars_c, sigma) =
		     case vars_c of
			 X :: rest =>
			 PF_L1 (fn t =>
				   do_abbrv_use (rest, sigma ++ {X => t}))
		       | _ => do_abbrv_use_1 (neg, {}, sigma)
	     in
		 do_abbrv_use (Xsort (gclause_vars c), {})
	     end
    else raise PfcAbbrvUseEvt;

fun pfc_apply_subst (pf, c, {}) = (pf, c)
  | pfc_apply_subst (pf, c as GCLAUSE (neg, pos), sigma) =
    let val Xs = Xsort (gclause_vars c)
	val tsub = tsubst sigma
	val csigma = GCLAUSE ([tsub t | t in list neg], [tsub t | t in list pos])
	val Ys = Xsort (gclause_vars csigma)
	fun do_apply_subst (Ys, sigma') =
	    case Ys of
		Y :: rest => PF_L1 (fn t =>
				       do_apply_subst (rest, sigma' ++ {Y => t}))
	      | _ => let val tsub' = tsubst sigma'
		     in
			 pfc_apply_l_1 (pf, [tsub' (if X inset sigma
							then ?sigma X
						    else V X)
					    | X in list Xs])
		     end
    in
	(do_apply_subst (Ys, {}), csigma)
    end;

exception PfcResolve;

fun pfc_resolve ((pf0, c0 as GCLAUSE (neg0, [a0])), prems,
		     c as GCLAUSE (neg, [a]), default_term) =
    let val vars0 = gclause_vars c0
	val Xs0 = Xsort vars0
	val vars_side = union {gclause_vars ci
			      | (_, ci) in list prems}
	val vars_premises = vars0 U vars_side
	val vars_conc = gclause_vars c
	val Xs = Xsort vars_conc
	val headmap = {(case posi of
			    [ai] => ai
			  | _ => raise PfcResolveEvt) => (pfi, ci, Xsort (gclause_vars ci))
		      | (pfi, ci as GCLAUSE (_, posi)) in list prems}
	fun do_resolve_1 (neg, negacc, sigma) =
	    case neg of
		A :: rest => PF_L2 (fn pf =>
				       do_resolve_1 (rest, negacc ++ {A => pf},
						     sigma))
	      | _ => let val pf0x = pfc_apply_l_1 (pf0,
						   [if X inset sigma
							then ?sigma X
						    else default_term
						   | X in list Xs0])
		     in
			 pfc_apply_l_2 (pf0x,
					[if A inset headmap
					     then let val (pfi, GCLAUSE (negi, _), Xsi)
							  = ?headmap A
						      val pfix
							  = pfc_apply_l_1 (pfi,
									   [if X inset sigma
										then ?sigma X
									    else default_term
									   | X in list Xsi])
						      val PF_L0 pfic =
							  pfc_apply_l_2 (pfix,
									 [if A inset negacc
									      then ?negacc A
									  else raise PfcResolve
									 | A in list negi])
						  in
						      pfic
						  end handle Bind => raise PfcResolve
					 else if A inset negacc
					     then ?negacc A
					 else raise PfcResolve
					| A in list neg0])
		     end
	fun do_resolve (Xs, sigma) =
	    case Xs of
		X :: rest =>
		PF_L1 (fn t =>
			  do_resolve (rest, sigma ++ {X => t}))
	      | _ => do_resolve_1 (neg, {}, sigma)
    in
	if a=a0 andalso
	    elems neg = union {if a inset headmap
				   then let val (_, GCLAUSE (negi, _), ...) = ?headmap a
					in
					    elems negi
					end
			       else {a}
			      | a in list neg0}
	    then do_resolve (Xs, {})
	else raise PfcResolveEvt
    end
  | pfc_resolve arg = raise PfcResolveEvt;

fun pfc_sort_simplify ((pf0, c0 as GCLAUSE (neg0, [a0])), prems,
			   c as GCLAUSE (neg, [a]), default_term) =
    let val vars0 = gclause_vars c0
	val Xs0 = Xsort vars0
	val vars_conc = gclause_vars c
	val Xs = Xsort vars_conc
	fun do_sort_simplify_1 (neg, negacc, sigma) =
	    case neg of
		A :: rest => PF_L2 (fn pf =>
				       do_sort_simplify_1 (rest,
							   negacc ++ {A => pf},
							   sigma))
	      | _ =>
		let val qr = ref [(A, pf)
				 | A => pf in map negacc]
		    val unitr = ref ({} : string term -m> pfc)
		    val idxr = ref ({} : string term -m>
				      (int ref * pfabs * string gclause) list ref)
		in
		    iterate
		      (case negi of
			   nil => let val PF_L0 pf =
					  pfc_apply_l_1 (pfai,
							 [if X inset sigma
							      then ?sigma X
							  else default_term
							 | X in list Xsi])
				  in
				      qr := (ai, pf) :: !qr
				  end
			 | _ =>
			   let val nr = ref (len negi)
			   in
			       iterate
				 cntr := (nr, pfai, ci) :: !cntr
			       | aij in list negi
			       val cntr = if aij inset !idxr
					      then ?(!idxr) aij
					  else let val r = ref nil
					       in
						   idxr := !idxr ++ {aij => r};
						   r
					       end
			       end
			   end
			   )
		    | (pfai, ci as GCLAUSE (negi, [ai])) in list (pf0,c0)::prems
		    val Xsi = Xsort (gclause_vars ci)
		    end;
		    while not (null (!qr)) do
			let val (A, pf) :: rest = !qr
			in
			    qr := rest;
			    if A inset !unitr
				then ()
			    else (unitr := !unitr ++ {A => pf};
				  if A inset !idxr
				      then
					  iterate
					    (dec nr;
					     if !nr=0
						 then let val Xsi = Xsort (gclause_vars ci)
							  val pf1 =
							      pfc_apply_l_1 (pfai,
									     [if X inset sigma
										  then ?sigma X
									      else default_term
									     | X in list Xsi])
							  val PF_L0 pf =
							      pfc_apply_l_2 (pf1,
									     [?(!unitr) aij
									     | aij in list negi])
						      in
							  qr := (ai, pf) :: !qr
						      end
					     else ()
						 )
					  | (nr, pfai, ci as GCLAUSE (negi, [ai]))
					    in list !(?(!idxr) A)
					  end
				  else ())
			end;
			if a0 inset !unitr
			    then PF_L0 (?(!unitr) a0)
			else raise PfcSortSimplifyEvt
		end
	fun do_sort_simplify (Xs, sigma) =
	    case Xs of
		X :: rest =>
		PF_L1 (fn t =>
			  do_sort_simplify (rest, sigma ++ {X => t}))
	      | _ => do_sort_simplify_1 (neg, {}, sigma)
    in
	if a=a0
	    then do_sort_simplify (Xs, {})
	else raise PfcSortSimplifyEvt
    end
  | pfc_sort_simplify arg = raise PfcSortSimplifyEvt;

(*
    let val facts = elems neg
	memofun pfc_prove goals =
		if goals = facts
		    then SOME []
		else (case goals \ facts of
			  {a} U rest =>
			  some
			    (pfa, c, GCLAUSE ([a | a in set goals], [a0])) :: pi
			  | (pfa, c as GCLAUSE (neg', [a']))
			    in list prems
				(*$V-*)
			  val true = (a=a')
				(*$V+*)
			  val goals' = rest U elems neg'
			  val SOME pi = pfc_prove goals'
			  end
			| _ => NONE)
	fun chain_resolve ([], pfa0, c0) = pfa0
	  | chain_resolve ((pfa1, sc1, c1) :: pi, pfa0, c0) =
	    chain_resolve (pi, pfc_resolve ((pfa0, c0), [(pfa1, sc1)],
						c1, default_term),
			   c1)
    in
	if a=a0
	    then (case pfc_prove (elems neg0) of
		      SOME pi => chain_resolve (pi, pf0, c0)
		    | _ => raise PfcSortSimplifyEvt)
	else raise PfcSortSimplifyEvt
    end;
*)

exception PfcWeakenPos;

fun pfc_weaken_pos (pfa, c as GCLAUSE (neg, [a]), c' as GCLAUSE (neg', pos)) =
    if neg=neg' andalso a inset elems pos
	then if c=c'
		 then pfa
	     else let val Xs = Xsort (gclause_vars c)
		      val Xs' = Xsort (gclause_vars c')
		      val axiom = GCLAUSE ([a], pos)
		      val AXs = Xsort (gclause_vars axiom)
		      fun do_weaken_pos_1 (neg, negacc, sigma) =
			  case neg of
			      A :: rest => PF_L2 (fn pf =>
						     do_weaken_pos_1 (rest,
								      negacc ++ {A => pf},
								      sigma))
			    | _ => (let val pfax = pfc_apply_l_1 (pfa,
								  [if X inset sigma
								       then ?sigma X
								   else raise PfcWeakenPos
								  | X in list Xs])
					val PF_L0 pfc = pfc_apply_l_2 (pfax,
								       [if A inset negacc
									    then ?negacc A
									else raise PfcWeakenPos
								       | A in list neg])
				    in
					PF_L0 (PFC (PFC_AXIOM "inj",
						    (AXs, axiom),
						    [if X inset sigma
							 then ?sigma X
						     else raise PfcWeakenPos
						    | X in list AXs],
						      [pfc]))
				    end handle Bind => raise PfcWeakenPos)
		      fun do_weaken_pos (Xs', sigma) =
			  case Xs' of
			      X :: rest =>
			      PF_L1 (fn t =>
					do_weaken_pos (rest, sigma ++ {X => t}))
			    | _ => do_weaken_pos_1 (neg, {}, sigma)
		  in
		      do_weaken_pos (Xs', {})
		  end
    else raise PfcWeakenPosEvt
  | pfc_weaken_pos _ = raise PfcWeakenPosEvt;

fun pfc_abbrv_defs (definitions, input, deductions, table) =
    let fun pfc_get_abbrv_defs c =
	    if c inset definitions orelse c inset input
		then ()
	    else if c inset deductions
		then case ?deductions c of
			 ("abbrv-def", nil) =>
			 (let val GCLAUSE (_, [f $ _]) = c
			  in
			      table := !table ++ {f => c}
			  end handle Bind => ())
		       | (_, prem_sigma_l) =>
			 iterate
			   pfc_get_abbrv_defs prem
			 | (prem, _) in list prem_sigma_l
			 end
	    else ()
    in
	pfc_get_abbrv_defs
    end;

val default_term = "*" $ nil;

local
    val nfa = re_make_nfa [(re_parse "resolve", fn _ => ())]
in
    fun matches_resolve P =
	case nfa_run (nfa, P) of
	    SOME _ => true
	  | _ => false
end;

fun make_natded (params as (definitions, input, deductions, table)) =
    let val get_abbrv_defs = pfc_abbrv_defs params
	fun make_lambda c =
	    if c inset definitions
		then pfc_from_clause (PFC_DEF, c)
	    else if c inset input
		then pfc_from_clause (PFC_INPUT, c)
	    else if c inset deductions
		then (case ?deductions c of
			  ("split-def", nil) =>
			  (pfc_split_def c handle PfcSplitDefEvt =>
			   let val f as |[put, convert, ...]| = outstring "clause "
			   in
			       print_gclause_pl (f, identity) c;
			       put " is claimed to be a splitting definition, but is not.";
			       raise PfcMakeNatdedEvt (convert ())
			   end)
			| ("split-use", [(prem, sigma)]) =>
			  (let val (lt, premise)
				   = pfc_apply_subst (make_lambda prem,
						      prem, sigma)
			   in
			       pfc_split_use (lt, premise, c)
			   end handle PfcSplitUseEvt =>
			       let val f as |[put, convert, ...]| = outstring "clause "
			       in
				   print_gclause_pl (f, identity) c;
				   put " is not obtained by splitting from clause ";
				   print_gclause_pl (f, identity) prem;
				   raise PfcMakeNatdedEvt (convert ())
			       end)
			| ("split-split", [(prem, sigma)]) =>
			  (let val (lt, premise)
				   = pfc_apply_subst (make_lambda prem,
						      prem, sigma)
			   in
			       pfc_split_split (lt, premise, c)
			   end handle PfcSplitSplitEvt =>
			       let val f as |[put, convert, ...]| = outstring "clause "
			       in
				   print_gclause_pl (f, identity) c;
				   put " is not obtained by split-split from clause ";
				   print_gclause_pl (f, identity) prem;
				   raise PfcMakeNatdedEvt (convert ())
			       end)
			| ("inter-def", nil) =>
			  (pfc_inter_def c handle PfcInterDefEvt =>
			   let val f as |[put, convert, ...]| = outstring "clause "
			   in
			       print_gclause_pl (f, identity) c;
			       put " is claimed to be an intersection definition, but is not.";
			       raise PfcMakeNatdedEvt (convert ())
			   end)
			| ("inter-use", [(prem, sigma)]) =>
			  (let val (lt, premise)
				   = pfc_apply_subst (make_lambda prem,
						      prem, sigma)
			   in
			       pfc_inter_use (lt, premise, c)
			   end handle PfcInterUseEvt =>
			       let val f as |[put, convert, ...]| = outstring "clause "
			       in
				   print_gclause_pl (f, identity) c;
				   put " is not obtained by introducing intersection predicates from clause ";
				   print_gclause_pl (f, identity) prem;
				   raise PfcMakeNatdedEvt (convert ())
			       end)
			| ("abbrv-def", nil) =>
			  (pfc_abbrv_def (table, c)
			   handle PfcAbbrvDefEvt =>
			   let val f as |[put, convert, ...]| = outstring "clause "
			   in
			       print_gclause_pl (f, identity) c;
			       put " is claimed to define an abbreviation, but does not.";
			       raise PfcMakeNatdedEvt (convert ())
			   end)
			| ("abbrv-use", [(prem, sigma)]) =>
			  (let val (lt, premise)
				   = pfc_apply_subst (make_lambda prem,
						      prem, sigma)
			   in
			       pfc_abbrv_use (table, lt, premise, c)
			   end handle PfcAbbrvUseEvt =>
			       let val f as |[put, convert, ...]| = outstring "clause "
			       in
				   print_gclause_pl (f, identity) c;
				   put " is not obtained by introducing abbreviations from clause ";
				   print_gclause_pl (f, identity) prem;
				   raise PfcMakeNatdedEvt (convert ())
			       end)
			| ("factor", [(prem, sigma)]) =>
			  let val (lt, c')
				  = pfc_apply_subst (make_lambda prem,
						     prem, sigma)
			  in
			      if c<>c'
				  then let val f as |[put, convert, ...]| = outstring "clause "
				       in
					   print_gclause_pl (f, identity) c;
					   put " is not obtained by factoring from clause ";
					   print_gclause_pl (f, identity) prem;
					   raise PfcMakeNatdedEvt (convert ())
				       end
			      else lt
			  end
			| ("weaken-pos", [(prem, sigma), ...]) =>
			  (let val (pfa, c')
				   = pfc_apply_subst (make_lambda prem,
						      prem, sigma)
			   in
			       pfc_weaken_pos (pfa, c', c)
			   end handle PfcWeakenPosEvt =>
			       let val f as |[put, convert, ...]| = outstring "clause "
			       in
				   print_gclause_pl (f, identity) c;
				   put " is not obtained by weakening on the positive side from clause ";
				   print_gclause_pl (f, identity) prem;
				   raise PfcMakeNatdedEvt (convert ())
			       end)
			| ("sort-simplify", premises) =>
			  (if null premises
			       then let val f as |[put, convert, ...]| = outstring
					    "rule sort-simplify used with no premise \
					     \to infer clause "
				    in
					print_gclause_pl (f, identity) c;
					raise PfcMakeNatdedEvt (convert ())
				    end
			   else let val prems = [pfc_apply_subst (make_lambda c,
								  c, sigma)
						| (c, sigma) in list premises]
				in
				    pfc_sort_simplify (hd prems, tl prems, c,
						       default_term)
				end handle _ =>
				let val f as |[put, convert, ...]| = outstring "clause "
				in
				    print_gclause_pl (f, identity) c;
				    put " is not obtained by sort simplification from premises.";
				    raise PfcMakeNatdedEvt (convert ())
				end)
			| (rulename, premises) =>
			  if matches_resolve rulename andalso
			      not (null premises)
			      then let val prems = [pfc_apply_subst (make_lambda c,
								     c, sigma)
						   | (c, sigma) in list premises]
				   in
				       pfc_resolve (hd prems, tl prems, c,
						    default_term)
				   end handle PfcResolveEvt =>
				   let val f as |[put, convert, ...]| = outstring "clause "
				   in
				       print_gclause_pl (f, identity) c;
				       put " is not obtained by resolution from premises.";
				       raise PfcMakeNatdedEvt (convert ())
				   end
			  else let val f as |[put, convert, ...]| = outstring "rule "
			       in
				   put rulename;
				   put " is unknown, or cannot justify clause ";
				   print_gclause_pl (f, identity) c;
				   raise PfcMakeNatdedEvt (convert ())
			       end)
		 else let val f as |[put, convert, ...]| = outstring "clause "
		      in
			  print_gclause_pl (f, identity) c;
			  put " has no proof.";
			  raise PfcMakeNatdedEvt (convert ())
		      end
    in
	fn c => (get_abbrv_defs c; make_lambda c)
    end;

