From 5ed12f0cdf498abf74d97b70d6105440860e3813 Mon Sep 17 00:00:00 2001 From: Mysaa Date: Mon, 11 Mar 2024 17:52:04 +0100 Subject: [PATCH] Added all type inference --- src/Infer.ml | 99 ++++++++++++++++++++++++++---------- tests.t/tuple-inversion.test | 1 + 2 files changed, 74 insertions(+), 26 deletions(-) create mode 100644 tests.t/tuple-inversion.test diff --git a/src/Infer.ml b/src/Infer.ml index 358152b..38d2cbc 100644 --- a/src/Infer.ml +++ b/src/Infer.ml @@ -30,14 +30,6 @@ module Make(T : Utils.Functor) = struct let eq v1 v2 = Eq(v1, v2) let decode v = MapErr(Decode v, fun e -> Cycle e) - let assume_pair = function - | [v1; v2] -> (v1, v2) - | other -> - Printf.ksprintf failwith - "Error: this implementation currently only supports pairs, - not tuples of size %d." - (List.length other) - (** This is a helper function to implement constraint generation for the [Annot] construct. @@ -51,11 +43,12 @@ module Make(T : Utils.Functor) = struct [∃(?w1 = ?v2 -> ?v3). ∃(?w2 = ?v1 -> ?w1). k ?w2], or equivalently [∃?w3 ?w4. ?w3 = ?v1 -> ?w4 ∧ ?w4 = ?v2 -> ?v3 ∧ k ?w3]. *) - let rec bind (ty : STLC.ty) (k : Constraint.variable -> ('a, 'e) t) : ('a, 'e) t = - (* Feel free to postpone implementing this function - until you implement the Annot case below. *) + let rec bind : type a . STLC.ty -> (Constraint.variable -> (a, err) t) -> (a, err) t = + fun ty k -> match ty with - | Constr Var x -> k x + | Constr Var x -> + let w = Var.fresh "w" in + Exist(w,Some (Var x),k w) | Constr Arrow (ta,tb) -> let w,ap,bp = Var.fresh "w",Var.fresh "a",Var.fresh "b" in Exist(ap,None, @@ -77,7 +70,6 @@ module Make(T : Utils.Functor) = struct List.fold_right (fun (tt,av) con -> Map(Conj(bind tt (fun x -> eq x av),con),fun ((),t) -> t)) arr ( Exist(w,Some (Structure.Prod (List.map snd arr)),k w) )) - end (** This function generates a typing constraint from an untyped term: [has_type env t w] generates a constraint [C] which contains [w] as @@ -112,36 +104,91 @@ module Make(T : Utils.Functor) = struct Exist(a, None, Ret (fun _ -> STLC.Var(x))) ) ~some:( - fun envt -> Map(eq envt w, fun _ -> STLC.Var(x)) + fun envt -> Map(eq envt w, fun () -> STLC.Var(x)) ) (Env.find_opt x env) ) | Untyped.App (t, u) -> - Utils.not_yet "Infer.has_type: App case" (env, t, u, fun () -> has_type) + let a,b,tau = Var.fresh "a", Var.fresh "b", Var.fresh "τ" in + Exist(a,None, + Exist(b,None, + Exist(tau,Some (Arrow(a,b)), + Map( + Conj(has_type env t tau,has_type env u a), + fun (tt,uu) -> App(tt,uu) + )))) | Untyped.Abs (x, t) -> let tau,a,b = Var.fresh "τ",Var.fresh "α", Var.fresh "β" in let newenv = Env.add x a env in - Exist(tau, Some (Arrow(a, b)), + Exist(a,None, + Exist(b,None, Map( Conj( Conj( has_type newenv t b, - eq tau w + Exist(tau,Some (Arrow (a,b)),eq tau w) ), - decode tau + decode a ), - fun ((tt,()),ty) -> Abs(x, ty, tt)) - ) + fun ((tt,()),ty) -> STLC.Abs(x, ty, tt)) + )) | Untyped.Let (x, t, u) -> - Utils.not_yet "Infer.has_type: Let case" (env, x, t, u, fun () -> has_type) + let a,b = Var.fresh "α", Var.fresh "β" in + let newenv = Env.add x a env in + Exist(a,None, + Exist(b,None, + Map( + Conj( + Conj( + Conj( + has_type env t a, + has_type newenv u b + ), + eq w b + ), + decode a + ), + fun (((tt,uu),()),ta) -> STLC.Let(x,ta,tt,uu)) + )) | Untyped.Annot (t, ty) -> - bind (fun w -> has_type env w) ty + Map( + bind ty (fun w -> has_type env t w), + fun tt -> STLC.Annot(tt,ty) + ) | Untyped.Tuple ts -> - let (t1, t2) = assume_pair ts in - Utils.not_yet "Infer.has_type: Tuple case" (env, t1, t2, fun () -> has_type) + let ww = Var.fresh "w" in + let arr = List.map (fun tt -> (tt,Var.fresh "t")) ts in (*On crée une variable par indice du tuple*) + List.fold_right (fun (_,ap) con -> Exist(ap,None,con)) arr ( (*On quantifie sur leur existence*) + Map( + (List.fold_right (fun (tt,av) con -> Map(Conj(has_type env tt av,con),fun (tt,tl) -> tt::tl)) arr ( (* Que chaque membre a le type attendu *) + Map( + Exist(ww,Some (Prod (List.map snd arr)), + eq w ww + ), + fun () -> [] + ) + )), + fun tl -> STLC.Tuple(tl) + ) + ) | Untyped.LetTuple (xs, t, u) -> - let (x1, x2) = assume_pair xs in - Utils.not_yet "Infer.has_type: LetTuple case" (env, x1, x2, t, u, fun () -> has_type) + let a = Var.fresh "a" in + let arr = List.map (fun x -> (x,Var.fresh "t")) xs in (*On crée une variable par variable du tuple*) + let newenv = List.fold_right (fun (x,ta) acc -> Env.add x ta acc) arr env in + List.fold_right (fun (_,ap) con -> Exist(ap,None,con)) arr ( (*On quantifie sur leur existence*) + Map( + List.fold_right (fun (_,tx) acc -> Map(Conj(decode tx,acc),fun (ttx,(tta,ttb,ttl)) -> (tta,ttb,ttx::ttl))) arr ( + Map( + Conj( + Exist(a,Some (Prod (List.map snd arr)),has_type env t a), + has_type newenv u w + ), + fun (tta,ttb) -> (tta,ttb,[]) + ) + ), + fun (tta,ttb,ttl) -> STLC.LetTuple(List.map2 (fun x y -> (x,y)) xs ttl,tta,ttb) + ) + ) | Do p -> (* Feel free to postone this until you start looking at random generation. Getting type inference to diff --git a/tests.t/tuple-inversion.test b/tests.t/tuple-inversion.test new file mode 100644 index 0000000..a9a608a --- /dev/null +++ b/tests.t/tuple-inversion.test @@ -0,0 +1 @@ +lambda p. let (x,y,z) = p in (z,y,x)