diff options
-rw-r--r-- | CHANGES | 1 | ||||
-rw-r--r-- | contrib/interface/name_to_ast.ml | 4 | ||||
-rw-r--r-- | contrib/interface/xlate.ml | 5 | ||||
-rw-r--r-- | parsing/g_vernac.ml4 | 12 | ||||
-rw-r--r-- | toplevel/command.ml | 17 | ||||
-rw-r--r-- | toplevel/command.mli | 22 | ||||
-rw-r--r-- | toplevel/record.ml | 2 | ||||
-rw-r--r-- | toplevel/record.mli | 5 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 13 | ||||
-rw-r--r-- | toplevel/vernacexpr.ml | 15 |
10 files changed, 46 insertions, 50 deletions
@@ -5,6 +5,7 @@ Language - Inductive definitions now accept ">" in constructor types to declare the corresponding constructor as a coercion. +- Idem for assumptions declarations and constants when the type is mentionned. ML tactic and vernacular commands diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml index 0f3dcdf67..5ba5e0e7e 100644 --- a/contrib/interface/name_to_ast.ml +++ b/contrib/interface/name_to_ast.ml @@ -97,7 +97,7 @@ let convert_constructors envpar names types = array_map2 (fun n t -> let coercion_flag = false (* arbitrary *) in - (n, coercion_flag, ast_of_constr true envpar t)) + (coercion_flag, (n, ast_of_constr true envpar t))) names types in Array.to_list array_idC;; @@ -146,7 +146,7 @@ let make_variable_ast name typ implicits = *) let make_variable_ast name typ implicits = (VernacAssumption - (AssumptionVariable, [name, constr_to_ast (body_of_type typ)])) + (AssumptionVariable, [false,(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 2e49ec4e3..233af4f7d 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -2290,7 +2290,7 @@ let xlate_check = | _ -> xlate_error "xlate_check";; let build_constructors l = - let f (id,coe,c) = + let f (coe,(id,c)) = if coe then xlate_error "TODO: coercions in constructors" else CT_constr (xlate_ident id, xlate_constr c) in CT_constr_list (List.map f l) @@ -2912,6 +2912,7 @@ let xlate_vernac = CT_variable (xlate_var kind, b) *) | VernacAssumption (kind, b) -> + let b = List.map snd b in (* TODO: handle possible coercions *) CT_variable (xlate_var kind, cvt_vernac_binders b) (* | "Check", ((Varg_string (CT_string kind)) :: (c :: [])) -> @@ -2980,7 +2981,7 @@ let xlate_vernac = *) | (*Record from tactics/Record.v *) VernacRecord - (add_coercion, s, binders, c1, rec_constructor_or_none, field_list) -> + ((add_coercion, s), binders, c1, rec_constructor_or_none, field_list) -> let record_constructor = xlate_ident_opt rec_constructor_or_none in (* match rec_constructor_or_none with | None -> CT_coerce_NONE_to_ID_OPT CT_none diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index caa3b7916..86e7629aa 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -125,8 +125,14 @@ GEXTEND Gram | IDENT "Variables" -> AssumptionVariable | IDENT "Parameters" -> AssumptionParameter ] ] ; + of_type_with_opt_coercion: + [ [ ":>" -> true + | ":"; ">" -> true + | ":" -> false ] ] + ; params: - [ [ idl = LIST1 ident SEP ","; ":"; c = constr -> join_binders (idl,c) + [ [ idl = LIST1 ident SEP ","; coe = of_type_with_opt_coercion; c = constr + -> List.map (fun c -> (coe,c)) (join_binders (idl,c)) ] ] ; ne_params_list: @@ -186,7 +192,7 @@ GEXTEND Gram ; constructor: [ [ id = ident; coe = of_type_with_opt_coercion; c = constr -> - (id,coe,c) ] ] + (coe,(id,c)) ] ] ; ne_constructor_list: [ [ idc = constructor; "|"; l = ne_constructor_list -> idc :: l @@ -285,7 +291,7 @@ GEXTEND Gram VernacInductive (f,indl') | record_token; oc = opt_coercion; name = ident; ps = indpar; ":"; s = sort; ":="; c = rec_constructor; "{"; fs = fields; "}" -> - VernacRecord (oc,name,ps,s,c,fs) + VernacRecord ((oc,name),ps,s,c,fs) ] ] ; gallina: diff --git a/toplevel/command.ml b/toplevel/command.ml index 234910af0..c6a038c3b 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -83,7 +83,7 @@ let declare_definition red_option ident (local,n) c typopt = | DischargeAt (disch_sp,_) -> if Lib.is_section_p disch_sp then begin let c = SectionLocalDef(ce'.const_entry_body,ce'.const_entry_type) in - let sp = declare_variable ident (Lib.cwd(), c, n) in + let _ = declare_variable ident (Lib.cwd(), c, n) in if_verbose message ((string_of_id ident) ^ " is defined"); if Pfedit.refining () then msgerrnl (str"Warning: Local definition " ++ pr_id ident ++ @@ -110,22 +110,25 @@ let declare_assumption ident n c = let c = interp_type Evd.empty (Global.env()) c in match n with | NeverDischarge -> - let _ = declare_constant ident (ParameterEntry c, NeverDischarge) in - assumption_message ident + let r = declare_constant ident (ParameterEntry c, NeverDischarge) in + assumption_message ident; + ConstRef r | DischargeAt (disch_sp,_) -> if Lib.is_section_p disch_sp then begin - let _ = declare_variable ident (Lib.cwd(),SectionLocalAssum c,n) in + let r = declare_variable ident (Lib.cwd(),SectionLocalAssum c,n) in assumption_message ident; if is_verbose () & Pfedit.refining () then msgerrnl (str"Warning: Variable " ++ pr_id ident ++ - str" is not visible from current goals") + str" is not visible from current goals"); + VarRef ident end else - let _ = declare_constant ident (ParameterEntry c, NeverDischarge) in + let r = declare_constant ident (ParameterEntry c, NeverDischarge) in assumption_message ident; if_verbose msg_warning (pr_id ident ++ str" is declared as a parameter" ++ str" because it is at a global level"); + ConstRef r | NotDeclare -> anomalylabstrm "Command.hypothesis_def_var" (str "Strength NotDeclare not for Variable, only for Let") @@ -220,7 +223,7 @@ let eq_la (id,ast) (id',ast') = id = id' & alpha_eq(ast,ast') let extract_coe lc = List.fold_right - (fun (id,addcoe,t) (l1,l2) -> + (fun (addcoe,(id,t)) (l1,l2) -> ((if addcoe then id::l1 else l1), (id,t)::l2)) lc ([],[]) let extract_coe_la_lc = function diff --git a/toplevel/command.mli b/toplevel/command.mli index 474fe9202..ea6c97e0e 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -21,32 +21,12 @@ open Library functions of [Declare]; they return an absolute reference to the defined object *) -(*i -val constant_entry_of_com : - Coqast.t * Coqast.t option * bool -> Safe_typing.constant_entry - -val declare_global_definition : - Names.identifier -> - Safe_typing.constant_entry -> - Declare.strength -> bool -> Nametab.global_reference - -val definition_body : identifier -> bool * strength -> - Coqast.t -> Coqast.t option -> global_reference -i*) - val declare_definition : Tacred.red_expr option -> identifier -> bool * strength -> Coqast.t -> Coqast.t option -> global_reference val syntax_definition : identifier -> Coqast.t -> unit -(*i -val hypothesis_def_var : bool -> identifier -> strength -> Coqast.t - -> global_reference - -val parameter_def_var : identifier -> Coqast.t -> constant -i*) - -val declare_assumption : identifier -> strength -> Coqast.t -> unit +val declare_assumption : identifier -> strength -> Coqast.t -> global_reference val build_mutual : Vernacexpr.inductive_expr list -> bool -> unit diff --git a/toplevel/record.ml b/toplevel/record.ml index c7907b167..10b9c42da 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -209,7 +209,7 @@ let declare_projections indsp coers fields = (* [fs] corresponds to fields and [ps] to parameters; [coers] is a boolean list telling if the corresponding fields must me declared as coercion *) -let definition_structure (is_coe,idstruc,ps,cfs,idbuild,s) = +let definition_structure ((is_coe,idstruc),ps,cfs,idbuild,s) = let coers,fs = List.split cfs in let nparams = List.length ps in let idps = List.map fst ps in diff --git a/toplevel/record.mli b/toplevel/record.mli index 1419b9c3c..90b40020e 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -12,6 +12,7 @@ open Names open Term open Sign +open Vernacexpr (*i*) (* [declare_projections ref coers params fields] declare projections of @@ -22,5 +23,5 @@ val declare_projections : inductive -> bool list -> rel_context -> constant option list val definition_structure : - bool * identifier * (identifier * Genarg.constr_ast) list * - (bool * Vernacexpr.local_decl_expr) list * identifier * sorts -> unit + identifier with_coercion * (identifier * Genarg.constr_ast) list * + (local_decl_expr with_coercion) list * identifier * sorts -> unit diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 8d8de77b9..9c11ae7cb 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -307,7 +307,10 @@ let vernac_exact_proof c = let vernac_assumption kind l = let stre = interp_assumption kind in - List.iter (fun (id,c) -> declare_assumption id stre c) l + List.iter + (fun (is_coe,(id,c)) -> + let r = declare_assumption id stre c in + if is_coe then Class.try_add_new_coercion r stre) l let vernac_inductive f indl = build_mutual indl f @@ -321,12 +324,12 @@ let vernac_scheme = build_scheme (**********************) (* Gallina extensions *) -let vernac_record iscoe struc binders sort nameopt cfs = +let vernac_record struc binders sort nameopt cfs = let const = match nameopt with - | None -> add_prefix "Build_" struc + | None -> add_prefix "Build_" (snd struc) | Some id -> id in let s = Astterm.interp_sort sort in - Record.definition_structure (iscoe,struc,binders,cfs,const,s) + Record.definition_structure (struc,binders,cfs,const,s) (* Sections *) @@ -876,7 +879,7 @@ let interp c = match c with | VernacScheme l -> vernac_scheme l (* Gallina extensions *) - | VernacRecord (coe,id,bl,s,idopt,fs) -> vernac_record coe id bl s idopt fs + | VernacRecord (id,bl,s,idopt,fs) -> vernac_record id bl s idopt fs | VernacBeginSection id -> vernac_begin_section id | VernacEndSection id -> vernac_end_section id | VernacRequire (export,spec,qidl) -> vernac_require export spec qidl diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 365192599..f1bd6ed52 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -140,12 +140,13 @@ type inductive_flag = bool (* true = Inductive; false = CoInductive *) type sort_expr = t -type simple_binders = identifier * constr_ast -type constructor_expr = identifier * coercion_flag * constr_ast +type simple_binder = identifier * constr_ast +type 'a with_coercion = coercion_flag * 'a +type constructor_expr = simple_binder with_coercion type inductive_expr = - identifier * simple_binders list * constr_ast * constructor_expr list + identifier * simple_binder list * constr_ast * constructor_expr list type fixpoint_expr = - identifier * simple_binders list * constr_ast * constr_ast + identifier * simple_binder list * constr_ast * constr_ast type cofixpoint_expr = identifier * constr_ast * constr_ast @@ -180,15 +181,15 @@ type vernac_expr = constr_ast * bool * Proof_type.declaration_hook | VernacEndProof of opacity_flag * (identifier * theorem_kind option) option | VernacExactProof of constr_ast - | VernacAssumption of assumption_kind * simple_binders list + | VernacAssumption of assumption_kind * simple_binder with_coercion list | VernacInductive of inductive_flag * inductive_expr list | VernacFixpoint of fixpoint_expr list | VernacCoFixpoint of cofixpoint_expr list | VernacScheme of (identifier * bool * qualid located * sort_expr) list (* Gallina extensions *) - | VernacRecord of coercion_flag * identifier * simple_binders list - * sort_expr * identifier option * (coercion_flag * local_decl_expr) list + | VernacRecord of identifier with_coercion * simple_binder list + * sort_expr * identifier option * local_decl_expr with_coercion list | VernacBeginSection of identifier | VernacEndSection of identifier | VernacRequire of |