# HG changeset patch # User huffman # Date 1287497104 25200 # Node ID a81758e0394d1d180dd81f38530eee9f4be79caa # Parent a12d35795cb9090c91955164f24acd520de93eb8 simplify fixrec pattern match function diff -r a12d35795cb9 -r a81758e0394d src/HOLCF/Tools/fixrec.ML --- a/src/HOLCF/Tools/fixrec.ML Sun Oct 17 09:53:47 2010 -0700 +++ b/src/HOLCF/Tools/fixrec.ML Tue Oct 19 07:05:04 2010 -0700 @@ -247,15 +247,15 @@ end; (* builds a monadic term for matching a function definition pattern *) -(* returns (name, arity, matcher) *) +(* returns (constant, (vars, matcher)) *) fun compile_lhs match_name pat rhs vs taken = case pat of Const(@{const_name Rep_CFun}, _) $ f $ x => let val (rhs', v, taken') = compile_pat match_name x rhs taken; in compile_lhs match_name f rhs' (v::vs) taken' end - | Free(_,_) => ((pat, length vs), big_lambdas vs rhs) - | Const(_,_) => ((pat, length vs), big_lambdas vs rhs) - | _ => fixrec_err ("function is not declared as constant in theory: " + | Free(_,_) => (pat, (vs, rhs)) + | Const(_,_) => (pat, (vs, rhs)) + | _ => fixrec_err ("invalid function pattern: " ^ ML_Syntax.print_term pat); fun strip_alls t = @@ -268,41 +268,24 @@ compile_lhs match_name lhs (mk_succeed rhs) [] (taken_names eq) end; -(* returns the sum (using +++) of the terms in ms *) -(* also applies "run" to the result! *) -fun fatbar arity ms = - let - fun LAM_Ts 0 t = ([], Term.fastype_of t) - | LAM_Ts n (_ $ Abs(_,T,t)) = - let val (Ts, U) = LAM_Ts (n-1) t in (T::Ts, U) end - | LAM_Ts _ _ = fixrec_err "fatbar: internal error, not enough LAMs"; - fun unLAM 0 t = t - | unLAM n (_$Abs(_,_,t)) = unLAM (n-1) t - | unLAM _ _ = fixrec_err "fatbar: internal error, not enough LAMs"; - fun reLAM ([], U) t = t - | reLAM (T::Ts, U) t = reLAM (Ts, T ->> U) (cabs_const(T,U)$Abs("",T,t)); - val msum = foldr1 mk_mplus (map (unLAM arity) ms); - val (Ts, U) = LAM_Ts arity (hd ms) - in - reLAM (rev Ts, dest_matchT U) (mk_run msum) - end; - (* this is the pattern-matching compiler function *) fun compile_eqs match_name eqs = let - val ((names, arities), mats) = - apfst ListPair.unzip (ListPair.unzip (map (compile_eq match_name) eqs)); - val cname = - case distinct (op =) names of + val (consts, matchers) = + ListPair.unzip (map (compile_eq match_name) eqs); + val const = + case distinct (op =) consts of [n] => n | _ => fixrec_err "all equations in block must define the same function"; - val arity = - case distinct (op =) arities of - [a] => a + val vars = + case distinct (op = o pairself length) (map fst matchers) of + [vars] => vars | _ => fixrec_err "all equations in block must have the same arity"; - val rhs = fatbar arity mats; + (* rename so all matchers use same free variables *) + fun rename (vs, t) = Term.subst_free (filter_out (op =) (vs ~~ vars)) t; + val rhs = big_lambdas vars (mk_run (foldr1 mk_mplus (map rename matchers))); in - mk_trp (cname === rhs) + mk_trp (const === rhs) end; (*************************************************************************)