src/Provers/classical.ML
changeset 6556 daa00919502b
parent 6502 bc30e13b36a8
child 6955 9e2d97ef55d2
equal deleted inserted replaced
6555:17b7b88a8e3c 6556:daa00919502b
    29 sig
    29 sig
    30   val clasetN: string
    30   val clasetN: string
    31   val clasetK: Object.kind
    31   val clasetK: Object.kind
    32   exception ClasetData of Object.T ref
    32   exception ClasetData of Object.T ref
    33   val setup: (theory -> theory) list
    33   val setup: (theory -> theory) list
    34   val fix_methods: Object.T * (Object.T -> Object.T) *
    34   val fix_methods: Object.T * (Object.T -> Object.T) * (Object.T -> Object.T) *
    35     (Object.T * Object.T -> Object.T) * (Sign.sg -> Object.T -> unit) -> unit
    35     (Object.T * Object.T -> Object.T) * (Sign.sg -> Object.T -> unit) -> unit
    36 end;
    36 end;
    37 
    37 
    38 signature CLASSICAL_DATA =
    38 signature CLASSICAL_DATA =
    39 sig
    39 sig
   179 
   179 
   180 local
   180 local
   181   fun undef _ = raise Match;
   181   fun undef _ = raise Match;
   182 
   182 
   183   val empty_ref = ref ERROR;
   183   val empty_ref = ref ERROR;
       
   184   val copy_fn = ref (undef: Object.T -> Object.T);
   184   val prep_ext_fn = ref (undef: Object.T -> Object.T);
   185   val prep_ext_fn = ref (undef: Object.T -> Object.T);
   185   val merge_fn = ref (undef: Object.T * Object.T -> Object.T);
   186   val merge_fn = ref (undef: Object.T * Object.T -> Object.T);
   186   val print_fn = ref (undef: Sign.sg -> Object.T -> unit);
   187   val print_fn = ref (undef: Sign.sg -> Object.T -> unit);
   187 
   188 
   188   val empty = ClasetData empty_ref;
   189   val empty = ClasetData empty_ref;
       
   190   fun copy exn = ! copy_fn exn;
   189   fun prep_ext exn = ! prep_ext_fn exn;
   191   fun prep_ext exn = ! prep_ext_fn exn;
   190   fun merge exn = ! merge_fn exn;
   192   fun merge exn = ! merge_fn exn;
   191   fun print sg exn = ! print_fn sg exn;
   193   fun print sg exn = ! print_fn sg exn;
   192 in
   194 in
   193   val setup = [Theory.init_data clasetK (empty, prep_ext, merge, print)];
   195   val setup = [Theory.init_data clasetK (empty, copy, prep_ext, merge, print)];
   194   fun fix_methods (e, ext, mrg, prt) =
   196   fun fix_methods (e, cp, ext, mrg, prt) =
   195     (empty_ref := e; prep_ext_fn := ext; merge_fn := mrg; print_fn := prt);
   197     (empty_ref := e; copy_fn := cp; prep_ext_fn := ext; merge_fn := mrg; print_fn := prt);
   196 end;
   198 end;
   197 
   199 
   198 
   200 
   199 end;
   201 end;
   200 
   202 
   785 
   787 
   786 local
   788 local
   787   val empty = CSData (ref empty_cs);
   789   val empty = CSData (ref empty_cs);
   788 
   790 
   789   (*create new references*)
   791   (*create new references*)
   790   fun prep_ext (ClasetData (ref (CSData (ref cs)))) =
   792   fun copy (ClasetData (ref (CSData (ref cs)))) =
   791     ClasetData (ref (CSData (ref cs)));
   793     ClasetData (ref (CSData (ref cs)));
       
   794   val prep_ext = copy;
   792 
   795 
   793   fun merge (ClasetData (ref (CSData (ref cs1))), ClasetData (ref (CSData (ref cs2)))) =
   796   fun merge (ClasetData (ref (CSData (ref cs1))), ClasetData (ref (CSData (ref cs2)))) =
   794     ClasetData (ref (CSData (ref (merge_cs (cs1, cs2)))));
   797     ClasetData (ref (CSData (ref (merge_cs (cs1, cs2)))));
   795 
   798 
   796   fun print (_: Sign.sg) (ClasetData (ref (CSData (ref cs)))) = print_cs cs;
   799   fun print (_: Sign.sg) (ClasetData (ref (CSData (ref cs)))) = print_cs cs;
   797 in
   800 in
   798   val _ = fix_methods (empty, prep_ext, merge, print);
   801   val _ = fix_methods (empty, copy, prep_ext, merge, print);
   799 end;
   802 end;
   800 
   803 
   801 
   804 
   802 (* access claset *)
   805 (* access claset *)
   803 
   806