products/sources/formale Sprachen/Coq/kernel/byterun image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: polynomial_pseudo_divide.prf   Sprache: C

Original von: Coq©

pragma once

include <caml/callback.h>
include <caml/stack.h>


#define Is_uint63(v) (Tag_val(v) == Custom_tag)

#define uint_of_value(val) (((uint32_t)(val)) >> 1)

define DECLARE_NULLOP(name) \
value uint63_##name() { \
  static value* cb = 0; \
  CAMLparam0(); \
  if (!cb) cb = caml_named_value("uint63 " #name); \
  CAMLreturn(*cb); \
  }

define DECLARE_UNOP(name) \
value uint63_##name##_ml(value x) { \
  static value* cb = 0; \
  CAMLparam1(x); \
  if (!cb) cb = caml_named_value("uint63 " #name); \
  CAMLreturn(caml_callback(*cb, x)); \
  }

define CALL_UNOP_NOASSIGN(name, x) \
  value uint63_return_value__; \
  value uint63_arg_x__ = (x); \
  Setup_for_gc; \
  uint63_return_value__ = uint63_##name##_ml(uint63_arg_x__); \
  Restore_after_gc

define CALL_UNOP(name, x) do{ \
    CALL_UNOP_NOASSIGN(name, x); \
    accu = uint63_return_value__; \
  }while(0)

define CALL_PREDICATE(r, name, x) do{ \
    CALL_UNOP_NOASSIGN(name, x); \
    (r) = Int_val(uint63_return_value__); \
  }while(0)

define DECLARE_BINOP(name) \
value uint63_##name##_ml(value x, value y) { \
  static value* cb = 0; \
  CAMLparam2(x, y); \
  if (!cb) cb = caml_named_value("uint63 " #name); \
  CAMLreturn(caml_callback2(*cb, x, y)); \
  }

define CALL_BINOP_NOASSIGN(name, x, y) \
  value uint63_return_value__; \
  value uint63_arg_x__ = (x); \
  value uint63_arg_y__ = (y); \
  Setup_for_gc; \
  uint63_return_value__ = uint63_##name##_ml(uint63_arg_x__, uint63_arg_y__); \
  Restore_after_gc

define CALL_BINOP(name, x, y) do{ \
    CALL_BINOP_NOASSIGN(name, x, y);  \
    accu = uint63_return_value__; \
  }while(0)

define CALL_RELATION(r, name, x, y) do{ \
    CALL_BINOP_NOASSIGN(name, x, y); \
    (r) = Int_val(uint63_return_value__); \
  }while(0)

define DECLARE_TEROP(name) \
value uint63_##name##_ml(value x, value y, value z) { \
  static value* cb = 0; \
  CAMLparam3(x, y, z); \
  if (!cb) cb = caml_named_value("uint63 " #name); \
  CAMLreturn(caml_callback3(*cb, x, y, z)); \
  }

define CALL_TEROP(name, x, y, z) do{ \
    value uint63_return_value__; \
    value uint63_arg_x__ = (x); \
    value uint63_arg_y__ = (y); \
    value uint63_arg_z__ = (z); \
    Setup_for_gc; \
    uint63_return_value__ = uint63_##name##_ml(uint63_arg_x__, uint63_arg_y__, uint63_arg_z__); \
    Restore_after_gc; \
    accu = uint63_return_value__; \
  }while(0)

DECLARE_NULLOP(one)
DECLARE_BINOP(add)
#define Uint63_add(x, y) CALL_BINOP(add, x, y)
DECLARE_BINOP(addcarry)
#define Uint63_addcarry(x, y) CALL_BINOP(addcarry, x, y)
DECLARE_TEROP(addmuldiv)
#define Uint63_addmuldiv(x, y, z) CALL_TEROP(addmuldiv, x, y, z)
DECLARE_BINOP(div)
#define Uint63_div(x, y) CALL_BINOP(div, x, y)
DECLARE_BINOP(eq)
#define Uint63_eq(r, x, y) CALL_RELATION(r, eq, x, y)
DECLARE_UNOP(eq0)
#define Uint63_eq0(r, x) CALL_PREDICATE(r, eq0, x)
DECLARE_UNOP(head0)
#define Uint63_head0(x) CALL_UNOP(head0, x)
DECLARE_BINOP(land)
#define Uint63_land(x, y) CALL_BINOP(land, x, y)
DECLARE_BINOP(leq)
#define Uint63_leq(r, x, y) CALL_RELATION(r, leq, x, y)
DECLARE_BINOP(lor)
#define Uint63_lor(x, y) CALL_BINOP(lor, x, y)
DECLARE_BINOP(lsl)
#define Uint63_lsl(x, y) CALL_BINOP(lsl, x, y)
DECLARE_UNOP(lsl1)
#define Uint63_lsl1(x) CALL_UNOP(lsl1, x)
DECLARE_BINOP(lsr)
#define Uint63_lsr(x, y) CALL_BINOP(lsr, x, y)
DECLARE_UNOP(lsr1)
#define Uint63_lsr1(x) CALL_UNOP(lsr1, x)
DECLARE_BINOP(lt)
#define Uint63_lt(r, x, y) CALL_RELATION(r, lt, x, y)
DECLARE_BINOP(lxor)
#define Uint63_lxor(x, y) CALL_BINOP(lxor, x, y)
DECLARE_BINOP(mod)
#define Uint63_mod(x, y) CALL_BINOP(mod, x, y)
DECLARE_BINOP(mul)
#define Uint63_mul(x, y) CALL_BINOP(mul, x, y)
DECLARE_BINOP(sub)
#define Uint63_sub(x, y) CALL_BINOP(sub, x, y)
DECLARE_BINOP(subcarry)
#define Uint63_subcarry(x, y) CALL_BINOP(subcarry, x, y)
DECLARE_UNOP(tail0)
#define Uint63_tail0(x) CALL_UNOP(tail0, x)

DECLARE_TEROP(div21_ml)
define Uint63_div21(x, y, z, q) do{ \
    value uint63_return_value__; \
    value uint63_arg_x__ = (x); \
    value uint63_arg_y__ = (y); \
    value uint63_arg_z__ = (z); \
    Setup_for_gc; \
    uint63_return_value__ = \
      uint63_div21_ml_ml(uint63_arg_x__, uint63_arg_y__, uint63_arg_z__); \
    Restore_after_gc; \
    *q = Field(uint63_return_value__, 0); \
    accu = Field(uint63_return_value__, 1); \
  }while(0)

DECLARE_BINOP(mulc_ml)
define Uint63_mulc(x, y, h) do{ \
    value uint63_return_value__; \
    value uint63_arg_x__ = (x); \
    value uint63_arg_y__ = (y); \
    Setup_for_gc; \
    uint63_return_value__ = \
      uint63_mulc_ml_ml(uint63_arg_x__, uint63_arg_y__); \
    Restore_after_gc; \
    *(h) = Field(uint63_return_value__, 0); \
    accu = Field(uint63_return_value__, 1); \
  }while(0)

¤ Dauer der Verarbeitung: 0.16 Sekunden  (vorverarbeitet)  ¤





Kontakt
Drucken
Kontakt
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff