aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/patternops.ml
blob: 3b3ad021e4ecf4fc8cdc710bf92f3c4e7920c244 (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
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open CErrors
open Util
open Names
open Globnames
open Nameops
open Term
open Vars
open Glob_term
open Pp
open Mod_subst
open Misctypes
open Decl_kinds
open Pattern
open Environ

let case_info_pattern_eq i1 i2 =
  i1.cip_style == i2.cip_style &&
  Option.equal eq_ind i1.cip_ind i2.cip_ind &&
  Option.equal (List.equal (==)) i1.cip_ind_tags i2.cip_ind_tags &&
  i1.cip_extensible == i2.cip_extensible

let rec constr_pattern_eq p1 p2 = match p1, p2 with
| PRef r1, PRef r2 -> eq_gr r1 r2
| PVar v1, PVar v2 -> Id.equal v1 v2
| PEvar (ev1, ctx1), PEvar (ev2, ctx2) ->
  Evar.equal ev1 ev2 && Array.equal constr_pattern_eq ctx1 ctx2
| PRel i1, PRel i2 ->
  Int.equal i1 i2
| PApp (t1, arg1), PApp (t2, arg2) ->
  constr_pattern_eq t1 t2 && Array.equal constr_pattern_eq arg1 arg2
| PSoApp (id1, arg1), PSoApp (id2, arg2) ->
  Id.equal id1 id2 && List.equal constr_pattern_eq arg1 arg2
| PLambda (v1, t1, b1), PLambda (v2, t2, b2) ->
  Name.equal v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2
| PProd (v1, t1, b1), PProd (v2, t2, b2) ->
  Name.equal v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2
| PLetIn (v1, b1, t1, c1), PLetIn (v2, b2, t2, c2) ->
  Name.equal v1 v2 && constr_pattern_eq b1 b2 &&
  Option.equal constr_pattern_eq t1 t2 && constr_pattern_eq c1 c2
| PSort s1, PSort s2 -> Miscops.glob_sort_eq s1 s2
| PMeta m1, PMeta m2 -> Option.equal Id.equal m1 m2
| PIf (t1, l1, r1), PIf (t2, l2, r2) ->
  constr_pattern_eq t1 t2 && constr_pattern_eq l1 l2 && constr_pattern_eq r1 r2
| PCase (info1, p1, r1, l1), PCase (info2, p2, r2, l2) ->
  case_info_pattern_eq info1 info2 &&
  constr_pattern_eq p1 p2 &&
  constr_pattern_eq r1 r2 &&
  List.equal pattern_eq l1 l2
| PFix f1, PFix f2 ->
  fixpoint_eq f1 f2
| PCoFix f1, PCoFix f2 ->
  cofixpoint_eq f1 f2
| _ -> false
(** FIXME: fixpoint and cofixpoint should be relativized to pattern *)

and pattern_eq (i1, j1, p1) (i2, j2, p2) =
  Int.equal i1 i2 && List.equal (==) j1 j2 && constr_pattern_eq p1 p2

and fixpoint_eq ((arg1, i1), r1) ((arg2, i2), r2) =
  Int.equal i1 i2 &&
  Array.equal Int.equal arg1 arg2 &&
  rec_declaration_eq r1 r2

and cofixpoint_eq (i1, r1) (i2, r2) =
  Int.equal i1 i2 &&
  rec_declaration_eq r1 r2

and rec_declaration_eq (n1, c1, r1) (n2, c2, r2) =
  Array.equal Name.equal n1 n2 &&
  Array.equal Term.eq_constr c1 c2 &&
  Array.equal Term.eq_constr r1 r2

let rec occur_meta_pattern = function
  | PApp (f,args) ->
      (occur_meta_pattern f) || (Array.exists occur_meta_pattern args)
  | PProj (_,arg) -> occur_meta_pattern arg
  | PLambda (na,t,c)  -> (occur_meta_pattern t) || (occur_meta_pattern c)
  | PProd (na,t,c)  -> (occur_meta_pattern t) || (occur_meta_pattern c)
  | PLetIn (na,b,t,c)  ->
     Option.fold_left (fun b t -> b || occur_meta_pattern t) (occur_meta_pattern b) t || (occur_meta_pattern c)
  | PIf (c,c1,c2)  ->
      (occur_meta_pattern c) ||
      (occur_meta_pattern c1) || (occur_meta_pattern c2)
  | PCase(_,p,c,br) ->
      (occur_meta_pattern p) ||
      (occur_meta_pattern c) ||
      (List.exists (fun (_,_,p) -> occur_meta_pattern p) br)
  | PMeta _ | PSoApp _ -> true
  | PEvar _ | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _ -> false

exception BoundPattern;;

let rec head_pattern_bound t =
  match t with
    | PProd (_,_,b)  -> head_pattern_bound b
    | PLetIn (_,_,_,b) -> head_pattern_bound b
    | PApp (c,args)  -> head_pattern_bound c
    | PIf (c,_,_)  -> head_pattern_bound c
    | PCase (_,p,c,br) -> head_pattern_bound c
    | PRef r         -> r
    | PVar id        -> VarRef id
    | PProj (p,c)    -> ConstRef (Projection.constant p)
    | PEvar _ | PRel _ | PMeta _ | PSoApp _  | PSort _ | PFix _
	-> raise BoundPattern
    (* Perhaps they were arguments, but we don't beta-reduce *)
    | PLambda _ -> raise BoundPattern
    | PCoFix _ -> anomaly ~label:"head_pattern_bound" (Pp.str "not a type.")

let head_of_constr_reference sigma c = match EConstr.kind sigma c with
  | Const (sp,_) -> ConstRef sp
  | Construct (sp,_) -> ConstructRef sp
  | Ind (sp,_) -> IndRef sp
  | Var id -> VarRef id
  | _ -> anomaly (Pp.str "Not a rigid reference.")

let pattern_of_constr env sigma t =
  let rec pattern_of_constr env t =
  let open Context.Rel.Declaration in
  match kind_of_term t with
    | Rel n  -> PRel n
    | Meta n -> PMeta (Some (Id.of_string ("META" ^ string_of_int n)))
    | Var id -> PVar id
    | Sort (Prop Null) -> PSort GProp
    | Sort (Prop Pos) -> PSort GSet
    | Sort (Type _) -> PSort (GType [])
    | Cast (c,_,_)      -> pattern_of_constr env c
    | LetIn (na,c,t,b) -> PLetIn (na,pattern_of_constr env c,Some (pattern_of_constr env t),
				  pattern_of_constr (push_rel (LocalDef (na,c,t)) env) b)
    | Prod (na,c,b)   -> PProd (na,pattern_of_constr env c,
				pattern_of_constr (push_rel (LocalAssum (na, c)) env) b)
    | Lambda (na,c,b) -> PLambda (na,pattern_of_constr env c,
				  pattern_of_constr (push_rel (LocalAssum (na, c)) env) b)
    | App (f,a) ->
        (match
          match kind_of_term f with
          | Evar (evk,args) ->
            (match snd (Evd.evar_source evk sigma) with
              Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar id) -> Some id
            | _ -> None)
          | _ -> None
         with
         | Some n -> PSoApp (n,Array.to_list (Array.map (pattern_of_constr env) a))
         | None -> PApp (pattern_of_constr env f,Array.map (pattern_of_constr env) a))
    | Const (sp,u)  -> PRef (ConstRef (constant_of_kn(canonical_con sp)))
    | Ind (sp,u)    -> PRef (canonical_gr (IndRef sp))
    | Construct (sp,u) -> PRef (canonical_gr (ConstructRef sp))
    | Proj (p, c) -> 
      pattern_of_constr env (EConstr.Unsafe.to_constr (Retyping.expand_projection env sigma p (EConstr.of_constr c) []))
    | Evar (evk,ctxt as ev) ->
      (match snd (Evd.evar_source evk sigma) with
      | Evar_kinds.MatchingVar (Evar_kinds.FirstOrderPatVar id) ->
        PMeta (Some id)
      | Evar_kinds.GoalEvar | Evar_kinds.VarInstance _ ->
        (* These are the two evar kinds used for existing goals *)
        (* see Proofview.mark_in_evm *)
         if Evd.is_defined sigma evk then pattern_of_constr env (Evd.existential_value sigma ev)
         else PEvar (evk,Array.map (pattern_of_constr env) ctxt)
      | Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar ido) -> assert false
      | _ -> 
	 PMeta None)
    | Case (ci,p,a,br) ->
        let cip =
	  { cip_style = ci.ci_pp_info.style;
	    cip_ind = Some ci.ci_ind;
	    cip_ind_tags = Some ci.ci_pp_info.ind_tags;
	    cip_extensible = false }
	in
	let branch_of_constr i c =
	  (i, ci.ci_pp_info.cstr_tags.(i), pattern_of_constr env c)
	in
	PCase (cip, pattern_of_constr env p, pattern_of_constr env a,
	       Array.to_list (Array.mapi branch_of_constr br))
    | Fix f -> PFix f
    | CoFix f -> PCoFix f in
  pattern_of_constr env t

