Remove T_abs with (Path = T_sub) and add T_abs & T_sub syntax...

...for type refinement.

The new

    T_abs & T_sub

mechanism is similar to the old

    T_abs with (Path = T_sub)

mechanism and also to the include mechanism

    {...T_abs; ...T_sub}

The main difference is that, instead of using a path to target a specific
substructure or requiring that no declarations overlap, an intersection,
`T_int`, of the nested declarations of `T_abs` and `T_sub`, is computed.

Then it is checked whether `T_abs :> T_int` and if so a substitution, `𝛿`, is
obtained.  Finally the nested declarations of `𝛿(T_abs)` and `T_sub` are merged.

Also, in `T1 & T2` both `T1` and `T2` are elaborated in the same environment
whereas in `{...T1; ...T2}` the environment for `T2` includes declarations from
`T1` and in `T1 with (P = T2)` the path `P` is specific to `T1`.

When defined, `T1 & T2` is always a subtype of both `T1` and `T2`

    T1 & T2  :>  T1
    T1 & T2  :>  T2

README.md

@@ -90,7 +90,7 @@ T ::=
     (X : T) => E            (pure function/functor/constructor type)
     '(X : T) => E           (implicit function/functor/constructor type)
     (= E)                   (singleton/alias type)
-    T with .Xs = E          (type refinement)
+    T & T                   (type refinement)
     wrap T                  (impredicative wrapped type)
     _                       (type wildcard)
     T as T                  (layered type (both operands have to be equal))
@@ -152,8 +152,6 @@ T ::= ...
     T1 => T2                        ~> (_ : T1) => T2
     P -> T                          ~> ($ : TP) -> let P in T  [2]
     P => T                          ~> ($ : TP) => let P in T  [2]
-    T with .Xs A1 ... An = E        ~> T with .Xs = fun A1 ... An => E
-    T with type .Xs A1 ... An = T'  ~> T with .Xs = fun A1 ... An => type T'
     let B in T                      ~> (let B in type T)
     rec P => T                      ~> (rec P => type T)
 

elab.ml

@@ -248,27 +248,29 @@ let rec elab_typ env typ l =
     in
     s1, lift_warn typ.at t1 (add_typs aks1 env) (zs1 @ zs2 @ zs3)
 
-  | EL.WithT(typ1, vars, exp) ->
-    let t2, zs2 = elab_pathexp env exp l in
-    let ExT(aks1, t1), zs1 = elab_typ env typ1 l in
-    let ls = List.map (fun var -> var.it) vars in
-Trace.debug (lazy ("[WithT] s1 = " ^ string_of_norm_extyp (ExT(aks1, t1))));
-Trace.debug (lazy ("[WithT] ls = " ^ String.concat "." ls));
-Trace.debug (lazy ("[WithT] t2 = " ^ string_of_norm_typ t2));
-    let ta = try project_typ ls t1 with Not_found ->
-      error typ.at ("path " ^ quote (String.concat "." ls) ^ " unbound") in
-Trace.debug (lazy ("[WithT] ta = " ^ string_of_norm_typ ta));
-    let bs = vars_typ ta in
-    let aks11 = List.filter (fun (a, k) -> not (VarSet.mem a bs)) aks1 in
-    let aks12 = List.filter (fun (a, k) -> VarSet.mem a bs) aks1 in
-Trace.debug (lazy ("[WithT] aks11 = " ^ string_of_norm_extyp (ExT(aks11, StrT []))));
-Trace.debug (lazy ("[WithT] aks12 = " ^ string_of_norm_extyp (ExT(aks12, StrT []))));
+  | EL.AndT(typ1, typ2) ->
+    let s1', zs1 = elab_typ env typ1 l in
+    let s2', zs2 = elab_typ env typ2 l in
+    let ExT(aks1, t1) as s1 = freshen_extyp env s1' in
+    let ExT(aks2, t2) as s2 = freshen_extyp (add_typs aks1 env) s2' in
+Trace.debug (lazy ("[AndT] s1 = " ^ string_of_norm_extyp s1));
+Trace.debug (lazy ("[AndT] s2 = " ^ string_of_norm_extyp s2));
+    let ti = intersect_typs t1 t2 in
+Trace.debug (lazy ("[AndT] ti = " ^ string_of_norm_typ ti));
+    let vi = vars_typ ti in
+    let aksi = List.filter (fun (a, k) -> VarSet.mem a vi) aks1 in
+Trace.debug (lazy ("[AndT] aksi = " ^ string_of_norm_extyp (ExT(aksi, StrT []))));
+    let aks = aks1 @ aks2 in
     let ts, zs3, _ =
