From f9a4ca41bc1313300f5f9b9092fe24825f435706 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 1 Feb 2017 15:56:45 +0100 Subject: Replacing "cast surgery" in LetIn by a proper field (see PR #404). This is a patch fulfilling the relevant remark of Maxime that an explicit information at the ML type level would be better than "cast surgery" to carry the optional type of a let-in. There are a very few semantic changes. - a "(x:t:=c)" in a block of binders is now written in the more standard way "(x:=c:t)" - in notations, the type of a let-in is not displayed if not explicitly asked so. See discussion at PR #417 for more information. --- interp/implicit_quantifiers.ml | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) (limited to 'interp/implicit_quantifiers.ml') diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index ececce340..7f11c0a3b 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -109,10 +109,11 @@ let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr li let l' = free_vars_of_constr_expr c ~bound:bdvars l in aux (Id.Set.union (ids_of_list bound) bdvars) l' tl - | ((CLocalDef (n, c)) :: tl) -> + | ((CLocalDef (n, c, t)) :: tl) -> let bound = match snd n with Anonymous -> [] | Name n -> [n] in let l' = free_vars_of_constr_expr c ~bound:bdvars l in - aux (Id.Set.union (ids_of_list bound) bdvars) l' tl + let l'' = Option.fold_left (fun l t -> free_vars_of_constr_expr t ~bound:bdvars l) l' t in + aux (Id.Set.union (ids_of_list bound) bdvars) l'' tl | CLocalPattern _ :: tl -> assert false | [] -> bdvars, l @@ -131,10 +132,15 @@ let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.emp else (id, loc) :: vs else vs | GApp (loc,f,args) -> List.fold_left (vars bound) vs (f::args) - | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) | GLetIn (loc,na,ty,c) -> + | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) -> let vs' = vars bound vs ty in let bound' = add_name_to_ids bound na in vars bound' vs' c + | GLetIn (loc,na,b,ty,c) -> + let vs' = vars bound vs b in + let vs'' = Option.fold_left (vars bound) vs' ty in + let bound' = add_name_to_ids bound na in + vars bound' vs'' c | GCases (loc,sty,rtntypopt,tml,pl) -> let vs1 = vars_option bound vs rtntypopt in let vs2 = List.fold_left (fun vs (tm,_) -> vars bound vs tm) vs1 tml in @@ -318,7 +324,7 @@ let implicits_of_glob_constr ?(with_products=true) l = | _ -> () in [] | GLambda (loc, na, bk, t, b) -> abs na bk b - | GLetIn (loc, na, t, b) -> aux i b + | GLetIn (loc, na, b, t, c) -> aux i c | GRec (_, fix_kind, nas, args, tys, bds) -> let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in List.fold_left_i (fun i l (na,bk,_,_) -> add_impl i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb) -- cgit v1.2.3