src/HOL/Fun.thy
changeset 25886 7753e0d81b7a
parent 24286 7619080e49f0
child 26105 ae06618225ec
     1.1 --- a/src/HOL/Fun.thy	Thu Jan 10 19:09:21 2008 +0100
     1.2 +++ b/src/HOL/Fun.thy	Thu Jan 10 19:10:08 2008 +0100
     1.3 @@ -497,6 +497,28 @@
     1.4  
     1.5  subsection {* Code generator setup *}
     1.6  
     1.7 +types_code
     1.8 +  "fun"  ("(_ ->/ _)")
     1.9 +attach (term_of) {*
    1.10 +fun term_of_fun_type _ aT _ bT _ = Free ("<function>", aT --> bT);
    1.11 +*}
    1.12 +attach (test) {*
    1.13 +fun gen_fun_type aF aT bG bT i =
    1.14 +  let
    1.15 +    val tab = ref [];
    1.16 +    fun mk_upd (x, (_, y)) t = Const ("Fun.fun_upd",
    1.17 +      (aT --> bT) --> aT --> bT --> aT --> bT) $ t $ aF x $ y ()
    1.18 +  in
    1.19 +    (fn x =>
    1.20 +       case AList.lookup op = (!tab) x of
    1.21 +         NONE =>
    1.22 +           let val p as (y, _) = bG i
    1.23 +           in (tab := (x, p) :: !tab; y) end
    1.24 +       | SOME (y, _) => y,
    1.25 +     fn () => Basics.fold mk_upd (!tab) (Const ("arbitrary", aT --> bT)))
    1.26 +  end;
    1.27 +*}
    1.28 +
    1.29  code_const "op \<circ>"
    1.30    (SML infixl 5 "o")
    1.31    (Haskell infixr 9 ".")