dropping return in imperative monad bindings
authorhaftmann
Mon Apr 28 13:41:04 2008 +0200 (2008-04-28)
changeset 26753094d70c81243
parent 26752 6b276119139b
child 26754 c0424e4de33d
dropping return in imperative monad bindings
src/HOL/Library/Heap_Monad.thy
src/Tools/code/code_target.ML
     1.1 --- a/src/HOL/Library/Heap_Monad.thy	Sun Apr 27 17:13:01 2008 +0200
     1.2 +++ b/src/HOL/Library/Heap_Monad.thy	Mon Apr 28 13:41:04 2008 +0200
     1.3 @@ -299,9 +299,8 @@
     1.4  subsubsection {* SML *}
     1.5  
     1.6  code_type Heap (SML "unit/ ->/ _")
     1.7 -term "op \<guillemotright>="
     1.8  code_const Heap (SML "raise/ (Fail/ \"bare Heap\")")
     1.9 -code_monad run "op \<guillemotright>=" "()" SML
    1.10 +code_monad run "op \<guillemotright>=" return "()" SML
    1.11  code_const run (SML "_")
    1.12  code_const return (SML "(fn/ ()/ =>/ _)")
    1.13  code_const "Heap_Monad.Fail" (SML "Fail")
    1.14 @@ -312,7 +311,7 @@
    1.15  
    1.16  code_type Heap (OCaml "_")
    1.17  code_const Heap (OCaml "failwith/ \"bare Heap\"")
    1.18 -code_monad run "op \<guillemotright>=" "()" OCaml
    1.19 +code_monad run "op \<guillemotright>=" return "()" OCaml
    1.20  code_const run (OCaml "_")
    1.21  code_const return (OCaml "(fn/ ()/ =>/ _)")
    1.22  code_const "Heap_Monad.Fail" (OCaml "Failure")
     2.1 --- a/src/Tools/code/code_target.ML	Sun Apr 27 17:13:01 2008 +0200
     2.2 +++ b/src/Tools/code/code_target.ML	Mon Apr 28 13:41:04 2008 +0200
     2.3 @@ -1855,7 +1855,7 @@
     2.4          | NONE => error "Illegal message expression";
     2.5    in (1, pretty) end;
     2.6  
     2.7 -fun pretty_imperative_monad_bind bind' unit' =
     2.8 +fun pretty_imperative_monad_bind bind' return' unit' =
     2.9    let
    2.10      val dummy_name = "";
    2.11      val dummy_type = ITyVar dummy_name;
    2.12 @@ -1869,16 +1869,18 @@
    2.13              val v = Name.variant vs "x";
    2.14              val ty' = (hd o fst o CodeThingol.unfold_fun) ty;
    2.15            in ((v, ty'), t `$ IVar v) end;
    2.16 +    fun force (t as IConst (c, _) `$ t') = if c = return'
    2.17 +          then t' else t `$ unitt
    2.18 +      | force t = t `$ unitt;
    2.19      fun tr_bind' [(t1, _), (t2, ty2)] =
    2.20        let
    2.21          val ((v, ty), t) = dest_abs (t2, ty2);
    2.22 -      in ICase (((t1 `$ unitt, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end
    2.23 -    and tr_bind'' (t as _ `$ _) = (case CodeThingol.unfold_app t
    2.24 +      in ICase (((force t1, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end
    2.25 +    and tr_bind'' t = case CodeThingol.unfold_app t
    2.26           of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if c = bind'
    2.27                then tr_bind' [(x1, ty1), (x2, ty2)]
    2.28 -              else t `$ unitt
    2.29 -          | _ => t `$ unitt)
    2.30 -      | tr_bind'' t = t `$ unitt;
    2.31 +              else force t
    2.32 +          | _ => force t;
    2.33      fun tr_bind ts = (dummy_name, dummy_type)
    2.34        `|-> ICase (((IVar dummy_name, dummy_type), [(unitt, tr_bind' ts)]), dummy_case_term);
    2.35      fun pretty pr vars fxy ts = pr vars fxy (tr_bind ts);
    2.36 @@ -2009,17 +2011,18 @@
    2.37  fun add_modl_alias target =
    2.38    map_module_alias target o Symtab.update o apsnd CodeName.check_modulename;
    2.39  
    2.40 -fun add_monad target c_run c_bind c_unit thy =
    2.41 +fun add_monad target c_run c_bind c_return_unit thy =
    2.42    let
    2.43      val c_run' = CodeUnit.read_const thy c_run;
    2.44      val c_bind' = CodeUnit.read_const thy c_bind;
    2.45      val c_bind'' = CodeName.const thy c_bind';
    2.46 -    val c_unit'' = Option.map (CodeName.const thy o CodeUnit.read_const thy) c_unit;
    2.47 +    val c_return_unit'' = (Option.map o pairself)
    2.48 +      (CodeName.const thy o CodeUnit.read_const thy) c_return_unit;
    2.49      val is_haskell = target = target_Haskell;
    2.50 -    val _ = if is_haskell andalso is_some c_unit''
    2.51 +    val _ = if is_haskell andalso is_some c_return_unit''
    2.52        then error ("No unit entry may be given for Haskell monad")
    2.53        else ();
    2.54 -    val _ = if not is_haskell andalso is_none c_unit''
    2.55 +    val _ = if not is_haskell andalso is_none c_return_unit''
    2.56        then error ("Unit entry must be given for SML/OCaml monad")
    2.57        else ();
    2.58    in if target = target_Haskell then
    2.59 @@ -2031,7 +2034,8 @@
    2.60    else
    2.61      thy
    2.62      |> gen_add_syntax_const (K I) target c_bind'
    2.63 -          (SOME (pretty_imperative_monad_bind c_bind'' (the c_unit'')))
    2.64 +          (SOME (pretty_imperative_monad_bind c_bind''
    2.65 +            ((fst o the) c_return_unit'') ((snd o the) c_return_unit'')))
    2.66    end;
    2.67  
    2.68  fun gen_allow_exception prep_cs raw_c thy =
    2.69 @@ -2185,10 +2189,10 @@
    2.70  
    2.71  val _ =
    2.72    OuterSyntax.command "code_monad" "define code syntax for monads" K.thy_decl (
    2.73 -    P.term -- P.term -- ((P.term >> SOME) -- Scan.repeat1 P.name
    2.74 +    P.term -- P.term -- ((P.term -- P.term >> SOME) -- Scan.repeat1 P.name
    2.75        || Scan.succeed NONE -- Scan.repeat1 P.name)
    2.76 -    >> (fn ((raw_run, raw_bind), (raw_unit, targets)) => Toplevel.theory 
    2.77 -          (fold (fn target => add_monad target raw_run raw_bind raw_unit) targets))
    2.78 +    >> (fn ((raw_run, raw_bind), (raw_unit_return, targets)) => Toplevel.theory 
    2.79 +          (fold (fn target => add_monad target raw_run raw_bind raw_unit_return) targets))
    2.80    );
    2.81  
    2.82  val _ =