Commit 8d89520d authored by SCHERER Gabriel's avatar SCHERER Gabriel
Browse files

Merge branch 'F-annot' into 'master'

Add annotations to System F

See merge request !28
parents 763c61b3 a1d83bd9
Pipeline #262640 passed with stage
in 8 minutes and 5 seconds
......@@ -53,6 +53,7 @@ type tevar = string
type ('a, 'b) term =
| Var of tevar
| Hole of ('a, 'b) typ * ('a, 'b) term list
| Annot of ('a, 'b) term * ('a, 'b) typ
| Abs of tevar * ('a, 'b) typ * ('a, 'b) term
| App of ('a, 'b) term * ('a, 'b) term
| Let of tevar * ('a, 'b) term * ('a, 'b) term
......@@ -69,6 +70,7 @@ and ('a,'b) branch = ('a,'b) pattern * ('a,'b) term
and ('a,'b) pattern =
| PVar of tevar
| PAnnot of ('a, 'b) pattern * ('a, 'b) typ
| PWildcard
| PInj of (('a,'b) typ list) * int * ('a,'b) pattern
| PTuple of ('a,'b) pattern list
......@@ -174,6 +176,10 @@ module TypeInTerm : DeBruijn.TRAVERSE
let ty' = TypeInType.traverse lookup extend env ty in
let ts' = List.map (trav env) ts in
Hole (ty', ts')
| Annot (t, ty) ->
let t' = trav env t
and ty' = TypeInType.traverse lookup extend env ty in
Annot (t', ty')
| Abs (x, ty, t) ->
let ty' = TypeInType.traverse lookup extend env ty
and t' = trav env t in
......@@ -232,6 +238,10 @@ module TypeInTerm : DeBruijn.TRAVERSE
PVar x
| PWildcard ->
PWildcard
| PAnnot (p, ty) ->
let p' = trav env p
and ty' = TypeInType.traverse lookup extend env ty in
PAnnot (p', ty')
| PInj (tys, i, pat) ->
let tys' = List.map (TypeInType.traverse lookup extend env) tys
and pat' = trav env pat in
......
......@@ -57,6 +57,7 @@ type tevar =
type ('a, 'b) term =
| Var of tevar
| Hole of ('a, 'b) typ * ('a, 'b) term list
| Annot of ('a, 'b) term * ('a, 'b) typ
| Abs of tevar * ('a, 'b) typ * ('a, 'b) term
| App of ('a, 'b) term * ('a, 'b) term
| Let of tevar * ('a, 'b) term * ('a, 'b) term
......@@ -73,6 +74,7 @@ and ('a,'b) branch = ('a,'b) pattern * ('a,'b) term
and ('a,'b) pattern =
| PVar of tevar
| PAnnot of ('a, 'b) pattern * ('a, 'b) typ
| PWildcard
| PInj of (('a,'b) typ list) * int * ('a,'b) pattern
| PTuple of ('a,'b) pattern list
......
......@@ -40,6 +40,8 @@ let rec translate_term env (t : F.nominal_term) : P.term =
P.Var x
| F.Hole (ty, ts) ->
P.Hole (Some (translate_type env ty), List.map (self env) ts)
| F.Annot (t, ty) ->
P.Annot (self env t, ([], translate_type env ty))
| F.Abs (x, ty, t) ->
let annot = P.PAnnot (P.PVar x, ([], translate_type env ty)) in
P.Abs (annot, self env t)
......@@ -84,6 +86,8 @@ and translate_pattern env pat =
P.PVar x
| F.PWildcard ->
P.PWildcard
| F.PAnnot (p, ty) ->
P.PAnnot (self env p, ([], translate_type env ty))
| F.PInj (tys, i, p) ->
P.PInj (Some (List.map (translate_type env) tys), i, self env p)
| F.PTuple ps ->
......
......@@ -207,6 +207,9 @@ let rec typeof datatype_env env (t : debruijn_term) : debruijn_type =
ignore (typeof env t) in
List.iter on_subterm ts;
ty
| Annot (t, ty) ->
typeof env t -- ty;
ty
| Abs (x, ty1, t) ->
let ty2 = typeof (extend_with_tevar env x ty1) t in
TyArrow (ty1, ty2)
......@@ -278,6 +281,9 @@ and binding_pattern datatype_env scrutinee_ty pat =
singleton x scrutinee_ty
| PWildcard ->
empty
| PAnnot (pat, ty) ->
scrutinee_ty -- ty;
binding_pattern ty pat
| PInj (tys, i, pat) ->
scrutinee_ty -- TySum tys;
let ty' = nth_type (TySum tys) tys i in
......
......@@ -282,12 +282,22 @@ let convert env params ty =
exception VariableConflict of string
let convert_annot env ((flex_vars, ty) : ML.type_annotation)
: (variable, 'r) binder
: (variable * F.nominal_type co, 'r) binder
= fun k ->
let@ params =
flex_vars |> mapM_now (fun alpha k -> let@ v = exist in k (alpha, v)) in
let@ params, witnesses =
flex_vars |> mapM_both (fun alpha k ->
let@ v = exist in
k (
(alpha, v),
let+ ty' = witness v in (alpha, ty'))
)
in
let@ v = convert env params ty in
k v
k (v,
let+ ws = witnesses in
let translate_var alpha = List.assoc alpha ws in
ML2F.translate_type translate_var ty
)
(* -------------------------------------------------------------------------- *)
......@@ -367,10 +377,11 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
u'))
| ML.Annot (t, annot) ->
let@ v = convert_annot typedecl_env annot in
let@ v, annot' = convert_annot typedecl_env annot in
let+ () = v -- w
and+ t' = hastype t v in
t'
and+ t' = hastype t v
and+ annot' = annot' in
F.Annot (t', annot')
| ML.Tuple ts ->
let on_term (t:ML.term) : ('b * 'c co, 'r) binder =
......@@ -515,10 +526,13 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
k ([], pure (F.PWildcard))
| ML.PAnnot (pat, annot) ->
let@ v = convert_annot typedecl_env annot in
let@ v, annot' = convert_annot typedecl_env annot in
let@ (pat_env, pat) = hastype_pat typedecl_env pat v in
let+ () = v -- w
and+ res = k (pat_env, pat)
and+ res = k (pat_env,
let+ pat = pat
and+ annot' = annot'
in F.PAnnot(pat, annot'))
in res
| ML.PTuple pats ->
......
......@@ -8,14 +8,14 @@ let fresh_tyvar =
(* Translation of ML datatype environment into System F datatype environment. *)
(* Given a way to translate ML type variables into System F type variables,
(* Given a way to translate ML type variables into System F type,
this function translates an ML type into a System F type. *)
let rec translate_type (translate_tyvar : ML.tyvar -> F.tyvar) (ty : ML.typ)
let rec translate_type (translate_tyvar : ML.tyvar -> F.nominal_type) (ty : ML.typ)
: F.nominal_type =
let trans ty = translate_type translate_tyvar ty in
match ty with
| ML.TyVar tv ->
F.TyVar (translate_tyvar tv)
translate_tyvar tv
| ML.TyArrow (ty1, ty2) ->
F.TyArrow (trans ty1, trans ty2)
| ML.TyProduct tys ->
......@@ -43,7 +43,7 @@ let translate_datatype tdescr =
ty
in
let new_arg_type =
translate_type (fun tv -> List.assoc tv assoc) arg_type
translate_type (fun tv -> F.TyVar (List.assoc tv assoc)) arg_type
in
Datatype.{
label_name = ldescr.label_name;
......
......@@ -98,6 +98,11 @@ let let_prod k n self = QCheck.Gen.(
in ML.LetProd ([x1; x2], t1, t2)
)
let annot k n self = QCheck.Gen.(
let+ t = self (k, n-1) in
ML.Annot (t, (["'a"], ML.TyVar "'a"))
)
let term_gen = QCheck.Gen.(
fix
(fun self (k, n) ->
......@@ -116,6 +121,7 @@ let term_gen = QCheck.Gen.(
1, tuple k n self ;
1, let_ k n self ;
1, let_prod k n self ;
1, annot k n self ;
]
)
)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment