permissive check for pattern discipline in case schemes
authorhaftmann
Fri Feb 20 18:29:10 2009 +0100 (2009-02-20)
changeset 3002355954f726043
parent 30022 1d8b8fa19074
child 30024 5e9d471afef3
permissive check for pattern discipline in case schemes
src/Pure/Isar/code.ML
src/Tools/code/code_thingol.ML
     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  
     2.1 --- a/src/Tools/code/code_thingol.ML	Fri Feb 20 18:29:10 2009 +0100
     2.2 +++ b/src/Tools/code/code_thingol.ML	Fri Feb 20 18:29:10 2009 +0100
     2.3 @@ -453,7 +453,7 @@
     2.4    let
     2.5      val err_class = Sorts.class_error (Syntax.pp_global thy) e;
     2.6      val err_thm = case thm
     2.7 -     of SOME thm => "\n(in defining equation " ^ Display.string_of_thm thm ^ ")" | NONE => "";
     2.8 +     of SOME thm => "\n(in code equation " ^ Display.string_of_thm thm ^ ")" | NONE => "";
     2.9      val err_typ = "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort "
    2.10        ^ Syntax.string_of_sort_global thy sort;
    2.11    in error ("Wellsortedness error" ^ err_thm ^ ":\n" ^ err_typ ^ "\n" ^ err_class) end;
    2.12 @@ -582,9 +582,8 @@
    2.13      fun stmt_classparam class =
    2.14        ensure_class thy algbr funcgr class
    2.15        #>> (fn class => Classparam (c, class));
    2.16 -    fun stmt_fun ((vs, raw_ty), raw_thms) =
    2.17 +    fun stmt_fun ((vs, ty), raw_thms) =
    2.18        let
    2.19 -        val ty = Logic.unvarifyT raw_ty; (*FIXME change convention here*)
    2.20          val thms = if null (Term.add_tfreesT ty []) orelse (null o fst o strip_type) ty
    2.21            then raw_thms
    2.22            else (map o apfst) (Code_Unit.expand_eta thy 1) raw_thms;
    2.23 @@ -643,11 +642,6 @@
    2.24      val ts_clause = nth_drop t_pos ts;
    2.25      fun mk_clause (co, num_co_args) t =
    2.26        let
    2.27 -        val _ = if (is_some o Code.get_datatype_of_constr thy) co then ()
    2.28 -          else error ("Non-constructor " ^ quote co
    2.29 -            ^ " encountered in case pattern"
    2.30 -            ^ (case thm of NONE => ""
    2.31 -              | SOME thm => ", in equation\n" ^ Display.string_of_thm thm))
    2.32          val (vs, body) = Term.strip_abs_eta num_co_args t;
    2.33          val not_undefined = case body
    2.34           of (Const (c, _)) => not (Code.is_undefined thy c)
    2.35 @@ -702,9 +696,7 @@
    2.36      translate_case thy algbr funcgr thm case_scheme ((c, ty), ts)
    2.37  and translate_app thy algbr funcgr thm (c_ty_ts as ((c, _), _)) =
    2.38    case Code.get_case_scheme thy c
    2.39 -   of SOME (base_case_scheme as (_, case_pats)) =>
    2.40 -        translate_app_case thy algbr funcgr thm
    2.41 -          (1 + Int.max (1, length case_pats), base_case_scheme) c_ty_ts
    2.42 +   of SOME case_scheme => translate_app_case thy algbr funcgr thm case_scheme c_ty_ts
    2.43      | NONE => translate_app_const thy algbr funcgr thm c_ty_ts;
    2.44  
    2.45