clarified Isabelle/Haskell type Term, following Isabelle/Scala (see 446b887e23c7);
authorwenzelm
Sun, 14 Jul 2024 18:10:06 +0200
changeset 80568 fbb655bf62d4
parent 80567 b2c14b489e60
child 80570 4d4f107a778f
child 80579 69cf3c308d6c
clarified Isabelle/Haskell type Term, following Isabelle/Scala (see 446b887e23c7);
src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Sun Jul 14 17:56:54 2024 +0200
+++ b/src/Tools/Haskell/Haskell.thy	Sun Jul 14 18:10:06 2024 +0200
@@ -2347,6 +2347,7 @@
   | Bound Int
   | Abs (Name, Typ, Term)
   | App (Term, Term)
+  | OFCLASS (Typ, Name)
   deriving (Show, Eq, Ord)
 
 
@@ -2681,7 +2682,8 @@
     \case { Var (a, b) -> Just (indexname a, typ_body b); _ -> Nothing },
     \case { Bound a -> Just ([], int a); _ -> Nothing },
     \case { Abs (a, b, c) -> Just ([a], pair typ term (b, c)); _ -> Nothing },
-    \case { App a -> Just ([], pair term term a); _ -> Nothing }]
+    \case { App a -> Just ([], pair term term a); _ -> Nothing },
+    \case { OFCLASS (a, b) -> Just ([b], typ a); _ -> Nothing }]
 \<close>
 
 generate_file "Isabelle/Term_XML/Decode.hs" = \<open>
@@ -2730,7 +2732,8 @@
     \(a, b) -> Var (indexname a, typ_body b),
     \([], a) -> Bound (int a),
     \([a], b) -> let (c, d) = pair typ term b in Abs (a, c, d),
-    \([], a) -> App (pair term term a)]
+    \([], a) -> App (pair term term a),
+    \([a], b) -> OFCLASS (typ b, a)]
 \<close>
 
 generate_file "Isabelle/XML/Classes.hs" = \<open>