← Back to branch summary

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

« back to all changes in this revision

Viewing changes to contrib/interface/translate.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:
contrib/interface/translate.ml
 
1
open Names;;
 
2
open Sign;;
 
3
open Util;;
 
4
open Term;;
 
5
open Pp;;
 
6
open Libobject;;
 
7
open Library;;
 
8
open Vernacinterp;;
 
9
open Tacmach;;
 
10
open Pfedit;;
 
11
open Parsing;;
 
12
open Evd;;
 
13
open Evarutil;;
 
14
 
 
15
open Xlate;;
 
16
open Vtp;;
 
17
open Ascent;;
 
18
open Environ;;
 
19
open Proof_type;;
 
20
 
 
21
(*translates a formula into a centaur-tree --> FORMULA *)
 
22
let translate_constr at_top env c =
 
23
  xlate_formula (Constrextern.extern_constr at_top env c);;
 
24
 
 
25
(*translates a named_context into a centaur-tree --> PREMISES_LIST *)
 
26
(* this code is inspired from printer.ml (function pr_named_context_of) *)
 
27
let translate_sign env =
 
28
  let l = 
 
29
    Environ.fold_named_context
 
30
      (fun env (id,v,c) l -> 
 
31
         (match v with
 
32
              None ->
 
33
                CT_premise(CT_ident(string_of_id id), translate_constr false env c)
 
34
            | Some v1 ->
 
35
                CT_eval_result
 
36
                  (CT_coerce_ID_to_FORMULA (CT_ident (string_of_id id)),
 
37
                   translate_constr false env v1,
 
38
                   translate_constr false env c))::l)
 
39
      env ~init:[] 
 
40
  in
 
41
  CT_premises_list l;;
 
42
       
 
43
(* the function rev_and_compact performs two operations:
 
44
   1- it reverses the list of integers given as argument
 
45
   2- it replaces sequences of "1" by a negative number that is
 
46
      the length of the sequence. *)
 
47
let rec rev_and_compact l = function
 
48
    [] -> l
 
49
  | 1::tl -> 
 
50
      (match l with
 
51
              n::tl' -> 
 
52
        if n < 0 then
 
53
          rev_and_compact ((n - 1)::tl') tl
 
54
        else
 
55
          rev_and_compact ((-1)::l) tl
 
56
      |       [] -> rev_and_compact [-1] tl)
 
57
  | a::tl ->
 
58
      if a < 0 then
 
59
      (match l with
 
60
        n::tl' ->
 
61
          if n < 0 then
 
62
            rev_and_compact ((n + a)::tl') tl
 
63
          else
 
64
            rev_and_compact (a::l) tl
 
65
      | [] -> rev_and_compact (a::l) tl)
 
66
      else
 
67
      rev_and_compact (a::l) tl;;
 
68
 
 
69
(*translates an int list into a centaur-tree --> SIGNED_INT_LIST *)
 
70
let translate_path l =
 
71
 CT_signed_int_list
 
72
 (List.map (function n -> CT_coerce_INT_to_SIGNED_INT (CT_int n))
 
73
    (rev_and_compact [] l));;
 
74
 
 
75
(*translates a path and a goal into a centaur-tree --> RULE *)
 
76
let translate_goal (g:goal) =
 
77
 CT_rule(translate_sign (evar_env g), translate_constr true (evar_env g) g.evar_concl);;
 
78
 
 
79
let translate_goals (gl: goal list) =
 
80
 CT_rule_list (List.map translate_goal gl);;