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