added intern/extern/extern_early;
authorwenzelm
Sat Apr 08 22:51:17 2006 +0200 (2006-04-08)
changeset 1936438799cfa34e5
parent 19363 667b5ea637dd
child 19365 4fd1246d7998
added intern/extern/extern_early;
added expand_abbrevs flag;
strip_abss: demand ocurrences of bounds in body;
const decl: added flag for early externing (disabled for authentic syntax);
abbrevs: support print mode;
major cleanup;
src/Pure/consts.ML
     1.1 --- a/src/Pure/consts.ML	Sat Apr 08 22:51:06 2006 +0200
     1.2 +++ b/src/Pure/consts.ML	Sat Apr 08 22:51:17 2006 +0200
     1.3 @@ -10,119 +10,161 @@
     1.4  sig
     1.5    type T
     1.6    val eq_consts: T * T -> bool
     1.7 +  val abbrevs_of: T -> string list -> (term * term) list
     1.8    val dest: T ->
     1.9     {constants: (typ * term option) NameSpace.table,
    1.10      constraints: typ NameSpace.table}
    1.11 +  val declaration: T -> string -> typ                               (*exception TYPE*)
    1.12 +  val monomorphic: T -> string -> bool                              (*exception TYPE*)
    1.13 +  val constraint: T -> string -> typ                                (*exception TYPE*)
    1.14    val space_of: T -> NameSpace.T
    1.15 -  val abbrevs_of: T -> (term * term) list
    1.16 -  val declaration: T -> string -> typ                           (*exception TYPE*)
    1.17 -  val monomorphic: T -> string -> bool                          (*exception TYPE*)
    1.18 -  val constraint: T -> string -> typ                            (*exception TYPE*)
    1.19 -  val certify: Pretty.pp -> Type.tsig -> T -> term -> term      (*exception TYPE*)
    1.20 +  val intern: T -> xstring -> string
    1.21 +  val extern: T -> string -> xstring
    1.22 +  val extern_early: T -> string -> xstring
    1.23    val read_const: T -> string -> term
    1.24 +  val certify: Pretty.pp -> Type.tsig -> T -> term -> term          (*exception TYPE*)
    1.25    val typargs: T -> string * typ -> typ list
    1.26    val instance: T -> string * typ list -> typ
    1.27 -  val declare: NameSpace.naming -> bstring * typ -> T -> T
    1.28 -  val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> bool -> bstring * term -> T -> T
    1.29 +  val declare: NameSpace.naming -> (bstring * typ) * bool -> T -> T
    1.30    val constrain: string * typ option -> T -> T
    1.31 +  val expand_abbrevs: bool -> T -> T
    1.32 +  val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> string ->
    1.33 +    (bstring * term) * bool -> T -> T
    1.34    val hide: bool -> string -> T -> T
    1.35    val empty: T
    1.36    val merge: T * T -> T
    1.37 -end
    1.38 +end;
    1.39  
    1.40  structure Consts: CONSTS =
    1.41  struct
    1.42  
    1.43 -(** datatype T **)
    1.44 +
    1.45 +(** consts type **)
    1.46 +
    1.47 +(* datatype T *)
    1.48  
    1.49 -datatype decl =
    1.50 -  LogicalConst of typ * int list list |
    1.51 -  Abbreviation of typ * term;
    1.52 +datatype kind =
    1.53 +  LogicalConst of int list list |
    1.54 +  Abbreviation of term;
    1.55 +
    1.56 +type decl =
    1.57 +  (typ * kind) *
    1.58 +  bool; (*early externing*)
    1.59  
    1.60  datatype T = Consts of
    1.61 - {decls: (decl * serial) NameSpace.table,
    1.62 -  abbrevs: (term * term) list,
    1.63 -  constraints: typ Symtab.table} * stamp;
    1.64 + {decls: (decl * stamp) NameSpace.table,
    1.65 +  constraints: typ Symtab.table,
    1.66 +  rev_abbrevs: (term * term) list Symtab.table,
    1.67 +  expand_abbrevs: bool} * stamp;
    1.68  
    1.69  fun eq_consts (Consts (_, s1), Consts (_, s2)) = s1 = s2;
    1.70  
    1.71 -fun make_consts (decls, abbrevs, constraints) =
    1.72 -  Consts ({decls = decls, abbrevs = abbrevs, constraints = constraints}, stamp ());
    1.73 +fun make_consts (decls, constraints, rev_abbrevs, expand_abbrevs) =
    1.74 +  Consts ({decls = decls, constraints = constraints,
    1.75 +    expand_abbrevs = expand_abbrevs, rev_abbrevs = rev_abbrevs}, stamp ());
    1.76  
    1.77 -fun map_consts f (Consts ({decls, abbrevs, constraints}, _)) =
    1.78 -  make_consts (f (decls, abbrevs, constraints));
    1.79 +fun map_consts f (Consts ({decls, constraints, rev_abbrevs, expand_abbrevs}, _)) =
    1.80 +  make_consts (f (decls, constraints, rev_abbrevs, expand_abbrevs));
    1.81 +
    1.82 +fun abbrevs_of (Consts ({rev_abbrevs, ...}, _)) modes =
    1.83 +  List.concat (map (Symtab.lookup_list rev_abbrevs) modes);
    1.84 +
    1.85  
    1.86 -fun dest (Consts ({decls = (space, decls), abbrevs = _, constraints}, _)) =
    1.87 - {constants = (space, Symtab.fold
    1.88 -    (fn (c, (LogicalConst (T, _), _)) => Symtab.update (c, (T, NONE))
    1.89 -      | (c, (Abbreviation (T, t), _)) => Symtab.update (c, (T, SOME t))) decls Symtab.empty),
    1.90 +(* dest consts *)
    1.91 +
    1.92 +fun dest_kind (LogicalConst _) = NONE
    1.93 +  | dest_kind (Abbreviation t) = SOME t;
    1.94 +
    1.95 +fun dest (Consts ({decls = (space, decls), constraints, ...}, _)) =
    1.96 + {constants = (space,
    1.97 +    Symtab.fold (fn (c, (((T, kind), _), _)) =>
    1.98 +      Symtab.update (c, (T, dest_kind kind))) decls Symtab.empty),
    1.99    constraints = (space, constraints)};
   1.100  
   1.101 -fun space_of (Consts ({decls = (space, _), ...}, _)) = space;
   1.102 -fun abbrevs_of (Consts ({abbrevs, ...}, _)) = abbrevs;
   1.103 -
   1.104  
   1.105  (* lookup consts *)
   1.106  
   1.107 -fun err_undeclared c = raise TYPE ("Undeclared constant: " ^ quote c, [], []);
   1.108 -
   1.109  fun the_const (Consts ({decls = (_, tab), ...}, _)) c =
   1.110 -  (case Symtab.lookup tab c of SOME (decl, _) => decl | NONE => err_undeclared c);
   1.111 +  (case Symtab.lookup tab c of
   1.112 +    SOME (decl, _) => decl
   1.113 +  | NONE => raise TYPE ("Undeclared constant: " ^ quote c, [], []));
   1.114  
   1.115  fun logical_const consts c =
   1.116 -  (case the_const consts c of LogicalConst d => d | _ => err_undeclared c);
   1.117 +  (case the_const consts c of
   1.118 +    ((T, LogicalConst ps), _) => (T, ps)
   1.119 +  | _ => raise TYPE ("Illegal abbreviation: " ^ quote c, [], []));
   1.120  
   1.121 -fun declaration consts c = #1 (logical_const consts c);
   1.122 -fun monomorphic consts c = null (#2 (logical_const consts c));
   1.123 +val declaration = #1 oo logical_const;
   1.124 +val type_arguments = #2 oo logical_const;
   1.125 +val monomorphic = null oo type_arguments;
   1.126  
   1.127  fun constraint (consts as Consts ({constraints, ...}, _)) c =
   1.128    (case Symtab.lookup constraints c of
   1.129      SOME T => T
   1.130 -  | NONE => (case the_const consts c of LogicalConst (T, _) => T | Abbreviation (T, _) => T));
   1.131 +  | NONE => #1 (#1 (the_const consts c)));
   1.132  
   1.133  
   1.134 -(* certify: check/expand consts *)
   1.135 +(* name space *)
   1.136 +
   1.137 +fun space_of (Consts ({decls = (space, _), ...}, _)) = space;
   1.138 +
   1.139 +val intern = NameSpace.intern o space_of;
   1.140 +val extern = NameSpace.extern o space_of;
   1.141 +
   1.142 +fun extern_early consts c =
   1.143 +  (case try (the_const consts) c of
   1.144 +    SOME (_, true) => extern consts c
   1.145 +  | _ => Syntax.constN ^ c);
   1.146 +
   1.147  
   1.148 -fun certify pp tsig consts =
   1.149 +(* read_const *)
   1.150 +
   1.151 +fun read_const consts raw_c =
   1.152 +  let
   1.153 +    val c = intern consts raw_c;
   1.154 +    val _ = the_const consts c handle TYPE (msg, _, _) => error msg;
   1.155 +  in Const (c, dummyT) end;
   1.156 +
   1.157 +
   1.158 +(* certify *)
   1.159 +
   1.160 +fun certify pp tsig (consts as Consts ({expand_abbrevs, ...}, _)) =
   1.161    let
   1.162      fun err msg (c, T) =
   1.163        raise TYPE (msg ^ " " ^ quote c ^ " :: " ^ Pretty.string_of_typ pp T, [], []);
   1.164      fun cert tm =
   1.165        let
   1.166          val (head, args) = Term.strip_comb tm;
   1.167 -        val args' = map cert args;
   1.168 +        fun comb h = Term.list_comb (h, map cert args);
   1.169        in
   1.170          (case head of
   1.171 -          Const (c, T) =>
   1.172 -            (case the_const consts c of
   1.173 -              LogicalConst (U, _) =>
   1.174 -                if Type.typ_instance tsig (T, U) then Term.list_comb (head, args')
   1.175 -                else err "Illegal type for constant" (c, T)
   1.176 -            | Abbreviation (U, u) =>
   1.177 -                Term.betapplys (Envir.expand_atom tsig T (U, u) handle TYPE _ =>
   1.178 -                  err "Illegal type for abbreviation" (c, T), args'))
   1.179 -        | Abs (x, T, t) => Term.list_comb (Abs (x, T, cert t), args')
   1.180 -        | _ => Term.list_comb (head, args'))
   1.181 +          Abs (x, T, t) => comb (Abs (x, T, cert t))
   1.182 +        | Const (c, T) =>
   1.183 +            let
   1.184 +              val T' = Type.cert_typ tsig T;
   1.185 +              val ((U, kind), _) = the_const consts c;
   1.186 +            in
   1.187 +              if not (Type.typ_instance tsig (T', U)) then
   1.188 +                err "Illegal type for constant" (c, T)
   1.189 +              else
   1.190 +                (case (kind, expand_abbrevs) of
   1.191 +                  (Abbreviation u, true) =>
   1.192 +                    Term.betapplys (Envir.expand_atom tsig T' (U, u) handle TYPE _ =>
   1.193 +                      err "Illegal type for abbreviation" (c, T), map cert args)
   1.194 +                | _ => comb head)
   1.195 +            end
   1.196 +        | _ => comb head)
   1.197        end;
   1.198    in cert end;
   1.199  
   1.200  
   1.201 -(* read_const *)
   1.202 -
   1.203 -fun read_const consts raw_c =
   1.204 -  let
   1.205 -    val c = NameSpace.intern (space_of consts) raw_c;
   1.206 -    val _ = the_const consts c handle TYPE (msg, _, _) => error msg;
   1.207 -  in Const (c, dummyT) end;
   1.208 -
   1.209 -
   1.210  (* typargs -- view actual const type as instance of declaration *)
   1.211  
   1.212 -fun sub (Type (_, Ts)) (i :: is) = sub (nth Ts i) is
   1.213 -  | sub T [] = T
   1.214 -  | sub T _ = raise Subscript;
   1.215 +fun subscript (Type (_, Ts)) (i :: is) = subscript (nth Ts i) is
   1.216 +  | subscript T [] = T
   1.217 +  | subscript T _ = raise Subscript;
   1.218  
   1.219 -fun typargs consts (c, T) = map (sub T) (#2 (logical_const consts c));
   1.220 +fun typargs consts (c, T) = map (subscript T) (type_arguments consts c);
   1.221  
   1.222  fun instance consts (c, Ts) =
   1.223    let
   1.224 @@ -132,7 +174,7 @@
   1.225  
   1.226  
   1.227  
   1.228 -(** declare consts **)
   1.229 +(** build consts **)
   1.230  
   1.231  fun err_dup_consts cs =
   1.232    error ("Duplicate declaration of constant(s) " ^ commas_quote cs);
   1.233 @@ -146,32 +188,50 @@
   1.234  
   1.235  (* name space *)
   1.236  
   1.237 -fun hide fully c = map_consts (fn (decls, abbrevs, constraints) =>
   1.238 -  (apfst (NameSpace.hide fully c) decls, abbrevs, constraints));
   1.239 +fun hide fully c = map_consts (fn (decls, constraints, rev_abbrevs, expand_abbrevs) =>
   1.240 +  (apfst (NameSpace.hide fully c) decls, constraints, rev_abbrevs, expand_abbrevs));
   1.241  
   1.242  
   1.243  (* declarations *)
   1.244  
   1.245 -fun declare naming (c, declT) = map_consts (fn (decls, abbrevs, constraints) =>
   1.246 +fun declare naming ((c, declT), early) =
   1.247 +    map_consts (fn (decls, constraints, rev_abbrevs, expand_abbrevs) =>
   1.248    let
   1.249      fun args_of (Type (_, Ts)) pos = args_of_list Ts 0 pos
   1.250        | args_of (TVar v) pos = insert (eq_fst op =) (v, rev pos)
   1.251        | args_of (TFree _) _ = I
   1.252      and args_of_list (T :: Ts) i is = args_of T (i :: is) #> args_of_list Ts (i + 1) is
   1.253        | args_of_list [] _ _ = I;
   1.254 -    val decl = (c, (LogicalConst (declT, map #2 (rev (args_of declT [] []))), serial ()));
   1.255 -  in (extend_decls naming decl decls, abbrevs, constraints) end);
   1.256 +    val decl = (((declT, LogicalConst (map #2 (rev (args_of declT [] [])))), early), stamp ());
   1.257 +  in (extend_decls naming (c, decl) decls, constraints, rev_abbrevs, expand_abbrevs) end);
   1.258 +
   1.259 +
   1.260 +(* constraints *)
   1.261 +
   1.262 +fun constrain (c, C) consts =
   1.263 +  consts |> map_consts (fn (decls, constraints, rev_abbrevs, expand_abbrevs) =>
   1.264 +    (the_const consts c handle TYPE (msg, _, _) => error msg;
   1.265 +      (decls,
   1.266 +        constraints |> (case C of SOME T => Symtab.update (c, T) | NONE => Symtab.delete_safe c),
   1.267 +        rev_abbrevs, expand_abbrevs)));
   1.268  
   1.269  
   1.270  (* abbreviations *)
   1.271  
   1.272 +fun expand_abbrevs b = map_consts (fn (decls, constraints, rev_abbrevs, _) =>
   1.273 +  (decls, constraints, rev_abbrevs, b));
   1.274 +
   1.275  local
   1.276  
   1.277 -fun strip_abss (Abs (a, T, t)) =
   1.278 -      ([], t) :: map (fn (xs, b) => ((a, T) :: xs, b)) (strip_abss t)
   1.279 -  | strip_abss t = [([], t)];
   1.280 +fun strip_abss tm = ([], tm) ::
   1.281 +  (case tm of
   1.282 +    Abs (a, T, t) =>
   1.283 +      if Term.loose_bvar1 (t, 0) then
   1.284 +        strip_abss t |> map (fn (xs, b) => ((a, T) :: xs, b))
   1.285 +      else []
   1.286 +  | _ => []);
   1.287  
   1.288 -fun revert_abbrev const rhs =
   1.289 +fun rev_abbrev const rhs =
   1.290    let
   1.291      fun abbrev (xs, body) =
   1.292        let val vars = fold (fn (x, T) => cons (Var ((x, 0), T))) (Term.rename_wrt_term body xs) []
   1.293 @@ -180,41 +240,45 @@
   1.294  
   1.295  in
   1.296  
   1.297 -fun abbreviate pp tsig naming revert (c, raw_rhs) consts =
   1.298 -    consts |> map_consts (fn (decls, abbrevs, constraints) =>
   1.299 +fun abbreviate pp tsig naming mode ((c, raw_rhs), early) consts =
   1.300    let
   1.301 -    val rhs = certify pp tsig consts raw_rhs;
   1.302 +    val rhs = raw_rhs
   1.303 +      |> Term.map_term_types (Type.cert_typ tsig)
   1.304 +      |> certify pp tsig (consts |> expand_abbrevs false);
   1.305 +    val rhs' = rhs
   1.306 +      |> certify pp tsig (consts |> expand_abbrevs true);
   1.307      val T = Term.fastype_of rhs;
   1.308 -    val decls' = decls |> extend_decls naming (c, (Abbreviation (T, rhs), serial ()));
   1.309 -    val abbrevs' =
   1.310 -      if revert then revert_abbrev (NameSpace.full naming c, T) rhs @ abbrevs else abbrevs;
   1.311 -  in (decls', abbrevs', constraints) end);
   1.312 +  in
   1.313 +    consts |> map_consts (fn (decls, constraints, rev_abbrevs, expand_abbrevs) =>
   1.314 +      let
   1.315 +        val decls' = decls
   1.316 +          |> extend_decls naming (c, (((T, Abbreviation rhs'), early), stamp ()));
   1.317 +        val rev_abbrevs' = rev_abbrevs
   1.318 +          |> Symtab.default (mode, [])
   1.319 +          |> Symtab.map_entry mode (append (rev_abbrev (NameSpace.full naming c, T) rhs));
   1.320 +      in (decls', constraints, rev_abbrevs', expand_abbrevs) end)
   1.321 +  end;
   1.322  
   1.323  end;
   1.324  
   1.325  
   1.326 -(* constraints *)
   1.327 -
   1.328 -fun constrain (c, opt_T) consts = consts |> map_consts (fn (decls, abbrevs, constraints) =>
   1.329 -  (the_const consts c handle TYPE (msg, _, _) => error msg;
   1.330 -    (decls, abbrevs, constraints |>
   1.331 -      (case opt_T of SOME T => Symtab.update (c, T) | NONE => Symtab.delete_safe c))));
   1.332 -
   1.333 -
   1.334  (* empty and merge *)
   1.335  
   1.336 -val empty = make_consts (NameSpace.empty_table, [], Symtab.empty);
   1.337 +val empty = make_consts (NameSpace.empty_table, Symtab.empty, Symtab.empty, true);
   1.338  
   1.339  fun merge
   1.340 -   (Consts ({decls = decls1, abbrevs = abbrevs1, constraints = constraints1}, _),
   1.341 -    Consts ({decls = decls2, abbrevs = abbrevs2, constraints = constraints2}, _)) =
   1.342 +   (Consts ({decls = decls1, constraints = constraints1,
   1.343 +      rev_abbrevs = rev_abbrevs1, expand_abbrevs = expand_abbrevs1}, _),
   1.344 +    Consts ({decls = decls2, constraints = constraints2,
   1.345 +      rev_abbrevs = rev_abbrevs2, expand_abbrevs = expand_abbrevs2}, _)) =
   1.346    let
   1.347      val decls' = NameSpace.merge_tables (eq_snd (op =)) (decls1, decls2)
   1.348        handle Symtab.DUPS cs => err_dup_consts cs;
   1.349 -    val abbrevs' =
   1.350 -      Library.merge (fn ((t, u), (t', u')) => t aconv t' andalso u aconv u') (abbrevs1, abbrevs2);
   1.351      val constraints' = Symtab.merge (op =) (constraints1, constraints2)
   1.352        handle Symtab.DUPS cs => err_inconsistent_constraints cs;
   1.353 -  in make_consts (decls', abbrevs', constraints') end;
   1.354 +    val rev_abbrevs' = (rev_abbrevs1, rev_abbrevs2) |> Symtab.join
   1.355 +      (K (Library.merge (fn ((t, u), (t', u')) => t aconv t' andalso u aconv u')));
   1.356 +    val expand_abbrevs' = expand_abbrevs1 orelse expand_abbrevs2;
   1.357 +  in make_consts (decls', constraints', rev_abbrevs', expand_abbrevs') end;
   1.358  
   1.359  end;