src/Pure/sign.ML
changeset 18941 18cb1e2ab77d
parent 18928 042608ffa2ec
child 18967 ea42ab6c08d1
     1.1 --- a/src/Pure/sign.ML	Mon Feb 06 20:59:07 2006 +0100
     1.2 +++ b/src/Pure/sign.ML	Mon Feb 06 20:59:08 2006 +0100
     1.3 @@ -25,6 +25,8 @@
     1.4    val del_modesyntax_i: (string * bool) -> (bstring * typ * mixfix) list -> theory -> theory
     1.5    val add_consts: (bstring * string * mixfix) list -> theory -> theory
     1.6    val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
     1.7 +  val add_abbrevs: (bstring * string * mixfix) list -> theory -> theory
     1.8 +  val add_abbrevs_i: (bstring * term * mixfix) list -> theory -> theory
     1.9    val add_const_constraint: xstring * string -> theory -> theory
    1.10    val add_const_constraint_i: string * typ -> theory -> theory
    1.11    val add_classes: (bstring * xstring list) list -> theory -> theory
    1.12 @@ -116,6 +118,7 @@
    1.13    val const_monomorphic: theory -> string -> bool
    1.14    val const_typargs: theory -> string * typ -> typ list
    1.15    val const_instance: theory -> string * typ list -> typ
    1.16 +  val const_expansion: theory -> string * typ -> term option
    1.17    val class_space: theory -> NameSpace.T
    1.18    val type_space: theory -> NameSpace.T
    1.19    val const_space: theory -> NameSpace.T
    1.20 @@ -155,6 +158,8 @@
    1.21    val certify_prop: Pretty.pp -> theory -> term -> term * typ * int
    1.22    val cert_term: theory -> term -> term
    1.23    val cert_prop: theory -> term -> term
    1.24 +  val no_vars: Pretty.pp -> term -> term
    1.25 +  val cert_def: Pretty.pp -> term -> (string * typ) * term
    1.26    val read_sort': Syntax.syntax -> Context.generic -> string -> sort
    1.27    val read_sort: theory -> string -> sort
    1.28    val read_typ': Syntax.syntax -> Context.generic ->
    1.29 @@ -183,8 +188,6 @@
    1.30    val simple_read_term: theory -> typ -> string -> term
    1.31    val read_term: theory -> string -> term
    1.32    val read_prop: theory -> string -> term
    1.33 -  val const_of_class: class -> string
    1.34 -  val class_of_const: string -> class
    1.35    include SIGN_THEORY
    1.36  end
    1.37  
    1.38 @@ -285,6 +288,7 @@
    1.39  val const_monomorphic = Consts.monomorphic o consts_of;
    1.40  val const_typargs = Consts.typargs o consts_of;
    1.41  val const_instance = Consts.instance o consts_of;
    1.42 +fun const_expansion thy = Consts.expansion (tsig_of thy) (consts_of thy);
    1.43  
    1.44  val declared_tyname = Symtab.defined o #2 o #types o Type.rep_tsig o tsig_of;
    1.45  val declared_const = is_some oo const_type;
    1.46 @@ -324,7 +328,7 @@
    1.47    let
    1.48      fun f' x = let val y = f x in if x = y then NONE else SOME (x, y) end;
    1.49      val tab = List.mapPartial f' (add_names (t, []));
    1.50 -    fun get x = if_none (AList.lookup (op =) tab x) x;
    1.51 +    fun get x = the_default x (AList.lookup (op =) tab x);
    1.52    in get end;
    1.53  
    1.54  fun typ_mapping f g thy T =
    1.55 @@ -439,28 +443,18 @@
    1.56    let
    1.57      val _ = Context.check_thy thy;
    1.58  
    1.59 -    val tm' = map_term_types (certify_typ thy) tm;
    1.60 -    val tm' = if tm = tm' then tm else tm';  (*avoid copying of already normal term*)
    1.61 -
    1.62 -    fun err msg = raise TYPE (msg, [], [tm']);
    1.63 -
    1.64 -    fun show_const a T = quote a ^ " :: " ^ Pretty.string_of_typ pp T;
    1.65 +    fun check_vars (t $ u) = (check_vars t; check_vars u)
    1.66 +      | check_vars (Abs (_, _, t)) = check_vars t
    1.67 +      | check_vars (t as Var ((x, i), _)) =
    1.68 +          if i < 0 then raise TYPE ("Malformed variable: " ^ quote x, [], [t]) else ()
    1.69 +      | check_vars _ = ();
    1.70  
    1.71 -    fun check_atoms (t $ u) = (check_atoms t; check_atoms u)
    1.72 -      | check_atoms (Abs (_, _, t)) = check_atoms t
    1.73 -      | check_atoms (Const (a, T)) =
    1.74 -          (case const_type thy a of
    1.75 -            NONE => err ("Undeclared constant " ^ show_const a T)
    1.76 -          | SOME U =>
    1.77 -              if typ_instance thy (T, U) then ()
    1.78 -              else err ("Illegal type for constant " ^ show_const a T))
    1.79 -      | check_atoms (Var ((x, i), _)) =
    1.80 -          if i < 0 then err ("Malformed variable: " ^ quote x) else ()
    1.81 -      | check_atoms _ = ();
    1.82 -  in
    1.83 -    check_atoms tm';
    1.84 -    (tm', type_check pp tm', maxidx_of_term tm')
    1.85 -  end;
    1.86 +    val tm' = tm
    1.87 +      |> map_term_types (certify_typ thy)
    1.88 +      |> Consts.certify pp (tsig_of thy) (consts_of thy)
    1.89 +      |> tap check_vars;
    1.90 +    val tm' = if tm = tm' then tm else tm';  (*avoid copying of already normal term*)
    1.91 +  in (tm', type_check pp tm', maxidx_of_term tm') end;
    1.92  
    1.93  end;
    1.94  
    1.95 @@ -472,6 +466,24 @@
    1.96  fun cert_prop thy tm = #1 (certify_prop (pp thy) thy tm);
    1.97  
    1.98  
    1.99 +(* specifications *)
   1.100 +
   1.101 +fun no_vars pp tm =
   1.102 +  (case (Term.term_vars tm, Term.term_tvars tm) of
   1.103 +    ([], []) => tm
   1.104 +  | (ts, ixns) => error (Pretty.string_of (Pretty.block (Pretty.breaks
   1.105 +      (Pretty.str "Illegal schematic variable(s) in term:" ::
   1.106 +       map (Pretty.term pp) ts @ map (Pretty.typ pp o TVar) ixns)))));
   1.107 +
   1.108 +fun cert_def pp tm =
   1.109 +  let val ((lhs, rhs), _) = tm
   1.110 +    |> no_vars pp
   1.111 +    |> Logic.strip_imp_concl
   1.112 +    |> Logic.dest_def pp Term.is_Const (K false) (K false)
   1.113 +  in (Term.dest_Const (Term.head_of lhs), rhs) end
   1.114 +  handle TERM (msg, _) => error msg;
   1.115 +
   1.116 +
   1.117  
   1.118  (** read and certify entities **)    (*exception ERROR*)
   1.119  
   1.120 @@ -715,6 +727,35 @@
   1.121  end;
   1.122  
   1.123  
   1.124 +(* add abbreviations *)
   1.125 +
   1.126 +local
   1.127 +
   1.128 +fun gen_add_abbrevs prep_term raw_args thy =
   1.129 +  let
   1.130 +    val prep_tm =
   1.131 +      Compress.term thy o Logic.varify o no_vars (pp thy) o Term.no_dummy_patterns o prep_term thy;
   1.132 +    fun prep (raw_c, raw_t, mx) =
   1.133 +      let
   1.134 +        val c = Syntax.const_name raw_c mx;
   1.135 +        val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg)
   1.136 +          handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
   1.137 +      in ((c, t), (raw_c, Term.fastype_of t, mx)) end;
   1.138 +    val (abbrs, syn) = split_list (map prep raw_args);
   1.139 +  in
   1.140 +    thy
   1.141 +    |> map_consts (fold (Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy)) abbrs)
   1.142 +    |> add_syntax_i syn
   1.143 +  end;
   1.144 +
   1.145 +in
   1.146 +
   1.147 +val add_abbrevs = gen_add_abbrevs read_term;
   1.148 +val add_abbrevs_i = gen_add_abbrevs cert_term;
   1.149 +
   1.150 +end;
   1.151 +
   1.152 +
   1.153  (* add constraints *)
   1.154  
   1.155  fun gen_add_constraint int_const prep_typ (raw_c, raw_T) thy =
   1.156 @@ -732,12 +773,6 @@
   1.157  
   1.158  (* add type classes *)
   1.159  
   1.160 -val classN = "_class";
   1.161 -
   1.162 -val const_of_class = suffix classN;
   1.163 -fun class_of_const c = unsuffix classN c
   1.164 -  handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []);
   1.165 -
   1.166  fun gen_add_class int_class (bclass, raw_classes) thy =
   1.167    thy |> map_sign (fn (naming, syn, tsig, consts) =>
   1.168      let
   1.169 @@ -745,7 +780,7 @@
   1.170        val syn' = Syntax.extend_consts [bclass] syn;
   1.171        val tsig' = Type.add_classes (pp thy) naming [(bclass, classes)] tsig;
   1.172      in (naming, syn', tsig', consts) end)
   1.173 -  |> add_consts_i [(const_of_class bclass, a_itselfT --> propT, NoSyn)];
   1.174 +  |> add_consts_i [(Logic.const_of_class bclass, a_itselfT --> propT, NoSyn)];
   1.175  
   1.176  val add_classes = fold (gen_add_class intern_class);
   1.177  val add_classes_i = fold (gen_add_class (K I));