Paris7/unification-pfa
Archived
1
0
Fork 0
Code Issues Activity

add ocamlformat

Browse source
This commit is contained in:
Mylloon 2024-03-11 15:18:02 +01:00
parent e942f30703
commit 6952cb9be0
Signed by: Anri
GPG key ID: A82D63DFF8D1317F
5 changed files with 31 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
.ocamlformat Normal file
View file

@ -0,0 +1 @@
profile = janestreet

15
lib/term.mli
View file

@ -2,11 +2,16 @@
This module contains the syntax of terms of a minimal programming language. This module contains the syntax of terms of a minimal programming language.
*) *)
type binop = type binop =
| Plus | Minus | Times | Div | Plus
[@@deriving eq, ord, show] | Minus
| Times
| Div
[@@deriving eq, ord, show]
type projection = First | Second type projection =
[@@deriving eq, ord, show] | First
| Second
[@@deriving eq, ord, show]
(* (*
Every value of type Term.t is the abstract syntax tree of a program. Every value of type Term.t is the abstract syntax tree of a program.
@ -19,4 +24,4 @@ type t =
| Proj of projection * t | Proj of projection * t
| Fun of Identifier.t * t | Fun of Identifier.t * t
| App of t * t | App of t * t
[@@deriving eq, ord, show] [@@deriving eq, ord, show]

2
lib/type.mli
View file

@ -3,4 +3,4 @@ type t =
| Int | Int
| Product of t * t | Product of t * t
| Arrow of t * t | Arrow of t * t
[@@deriving eq, ord, show] [@@deriving eq, ord, show]

1
lib/unification.mli
View file

@ -5,6 +5,5 @@
You can use the slides on the Herbrand / Robinson algorithm You can use the slides on the Herbrand / Robinson algorithm
to start designing your implementation. to start designing your implementation.
*) *)
val unify : Type.t -> Type.t -> TypeSubstitution.t option val unify : Type.t -> Type.t -> TypeSubstitution.t option

25
test/test_projet_pfa_23_24.ml
View file

@ -1,19 +1,32 @@
open TypeInference open TypeInference
let tests_typeof = (* TODO: add more tests *) let tests_typeof =
(* TODO: add more tests *)
let x = Identifier.fresh () in let x = Identifier.fresh () in
let y = Identifier.fresh () in let y = Identifier.fresh () in
[ ("0", Term.IntConst 0, Some Type.Int); [ "0", Term.IntConst 0, Some Type.Int
("fun x -> fun y -> x+y", Term.(Fun (x, Fun (y, Binop (Var x, Plus, Var y)))), Some Type.(Arrow (Int, Arrow (Int, Int)))); ] ; ( "fun x -> fun y -> x+y"
, Term.(Fun (x, Fun (y, Binop (Var x, Plus, Var y))))
, Some Type.(Arrow (Int, Arrow (Int, Int))) )
]
;;
let typeModule = (module Type : Alcotest.TESTABLE with type t = Type.t) let typeModule = (module Type : Alcotest.TESTABLE with type t = Type.t)
let check_typeof term_text term expected_type = let check_typeof term_text term expected_type =
let open Alcotest in let open Alcotest in
test_case term_text `Quick (fun () -> check (option typeModule) "Same type" expected_type (Inference.typeof term)) test_case term_text `Quick (fun () ->
check (option typeModule) "Same type" expected_type (Inference.typeof term))
;;
let () = let () =
let open Alcotest in let open Alcotest in
run "Inference" [ run
"typeof", List.map (fun (term_text, term, expected_type) -> check_typeof term_text term expected_type) tests_typeof ; "Inference"
[ ( "typeof"
, List.map
(fun (term_text, term, expected_type) ->
check_typeof term_text term expected_type)
tests_typeof )
] ]
;;