Stefan pushed to branch main at Stefan / Typer
Commits: 9da75535 by Maxim Bernard at 2024-08-09T16:20:11-04:00 Change tuple implementation and behavior of the `_<-_` operator.
This operator is now used to unpack any `datacons`, possibly with nested patterns. It also supports the tuple notation.
* btl/assign-datacons.typer: Implementation of the `assign-datacons` macro, which generates a series of assignments, each corresponding to a specific value in the provided datacons.
* btl/pervasive.typer: Set `_<-_` to newly defined `assign-datacons` macro. Add `List_filter` function (required by `assign-datacons` module). Remove definitions: `tuple-nth` macro, pair and triplet (which have been moved to the tuple module) and `BoolMod`. Move do-lib definitions and certain List functions further in the file, since they require definitions in tuple-lib.
* btl/tuple.typer: Redesign and simplify how Typer implements tuples. Tuples are now one of the nine predefined ADTs, containing up to 10 items. The comma operator (defined in `pervasive.typer`) now simply calls the approprate constructor based on the number of arguments.
* btl/case.typer: * btl/qcase.typer: Make necessary adaptations required by changes in tuple implementation.
- - - - -
5 changed files:
- + btl/assign-datacons.typer - btl/case.typer - btl/pervasive.typer - btl/qcase.typer - btl/tuple.typer
Changes:
===================================== btl/assign-datacons.typer ===================================== @@ -0,0 +1,210 @@ +get-symbol-name sexp = + let error-msg = "<ERROR: not a symbol>" + in Sexp_dispatch sexp + (lambda _ _ -> error-msg) % node + (lambda name -> name) % symbol + (lambda _ -> error-msg) % string + (lambda _ -> error-msg) % int + (lambda _ -> error-msg) % float + (lambda _ -> error-msg); % block + +get-constructor-name pattern-sexp = + let error-msg = "<ERROR: invalid constructor name>" + in Sexp_dispatch pattern-sexp + % Must be a node... + (lambda head _ -> + Sexp_dispatch head + (lambda _ _ -> error-msg) + % ...whose head is a symbol. + (lambda name -> name) + (lambda _ -> error-msg) + (lambda _ -> error-msg) + (lambda _ -> error-msg) + (lambda _ -> error-msg)) + (lambda _ -> error-msg) + (lambda _ -> error-msg) + (lambda _ -> error-msg) + (lambda _ -> error-msg) + (lambda _ -> error-msg); + +get-subpatterns pattern-sexp = + Sexp_dispatch pattern-sexp + (lambda _ args -> args) + (lambda sym-name -> (cons (Sexp_symbol sym-name) nil)) + (lambda _ -> nil) + (lambda _ -> nil) + (lambda _ -> nil) + (lambda _ -> nil); + +% If `pattern-sexp` is of the form `a,b,c,...`, converts in into the appropriate +% tuple (e.g. `tuple3 a b c`). +expand-tuple pattern-sexp = + if String_eq "_,_" (get-constructor-name pattern-sexp) + then tuple-lib.make-tuple-impl (get-subpatterns pattern-sexp) + else pattern-sexp; + +% E.g. with argument `(a (b x y) z)`, returns `["x", "y", "z"]` +get-newvars-names : List Sexp -> List String; +get-newvars-names subpatterns = + List_foldl + (lambda acc pat -> + Sexp_dispatch pat + % node + (lambda _head tail -> + List_concat acc (get-newvars-names tail)) + % symbol + (lambda name -> List_concat acc (cons name nil)) + % all other cases should not occur + (lambda _ -> acc) + (lambda _ -> acc) + (lambda _ -> acc) + (lambda _ -> acc)) + nil + subpatterns; + +pattern-has-var pat var-name = + case List_find + (lambda candidate -> String_eq var-name candidate) + (get-newvars-names (get-subpatterns pat)) + | some _ => true + | none => false; + +% Generates a `case` matching over `subject`, which is supposed to have a single +% constructor `cstr-name` with `nb-params` operands, but only accesses the +% `var-idx`-th operand, under the bound variable `var-sym`. The branch returns +% `ret-val`. +make-single-case : Sexp -> String -> Int -> Int -> Sexp -> Sexp -> Sexp; +make-single-case subject cstr-name nb-params var-idx var-sym ret-val = + let mk-pat-params : Int -> List Sexp; + mk-pat-params i = + let current-sym = if Int_eq i var-idx + then var-sym + else (Sexp_symbol "_") + in if Int_< i nb-params + then cons current-sym (mk-pat-params (Int_+ 1 i)) + else nil; + pattern = (Sexp_node (Sexp_symbol cstr-name) (mk-pat-params 0)); + branch-node = (Sexp_node (Sexp_symbol "_=>_") + (cons pattern (cons ret-val nil))) + in Sexp_node (Sexp_symbol "##case_") + (cons (Sexp_node (Sexp_symbol "_|_") + (cons subject (cons branch-node nil))) + nil); + +% Generates the `case` cascade that accesses and returns the `var-name` value +% in `subpatterns`, matching over `subject`. +make-case-for-var : String -> String -> List Sexp -> Sexp -> Sexp -> Sexp; +make-case-for-var var-name cstr-name subpatterns subject temp-matching-var = + let nb-params = List_length subpatterns; + in case List_find (lambda pat-idx-pair -> + case pat-idx-pair + | pair pat _ => pattern-has-var pat var-name) + (List_mapi pair subpatterns) + | some found-subpattern => + % There is a corresponding subpattern with a variable named `var-name`. + (case found-subpattern + | pair pat idx => + Sexp_dispatch + pat + % node case : has subpatterns + (lambda sub-cstr-name sub-subpatterns -> + let body = make-case-for-var var-name + (get-symbol-name sub-cstr-name) + sub-subpatterns + temp-matching-var + temp-matching-var + in make-single-case subject + cstr-name + nb-params + idx + temp-matching-var + body) + % symbol case : is the variable we're looking for + (lambda _ -> + make-single-case subject + cstr-name + nb-params + idx + temp-matching-var + temp-matching-var) + % other cases : error (cannot occur) + (lambda _ -> Sexp_error) + (lambda _ -> Sexp_error) + (lambda _ -> Sexp_error) + (lambda _ -> Sexp_error)) + | none => + % Logically should not occur + Sexp_symbol "error none"; + +assign-datacons = macro + (lambda args -> + let + pattern-sexp = List_nth 0 args Sexp_error; % e.g. `(a (b x y) z)` + value-sexp = List_nth 1 args Sexp_error; % e.g. `someFunction 1 2 3` + + pattern-sexp-norm = expand-tuple pattern-sexp; + + cstr-name = get-constructor-name pattern-sexp-norm; + subpatterns = get-subpatterns pattern-sexp-norm; + + new-bound-variables = get-newvars-names subpatterns; % `["x", "y", "z"]` + + make-bound-var-asgn-list datacons-var temp-matching-var = + List_map + (lambda var-name -> + make-decl + (Sexp_symbol var-name) + (make-case-for-var var-name + cstr-name + subpatterns + datacons-var + temp-matching-var)) + % Only consider variables not named `_` + (List_filter + (lambda var-name -> not (String_eq var-name "_")) + new-bound-variables); + + % Final list of assignments, which contains : + % - an unnamed variable with the value being filtered over + % - every bound variable from the pattern (`x`, `y` and `z` from the above + % example), whose value is a cascade of `case`s returning the appropriate + % element from `tuple-varname` + % e.g. + % gensym0 = someFunction 1 2 3; + % x = case gensym0 + % | a gensym1 _ => + % case gensym1 + % | b gensym1 _ => gensym1; + % y = case gensym0 + % | a gensym1 _ => + % case gensym1 + % | b _ gensym1 => gensym1; + % z = case gensym0 + % | a _ gensym1 => + % gensym1; + make-defs-list = lambda datacons-var temp-matching-var -> + cons (make-decl datacons-var value-sexp) + (make-bound-var-asgn-list datacons-var temp-matching-var) + in do { + datacons-var <- gensym (); + temp-matching-var <- gensym (); + IO_return (Sexp_node (Sexp_symbol "_;_") + (make-defs-list datacons-var temp-matching-var)); + }); + +% `(a (b x y) z) <- somevalue` +test1 = cons (quote (a (b x y) z)) + (cons (quote somevalue) nil); + +% `a, (b x _ z), c <- sometuple` +test2 = cons (quote (a, (b x _ z), c)) + (cons (quote sometuple) nil); + +runtest test = + IO_run + (do { + res <- Macro_expand assign-datacons test; + Sexp_debug_print res; + IO_return unit + }) + ();
===================================== btl/case.typer ===================================== @@ -610,7 +610,7 @@ in do { %% Take note that "renamed pattern" correspond to all pattern in list "B" %% and list "C" is the childs of list "B" in the same order. %% -part-type = Pair (Triplet Pat (List Var) (List (Pair Pat (List (Pair Var Var))))) (List (Pair Pats Code)); +part-type = Pair (Tuple Pat (List Var) (List (Pair Pat (List (Pair Var Var))))) (List (Pair Pats Code));
%% %% Takes a list of branches (pair of (patterns, body)) @@ -716,7 +716,7 @@ partition-branches branches = let rvars <- gen-vars ivars; rpat <- renamed-pat pat rvars; vars <- List_foldl (ff rvars) (IO_return nil) pp; - IO_return (pair (triplet rpat rvars (List_merge pp vars)) tt); + IO_return (pair (rpat, rvars, (List_merge pp vars)) tt); };
in io-list (List_map mf pre-parts); @@ -730,7 +730,7 @@ in do { %% reminder %% %% part-type = Pair -%% (Triplet Pat (List Var) (List (Pair Pat (List (Pair Var Var))))) +%% (Tuple Pat (List Var) (List (Pair Pat (List (Pair Var Var))))) %% (List (Pair Pats Code)); %%
@@ -763,8 +763,9 @@ merge-dflt parts odflt = let preppend : Pat -> List (Pair Pat (List (Pair Var Var))) -> List (Pair Pats Code) -> part-type -> part-type; preppend pat vars branches part = case part - | pair p b => (case p | triplet _ lv v => - pair (triplet pat lv (List_concat vars v)) (List_concat branches b)); + | pair p b => + let (_, lv, v) <- p + in pair (pat, lv, (List_concat vars v)) (List_concat branches b);
%% %% Append child branches if we see more than one default branches @@ -780,21 +781,22 @@ merge-dflt parts odflt = let append : Pat -> List (Pair Pat (List (Pair Var Var))) -> List (Pair Pats Code) -> part-type -> part-type; append pat vars branches part = case part - | pair p b => (case p | triplet _ lv v => - pair (triplet pat lv (List_concat v vars)) (List_concat b branches)); + | pair p b => + let (_, lv, v) <- p + in pair (pat, lv, (List_concat v vars)) (List_concat b branches);
in case parts | cons part parts => (case part | pair p pp => - (case p | triplet pat _ vars => - if (dflt? pat) then - (case odflt - | some dflt => merge-dflt parts (some (append pat vars pp dflt)) - | none => merge-dflt parts (some part)) - else - (case odflt - %% merge previous default to all branches - | some dflt => cons (preppend pat vars pp dflt) (merge-dflt parts odflt) - | none => cons part (merge-dflt parts odflt)))) + let (pat, _, vars) <- p + in if (dflt? pat) then + (case odflt + | some dflt => merge-dflt parts (some (append pat vars pp dflt)) + | none => merge-dflt parts (some part)) + else + (case odflt + %% merge previous default to all branches + | some dflt => cons (preppend pat vars pp dflt) (merge-dflt parts odflt) + | none => cons part (merge-dflt parts odflt))) | nil => (case odflt | some dflt => (cons dflt nil) | none => nil); @@ -840,7 +842,7 @@ in List_map (preppend-dflt max-len) branches; %% reminder %% %% part-type = Pair -%% (Triplet +%% (Tuple %% Pat (List Var) (List (Pair Pat (List (Pair Var Var))))) %% (List (Pair Pats Code)); %% @@ -952,11 +954,12 @@ compile-case subjects branches = let %% translate-part : part-type -> IO Code; translate-part branch = case branch - | pair patterns branches => (case patterns - | triplet pat rvars pats-vars => do { - sub-cases <- translate-sub-pats rvars pats-vars branches; - IO_return (quote (_=>_ (uquote pat) (uquote sub-cases))); - }); + | pair patterns branches => + let (pat, rvars, pats-vars) <- patterns + in do { + sub-cases <- translate-sub-pats rvars pats-vars branches; + IO_return (quote (_=>_ (uquote pat) (uquote sub-cases))); + };
%% %% Generate code from all partition
===================================== btl/pervasive.typer ===================================== @@ -185,6 +185,16 @@ List_fold2 f o xs ys = case xs List_empty : List ?a -> Bool; List_empty xs = Int_eq (List_length xs) (Integer->Int 0);
+% Only keeps items whose `f` predicate returns true +List_filter : (?a -> Bool) -> List ?a -> List ?a; +List_filter f l = + case l + | nil => nil + | cons x xs => + (case (f x) + | true => cons x (List_filter f xs) + | false => List_filter f xs); + %%% Good 'ol combinators
id x = x; @@ -410,55 +420,6 @@ type Sexp_wrapper
Sexp_wrap s = Sexp_dispatch s node symbol string integer float block;
-%%%% Tuples - -%% Sample tuple: a module holding Bool and its constructors. -BoolMod = (##datacons - %% We need the `?` metavars to be lexically outside of the - %% `typecons` expression, otherwise they end up generalized, so - %% we end up with a type constructor like - %% - %% typecons _ (cons (τ₁ : Type) (t : τ₁) - %% (τ₂ : Type) (true : τ₂) - %% (τ₃ : Type) (false : τ₃)) - %% - %% And it's actually even worse because it tries to generalize - %% over the level of those `Type`s, so we end up with an invalid - %% inductive type. - ((lambda t1 t2 t3 - -> typecons _ (cons (t :: t1) (true :: t2) (false :: t3))) - ? ? ?) - cons) - (_ := Bool) (_ := true) (_ := false); - -Pair = typecons (Pair (a : Type) (b : Type)) (pair (fst : a) (snd : b)); -pair = datacons Pair pair; - -%% Triplet (tuple with 3 values) -type Triplet (a : Type) (b : Type) (c : Type) - | triplet (x : a) (y : b) (z : c); - -%%%% List with tuple - -%% Merge two List to a List of Pair -%% Both List must be of same length -List_merge : List ?a -> List ?b -> List (Pair ?a ?b); -List_merge xs ys = case xs - | cons x xs => ( case ys - | cons y ys => cons (pair x y) (List_merge xs ys) - | nil => nil ) % error - | nil => nil; - -%% `Unmerge` a List of Pair -%% The two functions name said it all -List_map-fst xs = let - mf p = case p | pair x _ => x; -in List_map mf xs; - -List_map-snd xs = let - mf p = case p | pair _ y => y; -in List_map mf xs; - %%%% Logic
%% `False` should be one of the many empty types. @@ -600,52 +561,83 @@ typeclass Monad; define-operator "<-" 80 96;
%% -%% `List` is the type and `list` is the module +%% Module containing tuple definitions, including the macro used for expanding +%% the comma (`_,_`) operator. +%% Used by `case_` and by `_<-_` %% -list = load "btl/list.typer"; +tuple-lib = load "btl/tuple.typer"; + +Pair = tuple-lib.Pair; +Tuple3 = tuple-lib.Tuple3; +Tuple4 = tuple-lib.Tuple4; +Tuple5 = tuple-lib.Tuple5; +Tuple6 = tuple-lib.Tuple6; +Tuple7 = tuple-lib.Tuple7; +Tuple8 = tuple-lib.Tuple8; +Tuple9 = tuple-lib.Tuple9; +Tuple10 = tuple-lib.Tuple10; + +pair = tuple-lib.pair; +tuple3 = tuple-lib.tuple3; +tuple4 = tuple-lib.tuple4; +tuple5 = tuple-lib.tuple5; +tuple6 = tuple-lib.tuple6; +tuple7 = tuple-lib.tuple7; +tuple8 = tuple-lib.tuple8; +tuple9 = tuple-lib.tuple9; +tuple10 = tuple-lib.tuple10;
%% -%% Macro `do` for easier series of IO operation +%% Instantiate a tuple from expressions %% %% e.g.: -%% do { IO_return true; }; +%% tup = (x,y,z); %% -do-lib = load "btl/do.typer"; -do-impl = do-lib.do-impl; -do = do-lib.do; -do* = do-lib.do*; +_,_ = tuple-lib.make-tuple;
-%% -%% Module containing various macros for tuple -%% Used by `case_` -%% -tuple-lib = load "btl/tuple.typer"; +Tuple = tuple-lib.tuple-type;
%% -%% Get the nth element of a tuple +%% Functions over lists of tuples %% -%% e.g.: -%% tuple-nth tup 0; -%% -tuple-nth = tuple-lib.tuple-nth; + +%% Merge two List to a List of Pair +%% Both List must be of same length +List_merge : List ?a -> List ?b -> List (Pair ?a ?b); +List_merge xs ys = case xs + | cons x xs => ( case ys + | cons y ys => cons (pair x y) (List_merge xs ys) + | nil => nil ) % error + | nil => nil; + +%% `Unmerge` a List of Pair +%% The two functions name said it all +List_map-fst xs = let + mf p = case p | pair x _ => x; +in List_map mf xs; + +List_map-snd xs = let + mf p = case p | pair _ y => y; + in List_map mf xs;
%% -%% Affectation of tuple -%% -%% e.g.: -%% (x,y,z) <- tup; +%% `List` is the type and `list` is the module %% -_<-_ = tuple-lib.assign-tuple; +list = load "btl/list.typer"; +
%% -%% Instantiate a tuple from expressions +%% Macro `do` for easier series of IO operation %% %% e.g.: -%% tup = (x,y,z); +%% do { IO_return true; }; %% -_,_ = tuple-lib.make-tuple; +do-lib = load "btl/do.typer"; +do-impl = do-lib.do-impl; +do = do-lib.do; +do* = do-lib.do*;
-Tuple = tuple-lib.tuple-type; +_<-_ = let lib = load "btl/assign-datacons.typer" in lib.assign-datacons;
%% %% Macro `case` for a some more complex pattern matching
===================================== btl/qcase.typer ===================================== @@ -59,12 +59,12 @@ qcase_impl = lambda (sexps : List Sexp) -> %% Triple of the expression to eliminate, the underlying type A %% and the relation R %% A and R are optional - elim_expr_details : Triplet Sexp (Option Sexp) (Option Sexp); + elim_expr_details : Tuple Sexp (Option Sexp) (Option Sexp); elim_expr_details = let - kerr = K (triplet Sexp_error none none); + kerr = K (Sexp_error, none, none); extract_from_annotated_e : Sexp -> List Sexp -> - Triplet Sexp (Option Sexp) (Option Sexp); + Tuple Sexp (Option Sexp) (Option Sexp); extract_from_annotated_e _ xs = if (Int_eq (List_length xs) 2) then @@ -82,10 +82,10 @@ qcase_impl = lambda (sexps : List Sexp) -> a = List_nth 0 sexps Sexp_error; r = List_nth 1 sexps Sexp_error; in - triplet e (some a) (some r) + (e, (some a), (some r)) else - triplet e (some Sexp_error) (some Sexp_error); - kerr' = K (triplet e (some Sexp_error) (some Sexp_error)); + (e, (some Sexp_error), (some Sexp_error)); + kerr' = K (e, (some Sexp_error), (some Sexp_error)); in Sexp_dispatch e_type extract_type % Nodes @@ -95,9 +95,9 @@ qcase_impl = lambda (sexps : List Sexp) -> kerr' % Float kerr' % List of Sexp else - triplet Sexp_error none none; + (Sexp_error, none, none); extract_targ_from_node : Sexp -> List Sexp -> - Triplet Sexp (Option Sexp) (Option Sexp); + Tuple Sexp (Option Sexp) (Option Sexp); extract_targ_from_node x xs = %% Check if annotation is present if (is_sym x "_:_") @@ -107,12 +107,12 @@ qcase_impl = lambda (sexps : List Sexp) -> else %% No annotation was given, return the entire %% expresson as the elimination target - triplet x none none; + (x, none, none); in Sexp_dispatch elim_targ_sexp extract_targ_from_node % Nodes - (lambda _ -> triplet elim_targ_sexp - none none) % Symbol + (lambda _ -> (elim_targ_sexp, + none, none)) % Symbol kerr % String kerr % Integer kerr % Float @@ -262,18 +262,18 @@ qcase_impl = lambda (sexps : List Sexp) -> kerr % Float kerr; % List of Sexp qelim_args : List Sexp; - qelim_args = case elim_expr_details - | triplet e a r => - let - res = (cons elim_fn - (cons elim_compat - (cons e nil))); - res' = (case r - | none => res - | some r' => - (cons (build_explicit_arg "R" r') res)); - in - res'; + qelim_args = + let + (e, a, r) <- elim_expr_details; + res = (cons elim_fn + (cons elim_compat + (cons e nil))); + res' = (case r + | none => res + | some r' => + (cons (build_explicit_arg "R" r') res)); + in + res'; qelim_sexp = Sexp_node (Sexp_symbol "Quotient_elim") qelim_args; in
===================================== btl/tuple.typer ===================================== @@ -1,246 +1,81 @@ %%% tuple.typer --- Notation `_,_` for tuples
-%% Here's an example similar to tuple from `load` -%% -%% Sample tuple: a module holding Bool and its constructors. -%% -%% We need the `?` metavars to be lexically outside of the -%% `typecons` expression, otherwise they end up generalized, so -%% we end up with a type constructor like -%% -%% typecons _ (cons (τ₁ : Type) (t : τ₁) -%% (τ₂ : Type) (true : τ₂) -%% (τ₃ : Type) (false : τ₃)) -%% -%% And it's actually even worse because it tries to generalize -%% over the level of those `Type`s, so we end up with an invalid -%% inductive type. -%% -%% BoolMod = (##datacons -%% ((lambda t1 t2 t3 -%% -> typecons _ (cons (t :: t1) (true :: t2) (false :: t3))) -%% ? ? ?) -%% cons) -%% (_ := Bool) (_ := true) (_ := false); -%% - -%% List_nth = list.nth; -%% List_map = list.map; -%% List_mapi = list.mapi; -%% List_map2 = list.map2; -%% List_concat = list.concat; - -%% -%% Move IO outside List (from element to List) -%% (The function's type explain everything) -%% -io-list : List (IO ?a) -> IO (List ?a); -io-list l = let - ff : IO (List ?a) -> IO ?a -> IO (List ?a); - ff o v = do { - o <- o; - v <- v; - IO_return (cons v o); - }; -in do { - l <- (List_foldl ff (IO_return nil) l); - IO_return (List_reverse l nil); -}; - -%% -%% Generate a List of pseudo-unique symbol -%% -%% Takes a List of Sexp and generate a List of new name of the same length -%% whatever are the element of the List -%% -gen-vars : List Sexp -> IO (List Sexp); -gen-vars vars = io-list (List_map - (lambda _ -> gensym ()) - vars); - -%% -%% Reference for tuple's implicit field name -%% -%% Takes a list of vars (it could actually only takes a length) -%% Returns symbol `%n` with n in [0,length) (integer only, obviously) -%% -gen-tuple-names : List Sexp -> List Sexp; -gen-tuple-names vars = List_mapi - (lambda _ i -> Sexp_symbol (String_concat "%" (Int->String i))) - vars; - -%% -%% Takes a list -%% Returns a list of the same length with every element set to "?" symbol -%% -gen-deduce : List Sexp -> List Sexp; -gen-deduce vars = List_map - (lambda _ -> Sexp_symbol "?") - vars; - -%%% -%%% Access one tuple's element -%%% - -%% -%% This is a macro with conceptualy this signature: -%% tuple-nth : (tup-type : Type) ≡> (elem-type : Type) ≡> tup-type -> Int -> elem-type; -%% -%% Returns the n'th element of the tuple -%% -tuple-nth = macro (lambda args -> let - - nerr = lambda _ -> (Int->Integer (-1)); - - %% argument `n` of this macro - n : Integer; - n = Sexp_dispatch (List_nth 1 args Sexp_error) - (lambda _ _ -> nerr ()) - nerr nerr - (lambda n -> n) - nerr nerr; - - %% implicit tuple field name - elem-sym : Sexp; - elem-sym = Sexp_symbol (String_concat "%" (Integer->String n)); - - %% tuple, argument of this macro - tup : Sexp; - tup = List_nth 0 args Sexp_error; - -in IO_return (Sexp_node (Sexp_symbol "__.__") (cons tup (cons elem-sym nil))) -); - -%%% -%%% Affectation, unwraping tuple -%%% - -%% -%% syntax: -%% (x, y, z) <- p; -%% -%% and then `x`, `y`, `z` are defined as tuple's element 0, 1, 2 -%% -assign-tuple = macro (lambda args -> let - - xserr = lambda _ -> (nil : List Sexp); - - %% Expect a ","-node - %% Returns variables - get-tup-elem : Sexp -> List Sexp; - get-tup-elem sexp = Sexp_dispatch sexp - (lambda s ss -> - if (Sexp_eq s (Sexp_symbol "_,_")) then - (ss) - else - (nil)) - xserr xserr xserr xserr xserr; - - %% map every tuple's variable - %% using `tuple-nth` to assign element to variable - mf : Sexp -> Sexp -> Int -> Sexp; - mf t arg i = Sexp_node (Sexp_symbol "_=_") - (cons arg (cons (Sexp_node (Sexp_symbol "tuple-nth") - (cons t (cons (Sexp_integer (Int->Integer i)) nil))) nil)); - -in do { - IO_return (Sexp_node (Sexp_symbol "_;_") (List_mapi - (mf (List_nth 1 args Sexp_error)) - (get-tup-elem (List_nth 0 args Sexp_error)))); -}); - -%% -%% Wrap the third argument `fun` with a `let` definition for each variables -%% Names are taken from `rvars` and definition are taken from `ivars` -%% - -wrap-vars : List Sexp -> List Sexp -> Sexp -> Sexp; -wrap-vars ivars rvars fun = List_fold2 (lambda fun v0 v1 -> - %% - %% I prefer `let` definition because a lambda function would need a type - %% (quote ((lambda (uquote v0) -> (uquote fun)) (uquote v1)))) - %% - (quote (let (uquote v1) = (uquote v0) in (uquote fun)))) - fun ivars rvars; - -%% -%% Takes a list of values (expressions) as Sexp (like a variable, 1, 1.0, "str", etc) -%% Returns a tuple containing those values -%% -make-tuple-impl : List Sexp -> IO Sexp; -make-tuple-impl values = let - - %% map tuple element declaration - mf1 : Sexp -> Sexp -> Sexp; - mf1 name value = Sexp_node (Sexp_symbol "_::_") (cons name (cons value nil)); - - %% map tuple element value - mf2 : Sexp -> Sexp -> Sexp; - mf2 value nth = Sexp_node (Sexp_symbol "_:=_") (cons nth (cons value nil)); - - ff1 : Sexp -> Sexp -> Sexp -> Sexp; - ff1 body arg arg-t = Sexp_node (Sexp_symbol "lambda_->_") - (cons (Sexp_node (Sexp_symbol "_:_") (cons arg (cons arg-t nil))) - (cons body nil)); - - ff2 : Sexp -> Sexp -> Sexp; - ff2 body arg = Sexp_node (Sexp_symbol "lambda_≡>_") - (cons (Sexp_node (Sexp_symbol "_:_") (cons arg (cons (Sexp_symbol "Type") nil))) - (cons body nil)); - -in do { - args-t <- gen-vars values; - - args <- gen-vars values; - - names <- IO_return (gen-tuple-names values); - - tuple-t <- IO_return (Sexp_node (Sexp_symbol "typecons") - (cons (Sexp_symbol "Tuple") - (cons (Sexp_node (Sexp_symbol "cons") (List_map2 mf1 names args-t)) nil))); - - tuple <- IO_return (Sexp_node (Sexp_node (Sexp_symbol "datacons") - (cons tuple-t (cons (Sexp_symbol "cons") nil))) - (List_map2 mf2 args names)); - - fun <- IO_return (List_foldl ff2 - (List_fold2 ff1 tuple (List_reverse args nil) - (List_reverse args-t nil)) - (List_reverse args-t nil)); - - values <- IO_return (List_reverse values nil); - - affect <- IO_return (Sexp_node fun (List_reverse values nil)); - - IO_return affect; -}; - -%% -%% Macro to instantiate a tuple -%% -make-tuple = macro (lambda args -> do { - r <- make-tuple-impl args; - r <- IO_return r; - IO_return r; -}); - -%% -%% Macro returning the type of a tuple -%% -%% Takes element's type as argument -%% -tuple-type = macro (lambda args -> let - - mf : Sexp -> Sexp -> Sexp; - mf n t = Sexp_node (Sexp_symbol "_::_") - (cons n (cons t nil)); - -in do { - names <- IO_return (gen-tuple-names args); - - r <- IO_return (Sexp_node (Sexp_symbol "typecons") (cons - (Sexp_symbol "Tuple") (cons (Sexp_node (Sexp_symbol "cons") - (List_map2 mf names args)) nil))); - - IO_return r; -}); +type Pair (a : Type) (b : Type) + | pair (fst : a) (snd : b); + +type Tuple3 (a : Type) (b : Type) (c : Type) + | tuple3 (v1 : a) (v2 : b) (v3 : c); + +type Tuple4 (a : Type) (b : Type) (c : Type) (d : Type) + | tuple4 (v1 : a) (v2 : b) (v3 : c) (v4 : d); + +type Tuple5 (a : Type) (b : Type) (c : Type) (d : Type) (e : Type) + | tuple5 (v1 : a) (v2 : b) (v3 : c) (v4 : d) (v5 : e); + +type Tuple6 (a : Type) (b : Type) (c : Type) (d : Type) (e : Type) (f : Type) + | tuple6 (v1 : a) (v2 : b) (v3 : c) (v4 : d) (v5 : e) (v6 : f); + +type Tuple7 + (a : Type) (b : Type) (c : Type) (d : Type) (e : Type) + (f : Type) (g : Type) + | tuple7 + (v1 : a) (v2 : b) (v3 : c) (v4 : d) (v5 : e) + (v6 : f) (v7 : g); + +type Tuple8 + (a : Type) (b : Type) (c : Type) (d : Type) (e : Type) + (f : Type) (g : Type) (h : Type) + | tuple8 + (v1 : a) (v2 : b) (v3 : c) (v4 : d) (v5 : e) + (v6 : f) (v7 : g) (v8 : h); + +type Tuple9 + (a : Type) (b : Type) (c : Type) (d : Type) (e : Type) + (f : Type) (g : Type) (h : Type) (i : Type) + | tuple9 + (v1 : a) (v2 : b) (v3 : c) (v4 : d) (v5 : e) + (v6 : f) (v7 : g) (v8 : h) (v9 : i); + +type Tuple10 + (a : Type) (b : Type) (c : Type) (d : Type) (e : Type) + (f : Type) (g : Type) (h : Type) (i : Type) (j : Type) + | tuple10 + (v1 : a) (v2 : b) (v3 : c) (v4 : d) (v5 : e) + (v6 : f) (v7 : g) (v8 : h) (v9 : i) (v10 : j); + +tuple-cstr-names = + cons "pair" + (cons "tuple3" + (cons "tuple4" + (cons "tuple5" + (cons "tuple6" + (cons "tuple7" + (cons "tuple8" + (cons "tuple9" + (cons "tuple10" nil)))))))); + +tuple-type-names = + cons "Pair" + (cons "Tuple3" + (cons "Tuple4" + (cons "Tuple5" + (cons "Tuple6" + (cons "Tuple7" + (cons "Tuple8" + (cons "Tuple9" + (cons "Tuple10" nil)))))))); + +make-sexp-from-names : List String -> List Sexp -> Sexp; +make-sexp-from-names name-list args = + let nb-args = List_length args; + tuple-name = List_nth (Int_- nb-args 2) name-list "" + in if Int_<= nb-args 10 + then Sexp_node (Sexp_symbol tuple-name) args + else Sexp_symbol "<ERROR: limit 10 items per tuple>"; + +make-tuple-impl = make-sexp-from-names tuple-cstr-names; +tuple-type-impl = make-sexp-from-names tuple-type-names; + +make-tuple = macro (lambda args -> IO_return (make-tuple-impl args)); + +tuple-type = macro (lambda args -> IO_return (tuple-type-impl args));
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/9da7553594a3908e07aa8234d5adaf7909...