diff options
Diffstat (limited to 'vernac/comProgramFixpoint.ml')
| -rw-r--r-- | vernac/comProgramFixpoint.ml | 51 |
1 files changed, 24 insertions, 27 deletions
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index ad7c65b70c..69e2a209eb 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 @@ -230,12 +230,9 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = in (* XXX: Capturing sigma here... bad bad *) let hook = Lemmas.mk_hook (hook sigma) in - (* XXX: Grounding non-ground terms here... bad bad *) - let fullcoqc = EConstr.to_constr ~abort_on_undefined_evars:false sigma def in - let fullctyp = EConstr.to_constr sigma typ in Obligations.check_evars env sigma; let evars, _, evars_def, evars_typ = - Obligations.eterm_obligations env recname sigma 0 fullcoqc fullctyp + Obligations.eterm_obligations env recname sigma 0 def typ in let ctx = Evd.evar_universe_context sigma in ignore(Obligations.add_definition recname ~term:evars_def ~univdecl:decl @@ -246,7 +243,7 @@ let out_def = function | None -> user_err Pp.(str "Program Fixpoint needs defined bodies.") let collect_evars_of_term evd c ty = - let evars = Evar.Set.union (Evd.evars_of_term c) (Evd.evars_of_term ty) in + let evars = Evar.Set.union (Evd.evars_of_term evd c) (Evd.evars_of_term evd ty) in Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev)) evars (Evd.from_ctx (Evd.evar_universe_context evd)) @@ -262,17 +259,13 @@ let do_program_recursive local poly fixkind fixl ntns = let evd = nf_evar_map_undefined evd in let collect_evars id def typ imps = (* Generalize by the recursive prototypes *) - let def = - EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign) - and typ = - (* Worrying... *) - EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign) - in + let def = nf_evar evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign) in + let typ = nf_evar evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign) in let evm = collect_evars_of_term evd def typ in let evars, _, def, typ = Obligations.eterm_obligations env id evm - (List.length rec_sign) def typ - in (id, def, typ, imps, evars) + (List.length rec_sign) def typ in + (id, def, typ, imps, evars) in let (fixnames,fixrs,fixdefs,fixtypes) = fix in let fiximps = List.map pi2 info in @@ -304,22 +297,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 | _, _ -> |