diff options
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 95 |
1 files changed, 45 insertions, 50 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index bc5cdf726..81ddb2731 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -288,24 +288,19 @@ let check_hidden_implicit_parameters id (_,_,_,(indnames,_)) = errorlabstrm "" (strbrk "A parameter or name of an inductive type " ++ pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.") -let push_name_env ?(fail_anonymous=false) lvar (ids,unb,tmpsc,scopes as env) = function - | Anonymous -> - if fail_anonymous then errorlabstrm "" (str "Anonymous variables not allowed"); +let push_name_env ?(global_level=false) lvar (ids,unb,tmpsc,scopes as env) = + function + | loc,Anonymous -> + if global_level then + user_err_loc (loc,"", str "Anonymous variables not allowed"); env - | Name id -> + | loc,Name id -> check_hidden_implicit_parameters id lvar; - (Idset.add id ids, unb,tmpsc,scopes) - -let push_loc_name_env ?(fail_anonymous=false) lvar (ids,unb,tmpsc,scopes as env) loc = function - | Anonymous -> - if fail_anonymous then user_err_loc (loc,"", str "Anonymous variables not allowed"); - env - | Name id -> - check_hidden_implicit_parameters id lvar; - Dumpglob.dump_binding loc id; + if global_level then Dumpglob.dump_definition (loc,id) true "var" + else Dumpglob.dump_binding loc id; (Idset.add id ids,unb,tmpsc,scopes) -let intern_generalized_binder ?(fail_anonymous=false) intern_type lvar +let intern_generalized_binder ?(global_level=false) intern_type lvar (ids,unb,tmpsc,sc as env) bl (loc, na) b b' t ty = let ids = match na with Anonymous -> ids | Name na -> Idset.add na ids in let ty, ids' = @@ -315,11 +310,11 @@ let intern_generalized_binder ?(fail_anonymous=false) intern_type lvar in let ty' = intern_type (ids,true,tmpsc,sc) ty in let fvs = Implicit_quantifiers.generalizable_vars_of_rawconstr ~bound:ids ~allowed:ids' ty' in - let env' = List.fold_left (fun env (x, l) -> push_loc_name_env ~fail_anonymous lvar env l (Name x)) env fvs in + let env' = List.fold_left (fun env (x, l) -> push_name_env ~global_level lvar env (l, Name x)) env fvs in let bl = List.map (fun (id, loc) -> (Name id, b, None, RHole (loc, Evd.BinderType (Name id)))) fvs in let na = match na with | Anonymous -> - if fail_anonymous then na + if global_level then na else let name = let id = @@ -329,24 +324,24 @@ let intern_generalized_binder ?(fail_anonymous=false) intern_type lvar in Implicit_quantifiers.make_fresh ids' (Global.env ()) id in Name name | _ -> na - in (push_loc_name_env ~fail_anonymous lvar env' loc na), (na,b',None,ty') :: List.rev bl + in (push_name_env ~global_level lvar env' (loc,na)), (na,b',None,ty') :: List.rev bl -let intern_local_binder_aux ?(fail_anonymous=false) intern intern_type lvar ((ids,unb,ts,sc as env),bl) = function +let intern_local_binder_aux ?(global_level=false) intern intern_type lvar (env,bl) = function | LocalRawAssum(nal,bk,ty) -> (match bk with | Default k -> - let (loc,na) = List.hd nal in + 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 List.fold_left - (fun ((ids,unb,ts,sc),bl) (_,na) -> - ((name_fold Idset.add na ids,unb,ts,sc), (na,k,None,ty)::bl)) + (fun (env,bl) na -> + (push_name_env lvar env na,(snd na,k,None,ty)::bl)) (env,bl) nal | Generalized (b,b',t) -> - let env, b = intern_generalized_binder ~fail_anonymous intern_type lvar env bl (List.hd nal) b b' t ty in + let env, b = intern_generalized_binder ~global_level intern_type lvar env bl (List.hd nal) b b' t ty in env, b @ bl) - | LocalRawDef((loc,na),def) -> - ((name_fold Idset.add na ids,unb,ts,sc), + | LocalRawDef((loc,na as locna),def) -> + (push_name_env lvar env locna, (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl) let intern_generalization intern (ids,unb,tmp_scope,scopes as env) lvar loc bk ak c = @@ -369,7 +364,7 @@ let intern_generalization intern (ids,unb,tmp_scope,scopes as env) lvar loc bk a RLambda (join_loc loc' loc, Name id, bk, RHole (loc', Evd.BinderType (Name id)), acc)) in List.fold_right (fun (id, loc as lid) (env, acc) -> - let env' = push_loc_name_env lvar env loc (Name id) in + let env' = push_name_env lvar env (loc, Name id) in (env', abs lid acc)) fvs (env,c) in c' @@ -1101,9 +1096,9 @@ let internalize sigma globalenv env allow_patvar lvar c = intern env c2 | CLambdaN (loc,(nal,bk,ty)::bll,c2) -> iterate_lam loc (reset_tmp_scope env) bk ty (CLambdaN (loc, bll, c2)) nal - | CLetIn (loc,(loc1,na),c1,c2) -> - RLetIn (loc, na, intern (reset_tmp_scope env) c1, - intern (push_loc_name_env lvar env loc1 na) c2) + | CLetIn (loc,na,c1,c2) -> + RLetIn (loc, snd na, intern (reset_tmp_scope env) c1, + intern (push_name_env lvar env na) c2) | CNotation (loc,"- _",([CPrim (_,Numeral p)],[])) when Bigint.is_strictly_pos p -> intern env (CPrim (loc,Numeral (Bigint.neg p))) @@ -1171,7 +1166,7 @@ let internalize sigma globalenv env allow_patvar lvar c = let p' = Option.map (fun p -> let env'' = List.fold_left (push_name_env lvar) env ids in intern_type env'' p) po in - RLetTuple (loc, nal, (na', p'), b', + RLetTuple (loc, List.map snd nal, (na', p'), b', intern (List.fold_left (push_name_env lvar) env nal) c) | CIf (loc, c, (na,po), b1, b2) -> let env' = reset_tmp_scope env in @@ -1246,27 +1241,27 @@ let internalize sigma globalenv env allow_patvar lvar c = if List.length l <> nindargs then error_wrong_numarg_inductive_loc loc globalenv ind nindargs; let nal = List.map (function - | RHole loc -> Anonymous - | RVar (_,id) -> Name id + | RHole (loc,_) -> loc,Anonymous + | RVar (loc,id) -> loc,Name id | c -> user_err_loc (loc_of_rawconstr c,"",str "Not a name.")) l in let parnal,realnal = list_chop nparams nal in - if List.exists ((<>) Anonymous) parnal then + if List.exists (fun (_,na) -> na <> Anonymous) parnal then error_inductive_parameter_not_implicit loc; - realnal, Some (loc,ind,nparams,realnal) + realnal, Some (loc,ind,nparams,List.map snd realnal) | None -> [], None in let na = match tm', na with - | RVar (_,id), None when Idset.mem id vars -> Name id - | RRef (loc, VarRef id), None -> Name id - | _, None -> Anonymous - | _, Some na -> na in - (tm',(na,typ)), na::ids + | RVar (loc,id), None when Idset.mem id vars -> loc,Name id + | RRef (loc, VarRef id), None -> loc,Name id + | _, None -> dummy_loc,Anonymous + | _, Some (loc,na) -> loc,na in + (tm',(snd na,typ)), na::ids and iterate_prod loc2 env bk ty body nal = let rec default env bk = function - | (loc1,na)::nal -> + | (loc1,na as locna)::nal -> if nal <> [] then check_capture loc1 ty na; - let body = default (push_loc_name_env lvar env loc1 na) bk nal in + let body = default (push_name_env lvar env locna) bk nal in let ty = locate_if_isevar loc1 na (intern_type env ty) in RProd (join_loc loc1 loc2, na, bk, ty, body) | [] -> intern_type env body @@ -1281,9 +1276,9 @@ let internalize sigma globalenv env allow_patvar lvar c = and iterate_lam loc2 env bk ty body nal = let rec default env bk = function - | (loc1,na)::nal -> + | (loc1,na as locna)::nal -> if nal <> [] then check_capture loc1 ty na; - let body = default (push_loc_name_env lvar env loc1 na) bk nal in + let body = default (push_name_env lvar env locna) bk nal in let ty = locate_if_isevar loc1 na (intern_type env ty) in RLambda (join_loc loc1 loc2, na, bk, ty, body) | [] -> intern env body @@ -1488,10 +1483,10 @@ let my_intern_constr sigma env lvar acc c = let my_intern_type sigma env lvar acc c = my_intern_constr sigma env lvar (set_type_scope acc) c -let intern_context fail_anonymous sigma env params = +let intern_context global_level sigma env params = let lvar = (([],[]),Environ.named_context env, [], ([], [])) in snd (List.fold_left - (intern_local_binder_aux ~fail_anonymous (my_intern_constr sigma env lvar) (my_intern_type sigma env lvar) lvar) + (intern_local_binder_aux ~global_level (my_intern_constr sigma env lvar) (my_intern_type sigma env lvar) lvar) ((extract_ids env,false,None,[]), []) params) let interp_rawcontext_gen understand_type understand_judgment env bl = @@ -1517,15 +1512,15 @@ let interp_rawcontext_gen understand_type understand_judgment env bl = (env,[],1,[]) (List.rev bl) in (env, par), impls -let interp_context_gen understand_type understand_judgment ?(fail_anonymous=false) sigma env params = - let bl = intern_context fail_anonymous sigma env params in +let interp_context_gen understand_type understand_judgment ?(global_level=false) sigma env params = + let bl = intern_context global_level sigma env params in interp_rawcontext_gen understand_type understand_judgment env bl -let interp_context ?(fail_anonymous=false) sigma env params = +let interp_context ?(global_level=false) sigma env params = interp_context_gen (Default.understand_type sigma) - (Default.understand_judgment sigma) ~fail_anonymous sigma env params + (Default.understand_judgment sigma) ~global_level sigma env params -let interp_context_evars ?(fail_anonymous=false) evdref env params = +let interp_context_evars ?(global_level=false) evdref env params = interp_context_gen (fun env t -> Default.understand_tcc_evars evdref env IsType t) - (Default.understand_judgment_tcc evdref) ~fail_anonymous !evdref env params + (Default.understand_judgment_tcc evdref) ~global_level !evdref env params |