cleanup in typedef/datatype package
authorhaftmann
Thu Apr 06 16:13:17 2006 +0200 (2006-04-06)
changeset 1934936e537f89585
parent 19348 f2283f334e42
child 19350 2e1c7ca05ee0
cleanup in typedef/datatype package
TFL/tfl.ML
TFL/thry.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Import/replay.ML
src/HOLCF/IOA/Modelcheck/MuIOA.ML
src/HOLCF/pcpodef_package.ML
     1.1 --- a/TFL/tfl.ML	Thu Apr 06 16:12:57 2006 +0200
     1.2 +++ b/TFL/tfl.ML	Thu Apr 06 16:13:17 2006 +0200
     1.3 @@ -449,7 +449,7 @@
     1.4         not simplified. Otherwise large examples (Red-Black trees) are too
     1.5         slow.*)
     1.6       val case_ss = HOL_basic_ss addcongs
     1.7 -       DatatypePackage.weak_case_congs_of theory addsimps case_rewrites
     1.8 +       (map (#weak_case_cong o snd) o Symtab.dest o DatatypePackage.get_datatypes) theory addsimps case_rewrites
     1.9       val corollaries' = map (Simplifier.simplify case_ss) corollaries
    1.10       val extract = R.CONTEXT_REWRITE_RULE
    1.11                       (f, [R], cut_apply, meta_tflCongs@context_congs)
     2.1 --- a/TFL/thry.ML	Thu Apr 06 16:12:57 2006 +0200
     2.2 +++ b/TFL/thry.ML	Thu Apr 06 16:13:17 2006 +0200
     2.3 @@ -59,22 +59,21 @@
     2.4   * Get information about datatypes
     2.5   *---------------------------------------------------------------------------*)
     2.6  
     2.7 -val get_info = Symtab.lookup o DatatypePackage.get_datatypes;
     2.8 -
     2.9 -fun match_info thy tname =
    2.10 -  case (DatatypePackage.case_const_of thy tname, DatatypePackage.constrs_of thy tname) of
    2.11 -      (SOME case_const, SOME constructors) =>
    2.12 -        SOME {case_const = case_const, constructors = constructors}
    2.13 +fun match_info thy dtco =
    2.14 +  case (DatatypePackage.get_datatype thy dtco,
    2.15 +         DatatypePackage.get_datatype_constrs thy dtco) of
    2.16 +      (SOME { case_name, ... }, SOME constructors) =>
    2.17 +        SOME {case_const = Const (case_name, Sign.the_const_type thy case_name), constructors = map Const constructors}
    2.18      | _ => NONE;
    2.19  
    2.20 -fun induct_info thy tname = case get_info thy tname of
    2.21 +fun induct_info thy dtco = case DatatypePackage.get_datatype thy dtco of
    2.22          NONE => NONE
    2.23        | SOME {nchotomy, ...} =>
    2.24            SOME {nchotomy = nchotomy,
    2.25 -                constructors = valOf (DatatypePackage.constrs_of thy tname)};
    2.26 +                constructors = (map Const o the o DatatypePackage.get_datatype_constrs thy) dtco};
    2.27  
    2.28  fun extract_info thy =
    2.29 - let val infos = map snd (Symtab.dest (DatatypePackage.get_datatypes thy))
    2.30 + let val infos = (map snd o Symtab.dest o DatatypePackage.get_datatypes) thy
    2.31   in {case_congs = map (mk_meta_eq o #case_cong) infos,
    2.32       case_rewrites = List.concat (map (map mk_meta_eq o #case_rewrites) infos)}
    2.33   end;
     3.1 --- a/src/HOL/Import/proof_kernel.ML	Thu Apr 06 16:12:57 2006 +0200
     3.2 +++ b/src/HOL/Import/proof_kernel.ML	Thu Apr 06 16:13:17 2006 +0200
     3.3 @@ -2094,7 +2094,7 @@
     3.4  	    val tnames = map fst tfrees
     3.5  	    val tsyn = mk_syn thy tycname
     3.6  	    val typ = (tycname,tnames,tsyn)
     3.7 -	    val (thy',typedef_info) = TypedefPackage.add_typedef_i false (SOME thmname) typ c NONE (rtac th2 1) thy	    
     3.8 +	    val (typedef_info, thy') = TypedefPackage.add_typedef_i false (SOME thmname) typ c NONE (rtac th2 1) thy	    
     3.9              val _ = ImportRecorder.add_typedef (SOME thmname) typ c NONE th2
    3.10  				      
    3.11  	    val th3 = (#type_definition typedef_info) RS typedef_hol2hol4
    3.12 @@ -2187,7 +2187,7 @@
    3.13  	    val tnames = sort string_ord (map fst tfrees)
    3.14  	    val tsyn = mk_syn thy tycname
    3.15  	    val typ = (tycname,tnames,tsyn)
    3.16 -	    val (thy', typedef_info) = TypedefPackage.add_typedef_i false NONE typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy
    3.17 +	    val (typedef_info, thy') = TypedefPackage.add_typedef_i false NONE typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy
    3.18  	    val _ = ImportRecorder.add_typedef NONE typ c (SOME(rep_name,abs_name)) th2
    3.19  	    val fulltyname = Sign.intern_type thy' tycname
    3.20  	    val aty = Type (fulltyname, map mk_vartype tnames)
     4.1 --- a/src/HOL/Import/replay.ML	Thu Apr 06 16:12:57 2006 +0200
     4.2 +++ b/src/HOL/Import/replay.ML	Thu Apr 06 16:13:17 2006 +0200
     4.3 @@ -344,7 +344,7 @@
     4.4  	  | delta (Hol_theorem (thyname, thmname, th)) thy =
     4.5  	    add_hol4_theorem thyname thmname ([], th_of thy th) thy
     4.6  	  | delta (Typedef (thmname, typ, c, repabs, th)) thy = 
     4.7 -	    fst(TypedefPackage.add_typedef_i false thmname typ c repabs (rtac (th_of thy th) 1) thy)
     4.8 +	    snd (TypedefPackage.add_typedef_i false thmname typ c repabs (rtac (th_of thy th) 1) thy)
     4.9  	  | delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy =  
    4.10  	    add_hol4_type_mapping thyname tycname true fulltyname thy
    4.11  	  | delta (Indexed_theorem (i, th)) thy = 
     5.1 --- a/src/HOLCF/IOA/Modelcheck/MuIOA.ML	Thu Apr 06 16:12:57 2006 +0200
     5.2 +++ b/src/HOLCF/IOA/Modelcheck/MuIOA.ML	Thu Apr 06 16:13:17 2006 +0200
     5.3 @@ -157,14 +157,12 @@
     5.4  
     5.5  in
     5.6  
     5.7 -fun mk_sim_oracle sign (subgoal,thl) =
     5.8 -(let
     5.9 -        val weak_case_congs = DatatypePackage.weak_case_congs_of sign;
    5.10 -
    5.11 -	val concl = (Logic.strip_imp_concl subgoal);
    5.12 -
    5.13 -	val ic_str = delete_ul_string(Sign.string_of_term sign (IntC sign concl));
    5.14 -	val ia_str = delete_ul_string(Sign.string_of_term sign (IntA sign concl));
    5.15 +fun mk_sim_oracle sign (subgoal, thl) = (
    5.16 +  let
    5.17 +    val weak_case_congs = (map (#weak_case_cong o snd) o Symtab.dest o DatatypePackage.get_datatypes) sign;
    5.18 +    val concl = Logic.strip_imp_concl subgoal;
    5.19 +    val ic_str = delete_ul_string(Sign.string_of_term sign (IntC sign concl));
    5.20 +    val ia_str = delete_ul_string(Sign.string_of_term sign (IntA sign concl));
    5.21  	val sc_str = delete_ul_string(Sign.string_of_term sign (StartC sign concl));	
    5.22  	val sa_str = delete_ul_string(Sign.string_of_term sign (StartA sign concl));
    5.23  	val tc_str = delete_ul_string(Sign.string_of_term sign (TransC sign concl));
     6.1 --- a/src/HOLCF/pcpodef_package.ML	Thu Apr 06 16:12:57 2006 +0200
     6.2 +++ b/src/HOLCF/pcpodef_package.ML	Thu Apr 06 16:13:17 2006 +0200
     6.3 @@ -98,14 +98,13 @@
     6.4      fun make_po tac thy =
     6.5        thy
     6.6        |> TypedefPackage.add_typedef_i def (SOME name) (t, vs, mx) set opt_morphs tac
     6.7 -      |>> AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.sq_ord"])
     6.8 +      ||> AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.sq_ord"])
     6.9             (ClassPackage.intro_classes_tac [])
    6.10 -      |>>> (PureThy.add_defs_i true [Thm.no_attributes less_def] #> Library.swap)
    6.11 -      |> (fn (thy', ({type_definition, set_def, ...}, [less_definition])) =>
    6.12 -           thy'
    6.13 -           |> AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.po"])
    6.14 +      ||>> PureThy.add_defs_i true [Thm.no_attributes less_def]
    6.15 +      |-> (fn ({type_definition, set_def, ...}, [less_definition]) =>
    6.16 +          AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.po"])
    6.17               (Tactic.rtac (typedef_po OF [type_definition, less_definition]) 1)
    6.18 -           |> rpair (type_definition, less_definition, set_def));
    6.19 +           #> rpair (type_definition, less_definition, set_def));
    6.20      
    6.21      fun make_cpo admissible (theory, defs as (type_def, less_def, set_def)) =
    6.22        let