Quelle entity.ML Sprache: SML

(*  Title:      Pure/Isar/entity.ML
    Author:     Makarius

Entity definitions within a global or local theory context.
*)

signature ENTITY =
sig
  type 'a data_ops =
   {get_data: Context.generic -> 'a Name_Space.table,
    put_data: 'a Name_Space.table -> Context.generic -> Context.generic}
  val define_global: 'a data_ops -> binding -> 'a -> theory -> string * theory
  val define: 'a data_ops -> binding -> 'a -> local_theory -> string * local_theory
end;

structure Entity: ENTITY =
struct

(* context data *)

type 'a data_ops =
{get_data: Context.generic -> 'a Name_Space.table,
  put_data: 'a Name_Space.table -> Context.generic -> Context.generic};

(* global definition (foundation) *)

fun define_global {get_data, put_data} b x thy =
  let
    val context = Context.Theory thy;
    val (name, data') = Name_Space.define context true (b, x) (get_data context);
  in (name, Context.the_theory (put_data data' context)) end;

(* local definition *)

fun alias {get_data, put_data} binding name =
  Local_Theory.declaration {syntax = false, pervasive = false, pos = Binding.pos_of binding}
    (fn phi => fn context =>
      let
        val naming = Name_Space.naming_of context;
        val binding' = Morphism.binding phi binding;
        val data' = Name_Space.alias_table naming binding' name (get_data context);
      in put_data data' context end);

fun transfer {get_data, put_data} ctxt =
  let
    val data0 = get_data (Context.Theory (Proof_Context.theory_of ctxt));
    val data' = Name_Space.merge_tables (data0, get_data (Context.Proof ctxt));
  in Context.proof_map (put_data data') ctxt end;

fun define ops binding x =
  Local_Theory.background_theory_result (define_global ops binding x)
  #-> (fn name =>
    Local_Theory.map_contexts (K (transfer ops))
    #> alias ops binding name
    #> pair name);

end;

quality93%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.