← Back to branch summary

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

« back to all changes in this revision

Viewing changes to contrib/firstorder/instances.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/firstorder/instances.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
(*i $Id: instances.ml 10410 2007-12-31 13:11:55Z msozeau $ i*)
 
10
 
 
11
open Formula
 
12
open Sequent
 
13
open Unify
 
14
open Rules
 
15
open Util
 
16
open Term
 
17
open Rawterm
 
18
open Tacmach
 
19
open Tactics
 
20
open Tacticals
 
21
open Termops
 
22
open Reductionops
 
23
open Declarations
 
24
open Formula
 
25
open Sequent
 
26
open Names
 
27
open Libnames
 
28
 
 
29
let compare_instance inst1 inst2=
 
30
        match inst1,inst2 with
 
31
            Phantom(d1),Phantom(d2)->
 
32
              (OrderedConstr.compare d1 d2)
 
33
          | Real((m1,c1),n1),Real((m2,c2),n2)->
 
34
              ((-) =? (-) ==? OrderedConstr.compare) m2 m1 n1 n2 c1 c2
 
35
          | Phantom(_),Real((m,_),_)-> if m=0 then -1 else 1
 
36
          | Real((m,_),_),Phantom(_)-> if m=0 then 1 else -1
 
37
 
 
38
let compare_gr id1 id2=
 
39
  if id1==id2 then 0 else
 
40
    if id1==dummy_id then 1 
 
41
    else if id2==dummy_id then -1 
 
42
    else Pervasives.compare id1 id2
 
43
 
 
44
module OrderedInstance=
 
45
struct
 
46
  type t=instance * Libnames.global_reference
 
47
  let compare (inst1,id1) (inst2,id2)=
 
48
    (compare_instance =? compare_gr) inst2 inst1 id2 id1
 
49
    (* we want a __decreasing__ total order *)
 
50
end
 
51
  
 
52
module IS=Set.Make(OrderedInstance)
 
53
 
 
54
let make_simple_atoms seq=
 
55
  let ratoms=
 
56
    match seq.glatom with
 
57
        Some t->[t]
 
58
      | None->[]
 
59
  in {negative=seq.latoms;positive=ratoms}
 
60
 
 
61
let do_sequent setref triv id seq i dom atoms=
 
62
  let flag=ref true in
 
63
  let phref=ref triv in
 
64
  let do_atoms a1 a2 =
 
65
    let do_pair t1 t2 = 
 
66
      match unif_atoms i dom t1 t2 with
 
67
          None->()
 
68
        | Some (Phantom _) ->phref:=true
 
69
        | Some c ->flag:=false;setref:=IS.add (c,id) !setref in
 
70
      List.iter (fun t->List.iter (do_pair t) a2.negative) a1.positive;
 
71
      List.iter (fun t->List.iter (do_pair t) a2.positive) a1.negative in
 
72
    HP.iter (fun lf->do_atoms atoms lf.atoms) seq.redexes;
 
73
    do_atoms atoms (make_simple_atoms seq);
 
74
    !flag && !phref 
 
75
 
 
76
let match_one_quantified_hyp setref seq lf=
 
77
  match lf.pat with 
 
78
      Left(Lforall(i,dom,triv))|Right(Rexists(i,dom,triv))->
 
79
        if do_sequent setref triv lf.id seq i dom lf.atoms then
 
80
          setref:=IS.add ((Phantom dom),lf.id) !setref 
 
81
    | _ ->anomaly "can't happen" 
 
82
 
 
83
let give_instances lf seq=
 
84
  let setref=ref IS.empty in
 
85
    List.iter (match_one_quantified_hyp setref seq) lf;
 
86
    IS.elements !setref
 
87
                  
 
88
(* collector for the engine *)
 
89
 
 
90
let rec collect_quantified seq=
 
91
  try
 
92
    let hd,seq1=take_formula seq in
 
93
      (match hd.pat with 
 
94
           Left(Lforall(_,_,_)) | Right(Rexists(_,_,_)) -> 
 
95
             let (q,seq2)=collect_quantified seq1 in
 
96
               ((hd::q),seq2)
 
97
         | _->[],seq)
 
98
  with Heap.EmptyHeap -> [],seq
 
99
 
 
100
(* open instances processor *)
 
101
 
 
102
let dummy_constr=mkMeta (-1)
 
103
 
 
104
let dummy_bvid=id_of_string "x"
 
105
 
 
106
let mk_open_instance id gl m t=
 
107
  let env=pf_env gl in
 
108
  let evmap=Refiner.project gl in
 
