From 9d47cc0af706ed1cd4ab87c2d402a0457a9b6a5c Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 19 Nov 2015 17:48:32 +0100 Subject: Fix bug #4433, removing hack on evars appearing in a pattern from a constr, and the associated signature, not needed anymore. Update CHANGES, no evar_map is produced by pattern_of_constr anymore. --- pretyping/patternops.ml | 29 +++++++---------------------- 1 file changed, 7 insertions(+), 22 deletions(-) (limited to 'pretyping/patternops.ml') diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index fb629d049f..83bf355cc2 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -122,9 +122,6 @@ let head_of_constr_reference c = match kind_of_term c with | _ -> anomaly (Pp.str "Not a rigid reference") 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 @@ -143,14 +140,9 @@ let pattern_of_constr env sigma t = | App (f,a) -> (match match kind_of_term f with - | Evar (evk,args as ev) -> + | Evar (evk,args) -> (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 + Evar_kinds.MatchingVar (true,id) -> Some id | _ -> None) | _ -> None with @@ -162,13 +154,11 @@ let pattern_of_constr env sigma t = | Proj (p, c) -> pattern_of_constr env (Retyping.expand_projection env sigma p c []) | Evar (evk,ctxt as ev) -> - 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) + 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) | _ -> @@ -189,12 +179,7 @@ let pattern_of_constr env sigma t = Array.to_list (Array.mapi branch_of_constr br)) | 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 *) - (sigma,!ctx,p) + pattern_of_constr env t (* To process patterns, we need a translation without typing at all. *) @@ -234,7 +219,7 @@ let instantiate_pattern env sigma lvar c = ctx in let c = substl inst c in - pi3 (pattern_of_constr env sigma c) + 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 @@ -259,7 +244,7 @@ let rec subst_pattern subst pat = | PRef ref -> let ref',t = subst_global subst ref in if ref' == ref then pat else - pi3 (pattern_of_constr (Global.env()) Evd.empty t) + pattern_of_constr (Global.env()) Evd.empty t | PVar _ | PEvar _ | PRel _ -> pat -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- pretyping/patternops.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/patternops.ml') diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 83bf355cc2..af46c390a6 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* match (prod_assum (snd (decompose_prod_n_assum n c))) with | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc Suppose that you do not know about rel-context and named-context. (that is the case of people who just started to read the source code) Merlin would tell you that the type of the value you are destructing by "match" is: 'a * 'b option * Constr.t (* worst-case scenario *) or Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *) To me, this is akin to wearing an opaque veil. It is hard to figure out the meaning of the values you are looking at. In particular, it is hard to discover the connection between the value we are destructing above and the datatypes and functions defined in the "kernel/context.ml" file. In this case, the connection is there, but it is not visible (between the function above and the "Context" module). ------------------------------------------------------------------------ Now consider, what happens when the reader see the same function presented in the following form: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc If the reader haven't seen "LocalAssum" before, (s)he can use Merlin to jump to the corresponding definition and learn more. In this case, the connection is there, and it is directly visible (between the function above and the "Context" module). (2) Also, if we already have the concepts such as: - local declaration - local assumption - local definition and we describe these notions meticulously in the Reference Manual, then it is a real pity not to reinforce the connection of the actual code with the abstract description we published. --- pretyping/patternops.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'pretyping/patternops.ml') diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index af46c390a6..827071054a 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -123,6 +123,7 @@ let head_of_constr_reference c = match kind_of_term c with 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))) @@ -132,11 +133,11 @@ let pattern_of_constr env sigma t = | Sort (Type _) -> PSort (GType []) | Cast (c,_,_) -> pattern_of_constr env c | LetIn (na,c,t,b) -> PLetIn (na,pattern_of_constr env c, - pattern_of_constr (push_rel (na,Some c,t) env) b) + 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 (na, None, c) env) b) + 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 (na, None, c) env) b) + pattern_of_constr (push_rel (LocalAssum (na, c)) env) b) | App (f,a) -> (match match kind_of_term f with -- cgit v1.2.3