added first version of user-space type system for class target
authorhaftmann
Mon Oct 08 08:04:28 2007 +0200 (2007-10-08)
changeset 24901d3cbf79769b9
parent 24900 5471709833a4
child 24902 49f002c3964e
added first version of user-space type system for class target
src/HOL/HOL.thy
src/HOL/Real/RealVector.thy
src/Pure/Isar/class.ML
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/HOL/HOL.thy	Mon Oct 08 08:04:26 2007 +0200
     1.2 +++ b/src/HOL/HOL.thy	Mon Oct 08 08:04:28 2007 +0200
     1.3 @@ -22,13 +22,13 @@
     1.4    "~~/src/Provers/eqsubst.ML"
     1.5    "~~/src/Provers/quantifier1.ML"
     1.6    ("simpdata.ML")
     1.7 +  "~~/src/Tools/induct.ML"
     1.8    "~~/src/Tools/code/code_name.ML"
     1.9    "~~/src/Tools/code/code_funcgr.ML"
    1.10    "~~/src/Tools/code/code_thingol.ML"
    1.11    "~~/src/Tools/code/code_target.ML"
    1.12    "~~/src/Tools/code/code_package.ML"
    1.13    "~~/src/Tools/nbe.ML"
    1.14 -  "~~/src/Tools/induct.ML"
    1.15  begin
    1.16  
    1.17  subsection {* Primitive logic *}
    1.18 @@ -205,13 +205,13 @@
    1.19  subsubsection {* Generic classes and algebraic operations *}
    1.20  
    1.21  class default = type +
    1.22 -  fixes default :: "'a"
    1.23 +  fixes default :: 'a
    1.24  
    1.25  class zero = type + 
    1.26 -  fixes zero :: "'a"  ("\<^loc>0")
    1.27 +  fixes zero :: 'a  ("\<^loc>0")
    1.28  
    1.29  class one = type +
    1.30 -  fixes one  :: "'a"  ("\<^loc>1")
    1.31 +  fixes one  :: 'a  ("\<^loc>1")
    1.32  
    1.33  hide (open) const zero one
    1.34  
    1.35 @@ -295,11 +295,6 @@
    1.36    less_eq  ("(_/ \<le> _)"  [51, 51] 50)
    1.37  
    1.38  notation (input)
    1.39 -  greater  (infix ">" 50)
    1.40 -
    1.41 -notation (input)
    1.42 -  greater_eq  (infix ">=" 50)
    1.43 -and
    1.44    greater_eq  (infix "\<ge>" 50)
    1.45  
    1.46  syntax
     2.1 --- a/src/HOL/Real/RealVector.thy	Mon Oct 08 08:04:26 2007 +0200
     2.2 +++ b/src/HOL/Real/RealVector.thy	Mon Oct 08 08:04:28 2007 +0200
     2.3 @@ -54,11 +54,6 @@
     2.4  
     2.5  end
     2.6  
     2.7 -abbreviation
     2.8 -  divideR :: "'a \<Rightarrow> real \<Rightarrow> 'a\<Colon>scaleR" (infixl "'/#" 70)
     2.9 -where
    2.10 -  "x /# r == scaleR (inverse r) x"
    2.11 -
    2.12  notation (xsymbols)
    2.13    scaleR (infixr "*\<^sub>R" 75) and
    2.14    divideR (infixl "'/\<^sub>R" 70)
     3.1 --- a/src/Pure/Isar/class.ML	Mon Oct 08 08:04:26 2007 +0200
     3.2 +++ b/src/Pure/Isar/class.ML	Mon Oct 08 08:04:28 2007 +0200
     3.3 @@ -45,13 +45,10 @@
     3.4    val param_const: theory -> string -> (string * string) option
     3.5    val params_of_sort: theory -> sort -> (string * (string * typ)) list
     3.6  
     3.7 -  (*experimental*)
     3.8 -  val init_ref: (sort -> Proof.context -> Proof.context) ref
     3.9 -  val init: sort -> Proof.context -> Proof.context;
    3.10 -  val init_exp: sort -> Proof.context -> Proof.context;
    3.11 +  val init: class -> Proof.context -> Proof.context;
    3.12    val local_syntax: theory -> class -> bool
    3.13 -  val add_abbrev_in_class: string -> (string * term) * Syntax.mixfix
    3.14 -    -> theory -> term * theory
    3.15 +  val add_abbrev_in_class: string -> Syntax.mode -> (string * term) * mixfix
    3.16 +    -> theory -> theory
    3.17  end;
    3.18  
    3.19  structure Class : CLASS =
    3.20 @@ -62,8 +59,8 @@
    3.21  fun fork_mixfix is_loc some_class mx =
    3.22    let
    3.23      val mx' = Syntax.unlocalize_mixfix mx;
    3.24 -    val mx_global = if is_some some_class orelse (is_loc andalso mx = mx')
    3.25 -      then NoSyn else mx';
    3.26 +    val mx_global = if not is_loc orelse (is_some some_class andalso not (mx = mx'))
    3.27 +      then mx' else NoSyn;
    3.28      val mx_local = if is_loc then mx else NoSyn;
    3.29    in (mx_global, mx_local) end;
    3.30  
    3.31 @@ -398,6 +395,15 @@
    3.32  
    3.33  fun local_operation thy = Option.join oo AList.lookup (op =) o these_operations thy;
    3.34  
    3.35 +fun sups_local_sort thy sort =
    3.36 +  let
    3.37 +    val sups = filter (is_some o lookup_class_data thy) sort
    3.38 +      |> Sign.minimize_sort thy;
    3.39 +    val local_sort = case sups
    3.40 +     of sup :: _ => #local_sort (the_class_data thy sup)
    3.41 +      | [] => sort;
    3.42 +  in (sups, local_sort) end;
    3.43 +
    3.44  fun local_syntax thy = #local_syntax o the_class_data thy;
    3.45  
    3.46  fun print_classes thy =
    3.47 @@ -445,7 +451,7 @@
    3.48      |> Symtab.update (locale, class)
    3.49    ));
    3.50  
    3.51 -fun register_const (class, (entry, def)) =
    3.52 +fun register_const class (entry, def) =
    3.53    (ClassData.map o apfst o Graph.map_node class o map_class_data o apsnd)
    3.54      (fn (defs, operations) => (def :: defs, apsnd SOME entry :: operations));
    3.55  
    3.56 @@ -545,18 +551,20 @@
    3.57  
    3.58  (** classes and class target **)
    3.59  
    3.60 -(* class context initialization - experimental *)
    3.61 +(* class context initialization *)
    3.62  
    3.63 -fun get_remove_constraints sort ctxt =
    3.64 +fun get_remove_constraints sups local_sort ctxt =
    3.65    let
    3.66 -    val operations = these_operations (ProofContext.theory_of ctxt) sort;
    3.67 +    val thy = ProofContext.theory_of ctxt;
    3.68 +    val operations = these_operations thy sups;
    3.69      fun get_remove (c, _) ctxt =
    3.70        let
    3.71          val ty = ProofContext.the_const_constraint ctxt c;
    3.72 -        val _ = tracing c;
    3.73 +        val ty' = map_atyps (fn ty as TFree (v, _) => if v = Name.aT
    3.74 +          then TFree (v, local_sort) else ty | ty => ty) ty;
    3.75        in
    3.76          ctxt
    3.77 -        |> ProofContext.add_const_constraint (c, NONE)
    3.78 +        |> ProofContext.add_const_constraint (c, SOME ty')
    3.79          |> pair (c, ty)
    3.80        end;
    3.81    in
    3.82 @@ -564,51 +572,43 @@
    3.83      |> fold_map get_remove operations
    3.84    end;
    3.85  
    3.86 -fun sort_term_check thy sort constraints =
    3.87 +fun sort_term_check thy sups local_sort constraints ts ctxt =
    3.88    let
    3.89 -    val local_operation = local_operation thy sort;
    3.90 -    fun default_typ consts c = case AList.lookup (op =) constraints c
    3.91 -     of SOME ty => SOME ty
    3.92 -      | NONE => try (Consts.the_constraint consts) c;
    3.93 -    fun infer_constraints ctxt ts =
    3.94 -        TypeInfer.infer_types (ProofContext.pp ctxt)
    3.95 -          (Sign.tsig_of (ProofContext.theory_of ctxt))
    3.96 -          I (default_typ (ProofContext.consts_of ctxt)) (K NONE)
    3.97 -          (Variable.names_of ctxt) (Variable.maxidx_of ctxt) NONE (map (rpair dummyT) ts)
    3.98 -        |> fst |> map fst
    3.99 -      handle TYPE (msg, _, _) => error msg;
   3.100 -    fun check_typ c idx ty = case (nth (Sign.const_typargs thy (c, ty)) idx) (*FIXME localize*)
   3.101 -     of TFree (v, _) => v = Name.aT
   3.102 -      | TVar (vi, _) => TypeInfer.is_param vi (*FIXME substitute in all typs*)
   3.103 -      | _ => false;
   3.104 -    fun subst_operation (t as Const (c, ty)) = (case local_operation c
   3.105 -         of SOME (t', idx) => if check_typ c idx ty then t' else t
   3.106 -          | NONE => t)
   3.107 -      | subst_operation t = t;
   3.108 -    fun subst_operations ts ctxt =
   3.109 -      ts
   3.110 -      |> (map o map_aterms) subst_operation
   3.111 -      |> infer_constraints ctxt
   3.112 -      |> rpair ctxt; (*FIXME add constraints here*)
   3.113 -  in subst_operations end;
   3.114 +    val local_operation = local_operation thy sups;
   3.115 +    val consts = ProofContext.consts_of ctxt;
   3.116 +    fun check_typ (c, ty) (t', idx) = case nth (Consts.typargs consts (c, ty)) idx
   3.117 +     of TFree (v, _) => if v = Name.aT
   3.118 +          then apfst (AList.update (op =) ((c, ty), t')) else I
   3.119 +      | TVar (vi, _) => if TypeInfer.is_param vi
   3.120 +          then apfst (AList.update (op =) ((c, ty), t'))
   3.121 +            #> apsnd (insert (op =) vi) else I
   3.122 +      | _ => I;
   3.123 +    fun add_const (Const (c, ty)) = (case local_operation c
   3.124 +         of SOME (t', idx) => check_typ (c, ty) (t', idx)
   3.125 +          | NONE => I)
   3.126 +      | add_const _ = I;
   3.127 +    val (cs, typarams) = (fold o fold_aterms) add_const ts ([], []);
   3.128 +    val ts' = map (map_aterms
   3.129 +        (fn t as Const (c, ty) => the_default t (AList.lookup (op =) cs (c, ty)) | t => t)
   3.130 +      #> (map_types o map_type_tvar) (fn var as (vi, _) => if member (op =) typarams vi
   3.131 +           then TFree (Name.aT, local_sort) else TVar var)) ts;
   3.132 +    val ctxt' = fold (ProofContext.add_const_constraint o apsnd SOME) constraints ctxt;
   3.133 +  in (ts', ctxt') end;
   3.134  
   3.135 -fun init_exp sort ctxt =
   3.136 +fun init_class_ctxt thy sups local_sort ctxt =
   3.137 +  ctxt
   3.138 +  |> Variable.declare_term
   3.139 +      (Logic.mk_type (TFree (Name.aT, local_sort)))
   3.140 +  |> get_remove_constraints sups local_sort
   3.141 +  |-> (fn constraints => Context.proof_map (Syntax.add_term_check 50 "class"
   3.142 +        (sort_term_check thy sups local_sort constraints)));
   3.143 +
   3.144 +fun init class ctxt =
   3.145    let
   3.146      val thy = ProofContext.theory_of ctxt;
   3.147 -    val local_sort = (#local_sort o the_class_data thy) (hd sort);
   3.148 -    val term_check = sort_term_check thy sort;
   3.149 -  in
   3.150 -    ctxt
   3.151 -    |> Variable.declare_term
   3.152 -        (Logic.mk_type (TFree (Name.aT, local_sort)))
   3.153 -    |> get_remove_constraints sort
   3.154 -    |-> (fn constraints => Context.proof_map (Syntax.add_term_check 50 "class"
   3.155 -          (sort_term_check thy sort constraints)))
   3.156 -  end;
   3.157 -
   3.158 -val init_ref = ref (K I : sort -> Proof.context -> Proof.context);
   3.159 -fun init class = ! init_ref class;
   3.160 -
   3.161 +    val local_sort = (#local_sort o the_class_data thy) class;
   3.162 +  in init_class_ctxt thy [class] local_sort ctxt end;
   3.163 +  
   3.164  
   3.165  (* class definition *)
   3.166  
   3.167 @@ -625,12 +625,8 @@
   3.168  fun gen_class_spec prep_class prep_expr process_expr thy raw_supclasses raw_includes_elems =
   3.169    let
   3.170      val supclasses = map (prep_class thy) raw_supclasses;
   3.171 -    val sups = filter (is_some o lookup_class_data thy) supclasses
   3.172 -      |> Sign.minimize_sort thy;
   3.173 +    val (sups, local_sort) = sups_local_sort thy supclasses;
   3.174      val supsort = Sign.minimize_sort thy supclasses;
   3.175 -    val local_sort = case sups
   3.176 -     of sup :: _ => (#local_sort o the_class_data thy) sup
   3.177 -      | [] => supsort;
   3.178      val suplocales = map (Locale.Locale o #locale o the_class_data thy) sups;
   3.179      val (raw_elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e)
   3.180        | Locale.Expr i => apsnd (cons (prep_expr thy i))) raw_includes_elems ([], []);
   3.181 @@ -645,7 +641,7 @@
   3.182      ProofContext.init thy
   3.183      |> Locale.cert_expr supexpr [constrain]
   3.184      |> snd
   3.185 -    |> init supsort
   3.186 +    |> init_class_ctxt thy sups local_sort
   3.187      |> process_expr Locale.empty raw_elems
   3.188      |> fst
   3.189      |> (fn elems => ((((sups, supconsts), (supsort, local_sort, mergeexpr)),
   3.190 @@ -670,20 +666,16 @@
   3.191      fun extract_params thy name_locale =
   3.192        let
   3.193          val params = Locale.parameters_of thy name_locale;
   3.194 -        val local_sort = case AList.group (op =) ((maps typ_tfrees o map (snd o fst)) params)
   3.195 -         of [(_, local_sort :: _)] => local_sort
   3.196 -          | _ => Sign.defaultS thy
   3.197 -          | vs => error ("exactly one type variable required: " ^ commas (map fst vs));
   3.198          val _ = if Sign.subsort thy (supsort, local_sort) then () else error
   3.199            ("Sort " ^ Sign.string_of_sort thy local_sort
   3.200              ^ " is less general than permitted least general sort "
   3.201              ^ Sign.string_of_sort thy supsort);
   3.202        in
   3.203 -        (local_sort, (map fst params, params
   3.204 +        (map fst params, params
   3.205          |> (map o apfst o apsnd o Term.map_type_tfree) (K (TFree (Name.aT, local_sort)))
   3.206 -        |> (map o apsnd) (fork_mixfix true NONE #> fst)
   3.207 +        |> (map o apsnd) (fork_mixfix true (SOME "") #> fst)
   3.208          |> chop (length supconsts)
   3.209 -        |> snd))
   3.210 +        |> snd)
   3.211        end;
   3.212      fun extract_assumes name_locale params thy cs =
   3.213        let
   3.214 @@ -707,7 +699,7 @@
   3.215      |> Locale.add_locale_i (SOME "") bname mergeexpr elems
   3.216      |-> (fn name_locale => ProofContext.theory_result (
   3.217        `(fn thy => extract_params thy name_locale)
   3.218 -      #-> (fn (_, (globals, params)) =>
   3.219 +      #-> (fn (globals, params) =>
   3.220          AxClass.define_class_params (bname, supsort) params
   3.221            (extract_assumes name_locale params) other_consts
   3.222        #-> (fn (name_axclass, (consts, axioms)) =>
   3.223 @@ -742,6 +734,12 @@
   3.224        | subst_aterm t = t;
   3.225    in Term.map_aterms subst_aterm end;
   3.226  
   3.227 +fun mk_operation_entry thy (c, rhs) =
   3.228 +  let
   3.229 +    val typargs = Sign.const_typargs thy (c, fastype_of rhs);
   3.230 +    val typidx = find_index (fn TFree (w, _) => Name.aT = w | _ => false) typargs;
   3.231 +  in (c, (rhs, typidx)) end;
   3.232 +
   3.233  fun add_const_in_class class ((c, rhs), syn) thy =
   3.234    let
   3.235      val prfx = (Logic.const_of_class o NameSpace.base) class;
   3.236 @@ -759,17 +757,16 @@
   3.237      val ty'' = subst_typ ty';
   3.238      val c' = mk_name c;
   3.239      val def = (c, Logic.mk_equals (Const (c', ty'), rhs'));
   3.240 -    val (syn', _) = fork_mixfix true NONE syn;
   3.241 +    val (syn', _) = fork_mixfix true (SOME class) syn;
   3.242      fun interpret def thy =
   3.243        let
   3.244          val def' = symmetric def;
   3.245          val def_eq = Thm.prop_of def';
   3.246 -        val typargs = Sign.const_typargs thy (c', fastype_of rhs);
   3.247 -        val typidx = find_index (fn TFree (w, _) => Name.aT = w | _ => false) typargs;
   3.248 +        val entry = mk_operation_entry thy (c', rhs);
   3.249        in
   3.250          thy
   3.251          |> class_interpretation class [def'] [def_eq]
   3.252 -        |> register_const (class, ((c', (rhs, typidx)), def'))
   3.253 +        |> register_const class (entry, def')
   3.254        end;
   3.255    in
   3.256      thy
   3.257 @@ -783,21 +780,25 @@
   3.258      |> Sign.restore_naming thy
   3.259    end;
   3.260  
   3.261 -fun add_abbrev_in_class class ((c, rhs), syn) thy =
   3.262 +
   3.263 +(* abbreviation in class target *)
   3.264 +
   3.265 +fun add_abbrev_in_class class prmode ((c, rhs), syn) thy =
   3.266    let
   3.267 -    val local_sort = (#local_sort o the_class_data thy) class;
   3.268 -    val subst_typ = Term.map_type_tfree (fn var as (w, sort) =>
   3.269 -      if w = Name.aT then TFree (w, local_sort) else TFree var);
   3.270 -    val ty = fastype_of rhs;
   3.271 -    val rhs' = map_types subst_typ rhs;
   3.272 +    val prfx = (Logic.const_of_class o NameSpace.base) class;
   3.273 +    fun mk_name c =
   3.274 +      let
   3.275 +        val n1 = Sign.full_name thy c;
   3.276 +        val n2 = NameSpace.qualifier n1;
   3.277 +        val n3 = NameSpace.base n1;
   3.278 +      in NameSpace.implode [n2, prfx, prfx, n3] end;
   3.279 +    val c' = mk_name c;
   3.280 +    val rhs' = export_fixes thy class rhs;
   3.281 +    val ty' = fastype_of rhs';
   3.282    in
   3.283      thy
   3.284 -    |> Sign.parent_path (*FIXME*)
   3.285 -    |> Sign.add_abbrev Syntax.internalM [] (c, rhs)
   3.286 -    |-> (fn (lhs as Const (c', _), _) => register_abbrev class c'
   3.287 -      (*#> Sign.add_const_constraint (c', SOME ty)*)
   3.288 -      #> pair lhs)
   3.289 -    ||> Sign.restore_naming thy
   3.290 +    |> Sign.add_notation prmode [(Const (c', ty'), syn)]
   3.291 +    |> register_abbrev class c'
   3.292    end;
   3.293  
   3.294  
     4.1 --- a/src/Pure/Isar/theory_target.ML	Mon Oct 08 08:04:26 2007 +0200
     4.2 +++ b/src/Pure/Isar/theory_target.ML	Mon Oct 08 08:04:28 2007 +0200
     4.3 @@ -115,7 +115,8 @@
     4.4          val U = map #2 xs ---> T;
     4.5          val t = Term.list_comb (Const (Sign.full_name thy c, U), map Free xs);
     4.6          val (mx1, mx2) = Class.fork_mixfix is_loc some_class mx;
     4.7 -        val thy' = Sign.add_consts_authentic (ContextPosition.properties_of lthy) [(c, U, mx1)] thy;
     4.8 +        val mx3 = if is_loc then NoSyn else mx1;
     4.9 +        val thy' = Sign.add_consts_authentic (ContextPosition.properties_of lthy) [(c, U, mx3)] thy;
    4.10        in (((c, mx2), t), thy') end;
    4.11  
    4.12      fun const_class (SOME class) ((c, _), mx) (_, t) =
    4.13 @@ -182,12 +183,18 @@
    4.14      val U = Term.fastype_of u;
    4.15      val u' = singleton (Variable.export_terms (Variable.declare_term u target) thy_ctxt) u;
    4.16      val (mx1, mx2) = Class.fork_mixfix is_loc some_class mx;
    4.17 +    val mx3 = if is_loc then NoSyn else mx1;
    4.18 +    fun add_abbrev_in_class NONE = K I
    4.19 +      | add_abbrev_in_class (SOME class) =
    4.20 +          Class.add_abbrev_in_class class prmode;
    4.21    in
    4.22      lthy
    4.23      |> LocalTheory.theory_result
    4.24          (Sign.add_abbrev (#1 prmode) (ContextPosition.properties_of lthy) (c, u'))
    4.25 -    |-> (fn (lhs as Const (full_c, _), rhs) => LocalTheory.theory (Sign.add_notation prmode [(lhs, mx1)])
    4.26 +    |-> (fn (lhs as Const (full_c, _), rhs) => LocalTheory.theory (Sign.add_notation prmode [(lhs, mx3)])
    4.27      #> is_loc ? internal_abbrev prmode ((c, mx2), Term.list_comb (Const (full_c, U), xs))
    4.28 +    #> LocalTheory.raw_theory
    4.29 +         (add_abbrev_in_class some_class ((c, Term.list_comb (Const (full_c, U), xs)), mx1))
    4.30      #> local_abbrev (c, rhs))
    4.31    end;
    4.32  
    4.33 @@ -373,14 +380,10 @@
    4.34      val thy = ProofContext.theory_of ctxt;
    4.35      val is_loc = loc <> "";
    4.36      val some_class = Class.class_of_locale thy loc;
    4.37 -    fun class_init (SOME class) =
    4.38 -          Class.init [class]
    4.39 -      | class_init NONE =
    4.40 -          I;
    4.41    in
    4.42      ctxt
    4.43      |> Data.put (if is_loc then SOME loc else NONE)
    4.44 -    |> class_init some_class
    4.45 +    |> the_default I (Option.map Class.init some_class)
    4.46      |> LocalTheory.init (NameSpace.base loc)
    4.47       {pretty = pretty loc,
    4.48        consts = consts is_loc some_class,