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

fix issue with variable handling

Browse source
This commit is contained in:
Mylloon 2024-04-27 12:34:15 +02:00
parent fd68a06c08
commit ae73de8f64
Signed by: Anri
GPG key ID: A82D63DFF8D1317F
1 changed files with 3 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
lib/inference.ml
View file

@ -1,11 +1,7 @@
(** Infer the type of a given term and, if exists, returns the type of the term *) (** Infer the type of a given term and, if exists, returns the type of the term *)
let typeof t = let typeof t =
let rec infer env = function let rec infer env = function
| Term.Var id -> | Term.Var id -> TypeSubstitution.find id env, env
( (match TypeSubstitution.find id env with
| Some ty -> Some ty
| None -> Some (Type.Var id))
, env )
| Term.IntConst _ -> Some Type.Int, env | Term.IntConst _ -> Some Type.Int, env
| Term.Binop (t1, _, t2) -> | Term.Binop (t1, _, t2) ->
(* Both operands must have type Int *) (* Both operands must have type Int *)
@ -28,7 +24,8 @@ let typeof t =
| Term.Second -> Some ty2, env) | Term.Second -> Some ty2, env)
| _ -> None, env) | _ -> None, env)
| Term.Fun (id, body) -> | Term.Fun (id, body) ->
(match infer env body with let arg = TypeSubstitution.singleton id (Type.Var id) in
(match infer (TypeSubstitution.compose env arg) body with
| Some ty_body, env' -> | Some ty_body, env' ->
(match infer env' (Term.Var id) with (match infer env' (Term.Var id) with
| Some ty, _ -> Some (Type.Arrow (ty, ty_body)), env' | Some ty, _ -> Some (Type.Arrow (ty, ty_body)), env'