doppler1ProgCompScript.sml

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

val _ = new_theory "doppler1ProgComp";

val _ = translation_extends "cfSupport";

Definition theAST_pre_def:
  theAST_pre = \ (x:(string, string) id).
  if x = Short "T" then (((-30)/(1), (50)/(1)):real#real)
  else if x = Short "u" then (((-100)/(1), (100)/(1)):real#real)
  else if x = Short "v" then (((20)/(1), (20000)/(1)):real#real)
  else (0,0)
End

Definition theAST_def:
  theAST =
  [ Dlet unknown_loc (Pvar "doppler1")
    (Fun "u"(Fun "v"(Fun "T"
      (FpOptimise Opt
        (Let (SOME "t1")
        (App (FP_bop FP_Add)
          [
            (App FpFromWord [Lit (Word64 (4644537666646730342w:word64))]);
            (App (FP_bop FP_Mul)
            [
              (App FpFromWord [Lit (Word64 (4603579539098121011w:word64))]);
              Var (Short  "T")
            ])
          ])
        ((App (FP_bop FP_Div)
          [
            (App (FP_bop FP_Mul)
            [
              (App (FP_uop FP_Neg)
              [
                Var (Short  "t1")
              ]);
              Var (Short  "v")
            ]);
            (App (FP_bop FP_Mul)
            [
              (App (FP_bop FP_Add)
              [
                Var (Short  "t1");
                Var (Short  "u")
              ]);
              (App (FP_bop FP_Add)
              [
                Var (Short  "t1");
                Var (Short  "u")
              ])
            ])
          ])))))))]
End

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

val x = define_benchmark theAST_def theAST_pre_def true;

val _ = export_theory()