merged
authorhaftmann
Fri Dec 04 12:22:09 2009 +0100 (2009-12-04)
changeset 33972daf65be6bfe5
parent 33971 9c7fa7f76950
parent 33951 651028e34b5d
child 33973 78c0842510cb
merged
src/HOL/IsaMakefile
src/HOL/List.thy
src/Pure/Isar/code.ML
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/HOL/IsaMakefile	Fri Dec 04 12:17:43 2009 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Fri Dec 04 12:22:09 2009 +0100
     1.3 @@ -369,6 +369,7 @@
     1.4    Library/Sum_Of_Squares/sos_wrapper.ML					\
     1.5    Library/Sum_Of_Squares/sum_of_squares.ML Library/Fset.thy		\
     1.6    Library/Glbs.thy Library/normarith.ML Library/Executable_Set.thy	\
     1.7 +  Library/Crude_Executable_Set.thy					\
     1.8    Library/Infinite_Set.thy Library/FuncSet.thy				\
     1.9    Library/Permutations.thy Library/Bit.thy Library/FrechetDeriv.thy	\
    1.10    Library/Fraction_Field.thy Library/Fundamental_Theorem_Algebra.thy	\
    1.11 @@ -381,9 +382,9 @@
    1.12    Library/Order_Relation.thy Library/Nested_Environment.thy		\
    1.13    Library/Ramsey.thy Library/Zorn.thy Library/Library/ROOT.ML		\
    1.14    Library/Library/document/root.tex Library/Library/document/root.bib	\
    1.15 -  Library/Transitive_Closure_Table.thy Library/While_Combinator.thy \
    1.16 -  Library/Product_ord.thy	Library/Char_nat.thy \
    1.17 -  Library/Char_ord.thy Library/Option_ord.thy	\
    1.18 +  Library/Transitive_Closure_Table.thy Library/While_Combinator.thy	\
    1.19 +  Library/Product_ord.thy Library/Char_nat.thy				\
    1.20 +  Library/Char_ord.thy Library/Option_ord.thy				\
    1.21    Library/Sublist_Order.thy Library/List_lexord.thy			\
    1.22    Library/Coinductive_List.thy Library/AssocList.thy			\
    1.23    Library/Formal_Power_Series.thy Library/Binomial.thy			\
     2.1 --- a/src/HOL/List.thy	Fri Dec 04 12:17:43 2009 +0100
     2.2 +++ b/src/HOL/List.thy	Fri Dec 04 12:22:09 2009 +0100
     2.3 @@ -2665,6 +2665,10 @@
     2.4  apply(rule length_remdups_leq)
     2.5  done
     2.6  
     2.7 +lemma remdups_filter: "remdups(filter P xs) = filter P (remdups xs)"
     2.8 +apply(induct xs)
     2.9 +apply auto
    2.10 +done
    2.11  
    2.12  lemma distinct_map:
    2.13    "distinct(map f xs) = (distinct xs & inj_on f (set xs))"
     3.1 --- a/src/Pure/Isar/code.ML	Fri Dec 04 12:17:43 2009 +0100
     3.2 +++ b/src/Pure/Isar/code.ML	Fri Dec 04 12:22:09 2009 +0100
     3.3 @@ -12,6 +12,10 @@
     3.4    val read_bare_const: theory -> string -> string * typ
     3.5    val read_const: theory -> string -> string
     3.6    val string_of_const: theory -> string -> string
     3.7 +  val cert_signature: theory -> typ -> typ
     3.8 +  val read_signature: theory -> string -> typ
     3.9 +  val const_typ: theory -> string -> typ
    3.10 +  val subst_signatures: theory -> term -> term
    3.11    val args_number: theory -> string -> int
    3.12  
    3.13    (*constructor sets*)
    3.14 @@ -31,6 +35,10 @@
    3.15    val standard_typscheme: theory -> thm list -> thm list
    3.16  
    3.17    (*executable code*)
    3.18 +  val add_type: string -> theory -> theory
    3.19 +  val add_type_cmd: string -> theory -> theory
    3.20 +  val add_signature: string * typ -> theory -> theory
    3.21 +  val add_signature_cmd: string * string -> theory -> theory
    3.22    val add_datatype: (string * typ) list -> theory -> theory
    3.23    val add_datatype_cmd: string list -> theory -> theory
    3.24    val type_interpretation:
    3.25 @@ -102,6 +110,8 @@
    3.26  
    3.27  (* constants *)
    3.28  
    3.29 +fun typ_equiv tys = Type.raw_instance tys andalso Type.raw_instance (swap tys);
    3.30 +
    3.31  fun check_bare_const thy t = case try dest_Const t
    3.32   of SOME c_ty => c_ty
    3.33    | NONE => error ("Not a constant: " ^ Syntax.string_of_term_global thy t);
    3.34 @@ -147,6 +157,7 @@
    3.35  
    3.36  datatype spec = Spec of {
    3.37    history_concluded: bool,
    3.38 +  signatures: int Symtab.table * typ Symtab.table,
    3.39    eqns: ((bool * eqns) * (serial * eqns) list) Symtab.table
    3.40      (*with explicit history*),
    3.41    dtyps: ((serial * ((string * sort) list * (string * typ list) list)) list) Symtab.table
    3.42 @@ -154,16 +165,19 @@
    3.43    cases: (int * (int * string list)) Symtab.table * unit Symtab.table
    3.44  };
    3.45  
    3.46 -fun make_spec (history_concluded, (eqns, (dtyps, cases))) =
    3.47 -  Spec { history_concluded = history_concluded, eqns = eqns, dtyps = dtyps, cases = cases };
    3.48 -fun map_spec f (Spec { history_concluded = history_concluded, eqns = eqns,
    3.49 -  dtyps = dtyps, cases = cases }) =
    3.50 -  make_spec (f (history_concluded, (eqns, (dtyps, cases))));
    3.51 -fun merge_spec (Spec { history_concluded = _, eqns = eqns1,
    3.52 +fun make_spec (history_concluded, ((signatures, eqns), (dtyps, cases))) =
    3.53 +  Spec { history_concluded = history_concluded,
    3.54 +    signatures = signatures, eqns = eqns, dtyps = dtyps, cases = cases };
    3.55 +fun map_spec f (Spec { history_concluded = history_concluded, signatures = signatures,
    3.56 +  eqns = eqns, dtyps = dtyps, cases = cases }) =
    3.57 +  make_spec (f (history_concluded, ((signatures, eqns), (dtyps, cases))));
    3.58 +fun merge_spec (Spec { history_concluded = _, signatures = (tycos1, sigs1), eqns = eqns1,
    3.59      dtyps = dtyps1, cases = (cases1, undefs1) },
    3.60 -  Spec { history_concluded = _, eqns = eqns2,
    3.61 +  Spec { history_concluded = _, signatures = (tycos2, sigs2), eqns = eqns2,
    3.62      dtyps = dtyps2, cases = (cases2, undefs2) }) =
    3.63    let
    3.64 +    val signatures = (Symtab.merge (op =) (tycos1, tycos2),
    3.65 +      Symtab.merge typ_equiv (sigs1, sigs2));
    3.66      fun merge_eqns ((_, history1), (_, history2)) =
    3.67        let
    3.68          val raw_history = AList.merge (op = : serial * serial -> bool)
    3.69 @@ -176,14 +190,16 @@
    3.70      val dtyps = Symtab.join (K (AList.merge (op =) (K true))) (dtyps1, dtyps2);
    3.71      val cases = (Symtab.merge (K true) (cases1, cases2),
    3.72        Symtab.merge (K true) (undefs1, undefs2));
    3.73 -  in make_spec (false, (eqns, (dtyps, cases))) end;
    3.74 +  in make_spec (false, ((signatures, eqns), (dtyps, cases))) end;
    3.75  
    3.76  fun history_concluded (Spec { history_concluded, ... }) = history_concluded;
    3.77 +fun the_signatures (Spec { signatures, ... }) = signatures;
    3.78  fun the_eqns (Spec { eqns, ... }) = eqns;
    3.79  fun the_dtyps (Spec { dtyps, ... }) = dtyps;
    3.80  fun the_cases (Spec { cases, ... }) = cases;
    3.81  val map_history_concluded = map_spec o apfst;
    3.82 -val map_eqns = map_spec o apsnd o apfst;
    3.83 +val map_signatures = map_spec o apsnd o apfst o apfst;
    3.84 +val map_eqns = map_spec o apsnd o apfst o apsnd;
    3.85  val map_dtyps = map_spec o apsnd o apsnd o apfst;
    3.86  val map_cases = map_spec o apsnd o apsnd o apsnd;
    3.87  
    3.88 @@ -236,8 +252,8 @@
    3.89  structure Code_Data = TheoryDataFun
    3.90  (
    3.91    type T = spec * data Unsynchronized.ref;
    3.92 -  val empty = (make_spec (false,
    3.93 -    (Symtab.empty, (Symtab.empty, (Symtab.empty, Symtab.empty)))), Unsynchronized.ref empty_data);
    3.94 +  val empty = (make_spec (false, (((Symtab.empty, Symtab.empty), Symtab.empty),
    3.95 +    (Symtab.empty, (Symtab.empty, Symtab.empty)))), Unsynchronized.ref empty_data);
    3.96    fun copy (spec, data) = (spec, Unsynchronized.ref (! data));
    3.97    val extend = copy;
    3.98    fun merge _ ((spec1, _), (spec2, _)) =
    3.99 @@ -334,7 +350,44 @@
   3.100  
   3.101  (* constants *)
   3.102  
   3.103 -fun args_number thy = length o fst o strip_type o Sign.the_const_type thy;
   3.104 +fun arity_number thy tyco = case Symtab.lookup ((fst o the_signatures o the_exec) thy) tyco
   3.105 + of SOME n => n
   3.106 +  | NONE => Sign.arity_number thy tyco;
   3.107 +
   3.108 +fun build_tsig thy =
   3.109 +  let
   3.110 +    val (tycos, _) = (the_signatures o the_exec) thy;
   3.111 +    val decls = (#types o Type.rep_tsig o Sign.tsig_of) thy
   3.112 +      |> apsnd (Symtab.fold (fn (tyco, n) =>
   3.113 +          Symtab.update (tyco, Type.LogicalType n)) tycos);
   3.114 +  in Type.build_tsig ((Name_Space.empty "", Sorts.empty_algebra), [], decls) end;
   3.115 +
   3.116 +fun cert_signature thy = Logic.varifyT o Type.cert_typ (build_tsig thy) o Type.no_tvars;
   3.117 +
   3.118 +fun read_signature thy = cert_signature thy o Type.strip_sorts
   3.119 +  o Syntax.parse_typ (ProofContext.init thy);
   3.120 +
   3.121 +fun expand_signature thy = Type.cert_typ_mode Type.mode_syntax (Sign.tsig_of thy);
   3.122 +
   3.123 +fun lookup_typ thy = Symtab.lookup ((snd o the_signatures o the_exec) thy);
   3.124 +
   3.125 +fun const_typ thy c = case lookup_typ thy c
   3.126 + of SOME ty => ty
   3.127 +  | NONE => (Type.strip_sorts o Sign.the_const_type thy) c;
   3.128 +
   3.129 +fun subst_signature thy c ty =
   3.130 +  let
   3.131 +    fun mk_subst (Type (tyco, tys1)) (ty2 as Type (tyco2, tys2)) =
   3.132 +          fold2 mk_subst tys1 tys2
   3.133 +      | mk_subst ty (TVar (v, sort)) = Vartab.update (v, ([], ty))
   3.134 +  in case lookup_typ thy c
   3.135 +   of SOME ty' => Envir.subst_type (mk_subst ty (expand_signature thy ty') Vartab.empty) ty'
   3.136 +    | NONE => ty
   3.137 +  end;
   3.138 +
   3.139 +fun subst_signatures thy = map_aterms (fn Const (c, ty) => Const (c, subst_signature thy c ty) | t => t);
   3.140 +
   3.141 +fun args_number thy = length o fst o strip_type o const_typ thy;
   3.142  
   3.143  
   3.144  (* datatypes *)
   3.145 @@ -355,9 +408,10 @@
   3.146          val _ = if length tfrees <> length vs
   3.147            then no_constr "type variables missing in datatype" c_ty else ();
   3.148        in (tyco, vs) end;
   3.149 -    fun ty_sorts (c, ty) =
   3.150 +    fun ty_sorts (c, raw_ty) =
   3.151        let
   3.152 -        val ty_decl = (Logic.unvarifyT o Sign.the_const_type thy) c;
   3.153 +        val ty = subst_signature thy c raw_ty;
   3.154 +        val ty_decl = (Logic.unvarifyT o const_typ thy) c;
   3.155          val (tyco, _) = last_typ (c, ty) ty_decl;
   3.156          val (_, vs) = last_typ (c, ty) ty;
   3.157        in ((tyco, map snd vs), (c, (map fst vs, ty))) end;
   3.158 @@ -382,13 +436,13 @@
   3.159  fun get_datatype thy tyco =
   3.160    case these (Symtab.lookup ((the_dtyps o the_exec) thy) tyco)
   3.161     of (_, spec) :: _ => spec
   3.162 -    | [] => Sign.arity_number thy tyco
   3.163 +    | [] => arity_number thy tyco
   3.164          |> Name.invents Name.context Name.aT
   3.165          |> map (rpair [])
   3.166          |> rpair [];
   3.167  
   3.168  fun get_datatype_of_constr thy c =
   3.169 -  case (snd o strip_type o Sign.the_const_type thy) c
   3.170 +  case (snd o strip_type o const_typ thy) c
   3.171     of Type (tyco, _) => if member (op =) ((map fst o snd o get_datatype thy) tyco) c
   3.172         then SOME tyco else NONE
   3.173      | _ => NONE;
   3.174 @@ -446,21 +500,25 @@
   3.175            ("Variable with application on left hand side of equation\n"
   3.176              ^ Display.string_of_thm_global thy thm)
   3.177        | check n (t1 $ t2) = (check (n+1) t1; check 0 t2)
   3.178 -      | check n (Const (c_ty as (c, ty))) = if n = (length o fst o strip_type) ty
   3.179 -          then if not proper orelse is_constr_pat (AxClass.unoverload_const thy c_ty)
   3.180 -            then ()
   3.181 -            else bad_thm (quote c ^ " is not a constructor, on left hand side of equation\n"
   3.182 -              ^ Display.string_of_thm_global thy thm)
   3.183 -          else bad_thm
   3.184 -            ("Partially applied constant " ^ quote c ^ " on left hand side of equation\n"
   3.185 -               ^ Display.string_of_thm_global thy thm);
   3.186 +      | check n (Const (c_ty as (_, ty))) =
   3.187 +          let
   3.188 +            val c' = AxClass.unoverload_const thy c_ty
   3.189 +          in if n = (length o fst o strip_type o subst_signature thy c') ty
   3.190 +            then if not proper orelse is_constr_pat c'
   3.191 +              then ()
   3.192 +              else bad_thm (quote c ^ " is not a constructor, on left hand side of equation\n"
   3.193 +                ^ Display.string_of_thm_global thy thm)
   3.194 +            else bad_thm
   3.195 +              ("Partially applied constant " ^ quote c ^ " on left hand side of equation\n"
   3.196 +                 ^ Display.string_of_thm_global thy thm)
   3.197 +          end;
   3.198      val _ = map (check 0) args;
   3.199      val _ = if not proper orelse is_linear thm then ()
   3.200        else bad_thm ("Duplicate variables on left hand side of equation\n"
   3.201          ^ Display.string_of_thm_global thy thm);
   3.202      val _ = if (is_none o AxClass.class_of_param thy) c
   3.203        then ()
   3.204 -      else bad_thm ("Polymorphic constant as head in equation\n"
   3.205 +      else bad_thm ("Overloaded constant as head in equation\n"
   3.206          ^ Display.string_of_thm_global thy thm)
   3.207      val _ = if not (is_constr thy c)
   3.208        then ()
   3.209 @@ -488,29 +546,34 @@
   3.210  fun mk_eqn_liberal thy = Option.map (fn (thm, _) => (thm, is_linear thm))
   3.211    o try_thm (gen_assert_eqn thy (K true)) o rpair false o meta_rewrite thy;
   3.212  
   3.213 -(*those following are permissive wrt. to overloaded constants!*)
   3.214 +val head_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
   3.215  
   3.216 -val head_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
   3.217  fun const_typ_eqn thy thm =
   3.218    let
   3.219      val (c, ty) = head_eqn thm;
   3.220      val c' = AxClass.unoverload_const thy (c, ty);
   3.221 +      (*permissive wrt. to overloaded constants!*)
   3.222    in (c', ty) end;
   3.223 +
   3.224  fun const_eqn thy = fst o const_typ_eqn thy;
   3.225  
   3.226 -fun typscheme thy (c, ty) =
   3.227 +fun raw_typscheme thy (c, ty) =
   3.228    (map dest_TFree (Sign.const_typargs thy (c, ty)), Type.strip_sorts ty);
   3.229 +
   3.230 +fun typscheme thy (c, ty) = raw_typscheme thy (c, subst_signature thy c ty);
   3.231 +
   3.232  fun typscheme_eqn thy = typscheme thy o apsnd Logic.unvarifyT o const_typ_eqn thy;
   3.233 +
   3.234  fun typscheme_eqns thy c [] = 
   3.235        let
   3.236 -        val raw_ty = Sign.the_const_type thy c;
   3.237 +        val raw_ty = const_typ thy c;
   3.238          val tvars = Term.add_tvar_namesT raw_ty [];
   3.239          val tvars' = case AxClass.class_of_param thy c
   3.240           of SOME class => [TFree (Name.aT, [class])]
   3.241            | NONE => Name.invent_list [] Name.aT (length tvars)
   3.242                |> map (fn v => TFree (v, []));
   3.243          val ty = typ_subst_TVars (tvars ~~ tvars') raw_ty;
   3.244 -      in typscheme thy (c, ty) end
   3.245 +      in raw_typscheme thy (c, ty) end
   3.246    | typscheme_eqns thy c (thm :: _) = typscheme_eqn thy thm;
   3.247  
   3.248  fun assert_eqns_const thy c eqns =
   3.249 @@ -639,6 +702,34 @@
   3.250  
   3.251  (** declaring executable ingredients **)
   3.252  
   3.253 +(* constant signatures *)
   3.254 +
   3.255 +fun add_type tyco thy =
   3.256 +  case Symtab.lookup ((snd o #types o Type.rep_tsig o Sign.tsig_of) thy) tyco
   3.257 +   of SOME (Type.Abbreviation (vs, _, _)) =>
   3.258 +          (map_exec_purge NONE o map_signatures o apfst)
   3.259 +            (Symtab.update (tyco, length vs)) thy
   3.260 +    | _ => error ("No such type abbreviation: " ^ quote tyco);
   3.261 +
   3.262 +fun add_type_cmd s thy = add_type (Sign.intern_type thy s) thy;
   3.263 +
   3.264 +fun gen_add_signature prep_const prep_signature (raw_c, raw_ty) thy =
   3.265 +  let
   3.266 +    val c = prep_const thy raw_c;
   3.267 +    val ty = prep_signature thy raw_ty;
   3.268 +    val ty' = expand_signature thy ty;
   3.269 +    val ty'' = Sign.the_const_type thy c;
   3.270 +    val _ = if typ_equiv (ty', ty'') then () else
   3.271 +      error ("Illegal constant signature: " ^ Syntax.string_of_typ_global thy ty);
   3.272 +  in
   3.273 +    thy
   3.274 +    |> (map_exec_purge NONE o map_signatures o apsnd) (Symtab.update (c, ty))
   3.275 +  end;
   3.276 +
   3.277 +val add_signature = gen_add_signature (K I) cert_signature;
   3.278 +val add_signature_cmd = gen_add_signature read_const read_signature;
   3.279 +
   3.280 +
   3.281  (* datatypes *)
   3.282  
   3.283  structure Type_Interpretation =
     4.1 --- a/src/Tools/Code/code_thingol.ML	Fri Dec 04 12:17:43 2009 +0100
     4.2 +++ b/src/Tools/Code/code_thingol.ML	Fri Dec 04 12:22:09 2009 +0100
     4.3 @@ -711,7 +711,7 @@
     4.4  and translate_eqn thy algbr eqngr (thm, proper) =
     4.5    let
     4.6      val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
     4.7 -      o Logic.unvarify o prop_of) thm;
     4.8 +      o Code.subst_signatures thy o Logic.unvarify o prop_of) thm;
     4.9    in
    4.10      fold_map (translate_term thy algbr eqngr (SOME thm)) args
    4.11      ##>> translate_term thy algbr eqngr (SOME thm) rhs
    4.12 @@ -888,7 +888,7 @@
    4.13      val stmt_value =
    4.14        fold_map (translate_tyvar_sort thy algbr eqngr) vs
    4.15        ##>> translate_typ thy algbr eqngr ty
    4.16 -      ##>> translate_term thy algbr eqngr NONE t
    4.17 +      ##>> translate_term thy algbr eqngr NONE (Code.subst_signatures thy t)
    4.18        #>> (fn ((vs, ty), t) => Fun
    4.19          (Term.dummy_patternN, ((vs, ty), [(([], t), (Drule.dummy_thm, true))])));
    4.20      fun term_value (dep, (naming, program1)) =