diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrexpr_ops.ml | 22 | ||||
| -rw-r--r-- | interp/constrextern.ml | 75 | ||||
| -rw-r--r-- | interp/constrintern.ml | 160 | ||||
| -rw-r--r-- | interp/constrintern.mli | 18 | ||||
| -rw-r--r-- | interp/coqlib.ml | 146 | ||||
| -rw-r--r-- | interp/coqlib.mli | 43 | ||||
| -rw-r--r-- | interp/dumpglob.ml | 2 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.ml | 19 | ||||
| -rw-r--r-- | interp/modintern.ml | 2 | ||||
| -rw-r--r-- | interp/notation.ml | 18 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 23 | ||||
| -rw-r--r-- | interp/topconstr.ml | 8 |
12 files changed, 333 insertions, 203 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 85ad1cee74..1ba0cafa7a 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -91,10 +91,16 @@ and cases_pattern_notation_substitution_eq (s1, n1) (s2, n2) = List.equal cases_pattern_expr_eq s1 s2 && List.equal (List.equal cases_pattern_expr_eq) n1 n2 +let eq_universes u1 u2 = + match u1, u2 with + | None, None -> true + | Some l, Some l' -> l = l' + | _, _ -> false + let rec constr_expr_eq e1 e2 = if e1 == e2 then true else match e1, e2 with - | CRef r1, CRef r2 -> eq_reference r1 r2 + | CRef (r1,u1), CRef (r2,u2) -> eq_reference r1 r2 && eq_universes u1 u2 | CFix(_,id1,fl1), CFix(_,id2,fl2) -> eq_located Id.equal id1 id2 && List.equal fix_expr_eq fl1 fl2 @@ -111,7 +117,7 @@ let rec constr_expr_eq e1 e2 = Name.equal na1 na2 && constr_expr_eq a1 a2 && constr_expr_eq b1 b2 - | CAppExpl(_,(proj1,r1),al1), CAppExpl(_,(proj2,r2),al2) -> + | CAppExpl(_,(proj1,r1,_),al1), CAppExpl(_,(proj2,r2,_),al2) -> Option.equal Int.equal proj1 proj2 && eq_reference r1 r2 && List.equal constr_expr_eq al1 al2 @@ -221,8 +227,8 @@ and constr_notation_substitution_eq (e1, el1, bl1) (e2, el2, bl2) = List.equal (List.equal local_binder_eq) bl1 bl2 let constr_loc = function - | CRef (Ident (loc,_)) -> loc - | CRef (Qualid (loc,_)) -> loc + | CRef (Ident (loc,_),_) -> loc + | CRef (Qualid (loc,_),_) -> loc | CFix (loc,_,_) -> loc | CCoFix (loc,_,_) -> loc | CProdN (loc,_,_) -> loc @@ -272,8 +278,8 @@ let local_binders_loc bll = match bll with (** Pseudo-constructors *) -let mkIdentC id = CRef (Ident (Loc.ghost, id)) -let mkRefC r = CRef r +let mkIdentC id = CRef (Ident (Loc.ghost, id),None) +let mkRefC r = CRef (r,None) let mkCastC (a,k) = CCast (Loc.ghost,a,k) let mkLambdaC (idl,bk,a,b) = CLambdaN (Loc.ghost,[idl,bk,a],b) let mkLetInC (id,a,b) = CLetIn (Loc.ghost,id,a,b) @@ -324,13 +330,13 @@ let coerce_reference_to_id = function str "This expression should be a simple identifier.") let coerce_to_id = function - | CRef (Ident (loc,id)) -> (loc,id) + | CRef (Ident (loc,id),_) -> (loc,id) | a -> Errors.user_err_loc (constr_loc a,"coerce_to_id", str "This expression should be a simple identifier.") let coerce_to_name = function - | CRef (Ident (loc,id)) -> (loc,Name id) + | CRef (Ident (loc,id),_) -> (loc,Name id) | CHole (loc,_,_) -> (loc,Anonymous) | a -> Errors.user_err_loc (constr_loc a,"coerce_to_name", diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 6a893bde64..e4ac9426b3 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -439,6 +439,11 @@ let occur_name na aty = let is_projection nargs = function | Some r when not !Flags.raw_print && !print_projections -> + if true (* FIXME *) (* !Record.primitive_flag *) then + (match r with + | ConstRef c when Environ.is_projection c (Global.env ()) -> Some 1 + | _ -> None) + else (try let n = Recordops.find_projection_nparams r + 1 in if n <= nargs then Some n else None @@ -477,10 +482,12 @@ let explicitize loc inctx impl (cf,f) args = | args, [] -> List.map (fun a -> (a,None)) args (*In case of polymorphism*) | [], _ -> [] in match is_projection (List.length args) cf with - | Some i as ip -> + | Some i -> if not (List.is_empty impl) && is_status_implicit (List.nth impl (i-1)) then - let f' = match f with CRef f -> f | _ -> assert false in - CAppExpl (loc,(ip,f'),args) + let args = exprec 1 (args,impl) in + CApp (loc, (None, f), args) + (* let f',us = match f with CRef (f,us) -> f,us | _ -> assert false in *) + (* CAppExpl (loc,(ip,f',us),args) *) else let (args1,args2) = List.chop i args in let (impl1,impl2) = if List.is_empty impl then [],[] else List.chop i impl in @@ -488,29 +495,29 @@ let explicitize loc inctx impl (cf,f) args = let args2 = exprec (i+1) (args2,impl2) in CApp (loc,(Some (List.length args1),f),args1@args2) | None -> - let args = exprec 1 (args,impl) in - if List.is_empty args then f else CApp (loc, (None, f), args) + let args = exprec 1 (args,impl) in + if List.is_empty args then f else CApp (loc, (None, f), args) -let extern_global loc impl f = +let extern_global loc impl f us = if not !Constrintern.parsing_explicit && not (List.is_empty impl) && List.for_all is_status_implicit impl then - CAppExpl (loc, (None, f), []) + CAppExpl (loc, (None, f, us), []) else - CRef f + CRef (f,us) -let extern_app loc inctx impl (cf,f) args = +let extern_app loc inctx impl (cf,f) us args = if List.is_empty args then (* If coming from a notation "Notation a := @b" *) - CAppExpl (loc, (None, f), []) + CAppExpl (loc, (None, f, us), []) else if not !Constrintern.parsing_explicit && ((!Flags.raw_print || (!print_implicits && not !print_implicits_explicit_args)) && List.exists is_status_implicit impl) then - CAppExpl (loc, (is_projection (List.length args) cf, f), args) + CAppExpl (loc, (is_projection (List.length args) cf,f,us), args) else - explicitize loc inctx impl (cf,CRef f) args + explicitize loc inctx impl (cf,CRef (f,us)) args let rec extern_args extern scopes env args subscopes = match args with @@ -522,7 +529,7 @@ let rec extern_args extern scopes env args subscopes = extern argscopes env a :: extern_args extern scopes env args subscopes let rec remove_coercions inctx = function - | GApp (loc,GRef (_,r),args) as c + | GApp (loc,GRef (_,r,_),args) as c when not (!Flags.raw_print || !print_coercions) -> let nargs = List.length args in @@ -579,6 +586,10 @@ let extern_glob_sort = function | GType (Some _) as s when !print_universes -> s | GType _ -> GType None +let extern_universes = function + | Some _ as l when !print_universes -> l + | _ -> None + let rec extern inctx scopes vars r = let r' = remove_coercions inctx r in try @@ -590,11 +601,11 @@ let rec extern inctx scopes vars r = if !Flags.raw_print || !print_no_symbol then raise No_match; extern_symbol scopes vars r'' (uninterp_notations r'') with No_match -> match r' with - | GRef (loc,ref) -> + | GRef (loc,ref,us) -> extern_global loc (select_stronger_impargs (implicits_of_global ref)) - (extern_reference loc vars ref) + (extern_reference loc vars ref) (extern_universes us) - | GVar (loc,id) -> CRef (Ident (loc,id)) + | GVar (loc,id) -> CRef (Ident (loc,id),None) | GEvar (loc,n,None) when !print_meta_as_hole -> CHole (loc, None, None) @@ -606,7 +617,7 @@ let rec extern inctx scopes vars r = | GApp (loc,f,args) -> (match f with - | GRef (rloc,ref) -> + | GRef (rloc,ref,us) -> let subscopes = find_arguments_scope ref in let args = extern_args (extern true) (snd scopes) vars args subscopes in @@ -652,11 +663,24 @@ let rec extern inctx scopes vars r = | Not_found | No_match | Exit -> extern_app loc inctx (select_stronger_impargs (implicits_of_global ref)) - (Some ref,extern_reference rloc vars ref) args + (Some ref,extern_reference rloc vars ref) (extern_universes us) args end + + | GProj (loc,p,c) -> + let ref = ConstRef p in + let subscopes = find_arguments_scope ref in + let args = + extern_args (extern true) (snd scopes) vars (c :: args) subscopes + in + extern_app loc inctx [] (Some ref, extern_reference loc vars ref) + None args + | _ -> - explicitize loc inctx [] (None,sub_extern false scopes vars f) - (List.map (sub_extern true scopes vars) args)) + explicitize loc inctx [] (None,sub_extern false scopes vars f) + (List.map (sub_extern true scopes vars) args)) + + | GProj (loc,p,c) -> + extern inctx scopes vars (GApp (loc,r',[])) | GLetIn (loc,na,t,c) -> CLetIn (loc,(loc,na),sub_extern false scopes vars t, @@ -816,7 +840,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function let args1, args2 = List.chop n args in let subscopes, impls = match f with - | GRef (_,ref) -> + | GRef (_,ref,us) -> let subscopes = try List.skipn n (find_arguments_scope ref) with Failure _ -> [] in @@ -830,13 +854,13 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function [], [] in (if Int.equal n 0 then f else GApp (Loc.ghost,f,args1)), args2, subscopes, impls - | GApp (_,(GRef (_,ref) as f),args), None -> + | GApp (_,(GRef (_,ref,us) as f),args), None -> let subscopes = find_arguments_scope ref in let impls = select_impargs_size (List.length args) (implicits_of_global ref) in f, args, subscopes, impls - | GRef _, Some 0 -> GApp (Loc.ghost,t,[]), [], [], [] + | GRef (_,ref,us), Some 0 -> GApp (Loc.ghost,t,[]), [], [], [] | _, None -> t, [], [], [] | _ -> raise No_match in (* Try matching ... *) @@ -871,7 +895,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function List.map (fun (c,(scopt,scl)) -> extern true (scopt,scl@scopes) vars c, None) terms in - let a = CRef (Qualid (loc, shortest_qualid_of_syndef vars kn)) in + let a = CRef (Qualid (loc, shortest_qualid_of_syndef vars kn),None) in if List.is_empty l then a else CApp (loc,(None,a),l) in if List.is_empty args then e else @@ -934,7 +958,7 @@ let any_any_branch = (loc,[],[PatVar (loc,Anonymous)],GHole (loc,Evar_kinds.InternalHole,None)) let rec glob_of_pat env = function - | PRef ref -> GRef (loc,ref) + | PRef ref -> GRef (loc,ref,None) | PVar id -> GVar (loc,id) | PEvar (n,l) -> GEvar (loc,n,Some (Array.map_to_list (glob_of_pat env) l)) | PRel n -> @@ -946,6 +970,7 @@ let rec glob_of_pat env = function GVar (loc,id) | PMeta None -> GHole (loc,Evar_kinds.InternalHole, None) | PMeta (Some n) -> GPatVar (loc,(false,n)) + | PProj (p,c) -> GApp (loc,GRef (loc, ConstRef p,None),[glob_of_pat env c]) | PApp (f,args) -> GApp (loc,glob_of_pat env f,Array.map_to_list (glob_of_pat env) args) | PSoApp (n,args) -> diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 7fba83e66f..0905ad1d6b 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -93,7 +93,7 @@ let global_reference_of_reference ref = locate_reference (snd (qualid_of_reference ref)) let global_reference id = - constr_of_global (locate_reference (qualid_of_ident id)) + Universes.constr_of_global (locate_reference (qualid_of_ident id)) let construct_reference ctx id = try @@ -102,7 +102,7 @@ let construct_reference ctx id = global_reference id let global_reference_in_absolute_module dir id = - constr_of_global (Nametab.global_of_path (Libnames.make_path dir id)) + Universes.constr_of_global (Nametab.global_of_path (Libnames.make_path dir id)) (**********************************************************************) (* Internalization errors *) @@ -300,7 +300,7 @@ let reset_tmp_scope env = {env with tmp_scope = None} let set_scope env = function | CastConv (GSort _) -> set_type_scope env - | CastConv (GRef (_,ref) | GApp (_,GRef (_,ref),_)) -> + | CastConv (GRef (_,ref,_) | GApp (_,GRef (_,ref,_),_)) -> {env with tmp_scope = compute_scope_of_global ref} | _ -> env @@ -410,7 +410,7 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar let name = let id = match ty with - | CApp (_, (_, CRef (Ident (loc,id))), _) -> id + | CApp (_, (_, CRef (Ident (loc,id),_)), _) -> id | _ -> Id.of_string "H" in Implicit_quantifiers.make_fresh ids' (Global.env ()) id in Name name @@ -650,7 +650,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id = try let ty,expl_impls,impls,argsc = Id.Map.find id genv.impls in let expl_impls = List.map - (fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) expl_impls in + (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 @@ -682,19 +682,38 @@ 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), impls, scopes, [] + GRef (loc, ref, None), impls, scopes, [] with e when Errors.noncritical e -> (* [id] a goal variable *) GVar (loc,id), [], [], [] -let find_appl_head_data = function - | GRef (_,ref) as x -> x,implicits_of_global ref,find_arguments_scope ref,[] - | GApp (_,GRef (_,ref),l) as x +let is_projection_ref = function + | ConstRef r -> if Environ.is_projection r (Global.env ()) then Some r else None + | _ -> None + +let find_appl_head_data c = + match c with + | GRef (loc,ref,_) as x -> + let impls = implicits_of_global ref in + let isproj, impls = + match is_projection_ref ref with + | Some r -> true, List.map (projection_implicits (Global.env ()) r) impls + | None -> false, impls + in + let scopes = find_arguments_scope ref in + x, isproj, impls, scopes, [] + | GApp (_,GRef (_,ref,_),l) as x when l != [] && Flags.version_strictly_greater Flags.V8_2 -> let n = List.length l in - x,List.map (drop_first_implicits n) (implicits_of_global ref), - List.skipn_at_least n (find_arguments_scope ref),[] - | x -> x,[],[],[] + let impls = implicits_of_global ref in + let isproj, impls = + match is_projection_ref ref with + | Some r -> true, List.map (projection_implicits (Global.env ()) r) impls + | None -> false, impls + in + x, isproj, List.map (drop_first_implicits n) impls, + List.skipn_at_least n (find_arguments_scope ref),[] + | x -> x,false,[],[],[] let error_not_enough_arguments loc = user_err_loc (loc,"",str "Abbreviation is not applied enough.") @@ -726,8 +745,7 @@ let intern_reference ref = (* Is it a global reference or a syntactic definition? *) let intern_qualid loc qid intern env lvar args = match intern_extended_global_of_qualid (loc,qid) with - | TrueGlobal ref -> - GRef (loc, ref), args + | TrueGlobal ref -> GRef (loc, ref, None), args | SynDef sp -> let (ids,c) = Syntax_def.search_syntactic_definition sp in let nids = List.length ids in @@ -742,7 +760,7 @@ let intern_qualid loc qid intern env lvar args = (* Rule out section vars since these should have been found by intern_var *) let intern_non_secvar_qualid loc qid intern env lvar args = match intern_qualid loc qid intern env lvar args with - | GRef (_, VarRef _),_ -> raise Not_found + | GRef (_, VarRef _, _),_ -> raise Not_found | r -> r let intern_applied_reference intern env namedctx lvar args = function @@ -751,22 +769,24 @@ let intern_applied_reference intern env namedctx lvar args = function try intern_qualid loc qid intern env lvar args with Not_found -> error_global_not_found_loc loc qid in - find_appl_head_data r, args2 + let x, isproj, imp, scopes, l = find_appl_head_data r in + (x,imp,scopes,l), isproj, args2 | Ident (loc, id) -> - try intern_var env lvar namedctx loc id, args + try intern_var env lvar namedctx loc id, false, args with Not_found -> let qid = qualid_of_ident id in try let r,args2 = intern_non_secvar_qualid loc qid intern env lvar args in - find_appl_head_data r, args2 + let x, isproj, imp, scopes, l = find_appl_head_data r in + (x,imp,scopes,l), isproj, args2 with Not_found -> (* Extra allowance for non globalizing functions *) if !interning_grammar || env.unb then - (GVar (loc,id), [], [], []),args + (GVar (loc,id), [], [], []), false, args else error_global_not_found_loc loc qid let interp_reference vars r = - let (r,_,_,_),_ = + let (r,_,_,_),_,_ = intern_applied_reference (fun _ -> error_not_enough_arguments Loc.ghost) {ids = Id.Set.empty; unb = false ; tmp_scope = None; scopes = []; impls = empty_internalization_env} [] @@ -1276,10 +1296,9 @@ let merge_impargs l args = let check_projection isproj nargs r = match (r,isproj) with - | GRef (loc, ref), Some _ -> + | GRef (loc, ref, _), Some _ -> (try - let n = Recordops.find_projection_nparams ref + 1 in - if not (Int.equal nargs n) then + if not (Int.equal nargs 1) then user_err_loc (loc,"",str "Projection does not have the right number of explicit parameters."); with Not_found -> user_err_loc @@ -1291,7 +1310,8 @@ let get_implicit_name n imps = Some (Impargs.name_of_implicit (List.nth imps (n-1))) let set_hole_implicit i b = function - | GRef (loc,r) | GApp (_,GRef (loc,r),_) -> (loc,Evar_kinds.ImplicitArg (r,i,b),None) + | GRef (loc,r,_) | GApp (_,GRef (loc,r,_),_) -> (loc,Evar_kinds.ImplicitArg (r,i,b),None) + | GProj (loc,p,_) -> (loc,Evar_kinds.ImplicitArg (ConstRef p,i,b),None) | GVar (loc,id) -> (loc,Evar_kinds.ImplicitArg (VarRef id,i,b),None) | _ -> anomaly (Pp.str "Only refs have implicits") @@ -1335,14 +1355,17 @@ let extract_explicit_arg imps args = (**********************************************************************) (* Main loop *) +let is_projection_ref env = function + | ConstRef c -> Environ.is_projection c env + | _ -> false + let internalize globalenv env allow_patvar lvar c = let rec intern env = function - | CRef ref as x -> - let (c,imp,subscopes,l),_ = + | CRef (ref,us) as x -> + let (c,imp,subscopes,l),isproj,_ = intern_applied_reference intern env (Environ.named_context globalenv) lvar [] ref in - (match intern_impargs c env imp subscopes l with - | [] -> c - | l -> GApp (constr_loc x, c, l)) + apply_impargs (None, isproj) c env imp subscopes l (constr_loc x) + | CFix (loc, (locid,iddef), dl) -> let lf = List.map (fun ((_, id),_,_,_,_) -> id) dl in let dl = Array.of_list dl in @@ -1435,33 +1458,35 @@ let internalize globalenv env allow_patvar lvar c = | CDelimiters (loc, key, e) -> intern {env with tmp_scope = None; scopes = find_delimiters_scope loc key :: env.scopes} e - | CAppExpl (loc, (isproj,ref), args) -> - let (f,_,args_scopes,_),args = + | CAppExpl (loc, (isproj,ref,us), args) -> + let (f,_,args_scopes,_),_,args = let args = List.map (fun a -> (a,None)) args in - intern_applied_reference intern env (Environ.named_context globalenv) lvar args ref in - check_projection isproj (List.length args) f; + intern_applied_reference intern env (Environ.named_context globalenv) + lvar args ref in + (* check_projection isproj (List.length args) f; *) (* Rem: GApp(_,f,[]) stands for @f *) - GApp (loc, f, intern_args env args_scopes (List.map fst args)) + GApp (loc, f, intern_args env args_scopes (List.map fst args)) + | CApp (loc, (isproj,f), args) -> let isproj,f,args = match f with (* Compact notations like "t.(f args') args" *) - | CApp (_,(Some _,f), args') when not (Option.has_some isproj) -> isproj,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 = + let (c,impargs,args_scopes,l),isprojf,args = match f with - | CRef ref -> intern_applied_reference intern env (Environ.named_context globalenv) lvar args ref + | CRef (ref,us) -> + intern_applied_reference intern env + (Environ.named_context globalenv) lvar args ref | CNotation (loc,ntn,([],[],[])) -> let c = intern_notation intern env lvar loc ntn ([],[],[]) in - find_appl_head_data c, args - | x -> (intern env f,[],[],[]), args in - let args = - intern_impargs c env impargs args_scopes (merge_impargs l args) in - check_projection isproj (List.length args) c; - (match c with - (* Now compact "(f args') args" *) - | GApp (loc', f', args') -> GApp (Loc.merge loc' loc, f',args'@args) - | _ -> GApp (loc, c, args)) + let x, isproj, impl, scopes, l = find_appl_head_data c in + (x,impl,scopes,l), false, args + | x -> (intern env f,[],[],[]), false, args in + apply_impargs (isproj,isprojf) c env impargs args_scopes + (merge_impargs l args) loc + | CRecord (loc, _, fs) -> let cargs = sort_fields true loc fs @@ -1472,7 +1497,7 @@ let internalize globalenv env allow_patvar lvar c = | None -> user_err_loc (loc, "intern", str"No constructor inference.") | Some (n, constrname, args) -> let pars = List.make n (CHole (loc, None, None)) in - let app = CAppExpl (loc, (None, constrname), List.rev_append pars args) in + let app = CAppExpl (loc, (None, constrname,None), List.rev_append pars args) in intern env app end | CCases (loc, sty, rtnpo, tms, eqns) -> @@ -1500,7 +1525,7 @@ let internalize globalenv env allow_patvar lvar c = | [] -> Option.map (intern_type env') rtnpo (* Only PatVar in "in" clauses *) | l -> let thevars,thepats=List.split l in Some ( - GCases(Loc.ghost,Term.RegularStyle,Some (GSort (Loc.ghost,GType None)), (* "return Type" *) + GCases(Loc.ghost,Term.RegularStyle,(* Some (GSort (Loc.ghost,GType None)) *)None, (* "return Type" *) List.map (fun id -> GVar (Loc.ghost,id),(Name id,None)) thevars, (* "match v1,..,vn" *) [Loc.ghost,[],thepats, (* "|p1,..,pn" *) Option.cata (intern_type env') (GHole(Loc.ghost,Evar_kinds.CasesType,None)) rtnpo; (* "=> P" is there were a P "=> _" else *) @@ -1599,7 +1624,7 @@ let internalize globalenv env allow_patvar lvar c = (* the "as" part *) let extra_id,na = match tm', na with | GVar (loc,id), None when not (Id.Map.mem id (snd lvar)) -> Some id,(loc,Name id) - | GRef (loc, VarRef id), None -> Some id,(loc,Name id) + | GRef (loc, VarRef id, _), None -> Some id,(loc,Name id) | _, None -> None,(Loc.ghost,Anonymous) | _, Some (loc,na) -> None,(loc,na) in (* the "in" part *) @@ -1691,6 +1716,41 @@ let internalize globalenv env allow_patvar lvar c = intern_args env subscopes rargs in aux 1 l subscopes eargs rargs + and make_first_explicit (l, r) = + match r with + | hd :: tl -> l, None :: tl + | [] -> l, [] + + and apply_impargs (isproj,isprojf) c env imp subscopes l loc = + let l = + let imp = + if isprojf && isproj <> None then + (* Drop first implicit which corresponds to record given in c.(p) notation *) + List.map make_first_explicit imp + else imp + in intern_impargs c env imp subscopes l + in + if isprojf then + match c, l with + | GApp (loc', GRef (loc'', ConstRef f, _), hd :: tl), rest -> + let proj = GProj (Loc.merge loc'' (loc_of_glob_constr hd), f, hd) in + if List.is_empty tl then smart_gapp proj loc rest + else GApp (loc, proj, tl @ rest) + | GRef (loc', ConstRef f, _), hd :: tl -> + let proj = GProj (Loc.merge loc' (loc_of_glob_constr hd), f, hd) in + smart_gapp proj loc tl + | _ -> user_err_loc (loc, "apply_impargs", + str"Projection is not applied to enough arguments") + else + (* check_projection isproj *) + smart_gapp c loc l + + and smart_gapp f loc = function + | [] -> f + | l -> match f with + | GApp (loc', g, args) -> GApp (Loc.merge loc' loc, g, args@l) + | _ -> GApp (Loc.merge (loc_of_glob_constr f) loc, f, l) + and intern_args env subscopes = function | [] -> [] | a::args -> @@ -1871,7 +1931,7 @@ let interp_rawcontext_evars evdref env bl = (push_rel d env, d::params, succ n, impls) | Some b -> let c = understand_judgment_tcc evdref env b in - let d = (na, Some c.uj_val, Termops.refresh_universes c.uj_type) in + let d = (na, Some c.uj_val, c.uj_type) in (push_rel d env, d::params, succ n, impls)) (env,[],1,[]) (List.rev bl) in (env, par), impls diff --git a/interp/constrintern.mli b/interp/constrintern.mli index a0bcdc4f4e..9ce6ec7794 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -91,13 +91,13 @@ val intern_context : bool -> env -> internalization_env -> local_binder list -> (** Main interpretation functions expecting evars to be all resolved *) val interp_constr : evar_map -> env -> ?impls:internalization_env -> - constr_expr -> constr + constr_expr -> constr Univ.in_universe_context_set val interp_casted_constr : evar_map -> env -> ?impls:internalization_env -> - constr_expr -> types -> constr + constr_expr -> types -> constr Univ.in_universe_context_set val interp_type : evar_map -> env -> ?impls:internalization_env -> - constr_expr -> types + constr_expr -> types Univ.in_universe_context_set (** Main interpretation function expecting evars to be all resolved *) @@ -142,7 +142,7 @@ val interp_reference : ltac_sign -> reference -> glob_constr (** Interpret binders *) -val interp_binder : evar_map -> env -> Name.t -> constr_expr -> types +val interp_binder : evar_map -> env -> Name.t -> constr_expr -> types Univ.in_universe_context_set val interp_binder_evars : evar_map ref -> env -> Name.t -> constr_expr -> types @@ -153,6 +153,16 @@ val interp_context_evars : evar_map ref -> env -> local_binder list -> 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 -> *) +(* evar_map -> env -> local_binder 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 -> *) +(* evar_map -> env -> local_binder 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) *) diff --git a/interp/coqlib.ml b/interp/coqlib.ml index bf5d225b2c..3df071aff7 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -32,7 +32,7 @@ let find_reference locstr dir s = anomaly ~label:locstr (str "cannot find " ++ Libnames.pr_path sp) let coq_reference locstr dir s = find_reference locstr (coq::dir) s -let coq_constant locstr dir s = constr_of_global (coq_reference locstr dir s) +let coq_constant locstr dir s = Universes.constr_of_global (coq_reference locstr dir s) let gen_reference = coq_reference let gen_constant = coq_constant @@ -44,7 +44,7 @@ let has_suffix_in_dirs dirs ref = let global_of_extended q = try Some (global_of_extended_global q) with Not_found -> None -let gen_constant_in_modules locstr dirs s = +let gen_reference_in_modules locstr dirs s = let dirs = List.map make_dir dirs in let qualid = qualid_of_string s in let all = Nametab.locate_extended_all qualid in @@ -52,7 +52,7 @@ let gen_constant_in_modules locstr dirs s = let all = List.sort_uniquize RefOrdered_env.compare all in let these = List.filter (has_suffix_in_dirs dirs) all in match these with - | [x] -> constr_of_global x + | [x] -> x | [] -> anomaly ~label:locstr (str ("cannot find "^s^ " in module"^(if List.length dirs > 1 then "s " else " ")) ++ @@ -65,6 +65,9 @@ let gen_constant_in_modules locstr dirs s = str (" in module"^(if List.length dirs > 1 then "s " else " ")) ++ prlist_with_sep pr_comma pr_dirpath dirs) +let gen_constant_in_modules locstr dirs s = + Universes.constr_of_global (gen_reference_in_modules locstr dirs s) + (* For tactics/commands requiring vernacular libraries *) @@ -100,6 +103,10 @@ let logic_constant dir s = let d = "Logic"::dir in check_required_library (coq::d); gen_constant "Coqlib" d s +let logic_reference dir s = + let d = "Logic"::dir in + check_required_library ("Coq"::d); gen_reference "Coqlib" d s + let arith_dir = [coq;"Arith"] let arith_modules = [arith_dir] @@ -144,10 +151,14 @@ let make_con dir id = Globnames.encode_con dir (Id.of_string id) (** Identity *) -let id = make_con datatypes_module "id" -let type_of_id = make_con datatypes_module "ID" +let id = make_con datatypes_module "idProp" +let type_of_id = make_con datatypes_module "IDProp" -let _ = Termops.set_impossible_default_clause (mkConst id,mkConst type_of_id) +let _ = Termops.set_impossible_default_clause + (fun () -> + let c, ctx = Universes.fresh_global_instance (Global.env()) (ConstRef id) in + let (_, u) = destConst c in + (c,mkConstU (type_of_id,u)), ctx) (** Natural numbers *) let nat_kn = make_ind datatypes_module "nat" @@ -181,11 +192,11 @@ let jmeq_kn = make_ind jmeq_module "JMeq" let glob_jmeq = IndRef (jmeq_kn,0) type coq_sigma_data = { - proj1 : constr; - proj2 : constr; - elim : constr; - intro : constr; - typ : constr } + proj1 : global_reference; + proj2 : global_reference; + elim : global_reference; + intro : global_reference; + typ : global_reference } type coq_bool_data = { andb : constr; @@ -200,56 +211,58 @@ let build_bool_type () = let build_sigma_set () = anomaly (Pp.str "Use build_sigma_type") let build_sigma_type () = - { proj1 = init_constant ["Specif"] "projT1"; - proj2 = init_constant ["Specif"] "projT2"; - elim = init_constant ["Specif"] "sigT_rect"; - intro = init_constant ["Specif"] "existT"; - typ = init_constant ["Specif"] "sigT" } + { proj1 = init_reference ["Specif"] "projT1"; + proj2 = init_reference ["Specif"] "projT2"; + elim = init_reference ["Specif"] "sigT_rect"; + intro = init_reference ["Specif"] "existT"; + typ = init_reference ["Specif"] "sigT" } let build_sigma () = - { proj1 = init_constant ["Specif"] "proj1_sig"; - proj2 = init_constant ["Specif"] "proj2_sig"; - elim = init_constant ["Specif"] "sig_rect"; - intro = init_constant ["Specif"] "exist"; - typ = init_constant ["Specif"] "sig" } + { proj1 = init_reference ["Specif"] "proj1_sig"; + proj2 = init_reference ["Specif"] "proj2_sig"; + elim = init_reference ["Specif"] "sig_rect"; + intro = init_reference ["Specif"] "exist"; + typ = init_reference ["Specif"] "sig" } + let build_prod () = - { proj1 = init_constant ["Datatypes"] "fst"; - proj2 = init_constant ["Datatypes"] "snd"; - elim = init_constant ["Datatypes"] "prod_rec"; - intro = init_constant ["Datatypes"] "pair"; - typ = init_constant ["Datatypes"] "prod" } + { proj1 = init_reference ["Datatypes"] "fst"; + proj2 = init_reference ["Datatypes"] "snd"; + elim = init_reference ["Datatypes"] "prod_rec"; + intro = init_reference ["Datatypes"] "pair"; + typ = init_reference ["Datatypes"] "prod" } (* Equalities *) type coq_eq_data = { - eq : constr; - ind : constr; - refl : constr; - sym : constr; - trans: constr; - congr: constr } + eq : global_reference; + ind : global_reference; + refl : global_reference; + sym : global_reference; + trans: global_reference; + congr: global_reference } (* Data needed for discriminate and injection *) type coq_inversion_data = { - inv_eq : constr; (* : forall params, t -> Prop *) - inv_ind : constr; (* : forall params P y, eq params y -> P y *) - inv_congr: constr (* : forall params B (f:t->B) y, eq params y -> f c=f y *) + inv_eq : global_reference; (* : forall params, t -> Prop *) + inv_ind : global_reference; (* : forall params P y, eq params y -> P y *) + inv_congr: global_reference (* : forall params B (f:t->B) y, eq params y -> f c=f y *) } +let lazy_init_reference dir id = lazy (init_reference dir id) let lazy_init_constant dir id = lazy (init_constant dir id) -let lazy_logic_constant dir id = lazy (logic_constant dir id) +let lazy_logic_reference dir id = lazy (logic_reference dir id) (* Leibniz equality on Type *) -let coq_eq_eq = lazy_init_constant ["Logic"] "eq" -let coq_eq_refl = lazy_init_constant ["Logic"] "eq_refl" -let coq_eq_ind = lazy_init_constant ["Logic"] "eq_ind" -let coq_eq_congr = lazy_init_constant ["Logic"] "f_equal" -let coq_eq_sym = lazy_init_constant ["Logic"] "eq_sym" -let coq_eq_trans = lazy_init_constant ["Logic"] "eq_trans" -let coq_f_equal2 = lazy_init_constant ["Logic"] "f_equal2" +let coq_eq_eq = lazy_init_reference ["Logic"] "eq" +let coq_eq_refl = lazy_init_reference ["Logic"] "eq_refl" +let coq_eq_ind = lazy_init_reference ["Logic"] "eq_ind" +let coq_eq_congr = lazy_init_reference ["Logic"] "f_equal" +let coq_eq_sym = lazy_init_reference ["Logic"] "eq_sym" +let coq_eq_trans = lazy_init_reference ["Logic"] "eq_trans" +let coq_f_equal2 = lazy_init_reference ["Logic"] "f_equal2" let coq_eq_congr_canonical = - lazy_init_constant ["Logic"] "f_equal_canonical_form" + lazy_init_reference ["Logic"] "f_equal_canonical_form" let build_coq_eq_data () = let _ = check_required_library logic_module_name in { @@ -260,6 +273,9 @@ let build_coq_eq_data () = trans = Lazy.force coq_eq_trans; congr = Lazy.force coq_eq_congr } +let make_dirpath dir = + Names.make_dirpath (List.map id_of_string dir) + let build_coq_eq () = Lazy.force coq_eq_eq let build_coq_eq_refl () = Lazy.force coq_eq_refl let build_coq_eq_sym () = Lazy.force coq_eq_sym @@ -273,14 +289,15 @@ let build_coq_inversion_eq_data () = (* Heterogenous equality on Type *) -let coq_jmeq_eq = lazy_logic_constant ["JMeq"] "JMeq" -let coq_jmeq_refl = lazy_logic_constant ["JMeq"] "JMeq_refl" -let coq_jmeq_ind = lazy_logic_constant ["JMeq"] "JMeq_ind" -let coq_jmeq_sym = lazy_logic_constant ["JMeq"] "JMeq_sym" -let coq_jmeq_congr = lazy_logic_constant ["JMeq"] "JMeq_congr" -let coq_jmeq_trans = lazy_logic_constant ["JMeq"] "JMeq_trans" +let coq_jmeq_eq = lazy_logic_reference ["JMeq"] "JMeq" +let coq_jmeq_hom = lazy_logic_reference ["JMeq"] "JMeq_hom" +let coq_jmeq_refl = lazy_logic_reference ["JMeq"] "JMeq_refl" +let coq_jmeq_ind = lazy_logic_reference ["JMeq"] "JMeq_ind" +let coq_jmeq_sym = lazy_logic_reference ["JMeq"] "JMeq_sym" +let coq_jmeq_congr = lazy_logic_reference ["JMeq"] "JMeq_congr" +let coq_jmeq_trans = lazy_logic_reference ["JMeq"] "JMeq_trans" let coq_jmeq_congr_canonical = - lazy_logic_constant ["JMeq"] "JMeq_congr_canonical_form" + lazy_logic_reference ["JMeq"] "JMeq_congr_canonical_form" let build_coq_jmeq_data () = let _ = check_required_library jmeq_module_name in { @@ -291,14 +308,9 @@ let build_coq_jmeq_data () = trans = Lazy.force coq_jmeq_trans; congr = Lazy.force coq_jmeq_congr } -let join_jmeq_types eq = - mkLambda(Name (Id.of_string "A"),Termops.new_Type(), - mkLambda(Name (Id.of_string "x"),mkRel 1, - mkApp (eq,[|mkRel 2;mkRel 1;mkRel 2|]))) - let build_coq_inversion_jmeq_data () = let _ = check_required_library logic_module_name in { - inv_eq = join_jmeq_types (Lazy.force coq_jmeq_eq); + inv_eq = Lazy.force coq_jmeq_hom; inv_ind = Lazy.force coq_jmeq_ind; inv_congr = Lazy.force coq_jmeq_congr_canonical } @@ -308,13 +320,13 @@ let coq_sumbool = lazy_init_constant ["Specif"] "sumbool" let build_coq_sumbool () = Lazy.force coq_sumbool (* Equality on Type as a Type *) -let coq_identity_eq = lazy_init_constant ["Datatypes"] "identity" -let coq_identity_refl = lazy_init_constant ["Datatypes"] "identity_refl" -let coq_identity_ind = lazy_init_constant ["Datatypes"] "identity_ind" -let coq_identity_congr = lazy_init_constant ["Logic_Type"] "identity_congr" -let coq_identity_sym = lazy_init_constant ["Logic_Type"] "identity_sym" -let coq_identity_trans = lazy_init_constant ["Logic_Type"] "identity_trans" -let coq_identity_congr_canonical = lazy_init_constant ["Logic_Type"] "identity_congr_canonical_form" +let coq_identity_eq = lazy_init_reference ["Datatypes"] "identity" +let coq_identity_refl = lazy_init_reference ["Datatypes"] "identity_refl" +let coq_identity_ind = lazy_init_reference ["Datatypes"] "identity_ind" +let coq_identity_congr = lazy_init_reference ["Logic_Type"] "identity_congr" +let coq_identity_sym = lazy_init_reference ["Logic_Type"] "identity_sym" +let coq_identity_trans = lazy_init_reference ["Logic_Type"] "identity_trans" +let coq_identity_congr_canonical = lazy_init_reference ["Logic_Type"] "identity_congr_canonical_form" let build_coq_identity_data () = let _ = check_required_library datatypes_module_name in { @@ -333,9 +345,9 @@ let build_coq_inversion_identity_data () = inv_congr = Lazy.force coq_identity_congr_canonical } (* Equality to true *) -let coq_eq_true_eq = lazy_init_constant ["Datatypes"] "eq_true" -let coq_eq_true_ind = lazy_init_constant ["Datatypes"] "eq_true_ind" -let coq_eq_true_congr = lazy_init_constant ["Logic"] "eq_true_congr" +let coq_eq_true_eq = lazy_init_reference ["Datatypes"] "eq_true" +let coq_eq_true_ind = lazy_init_reference ["Datatypes"] "eq_true_ind" +let coq_eq_true_congr = lazy_init_reference ["Logic"] "eq_true_congr" let build_coq_inversion_eq_true_data () = let _ = check_required_library datatypes_module_name in diff --git a/interp/coqlib.mli b/interp/coqlib.mli index 9b0f8deb9c..d253cf7ddc 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -42,6 +42,7 @@ val gen_reference : message -> string list -> string -> global_reference (** Search in several modules (not prefixed by "Coq") *) val gen_constant_in_modules : string->string list list-> string -> constr +val gen_reference_in_modules : string->string list list-> string -> global_reference val arith_modules : string list list val zarith_base_modules : string list list val init_modules : string list list @@ -101,43 +102,49 @@ val build_bool_type : coq_bool_data delayed (** {6 For Equality tactics } *) type coq_sigma_data = { - proj1 : constr; - proj2 : constr; - elim : constr; - intro : constr; - typ : constr } + proj1 : global_reference; + proj2 : global_reference; + elim : global_reference; + intro : global_reference; + typ : global_reference } val build_sigma_set : coq_sigma_data delayed val build_sigma_type : coq_sigma_data delayed val build_sigma : coq_sigma_data delayed +(* val build_sigma_type_in : Environ.env -> coq_sigma_data Univ.in_universe_context_set *) +(* val build_sigma_in : Environ.env -> coq_sigma_data Univ.in_universe_context_set *) +(* val build_prod_in : Environ.env -> coq_sigma_data Univ.in_universe_context_set *) +(* val build_coq_eq_data_in : Environ.env -> coq_eq_data Univ.in_universe_context_set *) + (** Non-dependent pairs in Set from Datatypes *) val build_prod : coq_sigma_data delayed type coq_eq_data = { - eq : constr; - ind : constr; - refl : constr; - sym : constr; - trans: constr; - congr: constr } + eq : global_reference; + ind : global_reference; + refl : global_reference; + sym : global_reference; + trans: global_reference; + congr: global_reference } val build_coq_eq_data : coq_eq_data delayed + val build_coq_identity_data : coq_eq_data delayed val build_coq_jmeq_data : coq_eq_data delayed -val build_coq_eq : constr delayed (** = [(build_coq_eq_data()).eq] *) -val build_coq_eq_refl : constr delayed (** = [(build_coq_eq_data()).refl] *) -val build_coq_eq_sym : constr delayed (** = [(build_coq_eq_data()).sym] *) -val build_coq_f_equal2 : constr delayed +val build_coq_eq : global_reference delayed (** = [(build_coq_eq_data()).eq] *) +val build_coq_eq_refl : global_reference delayed (** = [(build_coq_eq_data()).refl] *) +val build_coq_eq_sym : global_reference delayed (** = [(build_coq_eq_data()).sym] *) +val build_coq_f_equal2 : global_reference delayed (** Data needed for discriminate and injection *) type coq_inversion_data = { - inv_eq : constr; (** : forall params, args -> Prop *) - inv_ind : constr; (** : forall params P (H : P params) args, eq params args + inv_eq : global_reference; (** : forall params, args -> Prop *) + inv_ind : global_reference; (** : forall params P (H : P params) args, eq params args -> P args *) - inv_congr: constr (** : forall params B (f:t->B) args, eq params args -> + inv_congr: global_reference (** : forall params B (f:t->B) args, eq params args -> f params = f args *) } diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index ca5b0eddd3..80b5830fd1 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -110,7 +110,7 @@ let type_of_global_ref gr = "var" ^ type_of_logical_kind (Decls.variable_kind v) | Globnames.IndRef ind -> let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in - if mib.Declarations.mind_record then + if mib.Declarations.mind_record <> None then if mib.Declarations.mind_finite then "rec" else "corec" else if mib.Declarations.mind_finite then "ind" diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 2d55a6b63b..c69eb629de 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -90,8 +90,8 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = else l in let rec aux bdvars l c = match c with - | CRef (Ident (loc,id)) -> found loc id bdvars l - | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id)) :: _, [], [])) when not (Id.Set.mem id bdvars) -> + | CRef (Ident (loc,id),_) -> found loc id bdvars l + | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id),_) :: _, [], [])) when not (Id.Set.mem id bdvars) -> Topconstr.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add id bdvars) l c | c -> Topconstr.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c in aux bound l c @@ -127,6 +127,7 @@ let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.emp else (id, loc) :: vs else vs | GApp (loc,f,args) -> List.fold_left (vars bound) vs (f::args) + | GProj (loc,p,c) -> vars bound vs c | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) | GLetIn (loc,na,ty,c) -> let vs' = vars bound vs ty in let bound' = add_name_to_ids bound na in @@ -241,19 +242,19 @@ let combine_params avoid fn applied needed = let combine_params_freevar = fun avoid (_, (na, _, _)) -> let id' = next_name_away_from na avoid in - (CRef (Ident (Loc.ghost, id')), Id.Set.add id' avoid) + (CRef (Ident (Loc.ghost, id'),None), Id.Set.add id' avoid) let destClassApp cl = match cl with - | CApp (loc, (None, CRef ref), l) -> loc, ref, List.map fst l - | CAppExpl (loc, (None, ref), l) -> loc, ref, l - | CRef ref -> loc_of_reference ref, ref, [] + | CApp (loc, (None, CRef (ref,_)), l) -> loc, ref, List.map fst l + | CAppExpl (loc, (None, ref,_), l) -> loc, ref, l + | CRef (ref,_) -> loc_of_reference ref, ref, [] | _ -> raise Not_found let destClassAppExpl cl = match cl with - | CApp (loc, (None, CRef ref), l) -> loc, ref, l - | CRef ref -> loc_of_reference ref, ref, [] + | CApp (loc, (None, CRef (ref,_)), l) -> loc, ref, l + | CRef (ref,_) -> loc_of_reference ref, ref, [] | _ -> raise Not_found let implicit_application env ?(allow_partial=true) f ty = @@ -285,7 +286,7 @@ let implicit_application env ?(allow_partial=true) f ty = end; let pars = List.rev (List.combine ci rd) in let args, avoid = combine_params avoid f par pars in - CAppExpl (loc, (None, id), args), avoid + CAppExpl (loc, (None, id, None), args), avoid in c, avoid let implicits_of_glob_constr ?(with_products=true) l = diff --git a/interp/modintern.ml b/interp/modintern.ml index 81d0a0f644..2d81194f2c 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -61,7 +61,7 @@ let transl_with_decl env = function | CWith_Module ((_,fqid),qid) -> WithMod (fqid,lookup_module qid) | CWith_Definition ((_,fqid),c) -> - WithDef (fqid,interp_constr Evd.empty env c) + WithDef (fqid,fst (interp_constr Evd.empty env c)) (*FIXME*) let loc_of_module = function | CMident (loc,_) | CMapply (loc,_,_) | CMwith (loc,_,_) -> loc diff --git a/interp/notation.ml b/interp/notation.ml index 6e5ac5f33e..6fd6001f4f 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -258,12 +258,12 @@ let notations_key_table = ref (KeyMap.empty : notation_rule list KeyMap.t) let prim_token_key_table = ref KeyMap.empty let glob_prim_constr_key = function - | GApp (_,GRef (_,ref),_) | GRef (_,ref) -> RefKey (canonical_gr ref) + | GApp (_,GRef (_,ref,_),_) | GRef (_,ref,_) -> RefKey (canonical_gr ref) | _ -> Oth let glob_constr_keys = function - | GApp (_,GRef (_,ref),_) -> [RefKey (canonical_gr ref); Oth] - | GRef (_,ref) -> [RefKey (canonical_gr ref)] + | GApp (_,GRef (_,ref,_),_) -> [RefKey (canonical_gr ref); Oth] + | GRef (_,ref,_) -> [RefKey (canonical_gr ref)] | _ -> [Oth] let cases_pattern_key = function @@ -455,8 +455,8 @@ let interp_prim_token = let rec rcp_of_glob looked_for = function | GVar (loc,id) -> RCPatAtom (loc,Some id) | GHole (loc,_,_) -> RCPatAtom (loc,None) - | GRef (loc,g) -> looked_for g; RCPatCstr (loc, g,[],[]) - | GApp (loc,GRef (_,g),l) -> + | GRef (loc,g,_) -> looked_for g; RCPatCstr (loc, g,[],[]) + | GApp (loc,GRef (_,g,_),l) -> looked_for g; RCPatCstr (loc, g, List.map (rcp_of_glob looked_for) l,[]) | _ -> raise Not_found @@ -502,7 +502,7 @@ let uninterp_prim_token_ind_pattern ind args = if not b then raise Notation_ops.No_match; let args' = List.map (fun x -> snd (glob_constr_of_closed_cases_pattern x)) args in - let ref = GRef (Loc.ghost,ref) in + let ref = GRef (Loc.ghost,ref,None) in match numpr (GApp (Loc.ghost,ref,args')) with | None -> raise Notation_ops.No_match | Some n -> (sc,n) @@ -655,13 +655,13 @@ let rebuild_arguments_scope (req,r,l,_) = match req with | ArgsScopeNoDischarge -> assert false | ArgsScopeAuto -> - let scs,cls = compute_arguments_scope_full (Global.type_of_global r) in + let scs,cls = compute_arguments_scope_full (fst(Universes.type_of_global r)(*FIXME?*)) in (req,r,scs,cls) | ArgsScopeManual -> (* Add to the manually given scopes the one found automatically for the extra parameters of the section. Discard the classes of the manually given scopes to avoid further re-computations. *) - let l',cls = compute_arguments_scope_full (Global.type_of_global r) in + let l',cls = compute_arguments_scope_full (Global.type_of_global_unsafe r) in let nparams = List.length l' - List.length l in let l1 = List.firstn nparams l' in let cls1 = List.firstn nparams cls in @@ -705,7 +705,7 @@ let find_arguments_scope r = with Not_found -> [] let declare_ref_arguments_scope ref = - let t = Global.type_of_global ref in + let t = Global.type_of_global_unsafe ref in declare_arguments_scope_gen ArgsScopeAuto ref (compute_arguments_scope_full t) diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 12b256c453..4984bfc387 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -55,6 +55,7 @@ let ldots_var = Id.of_string ".." let glob_constr_of_notation_constr_with_binders loc g f e = function | NVar id -> GVar (loc,id) | NApp (a,args) -> GApp (loc,f e a, List.map (f e) args) + | NProj (p,c) -> GProj (loc,p,f e c) | NList (x,y,iter,tail,swap) -> let t = f e tail in let it = f e iter in let innerl = (ldots_var,t)::(if swap then [] else [x,GVar(loc,y)]) in @@ -106,7 +107,7 @@ let glob_constr_of_notation_constr_with_binders loc g f e = function | NSort x -> GSort (loc,x) | NHole (x, arg) -> GHole (loc, x, arg) | NPatVar n -> GPatVar (loc,(false,n)) - | NRef x -> GRef (loc,x) + | NRef x -> GRef (loc,x,None) let glob_constr_of_notation_constr loc x = let rec aux () x = @@ -146,9 +147,10 @@ let split_at_recursive_part c = let on_true_do b f c = if b then (f c; b) else b let compare_glob_constr f add t1 t2 = match t1,t2 with - | GRef (_,r1), GRef (_,r2) -> eq_gr r1 r2 + | GRef (_,r1,_), GRef (_,r2,_) -> eq_gr r1 r2 | GVar (_,v1), GVar (_,v2) -> on_true_do (Id.equal v1 v2) add (Name v1) | GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 && List.for_all2eq f l1 l2 + | GProj (_,p1,c1), GProj (_, p2, c2) -> eq_constant p1 p2 && f c1 c2 | GLambda (_,na1,bk1,ty1,c1), GLambda (_,na2,bk2,ty2,c2) when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 -> on_true_do (f ty1 ty2 && f c1 c2) add na1 @@ -164,7 +166,7 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with | _,(GCases _ | GRec _ | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _) -> error "Unsupported construction in recursive notations." - | (GRef _ | GVar _ | GApp _ | GLambda _ | GProd _ + | (GRef _ | GVar _ | GApp _ | GProj _ | GLambda _ | GProd _ | GHole _ | GSort _ | GLetIn _), _ -> false @@ -259,6 +261,7 @@ let notation_constr_and_vars_of_glob_constr a = and aux' = function | GVar (_,id) -> add_id found id; NVar id | GApp (_,g,args) -> NApp (aux g, List.map aux args) + | GProj (_,p,c) -> NProj (p, aux c) | GLambda (_,na,bk,ty,c) -> add_name found na; NLambda (na,aux ty,aux c) | GProd (_,na,bk,ty,c) -> add_name found na; NProd (na,aux ty,aux c) | GLetIn (_,na,b,c) -> add_name found na; NLetIn (na,aux b,aux c) @@ -288,7 +291,7 @@ let notation_constr_and_vars_of_glob_constr a = | GCast (_,c,k) -> NCast (aux c,Miscops.map_cast_type aux k) | GSort (_,s) -> NSort s | GHole (_,w,arg) -> NHole (w, arg) - | GRef (_,r) -> NRef r + | GRef (_,r,_) -> NRef r | GPatVar (_,(_,n)) -> NPatVar n | GEvar _ -> error "Existential variables not allowed in notations." @@ -365,7 +368,7 @@ let rec subst_pat subst pat = match pat with | PatVar _ -> pat | PatCstr (loc,((kn,i),j),cpl,n) -> - let kn' = subst_ind subst kn + let kn' = subst_mind subst kn and cpl' = List.smartmap (subst_pat subst) cpl in if kn' == kn && cpl' == cpl then pat else PatCstr (loc,((kn',i),j),cpl',n) @@ -385,6 +388,12 @@ let rec subst_notation_constr subst bound raw = if r' == r && rl' == rl then raw else NApp(r',rl') + | NProj (p,c) -> + let p' = subst_constant subst p in + let c' = subst_notation_constr subst bound c in + if p == p' && c == c' then raw else + NProj (p',c') + | NList (id1,id2,r1,r2,b) -> let r1' = subst_notation_constr subst bound r1 and r2' = subst_notation_constr subst bound r2 in @@ -421,7 +430,7 @@ let rec subst_notation_constr subst bound raw = (fun (a,(n,signopt) as x) -> let a' = subst_notation_constr subst bound a in let signopt' = Option.map (fun ((indkn,i),nal as z) -> - let indkn' = subst_ind subst indkn in + let indkn' = subst_mind subst indkn in if indkn == indkn' then z else ((indkn',i),nal)) signopt in if a' == a && signopt' == signopt then x else (a',(n,signopt'))) rl @@ -658,7 +667,7 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 = (* Matching compositionally *) | GVar (_,id1), NVar id2 when alpha_var id1 id2 alp -> sigma - | GRef (_,r1), NRef r2 when (eq_gr r1 r2) -> sigma + | GRef (_,r1,_), NRef r2 when (eq_gr r1 r2) -> sigma | GPatVar (_,(_,n1)), NPatVar n2 when Id.equal n1 n2 -> sigma | GApp (loc,f1,l1), NApp (f2,l2) -> let n1 = List.length l1 and n2 = List.length l2 in diff --git a/interp/topconstr.ml b/interp/topconstr.ml index cea5060597..b043f3d423 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -101,7 +101,7 @@ let rec fold_local_binders g f n acc b = function f n acc b let fold_constr_expr_with_binders g f n acc = function - | CAppExpl (loc,(_,_),l) -> List.fold_left (f n) acc l + | CAppExpl (loc,(_,_,_),l) -> List.fold_left (f n) acc l | CApp (loc,(_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l) | CProdN (_,l,b) | CLambdaN (_,l,b) -> fold_constr_expr_binders g f n acc b l | CLetIn (_,na,a,b) -> fold_constr_expr_binders g f n acc b [[na],default_binder_kind,a] @@ -141,7 +141,7 @@ let fold_constr_expr_with_binders g f n acc = function let free_vars_of_constr_expr c = let rec aux bdvars l = function - | CRef (Ident (_,id)) -> if Id.List.mem id bdvars then l else Id.Set.add id l + | CRef (Ident (_,id),_) -> if Id.List.mem id bdvars then l else Id.Set.add id l | c -> fold_constr_expr_with_binders (fun a l -> a::l) aux bdvars l c in aux [] Id.Set.empty c @@ -250,8 +250,8 @@ let map_constr_expr_with_binders g f e = function (* Used in constrintern *) let rec replace_vars_constr_expr l = function - | CRef (Ident (loc,id)) as x -> - (try CRef (Ident (loc,Id.Map.find id l)) with Not_found -> x) + | CRef (Ident (loc,id),us) as x -> + (try CRef (Ident (loc,Id.Map.find id l),us) with Not_found -> x) | c -> map_constr_expr_with_binders Id.Map.remove replace_vars_constr_expr l c |