From: Stefano Zacchiroli Date: Tue, 2 Mar 2004 17:12:19 +0000 (+0000) Subject: - regtest now handles more than one interpretation: the tests committed X-Git-Tag: v0_0_4~56 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9b0237f419714f67bfe4ae0cdee2c59986588e50;p=helm.git - regtest now handles more than one interpretation: the tests committed here have been ported to latest regtest format - more informative failure report --- diff --git a/helm/gTopLevel/regtest.ml b/helm/gTopLevel/regtest.ml index e31b1da05..4e72bdd54 100644 --- a/helm/gTopLevel/regtest.ml +++ b/helm/gTopLevel/regtest.ml @@ -191,17 +191,33 @@ let as_expected report_fname expected found = (if Sys.file_exists report_fname then Sys.remove report_fname) ; let och = lazy (open_out report_fname) in let print_endline s = print_endline_to_channel (Lazy.force och) s in + let print_interpretation test = + print_endline "## Interpretation dump ##"; + print_endline "# Disambiguation environment:"; + print_endline test.eenv; + print_endline "# Metasenv:"; + print_endline test.emetasenv; + print_endline "# Term:"; + print_endline test.eterm; + print_endline "# Type:"; + print_endline test.etype; + print_endline "# Reduced term:"; + print_endline test.ereduced; + in let rec aux = function [],[] -> true | ex::extl, fo::fotl -> - as_expected_one och ex fo && - aux (extl,fotl) + let outcome1 = as_expected_one och ex fo in + let outcome2 = aux (extl,fotl) in + outcome1 && outcome2 | [],found -> - print_endline "### Too many interpretations found" ; + print_endline "### Too many interpretations found:" ; + List.iter print_interpretation found; false | expected,[] -> - print_endline "### Too few interpretations found" ; + print_endline "### Too few interpretations found:" ; + List.iter print_interpretation expected; false in let outcome = aux (expected,found) in diff --git a/helm/gTopLevel/tests/fix00.cic.test b/helm/gTopLevel/tests/fix00.cic.test index 901acd990..8719cbed3 100644 --- a/helm/gTopLevel/tests/fix00.cic.test +++ b/helm/gTopLevel/tests/fix00.cic.test @@ -6,6 +6,12 @@ let rec fact = | (S (x: nat)) \Rightarrow (mult (S x) (fact x)) ] in (fact 4) +###### INTERPRETATION NUMBER 1 ###### +### (* disambiguation environment *) +alias id S = cic:/Coq/Init/Datatypes/nat.ind#1/1/2 +alias id mult = cic:/Coq/Init/Peano/mult.con +alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1 +alias num (instance 0) = "natural number" ### (* METASENV after disambiguation *) ### (* TERM after disambiguation *) @@ -23,7 +29,7 @@ nat ### (* REDUCED disambiguated term *) (S ( Fix plus { -plus / 0 : (n:nat)(nat->nat) := +plus / 0 : (n:nat)(m:nat)nat := [n:nat][m:nat] <[n0:nat]nat>Cases n of O => m @@ -31,7 +37,7 @@ plus / 0 : (n:nat)(nat->nat) := end} (S ( Fix plus { -plus / 0 : (n:nat)(nat->nat) := +plus / 0 : (n:nat)(m:nat)nat := [n:nat][m:nat] <[n0:nat]nat>Cases n of O => m @@ -39,7 +45,7 @@ plus / 0 : (n:nat)(nat->nat) := end} O (S ( Fix plus { -plus / 0 : (n:nat)(nat->nat) := +plus / 0 : (n:nat)(m:nat)nat := [n:nat][m:nat] <[n0:nat]nat>Cases n of O => m @@ -47,7 +53,7 @@ plus / 0 : (n:nat)(nat->nat) := end} (S ( Fix plus { -plus / 0 : (n:nat)(nat->nat) := +plus / 0 : (n:nat)(m:nat)nat := [n:nat][m:nat] <[n0:nat]nat>Cases n of O => m @@ -55,7 +61,7 @@ plus / 0 : (n:nat)(nat->nat) := end} O O)) (S ( Fix plus { -plus / 0 : (n:nat)(nat->nat) := +plus / 0 : (n:nat)(m:nat)nat := [n:nat][m:nat] <[n0:nat]nat>Cases n of O => m @@ -63,7 +69,7 @@ plus / 0 : (n:nat)(nat->nat) := end} (S ( Fix plus { -plus / 0 : (n:nat)(nat->nat) := +plus / 0 : (n:nat)(m:nat)nat := [n:nat][m:nat] <[n0:nat]nat>Cases n of O => m @@ -71,7 +77,7 @@ plus / 0 : (n:nat)(nat->nat) := end} O O)) O)))))) (S ( Fix plus { -plus / 0 : (n:nat)(nat->nat) := +plus / 0 : (n:nat)(m:nat)nat := [n:nat][m:nat] <[n0:nat]nat>Cases n of O => m @@ -79,7 +85,7 @@ plus / 0 : (n:nat)(nat->nat) := end} (S ( Fix plus { -plus / 0 : (n:nat)(nat->nat) := +plus / 0 : (n:nat)(m:nat)nat := [n:nat][m:nat] <[n0:nat]nat>Cases n of O => m @@ -87,7 +93,7 @@ plus / 0 : (n:nat)(nat->nat) := end} O (S ( Fix plus { -plus / 0 : (n:nat)(nat->nat) := +plus / 0 : (n:nat)(m:nat)nat := [n:nat][m:nat] <[n0:nat]nat>Cases n of O => m @@ -95,7 +101,7 @@ plus / 0 : (n:nat)(nat->nat) := end} (S ( Fix plus { -plus / 0 : (n:nat)(nat->nat) := +plus / 0 : (n:nat)(m:nat)nat := [n:nat][m:nat] <[n0:nat]nat>Cases n of O => m @@ -103,7 +109,7 @@ plus / 0 : (n:nat)(nat->nat) := end} O O)) (S ( Fix plus { -plus / 0 : (n:nat)(nat->nat) := +plus / 0 : (n:nat)(m:nat)nat := [n:nat][m:nat] <[n0:nat]nat>Cases n of O => m @@ -111,7 +117,7 @@ plus / 0 : (n:nat)(nat->nat) := end} (S ( Fix plus { -plus / 0 : (n:nat)(nat->nat) := +plus / 0 : (n:nat)(m:nat)nat := [n:nat][m:nat] <[n0:nat]nat>Cases n of O => m @@ -119,7 +125,7 @@ plus / 0 : (n:nat)(nat->nat) := end} O O)) O)))))) (S ( Fix plus { -plus / 0 : (n:nat)(nat->nat) := +plus / 0 : (n:nat)(m:nat)nat := [n:nat][m:nat] <[n0:nat]nat>Cases n of O => m @@ -127,7 +133,7 @@ plus / 0 : (n:nat)(nat->nat) := end} (S ( Fix plus { -plus / 0 : (n:nat)(nat->nat) := +plus / 0 : (n:nat)(m:nat)nat := [n:nat][m:nat] <[n0:nat]nat>Cases n of O => m @@ -135,7 +141,7 @@ plus / 0 : (n:nat)(nat->nat) := end} O (S ( Fix plus { -plus / 0 : (n:nat)(nat->nat) := +plus / 0 : (n:nat)(m:nat)nat := [n:nat][m:nat] <[n0:nat]nat>Cases n of O => m @@ -143,7 +149,7 @@ plus / 0 : (n:nat)(nat->nat) := end} (S ( Fix plus { -plus / 0 : (n:nat)(nat->nat) := +plus / 0 : (n:nat)(m:nat)nat := [n:nat][m:nat] <[n0:nat]nat>Cases n of O => m @@ -151,7 +157,7 @@ plus / 0 : (n:nat)(nat->nat) := end} O O)) (S ( Fix plus { -plus / 0 : (n:nat)(nat->nat) := +plus / 0 : (n:nat)(m:nat)nat := [n:nat][m:nat] <[n0:nat]nat>Cases n of O => m @@ -159,7 +165,7 @@ plus / 0 : (n:nat)(nat->nat) := end} (S ( Fix plus { -plus / 0 : (n:nat)(nat->nat) := +plus / 0 : (n:nat)(m:nat)nat := [n:nat][m:nat] <[n0:nat]nat>Cases n of O => m @@ -167,7 +173,7 @@ plus / 0 : (n:nat)(nat->nat) := end} O O)) O)))))) (S ( Fix plus { -plus / 0 : (n:nat)(nat->nat) := +plus / 0 : (n:nat)(m:nat)nat := [n:nat][m:nat] <[n0:nat]nat>Cases n of O => m @@ -175,7 +181,7 @@ plus / 0 : (n:nat)(nat->nat) := end} (S ( Fix plus { -plus / 0 : (n:nat)(nat->nat) := +plus / 0 : (n:nat)(m:nat)nat := [n:nat][m:nat] <[n0:nat]nat>Cases n of O => m @@ -183,7 +189,7 @@ plus / 0 : (n:nat)(nat->nat) := end} O (S ( Fix plus { -plus / 0 : (n:nat)(nat->nat) := +plus / 0 : (n:nat)(m:nat)nat := [n:nat][m:nat] <[n0:nat]nat>Cases n of O => m @@ -191,7 +197,7 @@ plus / 0 : (n:nat)(nat->nat) := end} (S ( Fix plus { -plus / 0 : (n:nat)(nat->nat) := +plus / 0 : (n:nat)(m:nat)nat := [n:nat][m:nat] <[n0:nat]nat>Cases n of O => m @@ -199,7 +205,7 @@ plus / 0 : (n:nat)(nat->nat) := end} O O)) (S ( Fix plus { -plus / 0 : (n:nat)(nat->nat) := +plus / 0 : (n:nat)(m:nat)nat := [n:nat][m:nat] <[n0:nat]nat>Cases n of O => m @@ -207,7 +213,7 @@ plus / 0 : (n:nat)(nat->nat) := end} (S ( Fix plus { -plus / 0 : (n:nat)(nat->nat) := +plus / 0 : (n:nat)(m:nat)nat := [n:nat][m:nat] <[n0:nat]nat>Cases n of O => m diff --git a/helm/gTopLevel/tests/forall00.cic.test b/helm/gTopLevel/tests/forall00.cic.test index 1665098f7..29a06443b 100644 --- a/helm/gTopLevel/tests/forall00.cic.test +++ b/helm/gTopLevel/tests/forall00.cic.test @@ -1,4 +1,9 @@ \forall n:nat. \forall m. n + m = n +###### INTERPRETATION NUMBER 1 ###### +### (* disambiguation environment *) +alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1 +alias symbol "eq" (instance 0) = "leibnitz's equality" +alias symbol "plus" (instance 0) = "natural plus" ### (* METASENV after disambiguation *) ### (* TERM after disambiguation *) diff --git a/helm/gTopLevel/tests/lambda01.cic.test b/helm/gTopLevel/tests/lambda01.cic.test index 8c9b561c4..4ca229fa8 100644 --- a/helm/gTopLevel/tests/lambda01.cic.test +++ b/helm/gTopLevel/tests/lambda01.cic.test @@ -1,5 +1,11 @@ (\lambda f. (f 0 (le_n 0)) \lambda n. \lambda H. (refl_equal nat 0)) +###### INTERPRETATION NUMBER 1 ###### +### (* disambiguation environment *) +alias id le_n = cic:/Coq/Init/Peano/le.ind#1/1/1 +alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1 +alias id refl_equal = cic:/Coq/Init/Logic/eq.ind#1/1/1 +alias num (instance 0) = "natural number" ### (* METASENV after disambiguation *) ### (* TERM after disambiguation *) diff --git a/helm/gTopLevel/tests/lambda02.cic.test b/helm/gTopLevel/tests/lambda02.cic.test index fde5288f9..259140c9e 100644 --- a/helm/gTopLevel/tests/lambda02.cic.test +++ b/helm/gTopLevel/tests/lambda02.cic.test @@ -1,4 +1,11 @@ \lambda f:(\forall n:nat. (\forall H:(le 0 n). (n=n))). (f 0 (le_n 0)) +###### INTERPRETATION NUMBER 1 ###### +### (* disambiguation environment *) +alias id le = cic:/Coq/Init/Peano/le.ind#1/1 +alias id le_n = cic:/Coq/Init/Peano/le.ind#1/1/1 +alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1 +alias num (instance 0) = "natural number" +alias symbol "eq" (instance 0) = "leibnitz's equality" ### (* METASENV after disambiguation *) ### (* TERM after disambiguation *) diff --git a/helm/gTopLevel/tests/lambda03.cic.test b/helm/gTopLevel/tests/lambda03.cic.test index e6d731cde..4f21c8339 100644 --- a/helm/gTopLevel/tests/lambda03.cic.test +++ b/helm/gTopLevel/tests/lambda03.cic.test @@ -1,5 +1,12 @@ \lambda n:nat. \lambda H:n=n.\lambda g:(?\to (le n 0))\to True.(g \lambda f.(f n H)) +###### INTERPRETATION NUMBER 1 ###### +### (* disambiguation environment *) +alias id True = cic:/Coq/Init/Logic/True.ind#1/1 +alias id le = cic:/Coq/Init/Peano/le.ind#1/1 +alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1 +alias num (instance 0) = "natural number" +alias symbol "eq" (instance 0) = "leibnitz's equality" ### (* METASENV after disambiguation *) ### (* TERM after disambiguation *) diff --git a/helm/gTopLevel/tests/match00.cic.test b/helm/gTopLevel/tests/match00.cic.test index 03db53319..b2de9dbd1 100644 --- a/helm/gTopLevel/tests/match00.cic.test +++ b/helm/gTopLevel/tests/match00.cic.test @@ -4,6 +4,13 @@ match (S O):nat with [ O \Rightarrow O | (S x) \Rightarrow false ] +###### INTERPRETATION NUMBER 1 ###### +### (* disambiguation environment *) +alias id O = cic:/Coq/Init/Datatypes/nat.ind#1/1/1 +alias id S = cic:/Coq/Init/Datatypes/nat.ind#1/1/2 +alias id bool = cic:/Coq/Init/Datatypes/bool.ind#1/1 +alias id false = cic:/Coq/Init/Datatypes/bool.ind#1/1/2 +alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1 ### (* METASENV after disambiguation *) ### (* TERM after disambiguation *) diff --git a/helm/gTopLevel/tests/match01.cic.test b/helm/gTopLevel/tests/match01.cic.test index 089665f6a..8d734e28f 100644 --- a/helm/gTopLevel/tests/match01.cic.test +++ b/helm/gTopLevel/tests/match01.cic.test @@ -2,6 +2,14 @@ match (le_n O): le with [ le_n \Rightarrow (refl_equal nat O) | (le_S x y) \Rightarrow (refl_equal nat O) ] +###### INTERPRETATION NUMBER 1 ###### +### (* disambiguation environment *) +alias id O = cic:/Coq/Init/Datatypes/nat.ind#1/1/1 +alias id eq = cic:/Coq/Init/Logic/eq.ind#1/1 +alias id le = cic:/Coq/Init/Peano/le.ind#1/1 +alias id le_n = cic:/Coq/Init/Peano/le.ind#1/1/1 +alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1 +alias id refl_equal = cic:/Coq/Init/Logic/eq.ind#1/1/1 ### (* METASENV after disambiguation *) ### (* TERM after disambiguation *) diff --git a/helm/gTopLevel/tests/match02.cic.test b/helm/gTopLevel/tests/match02.cic.test index c26510274..49f680053 100644 --- a/helm/gTopLevel/tests/match02.cic.test +++ b/helm/gTopLevel/tests/match02.cic.test @@ -2,6 +2,14 @@ match (le_S 0 0 (le_n 0)): le with [ le_n \Rightarrow (le_S 0 0 (le_n 0)) | (le_S x y) \Rightarrow (le_S 0 (S x) (le_S 0 x y)) ] +###### INTERPRETATION NUMBER 1 ###### +### (* disambiguation environment *) +alias id S = cic:/Coq/Init/Datatypes/nat.ind#1/1/2 +alias id le = cic:/Coq/Init/Peano/le.ind#1/1 +alias id le_S = cic:/Coq/Init/Peano/le.ind#1/1/2 +alias id le_n = cic:/Coq/Init/Peano/le.ind#1/1/1 +alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1 +alias num (instance 0) = "natural number" ### (* METASENV after disambiguation *) ### (* TERM after disambiguation *) diff --git a/helm/gTopLevel/tests/match03.cic.test b/helm/gTopLevel/tests/match03.cic.test index 16b4097e7..94681ed59 100644 --- a/helm/gTopLevel/tests/match03.cic.test +++ b/helm/gTopLevel/tests/match03.cic.test @@ -2,6 +2,13 @@ match true:bool with [ true \Rightarrow O | false \Rightarrow (S O) ] +###### INTERPRETATION NUMBER 1 ###### +### (* disambiguation environment *) +alias id O = cic:/Coq/Init/Datatypes/nat.ind#1/1/1 +alias id S = cic:/Coq/Init/Datatypes/nat.ind#1/1/2 +alias id bool = cic:/Coq/Init/Datatypes/bool.ind#1/1 +alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1 +alias id true = cic:/Coq/Init/Datatypes/bool.ind#1/1/1 ### (* METASENV after disambiguation *) ### (* TERM after disambiguation *) diff --git a/helm/gTopLevel/tests/match04.cic.test b/helm/gTopLevel/tests/match04.cic.test index 280bfbf5d..9c8016c60 100644 --- a/helm/gTopLevel/tests/match04.cic.test +++ b/helm/gTopLevel/tests/match04.cic.test @@ -2,6 +2,11 @@ match O:nat with [ O \Rightarrow O | (S x) \Rightarrow (S (S x)) ] +###### INTERPRETATION NUMBER 1 ###### +### (* disambiguation environment *) +alias id O = cic:/Coq/Init/Datatypes/nat.ind#1/1/1 +alias id S = cic:/Coq/Init/Datatypes/nat.ind#1/1/2 +alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1 ### (* METASENV after disambiguation *) ### (* TERM after disambiguation *) diff --git a/helm/gTopLevel/tests/match05.cic.test b/helm/gTopLevel/tests/match05.cic.test index 6bda244d4..921264d6a 100644 --- a/helm/gTopLevel/tests/match05.cic.test +++ b/helm/gTopLevel/tests/match05.cic.test @@ -2,6 +2,45 @@ match nil:list with [ nil \Rightarrow nil | (cons x y) \Rightarrow (cons x y) ] +###### INTERPRETATION NUMBER 1 ###### +### (* disambiguation environment *) +alias id cons = cic:/Algebra/algebra/ListType/list.ind#1/1/2 +alias id list = cic:/Algebra/algebra/ListType/list.ind#1/1 +alias id nil = cic:/Algebra/algebra/ListType/list.ind#1/1/1 +### (* METASENV after disambiguation *) +_ :? _; _ :? _ |- ?25: Type +### (* TERM after disambiguation *) + +<[x:list{A:=?25[_ ; _]}]list{A:=?25[_ ; _]}>Cases nil{A:=?25[_ ; _]} of + nil => nil{A:=?25[_ ; _]} + cons => [x:?25[_ ; _]][y:list{A:=?25[x ; _]}](cons{A:=?25[x ; y]} x y) +end +### (* TYPE_OF the disambiguated term *) +([x:list{A:=?25[_ ; _]}]list{A:=?25[_ ; _]} nil{A:=?25[_ ; _]}) +### (* REDUCED disambiguated term *) +nil{A:=?25[_ ; _]} +###### INTERPRETATION NUMBER 2 ###### +### (* disambiguation environment *) +alias id cons = cic:/Coq/Lists/List/list.ind#1/1/2 +alias id list = cic:/Coq/Lists/List/list.ind#1/1 +alias id nil = cic:/Coq/Lists/List/list.ind#1/1/1 +### (* METASENV after disambiguation *) +_ :? _; _ :? _ |- ?25: Set +### (* TERM after disambiguation *) + +<[x:list{A:=?25[_ ; _]}]list{A:=?25[_ ; _]}>Cases nil{A:=?25[_ ; _]} of + nil => nil{A:=?25[_ ; _]} + cons => [x:?25[_ ; _]][y:list{A:=?25[x ; _]}](cons{A:=?25[x ; y]} x y) +end +### (* TYPE_OF the disambiguated term *) +([x:list{A:=?25[_ ; _]}]list{A:=?25[_ ; _]} nil{A:=?25[_ ; _]}) +### (* REDUCED disambiguated term *) +nil{A:=?25[_ ; _]} +###### INTERPRETATION NUMBER 3 ###### +### (* disambiguation environment *) +alias id cons = cic:/Coq/Lists/MonoList/list.ind#1/1/2 +alias id list = cic:/Coq/Lists/MonoList/list.ind#1/1 +alias id nil = cic:/Coq/Lists/MonoList/list.ind#1/1/1 ### (* METASENV after disambiguation *) ### (* TERM after disambiguation *) @@ -14,3 +53,20 @@ end ([x:list]list nil) ### (* REDUCED disambiguated term *) nil +###### INTERPRETATION NUMBER 4 ###### +### (* disambiguation environment *) +alias id cons = cic:/Lannion/continuations/weight/specif/list.ind#1/1/2 +alias id list = cic:/Lannion/continuations/weight/specif/list.ind#1/1 +alias id nil = cic:/Lannion/continuations/weight/specif/list.ind#1/1/1 +### (* METASENV after disambiguation *) +_ :? _; _ :? _ |- ?25: Set +### (* TERM after disambiguation *) + +<[x:list{A:=?25[_ ; _]}]list{A:=?25[_ ; _]}>Cases nil{A:=?25[_ ; _]} of + nil => nil{A:=?25[_ ; _]} + cons => [x:?25[_ ; _]][y:list{A:=?25[x ; _]}](cons{A:=?25[x ; y]} x y) +end +### (* TYPE_OF the disambiguated term *) +([x:list{A:=?25[_ ; _]}]list{A:=?25[_ ; _]} nil{A:=?25[_ ; _]}) +### (* REDUCED disambiguated term *) +nil{A:=?25[_ ; _]} diff --git a/helm/gTopLevel/tests/match06.cic.test b/helm/gTopLevel/tests/match06.cic.test index d7078f0ac..041095638 100644 --- a/helm/gTopLevel/tests/match06.cic.test +++ b/helm/gTopLevel/tests/match06.cic.test @@ -1,6 +1,10 @@ \lambda x:False. [\lambda h:False. True] match x:False with [] +###### INTERPRETATION NUMBER 1 ###### +### (* disambiguation environment *) +alias id False = cic:/Coq/Init/Logic/False.ind#1/1 +alias id True = cic:/Coq/Init/Logic/True.ind#1/1 ### (* METASENV after disambiguation *) ### (* TERM after disambiguation *) diff --git a/helm/gTopLevel/tests/match07.cic.test b/helm/gTopLevel/tests/match07.cic.test index ec1ad7156..a8331cff1 100644 --- a/helm/gTopLevel/tests/match07.cic.test +++ b/helm/gTopLevel/tests/match07.cic.test @@ -2,6 +2,13 @@ match true with [ true \Rightarrow O | false \Rightarrow (S O) ] +###### INTERPRETATION NUMBER 1 ###### +### (* disambiguation environment *) +alias id O = cic:/Coq/Init/Datatypes/nat.ind#1/1/1 +alias id S = cic:/Coq/Init/Datatypes/nat.ind#1/1/2 +alias id bool = cic:/Coq/Init/Datatypes/bool.ind#1/1 +alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1 +alias id true = cic:/Coq/Init/Datatypes/bool.ind#1/1/1 ### (* METASENV after disambiguation *) ### (* TERM after disambiguation *)