1.1 --- a/src/Pure/Isar/code.ML Fri Feb 20 18:29:10 2009 +0100
1.2 +++ b/src/Pure/Isar/code.ML Fri Feb 20 18:29:10 2009 +0100
1.3 @@ -35,7 +35,7 @@
1.4 val these_raw_eqns: theory -> string -> (thm * bool) list
1.5 val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list)
1.6 val get_datatype_of_constr: theory -> string -> string option
1.7 - val get_case_scheme: theory -> string -> (int * string list) option
1.8 + val get_case_scheme: theory -> string -> (int * (int * string list)) option
1.9 val is_undefined: theory -> string -> bool
1.10 val default_typscheme: theory -> string -> (string * sort) list * typ
1.11
1.12 @@ -111,7 +111,7 @@
1.13
1.14 (** logical and syntactical specification of executable code **)
1.15
1.16 -(* defining equations *)
1.17 +(* code equations *)
1.18
1.19 type eqns = bool * (thm * bool) list lazy;
1.20 (*default flag, theorems with linear flag (perhaps lazy)*)
1.21 @@ -136,7 +136,7 @@
1.22 Pattern.matchess thy (args, (map incr_idx o curry Library.take (length args)) args');
1.23 fun drop (thm', linear') = if (linear orelse not linear')
1.24 andalso matches_args (args_of thm') then
1.25 - (warning ("Code generator: dropping redundant defining equation\n" ^ Display.string_of_thm thm'); true)
1.26 + (warning ("Code generator: dropping redundant code equation\n" ^ Display.string_of_thm thm'); true)
1.27 else false;
1.28 in (thm, linear) :: filter_out drop thms end;
1.29
1.30 @@ -409,7 +409,7 @@
1.31 in
1.32 (Pretty.writeln o Pretty.chunks) [
1.33 Pretty.block (
1.34 - Pretty.str "defining equations:"
1.35 + Pretty.str "code equations:"
1.36 :: Pretty.fbrk
1.37 :: (Pretty.fbreaks o map pretty_eqn) eqns
1.38 ),
1.39 @@ -452,7 +452,7 @@
1.40 val ty1 :: tys = map (snd o Code_Unit.const_typ_eqn) thms';
1.41 fun unify ty env = Sign.typ_unify thy (ty1, ty) env
1.42 handle Type.TUNIFY =>
1.43 - error ("Type unificaton failed, while unifying defining equations\n"
1.44 + error ("Type unificaton failed, while unifying code equations\n"
1.45 ^ (cat_lines o map Display.string_of_thm) thms
1.46 ^ "\nwith types\n"
1.47 ^ (cat_lines o map (Code_Unit.string_of_typ thy)) (ty1 :: tys));
1.48 @@ -463,7 +463,7 @@
1.49
1.50 fun check_linear (eqn as (thm, linear)) =
1.51 if linear then eqn else Code_Unit.bad_thm
1.52 - ("Duplicate variables on left hand side of defining equation:\n"
1.53 + ("Duplicate variables on left hand side of code equation:\n"
1.54 ^ Display.string_of_thm thm);
1.55
1.56 fun mk_eqn thy linear =
1.57 @@ -525,22 +525,13 @@
1.58 then SOME tyco else NONE
1.59 | _ => NONE;
1.60
1.61 -fun get_constr_typ thy c =
1.62 - case get_datatype_of_constr thy c
1.63 - of SOME tyco => let
1.64 - val (vs, cos) = get_datatype thy tyco;
1.65 - val SOME tys = AList.lookup (op =) cos c;
1.66 - val ty = tys ---> Type (tyco, map TFree vs);
1.67 - in SOME (Logic.varifyT ty) end
1.68 - | NONE => NONE;
1.69 -
1.70 fun recheck_eqn thy = Code_Unit.error_thm
1.71 (Code_Unit.assert_linear (is_some o get_datatype_of_constr thy) o apfst (Code_Unit.assert_eqn thy));
1.72
1.73 fun recheck_eqns_const thy c eqns =
1.74 let
1.75 fun cert (eqn as (thm, _)) = if c = Code_Unit.const_eqn thm
1.76 - then eqn else error ("Wrong head of defining equation,\nexpected constant "
1.77 + then eqn else error ("Wrong head of code equation,\nexpected constant "
1.78 ^ Code_Unit.string_of_const thy c ^ "\n" ^ Display.string_of_thm thm)
1.79 in map (cert o recheck_eqn thy) eqns end;
1.80
1.81 @@ -554,11 +545,11 @@
1.82 let
1.83 val c = Code_Unit.const_eqn thm;
1.84 val _ = if not default andalso (is_some o AxClass.class_of_param thy) c
1.85 - then error ("Rejected polymorphic equation for overloaded constant:\n"
1.86 + then error ("Rejected polymorphic code equation for overloaded constant:\n"
1.87 ^ Display.string_of_thm thm)
1.88 else ();
1.89 val _ = if not default andalso (is_some o get_datatype_of_constr thy) c
1.90 - then error ("Rejected equation for datatype constructor:\n"
1.91 + then error ("Rejected code equation for datatype constructor:\n"
1.92 ^ Display.string_of_thm thm)
1.93 else ();
1.94 in change_eqns false c (add_thm thy default (thm, linear)) thy end
1.95 @@ -583,7 +574,12 @@
1.96
1.97 fun del_eqns c = change_eqns true c (K (false, Lazy.value []));
1.98
1.99 -fun get_case_scheme thy = Symtab.lookup ((fst o the_cases o the_exec) thy);
1.100 +fun get_case_scheme thy c = case Symtab.lookup ((fst o the_cases o the_exec) thy) c
1.101 + of SOME (base_case_scheme as (_, case_pats)) =>
1.102 + if forall (is_some o get_datatype_of_constr thy) case_pats
1.103 + then SOME (1 + Int.max (1, length case_pats), base_case_scheme)
1.104 + else NONE
1.105 + | NONE => NONE;
1.106
1.107 val is_undefined = Symtab.defined o snd o the_cases o the_exec;
1.108
1.109 @@ -727,18 +723,16 @@
1.110
1.111 fun default_typscheme thy c =
1.112 let
1.113 - val typscheme = curry (Code_Unit.typscheme thy) c
1.114 - val the_const_type = snd o dest_Const o TermSubst.zero_var_indexes
1.115 - o curry Const "" o Sign.the_const_type thy;
1.116 + fun the_const_typscheme c = (curry (Code_Unit.typscheme thy) c o snd o dest_Const
1.117 + o TermSubst.zero_var_indexes o curry Const "" o Sign.the_const_type thy) c;
1.118 + fun strip_sorts (vs, ty) = (map (fn (v, _) => (v, [])) vs, ty);
1.119 in case AxClass.class_of_param thy c
1.120 - of SOME class => the_const_type c
1.121 - |> Term.map_type_tvar (K (TVar ((Name.aT, 0), [class])))
1.122 - |> typscheme
1.123 - | NONE => (case get_constr_typ thy c
1.124 - of SOME ty => typscheme ty
1.125 - | NONE => (case get_eqns thy c
1.126 - of (thm, _) :: _ => snd (Code_Unit.head_eqn thy (Drule.zero_var_indexes thm))
1.127 - | [] => typscheme (the_const_type c))) end;
1.128 + of SOME class => ([(Name.aT, [class])], snd (the_const_typscheme c))
1.129 + | NONE => if is_some (get_datatype_of_constr thy c)
1.130 + then strip_sorts (the_const_typscheme c)
1.131 + else case get_eqns thy c
1.132 + of (thm, _) :: _ => snd (Code_Unit.head_eqn thy (Drule.zero_var_indexes thm))
1.133 + | [] => strip_sorts (the_const_typscheme c) end;
1.134
1.135 end; (*local*)
1.136