← Back to branch summary

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

« back to all changes in this revision

Viewing changes to toplevel/discharge.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:
toplevel/discharge.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: discharge.ml 10861 2008-04-28 08:19:14Z herbelin $ *)
 
10
 
 
11
open Names
 
12
open Util
 
13
open Sign
 
14
open Term
 
15
open Entries
 
16
open Declarations
 
17
open Cooking
 
18
 
 
19
(********************************)
 
20
(* Discharging mutual inductive *)
 
21
 
 
22
let detype_param = function
 
23
  | (Name id,None,p) -> id, Entries.LocalAssum p
 
24
  | (Name id,Some p,_) -> id, Entries.LocalDef p
 
25
  | (Anonymous,_,_) -> anomaly"Unnamed inductive local variable"
 
26
 
 
27
(* Replace
 
28
 
 
29
     Var(y1)..Var(yq):C1..Cq |- Ij:Bj
 
30
     Var(y1)..Var(yq):C1..Cq; I1..Ip:B1..Bp |- ci : Ti
 
31
 
 
32
   by
 
33
 
 
34
     |- Ij: (y1..yq:C1..Cq)Bj
 
35
     I1..Ip:(B1 y1..yq)..(Bp y1..yq) |- ci : (y1..yq:C1..Cq)Ti[Ij:=(Ij y1..yq)]
 
36
*)
 
37
 
 
38
let abstract_inductive hyps nparams inds =
 
39
  let ntyp = List.length inds in 
 
40
  let nhyp = named_context_length hyps in
 
41
  let args = instance_from_named_context (List.rev hyps) in
 
42
  let subs = list_tabulate (fun k -> lift nhyp (mkApp(mkRel (k+1),args))) ntyp in
 
43
  let inds' =
 
44
    List.map
 
45
      (function (tname,arity,cnames,lc) -> 
 
46
        let lc' = List.map (substl subs) lc in
 
47
        let lc'' = List.map (fun b -> Termops.it_mkNamedProd_wo_LetIn b hyps) lc' in
 
48
        let arity' = Termops.it_mkNamedProd_wo_LetIn arity hyps in
 
49
        (tname,arity',cnames,lc''))
 
50
        inds in
 
51
  let nparams' = nparams + Array.length args in
 
52
(* To be sure to be the same as before, should probably be moved to process_inductive *) 
 
53
  let params' = let (_,arity,_,_) = List.hd inds' in 
 
54
                let (params,_) = decompose_prod_n_assum nparams' arity in
 
55
                  List.map detype_param params
 
56
  in
 
57
  let ind'' = 
 
58
  List.map 
 
59
    (fun (a,arity,c,lc) ->
 
60
      let _, short_arity = decompose_prod_n_assum nparams' arity in
 
61
      let shortlc =
 
62
        List.map (fun c -> snd (decompose_prod_n_assum nparams' c)) lc in
 
63
      { mind_entry_typename = a;
 
64
        mind_entry_arity = short_arity;
 
65
        mind_entry_consnames = c;
 
66
        mind_entry_lc = shortlc })
 
67
    inds'
 
68
  in (params',ind'')
 
69
 
 
70
 
 
71
let process_inductive sechyps modlist mib =
 
72
  let nparams = mib.mind_nparams in
 
73
  let inds = 
 
74
    array_map_to_list
 
75
      (fun mip ->
 
76
         let arity = expmod_constr modlist (Termops.refresh_universes_strict (Inductive.type_of_inductive (Global.env()) (mib,mip))) in
 
77
         let lc = Array.map (expmod_constr modlist) mip.mind_user_lc in
 
78
         (mip.mind_typename,
 
79
          arity,
 
80
          Array.to_list mip.mind_consnames,
 
81
          Array.to_list lc))
 
82
      mib.mind_packets in
 
83
  let sechyps' = map_named_context (expmod_constr modlist) sechyps in
 
84
  let (params',inds') = abstract_inductive sechyps' nparams inds in
 
85
  { mind_entry_record = mib.mind_record;
 
86
    mind_entry_finite = mib.mind_finite;
 
87
    mind_entry_params = params';
 
88
    mind_entry_inds = inds' }