Mysaa/mpri-2.4-project-2023-2024
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Added annotation, but not working

Browse Source
This commit is contained in:
Mysaa 2024-03-10 20:51:14 +01:00
parent 1fc5a46904
commit 5caeca79ff
Signed by: Mysaa
GPG Key ID: 7054D5D6A90F084F
1 changed files with 37 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

46
src/Infer.ml
View File

@ -54,7 +54,30 @@ module Make(T : Utils.Functor) = struct
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. *)
Utils.not_yet "Infer.bind" (ty, k, fun () -> bind)
match ty with
| Constr Var x -> k x
| Constr Arrow (ta,tb) ->
let w,ap,bp = Var.fresh "w",Var.fresh "a",Var.fresh "b" in
Exist(ap,None,
Exist(bp,None,
Map(
Conj(
bind ta (fun x -> eq x ap),
Conj(
bind tb (fun x -> eq x bp),
Exist(w,Some (Structure.Arrow (ap,bp)),k w)
)
),
fun ((),((),t)) -> t
)))
| Constr Prod l ->
let w = Var.fresh "w" in
let arr = List.map (fun ty -> (ty,Var.fresh "t")) l in
List.fold_right (fun (_,ap) con -> Exist(ap,None,con)) arr (
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
@ -99,24 +122,29 @@ module Make(T : Utils.Functor) = struct
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)),
Map(Conj(
has_type newenv t b,
eq tau w
), fun t -> let (x,_) = p in x) (* term * unit -> term isomorphism *)
Map(
Conj(
Conj(
has_type newenv t b,
eq tau w
),
decode tau
),
fun ((tt,()),ty) -> Abs(x, ty, tt))
)
| Untyped.Let (x, t, u) ->
Utils.not_yet "Infer.has_type: Let case" (env, x, t, u, fun () -> has_type)
| Untyped.Annot (t, ty) ->
Utils.not_yet "Infer.has_type: Let case" (env, t, ty, bind, fun () -> has_type)
bind (fun w -> has_type env w) ty
| Untyped.Tuple ts ->
let (t1, t2) = assume_pair ts in
Utils.not_yet "Infer.has_type: Let case" (env, t1, t2, fun () -> has_type)
Utils.not_yet "Infer.has_type: Tuple case" (env, t1, t2, fun () -> has_type)
| Untyped.LetTuple (xs, t, u) ->
let (x1, x2) = assume_pair xs in
Utils.not_yet "Infer.has_type: Let case" (env, x1, x2, t, u, fun () -> has_type)
Utils.not_yet "Infer.has_type: LetTuple case" (env, x1, x2, t, u, fun () -> has_type)
| Do p ->
(* Feel free to postone this until you start looking
at random generation. Getting type inference to
work on all the other cases is a good first step. *)
Utils.not_yet "Infer.has_type: Let case" (env, p, fun () -> has_type)
Utils.not_yet "Infer.has_type: Do case" (env, p, fun () -> has_type)
end