mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
1f766d2549
Two of the three examples which are extracted to ocaml code and then to javascript are not working, but they were broken since the new extraction which is bound to the use of Zarith and not Num. They should be repaired when js_of_ocaml supports Zarith
35 lines
755 B
OCaml
35 lines
755 B
OCaml
|
|
open Format
|
|
|
|
let () =
|
|
printf "%d@."
|
|
(EuclideanAlgorithm63.euclid (int_of_string Sys.argv.(1)) (int_of_string Sys.argv.(2)))
|
|
|
|
(*
|
|
let usage () =
|
|
eprintf "Reduction of combinator terms@.";
|
|
eprintf "Usage: %s <combinator term>@." Sys.argv.(0);
|
|
exit 2
|
|
|
|
let input =
|
|
if Array.length Sys.argv <> 2 then usage ();
|
|
Sys.argv.(1)
|
|
|
|
let input_term =
|
|
if input = "go" then
|
|
let i = Vstte12_combinators__Combinators.i in
|
|
Vstte12_combinators__Combinators.App(i,i)
|
|
else
|
|
try Parse.parse_term input
|
|
with _ ->
|
|
begin
|
|
eprintf "syntax error@.";
|
|
usage ()
|
|
end
|
|
|
|
let () =
|
|
let a = Vstte12_combinators__Combinators.reduction input_term in
|
|
printf "The normal form of %a is %a@."
|
|
Parse.pr input_term Parse.pr a
|
|
*)
|