Simon Génier pushed to branch sexp-case at Stefan / Typer

Commits: aadf51c9 by Simon Génier at 2020-12-12T05:50:08-05:00 Add a sexp-case macro.

This macro lets you write case-like expressions for Sexp, which I hope are neater than Sexp_dispatch. The code is quite tedious because it is written to be loaded quite early, before some key macros like the enhanced case and lambda. This is because sexp-case is meant to help macro authorship, including these quite complicated macros! It was also necessary to shuffle a few definitions in pervasive.typer to allow us to write it as early as possible.

Was it a waste of time to write this macro when Sexp_wrapper exists? Probably. I was not aware of the existence of Sexp_wrapper until I was almost done with sexp-case_.

- - - - - 36bdbe04 by Simon Génier at 2020-12-12T05:50:30-05:00 Use sexp-case in a few places.

- - - - - 272c2a39 by Simon Génier at 2020-12-12T06:53:24-05:00 Better error messages when => is missing in sexp-case.

- - - - - 7060dab9 by Simon Génier at 2020-12-12T07:21:13-05:00 Use sexp-case in case.typer.

- - - - -

3 changed files:

- btl/case.typer - btl/pervasive.typer - + btl/sexp-case.typer

Changes:

===================================== btl/case.typer ===================================== @@ -70,30 +70,24 @@ in Sexp_node (Sexp_symbol "##datacons") %% `cons expr1 expr2 ... ` %% expand-tuple-ctor : Sexp -> Sexp; -expand-tuple-ctor sexp = let - - err = (lambda _ -> Sexp_error); - -in Sexp_dispatch sexp - (lambda s ss -> +expand-tuple-ctor sexp = + sexp-case sexp + | node s ss => if (Sexp_eq s (Sexp_symbol "_,_")) then (Sexp_node tuple-ctor ss) else - (Sexp_node s ss)) - (lambda _ -> sexp) - err err err err; + (Sexp_node s ss) + | symbol _ => sexp + | _ => Sexp_error;

%% %% Is tuple %% tuple? : Sexp -> Bool; -tuple? sexp = let - - sfalse = (lambda _ -> false); - -in Sexp_dispatch sexp - (lambda s _ -> Sexp_eq s tuple-ctor) - sfalse sfalse sfalse sfalse sfalse; +tuple? sexp = + sexp-case sexp + | node s _ => Sexp_eq s tuple-ctor + | _ => false;

%% %% Get matched expression (e.g. case (var1,var2,...) | ...) @@ -108,20 +102,15 @@ in Sexp_dispatch sexp %% It used to be more useful.) %% get-tup-exprs : Sexp -> List Sexp; -get-tup-exprs sexp = let - - err = (lambda _ -> cons Sexp_error nil); - - get-tup-exprs-helper : Sexp -> List Sexp -> List Sexp; - get-tup-exprs-helper s ss = case (Sexp_eq (Sexp_symbol "_,_") s) - | true => cons (Sexp_node s ss) nil % tuple - %% constructor or function called (only 1 pattern) - | false => cons (Sexp_node s ss) nil; - -in Sexp_dispatch sexp - get-tup-exprs-helper - (lambda s -> cons (Sexp_symbol s) nil) - err err err err; +get-tup-exprs sexp = + sexp-case sexp + | node s ss => + (case (Sexp_eq (Sexp_symbol "_,_") s) + | true => cons (Sexp_node s ss) nil % tuple + %% constructor or function called (only 1 pattern) + | false => cons (Sexp_node s ss) nil) + | symbol s => cons (Sexp_symbol s) nil + | _ => cons Sexp_error nil;

%% %% Some alias to clarify type of functions @@ -148,9 +137,6 @@ dflt? v = Sexp_eq dflt-var v; %% get-branches : List Sexp -> List Sexp -> List (Pair Pats Code); get-branches vars sexps = let - - perr = (lambda _ -> pair (cons Pat_error nil) Code_error); - %% here, sexp is a node of patterns (the lhs of a "_=>_"-node) to-case : Sexp -> Pair Pats Code; to-case sexp = let @@ -161,14 +147,14 @@ get-branches vars sexps = let else (List_map expand-tuple-ctor (get-tup-exprs sexp));

- in Sexp_dispatch sexp - - (lambda s ss -> case (Sexp_eq (Sexp_symbol "_=>_") s) - %% expecting a Sexp_node as second argument to _=>_ - | true => pair (tup-exprs (List_nth 0 ss Pat_error)) (List_nth 1 ss Code_error) - | false => pair (cons Pat_error nil) Code_error) - - perr perr perr perr perr; + in + sexp-case sexp + | node s ss => + (case (Sexp_eq (Sexp_symbol "_=>_") s) + %% expecting a Sexp_node as second argument to _=>_ + | true => pair (tup-exprs (List_nth 0 ss Pat_error)) (List_nth 1 ss Code_error) + | false => pair (cons Pat_error nil) Code_error) + | _ => pair (cons Pat_error nil) Code_error;

