Skip to content

GitLab

Commit ff65c47f authored by Pietro Abate's avatar Pietro Abate
Browse files

Make sure fresh variables are really fresh in Tallying.apply

parent 3e06d10f
Hide whitespace changes
Inline Side-by-side
kim_multi.ml deleted 100644 → 0
View file @ 3e06d10f
open TypesOUnit;;
open Types;;
let and_size1 = ref ~-1
let arrow_size1 = ref ~-1
let and_size2 = ref ~-1
let arrow_size2 = ref ~-1
let init_counters () =
and_size1 := ~-1;
and_size2 := ~-1;
arrow_size1 := ~-1;
arrow_size2 := ~-1
let parse_typ s =
let and_size, arrow_size =
if !and_size2 = ~-1 then
and_size2,arrow_size2
else
and_size1,arrow_size1
in
and_size := 0; arrow_size := 0;
for i = 0 to String.length s - 2 do
match s.[i], s.[i+1] with
'&',_ -> incr and_size
| '-', '>' -> incr arrow_size
| _ -> ()
done;
let st = Stream.of_string s in
let astpat = Parser.pat st in
let nodepat = Typer.typ Builtin.env astpat in
Types.descr nodepat
;;
let funs =
(* List of pairs f, args where f is a function types expecting n arguments and
args is a list of n types *)
List.map (fun (f,a) ->
(parse_typ f, List.map parse_typ a,f,a))
Test_arity6.l;;
(* (* HERE Examples with higher order *)
["( 'A01 -> 'B01 ) -> 'A01 -> ('B01)", [
" ('C01 -> 'D01 ) ";
" ('C01 )";
];
"( 'A11 -> 'B11 ) -> ( 'A12 -> 'B12 ) -> 'A11 -> 'A12 -> ('B11, 'B12)", [
" ('C11 -> 'D11 ) ";
" ('C12 -> 'D12 ) ";
" ('C11 )";
" ('C12 )";
];
"( 'A21 -> 'B21 ) -> ( 'A22 -> 'B22 ) -> ( 'A23 -> 'B23 ) -> 'A21 -> 'A22 -> 'A23 -> ('B21, 'B22, 'B23)", [
" ('C21 -> 'D21 ) ";
" ('C22 -> 'D22 ) ";
" ('C23 -> 'D23 ) ";
" ('C21 )";
" ('C22 )";
" ('C23 )";
];
"( 'A31 -> 'B31 ) -> ( 'A32 -> 'B32 ) -> ( 'A33 -> 'B33 ) -> ( 'A34 -> 'B34 ) -> 'A31 -> 'A32 -> 'A33 -> 'A34 -> ('B31, 'B32, 'B33, 'B34)", [
" ('C31 -> 'D31 ) ";
" ('C32 -> 'D32 ) ";
" ('C33 -> 'D33 ) ";
" ('C34 -> 'D34 ) ";
" ('C31 )";
" ('C32 )";
" ('C33 )";
" ('C34 )";
];
"( 'A41 -> 'B41 ) -> ( 'A42 -> 'B42 ) -> ( 'A43 -> 'B43 ) -> ( 'A44 -> 'B44 ) -> ( 'A45 -> 'B45 ) -> 'A41 -> 'A42 -> 'A43 -> 'A44 -> 'A45 -> ('B41, 'B42, 'B43, 'B44, 'B45)", [
" ('C41 -> 'D41 ) ";
" ('C42 -> 'D42 ) ";
" ('C43 -> 'D43 ) ";
" ('C44 -> 'D44 ) ";
" ('C45 -> 'D45 ) ";
" ('C41 )";
" ('C42 )";
" ('C43 )";
" ('C44 )";
" ('C45 )";
];
"( 'A51 -> 'B51 ) -> ( 'A52 -> 'B52 ) -> ( 'A53 -> 'B53 ) -> ( 'A54 -> 'B54 ) -> ( 'A55 -> 'B55 ) -> ( 'A56 -> 'B56 ) -> 'A51 -> 'A52 -> 'A53 -> 'A54 -> 'A55 -> 'A56 -> ('B51, 'B52, 'B53, 'B54, 'B55, 'B56)", [
" ('C51 -> 'D51 ) ";
" ('C52 -> 'D52 ) ";
" ('C53 -> 'D53 ) ";
" ('C54 -> 'D54 ) ";
" ('C55 -> 'D55 ) ";
" ('C56 -> 'D56 ) ";
" ('C51 )";
" ('C52 )";
" ('C53 )";
" ('C54 )";
" ('C55 )";
" ('C56 )";
];
"( 'A61 -> 'B61 ) -> ( 'A62 -> 'B62 ) -> ( 'A63 -> 'B63 ) -> ( 'A64 -> 'B64 ) -> ( 'A65 -> 'B65 ) -> ( 'A66 -> 'B66 ) -> ( 'A67 -> 'B67 ) -> 'A61 -> 'A62 -> 'A63 -> 'A64 -> 'A65 -> 'A66 -> 'A67 -> ('B61, 'B62, 'B63, 'B64, 'B65, 'B66, 'B67)", [
" ('C61 -> 'D61 ) ";
" ('C62 -> 'D62 ) ";
" ('C63 -> 'D63 ) ";
" ('C64 -> 'D64 ) ";
" ('C65 -> 'D65 ) ";
" ('C66 -> 'D66 ) ";
" ('C67 -> 'D67 ) ";
" ('C61 )";
" ('C62 )";
" ('C63 )";
" ('C64 )";
" ('C65 )";
" ('C66 )";
" ('C67 )";
];
"( 'A71 -> 'B71 ) -> ( 'A72 -> 'B72 ) -> ( 'A73 -> 'B73 ) -> ( 'A74 -> 'B74 ) -> ( 'A75 -> 'B75 ) -> ( 'A76 -> 'B76 ) -> ( 'A77 -> 'B77 ) -> ( 'A78 -> 'B78 ) -> 'A71 -> 'A72 -> 'A73 -> 'A74 -> 'A75 -> 'A76 -> 'A77 -> 'A78 -> ('B71, 'B72, 'B73, 'B74, 'B75, 'B76, 'B77, 'B78)", [
" ('C71 -> 'D71 ) ";
" ('C72 -> 'D72 ) ";
" ('C73 -> 'D73 ) ";
" ('C74 -> 'D74 ) ";
" ('C75 -> 'D75 ) ";
" ('C76 -> 'D76 ) ";
" ('C77 -> 'D77 ) ";
" ('C78 -> 'D78 ) ";
" ('C71 )";
" ('C72 )";
" ('C73 )";
" ('C74 )";
" ('C75 )";
" ('C76 )";
" ('C77 )";
" ('C78 )";
];
"( 'A81 -> 'B81 ) -> ( 'A82 -> 'B82 ) -> ( 'A83 -> 'B83 ) -> ( 'A84 -> 'B84 ) -> ( 'A85 -> 'B85 ) -> ( 'A86 -> 'B86 ) -> ( 'A87 -> 'B87 ) -> ( 'A88 -> 'B88 ) -> ( 'A89 -> 'B89 ) -> 'A81 -> 'A82 -> 'A83 -> 'A84 -> 'A85 -> 'A86 -> 'A87 -> 'A88 -> 'A89 -> ('B81, 'B82, 'B83, 'B84, 'B85, 'B86, 'B87, 'B88, 'B89)", [
" ('C81 -> 'D81 ) ";
" ('C82 -> 'D82 ) ";
" ('C83 -> 'D83 ) ";
" ('C84 -> 'D84 ) ";
" ('C85 -> 'D85 ) ";
" ('C86 -> 'D86 ) ";
" ('C87 -> 'D87 ) ";
" ('C88 -> 'D88 ) ";
" ('C89 -> 'D89 ) ";
" ('C81 )";
" ('C82 )";
" ('C83 )";
" ('C84 )";
" ('C85 )";
" ('C86 )";
" ('C87 )";
" ('C88 )";
" ('C89 )";
];
"( 'A91 -> 'B91 ) -> ( 'A92 -> 'B92 ) -> ( 'A93 -> 'B93 ) -> ( 'A94 -> 'B94 ) -> ( 'A95 -> 'B95 ) -> ( 'A96 -> 'B96 ) -> ( 'A97 -> 'B97 ) -> ( 'A98 -> 'B98 ) -> ( 'A99 -> 'B99 ) -> ( 'A910 -> 'B910 ) -> 'A91 -> 'A92 -> 'A93 -> 'A94 -> 'A95 -> 'A96 -> 'A97 -> 'A98 -> 'A99 -> 'A910 -> ('B91, 'B92, 'B93, 'B94, 'B95, 'B96, 'B97, 'B98, 'B99, 'B910)", [
" ('C91 -> 'D91 ) ";
" ('C92 -> 'D92 ) ";
" ('C93 -> 'D93 ) ";
" ('C94 -> 'D94 ) ";
" ('C95 -> 'D95 ) ";
" ('C96 -> 'D96 ) ";
" ('C97 -> 'D97 ) ";
" ('C98 -> 'D98 ) ";
" ('C99 -> 'D99 ) ";
" ('C910 -> 'D910 ) ";
" ('C91 )";
" ('C92 )";
" ('C93 )";
" ('C94 )";
" ('C95 )";
" ('C96 )";
" ('C97 )";
" ('C98 )";
" ('C99 )";
" ('C910 )";
];
"( 'A101 -> 'B101 ) -> ( 'A102 -> 'B102 ) -> ( 'A103 -> 'B103 ) -> ( 'A104 -> 'B104 ) -> ( 'A105 -> 'B105 ) -> ( 'A106 -> 'B106 ) -> ( 'A107 -> 'B107 ) -> ( 'A108 -> 'B108 ) -> ( 'A109 -> 'B109 ) -> ( 'A1010 -> 'B1010 ) -> ( 'A1011 -> 'B1011 ) -> 'A101 -> 'A102 -> 'A103 -> 'A104 -> 'A105 -> 'A106 -> 'A107 -> 'A108 -> 'A109 -> 'A1010 -> 'A1011 -> ('B101, 'B102, 'B103, 'B104, 'B105, 'B106, 'B107, 'B108, 'B109, 'B1010, 'B1011)", [
" ('C101 -> 'D101 ) ";
" ('C102 -> 'D102 ) ";
" ('C103 -> 'D103 ) ";
" ('C104 -> 'D104 ) ";
" ('C105 -> 'D105 ) ";
" ('C106 -> 'D106 ) ";
" ('C107 -> 'D107 ) ";
" ('C108 -> 'D108 ) ";
" ('C109 -> 'D109 ) ";
" ('C1010 -> 'D1010 ) ";
" ('C1011 -> 'D1011 ) ";
" ('C101 )";
" ('C102 )";
" ('C103 )";
" ('C104 )";
" ('C105 )";
" ('C106 )";
" ('C107 )";
" ('C108 )";
" ('C109 )";
" ('C1010 )";
" ('C1011 )";
];
"( 'A111 -> 'B111 ) -> ( 'A112 -> 'B112 ) -> ( 'A113 -> 'B113 ) -> ( 'A114 -> 'B114 ) -> ( 'A115 -> 'B115 ) -> ( 'A116 -> 'B116 ) -> ( 'A117 -> 'B117 ) -> ( 'A118 -> 'B118 ) -> ( 'A119 -> 'B119 ) -> ( 'A1110 -> 'B1110 ) -> ( 'A1111 -> 'B1111 ) -> ( 'A1112 -> 'B1112 ) -> 'A111 -> 'A112 -> 'A113 -> 'A114 -> 'A115 -> 'A116 -> 'A117 -> 'A118 -> 'A119 -> 'A1110 -> 'A1111 -> 'A1112 -> ('B111, 'B112, 'B113, 'B114, 'B115, 'B116, 'B117, 'B118, 'B119, 'B1110, 'B1111, 'B1112)", [
" ('C111 -> 'D111 ) ";
" ('C112 -> 'D112 ) ";
" ('C113 -> 'D113 ) ";
" ('C114 -> 'D114 ) ";
" ('C115 -> 'D115 ) ";
" ('C116 -> 'D116 ) ";
" ('C117 -> 'D117 ) ";
" ('C118 -> 'D118 ) ";
" ('C119 -> 'D119 ) ";
" ('C1110 -> 'D1110 ) ";
" ('C1111 -> 'D1111 ) ";
" ('C1112 -> 'D1112 ) ";
" ('C111 )";
" ('C112 )";
" ('C113 )";
" ('C114 )";
" ('C115 )";
" ('C116 )";
" ('C117 )";
" ('C118 )";
" ('C119 )";
" ('C1110 )";
" ('C1111 )";
" ('C1112 )";
];
"( 'A121 -> 'B121 ) -> ( 'A122 -> 'B122 ) -> ( 'A123 -> 'B123 ) -> ( 'A124 -> 'B124 ) -> ( 'A125 -> 'B125 ) -> ( 'A126 -> 'B126 ) -> ( 'A127 -> 'B127 ) -> ( 'A128 -> 'B128 ) -> ( 'A129 -> 'B129 ) -> ( 'A1210 -> 'B1210 ) -> ( 'A1211 -> 'B1211 ) -> ( 'A1212 -> 'B1212 ) -> ( 'A1213 -> 'B1213 ) -> 'A121 -> 'A122 -> 'A123 -> 'A124 -> 'A125 -> 'A126 -> 'A127 -> 'A128 -> 'A129 -> 'A1210 -> 'A1211 -> 'A1212 -> 'A1213 -> ('B121, 'B122, 'B123, 'B124, 'B125, 'B126, 'B127, 'B128, 'B129, 'B1210, 'B1211, 'B1212, 'B1213)", [
" ('C121 -> 'D121 ) ";
" ('C122 -> 'D122 ) ";
" ('C123 -> 'D123 ) ";
" ('C124 -> 'D124 ) ";
" ('C125 -> 'D125 ) ";
" ('C126 -> 'D126 ) ";
" ('C127 -> 'D127 ) ";
" ('C128 -> 'D128 ) ";
" ('C129 -> 'D129 ) ";
" ('C1210 -> 'D1210 ) ";
" ('C1211 -> 'D1211 ) ";
" ('C1212 -> 'D1212 ) ";
" ('C1213 -> 'D1213 ) ";
" ('C121 )";
" ('C122 )";
" ('C123 )";
" ('C124 )";
" ('C125 )";
" ('C126 )";
" ('C127 )";
" ('C128 )";
" ('C129 )";
" ('C1210 )";
" ('C1211 )";
" ('C1212 )";
" ('C1213 )";
];
"( 'A131 -> 'B131 ) -> ( 'A132 -> 'B132 ) -> ( 'A133 -> 'B133 ) -> ( 'A134 -> 'B134 ) -> ( 'A135 -> 'B135 ) -> ( 'A136 -> 'B136 ) -> ( 'A137 -> 'B137 ) -> ( 'A138 -> 'B138 ) -> ( 'A139 -> 'B139 ) -> ( 'A1310 -> 'B1310 ) -> ( 'A1311 -> 'B1311 ) -> ( 'A1312 -> 'B1312 ) -> ( 'A1313 -> 'B1313 ) -> ( 'A1314 -> 'B1314 ) -> 'A131 -> 'A132 -> 'A133 -> 'A134 -> 'A135 -> 'A136 -> 'A137 -> 'A138 -> 'A139 -> 'A1310 -> 'A1311 -> 'A1312 -> 'A1313 -> 'A1314 -> ('B131, 'B132, 'B133, 'B134, 'B135, 'B136, 'B137, 'B138, 'B139, 'B1310, 'B1311, 'B1312, 'B1313, 'B1314)", [
" ('C131 -> 'D131 ) ";
" ('C132 -> 'D132 ) ";
" ('C133 -> 'D133 ) ";
" ('C134 -> 'D134 ) ";
" ('C135 -> 'D135 ) ";
" ('C136 -> 'D136 ) ";
" ('C137 -> 'D137 ) ";
" ('C138 -> 'D138 ) ";
" ('C139 -> 'D139 ) ";
" ('C1310 -> 'D1310 ) ";
" ('C1311 -> 'D1311 ) ";
" ('C1312 -> 'D1312 ) ";
" ('C1313 -> 'D1313 ) ";
" ('C1314 -> 'D1314 ) ";
" ('C131 )";
" ('C132 )";
" ('C133 )";
" ('C134 )";
" ('C135 )";
" ('C136 )";
" ('C137 )";
" ('C138 )";
" ('C139 )";
" ('C1310 )";
" ('C1311 )";
" ('C1312 )";
" ('C1313 )";
" ('C1314 )";
];
"( 'A141 -> 'B141 ) -> ( 'A142 -> 'B142 ) -> ( 'A143 -> 'B143 ) -> ( 'A144 -> 'B144 ) -> ( 'A145 -> 'B145 ) -> ( 'A146 -> 'B146 ) -> ( 'A147 -> 'B147 ) -> ( 'A148 -> 'B148 ) -> ( 'A149 -> 'B149 ) -> ( 'A1410 -> 'B1410 ) -> ( 'A1411 -> 'B1411 ) -> ( 'A1412 -> 'B1412 ) -> ( 'A1413 -> 'B1413 ) -> ( 'A1414 -> 'B1414 ) -> ( 'A1415 -> 'B1415 ) -> 'A141 -> 'A142 -> 'A143 -> 'A144 -> 'A145 -> 'A146 -> 'A147 -> 'A148 -> 'A149 -> 'A1410 -> 'A1411 -> 'A1412 -> 'A1413 -> 'A1414 -> 'A1415 -> ('B141, 'B142, 'B143, 'B144, 'B145, 'B146, 'B147, 'B148, 'B149, 'B1410, 'B1411, 'B1412, 'B1413, 'B1414, 'B1415)", [
" ('C141 -> 'D141 ) ";
" ('C142 -> 'D142 ) ";
" ('C143 -> 'D143 ) ";
" ('C144 -> 'D144 ) ";
" ('C145 -> 'D145 ) ";
" ('C146 -> 'D146 ) ";
" ('C147 -> 'D147 ) ";
" ('C148 -> 'D148 ) ";
" ('C149 -> 'D149 ) ";
" ('C1410 -> 'D1410 ) ";
" ('C1411 -> 'D1411 ) ";
" ('C1412 -> 'D1412 ) ";
" ('C1413 -> 'D1413 ) ";
" ('C1414 -> 'D1414 ) ";
" ('C1415 -> 'D1415 ) ";
" ('C141 )";
" ('C142 )";
" ('C143 )";
" ('C144 )";
" ('C145 )";
" ('C146 )";
" ('C147 )";
" ('C148 )";
" ('C149 )";
" ('C1410 )";
" ('C1411 )";
" ('C1412 )";
" ('C1413 )";
" ('C1414 )";
" ('C1415 )";
];
]
;;
*)
(* (* HERE easy examples with Integers *)
[
"'A01 -> Int", [
"Int";
];
"'A11 -> 'A12 -> Int", [
"Int";
"Int";
];
"'A21 -> 'A22 -> 'A23 -> Int", [
"Int";
"Int";
"Int";
];
"'A31 -> 'A32 -> 'A33 -> 'A34 -> Int", [
"Int";
"Int";
"Int";
"Int";
];
"'A41 -> 'A42 -> 'A43 -> 'A44 -> 'A45 -> Int", [
"Int";
"Int";
"Int";
"Int";
"Int";
];
"'A51 -> 'A52 -> 'A53 -> 'A54 -> 'A55 -> 'A56 -> Int", [
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
];
"'A61 -> 'A62 -> 'A63 -> 'A64 -> 'A65 -> 'A66 -> 'A67 -> Int", [
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
];
"'A71 -> 'A72 -> 'A73 -> 'A74 -> 'A75 -> 'A76 -> 'A77 -> 'A78 -> Int", [
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
];
"'A81 -> 'A82 -> 'A83 -> 'A84 -> 'A85 -> 'A86 -> 'A87 -> 'A88 -> 'A89 -> Int", [
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
];
"'A91 -> 'A92 -> 'A93 -> 'A94 -> 'A95 -> 'A96 -> 'A97 -> 'A98 -> 'A99 -> 'A910 -> Int", [
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
];
"'A101 -> 'A102 -> 'A103 -> 'A104 -> 'A105 -> 'A106 -> 'A107 -> 'A108 -> 'A109 -> 'A1010 -> 'A1011 -> Int", [
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
];
"'A111 -> 'A112 -> 'A113 -> 'A114 -> 'A115 -> 'A116 -> 'A117 -> 'A118 -> 'A119 -> 'A1110 -> 'A1111 -> 'A1112 -> Int", [
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
];
"'A121 -> 'A122 -> 'A123 -> 'A124 -> 'A125 -> 'A126 -> 'A127 -> 'A128 -> 'A129 -> 'A1210 -> 'A1211 -> 'A1212 -> 'A1213 -> Int", [
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
];
"'A131 -> 'A132 -> 'A133 -> 'A134 -> 'A135 -> 'A136 -> 'A137 -> 'A138 -> 'A139 -> 'A1310 -> 'A1311 -> 'A1312 -> 'A1313 -> 'A1314 -> Int", [
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
];
"'A141 -> 'A142 -> 'A143 -> 'A144 -> 'A145 -> 'A146 -> 'A147 -> 'A148 -> 'A149 -> 'A1410 -> 'A1411 -> 'A1412 -> 'A1413 -> 'A1414 -> 'A1415 -> Int", [
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
];
"'A151 -> 'A152 -> 'A153 -> 'A154 -> 'A155 -> 'A156 -> 'A157 -> 'A158 -> 'A159 -> 'A1510 -> 'A1511 -> 'A1512 -> 'A1513 -> 'A1514 -> 'A1515 -> 'A1516 -> Int", [
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
];
"'A161 -> 'A162 -> 'A163 -> 'A164 -> 'A165 -> 'A166 -> 'A167 -> 'A168 -> 'A169 -> 'A1610 -> 'A1611 -> 'A1612 -> 'A1613 -> 'A1614 -> 'A1615 -> 'A1616 -> 'A1617 -> Int", [
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
];
"'A171 -> 'A172 -> 'A173 -> 'A174 -> 'A175 -> 'A176 -> 'A177 -> 'A178 -> 'A179 -> 'A1710 -> 'A1711 -> 'A1712 -> 'A1713 -> 'A1714 -> 'A1715 -> 'A1716 -> 'A1717 -> 'A1718 -> Int", [
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
];
"'A181 -> 'A182 -> 'A183 -> 'A184 -> 'A185 -> 'A186 -> 'A187 -> 'A188 -> 'A189 -> 'A1810 -> 'A1811 -> 'A1812 -> 'A1813 -> 'A1814 -> 'A1815 -> 'A1816 -> 'A1817 -> 'A1818 -> 'A1819 -> Int", [
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
];
"'A191 -> 'A192 -> 'A193 -> 'A194 -> 'A195 -> 'A196 -> 'A197 -> 'A198 -> 'A199 -> 'A1910 -> 'A1911 -> 'A1912 -> 'A1913 -> 'A1914 -> 'A1915 -> 'A1916 -> 'A1917 -> 'A1918 -> 'A1919 -> 'A1920 -> Int", [
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
"Int";
];
];; *)
let count = ref 0
let all_times = ref []
let time msg f arg1 arg2 =
incr count;
let t1 = Unix.gettimeofday () in
let res = f arg1 arg2
in
let t2 = Unix.gettimeofday () in
let time = (1000. *. (t2 -. t1)) in
all_times := ( (!and_size1, !arrow_size1, !and_size2, !arrow_size2), time) :: !all_times;
init_counters ();
let () = Printf.printf "%s\n=>%f ms (%i)\n-------\n\n%!"
msg time !count
in res
;;
let () = at_exit (fun () ->
let arr = Array.of_list (List.sort (fun (_,x) (_,y) -> Pervasives.compare x y) !all_times) in
let len =
Array.length arr
in
let min = snd arr.(0) in
let max = snd arr.(len-1) in
let med = if len mod 2 = 0 then ((snd arr.(len/2)) +. (snd arr.(len/2 + 1)))/. 2.
else snd arr.(len/2)
in
let total = Array.fold_left (fun acc (_,x) -> x +. acc) 0. arr in
let avg = total /. (float len) in
Printf.eprintf "Number of tests: %i, Total time: %fms, Median time: %fms, Average time: %fms, Min: %fms, Max: %fms\n%!" !count
total med avg min max;
Array.iter (fun ((i,j, k, l), f) ->
Printf.eprintf "%i, %i, %i, %i, %f\n" i j k l f) arr
)
;;
let apply f a = Types.apply_full f a
;;
let apply_list f l = List.fold_left apply f l
;;
let _ =
List.iter (fun (f,a,s,arg) -> print_endline s; List.iter print_endline arg; ignore (time "Application" apply_list f a)) funs
;;
types/types.ml
View file @ ff65c47f
......@@ -2610,6 +2610,7 @@ module Positive = struct
descr(solve x)
end
(* Pre-condition : alpha \not\in \delta *)
let substitute t (alpha,s) =
if no_var t then t
else begin
......@@ -2639,9 +2640,7 @@ module Positive = struct
(* We cannot use the variance annotation of variables to simplify them,
since variables are shared amongst types. If we have two types
A -> A and (A,A) (produced by the algorithm) then we can still simplify the
latter but the variance annotation tells us that A is invariant.
*)
latter but the variance annotation tells us that A is invariant. *)
let collect_variables delta v =
(* we memoize based on the pair (pos, v), since v can occur both
positively and negatively. and we want to manage the variables
......@@ -2654,10 +2653,14 @@ module Positive = struct
let equal (a,b) (c,d) = a == c && b == d
end)
in
let rec pretty_name i acc =
let ni,nm = i/26, i mod 26 in
let acc = acc ^ (String.make 1 (OldChar.chr (OldChar.code 'a' + nm))) in
if ni == 0 then acc else pretty_name ni acc
let rec freshvar idx =
let rec pretty i acc =
let ni,nm = i/26, i mod 26 in
let acc = acc ^ (String.make 1 (OldChar.chr (OldChar.code 'a' + nm))) in
if ni == 0 then acc else pretty ni acc
in
let x = Var.mk (pretty !idx "") in
if Var.Set.mem x delta then (incr idx; freshvar idx) else x
in
let vars = Hashtbl.create 17 in
let memo = Memo.create 17 in
......@@ -2674,16 +2677,11 @@ module Positive = struct
begin try
let td = Hashtbl.find vars d in
(* polarity conflict, replace the binding by a new, pretty-printed variable *)