File ProofObligationMgr.sml


(* *********************************************************************** *)
(*									   *)
(* Author: B. Wolff,                                                       *)
(* Date: 21.09.06				 			   *)
(* Purpose of this file: A Generic Proof-Obligation(PO)Manager for Isabelle*)
(*                       It allows introduction and bookkeeping of PO's    *)
(*                       The package also defines the generic part of      *)
(*                       the ISAR syntax, i.e. po, discharge, list_po,     *)
(*                       show_po, etc.                                     *)
(*                       Some hack prevents the easy use of sorry or done. *)
(*									   *)
(* *********************************************************************** *)



structure POKind =
  struct

    datatype kind = wff | repr | meth | lethal 
                    (* classes of proof obligations, e.g.
		       well-formedness-constraint, 
		       representational-constraint,
		       methodological-constraint
                       (resulting from analytical statements),
		       lethal-side-condition ... 
		       As "lethal side condition" we consider
		       deep logical inconsistencies that are
		       *tolerated* on the object logical level
		       (such as False on axdef in Z) *)


  end 

signature FMETHOD =
  sig
    val  PO_classifier : POKind.kind Symtab.table
                        (* data requirement: keys in symtab
			   must neither contain "_" nor "." *)
    type content        (* state of the method package *)
    val  init          : content
    val  merge         : content * content -> content
    val  print         : content -> unit
  end


signature PO_MGR =
  sig
    val  PO_state_setup   : (theory -> theory) list 
                            (* making isar initilizing
                               this component *)

    type path
    type state

    val  get_state        : theory -> state   
    val  mt_state         : state
    val  print_state      : 'a -> state -> unit

    structure FMethod     : FMETHOD
    val  get_content      : theory -> FMethod.content
    val  set_content      : FMethod.content -> theory -> theory

    val  get_path         : theory -> path
    val  set_path         : path -> theory -> theory

    val  get_prover_tab   : theory -> tactic Symtab.table
    val  set_prover_tab   : tactic Symtab.table -> theory -> theory

    type PO_name
    (* A PO_name is :  a) a path  b) a classifier c) a core name
       d) an index. (PO Management makes sure that  PO_names are unique. *)

    val  mk_PO_name       : path * string * string * int -> PO_name
    val  dest_PO_name     : PO_name -> (path * string * string * int) option

    val  declare_PO       : path option * string * string
                            -> cterm -> theory -> theory
			    
    val  prove_i_PO       : bool -> string -> theory -> theory
    (* essential discharge mechanism (classical goal package)
       PRE string must be declared PO name
       POST proof state opened in goal package.
            if bool true, then also automatic proof attempt.
       NOT ISAR READY.
     *)
    val  prove_PO     : string -> theory -> Proof.state
    (* essential discharge mechanism (ISAR version)
       PRE string must be declared PO name
       POST proof state opened in goal package.
     *)
    
    (* NOT EXPORTED:
    val  set_status_of_PO : cterm -> string -> theory -> theory
    would allow to discharge PO's. *)

    val  get_status_of_PO : cterm -> theory -> string option option

    val  get_name_of_PO   : cterm -> theory -> PO_name option

    val  get_PO_from_name : string -> theory -> cterm

    val  list_POs         : string list -> theory -> string list

    val  check_statistics : string list -> theory -> unit
  end



functor PO_Manager (FMethod : FMETHOD) : PO_MGR =
struct
    open POKind
    structure FMethod = FMethod
    val DEBUG = ref([]:string list)

    type PO_name = string

    fun isClassifier x = x mem (map fst (Symtab.dest FMethod.PO_classifier)) 

    fun mk_PO_name (path, classifier,corename,index) =
        if isClassifier classifier 
        then path^NameSpace.separator^classifier^"_"
             ^corename^"_"^(Int.toString index)
        else error "mk_PO_name"

    fun dest_PO_name name =
        let val path = NameSpace.drop_base name
        in case String.tokens (fn c => c= #"_") (NameSpace.base name) of
           [cl,co,instr] => case Int.fromString instr of 
                               SOME i => if isClassifier cl 
                                         then SOME (path,cl,co,i)
                                         else NONE
                             | NONE   => NONE
            | _ => NONE
        end

    fun mk_PO_name_base (path, classifier,corename) = 
        if isClassifier classifier 
        then path^NameSpace.separator^classifier^"_"^corename 
        else error "mk_PO_name_base"


    fun fast_cterm_ord (ct1,ct2) =
        prod_ord string_ord Term.fast_term_ord
            ((Context.theory_name (theory_of_cterm ct1), term_of ct1),
             (Context.theory_name (theory_of_cterm ct2), term_of ct2)) 

    structure Ctermtab = TableFun(type key = cterm val ord = fast_cterm_ord);

    type path  = string

    datatype state = MkState of 
                      {act_path      : path,
                       method_state  : FMethod.content,
                       PO_prover_tab : tactic Symtab.table,
				       (* PO_classifier to tactic *)
                       PO_tab        : (cterm*string option) list Symtab.table,
                                       (* PO_name without index to PO reprs *)
		       ran_PO_tab    : path Ctermtab.table
                      }

    val mt_state = MkState{act_path = "",
                           method_state = FMethod.init,
                           PO_prover_tab=Symtab.make 
                                         (map (fn (n,_)=> (n,no_tac))
                                              (Symtab.dest FMethod.PO_classifier)),
                           PO_tab = Symtab.empty,
                           ran_PO_tab = Ctermtab.empty
                          }

   fun merge_state pp (MkState state1, MkState state2) =
       let val {act_path = ap1,method_state=ms1,PO_prover_tab= pt1, 
                PO_tab = t1, ran_PO_tab = rpt1} = state1
           val {act_path = ap2,method_state=ms2,PO_prover_tab= pt2, 
                PO_tab = t2, ran_PO_tab = rpt2} = state1
       in  MkState{act_path = "",
                   method_state = FMethod.merge(ms1,ms2),
                   PO_prover_tab = pt2,
                   PO_tab = Symtab.merge(op =)(t1,t2),
                   ran_PO_tab = Ctermtab.merge(op =)(rpt1,rpt2)
                  }
       end


   fun pr1 str =(writeln""; 
                 case the(Symtab.lookup FMethod.PO_classifier str) of
                       wff   => (writeln("well-formedness proof-obligations:"^str))
                     | repr  => (writeln("representational proof-obligations:"^str))
                     | meth  => (writeln("methodological proof-obligations:"^str))
                     | lethal=> (writeln("lethal proof-obligations:"^str)));


   fun print_state thy (MkState{PO_tab, method_state, ...}) =
       let fun pr_po (name, []) = (NameSpace.base name)^" "
              |pr_po (name, S)  = String.concat
                                  (map (fn (m,n) =>(NameSpace.base name)^"_"^
                                                   (Int.toString n)^" ")
                                       (S ~~ (1 upto (length S))))   
           val dom = map pr_po (Symtab.dest PO_tab)
           fun is str = Library.mapfilter (fn x => if String.isPrefix str x
                                           then SOME(String.substring(str,size str,
                                                                         (size x) - 
                                                                         size str)) 
                                           else NONE) 
                                dom
           fun pr2 str = (let val H = is str 
                          in  if null H then ()
                              else (pr1 str; writeln (String.concat H))
                          end)
    in  Library.seq (pr2 o fst) (Symtab.dest FMethod.PO_classifier);
        writeln ("FMethod Package Content:"); FMethod.print method_state  
    end


   structure PO_Data : THEORY_DATA_ARGS =
   struct
     val name = "PO-mgr-state"
     type T = state
     val empty = mt_state
     fun copy T = T
     fun prep_ext T = T
     fun extend T = T
     val merge  = merge_state
     val print  = print_state
   end;

   structure PO_state_management = TheoryDataFun(PO_Data);
   val PO_state_setup = [PO_state_management.init]

   val get_state = PO_state_management.get

   fun set_path path = 
       let fun f (MkState{act_path,method_state,PO_prover_tab,PO_tab,ran_PO_tab}) =  
                 (MkState{act_path=path,method_state=method_state,PO_prover_tab=PO_prover_tab,
                          PO_tab=PO_tab,ran_PO_tab=ran_PO_tab})
       in  PO_state_management.map f end

   fun get_path thy =
       let val MkState{act_path, ...} = PO_state_management.get thy
       in  act_path end


   fun set_content ct = 
       let fun f (MkState{act_path,method_state,PO_prover_tab,PO_tab,ran_PO_tab}) =  
                 (MkState{act_path=act_path,method_state=ct,PO_prover_tab=PO_prover_tab,
                          PO_tab=PO_tab,ran_PO_tab=ran_PO_tab})
       in  PO_state_management.map f end
  
   fun get_content thy =
       let val MkState{method_state, ...} = PO_state_management.get thy
       in  method_state end
 
   fun set_prover_tab tab = 
       let fun f (MkState{act_path,method_state,PO_prover_tab,PO_tab,ran_PO_tab}) =  
                 (MkState{act_path=act_path,method_state=method_state,PO_prover_tab=tab,
                          PO_tab=PO_tab,ran_PO_tab=ran_PO_tab})
       in  PO_state_management.map f end


   fun get_prover_tab thy =
       let val MkState{PO_prover_tab, ...} = PO_state_management.get thy
       in  PO_prover_tab end

   fun get_name_of_PO ct thy = 
       let val MkState{act_path,method_state,PO_prover_tab,PO_tab,ran_PO_tab} = 
                       PO_state_management.get thy 
       in  Ctermtab.lookup ran_PO_tab ct
       end 


   fun get_status_of_PO  ct thy =
       (* PRE: ct is a declared PO *)
       let val p = the(get_name_of_PO ct thy)
           val SOME(path,class,core,n) = dest_PO_name p
           val MkState{act_path,method_state,PO_prover_tab,PO_tab,ran_PO_tab} = 
                                PO_state_management.get thy 
           val SOME ll = Symtab.lookup PO_tab (mk_PO_name_base(path,class,core))
           val (_,status) = List.nth(ll,n-1)
       in  SOME status end;


   fun get_PO_from_name name thy = 
       let val (path,class,core,n) = case dest_PO_name name of
                                       NONE => error("illegal name format:" ^ name)
				     | SOME x => x
           val MkState{act_path,method_state,PO_prover_tab,PO_tab,ran_PO_tab} = 
                                PO_state_management.get thy 
           val ll = Symtab.lookup PO_tab (mk_PO_name_base(path,class,core))
       in  case ll of 
             SOME ll => if n <= length ll then (fst(List.nth(ll,n-1)))
                        else error"get_PO_from_name: undeclared PO name (index)"
           | NONE    => error"get_PO_from_name: undeclared PO name"
       end


   fun set_status_of_PO ct po_attempt thy =
         (* PRE: ct is a declared PO *)
       let val p = case (get_name_of_PO ct thy) of
                     NONE =>  error("unknown proof obligation:" ^ 
		                    (Sign.string_of_term thy (term_of ct)))
                   | SOME p => p
           val SOME(path,class,core,n) = dest_PO_name p
           val poname_base = mk_PO_name_base(path,class,core) 
           val MkState{act_path,method_state,PO_prover_tab,PO_tab,ran_PO_tab} = 
                               PO_state_management.get thy 
           val SOME ll = Symtab.lookup PO_tab poname_base
           val ll'     = map_nth_elem (n-1) 
                                      (fn (ct,_) => (ct, SOME po_attempt))
                                      (ll)
           val PO_tab' = Symtab.update(poname_base,ll')(PO_tab)
           val state'  = MkState{act_path=act_path,method_state=method_state,
                                 PO_prover_tab=PO_prover_tab,
                                 PO_tab=PO_tab',ran_PO_tab=ran_PO_tab} 
       in  PO_state_management.put state' thy
       end




   fun declare_PO (path_O, class, core) (ct) (thy) =
                           (* PRE : path_0 must be path, class a classifier.
			            cterm must be of type prop.
				    It can contain free vars and
				    free typevars.
			      POST: Generates unique name
			            (cterm decides !!!) and 
				    entry in PO_tab *)
       let val _  = if isClassifier class 
                    then ()
                    else error "declare_PO: not leagal classifier"
           val MkState{act_path,method_state,PO_prover_tab,PO_tab,ran_PO_tab} = 
                       PO_state_management.get thy 
           val path =(case path_O of
                        SOME(p) => p
                      | NONE    => act_path)
       in case Ctermtab.lookup ran_PO_tab ct of
           SOME _ => thy (* PO exists already *)
         | NONE   =>(let val poname_base = mk_PO_name_base(path,class,core) 
                         val po_s   = case Symtab.lookup PO_tab poname_base of
                                        NONE => []
                                       |SOME p => p
                         val poname = poname_base^"_"^
                                      (Int.toString (length po_s + 1))
                         val ran_PO_tab' = Ctermtab.update(ct,poname)
                                                          (ran_PO_tab)
                         val PO_tab' = Symtab.update(poname_base,
                                                     po_s@[(ct,NONE)])
                                                    (PO_tab) 
                     in  PO_state_management.put 
                         (MkState{act_path=act_path,method_state=method_state,
                                  PO_prover_tab=PO_prover_tab,
                                  PO_tab=PO_tab',ran_PO_tab=ran_PO_tab'}) thy
                     end)
      end  


    fun prove_i_PO discharge_automatic name thy =
    let val MkState{act_path,method_state,PO_prover_tab,PO_tab,ran_PO_tab} = 
                       PO_state_management.get thy 
        val (path,class,core,n) = case dest_PO_name name of
	                            SOME x => x
			          | NONE => error"illegal format of PO name"
        val poname_base = mk_PO_name_base(path,class,core)
        val ll = case Symtab.lookup PO_tab poname_base of 
                   NONE => error("undeclared proof obligation: "^name)
                 | SOME ll => ll
        val (po,_) = List.nth(ll,n-1)
	val name' = mk_PO_name(Context.theory_name thy, class,core,n)
        val thy' = set_status_of_PO po name' thy 
        val tac = case Symtab.lookup PO_prover_tab class of
                    NONE => no_tac
                  | SOME tac => tac
        fun nthm () = prove_goalw_cterm [] po (fn prems => [cut_facts_tac prems 1,tac]) 
    in  if discharge_automatic 
	then (bind_thm(name',nthm()); thy')
        else (goalw_cterm [] (po);thy')
    end


    fun prove_PO name thy =
    let val ct = get_PO_from_name name thy
        val y' = ("",[])
        val w' = [(((* NameSpace.base *) name,[]),[(term_of ct,([],[]))])]
    in  (Proof.theorem_i Drule.lemmaK (K (K I)) (SOME "") y' w' o 
         ProofContext.init) thy 
    end

    fun gen_store_PO_attempt opt_lemmaname name thy =
    let val ct = get_PO_from_name name thy
        val (path,class,core,n) = case dest_PO_name name of
	                            SOME x => x
			          | NONE => error"illegal format of PO name"
	val name'  = case opt_lemmaname of
                      NONE => mk_PO_name(Context.theory_name thy,class,core,n)
                              (* generic name *)
                     |SOME x=>(Context.theory_name thy^NameSpace.separator^x)
                              (* user controlled name *)   
    in  set_status_of_PO ct name' thy end 


   fun list_POs filtr thy =
       let val _ = if forall isClassifier filtr then ()
                   else error"not a classifier"
           val MkState{act_path,method_state,PO_prover_tab,PO_tab,ran_PO_tab} = 
                               PO_state_management.get thy
           fun isExcluded name_base = let val (_,class,_,_)=
                                              the(dest_PO_name(name_base^"_1"))
                                      in class mem filtr end 
           fun expand (nb,S) = if isExcluded nb
                               then []
                               else map (fn ((_,stat),x)=>
                                             (nb^"_"^(Int.toString x)^" ",stat)) 
                                        (S ~~ (1 upto length S))
           val cc = Library.flat (map expand (Symtab.dest PO_tab))
       in  (map fst cc) end


   fun check_statistics ignore_class_list thy =  
       let val MkState{act_path,method_state,PO_prover_tab,PO_tab,ran_PO_tab} = 
                               PO_state_management.get thy
           fun expand (nb,S) = map (fn ((_,stat),x)=>(nb^"_"^(Int.toString x),stat)) 
                                   (S ~~ (1 upto length S))
           val cc = Library.flat (map expand (Symtab.dest PO_tab))
           fun check (name,status) = case status of
                                      NONE => true (* no proof attempt *)
                                    | SOME p => ((Goals.get_thm thy p; false)  
                                                (* Has theorem really been
                                                   proven, i.e. has the proof
                                                   been completed? 
                                                   At the moment, there is no
                                                   check for sorry ... *)
                                                 handle _ => true)
           val not_discharged = filter check cc
           val _ = let val classes = (map fst (Symtab.dest FMethod.PO_classifier)) 
                   in  if forall(fn x => x mem classes) ignore_class_list
                       then ()
                       else error"Undefined PO class!"
                   end
           fun is_name_of_class class n = let val (_,cl,_,_)=the(dest_PO_name n)
                                          in cl = class end
           fun is_PO_in_class class = (class, 
                                       filter ((is_name_of_class class) o fst) 
                                              not_discharged)
           val class_nds = map is_PO_in_class ignore_class_list
           fun sum [] = 0 | sum (a::R) = a + (sum R)
           val no_ignored_nd  = sum (map (length o snd) class_nds) 
           val no_nd = (length not_discharged) - no_ignored_nd  
           fun pr3 (class, []) = ()
              |pr3 (class, S) = (pr1 class; Library.seq (fn (n,_) => writeln n) S)  
       in  writeln("Statistics of Proof-Obligations:");
           writeln("================================");
           if no_ignored_nd > 0 
           then writeln("There are "^(Int.toString no_ignored_nd)^
                        " unproven proof-obligations (ignored due to filtering). ")
           else ();
           if no_nd > 0
           then error("There are "^(Int.toString no_nd)^
                      " unproven proof-obligations (can not ignore!). \n"^ 
                      "Check failed.")
           else ();
           if  no_ignored_nd <= 0 andalso no_nd <= 0
           then (writeln ("There have been "^Int.toString(length cc)^
                          " proof obligations.");
                 if length cc > 0 
                 then writeln ("All of them have been discharged.")
                 else ())
           else ()
       end     



structure P = OuterParse and K = OuterKeyword;

val show_poP =
  let val xname1 = Scan.repeat1 P.xname
      fun show_pos S thy = 
          (List.app (fn x => writeln (Sign.string_of_term thy (term_of
                                       (get_PO_from_name x thy)))) S;thy)
  in  OuterSyntax.improper_command "show_po" "print proof obligation" K.diag
      (xname1 >> (Toplevel.theory o show_pos))
  end;
val _ =  OuterSyntax.add_parsers [show_poP];


val poP =
  let fun store name  =  gen_store_PO_attempt NONE name
  in  OuterSyntax.command "po" 
                          "prove proof obligation" 
                          K.thy_goal
      (P.xname >> (fn x => (Toplevel.print 
                            o (Toplevel.theory_to_proof(prove_PO x)))))
  end;
val _ =  OuterSyntax.add_parsers [poP];


fun dischargedT prf =
    let
        val prf_state = ProofHistory.current prf;
        val thy       = Proof.theory_of prf_state;
        val name      = let
                           val goal = hd(filter(fn x=>String.isPrefix"goal" x)
                                               (map Pretty.string_of 
                                                    (Proof.pretty_state 0 
                                                             prf_state)))
                           val _::_::name::_ = if (goal = "")
                                               then ["","",""]
                                               else String.tokens 
                                                   (fn x => x = #"(" orelse 
                                                            x = #")") 
                                                    goal
                         in
                           name
                         end
        val _          = writeln name;
        val top_thm    = snd(snd(Proof.get_goal(prf_state)));
        val thy        = fst(PureThy.add_thms 
                              [((NameSpace.base name,top_thm),[])] 
                              (thy));
        val thy        = gen_store_PO_attempt NONE name thy
    in
        thy
    end


val dischargedP =
    OuterSyntax.command "discharged" 
                        "proof obligation discharged (and theorem stated)"
                        OuterKeyword.qed_global
                        (Scan.succeed (Toplevel.print3 o 
                                       (Toplevel.proof_to_theory dischargedT)));
val _ =  OuterSyntax.add_parsers [dischargedP];


val list_poP =
  let val xname1 =  Scan.optional (P.$$$ "except" |-- (Scan.repeat1 P.xname)) []
      fun list_PO S thy = (List.app writeln (list_POs S thy);thy)
  in  OuterSyntax.improper_command "list_po" "list impending proof obligations" 
      K.diag (xname1 >> (Toplevel.theory o list_PO))
  end;
val _ = OuterSyntax.add_parsers  [list_poP];
val _ = OuterSyntax.add_keywords ["except"];


val check_poP =
  let val xname1 =  Scan.optional (P.$$$ "except" |-- (Scan.repeat1 P.xname)) []
      fun check_po S thy = (check_statistics S thy; thy)
  in  OuterSyntax.improper_command "check_po" "check proof obligation" K.diag
      (xname1 >> (Toplevel.theory o check_po))
  end;   
val _ =  OuterSyntax.add_parsers [check_poP];


end (*struct*)