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 _ =