From 3aa07bc00899749dbd14ebb63cdc7007f233bdce Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 6 Apr 2012 22:01:59 +0000 Subject: Fixing a few bugs (see #2571) related to interpretation of multiple binders - fixing missing spaces in the format of the exists' notations (Logic.v); - fixing wrong variable name in check_is_hole error message (topconstr.ml); - interpret expressions with open binders such as "forall x y, t" as "forall (x:_) (y:_),t" instead of "forall (x y:_),t" to avoid the "implicit type" of a variable being propagated to the type of another variable of different base name. An open question remains: when writing explicitly "forall (x y:_),t", should the types of x and y be the same or not. To avoid the "bug" that x and y have implicit types but the one of x takes precedences, I enforced the interpretation (in constrintern, not in parsing) that "forall (x y:_),t" means the same as "forall (x:_) (y:_),t". However, another choice could have been made. Then one would have to check that if x and y have implicit types, they are the same; also, glob_constr should ideally be changed to support a GProd and GLam with multiple names in the same type, especially if this type is an evar. On the contrary, one might also want e.g. "forall x y : list _, t" to mean "forall (x:list _) (y:list _), t" with distinct instanciations of "_" ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15121 85f007b7-540e-0410-9357-904b9bb8a0f7 --- interp/constrintern.ml | 52 ++++++++++++++++++++++++++++---------------------- interp/topconstr.ml | 2 +- 2 files changed, 30 insertions(+), 24 deletions(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 3890931274..d4639987a8 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -421,12 +421,12 @@ let intern_local_binder_aux ?(global_level=false) intern intern_type lvar (env,b | LocalRawAssum(nal,bk,ty) -> (match bk with | Default k -> - let (loc,na) = List.hd nal in - (* TODO: fail if several names with different implicit types *) - let ty = locate_if_isevar loc na (intern_type env ty) in + let ty = intern_type env ty in + let impls = impls_type_list ty in List.fold_left - (fun (env,bl) na -> - (push_name_env lvar (impls_type_list ty) env na,(snd na,k,None,ty)::bl)) + (fun (env,bl) (loc,na as locna) -> + (push_name_env lvar impls env locna, + (na,k,None,locate_if_isevar loc na ty)::bl)) (env,bl) nal | Generalized (b,b',t) -> let env, b = intern_generalized_binder ~global_level intern_type lvar env bl (List.hd nal) b b' t ty in @@ -465,12 +465,12 @@ let iterate_binder intern lvar (env,bl) = function let intern_type env = intern (set_type_scope env) in (match bk with | Default k -> - let (loc,na) = List.hd nal in - (* TODO: fail if several names with different implicit types *) let ty = intern_type env ty in - let ty = locate_if_isevar loc na ty in + let impls = impls_type_list ty in List.fold_left - (fun (env,bl) na -> (push_name_env lvar (impls_type_list ty) env na,(snd na,k,None,ty)::bl)) + (fun (env,bl) (loc,na as locna) -> + (push_name_env lvar impls env locna, + (na,k,None,locate_if_isevar loc na ty)::bl)) (env,bl) nal | Generalized (b,b',t) -> let env, b = intern_generalized_binder intern_type lvar env bl (List.hd nal) b b' t ty in @@ -1614,13 +1614,16 @@ let internalize sigma globalenv env allow_patvar lvar c = (tm',(snd na,typ)), extra_id, match_td and iterate_prod loc2 env bk ty body nal = - let rec default env bk = function - | (loc1,na as locna)::nal -> - if nal <> [] then check_capture loc1 ty na; - let ty = locate_if_isevar loc1 na (intern_type env ty) in - let body = default (push_name_env lvar (impls_type_list ty) env locna) bk nal in - GProd (join_loc loc1 loc2, na, bk, ty, body) - | [] -> intern_type env body + let default env bk = function + | (loc1,na)::nal' as nal -> + if nal' <> [] then check_capture loc1 ty na; + let ty = intern_type env ty in + let impls = impls_type_list ty in + let env = List.fold_left (push_name_env lvar impls) env nal in + List.fold_right (fun (loc,na) c -> + GProd (join_loc loc loc2, na, bk, locate_if_isevar loc na ty, c)) + nal (intern_type env body) + | [] -> assert false in match bk with | Default b -> default env b nal @@ -1630,13 +1633,16 @@ let internalize sigma globalenv env allow_patvar lvar c = it_mkGProd ibind body and iterate_lam loc2 env bk ty body nal = - let rec default env bk = function - | (loc1,na as locna)::nal -> - if nal <> [] then check_capture loc1 ty na; - let ty = locate_if_isevar loc1 na (intern_type env ty) in - let body = default (push_name_env lvar (impls_type_list ty) env locna) bk nal in - GLambda (join_loc loc1 loc2, na, bk, ty, body) - | [] -> intern env body + let default env bk = function + | (loc1,na)::nal' as nal -> + if nal' <> [] then check_capture loc1 ty na; + let ty = intern_type env ty in + let impls = impls_type_list ty in + let env = List.fold_left (push_name_env lvar impls) env nal in + List.fold_right (fun (loc,na) c -> + GLambda (join_loc loc loc2, na, bk, locate_if_isevar loc na ty, c)) + nal (intern env body) + | [] -> assert false in match bk with | Default b -> default env b nal | Generalized (b, b', t) -> diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 8db5b0afa2..7d3acf66a8 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -240,7 +240,7 @@ let compare_recursive_parts found f (iterator,subc) = | GLambda (_,Name x,_,t_x,c), GLambda (_,Name y,_,t_y,term) | GProd (_,Name x,_,t_x,c), GProd (_,Name y,_,t_y,term) -> (* We found a binding position where it differs *) - check_is_hole y t_x; + check_is_hole x t_x; check_is_hole y t_y; !diff = None && (diff := Some (x,y,None); aux c term) | _ -> -- cgit v1.2.3