(* To process patterns, we need a translation without typing at all. *)

let map_pattern_with_binders g f l = function
  | PApp (p,pl) -> PApp (f l p, Array.map (f l) pl)
  | PSoApp (n,pl) -> PSoApp (n, List.map (f l) pl)
  | PLambda (n,a,b) -> PLambda (n,f l a,f (g n l) b)
  | PProd (n,a,b) -> PProd (n,f l a,f (g n l) b)
  | PLetIn (n,a,t,b) -> PLetIn (n,f l a,Option.map (f l) t,f (g n l) b)
  | PIf (c,b1,b2) -> PIf (f l c,f l b1,f l b2)
  | PCase (ci,po,p,pl) ->
    PCase (ci,f l po,f l p, List.map (fun (i,n,c) -> (i,n,f l c)) pl)
  | PProj (p,pc) -> PProj (p, f l pc)
  (* Non recursive *)
  | (PVar _ | PEvar _ | PRel _ | PRef _  | PSort _  | PMeta _
  (* Bound to terms *)
  | PFix _ | PCoFix _ as x) -> x

let error_instantiate_pattern id l =
  let is = match l with
  | [_] -> "is" 
  | _ -> "are"
  in
  user_err  (str "Cannot substitute the term bound to " ++ pr_id id
    ++ strbrk " in pattern because the term refers to " ++ pr_enum pr_id l
    ++ strbrk " which " ++ str is ++ strbrk " not bound in the pattern.")

