Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/Pure/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 2 kB

Quelle term_sharing.ML Sprache: SML

(*  Title:      Pure/term_sharing.ML
    Author:     Makarius

Local sharing of type/term sub-structure, with global interning of
formal entity names.
*)

signature TERM_SHARING =
sig
  val init: theory -> (typ -> typ) * (term -> term)
  val typs: theory -> typ list -> typ list
  val terms: theory -> term list -> term list
end;

structure Term_Sharing: TERM_SHARING =
struct

structure Syntax_Termtab = Table(type key = term val ord = Term_Ord.syntax_term_ord);

fun init thy =
  let
    val {classes = (_, algebra), types, ...} = Type.rep_tsig (Sign.tsig_of thy);

    val class = perhaps (try (#1 o Graph.get_entry (Sorts.classes_of algebra)));
    val tycon = perhaps (Option.map #1 o Name_Space.lookup_key types);
    val const = perhaps (Consts.get_const_name (Sign.consts_of thy));

    val typs = Unsynchronized.ref (Typtab.empty: Typtab.set);
    val terms = Unsynchronized.ref (Syntax_Termtab.empty: Syntax_Termtab.set);

    fun typ T =
      (case Typtab.lookup_key (! typs) T of
        SOME (T', ()) => T'
      | NONE =>
          let
            val T' =
              (case T of
                Type (a, Ts) => Type (tycon a, map typ Ts)
              | TFree (a, S) => TFree (a, map class S)
              | TVar (a, S) => TVar (a, map class S));
            val _ = Unsynchronized.change typs (Typtab.insert_set T');
          in T' end);

    fun term tm =
      (case Syntax_Termtab.lookup_key (! terms) tm of
        SOME (tm', ()) => tm'
      | NONE =>
          let
            val tm' =
              (case tm of
                Const (c, T) => Const (const c, typ T)
              | Free (x, T) => Free (x, typ T)
              | Var (xi, T) => Var (xi, typ T)
              | Bound i => Bound i
              | Abs (x, T, t) => Abs (x, typ T, term t)
              | t $ u => term t $ term u);
            val _ = Unsynchronized.change terms (Syntax_Termtab.insert_set tm');
          in tm' end);

    fun check eq f x =
      let val x' = f x in
        if eq (x, x') then x'
        else raise Fail "Something is utterly wrong"
      end;

  in (check (op =) typ, check (op =) term) end;

val typs = map o #1 o init;
val terms = map o #2 o init;

end;

quality95%

¤ Dauer der Verarbeitung: 0.10 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.