# HG changeset patch # User wenzelm # Date 1257192221 -3600 # Node ID 5b499f36dd259e1ca8a6aa74dc51dee8b130f45b # Parent bb3a5fa94a91fe02f58569ea473a39e6aa8823e2 modernized structure Proof_Node; diff -r bb3a5fa94a91 -r 5b499f36dd25 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Mon Nov 02 20:57:48 2009 +0100 +++ b/src/Pure/Isar/isar_syn.ML Mon Nov 02 21:03:41 2009 +0100 @@ -685,7 +685,7 @@ OuterSyntax.command "proof" "backward proof" (K.tag_proof K.prf_block) (Scan.option Method.parse >> (fn m => Toplevel.print o - Toplevel.actual_proof (ProofNode.applys (Proof.proof m)) o + Toplevel.actual_proof (Proof_Node.applys (Proof.proof m)) o Toplevel.skip_proof (fn i => i + 1))); @@ -720,7 +720,7 @@ val _ = OuterSyntax.command "back" "backtracking of proof command" (K.tag_proof K.prf_script) - (Scan.succeed (Toplevel.print o Toplevel.actual_proof ProofNode.back o Toplevel.skip_proof I)); + (Scan.succeed (Toplevel.print o Toplevel.actual_proof Proof_Node.back o Toplevel.skip_proof I)); (* nested commands *) diff -r bb3a5fa94a91 -r 5b499f36dd25 src/Pure/Isar/proof_node.ML --- a/src/Pure/Isar/proof_node.ML Mon Nov 02 20:57:48 2009 +0100 +++ b/src/Pure/Isar/proof_node.ML Mon Nov 02 21:03:41 2009 +0100 @@ -15,36 +15,36 @@ val apply: (Proof.state -> Proof.state) -> T -> T end; -structure ProofNode: PROOF_NODE = +structure Proof_Node: PROOF_NODE = struct (* datatype *) -datatype T = ProofNode of +datatype T = Proof_Node of (Proof.state * (*first result*) Proof.state Seq.seq) * (*alternative results*) int; (*linear proof position*) -fun init st = ProofNode ((st, Seq.empty), 0); +fun init st = Proof_Node ((st, Seq.empty), 0); -fun current (ProofNode ((st, _), _)) = st; -fun position (ProofNode (_, n)) = n; +fun current (Proof_Node ((st, _), _)) = st; +fun position (Proof_Node (_, n)) = n; (* backtracking *) -fun back (ProofNode ((_, stq), n)) = +fun back (Proof_Node ((_, stq), n)) = (case Seq.pull stq of NONE => error "back: no alternatives" - | SOME res => ProofNode (res, n)); + | SOME res => Proof_Node (res, n)); (* apply transformer *) -fun applys f (ProofNode ((st, _), n)) = +fun applys f (Proof_Node ((st, _), n)) = (case Seq.pull (f st) of NONE => error "empty result sequence -- proof command failed" - | SOME res => ProofNode (res, n + 1)); + | SOME res => Proof_Node (res, n + 1)); fun apply f = applys (Seq.single o f); diff -r bb3a5fa94a91 -r 5b499f36dd25 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Mon Nov 02 20:57:48 2009 +0100 +++ b/src/Pure/Isar/toplevel.ML Mon Nov 02 21:03:41 2009 +0100 @@ -72,7 +72,7 @@ val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition val proofs: (Proof.state -> Proof.state Seq.seq) -> transition -> transition val proof: (Proof.state -> Proof.state) -> transition -> transition - val actual_proof: (ProofNode.T -> ProofNode.T) -> transition -> transition + val actual_proof: (Proof_Node.T -> Proof_Node.T) -> transition -> transition val skip_proof: (int -> int) -> transition -> transition val skip_proof_to_theory: (int -> bool) -> transition -> transition val get_id: transition -> string option @@ -121,7 +121,7 @@ datatype node = Theory of generic_theory * Proof.context option (*theory with presentation context*) | - Proof of ProofNode.T * ((Proof.context -> generic_theory) * generic_theory) + Proof of Proof_Node.T * ((Proof.context -> generic_theory) * generic_theory) (*proof node, finish, original theory*) | SkipProof of int * (generic_theory * generic_theory); (*proof depth, resulting theory, original theory*) @@ -130,7 +130,7 @@ val proof_node = fn Proof (prf, _) => SOME prf | _ => NONE; fun cases_node f _ (Theory (gthy, _)) = f gthy - | cases_node _ g (Proof (prf, _)) = g (ProofNode.current prf) + | cases_node _ g (Proof (prf, _)) = g (Proof_Node.current prf) | cases_node f _ (SkipProof (_, (gthy, _))) = f gthy; val context_node = cases_node Context.proof_of Proof.context_of; @@ -148,7 +148,7 @@ fun level (State (NONE, _)) = 0 | level (State (SOME (Theory _, _), _)) = 0 - | level (State (SOME (Proof (prf, _), _), _)) = Proof.level (ProofNode.current prf) + | level (State (SOME (Proof (prf, _), _), _)) = Proof.level (Proof_Node.current prf) | level (State (SOME (SkipProof (d, _), _), _)) = d + 1; (*different notion of proof depth!*) fun str_of_state (State (NONE, _)) = "at top level" @@ -184,7 +184,7 @@ fun proof_position_of state = (case node_of state of - Proof (prf, _) => ProofNode.position prf + Proof (prf, _) => Proof_Node.position prf | _ => raise UNDEF); val enter_proof_body = node_case (Proof.init o Context.proof_of) Proof.enter_forward; @@ -207,7 +207,7 @@ NONE => [] | SOME (Theory (gthy, _)) => if prf_only then [] else pretty_context gthy | SOME (Proof (prf, _)) => - Proof.pretty_state (ProofNode.position prf) (ProofNode.current prf) + Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf) | SOME (SkipProof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]) |> Pretty.markup_chunks Markup.state |> Pretty.writeln; @@ -450,7 +450,7 @@ fun end_proof f = transaction (fn int => (fn Proof (prf, (finish, _)) => - let val state = ProofNode.current prf in + let val state = Proof_Node.current prf in if can (Proof.assert_bottom true) state then let val ctxt' = f int state; @@ -475,7 +475,7 @@ else (); if skip andalso not schematic then SkipProof (0, (finish gthy (Proof.global_skip_proof int prf), gthy)) - else Proof (ProofNode.init prf, (finish gthy, gthy)) + else Proof (Proof_Node.init prf, (finish gthy, gthy)) end | _ => raise UNDEF)); @@ -499,12 +499,12 @@ | _ => raise UNDEF)); val present_proof = present_transaction (fn _ => - (fn Proof (prf, x) => Proof (ProofNode.apply I prf, x) + (fn Proof (prf, x) => Proof (Proof_Node.apply I prf, x) | skip as SkipProof _ => skip | _ => raise UNDEF)); fun proofs' f = transaction (fn int => - (fn Proof (prf, x) => Proof (ProofNode.applys (f int) prf, x) + (fn Proof (prf, x) => Proof (Proof_Node.applys (f int) prf, x) | skip as SkipProof _ => skip | _ => raise UNDEF)); @@ -654,7 +654,7 @@ Future.fork_pri ~1 (fn () => let val (states, result_state) = (case st' of State (SOME (Proof (_, (_, orig_gthy)), exit), prev) - => State (SOME (Proof (ProofNode.init prf, (finish, orig_gthy)), exit), prev)) + => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy)), exit), prev)) |> fold_map command_result body_trs ||> command (end_tr |> set_print false); in (states, presentation_context_of result_state) end))