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