ML monad support
authorhaftmann
Tue Sep 25 12:16:14 2007 +0200 (2007-09-25)
changeset 24702f875049a13a1
parent 24701 f8bfd592a6dc
child 24703 0041117b756c
ML monad support
src/Tools/code/code_target.ML
     1.1 --- a/src/Tools/code/code_target.ML	Tue Sep 25 12:16:13 2007 +0200
     1.2 +++ b/src/Tools/code/code_target.ML	Tue Sep 25 12:16:14 2007 +0200
     1.3 @@ -1743,20 +1743,26 @@
     1.4          | NONE => error "Illegal ml_string expression";
     1.5    in (1, pretty) end;
     1.6  
     1.7 -val pretty_imperative_monad_bind =
     1.8 +fun pretty_imperative_monad_bind bind' =
     1.9    let
    1.10 -    fun pretty (pr : CodeName.var_ctxt -> fixity -> iterm -> Pretty.T)
    1.11 -          vars fxy [(t1, _), ((v, ty) `|-> t2, _)] =
    1.12 -            pr vars fxy (ICase (((t1, ty), ([(IVar v, t2)])), IVar ""))
    1.13 -      | pretty pr vars fxy [(t1, _), (t2, ty2)] =
    1.14 +    fun dest_abs ((v, ty) `|-> t, _) = ((v, ty), t)
    1.15 +      | dest_abs (t, ty) =
    1.16            let
    1.17 -            (*this code suffers from the lack of a proper concept for bindings*)
    1.18 -            val vs = CodeThingol.fold_varnames cons t2 [];
    1.19 +            val vs = CodeThingol.fold_varnames cons t [];
    1.20              val v = Name.variant vs "x";
    1.21 -            val vars' = CodeName.intro_vars [v] vars;
    1.22 -            val var = IVar v;
    1.23 -            val ty = (hd o fst o CodeThingol.unfold_fun) ty2;
    1.24 -          in pr vars' fxy (ICase (((t1, ty), ([(var, t2 `$ var)])), IVar "")) end;
    1.25 +            val ty' = (hd o fst o CodeThingol.unfold_fun) ty;
    1.26 +          in ((v, ty'), t `$ IVar v) end;
    1.27 +    fun tr_bind [(t1, _), (t2, ty2)] =
    1.28 +      let
    1.29 +        val ((v, ty), t) = dest_abs (t2, ty2);
    1.30 +      in ICase (((t1, ty), [(IVar v, tr_bind' t)]), IVar "") end
    1.31 +    and tr_bind' (t as _ `$ _) = (case CodeThingol.unfold_app t
    1.32 +         of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if c = bind'
    1.33 +              then tr_bind [(x1, ty1), (x2, ty2)]
    1.34 +              else t
    1.35 +          | _ => t)
    1.36 +      | tr_bind' t = t;
    1.37 +    fun pretty pr vars fxy ts = pr vars fxy (tr_bind ts);
    1.38    in (2, pretty) end;
    1.39  
    1.40  end; (*local*)
    1.41 @@ -2015,12 +2021,8 @@
    1.42    end;
    1.43  
    1.44  fun add_pretty_imperative_monad_bind target bind thy =
    1.45 -  let
    1.46 -    val pr = pretty_imperative_monad_bind
    1.47 -  in
    1.48 -    thy
    1.49 -    |> add_syntax_const target bind (SOME pr)
    1.50 -  end;
    1.51 +  add_syntax_const target bind (SOME (pretty_imperative_monad_bind
    1.52 +    (CodeName.const thy bind))) thy;
    1.53  
    1.54  val add_haskell_monad = gen_add_haskell_monad CodeUnit.read_const;
    1.55