Skip to content

Commit

Permalink
first class kind TYPESET
Browse files Browse the repository at this point in the history
  • Loading branch information
skaller committed May 28, 2022
1 parent bd5fc03 commit e53c179
Show file tree
Hide file tree
Showing 12 changed files with 58 additions and 41 deletions.
2 changes: 1 addition & 1 deletion GNUmakefile
Original file line number Diff line number Diff line change
Expand Up @@ -284,7 +284,7 @@ perf-dir:
tutopt-dir:
mkdir -p ${BUILDROOT}/tutopt
${BUILDBIN}/flx_tangle --indir=${BUILDROOT}/share/src/web/tutopt --outdir=${BUILDROOT}/test/tutopt
for file in src/web/tutopt/*.fdoc; do ${BUILDBIN}/flx_iscr $$file ${BUILDROOT}/test/tutopt; done
-for file in src/web/tutopt/*.fdoc; do ${BUILDBIN}/flx_iscr $$file ${BUILDROOT}/test/tutopt; done

tut-dir:
mkdir -p ${BUILDROOT}/tut
Expand Down
2 changes: 1 addition & 1 deletion src/compiler/flx_core/flx_ast.ml
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,7 @@ and kindcode_t =
| KND_bool
| KND_nat
| KND_generic
| KND_typeset of string (* excl mark *)
| KND_typeset
| KND_function of kindcode_t * kindcode_t
| KND_tuple of kindcode_t list
| KND_tpattern of typecode_t
Expand Down
2 changes: 1 addition & 1 deletion src/compiler/flx_core/flx_btype.ml
Original file line number Diff line number Diff line change
Expand Up @@ -928,14 +928,14 @@ let rec bmt msg mt = match mt with
| Flx_ast.KND_compactlinear-> kind_compactlinear
| Flx_ast.KND_unitsum -> kind_unitsum
| Flx_ast.KND_nat -> kind_nat
| Flx_ast.KND_typeset -> kind_typeset
| Flx_ast.KND_bool -> kind_bool
| Flx_ast.KND_function (t1,t2) -> kind_function (bmt msg t1, bmt msg t2)
| Flx_ast.KND_tuple(ts) -> kind_tuple(List.map (bmt msg) ts)
| Flx_ast.KND_var s -> kind_var s

(* 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_typeset ts -> print_endline ("BMT typeset 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

Expand Down
2 changes: 1 addition & 1 deletion src/compiler/flx_core/flx_btype_kind.ml
Original file line number Diff line number Diff line change
Expand Up @@ -148,7 +148,7 @@ print_endline ("Flx_btype_kind.metatype' case type_apply: " ^ Flx_btype.st typ);
| BTYP_type_set _
| BTYP_type_set_union _
| BTYP_type_set_intersection _
-> kind_type (* WRONG but lets see what happens ! *)
-> kind_typeset (* WRONG but lets see what happens ! *)

| BTYP_ellipsis -> kind_type

Expand Down
4 changes: 4 additions & 0 deletions src/compiler/flx_core/flx_kind.ml
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ type kind =
| KIND_compactlinear
| KIND_bool
| KIND_nat
| KIND_typeset
| KIND_tuple of kind list
| KIND_function of kind * kind (* the kind of a type function from domain to codomain kinds *)
| KIND_var of string
Expand All @@ -25,6 +26,7 @@ let rec sk k =
| KIND_compactlinear -> "COMPACTLINEAR"
| KIND_bool -> "BOOL"
| KIND_nat -> "NAT"
| KIND_typeset -> "TYPESET"
| KIND_tuple ks -> "(" ^ Flx_util.catmap ", " sk ks ^")"
| KIND_function (d,c) -> sk d ^ " -> " ^ sk c
| KIND_var s -> s
Expand Down Expand Up @@ -63,6 +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_function (d, c) = KIND_function (d,c)
let kind_tuple ks = KIND_tuple ks
let kind_var s = KIND_var s
Expand Down Expand Up @@ -105,6 +108,7 @@ let ksolve_subtypes add_eqn lhs rhs (mgu:kmgu_t ref) =


| KIND_nat, KIND_nat
| KIND_typeset, KIND_typeset
| KIND_bool, KIND_bool
-> ()

Expand Down
2 changes: 1 addition & 1 deletion src/compiler/flx_core/flx_print.ml
Original file line number Diff line number Diff line change
Expand Up @@ -375,7 +375,7 @@ and str_of_kindcode (k:kindcode_t) : string =
| KND_bool -> "BOOL"
| KND_nat -> "NAT"
| KND_generic -> "GENERIC"
| KND_typeset s -> "!" ^ s
| 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
Expand Down
9 changes: 1 addition & 8 deletions src/compiler/flx_desugar/flx_sex2flx.ml
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,7 @@ and kind_of_sex sr x : kindcode_t =
| Lst [Id "knd_name"; Str "UNITSUM"] -> KND_unitsum
| Lst [Id "knd_name"; Str "BOOL"] -> KND_bool
| 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 *)
Expand All @@ -75,14 +76,6 @@ and kind_of_sex sr x : kindcode_t =
print_endline ( Sex_print.string_of_sex x );
raise Not_kind


(*
| KND_typeset of string (* excl mark *)
| KND_tpattern of typecode_t
| KND_special of string
*)


and type_of_sex sr w : typecode_t = xtype_t sr w

and xtype_t sr x : typecode_t =
Expand Down
1 change: 1 addition & 0 deletions src/misc/vim/syntax/felix.vim
Original file line number Diff line number Diff line change
Expand Up @@ -155,6 +155,7 @@ syn keyword felixStatement then
syn keyword felixStatement todo
syn keyword felixStatement to
syn keyword felixStatement typedef
syn keyword felixStatement typeset
syn keyword felixStatement typefun
syn keyword felixStatement type
syn keyword felixStatement union
Expand Down
38 changes: 19 additions & 19 deletions src/packages/core_scalar_types.fdoc
Original file line number Diff line number Diff line change
Expand Up @@ -182,77 +182,77 @@ union of two typesets.

@tangle scalar.flx
//$ Types associated with raw address calculations.
typedef addressing = typesetof (
typeset addressing = {
byte,
address,
caddress
);
};

//$ Character types.
typedef chars = typesetof (char);
typeset chars = {char};

@h2 Integers
@tangle scalar.flx
//$ "natural" sized signed integer types.
//$ These correspond to C/C++ core types.
typedef fast_sints = typesetof (tiny, short, int, long, vlong);
typeset fast_sints = {tiny, short, int, long, vlong};

//$ Exact sized signed integer types.
//$ In C these are typedefs.
//$ In Felix they're distinct types.
typedef exact_sints = typesetof(int8,int16,int32,int64);
typeset exact_sints = {int8,int16,int32,int64};

//$ "natural" sized unsigned integer types.
//$ These correspond to C/C++ core types.
typedef fast_uints = typesetof (utiny, ushort, uint, ulong,uvlong);
typeset fast_uints = {utiny, ushort, uint, ulong,uvlong};

//$ Exact sized unsigned integer types.
//$ In C these are typedefs.
//$ In Felix they're distinct types.
typedef exact_uints = typesetof (uint8,uint16,uint32,uint64,uint128,uint256);
typeset exact_uints = {uint8,uint16,uint32,uint64,uint128,uint256};

//$ Weirdo signed integers types corresponding to
//$ typedefs in C.
typedef weird_sints = typesetof (ptrdiff, ssize, intmax, intptr);
typeset weird_sints = {ptrdiff, ssize, intmax, intptr};

//$ Weirdo unsigned integers types corresponding to
//$ typedefs in C.
typedef weird_uints = typesetof (size, uintmax, uintptr);
typeset weird_uints = {size, uintmax, uintptr};

//$ All the signed integers.
typedef sints = fast_sints \cup exact_sints \cup weird_sints;
typeset sints = fast_sints \cup exact_sints \cup weird_sints;

//$ All the usigned integers.
typedef uints = fast_uints \cup exact_uints \cup weird_uints;
typeset uints = fast_uints \cup exact_uints \cup weird_uints;

//$ All the fast integers.
typedef fast_ints = fast_sints \cup fast_uints;
typeset fast_ints = fast_sints \cup fast_uints;

//$ All the exact integers.
typedef exact_ints = exact_sints \cup exact_uints;
typeset exact_ints = exact_sints \cup exact_uints;

//$ All the integers.
typedef ints = sints \cup uints;
typeset ints = sints \cup uints;

@h2 Floats
@tangle scalar.flx
//$ All the core floating point types.
typedef floats = typesetof (float, double, ldouble);
typeset floats = {float, double, ldouble};

//$ All the core approximations to real types.
typedef reals = ints \cup floats;
typeset reals = ints \cup floats;

//$ All the core approximations to complex types.
typedef complexes = typesetof (fcomplex,dcomplex,lcomplex);
typeset complexes = {fcomplex,dcomplex,lcomplex};

//$ All the core approximations to numbers.
typedef numbers = reals \cup complexes;
typeset numbers = reals \cup complexes;
@

@h2 All Scalars.
@tangle scalar.flx
//$ All the basic scalar types.
typedef basic_types = bool \cup numbers \cup chars \cup addressing;
typeset basic_types = bool \cup numbers \cup chars \cup addressing;

// we define this now, we will open it later...
instance [t in basic_types] Eq[t] {
Expand Down
27 changes: 23 additions & 4 deletions src/packages/grammar.fdoc
Original file line number Diff line number Diff line change
Expand Up @@ -119,9 +119,6 @@ syntax types {
t[scomparison_pri]:= t[>scomparison_pri] cmp t[>scomparison_pri] =>#
"(tbinop _2 _1 _3))";

t[ssetunion_pri] := t[ssetunion_pri] "\cup" t[>ssetunion_pri] =># "`(typ_typesetunion ,_sr ,_1 ,_3)";
t[ssetintersection_pri] := t[ssetintersection_pri] "\cap" t[>ssetintersection_pri] =># "`(typ_typesetintersection ,_sr ,_1 ,_3)";

// right arrows: RIGHT ASSOCIATIVE!
//$ Function type, right associative.
t[sarrow_pri] := t[>sarrow_pri] "->" t[sarrow_pri] =># "`(typ_arrow (,_1 ,_3))";
Expand Down Expand Up @@ -168,8 +165,30 @@ syntax types {
t[sapplication_pri] := t[sapplication_pri] t[>sapplication_pri] =>#
"`(typ_apply ,_sr (,_1 ,_2))" note "apply";

// -----------------
// typesets
// -----------------

//$ Typeset
stmt := "typeset" sdeclname "=" typeset ";" =>#
"""
`(ast_type_alias ,_sr ,(first _2) ,(second _2) ,_4)
""";

typeset = tys[slambda_pri];

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> "}" =>#
"`(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)";

// -----------------


t[sfactor_pri] := t[sfactor_pri] "." t[>sfactor_pri] =># "`(typ_apply ,_sr (,_3 ,_1))";

Expand Down Expand Up @@ -4728,7 +4747,7 @@ syntax statements {
seqorin:= "=" stypeexpr =># "`(Eq ,_2)";

//$ Individual type variable membership constraint.
seqorin:= "in" stypeexpr =># "`(In ,_2)";
seqorin:= "in" typeset =># "`(In ,_2)";

//$ No constraint!
seqorin:= sepsilon =># "'NoConstraint";
Expand Down
2 changes: 1 addition & 1 deletion src/packages/strings.fdoc
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ type string = "::std::basic_string<char>"
encoder "::flx::gc::generic::string_encoder",
decoder "::flx::gc::generic::string_decoder"
;
typedef strings = typesetof (string);
typeset strings = {string};

class Str [T] {
virtual fun str: T -> string;
Expand Down
8 changes: 4 additions & 4 deletions src/web/tut/intro_11.fdoc
Original file line number Diff line number Diff line change
Expand Up @@ -60,10 +60,10 @@ But it's wrong. How do we fix this?

Here's the answer:
@felix
typedef myints = typesetof (myshort, myint, mylong);
typedef myuints = typesetof (myushort, myuint, myulong);
typedef myfloats = typesetof (myfloat, mydouble);
typedef mynumbers = myints \cup myuints \cup myfloats;
typeset myints = {myshort, myint, mylong};
typeset myuints = {myushort, myuint, myulong};
typeset myfloats = {myfloat, mydouble};
typeset mynumbers = myints \cup myuints \cup myfloats;

fun mymake [T in mynumbers] : int -> T = "int($1)";
fun *[T in mynumbers] : T * T -> T = "$1*$2";
Expand Down

0 comments on commit e53c179

Please sign in to comment.