# HG changeset patch # User haftmann # Date 1235150950 -3600 # Node ID 55954f7260431a8c68ecebaf941d54fdfda37b59 # Parent 1d8b8fa190741656397d9dcda3d0ad0f30cf2159 permissive check for pattern discipline in case schemes diff -r 1d8b8fa19074 -r 55954f726043 src/Pure/Isar/code.ML --- 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*) diff -r 1d8b8fa19074 -r 55954f726043 src/Tools/code/code_thingol.ML --- 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;