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

oops

Browse source
This commit is contained in:
Mylloon 2024-04-30 13:46:49 +02:00
parent fb7fc53863
commit 63eefc3166
Signed by: Anri
GPG key ID: A82D63DFF8D1317F
2 changed files with 9 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
lib/inference.ml
View file

@ -27,10 +27,8 @@ let typeof t =
(match TypeSubstitution.find id env' with (match TypeSubstitution.find id env' with
| Some ty -> Some ty, env' | Some ty -> Some ty, env'
| None -> None, env') | None -> None, env')
(* Directly the type *)
| Some ty, _ -> Some ty, env
(* Bad typed *) (* Bad typed *)
| None, _ -> None, env) | _ -> None, env)
| Term.Fun (id, body) -> | Term.Fun (id, body) ->
let arg = TypeSubstitution.singleton id (Type.Var id) in let arg = TypeSubstitution.singleton id (Type.Var id) in
(match infer (TypeSubstitution.compose arg env) body with (match infer (TypeSubstitution.compose arg env) body with

9
test/test_projet_pfa_23_24.ml
View file

@ -55,12 +55,19 @@ let tests_typeof =
( "(fun x -> fst x) (1, 2)" ( "(fun x -> fst x) (1, 2)"
, Term.(App (Fun (x, Proj (First, Var x)), Pair (IntConst 1, IntConst 2))) , Term.(App (Fun (x, Proj (First, Var x)), Pair (IntConst 1, IntConst 2)))
, Some Type.Int ) , Some Type.Int )
; (* Function application with nested pair and projection *) ; (* Bad Application on a function application with nested pair and projection *)
( "(fun x -> fst (snd x)) ((1, 2), 3)" ( "(fun x -> fst (snd x)) ((1, 2), 3)"
, Term.( , Term.(
App App
( Fun (x, Proj (First, Proj (Second, Var x))) ( Fun (x, Proj (First, Proj (Second, Var x)))
, Pair (Pair (IntConst 1, IntConst 2), IntConst 3) )) , Pair (Pair (IntConst 1, IntConst 2), IntConst 3) ))
, None )
; (* Function application with nested pair and projection *)
( "(fun x -> fst (snd x)) ((1, 2), (3, 2))"
, Term.(
App
( Fun (x, Proj (First, Proj (Second, Var x)))
, Pair (Pair (IntConst 1, IntConst 2), Pair (IntConst 3, IntConst 2)) ))
, Some Type.Int ) , Some Type.Int )
(* ; (* x -> y -> (x -> y -> z) -> z *) (* ; (* x -> y -> (x -> y -> z) -> z *)
( "fun x -> fun y -> fun z -> z x y" ( "fun x -> fun y -> fun z -> z x y"