src/Pure/defs.ML
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (21 months ago)
changeset 66695 91500c024c7f
parent 62181 4025b5ce1901
permissions -rw-r--r--
tuned;
     1 (*  Title:      Pure/defs.ML
     2     Author:     Makarius
     3 
     4 Global well-formedness checks for overloaded definitions (mixed constants and
     5 types). Recall that constant definitions may be explained syntactically within
     6 Pure, but type definitions require particular set-theoretic semantics.
     7 *)
     8 
     9 signature DEFS =
    10 sig
    11   datatype item_kind = Const | Type
    12   type item = item_kind * string
    13   type entry = item * typ list
    14   val item_kind_ord: item_kind * item_kind -> order
    15   val plain_args: typ list -> bool
    16   type context = Proof.context * (Name_Space.T * Name_Space.T)
    17   val global_context: theory -> context
    18   val space: context -> item_kind -> Name_Space.T
    19   val pretty_item: context -> item -> Pretty.T
    20   val pretty_args: Proof.context -> typ list -> Pretty.T list
    21   val pretty_entry: context -> entry -> Pretty.T
    22   type T
    23   type spec =
    24    {def: string option,
    25     description: string,
    26     pos: Position.T,
    27     lhs: typ list,
    28     rhs: entry list}
    29   val all_specifications_of: T -> (item * spec list) list
    30   val specifications_of: T -> item -> spec list
    31   val dest: T ->
    32    {restricts: (entry * string) list,
    33     reducts: (entry * entry list) list}
    34   val empty: T
    35   val merge: context -> T * T -> T
    36   val define: context -> bool -> string option -> string -> entry -> entry list -> T -> T
    37   val get_deps: T -> item -> (typ list * entry list) list
    38 end;
    39 
    40 structure Defs: DEFS =
    41 struct
    42 
    43 (* specification items *)
    44 
    45 datatype item_kind = Const | Type;
    46 type item = item_kind * string;
    47 type entry = item * typ list;
    48 
    49 fun item_kind_ord (Const, Type) = LESS
    50   | item_kind_ord (Type, Const) = GREATER
    51   | item_kind_ord _ = EQUAL;
    52 
    53 structure Itemtab = Table(type key = item val ord = prod_ord item_kind_ord fast_string_ord);
    54 
    55 
    56 (* pretty printing *)
    57 
    58 type context = Proof.context * (Name_Space.T * Name_Space.T);
    59 
    60 fun global_context thy =
    61   (Syntax.init_pretty_global thy, (Sign.const_space thy, Sign.type_space thy));
    62 
    63 fun space ((_, spaces): context) kind =
    64   if kind = Const then #1 spaces else #2 spaces;
    65 
    66 fun pretty_item (context as (ctxt, _)) (kind, name) =
    67   let val prt_name = Name_Space.pretty ctxt (space context kind) name in
    68     if kind = Const then prt_name
    69     else Pretty.block [Pretty.keyword1 "type", Pretty.brk 1, prt_name]
    70   end;
    71 
    72 fun pretty_args ctxt args =
    73   if null args then []
    74   else [Pretty.list "(" ")" (map (Syntax.pretty_typ ctxt o Logic.unvarifyT_global) args)];
    75 
    76 fun pretty_entry context (c, args) =
    77   Pretty.block (pretty_item context c :: pretty_args (#1 context) args);
    78 
    79 
    80 (* type arguments *)
    81 
    82 fun plain_args args =
    83   forall Term.is_TVar args andalso not (has_duplicates (op =) args);
    84 
    85 fun disjoint_args (Ts, Us) =
    86   not (Type.could_unifys (Ts, Us)) orelse
    87     ((Type.raw_unifys (Ts, map (Logic.incr_tvar (maxidx_of_typs Ts + 1)) Us) Vartab.empty; false)
    88       handle Type.TUNIFY => true);
    89 
    90 fun match_args (Ts, Us) =
    91   if Type.could_matches (Ts, Us) then
    92     Option.map Envir.subst_type
    93       (SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE)
    94   else NONE;
    95 
    96 
    97 (* datatype defs *)
    98 
    99 type spec =
   100  {def: string option,
   101   description: string,
   102   pos: Position.T,
   103   lhs: typ list,
   104   rhs: entry list};
   105 
   106 type def =
   107  {specs: spec Inttab.table,  (*source specifications*)
   108   restricts: (typ list * string) list,  (*global restrictions imposed by incomplete patterns*)
   109   reducts: (typ list * entry list) list};  (*specifications as reduction system*)
   110 
   111 fun make_def (specs, restricts, reducts) =
   112   {specs = specs, restricts = restricts, reducts = reducts}: def;
   113 
   114 fun map_def c f =
   115   Itemtab.default (c, make_def (Inttab.empty, [], [])) #>
   116   Itemtab.map_entry c (fn {specs, restricts, reducts}: def =>
   117     make_def (f (specs, restricts, reducts)));
   118 
   119 
   120 datatype T = Defs of def Itemtab.table;
   121 
   122 fun lookup_list which defs c =
   123   (case Itemtab.lookup defs c of
   124     SOME (def: def) => which def
   125   | NONE => []);
   126 
   127 fun all_specifications_of (Defs defs) =
   128   (map o apsnd) (map snd o Inttab.dest o #specs) (Itemtab.dest defs);
   129 
   130 fun specifications_of (Defs defs) = lookup_list (map snd o Inttab.dest o #specs) defs;
   131 
   132 val restricts_of = lookup_list #restricts;
   133 val reducts_of = lookup_list #reducts;
   134 
   135 fun dest (Defs defs) =
   136   let
   137     val restricts = Itemtab.fold (fn (c, {restricts, ...}) =>
   138       fold (fn (args, description) => cons ((c, args), description)) restricts) defs [];
   139     val reducts = Itemtab.fold (fn (c, {reducts, ...}) =>
   140       fold (fn (args, deps) => cons ((c, args), deps)) reducts) defs [];
   141   in {restricts = restricts, reducts = reducts} end;
   142 
   143 val empty = Defs Itemtab.empty;
   144 
   145 
   146 (* specifications *)
   147 
   148 fun disjoint_specs context c (i, {description = a, pos = pos_a, lhs = Ts, ...}: spec) =
   149   Inttab.forall (fn (j, {description = b, pos = pos_b, lhs = Us, ...}: spec) =>
   150     i = j orelse disjoint_args (Ts, Us) orelse
   151       error ("Clash of specifications for " ^
   152         Pretty.unformatted_string_of (pretty_item context c) ^ ":\n" ^
   153         "  " ^ quote a ^ Position.here pos_a ^ "\n" ^
   154         "  " ^ quote b ^ Position.here pos_b));
   155 
   156 fun join_specs context c ({specs = specs1, restricts, reducts}, {specs = specs2, ...}: def) =
   157   let
   158     val specs' =
   159       Inttab.fold (fn spec2 => (disjoint_specs context c spec2 specs1; Inttab.update spec2))
   160         specs2 specs1;
   161   in make_def (specs', restricts, reducts) end;
   162 
   163 fun update_specs context c spec = map_def c (fn (specs, restricts, reducts) =>
   164   (disjoint_specs context c spec specs; (Inttab.update spec specs, restricts, reducts)));
   165 
   166 
   167 (* normalized dependencies: reduction with well-formedness check *)
   168 
   169 local
   170 
   171 val prt = Pretty.string_of oo pretty_entry;
   172 
   173 fun err context (c, Ts) (d, Us) s1 s2 =
   174   error (s1 ^ " dependency of " ^ prt context (c, Ts) ^ " -> " ^ prt context (d, Us) ^ s2);
   175 
   176 fun acyclic context (c, Ts) (d, Us) =
   177   c <> d orelse
   178   is_none (match_args (Ts, Us)) orelse
   179   err context (c, Ts) (d, Us) "Circular" "";
   180 
   181 fun reduction context defs const deps =
   182   let
   183     fun reduct Us (Ts, rhs) =
   184       (case match_args (Ts, Us) of
   185         NONE => NONE
   186       | SOME subst => SOME (map (apsnd (map subst)) rhs));
   187     fun reducts (d, Us) = get_first (reduct Us) (reducts_of defs d);
   188 
   189     val reds = map (`reducts) deps;
   190     val deps' =
   191       if forall (is_none o #1) reds then NONE
   192       else SOME (fold_rev
   193         (fn (NONE, dp) => insert (op =) dp | (SOME dps, _) => fold (insert (op =)) dps) reds []);
   194     val _ = forall (acyclic context const) (the_default deps deps');
   195   in deps' end;
   196 
   197 fun restriction context defs (c, Ts) (d, Us) =
   198   plain_args Us orelse
   199   (case find_first (fn (Rs, _) => not (disjoint_args (Rs, Us))) (restricts_of defs d) of
   200     SOME (Rs, description) =>
   201       err context (c, Ts) (d, Us) "Malformed"
   202         ("\n(restriction " ^ prt context (d, Rs) ^ " from " ^ quote description ^ ")")
   203   | NONE => true);
   204 
   205 in
   206 
   207 fun normalize context =
   208   let
   209     fun check_def defs (c, {reducts, ...}: def) =
   210       reducts |> forall (fn (Ts, deps) => forall (restriction context defs (c, Ts)) deps);
   211     fun check_defs defs = Itemtab.forall (check_def defs) defs;
   212 
   213     fun norm_update (c, {reducts, ...}: def) (changed, defs) =
   214       let
   215         val reducts' = reducts |> map (fn (Ts, deps) =>
   216           (Ts, perhaps (reduction context defs (c, Ts)) deps));
   217       in
   218         if reducts = reducts' then (changed, defs)
   219         else (true, defs |> map_def c (fn (specs, restricts, _) => (specs, restricts, reducts')))
   220       end;
   221     fun norm_loop defs =
   222       (case Itemtab.fold norm_update defs (false, defs) of
   223         (true, defs') => norm_loop defs'
   224       | (false, _) => defs);
   225   in norm_loop #> tap check_defs end;
   226 
   227 fun dependencies context (c, args) restr deps =
   228   map_def c (fn (specs, restricts, reducts) =>
   229     let
   230       val restricts' = Library.merge (op =) (restricts, restr);
   231       val reducts' = insert (op =) (args, deps) reducts;
   232     in (specs, restricts', reducts') end)
   233   #> normalize context;
   234 
   235 end;
   236 
   237 
   238 (* merge *)
   239 
   240 fun merge context (Defs defs1, Defs defs2) =
   241   let
   242     fun add_deps (c, args) restr deps defs =
   243       if AList.defined (op =) (reducts_of defs c) args then defs
   244       else dependencies context (c, args) restr deps defs;
   245     fun add_def (c, {restricts, reducts, ...}: def) =
   246       fold (fn (args, deps) => add_deps (c, args) restricts deps) reducts;
   247   in
   248     Defs (Itemtab.join (join_specs context) (defs1, defs2)
   249       |> normalize context |> Itemtab.fold add_def defs2)
   250   end;
   251 
   252 
   253 (* define *)
   254 
   255 fun define context unchecked def description (c, args) deps (Defs defs) =
   256   let
   257     val pos = Position.thread_data ();
   258     val restr =
   259       if plain_args args orelse
   260         (case args of [Term.Type (_, rec_args)] => plain_args rec_args | _ => false)
   261       then [] else [(args, description)];
   262     val spec =
   263       (serial (), {def = def, description = description, pos = pos, lhs = args, rhs = deps});
   264     val defs' = defs |> update_specs context c spec;
   265   in Defs (defs' |> (if unchecked then I else dependencies context (c, args) restr deps)) end;
   266 
   267 fun get_deps (Defs defs) c = reducts_of defs c;
   268 
   269 end;