--- a/src/Tools/Haskell/Haskell.thy Wed Aug 25 17:46:53 2021 +0200
+++ b/src/Tools/Haskell/Haskell.thy Wed Aug 25 22:16:27 2021 +0200
@@ -2229,7 +2229,7 @@
module Isabelle.Term (
Indexname, Sort, Typ(..), Term(..),
Free, lambda, declare_frees, incr_boundvars, subst_bound, dest_abs, strip_abs,
- type_op0, type_op1, op0, op1, op2, typed_op1, typed_op2, binder,
+ type_op0, type_op1, op0, op1, op2, typed_op0, typed_op1, typed_op2, binder,
dummyS, dummyT, is_dummyT, propT, is_propT, (-->), dest_funT, (--->),
aconv, list_comb, strip_comb, head_of
)
@@ -2363,6 +2363,13 @@
dest (App (App (Const (c, _), t), u)) | c == name = Just (t, u)
dest _ = Nothing
+typed_op0 :: Name -> (Typ -> Term, Term -> Maybe Typ)
+typed_op0 name = (mk, dest)
+ where
+ mk ty = Const (name, [ty])
+ dest (Const (c, [ty])) | c == name = Just ty
+ dest _ = Nothing
+
typed_op1 :: Name -> (Typ -> Term -> Term, Term -> Maybe (Typ, Term))
typed_op1 name = (mk, dest)
where
@@ -2479,7 +2486,8 @@
mk_not, dest_not, mk_conj, dest_conj, mk_disj, dest_disj,
mk_imp, dest_imp, mk_iff, dest_iff,
mk_all_op, dest_all_op, mk_ex_op, dest_ex_op,
- mk_all, dest_all, mk_ex, dest_ex
+ mk_all, dest_all, mk_ex, dest_ex,
+ mk_undefined, dest_undefined
)
where
@@ -2540,6 +2548,9 @@
mk_ex :: Free -> Term -> Term; dest_ex :: Name.Context -> Term -> Maybe (Free, Term)
(mk_ex, dest_ex) = binder \<open>\<^const_name>\<open>Ex\<close>\<close>
+
+mk_undefined :: Typ -> Term; dest_undefined :: Term -> Maybe Typ
+(mk_undefined, dest_undefined) = typed_op0 \<open>\<^const_name>\<open>undefined\<close>\<close>
\<close>
generate_file "Isabelle/Term_XML/Encode.hs" = \<open>