diff options
91 files changed, 873 insertions, 1027 deletions
diff --git a/dev/core.dbg b/dev/core.dbg index f04e5c07b..6acdd0152 100644 --- a/dev/core.dbg +++ b/dev/core.dbg @@ -3,6 +3,7 @@ load_printer threads.cma load_printer str.cma load_printer clib.cma load_printer lib.cma +load_printer dynlink.cma load_printer kernel.cma load_printer library.cma load_printer engine.cma diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 03742fb8a..af077bbb4 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -33,6 +33,17 @@ The following type aliases where removed The module Constrarg was merged into Stdarg. +The following types have been moved and modified: + + local_binder -> local_binder_expr + glob_binder merged with glob_decl + +The following constructors have been renamed: + + LocalRawDef -> CLocalDef + LocalRawAssum -> CLocalAssum + LocalPattern -> CLocalPattern + ** Ltac API ** Many Ltac specific API has been moved in its own ltac/ folder. Amongst other diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 4a1d688f5..45b5a1007 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -358,7 +358,7 @@ object(self) | Good evs -> proof#set_goals goals; proof#set_evars evs; - proof#refresh (); + proof#refresh ~force:true; Coq.return () ) ) diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml index 6fbed38fb..e787e48bf 100644 --- a/ide/texmacspp.ml +++ b/ide/texmacspp.ml @@ -15,6 +15,7 @@ open Bigint open Decl_kinds open Extend open Libnames +open Constrexpr_ops let unlock loc = let start, stop = Loc.unloc loc in @@ -228,14 +229,15 @@ and pp_decl_notation ((_, s), ce, sc) = (* don't know what it is for now *) Element ("decl_notation", ["name", s], [pp_expr ce]) and pp_local_binder lb = (* don't know what it is for now *) match lb with - | LocalRawDef ((_, nam), ce) -> + | CLocalDef ((loc, nam), ce, ty) -> let attrs = ["name", string_of_name nam] in - pp_expr ~attr:attrs ce - | LocalRawAssum (namll, _, ce) -> + let value = match ty with Some t -> CCast (Loc.merge (constr_loc ce) (constr_loc t),ce, CastConv t) | None -> ce in + pp_expr ~attr:attrs value + | CLocalAssum (namll, _, ce) -> let ppl = List.map (fun (loc, nam) -> (xmlCst (string_of_name nam) loc)) namll in xmlTyped (ppl @ [pp_expr ce]) - | LocalPattern _ -> + | CLocalPattern _ -> assert false and pp_local_decl_expr lde = (* don't know what it is for now *) match lde with @@ -465,7 +467,8 @@ and pp_expr ?(attr=[]) e = [Element ("scrutinees", [], List.map pp_case_expr cel)] @ [pp_branch_expr_list bel])) | CRecord (_, _) -> assert false - | CLetIn (loc, (varloc, var), value, body) -> + | CLetIn (loc, (varloc, var), value, typ, body) -> + let value = match typ with Some t -> CCast (Loc.merge (constr_loc value) (constr_loc t),value, CastConv t) | None -> value in xmlApply loc (xmlOperator "let" loc :: [xmlCst (string_of_name var) varloc; pp_expr value; pp_expr body]) diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index b5405570c..3cbe58388 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -14,7 +14,7 @@ class type proof_view = object inherit GObj.widget method buffer : GText.buffer - method refresh : unit -> unit + method refresh : force:bool -> unit method clear : unit -> unit method set_goals : Interface.goals option -> unit method set_evars : Interface.evar list option -> unit @@ -197,6 +197,7 @@ let proof_view () = inherit GObj.widget view#as_widget val mutable goals = None val mutable evars = None + val mutable last_width = -1 method buffer = text_buffer @@ -206,13 +207,24 @@ let proof_view () = method set_evars evs = evars <- evs - method refresh () = - let dummy _ () = () in - display (mode_tactic dummy) view goals None evars + method refresh ~force = + (* We need to block updates here due to the following race: + insertion of messages may create a vertical scrollbar, this + will trigger a width change, calling refresh again and + going into an infinite loop. *) + let width = Ideutils.textview_width view in + (* Could still this method race if the scrollbar changes the + textview_width ?? *) + let needed = force || last_width <> width in + if needed then begin + last_width <- width; + let dummy _ () = () in + display (mode_tactic dummy) view goals None evars + end end in (* Is there a better way to connect the signal ? *) (* Can this be done in the object constructor? *) - let w_cb _ = pf#refresh () in + let w_cb _ = pf#refresh ~force:false in ignore (view#misc#connect#size_allocate w_cb); pf diff --git a/ide/wg_ProofView.mli b/ide/wg_ProofView.mli index aa01d955d..a90d429d0 100644 --- a/ide/wg_ProofView.mli +++ b/ide/wg_ProofView.mli @@ -10,7 +10,7 @@ class type proof_view = object inherit GObj.widget method buffer : GText.buffer - method refresh : unit -> unit + method refresh : force:bool -> unit method clear : unit -> unit method set_goals : Interface.goals option -> unit method set_evars : Interface.evar list option -> unit diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index 5f80d6897..d7950e5fd 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -111,7 +111,7 @@ let to_box = let open Pp in ) let rec of_pp (pp : Pp.std_ppcmds) = let open Pp in match Pp.repr pp with - | Ppcmd_empty -> constructor "ppdoc" "emtpy" [] + | Ppcmd_empty -> constructor "ppdoc" "empty" [] | Ppcmd_string s -> constructor "ppdoc" "string" [of_string s] | Ppcmd_glue sl -> constructor "ppdoc" "glue" [of_list of_pp sl] | Ppcmd_box (bt,s) -> constructor "ppdoc" "box" [of_pair of_box of_pp (bt,s)] diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 59c24900d..53c97f6b6 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -37,10 +37,10 @@ let binder_kind_eq b1 b2 = match b1, b2 with let default_binder_kind = Default Explicit let names_of_local_assums bl = - List.flatten (List.map (function LocalRawAssum(l,_,_)->l|_->[]) bl) + List.flatten (List.map (function CLocalAssum(l,_,_)->l|_->[]) bl) let names_of_local_binders bl = - List.flatten (List.map (function LocalRawAssum(l,_,_)->l|LocalRawDef(l,_)->[l]|LocalPattern _ -> assert false) bl) + List.flatten (List.map (function CLocalAssum(l,_,_)->l|CLocalDef(l,_,_)->[l]|CLocalPattern _ -> assert false) bl) (**********************************************************************) (* Functions on constr_expr *) @@ -113,9 +113,10 @@ let rec constr_expr_eq e1 e2 = | CLambdaN(_,bl1,a1), CLambdaN(_,bl2,a2) -> List.equal binder_expr_eq bl1 bl2 && constr_expr_eq a1 a2 - | CLetIn(_,(_,na1),a1,b1), CLetIn(_,(_,na2),a2,b2) -> + | CLetIn(_,(_,na1),a1,t1,b1), CLetIn(_,(_,na2),a2,t2,b2) -> Name.equal na1 na2 && constr_expr_eq a1 a2 && + Option.equal constr_expr_eq t1 t2 && constr_expr_eq b1 b2 | CAppExpl(_,(proj1,r1,_),al1), CAppExpl(_,(proj2,r2,_),al2) -> Option.equal Int.equal proj1 proj2 && @@ -212,9 +213,9 @@ and recursion_order_expr_eq r1 r2 = match r1, r2 with | _ -> false and local_binder_eq l1 l2 = match l1, l2 with -| LocalRawDef (n1, e1), LocalRawDef (n2, e2) -> - eq_located Name.equal n1 n2 && constr_expr_eq e1 e2 -| LocalRawAssum (n1, _, e1), LocalRawAssum (n2, _, e2) -> +| CLocalDef (n1, e1, t1), CLocalDef (n2, e2, t2) -> + eq_located Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2 +| CLocalAssum (n1, _, e1), CLocalAssum (n2, _, e2) -> (** Don't care about the [binder_kind] *) List.equal (eq_located Name.equal) n1 n2 && constr_expr_eq e1 e2 | _ -> false @@ -234,7 +235,7 @@ let constr_loc = function | CCoFix (loc,_,_) -> loc | CProdN (loc,_,_) -> loc | CLambdaN (loc,_,_) -> loc - | CLetIn (loc,_,_,_) -> loc + | CLetIn (loc,_,_,_,_) -> loc | CAppExpl (loc,_,_) -> loc | CApp (loc,_,_) -> loc | CRecord (loc,_) -> loc @@ -269,10 +270,11 @@ let raw_cases_pattern_expr_loc = function | RCPatOr (loc,_) -> loc let local_binder_loc = function - | LocalRawAssum ((loc,_)::_,_,t) - | LocalRawDef ((loc,_),t) -> Loc.merge loc (constr_loc t) - | LocalRawAssum ([],_,_) -> assert false - | LocalPattern (loc,_,_) -> loc + | CLocalAssum ((loc,_)::_,_,t) + | CLocalDef ((loc,_),t,None) -> Loc.merge loc (constr_loc t) + | CLocalDef ((loc,_),b,Some t) -> Loc.merge loc (Loc.merge (constr_loc b) (constr_loc t)) + | CLocalAssum ([],_,_) -> assert false + | CLocalPattern (loc,_,_) -> loc let local_binders_loc bll = match bll with | [] -> Loc.ghost @@ -285,7 +287,7 @@ 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) +let mkLetInC (id,a,t,b) = CLetIn (Loc.ghost,id,a,t,b) let mkProdC (idl,bk,a,b) = CProdN (Loc.ghost,[idl,bk,a],b) let mkAppC (f,l) = @@ -308,17 +310,17 @@ let expand_pattern_binders mkC bl c = | b :: bl -> let (env, bl, c) = loop bl c in match b with - | LocalRawDef (n, _) -> + | CLocalDef (n, _, _) -> let env = add_name_in_env env n in (env, b :: bl, c) - | LocalRawAssum (nl, _, _) -> + | CLocalAssum (nl, _, _) -> let env = List.fold_left add_name_in_env env nl in (env, b :: bl, c) - | LocalPattern (loc, p, ty) -> + | CLocalPattern (loc, p, ty) -> let ni = Hook.get fresh_var env c in let id = (loc, Name ni) in let b = - LocalRawAssum + CLocalAssum ([id], Default Explicit, match ty with | Some ty -> ty @@ -338,13 +340,13 @@ let expand_pattern_binders mkC bl c = let mkCProdN loc bll c = let rec loop loc bll c = match bll with - | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll -> + | CLocalAssum ((loc1,_)::_ as idl,bk,t) :: bll -> CProdN (loc,[idl,bk,t],loop (Loc.merge loc1 loc) bll c) - | LocalRawDef ((loc1,_) as id,b) :: bll -> - CLetIn (loc,id,b,loop (Loc.merge loc1 loc) bll c) + | CLocalDef ((loc1,_) as id,b,t) :: bll -> + CLetIn (loc,id,b,t,loop (Loc.merge loc1 loc) bll c) | [] -> c - | LocalRawAssum ([],_,_) :: bll -> loop loc bll c - | LocalPattern (loc,p,ty) :: bll -> assert false + | CLocalAssum ([],_,_) :: bll -> loop loc bll c + | CLocalPattern (loc,p,ty) :: bll -> assert false in let (bll, c) = expand_pattern_binders loop bll c in loop loc bll c @@ -352,32 +354,32 @@ let mkCProdN loc bll c = let mkCLambdaN loc bll c = let rec loop loc bll c = match bll with - | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll -> + | CLocalAssum ((loc1,_)::_ as idl,bk,t) :: bll -> CLambdaN (loc,[idl,bk,t],loop (Loc.merge loc1 loc) bll c) - | LocalRawDef ((loc1,_) as id,b) :: bll -> - CLetIn (loc,id,b,loop (Loc.merge loc1 loc) bll c) + | CLocalDef ((loc1,_) as id,b,t) :: bll -> + CLetIn (loc,id,b,t,loop (Loc.merge loc1 loc) bll c) | [] -> c - | LocalRawAssum ([],_,_) :: bll -> loop loc bll c - | LocalPattern (loc,p,ty) :: bll -> assert false + | CLocalAssum ([],_,_) :: bll -> loop loc bll c + | CLocalPattern (loc,p,ty) :: bll -> assert false in let (bll, c) = expand_pattern_binders loop bll c in loop loc bll c let rec abstract_constr_expr c = function | [] -> c - | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl) - | LocalRawAssum (idl,bk,t)::bl -> + | CLocalDef (x,b,t)::bl -> mkLetInC(x,b,t,abstract_constr_expr c bl) + | CLocalAssum (idl,bk,t)::bl -> List.fold_right (fun x b -> mkLambdaC([x],bk,t,b)) idl (abstract_constr_expr c bl) - | LocalPattern _::_ -> assert false + | CLocalPattern _::_ -> assert false let rec prod_constr_expr c = function | [] -> c - | LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_constr_expr c bl) - | LocalRawAssum (idl,bk,t)::bl -> + | CLocalDef (x,b,t)::bl -> mkLetInC(x,b,t,prod_constr_expr c bl) + | CLocalAssum (idl,bk,t)::bl -> List.fold_right (fun x b -> mkProdC([x],bk,t,b)) idl (prod_constr_expr c bl) - | LocalPattern _::_ -> assert false + | CLocalPattern _::_ -> assert false let coerce_reference_to_id = function | Ident (_,id) -> id diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index a92da035f..45e3a19bc 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -23,8 +23,8 @@ val constr_expr_eq : constr_expr -> constr_expr -> bool (** Equality on [constr_expr]. This is a syntactical one, which is oblivious to some parsing details, including locations. *) -val local_binder_eq : local_binder -> local_binder -> bool -(** Equality on [local_binder]. Same properties as [constr_expr_eq]. *) +val local_binder_eq : local_binder_expr -> local_binder_expr -> bool +(** Equality on [local_binder_expr]. Same properties as [constr_expr_eq]. *) val binding_kind_eq : Decl_kinds.binding_kind -> Decl_kinds.binding_kind -> bool (** Equality on [binding_kind] *) @@ -37,7 +37,7 @@ val binder_kind_eq : binder_kind -> binder_kind -> bool val constr_loc : constr_expr -> Loc.t val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t val raw_cases_pattern_expr_loc : raw_cases_pattern_expr -> Loc.t -val local_binders_loc : local_binder list -> Loc.t +val local_binders_loc : local_binder_expr list -> Loc.t (** {6 Constructors}*) @@ -46,22 +46,22 @@ val mkRefC : reference -> constr_expr val mkAppC : constr_expr * constr_expr list -> constr_expr val mkCastC : constr_expr * constr_expr cast_type -> constr_expr val mkLambdaC : Name.t located list * binder_kind * constr_expr * constr_expr -> constr_expr -val mkLetInC : Name.t located * constr_expr * constr_expr -> constr_expr +val mkLetInC : Name.t located * constr_expr * constr_expr option * constr_expr -> constr_expr val mkProdC : Name.t located list * binder_kind * constr_expr * constr_expr -> constr_expr -val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr -val prod_constr_expr : constr_expr -> local_binder list -> constr_expr +val abstract_constr_expr : constr_expr -> local_binder_expr list -> constr_expr +val prod_constr_expr : constr_expr -> local_binder_expr list -> constr_expr -val mkCLambdaN : Loc.t -> local_binder list -> constr_expr -> constr_expr +val mkCLambdaN : Loc.t -> local_binder_expr list -> constr_expr -> constr_expr (** Same as [abstract_constr_expr], with location *) -val mkCProdN : Loc.t -> local_binder list -> constr_expr -> constr_expr +val mkCProdN : Loc.t -> local_binder_expr list -> constr_expr -> constr_expr (** Same as [prod_constr_expr], with location *) val fresh_var_hook : (Names.Id.t list -> Constrexpr.constr_expr -> Names.Id.t) Hook.t val expand_pattern_binders : - (Loc.t -> local_binder list -> constr_expr -> constr_expr) -> - local_binder list -> constr_expr -> local_binder list * constr_expr + (Loc.t -> local_binder_expr list -> constr_expr -> constr_expr) -> + local_binder_expr list -> constr_expr -> local_binder_expr list * constr_expr (** {6 Destructors}*) @@ -78,9 +78,9 @@ val coerce_to_name : constr_expr -> Name.t located val default_binder_kind : binder_kind -val names_of_local_binders : local_binder list -> Name.t located list +val names_of_local_binders : local_binder_expr list -> Name.t located list (** Retrieve a list of binding names from a list of binders. *) -val names_of_local_assums : local_binder list -> Name.t located list -(** Same as [names_of_local_binders], but does not take the [let] bindings into +val names_of_local_assums : local_binder_expr list -> Name.t located list +(** Same as [names_of_local_binder_exprs], but does not take the [let] bindings into account. *) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 8debc06bb..f272d219a 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -598,6 +598,14 @@ let extern_optimal_prim_token scopes r r' = | _ -> raise No_match (**********************************************************************) +(* mapping decl *) + +let extended_glob_local_binder_of_decl loc = function + | (p,bk,None,t) -> GLocalAssum (loc,p,bk,t) + | (p,bk,Some x,GHole (_, _, Misctypes.IntroAnonymous, None)) -> GLocalDef (loc,p,bk,x,None) + | (p,bk,Some x,t) -> GLocalDef (loc,p,bk,x,Some t) + +(**********************************************************************) (* mapping glob_constr to constr_expr *) let extern_glob_sort = function @@ -692,8 +700,9 @@ let rec extern inctx scopes vars r = explicitize loc inctx [] (None,sub_extern false scopes vars f) (List.map (fun c -> lazy (sub_extern true scopes vars c)) args)) - | GLetIn (loc,na,t,c) -> - CLetIn (loc,(loc,na),sub_extern false scopes vars t, + | GLetIn (loc,na,b,t,c) -> + CLetIn (loc,(loc,na),sub_extern false scopes vars b, + Option.map (extern_typ scopes vars) t, extern inctx scopes (add_vname vars na) c) | GProd (loc,na,bk,t,c) -> @@ -756,7 +765,7 @@ let rec extern inctx scopes vars r = let listdecl = Array.mapi (fun i fi -> let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in - let bl = List.map (fun (p,bk,x,t) -> (Inl p,bk,x,t)) bl in + let bl = List.map (extended_glob_local_binder_of_decl loc) bl in let (assums,ids,bl) = extern_local_binder scopes vars bl in let vars0 = List.fold_right (name_fold Id.Set.add) ids vars in let vars1 = List.fold_right (name_fold Id.Set.add) ids vars' in @@ -773,7 +782,7 @@ let rec extern inctx scopes vars r = | GCoFix n -> let listdecl = Array.mapi (fun i fi -> - let bl = List.map (fun (p,bk,x,t) -> (Inl p,bk,x,t)) blv.(i) in + let bl = List.map (extended_glob_local_binder_of_decl loc) blv.(i) in let (_,ids,bl) = extern_local_binder scopes vars bl in let vars0 = List.fold_right (name_fold Id.Set.add) ids vars in let vars1 = List.fold_right (name_fold Id.Set.add) ids vars' in @@ -817,33 +826,32 @@ and factorize_lambda inctx scopes vars na bk aty c = and extern_local_binder scopes vars = function [] -> ([],[],[]) - | (Inl na,bk,Some bd,ty)::l -> + | GLocalDef (_,na,bk,bd,ty)::l -> let (assums,ids,l) = extern_local_binder scopes (name_fold Id.Set.add na vars) l in (assums,na::ids, - LocalRawDef((Loc.ghost,na), extern false scopes vars bd) :: l) + CLocalDef((Loc.ghost,na), extern false scopes vars bd, + Option.map (extern false scopes vars) ty) :: l) - | (Inl na,bk,None,ty)::l -> + | GLocalAssum (_,na,bk,ty)::l -> let ty = extern_typ scopes vars ty in (match extern_local_binder scopes (name_fold Id.Set.add na vars) l with - (assums,ids,LocalRawAssum(nal,k,ty')::l) + (assums,ids,CLocalAssum(nal,k,ty')::l) when constr_expr_eq ty ty' && match na with Name id -> not (occur_var_constr_expr id ty') | _ -> true -> (na::assums,na::ids, - LocalRawAssum((Loc.ghost,na)::nal,k,ty')::l) + CLocalAssum((Loc.ghost,na)::nal,k,ty')::l) | (assums,ids,l) -> (na::assums,na::ids, - LocalRawAssum([(Loc.ghost,na)],Default bk,ty) :: l)) - - | (Inr p,bk,Some bd,ty)::l -> assert false + CLocalAssum([(Loc.ghost,na)],Default bk,ty) :: l)) - | (Inr p,bk,None,ty)::l -> + | GLocalPattern (_,(p,_),_,bk,ty)::l -> let ty = if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in let p = extern_cases_pattern vars p in let (assums,ids,l) = extern_local_binder scopes vars l in - (assums,ids, LocalPattern(Loc.ghost,p,ty) :: l) + (assums,ids, CLocalPattern(Loc.ghost,p,ty) :: l) and extern_eqn inctx scopes vars (loc,ids,pl,c) = (loc,[loc,List.map (extern_cases_pattern_in_scope scopes vars) pl], @@ -1017,8 +1025,9 @@ let rec glob_of_pat env sigma = function List.map (glob_of_pat env sigma) args) | PProd (na,t,c) -> GProd (loc,na,Explicit,glob_of_pat env sigma t,glob_of_pat (na::env) sigma c) - | PLetIn (na,t,c) -> - GLetIn (loc,na,glob_of_pat env sigma t, glob_of_pat (na::env) sigma c) + | PLetIn (na,b,t,c) -> + GLetIn (loc,na,glob_of_pat env sigma b, Option.map (glob_of_pat env sigma) t, + glob_of_pat (na::env) sigma c) | PLambda (na,t,c) -> GLambda (loc,na,Explicit,glob_of_pat env sigma t, glob_of_pat (na::env) sigma c) | PIf (c,b1,b2) -> @@ -1056,5 +1065,5 @@ let extern_rel_context where env sigma sign = let where = Option.map EConstr.of_constr where in let a = detype_rel_context where [] (names_of_rel_context env,env) sigma sign in let vars = vars_of_env env in - let a = List.map (fun (p,bk,x,t) -> (Inl p,bk,x,t)) a in + let a = List.map (extended_glob_local_binder_of_decl Loc.ghost) a in pi3 (extern_local_binder (None,[]) vars a) diff --git a/interp/constrextern.mli b/interp/constrextern.mli index f617faa38..b39339450 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -41,7 +41,7 @@ val extern_reference : Loc.t -> Id.Set.t -> global_reference -> reference val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr val extern_sort : Evd.evar_map -> sorts -> glob_sort val extern_rel_context : constr option -> env -> Evd.evar_map -> - Context.Rel.t -> local_binder list + Context.Rel.t -> local_binder_expr list (** Printing options *) val print_implicits : bool ref diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8fee191af..d75487ecf 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -65,8 +65,6 @@ type var_internalization_data = type internalization_env = (var_internalization_data) Id.Map.t -type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr) - type ltac_sign = { ltac_vars : Id.Set.t; ltac_bound : Id.Set.t; @@ -306,12 +304,12 @@ let reset_tmp_scope env = {env with tmp_scope = None} let rec it_mkGProd loc2 env body = match env with - (loc1, (na, bk, _, t)) :: tl -> it_mkGProd loc2 tl (GProd (Loc.merge loc1 loc2, na, bk, t, body)) + (loc1, (na, bk, t)) :: tl -> it_mkGProd loc2 tl (GProd (Loc.merge loc1 loc2, na, bk, t, body)) | [] -> body let rec it_mkGLambda loc2 env body = match env with - (loc1, (na, bk, _, t)) :: tl -> it_mkGLambda loc2 tl (GLambda (Loc.merge loc1 loc2, na, bk, t, body)) + (loc1, (na, bk, t)) :: tl -> it_mkGLambda loc2 tl (GLambda (Loc.merge loc1 loc2, na, bk, t, body)) | [] -> body (**********************************************************************) @@ -399,7 +397,7 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar env fvs in let bl = List.map (fun (id, loc) -> - (loc, (Name id, b, None, GHole (loc, Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None)))) + (loc, (Name id, b, GHole (loc, Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None)))) fvs in let na = match na with @@ -414,7 +412,7 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar in Implicit_quantifiers.make_fresh ids' (Global.env ()) id in Name name | _ -> na - in (push_name_env ~global_level lvar (impls_type_list ty')(*?*) env' (loc,na)), (loc,(na,b',None,ty')) :: List.rev bl + in (push_name_env ~global_level lvar (impls_type_list ty')(*?*) env' (loc,na)), (loc,(na,b',ty')) :: List.rev bl let intern_assumption intern lvar env nal bk ty = let intern_type env = intern (set_type_scope env) in @@ -426,7 +424,7 @@ let intern_assumption intern lvar env nal bk ty = List.fold_left (fun (env, bl) (loc, na as locna) -> (push_name_env lvar impls env locna, - (loc,(na,k,None,locate_if_hole loc na ty))::bl)) + (loc,(na,k,locate_if_hole loc na ty))::bl)) (env, []) nal | Generalized (b,b',t) -> let env, b = intern_generalized_binder intern_type lvar env (List.hd nal) b b' t ty in @@ -457,47 +455,47 @@ let intern_local_pattern intern lvar env p = env) env (free_vars_of_pat [] p) -type binder_data = - | BDRawDef of (Loc.t * glob_binder) - | BDPattern of - (Loc.t * (cases_pattern * Id.t list) * - (bool ref * - (Notation_term.tmp_scope_name option * - Notation_term.tmp_scope_name list) - option ref * Notation_term.notation_var_internalization_type) - Names.Id.Map.t * - intern_env * constr_expr) +let glob_local_binder_of_extended = function + | GLocalAssum (loc,na,bk,t) -> (na,bk,None,t) + | GLocalDef (loc,na,bk,c,Some t) -> (na,bk,Some c,t) + | GLocalDef (loc,na,bk,c,None) -> + let t = GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) in + (na,bk,Some c,t) + | GLocalPattern (loc,_,_,_,_) -> + Loc.raise ~loc (Stream.Error "pattern with quote not allowed here.") let intern_cases_pattern_fwd = ref (fun _ -> failwith "intern_cases_pattern_fwd") let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = function - | LocalRawAssum(nal,bk,ty) -> + | CLocalAssum(nal,bk,ty) -> let env, bl' = intern_assumption intern lvar env nal bk ty in - let bl' = List.map (fun a -> BDRawDef a) bl' in + let bl' = List.map (fun (loc,(na,c,t)) -> GLocalAssum (loc,na,c,t)) bl' in env, bl' @ bl - | LocalRawDef((loc,na as locna),def) -> - let indef = intern env def in - let term, ty = - match indef with - | GCast (loc, b, Misctypes.CastConv t) -> b, t - | _ -> indef, GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) - in - (push_name_env lvar (impls_term_list indef) env locna, - (BDRawDef ((loc,(na,Explicit,Some(term),ty))))::bl) - | LocalPattern (loc,p,ty) -> + | CLocalDef((loc,na as locna),def,ty) -> + let term = intern env def in + let ty = Option.map (intern env) ty in + (push_name_env lvar (impls_term_list term) env locna, + GLocalDef (loc,na,Explicit,term,ty) :: bl) + | CLocalPattern (loc,p,ty) -> let tyc = match ty with | Some ty -> ty | None -> CHole(loc,None,Misctypes.IntroAnonymous,None) in let env = intern_local_pattern intern lvar env p in + let il = List.map snd (free_vars_of_pat [] p) in let cp = match !intern_cases_pattern_fwd (None,env.scopes) p with | (_, [(_, cp)]) -> cp | _ -> assert false in - let il = List.map snd (free_vars_of_pat [] p) in - (env, BDPattern(loc,(cp,il),lvar,env,tyc) :: bl) + let ienv = Id.Set.elements env.ids in + let id = Namegen.next_ident_away (Id.of_string "pat") ienv in + let na = (loc, Name id) in + let bk = Default Explicit in + let _, bl' = intern_assumption intern lvar env [na] bk tyc in + let _,(_,bk,t) = List.hd bl' in + (env, GLocalPattern(loc,(cp,il),id,bk,t) :: bl) let intern_generalization intern env lvar loc bk ak c = let c = intern {env with unb = true} c in @@ -567,35 +565,29 @@ let traverse_binder (terms,_,_ as subst) avoid (renaming,env) = function (renaming',env), Name id' type letin_param = - | LPLetIn of Loc.t * (Name.t * glob_constr) + | LPLetIn of Loc.t * (Name.t * glob_constr * glob_constr option) | LPCases of Loc.t * (cases_pattern * Id.t list) * Id.t let make_letins = List.fold_right (fun a c -> match a with - | LPLetIn (loc,(na,b)) -> - GLetIn(loc,na,b,c) + | LPLetIn (loc,(na,b,t)) -> + GLetIn(loc,na,b,t,c) | LPCases (loc,(cp,il),id) -> let tt = (GVar(loc,id),(Name id,None)) in GCases(loc,Misctypes.LetPatternStyle,None,[tt],[(loc,il,[cp],c)])) -let rec subordinate_letins intern letins = function +let rec subordinate_letins letins = function (* binders come in reverse order; the non-let are returned in reverse order together *) (* with the subordinated let-in in writing order *) - | BDRawDef (loc,(na,_,Some b,t))::l -> - subordinate_letins intern (LPLetIn (loc,(na,b))::letins) l - | BDRawDef (loc,(na,bk,None,t))::l -> - let letins',rest = subordinate_letins intern [] l in + | GLocalDef (loc,na,_,b,t)::l -> + subordinate_letins (LPLetIn (loc,(na,b,t))::letins) l + | GLocalAssum (loc,na,bk,t)::l -> + let letins',rest = subordinate_letins [] l in letins',((loc,(na,bk,t)),letins)::rest - | BDPattern (loc,u,lvar,env,tyc) :: l -> - let ienv = Id.Set.elements env.ids in - let id = Namegen.next_ident_away (Id.of_string "pat") ienv in - let na = (loc, Name id) in - let bk = Default Explicit in - let _, bl' = intern_assumption intern lvar env [na] bk tyc in - let bl' = List.map (fun a -> BDRawDef a) bl' in - subordinate_letins intern (LPCases (loc,u,id)::letins) (bl'@ l) + | GLocalPattern (loc,u,id,bk,t) :: l -> + subordinate_letins (LPCases (loc,u,id)::letins) ([GLocalAssum (loc,Name id,bk,t)] @ l) | [] -> letins,[] @@ -609,10 +601,11 @@ let terms_of_binders bl = let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in CAppExpl (loc,(None,r,None),params @ List.map term_of_pat l) in let rec extract_variables = function - | BDRawDef (loc,(Name id,_,None,_))::l -> CRef (Ident (loc,id), None) :: extract_variables l - | BDRawDef (loc,(Name id,_,Some _,_))::l -> extract_variables l - | BDRawDef (loc,(Anonymous,_,_,_))::l -> error "Cannot turn \"_\" into a term." - | BDPattern (loc,(u,_),lvar,env,tyc) :: l -> term_of_pat u :: extract_variables l + | GLocalAssum (loc,Name id,_,_)::l -> CRef (Ident (loc,id), None) :: extract_variables l + | GLocalDef (loc,Name id,_,_,_)::l -> extract_variables l + | GLocalDef (loc,Anonymous,_,_,_)::l + | GLocalAssum (loc,Anonymous,_,_)::l -> error "Cannot turn \"_\" into a term." + | GLocalPattern (loc,(u,_),_,_,_) :: l -> term_of_pat u :: extract_variables l | [] -> [] in extract_variables bl @@ -674,7 +667,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = (* All elements of the list are in scopes (scopt,subscopes) *) let (bl,(scopt,subscopes)) = Id.Map.find x binders in let env,bl = List.fold_left (intern_local_binder_aux intern ntnvars) (env,[]) bl in - let letins,bl = subordinate_letins intern [] bl in + let letins,bl = subordinate_letins [] bl in let termin = aux (terms,None,None) (renaming,env) terminator in let res = List.fold_left (fun t binder -> aux (terms,Some(y,binder),Some t) subinfos iter) @@ -1545,10 +1538,8 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = 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 rbefore = List.map (function BDRawDef a -> a | BDPattern _ -> assert false) rbefore in let ro = f (intern env') in - let n' = Option.map (fun _ -> List.count (fun (_,(_,_,b,_)) -> (* remove let-ins *) b = None) rbefore) n in - let rbefore = List.map (fun a -> BDRawDef a) rbefore in + let n' = Option.map (fun _ -> List.count (function 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) = @@ -1560,24 +1551,19 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = | CMeasureRec (m,r) -> intern_ro_arg (fun f -> GMeasureRec (f m, Option.map f r)) in - let bl = - List.rev_map - (function - | BDRawDef a -> a - | BDPattern (loc,_,_,_,_) -> - Loc.raise ~loc (Stream.Error "pattern with quote not allowed after fix")) rbl in - ((n, ro), bl, intern_type env' ty, env')) dl in + let bl = List.rev (List.map glob_local_binder_of_extended rbl) in + ((n, ro), 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 + 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 (Loc.ghost, Name name)) 0 env' lf in (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in GRec (loc,GFix (Array.map (fun (ro,_,_,_) -> ro) idl,n), Array.of_list lf, - Array.map (fun (_,bl,_,_) -> List.map snd bl) idl, + Array.map (fun (_,bl,_,_) -> bl) idl, Array.map (fun (_,_,ty,_) -> ty) idl, Array.map (fun (_,_,_,bd) -> bd) idl) | CCoFix (loc, (locid,iddef), dl) -> @@ -1591,20 +1577,18 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = let idl_tmp = Array.map (fun ((loc,id),bl,ty,_) -> let (env',rbl) = List.fold_left intern_local_binder (env,[]) bl in - let rbl = List.map (function BDRawDef a -> a | BDPattern _ -> - Loc.raise ~loc (Stream.Error "pattern with quote not allowed after cofix")) rbl in - (List.rev rbl, + (List.rev (List.map glob_local_binder_of_extended rbl), intern_type env' ty,env')) dl in let idl = Array.map2 (fun (_,_,_,bd) (b,c,env') -> let env'' = List.fold_left_i (fun i en name -> let (bli,tyi,_) = idl_tmp.(i) in - let cofix_args = List.map (fun (_, (na, bk, _, _)) -> (build_impls bk na)) bli in + let cofix_args = List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli in push_name_env ntnvars (impls_type_list ~args:cofix_args tyi) en (Loc.ghost, Name name)) 0 env' lf in (b,c,intern {env'' with tmp_scope = None} bd)) dl idl_tmp in GRec (loc,GCoFix n, Array.of_list lf, - Array.map (fun (bl,_,_) -> List.map snd bl) idl, + Array.map (fun (bl,_,_) -> bl) idl, Array.map (fun (_,ty,_) -> ty) idl, Array.map (fun (_,_,bd) -> bd) idl) | CProdN (loc,[],c2) -> @@ -1615,9 +1599,10 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = intern env c2 | CLambdaN (loc,(nal,bk,ty)::bll,c2) -> iterate_lam loc (reset_tmp_scope env) bk ty (CLambdaN (loc, bll, c2)) nal - | CLetIn (loc,na,c1,c2) -> + | CLetIn (loc,na,c1,t,c2) -> let inc1 = intern (reset_tmp_scope env) c1 in - GLetIn (loc, snd na, inc1, + let int = Option.map (intern_type env) t in + GLetIn (loc, snd na, inc1, int, intern (push_name_env ntnvars (impls_term_list inc1) env na) c2) | CNotation (loc,"- _",([CPrim (_,Numeral p)],[],[])) when Bigint.is_strictly_pos p -> @@ -2070,18 +2055,11 @@ let intern_context global_level env impl_env binders = let lvar = (empty_ltac_sign, Id.Map.empty) in let lenv, bl = List.fold_left (fun (lenv, bl) b -> - let bl = List.map (fun a -> BDRawDef a) bl in let (env, bl) = intern_local_binder_aux ~global_level (my_intern_constr env lvar) Id.Map.empty (lenv, bl) b in - let bl = - List.map - (function - | BDRawDef a -> a - | BDPattern (loc,_,_,_,_) -> - Loc.raise ~loc (Stream.Error "pattern with quote not allowed here")) bl in (env, bl)) ({ids = extract_ids env; unb = false; tmp_scope = None; scopes = []; impls = impl_env}, []) binders in - (lenv.impls, List.map snd bl) + (lenv.impls, List.map glob_local_binder_of_extended bl) with InternalizationError (loc,e) -> user_err ~loc ~hdr:"internalize" (explain_internalization_error e) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index ae7f511f4..758d4e650 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -75,8 +75,6 @@ type ltac_sign = { val empty_ltac_sign : ltac_sign -type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr) - (** {6 Internalization performs interpretation of global names and notations } *) val intern_constr : env -> constr_expr -> glob_constr @@ -90,7 +88,7 @@ val intern_gen : typing_constraint -> env -> val intern_pattern : env -> cases_pattern_expr -> Id.t list * (Id.t Id.Map.t * cases_pattern) list -val intern_context : bool -> env -> internalization_env -> local_binder list -> internalization_env * glob_binder list +val intern_context : bool -> env -> internalization_env -> local_binder_expr list -> internalization_env * glob_decl list (** {6 Composing internalization with type inference (pretyping) } *) @@ -159,16 +157,16 @@ val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> EConst val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int -> - env -> evar_map ref -> local_binder list -> + env -> evar_map ref -> local_binder_expr list -> internalization_env * ((env * EConstr.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 list -> internalization_env * ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *) +(* 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 list -> *) +(* env -> evar_map -> local_binder_expr list -> *) (* internalization_env * *) (* ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *) diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 77a8ed680..7f11c0a3b 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -102,19 +102,20 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = let ids_of_names l = List.fold_left (fun acc x -> match snd x with Name na -> na :: acc | Anonymous -> acc) [] l -let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder list) = +let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr list) = let rec aux bdvars l c = match c with - ((LocalRawAssum (n, _, c)) :: tl) -> + ((CLocalAssum (n, _, c)) :: tl) -> let bound = ids_of_names n in let l' = free_vars_of_constr_expr c ~bound:bdvars l in aux (Id.Set.union (ids_of_list bound) bdvars) l' tl - | ((LocalRawDef (n, c)) :: tl) -> + | ((CLocalDef (n, c, t)) :: tl) -> let bound = match snd n with Anonymous -> [] | Name n -> [n] in let l' = free_vars_of_constr_expr c ~bound:bdvars l in - aux (Id.Set.union (ids_of_list bound) bdvars) l' tl + let l'' = Option.fold_left (fun l t -> free_vars_of_constr_expr t ~bound:bdvars l) l' t in + aux (Id.Set.union (ids_of_list bound) bdvars) l'' tl - | LocalPattern _ :: tl -> assert false + | CLocalPattern _ :: tl -> assert false | [] -> bdvars, l in aux bound l binders @@ -131,10 +132,15 @@ 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) - | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) | GLetIn (loc,na,ty,c) -> + | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) -> let vs' = vars bound vs ty in let bound' = add_name_to_ids bound na in vars bound' vs' c + | GLetIn (loc,na,b,ty,c) -> + let vs' = vars bound vs b in + let vs'' = Option.fold_left (vars bound) vs' ty in + let bound' = add_name_to_ids bound na in + vars bound' vs'' c | GCases (loc,sty,rtntypopt,tml,pl) -> let vs1 = vars_option bound vs rtntypopt in let vs2 = List.fold_left (fun vs (tm,_) -> vars bound vs tm) vs1 tml in @@ -318,7 +324,7 @@ let implicits_of_glob_constr ?(with_products=true) l = | _ -> () in [] | GLambda (loc, na, bk, t, b) -> abs na bk b - | GLetIn (loc, na, t, b) -> aux i b + | GLetIn (loc, na, b, t, c) -> aux i c | GRec (_, fix_kind, nas, args, tys, bds) -> let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in List.fold_left_i (fun i l (na,bk,_,_) -> add_impl i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb) diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index d0327e506..71009ec3c 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -25,7 +25,7 @@ val free_vars_of_constr_expr : constr_expr -> ?bound:Id.Set.t -> Id.t list -> Id.t list val free_vars_of_binders : - ?bound:Id.Set.t -> Id.t list -> local_binder list -> Id.Set.t * Id.t list + ?bound:Id.Set.t -> Id.t list -> local_binder_expr list -> Id.Set.t * Id.t list (** Returns the generalizable free ids in left-to-right order with the location of their first occurrence *) diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 549e8e787..8b4fadb5a 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -36,7 +36,7 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with on_true_do (f ty1 ty2 && f c1 c2) add na1 | GHole _, GHole _ -> true | GSort (_,s1), GSort (_,s2) -> Miscops.glob_sort_eq s1 s2 - | GLetIn (_,na1,b1,c1), GLetIn (_,na2,b2,c2) when Name.equal na1 na2 -> + | GLetIn (_,na1,b1,t1,c1), GLetIn (_,na2,b2,t2,c2) when Name.equal na1 na2 -> on_true_do (f b1 b2 && f c1 c2) add na1 | (GCases _ | GRec _ | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _),_ @@ -63,8 +63,9 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with | NBinderList (i1, j1, t1, u1), NBinderList (i2, j2, t2, u2) -> Id.equal i1 i2 && Id.equal j1 j2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2 -| NLetIn (na1, t1, u1), NLetIn (na2, t2, u2) -> - Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2 +| NLetIn (na1, b1, t1, u1), NLetIn (na2, b2, t2, u2) -> + Name.equal na1 na2 && eq_notation_constr vars b1 b2 && + Option.equal (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2 | NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (** FIXME? *) let eqpat (p1, t1) (p2, t2) = List.equal cases_pattern_eq p1 p2 && @@ -168,8 +169,8 @@ let glob_constr_of_notation_constr_with_binders loc g f e = function let e',na = g e na in GLambda (loc,na,Explicit,f e ty,f e' c) | NProd (na,ty,c) -> let e',na = g e na in GProd (loc,na,Explicit,f e ty,f e' c) - | NLetIn (na,b,c) -> - let e',na = g e na in GLetIn (loc,na,f e b,f e' c) + | NLetIn (na,b,t,c) -> + let e',na = g e na in GLetIn (loc,na,f e b,Option.map (f e) t,f e' c) | NCases (sty,rtntypopt,tml,eqnl) -> let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') -> let e',t' = match t with @@ -347,7 +348,7 @@ let notation_constr_and_vars_of_glob_constr a = | GApp (_,g,args) -> NApp (aux g, List.map aux args) | 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) + | GLetIn (_,na,b,t,c) -> add_name found na; NLetIn (na,aux b,Option.map aux t,aux c) | GCases (_,sty,rtntypopt,tml,eqnl) -> let f (_,idl,pat,rhs) = List.iter (add_id found) idl; (pat,aux rhs) in NCases (sty,Option.map aux rtntypopt, @@ -497,11 +498,12 @@ let rec subst_notation_constr subst bound raw = if r1' == r1 && r2' == r2 then raw else NBinderList (id1,id2,r1',r2') - | NLetIn (n,r1,r2) -> - let r1' = subst_notation_constr subst bound r1 - and r2' = subst_notation_constr subst bound r2 in - if r1' == r1 && r2' == r2 then raw else - NLetIn (n,r1',r2') + | NLetIn (n,r1,t,r2) -> + let r1' = subst_notation_constr subst bound r1 in + let t' = Option.smartmap (subst_notation_constr subst bound) t in + let r2' = subst_notation_constr subst bound r2 in + if r1' == r1 && t == t' && r2' == r2 then raw else + NLetIn (n,r1',t',r2') | NCases (sty,rtntypopt,rl,branches) -> let rtntypopt' = Option.smartmap (subst_notation_constr subst bound) rtntypopt @@ -781,18 +783,23 @@ let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma) | GHole _, _ -> v' | _, GHole _ -> v | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v else raise No_match in + let unify_opt_term alp v v' = + match v, v' with + | Some t, Some t' -> Some (unify_term alp t t') + | (Some _ as x), None | None, (Some _ as x) -> x + | None, None -> None in let unify_binding_kind bk bk' = if bk == bk' then bk' else raise No_match in let unify_binder alp b b' = match b, b' with - | (Inl na, bk, None, t), (Inl na', bk', None, t') (* assum *) -> + | GLocalAssum (loc,na,bk,t), GLocalAssum (_,na',bk',t') -> let alp, na = unify_name alp na na' in - alp, (Inl na, unify_binding_kind bk bk', None, unify_term alp t t') - | (Inl na, bk, Some c, t), (Inl na', bk', Some c', t') (* let *) -> + alp, GLocalAssum (loc, na, unify_binding_kind bk bk', unify_term alp t t') + | GLocalDef (loc,na,bk,c,t), GLocalDef (_,na',bk',c',t') -> let alp, na = unify_name alp na na' in - alp, (Inl na, unify_binding_kind bk bk', Some (unify_term alp c c'), unify_term alp t t') - | (Inr p, bk, None, t), (Inr p', bk', None, t') (* pattern *) -> + alp, GLocalDef (loc, na, unify_binding_kind bk bk', unify_term alp c c', unify_opt_term alp t t') + | GLocalPattern (loc,(p,ids),id,bk,t), GLocalPattern (_,(p',_),_,bk',t') -> let alp, p = unify_pat alp p p' in - alp, (Inr p, unify_binding_kind bk bk', None, unify_term alp t t') + alp, GLocalPattern (loc, (p,ids), id, unify_binding_kind bk bk', unify_term alp t t') | _ -> raise No_match in let rec unify alp bl bl' = match bl, bl' with @@ -821,16 +828,16 @@ let bind_bindinglist_as_term_env alp (terms,onlybinders,termlists,binderlists) v else raise No_match in let unify_term_binder c b' = match c, b' with - | GVar (_, id), (Inl na', bk', None, t') (* assum *) -> - (Inl (unify_id id na'), bk', None, t') - | c, (Inr p', bk', None, t') (* pattern *) -> + | GVar (loc, id), GLocalAssum (_, na', bk', t') -> + GLocalAssum (loc, unify_id id na', bk', t') + | c, GLocalPattern (loc, (p',ids), id, bk', t') -> let p = pat_binder_of_term c in - (Inr (unify_pat p p'), bk', None, t') + GLocalPattern (loc, (unify_pat p p',ids), id, bk', t') | _ -> raise No_match in let rec unify cl bl' = match cl, bl' with | [], [] -> [] - | c :: cl, (Inl _, _, Some _,t) :: bl' -> unify cl bl' + | c :: cl, GLocalDef (_, _, _, _, t) :: bl' -> unify cl bl' | c :: cl, b' :: bl' -> unify_term_binder c b' :: unify cl bl' | _ -> raise No_match in let bl = unify cl bl' in @@ -883,19 +890,19 @@ let rec match_cases_pattern_binders metas acc pat1 pat2 = let glue_letin_with_decls = true let rec match_iterated_binders islambda decls = function - | GLambda (_,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b)])) + | GLambda (loc,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,ids,[cp],b)])) when islambda && Id.equal p e -> - match_iterated_binders islambda ((Inr cp,bk,None,t)::decls) b - | GLambda (_,na,bk,t,b) when islambda -> - match_iterated_binders islambda ((Inl na,bk,None,t)::decls) b - | GProd (_,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b)])) + match_iterated_binders islambda (GLocalPattern (loc,(cp,ids),p,bk,t)::decls) b + | GLambda (loc,na,bk,t,b) when islambda -> + match_iterated_binders islambda (GLocalAssum (loc,na,bk,t)::decls) b + | GProd (loc,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,ids,[cp],b)])) when not islambda && Id.equal p e -> - match_iterated_binders islambda ((Inr cp,bk,None,t)::decls) b - | GProd (_,(Name _ as na),bk,t,b) when not islambda -> - match_iterated_binders islambda ((Inl na,bk,None,t)::decls) b - | GLetIn (loc,na,c,b) when glue_letin_with_decls -> + match_iterated_binders islambda (GLocalPattern (loc,(cp,ids),p,bk,t)::decls) b + | GProd (loc,(Name _ as na),bk,t,b) when not islambda -> + match_iterated_binders islambda (GLocalAssum (loc,na,bk,t)::decls) b + | GLetIn (loc,na,c,t,b) when glue_letin_with_decls -> match_iterated_binders islambda - ((Inl na,Explicit (*?*), Some c,GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None))::decls) b + (GLocalDef (loc,na,Explicit (*?*), c,t)::decls) b | b -> (decls,b) let remove_sigma x (terms,onlybinders,termlists,binderlists) = @@ -972,29 +979,29 @@ let rec match_ inner u alp metas sigma a1 a2 = match_termlist (match_hd u alp) alp metas sigma r1 x y iter termin lassoc (* "λ p, let 'cp = p in t" -> "λ 'cp, t" *) - | GLambda (_,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b1)])), + | GLambda (loc,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,ids,[cp],b1)])), NBinderList (x,_,NLambda (Name _id2,_,b2),termin) when Id.equal p e -> - let (decls,b) = match_iterated_binders true [(Inr cp,bk,None,t1)] b1 in + let (decls,b) = match_iterated_binders true [GLocalPattern(loc,(cp,ids),p,bk,t1)] b1 in let alp,sigma = bind_bindinglist_env alp sigma x decls in match_in u alp metas sigma b termin (* Matching recursive notations for binders: ad hoc cases supporting let-in *) - | GLambda (_,na1,bk,t1,b1), NBinderList (x,_,NLambda (Name _id2,_,b2),termin)-> - let (decls,b) = match_iterated_binders true [(Inl na1,bk,None,t1)] b1 in + | GLambda (loc,na1,bk,t1,b1), NBinderList (x,_,NLambda (Name _id2,_,b2),termin)-> + let (decls,b) = match_iterated_binders true [GLocalAssum (loc,na1,bk,t1)] b1 in (* TODO: address the possibility that termin is a Lambda itself *) let alp,sigma = bind_bindinglist_env alp sigma x decls in match_in u alp metas sigma b termin (* "∀ p, let 'cp = p in t" -> "∀ 'cp, t" *) - | GProd (_,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b1)])), + | GProd (loc,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,ids,[cp],b1)])), NBinderList (x,_,NProd (Name _id2,_,b2),(NVar v as termin)) when Id.equal p e -> - let (decls,b) = match_iterated_binders true [(Inr cp,bk,None,t1)] b1 in + let (decls,b) = match_iterated_binders true [GLocalPattern (loc,(cp,ids),p,bk,t1)] b1 in let alp,sigma = bind_bindinglist_env alp sigma x decls in match_in u alp metas sigma b termin - | GProd (_,na1,bk,t1,b1), NBinderList (x,_,NProd (Name _id2,_,b2),termin) + | GProd (loc,na1,bk,t1,b1), NBinderList (x,_,NProd (Name _id2,_,b2),termin) when na1 != Anonymous -> - let (decls,b) = match_iterated_binders false [(Inl na1,bk,None,t1)] b1 in + let (decls,b) = match_iterated_binders false [GLocalAssum (loc,na1,bk,t1)] b1 in (* TODO: address the possibility that termin is a Prod itself *) let alp,sigma = bind_bindinglist_env alp sigma x decls in match_in u alp metas sigma b termin @@ -1003,18 +1010,18 @@ let rec match_ inner u alp metas sigma a1 a2 = match_binderlist_with_app (match_hd u) alp metas sigma r x y iter termin (* Matching individual binders as part of a recursive pattern *) - | GLambda (_,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b1)])), + | GLambda (loc,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,ids,[cp],b1)])), NLambda (Name id,_,b2) when is_bindinglist_meta id metas -> - let alp,sigma = bind_bindinglist_env alp sigma id [(Inr cp,bk,None,t)] in + let alp,sigma = bind_bindinglist_env alp sigma id [GLocalPattern (loc,(cp,ids),p,bk,t)] in match_in u alp metas sigma b1 b2 - | GLambda (_,na,bk,t,b1), NLambda (Name id,_,b2) + | GLambda (loc,na,bk,t,b1), NLambda (Name id,_,b2) when is_bindinglist_meta id metas -> - let alp,sigma = bind_bindinglist_env alp sigma id [(Inl na,bk,None,t)] in + let alp,sigma = bind_bindinglist_env alp sigma id [GLocalAssum (loc,na,bk,t)] in match_in u alp metas sigma b1 b2 - | GProd (_,na,bk,t,b1), NProd (Name id,_,b2) + | GProd (loc,na,bk,t,b1), NProd (Name id,_,b2) when is_bindinglist_meta id metas && na != Anonymous -> - let alp,sigma = bind_bindinglist_env alp sigma id [(Inl na,bk,None,t)] in + let alp,sigma = bind_bindinglist_env alp sigma id [GLocalAssum (loc,na,bk,t)] in match_in u alp metas sigma b1 b2 (* Matching compositionally *) @@ -1035,8 +1042,12 @@ let rec match_ inner u alp metas sigma a1 a2 = match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2 | GProd (_,na1,_,t1,b1), NProd (na2,t2,b2) -> match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2 - | GLetIn (_,na1,t1,b1), NLetIn (na2,t2,b2) -> - match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2 + | GLetIn (_,na1,b1,_,c1), NLetIn (na2,b2,None,c2) + | GLetIn (_,na1,b1,None,c1), NLetIn (na2,b2,_,c2) -> + match_binders u alp metas na1 na2 (match_in u alp metas sigma b1 b2) c1 c2 + | GLetIn (_,na1,b1,Some t1,c1), NLetIn (na2,b2,Some t2,c2) -> + match_binders u alp metas na1 na2 + (match_in u alp metas (match_in u alp metas sigma b1 b2) t1 t2) c1 c2 | GCases (_,sty1,rtno1,tml1,eqnl1), NCases (sty2,rtno2,tml2,eqnl2) when sty1 == sty2 && Int.equal (List.length tml1) (List.length tml2) @@ -1102,7 +1113,7 @@ let rec match_ inner u alp metas sigma a1 a2 = | _ -> assert false in let (alp,sigma) = if is_bindinglist_meta id metas then - bind_bindinglist_env alp sigma id [(Inl (Name id'),Explicit,None,t1)] + bind_bindinglist_env alp sigma id [GLocalAssum (Loc.ghost,Name id',Explicit,t1)] else match_names metas (alp,sigma) (Name id') na in match_in u alp metas sigma (mkGApp Loc.ghost b1 (GVar (Loc.ghost,id'))) b2 diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index c8fcbf741..a61ba172e 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -47,12 +47,9 @@ val glob_constr_of_notation_constr : Loc.t -> notation_constr -> glob_constr exception No_match -type glob_decl2 = - (name, cases_pattern) Util.union * Decl_kinds.binding_kind * - glob_constr option * glob_constr val match_notation_constr : bool -> glob_constr -> interpretation -> (glob_constr * subscopes) list * (glob_constr list * subscopes) list * - (glob_decl2 list * subscopes) list + (extended_glob_local_binder list * subscopes) list val match_notation_constr_cases_pattern : cases_pattern -> interpretation -> diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index 178c1c1f9..d863e0561 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -28,7 +28,7 @@ let global_of_extended_global_head = function | NRef ref -> ref | NApp (rc, _) -> head_of rc | NCast (rc, _) -> head_of rc - | NLetIn (_, _, rc) -> head_of rc + | NLetIn (_, _, _, rc) -> head_of rc | _ -> raise Not_found in head_of syn_def diff --git a/interp/topconstr.ml b/interp/topconstr.ml index fd57b70ca..89e04b69d 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -89,13 +89,13 @@ let rec fold_constr_expr_binders g f n acc b = function f n acc b let rec fold_local_binders g f n acc b = function - | LocalRawAssum (nal,bk,t)::l -> + | CLocalAssum (nal,bk,t)::l -> let nal = snd (List.split nal) in let n' = List.fold_right (name_fold g) nal n in f n (fold_local_binders g f n' acc b l) t - | LocalRawDef ((_,na),t)::l -> - f n (fold_local_binders g f (name_fold g na n) acc b l) t - | LocalPattern (_,pat,t)::l -> + | CLocalDef ((_,na),c,t)::l -> + Option.fold_left (f n) (f n (fold_local_binders g f (name_fold g na n) acc b l) c) t + | CLocalPattern (_,pat,t)::l -> let acc = fold_local_binders g f (cases_pattern_fold_names g n pat) acc b l in Option.fold_left (f n) acc t | [] -> @@ -105,7 +105,8 @@ let fold_constr_expr_with_binders g f n acc = function | 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] + | CLetIn (_,na,a,t,b) -> + f (name_fold g (snd na) n) (Option.fold_left (f n) (f n acc a) t) b | CCast (loc,a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b | CCast (loc,a,CastCoerce) -> f n acc a | CNotation (_,_,(l,ll,bll)) -> @@ -160,7 +161,7 @@ let split_at_annot bl na = end | Some (loc, id) -> let rec aux acc = function - | LocalRawAssum (bls, k, t) as x :: rest -> + | CLocalAssum (bls, k, t) as x :: rest -> let test (_, na) = match na with | Name id' -> Id.equal id id' | Anonymous -> false @@ -171,12 +172,12 @@ let split_at_annot bl na = | _ -> let ans = match l with | [] -> acc - | _ -> LocalRawAssum (l, k, t) :: acc + | _ -> CLocalAssum (l, k, t) :: acc in - (List.rev ans, LocalRawAssum (r, k, t) :: rest) + (List.rev ans, CLocalAssum (r, k, t) :: rest) end - | LocalRawDef _ as x :: rest -> aux (x :: acc) rest - | LocalPattern (loc,_,_) :: rest -> + | CLocalDef _ as x :: rest -> aux (x :: acc) rest + | CLocalPattern (loc,_,_) :: rest -> Loc.raise ~loc (Stream.Error "pattern with quote not allowed after fix") | [] -> user_err ~loc @@ -196,13 +197,13 @@ let map_binders f g e bl = let map_local_binders f g e bl = (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *) let h (e,bl) = function - LocalRawAssum(nal,k,ty) -> - (map_binder g e nal, LocalRawAssum(nal,k,f e ty)::bl) - | LocalRawDef((loc,na),ty) -> - (name_fold g na e, LocalRawDef((loc,na),f e ty)::bl) - | LocalPattern (loc,pat,t) -> + CLocalAssum(nal,k,ty) -> + (map_binder g e nal, CLocalAssum(nal,k,f e ty)::bl) + | CLocalDef((loc,na),c,ty) -> + (name_fold g na e, CLocalDef((loc,na),f e c,Option.map (f e) ty)::bl) + | CLocalPattern (loc,pat,t) -> let ids = ids_of_pattern pat in - (Id.Set.fold g ids e, LocalPattern (loc,pat,Option.map (f e) t)::bl) in + (Id.Set.fold g ids e, CLocalPattern (loc,pat,Option.map (f e) t)::bl) in let (e,rbl) = List.fold_left h (e,[]) bl in (e, List.rev rbl) @@ -214,7 +215,8 @@ let map_constr_expr_with_binders g f e = function let (e,bl) = map_binders f g e bl in CProdN (loc,bl,f e b) | CLambdaN (loc,bl,b) -> let (e,bl) = map_binders f g e bl in CLambdaN (loc,bl,f e b) - | CLetIn (loc,na,a,b) -> CLetIn (loc,na,f e a,f (name_fold g (snd na) e) b) + | CLetIn (loc,na,a,t,b) -> + CLetIn (loc,na,f e a,Option.map (f e) t,f (name_fold g (snd na) e) b) | CCast (loc,a,c) -> CCast (loc,f e a, Miscops.map_cast_type (f e) c) | CNotation (loc,n,(l,ll,bll)) -> (* This is an approximation because we don't know what binds what *) diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 95d702f8d..b6ac40041 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -25,7 +25,7 @@ val occur_var_constr_expr : Id.t -> constr_expr -> bool (** Specific function for interning "in indtype" syntax of "match" *) val ids_of_cases_indtype : cases_pattern_expr -> Id.Set.t -val split_at_annot : local_binder list -> Id.t located option -> local_binder list * local_binder list +val split_at_annot : local_binder_expr list -> Id.t located option -> local_binder_expr list * local_binder_expr list (** Used in typeclasses *) diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index 0cbb29575..49bafadc8 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -72,7 +72,7 @@ and constr_expr = | CCoFix of Loc.t * Id.t located * cofix_expr list | CProdN of Loc.t * binder_expr list * constr_expr | CLambdaN of Loc.t * binder_expr list * constr_expr - | CLetIn of Loc.t * Name.t located * constr_expr * constr_expr + | CLetIn of Loc.t * Name.t located * constr_expr * constr_expr option * constr_expr | CAppExpl of Loc.t * (proj_flag * reference * instance_expr option) * constr_expr list | CApp of Loc.t * (proj_flag * constr_expr) * (constr_expr * explicitation located option) list @@ -111,10 +111,10 @@ and binder_expr = and fix_expr = Id.t located * (Id.t located option * recursion_order_expr) * - local_binder list * constr_expr * constr_expr + local_binder_expr list * constr_expr * constr_expr and cofix_expr = - Id.t located * local_binder list * constr_expr * constr_expr + Id.t located * local_binder_expr list * constr_expr * constr_expr and recursion_order_expr = | CStructRec @@ -122,15 +122,15 @@ and recursion_order_expr = | CMeasureRec of constr_expr * constr_expr option (** measure, relation *) (** Anonymous defs allowed ?? *) -and local_binder = - | LocalRawDef of Name.t located * constr_expr - | LocalRawAssum of Name.t located list * binder_kind * constr_expr - | LocalPattern of Loc.t * cases_pattern_expr * constr_expr option +and local_binder_expr = + | CLocalAssum of Name.t located list * binder_kind * constr_expr + | CLocalDef of Name.t located * constr_expr * constr_expr option + | CLocalPattern of Loc.t * cases_pattern_expr * constr_expr option and constr_notation_substitution = constr_expr list * (** for constr subterms *) constr_expr list list * (** for recursive notations *) - local_binder list list (** for binders subexpressions *) + local_binder_expr list list (** for binders subexpressions *) type typeclass_constraint = (Name.t located * Id.t located list option) * binding_kind * constr_expr diff --git a/intf/glob_term.mli b/intf/glob_term.mli index b3159c860..ced5a8b44 100644 --- a/intf/glob_term.mli +++ b/intf/glob_term.mli @@ -42,7 +42,7 @@ type glob_constr = | GApp of Loc.t * glob_constr * glob_constr list | GLambda of Loc.t * Name.t * binding_kind * glob_constr * glob_constr | GProd of Loc.t * Name.t * binding_kind * glob_constr * glob_constr - | GLetIn of Loc.t * Name.t * glob_constr * glob_constr + | GLetIn of Loc.t * Name.t * glob_constr * glob_constr option * glob_constr | GCases of Loc.t * case_style * glob_constr option * tomatch_tuples * cases_clauses (** [GCases(l,style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in [MatchStyle]) *) | GLetTuple of Loc.t * Name.t list * (Name.t * glob_constr option) * @@ -78,6 +78,11 @@ and cases_clause = (Loc.t * Id.t list * cases_pattern list * glob_constr) of [t] are members of [il]. *) and cases_clauses = cases_clause list +type extended_glob_local_binder = + | GLocalAssum of Loc.t * Name.t * binding_kind * glob_constr + | GLocalDef of Loc.t * Name.t * binding_kind * glob_constr * glob_constr option + | GLocalPattern of Loc.t * (cases_pattern * Id.t list) * Id.t * binding_kind * glob_constr + (** A globalised term together with a closure representing the value of its free variables. Intended for use when these variables are taken from the Ltac environment. *) diff --git a/intf/notation_term.mli b/intf/notation_term.mli index 1ab9980a5..753fa657a 100644 --- a/intf/notation_term.mli +++ b/intf/notation_term.mli @@ -30,7 +30,7 @@ type notation_constr = | NLambda of Name.t * notation_constr * notation_constr | NProd of Name.t * notation_constr * notation_constr | NBinderList of Id.t * Id.t * notation_constr * notation_constr - | NLetIn of Name.t * notation_constr * notation_constr + | NLetIn of Name.t * notation_constr * notation_constr option * notation_constr | NCases of case_style * notation_constr option * (notation_constr * (Name.t * (inductive * Name.t list) option)) list * (cases_pattern list * notation_constr) list diff --git a/intf/pattern.mli b/intf/pattern.mli index ac84b91e6..48381cacd 100644 --- a/intf/pattern.mli +++ b/intf/pattern.mli @@ -68,7 +68,7 @@ type constr_pattern = | PProj of projection * constr_pattern | PLambda of Name.t * constr_pattern * constr_pattern | PProd of Name.t * constr_pattern * constr_pattern - | PLetIn of Name.t * constr_pattern * constr_pattern + | PLetIn of Name.t * constr_pattern * constr_pattern option * constr_pattern | PSort of glob_sort | PMeta of patvar option | PIf of constr_pattern * constr_pattern * constr_pattern diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 8827bc132..25d3c705f 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -175,15 +175,15 @@ type plident = lident * lident list option type sort_expr = glob_sort type definition_expr = - | ProveBody of local_binder list * constr_expr - | DefineBody of local_binder list * Genredexpr.raw_red_expr option * constr_expr + | ProveBody of local_binder_expr list * constr_expr + | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr * constr_expr option type fixpoint_expr = - plident * (Id.t located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr option + plident * (Id.t located option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr option type cofixpoint_expr = - plident * local_binder list * constr_expr * constr_expr option + plident * local_binder_expr list * constr_expr * constr_expr option type local_decl_expr = | AssumExpr of lname * constr_expr @@ -202,14 +202,14 @@ type constructor_list_or_record_decl_expr = | Constructors of constructor_expr list | RecordDecl of lident option * local_decl_expr with_instance with_priority with_notation list type inductive_expr = - plident with_coercion * local_binder list * constr_expr option * inductive_kind * + plident with_coercion * local_binder_expr list * constr_expr option * inductive_kind * constructor_list_or_record_decl_expr type one_inductive_expr = - plident * local_binder list * constr_expr option * constructor_expr list + plident * local_binder_expr list * constr_expr option * constructor_expr list type proof_expr = - plident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option) + plident option * (local_binder_expr list * constr_expr * (lident option * recursion_order_expr) option) type syntax_modifier = | SetItemLevel of string list * Extend.production_level @@ -283,14 +283,9 @@ type bullet = | Plus of int (** {6 Types concerning Stm} *) -type 'a stm_vernac = +type stm_vernac = | JoinDocument - | Finish | Wait - | PrintDag - | Observe of Stateid.t - | Command of 'a (* An out of flow command not to be recorded by Stm *) - | PGLast of 'a (* To ease the life of PG *) (** {6 Types concerning the module layer} *) @@ -370,12 +365,12 @@ type vernac_expr = (* Type classes *) | VernacInstance of bool * (* abstract instance *) - local_binder list * (* super *) + local_binder_expr list * (* super *) typeclass_constraint * (* instance name, class name, params *) (bool * constr_expr) option * (* props *) hint_info_expr - | VernacContext of local_binder list + | VernacContext of local_binder_expr list | VernacDeclareInstances of (reference * hint_info_expr) list (* instances names, priorities and patterns *) @@ -450,8 +445,9 @@ type vernac_expr = | VernacRegister of lident * register_kind | VernacComments of comment list - (* Stm backdoor *) - | VernacStm of vernac_expr stm_vernac + (* Stm backdoor: used in fake_id, will be removed when fake_ide + becomes aware of feedback about completed jobs. *) + | VernacStm of stm_vernac (* Proof management *) | VernacGoal of constr_expr @@ -509,16 +505,11 @@ and report_with = Stateid.t * Feedback.route_id (* feedback on id/route *) and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *) and vernac_start = string * opacity_guarantee * Id.t list and vernac_sideff_type = Id.t list -and vernac_is_alias = bool and vernac_part_of_script = bool and vernac_control = - | VtFinish | VtWait | VtJoinDocument - | VtPrintDag - | VtObserve of Stateid.t | VtBack of Stateid.t - | VtPG and opacity_guarantee = | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) diff --git a/library/summary.ml b/library/summary.ml index 2ec4760d6..d9f644100 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -108,7 +108,7 @@ let unfreeze_summaries fs = with e when CErrors.noncritical e -> let e = CErrors.push e in Feedback.msg_error - Pp.(seq [str "Error unfrezing summay %s\n%s\n%!"; + Pp.(seq [str "Error unfreezing summary %s\n%s\n%!"; str (name_of_summary id); CErrors.iprint e]); iraise e diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 07e4ddf84..496b20002 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -233,11 +233,11 @@ type (_, _) entry = | TTName : ('self, Name.t Loc.located) entry | TTReference : ('self, reference) entry | TTBigint : ('self, Bigint.bigint) entry -| TTBinder : ('self, local_binder list) entry +| TTBinder : ('self, local_binder_expr list) entry | TTConstr : prod_info * 'r target -> ('r, 'r) entry | TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry -| TTBinderListT : ('self, local_binder list) entry -| TTBinderListF : Tok.t list -> ('self, local_binder list list) entry +| TTBinderListT : ('self, local_binder_expr list) entry +| TTBinderListF : Tok.t list -> ('self, local_binder_expr list list) entry type _ any_entry = TTAny : ('s, 'r) entry -> 's any_entry @@ -324,7 +324,7 @@ let cases_pattern_expr_of_name (loc,na) = match na with type 'r env = { constrs : 'r list; constrlists : 'r list list; - binders : (local_binder list * bool) list; + binders : (local_binder_expr list * bool) list; } let push_constr subst v = { subst with constrs = v :: subst.constrs } diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 47455f984..c127e7880 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -38,7 +38,7 @@ let mk_cast = function in CCast(loc, c, CastConv ty) let binder_of_name expl (loc,na) = - LocalRawAssum ([loc, na], Default expl, + CLocalAssum ([loc, na], Default expl, CHole (loc, Some (Evar_kinds.BinderType na), IntroAnonymous, None)) let binders_of_names l = @@ -240,17 +240,18 @@ GEXTEND Gram mkCLambdaN (!@loc) bl c | "let"; id=name; bl = binders; ty = type_cstr; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> - let loc1 = - Loc.merge (local_binders_loc bl) (constr_loc c1) - in - CLetIn(!@loc,id,mkCLambdaN loc1 bl (mk_cast(c1,ty)),c2) + let ty,c1 = match ty, c1 with + | (_,None), CCast(loc,c, CastConv t) -> (constr_loc t,Some t), c (* Tolerance, see G_vernac.def_body *) + | _, _ -> ty, c1 in + CLetIn(!@loc,id,mkCLambdaN (constr_loc c1) bl c1, + Option.map (mkCProdN (fst ty) bl) (snd ty), c2) | "let"; fx = single_fix; "in"; c = operconstr LEVEL "200" -> let fixp = mk_single_fix fx in let (li,id) = match fixp with CFix(_,id,_) -> id | CCoFix(_,id,_) -> id | _ -> assert false in - CLetIn(!@loc,(li,Name id),fixp,c) + CLetIn(!@loc,(li,Name id),fixp,None,c) | "let"; lb = ["("; l=LIST0 name SEP ","; ")" -> l | "()" -> []]; po = return_type; ":="; c1 = operconstr LEVEL "200"; "in"; @@ -412,11 +413,11 @@ GEXTEND Gram impl_ident_tail: [ [ "}" -> binder_of_name Implicit | nal=LIST1 name; ":"; c=lconstr; "}" -> - (fun na -> LocalRawAssum (na::nal,Default Implicit,c)) + (fun na -> CLocalAssum (na::nal,Default Implicit,c)) | nal=LIST1 name; "}" -> - (fun na -> LocalRawAssum (na::nal,Default Implicit,CHole (Loc.join_loc (fst na) !@loc, Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None))) + (fun na -> CLocalAssum (na::nal,Default Implicit,CHole (Loc.join_loc (fst na) !@loc, Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None))) | ":"; c=lconstr; "}" -> - (fun na -> LocalRawAssum ([na],Default Implicit,c)) + (fun na -> CLocalAssum ([na],Default Implicit,c)) ] ] ; fixannot: @@ -442,12 +443,12 @@ GEXTEND Gram the latter is unique *) [ [ (* open binder *) id = name; idl = LIST0 name; ":"; c = lconstr -> - [LocalRawAssum (id::idl,Default Explicit,c)] + [CLocalAssum (id::idl,Default Explicit,c)] (* binders factorized with open binder *) | id = name; idl = LIST0 name; bl = binders -> binders_of_names (id::idl) @ bl | id1 = name; ".."; id2 = name -> - [LocalRawAssum ([id1;(!@loc,Name ldots_var);id2], + [CLocalAssum ([id1;(!@loc,Name ldots_var);id2], Default Explicit,CHole (!@loc, None, IntroAnonymous, None))] | bl = closed_binder; bl' = binders -> bl@bl' @@ -457,37 +458,39 @@ GEXTEND Gram [ [ l = LIST0 binder -> List.flatten l ] ] ; binder: - [ [ id = name -> [LocalRawAssum ([id],Default Explicit,CHole (!@loc, None, IntroAnonymous, None))] + [ [ id = name -> [CLocalAssum ([id],Default Explicit,CHole (!@loc, None, IntroAnonymous, None))] | bl = closed_binder -> bl ] ] ; closed_binder: [ [ "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" -> - [LocalRawAssum (id::idl,Default Explicit,c)] + [CLocalAssum (id::idl,Default Explicit,c)] | "("; id=name; ":"; c=lconstr; ")" -> - [LocalRawAssum ([id],Default Explicit,c)] + [CLocalAssum ([id],Default Explicit,c)] | "("; id=name; ":="; c=lconstr; ")" -> - [LocalRawDef (id,c)] + (match c with + | CCast(_,c, CastConv t) -> [CLocalDef (id,c,Some t)] + | _ -> [CLocalDef (id,c,None)]) | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> - [LocalRawDef (id,CCast (Loc.merge (constr_loc t) (!@loc),c, CastConv t))] + [CLocalDef (id,c,Some t)] | "{"; id=name; "}" -> - [LocalRawAssum ([id],Default Implicit,CHole (!@loc, None, IntroAnonymous, None))] + [CLocalAssum ([id],Default Implicit,CHole (!@loc, None, IntroAnonymous, None))] | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" -> - [LocalRawAssum (id::idl,Default Implicit,c)] + [CLocalAssum (id::idl,Default Implicit,c)] | "{"; id=name; ":"; c=lconstr; "}" -> - [LocalRawAssum ([id],Default Implicit,c)] + [CLocalAssum ([id],Default Implicit,c)] | "{"; id=name; idl=LIST1 name; "}" -> - List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (!@loc, None, IntroAnonymous, None))) (id::idl) + List.map (fun id -> CLocalAssum ([id],Default Implicit,CHole (!@loc, None, IntroAnonymous, None))) (id::idl) | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" -> - List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Explicit, b), t)) tc + List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, Explicit, b), t)) tc | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" -> - List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Implicit, b), t)) tc + List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, Implicit, b), t)) tc | "'"; p = pattern LEVEL "0" -> let (p, ty) = match p with | CPatCast (_, p, ty) -> (p, Some ty) | _ -> (p, None) in - [LocalPattern (!@loc, p, ty)] + [CLocalPattern (!@loc, p, ty)] ] ] ; typeclass_constraint: diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 18807113c..ded7a557c 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -66,13 +66,7 @@ GEXTEND Gram (* Stm backdoor *) | IDENT "Stm"; IDENT "JoinDocument"; "." -> VernacStm JoinDocument - | IDENT "Stm"; IDENT "Finish"; "." -> VernacStm Finish | IDENT "Stm"; IDENT "Wait"; "." -> VernacStm Wait - | IDENT "Stm"; IDENT "PrintDag"; "." -> VernacStm PrintDag - | IDENT "Stm"; IDENT "Observe"; id = INT; "." -> - VernacStm (Observe (Stateid.of_int (int_of_string id))) - | IDENT "Stm"; IDENT "Command"; v = vernac_aux -> VernacStm (Command v) - | IDENT "Stm"; IDENT "PGLast"; v = vernac_aux -> VernacStm (PGLast v) | v = vernac_poly -> v ] ] @@ -249,7 +243,7 @@ GEXTEND Gram | _ -> DefineBody (bl, red, c, None)) | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr -> let ((bl, c), tyo) = - if List.exists (function LocalPattern _ -> true | _ -> false) bl + if List.exists (function CLocalPattern _ -> true | _ -> false) bl then let c = CCast (!@loc, c, CastConv t) in (expand_pattern_binders mkCLambdaN bl c, None) @@ -340,8 +334,8 @@ GEXTEND Gram binder_nodef: [ [ b = binder_let -> (match b with - LocalRawAssum(l,ty) -> (l,ty) - | LocalRawDef _ -> + CLocalAssum(l,ty) -> (l,ty) + | CLocalDef _ -> Util.user_err_loc (loc,"fix_param",Pp.str"defined binder not allowed here.")) ] ] ; diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index cf5174af9..6c148d393 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -162,11 +162,11 @@ module Constr : val pattern : cases_pattern_expr Gram.entry val constr_pattern : constr_expr Gram.entry val lconstr_pattern : constr_expr Gram.entry - val closed_binder : local_binder list Gram.entry - val binder : local_binder list Gram.entry (* closed_binder or variable *) - val binders : local_binder list Gram.entry (* list of binder *) - val open_binders : local_binder list Gram.entry - val binders_fixannot : (local_binder list * (Id.t located option * recursion_order_expr)) Gram.entry + val closed_binder : local_binder_expr list Gram.entry + val binder : local_binder_expr list Gram.entry (* closed_binder or variable *) + val binders : local_binder_expr list Gram.entry (* list of binder *) + val open_binders : local_binder_expr list Gram.entry + val binders_fixannot : (local_binder_expr list * (Id.t located option * recursion_order_expr)) Gram.entry val typeclass_constraint : (Name.t located * bool * constr_expr) Gram.entry val record_declaration : constr_expr Gram.entry val appl_arg : (constr_expr * explicitation located option) Gram.entry diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 3aa572529..a29480a55 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -264,7 +264,7 @@ let prod_one_id (loc,id) glob = GHole (loc,Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), glob) let let_in_one_alias (id,pat) glob = - GLetIn (Loc.ghost,Name id, glob_of_pat pat, glob) + GLetIn (Loc.ghost,Name id, glob_of_pat pat, None, glob) let rec bind_primary_aliases map pat = match pat with @@ -359,10 +359,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps = let rids=ref ([],pat_vars) in let npatt= deanonymize rids patt in List.rev (fst !rids),npatt in - let term2 = - GLetIn(Loc.ghost,Anonymous, - GCast(Loc.ghost,glob_of_pat npatt, - CastConv app_ind),term1) in + let term2=GLetIn(Loc.ghost,Anonymous,glob_of_pat npatt,Some app_ind,term1) in let term3=List.fold_right let_in_one_alias aliases term2 in let term4=List.fold_right prod_one_id loc_ids term3 in let term5=List.fold_right prod_one_hyp params term4 in diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 8aab3b742..7dc869131 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -42,7 +42,7 @@ let compose_glob_context = match bt with | Lambda n -> mkGLambda(n,t,acc) | Prod n -> mkGProd(n,t,acc) - | LetIn n -> mkGLetIn(n,t,acc) + | LetIn n -> mkGLetIn(n,t,None,acc) in List.fold_right compose_binder @@ -489,7 +489,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = | u::l -> match t with | GLambda(loc,na,_,nat,b) -> - GLetIn(Loc.ghost,na,u,aux b l) + GLetIn(Loc.ghost,na,u,None,aux b l) | _ -> GApp(Loc.ghost,t,l) in @@ -535,7 +535,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = args_res.result } | GApp _ -> assert false (* we have collected all the app in [glob_decompose_app] *) - | GLetIn(_,n,t,b) -> + | GLetIn(_,n,v,t,b) -> (* if we have [(let x := v in b) t1 ... tn] , we discard our work and compute the list of constructor for [let x = v in (b t1 ... tn)] up to alpha conversion @@ -559,7 +559,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = env funnames avoid - (mkGLetIn(new_n,t,mkGApp(new_b,args))) + (mkGLetIn(new_n,v,t,mkGApp(new_b,args))) | GCases _ | GIf _ | GLetTuple _ -> (* we have [(match e1, ...., en with ..... end) t1 tn] we first compute the result from the case and @@ -603,12 +603,13 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let new_env = raw_push_named (n,None,t) env in let b_res = build_entry_lc new_env funnames avoid b in combine_results (combine_prod n) t_res b_res - | GLetIn(_,n,v,b) -> + | GLetIn(loc,n,v,typ,b) -> (* we first compute the list of constructor corresponding to the body of the function, then the one corresponding to the value [t] and combine the two result *) + let v = match typ with None -> v | Some t -> GCast (loc,v,CastConv t) in let v_res = build_entry_lc env funnames avoid v in let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in let v_type = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr v_as_constr) in @@ -1118,8 +1119,9 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (* We have renamed all the anonymous functions during alpha_renaming phase *) end - | GLetIn(_,n,t,b) -> + | GLetIn(loc,n,v,t,b) -> begin + let t = match t with None -> v | Some t -> GCast (loc,v,CastConv t) in let not_free_in_t id = not (is_free_in id t) in let evd = (Evd.from_env env) in let t',ctx = Pretyping.understand env evd t in @@ -1135,7 +1137,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = match n with | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args -> new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) - | _ -> GLetIn(Loc.ghost,n,t,new_b), + | _ -> GLetIn(Loc.ghost,n,t,None,new_b), (* HOPING IT WOULD WORK *) Id.Set.filter not_free_in_t id_to_exclude end | GLetTuple(_,nal,(na,rto),t,b) -> @@ -1193,9 +1195,13 @@ let rec compute_cst_params relnames params = function compute_cst_params_from_app [] (params,rtl) | GApp(_,f,args) -> List.fold_left (compute_cst_params relnames) params (f::args) - | GLambda(_,_,_,t,b) | GProd(_,_,_,t,b) | GLetIn(_,_,t,b) | GLetTuple(_,_,_,t,b) -> + | GLambda(_,_,_,t,b) | GProd(_,_,_,t,b) | GLetTuple(_,_,_,t,b) -> let t_params = compute_cst_params relnames params t in compute_cst_params relnames t_params b + | GLetIn(_,_,v,t,b) -> + let v_params = compute_cst_params relnames params v in + let t_params = Option.fold_left (compute_cst_params relnames) v_params t in + compute_cst_params relnames t_params b | GCases _ -> params (* If there is still cases at this point they can only be discrimination ones *) @@ -1206,12 +1212,12 @@ let rec compute_cst_params relnames params = function and compute_cst_params_from_app acc (params,rtl) = match params,rtl with | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *) - | ((Name id,_,is_defined) as param)::params',(GVar(_,id'))::rtl' - when Id.compare id id' == 0 && not is_defined -> + | ((Name id,_,None) as param)::params',(GVar(_,id'))::rtl' + when Id.compare id id' == 0 -> compute_cst_params_from_app (param::acc) (params',rtl') | _ -> List.rev acc -let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * bool) list array) csts = +let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * glob_constr option) list array) csts = let rels_params = Array.mapi (fun i args -> @@ -1226,11 +1232,11 @@ let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * bool) let _ = try List.iteri - (fun i ((n,nt,is_defined) as param) -> + (fun i ((n,nt,typ) as param) -> if Array.for_all (fun l -> - let (n',nt',is_defined') = List.nth l i in - Name.equal n n' && glob_constr_eq nt nt' && (is_defined : bool) == is_defined') + let (n',nt',typ') = List.nth l i in + Name.equal n n' && glob_constr_eq nt nt' && Option.equal glob_constr_eq typ typ') rels_params then l := param::!l @@ -1245,15 +1251,15 @@ let rec rebuild_return_type rt = match rt with | Constrexpr.CProdN(loc,n,t') -> Constrexpr.CProdN(loc,n,rebuild_return_type t') - | Constrexpr.CLetIn(loc,na,t,t') -> - Constrexpr.CLetIn(loc,na,t,rebuild_return_type t') + | Constrexpr.CLetIn(loc,na,v,t,t') -> + Constrexpr.CLetIn(loc,na,v,t,rebuild_return_type t') | _ -> Constrexpr.CProdN(Loc.ghost,[[Loc.ghost,Anonymous], Constrexpr.Default Decl_kinds.Explicit,rt], Constrexpr.CSort(Loc.ghost,GType [])) let do_build_inductive - evd (funconstants: Term.pconstant list) (funsargs: (Name.t * glob_constr * bool) list list) + evd (funconstants: Term.pconstant list) (funsargs: (Name.t * glob_constr * glob_constr option) list list) returned_types (rtl:glob_constr list) = let _time1 = System.get_time () in @@ -1294,16 +1300,17 @@ let do_build_inductive let resa = Array.map (build_entry_lc env funnames_as_set []) rta in let env_with_graphs = let rel_arity i funargs = (* Rebuilding arities (with parameters) *) - let rel_first_args :(Name.t * Glob_term.glob_constr * bool ) list = + let rel_first_args :(Name.t * Glob_term.glob_constr * Glob_term.glob_constr option ) list = funargs in List.fold_right - (fun (n,t,is_defined) acc -> - if is_defined - then + (fun (n,t,typ) acc -> + match typ with + | Some typ -> Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, + Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ), acc) - else + | None -> Constrexpr.CProdN (Loc.ghost, [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], @@ -1361,16 +1368,17 @@ let do_build_inductive rel_constructors in let rel_arity i funargs = (* Reduilding arities (with parameters) *) - let rel_first_args :(Name.t * Glob_term.glob_constr * bool ) list = + let rel_first_args :(Name.t * Glob_term.glob_constr * Glob_term.glob_constr option ) list = (snd (List.chop nrel_params funargs)) in List.fold_right - (fun (n,t,is_defined) acc -> - if is_defined - then + (fun (n,t,typ) acc -> + match typ with + | Some typ -> Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, + Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ), acc) - else + | None -> Constrexpr.CProdN (Loc.ghost, [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], @@ -1397,12 +1405,13 @@ let do_build_inductive in let rel_params = List.map - (fun (n,t,is_defined) -> - if is_defined - then - Constrexpr.LocalRawDef((Loc.ghost,n), Constrextern.extern_glob_constr Id.Set.empty t) - else - Constrexpr.LocalRawAssum + (fun (n,t,typ) -> + match typ with + | Some typ -> + Constrexpr.CLocalDef((Loc.ghost,n), Constrextern.extern_glob_constr Id.Set.empty t, + Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ)) + | None -> + Constrexpr.CLocalAssum ([(Loc.ghost,n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Id.Set.empty t) ) rels_params diff --git a/plugins/funind/glob_term_to_relation.mli b/plugins/funind/glob_term_to_relation.mli index 5bb1376e2..0cab5a6d3 100644 --- a/plugins/funind/glob_term_to_relation.mli +++ b/plugins/funind/glob_term_to_relation.mli @@ -12,7 +12,7 @@ val build_inductive : *) Evd.evar_map -> Term.pconstant list -> - (Name.t*Glob_term.glob_constr*bool) list list -> (* The list of function args *) + (Name.t*Glob_term.glob_constr*Glob_term.glob_constr option) list list -> (* The list of function args *) Constrexpr.constr_expr list -> (* The list of function returned type *) Glob_term.glob_constr list -> (* the list of body *) unit diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 4e561fc7e..99f50437b 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -15,7 +15,7 @@ let mkGVar id = GVar(Loc.ghost,id) let mkGApp(rt,rtl) = GApp(Loc.ghost,rt,rtl) let mkGLambda(n,t,b) = GLambda(Loc.ghost,n,Explicit,t,b) let mkGProd(n,t,b) = GProd(Loc.ghost,n,Explicit,t,b) -let mkGLetIn(n,t,b) = GLetIn(Loc.ghost,n,t,b) +let mkGLetIn(n,b,t,c) = GLetIn(Loc.ghost,n,b,t,c) let mkGCases(rto,l,brl) = GCases(Loc.ghost,Term.RegularStyle,rto,l,brl) let mkGSort s = GSort(Loc.ghost,s) let mkGHole () = GHole(Loc.ghost,Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None) @@ -37,8 +37,8 @@ let glob_decompose_prod_or_letin = let rec glob_decompose_prod args = function | GProd(_,n,k,t,b) -> glob_decompose_prod ((n,None,Some t)::args) b - | GLetIn(_,n,t,b) -> - glob_decompose_prod ((n,Some t,None)::args) b + | GLetIn(_,n,b,t,c) -> + glob_decompose_prod ((n,Some b,t)::args) c | rt -> args,rt in glob_decompose_prod [] @@ -51,7 +51,7 @@ let glob_compose_prod_or_letin = fun concl decl -> match decl with | (n,None,Some t) -> mkGProd(n,t,concl) - | (n,Some bdy,None) -> mkGLetIn(n,bdy,concl) + | (n,Some bdy,t) -> mkGLetIn(n,bdy,t,concl) | _ -> assert false) let glob_decompose_prod_n n = @@ -73,8 +73,8 @@ let glob_decompose_prod_or_letin_n n = match c with | GProd(_,n,_,t,b) -> glob_decompose_prod (i-1) ((n,None,Some t)::args) b - | GLetIn(_,n,t,b) -> - glob_decompose_prod (i-1) ((n,Some t,None)::args) b + | GLetIn(_,n,b,t,c) -> + glob_decompose_prod (i-1) ((n,Some b,t)::args) c | rt -> args,rt in glob_decompose_prod n [] @@ -150,10 +150,11 @@ let change_vars = change_vars mapping t, change_vars (remove_name_from_mapping mapping name) b ) - | GLetIn(loc,name,def,b) -> + | GLetIn(loc,name,def,typ,b) -> GLetIn(loc, name, change_vars mapping def, + Option.map (change_vars mapping) typ, change_vars (remove_name_from_mapping mapping name) b ) | GLetTuple(loc,nal,(na,rto),b,e) -> @@ -272,10 +273,11 @@ let rec alpha_rt excluded rt = let new_t = alpha_rt excluded t in let new_b = alpha_rt excluded b in GProd(loc,Anonymous,k,new_t,new_b) - | GLetIn(loc,Anonymous,t,b) -> - let new_t = alpha_rt excluded t in + | GLetIn(loc,Anonymous,b,t,c) -> let new_b = alpha_rt excluded b in - GLetIn(loc,Anonymous,new_t,new_b) + let new_t = Option.map (alpha_rt excluded) t in + let new_c = alpha_rt excluded c in + GLetIn(loc,Anonymous,new_b,new_t,new_c) | GLambda(loc,Name id,k,t,b) -> let new_id = Namegen.next_ident_away id excluded in let t,b = @@ -302,19 +304,17 @@ let rec alpha_rt excluded rt = let new_t = alpha_rt new_excluded t in let new_b = alpha_rt new_excluded b in GProd(loc,Name new_id,k,new_t,new_b) - | GLetIn(loc,Name id,t,b) -> + | GLetIn(loc,Name id,b,t,c) -> let new_id = Namegen.next_ident_away id excluded in - let t,b = - if Id.equal new_id id - then t,b - else - let replace = change_vars (Id.Map.add id new_id Id.Map.empty) in - (t,replace b) + let c = + if Id.equal new_id id then c + else change_vars (Id.Map.add id new_id Id.Map.empty) c in let new_excluded = new_id::excluded in - let new_t = alpha_rt new_excluded t in let new_b = alpha_rt new_excluded b in - GLetIn(loc,Name new_id,new_t,new_b) + let new_t = Option.map (alpha_rt new_excluded) t in + let new_c = alpha_rt new_excluded c in + GLetIn(loc,Name new_id,new_b,new_t,new_c) | GLetTuple(loc,nal,(na,rto),t,b) -> @@ -388,13 +388,20 @@ let is_free_in id = | GEvar _ -> false | GPatVar _ -> false | GApp(_,rt,rtl) -> List.exists is_free_in (rt::rtl) - | GLambda(_,n,_,t,b) | GProd(_,n,_,t,b) | GLetIn(_,n,t,b) -> + | GLambda(_,n,_,t,b) | GProd(_,n,_,t,b) -> let check_in_b = match n with | Name id' -> not (Id.equal id' id) | _ -> true in is_free_in t || (check_in_b && is_free_in b) + | GLetIn(_,n,b,t,c) -> + let check_in_c = + match n with + | Name id' -> not (Id.equal id' id) + | _ -> true + in + is_free_in b || Option.cata is_free_in true t || (check_in_c && is_free_in c) | GCases(_,_,_,el,brl) -> (List.exists (fun (e,_) -> is_free_in e) el) || List.exists is_free_in_br brl @@ -473,11 +480,12 @@ let replace_var_by_term x_id term = replace_var_by_pattern t, replace_var_by_pattern b ) - | GLetIn(_,Name id,_,_) when Id.compare id x_id == 0 -> rt - | GLetIn(loc,name,def,b) -> + | GLetIn(_,Name id,_,_,_) when Id.compare id x_id == 0 -> rt + | GLetIn(loc,name,def,typ,b) -> GLetIn(loc, name, replace_var_by_pattern def, + Option.map (replace_var_by_pattern) typ, replace_var_by_pattern b ) | GLetTuple(_,nal,_,_,_) @@ -589,7 +597,7 @@ let ids_of_glob_constr c = ids_of_glob_constr [] g @ List.flatten (List.map (ids_of_glob_constr []) args) @ acc | GLambda (loc,na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc | GProd (loc,na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc - | GLetIn (loc,na,b,c) -> idof na :: ids_of_glob_constr [] b @ ids_of_glob_constr [] c @ acc + | GLetIn (loc,na,b,t,c) -> idof na :: ids_of_glob_constr [] b @ Option.cata (ids_of_glob_constr []) [] t @ ids_of_glob_constr [] c @ acc | GCast (loc,c,(CastConv t|CastVM t|CastNative t)) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] t @ acc | GCast (loc,c,CastCoerce) -> ids_of_glob_constr [] c @ acc | GIf (loc,c,(na,po),b1,b2) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] b1 @ ids_of_glob_constr [] b2 @ acc @@ -633,9 +641,9 @@ let zeta_normalize = zeta_normalize_term t, zeta_normalize_term b ) - | GLetIn(_,Name id,def,b) -> + | GLetIn(_,Name id,def,typ,b) -> zeta_normalize_term (replace_var_by_term id def b) - | GLetIn(loc,Anonymous,def,b) -> zeta_normalize_term b + | GLetIn(loc,Anonymous,def,typ,b) -> zeta_normalize_term b | GLetTuple(loc,nal,(na,rto),def,b) -> GLetTuple(loc, nal, @@ -690,7 +698,7 @@ let expand_as = | GApp(loc,f,args) -> GApp(loc,expand_as map f,List.map (expand_as map) args) | GLambda(loc,na,k,t,b) -> GLambda(loc,na,k,expand_as map t, expand_as map b) | GProd(loc,na,k,t,b) -> GProd(loc,na,k,expand_as map t, expand_as map b) - | GLetIn(loc,na,v,b) -> GLetIn(loc,na, expand_as map v,expand_as map b) + | GLetIn(loc,na,v,typ,b) -> GLetIn(loc,na, expand_as map v,Option.map (expand_as map) typ,expand_as map b) | GLetTuple(loc,nal,(na,po),v,b) -> GLetTuple(loc,nal,(na,Option.map (expand_as map) po), expand_as map v, expand_as map b) diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index 179e8fe8d..84359a36b 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -19,7 +19,7 @@ val mkGVar : Id.t -> glob_constr val mkGApp : glob_constr*(glob_constr list) -> glob_constr val mkGLambda : Name.t * glob_constr * glob_constr -> glob_constr val mkGProd : Name.t * glob_constr * glob_constr -> glob_constr -val mkGLetIn : Name.t * glob_constr * glob_constr -> glob_constr +val mkGLetIn : Name.t * glob_constr * glob_constr option * glob_constr -> glob_constr val mkGCases : glob_constr option * tomatch_tuples * cases_clauses -> glob_constr val mkGSort : glob_sort -> glob_constr val mkGHole : unit -> glob_constr (* we only build Evd.BinderType Anonymous holes *) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 2852152e1..ebeddf5f6 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -134,11 +134,11 @@ let functional_induction with_clean c princl pat = let rec abstract_glob_constr c = function | [] -> c - | Constrexpr.LocalRawDef (x,b)::bl -> Constrexpr_ops.mkLetInC(x,b,abstract_glob_constr c bl) - | Constrexpr.LocalRawAssum (idl,k,t)::bl -> + | Constrexpr.CLocalDef (x,b,t)::bl -> Constrexpr_ops.mkLetInC(x,b,t,abstract_glob_constr c bl) + | Constrexpr.CLocalAssum (idl,k,t)::bl -> List.fold_right (fun x b -> Constrexpr_ops.mkLambdaC([x],k,t,b)) idl (abstract_glob_constr c bl) - | Constrexpr.LocalPattern _::bl -> assert false + | Constrexpr.CLocalPattern _::bl -> assert false let interp_casted_constr_with_implicits env sigma impls c = Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls @@ -197,8 +197,10 @@ let is_rec names = | GRec _ -> error "GRec not handled" | GIf(_,b,_,lhs,rhs) -> (lookup names b) || (lookup names lhs) || (lookup names rhs) - | GLetIn(_,na,t,b) | GLambda(_,na,_,t,b) | GProd(_,na,_,t,b) -> + | GProd(_,na,_,t,b) | GLambda(_,na,_,t,b) -> lookup names t || lookup (Nameops.name_fold Id.Set.remove na names) b + | GLetIn(_,na,b,t,c) -> + lookup names b || Option.cata (lookup names) true t || lookup (Nameops.name_fold Id.Set.remove na names) c | GLetTuple(_,nal,_,t,b) -> lookup names t || lookup (List.fold_left @@ -220,9 +222,9 @@ let is_rec names = let rec local_binders_length = function (* Assume that no `{ ... } contexts occur *) | [] -> 0 - | Constrexpr.LocalRawDef _::bl -> 1 + local_binders_length bl - | Constrexpr.LocalRawAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl - | Constrexpr.LocalPattern _::bl -> assert false + | Constrexpr.CLocalDef _::bl -> 1 + local_binders_length bl + | Constrexpr.CLocalAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl + | Constrexpr.CLocalPattern _::bl -> assert false let prepare_body ((name,_,args,types,_),_) rt = let n = local_binders_length args in @@ -511,7 +513,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas | None -> begin match args with - | [Constrexpr.LocalRawAssum ([(_,Name x)],k,t)] -> t,x + | [Constrexpr.CLocalAssum ([(_,Name x)],k,t)] -> t,x | _ -> error "Recursive argument must be specified" end | Some wf_args -> @@ -519,7 +521,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas match List.find (function - | Constrexpr.LocalRawAssum(l,k,t) -> + | Constrexpr.CLocalAssum(l,k,t) -> List.exists (function (_,Name id) -> Id.equal id wf_args | _ -> false) l @@ -527,7 +529,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas ) args with - | Constrexpr.LocalRawAssum(_,k,t) -> t,wf_args + | Constrexpr.CLocalAssum(_,k,t) -> t,wf_args | _ -> assert false with Not_found -> assert false in @@ -585,10 +587,10 @@ let make_assoc assoc l1 l2 = let rec rebuild_bl (aux,assoc) bl typ = match bl,typ with | [], _ -> (List.rev aux,replace_vars_constr_expr assoc typ,assoc) - | (Constrexpr.LocalRawAssum(nal,bk,_))::bl',typ -> + | (Constrexpr.CLocalAssum(nal,bk,_))::bl',typ -> rebuild_nal (aux,assoc) bk bl' nal (List.length nal) typ - | (Constrexpr.LocalRawDef(na,_))::bl',Constrexpr.CLetIn(_,_,nat,typ') -> - rebuild_bl ((Constrexpr.LocalRawDef(na,replace_vars_constr_expr assoc nat)::aux),assoc) + | (Constrexpr.CLocalDef(na,_,_))::bl',Constrexpr.CLetIn(_,_,nat,ty,typ') -> + rebuild_bl ((Constrexpr.CLocalDef(na,replace_vars_constr_expr assoc nat,Option.map (replace_vars_constr_expr assoc) ty (* ??? *))::aux),assoc) bl' typ' | _ -> assert false and rebuild_nal (aux,assoc) bk bl' nal lnal typ = @@ -601,7 +603,7 @@ let rec rebuild_bl (aux,assoc) bl typ = then let old_nal',new_nal' = List.chop lnal nal' in let nassoc = make_assoc assoc old_nal' nal in - let assum = LocalRawAssum(nal,bk,replace_vars_constr_expr assoc nal't) in + let assum = CLocalAssum(nal,bk,replace_vars_constr_expr assoc nal't) in rebuild_bl ((assum :: aux), nassoc) bl' (if List.is_empty new_nal' && List.is_empty rest then typ' @@ -611,7 +613,7 @@ let rec rebuild_bl (aux,assoc) bl typ = else let captured_nal,non_captured_nal = List.chop lnal' nal in let nassoc = make_assoc assoc nal' captured_nal in - let assum = LocalRawAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't) in + let assum = CLocalAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't) in rebuild_nal ((assum :: aux), nassoc) bk bl' non_captured_nal (lnal - lnal') (CProdN(Loc.ghost,rest,typ')) | _ -> assert false @@ -741,8 +743,8 @@ let rec add_args id new_args b = CLambdaN(loc, List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, add_args id new_args b1) - | CLetIn(loc,na,b1,b2) -> - CLetIn(loc,na,add_args id new_args b1,add_args id new_args b2) + | CLetIn(loc,na,b1,t,b2) -> + CLetIn(loc,na,add_args id new_args b1,Option.map (add_args id new_args) t,add_args id new_args b2) | CAppExpl(loc,(pf,r,us),exprl) -> begin match r with @@ -828,7 +830,7 @@ let rec chop_n_arrow n t = | _ -> anomaly (Pp.str "Not enough products") -let rec get_args b t : Constrexpr.local_binder list * +let rec get_args b t : Constrexpr.local_binder_expr list * Constrexpr.constr_expr * Constrexpr.constr_expr = match b with | Constrexpr.CLambdaN (loc, (nal_ta), b') -> @@ -839,7 +841,7 @@ let rec get_args b t : Constrexpr.local_binder list * in let nal_tas,b'',t'' = get_args b' (chop_n_arrow n t) in (List.map (fun (nal,k,ta) -> - (Constrexpr.LocalRawAssum (nal,k,ta))) nal_ta)@nal_tas, b'',t'' + (Constrexpr.CLocalAssum (nal,k,ta))) nal_ta)@nal_tas, b'',t'' end | _ -> [],b,t @@ -880,13 +882,13 @@ let make_graph (f_ref:global_reference) = List.flatten (List.map (function - | Constrexpr.LocalRawDef (na,_)-> [] - | Constrexpr.LocalRawAssum (nal,_,_) -> + | Constrexpr.CLocalDef (na,_,_)-> [] + | Constrexpr.CLocalAssum (nal,_,_) -> List.map (fun (loc,n) -> CRef(Libnames.Ident(loc, Nameops.out_name n),None)) nal - | Constrexpr.LocalPattern _ -> assert false + | Constrexpr.CLocalPattern _ -> assert false ) nal_tas ) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 2889d8d03..20da12f39 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -70,8 +70,8 @@ let chop_rlambda_n = then List.rev acc,rt else match rt with - | Glob_term.GLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b - | Glob_term.GLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b + | Glob_term.GLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,None)::acc) (n-1) b + | Glob_term.GLetIn(_,name,v,t,b) -> chop_lambda_n ((name,v,t)::acc) (n-1) b | _ -> raise (CErrors.UserError(Some "chop_rlambda_n", str "chop_rlambda_n: Not enough Lambdas")) diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 5836d6519..5c3e73e9d 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -34,7 +34,7 @@ val list_add_set_eq : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list val chop_rlambda_n : int -> Glob_term.glob_constr -> - (Name.t*Glob_term.glob_constr*bool) list * Glob_term.glob_constr + (Name.t*Glob_term.glob_constr*Glob_term.glob_constr option) list * Glob_term.glob_constr val chop_rprod_n : int -> Glob_term.glob_constr -> (Name.t*Glob_term.glob_constr) list * Glob_term.glob_constr diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index c0298d06c..f1ca57585 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -512,14 +512,14 @@ let rec merge_app c1 c2 id1 id2 shift filter_shift_stable = let args = filter_shift_stable lnk (arr1 @ arr2) in GApp (Loc.ghost,GVar (Loc.ghost,shift.ident) , args) | GApp(_,f1, arr1), GApp(_,f2,arr2) -> raise NoMerge - | GLetIn(_,nme,bdy,trm) , _ -> + | GLetIn(_,nme,bdy,typ,trm) , _ -> let _ = prstr "\nICI2!\n" in let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in - GLetIn(Loc.ghost,nme,bdy,newtrm) - | _, GLetIn(_,nme,bdy,trm) -> + GLetIn(Loc.ghost,nme,bdy,typ,newtrm) + | _, GLetIn(_,nme,bdy,typ,trm) -> let _ = prstr "\nICI3!\n" in let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in - GLetIn(Loc.ghost,nme,bdy,newtrm) + GLetIn(Loc.ghost,nme,bdy,typ,newtrm) | _ -> let _ = prstr "\nICI4!\n" in raise NoMerge @@ -530,14 +530,14 @@ let rec merge_app_unsafe c1 c2 shift filter_shift_stable = let args = filter_shift_stable lnk (arr1 @ arr2) in GApp (Loc.ghost,GVar(Loc.ghost,shift.ident) , args) (* FIXME: what if the function appears in the body of the let? *) - | GLetIn(_,nme,bdy,trm) , _ -> + | GLetIn(_,nme,bdy,typ,trm) , _ -> let _ = prstr "\nICI2 '!\n" in let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in - GLetIn(Loc.ghost,nme,bdy,newtrm) - | _, GLetIn(_,nme,bdy,trm) -> + GLetIn(Loc.ghost,nme,bdy,typ,newtrm) + | _, GLetIn(_,nme,bdy,typ,trm) -> let _ = prstr "\nICI3 '!\n" in let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in - GLetIn(Loc.ghost,nme,bdy,newtrm) + GLetIn(Loc.ghost,nme,bdy,typ,newtrm) | _ -> let _ = prstr "\nICI4 '!\n" in raise NoMerge @@ -825,7 +825,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = let _ = prNamedRConstr (string_of_name nme) tp in let _ = prstr " ; " in let typ = glob_constr_to_constr_expr tp in - LocalRawAssum ([(Loc.ghost,nme)], Constrexpr_ops.default_binder_kind, typ) :: acc) + CLocalAssum ([(Loc.ghost,nme)], Constrexpr_ops.default_binder_kind, typ) :: acc) [] params in let concl = Constrextern.extern_constr false (Global.env()) Evd.empty concl in let arity,_ = diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index aab568746..fd33a779d 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -8,6 +8,8 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +DECLARE PLUGIN "ltac_plugin" + open Util open Pp open Compat diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4 index d286a5870..3e6e2db60 100644 --- a/plugins/ltac/g_obligations.ml4 +++ b/plugins/ltac/g_obligations.ml4 @@ -70,7 +70,7 @@ GEXTEND Gram Constr.closed_binder: [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in - [LocalRawAssum ([id], default_binder_kind, typ)] + [CLocalAssum ([id], default_binder_kind, typ)] ] ]; END diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index b1c4f58eb..c50100bf5 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -183,7 +183,7 @@ VERNAC COMMAND EXTEND AddRelation3 CLASSIFIED AS SIDEFF [ declare_relation a aeq n None None (Some lemma3) ] END -type binders_argtype = local_binder list +type binders_argtype = local_binder_expr list let wit_binders = (Genarg.create_arg "binders" : binders_argtype Genarg.uniform_genarg_type) diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 10fec2032..7a20838a2 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -78,17 +78,17 @@ val is_applied_rewrite_relation : env -> evar_map -> rel_context -> constr -> types option val declare_relation : - ?binders:local_binder list -> constr_expr -> constr_expr -> Id.t -> + ?binders:local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> constr_expr option -> constr_expr option -> constr_expr option -> unit val add_setoid : - bool -> local_binder list -> constr_expr -> constr_expr -> constr_expr -> + bool -> local_binder_expr list -> constr_expr -> constr_expr -> constr_expr -> Id.t -> unit val add_morphism_infer : bool -> constr_expr -> Id.t -> unit val add_morphism : - bool -> local_binder list -> constr_expr -> constr_expr -> Id.t -> unit + bool -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> unit val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 01e20d0f1..3150d6a1b 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -156,7 +156,7 @@ let mkCHole loc = CHole (loc, None, IntroAnonymous, None) let mkCLambda loc name ty t = CLambdaN (loc, [[loc, name], Default Explicit, ty], t) let mkCLetIn loc name bo t = - CLetIn (loc, (loc, name), bo, t) + CLetIn (loc, (loc, name), bo, None, t) let mkCCast loc t ty = CCast (loc,t, dC ty) (** Constructors for rawconstr *) let mkRHole = GHole (dummy_loc, InternalHole, IntroAnonymous, None) @@ -1204,7 +1204,7 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = pp(lazy(str"typed as: " ++ pr_pattern_w_ids red)); let mkXLetIn loc x (a,(g,c)) = match c with | Some b -> a,(g,Some (mkCLetIn loc x (mkCHole loc) b)) - | None -> a,(GLetIn (loc,x,(GHole (loc, BinderType x, IntroAnonymous, None)), g), None) in + | None -> a,(GLetIn (loc,x,(GHole (loc, BinderType x, IntroAnonymous, None)), None, g), None) in match red with | T t -> let sigma, t = interp_term ist gl t in sigma, T t | In_T t -> let sigma, t = interp_term ist gl t in sigma, In_T t diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 30b83cf88..efe03bc2e 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -275,7 +275,11 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels sorec ((na1,na2,c2)::ctx) (EConstr.push_rel (LocalAssum (na2,c2)) env) (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2 - | PLetIn (na1,c1,d1), LetIn(na2,c2,t2,d2) -> + | PLetIn (na1,c1,Some t1,d1), LetIn(na2,c2,t2,d2) -> + sorec ((na1,na2,t2)::ctx) (EConstr.push_rel (LocalDef (na2,c2,t2)) env) + (add_binders na1 na2 binding_vars (sorec ctx env (sorec ctx env subst c1 c2) t1 t2)) d1 d2 + + | PLetIn (na1,c1,None,d1), LetIn(na2,c2,t2,d2) -> sorec ((na1,na2,t2)::ctx) (EConstr.push_rel (LocalDef (na2,c2,t2)) env) (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2 diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index e4d7ab38d..38e71b1f9 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -334,7 +334,7 @@ let extract_nondep_branches test c b l = match r,l with | r, [] -> r | GLambda (_,_,_,_,t), false::l -> strip l t - | GLetIn (_,_,_,t), true::l -> strip l t + | GLetIn (_,_,_,_,t), true::l -> strip l t (* FIXME: do we need adjustment? *) | _,_ -> assert false in if test c l then Some (strip l b) else None @@ -344,7 +344,7 @@ let it_destRLambda_or_LetIn_names l c = match c, l with | _, [] -> (List.rev nal,c) | GLambda (_,na,_,_,c), false::l -> aux l (na::nal) c - | GLetIn (_,na,_,c), true::l -> aux l (na::nal) c + | GLetIn (_,na,_,_,c), true::l -> aux l (na::nal) c | _, true::l -> (* let-expansion *) aux l (Anonymous :: nal) c | _, false::l -> (* eta-expansion *) @@ -696,9 +696,8 @@ and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c = let c = detype (lax,false) avoid env sigma (Option.get body) in (* Heuristic: we display the type if in Prop *) let s = try Retyping.get_sort_family_of (snd env) sigma ty with _ when !Flags.in_debugger || !Flags.in_toplevel -> InType (* Can fail because of sigma missing in debugger *) in - let c = if s != InProp then c else - GCast (dl, c, CastConv (detype (lax,false) avoid env sigma ty)) in - GLetIn (dl, na', c, r) + let t = if s != InProp then None else Some (detype (lax,false) avoid env sigma ty) in + GLetIn (dl, na', c, t, r) let detype_rel_context ?(lax=false) where avoid env sigma sign = let where = Option.map (fun c -> EConstr.it_mkLambda_or_LetIn c sign) where in @@ -771,9 +770,9 @@ let detype_closed_glob ?lax isgoal avoid env sigma t = | GProd (loc,id,k,t,c) -> let id = convert_name cl id in GProd(loc,id,k,detype_closed_glob cl t, detype_closed_glob cl c) - | GLetIn (loc,id,b,e) -> + | GLetIn (loc,id,b,t,e) -> let id = convert_name cl id in - GLetIn(loc,id,detype_closed_glob cl b, detype_closed_glob cl e) + GLetIn(loc,id,detype_closed_glob cl b, Option.map (detype_closed_glob cl) t, detype_closed_glob cl e) | GLetTuple (loc,ids,(n,r),b,e) -> let ids = List.map (convert_name cl) ids in let n = convert_name cl n in @@ -832,10 +831,12 @@ let rec subst_glob_constr subst raw = if r1' == r1 && r2' == r2 then raw else GProd (loc,n,bk,r1',r2') - | GLetIn (loc,n,r1,r2) -> - let r1' = subst_glob_constr subst r1 and r2' = subst_glob_constr subst r2 in - if r1' == r1 && r2' == r2 then raw else - GLetIn (loc,n,r1',r2') + | GLetIn (loc,n,r1,t,r2) -> + let r1' = subst_glob_constr subst r1 in + let t' = Option.smartmap (subst_glob_constr subst) t in + let r2' = subst_glob_constr subst r2 in + if r1' == r1 && t == t' && r2' == r2 then raw else + GLetIn (loc,n,r1',t',r2') | GCases (loc,sty,rtno,rl,branches) -> let rtno' = Option.smartmap (subst_glob_constr subst) rtno diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 51660818f..ebbfa195f 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -77,8 +77,8 @@ let rec glob_constr_eq c1 c2 = match c1, c2 with | GProd (_, na1, bk1, t1, c1), GProd (_, na2, bk2, t2, c2) -> Name.equal na1 na2 && binding_kind_eq bk1 bk2 && glob_constr_eq t1 t2 && glob_constr_eq c1 c2 -| GLetIn (_, na1, t1, c1), GLetIn (_, na2, t2, c2) -> - Name.equal na1 na2 && glob_constr_eq t1 t2 && glob_constr_eq c1 c2 +| GLetIn (_, na1, b1, t1, c1), GLetIn (_, na2, b2, t2, c2) -> + Name.equal na1 na2 && glob_constr_eq b1 b2 && Option.equal glob_constr_eq t1 t2 && glob_constr_eq c1 c2 | GCases (_, st1, c1, tp1, cl1), GCases (_, st2, c2, tp2, cl2) -> case_style_eq st1 st2 && Option.equal glob_constr_eq c1 c2 && List.equal tomatch_tuple_eq tp1 tp2 && @@ -152,10 +152,11 @@ let map_glob_constr_left_to_right f = function let comp1 = f ty in let comp2 = f c in GProd (loc,na,bk,comp1,comp2) - | GLetIn (loc,na,b,c) -> + | GLetIn (loc,na,b,t,c) -> let comp1 = f b in + let compt = Option.map f t in let comp2 = f c in - GLetIn (loc,na,comp1,comp2) + GLetIn (loc,na,comp1,compt,comp2) | GCases (loc,sty,rtntypopt,tml,pl) -> let comp1 = Option.map f rtntypopt in let comp2 = Util.List.map_left (fun (tm,x) -> (f tm,x)) tml in @@ -189,8 +190,10 @@ let fold_return_type f acc (na,tyopt) = Option.fold_left f acc tyopt let fold_glob_constr f acc = function | GVar _ -> acc | GApp (_,c,args) -> List.fold_left f (f acc c) args - | GLambda (_,_,_,b,c) | GProd (_,_,_,b,c) | GLetIn (_,_,b,c) -> + | GLambda (_,_,_,b,c) | GProd (_,_,_,b,c) -> f (f acc b) c + | GLetIn (_,_,b,t,c) -> + f (Option.fold_left f (f acc b) t) c | GCases (_,_,rtntypopt,tml,pl) -> let fold_pattern acc (_,idl,p,c) = f acc c in List.fold_left fold_pattern @@ -225,8 +228,8 @@ let occur_glob_constr id = (occur ty) || (not (same_id na id) && (occur c)) | GProd (loc,na,bk,ty,c) -> (occur ty) || (not (same_id na id) && (occur c)) - | GLetIn (loc,na,b,c) -> - (occur b) || (not (same_id na id) && (occur c)) + | GLetIn (loc,na,b,t,c) -> + (Option.fold_left (fun b t -> occur t || b) (occur b) t) || (not (same_id na id) && (occur c)) | GCases (loc,sty,rtntypopt,tml,pl) -> (occur_option rtntypopt) || (List.exists (fun (tm,_) -> occur tm) tml) @@ -270,10 +273,15 @@ let free_glob_vars = let rec vars bounded vs = function | GVar (loc,id') -> if Id.Set.mem id' bounded then vs else Id.Set.add id' vs | GApp (loc,f,args) -> List.fold_left (vars bounded) vs (f::args) - | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) | GLetIn (loc,na,ty,c) -> + | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) -> let vs' = vars bounded vs ty in let bounded' = add_name_to_ids bounded na in vars bounded' vs' c + | GLetIn (loc,na,b,ty,c) -> + let vs' = vars bounded vs b in + let vs'' = Option.fold_left (vars bounded) vs' ty in + let bounded' = add_name_to_ids bounded na in + vars bounded' vs'' c | GCases (loc,sty,rtntypopt,tml,pl) -> let vs1 = vars_option bounded vs rtntypopt in let vs2 = List.fold_left (fun vs (tm,_) -> vars bounded vs tm) vs1 tml in @@ -346,7 +354,7 @@ let add_and_check_ident id set = let bound_glob_vars = let rec vars bound = function - | GLambda (_,na,_,_,_) | GProd (_,na,_,_,_) | GLetIn (_,na,_,_) as c -> + | GLambda (_,na,_,_,_) | GProd (_,na,_,_,_) | GLetIn (_,na,_,_,_) as c -> let bound = name_fold add_and_check_ident na bound in fold_glob_constr vars bound c | GCases (loc,sty,rtntypopt,tml,pl) -> @@ -460,7 +468,7 @@ let loc_of_glob_constr = function | GApp (loc,_,_) -> loc | GLambda (loc,_,_,_,_) -> loc | GProd (loc,_,_,_,_) -> loc - | GLetIn (loc,_,_,_) -> loc + | GLetIn (loc,_,_,_,_) -> loc | GCases (loc,_,_,_,_) -> loc | GLetTuple (loc,_,_,_,_) -> loc | GIf (loc,_,_,_,_) -> loc @@ -512,9 +520,9 @@ let rec rename_glob_vars l = function | GLambda (loc,na,bk,t,c) -> let na',l' = update_subst na l in GLambda (loc,na',bk,rename_glob_vars l t,rename_glob_vars l' c) - | GLetIn (loc,na,b,c) -> + | GLetIn (loc,na,b,t,c) -> let na',l' = update_subst na l in - GLetIn (loc,na',rename_glob_vars l b,rename_glob_vars l' c) + GLetIn (loc,na',rename_glob_vars l b,Option.map (rename_glob_vars l) t,rename_glob_vars l' c) (* Lazy strategy: we fail if a collision with renaming occurs, rather than renaming further *) | GCases (loc,ci,po,tomatchl,cls) -> let test_pred_pat (na,ino) = diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index d6a7c5192..318f94be2 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -44,8 +44,9 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with Name.equal v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2 | PProd (v1, t1, b1), PProd (v2, t2, b2) -> Name.equal v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2 -| PLetIn (v1, t1, b1), PLetIn (v2, t2, b2) -> - Name.equal v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2 +| PLetIn (v1, b1, t1, c1), PLetIn (v2, b2, t2, c2) -> + Name.equal v1 v2 && constr_pattern_eq b1 b2 && + Option.equal constr_pattern_eq t1 t2 && constr_pattern_eq c1 c2 | PSort s1, PSort s2 -> Miscops.glob_sort_eq s1 s2 | PMeta m1, PMeta m2 -> Option.equal Id.equal m1 m2 | PIf (t1, l1, r1), PIf (t2, l2, r2) -> @@ -85,7 +86,8 @@ let rec occur_meta_pattern = function | PProj (_,arg) -> occur_meta_pattern arg | PLambda (na,t,c) -> (occur_meta_pattern t) || (occur_meta_pattern c) | PProd (na,t,c) -> (occur_meta_pattern t) || (occur_meta_pattern c) - | PLetIn (na,t,c) -> (occur_meta_pattern t) || (occur_meta_pattern c) + | PLetIn (na,b,t,c) -> + Option.fold_left (fun b t -> b || occur_meta_pattern t) (occur_meta_pattern b) t || (occur_meta_pattern c) | PIf (c,c1,c2) -> (occur_meta_pattern c) || (occur_meta_pattern c1) || (occur_meta_pattern c2) @@ -101,7 +103,7 @@ exception BoundPattern;; let rec head_pattern_bound t = match t with | PProd (_,_,b) -> head_pattern_bound b - | PLetIn (_,_,b) -> head_pattern_bound b + | PLetIn (_,_,_,b) -> head_pattern_bound b | PApp (c,args) -> head_pattern_bound c | PIf (c,_,_) -> head_pattern_bound c | PCase (_,p,c,br) -> head_pattern_bound c @@ -132,7 +134,7 @@ let pattern_of_constr env sigma t = | Sort (Prop Pos) -> PSort GSet | Sort (Type _) -> PSort (GType []) | Cast (c,_,_) -> pattern_of_constr env c - | LetIn (na,c,t,b) -> PLetIn (na,pattern_of_constr env c, + | LetIn (na,c,t,b) -> PLetIn (na,pattern_of_constr env c,Some (pattern_of_constr env t), pattern_of_constr (push_rel (LocalDef (na,c,t)) env) b) | Prod (na,c,b) -> PProd (na,pattern_of_constr env c, pattern_of_constr (push_rel (LocalAssum (na, c)) env) b) @@ -185,7 +187,7 @@ let map_pattern_with_binders g f l = function | PSoApp (n,pl) -> PSoApp (n, List.map (f l) pl) | PLambda (n,a,b) -> PLambda (n,f l a,f (g n l) b) | PProd (n,a,b) -> PProd (n,f l a,f (g n l) b) - | PLetIn (n,a,b) -> PLetIn (n,f l a,f (g n l) b) + | PLetIn (n,a,t,b) -> PLetIn (n,f l a,Option.map (f l) t,f (g n l) b) | PIf (c,b1,b2) -> PIf (f l c,f l b1,f l b2) | PCase (ci,po,p,pl) -> PCase (ci,f l po,f l p, List.map (fun (i,n,c) -> (i,n,f l c)) pl) @@ -272,11 +274,12 @@ let rec subst_pattern subst pat = let c2' = subst_pattern subst c2 in if c1' == c1 && c2' == c2 then pat else PProd (name,c1',c2') - | PLetIn (name,c1,c2) -> + | PLetIn (name,c1,t,c2) -> let c1' = subst_pattern subst c1 in + let t' = Option.smartmap (subst_pattern subst) t in let c2' = subst_pattern subst c2 in - if c1' == c1 && c2' == c2 then pat else - PLetIn (name,c1',c2') + if c1' == c1 && t' == t && c2' == c2 then pat else + PLetIn (name,c1',t',c2') | PSort _ | PMeta _ -> pat | PIf (c,c1,c2) -> @@ -341,9 +344,10 @@ let rec pat_of_raw metas vars = function name_iter (fun n -> metas := n::!metas) na; PProd (na, pat_of_raw metas vars c1, pat_of_raw metas (na::vars) c2) - | GLetIn (_,na,c1,c2) -> + | GLetIn (_,na,c1,t,c2) -> name_iter (fun n -> metas := n::!metas) na; PLetIn (na, pat_of_raw metas vars c1, + Option.map (pat_of_raw metas vars) t, pat_of_raw metas (na::vars) c2) | GSort (_,s) -> PSort s diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index c673851c8..4a73a9e0c 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -812,14 +812,14 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre iraise (e, info) in inh_conv_coerce_to_tycon loc env evdref resj tycon - | GLetIn(loc,name,c1,c2) -> - let j = - match c1 with - | GCast (loc, c, CastConv t) -> - let tj = pretype_type empty_valcon env evdref lvar t in - pretype (mk_tycon tj.utj_val) env evdref lvar c - | _ -> pretype empty_tycon env evdref lvar c1 - in + | GLetIn(loc,name,c1,t,c2) -> + let tycon1 = + match t with + | Some t -> + mk_tycon (pretype_type empty_valcon env evdref lvar t).utj_val + | None -> + empty_tycon in + let j = pretype tycon1 env evdref lvar c1 in let t = evd_comb1 (Evarsolve.refresh_universes ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env) evdref j.uj_type in diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index d92d83275..38eeda9b9 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -317,9 +317,9 @@ let tag_var = tag Tag.variable pr_sep_com spc (pr ltop) rhs)) let begin_of_binder = function - LocalRawDef((loc,_),_) -> fst (Loc.unloc loc) - | LocalRawAssum((loc,_)::_,_,_) -> fst (Loc.unloc loc) - | LocalPattern(loc,_,_) -> fst (Loc.unloc loc) + | CLocalDef((loc,_),_,_) -> fst (Loc.unloc loc) + | CLocalAssum((loc,_)::_,_,_) -> fst (Loc.unloc loc) + | CLocalPattern(loc,_,_) -> fst (Loc.unloc loc) | _ -> assert false let begin_of_binders = function @@ -360,15 +360,13 @@ let tag_var = tag Tag.variable hov 1 (if many then surround_impl b s else surround_implicit b s) let pr_binder_among_many pr_c = function - | LocalRawAssum (nal,k,t) -> + | CLocalAssum (nal,k,t) -> pr_binder true pr_c (nal,k,t) - | LocalRawDef (na,c) -> - let c,topt = match c with - | CCast(_,c, (CastConv t|CastVM t|CastNative t)) -> c, t - | _ -> c, CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) in - surround (pr_lname na ++ pr_opt_type pr_c topt ++ - str":=" ++ cut() ++ pr_c c) - | LocalPattern (loc,p,tyo) -> + | CLocalDef (na,c,topt) -> + surround (pr_lname na ++ + pr_opt_no_spc (fun t -> str " :" ++ ws 1 ++ pr_c t) topt ++ + str" :=" ++ spc() ++ pr_c c) + | CLocalPattern (loc,p,tyo) -> let p = pr_patt lsimplepatt p in match tyo with | None -> @@ -382,9 +380,9 @@ let tag_var = tag Tag.variable let pr_delimited_binders kw sep pr_c bl = let n = begin_of_binders bl in match bl with - | [LocalRawAssum (nal,k,t)] -> + | [CLocalAssum (nal,k,t)] -> kw n ++ pr_binder false pr_c (nal,k,t) - | (LocalRawAssum _ | LocalPattern _) :: _ as bdl -> + | (CLocalAssum _ | CLocalPattern _) :: _ as bdl -> kw n ++ pr_undelimited_binders sep pr_c bdl | _ -> assert false @@ -395,33 +393,33 @@ let tag_var = tag Tag.variable let rec extract_prod_binders = function (* | CLetIn (loc,na,b,c) as x -> let bl,c = extract_prod_binders c in - if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*) + if bl = [] then [], x else CLocalDef (na,b) :: bl, c*) | CProdN (loc,[],c) -> extract_prod_binders c | CProdN (loc,[[_,Name id],bk,t], CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)])) when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) -> let bl,c = extract_prod_binders b in - LocalPattern (loc,p,None) :: bl, c + CLocalPattern (loc,p,None) :: bl, c | CProdN (loc,(nal,bk,t)::bl,c) -> let bl,c = extract_prod_binders (CProdN(loc,bl,c)) in - LocalRawAssum (nal,bk,t) :: bl, c + CLocalAssum (nal,bk,t) :: bl, c | c -> [], c let rec extract_lam_binders = function (* | CLetIn (loc,na,b,c) as x -> let bl,c = extract_lam_binders c in - if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*) + if bl = [] then [], x else CLocalDef (na,b) :: bl, c*) | CLambdaN (loc,[],c) -> extract_lam_binders c | CLambdaN (loc,[[_,Name id],bk,t], CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)])) when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) -> let bl,c = extract_lam_binders b in - LocalPattern (loc,p,None) :: bl, c + CLocalPattern (loc,p,None) :: bl, c | CLambdaN (loc,(nal,bk,t)::bl,c) -> let bl,c = extract_lam_binders (CLambdaN(loc,bl,c)) in - LocalRawAssum (nal,bk,t) :: bl, c + CLocalAssum (nal,bk,t) :: bl, c | c -> [], c let split_lambda = function @@ -450,7 +448,7 @@ let tag_var = tag Tag.variable let (na,_,def) = split_lambda def in let (na,t,typ) = split_product na typ in let (bl,typ,def) = split_fix (n-1) typ def in - (LocalRawAssum ([na],default_binder_kind,t)::bl,typ,def) + (CLocalAssum ([na],default_binder_kind,t)::bl,typ,def) let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c = let pr_body = @@ -467,9 +465,9 @@ let tag_var = tag Tag.variable match (ro : Constrexpr.recursion_order_expr) with | CStructRec -> let names_of_binder = function - | LocalRawAssum (nal,_,_) -> nal - | LocalRawDef (_,_) -> [] - | LocalPattern _ -> assert false + | CLocalAssum (nal,_,_) -> nal + | CLocalDef (_,_,_) -> [] + | CLocalPattern _ -> assert false in let ids = List.flatten (List.map names_of_binder bl) in if List.length ids > 1 then spc() ++ str "{" ++ keyword "struct" ++ spc () ++ pr_id id ++ str"}" @@ -588,7 +586,7 @@ let tag_var = tag Tag.variable pr_fun_sep ++ pr spc ltop a), llambda ) - | CLetIn (_,(_,Name x),(CFix(_,(_,x'),[_])|CCoFix(_,(_,x'),[_]) as fx), b) + | CLetIn (_,(_,Name x),(CFix(_,(_,x'),[_])|CCoFix(_,(_,x'),[_]) as fx), t, b) when Id.equal x x' -> return ( hv 0 ( @@ -598,11 +596,12 @@ let tag_var = tag Tag.variable pr spc ltop b), lletin ) - | CLetIn (_,x,a,b) -> + | CLetIn (_,x,a,t,b) -> return ( hv 0 ( - hov 2 (keyword "let" ++ spc () ++ pr_lname x ++ str " :=" - ++ pr spc ltop a ++ spc () + hov 2 (keyword "let" ++ spc () ++ pr_lname x + ++ pr_opt_no_spc (fun t -> str " :" ++ ws 1 ++ pr mt ltop t) t + ++ str " :=" ++ pr spc ltop a ++ spc () ++ keyword "in") ++ pr spc ltop b), lletin @@ -703,7 +702,7 @@ let tag_var = tag Tag.variable | CEvar (_,n,l) -> return (pr_evar (pr mt) n l, latom) | CPatVar (_,p) -> - return (str "?" ++ pr_patvar p, latom) + return (str "@?" ++ pr_patvar p, latom) | CSort (_,s) -> return (pr_glob_sort s, latom) | CCast (_,a,b) -> diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index a0106837a..f92caf426 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -19,12 +19,12 @@ open Names open Misctypes val extract_lam_binders : - constr_expr -> local_binder list * constr_expr + constr_expr -> local_binder_expr list * constr_expr val extract_prod_binders : - constr_expr -> local_binder list * constr_expr + constr_expr -> local_binder_expr list * constr_expr val split_fix : int -> constr_expr -> constr_expr -> - local_binder list * constr_expr * constr_expr + local_binder_expr list * constr_expr * constr_expr val prec_less : int -> int * Ppextend.parenRelation -> bool @@ -50,12 +50,12 @@ val pr_patvar : patvar -> std_ppcmds val pr_glob_level : glob_level -> std_ppcmds val pr_glob_sort : glob_sort -> std_ppcmds val pr_guard_annot : (constr_expr -> std_ppcmds) -> - local_binder list -> + local_binder_expr list -> ('a * Names.Id.t) option * recursion_order_expr -> std_ppcmds val pr_record_body : (reference * constr_expr) list -> std_ppcmds -val pr_binders : local_binder list -> std_ppcmds +val pr_binders : local_binder_expr list -> std_ppcmds val pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds val pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds val pr_constr_expr : constr_expr -> std_ppcmds diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 78ef4d4ba..cfc2e48d1 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -534,18 +534,8 @@ open Decl_kinds (* Stm *) | VernacStm JoinDocument -> return (keyword "Stm JoinDocument") - | VernacStm PrintDag -> - return (keyword "Stm PrintDag") - | VernacStm Finish -> - return (keyword "Stm Finish") | VernacStm Wait -> return (keyword "Stm Wait") - | VernacStm (Observe id) -> - return (keyword "Stm Observe " ++ str(Stateid.to_string id)) - | VernacStm (Command v) -> - return (keyword "Stm Command " ++ pr_vernac_body v) - | VernacStm (PGLast v) -> - return (keyword "Stm PGLast " ++ pr_vernac_body v) (* Proof management *) | VernacAbortAll -> diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 2fc8bc82d..aa422e36a 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -205,6 +205,11 @@ let print_opacity ref = str "transparent (with minimal expansion weight)"] (*******************) + +let print_if_is_coercion ref = + if Classops.coercion_exists ref then [pr_global ref ++ str " is a coercion"] else [] + +(*******************) (* *) let print_polymorphism ref = @@ -258,7 +263,8 @@ let print_name_infos ref = type_info_for_implicit @ print_renames_list (mt()) renames @ print_impargs_list (mt()) impls @ - print_argument_scopes (mt()) scopes + print_argument_scopes (mt()) scopes @ + print_if_is_coercion ref let print_id_args_data test pr id l = if List.exists test l then diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml index f51586c73..2c489d6de 100644 --- a/proofs/proof_using.ml +++ b/proofs/proof_using.ml @@ -108,7 +108,7 @@ let remove_ids_and_lets env s ids = let suggest_Proof_using name env vars ids_typ context_ids = let module S = Id.Set in let open Pp in - let print x = Feedback.msg_error x in + let print x = Feedback.msg_debug x in let pr_set parens s = let wrap ppcmds = if parens && S.cardinal s > 1 then str "(" ++ ppcmds ++ str ")" diff --git a/stm/stm.ml b/stm/stm.ml index b8a406430..2b6ee5511 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2235,10 +2235,13 @@ let known_state ?(redefine_qed=false) ~cache id = if eff then update_global_env () ), (if eff then `Yes else cache), true | `Cmd { cast = x; ceff = eff } -> (fun () -> - resilient_command reach view.next; - stm_vernac_interp id x; - if eff then update_global_env () - ), (if eff then `Yes else cache), true + (match !Flags.async_proofs_mode with + | Flags.APon | Flags.APonLazy -> + resilient_command reach view.next + | Flags.APoff -> reach view.next); + stm_vernac_interp id x; + if eff then update_global_env () + ), (if eff then `Yes else cache), true | `Fork ((x,_,_,_), None) -> (fun () -> resilient_command reach view.next; stm_vernac_interp id x; @@ -2528,20 +2531,12 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty stm_prerr_endline (fun () -> " classified as: " ^ string_of_vernac_classification c); match c with - (* PG stuff *) - | VtStm(VtPG,false), VtNow -> stm_vernac_interp Stateid.dummy x; `Ok - | VtStm(VtPG,_), _ -> anomaly(str "PG command in script or VtLater") (* Joining various parts of the document *) | VtStm (VtJoinDocument, b), VtNow -> join (); `Ok - | VtStm (VtFinish, b), VtNow -> finish (); `Ok - | VtStm (VtWait, b), VtNow -> finish (); wait (); `Ok - | VtStm (VtPrintDag, b), VtNow -> - VCS.print ~now:true (); `Ok - | VtStm (VtObserve id, b), VtNow -> observe id; `Ok - | VtStm ((VtObserve _ | VtFinish | VtJoinDocument - |VtPrintDag |VtWait),_), VtLater -> + | VtStm (VtWait, b), VtNow -> finish (); wait (); `Ok + | VtStm ((VtJoinDocument|VtWait),_), VtLater -> anomaly(str"classifier: join actions cannot be classified as VtLater") - + (* Back *) | VtStm (VtBack oid, true), w -> let id = VCS.new_node ~id:newtip () in @@ -2704,15 +2699,6 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty | VtUnknown, VtLater -> anomaly(str"classifier: VtUnknown must imply VtNow") end in - (* Proof General *) - begin match expr with - | VernacStm (PGLast _) -> - if not (VCS.Branch.equal head VCS.Branch.master) then - stm_vernac_interp Stateid.dummy - { verbose = true; loc = Loc.ghost; indentation = 0; strlen = 0; - expr = VernacShow (ShowGoal OpenSubgoals) } - | _ -> () - end; stm_prerr_endline (fun () -> "processed }}}"); VCS.print (); rc diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index dc5be08a3..5908c09d0 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -33,9 +33,7 @@ let string_of_vernac_type = function | VtQuery (b,(id,route)) -> "Query " ^ string_of_in_script b ^ " report " ^ Stateid.to_string id ^ " route " ^ string_of_int route - | VtStm ((VtFinish|VtJoinDocument|VtObserve _|VtPrintDag|VtWait), b) -> - "Stm " ^ string_of_in_script b - | VtStm (VtPG, b) -> "Stm PG " ^ string_of_in_script b + | VtStm ((VtJoinDocument|VtWait), b) -> "Stm " ^ string_of_in_script b | VtStm (VtBack _, b) -> "Stm Back " ^ string_of_in_script b let string_of_vernac_when = function @@ -52,12 +50,6 @@ let declare_vernac_classifier = classifiers := !classifiers @ [s,f] -let elide_part_of_script_and_now (a, _) = - match a with - | VtQuery (_,id) -> VtQuery (false,id), VtNow - | VtStm (x, _) -> VtStm (x, false), VtNow - | x -> x, VtNow - let make_polymorphic (a, b as x) = match a with | VtStartProof (x, _, ids) -> @@ -69,23 +61,14 @@ let set_undo_classifier f = undo_classifier := f let rec classify_vernac e = let static_classifier e = match e with - (* PG compatibility *) - | VernacUnsetOption (["Silent"]|["Undo"]|["Printing";"Depth"]) - | VernacSetOption ((["Silent"]|["Undo"]|["Printing";"Depth"]),_) - when !Flags.print_emacs -> VtStm(VtPG,false), VtNow (* Univ poly compatibility: we run it now, so that we can just * look at Flags in stm.ml. Would be nicer to have the stm * look at the entire dag to detect this option. *) | VernacSetOption (["Universe"; "Polymorphism"],_) | VernacUnsetOption (["Universe"; "Polymorphism"]) -> VtSideff [], VtNow (* Stm *) - | VernacStm Finish -> VtStm (VtFinish, true), VtNow - | VernacStm Wait -> VtStm (VtWait, true), VtNow + | VernacStm Wait -> VtStm (VtWait, true), VtNow | VernacStm JoinDocument -> VtStm (VtJoinDocument, true), VtNow - | VernacStm PrintDag -> VtStm (VtPrintDag, true), VtNow - | VernacStm (Observe id) -> VtStm (VtObserve id, true), VtNow - | VernacStm (Command x) -> elide_part_of_script_and_now (classify_vernac x) - | VernacStm (PGLast x) -> fst (classify_vernac x), VtNow (* Nested vernac exprs *) | VernacProgram e -> classify_vernac e | VernacLocal (_,e) -> classify_vernac e diff --git a/test-suite/bugs/closed/4957.v b/test-suite/bugs/closed/4957.v new file mode 100644 index 000000000..0efd87ac0 --- /dev/null +++ b/test-suite/bugs/closed/4957.v @@ -0,0 +1,6 @@ +Ltac get_value H := eval cbv delta [H] in H. + +Goal True. +refine (let X := _ in _). +let e := get_value X in unify e Prop. +Abort. diff --git a/test-suite/output/ErrorInModule.out b/test-suite/output/ErrorInModule.out new file mode 100644 index 000000000..851ecd930 --- /dev/null +++ b/test-suite/output/ErrorInModule.out @@ -0,0 +1,2 @@ +File "stdin", line 3, characters 20-31: +Error: The reference nonexistent was not found in the current environment. diff --git a/test-suite/output/ErrorInModule.v b/test-suite/output/ErrorInModule.v new file mode 100644 index 000000000..e69e23276 --- /dev/null +++ b/test-suite/output/ErrorInModule.v @@ -0,0 +1,4 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-quick") -*- *) +Module M. + Definition foo := nonexistent. +End M. diff --git a/test-suite/output/ErrorInSection.out b/test-suite/output/ErrorInSection.out new file mode 100644 index 000000000..851ecd930 --- /dev/null +++ b/test-suite/output/ErrorInSection.out @@ -0,0 +1,2 @@ +File "stdin", line 3, characters 20-31: +Error: The reference nonexistent was not found in the current environment. diff --git a/test-suite/output/ErrorInSection.v b/test-suite/output/ErrorInSection.v new file mode 100644 index 000000000..3036f8f05 --- /dev/null +++ b/test-suite/output/ErrorInSection.v @@ -0,0 +1,4 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-quick") -*- *) +Section S. + Definition foo := nonexistent. +End S. diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index ad60aeccc..1ec701ae8 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -32,7 +32,7 @@ let d := 2 in ∃ z : nat, let e := 3 in let f := 4 in x + y = z + d : Type -> Prop λ A : Type, ∀ n p : A, n = p : Type -> Prop -let' f (x y : nat) (a:=0) (z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2 +let' f (x y : nat) (a := 0) (z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2 : bool -> nat λ (f : nat -> nat) (x : nat), f(x) + S(x) : (nat -> nat) -> nat -> nat diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out new file mode 100644 index 000000000..128bc7767 --- /dev/null +++ b/test-suite/output/UnivBinders.out @@ -0,0 +1,6 @@ +bar@{u} = nat + : Wrap@{u} Set +(* u |= Set < u + *) + +bar is universe polymorphic diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v new file mode 100644 index 000000000..d9e89e43c --- /dev/null +++ b/test-suite/output/UnivBinders.v @@ -0,0 +1,7 @@ +Set Universe Polymorphism. +Set Printing Universes. + +Class Wrap A := wrap : A. + +Instance bar@{u} : Wrap@{u} Set. Proof nat. +Print bar. diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out index c0eede99e..c70467912 100644 --- a/test-suite/output/inference.out +++ b/test-suite/output/inference.out @@ -6,7 +6,7 @@ fun e : option L => match e with : option L -> option L fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H : forall m n p : nat, S m <= S n + p -> m <= n + p -fun n : nat => let x := A n : T n in ?t ?y : T n +fun n : nat => let x : T n := A n in ?t ?y : T n : forall n : nat, T n where ?t : [n : nat x := A n : T n |- ?T -> T n] diff --git a/test-suite/success/univnames.v b/test-suite/success/univnames.v index 048b53d26..fe3b8c1d7 100644 --- a/test-suite/success/univnames.v +++ b/test-suite/success/univnames.v @@ -21,6 +21,17 @@ Inductive bla@{l k} : Type@{k} := blaI : Type@{l} -> bla. Inductive blacopy@{k l} : Type@{k} := blacopyI : Type@{l} -> blacopy. +Class Wrap A := wrap : A. + +Fail Instance bad@{} : Wrap Type := Type. + +Instance bad@{} : Wrap Type. +Fail Proof Type. +Abort. + +Instance bar@{u} : Wrap@{u} Set. Proof nat. + + Monomorphic Universe g. -Inductive blacopy'@{l} : Type@{g} := blacopy'I : Type@{l} -> blacopy'.
\ No newline at end of file +Inductive blacopy'@{l} : Type@{g} := blacopy'I : Type@{l} -> blacopy'. diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v index 048e409cd..5f04cf242 100644 --- a/theories/QArith/Qreals.v +++ b/theories/QArith/Qreals.v @@ -15,7 +15,8 @@ Definition Q2R (x : Q) : R := (IZR (Qnum x) * / IZR (QDen x))%R. Lemma IZR_nz : forall p : positive, IZR (Zpos p) <> 0%R. Proof. -intros; apply not_O_IZR; auto with qarith. +intros. +now apply not_O_IZR. Qed. Hint Resolve IZR_nz Rmult_integral_contrapositive. @@ -48,8 +49,7 @@ assert ((X1 * Y2)%R = (Y1 * X2)%R). apply IZR_eq; auto. clear H. field_simplify_eq; auto. -ring_simplify X1 Y2 (Y2 * X1)%R. -rewrite H0; ring. +rewrite H0; ring. Qed. Lemma Rle_Qle : forall x y : Q, (Q2R x <= Q2R y)%R -> x<=y. @@ -66,10 +66,8 @@ replace (X1 * Y2)%R with (X1 * / X2 * (X2 * Y2))%R; try (field; auto). replace (Y1 * X2)%R with (Y1 * / Y2 * (X2 * Y2))%R; try (field; auto). apply Rmult_le_compat_r; auto. apply Rmult_le_pos. -unfold X2; replace 0%R with (IZR 0); auto; apply IZR_le; - auto with zarith. -unfold Y2; replace 0%R with (IZR 0); auto; apply IZR_le; - auto with zarith. +now apply IZR_le. +now apply IZR_le. Qed. Lemma Qle_Rle : forall x y : Q, x<=y -> (Q2R x <= Q2R y)%R. @@ -88,10 +86,8 @@ replace (X1 * / X2)%R with (X1 * Y2 * (/ X2 * / Y2))%R; try (field; auto). replace (Y1 * / Y2)%R with (Y1 * X2 * (/ X2 * / Y2))%R; try (field; auto). apply Rmult_le_compat_r; auto. apply Rmult_le_pos; apply Rlt_le; apply Rinv_0_lt_compat. -unfold X2; replace 0%R with (IZR 0); auto; apply IZR_lt; red; - auto with zarith. -unfold Y2; replace 0%R with (IZR 0); auto; apply IZR_lt; red; - auto with zarith. +now apply IZR_lt. +now apply IZR_lt. Qed. Lemma Rlt_Qlt : forall x y : Q, (Q2R x < Q2R y)%R -> x<y. @@ -108,10 +104,8 @@ replace (X1 * Y2)%R with (X1 * / X2 * (X2 * Y2))%R; try (field; auto). replace (Y1 * X2)%R with (Y1 * / Y2 * (X2 * Y2))%R; try (field; auto). apply Rmult_lt_compat_r; auto. apply Rmult_lt_0_compat. -unfold X2; replace 0%R with (IZR 0); auto; apply IZR_lt; red; - auto with zarith. -unfold Y2; replace 0%R with (IZR 0); auto; apply IZR_lt; red; - auto with zarith. +now apply IZR_lt. +now apply IZR_lt. Qed. Lemma Qlt_Rlt : forall x y : Q, x<y -> (Q2R x < Q2R y)%R. @@ -130,10 +124,8 @@ replace (X1 * / X2)%R with (X1 * Y2 * (/ X2 * / Y2))%R; try (field; auto). replace (Y1 * / Y2)%R with (Y1 * X2 * (/ X2 * / Y2))%R; try (field; auto). apply Rmult_lt_compat_r; auto. apply Rmult_lt_0_compat; apply Rinv_0_lt_compat. -unfold X2; replace 0%R with (IZR 0); auto; apply IZR_lt; red; - auto with zarith. -unfold Y2; replace 0%R with (IZR 0); auto; apply IZR_lt; red; - auto with zarith. +now apply IZR_lt. +now apply IZR_lt. Qed. Lemma Q2R_plus : forall x y : Q, Q2R (x+y) = (Q2R x + Q2R y)%R. diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v index c3ab8edc5..17ffc0fe3 100644 --- a/theories/Reals/AltSeries.v +++ b/theories/Reals/AltSeries.v @@ -339,51 +339,24 @@ Proof. symmetry ; apply S_pred with 0%nat. assumption. apply Rle_lt_trans with (/ INR (2 * N)). - apply Rmult_le_reg_l with (INR (2 * N)). + apply Rinv_le_contravar. rewrite mult_INR; apply Rmult_lt_0_compat; [ simpl; prove_sup0 | apply lt_INR_0; assumption ]. - rewrite <- Rinv_r_sym. - apply Rmult_le_reg_l with (INR (2 * n)). - rewrite mult_INR; apply Rmult_lt_0_compat; - [ simpl; prove_sup0 | apply lt_INR_0; assumption ]. - rewrite (Rmult_comm (INR (2 * n))); rewrite Rmult_assoc; - rewrite <- Rinv_l_sym. - do 2 rewrite Rmult_1_r; apply le_INR. - apply (fun m n p:nat => mult_le_compat_l p n m); assumption. - replace n with (S (pred n)). - apply not_O_INR; discriminate. - symmetry ; apply S_pred with 0%nat. - assumption. - replace N with (S (pred N)). - apply not_O_INR; discriminate. - symmetry ; apply S_pred with 0%nat. - assumption. + apply le_INR. + now apply mult_le_compat_l. rewrite mult_INR. - rewrite Rinv_mult_distr. - replace (INR 2) with 2; [ idtac | reflexivity ]. - apply Rmult_lt_reg_l with 2. - prove_sup0. - rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym; [ idtac | discrR ]. - rewrite Rmult_1_l; apply Rmult_lt_reg_l with (INR N). - apply lt_INR_0; assumption. - rewrite <- Rinv_r_sym. - apply Rmult_lt_reg_l with (/ (2 * eps)). - apply Rinv_0_lt_compat; assumption. - rewrite Rmult_1_r; - replace (/ (2 * eps) * (INR N * (2 * eps))) with - (INR N * (2 * eps * / (2 * eps))); [ idtac | ring ]. - rewrite <- Rinv_r_sym. - rewrite Rmult_1_r; replace (INR N) with (IZR (Z.of_nat N)). - rewrite <- H4. - elim H1; intros; assumption. - symmetry ; apply INR_IZR_INZ. - apply prod_neq_R0; - [ discrR | red; intro; rewrite H8 in H; elim (Rlt_irrefl _ H) ]. - apply not_O_INR. - red; intro; rewrite H8 in H5; elim (lt_irrefl _ H5). - replace (INR 2) with 2; [ discrR | reflexivity ]. - apply not_O_INR. - red; intro; rewrite H8 in H5; elim (lt_irrefl _ H5). + apply Rmult_lt_reg_l with (INR N / eps). + apply Rdiv_lt_0_compat with (2 := H). + now apply (lt_INR 0). + replace (_ */ _) with (/(2 * eps)). + replace (_ / _ * _) with (INR N). + rewrite INR_IZR_INZ. + now rewrite <- H4. + field. + now apply Rgt_not_eq. + simpl (INR 2); field; split. + now apply Rgt_not_eq, (lt_INR 0). + now apply Rgt_not_eq. apply Rle_ge; apply PI_tg_pos. apply lt_le_trans with N; assumption. elim H1; intros H5 _. @@ -395,7 +368,6 @@ Proof. elim (Rlt_irrefl _ (Rlt_trans _ _ _ H6 H5)). elim (lt_n_O _ H6). apply le_IZR. - simpl. left; apply Rlt_trans with (/ (2 * eps)). apply Rinv_0_lt_compat; assumption. elim H1; intros; assumption. diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v index b14d807d2..eb4a3b804 100644 --- a/theories/Reals/Cos_plus.v +++ b/theories/Reals/Cos_plus.v @@ -289,11 +289,9 @@ Proof. apply INR_fact_lt_0. rewrite <- Rinv_r_sym. rewrite Rmult_1_r. - replace 1 with (INR 1). - apply le_INR. + apply (le_INR 1). apply lt_le_S. apply INR_lt; apply INR_fact_lt_0. - reflexivity. apply INR_fact_neq_0. apply Rmult_le_reg_l with (INR (fact (S (N + n)))). apply INR_fact_lt_0. @@ -576,11 +574,9 @@ Proof. apply INR_fact_lt_0. rewrite <- Rinv_r_sym. rewrite Rmult_1_r. - replace 1 with (INR 1). - apply le_INR. + apply (le_INR 1). apply lt_le_S. apply INR_lt; apply INR_fact_lt_0. - reflexivity. apply INR_fact_neq_0. apply Rmult_le_reg_l with (INR (fact (S (S (N + n))))). apply INR_fact_lt_0. diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v index e9de24898..76f4e1449 100644 --- a/theories/Reals/Exp_prop.v +++ b/theories/Reals/Exp_prop.v @@ -532,7 +532,7 @@ Proof. apply Rmult_le_reg_l with (INR (fact (div2 (pred n)))). apply INR_fact_lt_0. rewrite Rmult_1_r; rewrite <- Rinv_r_sym. - replace 1 with (INR 1); [ apply le_INR | reflexivity ]. + apply (le_INR 1). apply lt_le_S. apply INR_lt. apply INR_fact_lt_0. diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index dd2108159..7e1cc3e03 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -1629,7 +1629,7 @@ Hint Resolve lt_INR: real. Lemma lt_1_INR : forall n:nat, (1 < n)%nat -> 1 < INR n. Proof. - intros; replace 1 with (INR 1); auto with real. + apply lt_INR. Qed. Hint Resolve lt_1_INR: real. @@ -1653,17 +1653,16 @@ Hint Resolve pos_INR: real. Lemma INR_lt : forall n m:nat, INR n < INR m -> (n < m)%nat. Proof. - double induction n m; intros. - simpl; exfalso; apply (Rlt_irrefl 0); auto. - auto with arith. - generalize (pos_INR (S n0)); intro; cut (INR 0 = 0); - [ intro H2; rewrite H2 in H0; idtac | simpl; trivial ]. - generalize (Rle_lt_trans 0 (INR (S n0)) 0 H1 H0); intro; exfalso; - apply (Rlt_irrefl 0); auto. - do 2 rewrite S_INR in H1; cut (INR n1 < INR n0). - intro H2; generalize (H0 n0 H2); intro; auto with arith. - apply (Rplus_lt_reg_l 1 (INR n1) (INR n0)). - rewrite Rplus_comm; rewrite (Rplus_comm 1 (INR n0)); trivial. + intros n m. revert n. + induction m ; intros n H. + - elim (Rlt_irrefl 0). + apply Rle_lt_trans with (2 := H). + apply pos_INR. + - destruct n as [|n]. + apply Nat.lt_0_succ. + apply lt_n_S, IHm. + rewrite 2!S_INR in H. + apply Rplus_lt_reg_r with (1 := H). Qed. Hint Resolve INR_lt: real. @@ -1707,14 +1706,10 @@ Hint Resolve not_INR: real. Lemma INR_eq : forall n m:nat, INR n = INR m -> n = m. Proof. - intros; case (le_or_lt n m); intros H1. - case (le_lt_or_eq _ _ H1); intros H2; auto. - cut (n <> m). - intro H3; generalize (not_INR n m H3); intro H4; exfalso; auto. - omega. - symmetry ; cut (m <> n). - intro H3; generalize (not_INR m n H3); intro H4; exfalso; auto. - omega. + intros n m HR. + destruct (dec_eq_nat n m) as [H|H]. + exact H. + now apply not_INR in H. Qed. Hint Resolve INR_eq: real. @@ -1728,7 +1723,8 @@ Hint Resolve INR_le: real. Lemma not_1_INR : forall n:nat, n <> 1%nat -> INR n <> 1. Proof. - replace 1 with (INR 1); auto with real. + intros n. + apply not_INR. Qed. Hint Resolve not_1_INR: real. @@ -1905,8 +1901,8 @@ Qed. (**********) Lemma le_IZR_R1 : forall n:Z, IZR n <= 1 -> (n <= 1)%Z. Proof. - pattern 1 at 1; replace 1 with (IZR 1); intros; auto. - apply le_IZR; trivial. + intros n. + apply le_IZR. Qed. (**********) @@ -1935,7 +1931,7 @@ Proof. intros z [H1 H2]. apply Z.le_antisymm. apply Z.lt_succ_r; apply lt_IZR; trivial. - replace 0%Z with (Z.succ (-1)); trivial. + change 0%Z with (Z.succ (-1)). apply Z.le_succ_l; apply lt_IZR; trivial. Qed. @@ -2012,12 +2008,11 @@ Lemma double_var : forall r1, r1 = r1 / 2 + r1 / 2. Proof. intro; rewrite <- double; unfold Rdiv; rewrite <- Rmult_assoc; symmetry ; apply Rinv_r_simpl_m. - replace 2 with (INR 2); - [ apply not_0_INR; discriminate | unfold INR; ring ]. + now apply not_0_IZR. Qed. Lemma R_rm : ring_morph - R0 R1 Rplus Rmult Rminus Ropp eq + 0%R 1%R Rplus Rmult Rminus Ropp eq 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool IZR. Proof. constructor ; try easy. diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v index e9b1762af..46583d374 100644 --- a/theories/Reals/R_Ifp.v +++ b/theories/Reals/R_Ifp.v @@ -42,28 +42,23 @@ Qed. Lemma up_tech : forall (r:R) (z:Z), IZR z <= r -> r < IZR (z + 1) -> (z + 1)%Z = up r. Proof. - intros; generalize (Rplus_le_compat_l 1 (IZR z) r H); intro; clear H; - rewrite (Rplus_comm 1 (IZR z)) in H1; rewrite (Rplus_comm 1 r) in H1; - cut (1 = IZR 1); auto with zarith real. - intro; generalize H1; pattern 1 at 1; rewrite H; intro; clear H H1; - rewrite <- (plus_IZR z 1) in H2; apply (tech_up r (z + 1)); - auto with zarith real. + intros. + apply tech_up with (1 := H0). + rewrite plus_IZR. + now apply Rplus_le_compat_r. Qed. (**********) Lemma fp_R0 : frac_part 0 = 0. Proof. - unfold frac_part; unfold Int_part; elim (archimed 0); intros; - unfold Rminus; elim (Rplus_ne (- IZR (up 0 - 1))); - intros a b; rewrite b; clear a b; rewrite <- Z_R_minus; - cut (up 0 = 1%Z). - intro; rewrite H1; - rewrite (Rminus_diag_eq (IZR 1) (IZR 1) (eq_refl (IZR 1))); - apply Ropp_0. - elim (archimed 0); intros; clear H2; unfold Rgt in H1; - rewrite (Rminus_0_r (IZR (up 0))) in H0; generalize (lt_O_IZR (up 0) H1); - intro; clear H1; generalize (le_IZR_R1 (up 0) H0); - intro; clear H H0; omega. + unfold frac_part, Int_part. + replace (up 0) with 1%Z. + now rewrite <- minus_IZR. + destruct (archimed 0) as [H1 H2]. + apply lt_IZR in H1. + rewrite <- minus_IZR in H2. + apply le_IZR in H2. + omega. Qed. (**********) @@ -229,8 +224,7 @@ Proof. rewrite (Rplus_opp_r (IZR (Int_part r1) - IZR (Int_part r2))) in H; elim (Rplus_ne (r1 - r2)); intros a b; rewrite b in H; clear a b; rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H0; - rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H; - cut (1 = IZR 1); auto with zarith real. + rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H. rewrite <- (plus_IZR (Int_part r1 - Int_part r2) 1) in H; generalize (up_tech (r1 - r2) (Int_part r1 - Int_part r2) H0 H); intros; clear H H0; unfold Int_part at 1; @@ -497,8 +491,7 @@ Proof. in H0; rewrite (Rplus_opp_r (IZR (Int_part r1) + IZR (Int_part r2))) in H0; elim (Rplus_ne (IZR (Int_part r1) + IZR (Int_part r2))); intros a b; rewrite a in H0; clear a b; elim (Rplus_ne (r1 + r2)); - intros a b; rewrite b in H0; clear a b; cut (1 = IZR 1); - auto with zarith real. + intros a b; rewrite b in H0; clear a b. rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H0; rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H1; rewrite <- (plus_IZR (Int_part r1 + Int_part r2) 1) in H1; diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v index 27cb356a0..b749da0d2 100644 --- a/theories/Reals/Ranalysis2.v +++ b/theories/Reals/Ranalysis2.v @@ -423,10 +423,7 @@ Proof. intro; rewrite H11 in H10; assert (H12 := Rmult_lt_compat_l 2 _ _ Hyp H10); rewrite Rmult_1_r in H12; rewrite <- Rinv_r_sym in H12; [ idtac | discrR ]. - cut (IZR 1 < IZR 2). - unfold IZR; unfold INR, Pos.to_nat; simpl; intro; - elim (Rlt_irrefl 1 (Rlt_trans _ _ _ H13 H12)). - apply IZR_lt; omega. + now apply lt_IZR in H12. unfold Rabs; case (Rcase_abs (/ 2)) as [Hlt|Hge]. assert (Hyp : 0 < 2). prove_sup0. diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index 7885d697f..af7cbb940 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -83,11 +83,10 @@ Proof. cut (x = INR (pred x0)). intro H19; rewrite H19; apply le_INR; apply lt_le_S; apply INR_lt; rewrite H18; rewrite <- H19; assumption. - rewrite H10; rewrite H8; rewrite <- INR_IZR_INZ; replace 1 with (INR 1); - [ idtac | reflexivity ]; rewrite <- minus_INR. - replace (x0 - 1)%nat with (pred x0); - [ reflexivity - | case x0; [ reflexivity | intro; simpl; apply minus_n_O ] ]. + rewrite H10; rewrite H8; rewrite <- INR_IZR_INZ; + rewrite <- (minus_INR _ 1). + apply f_equal; + case x0; [ reflexivity | intro; apply sym_eq, minus_n_O ]. induction x0 as [|x0 Hrecx0]. rewrite H8 in H3. rewrite <- INR_IZR_INZ in H3; simpl in H3. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H6 H3)). diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v index f07140752..843aa2752 100644 --- a/theories/Reals/Rlimit.v +++ b/theories/Reals/Rlimit.v @@ -29,59 +29,28 @@ Qed. Lemma eps2 : forall eps:R, eps * / 2 + eps * / 2 = eps. Proof. intro esp. - assert (H := double_var esp). - unfold Rdiv in H. - symmetry ; exact H. + apply eq_sym, double_var. Qed. (*********) Lemma eps4 : forall eps:R, eps * / (2 + 2) + eps * / (2 + 2) = eps * / 2. Proof. intro eps. - replace (2 + 2) with 4. - pattern eps at 3; rewrite double_var. - rewrite (Rmult_plus_distr_r (eps / 2) (eps / 2) (/ 2)). - unfold Rdiv. - repeat rewrite Rmult_assoc. - rewrite <- Rinv_mult_distr. - reflexivity. - discrR. - discrR. - ring. + field. Qed. (*********) Lemma Rlt_eps2_eps : forall eps:R, eps > 0 -> eps * / 2 < eps. Proof. intros. - pattern eps at 2; rewrite <- Rmult_1_r. - repeat rewrite (Rmult_comm eps). - apply Rmult_lt_compat_r. - exact H. - apply Rmult_lt_reg_l with 2. fourier. - rewrite Rmult_1_r; rewrite <- Rinv_r_sym. - fourier. - discrR. Qed. (*********) Lemma Rlt_eps4_eps : forall eps:R, eps > 0 -> eps * / (2 + 2) < eps. Proof. intros. - replace (2 + 2) with 4. - pattern eps at 2; rewrite <- Rmult_1_r. - repeat rewrite (Rmult_comm eps). - apply Rmult_lt_compat_r. - exact H. - apply Rmult_lt_reg_l with 4. - replace 4 with 4. - apply Rmult_lt_0_compat; fourier. - ring. - rewrite Rmult_1_r; rewrite <- Rinv_r_sym. fourier. - discrR. - ring. Qed. (*********) diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index f62ed2a6c..b8040bb4f 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -456,7 +456,7 @@ Proof. unfold Rpower; auto. rewrite Rpower_mult. rewrite Rinv_l. - replace 1 with (INR 1); auto. + change 1 with (INR 1). repeat rewrite Rpower_pow; simpl. pattern x at 1; rewrite <- (sqrt_sqrt x (Rlt_le _ _ H)). ring. diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v index b3c9c7449..6c2b0a1a7 100644 --- a/theories/Reals/Rsqrt_def.v +++ b/theories/Reals/Rsqrt_def.v @@ -648,7 +648,7 @@ Proof. Qed. (** We can now define the square root function as the reciprocal - transformation of the square root function *) + transformation of the square function *) Lemma Rsqrt_exists : forall y:R, 0 <= y -> { z:R | 0 <= z /\ y = Rsqr z }. Proof. diff --git a/theories/Reals/Rtrigo1.v b/theories/Reals/Rtrigo1.v index 17b9677ef..5a999eebe 100644 --- a/theories/Reals/Rtrigo1.v +++ b/theories/Reals/Rtrigo1.v @@ -694,16 +694,15 @@ Proof. rewrite <- Rinv_l_sym. do 2 rewrite Rmult_1_r; apply Rle_lt_trans with (INR (fact (2 * n + 1)) * 4). apply Rmult_le_compat_l. - replace 0 with (INR 0); [ idtac | reflexivity ]; apply le_INR; apply le_O_n. - simpl in |- *; rewrite Rmult_1_r; replace 4 with (Rsqr 2); - [ idtac | ring_Rsqr ]; replace (a * a) with (Rsqr a); - [ idtac | reflexivity ]; apply Rsqr_incr_1. + apply pos_INR. + simpl in |- *; rewrite Rmult_1_r; change 4 with (Rsqr 2); + apply Rsqr_incr_1. apply Rle_trans with (PI / 2); [ assumption | unfold Rdiv in |- *; apply Rmult_le_reg_l with 2; [ prove_sup0 | rewrite <- Rmult_assoc; rewrite Rinv_r_simpl_m; - [ replace 4 with 4; [ apply PI_4 | ring ] | discrR ] ] ]. + [ apply PI_4 | discrR ] ] ]. left; assumption. left; prove_sup0. rewrite H1; replace (2 * n + 1 + 2)%nat with (S (S (2 * n + 1))). @@ -725,9 +724,8 @@ Proof. cut (0 <= x). intro; apply Rplus_le_le_0_compat; repeat apply Rmult_le_pos; assumption || left; prove_sup. - unfold x in |- *; replace 0 with (INR 0); - [ apply le_INR; apply le_O_n | reflexivity ]. - prove_sup0. + apply pos_INR. + now apply IZR_lt. ring. apply INR_fact_neq_0. apply INR_fact_neq_0. @@ -735,39 +733,33 @@ Proof. Qed. Lemma SIN : forall a:R, 0 <= a -> a <= PI -> sin_lb a <= sin a <= sin_ub a. +Proof. intros; unfold sin_lb, sin_ub in |- *; apply (sin_bound a 1 H H0). Qed. Lemma COS : forall a:R, - PI / 2 <= a -> a <= PI / 2 -> cos_lb a <= cos a <= cos_ub a. +Proof. intros; unfold cos_lb, cos_ub in |- *; apply (cos_bound a 1 H H0). Qed. (**********) Lemma _PI2_RLT_0 : - (PI / 2) < 0. Proof. - rewrite <- Ropp_0; apply Ropp_lt_contravar; apply PI2_RGT_0. + assert (H := PI_RGT_0). + fourier. Qed. Lemma PI4_RLT_PI2 : PI / 4 < PI / 2. Proof. - unfold Rdiv in |- *; apply Rmult_lt_compat_l. - apply PI_RGT_0. - apply Rinv_lt_contravar. - apply Rmult_lt_0_compat; prove_sup0. - pattern 2 at 1 in |- *; rewrite <- Rplus_0_r. - replace 4 with (2 + 2); [ apply Rplus_lt_compat_l; prove_sup0 | ring ]. + assert (H := PI_RGT_0). + fourier. Qed. Lemma PI2_Rlt_PI : PI / 2 < PI. Proof. - unfold Rdiv in |- *; pattern PI at 2 in |- *; rewrite <- Rmult_1_r. - apply Rmult_lt_compat_l. - apply PI_RGT_0. - rewrite <- Rinv_1; apply Rinv_lt_contravar. - rewrite Rmult_1_l; prove_sup0. - pattern 1 at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; - apply Rlt_0_1. + assert (H := PI_RGT_0). + fourier. Qed. (***************************************************) @@ -784,12 +776,10 @@ Proof. rewrite H3; rewrite sin_PI2; apply Rlt_0_1. rewrite <- sin_PI_x; generalize (Ropp_gt_lt_contravar x (PI / 2) H3); intro H4; generalize (Rplus_lt_compat_l PI (- x) (- (PI / 2)) H4). - replace (PI + - x) with (PI - x). replace (PI + - (PI / 2)) with (PI / 2). intro H5; generalize (Ropp_lt_gt_contravar x PI H0); intro H6; change (- PI < - x) in H6; generalize (Rplus_lt_compat_l PI (- PI) (- x) H6). rewrite Rplus_opp_r. - replace (PI + - x) with (PI - x). intro H7; elim (SIN (PI - x) (Rlt_le 0 (PI - x) H7) @@ -797,9 +787,7 @@ Proof. intros H8 _; generalize (sin_lb_gt_0 (PI - x) H7 (Rlt_le (PI - x) (PI / 2) H5)); intro H9; apply (Rlt_le_trans 0 (sin_lb (PI - x)) (sin (PI - x)) H9 H8). - reflexivity. - pattern PI at 2 in |- *; rewrite double_var; ring. - reflexivity. + field. Qed. Theorem cos_gt_0 : forall x:R, - (PI / 2) < x -> x < PI / 2 -> 0 < cos x. @@ -852,16 +840,12 @@ Proof. rewrite <- (Ropp_involutive (cos x)); apply Ropp_le_ge_contravar; rewrite <- neg_cos; replace (x + PI) with (x - PI + 2 * INR 1 * PI). rewrite cos_period; apply cos_ge_0. - replace (- (PI / 2)) with (- PI + PI / 2). + replace (- (PI / 2)) with (- PI + PI / 2) by field. unfold Rminus in |- *; rewrite (Rplus_comm x); apply Rplus_le_compat_l; assumption. - pattern PI at 1 in |- *; rewrite (double_var PI); rewrite Ropp_plus_distr; - ring. unfold Rminus in |- *; rewrite Rplus_comm; - replace (PI / 2) with (- PI + 3 * (PI / 2)). + replace (PI / 2) with (- PI + 3 * (PI / 2)) by field. apply Rplus_le_compat_l; assumption. - pattern PI at 1 in |- *; rewrite (double_var PI); rewrite Ropp_plus_distr; - ring. unfold INR in |- *; ring. Qed. @@ -902,16 +886,12 @@ Proof. apply Ropp_lt_gt_contravar; rewrite <- neg_cos; replace (x + PI) with (x - PI + 2 * INR 1 * PI). rewrite cos_period; apply cos_gt_0. - replace (- (PI / 2)) with (- PI + PI / 2). + replace (- (PI / 2)) with (- PI + PI / 2) by field. unfold Rminus in |- *; rewrite (Rplus_comm x); apply Rplus_lt_compat_l; assumption. - pattern PI at 1 in |- *; rewrite (double_var PI); rewrite Ropp_plus_distr; - ring. unfold Rminus in |- *; rewrite Rplus_comm; - replace (PI / 2) with (- PI + 3 * (PI / 2)). + replace (PI / 2) with (- PI + 3 * (PI / 2)) by field. apply Rplus_lt_compat_l; assumption. - pattern PI at 1 in |- *; rewrite (double_var PI); rewrite Ropp_plus_distr; - ring. unfold INR in |- *; ring. Qed. @@ -948,7 +928,7 @@ Lemma cos_ge_0_3PI2 : forall x:R, 3 * (PI / 2) <= x -> x <= 2 * PI -> 0 <= cos x. Proof. intros; rewrite <- cos_neg; rewrite <- (cos_period (- x) 1); - unfold INR in |- *; replace (- x + 2 * 1 * PI) with (2 * PI - x). + unfold INR in |- *; replace (- x + 2 * 1 * PI) with (2 * PI - x) by ring. generalize (Ropp_le_ge_contravar x (2 * PI) H0); intro H1; generalize (Rge_le (- x) (- (2 * PI)) H1); clear H1; intro H1; generalize (Rplus_le_compat_l (2 * PI) (- (2 * PI)) (- x) H1). @@ -957,36 +937,30 @@ Proof. generalize (Rge_le (- (3 * (PI / 2))) (- x) H3); clear H3; intro H3; generalize (Rplus_le_compat_l (2 * PI) (- x) (- (3 * (PI / 2))) H3). - replace (2 * PI + - (3 * (PI / 2))) with (PI / 2). + replace (2 * PI + - (3 * (PI / 2))) with (PI / 2) by field. intro H4; apply (cos_ge_0 (2 * PI - x) (Rlt_le (- (PI / 2)) (2 * PI - x) (Rlt_le_trans (- (PI / 2)) 0 (2 * PI - x) _PI2_RLT_0 H2)) H4). - rewrite double; pattern PI at 2 3 in |- *; rewrite double_var; ring. - ring. Qed. Lemma form1 : forall p q:R, cos p + cos q = 2 * cos ((p - q) / 2) * cos ((p + q) / 2). Proof. intros p q; pattern p at 1 in |- *; - replace p with ((p - q) / 2 + (p + q) / 2). - rewrite <- (cos_neg q); replace (- q) with ((p - q) / 2 - (p + q) / 2). + replace p with ((p - q) / 2 + (p + q) / 2) by field. + rewrite <- (cos_neg q); replace (- q) with ((p - q) / 2 - (p + q) / 2) by field. rewrite cos_plus; rewrite cos_minus; ring. - pattern q at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring. - pattern p at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring. Qed. Lemma form2 : forall p q:R, cos p - cos q = -2 * sin ((p - q) / 2) * sin ((p + q) / 2). Proof. intros p q; pattern p at 1 in |- *; - replace p with ((p - q) / 2 + (p + q) / 2). - rewrite <- (cos_neg q); replace (- q) with ((p - q) / 2 - (p + q) / 2). + replace p with ((p - q) / 2 + (p + q) / 2) by field. + rewrite <- (cos_neg q); replace (- q) with ((p - q) / 2 - (p + q) / 2) by field. rewrite cos_plus; rewrite cos_minus; ring. - pattern q at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring. - pattern p at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring. Qed. Lemma form3 : @@ -1004,11 +978,9 @@ Lemma form4 : forall p q:R, sin p - sin q = 2 * cos ((p + q) / 2) * sin ((p - q) / 2). Proof. intros p q; pattern p at 1 in |- *; - replace p with ((p - q) / 2 + (p + q) / 2). - pattern q at 3 in |- *; replace q with ((p + q) / 2 - (p - q) / 2). + replace p with ((p - q) / 2 + (p + q) / 2) by field. + pattern q at 3 in |- *; replace q with ((p + q) / 2 - (p - q) / 2) by field. rewrite sin_plus; rewrite sin_minus; ring. - pattern q at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring. - pattern p at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring. Qed. @@ -1064,13 +1036,13 @@ Proof. repeat rewrite (Rmult_comm (/ 2)). clear H4; intro H4; generalize (Rplus_le_compat (- (PI / 2)) x (- (PI / 2)) y H H1); - replace (- (PI / 2) + - (PI / 2)) with (- PI). + replace (- (PI / 2) + - (PI / 2)) with (- PI) by field. intro H5; generalize (Rmult_le_compat_l (/ 2) (- PI) (x + y) (Rlt_le 0 (/ 2) (Rinv_0_lt_compat 2 Hyp)) H5). - replace (/ 2 * (x + y)) with ((x + y) / 2). - replace (/ 2 * - PI) with (- (PI / 2)). + replace (/ 2 * (x + y)) with ((x + y) / 2) by apply Rmult_comm. + replace (/ 2 * - PI) with (- (PI / 2)) by field. clear H5; intro H5; elim H4; intro H40. elim H5; intro H50. generalize (cos_gt_0 ((x + y) / 2) H50 H40); intro H6; @@ -1092,13 +1064,6 @@ Proof. rewrite H40 in H3; assert (H50 := cos_PI2); unfold Rdiv in H50; rewrite H50 in H3; rewrite Rmult_0_r in H3; rewrite Rmult_0_l in H3; elim (Rlt_irrefl 0 H3). - unfold Rdiv in |- *. - rewrite <- Ropp_mult_distr_l_reverse. - apply Rmult_comm. - unfold Rdiv in |- *; apply Rmult_comm. - pattern PI at 1 in |- *; rewrite double_var. - rewrite Ropp_plus_distr. - reflexivity. Qed. Lemma sin_increasing_1 : @@ -1108,43 +1073,42 @@ Lemma sin_increasing_1 : Proof. intros; generalize (Rplus_lt_compat_l x x y H3); intro H4; generalize (Rplus_le_compat (- (PI / 2)) x (- (PI / 2)) x H H); - replace (- (PI / 2) + - (PI / 2)) with (- PI). + replace (- (PI / 2) + - (PI / 2)) with (- PI) by field. assert (Hyp : 0 < 2). prove_sup0. intro H5; generalize (Rle_lt_trans (- PI) (x + x) (x + y) H5 H4); intro H6; generalize (Rmult_lt_compat_l (/ 2) (- PI) (x + y) (Rinv_0_lt_compat 2 Hyp) H6); - replace (/ 2 * - PI) with (- (PI / 2)). - replace (/ 2 * (x + y)) with ((x + y) / 2). + replace (/ 2 * - PI) with (- (PI / 2)) by field. + replace (/ 2 * (x + y)) with ((x + y) / 2) by apply Rmult_comm. clear H4 H5 H6; intro H4; generalize (Rplus_lt_compat_l y x y H3); intro H5; rewrite Rplus_comm in H5; generalize (Rplus_le_compat y (PI / 2) y (PI / 2) H2 H2). rewrite <- double_var. intro H6; generalize (Rlt_le_trans (x + y) (y + y) PI H5 H6); intro H7; generalize (Rmult_lt_compat_l (/ 2) (x + y) PI (Rinv_0_lt_compat 2 Hyp) H7); - replace (/ 2 * PI) with (PI / 2). - replace (/ 2 * (x + y)) with ((x + y) / 2). + replace (/ 2 * PI) with (PI / 2) by apply Rmult_comm. + replace (/ 2 * (x + y)) with ((x + y) / 2) by apply Rmult_comm. clear H5 H6 H7; intro H5; generalize (Ropp_le_ge_contravar (- (PI / 2)) y H1); rewrite Ropp_involutive; clear H1; intro H1; generalize (Rge_le (PI / 2) (- y) H1); clear H1; intro H1; generalize (Ropp_le_ge_contravar y (PI / 2) H2); clear H2; intro H2; generalize (Rge_le (- y) (- (PI / 2)) H2); clear H2; intro H2; generalize (Rplus_lt_compat_l (- y) x y H3); - replace (- y + x) with (x - y). + replace (- y + x) with (x - y) by apply Rplus_comm. rewrite Rplus_opp_l. intro H6; generalize (Rmult_lt_compat_l (/ 2) (x - y) 0 (Rinv_0_lt_compat 2 Hyp) H6); - rewrite Rmult_0_r; replace (/ 2 * (x - y)) with ((x - y) / 2). + rewrite Rmult_0_r; replace (/ 2 * (x - y)) with ((x - y) / 2) by apply Rmult_comm. clear H6; intro H6; generalize (Rplus_le_compat (- (PI / 2)) x (- (PI / 2)) (- y) H H2); - replace (- (PI / 2) + - (PI / 2)) with (- PI). - replace (x + - y) with (x - y). + replace (- (PI / 2) + - (PI / 2)) with (- PI) by field. intro H7; generalize (Rmult_le_compat_l (/ 2) (- PI) (x - y) (Rlt_le 0 (/ 2) (Rinv_0_lt_compat 2 Hyp)) H7); - replace (/ 2 * - PI) with (- (PI / 2)). - replace (/ 2 * (x - y)) with ((x - y) / 2). + replace (/ 2 * - PI) with (- (PI / 2)) by field. + replace (/ 2 * (x - y)) with ((x - y) / 2) by apply Rmult_comm. clear H7; intro H7; clear H H0 H1 H2; apply Rminus_lt; rewrite form4; generalize (cos_gt_0 ((x + y) / 2) H4 H5); intro H8; generalize (Rmult_lt_0_compat 2 (cos ((x + y) / 2)) Hyp H8); @@ -1159,23 +1123,6 @@ Proof. 2 * cos ((x + y) / 2)) H10 H8); intro H11; rewrite Rmult_0_r in H11; rewrite Rmult_comm; assumption. apply Ropp_lt_gt_contravar; apply PI2_Rlt_PI. - unfold Rdiv in |- *; apply Rmult_comm. - unfold Rdiv in |- *; rewrite <- Ropp_mult_distr_l_reverse; apply Rmult_comm. - reflexivity. - pattern PI at 1 in |- *; rewrite double_var. - rewrite Ropp_plus_distr. - reflexivity. - unfold Rdiv in |- *; apply Rmult_comm. - unfold Rminus in |- *; apply Rplus_comm. - unfold Rdiv in |- *; apply Rmult_comm. - unfold Rdiv in |- *; apply Rmult_comm. - unfold Rdiv in |- *; apply Rmult_comm. - unfold Rdiv in |- *. - rewrite <- Ropp_mult_distr_l_reverse. - apply Rmult_comm. - pattern PI at 1 in |- *; rewrite double_var. - rewrite Ropp_plus_distr. - reflexivity. Qed. Lemma sin_decreasing_0 : @@ -1190,33 +1137,16 @@ Proof. generalize (Rplus_le_compat_l (- PI) (PI / 2) x H0); generalize (Rplus_le_compat_l (- PI) y (3 * (PI / 2)) H1); generalize (Rplus_le_compat_l (- PI) (PI / 2) y H2); - replace (- PI + x) with (x - PI). - replace (- PI + PI / 2) with (- (PI / 2)). - replace (- PI + y) with (y - PI). - replace (- PI + 3 * (PI / 2)) with (PI / 2). - replace (- (PI - x)) with (x - PI). - replace (- (PI - y)) with (y - PI). + replace (- PI + x) with (x - PI) by apply Rplus_comm. + replace (- PI + PI / 2) with (- (PI / 2)) by field. + replace (- PI + y) with (y - PI) by apply Rplus_comm. + replace (- PI + 3 * (PI / 2)) with (PI / 2) by field. + replace (- (PI - x)) with (x - PI) by ring. + replace (- (PI - y)) with (y - PI) by ring. intros; change (sin (y - PI) < sin (x - PI)) in H8; - apply Rplus_lt_reg_l with (- PI); rewrite Rplus_comm; - replace (y + - PI) with (y - PI). - rewrite Rplus_comm; replace (x + - PI) with (x - PI). + apply Rplus_lt_reg_l with (- PI); rewrite Rplus_comm. + rewrite (Rplus_comm _ x). apply (sin_increasing_0 (y - PI) (x - PI) H4 H5 H6 H7 H8). - reflexivity. - reflexivity. - unfold Rminus in |- *; rewrite Ropp_plus_distr. - rewrite Ropp_involutive. - apply Rplus_comm. - unfold Rminus in |- *; rewrite Ropp_plus_distr. - rewrite Ropp_involutive. - apply Rplus_comm. - pattern PI at 2 in |- *; rewrite double_var. - rewrite Ropp_plus_distr. - ring. - unfold Rminus in |- *; apply Rplus_comm. - pattern PI at 2 in |- *; rewrite double_var. - rewrite Ropp_plus_distr. - ring. - unfold Rminus in |- *; apply Rplus_comm. Qed. Lemma sin_decreasing_1 : @@ -1230,24 +1160,14 @@ Proof. generalize (Rplus_le_compat_l (- PI) y (3 * (PI / 2)) H1); generalize (Rplus_le_compat_l (- PI) (PI / 2) y H2); generalize (Rplus_lt_compat_l (- PI) x y H3); - replace (- PI + PI / 2) with (- (PI / 2)). - replace (- PI + y) with (y - PI). - replace (- PI + 3 * (PI / 2)) with (PI / 2). - replace (- PI + x) with (x - PI). + replace (- PI + PI / 2) with (- (PI / 2)) by field. + replace (- PI + y) with (y - PI) by apply Rplus_comm. + replace (- PI + 3 * (PI / 2)) with (PI / 2) by field. + replace (- PI + x) with (x - PI) by apply Rplus_comm. intros; apply Ropp_lt_cancel; repeat rewrite <- sin_neg; - replace (- (PI - x)) with (x - PI). - replace (- (PI - y)) with (y - PI). + replace (- (PI - x)) with (x - PI) by ring. + replace (- (PI - y)) with (y - PI) by ring. apply (sin_increasing_1 (x - PI) (y - PI) H7 H8 H5 H6 H4). - unfold Rminus in |- *; rewrite Ropp_plus_distr. - rewrite Ropp_involutive. - apply Rplus_comm. - unfold Rminus in |- *; rewrite Ropp_plus_distr. - rewrite Ropp_involutive. - apply Rplus_comm. - unfold Rminus in |- *; apply Rplus_comm. - pattern PI at 2 in |- *; rewrite double_var; ring. - unfold Rminus in |- *; apply Rplus_comm. - pattern PI at 2 in |- *; rewrite double_var; ring. Qed. Lemma cos_increasing_0 : @@ -1287,31 +1207,16 @@ Proof. generalize (Rplus_lt_compat_l (-3 * (PI / 2)) x y H5); rewrite <- (cos_neg x); rewrite <- (cos_neg y); rewrite <- (cos_period (- x) 1); rewrite <- (cos_period (- y) 1); - unfold INR in |- *; replace (-3 * (PI / 2) + x) with (x - 3 * (PI / 2)). - replace (-3 * (PI / 2) + y) with (y - 3 * (PI / 2)). - replace (-3 * (PI / 2) + PI) with (- (PI / 2)). - replace (-3 * (PI / 2) + 2 * PI) with (PI / 2). + unfold INR in |- *; replace (-3 * (PI / 2) + x) with (x - 3 * (PI / 2)) by ring. + replace (-3 * (PI / 2) + y) with (y - 3 * (PI / 2)) by ring. + replace (-3 * (PI / 2) + PI) with (- (PI / 2)) by field. + replace (-3 * (PI / 2) + 2 * PI) with (PI / 2) by field. clear H1 H2 H3 H4 H5; intros H1 H2 H3 H4 H5; - replace (- x + 2 * 1 * PI) with (PI / 2 - (x - 3 * (PI / 2))). - replace (- y + 2 * 1 * PI) with (PI / 2 - (y - 3 * (PI / 2))). + replace (- x + 2 * 1 * PI) with (PI / 2 - (x - 3 * (PI / 2))) by field. + replace (- y + 2 * 1 * PI) with (PI / 2 - (y - 3 * (PI / 2))) by field. repeat rewrite cos_shift; apply (sin_increasing_1 (x - 3 * (PI / 2)) (y - 3 * (PI / 2)) H5 H4 H3 H2 H1). - rewrite Rmult_1_r. - rewrite (double PI); pattern PI at 3 4 in |- *; rewrite double_var. - ring. - rewrite Rmult_1_r. - rewrite (double PI); pattern PI at 3 4 in |- *; rewrite double_var. - ring. - rewrite (double PI); pattern PI at 3 4 in |- *; rewrite double_var. - ring. - pattern PI at 3 in |- *; rewrite double_var; ring. - unfold Rminus in |- *. - rewrite <- Ropp_mult_distr_l_reverse. - apply Rplus_comm. - unfold Rminus in |- *. - rewrite <- Ropp_mult_distr_l_reverse. - apply Rplus_comm. Qed. Lemma cos_decreasing_0 : @@ -1350,31 +1255,8 @@ Lemma tan_diff : cos x <> 0 -> cos y <> 0 -> tan x - tan y = sin (x - y) / (cos x * cos y). Proof. intros; unfold tan in |- *; rewrite sin_minus. - unfold Rdiv in |- *. - unfold Rminus in |- *. - rewrite Rmult_plus_distr_r. - rewrite Rinv_mult_distr. - repeat rewrite (Rmult_comm (sin x)). - repeat rewrite Rmult_assoc. - rewrite (Rmult_comm (cos y)). - repeat rewrite Rmult_assoc. - rewrite <- Rinv_l_sym. - rewrite Rmult_1_r. - rewrite (Rmult_comm (sin x)). - apply Rplus_eq_compat_l. - rewrite <- Ropp_mult_distr_l_reverse. - rewrite <- Ropp_mult_distr_r_reverse. - rewrite (Rmult_comm (/ cos x)). - repeat rewrite Rmult_assoc. - rewrite (Rmult_comm (cos x)). - repeat rewrite Rmult_assoc. - rewrite <- Rinv_l_sym. - rewrite Rmult_1_r. - reflexivity. - assumption. - assumption. - assumption. - assumption. + field. + now split. Qed. Lemma tan_increasing_0 : @@ -1411,10 +1293,9 @@ Proof. intro H11; generalize (Rge_le (- y) (- (PI / 4)) H11); clear H11; intro H11; generalize (Rplus_le_compat (- (PI / 4)) x (- (PI / 4)) (- y) H H11); - generalize (Rplus_le_compat x (PI / 4) (- y) (PI / 4) H0 H10); - replace (x + - y) with (x - y). - replace (PI / 4 + PI / 4) with (PI / 2). - replace (- (PI / 4) + - (PI / 4)) with (- (PI / 2)). + generalize (Rplus_le_compat x (PI / 4) (- y) (PI / 4) H0 H10). + replace (PI / 4 + PI / 4) with (PI / 2) by field. + replace (- (PI / 4) + - (PI / 4)) with (- (PI / 2)) by field. intros; case (Rtotal_order 0 (x - y)); intro H14. generalize (sin_gt_0 (x - y) H14 (Rle_lt_trans (x - y) (PI / 2) PI H12 PI2_Rlt_PI)); @@ -1422,28 +1303,6 @@ Proof. elim H14; intro H15. rewrite <- H15 in H9; rewrite sin_0 in H9; elim (Rlt_irrefl 0 H9). apply Rminus_lt; assumption. - pattern PI at 1 in |- *; rewrite double_var. - unfold Rdiv in |- *. - rewrite Rmult_plus_distr_r. - repeat rewrite Rmult_assoc. - rewrite <- Rinv_mult_distr. - rewrite Ropp_plus_distr. - replace 4 with 4. - reflexivity. - ring. - discrR. - discrR. - pattern PI at 1 in |- *; rewrite double_var. - unfold Rdiv in |- *. - rewrite Rmult_plus_distr_r. - repeat rewrite Rmult_assoc. - rewrite <- Rinv_mult_distr. - replace 4 with 4. - reflexivity. - ring. - discrR. - discrR. - reflexivity. case (Rcase_abs (sin (x - y))); intro H9. assumption. generalize (Rge_le (sin (x - y)) 0 H9); clear H9; intro H9; @@ -1457,8 +1316,7 @@ Proof. (Rlt_le 0 (/ (cos x * cos y)) H12)); intro H13; elim (Rlt_irrefl 0 (Rle_lt_trans 0 (sin (x - y) * / (cos x * cos y)) 0 H13 H3)). - rewrite Rinv_mult_distr. - reflexivity. + apply Rinv_mult_distr. assumption. assumption. Qed. @@ -1496,9 +1354,8 @@ Proof. clear H10 H11; intro H8; generalize (Ropp_le_ge_contravar y (PI / 4) H2); intro H11; generalize (Rge_le (- y) (- (PI / 4)) H11); clear H11; intro H11; - generalize (Rplus_le_compat (- (PI / 4)) x (- (PI / 4)) (- y) H H11); - replace (x + - y) with (x - y). - replace (- (PI / 4) + - (PI / 4)) with (- (PI / 2)). + generalize (Rplus_le_compat (- (PI / 4)) x (- (PI / 4)) (- y) H H11). + replace (- (PI / 4) + - (PI / 4)) with (- (PI / 2)) by field. clear H11; intro H9; generalize (Rlt_minus x y H3); clear H3; intro H3; clear H H0 H1 H2 H4 H5 HP1 HP2; generalize PI2_Rlt_PI; intro H1; generalize (Ropp_lt_gt_contravar (PI / 2) PI H1); @@ -1509,18 +1366,6 @@ Proof. generalize (Rmult_lt_gt_compat_neg_l (sin (x - y)) 0 (/ (cos x * cos y)) H2 H8); rewrite Rmult_0_r; intro H4; assumption. - pattern PI at 1 in |- *; rewrite double_var. - unfold Rdiv in |- *. - rewrite Rmult_plus_distr_r. - repeat rewrite Rmult_assoc. - rewrite <- Rinv_mult_distr. - replace 4 with 4. - rewrite Ropp_plus_distr. - reflexivity. - ring. - discrR. - discrR. - reflexivity. apply Rinv_mult_distr; assumption. Qed. @@ -1762,8 +1607,7 @@ Proof. rewrite Rplus_0_r. rewrite Ropp_Ropp_IZR. rewrite Rplus_opp_r. - left; replace 0 with (IZR 0); [ apply IZR_lt | reflexivity ]. - assumption. + now apply Rlt_le, IZR_lt. rewrite <- sin_neg. rewrite Ropp_mult_distr_l_reverse. rewrite Ropp_involutive. diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v index 092bc30d0..55cb74e35 100644 --- a/theories/Reals/Rtrigo_alt.v +++ b/theories/Reals/Rtrigo_alt.v @@ -99,24 +99,22 @@ Proof. apply Rle_trans with 20. apply Rle_trans with 16. replace 16 with (Rsqr 4); [ idtac | ring_Rsqr ]. - replace (a * a) with (Rsqr a); [ idtac | reflexivity ]. apply Rsqr_incr_1. assumption. assumption. - left; prove_sup0. - rewrite <- (Rplus_0_r 16); replace 20 with (16 + 4); - [ apply Rplus_le_compat_l; left; prove_sup0 | ring ]. - rewrite <- (Rplus_comm 20); pattern 20 at 1; rewrite <- Rplus_0_r; - apply Rplus_le_compat_l. + now apply IZR_le. + now apply IZR_le. + rewrite <- (Rplus_0_l 20) at 1; + apply Rplus_le_compat_r. apply Rplus_le_le_0_compat. - repeat apply Rmult_le_pos. - left; prove_sup0. - left; prove_sup0. - replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ]. - replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ]. apply Rmult_le_pos. - left; prove_sup0. - replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ]. + apply Rmult_le_pos. + now apply IZR_le. + apply pos_INR. + apply pos_INR. + apply Rmult_le_pos. + now apply IZR_le. + apply pos_INR. apply INR_fact_neq_0. apply INR_fact_neq_0. simpl; ring. @@ -182,16 +180,14 @@ Proof. replace (- sum_f_R0 (tg_alt Un) (S (2 * n))) with (-1 * sum_f_R0 (tg_alt Un) (S (2 * n))); [ rewrite scal_sum | ring ]. apply sum_eq; intros; unfold sin_term, Un, tg_alt; - replace ((-1) ^ S i) with (-1 * (-1) ^ i). + change ((-1) ^ S i) with (-1 * (-1) ^ i). unfold Rdiv; ring. - reflexivity. replace (- sum_f_R0 (tg_alt Un) (2 * n)) with (-1 * sum_f_R0 (tg_alt Un) (2 * n)); [ rewrite scal_sum | ring ]. apply sum_eq; intros. unfold sin_term, Un, tg_alt; - replace ((-1) ^ S i) with (-1 * (-1) ^ i). + change ((-1) ^ S i) with (-1 * (-1) ^ i). unfold Rdiv; ring. - reflexivity. replace (2 * (n + 1))%nat with (S (S (2 * n))). reflexivity. ring. @@ -279,26 +275,23 @@ Proof. with (4 * INR n1 * INR n1 + 14 * INR n1 + 12); [ idtac | ring ]. apply Rle_trans with 12. apply Rle_trans with 4. - replace 4 with (Rsqr 2); [ idtac | ring_Rsqr ]. - replace (a0 * a0) with (Rsqr a0); [ idtac | reflexivity ]. + change 4 with (Rsqr 2). apply Rsqr_incr_1. assumption. - discrR. assumption. - left; prove_sup0. - pattern 4 at 1; rewrite <- Rplus_0_r; replace 12 with (4 + 8); - [ apply Rplus_le_compat_l; left; prove_sup0 | ring ]. - rewrite <- (Rplus_comm 12); pattern 12 at 1; rewrite <- Rplus_0_r; - apply Rplus_le_compat_l. + now apply IZR_le. + now apply IZR_le. + rewrite <- (Rplus_0_l 12) at 1; + apply Rplus_le_compat_r. apply Rplus_le_le_0_compat. - repeat apply Rmult_le_pos. - left; prove_sup0. - left; prove_sup0. - replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ]. - replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ]. apply Rmult_le_pos. - left; prove_sup0. - replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ]. + apply Rmult_le_pos. + now apply IZR_le. + apply pos_INR. + apply pos_INR. + apply Rmult_le_pos. + now apply IZR_le. + apply pos_INR. apply INR_fact_neq_0. apply INR_fact_neq_0. simpl; ring. @@ -351,15 +344,13 @@ Proof. replace (- sum_f_R0 (tg_alt Un) (S (2 * n0))) with (-1 * sum_f_R0 (tg_alt Un) (S (2 * n0))); [ rewrite scal_sum | ring ]. apply sum_eq; intros; unfold cos_term, Un, tg_alt; - replace ((-1) ^ S i) with (-1 * (-1) ^ i). + change ((-1) ^ S i) with (-1 * (-1) ^ i). unfold Rdiv; ring. - reflexivity. replace (- sum_f_R0 (tg_alt Un) (2 * n0)) with (-1 * sum_f_R0 (tg_alt Un) (2 * n0)); [ rewrite scal_sum | ring ]; apply sum_eq; intros; unfold cos_term, Un, tg_alt; - replace ((-1) ^ S i) with (-1 * (-1) ^ i). + change ((-1) ^ S i) with (-1 * (-1) ^ i). unfold Rdiv; ring. - reflexivity. replace (2 * (n0 + 1))%nat with (S (S (2 * n0))). reflexivity. ring. diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v index 0d2a9a8ba..b46df202e 100644 --- a/theories/Reals/Rtrigo_def.v +++ b/theories/Reals/Rtrigo_def.v @@ -157,7 +157,7 @@ Proof. apply Rinv_0_lt_compat; assumption. rewrite H3 in H0; assumption. apply lt_le_trans with 1%nat; [ apply lt_O_Sn | apply le_max_r ]. - apply le_IZR; replace (IZR 0) with 0; [ idtac | reflexivity ]; left; + apply le_IZR; left; apply Rlt_trans with (/ eps); [ apply Rinv_0_lt_compat; assumption | assumption ]. assert (H0 := archimed (/ eps)). @@ -194,30 +194,27 @@ Proof. elim H1; intros; assumption. apply lt_le_trans with (S n). unfold ge in H2; apply le_lt_n_Sm; assumption. - replace (2 * n + 1)%nat with (S (2 * n)); [ idtac | ring ]. + replace (2 * n + 1)%nat with (S (2 * n)) by ring. apply le_n_S; apply le_n_2n. apply Rmult_lt_reg_l with (INR (2 * S n)). apply lt_INR_0; replace (2 * S n)%nat with (S (S (2 * n))). apply lt_O_Sn. - replace (S n) with (n + 1)%nat; [ idtac | ring ]. + replace (S n) with (n + 1)%nat by ring. ring. rewrite <- Rinv_r_sym. - rewrite Rmult_1_r; replace 1 with (INR 1); [ apply lt_INR | reflexivity ]. + rewrite Rmult_1_r. + apply (lt_INR 1). replace (2 * S n)%nat with (S (S (2 * n))). apply lt_n_S; apply lt_O_Sn. - replace (S n) with (n + 1)%nat; [ ring | ring ]. + ring. apply not_O_INR; discriminate. apply not_O_INR; discriminate. replace (2 * n + 1)%nat with (S (2 * n)); [ apply not_O_INR; discriminate | ring ]. apply Rle_ge; left; apply Rinv_0_lt_compat. apply lt_INR_0. - replace (2 * S n * (2 * n + 1))%nat with (S (S (4 * (n * n) + 6 * n))). + replace (2 * S n * (2 * n + 1))%nat with (2 + (4 * (n * n) + 6 * n))%nat by ring. apply lt_O_Sn. - apply INR_eq. - repeat rewrite S_INR; rewrite plus_INR; repeat rewrite mult_INR; - rewrite plus_INR; rewrite mult_INR; repeat rewrite S_INR; - replace (INR 0) with 0; [ ring | reflexivity ]. Qed. Lemma cosn_no_R0 : forall n:nat, cos_n n <> 0. @@ -318,28 +315,25 @@ Proof. elim H1; intros; assumption. apply lt_le_trans with (S n). unfold ge in H2; apply le_lt_n_Sm; assumption. - replace (2 * S n + 1)%nat with (S (2 * S n)); [ idtac | ring ]. + replace (2 * S n + 1)%nat with (S (2 * S n)) by ring. apply le_S; apply le_n_2n. apply Rmult_lt_reg_l with (INR (2 * S n)). apply lt_INR_0; replace (2 * S n)%nat with (S (S (2 * n))); - [ apply lt_O_Sn | replace (S n) with (n + 1)%nat; [ idtac | ring ]; ring ]. + [ apply lt_O_Sn | ring ]. rewrite <- Rinv_r_sym. - rewrite Rmult_1_r; replace 1 with (INR 1); [ apply lt_INR | reflexivity ]. + rewrite Rmult_1_r. + apply (lt_INR 1). replace (2 * S n)%nat with (S (S (2 * n))). apply lt_n_S; apply lt_O_Sn. - replace (S n) with (n + 1)%nat; [ ring | ring ]. + ring. apply not_O_INR; discriminate. apply not_O_INR; discriminate. apply not_O_INR; discriminate. - left; change (0 < / INR ((2 * S n + 1) * (2 * S n))); - apply Rinv_0_lt_compat. + left; apply Rinv_0_lt_compat. apply lt_INR_0. replace ((2 * S n + 1) * (2 * S n))%nat with - (S (S (S (S (S (S (4 * (n * n) + 10 * n))))))). + (6 + (4 * (n * n) + 10 * n))%nat by ring. apply lt_O_Sn. - apply INR_eq; repeat rewrite S_INR; rewrite plus_INR; repeat rewrite mult_INR; - rewrite plus_INR; rewrite mult_INR; repeat rewrite S_INR; - replace (INR 0) with 0; [ ring | reflexivity ]. Qed. Lemma sin_no_R0 : forall n:nat, sin_n n <> 0. diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v index 5a2a07c42..3697999f7 100644 --- a/theories/Reals/SeqProp.v +++ b/theories/Reals/SeqProp.v @@ -1167,7 +1167,7 @@ Proof. assert (H6 := archimed (Rabs x)); fold M in H6; elim H6; intros. rewrite H4 in H7; rewrite <- INR_IZR_INZ in H7. simpl in H7; elim (Rlt_irrefl _ (Rlt_trans _ _ _ H2 H7)). - replace 1 with (INR 1); [ apply le_INR | reflexivity ]; apply le_n_S; + apply (le_INR 1); apply le_n_S; apply le_O_n. apply le_IZR; simpl; left; apply Rlt_trans with (Rabs x). assumption. diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index 1f8b76cb6..c49451776 100644 --- a/theories/Vectors/VectorDef.v +++ b/theories/Vectors/VectorDef.v @@ -147,6 +147,16 @@ Definition shiftrepeat {A} := @rectS _ (fun n _ => t A (S (S n))) (fun h => h :: h :: []) (fun h _ _ H => h :: H). Global Arguments shiftrepeat {A} {n} v. +(** Take first [p] elements of a vector *) +Fixpoint take {A} {n} (p:nat) (le:p <= n) (v:t A n) : t A p := + match p as p return p <= n -> t A p with + | 0 => fun _ => [] + | S p' => match v in t _ n return S p' <= n -> t A (S p') with + | []=> fun le => False_rect _ (Nat.nle_succ_0 p' le) + | x::xs => fun le => x::take p' (le_S_n p' _ le) xs + end + end le. + (** Remove [p] last elements of a vector *) Lemma trunc : forall {A} {n} (p:nat), n > p -> t A n -> t A (n - p). diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v index c5278b918..869d0fb5a 100644 --- a/theories/Vectors/VectorSpec.v +++ b/theories/Vectors/VectorSpec.v @@ -122,3 +122,32 @@ induction l. - reflexivity. - unfold to_list; simpl. now f_equal. Qed. + +Lemma take_O : forall {A} {n} le (v:t A n), take 0 le v = []. +Proof. + reflexivity. +Qed. + +Lemma take_idem : forall {A} p n (v:t A n) le le', + take p le' (take p le v) = take p le v. +Proof. + induction p; intros n v le le'. + - auto. + - destruct v. inversion le. simpl. apply f_equal. apply IHp. +Qed. + +Lemma take_app : forall {A} {n} (v:t A n) {m} (w:t A m) le, take n le (append v w) = v. +Proof. + induction v; intros m w le. + - reflexivity. + - simpl. apply f_equal. apply IHv. +Qed. + +(* Proof is irrelevant for [take] *) +Lemma take_prf_irr : forall {A} p {n} (v:t A n) le le', take p le v = take p le' v. +Proof. + induction p; intros n v le le'. + - reflexivity. + - destruct v. inversion le. simpl. apply f_equal. apply IHp. +Qed. + diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 06908abb6..9917a49b4 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -266,9 +266,9 @@ let ensure_bname src tgt = let src, tgt = Filename.basename src, Filename.basename tgt in let src, tgt = chop_extension src, chop_extension tgt in if src <> tgt then begin - Feedback.msg_error (str "Source and target file names must coincide, directories can differ"); - Feedback.msg_error (str "Source: " ++ str src); - Feedback.msg_error (str "Target: " ++ str tgt); + Feedback.msg_error (str "Source and target file names must coincide, directories can differ" ++ fnl () ++ + str "Source: " ++ str src ++ fnl () ++ + str "Target: " ++ str tgt); flush_all (); exit 1 end diff --git a/vernac/classes.ml b/vernac/classes.ml index c3300a361..833719965 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -338,7 +338,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p the refinement manually.*) let gls = List.rev (Evd.future_goals evm) in let evm = Evd.reset_future_goals evm in - Lemmas.start_proof id kind evm (EConstr.of_constr termtype) + Lemmas.start_proof id ?pl kind evm (EConstr.of_constr termtype) (Lemmas.mk_hook (fun _ -> instance_hook k pri global imps ?hook)); (* spiwack: I don't know what to do with the status here. *) diff --git a/vernac/classes.mli b/vernac/classes.mli index d2cb788ea..69ea84158 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -42,7 +42,7 @@ val new_instance : ?global:bool -> (** Not global by default. *) ?refine:bool -> (** Allow refinement *) Decl_kinds.polymorphic -> - local_binder list -> + local_binder_expr list -> typeclass_constraint -> (bool * constr_expr) option -> ?generalize:bool -> @@ -63,4 +63,4 @@ val id_of_class : typeclass -> Id.t (** returns [false] if, for lack of section, it declares an assumption (unless in a module type). *) -val context : Decl_kinds.polymorphic -> local_binder list -> bool +val context : Decl_kinds.polymorphic -> local_binder_expr list -> bool diff --git a/vernac/command.ml b/vernac/command.ml index db203b425..0393669d4 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -55,7 +55,7 @@ let rec under_binders env sigma f n c = let rec complete_conclusion a cs = function | CProdN (loc,bl,c) -> CProdN (loc,bl,complete_conclusion a cs c) - | CLetIn (loc,b,t,c) -> CLetIn (loc,b,t,complete_conclusion a cs c) + | CLetIn (loc,na,b,t,c) -> CLetIn (loc,na,b,t,complete_conclusion a cs c) | CHole (loc, k, _, _) -> let (has_no_args,name,params) = a in if not has_no_args then @@ -378,7 +378,7 @@ type structured_one_inductive_expr = { } type structured_inductive_expr = - local_binder list * structured_one_inductive_expr list + local_binder_expr list * structured_one_inductive_expr list let minductive_message warn = function | [] -> error "No inductive definition." @@ -424,7 +424,7 @@ let rec check_anonymous_type ind = match ind with | GSort (_, GType []) -> true | GProd (_, _, _, _, e) - | GLetIn (_, _, _, e) + | GLetIn (_, _, _, _, e) | GLambda (_, _, _, _, e) | GApp (_, e, _) | GCast (_, e, _) -> check_anonymous_type e @@ -569,10 +569,10 @@ let check_named (loc, na) = match na with let check_param = function -| LocalRawDef (na, _) -> check_named na -| LocalRawAssum (nas, Default _, _) -> List.iter check_named nas -| LocalRawAssum (nas, Generalized _, _) -> () -| LocalPattern _ -> assert false +| CLocalDef (na, _, _) -> check_named na +| CLocalAssum (nas, Default _, _) -> List.iter check_named nas +| CLocalAssum (nas, Generalized _, _) -> () +| CLocalPattern _ -> assert false let interp_mutual_inductive (paramsl,indl) notations poly prv finite = check_all_names_different indl; @@ -840,7 +840,7 @@ type structured_fixpoint_expr = { fix_name : Id.t; fix_univs : lident list option; fix_annot : Id.t Loc.located option; - fix_binders : local_binder list; + fix_binders : local_binder_expr list; fix_body : constr_expr option; fix_type : constr_expr } diff --git a/vernac/command.mli b/vernac/command.mli index fae783ef0..7cd0afeec 100644 --- a/vernac/command.mli +++ b/vernac/command.mli @@ -32,7 +32,7 @@ val get_declare_definition_hook : unit -> (Safe_typing.private_constants definit (** {6 Definitions/Let} *) val interp_definition : - lident list option -> local_binder list -> polymorphic -> red_expr option -> constr_expr -> + lident list option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr -> constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * Universes.universe_binders * Impargs.manual_implicits @@ -41,13 +41,13 @@ val declare_definition : Id.t -> definition_kind -> Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference val do_definition : Id.t -> definition_kind -> lident list option -> - local_binder list -> red_expr option -> constr_expr -> + local_binder_expr list -> red_expr option -> constr_expr -> constr_expr option -> unit Lemmas.declaration_hook -> unit (** {6 Parameters/Assumptions} *) (* val interp_assumption : env -> evar_map ref -> *) -(* local_binder list -> constr_expr -> *) +(* local_binder_expr list -> constr_expr -> *) (* types Univ.in_universe_context_set * Impargs.manual_implicits *) (** returns [false] if the assumption is neither local to a section, @@ -78,7 +78,7 @@ type structured_one_inductive_expr = { } type structured_inductive_expr = - local_binder list * structured_one_inductive_expr list + local_binder_expr list * structured_one_inductive_expr list val extract_mutual_inductive_declaration_components : (one_inductive_expr * decl_notation list) list -> @@ -114,7 +114,7 @@ type structured_fixpoint_expr = { fix_name : Id.t; fix_univs : lident list option; fix_annot : Id.t Loc.located option; - fix_binders : local_binder list; + fix_binders : local_binder_expr list; fix_body : constr_expr option; fix_type : constr_expr } diff --git a/vernac/record.ml b/vernac/record.ml index e1c99fa2a..490a2a49d 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -109,9 +109,9 @@ let typecheck_params_and_fields def id pl t ps nots fs = | _ -> () in List.iter - (function LocalRawDef (b, _) -> error default_binder_kind b - | LocalRawAssum (ls, bk, ce) -> List.iter (error bk) ls - | LocalPattern (loc,_,_) -> + (function CLocalDef (b, _, _) -> error default_binder_kind b + | CLocalAssum (ls, bk, ce) -> List.iter (error bk) ls + | CLocalPattern (loc,_,_) -> Loc.raise ~loc (Stream.Error "pattern with quote not allowed in record parameters.")) ps in let impls_env, ((env1,newps), imps) = interp_context_evars env0 evars ps in diff --git a/vernac/record.mli b/vernac/record.mli index c50e57786..3fd651db9 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -39,7 +39,7 @@ val declare_structure : val definition_structure : inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind * - plident with_coercion * local_binder list * + plident with_coercion * local_binder_expr list * (local_decl_expr with_instance with_priority with_notation) list * Id.t * constr_expr option -> global_reference diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 66796d1dc..53d49ddbc 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -67,8 +67,7 @@ let show_node () = could, possibly, be cleaned away. (Feb. 2010) *) () -let show_thesis () = - Feedback.msg_error (anomaly (Pp.str "TODO") ) +let show_thesis () = CErrors.anomaly (Pp.str "Show Thesis: TODO") let show_top_evars () = (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *) @@ -2216,6 +2215,11 @@ let with_fail b f = let interp ?(verbosely=true) ?proof (loc,c) = let orig_program_mode = Flags.is_program_mode () in let rec aux ?locality ?polymorphism isprogcmd = function + + (* This assert case will be removed when fake_ide can understand + completion feedback *) + | VernacStm _ -> assert false (* Done by Stm *) + | VernacProgram c when not isprogcmd -> aux ?locality ?polymorphism true c | VernacProgram _ -> CErrors.error "Program mode specified twice" | VernacLocal (b, c) when Option.is_empty locality -> @@ -2224,9 +2228,6 @@ let interp ?(verbosely=true) ?proof (loc,c) = aux ?locality ~polymorphism:b isprogcmd c | VernacPolymorphic (b, c) -> CErrors.error "Polymorphism specified twice" | VernacLocal _ -> CErrors.error "Locality specified twice" - | VernacStm (Command c) -> aux ?locality ?polymorphism isprogcmd c - | VernacStm (PGLast c) -> aux ?locality ?polymorphism isprogcmd c - | VernacStm _ -> assert false (* Done by Stm *) | VernacFail v -> with_fail true (fun () -> aux ?locality ?polymorphism isprogcmd v) | VernacTimeout (n,v) -> |