1
0
Fork 0
This repository has been archived on 2024-05-03. You can view files and clone it, but cannot push or open issues or pull requests.
unification-pfa/test/test_projet_pfa_23_24.ml
2024-04-30 11:16:16 +02:00

75 lines
2.7 KiB
Standard ML

open TypeInference
let tests_typeof =
let x = Identifier.fresh () in
let y = Identifier.fresh () in
let z = Identifier.fresh () in
[ (* IntConst *)
"0", Term.IntConst 0, Some Type.Int
; (* int -> int -> int = <fun> *)
( "fun x -> fun y -> x + y"
, Term.(Fun (x, Fun (y, Binop (Var x, Plus, Var y))))
, Some Type.(Arrow (Int, Arrow (Int, Int))) )
; (* Not typed variable *)
"x", Term.(Var "x"), None
; (* Binary operation *)
"1 + 2", Term.(Binop (IntConst 1, Plus, IntConst 2)), Some Type.Int
; (* Pair *)
"(1, 2)", Term.(Pair (IntConst 1, IntConst 2)), Some Type.(Product (Int, Int))
; (* Projection with first *)
"fst (1, 2)", Term.(Proj (First, Pair (IntConst 1, IntConst 2))), Some Type.Int
; (* Projection with second *)
"snd (1, 2)", Term.(Proj (Second, Pair (IntConst 1, IntConst 2))), Some Type.Int
; (* Apply (int) into (fun : int -> int) *)
( "(fun x -> x + 1) 5"
, Term.(App (Fun (x, Binop (Var x, Plus, IntConst 1)), IntConst 5))
, Some Type.Int )
; (* Apply product (int * int) into a not compatible function (fun : int -> int) *)
( "(fun x -> x + 1) (1, 2)"
, Term.(App (Fun (x, Binop (Var x, Plus, IntConst 1)), Pair (IntConst 1, IntConst 2)))
, None )
; (* int -> int -> int = <fun> *)
( "fun x -> fun y -> x * y"
, Term.(Fun (x, Fun (y, Binop (Var x, Times, Var y))))
, Some Type.(Arrow (Int, Arrow (Int, Int))) )
; (* int -> int -> int = <fun> *)
( "fun x -> fun y -> x - y"
, Term.(Fun (x, Fun (y, Binop (Var x, Minus, Var y))))
, Some Type.(Arrow (Int, Arrow (Int, Int))) )
; (* int -> int -> int = <fun> *)
( "fun x -> fun y -> y / x"
, Term.(Fun (x, Fun (y, Binop (Var y, Div, Var x))))
, Some Type.(Arrow (Int, Arrow (Int, Int))) )
; (* Use of a non declared variable *)
"fun x -> fun y -> y / z", Term.(Fun (x, Fun (y, Binop (Var y, Div, Var z)))), None
(* Type mismatch between argument and function *)
; ( "(fun x -> x + 1) true"
, Term.(App (Fun (x, Binop (Var x, Plus, IntConst 1)), Var x))
, None )
; (* Nested functions *)
( "(fun x -> fun y -> x + y) 3 4"
, Term.(
App (App (Fun (x, Fun (y, Binop (Var x, Plus, Var y))), IntConst 3), IntConst 4))
, Some Type.Int )
]
;;
let typeModule = (module Type : Alcotest.TESTABLE with type t = Type.t)
let check_typeof term_text term expected_type =
let open Alcotest in
test_case term_text `Quick (fun () ->
check (option typeModule) "Same type" expected_type (Inference.typeof term))
;;
let () =
let open Alcotest in
run
"Inference"
[ ( "typeof"
, List.map
(fun (term_text, term, expected_type) ->
check_typeof term_text term expected_type)
tests_typeof )
]
;;