--- 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;