Jonathan Graveline pushed to branch graveline at Stefan / Typer

Commits: 9fd7015b by Jonathan Graveline at 2018-08-31T21:25:07Z Revised comments and documentation from btl/ and samples/

- - - - -

10 changed files:

- btl/builtins.typer - btl/case.typer - btl/do.typer - btl/plain-let.typer - btl/tuple.typer - samples/bbst.typer - samples/decltype.typer - samples/math.typer - samples/myers.typer - samples/table.typer

Changes:

===================================== btl/builtins.typer ===================================== @@ -222,7 +222,7 @@ Parser_custom = Built-in "Parser.custom" : Elab_Context -> Sexp -> List Sexp; %% %% Parse an Sexp with the latest context %% -%% (I think previous top level definition should be in the context) +%% (Previous top level definition should be in the context) %% Parser_newest = Built-in "Parser.newest" : Sexp -> List Sexp;

@@ -308,15 +308,34 @@ Sys_exit = Built-in "Sys.exit" : Int -> IO Unit; %% Ref = typecons (Ref (a : Type)) (Ref a); %%

+%% +%% Takes a value +%% Returns a value modifiable in the IO monad +%% and which already contain the specified value +%% Ref_make = Built-in "Ref.make" : (a : Type) ≡> a -> IO (Ref a); + +%% +%% Takes a Ref +%% Returns in the IO monad the value in the Ref +%% Ref_read = Built-in "Ref.read" : (a : Type) ≡> Ref a -> IO a; + +%% +%% Takes a value and a Ref +%% Returns the an empty command +%% and set the Ref to contain specified value +%% Ref_write = Built-in "Ref.write" : (a : Type) ≡> a -> Ref a -> IO Unit;

%% %% gensym for macro +%% %% Generate pseudo-unique symbol -%% At least they cannot be obtained outside macro -%% In macro you should NOT use symbol of the form " %gensym% ..." +%% +%% At least they cannot be obtained outside macro. +%% In macro you should NOT use symbol of the form " %gensym% ...". +%% Assume the tree dots to be anything. %% gensym = Built-in "gensym" : Unit -> IO Sexp;

@@ -373,7 +392,6 @@ Elab_debug-doc = Built-in "Elab.debug-doc" : String -> Elab_Context -> String;

%% %% Print message and/or fail (terminate) -%% These messages are registered like any other error %% And location is printed before the error %%

===================================== btl/case.typer ===================================== @@ -13,6 +13,10 @@ %%%% %%%% Another problem is that this macro is dependent of tuple implementation %%%% +%%%% (It is important to match every variable only once because Typer code +%%%% must always return a value. We cannot just translate to `if then else` +%%%% like construction. Otherwise what will we do if nothing match?) +%%%%

