variables in type schemes must be renamed simultaneously with variables in equations
authorhaftmann
Mon Oct 05 08:36:33 2009 +0200 (2009-10-05 ago)
changeset 32872019201eb7e07
parent 32869 159309603edc
child 32873 333945c9ac6a
variables in type schemes must be renamed simultaneously with variables in equations
src/Pure/Isar/code.ML
src/Tools/Code/code_preproc.ML
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Pure/Isar/code.ML	Sun Oct 04 12:59:22 2009 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Mon Oct 05 08:36:33 2009 +0200
     1.3 @@ -28,6 +28,8 @@
     1.4      -> (thm * bool) list -> (thm * bool) list
     1.5    val const_typ_eqn: theory -> thm -> string * typ
     1.6    val typscheme_eqn: theory -> thm -> (string * sort) list * typ
     1.7 +  val typscheme_rhss_eqns: theory -> string -> thm list
     1.8 +    -> ((string * sort) list * typ) * (string * typ list) list
     1.9  
    1.10    (*executable code*)
    1.11    val add_datatype: (string * typ) list -> theory -> theory
    1.12 @@ -117,6 +119,15 @@
    1.13      val ty' = Logic.unvarifyT ty;
    1.14    in (map dest_TFree (Sign.const_typargs thy (c, ty')), Type.strip_sorts ty') end;
    1.15  
    1.16 +fun default_typscheme thy c =
    1.17 +  let
    1.18 +    val ty = (snd o dest_Const o Term_Subst.zero_var_indexes o curry Const c
    1.19 +      o Type.strip_sorts o Sign.the_const_type thy) c;
    1.20 +  in case AxClass.class_of_param thy c
    1.21 +   of SOME class => ([(Name.aT, [class])], ty)
    1.22 +    | NONE => typscheme thy (c, ty)
    1.23 +  end;
    1.24 +
    1.25  
    1.26  (** data store **)
    1.27  
    1.28 @@ -515,6 +526,15 @@
    1.29  fun typscheme_eqn thy = typscheme thy o const_typ_eqn thy;
    1.30  fun const_eqn thy = fst o const_typ_eqn thy;
    1.31  
    1.32 +fun consts_of thy thms = [] |> (fold o fold o fold_aterms)
    1.33 +  (fn Const (c, ty) => insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty)) | _ => I)
    1.34 +    (map (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of) thms);
    1.35 +
    1.36 +fun typscheme_rhss_eqns thy c [] =
    1.37 +      (default_typscheme thy c, [])
    1.38 +  | typscheme_rhss_eqns thy c (thms as thm :: _) =
    1.39 +      (typscheme_eqn thy thm, consts_of thy thms);
    1.40 +
    1.41  fun assert_eqns_const thy c eqns =
    1.42    let
    1.43      fun cert (eqn as (thm, _)) = if c = const_eqn thy thm
    1.44 @@ -529,7 +549,7 @@
    1.45      fun inter_sorts vs =
    1.46        fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd) vs [];
    1.47      val sorts = map_transpose inter_sorts vss;
    1.48 -    val vts = Name.names Name.context Name.aT sorts
    1.49 +    val vts = Name.names Name.context "'X" sorts
    1.50        |> map (fn (v, sort) => TVar ((v, 0), sort));
    1.51    in map2 (fn vs => Thm.certify_instantiate (vs ~~ vts, [])) vss thms end;
    1.52  
     2.1 --- a/src/Tools/Code/code_preproc.ML	Sun Oct 04 12:59:22 2009 +0200
     2.2 +++ b/src/Tools/Code/code_preproc.ML	Mon Oct 05 08:36:33 2009 +0200
     2.3 @@ -227,27 +227,6 @@
     2.4    map (fn (c, _) => AxClass.param_of_inst thy (c, tyco))
     2.5      o maps (#params o AxClass.get_info thy);
     2.6  
     2.7 -fun consts_of thy eqns = [] |> (fold o fold o fold_aterms)
     2.8 -  (fn Const (c, ty) => insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty)) | _ => I)
     2.9 -    (map (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of o fst) eqns);
    2.10 -
    2.11 -fun default_typscheme_of thy c =
    2.12 -  let
    2.13 -    val ty = (snd o dest_Const o Term_Subst.zero_var_indexes o curry Const c
    2.14 -      o Type.strip_sorts o Sign.the_const_type thy) c;
    2.15 -  in case AxClass.class_of_param thy c
    2.16 -   of SOME class => ([(Name.aT, [class])], ty)
    2.17 -    | NONE => Code.typscheme thy (c, ty)
    2.18 -  end;
    2.19 -
    2.20 -fun tyscm_rhss_of thy c eqns =
    2.21 -  let
    2.22 -    val tyscm = case eqns
    2.23 -     of [] => default_typscheme_of thy c
    2.24 -      | ((thm, _) :: _) => Code.typscheme_eqn thy thm;
    2.25 -    val rhss = consts_of thy eqns;
    2.26 -  in (tyscm, rhss) end;
    2.27 -
    2.28  
    2.29  (* data structures *)
    2.30  
    2.31 @@ -287,7 +266,7 @@
    2.32      | NONE => let
    2.33          val eqns = Code.these_eqns thy c
    2.34            |> preprocess thy c;
    2.35 -        val ((lhs, _), rhss) = tyscm_rhss_of thy c eqns;
    2.36 +        val ((lhs, _), rhss) = Code.typscheme_rhss_eqns thy c (map fst eqns);
    2.37        in ((lhs, rhss), eqns) end;
    2.38  
    2.39  fun obtain_instance thy arities (inst as (class, tyco)) =
    2.40 @@ -434,7 +413,7 @@
    2.41        Vartab.update ((v, 0), sort)) lhs;
    2.42      val eqns = proto_eqns
    2.43        |> (map o apfst) (inst_thm thy inst_tab);
    2.44 -    val (tyscm, rhss') = tyscm_rhss_of thy c eqns;
    2.45 +    val (tyscm, rhss') = Code.typscheme_rhss_eqns thy c (map fst eqns);
    2.46      val eqngr' = Graph.new_node (c, (tyscm, eqns)) eqngr;
    2.47    in (map (pair c) rhss' @ rhss, eqngr') end;
    2.48  
     3.1 --- a/src/Tools/Code/code_thingol.ML	Sun Oct 04 12:59:22 2009 +0200
     3.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Oct 05 08:36:33 2009 +0200
     3.3 @@ -554,16 +554,21 @@
     3.4      fun stmt_classparam class =
     3.5        ensure_class thy algbr funcgr class
     3.6        #>> (fn class => Classparam (c, class));
     3.7 -    fun stmt_fun ((vs, ty), eqns) =
     3.8 -      fold_map (translate_tyvar_sort thy algbr funcgr) vs
     3.9 -      ##>> translate_typ thy algbr funcgr ty
    3.10 -      ##>> fold_map (translate_eqn thy algbr funcgr) (burrow_fst (clean_thms thy) eqns)
    3.11 -      #>> (fn info => Fun (c, info));
    3.12 +    fun stmt_fun raw_eqns =
    3.13 +      let
    3.14 +        val eqns = burrow_fst (clean_thms thy) raw_eqns;
    3.15 +        val ((vs, ty), _) = Code.typscheme_rhss_eqns thy c (map fst eqns);
    3.16 +      in
    3.17 +        fold_map (translate_tyvar_sort thy algbr funcgr) vs
    3.18 +        ##>> translate_typ thy algbr funcgr ty
    3.19 +        ##>> fold_map (translate_eqn thy algbr funcgr) eqns
    3.20 +        #>> (fn info => Fun (c, info))
    3.21 +      end;
    3.22      val stmt_const = case Code.get_datatype_of_constr thy c
    3.23       of SOME tyco => stmt_datatypecons tyco
    3.24        | NONE => (case AxClass.class_of_param thy c
    3.25           of SOME class => stmt_classparam class
    3.26 -          | NONE => stmt_fun (Code_Preproc.typ funcgr c, Code_Preproc.eqns funcgr c))
    3.27 +          | NONE => stmt_fun (Code_Preproc.eqns funcgr c))
    3.28    in ensure_stmt lookup_const (declare_const thy) stmt_const c end
    3.29  and ensure_class thy (algbr as (_, algebra)) funcgr class =
    3.30    let