equal
deleted
inserted
replaced
90 val detect_closure_state: thm -> bool |
90 val detect_closure_state: thm -> bool |
91 val STATIC: (unit -> unit) -> context_tactic |
91 val STATIC: (unit -> unit) -> context_tactic |
92 val RUNTIME: context_tactic -> context_tactic |
92 val RUNTIME: context_tactic -> context_tactic |
93 val sleep: Time.time -> context_tactic |
93 val sleep: Time.time -> context_tactic |
94 val evaluate: text -> Proof.context -> method |
94 val evaluate: text -> Proof.context -> method |
|
95 val evaluate_runtime: text -> Proof.context -> method |
95 type modifier = {init: Proof.context -> Proof.context, attribute: attribute, pos: Position.T} |
96 type modifier = {init: Proof.context -> Proof.context, attribute: attribute, pos: Position.T} |
96 val modifier: attribute -> Position.T -> modifier |
97 val modifier: attribute -> Position.T -> modifier |
97 val old_section_parser: bool Config.T |
98 val old_section_parser: bool Config.T |
98 val sections: modifier parser list -> unit context_parser |
99 val sections: modifier parser list -> unit context_parser |
99 type text_range = text * Position.range |
100 type text_range = text * Position.range |
101 val position: text_range option -> Position.T |
102 val position: text_range option -> Position.T |
102 val reports_of: text_range -> Position.report list |
103 val reports_of: text_range -> Position.report list |
103 val report: text_range -> unit |
104 val report: text_range -> unit |
104 val parser: int -> text_range parser |
105 val parser: int -> text_range parser |
105 val parse: text_range parser |
106 val parse: text_range parser |
|
107 val read: Proof.context -> Token.src -> text |
|
108 val read_closure: Proof.context -> Token.src -> text * Token.src |
|
109 val read_closure_input: Proof.context -> Input.source -> text * Token.src |
|
110 val text_closure: text context_parser |
106 end; |
111 end; |
107 |
112 |
108 structure Method: METHOD = |
113 structure Method: METHOD = |
109 struct |
114 struct |
110 |
115 |
573 | eval (Source src) = eval0 (method_cmd ctxt src ctxt) |
578 | eval (Source src) = eval0 (method_cmd ctxt src ctxt) |
574 | eval (Combinator (_, c, txts)) = combinator c (map eval txts); |
579 | eval (Combinator (_, c, txts)) = combinator c (map eval txts); |
575 in eval text o Seq.Result end; |
580 in eval text o Seq.Result end; |
576 |
581 |
577 end; |
582 end; |
|
583 |
|
584 fun evaluate_runtime text ctxt = |
|
585 let |
|
586 val text' = |
|
587 text |> (map_source o map o Token.map_facts) |
|
588 (fn SOME name => |
|
589 (case Proof_Context.lookup_fact ctxt name of |
|
590 SOME {dynamic = true, thms} => K thms |
|
591 | _ => I) |
|
592 | NONE => I); |
|
593 val ctxt' = Config.put closure false ctxt; |
|
594 in fn facts => RUNTIME (fn st => evaluate text' ctxt' facts st) end; |
578 |
595 |
579 |
596 |
580 |
597 |
581 (** concrete syntax **) |
598 (** concrete syntax **) |
582 |
599 |
739 in Scan.trace meth >> (fn (m, toks) => (m, Token.range_of toks)) end; |
756 in Scan.trace meth >> (fn (m, toks) => (m, Token.range_of toks)) end; |
740 |
757 |
741 val parse = parser 4; |
758 val parse = parser 4; |
742 |
759 |
743 end; |
760 end; |
|
761 |
|
762 |
|
763 (* read method text *) |
|
764 |
|
765 fun read ctxt src = |
|
766 (case Scan.read Token.stopper (Parse.!!! (parser 0 --| Scan.ahead Parse.eof)) src of |
|
767 SOME (text, range) => |
|
768 if checked_text text then text |
|
769 else (report (text, range); check_text ctxt text) |
|
770 | NONE => error ("Failed to parse method" ^ Position.here (#1 (Token.range_of src)))); |
|
771 |
|
772 fun read_closure ctxt src0 = |
|
773 let |
|
774 val src1 = map Token.init_assignable src0; |
|
775 val text = read ctxt src1 |> map_source (method_closure ctxt); |
|
776 val src2 = map Token.closure src1; |
|
777 in (text, src2) end; |
|
778 |
|
779 fun read_closure_input ctxt = |
|
780 Input.source_explode #> |
|
781 Token.read_no_commands (Thy_Header.get_keywords' ctxt) (Scan.one Token.not_eof) #> |
|
782 read_closure ctxt; |
|
783 |
|
784 val text_closure = |
|
785 Args.context -- Scan.lift (Parse.token Parse.text) >> (fn (ctxt, tok) => |
|
786 (case Token.get_value tok of |
|
787 SOME (Token.Source src) => read ctxt src |
|
788 | _ => |
|
789 let |
|
790 val (text, src) = read_closure_input ctxt (Token.input_of tok); |
|
791 val _ = Token.assign (SOME (Token.Source src)) tok; |
|
792 in text end)); |
744 |
793 |
745 |
794 |
746 (* theory setup *) |
795 (* theory setup *) |
747 |
796 |
748 val _ = Theory.setup |
797 val _ = Theory.setup |
790 (fn (quant, i) => K (SIMPLE_METHOD'' quant (rotate_tac i)))) |
839 (fn (quant, i) => K (SIMPLE_METHOD'' quant (rotate_tac i)))) |
791 "rotate assumptions of goal" #> |
840 "rotate assumptions of goal" #> |
792 setup @{binding tactic} (parse_tactic >> (K o METHOD)) |
841 setup @{binding tactic} (parse_tactic >> (K o METHOD)) |
793 "ML tactic as proof method" #> |
842 "ML tactic as proof method" #> |
794 setup @{binding raw_tactic} (parse_tactic >> (fn tac => fn _ => CONTEXT_TACTIC o tac)) |
843 setup @{binding raw_tactic} (parse_tactic >> (fn tac => fn _ => CONTEXT_TACTIC o tac)) |
795 "ML tactic as raw proof method"); |
844 "ML tactic as raw proof method" #> |
|
845 setup @{binding use} |
|
846 (Attrib.thms -- (Scan.lift (Parse.$$$ "in") |-- text_closure) >> |
|
847 (fn (thms, text) => fn ctxt => fn _ => evaluate_runtime text ctxt thms)) |
|
848 "indicate method facts and context for method expression"); |
796 |
849 |
797 |
850 |
798 (*final declarations of this structure!*) |
851 (*final declarations of this structure!*) |
799 val unfold = unfold_meth; |
852 val unfold = unfold_meth; |
800 val fold = fold_meth; |
853 val fold = fold_meth; |