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