%% map all "_=>_"-node to (patterns, body) pair helper : List Sexp -> List (Pair Pats Code); @@ -184,40 +170,38 @@ in helper sexps; %% kinds : Sexp -> IO (List Bool); kinds pat = let - - %% - %% errors used in Sexp_dispatch - %% - serr = lambda _ -> Sexp_error; - strerr = K "< error >"; - xserr = lambda _ -> (nil : List Sexp); - %% %% Get constructor of `pat` %% ctor : String; ctor = let ctor-name : Sexp -> String; - ctor-name pat = Sexp_dispatch pat - (lambda s ss -> ctor-name s) - I strerr strerr strerr strerr; + ctor-name pat = + sexp-case pat + | node s _ => ctor-name s + | symbol s => s + | _ => "< error >"; in ctor-name pat;

%% %% Get args from the `pat` node %% args : List Sexp; - args = Sexp_dispatch pat - (lambda s ss -> ss) - (lambda _ -> (nil : List Sexp)) % FIXME: Redundant type annotation. - xserr xserr xserr xserr; + args = + sexp-case pat + | node _ ss => ss + | _ => + % FIXME: Redundant type annotation. + (nil : List Sexp);

%% %% Just get a String from a symbol %% str_of_sym : Sexp -> String; - str_of_sym arg = Sexp_dispatch arg - (lambda _ _ -> "< error >") I strerr strerr strerr strerr; + str_of_sym arg = + sexp-case arg + | symbol s => s + | _ => "< error >";

%% %% map function for all pattern's variables @@ -230,20 +214,17 @@ kinds pat = let %% arguments with name, other without name and all this in a random order %% mf : Elab_Context -> Sexp -> Int -> Bool; - mf env arg i = Sexp_dispatch arg - (lambda s ss -> if (Sexp_eq s (Sexp_symbol "_:=_")) then - ( if (Sexp_eq (List_nth 0 ss Sexp_error) dflt-var) then - (Elab_is-nth-erasable ctor i env) - else - (Elab_is-arg-erasable ctor (str_of_sym (List_nth 0 ss Sexp_error)) env) ) - else - (false)) - (lambda _ -> false) - (lambda _ -> false) - (lambda _ -> false) - (lambda _ -> false) - (lambda _ -> false); - + mf env arg i = + sexp-case arg + | node s ss => + if (Sexp_eq s (Sexp_symbol "_:=_")) then + (if (Sexp_eq (List_nth 0 ss Sexp_error) dflt-var) then + (Elab_is-nth-erasable ctor i env) + else + (Elab_is-arg-erasable ctor (str_of_sym (List_nth 0 ss Sexp_error)) env) ) + else + (false) + | _ => false;

%% %% What to do if argument are named (`(arg-name := x)`)? @@ -265,14 +246,6 @@ in ks; %% renamed-pat : Sexp -> List Sexp -> IO Sexp; renamed-pat pat names = let - - %% - %% errors used in Sexp_dispatch - %% - serr = lambda _ -> Sexp_error; - strerr = lambda _ -> "< error >"; - xserr = lambda _ -> (nil : List Sexp); - %% %% true if `pat` is a tuple, false if it is a %% single expression @@ -290,10 +263,11 @@ renamed-pat pat names = let %% Get the constructor of the pattern as argument %% ctor : Sexp -> String; - ctor pat = Sexp_dispatch pat - (lambda s _ -> ctor s) - (lambda s -> s) - strerr strerr strerr strerr; + ctor pat = + sexp-case pat + | node s _ => ctor s + | symbol s => s + | _ => "< error >";

%% %% Map function to rename `pat` with symbol in `names` @@ -305,8 +279,9 @@ renamed-pat pat names = let %% and if it already use explicit field or not %% mf : List Bool -> Sexp -> Int -> Sexp; - mf kinds v i = Sexp_dispatch v - (lambda sym ss -> + mf kinds v i = + sexp-case v + | node sym ss => if (Sexp_eq sym (Sexp_symbol "_:=_")) then if (List_nth i kinds false) then %% if client use multiple name for the same erasable args, @@ -319,21 +294,22 @@ renamed-pat pat names = let (Sexp_node (Sexp_symbol "_:=_") (cons (tuple-nth i) (cons (List_nth i names Sexp_error) nil))) else - (List_nth i names Sexp_error)) - (lambda _ -> if tup then + (List_nth i names Sexp_error) + | symbol _ => if tup then (Sexp_node (Sexp_symbol "_:=_") (cons (tuple-nth i) (cons (List_nth i names Sexp_error) nil))) else - (List_nth i names Sexp_error)) - serr serr serr serr; + (List_nth i names Sexp_error) + | _ => Sexp_error;

in do { pat <- IO_return pat; kinds <- kinds pat; - IO_return (Sexp_dispatch pat - (lambda s ss -> Sexp_node s (List_mapi (mf kinds) ss)) - (lambda s -> Sexp_symbol s) - serr serr serr serr); + IO_return + (sexp-case pat + | node s ss => Sexp_node s (List_mapi (mf kinds) ss) + | symbol s => Sexp_symbol s + | _ => Sexp_error); };

