use TheoryData to keep track of pattern match combinators
authorhuffman
Thu Feb 26 10:28:53 2009 -0800 (2009-02-26)
changeset 301316be1be402ef0
parent 30130 e23770bc97c8
child 30132 243a05a67c41
use TheoryData to keep track of pattern match combinators
src/HOLCF/Fixrec.thy
src/HOLCF/Tools/domain/domain_axioms.ML
src/HOLCF/Tools/fixrec_package.ML
     1.1 --- a/src/HOLCF/Fixrec.thy	Thu Feb 26 08:48:33 2009 -0800
     1.2 +++ b/src/HOLCF/Fixrec.thy	Thu Feb 26 10:28:53 2009 -0800
     1.3 @@ -583,6 +583,20 @@
     1.4  
     1.5  use "Tools/fixrec_package.ML"
     1.6  
     1.7 +setup {* FixrecPackage.setup *}
     1.8 +
     1.9 +setup {*
    1.10 +  FixrecPackage.add_matchers
    1.11 +    [ (@{const_name up}, @{const_name match_up}),
    1.12 +      (@{const_name sinl}, @{const_name match_sinl}),
    1.13 +      (@{const_name sinr}, @{const_name match_sinr}),
    1.14 +      (@{const_name spair}, @{const_name match_spair}),
    1.15 +      (@{const_name cpair}, @{const_name match_cpair}),
    1.16 +      (@{const_name ONE}, @{const_name match_ONE}),
    1.17 +      (@{const_name TT}, @{const_name match_TT}),
    1.18 +      (@{const_name FF}, @{const_name match_FF}) ]
    1.19 +*}
    1.20 +
    1.21  hide (open) const return bind fail run cases
    1.22  
    1.23  end
     2.1 --- a/src/HOLCF/Tools/domain/domain_axioms.ML	Thu Feb 26 08:48:33 2009 -0800
     2.2 +++ b/src/HOLCF/Tools/domain/domain_axioms.ML	Thu Feb 26 10:28:53 2009 -0800
     2.3 @@ -39,7 +39,7 @@
     2.4      fun one_con (con,args) =
     2.5          foldr /\# (list_ccomb (%%:con, mapn (idxs (length args)) 1 args)) args;
     2.6    in ("copy_def", %%:(dname^"_copy") ==
     2.7 -       /\"f" (list_ccomb (%%:(dname^"_when"), map one_con cons))) end;
     2.8 +       /\ "f" (list_ccomb (%%:(dname^"_when"), map one_con cons))) end;
     2.9  
    2.10  (* -- definitions concerning the constructors, discriminators and selectors - *)
    2.11  
    2.12 @@ -107,7 +107,7 @@
    2.13      [when_def, copy_def] @
    2.14       con_defs @ dis_defs @ mat_defs @ pat_defs @ sel_defs @
    2.15      [take_def, finite_def])
    2.16 -end; (* let *)
    2.17 +end; (* let (calc_axioms) *)
    2.18  
    2.19  fun infer_props thy = map (apsnd (FixrecPackage.legacy_infer_prop thy));
    2.20  
    2.21 @@ -117,6 +117,14 @@
    2.22  fun add_defs_i x = snd o (PureThy.add_defs false) (map (Thm.no_attributes o apfst Binding.name) x);
    2.23  fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
    2.24  
    2.25 +fun add_matchers (((dname,_),cons) : eq) thy =
    2.26 +  let
    2.27 +    val con_names = map fst cons;
    2.28 +    val mat_names = map mat_name con_names;
    2.29 +    fun qualify n = Sign.full_name thy (Binding.name n);
    2.30 +    val ms = map qualify con_names ~~ map qualify mat_names;
    2.31 +  in FixrecPackage.add_matchers ms thy end;
    2.32 +
    2.33  in (* local *)
    2.34  
    2.35  fun add_axioms (comp_dnam, eqs : eq list) thy' = let
    2.36 @@ -125,7 +133,7 @@
    2.37    val x_name = idx_name dnames "x"; 
    2.38    fun copy_app dname = %%:(dname^"_copy")`Bound 0;
    2.39    val copy_def = ("copy_def" , %%:(comp_dname^"_copy") ==
    2.40 -				    /\"f"(mk_ctuple (map copy_app dnames)));
    2.41 +				    /\ "f"(mk_ctuple (map copy_app dnames)));
    2.42    val bisim_def = ("bisim_def",%%:(comp_dname^"_bisim")==mk_lam("R",
    2.43      let
    2.44        fun one_con (con,args) = let
    2.45 @@ -164,7 +172,8 @@
    2.46  in thy |> Sign.add_path comp_dnam  
    2.47         |> add_defs_infer (bisim_def::(if length eqs>1 then [copy_def] else []))
    2.48         |> Sign.parent_path
    2.49 -end;
    2.50 +       |> fold add_matchers eqs
    2.51 +end; (* let (add_axioms) *)
    2.52  
    2.53  end; (* local *)
    2.54  end; (* struct *)
     3.1 --- a/src/HOLCF/Tools/fixrec_package.ML	Thu Feb 26 08:48:33 2009 -0800
     3.2 +++ b/src/HOLCF/Tools/fixrec_package.ML	Thu Feb 26 10:28:53 2009 -0800
     3.3 @@ -12,6 +12,8 @@
     3.4    val add_fixrec_i: bool -> ((binding * attribute list) * term) list list -> theory -> theory
     3.5    val add_fixpat: Attrib.binding * string list -> theory -> theory
     3.6    val add_fixpat_i: (binding * attribute list) * term list -> theory -> theory
     3.7 +  val add_matchers: (string * string) list -> theory -> theory
     3.8 +  val setup: theory -> theory
     3.9  end;
    3.10  
    3.11  structure FixrecPackage: FIXREC_PACKAGE =
    3.12 @@ -123,6 +125,17 @@
    3.13  (*********** monadic notation and pattern matching compilation ***********)
    3.14  (*************************************************************************)
    3.15  
    3.16 +structure FixrecMatchData = TheoryDataFun (
    3.17 +  type T = string Symtab.table;
    3.18 +  val empty = Symtab.empty;
    3.19 +  val copy = I;
    3.20 +  val extend = I;
    3.21 +  fun merge _ tabs : T = Symtab.merge (K true) tabs;
    3.22 +);
    3.23 +
    3.24 +(* associate match functions with pattern constants *)
    3.25 +fun add_matchers ms = FixrecMatchData.map (fold Symtab.update ms);
    3.26 +
    3.27  fun add_names (Const(a,_), bs) = insert (op =) (Sign.base_name a) bs
    3.28    | add_names (Free(a,_) , bs) = insert (op =) a bs
    3.29    | add_names (f $ u     , bs) = add_names (f, add_names(u, bs))
    3.30 @@ -132,20 +145,20 @@
    3.31  fun add_terms ts xs = foldr add_names xs ts;
    3.32  
    3.33  (* builds a monadic term for matching a constructor pattern *)
    3.34 -fun pre_build pat rhs vs taken =
    3.35 +fun pre_build match_name pat rhs vs taken =
    3.36    case pat of
    3.37      Const(@{const_name Rep_CFun},_)$f$(v as Free(n,T)) =>
    3.38 -      pre_build f rhs (v::vs) taken
    3.39 +      pre_build match_name f rhs (v::vs) taken
    3.40    | Const(@{const_name Rep_CFun},_)$f$x =>
    3.41 -      let val (rhs', v, taken') = pre_build x rhs [] taken;
    3.42 -      in pre_build f rhs' (v::vs) taken' end
    3.43 +      let val (rhs', v, taken') = pre_build match_name x rhs [] taken;
    3.44 +      in pre_build match_name f rhs' (v::vs) taken' end
    3.45    | Const(c,T) =>
    3.46        let
    3.47          val n = Name.variant taken "v";
    3.48          fun result_type (Type(@{type_name "->"},[_,T])) (x::xs) = result_type T xs
    3.49            | result_type T _ = T;
    3.50          val v = Free(n, result_type T vs);
    3.51 -        val m = "match_"^(extern_name(Sign.base_name c));
    3.52 +        val m = match_name c;
    3.53          val k = lambda_ctuple vs rhs;
    3.54        in
    3.55          (%%:@{const_name Fixrec.bind}`(%%:m`v)`k, v, n::taken)
    3.56 @@ -155,19 +168,22 @@
    3.57  
    3.58  (* builds a monadic term for matching a function definition pattern *)
    3.59  (* returns (name, arity, matcher) *)
    3.60 -fun building pat rhs vs taken =
    3.61 +fun building match_name pat rhs vs taken =
    3.62    case pat of
    3.63      Const(@{const_name Rep_CFun}, _)$f$(v as Free(n,T)) =>
    3.64 -      building f rhs (v::vs) taken
    3.65 +      building match_name f rhs (v::vs) taken
    3.66    | Const(@{const_name Rep_CFun}, _)$f$x =>
    3.67 -      let val (rhs', v, taken') = pre_build x rhs [] taken;
    3.68 -      in building f rhs' (v::vs) taken' end
    3.69 +      let val (rhs', v, taken') = pre_build match_name x rhs [] taken;
    3.70 +      in building match_name f rhs' (v::vs) taken' end
    3.71    | Const(name,_) => (name, length vs, big_lambdas vs rhs)
    3.72    | _ => fixrec_err "function is not declared as constant in theory";
    3.73  
    3.74 -fun match_eq eq = 
    3.75 +fun match_eq match_name eq = 
    3.76    let val (lhs,rhs) = dest_eqs eq;
    3.77 -  in building lhs (%%:@{const_name Fixrec.return}`rhs) [] (add_terms [eq] []) end;
    3.78 +  in
    3.79 +    building match_name lhs (%%:@{const_name Fixrec.return}`rhs) []
    3.80 +      (add_terms [eq] [])
    3.81 +  end;
    3.82  
    3.83  (* returns the sum (using +++) of the terms in ms *)
    3.84  (* also applies "run" to the result! *)
    3.85 @@ -190,9 +206,9 @@
    3.86        in (x::xs, y::ys, z::zs) end;
    3.87  
    3.88  (* this is the pattern-matching compiler function *)
    3.89 -fun compile_pats eqs = 
    3.90 +fun compile_pats match_name eqs = 
    3.91    let
    3.92 -    val ((n::names),(a::arities),mats) = unzip3 (map match_eq eqs);
    3.93 +    val ((n::names),(a::arities),mats) = unzip3 (map (match_eq match_name) eqs);
    3.94      val cname = if forall (fn x => n=x) names then n
    3.95            else fixrec_err "all equations in block must define the same function";
    3.96      val arity = if forall (fn x => a=x) arities then a
    3.97 @@ -235,8 +251,14 @@
    3.98      
    3.99      fun unconcat [] _ = []
   3.100        | unconcat (n::ns) xs = List.take (xs,n) :: unconcat ns (List.drop (xs,n));
   3.101 +    val matcher_tab = FixrecMatchData.get thy;
   3.102 +    fun match_name c =
   3.103 +          case Symtab.lookup matcher_tab c of SOME m => m
   3.104 +            | NONE => fixrec_err ("unknown pattern constructor: " ^ c);
   3.105 +
   3.106      val pattern_blocks = unconcat lengths (map Logic.strip_imp_concl eqn_ts');
   3.107 -    val compiled_ts = map (legacy_infer_term thy o compile_pats) pattern_blocks;
   3.108 +    val compiled_ts =
   3.109 +          map (legacy_infer_term thy o compile_pats match_name) pattern_blocks;
   3.110      val (thy', cnames, fixdef_thms, unfold_thms) = add_fixdefs compiled_ts thy;
   3.111    in
   3.112      if strict then let (* only prove simp rules if strict = true *)
   3.113 @@ -312,4 +334,6 @@
   3.114  
   3.115  end; (* local structure *)
   3.116  
   3.117 +val setup = FixrecMatchData.init;
   3.118 +
   3.119  end;