File ‹Isar_Interface.ML›
signature PSL_INTERFACE =
sig
val activate_isar_interface : unit -> unit;
type strategy;
val try_hard_strategy : Proof.context -> strategy option;
val try_parallel_strategy : Proof.context -> strategy option;
end;
structure PSL_Interface : PSL_INTERFACE =
struct
structure Mp = Monadic_Prover;
structure Pc = Parser_Combinator;
type strategy = Mp.str;
structure Data = Generic_Data
(
type T = strategy Symtab.table;
val empty = Symtab.empty : T;
val merge = Symtab.merge (K true);
);
fun lookup ctxt = (Symtab.lookup o Data.get) (Context.Proof ctxt);
fun update k v = Data.map (Symtab.update_new (k, v));
structure Lookup : LOOKUP =
struct
fun get_str ctxt name =
let
val some_str = lookup ctxt name : Mp.str option;
val strategy = Utils.the' (name ^ "?\nDid you really define such a strategy?\n"
^ "Also, you should not forget that PThenOne and PThenAll take *exactly* two sub-strategies!")
some_str : Mp.str;
in
strategy
end;
end;
structure PSL_Parser = mk_PSL_Parser(Lookup);
fun put_strategy (name:string, str:strategy) = update name str
|> Context.theory_map
|> Local_Theory.background_theory;
fun tokens_to_string tokens = tokens |> map Token.unparse |> String.concatWith " ";
fun string_parser_to_token_parser (symbols_parser:'a Pc.parser) = (fn (tokens:Token.T list) =>
tokens
|> tokens_to_string
|> Symbol.explode
|> symbols_parser
|> Seq.hd
|> apsnd (K ([]))) : 'a Token.parser;
fun parse_strategy_def_tokens ctxt = string_parser_to_token_parser (PSL_Parser.strategy_parser ctxt)
: (string * Mp.str) Token.parser;
val parse_and_put_strategy_def : (local_theory -> local_theory) Token.parser = fn tokens =>
let
fun get_token_parser ctxt = parse_strategy_def_tokens ctxt : (string * Mp.str) Token.parser;
fun get_token_p_result ctxt = get_token_parser ctxt tokens |> fst : string * Mp.str;
fun put_str_in_lthy (lthy:local_theory) = put_strategy (get_token_p_result lthy) lthy;
in
(put_str_in_lthy, [])
end;
fun get_monad_tactic (strategy:strategy) (proof_state:Proof.state) =
let
val core_tac = Mp.desugar strategy;
val interpret = Mp.interpret;
fun hard_timeout_in (sec:real) = Timeout.apply (seconds sec);
in
hard_timeout_in 60000.0
(interpret (Mp.eval_prim, Mp.eval_para, Mp.eval_strategic, Mp.m_equal, Mp.iddfc, (5,20))
core_tac) proof_state
end : Proof.state Mp.monad;
type trans_trans = Toplevel.transition -> Toplevel.transition;
val strategy_invocation_parser = PSL_Parser.invocation_parser : string Pc.parser;
local
infix >>=;
val op >>= = Parser_Combinator.>>=;
in
fun invocation_parser_to_trans_trans_parser (inv_p : string Pc.parser)
(get_trans_trans : string -> trans_trans) =
string_parser_to_token_parser (inv_p >>= (Pc.result o get_trans_trans)) : trans_trans Token.parser;
end;
fun get_trans_trans (strategy_name:string) =
(((Toplevel.keep_proof:(Toplevel.state -> unit) -> trans_trans)
(fn top =>
let
type log = Dynamic_Utils.log;
val lmap = Seq.map;
val context = Toplevel.context_of top : Proof.context;
val some_strategy = lookup context strategy_name;
val strategy = Utils.the' (strategy_name ^ "? You haven't defined such a strategy!")
some_strategy;
val tactic = get_monad_tactic strategy : Proof.state Mp.stttac;
val proof_state = Toplevel.proof_of top;
val results' = tactic proof_state : Proof.state Mp.monad;
val results = results' [] : (log * Proof.state) Seq.seq;
val logs = lmap fst results : log Seq.seq;
val applies = lmap Dynamic_Utils.mk_apply_script logs;
val print = writeln (case Seq.pull applies of
NONE => error "empty sequence. no proof found."
| SOME _ => Seq.hd applies);
in
print
end)
):trans_trans);
fun activate_isar_interface _ =
let
val _ = Outer_Syntax.local_theory @{command_keyword strategy} "PSL strategy definition"
parse_and_put_strategy_def;
val _ =
Outer_Syntax.command @{command_keyword find_proof}
"find_proof tries to find a proof based on high level strategies provided in advance.."
(invocation_parser_to_trans_trans_parser strategy_invocation_parser get_trans_trans);
val _ =
Outer_Syntax.command @{command_keyword try_hard}
"try_hard to find efficient proof-scripts."
(Scan.succeed (get_trans_trans "Try_Hard"))
val _ =
Outer_Syntax.command @{command_keyword try_hard_one}
"try_hard to find efficient proof-scripts."
(Scan.succeed (get_trans_trans "Try_Hard_One"))
val _ =
Outer_Syntax.command @{command_keyword try_hard_all}
"try_hard to find efficient proof-scripts."
(Scan.succeed (get_trans_trans "Try_Hard_All"))
val _ =
Outer_Syntax.command @{command_keyword try_parallel}
"try_hard to find efficient proof-scripts."
(Scan.succeed (get_trans_trans "Try_Parallel"))
in () end;
fun try_hard_strategy (ctxt:Proof.context) = lookup ctxt "Try_Hard";
fun try_parallel_strategy (ctxt:Proof.context) = lookup ctxt "Try_Parallel";
end;
PSL_Interface.activate_isar_interface ();