src/Pure/defs.ML
author blanchet
Mon May 19 23:43:53 2014 +0200 (2014-05-19)
changeset 57008 10f68b83b474
parent 56050 fdccbb97915a
child 57520 3ad1b289f21b
permissions -rw-r--r--
use E 1.8's auto scheduler option
     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   val pretty_const: Proof.context -> string * typ list -> Pretty.T
    11   val plain_args: typ list -> bool
    12   type T
    13   type spec =
    14    {def: string option,
    15     description: string,
    16     pos: Position.T,
    17     lhs: typ list,
    18     rhs: (string * typ list) list}
    19   val all_specifications_of: T -> (string * spec list) list
    20   val specifications_of: T -> string -> spec list
    21   val dest: T ->
    22    {restricts: ((string * typ list) * string) list,
    23     reducts: ((string * typ list) * (string * typ list) list) list}
    24   val empty: T
    25   val merge: Proof.context -> T * T -> T
    26   val define: Proof.context -> bool -> string option -> string ->
    27     string * typ list -> (string * typ list) list -> T -> T
    28 end
    29 
    30 structure Defs: DEFS =
    31 struct
    32 
    33 (* type arguments *)
    34 
    35 type args = typ list;
    36 
    37 fun pretty_const ctxt (c, args) =
    38   let
    39     val prt_args =
    40       if null args then []
    41       else [Pretty.list "(" ")" (map (Syntax.pretty_typ ctxt o Logic.unvarifyT_global) args)];
    42   in Pretty.block (Pretty.str c :: prt_args) end;
    43 
    44 fun plain_args args =
    45   forall Term.is_TVar args andalso not (has_duplicates (op =) args);
    46 
    47 fun disjoint_args (Ts, Us) =
    48   not (Type.could_unifys (Ts, Us)) orelse
    49     ((Type.raw_unifys (Ts, map (Logic.incr_tvar (maxidx_of_typs Ts + 1)) Us) Vartab.empty; false)
    50       handle Type.TUNIFY => true);
    51 
    52 fun match_args (Ts, Us) =
    53   if Type.could_matches (Ts, Us) then
    54     Option.map Envir.subst_type
    55       (SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE)
    56   else NONE;
    57 
    58 
    59 (* datatype defs *)
    60 
    61 type spec =
    62  {def: string option,
    63   description: string,
    64   pos: Position.T,
    65   lhs: args,
    66   rhs: (string * args) list};
    67 
    68 type def =
    69  {specs: spec Inttab.table,  (*source specifications*)
    70   restricts: (args * string) list,  (*global restrictions imposed by incomplete patterns*)
    71   reducts: (args * (string * args) list) list};  (*specifications as reduction system*)
    72 
    73 fun make_def (specs, restricts, reducts) =
    74   {specs = specs, restricts = restricts, reducts = reducts}: def;
    75 
    76 fun map_def c f =
    77   Symtab.default (c, make_def (Inttab.empty, [], [])) #>
    78   Symtab.map_entry c (fn {specs, restricts, reducts}: def =>
    79     make_def (f (specs, restricts, reducts)));
    80 
    81 
    82 datatype T = Defs of def Symtab.table;
    83 
    84 fun lookup_list which defs c =
    85   (case Symtab.lookup defs c of
    86     SOME (def: def) => which def
    87   | NONE => []);
    88 
    89 fun all_specifications_of (Defs defs) =
    90   (map o apsnd) (map snd o Inttab.dest o #specs) (Symtab.dest defs);
    91 
    92 fun specifications_of (Defs defs) = lookup_list (map snd o Inttab.dest o #specs) defs;
    93 
    94 val restricts_of = lookup_list #restricts;
    95 val reducts_of = lookup_list #reducts;
    96 
    97 fun dest (Defs defs) =
    98   let
    99     val restricts = Symtab.fold (fn (c, {restricts, ...}) =>
   100       fold (fn (args, description) => cons ((c, args), description)) restricts) defs [];
   101     val reducts = Symtab.fold (fn (c, {reducts, ...}) =>
   102       fold (fn (args, deps) => cons ((c, args), deps)) reducts) defs [];
   103   in {restricts = restricts, reducts = reducts} end;
   104 
   105 val empty = Defs Symtab.empty;
   106 
   107 
   108 (* specifications *)
   109 
   110 fun disjoint_specs c (i, {description = a, pos = pos_a, lhs = Ts, ...}: spec) =
   111   Inttab.forall (fn (j, {description = b, pos = pos_b, lhs = Us, ...}: spec) =>
   112     i = j orelse disjoint_args (Ts, Us) orelse
   113       error ("Clash of specifications for constant " ^ quote c ^ ":\n" ^
   114         "  " ^ quote a ^ Position.here pos_a ^ "\n" ^
   115         "  " ^ quote b ^ Position.here pos_b));
   116 
   117 fun join_specs c ({specs = specs1, restricts, reducts}, {specs = specs2, ...}: def) =
   118   let
   119     val specs' =
   120       Inttab.fold (fn spec2 => (disjoint_specs c spec2 specs1; Inttab.update spec2)) specs2 specs1;
   121   in make_def (specs', restricts, reducts) end;
   122 
   123 fun update_specs c spec = map_def c (fn (specs, restricts, reducts) =>
   124   (disjoint_specs c spec specs; (Inttab.update spec specs, restricts, reducts)));
   125 
   126 
   127 (* normalized dependencies: reduction with well-formedness check *)
   128 
   129 local
   130 
   131 val prt = Pretty.string_of oo pretty_const;
   132 fun err ctxt (c, args) (d, Us) s1 s2 =
   133   error (s1 ^ " dependency of constant " ^ prt ctxt (c, args) ^ " -> " ^ prt ctxt (d, Us) ^ s2);
   134 
   135 fun contained (U as TVar _) (Type (_, Ts)) = exists (fn T => T = U orelse contained U T) Ts
   136   | contained _ _ = false;
   137 
   138 fun acyclic ctxt (c, args) (d, Us) =
   139   c <> d orelse
   140   exists (fn U => exists (contained U) args) Us orelse
   141   is_none (match_args (args, Us)) orelse
   142   err ctxt (c, args) (d, Us) "Circular" "";
   143 
   144 fun wellformed ctxt defs (c, args) (d, Us) =
   145   forall is_TVar Us orelse
   146   (case find_first (fn (Ts, _) => not (disjoint_args (Ts, Us))) (restricts_of defs d) of
   147     SOME (Ts, description) =>
   148       err ctxt (c, args) (d, Us) "Malformed"
   149         ("\n(restriction " ^ prt ctxt (d, Ts) ^ " from " ^ quote description ^ ")")
   150   | NONE => true);
   151 
   152 fun reduction ctxt defs const deps =
   153   let
   154     fun reduct Us (Ts, rhs) =
   155       (case match_args (Ts, Us) of
   156         NONE => NONE
   157       | SOME subst => SOME (map (apsnd (map subst)) rhs));
   158     fun reducts (d, Us) = get_first (reduct Us) (reducts_of defs d);
   159 
   160     val reds = map (`reducts) deps;
   161     val deps' =
   162       if forall (is_none o #1) reds then NONE
   163       else SOME (fold_rev
   164         (fn (NONE, dp) => insert (op =) dp | (SOME dps, _) => fold (insert (op =)) dps) reds []);
   165     val _ = forall (acyclic ctxt const) (the_default deps deps');
   166   in deps' end;
   167 
   168 in
   169 
   170 fun normalize ctxt =
   171   let
   172     fun norm_update (c, {reducts, ...}: def) (changed, defs) =
   173       let
   174         val reducts' = reducts |> map (fn (args, deps) =>
   175           (args, perhaps (reduction ctxt defs (c, args)) deps));
   176       in
   177         if reducts = reducts' then (changed, defs)
   178         else (true, defs |> map_def c (fn (specs, restricts, _) => (specs, restricts, reducts')))
   179       end;
   180     fun norm_all defs =
   181       (case Symtab.fold norm_update defs (false, defs) of
   182         (true, defs') => norm_all defs'
   183       | (false, _) => defs);
   184     fun check defs (c, {reducts, ...}: def) =
   185       reducts |> forall (fn (args, deps) => forall (wellformed ctxt defs (c, args)) deps);
   186   in norm_all #> (fn defs => tap (Symtab.forall (check defs)) defs) end;
   187 
   188 fun dependencies ctxt (c, args) restr deps =
   189   map_def c (fn (specs, restricts, reducts) =>
   190     let
   191       val restricts' = Library.merge (op =) (restricts, restr);
   192       val reducts' = insert (op =) (args, deps) reducts;
   193     in (specs, restricts', reducts') end)
   194   #> normalize ctxt;
   195 
   196 end;
   197 
   198 
   199 (* merge *)
   200 
   201 fun merge ctxt (Defs defs1, Defs defs2) =
   202   let
   203     fun add_deps (c, args) restr deps defs =
   204       if AList.defined (op =) (reducts_of defs c) args then defs
   205       else dependencies ctxt (c, args) restr deps defs;
   206     fun add_def (c, {restricts, reducts, ...}: def) =
   207       fold (fn (args, deps) => add_deps (c, args) restricts deps) reducts;
   208   in
   209     Defs (Symtab.join join_specs (defs1, defs2)
   210       |> normalize ctxt |> Symtab.fold add_def defs2)
   211   end;
   212 
   213 
   214 (* define *)
   215 
   216 fun define ctxt unchecked def description (c, args) deps (Defs defs) =
   217   let
   218     val pos = Position.thread_data ();
   219     val restr =
   220       if plain_args args orelse
   221         (case args of [Type (_, rec_args)] => plain_args rec_args | _ => false)
   222       then [] else [(args, description)];
   223     val spec =
   224       (serial (), {def = def, description = description, pos = pos, lhs = args, rhs = deps});
   225     val defs' = defs |> update_specs c spec;
   226   in Defs (defs' |> (if unchecked then I else dependencies ctxt (c, args) restr deps)) end;
   227 
   228 end;