tuned;
authorwenzelm
Tue Feb 16 13:35:42 2010 +0100 (2010-02-16)
changeset 351448b8302da3a55
parent 35143 7b2538c987e7
child 35145 f132a4fd8679
tuned;
src/HOL/Record.thy
src/HOL/Tools/record.ML
     1.1 --- a/src/HOL/Record.thy	Tue Feb 16 13:26:21 2010 +0100
     1.2 +++ b/src/HOL/Record.thy	Tue Feb 16 13:35:42 2010 +0100
     1.3 @@ -425,17 +425,17 @@
     1.4    "_constify"           :: "id => ident"                        ("_")
     1.5    "_constify"           :: "longid => ident"                    ("_")
     1.6  
     1.7 -  "_field_type"         :: "[ident, type] => field_type"        ("(2_ ::/ _)")
     1.8 +  "_field_type"         :: "ident => type => field_type"        ("(2_ ::/ _)")
     1.9    ""                    :: "field_type => field_types"          ("_")
    1.10 -  "_field_types"        :: "[field_type, field_types] => field_types"    ("_,/ _")
    1.11 +  "_field_types"        :: "field_type => field_types => field_types"    ("_,/ _")
    1.12    "_record_type"        :: "field_types => type"                ("(3'(| _ |'))")
    1.13 -  "_record_type_scheme" :: "[field_types, type] => type"        ("(3'(| _,/ (2... ::/ _) |'))")
    1.14 +  "_record_type_scheme" :: "field_types => type => type"        ("(3'(| _,/ (2... ::/ _) |'))")
    1.15  
    1.16 -  "_field"              :: "[ident, 'a] => field"               ("(2_ =/ _)")
    1.17 +  "_field"              :: "ident => 'a => field"               ("(2_ =/ _)")
    1.18    ""                    :: "field => fields"                    ("_")
    1.19 -  "_fields"             :: "[field, fields] => fields"          ("_,/ _")
    1.20 +  "_fields"             :: "field => fields => fields"          ("_,/ _")
    1.21    "_record"             :: "fields => 'a"                       ("(3'(| _ |'))")
    1.22 -  "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
    1.23 +  "_record_scheme"      :: "fields => 'a => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
    1.24  
    1.25    "_update_name"        :: idt
    1.26    "_update"             :: "ident => 'a => update"              ("(2_ :=/ _)")
     2.1 --- a/src/HOL/Tools/record.ML	Tue Feb 16 13:26:21 2010 +0100
     2.2 +++ b/src/HOL/Tools/record.ML	Tue Feb 16 13:35:42 2010 +0100
     2.3 @@ -270,11 +270,9 @@
     2.4  val Trueprop = HOLogic.mk_Trueprop;
     2.5  fun All xs t = Term.list_all_free (xs, t);
     2.6  
     2.7 -infix 9 $$;
     2.8  infix 0 :== ===;
     2.9  infixr 0 ==>;
    2.10  
    2.11 -val op $$ = Term.list_comb;
    2.12  val op :== = Primitive_Defs.mk_defpair;
    2.13  val op === = Trueprop o HOLogic.mk_eq;
    2.14  val op ==> = Logic.mk_implies;
    2.15 @@ -586,9 +584,9 @@
    2.16    let
    2.17      val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
    2.18        Records_Data.get thy;
    2.19 -    val data = make_record_data records sel_upd
    2.20 -      equalities extinjects (Symtab.update_new (name, thm) extsplit) splits
    2.21 -      extfields fieldext;
    2.22 +    val data =
    2.23 +      make_record_data records sel_upd equalities extinjects
    2.24 +        (Symtab.update_new (name, thm) extsplit) splits extfields fieldext;
    2.25    in Records_Data.put data thy end;
    2.26  
    2.27  
    2.28 @@ -598,9 +596,9 @@
    2.29    let
    2.30      val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
    2.31        Records_Data.get thy;
    2.32 -    val data = make_record_data records sel_upd
    2.33 -      equalities extinjects extsplit (Symtab.update_new (name, thmP) splits)
    2.34 -      extfields fieldext;
    2.35 +    val data =
    2.36 +      make_record_data records sel_upd equalities extinjects extsplit
    2.37 +        (Symtab.update_new (name, thmP) splits) extfields fieldext;
    2.38    in Records_Data.put data thy end;
    2.39  
    2.40  val get_splits = Symtab.lookup o #splits o Records_Data.get;
    2.41 @@ -619,8 +617,7 @@
    2.42      val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
    2.43        Records_Data.get thy;
    2.44      val data =
    2.45 -      make_record_data records sel_upd
    2.46 -        equalities extinjects extsplit splits
    2.47 +      make_record_data records sel_upd equalities extinjects extsplit splits
    2.48          (Symtab.update_new (name, fields) extfields) fieldext;
    2.49    in Records_Data.put data thy end;
    2.50  
    2.51 @@ -701,7 +698,8 @@
    2.52  
    2.53  fun decode_type thy t =
    2.54    let
    2.55 -    fun get_sort xs n = AList.lookup (op =) xs (n: indexname) |> the_default (Sign.defaultS thy);
    2.56 +    fun get_sort env xi =
    2.57 +      the_default (Sign.defaultS thy) (AList.lookup (op =) env (xi: indexname));
    2.58      val map_sort = Sign.intern_sort thy;
    2.59    in
    2.60      Syntax.typ_of_term (get_sort (Syntax.term_sorts map_sort t)) map_sort t
    2.61 @@ -711,6 +709,8 @@
    2.62  
    2.63  (* parse translations *)
    2.64  
    2.65 +local
    2.66 +
    2.67  fun gen_field_tr mark sfx (t as Const (c, _) $ Const (name, _) $ arg) =
    2.68        if c = mark then Syntax.const (suffix sfx name) $ Abs ("_", dummyT, arg)
    2.69        else raise TERM ("gen_field_tr: " ^ mark, [t])
    2.70 @@ -721,17 +721,20 @@
    2.71        else [gen_field_tr mark sfx tm]
    2.72    | gen_fields_tr _ mark sfx tm = [gen_field_tr mark sfx tm];
    2.73  
    2.74 +in
    2.75  
    2.76  fun record_update_tr [t, u] =
    2.77        fold (curry op $)
    2.78          (gen_fields_tr @{syntax_const "_updates"} @{syntax_const "_update"} updateN u) t
    2.79    | record_update_tr ts = raise TERM ("record_update_tr", ts);
    2.80  
    2.81 -fun update_name_tr (Free (x, T) :: ts) = Free (suffix updateN x, T) $$ ts
    2.82 -  | update_name_tr (Const (x, T) :: ts) = Const (suffix updateN x, T) $$ ts
    2.83 +end;
    2.84 +
    2.85 +fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix updateN x, T), ts)
    2.86 +  | update_name_tr (Const (x, T) :: ts) = list_comb (Const (suffix updateN x, T), ts)
    2.87    | update_name_tr (((c as Const (@{syntax_const "_constrain"}, _)) $ t $ ty) :: ts) =
    2.88        (* FIXME @{type_syntax} *)
    2.89 -      (c $ update_name_tr [t] $ (Syntax.const "fun" $ ty $ Syntax.const "dummy")) $$ ts
    2.90 +      list_comb (c $ update_name_tr [t] $ (Syntax.const "fun" $ ty $ Syntax.const "dummy"), ts)
    2.91    | update_name_tr ts = raise TERM ("update_name_tr", ts);
    2.92  
    2.93  fun dest_ext_field mark (t as (Const (c, _) $ Const (name, _) $ arg)) =
    2.94 @@ -2091,15 +2094,18 @@
    2.95      val upd_specs = map mk_upd_spec (fields_more ~~ lastN updator_thms);
    2.96  
    2.97      (*derived operations*)
    2.98 -    val make_spec = Const (full (Binding.name makeN), all_types ---> recT0) $$ all_vars :==
    2.99 -      mk_rec (all_vars @ [HOLogic.unit]) 0;
   2.100 -    val fields_spec = Const (full (Binding.name fields_selN), types ---> Type extension) $$ vars :==
   2.101 -      mk_rec (all_vars @ [HOLogic.unit]) parent_len;
   2.102 +    val make_spec =
   2.103 +      list_comb (Const (full (Binding.name makeN), all_types ---> recT0), all_vars) :==
   2.104 +        mk_rec (all_vars @ [HOLogic.unit]) 0;
   2.105 +    val fields_spec =
   2.106 +      list_comb (Const (full (Binding.name fields_selN), types ---> Type extension), vars) :==
   2.107 +        mk_rec (all_vars @ [HOLogic.unit]) parent_len;
   2.108      val extend_spec =
   2.109        Const (full (Binding.name extendN), recT0 --> moreT --> rec_schemeT0) $ r_unit0 $ more :==
   2.110 -      mk_rec ((map (mk_sel r_unit0) all_fields) @ [more]) 0;
   2.111 -    val truncate_spec = Const (full (Binding.name truncateN), rec_schemeT0 --> recT0) $ r0 :==
   2.112 -      mk_rec ((map (mk_sel r0) all_fields) @ [HOLogic.unit]) 0;
   2.113 +        mk_rec ((map (mk_sel r_unit0) all_fields) @ [more]) 0;
   2.114 +    val truncate_spec =
   2.115 +      Const (full (Binding.name truncateN), rec_schemeT0 --> recT0) $ r0 :==
   2.116 +        mk_rec ((map (mk_sel r0) all_fields) @ [HOLogic.unit]) 0;
   2.117  
   2.118  
   2.119      (* 2st stage: defs_thy *)