← Back to branch summary

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

« back to all changes in this revision

Viewing changes to contrib/interface/dad.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/dad.ml
 
1
(* This file contains an ml version of drag-and-drop. *)
 
2
 
 
3
(* #use "/net/home/bertot/experiments/pcoq/src/dad/dad.ml" *)
 
4
 
 
5
open Names;;
 
6
open Term;;
 
7
open Rawterm;;
 
8
open Util;;
 
9
open Environ;;
 
10
open Tactics;;
 
11
open Tacticals;;
 
12
open Pattern;;
 
13
open Matching;;
 
14
open Reduction;;
 
15
open Constrextern;;
 
16
open Constrintern;;
 
17
open Vernacinterp;;
 
18
open Libnames;;
 
19
open Nametab
 
20
 
 
21
open Proof_type;;
 
22
open Proof_trees;;
 
23
open Tacmach;;
 
24
open Typing;;
 
25
open Pp;;
 
26
 
 
27
open Paths;;
 
28
 
 
29
open Topconstr;;
 
30
open Genarg;;
 
31
open Tacexpr;;
 
32
open Rawterm;;
 
33
 
 
34
(* In a first approximation, drag-and-drop rules are like in CtCoq
 
35
   1/ a pattern,
 
36
   2,3/ Two paths: start and end positions,
 
37
   4/ the degree: the number of steps the algorithm should go up from the
 
38
      longest common prefix,
 
39
   5/ the tail path: the suffix of the longest common prefix of length the
 
40
      degree,
 
41
   6/ the command pattern, where meta variables are represented by objects
 
42
      of the form Node(_,"META"; [Num(_,i)])
 
43
*)
 
44
 
 
45
 
 
46
type dad_rule =
 
47
    constr_expr * int list * int list * int * int list
 
48
    * raw_atomic_tactic_expr;;
 
49
 
 
50
(* This value will be used systematically when constructing objects *)
 
51
 
 
52
let zz = Util.dummy_loc;;
 
53
 
 
54
(* This function receives a length n, a path p, and a term and returns a
 
55
   couple whose first component is the subterm designated by the prefix
 
56
   of p of length n, and the second component is the rest of the path *)
 
57
 
 
58
let rec get_subterm  (depth:int) (path: int list) (constr:constr) =
 
59
  match depth, path, kind_of_term constr with
 
60
    0, l, c -> (constr,l)
 
61
  | n, 2::a::tl, App(func,arr) -> 
 
62
      get_subterm (n - 2) tl arr.(a-1)
 
63
  | _,l,_ -> failwith (int_list_to_string 
 
64
                        "wrong path or wrong form of term"
 
65
                        l);;
 
66
 
 
67
(* This function maps a substitution on an abstract syntax tree.  The
 
68
   first argument, an object of type env, is necessary to
 
69
   transform constr terms into abstract syntax trees.  The second argument is
 
70
   the substitution, a list of pairs linking an integer and a constr term. *)
 
71
 
 
72
let rec map_subst (env :env) (subst:patvar_map) = function
 
73
  | CPatVar (_,(_,i)) ->
 
74
      let constr = List.assoc i subst in
 
75
      extern_constr false env constr
 
76
  | x -> map_constr_expr_with_binders (fun _ x -> x) (map_subst env) subst x;;
 
77
 
 
78
let map_subst_tactic env subst = function
 
79
  | TacExtend (loc,("Rewrite" as x),[b;cbl]) ->
 
80
      let c,bl = out_gen rawwit_constr_with_bindings cbl in
 
81
      assert (bl = NoBindings);
 
82
      let c = (map_subst env subst c,NoBindings) in
 
83
      TacExtend (loc,x,[b;in_gen rawwit_constr_with_bindings c])
 
84
  | _ -> failwith "map_subst_tactic: unsupported tactic"
 
85
 
 
86
(* This function is really the one that is important. *)
 
87
let rec find_cmd (l:(string * dad_rule) list) env constr p p1 p2 =
 
88
  match l with
 
89
    [] -> failwith "nothing happens"
 
90
  | (name, (pat, p_f, p_l, deg, p_r, cmd))::tl ->
 
91
     let length = List.length p in
 
92
     try
 
93
       if deg > length then
 
94
         failwith "internal"
 
95
       else
 
96
         let term_to_match, p_r = 
 
97
             try 
 
98
                get_subterm (length - deg) p constr
 
99
             with
 
100
                Failure s -> failwith "internal" in
 
101
         let _, constr_pat = 
 
102
            intern_constr_pattern Evd.empty (Global.env())
 
103
               ((*ct_to_ast*) pat) in
 
104
         let subst = matches constr_pat term_to_match in
 
105
         if (is_prefix p_f (p_r@p1)) & (is_prefix p_l (p_r@p2)) then
 
106
           TacAtom (zz, map_subst_tactic env subst cmd)
 
107
         else
 
108
           failwith "internal"
 
109
     with
 
110
       Failure "internal" -> find_cmd tl env constr p p1 p2
 
111
     | PatternMatchingFailure -> find_cmd tl env constr p p1 p2;;
 
112
 
 
113
 
 
114
let dad_rule_list = ref ([]: (string * dad_rule) list);;
 
115
 
 
116
(*
 
117
(* \\ This function is also used in pbp. *)
 
118
let rec tactic_args_to_ints = function
 
119
    [] -> []
 
120
  | (Integer n)::l -> n::(tactic_args_to_ints l)
 
121
  | _ -> failwith "expecting only numbers";;
 
122
 
 
123
(* We assume that the two lists of integers for the tactic are simply
 
124
   given in one list, separated by a dummy tactic. *)
 
125
let rec part_tac_args l = function
 
126
    [] -> l,[]
 
127
  | (Tacexp a)::tl -> l, (tactic_args_to_ints tl)
 
128
  | (Integer n)::tl -> part_tac_args (n::l) tl
 
129
  | _ -> failwith "expecting only numbers and the word \"to\"";;
 
130
 
 
131
 
 
132
(* The dad_tac tactic takes a display_function as argument.  This makes
 
133
   it possible to use it in pcoq, but also in other contexts, just by
 
134
   changing the output routine. *)
 
135
let dad_tac display_function = function
 
136
   l -> let p1, p2 = part_tac_args [] l in
 
137
        (function g ->
 
138
           let (p_a, p1prime, p2prime) = decompose_path (List.rev p1,p2) in
 
139
           (display_function 
 
140
            (find_cmd (!dad_rule_list) (pf_env g)
 
141
               (pf_concl g) p_a p1prime p2prime));
 
142
            tclIDTAC g);;
 
143
*)
 
144
let dad_tac display_function p1 p2 g =
 
145
  let (p_a, p1prime, p2prime) = decompose_path (p1,p2) in
 
146
  (display_function 
 
147
    (find_cmd (!dad_rule_list) (pf_env g) (pf_concl g) p_a p1prime p2prime));
 
148
  tclIDTAC g;;
 
149
 
 
150
(* Now we enter dad rule list management. *)
 
151
 
 
152
let add_dad_rule name patt p1 p2 depth pr command =
 
153
  dad_rule_list := (name, 
 
154
                    (patt, p1, p2, depth, pr, command))::!dad_rule_list;;
 
155
 
 
156
let rec remove_if_exists name = function
 
157
    [] -> false, []
 
158
  | ((a,b) as rule1)::tl -> if a = name then 
 
159
               let result1, l = (remove_if_exists name tl) in
 
160
               true, l
 
161
             else
 
162
               let result1, l = remove_if_exists name tl in
 
163
               result1, (rule1::l);;
 
164
 
 
165
let remove_dad_rule name =
 
166
  let result1, result2 = remove_if_exists name !dad_rule_list in
 
167
  if result1 then
 
168
    failwith("No such name among the drag and drop rules " ^ name)
 
169
  else
 
170
     dad_rule_list := result2;;
 
171
 
 
172
let dad_rule_names () =
 
173
    List.map (function (s,_) -> s) !dad_rule_list;;
 
174
 
 
175
(* this function is inspired from matches_core in pattern.ml *)
 
176
let constrain ((n : patvar),(pat : constr_pattern)) sigma =
 
177
  if List.mem_assoc n sigma then
 
178
    if pat = (List.assoc n sigma) then sigma
 
179
    else failwith "internal"
 
180
  else 
 
181
    (n,pat)::sigma
 
182
    
 
183
(* This function is inspired from matches_core in pattern.ml *)
 
184
let more_general_pat pat1 pat2 = 
 
185
  let rec match_rec sigma p1 p2 =
 
186
    match p1, p2 with
 
187
      | PMeta (Some n), m -> constrain (n,m) sigma
 
188
 
 
189
      | PMeta None, m -> sigma
 
190
 
 
191
      | PRef (VarRef sp1), PRef(VarRef sp2) when sp1 = sp2 -> sigma
 
192
 
 
193
      | PVar v1, PVar v2 when v1 = v2 -> sigma
 
194
 
 
195
      | PRef ref1, PRef ref2 when ref1 = ref2 -> sigma
 
196
 
 
197
      | PRel n1, PRel n2 when n1 = n2 -> sigma
 
198
 
 
199
      | PSort (RProp c1), PSort (RProp c2) when c1 = c2 -> sigma
 
200
 
 
201
      | PSort (RType _), PSort (RType _) -> sigma
 
202
 
 
203
      | PApp (c1,arg1), PApp (c2,arg2) ->
 
204
        (try array_fold_left2 match_rec (match_rec sigma c1 c2) arg1 arg2
 
205
         with Invalid_argument _ -> failwith "internal")
 
206
      | _ -> failwith "unexpected case in more_general_pat" in 
 
207
  try let _ = match_rec [] pat1 pat2 in true
 
208
  with Failure "internal" -> false;;
 
209
 
 
210
let more_general r1 r2 =
 
211
  match r1,r2 with
 
212
    (_,(patt1,p11,p12,_,_,_)),
 
213
    (_,(patt2,p21,p22,_,_,_)) ->
 
214
        (more_general_pat patt1 patt2) &
 
215
      (is_prefix p11 p21) & (is_prefix p12 p22);;
 
216
 
 
217
let not_less_general r1 r2 = 
 
218
  not (match r1,r2 with
 
219
    (_,(patt1,p11,p12,_,_,_)),
 
220
    (_,(patt2,p21,p22,_,_,_)) ->
 
221
        (more_general_pat patt1 patt2) &
 
222
      (is_prefix p21 p11) & (is_prefix p22 p12));;
 
223
 
 
224
let rec add_in_list_sorting rule1 = function
 
225
    [] -> [rule1]
 
226
  | (b::tl) as this_list ->
 
227
      if more_general rule1 b  then
 
228
        b::(add_in_list_sorting rule1 tl)
 
229
      else if not_less_general rule1 b then
 
230
        let tl2 = add_in_list_sorting_aux rule1 tl in
 
231
        (match tl2 with
 
232
          [] -> rule1::this_list
 
233
        | _ -> b::tl2)
 
234
      else
 
235
        rule1::this_list
 
236
and add_in_list_sorting_aux rule1 = function
 
237
    [] -> []
 
238
  | b::tl -> 
 
239
      if more_general rule1 b then
 
240
        b::(add_in_list_sorting rule1 tl)
 
241
      else
 
242
        let tl2 = add_in_list_sorting_aux rule1 tl in
 
243
        (match tl2 with
 
244
          [] -> []
 
245
        | _ -> rule1::tl2);;
 
246
 
 
247
let rec sort_list = function
 
248
    [] -> [] 
 
249
  | a::l -> add_in_list_sorting a (sort_list l);;
 
250
 
 
251
let mk_dad_meta n = CPatVar (zz,(true,Nameops.make_ident "DAD" (Some n)));;
 
252
let mk_rewrite lr ast =
 
253
  let b = in_gen rawwit_bool lr in
 
254
  let cb = in_gen rawwit_constr_with_bindings (ast,NoBindings) in
 
255
  TacExtend (zz,"Rewrite",[b;cb])
 
256
 
 
257
open Vernacexpr
 
258
 
 
259
let dad_status = ref false;;
 
260
 
 
261
let start_dad () = dad_status := true;;
 
262
 
 
263
let add_dad_rule_fn name pat p1 p2 tac =
 
264
  let pr = match decompose_path (p1, p2) with pr, _, _ -> pr in
 
265
  add_dad_rule name pat p1 p2 (List.length pr) pr tac;;
 
266
 
 
267
(* To be parsed by camlp4
 
268
 
 
269
(*i camlp4deps: "parsing/grammar.cma" i*)
 
270
 
 
271
VERNAC COMMAND EXTEND AddDadRule
 
272
  [ "Add" "Dad" "Rule" string(name) constr(pat)
 
273
    "From" natural_list(p1) "To" natural_list(p2) tactic(tac) ] ->
 
274
  [ add_dad_rule_fn name pat p1 p2 tac ]
 
275
END
 
276
 
 
277
*)
 
278
 
 
279
let mk_id s = mkIdentC (id_of_string s);;
 
280
let mkMetaC = mk_dad_meta;;
 
281
 
 
282
add_dad_rule "distributivity-inv"
 
283
(mkAppC(mk_id("mult"),[mkAppC(mk_id("plus"),[mkMetaC(4);mkMetaC(3)]);mkMetaC(2)]))
 
284
[2; 2]
 
285
[2; 1]
 
286
1
 
287
[2]
 
288
(mk_rewrite true (mkAppC(mk_id( "mult_plus_distr"),[(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])));
 
289
 
 
290
add_dad_rule "distributivity1-r"
 
291
(mkAppC(mk_id("plus"),[mkAppC(mk_id("mult"),[mkMetaC(4);mkMetaC(2)]);mkAppC(mk_id("mult"),[mkMetaC(3);mkMetaC(2)])]))
 
292
[2; 2; 2; 2]
 
293
[]
 
294
0
 
295
[]
 
296
(mk_rewrite false (mkAppC(mk_id("mult_plus_distr"),[(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])));
 
297
 
 
298
add_dad_rule "distributivity1-l"
 
299
(mkAppC(mk_id("plus"),[mkAppC(mk_id("mult"),[mkMetaC(4);mkMetaC(2)]);mkAppC(mk_id("mult"),[mkMetaC(3);mkMetaC(2)])]))
 
300
[2; 1; 2; 2]
 
301
[]
 
302
0
 
303
[]
 
304
(mk_rewrite false (mkAppC(mk_id( "mult_plus_distr"),[(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])));
 
305
 
 
306
add_dad_rule "associativity"
 
307
(mkAppC(mk_id("plus"),[mkAppC(mk_id("plus"),[mkMetaC(4);mkMetaC(3)]);mkMetaC(2)]))
 
308
[2; 1]
 
309
[]
 
310
0
 
311
[]
 
312
(mk_rewrite true (mkAppC(mk_id( "plus_assoc_r"),[(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])));
 
313
 
 
314
add_dad_rule "minus-identity-lr"
 
315
(mkAppC(mk_id("minus"),[mkMetaC(2);mkMetaC(2)]))
 
316
[2; 1]
 
317
[2; 2]
 
318
1
 
319
[2]
 
320
(mk_rewrite false (mkAppC(mk_id( "minus_n_n"),[(mk_dad_meta 2) ])));
 
321
 
 
322
add_dad_rule "minus-identity-rl"
 
323
(mkAppC(mk_id("minus"),[mkMetaC(2);mkMetaC(2)]))
 
324
[2; 2]
 
325
[2; 1]
 
326
1
 
327
[2]
 
328
(mk_rewrite false (mkAppC(mk_id( "minus_n_n"),[(mk_dad_meta 2) ])));
 
329
 
 
330
add_dad_rule "plus-sym-rl"
 
331
(mkAppC(mk_id("plus"),[mkMetaC(3);mkMetaC(2)]))
 
332
[2; 2]
 
333
[2; 1]
 
334
1
 
335
[2]
 
336
(mk_rewrite true (mkAppC(mk_id( "plus_sym"),[(mk_dad_meta 3) ;(mk_dad_meta 2) ])));
 
337
 
 
338
add_dad_rule "plus-sym-lr"
 
339
(mkAppC(mk_id("plus"),[mkMetaC(3);mkMetaC(2)]))
 
340
[2; 1]
 
341
[2; 2]
 
342
1
 
343
[2]
 
344
(mk_rewrite true (mkAppC(mk_id( "plus_sym"),[(mk_dad_meta 3) ;(mk_dad_meta 2) ])));
 
345
 
 
346
add_dad_rule "absorb-0-r-rl"
 
347
(mkAppC(mk_id("plus"),[mkMetaC(2);mk_id("O")]))
 
348
[2; 2]
 
349
[1]
 
350
0
 
351
[]
 
352
(mk_rewrite false (mkAppC(mk_id( "plus_n_O"),[(mk_dad_meta 2) ])));
 
353
 
 
354
add_dad_rule "absorb-0-r-lr"
 
355
(mkAppC(mk_id("plus"),[mkMetaC(2);mk_id("O")]))
 
356
[1]
 
357
[2; 2]
 
358
0
 
359
[]
 
360
(mk_rewrite false (mkAppC(mk_id( "plus_n_O"),[(mk_dad_meta 2) ])));
 
361
 
 
362
add_dad_rule "plus-permute-lr"
 
363
(mkAppC(mk_id("plus"),[mkMetaC(4);mkAppC(mk_id("plus"),[mkMetaC(3);mkMetaC(2)])]))
 
364
[2; 1]
 
365
[2; 2; 2; 1]
 
366
1
 
367
[2]
 
368
(mk_rewrite true (mkAppC(mk_id( "plus_permute"),[(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])));
 
369
 
 
370
add_dad_rule "plus-permute-rl"
 
371
(mkAppC(mk_id("plus"),[mkMetaC(4);mkAppC(mk_id("plus"),[mkMetaC(3);mkMetaC(2)])]))
 
372
[2; 2; 2; 1]
 
373
[2; 1]
 
374
1
 
375
[2]
 
376
(mk_rewrite true (mkAppC(mk_id( "plus_permute"),[(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])));;
 
377
 
 
378
vinterp_add "StartDad"
 
379
   (function
 
380
     | [] ->
 
381
       (function () -> start_dad())
 
382
     | _ -> errorlabstrm "StartDad" (mt()));;