diff options
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 1167 |
1 files changed, 263 insertions, 904 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 05a22829..700efc99 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -6,63 +6,32 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: command.ml 12187 2009-06-13 19:36:59Z msozeau $ *) +(* $Id$ *) open Pp open Util open Flags open Term open Termops -open Declarations open Entries -open Inductive open Environ -open Reduction open Redexpr open Declare -open Nametab open Names open Libnames open Nameops open Topconstr -open Library -open Libobject open Constrintern -open Proof_type -open Tacmach -open Safe_typing open Nametab open Impargs -open Typeops open Reductionops open Indtypes -open Vernacexpr open Decl_kinds open Pretyping open Evarutil open Evarconv open Notation -open Goptions -open Mod_subst -open Evd -open Decls - -let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,default_binder_kind,a,b)) -let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,default_binder_kind,a,b)) - -let rec abstract_constr_expr c = function - | [] -> c - | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl) - | LocalRawAssum (idl,k,t)::bl -> - List.fold_right (fun x b -> mkLambdaC([x],k,t,b)) idl - (abstract_constr_expr c bl) - -let rec generalize_constr_expr c = function - | [] -> c - | LocalRawDef (x,b)::bl -> mkLetInC(x,b,generalize_constr_expr c bl) - | LocalRawAssum (idl,k,t)::bl -> - List.fold_right (fun x b -> mkProdC([x],k,t,b)) idl - (generalize_constr_expr c bl) +open Indschemes let rec under_binders env f n c = if n = 0 then f env Evd.empty c else @@ -73,14 +42,6 @@ let rec under_binders env f n c = mkLetIn (x,b,t,under_binders (push_rel (x,Some b,t) env) f (n-1) c) | _ -> assert false -let rec destSubCast c = match kind_of_term c with - | Lambda (x,t,c) -> - let (b,u) = destSubCast c in mkLambda (x,t,b), mkProd (x,t,u) - | LetIn (x,b,t,c) -> - let (d,u) = destSubCast c in mkLetIn (x,b,t,d), mkLetIn (x,b,t,u) - | Cast (b,_, u) -> (b,u) - | _ -> assert false - let rec complete_conclusion a cs = function | CProdN (loc,bl,c) -> CProdN (loc,bl,complete_conclusion a cs c) | CLetIn (loc,b,t,c) -> CLetIn (loc,b,t,complete_conclusion a cs c) @@ -98,92 +59,86 @@ let rec complete_conclusion a cs = function (* 1| Constant definitions *) -let definition_message id = - if_verbose message ((string_of_id id) ^ " is defined") +let red_constant_entry n ce = function + | None -> ce + | Some red -> + let body = ce.const_entry_body in + { ce with const_entry_body = + under_binders (Global.env()) (fst (reduction_of_red_expr red)) n body } -let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) = +let interp_definition boxed bl red_option c ctypopt = let env = Global.env() in - match comtypopt with - None -> - let b = abstract_constr_expr com bl in - let b, imps = interp_constr_evars_impls env b in - imps, - { const_entry_body = b; + let evdref = ref Evd.empty in + let (env_bl, ctx), imps1 = + interp_context_evars ~fail_anonymous:false evdref env bl in + let imps,ce = + match ctypopt with + None -> + let c, imps2 = interp_constr_evars_impls ~evdref ~fail_evar:false env_bl c in + let body = nf_evar !evdref (it_mkLambda_or_LetIn c ctx) in + check_evars env Evd.empty !evdref body; + imps1@imps2, + { const_entry_body = body; const_entry_type = None; - const_entry_opaque = opacity; + const_entry_opaque = false; const_entry_boxed = boxed } - | Some comtyp -> - (* We use a cast to avoid troubles with evars in comtyp *) - (* that can only be resolved knowing com *) - let b = abstract_constr_expr (mkCastC (com, Rawterm.CastConv (DEFAULTcast,comtyp))) bl in - let b, imps = interp_constr_evars_impls env b in - let (body,typ) = destSubCast b in - imps, + | Some ctyp -> + let ty, impls = interp_type_evars_impls ~evdref ~fail_evar:false env_bl ctyp in + let c, imps2 = interp_casted_constr_evars_impls ~evdref ~fail_evar:false env_bl c ty in + let body = nf_evar !evdref (it_mkLambda_or_LetIn c ctx) in + let typ = nf_evar !evdref (it_mkProd_or_LetIn ty ctx) in + check_evars env Evd.empty !evdref body; + check_evars env Evd.empty !evdref typ; + imps1@imps2, { const_entry_body = body; const_entry_type = Some typ; - const_entry_opaque = opacity; + const_entry_opaque = false; const_entry_boxed = boxed } + in + red_constant_entry (rel_context_length ctx) ce red_option, imps -let red_constant_entry bl ce = function - | None -> ce - | Some red -> - let body = ce.const_entry_body in - { ce with const_entry_body = - under_binders (Global.env()) (fst (reduction_of_red_expr red)) - (local_binders_length bl) - body } - -let declare_global_definition ident ce local imps = - let kn = declare_constant ident (DefinitionEntry ce,IsDefinition Definition) in +let declare_global_definition ident ce local k imps = + let kn = declare_constant ident (DefinitionEntry ce,IsDefinition k) in let gr = ConstRef kn in maybe_declare_manual_implicits false gr imps; if local = Local && Flags.is_verbose() then msg_warning (pr_id ident ++ str" is declared as a global definition"); definition_message ident; + Autoinstance.search_declaration (ConstRef kn); gr let declare_definition_hook = ref ignore let set_declare_definition_hook = (:=) declare_definition_hook let get_declare_definition_hook () = !declare_definition_hook -let declare_definition ident (local,boxed,dok) bl red_option c typopt hook = - let imps, ce = constant_entry_of_com (bl,c,typopt,false,boxed) in - let ce' = red_constant_entry bl ce red_option in - !declare_definition_hook ce'; +let declare_definition ident (local,k) ce imps hook = + !declare_definition_hook ce; let r = match local with | Local when Lib.sections_are_opened () -> let c = - SectionLocalDef(ce'.const_entry_body,ce'.const_entry_type,false) in - let _ = declare_variable ident (Lib.cwd(),c,IsDefinition Definition) in + SectionLocalDef(ce.const_entry_body,ce.const_entry_type,false) in + let _ = declare_variable ident (Lib.cwd(),c,IsDefinition k) in definition_message ident; - if Pfedit.refining () then - Flags.if_verbose msg_warning - (str"Local definition " ++ pr_id ident ++ + if Pfedit.refining () then + Flags.if_verbose msg_warning + (str"Local definition " ++ pr_id ident ++ str" is not visible from current goals"); VarRef ident | (Global|Local) -> - declare_global_definition ident ce' local imps in + declare_global_definition ident ce local k imps in hook local r -let syntax_definition ident (vars,c) local onlyparse = - let ((vars,_),pat) = interp_aconstr [] (vars,[]) c in - let onlyparse = onlyparse or Metasyntax.is_not_printable pat in - Syntax_def.declare_syntactic_definition local ident onlyparse (vars,pat) - (* 2| Variable/Hypothesis/Parameter/Axiom declarations *) -let assumption_message id = - if_verbose message ((string_of_id id) ^ " is assumed") - -let declare_one_assumption is_coe (local,kind) c imps impl keep nl (_,ident) = +let declare_assumption is_coe (local,kind) c imps impl nl (_,ident) = let r = match local with | Local when Lib.sections_are_opened () -> - let _ = - declare_variable ident - (Lib.cwd(), SectionLocalAssum (c,impl,keep), IsAssumption kind) in + let _ = + declare_variable ident + (Lib.cwd(), SectionLocalAssum (c,impl), IsAssumption kind) in assumption_message ident; - if is_verbose () & Pfedit.refining () then - msgerrnl (str"Warning: Variable " ++ pr_id ident ++ + if is_verbose () & Pfedit.refining () then + msgerrnl (str"Warning: Variable " ++ pr_id ident ++ str" is not visible from current goals"); VarRef ident | (Global|Local) -> @@ -195,283 +150,26 @@ let declare_one_assumption is_coe (local,kind) c imps impl keep nl (_,ident) = if local=Local & Flags.is_verbose () then msg_warning (pr_id ident ++ str" is declared as a parameter" ++ str" because it is at a global level"); + Autoinstance.search_declaration (ConstRef kn); gr in if is_coe then Class.try_add_new_coercion r local -let declare_assumption_hook = ref ignore -let set_declare_assumption_hook = (:=) declare_assumption_hook - -let declare_assumption idl is_coe k bl c impl keep nl = - if not (Pfedit.refining ()) then - let c = generalize_constr_expr c bl in - let env = Global.env () in - let c', imps = interp_type_evars_impls env c in - !declare_assumption_hook c'; - List.iter (declare_one_assumption is_coe k c' imps impl keep nl) idl - else - errorlabstrm "Command.Assumption" - (str "Cannot declare an assumption while in proof editing mode.") - -(* 3a| Elimination schemes for mutual inductive definitions *) - -open Indrec -open Inductiveops +let declare_assumptions_hook = ref ignore +let set_declare_assumptions_hook = (:=) declare_assumptions_hook +let interp_assumption bl c = + let c = prod_constr_expr c bl in + let env = Global.env () in + interp_type_evars_impls env c -let non_type_eliminations = - [ (InProp,elimination_suffix InProp); - (InSet,elimination_suffix InSet) ] +let declare_assumptions idl is_coe k c imps impl_is_on nl = + !declare_assumptions_hook c; + List.iter (declare_assumption is_coe k c imps impl_is_on nl) idl -let declare_one_elimination ind = - let (mib,mip) = Global.lookup_inductive ind in - let mindstr = string_of_id mip.mind_typename in - let declare s c t = - let id = id_of_string s in - let kn = Declare.declare_internal_constant id - (DefinitionEntry - { const_entry_body = c; - const_entry_type = t; - const_entry_opaque = false; - const_entry_boxed = Flags.boxed_definitions() }, - Decl_kinds.IsDefinition Definition) in - definition_message id; - kn - in - let env = Global.env () in - let sigma = Evd.empty in - let elim_scheme = Indrec.build_indrec env sigma ind in - let npars = - (* if a constructor of [ind] contains a recursive call, the scheme - is generalized only wrt recursively uniform parameters *) - if (Inductiveops.mis_is_recursive_subset [snd ind] mip.mind_recargs) - then - mib.mind_nparams_rec - else - mib.mind_nparams in - let make_elim s = Indrec.instantiate_indrec_scheme s npars elim_scheme in - let kelim = elim_sorts (mib,mip) in - (* in case the inductive has a type elimination, generates only one - induction scheme, the other ones share the same code with the - apropriate type *) - if List.mem InType kelim then - let elim = make_elim (new_sort_in_family InType) in - let cte = declare (mindstr^(Indrec.elimination_suffix InType)) elim None in - let c = mkConst cte in - let t = type_of_constant (Global.env()) cte in - List.iter (fun (sort,suff) -> - let (t',c') = - Indrec.instantiate_type_indrec_scheme (new_sort_in_family sort) - npars c t in - let _ = declare (mindstr^suff) c' (Some t') in ()) - non_type_eliminations - else (* Impredicative or logical inductive definition *) - List.iter - (fun (sort,suff) -> - if List.mem sort kelim then - let elim = make_elim (new_sort_in_family sort) in - let _ = declare (mindstr^suff) elim None in ()) - non_type_eliminations - -(* bool eq declaration flag && eq dec declaration flag *) -let eq_flag = ref false -let _ = - declare_bool_option - { optsync = true; - optname = "automatic declaration of boolean equality"; - optkey = (SecondaryTable ("Equality","Scheme")); - optread = (fun () -> !eq_flag) ; - optwrite = (fun b -> eq_flag := b) } - -(* boolean equality *) -let (inScheme,outScheme) = - declare_object {(default_object "EQSCHEME") with - cache_function = Ind_tables.cache_scheme; - load_function = (fun _ -> Ind_tables.cache_scheme); - subst_function = Auto_ind_decl.subst_in_constr; - export_function = Ind_tables.export_scheme } - -let declare_eq_scheme sp = - let mib = Global.lookup_mind sp in - let nb_ind = Array.length mib.mind_packets in - let eq_array = Auto_ind_decl.make_eq_scheme sp in - try - for i=0 to (nb_ind-1) do - let cpack = Array.get mib.mind_packets i in - let nam = id_of_string ((string_of_id cpack.mind_typename)^"_beq") - in - let cst_entry = {const_entry_body = eq_array.(i); - const_entry_type = None; - const_entry_opaque = false; - const_entry_boxed = Flags.boxed_definitions() } - in - let cst_decl = (DefinitionEntry cst_entry),(IsDefinition Definition) - in - let cst = Declare.declare_constant nam cst_decl in - Lib.add_anonymous_leaf (inScheme ((sp,i),mkConst cst)); - definition_message nam - done - with Not_found -> - error "Your type contains Parameters without a boolean equality." - -(* decidability of eq *) - - -let (inBoolLeib,outBoolLeib) = - declare_object {(default_object "BOOLLIEB") with - cache_function = Ind_tables.cache_bl; - load_function = (fun _ -> Ind_tables.cache_bl); - subst_function = Auto_ind_decl.subst_in_constr; - export_function = Ind_tables.export_bool_leib } - -let (inLeibBool,outLeibBool) = - declare_object {(default_object "LIEBBOOL") with - cache_function = Ind_tables.cache_lb; - load_function = (fun _ -> Ind_tables.cache_lb); - subst_function = Auto_ind_decl.subst_in_constr; - export_function = Ind_tables.export_leib_bool } - -let (inDec,outDec) = - declare_object {(default_object "EQDEC") with - cache_function = Ind_tables.cache_dec; - load_function = (fun _ -> Ind_tables.cache_dec); - subst_function = Auto_ind_decl.subst_in_constr; - export_function = Ind_tables.export_dec_proof } - -let start_hook = ref ignore -let set_start_hook = (:=) start_hook - -let start_proof id kind c ?init_tac ?(compute_guard=false) hook = - let sign = Global.named_context () in - let sign = clear_proofs sign in - !start_hook c; - Pfedit.start_proof id kind sign c ?init_tac ~compute_guard hook - -let adjust_guardness_conditions const = - (* Try all combinations... not optimal *) - match kind_of_term const.const_entry_body with - | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> - let possible_indexes = - List.map (fun c -> - interval 0 (List.length (fst (Sign.decompose_lam_assum c)))) - (Array.to_list fixdefs) in - let indexes = search_guard dummy_loc (Global.env()) possible_indexes fixdecls in - { const with const_entry_body = mkFix ((indexes,0),fixdecls) } - | c -> const - -let save id const do_guard (locality,kind) hook = - let const = if do_guard then adjust_guardness_conditions const else const in - let {const_entry_body = pft; - const_entry_type = tpo; - const_entry_opaque = opacity } = const in - let k = logical_kind_of_goal_kind kind in - let l,r = match locality with - | Local when Lib.sections_are_opened () -> - let c = SectionLocalDef (pft, tpo, opacity) in - let _ = declare_variable id (Lib.cwd(), c, k) in - (Local, VarRef id) - | Local | Global -> - let kn = declare_constant id (DefinitionEntry const, k) in - (Global, ConstRef kn) in - Pfedit.delete_current_proof (); - definition_message id; - hook l r - -let save_hook = ref ignore -let set_save_hook f = save_hook := f - -let save_named opacity = - let id,(const,do_guard,persistence,hook) = Pfedit.cook_proof !save_hook in - let const = { const with const_entry_opaque = opacity } in - save id const do_guard persistence hook - -let make_eq_decidability ind = - (* fetching data *) - let mib = Global.lookup_mind (fst ind) in - let nparams = mib.mind_nparams in - let nparrec = mib.mind_nparams_rec in - let lnonparrec,lnamesparrec = - context_chop (nparams-nparrec) mib.mind_params_ctxt in - let proof_name = (string_of_id( - Array.get mib.mind_packets (snd ind)).mind_typename)^"_eq_dec" in - let bl_name =(string_of_id( - Array.get mib.mind_packets (snd ind)).mind_typename)^"_dec_bl" in - let lb_name =(string_of_id( - Array.get mib.mind_packets (snd ind)).mind_typename)^"_dec_lb" in - (* main calls*) - if Ind_tables.check_bl_proof ind - then (message (bl_name^" is already declared.")) - else ( - start_proof (id_of_string bl_name) - (Global,Proof Theorem) - (Auto_ind_decl.compute_bl_goal ind lnamesparrec nparrec) - (fun _ _ -> ()); - Auto_ind_decl.compute_bl_tact ind lnamesparrec nparrec; - save_named true; - Lib.add_anonymous_leaf - (inBoolLeib (ind,mkConst (Lib.make_con (id_of_string bl_name)))) -(* definition_message (id_of_string bl_name) *) - ); - if Ind_tables.check_lb_proof ind - then (message (lb_name^" is already declared.")) - else ( - start_proof (id_of_string lb_name) - (Global,Proof Theorem) - (Auto_ind_decl.compute_lb_goal ind lnamesparrec nparrec) - ( fun _ _ -> ()); - Auto_ind_decl.compute_lb_tact ind lnamesparrec nparrec; - save_named true; - Lib.add_anonymous_leaf - (inLeibBool (ind,mkConst (Lib.make_con (id_of_string lb_name)))) -(* definition_message (id_of_string lb_name) *) - ); - if Ind_tables.check_dec_proof ind - then (message (proof_name^" is already declared.")) - else ( - start_proof (id_of_string proof_name) - (Global,Proof Theorem) - (Auto_ind_decl.compute_dec_goal ind lnamesparrec nparrec) - ( fun _ _ -> ()); - Auto_ind_decl.compute_dec_tact ind lnamesparrec nparrec; - save_named true; - Lib.add_anonymous_leaf - (inDec (ind,mkConst (Lib.make_con (id_of_string proof_name)))) -(* definition_message (id_of_string proof_name) *) - ) - -(* end of automated definition on ind*) - -let declare_eliminations sp = - let mib = Global.lookup_mind sp in - if mib.mind_finite then begin - if (!eq_flag) then (declare_eq_scheme sp); - for i = 0 to Array.length mib.mind_packets - 1 do - declare_one_elimination (sp,i); - try - if (!eq_flag) then (make_eq_decidability (sp,i)) - with _ -> - Pfedit.delete_current_proof(); - message "Error while computing decidability scheme. Please report." - done; - end +(* 3a| Elimination schemes for mutual inductive definitions *) (* 3b| Mutual inductive definitions *) -let compute_interning_datas env ty l nal typl impll = - let mk_interning_data na typ impls = - let idl, impl = - let impl = - compute_implicits_with_manual env typ (is_implicit_args ()) impls - in - let sub_impl,_ = list_chop (List.length l) impl in - let sub_impl' = List.filter is_status_implicit sub_impl in - (List.map name_of_implicit sub_impl', impl) - in - (na, (ty, idl, impl, compute_arguments_scope typ)) in - (l, list_map3 mk_interning_data nal typl impll) - -let declare_interning_data (_,impls) (df,c,scope) = - silently (Metasyntax.add_notation_interpretation df impls c) scope - let push_named_types env idl tl = List.fold_left2 (fun env id t -> Environ.push_named (id,None,t) env) env idl tl @@ -480,16 +178,19 @@ let push_types env idl tl = List.fold_left2 (fun env id t -> Environ.push_rel (Name id,None,t) env) env idl tl -type inductive_expr = { +type structured_one_inductive_expr = { ind_name : identifier; ind_arity : constr_expr; ind_lc : (identifier * constr_expr) list } +type structured_inductive_expr = + local_binder list * structured_one_inductive_expr list + let minductive_message = function | [] -> error "No inductive definition." | [x] -> (pr_id x ++ str " is defined") - | l -> hov 0 (prlist_with_sep pr_coma pr_id l ++ + | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++ spc () ++ str "are defined") let check_all_names_different indl = @@ -503,15 +204,15 @@ let check_all_names_different indl = if l <> [] then raise (InductiveError (SameNamesOverlap l)) let mk_mltype_data evdref env assums arity indname = - let is_ml_type = is_sort env (evars_of !evdref) arity in + let is_ml_type = is_sort env !evdref arity in (is_ml_type,indname,assums) let prepare_param = function - | (na,None,t) -> out_name na, LocalAssum t + | (na,None,t) -> out_name na, LocalAssum t | (na,Some b,_) -> out_name na, LocalDef b let interp_ind_arity evdref env ind = - interp_type_evars evdref env ind.ind_arity + interp_type_evars_impls ~evdref env ind.ind_arity let interp_cstrs evdref env impls mldata arity ind = let cnames,ctyps = List.split ind.ind_lc in @@ -521,12 +222,12 @@ let interp_cstrs evdref env impls mldata arity ind = let ctyps'', cimpls = List.split (List.map (interp_type_evars_impls ~evdref env ~impls) ctyps') in (cnames, ctyps'', cimpls) -let interp_mutual paramsl indl notations finite = +let interp_mutual_inductive (paramsl,indl) notations finite = check_all_names_different indl; let env0 = Global.env() in - let evdref = ref (Evd.create_evar_defs Evd.empty) in - let (env_params, ctx_params), userimpls = - interp_context_evars ~fail_anonymous:false evdref env0 paramsl + let evdref = ref Evd.empty in + let (env_params, ctx_params), userimpls = + interp_context_evars ~fail_anonymous:false evdref env0 paramsl in let indnames = List.map (fun ind -> ind.ind_name) indl in @@ -536,19 +237,20 @@ let interp_mutual paramsl indl notations finite = (* Interpret the arities *) let arities = List.map (interp_ind_arity evdref env_params) indl in - let fullarities = List.map (fun c -> it_mkProd_or_LetIn c ctx_params) arities in + let fullarities = List.map (fun (c, _) -> it_mkProd_or_LetIn c ctx_params) arities in let env_ar = push_types env0 indnames fullarities in let env_ar_params = push_rel_context ctx_params env_ar in (* Compute interpretation metadatas *) - let indimpls = List.map (fun _ -> userimpls) fullarities in - let impls = compute_interning_datas env0 Inductive params indnames fullarities indimpls in + let indimpls = List.map (fun (_, impls) -> userimpls @ lift_implicits (List.length userimpls) impls) arities in + let arities = List.map fst arities in + let impls = compute_full_internalization_env env0 Inductive params indnames fullarities indimpls in let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in let constructors = - States.with_state_protection (fun () -> + States.with_state_protection (fun () -> (* Temporary declaration of notations and scopes *) - List.iter (declare_interning_data impls) notations; + List.iter (Metasyntax.set_notation_for_interpretation impls) notations; (* Interpret the constructor types *) list_map3 (interp_cstrs evdref env_ar_params impls) mldatas arities indl) () in @@ -556,7 +258,7 @@ let interp_mutual paramsl indl notations finite = (* Instantiate evars and check all are resolved *) let evd,_ = consider_remaining_unif_problems env_params !evdref in let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env_params evd in - let sigma = evars_of evd in + let sigma = evd in let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map (nf_evar sigma) cl,impsl)) constructors in let ctx_params = Sign.map_rel_context (nf_evar sigma) ctx_params in let arities = List.map (nf_evar sigma) arities in @@ -565,7 +267,7 @@ let interp_mutual paramsl indl notations finite = List.iter (fun (_,ctyps,_) -> List.iter (check_evars env_ar_params Evd.empty evd) ctyps) constructors; - + (* Build the inductive entries *) let entries = list_map3 (fun ind arity (cnames,ctypes,cimpls) -> { mind_entry_typename = ind.ind_name; @@ -573,17 +275,17 @@ let interp_mutual paramsl indl notations finite = mind_entry_consnames = cnames; mind_entry_lc = ctypes }) indl arities constructors in - let impls = + let impls = let len = List.length ctx_params in - List.map (fun (_,_,impls) -> - userimpls, List.map (fun impls -> - userimpls @ (lift_implicits len impls)) impls) constructors + List.map2 (fun indimpls (_,_,cimpls) -> + indimpls, List.map (fun impls -> + userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors in (* Build the mutual inductive entry *) { mind_entry_params = List.map prepare_param ctx_params; - mind_entry_record = false; - mind_entry_finite = finite; - mind_entry_inds = entries }, + mind_entry_record = false; + mind_entry_finite = finite; + mind_entry_inds = entries }, impls let eq_constr_expr c1 c2 = @@ -604,7 +306,7 @@ let eq_local_binders bl1 bl2 = List.length bl1 = List.length bl2 && List.for_all2 eq_local_binder bl1 bl2 let extract_coercions indl = - let mkqid (_,((_,id),_)) = make_short_qualid id in + let mkqid (_,((_,id),_)) = qualid_of_ident id in let extract lc = List.filter (fun (iscoe,_) -> iscoe) lc in List.map mkqid (List.flatten(List.map (fun (_,_,_,lc) -> extract lc) indl)) @@ -613,88 +315,64 @@ let extract_params indl = match paramsl with | [] -> anomaly "empty list of inductive types" | params::paramsl -> - if not (List.for_all (eq_local_binders params) paramsl) then error + if not (List.for_all (eq_local_binders params) paramsl) then error "Parameters should be syntactically the same for each inductive type."; params -let prepare_inductive ntnl indl = - let indl = - List.map (fun ((_,indname),_,ar,lc) -> { - ind_name = indname; - ind_arity = Option.cata (fun x -> x) (CSort (dummy_loc, Rawterm.RType None)) ar; - ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc - }) indl in - List.fold_right Option.List.cons ntnl [], indl - - -let elim_flag = ref true -let _ = - declare_bool_option - { optsync = true; - optname = "automatic declaration of eliminations"; - optkey = (SecondaryTable ("Elimination","Schemes")); - optread = (fun () -> !elim_flag) ; - optwrite = (fun b -> elim_flag := b) } - -let declare_mutual_with_eliminations isrecord mie impls = +let extract_inductive indl = + List.map (fun ((_,indname),_,ar,lc) -> { + ind_name = indname; + ind_arity = Option.cata (fun x -> x) (CSort (dummy_loc, Rawterm.RType None)) ar; + ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc + }) indl + +let extract_mutual_inductive_declaration_components indl = + let indl,ntnl = List.split indl in + let params = extract_params indl in + let coes = extract_coercions indl in + let indl = extract_inductive indl in + (params,indl), coes, List.flatten ntnl + +let declare_mutual_inductive_with_eliminations isrecord mie impls = let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in - let (_,kn) = declare_mind isrecord mie in - list_iter_i (fun i (indimpls, constrimpls) -> - let ind = (kn,i) in - maybe_declare_manual_implicits false (IndRef ind) indimpls; - list_iter_i - (fun j impls -> - maybe_declare_manual_implicits false (ConstructRef (ind, succ j)) impls) - constrimpls) + let (_,kn) = declare_mind isrecord mie in + let mind = Global.mind_of_delta (mind_of_kn kn) in + list_iter_i (fun i (indimpls, constrimpls) -> + let ind = (mind,i) in + Autoinstance.search_declaration (IndRef ind); + maybe_declare_manual_implicits false (IndRef ind) indimpls; + list_iter_i + (fun j impls -> +(* Autoinstance.search_declaration (ConstructRef (ind,j));*) + maybe_declare_manual_implicits false (ConstructRef (ind, succ j)) impls) + constrimpls) impls; - if_verbose ppnl (minductive_message names); - if !elim_flag then declare_eliminations kn; - kn + if_verbose ppnl (minductive_message names); + declare_default_schemes mind; + mind -let build_mutual l finite = - let indl,ntnl = List.split l in - let paramsl = extract_params indl in - let coes = extract_coercions indl in - let notations,indl = prepare_inductive ntnl indl in - let mie,impls = interp_mutual paramsl indl notations finite in - (* Declare the mutual inductive block with its eliminations *) - ignore (declare_mutual_with_eliminations false mie impls); +open Vernacexpr + +type one_inductive_impls = + Impargs.manual_explicitation list (* for inds *)* + Impargs.manual_explicitation list list (* for constrs *) + +type one_inductive_expr = + lident * local_binder list * constr_expr option * constructor_expr list + +let do_mutual_inductive indl finite = + let indl,coes,ntns = extract_mutual_inductive_declaration_components indl in + (* Interpret the types *) + let mie,impls = interp_mutual_inductive indl ntns finite in + (* Declare the mutual inductive block with its associated schemes *) + ignore (declare_mutual_inductive_with_eliminations UserVerbose mie impls); (* Declare the possible notations of inductive types *) - List.iter (declare_interning_data ([],[])) notations; + List.iter Metasyntax.add_notation_interpretation ntns; (* Declare the coercions *) List.iter (fun qid -> Class.try_add_new_coercion (locate qid) Global) coes (* 3c| Fixpoints and co-fixpoints *) -let pr_rank = function - | 0 -> str "1st" - | 1 -> str "2nd" - | 2 -> str "3rd" - | n -> str ((string_of_int (n+1))^"th") - -let recursive_message indexes = function - | [] -> anomaly "no recursive definition" - | [id] -> pr_id id ++ str " is recursively defined" ++ - (match indexes with - | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)" - | _ -> mt ()) - | l -> hov 0 (prlist_with_sep pr_coma pr_id l ++ - spc () ++ str "are recursively defined" ++ - match indexes with - | Some a -> spc () ++ str "(decreasing respectively on " ++ - prlist_with_sep pr_coma pr_rank (Array.to_list a) ++ - str " arguments)" - | None -> mt ()) - -let corecursive_message _ = function - | [] -> error "No corecursive definition." - | [id] -> pr_id id ++ str " is corecursively defined" - | l -> hov 0 (prlist_with_sep pr_coma pr_id l ++ - spc () ++ str "are corecursively defined") - -let recursive_message isfix = - if isfix=Fixpoint then recursive_message else corecursive_message - (* An (unoptimized) function that maps preorders to partial orders... Input: a list of associations (x,[y1;...;yn]), all yi distincts @@ -717,11 +395,11 @@ let rec partial_order = function | (z, Inr zge) when List.mem x zge -> (z, Inr (list_union zge xge')) | r -> r) res in (x,Inr xge')::res - | y::xge -> - let rec link y = + | y::xge -> + let rec link y = try match List.assoc y res with | Inl z -> link z - | Inr yge -> + | Inr yge -> if List.mem x yge then let res = List.remove_assoc y res in let res = List.map (function @@ -737,43 +415,41 @@ let rec partial_order = function browse res (list_add_set y (list_union xge' yge)) xge with Not_found -> browse res (list_add_set y xge') xge in link y - in browse (partial_order rest) [] xge + in browse (partial_order rest) [] xge -let non_full_mutual_message x xge y yge kind rest = - let reason = - if List.mem x yge then +let non_full_mutual_message x xge y yge isfix rest = + let reason = + if List.mem x yge then string_of_id y^" depends on "^string_of_id x^" but not conversely" - else if List.mem y xge then + else if List.mem y xge then string_of_id x^" depends on "^string_of_id y^" but not conversely" else string_of_id y^" and "^string_of_id x^" are not mutually dependent" in let e = if rest <> [] then "e.g.: "^reason else reason in - let k = if kind=Fixpoint then "fixpoint" else "cofixpoint" in + let k = if isfix then "fixpoint" else "cofixpoint" in let w = - if kind=Fixpoint then "Well-foundedness check may fail unexpectedly.\n" - else "" in - "Not a fully mutually defined "^k^"\n("^e^").\n"^w + if isfix + then strbrk "Well-foundedness check may fail unexpectedly." ++ fnl() + else mt () in + strbrk ("Not a fully mutually defined "^k) ++ fnl () ++ + strbrk ("("^e^").") ++ fnl () ++ w -let check_mutuality env kind fixl = +let check_mutuality env isfix fixl = let names = List.map fst fixl in let preorder = - List.map (fun (id,def) -> + List.map (fun (id,def) -> (id, List.filter (fun id' -> id<>id' & occur_var env id' def) names)) fixl in let po = partial_order preorder in match List.filter (function (_,Inr _) -> true | _ -> false) po with | (x,Inr xge)::(y,Inr yge)::rest -> - if_verbose warning (non_full_mutual_message x xge y yge kind rest) + if_verbose msg_warning (non_full_mutual_message x xge y yge isfix rest) | _ -> () -type fixpoint_kind = - | IsFixpoint of (identifier located option * recursion_order_expr) list - | IsCoFixpoint - -type fixpoint_expr = { +type structured_fixpoint_expr = { fix_name : identifier; fix_binders : local_binder list; - fix_body : constr_expr; + fix_body : constr_expr option; fix_type : constr_expr } @@ -784,9 +460,10 @@ let interp_fix_ccl evdref (env,_) fix = interp_type_evars evdref env fix.fix_type let interp_fix_body evdref env_rec impls (_,ctx) fix ccl = - let env = push_rel_context ctx env_rec in - let body = interp_casted_constr_evars evdref env ~impls fix.fix_body ccl in - it_mkLambda_or_LetIn body ctx + Option.map (fun body -> + let env = push_rel_context ctx env_rec in + let body = interp_casted_constr_evars evdref env ~impls body ccl in + it_mkLambda_or_LetIn body ctx) fix.fix_body let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx @@ -799,9 +476,10 @@ let declare_fix boxed kind f def t imps = } in let kn = declare_constant f (DefinitionEntry ce,IsDefinition kind) in let gr = ConstRef kn in - maybe_declare_manual_implicits false gr imps; - gr - + Autoinstance.search_declaration (ConstRef kn); + maybe_declare_manual_implicits false gr imps; + gr + 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 @@ -809,454 +487,135 @@ let prepare_recursive_declaration fixnames fixtypes fixdefs = (* Jump over let-bindings. *) -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 -> +let compute_possible_guardness_evidences na fix (ids,_) = + match index_of_annot fix.fix_binders na with + | Some i -> [i] + | 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 + 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 + interval 0 (List.length ids - 1) + +type recursive_preentry = + identifier list * constr option list * types list -let interp_recursive fixkind l boxed = +let interp_recursive isfix fixl notations = let env = Global.env() in - let fixl, ntnl = List.split l in - let kind = if fixkind <> IsCoFixpoint then Fixpoint else CoFixpoint in let fixnames = List.map (fun fix -> fix.fix_name) fixl in (* Interp arities allowing for unresolved types *) - let evdref = ref (Evd.create_evar_defs Evd.empty) in + 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 fixtypes = List.map (nf_evar (evars_of !evdref)) fixtypes in + let fixtypes = List.map (nf_evar !evdref) fixtypes in let env_rec = push_named_types env fixnames fixtypes in (* Get interpretation metadatas *) - let impls = compute_interning_datas env Recursive [] fixnames fixtypes fiximps in - let notations = List.fold_right Option.List.cons ntnl [] in + let impls = compute_full_internalization_env env Recursive [] fixnames fixtypes fiximps in (* Interp bodies with rollback because temp use of notations/implicit *) - let fixdefs = - States.with_state_protection (fun () -> - List.iter (declare_interning_data impls) notations; + 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 (* Instantiate evars and check all are resolved *) let evd,_ = consider_remaining_unif_problems env_rec !evdref in - let fixdefs = List.map (nf_evar (evars_of evd)) fixdefs in - let fixtypes = List.map (nf_evar (evars_of evd)) fixtypes in + let fixdefs = List.map (Option.map (nf_evar evd)) fixdefs in + let fixtypes = List.map (nf_evar evd) fixtypes in + let fixctxnames = List.map (fun (_,ctx) -> List.map pi1 ctx) fixctxs in let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env evd in - List.iter (check_evars env_rec Evd.empty evd) fixdefs; + List.iter (Option.iter (check_evars env_rec Evd.empty evd)) fixdefs; List.iter (check_evars env Evd.empty evd) fixtypes; - check_mutuality env kind (List.combine fixnames fixdefs); + if not (List.mem None fixdefs) then begin + let fixdefs = List.map Option.get fixdefs in + check_mutuality env isfix (List.combine fixnames fixdefs) + end; (* Build the fix declaration block *) - let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in - let indexes, fixdecls = - match fixkind with - | IsFixpoint wfl -> - let possible_indexes = - list_map3 compute_possible_guardness_evidences wfl fixctxs fixtypes in - let indexes = search_guard dummy_loc env possible_indexes fixdecls in - Some indexes, list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 l - | IsCoFixpoint -> - None, list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 l - in - - (* Declare the recursive definitions *) - ignore (list_map4 (declare_fix boxed kind) fixnames fixdecls fixtypes fiximps); - if_verbose ppnl (recursive_message kind indexes fixnames); - + (fixnames,fixdefs,fixtypes),List.combine fixctxnames fiximps + +let interp_fixpoint = interp_recursive true +let interp_cofixpoint = interp_recursive false + +let declare_fixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns = + if List.mem None fixdefs then + (* Some bodies to define by proof *) + let thms = + list_map3 (fun id t imps -> (id,(t,imps))) fixnames fixtypes fiximps in + let init_tac = + Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC) + fixdefs) in + Lemmas.start_proof_with_initialization (Global,DefinitionBody Fixpoint) + (Some(false,indexes,init_tac)) thms None (fun _ _ -> ()) + else begin + (* We shortcut the proof process *) + let fixdefs = List.map Option.get fixdefs in + let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in + let indexes = search_guard dummy_loc (Global.env()) indexes fixdecls in + let fiximps = List.map snd fiximps in + let fixdecls = + list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in + ignore (list_map4 (declare_fix boxed Fixpoint) fixnames fixdecls fixtypes fiximps); + (* Declare the recursive definitions *) + fixpoint_message (Some indexes) fixnames; + end; (* Declare notations *) - List.iter (declare_interning_data ([],[])) notations - -let build_recursive l b = - let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in - let fixl = List.map (fun (((_,id),_,bl,typ,def),ntn) -> - ({fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ},ntn)) - l in - interp_recursive (IsFixpoint g) fixl b - -let build_corecursive l b = - let fixl = List.map (fun (((_,id),bl,typ,def),ntn) -> - ({fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ},ntn)) - l in - interp_recursive IsCoFixpoint fixl b - -(* 3d| Schemes *) -let rec split_scheme l = - let env = Global.env() in - match l with - | [] -> [],[] - | (Some id,t)::q -> let l1,l2 = split_scheme q in - ( match t with - | InductionScheme (x,y,z) -> ((id,x,y,z)::l1),l2 - | EqualityScheme x -> l1,(x::l2) - ) -(* - if no name has been provided, we build one from the types of the ind -requested -*) - | (None,t)::q -> - let l1,l2 = split_scheme q in - ( match t with - | InductionScheme (x,y,z) -> - let ind = mkInd (Nametab.inductive_of_reference y) in - let sort_of_ind = family_of_sort (Typing.sort_of env Evd.empty ind) -in - let z' = family_of_sort (interp_sort z) in - let suffix = ( - match sort_of_ind with - | InProp -> - if x then (match z' with - | InProp -> "_ind_nodep" - | InSet -> "_rec_nodep" - | InType -> "_rect_nodep") - else ( match z' with - | InProp -> "_ind" - | InSet -> "_rec" - | InType -> "_rect" ) - | _ -> - if x then (match z' with - | InProp -> "_ind" - | InSet -> "_rec" - | InType -> "_rect" ) - else (match z' with - | InProp -> "_ind_nodep" - | InSet -> "_rec_nodep" - | InType -> "_rect_nodep") - ) in - let newid = (string_of_id (Pcoq.coerce_global_to_id y))^suffix in - let newref = (dummy_loc,id_of_string newid) in - ((newref,x,y,z)::l1),l2 - | EqualityScheme x -> l1,(x::l2) - ) - - -let build_induction_scheme lnamedepindsort = - let lrecnames = List.map (fun ((_,f),_,_,_) -> f) lnamedepindsort - and sigma = Evd.empty - and env0 = Global.env() in - let lrecspec = - List.map - (fun (_,dep,indid,sort) -> - let ind = Nametab.inductive_of_reference indid in - let (mib,mip) = Global.lookup_inductive ind in - (ind,mib,mip,dep,interp_elimination_sort sort)) - lnamedepindsort - in - let listdecl = Indrec.build_mutual_indrec env0 sigma lrecspec in - let rec declare decl fi lrecref = - let decltype = Retyping.get_type_of env0 Evd.empty decl in - let decltype = refresh_universes decltype in - let ce = { const_entry_body = decl; - const_entry_type = Some decltype; - const_entry_opaque = false; - const_entry_boxed = Flags.boxed_definitions() } in - let kn = declare_constant fi (DefinitionEntry ce, IsDefinition Scheme) in - ConstRef kn :: lrecref - in - let _ = List.fold_right2 declare listdecl lrecnames [] in - if_verbose ppnl (recursive_message Fixpoint None lrecnames) - -let build_scheme l = - let ischeme,escheme = split_scheme l in -(* we want 1 kind of scheme at a time so we check if the user -tried to declare different schemes at once *) - if (ischeme <> []) && (escheme <> []) - then - error "Do not declare equality and induction scheme at the same time." - else ( - if ischeme <> [] then build_induction_scheme ischeme; - List.iter ( fun indname -> - let ind = Nametab.inductive_of_reference indname - in declare_eq_scheme (fst ind); - try - make_eq_decidability ind - with _ -> - Pfedit.delete_current_proof(); - message "Error while computing decidability scheme. Please report." - ) escheme - ) - -let list_split_rev_at index l = - let rec aux i acc = function - hd :: tl when i = index -> acc, tl - | hd :: tl -> aux (succ i) (hd :: acc) tl - | [] -> failwith "list_split_at: Invalid argument" - in aux 0 [] l - -let fold_left' f = function - [] -> raise (Invalid_argument "fold_right'") - | hd :: tl -> List.fold_left f hd tl - -let build_combined_scheme name schemes = - let env = Global.env () in -(* let nschemes = List.length schemes in *) - let find_inductive ty = - let (ctx, arity) = decompose_prod ty in - let (_, last) = List.hd ctx in - match kind_of_term last with - | App (ind, args) -> - let ind = destInd ind in - let (_,spec) = Inductive.lookup_mind_specif env ind in - ctx, ind, spec.mind_nrealargs - | _ -> ctx, destInd last, 0 - in - let defs = - List.map (fun x -> - let refe = Ident x in - let qualid = qualid_of_reference refe in - let cst = try Nametab.locate_constant (snd qualid) - with Not_found -> error ((string_of_qualid (snd qualid))^" is not declared.") - in - let ty = Typeops.type_of_constant env cst in - qualid, cst, ty) - schemes - in - let (qid, c, t) = List.hd defs in - let ctx, ind, nargs = find_inductive t in - (* Number of clauses, including the predicates quantification *) - let prods = nb_prod t - (nargs + 1) in - let coqand = Coqlib.build_coq_and () and coqconj = Coqlib.build_coq_conj () in - let relargs = rel_vect 0 prods in - let concls = List.rev_map - (fun (_, cst, t) -> - mkApp(mkConst cst, relargs), - snd (decompose_prod_n prods t)) defs in - let concl_bod, concl_typ = - fold_left' - (fun (accb, acct) (cst, x) -> - mkApp (coqconj, [| x; acct; cst; accb |]), - mkApp (coqand, [| x; acct |])) concls - in - let ctx, _ = - list_split_rev_at prods - (List.rev_map (fun (x, y) -> x, None, y) ctx) in - let typ = it_mkProd_wo_LetIn concl_typ ctx in - let body = it_mkLambda_or_LetIn concl_bod ctx in - let ce = { const_entry_body = body; - const_entry_type = Some typ; - const_entry_opaque = false; - const_entry_boxed = Flags.boxed_definitions() } in - let _ = declare_constant (snd name) (DefinitionEntry ce, IsDefinition Scheme) in - if_verbose ppnl (recursive_message Fixpoint None [snd name]) -(* 4| Goal declaration *) - -(* 4.1| Support for mutually proved theorems *) - -let retrieve_first_recthm = function - | VarRef id -> - (pi2 (Global.lookup_named id),variable_opacity id) - | ConstRef cst -> - let {const_body=body;const_opaque=opaq} = Global.lookup_constant cst in - (Option.map Declarations.force body,opaq) - | _ -> assert false - -let default_thm_id = id_of_string "Unnamed_thm" - -let compute_proof_name = function - | Some (loc,id) -> - (* We check existence here: it's a bit late at Qed time *) - if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then - user_err_loc (loc,"",pr_id id ++ str " already exists."); - id - | None -> - let rec next avoid id = - let id = next_global_ident_away false id avoid in - if Nametab.exists_cci (Lib.make_path id) then next (id::avoid) id - else id - in - next (Pfedit.get_all_proof_names ()) default_thm_id - -let save_remaining_recthms (local,kind) body opaq i (id,(t_i,imps)) = - match body with - | None -> - (match local with - | Local -> - let impl=false in (* copy values from Vernacentries *) - let k = IsAssumption Conjectural in - let c = SectionLocalAssum (t_i,impl,[]) in - let _ = declare_variable id (Lib.cwd(),c,k) in - (Local,VarRef id,imps) - | Global -> - let k = IsAssumption Conjectural in - let kn = declare_constant id (ParameterEntry (t_i,false), k) in - (Global,ConstRef kn,imps)) - | Some body -> - let k = logical_kind_of_goal_kind kind in - let body_i = match kind_of_term body with - | Fix ((nv,0),decls) -> mkFix ((nv,i),decls) - | CoFix (0,decls) -> mkCoFix (i,decls) - | _ -> anomaly "Not a proof by induction" in - match local with - | Local -> - let c = SectionLocalDef (body_i, Some t_i, opaq) in - let _ = declare_variable id (Lib.cwd(), c, k) in - (Local,VarRef id,imps) - | Global -> - let const = - { const_entry_body = body_i; - const_entry_type = Some t_i; - const_entry_opaque = opaq; - const_entry_boxed = false (* copy of what cook_proof does *)} in - let kn = declare_constant id (DefinitionEntry const, k) in - (Global,ConstRef kn,imps) - -let look_for_mutual_statements thms = - if List.tl thms <> [] then - (* More than one statement: we look for a common inductive hyp or a *) - (* common coinductive conclusion *) - let n = List.length thms in - let inds = List.map (fun (id,(t,_) as x) -> - let (hyps,ccl) = Sign.decompose_prod_assum t in - let whnf_hyp_hds = fold_map_rel_context - (fun env c -> fst (whd_betadeltaiota_stack env Evd.empty c)) - (Global.env()) hyps in - let ind_hyps = - List.flatten (list_map_i (fun i (_,b,t) -> - match kind_of_term t with - | Ind (kn,_ as ind) when - let mind = Global.lookup_mind kn in - mind.mind_finite & b = None -> - [ind,x,i] - | _ -> - []) 1 (List.rev whnf_hyp_hds)) in - let ind_ccl = - let cclenv = push_rel_context hyps (Global.env()) in - let whnf_ccl,_ = whd_betadeltaiota_stack cclenv Evd.empty ccl in - match kind_of_term whnf_ccl with - | Ind (kn,_ as ind) when - let mind = Global.lookup_mind kn in - mind.mind_ntypes = n & not mind.mind_finite -> - [ind,x,0] - | _ -> - [] in - ind_hyps,ind_ccl) thms in - let inds_hyps,ind_ccls = List.split inds in - let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> kn = kn' in - (* Check if all conclusions are coinductive in the same type *) - (* (degenerated cartesian product since there is at most one coind ccl) *) - let same_indccl = - list_cartesians_filter (fun hyp oks -> - if List.for_all (of_same_mutind hyp) oks - then Some (hyp::oks) else None) [] ind_ccls in - let ordered_same_indccl = - List.filter (list_for_all_i (fun i ((kn,j),_,_) -> i=j) 0) same_indccl in - (* Check if some hypotheses are inductive in the same type *) - let common_same_indhyp = - list_cartesians_filter (fun hyp oks -> - if List.for_all (of_same_mutind hyp) oks - then Some (hyp::oks) else None) [] inds_hyps in - let ordered_inds,finite = - match ordered_same_indccl, common_same_indhyp with - | indccl::rest, _ -> - assert (rest=[]); - (* One occ. of common coind ccls and no common inductive hyps *) - if common_same_indhyp <> [] then - if_verbose warning "Assuming mutual coinductive statements."; - flush_all (); - indccl, true - | [], _::_ -> - if same_indccl <> [] && - list_distinct (List.map pi1 (List.hd same_indccl)) then - if_verbose warn (strbrk "Coinductive statements do not follow the order of definition, assume the proof to be by induction."); flush_all (); - (* assume the largest indices as possible *) - list_last common_same_indhyp, false - | _, [] -> - error - ("Cannot find common (mutual) inductive premises or coinductive" ^ - " conclusions in the statements.") - in - let nl,thms = List.split (List.map (fun (_,x,i) -> (i,x)) ordered_inds) in - let rec_tac = - if finite then - match List.map (fun (id,(t,_)) -> (id,t)) thms with - | (id,_)::l -> Hiddentac.h_mutual_cofix true id l - | _ -> assert false - else - (* nl is dummy: it will be recomputed at Qed-time *) - match List.map2 (fun (id,(t,_)) n -> (id,n,t)) thms nl with - | (id,n,_)::l -> Hiddentac.h_mutual_fix true id n l - | _ -> assert false in - Some rec_tac,thms - else - None, thms - -(* 4.2| General support for goals *) - -let start_proof_com kind thms hook = - let thms = List.map (fun (sopt,(bl,t)) -> - (compute_proof_name sopt, - interp_type_evars_impls (Global.env()) (generalize_constr_expr t bl))) - thms in - let rec_tac,thms = look_for_mutual_statements thms in - match thms with - | [] -> anomaly "No proof to start" - | (id,(t,imps))::other_thms -> - let hook strength ref = - let other_thms_data = - if other_thms = [] then [] else - (* there are several theorems defined mutually *) - let body,opaq = retrieve_first_recthm ref in - list_map_i (save_remaining_recthms kind body opaq) 1 other_thms in - let thms_data = (strength,ref,imps)::other_thms_data in - List.iter (fun (strength,ref,imps) -> - maybe_declare_manual_implicits false ref imps; - hook strength ref) thms_data in - start_proof id kind t ?init_tac:rec_tac - ~compute_guard:(rec_tac<>None) hook - -let check_anonymity id save_ident = - if atompart_of_id id <> "Unnamed_thm" then - error "This command can only be used for unnamed theorem." -(* - message("Overriding name "^(string_of_id id)^" and using "^save_ident) -*) - -let save_anonymous opacity save_ident = - let id,(const,do_guard,persistence,hook) = Pfedit.cook_proof !save_hook in - let const = { const with const_entry_opaque = opacity } in - check_anonymity id save_ident; - save save_ident const do_guard persistence hook - -let save_anonymous_with_strength kind opacity save_ident = - let id,(const,do_guard,_,hook) = Pfedit.cook_proof !save_hook in - let const = { const with const_entry_opaque = opacity } in - check_anonymity id save_ident; - (* we consider that non opaque behaves as local for discharge *) - save save_ident const do_guard (Global, Proof kind) hook - -let admit () = - let (id,k,typ,hook) = Pfedit.current_proof_statement () in -(* Contraire aux besoins d'interactivité... - if k <> IsGlobal (Proof Conjecture) then - error "Only statements declared as conjecture can be admitted"; -*) - let kn = - declare_constant id (ParameterEntry (typ,false), IsAssumption Conjectural) in - Pfedit.delete_current_proof (); - assumption_message id; - hook Global (ConstRef kn) + List.iter Metasyntax.add_notation_interpretation ntns + +let declare_cofixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) ntns = + if List.mem None fixdefs then + (* Some bodies to define by proof *) + let thms = + list_map3 (fun id t imps -> (id,(t,imps))) fixnames fixtypes fiximps in + let init_tac = + Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC) + fixdefs) in + Lemmas.start_proof_with_initialization (Global,DefinitionBody CoFixpoint) + (Some(true,[],init_tac)) thms None (fun _ _ -> ()) + else begin + (* We shortcut the proof process *) + let fixdefs = List.map Option.get fixdefs in + let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in + let fixdecls = list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in + let fiximps = List.map snd fiximps in + ignore (list_map4 (declare_fix boxed CoFixpoint) fixnames fixdecls fixtypes fiximps); + (* Declare the recursive definitions *) + cofixpoint_message fixnames + end; + (* Declare notations *) + List.iter Metasyntax.add_notation_interpretation ntns -let get_current_context () = - try Pfedit.get_current_goal_context () - with e when Logic.catchable_exception e -> - (Evd.empty, Global.env()) +let extract_decreasing_argument = function + | (_,(na,CStructRec),_,_,_) -> na + | _ -> error + "Only structural decreasing is supported for a non-Program Fixpoint" +let extract_fixpoint_components l = + let fixl, ntnl = List.split l in + let wfl = List.map extract_decreasing_argument fixl in + let fixl = List.map (fun ((_,id),_,bl,typ,def) -> + {fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ}) fixl in + fixl, List.flatten ntnl, wfl +let extract_cofixpoint_components l = + let fixl, ntnl = List.split l in + List.map (fun ((_,id),bl,typ,def) -> + {fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ}) fixl, + List.flatten ntnl + +let do_fixpoint l b = + let fixl,ntns,wfl = extract_fixpoint_components l in + let fix = interp_fixpoint fixl ntns in + let possible_indexes = + list_map3 compute_possible_guardness_evidences wfl fixl (snd fix) in + declare_fixpoint b fix possible_indexes ntns + +let do_cofixpoint l b = + let fixl,ntns = extract_cofixpoint_components l in + declare_cofixpoint b (interp_cofixpoint fixl ntns) ntns |