open Closure open RedFlags open Declarations open Entries open Dyn open Libobject open Pattern open Matching open Pp open Rawterm 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 Termops 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 module SPretyping = Subtac_pretyping.Pretyping open Subtac_utils open Pretyping (*********************************************************************) (* Functions to parse and interpret constructions *) let evar_nf isevars c = isevars := Evarutil.nf_evar_defs !isevars; Evarutil.nf_isevar !isevars c let interp_gen kind isevars env ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[])) c = let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars (Evd.evars_of !isevars) env c in let c' = Subtac_utils.rewrite_cases env c' in (try trace (str "Pretyping " ++ my_print_constr_expr c) with _ -> ()); let c' = SPretyping.pretype_gen 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 isevars env ?(impls=([],[])) c = interp_gen IsType isevars env ~impls c let interp_casted_constr isevars env ?(impls=([],[])) 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 (Evd.evars_of !isevars) env c in let c' = SPretyping.pretype_gen 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 (Evd.evars_of !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 | RHole _ -> (try match na with | Name id -> Reserve.find_reserved_type id | Anonymous -> raise Not_found with Not_found -> RHole (loc, Evd.BinderType na)) | x -> x let interp_binder sigma env na t = let t = Constrintern.intern_gen true (Evd.evars_of !sigma) env t in SPretyping.understand_type (Evd.evars_of !sigma) env (locate_if_isevar (loc_of_rawconstr t) na t) let interp_context sigma env params = List.fold_left (fun (env,params) d -> match d with | LocalRawAssum ([_,na],(CHole _ as t)) -> let t = interp_binder sigma env na t in let d = (na,None,t) in (push_rel d env, d::params) | LocalRawAssum (nal,t) -> let t = interp_type sigma env t in let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in let ctx = List.rev ctx in (push_rel_context ctx env, ctx@params) | LocalRawDef ((_,na),c) -> let c = interp_constr_judgment sigma env c in let d = (na, Some c.uj_val, c.uj_type) in (push_rel d env,d::params)) (env,[]) params (* try to find non recursive definitions *) let list_chop_hd i l = match list_chop i l with | (l1,x::l2) -> (l1,x,l2) | _ -> 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 (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 definition_message id = Options.if_verbose message ((string_of_id id) ^ " is defined") let recursive_message v = match Array.length v with | 0 -> error "no recursive definition" | 1 -> (Printer.pr_global v.(0) ++ str " is recursively defined") | _ -> hov 0 (prvect_with_sep pr_coma Printer.pr_global v ++ spc () ++ str "are recursively defined") let filter_map f l = let rec aux acc = function hd :: tl -> (match f hd with Some t -> aux (t :: acc) tl | None -> aux acc tl) | [] -> List.rev acc in aux [] l 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, c) :: tl -> aux (List.fold_left (fun acc n -> (n, None, Some c) :: acc) acc nl) tl | [] -> List.rev acc in aux [] l let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed = let sigma = Evd.empty and env0 = Global.env() in let lnameargsardef = (*List.map (fun (f, d) -> Subtac_interp_fixpoint.rewrite_fixpoint env0 protos (f, d))*) lnameargsardef in let lrecnames = List.map (fun ((f,_,_,_,_),_) -> f) lnameargsardef and nv = List.map (fun ((_,n,_,_,_),_) -> n) lnameargsardef in (* Build the recursive context and notations for the recursive types *) let (rec_sign,rec_impls,arityl) = List.fold_left (fun (env,impls,arl) ((recname,(n, ro),bl,arityc,body),_) -> let isevars = ref (Evd.create_evar_defs sigma) in match ro with CStructRec -> let arityc = Command.generalize_constr_expr arityc bl in let arity = interp_type isevars env0 arityc in let impl = if Impargs.is_implicit_args() then Impargs.compute_implicits env0 arity else [] in let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in (Environ.push_named (recname,None,arity) env, impls', (isevars, None, arity)::arl) | CWfRec r -> let n = out_some n in let _ = try trace (str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++ Ppconstr.pr_binders bl ++ str " : " ++ Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++ Ppconstr.pr_constr_expr body) with _ -> () in let env', binders_rel = interp_context isevars env0 bl in let after, ((argname, _, argtyp) as arg), before = list_chop_hd n binders_rel in let argid = match argname with Name n -> n | _ -> assert(false) in let after' = List.map (fun (n, c, t) -> (n, option_map (lift 1) c, lift 1 t)) after in let envwf = push_rel_context before env0 in let wf_rel = interp_constr isevars envwf r in let accarg_id = id_of_string ("Acc_" ^ string_of_id argid) in let accarg = (Name accarg_id, None, mkApp (Lazy.force acc_inv, [| argtyp; wf_rel; mkRel 1 |])) in let argid' = id_of_string (string_of_id argid ^ "'") in let before_length, after_length = List.length before, List.length after in let full_length = before_length + 1 + after_length in let wfarg len = (Name argid, None, mkSubset (Name argid') argtyp (mkApp (wf_rel, [|mkRel 1; mkRel (len + 1)|]))) in let new_bl = after' @ (accarg :: arg :: before) and intern_bl = after @ (wfarg (before_length + 1) :: before) in let intern_env = push_rel_context intern_bl env0 in let env' = push_rel_context new_bl env0 in let arity = interp_type isevars intern_env arityc in let intern_arity = it_mkProd_or_LetIn arity intern_bl in let arity' = interp_type isevars env' arityc in let arity' = it_mkProd_or_LetIn arity' new_bl in let fun_bl = after @ ((Name recname, None, intern_arity) :: arg :: before) in let _ = let pr c = my_print_constr env c in let prr = Printer.pr_rel_context env in try trace (str "Fun bl: " ++ prr fun_bl ++ spc () ++ str "Intern bl" ++ prr intern_bl ++ spc () ++ str "Extern bl" ++ prr new_bl ++ spc () ++ str "Intern arity: " ++ pr intern_arity) with _ -> () in let impl = if Impargs.is_implicit_args() then Impargs.compute_implicits intern_env arity' else [] in let impls' = (recname,([],impl,compute_arguments_scope arity'))::impls in (Environ.push_named (recname,None,arity') env, impls', (isevars, Some (full_length - n, argtyp, wf_rel, fun_bl, intern_bl, intern_arity), arity')::arl)) (env0,[],[]) lnameargsardef in let arityl = List.rev arityl in let notations = List.fold_right (fun (_,ntnopt) l -> option_cons ntnopt l) lnameargsardef [] in let recdef = (* Declare local notations *) let fs = States.freeze() in let def = try List.iter (fun (df,c,scope) -> (* No scope for tmp notation *) Metasyntax.add_notation_interpretation df rec_impls c None) notations; List.map2 (fun ((_,_,bl,_,def),_) (isevars, info, arity) -> match info with None -> let def = abstract_constr_expr def bl in isevars, info, interp_casted_constr isevars rec_sign ~impls:([],rec_impls) def arity | Some (n, artyp, wfrel, fun_bl, intern_bl, intern_arity) -> let rec_sign = push_rel_context fun_bl rec_sign in let cstr = interp_casted_constr isevars rec_sign ~impls:([],rec_impls) def intern_arity in isevars, info, it_mkLambda_or_LetIn cstr fun_bl) lnameargsardef arityl with e -> States.unfreeze fs; raise e in States.unfreeze fs; def in let (lnonrec,(namerec,defrec,arrec,nvrec)) = collect_non_rec env0 lrecnames recdef arityl nv in let nvrec' = Array.map (function (Some n,_) -> n | _ -> 0) nvrec in(* ignore rec order *) let declare arrec defrec = let recvec = Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in let rec declare i fi = (try trace (str "Declaring: " ++ pr_id fi ++ spc () ++ my_print_constr env0 (recvec.(i))); with _ -> ()); let ce = { const_entry_body = mkFix ((nvrec',i),recdecls); const_entry_type = Some arrec.(i); const_entry_opaque = false; const_entry_boxed = boxed} in let kn = Declare.declare_constant fi (DefinitionEntry ce,IsDefinition Fixpoint) in (ConstRef kn) in (* declare the recursive definitions *) let lrefrec = Array.mapi declare namerec in Options.if_verbose ppnl (recursive_message lrefrec); (*(* The others are declared as normal definitions *) let var_subst id = (id, Constrintern.global_reference id) in let _ = List.fold_left (fun subst (f,def,t) -> let ce = { const_entry_body = replace_vars subst def; const_entry_type = Some t; const_entry_opaque = false; const_entry_boxed = boxed } in let _ = Declare.declare_constant f (DefinitionEntry ce,IsDefinition Definition) in warning ((string_of_id f)^" is non-recursively defined"); (var_subst f) :: subst) (List.map var_subst (Array.to_list namerec)) lnonrec in*) List.iter (fun (df,c,scope) -> Metasyntax.add_notation_interpretation df [] c scope) notations in let declare l = let recvec = Array.of_list l and arrec = Array.map pi3 arrec in declare arrec recvec in let recdefs = Array.length defrec in trace (int recdefs ++ str " recursive definitions"); (* Solve remaining evars *) let rec collect_evars i acc = if i < recdefs then let (isevars, info, def) = defrec.(i) in let _ = try trace (str "In solve evars, isevars is: " ++ Evd.pr_evar_defs !isevars) with _ -> () in let def = evar_nf isevars def in let isevars = Evd.undefined_evars !isevars in let _ = try trace (str "In solve evars, undefined is: " ++ Evd.pr_evar_defs isevars) with _ -> () in let evm = Evd.evars_of isevars in let _, _, typ = arrec.(i) in let id = namerec.(i) in (* Generalize by the recursive prototypes *) let def = Termops.it_mkNamedLambda_or_LetIn def (Environ.named_context rec_sign) and typ = Termops.it_mkNamedProd_or_LetIn typ (Environ.named_context rec_sign) in let evars_def, evars_typ, evars = Eterm.eterm_term evm def (Some typ) in (*let evars_typ = match evars_typ with Some t -> t | None -> assert(false) in*) (*let fi = id_of_string (string_of_id id ^ "_evars") in*) (*let ce = { const_entry_body = evars_def; const_entry_type = Some evars_typ; const_entry_opaque = false; const_entry_boxed = boxed} in let kn = Declare.declare_constant fi (DefinitionEntry ce,IsDefinition Definition) in definition_message fi; trace (str (string_of_id fi) ++ str " is defined");*) let evar_sum = if evars = [] then None else ( (try trace (str "Building evars sum for : "); List.iter (fun (n, t) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env0 t)) evars; with _ -> ()); let sum = Subtac_utils.build_dependent_sum evars in (try trace (str "Evars sum: " ++ my_print_constr env0 (snd sum)); with _ -> ()); Some sum) in collect_evars (succ i) ((id, evars_def, evar_sum) :: acc) else acc in let defs = collect_evars 0 [] in (* Solve evars then create the definitions *) let real_evars = filter_map (fun (id, kn, sum) -> match sum with Some (sumtac, sumg) -> Some (id, kn, sumg, sumtac) | None -> None) defs in Subtac_utils.and_tac real_evars (fun f _ gr -> let _ = trace (str "Got a proof of: " ++ pr_global gr ++ str "type: " ++ my_print_constr (Global.env ()) (Global.type_of_global gr)) in let constant = match gr with Libnames.ConstRef c -> c | _ -> assert(false) in try (*let value = Environ.constant_value (Global.env ()) constant in*) let pis = f (mkConst constant) in (try (trace (str "Accessors: " ++ List.fold_right (fun (_, _, _, c) acc -> my_print_constr env0 c ++ spc () ++ acc) pis (mt())); trace (str "Applied existentials: " ++ (List.fold_right (fun (id, kn, sumg, pi) acc -> let args = Subtac_utils.destruct_ex pi sumg in my_print_constr env0 (mkApp (kn, Array.of_list args))) pis (mt ())))) with _ -> ()); let rec aux pis acc = function (id, kn, sum) :: tl -> (match sum with None -> aux pis (kn :: acc) tl | Some (_, sumg) -> let (id, kn, sumg, pi), pis = List.hd pis, List.tl pis in let args = Subtac_utils.destruct_ex pi sumg in let args = List.map (fun c -> try Reductionops.whd_betadeltaiota (Global.env ()) Evd.empty c with Not_found -> trace (str "Not_found while reducing " ++ my_print_constr (Global.env ()) c); c ) args in let _, newdef = decompose_lam_n (recdefs + List.length args) kn in let constr = Term.substl (mkRel 1 :: List.rev args) newdef in aux pis (constr :: acc) tl) | [] -> List.rev acc in declare (aux pis [] defs) with Environ.NotEvaluableConst cer -> match cer with Environ.NoBody -> trace (str "Constant has no body") | Environ.Opaque -> trace (str "Constant is opaque") )