← Back to branch summary

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

« back to all changes in this revision

Viewing changes to checker/validate.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:
checker/validate.ml
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(* $Id$ *)
 
10
 
 
11
(* This module defines validation functions to ensure an imported
 
12
   value (using input_value) has the correct structure. *)
 
13
 
 
14
let rec pr_obj_rec o =
 
15
  if Obj.is_int o then
 
16
    Format.print_int(Obj.magic o)
 
17
  else if Obj.is_block o then
 
18
    let t = Obj.tag o in
 
19
    if t > Obj.no_scan_tag then
 
20
      if t = Obj.string_tag then
 
21
        Format.print_string ("\""^String.escaped(Obj.magic o)^"\"")
 
22
      else
 
23
        Format.print_string "?"
 
24
    else
 
25
      (let n = Obj.size o in
 
26
      Format.print_string ("#"^string_of_int t^"(");
 
27
      Format.open_hvbox 0;
 
28
      for i = 0 to n-1 do
 
29
        pr_obj_rec (Obj.field o i);
 
30
        if i<>n-1 then (Format.print_string ","; Format.print_cut())
 
31
      done;
 
32
      Format.close_box();
 
33
      Format.print_string ")")
 
34
  else Format.print_string "?"
 
35
 
 
36
let pr_obj o = pr_obj_rec o; Format.print_newline()
 
37
 
 
38
(**************************************************************************)
 
39
(* Obj low-level validators *)
 
40
 
 
41
exception ValidObjError of string * Obj.t
 
42
let fail o s = raise (ValidObjError(s,o))
 
43
 
 
44
let apply debug f x =
 
45
  let o = Obj.repr x in
 
46
  try f o
 
47
  with ValidObjError(msg,obj) ->
 
48
    if debug then begin
 
49
      print_endline ("Validation failed: "^msg);
 
50
      pr_obj obj
 
51
    end;
 
52
    failwith "validation failed"
 
53
 
 
54
(* data not validated *)
 
55
let no_val (o:Obj.t) = ()
 
56
 
 
57
(* Check that object o is a block with tag t *)
 
58
let val_tag t o =
 
59
  if Obj.is_block o && Obj.tag o = t then ()
 
60
  else fail o ("expected tag "^string_of_int t)
 
61
 
 
62
let val_block s o =
 
63
  if Obj.is_block o then
 
64
    (if Obj.tag o > Obj.no_scan_tag then
 
65
      fail o (s^": found no scan tag"))
 
66
  else fail o (s^": expected block obj")
 
67
 
 
68
(* Check that an object is a tuple (or a record). v is an array of
 
69
   validation functions for each field. Its size corresponds to the
 
70
   expected size of the object. *)
 
71
let val_tuple s v o =
 
72
  let n = Array.length v in
 
73
  val_block ("tuple: "^s) o;
 
74
  if Obj.size o = n then
 
75
    Array.iteri (fun i f -> f (Obj.field o i)) v
 
76
  else
 
77
    fail o ("tuple:" ^s^" size found:"^string_of_int (Obj.size o))
 
78
 
 
79
(* Check that the object is either a constant constructor of tag < cc,
 
80
   or a constructed variant. each element of vv is an array of
 
81
   validation functions to be applied to the constructor arguments.
 
82
   The size of vv corresponds to the number of non-constant
 
83
   constructors, and the size of vv.(i) is the expected arity of the
 
84
   i-th non-constant constructor. *)
 
85
let val_sum s cc vv o =
 
86
  if Obj.is_block o then
 
87
    (val_block s o;
 
88
    let n = Array.length vv in
 
89
    let i = Obj.tag o in
 
90
    if i < n then val_tuple (s^"(tag "^string_of_int i^")") vv.(i) o
 
91
    else fail o ("bad tag in (sum type) "^s^": max is "^string_of_int i))
 
92
  else if Obj.is_int o then
 
93
    let (n:int) = Obj.magic o in
 
94
    (if n<0 || n>=cc then
 
95
      fail o (s^": bad constant constructor "^string_of_int n))
 
96
  else fail o ("not a sum ("^s^")")
 
97
 
 
98
let val_enum s n = val_sum s n [||]
 
99
 
 
100
(* Recursive types: avoid looping by eta-expansion *)
 
101
let rec val_rec_sum s cc f o =
 
102
  val_sum s cc (f (val_rec_sum s cc f)) o
 
103
 
 
104
let rec val_rectype f o =
 
105
  f (val_rectype f) o
 
106
 
 
107
(**************************************************************************)
 
108
(* Builtin types *)
 
109
 
 
110
(* Check the o is an array of values satisfying f. *)
 
111
let val_array ?(name="array") f o =
 
112
  val_block name o;
 
113
  for i = 0 to Obj.size o - 1 do
 
114
    (f (Obj.field o i):unit)
 
115
  done
 
116
 
 
117
(* Integer validator *)
 
118
let val_int o =
 
119
  if not (Obj.is_int o) then fail o "expected an int"
 
120
 
 
121
(* String validator *)
 
122
let val_str o =
 
123
  try val_tag Obj.string_tag o
 
124
  with Failure _ -> fail o "expected a string"
 
125
 
 
126
(* Booleans *)
 
127
let val_bool = val_enum "bool" 2
 
128
 
 
129
(* Option type *)
 
130
let val_opt ?(name="option") f = val_sum name 1 [|[|f|]|]
 
131
 
 
132
(* Lists *)
 
133
let val_list ?(name="list") f =
 
134
  val_rec_sum name 1 (fun vlist -> [|[|f;vlist|]|])
 
135
 
 
136
(* Reference *)
 
137
let val_ref ?(name="ref") f = val_tuple name [|f|]
 
138
 
 
139
(**************************************************************************)
 
140
(* Standard library types *)
 
141
 
 
142
(* Sets *)
 
143
let val_set ?(name="Set.t") f =
 
144
  val_rec_sum name 1 (fun vset -> [|[|vset;f;vset;val_int|]|])
 
145
 
 
146
(* Maps *)
 
147
let rec val_map ?(name="Map.t") fk fv =
 
148
  val_rec_sum name 1 (fun vmap -> [|[|vmap;fk;fv;vmap;val_int|]|])
 
149
 
 
150
(**************************************************************************)
 
151
(* Coq types *)
 
152
 
 
153
(* names *)
 
154
let val_id = val_str
 
155
 
 
156
let val_dp = val_list ~name:"dirpath" val_id
 
157
 
 
158
let val_name = val_sum "name" 1 [|[|val_id|]|]
 
159
 
 
160
let val_uid = val_tuple "uniq_ident" [|val_int;val_str;val_dp|]
 
161
 
 
162
let val_mp =
 
163
  val_rec_sum "module_path" 0
 
164
    (fun vmp -> [|[|val_dp|];[|val_uid|];[|val_uid|];[|vmp;val_id|]|])
 
165
 
 
166
let val_kn = val_tuple "kernel_name" [|val_mp;val_dp;val_id|]
 
167
 
 
168
let val_ind = val_tuple "inductive"[|val_kn;val_int|]
 
169
let val_cstr = val_tuple "constructor"[|val_ind;val_int|]
 
170
 
 
171
(* univ *)
 
172
let val_level = val_sum "level" 1 [|[|val_dp;val_int|]|]
 
173
let val_univ = val_sum "univ" 0
 
174
  [|[|val_level|];[|val_list val_level;val_list val_level|]|]
 
175
 
 
176
let val_cstrs =
 
177
  val_set ~name:"Univ.constraints"
 
178
   (val_tuple "univ_constraint"
 
179
     [|val_level;val_enum "order_request" 3;val_level|])