combinators for single-threaded operations
authorhaftmann
Fri May 15 16:39:18 2009 +0200 (2009-05-15)
changeset 3118313effe47174c
parent 31182 7ac0a57a57ed
child 31184 6dc73ea0dbc0
combinators for single-threaded operations
src/HOL/Tools/hologic.ML
     1.1 --- a/src/HOL/Tools/hologic.ML	Fri May 15 16:39:18 2009 +0200
     1.2 +++ b/src/HOL/Tools/hologic.ML	Fri May 15 16:39:18 2009 +0200
     1.3 @@ -122,6 +122,8 @@
     1.4    val mk_typerep: typ -> term
     1.5    val mk_term_of: typ -> term -> term
     1.6    val reflect_term: term -> term
     1.7 +  val mk_return: typ -> typ -> term -> term
     1.8 +  val mk_ST: ((term * typ) * (string * typ) option)  list -> term -> typ -> typ option * typ -> term
     1.9  end;
    1.10  
    1.11  structure HOLogic: HOLOGIC =
    1.12 @@ -612,8 +614,23 @@
    1.13    | reflect_term (t1 $ t2) =
    1.14        Const ("Code_Eval.App", termT --> termT --> termT)
    1.15          $ reflect_term t1 $ reflect_term t2
    1.16 -  | reflect_term (t as Free _) = t
    1.17 -  | reflect_term (t as Bound _) = t
    1.18 -  | reflect_term (Abs (v, _, t)) = Abs (v, termT, reflect_term t);
    1.19 +  | reflect_term (Abs (v, _, t)) = Abs (v, termT, reflect_term t)
    1.20 +  | reflect_term t = t;
    1.21 +
    1.22 +
    1.23 +(* open state monads *)
    1.24 +
    1.25 +fun mk_return T U x = pair_const T U $ x;
    1.26 +
    1.27 +fun mk_ST clauses t U (someT, V) =
    1.28 +  let
    1.29 +    val R = case someT of SOME T => mk_prodT (T, V) | NONE => V
    1.30 +    fun mk_clause ((t, U), SOME (v, T)) (t', U') =
    1.31 +          (Const ("Product_Type.scomp", (U --> mk_prodT (T, U')) --> (T --> U' --> R) --> U --> R)
    1.32 +            $ t $ lambda (Free (v, T)) t', U)
    1.33 +      | mk_clause ((t, U), NONE) (t', U') =
    1.34 +          (Const ("Product_Type.fcomp", (U --> U') --> (U' --> R) --> U --> R)
    1.35 +            $ t $ t', U)
    1.36 +  in fold_rev mk_clause clauses (t, U) |> fst end;
    1.37  
    1.38  end;