From c487e02b0b8bffbe3135d7024f25d03a2f5f1af4 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 29 Jul 2015 16:37:29 +0200 Subject: Adding test for bug #3779. --- test-suite/bugs/closed/3779.v | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 test-suite/bugs/closed/3779.v diff --git a/test-suite/bugs/closed/3779.v b/test-suite/bugs/closed/3779.v new file mode 100644 index 0000000000..eb0d206c5c --- /dev/null +++ b/test-suite/bugs/closed/3779.v @@ -0,0 +1,11 @@ +Set Universe Polymorphism. +Record UnitSubuniverse := { a : Type@{sm} ; x : (Type@{sm} : Type@{lg}) ; inO_internal : Type@{lg} -> Type@{lg} }. +Class In (O : UnitSubuniverse@{sm lg}) (T : Type@{lg}) := in_inO_internal : inO_internal O T. +Section foo. + Universes sm lg. + Context (O : UnitSubuniverse@{sm lg}). + Context {A : Type@{sm}}. + Context (H' : forall (C : Type@{lg}) `{In@{sm lg} O C} (f : A -> C), In@{sm lg} O C). + Fail Check (H' : forall (C : Type@{lg}) `{In@{i j} O C} (f : A -> C), In@{j i} O C). + Fail Context (H'' : forall (C : Type@{lg}) `{In@{i j} O C} (f : A -> C), In@{j i} O C). +End foo. -- cgit v1.2.3 From 8506a4d60417ce498ce4525de044a6a590a5e922 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 29 Jul 2015 18:38:27 +0200 Subject: Rewrite the main loop of coq-tex. Before this commit, coq-tex was reading the .v file and was guessing how many lines from the coqtop output it should display. Now, it reads the coqtop output and it guesses how many lines from the .v file it should display. That way, coq-tex no longer needs to embed a parser; it relies on coqtop for parsing. This is much more robust and makes it possible to properly handle script such as the following one: Goal { True } + { False }. { left. exact I. } As before, if there is a way for a script to produce something that looks like a prompt (that is, a line that starts with "foo < "), coq-tex will be badly confused. --- tools/coq_tex.ml | 160 ++++++++++++++++++++++++++----------------------------- 1 file changed, 76 insertions(+), 84 deletions(-) diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml index fc652f584c..9a5ff86ef3 100644 --- a/tools/coq_tex.ml +++ b/tools/coq_tex.ml @@ -24,10 +24,7 @@ let hrule = ref false let small = ref false let boot = ref false -let coq_prompt = Str.regexp "Coq < " -let any_prompt = Str.regexp "^[A-Z0-9a-z_\\$']* < " - -let remove_prompt s = Str.replace_first any_prompt "" s +let any_prompt = Str.regexp "[A-Z0-9a-z_\\$']* < " (* First pass: extract the Coq phrases to evaluate from [texfile] * and put them into the file [inputv] *) @@ -66,9 +63,6 @@ let extract texfile inputv = let begin_coq_example = Str.regexp "\\\\begin{coq_\\(example\\|example\\*\\|example\\#\\)}[ \t]*$" let begin_coq_eval = Str.regexp "\\\\begin{coq_eval}[ \t]*$" -let end_coq_example = Str.regexp "\\\\end{coq_\\(example\\|example\\*\\|example\\#\\)}[ \t]*$" -let end_coq_eval = Str.regexp "\\\\end{coq_eval}[ \t]*$" -let dot_end_line = Str.regexp "\\(\\.\\|}\\)[ \t]*\\((\\*.*\\*)\\)?[ \t]*$" let has_match r s = try let _ = Str.search_forward r s 0 in true with Not_found -> false @@ -111,99 +105,97 @@ let insert texfile coq_output result = let c_tex = open_in texfile in let c_coq = open_in coq_output in let c_out = open_out result in - (* next_block k : this function reads the next block of Coq output - * removing the k leading prompts. - * it returns the block as a list of string) *) - let last_read = ref "" in - let next_block k = - if !last_read = "" then last_read := input_line c_coq; - (* skip k prompts *) - for _i = 1 to k do - last_read := remove_prompt !last_read; - done; + (* read lines until a prompt is found (starting from the second line), + purge prompts on the first line and return their number *) + let last_read = ref (input_line c_coq) in + let read_output () = + let first = !last_read in + let nb = ref 0 in + (* remove the leading prompts *) + let rec skip_prompts pos = + if Str.string_match any_prompt first pos then + let () = incr nb in + skip_prompts (Str.match_end ()) + else pos in + let first = + let start = skip_prompts 0 in + String.sub first start (String.length first - start) in (* read and return the following lines until a prompt is found *) let rec read_lines () = let s = input_line c_coq in if Str.string_match any_prompt s 0 then begin last_read := s; [] end else - s :: (read_lines ()) - in - let first = !last_read in first :: (read_lines ()) - in - (* we are just after \end{coq_...} block *) - let rec just_after () = + s :: read_lines () in + (first :: read_lines (), !nb) in + let unhandled_output = ref None in + (* we are inside a \begin{coq_...} ... \end{coq_...} block + * show_... tell what kind of block it is *) + let rec inside show_answers show_questions not_first = let s = input_line c_tex in - if Str.string_match begin_coq_example s 0 then begin - inside (Str.matched_group 1 s <> "example*") - (Str.matched_group 1 s <> "example#") 0 false - end - else begin - if !hrule then output_string c_out "\\hrulefill\\\\\n"; - output_string c_out "\\end{flushleft}\n"; - if !small then output_string c_out "\\end{small}\n"; - if Str.string_match begin_coq_eval s 0 then - eval 0 + if not (Str.string_match end_coq s 0) then begin + let (bl,n) = + match !unhandled_output with + | Some some -> unhandled_output := None; some + | None -> read_output () in + assert (n > 0); + if not_first then output_string c_out "\\medskip\n"; + if !verbose then Printf.printf "Coq < %s\n" s; + if show_questions then encapsule false c_out ("Coq < " ^ s); + let rec read_lines k = + if k = 0 then [] + else + let s = input_line c_tex in + if Str.string_match end_coq s 0 then [] + else s :: read_lines (k - 1) in + let al = read_lines (n - 1) in + if !verbose then List.iter (Printf.printf " %s\n") al; + if show_questions then + List.iter (fun s -> encapsule false c_out (" " ^ s)) al; + let la = n - 1 - List.length al in + if la <> 0 then + (* this happens when the block ends with a comment; the output + is for the command at the beginning of the next block *) + unhandled_output := Some (bl, la) else begin - output_string c_out (s ^ "\n"); - outside () + if !verbose then List.iter print_endline bl; + if show_answers then print_block c_out bl; + inside show_answers show_questions (show_answers || show_questions) end - end + end in (* we are outside of a \begin{coq_...} ... \end{coq_...} block *) - and outside () = - let s = input_line c_tex in - if Str.string_match begin_coq_example s 0 then begin + let rec outside just_after = + let start_block () = if !small then output_string c_out "\\begin{small}\n"; output_string c_out "\\begin{flushleft}\n"; + if !hrule then output_string c_out "\\hrulefill\\\\\n" in + let end_block () = if !hrule then output_string c_out "\\hrulefill\\\\\n"; - inside (Str.matched_group 1 s <> "example*") - (Str.matched_group 1 s <> "example#") 0 true - end else if Str.string_match begin_coq_eval s 0 then - eval 0 - else begin - output_string c_out (s ^ "\n"); - outside () - end - (* we are inside a \begin{coq_example?} ... \end{coq_example?} block - * show_answers tells what kind of block it is - * k is the number of lines read until now *) - and inside show_answers show_questions k first_block = + output_string c_out "\\end{flushleft}\n"; + if !small then output_string c_out "\\end{small}\n" in let s = input_line c_tex in - if Str.string_match end_coq_example s 0 then begin - just_after () + if Str.string_match begin_coq s 0 then begin + let kind = Str.matched_group 1 s in + if kind = "eval" then begin + if just_after then end_block (); + inside false false false; + outside false + end else begin + let show_answers = kind <> "example*" in + let show_questions = kind <> "example#" in + if not just_after then start_block (); + inside show_answers show_questions just_after; + outside true + end end else begin - let prompt = if k = 0 then "Coq < " else " " in - if !verbose then Printf.printf "%s%s\n" prompt s; - if (not first_block) && k=0 then output_string c_out "\\medskip\n"; - if show_questions then encapsule false c_out (prompt ^ s); - if has_match dot_end_line s then begin - let bl = next_block (succ k) in - if !verbose then List.iter print_endline bl; - if show_answers then print_block c_out bl; - inside show_answers show_questions 0 false - end else - inside show_answers show_questions (succ k) first_block - end - (* we are inside a \begin{coq_eval} ... \end{coq_eval} block - * k is the number of lines read until now *) - and eval k = - let s = input_line c_tex in - if Str.string_match end_coq_eval s 0 then - outside () - else begin - if !verbose then Printf.printf "Coq < %s\n" s; - if has_match dot_end_line s then - let bl = next_block (succ k) in - if !verbose then List.iter print_endline bl; - eval 0 - else - eval (succ k) - end - in + if just_after then end_block (); + output_string c_out (s ^ "\n"); + outside false + end in try - let _ = next_block 0 in (* to skip the Coq banner *) - let _ = next_block 0 in (* to skip the Coq answer to Set Printing Width *) - outside () + let _ = read_output () in (* to skip the Coq banner *) + let _ = read_output () in (* to skip the Coq answer to Set Printing Width *) + outside false with End_of_file -> begin close_in c_tex; close_in c_coq; -- cgit v1.2.3 From f7180b6a33349ded33269d3ba25a9e0ed75d1896 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 29 Jul 2015 18:46:18 +0200 Subject: Improve the FAQ a bit. --- doc/faq/FAQ.tex | 33 +++++++++++++++++++++------------ 1 file changed, 21 insertions(+), 12 deletions(-) diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index b03aa64090..899b196350 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -849,7 +849,7 @@ mapped to {\Prop}. Use some theorem or assumption or use the {\split} tactic. \begin{coq_example} -Goal forall A B:Prop, A->B-> A/\B. +Goal forall A B:Prop, A -> B -> A/\B. intros. split. assumption. @@ -859,16 +859,25 @@ Qed. \Question{My goal contains a conjunction as an hypothesis, how can I use it?} -If you want to decompose your hypothesis into other hypothesis you can use the {\decompose} tactic: +If you want to decompose a hypothesis into several hypotheses, you can +use the {\destruct} tactic: \begin{coq_example} -Goal forall A B:Prop, A/\B-> B. +Goal forall A B:Prop, A/\B -> B. intros. -decompose [and] H. +destruct H as [H1 H2]. assumption. Qed. \end{coq_example} +You can also perform the destruction at the time of introduction: + +\begin{coq_example} +Goal forall A B:Prop, A/\B -> B. +intros A B [H1 H2]. +assumption. +Qed. +\end{coq_example} \Question{My goal is a disjunction, how can I prove it?} @@ -878,7 +887,7 @@ reasoning step, use the {\tt classic} axiom to prove the right part with the ass that the left part of the disjunction is false. \begin{coq_example} -Goal forall A B:Prop, A-> A\/B. +Goal forall A B:Prop, A -> A\/B. intros. left. assumption. @@ -890,14 +899,14 @@ An example using classical reasoning: \begin{coq_example} Require Import Classical. -Ltac classical_right := -match goal with -| _:_ |-?X1 \/ _ => (elim (classic X1);intro;[left;trivial|right]) +Ltac classical_right := +match goal with +| _:_ |- ?X1 \/ _ => (elim (classic X1);intro;[left;trivial|right]) end. -Ltac classical_left := -match goal with -| _:_ |- _ \/?X1 => (elim (classic X1);intro;[right;trivial|left]) +Ltac classical_left := +match goal with +| _:_ |- _ \/ ?X1 => (elim (classic X1);intro;[right;trivial|left]) end. @@ -1199,7 +1208,7 @@ Qed. \end{coq_example} -\Question{My goal is an inequality on integers in Presburger's arithmetic (an expression build from +,-,constants and variables), how can I prove it?} +\Question{My goal is an inequality on integers in Presburger's arithmetic (an expression build from $+$, $-$, constants, and variables), how can I prove it?} \begin{coq_example} -- cgit v1.2.3 From ffb2788b92323901c1024d1eae221e4beb4b6670 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 29 Jul 2015 19:07:54 +0200 Subject: Remove empty commands from the output of coq-tex. --- tools/coq_tex.ml | 29 +++++++++++++++++++---------- 1 file changed, 19 insertions(+), 10 deletions(-) diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml index 9a5ff86ef3..9c91889a03 100644 --- a/tools/coq_tex.ml +++ b/tools/coq_tex.ml @@ -129,16 +129,20 @@ let insert texfile coq_output result = s :: read_lines () in (first :: read_lines (), !nb) in let unhandled_output = ref None in + let read_output () = + match !unhandled_output with + | Some some -> unhandled_output := None; some + | None -> read_output () in (* we are inside a \begin{coq_...} ... \end{coq_...} block * show_... tell what kind of block it is *) - let rec inside show_answers show_questions not_first = + let rec inside show_answers show_questions not_first discarded = let s = input_line c_tex in - if not (Str.string_match end_coq s 0) then begin - let (bl,n) = - match !unhandled_output with - | Some some -> unhandled_output := None; some - | None -> read_output () in - assert (n > 0); + if s = "" then + inside show_answers show_questions not_first (discarded + 1) + else if not (Str.string_match end_coq s 0) then begin + let (bl,n) = read_output () in + assert (n > discarded); + let n = n - discarded in if not_first then output_string c_out "\\medskip\n"; if !verbose then Printf.printf "Coq < %s\n" s; if show_questions then encapsule false c_out ("Coq < " ^ s); @@ -160,8 +164,13 @@ let insert texfile coq_output result = else begin if !verbose then List.iter print_endline bl; if show_answers then print_block c_out bl; - inside show_answers show_questions (show_answers || show_questions) + inside show_answers show_questions (show_answers || show_questions) 0 end + end else if discarded > 0 then begin + (* this happens when the block ends with an empty line *) + let (bl,n) = read_output () in + assert (n > discarded); + unhandled_output := Some (bl, n - discarded) end in (* we are outside of a \begin{coq_...} ... \end{coq_...} block *) let rec outside just_after = @@ -178,13 +187,13 @@ let insert texfile coq_output result = let kind = Str.matched_group 1 s in if kind = "eval" then begin if just_after then end_block (); - inside false false false; + inside false false false 0; outside false end else begin let show_answers = kind <> "example*" in let show_questions = kind <> "example#" in if not just_after then start_block (); - inside show_answers show_questions just_after; + inside show_answers show_questions just_after 0; outside true end end else begin -- cgit v1.2.3 From 9a5fb78ef3c7c5d4f568a4d04e169475e9105def Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 29 Jul 2015 19:58:39 +0200 Subject: Make coq-tex more robust with respect to the (non-)command on the last line. --- tools/coq_tex.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml index 9c91889a03..f65708698c 100644 --- a/tools/coq_tex.ml +++ b/tools/coq_tex.ml @@ -55,7 +55,10 @@ let extract texfile inputv = ("Set Printing Width " ^ (string_of_int !linelen) ^".\n"); outside () with End_of_file -> - begin close_in chan_in; close_out chan_out end + (* a dummy command, just in case the last line was a comment *) + output_string chan_out "Set Printing Width 78.\n"; + close_in chan_in; + close_out chan_out (* Second pass: insert the answers of Coq from [coq_output] into the * TeX file [texfile]. The result goes in file [result]. *) -- cgit v1.2.3 From 5383cdc276d9ba7f1bb05bfe5aeae0a25edbd4a4 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 30 Jul 2015 07:56:49 +0200 Subject: Remove usage of Printexc.catch in the tools, as it is deprecated since 2001. "This function is deprecated: the runtime system is now able to print uncaught exceptions as precisely as Printexc.catch does. Moreover, calling Printexc.catch makes it harder to track the location of the exception using the debugger or the stack backtrace facility. So, do not use Printexc.catch in new code." --- tools/coq_makefile.ml | 4 +--- tools/coq_tex.ml | 4 +--- tools/coqdep_boot.ml | 4 +--- tools/coqdoc/main.ml | 4 +--- tools/coqwc.mll | 4 +--- tools/gallina.ml | 5 +---- 6 files changed, 6 insertions(+), 19 deletions(-) diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 8f4772e286..71134c2d97 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -842,11 +842,9 @@ let do_makefile args = if not (makefile = None) then close_out !output_channel; exit 0 -let main () = +let _ = let args = if Array.length Sys.argv = 1 then usage (); List.tl (Array.to_list Sys.argv) in do_makefile args - -let _ = Printexc.catch main () diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml index f65708698c..53444cee78 100644 --- a/tools/coq_tex.ml +++ b/tools/coq_tex.ml @@ -285,7 +285,7 @@ let find_coqtop () = "coqtop" end -let main () = +let _ = parse_cl (); if !image = "" then image := Filename.quote (find_coqtop ()); if !boot then image := !image ^ " -boot"; @@ -298,5 +298,3 @@ let main () = flush stdout end; List.iter one_file (List.rev !files) - -let _ = Printexc.catch main () diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml index 2d5fd36a63..64ce66d2d1 100644 --- a/tools/coqdep_boot.ml +++ b/tools/coqdep_boot.ml @@ -30,7 +30,7 @@ let rec parse = function | f :: ll -> treat_file None f; parse ll | [] -> () -let coqdep_boot () = +let _ = let () = option_boot := true in if Array.length Sys.argv < 2 then exit 1; parse (List.tl (Array.to_list Sys.argv)); @@ -47,5 +47,3 @@ let coqdep_boot () = end; if !option_c then mL_dependencies (); coq_dependencies () - -let _ = Printexc.catch coqdep_boot () diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 9531cd2b07..2554ed495b 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -557,10 +557,8 @@ let produce_output fl = (*s \textbf{Main program.} Print the banner, parse the command line, read the files and then call [produce_document] from module [Web]. *) -let main () = +let _ = let files = parse () in Index.init_coqlib_library (); if not !quiet then banner (); if files <> [] then produce_output files - -let _ = Printexc.catch main () diff --git a/tools/coqwc.mll b/tools/coqwc.mll index 417ec5355c..9a42553da2 100644 --- a/tools/coqwc.mll +++ b/tools/coqwc.mll @@ -276,7 +276,7 @@ let rec parse = function (*s Main program. *) -let main () = +let _ = let files = parse (List.tl (Array.to_list Sys.argv)) in if not (!spec_only || !proof_only) then printf " spec proof comments\n"; @@ -285,8 +285,6 @@ let main () = | [f] -> process_file f | _ -> List.iter process_file files; print_totals () -let _ = Printexc.catch main () - (*i*)}(*i*) diff --git a/tools/gallina.ml b/tools/gallina.ml index 279919c582..5ce19e7f88 100644 --- a/tools/gallina.ml +++ b/tools/gallina.ml @@ -39,7 +39,7 @@ let traite_stdin () = with Sys_error _ -> () -let gallina () = +let _ = let lg_command = Array.length Sys.argv in if lg_command < 2 then begin output_string stderr "Usage: gallina [-] [-stdout] file1 file2 ...\n"; @@ -59,6 +59,3 @@ let gallina () = traite_stdin () else List.iter traite_fichier !vfiles - -let _ = Printexc.catch gallina () - -- cgit v1.2.3 From 52940b19a7f47fa5022d75c5679785ac90aaa0dc Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 30 Jul 2015 08:10:05 +0200 Subject: Remove unused variables. --- tools/coq_tex.ml | 13 +------------ 1 file changed, 1 insertion(+), 12 deletions(-) diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml index 53444cee78..26a9715ef7 100644 --- a/tools/coq_tex.ml +++ b/tools/coq_tex.ml @@ -63,17 +63,6 @@ let extract texfile inputv = (* Second pass: insert the answers of Coq from [coq_output] into the * TeX file [texfile]. The result goes in file [result]. *) -let begin_coq_example = - Str.regexp "\\\\begin{coq_\\(example\\|example\\*\\|example\\#\\)}[ \t]*$" -let begin_coq_eval = Str.regexp "\\\\begin{coq_eval}[ \t]*$" - -let has_match r s = - try let _ = Str.search_forward r s 0 in true with Not_found -> false - -let percent = Str.regexp "%" -let bang = Str.regexp "!" -let expos = Str.regexp "^" - let tex_escaped s = let dollar = "\\$" and backslash = "\\\\" and expon = "\\^" in let delims = Str.regexp ("[_{}&%#" ^ dollar ^ backslash ^ expon ^"~ <>'`]") in @@ -216,7 +205,7 @@ let insert texfile coq_output result = (* Process of one TeX file *) -let rm f = try Sys.remove f with any -> () +let rm f = try Sys.remove f with _ -> () let one_file texfile = let inputv = Filename.temp_file "coq_tex" ".v" in -- cgit v1.2.3 From 070139d3a82ea23e4d050dd5ccebe3f17047cc62 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 30 Jul 2015 08:19:10 +0200 Subject: Fix broken regexp. Characters do not need to be escaped in character ranges. It just had the effect of matching backslashes four times. --- tools/coq_tex.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml index 26a9715ef7..8218f84f1f 100644 --- a/tools/coq_tex.ml +++ b/tools/coq_tex.ml @@ -64,8 +64,7 @@ let extract texfile inputv = * TeX file [texfile]. The result goes in file [result]. *) let tex_escaped s = - let dollar = "\\$" and backslash = "\\\\" and expon = "\\^" in - let delims = Str.regexp ("[_{}&%#" ^ dollar ^ backslash ^ expon ^"~ <>'`]") in + let delims = Str.regexp "[_{}&%#$\\^~ <>'`]" in let adapt_delim = function | "_" | "{" | "}" | "&" | "%" | "#" | "$" as c -> "\\"^c | "\\" -> "{\\char'134}" -- cgit v1.2.3 From a9f3607ae72517156301570a4ffa05908609b7e0 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 30 Jul 2015 08:30:00 +0200 Subject: Fix width of underscore in coq_tex output. --- tools/coq_tex.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml index 8218f84f1f..dbdc2e9db1 100644 --- a/tools/coq_tex.ml +++ b/tools/coq_tex.ml @@ -66,7 +66,8 @@ let extract texfile inputv = let tex_escaped s = let delims = Str.regexp "[_{}&%#$\\^~ <>'`]" in let adapt_delim = function - | "_" | "{" | "}" | "&" | "%" | "#" | "$" as c -> "\\"^c + | "{" | "}" | "&" | "%" | "#" | "$" as c -> "\\"^c + | "_" -> "{\\char`\\_}" | "\\" -> "{\\char'134}" | "^" -> "{\\char'136}" | "~" -> "{\\char'176}" -- cgit v1.2.3 From 35a743761478fffaaafd54368a5dcbcecd3133eb Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 30 Jul 2015 09:53:30 +0200 Subject: Fix some broken Coq scripts in the documentation. --- doc/faq/FAQ.tex | 20 ++++++++++++-------- doc/refman/Micromega.tex | 8 ++++---- doc/refman/Program.tex | 10 +++++----- doc/refman/RefMan-ext.tex | 15 ++++++++------- doc/refman/RefMan-gal.tex | 7 +++++-- doc/refman/RefMan-tac.tex | 6 +++--- doc/refman/Setoid.tex | 8 ++++---- 7 files changed, 41 insertions(+), 33 deletions(-) diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index 899b196350..d75c3b8a62 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -1570,7 +1570,7 @@ If you type for instance the following ``definition'': Reset Initial. \end{coq_eval} \begin{coq_example} -Definition max (n p : nat) := if n <= p then p else n. +Fail Definition max (n p : nat) := if n <= p then p else n. \end{coq_example} As \Coq~ says, the term ``~\texttt{n <= p}~'' is a proposition, i.e. a @@ -1738,7 +1738,7 @@ mergesort} as an example). the arguments of the loop. \begin{coq_eval} -Open Scope R_scope. +Reset Initial. Require Import List. \end{coq_eval} @@ -1751,21 +1751,25 @@ Definition R (a b:list nat) := length a < length b. \begin{coq_example*} Lemma Rwf : well_founded R. \end{coq_example*} +\begin{coq_eval} +Admitted. +\end{coq_eval} \item Define the step function (which needs proofs that recursive calls are on smaller arguments). -\begin{verbatim} -Definition split (l : list nat) - : {l1: list nat | R l1 l} * {l2 : list nat | R l2 l} - := (* ... *) . -Definition concat (l1 l2 : list nat) : list nat := (* ... *) . +\begin{coq_example*} +Definition split (l : list nat) + : {l1: list nat | R l1 l} * {l2 : list nat | R l2 l}. +Admitted. +Definition concat (l1 l2 : list nat) : list nat. +Admitted. Definition merge_step (l : list nat) (f: forall l':list nat, R l' l -> list nat) := let (lH1,lH2) := (split l) in let (l1,H1) := lH1 in let (l2,H2) := lH2 in concat (f l1 H1) (f l2 H2). -\end{verbatim} +\end{coq_example*} \item Define the recursive function by fixpoint on the step function. diff --git a/doc/refman/Micromega.tex b/doc/refman/Micromega.tex index 4a4fab1538..551f6c205b 100644 --- a/doc/refman/Micromega.tex +++ b/doc/refman/Micromega.tex @@ -140,12 +140,12 @@ Rougthly speaking, the deductive power of {\tt lia} is the combined deductive po However, it solves linear goals that {\tt omega} and {\tt romega} do not solve, such as the following so-called \emph{omega nightmare}~\cite{TheOmegaPaper}. \begin{coq_example*} - Goal forall x y, - 27 <= 11 * x + 13 * y <= 45 -> - -10 <= 7 * x - 9 * y <= 4 -> False. +Goal forall x y, + 27 <= 11 * x + 13 * y <= 45 -> + -10 <= 7 * x - 9 * y <= 4 -> False. \end{coq_example*} \begin{coq_eval} -intro x; lia. +intros x y; lia. \end{coq_eval} The estimation of the relative efficiency of lia \emph{vs} {\tt omega} and {\tt romega} is under evaluation. diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex index 76bcaaae67..8e078e9814 100644 --- a/doc/refman/Program.tex +++ b/doc/refman/Program.tex @@ -42,20 +42,20 @@ operation (see Section~\ref{Caseexpr}). generalized by the corresponding equality. As an example, the expression: -\begin{coq_example*} +\begin{verbatim} match x with | 0 => t | S n => u end. -\end{coq_example*} +\end{verbatim} will be first rewritten to: -\begin{coq_example*} +\begin{verbatim} (match x as y return (x = y -> _) with | 0 => fun H : x = 0 -> t | S n => fun H : x = S n -> u end) (eq_refl n). -\end{coq_example*} - +\end{verbatim} + This permits to get the proper equalities in the context of proof obligations inside clauses, without which reasoning is very limited. diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index d63d22a71c..d21c91201d 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -749,9 +749,12 @@ Function plus (n m : nat) {struct n} : nat := each branch. Function does not support partial application of the function being defined. Thus, the following example cannot be accepted due to the presence of partial application of \ident{wrong} into the body of \ident{wrong}~: +\begin{coq_eval} +Require List. +\end{coq_eval} \begin{coq_example*} - Function wrong (C:nat) : nat := - List.hd(List.map wrong (C::nil)). +Fail Function wrong (C:nat) : nat := + List.hd 0 (List.map wrong (C::nil)). \end{coq_example*} For now dependent cases are not treated for non structurally terminating functions. @@ -1633,13 +1636,11 @@ one of the other arguments, then only the type of the first of these arguments is taken into account, and not an upper type of all of them. As a consequence, the inference of the implicit argument of ``='' fails in - \begin{coq_example*} -Check nat = Prop. +Fail Check nat = Prop. \end{coq_example*} -but succeeds in - +but succeeds in \begin{coq_example*} Check Prop = nat. \end{coq_example*} @@ -2010,7 +2011,7 @@ binding as well as those introduced by tactic binding. The expression {\expr} can be any tactic expression as described at section~\ref{TacticLanguage}. \begin{coq_example*} -Definition foo (x : A) : A := $( exact x )$. +Definition foo (x : nat) : nat := $( exact x )$. \end{coq_example*} This construction is useful when one wants to define complicated terms using diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index cf83d0c722..9b527053c3 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -587,6 +587,9 @@ is a variable, the {\tt as} clause can be omitted and the term being matched can serve itself as binding name in the return type. For instance, the following alternative definition is accepted and has the same meaning as the previous one. +\begin{coq_eval} +Reset bool_case. +\end{coq_eval} \begin{coq_example*} Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false) := match b return or (eq bool b true) (eq bool b false) with @@ -623,7 +626,7 @@ For instance, in the following example: \begin{coq_example*} Definition eq_sym (A:Type) (x y:A) (H:eq A x y) : eq A y x := match H in eq _ _ z return eq A z x with - | eq_refl => eq_refl A x + | eq_refl _ _ => eq_refl A x end. \end{coq_example*} the type of the branch has type {\tt eq~A~x~x} because the third @@ -1120,7 +1123,7 @@ This is an alternative definition of lists where we specify the arguments of the constructors rather than their full type. \item \begin{coq_example*} -Variant sum (A B:Set) : Set := left : A->sum A B | right : B->Sum A B. +Variant sum (A B:Set) : Set := left : A -> sum A B | right : B -> sum A B. \end{coq_example*} The {\tt Variant} keyword is identical to the {\tt Inductive} keyword, except that it disallows recursive definition of types (in particular diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 8f9ba1ec60..cc262708ab 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3129,7 +3129,7 @@ follows: \comindex{Arguments} A constant can be marked to be never unfolded by \texttt{cbn} or \texttt{simpl}: \begin{coq_example*} -Arguments minus x y : simpl never. +Arguments minus n m : simpl never. \end{coq_example*} After that command an expression like \texttt{(minus (S x) y)} is left untouched by the tactics \texttt{cbn} and \texttt{simpl}. @@ -3156,7 +3156,7 @@ A constant can be marked to be unfolded only if an entire set of arguments evaluates to a constructor. The {\tt !} symbol can be used to mark such arguments. \begin{coq_example*} -Arguments minus !x !y. +Arguments minus !n !m. \end{coq_example*} After that command, the expression {\tt (minus (S x) y)} is left untouched by {\tt simpl}, while {\tt (minus (S x) (S y))} is reduced to {\tt (minus x y)}. @@ -3164,7 +3164,7 @@ After that command, the expression {\tt (minus (S x) y)} is left untouched by A special heuristic to determine if a constant has to be unfolded can be activated with the following command: \begin{coq_example*} -Arguments minus x y : simpl nomatch. +Arguments minus n m : simpl nomatch. \end{coq_example*} The heuristic avoids to perform a simplification step that would expose a {\tt match} construct in head position. For example the diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex index 3770ba574b..2c9602a229 100644 --- a/doc/refman/Setoid.tex +++ b/doc/refman/Setoid.tex @@ -658,17 +658,17 @@ arguments (or whatever subrelation of the pointwise extension). For example, one could declare the \texttt{map} combinator on lists as a morphism: \begin{coq_eval} -Require Import List. +Require Import List Setoid Morphisms. Set Implicit Arguments. Inductive list_equiv {A:Type} (eqA : relation A) : relation (list A) := | eq_nil : list_equiv eqA nil nil -| eq_cons : forall x y, eqA x y -> +| eq_cons : forall x y, eqA x y -> forall l l', list_equiv eqA l l' -> list_equiv eqA (x :: l) (y :: l'). +Generalizable All Variables. \end{coq_eval} \begin{coq_example*} Instance map_morphism `{Equivalence A eqA, Equivalence B eqB} : - Proper ((eqA ==> eqB) ==> list_equiv eqA ==> list_equiv eqB) - (@map A B). + Proper ((eqA ==> eqB) ==> list_equiv eqA ==> list_equiv eqB) (@map A B). \end{coq_example*} where \texttt{list\_equiv} implements an equivalence on lists -- cgit v1.2.3 From 8ccd08f6bc6bcbda01cf65d2b6e7ecd62e4c4972 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 30 Jul 2015 10:04:49 +0200 Subject: Remove some output of Qed in the FAQ. --- doc/faq/FAQ.tex | 143 ++++++++++++++++++++++++++++++++++++++------------------ 1 file changed, 98 insertions(+), 45 deletions(-) diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index d75c3b8a62..3e14e330b0 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -854,8 +854,10 @@ intros. split. assumption. assumption. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{My goal contains a conjunction as an hypothesis, how can I use it?} @@ -867,8 +869,10 @@ Goal forall A B:Prop, A/\B -> B. intros. destruct H as [H1 H2]. assumption. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} You can also perform the destruction at the time of introduction: @@ -876,8 +880,10 @@ You can also perform the destruction at the time of introduction: Goal forall A B:Prop, A/\B -> B. intros A B [H1 H2]. assumption. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{My goal is a disjunction, how can I prove it?} @@ -891,8 +897,10 @@ Goal forall A B:Prop, A -> A\/B. intros. left. assumption. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} An example using classical reasoning: @@ -914,8 +922,10 @@ Goal forall A B:Prop, (~A -> B) -> A\/B. intros. classical_right. auto. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{My goal is an universally quantified statement, how can I prove it?} @@ -944,8 +954,10 @@ Goal exists x:nat, forall y, x+y=y. exists 0. intros. auto. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{My goal is solvable by some lemma, how can I prove it?} @@ -963,8 +975,10 @@ Qed. Goal 3+0 = 3. apply mylemma. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} @@ -981,8 +995,10 @@ Just use the {\reflexivity} tactic. Goal forall x, 0+x = x. intros. reflexivity. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{My goal is a {\tt let x := a in ...}, how can I prove it?} @@ -1013,8 +1029,10 @@ Goal forall x y : nat, x=y -> y=x. intros. symmetry. assumption. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{My hypothesis is an equality, how can I swap the left and right hand terms?} @@ -1025,8 +1043,10 @@ Goal forall x y : nat, x=y -> y=x. intros. symmetry in H. assumption. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{My goal is an equality, how can I prove it by transitivity?} @@ -1038,8 +1058,10 @@ intros. transitivity y. assumption. assumption. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{My goal would be solvable using {\tt apply;assumption} if it would not create meta-variables, how can I prove it?} @@ -1075,7 +1097,6 @@ eapply trans. apply H. auto. Qed. - \end{coq_example} \Question{My goal is solvable by some lemma within a set of lemmas and I don't want to remember which one, how can I prove it?} @@ -1112,8 +1133,10 @@ Use the {\assumption} tactic. Goal 1=1 -> 1=1. intro. assumption. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{My goal appears twice in the hypotheses and I want to choose which one is used, how can I do it?} @@ -1123,8 +1146,10 @@ Use the {\exact} tactic. Goal 1=1 -> 1=1 -> 1=1. intros. exact H0. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{What can be the difference between applying one hypothesis or another in the context of the last question?} @@ -1140,8 +1165,10 @@ Just use the {\tauto} tactic. Goal forall A B:Prop, A-> (A\/B) /\ A. intros. tauto. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{My goal is a first order formula, how can I prove it?} @@ -1158,8 +1185,10 @@ Just use the {\congruence} tactic. Goal forall a b c d e, a=d -> b=e -> c+b=d -> c+e=a. intros. congruence. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{My goal is a disequality solvable by a sequence of rewrites, how can I prove it?} @@ -1170,8 +1199,10 @@ Just use the {\congruence} tactic. Goal forall a b c d, a<>d -> b=a -> d=c+b -> b<>c+b. intros. congruence. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{My goal is an equality on some ring (e.g. natural numbers), how can I prove it?} @@ -1182,11 +1213,13 @@ Just use the {\ring} tactic. Require Import ZArith. Require Ring. Local Open Scope Z_scope. -Goal forall a b : Z, (a+b)*(a+b) = a*a + 2*a*b + b*b. +Goal forall a b : Z, (a+b)*(a+b) = a*a + 2*a*b + b*b. intros. ring. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{My goal is an equality on some field (e.g. real numbers), how can I prove it?} @@ -1196,16 +1229,14 @@ Just use the {\field} tactic. Require Import Reals. Require Ring. Local Open Scope R_scope. -Goal forall a b : R, b*a<>0 -> (a/b) * (b/a) = 1. +Goal forall a b : R, b*a<>0 -> (a/b) * (b/a) = 1. intros. field. -cut (b*a <>0 -> a<>0). -cut (b*a <>0 -> b<>0). -auto. -auto with real. -auto with real. -Qed. +split ; auto with real. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{My goal is an inequality on integers in Presburger's arithmetic (an expression build from $+$, $-$, constants, and variables), how can I prove it?} @@ -1215,11 +1246,13 @@ Qed. Require Import ZArith. Require Omega. Local Open Scope Z_scope. -Goal forall a : Z, a>0 -> a+a > a. +Goal forall a : Z, a>0 -> a+a > a. intros. omega. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{My goal is an equation solvable using equational hypothesis on some ring (e.g. natural numbers), how can I prove it?} @@ -1242,16 +1275,22 @@ assert (A->C). intro;apply H0;apply H;assumption. apply H2. assumption. +\end{coq_example} +\begin{coq_example*} Qed. +\end{coq_example*} +\begin{coq_example} Goal forall A B C D : Prop, (A -> B) -> (B->C) -> A -> C. intros. cut (A->C). intro. apply H2;assumption. intro;apply H0;apply H;assumption. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} @@ -1342,8 +1381,10 @@ H1 *) intros A B C H H0 H1. repeat split;assumption. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{I want to automatize the use of some tactic, how can I do it?} @@ -1356,8 +1397,10 @@ Goal forall A B C : Prop, A -> B/\C -> A/\B/\C. Proof with assumption. intros. split... -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{I want to execute the {\texttt proof with} tactic only if it solves the goal, how can I do it?} @@ -1369,8 +1412,10 @@ Local Open Scope Z_scope. Goal forall a b c : Z, a+b=b+a. Proof with try solve [ring]. intros... -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{How can I do the opposite of the {\intro} tactic?} @@ -1382,8 +1427,10 @@ intros. generalize H. intro. auto. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{One of the hypothesis is an equality between a variable and some term, I want to get rid of this variable, how can I do it?} @@ -1521,8 +1568,10 @@ You can use the {\discriminate} tactic. Inductive toto : Set := | C1 : toto | C2 : toto. Goal C1 <> C2. discriminate. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{During an inductive proof, how to get rid of impossible cases of an inductive definition?} @@ -1824,9 +1873,9 @@ induction 1. inversion 1. inversion 1. apply IHeven; trivial. \end{coq_example} -\begin{coq_eval} +\begin{coq_example*} Qed. -\end{coq_eval} +\end{coq_example*} In case the type of the second induction hypothesis is not dependent, {\tt inversion} can just be replaced by {\tt destruct}. @@ -1861,10 +1910,10 @@ Double induction (or induction on pairs) is a restriction of the lexicographic induction. Here is an example of double induction. \begin{coq_example} -Lemma nat_double_ind : -forall P : nat -> nat -> Prop, P 0 0 -> - (forall m n, P m n -> P m (S n)) -> - (forall m n, P m n -> P (S m) n) -> +Lemma nat_double_ind : +forall P : nat -> nat -> Prop, P 0 0 -> + (forall m n, P m n -> P m (S n)) -> + (forall m n, P m n -> P (S m) n) -> forall m n, P m n. intros P H00 HmS HSn; induction m. (* case 0 *) @@ -1872,9 +1921,9 @@ induction n; [assumption | apply HmS; apply IHn]. (* case Sm *) intro n; apply HSn; apply IHm. \end{coq_example} -\begin{coq_eval} +\begin{coq_example*} Qed. -\end{coq_eval} +\end{coq_example*} \Question{How to define a function by nested recursion?} @@ -1909,7 +1958,7 @@ Set Implicit Arguments. CoInductive Stream (A:Set) : Set := Cons : A -> Stream A -> Stream A. CoFixpoint nats (n:nat) : Stream nat := Cons n (nats (S n)). -Lemma Stream_unfold : +Lemma Stream_unfold : forall n:nat, nats n = Cons n (nats (S n)). Proof. intro; @@ -1917,8 +1966,10 @@ Proof. | Cons x s => Cons x s end). case (nats n); reflexivity. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} @@ -2599,8 +2650,10 @@ eapply eq_trans. Show Existentials. eassumption. assumption. -Qed. \end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{What can I do if I get ``Cannot solve a second-order unification problem''?} -- cgit v1.2.3 From 5cf7ce6afae0e8e5310755f05a26450f428da04f Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 30 Jul 2015 10:19:35 +0200 Subject: Avoid suggesting elim and decompose in the FAQ. --- doc/faq/FAQ.tex | 20 ++++++++++++++------ 1 file changed, 14 insertions(+), 6 deletions(-) diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index 3e14e330b0..c8dd220baf 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -1012,13 +1012,21 @@ Just use the {\destruct} c as (a,...,b) tactic. \Question{My goal contains some existential hypotheses, how can I use it?} -You can use the tactic {\elim} with you hypotheses as an argument. +As with conjunctive hypotheses, you can use the {\destruct} tactic or +the {\intros} tactic to decompose them into several hypotheses. -\Question{My goal contains some existential hypotheses, how can I use it and decompose my knowledge about this new thing into different hypotheses?} - -\begin{verbatim} -Ltac DecompEx H P := elim H;intro P;intro TO;decompose [and] TO;clear TO;clear H. -\end{verbatim} +\begin{coq_example*} +Require Import Arith. +\end{coq_example*} +\begin{coq_example} +Goal forall x, (exists y, x * y = 1) -> x = 1. +intros x [y H]. +apply mult_is_one in H. +easy. +\end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} \Question{My goal is an equality, how can I swap the left and right hand terms?} -- cgit v1.2.3 From 5e60af46bdcb5aa487737961859f80181486516b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 28 Jul 2015 19:25:51 +0200 Subject: A printer for printing constants of the env (maybe useful when there are not too many of them). --- dev/top_printers.ml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/dev/top_printers.ml b/dev/top_printers.ml index f969f01329..f9f2e1b09e 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -229,6 +229,11 @@ let ppenv e = pp (str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++ str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]") +let ppenvwithcst e = pp + (str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++ + str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]" ++ spc() ++ + str "{" ++ Cmap_env.fold (fun a _ s -> pr_con a ++ spc () ++ s) (Obj.magic e).Pre_env.env_globals.Pre_env.env_constants (mt ()) ++ str "}") + let pptac = (fun x -> pp(Pptactic.pr_glob_tactic (Global.env()) x)) let ppobj obj = Format.print_string (Libobject.object_tag obj) -- cgit v1.2.3 From 9f81b58551958aea2a85bcdd0cc3f88bf4634c92 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 29 Jul 2015 01:26:00 +0200 Subject: Fixing bug #4289 (hash-consing only user part of constant not compatible with a unique bound module name counter which is not synchronous with the backtracking). We changed hash-consing of kernel name pairs to a purely memory management issue, not trying to exploit logical properties such as "syntactically equal user names have syntactically same canonical names" (which is true in a given logical session, but not in memory, at least because of residual values after backtracking). --- kernel/names.ml | 24 +++++++++++++++++------- 1 file changed, 17 insertions(+), 7 deletions(-) diff --git a/kernel/names.ml b/kernel/names.ml index f217c932cc..19fe62ec85 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -453,6 +453,9 @@ module KNset = KNmap.Set - when user and canonical parts differ, we cannot be in a section anymore, hence the dirpath must be empty - two pairs with the same user part should have the same canonical part + in a given environment (though with backtracking, the hash-table can + contains pairs with same user part but different canonical part from + a previous state of the session) Note: since most of the time the canonical and user parts are equal, we handle this case with a particular constructor to spare some memory *) @@ -504,7 +507,7 @@ module KerPair = struct let debug_print kp = str (debug_to_string kp) (** For ordering kernel pairs, both user or canonical parts may make - sense, according to your needs : user for the environments, canonical + sense, according to your needs: user for the environments, canonical for other uses (ex: non-logical things). *) module UserOrd = struct @@ -521,16 +524,18 @@ module KerPair = struct let hash x = KerName.hash (canonical x) end - (** Default comparison is on the canonical part *) + (** Default (logical) comparison is on the canonical part *) let equal = CanOrd.equal - (** Hash-consing : we discriminate only on the user part, since having - the same user part implies having the same canonical part - (invariant of the system). *) + (** Hash-consing (despite having the same user part implies having + the same canonical part is a logical invariant of the system, it + is not necessarily an invariant in memory, so we treat kernel + names as they are syntactically for hash-consing) *) let hash = function | Same kn -> KerName.hash kn - | Dual (kn, _) -> KerName.hash kn + | Dual (knu, knc) -> + Hashset.Combine.combine (KerName.hash knu) (KerName.hash knc) module Self_Hashcons = struct @@ -539,7 +544,12 @@ module KerPair = struct let hashcons hkn = function | Same kn -> Same (hkn kn) | Dual (knu,knc) -> make (hkn knu) (hkn knc) - let equal x y = (user x) == (user y) + let equal x y = (* physical comparison on subterms *) + x == y || + match x,y with + | Same x, Same y -> x == y + | Dual (ux,cx), Dual (uy,cy) -> ux == uy && cx == cy + | (Same _ | Dual _), _ -> false let hash = hash end -- cgit v1.2.3 From 5a6e0088adb4e817133d4d7f5a547fbc23fe7951 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 30 Jul 2015 14:00:12 +0200 Subject: Test file for bug #4289 (buggy hash-consing of kernel name pairs breaking backtracking in the presence of functors). In "interactive" rather than "bugs" because of the use of Back. --- test-suite/interactive/4289.v | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 test-suite/interactive/4289.v diff --git a/test-suite/interactive/4289.v b/test-suite/interactive/4289.v new file mode 100644 index 0000000000..610a509c9b --- /dev/null +++ b/test-suite/interactive/4289.v @@ -0,0 +1,14 @@ +(* Checking backtracking with modules which used to fail due to an + hash-consing bug *) + +Module Type A. + Axiom B : nat. +End A. +Module C (a : A). + Include a. + Definition c : nat := B. +End C. +Back 4. +Module C (a : A). + Include a. + Definition c : nat := B. -- cgit v1.2.3 From 7a370cbd36a63ba8274d5ac0a3b55e0415f33d2c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 30 Jul 2015 10:16:59 +0200 Subject: STM: remove assertion not being true for nested, immediate, proofs (#4313) --- stm/stm.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/stm/stm.ml b/stm/stm.ml index 9e82dd156d..073a6eeb3a 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1837,7 +1837,6 @@ let known_state ?(redefine_qed=false) ~cache id = Proof_global.discard_all () ), (if redefine_qed then `No else `Yes), true | `Sync (name, _, `Immediate) -> (fun () -> - assert (Stateid.equal view.next eop); reach eop; vernac_interp id x; Proof_global.discard_all () ), `Yes, true | `Sync (name, pua, reason) -> (fun () -> -- cgit v1.2.3 From 15a23fc7c103ba47d3f5e77853ff515d926573ca Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 30 Jul 2015 10:39:50 +0200 Subject: STM: fix backtrack in presence of nested, immediate, proofs --- stm/stm.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/stm/stm.ml b/stm/stm.ml index 073a6eeb3a..b6c6d41879 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2305,9 +2305,7 @@ let edit_at id = let rec master_for_br root tip = if Stateid.equal tip Stateid.initial then tip else match VCS.visit tip with - | { next } when next = root -> root - | { step = `Fork _ } -> tip - | { step = `Sideff (`Ast(_,id)|`Id id) } -> id + | { step = (`Fork _ | `Sideff _ | `Qed _) } -> tip | { next } -> master_for_br root next in let reopen_branch start at_id mode qed_id tip old_branch = let master_id, cancel_switch, keep = -- cgit v1.2.3 From 5d0ff1782ab54914e7b0e5a736922aa297d327c8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 30 Jul 2015 10:41:13 +0200 Subject: STM: emit a warning when a QED/Admitted proof contains a nested lemma --- stm/stm.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/stm/stm.ml b/stm/stm.ml index b6c6d41879..ee12e48d5d 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1688,7 +1688,10 @@ let collect_proof keep cur hd brkind id = assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch); let name = name ids in `MaybeASync (parent last, None, accn, name, delegate name) - | `Sideff _ -> `Sync (no_name,None,`NestedProof) + | `Sideff _ -> + Pp.(msg_warning (strbrk ("Nested proofs are deprecated and will "^ + "stop working in the next Coq version"))); + `Sync (no_name,None,`NestedProof) | _ -> `Sync (no_name,None,`Unknown) in let make_sync why = function | `Sync(name,pua,_) -> `Sync (name,pua,why) -- cgit v1.2.3 From 63ecb7386ae6e705d3f5577e01ec543f706c9427 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 30 Jul 2015 14:35:15 +0200 Subject: STM: make multiple, admitted, nested proofs work (fix #4314) --- stm/stm.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/stm/stm.ml b/stm/stm.ml index ee12e48d5d..bf91c3aa4f 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1858,9 +1858,8 @@ let known_state ?(redefine_qed=false) ~cache id = Some(Proof_global.close_proof ~keep_body_ucst_separate:false (State.exn_on id ~valid:eop)) in - reach view.next; - if keep == VtKeepAsAxiom then - Option.iter (vernac_interp id) pua; + if keep != VtKeepAsAxiom then + reach view.next; let wall_clock2 = Unix.gettimeofday () in vernac_interp id ?proof x; let wall_clock3 = Unix.gettimeofday () in -- cgit v1.2.3 From 1ee23d71dadd6211c36afe8d2891b7170535cd62 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 30 Jul 2015 15:55:24 +0200 Subject: Followup of 9f81b58551. The hash function exported by the interface ought to respect the equality. Therefore, we only use the syntactic hash for the hashconsing module while using the canonical hash in the API. --- kernel/names.ml | 22 ++++++++++------------ 1 file changed, 10 insertions(+), 12 deletions(-) diff --git a/kernel/names.ml b/kernel/names.ml index 19fe62ec85..ae2b3b6389 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -524,18 +524,9 @@ module KerPair = struct let hash x = KerName.hash (canonical x) end - (** Default (logical) comparison is on the canonical part *) + (** Default (logical) comparison and hash is on the canonical part *) let equal = CanOrd.equal - - (** Hash-consing (despite having the same user part implies having - the same canonical part is a logical invariant of the system, it - is not necessarily an invariant in memory, so we treat kernel - names as they are syntactically for hash-consing) *) - - let hash = function - | Same kn -> KerName.hash kn - | Dual (knu, knc) -> - Hashset.Combine.combine (KerName.hash knu) (KerName.hash knc) + let hash = CanOrd.hash module Self_Hashcons = struct @@ -550,7 +541,14 @@ module KerPair = struct | Same x, Same y -> x == y | Dual (ux,cx), Dual (uy,cy) -> ux == uy && cx == cy | (Same _ | Dual _), _ -> false - let hash = hash + (** Hash-consing (despite having the same user part implies having + the same canonical part is a logical invariant of the system, it + is not necessarily an invariant in memory, so we treat kernel + names as they are syntactically for hash-consing) *) + let hash = function + | Same kn -> KerName.hash kn + | Dual (knu, knc) -> + Hashset.Combine.combine (KerName.hash knu) (KerName.hash knc) end module HashKP = Hashcons.Make(Self_Hashcons) -- cgit v1.2.3 From 505eb0f0dae9b8a6ac810070d60916b67942b305 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 31 Jul 2015 09:34:48 +0200 Subject: Remove some outdated files and fix permissions. --- README.doc | 0 doc/common/macros.tex | 0 doc/common/title.tex | 0 doc/stdlib/Library.tex | 0 doc/tutorial/Tutorial.tex | 0 test-suite/interactive/ParalITP_smallproofs.v | 0 test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v | 0 theories/Arith/intro.tex | 55 ------------------------ theories/Bool/intro.tex | 16 ------- theories/Lists/intro.tex | 20 --------- theories/Logic/intro.tex | 8 ---- theories/NArith/intro.tex | 5 --- theories/PArith/intro.tex | 4 -- theories/Reals/intro.tex | 4 -- theories/Relations/intro.tex | 23 ---------- theories/Setoids/intro.tex | 1 - theories/Sets/intro.tex | 24 ----------- theories/Sorting/intro.tex | 1 - theories/Wellfounded/intro.tex | 4 -- theories/ZArith/intro.tex | 6 --- tools/README.coq-tex | 13 ------ tools/README.emacs | 0 tools/coq-sl.sty | 0 23 files changed, 184 deletions(-) mode change 100755 => 100644 README.doc mode change 100755 => 100644 doc/common/macros.tex mode change 100755 => 100644 doc/common/title.tex mode change 100755 => 100644 doc/stdlib/Library.tex mode change 100755 => 100644 doc/tutorial/Tutorial.tex mode change 100755 => 100644 test-suite/interactive/ParalITP_smallproofs.v mode change 100755 => 100644 test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v delete mode 100755 theories/Arith/intro.tex delete mode 100644 theories/Bool/intro.tex delete mode 100755 theories/Lists/intro.tex delete mode 100755 theories/Logic/intro.tex delete mode 100644 theories/NArith/intro.tex delete mode 100644 theories/PArith/intro.tex delete mode 100644 theories/Reals/intro.tex delete mode 100755 theories/Relations/intro.tex delete mode 100644 theories/Setoids/intro.tex delete mode 100755 theories/Sets/intro.tex delete mode 100644 theories/Sorting/intro.tex delete mode 100755 theories/Wellfounded/intro.tex delete mode 100755 theories/ZArith/intro.tex delete mode 100755 tools/README.coq-tex mode change 100755 => 100644 tools/README.emacs mode change 100755 => 100644 tools/coq-sl.sty diff --git a/README.doc b/README.doc old mode 100755 new mode 100644 diff --git a/doc/common/macros.tex b/doc/common/macros.tex old mode 100755 new mode 100644 diff --git a/doc/common/title.tex b/doc/common/title.tex old mode 100755 new mode 100644 diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex old mode 100755 new mode 100644 diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex old mode 100755 new mode 100644 diff --git a/test-suite/interactive/ParalITP_smallproofs.v b/test-suite/interactive/ParalITP_smallproofs.v old mode 100755 new mode 100644 diff --git a/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v b/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v old mode 100755 new mode 100644 diff --git a/theories/Arith/intro.tex b/theories/Arith/intro.tex deleted file mode 100755 index 655de34ca8..0000000000 --- a/theories/Arith/intro.tex +++ /dev/null @@ -1,55 +0,0 @@ -\section{Arith}\label{Arith} - -The {\tt Arith} library deals with various arithmetical notions and -their properties. - -\subsection*{Standard {\tt Arith} library} - -The following files are automatically loaded by {\tt Require Arith}. - -\begin{itemize} - -\item {\tt Le.v} states and proves properties of the large order {\tt le}. - -\item {\tt Lt.v} states and proves properties of the strict order {\tt -lt} (especially, the relationship with {\tt le}). - -\item {\tt Plus.v} states and proves properties on the addition. - -\item {\tt Gt.v} states and proves properties on the strict order {\tt gt}. - -\item {\tt Minus.v} defines the difference on -{\tt nat} and proves properties of it. On {\tt nat}, {\tt (minus n p)} is -{\tt O} if {\tt n} $<$ {\tt p}. - -\item {\tt Mult.v} states and proves properties on the multiplication. - -\item {\tt Between.v} defines modalities on {\tt nat} and proves properties -of them. - -\end{itemize} - -\subsection*{Additional {\tt Arith} library} - -\begin{itemize} - -\item {\tt Compare.v}, {\tt Compare\_dec.v} and {\tt Peano\_dec.v} state -and prove various decidability results on {\tt nat}. - -\item {\tt Wf\_nat.v} states and proves various induction and recursion -principles on {\tt nat}. Especially, recursion for objects measurable by -a natural number and recursion on {\tt nat * nat} are provided. - -\item {\tt Min.v} defines the minimum of two natural numbers and proves -properties of it. - -\item {\tt Eqnat.v} defines a specific equality on {\tt nat} and shows -the equivalence with Leibniz' equality. - -\item {\tt Euclid.v} proves that the euclidean -division specification is realisable. Conversely, {\tt Div.v} exhibits -two different algorithms and semi-automatically reconstruct the proof of -their correctness. These files emphasize the extraction of program vs -reconstruction of proofs paradigm. - -\end{itemize} diff --git a/theories/Bool/intro.tex b/theories/Bool/intro.tex deleted file mode 100644 index 22ee38aab5..0000000000 --- a/theories/Bool/intro.tex +++ /dev/null @@ -1,16 +0,0 @@ -\section{Bool}\label{Bool} - -The BOOL library includes the following files: - -\begin{itemize} - -\item {\tt Bool.v} defines standard operations on booleans and states - and proves simple facts on them. -\item {\tt IfProp.v} defines a disjunction which contains its proof - and states its properties. -\item {\tt Zerob.v} defines the test against 0 on natural numbers and - states and proves properties of it. -\item {\tt Orb.v} states and proves facts on the boolean or. -\item {\tt DecBool.v} defines a conditional from a proof of - decidability and states its properties. -\end{itemize} diff --git a/theories/Lists/intro.tex b/theories/Lists/intro.tex deleted file mode 100755 index d372de8edd..0000000000 --- a/theories/Lists/intro.tex +++ /dev/null @@ -1,20 +0,0 @@ -\section{Lists}\label{Lists} - -This library includes the following files: - -\begin{itemize} - -\item {\tt List.v} contains definitions of (polymorphic) lists, - functions on lists such as head, tail, map, append and prove some - properties of these functions. Implicit arguments are used in this - library, so you should read the Reference Manual about implicit - arguments before using it. - -\item {\tt ListSet.v} contains definitions and properties of finite - sets, implemented as lists. - -\item {\tt Streams.v} defines the type of infinite lists (streams). It is a - co-inductive type. Basic facts are stated and proved. The streams are - also polymorphic. - -\end{itemize} diff --git a/theories/Logic/intro.tex b/theories/Logic/intro.tex deleted file mode 100755 index 1fb294f2f5..0000000000 --- a/theories/Logic/intro.tex +++ /dev/null @@ -1,8 +0,0 @@ -\section{Logic}\label{Logic} - -This library deals with classical logic and its properties. -The main file is {\tt Classical.v}. - -This library also provides some facts on equalities for dependent -types. See the files {\tt Eqdep.v} and {\tt JMeq.v}. - diff --git a/theories/NArith/intro.tex b/theories/NArith/intro.tex deleted file mode 100644 index bf39bc36c6..0000000000 --- a/theories/NArith/intro.tex +++ /dev/null @@ -1,5 +0,0 @@ -\section{Binary natural numbers : NArith}\label{NArith} - -Here are defined various arithmetical notions and their properties, -similar to those of {\tt Arith}. - diff --git a/theories/PArith/intro.tex b/theories/PArith/intro.tex deleted file mode 100644 index ffce881edb..0000000000 --- a/theories/PArith/intro.tex +++ /dev/null @@ -1,4 +0,0 @@ -\section{Binary positive integers : PArith}\label{PArith} - -Here are defined various arithmetical notions and their properties, -similar to those of {\tt Arith}. diff --git a/theories/Reals/intro.tex b/theories/Reals/intro.tex deleted file mode 100644 index 433172585b..0000000000 --- a/theories/Reals/intro.tex +++ /dev/null @@ -1,4 +0,0 @@ -\section{Reals}\label{Reals} - -This library contains an axiomatization of real numbers. -The main file is \texttt{Reals.v}. diff --git a/theories/Relations/intro.tex b/theories/Relations/intro.tex deleted file mode 100755 index 5056f36f97..0000000000 --- a/theories/Relations/intro.tex +++ /dev/null @@ -1,23 +0,0 @@ -\section{Relations}\label{Relations} - -This library develops closure properties of relations. - -\begin{itemize} -\item {\tt Relation\_Definitions.v} deals with the general notions - about binary relations (orders, equivalences, ...) - -\item {\tt Relation\_Operators.v} and {\tt Rstar.v} define various - closures of relations (by symmetry, by transitivity, ...) and - lexicographic orderings. - -\item {\tt Operators\_Properties.v} states and proves facts on the - various closures of a relation. - -\item {\tt Relations.v} puts {\tt Relation\_Definitions.v}, {\tt - Relation\_Operators.v} and \\ - {\tt Operators\_Properties.v} together. - -\item {\tt Newman.v} proves Newman's lemma on noetherian and locally - confluent relations. - -\end{itemize} diff --git a/theories/Setoids/intro.tex b/theories/Setoids/intro.tex deleted file mode 100644 index 50cd025de3..0000000000 --- a/theories/Setoids/intro.tex +++ /dev/null @@ -1 +0,0 @@ -\section{Setoids}\label{Setoids} diff --git a/theories/Sets/intro.tex b/theories/Sets/intro.tex deleted file mode 100755 index 83c2177fd3..0000000000 --- a/theories/Sets/intro.tex +++ /dev/null @@ -1,24 +0,0 @@ -\section{Sets}\label{Sets} - -This is a library on sets defined by their characteristic predicate. -It contains the following modules: - -\begin{itemize} -\item {\tt Ensembles.v} -\item {\tt Constructive\_sets.v}, {\tt Classical\_sets.v} -\item {\tt Relations\_1.v}, {\tt Relations\_2.v}, - {\tt Relations\_3.v}, {\tt Relations\_1\_facts.v}, \\ - {\tt Relations\_2\_facts.v}, {\tt Relations\_3\_facts.v} -\item {\tt Partial\_Order.v}, {\tt Cpo.v} -\item {\tt Powerset.v}, {\tt Powerset\_facts.v}, - {\tt Powerset\_Classical\_facts.v} -\item {\tt Finite\_sets.v}, {\tt Finite\_sets\_facts.v} -\item {\tt Image.v} -\item {\tt Infinite\_sets.v} -\item {\tt Integers.v} -\end{itemize} - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: t -%%% End: diff --git a/theories/Sorting/intro.tex b/theories/Sorting/intro.tex deleted file mode 100644 index 64ae4c8881..0000000000 --- a/theories/Sorting/intro.tex +++ /dev/null @@ -1 +0,0 @@ -\section{Sorting}\label{Sorting} diff --git a/theories/Wellfounded/intro.tex b/theories/Wellfounded/intro.tex deleted file mode 100755 index 126071e286..0000000000 --- a/theories/Wellfounded/intro.tex +++ /dev/null @@ -1,4 +0,0 @@ -\section{Well-founded relations}\label{Wellfounded} - -This library gives definitions and results about well-founded relations. - diff --git a/theories/ZArith/intro.tex b/theories/ZArith/intro.tex deleted file mode 100755 index 21e52c1982..0000000000 --- a/theories/ZArith/intro.tex +++ /dev/null @@ -1,6 +0,0 @@ -\section{Binary integers : ZArith} -The {\tt ZArith} library deals with binary integers (those used -by the {\tt Omega} decision tactic). -Here are defined various arithmetical notions and their properties, -similar to those of {\tt Arith}. - diff --git a/tools/README.coq-tex b/tools/README.coq-tex deleted file mode 100755 index 5c7606a968..0000000000 --- a/tools/README.coq-tex +++ /dev/null @@ -1,13 +0,0 @@ -DESCRIPTION. - -The coq-tex filter extracts Coq phrases embedded in LaTeX files, -evaluates them, and insert the outcome of the evaluation after each -phrase. - -The filter is written in Perl, so you'll need Perl version 4 installed -on your machine. - -USAGE. See the manual page (coq-tex.1). - -AUTHOR. Jean-Christophe Filliatre (jcfillia@lip.ens-lyon.fr) - from caml-tex of Xavier Leroy. diff --git a/tools/README.emacs b/tools/README.emacs old mode 100755 new mode 100644 diff --git a/tools/coq-sl.sty b/tools/coq-sl.sty old mode 100755 new mode 100644 -- cgit v1.2.3 From ce4c3ddec6c91dc277c922aaac58395c92941710 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 31 Jul 2015 17:01:17 +0200 Subject: Improve the table of content of the reference manual. Also remove AsyncProofs.tex from the list of preprocessed files, as it is doubtful it will ever contains Coq scripts. --- Makefile.common | 5 +- doc/refman/AsyncProofs.tex | 10 +- doc/refman/Natural.tex | 425 ---------------------------------------- doc/refman/Reference-Manual.tex | 4 +- 4 files changed, 9 insertions(+), 435 deletions(-) delete mode 100644 doc/refman/Natural.tex diff --git a/Makefile.common b/Makefile.common index 07df8bb157..de26eeb9b8 100644 --- a/Makefile.common +++ b/Makefile.common @@ -127,13 +127,14 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ RefMan-decl.v.tex RefMan-pro.v.tex RefMan-sch.v.tex \ Cases.v.tex Coercion.v.tex CanonicalStructures.v.tex Extraction.v.tex \ Program.v.tex Omega.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \ - Setoid.v.tex Classes.v.tex AsyncProofs.v.tex Universes.v.tex \ + Setoid.v.tex Classes.v.tex Universes.v.tex \ Misc.v.tex) REFMANTEXFILES:=$(addprefix doc/refman/, \ headers.sty Reference-Manual.tex \ RefMan-pre.tex RefMan-int.tex RefMan-com.tex \ - RefMan-uti.tex RefMan-ide.tex RefMan-add.tex RefMan-modr.tex ) \ + RefMan-uti.tex RefMan-ide.tex RefMan-add.tex RefMan-modr.tex \ + AsyncProofs.tex ) \ $(REFMANCOQTEXFILES) \ REFMANEPSFILES:=doc/refman/coqide.eps doc/refman/coqide-queries.eps diff --git a/doc/refman/AsyncProofs.tex b/doc/refman/AsyncProofs.tex index 47dc1ac1a6..7cf5004003 100644 --- a/doc/refman/AsyncProofs.tex +++ b/doc/refman/AsyncProofs.tex @@ -5,7 +5,7 @@ \index{Asynchronous and Parallel Proof Processing!presentation} This chapter explains how proofs can be asynchronously processed by Coq. -This feature improves the reactiveness of the system when used in interactive +This feature improves the reactivity of the system when used in interactive mode via CoqIDE. In addition to that, it allows Coq to take advantage of parallel hardware when used as a batch compiler by decoupling the checking of statements and definitions from the construction and checking of proofs @@ -24,7 +24,7 @@ are universe inconsistencies. Last, at the time of writing, only opaque proofs (ending with \texttt{Qed} or \texttt{Admitted}) can be processed asynchronously. -\subsection{Proof annotations} +\section{Proof annotations} To process a proof asynchronously Coq needs to know the precise statement of the theorem without looking at the proof. This requires some annotations @@ -52,7 +52,7 @@ The command \texttt{Set Suggest Proof Using} makes Coq suggest, when a \texttt{Qed} command is processed, a correct proof annotation. It is up to the user to modify the proof script accordingly. -\subsection{Interactive mode} +\section{Interactive mode} At the time of writing the only user interface supporting asynchronous proof processing is CoqIDE. @@ -85,7 +85,7 @@ reduce the reactivity of the master process to user commands. To disable this feature, one can pass the \texttt{-async-proofs off} flag to CoqIDE. -\subsection{Batch mode} +\section{Batch mode} When Coq is used as a batch compiler by running \texttt{coqc} or \texttt{coqtop -compile}, it produces a \texttt{.vo} file for each @@ -148,7 +148,7 @@ globally consistent. Hence this compilation mode is only useful for quick regression testing and on developments not making heavy use of the $Type$ hierarchy. -\subsection{Limiting the number of parallel workers} +\section{Limiting the number of parallel workers} \label{coqworkmgr} Many Coq processes may run on the same computer, and each of them may start diff --git a/doc/refman/Natural.tex b/doc/refman/Natural.tex deleted file mode 100644 index f33c0d3563..0000000000 --- a/doc/refman/Natural.tex +++ /dev/null @@ -1,425 +0,0 @@ -\achapter{\texttt{Natural} : proofs in natural language} -\aauthor{Yann Coscoy} - -\asection{Introduction} - -\Natural~ is a package allowing the writing of proofs in natural -language. For instance, the proof in \Coq~of the induction principle on pairs -of natural numbers looks like this: - -\begin{coq_example*} -Require Natural. -\end{coq_example*} -\begin{coq_example} -Print nat_double_ind. -\end{coq_example} - -Piping it through the \Natural~pretty-printer gives: - -\comindex{Print Natural} -\begin{coq_example} -Print Natural nat_double_ind. -\end{coq_example} - -\asection{Activating \Natural} - -To enable the printing of proofs in natural language, you should -type under \texttt{coqtop} or \texttt{coqtop -full} the command - -\begin{coq_example*} -Require Natural. -\end{coq_example*} - -By default, proofs are transcripted in english. If you wish to print them -in French, set the French option by - -\comindex{Set Natural} -\begin{coq_example*} -Set Natural French. -\end{coq_example*} - -If you want to go back to English, type in - -\begin{coq_example*} -Set Natural English. -\end{coq_example*} - -Currently, only \verb=French= and \verb=English= are available. - -You may see for example the natural transcription of the proof of -the induction principle on pairs of natural numbers: - -\begin{coq_example*} -Print Natural nat_double_ind. -\end{coq_example*} - -You may also show in natural language the current proof in progress: - -\comindex{Show Natural} -\begin{coq_example} -Goal (n:nat)(le O n). -Induction n. -Show Natural Proof. -\end{coq_example} - -\subsection*{Restrictions} - -For \Natural, a proof is an object of type a proposition (i.e. an -object of type something of type {\tt Prop}). Only proofs are written -in natural language when typing {\tt Print Natural \ident}. All other -objects (the objects of type something which is of type {\tt Set} or -{\tt Type}) are written as usual $\lambda$-terms. - -\asection{Customizing \Natural} - -The transcription of proofs in natural language is mainly a paraphrase of -the formal proofs, but some specific hints in the transcription -can be given. -Three kinds of customization are available. - -\asubsection{Implicit proof steps} - -\subsubsection*{Implicit lemmas} - -Applying a given lemma or theorem \verb=lem1= of statement, say $A -\Rightarrow B$, to an hypothesis, say $H$ (assuming $A$) produces the -following kind of output translation: - -\begin{verbatim} -... -Using lem1 with H we get B. -... -\end{verbatim} - -But sometimes, you may prefer not to see the explicit invocation to -the lemma. You may prefer to see: - -\begin{verbatim} -... -With H we have A. -... -\end{verbatim} - -This is possible by declaring the lemma as implicit. You should type: - -\comindex{Add Natural} -\begin{coq_example*} -Add Natural Implicit lem1. -\end{coq_example*} - -By default, the lemmas \verb=proj1=, \verb=proj2=, \verb=sym_equal= -and \verb=sym_eqT= are declared implicit. To remove a lemma or a theorem -previously declared as implicit, say \verb=lem1=, use the command - -\comindex{Remove Natural} -\begin{coq_example*} -Remove Natural Implicit lem1. -\end{coq_example*} - -To test if the lemma or theorem \verb=lem1= is, or is not, -declared as implicit, type - -\comindex{Test Natural} -\begin{coq_example*} -Test Natural Implicit for lem1. -\end{coq_example*} - -\subsubsection*{Implicit proof constructors} - -Let \verb=constr1= be a proof constructor of a given inductive -proposition (or predicate) -\verb=Q= (of type \verb=Prop=). Assume \verb=constr1= proves -\verb=(x:A)(P x)->(Q x)=. Then, applying \verb=constr1= to an hypothesis, -say \verb=H= (assuming \verb=(P a)=) produces the following kind of output: - -\begin{verbatim} -... -By the definition of Q, with H we have (Q a). -... -\end{verbatim} - -But sometimes, you may prefer not to see the explicit invocation to -this constructor. You may prefer to see: - -\begin{verbatim} -... -With H we have (Q a). -... -\end{verbatim} - -This is possible by declaring the constructor as implicit. You should -type, as before: - -\comindex{Add Natural Implicit} -\begin{coq_example*} -Add Natural Implicit constr1. -\end{coq_example*} - -By default, the proposition (or predicate) constructors - -\verb=conj=, \verb=or_introl=, \verb=or_intror=, \verb=ex_intro=, -\verb=eq_refl= and \verb=exist= - -\noindent are declared implicit. Note that declaring implicit the -constructor of a datatype (i.e. an inductive type of type \verb=Set=) -has no effect. - -As above, you can remove or test a constant declared implicit. - -\subsubsection*{Implicit inductive constants} - -Let \verb=Ind= be an inductive type (either a proposition (or a -predicate) -- on \verb=Prop= --, or a datatype -- on \verb=Set=). -Suppose the proof proceeds by induction on an hypothesis \verb=h= -proving \verb=Ind= (or more generally \verb=(Ind A1 ... An)=). The -following kind of output is produced: - -\begin{verbatim} -... -With H, we will prove A by induction on the definition of Ind. -Case 1. ... -Case 2. ... -... -\end{verbatim} - -But sometimes, you may prefer not to see the explicit invocation to -\verb=Ind=. You may prefer to see: - -\begin{verbatim} -... -We will prove A by induction on H. -Case 1. ... -Case 2. ... -... -\end{verbatim} - -This is possible by declaring the inductive type as implicit. You should -type, as before: - -\comindex{Add Natural Implicit} -\begin{coq_example*} -Add Natural Implicit Ind. -\end{coq_example*} - -This kind of parameterization works for any inductively defined -proposition (or predicate) or datatype. Especially, it works whatever -the definition is recursive or purely by cases. - -By default, the data type \verb=nat= and the inductive connectives -\verb=and=, \verb=or=, \verb=sig=, \verb=False=, \verb=eq=, -\verb=eqT=, \verb=ex= and \verb=exT= are declared implicit. - -As above, you can remove or test a constant declared implicit. Use -{\tt Remove Natural Contractible $id$} or {\tt Test Natural -Contractible for $id$}. - -\asubsection{Contractible proof steps} - -\subsubsection*{Contractible lemmas or constructors} - -Some lemmas, theorems or proof constructors of inductive predicates are -often applied in a row and you obtain an output of this kind: - -\begin{verbatim} -... -Using T with H1 and H2 we get P. - * By H3 we have Q. - Using T with theses results we get R. -... -\end{verbatim} - -where \verb=T=, \verb=H1=, \verb=H2= and \verb=H3= prove statements -of the form \verb=(X,Y:Prop)X->Y->(L X Y)=, \verb=A=, \verb=B= and \verb=C= -respectively (and thus \verb=R= is \verb=(L (L A B) C)=). - -You may obtain a condensed output of the form - -\begin{verbatim} -... -Using T with H1, H2, and H3 we get R. -... -\end{verbatim} - -by declaring \verb=T= as contractible: - -\comindex{Add Natural Contractible} -\begin{coq_example*} -Add Natural Contractible T. -\end{coq_example*} - -By default, the lemmas \verb=proj1=, \verb=proj2= and the proof -constructors \verb=conj=, \verb=or_introl=, \verb=or_intror= are -declared contractible. As for implicit notions, you can remove or -test a lemma or constructor declared contractible. - -\subsubsection*{Contractible induction steps} - -Let \verb=Ind= be an inductive type. When the proof proceeds by -induction in a row, you may obtain an output of this kind: - -\begin{verbatim} -... -We have (Ind A (Ind B C)). -We use definition of Ind in a study in two cases. -Case 1: We have A. -Case 2: We have (Ind B C). - We use definition of Ind in a study of two cases. - Case 2.1: We have B. - Case 2.2: We have C. -... -\end{verbatim} - -You may prefer to see - -\begin{verbatim} -... -We have (Ind A (Ind B C)). -We use definition of Ind in a study in three cases. -Case 1: We have A. -Case 2: We have B. -Case 3: We have C. -... -\end{verbatim} - -This is possible by declaring \verb=Ind= as contractible: - -\begin{coq_example*} -Add Natural Contractible T. -\end{coq_example*} - -By default, only \verb=or= is declared as a contractible inductive -constant. -As for implicit notions, you can remove or test an inductive notion declared -contractible. - -\asubsection{Transparent definitions} - -``Normal'' definitions are all constructions except proofs and proof constructors. - -\subsubsection*{Transparent non inductive normal definitions} - -When using the definition of a non inductive constant, say \verb=D=, the -following kind of output is produced: - -\begin{verbatim} -... -We have proved C which is equivalent to D. -... -\end{verbatim} - -But you may prefer to hide that D comes from the definition of C as -follows: - -\begin{verbatim} -... -We have prove D. -... -\end{verbatim} - -This is possible by declaring \verb=C= as transparent: - -\comindex{Add Natural Transparent} -\begin{coq_example*} -Add Natural Transparent D. -\end{coq_example*} - -By default, only \verb=not= (normally written \verb=~=) is declared as -a non inductive transparent definition. -As for implicit and contractible definitions, you can remove or test a -non inductive definition declared transparent. -Use \texttt{Remove Natural Transparent} \ident or -\texttt{Test Natural Transparent for} \ident. - -\subsubsection*{Transparent inductive definitions} - -Let \verb=Ind= be an inductive proposition (more generally: a -predicate \verb=(Ind x1 ... xn)=). Suppose the definition of -\verb=Ind= is non recursive and built with just -one constructor proving something like \verb=A -> B -> Ind=. -When coming back to the definition of \verb=Ind= the -following kind of output is produced: - -\begin{verbatim} -... -Assume Ind (H). - We use H with definition of Ind. - We have A and B. - ... -\end{verbatim} - -When \verb=H= is not used a second time in the proof, you may prefer -to hide that \verb=A= and \verb=B= comes from the definition of -\verb=Ind=. You may prefer to get directly: - -\begin{verbatim} -... -Assume A and B. -... -\end{verbatim} - -This is possible by declaring \verb=Ind= as transparent: - -\begin{coq_example*} -Add Natural Transparent Ind. -\end{coq_example*} - -By default, \verb=and=, \verb=or=, \verb=ex=, \verb=exT=, \verb=sig= -are declared as inductive transparent constants. As for implicit and -contractible constants, you can remove or test an inductive -constant declared transparent. - -As for implicit and contractible constants, you can remove or test an -inductive constant declared transparent. - -\asubsection{Extending the maximal depth of nested text} - -The depth of nested text is limited. To know the current depth, do: - -\comindex{Set Natural Depth} -\begin{coq_example} -Set Natural Depth. -\end{coq_example} - -To change the maximal depth of nested text (for instance to 125) do: - -\begin{coq_example} -Set Natural Depth 125. -\end{coq_example} - -\asubsection{Restoring the default parameterization} - -The command \verb=Set Natural Default= sets back the parameterization tables of -\Natural~ to their default values, as listed in the above sections. -Moreover, the language is set back to English and the max depth of -nested text is set back to its initial value. - -\asubsection{Printing the current parameterization} - -The commands {\tt Print Natural Implicit}, {\tt Print Natural -Contractible} and {\tt Print \\ Natural Transparent} print the list of -constructions declared {\tt Implicit}, {\tt Contractible}, -{\tt Transparent} respectively. - -\asubsection{Interferences with \texttt{Reset}} - -The customization of \texttt{Natural} is dependent of the \texttt{Reset} -command. If you reset the environment back to a point preceding an -\verb=Add Natural ...= command, the effect of the command will be -erased. Similarly, a reset back to a point before a -\verb=Remove Natural ... = command invalidates the removal. - -\asection{Error messages} - -An error occurs when trying to \verb=Print=, to \verb=Add=, to -\verb=Test=, or to \verb=remove= an undefined ident. Similarly, an -error occurs when trying to set a language unknown from \Natural. -Errors may also occur when trying to parameterize the printing of -proofs: some parameterization are effectively forbidden. -Note that to \verb=Remove= an ident absent from a table or to -\verb=Add= to a table an already present ident does not lead to an -error. - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index 907b30b3e0..ac28e0ba03 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -114,16 +114,14 @@ Options A and B of the licence are {\em not} elected.} \include{Coercion.v}% \include{CanonicalStructures.v}% \include{Classes.v}% -%%SUPPRIME \include{Natural.v}% \include{Omega.v}% \include{Micromega.v} -%%SUPPRIME \include{Correctness.v}% = preuve de pgms imperatifs \include{Extraction.v}% \include{Program.v}% \include{Polynom.v}% = Ring \include{Nsatz.v}% \include{Setoid.v}% Tactique pour les setoides -\include{AsyncProofs.v}% Paral-ITP +\include{AsyncProofs}% Paral-ITP \include{Universes.v}% Universe polymorphes \include{Misc.v} %BEGIN LATEX -- cgit v1.2.3 From 947206269dc31bb6b919fce935e1748bc440d960 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 31 Jul 2015 17:01:39 +0200 Subject: Fix typos in the Micromega part of the reference manual. --- doc/refman/Micromega.tex | 135 +++++++++++++++++++++++++++-------------------- 1 file changed, 78 insertions(+), 57 deletions(-) diff --git a/doc/refman/Micromega.tex b/doc/refman/Micromega.tex index 551f6c205b..1efed6ef76 100644 --- a/doc/refman/Micromega.tex +++ b/doc/refman/Micromega.tex @@ -1,4 +1,4 @@ -\achapter{Micromega : tactics for solving arithmetic goals over ordered rings} +\achapter{Micromega: tactics for solving arithmetic goals over ordered rings} \aauthor{Frédéric Besson and Evgeny Makarov} \newtheorem{theorem}{Theorem} @@ -6,33 +6,40 @@ \asection{Short description of the tactics} \tacindex{psatz} \tacindex{lra} \label{sec:psatz-hurry} -The {\tt Psatz} module ({\tt Require Import Psatz.}) gives access to several tactics for solving arithmetic goals over - {\tt Z}\footnote{Support for {\tt nat} and {\tt N} is obtained by pre-processing the goal with the {\tt zify} tactic.}, {\tt Q} and {\tt R}: +The {\tt Psatz} module ({\tt Require Import Psatz.}) gives access to +several tactics for solving arithmetic goals over {\tt Z}, {\tt Q}, and +{\tt R}:\footnote{Support for {\tt nat} and {\tt N} is obtained by + pre-processing the goal with the {\tt zify} tactic.} \begin{itemize} \item {\tt lia} is a decision procedure for linear integer arithmetic (see Section~\ref{sec:lia}); \item {\tt nia} is an incomplete proof procedure for integer non-linear arithmetic (see Section~\ref{sec:nia}); \item {\tt lra} is a decision procedure for linear (real or rational) arithmetic goals (see Section~\ref{sec:lra}); -\item {\tt psatz D n} where {\tt D} is {\tt Z}, {\tt Q} or {\tt R} and {\tt n} is an optional integer limiting the proof search depth is -is an incomplete proof procedure for non-linear arithmetic. It is based on John Harrison's Hol light driver to the external prover {\tt cspd}\footnote{Sources and binaries can be found at \url{https://projects.coin-or.org/Csdp}}. - Note that the {\tt csdp} driver is generating - a \emph{proof cache} which allows rerunning scripts even without {\tt csdp} (see Section~\ref{sec:psatz}). +\item {\tt psatz D n} where {\tt D} is {\tt Z} or {\tt Q} or {\tt R}, and + {\tt n} is an optional integer limiting the proof search depth is is an + incomplete proof procedure for non-linear arithmetic. It is based on + John Harrison's HOL Light driver to the external prover {\tt + csdp}\footnote{Sources and binaries can be found at + \url{https://projects.coin-or.org/Csdp}}. Note that the {\tt csdp} + driver is generating a \emph{proof cache} which makes it possible to + rerun scripts even without {\tt csdp} (see Section~\ref{sec:psatz}). \end{itemize} -The tactics solve propositional formulas parameterised by atomic arithmetics expressions +The tactics solve propositional formulas parameterized by atomic arithmetic expressions interpreted over a domain $D \in \{\mathbb{Z}, \mathbb{Q}, \mathbb{R} \}$. The syntax of the formulas is the following: \[ \begin{array}{lcl} - F &::=& A \mid P \mid \mathit{True} \mid \mathit{False} \mid F_1 \land F_2 \mid F_1 \lor F_2 \mid F_1 \leftrightarrow F_2 \mid F_1 \to F_2 \mid \sim F\\ + F &::=& A \mid P \mid \mathit{True} \mid \mathit{False} \mid F_1 \land F_2 \mid F_1 \lor F_2 \mid F_1 \leftrightarrow F_2 \mid F_1 \to F_2 \mid \neg F\\ A &::=& p_1 = p_2 \mid p_1 > p_2 \mid p_1 < p_2 \mid p_1 \ge p_2 \mid p_1 \le p_2 \\ p &::=& c \mid x \mid {-}p \mid p_1 - p_2 \mid p_1 + p_2 \mid p_1 \times p_2 \mid p \verb!^! n - \end{array} - \] - where $c$ is a numeric constant, $x\in D$ is a numeric variable and the operators $-$, $+$, $\times$, are - respectively subtraction, addition, product, $p \verb!^!n $ is exponentiation by a constant $n$, $P$ is an - arbitrary proposition. +\end{array} +\] +where $c$ is a numeric constant, $x\in D$ is a numeric variable, the +operators $-$, $+$, $\times$ are respectively subtraction, addition, +product, $p \verb!^!n $ is exponentiation by a constant $n$, $P$ is an +arbitrary proposition. % - For {\tt Q}, equality is not leibnitz equality {\tt =} but the equality of rationals {\tt ==}. + For {\tt Q}, equality is not Leibniz equality {\tt =} but the equality of rationals {\tt ==}. For {\tt Z} (resp. {\tt Q} ), $c$ ranges over integer constants (resp. rational constants). %% The following table details for each domain $D \in \{\mathbb{Z},\mathbb{Q},\mathbb{R}\}$ the range of constants $c$ and exponent $n$. @@ -47,79 +54,89 @@ For {\tt Z} (resp. {\tt Q} ), $c$ ranges over integer constants (resp. rational %% \hline %% \end{array} %% \] -For {\tt R}, the tactic recognises as real constants the following expressions: +For {\tt R}, the tactic recognizes as real constants the following expressions: \begin{verbatim} -c ::= R0 | R1 | Rmul(c,c) | Rplus(c,c) | Rminus(c,c) | IZR z | IQR q | Rdiv(c,c) | Rinv c +c ::= R0 | R1 | Rmul(c,c) | Rplus(c,c) | Rminus(c,c) | IZR z | IQR q + | Rdiv(c,c) | Rinv c \end{verbatim} -where ${\tt z}$ is a constant in {\tt Z} and {\tt q} is a constant in {\tt Q}. +where {\tt z} is a constant in {\tt Z} and {\tt q} is a constant in {\tt Q}. This includes integer constants written using the decimal notation \emph{i.e.,} {\tt c\%R}. \asection{\emph{Positivstellensatz} refutations} \label{sec:psatz-back} The name {\tt psatz} is an abbreviation for \emph{positivstellensatz} -- literally positivity theorem -- which -generalises Hilbert's \emph{nullstellensatz}. +generalizes Hilbert's \emph{nullstellensatz}. % -It relies on the notion of $\mathit{Cone}$. Given a (finite) set of polynomials $S$, $Cone(S)$ is -inductively defined as the smallest set of polynomials closed under the following rules: +It relies on the notion of $\mathit{Cone}$. Given a (finite) set of +polynomials $S$, $\mathit{Cone}(S)$ is inductively defined as the +smallest set of polynomials closed under the following rules: \[ \begin{array}{l} -\dfrac{p \in S}{p \in Cone(S)} \quad -\dfrac{}{p^2 \in Cone(S)} \quad -\dfrac{p_1 \in Cone(S) \quad p_2 \in Cone(S) \quad \Join \in \{+,*\}} {p_1 \Join p_2 \in Cone(S)}\\ +\dfrac{p \in S}{p \in \mathit{Cone}(S)} \quad +\dfrac{}{p^2 \in \mathit{Cone}(S)} \quad +\dfrac{p_1 \in \mathit{Cone}(S) \quad p_2 \in \mathit{Cone}(S) \quad +\Join \in \{+,*\}} {p_1 \Join p_2 \in \mathit{Cone}(S)}\\ \end{array} \] -The following theorem provides a proof principle for checking that a set of polynomial inequalities do not have solutions\footnote{Variants deal with equalities and strict inequalities.}: +The following theorem provides a proof principle for checking that a set +of polynomial inequalities does not have solutions.\footnote{Variants + deal with equalities and strict inequalities.} \begin{theorem} \label{thm:psatz} Let $S$ be a set of polynomials.\\ - If ${-}1$ belongs to $Cone(S)$ then the conjunction $\bigwedge_{p \in S} p\ge 0$ is unsatisfiable. + If ${-}1$ belongs to $\mathit{Cone}(S)$ then the conjunction + $\bigwedge_{p \in S} p\ge 0$ is unsatisfiable. \end{theorem} A proof based on this theorem is called a \emph{positivstellensatz} refutation. % -The tactics work as follows. Formulas are normalised into conjonctive normal form $\bigwedge_i C_i$ where +The tactics work as follows. Formulas are normalized into conjunctive normal form $\bigwedge_i C_i$ where $C_i$ has the general form $(\bigwedge_{j\in S_i} p_j \Join 0) \to \mathit{False})$ and $\Join \in \{>,\ge,=\}$ for $D\in \{\mathbb{Q},\mathbb{R}\}$ and $\Join \in \{\ge, =\}$ for $\mathbb{Z}$. % For each conjunct $C_i$, the tactic calls a oracle which searches for $-1$ within the cone. % -Upon success, the oracle returns a \emph{cone expression} that is normalised by the {\tt ring} tactic (see chapter~\ref{ring}) and checked to be +Upon success, the oracle returns a \emph{cone expression} that is normalized by the {\tt ring} tactic (see chapter~\ref{ring}) and checked to be $-1$. -\asection{{\tt lra} : a decision procedure for linear real and rational arithmetic} +\asection{{\tt lra}: a decision procedure for linear real and rational arithmetic} \label{sec:lra} The {\tt lra} tactic is searching for \emph{linear} refutations using -Fourier elimination\footnote{More efficient linear programming techniques could equally be employed}. As a -result, this tactic explores a subset of the $Cone$ defined as: +Fourier elimination.\footnote{More efficient linear programming + techniques could equally be employed.} As a result, this tactic +explores a subset of the $\mathit{Cone}$ defined as \[ -LinCone(S) =\left\{ \left. \sum_{p \in S} \alpha_p \times p\ \right|\ \alpha_p \mbox{ are positive constants} \right\} +\mathit{LinCone}(S) =\left\{ \left. \sum_{p \in S} \alpha_p \times p~\right| +~\alpha_p \mbox{ are positive constants} \right\}. \] The deductive power of {\tt lra} is the combined deductive power of {\tt ring\_simplify} and {\tt fourier}. % There is also an overlap with the {\tt field} tactic {\emph e.g.}, {\tt x = 10 * x / 10} is solved by {\tt lra}. -\asection{ {\tt psatz} : a proof procedure for non-linear arithmetic} +\asection{{\tt psatz}: a proof procedure for non-linear arithmetic} \label{sec:psatz} -The {\tt psatz} tactic explores the $Cone$ by increasing degrees -- hence the depth parameter $n$. +The {\tt psatz} tactic explores the $\mathit{Cone}$ by increasing degrees -- hence the depth parameter $n$. In theory, such a proof search is complete -- if the goal is provable the search eventually stops. -Unfortunately, the external oracle is using numeric (approximate) optimisation techniques that might miss a +Unfortunately, the external oracle is using numeric (approximate) optimization techniques that might miss a refutation. -To illustrate the working of the tactic, consider we wish to prove the following Coq goal.\\ +To illustrate the working of the tactic, consider we wish to prove the following Coq goal. \begin{coq_eval} - Require Import ZArith Psatz. - Open Scope Z_scope. +Require Import ZArith Psatz. +Open Scope Z_scope. \end{coq_eval} \begin{coq_example*} - Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False. +Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False. \end{coq_example*} \begin{coq_eval} intro x; psatz Z 2. \end{coq_eval} -Such a goal is solved by {\tt intro x; psatz Z 2}. The oracle returns the cone expression $2 \times -(\mathbf{x-1}) + \mathbf{x-1}\times\mathbf{x-1} + \mathbf{-x^2}$ (polynomial hypotheses are printed in bold). By construction, this -expression belongs to $Cone(\{-x^2, x -1\})$. Moreover, by running {\tt ring} we obtain $-1$. By +Such a goal is solved by {\tt intro x; psatz Z 2}. The oracle returns the +cone expression $2 \times (\mathbf{x-1}) + (\mathbf{x-1}) \times +(\mathbf{x-1}) + \mathbf{-x^2}$ (polynomial hypotheses are printed in +bold). By construction, this expression belongs to $\mathit{Cone}(\{-x^2, +x -1\})$. Moreover, by running {\tt ring} we obtain $-1$. By Theorem~\ref{thm:psatz}, the goal is valid. % @@ -128,14 +145,14 @@ Theorem~\ref{thm:psatz}, the goal is valid. %% This amounts to searching for $p$ in the cone without generators \emph{i.e.}, $Cone(\{\})$. % -\asection{ {\tt lia} : a tactic for linear integer arithmetic } +\asection{{\tt lia}: a tactic for linear integer arithmetic} \tacindex{lia} \label{sec:lia} -The tactic {\tt lia} ({\tt Require Lia.}) offers an alternative to the {\tt omega} and {\tt romega} tactic (see -Chapter~\ref{OmegaChapter}). +The tactic {\tt lia} offers an alternative to the {\tt omega} and {\tt + romega} tactic (see Chapter~\ref{OmegaChapter}). % -Rougthly speaking, the deductive power of {\tt lia} is the combined deductive power of {\tt ring\_simplify} and {\tt omega}. +Roughly speaking, the deductive power of {\tt lia} is the combined deductive power of {\tt ring\_simplify} and {\tt omega}. % However, it solves linear goals that {\tt omega} and {\tt romega} do not solve, such as the following so-called \emph{omega nightmare}~\cite{TheOmegaPaper}. @@ -147,18 +164,20 @@ Goal forall x y, \begin{coq_eval} intros x y; lia. \end{coq_eval} -The estimation of the relative efficiency of lia \emph{vs} {\tt omega} +The estimation of the relative efficiency of {\tt lia} \emph{vs} {\tt omega} and {\tt romega} is under evaluation. \paragraph{High level view of {\tt lia}.} -Over $\mathbb{R}$, \emph{positivstellensatz} refutations are a complete proof principle\footnote{In practice, the oracle might fail to produce such a refutation.}. +Over $\mathbb{R}$, \emph{positivstellensatz} refutations are a complete +proof principle.\footnote{In practice, the oracle might fail to produce + such a refutation.} % However, this is not the case over $\mathbb{Z}$. % -Actually, \emph{positivstellensatz} refutations are not even sufficient to decide linear \emph{integer} -arithmetics. +Actually, \emph{positivstellensatz} refutations are not even sufficient +to decide linear \emph{integer} arithmetic. % -The canonical exemple is {\tt 2 * x = 1 -> False} which is a theorem of $\mathbb{Z}$ but not a theorem of $\mathbb{R}$. +The canonical example is {\tt 2 * x = 1 -> False} which is a theorem of $\mathbb{Z}$ but not a theorem of $\mathbb{R}$. % To remedy this weakness, the {\tt lia} tactic is using recursively a combination of: % @@ -177,17 +196,18 @@ To remedy this weakness, the {\tt lia} tactic is using recursively a combination p \ge c \Rightarrow p \ge \lceil c \rceil \] \end{theorem} -For instance, from $2 * x = 1$ we can deduce +For instance, from $2 x = 1$ we can deduce \begin{itemize} \item $x \ge 1/2$ which cut plane is $ x \ge \lceil 1/2 \rceil = 1$; \item $ x \le 1/2$ which cut plane is $ x \le \lfloor 1/2 \rfloor = 0$. \end{itemize} -By combining these two facts (in normal form) $x - 1 \ge 0$ and $-x \ge 0$, we conclude by exhibiting a -\emph{positivstellensatz} refutation ($-1 \equiv \mathbf{x-1} + \mathbf{-x} \in Cone(\{x-1,x\})$). +By combining these two facts (in normal form) $x - 1 \ge 0$ and $-x \ge +0$, we conclude by exhibiting a \emph{positivstellensatz} refutation: $-1 +\equiv \mathbf{x-1} + \mathbf{-x} \in \mathit{Cone}(\{x-1,x\})$. Cutting plane proofs and linear \emph{positivstellensatz} refutations are a complete proof principle for integer linear arithmetic. -\paragraph{Case split} allow to enumerate over the possible values of an expression. +\paragraph{Case split} enumerates over the possible values of an expression. \begin{theorem} Let $p$ be an integer and $c_1$ and $c_2$ integer constants. \[ @@ -199,7 +219,7 @@ Our current oracle tries to find an expression $e$ with a small range $[c_1,c_2] We generate $c_2 - c_1$ subgoals which contexts are enriched with an equation $e = i$ for $i \in [c_1,c_2]$ and recursively search for a proof. -\asection{ {\tt nia} : a proof procedure for non-linear integer arithmetic} +\asection{{\tt nia}: a proof procedure for non-linear integer arithmetic} \tacindex{nia} \label{sec:nia} The {\tt nia} tactic is an {\emph experimental} proof procedure for non-linear integer arithmetic. @@ -212,7 +232,8 @@ This pre-processing does the following: monomial, the context is enriched with $x^2\ge 0$; \item For all pairs of hypotheses $e_1\ge 0$, $e_2 \ge 0$, the context is enriched with $e_1 \times e_2 \ge 0$. \end{itemize} -After pre-processing, the linear prover of {\tt lia} is searching for a proof by abstracting monomials by variables. +After pre-processing, the linear prover of {\tt lia} searches for a proof +by abstracting monomials by variables. -- cgit v1.2.3 From 71e0a34f89d03787003df1a30bb793bd71ebb775 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 31 Jul 2015 17:28:40 +0200 Subject: Fix typos in the Extraction part of the reference manual. In particular, fix the name of all the user contributions. --- doc/refman/Extraction.tex | 99 ++++++++++++++++++++--------------------------- 1 file changed, 43 insertions(+), 56 deletions(-) diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex index 187fe53428..74c8374de4 100644 --- a/doc/refman/Extraction.tex +++ b/doc/refman/Extraction.tex @@ -110,17 +110,14 @@ even if some inlining is done, the inlined constant are nevertheless printed, to ensure session-independent programs. Concerning Haskell, type-preserving optimizations are less useful -because of lazyness. We still make some optimizations, for example in +because of laziness. We still make some optimizations, for example in order to produce more readable code. The type-preserving optimizations are controlled by the following \Coq\ options: \begin{description} -\item \optindex{Extraction Optimize} -{\tt Set Extraction Optimize.} - -\item {\tt Unset Extraction Optimize.} +\item \optindex{Extraction Optimize} {\tt Unset Extraction Optimize.} Default is Set. This controls all type-preserving optimizations made on the ML terms (mostly reduction of dummy beta/iota redexes, but also @@ -130,8 +127,6 @@ ML term as close as possible to the Coq term. \item \optindex{Extraction Conservative Types} {\tt Set Extraction Conservative Types.} -\item {\tt Unset Extraction Conservative Types.} - Default is Unset. This controls the non type-preserving optimizations made on ML terms (which try to avoid function abstraction of dummy types). Turn this option to Set to make sure that {\tt e:t} @@ -141,8 +136,6 @@ code of {\tt e} and {\tt t} respectively. \item \optindex{Extraction KeepSingleton} {\tt Set Extraction KeepSingleton.} -\item {\tt Unset Extraction KeepSingleton.} - Default is Unset. Normally, when the extraction of an inductive type produces a singleton type (i.e. a type with only one constructor, and only one argument to this constructor), the inductive structure is @@ -150,21 +143,15 @@ removed and this type is seen as an alias to the inner type. The typical example is {\tt sig}. This option allows disabling this optimization when one wishes to preserve the inductive structure of types. -\item \optindex{Extraction AutoInline} -{\tt Set Extraction AutoInline.} - -\item {\tt Unset Extraction AutoInline.} +\item \optindex{Extraction AutoInline} {\tt Unset Extraction AutoInline.} -Default is Set, so by default, the extraction mechanism is free to -inline the bodies of some defined constants, according to some heuristics +Default is Set. The extraction mechanism +inlines the bodies of some defined constants, according to some heuristics like size of bodies, uselessness of some arguments, etc. Those heuristics are not always perfect; if you want to disable this feature, do it by Unset. -\item \comindex{Extraction Inline} -{\tt Extraction Inline} \qualid$_1$ \dots\ \qualid$_n$. - -\item \comindex{Extraction NoInline} -{\tt Extraction NoInline} \qualid$_1$ \dots\ \qualid$_n$. +\item \comindex{Extraction Inline} \comindex{Extraction NoInline} +{\tt Extraction [Inline|NoInline] \qualid$_1$ \dots\ \qualid$_n$}. In addition to the automatic inline feature, you can tell to inline some more constants by the {\tt Extraction Inline} command. Conversely, @@ -265,28 +252,28 @@ extracted files. The extraction recognizes whether the realized axiom should become a ML type constant or a ML object declaration. \Example -\begin{coq_example} +\begin{coq_example*} Axiom X:Set. Axiom x:X. Extract Constant X => "int". Extract Constant x => "0". -\end{coq_example} +\end{coq_example*} Notice that in the case of type scheme axiom (i.e. whose type is an arity, that is a sequence of product finished by a sort), then some type -variables has to be given. The syntax is then: +variables have to be given. The syntax is then: \begin{description} -\item{\tt Extract Constant} \qualid\ \str$_1$ \dots\ \str$_n$ {\tt =>} \str. +\item{\tt Extract Constant \qualid\ \str$_1$ \dots\ \str$_n$ => \str.} \end{description} The number of type variables is checked by the system. \Example -\begin{coq_example} +\begin{coq_example*} Axiom Y : Set -> Set -> Set. Extract Constant Y "'a" "'b" => " 'a*'b ". -\end{coq_example} +\end{coq_example*} Realizing an axiom via {\tt Extract Constant} is only useful in the case of an informative axiom (of sort Type or Set). A logical axiom @@ -308,7 +295,7 @@ types and constructors. For instance, the user may want to use the ML native boolean type instead of \Coq\ one. The syntax is the following: \begin{description} -\item{\tt Extract Inductive} \qualid\ {\tt =>} \str\ {\tt [} \str\ \dots\ \str\ {\tt ]}\ {\it optstring}.\par +\item{\tt Extract Inductive \qualid\ => \str\ [ \str\ \dots\ \str\ ] {\it optstring}.}\par Give an ML extraction for the given inductive type. You must specify extractions for the type itself (first \str) and all its constructors (between square brackets). If given, the final optional @@ -412,7 +399,7 @@ For example, here are two kinds of problem that can occur: \begin{itemize} \item If some part of the program is {\em very} polymorphic, there may be no ML type for it. In that case the extraction to ML works - all right but the generated code may be refused by the ML + alright but the generated code may be refused by the ML type-checker. A very well known example is the {\em distr-pair} function: \begin{verbatim} @@ -549,34 +536,34 @@ Some pathological examples of extraction are grouped in the file \asubsection{Users' Contributions} - Several of the \Coq\ Users' Contributions use extraction to produce - certified programs. In particular the following ones have an automatic - extraction test (just run {\tt make} in those directories): - - \begin{itemize} - \item Bordeaux/Additions - \item Bordeaux/EXCEPTIONS - \item Bordeaux/SearchTrees - \item Dyade/BDDS - \item Lannion - \item Lyon/CIRCUITS - \item Lyon/FIRING-SQUAD - \item Marseille/CIRCUITS - \item Muenchen/Higman - \item Nancy/FOUnify - \item Rocq/ARITH/Chinese - \item Rocq/COC - \item Rocq/GRAPHS - \item Rocq/HIGMAN - \item Sophia-Antipolis/Stalmarck - \item Suresnes/BDD - \end{itemize} - - Lannion, Rocq/HIGMAN and Lyon/CIRCUITS are a bit particular. They are - examples of developments where {\tt Obj.magic} are needed. - This is probably due to an heavy use of impredicativity. - After compilation those two examples run nonetheless, - thanks to the correction of the extraction~\cite{Let02}. +Several of the \Coq\ Users' Contributions use extraction to produce +certified programs. In particular the following ones have an automatic +extraction test: + +\begin{itemize} +\item {\tt additions} +\item {\tt bdds} +\item {\tt canon-bdds} +\item {\tt chinese} +\item {\tt continuations} +\item {\tt coq-in-coq} +\item {\tt exceptions} +\item {\tt firing-squad} +\item {\tt founify} +\item {\tt graphs} +\item {\tt higman-cf} +\item {\tt higman-nw} +\item {\tt hardware} +\item {\tt multiplier} +\item {\tt search-trees} +\item {\tt stalmarck} +\end{itemize} + +{\tt continuations} and {\tt multiplier} are a bit particular. They are +examples of developments where {\tt Obj.magic} are needed. This is +probably due to an heavy use of impredicativity. After compilation, those +two examples run nonetheless, thanks to the correction of the +extraction~\cite{Let02}. %%% Local Variables: %%% mode: latex -- cgit v1.2.3 From 1eb48ca8695a26fa5ca248a2201a164f90885360 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 30 Jul 2015 18:05:41 +0200 Subject: For convenience, making yes and on, and no and off synonymous in command line. Documenting only the former for simplicity and uniformity with predating option -with-geoproof. --- toplevel/coqtop.ml | 12 ++++++------ toplevel/usage.ml | 2 +- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 5540dc0ff1..d67559d77f 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -41,8 +41,8 @@ let toploop = ref None let color : [`ON | `AUTO | `OFF] ref = ref `AUTO let set_color = function -| "on" -> color := `ON -| "off" -> color := `OFF +| "yes" | "on" -> color := `ON +| "no" | "off" -> color := `OFF | "auto" -> color := `AUTO | _ -> prerr_endline ("Error: on/off/auto expected after option color"); exit 1 @@ -326,8 +326,8 @@ let get_priority opt s = prerr_endline ("Error: low/high expected after "^opt); exit 1 let get_async_proofs_mode opt = function - | "off" -> Flags.APoff - | "on" -> Flags.APon + | "no" | "off" -> Flags.APoff + | "yes" | "on" -> Flags.APon | "lazy" -> Flags.APonLazy | _ -> prerr_endline ("Error: on/off/lazy expected after "^opt); exit 1 @@ -341,8 +341,8 @@ let set_worker_id opt s = Flags.async_proofs_worker_id := s let get_bool opt = function - | "yes" -> true - | "no" -> false + | "yes" | "on" -> true + | "no" | "off" -> false | _ -> prerr_endline ("Error: yes/no expected after option "^opt); exit 1 let get_int opt n = diff --git a/toplevel/usage.ml b/toplevel/usage.ml index f3f8dfd8ae..a5d8450b9d 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -58,7 +58,7 @@ let print_usage_channel co command = \n\ \n -quiet unset display of extra information (implies -w none)\ \n -w (all|none) configure display of warnings\ -\n -color (on|off|auto) configure color output\ +\n -color (yes|no|auto) configure color output\ \n\ \n -q skip loading of rcfile\ \n -init-file f set the rcfile to f\ -- cgit v1.2.3 From cb0dea2a0c2993d4ca7747afc61fecdbb1c525b1 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 30 Jul 2015 19:20:39 +0200 Subject: Documenting change of behavior of apply when the lemma is a tuple and applying a component of the tuple. --- CHANGES | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/CHANGES b/CHANGES index 733bcc7cf5..2e5e30ef8d 100644 --- a/CHANGES +++ b/CHANGES @@ -35,7 +35,6 @@ API * A new safe pf_type_of function. All uses of unsafe_* functions should be eventually eliminated. - Tools - Added an option -w to control the output of coqtop warnings. @@ -359,6 +358,10 @@ Tactics trace anymore. Use "Info 1 auto" instead. The same goes for "info_trivial". On the other hand "info_eauto" still works fine, while "Info 1 eauto" prints a trivial trace. +- When using a lemma of the prototypical form "forall A, {a:A & P a}", + "apply" and "apply in" do not instantiate anymore "A" with the + current goal and use "a" as the proof, as they were sometimes doing, + now considering that it is a too powerful decision. Program -- cgit v1.2.3 From 2418cf8d5ff6f479a5b43a87c861141bf9067507 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 31 Jul 2015 21:31:37 +0200 Subject: Granting Jason's request for an ad hoc compatibility option on considering trivial unifications "?x = t" in tactics working under conjunctions (see #3545). Also updating and fixing wrong comments in test apply.v. --- CHANGES | 3 +++ doc/refman/RefMan-tac.tex | 17 +++++++++++++++++ tactics/tactics.ml | 20 +++++++++++++++++++- test-suite/success/apply.v | 36 +++++++++++++++++++----------------- 4 files changed, 58 insertions(+), 18 deletions(-) diff --git a/CHANGES b/CHANGES index 2e5e30ef8d..08484a4b9b 100644 --- a/CHANGES +++ b/CHANGES @@ -20,6 +20,9 @@ Tactics will eventually fail and backtrack. * "Strict" changes the behavior of an unloaded hint to the one of the fail tactic, allowing to emulate the hopefully future import-scoped hint mechanism. +- New compatibility flag "Universal Lemma Under Conjunction" which + let tactics working under conjunctions apply sublemmas of the form + "forall A, ... -> A". API diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index cc262708ab..fa6f783934 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -485,7 +485,24 @@ apply Rmp. Reset R. \end{coq_eval} +\noindent {\bf Remark: } When the conclusion of the type of the term +to apply is an inductive type isomorphic to a tuple type and {\em apply} +looks recursively whether a component of the tuple matches the goal, +it excludes components whose statement would result in applying an +universal lemma of the form {\tt forall A, ... -> A}. Excluding this +kind of lemma can be avoided by setting the following option: + +\begin{quote} +\optindex{Universal Lemma Under Conjunction} +{\tt Set Universal Lemma Under Conjunction} +\end{quote} + +This option, which preserves compatibility with versions of {\Coq} +prior to 8.4 is also available for {\tt apply {\term} in {\ident}} +(see Section~\ref{apply-in}). + \subsection{\tt apply {\term} in {\ident}} +\label{apply-in} \tacindex{apply \dots\ in} This tactic applies to any goal. The argument {\term} is a term diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 402a9e88a1..6d81a48705 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -109,6 +109,24 @@ let _ = optread = (fun () -> !clear_hyp_by_default) ; optwrite = (fun b -> clear_hyp_by_default := b) } +(* Compatibility option useful in developments using apply intensively + in ltac code *) + +let universal_lemma_under_conjunctions = ref false + +let accept_universal_lemma_under_conjunctions () = + !universal_lemma_under_conjunctions + +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "trivial unification in tactics applying under conjunctions"; + optkey = ["Universal";"Lemma";"Under";"Conjunction"]; + optread = (fun () -> !universal_lemma_under_conjunctions) ; + optwrite = (fun b -> universal_lemma_under_conjunctions := b) } + + (*********************************************) (* Tactics *) (*********************************************) @@ -1332,7 +1350,7 @@ let make_projection env sigma params cstr sign elim i n c u = (* to avoid surprising unifications, excludes flexible projection types or lambda which will be instantiated by Meta/Evar *) && not (isEvar (fst (whd_betaiota_stack sigma t))) - && not (isRel t && destRel t > n-i) + && (accept_universal_lemma_under_conjunctions () || not (isRel t)) then let t = lift (i+1-n) t in let abselim = beta_applist (elim,params@[t;branch]) in diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index a4ed76c5a0..24d5cf8a99 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -333,13 +333,10 @@ exact (refl_equal 3). exact (refl_equal 4). Qed. -(* From 12612, descent in conjunctions is more powerful *) +(* From 12612, Dec 2009, descent in conjunctions is more powerful *) (* The following, which was failing badly in bug 1980, is now properly rejected, as descend in conjunctions builds an - ill-formed elimination from Prop to Type. - - Added Aug 2014: why it fails is now that trivial unification ?x = goal is - rejected by the descent in conjunctions to avoid surprising results. *) + ill-formed elimination from Prop to the domain of ex which is in Type. *) Goal True. Fail eapply ex_intro. @@ -351,28 +348,32 @@ Fail eapply (ex_intro _). exact I. Qed. -(* Note: the following succeed directly (i.e. w/o "exact I") since - Aug 2014 since the descent in conjunction does not use a "cut" - anymore: the iota-redex is contracted and we get rid of the - uninstantiated evars - - Is it good or not? Maybe it does not matter so much. +(* No failure here, because the domain of ex is in Prop *) Goal True. -eapply (ex_intro (fun _ => True) I). -exact I. (* Not needed since Aug 2014 *) +eapply (ex_intro (fun _ => 0=0) I). +reflexivity. Qed. Goal True. -eapply (ex_intro (fun _ => True) I _). -exact I. (* Not needed since Aug 2014 *) +eapply (ex_intro (fun _ => 0=0) I _). +Unshelve. (* In 8.4: Grab Existential Variables. *) +reflexivity. Qed. Goal True. eapply (fun (A:Prop) (x:A) => conj I x). -exact I. (* Not needed since Aug 2014 *) +Unshelve. (* In 8.4: the goal ?A was there *) +exact I. Qed. -*) + +(* Testing compatibility mode with v8.4 *) + +Goal True. +Fail eapply existT. +Set Trivial Tactic Unification Under Conjunction. +eapply existT. +Abort. (* The following was not accepted from r12612 to r12657 *) @@ -463,6 +464,7 @@ Abort. Goal forall H:0=0, H = H. intros. Fail apply eq_sym in H. +Abort. (* Check that unresolved evars not originally present in goal prevent apply in to work*) -- cgit v1.2.3 From 817308ab59daa40bef09838cfc3d810863de0e46 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 2 Aug 2015 16:53:39 +0200 Subject: Fixing #4221 (interpreting bound variables using ltac env was possibly capturing bound names unexpectingly). We moved renaming to after finding bindings, i.e. in pretyping "fun x y => x + y" in an ltac environment where y is ltac-bound to x, we type the body in environment "x y |-" but build "fun y y => Rel 2 + Rel 1" (which later on is displayed into "fun y y0 => y + y0"). We renounced to renaming in "match" patterns, which was anyway not working well, as e.g. in let x := ipattern:y in (forall z, match z with S x => x | x => x end = 0). which was producing forall z : nat, match z with 0 => z | S y => y end = 0 because the names in default branches are treated specifically. It would be easy to support renaming in match again, by putting the ltac env in the Cases.pattern_matching_problem state and to rename the names in "typs" (from build_branch), just before returning them at the end of the function (and similarly in abstract_predicate for the names occurring in the return predicate). However, we rename binders in fix which were not interpreted. There are some difficulties with evar because we want them defined in the interpreted env (see comment to ltac_interp_name_env). fix ltac name --- pretyping/pretyping.ml | 76 ++++++++++++++++++++++++++----------------- pretyping/pretyping.mli | 4 +-- test-suite/bugs/closed/4221.v | 9 +++++ test-suite/success/ltac.v | 8 +++++ 4 files changed, 65 insertions(+), 32 deletions(-) create mode 100644 test-suite/bugs/closed/4221.v diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 03fe2122c0..a212735c04 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -270,6 +270,18 @@ let ltac_interp_name { ltac_idents ; ltac_genargs } = function str"It cannot be used in a binder.") else n +let ltac_interp_name_env k0 lvar env = + (* envhd is the initial part of the env when pretype was called first *) + (* (in practice is is probably 0, but we have to grant the + specification of pretype which accepts to start with a non empty + rel_context) *) + (* tail is the part of the env enriched by pretyping *) + let n = rel_context_length (rel_context env) - k0 in + let ctxt,_ = List.chop n (rel_context env) in + let env = pop_rel_context n env in + let ctxt = List.map (fun (na,c,t) -> ltac_interp_name lvar na,c,t) ctxt in + push_rel_context ctxt env + let invert_ltac_bound_name lvar env id0 id = let id = Id.Map.find id lvar.ltac_idents in try mkRel (pi1 (lookup_rel_id id (rel_context env))) @@ -289,10 +301,6 @@ let pretype_id pretype loc env evdref lvar id = let sigma = !evdref in (* Look for the binder of [id] *) try - let id = - try Id.Map.find id lvar.ltac_idents - with Not_found -> id - in let (n,_,typ) = lookup_rel_id id (rel_context env) in { uj_val = mkRel n; uj_type = lift n typ } with Not_found -> @@ -413,10 +421,10 @@ let is_GHole = function let evars = ref Id.Map.empty -let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var_map) t = +let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var_map) t = let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in - let pretype_type = pretype_type resolve_tc in - let pretype = pretype resolve_tc in + let pretype_type = pretype_type k0 resolve_tc in + let pretype = pretype k0 resolve_tc in match t with | GRef (loc,ref,u) -> inh_conv_coerce_to_tycon loc env evdref @@ -436,12 +444,13 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var with Not_found -> user_err_loc (loc,"",str "Unknown existential variable.") in let hyps = evar_filtered_context (Evd.find !evdref evk) in - let args = pretype_instance resolve_tc env evdref lvar loc hyps evk inst in + let args = pretype_instance k0 resolve_tc env evdref lvar loc hyps evk inst in let c = mkEvar (evk, args) in let j = (Retyping.get_judgment_of env !evdref c) in inh_conv_coerce_to_tycon loc env evdref j tycon | GPatVar (loc,(someta,n)) -> + let env = ltac_interp_name_env k0 lvar env in let ty = match tycon with | Some ty -> ty @@ -450,6 +459,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty } | GHole (loc, k, naming, None) -> + let env = ltac_interp_name_env k0 lvar env in let ty = match tycon with | Some ty -> ty @@ -458,6 +468,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var { uj_val = e_new_evar env evdref ~src:(loc,k) ~naming ty; uj_type = ty } | GHole (loc, k, _naming, Some arg) -> + let env = ltac_interp_name_env k0 lvar env in let ty = match tycon with | Some ty -> ty @@ -474,12 +485,14 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var | (na,bk,None,ty)::bl -> let ty' = pretype_type empty_valcon env evdref lvar ty in let dcl = (na,None,ty'.utj_val) in - type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl + let dcl' = (ltac_interp_name lvar na,None,ty'.utj_val) in + type_bl (push_rel dcl env) (add_rel_decl dcl' ctxt) bl | (na,bk,Some bd,ty)::bl -> let ty' = pretype_type empty_valcon env evdref lvar ty in let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar bd in let dcl = (na,Some bd'.uj_val,ty'.utj_val) in - type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl in + let dcl' = (ltac_interp_name lvar na,Some bd'.uj_val,ty'.utj_val) in + type_bl (push_rel dcl env) (add_rel_decl dcl' ctxt) bl in let ctxtv = Array.map (type_bl env empty_rel_context) bl in let larj = Array.map2 @@ -647,9 +660,9 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var (* The name specified by ltac is used also to create bindings. So the substitution must also be applied on variables before they are looked up in the rel context. *) - let name = ltac_interp_name lvar name in let var = (name,None,j.utj_val) in let j' = pretype rng (push_rel var env) evdref lvar c2 in + let name = ltac_interp_name lvar name in let resj = judge_of_abstraction env (orelse_name name name') j j' in inh_conv_coerce_to_tycon loc env evdref resj tycon @@ -658,7 +671,6 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var (* The name specified by ltac is used also to create bindings. So the substitution must also be applied on variables before they are looked up in the rel context. *) - let name = ltac_interp_name lvar name in let j' = match name with | Anonymous -> let j = pretype_type empty_valcon env evdref lvar c2 in @@ -668,6 +680,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var let env' = push_rel_assum var env in pretype_type empty_valcon env' evdref lvar c2 in + let name = ltac_interp_name lvar name in let resj = try judge_of_product env name j j' @@ -689,10 +702,10 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var (* The name specified by ltac is used also to create bindings. So the substitution must also be applied on variables before they are looked up in the rel context. *) - let name = ltac_interp_name lvar name in let var = (name,Some j.uj_val,t) in let tycon = lift_tycon 1 tycon in let j' = pretype tycon (push_rel var env) evdref lvar c2 in + let name = ltac_interp_name lvar name in { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ; uj_type = subst1 j.uj_val j'.uj_type } @@ -712,8 +725,6 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var if not (Int.equal (List.length nal) cs.cs_nargs) then user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables."); - let nal = List.map (fun na -> ltac_interp_name lvar na) nal in - let na = ltac_interp_name lvar na in let fsign, record = match get_projections env indf with | None -> List.map2 (fun na (_,c,t) -> (na,c,t)) @@ -729,10 +740,12 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var (na, c, t) :: aux (n+1) k names l | [], [] -> [] | _ -> assert false - in aux 1 1 (List.rev nal) cs.cs_args, true - in + in aux 1 1 (List.rev nal) cs.cs_args, true in let obj ind p v f = if not record then + let nal = List.map (fun na -> ltac_interp_name lvar na) nal in + let nal = List.rev nal in + let fsign = List.map2 (fun na (_,b,t) -> (na,b,t)) nal fsign in let f = it_mkLambda_or_LetIn f fsign in let ci = make_case_info env (fst ind) LetStyle in mkCase (ci, p, cj.uj_val,[|f|]) @@ -818,7 +831,9 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var | None -> let p = match tycon with | Some ty -> ty - | None -> new_type_evar env evdref loc + | None -> + let env = ltac_interp_name_env k0 lvar env in + new_type_evar env evdref loc in it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in let pred = nf_evar !evdref pred in @@ -854,9 +869,6 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var inh_conv_coerce_to_tycon loc env evdref cj tycon | GCases (loc,sty,po,tml,eqns) -> - let (tml,eqns) = - Glob_ops.map_pattern_binders (fun na -> ltac_interp_name lvar na) tml eqns - in Cases.compile_cases loc sty ((fun vtyc env evdref -> pretype vtyc env evdref lvar),evdref) tycon env (* loc *) (po,tml,eqns) @@ -903,13 +915,13 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var { uj_val = v; uj_type = tval } in inh_conv_coerce_to_tycon loc env evdref cj tycon -and pretype_instance resolve_tc env evdref lvar loc hyps evk update = +and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = let f (id,_,t) (subst,update) = let t = replace_vars subst t in let c, update = try let c = List.assoc id update in - let c = pretype resolve_tc (mk_tycon t) env evdref lvar c in + let c = pretype k0 resolve_tc (mk_tycon t) env evdref lvar c in c.uj_val, List.remove_assoc id update with Not_found -> try @@ -929,7 +941,7 @@ and pretype_instance resolve_tc env evdref lvar loc hyps evk update = Array.map_of_list snd subst (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) -and pretype_type resolve_tc valcon env evdref lvar = function +and pretype_type k0 resolve_tc valcon env evdref lvar = function | GHole (loc, knd, naming, None) -> (match valcon with | Some v -> @@ -945,11 +957,12 @@ and pretype_type resolve_tc valcon env evdref lvar = function { utj_val = v; utj_type = s } | None -> + let env = ltac_interp_name_env k0 lvar env in let s = evd_comb0 (new_sort_variable univ_flexible_alg) evdref in { utj_val = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s); utj_type = s}) | c -> - let j = pretype resolve_tc empty_tycon env evdref lvar c in + let j = pretype k0 resolve_tc empty_tycon env evdref lvar c in let loc = loc_of_glob_constr c in let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in match valcon with @@ -962,13 +975,14 @@ and pretype_type resolve_tc valcon env evdref lvar = function let ise_pretype_gen flags env sigma lvar kind c = let evdref = ref sigma in + let k0 = rel_context_length (rel_context env) in let c' = match kind with | WithoutTypeConstraint -> - (pretype flags.use_typeclasses empty_tycon env evdref lvar c).uj_val + (pretype k0 flags.use_typeclasses empty_tycon env evdref lvar c).uj_val | OfType exptyp -> - (pretype flags.use_typeclasses (mk_tycon exptyp) env evdref lvar c).uj_val + (pretype k0 flags.use_typeclasses (mk_tycon exptyp) env evdref lvar c).uj_val | IsType -> - (pretype_type flags.use_typeclasses empty_valcon env evdref lvar c).utj_val + (pretype_type k0 flags.use_typeclasses empty_valcon env evdref lvar c).utj_val in process_inference_flags flags env sigma (!evdref,c') @@ -1003,14 +1017,16 @@ let on_judgment f j = let understand_judgment env sigma c = let evdref = ref sigma in - let j = pretype true empty_tycon env evdref empty_lvar c in + let k0 = rel_context_length (rel_context env) in + let j = pretype k0 true empty_tycon env evdref empty_lvar c in let j = on_judgment (fun c -> let evd, c = process_inference_flags all_and_fail_flags env sigma (!evdref,c) in evdref := evd; c) j in j, Evd.evar_universe_context !evdref let understand_judgment_tcc env evdref c = - let j = pretype true empty_tycon env evdref empty_lvar c in + let k0 = rel_context_length (rel_context env) in + let j = pretype k0 true empty_tycon env evdref empty_lvar c in on_judgment (fun c -> let (evd,c) = process_inference_flags all_no_fail_flags env Evd.empty (!evdref,c) in evdref := evd; c) j diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 142b54513e..a6aa086579 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -123,11 +123,11 @@ val check_evars_are_solved : (**/**) (** Internal of Pretyping... *) val pretype : - bool -> type_constraint -> env -> evar_map ref -> + int -> bool -> type_constraint -> env -> evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment val pretype_type : - bool -> val_constraint -> env -> evar_map ref -> + int -> bool -> val_constraint -> env -> evar_map ref -> ltac_var_map -> glob_constr -> unsafe_type_judgment val ise_pretype_gen : diff --git a/test-suite/bugs/closed/4221.v b/test-suite/bugs/closed/4221.v new file mode 100644 index 0000000000..bc120fb1ff --- /dev/null +++ b/test-suite/bugs/closed/4221.v @@ -0,0 +1,9 @@ +(* Some test checking that interpreting binder names using ltac + context does not accidentally break the bindings *) + +Goal (forall x : nat, x = 1 -> False) -> 1 = 1 -> False. + intros H0 x. + lazymatch goal with + | [ x : forall k : nat, _ |- _ ] + => specialize (fun H0 => x 1 H0) + end. diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index badce063e8..952f35bc35 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -298,3 +298,11 @@ evar(foo:nat). let evval := eval compute in foo in not_eq evval 1. let evval := eval compute in foo in not_eq 1 evval. Abort. + +(* Check instantiation of binders using ltac names *) + +Goal True. +let x := ipattern:y in assert (forall x y, x = y + 0). +intro. +destruct y. (* Check that the name is y here *). +Abort. -- cgit v1.2.3 From fdab811e58094accc02875c1f83e6476f4598d26 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 31 Jul 2015 18:33:06 +0200 Subject: Removing the generalization of the body of inductive schemes from Auto_ind_decl over the internal lemmas. The schemes are built in the main process and the internal lemmas are actually already also in the environment. --- proofs/pfedit.ml | 4 ++-- proofs/pfedit.mli | 2 +- toplevel/auto_ind_decl.ml | 6 +++--- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index d024c01ba5..bde0a1c168 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -145,12 +145,12 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo delete_current_proof (); iraise reraise -let build_by_tactic env ctx ?(poly=false) typ tac = +let build_by_tactic ?(side_eff=true) env ctx ?(poly=false) typ tac = let id = Id.of_string ("temporary_proof"^string_of_int (next())) in let sign = val_of_named_context (named_context env) in let gk = Global, poly, Proof Theorem in let ce, status, univs = build_constant_by_tactic id ctx sign ~goal_kind:gk typ tac in - let ce = Term_typing.handle_entry_side_effects env ce in + let ce = if side_eff then Term_typing.handle_entry_side_effects env ce else { ce with const_entry_body = Future.chain ~pure:true ce.const_entry_body (fun (pt, _) -> pt, Declareops.no_seff) } in let (cb, ctx), se = Future.force ce.const_entry_body in assert(Declareops.side_effects_is_empty se); assert(Univ.ContextSet.is_empty ctx); diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 5e0fb4dd36..4aa3c3bfd2 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -153,7 +153,7 @@ val build_constant_by_tactic : types -> unit Proofview.tactic -> Entries.definition_entry * bool * Evd.evar_universe_context -val build_by_tactic : env -> Evd.evar_universe_context -> ?poly:polymorphic -> +val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic -> types -> unit Proofview.tactic -> constr * bool * Evd.evar_universe_context diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index d1452fca21..16683d243e 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -637,7 +637,7 @@ let make_bl_scheme mind = context_chop (nparams-nparrec) mib.mind_params_ctxt in let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in let ctx = Evd.empty_evar_universe_context (*FIXME univs *) in - let (ans, _, ctx) = Pfedit.build_by_tactic (Global.env()) ctx bl_goal + let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff:false (Global.env()) ctx bl_goal (compute_bl_tact (!bl_scheme_kind_aux()) (ind, Univ.Instance.empty) lnamesparrec nparrec) in ([|ans|], ctx), eff @@ -759,7 +759,7 @@ let make_lb_scheme mind = context_chop (nparams-nparrec) mib.mind_params_ctxt in let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in let ctx = Evd.empty_evar_universe_context in - let (ans, _, ctx) = Pfedit.build_by_tactic (Global.env()) ctx lb_goal + let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff:false (Global.env()) ctx lb_goal (compute_lb_tact (!lb_scheme_kind_aux()) ind lnamesparrec nparrec) in ([|ans|], ctx (* FIXME *)), eff @@ -930,7 +930,7 @@ let make_eq_decidability mind = let ctx = Evd.empty_evar_universe_context (* FIXME *)in let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in - let (ans, _, ctx) = Pfedit.build_by_tactic (Global.env()) ctx + let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff:false (Global.env()) ctx (compute_dec_goal (ind,u) lnamesparrec nparrec) (compute_dec_tact ind lnamesparrec nparrec) in -- cgit v1.2.3 From d8226295e6237a43de33475f798c3c8ac6ac4866 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 31 Jul 2015 18:45:41 +0200 Subject: Give a way to control if the decidable-equality schemes are built like in 8.4 with the schemes of the subcomponent of an inductive added to the environment or discharged as let-ins over the main scheme. As of today, decidable-equality schemes are built when calling vernacular command (Inductive with option Set Dedicable Equality Schemes, or Scheme Equality), so there is no need to discharge the sub-schemes as let-ins. But if ever the schemes are built from within an opaque proof and one would not like the schemes and a fortiori the subschemes to appear in the env, the new addition of a parameter internal_flag to "find_scheme" allows this possibility (then to be set to KernelSilent). --- tactics/elimschemes.ml | 20 ++++++++++---------- tactics/eqschemes.ml | 18 +++++++++--------- toplevel/auto_ind_decl.ml | 42 +++++++++++++++++++++++++----------------- toplevel/ind_tables.ml | 32 +++++++++++++++----------------- toplevel/ind_tables.mli | 15 ++++++--------- 5 files changed, 65 insertions(+), 62 deletions(-) diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 749e0d2b5b..dbaa60d610 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -21,7 +21,7 @@ open Ind_tables (* Induction/recursion schemes *) -let optimize_non_type_induction_scheme kind dep sort ind = +let optimize_non_type_induction_scheme kind dep sort _ ind = let env = Global.env () in let sigma = Evd.from_env env in if check_scheme kind ind then @@ -68,15 +68,15 @@ let build_induction_scheme_in_type dep sort ind = let rect_scheme_kind_from_type = declare_individual_scheme_object "_rect_nodep" - (fun x -> build_induction_scheme_in_type false InType x, Declareops.no_seff) + (fun _ x -> build_induction_scheme_in_type false InType x, Declareops.no_seff) let rect_scheme_kind_from_prop = declare_individual_scheme_object "_rect" ~aux:"_rect_from_prop" - (fun x -> build_induction_scheme_in_type false InType x, Declareops.no_seff) + (fun _ x -> build_induction_scheme_in_type false InType x, Declareops.no_seff) let rect_dep_scheme_kind_from_type = declare_individual_scheme_object "_rect" ~aux:"_rect_from_type" - (fun x -> build_induction_scheme_in_type true InType x, Declareops.no_seff) + (fun _ x -> build_induction_scheme_in_type true InType x, Declareops.no_seff) let ind_scheme_kind_from_type = declare_individual_scheme_object "_ind_nodep" @@ -109,24 +109,24 @@ let build_case_analysis_scheme_in_type dep sort ind = let case_scheme_kind_from_type = declare_individual_scheme_object "_case_nodep" - (fun x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff) let case_scheme_kind_from_prop = declare_individual_scheme_object "_case" ~aux:"_case_from_prop" - (fun x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff) let case_dep_scheme_kind_from_type = declare_individual_scheme_object "_case" ~aux:"_case_from_type" - (fun x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff) let case_dep_scheme_kind_from_type_in_prop = declare_individual_scheme_object "_casep_dep" - (fun x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff) let case_dep_scheme_kind_from_prop = declare_individual_scheme_object "_case_dep" - (fun x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff) let case_dep_scheme_kind_from_prop_in_prop = declare_individual_scheme_object "_casep" - (fun x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff) diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 8643fe10f0..f7d3ad5d0a 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -191,7 +191,7 @@ let build_sym_scheme env ind = let sym_scheme_kind = declare_individual_scheme_object "_sym_internal" - (fun ind -> + (fun _ ind -> let c, ctx = build_sym_scheme (Global.env() (* side-effect! *)) ind in (c, ctx), Declareops.no_seff) @@ -262,7 +262,7 @@ let build_sym_involutive_scheme env ind = let sym_involutive_scheme_kind = declare_individual_scheme_object "_sym_involutive" - (fun ind -> + (fun _ ind -> build_sym_involutive_scheme (Global.env() (* side-effect! *)) ind) (**********************************************************************) @@ -650,7 +650,7 @@ let build_r2l_forward_rew_scheme = build_r2l_forward_rew_scheme (**********************************************************************) let rew_l2r_dep_scheme_kind = declare_individual_scheme_object "_rew_r_dep" - (fun ind -> build_l2r_rew_scheme true (Global.env()) ind InType) + (fun _ ind -> build_l2r_rew_scheme true (Global.env()) ind InType) (**********************************************************************) (* Dependent rewrite from right-to-left in conclusion *) @@ -660,7 +660,7 @@ let rew_l2r_dep_scheme_kind = (**********************************************************************) let rew_r2l_dep_scheme_kind = declare_individual_scheme_object "_rew_dep" - (fun ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) + (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) (**********************************************************************) (* Dependent rewrite from right-to-left in hypotheses *) @@ -670,7 +670,7 @@ let rew_r2l_dep_scheme_kind = (**********************************************************************) let rew_r2l_forward_dep_scheme_kind = declare_individual_scheme_object "_rew_fwd_dep" - (fun ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) + (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) (**********************************************************************) (* Dependent rewrite from left-to-right in hypotheses *) @@ -680,7 +680,7 @@ let rew_r2l_forward_dep_scheme_kind = (**********************************************************************) let rew_l2r_forward_dep_scheme_kind = declare_individual_scheme_object "_rew_fwd_r_dep" - (fun ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) + (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) (**********************************************************************) (* Non-dependent rewrite from either left-to-right in conclusion or *) @@ -693,7 +693,7 @@ let rew_l2r_forward_dep_scheme_kind = (**********************************************************************) let rew_l2r_scheme_kind = declare_individual_scheme_object "_rew_r" - (fun ind -> fix_r2l_forward_rew_scheme + (fun _ ind -> fix_r2l_forward_rew_scheme (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Declareops.no_seff) (**********************************************************************) @@ -704,7 +704,7 @@ let rew_l2r_scheme_kind = (**********************************************************************) let rew_r2l_scheme_kind = declare_individual_scheme_object "_rew" - (fun ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Declareops.no_seff) + (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Declareops.no_seff) (* End of rewriting schemes *) @@ -780,6 +780,6 @@ let build_congr env (eq,refl,ctx) ind = in c, Evd.evar_universe_context_of ctx let congr_scheme_kind = declare_individual_scheme_object "_congr" - (fun ind -> + (fun _ ind -> (* May fail if equality is not defined *) build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind, Declareops.no_seff) diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 16683d243e..118ffb3e80 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -111,7 +111,7 @@ let check_bool_is_defined () = let beq_scheme_kind_aux = ref (fun _ -> failwith "Undefined") -let build_beq_scheme kn = +let build_beq_scheme mode kn = check_bool_is_defined (); (* fetching global env *) let env = Global.env() in @@ -188,7 +188,7 @@ let build_beq_scheme kn = else begin try let eq, eff = - let c, eff = find_scheme (!beq_scheme_kind_aux()) (kn',i) in + let c, eff = find_scheme ~mode (!beq_scheme_kind_aux()) (kn',i) in mkConst c, eff in let eqa, eff = let eqa, effs = List.split (List.map aux a) in @@ -330,7 +330,7 @@ let destruct_ind c = so from Ai we can find the the correct eq_Ai bl_ai or lb_ai *) (* used in the leib -> bool side*) -let do_replace_lb lb_scheme_key aavoid narg p q = +let do_replace_lb mode lb_scheme_key aavoid narg p q = let avoid = Array.of_list aavoid in let do_arg v offset = try @@ -360,7 +360,7 @@ let do_replace_lb lb_scheme_key aavoid narg p q = let u,v = destruct_ind type_of_pq in let lb_type_of_p = try - let c, eff = find_scheme lb_scheme_key (out_punivs u) (*FIXME*) in + let c, eff = find_scheme ~mode lb_scheme_key (out_punivs u) (*FIXME*) in Proofview.tclUNIT (mkConst c, eff) with Not_found -> (* spiwack: the format of this error message should probably @@ -388,7 +388,7 @@ let do_replace_lb lb_scheme_key aavoid narg p q = end (* used in the bool -> leib side *) -let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt = +let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = let avoid = Array.of_list aavoid in let do_arg v offset = try @@ -551,7 +551,7 @@ let compute_bl_goal ind lnamesparrec nparrec = (mkApp(Lazy.force eq,[|mkFullInd (ind,u) (nparrec+3);mkVar n;mkVar m|])) ))), eff -let compute_bl_tact bl_scheme_key ind lnamesparrec nparrec = +let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec = let list_id = list_id lnamesparrec in let avoid = ref [] in let first_intros = @@ -608,7 +608,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). if eq_gr (IndRef indeq) Coqlib.glob_eq then Tacticals.New.tclTHEN - (do_replace_bl bl_scheme_key ind + (do_replace_bl mode bl_scheme_key ind (!avoid) nparrec (ca.(2)) (ca.(1))) @@ -625,7 +625,12 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). let bl_scheme_kind_aux = ref (fun _ -> failwith "Undefined") -let make_bl_scheme mind = +let side_effect_of_mode = function + | Declare.KernelVerbose -> false + | Declare.KernelSilent -> true + | Declare.UserVerbose -> false + +let make_bl_scheme mode mind = let mib = Global.lookup_mind mind in if not (Int.equal (Array.length mib.mind_packets) 1) then errorlabstrm "" @@ -637,8 +642,9 @@ let make_bl_scheme mind = context_chop (nparams-nparrec) mib.mind_params_ctxt in let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in let ctx = Evd.empty_evar_universe_context (*FIXME univs *) in - let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff:false (Global.env()) ctx bl_goal - (compute_bl_tact (!bl_scheme_kind_aux()) (ind, Univ.Instance.empty) lnamesparrec nparrec) + let side_eff = side_effect_of_mode mode in + let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx bl_goal + (compute_bl_tact mode (!bl_scheme_kind_aux()) (ind, Univ.Instance.empty) lnamesparrec nparrec) in ([|ans|], ctx), eff @@ -688,7 +694,7 @@ let compute_lb_goal ind lnamesparrec nparrec = (mkApp(eq,[|bb;mkApp(eqI,[|mkVar n;mkVar m|]);tt|])) ))), eff -let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec = +let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = let list_id = list_id lnamesparrec in let avoid = ref [] in let first_intros = @@ -732,7 +738,7 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec = | App(c,ca) -> (match (kind_of_term ca.(1)) with | App(c',ca') -> let n = Array.length ca' in - do_replace_lb lb_scheme_key + do_replace_lb mode lb_scheme_key (!avoid) nparrec ca'.(n-2) ca'.(n-1) @@ -747,7 +753,7 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec = let lb_scheme_kind_aux = ref (fun () -> failwith "Undefined") -let make_lb_scheme mind = +let make_lb_scheme mode mind = let mib = Global.lookup_mind mind in if not (Int.equal (Array.length mib.mind_packets) 1) then errorlabstrm "" @@ -759,8 +765,9 @@ let make_lb_scheme mind = context_chop (nparams-nparrec) mib.mind_params_ctxt in let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in let ctx = Evd.empty_evar_universe_context in - let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff:false (Global.env()) ctx lb_goal - (compute_lb_tact (!lb_scheme_kind_aux()) ind lnamesparrec nparrec) + let side_eff = side_effect_of_mode mode in + let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx lb_goal + (compute_lb_tact mode (!lb_scheme_kind_aux()) ind lnamesparrec nparrec) in ([|ans|], ctx (* FIXME *)), eff @@ -919,7 +926,7 @@ let compute_dec_tact ind lnamesparrec nparrec = ] end -let make_eq_decidability mind = +let make_eq_decidability mode mind = let mib = Global.lookup_mind mind in if not (Int.equal (Array.length mib.mind_packets) 1) then raise DecidabilityMutualNotSupported; @@ -930,7 +937,8 @@ let make_eq_decidability mind = let ctx = Evd.empty_evar_universe_context (* FIXME *)in let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in - let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff:false (Global.env()) ctx + let side_eff = side_effect_of_mode mode in + let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx (compute_dec_goal (ind,u) lnamesparrec nparrec) (compute_dec_tact ind lnamesparrec nparrec) in diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index 0d39466ede..b59d6fc8ae 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -28,11 +28,10 @@ open Pp (**********************************************************************) (* Registering schemes in the environment *) - type mutual_scheme_object_function = - mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects + internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects type individual_scheme_object_function = - inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects + internal_flag -> inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects type 'a scheme_kind = string @@ -141,32 +140,31 @@ let define internal id c p univs = in kn -let define_individual_scheme_base kind suff f internal idopt (mind,i as ind) = - let (c, ctx), eff = f ind in +let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) = + let (c, ctx), eff = f mode ind in let mib = Global.lookup_mind mind in let id = match idopt with | Some id -> id | None -> add_suffix mib.mind_packets.(i).mind_typename suff in - let const = define internal id c mib.mind_polymorphic ctx in + let const = define mode id c mib.mind_polymorphic ctx in declare_scheme kind [|ind,const|]; const, Declareops.cons_side_effects (Safe_typing.sideff_of_scheme kind (Global.safe_env()) [ind,const]) eff -let define_individual_scheme kind internal names (mind,i as ind) = +let define_individual_scheme kind mode names (mind,i as ind) = match Hashtbl.find scheme_object_table kind with | _,MutualSchemeFunction f -> assert false | s,IndividualSchemeFunction f -> - define_individual_scheme_base kind s f internal names ind + define_individual_scheme_base kind s f mode names ind -let define_mutual_scheme_base kind suff f internal names mind = - let (cl, ctx), eff = f mind in +let define_mutual_scheme_base kind suff f mode names mind = + let (cl, ctx), eff = f mode mind in let mib = Global.lookup_mind mind in let ids = Array.init (Array.length mib.mind_packets) (fun i -> try Int.List.assoc i names with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in - let consts = Array.map2 (fun id cl -> - define internal id cl mib.mind_polymorphic ctx) ids cl in + define mode id cl mib.mind_polymorphic ctx) ids cl in let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in declare_scheme kind schemes; consts, @@ -175,11 +173,11 @@ let define_mutual_scheme_base kind suff f internal names mind = kind (Global.safe_env()) (Array.to_list schemes)) eff -let define_mutual_scheme kind internal names mind = +let define_mutual_scheme kind mode names mind = match Hashtbl.find scheme_object_table kind with | _,IndividualSchemeFunction _ -> assert false | s,MutualSchemeFunction f -> - define_mutual_scheme_base kind s f internal names mind + define_mutual_scheme_base kind s f mode names mind let find_scheme_on_env_too kind ind = let s = String.Map.find kind (Indmap.find ind !scheme_map) in @@ -188,14 +186,14 @@ let find_scheme_on_env_too kind ind = kind (Global.safe_env()) [ind, s]) Declareops.no_seff -let find_scheme kind (mind,i as ind) = +let find_scheme ?(mode=KernelSilent) kind (mind,i as ind) = try find_scheme_on_env_too kind ind with Not_found -> match Hashtbl.find scheme_object_table kind with | s,IndividualSchemeFunction f -> - define_individual_scheme_base kind s f KernelSilent None ind + define_individual_scheme_base kind s f mode None ind | s,MutualSchemeFunction f -> - let ca, eff = define_mutual_scheme_base kind s f KernelSilent [] mind in + let ca, eff = define_mutual_scheme_base kind s f mode [] mind in ca.(i), eff let check_scheme kind ind = diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli index 98eaac0928..d0844dd946 100644 --- a/toplevel/ind_tables.mli +++ b/toplevel/ind_tables.mli @@ -8,6 +8,7 @@ open Term open Names +open Declare (** This module provides support for registering inductive scheme builders, declaring schemes and generating schemes on demand *) @@ -19,9 +20,9 @@ type individual type 'a scheme_kind type mutual_scheme_object_function = - mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects + internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects type individual_scheme_object_function = - inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects + internal_flag -> inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects (** Main functions to register a scheme builder *) @@ -32,21 +33,17 @@ val declare_individual_scheme_object : string -> ?aux:string -> individual_scheme_object_function -> individual scheme_kind -(* -val declare_scheme : 'a scheme_kind -> (inductive * constant) array -> unit -*) - (** Force generation of a (mutually) scheme with possibly user-level names *) val define_individual_scheme : individual scheme_kind -> - Declare.internal_flag (** internal *) -> + internal_flag (** internal *) -> Id.t option -> inductive -> constant * Declareops.side_effects -val define_mutual_scheme : mutual scheme_kind -> Declare.internal_flag (** internal *) -> +val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) -> (int * Id.t) list -> mutual_inductive -> constant array * Declareops.side_effects (** Main function to retrieve a scheme in the cache or to generate it *) -val find_scheme : 'a scheme_kind -> inductive -> constant * Declareops.side_effects +val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> constant * Declareops.side_effects val check_scheme : 'a scheme_kind -> inductive -> bool -- cgit v1.2.3 From f556da10a117396c2c796f6915321b67849f65cd Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 31 Jul 2015 18:53:21 +0200 Subject: Adding eq/compare/hash for syntactic view at constant/inductive/constructor kernel_name pairs rather than viewing them from only the user or canonical part. Hopefully more uniformity in Constr.hasheq (using systematically == on subterms). A semantic change: Cooking now indexing again on full pairs of kernel names rather than only on the canonical names, so as to preserve user name. Also, in pair of kernel names, ensuring the compact representation is used as soon as both names are the same. --- kernel/constr.ml | 20 +++++++++----------- kernel/cooking.ml | 12 ++++++------ kernel/names.ml | 42 +++++++++++++++++++++++++++++++++++++++++- kernel/names.mli | 26 +++++++++++++++++++++++++- 4 files changed, 81 insertions(+), 19 deletions(-) diff --git a/kernel/constr.ml b/kernel/constr.ml index e2b1d3fd9c..043663f531 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -732,12 +732,10 @@ let hasheq t1 t2 = n1 == n2 && b1 == b2 && t1 == t2 && c1 == c2 | App (c1,l1), App (c2,l2) -> c1 == c2 && array_eqeq l1 l2 | Proj (p1,c1), Proj(p2,c2) -> p1 == p2 && c1 == c2 - | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && array_eqeq l1 l2 + | Evar (e1,l1), Evar (e2,l2) -> e1 == e2 && array_eqeq l1 l2 | Const (c1,u1), Const (c2,u2) -> c1 == c2 && u1 == u2 - | Ind ((sp1,i1),u1), Ind ((sp2,i2),u2) -> - sp1 == sp2 && Int.equal i1 i2 && u1 == u2 - | Construct (((sp1,i1),j1),u1), Construct (((sp2,i2),j2),u2) -> - sp1 == sp2 && Int.equal i1 i2 && Int.equal j1 j2 && u1 == u2 + | Ind (ind1,u1), Ind (ind2,u2) -> ind1 == ind2 && u1 == u2 + | Construct (cstr1,u1), Construct (cstr2,u2) -> cstr1 == cstr2 && u1 == u2 | Case (ci1,p1,c1,bl1), Case (ci2,p2,c2,bl2) -> ci1 == ci2 && p1 == p2 && c1 == c2 && array_eqeq bl1 bl2 | Fix ((ln1, i1),(lna1,tl1,bl1)), Fix ((ln2, i2),(lna2,tl2,bl2)) -> @@ -815,19 +813,19 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = | Proj (p,c) -> let c, hc = sh_rec c in let p' = Projection.hcons p in - (Proj (p', c), combinesmall 17 (combine (Projection.hash p') hc)) + (Proj (p', c), combinesmall 17 (combine (Projection.SyntacticOrd.hash p') hc)) | Const (c,u) -> let c' = sh_con c in let u', hu = sh_instance u in - (Const (c', u'), combinesmall 9 (combine (Constant.hash c) hu)) - | Ind ((kn,i) as ind,u) -> + (Const (c', u'), combinesmall 9 (combine (Constant.SyntacticOrd.hash c) hu)) + | Ind (ind,u) -> let u', hu = sh_instance u in (Ind (sh_ind ind, u'), - combinesmall 10 (combine (ind_hash ind) hu)) - | Construct ((((kn,i),j) as c,u))-> + combinesmall 10 (combine (ind_syntactic_hash ind) hu)) + | Construct (c,u) -> let u', hu = sh_instance u in (Construct (sh_construct c, u'), - combinesmall 11 (combine (constructor_hash c) hu)) + combinesmall 11 (combine (constructor_syntactic_hash c) hu)) | Case (ci,p,c,bl) -> let p, hp = sh_rec p and c, hc = sh_rec c in diff --git a/kernel/cooking.ml b/kernel/cooking.ml index be71bd7b41..9849f156c9 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -44,15 +44,15 @@ module RefHash = struct type t = my_global_reference let equal gr1 gr2 = match gr1, gr2 with - | ConstRef c1, ConstRef c2 -> Constant.CanOrd.equal c1 c2 - | IndRef i1, IndRef i2 -> eq_ind i1 i2 - | ConstructRef c1, ConstructRef c2 -> eq_constructor c1 c2 + | ConstRef c1, ConstRef c2 -> Constant.SyntacticOrd.equal c1 c2 + | IndRef i1, IndRef i2 -> eq_syntactic_ind i1 i2 + | ConstructRef c1, ConstructRef c2 -> eq_syntactic_constructor c1 c2 | _ -> false open Hashset.Combine let hash = function - | ConstRef c -> combinesmall 1 (Constant.hash c) - | IndRef i -> combinesmall 2 (ind_hash i) - | ConstructRef c -> combinesmall 3 (constructor_hash c) + | ConstRef c -> combinesmall 1 (Constant.SyntacticOrd.hash c) + | IndRef i -> combinesmall 2 (ind_syntactic_hash i) + | ConstructRef c -> combinesmall 3 (constructor_syntactic_hash c) end module RefTable = Hashtbl.Make(RefHash) diff --git a/kernel/names.ml b/kernel/names.ml index ae2b3b6389..bc33932086 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -477,7 +477,7 @@ module KerPair = struct | Dual (kn,_) -> kn let same kn = Same kn - let make knu knc = if knu == knc then Same knc else Dual (knu,knc) + let make knu knc = if KerName.equal knu knc then Same knc else Dual (knu,knc) let make1 = same let make2 mp l = same (KerName.make2 mp l) @@ -524,6 +524,23 @@ module KerPair = struct let hash x = KerName.hash (canonical x) end + module SyntacticOrd = struct + type t = kernel_pair + let compare x y = match x, y with + | Same knx, Same kny -> KerName.compare knx kny + | Dual (knux,kncx), Dual (knuy,kncy) -> + let c = KerName.compare knux knuy in + if not (Int.equal c 0) then c + else KerName.compare kncx kncy + | Same _, _ -> -1 + | Dual _, _ -> 1 + let equal x y = x == y || compare x y = 0 + let hash = function + | Same kn -> KerName.hash kn + | Dual (knu, knc) -> + Hashset.Combine.combine (KerName.hash knu) (KerName.hash knc) + end + (** Default (logical) comparison and hash is on the canonical part *) let equal = CanOrd.equal let hash = CanOrd.hash @@ -590,6 +607,8 @@ let index_of_constructor (ind, i) = i let eq_ind (m1, i1) (m2, i2) = Int.equal i1 i2 && MutInd.equal m1 m2 let eq_user_ind (m1, i1) (m2, i2) = Int.equal i1 i2 && MutInd.UserOrd.equal m1 m2 +let eq_syntactic_ind (m1, i1) (m2, i2) = + Int.equal i1 i2 && MutInd.SyntacticOrd.equal m1 m2 let ind_ord (m1, i1) (m2, i2) = let c = Int.compare i1 i2 in @@ -597,15 +616,22 @@ let ind_ord (m1, i1) (m2, i2) = let ind_user_ord (m1, i1) (m2, i2) = let c = Int.compare i1 i2 in if Int.equal c 0 then MutInd.UserOrd.compare m1 m2 else c +let ind_syntactic_ord (m1, i1) (m2, i2) = + let c = Int.compare i1 i2 in + if Int.equal c 0 then MutInd.SyntacticOrd.compare m1 m2 else c let ind_hash (m, i) = Hashset.Combine.combine (MutInd.hash m) (Int.hash i) let ind_user_hash (m, i) = Hashset.Combine.combine (MutInd.UserOrd.hash m) (Int.hash i) +let ind_syntactic_hash (m, i) = + Hashset.Combine.combine (MutInd.SyntacticOrd.hash m) (Int.hash i) let eq_constructor (ind1, j1) (ind2, j2) = Int.equal j1 j2 && eq_ind ind1 ind2 let eq_user_constructor (ind1, j1) (ind2, j2) = Int.equal j1 j2 && eq_user_ind ind1 ind2 +let eq_syntactic_constructor (ind1, j1) (ind2, j2) = + Int.equal j1 j2 && eq_syntactic_ind ind1 ind2 let constructor_ord (ind1, j1) (ind2, j2) = let c = Int.compare j1 j2 in @@ -613,11 +639,16 @@ let constructor_ord (ind1, j1) (ind2, j2) = let constructor_user_ord (ind1, j1) (ind2, j2) = let c = Int.compare j1 j2 in if Int.equal c 0 then ind_user_ord ind1 ind2 else c +let constructor_syntactic_ord (ind1, j1) (ind2, j2) = + let c = Int.compare j1 j2 in + if Int.equal c 0 then ind_syntactic_ord ind1 ind2 else c let constructor_hash (ind, i) = Hashset.Combine.combine (ind_hash ind) (Int.hash i) let constructor_user_hash (ind, i) = Hashset.Combine.combine (ind_user_hash ind) (Int.hash i) +let constructor_syntactic_hash (ind, i) = + Hashset.Combine.combine (ind_syntactic_hash ind) (Int.hash i) module InductiveOrdered = struct type t = inductive @@ -805,6 +836,15 @@ struct let hash (c, b) = (if b then 0 else 1) + Constant.hash c + module SyntacticOrd = struct + type t = constant * bool + let compare (c, b) (c', b') = + if b = b' then Constant.SyntacticOrd.compare c c' else -1 + let equal (c, b as x) (c', b' as x') = + x == x' || b = b' && Constant.SyntacticOrd.equal c c' + let hash (c, b) = (if b then 0 else 1) + Constant.SyntacticOrd.hash c + end + module Self_Hashcons = struct type _t = t diff --git a/kernel/names.mli b/kernel/names.mli index 7cc4443752..9a8977c92f 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -305,6 +305,12 @@ sig val hash : t -> int end + module SyntacticOrd : sig + val compare : t -> t -> int + val equal : t -> t -> bool + val hash : t -> int + end + val equal : t -> t -> bool (** Default comparison, alias for [CanOrd.equal] *) @@ -379,6 +385,12 @@ sig val hash : t -> int end + module SyntacticOrd : sig + val compare : t -> t -> int + val equal : t -> t -> bool + val hash : t -> int + end + val equal : t -> t -> bool (** Default comparison, alias for [CanOrd.equal] *) @@ -417,16 +429,22 @@ val inductive_of_constructor : constructor -> inductive val index_of_constructor : constructor -> int val eq_ind : inductive -> inductive -> bool val eq_user_ind : inductive -> inductive -> bool +val eq_syntactic_ind : inductive -> inductive -> bool val ind_ord : inductive -> inductive -> int val ind_hash : inductive -> int val ind_user_ord : inductive -> inductive -> int val ind_user_hash : inductive -> int +val ind_syntactic_ord : inductive -> inductive -> int +val ind_syntactic_hash : inductive -> int val eq_constructor : constructor -> constructor -> bool val eq_user_constructor : constructor -> constructor -> bool +val eq_syntactic_constructor : constructor -> constructor -> bool val constructor_ord : constructor -> constructor -> int -val constructor_user_ord : constructor -> constructor -> int val constructor_hash : constructor -> int +val constructor_user_ord : constructor -> constructor -> int val constructor_user_hash : constructor -> int +val constructor_syntactic_ord : constructor -> constructor -> int +val constructor_syntactic_hash : constructor -> int (** Better to have it here that in Closure, since required in grammar.cma *) type evaluable_global_reference = @@ -640,6 +658,12 @@ module Projection : sig val make : constant -> bool -> t + module SyntacticOrd : sig + val compare : t -> t -> int + val equal : t -> t -> bool + val hash : t -> int + end + val constant : t -> constant val unfolded : t -> bool val unfold : t -> t -- cgit v1.2.3 From 979de570714d340aaab7a6e99e08d46aa616e7da Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 2 Aug 2015 14:45:24 +0200 Subject: A patch renaming equal into eq in the module dealing with hash-consing, so as to avoid having too many kinds of equalities with same name. --- kernel/constr.ml | 8 ++++---- kernel/names.ml | 16 ++++++++-------- kernel/sorts.ml | 2 +- kernel/univ.ml | 22 +++++++++++----------- lib/cSet.ml | 2 +- lib/hashcons.ml | 12 ++++++------ lib/hashcons.mli | 12 ++++++------ lib/hashset.ml | 4 ++-- lib/hashset.mli | 2 +- 9 files changed, 40 insertions(+), 40 deletions(-) diff --git a/kernel/constr.ml b/kernel/constr.ml index 043663f531..644f866b35 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -755,10 +755,10 @@ let hasheq t1 t2 = once and for all the table we'll use for hash-consing all constr *) module HashsetTerm = - Hashset.Make(struct type t = constr let equal = hasheq end) + Hashset.Make(struct type t = constr let eq = hasheq end) module HashsetTermArray = - Hashset.Make(struct type t = constr array let equal = array_eqeq end) + Hashset.Make(struct type t = constr array let eq = array_eqeq end) let term_table = HashsetTerm.create 19991 (* The associative table to hashcons terms. *) @@ -928,7 +928,7 @@ struct List.equal (==) info1.ind_tags info2.ind_tags && Array.equal (List.equal (==)) info1.cstr_tags info2.cstr_tags && info1.style == info2.style - let equal ci ci' = + let eq ci ci' = ci.ci_ind == ci'.ci_ind && Int.equal ci.ci_npar ci'.ci_npar && Array.equal Int.equal ci.ci_cstr_ndecls ci'.ci_cstr_ndecls && (* we use [Array.equal] on purpose *) @@ -970,7 +970,7 @@ module Hsorts = let hashcons huniv = function Prop c -> Prop c | Type u -> Type (huniv u) - let equal s1 s2 = + let eq s1 s2 = s1 == s2 || match (s1,s2) with (Prop c1, Prop c2) -> c1 == c2 diff --git a/kernel/names.ml b/kernel/names.ml index bc33932086..a99702d159 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -102,7 +102,7 @@ struct let hashcons hident = function | Name id -> Name (hident id) | n -> n - let equal n1 n2 = + let eq n1 n2 = n1 == n2 || match (n1,n2) with | (Name id1, Name id2) -> id1 == id2 @@ -236,7 +236,7 @@ struct type t = _t type u = (Id.t -> Id.t) * (DirPath.t -> DirPath.t) let hashcons (hid,hdir) (n,s,dir) = (n,hid s,hdir dir) - let equal ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) = + let eq ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) = (x == y) || (Int.equal n1 n2 && s1 == s2 && dir1 == dir2) let hash = hash @@ -327,7 +327,7 @@ module ModPath = struct | MPfile dir -> MPfile (hdir dir) | MPbound m -> MPbound (huniqid m) | MPdot (md,l) -> MPdot (hashcons hfuns md, hstr l) - let rec equal d1 d2 = + let rec eq d1 d2 = d1 == d2 || match d1,d2 with | MPfile dir1, MPfile dir2 -> dir1 == dir2 @@ -423,7 +423,7 @@ module KerName = struct let hashcons (hmod,hdir,hstr) kn = let { modpath = mp; dirpath = dp; knlabel = l; refhash; } = kn in { modpath = hmod mp; dirpath = hdir dp; knlabel = hstr l; refhash; canary; } - let equal kn1 kn2 = + let eq kn1 kn2 = kn1.modpath == kn2.modpath && kn1.dirpath == kn2.dirpath && kn1.knlabel == kn2.knlabel let hash = hash @@ -552,7 +552,7 @@ module KerPair = struct let hashcons hkn = function | Same kn -> Same (hkn kn) | Dual (knu,knc) -> make (hkn knu) (hkn knc) - let equal x y = (* physical comparison on subterms *) + let eq x y = (* physical comparison on subterms *) x == y || match x,y with | Same x, Same y -> x == y @@ -693,7 +693,7 @@ module Hind = Hashcons.Make( type t = inductive type u = MutInd.t -> MutInd.t let hashcons hmind (mind, i) = (hmind mind, i) - let equal (mind1,i1) (mind2,i2) = mind1 == mind2 && Int.equal i1 i2 + let eq (mind1,i1) (mind2,i2) = mind1 == mind2 && Int.equal i1 i2 let hash = ind_hash end) @@ -702,7 +702,7 @@ module Hconstruct = Hashcons.Make( type t = constructor type u = inductive -> inductive let hashcons hind (ind, j) = (hind ind, j) - let equal (ind1, j1) (ind2, j2) = ind1 == ind2 && Int.equal j1 j2 + let eq (ind1, j1) (ind2, j2) = ind1 == ind2 && Int.equal j1 j2 let hash = constructor_hash end) @@ -851,7 +851,7 @@ struct type t = _t type u = Constant.t -> Constant.t let hashcons hc (c,b) = (hc c,b) - let equal ((c,b) as x) ((c',b') as y) = + let eq ((c,b) as x) ((c',b') as y) = x == y || (c == c' && b == b') let hash = hash end diff --git a/kernel/sorts.ml b/kernel/sorts.ml index e2854abfd3..2baf9b1335 100644 --- a/kernel/sorts.ml +++ b/kernel/sorts.ml @@ -98,7 +98,7 @@ module Hsorts = let u' = huniv u in if u' == u then c else Type u' | s -> s - let equal s1 s2 = match (s1,s2) with + let eq s1 s2 = match (s1,s2) with | (Prop c1, Prop c2) -> c1 == c2 | (Type u1, Type u2) -> u1 == u2 |_ -> false diff --git a/kernel/univ.ml b/kernel/univ.ml index 336cdb653e..09a64d1b09 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -35,7 +35,7 @@ module type Hashconsed = sig type t val hash : t -> int - val equal : t -> t -> bool + val eq : t -> t -> bool val hcons : t -> t end @@ -53,7 +53,7 @@ struct type t = _t type u = (M.t -> M.t) let hash = function Nil -> 0 | Cons (_, h, _) -> h - let equal l1 l2 = match l1, l2 with + let eq l1 l2 = match l1, l2 with | Nil, Nil -> true | Cons (x1, _, l1), Cons (x2, _, l2) -> x1 == x2 && l1 == l2 | _ -> false @@ -135,12 +135,12 @@ module HList = struct let rec remove x = function | Nil -> nil | Cons (y, _, l) -> - if H.equal x y then l + if H.eq x y then l else cons y (remove x l) let rec mem x = function | Nil -> false - | Cons (y, _, l) -> H.equal x y || mem x l + | Cons (y, _, l) -> H.eq x y || mem x l let rec compare cmp l1 l2 = match l1, l2 with | Nil, Nil -> 0 @@ -251,7 +251,7 @@ module Level = struct type _t = t type t = _t type u = unit - let equal x y = x.hash == y.hash && RawLevel.hequal x.data y.data + let eq x y = x.hash == y.hash && RawLevel.hequal x.data y.data let hash x = x.hash let hashcons () x = let data' = RawLevel.hcons x.data in @@ -398,7 +398,7 @@ struct let hashcons hdir (b,n as x) = let b' = hdir b in if b' == b then x else (b',n) - let equal l1 l2 = + let eq l1 l2 = l1 == l2 || match l1,l2 with | (b,n), (b',n') -> b == b' && n == n' @@ -417,7 +417,7 @@ struct let hcons = Hashcons.simple_hcons H.generate H.hcons Level.hcons let hash = ExprHash.hash - let equal x y = x == y || + let eq x y = x == y || (let (u,n) = x and (v,n') = y in Int.equal n n' && Level.equal u v) @@ -1293,7 +1293,7 @@ module Hconstraint = type t = univ_constraint type u = universe_level -> universe_level let hashcons hul (l1,k,l2) = (hul l1, k, hul l2) - let equal (l1,k,l2) (l1',k',l2') = + let eq (l1,k,l2) (l1',k',l2') = l1 == l1' && k == k' && l2 == l2' let hash = Hashtbl.hash end) @@ -1305,7 +1305,7 @@ module Hconstraints = type u = univ_constraint -> univ_constraint let hashcons huc s = Constraint.fold (fun x -> Constraint.add (huc x)) s Constraint.empty - let equal s s' = + let eq s s' = List.for_all2eq (==) (Constraint.elements s) (Constraint.elements s') @@ -1676,7 +1676,7 @@ struct a end - let equal t1 t2 = + let eq t1 t2 = t1 == t2 || (Int.equal (Array.length t1) (Array.length t2) && let rec aux i = @@ -2043,7 +2043,7 @@ module Huniverse_set = type u = universe_level -> universe_level let hashcons huc s = LSet.fold (fun x -> LSet.add (huc x)) s LSet.empty - let equal s s' = + let eq s s' = LSet.equal s s' let hash = Hashtbl.hash end) diff --git a/lib/cSet.ml b/lib/cSet.ml index d7d5c70b39..783165630e 100644 --- a/lib/cSet.ml +++ b/lib/cSet.ml @@ -57,7 +57,7 @@ struct open Hashset.Combine type t = set type u = M.t -> M.t - let equal s1 s2 = s1 == s2 || eqeq (spine s1 []) (spine s2 []) + let eq s1 s2 = s1 == s2 || eqeq (spine s1 []) (spine s2 []) let hash s = Set.fold (fun v accu -> combine (H.hash v) accu) s 0 let hashcons = umap end diff --git a/lib/hashcons.ml b/lib/hashcons.ml index 46ba0b6285..d368e20e6d 100644 --- a/lib/hashcons.ml +++ b/lib/hashcons.ml @@ -15,7 +15,7 @@ * of objects of type t (u usually has the form (t1->t1)*(t2->t2)*...). * [hashcons u x] is a function that hash-cons the sub-structures of x using * the hash-consing functions u provides. - * [equal] is a comparison function. It is allowed to use physical equality + * [eq] is a comparison function. It is allowed to use physical equality * on the sub-terms hash-consed by the hashcons function. * [hash] is the hash function given to the Hashtbl.Make function * @@ -27,7 +27,7 @@ module type HashconsedType = type t type u val hashcons : u -> t -> t - val equal : t -> t -> bool + val eq : t -> t -> bool val hash : t -> int end @@ -53,7 +53,7 @@ module Make (X : HashconsedType) : (S with type t = X.t and type u = X.u) = (* We create the type of hashtables for t, with our comparison fun. * An invariant is that the table never contains two entries equals - * w.r.t (=), although the equality on keys is X.equal. This is + * w.r.t (=), although the equality on keys is X.eq. This is * granted since we hcons the subterms before looking up in the table. *) module Htbl = Hashset.Make(X) @@ -124,7 +124,7 @@ module Hlist (D:HashedType) = let hashcons (hrec,hdata) = function | x :: l -> hdata x :: hrec l | l -> l - let equal l1 l2 = + let eq l1 l2 = l1 == l2 || match l1, l2 with | [], [] -> true @@ -144,7 +144,7 @@ module Hstring = Make( type t = string type u = unit let hashcons () s =(* incr accesstr;*) s - external equal : string -> string -> bool = "caml_string_equal" "noalloc" + external eq : string -> string -> bool = "caml_string_equal" "noalloc" (** Copy from CString *) let rec hash len s i accu = if i = len then accu @@ -191,7 +191,7 @@ module Hobj = Make( type t = Obj.t type u = (Obj.t -> Obj.t) * unit let hashcons (hrec,_) = hash_obj hrec - let equal = comp_obj + let eq = comp_obj let hash = Hashtbl.hash end) diff --git a/lib/hashcons.mli b/lib/hashcons.mli index 8d0adc3fd6..93890c494b 100644 --- a/lib/hashcons.mli +++ b/lib/hashcons.mli @@ -14,9 +14,9 @@ module type HashconsedType = sig (** {6 Generic hashconsing signature} - Given an equivalence relation [equal], a hashconsing function is a + Given an equivalence relation [eq], a hashconsing function is a function that associates the same canonical element to two elements - related by [equal]. Usually, the element chosen is canonical w.r.t. + related by [eq]. Usually, the element chosen is canonical w.r.t. physical equality [(==)], so as to reduce memory consumption and enhance efficiency of equality tests. @@ -32,15 +32,15 @@ module type HashconsedType = Usually a tuple of functions. *) val hashcons : u -> t -> t (** The actual hashconsing function, using its fist argument to recursively - hashcons substructures. It should be compatible with [equal], that is - [equal x (hashcons f x) = true]. *) - val equal : t -> t -> bool + hashcons substructures. It should be compatible with [eq], that is + [eq x (hashcons f x) = true]. *) + val eq : t -> t -> bool (** A comparison function. It is allowed to use physical equality on the sub-terms hashconsed by the [hashcons] function, but it should be insensible to shallow copy of the compared object. *) val hash : t -> int (** A hash function passed to the underlying hashtable structure. [hash] - should be compatible with [equal], i.e. if [equal x y = true] then + should be compatible with [eq], i.e. if [eq x y = true] then [hash x = hash y]. *) end diff --git a/lib/hashset.ml b/lib/hashset.ml index 1ca6cc6418..9454aef9bb 100644 --- a/lib/hashset.ml +++ b/lib/hashset.ml @@ -16,7 +16,7 @@ module type EqType = sig type t - val equal : t -> t -> bool + val eq : t -> t -> bool end type statistics = { @@ -183,7 +183,7 @@ module Make (E : EqType) = if i >= sz then ifnotfound index else if h = hashes.(i) then begin match Weak.get bucket i with - | Some v when E.equal v d -> v + | Some v when E.eq v d -> v | _ -> loop (i + 1) end else loop (i + 1) in diff --git a/lib/hashset.mli b/lib/hashset.mli index a455eec662..270484d8a6 100644 --- a/lib/hashset.mli +++ b/lib/hashset.mli @@ -16,7 +16,7 @@ module type EqType = sig type t - val equal : t -> t -> bool + val eq : t -> t -> bool end type statistics = { -- cgit v1.2.3 From b78d86d50727af61e0c4417cf2ef12cbfc73239d Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 23 Jun 2015 16:59:01 +0200 Subject: Adding a notation { x & P } for { x : _ & P }. --- theories/Init/Notations.v | 3 +++ theories/Init/Specif.v | 2 ++ 2 files changed, 5 insertions(+) diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index a7bdba90aa..07d7f91506 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -69,6 +69,9 @@ Reserved Notation "{ x }" (at level 0, x at level 99). Reserved Notation "{ x | P }" (at level 0, x at level 99). Reserved Notation "{ x | P & Q }" (at level 0, x at level 99). +Reserved Notation "{ x & P }" (at level 0, x at level 99). +Reserved Notation "{ x & P & Q }" (at level 0, x at level 99). + Reserved Notation "{ x : A | P }" (at level 0, x at level 99). Reserved Notation "{ x : A | P & Q }" (at level 0, x at level 99). diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 1384901b70..ecdbef7f61 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -48,6 +48,8 @@ Notation "{ x | P & Q }" := (sig2 (fun x => P) (fun x => Q)) : type_scope. Notation "{ x : A | P }" := (sig (A:=A) (fun x => P)) : type_scope. Notation "{ x : A | P & Q }" := (sig2 (A:=A) (fun x => P) (fun x => Q)) : type_scope. +Notation "{ x & P }" := (sigT (fun x => P)) : type_scope. +Notation "{ x & P & Q }" := (sigT2 (fun x => P) (fun x => Q)) : type_scope. Notation "{ x : A & P }" := (sigT (A:=A) (fun x => P)) : type_scope. Notation "{ x : A & P & Q }" := (sigT2 (A:=A) (fun x => P) (fun x => Q)) : type_scope. -- cgit v1.2.3 From 21525bae8801d98ff2f1b52217d7603505ada2d2 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 3 Jul 2015 21:13:05 +0200 Subject: Cosmetic in evarconv.ml: naming a local function for better readibility. --- pretyping/evarconv.ml | 35 ++++++++++++++++++----------------- 1 file changed, 18 insertions(+), 17 deletions(-) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index bb07bf0563..4fed09d6f4 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -425,8 +425,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) (Stack.zip apprF) tM else quick_fail i) ev lF tM i - and consume (termF,skF as apprF) (termM,skM as apprM) i = + and consume (termF,skF as apprF) (termM,skM as apprM) i = if not (Stack.is_empty skF && Stack.is_empty skM) then + (* This tries first-order matching *) consume_stack on_left apprF apprM i else quick_fail i and delta i = @@ -469,28 +470,28 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | Construct u -> eta_constructor ts env evd skR u skF termF | _ -> UnifFailure (evd,NotSameHead) in + let postpone tR lF evd = + (* Postpone the use of an heuristic *) + if not (occur_rigidly (fst ev) evd tR) then + let evd,tF = + if isRel tR || isVar tR then + (* Optimization so as to generate candidates *) + let evd,ev = evar_absorb_arguments env evd ev lF in + evd,mkEvar ev + else + evd,Stack.zip apprF in + switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) evd)) + tF tR + else + UnifFailure (evd,OccurCheck (fst ev,tR)) + in match Stack.list_of_app_stack skF with | None -> ise_try evd [consume_stack on_left apprF apprR; eta] | Some lF -> let tR = Stack.zip apprR in miller_pfenning on_left - (fun () -> - ise_try evd - [eta;(* Postpone the use of an heuristic *) - (fun i -> - if not (occur_rigidly (fst ev) i tR) then - let i,tF = - if isRel tR || isVar tR then - (* Optimization so as to generate candidates *) - let i,ev = evar_absorb_arguments env i ev lF in - i,mkEvar ev - else - i,Stack.zip apprF in - switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) - tF tR - else - UnifFailure (evd,OccurCheck (fst ev,tR)))]) + (fun () -> ise_try evd [eta;postpone tR lF]) ev lF tR evd in let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in -- cgit v1.2.3 From 342fed039e53f00ff8758513149f8d41fa3a2e99 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 3 Jul 2015 21:14:09 +0200 Subject: Evarconv.ml: small cut-elimination, saving useless zip. --- pretyping/evarconv.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 4fed09d6f4..3f4411c058 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -417,7 +417,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let not_only_app = Stack.not_purely_applicative skM in let f1 i = match Stack.list_of_app_stack skF with - | None -> default_fail evd + | None -> quick_fail evd | Some lF -> let tM = Stack.zip apprM in miller_pfenning on_left -- cgit v1.2.3 From 6737055d165c91904fc04534bee6b9c05c0235b1 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 30 Mar 2015 15:35:04 +0200 Subject: Cosmetic changes in evarconv.ml: hopefully using better self-documenting names. --- pretyping/evarconv.ml | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 3f4411c058..3b51cb1feb 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -380,12 +380,14 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty in let consume_stack on_left (termF,skF) (termO,skO) evd = let switch f a b = if on_left then f a b else f b a in - let not_only_app = Stack.not_purely_applicative skO in - match switch (ise_stack2 not_only_app env evd (evar_conv_x ts)) skF skO with - |Some (l,r), Success i' when on_left && (not_only_app || List.is_empty l) -> - switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,l)) (Stack.zip(termO,r)) - |Some (r,l), Success i' when not on_left && (not_only_app || List.is_empty l) -> - switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,l)) (Stack.zip(termO,r)) + let not_only_appO = Stack.not_purely_applicative skO in + match switch (ise_stack2 not_only_appO env evd (evar_conv_x ts)) skF skO with + |Some (lF,rO), Success i' when on_left && (not_only_appO || List.is_empty lF) -> + (* Case (?termF,stk) = (termO,u1..un::stk') with stk,stk' w/o app *) + (* or (?termF,stk) = (termO,u1..un::stk') with stk,stk' w/o app *) + switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,lF)) (Stack.zip(termO,rO)) + |Some (rO,lF), Success i' when not on_left && (not_only_appO || List.is_empty lF) -> + switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,lF)) (Stack.zip(termO,rO)) |None, Success i' -> switch (evar_conv_x ts env i' pbty) termF termO |_, (UnifFailure _ as x) -> x |Some _, _ -> UnifFailure (evd,NotSameArgSize) in -- cgit v1.2.3 From d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 30 Mar 2015 15:41:46 +0200 Subject: Cosmetic changes in evarconv.ml: hopefully more regular form and naming of arguments of eta. --- pretyping/evarconv.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 3b51cb1feb..d3e18953a5 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -391,15 +391,15 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty |None, Success i' -> switch (evar_conv_x ts env i' pbty) termF termO |_, (UnifFailure _ as x) -> x |Some _, _ -> UnifFailure (evd,NotSameArgSize) in - let eta env evd onleft sk term sk' term' = - assert (match sk with [] -> true | _ -> false); - let (na,c1,c'1) = destLambda term in + let eta env evd onleft (termR,skR) (termO,skO) = + assert (match skR with [] -> true | _ -> false); + let (na,c1,c'1) = destLambda termR in let c = nf_evar evd c1 in let env' = push_rel (na,None,c) env in let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env' evd Cst_stack.empty (c'1, Stack.empty) in let out2 = whd_nored_state evd - (Stack.zip (term', sk' @ [Stack.Shift 1]), Stack.append_app [|mkRel 1|] Stack.empty), + (Stack.zip (termO, skO @ [Stack.Shift 1]), Stack.append_app [|mkRel 1|] Stack.empty), Cst_stack.empty in if onleft then evar_eqappr_x ts env' evd CONV out1 out2 else evar_eqappr_x ts env' evd CONV out2 out1 @@ -468,7 +468,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let switch f a b = if on_left then f a b else f b a in let eta evd = match kind_of_term termR with - | Lambda _ -> eta env evd false skR termR skF termF + | Lambda _ -> eta env evd false apprR apprF | Construct u -> eta_constructor ts env evd skR u skF termF | _ -> UnifFailure (evd,NotSameHead) in @@ -712,10 +712,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (* Eta-expansion *) | Rigid, _ when isLambda term1 -> - eta env evd true sk1 term1 sk2 term2 + eta env evd true appr1 appr2 | _, Rigid when isLambda term2 -> - eta env evd false sk2 term2 sk1 term1 + eta env evd false appr2 appr1 | Rigid, Rigid -> begin match kind_of_term term1, kind_of_term term2 with -- cgit v1.2.3 From fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 30 Mar 2015 15:43:56 +0200 Subject: Cosmetic changes in evarconv.ml: hopefully more regular names and form of arguments of eta_constructor. --- pretyping/evarconv.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index d3e18953a5..b73ff2bc5d 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -469,7 +469,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let eta evd = match kind_of_term termR with | Lambda _ -> eta env evd false apprR apprF - | Construct u -> eta_constructor ts env evd skR u skF termF + | Construct u -> eta_constructor ts env evd (u,skR) apprF | _ -> UnifFailure (evd,NotSameHead) in let postpone tR lF evd = @@ -755,10 +755,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty rigids env evd sk1 term1 sk2 term2 | Construct u, _ -> - eta_constructor ts env evd sk1 u sk2 term2 + eta_constructor ts env evd (u,sk1) appr2 | _, Construct u -> - eta_constructor ts env evd sk2 u sk1 term1 + eta_constructor ts env evd (u,sk2) appr1 | Fix ((li1, i1),(_,tys1,bds1 as recdef1)), Fix ((li2, i2),(_,tys2,bds2)) -> (* Partially applied fixs *) if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then @@ -854,7 +854,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) (fst (decompose_app_vect (substl ks h))))] else UnifFailure(evd,(*dummy*)NotSameHead) -and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = +and eta_constructor ts env evd (((ind, i), u),sk1) (term2,sk2) = let mib = lookup_mind (fst ind) env in match mib.Declarations.mind_record with | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> -- cgit v1.2.3 From 27fb880ab6924ec20ce44aeaeb8d89592c1b91cd Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 3 Jul 2015 21:25:15 +0200 Subject: Failing when reaching end of file with unterminated comment when parsing Make (project) file. --- ide/project_file.ml4 | 1 + 1 file changed, 1 insertion(+) diff --git a/ide/project_file.ml4 b/ide/project_file.ml4 index f7279f9cfe..152f76cc0e 100644 --- a/ide/project_file.ml4 +++ b/ide/project_file.ml4 @@ -28,6 +28,7 @@ let rec parse_string = parser and parse_string2 = parser | [< ''"' >] -> "" | [< 'c; s >] -> (String.make 1 c)^(parse_string2 s) + | [< >] -> raise Parsing_error and parse_skip_comment = parser | [< ''\n'; s >] -> s | [< 'c; s >] -> parse_skip_comment s -- cgit v1.2.3 From 7532f3243ba585f21a8f594d3dc788e38dfa2cb8 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 3 Jul 2015 21:28:04 +0200 Subject: Hopefully clearer printing of stack when debugging evarconv unification. --- pretyping/reductionops.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index dc70f36ccf..2892de7c45 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -306,7 +306,9 @@ struct | Update t -> str "ZUpdate(" ++ pr_c t ++ str ")" and pr pr_c l = let open Pp in - prlist_with_sep pr_semicolon (fun x -> hov 1 (pr_member pr_c x)) l + str "[" ++ + prlist_with_sep pr_semicolon (fun x -> hov 1 (pr_member pr_c x)) l ++ + str "]" and pr_cst_member pr_c c = let open Pp in -- cgit v1.2.3 From 21e41af41b52914469885f40155702f325d5c786 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 3 Jul 2015 21:28:24 +0200 Subject: Documenting in passing. --- pretyping/reductionops.mli | 3 +++ 1 file changed, 3 insertions(+) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 1df2a73b2e..51df07f286 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -90,6 +90,9 @@ module Stack : sig val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option val not_purely_applicative : 'a t -> bool + + (** @return the arguments in the stack if a purely applicative + stack, None otherwise *) val list_of_app_stack : constr t -> constr list option val assign : 'a t -> int -> 'a -> 'a t -- cgit v1.2.3 From b9c96c601a8366b75ee8b76d3184ee57379e2620 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 2 Aug 2015 18:41:08 +0200 Subject: Fixing pop_rel_context --- kernel/environ.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kernel/environ.ml b/kernel/environ.ml index 30b28177c9..109e3830c2 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -162,7 +162,7 @@ let reset_context = reset_with_named_context empty_named_context_val let pop_rel_context n env = let ctxt = env.env_rel_context in { env with - env_rel_context = List.firstn (List.length ctxt - n) ctxt; + env_rel_context = List.skipn n ctxt; env_nb_rel = env.env_nb_rel - n } let fold_named_context f env ~init = -- cgit v1.2.3 From 164637cc3a4e8895ed4ec420e300bd692d3e7812 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 2 Aug 2015 18:47:08 +0200 Subject: Fixing test apply.v (had wrong option name). --- test-suite/success/apply.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index 24d5cf8a99..074004fa12 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -371,7 +371,7 @@ Qed. Goal True. Fail eapply existT. -Set Trivial Tactic Unification Under Conjunction. +Set Universal Lemma Under Conjunction. eapply existT. Abort. -- cgit v1.2.3 From 707bfd5719b76d131152a258d49740165fbafe03 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 2 Aug 2015 19:11:21 +0200 Subject: Hconsing continued --- checker/univ.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/checker/univ.ml b/checker/univ.ml index 3bcb3bc950..912d20e0d1 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -33,7 +33,7 @@ module type Hashconsed = sig type t val hash : t -> int - val equal : t -> t -> bool + val eq : t -> t -> bool val hcons : t -> t end @@ -51,7 +51,7 @@ struct type t = _t type u = (M.t -> M.t) let hash = function Nil -> 0 | Cons (_, h, _) -> h - let equal l1 l2 = match l1, l2 with + let eq l1 l2 = match l1, l2 with | Nil, Nil -> true | Cons (x1, _, l1), Cons (x2, _, l2) -> x1 == x2 && l1 == l2 | _ -> false @@ -131,7 +131,7 @@ module HList = struct let rec remove x = function | Nil -> nil | Cons (y, _, l) -> - if H.equal x y then l + if H.eq x y then l else cons y (remove x l) end @@ -229,7 +229,7 @@ module Level = struct type _t = t type t = _t type u = unit - let equal x y = x.hash == y.hash && RawLevel.hequal x.data y.data + let eq x y = x.hash == y.hash && RawLevel.hequal x.data y.data let hash x = x.hash let hashcons () x = let data' = RawLevel.hcons x.data in @@ -319,7 +319,7 @@ struct let hashcons hdir (b,n as x) = let b' = hdir b in if b' == b then x else (b',n) - let equal l1 l2 = + let eq l1 l2 = l1 == l2 || match l1,l2 with | (b,n), (b',n') -> b == b' && n == n' @@ -338,7 +338,7 @@ struct let hcons = Hashcons.simple_hcons H.generate H.hcons Level.hcons let hash = ExprHash.hash - let equal x y = x == y || + let eq x y = x == y || (let (u,n) = x and (v,n') = y in Int.equal n n' && Level.equal u v) @@ -1079,7 +1079,7 @@ struct a end - let equal t1 t2 = + let eq t1 t2 = t1 == t2 || (Int.equal (Array.length t1) (Array.length t2) && let rec aux i = -- cgit v1.2.3 From 35ba593b4ecb805b4e69c01c56fb4b93dfafdf0b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 2 Aug 2015 19:31:00 +0200 Subject: Reverting 16 last commits, committed mistakenly using the wrong push command. Sorry so much. Reverted: 707bfd5719b76d131152a258d49740165fbafe03. 164637cc3a4e8895ed4ec420e300bd692d3e7812. b9c96c601a8366b75ee8b76d3184ee57379e2620. 21e41af41b52914469885f40155702f325d5c786. 7532f3243ba585f21a8f594d3dc788e38dfa2cb8. 27fb880ab6924ec20ce44aeaeb8d89592c1b91cd. fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c. d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962. 6737055d165c91904fc04534bee6b9c05c0235b1. 342fed039e53f00ff8758513149f8d41fa3a2e99. 21525bae8801d98ff2f1b52217d7603505ada2d2. b78d86d50727af61e0c4417cf2ef12cbfc73239d. 979de570714d340aaab7a6e99e08d46aa616e7da. f556da10a117396c2c796f6915321b67849f65cd. d8226295e6237a43de33475f798c3c8ac6ac4866. fdab811e58094accc02875c1f83e6476f4598d26. --- checker/univ.ml | 14 ++++----- ide/project_file.ml4 | 1 - kernel/constr.ml | 28 +++++++++--------- kernel/cooking.ml | 12 ++++---- kernel/environ.ml | 2 +- kernel/names.ml | 58 ++++++------------------------------ kernel/names.mli | 26 +---------------- kernel/sorts.ml | 2 +- kernel/univ.ml | 22 +++++++------- lib/cSet.ml | 2 +- lib/hashcons.ml | 12 ++++---- lib/hashcons.mli | 12 ++++---- lib/hashset.ml | 4 +-- lib/hashset.mli | 2 +- pretyping/evarconv.ml | 73 ++++++++++++++++++++++------------------------ pretyping/reductionops.ml | 4 +-- pretyping/reductionops.mli | 3 -- proofs/pfedit.ml | 4 +-- proofs/pfedit.mli | 2 +- tactics/elimschemes.ml | 20 ++++++------- tactics/eqschemes.ml | 18 ++++++------ test-suite/success/apply.v | 2 +- theories/Init/Notations.v | 3 -- theories/Init/Specif.v | 2 -- toplevel/auto_ind_decl.ml | 42 +++++++++++--------------- toplevel/ind_tables.ml | 32 ++++++++++---------- toplevel/ind_tables.mli | 15 ++++++---- 27 files changed, 169 insertions(+), 248 deletions(-) diff --git a/checker/univ.ml b/checker/univ.ml index 912d20e0d1..3bcb3bc950 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -33,7 +33,7 @@ module type Hashconsed = sig type t val hash : t -> int - val eq : t -> t -> bool + val equal : t -> t -> bool val hcons : t -> t end @@ -51,7 +51,7 @@ struct type t = _t type u = (M.t -> M.t) let hash = function Nil -> 0 | Cons (_, h, _) -> h - let eq l1 l2 = match l1, l2 with + let equal l1 l2 = match l1, l2 with | Nil, Nil -> true | Cons (x1, _, l1), Cons (x2, _, l2) -> x1 == x2 && l1 == l2 | _ -> false @@ -131,7 +131,7 @@ module HList = struct let rec remove x = function | Nil -> nil | Cons (y, _, l) -> - if H.eq x y then l + if H.equal x y then l else cons y (remove x l) end @@ -229,7 +229,7 @@ module Level = struct type _t = t type t = _t type u = unit - let eq x y = x.hash == y.hash && RawLevel.hequal x.data y.data + let equal x y = x.hash == y.hash && RawLevel.hequal x.data y.data let hash x = x.hash let hashcons () x = let data' = RawLevel.hcons x.data in @@ -319,7 +319,7 @@ struct let hashcons hdir (b,n as x) = let b' = hdir b in if b' == b then x else (b',n) - let eq l1 l2 = + let equal l1 l2 = l1 == l2 || match l1,l2 with | (b,n), (b',n') -> b == b' && n == n' @@ -338,7 +338,7 @@ struct let hcons = Hashcons.simple_hcons H.generate H.hcons Level.hcons let hash = ExprHash.hash - let eq x y = x == y || + let equal x y = x == y || (let (u,n) = x and (v,n') = y in Int.equal n n' && Level.equal u v) @@ -1079,7 +1079,7 @@ struct a end - let eq t1 t2 = + let equal t1 t2 = t1 == t2 || (Int.equal (Array.length t1) (Array.length t2) && let rec aux i = diff --git a/ide/project_file.ml4 b/ide/project_file.ml4 index 152f76cc0e..f7279f9cfe 100644 --- a/ide/project_file.ml4 +++ b/ide/project_file.ml4 @@ -28,7 +28,6 @@ let rec parse_string = parser and parse_string2 = parser | [< ''"' >] -> "" | [< 'c; s >] -> (String.make 1 c)^(parse_string2 s) - | [< >] -> raise Parsing_error and parse_skip_comment = parser | [< ''\n'; s >] -> s | [< 'c; s >] -> parse_skip_comment s diff --git a/kernel/constr.ml b/kernel/constr.ml index 644f866b35..e2b1d3fd9c 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -732,10 +732,12 @@ let hasheq t1 t2 = n1 == n2 && b1 == b2 && t1 == t2 && c1 == c2 | App (c1,l1), App (c2,l2) -> c1 == c2 && array_eqeq l1 l2 | Proj (p1,c1), Proj(p2,c2) -> p1 == p2 && c1 == c2 - | Evar (e1,l1), Evar (e2,l2) -> e1 == e2 && array_eqeq l1 l2 + | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && array_eqeq l1 l2 | Const (c1,u1), Const (c2,u2) -> c1 == c2 && u1 == u2 - | Ind (ind1,u1), Ind (ind2,u2) -> ind1 == ind2 && u1 == u2 - | Construct (cstr1,u1), Construct (cstr2,u2) -> cstr1 == cstr2 && u1 == u2 + | Ind ((sp1,i1),u1), Ind ((sp2,i2),u2) -> + sp1 == sp2 && Int.equal i1 i2 && u1 == u2 + | Construct (((sp1,i1),j1),u1), Construct (((sp2,i2),j2),u2) -> + sp1 == sp2 && Int.equal i1 i2 && Int.equal j1 j2 && u1 == u2 | Case (ci1,p1,c1,bl1), Case (ci2,p2,c2,bl2) -> ci1 == ci2 && p1 == p2 && c1 == c2 && array_eqeq bl1 bl2 | Fix ((ln1, i1),(lna1,tl1,bl1)), Fix ((ln2, i2),(lna2,tl2,bl2)) -> @@ -755,10 +757,10 @@ let hasheq t1 t2 = once and for all the table we'll use for hash-consing all constr *) module HashsetTerm = - Hashset.Make(struct type t = constr let eq = hasheq end) + Hashset.Make(struct type t = constr let equal = hasheq end) module HashsetTermArray = - Hashset.Make(struct type t = constr array let eq = array_eqeq end) + Hashset.Make(struct type t = constr array let equal = array_eqeq end) let term_table = HashsetTerm.create 19991 (* The associative table to hashcons terms. *) @@ -813,19 +815,19 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = | Proj (p,c) -> let c, hc = sh_rec c in let p' = Projection.hcons p in - (Proj (p', c), combinesmall 17 (combine (Projection.SyntacticOrd.hash p') hc)) + (Proj (p', c), combinesmall 17 (combine (Projection.hash p') hc)) | Const (c,u) -> let c' = sh_con c in let u', hu = sh_instance u in - (Const (c', u'), combinesmall 9 (combine (Constant.SyntacticOrd.hash c) hu)) - | Ind (ind,u) -> + (Const (c', u'), combinesmall 9 (combine (Constant.hash c) hu)) + | Ind ((kn,i) as ind,u) -> let u', hu = sh_instance u in (Ind (sh_ind ind, u'), - combinesmall 10 (combine (ind_syntactic_hash ind) hu)) - | Construct (c,u) -> + combinesmall 10 (combine (ind_hash ind) hu)) + | Construct ((((kn,i),j) as c,u))-> let u', hu = sh_instance u in (Construct (sh_construct c, u'), - combinesmall 11 (combine (constructor_syntactic_hash c) hu)) + combinesmall 11 (combine (constructor_hash c) hu)) | Case (ci,p,c,bl) -> let p, hp = sh_rec p and c, hc = sh_rec c in @@ -928,7 +930,7 @@ struct List.equal (==) info1.ind_tags info2.ind_tags && Array.equal (List.equal (==)) info1.cstr_tags info2.cstr_tags && info1.style == info2.style - let eq ci ci' = + let equal ci ci' = ci.ci_ind == ci'.ci_ind && Int.equal ci.ci_npar ci'.ci_npar && Array.equal Int.equal ci.ci_cstr_ndecls ci'.ci_cstr_ndecls && (* we use [Array.equal] on purpose *) @@ -970,7 +972,7 @@ module Hsorts = let hashcons huniv = function Prop c -> Prop c | Type u -> Type (huniv u) - let eq s1 s2 = + let equal s1 s2 = s1 == s2 || match (s1,s2) with (Prop c1, Prop c2) -> c1 == c2 diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 9849f156c9..be71bd7b41 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -44,15 +44,15 @@ module RefHash = struct type t = my_global_reference let equal gr1 gr2 = match gr1, gr2 with - | ConstRef c1, ConstRef c2 -> Constant.SyntacticOrd.equal c1 c2 - | IndRef i1, IndRef i2 -> eq_syntactic_ind i1 i2 - | ConstructRef c1, ConstructRef c2 -> eq_syntactic_constructor c1 c2 + | ConstRef c1, ConstRef c2 -> Constant.CanOrd.equal c1 c2 + | IndRef i1, IndRef i2 -> eq_ind i1 i2 + | ConstructRef c1, ConstructRef c2 -> eq_constructor c1 c2 | _ -> false open Hashset.Combine let hash = function - | ConstRef c -> combinesmall 1 (Constant.SyntacticOrd.hash c) - | IndRef i -> combinesmall 2 (ind_syntactic_hash i) - | ConstructRef c -> combinesmall 3 (constructor_syntactic_hash c) + | ConstRef c -> combinesmall 1 (Constant.hash c) + | IndRef i -> combinesmall 2 (ind_hash i) + | ConstructRef c -> combinesmall 3 (constructor_hash c) end module RefTable = Hashtbl.Make(RefHash) diff --git a/kernel/environ.ml b/kernel/environ.ml index 109e3830c2..30b28177c9 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -162,7 +162,7 @@ let reset_context = reset_with_named_context empty_named_context_val let pop_rel_context n env = let ctxt = env.env_rel_context in { env with - env_rel_context = List.skipn n ctxt; + env_rel_context = List.firstn (List.length ctxt - n) ctxt; env_nb_rel = env.env_nb_rel - n } let fold_named_context f env ~init = diff --git a/kernel/names.ml b/kernel/names.ml index a99702d159..ae2b3b6389 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -102,7 +102,7 @@ struct let hashcons hident = function | Name id -> Name (hident id) | n -> n - let eq n1 n2 = + let equal n1 n2 = n1 == n2 || match (n1,n2) with | (Name id1, Name id2) -> id1 == id2 @@ -236,7 +236,7 @@ struct type t = _t type u = (Id.t -> Id.t) * (DirPath.t -> DirPath.t) let hashcons (hid,hdir) (n,s,dir) = (n,hid s,hdir dir) - let eq ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) = + let equal ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) = (x == y) || (Int.equal n1 n2 && s1 == s2 && dir1 == dir2) let hash = hash @@ -327,7 +327,7 @@ module ModPath = struct | MPfile dir -> MPfile (hdir dir) | MPbound m -> MPbound (huniqid m) | MPdot (md,l) -> MPdot (hashcons hfuns md, hstr l) - let rec eq d1 d2 = + let rec equal d1 d2 = d1 == d2 || match d1,d2 with | MPfile dir1, MPfile dir2 -> dir1 == dir2 @@ -423,7 +423,7 @@ module KerName = struct let hashcons (hmod,hdir,hstr) kn = let { modpath = mp; dirpath = dp; knlabel = l; refhash; } = kn in { modpath = hmod mp; dirpath = hdir dp; knlabel = hstr l; refhash; canary; } - let eq kn1 kn2 = + let equal kn1 kn2 = kn1.modpath == kn2.modpath && kn1.dirpath == kn2.dirpath && kn1.knlabel == kn2.knlabel let hash = hash @@ -477,7 +477,7 @@ module KerPair = struct | Dual (kn,_) -> kn let same kn = Same kn - let make knu knc = if KerName.equal knu knc then Same knc else Dual (knu,knc) + let make knu knc = if knu == knc then Same knc else Dual (knu,knc) let make1 = same let make2 mp l = same (KerName.make2 mp l) @@ -524,23 +524,6 @@ module KerPair = struct let hash x = KerName.hash (canonical x) end - module SyntacticOrd = struct - type t = kernel_pair - let compare x y = match x, y with - | Same knx, Same kny -> KerName.compare knx kny - | Dual (knux,kncx), Dual (knuy,kncy) -> - let c = KerName.compare knux knuy in - if not (Int.equal c 0) then c - else KerName.compare kncx kncy - | Same _, _ -> -1 - | Dual _, _ -> 1 - let equal x y = x == y || compare x y = 0 - let hash = function - | Same kn -> KerName.hash kn - | Dual (knu, knc) -> - Hashset.Combine.combine (KerName.hash knu) (KerName.hash knc) - end - (** Default (logical) comparison and hash is on the canonical part *) let equal = CanOrd.equal let hash = CanOrd.hash @@ -552,7 +535,7 @@ module KerPair = struct let hashcons hkn = function | Same kn -> Same (hkn kn) | Dual (knu,knc) -> make (hkn knu) (hkn knc) - let eq x y = (* physical comparison on subterms *) + let equal x y = (* physical comparison on subterms *) x == y || match x,y with | Same x, Same y -> x == y @@ -607,8 +590,6 @@ let index_of_constructor (ind, i) = i let eq_ind (m1, i1) (m2, i2) = Int.equal i1 i2 && MutInd.equal m1 m2 let eq_user_ind (m1, i1) (m2, i2) = Int.equal i1 i2 && MutInd.UserOrd.equal m1 m2 -let eq_syntactic_ind (m1, i1) (m2, i2) = - Int.equal i1 i2 && MutInd.SyntacticOrd.equal m1 m2 let ind_ord (m1, i1) (m2, i2) = let c = Int.compare i1 i2 in @@ -616,22 +597,15 @@ let ind_ord (m1, i1) (m2, i2) = let ind_user_ord (m1, i1) (m2, i2) = let c = Int.compare i1 i2 in if Int.equal c 0 then MutInd.UserOrd.compare m1 m2 else c -let ind_syntactic_ord (m1, i1) (m2, i2) = - let c = Int.compare i1 i2 in - if Int.equal c 0 then MutInd.SyntacticOrd.compare m1 m2 else c let ind_hash (m, i) = Hashset.Combine.combine (MutInd.hash m) (Int.hash i) let ind_user_hash (m, i) = Hashset.Combine.combine (MutInd.UserOrd.hash m) (Int.hash i) -let ind_syntactic_hash (m, i) = - Hashset.Combine.combine (MutInd.SyntacticOrd.hash m) (Int.hash i) let eq_constructor (ind1, j1) (ind2, j2) = Int.equal j1 j2 && eq_ind ind1 ind2 let eq_user_constructor (ind1, j1) (ind2, j2) = Int.equal j1 j2 && eq_user_ind ind1 ind2 -let eq_syntactic_constructor (ind1, j1) (ind2, j2) = - Int.equal j1 j2 && eq_syntactic_ind ind1 ind2 let constructor_ord (ind1, j1) (ind2, j2) = let c = Int.compare j1 j2 in @@ -639,16 +613,11 @@ let constructor_ord (ind1, j1) (ind2, j2) = let constructor_user_ord (ind1, j1) (ind2, j2) = let c = Int.compare j1 j2 in if Int.equal c 0 then ind_user_ord ind1 ind2 else c -let constructor_syntactic_ord (ind1, j1) (ind2, j2) = - let c = Int.compare j1 j2 in - if Int.equal c 0 then ind_syntactic_ord ind1 ind2 else c let constructor_hash (ind, i) = Hashset.Combine.combine (ind_hash ind) (Int.hash i) let constructor_user_hash (ind, i) = Hashset.Combine.combine (ind_user_hash ind) (Int.hash i) -let constructor_syntactic_hash (ind, i) = - Hashset.Combine.combine (ind_syntactic_hash ind) (Int.hash i) module InductiveOrdered = struct type t = inductive @@ -693,7 +662,7 @@ module Hind = Hashcons.Make( type t = inductive type u = MutInd.t -> MutInd.t let hashcons hmind (mind, i) = (hmind mind, i) - let eq (mind1,i1) (mind2,i2) = mind1 == mind2 && Int.equal i1 i2 + let equal (mind1,i1) (mind2,i2) = mind1 == mind2 && Int.equal i1 i2 let hash = ind_hash end) @@ -702,7 +671,7 @@ module Hconstruct = Hashcons.Make( type t = constructor type u = inductive -> inductive let hashcons hind (ind, j) = (hind ind, j) - let eq (ind1, j1) (ind2, j2) = ind1 == ind2 && Int.equal j1 j2 + let equal (ind1, j1) (ind2, j2) = ind1 == ind2 && Int.equal j1 j2 let hash = constructor_hash end) @@ -836,22 +805,13 @@ struct let hash (c, b) = (if b then 0 else 1) + Constant.hash c - module SyntacticOrd = struct - type t = constant * bool - let compare (c, b) (c', b') = - if b = b' then Constant.SyntacticOrd.compare c c' else -1 - let equal (c, b as x) (c', b' as x') = - x == x' || b = b' && Constant.SyntacticOrd.equal c c' - let hash (c, b) = (if b then 0 else 1) + Constant.SyntacticOrd.hash c - end - module Self_Hashcons = struct type _t = t type t = _t type u = Constant.t -> Constant.t let hashcons hc (c,b) = (hc c,b) - let eq ((c,b) as x) ((c',b') as y) = + let equal ((c,b) as x) ((c',b') as y) = x == y || (c == c' && b == b') let hash = hash end diff --git a/kernel/names.mli b/kernel/names.mli index 9a8977c92f..7cc4443752 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -305,12 +305,6 @@ sig val hash : t -> int end - module SyntacticOrd : sig - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int - end - val equal : t -> t -> bool (** Default comparison, alias for [CanOrd.equal] *) @@ -385,12 +379,6 @@ sig val hash : t -> int end - module SyntacticOrd : sig - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int - end - val equal : t -> t -> bool (** Default comparison, alias for [CanOrd.equal] *) @@ -429,22 +417,16 @@ val inductive_of_constructor : constructor -> inductive val index_of_constructor : constructor -> int val eq_ind : inductive -> inductive -> bool val eq_user_ind : inductive -> inductive -> bool -val eq_syntactic_ind : inductive -> inductive -> bool val ind_ord : inductive -> inductive -> int val ind_hash : inductive -> int val ind_user_ord : inductive -> inductive -> int val ind_user_hash : inductive -> int -val ind_syntactic_ord : inductive -> inductive -> int -val ind_syntactic_hash : inductive -> int val eq_constructor : constructor -> constructor -> bool val eq_user_constructor : constructor -> constructor -> bool -val eq_syntactic_constructor : constructor -> constructor -> bool val constructor_ord : constructor -> constructor -> int -val constructor_hash : constructor -> int val constructor_user_ord : constructor -> constructor -> int +val constructor_hash : constructor -> int val constructor_user_hash : constructor -> int -val constructor_syntactic_ord : constructor -> constructor -> int -val constructor_syntactic_hash : constructor -> int (** Better to have it here that in Closure, since required in grammar.cma *) type evaluable_global_reference = @@ -658,12 +640,6 @@ module Projection : sig val make : constant -> bool -> t - module SyntacticOrd : sig - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int - end - val constant : t -> constant val unfolded : t -> bool val unfold : t -> t diff --git a/kernel/sorts.ml b/kernel/sorts.ml index 2baf9b1335..e2854abfd3 100644 --- a/kernel/sorts.ml +++ b/kernel/sorts.ml @@ -98,7 +98,7 @@ module Hsorts = let u' = huniv u in if u' == u then c else Type u' | s -> s - let eq s1 s2 = match (s1,s2) with + let equal s1 s2 = match (s1,s2) with | (Prop c1, Prop c2) -> c1 == c2 | (Type u1, Type u2) -> u1 == u2 |_ -> false diff --git a/kernel/univ.ml b/kernel/univ.ml index 09a64d1b09..336cdb653e 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -35,7 +35,7 @@ module type Hashconsed = sig type t val hash : t -> int - val eq : t -> t -> bool + val equal : t -> t -> bool val hcons : t -> t end @@ -53,7 +53,7 @@ struct type t = _t type u = (M.t -> M.t) let hash = function Nil -> 0 | Cons (_, h, _) -> h - let eq l1 l2 = match l1, l2 with + let equal l1 l2 = match l1, l2 with | Nil, Nil -> true | Cons (x1, _, l1), Cons (x2, _, l2) -> x1 == x2 && l1 == l2 | _ -> false @@ -135,12 +135,12 @@ module HList = struct let rec remove x = function | Nil -> nil | Cons (y, _, l) -> - if H.eq x y then l + if H.equal x y then l else cons y (remove x l) let rec mem x = function | Nil -> false - | Cons (y, _, l) -> H.eq x y || mem x l + | Cons (y, _, l) -> H.equal x y || mem x l let rec compare cmp l1 l2 = match l1, l2 with | Nil, Nil -> 0 @@ -251,7 +251,7 @@ module Level = struct type _t = t type t = _t type u = unit - let eq x y = x.hash == y.hash && RawLevel.hequal x.data y.data + let equal x y = x.hash == y.hash && RawLevel.hequal x.data y.data let hash x = x.hash let hashcons () x = let data' = RawLevel.hcons x.data in @@ -398,7 +398,7 @@ struct let hashcons hdir (b,n as x) = let b' = hdir b in if b' == b then x else (b',n) - let eq l1 l2 = + let equal l1 l2 = l1 == l2 || match l1,l2 with | (b,n), (b',n') -> b == b' && n == n' @@ -417,7 +417,7 @@ struct let hcons = Hashcons.simple_hcons H.generate H.hcons Level.hcons let hash = ExprHash.hash - let eq x y = x == y || + let equal x y = x == y || (let (u,n) = x and (v,n') = y in Int.equal n n' && Level.equal u v) @@ -1293,7 +1293,7 @@ module Hconstraint = type t = univ_constraint type u = universe_level -> universe_level let hashcons hul (l1,k,l2) = (hul l1, k, hul l2) - let eq (l1,k,l2) (l1',k',l2') = + let equal (l1,k,l2) (l1',k',l2') = l1 == l1' && k == k' && l2 == l2' let hash = Hashtbl.hash end) @@ -1305,7 +1305,7 @@ module Hconstraints = type u = univ_constraint -> univ_constraint let hashcons huc s = Constraint.fold (fun x -> Constraint.add (huc x)) s Constraint.empty - let eq s s' = + let equal s s' = List.for_all2eq (==) (Constraint.elements s) (Constraint.elements s') @@ -1676,7 +1676,7 @@ struct a end - let eq t1 t2 = + let equal t1 t2 = t1 == t2 || (Int.equal (Array.length t1) (Array.length t2) && let rec aux i = @@ -2043,7 +2043,7 @@ module Huniverse_set = type u = universe_level -> universe_level let hashcons huc s = LSet.fold (fun x -> LSet.add (huc x)) s LSet.empty - let eq s s' = + let equal s s' = LSet.equal s s' let hash = Hashtbl.hash end) diff --git a/lib/cSet.ml b/lib/cSet.ml index 783165630e..d7d5c70b39 100644 --- a/lib/cSet.ml +++ b/lib/cSet.ml @@ -57,7 +57,7 @@ struct open Hashset.Combine type t = set type u = M.t -> M.t - let eq s1 s2 = s1 == s2 || eqeq (spine s1 []) (spine s2 []) + let equal s1 s2 = s1 == s2 || eqeq (spine s1 []) (spine s2 []) let hash s = Set.fold (fun v accu -> combine (H.hash v) accu) s 0 let hashcons = umap end diff --git a/lib/hashcons.ml b/lib/hashcons.ml index d368e20e6d..46ba0b6285 100644 --- a/lib/hashcons.ml +++ b/lib/hashcons.ml @@ -15,7 +15,7 @@ * of objects of type t (u usually has the form (t1->t1)*(t2->t2)*...). * [hashcons u x] is a function that hash-cons the sub-structures of x using * the hash-consing functions u provides. - * [eq] is a comparison function. It is allowed to use physical equality + * [equal] is a comparison function. It is allowed to use physical equality * on the sub-terms hash-consed by the hashcons function. * [hash] is the hash function given to the Hashtbl.Make function * @@ -27,7 +27,7 @@ module type HashconsedType = type t type u val hashcons : u -> t -> t - val eq : t -> t -> bool + val equal : t -> t -> bool val hash : t -> int end @@ -53,7 +53,7 @@ module Make (X : HashconsedType) : (S with type t = X.t and type u = X.u) = (* We create the type of hashtables for t, with our comparison fun. * An invariant is that the table never contains two entries equals - * w.r.t (=), although the equality on keys is X.eq. This is + * w.r.t (=), although the equality on keys is X.equal. This is * granted since we hcons the subterms before looking up in the table. *) module Htbl = Hashset.Make(X) @@ -124,7 +124,7 @@ module Hlist (D:HashedType) = let hashcons (hrec,hdata) = function | x :: l -> hdata x :: hrec l | l -> l - let eq l1 l2 = + let equal l1 l2 = l1 == l2 || match l1, l2 with | [], [] -> true @@ -144,7 +144,7 @@ module Hstring = Make( type t = string type u = unit let hashcons () s =(* incr accesstr;*) s - external eq : string -> string -> bool = "caml_string_equal" "noalloc" + external equal : string -> string -> bool = "caml_string_equal" "noalloc" (** Copy from CString *) let rec hash len s i accu = if i = len then accu @@ -191,7 +191,7 @@ module Hobj = Make( type t = Obj.t type u = (Obj.t -> Obj.t) * unit let hashcons (hrec,_) = hash_obj hrec - let eq = comp_obj + let equal = comp_obj let hash = Hashtbl.hash end) diff --git a/lib/hashcons.mli b/lib/hashcons.mli index 93890c494b..8d0adc3fd6 100644 --- a/lib/hashcons.mli +++ b/lib/hashcons.mli @@ -14,9 +14,9 @@ module type HashconsedType = sig (** {6 Generic hashconsing signature} - Given an equivalence relation [eq], a hashconsing function is a + Given an equivalence relation [equal], a hashconsing function is a function that associates the same canonical element to two elements - related by [eq]. Usually, the element chosen is canonical w.r.t. + related by [equal]. Usually, the element chosen is canonical w.r.t. physical equality [(==)], so as to reduce memory consumption and enhance efficiency of equality tests. @@ -32,15 +32,15 @@ module type HashconsedType = Usually a tuple of functions. *) val hashcons : u -> t -> t (** The actual hashconsing function, using its fist argument to recursively - hashcons substructures. It should be compatible with [eq], that is - [eq x (hashcons f x) = true]. *) - val eq : t -> t -> bool + hashcons substructures. It should be compatible with [equal], that is + [equal x (hashcons f x) = true]. *) + val equal : t -> t -> bool (** A comparison function. It is allowed to use physical equality on the sub-terms hashconsed by the [hashcons] function, but it should be insensible to shallow copy of the compared object. *) val hash : t -> int (** A hash function passed to the underlying hashtable structure. [hash] - should be compatible with [eq], i.e. if [eq x y = true] then + should be compatible with [equal], i.e. if [equal x y = true] then [hash x = hash y]. *) end diff --git a/lib/hashset.ml b/lib/hashset.ml index 9454aef9bb..1ca6cc6418 100644 --- a/lib/hashset.ml +++ b/lib/hashset.ml @@ -16,7 +16,7 @@ module type EqType = sig type t - val eq : t -> t -> bool + val equal : t -> t -> bool end type statistics = { @@ -183,7 +183,7 @@ module Make (E : EqType) = if i >= sz then ifnotfound index else if h = hashes.(i) then begin match Weak.get bucket i with - | Some v when E.eq v d -> v + | Some v when E.equal v d -> v | _ -> loop (i + 1) end else loop (i + 1) in diff --git a/lib/hashset.mli b/lib/hashset.mli index 270484d8a6..a455eec662 100644 --- a/lib/hashset.mli +++ b/lib/hashset.mli @@ -16,7 +16,7 @@ module type EqType = sig type t - val eq : t -> t -> bool + val equal : t -> t -> bool end type statistics = { diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index b73ff2bc5d..bb07bf0563 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -380,26 +380,24 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty in let consume_stack on_left (termF,skF) (termO,skO) evd = let switch f a b = if on_left then f a b else f b a in - let not_only_appO = Stack.not_purely_applicative skO in - match switch (ise_stack2 not_only_appO env evd (evar_conv_x ts)) skF skO with - |Some (lF,rO), Success i' when on_left && (not_only_appO || List.is_empty lF) -> - (* Case (?termF,stk) = (termO,u1..un::stk') with stk,stk' w/o app *) - (* or (?termF,stk) = (termO,u1..un::stk') with stk,stk' w/o app *) - switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,lF)) (Stack.zip(termO,rO)) - |Some (rO,lF), Success i' when not on_left && (not_only_appO || List.is_empty lF) -> - switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,lF)) (Stack.zip(termO,rO)) + let not_only_app = Stack.not_purely_applicative skO in + match switch (ise_stack2 not_only_app env evd (evar_conv_x ts)) skF skO with + |Some (l,r), Success i' when on_left && (not_only_app || List.is_empty l) -> + switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,l)) (Stack.zip(termO,r)) + |Some (r,l), Success i' when not on_left && (not_only_app || List.is_empty l) -> + switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,l)) (Stack.zip(termO,r)) |None, Success i' -> switch (evar_conv_x ts env i' pbty) termF termO |_, (UnifFailure _ as x) -> x |Some _, _ -> UnifFailure (evd,NotSameArgSize) in - let eta env evd onleft (termR,skR) (termO,skO) = - assert (match skR with [] -> true | _ -> false); - let (na,c1,c'1) = destLambda termR in + let eta env evd onleft sk term sk' term' = + assert (match sk with [] -> true | _ -> false); + let (na,c1,c'1) = destLambda term in let c = nf_evar evd c1 in let env' = push_rel (na,None,c) env in let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env' evd Cst_stack.empty (c'1, Stack.empty) in let out2 = whd_nored_state evd - (Stack.zip (termO, skO @ [Stack.Shift 1]), Stack.append_app [|mkRel 1|] Stack.empty), + (Stack.zip (term', sk' @ [Stack.Shift 1]), Stack.append_app [|mkRel 1|] Stack.empty), Cst_stack.empty in if onleft then evar_eqappr_x ts env' evd CONV out1 out2 else evar_eqappr_x ts env' evd CONV out2 out1 @@ -419,7 +417,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let not_only_app = Stack.not_purely_applicative skM in let f1 i = match Stack.list_of_app_stack skF with - | None -> quick_fail evd + | None -> default_fail evd | Some lF -> let tM = Stack.zip apprM in miller_pfenning on_left @@ -427,9 +425,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) (Stack.zip apprF) tM else quick_fail i) ev lF tM i - and consume (termF,skF as apprF) (termM,skM as apprM) i = + and consume (termF,skF as apprF) (termM,skM as apprM) i = if not (Stack.is_empty skF && Stack.is_empty skM) then - (* This tries first-order matching *) consume_stack on_left apprF apprM i else quick_fail i and delta i = @@ -468,32 +465,32 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let switch f a b = if on_left then f a b else f b a in let eta evd = match kind_of_term termR with - | Lambda _ -> eta env evd false apprR apprF - | Construct u -> eta_constructor ts env evd (u,skR) apprF + | Lambda _ -> eta env evd false skR termR skF termF + | Construct u -> eta_constructor ts env evd skR u skF termF | _ -> UnifFailure (evd,NotSameHead) in - let postpone tR lF evd = - (* Postpone the use of an heuristic *) - if not (occur_rigidly (fst ev) evd tR) then - let evd,tF = - if isRel tR || isVar tR then - (* Optimization so as to generate candidates *) - let evd,ev = evar_absorb_arguments env evd ev lF in - evd,mkEvar ev - else - evd,Stack.zip apprF in - switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) evd)) - tF tR - else - UnifFailure (evd,OccurCheck (fst ev,tR)) - in match Stack.list_of_app_stack skF with | None -> ise_try evd [consume_stack on_left apprF apprR; eta] | Some lF -> let tR = Stack.zip apprR in miller_pfenning on_left - (fun () -> ise_try evd [eta;postpone tR lF]) + (fun () -> + ise_try evd + [eta;(* Postpone the use of an heuristic *) + (fun i -> + if not (occur_rigidly (fst ev) i tR) then + let i,tF = + if isRel tR || isVar tR then + (* Optimization so as to generate candidates *) + let i,ev = evar_absorb_arguments env i ev lF in + i,mkEvar ev + else + i,Stack.zip apprF in + switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) + tF tR + else + UnifFailure (evd,OccurCheck (fst ev,tR)))]) ev lF tR evd in let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in @@ -712,10 +709,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (* Eta-expansion *) | Rigid, _ when isLambda term1 -> - eta env evd true appr1 appr2 + eta env evd true sk1 term1 sk2 term2 | _, Rigid when isLambda term2 -> - eta env evd false appr2 appr1 + eta env evd false sk2 term2 sk1 term1 | Rigid, Rigid -> begin match kind_of_term term1, kind_of_term term2 with @@ -755,10 +752,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty rigids env evd sk1 term1 sk2 term2 | Construct u, _ -> - eta_constructor ts env evd (u,sk1) appr2 + eta_constructor ts env evd sk1 u sk2 term2 | _, Construct u -> - eta_constructor ts env evd (u,sk2) appr1 + eta_constructor ts env evd sk2 u sk1 term1 | Fix ((li1, i1),(_,tys1,bds1 as recdef1)), Fix ((li2, i2),(_,tys2,bds2)) -> (* Partially applied fixs *) if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then @@ -854,7 +851,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) (fst (decompose_app_vect (substl ks h))))] else UnifFailure(evd,(*dummy*)NotSameHead) -and eta_constructor ts env evd (((ind, i), u),sk1) (term2,sk2) = +and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = let mib = lookup_mind (fst ind) env in match mib.Declarations.mind_record with | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 2892de7c45..dc70f36ccf 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -306,9 +306,7 @@ struct | Update t -> str "ZUpdate(" ++ pr_c t ++ str ")" and pr pr_c l = let open Pp in - str "[" ++ - prlist_with_sep pr_semicolon (fun x -> hov 1 (pr_member pr_c x)) l ++ - str "]" + prlist_with_sep pr_semicolon (fun x -> hov 1 (pr_member pr_c x)) l and pr_cst_member pr_c c = let open Pp in diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 51df07f286..1df2a73b2e 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -90,9 +90,6 @@ module Stack : sig val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option val not_purely_applicative : 'a t -> bool - - (** @return the arguments in the stack if a purely applicative - stack, None otherwise *) val list_of_app_stack : constr t -> constr list option val assign : 'a t -> int -> 'a -> 'a t diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index bde0a1c168..d024c01ba5 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -145,12 +145,12 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo delete_current_proof (); iraise reraise -let build_by_tactic ?(side_eff=true) env ctx ?(poly=false) typ tac = +let build_by_tactic env ctx ?(poly=false) typ tac = let id = Id.of_string ("temporary_proof"^string_of_int (next())) in let sign = val_of_named_context (named_context env) in let gk = Global, poly, Proof Theorem in let ce, status, univs = build_constant_by_tactic id ctx sign ~goal_kind:gk typ tac in - let ce = if side_eff then Term_typing.handle_entry_side_effects env ce else { ce with const_entry_body = Future.chain ~pure:true ce.const_entry_body (fun (pt, _) -> pt, Declareops.no_seff) } in + let ce = Term_typing.handle_entry_side_effects env ce in let (cb, ctx), se = Future.force ce.const_entry_body in assert(Declareops.side_effects_is_empty se); assert(Univ.ContextSet.is_empty ctx); diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 4aa3c3bfd2..5e0fb4dd36 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -153,7 +153,7 @@ val build_constant_by_tactic : types -> unit Proofview.tactic -> Entries.definition_entry * bool * Evd.evar_universe_context -val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic -> +val build_by_tactic : env -> Evd.evar_universe_context -> ?poly:polymorphic -> types -> unit Proofview.tactic -> constr * bool * Evd.evar_universe_context diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index dbaa60d610..749e0d2b5b 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -21,7 +21,7 @@ open Ind_tables (* Induction/recursion schemes *) -let optimize_non_type_induction_scheme kind dep sort _ ind = +let optimize_non_type_induction_scheme kind dep sort ind = let env = Global.env () in let sigma = Evd.from_env env in if check_scheme kind ind then @@ -68,15 +68,15 @@ let build_induction_scheme_in_type dep sort ind = let rect_scheme_kind_from_type = declare_individual_scheme_object "_rect_nodep" - (fun _ x -> build_induction_scheme_in_type false InType x, Declareops.no_seff) + (fun x -> build_induction_scheme_in_type false InType x, Declareops.no_seff) let rect_scheme_kind_from_prop = declare_individual_scheme_object "_rect" ~aux:"_rect_from_prop" - (fun _ x -> build_induction_scheme_in_type false InType x, Declareops.no_seff) + (fun x -> build_induction_scheme_in_type false InType x, Declareops.no_seff) let rect_dep_scheme_kind_from_type = declare_individual_scheme_object "_rect" ~aux:"_rect_from_type" - (fun _ x -> build_induction_scheme_in_type true InType x, Declareops.no_seff) + (fun x -> build_induction_scheme_in_type true InType x, Declareops.no_seff) let ind_scheme_kind_from_type = declare_individual_scheme_object "_ind_nodep" @@ -109,24 +109,24 @@ let build_case_analysis_scheme_in_type dep sort ind = let case_scheme_kind_from_type = declare_individual_scheme_object "_case_nodep" - (fun _ x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff) + (fun x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff) let case_scheme_kind_from_prop = declare_individual_scheme_object "_case" ~aux:"_case_from_prop" - (fun _ x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff) + (fun x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff) let case_dep_scheme_kind_from_type = declare_individual_scheme_object "_case" ~aux:"_case_from_type" - (fun _ x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff) + (fun x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff) let case_dep_scheme_kind_from_type_in_prop = declare_individual_scheme_object "_casep_dep" - (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff) + (fun x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff) let case_dep_scheme_kind_from_prop = declare_individual_scheme_object "_case_dep" - (fun _ x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff) + (fun x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff) let case_dep_scheme_kind_from_prop_in_prop = declare_individual_scheme_object "_casep" - (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff) + (fun x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff) diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index f7d3ad5d0a..8643fe10f0 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -191,7 +191,7 @@ let build_sym_scheme env ind = let sym_scheme_kind = declare_individual_scheme_object "_sym_internal" - (fun _ ind -> + (fun ind -> let c, ctx = build_sym_scheme (Global.env() (* side-effect! *)) ind in (c, ctx), Declareops.no_seff) @@ -262,7 +262,7 @@ let build_sym_involutive_scheme env ind = let sym_involutive_scheme_kind = declare_individual_scheme_object "_sym_involutive" - (fun _ ind -> + (fun ind -> build_sym_involutive_scheme (Global.env() (* side-effect! *)) ind) (**********************************************************************) @@ -650,7 +650,7 @@ let build_r2l_forward_rew_scheme = build_r2l_forward_rew_scheme (**********************************************************************) let rew_l2r_dep_scheme_kind = declare_individual_scheme_object "_rew_r_dep" - (fun _ ind -> build_l2r_rew_scheme true (Global.env()) ind InType) + (fun ind -> build_l2r_rew_scheme true (Global.env()) ind InType) (**********************************************************************) (* Dependent rewrite from right-to-left in conclusion *) @@ -660,7 +660,7 @@ let rew_l2r_dep_scheme_kind = (**********************************************************************) let rew_r2l_dep_scheme_kind = declare_individual_scheme_object "_rew_dep" - (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) + (fun ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) (**********************************************************************) (* Dependent rewrite from right-to-left in hypotheses *) @@ -670,7 +670,7 @@ let rew_r2l_dep_scheme_kind = (**********************************************************************) let rew_r2l_forward_dep_scheme_kind = declare_individual_scheme_object "_rew_fwd_dep" - (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) + (fun ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) (**********************************************************************) (* Dependent rewrite from left-to-right in hypotheses *) @@ -680,7 +680,7 @@ let rew_r2l_forward_dep_scheme_kind = (**********************************************************************) let rew_l2r_forward_dep_scheme_kind = declare_individual_scheme_object "_rew_fwd_r_dep" - (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) + (fun ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) (**********************************************************************) (* Non-dependent rewrite from either left-to-right in conclusion or *) @@ -693,7 +693,7 @@ let rew_l2r_forward_dep_scheme_kind = (**********************************************************************) let rew_l2r_scheme_kind = declare_individual_scheme_object "_rew_r" - (fun _ ind -> fix_r2l_forward_rew_scheme + (fun ind -> fix_r2l_forward_rew_scheme (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Declareops.no_seff) (**********************************************************************) @@ -704,7 +704,7 @@ let rew_l2r_scheme_kind = (**********************************************************************) let rew_r2l_scheme_kind = declare_individual_scheme_object "_rew" - (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Declareops.no_seff) + (fun ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Declareops.no_seff) (* End of rewriting schemes *) @@ -780,6 +780,6 @@ let build_congr env (eq,refl,ctx) ind = in c, Evd.evar_universe_context_of ctx let congr_scheme_kind = declare_individual_scheme_object "_congr" - (fun _ ind -> + (fun ind -> (* May fail if equality is not defined *) build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind, Declareops.no_seff) diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index 074004fa12..24d5cf8a99 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -371,7 +371,7 @@ Qed. Goal True. Fail eapply existT. -Set Universal Lemma Under Conjunction. +Set Trivial Tactic Unification Under Conjunction. eapply existT. Abort. diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index 07d7f91506..a7bdba90aa 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -69,9 +69,6 @@ Reserved Notation "{ x }" (at level 0, x at level 99). Reserved Notation "{ x | P }" (at level 0, x at level 99). Reserved Notation "{ x | P & Q }" (at level 0, x at level 99). -Reserved Notation "{ x & P }" (at level 0, x at level 99). -Reserved Notation "{ x & P & Q }" (at level 0, x at level 99). - Reserved Notation "{ x : A | P }" (at level 0, x at level 99). Reserved Notation "{ x : A | P & Q }" (at level 0, x at level 99). diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index ecdbef7f61..1384901b70 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -48,8 +48,6 @@ Notation "{ x | P & Q }" := (sig2 (fun x => P) (fun x => Q)) : type_scope. Notation "{ x : A | P }" := (sig (A:=A) (fun x => P)) : type_scope. Notation "{ x : A | P & Q }" := (sig2 (A:=A) (fun x => P) (fun x => Q)) : type_scope. -Notation "{ x & P }" := (sigT (fun x => P)) : type_scope. -Notation "{ x & P & Q }" := (sigT2 (fun x => P) (fun x => Q)) : type_scope. Notation "{ x : A & P }" := (sigT (A:=A) (fun x => P)) : type_scope. Notation "{ x : A & P & Q }" := (sigT2 (A:=A) (fun x => P) (fun x => Q)) : type_scope. diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 118ffb3e80..d1452fca21 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -111,7 +111,7 @@ let check_bool_is_defined () = let beq_scheme_kind_aux = ref (fun _ -> failwith "Undefined") -let build_beq_scheme mode kn = +let build_beq_scheme kn = check_bool_is_defined (); (* fetching global env *) let env = Global.env() in @@ -188,7 +188,7 @@ let build_beq_scheme mode kn = else begin try let eq, eff = - let c, eff = find_scheme ~mode (!beq_scheme_kind_aux()) (kn',i) in + let c, eff = find_scheme (!beq_scheme_kind_aux()) (kn',i) in mkConst c, eff in let eqa, eff = let eqa, effs = List.split (List.map aux a) in @@ -330,7 +330,7 @@ let destruct_ind c = so from Ai we can find the the correct eq_Ai bl_ai or lb_ai *) (* used in the leib -> bool side*) -let do_replace_lb mode lb_scheme_key aavoid narg p q = +let do_replace_lb lb_scheme_key aavoid narg p q = let avoid = Array.of_list aavoid in let do_arg v offset = try @@ -360,7 +360,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = let u,v = destruct_ind type_of_pq in let lb_type_of_p = try - let c, eff = find_scheme ~mode lb_scheme_key (out_punivs u) (*FIXME*) in + let c, eff = find_scheme lb_scheme_key (out_punivs u) (*FIXME*) in Proofview.tclUNIT (mkConst c, eff) with Not_found -> (* spiwack: the format of this error message should probably @@ -388,7 +388,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = end (* used in the bool -> leib side *) -let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = +let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt = let avoid = Array.of_list aavoid in let do_arg v offset = try @@ -551,7 +551,7 @@ let compute_bl_goal ind lnamesparrec nparrec = (mkApp(Lazy.force eq,[|mkFullInd (ind,u) (nparrec+3);mkVar n;mkVar m|])) ))), eff -let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec = +let compute_bl_tact bl_scheme_key ind lnamesparrec nparrec = let list_id = list_id lnamesparrec in let avoid = ref [] in let first_intros = @@ -608,7 +608,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). if eq_gr (IndRef indeq) Coqlib.glob_eq then Tacticals.New.tclTHEN - (do_replace_bl mode bl_scheme_key ind + (do_replace_bl bl_scheme_key ind (!avoid) nparrec (ca.(2)) (ca.(1))) @@ -625,12 +625,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). let bl_scheme_kind_aux = ref (fun _ -> failwith "Undefined") -let side_effect_of_mode = function - | Declare.KernelVerbose -> false - | Declare.KernelSilent -> true - | Declare.UserVerbose -> false - -let make_bl_scheme mode mind = +let make_bl_scheme mind = let mib = Global.lookup_mind mind in if not (Int.equal (Array.length mib.mind_packets) 1) then errorlabstrm "" @@ -642,9 +637,8 @@ let make_bl_scheme mode mind = context_chop (nparams-nparrec) mib.mind_params_ctxt in let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in let ctx = Evd.empty_evar_universe_context (*FIXME univs *) in - let side_eff = side_effect_of_mode mode in - let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx bl_goal - (compute_bl_tact mode (!bl_scheme_kind_aux()) (ind, Univ.Instance.empty) lnamesparrec nparrec) + let (ans, _, ctx) = Pfedit.build_by_tactic (Global.env()) ctx bl_goal + (compute_bl_tact (!bl_scheme_kind_aux()) (ind, Univ.Instance.empty) lnamesparrec nparrec) in ([|ans|], ctx), eff @@ -694,7 +688,7 @@ let compute_lb_goal ind lnamesparrec nparrec = (mkApp(eq,[|bb;mkApp(eqI,[|mkVar n;mkVar m|]);tt|])) ))), eff -let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = +let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec = let list_id = list_id lnamesparrec in let avoid = ref [] in let first_intros = @@ -738,7 +732,7 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = | App(c,ca) -> (match (kind_of_term ca.(1)) with | App(c',ca') -> let n = Array.length ca' in - do_replace_lb mode lb_scheme_key + do_replace_lb lb_scheme_key (!avoid) nparrec ca'.(n-2) ca'.(n-1) @@ -753,7 +747,7 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = let lb_scheme_kind_aux = ref (fun () -> failwith "Undefined") -let make_lb_scheme mode mind = +let make_lb_scheme mind = let mib = Global.lookup_mind mind in if not (Int.equal (Array.length mib.mind_packets) 1) then errorlabstrm "" @@ -765,9 +759,8 @@ let make_lb_scheme mode mind = context_chop (nparams-nparrec) mib.mind_params_ctxt in let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in let ctx = Evd.empty_evar_universe_context in - let side_eff = side_effect_of_mode mode in - let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx lb_goal - (compute_lb_tact mode (!lb_scheme_kind_aux()) ind lnamesparrec nparrec) + let (ans, _, ctx) = Pfedit.build_by_tactic (Global.env()) ctx lb_goal + (compute_lb_tact (!lb_scheme_kind_aux()) ind lnamesparrec nparrec) in ([|ans|], ctx (* FIXME *)), eff @@ -926,7 +919,7 @@ let compute_dec_tact ind lnamesparrec nparrec = ] end -let make_eq_decidability mode mind = +let make_eq_decidability mind = let mib = Global.lookup_mind mind in if not (Int.equal (Array.length mib.mind_packets) 1) then raise DecidabilityMutualNotSupported; @@ -937,8 +930,7 @@ let make_eq_decidability mode mind = let ctx = Evd.empty_evar_universe_context (* FIXME *)in let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in - let side_eff = side_effect_of_mode mode in - let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx + let (ans, _, ctx) = Pfedit.build_by_tactic (Global.env()) ctx (compute_dec_goal (ind,u) lnamesparrec nparrec) (compute_dec_tact ind lnamesparrec nparrec) in diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index b59d6fc8ae..0d39466ede 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -28,10 +28,11 @@ open Pp (**********************************************************************) (* Registering schemes in the environment *) + type mutual_scheme_object_function = - internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects + mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects type individual_scheme_object_function = - internal_flag -> inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects + inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects type 'a scheme_kind = string @@ -140,31 +141,32 @@ let define internal id c p univs = in kn -let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) = - let (c, ctx), eff = f mode ind in +let define_individual_scheme_base kind suff f internal idopt (mind,i as ind) = + let (c, ctx), eff = f ind in let mib = Global.lookup_mind mind in let id = match idopt with | Some id -> id | None -> add_suffix mib.mind_packets.(i).mind_typename suff in - let const = define mode id c mib.mind_polymorphic ctx in + let const = define internal id c mib.mind_polymorphic ctx in declare_scheme kind [|ind,const|]; const, Declareops.cons_side_effects (Safe_typing.sideff_of_scheme kind (Global.safe_env()) [ind,const]) eff -let define_individual_scheme kind mode names (mind,i as ind) = +let define_individual_scheme kind internal names (mind,i as ind) = match Hashtbl.find scheme_object_table kind with | _,MutualSchemeFunction f -> assert false | s,IndividualSchemeFunction f -> - define_individual_scheme_base kind s f mode names ind + define_individual_scheme_base kind s f internal names ind -let define_mutual_scheme_base kind suff f mode names mind = - let (cl, ctx), eff = f mode mind in +let define_mutual_scheme_base kind suff f internal names mind = + let (cl, ctx), eff = f mind in let mib = Global.lookup_mind mind in let ids = Array.init (Array.length mib.mind_packets) (fun i -> try Int.List.assoc i names with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in + let consts = Array.map2 (fun id cl -> - define mode id cl mib.mind_polymorphic ctx) ids cl in + define internal id cl mib.mind_polymorphic ctx) ids cl in let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in declare_scheme kind schemes; consts, @@ -173,11 +175,11 @@ let define_mutual_scheme_base kind suff f mode names mind = kind (Global.safe_env()) (Array.to_list schemes)) eff -let define_mutual_scheme kind mode names mind = +let define_mutual_scheme kind internal names mind = match Hashtbl.find scheme_object_table kind with | _,IndividualSchemeFunction _ -> assert false | s,MutualSchemeFunction f -> - define_mutual_scheme_base kind s f mode names mind + define_mutual_scheme_base kind s f internal names mind let find_scheme_on_env_too kind ind = let s = String.Map.find kind (Indmap.find ind !scheme_map) in @@ -186,14 +188,14 @@ let find_scheme_on_env_too kind ind = kind (Global.safe_env()) [ind, s]) Declareops.no_seff -let find_scheme ?(mode=KernelSilent) kind (mind,i as ind) = +let find_scheme kind (mind,i as ind) = try find_scheme_on_env_too kind ind with Not_found -> match Hashtbl.find scheme_object_table kind with | s,IndividualSchemeFunction f -> - define_individual_scheme_base kind s f mode None ind + define_individual_scheme_base kind s f KernelSilent None ind | s,MutualSchemeFunction f -> - let ca, eff = define_mutual_scheme_base kind s f mode [] mind in + let ca, eff = define_mutual_scheme_base kind s f KernelSilent [] mind in ca.(i), eff let check_scheme kind ind = diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli index d0844dd946..98eaac0928 100644 --- a/toplevel/ind_tables.mli +++ b/toplevel/ind_tables.mli @@ -8,7 +8,6 @@ open Term open Names -open Declare (** This module provides support for registering inductive scheme builders, declaring schemes and generating schemes on demand *) @@ -20,9 +19,9 @@ type individual type 'a scheme_kind type mutual_scheme_object_function = - internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects + mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects type individual_scheme_object_function = - internal_flag -> inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects + inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects (** Main functions to register a scheme builder *) @@ -33,17 +32,21 @@ val declare_individual_scheme_object : string -> ?aux:string -> individual_scheme_object_function -> individual scheme_kind +(* +val declare_scheme : 'a scheme_kind -> (inductive * constant) array -> unit +*) + (** Force generation of a (mutually) scheme with possibly user-level names *) val define_individual_scheme : individual scheme_kind -> - internal_flag (** internal *) -> + Declare.internal_flag (** internal *) -> Id.t option -> inductive -> constant * Declareops.side_effects -val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) -> +val define_mutual_scheme : mutual scheme_kind -> Declare.internal_flag (** internal *) -> (int * Id.t) list -> mutual_inductive -> constant array * Declareops.side_effects (** Main function to retrieve a scheme in the cache or to generate it *) -val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> constant * Declareops.side_effects +val find_scheme : 'a scheme_kind -> inductive -> constant * Declareops.side_effects val check_scheme : 'a scheme_kind -> inductive -> bool -- cgit v1.2.3 From 12667b1bb33e05ab473b8ee8c4ef9aede5fa2600 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 2 Aug 2015 18:41:08 +0200 Subject: Fixing pop_rel_context. This is necessary for the patch for #4221 (817308ab5) to work. --- kernel/environ.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kernel/environ.ml b/kernel/environ.ml index 30b28177c9..109e3830c2 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -162,7 +162,7 @@ let reset_context = reset_with_named_context empty_named_context_val let pop_rel_context n env = let ctxt = env.env_rel_context in { env with - env_rel_context = List.firstn (List.length ctxt - n) ctxt; + env_rel_context = List.skipn n ctxt; env_nb_rel = env.env_nb_rel - n } let fold_named_context f env ~init = -- cgit v1.2.3 From 47b4573a77ef88f8528c8247108eba8b04d81525 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 2 Aug 2015 18:47:08 +0200 Subject: Fixing test apply.v (had wrong option name). --- test-suite/success/apply.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index 24d5cf8a99..074004fa12 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -371,7 +371,7 @@ Qed. Goal True. Fail eapply existT. -Set Trivial Tactic Unification Under Conjunction. +Set Universal Lemma Under Conjunction. eapply existT. Abort. -- cgit v1.2.3 From 97fba91264669d495643f6a3de6a09790ae2a1da Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 2 Aug 2015 21:08:12 +0200 Subject: Continuing 817308ab (use ltac env for terms in ltac context) + fix of syntax in test file ltac.v. --- pretyping/pretyping.ml | 5 +++-- test-suite/success/ltac.v | 2 +- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index a212735c04..2858a5c1fe 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -297,13 +297,14 @@ let protected_get_type_of env sigma c = (str "Cannot reinterpret " ++ quote (print_constr c) ++ str " in the current environment.") -let pretype_id pretype loc env evdref lvar id = +let pretype_id pretype k0 loc env evdref lvar id = let sigma = !evdref in (* Look for the binder of [id] *) try let (n,_,typ) = lookup_rel_id id (rel_context env) in { uj_val = mkRel n; uj_type = lift n typ } with Not_found -> + let env = ltac_interp_name_env k0 lvar env in (* Check if [id] is an ltac variable *) try let (ids,c) = Id.Map.find id lvar.ltac_constrs in @@ -433,7 +434,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ | GVar (loc, id) -> inh_conv_coerce_to_tycon loc env evdref - (pretype_id (fun e r l t -> pretype tycon e r l t) loc env evdref lvar id) + (pretype_id (fun e r l t -> pretype tycon e r l t) k0 loc env evdref lvar id) tycon | GEvar (loc, id, inst) -> diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 952f35bc35..f9df021dc2 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -304,5 +304,5 @@ Abort. Goal True. let x := ipattern:y in assert (forall x y, x = y + 0). intro. -destruct y. (* Check that the name is y here *). +destruct y. (* Check that the name is y here *) Abort. -- cgit v1.2.3 From dda6d8f639c912597d5bf9e4f1d8c2c118b8dc48 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 3 Aug 2015 10:31:48 +0200 Subject: Test file for #4254: Mutual inductives with parameters on Type raises anomaly. --- test-suite/bugs/closed/4254.v | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 test-suite/bugs/closed/4254.v diff --git a/test-suite/bugs/closed/4254.v b/test-suite/bugs/closed/4254.v new file mode 100644 index 0000000000..ef219973df --- /dev/null +++ b/test-suite/bugs/closed/4254.v @@ -0,0 +1,13 @@ +Inductive foo (V:Type):Type := + | Foo : list (bar V) -> foo V +with bar (V:Type): Type := + | bar1: bar V + | bar2 : V -> bar V. + +Module WithPoly. +Polymorphic Inductive foo (V:Type):Type := + | Foo : list (bar V) -> foo V +with bar (V:Type): Type := + | bar1: bar V + | bar2 : V -> bar V. +End WithPoly. -- cgit v1.2.3