109
  let var_id=
 
110
    if id==dummy_id then dummy_bvid else
 
111
      let typ=pf_type_of gl (constr_of_global id) in
 
112
        (* since we know we will get a product, 
 
113
           reduction is not too expensive *)
 
114
      let (nam,_,_)=destProd (whd_betadeltaiota env evmap typ) in
 
115
        match nam with 
 
116
            Name id -> id
 
117
          | Anonymous ->  dummy_bvid in
 
118
  let revt=substl (list_tabulate (fun i->mkRel (m-i)) m) t in
 
119
  let rec aux n avoid=
 
120
    if n=0 then [] else
 
121
      let nid=(fresh_id avoid var_id gl) in
 
122
        (Name nid,None,dummy_constr)::(aux (n-1) (nid::avoid)) in
 
123
  let nt=it_mkLambda_or_LetIn revt (aux m []) in
 
124
  let rawt=Detyping.detype false [] [] nt in
 
125
  let rec raux n t=
 
126
    if n=0 then t else 
 
127
      match t with
 
128
          RLambda(loc,name,k,_,t0)->
 
129
            let t1=raux (n-1) t0 in
 
130
              RLambda(loc,name,k,RHole (dummy_loc,Evd.BinderType name),t1)
 
131
        | _-> anomaly "can't happen" in
 
132
  let ntt=try 
 
133
    Pretyping.Default.understand evmap env (raux m rawt)
 
134
  with _ -> 
 
135
    error "Untypable instance, maybe higher-order non-prenex quantification" in
 
136
    Sign.decompose_lam_n_assum m ntt
 
137
 
 
138
(* tactics   *)
 
139
 
 
140
let left_instance_tac (inst,id) continue seq=
 
141
  match inst with
 
142
      Phantom dom->
 
143
        if lookup (id,None) seq then 
 
144
          tclFAIL 0 (Pp.str "already done")
 
145
        else
 
146
          tclTHENS (cut dom) 
 
147
            [tclTHENLIST
 
148
               [introf;
 
149
                (fun gls->generalize 
 
150
                   [mkApp(constr_of_global id,
 
151
                          [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls);
 
152
                introf;
 
153
                tclSOLVE [wrap 1 false continue 
 
154
                            (deepen (record (id,None) seq))]];
 
155
            tclTRY assumption]
 
156
    | Real((m,t) as c,_)->
 
157
        if lookup (id,Some c) seq then 
 
158
          tclFAIL 0 (Pp.str "already done")
 
159
        else 
 
160
          let special_generalize=
 
161
            if m>0 then 
 
162
              fun gl-> 
 
163
                let (rc,ot)= mk_open_instance id gl m t in
 
164
                let gt= 
 
165
                  it_mkLambda_or_LetIn 
 
166
                    (mkApp(constr_of_global id,[|ot|])) rc in
 
167
                  generalize [gt] gl
 
168
            else
 
169
              generalize [mkApp(constr_of_global id,[|t|])]
 
170
          in
 
171
            tclTHENLIST 
 
172
              [special_generalize;
 
173
               introf; 
 
174
               tclSOLVE 
 
175
                 [wrap 1 false continue (deepen (record (id,Some c) seq))]]
 
176
              
 
177
let right_instance_tac inst continue seq=
 
178
  match inst with
 
179
      Phantom dom ->
 
180
        tclTHENS (cut dom) 
 
181
        [tclTHENLIST
 
182
           [introf;
 
183
            (fun gls->
 
184
               split (Rawterm.ImplicitBindings 
 
185
                        [mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls);
 
186
            tclSOLVE [wrap 0 true continue (deepen seq)]];
 
187
         tclTRY assumption] 
 
188
    | Real ((0,t),_) ->
 
189
        (tclTHEN (split (Rawterm.ImplicitBindings [t]))
 
190
           (tclSOLVE [wrap 0 true continue (deepen seq)]))
 
191
    | Real ((m,t),_) ->
 
192
        tclFAIL 0 (Pp.str "not implemented ... yet")
 
193
 
 
194
let instance_tac inst=
 
195
  if (snd inst)==dummy_id then 
 
196
    right_instance_tac (fst inst)
 
197
  else
 
198
    left_instance_tac inst
 
199
 
 
200
let quantified_tac lf backtrack continue seq gl=
 
201
  let insts=give_instances lf seq in
 
202
    tclORELSE
 
203
      (tclFIRST (List.map (fun inst->instance_tac inst continue seq) insts))
 
204
      backtrack gl
 
205
 
 
206