aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/constrMatching.ml
blob: 21e22e0bbfc87e767f71aa61fda422c79f4d2ab3 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(*i*)
open Pp
open Errors
open Util
open Names
open Globnames
open Nameops
open Termops
open Reductionops
open Term
open Vars
open Context
open Pattern
open Patternops
open Misctypes
(*i*)

(* Given a term with second-order variables in it,
   represented by Meta's, and possibly applied using [SOAPP] to
   terms, this function will perform second-order, binding-preserving,
   matching, in the case where the pattern is a pattern in the sense
   of Dale Miller.

   ALGORITHM:

   Given a pattern, we decompose it, flattening Cast's and apply's,
   recursing on all operators, and pushing the name of the binder each
   time we descend a binder.

   When we reach a first-order variable, we ask that the corresponding
   term's free-rels all be higher than the depth of the current stack.

   When we reach a second-order application, we ask that the
   intersection of the free-rels of the term and the current stack be
   contained in the arguments of the application, and in that case, we
   construct a LAMBDA with the names on the stack.

 *)

type bound_ident_map = Id.t Id.Map.t

exception PatternMatchingFailure

let warn_bound_meta name =
  msg_warning (str "Collision between bound variable " ++ pr_id name ++
    str " and a metavariable of same name.")

let warn_bound_bound name =
  msg_warning (str "Collision between bound variables of name " ++ pr_id name)

let warn_bound_again name =
  msg_warning (str "Collision between bound variable " ++ pr_id name ++
    str " and another bound variable of same name.")

let constrain n (ids, m as x) (names, terms as subst) =
  try
    let (ids', m') = Id.Map.find n terms in
    if List.equal Id.equal ids ids' && eq_constr m m' then subst
    else raise PatternMatchingFailure
  with Not_found ->
    let () = if Id.Map.mem n names then warn_bound_meta n in
    (names, Id.Map.add n x terms)

let add_binders na1 na2 (names, terms as subst) = match na1, na2 with
| Name id1, Name id2 ->
  if Id.Map.mem id1 names then
    let () = warn_bound_bound id1 in
    (names, terms)
  else
    let names = Id.Map.add id1 id2 names in
    let () = if Id.Map.mem id1 terms then warn_bound_again id1 in
    (names, terms)
| _ -> subst

let build_lambda toabstract stk (m : constr) =
  let rec buildrec m k stk = match stk with
  | [] -> m
  | (_, na, t) :: tl ->
    if Int.Set.mem k toabstract then
      buildrec (mkLambda (na, t, m)) (k + 1) tl
    else
      buildrec (lift (-1) m) (k + 1) tl
  in
  buildrec m 1 stk

let rec extract_bound_aux k accu frels stk = match stk with
| [] -> accu
| (na1, na2, _) :: stk ->
  if Int.Set.mem k frels then
    begin match na1 with
    | Name id ->
      let () = assert (match na2 with Anonymous -> false | Name _ -> true) in
      let () = if Id.Set.mem id accu then raise PatternMatchingFailure in
      extract_bound_aux (k + 1) (Id.Set.add id accu) frels stk
    | Anonymous -> raise PatternMatchingFailure
    end
  else extract_bound_aux (k + 1) accu frels stk

let extract_bound_vars frels stk =
  extract_bound_aux 1 Id.Set.empty frels stk

let dummy_constr = mkProp

let make_renaming ids = function
| (Name id, Name _, _) ->
  begin
    try mkRel (List.index Id.equal id ids)
    with Not_found -> dummy_constr
  end
| _ -> dummy_constr

let merge_binding allow_bound_rels stk n cT subst =
  let c = match stk with
  | [] -> (* Optimization *)
    ([], cT)
  | _ ->
    let frels = free_rels cT in
    if allow_bound_rels then
      let vars = extract_bound_vars frels stk in
      let ordered_vars = Id.Set.elements vars in
      let rename binding = make_renaming ordered_vars binding in
      let renaming = List.map rename stk in
      (ordered_vars, substl renaming cT)
    else
      let depth = List.length stk in
      let min_elt = try Int.Set.min_elt frels with Not_found -> succ depth in
      if depth < min_elt then
        ([], lift (- depth) cT)
      else raise PatternMatchingFailure
  in
  constrain n c subst

