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

fix arg inference

Browse source
This commit is contained in:
Mylloon 2024-04-30 12:02:14 +02:00
parent 9c41888ec1
commit 5daa03cb1a
Signed by: Anri
GPG key ID: A82D63DFF8D1317F
1 changed files with 7 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
lib/inference.ml
View file

@ -30,7 +30,7 @@ let typeof t =
| _ -> None, env)
| Term.Fun (id, body) ->
let arg = TypeSubstitution.singleton id (Type.Var id) in
(match infer (TypeSubstitution.compose env arg) body with
(match infer (TypeSubstitution.compose arg env) body with
| Some ty_body, env' ->
(match infer env' (Term.Var id) with
| Some ty, _ -> Some (Type.Arrow (ty, ty_body)), env'
@ -39,10 +39,14 @@ let typeof t =
| Term.App (t1, t2) ->
(* Infer the type of t1 and t2 *)
(match infer env t1, infer env t2 with
| (Some (Type.Arrow (ty_param, ty_fn)), _), (Some ty_args, _) ->
| (Some (Type.Arrow (ty_param, _)), _), (Some ty_args, _) ->
(* Check if the argument type matches the parameter type *)
(match Unification.unify ty_param ty_args with
| Some env' -> Some ty_fn, env'
| Some env' ->
(* Infer again now that we have some extra typing infos *)
(match infer env' t1 with
| Some (Type.Arrow (_, ty_fn)), env'' -> Some ty_fn, env''
| _ -> None, env)
| None -> None, env)
(* | (Some (Type.Var _ as ty1), _), _ ->
(* On this case we may have a function represented as a variable *)