added add_fixrec_i, add_fixpat_i;
authorwenzelm
Mon Jun 20 22:14:02 2005 +0200 (2005-06-20)
changeset 1648838bc902946b2
parent 16487 2060ebae96f9
child 16489 f66ab8a4e98f
added add_fixrec_i, add_fixpat_i;
ThyParse obsolete;
Sign.read_prop, Sign.cert_prop;
src/HOLCF/fixrec_package.ML
     1.1 --- a/src/HOLCF/fixrec_package.ML	Mon Jun 20 22:14:01 2005 +0200
     1.2 +++ b/src/HOLCF/fixrec_package.ML	Mon Jun 20 22:14:02 2005 +0200
     1.3 @@ -8,15 +8,14 @@
     1.4  signature FIXREC_PACKAGE =
     1.5  sig
     1.6    val add_fixrec: ((string * Attrib.src list) * string) list list -> theory -> theory
     1.7 +  val add_fixrec_i: ((string * theory attribute list) * term) list list -> theory -> theory
     1.8    val add_fixpat: ((string * Attrib.src list) * string) list -> theory -> theory
     1.9 +  val add_fixpat_i: ((string * theory attribute list) * term) list -> theory -> theory
    1.10  end;
    1.11  
    1.12  structure FixrecPackage: FIXREC_PACKAGE =
    1.13  struct
    1.14  
    1.15 -local
    1.16 -open ThyParse in
    1.17 -
    1.18  (* ->> is taken from holcf_logic.ML *)
    1.19  (* TODO: fix dependencies so we can import HOLCFLogic here *)
    1.20  infixr 6 ->>;
    1.21 @@ -234,44 +233,50 @@
    1.22  (*************************************************************************)
    1.23  
    1.24  (* this calls the main processing function and then returns the new state *)
    1.25 -fun add_fixrec blocks thy =
    1.26 +fun gen_add_fixrec prep_prop prep_attrib blocks thy =
    1.27    let
    1.28 -    val sg = sign_of thy;
    1.29      fun split_list2 xss = split_list (map split_list xss);
    1.30      val ((namess, srcsss), strss) = apfst split_list2 (split_list2 blocks);
    1.31 -    val attss = map (map (map (Attrib.global_attribute thy))) srcsss;
    1.32 -    val tss = map (map (term_of o Thm.read_cterm sg o rpair propT)) strss;
    1.33 -    val ts' = map (infer sg o compile_pats) tss;
    1.34 +    val attss = map (map (map (prep_attrib thy))) srcsss;
    1.35 +    val tss = map (map (prep_prop thy)) strss;
    1.36 +    val ts' = map (infer thy o compile_pats) tss;
    1.37      val (thy', cnames, fixdef_thms, unfold_thms) = add_fixdefs ts' thy;
    1.38    in
    1.39      make_simps cnames unfold_thms namess attss tss thy'
    1.40    end;
    1.41  
    1.42 +val add_fixrec = gen_add_fixrec Sign.read_prop Attrib.global_attribute;
    1.43 +val add_fixrec_i = gen_add_fixrec Sign.cert_prop (K I);
    1.44 +
    1.45 +
    1.46  (*************************************************************************)
    1.47  (******************************** Fixpat *********************************)
    1.48  (*************************************************************************)
    1.49  
    1.50 -fun fix_pat thy pat = 
    1.51 +fun fix_pat prep_term thy pat = 
    1.52    let
    1.53 -    val sg = sign_of thy;
    1.54 -    val t = term_of (Thm.read_cterm sg (pat, dummyT));
    1.55 +    val t = prep_term thy pat;
    1.56      val T = fastype_of t;
    1.57      val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T));
    1.58      val cname = case chead_of t of Const(c,_) => c | _ =>
    1.59                sys_error "FIXPAT: function is not declared as constant in theory";
    1.60 -    val unfold_thm = Goals.get_thm thy (cname^"_unfold");
    1.61 -    val rew = prove_goalw_cterm [] (cterm_of sg eq)
    1.62 +    val unfold_thm = PureThy.get_thm thy (Name (cname^"_unfold"));
    1.63 +    val rew = prove_goalw_cterm [] (cterm_of thy eq)
    1.64            (fn _ => [stac unfold_thm 1, simp_tac (simpset_of thy) 1]);
    1.65    in rew end;
    1.66  
    1.67 -fun add_fixpat pats thy = 
    1.68 +fun gen_add_fixpat prep_term prep_attrib pats thy =
    1.69    let
    1.70      val ((names, srcss), strings) = apfst ListPair.unzip (ListPair.unzip pats);
    1.71 -    val atts = map (map (Attrib.global_attribute thy)) srcss;
    1.72 -    val simps = map (fix_pat thy) strings;
    1.73 +    val atts = map (map (prep_attrib thy)) srcss;
    1.74 +    val simps = map (fix_pat prep_term thy) strings;
    1.75      val (thy', _) = PureThy.add_thms ((names ~~ simps) ~~ atts) thy;
    1.76    in thy' end;
    1.77  
    1.78 +val add_fixpat = gen_add_fixpat Sign.read_term Attrib.global_attribute;
    1.79 +val add_fixpat_i = gen_add_fixpat Sign.cert_term (K I);
    1.80 +
    1.81 +
    1.82  (*************************************************************************)
    1.83  (******************************** Parsers ********************************)
    1.84  (*************************************************************************)
    1.85 @@ -300,6 +305,4 @@
    1.86  
    1.87  end; (* local structure *)
    1.88  
    1.89 -end; (* local open *)
    1.90 -
    1.91  end; (* struct *)