diff options
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 90 |
1 files changed, 61 insertions, 29 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 1c8d957014..02db8f6aab 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -28,7 +28,6 @@ open Constrexpr open Constrexpr_ops open Notation_term open Notation_ops -open Nametab open Notation open Inductiveops open Decl_kinds @@ -121,6 +120,9 @@ type internalization_error = | UnboundFixName of bool * Id.t | NonLinearPattern of Id.t | BadPatternsNumber of int * int + | NotAProjection of qualid + | NotAProjectionOf of qualid * qualid + | ProjectionsOfDifferentRecords of qualid * qualid exception InternalizationError of internalization_error Loc.located @@ -146,6 +148,16 @@ let explain_bad_patterns_number n1 n2 = str "Expecting " ++ int n1 ++ str (String.plural n1 " pattern") ++ str " but found " ++ int n2 +let explain_field_not_a_projection field_id = + pr_qualid field_id ++ str ": Not a projection" + +let explain_field_not_a_projection_of field_id inductive_id = + pr_qualid field_id ++ str ": Not a projection of inductive " ++ pr_qualid inductive_id + +let explain_projections_of_diff_records inductive1_id inductive2_id = + str "This record contains fields of both " ++ pr_qualid inductive1_id ++ + str " and " ++ pr_qualid inductive2_id + let explain_internalization_error e = let pp = match e with | VariableCapture (id,id') -> explain_variable_capture id id' @@ -154,6 +166,11 @@ let explain_internalization_error e = | UnboundFixName (iscofix,id) -> explain_unbound_fix_name iscofix id | NonLinearPattern id -> explain_non_linear_pattern id | BadPatternsNumber (n1,n2) -> explain_bad_patterns_number n1 n2 + | NotAProjection field_id -> explain_field_not_a_projection field_id + | NotAProjectionOf (field_id, inductive_id) -> + explain_field_not_a_projection_of field_id inductive_id + | ProjectionsOfDifferentRecords (inductive1_id, inductive2_id) -> + explain_projections_of_diff_records inductive1_id inductive2_id in pp ++ str "." let error_bad_inductive_type ?loc = @@ -633,7 +650,7 @@ let terms_of_binders bl = | PatVar (Name id) -> CRef (qualid_of_ident id, None) | PatVar (Anonymous) -> error_cannot_coerce_wildcard_term ?loc () | PatCstr (c,l,_) -> - let qid = qualid_of_path ?loc (path_of_global (ConstructRef c)) in + let qid = qualid_of_path ?loc (Nametab.path_of_global (ConstructRef c)) in let hole = CAst.make ?loc @@ CHole (None,IntroAnonymous,None) in let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in CAppExpl ((None,qid,None),params @ List.map term_of_pat l)) pt in @@ -720,8 +737,8 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in try let gc = intern nenv c in - Id.Map.add id (gc, Some c) map - with GlobalizationError _ -> map + Id.Map.add id (gc, None) map + with Nametab.GlobalizationError _ -> map in let mk_env' (c, (onlyident,(tmp_scope,subscopes))) = let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in @@ -986,7 +1003,7 @@ let intern_extended_global_of_qualid qid = let intern_reference qid = let r = try intern_extended_global_of_qualid qid - with Not_found -> error_global_not_found qid + with Not_found -> Nametab.error_global_not_found qid in Smartlocate.global_of_extended_global r @@ -1058,11 +1075,11 @@ let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args qi (* Extra allowance for non globalizing functions *) if !interning_grammar || env.unb then (gvar (loc,qualid_basename qid) us, [], [], []), args - else error_global_not_found qid + else Nametab.error_global_not_found qid else let r,projapp,args2 = try intern_qualid qid intern env ntnvars us args - with Not_found -> error_global_not_found qid + with Not_found -> Nametab.error_global_not_found qid in let x, imp, scopes, l = find_appl_head_data r in (x,imp,scopes,l), args2 @@ -1282,6 +1299,10 @@ let check_duplicate loc fields = user_err ?loc (str "This record defines several times the field " ++ pr_qualid r ++ str ".") +let inductive_of_record loc record = + let inductive = IndRef (inductive_of_constructor record.Recordops.s_CONST) in + Nametab.shortest_qualid_of_global ?loc Id.Set.empty inductive + (** [sort_fields ~complete loc fields completer] expects a list [fields] of field assignments [f = e1; g = e2; ...], where [f, g] are fields of a record and [e1] are "values" (either terms, when @@ -1304,15 +1325,14 @@ let sort_fields ~complete loc fields completer = let gr = global_reference_of_reference first_field_ref in (gr, Recordops.find_projection gr) with Not_found -> - user_err ?loc ~hdr:"intern" - (pr_qualid first_field_ref ++ str": Not a projection") + raise (InternalizationError(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 = ConstructRef record.Recordops.s_CONST in - try shortest_qualid_of_global ?loc Id.Set.empty global_record_id + try Nametab.shortest_qualid_of_global ?loc Id.Set.empty global_record_id with Not_found -> anomaly (str "Environment corruption for records.") in let () = check_duplicate loc fields in @@ -1364,12 +1384,18 @@ let sort_fields ~complete loc fields completer = with Not_found -> user_err ?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 (ConstRef glob_id) in try CList.extract_first the_proj remaining_projs with Not_found -> - user_err ?loc - (str "This record contains fields of different records.") + let ind1 = inductive_of_record loc record in + let ind2 = inductive_of_record loc this_field_record in + raise (InternalizationError(loc, ProjectionsOfDifferentRecords (ind1, ind2))) in index_fields fields remaining_projs ((field_index, field_value) :: acc) | [] -> @@ -1493,7 +1519,7 @@ let drop_notations_pattern looked_for genv = in let rec drop_syndef top scopes qid pats = try - match locate_extended qid with + match Nametab.locate_extended qid with | SynDef sp -> let (vars,a) = Syntax_def.search_syntactic_definition sp in (match a with @@ -1550,7 +1576,7 @@ let drop_notations_pattern looked_for genv = | None -> raise (InternalizationError (loc,NotAConstructor head)) end | CPatCstr (qid, Some expl_pl, pl) -> - let g = try locate qid + let g = try Nametab.locate qid with Not_found -> raise (InternalizationError (loc,NotAConstructor qid)) in if expl_pl == [] then @@ -1863,12 +1889,11 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = Array.map (fun (bl,_,_) -> bl) idl, Array.map (fun (_,ty,_) -> ty) idl, Array.map (fun (_,_,bd) -> bd) idl) + | CProdN ([],c2) -> anomaly (Pp.str "The AST is malformed, found prod without binders.") | CProdN (bl,c2) -> let (env',bl) = List.fold_left intern_local_binder (env,[]) bl in expand_binders ?loc mkGProd bl (intern_type env' c2) - | CLambdaN ([],c2) -> - (* Such a term is built sometimes: it should not change scope *) - intern env c2 + | CLambdaN ([],c2) -> anomaly (Pp.str "The AST is malformed, found lambda without binders.") | CLambdaN (bl,c2) -> let (env',bl) = List.fold_left intern_local_binder (reset_tmp_scope env,[]) bl in expand_binders ?loc mkGLambda bl (intern env' c2) @@ -2026,15 +2051,22 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let (ltacvars, ntnvars) = lvar in (* Preventively declare notation variables in ltac as non-bindings *) Id.Map.iter (fun x (used_as_binder,_,_) -> used_as_binder := false) ntnvars; - let ntnvars = Id.Map.domain ntnvars in let extra = ltacvars.ltac_extra in + (* We inform ltac that the interning vars and the notation vars are bound *) + (* but we could instead rely on the "intern_sign" *) let lvars = Id.Set.union ltacvars.ltac_bound ltacvars.ltac_vars in - let lvars = Id.Set.union lvars ntnvars in + let lvars = Id.Set.union lvars (Id.Map.domain ntnvars) in let ltacvars = Id.Set.union lvars env.ids in + (* Propagating enough information for mutual interning with tac-in-term *) + let intern_sign = { + Genintern.intern_ids = env.ids; + Genintern.notation_variable_status = ntnvars + } in let ist = { Genintern.genv = globalenv; ltacvars; extra; + intern_sign; } in let (_, glb) = Genintern.generic_intern ist gen in Some glb @@ -2062,13 +2094,6 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | CCast (c1, c2) -> DAst.make ?loc @@ GCast (intern env c1, map_cast_type (intern_type env) c2) - | CProj (pr, c) -> - match intern_reference pr with - | ConstRef p -> - let p = Option.get @@ Recordops.find_primitive_projection p in - DAst.make ?loc @@ GProj (Projection.make p false, intern env c) - | _ -> - raise (InternalizationError (loc,IllegalMetavariable)) (* FIXME *) ) and intern_type env = intern (set_type_scope env) @@ -2326,16 +2351,23 @@ let intern_constr_pattern env sigma ?(as_type=false) ?(ltacvars=empty_ltac_sign) ~pattern_mode:true ~ltacvars env sigma c in pattern_of_glob_constr c +let intern_core kind env sigma ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign) + { Genintern.intern_ids = ids; Genintern.notation_variable_status = vl } c = + let tmp_scope = scope_of_type_kind sigma kind in + let impls = empty_internalization_env in + internalize env {ids; unb = false; tmp_scope; scopes = []; impls} + pattern_mode (ltacvars, vl) c + let interp_notation_constr env ?(impls=empty_internalization_env) nenv a = + let ids = extract_ids env in (* [vl] is intended to remember the scope of the free variables of [a] *) let vl = Id.Map.map (fun typ -> (ref false, ref None, typ)) nenv.ninterp_var_type in let impls = Id.Map.fold (fun id _ impls -> Id.Map.remove id impls) nenv.ninterp_var_type impls in - let c = internalize (Global.env()) {ids = extract_ids env; unb = false; - tmp_scope = None; scopes = []; impls = impls} + let c = internalize env {ids; unb = false; tmp_scope = None; scopes = []; impls} false (empty_ltac_sign, vl) a in + (* Splits variables into those that are binding, bound, or both *) (* Translate and check that [c] has all its free variables bound in [vars] *) let a, reversible = notation_constr_of_glob_constr nenv c in - (* Splits variables into those that are binding, bound, or both *) (* binding and bound *) let out_scope = function None -> None,[] | Some (a,l) -> a,l in let unused = match reversible with NonInjective ids -> ids | _ -> [] in |