--- a/src/Pure/Isar/code.ML Fri Feb 20 18:29:10 2009 +0100
+++ b/src/Pure/Isar/code.ML Fri Feb 20 18:29:10 2009 +0100
@@ -35,7 +35,7 @@
val these_raw_eqns: theory -> string -> (thm * bool) list
val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list)
val get_datatype_of_constr: theory -> string -> string option
- val get_case_scheme: theory -> string -> (int * string list) option
+ val get_case_scheme: theory -> string -> (int * (int * string list)) option
val is_undefined: theory -> string -> bool
val default_typscheme: theory -> string -> (string * sort) list * typ
@@ -111,7 +111,7 @@
(** logical and syntactical specification of executable code **)
-(* defining equations *)
+(* code equations *)
type eqns = bool * (thm * bool) list lazy;
(*default flag, theorems with linear flag (perhaps lazy)*)
@@ -136,7 +136,7 @@
Pattern.matchess thy (args, (map incr_idx o curry Library.take (length args)) args');
fun drop (thm', linear') = if (linear orelse not linear')
andalso matches_args (args_of thm') then
- (warning ("Code generator: dropping redundant defining equation\n" ^ Display.string_of_thm thm'); true)
+ (warning ("Code generator: dropping redundant code equation\n" ^ Display.string_of_thm thm'); true)
else false;
in (thm, linear) :: filter_out drop thms end;
@@ -409,7 +409,7 @@
in
(Pretty.writeln o Pretty.chunks) [
Pretty.block (
- Pretty.str "defining equations:"
+ Pretty.str "code equations:"
:: Pretty.fbrk
:: (Pretty.fbreaks o map pretty_eqn) eqns
),
@@ -452,7 +452,7 @@
val ty1 :: tys = map (snd o Code_Unit.const_typ_eqn) thms';
fun unify ty env = Sign.typ_unify thy (ty1, ty) env
handle Type.TUNIFY =>
- error ("Type unificaton failed, while unifying defining equations\n"
+ error ("Type unificaton failed, while unifying code equations\n"
^ (cat_lines o map Display.string_of_thm) thms
^ "\nwith types\n"
^ (cat_lines o map (Code_Unit.string_of_typ thy)) (ty1 :: tys));
@@ -463,7 +463,7 @@
fun check_linear (eqn as (thm, linear)) =
if linear then eqn else Code_Unit.bad_thm
- ("Duplicate variables on left hand side of defining equation:\n"
+ ("Duplicate variables on left hand side of code equation:\n"
^ Display.string_of_thm thm);
fun mk_eqn thy linear =
@@ -525,22 +525,13 @@
then SOME tyco else NONE
| _ => NONE;
-fun get_constr_typ thy c =
- case get_datatype_of_constr thy c
- of SOME tyco => let
- val (vs, cos) = get_datatype thy tyco;
- val SOME tys = AList.lookup (op =) cos c;
- val ty = tys ---> Type (tyco, map TFree vs);
- in SOME (Logic.varifyT ty) end
- | NONE => NONE;
-
fun recheck_eqn thy = Code_Unit.error_thm
(Code_Unit.assert_linear (is_some o get_datatype_of_constr thy) o apfst (Code_Unit.assert_eqn thy));
fun recheck_eqns_const thy c eqns =
let
fun cert (eqn as (thm, _)) = if c = Code_Unit.const_eqn thm
- then eqn else error ("Wrong head of defining equation,\nexpected constant "
+ then eqn else error ("Wrong head of code equation,\nexpected constant "
^ Code_Unit.string_of_const thy c ^ "\n" ^ Display.string_of_thm thm)
in map (cert o recheck_eqn thy) eqns end;
@@ -554,11 +545,11 @@
let
val c = Code_Unit.const_eqn thm;
val _ = if not default andalso (is_some o AxClass.class_of_param thy) c
- then error ("Rejected polymorphic equation for overloaded constant:\n"
+ then error ("Rejected polymorphic code equation for overloaded constant:\n"
^ Display.string_of_thm thm)
else ();
val _ = if not default andalso (is_some o get_datatype_of_constr thy) c
- then error ("Rejected equation for datatype constructor:\n"
+ then error ("Rejected code equation for datatype constructor:\n"
^ Display.string_of_thm thm)
else ();
in change_eqns false c (add_thm thy default (thm, linear)) thy end
@@ -583,7 +574,12 @@
fun del_eqns c = change_eqns true c (K (false, Lazy.value []));
-fun get_case_scheme thy = Symtab.lookup ((fst o the_cases o the_exec) thy);
+fun get_case_scheme thy c = case Symtab.lookup ((fst o the_cases o the_exec) thy) c
+ of SOME (base_case_scheme as (_, case_pats)) =>
+ if forall (is_some o get_datatype_of_constr thy) case_pats
+ then SOME (1 + Int.max (1, length case_pats), base_case_scheme)
+ else NONE
+ | NONE => NONE;
val is_undefined = Symtab.defined o snd o the_cases o the_exec;
@@ -727,18 +723,16 @@
fun default_typscheme thy c =
let
- val typscheme = curry (Code_Unit.typscheme thy) c
- val the_const_type = snd o dest_Const o TermSubst.zero_var_indexes
- o curry Const "" o Sign.the_const_type thy;
+ fun the_const_typscheme c = (curry (Code_Unit.typscheme thy) c o snd o dest_Const
+ o TermSubst.zero_var_indexes o curry Const "" o Sign.the_const_type thy) c;
+ fun strip_sorts (vs, ty) = (map (fn (v, _) => (v, [])) vs, ty);
in case AxClass.class_of_param thy c
- of SOME class => the_const_type c
- |> Term.map_type_tvar (K (TVar ((Name.aT, 0), [class])))
- |> typscheme
- | NONE => (case get_constr_typ thy c
- of SOME ty => typscheme ty
- | NONE => (case get_eqns thy c
- of (thm, _) :: _ => snd (Code_Unit.head_eqn thy (Drule.zero_var_indexes thm))
- | [] => typscheme (the_const_type c))) end;
+ of SOME class => ([(Name.aT, [class])], snd (the_const_typscheme c))
+ | NONE => if is_some (get_datatype_of_constr thy c)
+ then strip_sorts (the_const_typscheme c)
+ else case get_eqns thy c
+ of (thm, _) :: _ => snd (Code_Unit.head_eqn thy (Drule.zero_var_indexes thm))
+ | [] => strip_sorts (the_const_typscheme c) end;
end; (*local*)
--- a/src/Tools/code/code_thingol.ML Fri Feb 20 18:29:10 2009 +0100
+++ b/src/Tools/code/code_thingol.ML Fri Feb 20 18:29:10 2009 +0100
@@ -453,7 +453,7 @@
let
val err_class = Sorts.class_error (Syntax.pp_global thy) e;
val err_thm = case thm
- of SOME thm => "\n(in defining equation " ^ Display.string_of_thm thm ^ ")" | NONE => "";
+ of SOME thm => "\n(in code equation " ^ Display.string_of_thm thm ^ ")" | NONE => "";
val err_typ = "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort "
^ Syntax.string_of_sort_global thy sort;
in error ("Wellsortedness error" ^ err_thm ^ ":\n" ^ err_typ ^ "\n" ^ err_class) end;
@@ -582,9 +582,8 @@
fun stmt_classparam class =
ensure_class thy algbr funcgr class
#>> (fn class => Classparam (c, class));
- fun stmt_fun ((vs, raw_ty), raw_thms) =
+ fun stmt_fun ((vs, ty), raw_thms) =
let
- val ty = Logic.unvarifyT raw_ty; (*FIXME change convention here*)
val thms = if null (Term.add_tfreesT ty []) orelse (null o fst o strip_type) ty
then raw_thms
else (map o apfst) (Code_Unit.expand_eta thy 1) raw_thms;
@@ -643,11 +642,6 @@
val ts_clause = nth_drop t_pos ts;
fun mk_clause (co, num_co_args) t =
let
- val _ = if (is_some o Code.get_datatype_of_constr thy) co then ()
- else error ("Non-constructor " ^ quote co
- ^ " encountered in case pattern"
- ^ (case thm of NONE => ""
- | SOME thm => ", in equation\n" ^ Display.string_of_thm thm))
val (vs, body) = Term.strip_abs_eta num_co_args t;
val not_undefined = case body
of (Const (c, _)) => not (Code.is_undefined thy c)
@@ -702,9 +696,7 @@
translate_case thy algbr funcgr thm case_scheme ((c, ty), ts)
and translate_app thy algbr funcgr thm (c_ty_ts as ((c, _), _)) =
case Code.get_case_scheme thy c
- of SOME (base_case_scheme as (_, case_pats)) =>
- translate_app_case thy algbr funcgr thm
- (1 + Int.max (1, length case_pats), base_case_scheme) c_ty_ts
+ of SOME case_scheme => translate_app_case thy algbr funcgr thm case_scheme c_ty_ts
| NONE => translate_app_const thy algbr funcgr thm c_ty_ts;