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