← Back to branch summary

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

« back to all changes in this revision

Viewing changes to kernel/vm.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/vm.mli
 
1
open Names
 
2
open Term
 
3
open Cbytecodes
 
4
open Cemitcodes
 
5
 
 
6
 
 
7
val set_drawinstr : unit -> unit
 
8
 
 
9
val transp_values : unit -> bool
 
10
val set_transp_values : bool -> unit
 
11
(* le code machine *)
 
12
type tcode 
 
13
 
 
14
(* Les valeurs ***********)
 
15
 
 
16
type vprod 
 
17
type vfun
 
18
type vfix
 
19
type vcofix
 
20
type vblock
 
21
type vswitch
 
22
type arguments
 
23
 
 
24
type atom = 
 
25
  | Aid of id_key
 
26
  | Aiddef of id_key * values
 
27
  | Aind of inductive
 
28
 
 
29
(* Les zippers *)
 
30
 
 
31
type zipper =
 
32
  | Zapp of arguments
 
33
  | Zfix of vfix*arguments  (* Peut-etre vide *)
 
34
  | Zswitch of vswitch
 
35
 
 
36
type stack = zipper list
 
37
 
 
38
type to_up
 
39
 
 
40
type whd =
 
41
  | Vsort of sorts
 
42
  | Vprod of vprod 
 
43
  | Vfun of vfun
 
44
  | Vfix of vfix * arguments option
 
45
  | Vcofix of vcofix * to_up * arguments option
 
46
  | Vconstr_const of int
 
47
  | Vconstr_block of vblock
 
48
  | Vatom_stk of atom * stack
 
49
 
 
50
(** Constructors *)
 
51
val val_of_str_const : structured_constant -> values
 
52
 
 
53
val val_of_rel : int -> values 
 
54
val val_of_rel_def : int -> values -> values 
 
55
 
 
56
val val_of_named : identifier -> values
 
57
val val_of_named_def : identifier -> values -> values
 
58
 
 
59
val val_of_constant : constant -> values 
 
60
val val_of_constant_def : int -> constant -> values -> values
 
61
 
 
62
(** Destructors *)
 
63
val whd_val : values -> whd
 
64
 
 
65
(* Arguments *)  
 
66
val nargs : arguments -> int
 
67
val arg : arguments -> int -> values
 
68
 
 
69
(* Product *)
 
70
val dom : vprod -> values
 
71
val codom : vprod -> vfun
 
72
 
 
73
(* Function *)
 
74
val body_of_vfun : int -> vfun -> values 
 
75
val decompose_vfun2  : int -> vfun -> vfun -> int * values * values
 
76
 
 
77
(* Fix *)
 
78
val current_fix : vfix -> int
 
79
val check_fix : vfix -> vfix -> bool
 
80
val rec_args : vfix -> int array 
 
81
val reduce_fix : int -> vfix -> vfun array * values array
 
82
                              (* bodies ,  types *)
 
83
 
 
84
(* CoFix *)
 
85
val current_cofix : vcofix -> int 
 
86
val check_cofix : vcofix -> vcofix -> bool
 
87
val reduce_cofix : int -> vcofix -> values array * values array
 
88
                                      (* bodies , types *)
 
89
(* Block *)
 
90
val btag : vblock -> int
 
91
val bsize : vblock -> int
 
92
val bfield : vblock -> int -> values
 
93
 
 
94
(* Switch *)
 
95
val check_switch : vswitch -> vswitch -> bool
 
96
val case_info : vswitch -> case_info
 
97
val type_of_switch : vswitch -> values
 
98
val branch_of_switch : int -> vswitch -> (int * values) array
 
99
 
 
100
(* Evaluation *)
 
101
val whd_stack : values -> stack -> whd
 
102
val force_whd : values -> stack -> whd
 
103
 
 
104