src/Pure/theory.ML
author wenzelm
Sat Mar 09 23:57:07 2019 +0100 (2 months ago ago)
changeset 70067 0cb8753bdb50
parent 69295 bf6937af7fe8
permissions -rw-r--r--
clarified signature;
     1 (*  Title:      Pure/theory.ML
     2     Author:     Lawrence C Paulson and Markus Wenzel
     3 
     4 Logical theory content: axioms, definitions, and begin/end wrappers.
     5 *)
     6 
     7 signature THEORY =
     8 sig
     9   val parents_of: theory -> theory list
    10   val ancestors_of: theory -> theory list
    11   val nodes_of: theory -> theory list
    12   val setup: (theory -> theory) -> unit
    13   val local_setup: (Proof.context -> Proof.context) -> unit
    14   val install_pure: theory -> unit
    15   val get_pure: unit -> theory
    16   val get_pure_bootstrap: unit -> theory
    17   val get_markup: theory -> Markup.T
    18   val check: {long: bool} -> Proof.context -> string * Position.T -> theory
    19   val axiom_table: theory -> term Name_Space.table
    20   val axiom_space: theory -> Name_Space.T
    21   val axioms_of: theory -> (string * term) list
    22   val all_axioms_of: theory -> (string * term) list
    23   val defs_of: theory -> Defs.T
    24   val at_begin: (theory -> theory option) -> theory -> theory
    25   val at_end: (theory -> theory option) -> theory -> theory
    26   val begin_theory: string * Position.T -> theory list -> theory
    27   val end_theory: theory -> theory
    28   val add_axiom: Proof.context -> binding * term -> theory -> theory
    29   val const_dep: theory -> string * typ -> Defs.entry
    30   val type_dep: string * typ list -> Defs.entry
    31   val add_deps: Defs.context -> string -> Defs.entry -> Defs.entry list -> theory -> theory
    32   val add_deps_global: string -> Defs.entry -> Defs.entry list -> theory -> theory
    33   val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> theory
    34   val specify_const: (binding * typ) * mixfix -> theory -> term * theory
    35   val check_overloading: Proof.context -> bool -> string * typ -> unit
    36 end
    37 
    38 structure Theory: THEORY =
    39 struct
    40 
    41 
    42 (** theory context operations **)
    43 
    44 val parents_of = Context.parents_of;
    45 val ancestors_of = Context.ancestors_of;
    46 fun nodes_of thy = thy :: ancestors_of thy;
    47 
    48 fun setup f = Context.>> (Context.map_theory f);
    49 fun local_setup f = Context.>> (Context.map_proof f);
    50 
    51 
    52 (* implicit theory Pure *)
    53 
    54 val pure: theory Single_Assignment.var = Single_Assignment.var "pure";
    55 
    56 fun install_pure thy = Single_Assignment.assign pure thy;
    57 
    58 fun get_pure () =
    59   (case Single_Assignment.peek pure of
    60     SOME thy => thy
    61   | NONE => raise Fail "Theory Pure not present");
    62 
    63 fun get_pure_bootstrap () =
    64   (case Single_Assignment.peek pure of
    65     SOME thy => thy
    66   | NONE => Context.the_global_context ());
    67 
    68 
    69 
    70 (** datatype thy **)
    71 
    72 type wrapper = (theory -> theory option) * stamp;
    73 
    74 fun apply_wrappers (wrappers: wrapper list) =
    75   perhaps (perhaps_loop (perhaps_apply (map fst wrappers)));
    76 
    77 datatype thy = Thy of
    78  {pos: Position.T,
    79   id: serial,
    80   axioms: term Name_Space.table,
    81   defs: Defs.T,
    82   wrappers: wrapper list * wrapper list};
    83 
    84 fun make_thy (pos, id, axioms, defs, wrappers) =
    85   Thy {pos = pos, id = id, axioms = axioms, defs = defs, wrappers = wrappers};
    86 
    87 structure Thy = Theory_Data'
    88 (
    89   type T = thy;
    90   val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table;
    91   val empty = make_thy (Position.none, 0, empty_axioms, Defs.empty, ([], []));
    92 
    93   fun extend (Thy {pos = _, id = _, axioms = _, defs, wrappers}) =
    94     make_thy (Position.none, 0, empty_axioms, defs, wrappers);
    95 
    96   fun merge old_thys (thy1, thy2) =
    97     let
    98       val Thy {pos = _, id = _, axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
    99       val Thy {pos = _, id = _, axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
   100 
   101       val axioms' = empty_axioms;
   102       val defs' = Defs.merge (Defs.global_context (fst old_thys)) (defs1, defs2);
   103       val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
   104       val ens' = Library.merge (eq_snd op =) (ens1, ens2);
   105     in make_thy (Position.none, 0, axioms', defs', (bgs', ens')) end;
   106 );
   107 
   108 fun rep_theory thy = Thy.get thy |> (fn Thy args => args);
   109 
   110 fun map_thy f = Thy.map (fn (Thy {pos, id, axioms, defs, wrappers}) =>
   111   make_thy (f (pos, id, axioms, defs, wrappers)));
   112 
   113 fun map_axioms f =
   114   map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, f axioms, defs, wrappers));
   115 
   116 fun map_defs f =
   117   map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, axioms, f defs, wrappers));
   118 
   119 fun map_wrappers f =
   120   map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, axioms, defs, f wrappers));
   121 
   122 
   123 (* entity markup *)
   124 
   125 fun theory_markup def name id pos =
   126   if id = 0 then Markup.empty
   127   else
   128     Markup.properties (Position.entity_properties_of def id pos)
   129       (Markup.entity Markup.theoryN name);
   130 
   131 fun init_markup (name, pos) thy =
   132   let
   133     val id = serial ();
   134     val _ = Position.report pos (theory_markup true name id pos);
   135   in map_thy (fn (_, _, axioms, defs, wrappers) => (pos, id, axioms, defs, wrappers)) thy end;
   136 
   137 fun get_markup thy =
   138   let val {pos, id, ...} = rep_theory thy
   139   in theory_markup false (Context.theory_name thy) id pos end;
   140 
   141 fun check long ctxt (name, pos) =
   142   let
   143     val thy = Proof_Context.theory_of ctxt;
   144     val thy' =
   145       Context.get_theory long thy name
   146         handle ERROR msg =>
   147           let
   148             val completion_report =
   149               Completion.make_report (name, pos)
   150                 (fn completed =>
   151                   map (Context.theory_name' long) (ancestors_of thy)
   152                   |> filter (completed o Long_Name.base_name)
   153                   |> sort_strings
   154                   |> map (fn a => (a, (Markup.theoryN, a))));
   155           in error (msg ^ Position.here pos ^ completion_report) end;
   156     val _ = Context_Position.report ctxt pos (get_markup thy');
   157   in thy' end;
   158 
   159 
   160 (* basic operations *)
   161 
   162 val axiom_table = #axioms o rep_theory;
   163 val axiom_space = Name_Space.space_of_table o axiom_table;
   164 
   165 val axioms_of = Name_Space.dest_table o axiom_table;
   166 fun all_axioms_of thy = maps axioms_of (nodes_of thy);
   167 
   168 val defs_of = #defs o rep_theory;
   169 
   170 
   171 (* begin/end theory *)
   172 
   173 val begin_wrappers = rev o #1 o #wrappers o rep_theory;
   174 val end_wrappers = rev o #2 o #wrappers o rep_theory;
   175 
   176 fun at_begin f = map_wrappers (apfst (cons (f, stamp ())));
   177 fun at_end f = map_wrappers (apsnd (cons (f, stamp ())));
   178 
   179 fun begin_theory (name, pos) imports =
   180   if name = Context.PureN then
   181     (case imports of
   182       [thy] => init_markup (name, pos) thy
   183     | _ => error "Bad bootstrapping of theory Pure")
   184   else
   185     let
   186       val thy = Context.begin_thy name imports;
   187       val wrappers = begin_wrappers thy;
   188     in
   189       thy
   190       |> init_markup (name, pos)
   191       |> Sign.local_path
   192       |> Sign.map_naming (Name_Space.set_theory_name (Long_Name.base_name name))
   193       |> apply_wrappers wrappers
   194       |> tap (Syntax.force_syntax o Sign.syn_of)
   195     end;
   196 
   197 fun end_theory thy =
   198   thy
   199   |> apply_wrappers (end_wrappers thy)
   200   |> Sign.change_check
   201   |> Context.finish_thy;
   202 
   203 
   204 
   205 (** primitive specifications **)
   206 
   207 (* raw axioms *)
   208 
   209 fun cert_axm ctxt (b, raw_tm) =
   210   let
   211     val thy = Proof_Context.theory_of ctxt;
   212     val t = Sign.cert_prop thy raw_tm
   213       handle TYPE (msg, _, _) => error msg
   214         | TERM (msg, _) => error msg;
   215     val _ = Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
   216 
   217     val bad_sorts =
   218       rev ((fold_types o fold_atyps_sorts) (fn (_, []) => I | (T, _) => insert (op =) T) t []);
   219     val _ = null bad_sorts orelse
   220       error ("Illegal sort constraints in primitive specification: " ^
   221         commas (map (Syntax.string_of_typ (Config.put show_sorts true ctxt)) bad_sorts));
   222   in (b, Sign.no_vars ctxt t) end
   223   handle ERROR msg => cat_error msg ("The error(s) above occurred in axiom " ^ Binding.print b);
   224 
   225 fun add_axiom ctxt raw_axm thy = thy |> map_axioms (fn axioms =>
   226   let
   227     val axm = apsnd Logic.varify_global (cert_axm ctxt raw_axm);
   228     val context = ctxt
   229       |> Sign.inherit_naming thy
   230       |> Context_Position.set_visible_generic false;
   231     val (_, axioms') = Name_Space.define context true axm axioms;
   232   in axioms' end);
   233 
   234 
   235 (* dependencies *)
   236 
   237 fun const_dep thy (c, T) = ((Defs.Const, c), Sign.const_typargs thy (c, T));
   238 fun type_dep (c, args) = ((Defs.Type, c), args);
   239 
   240 fun dependencies (context as (ctxt, _)) unchecked def description lhs rhs =
   241   let
   242     fun prep (item, args) =
   243       (case fold Term.add_tvarsT args [] of
   244         [] => (item, map Logic.varifyT_global args)
   245       | vs => raise TYPE ("Illegal schematic type variable(s)", map TVar vs, []));
   246 
   247     val lhs_vars = fold Term.add_tfreesT (snd lhs) [];
   248     val rhs_extras =
   249       fold (fn (_, args) => args |> (fold o Term.fold_atyps) (fn TFree v =>
   250         if member (op =) lhs_vars v then I else insert (op =) v)) rhs [];
   251     val _ =
   252       if null rhs_extras then ()
   253       else error ("Specification depends on extra type variables: " ^
   254         commas_quote (map (Syntax.string_of_typ ctxt o TFree) rhs_extras) ^
   255         "\nThe error(s) above occurred in " ^ quote description);
   256   in Defs.define context unchecked def description (prep lhs) (map prep rhs) end;
   257 
   258 fun cert_entry thy ((Defs.Const, c), args) =
   259       Sign.cert_term thy (Const (c, Sign.const_instance thy (c, args)))
   260       |> dest_Const |> const_dep thy
   261   | cert_entry thy ((Defs.Type, c), args) =
   262       Sign.certify_typ thy (Type (c, args)) |> dest_Type |> type_dep;
   263 
   264 fun add_deps context a raw_lhs raw_rhs thy =
   265   let
   266     val (lhs as ((_, lhs_name), _)) :: rhs = map (cert_entry thy) (raw_lhs :: raw_rhs);
   267     val description = if a = "" then lhs_name ^ " axiom" else a;
   268   in thy |> map_defs (dependencies context false NONE description lhs rhs) end;
   269 
   270 fun add_deps_global a x y thy =
   271   add_deps (Defs.global_context thy) a x y thy;
   272 
   273 fun specify_const decl thy =
   274   let val (t, thy') = Sign.declare_const_global decl thy;
   275   in (t, add_deps_global "" (const_dep thy' (dest_Const t)) [] thy') end;
   276 
   277 
   278 (* overloading *)
   279 
   280 fun check_overloading ctxt overloaded (c, T) =
   281   let
   282     val thy = Proof_Context.theory_of ctxt;
   283 
   284     val declT = Sign.the_const_constraint thy c
   285       handle TYPE (msg, _, _) => error msg;
   286     val T' = Logic.varifyT_global T;
   287 
   288     fun message sorts txt =
   289       [Pretty.block [Pretty.str "Specification of constant ",
   290         Pretty.str c, Pretty.str " ::", Pretty.brk 1,
   291         Pretty.quote (Syntax.pretty_typ (Config.put show_sorts sorts ctxt) T)],
   292         Pretty.str txt] |> Pretty.chunks |> Pretty.string_of;
   293   in
   294     if Sign.typ_instance thy (declT, T') then ()
   295     else if Type.raw_instance (declT, T') then
   296       error (message true "imposes additional sort constraints on the constant declaration")
   297     else if overloaded then ()
   298     else
   299       error (message false "is strictly less general than the declared type (overloading required)")
   300   end;
   301 
   302 
   303 (* definitional axioms *)
   304 
   305 local
   306 
   307 fun check_def (context as (ctxt, _)) thy unchecked overloaded (b, tm) defs =
   308   let
   309     val name = Sign.full_name thy b;
   310     val ((lhs, rhs), _, _) =
   311       Primitive_Defs.dest_def ctxt
   312         {check_head = Term.is_Const,
   313          check_free_lhs = K true,
   314          check_free_rhs = K false,
   315          check_tfree = K false} tm
   316       handle TERM (msg, _) => error msg;
   317     val lhs_const = Term.dest_Const (Term.head_of lhs);
   318 
   319     val rhs_consts =
   320       fold_aterms (fn Const const => insert (op =) (const_dep thy const) | _ => I) rhs [];
   321     val rhs_types =
   322       (fold_types o fold_subtypes) (fn Type t => insert (op =) (type_dep t) | _ => I) rhs [];
   323     val rhs_deps = rhs_consts @ rhs_types;
   324 
   325     val _ = check_overloading ctxt overloaded lhs_const;
   326   in defs |> dependencies context unchecked (SOME name) name (const_dep thy lhs_const) rhs_deps end
   327   handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
   328    [Pretty.str ("The error(s) above occurred in definition " ^ Binding.print b ^ ":"),
   329     Pretty.fbrk, Pretty.quote (Syntax.pretty_term ctxt tm)]));
   330 
   331 in
   332 
   333 fun add_def (context as (ctxt, _)) unchecked overloaded raw_axm thy =
   334   let val axm = cert_axm ctxt raw_axm in
   335     thy
   336     |> map_defs (check_def context thy unchecked overloaded axm)
   337     |> add_axiom ctxt axm
   338   end;
   339 
   340 end;
   341 
   342 end;