diff options
67 files changed, 2281 insertions, 326 deletions
diff --git a/.gitignore b/.gitignore index 56e1905981..4116190801 100644 --- a/.gitignore +++ b/.gitignore @@ -129,6 +129,7 @@ ltac/extratactics.ml ltac/extraargs.ml ltac/profile_ltac_tactics.ml ide/coqide_main.ml +plugins/ssrmatching/ssrmatching.ml # other auto-generated files @@ -34,6 +34,8 @@ Notations Tools - coqc accepts a -o option to specify the output file name +- coqtop accepts --print-version to print Coq and OCaml versions in + easy to parse format Changes from V8.5pl1 to V8.5pl2 =============================== @@ -9,6 +9,7 @@ This product includes also software developed by Claudio Sacerdoti Coen, HELM, University of Bologna, (plugins/xml) Pierre Corbineau, Radboud University, Nijmegen (declarative mode) John Harrison, University of Cambridge (csdp wrapper) + Georges Gonthier, Microsoft Research - Inria Joint Centre (plugins/ssrmatching) The file CREDITS contains a list of contributors. The credits section in the Reference Manual details contributions. @@ -54,6 +54,9 @@ plugins/setoid_ring developed by Benjamin Grégoire (INRIA-Everest, 2005-2006), Assia Mahboubi, Laurent Théry (INRIA-Marelle, 2006) and Bruno Barras (INRIA LogiCal, 2005-2006), +plugins/ssrmatching + developed by Georges Gonthier (Microsoft Research - Inria Joint Centre, 2007-2011), + and Enrico Tassi (Inria-Marelle, 2011-now) plugins/subtac developed by Matthieu Sozeau (LRI, 2005-2008) plugins/micromega diff --git a/Makefile.common b/Makefile.common index 4742bb51e8..e156b101ca 100644 --- a/Makefile.common +++ b/Makefile.common @@ -61,7 +61,8 @@ PLUGINS:=\ omega romega micromega quote \ setoid_ring extraction fourier \ cc funind firstorder derive \ - rtauto nsatz syntax decl_mode btauto + rtauto nsatz syntax decl_mode btauto \ + ssrmatching SRCDIRS:=\ $(CORESRCDIRS) \ @@ -119,13 +120,14 @@ OTHERSYNTAXCMA:=$(addprefix plugins/syntax/, \ string_syntax_plugin.cmo ) DECLMODECMA:=plugins/decl_mode/decl_mode_plugin.cmo DERIVECMA:=plugins/derive/derive_plugin.cmo +SSRMATCHINGCMA:=plugins/ssrmatching/ssrmatching_plugin.cmo PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) $(DECLMODECMA) \ $(QUOTECMA) $(RINGCMA) \ $(FOURIERCMA) $(EXTRACTIONCMA) \ $(CCCMA) $(FOCMA) $(RTAUTOCMA) $(BTAUTOCMA) \ $(FUNINDCMA) $(NSATZCMA) $(NATSYNTAXCMA) $(OTHERSYNTAXCMA) \ - $(DERIVECMA) + $(DERIVECMA) $(SSRMATCHINGCMA) ifneq ($(HASNATDYNLINK),false) STATICPLUGINS:= diff --git a/checker/cic.mli b/checker/cic.mli index 00ac2f56c3..469cf8d4c8 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -212,6 +212,15 @@ type constant_def = type constant_universes = Univ.universe_context +(** The [typing_flags] are instructions to the type-checker which + modify its behaviour. The typing flags used in the type-checking + of a constant are tracked in their {!constant_body} so that they + can be displayed to the user. *) +type typing_flags = { + check_guarded : bool; (** If [false] then fixed points and co-fixed + points are assumed to be total. *) +} + type constant_body = { const_hyps : section_context; (** New: younger hyp at top *) const_body : constant_def; @@ -220,7 +229,9 @@ type constant_body = { const_polymorphic : bool; (** Is it polymorphic or not *) const_universes : constant_universes; const_proj : projection_body option; - const_inline_code : bool } + const_inline_code : bool; + const_typing_flags : typing_flags; +} (** {6 Representation of mutual inductive types } *) @@ -316,6 +327,8 @@ type mutual_inductive_body = { mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) + mind_checked_positive : bool; (** [false] when the mutual-inductive was assumed to be well-founded, bypassing the positivity checker. *) + (** {8 Data for native compilation } *) mind_native_name : native_name ref; (** status of the code (linked or not, and where) *) diff --git a/checker/values.ml b/checker/values.ml index 19cbb50606..dd29f6fbe0 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -13,7 +13,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 9f7fd499f812b6548a55f7067e6a9d06 checker/cic.mli +MD5 7d7963269852d32324e10aa77beb938d checker/cic.mli *) @@ -213,6 +213,9 @@ let v_projbody = v_tuple "proj_eta" [|v_constr;v_constr|]; v_constr|] +let v_typing_flags = + v_tuple "typing_flags" [|v_bool|] + let v_cb = v_tuple "constant_body" [|v_section_ctxt; v_cst_def; @@ -221,7 +224,8 @@ let v_cb = v_tuple "constant_body" v_bool; v_context; Opt v_projbody; - v_bool|] + v_bool; + v_typing_flags|] let v_recarg = v_sum "recarg" 1 (* Norec *) [|[|v_ind|] (* Mrec *);[|v_ind|] (* Imbr *)|] @@ -270,7 +274,8 @@ let v_ind_pack = v_tuple "mutual_inductive_body" v_rctxt; v_bool; v_context; - Opt v_bool|] + Opt v_bool; + v_bool|] let v_with = Sum ("with_declaration_body",0, diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 79affb36f5..9f10b2502a 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -1,4 +1,5 @@ (************************************************************************) + (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) @@ -47,6 +48,7 @@ let init_stdout, read_stdout = let pr_with_pid s = Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) s +let pr_error s = pr_with_pid s let pr_debug s = if !Flags.debug then pr_with_pid s let pr_debug_call q = @@ -517,11 +519,11 @@ let loop () = pr_debug "End of input, exiting gracefully."; exit 0 | Xml_parser.Error (err, loc) -> - pr_debug ("Syntax error in query: " ^ Xml_parser.error_msg err); - exit 1 - | Serialize.Marshal_error _ -> - pr_debug "Incorrect query."; - exit 1 + pr_error ("XML syntax error: " ^ Xml_parser.error_msg err) + | Serialize.Marshal_error (msg,node) -> + pr_error "Unexpected XML message"; + pr_error ("Expected XML node: " ^ msg); + pr_error ("XML tree received: " ^ Xml_printer.to_string_fmt node) | any -> pr_debug ("Fatal exception in coqtop:\n" ^ Printexc.to_string any); exit 1 diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml index d1d6de9ae8..f445f2e08d 100644 --- a/ide/texmacspp.ml +++ b/ide/texmacspp.ml @@ -188,6 +188,7 @@ match sm with | LeftA -> ["associativity", "left"] end | SetEntryType (s, _) -> ["entrytype", s] + | SetOnlyPrinting -> ["onlyprinting", ""] | SetOnlyParsing v -> ["compat", Flags.pr_version v] | SetFormat (system, (loc, s)) -> let start, stop = unlock loc in diff --git a/interp/notation.ml b/interp/notation.ml index b19fd9e1fe..7ad104d036 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -967,23 +967,27 @@ let pr_visibility prglob = function type unparsing_rule = unparsing list * precedence type extra_unparsing_rules = (string * string) list (* Concrete syntax for symbolic-extension table *) -let printing_rules = - ref (String.Map.empty : (unparsing_rule * extra_unparsing_rules) String.Map.t) +let notation_rules = + ref (String.Map.empty : (unparsing_rule * extra_unparsing_rules * notation_grammar) String.Map.t) -let declare_notation_printing_rule ntn ~extra unpl = - printing_rules := String.Map.add ntn (unpl,extra) !printing_rules +let declare_notation_rule ntn ~extra unpl gram = + notation_rules := String.Map.add ntn (unpl,extra,gram) !notation_rules let find_notation_printing_rule ntn = - try fst (String.Map.find ntn !printing_rules) + try pi1 (String.Map.find ntn !notation_rules) with Not_found -> anomaly (str "No printing rule found for " ++ str ntn) let find_notation_extra_printing_rules ntn = - try snd (String.Map.find ntn !printing_rules) + try pi2 (String.Map.find ntn !notation_rules) with Not_found -> [] +let find_notation_parsing_rules ntn = + try pi3 (String.Map.find ntn !notation_rules) + with Not_found -> anomaly (str "No parsing rule found for " ++ str ntn) + let add_notation_extra_printing_rule ntn k v = try - printing_rules := - let p, pp = String.Map.find ntn !printing_rules in - String.Map.add ntn (p, (k,v) :: pp) !printing_rules + notation_rules := + let p, pp, gr = String.Map.find ntn !notation_rules in + String.Map.add ntn (p, (k,v) :: pp, gr) !notation_rules with Not_found -> user_err_loc (Loc.ghost,"add_notation_extra_printing_rule", str "No such Notation.") @@ -993,7 +997,7 @@ let add_notation_extra_printing_rule ntn k v = let freeze _ = (!scope_map, !notation_level_map, !scope_stack, !arguments_scope, - !delimiters_map, !notations_key_table, !printing_rules, + !delimiters_map, !notations_key_table, !notation_rules, !scope_class_map) let unfreeze (scm,nlm,scs,asc,dlm,fkm,pprules,clsc) = @@ -1003,7 +1007,7 @@ let unfreeze (scm,nlm,scs,asc,dlm,fkm,pprules,clsc) = delimiters_map := dlm; arguments_scope := asc; notations_key_table := fkm; - printing_rules := pprules; + notation_rules := pprules; scope_class_map := clsc let init () = @@ -1011,7 +1015,7 @@ let init () = notation_level_map := String.Map.empty; delimiters_map := String.Map.empty; notations_key_table := KeyMap.empty; - printing_rules := String.Map.empty; + notation_rules := String.Map.empty; scope_class_map := initial_scope_class_map let _ = diff --git a/interp/notation.mli b/interp/notation.mli index 480979ccc3..a85dc50f2f 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -196,10 +196,11 @@ val pr_visibility: (glob_constr -> std_ppcmds) -> scope_name option -> std_ppcmd (** Declare and look for the printing rule for symbolic notations *) type unparsing_rule = unparsing list * precedence type extra_unparsing_rules = (string * string) list -val declare_notation_printing_rule : - notation -> extra:extra_unparsing_rules -> unparsing_rule -> unit +val declare_notation_rule : + notation -> extra:extra_unparsing_rules -> unparsing_rule -> notation_grammar -> unit val find_notation_printing_rule : notation -> unparsing_rule val find_notation_extra_printing_rules : notation -> extra_unparsing_rules +val find_notation_parsing_rules : notation -> notation_grammar val add_notation_extra_printing_rule : notation -> string -> string -> unit (** Rem: printing rules for primitive token are canonical *) diff --git a/intf/notation_term.mli b/intf/notation_term.mli index 7c5d7657be..883b017727 100644 --- a/intf/notation_term.mli +++ b/intf/notation_term.mli @@ -78,3 +78,19 @@ type notation_interp_env = { ninterp_rec_vars : Id.t Id.Map.t; mutable ninterp_only_parse : bool; } + +type grammar_constr_prod_item = + | GramConstrTerminal of Tok.t + | GramConstrNonTerminal of Extend.constr_prod_entry_key * Id.t option + | GramConstrListMark of int * bool + (* tells action rule to make a list of the n previous parsed items; + concat with last parsed list if true *) + +type notation_grammar = { + notgram_level : int; + notgram_assoc : Extend.gram_assoc option; + notgram_notation : Constrexpr.notation; + notgram_prods : grammar_constr_prod_item list list; + notgram_typs : notation_var_internalization_type list; + notgram_onlyprinting : bool; +} diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 6ce15a7c5a..cfa30a4d54 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -206,6 +206,7 @@ type syntax_modifier = | SetAssoc of Extend.gram_assoc | SetEntryType of string * Extend.simple_constr_prod_entry_key | SetOnlyParsing of Flags.compat_version + | SetOnlyPrinting | SetFormat of string * string located type proof_end = diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 1b77d5b7cb..8b42a90e48 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -66,6 +66,15 @@ type constant_def = type constant_universes = Univ.universe_context +(** The [typing_flags] are instructions to the type-checker which + modify its behaviour. The typing flags used in the type-checking + of a constant are tracked in their {!constant_body} so that they + can be displayed to the user. *) +type typing_flags = { + check_guarded : bool; (** If [false] then fixed points and co-fixed + points are assumed to be total. *) +} + (* some contraints are in constant_constraints, some other may be in * the OpaueDef *) type constant_body = { @@ -76,7 +85,11 @@ type constant_body = { const_polymorphic : bool; (** Is it polymorphic or not *) const_universes : constant_universes; const_proj : projection_body option; - const_inline_code : bool } + const_inline_code : bool; + const_typing_flags : typing_flags; (** The typing options which + were used for + type-checking. *) +} (** {6 Representation of mutual inductive types in the kernel } *) @@ -178,6 +191,7 @@ type mutual_inductive_body = { mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) + mind_checked_positive : bool; (** [false] when the mutual-inductive was assumed to be well-founded, bypassing the positivity checker. *) } (** {6 Module declarations } *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index a09a8b7862..78e2f386e6 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -131,7 +131,8 @@ let subst_const_body sub cb = Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code; const_polymorphic = cb.const_polymorphic; const_universes = cb.const_universes; - const_inline_code = cb.const_inline_code } + const_inline_code = cb.const_inline_code; + const_typing_flags = cb.const_typing_flags } (** {7 Hash-consing of constants } *) @@ -254,7 +255,9 @@ let subst_mind_body sub mib = mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ; mind_polymorphic = mib.mind_polymorphic; mind_universes = mib.mind_universes; - mind_private = mib.mind_private } + mind_private = mib.mind_private; + mind_checked_positive = mib.mind_checked_positive; + } let inductive_instance mib = if mib.mind_polymorphic then diff --git a/kernel/entries.mli b/kernel/entries.mli index d07ca2103f..8b29e3abd7 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -51,7 +51,10 @@ type mutual_inductive_entry = { mind_entry_inds : one_inductive_entry list; mind_entry_polymorphic : bool; mind_entry_universes : Univ.universe_context; - mind_entry_private : bool option } + mind_entry_private : bool option; + mind_entry_check_positivity : bool; + (** [false] if positivity is to be assumed. *) +} (** {6 Constants (Definition/Axiom) } *) type 'a proof_output = constr Univ.in_universe_context_set * 'a diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml index 7f4ba8ecbe..35c162cf3b 100644 --- a/kernel/fast_typeops.ml +++ b/kernel/fast_typeops.ml @@ -327,7 +327,7 @@ let type_fixpoint env lna lar vdef vdeft = (* ATTENTION : faudra faire le typage du contexte des Const, Ind et Constructsi un jour cela devient des constructions arbitraires et non plus des variables *) -let rec execute env cstr = +let rec execute ~flags env cstr = let open Context.Rel.Declaration in match kind_of_term cstr with (* Atomic terms *) @@ -347,12 +347,12 @@ let rec execute env cstr = judge_of_constant env c | Proj (p, c) -> - let ct = execute env c in + let ct = execute ~flags env c in judge_of_projection env p c ct (* Lambda calculus operators *) | App (f,args) -> - let argst = execute_array env args in + let argst = execute_array ~flags env args in let ft = match kind_of_term f with | Ind ind when Environ.template_polymorphic_pind ind env -> @@ -365,7 +365,7 @@ let rec execute env cstr = judge_of_constant_knowing_parameters env cst args | _ -> (* Full or no sort-polymorphism *) - execute env f + execute ~flags env f in judge_of_apply env f ft args argst @@ -373,25 +373,25 @@ let rec execute env cstr = | Lambda (name,c1,c2) -> let _ = execute_is_type env c1 in let env1 = push_rel (LocalAssum (name,c1)) env in - let c2t = execute env1 c2 in + let c2t = execute ~flags env1 c2 in judge_of_abstraction env name c1 c2t | Prod (name,c1,c2) -> - let vars = execute_is_type env c1 in + let vars = execute_is_type ~flags env c1 in let env1 = push_rel (LocalAssum (name,c1)) env in - let vars' = execute_is_type env1 c2 in + let vars' = execute_is_type ~flags env1 c2 in judge_of_product env name vars vars' | LetIn (name,c1,c2,c3) -> - let c1t = execute env c1 in + let c1t = execute ~flags env c1 in let _c2s = execute_is_type env c2 in let _ = judge_of_cast env c1 c1t DEFAULTcast c2 in let env1 = push_rel (LocalDef (name,c1,c2)) env in - let c3t = execute env1 c3 in + let c3t = execute ~flags env1 c3 in subst1 c1 c3t | Cast (c,k,t) -> - let ct = execute env c in + let ct = execute ~flags env c in let _ts = execute_type env t in let _ = judge_of_cast env c ct k t in t @@ -404,20 +404,20 @@ let rec execute env cstr = judge_of_constructor env c | Case (ci,p,c,lf) -> - let ct = execute env c in - let pt = execute env p in - let lft = execute_array env lf in + let ct = execute ~flags env c in + let pt = execute ~flags env p in + let lft = execute_array ~flags env lf in judge_of_case env ci p pt c ct lf lft | Fix ((vn,i as vni),recdef) -> - let (fix_ty,recdef') = execute_recdef env recdef i in + let (fix_ty,recdef') = execute_recdef ~flags env recdef i in let fix = (vni,recdef') in - check_fix env fix; fix_ty + check_fix env ~flags fix; fix_ty | CoFix (i,recdef) -> - let (fix_ty,recdef') = execute_recdef env recdef i in + let (fix_ty,recdef') = execute_recdef ~flags env recdef i in let cofix = (i,recdef') in - check_cofix env cofix; fix_ty + check_cofix env ~flags cofix; fix_ty (* Partial proofs: unsupported by the kernel *) | Meta _ -> @@ -426,38 +426,41 @@ let rec execute env cstr = | Evar _ -> anomaly (Pp.str "the kernel does not support existential variables") -and execute_is_type env constr = - let t = execute env constr in +and execute_is_type ~flags env constr = + let t = execute ~flags env constr in check_type env constr t -and execute_type env constr = - let t = execute env constr in +and execute_type ~flags env constr = + let t = execute ~flags env constr in type_judgment env constr t -and execute_recdef env (names,lar,vdef) i = - let lart = execute_array env lar in +and execute_recdef ~flags env (names,lar,vdef) i = + let lart = execute_array ~flags env lar in let lara = Array.map2 (assumption_of_judgment env) lar lart in let env1 = push_rec_types (names,lara,vdef) env in - let vdeft = execute_array env1 vdef in + let vdeft = execute_array ~flags env1 vdef in let () = type_fixpoint env1 names lara vdef vdeft in (lara.(i),(names,lara,vdef)) -and execute_array env = Array.map (execute env) +and execute_array ~flags env = Array.map (execute ~flags env) (* Derived functions *) -let infer env constr = - let t = execute env constr in +let infer ~flags env constr = + let t = execute ~flags env constr in make_judge constr t let infer = if Flags.profile then let infer_key = Profile.declare_profile "Fast_infer" in - Profile.profile2 infer_key infer - else infer + Profile.profile3 infer_key (fun a b c -> infer ~flags:a b c) + else (fun a b c -> infer ~flags:a b c) -let infer_type env constr = - execute_type env constr +(* Restores the labels of [infer] lost to profiling. *) +let infer ~flags env t = infer flags env t -let infer_v env cv = - let jv = execute_array env cv in +let infer_type ~flags env constr = + execute_type ~flags env constr + +let infer_v ~flags env cv = + let jv = execute_array ~flags env cv in make_judgev cv jv diff --git a/kernel/fast_typeops.mli b/kernel/fast_typeops.mli index 05d52b2d3c..45a6030384 100644 --- a/kernel/fast_typeops.mli +++ b/kernel/fast_typeops.mli @@ -8,6 +8,7 @@ open Term open Environ +open Declarations (** {6 Typing functions (not yet tagged as safe) } @@ -18,6 +19,6 @@ open Environ *) -val infer : env -> constr -> unsafe_judgment -val infer_v : env -> constr array -> unsafe_judgment array -val infer_type : env -> types -> unsafe_type_judgment +val infer : flags:typing_flags -> env -> constr -> unsafe_judgment +val infer_v : flags:typing_flags -> env -> constr array -> unsafe_judgment array +val infer_type : flags:typing_flags -> env -> types -> unsafe_type_judgment diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index edb758f078..b74788d217 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -483,8 +483,12 @@ let array_min nmr a = if Int.equal nmr 0 then 0 else for use by the guard condition (terms at these positions are considered sub-terms) as well as the number of of non-uniform arguments (used to generate induction schemes, so a priori less - relevant to the kernel). *) -let check_positivity_one recursive (env,_,ntypes,_ as ienv) paramsctxt (_,i as ind) nnonrecargs lcnames indlc = + relevant to the kernel). + + If [chkpos] is [false] then positivity is assumed, and + [check_positivity_one] computes the subterms occurrences in a + best-effort fashion. *) +let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt (_,i as ind) nnonrecargs lcnames indlc = let nparamsctxt = Context.Rel.length paramsctxt in let nmr = Context.Rel.nhyps paramsctxt in (** Positivity of one argument [c] of a constructor (i.e. the @@ -501,9 +505,12 @@ let check_positivity_one recursive (env,_,ntypes,_ as ienv) paramsctxt (_,i as i recursive call. Occurrences in the right-hand side of the product must be strictly positive.*) (match weaker_noccur_between env n ntypes b with - None -> failwith_non_pos_list n ntypes [b] + | None when chkpos -> + failwith_non_pos_list n ntypes [b] + | None -> + check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d | Some b -> - check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d) + check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d) | Rel k -> (try let (ra,rarg) = List.nth ra_env (k-1) in let largs = List.map (whd_betadeltaiota env) largs in @@ -515,7 +522,8 @@ let check_positivity_one recursive (env,_,ntypes,_ as ienv) paramsctxt (_,i as i (** The case where one of the inductives of the mutually inductive block occurs as an argument of another is not known to be safe. So Coq rejects it. *) - if not (List.for_all (noccur_between n ntypes) largs) + if chkpos && + not (List.for_all (noccur_between n ntypes) largs) then failwith_non_pos_list n ntypes largs else (nmr1,rarg) with Failure _ | Invalid_argument _ -> (nmr,mk_norec)) @@ -530,8 +538,9 @@ let check_positivity_one recursive (env,_,ntypes,_ as ienv) paramsctxt (_,i as i (** If an inductive of the mutually inductive block appears in any other way, then the positivy check gives up. *) - if noccur_between n ntypes x && - List.for_all (noccur_between n ntypes) largs + if not chkpos || + (noccur_between n ntypes x && + List.for_all (noccur_between n ntypes) largs) then (nmr,mk_norec) else failwith_non_pos_list n ntypes (x::largs) @@ -553,7 +562,7 @@ let check_positivity_one recursive (env,_,ntypes,_ as ienv) paramsctxt (_,i as i (** Inductives of the inductive block being defined are only allowed to appear nested in the parameters of another inductive type. Not in the proper indices. *) - if not (List.for_all (noccur_between n ntypes) auxnonrecargs) then + if chkpos && not (List.for_all (noccur_between n ntypes) auxnonrecargs) then failwith_non_pos_list n ntypes auxnonrecargs; (* Nested mutual inductive types are not supported *) let auxntyp = mib.mind_ntypes in @@ -613,7 +622,8 @@ let check_positivity_one recursive (env,_,ntypes,_ as ienv) paramsctxt (_,i as i | _ -> raise (IllFormedInd (LocalNotConstructor(paramsctxt,nnonrecargs))) end else - if not (List.for_all (noccur_between n ntypes) largs) + if chkpos && + not (List.for_all (noccur_between n ntypes) largs) then failwith_non_pos_list n ntypes largs in (nmr, List.rev lrec) @@ -633,9 +643,13 @@ let check_positivity_one recursive (env,_,ntypes,_ as ienv) paramsctxt (_,i as i and nmr' = array_min nmr irecargs_nmr in (nmr', mk_paths (Mrec ind) irecargs) -(** [check_positivity kn env_ar paramsctxt inds] checks that the mutually - inductive block [inds] is strictly positive. *) -let check_positivity kn env_ar_par paramsctxt finite inds = +(** [check_positivity ~chkpos kn env_ar paramsctxt inds] checks that the mutually + inductive block [inds] is strictly positive. + + If [chkpos] is [false] then positivity is assumed, and + [check_positivity_one] computes the subterms occurrences in a + best-effort fashion. *) +let check_positivity ~chkpos kn env_ar_par paramsctxt finite inds = let ntypes = Array.length inds in let recursive = finite != Decl_kinds.BiFinite in let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) in @@ -647,7 +661,7 @@ let check_positivity kn env_ar_par paramsctxt finite inds = List.init nparamsctxt (fun _ -> (Norec,mk_norec)) @ ra_env_ar in let ienv = (env_ar_par, 1+nparamsctxt, ntypes, ra_env_ar_par) in let nnonrecargs = Context.Rel.nhyps sign - nmr in - check_positivity_one recursive ienv paramsctxt (kn,i) nnonrecargs lcnames lc + check_positivity_one ~chkpos recursive ienv paramsctxt (kn,i) nnonrecargs lcnames lc in let irecargs_nmr = Array.mapi check_one inds in let irecargs = Array.map snd irecargs_nmr @@ -802,7 +816,7 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params Array.of_list (List.rev kns), Array.of_list (List.rev pbs) -let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nmr recargs = +let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nmr recargs is_checked = let ntypes = Array.length inds in (* Compute the set of used section variables *) let hyps = used_section_variables env inds in @@ -908,6 +922,7 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm mind_polymorphic = p; mind_universes = ctx; mind_private = prv; + mind_checked_positive = is_checked; } (************************************************************************) @@ -916,10 +931,11 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm let check_inductive env kn mie = (* First type-check the inductive definition *) let (env_ar, env_ar_par, paramsctxt, inds) = typecheck_inductive env mie in + let chkpos = mie.mind_entry_check_positivity in (* Then check positivity conditions *) - let (nmr,recargs) = check_positivity kn env_ar_par paramsctxt mie.mind_entry_finite inds in + let (nmr,recargs) = check_positivity ~chkpos kn env_ar_par paramsctxt mie.mind_entry_finite inds in (* Build the inductive packets *) build_inductive env mie.mind_entry_polymorphic mie.mind_entry_private mie.mind_entry_universes env_ar paramsctxt kn mie.mind_entry_record mie.mind_entry_finite - inds nmr recargs + inds nmr recargs chkpos diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 499cbf0dfd..24bdaa5c43 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -1067,21 +1067,24 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = (Array.map fst rv, Array.map snd rv) -let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) = - let (minds, rdef) = inductive_of_mutfix env fix in - let get_tree (kn,i) = - let mib = Environ.lookup_mind kn env in - mib.mind_packets.(i).mind_recargs - in - let trees = Array.map (fun (mind,_) -> get_tree mind) minds in - for i = 0 to Array.length bodies - 1 do - let (fenv,body) = rdef.(i) in - let renv = make_renv fenv nvect.(i) trees.(i) in - try check_one_fix renv nvect trees body - with FixGuardError (fixenv,err) -> - error_ill_formed_rec_body fixenv err names i - (push_rec_types recdef env) (judgment_of_fixpoint recdef) - done +let check_fix env ~flags ((nvect,_),(names,_,bodies as recdef) as fix) = + if flags.check_guarded then + let (minds, rdef) = inductive_of_mutfix env fix in + let get_tree (kn,i) = + let mib = Environ.lookup_mind kn env in + mib.mind_packets.(i).mind_recargs + in + let trees = Array.map (fun (mind,_) -> get_tree mind) minds in + for i = 0 to Array.length bodies - 1 do + let (fenv,body) = rdef.(i) in + let renv = make_renv fenv nvect.(i) trees.(i) in + try check_one_fix renv nvect trees body + with FixGuardError (fixenv,err) -> + error_ill_formed_rec_body fixenv err names i + (push_rec_types recdef env) (judgment_of_fixpoint recdef) + done + else + () (* let cfkey = Profile.declare_profile "check_fix";; @@ -1192,12 +1195,15 @@ let check_one_cofix env nbfix def deftype = (* The function which checks that the whole block of definitions satisfies the guarded condition *) -let check_cofix env (bodynum,(names,types,bodies as recdef)) = - let nbfix = Array.length bodies in - for i = 0 to nbfix-1 do - let fixenv = push_rec_types recdef env in - try check_one_cofix fixenv nbfix bodies.(i) types.(i) - with CoFixGuardError (errenv,err) -> - error_ill_formed_rec_body errenv err names i - fixenv (judgment_of_fixpoint recdef) - done +let check_cofix env ~flags (bodynum,(names,types,bodies as recdef)) = + if flags.check_guarded then + let nbfix = Array.length bodies in + for i = 0 to nbfix-1 do + let fixenv = push_rec_types recdef env in + try check_one_cofix fixenv nbfix bodies.(i) types.(i) + with CoFixGuardError (errenv,err) -> + error_ill_formed_rec_body errenv err names i + fixenv (judgment_of_fixpoint recdef) + done + else + () diff --git a/kernel/inductive.mli b/kernel/inductive.mli index c0d18bc6eb..25a5574721 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -94,8 +94,11 @@ val inductive_sort_family : one_inductive_body -> sorts_family val check_case_info : env -> pinductive -> case_info -> unit (** {6 Guard conditions for fix and cofix-points. } *) -val check_fix : env -> fixpoint -> unit -val check_cofix : env -> cofixpoint -> unit + +(** When [chk] is false, the guard condition is not actually + checked. *) +val check_fix : env -> flags:typing_flags -> fixpoint -> unit +val check_cofix : env -> flags:typing_flags -> cofixpoint -> unit (** {6 Support for sort-polymorphic inductive types } *) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index ce05190b6f..72d6ee518f 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -373,8 +373,8 @@ let safe_push_named d env = Environ.push_named d env -let push_named_def (id,de) senv = - let c,typ,univs = Term_typing.translate_local_def senv.revstruct senv.env id de in +let push_named_def ~flags (id,de) senv = + let c,typ,univs = Term_typing.translate_local_def ~flags senv.revstruct senv.env id de in let poly = de.Entries.const_entry_polymorphic in let univs = Univ.ContextSet.of_context univs in let c, univs = match c with @@ -388,9 +388,9 @@ let push_named_def (id,de) senv = let env'' = safe_push_named (LocalDef (id,c,typ)) senv'.env in univs, {senv' with env=env''} -let push_named_assum ((id,t,poly),ctx) senv = +let push_named_assum ~flags ((id,t,poly),ctx) senv = let senv' = push_context_set poly ctx senv in - let t = Term_typing.translate_local_assum senv'.env t in + let t = Term_typing.translate_local_assum ~flags senv'.env t in let env'' = safe_push_named (LocalAssum (id,t)) senv'.env in {senv' with env=env''} @@ -479,7 +479,7 @@ let update_resolver f senv = { senv with modresolver = f senv.modresolver } (** Insertion of constants and parameters in environment *) type global_declaration = - | ConstantEntry of bool * private_constants Entries.constant_entry + | ConstantEntry of bool * private_constants Entries.constant_entry * Declarations.typing_flags | GlobalRecipe of Cooking.recipe type exported_private_constant = @@ -512,10 +512,10 @@ let add_constant dir l decl senv = let no_section = DirPath.is_empty dir in let seff_to_export, decl = match decl with - | ConstantEntry (true, ce) -> + | ConstantEntry (true, ce, flags) -> let exports, ce = - Term_typing.export_side_effects senv.revstruct senv.env ce in - exports, ConstantEntry (false, ce) + Term_typing.export_side_effects ~flags senv.revstruct senv.env ce in + exports, ConstantEntry (false, ce, flags) | _ -> [], decl in let senv = @@ -524,8 +524,8 @@ let add_constant dir l decl senv = let senv = let cb = match decl with - | ConstantEntry (export_seff,ce) -> - Term_typing.translate_constant senv.revstruct senv.env kn ce + | ConstantEntry (export_seff,ce,flags) -> + Term_typing.translate_constant ~flags senv.revstruct senv.env kn ce | GlobalRecipe r -> let cb = Term_typing.translate_recipe senv.env kn r in if no_section then Declareops.hcons_const_body cb else cb in diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 71dac321f6..b614a368cb 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -77,19 +77,21 @@ val is_joined_environment : safe_environment -> bool (** Insertion of local declarations (Local or Variables) *) val push_named_assum : + flags:Declarations.typing_flags -> (Id.t * Term.types * bool (* polymorphic *)) Univ.in_universe_context_set -> safe_transformer0 (** Returns the full universe context necessary to typecheck the definition (futures are forced) *) val push_named_def : + flags:Declarations.typing_flags -> Id.t * private_constants Entries.definition_entry -> Univ.universe_context_set safe_transformer (** Insertion of global axioms or definitions *) type global_declaration = (* bool: export private constants *) - | ConstantEntry of bool * private_constants Entries.constant_entry + | ConstantEntry of bool * private_constants Entries.constant_entry * Declarations.typing_flags | GlobalRecipe of Cooking.recipe type exported_private_constant = diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 6bfd2457a8..8d74dc3902 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -22,18 +22,18 @@ open Entries open Typeops open Fast_typeops -let constrain_type env j poly subst = function +let constrain_type ~flags env j poly subst = function | `None -> if not poly then (* Old-style polymorphism *) make_polymorphic_if_constant_for_ind env j else RegularArity (Vars.subst_univs_level_constr subst j.uj_type) | `Some t -> - let tj = infer_type env t in + let tj = infer_type ~flags env t in let _ = judge_of_cast env j DEFAULTcast tj in assert (eq_constr t tj.utj_val); RegularArity (Vars.subst_univs_level_constr subst t) | `SomeWJ (t, tj) -> - let tj = infer_type env t in + let tj = infer_type ~flags env t in let _ = judge_of_cast env j DEFAULTcast tj in assert (eq_constr t tj.utj_val); RegularArity (Vars.subst_univs_level_constr subst t) @@ -171,11 +171,11 @@ let feedback_completion_typecheck = Option.iter (fun state_id -> feedback ~id:(State state_id) Feedback.Complete) -let infer_declaration ~trust env kn dcl = +let infer_declaration ~flags ~trust env kn dcl = match dcl with | ParameterEntry (ctx,poly,(t,uctx),nl) -> let env = push_context ~strict:(not poly) uctx env in - let j = infer env t in + let j = infer ~flags env t in let abstract = poly && not (Option.is_empty kn) in let usubst, univs = Univ.abstract_universes abstract uctx in let c = Typeops.assumption_of_judgment env j in @@ -196,7 +196,7 @@ let infer_declaration ~trust env kn dcl = let env' = push_context_set uctx env in let j = let body,env',ectx = skip_trusted_seff valid_signatures body env' in - let j = infer env' body in + let j = infer ~flags env' body in unzip ectx j in let j = hcons_j j in let subst = Univ.LMap.empty in @@ -220,8 +220,8 @@ let infer_declaration ~trust env kn dcl = let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in let usubst, univs = Univ.abstract_universes abstract (Univ.ContextSet.to_context ctx) in - let j = infer env body in - let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in + let j = infer ~flags env body in + let typ = constrain_type ~flags env j c.const_entry_polymorphic usubst (map_option_typ typ) in let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in let def = if opaque then OpaqueDef (Opaqueproof.create (Future.from_val (def, Univ.ContextSet.empty))) @@ -268,7 +268,7 @@ let record_aux env s_ty s_bo suggested_expr = let suggest_proof_using = ref (fun _ _ _ _ _ -> "") let set_suggest_proof_using f = suggest_proof_using := f -let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) = +let build_constant_declaration ~flags kn env (def,typ,proj,poly,univs,inline_code,ctx) = let open Context.Named.Declaration in let check declared inferred = let mk_set l = List.fold_right Id.Set.add (List.map get_id l) Id.Set.empty in @@ -352,7 +352,9 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) const_body_code = None; const_polymorphic = poly; const_universes = univs; - const_inline_code = inline_code } + const_inline_code = inline_code; + const_typing_flags = flags; + } in let env = add_constant kn cb env in compile_constant_body env comp_univs def @@ -365,13 +367,14 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) const_body_code = tps; const_polymorphic = poly; const_universes = univs; - const_inline_code = inline_code } + const_inline_code = inline_code; + const_typing_flags = flags } (*s Global and local constant declaration. *) -let translate_constant mb env kn ce = - build_constant_declaration kn env - (infer_declaration ~trust:mb env (Some kn) ce) +let translate_constant ~flags mb env kn ce = + build_constant_declaration ~flags kn env + (infer_declaration ~flags ~trust:mb env (Some kn) ce) let constant_entry_of_side_effect cb u = let pt = @@ -406,7 +409,7 @@ type side_effect_role = type exported_side_effect = constant * constant_body * side_effects constant_entry * side_effect_role -let export_side_effects mb env ce = +let export_side_effects ~flags mb env ce = match ce with | ParameterEntry _ | ProjectionEntry _ -> [], ce | DefinitionEntry c -> @@ -447,7 +450,7 @@ let export_side_effects mb env ce = let env, cbs = List.fold_left (fun (env,cbs) (kn, ocb, u, r) -> let ce = constant_entry_of_side_effect ocb u in - let cb = translate_constant mb env kn ce in + let cb = translate_constant ~flags mb env kn ce in (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,ce,r) :: cbs)) (env,[]) cbs in translate_seff sl rest (cbs @ acc) env @@ -462,17 +465,17 @@ let export_side_effects mb env ce = translate_seff trusted seff [] env ;; -let translate_local_assum env t = - let j = infer env t in +let translate_local_assum ~flags env t = + let j = infer ~flags env t in let t = Typeops.assumption_of_judgment env j in t let translate_recipe env kn r = - build_constant_declaration kn env (Cooking.cook_constant env r) + build_constant_declaration ~flags:{check_guarded=true} kn env (Cooking.cook_constant env r) -let translate_local_def mb env id centry = +let translate_local_def ~flags mb env id centry = let def,typ,proj,poly,univs,inline_code,ctx = - infer_declaration ~trust:mb env None (DefinitionEntry centry) in + infer_declaration ~flags ~trust:mb env None (DefinitionEntry centry) in let typ = type_of_constant_type env typ in if ctx = None && !Flags.compilation_mode = Flags.BuildVo then begin match def with diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index fcd95576c0..b635f2d314 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -12,10 +12,10 @@ open Environ open Declarations open Entries -val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry -> +val translate_local_def : flags:typing_flags -> structure_body -> env -> Id.t -> side_effects definition_entry -> constant_def * types * constant_universes -val translate_local_assum : env -> types -> types +val translate_local_assum : flags:typing_flags -> env -> types -> types val mk_pure_proof : constr -> side_effects proof_output @@ -32,7 +32,7 @@ val inline_entry_side_effects : val uniq_seff : side_effects -> side_effects val translate_constant : - structure_body -> env -> constant -> side_effects constant_entry -> + flags:typing_flags -> structure_body -> env -> constant -> side_effects constant_entry -> constant_body type side_effect_role = @@ -47,7 +47,7 @@ type exported_side_effect = * be pushed in the safe_env by safe typing. The main constant entry * needs to be translated as usual after this step. *) val export_side_effects : - structure_body -> env -> side_effects constant_entry -> + flags:typing_flags -> structure_body -> env -> side_effects constant_entry -> exported_side_effect list * side_effects constant_entry val constant_entry_of_side_effect : @@ -60,11 +60,11 @@ val translate_recipe : env -> constant -> Cooking.recipe -> constant_body (** Internal functions, mentioned here for debug purpose only *) -val infer_declaration : trust:structure_body -> env -> constant option -> +val infer_declaration : flags:typing_flags -> trust:structure_body -> env -> constant option -> side_effects constant_entry -> Cooking.result val build_constant_declaration : - constant -> env -> Cooking.result -> constant_body + flags:typing_flags -> constant -> env -> Cooking.result -> constant_body val set_suggest_proof_using : (string -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> string) -> unit diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 0ea68e2bcc..a94a049df1 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -500,13 +500,13 @@ let rec execute env cstr = | Fix ((vn,i as vni),recdef) -> let (fix_ty,recdef') = execute_recdef env recdef i in let fix = (vni,recdef') in - check_fix env fix; + check_fix ~flags:{check_guarded=true} env fix; make_judge (mkFix fix) fix_ty | CoFix (i,recdef) -> let (fix_ty,recdef') = execute_recdef env recdef i in let cofix = (i,recdef') in - check_cofix env cofix; + check_cofix ~flags:{check_guarded=true} env cofix; (make_judge (mkCoFix cofix) fix_ty) (* Partial proofs: unsupported by the kernel *) diff --git a/library/declare.ml b/library/declare.ml index 84284fd182..9ec299bed9 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -58,11 +58,11 @@ let cache_variable ((sp,_),o) = let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *) | SectionLocalAssum ((ty,ctx),poly,impl) -> - let () = Global.push_named_assum ((id,ty,poly),ctx) in + let () = Global.push_named_assum ~flags:{check_guarded=true} ((id,ty,poly),ctx) in let impl = if impl then Implicit else Explicit in impl, true, poly, ctx | SectionLocalDef (de) -> - let univs = Global.push_named_def (id,de) in + let univs = Global.push_named_def ~flags:{check_guarded=true} (id,de) in Explicit, de.const_entry_opaque, de.const_entry_polymorphic, univs in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); @@ -180,7 +180,7 @@ let discharge_constant ((sp, kn), obj) = (* Hack to reduce the size of .vo: we keep only what load/open needs *) let dummy_constant_entry = ConstantEntry - (false, ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None)) + (false, ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None), {check_guarded=true}) let dummy_constant cst = { cst_decl = dummy_constant_entry; @@ -205,7 +205,7 @@ let (inConstant, outConstant : (constant_obj -> obj) * (obj -> constant_obj)) = let declare_scheme = ref (fun _ _ -> assert false) let set_declare_scheme f = declare_scheme := f -let declare_constant_common id cst = +let declare_constant_common ~flags id cst = let update_tables c = (* Printf.eprintf "tables: %s\n%!" (Names.Constant.to_string c); *) declare_constant_implicits c; @@ -216,7 +216,7 @@ let declare_constant_common id cst = List.iter (fun (c,ce,role) -> (* handling of private_constants just exported *) let o = inConstant { - cst_decl = ConstantEntry (false, ce); + cst_decl = ConstantEntry (false, ce, flags); cst_hyps = [] ; cst_kind = IsProof Theorem; cst_locl = false; @@ -246,7 +246,7 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types const_entry_feedback = None; const_entry_inline_code = inline} -let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) = +let declare_constant ?(flags={check_guarded=true}) ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) = let export = (* We deal with side effects *) match cd with | DefinitionEntry de when @@ -259,24 +259,24 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e | _ -> false in let cst = { - cst_decl = ConstantEntry (export,cd); + cst_decl = ConstantEntry (export,cd,flags); cst_hyps = [] ; cst_kind = kind; cst_locl = local; cst_exported = []; cst_was_seff = false; } in - let kn = declare_constant_common id cst in + let kn = declare_constant_common id cst ~flags in let () = if_xml (Hook.get f_xml_declare_constant) (internal, kn) in kn -let declare_definition ?(internal=UserIndividualRequest) +let declare_definition ?flags ?(internal=UserIndividualRequest) ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false) ?(poly=false) id ?types (body,ctx) = let cb = definition_entry ?types ~poly ~univs:(Univ.ContextSet.to_context ctx) ~opaque body in - declare_constant ~internal ~local id + declare_constant ?flags ~internal ~local id (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind) (** Declaration of inductive blocks *) @@ -353,7 +353,8 @@ let dummy_inductive_entry (_,m) = ([],{ mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; mind_entry_polymorphic = false; mind_entry_universes = Univ.UContext.empty; - mind_entry_private = None }) + mind_entry_private = None; + mind_entry_check_positivity = true; }) type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry @@ -373,7 +374,7 @@ let declare_projections mind = Array.iteri (fun i kn -> let id = Label.to_id (Constant.label kn) in let entry = {proj_entry_ind = mind; proj_entry_arg = i} in - let kn' = declare_constant id (ProjectionEntry entry, + let kn' = declare_constant ~flags:{check_guarded=true} id (ProjectionEntry entry, IsDefinition StructureComponent) in assert(eq_constant kn kn')) kns; true,true diff --git a/library/declare.mli b/library/declare.mli index 8dd24d2780..3ba63b5a6b 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -54,9 +54,11 @@ val definition_entry : ?fix_exn:Future.fix_exn -> ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry val declare_constant : + ?flags:Declarations.typing_flags -> (** default [check_guarded=true] *) ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant val declare_definition : + ?flags:Declarations.typing_flags -> (** default [check_guarded=true] *) ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind -> ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> constr Univ.in_universe_context_set -> constant diff --git a/library/global.ml b/library/global.ml index 2398e92b03..f4ee62b6e5 100644 --- a/library/global.ml +++ b/library/global.ml @@ -77,8 +77,8 @@ let globalize_with_summary fs f = let i2l = Label.of_id -let push_named_assum a = globalize0 (Safe_typing.push_named_assum a) -let push_named_def d = globalize (Safe_typing.push_named_def d) +let push_named_assum ~flags a = globalize0 (Safe_typing.push_named_assum ~flags a) +let push_named_def ~flags d = globalize (Safe_typing.push_named_def ~flags d) let add_constraints c = globalize0 (Safe_typing.add_constraints c) let push_context_set b c = globalize0 (Safe_typing.push_context_set b c) let push_context b c = globalize0 (Safe_typing.push_context b c) diff --git a/library/global.mli b/library/global.mli index bf653307c4..7c6cecb4e3 100644 --- a/library/global.mli +++ b/library/global.mli @@ -30,8 +30,8 @@ val set_engagement : Declarations.engagement -> unit (** Variables, Local definitions, constants, inductive types *) -val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit -val push_named_def : (Id.t * Safe_typing.private_constants Entries.definition_entry) -> Univ.universe_context_set +val push_named_assum : flags:Declarations.typing_flags -> (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit +val push_named_def : flags:Declarations.typing_flags -> (Id.t * Safe_typing.private_constants Entries.definition_entry) -> Univ.universe_context_set val add_constant : DirPath.t -> Id.t -> Safe_typing.global_declaration -> diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index ab61c8abba..649764da37 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -385,7 +385,7 @@ let interp_ltac_var coerce ist env locid = with Not_found -> anomaly (str "Detected '" ++ Id.print (snd locid) ++ str "' as ltac var at interning time") let interp_ident ist env sigma id = - try try_interp_ltac_var (coerce_to_ident false env) ist (Some (env,sigma)) (dloc,id) + try try_interp_ltac_var (coerce_var_to_ident false env) ist (Some (env,sigma)) (dloc,id) with Not_found -> id let pf_interp_ident id gl = interp_ident id (pf_env gl) (project gl) @@ -541,6 +541,10 @@ let extract_ids ids lfun = let default_fresh_id = Id.of_string "H" let interp_fresh_id ist env sigma l = + let extract_ident ist env sigma id = + try try_interp_ltac_var (coerce_to_ident_not_fresh sigma env) + ist (Some (env,sigma)) (dloc,id) + with Not_found -> id in let ids = List.map_filter (function ArgVar (_, id) -> Some id | _ -> None) l in let avoid = match TacStore.get ist.extra f_avoid_ids with | None -> [] @@ -553,7 +557,7 @@ let interp_fresh_id ist env sigma l = let s = String.concat "" (List.map (function | ArgArg s -> s - | ArgVar (_,id) -> Id.to_string (interp_ident ist env sigma id)) l) in + | ArgVar (_,id) -> Id.to_string (extract_ident ist env sigma id)) l) in let s = if CLexer.is_keyword s then s^"0" else s in Id.of_string s in Tactics.fresh_id_in_env avoid id env @@ -570,7 +574,7 @@ let extract_ltac_constr_context ist env = with CannotCoerceTo _ -> map in let add_ident id env v map = - try Id.Map.add id (coerce_to_ident false env v) map + try Id.Map.add id (coerce_var_to_ident false env v) map with CannotCoerceTo _ -> map in let fold id v {idents;typed;untyped} = diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 21a9afa293..ade31c1d3c 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -9,9 +9,10 @@ open Errors open Util open Pcoq -open Extend open Constrexpr +open Notation open Notation_term +open Extend open Libnames open Names @@ -320,13 +321,6 @@ let cases_pattern_expr_of_name (loc,na) = match na with | Anonymous -> CPatAtom (loc,None) | Name id -> CPatAtom (loc,Some (Ident (loc,id))) -type grammar_constr_prod_item = - | GramConstrTerminal of Tok.t - | GramConstrNonTerminal of constr_prod_entry_key * Id.t option - | GramConstrListMark of int * bool - (* tells action rule to make a list of the n previous parsed items; - concat with last parsed list if true *) - type 'r env = { constrs : 'r list; constrlists : 'r list list; @@ -444,14 +438,6 @@ let make_act : type r. r target -> _ -> r gen_eval = function let env = (env.constrs, env.constrlists) in CPatNotation (loc, notation, env, []) -type notation_grammar = { - notgram_level : int; - notgram_assoc : gram_assoc option; - notgram_notation : notation; - notgram_prods : grammar_constr_prod_item list list; - notgram_typs : notation_var_internalization_type list; -} - let extend_constr state forpat ng = let n = ng.notgram_level in let assoc = ng.notgram_assoc in @@ -491,12 +477,3 @@ let constr_grammar : (Notation.level * notation_grammar) grammar_command = create_grammar_command "Notation" extend_constr_notation let extend_constr_grammar pr ntn = extend_grammar_command constr_grammar (pr, ntn) - -let recover_constr_grammar ntn prec = - let filter (prec', ng) = - if Notation.level_eq prec prec' && String.equal ntn ng.notgram_notation then Some ng - else None - in - match List.map_filter filter (recover_grammar_command constr_grammar) with - | [x] -> x - | _ -> assert false diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli index 1fe06a29df..6dda3817ae 100644 --- a/parsing/egramcoq.mli +++ b/parsing/egramcoq.mli @@ -19,28 +19,7 @@ open Egramml (** This is the part specific to Coq-level Notation and Tactic Notation. For the ML-level tactic and vernac extensions, see Egramml. *) -(** For constr notations *) - -type grammar_constr_prod_item = - | GramConstrTerminal of Tok.t - | GramConstrNonTerminal of constr_prod_entry_key * Id.t option - | GramConstrListMark of int * bool - (* tells action rule to make a list of the n previous parsed items; - concat with last parsed list if true *) - -type notation_grammar = { - notgram_level : int; - notgram_assoc : gram_assoc option; - notgram_notation : notation; - notgram_prods : grammar_constr_prod_item list list; - notgram_typs : notation_var_internalization_type list; -} - (** {5 Adding notations} *) -val extend_constr_grammar : Notation.level -> notation_grammar -> unit +val extend_constr_grammar : Notation.level -> Notation_term.notation_grammar -> unit (** Add a term notation rule to the parsing system. *) - -val recover_constr_grammar : notation -> Notation.level -> notation_grammar -(** For a declared grammar, returns the rule + the ordered entry types - of variables in the rule (for use in the interpretation) *) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 0df15babd1..9c1f5afb86 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -1076,6 +1076,7 @@ GEXTEND Gram | IDENT "left"; IDENT "associativity" -> SetAssoc LeftA | IDENT "right"; IDENT "associativity" -> SetAssoc RightA | IDENT "no"; IDENT "associativity" -> SetAssoc NonA + | IDENT "only"; IDENT "printing" -> SetOnlyPrinting | IDENT "only"; IDENT "parsing" -> SetOnlyParsing Flags.Current | IDENT "compat"; s = STRING -> diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index c424fe1226..f69c4d8217 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1432,7 +1432,7 @@ let do_build_inductive (* in *) let _time2 = System.get_time () in try - with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false)) Decl_kinds.Finite + with_full_print (Flags.silently (Command.do_mutual_inductive true rel_inds (Flags.is_universe_polymorphism ()) false)) Decl_kinds.Finite with | UserError(s,msg) as e -> let _time3 = System.get_time () in diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 0cacb003d8..d8340dddb4 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -400,7 +400,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp in evd,List.rev rev_pconstants | _ -> - Command.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; + Command.do_fixpoint ~flags:{Declarations.check_guarded=true} Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; let evd,rev_pconstants = List.fold_left (fun (evd,l) ((((_,fname),_),_,_,_,_),_) -> diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 99a165044c..a78eb1af76 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -887,7 +887,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive) let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in (* Declare inductive *) let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in - let mie,pl,impls = Command.interp_mutual_inductive indl [] + let mie,pl,impls = Command.interp_mutual_inductive true indl [] false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in (* Declare the mutual inductive block with its associated schemes *) ignore (Command.declare_mutual_inductive_with_eliminations mie pl impls) diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v index 77863edc1e..fc02cef100 100644 --- a/plugins/setoid_ring/Ring_tac.v +++ b/plugins/setoid_ring/Ring_tac.v @@ -422,8 +422,6 @@ Tactic Notation (at level 0) let G := Get_goal in ring_lookup (PackRing Ring_simplify) [lH] rl G. -(* MON DIEU QUE C'EST MOCHE !!!!!!!!!!!!! *) - Tactic Notation "ring_simplify" constr_list(rl) "in" hyp(H):= let G := Get_goal in let t := type of H in diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 new file mode 100644 index 0000000000..933e2baee3 --- /dev/null +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -0,0 +1,1436 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) + +(* Defining grammar rules with "xx" in it automatically declares keywords too, + * we thus save the lexer to restore it at the end of the file *) +let frozen_lexer = CLexer.freeze () ;; + +(*i camlp4use: "pa_extend.cmo" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) + +open Names +open Pp +open Pcoq +open Genarg +open Constrarg +open Term +open Vars +open Topconstr +open Libnames +open Tactics +open Tacticals +open Termops +open Namegen +open Recordops +open Tacmach +open Coqlib +open Glob_term +open Util +open Evd +open Extend +open Goptions +open Tacexpr +open Proofview.Notations +open Tacinterp +open Pretyping +open Constr +open Tactic +open Extraargs +open Ppconstr +open Printer + +open Globnames +open Misctypes +open Decl_kinds +open Evar_kinds +open Constrexpr +open Constrexpr_ops +open Notation_term +open Notation_ops +open Locus +open Locusops + +DECLARE PLUGIN "ssrmatching_plugin" + +type loc = Loc.t +let dummy_loc = Loc.ghost +let errorstrm = Errors.errorlabstrm "ssrmatching" +let loc_error loc msg = Errors.user_err_loc (loc, msg, str msg) +let ppnl = Feedback.msg_info + +(* 0 cost pp function. Active only if env variable SSRDEBUG is set *) +(* or if SsrDebug is Set *) +let pp_ref = ref (fun _ -> ()) +let ssr_pp s = Feedback.msg_debug (str"SSR: "++Lazy.force s) +let _ = + try ignore(Sys.getenv "SSRMATCHINGDEBUG"); pp_ref := ssr_pp + with Not_found -> () +let debug b = + if b then pp_ref := ssr_pp else pp_ref := fun _ -> () +let _ = + Goptions.declare_bool_option + { Goptions.optsync = false; + Goptions.optname = "ssrmatching debugging"; + Goptions.optkey = ["Debug";"SsrMatching"]; + Goptions.optdepr = false; + Goptions.optread = (fun _ -> !pp_ref == ssr_pp); + Goptions.optwrite = debug } +let pp s = !pp_ref s + +(** Utils {{{ *****************************************************************) +let env_size env = List.length (Environ.named_context env) +let safeDestApp c = + match kind_of_term c with App (f, a) -> f, a | _ -> c, [| |] +let get_index = function ArgArg i -> i | _ -> + Errors.anomaly (str"Uninterpreted index") +(* Toplevel constr must be globalized twice ! *) +let glob_constr ist genv = function + | _, Some ce -> + let vars = Id.Map.fold (fun x _ accu -> Id.Set.add x accu) ist.lfun Id.Set.empty in + let ltacvars = { Constrintern.empty_ltac_sign with Constrintern.ltac_vars = vars } in + Constrintern.intern_gen WithoutTypeConstraint ~ltacvars:ltacvars genv ce + | rc, None -> rc + +(* Term printing utilities functions for deciding bracketing. *) +let pr_paren prx x = hov 1 (str "(" ++ prx x ++ str ")") +(* String lexing utilities *) +let skip_wschars s = + let rec loop i = match s.[i] with '\n'..' ' -> loop (i + 1) | _ -> i in loop +(* We also guard characters that might interfere with the ssreflect *) +(* tactic syntax. *) +let guard_term ch1 s i = match s.[i] with + | '(' -> false + | '{' | '/' | '=' -> true + | _ -> ch1 = '(' +(* The call 'guard s i' should return true if the contents of s *) +(* starting at i need bracketing to avoid ambiguities. *) +let pr_guarded guard prc c = + msg_with Format.str_formatter (prc c); + let s = Format.flush_str_formatter () ^ "$" in + if guard s (skip_wschars s 0) then pr_paren prc c else prc c +(* More sensible names for constr printers *) +let pr_constr = pr_constr +let prl_glob_constr c = pr_lglob_constr_env (Global.env ()) c +let pr_glob_constr c = pr_glob_constr_env (Global.env ()) c +let prl_constr_expr = pr_lconstr_expr +let pr_constr_expr = pr_constr_expr +let prl_glob_constr_and_expr = function + | _, Some c -> prl_constr_expr c + | c, None -> prl_glob_constr c +let pr_glob_constr_and_expr = function + | _, Some c -> pr_constr_expr c + | c, None -> pr_glob_constr c +let pr_term (k, c) = pr_guarded (guard_term k) pr_glob_constr_and_expr c +let prl_term (k, c) = pr_guarded (guard_term k) prl_glob_constr_and_expr c + +(** Adding a new uninterpreted generic argument type *) +let add_genarg tag pr = + let wit = Genarg.make0 tag in + let tag = Geninterp.Val.create tag in + let glob ist x = (ist, x) in + let subst _ x = x in + let interp ist x = Ftactic.return (Geninterp.Val.Dyn (tag, x)) in + let gen_pr _ _ _ = pr in + let () = Genintern.register_intern0 wit glob in + let () = Genintern.register_subst0 wit subst in + let () = Geninterp.register_interp0 wit interp in + let () = Geninterp.register_val0 wit (Some (Geninterp.Val.Base tag)) in + Pptactic.declare_extra_genarg_pprule wit gen_pr gen_pr gen_pr; + wit + +(** Constructors for cast type *) +let dC t = CastConv t +(** Constructors for constr_expr *) +let isCVar = function CRef (Ident _, _) -> true | _ -> false +let destCVar = function CRef (Ident (_, id), _) -> id | _ -> + Errors.anomaly (str"not a CRef") +let mkCHole loc = CHole (loc, None, IntroAnonymous, None) +let mkCLambda loc name ty t = + CLambdaN (loc, [[loc, name], Default Explicit, ty], t) +let mkCLetIn loc name bo t = + CLetIn (loc, (loc, name), bo, t) +let mkCCast loc t ty = CCast (loc,t, dC ty) +(** Constructors for rawconstr *) +let mkRHole = GHole (dummy_loc, InternalHole, IntroAnonymous, None) +let mkRApp f args = if args = [] then f else GApp (dummy_loc, f, args) +let mkRCast rc rt = GCast (dummy_loc, rc, dC rt) +let mkRLambda n s t = GLambda (dummy_loc, n, Explicit, s, t) + +(* ssrterm conbinators *) +let combineCG t1 t2 f g = match t1, t2 with + | (x, (t1, None)), (_, (t2, None)) -> x, (g t1 t2, None) + | (x, (_, Some t1)), (_, (_, Some t2)) -> x, (mkRHole, Some (f t1 t2)) + | _, (_, (_, None)) -> Errors.anomaly (str"have: mixed C-G constr") + | _ -> Errors.anomaly (str"have: mixed G-C constr") +let loc_ofCG = function + | (_, (s, None)) -> Glob_ops.loc_of_glob_constr s + | (_, (_, Some s)) -> Constrexpr_ops.constr_loc s + +let mk_term k c = k, (mkRHole, Some c) +let mk_lterm = mk_term ' ' + +let pf_type_of gl t = let sigma, ty = pf_type_of gl t in re_sig (sig_it gl) sigma, ty + +(* }}} *) + +(** Profiling {{{ *************************************************************) +type profiler = { + profile : 'a 'b. ('a -> 'b) -> 'a -> 'b; + reset : unit -> unit; + print : unit -> unit } +let profile_now = ref false +let something_profiled = ref false +let profilers = ref [] +let add_profiler f = profilers := f :: !profilers;; +let profile b = + profile_now := b; + if b then List.iter (fun f -> f.reset ()) !profilers; + if not b then List.iter (fun f -> f.print ()) !profilers +;; +let _ = + Goptions.declare_bool_option + { Goptions.optsync = false; + Goptions.optname = "ssrmatching profiling"; + Goptions.optkey = ["SsrMatchingProfiling"]; + Goptions.optread = (fun _ -> !profile_now); + Goptions.optdepr = false; + Goptions.optwrite = profile } +let () = + let prof_total = + let init = ref 0.0 in { + profile = (fun f x -> assert false); + reset = (fun () -> init := Unix.gettimeofday ()); + print = (fun () -> if !something_profiled then + prerr_endline + (Printf.sprintf "!! %-39s %10d %9.4f %9.4f %9.4f" + "total" 0 (Unix.gettimeofday() -. !init) 0.0 0.0)) } in + let prof_legenda = { + profile = (fun f x -> assert false); + reset = (fun () -> ()); + print = (fun () -> if !something_profiled then begin + prerr_endline + (Printf.sprintf "!! %39s ---------- --------- --------- ---------" + (String.make 39 '-')); + prerr_endline + (Printf.sprintf "!! %-39s %10s %9s %9s %9s" + "function" "#calls" "total" "max" "average") end) } in + add_profiler prof_legenda; + add_profiler prof_total +;; + +let mk_profiler s = + let total, calls, max = ref 0.0, ref 0, ref 0.0 in + let reset () = total := 0.0; calls := 0; max := 0.0 in + let profile f x = + if not !profile_now then f x else + let before = Unix.gettimeofday () in + try + incr calls; + let res = f x in + let after = Unix.gettimeofday () in + let delta = after -. before in + total := !total +. delta; + if delta > !max then max := delta; + res + with exc -> + let after = Unix.gettimeofday () in + let delta = after -. before in + total := !total +. delta; + if delta > !max then max := delta; + raise exc in + let print () = + if !calls <> 0 then begin + something_profiled := true; + prerr_endline + (Printf.sprintf "!! %-39s %10d %9.4f %9.4f %9.4f" + s !calls !total !max (!total /. (float_of_int !calls))) end in + let prof = { profile = profile; reset = reset; print = print } in + add_profiler prof; + prof +;; +(* }}} *) + +exception NoProgress + +(** Unification procedures. *) + +(* To enforce the rigidity of the rooted match we always split *) +(* top applications, so the unification procedures operate on *) +(* arrays of patterns and terms. *) +(* We perform three kinds of unification: *) +(* EQ: exact conversion check *) +(* FO: first-order unification of evars, without conversion *) +(* HO: higher-order unification with conversion *) +(* The subterm unification strategy is to find the first FO *) +(* match, if possible, and the first HO match otherwise, then *) +(* compute all the occurrences that are EQ matches for the *) +(* relevant subterm. *) +(* Additional twists: *) +(* - If FO/HO fails then we attempt to fill evars using *) +(* typeclasses before raising an outright error. We also *) +(* fill typeclasses even after a successful match, since *) +(* beta-reduction and canonical instances may leave *) +(* undefined evars. *) +(* - We do postchecks to rule out matches that are not *) +(* closed or that assign to a global evar; these can be *) +(* disabled for rewrite or dependent family matches. *) +(* - We do a full FO scan before turning to HO, as the FO *) +(* comparison can be much faster than the HO one. *) + +let unif_EQ env sigma p c = + let evars = existential_opt_value sigma, Evd.universes sigma in + try let _ = Reduction.conv env p ~evars c in true with _ -> false + +let unif_EQ_args env sigma pa a = + let n = Array.length pa in + let rec loop i = (i = n) || unif_EQ env sigma pa.(i) a.(i) && loop (i + 1) in + loop 0 + +let prof_unif_eq_args = mk_profiler "unif_EQ_args";; +let unif_EQ_args env sigma pa a = + prof_unif_eq_args.profile (unif_EQ_args env sigma pa) a +;; + +let unif_HO env ise p c = Evarconv.the_conv_x env p c ise + +let unif_HOtype env ise p c = Evarconv.the_conv_x_leq env p c ise + +let unif_HO_args env ise0 pa i ca = + let n = Array.length pa in + let rec loop ise j = + if j = n then ise else loop (unif_HO env ise pa.(j) ca.(i + j)) (j + 1) in + loop ise0 0 + +(* FO unification should boil down to calling w_unify with no_delta, but *) +(* alas things are not so simple: w_unify does partial type-checking, *) +(* which breaks down when the no-delta flag is on (as the Coq type system *) +(* requires full convertibility. The workaround here is to convert all *) +(* evars into metas, since 8.2 does not TC metas. This means some lossage *) +(* for HO evars, though hopefully Miller patterns can pick up some of *) +(* those cases, and HO matching will mop up the rest. *) +let flags_FO = + let flags = + { (Unification.default_no_delta_unify_flags ()).Unification.core_unify_flags + with + Unification.modulo_conv_on_closed_terms = None; + Unification.modulo_eta = true; + Unification.modulo_betaiota = true; + Unification.modulo_delta_types = full_transparent_state} + in + { Unification.core_unify_flags = flags; + Unification.merge_unify_flags = flags; + Unification.subterm_unify_flags = flags; + Unification.allow_K_in_toplevel_higher_order_unification = false; + Unification.resolve_evars = + (Unification.default_no_delta_unify_flags ()).Unification.resolve_evars + } +let unif_FO env ise p c = + Unification.w_unify env ise Reduction.CONV ~flags:flags_FO p c + +(* Perform evar substitution in main term and prune substitution. *) +let nf_open_term sigma0 ise c = + let s = ise and s' = ref sigma0 in + let rec nf c' = match kind_of_term c' with + | Evar ex -> + begin try nf (existential_value s ex) with _ -> + let k, a = ex in let a' = Array.map nf a in + if not (Evd.mem !s' k) then + s' := Evd.add !s' k (Evarutil.nf_evar_info s (Evd.find s k)); + mkEvar (k, a') + end + | _ -> map_constr nf c' in + let copy_def k evi () = + if evar_body evi != Evd.Evar_empty then () else + match Evd.evar_body (Evd.find s k) with + | Evar_defined c' -> s' := Evd.define k (nf c') !s' + | _ -> () in + let c' = nf c in let _ = Evd.fold copy_def sigma0 () in + !s', Evd.evar_universe_context s, c' + +let unif_end env sigma0 ise0 pt ok = + let ise = Evarconv.consider_remaining_unif_problems env ise0 in + let s, uc, t = nf_open_term sigma0 ise pt in + let ise1 = create_evar_defs s in + let ise1 = Evd.set_universe_context ise1 uc in + let ise2 = Typeclasses.resolve_typeclasses ~fail:true env ise1 in + if not (ok ise) then raise NoProgress else + if ise2 == ise1 then (s, uc, t) + else + let s, uc', t = nf_open_term sigma0 ise2 t in + s, Evd.union_evar_universe_context uc uc', t + +let pf_unif_HO gl sigma pt p c = + let env = pf_env gl in + let ise = unif_HO env (create_evar_defs sigma) p c in + unif_end env (project gl) ise pt (fun _ -> true) + +let unify_HO env sigma0 t1 t2 = + let sigma = unif_HO env sigma0 t1 t2 in + let sigma, uc, _ = unif_end env sigma0 sigma t2 (fun _ -> true) in + Evd.set_universe_context sigma uc + +let pf_unify_HO gl t1 t2 = + let env, sigma0, si = pf_env gl, project gl, sig_it gl in + let sigma = unify_HO env sigma0 t1 t2 in + re_sig si sigma + +(* This is what the definition of iter_constr should be... *) +let iter_constr_LR f c = match kind_of_term c with + | Evar (k, a) -> Array.iter f a + | Cast (cc, _, t) -> f cc; f t + | Prod (_, t, b) | Lambda (_, t, b) -> f t; f b + | LetIn (_, v, t, b) -> f v; f t; f b + | App (cf, a) -> f cf; Array.iter f a + | Case (_, p, v, b) -> f v; f p; Array.iter f b + | Fix (_, (_, t, b)) | CoFix (_, (_, t, b)) -> + for i = 0 to Array.length t - 1 do f t.(i); f b.(i) done + | _ -> () + +(* The comparison used to determine which subterms matches is KEYED *) +(* CONVERSION. This looks for convertible terms that either have the same *) +(* same head constant as pat if pat is an application (after beta-iota), *) +(* or start with the same constr constructor (esp. for LetIn); this is *) +(* disregarded if the head term is let x := ... in x, and casts are always *) +(* ignored and removed). *) +(* Record projections get special treatment: in addition to the projection *) +(* constant itself, ssreflect also recognizes head constants of canonical *) +(* projections. *) + +exception NoMatch +type ssrdir = L2R | R2L +let pr_dir_side = function L2R -> str "LHS" | R2L -> str "RHS" +let inv_dir = function L2R -> R2L | R2L -> L2R + + +type pattern_class = + | KpatFixed + | KpatConst + | KpatEvar of existential_key + | KpatLet + | KpatLam + | KpatRigid + | KpatFlex + | KpatProj of constant + +type tpattern = { + up_k : pattern_class; + up_FO : constr; + up_f : constr; + up_a : constr array; + up_t : constr; (* equation proof term or matched term *) + up_dir : ssrdir; (* direction of the rule *) + up_ok : constr -> evar_map -> bool; (* progess test for rewrite *) + } + +let all_ok _ _ = true + +let proj_nparams c = + try 1 + Recordops.find_projection_nparams (ConstRef c) with _ -> 0 + +let isFixed c = match kind_of_term c with + | Var _ | Ind _ | Construct _ | Const _ -> true + | _ -> false + +let isRigid c = match kind_of_term c with + | Prod _ | Sort _ | Lambda _ | Case _ | Fix _ | CoFix _ -> true + | _ -> false + +exception UndefPat + +let hole_var = mkVar (id_of_string "_") +let pr_constr_pat c0 = + let rec wipe_evar c = + if isEvar c then hole_var else map_constr wipe_evar c in + pr_constr (wipe_evar c0) + +(* Turn (new) evars into metas *) +let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 = + let ise = ref ise0 in + let sigma = ref ise0 in + let nenv = env_size env + if hack then 1 else 0 in + let rec put c = match kind_of_term c with + | Evar (k, a as ex) -> + begin try put (existential_value !sigma ex) + with NotInstantiatedEvar -> + if Evd.mem sigma0 k then map_constr put c else + let evi = Evd.find !sigma k in + let dc = List.firstn (max 0 (Array.length a - nenv)) (evar_filtered_context evi) in + let abs_dc (d, c) = function + | Context.Named.Declaration.LocalDef (x, b, t) -> + d, mkNamedLetIn x (put b) (put t) c + | Context.Named.Declaration.LocalAssum (x, t) -> + mkVar x :: d, mkNamedProd x (put t) c in + let a, t = + Context.Named.fold_inside abs_dc ~init:([], (put evi.evar_concl)) dc in + let m = Evarutil.new_meta () in + ise := meta_declare m t !ise; + sigma := Evd.define k (applist (mkMeta m, a)) !sigma; + put (existential_value !sigma ex) + end + | _ -> map_constr put c in + let c1 = put c0 in !ise, c1 + +(* Compile a match pattern from a term; t is the term to fill. *) +(* p_origin can be passed to obtain a better error message *) +let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p = + let k, f, a = + let f, a = Reductionops.whd_betaiota_stack ise p in + match kind_of_term f with + | Const (p,_) -> + let np = proj_nparams p in + if np = 0 || np > List.length a then KpatConst, f, a else + let a1, a2 = List.chop np a in KpatProj p, applist(f, a1), a2 + | Var _ | Ind _ | Construct _ -> KpatFixed, f, a + | Evar (k, _) -> + if Evd.mem sigma0 k then KpatEvar k, f, a else + if a <> [] then KpatFlex, f, a else + (match p_origin with None -> Errors.error "indeterminate pattern" + | Some (dir, rule) -> + errorstrm (str "indeterminate " ++ pr_dir_side dir + ++ str " in " ++ pr_constr_pat rule)) + | LetIn (_, v, _, b) -> + if b <> mkRel 1 then KpatLet, f, a else KpatFlex, v, a + | Lambda _ -> KpatLam, f, a + | _ -> KpatRigid, f, a in + let aa = Array.of_list a in + let ise', p' = evars_for_FO ~hack env sigma0 ise (mkApp (f, aa)) in + ise', + { up_k = k; up_FO = p'; up_f = f; + up_a = aa; up_ok = ok; up_dir = dir; up_t = t} + +(* Specialize a pattern after a successful match: assign a precise head *) +(* kind and arity for Proj and Flex patterns. *) +let ungen_upat lhs (sigma, uc, t) u = + let f, a = safeDestApp lhs in + let k = match kind_of_term f with + | Var _ | Ind _ | Construct _ -> KpatFixed + | Const _ -> KpatConst + | Evar (k, _) -> if is_defined sigma k then raise NoMatch else KpatEvar k + | LetIn _ -> KpatLet + | Lambda _ -> KpatLam + | _ -> KpatRigid in + sigma, uc, {u with up_k = k; up_FO = lhs; up_f = f; up_a = a; up_t = t} + +let nb_cs_proj_args pc f u = + let na k = + List.length (snd (lookup_canonical_conversion (ConstRef pc, k))).o_TCOMPS in + try match kind_of_term f with + | Prod _ -> na Prod_cs + | Sort s -> na (Sort_cs (family_of_sort s)) + | Const (c',_) when Constant.equal c' pc -> Array.length (snd (destApp u.up_f)) + | Var _ | Ind _ | Construct _ | Const _ -> na (Const_cs (global_of_constr f)) + | _ -> -1 + with Not_found -> -1 + +let isEvar_k k f = + match kind_of_term f with Evar (k', _) -> k = k' | _ -> false + +let nb_args c = + match kind_of_term c with App (_, a) -> Array.length a | _ -> 0 + +let mkSubArg i a = if i = Array.length a then a else Array.sub a 0 i +let mkSubApp f i a = if i = 0 then f else mkApp (f, mkSubArg i a) + +let splay_app ise = + let rec loop c a = match kind_of_term c with + | App (f, a') -> loop f (Array.append a' a) + | Cast (c', _, _) -> loop c' a + | Evar ex -> + (try loop (existential_value ise ex) a with _ -> c, a) + | _ -> c, a in + fun c -> match kind_of_term c with + | App (f, a) -> loop f a + | Cast _ | Evar _ -> loop c [| |] + | _ -> c, [| |] + +let filter_upat i0 f n u fpats = + let na = Array.length u.up_a in + if n < na then fpats else + let np = match u.up_k with + | KpatConst when Term.eq_constr u.up_f f -> na + | KpatFixed when Term.eq_constr u.up_f f -> na + | KpatEvar k when isEvar_k k f -> na + | KpatLet when isLetIn f -> na + | KpatLam when isLambda f -> na + | KpatRigid when isRigid f -> na + | KpatFlex -> na + | KpatProj pc -> + let np = na + nb_cs_proj_args pc f u in if n < np then -1 else np + | _ -> -1 in + if np < na then fpats else + let () = if !i0 < np then i0 := n in (u, np) :: fpats + +let filter_upat_FO i0 f n u fpats = + let np = nb_args u.up_FO in + if n < np then fpats else + let ok = match u.up_k with + | KpatConst -> Term.eq_constr u.up_f f + | KpatFixed -> Term.eq_constr u.up_f f + | KpatEvar k -> isEvar_k k f + | KpatLet -> isLetIn f + | KpatLam -> isLambda f + | KpatRigid -> isRigid f + | KpatProj pc -> Term.eq_constr f (mkConst pc) + | KpatFlex -> i0 := n; true in + if ok then begin if !i0 < np then i0 := np; (u, np) :: fpats end else fpats + +exception FoundUnif of (evar_map * evar_universe_context * tpattern) +(* Note: we don't update env as we descend into the term, as the primitive *) +(* unification procedure always rejects subterms with bound variables. *) + +let dont_impact_evars_in cl = + let evs_in_cl = Evd.evars_of_term cl in + fun sigma -> Evar.Set.for_all (fun k -> + try let _ = Evd.find_undefined sigma k in true + with Not_found -> false) evs_in_cl + +(* We are forced to duplicate code between the FO/HO matching because we *) +(* have to work around several kludges in unify.ml: *) +(* - w_unify drops into second-order unification when the pattern is an *) +(* application whose head is a meta. *) +(* - w_unify tries to unify types without subsumption when the pattern *) +(* head is an evar or meta (e.g., it fails on ?1 = nat when ?1 : Type). *) +(* - w_unify expands let-in (zeta conversion) eagerly, whereas we want to *) +(* match a head let rigidly. *) +let match_upats_FO upats env sigma0 ise orig_c = + let dont_impact_evars = dont_impact_evars_in orig_c in + let rec loop c = + let f, a = splay_app ise c in let i0 = ref (-1) in + let fpats = + List.fold_right (filter_upat_FO i0 f (Array.length a)) upats [] in + while !i0 >= 0 do + let i = !i0 in i0 := -1; + let c' = mkSubApp f i a in + let one_match (u, np) = + let skip = + if i <= np then i < np else + if u.up_k == KpatFlex then begin i0 := i - 1; false end else + begin if !i0 < np then i0 := np; true end in + if skip || not (closed0 c') then () else try + let _ = match u.up_k with + | KpatFlex -> + let kludge v = mkLambda (Anonymous, mkProp, v) in + unif_FO env ise (kludge u.up_FO) (kludge c') + | KpatLet -> + let kludge vla = + let vl, a = safeDestApp vla in + let x, v, t, b = destLetIn vl in + mkApp (mkLambda (x, t, b), Array.cons v a) in + unif_FO env ise (kludge u.up_FO) (kludge c') + | _ -> unif_FO env ise u.up_FO c' in + let ise' = (* Unify again using HO to assign evars *) + let p = mkApp (u.up_f, u.up_a) in + try unif_HO env ise p c' with _ -> raise NoMatch in + let lhs = mkSubApp f i a in + let pt' = unif_end env sigma0 ise' u.up_t (u.up_ok lhs) in + raise (FoundUnif (ungen_upat lhs pt' u)) + with FoundUnif (s,_,_) as sig_u when dont_impact_evars s -> raise sig_u + | Not_found -> Errors.anomaly (str"incomplete ise in match_upats_FO") + | _ -> () in + List.iter one_match fpats + done; + iter_constr_LR loop f; Array.iter loop a in + try loop orig_c with Invalid_argument _ -> Errors.anomaly (str"IN FO") + +let prof_FO = mk_profiler "match_upats_FO";; +let match_upats_FO upats env sigma0 ise c = + prof_FO.profile (match_upats_FO upats env sigma0) ise c +;; + + +let match_upats_HO ~on_instance upats env sigma0 ise c = + let dont_impact_evars = dont_impact_evars_in c in + let it_did_match = ref false in + let failed_because_of_TC = ref false in + let rec aux upats env sigma0 ise c = + let f, a = splay_app ise c in let i0 = ref (-1) in + let fpats = List.fold_right (filter_upat i0 f (Array.length a)) upats [] in + while !i0 >= 0 do + let i = !i0 in i0 := -1; + let one_match (u, np) = + let skip = + if i <= np then i < np else + if u.up_k == KpatFlex then begin i0 := i - 1; false end else + begin if !i0 < np then i0 := np; true end in + if skip then () else try + let ise' = match u.up_k with + | KpatFixed | KpatConst -> ise + | KpatEvar _ -> + let _, pka = destEvar u.up_f and _, ka = destEvar f in + unif_HO_args env ise pka 0 ka + | KpatLet -> + let x, v, t, b = destLetIn f in + let _, pv, _, pb = destLetIn u.up_f in + let ise' = unif_HO env ise pv v in + unif_HO + (Environ.push_rel (Context.Rel.Declaration.LocalAssum(x, t)) env) + ise' pb b + | KpatFlex | KpatProj _ -> + unif_HO env ise u.up_f (mkSubApp f (i - Array.length u.up_a) a) + | _ -> unif_HO env ise u.up_f f in + let ise'' = unif_HO_args env ise' u.up_a (i - Array.length u.up_a) a in + let lhs = mkSubApp f i a in + let pt' = unif_end env sigma0 ise'' u.up_t (u.up_ok lhs) in + on_instance (ungen_upat lhs pt' u) + with FoundUnif (s,_,_) as sig_u when dont_impact_evars s -> raise sig_u + | NoProgress -> it_did_match := true + | Pretype_errors.PretypeError + (_,_,Pretype_errors.UnsatisfiableConstraints _) -> + failed_because_of_TC:=true + | e when Errors.noncritical e -> () in + List.iter one_match fpats + done; + iter_constr_LR (aux upats env sigma0 ise) f; + Array.iter (aux upats env sigma0 ise) a + in + aux upats env sigma0 ise c; + if !it_did_match then raise NoProgress; + !failed_because_of_TC + +let prof_HO = mk_profiler "match_upats_HO";; +let match_upats_HO ~on_instance upats env sigma0 ise c = + prof_HO.profile (match_upats_HO ~on_instance upats env sigma0) ise c +;; + + +let fixed_upat = function +| {up_k = KpatFlex | KpatEvar _ | KpatProj _} -> false +| {up_t = t} -> not (occur_existential t) + +let do_once r f = match !r with Some _ -> () | None -> r := Some (f ()) + +let assert_done r = + match !r with Some x -> x | None -> Errors.anomaly (str"do_once never called") + +let assert_done_multires r = + match !r with + | None -> Errors.anomaly (str"do_once never called") + | Some (n, xs) -> + r := Some (n+1,xs); + try List.nth xs n with Failure _ -> raise NoMatch + +type subst = Environ.env -> Term.constr -> Term.constr -> int -> Term.constr +type find_P = + Environ.env -> Term.constr -> int -> + k:subst -> + Term.constr +type conclude = unit -> + Term.constr * ssrdir * (Evd.evar_map * Evd.evar_universe_context * Term.constr) + +(* upats_origin makes a better error message only *) +let mk_tpattern_matcher ?(all_instances=false) + ?(raise_NoMatch=false) ?upats_origin sigma0 occ (ise, upats) += + let nocc = ref 0 and skip_occ = ref false in + let use_occ, occ_list = match occ with + | Some (true, ol) -> ol = [], ol + | Some (false, ol) -> ol <> [], ol + | None -> false, [] in + let max_occ = List.fold_right max occ_list 0 in + let subst_occ = + let occ_set = Array.make max_occ (not use_occ) in + let _ = List.iter (fun i -> occ_set.(i - 1) <- use_occ) occ_list in + let _ = if max_occ = 0 then skip_occ := use_occ in + fun () -> incr nocc; + if !nocc = max_occ then skip_occ := use_occ; + if !nocc <= max_occ then occ_set.(!nocc - 1) else not use_occ in + let upat_that_matched = ref None in + let match_EQ env sigma u = + match u.up_k with + | KpatLet -> + let x, pv, t, pb = destLetIn u.up_f in + let env' = + Environ.push_rel (Context.Rel.Declaration.LocalAssum(x, t)) env in + let match_let f = match kind_of_term f with + | LetIn (_, v, _, b) -> unif_EQ env sigma pv v && unif_EQ env' sigma pb b + | _ -> false in match_let + | KpatFixed -> Term.eq_constr u.up_f + | KpatConst -> Term.eq_constr u.up_f + | KpatLam -> fun c -> + (match kind_of_term c with + | Lambda _ -> unif_EQ env sigma u.up_f c + | _ -> false) + | _ -> unif_EQ env sigma u.up_f in +let p2t p = mkApp(p.up_f,p.up_a) in +let source () = match upats_origin, upats with + | None, [p] -> + (if fixed_upat p then str"term " else str"partial term ") ++ + pr_constr_pat (p2t p) ++ spc() + | Some (dir,rule), [p] -> str"The " ++ pr_dir_side dir ++ str" of " ++ + pr_constr_pat rule ++ fnl() ++ ws 4 ++ pr_constr_pat (p2t p) ++ fnl() + | Some (dir,rule), _ -> str"The " ++ pr_dir_side dir ++ str" of " ++ + pr_constr_pat rule ++ spc() + | _, [] | None, _::_::_ -> + Errors.anomaly (str"mk_tpattern_matcher with no upats_origin") in +let on_instance, instances = + let instances = ref [] in + (fun x -> + if all_instances then instances := !instances @ [x] + else raise (FoundUnif x)), + (fun () -> !instances) in +let rec uniquize = function + | [] -> [] + | (sigma,_,{ up_f = f; up_a = a; up_t = t } as x) :: xs -> + let t = Reductionops.nf_evar sigma t in + let f = Reductionops.nf_evar sigma f in + let a = Array.map (Reductionops.nf_evar sigma) a in + let neq (sigma1,_,{ up_f = f1; up_a = a1; up_t = t1 }) = + let t1 = Reductionops.nf_evar sigma1 t1 in + let f1 = Reductionops.nf_evar sigma1 f1 in + let a1 = Array.map (Reductionops.nf_evar sigma1) a1 in + not (Term.eq_constr t t1 && + Term.eq_constr f f1 && CArray.for_all2 Term.eq_constr a a1) in + x :: uniquize (List.filter neq xs) in + +((fun env c h ~k -> + do_once upat_that_matched (fun () -> + let failed_because_of_TC = ref false in + try + if not all_instances then match_upats_FO upats env sigma0 ise c; + failed_because_of_TC:=match_upats_HO ~on_instance upats env sigma0 ise c; + raise NoMatch + with FoundUnif sigma_u -> 0,[sigma_u] + | (NoMatch|NoProgress) when all_instances && instances () <> [] -> + 0, uniquize (instances ()) + | NoMatch when (not raise_NoMatch) -> + if !failed_because_of_TC then + errorstrm (source ()++strbrk"matches but type classes inference fails") + else + errorstrm (source () ++ str "does not match any subterm of the goal") + | NoProgress when (not raise_NoMatch) -> + let dir = match upats_origin with Some (d,_) -> d | _ -> + Errors.anomaly (str"mk_tpattern_matcher with no upats_origin") in + errorstrm (str"all matches of "++source()++ + str"are equal to the " ++ pr_dir_side (inv_dir dir)) + | NoProgress -> raise NoMatch); + let sigma, _, ({up_f = pf; up_a = pa} as u) = + if all_instances then assert_done_multires upat_that_matched + else List.hd (snd(assert_done upat_that_matched)) in +(* pp(lazy(str"sigma@tmatch=" ++ pr_evar_map None sigma)); *) + if !skip_occ then ((*ignore(k env u.up_t 0);*) c) else + let match_EQ = match_EQ env sigma u in + let pn = Array.length pa in + let rec subst_loop (env,h as acc) c' = + if !skip_occ then c' else + let f, a = splay_app sigma c' in + if Array.length a >= pn && match_EQ f && unif_EQ_args env sigma pa a then + let a1, a2 = Array.chop (Array.length pa) a in + let fa1 = mkApp (f, a1) in + let f' = if subst_occ () then k env u.up_t fa1 h else fa1 in + mkApp (f', Array.map_left (subst_loop acc) a2) + else + (* TASSI: clear letin values to avoid unfolding *) + let inc_h rd (env,h') = + let ctx_item = + match rd with + | Context.Rel.Declaration.LocalAssum _ as x -> x + | Context.Rel.Declaration.LocalDef (x,_,y) -> + Context.Rel.Declaration.LocalAssum(x,y) in + Environ.push_rel ctx_item env, h' + 1 in + let f' = map_constr_with_binders_left_to_right inc_h subst_loop acc f in + mkApp (f', Array.map_left (subst_loop acc) a) in + subst_loop (env,h) c) : find_P), +((fun () -> + let sigma, uc, ({up_f = pf; up_a = pa} as u) = + match !upat_that_matched with + | Some (_,x) -> List.hd x | None when raise_NoMatch -> raise NoMatch + | None -> Errors.anomaly (str"companion function never called") in + let p' = mkApp (pf, pa) in + if max_occ <= !nocc then p', u.up_dir, (sigma, uc, u.up_t) + else errorstrm (str"Only " ++ int !nocc ++ str" < " ++ int max_occ ++ + str(String.plural !nocc " occurence") ++ match upats_origin with + | None -> str" of" ++ spc() ++ pr_constr_pat p' + | Some (dir,rule) -> str" of the " ++ pr_dir_side dir ++ fnl() ++ + ws 4 ++ pr_constr_pat p' ++ fnl () ++ + str"of " ++ pr_constr_pat rule)) : conclude) + +type ('ident, 'term) ssrpattern = + | T of 'term + | In_T of 'term + | X_In_T of 'ident * 'term + | In_X_In_T of 'ident * 'term + | E_In_X_In_T of 'term * 'ident * 'term + | E_As_X_In_T of 'term * 'ident * 'term + +let pr_pattern = function + | T t -> prl_term t + | In_T t -> str "in " ++ prl_term t + | X_In_T (x,t) -> prl_term x ++ str " in " ++ prl_term t + | In_X_In_T (x,t) -> str "in " ++ prl_term x ++ str " in " ++ prl_term t + | E_In_X_In_T (e,x,t) -> + prl_term e ++ str " in " ++ prl_term x ++ str " in " ++ prl_term t + | E_As_X_In_T (e,x,t) -> + prl_term e ++ str " as " ++ prl_term x ++ str " in " ++ prl_term t + +let pr_pattern_w_ids = function + | T t -> prl_term t + | In_T t -> str "in " ++ prl_term t + | X_In_T (x,t) -> pr_id x ++ str " in " ++ prl_term t + | In_X_In_T (x,t) -> str "in " ++ pr_id x ++ str " in " ++ prl_term t + | E_In_X_In_T (e,x,t) -> + prl_term e ++ str " in " ++ pr_id x ++ str " in " ++ prl_term t + | E_As_X_In_T (e,x,t) -> + prl_term e ++ str " as " ++ pr_id x ++ str " in " ++ prl_term t + +let pr_pattern_aux pr_constr = function + | T t -> pr_constr t + | In_T t -> str "in " ++ pr_constr t + | X_In_T (x,t) -> pr_constr x ++ str " in " ++ pr_constr t + | In_X_In_T (x,t) -> str "in " ++ pr_constr x ++ str " in " ++ pr_constr t + | E_In_X_In_T (e,x,t) -> + pr_constr e ++ str " in " ++ pr_constr x ++ str " in " ++ pr_constr t + | E_As_X_In_T (e,x,t) -> + pr_constr e ++ str " as " ++ pr_constr x ++ str " in " ++ pr_constr t +let pp_pattern (sigma, p) = + pr_pattern_aux (fun t -> pr_constr_pat (pi3 (nf_open_term sigma sigma t))) p +let pr_cpattern = pr_term +let pr_rpattern _ _ _ = pr_pattern + +let pr_option f = function None -> mt() | Some x -> f x +let pr_ssrpattern _ _ _ = pr_option pr_pattern +let pr_pattern_squarep = pr_option (fun r -> str "[" ++ pr_pattern r ++ str "]") +let pr_ssrpattern_squarep _ _ _ = pr_pattern_squarep +let pr_pattern_roundp = pr_option (fun r -> str "(" ++ pr_pattern r ++ str ")") +let pr_ssrpattern_roundp _ _ _ = pr_pattern_roundp + +let wit_rpatternty = add_genarg "rpatternty" pr_pattern + +let glob_ssrterm gs = function + | k, (_, Some c) as x -> k, + let x = Tacintern.intern_constr gs c in + fst x, Some c + | ct -> ct + +let glob_rpattern s p = + match p with + | T t -> T (glob_ssrterm s t) + | In_T t -> In_T (glob_ssrterm s t) + | X_In_T(x,t) -> X_In_T (x,glob_ssrterm s t) + | In_X_In_T(x,t) -> In_X_In_T (x,glob_ssrterm s t) + | E_In_X_In_T(e,x,t) -> E_In_X_In_T (glob_ssrterm s e,x,glob_ssrterm s t) + | E_As_X_In_T(e,x,t) -> E_As_X_In_T (glob_ssrterm s e,x,glob_ssrterm s t) + +let subst_ssrterm s (k, c) = k, Tacsubst.subst_glob_constr_and_expr s c + +let subst_rpattern s = function + | T t -> T (subst_ssrterm s t) + | In_T t -> In_T (subst_ssrterm s t) + | X_In_T(x,t) -> X_In_T (x,subst_ssrterm s t) + | In_X_In_T(x,t) -> In_X_In_T (x,subst_ssrterm s t) + | E_In_X_In_T(e,x,t) -> E_In_X_In_T (subst_ssrterm s e,x,subst_ssrterm s t) + | E_As_X_In_T(e,x,t) -> E_As_X_In_T (subst_ssrterm s e,x,subst_ssrterm s t) + +ARGUMENT EXTEND rpattern + TYPED AS rpatternty + PRINTED BY pr_rpattern + GLOBALIZED BY glob_rpattern + SUBSTITUTED BY subst_rpattern + | [ lconstr(c) ] -> [ T (mk_lterm c) ] + | [ "in" lconstr(c) ] -> [ In_T (mk_lterm c) ] + | [ lconstr(x) "in" lconstr(c) ] -> + [ X_In_T (mk_lterm x, mk_lterm c) ] + | [ "in" lconstr(x) "in" lconstr(c) ] -> + [ In_X_In_T (mk_lterm x, mk_lterm c) ] + | [ lconstr(e) "in" lconstr(x) "in" lconstr(c) ] -> + [ E_In_X_In_T (mk_lterm e, mk_lterm x, mk_lterm c) ] + | [ lconstr(e) "as" lconstr(x) "in" lconstr(c) ] -> + [ E_As_X_In_T (mk_lterm e, mk_lterm x, mk_lterm c) ] +END + + + +type cpattern = char * glob_constr_and_expr +let tag_of_cpattern = fst +let loc_of_cpattern = loc_ofCG +let cpattern_of_term t = t +type occ = (bool * int list) option + +type rpattern = (cpattern, cpattern) ssrpattern +let pr_rpattern = pr_pattern + +type pattern = Evd.evar_map * (Term.constr, Term.constr) ssrpattern + + +let id_of_cpattern = function + | _,(_,Some (CRef (Ident (_, x), _))) -> Some x + | _,(_,Some (CAppExpl (_, (_, Ident (_, x), _), []))) -> Some x + | _,(GRef (_, VarRef x, _) ,None) -> Some x + | _ -> None +let id_of_Cterm t = match id_of_cpattern t with + | Some x -> x + | None -> loc_error (loc_of_cpattern t) "Only identifiers are allowed here" + +let of_ftactic ftac gl = + let r = ref None in + let tac = Ftactic.run ftac (fun ans -> r := Some ans; Proofview.tclUNIT ()) in + let tac = Proofview.V82.of_tactic tac in + let { sigma = sigma } = tac gl in + let ans = match !r with + | None -> assert false (** If the tactic failed we should not reach this point *) + | Some ans -> ans + in + (sigma, ans) + +let interp_wit wit ist gl x = + let globarg = in_gen (glbwit wit) x in + let arg = interp_genarg ist globarg in + let (sigma, arg) = of_ftactic arg gl in + sigma, Value.cast (topwit wit) arg +let interp_constr = interp_wit wit_constr +let interp_open_constr ist gl gc = + interp_wit wit_open_constr ist gl gc +let pf_intern_term ist gl (_, c) = glob_constr ist (pf_env gl) c +let interp_term ist gl (_, c) = (interp_open_constr ist gl c) +let pr_ssrterm _ _ _ = pr_term +let input_ssrtermkind strm = match Compat.get_tok (stream_nth 0 strm) with + | Tok.KEYWORD "(" -> '(' + | Tok.KEYWORD "@" -> '@' + | _ -> ' ' +let ssrtermkind = Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind + +(* This piece of code asserts the following notations are reserved *) +(* Reserved Notation "( a 'in' b )" (at level 0). *) +(* Reserved Notation "( a 'as' b )" (at level 0). *) +(* Reserved Notation "( a 'in' b 'in' c )" (at level 0). *) +(* Reserved Notation "( a 'as' b 'in' c )" (at level 0). *) +let glob_cpattern gs p = + pp(lazy(str"globbing pattern: " ++ pr_term p)); + let glob x = snd (glob_ssrterm gs (mk_lterm x)) in + let encode k s l = + let name = Name (id_of_string ("_ssrpat_" ^ s)) in + k, (mkRCast mkRHole (mkRLambda name mkRHole (mkRApp mkRHole l)), None) in + let bind_in t1 t2 = + let d = dummy_loc in let n = Name (destCVar t1) in + fst (glob (mkCCast d (mkCHole d) (mkCLambda d n (mkCHole d) t2))) in + let check_var t2 = if not (isCVar t2) then + loc_error (constr_loc t2) "Only identifiers are allowed here" in + match p with + | _, (_, None) as x -> x + | k, (v, Some t) as orig -> + if k = 'x' then glob_ssrterm gs ('(', (v, Some t)) else + match t with + | CNotation(_, "( _ in _ )", ([t1; t2], [], [])) -> + (try match glob t1, glob t2 with + | (r1, None), (r2, None) -> encode k "In" [r1;r2] + | (r1, Some _), (r2, Some _) when isCVar t1 -> + encode k "In" [r1; r2; bind_in t1 t2] + | (r1, Some _), (r2, Some _) -> encode k "In" [r1; r2] + | _ -> Errors.anomaly (str"where are we?") + with _ when isCVar t1 -> encode k "In" [bind_in t1 t2]) + | CNotation(_, "( _ in _ in _ )", ([t1; t2; t3], [], [])) -> + check_var t2; encode k "In" [fst (glob t1); bind_in t2 t3] + | CNotation(_, "( _ as _ )", ([t1; t2], [], [])) -> + encode k "As" [fst (glob t1); fst (glob t2)] + | CNotation(_, "( _ as _ in _ )", ([t1; t2; t3], [], [])) -> + check_var t2; encode k "As" [fst (glob t1); bind_in t2 t3] + | _ -> glob_ssrterm gs orig +;; + +let interp_ssrterm _ gl t = Tacmach.project gl, t + +ARGUMENT EXTEND cpattern + PRINTED BY pr_ssrterm + INTERPRETED BY interp_ssrterm + GLOBALIZED BY glob_cpattern SUBSTITUTED BY subst_ssrterm + RAW_TYPED AS cpattern RAW_PRINTED BY pr_ssrterm + GLOB_TYPED AS cpattern GLOB_PRINTED BY pr_ssrterm +| [ "Qed" constr(c) ] -> [ mk_lterm c ] +END + +let (!@) = Compat.to_coqloc + +GEXTEND Gram + GLOBAL: cpattern; + cpattern: [[ k = ssrtermkind; c = constr -> + let pattern = mk_term k c in + if loc_ofCG pattern <> !@loc && k = '(' then mk_term 'x' c else pattern ]]; +END + +ARGUMENT EXTEND lcpattern + TYPED AS cpattern + PRINTED BY pr_ssrterm + INTERPRETED BY interp_ssrterm + GLOBALIZED BY glob_cpattern SUBSTITUTED BY subst_ssrterm + RAW_TYPED AS cpattern RAW_PRINTED BY pr_ssrterm + GLOB_TYPED AS cpattern GLOB_PRINTED BY pr_ssrterm +| [ "Qed" lconstr(c) ] -> [ mk_lterm c ] +END + +GEXTEND Gram + GLOBAL: lcpattern; + lcpattern: [[ k = ssrtermkind; c = lconstr -> + let pattern = mk_term k c in + if loc_ofCG pattern <> !@loc && k = '(' then mk_term 'x' c else pattern ]]; +END + +let thin id sigma goal = + let ids = Id.Set.singleton id in + let env = Goal.V82.env sigma goal in + let cl = Goal.V82.concl sigma goal in + let evdref = ref (Evd.clear_metas sigma) in + let ans = + try Some (Evarutil.clear_hyps_in_evi env evdref (Environ.named_context_val env) cl ids) + with Evarutil.ClearDependencyError _ -> None + in + match ans with + | None -> sigma + | Some (hyps, concl) -> + let sigma = !evdref in + let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in + let sigma = Goal.V82.partial_solution_to sigma goal gl ev in + sigma + +let pr_ist { lfun= lfun } = + prlist_with_sep spc + (fun (id, Geninterp.Val.Dyn(ty,_)) -> + pr_id id ++ str":" ++ Geninterp.Val.pr ty) (Id.Map.bindings lfun) + +let interp_pattern ?wit_ssrpatternarg ist gl red redty = + pp(lazy(str"interpreting: " ++ pr_pattern red)); + pp(lazy(str" in ist: " ++ pr_ist ist)); + let xInT x y = X_In_T(x,y) and inXInT x y = In_X_In_T(x,y) in + let inT x = In_T x and eInXInT e x t = E_In_X_In_T(e,x,t) in + let eAsXInT e x t = E_As_X_In_T(e,x,t) in + let mkG ?(k=' ') x = k,(x,None) in + let decode ist t ?reccall f g = + try match (pf_intern_term ist gl t) with + | GCast(_,GHole _,CastConv(GLambda(_,Name x,_,_,c))) -> f x (' ',(c,None)) + | GVar(_,id) + when Id.Map.mem id ist.lfun && + not(Option.is_empty reccall) && + not(Option.is_empty wit_ssrpatternarg) -> + let v = Id.Map.find id ist.lfun in + Option.get reccall + (Value.cast (topwit (Option.get wit_ssrpatternarg)) v) + | it -> g t with e when Errors.noncritical e -> g t in + let decodeG t f g = decode ist (mkG t) f g in + let bad_enc id _ = Errors.anomaly (str"bad encoding for pattern "++str id) in + let cleanup_XinE h x rp sigma = + let h_k = match kind_of_term h with Evar (k,_) -> k | _ -> assert false in + let to_clean, update = (* handle rename if x is already used *) + let ctx = pf_hyps gl in + let len = Context.Named.length ctx in + let name = ref None in + try ignore(Context.Named.lookup x ctx); (name, fun k -> + if !name = None then + let nctx = Evd.evar_context (Evd.find sigma k) in + let nlen = Context.Named.length nctx in + if nlen > len then begin + name := Some (Context.Named.Declaration.get_id (List.nth nctx (nlen - len - 1))) + end) + with Not_found -> ref (Some x), fun _ -> () in + let sigma0 = project gl in + let new_evars = + let rec aux acc t = match kind_of_term t with + | Evar (k,_) -> + if k = h_k || List.mem k acc || Evd.mem sigma0 k then acc else + (update k; k::acc) + | _ -> fold_constr aux acc t in + aux [] (Evarutil.nf_evar sigma rp) in + let sigma = + List.fold_left (fun sigma e -> + if Evd.is_defined sigma e then sigma else (* clear may be recursive *) + if Option.is_empty !to_clean then sigma else + let name = Option.get !to_clean in + pp(lazy(pr_id name)); + thin name sigma e) + sigma new_evars in + sigma in + let red = let rec decode_red (ist,red) = match red with + | T(k,(GCast (_,GHole _,(CastConv(GLambda (_,Name id,_,_,t)))),None)) + when let id = string_of_id id in let len = String.length id in + (len > 8 && String.sub id 0 8 = "_ssrpat_") -> + let id = string_of_id id in let len = String.length id in + (match String.sub id 8 (len - 8), t with + | "In", GApp(_, _, [t]) -> decodeG t xInT (fun x -> T x) + | "In", GApp(_, _, [e; t]) -> decodeG t (eInXInT (mkG e)) (bad_enc id) + | "In", GApp(_, _, [e; t; e_in_t]) -> + decodeG t (eInXInT (mkG e)) + (fun _ -> decodeG e_in_t xInT (fun _ -> assert false)) + | "As", GApp(_, _, [e; t]) -> decodeG t (eAsXInT (mkG e)) (bad_enc id) + | _ -> bad_enc id ()) + | T t -> decode ist ~reccall:decode_red t xInT (fun x -> T x) + | In_T t -> decode ist t inXInT inT + | X_In_T (e,t) -> decode ist t (eInXInT e) (fun x -> xInT (id_of_Cterm e) x) + | In_X_In_T (e,t) -> inXInT (id_of_Cterm e) t + | E_In_X_In_T (e,x,rp) -> eInXInT e (id_of_Cterm x) rp + | E_As_X_In_T (e,x,rp) -> eAsXInT e (id_of_Cterm x) rp in + decode_red (ist,red) in + pp(lazy(str"decoded as: " ++ pr_pattern_w_ids red)); + let red = match redty with None -> red | Some ty -> let ty = ' ', ty in + match red with + | T t -> T (combineCG t ty (mkCCast (loc_ofCG t)) mkRCast) + | X_In_T (x,t) -> + let ty = pf_intern_term ist gl ty in + E_As_X_In_T (mkG (mkRCast mkRHole ty), x, t) + | E_In_X_In_T (e,x,t) -> + let ty = mkG (pf_intern_term ist gl ty) in + E_In_X_In_T (combineCG e ty (mkCCast (loc_ofCG t)) mkRCast, x, t) + | E_As_X_In_T (e,x,t) -> + let ty = mkG (pf_intern_term ist gl ty) in + E_As_X_In_T (combineCG e ty (mkCCast (loc_ofCG t)) mkRCast, x, t) + | red -> red in + pp(lazy(str"typed as: " ++ pr_pattern_w_ids red)); + let mkXLetIn loc x (a,(g,c)) = match c with + | Some b -> a,(g,Some (mkCLetIn loc x (mkCHole loc) b)) + | None -> a,(GLetIn (loc,x,(GHole (loc, BinderType x, IntroAnonymous, None)), g), None) in + match red with + | T t -> let sigma, t = interp_term ist gl t in sigma, T t + | In_T t -> let sigma, t = interp_term ist gl t in sigma, In_T t + | X_In_T (x, rp) | In_X_In_T (x, rp) -> + let mk x p = match red with X_In_T _ -> X_In_T(x,p) | _ -> In_X_In_T(x,p) in + let rp = mkXLetIn dummy_loc (Name x) rp in + let sigma, rp = interp_term ist gl rp in + let _, h, _, rp = destLetIn rp in + let sigma = cleanup_XinE h x rp sigma in + let rp = subst1 h (Evarutil.nf_evar sigma rp) in + sigma, mk h rp + | E_In_X_In_T(e, x, rp) | E_As_X_In_T (e, x, rp) -> + let mk e x p = + match red with E_In_X_In_T _ ->E_In_X_In_T(e,x,p)|_->E_As_X_In_T(e,x,p) in + let rp = mkXLetIn dummy_loc (Name x) rp in + let sigma, rp = interp_term ist gl rp in + let _, h, _, rp = destLetIn rp in + let sigma = cleanup_XinE h x rp sigma in + let rp = subst1 h (Evarutil.nf_evar sigma rp) in + let sigma, e = interp_term ist (re_sig (sig_it gl) sigma) e in + sigma, mk e h rp +;; +let interp_cpattern ist gl red redty = interp_pattern ist gl (T red) redty;; +let interp_rpattern ~wit_ssrpatternarg ist gl red = interp_pattern ~wit_ssrpatternarg ist gl red None;; + +let id_of_pattern = function + | _, T t -> (match kind_of_term t with Var id -> Some id | _ -> None) + | _ -> None + +(* The full occurrence set *) +let noindex = Some(false,[]) + +(* calls do_subst on every sub-term identified by (pattern,occ) *) +let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = + let fs sigma x = Reductionops.nf_evar sigma x in + let pop_evar sigma e p = + let { Evd.evar_body = e_body } as e_def = Evd.find sigma e in + let e_body = match e_body with Evar_defined c -> c + | _ -> errorstrm (str "Matching the pattern " ++ pr_constr p ++ + str " did not instantiate ?" ++ int (Evar.repr e) ++ spc () ++ + str "Does the variable bound by the \"in\" construct occur "++ + str "in the pattern?") in + let sigma = + Evd.add (Evd.remove sigma e) e {e_def with Evd.evar_body = Evar_empty} in + sigma, e_body in + let ex_value hole = + match kind_of_term hole with Evar (e,_) -> e | _ -> assert false in + let mk_upat_for ?hack env sigma0 (sigma, t) ?(p=t) ok = + let sigma,pat= mk_tpattern ?hack env sigma0 (sigma,p) ok L2R (fs sigma t) in + sigma, [pat] in + match pattern with + | None -> do_subst env0 concl0 concl0 1 + | Some (sigma, (T rp | In_T rp)) -> + let rp = fs sigma rp in + let ise = create_evar_defs sigma in + let occ = match pattern with Some (_, T _) -> occ | _ -> noindex in + let rp = mk_upat_for env0 sigma0 (ise, rp) all_ok in + let find_T, end_T = mk_tpattern_matcher ?raise_NoMatch sigma0 occ rp in + let concl = find_T env0 concl0 1 do_subst in + let _ = end_T () in + concl + | Some (sigma, (X_In_T (hole, p) | In_X_In_T (hole, p))) -> + let p = fs sigma p in + let occ = match pattern with Some (_, X_In_T _) -> occ | _ -> noindex in + let ex = ex_value hole in + let rp = mk_upat_for ~hack:true env0 sigma0 (sigma, p) all_ok in + let find_T, end_T = mk_tpattern_matcher sigma0 noindex rp in + (* we start from sigma, so hole is considered a rigid head *) + let holep = mk_upat_for env0 sigma (sigma, hole) all_ok in + let find_X, end_X = mk_tpattern_matcher ?raise_NoMatch sigma occ holep in + let concl = find_T env0 concl0 1 (fun env c _ h -> + let p_sigma = unify_HO env (create_evar_defs sigma) c p in + let sigma, e_body = pop_evar p_sigma ex p in + fs p_sigma (find_X env (fs sigma p) h + (fun env _ -> do_subst env e_body))) in + let _ = end_X () in let _ = end_T () in + concl + | Some (sigma, E_In_X_In_T (e, hole, p)) -> + let p, e = fs sigma p, fs sigma e in + let ex = ex_value hole in + let rp = mk_upat_for ~hack:true env0 sigma0 (sigma, p) all_ok in + let find_T, end_T = mk_tpattern_matcher sigma0 noindex rp in + let holep = mk_upat_for env0 sigma (sigma, hole) all_ok in + let find_X, end_X = mk_tpattern_matcher sigma noindex holep in + let re = mk_upat_for env0 sigma0 (sigma, e) all_ok in + let find_E, end_E = mk_tpattern_matcher ?raise_NoMatch sigma0 occ re in + let concl = find_T env0 concl0 1 (fun env c _ h -> + let p_sigma = unify_HO env (create_evar_defs sigma) c p in + let sigma, e_body = pop_evar p_sigma ex p in + fs p_sigma (find_X env (fs sigma p) h (fun env c _ h -> + find_E env e_body h do_subst))) in + let _ = end_E () in let _ = end_X () in let _ = end_T () in + concl + | Some (sigma, E_As_X_In_T (e, hole, p)) -> + let p, e = fs sigma p, fs sigma e in + let ex = ex_value hole in + let rp = + let e_sigma = unify_HO env0 sigma hole e in + e_sigma, fs e_sigma p in + let rp = mk_upat_for ~hack:true env0 sigma0 rp all_ok in + let find_TE, end_TE = mk_tpattern_matcher sigma0 noindex rp in + let holep = mk_upat_for env0 sigma (sigma, hole) all_ok in + let find_X, end_X = mk_tpattern_matcher sigma occ holep in + let concl = find_TE env0 concl0 1 (fun env c _ h -> + let p_sigma = unify_HO env (create_evar_defs sigma) c p in + let sigma, e_body = pop_evar p_sigma ex p in + fs p_sigma (find_X env (fs sigma p) h (fun env c _ h -> + let e_sigma = unify_HO env sigma e_body e in + let e_body = fs e_sigma e in + do_subst env e_body e_body h))) in + let _ = end_X () in let _ = end_TE () in + concl +;; + +let redex_of_pattern ?(resolve_typeclasses=false) env (sigma, p) = + let e = match p with + | In_T _ | In_X_In_T _ -> Errors.anomaly (str"pattern without redex") + | T e | X_In_T (e, _) | E_As_X_In_T (e, _, _) | E_In_X_In_T (e, _, _) -> e in + let sigma = + if not resolve_typeclasses then sigma + else Typeclasses.resolve_typeclasses ~fail:false env sigma in + Reductionops.nf_evar sigma e, Evd.evar_universe_context sigma + +let fill_occ_pattern ?raise_NoMatch env sigma cl pat occ h = + let do_make_rel, occ = + if occ = Some(true,[]) then false, Some(false,[1]) else true, occ in + let find_R, conclude = + let r = ref None in + (fun env c _ h' -> + do_once r (fun () -> c, Evd.empty_evar_universe_context); + if do_make_rel then mkRel (h'+h-1) else c), + (fun _ -> if !r = None then redex_of_pattern env pat else assert_done r) in + let cl = eval_pattern ?raise_NoMatch env sigma cl (Some pat) occ find_R in + let e = conclude cl in + e, cl +;; + +(* clenup interface for external use *) +let mk_tpattern ?p_origin env sigma0 sigma_t f dir c = + mk_tpattern ?p_origin env sigma0 sigma_t f dir c +;; + +let pf_fill_occ env concl occ sigma0 p (sigma, t) ok h = + let ise = create_evar_defs sigma in + let ise, u = mk_tpattern env sigma0 (ise,t) ok L2R p in + let find_U, end_U = + mk_tpattern_matcher ~raise_NoMatch:true sigma0 occ (ise,[u]) in + let concl = find_U env concl h (fun _ _ _ -> mkRel) in + let rdx, _, (sigma, uc, p) = end_U () in + sigma, uc, p, concl, rdx + +let fill_occ_term env cl occ sigma0 (sigma, t) = + try + let sigma',uc,t',cl,_= pf_fill_occ env cl occ sigma0 t (sigma, t) all_ok 1 in + if sigma' != sigma0 then Errors.error "matching impacts evars" + else cl, (Evd.merge_universe_context sigma' uc, t') + with NoMatch -> try + let sigma', uc, t' = + unif_end env sigma0 (create_evar_defs sigma) t (fun _ -> true) in + if sigma' != sigma0 then raise NoMatch + else cl, (Evd.merge_universe_context sigma' uc, t') + with _ -> + errorstrm (str "partial term " ++ pr_constr_pat t + ++ str " does not match any subterm of the goal") + +let pf_fill_occ_term gl occ t = + let sigma0 = project gl and env = pf_env gl and concl = pf_concl gl in + let cl,(_,t) = fill_occ_term env concl occ sigma0 t in + cl, t + +let cpattern_of_id id = ' ', (GRef (dummy_loc, VarRef id, None), None) + +let is_wildcard = function + | _,(_,Some (CHole _)|GHole _,None) -> true + | _ -> false + +(* "ssrpattern" *) +let pr_ssrpatternarg _ _ _ (_,cpat) = pr_rpattern cpat +let pr_ssrpatternarg_glob _ _ _ cpat = pr_rpattern cpat +let interp_ssrpatternarg ist gl p = project gl, (ist, p) + +ARGUMENT EXTEND ssrpatternarg + PRINTED BY pr_ssrpatternarg + INTERPRETED BY interp_ssrpatternarg + GLOBALIZED BY glob_rpattern + RAW_PRINTED BY pr_ssrpatternarg_glob + GLOB_PRINTED BY pr_ssrpatternarg_glob +| [ rpattern(pat) ] -> [ pat ] +END + +let pf_merge_uc uc gl = + re_sig (sig_it gl) (Evd.merge_universe_context (project gl) uc) + +let pf_unsafe_merge_uc uc gl = + re_sig (sig_it gl) (Evd.set_universe_context (project gl) uc) + +let interp_rpattern ist gl red = interp_rpattern ~wit_ssrpatternarg ist gl red + +let ssrpatterntac _ist (arg_ist,arg) gl = + let pat = interp_rpattern arg_ist gl arg in + let sigma0 = project gl in + let concl0 = pf_concl gl in + let (t, uc), concl_x = + fill_occ_pattern (Global.env()) sigma0 concl0 pat noindex 1 in + let gl, tty = pf_type_of gl t in + let concl = mkLetIn (Name (id_of_string "selected"), t, tty, concl_x) in + Proofview.V82.of_tactic (convert_concl concl DEFAULTcast) gl + +(* Register "ssrpattern" tactic *) +let () = + let mltac _ ist = + let arg = + let v = Id.Map.find (Names.Id.of_string "pattern") ist.lfun in + Value.cast (topwit wit_ssrpatternarg) v in + Proofview.V82.tactic (ssrpatterntac ist arg) in + let name = { mltac_plugin = "ssrmatching_plugin"; mltac_tactic = "ssrpattern"; } in + let () = Tacenv.register_ml_tactic name [|mltac|] in + let tac = + TacFun ([Some (Id.of_string "pattern")], + TacML (Loc.ghost, { mltac_name = name; mltac_index = 0 }, [])) in + let obj () = + Tacenv.register_ltac true false (Id.of_string "ssrpattern") tac in + Mltop.declare_cache_obj obj "ssrmatching_plugin" + +let ssrinstancesof ist arg gl = + let ok rhs lhs ise = true in +(* not (Term.eq_constr lhs (Evarutil.nf_evar ise rhs)) in *) + let env, sigma, concl = pf_env gl, project gl, pf_concl gl in + let sigma0, cpat = interp_cpattern ist gl arg None in + let pat = match cpat with T x -> x | _ -> errorstrm (str"Not supported") in + let etpat, tpat = mk_tpattern env sigma (sigma0,pat) (ok pat) L2R pat in + let find, conclude = + mk_tpattern_matcher ~all_instances:true ~raise_NoMatch:true + sigma None (etpat,[tpat]) in + let print env p c _ = ppnl (hov 1 (str"instance:" ++ spc() ++ pr_constr p ++ spc() ++ str "matches:" ++ spc() ++ pr_constr c)); c in + ppnl (str"BEGIN INSTANCES"); + try + while true do + ignore(find env concl 1 ~k:print) + done; raise NoMatch + with NoMatch -> ppnl (str"END INSTANCES"); tclIDTAC gl + +TACTIC EXTEND ssrinstoftpat +| [ "ssrinstancesoftpat" cpattern(arg) ] -> [ Proofview.V82.tactic (ssrinstancesof ist arg) ] +END + +(* We wipe out all the keywords generated by the grammar rules we defined. *) +(* The user is supposed to Require Import ssreflect or Require ssreflect *) +(* and Import ssreflect.SsrSyntax to obtain these keywords and as a *) +(* consequence the extended ssreflect grammar. *) +let () = CLexer.unfreeze frozen_lexer ;; + +(* vim: set filetype=ocaml foldmethod=marker: *) diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli new file mode 100644 index 0000000000..74a603e51c --- /dev/null +++ b/plugins/ssrmatching/ssrmatching.mli @@ -0,0 +1,241 @@ +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) + +open Genarg +open Tacexpr +open Environ +open Tacmach +open Evd +open Proof_type +open Term + +(** ******** Small Scale Reflection pattern matching facilities ************* *) + +(** Pattern parsing *) + +(** The type of context patterns, the patterns of the [set] tactic and + [:] tactical. These are patterns that identify a precise subterm. *) +type cpattern +val pr_cpattern : cpattern -> Pp.std_ppcmds + +(** CS cpattern: (f _), (X in t), (t in X in t), (t as X in t) *) +val cpattern : cpattern Pcoq.Gram.entry +val wit_cpattern : cpattern uniform_genarg_type + +(** OS cpattern: f _, (X in t), (t in X in t), (t as X in t) *) +val lcpattern : cpattern Pcoq.Gram.entry +val wit_lcpattern : cpattern uniform_genarg_type + +(** The type of rewrite patterns, the patterns of the [rewrite] tactic. + These patterns also include patterns that identify all the subterms + of a context (i.e. "in" prefix) *) +type rpattern +val pr_rpattern : rpattern -> Pp.std_ppcmds + +(** OS rpattern: f _, in t, X in t, in X in t, t in X in t, t as X in t *) +val rpattern : rpattern Pcoq.Gram.entry +val wit_rpattern : rpattern uniform_genarg_type + +(** Pattern interpretation and matching *) + +exception NoMatch +exception NoProgress + +(** AST for [rpattern] (and consequently [cpattern]) *) +type ('ident, 'term) ssrpattern = + | T of 'term + | In_T of 'term + | X_In_T of 'ident * 'term + | In_X_In_T of 'ident * 'term + | E_In_X_In_T of 'term * 'ident * 'term + | E_As_X_In_T of 'term * 'ident * 'term + +type pattern = evar_map * (constr, constr) ssrpattern +val pp_pattern : pattern -> Pp.std_ppcmds + +(** Extracts the redex and applies to it the substitution part of the pattern. + @raise Anomaly if called on [In_T] or [In_X_In_T] *) +val redex_of_pattern : + ?resolve_typeclasses:bool -> env -> pattern -> + constr Evd.in_evar_universe_context + +(** [interp_rpattern ise gl rpat] "internalizes" and "interprets" [rpat] + in the current [Ltac] interpretation signature [ise] and tactic input [gl]*) +val interp_rpattern : + Tacinterp.interp_sign -> goal sigma -> + rpattern -> + pattern + +(** [interp_cpattern ise gl cpat ty] "internalizes" and "interprets" [cpat] + in the current [Ltac] interpretation signature [ise] and tactic input [gl]. + [ty] is an optional type for the redex of [cpat] *) +val interp_cpattern : + Tacinterp.interp_sign -> goal sigma -> + cpattern -> glob_constr_and_expr option -> + pattern + +(** The set of occurrences to be matched. The boolean is set to true + * to signal the complement of this set (i.e. {-1 3}) *) +type occ = (bool * int list) option + +(** [subst e p t i]. [i] is the number of binders + traversed so far, [p] the term from the pattern, [t] the matched one *) +type subst = env -> constr -> constr -> int -> constr + +(** [eval_pattern b env sigma t pat occ subst] maps [t] calling [subst] on every + [occ] occurrence of [pat]. The [int] argument is the number of + binders traversed. If [pat] is [None] then then subst is called on [t]. + [t] must live in [env] and [sigma], [pat] must have been interpreted in + (an extension of) [sigma]. + @raise NoMatch if [pat] has no occurrence and [b] is [true] (default [false]) + @return [t] where all [occ] occurrences of [pat] have been mapped using + [subst] *) +val eval_pattern : + ?raise_NoMatch:bool -> + env -> evar_map -> constr -> + pattern option -> occ -> subst -> + constr + +(** [fill_occ_pattern b env sigma t pat occ h] is a simplified version of + [eval_pattern]. + It replaces all [occ] occurrences of [pat] in [t] with Rel [h]. + [t] must live in [env] and [sigma], [pat] must have been interpreted in + (an extension of) [sigma]. + @raise NoMatch if [pat] has no occurrence and [b] is [true] (default [false]) + @return the instance of the redex of [pat] that was matched and [t] + transformed as described above. *) +val fill_occ_pattern : + ?raise_NoMatch:bool -> + env -> evar_map -> constr -> + pattern -> occ -> int -> + constr Evd.in_evar_universe_context * constr + +(** *************************** Low level APIs ****************************** *) + +(* The primitive matching facility. It matches of a term with holes, like + the T pattern above, and calls a continuation on its occurrences. *) + +type ssrdir = L2R | R2L +val pr_dir_side : ssrdir -> Pp.std_ppcmds + +(** a pattern for a term with wildcards *) +type tpattern + +(** [mk_tpattern env sigma0 sigma_p ok p_origin dir t] compiles a term [t] + living in [env] [sigma] (an extension of [sigma0]) intro a [tpattern]. + The [tpattern] can hold a (proof) term [p] and a diction [dir]. The [ok] + callback is used to filter occurrences. + @return the compiled [tpattern] and its [evar_map] + @raise UserEerror is the pattern is a wildcard *) +val mk_tpattern : + ?p_origin:ssrdir * constr -> + env -> evar_map -> + evar_map * constr -> + (constr -> evar_map -> bool) -> + ssrdir -> constr -> + evar_map * tpattern + +(** [findP env t i k] is a stateful function that finds the next occurrence + of a tpattern and calls the callback [k] to map the subterm matched. + The [int] argument passed to [k] is the number of binders traversed so far + plus the initial value [i]. + @return [t] where the subterms identified by the selected occurrences of + the patter have been mapped using [k] + @raise NoMatch if the raise_NoMatch flag given to [mk_tpattern_matcher] is + [true] and if the pattern did not match + @raise UserEerror if the raise_NoMatch flag given to [mk_tpattern_matcher] is + [false] and if the pattern did not match *) +type find_P = + env -> constr -> int -> k:subst -> constr + +(** [conclude ()] asserts that all mentioned ocurrences have been visited. + @return the instance of the pattern, the evarmap after the pattern + instantiation, the proof term and the ssrdit stored in the tpattern + @raise UserEerror if too many occurrences were specified *) +type conclude = + unit -> constr * ssrdir * (evar_map * Evd.evar_universe_context * constr) + +(** [mk_tpattern_matcher b o sigma0 occ sigma_tplist] creates a pair + a function [find_P] and [conclude] with the behaviour explained above. + The flag [b] (default [false]) changes the error reporting behaviour + of [find_P] if none of the [tpattern] matches. The argument [o] can + be passed to tune the [UserError] eventually raised (useful if the + pattern is coming from the LHS/RHS of an equation) *) +val mk_tpattern_matcher : + ?all_instances:bool -> + ?raise_NoMatch:bool -> + ?upats_origin:ssrdir * constr -> + evar_map -> occ -> evar_map * tpattern list -> + find_P * conclude + +(** Example of [mk_tpattern_matcher] to implement + [rewrite \{occ\}\[in t\]rules]. + It first matches "in t" (called [pat]), then in all matched subterms + it matches the LHS of the rules using [find_R]. + [concl0] is the initial goal, [concl] will be the goal where some terms + are replaced by a De Bruijn index. The [rw_progress] extra check + selects only occurrences that are not rewritten to themselves (e.g. + an occurrence "x + x" rewritten with the commutativity law of addition + is skipped) {[ + let find_R, conclude = match pat with + | Some (_, In_T _) -> + let aux (sigma, pats) (d, r, lhs, rhs) = + let sigma, pat = + mk_tpattern env0 sigma0 (sigma, r) (rw_progress rhs) d lhs in + sigma, pats @ [pat] in + let rpats = List.fold_left aux (r_sigma, []) rules in + let find_R, end_R = mk_tpattern_matcher sigma0 occ rpats in + find_R ~k:(fun _ _ h -> mkRel h), + fun cl -> let rdx, d, r = end_R () in (d,r),rdx + | _ -> ... in + let concl = eval_pattern env0 sigma0 concl0 pat occ find_R in + let (d, r), rdx = conclude concl in ]} *) + +(* convenience shortcut: [pf_fill_occ_term gl occ (sigma,t)] returns + * the conclusion of [gl] where [occ] occurrences of [t] have been replaced + * by [Rel 1] and the instance of [t] *) +val pf_fill_occ_term : goal sigma -> occ -> evar_map * constr -> constr * constr + +(* It may be handy to inject a simple term into the first form of cpattern *) +val cpattern_of_term : char * glob_constr_and_expr -> cpattern + +(** Helpers to make stateful closures. Example: a [find_P] function may be + called many times, but the pattern instantiation phase is performed only the + first time. The corresponding [conclude] has to return the instantiated + pattern redex. Since it is up to [find_P] to raise [NoMatch] if the pattern + has no instance, [conclude] considers it an anomaly if the pattern did + not match *) + +(** [do_once r f] calls [f] and updates the ref only once *) +val do_once : 'a option ref -> (unit -> 'a) -> unit +(** [assert_done r] return the content of r. @raise Anomaly is r is [None] *) +val assert_done : 'a option ref -> 'a + +(** Very low level APIs. + these are calls to evarconv's [the_conv_x] followed by + [consider_remaining_unif_problems] and [resolve_typeclasses]. + In case of failure they raise [NoMatch] *) + +val unify_HO : env -> evar_map -> constr -> constr -> evar_map +val pf_unify_HO : goal sigma -> constr -> constr -> goal sigma + +(** Some more low level functions needed to implement the full SSR language + on top of the former APIs *) +val tag_of_cpattern : cpattern -> char +val loc_of_cpattern : cpattern -> Loc.t +val id_of_pattern : pattern -> Names.variable option +val is_wildcard : cpattern -> bool +val cpattern_of_id : Names.variable -> cpattern +val cpattern_of_id : Names.variable -> cpattern +val pr_constr_pat : constr -> Pp.std_ppcmds +val pf_merge_uc : Evd.evar_universe_context -> goal Evd.sigma -> goal Evd.sigma +val pf_unsafe_merge_uc : Evd.evar_universe_context -> goal Evd.sigma -> goal Evd.sigma + +(* One can also "Set SsrMatchingDebug" from a .v *) +val debug : bool -> unit + +(* One should delimit a snippet with "Set SsrMatchingProfiling" and + * "Unset SsrMatchingProfiling" to get timings *) +val profile : bool -> unit + +(* eof *) diff --git a/plugins/ssrmatching/ssrmatching.v b/plugins/ssrmatching/ssrmatching.v new file mode 100644 index 0000000000..829ee05e11 --- /dev/null +++ b/plugins/ssrmatching/ssrmatching.v @@ -0,0 +1,26 @@ +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) +Declare ML Module "ssrmatching_plugin". + +Module SsrMatchingSyntax. + +(* Reserve the notation for rewrite patterns so that the user is not allowed *) +(* to declare it at a different level. *) +Reserved Notation "( a 'in' b )" (at level 0). +Reserved Notation "( a 'as' b )" (at level 0). +Reserved Notation "( a 'in' b 'in' c )" (at level 0). +Reserved Notation "( a 'as' b 'in' c )" (at level 0). + +(* Notation to define shortcuts for the "X in t" part of a pattern. *) +Notation "( X 'in' t )" := (_ : fun X => t) : ssrpatternscope. +Delimit Scope ssrpatternscope with pattern. + +(* Some shortcuts for recurrent "X in t" parts. *) +Notation RHS := (X in _ = X)%pattern. +Notation LHS := (X in X = _)%pattern. + +End SsrMatchingSyntax. + +Export SsrMatchingSyntax. + +Tactic Notation "ssrpattern" ssrpatternarg(p) := ssrpattern p . diff --git a/plugins/ssrmatching/ssrmatching_plugin.mlpack b/plugins/ssrmatching/ssrmatching_plugin.mlpack new file mode 100644 index 0000000000..5fb1f1567d --- /dev/null +++ b/plugins/ssrmatching/ssrmatching_plugin.mlpack @@ -0,0 +1 @@ +Ssrmatching diff --git a/plugins/ssrmatching/vo.itarget b/plugins/ssrmatching/vo.itarget new file mode 100644 index 0000000000..b0eb388349 --- /dev/null +++ b/plugins/ssrmatching/vo.itarget @@ -0,0 +1 @@ +ssrmatching.vo diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 80f1988a97..0b488308a1 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -592,9 +592,9 @@ let type_of_projection_knowing_arg env sigma p c ty = let control_only_guard env c = let check_fix_cofix e c = match kind_of_term c with | CoFix (_,(_,_,_) as cofix) -> - Inductive.check_cofix e cofix + Inductive.check_cofix ~flags:{check_guarded=true} e cofix | Fix (_,(_,_,_) as fix) -> - Inductive.check_fix e fix + Inductive.check_fix ~flags:{check_guarded=true} e fix | _ -> () in let rec iter env c = diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 378294c984..c894d96a78 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -72,14 +72,17 @@ open Inductiveops exception Found of int array -let search_guard loc env possible_indexes fixdefs = +(* spiwack: I chose [tflags] rather than [flags], like in the rest of + the code, for the argument name to avoid interference with the + argument for [inference_flags] also used in this module. *) +let search_guard ~tflags loc env possible_indexes fixdefs = (* Standard situation with only one possibility for each fix. *) (* We treat it separately in order to get proper error msg. *) let is_singleton = function [_] -> true | _ -> false in if List.for_all is_singleton possible_indexes then let indexes = Array.of_list (List.map List.hd possible_indexes) in let fix = ((indexes, 0),fixdefs) in - (try check_fix env fix + (try check_fix env ~flags:tflags fix with reraise -> let (e, info) = Errors.push reraise in let info = Loc.add_loc info loc in @@ -91,8 +94,14 @@ let search_guard loc env possible_indexes fixdefs = List.iter (fun l -> let indexes = Array.of_list l in - let fix = ((indexes, 0),fixdefs) in - try check_fix env fix; raise (Found indexes) + let fix = ((indexes, 0),fixdefs) in + (* spiwack: We search for a unspecified structural + argument under the assumption that we need to check the + guardedness condition (otherwise the first inductive argument + will be chosen). A more robust solution may be to raise an + error when totality is assumed but the strutural argument is + not specified. *) + try check_fix env ~flags:{Declarations.check_guarded=true} fix; raise (Found indexes) with TypeError _ -> ()) (List.combinations possible_indexes); let errmsg = "Cannot guess decreasing argument of fix." in @@ -606,11 +615,15 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ vn) in let fixdecls = (names,ftys,fdefs) in - let indexes = search_guard loc env possible_indexes fixdecls in + let indexes = + search_guard + ~tflags:{Declarations.check_guarded=true} + loc env possible_indexes fixdecls + in make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) | GCoFix i -> let cofix = (i,(names,ftys,fdefs)) in - (try check_cofix env cofix + (try check_cofix env ~flags:{Declarations.check_guarded=true} cofix with reraise -> let (e, info) = Errors.push reraise in let info = Loc.add_loc info loc in diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 824bb11aa4..2c02b4a217 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -22,7 +22,7 @@ open Misctypes (** An auxiliary function for searching for fixpoint guard indexes *) -val search_guard : +val search_guard : tflags:Declarations.typing_flags -> Loc.t -> env -> int list list -> rec_declaration -> int array type typing_constraint = OfType of types | IsType | WithoutTypeConstraint diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 52afa7f83a..598dd16d06 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -189,13 +189,13 @@ let rec execute env evdref cstr = | Fix ((vn,i as vni),recdef) -> let (_,tys,_ as recdef') = execute_recdef env evdref recdef in let fix = (vni,recdef') in - check_fix env fix; + check_fix env ~flags:{Declarations.check_guarded=true} fix; make_judge (mkFix fix) tys.(i) | CoFix (i,recdef) -> let (_,tys,_ as recdef') = execute_recdef env evdref recdef in let cofix = (i,recdef') in - check_cofix env cofix; + check_cofix env ~flags:{Declarations.check_guarded=true} cofix; make_judge (mkCoFix cofix) tys.(i) | Sort (Prop c) -> diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 10b2bda05e..cd7434843f 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -357,6 +357,7 @@ module Make | SetAssoc RightA -> keyword "right associativity" | SetAssoc NonA -> keyword "no associativity" | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ + | SetOnlyPrinting -> keyword "only printing" | SetOnlyParsing Flags.Current -> keyword "only parsing" | SetOnlyParsing v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"") | SetFormat("text",s) -> keyword "format " ++ pr_located qs s diff --git a/printing/printer.ml b/printing/printer.ml index cc8da4097d..2357ca0eaa 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -697,9 +697,14 @@ let prterm = pr_lconstr (* Printer function for sets of Assumptions.assumptions. It is used primarily by the Print Assumptions command. *) +type axiom = + | Constant of constant (* An axiom or a constant. *) + | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *) + | Guarded of constant (* a constant whose (co)fixpoints have been assumed to be guarded *) + type context_object = | Variable of Id.t (* A section variable or a Let definition *) - | Axiom of constant * (Label.t * Context.Rel.t * types) list + | Axiom of axiom * (Label.t * Context.Rel.t * types) list | Opaque of constant (* An opaque constant. *) | Transparent of constant @@ -707,12 +712,25 @@ type context_object = module OrderedContextObject = struct type t = context_object + + let compare_axiom x y = + match x,y with + | Constant k1 , Constant k2 -> + con_ord k1 k2 + | Positive m1 , Positive m2 -> + MutInd.CanOrd.compare m1 m2 + | Guarded k1 , Guarded k2 -> + con_ord k1 k2 + | _ , Constant _ -> 1 + | _ , Positive _ -> 1 + | _ -> -1 + let compare x y = match x , y with | Variable i1 , Variable i2 -> Id.compare i1 i2 | Variable _ , _ -> -1 | _ , Variable _ -> 1 - | Axiom (k1,_) , Axiom (k2, _) -> con_ord k1 k2 + | Axiom (k1,_) , Axiom (k2, _) -> compare_axiom k1 k2 | Axiom _ , _ -> -1 | _ , Axiom _ -> 1 | Opaque k1 , Opaque k2 -> con_ord k1 k2 @@ -745,17 +763,26 @@ let pr_assumptionset env s = try str " " ++ pr_ltype_env env sigma typ with e when Errors.noncritical e -> mt () in + let pr_axiom env ax typ = + match ax with + | Constant kn -> + safe_pr_constant env kn ++ safe_pr_ltype typ + | Positive m -> + hov 2 (MutInd.print m ++ spc () ++ strbrk"is positive.") + | Guarded kn -> + hov 2 (safe_pr_constant env kn ++ spc () ++ strbrk"is positive.") + in let fold t typ accu = let (v, a, o, tr) = accu in match t with | Variable id -> let var = pr_id id ++ str " : " ++ pr_ltype typ in (var :: v, a, o, tr) - | Axiom (kn,[]) -> - let ax = safe_pr_constant env kn ++ safe_pr_ltype typ in + | Axiom (axiom, []) -> + let ax = pr_axiom env axiom typ in (v, ax :: a, o, tr) - | Axiom (kn,l) -> - let ax = safe_pr_constant env kn ++ safe_pr_ltype typ ++ + | Axiom (axiom,l) -> + let ax = pr_axiom env axiom typ ++ cut() ++ prlist_with_sep cut (fun (lbl, ctx, ty) -> str " used in " ++ pr_label lbl ++ diff --git a/printing/printer.mli b/printing/printer.mli index 70993bb727..695ab33b23 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -161,12 +161,16 @@ val prterm : constr -> std_ppcmds (** = pr_lconstr *) (** Declarations for the "Print Assumption" command *) +type axiom = + | Constant of constant (* An axiom or a constant. *) + | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *) + | Guarded of constant (* a constant whose (co)fixpoints have been assumed to be guarded *) + type context_object = - | Variable of Id.t (** A section variable or a Let definition *) - (** An axiom and the type it inhabits (if an axiom of the empty type) *) - | Axiom of constant * (Label.t * Context.Rel.t * types) list - | Opaque of constant (** An opaque constant. *) - | Transparent of constant (** A transparent constant *) + | Variable of Id.t (* A section variable or a Let definition *) + | Axiom of axiom * (Label.t * Context.Rel.t * types) list + | Opaque of constant (* An opaque constant. *) + | Transparent of constant module ContextObjectSet : Set.S with type elt = context_object module ContextObjectMap : CMap.ExtS diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 0a63a3a0fe..b84b1265e0 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -79,7 +79,7 @@ let adjust_guardness_conditions const = function List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l) env (Safe_typing.side_effects_of_private_constants eff) in let indexes = - search_guard Loc.ghost env + search_guard ~tflags:{Declarations.check_guarded=true} Loc.ghost env possible_indexes fixdecls in (mkFix ((indexes,0),fixdecls), ctx), eff | _ -> (body, ctx), eff) } diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml index d53c1cc04a..0110510d35 100644 --- a/tactics/taccoerce.ml +++ b/tactics/taccoerce.ml @@ -107,7 +107,7 @@ let coerce_to_constr_context v = else raise (CannotCoerceTo "a term context") (* Interprets an identifier which must be fresh *) -let coerce_to_ident fresh env v = +let coerce_var_to_ident fresh env v = let v = Value.normalize v in let fail () = raise (CannotCoerceTo "a fresh identifier") in if has_type v (topwit wit_intro_pattern) then @@ -124,6 +124,52 @@ let coerce_to_ident fresh env v = destVar c else fail () + +(* Interprets, if possible, a constr to an identifier which may not + be fresh but suitable to be given to the fresh tactic. Works for + vars, constants, inductive, constructors and sorts. *) +let coerce_to_ident_not_fresh g env v = +let id_of_name = function + | Names.Anonymous -> Id.of_string "x" + | Names.Name x -> x in + let v = Value.normalize v in + let fail () = raise (CannotCoerceTo "an identifier") in + if has_type v (topwit wit_intro_pattern) then + match out_gen (topwit wit_intro_pattern) v with + | _, IntroNaming (IntroIdentifier id) -> id + | _ -> fail () + else if has_type v (topwit wit_var) then + out_gen (topwit wit_var) v + else + match Value.to_constr v with + | None -> fail () + | Some c -> + match Constr.kind c with + | Var id -> id + | Meta m -> id_of_name (Evd.meta_name g m) + | Evar (kn,_) -> + begin match Evd.evar_ident kn g with + | None -> fail () + | Some id -> id + end + | Const (cst,_) -> Label.to_id (Constant.label cst) + | Construct (cstr,_) -> + let ref = Globnames.ConstructRef cstr in + let basename = Nametab.basename_of_global ref in + basename + | Ind (ind,_) -> + let ref = Globnames.IndRef ind in + let basename = Nametab.basename_of_global ref in + basename + | Sort s -> + begin + match s with + | Prop _ -> Label.to_id (Label.make "Prop") + | Type _ -> Label.to_id (Label.make "Type") + end + | _ -> fail() + + let coerce_to_intro_pattern env v = let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then diff --git a/tactics/taccoerce.mli b/tactics/taccoerce.mli index 7a963f95f3..0b67f8726e 100644 --- a/tactics/taccoerce.mli +++ b/tactics/taccoerce.mli @@ -50,7 +50,9 @@ end val coerce_to_constr_context : Value.t -> constr -val coerce_to_ident : bool -> Environ.env -> Value.t -> Id.t +val coerce_var_to_ident : bool -> Environ.env -> Value.t -> Id.t + +val coerce_to_ident_not_fresh : Evd.evar_map -> Environ.env -> Value.t -> Id.t val coerce_to_intro_pattern : Environ.env -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr diff --git a/test-suite/success/ssrpattern.v b/test-suite/success/ssrpattern.v new file mode 100644 index 0000000000..96f0bbac92 --- /dev/null +++ b/test-suite/success/ssrpattern.v @@ -0,0 +1,22 @@ +Require Import ssrmatching. + +(*Set Debug SsrMatching.*) + +Tactic Notation "at" "[" ssrpatternarg(pat) "]" tactic(t) := + let name := fresh in + let def_name := fresh in + ssrpattern pat; + intro name; + pose proof (refl_equal name) as def_name; + unfold name at 1 in def_name; + t def_name; + [ rewrite <- def_name | idtac.. ]; + clear name def_name. + +Lemma test (H : True -> True -> 3 = 7) : 28 = 3 * 4. +Proof. +at [ X in X * 4 ] ltac:(fun place => rewrite -> H in place). +- reflexivity. +- trivial. +- trivial. +Qed. diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml index 1802b2d366..c05c5f6c28 100644 --- a/toplevel/assumptions.ml +++ b/toplevel/assumptions.ml @@ -286,11 +286,17 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = if is_local_assum decl then ContextObjectMap.add (Variable id) t accu else accu | ConstRef kn -> - let cb = lookup_constant kn in + let cb = lookup_constant kn in + let accu = + if cb.const_typing_flags.check_guarded then accu + else + let l = try Refmap_env.find obj ax2ty with Not_found -> [] in + ContextObjectMap.add (Axiom (Guarded kn, l)) Constr.mkProp accu + in if not (Declareops.constant_has_body cb) then let t = type_of_constant cb in let l = try Refmap_env.find obj ax2ty with Not_found -> [] in - ContextObjectMap.add (Axiom (kn,l)) t accu + ContextObjectMap.add (Axiom (Constant kn,l)) t accu else if add_opaque && (Declareops.is_opaque cb || not (Cpred.mem kn knst)) then let t = type_of_constant cb in ContextObjectMap.add (Opaque kn) t accu @@ -299,6 +305,12 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = ContextObjectMap.add (Transparent kn) t accu else accu - | IndRef _ | ConstructRef _ -> accu + | IndRef (m,_) | ConstructRef ((m,_),_) -> + let mind = Global.lookup_mind m in + if mind.mind_checked_positive then + accu + else + let l = try Refmap_env.find obj ax2ty with Not_found -> [] in + ContextObjectMap.add (Axiom (Positive m, l)) Constr.mkProp accu in Refmap_env.fold fold graph ContextObjectMap.empty diff --git a/toplevel/command.ml b/toplevel/command.ml index f0f678e08c..6f2dd1bf15 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -145,9 +145,9 @@ let get_locality id = function | Local -> true | Global -> false -let declare_global_definition ident ce local k pl imps = +let declare_global_definition ~flags ident ce local k pl imps = let local = get_locality ident local in - let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in + let kn = declare_constant ~flags ident ~local (DefinitionEntry ce, IsDefinition k) in let gr = ConstRef kn in let () = maybe_declare_manual_implicits false gr imps in let () = Universes.register_universe_binders gr pl in @@ -158,7 +158,7 @@ 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, p, k) ce pl imps hook = +let declare_definition ~flags ident (local, p, k) ce pl imps hook = let fix_exn = Future.fix_exn_of ce.const_entry_body in let () = !declare_definition_hook ce in let r = match local with @@ -175,11 +175,11 @@ let declare_definition ident (local, p, k) ce pl imps hook = in gr | Discharge | Local | Global -> - declare_global_definition ident ce local k pl imps in + declare_global_definition ~flags ident ce local k pl imps in Lemmas.call_hook fix_exn hook local r let _ = Obligations.declare_definition_ref := - (fun i k c imps hook -> declare_definition i k c [] imps hook) + (fun i k c imps hook -> declare_definition ~flags:{Declarations.check_guarded=true} i k c [] imps hook) let do_definition ident k pl bl red_option c ctypopt hook = let (ce, evd, pl', imps as def) = @@ -203,7 +203,7 @@ let do_definition ident k pl bl red_option c ctypopt hook = ignore(Obligations.add_definition ident ~term:c cty ctx ?pl ~implicits:imps ~kind:k ~hook obls) else let ce = check_definition def in - ignore(declare_definition ident k ce pl' imps + ignore(declare_definition ~flags:{Declarations.check_guarded=true} ident k ce pl' imps (Lemmas.mk_hook (fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r))) @@ -549,7 +549,7 @@ let check_param = function | LocalRawAssum (nas, Default _, _) -> List.iter check_named nas | LocalRawAssum (nas, Generalized _, _) -> () -let interp_mutual_inductive (paramsl,indl) notations poly prv finite = +let interp_mutual_inductive chk (paramsl,indl) notations poly prv finite = check_all_names_different indl; List.iter check_param paramsl; let env0 = Global.env() in @@ -630,7 +630,8 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = mind_entry_inds = entries; mind_entry_polymorphic = poly; mind_entry_private = if prv then Some false else None; - mind_entry_universes = uctx }, + mind_entry_universes = uctx; + mind_entry_check_positivity = chk; }, pl, impls (* Very syntactical equality *) @@ -715,17 +716,20 @@ type one_inductive_impls = Impargs.manual_explicitation list (* for inds *)* Impargs.manual_explicitation list list (* for constrs *) -let do_mutual_inductive indl poly prv finite = +let do_mutual_inductive chk indl poly prv finite = let indl,coes,ntns = extract_mutual_inductive_declaration_components indl in (* Interpret the types *) - let mie,pl,impls = interp_mutual_inductive indl ntns poly prv finite in + let mie,pl,impls = interp_mutual_inductive chk indl ntns poly prv finite in (* Declare the mutual inductive block with its associated schemes *) ignore (declare_mutual_inductive_with_eliminations mie pl impls); (* Declare the possible notations of inductive types *) List.iter Metasyntax.add_notation_interpretation ntns; (* Declare the coercions *) - List.iter (fun qid -> Class.try_add_new_coercion (locate qid) false poly) coes - + List.iter (fun qid -> Class.try_add_new_coercion (locate qid) false poly) coes; + (* If [chk] is [false] (i.e. positivity is assumed) declares itself + as unsafe. *) + if not chk then Feedback.feedback Feedback.AddedAxiom else () + (* 3c| Fixpoints and co-fixpoints *) (* An (unoptimized) function that maps preorders to partial orders... @@ -829,12 +833,12 @@ let interp_fix_body env_rec evdref impls (_,ctx) fix ccl = let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx -let declare_fix ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),eff) t imps = +let declare_fix ~flags ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),eff) t imps = let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in - declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r)) + declare_definition ~flags f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r)) let _ = Obligations.declare_fix_ref := - (fun ?opaque k ctx f d t imps -> declare_fix ?opaque k [] ctx f d t imps) + (fun ?opaque k ctx f d t imps -> declare_fix ~flags:{Declarations.check_guarded=true} ?opaque k [] ctx f d t imps) let prepare_recursive_declaration fixnames fixtypes fixdefs = let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in @@ -1135,7 +1139,7 @@ let interp_cofixpoint l ntns = check_recursive false env evd fix; (fix,pl,Evd.evar_universe_context evd,info) -let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns = +let declare_fixpoint ~flags local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns = if List.exists Option.is_empty fixdefs then (* Some bodies to define by proof *) let thms = @@ -1155,7 +1159,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind let fixdefs = List.map Option.get fixdefs in let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in let env = Global.env() in - let indexes = search_guard Loc.ghost env indexes fixdecls in + let indexes = search_guard ~tflags:flags Loc.ghost env indexes fixdecls in let fiximps = List.map (fun (n,r,p) -> r) fiximps in let vars = Universes.universes_of_constr (mkFix ((indexes,0),fixdecls)) in let fixdecls = @@ -1164,7 +1168,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind let evd = Evd.restrict_universe_context evd vars in let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in let pl, ctx = Evd.universe_context ?names:pl evd in - ignore (List.map4 (declare_fix (local, poly, Fixpoint) pl ctx) + ignore (List.map4 (declare_fix ~flags (local, poly, Fixpoint) pl ctx) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) fixpoint_message (Some indexes) fixnames; @@ -1172,7 +1176,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind (* Declare notations *) List.iter Metasyntax.add_notation_interpretation ntns -let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ntns = +let declare_cofixpoint ~flags local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ntns = if List.exists Option.is_empty fixdefs then (* Some bodies to define by proof *) let thms = @@ -1198,7 +1202,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in let pl, ctx = Evd.universe_context ?names:pl evd in - ignore (List.map4 (declare_fix (local, poly, CoFixpoint) pl ctx) + ignore (List.map4 (declare_fix ~flags (local, poly, CoFixpoint) pl ctx) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) cofixpoint_message fixnames @@ -1264,8 +1268,14 @@ let do_program_recursive local p fixkind fixl ntns = Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs) in let indexes = - Pretyping.search_guard Loc.ghost (Global.env ()) possible_indexes fixdecls in - List.iteri (fun i _ -> Inductive.check_fix env ((indexes,i),fixdecls)) fixl + Pretyping.search_guard + ~tflags:{Declarations.check_guarded=true} + Loc.ghost (Global.env ()) possible_indexes fixdecls in + List.iteri (fun i _ -> + Inductive.check_fix env + ~flags:{Declarations.check_guarded=true} + ((indexes,i),fixdecls)) + fixl end in let ctx = Evd.evar_universe_context evd in let kind = match fixkind with @@ -1299,19 +1309,21 @@ let do_program_fixpoint local poly l = errorlabstrm "do_program_fixpoint" (str "Well-founded fixpoints not allowed in mutually recursive blocks") -let do_fixpoint local poly l = +let do_fixpoint ~flags local poly l = if Flags.is_program_mode () then do_program_fixpoint local poly l else let fixl, ntns = extract_fixpoint_components true l in let (_, _, _, info as fix) = interp_fixpoint fixl ntns in let possible_indexes = List.map compute_possible_guardness_evidences info in - declare_fixpoint local poly fix possible_indexes ntns + declare_fixpoint ~flags local poly fix possible_indexes ntns; + if not flags.Declarations.check_guarded then Feedback.feedback Feedback.AddedAxiom else () -let do_cofixpoint local poly l = +let do_cofixpoint ~flags local poly l = let fixl,ntns = extract_cofixpoint_components l in if Flags.is_program_mode () then do_program_recursive local poly Obligations.IsCoFixpoint fixl ntns else let cofix = interp_cofixpoint fixl ntns in - declare_cofixpoint local poly cofix ntns + declare_cofixpoint ~flags local poly cofix ntns; + if not flags.Declarations.check_guarded then Feedback.feedback Feedback.AddedAxiom else () diff --git a/toplevel/command.mli b/toplevel/command.mli index b97cb487d5..2d27552a19 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -36,7 +36,7 @@ val interp_definition : constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * Universes.universe_binders * Impargs.manual_implicits -val declare_definition : Id.t -> definition_kind -> +val declare_definition : flags:Declarations.typing_flags -> Id.t -> definition_kind -> Safe_typing.private_constants definition_entry -> Universes.universe_binders -> Impargs.manual_implicits -> Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference @@ -91,6 +91,7 @@ type one_inductive_impls = Impargs.manual_implicits list (** for constrs *) val interp_mutual_inductive : + bool -> (* if [false], then positivity is assumed *) structured_inductive_expr -> decl_notation list -> polymorphic -> private_flag -> Decl_kinds.recursivity_kind -> mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list @@ -105,6 +106,7 @@ val declare_mutual_inductive_with_eliminations : (** Entry points for the vernacular commands Inductive and CoInductive *) val do_mutual_inductive : + bool -> (* if [false], then positivity is assumed *) (one_inductive_expr * decl_notation list) list -> polymorphic -> private_flag -> Decl_kinds.recursivity_kind -> unit @@ -148,12 +150,13 @@ val interp_cofixpoint : (** Registering fixpoints and cofixpoints in the environment *) val declare_fixpoint : + flags:Declarations.typing_flags -> locality -> polymorphic -> recursive_preentry * lident list option * Evd.evar_universe_context * (Name.t list * Impargs.manual_implicits * int option) list -> lemma_possible_guards -> decl_notation list -> unit -val declare_cofixpoint : locality -> polymorphic -> +val declare_cofixpoint : flags:Declarations.typing_flags -> locality -> polymorphic -> recursive_preentry * lident list option * Evd.evar_universe_context * (Name.t list * Impargs.manual_implicits * int option) list -> decl_notation list -> unit @@ -161,14 +164,16 @@ val declare_cofixpoint : locality -> polymorphic -> (** Entry points for the vernacular commands Fixpoint and CoFixpoint *) val do_fixpoint : + flags:Declarations.typing_flags -> (* When [false], assume guarded. *) locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit val do_cofixpoint : + flags:Declarations.typing_flags -> (* When [false], assume guarded. *) locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit (** Utils *) val check_mutuality : Environ.env -> bool -> (Id.t * types) list -> unit -val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.universe_context -> Id.t -> +val declare_fix : flags:Declarations.typing_flags -> ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.universe_context -> Id.t -> Safe_typing.private_constants Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index a820008d2e..46fb55b5f7 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -575,6 +575,7 @@ let parse_args arglist = |"-type-in-type" -> set_type_in_type () |"-unicode" -> add_require "Utf8_core" |"-v"|"--version" -> Usage.version (exitcode ()) + |"--print-version" -> Usage.machine_readable_version (exitcode ()) |"-verbose-compat-notations" -> verb_compat_ntn := true |"-where" -> print_where := true |"-xml" -> Flags.xml_export := true diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 6b267283a4..74361eb1c6 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -116,5 +116,6 @@ let process_inductive (sechyps,abs_ctx) modlist mib = mind_entry_inds = inds'; mind_entry_polymorphic = mib.mind_polymorphic; mind_entry_private = mib.mind_private; - mind_entry_universes = univs + mind_entry_universes = univs; + mind_entry_check_positivity = mib.mind_checked_positive; } diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index f995a390cf..a43758e3c9 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -497,7 +497,7 @@ let map_inductive_block f kn n = for i=0 to n-1 do f (kn,i) done let declare_default_schemes kn = let mib = Global.lookup_mind kn in let n = Array.length mib.mind_packets in - if !elim_flag && (mib.mind_finite <> BiFinite || !bifinite_elim_flag) then + if !elim_flag && (mib.mind_finite <> BiFinite || !bifinite_elim_flag) && mib.mind_checked_positive then declare_induction_schemes kn; if !case_flag then map_inductive_block declare_one_case_analysis_scheme kn n; if is_eq_flag() then try_declare_beq_scheme kn; diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index b22d53f546..7d8c670259 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -680,6 +680,7 @@ type syntax_extension_obj = locality_flag * syntax_extension list let cache_one_syntax_extension se = let ntn = se.synext_notation in let prec = se.synext_level in + let onlyprint = se.synext_notgram.notgram_onlyprinting in try let oldprec = Notation.level_of_notation ntn in if not (Notation.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec @@ -687,10 +688,10 @@ let cache_one_syntax_extension se = (* Reserve the notation level *) Notation.declare_notation_level ntn prec; (* Declare the parsing rule *) - Egramcoq.extend_constr_grammar prec se.synext_notgram; - (* Declare the printing rule *) - Notation.declare_notation_printing_rule ntn - ~extra:se.synext_extra (se.synext_unparsing, fst prec) + if not onlyprint then Egramcoq.extend_constr_grammar prec se.synext_notgram; + (* Declare the notation rule *) + Notation.declare_notation_rule ntn + ~extra:se.synext_extra (se.synext_unparsing, fst prec) se.synext_notgram let cache_syntax_extension (_, (_, sy)) = List.iter cache_one_syntax_extension sy @@ -723,9 +724,10 @@ let inSyntaxExtension : syntax_extension_obj -> obj = let interp_modifiers modl = let onlyparsing = ref false in + let onlyprinting = ref false in let rec interp assoc level etyps format extra = function | [] -> - (assoc,level,etyps,!onlyparsing,format,extra) + (assoc,level,etyps,!onlyparsing,!onlyprinting,format,extra) | SetEntryType (s,typ) :: l -> let id = Id.of_string s in if Id.List.mem_assoc id etyps then @@ -750,6 +752,9 @@ let interp_modifiers modl = | SetOnlyParsing _ :: l -> onlyparsing := true; interp assoc level etyps format extra l + | SetOnlyPrinting :: l -> + onlyprinting := true; + interp assoc level etyps format extra l | SetFormat ("text",s) :: l -> if not (Option.is_empty format) then error "A format is given more than once."; interp assoc level etyps (Some s) extra l @@ -758,7 +763,7 @@ let interp_modifiers modl = in interp None None [] None [] modl let check_infix_modifiers modifiers = - let (assoc,level,t,b,fmt,extra) = interp_modifiers modifiers in + let (_, _, t, _, _, _, _) = interp_modifiers modifiers in if not (List.is_empty t) then error "Explicit entry level or type unexpected in infix notation." @@ -769,13 +774,20 @@ let check_useless_entry_types recvars mainvars etyps = (pr_id x ++ str " is unbound in the notation.") | _ -> () -let no_syntax_modifiers = function - | [] | [SetOnlyParsing _] -> true - | _ -> false +let not_a_syntax_modifier = function +| SetOnlyParsing _ -> true +| SetOnlyPrinting -> true +| _ -> false -let is_only_parsing = function - | [SetOnlyParsing _] -> true - | _ -> false +let no_syntax_modifiers mods = List.for_all not_a_syntax_modifier mods + +let is_only_parsing mods = + let test = function SetOnlyParsing _ -> true | _ -> false in + List.exists test mods + +let is_only_printing mods = + let test = function SetOnlyPrinting -> true | _ -> false in + List.exists test mods (* Compute precedences from modifiers (or find default ones) *) @@ -942,7 +954,7 @@ let remove_curly_brackets l = in aux true l let compute_syntax_data df modifiers = - let (assoc,n,etyps,onlyparse,fmt,extra) = interp_modifiers modifiers in + let (assoc,n,etyps,onlyparse,onlyprint,fmt,extra) = interp_modifiers modifiers in let assoc = match assoc with None -> (* default *) Some NonA | a -> a in let toks = split_notation_string df in let (recvars,mainvars,symbols) = analyze_notation_tokens toks in @@ -968,17 +980,22 @@ let compute_syntax_data df modifiers = let sy_data = (n,sy_typs,symbols',fmt) in let sy_fulldata = (i_typs,ntn_for_grammar,prec,need_squash,sy_data) in let df' = ((Lib.library_dp(),Lib.current_dirpath true),df) in - let i_data = (onlyparse,recvars,mainvars,(ntn_for_interp,df')) in + let i_data = (onlyparse,onlyprint,recvars,mainvars,(ntn_for_interp,df')) in (* Return relevant data for interpretation and for parsing/printing *) (msgs,i_data,i_typs,sy_fulldata,extra) let compute_pure_syntax_data df mods = - let (msgs,(onlyparse,_,_,_),_,sy_data,extra) = compute_syntax_data df mods in + let (msgs,(onlyparse,onlyprint,_,_,_),_,sy_data,extra) = compute_syntax_data df mods in let msgs = if onlyparse then (Feedback.msg_warning, strbrk "The only parsing modifier has no effect in Reserved Notation.")::msgs else msgs in + let msgs = + if onlyprint then + (Feedback.msg_warning, + strbrk "The only printing modifier has no effect in Reserved Notation.")::msgs + else msgs in msgs, sy_data, extra (**********************************************************************) @@ -1063,7 +1080,7 @@ let recover_syntax ntn = let prec = Notation.level_of_notation ntn in let pp_rule,_ = Notation.find_notation_printing_rule ntn in let pp_extra_rules = Notation.find_notation_extra_printing_rules ntn in - let pa_rule = Egramcoq.recover_constr_grammar ntn prec in + let pa_rule = Notation.find_notation_parsing_rules ntn in { synext_level = prec; synext_notation = ntn; synext_notgram = pa_rule; @@ -1086,22 +1103,24 @@ let recover_notation_syntax rawntn = (**********************************************************************) (* Main entry point for building parsing and printing rules *) -let make_pa_rule i_typs (n,typs,symbols,_) ntn = +let make_pa_rule i_typs (n,typs,symbols,_) ntn onlyprint = let assoc = recompute_assoc typs in let prod = make_production typs symbols in { notgram_level = n; notgram_assoc = assoc; notgram_notation = ntn; notgram_prods = prod; - notgram_typs = i_typs; } + notgram_typs = i_typs; + notgram_onlyprinting = onlyprint; + } let make_pp_rule (n,typs,symbols,fmt) = match fmt with | None -> [UnpBox (PpHOVB 0, make_hunks typs symbols n)] | Some fmt -> hunks_of_format (n, List.split typs) (symbols, parse_format fmt) -let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) extra = - let pa_rule = make_pa_rule i_typs sy_data ntn in +let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) extra onlyprint = + let pa_rule = make_pa_rule i_typs sy_data ntn onlyprint in let pp_rule = make_pp_rule sy_data in let sy = { synext_level = prec; @@ -1124,10 +1143,10 @@ let to_map l = let add_notation_in_scope local df c mods scope = let (msgs,i_data,i_typs,sy_data,extra) = compute_syntax_data df mods in - (* Prepare the parsing and printing rules *) - let sy_rules = make_syntax_rules sy_data extra in (* Prepare the interpretation *) - let (onlyparse, recvars,mainvars, df') = i_data in + let (onlyparse, onlyprint, recvars,mainvars, df') = i_data in + (* Prepare the parsing and printing rules *) + let sy_rules = make_syntax_rules sy_data extra onlyprint in let i_vars = make_internalization_vars recvars mainvars i_typs in let nenv = { ninterp_var_type = to_map i_vars; @@ -1188,7 +1207,7 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env) let add_syntax_extension local ((loc,df),mods) = let msgs, sy_data, extra = compute_pure_syntax_data df mods in - let sy_rules = make_syntax_rules sy_data extra in + let sy_rules = make_syntax_rules sy_data extra false in Flags.if_verbose (List.iter (fun (f,x) -> f x)) msgs; Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules)) @@ -1200,7 +1219,7 @@ let add_notation_interpretation ((loc,df),c,sc) = let set_notation_for_interpretation impls ((_,df),c,sc) = (try ignore - (silently (add_notation_interpretation_core false df ~impls c sc) false); + (silently (fun () -> add_notation_interpretation_core false df ~impls c sc false) ()); with NoSyntaxRule -> error "Parsing rule for this notation has to be previously declared."); Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index dbc3ccaac4..00fd972109 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -567,7 +567,8 @@ let declare_mutual_definition l = List.map3 compute_possible_guardness_evidences wfl fixdefs fixtypes in let indexes = - Pretyping.search_guard Loc.ghost (Global.env()) + Pretyping.search_guard ~tflags:{Declarations.check_guarded=true} + Loc.ghost (Global.env()) possible_indexes fixdecls in Some indexes, List.map_i (fun i _ -> diff --git a/toplevel/record.ml b/toplevel/record.ml index 0c3bd953c0..214d44d83f 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -361,7 +361,7 @@ let structure_signature ctx = open Typeclasses -let declare_structure finite poly ctx id idbuild paramimpls params arity template +let declare_structure chk finite poly ctx id idbuild paramimpls params arity template fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers sign = let nparams = List.length params and nfields = List.length fields in let args = Context.Rel.to_extended_list nfields params in @@ -386,7 +386,8 @@ let declare_structure finite poly ctx id idbuild paramimpls params arity templat mind_entry_inds = [mie_ind]; mind_entry_polymorphic = poly; mind_entry_private = None; - mind_entry_universes = ctx } in + mind_entry_universes = ctx; + mind_entry_check_positivity = chk; } in let kn = Command.declare_mutual_inductive_with_eliminations mie [] [(paramimpls,[])] in let rsp = (kn,0) in (* This is ind path of idstruc *) let cstr = (rsp,1) in @@ -405,7 +406,7 @@ let implicits_of_context ctx = in ExplByPos (i, explname), (true, true, true)) 1 (List.rev (Anonymous :: (List.map get_name ctx))) -let declare_class finite def poly ctx id idbuild paramimpls params arity +let declare_class chk finite def poly ctx id idbuild paramimpls params arity template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities sign = let fieldimpls = (* Make the class implicit in the projections, and the params if applicable. *) @@ -448,7 +449,7 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity in cref, [Name proj_name, sub, Some proj_cst] | _ -> - let ind = declare_structure BiFinite poly ctx (snd id) idbuild paramimpls + let ind = declare_structure chk BiFinite poly ctx (snd id) idbuild paramimpls params arity template fieldimpls fields ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign in @@ -527,8 +528,9 @@ open Vernacexpr (* [fs] corresponds to fields and [ps] to parameters; [coers] is a list telling if the corresponding fields must me declared as coercions - or subinstances *) -let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,idbuild,s) = + or subinstances. When [chk] is false positivity is + assumed. *) +let definition_structure chk (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,idbuild,s) = let cfs,notations = List.split cfs in let cfs,priorities = List.split cfs in let coers,fs = List.split cfs in @@ -549,14 +551,14 @@ let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,id let sign = structure_signature (fields@params) in let gr = match kind with | Class def -> - let gr = declare_class finite def poly ctx (loc,idstruc) idbuild + let gr = declare_class chk finite def poly ctx (loc,idstruc) idbuild implpars params arity template implfs fields is_coe coers priorities sign in gr | _ -> let implfs = List.map (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs in - let ind = declare_structure finite poly ctx idstruc + let ind = declare_structure chk finite poly ctx idstruc idbuild implpars params arity template implfs fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in IndRef ind diff --git a/toplevel/record.mli b/toplevel/record.mli index 26eb3378bb..5253262376 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -24,7 +24,9 @@ val declare_projections : coercion_flag list -> manual_explicitation list list -> Context.Rel.t -> (Name.t * bool) list * constant option list -val declare_structure : Decl_kinds.recursivity_kind -> +val declare_structure : + bool -> (** check positivity? *) + Decl_kinds.recursivity_kind -> bool (** polymorphic?*) -> Univ.universe_context -> Id.t -> Id.t -> manual_explicitation list -> Context.Rel.t -> (** params *) constr -> (** arity *) @@ -37,6 +39,7 @@ val declare_structure : Decl_kinds.recursivity_kind -> inductive val definition_structure : + bool -> (** check positivity? *) inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind * plident with_coercion * local_binder list * (local_decl_expr with_instance with_priority with_notation) list * Id.t * constr_expr option -> global_reference diff --git a/toplevel/usage.ml b/toplevel/usage.ml index ffbbe7ed4a..8f77aea440 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -11,6 +11,10 @@ let version ret = Coq_config.version Coq_config.date; Printf.printf "compiled on %s with OCaml %s\n" Coq_config.compile_date Coq_config.caml_version; exit ret +let machine_readable_version ret = + Printf.printf "%s %s\n" + Coq_config.version Coq_config.caml_version; + exit ret (* print the usage of coqtop (or coqc) on channel co *) diff --git a/toplevel/usage.mli b/toplevel/usage.mli index 3ce9e93ee5..dccb40e713 100644 --- a/toplevel/usage.mli +++ b/toplevel/usage.mli @@ -9,6 +9,7 @@ (** {6 Prints the version number on the standard output and exits (with 0). } *) val version : int -> 'a +val machine_readable_version : int -> 'a (** {6 Prints the usage on the error output, preceeded by a user-provided message. } *) val print_usage : string -> unit diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 222b7d3df1..0b4dc0d185 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -519,7 +519,7 @@ let vernac_assumption locality poly (local, kind) l nl = let status = do_assumptions kind nl l in if not status then Feedback.feedback Feedback.AddedAxiom -let vernac_record k poly finite struc binders sort nameopt cfs = +let vernac_record chk k poly finite struc binders sort nameopt cfs = let const = match nameopt with | None -> add_prefix "Build_" (snd (fst (snd struc))) | Some (_,id as lid) -> @@ -530,9 +530,14 @@ let vernac_record k poly finite struc binders sort nameopt cfs = match x with | Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj" | _ -> ()) cfs); - ignore(Record.definition_structure (k,poly,finite,struc,binders,cfs,const,sort)) - -let vernac_inductive poly lo finite indl = + ignore(Record.definition_structure chk (k,poly,finite,struc,binders,cfs,const,sort)) + +(** When [chk] is false, positivity is assumed. When [poly] is true + the type is declared polymorphic. When [lo] is true, then the type + is declared private (as per the [Private] keyword). [finite] + indicates whether the type is inductive, co-inductive or + neither. *) +let vernac_inductive chk poly lo finite indl = if Dumpglob.dump () then List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) -> match cstrs with @@ -548,14 +553,14 @@ let vernac_inductive poly lo finite indl = | [ (_ , _ , _ ,Variant, RecordDecl _),_ ] -> Errors.error "The Variant keyword cannot be used to define a record type. Use Record instead." | [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] -> - vernac_record (match b with Class true -> Class false | _ -> b) + vernac_record chk (match b with Class true -> Class false | _ -> b) poly finite id bl c oc fs | [ ( id , bl , c , Class true, Constructors [l]), _ ] -> let f = let (coe, ((loc, id), ce)) = l in let coe' = if coe then Some true else None in (((coe', AssumExpr ((loc, Name id), ce)), None), []) - in vernac_record (Class true) poly finite id bl c None [f] + in vernac_record chk (Class true) poly finite id bl c None [f] | [ ( id , bl , c , Class true, _), _ ] -> Errors.error "Definitional classes must have a single method" | [ ( id , bl , c , Class false, Constructors _), _ ] -> @@ -569,19 +574,19 @@ let vernac_inductive poly lo finite indl = | _ -> Errors.error "Cannot handle mutually (co)inductive records." in let indl = List.map unpack indl in - do_mutual_inductive indl poly lo finite + do_mutual_inductive chk indl poly lo finite -let vernac_fixpoint locality poly local l = +let vernac_fixpoint ~flags locality poly local l = let local = enforce_locality_exp locality local in if Dumpglob.dump () then List.iter (fun (((lid,_), _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; - do_fixpoint local poly l + do_fixpoint ~flags local poly l -let vernac_cofixpoint locality poly local l = +let vernac_cofixpoint ~flags locality poly local l = let local = enforce_locality_exp locality local in if Dumpglob.dump () then List.iter (fun (((lid,_), _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; - do_cofixpoint local poly l + do_cofixpoint ~flags local poly l let vernac_scheme l = if Dumpglob.dump () then @@ -1726,6 +1731,7 @@ let vernac_load interp fname = try while true do interp (snd (parse_sentence input)) done with End_of_input -> () +let all_checks = { Declarations.check_guarded = true } (* "locality" is the prefix "Local" attribute, while the "local" component * is the outdated/deprecated "Local" attribute of some vernacular commands @@ -1763,9 +1769,9 @@ let interp ?proof ~loc locality poly c = | VernacEndProof e -> vernac_end_proof ?proof e | VernacExactProof c -> vernac_exact_proof c | VernacAssumption (stre,nl,l) -> vernac_assumption locality poly stre l nl - | VernacInductive (priv,finite,l) -> vernac_inductive poly priv finite l - | VernacFixpoint (local, l) -> vernac_fixpoint locality poly local l - | VernacCoFixpoint (local, l) -> vernac_cofixpoint locality poly local l + | VernacInductive (priv,finite,l) -> vernac_inductive true poly priv finite l + | VernacFixpoint (local, l) -> vernac_fixpoint locality ~flags:all_checks poly local l + | VernacCoFixpoint (local, l) -> vernac_cofixpoint ~flags:all_checks locality poly local l | VernacScheme l -> vernac_scheme l | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l | VernacUniverse l -> vernac_universe loc poly l |