-      try sub_typ env t2 ta (varTs aks12) with Sub e -> error exp.at
-        ("refinement type does not match type component: " ^ Sub.string_of_error e)
-    in
-    ExT(aks11, subst_typ (subst aks12 ts) t1),
-    lift_warn typ.at t1 (add_typs aks11 env) (zs1 @ zs2 @ zs3)
+      try sub_typ (add_typs aks env) t2 ti (varTs aksi) with Sub e ->
+        error typ.at ("type refinement does not match: " ^ Sub.string_of_error e) in
+Trace.debug (lazy ("[AndT] ts = " ^ String.concat ", " (List.map string_of_norm_typ ts)));
+    let t = merge_typs (subst_typ (subst (Lib.List.take (List.length ts) aksi) ts) t1) t2 in
+Trace.debug (lazy ("[AndT] t = " ^ string_of_norm_typ t));
+    let vt = vars_typ t in
+    let s = ExT(List.filter (fun (a, k) -> VarSet.mem a vt) aks, t) in
+Trace.debug (lazy ("[AndT] s = " ^ string_of_norm_extyp s));
+    s, lift_warn typ.at t env (zs1 @ zs2 @ zs3)
 
 and elab_dec env dec l =
   Trace.elab (lazy ("[elab_dec] " ^ EL.label_of_dec dec));

lexer.mll

@@ -85,7 +85,7 @@ rule token = parse
   | "then" { THEN }
   | "type" { TYPE }
   | "unwrap" { UNWRAP }
-  | "with" { WITH }
+  | "&" { AMP }
   | "@" { AT }
   | "=" { EQUAL }
   | ":" { COLON }

paper.1ml

@@ -71,7 +71,7 @@ type MAP =
   lookup (a : type) : key -> map a -> opt a;
 };
 
-Map (Key : EQ) :> MAP with (type key = Key.t) =
+Map (Key : EQ) :> MAP & {key = Key.t} =
 {
   type key = Key.t;
   type map a = key -> opt a;
@@ -154,7 +154,7 @@ joinM (M : MONAD) (a : type) (mm : M.t (M.t a)) : M.t a =
   M.bind (M.t a) a mm (fun (m : M.t a) => m);
 
 StackM (M : MONAD) =
-  rec (Loop : (n : int) -> (MONAD_TRANS with (base = M.t))) =>
+  rec (Loop : (n : int) -> (MONAD_TRANS & {base = M.t})) =>
   fun (n : int) =>
   if n == 1 then
     { include M;
@@ -175,7 +175,7 @@ StackM (M : MONAD) =
           (fun (mx : M.t a) => M.bind a b mx
             (fun (x : a) => f x));
     }
-  ) : MONAD_TRANS with (type base a = M.t a);
+  ) : MONAD_TRANS & {base = M.t};
 ;)
 
 ;; Predicativity
@@ -227,7 +227,7 @@ type MAP =
   lookup 'a : key -> map a -> opt a;
   add 'a : key -> a -> map a -> map a
 };
