From 414cfd64702be920c9d96514e3802bc950b5ea0b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Maxime=20D=C3=A9n=C3=A8s?= Date: Fri, 7 Dec 2018 13:38:59 +0100 Subject: [PATCH] Clean the representation of recursive annotation in Constrexpr We make clearer which arguments are optional and which are mandatory. Some of these representations are tricky because of small differences between Program and Function, which share the same infrastructure. As a side-effect of this cleanup, Program Fixpoint can now be used with e.g. {measure (m + n) R}. Previously, parentheses were required around R. --- interp/constrexpr.ml | 8 ++-- interp/constrexpr_ops.ml | 15 ++++--- interp/constrextern.ml | 22 +++------ interp/constrintern.ml | 67 +++++++++++++-------------- interp/notation_ops.ml | 2 +- interp/notation_term.ml | 2 +- parsing/g_constr.mlg | 14 +++--- parsing/pcoq.mli | 2 +- plugins/funind/g_indfun.mlg | 6 ++- plugins/funind/indfun.ml | 87 ++++++++++++++++++------------------ plugins/ssr/ssrparser.mlg | 4 +- pretyping/detyping.ml | 2 +- pretyping/glob_ops.ml | 16 ++----- pretyping/glob_term.ml | 19 +++----- pretyping/patternops.ml | 24 +++++----- pretyping/pretyping.ml | 4 +- printing/ppconstr.ml | 17 +++---- printing/ppconstr.mli | 2 +- printing/proof_diffs.ml | 12 ++--- vernac/comFixpoint.ml | 25 ++++++++--- vernac/comFixpoint.mli | 2 +- vernac/comProgramFixpoint.ml | 32 +++++++------ vernac/obligations.ml | 4 +- vernac/obligations.mli | 2 +- vernac/vernacexpr.ml | 2 +- 25 files changed, 191 insertions(+), 201 deletions(-) diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index 7a14a4e708c3..653bb68f30c0 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -134,16 +134,16 @@ and branch_expr = (cases_pattern_expr list list * constr_expr) CAst.t and fix_expr = - lident * (lident option * recursion_order_expr) * + lident * (recursion_order_expr CAst.t) option * local_binder_expr list * constr_expr * constr_expr and cofix_expr = lident * local_binder_expr list * constr_expr * constr_expr and recursion_order_expr = - | CStructRec - | CWfRec of constr_expr - | CMeasureRec of constr_expr * constr_expr option (** measure, relation *) + | CStructRec of lident + | CWfRec of lident * constr_expr + | CMeasureRec of lident option * constr_expr * constr_expr option (** argument, measure, relation *) (* Anonymous defs allowed ?? *) and local_binder_expr = diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 60610b92b861..db860e0c3bd4 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -196,10 +196,9 @@ and branch_expr_eq {CAst.v=(p1, e1)} {CAst.v=(p2, e2)} = List.equal (List.equal cases_pattern_expr_eq) p1 p2 && constr_expr_eq e1 e2 -and fix_expr_eq (id1,(j1, r1),bl1,a1,b1) (id2,(j2, r2),bl2,a2,b2) = +and fix_expr_eq (id1,r1,bl1,a1,b1) (id2,r2,bl2,a2,b2) = (eq_ast Id.equal id1 id2) && - Option.equal (eq_ast Id.equal) j1 j2 && - recursion_order_expr_eq r1 r2 && + Option.equal (eq_ast recursion_order_expr_eq) r1 r2 && List.equal local_binder_eq bl1 bl2 && constr_expr_eq a1 a2 && constr_expr_eq b1 b2 @@ -211,9 +210,11 @@ and cofix_expr_eq (id1,bl1,a1,b1) (id2,bl2,a2,b2) = constr_expr_eq b1 b2 and recursion_order_expr_eq r1 r2 = match r1, r2 with - | CStructRec, CStructRec -> true - | CWfRec e1, CWfRec e2 -> constr_expr_eq e1 e2 - | CMeasureRec (e1, o1), CMeasureRec (e2, o2) -> + | CStructRec i1, CStructRec i2 -> eq_ast Id.equal i1 i2 + | CWfRec (i1,e1), CWfRec (i2,e2) -> + constr_expr_eq e1 e2 + | CMeasureRec (i1, e1, o1), CMeasureRec (i2, e2, o2) -> + Option.equal (eq_ast Id.equal) i1 i2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq o1 o2 | _ -> false @@ -349,7 +350,7 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function (f (Option.fold_right (CAst.with_val (Name.fold_right g)) ona n)) acc po | CFix (_,l) -> let n' = List.fold_right (fun ( { CAst.v = id },_,_,_,_) -> g id) l n in - List.fold_right (fun (_,(_,o),lb,t,c) acc -> + List.fold_right (fun (_,ro,lb,t,c) acc -> fold_local_binders g f n' (fold_local_binders g f n acc t lb) c lb) l acc | CCoFix (_,_) -> diff --git a/interp/constrextern.ml b/interp/constrextern.ml index b89b6b57653b..3b169edaab9d 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -938,13 +938,12 @@ let rec extern inctx (custom,scopes as allscopes) vars r = let (assums,ids,bl) = extern_local_binder scopes vars bl in let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in - let n = - match fst nv.(i) with - | None -> None - | Some x -> Some (CAst.make @@ Name.get_id (List.nth assums x)) - in - let ro = extern_recursion_order scopes vars (snd nv.(i)) in - ((CAst.make fi), (n, ro), bl, extern_typ scopes vars0 ty, + let n = + match nv.(i) with + | None -> None + | Some x -> Some (CAst.make @@ CStructRec (CAst.make @@ Name.get_id (List.nth assums x))) + in + ((CAst.make fi), n, bl, extern_typ scopes vars0 ty, extern false scopes vars1 def)) idv in CFix (CAst.(make ?loc idv.(n)), Array.to_list listdecl) @@ -1159,13 +1158,6 @@ and extern_notation (custom,scopes as allscopes) lonely_seen vars t = function let lonely_seen = add_lonely keyrule lonely_seen in extern_notation allscopes lonely_seen vars t rules -and extern_recursion_order scopes vars = function - GStructRec -> CStructRec - | GWfRec c -> CWfRec (extern true scopes vars c) - | GMeasureRec (m,r) -> CMeasureRec (extern true scopes vars m, - Option.map (extern true scopes vars) r) - - let extern_glob_constr vars c = extern false (InConstrEntrySomeLevel,(None,[])) vars c @@ -1294,7 +1286,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with let v = Array.map3 (fun c t i -> Detyping.share_pattern_names glob_of_pat (i+1) [] def_avoid def_env sigma c (Patternops.lift_pattern n t)) bl tl ln in - GRec(GFix (Array.map (fun i -> Some i, GStructRec) ln,i),Array.of_list (List.rev lfi), + GRec(GFix (Array.map (fun i -> Some i) ln,i),Array.of_list (List.rev lfi), Array.map (fun (bl,_,_) -> bl) v, Array.map (fun (_,_,ty) -> ty) v, Array.map (fun (_,bd,_) -> bd) v) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 3329ba204798..c0801067ce80 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1845,51 +1845,44 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = in apply_impargs c env imp subscopes l loc - | CFix ({ CAst.loc = locid; v = iddef}, dl) -> + | CFix ({ CAst.loc = locid; v = iddef}, dl) -> let lf = List.map (fun ({CAst.v = id},_,_,_,_) -> id) dl in let dl = Array.of_list dl in - let n = - try List.index0 Id.equal iddef lf + let n = + try List.index0 Id.equal iddef lf with Not_found -> - raise (InternalizationError (locid,UnboundFixName (false,iddef))) - in - let idl_temp = Array.map - (fun (id,(n,order),bl,ty,_) -> - let intern_ro_arg f = - let before, after = split_at_annot bl n in - let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in - let ro = f (intern env') in - let n' = Option.map (fun _ -> List.count (fun c -> match DAst.get c with - | GLocalAssum _ -> true - | _ -> false (* remove let-ins *)) - rbefore) n in - n', ro, List.fold_left intern_local_binder (env',rbefore) after - in - let n, ro, (env',rbl) = - match order with - | CStructRec -> - intern_ro_arg (fun _ -> GStructRec) - | CWfRec c -> - intern_ro_arg (fun f -> GWfRec (f c)) - | CMeasureRec (m,r) -> - intern_ro_arg (fun f -> GMeasureRec (f m, Option.map f r)) - in - let bl = List.rev (List.map glob_local_binder_of_extended rbl) in - ((n, ro), bl, intern_type env' ty, env')) dl in + raise (InternalizationError (locid,UnboundFixName (false,iddef))) + in + let idl_temp = Array.map + (fun (id,recarg,bl,ty,_) -> + let recarg = Option.map (function { CAst.v = v } -> match v with + | CStructRec i -> i + | _ -> anomaly Pp.(str "Non-structural recursive argument in non-program fixpoint")) recarg + in + let before, after = split_at_annot bl recarg in + let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in + let n = Option.map (fun _ -> List.count (fun c -> match DAst.get c with + | GLocalAssum _ -> true + | _ -> false (* remove let-ins *)) + rbefore) recarg in + let (env',rbl) = List.fold_left intern_local_binder (env',rbefore) after in + let bl = List.rev (List.map glob_local_binder_of_extended rbl) in + (n, bl, intern_type env' ty, env')) dl in let idl = Array.map2 (fun (_,_,_,_,bd) (a,b,c,env') -> - let env'' = List.fold_left_i (fun i en name -> - let (_,bli,tyi,_) = idl_temp.(i) in - let fix_args = (List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli) in - push_name_env ntnvars (impls_type_list ~args:fix_args tyi) - en (CAst.make @@ Name name)) 0 env' lf in - (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in - DAst.make ?loc @@ - GRec (GFix - (Array.map (fun (ro,_,_,_) -> ro) idl,n), + let env'' = List.fold_left_i (fun i en name -> + let (_,bli,tyi,_) = idl_temp.(i) in + let fix_args = (List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli) in + push_name_env ntnvars (impls_type_list ~args:fix_args tyi) + en (CAst.make @@ Name name)) 0 env' lf in + (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in + DAst.make ?loc @@ + GRec (GFix + (Array.map (fun (ro,_,_,_) -> ro) idl,n), Array.of_list lf, Array.map (fun (_,bl,_,_) -> bl) idl, Array.map (fun (_,_,ty,_) -> ty) idl, Array.map (fun (_,_,_,bd) -> bd) idl) + | CCoFix ({ CAst.loc = locid; v = iddef }, dl) -> let lf = List.map (fun ({CAst.v = id},_,_,_) -> id) dl in let dl = Array.of_list dl in diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 9801e56ca136..7f084fffdd02 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -957,7 +957,7 @@ let match_fix_kind fk1 fk2 = match (fk1,fk2) with | GCoFix n1, GCoFix n2 -> Int.equal n1 n2 | GFix (nl1,n1), GFix (nl2,n2) -> - let test (n1, _) (n2, _) = match n1, n2 with + let test n1 n2 = match n1, n2 with | _, None -> true | Some id1, Some id2 -> Int.equal id1 id2 | _ -> false diff --git a/interp/notation_term.ml b/interp/notation_term.ml index 6fe20486dcd9..5024f5c26f0b 100644 --- a/interp/notation_term.ml +++ b/interp/notation_term.ml @@ -38,7 +38,7 @@ type notation_constr = notation_constr * notation_constr | NIf of notation_constr * (Name.t * notation_constr option) * notation_constr * notation_constr - | NRec of fix_kind * Id.t array * + | NRec of glob_fix_kind * Id.t array * (Name.t * notation_constr option * notation_constr) list array * notation_constr array * notation_constr array | NSort of glob_sort diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 0586dda5557c..77861550924f 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -56,10 +56,10 @@ let mk_fixb (id,bl,ann,body,(loc,tyc)) : fix_expr = (id,ann,bl,ty,body) let mk_cofixb (id,bl,ann,body,(loc,tyc)) : cofix_expr = - let _ = Option.map (fun { CAst.loc = aloc } -> + Option.iter (fun { CAst.loc = aloc } -> CErrors.user_err ?loc:aloc ~hdr:"Constr:mk_cofixb" - (Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in + (Pp.str"Annotation forbidden in cofix expression.")) ann; let ty = match tyc with Some ty -> ty | None -> CAst.make @@ CHole (None, IntroAnonymous, None) in @@ -440,10 +440,10 @@ GRAMMAR EXTEND Gram ] ] ; fixannot: - [ [ "{"; IDENT "struct"; id=identref; "}" -> { (Some id, CStructRec) } - | "{"; IDENT "wf"; rel=constr; id=OPT identref; "}" -> { (id, CWfRec rel) } + [ [ "{"; IDENT "struct"; id=identref; "}" -> { CStructRec id } + | "{"; IDENT "wf"; rel=constr; id=identref; "}" -> { CWfRec(id,rel) } | "{"; IDENT "measure"; m=constr; id=OPT identref; - rel=OPT constr; "}" -> { (id, CMeasureRec (m,rel)) } + rel=OPT constr; "}" -> { CMeasureRec (id,m,rel) } ] ] ; impl_name_head: @@ -452,9 +452,9 @@ GRAMMAR EXTEND Gram binders_fixannot: [ [ na = impl_name_head; assum = impl_ident_tail; bl = binders_fixannot -> { (assum na :: fst bl), snd bl } - | f = fixannot -> { [], f } + | f = fixannot -> { [], Some (CAst.make ~loc f) } | b = binder; bl = binders_fixannot -> { b @ fst bl, snd bl } - | -> { [], (None, CStructRec) } + | -> { [], None } ] ] ; open_binders: diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 5d8897cb47ea..84d19730fa96 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -191,7 +191,7 @@ module Constr : val binder : local_binder_expr list Entry.t (* closed_binder or variable *) val binders : local_binder_expr list Entry.t (* list of binder *) val open_binders : local_binder_expr list Entry.t - val binders_fixannot : (local_binder_expr list * (lident option * recursion_order_expr)) Entry.t + val binders_fixannot : (local_binder_expr list * recursion_order_expr CAst.t option) Entry.t val typeclass_constraint : (lname * bool * constr_expr) Entry.t val record_declaration : constr_expr Entry.t val appl_arg : (constr_expr * explicitation CAst.t option) Entry.t diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index 4e8cf80ed2a7..a3973732adcc 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -179,8 +179,10 @@ let () = VERNAC COMMAND EXTEND Function | ![ proof ] ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] => { let hard = List.exists (function - | _,((_,(_,(CMeasureRec _|CWfRec _)),_,_,_),_) -> true - | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in + | _,((_,(Some { CAst.v = CMeasureRec _ } + | Some { CAst.v = CWfRec _}),_,_,_),_) -> true + | _,((_,Some { CAst.v = CStructRec _ },_,_,_),_) + | _,((_,None,_,_,_),_) -> false) recsl in match Vernac_classifier.classify_vernac (Vernacexpr.(VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)))) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index e582362e257a..6494e90a0325 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -469,11 +469,6 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas CAst.(with_val (fun x -> x)) (Constrexpr_ops.names_of_local_assums args) in - match wf_arg with - | None -> - if Int.equal (List.length names) 1 then 1 - else error "Recursive argument must be specified" - | Some wf_arg -> List.index Name.equal (Name wf_arg) names in let unbounded_eq = @@ -575,7 +570,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas in wf_rel_with_mes,false in - register_wf ~is_mes:is_mes fname rec_impls wf_rel_from_mes (Some wf_arg) + register_wf ~is_mes:is_mes fname rec_impls wf_rel_from_mes wf_arg using_lemmas args ret_type body let map_option f = function @@ -623,15 +618,15 @@ and rebuild_nal aux bk bl' nal typ = let rebuild_bl aux bl typ = rebuild_bl aux bl typ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = - let fixl,ntns = ComFixpoint.extract_fixpoint_components false fixpoint_exprl in + let fixl,ntns = ComFixpoint.extract_fixpoint_components ~structonly:false fixpoint_exprl in let ((_,_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl ntns in let constr_expr_typel = with_full_print (List.map (fun c -> Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx) (EConstr.of_constr c))) typel in let fixpoint_exprl_with_new_bl = - List.map2 (fun ((lna,(rec_arg_opt,rec_order),bl,ret_typ,opt_body),notation_list) fix_typ -> + List.map2 (fun ((lna,rec_order_opt,bl,ret_typ,opt_body),notation_list) fix_typ -> let new_bl',new_ret_type = rebuild_bl [] bl fix_typ in - (((lna,(rec_arg_opt,rec_order),new_bl',new_ret_type,opt_body),notation_list):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) + (((lna,rec_order_opt,new_bl',new_ret_type,opt_body),notation_list):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) ) fixpoint_exprl constr_expr_typel in @@ -643,7 +638,7 @@ let do_generate_principle ~pstate pconstants on_error register_built interactive List.iter (fun (_,l) -> if not (List.is_empty l) then error "Function does not support notations for now") fixpoint_exprl; let pstate, _is_struct = match fixpoint_exprl with - | [((_,(wf_x,Constrexpr.CWfRec wf_rel),_,_,_),_) as fixpoint_expr] -> + | [((_,Some {CAst.v = Constrexpr.CWfRec (wf_x,wf_rel)},_,_,_),_) as fixpoint_expr] -> let (((({CAst.v=name},pl),_,args,types,body)),_) as fixpoint_expr = match recompute_binder_list [fixpoint_expr] with | [e] -> e @@ -665,9 +660,9 @@ let do_generate_principle ~pstate pconstants on_error register_built interactive true in if register_built - then register_wf name rec_impls wf_rel (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook, false + then register_wf name rec_impls wf_rel wf_x.CAst.v using_lemmas args types body pre_hook, false else pstate, false - |[((_,(wf_x,Constrexpr.CMeasureRec(wf_mes,wf_rel_opt)),_,_,_),_) as fixpoint_expr] -> + |[((_,Some {CAst.v = Constrexpr.CMeasureRec(wf_x,wf_mes,wf_rel_opt)},_,_,_),_) as fixpoint_expr] -> let (((({CAst.v=name},_),_,args,types,body)),_) as fixpoint_expr = match recompute_binder_list [fixpoint_expr] with | [e] -> e @@ -692,9 +687,9 @@ let do_generate_principle ~pstate pconstants on_error register_built interactive then register_mes name rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook, true else pstate, true | _ -> - List.iter (function ((_na,(_,ord),_args,_body,_type),_not) -> + List.iter (function ((_na,ord,_args,_body,_type),_not) -> match ord with - | Constrexpr.CMeasureRec _ | Constrexpr.CWfRec _ -> + | Some { CAst.v = (Constrexpr.CMeasureRec _ | Constrexpr.CWfRec _) } -> error ("Cannot use mutual definition with well-founded recursion or measure") | _ -> () @@ -869,38 +864,42 @@ let make_graph ~pstate (f_ref : GlobRef.t) = ) () in - let (nal_tas,b,t) = get_args extern_body extern_type in - let expr_list = - match b.CAst.v with - | Constrexpr.CFix(l_id,fixexprl) -> - let l = - List.map - (fun (id,(n,recexp),bl,t,b) -> - let { CAst.loc; v=rec_id } = Option.get n in - let new_args = - List.flatten - (List.map - (function - | Constrexpr.CLocalDef (na,_,_)-> [] - | Constrexpr.CLocalAssum (nal,_,_) -> - List.map - (fun {CAst.loc;v=n} -> CAst.make ?loc @@ - CRef(Libnames.qualid_of_ident ?loc @@ Nameops.Name.get_id n,None)) - nal - | Constrexpr.CLocalPattern _ -> assert false - ) - nal_tas - ) - in - let b' = add_args id.CAst.v new_args b in - ((((id,None), ( Some CAst.(make rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) - ) - fixexprl - in - l + let (nal_tas,b,t) = get_args extern_body extern_type in + let expr_list = + match b.CAst.v with + | Constrexpr.CFix(l_id,fixexprl) -> + let l = + List.map + (fun (id,recexp,bl,t,b) -> + let { CAst.loc; v=rec_id } = match Option.get recexp with + | { CAst.v = CStructRec id } -> id + | { CAst.v = CWfRec (id,_) } -> id + | { CAst.v = CMeasureRec (oid,_,_) } -> Option.get oid + in + let new_args = + List.flatten + (List.map + (function + | Constrexpr.CLocalDef (na,_,_)-> [] + | Constrexpr.CLocalAssum (nal,_,_) -> + List.map + (fun {CAst.loc;v=n} -> CAst.make ?loc @@ + CRef(Libnames.qualid_of_ident ?loc @@ Nameops.Name.get_id n,None)) + nal + | Constrexpr.CLocalPattern _ -> assert false + ) + nal_tas + ) + in + let b' = add_args id.CAst.v new_args b in + ((((id,None), ( Some (CAst.make (CStructRec (CAst.make rec_id)))),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) + ) + fixexprl + in + l | _ -> let id = Label.to_id (Constant.label c) in - [((CAst.make id,None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]] + [((CAst.make id,None),None,nal_tas,t,Some b),[]] in let mp = Constant.modpath c in let pstate = do_generate_principle ~pstate [c,Univ.Instance.empty] error_error false false expr_list in diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 7cd62f4ead36..f44962f213fd 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -1200,7 +1200,7 @@ let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with | [BFcast], { v = CCast (c, Glob_term.CastConv t) } -> [Bcast t], c | BFrec (has_str, has_cast) :: h, - { v = CFix ( _, [_, (Some locn, CStructRec), bl, t, c]) } -> + { v = CFix ( _, [_, Some {CAst.v = CStructRec locn}, bl, t, c]) } -> let bs = format_local_binders h bl in let bstr = if has_str then [Bstruct (Name locn.CAst.v)] else [] in bs @ bstr @ (if has_cast then [Bcast t] else []), c @@ -1424,7 +1424,7 @@ ARGUMENT EXTEND ssrfixfwd TYPED AS (ident * ssrfwd) PRINTED BY { pr_ssrfixfwd } | [] -> CErrors.user_err (Pp.str "Bad structural argument") in loop (names_of_local_assums lb) in let h' = BFrec (has_struct, has_cast) :: binders_fmts bs in - let fix = CAst.make ~loc @@ CFix (lid, [lid, (Some i, CStructRec), lb, t', c']) in + let fix = CAst.make ~loc @@ CFix (lid, [lid, (Some (CAst.make (CStructRec i))), lb, t', c']) in id, ((fk, h'), { ac with body = fix }) } END diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index eaa573633674..062e3ca8b2ca 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -653,7 +653,7 @@ let detype_fix detype flags avoid env sigma (vn,_ as nvn) (names,tys,bodies) = let v = Array.map3 (fun c t i -> share_names detype flags (i+1) [] def_avoid def_env sigma c (lift n t)) bodies tys vn in - GRec(GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi), + GRec(GFix (Array.map (fun i -> Some i) (fst nvn), snd nvn),Array.of_list (List.rev lfi), Array.map (fun (bl,_,_) -> bl) v, Array.map (fun (_,_,ty) -> ty) v, Array.map (fun (_,bd,_) -> bd) v) diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 6da168711c16..85b9faac7772 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -106,19 +106,9 @@ let glob_decl_eq f (na1, bk1, c1, t1) (na2, bk2, c2, t2) = Name.equal na1 na2 && binding_kind_eq bk1 bk2 && Option.equal f c1 c2 && f t1 t2 -let fix_recursion_order_eq f o1 o2 = match o1, o2 with - | GStructRec, GStructRec -> true - | GWfRec c1, GWfRec c2 -> f c1 c2 - | GMeasureRec (c1, o1), GMeasureRec (c2, o2) -> - f c1 c2 && Option.equal f o1 o2 - | (GStructRec | GWfRec _ | GMeasureRec _), _ -> false - -let fix_kind_eq f k1 k2 = match k1, k2 with +let fix_kind_eq k1 k2 = match k1, k2 with | GFix (a1, i1), GFix (a2, i2) -> - let eq (i1, o1) (i2, o2) = - Option.equal Int.equal i1 i2 && fix_recursion_order_eq f o1 o2 - in - Int.equal i1 i2 && Array.equal eq a1 a2 + Int.equal i1 i2 && Array.equal (Option.equal Int.equal) a1 a2 | GCoFix i1, GCoFix i2 -> Int.equal i1 i2 | (GFix _ | GCoFix _), _ -> false @@ -150,7 +140,7 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with f m1 m2 && Name.equal pat1 pat2 && Option.equal f p1 p2 && f c1 c2 && f t1 t2 | GRec (kn1, id1, decl1, t1, c1), GRec (kn2, id2, decl2, t2, c2) -> - fix_kind_eq f kn1 kn2 && Array.equal Id.equal id1 id2 && + fix_kind_eq kn1 kn2 && Array.equal Id.equal id1 id2 && Array.equal (fun l1 l2 -> List.equal (glob_decl_eq f) l1 l2) decl1 decl2 && Array.equal f c1 c2 && Array.equal f t1 t2 | GSort s1, GSort s2 -> glob_sort_eq s1 s2 diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index c57cf88cc61a..02cb294f6d7d 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -41,6 +41,12 @@ type glob_constraint = glob_level * Univ.constraint_type * glob_level type sort_info = (Libnames.qualid * int) option list type glob_sort = sort_info glob_sort_gen +type glob_recarg = int option + +and glob_fix_kind = + | GFix of (glob_recarg array * int) + | GCoFix of int + (** Casts *) type 'a cast_type = @@ -78,7 +84,7 @@ type 'a glob_constr_r = (** [GCases(style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in [MatchStyle]) *) | GLetTuple of Name.t list * (Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g | GIf of 'a glob_constr_g * (Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g - | GRec of 'a fix_kind_g * Id.t array * 'a glob_decl_g list array * + | GRec of glob_fix_kind * Id.t array * 'a glob_decl_g list array * 'a glob_constr_g array * 'a glob_constr_g array | GSort of glob_sort | GHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option @@ -88,15 +94,6 @@ and 'a glob_constr_g = ('a glob_constr_r, 'a) DAst.t and 'a glob_decl_g = Name.t * binding_kind * 'a glob_constr_g option * 'a glob_constr_g -and 'a fix_recursion_order_g = - | GStructRec - | GWfRec of 'a glob_constr_g - | GMeasureRec of 'a glob_constr_g * 'a glob_constr_g option - -and 'a fix_kind_g = - | GFix of ((int option * 'a fix_recursion_order_g) array * int) - | GCoFix of int - and 'a predicate_pattern_g = Name.t * (inductive * Name.t list) CAst.t option (** [(na,id)] = "as 'na' in 'id'" where if [id] is [Some(l,I,k,args)]. *) @@ -117,9 +114,7 @@ type tomatch_tuples = [ `any ] tomatch_tuples_g type cases_clause = [ `any ] cases_clause_g type cases_clauses = [ `any ] cases_clauses_g type glob_decl = [ `any ] glob_decl_g -type fix_kind = [ `any ] fix_kind_g type predicate_pattern = [ `any ] predicate_pattern_g -type fix_recursion_order = [ `any ] fix_recursion_order_g type any_glob_constr = AnyGlobConstr : 'r glob_constr_g -> any_glob_constr diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index b29afd1fd2b1..c788efda483f 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -470,17 +470,19 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function PCase (info, pred, pat_of_raw metas vars c, brs) | GRec (GFix (ln,n), ids, decls, tl, cl) -> - if Array.exists (function (Some n, GStructRec) -> false | _ -> true) ln then - err ?loc (Pp.str "\"struct\" annotation is expected.") - else - let ln = Array.map (fst %> Option.get) ln in - let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in - let tl = Array.map (fun (ctx,tl) -> it_mkPProd_or_LetIn tl ctx) ctxtl in - let vars = Array.fold_left (fun vars na -> Name na::vars) vars ids in - let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls cl in - let cl = Array.map (fun (ctx,cl) -> it_mkPLambda_or_LetIn cl ctx) ctxtl in - let names = Array.map (fun id -> Name id) ids in - PFix ((ln,n), (names, tl, cl)) + let get_struct_arg = function + | Some n -> n + | None -> err ?loc (Pp.str "\"struct\" annotation is expected.") + (* TODO why can't the annotation be omitted? *) + in + let ln = Array.map get_struct_arg ln in + let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in + let tl = Array.map (fun (ctx,tl) -> it_mkPProd_or_LetIn tl ctx) ctxtl in + let vars = Array.fold_left (fun vars na -> Name na::vars) vars ids in + let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls cl in + let cl = Array.map (fun (ctx,cl) -> it_mkPLambda_or_LetIn cl ctx) ctxtl in + let names = Array.map (fun id -> Name id) ids in + PFix ((ln,n), (names, tl, cl)) | GRec (GCoFix n, ids, decls, tl, cl) -> let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 0f7676cd1929..48d981082cd1 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -607,10 +607,10 @@ let rec pretype ~program_mode ~poly k0 resolve_tc (tycon : type_constraint) (env fixpoints ?) *) let possible_indexes = Array.to_list (Array.mapi - (fun i (n,_) -> match n with + (fun i annot -> match annot with | Some n -> [n] | None -> List.map_i (fun i _ -> i) 0 ctxtv.(i)) - vn) + vn) in let fixdecls = (names,ftys,fdefs) in let indexes = esearch_guard ?loc !!env sigma possible_indexes fixdecls in diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 0ae3de73219b..4dc3ba8789b4 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -399,12 +399,12 @@ let tag_var = tag Tag.variable pr_opt_type_spc pr t ++ str " :=" ++ pr_sep_com (fun () -> brk(1,2)) (pr_body ltop) c - let pr_guard_annot pr_aux bl (n,ro) = - match n with + let pr_guard_annot pr_aux bl ro = + match ro with | None -> mt () - | Some {loc; v = id} -> + | Some {loc; v = ro} -> match (ro : Constrexpr.recursion_order_expr) with - | CStructRec -> + | CStructRec { v = id } -> let names_of_binder = function | CLocalAssum (nal,_,_) -> nal | CLocalDef (_,_,_) -> [] @@ -413,10 +413,11 @@ let tag_var = tag Tag.variable if List.length ids > 1 then spc() ++ str "{" ++ keyword "struct" ++ spc () ++ pr_id id ++ str"}" else mt() - | CWfRec c -> - spc() ++ str "{" ++ keyword "wf" ++ spc () ++ pr_aux c ++ spc() ++ pr_id id ++ str"}" - | CMeasureRec (m,r) -> - spc() ++ str "{" ++ keyword "measure" ++ spc () ++ pr_aux m ++ spc() ++ pr_id id++ + | CWfRec (id,c) -> + spc() ++ str "{" ++ keyword "wf" ++ spc () ++ pr_aux c ++ spc() ++ pr_lident id ++ str"}" + | CMeasureRec (id,m,r) -> + spc() ++ str "{" ++ keyword "measure" ++ spc () ++ pr_aux m ++ + match id with None -> mt() | Some id -> spc () ++ pr_lident id ++ (match r with None -> mt() | Some r -> str" on " ++ pr_aux r) ++ str"}" let pr_fixdecl pr prd dangling_with_for ({v=id},ro,bl,t,c) = diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index db1687a49ba4..2e00b1289961 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -37,7 +37,7 @@ val pr_glob_level : Glob_term.glob_level -> Pp.t val pr_glob_sort : Glob_term.glob_sort -> Pp.t val pr_guard_annot : (constr_expr -> Pp.t) -> local_binder_expr list -> - lident option * recursion_order_expr -> + recursion_order_expr CAst.t option -> Pp.t val pr_record_body : (qualid * constr_expr) list -> Pp.t diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index d042a1d6507b..f378a5d2ddc9 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -438,18 +438,18 @@ let match_goals ot nt = | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (2)") in let recursion_order_expr ogname exp exp2 = - match exp, exp2 with - | CStructRec, CStructRec -> () - | CWfRec c, CWfRec c2 -> + match exp.CAst.v, exp2.CAst.v with + | CStructRec _, CStructRec _ -> () + | CWfRec (_,c), CWfRec (_,c2) -> constr_expr ogname c c2 - | CMeasureRec (m,r), CMeasureRec (m2,r2) -> + | CMeasureRec (_,m,r), CMeasureRec (_,m2,r2) -> constr_expr ogname m m2; constr_expr_opt ogname r r2 | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (3)") in let fix_expr ogname exp exp2 = - let (l,(lo,ro),lb,ce1,ce2), (l2,(lo2,ro2),lb2,ce12,ce22) = exp,exp2 in - recursion_order_expr ogname ro ro2; + let (l,ro,lb,ce1,ce2), (l2,ro2,lb2,ce12,ce22) = exp,exp2 in + Option.iter2 (recursion_order_expr ogname) ro ro2; iter2 (local_binder_expr ogname) lb lb2; constr_expr ogname ce1 ce12; constr_expr ogname ce2 ce22 diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 2aadbd224fab..1912646ffd4e 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -329,16 +329,27 @@ let declare_cofixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,c List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; pstate -let extract_decreasing_argument limit = function - | (na,CStructRec) -> na - | (na,_) when not limit -> na +let extract_decreasing_argument ~structonly = function { CAst.v = v } -> match v with + | CStructRec na -> na + | (CWfRec (na,_) | CMeasureRec (Some na,_,_)) when not structonly -> na + | CMeasureRec (None,_,_) when not structonly -> + user_err Pp.(str "Decreasing argument must be specificed in measure clause.") | _ -> user_err Pp.(str - "Only structural decreasing is supported for a non-Program Fixpoint") + "Well-founded induction requires Program Fixpoint or Function.") -let extract_fixpoint_components limit l = +let extract_fixpoint_components ~structonly l = let fixl, ntnl = List.split l in let fixl = List.map (fun (({CAst.v=id},pl),ann,bl,typ,def) -> - let ann = extract_decreasing_argument limit ann in + (* This is a special case: if there's only one binder, we pick it as the + recursive argument if none is provided. *) + let ann = Option.map (fun ann -> match bl, ann with + | [CLocalAssum([{ CAst.v = Name x }],_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } -> + CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel) + | [CLocalDef({ CAst.v = Name x },_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } -> + CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel) + | _, x -> x) ann + in + let ann = Option.map (extract_decreasing_argument ~structonly) ann in {fix_name = id; fix_annot = ann; fix_univs = pl; fix_binders = bl; fix_body = def; fix_type = typ}) fixl in fixl, List.flatten ntnl @@ -356,7 +367,7 @@ let check_safe () = flags.check_universes && flags.check_guarded let do_fixpoint ~ontop local poly l = - let fixl, ntns = extract_fixpoint_components true l in + let fixl, ntns = extract_fixpoint_components ~structonly:true l in let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl ntns in let possible_indexes = List.map compute_possible_guardness_evidences info in diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index 15ff5f449876..5937842f1738 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -62,7 +62,7 @@ val interp_recursive : (** Extracting the semantical components out of the raw syntax of (co)fixpoints declarations *) -val extract_fixpoint_components : bool -> +val extract_fixpoint_components : structonly:bool -> (fixpoint_expr * decl_notation list) list -> structured_fixpoint_expr list * decl_notation list diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 350b2d294575..20a2db7ca2f6 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -85,7 +85,7 @@ let rec telescope sigma l = let nf_evar_context sigma ctx = List.map (map_constr (fun c -> Evarutil.nf_evar sigma c)) ctx -let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = +let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = let open EConstr in let open Vars in let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in @@ -304,22 +304,26 @@ let do_program_recursive local poly fixkind fixl ntns = let do_program_fixpoint local poly l = let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in match g, l with - | [(n, CWfRec r)], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] -> - let recarg = - match n with - | Some n -> mkIdentC n.CAst.v - | None -> - user_err ~hdr:"do_program_fixpoint" - (str "Recursive argument required for well-founded fixpoints") - in build_wellfounded (id, pl, n, bl, typ, out_def def) poly r recarg ntn + | [Some { CAst.v = CWfRec (n,r) }], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] -> + let recarg = mkIdentC n.CAst.v in + build_wellfounded (id, pl, bl, typ, out_def def) poly r recarg ntn - | [(n, CMeasureRec (m, r))], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] -> - build_wellfounded (id, pl, n, bl, typ, out_def def) poly + | [Some { CAst.v = CMeasureRec (n, m, r) }], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] -> + (* We resolve here a clash between the syntax of Program Fixpoint and the one of funind *) + let r = match n, r with + | Some id, None -> + let loc = id.CAst.loc in + Some (CAst.make ?loc @@ CRef(qualid_of_ident ?loc id.CAst.v,None)) + | Some _, Some _ -> + user_err Pp.(str"Measure takes only two arguments in Program Fixpoint.") + | _, _ -> r + in + build_wellfounded (id, pl, bl, typ, out_def def) poly (Option.default (CAst.make @@ CRef (lt_ref,None)) r) m ntn - | _, _ when List.for_all (fun (n, ro) -> ro == CStructRec) g -> - let fixl,ntns = extract_fixpoint_components true l in - let fixkind = Obligations.IsFixpoint g in + | _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g -> + let fixl,ntns = extract_fixpoint_components ~structonly:true l in + let fixkind = Obligations.IsFixpoint (List.map (fun d -> d.fix_annot) fixl) in do_program_recursive local poly fixkind fixl ntns | _, _ -> diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 07194578c1be..1b1c618dc7fe 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -295,7 +295,7 @@ type obligation = type obligations = (obligation array * int) type fixpoint_kind = - | IsFixpoint of (lident option * Constrexpr.recursion_order_expr) list + | IsFixpoint of lident option list | IsCoFixpoint type notations = (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list @@ -486,7 +486,7 @@ let rec lam_index n t acc = lam_index n b (succ acc) | _ -> raise Not_found -let compute_possible_guardness_evidences (n,_) fixbody fixtype = +let compute_possible_guardness_evidences n fixbody fixtype = match n with | Some { CAst.loc; v = n } -> [lam_index n fixbody 0] | None -> diff --git a/vernac/obligations.mli b/vernac/obligations.mli index b1b7b1ec90ef..d25daeed9cd2 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -70,7 +70,7 @@ type notations = (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list type fixpoint_kind = - | IsFixpoint of (lident option * Constrexpr.recursion_order_expr) list + | IsFixpoint of lident option list | IsCoFixpoint val add_mutual_definitions : diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index ebfc47352215..8eacaed2eb9e 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -129,7 +129,7 @@ type definition_expr = * constr_expr option type fixpoint_expr = - ident_decl * (lident option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr option + ident_decl * recursion_order_expr CAst.t option * local_binder_expr list * constr_expr * constr_expr option type cofixpoint_expr = ident_decl * local_binder_expr list * constr_expr * constr_expr option