%% @@ -342,34 +318,28 @@ in do { %% is-pat : Pat -> IO Bool; is-pat pat = let - - %% - %% errors used in Sexp_dispatch - %% - err = lambda _ -> IO_return false; - serr = lambda _ -> "< error >"; - %% %% Get a String from a Sexp_symbol %% sym-str : Sexp -> String; - sym-str sexp = Sexp_dispatch sexp - (lambda _ _ -> serr ()) - (lambda str -> str) - serr serr serr serr; - -in Sexp_dispatch pat - (lambda sym _ -> do { + sym-str sexp = + sexp-case sexp + | symbol str => str + | _ => "< error >"; + +in + sexp-case pat + | node sym _ => do { env <- Elab_getenv (); ctor <- IO_return (Elab_isconstructor (sym-str sym) env); tupl <- IO_return (Sexp_eq sym (Sexp_symbol "_,_")); IO_return (or ctor tupl); - }) - (lambda sym -> do { + } + | symbol sym => do { env <- Elab_getenv (); IO_return (Elab_isconstructor sym env); - }) - err err err err; + } + | _ => IO_return false;

%% %% Takes two pattern and return true if the two pattern @@ -377,20 +347,15 @@ in Sexp_dispatch pat %% same-ctor? : Pat -> Pat -> Bool; same-ctor? p0 p1 = let - - %% - %% error used in Sexp_dispatch - %% - err = lambda _ -> Pat_error; - %% %% Get the constructor of a pattern %% ctor-of : Pat -> Sexp; - ctor-of p = Sexp_dispatch p - (lambda s _ -> s) - (lambda s -> Sexp_symbol s) - err err err err; + ctor-of pat = + sexp-case pat + | node s _ => s + | symbol _ => pat + | _ => Pat_error;

%% Compare head of node of both pattern in Sexp_eq (ctor-of p0) (ctor-of p1); @@ -403,12 +368,6 @@ in Sexp_eq (ctor-of p0) (ctor-of p1); %% introduced-vars : Pat -> IO (List Var); introduced-vars pat = let - - %% - %% error used in Sexp_dispatch - %% - serr = lambda _ -> IO_return (pair 0 nil); - %% %% List of kind of pattern argument %% @@ -433,8 +392,9 @@ introduced-vars pat = let IO_return (case p | pair x _ => x); };

- in Sexp_dispatch v - (lambda s ss -> do { + in + sexp-case v + | node s ss => do { o <- o; % bind i <- i; ks <- ks; @@ -445,8 +405,8 @@ introduced-vars pat = let (IO_return (pair (i + 1) (List_concat o (cons (List_nth 1 ss Var_error) nil)))) else (IO_return (pair (i + 1) (List_concat o (cons dflt-var nil)))); - }) - (lambda s -> do { + } + | symbol s => do { o <- o; % bind i <- i; sym <- IO_return (Sexp_symbol s); @@ -455,18 +415,16 @@ introduced-vars pat = let (IO_return (pair (i + 1) (List_concat o (cons dflt-var nil)))) else (IO_return (pair (i + 1) (List_concat o (cons sym nil)))); - }) - serr serr serr serr; + } + | _ => IO_return (pair 0 nil);

-in Sexp_dispatch pat - (lambda _ ss -> do { +in + sexp-case pat + | node _ ss => do { p <- (List_foldl ff (IO_return (pair 0 nil)) ss); - IO_return (case p - | pair _ xs => xs); - }) - (lambda _ -> IO_return nil) % constructor as a unique symbol (`true`, etc) - (lambda _ -> IO_return nil) (lambda _ -> IO_return nil) % error - (lambda _ -> IO_return nil) (lambda _ -> IO_return nil); % error + IO_return (case p | pair _ xs => xs); + } + | _ => IO_return nil;

%% %% Wrap the third argument (`fun`) with a `let` definition for each variables @@ -503,9 +461,6 @@ in List_map mf ps; %% pattern-sub-pats : Pat -> IO (List Pat); pattern-sub-pats pat = let - - err = lambda _ -> IO_return nil; - %% %% dflt-var mean there's no sub pattern %% @@ -522,17 +477,18 @@ pattern-sub-pats pat = let (IO_return dflt-var); };

