carbonGasProgCompScript.sml

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

val _ = new_theory "carbonGasProgComp";

val _ = translation_extends "cfSupport";

Definition theAST_pre_def:
  theAST_pre = \ (x:(string, string) id).
  if x = Short "v" then (((1)/(10), (1)/(2)):real#real)
  else (0,0)
End

Definition theAST_def:
  theAST =
  [ Dlet unknown_loc (Pvar "carbonGas")
    (Fun "v"
      (FpOptimise Opt
        (Let (SOME "p")
        (App FpFromWord [Lit (Word64 (4719966430336909312w:word64))])
        (          (Let (SOME "a")
          (App FpFromWord [Lit (Word64 (4600895393720208196w:word64))])
          (            (Let (SOME "b")
            (App FpFromWord [Lit (Word64 (4541426232537668655w:word64))])
            (              (Let (SOME "t")
              (App FpFromWord [Lit (Word64 (4643985272004935680w:word64))])
              (                (Let (SOME "n")
                (App FpFromWord [Lit (Word64 (4652007308841189376w:word64))])
                (                  (Let (SOME "k")
                  (App FpFromWord [Lit (Word64 (4265103357012230254w:word64))])
                  ((App (FP_bop FP_Sub)
                    [
                      (App (FP_bop FP_Mul)
                      [
                        (App (FP_bop FP_Add)
                        [
                          Var (Short  "p");
                          (App (FP_bop FP_Mul)
                          [
                            (App (FP_bop FP_Mul)
                            [
                              Var (Short  "a");
                              (App (FP_bop FP_Div)
                              [
                                Var (Short  "n");
                                Var (Short  "v")
                              ])
                            ]);
                            (App (FP_bop FP_Div)
                            [
                              Var (Short  "n");
                              Var (Short  "v")
                            ])
                          ])
                        ]);
                        (App (FP_bop FP_Sub)
                        [
                          Var (Short  "v");
                          (App (FP_bop FP_Mul)
                          [
                            Var (Short  "n");
                            Var (Short  "b")
                          ])
                        ])
                      ]);
                      (App (FP_bop FP_Mul)
                      [
                        (App (FP_bop FP_Mul)
                        [
                          Var (Short  "k");
                          Var (Short  "n")
                        ]);
                        Var (Short  "t")
                      ])
                    ])))))))))))))))]
End

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

val x = define_benchmark theAST_def theAST_pre_def true;

val _ = export_theory()