# HG changeset patch
# User wenzelm
# Date 1570886141 -7200
# Node ID 8e51ea8d460921dae923136648e6c7da1971444c
# Parent  f95a85446a24a91b4cfdb9e0c5dd6881c00bd0a6
adapted to ML version;

diff -r f95a85446a24 -r 8e51ea8d4609 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Sat Oct 12 15:01:13 2019 +0200
+++ b/src/Tools/Haskell/Haskell.thy	Sat Oct 12 15:15:41 2019 +0200
@@ -875,7 +875,7 @@
 -}
 
 module Isabelle.XML.Encode (
-  A, T, V,
+  A, T, V, P,
 
   int_atom, bool_atom, unit_atom,
 
@@ -892,6 +892,7 @@
 type A a = a -> String
 type T a = a -> XML.Body
 type V a = a -> Maybe ([String], XML.Body)
+type P a = a -> [String]
 
 
 -- atomic values
@@ -961,11 +962,11 @@
 -}
 
 module Isabelle.XML.Decode (
-  A, T, V,
+  A, T, V, P,
 
   int_atom, bool_atom, unit_atom,
 
-  tree, properties, string, init, bool, unit, pair, triple, list, variant
+  tree, properties, string, int, bool, unit, pair, triple, list, variant
 )
 where
 
@@ -980,6 +981,7 @@
 type A a = String -> a
 type T a = XML.Body -> a
 type V a = ([String], XML.Body) -> a
+type P a = [String] -> a
 
 err_atom = error "Malformed XML atom"
 err_body = error "Malformed XML body"
@@ -1358,7 +1360,7 @@
 
   Sort, dummyS,
 
-  Typ(..), dummyT, Term(..))
+  Typ(..), dummyT, is_dummyT, Term(..))
 where
 
 type Indexname = (String, Int)
@@ -1379,6 +1381,10 @@
 dummyT :: Typ
 dummyT = Type (\<open>\<^type_name>\<open>dummy\<close>\<close>, [])
 
+is_dummyT :: Typ -> Bool
+is_dummyT (Type (\<open>\<^type_name>\<open>dummy\<close>\<close>, [])) = True
+is_dummyT _ = False
+
 
 data Term =
     Const (String, [Typ])
@@ -1402,7 +1408,7 @@
 
 {-# LANGUAGE LambdaCase #-}
 
-module Isabelle.Term_XML.Encode (sort, typ, term)
+module Isabelle.Term_XML.Encode (indexname, sort, typ, typ_body, term)
 where
 
 import Isabelle.Library
@@ -1410,6 +1416,8 @@
 import Isabelle.XML.Encode
 import Isabelle.Term
 
+indexname :: P Indexname
+indexname (a, b) = if b == 0 then [a] else [a, int_atom b]
 
 sort :: T Sort
 sort = list string
@@ -1419,15 +1427,18 @@
   ty |> variant
    [\case { Type (a, b) -> Just ([a], list typ b); _ -> Nothing },
     \case { TFree (a, b) -> Just ([a], sort b); _ -> Nothing },
-    \case { TVar ((a, b), c) -> Just ([a, int_atom b], sort c); _ -> Nothing }]
+    \case { TVar (a, b) -> Just (indexname a, sort b); _ -> Nothing }]
+
+typ_body :: T Typ
+typ_body ty = if is_dummyT ty then [] else typ ty
 
 term :: T Term
 term t =
   t |> variant
    [\case { Const (a, b) -> Just ([a], list typ b); _ -> Nothing },
-    \case { Free (a, b) -> Just ([a], typ b); _ -> Nothing },
-    \case { Var ((a, b), c) -> Just ([a, int_atom b], typ c); _ -> Nothing },
-    \case { Bound a -> Just ([int_atom a], []); _ -> Nothing },
+    \case { Free (a, b) -> Just ([a], typ_body b); _ -> Nothing },
+    \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 }]
 \<close>
@@ -1442,7 +1453,7 @@
 See also \<^file>\<open>$ISABELLE_HOME/src/Pure/term_xml.ML\<close>.
 -}
 
-module Isabelle.Term_XML.Decode (sort, typ, term)
+module Isabelle.Term_XML.Decode (indexname, sort, typ, typ_body, term)
 where
 
 import Isabelle.Library
@@ -1451,6 +1462,10 @@
 import Isabelle.Term
 
 
+indexname :: P Indexname
+indexname [a] = (a, 0)
+indexname [a, b] = (a, int_atom b)
+
 sort :: T Sort
 sort = list string
 
@@ -1459,15 +1474,19 @@
   ty |> variant
   [\([a], b) -> Type (a, list typ b),
    \([a], b) -> TFree (a, sort b),
-   \([a, b], c) -> TVar ((a, int_atom b), sort c)]
+   \(a, b) -> TVar (indexname a, sort b)]
+
+typ_body :: T Typ
+typ_body [] = dummyT
+typ_body body = typ body
 
 term :: T Term
 term t =
   t |> variant
    [\([a], b) -> Const (a, list typ b),
-    \([a], b) -> Free (a, typ b),
-    \([a, b], c) -> Var ((a, int_atom b), typ c),
-    \([a], []) -> Bound (int_atom a),
+    \([a], b) -> Free (a, typ_body b),
+    \(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)]
 \<close>