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