← Back to branch summary

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

« back to all changes in this revision

Viewing changes to plugins/extraction/table.ml

  • Committer: Package Import Robot
  • Author(s): Stéphane Glondu
  • Date: 2012-01-03 23:42:48 UTC
  • mfrom: (1.2.4)
  • Revision ID: package-import@ubuntu.com-20120103234248-p9r8h1579n67v55a
Tags: 8.3pl3-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
plugins/extraction/table.ml
1
1
(************************************************************************)
2
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
3
 
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 
3
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
4
4
(*   \VV/  **************************************************************)
5
5
(*    //   *      This file is distributed under the terms of the       *)
6
6
(*         *       GNU Lesser General Public License Version 2.1        *)
7
7
(************************************************************************)
8
8
 
9
 
(*i $Id: table.ml 14012 2011-04-15 16:45:27Z letouzey $ i*)
 
9
(*i $Id: table.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
10
10
 
11
11
open Names
12
12
open Term
21
21
open Pp
22
22
open Miniml
23
23
 
24
 
(** Sets and maps for [global_reference] that do _not_ work modulo
25
 
    name equivalence (otherwise use Refset / Refmap ) *)
26
 
 
27
 
module RefOrd = struct type t = global_reference let compare = compare end
 
24
(** Sets and maps for [global_reference] that work modulo equivalent
 
25
    on the user part of the name (otherwise use Refset / Refmap ) *)
 
26
 
 
27
module RefOrd = struct
 
28
  type t = global_reference
 
29
  let compare x y =
 
30
    let make_name = function
 
31
      | ConstRef con -> ConstRef(constant_of_kn(user_con con))
 
32
      | IndRef (kn,i) -> IndRef(mind_of_kn(user_mind kn),i)
 
33
      | ConstructRef ((kn,i),j)-> ConstructRef((mind_of_kn(user_mind kn),i),j)
 
34
      | VarRef id -> VarRef id
 
35
    in
 
36
    Pervasives.compare (make_name x) (make_name y)
 
37
end
 
38
 
28
39
module Refmap' = Map.Make(RefOrd)
29
40
module Refset' = Set.Make(RefOrd)
30
41
 
316
327
       ++ str "some Declare Module outside any Module Type.\n"
317
328
       ++ str "This situation is currently unsupported by the extraction.")
318
329
 
 
330
let error_singleton_become_prop id =
 
331
  err (str "The informative inductive type " ++ pr_id id ++
 
332
       str " has a Prop instance.\n" ++
 
333
       str "This happens when a sort-polymorphic singleton inductive type\n" ++
 
334
       str "has logical parameters, such as (I,I) : (True * True) : Prop.\n" ++
 
335
       str "The Ocaml extraction cannot handle this situation yet.\n" ++
 
336
       str "Instead, use a sort-monomorphic type such as (True /\\ True)\n" ++
 
337
       str "or extract to Haskell.")
 
338
 
319
339
let error_unknown_module m =
320
340
  err (str "Module" ++ spc () ++ pr_qualid m ++ spc () ++ str "not found.")
321
341
 
335
355
            "Monolithic Extraction cannot deal with this situation.\n"^
336
356
            "Please "^s2^"use (Recursive) Extraction Library instead.\n"))
337
357
 
338
 
let error_record r =
339
 
  err (str "Record " ++ safe_pr_global r ++ str " has an anonymous field." ++
340
 
       fnl () ++ str "To help extraction, please use an explicit name.")
341
 
 
342
358
let msg_non_implicit r n id =
343
359
  let name = match id with
344
360
    | Anonymous -> ""