clarified Toplevel.state: more explicit types;
authorwenzelm
Sat Mar 09 13:19:13 2019 +0100 (6 weeks ago ago)
changeset 70064f8293bf510a0
parent 70063 a9e574e2cba5
child 70065 dec7cc38a5dc
clarified Toplevel.state: more explicit types;
presentation context is always present, with default to Pure.thy and fall-back to Pure bootstrap theory;
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/toplevel.ML
src/Pure/PIDE/command.ML
src/Pure/PIDE/document.ML
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Mar 09 10:31:20 2019 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Mar 09 13:19:13 2019 +0100
     1.3 @@ -180,19 +180,23 @@
     1.4  
     1.5  structure Diag_State = Proof_Data
     1.6  (
     1.7 -  type T = Toplevel.state;
     1.8 -  fun init _ = Toplevel.toplevel;
     1.9 +  type T = Toplevel.state option;
    1.10 +  fun init _ = NONE;
    1.11  );
    1.12  
    1.13  fun ml_diag verbose source = Toplevel.keep (fn state =>
    1.14    let
    1.15      val opt_ctxt =
    1.16        try Toplevel.generic_theory_of state
    1.17 -      |> Option.map (Context.proof_of #> Diag_State.put state);
    1.18 +      |> Option.map (Context.proof_of #> Diag_State.put (SOME state));
    1.19      val flags = ML_Compiler.verbose verbose ML_Compiler.flags;
    1.20    in ML_Context.eval_source_in opt_ctxt flags source end);
    1.21  
    1.22 -val diag_state = Diag_State.get;
    1.23 +fun diag_state ctxt =
    1.24 +  (case Diag_State.get ctxt of
    1.25 +    SOME st => st
    1.26 +  | NONE => Toplevel.init ());
    1.27 +
    1.28  val diag_goal = Proof.goal o Toplevel.proof_of o diag_state;
    1.29  
    1.30  val _ = Theory.setup
     2.1 --- a/src/Pure/Isar/toplevel.ML	Sat Mar 09 10:31:20 2019 +0100
     2.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Mar 09 13:19:13 2019 +0100
     2.3 @@ -9,7 +9,7 @@
     2.4    exception UNDEF
     2.5    type state
     2.6    val theory_toplevel: theory -> state
     2.7 -  val toplevel: state
     2.8 +  val init: unit -> state
     2.9    val is_toplevel: state -> bool
    2.10    val is_theory: state -> bool
    2.11    val is_proof: state -> bool
    2.12 @@ -101,6 +101,8 @@
    2.13  (* datatype node *)
    2.14  
    2.15  datatype node =
    2.16 +  Toplevel
    2.17 +    (*toplevel outside of theory body*) |
    2.18    Theory of generic_theory
    2.19      (*global or local theory*) |
    2.20    Proof of Proof_Node.T * ((Proof.context -> generic_theory) * generic_theory)
    2.21 @@ -112,68 +114,86 @@
    2.22  val proof_node = fn Proof (prf, _) => SOME prf | _ => NONE;
    2.23  val skipped_proof_node = fn Skipped_Proof _ => true | _ => false;
    2.24  
    2.25 -fun cases_node f _ (Theory gthy) = f gthy
    2.26 -  | cases_node _ g (Proof (prf, _)) = g (Proof_Node.current prf)
    2.27 -  | cases_node f _ (Skipped_Proof (_, (gthy, _))) = f gthy;
    2.28 +fun cases_node f _ _ Toplevel = f ()
    2.29 +  | cases_node _ g _ (Theory gthy) = g gthy
    2.30 +  | cases_node _ _ h (Proof (prf, _)) = h (Proof_Node.current prf)
    2.31 +  | cases_node _ g _ (Skipped_Proof (_, (gthy, _))) = g gthy;
    2.32 +
    2.33 +fun cases_proper_node g h = cases_node (fn () => raise UNDEF) g h;
    2.34 +
    2.35 +val get_theory = cases_node (K NONE) (SOME o Context.theory_of) (SOME o Proof.theory_of);
    2.36  
    2.37  
    2.38  (* datatype state *)
    2.39  
    2.40 -type node_presentation = node * Proof.context;  (*node with presentation context*)
    2.41 -fun node_presentation0 node = (node, cases_node Context.proof_of Proof.context_of node);
    2.42 +type node_presentation = node * Proof.context;
    2.43  
    2.44 -datatype state = State of node_presentation option * node_presentation option; (*current, previous*)
    2.45 +fun node_presentation0 node =
    2.46 +  (node, cases_proper_node Context.proof_of Proof.context_of node);
    2.47  
    2.48 -fun theory_toplevel thy = State (SOME (node_presentation0 (Theory (Context.Theory thy))), NONE);
    2.49 +datatype state =
    2.50 +  State of node_presentation * theory option;
    2.51 +    (*current node with presentation context, previous theory*)
    2.52  
    2.53 -val toplevel = State (NONE, NONE);
    2.54 +fun node_of (State ((node, _), _)) = node;
    2.55 +fun previous_theory_of (State (_, prev_thy)) = prev_thy;
    2.56  
    2.57 -fun is_toplevel (State (NONE, _)) = true
    2.58 -  | is_toplevel _ = false;
    2.59 +fun theory_toplevel thy =
    2.60 +  State (node_presentation0 (Theory (Context.Theory thy)), NONE);
    2.61  
    2.62 -fun level (State (NONE, _)) = 0
    2.63 -  | level (State (SOME (Theory _, _), _)) = 0
    2.64 -  | level (State (SOME (Proof (prf, _), _), _)) = Proof.level (Proof_Node.current prf)
    2.65 -  | level (State (SOME (Skipped_Proof (d, _), _), _)) = d + 1;   (*different notion of proof depth!*)
    2.66 +fun init () =
    2.67 +  let val thy0 = Theory.get_pure () handle Fail _ => Context.the_global_context ();
    2.68 +  in State ((Toplevel, Proof_Context.init_global thy0), NONE) end;
    2.69 +
    2.70 +fun level state =
    2.71 +  (case node_of state of
    2.72 +    Toplevel => 0
    2.73 +  | Theory _ => 0
    2.74 +  | Proof (prf, _) => Proof.level (Proof_Node.current prf)
    2.75 +  | Skipped_Proof (d, _) => d + 1);   (*different notion of proof depth!*)
    2.76  
    2.77 -fun str_of_state (State (NONE, SOME (Theory (Context.Theory thy), _))) =
    2.78 -      "at top level, result theory " ^ quote (Context.theory_name thy)
    2.79 -  | str_of_state (State (NONE, _)) = "at top level"
    2.80 -  | str_of_state (State (SOME (Theory (Context.Theory _), _), _)) = "in theory mode"
    2.81 -  | str_of_state (State (SOME (Theory (Context.Proof _), _), _)) = "in local theory mode"
    2.82 -  | str_of_state (State (SOME (Proof _, _), _)) = "in proof mode"
    2.83 -  | str_of_state (State (SOME (Skipped_Proof _, _), _)) = "in skipped proof mode";
    2.84 +fun str_of_state state =
    2.85 +  (case node_of state of
    2.86 +    Toplevel =>
    2.87 +      (case previous_theory_of state of
    2.88 +        NONE => "at top level"
    2.89 +      | SOME thy => "at top level, result theory " ^ quote (Context.theory_name thy))
    2.90 +  | Theory (Context.Theory _) => "in theory mode"
    2.91 +  | Theory (Context.Proof _) => "in local theory mode"
    2.92 +  | Proof _ => "in proof mode"
    2.93 +  | Skipped_Proof _ => "in skipped proof mode");
    2.94  
    2.95  
    2.96  (* current node *)
    2.97  
    2.98 -fun node_of (State (NONE, _)) = raise UNDEF
    2.99 -  | node_of (State (SOME (node, _), _)) = node;
   2.100 +fun is_toplevel state = (case node_of state of Toplevel => true | _ => false);
   2.101  
   2.102 -fun is_theory state = not (is_toplevel state) andalso is_some (theory_node (node_of state));
   2.103 -fun is_proof state = not (is_toplevel state) andalso is_some (proof_node (node_of state));
   2.104 -fun is_skipped_proof state = not (is_toplevel state) andalso skipped_proof_node (node_of state);
   2.105 +fun is_theory state =
   2.106 +  not (is_toplevel state) andalso is_some (theory_node (node_of state));
   2.107  
   2.108 -fun node_case f g state = cases_node f g (node_of state);
   2.109 +fun is_proof state =
   2.110 +  not (is_toplevel state) andalso is_some (proof_node (node_of state));
   2.111  
   2.112 -fun previous_theory_of (State (_, NONE)) = NONE
   2.113 -  | previous_theory_of (State (_, SOME (prev, _))) =
   2.114 -      SOME (cases_node Context.theory_of Proof.theory_of prev);
   2.115 +fun is_skipped_proof state =
   2.116 +  not (is_toplevel state) andalso skipped_proof_node (node_of state);
   2.117  
   2.118 -val context_of = node_case Context.proof_of Proof.context_of;
   2.119 -val generic_theory_of = node_case I (Context.Proof o Proof.context_of);
   2.120 -val theory_of = node_case Context.theory_of Proof.theory_of;
   2.121 -val proof_of = node_case (fn _ => error "No proof state") I;
   2.122 +fun proper_node_of state = if is_toplevel state then raise UNDEF else node_of state;
   2.123 +fun proper_node_case f g state = cases_proper_node f g (proper_node_of state);
   2.124 +
   2.125 +val context_of = proper_node_case Context.proof_of Proof.context_of;
   2.126 +val generic_theory_of = proper_node_case I (Context.Proof o Proof.context_of);
   2.127 +val theory_of = proper_node_case Context.theory_of Proof.theory_of;
   2.128 +val proof_of = proper_node_case (fn _ => error "No proof state") I;
   2.129  
   2.130  fun proof_position_of state =
   2.131 -  (case node_of state of
   2.132 +  (case proper_node_of state of
   2.133      Proof (prf, _) => Proof_Node.position prf
   2.134    | _ => ~1);
   2.135  
   2.136 -fun is_end_theory (State (NONE, SOME (Theory (Context.Theory _), _))) = true
   2.137 +fun is_end_theory (State ((Toplevel, _), SOME _)) = true
   2.138    | is_end_theory _ = false;
   2.139  
   2.140 -fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy), _))) = thy
   2.141 +fun end_theory _ (State ((Toplevel, _), SOME thy)) = thy
   2.142    | end_theory pos _ = error ("Malformed theory" ^ Position.here pos);
   2.143  
   2.144  
   2.145 @@ -185,13 +205,7 @@
   2.146    fun init _ = NONE;
   2.147  );
   2.148  
   2.149 -fun presentation_context0 state =
   2.150 -  (case state of
   2.151 -    State (SOME (_, ctxt), _) => ctxt
   2.152 -  | State (NONE, _) =>
   2.153 -      (case try Theory.get_pure () of
   2.154 -        SOME thy => Proof_Context.init_global thy
   2.155 -      | NONE => raise UNDEF));
   2.156 +fun presentation_context0 (State ((_, pr_ctxt), _)) = pr_ctxt;
   2.157  
   2.158  fun presentation_context (state as State (current, _)) =
   2.159    presentation_context0 state
   2.160 @@ -199,31 +213,31 @@
   2.161  
   2.162  fun presentation_state ctxt =
   2.163    (case Presentation_State.get ctxt of
   2.164 -    NONE => State (SOME (node_presentation0 (Theory (Context.Proof ctxt))), NONE)
   2.165 +    NONE => State (node_presentation0 (Theory (Context.Proof ctxt)), NONE)
   2.166    | SOME state => state);
   2.167  
   2.168  
   2.169  (* print state *)
   2.170  
   2.171  fun pretty_context state =
   2.172 -  (case try node_of state of
   2.173 -    NONE => []
   2.174 -  | SOME node =>
   2.175 -      let
   2.176 -        val gthy =
   2.177 -          (case node of
   2.178 -            Theory gthy => gthy
   2.179 -          | Proof (_, (_, gthy)) => gthy
   2.180 -          | Skipped_Proof (_, (_, gthy)) => gthy);
   2.181 -        val lthy = Context.cases Named_Target.theory_init I gthy;
   2.182 -      in Local_Theory.pretty lthy end);
   2.183 +  if is_toplevel state then []
   2.184 +  else
   2.185 +    let
   2.186 +      val gthy =
   2.187 +        (case node_of state of
   2.188 +          Toplevel => raise Match
   2.189 +        | Theory gthy => gthy
   2.190 +        | Proof (_, (_, gthy)) => gthy
   2.191 +        | Skipped_Proof (_, (_, gthy)) => gthy);
   2.192 +      val lthy = Context.cases Named_Target.theory_init I gthy;
   2.193 +    in Local_Theory.pretty lthy end;
   2.194  
   2.195  fun pretty_state state =
   2.196 -  (case try node_of state of
   2.197 -    NONE => []
   2.198 -  | SOME (Theory _) => []
   2.199 -  | SOME (Proof (prf, _)) => Proof.pretty_state (Proof_Node.current prf)
   2.200 -  | SOME (Skipped_Proof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]);
   2.201 +  (case node_of state of
   2.202 +    Toplevel => []
   2.203 +  | Theory _ => []
   2.204 +  | Proof (prf, _) => Proof.pretty_state (Proof_Node.current prf)
   2.205 +  | Skipped_Proof (d, _) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]);
   2.206  
   2.207  val string_of_state = pretty_state #> Pretty.chunks #> Pretty.string_of;
   2.208  
   2.209 @@ -242,8 +256,8 @@
   2.210  fun apply_transaction f g node =
   2.211    let
   2.212      val node_pr = node_presentation0 node;
   2.213 -    val context = cases_node I (Context.Proof o Proof.context_of) node;
   2.214 -    fun state_error e node_pr' = (State (SOME node_pr', SOME node_pr), e);
   2.215 +    val context = cases_proper_node I (Context.Proof o Proof.context_of) node;
   2.216 +    fun state_error e node_pr' = (State (node_pr', get_theory node), e);
   2.217  
   2.218      val (result, err) =
   2.219        node
   2.220 @@ -256,13 +270,6 @@
   2.221      | SOME exn => raise FAILURE (result, exn))
   2.222    end;
   2.223  
   2.224 -val exit_transaction =
   2.225 -  apply_transaction
   2.226 -    ((fn Theory (Context.Theory thy) => Theory (Context.Theory (Theory.end_theory thy))
   2.227 -       | node => node) #> node_presentation0)
   2.228 -    (K ())
   2.229 -  #> (fn State (node_pr', _) => State (NONE, node_pr'));
   2.230 -
   2.231  
   2.232  (* primitive transitions *)
   2.233  
   2.234 @@ -278,14 +285,20 @@
   2.235  
   2.236  local
   2.237  
   2.238 -fun apply_tr _ (Init f) (State (NONE, _)) =
   2.239 +fun apply_tr _ (Init f) (State ((Toplevel, _), _)) =
   2.240        let val node = Theory (Context.Theory (Runtime.controlled_execution NONE f ()))
   2.241 -      in State (SOME (node_presentation0 node), NONE) end
   2.242 -  | apply_tr _ Exit (State (SOME (node as Theory (Context.Theory _), _), _)) =
   2.243 -      exit_transaction node
   2.244 +      in State (node_presentation0 node, NONE) end
   2.245 +  | apply_tr _ Exit (State ((node as Theory (Context.Theory thy), _), _)) =
   2.246 +      let
   2.247 +        val State ((node', pr_ctxt), _) =
   2.248 +          node |> apply_transaction
   2.249 +            (fn _ => node_presentation0 (Theory (Context.Theory (Theory.end_theory thy))))
   2.250 +            (K ());
   2.251 +      in State ((Toplevel, pr_ctxt), get_theory node') end
   2.252    | apply_tr int (Keep f) state =
   2.253        Runtime.controlled_execution (try generic_theory_of state) (fn x => tap (f int) x) state
   2.254 -  | apply_tr int (Transaction (f, g)) (State (SOME (node, _), _)) =
   2.255 +  | apply_tr _ (Transaction _) (State ((Toplevel, _), _)) = raise UNDEF
   2.256 +  | apply_tr int (Transaction (f, g)) (State ((node, _), _)) =
   2.257        apply_transaction (fn x => f int x) g node
   2.258    | apply_tr _ _ _ = raise UNDEF;
   2.259  
   2.260 @@ -725,10 +738,10 @@
   2.261                    {name = "Toplevel.future_proof", pos = pos_of head_tr, pri = ~1}
   2.262                    (fn () =>
   2.263                      let
   2.264 -                      val State (SOME (Proof (prf, (_, orig_gthy)), _), prev) = st';
   2.265 +                      val State ((Proof (prf, (_, orig_gthy)), _), prev_thy) = st';
   2.266                        val node' = Proof (Proof_Node.apply (K state) prf, (finish, orig_gthy));
   2.267                        val (result, result_state) =
   2.268 -                        State (SOME (node_presentation0 node'), prev)
   2.269 +                        State (node_presentation0 node', prev_thy)
   2.270                          |> fold_map (element_result keywords) body_elems ||> command end_tr;
   2.271                      in (Result_List result, presentation_context0 result_state) end))
   2.272                #> (fn (res, state') => state' |> put_result (Result_Future res));
     3.1 --- a/src/Pure/PIDE/command.ML	Sat Mar 09 10:31:20 2019 +0100
     3.2 +++ b/src/Pure/PIDE/command.ML	Sat Mar 09 13:19:13 2019 +0100
     3.3 @@ -173,7 +173,10 @@
     3.4  fun init_eval_state opt_thy =
     3.5   {failed = false,
     3.6    command = Toplevel.empty,
     3.7 -  state = (case opt_thy of NONE => Toplevel.toplevel | SOME thy => Toplevel.theory_toplevel thy)};
     3.8 +  state =
     3.9 +    (case opt_thy of
    3.10 +      NONE => Toplevel.init ()
    3.11 +    | SOME thy => Toplevel.theory_toplevel thy)};
    3.12  
    3.13  datatype eval =
    3.14    Eval of
     4.1 --- a/src/Pure/PIDE/document.ML	Sat Mar 09 10:31:20 2019 +0100
     4.2 +++ b/src/Pure/PIDE/document.ML	Sat Mar 09 13:19:13 2019 +0100
     4.3 @@ -575,7 +575,7 @@
     4.4      val imports = #imports header;
     4.5  
     4.6      fun maybe_eval_result eval = Command.eval_result_state eval
     4.7 -      handle Fail _ => Toplevel.toplevel;
     4.8 +      handle Fail _ => Toplevel.init ();
     4.9  
    4.10      fun maybe_end_theory pos st = SOME (Toplevel.end_theory pos st)
    4.11        handle ERROR msg => (Output.error_message msg; NONE);
    4.12 @@ -586,7 +586,7 @@
    4.13            NONE =>
    4.14              maybe_end_theory pos
    4.15                (case get_result (snd (the (AList.lookup (op =) deps import))) of
    4.16 -                NONE => Toplevel.toplevel
    4.17 +                NONE => Toplevel.init ()
    4.18                | SOME (_, eval) => maybe_eval_result eval)
    4.19          | some => some)
    4.20          |> Option.map (fn thy => (thy, (pos, Theory.get_markup thy))));
     5.1 --- a/src/Pure/Thy/thy_info.ML	Sat Mar 09 10:31:20 2019 +0100
     5.2 +++ b/src/Pure/Thy/thy_info.ML	Sat Mar 09 13:19:13 2019 +0100
     5.3 @@ -295,7 +295,7 @@
     5.4        in (results, (st', pos')) end;
     5.5  
     5.6      val (results, (end_state, end_pos)) =
     5.7 -      fold_map element_result elements (Toplevel.toplevel, Position.none);
     5.8 +      fold_map element_result elements (Toplevel.init (), Position.none);
     5.9  
    5.10      val thy = Toplevel.end_theory end_pos end_state;
    5.11    in (results, thy) end;
    5.12 @@ -455,7 +455,7 @@
    5.13        Outer_Syntax.parse thy pos txt
    5.14        |> map (Toplevel.modify_init (K thy));
    5.15      val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs);
    5.16 -    val end_state = fold (Toplevel.command_exception true) trs Toplevel.toplevel;
    5.17 +    val end_state = fold (Toplevel.command_exception true) trs (Toplevel.init ());
    5.18    in Toplevel.end_theory end_pos end_state end;
    5.19  
    5.20  
     6.1 --- a/src/Pure/Thy/thy_output.ML	Sat Mar 09 10:31:20 2019 +0100
     6.2 +++ b/src/Pure/Thy/thy_output.ML	Sat Mar 09 13:19:13 2019 +0100
     6.3 @@ -449,7 +449,7 @@
     6.4    in
     6.5      if length command_results = length spans then
     6.6        ((NONE, []), NONE, true, [], (I, I))
     6.7 -      |> present Toplevel.toplevel (spans ~~ command_results)
     6.8 +      |> present (Toplevel.init ()) (spans ~~ command_results)
     6.9        |> present_trailer
    6.10        |> rev
    6.11      else error "Messed-up outer syntax for presentation"