abbreviate: always authentic, force expansion of internal abbreviations;
authorwenzelm
Sat Dec 09 18:05:39 2006 +0100 (2006-12-09 ago)
changeset 21720059e6b8cee8e
parent 21719 b67fbfc8a126
child 21721 908a93216f00
abbreviate: always authentic, force expansion of internal abbreviations;
tuned signature;
tuned;
src/Pure/consts.ML
     1.1 --- a/src/Pure/consts.ML	Sat Dec 09 18:05:38 2006 +0100
     1.2 +++ b/src/Pure/consts.ML	Sat Dec 09 18:05:39 2006 +0100
     1.3 @@ -12,11 +12,12 @@
     1.4    val eq_consts: T * T -> bool
     1.5    val abbrevs_of: T -> string list -> (term * term) list
     1.6    val dest: T ->
     1.7 -   {constants: (typ * term option) NameSpace.table,
     1.8 +   {constants: (typ * (term * term) option) NameSpace.table,
     1.9      constraints: typ NameSpace.table}
    1.10 -  val declaration: T -> string -> typ                               (*exception TYPE*)
    1.11 -  val monomorphic: T -> string -> bool                              (*exception TYPE*)
    1.12 -  val constraint: T -> string -> typ                                (*exception TYPE*)
    1.13 +  val the_abbreviation: T -> string -> typ * (term * term)          (*exception TYPE*)
    1.14 +  val the_declaration: T -> string -> typ                           (*exception TYPE*)
    1.15 +  val is_monomorphic: T -> string -> bool                           (*exception TYPE*)
    1.16 +  val the_constraint: T -> string -> typ                            (*exception TYPE*)
    1.17    val space_of: T -> NameSpace.T
    1.18    val intern: T -> xstring -> string
    1.19    val extern: T -> string -> xstring
    1.20 @@ -29,9 +30,9 @@
    1.21    val instance: T -> string * typ list -> typ
    1.22    val declare: NameSpace.naming -> (bstring * typ) * bool -> T -> T
    1.23    val constrain: string * typ option -> T -> T
    1.24 -  val expand_abbrevs: bool -> T -> T
    1.25 +  val set_expand: bool -> T -> T
    1.26    val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> string ->
    1.27 -    (bstring * term) * bool -> T -> ((string * typ) * term) * T
    1.28 +    bstring * term -> T -> ((string * typ) * term) * T
    1.29    val hide: bool -> string -> T -> T
    1.30    val empty: T
    1.31    val merge: T * T -> T
    1.32 @@ -46,8 +47,8 @@
    1.33  (* datatype T *)
    1.34  
    1.35  datatype kind =
    1.36 -  LogicalConst of int list list |
    1.37 -  Abbreviation of term;
    1.38 +  LogicalConst of int list list |      (*typargs positions*)
    1.39 +  Abbreviation of term * term * bool   (*rhs, normal rhs, force_expand*);
    1.40  
    1.41  type decl =
    1.42    (typ * kind) *
    1.43 @@ -57,16 +58,16 @@
    1.44   {decls: (decl * serial) NameSpace.table,
    1.45    constraints: typ Symtab.table,
    1.46    rev_abbrevs: (term * term) list Symtab.table,
    1.47 -  expand_abbrevs: bool} * stamp;
    1.48 +  do_expand: bool} * stamp;
    1.49  
    1.50  fun eq_consts (Consts (_, s1), Consts (_, s2)) = s1 = s2;
    1.51  
    1.52 -fun make_consts (decls, constraints, rev_abbrevs, expand_abbrevs) =
    1.53 +fun make_consts (decls, constraints, rev_abbrevs, do_expand) =
    1.54    Consts ({decls = decls, constraints = constraints, rev_abbrevs = rev_abbrevs,
    1.55 -    expand_abbrevs = expand_abbrevs}, stamp ());
    1.56 +    do_expand = do_expand}, stamp ());
    1.57  
    1.58 -fun map_consts f (Consts ({decls, constraints, rev_abbrevs, expand_abbrevs}, _)) =
    1.59 -  make_consts (f (decls, constraints, rev_abbrevs, expand_abbrevs));
    1.60 +fun map_consts f (Consts ({decls, constraints, rev_abbrevs, do_expand}, _)) =
    1.61 +  make_consts (f (decls, constraints, rev_abbrevs, do_expand));
    1.62  
    1.63  fun abbrevs_of (Consts ({rev_abbrevs, ...}, _)) modes =
    1.64    maps (Symtab.lookup_list rev_abbrevs) modes;
    1.65 @@ -75,7 +76,7 @@
    1.66  (* dest consts *)
    1.67  
    1.68  fun dest_kind (LogicalConst _) = NONE
    1.69 -  | dest_kind (Abbreviation t) = SOME t;
    1.70 +  | dest_kind (Abbreviation (t, t', _)) = SOME (t, t');
    1.71  
    1.72  fun dest (Consts ({decls = (space, decls), constraints, ...}, _)) =
    1.73   {constants = (space,
    1.74 @@ -94,13 +95,18 @@
    1.75  fun logical_const consts c =
    1.76    (case #1 (#1 (the_const consts c)) of
    1.77      (T, LogicalConst ps) => (T, ps)
    1.78 -  | _ => raise TYPE ("Illegal abbreviation: " ^ quote c, [], []));
    1.79 +  | _ => raise TYPE ("Not a logical constant: " ^ quote c, [], []));
    1.80  
    1.81 -val declaration = #1 oo logical_const;
    1.82 +fun the_abbreviation consts c =
    1.83 +  (case #1 (#1 (the_const consts c)) of
    1.84 +    (T, Abbreviation (t, t', _)) => (T, (t, t'))
    1.85 +  | _ => raise TYPE ("Not an abbreviated constant: " ^ quote c, [], []));
    1.86 +
    1.87 +val the_declaration = #1 oo logical_const;
    1.88  val type_arguments = #2 oo logical_const;
    1.89 -val monomorphic = null oo type_arguments;
    1.90 +val is_monomorphic = null oo type_arguments;
    1.91  
    1.92 -fun constraint (consts as Consts ({constraints, ...}, _)) c =
    1.93 +fun the_constraint (consts as Consts ({constraints, ...}, _)) c =
    1.94    (case Symtab.lookup constraints c of
    1.95      SOME T => T
    1.96    | NONE => #1 (#1 (#1 (the_const consts c))));
    1.97 @@ -138,7 +144,7 @@
    1.98  
    1.99  (* certify *)
   1.100  
   1.101 -fun certify pp tsig (consts as Consts ({expand_abbrevs, ...}, _)) =
   1.102 +fun certify pp tsig (consts as Consts ({do_expand, ...}, _)) =
   1.103    let
   1.104      fun err msg (c, T) =
   1.105        raise TYPE (msg ^ " " ^ quote c ^ " :: " ^ Pretty.string_of_typ pp T, [], []);
   1.106 @@ -158,10 +164,12 @@
   1.107                if not (Type.raw_instance (T', U)) then
   1.108                  err "Illegal type for constant" (c, T)
   1.109                else
   1.110 -                (case (kind, expand_abbrevs) of
   1.111 -                  (Abbreviation u, true) =>
   1.112 -                    Term.betapplys (Envir.expand_atom T' (U, u) handle TYPE _ =>
   1.113 -                      err "Illegal type for abbreviation" (c, T), args')
   1.114 +                (case kind of
   1.115 +                  Abbreviation (_, u, force_expand) =>
   1.116 +                    if do_expand orelse force_expand then
   1.117 +                      Term.betapplys (Envir.expand_atom T' (U, u) handle TYPE _ =>
   1.118 +                        err "Illegal type for abbreviation" (c, T), args')
   1.119 +                    else comb head
   1.120                  | _ => comb head)
   1.121              end
   1.122          | _ => comb head)
   1.123 @@ -179,7 +187,7 @@
   1.124  
   1.125  fun instance consts (c, Ts) =
   1.126    let
   1.127 -    val declT = declaration consts c;
   1.128 +    val declT = the_declaration consts c;
   1.129      val vars = map Term.dest_TVar (typargs consts (c, declT));
   1.130    in declT |> TermSubst.instantiateT (vars ~~ Ts) end;
   1.131  
   1.132 @@ -199,14 +207,14 @@
   1.133  
   1.134  (* name space *)
   1.135  
   1.136 -fun hide fully c = map_consts (fn (decls, constraints, rev_abbrevs, expand_abbrevs) =>
   1.137 -  (apfst (NameSpace.hide fully c) decls, constraints, rev_abbrevs, expand_abbrevs));
   1.138 +fun hide fully c = map_consts (fn (decls, constraints, rev_abbrevs, do_expand) =>
   1.139 +  (apfst (NameSpace.hide fully c) decls, constraints, rev_abbrevs, do_expand));
   1.140  
   1.141  
   1.142  (* declarations *)
   1.143  
   1.144  fun declare naming ((c, declT), authentic) =
   1.145 -    map_consts (fn (decls, constraints, rev_abbrevs, expand_abbrevs) =>
   1.146 +    map_consts (fn (decls, constraints, rev_abbrevs, do_expand) =>
   1.147    let
   1.148      fun args_of (Type (_, Ts)) pos = args_of_list Ts 0 pos
   1.149        | args_of (TVar v) pos = insert (eq_fst op =) (v, rev pos)
   1.150 @@ -215,22 +223,22 @@
   1.151        | args_of_list [] _ _ = I;
   1.152      val decl =
   1.153        (((declT, LogicalConst (map #2 (rev (args_of declT [] [])))), authentic), serial ());
   1.154 -  in (extend_decls naming (c, decl) decls, constraints, rev_abbrevs, expand_abbrevs) end);
   1.155 +  in (extend_decls naming (c, decl) decls, constraints, rev_abbrevs, do_expand) end);
   1.156  
   1.157  
   1.158  (* constraints *)
   1.159  
   1.160  fun constrain (c, C) consts =
   1.161 -  consts |> map_consts (fn (decls, constraints, rev_abbrevs, expand_abbrevs) =>
   1.162 +  consts |> map_consts (fn (decls, constraints, rev_abbrevs, do_expand) =>
   1.163      (the_const consts c handle TYPE (msg, _, _) => error msg;
   1.164        (decls,
   1.165          constraints |> (case C of SOME T => Symtab.update (c, T) | NONE => Symtab.delete_safe c),
   1.166 -        rev_abbrevs, expand_abbrevs)));
   1.167 +        rev_abbrevs, do_expand)));
   1.168  
   1.169  
   1.170  (* abbreviations *)
   1.171  
   1.172 -fun expand_abbrevs b = map_consts (fn (decls, constraints, rev_abbrevs, _) =>
   1.173 +fun set_expand b = map_consts (fn (decls, constraints, rev_abbrevs, _) =>
   1.174    (decls, constraints, rev_abbrevs, b));
   1.175  
   1.176  local
   1.177 @@ -243,38 +251,43 @@
   1.178        else []
   1.179    | _ => []);
   1.180  
   1.181 -fun rev_abbrev const rhs =
   1.182 +fun rev_abbrev lhs rhs =
   1.183    let
   1.184      fun abbrev (xs, body) =
   1.185        let val vars = fold (fn (x, T) => cons (Var ((x, 0), T))) (Term.rename_wrt_term body xs) []
   1.186 -      in (Term.subst_bounds (rev vars, body), Term.list_comb (Const const, vars)) end;
   1.187 +      in (Term.subst_bounds (rev vars, body), Term.list_comb (lhs, vars)) end;
   1.188    in map abbrev (strip_abss (Envir.beta_eta_contract rhs)) end;
   1.189  
   1.190  in
   1.191  
   1.192 -fun abbreviate pp tsig naming mode ((c, raw_rhs), authentic) consts =
   1.193 +fun abbreviate pp tsig naming mode (c, raw_rhs) consts =
   1.194    let
   1.195 -    val full_c = NameSpace.full naming c;
   1.196 +    val cert_term = certify pp tsig (consts |> set_expand false);
   1.197 +    val expand_term = certify pp tsig (consts |> set_expand true);
   1.198 +    val force_expand = (mode = #1 Syntax.internal_mode);
   1.199 +
   1.200      val rhs = raw_rhs
   1.201        |> Term.map_types (Type.cert_typ tsig)
   1.202 -      |> certify pp tsig (consts |> expand_abbrevs false);
   1.203 -    val rhs' = rhs
   1.204 -      |> certify pp tsig (consts |> expand_abbrevs true);
   1.205 +      |> cert_term;
   1.206 +    val rhs' = expand_term rhs;
   1.207      val T = Term.fastype_of rhs;
   1.208  
   1.209 +    val const = (NameSpace.full naming c, T);
   1.210 +    val lhs = Const const;
   1.211 +
   1.212      fun err msg = error (msg ^ " on rhs of abbreviation:\n" ^
   1.213 -      Pretty.string_of_term pp (Logic.mk_equals (Const (full_c, T), rhs)));
   1.214 +      Pretty.string_of_term pp (Logic.mk_equals (lhs, rhs)));
   1.215      val _ = Term.exists_subterm Term.is_Var rhs andalso err "Illegal schematic variables"
   1.216      val _ = null (Term.hidden_polymorphism rhs T) orelse err "Extra type variables";
   1.217    in
   1.218 -    consts |> map_consts (fn (decls, constraints, rev_abbrevs, expand_abbrevs) =>
   1.219 +    consts |> map_consts (fn (decls, constraints, rev_abbrevs, do_expand) =>
   1.220        let
   1.221 -        val decls' = decls
   1.222 -          |> extend_decls naming (c, (((T, Abbreviation rhs'), authentic), serial ()));
   1.223 +        val decls' = decls |> extend_decls naming
   1.224 +          (c, (((T, Abbreviation (rhs, rhs', force_expand)), true), serial ()));
   1.225          val rev_abbrevs' = rev_abbrevs
   1.226 -          |> fold (curry Symtab.update_list mode) (rev_abbrev (full_c, T) rhs);
   1.227 -      in (decls', constraints, rev_abbrevs', expand_abbrevs) end)
   1.228 -    |> pair ((full_c, T), rhs)
   1.229 +          |> fold (curry Symtab.update_list mode) (rev_abbrev lhs rhs);
   1.230 +      in (decls', constraints, rev_abbrevs', do_expand) end)
   1.231 +    |> pair (const, rhs)
   1.232    end;
   1.233  
   1.234  end;
   1.235 @@ -286,9 +299,9 @@
   1.236  
   1.237  fun merge
   1.238     (Consts ({decls = decls1, constraints = constraints1,
   1.239 -      rev_abbrevs = rev_abbrevs1, expand_abbrevs = expand_abbrevs1}, _),
   1.240 +      rev_abbrevs = rev_abbrevs1, do_expand = do_expand1}, _),
   1.241      Consts ({decls = decls2, constraints = constraints2,
   1.242 -      rev_abbrevs = rev_abbrevs2, expand_abbrevs = expand_abbrevs2}, _)) =
   1.243 +      rev_abbrevs = rev_abbrevs2, do_expand = do_expand2}, _)) =
   1.244    let
   1.245      val decls' = NameSpace.merge_tables (eq_snd (op =)) (decls1, decls2)
   1.246        handle Symtab.DUPS cs => err_dup_consts cs;
   1.247 @@ -296,7 +309,7 @@
   1.248        handle Symtab.DUPS cs => err_inconsistent_constraints cs;
   1.249      val rev_abbrevs' = (rev_abbrevs1, rev_abbrevs2) |> Symtab.join
   1.250        (K (Library.merge (fn ((t, u), (t', u')) => t aconv t' andalso u aconv u')));
   1.251 -    val expand_abbrevs' = expand_abbrevs1 orelse expand_abbrevs2;
   1.252 -  in make_consts (decls', constraints', rev_abbrevs', expand_abbrevs') end;
   1.253 +    val do_expand' = do_expand1 orelse do_expand2;
   1.254 +  in make_consts (decls', constraints', rev_abbrevs', do_expand') end;
   1.255  
   1.256  end;