# HG changeset patch # User haftmann # Date 1209309181 -7200 # Node ID 6b276119139be2e32566b073d7a0c7a830bcc516 # Parent 2b97ea3130c291a603fcbd95c54bc566ecb7c7e6 corrected ML semantics diff -r 2b97ea3130c2 -r 6b276119139b src/HOL/Library/Array.thy --- a/src/HOL/Library/Array.thy Sat Apr 26 13:20:16 2008 +0200 +++ b/src/HOL/Library/Array.thy Sun Apr 27 17:13:01 2008 +0200 @@ -171,12 +171,12 @@ code_type array (SML "_/ array") code_const Array (SML "raise/ (Fail/ \"bare Array\")") -code_const Array.new' (SML "Array.array ((_), (_))") -code_const Array.of_list (SML "Array.fromList") -code_const Array.make' (SML "Array.tabulate ((_), (_))") -code_const Array.length' (SML "Array.length") -code_const Array.nth' (SML "Array.sub ((_), (_))") -code_const Array.upd' (SML "Array.update ((_), (_), (_))") +code_const Array.new' (SML "(fn/ ()/ =>/ Array.array/ ((_),/ (_)))") +code_const Array.of_list (SML "(fn/ ()/ =>/ Array.fromList/ _)") +code_const Array.make' (SML "(fn/ ()/ =>/ Array.tabulate/ ((_),/ (_)))") +code_const Array.length' (SML "(fn/ ()/ =>/ Array.length/ _)") +code_const Array.nth' (SML "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))") +code_const Array.upd' (SML "(fn/ ()/ =>/ Array.update/ ((_),/ (_),/ (_)))") code_reserved SML Array @@ -185,12 +185,12 @@ code_type array (OCaml "_/ array") code_const Array (OCaml "failwith/ \"bare Array\"") -code_const Array.new' (OCaml "Array.make") -code_const Array.of_list (OCaml "Array.of_list") -code_const Array.make' (OCaml "Array.init") -code_const Array.length' (OCaml "Array.length") -code_const Array.nth' (OCaml "Array.get") -code_const Array.upd' (OCaml "Array.set") +code_const Array.new' (OCaml "(fn/ ()/ =>/ Array.make/ _/ _)") +code_const Array.of_list (OCaml "(fn/ ()/ =>/ Array.of'_list/ _)") +code_const Array.make' (OCaml "(fn/ ()/ =>/ Array.init/ _/ _)") +code_const Array.length' (OCaml "(fn/ ()/ =>/ Array.length/ _)") +code_const Array.nth' (OCaml "(fn/ ()/ =>/ Array.get/ _/ _)") +code_const Array.upd' (OCaml "(fn/ ()/ =>/ Array.set/ _/ _/ _)") code_reserved OCaml Array @@ -205,5 +205,4 @@ code_const Array.nth' (Haskell "readArray") code_const Array.upd' (Haskell "writeArray") - end diff -r 2b97ea3130c2 -r 6b276119139b src/HOL/Library/Heap_Monad.thy --- a/src/HOL/Library/Heap_Monad.thy Sat Apr 26 13:20:16 2008 +0200 +++ b/src/HOL/Library/Heap_Monad.thy Sun Apr 27 17:13:01 2008 +0200 @@ -298,24 +298,25 @@ subsubsection {* SML *} -code_type Heap (SML "_") +code_type Heap (SML "unit/ ->/ _") +term "op \=" code_const Heap (SML "raise/ (Fail/ \"bare Heap\")") -code_monad run "op \=" SML +code_monad run "op \=" "()" SML code_const run (SML "_") -code_const return (SML "_") +code_const return (SML "(fn/ ()/ =>/ _)") code_const "Heap_Monad.Fail" (SML "Fail") -code_const "Heap_Monad.raise_exc" (SML "raise") +code_const "Heap_Monad.raise_exc" (SML "(fn/ ()/ =>/ raise/ _)") subsubsection {* OCaml *} code_type Heap (OCaml "_") code_const Heap (OCaml "failwith/ \"bare Heap\"") -code_monad run "op \=" OCaml +code_monad run "op \=" "()" OCaml code_const run (OCaml "_") -code_const return (OCaml "_") +code_const return (OCaml "(fn/ ()/ =>/ _)") code_const "Heap_Monad.Fail" (OCaml "Failure") -code_const "Heap_Monad.raise_exc" (OCaml "raise") +code_const "Heap_Monad.raise_exc" (OCaml "(fn/ ()/ =>/ raise/ _)") code_reserved OCaml Failure raise @@ -366,7 +367,7 @@ code_type Heap (Haskell "ST '_s _") code_const Heap (Haskell "error \"bare Heap\")") code_const evaluate (Haskell "runST") -code_monad run bindM Haskell +code_monad run "op \=" Haskell code_const return (Haskell "return") code_const "Heap_Monad.Fail" (Haskell "_") code_const "Heap_Monad.raise_exc" (Haskell "error") diff -r 2b97ea3130c2 -r 6b276119139b src/HOL/Library/Ref.thy --- a/src/HOL/Library/Ref.thy Sat Apr 26 13:20:16 2008 +0200 +++ b/src/HOL/Library/Ref.thy Sun Apr 27 17:13:01 2008 +0200 @@ -62,9 +62,9 @@ code_type ref (SML "_/ ref") code_const Ref (SML "raise/ (Fail/ \"bare Ref\")") -code_const Ref.new (SML "ref") -code_const Ref.lookup (SML "'!") -code_const Ref.update (SML infixl 3 ":=") +code_const Ref.new (SML "(fn/ ()/ =>/ ref/ _)") +code_const Ref.lookup (SML "(fn/ ()/ =>/ !/ _)") +code_const Ref.update (SML "(fn/ ()/ =>/ _/ :=/ _)") code_reserved SML ref @@ -72,10 +72,10 @@ subsubsection {* OCaml *} code_type ref (OCaml "_/ ref") -code_const Ref (OCaml "failwith/ \"bare Ref\"") -code_const Ref.new (OCaml "ref") -code_const Ref.lookup (OCaml "'!") -code_const Ref.update (OCaml infixr 1 ":=") +code_const Ref (OCaml "failwith/ \"bare Ref\")") +code_const Ref.new (OCaml "(fn/ ()/ =>/ ref/ _)") +code_const Ref.lookup (OCaml "(fn/ ()/ =>/ !/ _)") +code_const Ref.update (OCaml "(fn/ ()/ =>/ _/ :=/ _)") code_reserved OCaml ref diff -r 2b97ea3130c2 -r 6b276119139b src/Tools/code/code_target.ML --- a/src/Tools/code/code_target.ML Sat Apr 26 13:20:16 2008 +0200 +++ b/src/Tools/code/code_target.ML Sun Apr 27 17:13:01 2008 +0200 @@ -1855,8 +1855,13 @@ | NONE => error "Illegal message expression"; in (1, pretty) end; -fun pretty_imperative_monad_bind bind' = +fun pretty_imperative_monad_bind bind' unit' = let + val dummy_name = ""; + val dummy_type = ITyVar dummy_name; + val dummy_case_term = IVar dummy_name; + (*assumption: dummy values are not relevant for serialization*) + val unitt = IConst (unit', ([], [])); fun dest_abs ((v, ty) `|-> t, _) = ((v, ty), t) | dest_abs (t, ty) = let @@ -1864,16 +1869,18 @@ val v = Name.variant vs "x"; val ty' = (hd o fst o CodeThingol.unfold_fun) ty; in ((v, ty'), t `$ IVar v) end; - fun tr_bind [(t1, _), (t2, ty2)] = + fun tr_bind' [(t1, _), (t2, ty2)] = let val ((v, ty), t) = dest_abs (t2, ty2); - in ICase (((t1, ty), [(IVar v, tr_bind' t)]), IVar "") end - and tr_bind' (t as _ `$ _) = (case CodeThingol.unfold_app t + in ICase (((t1 `$ unitt, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end + and tr_bind'' (t as _ `$ _) = (case CodeThingol.unfold_app t of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if c = bind' - then tr_bind [(x1, ty1), (x2, ty2)] - else t - | _ => t) - | tr_bind' t = t; + then tr_bind' [(x1, ty1), (x2, ty2)] + else t `$ unitt + | _ => t `$ unitt) + | tr_bind'' t = t `$ unitt; + fun tr_bind ts = (dummy_name, dummy_type) + `|-> ICase (((IVar dummy_name, dummy_type), [(unitt, tr_bind' ts)]), dummy_case_term); fun pretty pr vars fxy ts = pr vars fxy (tr_bind ts); in (2, pretty) end; @@ -2002,11 +2009,19 @@ fun add_modl_alias target = map_module_alias target o Symtab.update o apsnd CodeName.check_modulename; -fun add_monad target c_run c_bind thy = +fun add_monad target c_run c_bind c_unit thy = let val c_run' = CodeUnit.read_const thy c_run; val c_bind' = CodeUnit.read_const thy c_bind; val c_bind'' = CodeName.const thy c_bind'; + val c_unit'' = Option.map (CodeName.const thy o CodeUnit.read_const thy) c_unit; + val is_haskell = target = target_Haskell; + val _ = if is_haskell andalso is_some c_unit'' + then error ("No unit entry may be given for Haskell monad") + else (); + val _ = if not is_haskell andalso is_none c_unit'' + then error ("Unit entry must be given for SML/OCaml monad") + else (); in if target = target_Haskell then thy |> gen_add_syntax_const (K I) target_Haskell c_run' @@ -2016,7 +2031,7 @@ else thy |> gen_add_syntax_const (K I) target c_bind' - (SOME (pretty_imperative_monad_bind c_bind'')) + (SOME (pretty_imperative_monad_bind c_bind'' (the c_unit''))) end; fun gen_allow_exception prep_cs raw_c thy = @@ -2170,9 +2185,10 @@ val _ = OuterSyntax.command "code_monad" "define code syntax for monads" K.thy_decl ( - P.term -- P.term -- Scan.repeat1 P.name - >> (fn ((raw_run, raw_bind), targets) => Toplevel.theory - (fold (fn target => add_monad target raw_run raw_bind) targets)) + P.term -- P.term -- ((P.term >> SOME) -- Scan.repeat1 P.name + || Scan.succeed NONE -- Scan.repeat1 P.name) + >> (fn ((raw_run, raw_bind), (raw_unit, targets)) => Toplevel.theory + (fold (fn target => add_monad target raw_run raw_bind raw_unit) targets)) ); val _ =