let instantiate_pattern env sigma lvar c =
  let open EConstr in
  let open Vars in
  let rec aux vars = function
  | PVar id as x ->
      (try
	let ctx,c = Id.Map.find id lvar in
	try
	  let inst =
	    List.map
              (fun id -> mkRel (List.index Name.equal (Name id) vars))
              ctx
          in
	  let c = substl inst c in
	  (** FIXME: Stupid workaround to pattern_of_constr being evar sensitive *)
	  let c = Evarutil.nf_evar sigma c in
	  pattern_of_constr env sigma (EConstr.Unsafe.to_constr c)
	with Not_found (* List.index failed *) ->
	  let vars =
	    List.map_filter (function Name id -> Some id | _ -> None) vars in
	  error_instantiate_pattern id (List.subtract Id.equal ctx vars)
       with Not_found (* Map.find failed *) ->
	 x)
  | (PFix _ | PCoFix _) -> user_err Pp.(str "Non instantiable pattern.")
  | c ->
      map_pattern_with_binders (fun id vars -> id::vars) aux vars c in
  aux [] c

let rec liftn_pattern k n = function
  | PRel i as x -> if i >= n then PRel (i+k) else x
  | PFix x -> PFix (destFix (liftn k n (mkFix x)))
  | PCoFix x -> PCoFix (destCoFix (liftn k n (mkCoFix x)))
  | c -> map_pattern_with_binders (fun _ -> succ) (liftn_pattern k) n c

let lift_pattern k = liftn_pattern k 1