let matches_core convert allow_partial_app allow_bound_rels pat c =
  let convref ref c = 
    match ref, kind_of_term c with
    | VarRef id, Var id' -> Names.id_eq id id'
    | ConstRef c, Const (c',_) -> Names.eq_constant c c'
    | IndRef i, Ind (i', _) -> Names.eq_ind i i'
    | ConstructRef c, Construct (c',u) -> Names.eq_constructor c c'
    | _, _ -> (match convert with 
               | None -> false
	       | Some (env,sigma) -> 
	         let sigma,c' = Evd.fresh_global env sigma ref in
		   is_conv env sigma c' c)
  in
  let rec sorec stk subst p t =
    let cT = strip_outer_cast t in
    match p,kind_of_term cT with
      | PSoApp (n,args),m ->
        let fold accu = function
        | PRel n -> Int.Set.add n accu
        | _ -> error "Only bound indices allowed in second order pattern matching."
        in
        let relargs = List.fold_left fold Int.Set.empty args in
        let frels = free_rels cT in
        if Int.Set.subset frels relargs then
          constrain n ([], build_lambda relargs stk cT) subst
        else
          raise PatternMatchingFailure

      | PMeta (Some n), m -> merge_binding allow_bound_rels stk n cT subst

      | PMeta None, m -> subst

      | PRef (VarRef v1), Var v2 when Id.equal v1 v2 -> subst

      | PVar v1, Var v2 when Id.equal v1 v2 -> subst

      | PRef ref, _ when convref ref cT -> subst

      | PRel n1, Rel n2 when Int.equal n1 n2 -> subst

      | PSort GProp, Sort (Prop Null) -> subst

      | PSort GSet, Sort (Prop Pos) -> subst

      | PSort (GType _), Sort (Type _) -> subst

      | PApp (p, [||]), _ -> sorec stk subst p t

      | PApp (PApp (h, a1), a2), _ ->
          sorec stk subst (PApp(h,Array.append a1 a2)) t

      | PApp (PMeta meta,args1), App (c2,args2) when allow_partial_app ->
          let p = Array.length args2 - Array.length args1 in
          if p >= 0 then
            let args21, args22 = Array.chop p args2 in
	    let c = mkApp(c2,args21) in
            let subst =
              match meta with
              | None -> subst
              | Some n -> merge_binding allow_bound_rels stk n c subst in
            Array.fold_left2 (sorec stk) subst args1 args22
          else raise PatternMatchingFailure

      | PApp (c1,arg1), App (c2,arg2) ->
	(match c1, kind_of_term c2 with
	| PRef (ConstRef r), Proj _ ->
      	  (let subst = (sorec stk subst (PProj (r,arg1.(0))) c2) in
	     try Array.fold_left2 (sorec stk) subst (Array.tl arg1) arg2
	     with Invalid_argument _ -> raise PatternMatchingFailure)
	| _ ->
          (try Array.fold_left2 (sorec stk) (sorec stk subst c1 c2) arg1 arg2
           with Invalid_argument _ -> raise PatternMatchingFailure))
	  
      | PProj (p1,c1), Proj (p2,c2) when eq_constant p1 p2 ->
          sorec stk subst c1 c2

      | PProd (na1,c1,d1), Prod(na2,c2,d2) ->
	  sorec ((na1,na2,c2)::stk)
            (add_binders na1 na2 (sorec stk subst c1 c2)) d1 d2

      | PLambda (na1,c1,d1), Lambda(na2,c2,d2) ->
	  sorec ((na1,na2,c2)::stk)
            (add_binders na1 na2 (sorec stk subst c1 c2)) d1 d2

      | PLetIn (na1,c1,d1), LetIn(na2,c2,t2,d2) ->
	  sorec ((na1,na2,t2)::stk)
            (add_binders na1 na2 (sorec stk subst c1 c2)) d1 d2

      | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) ->
	  let ctx,b2 = decompose_lam_n_assum ci.ci_cstr_ndecls.(0) b2 in
	  let ctx',b2' = decompose_lam_n_assum ci.ci_cstr_ndecls.(1) b2' in
	  let n = rel_context_length ctx in
          let n' = rel_context_length ctx' in
	  if noccur_between 1 n b2 && noccur_between 1 n' b2' then
	    let s =
	      List.fold_left (fun l (na,_,t) -> (Anonymous,na,t)::l) stk ctx in
	    let s' =
	      List.fold_left (fun l (na,_,t) -> (Anonymous,na,t)::l) stk ctx' in
	    let b1 = lift_pattern n b1 and b1' = lift_pattern n' b1' in
	    sorec s' (sorec s (sorec stk subst a1 a2) b1 b2) b1' b2'
          else
            raise PatternMatchingFailure

      | PCase (ci1,p1,a1,br1), Case (ci2,p2,a2,br2) ->
	  let n2 = Array.length br2 in
          let () = match ci1.cip_ind with
          | None -> ()
          | Some ind1 ->
            (** ppedrot: Something spooky going here. The comparison used to be
                the generic one, so I may have broken something. *)
            if not (eq_ind ind1 ci2.ci_ind) then raise PatternMatchingFailure
          in
          let () =
            if not ci1.cip_extensible && not (Int.equal (List.length br1) n2)
            then raise PatternMatchingFailure
          in
	  let chk_branch subst (j,n,c) =
	    (* (ind,j+1) is normally known to be a correct constructor
	       and br2 a correct match over the same inductive *)
	    assert (j < n2);
	    sorec stk subst c br2.(j)
	  in
	  let chk_head = sorec stk (sorec stk subst a1 a2) p1 p2 in
	  List.fold_left chk_branch chk_head br1

      |	PFix c1, Fix _ when eq_constr (mkFix c1) cT -> subst
      |	PCoFix c1, CoFix _ when eq_constr (mkCoFix c1) cT -> subst
      | _ -> raise PatternMatchingFailure

  in
  sorec [] (Id.Map.empty, Id.Map.empty) pat c

let matches_core_closed convert allow_partial_app pat c =
  let names, subst = matches_core convert allow_partial_app false pat c in
  (names, Id.Map.map snd subst)

let extended_matches = matches_core None true true

let matches pat c = snd (matches_core_closed None true pat c)

let special_meta = (-1)

type matching_result =
    { m_sub : bound_ident_map * patvar_map;
      m_ctx : constr; }

let mkresult s c n = IStream.Cons ( { m_sub=s; m_ctx=c; } , (IStream.thunk n) )

let isPMeta = function PMeta _ -> true | _ -> false

let matches_head pat c =
  let head =
    match pat, kind_of_term c with
    | PApp (c1,arg1), App (c2,arg2) ->
        if isPMeta c1 then c else
        let n1 = Array.length arg1 in
        if n1 < Array.length arg2 then mkApp (c2,Array.sub arg2 0 n1) else c
    | c1, App (c2,arg2) when not (isPMeta c1) -> c2
    | _ -> c in
  matches pat head

(* Tells if it is an authorized occurrence and if the instance is closed *)
let authorized_occ partial_app closed pat c mk_ctx next =
  try
    let sigma = matches_core_closed None partial_app pat c in
    if closed && Id.Map.exists (fun _ c -> not (closed0 c)) (snd sigma)
    then next ()
    else mkresult sigma (mk_ctx (mkMeta special_meta)) next
  with PatternMatchingFailure -> next ()

(* Tries to match a subterm of [c] with [pat] *)
let sub_match ?(partial_app=false) ?(closed=true) pat c =
  let rec aux c mk_ctx next =
  match kind_of_term c with
  | Cast (c1,k,c2) ->
      let next_mk_ctx lc = mk_ctx (mkCast (List.hd lc, k,c2)) in
      let next () = try_aux [c1] next_mk_ctx next in
      authorized_occ partial_app closed pat c mk_ctx next
  | Lambda (x,c1,c2) ->
      let next_mk_ctx lc = mk_ctx (mkLambda (x,List.hd lc,List.nth lc 1)) in
      let next () = try_aux [c1;c2] next_mk_ctx next in
      authorized_occ partial_app closed pat c mk_ctx next
  | Prod (x,c1,c2) ->
      let next_mk_ctx lc = mk_ctx (mkProd (x,List.hd lc,List.nth lc 1)) in
      let next () = try_aux [c1;c2] next_mk_ctx next in
      authorized_occ partial_app closed pat c mk_ctx next
  | LetIn (x,c1,t,c2) ->
      let next_mk_ctx = function
      | [c1;c2] -> mkLetIn (x,c1,t,c2)
      | _ -> assert false
      in
      let next () = try_aux [c1;c2] next_mk_ctx next in
      authorized_occ partial_app closed pat c mk_ctx next
  | App (c1,lc) ->
      let next () =
        let topdown = true in
        if partial_app then
          if topdown then
            let lc1 = Array.sub lc 0 (Array.length lc - 1) in
            let app = mkApp (c1,lc1) in
            let mk_ctx = function
              | [app';c] -> mk_ctx (mkApp (app',[|c|]))
              | _ -> assert false in
            try_aux [app;Array.last lc] mk_ctx next
          else
            let rec aux2 app args next =
              match args with
              | [] ->
                  let mk_ctx le =
                    mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in
                  try_aux (c1::Array.to_list lc) mk_ctx next
              | arg :: args ->
                  let app = mkApp (app,[|arg|]) in
                  let next () = aux2 app args next in
                  let mk_ctx ce = mk_ctx (mkApp (ce, Array.of_list args)) in
                  aux app mk_ctx next in
            aux2 c1 (Array.to_list lc) next
        else
          let mk_ctx le =
            mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in
          try_aux (c1::Array.to_list lc) mk_ctx next
      in
      authorized_occ partial_app closed pat c mk_ctx next
  | Case (ci,hd,c1,lc) ->
      let next_mk_ctx = function
      | [] -> assert false
      | c1 :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc))
      in
      let next () = try_aux (c1 :: Array.to_list lc) next_mk_ctx next in
      authorized_occ partial_app closed pat c mk_ctx next
  | Fix (indx,(names,types,bodies)) ->
    let nb_fix = Array.length types in
    let next_mk_ctx le =
      let (ntypes,nbodies) = CList.chop nb_fix le in
      mk_ctx (mkFix (indx,(names, Array.of_list ntypes, Array.of_list nbodies))) in
    let next () =
      try_aux
	((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next in
    authorized_occ partial_app closed pat c mk_ctx next
  | CoFix (i,(names,types,bodies)) ->
    let nb_fix = Array.length types in
    let next_mk_ctx le =
      let (ntypes,nbodies) = CList.chop nb_fix le in
      mk_ctx (mkCoFix (i,(names, Array.of_list ntypes, Array.of_list nbodies))) in
    let next () =
      try_aux ((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next in
    authorized_occ partial_app closed pat c mk_ctx next
  | Proj (p,c') ->
    let next_mk_ctx le = mk_ctx (mkProj (p,List.hd le)) in
    let next () = try_aux [c'] next_mk_ctx next in
      authorized_occ partial_app closed pat c mk_ctx next
  | Construct _| Ind _|Evar _|Const _ | Rel _|Meta _|Var _|Sort _ ->
      authorized_occ partial_app closed pat c mk_ctx next

  (* Tries [sub_match] for all terms in the list *)
  and try_aux lc mk_ctx next =
    let rec try_sub_match_rec lacc = function
      | [] -> next ()
      | c::tl ->
          let mk_ctx ce = mk_ctx (List.rev_append lacc (ce::tl)) in
          let next () = try_sub_match_rec (c::lacc) tl in
          aux c mk_ctx next in
    try_sub_match_rec [] lc in
  let lempty () = IStream.Nil in
  let result () = aux c (fun x -> x) lempty in
  IStream.thunk result

let match_subterm pat c = sub_match pat c

let match_appsubterm pat c = sub_match ~partial_app:true pat c

let match_subterm_gen app pat c = sub_match ~partial_app:app pat c

let is_matching pat c =
  try let _ = matches pat c in true
  with PatternMatchingFailure -> false

let is_matching_head pat c =
  try let _ = matches_head pat c in true
  with PatternMatchingFailure -> false

let is_matching_appsubterm ?(closed=true) pat c =
  let results = sub_match ~partial_app:true ~closed pat c in
  not (IStream.is_empty results)

let matches_conv env sigma c p =
  snd (matches_core_closed (Some (env,sigma)) false c p)

let is_matching_conv env sigma pat n =
  try let _ = matches_conv env sigma pat n in true
  with PatternMatchingFailure -> false