src/Pure/consts.ML
changeset 25048 5a94a87af697
parent 25041 c1efae25ee76
child 25116 31551aae280f
     1.1 --- a/src/Pure/consts.ML	Tue Oct 16 16:18:36 2007 +0200
     1.2 +++ b/src/Pure/consts.ML	Tue Oct 16 17:06:09 2007 +0200
     1.3 @@ -14,12 +14,12 @@
     1.4    val dest: T ->
     1.5     {constants: (typ * (term * term) option) NameSpace.table,
     1.6      constraints: typ NameSpace.table}
     1.7 -  val the_type: T -> string -> typ                                  (*exception TYPE*)
     1.8 -  val the_abbreviation: T -> string -> typ * (term * term)          (*exception TYPE*)
     1.9 -  val type_scheme: T -> string -> typ                               (*exception TYPE*)
    1.10 -  val the_tags: T -> string -> Markup.property list                 (*exception TYPE*)
    1.11 -  val is_monomorphic: T -> string -> bool                           (*exception TYPE*)
    1.12 -  val the_constraint: T -> string -> typ                            (*exception TYPE*)
    1.13 +  val the_type: T -> string -> typ                             (*exception TYPE*)
    1.14 +  val the_abbreviation: T -> string -> typ * term              (*exception TYPE*)
    1.15 +  val type_scheme: T -> string -> typ                          (*exception TYPE*)
    1.16 +  val the_tags: T -> string -> Markup.property list            (*exception TYPE*)
    1.17 +  val is_monomorphic: T -> string -> bool                      (*exception TYPE*)
    1.18 +  val the_constraint: T -> string -> typ                       (*exception TYPE*)
    1.19    val space_of: T -> NameSpace.T
    1.20    val intern: T -> xstring -> string
    1.21    val extern: T -> string -> xstring
    1.22 @@ -34,6 +34,7 @@
    1.23    val constrain: string * typ option -> T -> T
    1.24    val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> string -> Markup.property list ->
    1.25      bstring * term -> T -> (term * term) * T
    1.26 +  val revert_abbrev: string -> string -> T -> T
    1.27    val hide: bool -> string -> T -> T
    1.28    val empty: T
    1.29    val merge: T * T -> T
    1.30 @@ -42,7 +43,6 @@
    1.31  structure Consts: CONSTS =
    1.32  struct
    1.33  
    1.34 -
    1.35  (** consts type **)
    1.36  
    1.37  (* datatype T *)
    1.38 @@ -92,7 +92,7 @@
    1.39  
    1.40  fun the_abbreviation consts c =
    1.41    (case the_const consts c of
    1.42 -    ({T, ...}, SOME abbr) => (T, dest_abbrev abbr)
    1.43 +    ({T, ...}, SOME {rhs, ...}) => (T, rhs)
    1.44    | _ => raise TYPE ("Not an abbreviated constant: " ^ quote c, [], []));
    1.45  
    1.46  val the_decl = #1 oo the_const;
    1.47 @@ -157,15 +157,17 @@
    1.48              let
    1.49                val T' = certT T;
    1.50                val ({T = U, ...}, abbr) = the_const consts c;
    1.51 +              fun expand u =
    1.52 +                Term.betapplys (Envir.expand_atom T' (U, u) handle TYPE _ =>
    1.53 +                  err "Illegal type for abbreviation" (c, T), args');
    1.54              in
    1.55                if not (Type.raw_instance (T', U)) then
    1.56                  err "Illegal type for constant" (c, T)
    1.57                else
    1.58                  (case abbr of
    1.59 -                  SOME {normal_rhs = u, force_expand, ...} =>
    1.60 -                    if do_expand orelse force_expand then
    1.61 -                      Term.betapplys (Envir.expand_atom T' (U, u) handle TYPE _ =>
    1.62 -                        err "Illegal type for abbreviation" (c, T), args')
    1.63 +                  SOME {rhs, normal_rhs, force_expand} =>
    1.64 +                    if do_expand then expand normal_rhs
    1.65 +                    else if force_expand then expand rhs
    1.66                      else comb head
    1.67                  | _ => comb head)
    1.68              end
    1.69 @@ -276,8 +278,8 @@
    1.70  
    1.71      fun err msg = error (msg ^ " on rhs of abbreviation:\n" ^
    1.72        Pretty.string_of_term pp (Logic.mk_equals (lhs, rhs)));
    1.73 -    val _ = Term.exists_subterm Term.is_Var rhs andalso err "Illegal schematic variables"
    1.74 -    val _ = null (Term.hidden_polymorphism rhs T) orelse err "Extra type variables";
    1.75 +    val _ = Term.exists_subterm Term.is_Var rhs andalso err "Illegal schematic variables";
    1.76 +    val _ = null (Term.hidden_polymorphism rhs) orelse err "Extra type variables";
    1.77    in
    1.78      consts |> map_consts (fn (decls, constraints, rev_abbrevs) =>
    1.79        let
    1.80 @@ -291,6 +293,13 @@
    1.81      |> pair (lhs, rhs)
    1.82    end;
    1.83  
    1.84 +fun revert_abbrev mode c consts = consts |> map_consts (fn (decls, constraints, rev_abbrevs) =>
    1.85 +  let
    1.86 +    val (T, rhs) = the_abbreviation consts c;
    1.87 +    val rev_abbrevs' = rev_abbrevs
    1.88 +      |> fold (curry Symtab.update_list mode) (rev_abbrev (Const (c, T)) rhs);
    1.89 +  in (decls, constraints, rev_abbrevs') end);
    1.90 +
    1.91  end;
    1.92  
    1.93