let rec subst_pattern subst pat =
  match pat with
  | PRef ref ->
      let ref',t = subst_global subst ref in
	if ref' == ref then pat else
	 pattern_of_constr (Global.env()) Evd.empty t
  | PVar _
  | PEvar _
  | PRel _ -> pat
  | PProj (p,c) -> 
      let p' = Projection.map (fun p -> 
	destConstRef (fst (subst_global subst (ConstRef p)))) p in
      let c' = subst_pattern subst c in
	if p' == p && c' == c then pat else
	  PProj(p',c')
  | PApp (f,args) ->
      let f' = subst_pattern subst f in
      let args' = Array.smartmap (subst_pattern subst) args in
	if f' == f && args' == args then pat else
	  PApp (f',args')
  | PSoApp (i,args) ->
      let args' = List.smartmap (subst_pattern subst) args in
	if args' == args then pat else
	  PSoApp (i,args')
  | PLambda (name,c1,c2) ->
      let c1' = subst_pattern subst c1 in
      let c2' = subst_pattern subst c2 in
	if c1' == c1 && c2' == c2 then pat else
	  PLambda (name,c1',c2')
  | PProd (name,c1,c2) ->
      let c1' = subst_pattern subst c1 in
      let c2' = subst_pattern subst c2 in
	if c1' == c1 && c2' == c2 then pat else
	  PProd (name,c1',c2')
  | PLetIn (name,c1,t,c2) ->
      let c1' = subst_pattern subst c1 in
      let t' = Option.smartmap (subst_pattern subst) t in
      let c2' = subst_pattern subst c2 in
	if c1' == c1 && t' == t && c2' == c2 then pat else
	  PLetIn (name,c1',t',c2')
  | PSort _
  | PMeta _ -> pat
  | PIf (c,c1,c2) ->
      let c' = subst_pattern subst c in
      let c1' = subst_pattern subst c1 in
      let c2' = subst_pattern subst c2 in
	if c' == c && c1' == c1 && c2' == c2 then pat else
	  PIf (c',c1',c2')
  | PCase (cip,typ,c,branches) ->
      let ind = cip.cip_ind in
      let ind' = Option.smartmap (subst_ind subst) ind in
      let cip' = if ind' == ind then cip else { cip with cip_ind = ind' } in
      let typ' = subst_pattern subst typ in
      let c' = subst_pattern subst c in
      let subst_branch ((i,n,c) as br) =
	let c' = subst_pattern subst c in
	if c' == c then br else (i,n,c')
      in
      let branches' = List.smartmap subst_branch branches in
      if cip' == cip && typ' == typ && c' == c && branches' == branches
      then pat
      else PCase(cip', typ', c', branches')
  | PFix fixpoint ->
      let cstr = mkFix fixpoint in
      let fixpoint' = destFix (subst_mps subst cstr) in
	if fixpoint' == fixpoint then pat else
	  PFix fixpoint'
  | PCoFix cofixpoint ->
      let cstr = mkCoFix cofixpoint in
      let cofixpoint' = destCoFix (subst_mps subst cstr) in
	if cofixpoint' == cofixpoint then pat else
	  PCoFix cofixpoint'

let mkPLambda na b = PLambda(na,PMeta None,b)
let rev_it_mkPLambda = List.fold_right mkPLambda

let err ?loc pp = user_err ?loc ~hdr:"pattern_of_glob_constr" pp

let warn_cast_in_pattern =
  CWarnings.create ~name:"cast-in-pattern" ~category:"automation"
    (fun () -> Pp.strbrk "Casts are ignored in patterns")

let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
  | GVar id ->
      (try PRel (List.index Name.equal (Name id) vars)
       with Not_found -> PVar id)
  | GPatVar (Evar_kinds.FirstOrderPatVar n) ->
      metas := n::!metas; PMeta (Some n)
  | GRef (gr,_) ->
      PRef (canonical_gr gr)
  (* Hack to avoid rewriting a complete interpretation of patterns *)
  | GApp (c, cl) ->
    begin match DAst.get c with
    | GPatVar (Evar_kinds.SecondOrderPatVar n) ->
      metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl)
    | _ ->
      PApp (pat_of_raw metas vars c,
	    Array.of_list (List.map (pat_of_raw metas vars) cl))
    end
  | GLambda (na,bk,c1,c2) ->
      Name.iter (fun n -> metas := n::!metas) na;
      PLambda (na, pat_of_raw metas vars c1,
	       pat_of_raw metas (na::vars) c2)
  | GProd (na,bk,c1,c2) ->
      Name.iter (fun n -> metas := n::!metas) na;
      PProd (na, pat_of_raw metas vars c1,
	       pat_of_raw metas (na::vars) c2)
  | GLetIn (na,c1,t,c2) ->
      Name.iter (fun n -> metas := n::!metas) na;
      PLetIn (na, pat_of_raw metas vars c1,
               Option.map (pat_of_raw metas vars) t,
	       pat_of_raw metas (na::vars) c2)
  | GSort s ->
      PSort s
  | GHole _ ->
      PMeta None
  | GCast (c,_) ->
      warn_cast_in_pattern ();
      pat_of_raw metas vars c
  | GIf (c,(_,None),b1,b2) ->
      PIf (pat_of_raw metas vars c,
           pat_of_raw metas vars b1,pat_of_raw metas vars b2)
  | GLetTuple (nal,(_,None),b,c) ->
      let mkGLambda na c = DAst.make ?loc @@
	GLambda (na,Explicit, DAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None),c) in
      let c = List.fold_right mkGLambda nal c in
      let cip =
	{ cip_style = LetStyle;
	  cip_ind = None;
	  cip_ind_tags = None;
	  cip_extensible = false }
      in
      let tags = List.map (fun _ -> false) nal (* Approximation which can be without let-ins... *) in
      PCase (cip, PMeta None, pat_of_raw metas vars b,
             [0,tags,pat_of_raw metas vars c])
  | GCases (sty,p,[c,(na,indnames)],brs) ->
      let get_ind p = match DAst.get p with 
      | PatCstr((ind,_),_,_) -> Some ind
      | _ -> None
      in
      let get_ind = function
	| (_,(_,[p],_))::_ -> get_ind p
	| _ -> None
      in
      let ind_tags,ind = match indnames with
	| Some (_,(ind,nal)) -> Some (List.length nal), Some ind
	| None -> None, get_ind brs
      in
      let ext,brs = pats_of_glob_branches loc metas vars ind brs
      in
      let pred = match p,indnames with
	| Some p, Some (_,(_,nal)) ->
          let nvars = na :: List.rev nal @ vars in
          rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p))
        | None, _ -> PMeta None
	| Some p, None ->
          match DAst.get p with
          | GHole _ -> PMeta None
          | _ ->
            user_err ?loc  (strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.")
      in
      let info =
	{ cip_style = sty;
	  cip_ind = ind;
	  cip_ind_tags = None;
	  cip_extensible = ext }
      in
      (* Nota : when we have a non-trivial predicate,
	 the inductive type is known. Same when we have at least
	 one non-trivial branch. These facts are used in [Constrextern]. *)
      PCase (info, pred, pat_of_raw metas vars c, brs)

  | r -> err ?loc (Pp.str "Non supported pattern.")
  )