-in Sexp_dispatch pat - (lambda ctor args -> do { +in + sexp-case pat + | node ctor args => do { r <- io-list (List_map map-arg args); IO_return r; - }) - (lambda sym -> do { + } + | symbol sym => do { %% constructor has no argument %% so there can't be any sub pattern IO_return nil; - }) - err err err err; + } + | _ => IO_return nil;

%% %% Takes a List of similar pattern (i.e. patterns with same constructor) @@ -1025,7 +981,9 @@ case-impl args = let

%% Expecting only one Sexp_node containing a case with arguments

-in (Sexp_dispatch (List_nth 0 args Sexp_error) - case1 err err err err err); +in + sexp-case List_nth 0 args Sexp_error + | node s ss => case1 s ss + | _ => IO_return Sexp_error;

case-macro = macro case-impl;

===================================== btl/pervasive.typer ===================================== @@ -36,6 +36,18 @@ Option = typecons (Option (ℓ ::: TypeLevel) (a : Type_ ℓ)) (none) (some a); some = datacons Option some; none = datacons Option none;

+%%%% `Result` type + +Result : Type -> Type -> Type; +Result = lambda α -> lambda β -> typecons Result (ok α) (err β); + +ok : (α : Type) ≡> (β : Type) ≡> α -> Result α β; +ok = lambda α ≡> lambda β ≡> datacons (Result α β) ok; + +err : (α : Type) ≡> (β : Type) ≡> β -> Result α β; +err = lambda α ≡> lambda β ≡> datacons (Result α β) err; + + %%%% List functions

List_length : List ?a -> Int; % Recursive defs aren't generalized :-( @@ -84,25 +96,99 @@ List_nth = lambda n -> lambda xs -> lambda d -> case xs | true => x | false => List_nth (n - 1) xs d;

-%%%% A more flexible `lambda` +%%%% Quasi-Quote macro + +%% f = (quote (uquote x) * x) (node _*_ [(Sexp_node unquote "x") "x"]) +%% +%% f = Sexp_node "*" cons (x, cons (Sexp_symbol "x") nil)) +%% +%% => x

%% An `Sexp` which we use to represents an *error*. Sexp_error = Sexp_symbol "<error>";

+%% Takes an Sexp `x` as argument and return an Sexp which represents code +%% which will construct an Sexp equivalent to `x` at run-time. +%% This is basically *cross stage persistence* for Sexp. +quote1 : Sexp -> Sexp; +quote1 x = let + qlist : List Sexp -> Sexp; + qlist xs = case xs + | nil => Sexp_symbol "nil" + | cons x xs => Sexp_node (Sexp_symbol "cons") + (cons (quote1 x) + (cons (qlist xs) nil)); + make_app = lambda str -> lambda sexp -> + Sexp_node (Sexp_symbol str) (cons sexp nil); + + node = lambda op -> lambda y -> + case (Sexp_eq op (Sexp_symbol "uquote")) + | true => List_head Sexp_error y + | false => Sexp_node (Sexp_symbol "##Sexp.node") + (cons (quote1 op) + (cons (qlist y) nil)); + symbol s = make_app "##Sexp.symbol" (Sexp_string s); + string s = make_app "##Sexp.string" (Sexp_string s); + integer i = make_app "##Sexp.integer" + (make_app "##Int->Integer" (Sexp_integer i)); + float f = make_app "##Sexp.float" (Sexp_float f); + block sxp = + %% FIXME ##Sexp.block takes a string (and prelexes + %% it) but we have a sexp, what should we do? + Sexp_symbol "<error FIXME block quoting>"; + in Sexp_dispatch x node symbol string integer float block; + +%% quote definition +quote = macro (lambda x -> IO_return (quote1 (List_head Sexp_error x))); + +%%%% "Module" access + +__.__ = + let mksel = lambda o -> lambda f -> + let constructor = Sexp_node (Sexp_symbol "##datacons") + (cons (Sexp_symbol "?") + (cons (Sexp_symbol "cons") + nil)); + pattern = Sexp_node constructor + (cons (Sexp_node (Sexp_symbol "_:=_") + (cons f (cons (Sexp_symbol "v") + nil))) + nil); + branch = Sexp_node (Sexp_symbol "_=>_") + (cons pattern (cons (Sexp_symbol "v") nil)); + in Sexp_node (Sexp_symbol "case_") + (cons (Sexp_node (Sexp_symbol "_|_") + (cons o (cons branch nil))) + nil) + in macro (lambda args + -> IO_return + case args + | cons o tail + => (case tail + | cons f _ => mksel o f + | nil => Sexp_error) + | nil => Sexp_error); + +%%%% Sexp-Case macro + +define-operator "sexp-case" () 43; +sexp-case-lib = load "btl/sexp-case.typer"; +sexp-case_ = macro (lambda (sexps : List Sexp) -> IO_return (sexp-case-lib.sexp-case-impl sexps)); + +%%%% A more flexible `lambda` + %% Sexp_to_list : Sexp -> List Sexp -> List Sexp; Sexp_to_list s = lambda exceptions -> - let singleton (_ : ?) = cons s nil in %FIXME: Get rid of ": ?"! - Sexp_dispatch - s - (node := lambda head -> lambda tail - -> case List_find (Sexp_eq head) exceptions - | some _ => singleton () + sexp-case s + | node head tail + => (case List_find (Sexp_eq head) exceptions + | some _ => cons s nil | none => cons head tail) - (symbol := lambda s - -> case String_eq "" s + | symbol name + => (case String_eq "" name | true => nil - | false => singleton ()) - singleton singleton singleton singleton; + | false => cons s nil) + | _ => cons s nil;

multiarg_lambda = %% This macro lets `lambda_->_` (and siblings) accept multiple arguments. @@ -191,47 +277,6 @@ I x = x; K : ?a -> (b : Type) ≡> b -> ?a; K x y = x;

-%%%% Quasi-Quote macro - -%% f = (quote (uquote x) * x) (node _*_ [(Sexp_node unquote "x") "x"]) -%% -%% f = Sexp_node "*" cons (x, cons (Sexp_symbol "x") nil)) -%% -%% => x - -%% Takes an Sexp `x` as argument and return an Sexp which represents code -%% which will construct an Sexp equivalent to `x` at run-time. -%% This is basically *cross stage persistence* for Sexp. -quote1 : Sexp -> Sexp; -quote1 x = let - qlist : List Sexp -> Sexp; - qlist xs = case xs - | nil => Sexp_symbol "nil" - | cons x xs => Sexp_node (Sexp_symbol "cons") - (cons (quote1 x) - (cons (qlist xs) nil)); - make_app str sexp = - Sexp_node (Sexp_symbol str) (cons sexp nil); - - node op y = case (Sexp_eq op (Sexp_symbol "uquote")) - | true => List_head Sexp_error y - | false => Sexp_node (Sexp_symbol "##Sexp.node") - (cons (quote1 op) - (cons (qlist y) nil)); - symbol s = make_app "##Sexp.symbol" (Sexp_string s); - string s = make_app "##Sexp.string" (Sexp_string s); - integer i = make_app "##Sexp.integer" - (make_app "##Int->Integer" (Sexp_integer i)); - float f = make_app "##Sexp.float" (Sexp_float f); - block sxp = - %% FIXME ##Sexp.block takes a string (and prelexes - %% it) but we have a sexp, what should we do? - Sexp_symbol "<error FIXME block quoting>"; - in Sexp_dispatch x node symbol string integer float block; - -%% quote definition -quote = macro (lambda x -> IO_return (quote1 (List_head Sexp_error x))); - %%%% The `type` declaration macro

%% Build a declaration: @@ -273,52 +318,37 @@ type-impl = lambda (x : List Sexp) -> %% Type name --^ ^------^ constructors

%% Return a list contained inside a node sexp. - let knil = K nil; - kerr = K Sexp_error; - - get-list : Sexp -> List Sexp; - get-list node = Sexp_dispatch node - (lambda op lst -> lst) % Nodes - knil % Symbol - knil % String - knil % Integer - knil % Float - knil; % List of Sexp + let get-list : Sexp -> List Sexp; + get-list node = + sexp-case node + | node _ lst => lst + | _ => (nil : List Sexp);

%% Get a name (symbol) from a sexp %% - (name t) -> name %% - name -> name get-name : Sexp -> Sexp; get-name sxp = - Sexp_dispatch sxp - (lambda op _ -> get-name op) % Nodes - (lambda _ -> sxp) % Symbol - kerr % String - kerr % Integer - kerr % Float - kerr; % List of Sexp + sexp-case sxp + | node op _ => get-name op + | symbol _ => sxp + | _ => Sexp_error;

get-args : Sexp -> List Sexp; get-args sxp = - Sexp_dispatch sxp - (lambda _ args -> args) % Nodes - (lambda _ -> (nil : List Sexp)) % Symbol - (lambda _ -> (nil : List Sexp)) % String - (lambda _ -> (nil : List Sexp)) % Integer - (lambda _ -> (nil : List Sexp)) % Float - (lambda _ -> (nil : List Sexp)); % List of Sexp + sexp-case sxp + | node _ args => args + | _ => (nil : List Sexp);

get-type : Sexp -> Sexp; get-type sxp = - Sexp_dispatch sxp - (lambda s ss -> case (Sexp_eq s (Sexp_symbol "_:_")) - | true => List_nth 1 ss Sexp_error - | false => sxp) - (lambda _ -> sxp) - (lambda _ -> Sexp_error) - (lambda _ -> Sexp_error) - (lambda _ -> Sexp_error) - (lambda _ -> Sexp_error); + sexp-case sxp + | node s ss + => (case Sexp_eq s (Sexp_symbol "_:_") + | true => List_nth 1 ss Sexp_error + | false => sxp) + | symbol _ => sxp + | _ => Sexp_error;

get-head = List_head Sexp_error;

@@ -404,32 +434,6 @@ BoolMod = (##datacons Pair = typecons (Pair (a : Type) (b : Type)) (pair (fst : a) (snd : b)); pair = datacons Pair pair;

-__.__ = - let mksel o f = - let constructor = Sexp_node (Sexp_symbol "##datacons") - (cons (Sexp_symbol "?") - (cons (Sexp_symbol "cons") - nil)); - pattern = Sexp_node constructor - (cons (Sexp_node (Sexp_symbol "_:=_") - (cons f (cons (Sexp_symbol "v") - nil))) - nil); - branch = Sexp_node (Sexp_symbol "_=>_") - (cons pattern (cons (Sexp_symbol "v") nil)); - in Sexp_node (Sexp_symbol "case_") - (cons (Sexp_node (Sexp_symbol "_|_") - (cons o (cons branch nil))) - nil) - in macro (lambda args - -> IO_return - case args - | cons o tail - => (case tail - | cons f _ => mksel o f - | nil => Sexp_error) - | nil => Sexp_error); - %% Triplet (tuple with 3 values) type Triplet (a : Type) (b : Type) (c : Type) | triplet (x : a) (y : b) (z : c); @@ -677,14 +681,9 @@ Test_file = macro (lambda args -> let (cons (Sexp_symbol "unit") nil);

%% Expecting a String and nothing else -in IO_return (Sexp_dispatch (List_nth 0 args Sexp_error) - (lambda _ _ -> ret) - (lambda _ -> ret) - %% `load` is a special form and takes a Sexp rather than a real `String` - (lambda s -> quote (let lib = load (uquote (Sexp_string s)); in lib.exec-test)) - (lambda _ -> ret) - (lambda _ -> ret) - (lambda _ -> ret)) +in IO_return (sexp-case List_nth 0 args Sexp_error + | string s => quote (let lib = load (uquote (Sexp_string s)); in lib.exec-test) + | _ => ret) );

%%% pervasive.typer ends here.

===================================== btl/sexp-case.typer ===================================== @@ -0,0 +1,426 @@ +%%% sexp-case.typer --- Case-like syntactic sugar for Sexp_dispatch. +%%% +%%% Language: builtins, quote, and uquote. + +NodeAcc : Type; +NodeAcc = + typecons + NodeAcc + (node-acc (head-var : Sexp) (tail-var : Sexp) (expr : Sexp)) +; + +node-acc : Sexp -> Sexp -> Sexp -> NodeAcc; +node-acc = datacons NodeAcc node-acc; + +AtomAcc : Type; +AtomAcc = typecons AtomAcc (atom-acc (var : Sexp) (expr : Sexp)); + +atom-acc : Sexp -> Sexp -> AtomAcc; +atom-acc = datacons AtomAcc atom-acc; + +SexpCaseAcc : Type; +SexpCaseAcc = + typecons + SexpCaseAcc + (sexp-case-acc + (node-acc : Option NodeAcc) + (symbol-acc : Option AtomAcc) + (string-acc : Option AtomAcc) + (int-acc : Option AtomAcc) + (float-acc : Option AtomAcc) + (block-acc : Option AtomAcc) + (otherwise-expr : Sexp)) +; + +sexp-case-acc : + Option NodeAcc -> + Option AtomAcc -> + Option AtomAcc -> + Option AtomAcc -> + Option AtomAcc -> + Option AtomAcc -> + Sexp -> + SexpCaseAcc +; +sexp-case-acc = datacons SexpCaseAcc sexp-case-acc; + +sexp<-sexp-case-acc : Sexp -> SexpCaseAcc -> Sexp; +sexp<-sexp-case-acc = lambda target -> lambda acc -> + let + otherwise-expr = + case acc + | sexp-case-acc _ _ _ _ _ _ otherwise-expr => otherwise-expr + ; + + node-λ = + case acc + | sexp-case-acc node-acc' _ _ _ _ _ _ => + case node-acc' + | none => quote (lambda _ -> lambda _ -> (uquote otherwise-expr)) + | some acc => + case acc + | node-acc head-var tail-var expr => + quote + (lambda (uquote head-var) -> + lambda (uquote tail-var) -> + (uquote expr)) + ; + + symbol-λ = + case acc + | sexp-case-acc _ symbol-acc _ _ _ _ _ => + case symbol-acc + | none => quote (lambda _ -> (uquote otherwise-expr)) + | some acc => + case acc + | atom-acc var expr => quote (lambda (uquote var) -> (uquote expr)) + ; + + string-λ = + case acc + | sexp-case-acc _ _ string-acc _ _ _ _ => + case string-acc + | none => quote (lambda _ -> (uquote otherwise-expr)) + | some acc => + case acc + | atom-acc var expr => quote (lambda (uquote var) -> (uquote expr)) + ; + + int-λ = + case acc + | sexp-case-acc _ _ _ int-acc _ _ _ => + case int-acc + | none => quote (lambda _ -> (uquote otherwise-expr)) + | some acc => + case acc + | atom-acc var expr => quote (lambda (uquote var) -> (uquote expr)) + ; + + float-λ = + case acc + | sexp-case-acc _ _ _ _ float-acc _ _ => + case float-acc + | none => quote (lambda _ -> (uquote otherwise-expr)) + | some acc => + case acc + | atom-acc var expr => quote (lambda (uquote var) -> (uquote expr)) + ; + + block-λ = + case acc + | sexp-case-acc _ _ _ _ _ block-acc _ => + case block-acc + | none => quote (lambda _ -> (uquote otherwise-expr)) + | some acc => + case acc + | atom-acc var expr => quote (lambda (uquote var) -> (uquote expr)) + ; + in + quote + (Sexp_dispatch + (uquote target) + (uquote node-λ) + (uquote symbol-λ) + (uquote string-λ) + (uquote int-λ) + (uquote float-λ) + (uquote block-λ)) +; + +%% +%% Case-like syntax for sexps that expands to a call to Sexp_dispatch. +%% +%% For example, +%% +%% sexp-case ?e +%% | node h t => ?e-node +%% | symbol n => ?e-symbol +%% | _ => ?e-else +%% +%% is turned into +%% +%% Sexp_dispatch +%% ?e +%% (lambda h t -> ?e-node) +%% (lambda n -> ?e-symbol) +%% (lambda _ -> ?e-else) +%% (lambda _ -> ?e-else) +%% (lambda _ -> ?e-else) +%% (lambda _ -> ?e-else) +%% (lambda _ -> ?e-else) +%% +%% TODO: allow subpatterns? +%% +%% sexp-case ?e +%% | node (symbol "_=>_") (cons pattern (cons expr nil)) => ?e-double-arrow +%% | _ => ?e-else +%% +sexp-case-impl : List Sexp -> Sexp; +sexp-case-impl = lambda args -> + let + not-bottom : Sexp; + not-bottom = Sexp_symbol "_|_"; + + sexp-symbol-name : Sexp -> Option String; + sexp-symbol-name = lambda perhaps-a-symbol -> + let none-string = none (a := String) + in + Sexp_dispatch + perhaps-a-symbol + (lambda _ -> lambda _ -> none-string) + (lambda name -> some name) + (lambda _ -> none-string) + (lambda _ -> none-string) + (lambda _ -> none-string) + (lambda _ -> none-string) + ; + + parse-node-pattern : + SexpCaseAcc -> + Sexp -> + List Sexp -> + Result SexpCaseAcc String + ; + parse-node-pattern = lambda acc -> lambda expr -> lambda pargs -> + case pargs + | nil => err "todo 1" + | cons head-var pargs' => + case pargs' + | nil => err "todo 2" + | cons tail-var pargs'' => + case pargs'' + | cons _ _ => err "todo 3" + | nil => + case acc + | sexp-case-acc na sym-a str-a ia fa ba oe => + case na + | some _ => err "todo 4" + | none => + let na' = some (node-acc head-var tail-var expr) + in ok (sexp-case-acc na' sym-a str-a ia fa ba oe) + ; + + parse-atom-pattern : + String -> + (Sexp -> Result SexpCaseAcc String) -> + List Sexp -> + Result SexpCaseAcc String + ; + parse-atom-pattern = + lambda pattern-name -> lambda update-acc -> lambda pargs -> + case pargs + | nil => + err (String_concat "missing binding for pattern " pattern-name) + | cons var pargs' => + case pargs' + | cons _ _ => + err (String_concat "too many bindings for pattern " pattern-name) + | nil => + update-acc var + ; + + update-symbol-acc : SexpCaseAcc -> Sexp -> Sexp -> Result SexpCaseAcc String; + update-symbol-acc = lambda acc -> lambda expr -> lambda var -> + case acc + | sexp-case-acc na sym-a str-a ia fa ba oe => + case sym-a + | some _ => err "multiple symbol patterns" + | none => + let sym-a' = some (atom-acc var expr) + in ok (sexp-case-acc na sym-a' str-a ia fa ba oe) + ; + + update-string-acc : SexpCaseAcc -> Sexp -> Sexp -> Result SexpCaseAcc String; + update-string-acc = lambda acc -> lambda expr -> lambda var -> + case acc + | sexp-case-acc na sym-a str-a ia fa ba oe => + case str-a + | some _ => err "multiple string patterns" + | none => + let str-a' = some (atom-acc var expr) + in ok (sexp-case-acc na sym-a str-a' ia fa ba oe) + ; + + update-int-acc : SexpCaseAcc -> Sexp -> Sexp -> Result SexpCaseAcc String; + update-int-acc = lambda acc -> lambda expr -> lambda var -> + case acc + | sexp-case-acc na sym-a str-a ia fa ba oe => + case ia + | some _ => err "multiple int patterns" + | none => + let ia' = some (atom-acc var expr) + in ok (sexp-case-acc na sym-a str-a ia' fa ba oe) + ; + + update-float-acc : SexpCaseAcc -> Sexp -> Sexp -> Result SexpCaseAcc String; + update-float-acc = lambda acc -> lambda expr -> lambda var -> + case acc + | sexp-case-acc na sym-a str-a ia fa ba oe => + case fa + | some _ => err "multiple float patterns" + | none => + let fa' = some (atom-acc var expr) + in ok (sexp-case-acc na sym-a str-a ia fa' ba oe) + ; + + update-block-acc : SexpCaseAcc -> Sexp -> Sexp -> Result SexpCaseAcc String; + update-block-acc = lambda acc -> lambda expr -> lambda var -> + case acc + | sexp-case-acc na sym-a str-a ia fa ba oe => + case ba + | some _ => err "multiple block patterns" + | none => + let ba' = some (atom-acc var expr) + in ok (sexp-case-acc na sym-a str-a ia fa ba' oe) + ; + + parse-otherwise-pattern : + SexpCaseAcc -> + Sexp -> + List Sexp -> + Result SexpCaseAcc String + ; + parse-otherwise-pattern = lambda acc -> lambda expr -> lambda pargs -> + case pargs + | cons _ _ => err "stray syntax after _" + | nil => + case acc + | sexp-case-acc na sym-a str-a ia fa ba _ => + ok (sexp-case-acc na sym-a str-a ia fa ba expr) + ; + + parse-pattern : + SexpCaseAcc -> + Sexp -> + Sexp -> + List Sexp -> + Result SexpCaseAcc String + ; + parse-pattern = lambda acc -> lambda expr -> lambda head -> lambda tail -> + case sexp-symbol-name head + | none => err "not a symbol" + | some name => + case String_eq name "node" + | true => + parse-node-pattern acc expr tail + | false => + case String_eq name "symbol" + | true => + parse-atom-pattern "symbol" (update-symbol-acc acc expr) tail + | false => + case String_eq name "string" + | true => + parse-atom-pattern "string" (update-string-acc acc expr) tail + | false => + case String_eq name "int" + | true => + parse-atom-pattern "int" (update-int-acc acc expr) tail + | false => + case String_eq name "float" + | true => + parse-atom-pattern "float" (update-float-acc acc expr) tail + | false => + case String_eq name "block" + | true => + parse-atom-pattern "block" (update-block-acc acc expr) tail + | false => + case String_eq name "_" + | true => + parse-otherwise-pattern acc expr tail + | false => err "_" + ; + + parse-arm : SexpCaseAcc -> Sexp -> List Sexp -> Result SexpCaseAcc String; + parse-arm = lambda acc -> lambda head -> lambda tail -> + case sexp-symbol-name head + | none => err "expected patterns and expressions to be delineated by `=>`" + | some head-name => + case String_eq head-name "_=>_" + | false => + err + (String_concat + "expected patterns and expressions to be delineated by `=>`, but I see `" + (String_concat head-name "`")) + | true => + case tail + | nil => err "todo 13" + | cons pattern tail' => + case tail' + | nil => err "todo 14" + | cons expr tail'' => + case tail'' + | cons _ _ => err "todo 15" + | nil => + Sexp_dispatch + pattern + (parse-pattern acc expr) + (lambda _ -> parse-pattern acc expr pattern nil) + (lambda _ -> err "invalid pattern: string") + (lambda _ -> err "invalid pattern: int") + (lambda _ -> err "invalid pattern: float") + (lambda _ -> err "invalid pattern: block") + ; + + parse-arms : List Sexp -> Result SexpCaseAcc String; + parse-arms = lambda arms -> + let + loop : List Sexp -> SexpCaseAcc -> Result SexpCaseAcc String; + loop = lambda arms -> lambda acc -> + case arms + | nil => ok acc + | cons arm arms => + let + result : Result SexpCaseAcc String; + result = + Sexp_dispatch + arm + (parse-arm acc) + (lambda _ -> err "invalid arm: symbol") + (lambda _ -> err "invalid arm: string") + (lambda _ -> err "invalid arm: int") + (lambda _ -> err "invalid arm: float") + (lambda _ -> err "invalid arm: block") + ; + in + case result + | (err (α := SexpCaseAcc) (β := String)) _ => result + | (ok (α := SexpCaseAcc) (β := String)) acc => loop arms acc + ; + + missing-wildcard : Sexp; + missing-wildcard = Sexp_symbol "missing wildcard pattern"; + in + loop arms (sexp-case-acc none none none none none none missing-wildcard) + ; + + expand-sexp-case : Sexp -> List Sexp -> Sexp; + expand-sexp-case = lambda head -> lambda tail -> + case Sexp_eq head not-bottom + | false => Sexp_symbol "expected arms delineated by `|`" + | true => + case tail + | nil => Sexp_symbol "expected at least one arm" + | cons target arms => + case parse-arms arms + | (err (α := SexpCaseAcc) (β := String)) message => + let message = String_concat "<error: " (String_concat message ">") + in Sexp_symbol message + | (ok (α := SexpCaseAcc) (β := String)) acc => + sexp<-sexp-case-acc target acc + ; + in + case args + | nil => Sexp_symbol "todo" + | cons head tail => + case tail + | nil => + Sexp_dispatch + head + expand-sexp-case + (lambda _ -> Sexp_symbol "invalid case expression: symbol") + (lambda _ -> Sexp_symbol "invalid case expression: string") + (lambda _ -> Sexp_symbol "invalid case expression: int") + (lambda _ -> Sexp_symbol "invalid case expression: float") + (lambda _ -> Sexp_symbol "invalid case expression: block") + | cons _ _ => Sexp_symbol "todo" +;

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/ab7984ee22961868b0346b69c1c34e070...