in
gen_term
-let convert g ety k predicate =
+let convert g ity k predicate =
let rec aux = function
- | C.ALambda (_, _, b, ety), C.ALambda (id, n, u, pred) ->
- C.ALambda (id, n, aux (b, u), aux (ety, pred))
- | C.AProd (_, _, b, ety), C.AProd (id, n, u, pred) ->
- C.AProd (id, n, aux (b, u), aux (ety, pred))
- | C.ALetIn (_, _, a, b, ety), C.ALetIn (id, n, v, u, pred) ->
- C.ALetIn (id, n, aux (a, v), aux (b, u), aux (ety, pred))
+ | C.ALambda (_, _, b, ity), C.ALambda (id, n, u, pred) ->
+ C.ALambda (id, n, aux (b, u), aux (ity, pred))
+ | C.AProd (_, _, b, ity), C.AProd (id, n, u, pred) ->
+ C.AProd (id, n, aux (b, u), aux (ity, pred))
+ | C.ALetIn (_, _, a, b, ity), C.ALetIn (id, n, v, u, pred) ->
+ C.ALetIn (id, n, aux (a, v), aux (b, u), aux (ity, pred))
| C.AAppl (_, bs), C.AAppl (id, us) when List.length bs = List.length us ->
let map b u = aux (b,u) in
C.AAppl (id, List.map2 map bs us)
- | C.ACast (_, ety, b), C.ACast (id, pred, u) ->
- C.ACast (id, aux (ety, pred), aux (b, u))
- | ety, C.AAppl (_, C.ALambda (_, _, _, pred) :: v :: []) ->
- aux (ety, subst 1 v pred)
- | ety, C.AAppl (id, C.ALambda (_, _, _, pred) :: v :: vs) ->
- aux (ety, C.AAppl (id, subst 1 v pred :: vs))
+ | C.ACast (_, ity, b), C.ACast (id, pred, u) ->
+ C.ACast (id, aux (ity, pred), aux (b, u))
+ | ity, C.AAppl (_, C.ALambda (_, _, _, pred) :: v :: []) ->
+ aux (ity, subst 1 v pred)
+ | ity, C.AAppl (id, C.ALambda (_, _, _, pred) :: v :: vs) ->
+ aux (ity, C.AAppl (id, subst 1 v pred :: vs))
| _, pred -> pred
in
- g k (aux (ety, predicate))
+ g k (aux (ity, predicate))
-let mk_pattern psno ety predicate =
- clear_absts (convert (generalize psno) ety) psno 0 predicate
+let mk_pattern psno ity predicate =
+ clear_absts (convert (generalize psno) ity) psno 0 predicate
+
+let beta v = function
+ | C.ALambda (_, _, _, t) -> subst 1 v t
+ | _ -> assert false
let get_clears c p xtypes =
let meta = C.Implicit None in
| entry :: tail -> aux (entry :: c) tail
in
aux [] c
-
+(*
let elim_inferred_type context goal arg using cpattern =
let metasenv, ugraph = [], Un.default_ugraph in
let ety = H.get_type "elim_inferred_type" context using in
let ty = C.Appl (predicate :: actual_args) in
let upto = List.length actual_args in
Rd.head_beta_reduce ~delta:false ~upto ty
-
+*)
let does_not_occur = function
| C.AImplicit (_, None) -> true
| _ -> false