From d91a0c27402f0f19a30147bb9d87387ca2a91fd0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 2 Feb 2017 10:18:48 +0100 Subject: "Standardizing" the name LocalPatten into LocalRawPattern. --- interp/implicit_quantifiers.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp/implicit_quantifiers.ml') diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 77a8ed680a..fe0e8d44b9 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -114,7 +114,7 @@ let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder list) = let l' = free_vars_of_constr_expr c ~bound:bdvars l in aux (Id.Set.union (ids_of_list bound) bdvars) l' tl - | LocalPattern _ :: tl -> assert false + | LocalRawPattern _ :: tl -> assert false | [] -> bdvars, l in aux bound l binders -- cgit v1.2.3 From 4e4fb7bd42364fd623f8e0e0d3007cd79d78764b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 2 Feb 2017 18:21:51 +0100 Subject: Renaming local_binder into local_binder_expr. This is a bit long, but it is to keep a symmetry with constr_expr. --- interp/implicit_quantifiers.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp/implicit_quantifiers.ml') diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index fe0e8d44b9..4caacc08c1 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -102,7 +102,7 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = let ids_of_names l = List.fold_left (fun acc x -> match snd x with Name na -> na :: acc | Anonymous -> acc) [] l -let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder list) = +let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr list) = let rec aux bdvars l c = match c with ((LocalRawAssum (n, _, c)) :: tl) -> let bound = ids_of_names n in -- cgit v1.2.3 From 648ce5e08f7245f2a775abd1304783c4167e9f2e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 2 Feb 2017 18:24:58 +0100 Subject: Unifying standard "constr_level" names for constructors of local_binder_expr. RawLocal -> CLocal --- interp/implicit_quantifiers.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'interp/implicit_quantifiers.ml') diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 4caacc08c1..ececce340d 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -104,17 +104,17 @@ let ids_of_names l = let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr list) = let rec aux bdvars l c = match c with - ((LocalRawAssum (n, _, c)) :: tl) -> + ((CLocalAssum (n, _, c)) :: tl) -> let bound = ids_of_names 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 - | ((LocalRawDef (n, c)) :: tl) -> + | ((CLocalDef (n, c)) :: 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 - | LocalRawPattern _ :: tl -> assert false + | CLocalPattern _ :: tl -> assert false | [] -> bdvars, l in aux bound l binders -- cgit v1.2.3 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 ececce340d..7f11c0a3b6 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