diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrexpr.ml | 11 | ||||
| -rw-r--r-- | interp/constrexpr_ops.ml | 19 | ||||
| -rw-r--r-- | interp/constrextern.ml | 47 | ||||
| -rw-r--r-- | interp/constrintern.ml | 121 | ||||
| -rw-r--r-- | interp/constrintern.mli | 13 | ||||
| -rw-r--r-- | interp/declare.ml | 23 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.ml | 36 | ||||
| -rw-r--r-- | interp/notation.ml | 2 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 13 | ||||
| -rw-r--r-- | interp/notation_term.ml | 2 |
10 files changed, 140 insertions, 147 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index 7a14a4e708..9f778d99e9 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -134,16 +134,17 @@ and branch_expr = (cases_pattern_expr list list * constr_expr) CAst.t and fix_expr = - lident * (lident option * recursion_order_expr) * + lident * recursion_order_expr option * local_binder_expr list * constr_expr * constr_expr and cofix_expr = lident * local_binder_expr list * constr_expr * constr_expr -and recursion_order_expr = - | CStructRec - | CWfRec of constr_expr - | CMeasureRec of constr_expr * constr_expr option (** measure, relation *) +and recursion_order_expr_r = + | CStructRec of lident + | CWfRec of lident * constr_expr + | CMeasureRec of lident option * constr_expr * constr_expr option (** argument, measure, relation *) +and recursion_order_expr = recursion_order_expr_r CAst.t (* Anonymous defs allowed ?? *) and local_binder_expr = diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 60610b92b8..443473d5b6 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -196,10 +196,9 @@ and branch_expr_eq {CAst.v=(p1, e1)} {CAst.v=(p2, e2)} = List.equal (List.equal cases_pattern_expr_eq) p1 p2 && constr_expr_eq e1 e2 -and fix_expr_eq (id1,(j1, r1),bl1,a1,b1) (id2,(j2, r2),bl2,a2,b2) = +and fix_expr_eq (id1,r1,bl1,a1,b1) (id2,r2,bl2,a2,b2) = (eq_ast Id.equal id1 id2) && - Option.equal (eq_ast Id.equal) j1 j2 && - recursion_order_expr_eq r1 r2 && + Option.equal recursion_order_expr_eq r1 r2 && List.equal local_binder_eq bl1 bl2 && constr_expr_eq a1 a2 && constr_expr_eq b1 b2 @@ -210,13 +209,17 @@ and cofix_expr_eq (id1,bl1,a1,b1) (id2,bl2,a2,b2) = constr_expr_eq a1 a2 && constr_expr_eq b1 b2 -and recursion_order_expr_eq r1 r2 = match r1, r2 with - | CStructRec, CStructRec -> true - | CWfRec e1, CWfRec e2 -> constr_expr_eq e1 e2 - | CMeasureRec (e1, o1), CMeasureRec (e2, o2) -> +and recursion_order_expr_eq_r r1 r2 = match r1, r2 with + | CStructRec i1, CStructRec i2 -> eq_ast Id.equal i1 i2 + | CWfRec (i1,e1), CWfRec (i2,e2) -> + constr_expr_eq e1 e2 + | CMeasureRec (i1, e1, o1), CMeasureRec (i2, e2, o2) -> + Option.equal (eq_ast Id.equal) i1 i2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq o1 o2 | _ -> false +and recursion_order_expr_eq r1 r2 = eq_ast recursion_order_expr_eq_r r1 r2 + and local_binder_eq l1 l2 = match l1, l2 with | CLocalDef (n1, e1, t1), CLocalDef (n2, e2, t2) -> eq_ast Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2 @@ -349,7 +352,7 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function (f (Option.fold_right (CAst.with_val (Name.fold_right g)) ona n)) acc po | CFix (_,l) -> let n' = List.fold_right (fun ( { CAst.v = id },_,_,_,_) -> g id) l n in - List.fold_right (fun (_,(_,o),lb,t,c) acc -> + List.fold_right (fun (_,ro,lb,t,c) acc -> fold_local_binders g f n' (fold_local_binders g f n acc t lb) c lb) l acc | CCoFix (_,_) -> diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 24b1362e6d..488c9a740f 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -212,7 +212,7 @@ let encode_record r = module PrintingRecordRecord = PrintingInductiveMake (struct - let encode = encode_record + let encode _env = encode_record let field = "Record" let title = "Types leading to pretty-printing using record notation: " let member_message s b = @@ -224,7 +224,7 @@ module PrintingRecordRecord = module PrintingRecordConstructor = PrintingInductiveMake (struct - let encode = encode_record + let encode _env = encode_record let field = "Constructor" let title = "Types leading to pretty-printing using constructor form: " let member_message s b = @@ -289,11 +289,11 @@ let extern_reference ?loc vars l = !my_extern_reference vars l let add_patt_for_params ind l = if !Flags.in_debugger then l else - Util.List.addn (Inductiveops.inductive_nparamdecls ind) (CAst.make @@ CPatAtom None) l + Util.List.addn (Inductiveops.inductive_nparamdecls (Global.env()) ind) (CAst.make @@ CPatAtom None) l let add_cpatt_for_params ind l = if !Flags.in_debugger then l else - Util.List.addn (Inductiveops.inductive_nparamdecls ind) (DAst.make @@ PatVar Anonymous) l + Util.List.addn (Inductiveops.inductive_nparamdecls (Global.env()) ind) (DAst.make @@ PatVar Anonymous) l let drop_implicits_in_patt cst nb_expl args = let impl_st = (implicits_of_global cst) in @@ -364,7 +364,7 @@ let mkPat ?loc qid l = CAst.make ?loc @@ let pattern_printable_in_both_syntax (ind,_ as c) = let impl_st = extract_impargs_data (implicits_of_global (ConstructRef c)) in - let nb_params = Inductiveops.inductive_nparams ind in + let nb_params = Inductiveops.inductive_nparams (Global.env()) ind in List.exists (fun (_,impls) -> (List.length impls >= nb_params) && let params,args = Util.List.chop nb_params impls in @@ -526,7 +526,7 @@ let rec extern_notation_ind_pattern allscopes lonely_seen vars ind args = functi let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args = (* pboutill: There are letins in pat which is incompatible with notations and not explicit application. *) - if !Flags.in_debugger||Inductiveops.inductive_has_local_defs ind then + if !Flags.in_debugger||Inductiveops.inductive_has_local_defs (Global.env()) ind then let c = extern_reference vars (IndRef ind) in let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in CAst.make @@ CPatCstr (c, Some (add_patt_for_params ind args), []) @@ -738,6 +738,14 @@ let extern_optimal extern r r' = | Some n, (Some ({ CAst.v = CDelimiters _}) | None) | _, Some n -> n | _ -> raise No_match +(* Helper function for safe and optimal printing of primitive tokens *) +(* such as those for Int63 *) +let extern_prim_token_delimiter_if_required n key_n scope_n scopes = + match availability_of_prim_token n scope_n scopes with + | Some None -> CPrim n + | None -> CDelimiters(key_n, CAst.make (CPrim n)) + | Some (Some key) -> CDelimiters(key, CAst.make (CPrim n)) + (**********************************************************************) (* mapping decl *) @@ -938,13 +946,12 @@ let rec extern inctx (custom,scopes as allscopes) vars r = let (assums,ids,bl) = extern_local_binder scopes vars bl in let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in - let n = - match fst nv.(i) with - | None -> None - | Some x -> Some (CAst.make @@ Name.get_id (List.nth assums x)) - in - let ro = extern_recursion_order scopes vars (snd nv.(i)) in - ((CAst.make fi), (n, ro), bl, extern_typ scopes vars0 ty, + let n = + match nv.(i) with + | None -> None + | Some x -> Some (CAst.make @@ CStructRec (CAst.make @@ Name.get_id (List.nth assums x))) + in + ((CAst.make fi), n, bl, extern_typ scopes vars0 ty, extern false scopes vars1 def)) idv in CFix (CAst.(make ?loc idv.(n)), Array.to_list listdecl) @@ -967,8 +974,11 @@ let rec extern inctx (custom,scopes as allscopes) vars r = | GCast (c, c') -> CCast (sub_extern true scopes vars c, map_cast_type (extern_typ scopes vars) c') + | GInt i -> - CPrim(Numeral (SPlus, NumTok.int (Uint63.to_string i))) + extern_prim_token_delimiter_if_required + (Numeral (SPlus, NumTok.int (Uint63.to_string i))) + "int63" "int63_scope" (snd scopes) in insert_coercion coercion (CAst.make ?loc c) @@ -1159,13 +1169,6 @@ and extern_notation (custom,scopes as allscopes) lonely_seen vars t = function let lonely_seen = add_lonely keyrule lonely_seen in extern_notation allscopes lonely_seen vars t rules -and extern_recursion_order scopes vars = function - GStructRec -> CStructRec - | GWfRec c -> CWfRec (extern true scopes vars c) - | GMeasureRec (m,r) -> CMeasureRec (extern true scopes vars m, - Option.map (extern true scopes vars) r) - - let extern_glob_constr vars c = extern false (InConstrEntrySomeLevel,(None,[])) vars c @@ -1294,7 +1297,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with let v = Array.map3 (fun c t i -> Detyping.share_pattern_names glob_of_pat (i+1) [] def_avoid def_env sigma c (Patternops.lift_pattern n t)) bl tl ln in - GRec(GFix (Array.map (fun i -> Some i, GStructRec) ln,i),Array.of_list (List.rev lfi), + GRec(GFix (Array.map (fun i -> Some i) ln,i),Array.of_list (List.rev lfi), Array.map (fun (bl,_,_) -> bl) v, Array.map (fun (_,_,ty) -> ty) v, Array.map (fun (_,bd,_) -> bd) v) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 59feb46dc1..c0801067ce 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -96,21 +96,6 @@ let is_global id = with Not_found -> false -let global_reference_of_reference qid = - locate_reference qid - -let global_reference id = - locate_reference (qualid_of_ident id) - -let construct_reference ctx id = - try - VarRef (let _ = Context.Named.lookup id ctx in id) - with Not_found -> - global_reference id - -let global_reference_in_absolute_module dir id = - Nametab.global_of_path (Libnames.make_path dir id) - (**********************************************************************) (* Internalization errors *) @@ -658,7 +643,7 @@ let terms_of_binders bl = | PatCstr (c,l,_) -> 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 + let params = List.make (Inductiveops.inductive_nparams (Global.env()) (fst c)) hole in CAppExpl ((None,qid,None),params @ List.map term_of_pat l)) pt in let rec extract_variables l = match l with | bnd :: l -> @@ -753,7 +738,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = else let _,((disjpat,_),_),_ = intern_pat ntnvars nenv c in match disjpat with - | [pat] -> (glob_constr_of_cases_pattern pat, None) + | [pat] -> (glob_constr_of_cases_pattern (Global.env()) pat, None) | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.loc () in let terms = Id.Map.fold mk_env terms Id.Map.empty in @@ -815,7 +800,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = else let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in match disjpat with - | [pat] -> glob_constr_of_cases_pattern pat + | [pat] -> glob_constr_of_cases_pattern (Global.env()) pat | _ -> user_err Pp.(str "Cannot turn a disjunctive pattern into a term.") with Not_found -> try @@ -1212,10 +1197,10 @@ let check_or_pat_variables loc ids idsl = @return if letin are included *) let check_constructor_length env loc cstr len_pl pl0 = let n = len_pl + List.length pl0 in - if Int.equal n (Inductiveops.constructor_nallargs cstr) then false else - (Int.equal n (Inductiveops.constructor_nalldecls cstr) || + if Int.equal n (Inductiveops.constructor_nallargs env cstr) then false else + (Int.equal n (Inductiveops.constructor_nalldecls env cstr) || (error_wrong_numarg_constructor ?loc env cstr - (Inductiveops.constructor_nrealargs cstr))) + (Inductiveops.constructor_nrealargs env cstr))) open Declarations @@ -1241,9 +1226,9 @@ let add_local_defs_and_check_length loc env g pl args = match g with have been given in the "explicit" arguments, which come from a "@C args" notation or from a custom user notation *) let pl' = insert_local_defs_in_pattern cstr pl in - let maxargs = Inductiveops.constructor_nalldecls cstr in + let maxargs = Inductiveops.constructor_nalldecls env cstr in if List.length pl' + List.length args > maxargs then - error_wrong_numarg_constructor ?loc env cstr (Inductiveops.constructor_nrealargs cstr); + error_wrong_numarg_constructor ?loc env cstr (Inductiveops.constructor_nrealargs env cstr); (* Two possibilities: either the args are given with explict variables for local definitions, then we give the explicit args extended with local defs, so that there is nothing more to be @@ -1273,15 +1258,15 @@ let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 in aux 0 (impl_list,pl2) let add_implicits_check_constructor_length env loc c len_pl1 pl2 = - let nargs = Inductiveops.constructor_nallargs c in - let nargs' = Inductiveops.constructor_nalldecls c in + let nargs = Inductiveops.constructor_nallargs env c in + let nargs' = Inductiveops.constructor_nalldecls env c in let impls_st = implicits_of_global (ConstructRef c) in add_implicits_check_length (error_wrong_numarg_constructor ?loc env c) nargs nargs' impls_st len_pl1 pl2 let add_implicits_check_ind_length env loc c len_pl1 pl2 = - let nallargs = inductive_nallargs_env env c in - let nalldecls = inductive_nalldecls_env env c in + let nallargs = inductive_nallargs env c in + let nalldecls = inductive_nalldecls env c in let impls_st = implicits_of_global (IndRef c) in add_implicits_check_length (error_wrong_numarg_inductive ?loc env c) nallargs nalldecls impls_st len_pl1 pl2 @@ -1289,8 +1274,8 @@ let add_implicits_check_ind_length env loc c len_pl1 pl2 = (** Do not raise NotEnoughArguments thanks to preconditions*) let chop_params_pattern loc ind args with_letin = let nparams = if with_letin - then Inductiveops.inductive_nparamdecls ind - else Inductiveops.inductive_nparams ind in + then Inductiveops.inductive_nparamdecls (Global.env()) ind + else Inductiveops.inductive_nparams (Global.env()) ind in assert (nparams <= List.length args); let params,args = List.chop nparams args in List.iter (fun c -> match DAst.get c with @@ -1310,10 +1295,11 @@ let find_constructor loc add_params ref = in cstr, match add_params with | Some nb_args -> + let env = Global.env () in let nb = - if Int.equal nb_args (Inductiveops.constructor_nrealdecls cstr) - then Inductiveops.inductive_nparamdecls ind - else Inductiveops.inductive_nparams ind + if Int.equal nb_args (Inductiveops.constructor_nrealdecls env cstr) + then Inductiveops.inductive_nparamdecls env ind + else Inductiveops.inductive_nparams env ind in List.make nb ([], [(Id.Map.empty, DAst.make @@ PatVar Anonymous)]) | None -> [] @@ -1354,7 +1340,7 @@ let sort_fields ~complete loc fields completer = | (first_field_ref, first_field_value):: other_fields -> let (first_field_glob_ref, record) = try - let gr = global_reference_of_reference first_field_ref in + let gr = locate_reference first_field_ref in (gr, Recordops.find_projection gr) with Not_found -> raise (InternalizationError(loc, NotAProjection first_field_ref)) @@ -1412,7 +1398,7 @@ let sort_fields ~complete loc fields completer = let rec index_fields fields remaining_projs acc = match fields with | (field_ref, field_value) :: fields -> - let field_glob_ref = try global_reference_of_reference field_ref + let field_glob_ref = try locate_reference field_ref with Not_found -> user_err ?loc ~hdr:"intern" (str "The field \"" ++ pr_qualid field_ref ++ str "\" does not exist.") in @@ -1859,51 +1845,44 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = in apply_impargs c env imp subscopes l loc - | CFix ({ CAst.loc = locid; v = iddef}, dl) -> + | CFix ({ CAst.loc = locid; v = iddef}, dl) -> let lf = List.map (fun ({CAst.v = id},_,_,_,_) -> id) dl in let dl = Array.of_list dl in - let n = - try List.index0 Id.equal iddef lf + let n = + try List.index0 Id.equal iddef lf with Not_found -> - raise (InternalizationError (locid,UnboundFixName (false,iddef))) - in - let idl_temp = Array.map - (fun (id,(n,order),bl,ty,_) -> - let intern_ro_arg f = - let before, after = split_at_annot bl n in - let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in - let ro = f (intern env') in - let n' = Option.map (fun _ -> List.count (fun c -> match DAst.get c with - | GLocalAssum _ -> true - | _ -> false (* remove let-ins *)) - rbefore) n in - n', ro, List.fold_left intern_local_binder (env',rbefore) after - in - let n, ro, (env',rbl) = - match order with - | CStructRec -> - intern_ro_arg (fun _ -> GStructRec) - | CWfRec c -> - intern_ro_arg (fun f -> GWfRec (f c)) - | CMeasureRec (m,r) -> - intern_ro_arg (fun f -> GMeasureRec (f m, Option.map f r)) - in - let bl = List.rev (List.map glob_local_binder_of_extended rbl) in - ((n, ro), bl, intern_type env' ty, env')) dl in + raise (InternalizationError (locid,UnboundFixName (false,iddef))) + in + let idl_temp = Array.map + (fun (id,recarg,bl,ty,_) -> + let recarg = Option.map (function { CAst.v = v } -> match v with + | CStructRec i -> i + | _ -> anomaly Pp.(str "Non-structural recursive argument in non-program fixpoint")) recarg + in + let before, after = split_at_annot bl recarg in + let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in + let n = Option.map (fun _ -> List.count (fun c -> match DAst.get c with + | GLocalAssum _ -> true + | _ -> false (* remove let-ins *)) + rbefore) recarg in + let (env',rbl) = List.fold_left intern_local_binder (env',rbefore) after in + let bl = List.rev (List.map glob_local_binder_of_extended rbl) in + (n, bl, intern_type env' ty, env')) dl in let idl = Array.map2 (fun (_,_,_,_,bd) (a,b,c,env') -> - let env'' = List.fold_left_i (fun i en name -> - let (_,bli,tyi,_) = idl_temp.(i) in - let fix_args = (List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli) in - push_name_env ntnvars (impls_type_list ~args:fix_args tyi) - en (CAst.make @@ Name name)) 0 env' lf in - (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in - DAst.make ?loc @@ - GRec (GFix - (Array.map (fun (ro,_,_,_) -> ro) idl,n), + let env'' = List.fold_left_i (fun i en name -> + let (_,bli,tyi,_) = idl_temp.(i) in + let fix_args = (List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli) in + push_name_env ntnvars (impls_type_list ~args:fix_args tyi) + en (CAst.make @@ Name name)) 0 env' lf in + (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in + DAst.make ?loc @@ + GRec (GFix + (Array.map (fun (ro,_,_,_) -> ro) idl,n), Array.of_list lf, Array.map (fun (_,bl,_,_) -> bl) idl, Array.map (fun (_,_,ty,_) -> ty) idl, Array.map (fun (_,_,_,bd) -> bd) idl) + | CCoFix ({ CAst.loc = locid; v = iddef }, dl) -> let lf = List.map (fun ({CAst.v = id},_,_,_) -> id) dl in let dl = Array.of_list dl in diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 2d14a0d0a7..0d4bc91f57 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -162,24 +162,11 @@ val interp_context_evars : env -> evar_map -> local_binder_expr list -> evar_map * (internalization_env * ((env * rel_context) * Impargs.manual_implicits)) -(* val interp_context_gen : (env -> glob_constr -> unsafe_type_judgment Evd.in_evar_universe_context) -> *) -(* (env -> Evarutil.type_constraint -> glob_constr -> unsafe_judgment Evd.in_evar_universe_context) -> *) -(* ?global_level:bool -> ?impl_env:internalization_env -> *) -(* env -> evar_map -> local_binder_expr list -> internalization_env * ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *) - -(* val interp_context : ?global_level:bool -> ?impl_env:internalization_env -> *) -(* env -> evar_map -> local_binder_expr list -> *) -(* internalization_env * *) -(* ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *) - (** Locating references of constructions, possibly via a syntactic definition (these functions do not modify the glob file) *) val locate_reference : Libnames.qualid -> GlobRef.t val is_global : Id.t -> bool -val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> GlobRef.t -val global_reference : Id.t -> GlobRef.t -val global_reference_in_absolute_module : DirPath.t -> Id.t -> GlobRef.t (** Interprets a term as the left-hand side of a notation. The returned map is guaranteed to have the same domain as the input one. *) diff --git a/interp/declare.ml b/interp/declare.ml index 08a6ac5f7b..76b4bab2ce 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -119,7 +119,6 @@ let set_declare_scheme f = declare_scheme := f let update_tables c = declare_constant_implicits c; - Heads.declare_head (EvalConstRef c); Notation.declare_ref_arguments_scope Evd.empty (ConstRef c) let register_side_effect (c, role) = @@ -257,7 +256,6 @@ let declare_variable id obj = let oname = add_leaf id (inVariable (Inr (id,obj))) in declare_var_implicits id; Notation.declare_ref_arguments_scope Evd.empty (VarRef id); - Heads.declare_head (EvalVarRef id); oname (** Declaration of inductive blocks *) @@ -348,6 +346,25 @@ let inInductive : mutual_inductive_entry -> obj = discharge_function = discharge_inductive; rebuild_function = rebuild_inductive } +let cache_prim (_,(p,c)) = Recordops.register_primitive_projection p c + +let load_prim _ p = cache_prim p + +let subst_prim (subst,(p,c)) = Mod_subst.subst_proj_repr subst p, Mod_subst.subst_constant subst c + +let discharge_prim (_,(p,c)) = Some (Lib.discharge_proj_repr p, c) + +let inPrim : (Projection.Repr.t * Constant.t) -> obj = + declare_object { + (default_object "PRIMPROJS") with + cache_function = cache_prim ; + load_function = load_prim; + subst_function = subst_prim; + classify_function = (fun x -> Substitute x); + discharge_function = discharge_prim } + +let declare_primitive_projection p c = Lib.add_anonymous_leaf (inPrim (p,c)) + let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) = let id = Label.to_id label in let univs, u = match univs with @@ -362,7 +379,7 @@ let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (ter let entry = definition_entry ~types ~univs term in let cst = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in - Recordops.declare_primitive_projection p cst + declare_primitive_projection p cst let declare_projections univs mind = diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 854651e7b7..dffccf02fc 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -231,23 +231,25 @@ let implicit_application env ?(allow_partial=true) f ty = | Some ({CAst.loc;v=(id, par, inst)}, gr) -> let avoid = Id.Set.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in let c, avoid = - let c = class_info gr in - let (ci, rd) = c.cl_context in - if not allow_partial then - begin - let opt_succ x n = match x with - | None -> succ n - | Some _ -> n - in - let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in - let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in - if not (Int.equal needlen applen) then - mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd - end; - let pars = List.rev (List.combine ci rd) in - let args, avoid = combine_params avoid f par pars in - CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid - in c, avoid + let env = Global.env () in + let sigma = Evd.from_env env in + let c = class_info env sigma gr in + let (ci, rd) = c.cl_context in + if not allow_partial then + begin + let opt_succ x n = match x with + | None -> succ n + | Some _ -> n + in + let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in + let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in + if not (Int.equal needlen applen) then + mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd + end; + let pars = List.rev (List.combine ci rd) in + let args, avoid = combine_params avoid f par pars in + CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid + in c, avoid let warn_ignoring_implicit_status = CWarnings.create ~name:"ignoring_implicit_status" ~category:"implicits" diff --git a/interp/notation.ml b/interp/notation.ml index b9aca82cf4..56504db04e 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1516,7 +1516,7 @@ let uninterp_prim_token c = with Not_found -> raise Notation_ops.No_match let uninterp_prim_token_cases_pattern c = - match glob_constr_of_closed_cases_pattern c with + match glob_constr_of_closed_cases_pattern (Global.env()) c with | exception Not_found -> raise Notation_ops.No_match | na,c -> let (sc,n) = uninterp_prim_token c in (na,sc,n) diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 7d7e10a05b..7f084fffdd 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -782,7 +782,7 @@ let rec pat_binder_of_term t = DAst.map (function | GApp (t, l) -> begin match DAst.get t with | GRef (ConstructRef cstr,_) -> - let nparams = Inductiveops.inductive_nparams (fst cstr) in + let nparams = Inductiveops.inductive_nparams (Global.env()) (fst cstr) in let _,l = List.chop nparams l in PatCstr (cstr, List.map pat_binder_of_term l, Anonymous) | _ -> raise No_match @@ -909,7 +909,8 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma) alp, add_env alp sigma var (DAst.make @@ GVar id) let bind_binding_as_term_env alp (terms,termlists,binders,binderlists as sigma) var c = - let pat = try cases_pattern_of_glob_constr Anonymous c with Not_found -> raise No_match in + let env = Global.env () in + let pat = try cases_pattern_of_glob_constr env Anonymous c with Not_found -> raise No_match in try (* If already bound to a binder, unify the term and the binder *) let patl' = Id.List.assoc var binders in @@ -956,7 +957,7 @@ let match_fix_kind fk1 fk2 = match (fk1,fk2) with | GCoFix n1, GCoFix n2 -> Int.equal n1 n2 | GFix (nl1,n1), GFix (nl2,n2) -> - let test (n1, _) (n2, _) = match n1, n2 with + let test n1 n2 = match n1, n2 with | _, None -> true | Some id1, Some id2 -> Int.equal id1 id2 | _ -> false @@ -1292,7 +1293,7 @@ let match_notation_constr u c (metas,pat) = | NtnTypeBinder (NtnBinderParsedAsConstr _) -> (match Id.List.assoc x binders with | [pat] -> - let v = glob_constr_of_cases_pattern pat in + let v = glob_constr_of_cases_pattern (Global.env()) pat in ((v,scl)::terms',termlists',binders',binderlists') | _ -> raise No_match) | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _) -> @@ -1333,11 +1334,11 @@ let rec match_cases_pattern metas (terms,termlists,(),() as sigma) a1 a2 = | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(0,[]) | PatVar Anonymous, NHole _ -> sigma,(0,[]) | PatCstr ((ind,_ as r1),largs,Anonymous), NRef (ConstructRef r2) when eq_constructor r1 r2 -> - let l = try add_patterns_for_params_remove_local_defs r1 largs with Not_found -> raise No_match in + let l = try add_patterns_for_params_remove_local_defs (Global.env ()) r1 largs with Not_found -> raise No_match in sigma,(0,l) | PatCstr ((ind,_ as r1),args1,Anonymous), NApp (NRef (ConstructRef r2),l2) when eq_constructor r1 r2 -> - let l1 = try add_patterns_for_params_remove_local_defs r1 args1 with Not_found -> raise No_match in + let l1 = try add_patterns_for_params_remove_local_defs (Global.env()) r1 args1 with Not_found -> raise No_match in let le2 = List.length l2 in if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length l1 then diff --git a/interp/notation_term.ml b/interp/notation_term.ml index 6fe20486dc..5024f5c26f 100644 --- a/interp/notation_term.ml +++ b/interp/notation_term.ml @@ -38,7 +38,7 @@ type notation_constr = notation_constr * notation_constr | NIf of notation_constr * (Name.t * notation_constr option) * notation_constr * notation_constr - | NRec of fix_kind * Id.t array * + | NRec of glob_fix_kind * Id.t array * (Name.t * notation_constr option * notation_constr) list array * notation_constr array * notation_constr array | NSort of glob_sort |