Jonathan Graveline pushed to branch graveline at Stefan / Typer

Commits: 4191f41f by Jonathan Graveline at 2018-08-01T02:22:54Z new built-in function `Parser_*` and use it in do.typer

- - - - - 38b621d2 by Jonathan Graveline at 2018-08-01T16:12:25Z use `if...then...else...` syntax where appropriate

udict and odict (from table and bbst) for convenience

- - - - - 28006ea4 by Jonathan Graveline at 2018-08-01T17:33:28Z define operator `<-`, use it in do.typer and tuple.typer

tuple now working with `,` (needed escape: `_,_`)

- - - - -

9 changed files:

- btl/builtins.typer - btl/case.typer - btl/do.typer - btl/pervasive.typer - btl/plain-let.typer - btl/tuple.typer - samples/bbst.typer - samples/table.typer - src/eval.ml

Changes:

===================================== btl/builtins.typer ===================================== @@ -202,6 +202,10 @@ Sexp_dispatch = Built-in "Sexp.dispatch"

Parser_default = Built-in "Parser.default" : Sexp -> List Sexp;

+Parser_custom = Built-in "Parser.custom" : Elab_Context -> Sexp -> List Sexp; + +Parser_newest = Built-in "Parser.newest" : Sexp -> List Sexp; + %%%% Array (without IO, but they could be added easily)

Array_append = Built-in "Array.append" : (a : Type) ≡> a -> Array a -> Array a;

===================================== btl/case.typer ===================================== @@ -200,16 +200,18 @@ introduced-vars pat = let ff o v = Sexp_dispatch v (lambda s ss -> do { o <- o; % bind - if_then_else_ (Sexp_eq s (Sexp_symbol "_:=_")) + if (Sexp_eq s (Sexp_symbol "_:=_")) then (return (List_concat o (cons (List_nth 1 ss Var_error) nil))) + else (return (List_concat o (cons dflt-var nil))); }) (lambda s -> do { o <- o; % bind sym <- return (Sexp_symbol s); b <- is-pat sym; - if_then_else_ (b) + if (b) then (return (List_concat o (cons dflt-var nil))) + else (return (List_concat o (cons sym nil))); }) serr serr serr serr; @@ -270,8 +272,9 @@ pattern-sub-pats pat = let map-arg : Var -> IO Var; map-arg arg = do { b <- is-pat arg; - if_then_else_ (b) + if (b) then (return arg) + else (return dflt-var); };

@@ -317,12 +320,13 @@ pattern-sub-pats-vars rvars branches = let psubs <- psubs; subs <- subs;

- if_then_else_ (List_empty subs) + if (List_empty subs) then (return psubs) + else (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_then_else_ (is-dflt c) (prev-sym) (new-sym) + in if (is-dflt c) then (prev-sym) else (new-sym) ) subs)); };

@@ -575,8 +579,9 @@ compile-case subjects branches = let sub-pats-vars <- sub-pats-vars;

sub-pats <- return (List_fold2 (lambda o pat var -> - if_then_else_ (is-dflt var) + if (is-dflt var) then (o) + else (List_concat o (cons pat nil)) ) nil sub-pats sub-pats-vars);

@@ -600,8 +605,9 @@ compile-case subjects branches = let %% variable without any corresponding sub pattern

r <- return (List_foldl (lambda o v -> - if_then_else_ (is-dflt v) + if (is-dflt v) then (o) + else (List_concat o (cons v nil)) ) nil r); return r;

===================================== btl/do.typer ===================================== @@ -17,7 +17,7 @@ %% do may contain do because it returns a command. %%

-assign = Sexp_symbol "<-"; +assign = Sexp_symbol "_<-_";

get-sym : Sexp -> Sexp; get-sym sexp = let @@ -25,8 +25,8 @@ get-sym sexp = let dflt-sym = (lambda _ -> (Sexp_symbol " %not used% "));

