Domain package uses ContProc for beta reduction
authorhuffman
Wed Jun 15 23:35:43 2005 +0200 (2005-06-15)
changeset 16403294a7864063e
parent 16402 36f41d5e3b3e
child 16404 5f263e81e366
Domain package uses ContProc for beta reduction
src/HOLCF/cont_proc.ML
src/HOLCF/domain/theorems.ML
     1.1 --- a/src/HOLCF/cont_proc.ML	Wed Jun 15 21:48:35 2005 +0200
     1.2 +++ b/src/HOLCF/cont_proc.ML	Wed Jun 15 23:35:43 2005 +0200
     1.3 @@ -7,6 +7,7 @@
     1.4  sig
     1.5    val is_lcf_term: term -> bool
     1.6    val cont_thms: term -> thm list
     1.7 +  val all_cont_thms: term -> thm list
     1.8    val cont_proc: theory -> simproc
     1.9    val setup: (theory -> theory) list
    1.10  end;
    1.11 @@ -57,20 +58,22 @@
    1.12          in (map (fn y => SOME (k y RS Lx)) ys, x') end;
    1.13  
    1.14    (* first list: cont thm for each dangling bound variable *)
    1.15 -  (* second list: cont thm for each LAM *)
    1.16 -  fun cont_thms1 (Const _ $ f $ t) = let
    1.17 -        val (cs1,ls1) = cont_thms1 f;
    1.18 -        val (cs2,ls2) = cont_thms1 t;
    1.19 -        in (zip cs1 cs2, ls1 @ ls2) end
    1.20 -    | cont_thms1 (Const _ $ Abs (_,_,t)) = let
    1.21 -        val (cs,ls) = cont_thms1 t;
    1.22 +  (* second list: cont thm for each LAM in t *)
    1.23 +  (* if b = false, only return cont thm for outermost LAMs *)
    1.24 +  fun cont_thms1 b (Const _ $ f $ t) = let
    1.25 +        val (cs1,ls1) = cont_thms1 b f;
    1.26 +        val (cs2,ls2) = cont_thms1 b t;
    1.27 +        in (zip cs1 cs2, if b then ls1 @ ls2 else []) end
    1.28 +    | cont_thms1 b (Const _ $ Abs (_,_,t)) = let
    1.29 +        val (cs,ls) = cont_thms1 b t;
    1.30          val (cs',l) = lam cs;
    1.31          in (cs',l::ls) end
    1.32 -    | cont_thms1 (Bound n) = (var n, [])
    1.33 -    | cont_thms1 _ = ([],[]);
    1.34 +    | cont_thms1 _ (Bound n) = (var n, [])
    1.35 +    | cont_thms1 _ _ = ([],[]);
    1.36  in
    1.37    (* precondition: is_lcf_term t = true *)
    1.38 -  fun cont_thms t = snd (cont_thms1 t);
    1.39 +  fun cont_thms t = snd (cont_thms1 false t);
    1.40 +  fun all_cont_thms t = snd (cont_thms1 true t);
    1.41  end;
    1.42  
    1.43  (*
     2.1 --- a/src/HOLCF/domain/theorems.ML	Wed Jun 15 21:48:35 2005 +0200
     2.2 +++ b/src/HOLCF/domain/theorems.ML	Wed Jun 15 23:35:43 2005 +0200
     2.3 @@ -93,36 +93,6 @@
     2.4  (* ----- generating beta reduction rules from definitions-------------------- *)
     2.5  
     2.6  local
     2.7 -  fun k NONE = cont_const | k (SOME x) = x;
     2.8 -  
     2.9 -  fun ap NONE NONE = NONE
    2.10 -  |   ap x    y    = SOME (standard (cont2cont_Rep_CFun OF [k x, k y]));
    2.11 -
    2.12 -  fun var 0 = [SOME cont_id]
    2.13 -  |   var n = NONE :: var (n-1);
    2.14 -
    2.15 -  fun zip []      []      = []
    2.16 -  |   zip []      (y::ys) = (ap NONE y   ) :: zip [] ys
    2.17 -  |   zip (x::xs) []      = (ap x    NONE) :: zip xs []
    2.18 -  |   zip (x::xs) (y::ys) = (ap x    y   ) :: zip xs ys
    2.19 -
    2.20 -  fun lam [] = ([], cont_const)
    2.21 -  |   lam (x::ys) = let val x' = k x
    2.22 -                        val Lx = x' RS cont2cont_LAM
    2.23 -                    in  (map (fn y => SOME (k y RS Lx)) ys, x')
    2.24 -                    end;
    2.25 -
    2.26 -  fun term_conts (Bound n) = (var n, [])
    2.27 -  |   term_conts (Const _) = ([],[])
    2.28 -  |   term_conts (Const _ $ Abs (_,_,t)) = let
    2.29 -          val (cs,ls) = term_conts t
    2.30 -          val (cs',l) = lam cs
    2.31 -          in  (cs',l::ls)
    2.32 -          end
    2.33 -  |   term_conts (Const _ $ f $ t)
    2.34 -         = (zip (fst (term_conts f)) (fst (term_conts t)), [])
    2.35 -  |   term_conts t = let val dummy = prin t in ([],[]) end;
    2.36 -
    2.37    fun arglist (Const _ $ Abs (s,_,t)) = let
    2.38          val (vars,body) = arglist t
    2.39          in  (s :: vars, body) end
    2.40 @@ -131,12 +101,12 @@
    2.41    fun bound_vars 0 = [] | bound_vars i = (Bound (i-1) :: bound_vars (i-1));
    2.42  in
    2.43    fun appl_of_def def = let
    2.44 -        val (_ $ con $ lam) = concl_of def
    2.45 -        val (vars, rhs) = arglist lam
    2.46 -        val lhs = Library.foldl (op `) (con, bound_vars (length vars));
    2.47 -        val appl = bind_fun vars (lhs == rhs)
    2.48 -        val ([],cs) = term_conts lam
    2.49 -        val betas = map (fn c => mk_meta_eq (c RS beta_cfun)) cs
    2.50 +        val (_ $ con $ lam) = concl_of def;
    2.51 +        val (vars, rhs) = arglist lam;
    2.52 +        val lhs = mk_cRep_CFun (con, bound_vars (length vars));
    2.53 +        val appl = bind_fun vars (lhs == rhs);
    2.54 +        val cs = ContProc.cont_thms lam;
    2.55 +        val betas = map (fn c => mk_meta_eq (c RS beta_cfun)) cs;
    2.56          in pg (def::betas) appl [rtac reflexive_thm 1] end;
    2.57  end;
    2.58