diff options
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 160 |
1 files changed, 97 insertions, 63 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 74de6f67ff..4502aa7ace 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Nameops @@ -33,10 +33,10 @@ open Context.Rel.Declaration (** constr_expr -> glob_constr translation: - it adds holes for implicit arguments - - it remplaces notations by their value (scopes stuff are here) + - it replaces notations by their value (scopes stuff are here) - it recognizes global vars from local ones - - it prepares pattern maching problems (a pattern becomes a tree where nodes - are constructor/variable pairs and leafs are variables) + - it prepares pattern matching problems (a pattern becomes a tree + where nodes are constructor/variable pairs and leafs are variables) All that at once, fasten your seatbelt! *) @@ -432,11 +432,6 @@ let intern_assumption intern lvar env nal bk ty = let env, b = intern_generalized_binder intern_type lvar env (List.hd nal) b b' t ty in env, b -let obj_string x = - if Obj.is_block (Obj.repr x) then - "tag = " ^ string_of_int (Obj.tag (Obj.repr x)) - else "int_val = " ^ string_of_int (Obj.magic x) - let rec free_vars_of_pat il = function | CPatCstr (loc, c, l1, l2) -> @@ -481,9 +476,14 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio let bl' = List.map (fun a -> BDRawDef a) bl' in env, bl' @ bl | LocalRawDef((loc,na as locna),def) -> - let indef = intern env def in + let indef = intern env def in + let term, ty = + match indef with + | GCast (loc, b, Misctypes.CastConv t) -> b, t + | _ -> indef, GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) + in (push_name_env lvar (impls_term_list indef) env locna, - (BDRawDef ((loc,(na,Explicit,Some(indef),GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None)))))::bl) + (BDRawDef ((loc,(na,Explicit,Some(term),ty))))::bl) | LocalPattern (loc,p,ty) -> let tyc = match ty with @@ -599,31 +599,52 @@ let rec subordinate_letins intern letins = function | [] -> letins,[] -let rec subst_iterator y t = function - | GVar (_,id) as x -> if Id.equal id y then t else x - | x -> map_glob_constr (subst_iterator y t) x +let terms_of_binders bl = + let rec term_of_pat = function + | PatVar (loc,Name id) -> CRef (Ident (loc,id), None) + | PatVar (loc,Anonymous) -> error "Cannot turn \"_\" into a term." + | PatCstr (loc,c,l,_) -> + let r = Qualid (loc,qualid_of_path (path_of_global (ConstructRef c))) in + let hole = CHole (loc,None,Misctypes.IntroAnonymous,None) in + let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in + CAppExpl (loc,(None,r,None),params @ List.map term_of_pat l) in + let rec extract_variables = function + | BDRawDef (loc,(Name id,_,None,_))::l -> CRef (Ident (loc,id), None) :: extract_variables l + | BDRawDef (loc,(Name id,_,Some _,_))::l -> extract_variables l + | BDRawDef (loc,(Anonymous,_,_,_))::l -> error "Cannot turn \"_\" into a term." + | BDPattern (loc,(u,_),lvar,env,tyc) :: l -> term_of_pat u :: extract_variables l + | [] -> [] in + extract_variables bl let instantiate_notation_constr loc intern ntnvars subst infos c = let (terms,termlists,binders) = subst in (* when called while defining a notation, avoid capturing the private binders of the expression by variables bound by the notation (see #3892) *) let avoid = Id.Map.domain ntnvars in - let rec aux (terms,binderopt as subst') (renaming,env) c = + let rec aux (terms,binderopt,terminopt as subst') (renaming,env) c = let subinfos = renaming,{env with tmp_scope = None} in match c with + | NVar id when Id.equal id ldots_var -> Option.get terminopt | NVar id -> subst_var subst' (renaming, env) id - | NList (x,_,iter,terminator,lassoc) -> - (try + | NList (x,y,iter,terminator,lassoc) -> + let l,(scopt,subscopes) = (* All elements of the list are in scopes (scopt,subscopes) *) - let (l,(scopt,subscopes)) = Id.Map.find x termlists in - let termin = aux subst' subinfos terminator in - let fold a t = - let nterms = Id.Map.add x (a, (scopt, subscopes)) terms in - subst_iterator ldots_var t (aux (nterms, binderopt) subinfos iter) - in - List.fold_right fold (if lassoc then List.rev l else l) termin - with Not_found -> - anomaly (Pp.str "Inconsistent substitution of recursive notation")) + try + let l,scopes = Id.Map.find x termlists in + (if lassoc then List.rev l else l),scopes + with Not_found -> + try + let (bl,(scopt,subscopes)) = Id.Map.find x binders in + let env,bl' = List.fold_left (intern_local_binder_aux intern ntnvars) (env,[]) bl in + terms_of_binders (if lassoc then bl' else List.rev bl'),(None,[]) + with Not_found -> + anomaly (Pp.str "Inconsistent substitution of recursive notation") in + let termin = aux (terms,None,None) subinfos terminator in + let fold a t = + let nterms = Id.Map.add y (a, (scopt, subscopes)) terms in + aux (nterms,None,Some t) subinfos iter + in + List.fold_right fold l termin | NHole (knd, naming, arg) -> let knd = match knd with | Evar_kinds.BinderType (Name id as na) -> @@ -658,16 +679,15 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = Some arg in GHole (loc, knd, naming, arg) - | NBinderList (x,_,iter,terminator) -> + | NBinderList (x,y,iter,terminator) -> (try (* All elements of the list are in scopes (scopt,subscopes) *) let (bl,(scopt,subscopes)) = Id.Map.find x binders in let env,bl = List.fold_left (intern_local_binder_aux intern ntnvars) (env,[]) bl in let letins,bl = subordinate_letins intern [] bl in - let termin = aux subst' (renaming,env) terminator in + let termin = aux (terms,None,None) (renaming,env) terminator in let res = List.fold_left (fun t binder -> - subst_iterator ldots_var t - (aux (terms,Some(x,binder)) subinfos iter)) + aux (terms,Some(y,binder),Some t) subinfos iter) termin bl in make_letins letins res with Not_found -> @@ -695,7 +715,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = | t -> glob_constr_of_notation_constr_with_binders loc (traverse_binder subst avoid) (aux subst') subinfos t - and subst_var (terms, binderopt) (renaming, env) id = + and subst_var (terms, _binderopt, _terminopt) (renaming, env) id = (* subst remembers the delimiters stack in the interpretation *) (* of the notations *) try @@ -708,7 +728,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = with Not_found -> (* Happens for local notation joint with inductive/fixpoint defs *) GVar (loc,id) - in aux (terms,None) infos c + in aux (terms,None,None) infos c let split_by_type ids = List.fold_right (fun (x,(scl,typ)) (l1,l2,l3) -> @@ -741,7 +761,13 @@ let string_of_ty = function | Method -> "meth" | Variable -> "var" -let intern_var genv (ltacvars,ntnvars) namedctx loc id = +let gvar (loc, id) us = match us with +| None -> GVar (loc, id) +| Some _ -> + user_err_loc (loc, "", str "Variable " ++ pr_id id ++ + str " cannot have a universe instance") + +let intern_var genv (ltacvars,ntnvars) namedctx loc id us = (* Is [id] an inductive type potentially with implicit *) try let ty,expl_impls,impls,argsc = Id.Map.find id genv.impls in @@ -749,21 +775,21 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id = (fun id -> CRef (Ident (loc,id),None), Some (loc,ExplByName id)) expl_impls in let tys = string_of_ty ty in Dumpglob.dump_reference loc "<>" (Id.to_string id) tys; - GVar (loc,id), make_implicits_list impls, argsc, expl_impls + gvar (loc,id) us, make_implicits_list impls, argsc, expl_impls with Not_found -> (* Is [id] bound in current term or is an ltac var bound to constr *) if Id.Set.mem id genv.ids || Id.Set.mem id ltacvars.ltac_vars then - GVar (loc,id), [], [], [] + gvar (loc,id) us, [], [], [] (* Is [id] a notation variable *) else if Id.Map.mem id ntnvars then - (set_var_scope loc id true genv ntnvars; GVar (loc,id), [], [], []) + (set_var_scope loc id true genv ntnvars; gvar (loc,id) us, [], [], []) (* Is [id] the special variable for recursive notations *) else if Id.equal id ldots_var then if Id.Map.is_empty ntnvars then error_ldots_var loc - else GVar (loc,id), [], [], [] + else gvar (loc,id) us, [], [], [] else if Id.Set.mem id ltacvars.ltac_bound then (* Is [id] bound to a free name in ltac (this is an ltac error message) *) user_err_loc (loc,"intern_var", @@ -778,10 +804,10 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id = let impls = implicits_of_global ref in let scopes = find_arguments_scope ref in Dumpglob.dump_reference loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var"; - GRef (loc, ref, None), impls, scopes, [] - with e when Errors.noncritical e -> + GRef (loc, ref, us), impls, scopes, [] + with e when CErrors.noncritical e -> (* [id] a goal variable *) - GVar (loc,id), [], [], [] + gvar (loc,id) us, [], [], [] let find_appl_head_data c = match c with @@ -843,9 +869,12 @@ let intern_qualid loc qid intern env lvar us args = let c = match us, c with | None, _ -> c | Some _, GRef (loc, ref, None) -> GRef (loc, ref, us) + | Some _, GApp (loc, GRef (loc', ref, None), arg) -> + GApp (loc, GRef (loc', ref, us), arg) | Some _, _ -> user_err_loc (loc, "", str "Notation " ++ pr_qualid qid ++ - str " cannot have a universe instance") + str " cannot have a universe instance, its expanded head + does not start with a reference") in c, projapp, args2 @@ -864,7 +893,7 @@ let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args = let x, imp, scopes, l = find_appl_head_data r in (x,imp,scopes,l), args2 | Ident (loc, id) -> - try intern_var env lvar namedctx loc id, args + try intern_var env lvar namedctx loc id us, args with Not_found -> let qid = qualid_of_ident id in try @@ -874,7 +903,7 @@ let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args = with Not_found -> (* Extra allowance for non globalizing functions *) if !interning_grammar || env.unb then - (GVar (loc,id), [], [], []), args + (gvar (loc,id) us, [], [], []), args else error_global_not_found_loc loc qid let interp_reference vars r = @@ -1049,12 +1078,10 @@ let sort_fields ~complete loc fields completer = match fields with | [] -> None | (first_field_ref, first_field_value):: other_fields -> - let env_error_msg = "Environment corruption for records." in - let first_field_glob_ref = - try global_reference_of_reference first_field_ref - with Not_found -> anomaly (Pp.str env_error_msg) in - let record = - try Recordops.find_projection first_field_glob_ref + let (first_field_glob_ref, record) = + try + let gr = global_reference_of_reference first_field_ref in + (gr, Recordops.find_projection gr) with Not_found -> user_err_loc (loc_of_reference first_field_ref, "intern", pr_reference first_field_ref ++ str": Not a projection") @@ -1065,7 +1092,8 @@ let sort_fields ~complete loc fields completer = let base_constructor = let global_record_id = ConstructRef record.Recordops.s_CONST in try Qualid (loc, shortest_qualid_of_global Id.Set.empty global_record_id) - with Not_found -> anomaly (Pp.str env_error_msg) in + with Not_found -> + anomaly (str "Environment corruption for records") in let (end_index, (* one past the last field index *) first_field_index, (* index of the first field of the record *) proj_list) (* list of projections *) @@ -1315,7 +1343,7 @@ let drop_notations_pattern looked_for = RCPatCstr (loc, g, List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl @ List.map (in_pat false scopes) args, []) - | NList (x,_,iter,terminator,lassoc) -> + | NList (x,y,iter,terminator,lassoc) -> if not (List.is_empty args) then user_err_loc (loc,"",strbrk "Application of arguments to a recursive notation not supported in patterns."); (try @@ -1323,7 +1351,7 @@ let drop_notations_pattern looked_for = let (l,(scopt,subscopes)) = Id.Map.find x substlist in let termin = in_not top loc scopes fullsubst [] terminator in List.fold_right (fun a t -> - let nsubst = Id.Map.add x (a, (scopt, subscopes)) subst in + let nsubst = Id.Map.add y (a, (scopt, subscopes)) subst in let u = in_not false loc scopes (nsubst, substlist) [] iter in subst_pat_iterator ldots_var t u) (if lassoc then List.rev l else l) termin @@ -1600,11 +1628,13 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = (merge_impargs l args) loc | CRecord (loc, fs) -> - let fields = - sort_fields ~complete:true loc fs - (fun _idx -> CHole (loc, Some (Evar_kinds.QuestionMark (Evar_kinds.Define true)), Misctypes.IntroAnonymous, None)) - in - begin + let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in + let fields = + sort_fields ~complete:true loc fs + (fun _idx -> CHole (loc, Some (Evar_kinds.QuestionMark st), + Misctypes.IntroAnonymous, None)) + in + begin match fields with | None -> user_err_loc (loc, "intern", str"No constructor inference.") | Some (n, constrname, args) -> @@ -1674,7 +1704,9 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = GIf (loc, c', (na', p'), intern env b1, intern env b2) | CHole (loc, k, naming, solve) -> let k = match k with - | None -> Evar_kinds.QuestionMark (Evar_kinds.Define true) + | None -> + let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in + Evar_kinds.QuestionMark st | Some k -> k in let solve = match solve with @@ -2021,11 +2053,13 @@ let interp_rawcontext_evars env evdref k bl = let (env, par, _, impls) = List.fold_left (fun (env,params,n,impls) (na, k, b, t) -> + let t' = + if Option.is_empty b then locate_if_hole (loc_of_glob_constr t) na t + else t + in + let t = understand_tcc_evars env evdref ~expected_type:IsType t' in match b with None -> - let t' = locate_if_hole (loc_of_glob_constr t) na t in - let t = - understand_tcc_evars env evdref ~expected_type:IsType t' in let d = LocalAssum (na,t) in let impls = if k == Implicit then @@ -2035,8 +2069,8 @@ let interp_rawcontext_evars env evdref k bl = in (push_rel d env, d::params, succ n, impls) | Some b -> - let c = understand_judgment_tcc env evdref b in - let d = LocalDef (na, c.uj_val, c.uj_type) in + let c = understand_tcc_evars env evdref ~expected_type:(OfType t) b in + let d = LocalDef (na, c, t) in (push_rel d env, d::params, n, impls)) (env,[],k+1,[]) (List.rev bl) in (env, par), impls |