Typeset grammar and kind TYPESET.

src/compiler/flx_core/flx_ast.ml

@@ -65,7 +65,7 @@ and kindcode_t =
   | KND_function of kindcode_t * kindcode_t 
   | KND_tuple of kindcode_t list
   | KND_tpattern of typecode_t
-  | KND_special of string
+  (* | KND_special of string *)
   | KND_var of string
 
 

src/compiler/flx_core/flx_beta.ml

@@ -12,32 +12,11 @@ open Flx_maps
 open Flx_btype_subst
 open Flx_kind
 
-let rec expand_typeset bsym_table counter sr t = 
-  let fe t = expand_typeset bsym_table counter sr t in
-  match t with
-  | BTYP_type_set ls
-  | BTYP_type_set_union ls ->
-     Flx_list.uniq_list (List.concat (List.map fe ls))
-  | BTYP_inst (`Alias,index,ts,mt) ->
-    begin try 
-       let bsym = Flx_bsym_table.find bsym_table index in
-       let bbdcl = Flx_bsym.bbdcl bsym in
-       begin match bbdcl with
-       | Flx_bbdcl.BBDCL_structural_type_alias (bvs, alias) 
-       | Flx_bbdcl.BBDCL_nominal_type_alias (bvs, alias) ->
-         let alias = Flx_btype_subst.tsubst sr bvs ts alias in
-         let alias = beta_reduce "Flx_beta:expand_typeset" counter bsym_table bsym.Flx_bsym.sr alias in
-         fe alias
-       | _ ->  assert false
-       end
-     with Not_found -> 
-       print_endline ("Flx_beta.expand_typeset: Unable to find symbol " ^ string_of_int index ^ " in bound symbol table!");
-       assert false
-    end
-  | t -> [t]
+(* This routine generates a typematch given an argument and a pattern list, any match
+   returns TRUE otherwise it returns FALSE. The patterns must be fully reduced.
+*) 
 
-and reduce_typeset_membership bsym_table counter sr elt tset =
-  let ls = expand_typeset bsym_table counter sr tset in
+let generate_typematch_predicate bsym_table counter sr elt ls =
   let e = BidSet.empty in
   let un = bbool true in
   let lss = List.rev_map (fun t -> {pattern=t; pattern_vars=e; assignments=[]},un) ls in
@@ -54,6 +33,37 @@ and reduce_typeset_membership bsym_table counter sr elt tset =
   Flx_btype.btyp_type_match (elt, lss)
 
 
+(* Reduce a typeset expression to a list of types *)
+let rec reduce_typeset bsym_table counter sr t = 
+  let r t = reduce_typeset bsym_table counter sr t in
+  match t with
+  (* each term must be a TYPE *)
+  | BTYP_type_set ts ->
+     List.map (beta_reduce' "Flx_beta.reduce_typeset" counter bsym_table sr 0 []) ts
+
+  (* each term must be a TYPESET *)
+  | BTYP_type_set_union tsets ->
+     Flx_list.uniq_list (List.concat (List.map r tsets))
+
+  | BTYP_inst (`Alias,index,ts,mt) ->
+    begin try 
+       let bsym = Flx_bsym_table.find bsym_table index in
+       let bbdcl = Flx_bsym.bbdcl bsym in
+       begin match bbdcl with
+       | Flx_bbdcl.BBDCL_structural_type_alias (bvs, alias) 
+       | Flx_bbdcl.BBDCL_nominal_type_alias (bvs, alias) ->
+         let alias = Flx_btype_subst.tsubst sr bvs ts alias in
+         let alias = beta_reduce' "Flx_beta.reduce_typeset" counter bsym_table sr 0 [] alias in
+         r alias
+       | _ -> assert false
+       end
+     with Not_found -> 
+       print_endline ("Flx_beta.expand_typeset: Unable to find symbol " ^ string_of_int index ^ " in bound symbol table!");
+       assert false
+    end
+  | t -> [t]
+
+
 (* fixpoint reduction: reduce
    Fix f. Lam x. e ==> Lam x. Fix z. e [f x -> z]
    to replace a recursive function
@@ -409,10 +419,11 @@ print_endline ("Beta-reducing typeop " ^ op ^ ", type=" ^ sbt bsym_table t);
   | BTYP_type_set ls -> btyp_type_set (List.map br ls)
 
   | BTYP_in (elt, tset) ->
-    let t = reduce_typeset_membership bsym_table counter sr elt tset in
+    let tset = beta_reduce' calltag counter bsym_table sr depth termlist tset in
+    let tsetelts = reduce_typeset bsym_table counter sr tset in 
+    let t = generate_typematch_predicate bsym_table counter sr elt tsetelts in
     beta_reduce' calltag counter bsym_table sr depth termlist t
 
-
   | BTYP_type_set_union ls ->
     let ls = List.rev_map br ls in
     (* split into explicit typesets and other terms

src/compiler/flx_core/flx_btype.ml

@@ -937,7 +937,6 @@ let rec bmt msg mt = match mt with
   (* this is wrong, we actually need to examine the pattern to find the kind *)
   | Flx_ast.KND_tpattern t -> kind_type (*  print_endline ("BMT tpattern fail " ^ msg); assert false *)
   | Flx_ast.KND_generic -> kind_type (* requied at least for GADTs to work *) 
-  | Flx_ast.KND_special s -> print_endline ("BMT special fail " ^ msg); assert false
 
 (* -------------------------------------------------------------------------- *)
 

src/compiler/flx_core/flx_kind.ml

@@ -65,7 +65,7 @@ let kind_unitsum = KIND_unitsum
 let kind_compactlinear = KIND_compactlinear
 let kind_bool = KIND_bool
 let kind_nat = KIND_nat
-let kind_typeset = KIND_nat
+let kind_typeset = KIND_typeset
 let kind_function (d, c) = KIND_function (d,c)
 let kind_tuple ks = KIND_tuple ks
 let kind_var s = KIND_var s

src/compiler/flx_core/flx_print.ml

@@ -378,7 +378,7 @@ and str_of_kindcode (k:kindcode_t) : string =
   | KND_typeset -> "TYPESET" 
   | KND_tuple ks -> catmap " * " str_of_kindcode ks
   | KND_function (d,c) -> str_of_kindcode d ^ " -> " ^ str_of_kindcode c
-  | KND_special s -> s
+  (* | KND_special s -> s *)
   | KND_tpattern t -> "TPATTERN(" ^ st 0 t ^ ")"
   | KND_var s -> "kvar_" ^ s
 

src/compiler/flx_desugar/flx_sex2flx.ml

@@ -66,11 +66,17 @@ and kind_of_sex sr x : kindcode_t =
   | Lst [Id "knd_name"; Str "NAT"] ->  KND_nat
   | Lst [Id "knd_name"; Str "TYPESET"] ->  KND_typeset
   | Lst [Id "knd_name"; Str "COMPACTLINEAR"] ->  KND_compactlinear
-  | Lst [Id "knd_name"; Str "GENERIC"] ->  KND_generic
-  (* NOTE: this is a HACK .. will do for now *)
-  | Lst [Id "knd_name"; Str name] -> KND_var name 
+
+  (* Combinators *)
   | Lst [Id "knd_arrow"; Lst[dom; cod]] -> KND_function (ki dom, ki cod)
   | Lst [Id "knd_tuple"; sr; Lst ts] -> KND_tuple (List.map ki ts)
+
+  (* this is a fudge: GENERIC isn't a kind but a rewriting directive *)
+  | Lst [Id "knd_name"; Str "GENERIC"] ->  KND_generic
+
+  (* NOTE: this is a HACK .. will do for now, note it has to go LAST in the pattern match *)
+  | Lst [Id "knd_name"; Str name] -> KND_var name 
+
   | _ ->
     print_endline ("Unexpected kind term"); 
     print_endline ( Sex_print.string_of_sex x );

src/packages/grammar.fdoc

@@ -168,24 +168,37 @@ syntax types {
   // -----------------
   // typesets
   // -----------------
+  priority
+    tset_lambda_pri <
+    tset_union_pri <
+    tset_intersection_pri <
+    tset_application_pri <
+    tset_atomic_pri 
+  ;
 
   //$ Typeset 
-  stmt := "typeset" sdeclname "=" typeset ";" =>#
+  stmt := "typeset" sdeclname "=" stypeset ";" =>#
     """
     `(ast_type_alias ,_sr ,(first _2) ,(second _2) ,_4)
     """;
 
-  typeset = tys[slambda_pri];
+  t[slambda_pri] := tys[tset_lambda_pri] =># '_1';
+
+  stypeset = tys[tset_lambda_pri];
+
+  tys[tset_atomic_pri] := squalified_name =># "_1"; 
+  tys[tset_atomic_pri] := "(" t[slambda_pri] ")"  =># "_2"; 
+  tys[tset_application_pri] := t[sapplication_pri] t[>sapplication_pri]  =># 
+    "`(typ_apply ,_sr (,_1 ,_2))" note "apply";
 
-  tys[satomic_pri] := squalified_name =># "_1"; 
-  tys[satomic_pri] := "(" tys[slambda_pri] ")"  =># "_2"; 
-  t[sapplication_pri] := "typesetof" "(" list::commalist1<stypeexpr> ")" =># 
-    "`(typ_typeset ,_sr ,_3)"; 
-  tys[satomic_pri] := "{" list::commalist1<stypeexpr> "}" =># 
+  //t[sapplication_pri] := "typesetof" "(" list::commalist1<stypeexpr> ")" =># "`(typ_typeset ,_sr ,_3)"; 
+  tys[tset_atomic_pri] := "{" list::commalist1<stypeexpr> "}" =># 
     "`(typ_typeset ,_sr ,_2)"; 
 
-  tys[ssetunion_pri] := tys[ssetunion_pri] "\cup" tys[>ssetunion_pri] =># "`(typ_typesetunion ,_sr ,_1 ,_3)";
-  tys[ssetintersection_pri] := tys[ssetintersection_pri] "\cap" tys[>ssetintersection_pri] =># "`(typ_typesetintersection ,_sr ,_1 ,_3)";
+  tys[tset_union_pri] := tys[tset_union_pri] "\cup" tys[>tset_union_pri] =># 
+    "`(typ_typesetunion ,_sr ,_1 ,_3)";
+  tys[tset_intersection_pri] := tys[tset_intersection_pri] "\cap" tys[>tset_intersection_pri] =># 
+    "`(typ_typesetintersection ,_sr ,_1 ,_3)";
 
   // -----------------
 
@@ -4747,7 +4760,7 @@ syntax statements {
   seqorin:= "=" stypeexpr =># "`(Eq ,_2)";
 
   //$ Individual type variable membership constraint.
-  seqorin:= "in" typeset =># "`(In ,_2)";
+  seqorin:= "in" stypeset =># "`(In ,_2)";
 
   //$ No constraint!
   seqorin:= sepsilon =># "'NoConstraint";

src/test/regress/rt/typeset-01.fdoc

@@ -0,0 +1,9 @@
+@title typeset expressions
+@felix
+typefun ty2(T:TYPE, U:TYPE):TYPESET => ({T,U});
+fun f[T in ty2(int, long) ] : T * T -> T = "$1+$2";
+fun g[T in ((fun(T:TYPE, U:TYPE):TYPESET => ({T,U})) (int, long)) ] : T * T -> T = "$1+$2";
+println$  f[int] (1,2), g[int] (1,2);
+@expect
+(3, 3)
+@

src/web/tut/polymorphism_02.fdoc

@@ -28,7 +28,7 @@ To solve the problem we use type constraints.
 
 First we introduce a construction to make a set of types:
 @felix
-typedef integers = typesetof(Int, Long);
+typeset integers = {Int, Long};
 @
 Now we write polymorphic functions with type constraints:
 @felix
@@ -82,7 +82,7 @@ println$ (f 1.2), f (Int 1);
 @
 Type sets also support the set union operator:
 @felix
-typedef mynumbers = integers \cup floats;
+typeset mynumbers = integers \cup floats;
 } // end class Constraints
 @
 Note that the typesets @{ints} and @{floats}, along with some other