diff options
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 316 |
1 files changed, 129 insertions, 187 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index a071ba7ec9..f82783f47d 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -48,22 +48,27 @@ open NumTok types and recursive definitions and of projection names in records *) type var_internalization_type = - | Inductive of Id.t list (* list of params *) * bool (* true = check for possible capture *) + | Inductive | Recursive | Method | Variable +type var_unique_id = string + +let var_uid = + let count = ref 0 in + fun id -> incr count; Id.to_string id ^ ":" ^ string_of_int !count + type var_internalization_data = (* type of the "free" variable, for coqdoc, e.g. while typing the constructor of JMeq, "JMeq" behaves as a variable of type Inductive *) var_internalization_type * - (* impargs to automatically add to the variable, e.g. for "JMeq A a B b" - in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *) - Id.t list * (* signature of impargs of the variable *) Impargs.implicit_status list * (* subscopes of the args of the variable *) - scope_name option list + scope_name option list * + (* unique ID for coqdoc links *) + var_unique_id type internalization_env = (var_internalization_data) Id.Map.t @@ -180,26 +185,18 @@ let parsing_explicit = ref false let empty_internalization_env = Id.Map.empty -let compute_explicitable_implicit imps = function - | Inductive (params,_) -> - (* In inductive types, the parameters are fixed implicit arguments *) - let sub_impl,_ = List.chop (List.length params) imps in - let sub_impl' = List.filter is_status_implicit sub_impl in - List.map name_of_implicit sub_impl' - | Recursive | Method | Variable -> - (* Unable to know in advance what the implicit arguments will be *) - [] - -let compute_internalization_data env sigma ty typ impl = +let compute_internalization_data env sigma id ty typ impl = let impl = compute_implicits_with_manual env sigma typ (is_implicit_args()) impl in - let expls_impl = compute_explicitable_implicit impl ty in - (ty, expls_impl, impl, compute_arguments_scope sigma typ) + (ty, impl, compute_arguments_scope sigma typ, var_uid id) let compute_internalization_env env sigma ?(impls=empty_internalization_env) ty = List.fold_left3 - (fun map id typ impl -> Id.Map.add id (compute_internalization_data env sigma ty typ impl) map) + (fun map id typ impl -> Id.Map.add id (compute_internalization_data env sigma id ty typ impl) map) impls +let extend_internalization_data (r, impls, scopes, uid) impl scope = + (r, impls@[impl], scopes@[scope], uid) + (**********************************************************************) (* Contracting "{ _ }" in notations *) @@ -355,7 +352,7 @@ let impls_binder_list = let impls_type_list n ?(args = []) = let rec aux acc n c = match DAst.get c with | GProd (na,bk,_,c) -> aux (build_impls n bk na acc) (n+1) c - | _ -> (Variable,[],List.rev acc,[]) + | _ -> List.rev acc in aux args n let impls_term_list n ?(args = []) = @@ -365,7 +362,7 @@ let impls_term_list n ?(args = []) = let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in let n,acc' = List.fold_left (fun (n,acc) (na, bk, _, _) -> (n+1,build_impls n bk na acc)) (n,acc) args.(nb) in aux acc' n bds.(nb) - |_ -> (Variable,[],List.rev acc,[]) + |_ -> List.rev acc in aux args n (* Check if in binder "(x1 x2 .. xn : t)", none of x1 .. xn-1 occurs in t *) @@ -429,20 +426,6 @@ let locate_if_hole ?loc na c = match DAst.get c with with Not_found -> DAst.make ?loc @@ GHole (Evar_kinds.BinderType na, naming, arg)) | _ -> c -let reset_hidden_inductive_implicit_test env = - { env with impls = Id.Map.map (function - | (Inductive (params,_),b,c,d) -> (Inductive (params,false),b,c,d) - | x -> x) env.impls } - -let check_hidden_implicit_parameters ?loc id impls = - if Id.Map.exists (fun _ -> function - | (Inductive (indparams,check),_,_,_) when check -> Id.List.mem id indparams - | _ -> false) impls - then - user_err ?loc (Id.print id ++ strbrk " is already used as name of " ++ - strbrk "a parameter of the inductive type; bound variables in " ++ - strbrk "the type of a constructor shall use a different name.") - let pure_push_name_env (id,implargs) env = {env with ids = Id.Set.add id env.ids; @@ -456,12 +439,12 @@ let push_name_env ntnvars implargs env = | { loc; v = Anonymous } -> env | { loc; v = Name id } -> - check_hidden_implicit_parameters ?loc id env.impls ; if Id.Map.is_empty ntnvars && Id.equal id ldots_var then error_ldots_var ?loc; set_var_scope ?loc id false (env.tmp_scope,env.scopes) ntnvars; - Dumpglob.dump_binding ?loc id; - pure_push_name_env (id,implargs) env + let uid = var_uid id in + Dumpglob.dump_binding ?loc uid; + pure_push_name_env (id,(Variable,implargs,[],uid)) env let remember_binders_impargs env bl = List.map_filter (fun (na,_,_,_) -> @@ -492,7 +475,7 @@ let intern_generalized_binder intern_type ntnvars let ty' = intern_type {env with ids = ids; unb = true} ty in let fvs = Implicit_quantifiers.generalizable_vars_of_glob_constr ~bound:ids ~allowed:ids' ty' in let env' = List.fold_left - (fun env {loc;v=x} -> push_name_env ntnvars (Variable,[],[],[])(*?*) env (make ?loc @@ Name x)) + (fun env {loc;v=x} -> push_name_env ntnvars [](*?*) env (make ?loc @@ Name x)) env fvs in let b' = check_implicit_meaningful ?loc b' env in let bl = List.map @@ -559,7 +542,7 @@ let intern_cases_pattern_as_binder ?loc ntnvars env p = user_err ?loc (str "Unsupported nested \"as\" clause."); il,disjpat in - let env = List.fold_right (fun {loc;v=id} env -> push_name_env ntnvars (Variable,[],[],[]) env (make ?loc @@ Name id)) il env in + let env = List.fold_right (fun {loc;v=id} env -> push_name_env ntnvars [] env (make ?loc @@ Name id)) il env in let na = alias_of_pat (List.hd disjpat) in let ienv = Name.fold_right Id.Set.remove na env.ids in let id = Namegen.next_name_away_with_default "pat" na ienv in @@ -615,7 +598,7 @@ let intern_generalization intern env ntnvars loc bk ak c = GLambda (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None), acc)) in List.fold_right (fun ({loc;v=id} as lid) (env, acc) -> - let env' = push_name_env ntnvars (Variable,[],[],[]) env CAst.(make @@ Name id) in + let env' = push_name_env ntnvars [] env CAst.(make @@ Name id) in (env', abs lid acc)) fvs (env,c) in c' @@ -706,7 +689,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam if onlyident then (* Do not try to interpret a variable as a constructor *) let na = out_patvar pat in - let env = push_name_env ntnvars (Variable,[],[],[]) env (make ?loc:pat.loc na) in + let env = push_name_env ntnvars [] env (make ?loc:pat.loc na) in (renaming,env), None, na else (* Interpret as a pattern *) @@ -909,9 +892,6 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = try let pat,(onlyident,scopes) = Id.Map.find id binders in let env = set_env_scopes env scopes in - (* We deactivate impls to avoid the check on hidden parameters *) - (* and since we are only interested in the pattern as a term *) - let env = reset_hidden_inductive_implicit_test env in if onlyident then term_of_name (out_patvar pat) else @@ -1015,13 +995,13 @@ let intern_notation intern env ntnvars loc ntn fullargs = (* Discriminating between bound variables and global references *) let string_of_ty = function - | Inductive _ -> "ind" + | Inductive -> "ind" | Recursive -> "def" | Method -> "meth" | Variable -> "var" let gvar (loc, id) us = match us with -| None -> DAst.make ?loc @@ GVar id +| None | Some [] -> DAst.make ?loc @@ GVar id | Some _ -> user_err ?loc (str "Variable " ++ Id.print id ++ str " cannot have a universe instance") @@ -1031,27 +1011,25 @@ let intern_var env (ltacvars,ntnvars) namedctx loc id us = if Id.Map.mem id ntnvars then begin if not (Id.Map.mem id env.impls) then set_var_scope ?loc id true (env.tmp_scope,env.scopes) ntnvars; - gvar (loc,id) us, [], [], [] + gvar (loc,id) us, [], [] end else (* Is [id] registered with implicit arguments *) try - let ty,expl_impls,impls,argsc = Id.Map.find id env.impls in - let expl_impls = List.map - (fun id -> CAst.make ?loc @@ CRef (qualid_of_ident ?loc id,None), Some (make ?loc @@ ExplByName id)) expl_impls in + let ty,impls,argsc,uid = Id.Map.find id env.impls in let tys = string_of_ty ty in - Dumpglob.dump_reference ?loc "<>" (Id.to_string id) tys; - gvar (loc,id) us, make_implicits_list impls, argsc, expl_impls + Dumpglob.dump_reference ?loc "<>" uid tys; + gvar (loc,id) us, make_implicits_list impls, argsc with Not_found -> (* Is [id] bound in current term or is an ltac var bound to constr *) if Id.Set.mem id env.ids || Id.Set.mem id ltacvars.ltac_vars then - gvar (loc,id) us, [], [], [] + gvar (loc,id) us, [], [] else if Id.equal id ldots_var (* Is [id] the special variable for recursive notations? *) then if Id.Map.is_empty ntnvars then error_ldots_var ?loc - else gvar (loc,id) us, [], [], [] + 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 ~hdr:"intern_var" @@ -1067,17 +1045,17 @@ let intern_var env (ltacvars,ntnvars) namedctx loc id us = let scopes = find_arguments_scope ref in Dumpglob.dump_secvar ?loc id; (* this raises Not_found when not a section variable *) (* Someday we should stop relying on Dumglob raising exceptions *) - DAst.make ?loc @@ GRef (ref, us), impls, scopes, [] + DAst.make ?loc @@ GRef (ref, us), impls, scopes with e when CErrors.noncritical e -> (* [id] a goal variable *) - gvar (loc,id) us, [], [], [] + gvar (loc,id) us, [], [] let find_appl_head_data c = match DAst.get c with | GRef (ref,_) -> let impls = implicits_of_global ref in let scopes = find_arguments_scope ref in - c, impls, scopes, [] + c, impls, scopes | GApp (r, l) -> begin match DAst.get r with | GRef (ref,_) -> @@ -1085,10 +1063,10 @@ let find_appl_head_data c = let impls = implicits_of_global ref in let scopes = find_arguments_scope ref in c, (if n = 0 then [] else List.map (drop_first_implicits n) impls), - List.skipn_at_least n scopes,[] - | _ -> c,[],[],[] + List.skipn_at_least n scopes + | _ -> c,[],[] end - | _ -> c,[],[],[] + | _ -> c,[],[] let error_not_enough_arguments ?loc = user_err ?loc (str "Abbreviation is not applied enough.") @@ -1196,13 +1174,12 @@ let intern_applied_reference ~isproj intern env namedctx (_, ntnvars as lvar) us try let r, realref, args2 = intern_qualid ~no_secvar:true qid intern env ntnvars us args in check_applied_projection isproj realref qid; - let x, imp, scopes, l = find_appl_head_data r in - (x,imp,scopes,l), args2 + find_appl_head_data r, args2 with Not_found -> (* Extra allowance for non globalizing functions *) if !interning_grammar || env.unb then (* check_applied_projection ?? *) - (gvar (loc,qualid_basename qid) us, [], [], []), args + (gvar (loc,qualid_basename qid) us, [], []), args else Nametab.error_global_not_found qid else let r,realref,args2 = @@ -1210,11 +1187,10 @@ let intern_applied_reference ~isproj intern env namedctx (_, ntnvars as lvar) us with Not_found -> Nametab.error_global_not_found qid in check_applied_projection isproj realref qid; - let x, imp, scopes, l = find_appl_head_data r in - (x,imp,scopes,l), args2 + find_appl_head_data r, args2 let interp_reference vars r = - let (r,_,_,_),_ = + let (r,_,_),_ = intern_applied_reference ~isproj:None (fun _ -> error_not_enough_arguments ?loc:None) {ids = Id.Set.empty; unb = false ; tmp_scope = None; scopes = []; impls = empty_internalization_env; @@ -1452,62 +1428,28 @@ let inductive_of_record loc record = let sort_fields ~complete loc fields completer = match fields with | [] -> None - | (first_field_ref, first_field_value):: other_fields -> + | (first_field_ref, _):: _ -> let (first_field_glob_ref, record) = try let gr = locate_reference first_field_ref in + Dumpglob.add_glob ?loc:first_field_ref.CAst.loc gr; (gr, Recordops.find_projection gr) with Not_found -> - raise (InternalizationError(loc, NotAProjection first_field_ref)) + raise (InternalizationError(first_field_ref.CAst.loc, NotAProjection first_field_ref)) in (* the number of parameters *) let nparams = record.Recordops.s_EXPECTEDPARAM in (* the reference constructor of the record *) - let base_constructor = - let global_record_id = GlobRef.ConstructRef record.Recordops.s_CONST in - try Nametab.shortest_qualid_of_global ?loc Id.Set.empty global_record_id - with Not_found -> - anomaly (str "Environment corruption for records.") in + let base_constructor = GlobRef.ConstructRef record.Recordops.s_CONST in let () = check_duplicate ?loc fields 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 *) - = - (* eliminate the first field from the projections, - but keep its index *) - let rec build_proj_list projs proj_kinds idx ~acc_first_idx acc = - match projs with - | [] -> (idx, acc_first_idx, acc) - | (Some field_glob_id) :: projs -> - let field_glob_ref = GlobRef.ConstRef field_glob_id in - let first_field = GlobRef.equal field_glob_ref first_field_glob_ref in - begin match proj_kinds with - | [] -> anomaly (Pp.str "Number of projections mismatch.") - | { Recordops.pk_true_proj = regular } :: proj_kinds -> - (* "regular" is false when the field is defined - by a let-in in the record declaration - (its value is fixed from other fields). *) - if first_field && not regular && complete then - user_err ?loc (str "No local fields allowed in a record construction.") - else if first_field then - build_proj_list projs proj_kinds (idx+1) ~acc_first_idx:idx acc - else if not regular && complete then - (* skip non-regular fields *) - build_proj_list projs proj_kinds idx ~acc_first_idx acc - else - build_proj_list projs proj_kinds (idx+1) ~acc_first_idx - ((idx, field_glob_id) :: acc) - end - | None :: projs -> - if complete then - (* we don't want anonymous fields *) - user_err ?loc (str "This record contains anonymous fields.") - else - (* anonymous arguments don't appear in proj_kinds *) - build_proj_list projs proj_kinds (idx+1) ~acc_first_idx acc - in - build_proj_list record.Recordops.s_PROJ record.Recordops.s_PROJKIND 1 ~acc_first_idx:0 [] - in + let build_proj idx proj kind = + if proj = None && complete then + (* we don't want anonymous fields *) + user_err ?loc (str "This record contains anonymous fields.") + else + (idx, proj, kind.Recordops.pk_true_proj) in + let proj_list = + List.map2_i build_proj 1 record.Recordops.s_PROJ record.Recordops.s_PROJKIND in (* now we want to have all fields assignments indexed by their place in the constructor *) let rec index_fields fields remaining_projs acc = @@ -1515,34 +1457,43 @@ let sort_fields ~complete loc fields completer = | (field_ref, field_value) :: fields -> let field_glob_ref = try locate_reference field_ref with Not_found -> - user_err ?loc ~hdr:"intern" + user_err ?loc:field_ref.CAst.loc ~hdr:"intern" (str "The field \"" ++ pr_qualid field_ref ++ str "\" does not exist.") in - let this_field_record = try Recordops.find_projection field_glob_ref - with Not_found -> - let inductive_ref = inductive_of_record loc record in - raise (InternalizationError(loc, NotAProjectionOf (field_ref, inductive_ref))) - in - let remaining_projs, (field_index, _) = - let the_proj (idx, glob_id) = GlobRef.equal field_glob_ref (GlobRef.ConstRef glob_id) in + let remaining_projs, (field_index, _, regular) = + let the_proj = function + | (idx, Some glob_id, _) -> GlobRef.equal field_glob_ref (GlobRef.ConstRef glob_id) + | (idx, None, _) -> false in try CList.extract_first the_proj remaining_projs with Not_found -> - let ind1 = inductive_of_record loc record in - let ind2 = inductive_of_record loc this_field_record in + let floc = field_ref.CAst.loc in + let this_field_record = + try Recordops.find_projection field_glob_ref + with Not_found -> + let inductive_ref = inductive_of_record floc record in + raise (InternalizationError(floc, NotAProjectionOf (field_ref, inductive_ref))) in + let ind1 = inductive_of_record floc record in + let ind2 = inductive_of_record floc this_field_record in raise (InternalizationError(loc, ProjectionsOfDifferentRecords (ind1, ind2))) in + if not regular && complete then + (* "regular" is false when the field is defined + by a let-in in the record declaration + (its value is fixed from other fields). *) + user_err ?loc (str "No local fields allowed in a record construction."); + Dumpglob.add_glob ?loc:field_ref.CAst.loc field_glob_ref; index_fields fields remaining_projs ((field_index, field_value) :: acc) | [] -> - (* the order does not matter as we sort them next, - List.rev_* is just for efficiency *) let remaining_fields = - let complete_field (idx, field_ref) = (idx, - completer idx field_ref record.Recordops.s_CONST) in - List.rev_map complete_field remaining_projs in + let complete_field (idx, field_ref, regular) = + if not regular && complete then + (* For terms, we keep only regular fields *) + None + else + Some (idx, completer idx field_ref record.Recordops.s_CONST) in + List.map_filter complete_field remaining_projs in List.rev_append remaining_fields acc in - let unsorted_indexed_fields = - index_fields other_fields proj_list - [(first_field_index, first_field_value)] in + let unsorted_indexed_fields = index_fields fields proj_list [] in let sorted_indexed_fields = let cmp_by_index (i, _) (j, _) = Int.compare i j in List.sort cmp_by_index unsorted_indexed_fields in @@ -1701,9 +1652,9 @@ let drop_notations_pattern looked_for genv = if get_asymmetric_patterns () then pl else let pars = List.make n (CAst.make ?loc @@ CPatAtom None) in List.rev_append pars pl in - match drop_syndef top scopes head pl with - | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr(a, b, c) - | None -> raise (InternalizationError (loc,NotAConstructor head)) + let (_,argscs) = find_remaining_scopes [] pl head in + let pats = List.map2 (in_pat_sc scopes) argscs pl in + DAst.make ?loc @@ RCPatCstr(head, [], pats) end | CPatCstr (head, None, pl) -> begin @@ -1882,18 +1833,6 @@ let intern_ind_pattern genv ntnvars scopes pat = (**********************************************************************) (* Utilities for application *) -let merge_impargs l args = - let test x = function - | (_, Some {v=y}) -> explicitation_eq x y - | _ -> false - in - List.fold_right (fun a l -> - match a with - | (_, Some {v=ExplByName id as x}) when - List.exists (test x) args -> l - | _ -> a::l) - l args - let get_implicit_name n imps = Some (Impargs.name_of_implicit (List.nth imps (n-1))) @@ -1954,11 +1893,11 @@ let extract_explicit_arg imps args = let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let rec intern env = CAst.with_loc_val (fun ?loc -> function | CRef (ref,us) -> - let (c,imp,subscopes,l),_ = + let (c,imp,subscopes),_ = intern_applied_reference ~isproj:None intern env (Environ.named_context_val globalenv) lvar us [] ref in - apply_impargs c env imp subscopes l loc + apply_impargs c env imp subscopes [] loc | CFix ({ CAst.loc = locid; v = iddef}, dl) -> let lf = List.map (fun ({CAst.v = id},_,_,_,_) -> id) dl in @@ -2053,8 +1992,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | CNotation (_,(InConstrEntrySomeLevel,"( _ )"),([a],[],[],[])) -> intern env a | CNotation (_,ntn,args) -> let c = intern_notation intern env ntnvars loc ntn args in - let x, impl, scopes, l = find_appl_head_data c in - apply_impargs x env impl scopes l loc + let x, impl, scopes = find_appl_head_data c in + apply_impargs x env impl scopes [] loc | CGeneralization (b,a,c) -> intern_generalization intern env ntnvars loc b a c | CPrim p -> @@ -2063,7 +2002,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = intern {env with tmp_scope = None; scopes = find_delimiters_scope ?loc key :: env.scopes} e | CAppExpl ((isproj,ref,us), args) -> - let (f,_,args_scopes,_),args = + let (f,_,args_scopes),args = let args = List.map (fun a -> (a,None)) args in intern_applied_reference ~isproj intern env (Environ.named_context_val globalenv) lvar us args ref @@ -2074,25 +2013,24 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = smart_gapp f loc (intern_args env args_scopes (List.map fst args)) | CApp ((isproj,f), args) -> - let isproj,f,args = match f.CAst.v with - (* Compact notations like "t.(f args') args" *) - | CApp ((Some _ as isproj',f), args') when not (Option.has_some isproj) -> - isproj',f,args'@args - (* Don't compact "(f args') args" to resolve implicits separately *) - | _ -> isproj,f,args in - let (c,impargs,args_scopes,l),args = - match f.CAst.v with - | CRef (ref,us) -> - intern_applied_reference ~isproj intern env - (Environ.named_context_val globalenv) lvar us args ref - | CNotation (_,ntn,ntnargs) -> - assert (Option.is_empty isproj); - let c = intern_notation intern env ntnvars loc ntn ntnargs in - let x, impl, scopes, l = find_appl_head_data c in - (x,impl,scopes,l), args - | _ -> assert (Option.is_empty isproj); (intern_no_implicit env f,[],[],[]), args in - apply_impargs c env impargs args_scopes - (merge_impargs l args) loc + let isproj,f,args = match f.CAst.v with + (* Compact notations like "t.(f args') args" *) + | CApp ((Some _ as isproj',f), args') when not (Option.has_some isproj) -> + isproj',f,args'@args + (* Don't compact "(f args') args" to resolve implicits separately *) + | _ -> isproj,f,args in + let (c,impargs,args_scopes),args = + match f.CAst.v with + | CRef (ref,us) -> + intern_applied_reference ~isproj intern env + (Environ.named_context_val globalenv) lvar us args ref + | CNotation (_,ntn,ntnargs) -> + assert (Option.is_empty isproj); + let c = intern_notation intern env ntnvars loc ntn ntnargs in + find_appl_head_data c, args + | _ -> assert (Option.is_empty isproj); (intern_no_implicit env f,[],[]), args in + apply_impargs c env impargs args_scopes + args loc | CRecord fs -> let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in @@ -2101,7 +2039,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = (fun _idx fieldname constructorname -> let open Evar_kinds in let fieldinfo : Evar_kinds.record_field = - {fieldname=fieldname; recordname=inductive_of_constructor constructorname} + {fieldname=Option.get fieldname; recordname=inductive_of_constructor constructorname} in CAst.make ?loc @@ CHole (Some (Evar_kinds.QuestionMark { Evar_kinds.default_question_mark with @@ -2113,10 +2051,12 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = match fields with | None -> user_err ?loc ~hdr:"intern" (str"No constructor inference.") | Some (n, constrname, args) -> + let args_scopes = find_arguments_scope constrname in let pars = List.make n (CAst.make ?loc @@ CHole (None, IntroAnonymous, None)) in - let app = CAst.make ?loc @@ CAppExpl ((None, constrname,None), List.rev_append pars args) in - intern env app - end + let args = intern_args env args_scopes (List.rev_append pars args) in + let hd = DAst.make @@ GRef (constrname,None) in + DAst.make ?loc @@ GApp (hd, args) + end | CCases (sty, rtnpo, tms, eqns) -> let as_in_vars = List.fold_left (fun acc (_,na,inb) -> (Option.fold_left (fun acc { CAst.v = y } -> Name.fold_right Id.Set.add y acc) acc na)) @@ -2133,9 +2073,10 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = List.rev_append match_td matchs) tms ([],Id.Set.empty,Id.Map.empty,[]) in let env' = Id.Set.fold - (fun var bli -> push_name_env ntnvars (Variable,[],[],[]) bli (CAst.make @@ Name var)) + (fun var bli -> push_name_env ntnvars [] bli (CAst.make @@ Name var)) (Id.Set.union ex_ids as_in_vars) - (reset_hidden_inductive_implicit_test (restart_lambda_binders env)) in + (restart_lambda_binders env) + in (* PatVars before a real pattern do not need to be matched *) let stripped_match_from_in = let rec aux = function @@ -2170,17 +2111,17 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = (* "in" is None so no match to add *) let ((b',(na',_)),_,_) = intern_case_item env' Id.Set.empty (b,na,None) in let p' = Option.map (fun u -> - let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env') + let env'' = push_name_env ntnvars [] env' (CAst.make na') in intern_type (slide_binders env'') u) po in DAst.make ?loc @@ GLetTuple (List.map (fun { CAst.v } -> v) nal, (na', p'), b', - intern (List.fold_left (push_name_env ntnvars (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c) + intern (List.fold_left (push_name_env ntnvars []) env nal) c) | CIf (c, (na,po), b1, b2) -> let env' = reset_tmp_scope env in let ((c',(na',_)),_,_) = intern_case_item env' Id.Set.empty (c,na,None) in (* no "in" no match to ad too *) let p' = Option.map (fun p -> - let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env) + let env'' = push_name_env ntnvars [] env (CAst.make na') in intern_type (slide_binders env'') p) po in DAst.make ?loc @@ @@ -2478,22 +2419,23 @@ let interp_open_constr ?(expected_type=WithoutTypeConstraint) env sigma c = (* Not all evars expected to be resolved and computation of implicit args *) -let interp_constr_evars_gen_impls ?(program_mode=false) env sigma +let interp_constr_evars_gen_impls ?(flags=Pretyping.all_no_fail_flags) env sigma ?(impls=empty_internalization_env) expected_type c = let c = intern_gen expected_type ~impls env sigma c in let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:(expected_type == IsType) c in - let flags = { Pretyping.all_no_fail_flags with program_mode } in let sigma, c = understand_tcc ~flags env sigma ~expected_type c in sigma, (c, imps) -let interp_constr_evars_impls ?program_mode env sigma ?(impls=empty_internalization_env) c = - interp_constr_evars_gen_impls ?program_mode env sigma ~impls WithoutTypeConstraint c +let interp_constr_evars_impls ?(program_mode=false) env sigma ?(impls=empty_internalization_env) c = + let flags = { Pretyping.all_no_fail_flags with program_mode } in + interp_constr_evars_gen_impls ~flags env sigma ~impls WithoutTypeConstraint c -let interp_casted_constr_evars_impls ?program_mode env evdref ?(impls=empty_internalization_env) c typ = - interp_constr_evars_gen_impls ?program_mode env evdref ~impls (OfType typ) c +let interp_casted_constr_evars_impls ?(program_mode=false) env evdref ?(impls=empty_internalization_env) c typ = + let flags = { Pretyping.all_no_fail_flags with program_mode } in + interp_constr_evars_gen_impls ~flags env evdref ~impls (OfType typ) c -let interp_type_evars_impls ?program_mode env sigma ?(impls=empty_internalization_env) c = - interp_constr_evars_gen_impls ?program_mode env sigma ~impls IsType c +let interp_type_evars_impls ?(flags=Pretyping.all_no_fail_flags) env sigma ?(impls=empty_internalization_env) c = + interp_constr_evars_gen_impls ~flags env sigma ~impls IsType c (* Not all evars expected to be resolved, with side-effect on evars *) |