src/Pure/Isar/toplevel.ML
changeset 70064 f8293bf510a0
parent 70063 a9e574e2cba5
child 70067 0cb8753bdb50
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sat Mar 09 10:31:20 2019 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Mar 09 13:19:13 2019 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4    exception UNDEF
     1.5    type state
     1.6    val theory_toplevel: theory -> state
     1.7 -  val toplevel: state
     1.8 +  val init: unit -> state
     1.9    val is_toplevel: state -> bool
    1.10    val is_theory: state -> bool
    1.11    val is_proof: state -> bool
    1.12 @@ -101,6 +101,8 @@
    1.13  (* datatype node *)
    1.14  
    1.15  datatype node =
    1.16 +  Toplevel
    1.17 +    (*toplevel outside of theory body*) |
    1.18    Theory of generic_theory
    1.19      (*global or local theory*) |
    1.20    Proof of Proof_Node.T * ((Proof.context -> generic_theory) * generic_theory)
    1.21 @@ -112,68 +114,86 @@
    1.22  val proof_node = fn Proof (prf, _) => SOME prf | _ => NONE;
    1.23  val skipped_proof_node = fn Skipped_Proof _ => true | _ => false;
    1.24  
    1.25 -fun cases_node f _ (Theory gthy) = f gthy
    1.26 -  | cases_node _ g (Proof (prf, _)) = g (Proof_Node.current prf)
    1.27 -  | cases_node f _ (Skipped_Proof (_, (gthy, _))) = f gthy;
    1.28 +fun cases_node f _ _ Toplevel = f ()
    1.29 +  | cases_node _ g _ (Theory gthy) = g gthy
    1.30 +  | cases_node _ _ h (Proof (prf, _)) = h (Proof_Node.current prf)
    1.31 +  | cases_node _ g _ (Skipped_Proof (_, (gthy, _))) = g gthy;
    1.32 +
    1.33 +fun cases_proper_node g h = cases_node (fn () => raise UNDEF) g h;
    1.34 +
    1.35 +val get_theory = cases_node (K NONE) (SOME o Context.theory_of) (SOME o Proof.theory_of);
    1.36  
    1.37  
    1.38  (* datatype state *)
    1.39  
    1.40 -type node_presentation = node * Proof.context;  (*node with presentation context*)
    1.41 -fun node_presentation0 node = (node, cases_node Context.proof_of Proof.context_of node);
    1.42 +type node_presentation = node * Proof.context;
    1.43  
    1.44 -datatype state = State of node_presentation option * node_presentation option; (*current, previous*)
    1.45 +fun node_presentation0 node =
    1.46 +  (node, cases_proper_node Context.proof_of Proof.context_of node);
    1.47  
    1.48 -fun theory_toplevel thy = State (SOME (node_presentation0 (Theory (Context.Theory thy))), NONE);
    1.49 +datatype state =
    1.50 +  State of node_presentation * theory option;
    1.51 +    (*current node with presentation context, previous theory*)
    1.52  
    1.53 -val toplevel = State (NONE, NONE);
    1.54 +fun node_of (State ((node, _), _)) = node;
    1.55 +fun previous_theory_of (State (_, prev_thy)) = prev_thy;
    1.56  
    1.57 -fun is_toplevel (State (NONE, _)) = true
    1.58 -  | is_toplevel _ = false;
    1.59 +fun theory_toplevel thy =
    1.60 +  State (node_presentation0 (Theory (Context.Theory thy)), NONE);
    1.61  
    1.62 -fun level (State (NONE, _)) = 0
    1.63 -  | level (State (SOME (Theory _, _), _)) = 0
    1.64 -  | level (State (SOME (Proof (prf, _), _), _)) = Proof.level (Proof_Node.current prf)
    1.65 -  | level (State (SOME (Skipped_Proof (d, _), _), _)) = d + 1;   (*different notion of proof depth!*)
    1.66 +fun init () =
    1.67 +  let val thy0 = Theory.get_pure () handle Fail _ => Context.the_global_context ();
    1.68 +  in State ((Toplevel, Proof_Context.init_global thy0), NONE) end;
    1.69 +
    1.70 +fun level state =
    1.71 +  (case node_of state of
    1.72 +    Toplevel => 0
    1.73 +  | Theory _ => 0
    1.74 +  | Proof (prf, _) => Proof.level (Proof_Node.current prf)
    1.75 +  | Skipped_Proof (d, _) => d + 1);   (*different notion of proof depth!*)
    1.76  
    1.77 -fun str_of_state (State (NONE, SOME (Theory (Context.Theory thy), _))) =
    1.78 -      "at top level, result theory " ^ quote (Context.theory_name thy)
    1.79 -  | str_of_state (State (NONE, _)) = "at top level"
    1.80 -  | str_of_state (State (SOME (Theory (Context.Theory _), _), _)) = "in theory mode"
    1.81 -  | str_of_state (State (SOME (Theory (Context.Proof _), _), _)) = "in local theory mode"
    1.82 -  | str_of_state (State (SOME (Proof _, _), _)) = "in proof mode"
    1.83 -  | str_of_state (State (SOME (Skipped_Proof _, _), _)) = "in skipped proof mode";
    1.84 +fun str_of_state state =
    1.85 +  (case node_of state of
    1.86 +    Toplevel =>
    1.87 +      (case previous_theory_of state of
    1.88 +        NONE => "at top level"
    1.89 +      | SOME thy => "at top level, result theory " ^ quote (Context.theory_name thy))
    1.90 +  | Theory (Context.Theory _) => "in theory mode"
    1.91 +  | Theory (Context.Proof _) => "in local theory mode"
    1.92 +  | Proof _ => "in proof mode"
    1.93 +  | Skipped_Proof _ => "in skipped proof mode");
    1.94  
    1.95  
    1.96  (* current node *)
    1.97  
    1.98 -fun node_of (State (NONE, _)) = raise UNDEF
    1.99 -  | node_of (State (SOME (node, _), _)) = node;
   1.100 +fun is_toplevel state = (case node_of state of Toplevel => true | _ => false);
   1.101  
   1.102 -fun is_theory state = not (is_toplevel state) andalso is_some (theory_node (node_of state));
   1.103 -fun is_proof state = not (is_toplevel state) andalso is_some (proof_node (node_of state));
   1.104 -fun is_skipped_proof state = not (is_toplevel state) andalso skipped_proof_node (node_of state);
   1.105 +fun is_theory state =
   1.106 +  not (is_toplevel state) andalso is_some (theory_node (node_of state));
   1.107  
   1.108 -fun node_case f g state = cases_node f g (node_of state);
   1.109 +fun is_proof state =
   1.110 +  not (is_toplevel state) andalso is_some (proof_node (node_of state));
   1.111  
   1.112 -fun previous_theory_of (State (_, NONE)) = NONE
   1.113 -  | previous_theory_of (State (_, SOME (prev, _))) =
   1.114 -      SOME (cases_node Context.theory_of Proof.theory_of prev);
   1.115 +fun is_skipped_proof state =
   1.116 +  not (is_toplevel state) andalso skipped_proof_node (node_of state);
   1.117  
   1.118 -val context_of = node_case Context.proof_of Proof.context_of;
   1.119 -val generic_theory_of = node_case I (Context.Proof o Proof.context_of);
   1.120 -val theory_of = node_case Context.theory_of Proof.theory_of;
   1.121 -val proof_of = node_case (fn _ => error "No proof state") I;
   1.122 +fun proper_node_of state = if is_toplevel state then raise UNDEF else node_of state;
   1.123 +fun proper_node_case f g state = cases_proper_node f g (proper_node_of state);
   1.124 +
   1.125 +val context_of = proper_node_case Context.proof_of Proof.context_of;
   1.126 +val generic_theory_of = proper_node_case I (Context.Proof o Proof.context_of);
   1.127 +val theory_of = proper_node_case Context.theory_of Proof.theory_of;
   1.128 +val proof_of = proper_node_case (fn _ => error "No proof state") I;
   1.129  
   1.130  fun proof_position_of state =
   1.131 -  (case node_of state of
   1.132 +  (case proper_node_of state of
   1.133      Proof (prf, _) => Proof_Node.position prf
   1.134    | _ => ~1);
   1.135  
   1.136 -fun is_end_theory (State (NONE, SOME (Theory (Context.Theory _), _))) = true
   1.137 +fun is_end_theory (State ((Toplevel, _), SOME _)) = true
   1.138    | is_end_theory _ = false;
   1.139  
   1.140 -fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy), _))) = thy
   1.141 +fun end_theory _ (State ((Toplevel, _), SOME thy)) = thy
   1.142    | end_theory pos _ = error ("Malformed theory" ^ Position.here pos);
   1.143  
   1.144  
   1.145 @@ -185,13 +205,7 @@
   1.146    fun init _ = NONE;
   1.147  );
   1.148  
   1.149 -fun presentation_context0 state =
   1.150 -  (case state of
   1.151 -    State (SOME (_, ctxt), _) => ctxt
   1.152 -  | State (NONE, _) =>
   1.153 -      (case try Theory.get_pure () of
   1.154 -        SOME thy => Proof_Context.init_global thy
   1.155 -      | NONE => raise UNDEF));
   1.156 +fun presentation_context0 (State ((_, pr_ctxt), _)) = pr_ctxt;
   1.157  
   1.158  fun presentation_context (state as State (current, _)) =
   1.159    presentation_context0 state
   1.160 @@ -199,31 +213,31 @@
   1.161  
   1.162  fun presentation_state ctxt =
   1.163    (case Presentation_State.get ctxt of
   1.164 -    NONE => State (SOME (node_presentation0 (Theory (Context.Proof ctxt))), NONE)
   1.165 +    NONE => State (node_presentation0 (Theory (Context.Proof ctxt)), NONE)
   1.166    | SOME state => state);
   1.167  
   1.168  
   1.169  (* print state *)
   1.170  
   1.171  fun pretty_context state =
   1.172 -  (case try node_of state of
   1.173 -    NONE => []
   1.174 -  | SOME node =>
   1.175 -      let
   1.176 -        val gthy =
   1.177 -          (case node of
   1.178 -            Theory gthy => gthy
   1.179 -          | Proof (_, (_, gthy)) => gthy
   1.180 -          | Skipped_Proof (_, (_, gthy)) => gthy);
   1.181 -        val lthy = Context.cases Named_Target.theory_init I gthy;
   1.182 -      in Local_Theory.pretty lthy end);
   1.183 +  if is_toplevel state then []
   1.184 +  else
   1.185 +    let
   1.186 +      val gthy =
   1.187 +        (case node_of state of
   1.188 +          Toplevel => raise Match
   1.189 +        | Theory gthy => gthy
   1.190 +        | Proof (_, (_, gthy)) => gthy
   1.191 +        | Skipped_Proof (_, (_, gthy)) => gthy);
   1.192 +      val lthy = Context.cases Named_Target.theory_init I gthy;
   1.193 +    in Local_Theory.pretty lthy end;
   1.194  
   1.195  fun pretty_state state =
   1.196 -  (case try node_of state of
   1.197 -    NONE => []
   1.198 -  | SOME (Theory _) => []
   1.199 -  | SOME (Proof (prf, _)) => Proof.pretty_state (Proof_Node.current prf)
   1.200 -  | SOME (Skipped_Proof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]);
   1.201 +  (case node_of state of
   1.202 +    Toplevel => []
   1.203 +  | Theory _ => []
   1.204 +  | Proof (prf, _) => Proof.pretty_state (Proof_Node.current prf)
   1.205 +  | Skipped_Proof (d, _) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]);
   1.206  
   1.207  val string_of_state = pretty_state #> Pretty.chunks #> Pretty.string_of;
   1.208  
   1.209 @@ -242,8 +256,8 @@
   1.210  fun apply_transaction f g node =
   1.211    let
   1.212      val node_pr = node_presentation0 node;
   1.213 -    val context = cases_node I (Context.Proof o Proof.context_of) node;
   1.214 -    fun state_error e node_pr' = (State (SOME node_pr', SOME node_pr), e);
   1.215 +    val context = cases_proper_node I (Context.Proof o Proof.context_of) node;
   1.216 +    fun state_error e node_pr' = (State (node_pr', get_theory node), e);
   1.217  
   1.218      val (result, err) =
   1.219        node
   1.220 @@ -256,13 +270,6 @@
   1.221      | SOME exn => raise FAILURE (result, exn))
   1.222    end;
   1.223  
   1.224 -val exit_transaction =
   1.225 -  apply_transaction
   1.226 -    ((fn Theory (Context.Theory thy) => Theory (Context.Theory (Theory.end_theory thy))
   1.227 -       | node => node) #> node_presentation0)
   1.228 -    (K ())
   1.229 -  #> (fn State (node_pr', _) => State (NONE, node_pr'));
   1.230 -
   1.231  
   1.232  (* primitive transitions *)
   1.233  
   1.234 @@ -278,14 +285,20 @@
   1.235  
   1.236  local
   1.237  
   1.238 -fun apply_tr _ (Init f) (State (NONE, _)) =
   1.239 +fun apply_tr _ (Init f) (State ((Toplevel, _), _)) =
   1.240        let val node = Theory (Context.Theory (Runtime.controlled_execution NONE f ()))
   1.241 -      in State (SOME (node_presentation0 node), NONE) end
   1.242 -  | apply_tr _ Exit (State (SOME (node as Theory (Context.Theory _), _), _)) =
   1.243 -      exit_transaction node
   1.244 +      in State (node_presentation0 node, NONE) end
   1.245 +  | apply_tr _ Exit (State ((node as Theory (Context.Theory thy), _), _)) =
   1.246 +      let
   1.247 +        val State ((node', pr_ctxt), _) =
   1.248 +          node |> apply_transaction
   1.249 +            (fn _ => node_presentation0 (Theory (Context.Theory (Theory.end_theory thy))))
   1.250 +            (K ());
   1.251 +      in State ((Toplevel, pr_ctxt), get_theory node') end
   1.252    | apply_tr int (Keep f) state =
   1.253        Runtime.controlled_execution (try generic_theory_of state) (fn x => tap (f int) x) state
   1.254 -  | apply_tr int (Transaction (f, g)) (State (SOME (node, _), _)) =
   1.255 +  | apply_tr _ (Transaction _) (State ((Toplevel, _), _)) = raise UNDEF
   1.256 +  | apply_tr int (Transaction (f, g)) (State ((node, _), _)) =
   1.257        apply_transaction (fn x => f int x) g node
   1.258    | apply_tr _ _ _ = raise UNDEF;
   1.259  
   1.260 @@ -725,10 +738,10 @@
   1.261                    {name = "Toplevel.future_proof", pos = pos_of head_tr, pri = ~1}
   1.262                    (fn () =>
   1.263                      let
   1.264 -                      val State (SOME (Proof (prf, (_, orig_gthy)), _), prev) = st';
   1.265 +                      val State ((Proof (prf, (_, orig_gthy)), _), prev_thy) = st';
   1.266                        val node' = Proof (Proof_Node.apply (K state) prf, (finish, orig_gthy));
   1.267                        val (result, result_state) =
   1.268 -                        State (SOME (node_presentation0 node'), prev)
   1.269 +                        State (node_presentation0 node', prev_thy)
   1.270                          |> fold_map (element_result keywords) body_elems ||> command end_tr;
   1.271                      in (Result_List result, presentation_context0 result_state) end))
   1.272                #> (fn (res, state') => state' |> put_result (Result_Future res));