← Back to branch summary

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

« back to all changes in this revision

Viewing changes to kernel/cbytecodes.ml

  • 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.ml
 
1
open Names
 
2
open Term
 
3
 
 
4
type tag = int 
 
5
 
 
6
let id_tag = 0
 
7
let iddef_tag = 1
 
8
let ind_tag = 2
 
9
let fix_tag = 3
 
10
let switch_tag = 4
 
11
let cofix_tag = 5
 
12
let cofix_evaluated_tag = 6
 
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
 
 
21
type reloc_table = (tag * int) array 
 
22
 
 
23
type annot_switch = 
 
24
   {ci : case_info; rtbl : reloc_table; tailcall : bool}
 
25
 
 
26
module Label = 
 
27
  struct
 
28
    type t = int
 
29
    let no = -1
 
30
    let counter = ref no
 
31
    let create () = incr counter; !counter
 
32
    let reset_label_counter () = counter := no 
 
33
  end
 
34
 
 
35
 
 
36
type instruction =
 
37
  | Klabel of Label.t
 
38
  | Kacc of int
 
39
  | Kenvacc of int
 
40
  | Koffsetclosure of int
 
41
  | Kpush
 
42
  | Kpop of int
 
43
  | Kpush_retaddr of Label.t
 
44
  | Kapply of int                       (*  number of arguments *)
 
45
  | Kappterm of int * int               (* number of arguments, slot size *)
 
46
  | Kreturn of int                      (* slot size *)
 
47
  | Kjump
 
48
  | Krestart
 
49
  | Kgrab of int                        (* number of arguments *)
 
50
  | Kgrabrec of int                     (* rec arg *)
 
51
  | Kclosure of Label.t * int           (* label, number of free variables *)
 
52
  | Kclosurerec of int * int * Label.t array * Label.t array 
 
53
                   (* nb fv, init, lbl types, lbl bodies *)
 
54
  | Kclosurecofix of int * int * Label.t array * Label.t array 
 
55
                   (* nb fv, init, lbl types, lbl bodies *)
 
56
  | Kgetglobal of constant
 
57
  | Kconst of structured_constant
 
58
  | Kmakeblock of int * tag             (* size, tag *)
 
59
  | Kmakeprod 
 
60
  | Kmakeswitchblock of Label.t * Label.t * annot_switch * int
 
61
  | Kswitch of Label.t array * Label.t array (* consts,blocks *)
 
62
  | Kpushfields of int 
 
63
  | Kfield of int
 
64
  | Ksetfield of int
 
65
  | Kstop
 
66
  | Ksequence of bytecodes * bytecodes
 
67
(* spiwack: instructions concerning integers *)
 
68
  | Kbranch of Label.t                  (* jump to label *)
 
69
  | Kaddint31                           (* adds the int31 in the accu 
 
70
                                           and the one ontop of the stack *)
 
71
  | Kaddcint31                          (* makes the sum and keeps the carry *)
 
72
  | Kaddcarrycint31                     (* sum +1, keeps the carry *)
 
73
  | Ksubint31                           (* subtraction modulo *)
 
74
  | Ksubcint31                          (* subtraction, keeps the carry *)
 
75
  | Ksubcarrycint31                      (* subtraction -1, keeps the carry *)
 
76
  | Kmulint31                           (* multiplication modulo *)
 
77
  | Kmulcint31                          (* multiplication, result in two
 
78
                                           int31, for exact computation *)
 
79
  | Kdiv21int31                          (* divides a double size integer
 
80
                                           (represented by an int31 in the 
 
81
                                           accumulator and one on the top of 
 
82
                                           the stack) by an int31. The result
 
83
                                           is a pair of the quotient and the 
 
84
                                           rest.
 
85
                                           If the divisor is 0, it returns
 
86
                                           0. *)
 
87
  | Kdivint31                           (* euclidian division (returns a pair
 
88
                                           quotient,rest) *)
 
