move definition of case combinator to domain_constructors.ML
authorhuffman
Mon Mar 01 09:55:32 2010 -0800 (2010-03-01)
changeset 35486c91854705b1d
parent 35485 7d7495f5e35e
child 35487 d1630f317ed0
move definition of case combinator to domain_constructors.ML
src/HOLCF/Tools/Domain/domain_axioms.ML
src/HOLCF/Tools/Domain/domain_constructors.ML
src/HOLCF/Tools/Domain/domain_syntax.ML
src/HOLCF/Tools/Domain/domain_theorems.ML
     1.1 --- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Mon Mar 01 08:33:49 2010 -0800
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Mon Mar 01 09:55:32 2010 -0800
     1.3 @@ -67,10 +67,6 @@
     1.4      val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name'));
     1.5      val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name'));
     1.6  
     1.7 -    val when_def = ("when_def",%%:(dname^"_when") == 
     1.8 -        List.foldr (uncurry /\ ) (/\x_name'((when_body cons (fn (x,y) =>
     1.9 -          Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons));
    1.10 -
    1.11      val copy_def =
    1.12        let fun r i = proj (Bound 0) eqs i;
    1.13        in
    1.14 @@ -95,7 +91,7 @@
    1.15  
    1.16    in (dnam,
    1.17        (if definitional then [] else [abs_iso_ax, rep_iso_ax, reach_ax]),
    1.18 -      (if definitional then [when_def] else [when_def, copy_def]) @
    1.19 +      (if definitional then [] else [copy_def]) @
    1.20        [take_def, finite_def])
    1.21    end; (* let (calc_axioms) *)
    1.22  
     2.1 --- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Mon Mar 01 08:33:49 2010 -0800
     2.2 +++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Mon Mar 01 09:55:32 2010 -0800
     2.3 @@ -11,7 +11,6 @@
     2.4        string
     2.5        -> (binding * (bool * binding option * typ) list * mixfix) list
     2.6        -> Domain_Isomorphism.iso_info
     2.7 -      -> thm
     2.8        -> theory
     2.9        -> { con_consts : term list,
    2.10             con_betas : thm list,
    2.11 @@ -367,30 +366,81 @@
    2.12      (spec : (term * (bool * typ) list) list)
    2.13      (lhsT : typ)
    2.14      (dname : string)
    2.15 -    (case_def : thm)
    2.16      (con_betas : thm list)
    2.17      (casedist : thm)
    2.18      (iso_locale : thm)
    2.19 +    (rep_const : term)
    2.20      (thy : theory)
    2.21      : ((typ -> term) * thm list) * theory =
    2.22    let
    2.23  
    2.24 +    (* TODO: move these to holcf_library.ML *)
    2.25 +    fun one_when_const T = Const (@{const_name one_when}, T ->> oneT ->> T);
    2.26 +    fun mk_one_when t = one_when_const (fastype_of t) ` t;
    2.27 +    fun mk_sscase (t, u) =
    2.28 +      let
    2.29 +        val (T, V) = dest_cfunT (fastype_of t);
    2.30 +        val (U, V) = dest_cfunT (fastype_of u);
    2.31 +      in sscase_const (T, U, V) ` t ` u end;
    2.32 +    fun strictify_const T = Const (@{const_name strictify}, T ->> T);
    2.33 +    fun mk_strictify t = strictify_const (fastype_of t) ` t;
    2.34 +    fun ssplit_const (T, U, V) =
    2.35 +      Const (@{const_name ssplit}, (T ->> U ->> V) ->> mk_sprodT (T, U) ->> V);
    2.36 +    fun mk_ssplit t =
    2.37 +      let val (T, (U, V)) = apsnd dest_cfunT (dest_cfunT (fastype_of t));
    2.38 +      in ssplit_const (T, U, V) ` t end;
    2.39 +    fun lambda_stuple []      t = mk_one_when t
    2.40 +      | lambda_stuple [x]     t = mk_strictify (big_lambda x t)
    2.41 +      | lambda_stuple [x,y]   t = mk_ssplit (big_lambdas [x, y] t)
    2.42 +      | lambda_stuple (x::xs) t = mk_ssplit (big_lambda x (lambda_stuple xs t));
    2.43 +
    2.44 +    (* eta contraction for simplifying definitions *)
    2.45 +    fun cont_eta_contract (Const(@{const_name Abs_CFun},TT) $ Abs(a,T,body)) = 
    2.46 +        (case cont_eta_contract body  of
    2.47 +           body' as (Const(@{const_name Abs_CFun},Ta) $ f $ Bound 0) => 
    2.48 +           if not (0 mem loose_bnos f) then incr_boundvars ~1 f 
    2.49 +           else   Const(@{const_name Abs_CFun},TT) $ Abs(a,T,body')
    2.50 +         | body' => Const(@{const_name Abs_CFun},TT) $ Abs(a,T,body'))
    2.51 +      | cont_eta_contract(f$t) = cont_eta_contract f $ cont_eta_contract t
    2.52 +      | cont_eta_contract t    = t;
    2.53 +
    2.54      (* prove rep/abs rules *)
    2.55      val rep_strict = iso_locale RS @{thm iso.rep_strict};
    2.56      val abs_inverse = iso_locale RS @{thm iso.abs_iso};
    2.57  
    2.58      (* calculate function arguments of case combinator *)
    2.59 -    val resultT = TVar (("'t",0), @{sort pcpo});
    2.60 +    val tns = map (fst o dest_TFree) (snd (dest_Type lhsT));
    2.61 +    val resultT = TFree (Name.variant tns "'t", @{sort pcpo});
    2.62      fun fTs T = map (fn (_, args) => map snd args -->> T) spec;
    2.63      val fns = Datatype_Prop.indexify_names (map (K "f") spec);
    2.64      val fs = map Free (fns ~~ fTs resultT);
    2.65      fun caseT T = fTs T -->> (lhsT ->> T);
    2.66  
    2.67 -    (* TODO: move definition of case combinator here *)
    2.68 -    val case_bind = Binding.name (dname ^ "_when");
    2.69 -    val case_name = Sign.full_name thy case_bind;
    2.70 -    fun case_const T = Const (case_name, caseT T);
    2.71 -    val case_app = list_ccomb (case_const resultT, fs);
    2.72 +    (* definition of case combinator *)
    2.73 +    local
    2.74 +      val case_bind = Binding.name (dname ^ "_when");
    2.75 +      fun one_con f (_, args) =
    2.76 +        let
    2.77 +          fun argT (lazy, T) = if lazy then mk_upT T else T;
    2.78 +          fun down (lazy, T) v = if lazy then from_up T ` v else v;
    2.79 +          val Ts = map argT args;
    2.80 +          val ns = Name.variant_list fns (Datatype_Prop.make_tnames Ts);
    2.81 +          val vs = map Free (ns ~~ Ts);
    2.82 +          val xs = map2 down args vs;
    2.83 +        in
    2.84 +          cont_eta_contract (lambda_stuple vs (list_ccomb (f, xs)))
    2.85 +        end;
    2.86 +      val body = foldr1 mk_sscase (map2 one_con fs spec);
    2.87 +      val rhs = big_lambdas fs (mk_cfcomp (body, rep_const));
    2.88 +      val ((case_consts, case_defs), thy) =
    2.89 +          define_consts [(case_bind, rhs, NoSyn)] thy;
    2.90 +      val case_name = Sign.full_name thy case_bind;
    2.91 +    in
    2.92 +      val case_def = hd case_defs;
    2.93 +      fun case_const T = Const (case_name, caseT T);
    2.94 +      val case_app = list_ccomb (case_const resultT, fs);
    2.95 +      val thy = thy;
    2.96 +    end;
    2.97  
    2.98      (* define syntax for case combinator *)
    2.99      (* TODO: re-implement case syntax using a parse translation *)
   2.100 @@ -441,9 +491,8 @@
   2.101      (* prove strictness of case combinator *)
   2.102      val case_strict =
   2.103        let
   2.104 -        val defs = [case_beta, mk_meta_eq rep_strict];
   2.105 -        val lhs = case_app ` mk_bottom lhsT;
   2.106 -        val goal = mk_trp (mk_eq (lhs, mk_bottom resultT));
   2.107 +        val defs = case_beta :: map mk_meta_eq [rep_strict, @{thm cfcomp2}];
   2.108 +        val goal = mk_trp (mk_strict case_app);
   2.109          val tacs = [resolve_tac @{thms sscase1 ssplit1 strictify1} 1];
   2.110        in prove thy defs goal (K tacs) end;
   2.111          
   2.112 @@ -460,7 +509,8 @@
   2.113            val defs = case_beta :: con_betas;
   2.114            val rules1 = @{thms sscase2 sscase3 ssplit2 fup2 ID1};
   2.115            val rules2 = @{thms con_defined_iff_rules};
   2.116 -          val rules = abs_inverse :: rules1 @ rules2;
   2.117 +          val rules3 = @{thms cfcomp2 one_when2};
   2.118 +          val rules = abs_inverse :: rules1 @ rules2 @ rules3;
   2.119            val tacs = [asm_simp_tac (beta_ss addsimps rules) 1];
   2.120          in prove thy defs goal (K tacs) end;
   2.121      in
   2.122 @@ -961,7 +1011,6 @@
   2.123      (dname : string)
   2.124      (spec : (binding * (bool * binding option * typ) list * mixfix) list)
   2.125      (iso_info : Domain_Isomorphism.iso_info)
   2.126 -    (case_def : thm)
   2.127      (thy : theory) =
   2.128    let
   2.129  
   2.130 @@ -995,7 +1044,7 @@
   2.131          val case_spec = map2 prep_con con_consts spec;
   2.132        in
   2.133          add_case_combinator case_spec lhsT dname
   2.134 -          case_def con_betas casedist iso_locale thy
   2.135 +          con_betas casedist iso_locale rep_const thy
   2.136        end;
   2.137  
   2.138      (* qualify constants and theorems with domain name *)
     3.1 --- a/src/HOLCF/Tools/Domain/domain_syntax.ML	Mon Mar 01 08:33:49 2010 -0800
     3.2 +++ b/src/HOLCF/Tools/Domain/domain_syntax.ML	Mon Mar 01 09:55:32 2010 -0800
     3.3 @@ -43,7 +43,6 @@
     3.4                                             | _ => foldr1 mk_sprodT (map opt_lazy args);
     3.5        fun freetvar s = let val tvar = mk_TFree s in
     3.6                           if tvar mem typevars then freetvar ("t"^s) else tvar end;
     3.7 -      fun when_type (_,args,_) = List.foldr (op ->>) (freetvar "t") (map third args);
     3.8      in
     3.9      val dtype  = Type(dname,typevars);
    3.10      val dtype2 = foldr1 mk_ssumT (map prod cons');
    3.11 @@ -51,7 +50,6 @@
    3.12      fun dbind s = Binding.name (dnam ^ s);
    3.13      val const_rep  = (dbind "_rep" ,              dtype  ->> dtype2, NoSyn);
    3.14      val const_abs  = (dbind "_abs" ,              dtype2 ->> dtype , NoSyn);
    3.15 -    val const_when = (dbind "_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn);
    3.16      val const_copy = (dbind "_copy", dtypeprod ->> dtype  ->> dtype , NoSyn);
    3.17      end;
    3.18  
    3.19 @@ -63,8 +61,7 @@
    3.20      val optional_consts =
    3.21          if definitional then [] else [const_rep, const_abs, const_copy];
    3.22  
    3.23 -  in (optional_consts @ [const_when] @ 
    3.24 -      [const_take, const_finite])
    3.25 +  in (optional_consts @ [const_take, const_finite])
    3.26    end; (* let *)
    3.27  
    3.28  (* ----- putting all the syntax stuff together ------------------------------ *)
     4.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Mar 01 08:33:49 2010 -0800
     4.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Mar 01 09:55:32 2010 -0800
     4.3 @@ -120,7 +120,6 @@
     4.4  in
     4.5    val ax_abs_iso  = ga "abs_iso"  dname;
     4.6    val ax_rep_iso  = ga "rep_iso"  dname;
     4.7 -  val ax_when_def = ga "when_def" dname;
     4.8    val ax_copy_def = ga "copy_def" dname;
     4.9  end; (* local *)
    4.10  
    4.11 @@ -154,7 +153,7 @@
    4.12  
    4.13  val (result, thy) =
    4.14    Domain_Constructors.add_domain_constructors
    4.15 -    (Long_Name.base_name dname) (snd dom_eqn) iso_info ax_when_def thy;
    4.16 +    (Long_Name.base_name dname) (snd dom_eqn) iso_info thy;
    4.17  
    4.18  val con_appls = #con_betas result;
    4.19  val {exhaust, casedist, ...} = result;