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