89
  | Kaddmuldivint31                     (* generic operation for shifting and
 
90
                                           cycling. Takes 3 int31 i j and s,
 
91
                                           and returns x*2^s+y/(2^(31-s) *)
 
92
  | Kcompareint31                       (* unsigned comparison of int31
 
93
                                           cf COMPAREINT31 in 
 
94
                                           kernel/byterun/coq_interp.c
 
95
                                           for more info *)
 
96
  | Khead0int31                         (* Give the numbers of 0 in head of a in31*)
 
97
  | Ktail0int31                         (* Give the numbers of 0 in tail of a in31 
 
98
                                           ie low bits *)
 
99
  | Kisconst of Label.t                 (* conditional jump *)
 
100
  | Kareconst of int*Label.t            (* conditional jump *)
 
101
  | Kcompint31                          (* dynamic compilation of int31 *)
 
102
  | Kdecompint31                        (* dynamic decompilation of int31 *)
 
103
(* /spiwack *)
 
104
 
 
105
and bytecodes = instruction list
 
106
 
 
107
type fv_elem = FVnamed of identifier | FVrel of int
 
108
 
 
109
type fv = fv_elem array
 
110
 
 
111
(* spiwack: this exception is expected to be raised by function expecting
 
112
            closed terms. *)
 
113
exception NotClosed
 
114
 
 
115
 
 
116
(*spiwack: both type have been moved from Cbytegen because I needed then
 
117
  for the retroknowledge *)
 
118
type vm_env = {
 
119
    size : int;              (* longueur de la liste [n] *)
 
120
    fv_rev : fv_elem list    (* [fvn; ... ;fv1] *)
 
121
  }    
 
122
   
 
123
   
 
124
type comp_env = { 
 
125
    nb_stack : int;              (* nbre de variables sur la pile          *)
 
126
    in_stack : int list;         (* position dans la pile                  *)
 
127
    nb_rec : int;                (* nbre de fonctions mutuellement         *)
 
128
                                 (* recursives =  nbr                      *)
 
129
    pos_rec  : instruction list; (* instruction d'acces pour les variables *)
 
130
                                 (*  de point fix ou de cofix              *)
 
131
    offset : int;                 
 
132
    in_env : vm_env ref 
 
133
  } 
 
134
 
 
135
 
 
136
 
 
137
(* --- Pretty print *)
 
138
open Format
 
139
let rec instruction ppf = function
 
140
  | Klabel lbl -> fprintf ppf "L%i:" lbl
 
141
  | Kacc n -> fprintf ppf "\tacc %i" n
 
142
  | Kenvacc n -> fprintf ppf "\tenvacc %i" n
 
143
  | Koffsetclosure n -> fprintf ppf "\toffsetclosure %i" n
 
144
  | Kpush -> fprintf ppf "\tpush"
 
145
  | Kpop n -> fprintf ppf "\tpop %i" n
 
146
  | Kpush_retaddr lbl -> fprintf ppf "\tpush_retaddr L%i" lbl
 
147
  | Kapply n -> fprintf ppf "\tapply %i" n
 
148
  | Kappterm(n, m) ->
 
149
      fprintf ppf "\tappterm %i, %i" n m
 
150
  | Kreturn n -> fprintf ppf "\treturn %i" n
 
151
  | Kjump -> fprintf ppf "\tjump"
 
152
  | Krestart -> fprintf ppf "\trestart"
 
153
  | Kgrab n -> fprintf ppf "\tgrab %i" n
 
154
  | Kgrabrec n -> fprintf ppf "\tgrabrec %i" n
 
155
  | Kclosure(lbl, n) ->
 
156
      fprintf ppf "\tclosure L%i, %i" lbl n
 
157
  | Kclosurerec(fv,init,lblt,lblb) ->
 
158
      fprintf ppf "\tclosurerec";
 
159
      fprintf ppf "%i , %i, " fv init;
 
160
      print_string "types = ";
 
161
      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblt;
 
162
      print_string " bodies = ";
 
163
      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb;
 
164
  | Kclosurecofix (fv,init,lblt,lblb) ->
 
165
      fprintf ppf "\tclosurecofix";
 
166
      fprintf ppf " %i , %i, " fv init;
 
167
      print_string "types = ";
 
168
      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblt;
 
169
      print_string " bodies = ";
 
170
      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb;
 
171
  | Kgetglobal id -> fprintf ppf "\tgetglobal %s" (Names.string_of_con id)
 
172
  | Kconst cst ->
 
173
      fprintf ppf "\tconst"
 
174
  | Kmakeblock(n, m) ->
 
175
      fprintf ppf "\tmakeblock %i, %i" n m
 
176
  | Kmakeprod -> fprintf ppf "\tmakeprod"
 
177
  | Kmakeswitchblock(lblt,lbls,_,sz) ->
 
178
      fprintf ppf "\tmakeswitchblock %i, %i, %i" lblt lbls sz
 
179
  | Kswitch(lblc,lblb) -> 
 
180
      fprintf ppf "\tswitch";
 
181
      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblc;
 
182
      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb;
 
183
  | Kpushfields n -> fprintf ppf "\tpushfields %i" n
 
184
  | Ksetfield n -> fprintf ppf "\tsetfield %i" n
 
185
  | Kfield  n -> fprintf ppf "\tgetfield %i" n
 
186
  | Kstop -> fprintf ppf "\tstop"
 
187
  | Ksequence (c1,c2) ->
 
188
      fprintf ppf "%a@ %a" instruction_list c1 instruction_list c2 
 
189
(* spiwack *)
 
190
  | Kbranch lbl -> fprintf ppf "\tbranch %i" lbl
 
191
  | Kaddint31 -> fprintf ppf "\taddint31"
 
192
  | Kaddcint31 -> fprintf ppf "\taddcint31"
 
193
  | Kaddcarrycint31 -> fprintf ppf "\taddcarrycint31"
 
194
  | Ksubint31 -> fprintf ppf "\tsubint31"
 
195
  | Ksubcint31 -> fprintf ppf "\tsubcint31"
 
196
  | Ksubcarrycint31 -> fprintf ppf "\tsubcarrycint31"
 
197
  | Kmulint31 -> fprintf ppf "\tmulint31"
 
198
  | Kmulcint31 -> fprintf ppf "\tmulcint31"
 
199
  | Kdiv21int31 -> fprintf ppf "\tdiv21int31"
 
200
  | Kdivint31 -> fprintf ppf "\tdivint31"
 
201
  | Kcompareint31 -> fprintf ppf "\tcompareint31"
 
202
  | Khead0int31 -> fprintf ppf "\thead0int31"
 
203
  | Ktail0int31 -> fprintf ppf "\ttail0int31"
 
204
  | Kaddmuldivint31 -> fprintf ppf "\taddmuldivint31"
 
205
  | Kisconst lbl -> fprintf ppf "\tisconst %i" lbl
 
206
  | Kareconst(n,lbl) -> fprintf ppf "\tareconst %i %i" n lbl
 
207
  | Kcompint31 -> fprintf ppf "\tcompint31"
 
208
  | Kdecompint31 -> fprintf ppf "\tdecompint"
 
209
 
 
210
(* /spiwack *)
 
211
 
 
212
 
 
213
and instruction_list ppf = function
 
214
    [] -> ()
 
215
  | Klabel lbl :: il ->
 
216
      fprintf ppf "L%i:%a" lbl instruction_list il
 
217
  | instr :: il ->
 
218
      fprintf ppf "%a@ %a" instruction instr instruction_list il
 
219
 
 
220
 
 
221
(*spiwack: moved this type in this file  because I needed it for 
 
222
  retroknowledge which can't depend from cbytegen *)
 
223
type block = 
 
224
  | Bconstr of constr
 
225
  | Bstrconst of structured_constant
 
226
  | Bmakeblock of int * block array
 
227
  | Bconstruct_app of int * int * int * block array
 
228
                  (* tag , nparams, arity *)
 
229
  | Bspecial of (comp_env -> block array -> int -> bytecodes -> bytecodes) * block array
 
230
                (* spiwack: compilation given by a function *)
 
231
                (* compilation function (see get_vm_constant_dynamic_info in 
 
232
                   retroknowledge.mli for more info) , argument array  *)
 
233
 
 
234
 
 
235
 
 
236
let draw_instr c =
 
237
  fprintf std_formatter "@[<v 0>%a@]" instruction_list c