open Closure open RedFlags open Declarations open Entries open Libobject open Pattern open Matching open Pp open Glob_term open Sign open Tacred open Util open Names open Nameops open Libnames open Nametab open Pfedit open Proof_type open Refiner open Tacmach open Tactic_debug open Topconstr open Term open Tacexpr open Safe_typing open Typing open Hiddentac open Genarg open Decl_kinds open Mod_subst open Printer open Inductiveops open Syntax_def open Environ open Tactics open Tacticals open Tacinterp open Vernacexpr open Notation open Evd open Evarutil module SPretyping = Subtac_pretyping.Pretyping open Subtac_utils open Pretyping open Subtac_obligations (*********************************************************************) (* Functions to parse and interpret constructions *) let evar_nf isevars c = Evarutil.nf_evar !isevars c let interp_gen kind isevars env ?(impls=Constrintern.empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=([],[])) c = let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars ( !isevars) env c in let c' = SPretyping.understand_tcc_evars isevars env kind c' in evar_nf isevars c' let interp_constr isevars env c = interp_gen (OfType None) isevars env c let interp_type_evars isevars env ?(impls=Constrintern.empty_internalization_env) c = interp_gen IsType isevars env ~impls c let interp_casted_constr isevars env ?(impls=Constrintern.empty_internalization_env) c typ = interp_gen (OfType (Some typ)) isevars env ~impls c let interp_casted_constr_evars isevars env ?(impls=Constrintern.empty_internalization_env) c typ = interp_gen (OfType (Some typ)) isevars env ~impls c let interp_open_constr isevars env c = msgnl (str "Pretyping " ++ my_print_constr_expr c); let c = Constrintern.intern_constr ( !isevars) env c in let c' = SPretyping.understand_tcc_evars isevars env (OfType None) c in evar_nf isevars c' let interp_constr_judgment isevars env c = let j = SPretyping.understand_judgment_tcc isevars env (Constrintern.intern_constr ( !isevars) env c) in { uj_val = evar_nf isevars j.uj_val; uj_type = evar_nf isevars j.uj_type } let locate_if_isevar loc na = function | GHole _ -> (try match na with | Name id -> glob_constr_of_aconstr loc (Reserve.find_reserved_type id) | Anonymous -> raise Not_found with Not_found -> GHole (loc, Evd.BinderType na)) | x -> x let interp_binder sigma env na t = let t = Constrintern.intern_gen true ( !sigma) env t in SPretyping.understand_tcc_evars sigma env IsType (locate_if_isevar (loc_of_glob_constr t) na t) let interp_context_evars evdref env params = let int_env, bl = Constrintern.intern_context false !evdref env Constrintern.empty_internalization_env params in let (env, par, _, impls) = List.fold_left (fun (env,params,n,impls) (na, k, b, t) -> match b with None -> let t' = locate_if_isevar (loc_of_glob_constr t) na t in let t = SPretyping.understand_tcc_evars evdref env IsType t' in let d = (na,None,t) in let impls = if k = Implicit then let na = match na with Name n -> Some n | Anonymous -> None in (ExplByPos (n, na), (true, true, true)) :: impls else impls in (push_rel d env, d::params, succ n, impls) | Some b -> let c = SPretyping.understand_judgment_tcc evdref env b in let d = (na, Some c.uj_val, c.uj_type) in (push_rel d env,d::params, succ n, impls)) (env,[],1,[]) (List.rev bl) in (env, par), impls (* try to find non recursive definitions *) let list_chop_hd i l = match list_chop i l with | (l1,x::l2) -> (l1,x,l2) | (x :: [], l2) -> ([], x, []) | _ -> assert(false) let collect_non_rec env = let rec searchrec lnonrec lnamerec ldefrec larrec nrec = try let i = list_try_find_i (fun i f -> if List.for_all (fun (_, def) -> not (Termops.occur_var env f def)) ldefrec then i else failwith "try_find_i") 0 lnamerec in let (lf1,f,lf2) = list_chop_hd i lnamerec in let (ldef1,def,ldef2) = list_chop_hd i ldefrec in let (lar1,ar,lar2) = list_chop_hd i larrec in let newlnv = try match list_chop i nrec with | (lnv1,_::lnv2) -> (lnv1@lnv2) | _ -> [] (* nrec=[] for cofixpoints *) with Failure "list_chop" -> [] in searchrec ((f,def,ar)::lnonrec) (lf1@lf2) (ldef1@ldef2) (lar1@lar2) newlnv with Failure "try_find_i" -> (List.rev lnonrec, (Array.of_list lnamerec, Array.of_list ldefrec, Array.of_list larrec, Array.of_list nrec)) in searchrec [] let list_of_local_binders l = let rec aux acc = function Topconstr.LocalRawDef (n, c) :: tl -> aux ((n, Some c, None) :: acc) tl | Topconstr.LocalRawAssum (nl, k, c) :: tl -> aux (List.fold_left (fun acc n -> (n, None, Some c) :: acc) acc nl) tl | [] -> List.rev acc in aux [] l let lift_binders k n l = let rec aux n = function | (id, t, c) :: tl -> (id, Option.map (liftn k n) t, liftn k n c) :: aux (pred n) tl | [] -> [] in aux n l let rec gen_rels = function 0 -> [] | n -> mkRel n :: gen_rels (pred n) let split_args n rel = match list_chop ((List.length rel) - n) rel with (l1, x :: l2) -> l1, x, l2 | _ -> assert(false) open Coqlib let sigT = Lazy.lazy_from_fun build_sigma_type let sigT_info = lazy { ci_ind = destInd (Lazy.force sigT).typ; ci_npar = 2; ci_cstr_ndecls = [|2|]; ci_pp_info = { ind_nargs = 0; style = LetStyle } } let rec telescope = function | [] -> assert false | [(n, None, t)] -> t, [n, Some (mkRel 1), t], mkRel 1 | (n, None, t) :: tl -> let ty, tys, (k, constr) = List.fold_left (fun (ty, tys, (k, constr)) (n, b, t) -> let pred = mkLambda (n, t, ty) in let sigty = mkApp ((Lazy.force sigT).typ, [|t; pred|]) in let intro = mkApp ((Lazy.force sigT).intro, [|lift k t; lift k pred; mkRel k; constr|]) in (sigty, pred :: tys, (succ k, intro))) (t, [], (2, mkRel 1)) tl in let (last, subst) = List.fold_right2 (fun pred (n, b, t) (prev, subst) -> let proj1 = applistc (Lazy.force sigT).proj1 [t; pred; prev] in let proj2 = applistc (Lazy.force sigT).proj2 [t; pred; prev] in (lift 1 proj2, (n, Some proj1, t) :: subst)) (List.rev tys) tl (mkRel 1, []) in ty, ((n, Some last, t) :: subst), constr | (n, Some b, t) :: tl -> let ty, subst, term = telescope tl in ty, ((n, Some b, t) :: subst), lift 1 term let nf_evar_context isevars ctx = List.map (fun (n, b, t) -> (n, Option.map (Evarutil.nf_evar isevars) b, Evarutil.nf_evar isevars t)) ctx let build_wellfounded (recname,n,bl,arityc,body) r measure notation = Coqlib.check_required_library ["Coq";"Program";"Wf"]; let sigma = Evd.empty in let isevars = ref (Evd.create_evar_defs sigma) in let env = Global.env() in let _pr c = my_print_constr env c in let _prr = Printer.pr_rel_context env in let _prn = Printer.pr_named_context env in let _pr_rel env = Printer.pr_rel_context env in let (env', binders_rel), impls = interp_context_evars isevars env bl in let len = List.length binders_rel in let top_env = push_rel_context binders_rel env in let top_arity = interp_type_evars isevars top_env arityc in let full_arity = it_mkProd_or_LetIn top_arity binders_rel in let argtyp, letbinders, make = telescope binders_rel in let argname = id_of_string "recarg" in let arg = (Name argname, None, argtyp) in let binders = letbinders @ [arg] in let binders_env = push_rel_context binders_rel env in let rel = interp_constr isevars env r in let relty = type_of env !isevars rel in let relargty = let error () = user_err_loc (constr_loc r, "Subtac_command.build_wellfounded", my_print_constr env rel ++ str " is not an homogeneous binary relation.") in try let ctx, ar = Reductionops.splay_prod_n env !isevars 2 relty in match ctx, kind_of_term ar with | [(_, None, t); (_, None, u)], Sort (Prop Null) when Reductionops.is_conv env !isevars t u -> t | _, _ -> error () with _ -> error () in let measure = interp_casted_constr isevars binders_env measure relargty in let wf_rel, wf_rel_fun, measure_fn = let measure_body, measure = it_mkLambda_or_LetIn measure letbinders, it_mkLambda_or_LetIn measure binders in let comb = constr_of_global (delayed_force measure_on_R_ref) in let wf_rel = mkApp (comb, [| argtyp; relargty; rel; measure |]) in let wf_rel_fun x y = mkApp (rel, [| subst1 x measure_body; subst1 y measure_body |]) in wf_rel, wf_rel_fun, measure in let wf_proof = mkApp (delayed_force well_founded, [| argtyp ; wf_rel |]) in let argid' = id_of_string (string_of_id argname ^ "'") in let wfarg len = (Name argid', None, mkSubset (Name argid') argtyp (wf_rel_fun (mkRel 1) (mkRel (len + 1)))) in let intern_bl = wfarg 1 :: [arg] in let _intern_env = push_rel_context intern_bl env in let proj = (delayed_force sig_).Coqlib.proj1 in let wfargpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel 3)) in let projection = (* in wfarg :: arg :: before *) mkApp (proj, [| argtyp ; wfargpred ; mkRel 1 |]) in let top_arity_let = it_mkLambda_or_LetIn top_arity letbinders in let intern_arity = substl [projection] top_arity_let in (* substitute the projection of wfarg for something, now intern_arity is in wfarg :: arg *) let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfarg 1] in let intern_fun_binder = (Name (add_suffix recname "'"), None, intern_fun_arity_prod) in let curry_fun = let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in let arg = mkApp ((delayed_force sig_).intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in let app = mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in let rcurry = mkApp (rel, [| measure; lift len measure |]) in let lam = (Name (id_of_string "recproof"), None, rcurry) in let body = it_mkLambda_or_LetIn app (lam :: binders_rel) in let ty = it_mkProd_or_LetIn (lift 1 top_arity) (lam :: binders_rel) in (Name recname, Some body, ty) in let fun_bl = intern_fun_binder :: [arg] in let lift_lets = Termops.lift_rel_context 1 letbinders in let intern_body = let ctx = (Name recname, None, pi3 curry_fun) :: binders_rel in let (r, l, impls, scopes) = Constrintern.compute_internalization_data env Constrintern.Recursive full_arity impls in let newimpls = Idmap.singleton recname (r, l, impls @ [(Some (id_of_string "recproof", Impargs.Manual, (true, false)))], scopes @ [None]) in interp_casted_constr isevars ~impls:newimpls (push_rel_context ctx env) body (lift 1 top_arity) in let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in let prop = mkLambda (Name argname, argtyp, top_arity_let) in let def = mkApp (constr_of_global (delayed_force fix_sub_ref), [| argtyp ; wf_rel ; make_existential dummy_loc ~opaque:(Define false) env isevars wf_proof ; prop ; intern_body_lam |]) in let _ = isevars := Evarutil.nf_evar_map !isevars in let binders_rel = nf_evar_context !isevars binders_rel in let binders = nf_evar_context !isevars binders in let top_arity = Evarutil.nf_evar !isevars top_arity in let hook, recname, typ = if List.length binders_rel > 1 then let name = add_suffix recname "_func" in let hook l gr = let body = it_mkLambda_or_LetIn (mkApp (constr_of_global gr, [|make|])) binders_rel in let ty = it_mkProd_or_LetIn top_arity binders_rel in let ce = { const_entry_body = Evarutil.nf_evar !isevars body; const_entry_secctx = None; const_entry_type = Some ty; const_entry_opaque = false } in let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in let gr = ConstRef c in if Impargs.is_implicit_args () || impls <> [] then Impargs.declare_manual_implicits false gr [impls] in let typ = it_mkProd_or_LetIn top_arity binders in hook, name, typ else let typ = it_mkProd_or_LetIn top_arity binders_rel in let hook l gr = if Impargs.is_implicit_args () || impls <> [] then Impargs.declare_manual_implicits false gr [impls] in hook, recname, typ in let fullcoqc = Evarutil.nf_evar !isevars def in let fullctyp = Evarutil.nf_evar !isevars typ in let evm = evars_of_term !isevars Evd.empty fullctyp in let evm = evars_of_term !isevars evm fullcoqc in let evm = non_instanciated_map env isevars evm in let evars, _, evars_def, evars_typ = Eterm.eterm_obligations env recname !isevars evm 0 fullcoqc fullctyp in Subtac_obligations.add_definition recname ~term:evars_def evars_typ evars ~hook let interp_fix_context evdref env fix = interp_context_evars evdref env fix.Command.fix_binders let interp_fix_ccl evdref (env,_) fix = interp_type_evars evdref env fix.Command.fix_type let interp_fix_body evdref env_rec impls (_,ctx) fix ccl = let env = push_rel_context ctx env_rec in let body = Option.map (fun c -> interp_casted_constr_evars evdref env ~impls c ccl) fix.Command.fix_body in Option.map (fun c -> it_mkLambda_or_LetIn c ctx) body let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx let prepare_recursive_declaration fixnames fixtypes fixdefs = let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in let names = List.map (fun id -> Name id) fixnames in (Array.of_list names, Array.of_list fixtypes, Array.of_list defs) let rel_index n ctx = list_index0 (Name n) (List.rev_map pi1 (List.filter (fun x -> pi2 x = None) ctx)) let rec unfold f b = match f b with | Some (x, b') -> x :: unfold f b' | None -> [] let compute_possible_guardness_evidences (n,_) (_, fixctx) fixtype = match n with | Some (loc, n) -> [rel_index n fixctx] | None -> (* If recursive argument was not given by user, we try all args. An earlier approach was to look only for inductive arguments, but doing it properly involves delta-reduction, and it finally doesn't seem to worth the effort (except for huge mutual fixpoints ?) *) let len = List.length fixctx in unfold (function x when x = len -> None | n -> Some (n, succ n)) 0 let push_named_context = List.fold_right push_named let check_evars env initial_sigma evd c = let sigma = evd in let c = nf_evar sigma c in let rec proc_rec c = match kind_of_term c with | Evar (evk,args) -> assert (Evd.mem sigma evk); if not (Evd.mem initial_sigma evk) then let (loc,k) = evar_source evk evd in (match k with | QuestionMark _ | ImplicitArg (_, _, false) -> () | _ -> let evi = nf_evar_info sigma (Evd.find sigma evk) in Pretype_errors.error_unsolvable_implicit loc env sigma evi k None) | _ -> iter_constr proc_rec c in proc_rec c let out_def = function | Some def -> def | None -> error "Program Fixpoint needs defined bodies." let interp_recursive fixkind l = let env = Global.env() in let fixl, ntnl = List.split l in let kind = fixkind <> IsCoFixpoint in let fixnames = List.map (fun fix -> fix.Command.fix_name) fixl in (* Interp arities allowing for unresolved types *) let evdref = ref Evd.empty in let fixctxs, fiximps = List.split (List.map (interp_fix_context evdref env) fixl) in let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in let fixtypes = List.map2 build_fix_type fixctxs fixccls in let rec_sign = List.fold_left2 (fun env' id t -> let sort = Retyping.get_type_of env !evdref t in let fixprot = try mkApp (delayed_force Subtac_utils.fix_proto, [|sort; t|]) with e -> t in (id,None,fixprot) :: env') [] fixnames fixtypes in let env_rec = push_named_context rec_sign env in (* Get interpretation metadatas *) let impls = Constrintern.compute_internalization_env env Constrintern.Recursive fixnames fixtypes fiximps in let notations = List.flatten ntnl in (* Interp bodies with rollback because temp use of notations/implicit *) let fixdefs = States.with_state_protection (fun () -> List.iter (Metasyntax.set_notation_for_interpretation impls) notations; list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls) () in let fixdefs = List.map out_def fixdefs in (* Instantiate evars and check all are resolved *) let evd = Evarconv.consider_remaining_unif_problems env_rec !evdref in let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:true ~fail:false env_rec evd in let evd = Evarutil.nf_evar_map evd in let fixdefs = List.map (nf_evar evd) fixdefs in let fixtypes = List.map (nf_evar evd) fixtypes in let rec_sign = nf_named_context_evar evd rec_sign in let recdefs = List.length rec_sign in List.iter (check_evars env_rec Evd.empty evd) fixdefs; List.iter (check_evars env Evd.empty evd) fixtypes; Command.check_mutuality env kind (List.combine fixnames fixdefs); (* Russell-specific code *) (* Get the interesting evars, those that were not instanciated *) let isevars = Evd.undefined_evars evd in let evm = isevars in (* Solve remaining evars *) let rec collect_evars id def typ imps = (* Generalize by the recursive prototypes *) let def = Termops.it_mkNamedLambda_or_LetIn def rec_sign and typ = Termops.it_mkNamedProd_or_LetIn typ rec_sign in let evm' = Subtac_utils.evars_of_term evm Evd.empty def in let evm' = Subtac_utils.evars_of_term evm evm' typ in let evars, _, def, typ = Eterm.eterm_obligations env id isevars evm' recdefs def typ in (id, def, typ, imps, evars) in let defs = list_map4 collect_evars fixnames fixdefs fixtypes fiximps in (match fixkind with | IsFixpoint wfl -> let possible_indexes = list_map3 compute_possible_guardness_evidences wfl fixctxs fixtypes in let fixdecls = Array.of_list (List.map (fun x -> Name x) fixnames), Array.of_list fixtypes, Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs) in let indexes = Pretyping.search_guard dummy_loc (Global.env ()) possible_indexes fixdecls in list_iter_i (fun i _ -> Inductive.check_fix env ((indexes,i),fixdecls)) l | IsCoFixpoint -> ()); Subtac_obligations.add_mutual_definitions defs notations fixkind let out_n = function Some n -> n | None -> raise Not_found let build_recursive l = let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in match g, l with [(n, CWfRec r)], [(((_,id),_,bl,typ,def),ntn)] -> ignore(build_wellfounded (id, n, bl, typ, out_def def) r (match n with Some n -> mkIdentC (snd n) | None -> errorlabstrm "Subtac_command.build_recursive" (str "Recursive argument required for well-founded fixpoints")) ntn) | [(n, CMeasureRec (m, r))], [(((_,id),_,bl,typ,def),ntn)] -> ignore(build_wellfounded (id, n, bl, typ, out_def def) (Option.default (CRef lt_ref) r) m ntn) | _, _ when List.for_all (fun (n, ro) -> ro = CStructRec) g -> let fixl = List.map (fun (((_,id),(n,ro),bl,typ,def),ntn) -> ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_annot = n; Command.fix_body = def; Command.fix_type = typ},ntn)) l in interp_recursive (IsFixpoint g) fixl | _, _ -> errorlabstrm "Subtac_command.build_recursive" (str "Well-founded fixpoints not allowed in mutually recursive blocks") let build_corecursive l = let fixl = List.map (fun (((_,id),bl,typ,def),ntn) -> ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_annot = None; Command.fix_body = def; Command.fix_type = typ},ntn)) l in interp_recursive IsCoFixpoint fixl