corrected ML semantics
authorhaftmann
Sun Apr 27 17:13:01 2008 +0200 (2008-04-27)
changeset 267526b276119139b
parent 26751 2b97ea3130c2
child 26753 094d70c81243
corrected ML semantics
src/HOL/Library/Array.thy
src/HOL/Library/Heap_Monad.thy
src/HOL/Library/Ref.thy
src/Tools/code/code_target.ML
     1.1 --- a/src/HOL/Library/Array.thy	Sat Apr 26 13:20:16 2008 +0200
     1.2 +++ b/src/HOL/Library/Array.thy	Sun Apr 27 17:13:01 2008 +0200
     1.3 @@ -171,12 +171,12 @@
     1.4  
     1.5  code_type array (SML "_/ array")
     1.6  code_const Array (SML "raise/ (Fail/ \"bare Array\")")
     1.7 -code_const Array.new' (SML "Array.array ((_), (_))")
     1.8 -code_const Array.of_list (SML "Array.fromList")
     1.9 -code_const Array.make' (SML "Array.tabulate ((_), (_))")
    1.10 -code_const Array.length' (SML "Array.length")
    1.11 -code_const Array.nth' (SML "Array.sub ((_), (_))")
    1.12 -code_const Array.upd' (SML "Array.update ((_), (_), (_))")
    1.13 +code_const Array.new' (SML "(fn/ ()/ =>/ Array.array/ ((_),/ (_)))")
    1.14 +code_const Array.of_list (SML "(fn/ ()/ =>/ Array.fromList/ _)")
    1.15 +code_const Array.make' (SML "(fn/ ()/ =>/ Array.tabulate/ ((_),/ (_)))")
    1.16 +code_const Array.length' (SML "(fn/ ()/ =>/ Array.length/ _)")
    1.17 +code_const Array.nth' (SML "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))")
    1.18 +code_const Array.upd' (SML "(fn/ ()/ =>/ Array.update/ ((_),/ (_),/ (_)))")
    1.19  
    1.20  code_reserved SML Array
    1.21  
    1.22 @@ -185,12 +185,12 @@
    1.23  
    1.24  code_type array (OCaml "_/ array")
    1.25  code_const Array (OCaml "failwith/ \"bare Array\"")
    1.26 -code_const Array.new' (OCaml "Array.make")
    1.27 -code_const Array.of_list (OCaml "Array.of_list")
    1.28 -code_const Array.make' (OCaml "Array.init")
    1.29 -code_const Array.length' (OCaml "Array.length")
    1.30 -code_const Array.nth' (OCaml "Array.get")
    1.31 -code_const Array.upd' (OCaml "Array.set")
    1.32 +code_const Array.new' (OCaml "(fn/ ()/ =>/ Array.make/ _/ _)")
    1.33 +code_const Array.of_list (OCaml "(fn/ ()/ =>/ Array.of'_list/ _)")
    1.34 +code_const Array.make' (OCaml "(fn/ ()/ =>/ Array.init/ _/ _)")
    1.35 +code_const Array.length' (OCaml "(fn/ ()/ =>/ Array.length/ _)")
    1.36 +code_const Array.nth' (OCaml "(fn/ ()/ =>/ Array.get/ _/ _)")
    1.37 +code_const Array.upd' (OCaml "(fn/ ()/ =>/ Array.set/ _/ _/ _)")
    1.38  
    1.39  code_reserved OCaml Array
    1.40  
    1.41 @@ -205,5 +205,4 @@
    1.42  code_const Array.nth' (Haskell "readArray")
    1.43  code_const Array.upd' (Haskell "writeArray")
    1.44  
    1.45 -
    1.46  end
     2.1 --- a/src/HOL/Library/Heap_Monad.thy	Sat Apr 26 13:20:16 2008 +0200
     2.2 +++ b/src/HOL/Library/Heap_Monad.thy	Sun Apr 27 17:13:01 2008 +0200
     2.3 @@ -298,24 +298,25 @@
     2.4  
     2.5  subsubsection {* SML *}
     2.6  
     2.7 -code_type Heap (SML "_")
     2.8 +code_type Heap (SML "unit/ ->/ _")
     2.9 +term "op \<guillemotright>="
    2.10  code_const Heap (SML "raise/ (Fail/ \"bare Heap\")")
    2.11 -code_monad run "op \<guillemotright>=" SML
    2.12 +code_monad run "op \<guillemotright>=" "()" SML
    2.13  code_const run (SML "_")
    2.14 -code_const return (SML "_")
    2.15 +code_const return (SML "(fn/ ()/ =>/ _)")
    2.16  code_const "Heap_Monad.Fail" (SML "Fail")
    2.17 -code_const "Heap_Monad.raise_exc" (SML "raise")
    2.18 +code_const "Heap_Monad.raise_exc" (SML "(fn/ ()/ =>/ raise/ _)")
    2.19  
    2.20  
    2.21  subsubsection {* OCaml *}
    2.22  
    2.23  code_type Heap (OCaml "_")
    2.24  code_const Heap (OCaml "failwith/ \"bare Heap\"")
    2.25 -code_monad run "op \<guillemotright>=" OCaml
    2.26 +code_monad run "op \<guillemotright>=" "()" OCaml
    2.27  code_const run (OCaml "_")
    2.28 -code_const return (OCaml "_")
    2.29 +code_const return (OCaml "(fn/ ()/ =>/ _)")
    2.30  code_const "Heap_Monad.Fail" (OCaml "Failure")
    2.31 -code_const "Heap_Monad.raise_exc" (OCaml "raise")
    2.32 +code_const "Heap_Monad.raise_exc" (OCaml "(fn/ ()/ =>/ raise/ _)")
    2.33  
    2.34  code_reserved OCaml Failure raise
    2.35  
    2.36 @@ -366,7 +367,7 @@
    2.37  code_type Heap (Haskell "ST '_s _")
    2.38  code_const Heap (Haskell "error \"bare Heap\")")
    2.39  code_const evaluate (Haskell "runST")
    2.40 -code_monad run bindM Haskell
    2.41 +code_monad run "op \<guillemotright>=" Haskell
    2.42  code_const return (Haskell "return")
    2.43  code_const "Heap_Monad.Fail" (Haskell "_")
    2.44  code_const "Heap_Monad.raise_exc" (Haskell "error")
     3.1 --- a/src/HOL/Library/Ref.thy	Sat Apr 26 13:20:16 2008 +0200
     3.2 +++ b/src/HOL/Library/Ref.thy	Sun Apr 27 17:13:01 2008 +0200
     3.3 @@ -62,9 +62,9 @@
     3.4  
     3.5  code_type ref (SML "_/ ref")
     3.6  code_const Ref (SML "raise/ (Fail/ \"bare Ref\")")
     3.7 -code_const Ref.new (SML "ref")
     3.8 -code_const Ref.lookup (SML "'!")
     3.9 -code_const Ref.update (SML infixl 3 ":=")
    3.10 +code_const Ref.new (SML "(fn/ ()/ =>/ ref/ _)")
    3.11 +code_const Ref.lookup (SML "(fn/ ()/ =>/ !/ _)")
    3.12 +code_const Ref.update (SML "(fn/ ()/ =>/ _/ :=/ _)")
    3.13  
    3.14  code_reserved SML ref
    3.15  
    3.16 @@ -72,10 +72,10 @@
    3.17  subsubsection {* OCaml *}
    3.18  
    3.19  code_type ref (OCaml "_/ ref")
    3.20 -code_const Ref (OCaml "failwith/ \"bare Ref\"")
    3.21 -code_const Ref.new (OCaml "ref")
    3.22 -code_const Ref.lookup (OCaml "'!")
    3.23 -code_const Ref.update (OCaml infixr 1 ":=")
    3.24 +code_const Ref (OCaml "failwith/ \"bare Ref\")")
    3.25 +code_const Ref.new (OCaml "(fn/ ()/ =>/ ref/ _)")
    3.26 +code_const Ref.lookup (OCaml "(fn/ ()/ =>/ !/ _)")
    3.27 +code_const Ref.update (OCaml "(fn/ ()/ =>/ _/ :=/ _)")
    3.28  
    3.29  code_reserved OCaml ref
    3.30  
     4.1 --- a/src/Tools/code/code_target.ML	Sat Apr 26 13:20:16 2008 +0200
     4.2 +++ b/src/Tools/code/code_target.ML	Sun Apr 27 17:13:01 2008 +0200
     4.3 @@ -1855,8 +1855,13 @@
     4.4          | NONE => error "Illegal message expression";
     4.5    in (1, pretty) end;
     4.6  
     4.7 -fun pretty_imperative_monad_bind bind' =
     4.8 +fun pretty_imperative_monad_bind bind' unit' =
     4.9    let
    4.10 +    val dummy_name = "";
    4.11 +    val dummy_type = ITyVar dummy_name;
    4.12 +    val dummy_case_term = IVar dummy_name;
    4.13 +    (*assumption: dummy values are not relevant for serialization*)
    4.14 +    val unitt = IConst (unit', ([], []));
    4.15      fun dest_abs ((v, ty) `|-> t, _) = ((v, ty), t)
    4.16        | dest_abs (t, ty) =
    4.17            let
    4.18 @@ -1864,16 +1869,18 @@
    4.19              val v = Name.variant vs "x";
    4.20              val ty' = (hd o fst o CodeThingol.unfold_fun) ty;
    4.21            in ((v, ty'), t `$ IVar v) end;
    4.22 -    fun tr_bind [(t1, _), (t2, ty2)] =
    4.23 +    fun tr_bind' [(t1, _), (t2, ty2)] =
    4.24        let
    4.25          val ((v, ty), t) = dest_abs (t2, ty2);
    4.26 -      in ICase (((t1, ty), [(IVar v, tr_bind' t)]), IVar "") end
    4.27 -    and tr_bind' (t as _ `$ _) = (case CodeThingol.unfold_app t
    4.28 +      in ICase (((t1 `$ unitt, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end
    4.29 +    and tr_bind'' (t as _ `$ _) = (case CodeThingol.unfold_app t
    4.30           of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if c = bind'
    4.31 -              then tr_bind [(x1, ty1), (x2, ty2)]
    4.32 -              else t
    4.33 -          | _ => t)
    4.34 -      | tr_bind' t = t;
    4.35 +              then tr_bind' [(x1, ty1), (x2, ty2)]
    4.36 +              else t `$ unitt
    4.37 +          | _ => t `$ unitt)
    4.38 +      | tr_bind'' t = t `$ unitt;
    4.39 +    fun tr_bind ts = (dummy_name, dummy_type)
    4.40 +      `|-> ICase (((IVar dummy_name, dummy_type), [(unitt, tr_bind' ts)]), dummy_case_term);
    4.41      fun pretty pr vars fxy ts = pr vars fxy (tr_bind ts);
    4.42    in (2, pretty) end;
    4.43  
    4.44 @@ -2002,11 +2009,19 @@
    4.45  fun add_modl_alias target =
    4.46    map_module_alias target o Symtab.update o apsnd CodeName.check_modulename;
    4.47  
    4.48 -fun add_monad target c_run c_bind thy =
    4.49 +fun add_monad target c_run c_bind c_unit thy =
    4.50    let
    4.51      val c_run' = CodeUnit.read_const thy c_run;
    4.52      val c_bind' = CodeUnit.read_const thy c_bind;
    4.53      val c_bind'' = CodeName.const thy c_bind';
    4.54 +    val c_unit'' = Option.map (CodeName.const thy o CodeUnit.read_const thy) c_unit;
    4.55 +    val is_haskell = target = target_Haskell;
    4.56 +    val _ = if is_haskell andalso is_some c_unit''
    4.57 +      then error ("No unit entry may be given for Haskell monad")
    4.58 +      else ();
    4.59 +    val _ = if not is_haskell andalso is_none c_unit''
    4.60 +      then error ("Unit entry must be given for SML/OCaml monad")
    4.61 +      else ();
    4.62    in if target = target_Haskell then
    4.63      thy
    4.64      |> gen_add_syntax_const (K I) target_Haskell c_run'
    4.65 @@ -2016,7 +2031,7 @@
    4.66    else
    4.67      thy
    4.68      |> gen_add_syntax_const (K I) target c_bind'
    4.69 -          (SOME (pretty_imperative_monad_bind c_bind''))
    4.70 +          (SOME (pretty_imperative_monad_bind c_bind'' (the c_unit'')))
    4.71    end;
    4.72  
    4.73  fun gen_allow_exception prep_cs raw_c thy =
    4.74 @@ -2170,9 +2185,10 @@
    4.75  
    4.76  val _ =
    4.77    OuterSyntax.command "code_monad" "define code syntax for monads" K.thy_decl (
    4.78 -    P.term -- P.term -- Scan.repeat1 P.name
    4.79 -    >> (fn ((raw_run, raw_bind), targets) => Toplevel.theory 
    4.80 -          (fold (fn target => add_monad target raw_run raw_bind) targets))
    4.81 +    P.term -- P.term -- ((P.term >> SOME) -- Scan.repeat1 P.name
    4.82 +      || Scan.succeed NONE -- Scan.repeat1 P.name)
    4.83 +    >> (fn ((raw_run, raw_bind), (raw_unit, targets)) => Toplevel.theory 
    4.84 +          (fold (fn target => add_monad target raw_run raw_bind raw_unit) targets))
    4.85    );
    4.86  
    4.87  val _ =