# HG changeset patch
# User haftmann
# Date 1242398358 -7200
# Node ID 13effe47174cfd636d2664cc6c4b1def4cfdf5a4
# Parent  7ac0a57a57ed443e476f677a327d7f1a88525349
combinators for single-threaded operations

diff -r 7ac0a57a57ed -r 13effe47174c src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Fri May 15 16:39:18 2009 +0200
+++ b/src/HOL/Tools/hologic.ML	Fri May 15 16:39:18 2009 +0200
@@ -122,6 +122,8 @@
   val mk_typerep: typ -> term
   val mk_term_of: typ -> term -> term
   val reflect_term: term -> term
+  val mk_return: typ -> typ -> term -> term
+  val mk_ST: ((term * typ) * (string * typ) option)  list -> term -> typ -> typ option * typ -> term
 end;
 
 structure HOLogic: HOLOGIC =
@@ -612,8 +614,23 @@
   | reflect_term (t1 $ t2) =
       Const ("Code_Eval.App", termT --> termT --> termT)
         $ reflect_term t1 $ reflect_term t2
-  | reflect_term (t as Free _) = t
-  | reflect_term (t as Bound _) = t
-  | reflect_term (Abs (v, _, t)) = Abs (v, termT, reflect_term t);
+  | reflect_term (Abs (v, _, t)) = Abs (v, termT, reflect_term t)
+  | reflect_term t = t;
+
+
+(* open state monads *)
+
+fun mk_return T U x = pair_const T U $ x;
+
+fun mk_ST clauses t U (someT, V) =
+  let
+    val R = case someT of SOME T => mk_prodT (T, V) | NONE => V
+    fun mk_clause ((t, U), SOME (v, T)) (t', U') =
+          (Const ("Product_Type.scomp", (U --> mk_prodT (T, U')) --> (T --> U' --> R) --> U --> R)
+            $ t $ lambda (Free (v, T)) t', U)
+      | mk_clause ((t, U), NONE) (t', U') =
+          (Const ("Product_Type.fcomp", (U --> U') --> (U' --> R) --> U --> R)
+            $ t $ t', U)
+  in fold_rev mk_clause clauses (t, U) |> fst end;
 
 end;