src/Provers/classical.ML
changeset 42439 9efdd0af15ac
parent 42361 23f352990944
child 42790 e07e56300faa
equal deleted inserted replaced
42438:cf963c834435 42439:9efdd0af15ac
    35 
    35 
    36 signature BASIC_CLASSICAL =
    36 signature BASIC_CLASSICAL =
    37 sig
    37 sig
    38   type claset
    38   type claset
    39   val empty_cs: claset
    39   val empty_cs: claset
    40   val print_cs: claset -> unit
    40   val print_cs: Proof.context -> claset -> unit
    41   val rep_cs:
    41   val rep_cs:
    42     claset -> {safeIs: thm list, safeEs: thm list,
    42     claset -> {safeIs: thm list, safeEs: thm list,
    43                  hazIs: thm list, hazEs: thm list,
    43                  hazIs: thm list, hazEs: thm list,
    44                  swrappers: (string * wrapper) list,
    44                  swrappers: (string * wrapper) list,
    45                  uwrappers: (string * wrapper) list,
    45                  uwrappers: (string * wrapper) list,
   256      safep_netpair = empty_netpair,
   256      safep_netpair = empty_netpair,
   257      haz_netpair   = empty_netpair,
   257      haz_netpair   = empty_netpair,
   258      dup_netpair   = empty_netpair,
   258      dup_netpair   = empty_netpair,
   259      xtra_netpair  = empty_netpair};
   259      xtra_netpair  = empty_netpair};
   260 
   260 
   261 fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...}) =
   261 fun print_cs ctxt (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...}) =
   262   let val pretty_thms = map Display.pretty_thm_without_context in
   262   let val pretty_thms = map (Display.pretty_thm ctxt) in
   263     [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
   263     [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
   264       Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs),
   264       Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs),
   265       Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs),
   265       Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs),
   266       Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs),
   266       Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs),
   267       Pretty.strs ("safe wrappers:" :: map #1 swrappers),
   267       Pretty.strs ("safe wrappers:" :: map #1 swrappers),
  1016 
  1016 
  1017 val _ =
  1017 val _ =
  1018   Outer_Syntax.improper_command "print_claset" "print context of Classical Reasoner"
  1018   Outer_Syntax.improper_command "print_claset" "print context of Classical Reasoner"
  1019     Keyword.diag
  1019     Keyword.diag
  1020     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
  1020     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
  1021       Toplevel.keep (print_cs o claset_of o Toplevel.context_of)));
  1021       Toplevel.keep (fn state =>
       
  1022         let val ctxt = Toplevel.context_of state
       
  1023         in print_cs ctxt (claset_of ctxt) end)));
  1022 
  1024 
  1023 end;
  1025 end;