-Map (Key : EQ) :> MAP with (type key = Key.t) =
+Map (Key : EQ) :> MAP & {key = Key.t} =
 {
   type key = Key.t;
   type map a = key -> opt a;

parser.mly

@@ -28,8 +28,7 @@ let parse_error s = raise (Source.Error (Source.nowhere_region, s))
 %token HOLE PRIMITIVE
 %token FUN REC LET IN DO WRAP UNWRAP TYPE ELLIPSIS
 %token IF THEN ELSE LOGICAL_OR LOGICAL_AND AS
-%token EQUAL COLON SEAL ARROW DARROW
-%token WITH
+%token EQUAL COLON SEAL ARROW DARROW AMP
 %token LPAR RPAR
 %token LBRACE RBRACE
 %token DOT AT TICK
@@ -67,12 +66,6 @@ name :
   | LPAR sym RPAR
     { $2 }
 ;
-namelist :
-  | name
-    { $1::[] }
-  | name DOT namelist
-    { $1::$3 }
-;
 
 head :
   | name
@@ -145,20 +138,18 @@ apptyp :
   | pathexp
     { PathT($1)@@at() }
 ;
-withtyp :
+andtyp :
   | apptyp
     { $1 }
-  | withtyp WITH LPAR namelist typparamlist EQUAL exp RPAR
-    { WithT($1, $4, funE($5, $7)@@span[ati 5; ati 7])@@at() }
-  | withtyp WITH LPAR TYPE namelist typparamlist EQUAL typ RPAR
-    { WithT($1, $5, funE($6, TypE($8)@@ati 8)@@span[ati 6; ati 8])@@at() }
+  | apptyp AMP andtyp
+    { AndT($1, $3)@@at() }
 ;
 typ :
-  | withtyp
+  | andtyp
     { $1 }
   | annparam arrow typ
     { funT([$1], $3, $2)@@at() }
-  | withtyp arrow typ
+  | andtyp arrow typ
     { let b, _ = varP("_"@@ati 1) in
       funT([(b, $1, Expl@@ati 2)@@ati 1], $3, $2)@@at() }
   | WRAP typ

prelude.1ml

@@ -222,7 +222,7 @@ type SET =
   card : set -> int;
 };
 
-Set (Elem : ORD) :> SET with (elem = Elem.t) =
+Set (Elem : ORD) :> SET & {elem = Elem.t} =
 {
   type elem = Elem.t;
   (==) x y = let ...Elem in (x <= y) && (y <= x);
@@ -249,7 +249,7 @@ type MAP =
   lookup 'a : key -> map a -> opt a;
 };
 
