diff options
author | 2017-04-13 15:05:16 +0200 | |
---|---|---|
committer | 2017-04-13 15:16:51 +0200 | |
commit | b4936da085b19ad508346d8e07ce1e922ef79c2d (patch) | |
tree | 8a51b2bead7486af7f0a59efc6c4882f2d5cc087 | |
parent | 4e70791036a1ab189579e109b428f46f45698b59 (diff) |
Using fold_glob_constr_with_binders to code bound_glob_vars.
To use the generic combinator, we introduce a side effect. I believe
that we have more to gain from a short code than from being purely
functional.
This also fixes the expected semantics since the variables binding the
return type in "match" were not taking into account.
-rw-r--r-- | pretyping/glob_ops.ml | 57 | ||||
-rw-r--r-- | test-suite/.csdp.cache | bin | 89077 -> 89077 bytes | |||
-rw-r--r-- | test-suite/success/boundvars.v | 9 |
3 files changed, 17 insertions, 49 deletions
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index aa296aace..080ec5ed1 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -300,57 +300,16 @@ let add_and_check_ident id set = Id.Set.add id set let bound_glob_vars = - let rec vars bound = function - | GLambda (_,na,_,_,_) | GProd (_,na,_,_,_) | GLetIn (_,na,_,_,_) as c -> - let bound = name_fold add_and_check_ident na bound in - fold_glob_constr vars bound c - | GCases (loc,sty,rtntypopt,tml,pl) -> - let bound = vars_option bound rtntypopt in - let bound = - List.fold_left (fun bound (tm,_) -> vars bound tm) bound tml in - List.fold_left vars_pattern bound pl - | GLetTuple (loc,nal,rtntyp,b,c) -> - let bound = vars_return_type bound rtntyp in - let bound = vars bound b in - let bound = List.fold_right (name_fold add_and_check_ident) nal bound in - vars bound c - | GIf (loc,c,rtntyp,b1,b2) -> - let bound = vars_return_type bound rtntyp in - let bound = vars bound c in - let bound = vars bound b1 in - vars bound b2 - | GRec (loc,fk,idl,bl,tyl,bv) -> - let bound = Array.fold_right Id.Set.add idl bound in - let vars_fix i bound fid = - let bound = - List.fold_left - (fun bound (na,k,bbd,bty) -> - let bound = vars_option bound bbd in - let bound = vars bound bty in - name_fold add_and_check_ident na bound - ) - bound - bl.(i) - in - let bound = vars bound tyl.(i) in - vars bound bv.(i) - in - Array.fold_left_i vars_fix bound idl - | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GVar _) -> bound - | GApp _ | GCast _ as c -> fold_glob_constr vars bound c - - and vars_pattern bound (loc,idl,p,c) = - let bound = List.fold_right add_and_check_ident idl bound in - vars bound c - - and vars_option bound = function None -> bound | Some p -> vars bound p - - and vars_return_type bound (na,tyopt) = - let bound = name_fold add_and_check_ident na bound in - vars_option bound tyopt + let rec vars bound = + fold_glob_constr_with_binders + (fun id () -> bound := add_and_check_ident id !bound) + (fun () () -> vars bound) + () () in fun rt -> - vars Id.Set.empty rt + let bound = ref Id.Set.empty in + vars bound rt; + !bound (** Mapping of names in binders *) diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache Binary files differindex b99d80e95..ba85286dd 100644 --- a/test-suite/.csdp.cache +++ b/test-suite/.csdp.cache diff --git a/test-suite/success/boundvars.v b/test-suite/success/boundvars.v index 7b6696af8..fafe27292 100644 --- a/test-suite/success/boundvars.v +++ b/test-suite/success/boundvars.v @@ -3,3 +3,12 @@ Check forall (x z:unit) (x y : match z as x return x=x with tt => eq_refl end = eq_refl), x=x. +(* An example showing a bug in the detection of bound variables *) + +Goal forall x, match x return x = x with 0 => eq_refl | _ => eq_refl end = eq_refl. +intro. +match goal with +|- (match x as y in nat return y = y with O => _ | S n => _ end) = _ => assert (forall y, y = 0) end. +intro. +Check x0. (* Check that "y" has been bound to "x0" while matching "match x as x0 return x0=x0 with ... end" *) +Abort. |