Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: TPTP_Parser.thy Sprache: C

Original von: Coq^©

/***********************************************************************/
/*                                                                     */
/*                           Coq Compiler                              */
/*                                                                     */
/*        Benjamin Gregoire, projets Logical and Cristal               */
/*                        INRIA Rocquencourt                           */
/*                                                                     */
/*                                                                     */
/***********************************************************************/

#ifndef _COQ_FIX_CODE_
#define _COQ_FIX_CODE_

#include <caml/mlvalues.h>
void * coq_stat_alloc (asize_t sz);

#ifdef THREADED_CODE
extern char ** coq_instr_table;
extern char * coq_instr_base;
void init_arity();
#define VALINSTR(instr) ((opcode_t)(coq_instr_table[instr] - coq_instr_base))
#else
#define VALINSTR(instr) instr
#endif /*  THREADED_CODE */

#define Is_instruction(pc,instr) (*pc == VALINSTR(instr))

value coq_tcode_of_code(value code);
value coq_makeaccu (value i);
value coq_pushpop (value i);
value coq_accucond (value i);
value coq_is_accumulate_code(value code);

#endif /* _COQ_FIX_CODE_ */

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.