-Map (Key : ORD) :> MAP with (key = Key.t) =
+Map (Key : ORD) :> MAP & {key = Key.t} =
 {
   type key = Key.t;
   (==) x y = let ...Key in (x <= y) && (y <= x);

regression.1ml

@@ -32,6 +32,28 @@ Equivalence: {
 
 ;;
 
+ExpressiveLanguageOfSignatures = {
+  type T = {type t; type u; x: t};
+  type V = {type t; type u; x: u};
+
+  type_error { type L = T & V };
+
+  type L1 = T & V & {type t; u = t};
+  type L2 = T & V & {x 'a: a};
+};
+
+And = {
+  type Reveal = {type t; x: t} & {t = int};
+  type Nested = {Nested: {type t; v: t}; x: Nested.t} & {Nested: {t = int}};
+  type RevealWithPath = {type t; toText: t -> text} & (= Int);
+
+  type RDS = {A: {type t}; B: {type t}}
+  &          {A: {type t}; B: {v: A.t}}
+  &          {B: {type t}; A: {v: B.t}};
+};
+
+;;
+
 hole_is_allowed_type_pattern (type _ _) = ();
 
 typparams_allowed (id 'a: a => a) ({alsoId 'x: x => x}) =

syntax.ml

@@ -27,7 +27,7 @@ and typ' =
   | WrapT of typ
   | EqT of exp
   | AsT of typ * typ
-  | WithT of typ * var list * exp
+  | AndT of typ * typ
 
 and dec = (dec', unit) phrase
 and dec' =
@@ -354,7 +354,7 @@ let label_of_typ t =
   | WrapT _ -> "WrapT"
   | EqT _ -> "EqT"
   | AsT _ -> "AsT"
-  | WithT _ -> "WithT"
+  | AndT _ -> "AndT"
 
 let label_of_dec d =
   match d.it with
@@ -407,8 +407,8 @@ let rec string_of_typ t =
   | WrapT(t) -> node' [string_of_typ t]
   | EqT(e) -> node' [string_of_exp e]
   | AsT(t1, t2) -> node' [string_of_typ t1; string_of_typ t2]
-  | WithT(t, xs, e) ->
-    node' ([string_of_typ t] @ List.map string_of_var xs @ [string_of_exp e])
+  | AndT(t1, t2) ->
+    node' [string_of_typ t1; string_of_typ t2]
 
 and string_of_dec d =
   let node' = node (label_of_dec d) in

talk.1ml

@@ -37,7 +37,7 @@ type MAP =
   add a : key -> a -> map a -> map a;
 };
 
-Map (Key : EQ) :> MAP with (type key = Key.t) =
+Map (Key : EQ) :> MAP & {key = Key.t} =
 {
   type key = Key.t;
   type map a = key -> opt a;
@@ -59,7 +59,7 @@ type MAP =
   add 'a : key -> a -> map a -> map a;
 };
 
-Map (Key : EQ) :> MAP with (type key = Key.t) =
+Map (Key : EQ) :> MAP & {key = Key.t} =
 {
   type key = Key.t;
   type map a = key -> opt a;

test.1ml

@@ -229,7 +229,7 @@ type SET =
   card : set -> int;
 };
 
-Set (Elem : ORD) :> SET with (elem = Elem.t) =
+Set (Elem : ORD) :> SET & {elem = Elem.t} =
 {
   type elem = Elem.t;
   type set = (int, elem -> bool);
@@ -254,7 +254,7 @@ type MAP =
   lookup 'a : key -> map a -> opt a;
 };
 
-Map (Key : ORD) :> MAP with (key = Key.t) =
+Map (Key : ORD) :> MAP & {key = Key.t} =
 {
   type key = Key.t;
   type map a = key -> opt a;

types.ml

@@ -111,12 +111,53 @@ let intersect_row r1 r2 =
 let diff_row r1 r2 =
   List.filter (fun (l1, _) -> List.for_all (fun (l2, _) -> l1 <> l2) r2) r1
 
-let rec project_typ ls t =
-  match ls, t with
-  | [], _ -> t
-  | l::ls', StrT(tr) -> project_typ ls' (List.assoc l tr)
-  | _ -> raise Not_found
-
+let rec intersect_typs t1 t2 =
+  match t1, t2 with
+  | StrT(r1), StrT(r2) ->
+    StrT(intersect_row r1 r2
+         |> List.map (fun (l, t1) ->
+                (l, intersect_typs t1 (List.assoc l r2))))
+  | _ ->
+    t1
+
+let rec has_typs = function
+  | VarT(_) -> false
+  | PrimT(_) -> false
+  | StrT(tr) -> List.exists (fun (_, t) -> has_typs t) tr
+  | FunT(aks, td, ExT(_, tr), e) ->
+    (match e with
+     | Implicit | Explicit Pure ->
+       has_typs tr
+     | Explicit Impure -> false)
+  | TypT(ExT(_, p)) -> true
+  | WrapT(_) -> false
+  | LamT(_) -> false
+  | AppT(_) -> false
+  | TupT(_) -> false
+  | DotT(_) -> false
+  | RecT(_) -> false
+  | InferT(_) -> false
+
+let rec merge_typs t1 t2 =
+  match t1, t2 with
+  | StrT(r1), StrT(r2) ->
+    let ls = List.map fst r1 @
+      List.filter (fun l -> not (List.mem_assoc l r1)) (List.map fst r2) in
+    let merge kind =
+      ls
+      |> List.filter (fun l ->
+          List.mem_assoc l r1 && kind (List.assoc l r1) ||
+          List.mem_assoc l r2 && kind (List.assoc l r2))
+      |> List.map (fun l ->
+          if List.mem_assoc l r1 && List.mem_assoc l r2 then
+            (l, merge_typs (List.assoc l r1) (List.assoc l r2))
+          else if List.mem_assoc l r2 then
+            (l, List.assoc l r2)
+          else
+            (l, List.assoc l r1)) in
+    StrT(merge has_typs @ merge (fun t -> not (has_typs t)))
+  | _ ->
+    t2
 
 (* Size check *)
 

types.mli

@@ -97,8 +97,8 @@ val map_rowi : (lab -> 'a -> 'b) -> 'a row -> 'b row
 val intersect_row : 'a row -> 'a row -> 'a row
 val diff_row : 'a row -> 'a row -> 'a row
 
-val project_typ : lab list -> typ -> typ (* raise Not_found *)
-
+val intersect_typs : typ -> typ -> typ
+val merge_typs : typ -> typ -> typ
 
 (* Size check *)