src/HOL/Tools/record.ML
changeset 35144 8b8302da3a55
parent 35142 495c623f1e3c
child 35145 f132a4fd8679
     1.1 --- a/src/HOL/Tools/record.ML	Tue Feb 16 13:26:21 2010 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Tue Feb 16 13:35:42 2010 +0100
     1.3 @@ -270,11 +270,9 @@
     1.4  val Trueprop = HOLogic.mk_Trueprop;
     1.5  fun All xs t = Term.list_all_free (xs, t);
     1.6  
     1.7 -infix 9 $$;
     1.8  infix 0 :== ===;
     1.9  infixr 0 ==>;
    1.10  
    1.11 -val op $$ = Term.list_comb;
    1.12  val op :== = Primitive_Defs.mk_defpair;
    1.13  val op === = Trueprop o HOLogic.mk_eq;
    1.14  val op ==> = Logic.mk_implies;
    1.15 @@ -586,9 +584,9 @@
    1.16    let
    1.17      val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
    1.18        Records_Data.get thy;
    1.19 -    val data = make_record_data records sel_upd
    1.20 -      equalities extinjects (Symtab.update_new (name, thm) extsplit) splits
    1.21 -      extfields fieldext;
    1.22 +    val data =
    1.23 +      make_record_data records sel_upd equalities extinjects
    1.24 +        (Symtab.update_new (name, thm) extsplit) splits extfields fieldext;
    1.25    in Records_Data.put data thy end;
    1.26  
    1.27  
    1.28 @@ -598,9 +596,9 @@
    1.29    let
    1.30      val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
    1.31        Records_Data.get thy;
    1.32 -    val data = make_record_data records sel_upd
    1.33 -      equalities extinjects extsplit (Symtab.update_new (name, thmP) splits)
    1.34 -      extfields fieldext;
    1.35 +    val data =
    1.36 +      make_record_data records sel_upd equalities extinjects extsplit
    1.37 +        (Symtab.update_new (name, thmP) splits) extfields fieldext;
    1.38    in Records_Data.put data thy end;
    1.39  
    1.40  val get_splits = Symtab.lookup o #splits o Records_Data.get;
    1.41 @@ -619,8 +617,7 @@
    1.42      val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
    1.43        Records_Data.get thy;
    1.44      val data =
    1.45 -      make_record_data records sel_upd
    1.46 -        equalities extinjects extsplit splits
    1.47 +      make_record_data records sel_upd equalities extinjects extsplit splits
    1.48          (Symtab.update_new (name, fields) extfields) fieldext;
    1.49    in Records_Data.put data thy end;
    1.50  
    1.51 @@ -701,7 +698,8 @@
    1.52  
    1.53  fun decode_type thy t =
    1.54    let
    1.55 -    fun get_sort xs n = AList.lookup (op =) xs (n: indexname) |> the_default (Sign.defaultS thy);
    1.56 +    fun get_sort env xi =
    1.57 +      the_default (Sign.defaultS thy) (AList.lookup (op =) env (xi: indexname));
    1.58      val map_sort = Sign.intern_sort thy;
    1.59    in
    1.60      Syntax.typ_of_term (get_sort (Syntax.term_sorts map_sort t)) map_sort t
    1.61 @@ -711,6 +709,8 @@
    1.62  
    1.63  (* parse translations *)
    1.64  
    1.65 +local
    1.66 +
    1.67  fun gen_field_tr mark sfx (t as Const (c, _) $ Const (name, _) $ arg) =
    1.68        if c = mark then Syntax.const (suffix sfx name) $ Abs ("_", dummyT, arg)
    1.69        else raise TERM ("gen_field_tr: " ^ mark, [t])
    1.70 @@ -721,17 +721,20 @@
    1.71        else [gen_field_tr mark sfx tm]
    1.72    | gen_fields_tr _ mark sfx tm = [gen_field_tr mark sfx tm];
    1.73  
    1.74 +in
    1.75  
    1.76  fun record_update_tr [t, u] =
    1.77        fold (curry op $)
    1.78          (gen_fields_tr @{syntax_const "_updates"} @{syntax_const "_update"} updateN u) t
    1.79    | record_update_tr ts = raise TERM ("record_update_tr", ts);
    1.80  
    1.81 -fun update_name_tr (Free (x, T) :: ts) = Free (suffix updateN x, T) $$ ts
    1.82 -  | update_name_tr (Const (x, T) :: ts) = Const (suffix updateN x, T) $$ ts
    1.83 +end;
    1.84 +
    1.85 +fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix updateN x, T), ts)
    1.86 +  | update_name_tr (Const (x, T) :: ts) = list_comb (Const (suffix updateN x, T), ts)
    1.87    | update_name_tr (((c as Const (@{syntax_const "_constrain"}, _)) $ t $ ty) :: ts) =
    1.88        (* FIXME @{type_syntax} *)
    1.89 -      (c $ update_name_tr [t] $ (Syntax.const "fun" $ ty $ Syntax.const "dummy")) $$ ts
    1.90 +      list_comb (c $ update_name_tr [t] $ (Syntax.const "fun" $ ty $ Syntax.const "dummy"), ts)
    1.91    | update_name_tr ts = raise TERM ("update_name_tr", ts);
    1.92  
    1.93  fun dest_ext_field mark (t as (Const (c, _) $ Const (name, _) $ arg)) =
    1.94 @@ -2091,15 +2094,18 @@
    1.95      val upd_specs = map mk_upd_spec (fields_more ~~ lastN updator_thms);
    1.96  
    1.97      (*derived operations*)
    1.98 -    val make_spec = Const (full (Binding.name makeN), all_types ---> recT0) $$ all_vars :==
    1.99 -      mk_rec (all_vars @ [HOLogic.unit]) 0;
   1.100 -    val fields_spec = Const (full (Binding.name fields_selN), types ---> Type extension) $$ vars :==
   1.101 -      mk_rec (all_vars @ [HOLogic.unit]) parent_len;
   1.102 +    val make_spec =
   1.103 +      list_comb (Const (full (Binding.name makeN), all_types ---> recT0), all_vars) :==
   1.104 +        mk_rec (all_vars @ [HOLogic.unit]) 0;
   1.105 +    val fields_spec =
   1.106 +      list_comb (Const (full (Binding.name fields_selN), types ---> Type extension), vars) :==
   1.107 +        mk_rec (all_vars @ [HOLogic.unit]) parent_len;
   1.108      val extend_spec =
   1.109        Const (full (Binding.name extendN), recT0 --> moreT --> rec_schemeT0) $ r_unit0 $ more :==
   1.110 -      mk_rec ((map (mk_sel r_unit0) all_fields) @ [more]) 0;
   1.111 -    val truncate_spec = Const (full (Binding.name truncateN), rec_schemeT0 --> recT0) $ r0 :==
   1.112 -      mk_rec ((map (mk_sel r0) all_fields) @ [HOLogic.unit]) 0;
   1.113 +        mk_rec ((map (mk_sel r_unit0) all_fields) @ [more]) 0;
   1.114 +    val truncate_spec =
   1.115 +      Const (full (Binding.name truncateN), rec_schemeT0 --> recT0) $ r0 :==
   1.116 +        mk_rec ((map (mk_sel r0) all_fields) @ [HOLogic.unit]) 0;
   1.117  
   1.118  
   1.119      (* 2st stage: defs_thy *)