diff options
Diffstat (limited to 'pretyping/patternops.ml')
| -rw-r--r-- | pretyping/patternops.ml | 52 |
1 files changed, 33 insertions, 19 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index c49bec9a..705e594a 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -123,6 +123,8 @@ let head_of_constr_reference c = match kind_of_term c with let pattern_of_constr env sigma t = let ctx = ref [] in + let keep = ref Evar.Set.empty in + let remove = ref Evar.Set.empty in let rec pattern_of_constr env t = match kind_of_term t with | Rel n -> PRel n @@ -141,28 +143,38 @@ let pattern_of_constr env sigma t = | App (f,a) -> (match match kind_of_term f with - Evar (evk,args as ev) -> - (match snd (Evd.evar_source evk sigma) with - Evar_kinds.MatchingVar (true,id) -> - ctx := (id,None,Evarutil.nf_evar sigma (existential_type sigma ev))::!ctx; - 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)) + | Evar (evk,args as ev) -> + (match snd (Evd.evar_source evk sigma) with + Evar_kinds.MatchingVar (true,id) -> + let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in + ctx := (id,None,ty)::!ctx; + keep := Evar.Set.union (evars_of_term ty) !keep; + remove := Evar.Set.add evk !remove; + 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 (Retyping.expand_projection env sigma p c []) | Evar (evk,ctxt as ev) -> - (match snd (Evd.evar_source evk sigma) with - | Evar_kinds.MatchingVar (b,id) -> - ctx := (id,None,Evarutil.nf_evar sigma (existential_type sigma ev))::!ctx; - assert (not b); PMeta (Some id) - | Evar_kinds.GoalEvar -> PEvar (evk,Array.map (pattern_of_constr env) ctxt) - | _ -> PMeta None) + remove := Evar.Set.add evk !remove; + (match snd (Evd.evar_source evk sigma) with + | Evar_kinds.MatchingVar (b,id) -> + let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in + ctx := (id,None,ty)::!ctx; + let () = ignore (pattern_of_constr env ty) in + assert (not b); PMeta (Some id) + | Evar_kinds.GoalEvar -> + PEvar (evk,Array.map (pattern_of_constr env) ctxt) + | _ -> + let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in + let () = ignore (pattern_of_constr env ty) in + PMeta None) | Case (ci,p,a,br) -> let cip = { cip_style = ci.ci_pp_info.style; @@ -178,9 +190,11 @@ let pattern_of_constr env sigma t = | Fix f -> PFix f | CoFix f -> PCoFix f in let p = pattern_of_constr env t in + let remove = Evar.Set.diff !remove !keep in + let sigma = Evar.Set.fold (fun ev acc -> Evd.remove acc ev) remove sigma in (* side-effect *) (* Warning: the order of dependencies in ctx is not ensured *) - (!ctx,p) + (sigma,!ctx,p) (* To process patterns, we need a translation without typing at all. *) @@ -220,7 +234,7 @@ let instantiate_pattern env sigma lvar c = ctx in let c = substl inst c in - snd (pattern_of_constr env sigma c) + pi3 (pattern_of_constr env sigma c) with Not_found (* List.index failed *) -> let vars = List.map_filter (function Name id -> Some id | _ -> None) vars in @@ -245,7 +259,7 @@ let rec subst_pattern subst pat = | PRef ref -> let ref',t = subst_global subst ref in if ref' == ref then pat else - snd (pattern_of_constr (Global.env()) Evd.empty t) + pi3 (pattern_of_constr (Global.env()) Evd.empty t) | PVar _ | PEvar _ | PRel _ -> pat |