migrated from Nums to Zarith as library for OCaml integer arithmetic
authorhaftmann
Sun Mar 10 15:16:45 2019 +0000 (2 months ago)
changeset 6990655534affe445
parent 69905 06f204a2f3c2
child 69907 4343c1bfa52d
migrated from Nums to Zarith as library for OCaml integer arithmetic
NEWS
lib/scripts/ocaml
lib/scripts/ocamlexec
src/HOL/Code_Numeral.thy
src/HOL/GCD.thy
src/HOL/Imperative_HOL/Array.thy
src/HOL/Library/Code_Real_Approx_By_Float.thy
src/HOL/Library/code_test.ML
src/HOL/String.thy
src/Tools/Code/code_ml.ML
src/Tools/Code/code_target.ML
     1.1 --- a/NEWS	Sun Mar 10 15:16:45 2019 +0000
     1.2 +++ b/NEWS	Sun Mar 10 15:16:45 2019 +0000
     1.3 @@ -123,6 +123,15 @@
     1.4  * Code generation for OCaml: proper strings are used for literals.
     1.5  Minor INCOMPATIBILITY.
     1.6  
     1.7 +* Code generation for OCaml: Zarith superseedes Nums as library for
     1.8 +integer arithmetic.  Use the following incantation to obtain a suitable
     1.9 +component setup:
    1.10 +
    1.11 +  isabelle ocaml_setup
    1.12 +  isabelle ocaml_opam install zarith
    1.13 +
    1.14 +Minor INCOMPATIBILITY
    1.15 +
    1.16  * Code generation for Haskell: code includes for Haskell must contain
    1.17  proper module frame, nothing is added magically any longer.
    1.18  INCOMPATIBILITY.
     2.1 --- a/lib/scripts/ocaml	Sun Mar 10 15:16:45 2019 +0000
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,13 +0,0 @@
     2.4 -#!/usr/bin/env bash
     2.5 -#
     2.6 -# Author: Makarius
     2.7 -#
     2.8 -# Invoke ocaml via "opam".
     2.9 -
    2.10 -if [ -d "$ISABELLE_OPAM_ROOT" ]
    2.11 -then
    2.12 -  isabelle_opam config exec --switch "$ISABELLE_OCAML_VERSION" -- ocaml "$@"
    2.13 -else
    2.14 -  echo "Cannot execute ocaml: missing Isabelle OCaml setup" >&2
    2.15 -  exit 127
    2.16 -fi
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/lib/scripts/ocamlexec	Sun Mar 10 15:16:45 2019 +0000
     3.3 @@ -0,0 +1,13 @@
     3.4 +#!/usr/bin/env bash
     3.5 +#
     3.6 +# Author: Makarius; Florian Haftmann
     3.7 +#
     3.8 +# Invoke command in OCaml environment setup by "opam".
     3.9 +
    3.10 +if [ -d "$ISABELLE_OPAM_ROOT" ]
    3.11 +then
    3.12 +  isabelle_opam config exec --switch "$ISABELLE_OCAML_VERSION" -- "$@"
    3.13 +else
    3.14 +  echo "Cannot execute: missing Isabelle OCaml setup" >&2
    3.15 +  exit 127
    3.16 +fi
     4.1 --- a/src/HOL/Code_Numeral.thy	Sun Mar 10 15:16:45 2019 +0000
     4.2 +++ b/src/HOL/Code_Numeral.thy	Sun Mar 10 15:16:45 2019 +0000
     4.3 @@ -652,7 +652,7 @@
     4.4  code_printing
     4.5    type_constructor integer \<rightharpoonup>
     4.6      (SML) "IntInf.int"
     4.7 -    and (OCaml) "Big'_int.big'_int"
     4.8 +    and (OCaml) "Z.t"
     4.9      and (Haskell) "Integer"
    4.10      and (Scala) "BigInt"
    4.11      and (Eval) "int"
    4.12 @@ -662,7 +662,7 @@
    4.13  code_printing
    4.14    constant "0::integer" \<rightharpoonup>
    4.15      (SML) "!(0/ :/ IntInf.int)"
    4.16 -    and (OCaml) "Big'_int.zero'_big'_int"
    4.17 +    and (OCaml) "Z.zero"
    4.18      and (Haskell) "!(0/ ::/ Integer)"
    4.19      and (Scala) "BigInt(0)"
    4.20  
    4.21 @@ -676,25 +676,25 @@
    4.22  code_printing
    4.23    constant "plus :: integer \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup>
    4.24      (SML) "IntInf.+ ((_), (_))"
    4.25 -    and (OCaml) "Big'_int.add'_big'_int"
    4.26 +    and (OCaml) "Z.add"
    4.27      and (Haskell) infixl 6 "+"
    4.28      and (Scala) infixl 7 "+"
    4.29      and (Eval) infixl 8 "+"
    4.30  | constant "uminus :: integer \<Rightarrow> _" \<rightharpoonup>
    4.31      (SML) "IntInf.~"
    4.32 -    and (OCaml) "Big'_int.minus'_big'_int"
    4.33 +    and (OCaml) "Z.neg"
    4.34      and (Haskell) "negate"
    4.35      and (Scala) "!(- _)"
    4.36      and (Eval) "~/ _"
    4.37  | constant "minus :: integer \<Rightarrow> _" \<rightharpoonup>
    4.38      (SML) "IntInf.- ((_), (_))"
    4.39 -    and (OCaml) "Big'_int.sub'_big'_int"
    4.40 +    and (OCaml) "Z.sub"
    4.41      and (Haskell) infixl 6 "-"
    4.42      and (Scala) infixl 7 "-"
    4.43      and (Eval) infixl 8 "-"
    4.44  | constant Code_Numeral.dup \<rightharpoonup>
    4.45      (SML) "IntInf.*/ (2,/ (_))"
    4.46 -    and (OCaml) "Big'_int.mult'_big'_int/ (Big'_int.big'_int'_of'_int/ 2)"
    4.47 +    and (OCaml) "Z.shift'_left/ _/ 1"
    4.48      and (Haskell) "!(2 * _)"
    4.49      and (Scala) "!(2 * _)"
    4.50      and (Eval) "!(2 * _)"
    4.51 @@ -705,37 +705,37 @@
    4.52      and (Scala) "!sys.error(\"sub\")"
    4.53  | constant "times :: integer \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup>
    4.54      (SML) "IntInf.* ((_), (_))"
    4.55 -    and (OCaml) "Big'_int.mult'_big'_int"
    4.56 +    and (OCaml) "Z.mul"
    4.57      and (Haskell) infixl 7 "*"
    4.58      and (Scala) infixl 8 "*"
    4.59      and (Eval) infixl 9 "*"
    4.60  | constant Code_Numeral.divmod_abs \<rightharpoonup>
    4.61      (SML) "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)"
    4.62 -    and (OCaml) "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)"
    4.63 +    and (OCaml) "!(fun k l ->/ if Z.equal Z.zero l then/ (Z.zero, l) else/ Z.div'_rem/ (Z.abs k)/ (Z.abs l))"
    4.64      and (Haskell) "divMod/ (abs _)/ (abs _)"
    4.65      and (Scala) "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))"
    4.66      and (Eval) "Integer.div'_mod/ (abs _)/ (abs _)"
    4.67  | constant "HOL.equal :: integer \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
    4.68      (SML) "!((_ : IntInf.int) = _)"
    4.69 -    and (OCaml) "Big'_int.eq'_big'_int"
    4.70 +    and (OCaml) "Z.equal"
    4.71      and (Haskell) infix 4 "=="
    4.72      and (Scala) infixl 5 "=="
    4.73      and (Eval) infixl 6 "="
    4.74  | constant "less_eq :: integer \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
    4.75      (SML) "IntInf.<= ((_), (_))"
    4.76 -    and (OCaml) "Big'_int.le'_big'_int"
    4.77 +    and (OCaml) "Z.leq"
    4.78      and (Haskell) infix 4 "<="
    4.79      and (Scala) infixl 4 "<="
    4.80      and (Eval) infixl 6 "<="
    4.81  | constant "less :: integer \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
    4.82      (SML) "IntInf.< ((_), (_))"
    4.83 -    and (OCaml) "Big'_int.lt'_big'_int"
    4.84 +    and (OCaml) "Z.lt"
    4.85      and (Haskell) infix 4 "<"
    4.86      and (Scala) infixl 4 "<"
    4.87      and (Eval) infixl 6 "<"
    4.88  | constant "abs :: integer \<Rightarrow> _" \<rightharpoonup>
    4.89      (SML) "IntInf.abs"
    4.90 -    and (OCaml) "Big'_int.abs'_big'_int"
    4.91 +    and (OCaml) "Z.abs"
    4.92      and (Haskell) "Prelude.abs"
    4.93      and (Scala) "_.abs"
    4.94      and (Eval) "abs"
     5.1 --- a/src/HOL/GCD.thy	Sun Mar 10 15:16:45 2019 +0000
     5.2 +++ b/src/HOL/GCD.thy	Sun Mar 10 15:16:45 2019 +0000
     5.3 @@ -2735,7 +2735,7 @@
     5.4  
     5.5  code_printing
     5.6    constant "gcd :: integer \<Rightarrow> _" \<rightharpoonup>
     5.7 -    (OCaml) "Big'_int.gcd'_big'_int"
     5.8 +    (OCaml) "!(fun k l -> if Z.equal k Z.zero then/ Z.abs l else if Z.equal/ l Z.zero then Z.abs k else Z.gcd k l)"
     5.9    and (Haskell) "Prelude.gcd"
    5.10    and (Scala) "_.gcd'((_)')"
    5.11    \<comment> \<open>There is no gcd operation in the SML standard library, so no code setup for SML\<close>
     6.1 --- a/src/HOL/Imperative_HOL/Array.thy	Sun Mar 10 15:16:45 2019 +0000
     6.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Sun Mar 10 15:16:45 2019 +0000
     6.3 @@ -458,13 +458,13 @@
     6.4  
     6.5  code_printing type_constructor array \<rightharpoonup> (OCaml) "_/ array"
     6.6  code_printing constant Array \<rightharpoonup> (OCaml) "failwith/ \"bare Array\""
     6.7 -code_printing constant Array.new' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Array.make/ (Big'_int.int'_of'_big'_int/ _)/ _)"
     6.8 +code_printing constant Array.new' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Array.make/ (Z.to'_int/ _)/ _)"
     6.9  code_printing constant Array.of_list \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Array.of'_list/ _)"
    6.10  code_printing constant Array.make' \<rightharpoonup> (OCaml)
    6.11 -  "(fun/ ()/ ->/ Array.init/ (Big'_int.int'_of'_big'_int/ _)/ (fun k'_ ->/ _/ (Big'_int.big'_int'_of'_int/ k'_)))"
    6.12 -code_printing constant Array.len' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))"
    6.13 -code_printing constant Array.nth' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Array.get/ _/ (Big'_int.int'_of'_big'_int/ _))"
    6.14 -code_printing constant Array.upd' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Array.set/ _/ (Big'_int.int'_of'_big'_int/ _)/ _)"
    6.15 +  "(fun/ ()/ ->/ Array.init/ (Z.to'_int/ _)/ (fun k'_ ->/ _/ (Z.of'_int/ k'_)))"
    6.16 +code_printing constant Array.len' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Z.of'_int/ (Array.length/ _))"
    6.17 +code_printing constant Array.nth' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Array.get/ _/ (Z.to'_int/ _))"
    6.18 +code_printing constant Array.upd' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Array.set/ _/ (Z.to'_int/ _)/ _)"
    6.19  code_printing constant "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" \<rightharpoonup> (OCaml) infixl 4 "="
    6.20  
    6.21  code_reserved OCaml Array
     7.1 --- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Sun Mar 10 15:16:45 2019 +0000
     7.2 +++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Sun Mar 10 15:16:45 2019 +0000
     7.3 @@ -155,7 +155,7 @@
     7.4  code_printing
     7.5    constant real_of_integer \<rightharpoonup>
     7.6      (SML) "Real.fromInt"
     7.7 -    and (OCaml) "Pervasives.float (Big'_int.int'_of'_big'_int (_))"
     7.8 +    and (OCaml) "Pervasives.float/ (Big'_int.to'_int (_))"
     7.9  
    7.10  context
    7.11  begin
     8.1 --- a/src/HOL/Library/code_test.ML	Sun Mar 10 15:16:45 2019 +0000
     8.2 +++ b/src/HOL/Library/code_test.ML	Sun Mar 10 15:16:45 2019 +0000
     8.3 @@ -442,7 +442,7 @@
     8.4  (* driver for OCaml *)
     8.5  
     8.6  val ocamlN = "OCaml"
     8.7 -val ISABELLE_OCAMLC = "ISABELLE_OCAMLC"
     8.8 +val ISABELLE_OPAM_ROOT = "ISABELLE_OPAM_ROOT"
     8.9  
    8.10  fun mk_driver_ocaml _ path _ value_name =
    8.11    let
    8.12 @@ -467,9 +467,9 @@
    8.13  
    8.14      val compiled_path = Path.append path (Path.basic "test")
    8.15      val compile_cmd =
    8.16 -      "\"$ISABELLE_OCAMLC\" -w pu -o " ^ File.bash_path compiled_path ^
    8.17 -      " -I " ^ File.bash_path path ^
    8.18 -      " nums.cma " ^ File.bash_path code_path ^ " " ^ File.bash_path driver_path
    8.19 +      "\"$ISABELLE_ROOT/lib/scripts/ocamlexec\" ocamlfind ocamlopt -w pu -package zarith -linkpkg " ^
    8.20 +      " -o " ^ File.bash_path compiled_path ^ " -I " ^ File.bash_path path ^ " " ^
    8.21 +      File.bash_path code_path ^ " " ^ File.bash_path driver_path
    8.22  
    8.23      val run_cmd = File.bash_path compiled_path
    8.24    in
    8.25 @@ -478,7 +478,7 @@
    8.26    end
    8.27  
    8.28  fun evaluate_in_ocaml ctxt =
    8.29 -  evaluate mk_driver_ocaml (SOME (ISABELLE_OCAMLC, "ocamlc executable")) ocamlN ctxt
    8.30 +  evaluate mk_driver_ocaml (SOME (ISABELLE_OPAM_ROOT, "ocaml opam environment")) ocamlN ctxt
    8.31  
    8.32  
    8.33  (* driver for GHC *)
     9.1 --- a/src/HOL/String.thy	Sun Mar 10 15:16:45 2019 +0000
     9.2 +++ b/src/HOL/String.thy	Sun Mar 10 15:16:45 2019 +0000
     9.3 @@ -673,7 +673,7 @@
     9.4      (SML) "!(String.implode/ o List.map (fn k => if 0 <= k andalso k < 128 then (Char.chr o IntInf.toInt) k else raise Fail \"Non-ASCII character in literal\"))"
     9.5      and (OCaml) "!(let xs = _
     9.6        and chr k =
     9.7 -        let l = Big'_int.int'_of'_big'_int k
     9.8 +        let l = Z.to'_int k
     9.9            in if 0 <= l && l < 128
    9.10            then Char.chr l
    9.11            else failwith \"Non-ASCII character in literal\"
    9.12 @@ -683,7 +683,7 @@
    9.13  | constant String.asciis_of_literal \<rightharpoonup>
    9.14      (SML) "!(List.map (fn c => let val k = Char.ord c in if k < 128 then IntInf.fromInt k else raise Fail \"Non-ASCII character in literal\" end) /o String.explode)"
    9.15      and (OCaml) "!(let s = _ in let rec exp i l = if i < 0 then l else exp (i - 1) (let k = Char.code (String.get s i) in
    9.16 -      if k < 128 then Big'_int.big'_int'_of'_int k :: l else failwith \"Non-ASCII character in literal\") in exp (String.length s - 1) [])"
    9.17 +      if k < 128 then Z.of'_int k :: l else failwith \"Non-ASCII character in literal\") in exp (String.length s - 1) [])"
    9.18      and (Haskell) "map/ (let ord k | (k < 128) = Prelude.toInteger k in ord . (Prelude.fromEnum :: Prelude.Char -> Prelude.Int))"
    9.19      and (Scala) "!(_.toList.map(c => { val k: Int = c.toInt; if (k < 128) BigInt(k) else sys.error(\"Non-ASCII character in literal\") }))"
    9.20  | class_instance String.literal :: equal \<rightharpoonup>
    10.1 --- a/src/Tools/Code/code_ml.ML	Sun Mar 10 15:16:45 2019 +0000
    10.2 +++ b/src/Tools/Code/code_ml.ML	Sun Mar 10 15:16:45 2019 +0000
    10.3 @@ -717,10 +717,10 @@
    10.4  
    10.5  val literals_ocaml = let
    10.6    fun numeral_ocaml k = if k < 0
    10.7 -    then "(Big_int.minus_big_int " ^ numeral_ocaml (~ k) ^ ")"
    10.8 +    then "(Z.neg " ^ numeral_ocaml (~ k) ^ ")"
    10.9      else if k <= 1073741823
   10.10 -      then "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
   10.11 -      else "(Big_int.big_int_of_string " ^ quote (string_of_int k) ^ ")"
   10.12 +      then "(Z.of_int " ^ string_of_int k ^ ")"
   10.13 +      else "(Z.of_string " ^ quote (string_of_int k) ^ ")"
   10.14  in Literals {
   10.15    literal_string = print_ocaml_string,
   10.16    literal_numeral = numeral_ocaml,
   10.17 @@ -885,9 +885,11 @@
   10.18        evaluation_args = []})
   10.19    #> Code_Target.add_language
   10.20      (target_OCaml, {serializer = serializer_ocaml, literals = literals_ocaml,
   10.21 -      check = {env_var = "ISABELLE_OCAML",
   10.22 -        make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
   10.23 -        make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu -safe-string nums.cma ROOT.ocaml"},
   10.24 +      check = {env_var = "ISABELLE_OPAM_ROOT",
   10.25 +        make_destination = fn p => Path.append p (Path.explode "ROOT.ml")
   10.26 +          (*extension demanded by OCaml compiler*),
   10.27 +        make_command = fn _ =>
   10.28 +          "\"$ISABELLE_ROOT/lib/scripts/ocamlexec\" ocamlfind ocamlopt -w pu -package zarith -linkpkg ROOT.ml"},
   10.29        evaluation_args = []})
   10.30    #> Code_Target.set_printings (Type_Constructor ("fun",
   10.31      [(target_SML, SOME (2, fun_syntax)), (target_OCaml, SOME (2, fun_syntax))]))
   10.32 @@ -904,6 +906,6 @@
   10.33        "sig", "struct", "then", "to", "true", "try", "type", "val",
   10.34        "virtual", "when", "while", "with"
   10.35      ]
   10.36 -  #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod", "Big_int"]);
   10.37 +  #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod", "Z"]);
   10.38  
   10.39  end; (*struct*)
    11.1 --- a/src/Tools/Code/code_target.ML	Sun Mar 10 15:16:45 2019 +0000
    11.2 +++ b/src/Tools/Code/code_target.ML	Sun Mar 10 15:16:45 2019 +0000
    11.3 @@ -422,8 +422,9 @@
    11.4          val _ = export_result ctxt (SOME (SOME destination)) 80
    11.5            (invoke_serializer ctxt target_name generatedN args program all_public syms)
    11.6          val cmd = make_command generatedN;
    11.7 +        val context_cmd = "cd " ^ File.bash_path p ^ " && " ^ cmd ^ " 2>&1";
    11.8        in
    11.9 -        if Isabelle_System.bash ("cd " ^ File.bash_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
   11.10 +        if Isabelle_System.bash context_cmd <> 0
   11.11          then error ("Code check failed for " ^ target_name ^ ": " ^ cmd)
   11.12          else ()
   11.13        end;