← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to kernel/cbytecodes.mli

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
kernel/cbytecodes.mli
 
1
open Names
 
2
open Term
 
3
 
 
4
type tag = int 
 
5
 
 
6
val id_tag : tag
 
7
val iddef_tag : tag
 
8
val ind_tag : tag
 
9
val fix_tag : tag
 
10
val switch_tag : tag
 
11
val cofix_tag : tag
 
12
val cofix_evaluated_tag : tag
 
13
 
 
14
type structured_constant =
 
15
  | Const_sorts of sorts
 
16
  | Const_ind of inductive
 
17
  | Const_b0 of tag                
 
18
  | Const_bn of tag * structured_constant array
 
19
 
 
20
type reloc_table = (tag * int) array 
 
21
 
 
22
type annot_switch = 
 
23
   {ci : case_info; rtbl : reloc_table; tailcall : bool}
 
24
 
 
25
module Label : 
 
26
  sig
 
27
    type t = int
 
28
    val no : t
 
29
    val create : unit -> t
 
30
    val reset_label_counter : unit -> unit
 
31
  end 
 
32
 
 
33
type instruction =
 
34
  | Klabel of Label.t
 
35
  | Kacc of int
 
36
  | Kenvacc of int
 
37
  | Koffsetclosure of int
 
38
  | Kpush
 
39
  | Kpop of int
 
40
  | Kpush_retaddr of Label.t
 
41
  | Kapply of int                       (*  number of arguments *)
 
42
  | Kappterm of int * int               (* number of arguments, slot size *)
 
43
  | Kreturn of int                      (* slot size *)
 
44
  | Kjump
 
45
  | Krestart
 
46
  | Kgrab of int                        (* number of arguments *)
 
47
  | Kgrabrec of int                     (* rec arg *)
 
48
  | Kclosure of Label.t * int           (* label, number of free variables *)
 
49
  | Kclosurerec of int * int * Label.t array * Label.t array 
 
50
                   (* nb fv, init, lbl types, lbl bodies *)
 
51
  | Kclosurecofix of int * int * Label.t array * Label.t array 
 
52
                   (* nb fv, init, lbl types, lbl bodies *)
 
53
  | Kgetglobal of constant
 
54
  | Kconst of structured_constant
 
55
  | Kmakeblock of int * tag             (* size, tag *)
 
56
  | Kmakeprod 
 
57
  | Kmakeswitchblock of Label.t * Label.t * annot_switch * int
 
58
  | Kswitch of Label.t array * Label.t array (* consts,blocks *)
 
59
  | Kpushfields of int 
 
60
  | Kfield of int
 
61
  | Ksetfield of int
 
62
  | Kstop
 
63
  | Ksequence of bytecodes * bytecodes
 
64
(* spiwack: instructions concerning integers *)
 
65
  | Kbranch of Label.t                  (* jump to label, is it needed ? *)
 
66
  | Kaddint31                           (* adds the int31 in the accu 
 
67
                                           and the one ontop of the stack *)
 
68
  | Kaddcint31                          (* makes the sum and keeps the carry *)
 
69
  | Kaddcarrycint31                     (* sum +1, keeps the carry *)
 
70
  | Ksubint31                           (* subtraction modulo *)
 
71
  | Ksubcint31                          (* subtraction, keeps the carry *)
 
72
  | Ksubcarrycint31                     (* subtraction -1, keeps the carry *)
 
73
  | Kmulint31                           (* multiplication modulo *)
 
74
  | Kmulcint31                          (* multiplication, result in two
 
75
                                           int31, for exact computation *)
 
76
  | Kdiv21int31                         (* divides a double size integer
 
77
                                           (represented by an int31 in the 
 
78
                                           accumulator and one on the top of 
 
79
                                           the stack) by an int31. The result
 
80
                                           is a pair of the quotient and the 
 
81
                                           rest.
 
82
                                           If the divisor is 0, it returns
 
83
                                           0. *)
 
84
  | Kdivint31                           (* euclidian division (returns a pair
 
85
                                           quotient,rest) *)
 
86
  | Kaddmuldivint31                     (* generic operation for shifting and
 
87
                                           cycling. Takes 3 int31 i j and s,
 
88
                                           and returns x*2^s+y/(2^(31-s) *)
 
89
  | Kcompareint31                        (* unsigned comparison of int31
 
90
                                           cf COMPAREINT31 in 
 
91
                                           kernel/byterun/coq_interp.c
 
92
                                           for more info *)
 
93
  | Khead0int31                         (* Give the numbers of 0 in head of a in31*)
 
94
  | Ktail0int31                         (* Give the numbers of 0 in tail of a in31 
 
95
                                           ie low bits *)
 
96
  | Kisconst of Label.t                 (* conditional jump *)
 
97
  | Kareconst of int*Label.t            (* conditional jump *)
 
98
  | Kcompint31                          (* dynamic compilation of int31 *)
 
99
  | Kdecompint31                        (* dynamix decompilation of int31 *)
 
100
(* /spiwack *)
 
101
 
 
102
 
 
103
and bytecodes = instruction list
 
104
 
 
105
type fv_elem = FVnamed of identifier | FVrel of int
 
106
 
 
107
type fv = fv_elem array
 
108
 
 
109
 
 
110
(* spiwack: this exception is expected to be raised by function expecting
 
111
            closed terms. *)
 
112
exception NotClosed
 
113
 
 
114
(*spiwack: both type have been moved from Cbytegen because I needed then
 
115
  for the retroknowledge *)
 
116
type vm_env = {
 
117
    size : int;              (* longueur de la liste [n] *)
 
118
    fv_rev : fv_elem list    (* [fvn; ... ;fv1] *)
 
119
  }    
 
120
   
 
121
   
 
122
type comp_env = { 
 
123
    nb_stack : int;              (* nbre de variables sur la pile          *)
 
124
    in_stack : int list;         (* position dans la pile                  *)
 
125
    nb_rec : int;                (* nbre de fonctions mutuellement         *)
 
126
                                 (* recursives =  nbr                      *)
 
127
    pos_rec  : instruction list; (* instruction d'acces pour les variables *)
 
128
                                 (*  de point fix ou de cofix              *)
 
129
    offset : int;                 
 
130
    in_env : vm_env ref 
 
131
  } 
 
132
 
 
133
val draw_instr : bytecodes -> unit
 
134
 
 
135
 
 
136
 
 
137
(*spiwack: moved this here because I needed it for retroknowledge *)
 
138
type block = 
 
139
  | Bconstr of constr
 
140
  | Bstrconst of structured_constant
 
141
  | Bmakeblock of int * block array
 
142
  | Bconstruct_app of int * int * int * block array
 
143
                  (* tag , nparams, arity *)
 
144
  | Bspecial of (comp_env -> block array -> int -> bytecodes -> bytecodes) * block array
 
145
                (* compilation function (see get_vm_constant_dynamic_info in 
 
146
                   retroknowledge.mli for more info) , argument array  *)