%% %% Move IO outside List (from element to List) @@ -45,7 +49,8 @@ gen-vars vars = io-list (List_map %% %% Constructor for a tuple %% -%% Used in patterns +%% Used in patterns to match +%% (expand-tuple-ctor, is-tuple, ...) %% tuple-ctor : Sexp; tuple-ctor = let @@ -81,8 +86,8 @@ in Sexp_dispatch sexp %% %% Is tuple %% -is-tuple : Sexp -> Bool; -is-tuple sexp = let +tuple? : Sexp -> Bool; +tuple? sexp = let

sfalse = (lambda _ -> false);

@@ -99,7 +104,8 @@ in Sexp_dispatch sexp %% case ... | (expr3,expr4,...) => ... %% %% (This function is now doing nothing since there's only one -%% variable at any time: one expression or a tuple of expressions) +%% variable at any time: one expression or a tuple of expressions. +%% It used to be more useful.) %% get-tup-exprs : Sexp -> List Sexp; get-tup-exprs sexp = let @@ -132,8 +138,8 @@ Code_error = Sexp_symbol "<code error>"; dflt-var : Var; dflt-var = Sexp_symbol "_";

-is-dflt : Var -> Bool; -is-dflt v = Sexp_eq dflt-var v; +dflt? : Var -> Bool; +dflt? v = Sexp_eq dflt-var v;

%% %% Takes a list of variable to match and a list of branch as "_=>_"-node @@ -278,7 +284,7 @@ renamed-pat pat names = let %% single expression %% tup : Bool; - tup = is-tuple pat; + tup = tuple? pat;

%% %% Get the name of the n'th element of any tuple @@ -375,8 +381,8 @@ in Sexp_dispatch pat %% Takes two pattern and return true if the two pattern %% has the same constructor %% -is-same-ctor : Pat -> Pat -> Bool; -is-same-ctor p0 p1 = let +same-ctor? : Pat -> Pat -> Bool; +same-ctor? p0 p1 = let

%% %% error used in Sexp_dispatch @@ -482,7 +488,7 @@ wrap-vars rhs lhs fun = List_fold2 (lambda fun v0 v1 ->

%% %% Take a List of branches and return a List of the first pattern in each branches -%% (I must keep the order from input to ouput) +%% (The order must be kept from input to ouput) %% head-pats : List (Pair Pats Code) -> List Pat; head-pats ps = let @@ -569,7 +575,7 @@ pattern-sub-pats-vars rvars branches = let (IO_return (List_mapi (lambda c n -> let new-sym = List_nth n rvars Var_error; prev-sym = List_nth n psubs dflt-var; - in if (is-dflt c) then (prev-sym) else (new-sym) + in if (dflt? c) then (prev-sym) else (new-sym) ) subs)); };

@@ -587,7 +593,7 @@ pattern-term pat rvars = let

ff : List (Pair Var Var) -> Var -> Var -> List (Pair Var Var); ff o v0 v1 = - if (is-dflt v0) then + if (dflt? v0) then (o) else (List_concat o (cons (pair v0 v1) nil)); @@ -602,10 +608,13 @@ in do { %% Type of one partition of branches (one branch with child branches) %% %% Pair of -%% Triplet of renamed pat, -%% original variable, -%% variables old/new and original pattern in each branch -%% List of next branch +%% Triplet of renamed pattern, +%% variables from renamed pattern, (list "A") +%% (old, new) variables and original pattern in each branch (list "B") +%% List of next branch (list "C") +%% +%% 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));

@@ -613,6 +622,10 @@ part-type = Pair (Triplet Pat (List Var) (List (Pair Pat (List (Pair Var Var)))) %% Takes a list of branches (pair of (patterns, body)) %% Return a list of partition %% +%% Partitioning is done according to `similar?` pattern +%% for exemple: `cons x xs` is similar to `cons y nil`, +%% even if we may later need to match `xs` or whatever to `nil`. +%% partition-branches : List (Pair Pats Code) -> IO (List part-type); partition-branches branches = let

@@ -643,8 +656,10 @@ partition-branches branches = let %% %% Type for first step partition %% - %% Pair of List sorted with similar head - %% they are similar when they have the same constructor + %% Pair of List with similar head + %% they are similar when they have the same constructor. + %% + %% Pair "similar patterns" "child of similar patterns" %% pre-part-type = Pair (List Pat) (List (Pair Pats Code));

@@ -655,8 +670,8 @@ partition-branches branches = let pre-parts : List pre-part-type; pre-parts = let

- is-similar : Pat -> Pat -> Bool; - is-similar p0 p1 = is-same-ctor p0 p1; + similar? : Pat -> Pat -> Bool; + similar? p0 p1 = same-ctor? p0 p1;

ff : List pre-part-type -> Pair Pat (Pair Pats Code) -> List pre-part-type; ff o p = case p | pair pat tail => (case o @@ -666,13 +681,13 @@ partition-branches branches = let %% default is both equivalent and different from every pattern? %% they are merged with `merge-dflt`

- if (is-dflt pat) then + if (dflt? pat) then (case part | pair pp tt => cons (pair (List_concat pp (cons pat nil)) (List_concat tt (cons tail nil))) (ff parts p)) % This line sometimes produce too many patterns else - (if (is-similar pat (List_nth 0 ps Pat_error)) then + (if (similar? pat (List_nth 0 ps Pat_error)) then (case part | pair pp tt => cons (pair (List_concat pp (cons pat nil)) (List_concat tt (cons tail nil))) @@ -685,6 +700,9 @@ partition-branches branches = let %% %% `pre-part-type` to `part-type` %% + %% We here add precomputed info about `similar?` patterns. + %% See `part-type` definition to know which information we must preserve. + %% parts : IO (List part-type); parts = let

@@ -725,7 +743,7 @@ in do { %% %% There's a need to merge branch because default branch may be anywhere %% -%% (I tried to consider default branches similar to every patterns +%% (I tried to consider default branches `similar?` to every patterns %% but it failed in some way. So here we are...) %% merge-dflt : List part-type -> Option part-type -> List part-type; @@ -741,9 +759,12 @@ merge-dflt parts odflt = let %% exemple: %% | (x,_,y) => ... %% | (x,k,z) => ... + %% %% In this exemple (and in Typer) I can suppose `y != z` (or there will be warning/error) %% If we take the first case first we did not match `k` and cannot jump to the next - %% But since `y != z` we can safely take the second first + %% But since `y != z` we can safely take the second first. + %% + %% In other word, we can match (k,z) before (_,y) and fall back if k or z did not match. %% preppend : Pat -> List (Pair Pat (List (Pair Var Var))) -> List (Pair Pats Code) -> part-type -> part-type; @@ -758,6 +779,10 @@ merge-dflt parts odflt = let %% | (x,_,z) => ... %% | (x,_,_) => ... %% + %% Obviously (_,_) will always match so we need to test (_,z) first. + %% (Kind of thing possibly done with "_" `similar?` to everything + %% but we would need `preppend` anyway) + %% append : Pat -> List (Pair Pat (List (Pair Var Var))) -> List (Pair Pats Code) -> part-type -> part-type; append pat vars branches part = case part @@ -767,7 +792,7 @@ merge-dflt parts odflt = let in case parts | cons part parts => (case part | pair p pp => (case p | triplet pat _ vars => - if (is-dflt pat) then + if (dflt? pat) then (case odflt | some dflt => merge-dflt parts (some (append pat vars pp dflt)) | none => merge-dflt parts (some part)) @@ -783,8 +808,8 @@ in case parts %% %% Takes some branches and preppend default variable to smaller branches %% -%% (Sub-pattern introduce new variable but if -%% it fail suplementary variable must match something else) +%% (Sub-pattern introduce new variable so if +%% it fail suplementary variable must match something else (i.e. default: "_")) %% adjust-len : List (Pair Pats Code) -> List (Pair Pats Code); adjust-len branches = let @@ -875,7 +900,7 @@ compile-case subjects branches = let sub-pats-vars <- sub-pats-vars;

sub-pats <- IO_return (List_fold2 (lambda o pat var -> - if (is-dflt var) then + if (dflt? var) then (o) else (List_concat o (cons pat nil)) @@ -903,7 +928,7 @@ compile-case subjects branches = let %%

r <- IO_return (List_foldl (lambda o v -> - if (is-dflt v) then + if (dflt? v) then (o) else (List_concat o (cons v nil))

===================================== btl/do.typer ===================================== @@ -98,8 +98,8 @@ in node; %% this way a-sym is defined within b-op and so on %% a-sym is now just `a` and not `IO a` %% -%% ( It could be possible to use `IO Ref` rather than a new variable -%% for each command, but will it be useful? ) +%% (It could be possible to use `IO Ref` rather than a new variable +%% for each command with same lhs symbol, but will it be useful?) %%

%%

===================================== btl/plain-let.typer ===================================== @@ -20,6 +20,7 @@

%% %% Takes the plain argument of macro `plain-let` +%% Returns the `plain-let` code %% impl : List Sexp -> IO Sexp; impl args = let

===================================== btl/tuple.typer ===================================== @@ -65,7 +65,7 @@ gen-vars vars = io-list (List_map %% Reference for tuple's implicit field name %% %% Takes a list of vars (it could actually only takes a length) -%% Returns symbol `%n` with n from 0 to the length of the argument +%% Returns symbol `%n` with n in [0,length) (integer only, obviously) %% gen-tuple-names : List Sexp -> List Sexp; gen-tuple-names vars = List_mapi @@ -122,7 +122,7 @@ in IO_return (Sexp_node (Sexp_symbol "__.__") (cons tup (cons elem-sym nil))) %% syntax: %% (x, y, z) <- p; %% -%% and then `x`, `y`, `z` are defined from tuple's element 0, 1, 2 +%% and then `x`, `y`, `z` are defined as tuple's element 0, 1, 2 %% assign-tuple = macro (lambda args -> let

@@ -153,7 +153,7 @@ in do { });

%% -%% Wrap the third argument (`fun`) with a `let` definition for each variables +%% Wrap the third argument `fun` with a `let` definition for each variables %% Names are taken from `rvars` and definition are taken from `ivars` %%

===================================== samples/bbst.typer ===================================== @@ -144,7 +144,9 @@ length tree = case tree empty? tree = (Int_eq (length tree) 0);

%% -%% Check if two value are equal with comparison function only +%% Check if two value are equal with ordering function only +%% +%% (As stated previously: ordering function must be like "<=" or ">=") %%

comp-equal : (a : Type) ≡> (a -> a -> Bool) -> a -> a -> Bool; @@ -286,8 +288,10 @@ insert elem tree = let | node-leaf => node3 d0 e k0 node-leaf node-leaf | _ => node2 d0 k0 (helper comp e k1))

+ %% %% When doing a recursion I try not to call helper on a node4 %% Because we then would need the parent of this node4 + %%

| node3 d0 d1 k0 k1 k2 => if (comp e d0) then @@ -371,8 +375,10 @@ insert elem tree = let | _ => node3 d0 d1 k0 k1 (helper comp e k2)))

| node4 d0 d1 d2 k0 k1 k2 k3 => - %% I need the parent of "p" + %% + %% I need the parent of `p` %% But it seems to work with other branch (see above) + %% helper comp e (node2 d1 (node2 d0 k0 k1) (node2 d2 k2 k3))

| node-leaf => node2 e node-leaf node-leaf; @@ -425,7 +431,7 @@ pop-leftmost' comp tree = let in (helper tree);

%% -%% Remove the smallest element +%% Remove the smallest element (when using "<=") %%

pop-leftmost : (a : Type) ≡> Bbst a -> Bbst a; @@ -476,7 +482,7 @@ pop-rightmost' comp tree = let in (helper tree);

%% -%% Remove the greatest element +%% Remove the greatest element (when using "<=") %%

pop-rightmost : (a : Type) ≡> Bbst a -> Bbst a; @@ -526,7 +532,7 @@ get-leftmost' comp tree = let in (helper tree);

%% -%% Get smallest element +%% Get smallest element (when using "<=") %%

get-leftmost : (a : Type) ≡> Bbst a -> Option a; @@ -573,7 +579,7 @@ get-rightmost' comp tree = let in (helper tree);

%% -%% Get greatest element +%% Get greatest element (when using "<=") %%

get-rightmost : (a : Type) ≡> Bbst a -> Option a;

===================================== samples/decltype.typer ===================================== @@ -42,9 +42,10 @@ take-str : (decl-type str-var) -> (decl-type "123"); take-str s = String_concat s s;

%% -%% This is the first exemple where we really need -%% type annotation (with current `##case_`) +%% Next are exemple where we really need +%% type annotation %% + take-bool : (decl-type bool-var) -> (decl-type true); take-bool b = case b | true => false

===================================== samples/math.typer ===================================== @@ -13,20 +13,22 @@ %% With this function we could remove built-in function Int->String %%

+Int2String-lut : Array String; +Int2String-lut = list.List->Array + (cons "0" (cons "1" (cons "2" (cons "3" (cons "4" + (cons "5" (cons "6" (cons "7" (cons "8" (cons "9" nil) + ))))))))); + Int2String : Int -> String; Int2String x = let

- lut : List String; - lut = cons "0" (cons "1" (cons "2" (cons "3" (cons "4" - (cons "5" (cons "6" (cons "7" (cons "8" (cons "9" nil) - )))))))); - helper : Int -> String; helper x = if (Int_eq x 0) then ("") else - (String_concat (helper (x / 10)) (List_nth (Int_mod x 10) lut "error")); + (String_concat (helper (x / 10)) + (Array_get "error" (Int_mod x 10) Int2String-lut));

in if (Int_eq x 0) then ("0")

===================================== samples/myers.typer ===================================== @@ -98,7 +98,7 @@ nth n l = car (nthcdr n l); set-nth : (a : Type) ≡> Int -> a -> t a -> t a; set-nth n v l = let

- % I should use the new case_ macro here! + %% I should use the new case_ macro here!

type Helper (a : Type) | pat1 (idx : Int) (data : a) (link1 : t a) (i : Int) (link2 : t a) @@ -229,7 +229,7 @@ map f l = let in foldr fp l mnil;

%% -%% Apply all element of a Myers list to a user function +%% Apply all element of a Myers list to a user function (one by one) %% Takes a function and a list %% Returns the length of the list %%

===================================== samples/table.typer ===================================== @@ -43,9 +43,6 @@ in case t %% %% Get the number of element in the tree %% -%% (we could easily keep track of element inserted and removed) -%% (currently O(n)) -%%

%% length t = let %% fold-fun len _ = len + 1;

View it on GitLab: https://gitlab.com/monnier/typer/commit/9fd7015bd8c351d3a0fb5aa68a2fc6a6d56a...