turbine3ProgCompScript.sml

(*
  Auto-generated by Daisy (https://gitlab.mpi-sws.org/AVA/daisy
  *)
(* INCLUDES, do not change those *)
open exampleLib;

val _ = new_theory "turbine3ProgComp";

val _ = translation_extends "cfSupport";

Definition theAST_pre_def:
  theAST_pre = \ (x:(string, string) id).
  if x = Short "r" then (((19)/(5), (39)/(5)):real#real)
  else if x = Short "v" then (((-9)/(2), (-3)/(10)):real#real)
  else if x = Short "w" then (((2)/(5), (9)/(10)):real#real)
  else (0,0)
End

Definition theAST_def:
  theAST =
  [ Dlet unknown_loc (Pvar "turbine3")
    (Fun "v"(Fun "w"(Fun "r"
      (FpOptimise Opt
(App (FP_bop FP_Sub)
        [
          (App (FP_bop FP_Sub)
          [
            (App (FP_bop FP_Sub)
            [
              (App FpFromWord [Lit (Word64 (4613937818241073152w:word64))]);
              (App (FP_bop FP_Div)
              [
                (App FpFromWord [Lit (Word64 (4611686018427387904w:word64))]);
                (App (FP_bop FP_Mul)
                [
                  Var (Short  "r");
                  Var (Short  "r")
                ])
              ])
            ]);
            (App (FP_bop FP_Div)
            [
              (App (FP_bop FP_Mul)
              [
                (App (FP_bop FP_Mul)
                [
                  (App FpFromWord [Lit (Word64 (4593671619917905920w:word64))]);
                  (App (FP_bop FP_Add)
                  [
                    (App FpFromWord [Lit (Word64 (4607182418800017408w:word64))]);
                    (App (FP_bop FP_Mul)
                    [
                      (App FpFromWord [Lit (Word64 (4611686018427387904w:word64))]);
                      Var (Short  "v")
                    ])
                  ])
                ]);
                (App (FP_bop FP_Mul)
                [
                  (App (FP_bop FP_Mul)
                  [
                    (App (FP_bop FP_Mul)
                    [
                      Var (Short  "w");
                      Var (Short  "w")
                    ]);
                    Var (Short  "r")
                  ]);
                  Var (Short  "r")
                ])
              ]);
              (App (FP_bop FP_Sub)
              [
                (App FpFromWord [Lit (Word64 (4607182418800017408w:word64))]);
                Var (Short  "v")
              ])
            ])
          ]);
          (App FpFromWord [Lit (Word64 (4602678819172646912w:word64))])
        ])))))]
End

Definition theErrBound_def:
  theErrBound = inv (2 pow (5))
End

val x = define_benchmark theAST_def theAST_pre_def true;

val _ = export_theory()