New syntax to introduce flexible variables.

This commit is contained in:
Olivier 2023-03-05 18:42:16 +01:00
parent 831ad5e504
commit d930badf40
9 changed files with 47 additions and 15 deletions

View File

@ -281,8 +281,8 @@ let get_loc t =
match t with
| ML.Var (pos, _) | ML.Hole (pos, _) | ML.Abs (pos, _, _)
| ML.App (pos, _, _) | ML.Let (pos, _, _, _, _) | ML.Annot (pos, _, _)
| ML.For (pos, _, _) | ML.Tuple (pos, _) | ML.LetProd (pos, _, _, _)
| ML.Variant (pos, _, _) | ML.Match (pos, _, _)
| ML.For (pos, _, _) | ML.Some_ (pos, _, _) | ML.Tuple (pos, _)
| ML.LetProd (pos, _, _, _) | ML.Variant (pos, _, _) | ML.Match (pos, _, _)
-> pos
let correlate loc c =
@ -430,10 +430,8 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
begin match annot with
| (_, [], ty) ->
convert_annot typedecl_env rigid_env [] w t ty
| (ML.Flexible, vs, ty) ->
let@ params =
vs |> mapM_now (fun alpha k -> let@ v = exist in k (alpha, v)) in
convert_annot typedecl_env rigid_env params w t ty
| (ML.Flexible, _vs, _ty) ->
assert false
| (ML.Rigid, _, _) ->
assert false
end
@ -462,6 +460,14 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
in
F.ftyapp ~loc (coerce ~loc alphas betas (F.ftyabs ~loc alphas t')) tys
| ML.Some_ (_, tyvars, t) ->
let on_tyvar alpha k =
let@ v = exist in k (alpha, v)
in
let@ new_bindings = mapM_now on_tyvar tyvars in
let rigid_env' = new_bindings @ rigid_env in
hastype rigid_env' t w
| ML.Tuple (loc, ts) ->
let on_term (t:ML.term) : ('b * 'c co, 'r) binder =
fun (k : ('b * 'c co) -> 'r co) : 'r co ->

View File

@ -39,6 +39,7 @@ type term =
| App of loc * term * term
| Let of loc * recursive_status * tevar * term * term
| For of loc * tyvar list * term
| Some_ of loc * tyvar list * term
| Annot of loc * term * type_annotation
| Tuple of loc * term list
| LetProd of loc * tevar list * term * term

View File

@ -82,6 +82,8 @@ let term_abs :=
| FOR ; tyvars = list(tyvar) ; IN ; t = term_abs ;
{ For (Some $loc, tyvars, t) }
| SOME ; tyvars = list(tyvar) ; IN ; t = term_abs ;
{ Some_ (Some $loc, tyvars, t) }
| ~ = term_app ; <>
let term_app :=
@ -120,8 +122,11 @@ let term_atom :=
| (Rigid, tyvars, ty) ->
For (Some $loc, tyvars,
Annot (Some $loc, t, (Flexible, [], ty)))
| _ ->
Annot (Some $loc, t, tyannot) }
| (Flexible, [], ty) ->
Annot (Some $loc, t, (Flexible, [], ty))
| (Flexible, tyvars, ty) ->
Some_ (Some $loc, tyvars,
Annot (Some $loc, t, (Flexible, [], ty))) }
| "(" ; ~ = term ; ")" ; <>

View File

@ -43,6 +43,8 @@ let rec translate_term (t : ML.term) : P.term =
P.Annot (self t, translate_annot tyannot)
| ML.For (_, tyvars, t) ->
P.For (tyvars, self t)
| ML.Some_ (_, tyvars, t) ->
P.Some_ (tyvars, self t)
| ML.Tuple (_, ts) ->
P.Tuple (List.map translate_term ts)
| ML.LetProd (_, xs, t, u) ->

View File

@ -29,6 +29,7 @@ type term =
| App of term * term
| Let of recursive_status * pattern * term * term
| For of tyvar list * term
| Some_ of tyvar list * term
| Annot of term * type_annotation
| TyAbs of tyvar * term
| TyApp of term * typ

View File

@ -158,12 +158,18 @@ let print_annot print_elem (rigidity, tyvars, typ) =
^//^ print_type typ
) rparen
let print_tyvars_introduction tyvars print_elem =
string "for" ^^ space
let print_tyvars_introduction kwd tyvars print_elem =
string kwd ^^ space
^^ separate_map space print_tyvar tyvars ^^ space
^^ string "in"
^^ prefix 0 1 empty print_elem
let print_rigid_introduction tyvars print_elem =
print_tyvars_introduction "for" tyvars print_elem
let print_flexible_introduction tyvars print_elem =
print_tyvars_introduction "some" tyvars print_elem
let rec print_term t =
print_term_abs t
@ -178,7 +184,9 @@ and print_term_abs t =
(print_term t1)
(print_term_abs t2)
| For (tyvars, t) ->
print_tyvars_introduction tyvars (print_term t)
print_rigid_introduction tyvars (print_term t)
| Some_ (tyvars, t) ->
print_flexible_introduction tyvars (print_term t)
| Abs _ ->
let (ps, t) = flatten_abs t in
print_nary_abstraction "fun" print_pattern ps (print_term_abs t)
@ -229,7 +237,8 @@ and print_term_atom t =
dot
| TyAbs _ | Let _ | Abs _ | Use _
| TyApp _ | App _ | Proj _ | Inj _
| Variant _ | Refl _ | For _ as t ->
| Variant _ | Refl _ | For _
| Some_ _ as t ->
parens (print_term t)
and print_match ty scrutinee brs =

View File

@ -63,7 +63,8 @@ let let_pair self k n =
let annot self k n =
let+ t = self (k, n - 1) in
ML.Annot (None, t, (ML.Flexible, ["'a"], ML.TyVar (None, "'a")))
ML.Some_ (None, ["'a"],
ML.Annot (None, t, (ML.Flexible, [], ML.TyVar (None, "'a"))))
let term = fix (fun self (k, n) ->
if n = 0 then begin

View File

@ -541,8 +541,9 @@ let test_id_rigid () =
let test_id_flexible () =
test_ok
"(fun x -> x : some 'a 'b. 'a -> 'b)"
(id_annot (ML.Flexible, ["'a"; "'b"], ML.TyArrow (None, alpha, beta)))
"some 'a 'b in (fun x -> x : 'a -> 'b)"
(ML.Some_ (None, ["'a"; "'b"],
id_annot (ML.Flexible, [], ML.TyArrow (None, alpha, beta))))
let test_suite =
let open Alcotest in

View File

@ -39,6 +39,8 @@ module Shrinker = struct
ML.Annot (pos, subst t x u, ty)
| ML.For (pos, tyvars, t) ->
ML.For (pos, tyvars, subst t x u)
| ML.Some_ (pos, tyvars, t) ->
ML.Some_ (pos, tyvars, subst t x u)
| ML.Variant (pos, ty, t) ->
ML.Variant (pos, ty, Option.map (fun t -> subst t x u) t)
| ML.Match (pos, t, brs) ->
@ -162,6 +164,10 @@ module Shrinker = struct
let+ t' = shrink_term t in
ML.For (pos, tyvars, t')
| ML.Some_ (pos, tyvars, t) ->
let+ t' = shrink_term t in
ML.Some_ (pos, tyvars, t')
| ML.Variant (pos, lab, t) ->
subterms (Option.to_list t)
<+> (