clarified terminology
authorhaftmann
Thu Oct 04 19:41:51 2007 +0200 (2007-10-04)
changeset 24837cacc5744be75
parent 24836 dab06e93ec28
child 24838 1d1bddf87353
clarified terminology
src/Pure/Isar/code.ML
src/Tools/code/code_thingol.ML
     1.1 --- a/src/Pure/Isar/code.ML	Thu Oct 04 19:41:50 2007 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Thu Oct 04 19:41:51 2007 +0200
     1.3 @@ -33,7 +33,9 @@
     1.4    val default_typ: theory -> string -> typ
     1.5  
     1.6    val preprocess_conv: cterm -> thm
     1.7 +  val preprocess_term: theory -> term -> term
     1.8    val postprocess_conv: cterm -> thm
     1.9 +  val postprocess_term: theory -> term -> term
    1.10  
    1.11    val add_attribute: string * (Args.T list -> attribute * Args.T list) -> theory -> theory
    1.12  
    1.13 @@ -526,9 +528,9 @@
    1.14  fun specific_constraints thy (class, tyco) =
    1.15    let
    1.16      val vs = Name.invents Name.context "" (Sign.arity_number thy tyco);
    1.17 -    val clsops = (map fst o these o Option.map snd
    1.18 +    val classparams = (map fst o these o Option.map snd
    1.19        o try (AxClass.params_of_class thy)) class;
    1.20 -    val funcs = clsops
    1.21 +    val funcs = classparams
    1.22        |> map (fn c => Class.inst_const thy (c, tyco))
    1.23        |> map (Symtab.lookup ((the_funcs o get_exec) thy))
    1.24        |> (map o Option.map) (Susp.force o fst)
    1.25 @@ -558,7 +560,7 @@
    1.26          (Sign.arity_number thy tyco) (Sign.minimize_sort thy (Sign.all_classes thy))
    1.27    end;
    1.28  
    1.29 -fun gen_classop_typ constr thy class (c, tyco) = 
    1.30 +fun gen_classparam_typ constr thy class (c, tyco) = 
    1.31    let
    1.32      val (var, cs) = try (AxClass.params_of_class thy) class |> the_default ("'a", [])
    1.33      val ty = (the o AList.lookup (op =) cs) c;
    1.34 @@ -582,18 +584,18 @@
    1.35      val operational_classes = fold add_iff_operational (Sign.all_classes thy) []
    1.36    in retrieve_algebra thy (member (op =) operational_classes) end;
    1.37  
    1.38 -val classop_weakest_typ = gen_classop_typ weakest_constraints;
    1.39 -val classop_strongest_typ = gen_classop_typ strongest_constraints;
    1.40 +val classparam_weakest_typ = gen_classparam_typ weakest_constraints;
    1.41 +val classparam_strongest_typ = gen_classparam_typ strongest_constraints;
    1.42  
    1.43  fun assert_func_typ thm =
    1.44    let
    1.45      val thy = Thm.theory_of_thm thm;
    1.46 -    fun check_typ_classop tyco (c, thm) =
    1.47 +    fun check_typ_classparam tyco (c, thm) =
    1.48            let
    1.49              val SOME class = AxClass.class_of_param thy c;
    1.50              val (_, ty) = CodeUnit.head_func thm;
    1.51 -            val ty_decl = classop_weakest_typ thy class (c, tyco);
    1.52 -            val ty_strongest = classop_strongest_typ thy class (c, tyco);
    1.53 +            val ty_decl = classparam_weakest_typ thy class (c, tyco);
    1.54 +            val ty_strongest = classparam_strongest_typ thy class (c, tyco);
    1.55              fun constrain thm = 
    1.56                let
    1.57                  val max = Thm.maxidx_of thm + 1;
    1.58 @@ -632,7 +634,7 @@
    1.59        end;
    1.60      fun check_typ (c, thm) =
    1.61        case Class.param_const thy c
    1.62 -       of SOME (c, tyco) => check_typ_classop tyco (c, thm)
    1.63 +       of SOME (c, tyco) => check_typ_classparam tyco (c, thm)
    1.64          | NONE => check_typ_fun (c, thm);
    1.65    in check_typ (const_of_func thy thm, thm) end;
    1.66  
    1.67 @@ -837,6 +839,13 @@
    1.68      val thm' = (conv o Thm.rhs_of) thm;
    1.69    in Thm.transitive thm thm' end
    1.70  
    1.71 +fun term_of_conv thy f =
    1.72 +  Thm.cterm_of thy
    1.73 +  #> f
    1.74 +  #> Thm.prop_of
    1.75 +  #> Logic.dest_equals
    1.76 +  #> snd;
    1.77 +
    1.78  in
    1.79  
    1.80  fun preprocess thy thms =
    1.81 @@ -859,6 +868,8 @@
    1.82      |> rhs_conv (Class.unoverload thy)
    1.83    end;
    1.84  
    1.85 +fun preprocess_term thy = term_of_conv thy preprocess_conv;
    1.86 +
    1.87  fun postprocess_conv ct =
    1.88    let
    1.89      val thy = Thm.theory_of_cterm ct;
    1.90 @@ -868,10 +879,12 @@
    1.91      |> rhs_conv (MetaSimplifier.rewrite false ((#posts o the_thmproc o get_exec) thy))
    1.92    end;
    1.93  
    1.94 +fun postprocess_term thy = term_of_conv thy postprocess_conv;
    1.95 +
    1.96  end; (*local*)
    1.97  
    1.98  fun default_typ_proto thy c = case Class.param_const thy c
    1.99 - of SOME (c, tyco) => classop_weakest_typ thy ((the o AxClass.class_of_param thy) c)
   1.100 + of SOME (c, tyco) => classparam_weakest_typ thy ((the o AxClass.class_of_param thy) c)
   1.101        (c, tyco) |> SOME
   1.102    | NONE => (case AxClass.class_of_param thy c
   1.103       of SOME class => SOME (Term.map_type_tvar
     2.1 --- a/src/Tools/code/code_thingol.ML	Thu Oct 04 19:41:50 2007 +0200
     2.2 +++ b/src/Tools/code/code_thingol.ML	Thu Oct 04 19:41:51 2007 +0200
     2.3 @@ -64,8 +64,8 @@
     2.4      | Datatype of (vname * sort) list * (string * itype list) list
     2.5      | Datatypecons of string
     2.6      | Class of vname * ((class * string) list * (string * itype) list)
     2.7 -    | Classop of class
     2.8      | Classrel of class * class
     2.9 +    | Classparam of class
    2.10      | Classinst of (class * (string * (vname * sort) list))
    2.11            * ((class * (string * (string * dict list list))) list
    2.12          * ((string * const) * thm) list);
    2.13 @@ -135,12 +135,12 @@
    2.14      class names             class
    2.15      type constructor names  tyco
    2.16      datatype names          dtco
    2.17 -    const names (general)   c
    2.18 +    const names (general)   c (const)
    2.19      constructor names       co
    2.20 -    class operation names   clsop (op)
    2.21 +    class parameter names   classparam
    2.22      arbitrary name          s
    2.23  
    2.24 -    v, c, co, clsop also annotated with types etc.
    2.25 +    v, c, co, classparam also annotated with types etc.
    2.26  
    2.27    constructs:
    2.28      sort                    sort
    2.29 @@ -251,8 +251,8 @@
    2.30    | Datatype of (vname * sort) list * (string * itype list) list
    2.31    | Datatypecons of string
    2.32    | Class of vname * ((class * string) list * (string * itype) list)
    2.33 -  | Classop of class
    2.34    | Classrel of class * class
    2.35 +  | Classparam of class
    2.36    | Classinst of (class * (string * (vname * sort) list))
    2.37          * ((class * (string * (string * dict list list))) list
    2.38        * ((string * const) * thm) list);