src/Tools/Code/code_ml.ML
changeset 69906 55534affe445
parent 69743 6a9a8ef5e4c6
child 69910 0c0f7b4a72bf
     1.1 --- a/src/Tools/Code/code_ml.ML	Sun Mar 10 15:16:45 2019 +0000
     1.2 +++ b/src/Tools/Code/code_ml.ML	Sun Mar 10 15:16:45 2019 +0000
     1.3 @@ -717,10 +717,10 @@
     1.4  
     1.5  val literals_ocaml = let
     1.6    fun numeral_ocaml k = if k < 0
     1.7 -    then "(Big_int.minus_big_int " ^ numeral_ocaml (~ k) ^ ")"
     1.8 +    then "(Z.neg " ^ numeral_ocaml (~ k) ^ ")"
     1.9      else if k <= 1073741823
    1.10 -      then "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
    1.11 -      else "(Big_int.big_int_of_string " ^ quote (string_of_int k) ^ ")"
    1.12 +      then "(Z.of_int " ^ string_of_int k ^ ")"
    1.13 +      else "(Z.of_string " ^ quote (string_of_int k) ^ ")"
    1.14  in Literals {
    1.15    literal_string = print_ocaml_string,
    1.16    literal_numeral = numeral_ocaml,
    1.17 @@ -885,9 +885,11 @@
    1.18        evaluation_args = []})
    1.19    #> Code_Target.add_language
    1.20      (target_OCaml, {serializer = serializer_ocaml, literals = literals_ocaml,
    1.21 -      check = {env_var = "ISABELLE_OCAML",
    1.22 -        make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
    1.23 -        make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu -safe-string nums.cma ROOT.ocaml"},
    1.24 +      check = {env_var = "ISABELLE_OPAM_ROOT",
    1.25 +        make_destination = fn p => Path.append p (Path.explode "ROOT.ml")
    1.26 +          (*extension demanded by OCaml compiler*),
    1.27 +        make_command = fn _ =>
    1.28 +          "\"$ISABELLE_ROOT/lib/scripts/ocamlexec\" ocamlfind ocamlopt -w pu -package zarith -linkpkg ROOT.ml"},
    1.29        evaluation_args = []})
    1.30    #> Code_Target.set_printings (Type_Constructor ("fun",
    1.31      [(target_SML, SOME (2, fun_syntax)), (target_OCaml, SOME (2, fun_syntax))]))
    1.32 @@ -904,6 +906,6 @@
    1.33        "sig", "struct", "then", "to", "true", "try", "type", "val",
    1.34        "virtual", "when", "while", "with"
    1.35      ]
    1.36 -  #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod", "Big_int"]);
    1.37 +  #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod", "Z"]);
    1.38  
    1.39  end; (*struct*)