1
/***********************************************************************/
5
/* Benjamin Gregoire, projets Logical and Cristal */
6
/* INRIA Rocquencourt */
9
/***********************************************************************/
11
#ifndef _COQ_INSTRUCT_
12
#define _COQ_INSTRUCT_
15
ACC0, ACC1, ACC2, ACC3, ACC4, ACC5, ACC6, ACC7, ACC,
17
PUSHACC0, PUSHACC1, PUSHACC2, PUSHACC3, PUSHACC4,
18
PUSHACC5, PUSHACC6, PUSHACC7, PUSHACC,
20
ENVACC1, ENVACC2, ENVACC3, ENVACC4, ENVACC,
21
PUSHENVACC1, PUSHENVACC2, PUSHENVACC3, PUSHENVACC4, PUSHENVACC,
23
APPLY, APPLY1, APPLY2, APPLY3,
24
APPTERM, APPTERM1, APPTERM2, APPTERM3,
25
RETURN, RESTART, GRAB, GRABREC,
26
CLOSURE, CLOSUREREC, CLOSURECOFIX,
27
OFFSETCLOSUREM2, OFFSETCLOSURE0, OFFSETCLOSURE2, OFFSETCLOSURE,
28
PUSHOFFSETCLOSUREM2, PUSHOFFSETCLOSURE0, PUSHOFFSETCLOSURE2,
30
GETGLOBAL, PUSHGETGLOBAL,
31
MAKEBLOCK, MAKEBLOCK1, MAKEBLOCK2, MAKEBLOCK3, MAKEBLOCK4,
33
GETFIELD0, GETFIELD1, GETFIELD,
34
SETFIELD0, SETFIELD1, SETFIELD,
35
CONST0, CONST1, CONST2, CONST3, CONSTINT,
36
PUSHCONST0, PUSHCONST1, PUSHCONST2, PUSHCONST3, PUSHCONSTINT,
37
ACCUMULATE, ACCUMULATECOND,
38
MAKESWITCHBLOCK, MAKEACCU, MAKEPROD,
41
ADDINT31, ADDCINT31, ADDCARRYCINT31,
42
SUBINT31, SUBCINT31, SUBCARRYCINT31,
43
MULCINT31, MULINT31, DIV21INT31, DIVINT31,
44
ADDMULDIVINT31, COMPAREINT31,
45
HEAD0INT31, TAIL0INT31,
47
COMPINT31, DECOMPINT31,
52
#endif /* _COQ_INSTRUCT_ */