and pats_of_glob_branches loc metas vars ind brs =
  let get_arg p = match DAst.get p with
    | PatVar na ->
      Name.iter (fun n -> metas := n::!metas) na;
      na
    | PatCstr(_,_,_) -> err ?loc:p.CAst.loc (Pp.str "Non supported pattern.")
  in
  let rec get_pat indexes = function
    | [] -> false, []
    | (loc',(_,[p], br)) :: brs ->
      begin match DAst.get p, DAst.get br, brs with
      | PatVar Anonymous, GHole _, [] ->
        true, [] (* ends with _ => _ *)
      | PatCstr((indsp,j),lv,_), _, _ ->
        let () = match ind with
        | Some sp when eq_ind sp indsp -> ()
        | _ ->
          err ?loc (Pp.str "All constructors must be in the same inductive type.")
        in
        if Int.Set.mem (j-1) indexes then
          err ?loc
            (str "No unique branch for " ++ int j ++ str"-th constructor.");
        let lna = List.map get_arg lv in
        let vars' = List.rev lna @ vars in
        let pat = rev_it_mkPLambda lna (pat_of_raw metas vars' br) in
        let ext,pats = get_pat (Int.Set.add (j-1) indexes) brs in
        let tags = List.map (fun _ -> false) lv (* approximation, w/o let-in *) in
        ext, ((j-1, tags, pat) :: pats)
      | _ ->
        err ?loc:loc' (Pp.str "Non supported pattern.")
      end
    | (loc,(_,_,_)) :: _ -> err ?loc (Pp.str "Non supported pattern.")
  in
  get_pat Int.Set.empty brs

let pattern_of_glob_constr c =
  let metas = ref [] in
  let p = pat_of_raw metas [] c in
  (!metas,p)