- let match_term m =
- let rec aux ctx status t =
- let b, status = eq ctx status t m in
- if b then
- let n,h,metasenv,subst,o = status.pstatus in
- let ty = NCicTypeChecker.typeof ~subst ~metasenv ctx t in
- let metasenv, instance, ty =
- NCicMetaSubst.mk_meta ~name:"expanded" metasenv ctx (`WithType ty)
- in
- let metasenv, subst =
- NCicUnification.unify (NCicUnifHint.db ()) metasenv subst ctx
- t instance
- in
- let status = { status with pstatus = n,h,metasenv,subst,o } in
- status, instance
- else NCicUntrusted.map_term_fold_a (fun e c -> e::c) ctx aux status t
- in
- aux
- in
- let rec select status ctx pat cic =
- match pat, cic with
- | NCic.Prod (_,s1,t1), NCic.Prod (n,s2,t2) ->
- let status, s = select status ctx s1 s2 in
- let ctx = (n, NCic.Decl s2) :: ctx in
- let status, t = select status ctx t1 t2 in
- status, NCic.Prod (n,s,t)
- | NCic.Appl l1, NCic.Appl l2 ->
- let status, l =
- List.fold_left2
- (fun (status,l) x y ->
- let status, x = select status ctx x y in
- status, l @ [x])
- (status,[]) l1 l2
- in
- status, NCic.Appl l
- | NCic.Implicit `Hole, t -> status, t
- | NCic.Implicit `Term, t ->
- let status, matched = disambiguate status matched None (Ctx ctx) in
- match_term matched ctx status t
- | _,t -> status, t
- in
- let status, term = select low_status context path term in
- let _,_,_,subst,_ = status.pstatus in
- let selections =
- HExtlib.filter_map
- (function (i,(Some "expanded",c,_,_)) -> Some i | _ -> None)
- subst
- in
- status, (name, context, term), selections