diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-03-22 14:33:22 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-03-22 14:36:14 +0100 |
commit | 8b73fd7c6ce423f8c8a2594e90200f2407795d52 (patch) | |
tree | 91db0f56763e6512016055a8dc47185f7317fe6b | |
parent | 6e0ca299c407125a8d65f54ab424bdae3667125e (diff) | |
parent | cd87eac3757d8925ff4ba7dee85efadb195153a3 (diff) |
Merge branch 'v8.6'
-rw-r--r-- | kernel/cemitcodes.ml | 31 | ||||
-rw-r--r-- | parsing/g_prim.ml4 | 5 | ||||
-rw-r--r-- | parsing/g_vernac.ml4 | 2 | ||||
-rw-r--r-- | parsing/pcoq.ml | 1 | ||||
-rw-r--r-- | parsing/pcoq.mli | 1 | ||||
-rw-r--r-- | tactics/class_tactics.ml | 12 | ||||
-rw-r--r-- | test-suite/bugs/closed/4969.v | 11 | ||||
-rw-r--r-- | test-suite/success/Notations.v | 7 | ||||
-rw-r--r-- | tools/coq_makefile.ml | 1 | ||||
-rw-r--r-- | vernac/metasyntax.ml | 16 |
10 files changed, 62 insertions, 25 deletions
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index f2c3b402b..40c1e027d 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -274,41 +274,44 @@ let emit_instr = function | Kstop -> out opSTOP -(* Emission of a list of instructions. Include some peephole optimization. *) +(* Emission of a current list and remaining lists of instructions. Include some peephole optimization. *) -let rec emit = function - | [] -> () +let rec emit insns remaining = match insns with + | [] -> + (match remaining with + [] -> () + | (first::rest) -> emit first rest) (* Peephole optimizations *) | Kpush :: Kacc n :: c -> if n < 8 then out(opPUSHACC0 + n) else (out opPUSHACC; out_int n); - emit c + emit c remaining | Kpush :: Kenvacc n :: c -> if n >= 1 && n <= 4 then out(opPUSHENVACC1 + n - 1) else (out opPUSHENVACC; out_int n); - emit c + emit c remaining | Kpush :: Koffsetclosure ofs :: c -> if Int.equal ofs (-2) || Int.equal ofs 0 || Int.equal ofs 2 then out(opPUSHOFFSETCLOSURE0 + ofs / 2) else (out opPUSHOFFSETCLOSURE; out_int ofs); - emit c + emit c remaining | Kpush :: Kgetglobal id :: c -> - out opPUSHGETGLOBAL; slot_for_getglobal id; emit c + out opPUSHGETGLOBAL; slot_for_getglobal id; emit c remaining | Kpush :: Kconst (Const_b0 i) :: c -> if i >= 0 && i <= 3 then out (opPUSHCONST0 + i) else (out opPUSHCONSTINT; out_int i); - emit c + emit c remaining | Kpush :: Kconst const :: c -> out opPUSHGETGLOBAL; slot_for_const const; - emit c + emit c remaining | Kpop n :: Kjump :: c -> - out opRETURN; out_int n; emit c + out opRETURN; out_int n; emit c remaining | Ksequence(c1,c2)::c -> - emit c1; emit c2;emit c + emit c1 (c2::c::remaining) (* Default case *) | instr :: c -> - emit_instr instr; emit c + emit_instr instr; emit c remaining (* Initialization *) @@ -379,8 +382,8 @@ let repr_body_code = function let to_memory (init_code, fun_code, fv) = init(); - emit init_code; - emit fun_code; + emit init_code []; + emit fun_code []; (** Later uses of this string are all purely functional *) let code = Bytes.sub_string !out_buffer 0 !out_position in let code = CString.hcons code in diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 820514b08..2db91b8f8 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -34,7 +34,7 @@ GEXTEND Gram GLOBAL: bigint natural integer identref name ident var preident fullyqualid qualid reference dirpath ne_lstring - ne_string string pattern_ident pattern_identref by_notation smart_global; + ne_string string lstring pattern_ident pattern_identref by_notation smart_global; preident: [ [ s = IDENT -> s ] ] ; @@ -106,6 +106,9 @@ GEXTEND Gram string: [ [ s = STRING -> s ] ] ; + lstring: + [ [ s = string -> (!@loc, s) ] ] + ; integer: [ [ i = INT -> my_int_of_string (!@loc) i | "-"; i = INT -> - my_int_of_string (!@loc) i ] ] diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index d46880831..18807113c 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -1112,7 +1112,7 @@ GEXTEND Gram idl = LIST0 ident; ":="; c = constr; b = only_parsing -> VernacSyntacticDefinition (id,(idl,c),local,b) - | IDENT "Notation"; local = obsolete_locality; s = ne_lstring; ":="; + | IDENT "Notation"; local = obsolete_locality; s = lstring; ":="; c = constr; modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; sc = OPT [ ":"; sc = IDENT -> sc ] -> diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index c5823440a..b8405ca8c 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -267,6 +267,7 @@ module Prim = let integer = gec_gen "integer" let bigint = Gram.entry_create "Prim.bigint" let string = gec_gen "string" + let lstring = Gram.entry_create "Prim.lstring" let reference = make_gen_entry uprim "reference" let by_notation = Gram.entry_create "by_notation" let smart_global = Gram.entry_create "smart_global" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index d987bb455..cf5174af9 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -136,6 +136,7 @@ module Prim : val bigint : Bigint.bigint Gram.entry val integer : int Gram.entry val string : string Gram.entry + val lstring : string located Gram.entry val qualid : qualid located Gram.entry val fullyqualid : Id.t list located Gram.entry val reference : reference Gram.entry diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index a85afcbf0..edfe21d34 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1613,10 +1613,16 @@ let is_ground c gl = else tclFAIL 0 (str"Not ground") gl let autoapply c i gl = + let open Proofview.Notations in let flags = auto_unif_flags Evar.Set.empty (Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in let cty = pf_unsafe_type_of gl c in let ce = mk_clenv_from gl (c,cty) in - let tac = { enter = fun gl -> (unify_e_resolve false flags).enter gl - ((c,cty,Univ.ContextSet.empty),0,ce) } in - Proofview.V82.of_tactic (Proofview.Goal.nf_enter tac) gl + let enter gl = + (unify_e_resolve false flags).enter gl + ((c,cty,Univ.ContextSet.empty),0,ce) <*> + Proofview.tclEVARMAP >>= (fun sigma -> + let sigma = Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals sigma in + Proofview.Unsafe.tclEVARS sigma) + in + Proofview.V82.of_tactic (Proofview.Goal.nf_enter { enter }) gl diff --git a/test-suite/bugs/closed/4969.v b/test-suite/bugs/closed/4969.v new file mode 100644 index 000000000..4dee41e22 --- /dev/null +++ b/test-suite/bugs/closed/4969.v @@ -0,0 +1,11 @@ +Require Import Classes.Init. + +Class C A := c : A. +Instance nat_C : C nat := 0. +Instance bool_C : C bool := true. +Lemma silly {A} `{C A} : 0 = 0 -> c = c -> True. +Proof. auto. Qed. + +Goal True. + class_apply @silly; [reflexivity|]. + reflexivity. Fail Qed. diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index 07bbb60c4..52acad746 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -128,3 +128,10 @@ Notation " |- {{ a }} b" := (a=b) (no associativity, at level 10). Goal True. {{ exact I. }} Qed. + +(* Check that we can have notations without any symbol iff they are "only printing". *) +Fail Notation "" := (@nil). +Notation "" := (@nil) (only printing). + +(* Check that a notation cannot be neither parsing nor printing. *) +Fail Notation "'foobarkeyword'" := (@nil) (only parsing, only printing). diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 4dfb7af6a..22b1408c0 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -673,6 +673,7 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other print "VO=vo\n"; print "VOFILES:=$(VFILES:.v=.$(VO))\n"; classify_files_by_root "VOFILES" l inc; + classify_files_by_root "VFILES" l inc; print "GLOBFILES:=$(VFILES:.v=.glob)\n"; print "GFILES:=$(VFILES:.v=.g)\n"; print "HTMLFILES:=$(VFILES:.v=.html)\n"; diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 0aaf6afd7..7e98d114a 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -932,8 +932,8 @@ let find_precedence lev etyps symbols = let first_symbol = let rec aux = function | Break _ :: t -> aux t - | h :: t -> h - | [] -> assert false (* rule is known to be productive *) in + | h :: t -> Some h + | [] -> None in aux symbols in let last_is_terminal () = let rec aux b = function @@ -943,7 +943,8 @@ let find_precedence lev etyps symbols = | [] -> b in aux false symbols in match first_symbol with - | NonTerminal x -> + | None -> [],0 + | Some (NonTerminal x) -> (try match List.assoc x etyps with | ETConstr _ -> error "The level of the leftmost non-terminal cannot be changed." @@ -966,11 +967,11 @@ let find_precedence lev etyps symbols = if Option.is_empty lev then error "A left-recursive notation must have an explicit level." else [],Option.get lev) - | Terminal _ when last_is_terminal () -> + | Some (Terminal _) when last_is_terminal () -> if Option.is_empty lev then ([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."], 0) else [],Option.get lev - | _ -> + | Some _ -> if Option.is_empty lev then error "Cannot determine the level."; [],Option.get lev @@ -1049,6 +1050,9 @@ let compute_syntax_data df modifiers = let open SynData in let open NotationMods in let mods = interp_modifiers modifiers in + let onlyprint = mods.only_printing in + let onlyparse = mods.only_parsing in + if onlyprint && onlyparse then error "A notation cannot be both 'only printing' and 'only parsing'."; let assoc = Option.append mods.assoc (Some NonA) in let toks = split_notation_string df in let recvars,mainvars,symbols = analyze_notation_tokens toks in @@ -1058,7 +1062,7 @@ let compute_syntax_data df modifiers = let ntn_for_interp = make_notation_key symbols in let symbols' = remove_curly_brackets symbols in let ntn_for_grammar = make_notation_key symbols' in - check_rule_productivity symbols'; + if not onlyprint then check_rule_productivity symbols'; (* Misc *) let need_squash = not (List.equal Notation.symbol_eq symbols symbols') in |