dropped imperative monad bind
authorhaftmann
Wed Jul 30 07:34:00 2008 +0200 (2008-07-30)
changeset 2771029702aa892a5
parent 27709 2ba55d217705
child 27711 5052736b8bcc
dropped imperative monad bind
src/Tools/code/code_target.ML
     1.1 --- a/src/Tools/code/code_target.ML	Wed Jul 30 07:33:59 2008 +0200
     1.2 +++ b/src/Tools/code/code_target.ML	Wed Jul 30 07:34:00 2008 +0200
     1.3 @@ -234,7 +234,7 @@
     1.4      val defined_target = is_some o Symtab.lookup (fst (CodeTargetData.get thy));
     1.5      val _ = case seri
     1.6       of Extends (super, _) => if defined_target super then ()
     1.7 -          else error ("No such target: " ^ quote super)
     1.8 +          else error ("Unknown code target language: " ^ quote super)
     1.9        | _ => ();
    1.10      val _ = if defined_target target
    1.11        then warning ("Overwriting existing target " ^ quote target)
    1.12 @@ -400,7 +400,7 @@
    1.13      vars fxy (app as ((c, (_, tys)), ts)) =
    1.14    case syntax_const c
    1.15     of NONE => if pat andalso not (is_cons c) then
    1.16 -        nerror thm "Non-constructor in pattern "
    1.17 +        nerror thm "Non-constructor in pattern"
    1.18          else brackify fxy (pr_app thm pat vars app)
    1.19      | SOME (i, pr) =>
    1.20          let
    1.21 @@ -411,7 +411,7 @@
    1.22          else if k < length ts
    1.23            then case chop k ts of (ts1, ts2) =>
    1.24              brackify fxy (pr' APP ts1 :: map (pr_term thm pat vars BR) ts2)
    1.25 -          else pr_term thm pat vars fxy (CodeThingol.eta_expand app k)
    1.26 +          else pr_term thm pat vars fxy (CodeThingol.eta_expand k app)
    1.27          end;
    1.28  
    1.29  fun gen_pr_bind pr_bind pr_term thm (fxy : fixity) ((v, pat), ty : itype) vars =
    1.30 @@ -540,7 +540,7 @@
    1.31          (str o deresolve) c :: map (pr_term thm pat vars BR) ts
    1.32        else if k = length ts then
    1.33          [(str o deresolve) c, Pretty.enum "," "(" ")" (map (pr_term thm pat vars NOBR) ts)]
    1.34 -      else [pr_term thm pat vars BR (CodeThingol.eta_expand app k)] end else
    1.35 +      else [pr_term thm pat vars BR (CodeThingol.eta_expand k app)] end else
    1.36          (str o deresolve) c
    1.37            :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts
    1.38      and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons thm pat vars
    1.39 @@ -818,7 +818,7 @@
    1.40            | [t] => [(str o deresolve) c, pr_term thm pat vars BR t]
    1.41            | _ => [(str o deresolve) c, Pretty.enum "," "(" ")"
    1.42                      (map (pr_term thm pat vars NOBR) ts)]
    1.43 -        else [pr_term thm pat vars BR (CodeThingol.eta_expand app (length tys))]
    1.44 +        else [pr_term thm pat vars BR (CodeThingol.eta_expand (length tys) app)]
    1.45        else (str o deresolve) c
    1.46          :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts)
    1.47      and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons thm pat vars
    1.48 @@ -1811,37 +1811,6 @@
    1.49          | NONE => nerror thm "Illegal message expression";
    1.50    in (1, pretty) end;
    1.51  
    1.52 -fun pretty_imperative_monad_bind bind' return' unit' =
    1.53 -  let
    1.54 -    val dummy_name = "";
    1.55 -    val dummy_type = ITyVar dummy_name;
    1.56 -    val dummy_case_term = IVar dummy_name;
    1.57 -    (*assumption: dummy values are not relevant for serialization*)
    1.58 -    val unitt = IConst (unit', ([], []));
    1.59 -    fun dest_abs ((v, ty) `|-> t, _) = ((v, ty), t)
    1.60 -      | dest_abs (t, ty) =
    1.61 -          let
    1.62 -            val vs = CodeThingol.fold_varnames cons t [];
    1.63 -            val v = Name.variant vs "x";
    1.64 -            val ty' = (hd o fst o CodeThingol.unfold_fun) ty;
    1.65 -          in ((v, ty'), t `$ IVar v) end;
    1.66 -    fun force (t as IConst (c, _) `$ t') = if c = return'
    1.67 -          then t' else t `$ unitt
    1.68 -      | force t = t `$ unitt;
    1.69 -    fun tr_bind' [(t1, _), (t2, ty2)] =
    1.70 -      let
    1.71 -        val ((v, ty), t) = dest_abs (t2, ty2);
    1.72 -      in ICase (((force t1, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end
    1.73 -    and tr_bind'' t = case CodeThingol.unfold_app t
    1.74 -         of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if c = bind'
    1.75 -              then tr_bind' [(x1, ty1), (x2, ty2)]
    1.76 -              else force t
    1.77 -          | _ => force t;
    1.78 -    fun tr_bind ts = (dummy_name, dummy_type)
    1.79 -      `|-> ICase (((IVar dummy_name, dummy_type), [(unitt, tr_bind' ts)]), dummy_case_term);
    1.80 -    fun pretty pr thm pat vars fxy ts = pr vars fxy (tr_bind ts);
    1.81 -  in (2, pretty) end;
    1.82 -
    1.83  end; (*local*)
    1.84  
    1.85  
    1.86 @@ -2114,32 +2083,18 @@
    1.87  fun add_module_alias target =
    1.88    map_module_alias target o Symtab.update o apsnd CodeName.check_modulename;
    1.89  
    1.90 -fun add_monad target raw_c_run raw_c_bind raw_c_return_unit thy =
    1.91 +fun add_monad target raw_c_run raw_c_bind thy =
    1.92    let
    1.93      val c_run = CodeUnit.read_const thy raw_c_run;
    1.94      val c_bind = CodeUnit.read_const thy raw_c_bind;
    1.95      val c_bind' = CodeName.const thy c_bind;
    1.96 -    val c_return_unit' = (Option.map o pairself)
    1.97 -      (CodeName.const thy o CodeUnit.read_const thy) raw_c_return_unit;
    1.98 -    val is_haskell = target = target_Haskell;
    1.99 -    val _ = if is_haskell andalso is_some c_return_unit'
   1.100 -      then error ("No unit entry may be given for Haskell monad")
   1.101 -      else ();
   1.102 -    val _ = if not is_haskell andalso is_none c_return_unit'
   1.103 -      then error ("Unit entry must be given for SML/OCaml monad")
   1.104 -      else ();
   1.105    in if target = target_Haskell then
   1.106      thy
   1.107      |> gen_add_syntax_const (K I) target_Haskell c_run
   1.108            (SOME (pretty_haskell_monad c_bind'))
   1.109      |> gen_add_syntax_const (K I) target_Haskell c_bind
   1.110            (simple_const_syntax (SOME (parse_infix fst (L, 1) ">>=")))
   1.111 -  else
   1.112 -    thy
   1.113 -    |> gen_add_syntax_const (K I) target c_bind
   1.114 -          (SOME (pretty_imperative_monad_bind c_bind'
   1.115 -            ((fst o the) c_return_unit') ((snd o the) c_return_unit')))
   1.116 -  end;
   1.117 +  else error "Only Haskell target allows for monad syntax" end;
   1.118  
   1.119  fun gen_allow_abort prep_cs raw_c thy =
   1.120    let
   1.121 @@ -2326,10 +2281,9 @@
   1.122  
   1.123  val _ =
   1.124    OuterSyntax.command "code_monad" "define code syntax for monads" K.thy_decl (
   1.125 -    P.term -- P.term -- ((P.term -- P.term >> SOME) -- Scan.repeat1 P.name
   1.126 -      || Scan.succeed NONE -- Scan.repeat1 P.name)
   1.127 -    >> (fn ((raw_run, raw_bind), (raw_unit_return, targets)) => Toplevel.theory 
   1.128 -          (fold (fn target => add_monad target raw_run raw_bind raw_unit_return) targets))
   1.129 +    P.term -- P.term -- P.name
   1.130 +    >> (fn ((raw_run, raw_bind), target) => Toplevel.theory 
   1.131 +          (add_monad target raw_run raw_bind))
   1.132    );
   1.133  
   1.134  val _ =