in Sexp_dispatch sexp - (lambda s ss -> if (Sexp_eq (List_nth 0 ss Sexp_error) assign) then - (s) + (lambda s ss -> if (Sexp_eq s assign) then + (List_nth 0 ss Sexp_error) else (dflt-sym ())) dflt-sym dflt-sym dflt-sym @@ -39,7 +39,7 @@ get-op sexp = let

helper = (lambda sexp -> Sexp_dispatch sexp

- ( lambda s ss -> if (Sexp_eq (List_nth 0 ss Sexp_error) assign) then + ( lambda s ss -> if (Sexp_eq s assign) then (Sexp_node (List_nth 1 ss Sexp_error) (List_tail (List_tail ss))) else (Sexp_node s ss) @@ -63,7 +63,7 @@ get-decl args = let

(lambda _ _ -> cons Sexp_error nil) err err err err

- (lambda l -> Parser_default l); + (lambda l -> Parser_newest l);

in node;

===================================== btl/pervasive.typer ===================================== @@ -525,6 +525,10 @@ test4 : Option Int; test4 = test1 : Option ?; test3 = test4;

+%%%% `<-` operator used in macro `do` and for tuple assignment + +define-operator "<-" 80 96; + %%%% %%%% Common library %%%%

===================================== btl/plain-let.typer ===================================== @@ -1,10 +1,7 @@ %%%% %%%% Macro `plain-let` %%%% -%%%% normal `let` but not recursive nor sequential -%%%% -%%%% (currently handle definition with `_=_`) -%%%% (would declaration be useful ? (e.g. `_:_`)) +%%%% basic `let` but not recursive nor sequential %%%%

%% List_nth = list.nth;

===================================== btl/tuple.typer ===================================== @@ -69,35 +69,6 @@ gen-deduce vars = List_map (lambda _ -> Sexp_symbol "?") vars;

-make-tuple : List Sexp -> IO Sexp; -make-tuple values = let - - mf1 : Sexp -> Sexp -> Sexp; - mf1 name value = Sexp_node (Sexp_symbol "_::_") (cons name (cons value nil)); - - mf2 : Sexp -> Sexp; - mf2 value = Sexp_node (Sexp_symbol "_:=_") (cons (Sexp_symbol "_") (cons value nil)); - -in do { - args <- gen-vars values; - names <- IO_return (gen-tuple-names values); - fun <- IO_return (Sexp_node (Sexp_symbol "lambda_->_") - (cons (Sexp_node (List_nth 0 args Sexp_error) (List_tail args)) (cons - (Sexp_node (Sexp_symbol "typecons") (cons (Sexp_symbol "_") - (cons (Sexp_node (Sexp_symbol "cons") (List_map2 mf1 names args)) nil))) - nil)) - ); - call-fun <- IO_return (Sexp_node fun (gen-deduce values)); - tuple <- IO_return (Sexp_node (Sexp_symbol "##datacons") - (cons call-fun (cons (Sexp_symbol "cons") nil))); - affect <- IO_return (Sexp_node tuple (List_map mf2 values)); - IO_return affect; -}; - -_:_ = macro (lambda args -> - make-tuple args -); - %%% %%% Access one tuple's element %%% @@ -128,10 +99,54 @@ in IO_return (Sexp_node (Sexp_symbol "__.__") (cons tup (cons elem-sym nil))) %%% Affectation, unwraping tuple %%%

-%% _=_ = macro (lambda args -> -%% -%% ); +_<-_ = macro (lambda args -> let

+ xserr = lambda _ -> (nil : List Sexp);

+ 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; + + 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 IO_return (Sexp_node (Sexp_symbol "_;_") (List_mapi + (mf (List_nth 1 args Sexp_error)) + (get-tup-elem (List_nth 0 args Sexp_error)))) +); + +make-tuple : List Sexp -> IO Sexp; +make-tuple values = let + + mf1 : Sexp -> Sexp -> Sexp; + mf1 name value = Sexp_node (Sexp_symbol "_::_") (cons name (cons value nil)); + + mf2 : Sexp -> Sexp; + mf2 value = Sexp_node (Sexp_symbol "_:=_") (cons (Sexp_symbol "_") (cons value nil));

+in do { + args <- gen-vars values; + names <- IO_return (gen-tuple-names values); + fun <- IO_return (Sexp_node (Sexp_symbol "lambda_->_") + (cons (Sexp_node (List_nth 0 args Sexp_error) (List_tail args)) (cons + (Sexp_node (Sexp_symbol "typecons") (cons (Sexp_symbol "_") + (cons (Sexp_node (Sexp_symbol "cons") (List_map2 mf1 names args)) nil))) + nil)) + ); + call-fun <- IO_return (Sexp_node fun (gen-deduce values)); + tuple <- IO_return (Sexp_node (Sexp_symbol "##datacons") + (cons call-fun (cons (Sexp_symbol "cons") nil))); + affect <- IO_return (Sexp_node tuple (List_map mf2 values)); + IO_return affect; +};

+_,_ = macro (lambda args -> + make-tuple args +);

===================================== samples/bbst.typer ===================================== @@ -146,9 +146,11 @@ is-empty tree = (Int_eq (length tree) 0); %%

comp-equal : (a : Type) ≡> (a -> a -> Bool) -> a -> a -> Bool; -comp-equal comp x y = if_then_else_ (comp x y) - (comp y x) - (false); +comp-equal comp x y = + if (comp x y) then + (comp y x) + else + (false);

%% %% Find an element in the tree and return it @@ -160,34 +162,46 @@ find elem tree = let helper : (a -> a -> Bool) -> a -> BbsTree a -> Option a; helper comp elem tree = case tree | node2 d0 l0 l1 => - if_then_else_ (comp elem d0) - (if_then_else_ (comp d0 elem) - (some d0) + if (comp elem d0) then + (if (comp d0 elem) then + (some d0) + else (helper comp elem l0)) + else (helper comp elem l1) | node3 d0 d1 l0 l1 l2 => - if_then_else_ (comp elem d0) - (if_then_else_ (comp d0 elem) + if (comp elem d0) then + (if (comp d0 elem) then (some d0) + else (helper comp elem l0)) - (if_then_else_ (comp elem d1) - (if_then_else_ (comp d1 elem) + else + (if (comp elem d1) then + (if (comp d1 elem) then (some d1) + else (helper comp elem l1)) + else (helper comp elem l2)) | node4 d0 d1 d2 l0 l1 l2 l3 => - if_then_else_ (comp elem d0) - (if_then_else_ (comp d0 elem) + if (comp elem d0) then + (if (comp d0 elem) then (some d0) + else (helper comp elem l0)) - (if_then_else_ (comp elem d1) - (if_then_else_ (comp d1 elem) + else + (if (comp elem d1) then + (if (comp d1 elem) then (some d1) + else (helper comp elem l1)) - (if_then_else_ (comp elem d2) - (if_then_else_ (comp d2 elem) + else + (if (comp elem d2) then + (if (comp d2 elem) then (some d2) + else (helper comp elem l2)) + else (helper comp elem l3))) | node-leaf => none;

@@ -218,40 +232,54 @@ insert elem tree = let helper comp e p = case p

| node2 d0 k0 k1 => - if_then_else_ (comp e d0) - (if_then_else_ (comp d0 e) + if (comp e d0) then + (if (comp d0 e) then (node2 e k0 k1) + else (case k0 | node4 e0 e1 e2 l0 l1 l2 l3 => - if_then_else_ (comp e e0) - (if_then_else_ (comp e0 e) + if (comp e e0) then + (if (comp e0 e) then (node2 d0 (node4 e e1 e2 l0 l1 l2 l3) k1) + else (node3 e1 d0 (helper comp e (node2 e0 l0 l1)) (node2 e2 l2 l3) k1)) - (if_then_else_ (comp e e1) - (if_then_else_ (comp e1 e) + else + (if (comp e e1) then + (if (comp e1 e) then (node2 d0 (node4 e0 e e2 l0 l1 l2 l3) k1) + else (node3 e1 d0 (helper comp e (node2 e0 l0 l1)) (node2 e2 l2 l3) k1)) - (if_then_else_ (comp e e2) - (if_then_else_ (comp e2 e) + else + (if (comp e e2) then + (if (comp e2 e) then (node2 d0 (node4 e0 e1 e l0 l1 l2 l3) k1) + else (node3 e1 d0 (node2 e0 l0 l1) (helper comp e (node2 e2 l2 l3)) k1)) + else (node3 e1 d0 (node2 e0 l0 l1) (helper comp e (node2 e2 l2 l3)) k1))) | node-leaf => node3 e d0 node-leaf node-leaf k1 | _ => node2 d0 (helper comp e k0) k1)) + else (case k1 | node4 e0 e1 e2 l0 l1 l2 l3 => - if_then_else_ (comp e e0) - (if_then_else_ (comp e0 e) + if (comp e e0) then + (if (comp e0 e) then (node2 d0 k0 (node4 e e1 e2 l0 l1 l2 l3)) + else (node3 d0 e1 k0 (helper comp e (node2 e0 l0 l1)) (node2 e2 l2 l3))) - (if_then_else_ (comp e e1) - (if_then_else_ (comp e1 e) + else + (if (comp e e1) then + (if (comp e1 e) then (node2 d0 k0 (node4 e0 e e2 l0 l1 l2 l3)) + else (node3 d0 e1 k0 (helper comp e (node2 e0 l0 l1)) (node2 e2 l2 l3))) - (if_then_else_ (comp e e2) - (if_then_else_ (comp e2 e) + else + (if (comp e e2) then + (if (comp e2 e) then (node2 d0 k0 (node4 e0 e1 e l0 l1 l2 l3)) + else (node3 d0 e1 k0 (node2 e0 l0 l1) (helper comp e (node2 e2 l2 l3)))) + else (node3 d0 e1 k0 (node2 e0 l0 l1) (helper comp e (node2 e2 l2 l3))))) | node-leaf => node3 d0 e k0 node-leaf node-leaf | _ => node2 d0 k0 (helper comp e k1)) @@ -260,60 +288,82 @@ insert elem tree = let %% Because we then would need the parent of this node4

| node3 d0 d1 k0 k1 k2 => - if_then_else_ (comp e d0) - (if_then_else_ (comp d0 e) + if (comp e d0) then + (if (comp d0 e) then (node3 e d1 k0 k1 k2) + else (case k0 | node4 e0 e1 e2 l0 l1 l2 l3 => - if_then_else_ (comp e e0) - (if_then_else_ (comp e0 e) + if (comp e e0) then + (if (comp e0 e) then (node3 d0 d1 (node4 e e1 e2 l0 l1 l2 l3) k1 k2) + else (node4 e1 d0 d1 (helper comp e (node2 e0 l0 l1)) (node2 e2 l2 l3) k1 k2)) - (if_then_else_ (comp e e1) - (if_then_else_ (comp e1 e) + else + (if (comp e e1) then + (if (comp e1 e) then (node3 d0 d1 (node4 e0 e e2 l0 l1 l2 l3) k1 k2) + else (node4 e1 d0 d1 (helper comp e (node2 e0 l0 l1)) (node2 e2 l2 l3) k1 k2)) - (if_then_else_ (comp e e2) - (if_then_else_ (comp e2 e) + else + (if (comp e e2) then + (if (comp e2 e) then (node3 d0 d1 (node4 e0 e1 e l0 l1 l2 l3) k1 k2) + else (node4 e1 d0 d1 (node2 e0 l0 l1) (helper comp e (node2 e2 l2 l3)) k1 k2)) + else (node4 e1 d0 d1 (node2 e0 l0 l1) (helper comp e (node2 e2 l2 l3)) k1 k2))) | node-leaf => node4 e d0 d1 node-leaf node-leaf k1 k2 | _ => node3 d0 d1 (helper comp e k0) k1 k2)) - (if_then_else_ (comp e d1) - (if_then_else_ (comp d1 e) + else + (if (comp e d1) then + (if (comp d1 e) then (node3 d0 e k0 k1 k2) + else (case k1 | node4 e0 e1 e2 l0 l1 l2 l3 => - if_then_else_ (comp e e0) - (if_then_else_ (comp e0 e) + if (comp e e0) then + (if (comp e0 e) then (node3 d0 d1 k0 (node4 e e1 e2 l0 l1 l2 l3) k2) + else (node4 d0 e1 d1 k0 (helper comp e (node2 e0 l0 l1)) (node2 e2 l2 l3) k2)) - (if_then_else_ (comp e e1) - (if_then_else_ (comp e1 e) + else + (if (comp e e1) then + (if (comp e1 e) then (node3 d0 d1 k0 (node4 e0 e e2 l0 l1 l2 l3) k2) + else (node4 d0 e1 d1 k0 (helper comp e (node2 e0 l0 l1)) (node2 e2 l2 l3) k2)) - (if_then_else_ (comp e e2) - (if_then_else_ (comp e2 e) + else + (if (comp e e2) then + (if (comp e2 e) then (node3 d0 d1 k0 (node4 e0 e1 e l0 l1 l2 l3) k2) + else (node4 d0 e1 d1 k0 (node2 e0 l0 l1) (helper comp e (node2 e2 l2 l3)) k2)) + else (node4 d0 e1 d1 k0 (node2 e0 l0 l1) (helper comp e (node2 e2 l2 l3)) k2))) | node-leaf => node4 d0 e d1 k0 node-leaf node-leaf k2 | _ => node3 d0 d1 k0 (helper comp e k1) k2)) + else (case k2 | node4 e0 e1 e2 l0 l1 l2 l3 => - if_then_else_ (comp e e0) - (if_then_else_ (comp e0 e) + if (comp e e0) then + (if (comp e0 e) then (node3 d0 d1 k0 k1 (node4 e e1 e2 l0 l1 l2 l3)) + else (node4 d0 d1 e1 k0 k1 (helper comp e (node2 e0 l0 l1)) (node2 e2 l2 l3))) - (if_then_else_ (comp e e1) - (if_then_else_ (comp e1 e) + else + (if (comp e e1) then + (if (comp e1 e) then (node3 d0 d1 k0 k1 (node4 e0 e e2 l0 l1 l2 l3)) + else (node4 d0 d1 e1 k0 k1 (helper comp e (node2 e0 l0 l1)) (node2 e2 l2 l3))) - (if_then_else_ (comp e e2) - (if_then_else_ (comp e2 e) + else + (if (comp e e2) then + (if (comp e2 e) then (node3 d0 d1 k0 k1 (node4 e0 e1 e l0 l1 l2 l3)) + else (node4 d0 d1 e1 k0 k1 (node2 e0 l0 l1) (helper comp e (node2 e2 l2 l3)))) + else (node4 d0 d1 e1 k0 k1 (node2 e0 l0 l1) (helper comp e (node2 e2 l2 l3))))) | node-leaf => node4 d0 d1 e k0 k1 node-leaf node-leaf | _ => node3 d0 d1 k0 k1 (helper comp e k2))) @@ -325,11 +375,12 @@ insert elem tree = let

| node-leaf => node2 e node-leaf node-leaf;

-in if_then_else_ (member elem tree) - (case tree % we may want to replace an element (partial comparison function) - | bbst s c t => bbst s c (helper c elem t)) - (case tree - | bbst s c t => bbst (s + 1) c (helper c elem t)); +in if (member elem tree) then + (case tree % we may want to replace an element (partial comparison function) + | bbst s c t => bbst s c (helper c elem t)) + else + (case tree + | bbst s c t => bbst (s + 1) c (helper c elem t));

%% %% Remove the smallest element. Used in remove. @@ -606,46 +657,59 @@ remove elem tree = let helper comp elem tree = case tree | node2 d l0 l1 =>

- if_then_else_ (comp elem d) - (if_then_else_ (comp d elem) + if (comp elem d) then + (if (comp d elem) then (rebuild-two comp l0 l1) + else (node2 d (helper comp elem l0) l1)) + else (node2 d l0 (helper comp elem l1))

| node3 d0 d1 l0 l1 l2 =>

- if_then_else_ (comp elem d0) - (if_then_else_ (comp d0 elem) + if (comp elem d0) then + (if (comp d0 elem) then (rebuild-left-three comp d1 l0 l1 l2) % replace d0 + else (node3 d0 d1 (helper comp elem l0) l1 l2)) - (if_then_else_ (comp elem d1) - (if_then_else_ (comp d1 elem) + else + (if (comp elem d1) then + (if (comp d1 elem) then (rebuild-right-three comp d0 l0 l1 l2) % replace d1 + else (node3 d0 d1 l0 (helper comp elem l1) l2)) + else (node3 d0 d1 l0 l1 (helper comp elem l2)))

| node4 d0 d1 d2 l0 l1 l2 l3 =>

- if_then_else_ (comp elem d0) - (if_then_else_ (comp d0 elem) + if (comp elem d0) then + (if (comp d0 elem) then (rebuild-left-four comp d1 d2 l0 l1 l2 l3) + else (node4 d0 d1 d2 (helper comp elem l0) l1 l2 l3)) - (if_then_else_ (comp elem d1) - (if_then_else_ (comp d1 elem) + else + (if (comp elem d1) then + (if (comp d1 elem) then (rebuild-middle-four comp d0 d2 l0 l1 l2 l3) + else (node4 d0 d1 d2 l0 (helper comp elem l1) l2 l3)) - (if_then_else_ (comp elem d2) - (if_then_else_ (comp d2 elem) + else + (if (comp elem d2) then + (if (comp d2 elem) then (rebuild-right-four comp d0 d1 l0 l1 l2 l3) + else (node4 d0 d1 d2 l0 l1 (helper comp elem l2) l3)) + else (node4 d0 d1 d2 l0 l1 l2 (helper comp elem l3))))

| node-leaf => node-leaf;

-in if_then_else_ (member elem tree) - (case tree - | bbst s c t => bbst (s - 1) c (helper c elem t)) - (tree); +in if (member elem tree) then + (case tree + | bbst s c t => bbst (s - 1) c (helper c elem t)) + else + (tree);

%% %% An empty tree with a key compare function as argument @@ -654,6 +718,48 @@ in if_then_else_ (member elem tree) empty : (a : Type) ≡> (a -> a -> Bool) -> Bbst a; empty comp-fun = bbst 0 comp-fun node-leaf;

+%%% +%%% Ordered dictionary +%%% + +odict-comp : (Key : Type) ≡> (Data : Type) ≡> (Key -> Key -> Bool) -> + ((Pair Key (Option Data)) -> (Pair Key (Option Data)) -> Bool); +odict-comp c = (lambda p0 -> (lambda p1 -> + case p0 | pair k0 _ => + case p1 | pair k1 _ => c k0 k1)); + +odict : (Key : Type) ≡> (Data : Type) ≡> (Key -> Key -> Bool) -> + Bbst (Pair Key (Option Data)); +odict c = bbst 0 (odict-comp c) node-leaf; + +odict-length : (Key : Type) ≡> (Data : Type) ≡> Bbst (Pair Key (Option Data)) -> Int; +odict-length t = length t; + +odict-find : (Key : Type) ≡> (Data : Type) ≡> Key -> + Bbst (Pair Key (Option Data)) -> Option Data; +odict-find k t = case (find (pair k none) t) + | some (pair _ d) => d + | none => none; + +odict-insert : (Key : Type) ≡> (Data : Type) ≡> Key -> Data -> + Bbst (Pair Key (Option Data)) -> Bbst (Pair Key (Option Data)); +odict-insert k d t = insert (pair k (some d)) t; + +odict-member : (Key : Type) ≡> (Data : Type) ≡> Key -> + Bbst (Pair Key (Option Data)) -> Bool; +odict-member k t = member (pair k none) t; + +odict-remove : (Key : Type) ≡> (Data : Type) ≡> Key -> + Bbst (Pair Key (Option Data)) -> Bbst (Pair Key (Option Data)); +odict-remove k t = remove (pair k none) t; + +odict-update : (Key : Type) ≡> (Data : Type) ≡> Key -> Data -> + Bbst (Pair Key (Option Data)) -> Bbst (Pair Key (Option Data)); +odict-update k d t = insert (pair k (some d)) t; + +odict-is-empty : (Key : Type) ≡> (Data : Type) ≡> Bbst (Pair Key (Option Data)) -> Bool; +odict-is-empty t = is-empty t; + %%% %%% Test helper %%% @@ -675,8 +781,8 @@ int-range1 : Int -> Int -> Bbst Int; int-range1 min max = let

helper : Int -> Bbst Int -> Bbst Int; - helper min tree = if_then_else_ (Int_eq min max) - (tree) (helper (min + 1) (insert min tree)); + helper min tree = if (Int_eq min max) then + (tree) else (helper (min + 1) (insert min tree));

in helper min (empty int-comp);

@@ -694,9 +800,10 @@ int-range2 min max = let

a = insert (max - 1) tree;

- in if_then_else_ (Int_eq min max) - (a) - (helper (min + 1) (max - 1) (insert min a)); + in if (Int_eq min max) then + (a) + else + (helper (min + 1) (max - 1) (insert min a));

in helper min max (empty int-comp);

@@ -708,7 +815,7 @@ remove-range : Int -> Int -> Bbst Int -> Bbst Int; remove-range min max tree = let

helper : Int -> Bbst Int -> Bbst Int; - helper min tree = if_then_else_ (Int_eq min max) - (tree) (helper (min + 1) (remove min tree)); + helper min tree = if (Int_eq min max) then + (tree) else (helper (min + 1) (remove min tree));

in helper min tree;

===================================== samples/table.typer ===================================== @@ -22,11 +22,11 @@ type Table (a : Type) | table (s : Int) (c : a -> a -> Bool) (h : a -> Int) (t : TableTree a);

%% -%% fold left in an unspecified order +%% fold in an unspecified order %%

-foldl : (b : Type) ≡> (a : Type) ≡> (b -> a -> b) -> b -> Table a -> b; -foldl f o t = let +fold : (b : Type) ≡> (a : Type) ≡> (b -> a -> b) -> b -> Table a -> b; +fold f o t = let

helper : (b : Type) ≡> (a : Type) ≡> (b -> a -> b) -> b -> TableTree a -> b; helper f o t = case t @@ -49,7 +49,7 @@ in case t

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

length : (a : Type) ≡> Table a -> Int; length t = case t @@ -70,18 +70,22 @@ find elem tree = let

get : a -> (a -> a -> Bool) -> List a -> Option a; get e c es = case es - | cons e1 es => if_then_else_ (c e e1) (some e1) (get e c es) + | cons e1 es => if (c e e1) then (some e1) else (get e c es) | nil => none;

helper : a -> (a -> a -> Bool) -> Int -> TableTree a -> Option a; helper e c h t = case t - | table-node l r => if_then_else_ (Int_eq 0 (Int_and h 1)) - (helper e c (Int_lsr h 1) l) - (helper e c (Int_lsr h 1) r) - | table-leaf h1 es => if_then_else_ (Int_eq h h1) - (get e c es) - (none) % element not found - | table-nil => none; % element not found + | table-node l r => + if (Int_eq 0 (Int_and h 1)) then + (helper e c (Int_lsr h 1) l) + else + (helper e c (Int_lsr h 1) r) + | table-leaf h1 es => + if (Int_eq h h1) then + (get e c es) + else + (none) % element not found + | table-nil => none; % element not found

in case tree | table _ c h t => (helper elem c (h elem) t); @@ -104,30 +108,32 @@ insert elem tree = let

replace-or-add : a -> (a -> a -> Bool) -> List a -> List a; replace-or-add e c es = case es - | cons e1 es => if_then_else_ (c e e1) - (cons e es) + | cons e1 es => if (c e e1) then + (cons e es) else (cons e1 (replace-or-add e c es)) | nil => (cons e nil);

helper : a -> (a -> a -> Bool) -> Int -> TableTree a -> TableTree a; helper e c h t = case t - | table-node l r => if_then_else_ (Int_eq 0 (Int_and h 1)) - (table-node (helper e c (Int_lsr h 1) l) r) + | table-node l r => if (Int_eq 0 (Int_and h 1)) then + (table-node (helper e c (Int_lsr h 1) l) r) else (table-node l (helper e c (Int_lsr h 1) r)) - | table-leaf h1 es => if_then_else_ (Int_eq h h1) - (table-leaf h1 (replace-or-add e c es)) - (if_then_else_ (Int_eq 0 (Int_and h1 1)) + | table-leaf h1 es => if (Int_eq h h1) then + (table-leaf h1 (replace-or-add e c es)) else + (if (Int_eq 0 (Int_and h1 1)) then (helper e c h (table-node (table-leaf (Int_lsr h1 1) es) table-nil)) + else (helper e c h (table-node table-nil (table-leaf (Int_lsr h1 1) es)))) | table-nil => table-leaf h (cons e nil);

-in if_then_else_ (member elem tree) - (case tree % we may want to replace a variable (partial comparison function) - | table s c h t => table s c h (helper elem c (h elem) t)) - (case tree - | table s c h t => table (s + 1) c h (helper elem c (h elem) t)); +in if (member elem tree) then + (case tree % we may want to replace a variable (partial comparison function) + | table s c h t => table s c h (helper elem c (h elem) t)) + else + (case tree + | table s c h t => table (s + 1) c h (helper elem c (h elem) t));

%% %% Remove an element from the tree. @@ -138,38 +144,41 @@ remove elem tree = let

is-empty : TableTree a -> Bool; is-empty t = case t - | table-node l r => if_then_else_ (is-empty l) - (is-empty r) + | table-node l r => if (is-empty l) then + (is-empty r) else (false) | table-leaf _ es => Int_eq 0 (List_length es) | table-nil => true;

pop-empty : TableTree a -> TableTree a; - pop-empty t = if_then_else_ (is-empty t) - (table-nil) + pop-empty t = if (is-empty t) then + (table-nil) else (t);

remove : a -> (a -> a -> Bool) -> List a -> List a; remove e c es = case es - | cons e1 es => if_then_else_ (c e e1) - (es) + | cons e1 es => if (c e e1) then + (es) else (cons e1 (remove e c es)) | nil => nil; % element not found

helper : a -> (a -> a -> Bool) -> Int -> TableTree a -> TableTree a; helper e c h t = case t - | table-node l r => if_then_else_ (Int_eq 0 (Int_and h 1)) - (pop-empty (table-node (helper e c (Int_lsr h 1) l) r)) - (pop-empty (table-node l (helper e c (Int_lsr h 1) r))) - | table-leaf h1 es => if_then_else_ (Int_eq h h1) - (pop-empty (table-leaf h1 (remove e c es))) - (table-leaf h1 es) % element not found + | table-node l r => if (Int_eq 0 (Int_and h 1)) then + (pop-empty (table-node (helper e c (Int_lsr h 1) l) r)) + else + (pop-empty (table-node l (helper e c (Int_lsr h 1) r))) + | table-leaf h1 es => if (Int_eq h h1) then + (pop-empty (table-leaf h1 (remove e c es))) + else + (table-leaf h1 es) % element not found | table-nil => table-nil; % element not found

-in if_then_else_ (member elem tree) - (case tree - | table s c h t => table (s - 1) c h (helper elem c (h elem) t)) - (tree); +in if (member elem tree) then + (case tree + | table s c h t => table (s - 1) c h (helper elem c (h elem) t)) + else + (tree);

%% %% Change an element @@ -190,6 +199,52 @@ update elem tree = insert elem tree; % used to be more complicated empty : (a : Type) ≡> (a -> a -> Bool) -> (a -> Int) -> Table a; empty comp-fun hash-fun = table 0 comp-fun hash-fun table-nil;

+%%% +%%% Unordered Dictionary +%%% + +udict-hash : (Key : Type) ≡> (Data : Type) ≡> (Key -> Int) -> + ((Pair Key (Option Data)) -> Int); +udict-hash h = (lambda p -> case p | pair k _ => h k); + +udict-comp : (Key : Type) ≡> (Data : Type) ≡> (Key -> Key -> Bool) -> + ((Pair Key (Option Data)) -> (Pair Key (Option Data)) -> Bool); +udict-comp c = (lambda p0 -> (lambda p1 -> + case p0 | pair k0 _ => + case p1 | pair k1 _ => c k0 k1)); + +udict : (Key : Type) ≡> (Data : Type) ≡> (Key -> Key -> Bool) -> (Key -> Int) -> + Table (Pair Key (Option Data)); +udict c h = table 0 (udict-comp c) (udict-hash h) table-nil; + +udict-length : (Key : Type) ≡> (Data : Type) ≡> Table (Pair Key (Option Data)) -> Int; +udict-length t = length t; + +udict-find : (Key : Type) ≡> (Data : Type) ≡> Key -> + Table (Pair Key (Option Data)) -> Option Data; +udict-find k t = case (find (pair k none) t) + | some (pair _ d) => d + | none => none; + +udict-insert : (Key : Type) ≡> (Data : Type) ≡> Key -> Data -> + Table (Pair Key (Option Data)) -> Table (Pair Key (Option Data)); +udict-insert k d t = insert (pair k (some d)) t; + +udict-member : (Key : Type) ≡> (Data : Type) ≡> Key -> + Table (Pair Key (Option Data)) -> Bool; +udict-member k t = member (pair k none) t; + +udict-remove : (Key : Type) ≡> (Data : Type) ≡> Key -> + Table (Pair Key (Option Data)) -> Table (Pair Key (Option Data)); +udict-remove k t = remove (pair k none) t; + +udict-update : (Key : Type) ≡> (Data : Type) ≡> Key -> Data -> + Table (Pair Key (Option Data)) -> Table (Pair Key (Option Data)); +udict-update k d t = update (pair k (some d)) t; + +udict-is-empty : (Key : Type) ≡> (Data : Type) ≡> Table (Pair Key (Option Data)) -> Bool; +udict-is-empty t = is-empty t; + %%% %%% Test helper %%% @@ -216,8 +271,8 @@ int-range : Int -> Int -> Table Int; int-range min max = let

helper : Int -> Table Int -> Table Int; - helper min tree = if_then_else_ (Int_eq min max) - (tree) (helper (min + 1) (insert min tree)); + helper min tree = if (Int_eq min max) then + (tree) else (helper (min + 1) (insert min tree));

in helper min (empty int-comp int-hash);

@@ -229,7 +284,7 @@ remove-range : Int -> Int -> Table Int -> Table Int; remove-range min max tree = let

helper : Int -> Table Int -> Table Int; - helper min tree = if_then_else_ (Int_eq min max) - (tree) (helper (min + 1) (remove min tree)); + helper min tree = if (Int_eq min max) then + (tree) else (helper (min + 1) (remove min tree));

in helper min tree;

===================================== src/eval.ml ===================================== @@ -131,6 +131,15 @@ let o2v_bool b = if b then ttrue else tfalse

let tunit = Vcons ((dloc, "()"), [])

+(* I'm using a ref because I think register_builtin_functions + get called after the default_ctx is created in elab. + Another solution could be to define a function in elaboration step + and then undefine it. The thing is elab_context may not exist at runtime + so I must save it somewhere if the Elab.* function persist. *) +let _last_elab_context = ref empty_elab_context + +let set_getenv (ectx : elab_context) = _last_elab_context := ectx + (* * Builtins *) @@ -291,7 +300,21 @@ let parser_default loc depth args_val = match args_val with | [Vsexp (Block (_,toks,_))] -> o2v_list (sexp_parse_all_to_list default_grammar (Lexer.lex default_stt toks) (Some ";")) | [s] -> (warning loc "Parser.default do nothing without a Block"; s) - | _ -> error loc "Parser.default expects a Block as argument" + | _ -> error loc "Parser.default expects a Block as argument" + +let parser_custom loc depth args_val = match args_val with + | [Velabctx ectx; Vsexp (Block (_,toks,_))] -> + let grm = ectx_get_grammar ectx in + o2v_list (sexp_parse_all_to_list grm (Lexer.lex default_stt toks) (Some ";")) + | [Velabctx _; s] -> (warning loc "Parser.custom do nothing without a Block"; s) + | _ -> error loc "Parser.custom expects an ElabContext and a Block as argument" + +let parser_newest loc depth args_val = match args_val with + | [Vsexp (Block (_,toks,_))] -> + let grm = ectx_get_grammar (!_last_elab_context) in + o2v_list (sexp_parse_all_to_list grm (Lexer.lex default_stt toks) (Some ";")) + | [s] -> (warning loc "Parser.newest do nothing without a Block"; s) + | _ -> error loc "Parser.newest expects a Block as argument"

let string_eq loc depth args_val = match args_val with | [Vstring s1; Vstring s2] -> o2v_bool (s1 = s2) @@ -726,19 +749,10 @@ let gensym = let count = ref 0 in Vsexp (Symbol (dloc,(" %gensym% no "^(string_of_int (!count))^" "))))) | _ -> error loc "gensym takes a Unit as argument")

-(* I'm using a ref because I think register_builtin_functions - get called after the default_ctx is created in elab. - Another solution could be to define a function in elaboration step - and then undefine it. The thing is elab_context may not exist at runtime - so I must save it somewhere if the Elab.* function persist. *) -let _last_elab_context = ref empty_elab_context - let getenv loc depth args_val = match args_val with | [v] -> Vcommand (fun () -> Velabctx !_last_elab_context) | _ -> error loc "getenv takes a single Unit as argument"

-let set_getenv (ectx : elab_context) = _last_elab_context := ectx - let is_bound loc depth args_val = match args_val with | [Vstring name; Velabctx ectx] -> o2v_bool (try (ignore (senv_lookup name ectx); true) @@ -871,6 +885,8 @@ let register_builtin_functions () = ("Sexp.node" , make_node, 2); ("Sexp.dispatch" , sexp_dispatch, 7); ("Parser.default", parser_default,1); + ("Parser.custom" , parser_custom,2); + ("Parser.newest" , parser_newest,1); ("String.=" , string_eq, 2); ("String.concat" , string_concat, 2); ("String.sub" , string_sub, 3);

View it on GitLab: https://gitlab.com/monnier/typer/compare/5c4ba82976eced85b5bc2dc5f645babb986...