diff options
author | soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-04-25 15:13:45 +0000 |
---|---|---|
committer | soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-04-25 15:13:45 +0000 |
commit | 40425048feff138e6c67555c7ee94142452d1cae (patch) | |
tree | b26134c830f386838f219b92a1c8960dd50c4287 | |
parent | 2c75beb4e24c91d3ecab07ca9279924205002ada (diff) |
New keyword "Inline" for Parameters and Axioms for automatic
delta-reduction at fonctor application.
Example:
Module Type S.
Parameter Inline N : Set.
End S.
Module F (X:S).
Definition t := X.N.
End F.
Module M.
Definition N := nat.
End M.
Module G := F M.
Print G.t.
G.t = nat
: Set
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9795 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | contrib/interface/name_to_ast.ml | 2 | ||||
-rw-r--r-- | contrib/interface/xlate.ml | 5 | ||||
-rw-r--r-- | contrib/subtac/subtac.ml | 12 | ||||
-rw-r--r-- | contrib/subtac/subtac_obligations.ml | 2 | ||||
-rw-r--r-- | ide/coq.ml | 2 | ||||
-rw-r--r-- | kernel/cooking.ml | 2 | ||||
-rw-r--r-- | kernel/cooking.mli | 3 | ||||
-rw-r--r-- | kernel/declarations.ml | 6 | ||||
-rw-r--r-- | kernel/declarations.mli | 3 | ||||
-rw-r--r-- | kernel/entries.ml | 2 | ||||
-rw-r--r-- | kernel/entries.mli | 2 | ||||
-rw-r--r-- | kernel/modops.ml | 26 | ||||
-rw-r--r-- | kernel/term_typing.ml | 11 | ||||
-rw-r--r-- | kernel/term_typing.mli | 4 | ||||
-rw-r--r-- | library/declare.ml | 2 | ||||
-rw-r--r-- | parsing/g_vernac.ml4 | 11 | ||||
-rw-r--r-- | parsing/ppvernac.ml | 2 | ||||
-rw-r--r-- | tactics/setoid_replace.ml | 2 | ||||
-rw-r--r-- | tactics/tactics.ml | 2 | ||||
-rw-r--r-- | toplevel/command.ml | 10 | ||||
-rw-r--r-- | toplevel/command.mli | 7 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 6 | ||||
-rw-r--r-- | toplevel/vernacexpr.ml | 2 |
23 files changed, 76 insertions, 50 deletions
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml index 9a503cfb5..bbde91aac 100644 --- a/contrib/interface/name_to_ast.ml +++ b/contrib/interface/name_to_ast.ml @@ -134,7 +134,7 @@ let implicits_to_ast_list implicits = let make_variable_ast name typ implicits = (VernacAssumption - ((Local,Definitional), + ((Local,Definitional),false,(*inline flag*) [false,([dummy_loc,name], constr_to_ast (body_of_type typ))])) ::(implicits_to_ast_list implicits);; diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 6d52be45d..639b4ae74 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1848,8 +1848,9 @@ let rec xlate_vernac = (xlate_defn kind, xlate_ident s, xlate_binder_list bl, cvt_optional_eval_for_definition c red_option, xlate_formula_opt typ_opt) - | VernacAssumption (kind, b) -> - CT_variable (xlate_var kind, cvt_vernac_binders b) + | VernacAssumption (kind,inline ,b) ->xlate_error "TODO: Parameter Inline" + (*inline : bool -> automatic delta reduction at fonctor application*) + (* CT_variable (xlate_var kind, cvt_vernac_binders b)*) | VernacCheckMayEval (None, numopt, c) -> CT_check (xlate_formula c) | VernacSearch (s,x) -> diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml index ff5df49e3..eb1d5baf7 100644 --- a/contrib/subtac/subtac.ml +++ b/contrib/subtac/subtac.ml @@ -78,18 +78,18 @@ let _ = Detyping.set_detype_anonymous (fun loc n -> RVar (loc, id_of_string ("An let assumption_message id = Options.if_verbose message ((string_of_id id) ^ " is assumed") -let declare_assumption env isevars idl is_coe k bl c = +let declare_assumption env isevars idl is_coe k bl c nl = if not (Pfedit.refining ()) then let evm, c, typ = Subtac_pretyping.subtac_process env isevars (snd (List.hd idl)) [] (Command.generalize_constr_expr c bl) None in - List.iter (Command.declare_one_assumption is_coe k c) idl + List.iter (Command.declare_one_assumption is_coe k c nl) idl else errorlabstrm "Command.Assumption" (str "Cannot declare an assumption while in proof editing mode.") -let vernac_assumption env isevars kind l = - List.iter (fun (is_coe,(idl,c)) -> declare_assumption env isevars idl is_coe kind [] c) l +let vernac_assumption env isevars kind l nl = + List.iter (fun (is_coe,(idl,c)) -> declare_assumption env isevars idl is_coe kind [] c nl) l let subtac (loc, command) = @@ -123,8 +123,8 @@ let subtac (loc, command) = start_proof_and_print env isevars (Some id) (Global, Proof thkind) (bl,t) hook - | VernacAssumption (stre,l) -> - vernac_assumption env isevars stre l + | VernacAssumption (stre,nl,l) -> + vernac_assumption env isevars stre l nl (*| VernacEndProof e -> subtac_end_proof e*) diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index e2101a2d9..34758721f 100644 --- a/contrib/subtac/subtac_obligations.ml +++ b/contrib/subtac/subtac_obligations.ml @@ -405,7 +405,7 @@ let admit_obligations n = match x.obl_body with None -> let x = subst_deps_obl obls x in - let kn = Declare.declare_constant x.obl_name (ParameterEntry x.obl_type, IsAssumption Conjectural) in + let kn = Declare.declare_constant x.obl_name (ParameterEntry (x.obl_type,false), IsAssumption Conjectural) in assumption_message x.obl_name; { x with obl_body = Some (mkConst kn) } | Some _ -> x) diff --git a/ide/coq.ml b/ide/coq.ml index a7d8da813..16b2460ad 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -354,7 +354,7 @@ let compute_reset_info = function | VernacDefineModule (_,(_,id), _, _, _) | VernacDeclareModule (_,(_,id), _, _) | VernacDeclareModuleType ((_,id), _, _) - | VernacAssumption (_, (_,((_,id)::_,_))::_) + | VernacAssumption (_,_ ,(_,((_,id)::_,_))::_) | VernacInductive (_, (((_,id),_,_,_),_) :: _) -> Reset (id, ref true) | VernacDefinition (_, (_,id), ProveBody _, _) diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 7751e5bf6..e9200cd75 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -131,4 +131,4 @@ let cook_constant env r = let typ = abstract_constant_type (expmod_constr r.d_modlist t) hyps in Typeops.make_polymorphic_if_arity env typ in let boxed = Cemitcodes.is_boxed cb.const_body_code in - (body, typ, cb.const_constraints, cb.const_opaque, boxed) + (body, typ, cb.const_constraints, cb.const_opaque, boxed,false) diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 0646b1c22..4afdaa55e 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -25,7 +25,8 @@ type recipe = { val cook_constant : env -> recipe -> - constr_substituted option * constant_type * constraints * bool * bool + constr_substituted option * constant_type * constraints * bool * bool + * bool (*s Utility functions used in module [Discharge]. *) diff --git a/kernel/declarations.ml b/kernel/declarations.ml index d0f2289dc..1be251a50 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -49,7 +49,8 @@ type constant_body = { const_body_code : Cemitcodes.to_patch_substituted; (* const_type_code : Cemitcodes.to_patch; *) const_constraints : constraints; - const_opaque : bool } + const_opaque : bool; + const_inline : bool} (*s Inductive types (internal representation with redundant information). *) @@ -202,7 +203,8 @@ let subst_const_body sub cb = { const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code; (*const_type_code = Cemitcodes.subst_to_patch sub cb.const_type_code;*) const_constraints = cb.const_constraints; - const_opaque = cb.const_opaque } + const_opaque = cb.const_opaque; + const_inline = cb.const_inline} let subst_arity sub = function | Monomorphic s -> diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 22cfd62a0..7f7f7dcc3 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -47,7 +47,8 @@ type constant_body = { const_body_code : to_patch_substituted; (*i const_type_code : to_patch;i*) const_constraints : constraints; - const_opaque : bool } + const_opaque : bool; + const_inline : bool} val subst_const_body : substitution -> constant_body -> constant_body diff --git a/kernel/entries.ml b/kernel/entries.ml index fb134b1c7..17da967c2 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -62,7 +62,7 @@ type definition_entry = { const_entry_opaque : bool; const_entry_boxed : bool} -type parameter_entry = types +type parameter_entry = types*bool type constant_entry = | DefinitionEntry of definition_entry diff --git a/kernel/entries.mli b/kernel/entries.mli index 61c0b8c3b..56ea852da 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -61,7 +61,7 @@ type definition_entry = { const_entry_opaque : bool; const_entry_boxed : bool } -type parameter_entry = types +type parameter_entry = types*bool (*inline flag*) type constant_entry = | DefinitionEntry of definition_entry diff --git a/kernel/modops.ml b/kernel/modops.ml index e9e1d67eb..96d19552a 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -235,13 +235,29 @@ and constants_of_modtype env mp modtype = | MTBfunsig _ -> [] (* returns a resolver for kn that maps mbid to mp *) -(* Nota: Some delta-expansions used to happen here. - Browse SVN if you want to know more. *) let resolver_of_environment mbid modtype mp env = let constants = constants_of_modtype env (MPbound mbid) modtype in - let resolve = List.map (fun (con,_) -> con,None) constants in - Mod_subst.make_resolver resolve - + let resolve = + List.map + (fun (con,expecteddef) -> + let con' = replace_mp_in_con (MPbound mbid) mp con in + let constr = + try + if expecteddef.Declarations.const_inline then + let constant = lookup_constant con' env in + if constant.Declarations.const_opaque then + None + else + option_map Declarations.force + constant.Declarations.const_body + else + None + with Not_found -> error_no_such_label (con_label con') + in + con,constr + ) constants + in + Mod_subst.make_resolver resolve let strengthen_const env mp l cb = match cb.const_opaque, cb.const_body with diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 8b0f45ac9..aedc44ac8 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -93,11 +93,11 @@ let infer_declaration env dcl = let (j,cst) = infer env c.const_entry_body in let (typ,cst) = constrain_type env j cst c.const_entry_type in Some (Declarations.from_val j.uj_val), typ, cst, - c.const_entry_opaque, c.const_entry_boxed - | ParameterEntry t -> + c.const_entry_opaque, c.const_entry_boxed, false + | ParameterEntry (t,nl) -> let (j,cst) = infer env t in None, NonPolymorphicType (Typeops.assumption_of_judgment env j), cst, - false, false + false, false, nl let global_vars_set_constant_type env = function | NonPolymorphicType t -> global_vars_set env t @@ -107,7 +107,7 @@ let global_vars_set_constant_type env = function (fun t c -> Idset.union (global_vars_set env t) c)) ctx ~init:Idset.empty -let build_constant_declaration env kn (body,typ,cst,op,boxed) = +let build_constant_declaration env kn (body,typ,cst,op,boxed,inline) = let ids = match body with | None -> global_vars_set_constant_type env typ @@ -124,7 +124,8 @@ let build_constant_declaration env kn (body,typ,cst,op,boxed) = const_body_code = tps; (* const_type_code = to_patch env typ;*) const_constraints = cst; - const_opaque = op } + const_opaque = op; + const_inline = inline} (*s Global and local constant declaration. *) diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 83434e2ec..abff3e8b7 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -26,10 +26,10 @@ val translate_local_assum : env -> types -> types * Univ.constraints val infer_declaration : env -> constant_entry -> - constr_substituted option * constant_type * constraints * bool * bool + constr_substituted option * constant_type * constraints * bool * bool * bool val build_constant_declaration : env -> 'a -> - constr_substituted option * constant_type * constraints * bool * bool -> + constr_substituted option * constant_type * constraints * bool * bool * bool -> constant_body val translate_constant : env -> constant -> constant_entry -> constant_body diff --git a/library/declare.ml b/library/declare.ml index f729f133d..6e9835487 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -177,7 +177,7 @@ let discharge_constant ((sp,kn),(cdt,dhyps,kind)) = Some (GlobalRecipe recipe,(discharged_hyps kn sechyps)@dhyps,kind) (* Hack to reduce the size of .vo: we keep only what load/open needs *) -let dummy_constant_entry = ConstantEntry (ParameterEntry mkProp) +let dummy_constant_entry = ConstantEntry (ParameterEntry (mkProp,false)) let dummy_constant (ce,_,mk) = dummy_constant_entry,[],mk diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 34d799745..6d0e3ffc4 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -120,11 +120,11 @@ GEXTEND Gram [ [ thm = thm_token; id = identref; bl = LIST0 binder_let; ":"; c = lconstr -> VernacStartTheoremProof (thm, id, (bl, c), false, no_hook) - | stre = assumption_token; bl = assum_list -> - VernacAssumption (stre, bl) - | stre = assumptions_token; bl = assum_list -> + | stre = assumption_token; nl = inline; bl = assum_list -> + VernacAssumption (stre, nl, bl) + | stre = assumptions_token; nl = inline; bl = assum_list -> test_plurial_form bl; - VernacAssumption (stre, bl) + VernacAssumption (stre, nl, bl) | IDENT "Boxed";"Definition";id = identref; b = def_body -> VernacDefinition ((Global,true,Definition), id, b, no_hook) | IDENT "Unboxed";"Definition";id = identref; b = def_body -> @@ -193,6 +193,9 @@ GEXTEND Gram | IDENT "Axioms" -> (Global, Logical) | IDENT "Parameters" -> (Global, Definitional) ] ] ; + inline: + [ ["Inline" -> true | -> false] ] + ; finite_token: [ [ "Inductive" -> true | "CoInductive" -> false ] ] diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 7d4104db3..c2571ad0a 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -515,7 +515,7 @@ let rec pr_vernac = function | Some tok -> str"Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_lident id)) | VernacExactProof c -> hov 2 (str"Proof" ++ pr_lconstrarg c) - | VernacAssumption (stre,l) -> + | VernacAssumption (stre,_,l) -> let n = List.length (List.flatten (List.map fst (List.map snd l))) in hov 2 (pr_assumption_token (n > 1) stre ++ spc() ++ diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 1273c65e4..269c40fec 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -908,7 +908,7 @@ let new_morphism m signature id hook = begin ignore (Declare.declare_internal_constant id - (ParameterEntry lem, IsAssumption Logical)) ; + (ParameterEntry (lem,false), IsAssumption Logical)) ; let mor_name = morphism_theory_id_of_morphism_proof_id id in let lemma_infos = Some (id,argsconstr,outputconstr) in add_morphism lemma_infos mor_name diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c496ffe64..defb7b749 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2524,7 +2524,7 @@ let admit_as_an_axiom gls = let concl = it_mkNamedProd_or_LetIn (pf_concl gls) sign in if occur_existential concl then error "\"admit\" cannot handle existentials"; let axiom = - let cd = Entries.ParameterEntry concl in + let cd = Entries.ParameterEntry (concl,false) in let con = Declare.declare_internal_constant na (cd,IsAssumption Logical) in constr_of_global (ConstRef con) in diff --git a/toplevel/command.ml b/toplevel/command.ml index f73fe5e9c..f0a9792fd 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -161,7 +161,7 @@ let syntax_definition ident c local onlyparse = let assumption_message id = if_verbose message ((string_of_id id) ^ " is assumed") -let declare_one_assumption is_coe (local,kind) c (_,ident) = +let declare_one_assumption is_coe (local,kind) c nl (_,ident) = let r = match local with | Local when Lib.sections_are_opened () -> let _ = @@ -174,7 +174,7 @@ let declare_one_assumption is_coe (local,kind) c (_,ident) = VarRef ident | (Global|Local) -> let kn = - declare_constant ident (ParameterEntry c, IsAssumption kind) in + declare_constant ident (ParameterEntry (c,nl), IsAssumption kind) in assumption_message ident; if local=Local & Options.is_verbose () then msg_warning (pr_id ident ++ str" is declared as a parameter" ++ @@ -182,11 +182,11 @@ let declare_one_assumption is_coe (local,kind) c (_,ident) = ConstRef kn in if is_coe then Class.try_add_new_coercion r local -let declare_assumption idl is_coe k bl c = +let declare_assumption idl is_coe k bl c nl= if not (Pfedit.refining ()) then let c = generalize_constr_expr c bl in let c = interp_type Evd.empty (Global.env()) c in - List.iter (declare_one_assumption is_coe k c) idl + List.iter (declare_one_assumption is_coe k c nl) idl else errorlabstrm "Command.Assumption" (str "Cannot declare an assumption while in proof editing mode.") @@ -799,7 +799,7 @@ let admit () = error "Only statements declared as conjecture can be admitted"; *) let kn = - declare_constant id (ParameterEntry typ, IsAssumption Conjectural) in + declare_constant id (ParameterEntry (typ,false), IsAssumption Conjectural) in Pfedit.delete_current_proof (); assumption_message id; hook Global (ConstRef kn) diff --git a/toplevel/command.mli b/toplevel/command.mli index 4fae32805..cf05f691b 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -36,11 +36,12 @@ val declare_definition : identifier -> definition_kind -> val syntax_definition : identifier -> constr_expr -> bool -> bool -> unit -val declare_one_assumption : coercion_flag -> assumption_kind -> Term.types -> - Names.variable located -> unit +val declare_one_assumption : coercion_flag -> assumption_kind -> Term.types -> bool + -> Names.variable located -> unit val declare_assumption : identifier located list -> - coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> unit + coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> bool + ->unit val build_mutual : (inductive_expr * decl_notation) list -> bool -> unit diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 7dacbeaba..4c0fb5046 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -348,8 +348,8 @@ let vernac_exact_proof c = errorlabstrm "Vernacentries.ExactProof" (str "Command 'Proof ...' can only be used at the beginning of the proof") -let vernac_assumption kind l = - List.iter (fun (is_coe,(idl,c)) -> declare_assumption idl is_coe kind [] c) l +let vernac_assumption kind l nl= + List.iter (fun (is_coe,(idl,c)) -> declare_assumption idl is_coe kind [] c nl) l let vernac_inductive f indl = build_mutual indl f @@ -1134,7 +1134,7 @@ let interp c = match c with vernac_start_proof k (Some id) t top f | VernacEndProof e -> vernac_end_proof e | VernacExactProof c -> vernac_exact_proof c - | VernacAssumption (stre,l) -> vernac_assumption stre l + | VernacAssumption (stre,nl,l) -> vernac_assumption stre l nl | VernacInductive (finite,l) -> vernac_inductive finite l | VernacFixpoint (l,b) -> vernac_fixpoint l b | VernacCoFixpoint (l,b) -> vernac_cofixpoint l b diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index cd0fb899c..042ef1e85 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -194,7 +194,7 @@ type vernac_expr = (local_binder list * constr_expr) * bool * declaration_hook | VernacEndProof of proof_end | VernacExactProof of constr_expr - | VernacAssumption of assumption_kind * simple_binder with_coercion list + | VernacAssumption of assumption_kind * bool * simple_binder with_coercion list | VernacInductive of inductive_flag * (inductive_expr * decl_notation) list | VernacFixpoint of (fixpoint_expr * decl_notation) list * bool | VernacCoFixpoint of (cofixpoint_expr * decl_notation) list * bool |