1.1 --- a/src/Pure/Isar/code.ML	Wed Dec 02 17:53:34 2009 +0100
     1.2 +++ b/src/Pure/Isar/code.ML	Wed Dec 02 17:53:35 2009 +0100
     1.3 @@ -12,6 +12,10 @@
     1.4    val read_bare_const: theory -> string -> string * typ
     1.5    val read_const: theory -> string -> string
     1.6    val string_of_const: theory -> string -> string
     1.7 +  val cert_signature: theory -> typ -> typ
     1.8 +  val read_signature: theory -> string -> typ
     1.9 +  val const_typ: theory -> string -> typ
    1.10 +  val subst_signatures: theory -> term -> term
    1.11    val args_number: theory -> string -> int
    1.12  
    1.13    (*constructor sets*)
    1.14 @@ -31,6 +35,10 @@
    1.15    val standard_typscheme: theory -> thm list -> thm list
    1.16  
    1.17    (*executable code*)
    1.18 +  val add_type: string -> theory -> theory
    1.19 +  val add_type_cmd: string -> theory -> theory
    1.20 +  val add_signature: string * typ -> theory -> theory
    1.21 +  val add_signature_cmd: string * string -> theory -> theory
    1.22    val add_datatype: (string * typ) list -> theory -> theory
    1.23    val add_datatype_cmd: string list -> theory -> theory
    1.24    val type_interpretation:
    1.25 @@ -102,6 +110,8 @@
    1.26  
    1.27  (* constants *)
    1.28  
    1.29 +fun typ_equiv tys = Type.raw_instance tys andalso Type.raw_instance (swap tys);
    1.30 +
    1.31  fun check_bare_const thy t = case try dest_Const t
    1.32   of SOME c_ty => c_ty
    1.33    | NONE => error ("Not a constant: " ^ Syntax.string_of_term_global thy t);
    1.34 @@ -147,6 +157,7 @@
    1.35  
    1.36  datatype spec = Spec of {
    1.37    history_concluded: bool,
    1.38 +  signatures: int Symtab.table * typ Symtab.table,
    1.39    eqns: ((bool * eqns) * (serial * eqns) list) Symtab.table
    1.40      (*with explicit history*),
    1.41    dtyps: ((serial * ((string * sort) list * (string * typ list) list)) list) Symtab.table
    1.42 @@ -154,16 +165,19 @@
    1.43    cases: (int * (int * string list)) Symtab.table * unit Symtab.table
    1.44  };
    1.45  
    1.46 -fun make_spec (history_concluded, (eqns, (dtyps, cases))) =
    1.47 -  Spec { history_concluded = history_concluded, eqns = eqns, dtyps = dtyps, cases = cases };
    1.48 -fun map_spec f (Spec { history_concluded = history_concluded, eqns = eqns,
    1.49 -  dtyps = dtyps, cases = cases }) =
    1.50 -  make_spec (f (history_concluded, (eqns, (dtyps, cases))));
    1.51 -fun merge_spec (Spec { history_concluded = _, eqns = eqns1,
    1.52 +fun make_spec (history_concluded, ((signatures, eqns), (dtyps, cases))) =
    1.53 +  Spec { history_concluded = history_concluded,
    1.54 +    signatures = signatures, eqns = eqns, dtyps = dtyps, cases = cases };
    1.55 +fun map_spec f (Spec { history_concluded = history_concluded, signatures = signatures,
    1.56 +  eqns = eqns, dtyps = dtyps, cases = cases }) =
    1.57 +  make_spec (f (history_concluded, ((signatures, eqns), (dtyps, cases))));
    1.58 +fun merge_spec (Spec { history_concluded = _, signatures = (tycos1, sigs1), eqns = eqns1,
    1.59      dtyps = dtyps1, cases = (cases1, undefs1) },
    1.60 -  Spec { history_concluded = _, eqns = eqns2,
    1.61 +  Spec { history_concluded = _, signatures = (tycos2, sigs2), eqns = eqns2,
    1.62      dtyps = dtyps2, cases = (cases2, undefs2) }) =
    1.63    let
    1.64 +    val signatures = (Symtab.merge (op =) (tycos1, tycos2),
    1.65 +      Symtab.merge typ_equiv (sigs1, sigs2));
    1.66      fun merge_eqns ((_, history1), (_, history2)) =
    1.67        let
    1.68          val raw_history = AList.merge (op = : serial * serial -> bool)
    1.69 @@ -176,14 +190,16 @@
    1.70      val dtyps = Symtab.join (K (AList.merge (op =) (K true))) (dtyps1, dtyps2);
    1.71      val cases = (Symtab.merge (K true) (cases1, cases2),
    1.72        Symtab.merge (K true) (undefs1, undefs2));
    1.73 -  in make_spec (false, (eqns, (dtyps, cases))) end;
    1.74 +  in make_spec (false, ((signatures, eqns), (dtyps, cases))) end;
    1.75  
    1.76  fun history_concluded (Spec { history_concluded, ... }) = history_concluded;
    1.77 +fun the_signatures (Spec { signatures, ... }) = signatures;
    1.78  fun the_eqns (Spec { eqns, ... }) = eqns;
    1.79  fun the_dtyps (Spec { dtyps, ... }) = dtyps;
    1.80  fun the_cases (Spec { cases, ... }) = cases;
    1.81  val map_history_concluded = map_spec o apfst;
    1.82 -val map_eqns = map_spec o apsnd o apfst;
    1.83 +val map_signatures = map_spec o apsnd o apfst o apfst;
    1.84 +val map_eqns = map_spec o apsnd o apfst o apsnd;
    1.85  val map_dtyps = map_spec o apsnd o apsnd o apfst;
    1.86  val map_cases = map_spec o apsnd o apsnd o apsnd;
    1.87  
    1.88 @@ -236,11 +252,11 @@
    1.89  structure Code_Data = TheoryDataFun
    1.90  (
    1.91    type T = spec * data Unsynchronized.ref;
    1.92 -  val empty = (make_spec (false,
    1.93 -    (Symtab.empty, (Symtab.empty, (Symtab.empty, Symtab.empty)))), Unsynchronized.ref empty_data);
    1.94 +  val empty = (make_spec (false, (((Symtab.empty, Symtab.empty), Symtab.empty),
    1.95 +    (Symtab.empty, (Symtab.empty, Symtab.empty)))), Unsynchronized.ref empty_data);
    1.96    fun copy (spec, data) = (spec, Unsynchronized.ref (! data));
    1.97    val extend = copy;
    1.98 -  fun merge pp ((spec1, data1), (spec2, data2)) =
    1.99 +  fun merge _ ((spec1, data1), (spec2, data2)) =
   1.100      (merge_spec (spec1, spec2), Unsynchronized.ref empty_data);
   1.101  );
   1.102  
   1.103 @@ -334,7 +350,44 @@
   1.104  
   1.105  (* constants *)
   1.106  
   1.107 -fun args_number thy = length o fst o strip_type o Sign.the_const_type thy;
   1.108 +fun arity_number thy tyco = case Symtab.lookup ((fst o the_signatures o the_exec) thy) tyco
   1.109 + of SOME n => n
   1.110 +  | NONE => Sign.arity_number thy tyco;
   1.111 +
   1.112 +fun build_tsig thy =
   1.113 +  let
   1.114 +    val (tycos, _) = (the_signatures o the_exec) thy;
   1.115 +    val decls = (#types o Type.rep_tsig o Sign.tsig_of) thy
   1.116 +      |> apsnd (Symtab.fold (fn (tyco, n) =>
   1.117 +          Symtab.update (tyco, Type.LogicalType n)) tycos);
   1.118 +  in Type.build_tsig ((Name_Space.empty "", Sorts.empty_algebra), [], decls) end;
   1.119 +
   1.120 +fun cert_signature thy = Logic.varifyT o Type.cert_typ (build_tsig thy) o Type.no_tvars;
   1.121 +
   1.122 +fun read_signature thy = cert_signature thy o Type.strip_sorts
   1.123 +  o Syntax.parse_typ (ProofContext.init thy);
   1.124 +
   1.125 +fun expand_signature thy = Type.cert_typ_mode Type.mode_syntax (Sign.tsig_of thy);
   1.126 +
   1.127 +fun lookup_typ thy = Symtab.lookup ((snd o the_signatures o the_exec) thy);
   1.128 +
   1.129 +fun const_typ thy c = case lookup_typ thy c
   1.130 + of SOME ty => ty
   1.131 +  | NONE => (Type.strip_sorts o Sign.the_const_type thy) c;
   1.132 +
   1.133 +fun subst_signature thy c ty =
   1.134 +  let
   1.135 +    fun mk_subst (Type (tyco, tys1)) (ty2 as Type (tyco2, tys2)) =
   1.136 +          fold2 mk_subst tys1 tys2
   1.137 +      | mk_subst ty (TVar (v, sort)) = Vartab.update (v, ([], ty))
   1.138 +  in case lookup_typ thy c
   1.139 +   of SOME ty' => Envir.subst_type (mk_subst ty (expand_signature thy ty') Vartab.empty) ty'
   1.140 +    | NONE => ty
   1.141 +  end;
   1.142 +
   1.143 +fun subst_signatures thy = map_aterms (fn Const (c, ty) => Const (c, subst_signature thy c ty) | t => t);
   1.144 +
   1.145 +fun args_number thy = length o fst o strip_type o const_typ thy;
   1.146  
   1.147  
   1.148  (* datatypes *)
   1.149 @@ -355,9 +408,10 @@
   1.150          val _ = if length tfrees <> length vs
   1.151            then no_constr "type variables missing in datatype" c_ty else ();
   1.152        in (tyco, vs) end;
   1.153 -    fun ty_sorts (c, ty) =
   1.154 +    fun ty_sorts (c, raw_ty) =
   1.155        let
   1.156 -        val ty_decl = (Logic.unvarifyT o Sign.the_const_type thy) c;
   1.157 +        val ty = subst_signature thy c raw_ty;
   1.158 +        val ty_decl = (Logic.unvarifyT o const_typ thy) c;
   1.159          val (tyco, _) = last_typ (c, ty) ty_decl;
   1.160          val (_, vs) = last_typ (c, ty) ty;
   1.161        in ((tyco, map snd vs), (c, (map fst vs, ty))) end;
   1.162 @@ -382,13 +436,13 @@
   1.163  fun get_datatype thy tyco =
   1.164    case these (Symtab.lookup ((the_dtyps o the_exec) thy) tyco)
   1.165     of (_, spec) :: _ => spec
   1.166 -    | [] => Sign.arity_number thy tyco
   1.167 +    | [] => arity_number thy tyco
   1.168          |> Name.invents Name.context Name.aT
   1.169          |> map (rpair [])
   1.170          |> rpair [];
   1.171  
   1.172  fun get_datatype_of_constr thy c =
   1.173 -  case (snd o strip_type o Sign.the_const_type thy) c
   1.174 +  case (snd o strip_type o const_typ thy) c
   1.175     of Type (tyco, _) => if member (op =) ((map fst o snd o get_datatype thy) tyco) c
   1.176         then SOME tyco else NONE
   1.177      | _ => NONE;
   1.178 @@ -446,21 +500,25 @@
   1.179            ("Variable with application on left hand side of equation\n"
   1.180              ^ Display.string_of_thm_global thy thm)
   1.181        | check n (t1 $ t2) = (check (n+1) t1; check 0 t2)
   1.182 -      | check n (Const (c_ty as (c, ty))) = if n = (length o fst o strip_type) ty
   1.183 -          then if not proper orelse is_constr_pat (AxClass.unoverload_const thy c_ty)
   1.184 -            then ()
   1.185 -            else bad_thm (quote c ^ " is not a constructor, on left hand side of equation\n"
   1.186 -              ^ Display.string_of_thm_global thy thm)
   1.187 -          else bad_thm
   1.188 -            ("Partially applied constant " ^ quote c ^ " on left hand side of equation\n"
   1.189 -               ^ Display.string_of_thm_global thy thm);
   1.190 +      | check n (Const (c_ty as (_, ty))) =
   1.191 +          let
   1.192 +            val c' = AxClass.unoverload_const thy c_ty
   1.193 +          in if n = (length o fst o strip_type o subst_signature thy c') ty
   1.194 +            then if not proper orelse is_constr_pat c'
   1.195 +              then ()
   1.196 +              else bad_thm (quote c ^ " is not a constructor, on left hand side of equation\n"
   1.197 +                ^ Display.string_of_thm_global thy thm)
   1.198 +            else bad_thm
   1.199 +              ("Partially applied constant " ^ quote c ^ " on left hand side of equation\n"
   1.200 +                 ^ Display.string_of_thm_global thy thm)
   1.201 +          end;
   1.202      val _ = map (check 0) args;
   1.203      val _ = if not proper orelse is_linear thm then ()
   1.204        else bad_thm ("Duplicate variables on left hand side of equation\n"
   1.205          ^ Display.string_of_thm_global thy thm);
   1.206      val _ = if (is_none o AxClass.class_of_param thy) c
   1.207        then ()
   1.208 -      else bad_thm ("Polymorphic constant as head in equation\n"
   1.209 +      else bad_thm ("Overloaded constant as head in equation\n"
   1.210          ^ Display.string_of_thm_global thy thm)
   1.211      val _ = if not (is_constr thy c)
   1.212        then ()
   1.213 @@ -488,29 +546,34 @@
   1.214  fun mk_eqn_liberal thy = Option.map (fn (thm, _) => (thm, is_linear thm))
   1.215    o try_thm (gen_assert_eqn thy (K true)) o rpair false o meta_rewrite thy;
   1.216  
   1.217 -(*those following are permissive wrt. to overloaded constants!*)
   1.218 +val head_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
   1.219  
   1.220 -val head_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
   1.221  fun const_typ_eqn thy thm =
   1.222    let
   1.223      val (c, ty) = head_eqn thm;
   1.224      val c' = AxClass.unoverload_const thy (c, ty);
   1.225 +      (*permissive wrt. to overloaded constants!*)
   1.226    in (c', ty) end;
   1.227 +
   1.228  fun const_eqn thy = fst o const_typ_eqn thy;
   1.229  
   1.230 -fun typscheme thy (c, ty) =
   1.231 +fun raw_typscheme thy (c, ty) =
   1.232    (map dest_TFree (Sign.const_typargs thy (c, ty)), Type.strip_sorts ty);
   1.233 +
   1.234 +fun typscheme thy (c, ty) = raw_typscheme thy (c, subst_signature thy c ty);
   1.235 +
   1.236  fun typscheme_eqn thy = typscheme thy o apsnd Logic.unvarifyT o const_typ_eqn thy;
   1.237 +
   1.238  fun typscheme_eqns thy c [] = 
   1.239        let
   1.240 -        val raw_ty = Sign.the_const_type thy c;
   1.241 +        val raw_ty = const_typ thy c;
   1.242          val tvars = Term.add_tvar_namesT raw_ty [];
   1.243          val tvars' = case AxClass.class_of_param thy c
   1.244           of SOME class => [TFree (Name.aT, [class])]
   1.245            | NONE => Name.invent_list [] Name.aT (length tvars)
   1.246                |> map (fn v => TFree (v, []));
   1.247          val ty = typ_subst_TVars (tvars ~~ tvars') raw_ty;
   1.248 -      in typscheme thy (c, ty) end
   1.249 +      in raw_typscheme thy (c, ty) end
   1.250    | typscheme_eqns thy c (thms as thm :: _) = typscheme_eqn thy thm;
   1.251  
   1.252  fun assert_eqns_const thy c eqns =
   1.253 @@ -639,6 +702,34 @@
   1.254  
   1.255  (** declaring executable ingredients **)
   1.256  
   1.257 +(* constant signatures *)
   1.258 +
   1.259 +fun add_type tyco thy =
   1.260 +  case Symtab.lookup ((snd o #types o Type.rep_tsig o Sign.tsig_of) thy) tyco
   1.261 +   of SOME (Type.Abbreviation (vs, _, _)) =>
   1.262 +          (map_exec_purge NONE o map_signatures o apfst)
   1.263 +            (Symtab.update (tyco, length vs)) thy
   1.264 +    | _ => error ("No such type abbreviation: " ^ quote tyco);
   1.265 +
   1.266 +fun add_type_cmd s thy = add_type (Sign.intern_type thy s) thy;
   1.267 +
   1.268 +fun gen_add_signature prep_const prep_signature (raw_c, raw_ty) thy =
   1.269 +  let
   1.270 +    val c = prep_const thy raw_c;
   1.271 +    val ty = prep_signature thy raw_ty;
   1.272 +    val ty' = expand_signature thy ty;
   1.273 +    val ty'' = Sign.the_const_type thy c;
   1.274 +    val _ = if typ_equiv (ty', ty'') then () else
   1.275 +      error ("Illegal constant signature: " ^ Syntax.string_of_typ_global thy ty);
   1.276 +  in
   1.277 +    thy
   1.278 +    |> (map_exec_purge NONE o map_signatures o apsnd) (Symtab.update (c, ty))
   1.279 +  end;
   1.280 +
   1.281 +val add_signature = gen_add_signature (K I) cert_signature;
   1.282 +val add_signature_cmd = gen_add_signature read_const read_signature;
   1.283 +
   1.284 +
   1.285  (* datatypes *)
   1.286  
   1.287  structure Type_Interpretation =