diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-28 16:15:10 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-31 02:04:10 +0200 |
commit | bf3b52f6a950490ad99b032cb0b41d32cff64824 (patch) | |
tree | f880e1ce1989cd67c06c8a29284f35fc123bec09 /pretyping | |
parent | 5dd98189c6554733fe4e22401e1637330cc8a30a (diff) |
Using a more explicit algebraic type for evars of kind "MatchingVar".
A priori considered to be a good programming style.
Diffstat (limited to 'pretyping')
-rw-r--r-- | pretyping/glob_ops.ml | 9 | ||||
-rw-r--r-- | pretyping/patternops.ml | 11 | ||||
-rw-r--r-- | pretyping/pretyping.ml | 4 |
3 files changed, 15 insertions, 9 deletions
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 923d7d938..a5701be2c 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -12,6 +12,7 @@ open Nameops open Globnames open Misctypes open Glob_term +open Evar_kinds (* Untyped intermediate terms, after ASTs and before constr. *) @@ -59,14 +60,18 @@ let cast_type_eq eq t1 t2 = match t1, t2 with | CastNative t1, CastNative t2 -> eq t1 t2 | _ -> false +let matching_var_kind_eq k1 k2 = match k1, k2 with +| FirstOrderPatVar ido1, FirstOrderPatVar ido2 -> Id.equal ido1 ido2 +| SecondOrderPatVar id1, SecondOrderPatVar id2 -> Id.equal id1 id2 +| (FirstOrderPatVar _ | SecondOrderPatVar _), _ -> false + let rec glob_constr_eq { CAst.v = c1 } { CAst.v = c2 } = match c1, c2 with | GRef (gr1, _), GRef (gr2, _) -> eq_gr gr1 gr2 | GVar id1, GVar id2 -> Id.equal id1 id2 | GEvar (id1, arg1), GEvar (id2, arg2) -> Id.equal id1 id2 && List.equal instance_eq arg1 arg2 -| GPatVar (b1, pat1), GPatVar (b2, pat2) -> - (b1 : bool) == b2 && Id.equal pat1 pat2 +| GPatVar k1, GPatVar k2 -> matching_var_kind_eq k1 k2 | GApp (f1, arg1), GApp (f2, arg2) -> glob_constr_eq f1 f2 && List.equal glob_constr_eq arg1 arg2 | GLambda (na1, bk1, t1, c1), GLambda (na2, bk2, t2, c2) -> diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 1c8ad0cdd..40711bf6b 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -143,7 +143,7 @@ let pattern_of_constr env sigma t = match kind_of_term f with | Evar (evk,args) -> (match snd (Evd.evar_source evk sigma) with - Evar_kinds.MatchingVar (true,id) -> Some id + Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar id) -> Some id | _ -> None) | _ -> None with @@ -156,13 +156,14 @@ let pattern_of_constr env sigma t = 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 (b,id) -> - assert (not b); PMeta (Some id) + | 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) -> @@ -329,12 +330,12 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function | GVar id -> (try PRel (List.index Name.equal (Name id) vars) with Not_found -> PVar id) - | GPatVar (false,n) -> + | 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 ({ CAst.v = GPatVar (true,n) }, cl) -> + | GApp ({ CAst.v = GPatVar (Evar_kinds.SecondOrderPatVar n) }, cl) -> metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl) | GApp (c,cl) -> PApp (pat_of_raw metas vars c, diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index e72394fa2..0e152eaa6 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -610,13 +610,13 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let j = (Retyping.get_judgment_of env.ExtraEnv.env !evdref c) in inh_conv_coerce_to_tycon ?loc env evdref j tycon - | GPatVar (someta,n) -> + | GPatVar kind -> let env = ltac_interp_name_env k0 lvar env !evdref in let ty = match tycon with | Some ty -> ty | None -> new_type_evar env evdref loc in - let k = Evar_kinds.MatchingVar (someta,n) in + let k = Evar_kinds.MatchingVar kind in { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty } | GHole (k, naming, None) -> |