src/HOLCF/Tools/Domain/domain_axioms.ML
changeset 35462 f5461b02d754
parent 35460 8cb42aa19358
child 35463 b20501588930
equal deleted inserted replaced
35461:34360a1e3537 35462:f5461b02d754
    75       let fun r i = proj (Bound 0) eqs i;
    75       let fun r i = proj (Bound 0) eqs i;
    76       in
    76       in
    77         ("copy_def", %%:(dname^"_copy") == /\ "f"
    77         ("copy_def", %%:(dname^"_copy") == /\ "f"
    78           (dc_abs oo (copy_of_dtyp map_tab r (dtyp_of_eq eqn)) oo dc_rep))
    78           (dc_abs oo (copy_of_dtyp map_tab r (dtyp_of_eq eqn)) oo dc_rep))
    79       end;
    79       end;
    80 
       
    81     val mat_defs =
       
    82       let
       
    83         fun mdef (con, _, _) =
       
    84           let
       
    85             val k = Bound 0
       
    86             val x = Bound 1
       
    87             fun one_con (con', _, args') =
       
    88                 if con'=con then k else List.foldr /\# mk_fail args'
       
    89             val w = list_ccomb(%%:(dname^"_when"), map one_con cons)
       
    90             val rhs = /\ "x" (/\ "k" (w ` x))
       
    91           in (mat_name con ^"_def", %%:(mat_name con) == rhs) end
       
    92       in map mdef cons end;
       
    93 
    80 
    94     val pat_defs =
    81     val pat_defs =
    95       let
    82       let
    96         fun pdef (con, _, args) =
    83         fun pdef (con, _, args) =
    97           let
    84           let
   123                    mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
   110                    mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
   124 
   111 
   125   in (dnam,
   112   in (dnam,
   126       (if definitional then [] else [abs_iso_ax, rep_iso_ax, reach_ax]),
   113       (if definitional then [] else [abs_iso_ax, rep_iso_ax, reach_ax]),
   127       (if definitional then [when_def] else [when_def, copy_def]) @
   114       (if definitional then [when_def] else [when_def, copy_def]) @
   128       mat_defs @ pat_defs @
   115       pat_defs @
   129       [take_def, finite_def])
   116       [take_def, finite_def])
   130   end; (* let (calc_axioms) *)
   117   end; (* let (calc_axioms) *)
   131 
   118 
   132 
   119 
   133 (* legacy type inference *)
   120 (* legacy type inference *)