Jonathan Graveline pushed to branch graveline at Stefan / Typer

Commits: d21c5eb6 by Stefan Monnier at 2018-07-25T19:13:16Z Allow `let` vars to be erasable in some circumstances

* src/opslexp.ml (nerased_let): New function. (check'): Use it. * tests/eval_test.ml ("Let-erased"): New test.

- - - - - 450e86fa by Jonathan Graveline at 2018-07-25T20:28:33Z *samples/list.typer, more consistent function's type declaration

- - - - - 5d4e2008 by Jonathan Graveline at 2018-07-25T20:35:26Z Stop compilation on error in `check` and elab functions Also store all errors and warnings for future use

- - - - - 2b2bac1b by Jonathan Graveline at 2018-07-25T20:40:47Z Print related name only when the name has underscore

- - - - - 26e9e4c2 by Jonathan Graveline at 2018-07-25T21:25:59Z Add an exception for sform_load's context when in pervasive.typer

- - - - - a188451f by Jonathan Graveline at 2018-07-26T02:52:06Z Merge branch 'master' of https://gitlab.com/monnier/typer into graveline

- - - - - be29169e by Jonathan Graveline at 2018-07-26T04:45:56Z Change lost somewhere in previous commit *samples/case2.typer *samples/do.typer *samples/list.typer

- - - - - b0b911ec by Jonathan Graveline at 2018-07-26T04:55:06Z Many change to use `load` in pervasive.typer and move some definition Temporary workaround for tuple access in macro `.`

renamed: samples/case2.typer -> btl/case.typer renamed: samples/do.typer -> btl/do.typer renamed: samples/list.typer -> btl/list.typer modified: btl/pervasive.typer deleted: samples/case.typer modified: src/opslexp.ml modified: tests/array_test.ml modified: tests/case_test.ml

- - - - -

14 changed files:

- samples/case2.typer → btl/case.typer - samples/do.typer → btl/do.typer - samples/list.typer → btl/list.typer - btl/pervasive.typer - − samples/case.typer - src/REPL.ml - src/debruijn.ml - src/elab.ml - src/lexp.ml - src/opslexp.ml - src/util.ml - tests/array_test.ml - tests/case_test.ml - tests/eval_test.ml

Changes:

===================================== samples/case2.typer → btl/case.typer ===================================== @@ -8,6 +8,22 @@ %%%% argument may be sub pattern or variable) %%%%

+%% Move IO outside List (from element to List) +%% (Was helpful for me when translating code that used to not be IO code) +%% (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 %% @@ -187,6 +203,8 @@ introduced-vars pat = let (lambda s ss -> do { o <- o; % bind if_then_else_ (Sexp_eq s (Sexp_symbol "_:=_")) + %% (if_then_else_ (Sexp_eq (List_nth 0 ss Var_error) dflt-var) + %% (return (List_concat o (cons dflt-var nil))) (return (List_concat o (cons (List_nth 1 ss Var_error) nil))) %% there's no introduced variable here %% `case` on sub pattern will introduce new variable

===================================== samples/do.typer → btl/do.typer ===================================== @@ -1,9 +1,6 @@ -%%% -%%% Macro : do -%%% -%%% This file may not be up to date with version -%%% in pervasive.typer -%%% +%%%% +%%%% Macro : do +%%%%

%% %% Here's an example :

===================================== samples/list.typer → btl/list.typer ===================================== @@ -2,18 +2,29 @@ %%%%% List %%%%%

-%%%% List type +%% +%% I kept it simple: +%% not using macro `lambda` +%% not usgin macro `case` +%% in case we want to change order of definition in pervasive.typer +%%

-%% FIXME: "t : ?" should be sufficient but triggers +%%%% List type

-t : Type -> Type; -type t (a : Type) - | nil - | cons (hd : a) (tl : t a); +%% +%% FIXME: "List : ?" should be sufficient but triggers +%% macro `type` isn't actually defined where this file is included +%% in pervasive.typer +%% +%% List : Type -> Type; +%% type List (a : Type) +%% | nil +%% | cons (hd : a) (tl : List a); +%%

%%%% List functions

-length : (a : Type) ≡> t a -> Int; +length : (a : Type) ≡> List a -> Int; length xs = case xs | nil => 0 | cons hd tl => @@ -21,71 +32,71 @@ length xs = case xs

%% ML's typical `head` function is not total, so can't be defined %% as-is in Typer. There are several workarounds: -%% - Provide a default value : `a -> t a -> a`; -%% - Disallow problem case : `(l : t a) -> (l != nil) -> a`; +%% - Provide a default value : `a -> List a -> a`; +%% - Disallow problem case : `(l : List a) -> (l != nil) -> a`; %% - Return an Option/Error -head1 : (a : Type) ≡> t a -> Option a; +head1 : (a : Type) ≡> List a -> Option a; head1 xs = case xs | nil => none | cons hd tl => some hd;

-head : (a : Type) ≡> t a -> Option a; +head : (a : Type) ≡> List a -> Option a; head xs = case xs | cons x _ => some x | nil => none;

-tail : (a : Type) ≡> t a -> t a; +tail : (a : Type) ≡> List a -> List a; tail xs = case xs | nil => nil | cons hd tl => tl;

-map : (a : Type) ≡> (b : Type) ≡> (a -> b) -> t a -> t b; +map : (a : Type) ≡> (b : Type) ≡> (a -> b) -> List a -> List b; map f = lambda xs -> case xs | nil => nil | cons x xs => cons (f x) (map f xs);

-mapi : (a : Type) ≡> (b : Type) ≡> (a -> Int -> b) -> t a -> t b; -mapi f xs = let - helper : (a -> Int -> b) -> Int -> t a -> t b; - helper f i xs = case xs +mapi : (a : Type) ≡> (b : Type) ≡> (a -> Int -> b) -> List a -> List b; +mapi = lambda f -> lambda xs -> let + helper : (a -> Int -> b) -> Int -> List a -> List b; + helper = lambda f -> lambda i -> lambda xs -> case xs | nil => nil | cons x xs => cons (f x i) (helper f (i + 1) xs); in helper f 0 xs;

-map2 : (?a -> ?b -> ?c) -> t ?a -> t ?b -> t ?c; -map2 f xs ys = case xs +map2 : (a : Type) ≡> (b : Type) ≡> (c : Type) ≡> (a -> b -> c) -> List a -> List b -> List c; +map2 = lambda f -> lambda xs -> lambda ys -> case xs | nil => nil | cons x xs => case ys | nil => nil % error | cons y ys => cons (f x y) (map2 f xs ys);

-foldli : (a : Type) ≡> (b : Type) ≡> (a -> b -> Int -> a) -> a -> t b -> a; -foldli f o xs = let - helper : (a -> b -> Int -> a) -> Int -> a -> t b -> a; - helper f i o xs = case xs +foldli : (a : Type) ≡> (b : Type) ≡> (a -> b -> Int -> a) -> a -> List b -> a; +foldli = lambda f -> lambda o -> lambda xs -> let + helper : (a -> b -> Int -> a) -> Int -> a -> List b -> a; + helper = lambda f -> lambda i -> lambda o -> lambda xs -> case xs | nil => o | cons x xs => helper f (i + 1) (f o x i) xs; in helper f 0 o xs;

%% Fold 2 List as long as both List are non-empty -fold2 : (?a -> ?b -> ?c -> ?a) -> ?a -> t ?b -> t ?c -> ?a; -fold2 f o xs ys = case xs +fold2 : (a : Type) ≡> (b : Type) ≡> (c : Type) ≡> (a -> b -> c -> a) -> a -> List b -> List c -> a; +fold2 = lambda f -> lambda o -> lambda xs -> lambda ys -> case xs | cons x xs => ( case ys | cons y ys => fold2 f (f o x y) xs ys | nil => o ) % may be an error | nil => o; % may or may not be an error

-foldr : (a : Type) ≡> (b : Type) ≡> (b -> a -> a) -> t b -> a -> a; -foldr f = lambda xs -> lambda i -> case xs +foldr : (a : Type) ≡> (b : Type) ≡> (b -> a -> a) -> List b -> a -> a; +foldr = lambda f -> lambda xs -> lambda i -> case xs | nil => i | cons x xs => f x (foldr f xs i);

-find : (a : Type) ≡> (a -> Bool) -> t a -> Option a; -find f = lambda xs -> case xs +find : (a : Type) ≡> (a -> Bool) -> List a -> Option a; +find = lambda f -> lambda xs -> case xs | nil => none | cons x xs => case f x | true => some x | false => find f xs;

-nth : (a : Type) ≡> Int -> t a -> a -> a; +nth : (a : Type) ≡> Int -> List a -> a -> a; nth = lambda n -> lambda xs -> lambda d -> case xs | nil => d | cons x xs @@ -93,21 +104,21 @@ nth = lambda n -> lambda xs -> lambda d -> case xs | true => x | false => nth (n - 1) xs d;

-reverse : (a : Type) ≡> t a -> t a -> t a; -reverse l t = case l +reverse : (a : Type) ≡> List a -> List a -> List a; +reverse = lambda l -> lambda t -> case l | nil => t | cons hd tl => reverse tl (cons hd t);

-concat : (a : Type) ≡> t a -> t a -> t a; -concat l t = reverse (reverse l nil) t; +concat : (a : Type) ≡> List a -> List a -> List a; +concat = lambda l -> lambda t -> reverse (reverse l nil) t;

-foldl : (a : Type) ≡> (b : Type) ≡> (a -> b -> a) -> a -> t b -> a; -foldl f i xs = case xs +foldl : (a : Type) ≡> (b : Type) ≡> (a -> b -> a) -> a -> List b -> a; +foldl = lambda f -> lambda i -> lambda xs -> case xs | nil => i | cons x xs => foldl f (f i x) xs;

-remove : (a : Type) ≡> (a -> Bool) -> t a -> t a; -remove f l = case l +remove : (a : Type) ≡> (a -> Bool) -> List a -> List a; +remove = lambda f -> lambda l -> case l | nil => nil | cons x xs => ( case (f x) | true => remove f xs @@ -116,8 +127,8 @@ remove f l = case l

%% Merge two List to a List of Pair %% Both List must be of same length -merge : t ?a -> t ?b -> t (Pair ?a ?b); -merge xs ys = case xs +merge : (a : Type) ≡> (b : Type) ≡> List a -> List b -> List (Pair a b); +merge = lambda xs -> lambda ys -> case xs | cons x xs => ( case ys | cons y ys => cons (pair x y) (merge xs ys) | nil => nil ) % error @@ -125,50 +136,34 @@ merge xs ys = case xs

%% `Unmerge` a List of Pair %% The two functions name said it all -map-fst : t (Pair ?a ?b) -> t ?a; -map-fst xs = let - mf : Pair ?a ?b -> ?a; +map-fst : (a : Type) ≡> (b : Type) ≡> List (Pair a b) -> List a; +map-fst = lambda xs -> let + mf : Pair a b -> a; mf p = case p | pair x _ => x; in map mf xs;

-map-snd : t (Pair ?a ?b) -> t ?b; -map-snd xs = let - mf : Pair ?a ?b -> ?b; +map-snd : (a : Type) ≡> (b : Type) ≡> List (Pair a b) -> List b; +map-snd = lambda xs -> let + mf : Pair a b -> b; mf p = case p | pair _ y => y; in map mf xs;

-%% Is argument List empty? -empty : t ?a -> Bool; -empty xs = Int_eq (length xs) 0; - -%% Move IO outside List (from element to List) -%% (Was helpful for me when translating code that used to not be IO code) -%% (The function's type explain everything) -io-list : t (IO ?a) -> IO (t ?a); -io-list l = let - ff : IO (t ?a) -> IO ?a -> IO (t ?a); - ff o v = do { - o <- o; - v <- v; - IO_return (cons v o); - }; -in do { - l <- (foldl ff (IO_return nil) l); - IO_return (reverse l nil); -}; +%% Is argument List empty +empty : (a : Type) ≡> List a -> Bool; +empty = lambda xs -> Int_eq (length xs) 0;

%%%% Sorting List

-sort : (a : Type) ≡> (a -> a -> Bool) -> t a -> t a; -sort o l = let +sort : (a : Type) ≡> (a -> a -> Bool) -> List a -> List a; +sort = lambda o -> lambda l -> let

- sortp : Option a -> t a -> t a -> t a -> t a; - sortp p lt gt l = case p + sortp : Option a -> List a -> List a -> List a -> List a; + sortp = lambda p -> lambda lt -> lambda gt -> lambda l -> case p | none => nil | some (pp) => ( case l | nil => ( let - ltp : t a; ltp = sortp (head1 lt) nil nil (tail lt); - gtp : t a; gtp = sortp (head1 gt) nil nil (tail gt); + ltp : List a; ltp = sortp (head1 lt) nil nil (tail lt); + gtp : List a; gtp = sortp (head1 gt) nil nil (tail gt); in concat ltp (cons pp gtp) ) | cons x xs => ( case (o x pp) @@ -181,8 +176,8 @@ in sortp (head1 l) nil nil (tail l);

%%%% Some algo on sorted list

-sfind : (a : Type) ≡> (a -> a -> Bool) -> (a -> Bool) -> a -> t a -> Option a; -sfind o f a l = case l +sfind : (a : Type) ≡> (a -> a -> Bool) -> (a -> Bool) -> a -> List a -> Option a; +sfind = lambda o -> lambda f -> lambda a -> lambda l -> case l | nil => none | cons x xs => ( case (f x) | true => some x @@ -192,39 +187,53 @@ sfind o f a l = case l ) );

-sall : (a : Type) ≡> (a -> Bool) -> t a -> t a; -sall f l = case l +sall : (a : Type) ≡> (a -> Bool) -> List a -> List a; +sall = lambda f -> lambda l -> case l | nil => nil | cons x xs => ( case (f x) | true => cons x (sall f xs) | false => sall f xs );

-sexist : (a : Type) ≡> (a -> a -> Bool) -> (a -> Bool) -> a -> t a -> Bool; -sexist o f a l = case (sfind o f a l) +sexist : (a : Type) ≡> (a -> a -> Bool) -> (a -> Bool) -> a -> List a -> Bool; +sexist = lambda o -> lambda f -> lambda a -> lambda l -> case (sfind o f a l) | none => false | some _ => true;

-sinsert : (a : Type) ≡> (a -> a -> Bool) -> a -> t a -> t a; -sinsert o a l = case l +sinsert : (a : Type) ≡> (a -> a -> Bool) -> a -> List a -> List a; +sinsert = lambda o -> lambda a -> lambda l -> case l | nil => cons a l | cons x xs => ( case (o x a) | true => cons a l | false => cons x (sinsert o a xs) );

-ssup : (a : Type) ≡> (a -> a -> Bool) -> a -> t a -> t a; -ssup o a l = case l +ssup : (a : Type) ≡> (a -> a -> Bool) -> a -> List a -> List a; +ssup = lambda o -> lambda a -> lambda l -> case l | nil => nil | cons x xs => ( case (o x a) | true => l | false => ssup o a xs );

-sinf : (a : Type) ≡> (a -> a -> Bool) -> a -> t a -> t a; -sinf o a l = case l +sinf : (a : Type) ≡> (a -> a -> Bool) -> a -> List a -> List a; +sinf = lambda o -> lambda a -> lambda l -> case l | nil => nil | cons x xs => ( case (o x a) | true => nil | false => cons x (sinf o a xs) ); + +%%%% +%%%% Array from List +%%%% + +List->Array : (a : Type) ≡> List a -> Array a; +List->Array xs = let + + helper : List a -> Array a -> Array a; + helper xs a = case xs + | cons x xs => helper xs (Array_append x a) + | nil => a; + +in (helper xs (Array_empty ()));

===================================== btl/pervasive.typer ===================================== @@ -405,10 +405,13 @@ __.__ = nil); branch = Sexp_node (Sexp_symbol "_=>_") (cons pattern (cons (Sexp_symbol "v") nil)); - in Sexp_node (Sexp_symbol "case_") + tmp-fix def = quote (let + (uquote (Sexp_symbol "%tuple element%")) = (uquote def) in + (uquote (Sexp_symbol "%tuple element%"))); + in tmp-fix (Sexp_node (Sexp_symbol "case_") (cons (Sexp_node (Sexp_symbol "_|_") (cons o (cons branch nil))) - nil) + nil)) in macro (lambda args -> IO_return case args @@ -501,138 +504,19 @@ test4 = test1 : Option ?; test3 = test4;

%%%% -%%%% Macro : do +%%%% Common library %%%%

-%% -%% Here's an example : -%% -%% fun = do { -%% str <- return "\n\tHello world!\n\n"; -%% print str; -%% }; -%% -%% str is bind by macro, -%% -%% fun is a command, -%% -%% do may contain do because it returns a command. -%% - -assign = Sexp_symbol "<-"; - -get-sym : Sexp -> Sexp; -get-sym sexp = let - - dflt-sym = (lambda _ -> (Sexp_symbol " %not used% ")); - - in Sexp_dispatch sexp - - ( lambda s ss -> if_then_else_ (Sexp_eq (List_nth 0 ss Sexp_error) assign) - (s) - (dflt-sym ()) - ) - - dflt-sym dflt-sym dflt-sym - dflt-sym dflt-sym; % there must be a command - -get-op : Sexp -> Sexp; -get-op sexp = let - - as-is = lambda _ -> sexp; - - helper = (lambda sexp -> Sexp_dispatch sexp - - ( lambda s ss -> if_then_else_ (Sexp_eq (List_nth 0 ss Sexp_error) assign) - (Sexp_node (List_nth 1 ss Sexp_error) (List_tail (List_tail ss))) - (Sexp_node s ss) - ) - - as-is as-is as-is as-is as-is - ); - - op = (helper sexp); +%% `List` is the type and `list` is the module (tuple)

-in if_then_else_ (Sexp_eq op (Sexp_symbol "")) Sexp_error op; +list = load_ "btl/list.typer";

-get-decl : List Sexp -> List Sexp; -get-decl args = let +%% macro `do` for easier series of IO operation

- err = lambda _ -> cons Sexp_error nil; - - % Expecting a Block of command separated by ";" - - node = Sexp_dispatch (List_nth 0 args Sexp_error) - - (lambda _ _ -> cons Sexp_error nil) err err err err - - (lambda l -> Parser_default l); +do = let lib = load_ "btl/do.typer" in lib.do;

-in node; - -%% -%% The idea of the macro is : -%% -%% IO_bind a-op (lambda a-sym -> [next command or return a-sym]) -%% IO_bind a-op (lambda a-sym -> (IO_bind b-op (lambda b-sym -> [next command or return b-sym]))) -%% -%% this way a-sym is defined within b-op and so on -%% a-sym is now just `a` and not `IO a` -%% - -set-fun : List Sexp -> Sexp; -set-fun args = let - - helper : Sexp -> List Sexp -> Sexp; - helper lsym args = case args - | cons s ss => (let - - sym = get-sym s; - - op = get-op s; - - in Sexp_node (Sexp_symbol "IO_bind") (cons (op) - (cons (Sexp_node (Sexp_symbol "lambda_->_") (cons sym (cons (helper sym ss) nil))) nil)) - ) - - | nil => Sexp_node (Sexp_symbol "IO_return") (cons lsym nil); - -in helper (Sexp_symbol "") args; % return Unit if no command given - -%% Serie of command - -do = macro (lambda args -> - (IO_return (set-fun (get-decl args))) -); - -%%%% -%%%% Array from List -%%%% +%% macro `case` for a little more complex pattern matching

-List->Array : (a : Type) ≡> List a -> Array a; -List->Array xs = let - - helper : List a -> Array a -> Array a; - helper xs a = case xs - | cons x xs => helper xs (Array_append x a) - | nil => a; - -in (helper xs (Array_empty ())); - -%% Move IO outside List (from element to List) -%% (Was helpful for me when translating code that used to not be IO code) -%% (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); -}; +case_ = let lib = load_ "btl/case.typer" in lib.case_;

%%% pervasive.typer ends here.

===================================== samples/case.typer deleted ===================================== @@ -1,521 +0,0 @@ -%%% -%%% Macro : case ... | ... -%%% -%%% (pattern matching) -%%% -%%% TODO : -%%% - Handle named constructor variable -%%% - Find a way to get no error when there's no default case -%%% and user pattern is exhaustive -%%% - -%% -%% Match every variable in each pattern with a list of VarTest. -%% -%% VarTest : -%% -%% var_test is (var_test [ctor to match]) -%% -%% Push current var n_times for sub test -%% push_var is (push_var n_times) -%% -%% sub_test introduce a variable for testing sub pattern -%% sub_test is (sub_test [sup. var name] [ctor to match]) -%% -%% Pattern : -%% -%% branch is (branch [list of var test] [user fun on match]) -%% -%% dflt_branch is (dflt_branch [user fun]) and always match -%% - -type VarTest - | var_test Sexp - | push_var Int - | sub_test Sexp Sexp; - -type Pattern - | branch (List VarTest) Sexp - | dflt_branch Sexp; - -%% -%% Get matched expression (e.g. case (var1,var2,...) | ...) -%% -%% Expression are separated by "," so it is useful for -%% case (expr1,expr2,...) ... -%% but also for -%% case ... | (expr3,expr4,...) => ... -%% - -get_exprs : Sexp -> List Sexp; -get_exprs sexp = let - - err = (lambda _ -> cons Sexp_error nil); - - get_exprs_helper : Sexp -> List Sexp -> List Sexp; - get_exprs_helper s ss = case (Sexp_eq (Sexp_symbol "_,_") s) - | true => (ss) % tuple - % constructor or function called (only 1 pattern) - | false => (cons (Sexp_node s ss) nil); - -in Sexp_dispatch sexp - get_exprs_helper - (lambda s -> (cons (Sexp_symbol s) nil)) - err err err - (lambda ss -> cons ss nil); % do nothing to Block - -mapi : (Sexp -> Int -> Sexp) -> Int -> List Sexp -> List Sexp; -mapi f i xs = case xs - | nil => nil - | cons x xs => cons (f x i) (mapi f (i + 1) xs); - -io_list : List (IO ?a) -> IO (List ?a); -io_list l = let - - fold_fun : IO (List ?a) -> IO ?a -> IO (List ?a); - fold_fun o v = do - { - o <- o; - v <- v; - IO_return (cons v o); - }; - -in do -{ - l <- (List_foldl fold_fun (IO_return nil) l); - IO_return (List_reverse l nil); -}; - -get_num_vars : List Sexp -> IO (List Sexp); -get_num_vars vars = io_list (List_map - (lambda _ -> gensym ()) - vars); - -%% -%% Get pattern to match -%% - -get_cases : List Sexp -> List Pattern; -get_cases sexps = let - - to_case : Sexp -> Pattern; - to_case sexp = Sexp_dispatch sexp - - (lambda s ss -> case (Sexp_eq (Sexp_symbol "_=>_") s) - % expecting a Sexp_node as second argument to _=>_ - | true => (branch - (List_map (lambda ctor -> var_test ctor) (get_exprs (List_nth 0 ss Sexp_error))) - (List_nth 1 ss Sexp_error)) - | false => (dflt_branch (Sexp_node s ss))) - - (lambda s -> dflt_branch (Sexp_symbol s)) - (lambda s -> dflt_branch (Sexp_string s)) - (lambda i -> dflt_branch (Sexp_integer i)) - (lambda f -> dflt_branch (Sexp_float f)) - - (lambda ss -> dflt_branch ss); - - helper : List Sexp -> List Pattern; - helper sexps = List_map (lambda s -> (to_case s)) sexps; - -in helper sexps; - -%% -%% return true if v is a ctor -%% -is_ctor : Sexp -> IO Bool; -is_ctor v = Sexp_dispatch v - (lambda _ _ -> IO_return true) - (lambda s -> do - { - env <- Elab_getenv (); - IO_return (Elab_isconstructor s env); - }) - (lambda _ -> IO_return false) (lambda _ -> IO_return false) - (lambda _ -> IO_return false) (lambda _ -> IO_return false); - -%% -%% Rename nth constructor inside ctor to sym -%% - -rename_nth : Int -> Sexp -> Sexp -> IO Sexp; -rename_nth n ctor sym = let - - mapiif : (Sexp -> Int -> Sexp) -> (Sexp -> IO Bool) - -> Int -> IO (List Sexp) -> IO (List Sexp); - mapiif f b i xs = let - - helper : (Sexp -> Int -> Sexp) -> (Sexp -> IO Bool) -> Int - -> List Sexp -> IO (List Sexp); - helper f b i xs = case xs - | nil => IO_return nil - | cons x xs => (let - - apply : (Sexp -> Int -> Sexp) -> (Sexp -> IO Bool) -> Int - -> List Sexp -> IO (List Sexp); - apply f b i xs = do - { - xs <- (helper f b (i + 1) xs); - IO_return (cons (f x i) xs); - }; - - continue : (Sexp -> Int -> Sexp) -> (Sexp -> IO Bool) -> Int - -> List Sexp -> IO (List Sexp); - continue f b i xs = do - { - xs <- (helper f b i xs); - IO_return (cons x xs); - }; - - in do - { - bv <- b x; - (if_then_else_ bv (apply f b i xs) (continue f b i xs)); - }); - - in do - { - xs <- xs; - helper f b i xs; - }; - - err = (lambda _ -> Sexp_symbol "<not a ctor (0)>"); - - %% - %% Check for ctor within englobing ctor and rename variable - %% - - sub_ctor : Sexp -> Int -> Sexp; - sub_ctor ctor i = Sexp_dispatch ctor - (lambda s ss -> if_then_else_ (Int_eq i n) - (sym) - (Sexp_symbol "_")) - (lambda s -> if_then_else_ (Int_eq i n) - (sym) - (Sexp_symbol "_")) - err err err err ; - - io_err = (lambda _ -> IO_return (Sexp_symbol "<not a ctor (1)>")); - -in (Sexp_dispatch ctor - (lambda s ss -> do - { - ss <- (mapiif sub_ctor is_ctor 0 (IO_return ss)); - IO_return (Sexp_node s ss); - }) - (lambda s -> IO_return (Sexp_symbol s)) - io_err io_err io_err io_err); - -%% -%% Expand sub pattern into sub_test -%% and optionaly push_var when there's -%% - -expand_cases : List Pattern -> IO (List Pattern); -expand_cases pats = let - - foldi : (Sexp -> Int -> ?a -> ?a) - -> Int -> ?a -> List Sexp -> ?a; - foldi f i o xs = case xs - | nil => o - | cons x xs => foldi f (i + 1) (f x i o) xs; - - get_sub_pattern : Sexp -> IO (List Sexp); - get_sub_pattern ctor = let - - err = (lambda _ -> Sexp_error); - - no_pattern : List Sexp -> ? -> IO (List Sexp); - no_pattern pats = (lambda _ -> IO_return pats); - - helper : List Sexp -> IO (List Sexp); - helper vars = List_foldl (lambda pats var -> do - { - pats <- pats; - Sexp_dispatch var - (lambda s ss -> IO_return (cons (Sexp_node s ss) pats)) - (lambda s -> do - { - b <- is_ctor (Sexp_symbol s); - if_then_else_ b - (IO_return (cons (Sexp_symbol s) pats)) - (no_pattern pats ()); - }) - (no_pattern pats) (no_pattern pats) (no_pattern pats) (no_pattern pats) - }) (IO_return nil) vars; - - in Sexp_dispatch ctor - (lambda s ss -> helper ss) - (no_pattern nil) (no_pattern nil) - (no_pattern nil) (no_pattern nil) (no_pattern nil); - - expand_one : IO (List VarTest) -> VarTest -> IO (List VarTest); - expand_one all test = case test - | push_var n => IO_bind all (lambda all -> - IO_return (List_concat all (cons (push_var n) nil))) - | _ => (let - - expand : VarTest -> IO (List VarTest); - expand test = let - - %% I don't expect to use multiple not_unique_sym at the same time - %% so the name may be reused - - not_unique_sym : Sexp; - not_unique_sym = Sexp_symbol " %not gensym% "; - - t : Sexp; - t = case test - | (var_test t) => t - | (sub_test _ t) => t - | _ => Sexp_error; - - renamed : Int -> IO VarTest; - renamed i = case test - | (var_test t) => IO_bind (rename_nth i t not_unique_sym) - (lambda t -> IO_return (var_test t)) - | (sub_test v t) => IO_bind (rename_nth i t not_unique_sym) - (lambda t -> IO_return (sub_test v t)) - | _ => IO_return (var_test Sexp_error); - - sub_pattern : IO (List Sexp); - sub_pattern = do - { - l <- get_sub_pattern t; - IO_return (List_reverse l nil); - }; - - sub_case : IO (List VarTest); - sub_case = let - - helper : Sexp -> VarTest -> List VarTest -> IO (List VarTest); - helper c r o = IO_return (List_concat o - (cons r (cons (sub_test not_unique_sym c) nil))); - - l : IO (List VarTest); - l = do - { - sub_pattern <- sub_pattern; - (foldi - (lambda c i o -> do - { - o <- o; - r <- (renamed i); - helper c r o; - }) 0 (IO_return nil) sub_pattern) - }; - - in do - { - l <- l; - sub_pattern <- sub_pattern; - IO_return (cons (push_var (List_length sub_pattern)) l); - }; - - in do - { - sub_pattern <- sub_pattern; - if_then_else_ (Int_eq (List_length sub_pattern) 0) - (do - { - all <- all; - IO_return (List_concat all (cons test nil)); - }) - (do - { - sub_case <- sub_case; - all <- all; - IO_return (List_concat all sub_case); - }) - }; - - in expand test); - - expand_all : Pattern -> IO Pattern; - expand_all p = case p - | (dflt_branch _) => IO_return p - | (branch cs f) => (let - - ctors : IO (List VarTest); - ctors = (List_foldl expand_one (IO_return nil) cs); - - stop_on_id : List VarTest -> IO Pattern; - stop_on_id ctors = if_then_else_ - (Int_eq (List_length cs) (List_length ctors)) - (IO_return (branch ctors f)) - (expand_all (branch ctors f)); - - in do - { - ctors <- ctors; - stop_on_id ctors; - }); - -in io_list (List_map expand_all pats); - -pattern_to_sexp : List Sexp -> List Pattern -> IO Sexp; -pattern_to_sexp vars pats = let - - vars_wrap : List Sexp -> Sexp -> List Sexp -> Sexp; - vars_wrap numvs succ vs = Sexp_node (List_foldl - (lambda o v -> (quote (lambda_->_ (uquote v) (uquote o)))) - succ vs) ( numvs ); - - to_case : Sexp -> Sexp -> Sexp -> Option Sexp -> Sexp; - to_case var ctor succ fail = case fail - | some fail => (quote (##case_ (_|_ (uquote var) - (_=>_ (uquote ctor) (uquote succ)) - (_=>_ _ (uquote fail))))) - | none => (quote (##case_ (_|_ (uquote var) - (_=>_ (uquote ctor) (uquote succ))))); - - push : Int -> List Sexp -> List Sexp; - push n vars = if_then_else_ (Int_<= n 1) - (vars) - (case vars - | (cons v _) => push (n - 1) (cons v vars) - | nil => nil); - - chain_ctors : List Sexp -> List VarTest -> Sexp -> Sexp -> Sexp; - chain_ctors vars tests succ fail = case vars - | (cons v vv) => (case tests - | (cons t tt) => (case t - | (var_test t) => if_then_else_ (Sexp_eq t (Sexp_symbol "_")) - (to_case v t (chain_ctors vv tt succ fail) none) - (to_case v t (chain_ctors vv tt succ fail) (some fail)) - | (sub_test v t) => if_then_else_ (Sexp_eq t (Sexp_symbol "_")) - (to_case v t (chain_ctors vars tt succ fail) none) - (to_case v t (chain_ctors vars tt succ fail) (some fail)) - | (push_var n) => (chain_ctors (push n vars) tt succ fail)) - | nil => Sexp_error) - | nil => (case tests - | (cons t tt) => (case t - | (var_test _) => Sexp_error - | (sub_test v t) => if_then_else_ (Sexp_eq t (Sexp_symbol "_")) - (to_case v t (chain_ctors vars tt succ fail) none) - (to_case v t (chain_ctors vars tt succ fail) (some fail)) - | (push_var n) => (chain_ctors (push n vars) tt succ fail)) - | nil => succ); - - chain_ctors_nofail : List Sexp -> List VarTest -> Sexp -> Sexp; - chain_ctors_nofail vars tests succ = case vars - | (cons v vv) => (case tests - | (cons t tt) => (case t - | (var_test t) => - (to_case v t (chain_ctors_nofail vv tt succ) none) - | (sub_test v t) => - (to_case v t (chain_ctors_nofail vars tt succ) none) - | (push_var n) => (chain_ctors_nofail (push n vars) tt succ)) - | nil => Sexp_error) - | nil => (case tests - | (cons t tt) => (case t - | (var_test _) => Sexp_error - | (sub_test v t) => - (to_case v t (chain_ctors_nofail vars tt succ) none) - | (push_var n) => (chain_ctors_nofail (push n vars) tt succ)) - | nil => succ); - - one_to_sexp : List Sexp -> Pattern -> Sexp -> Sexp; - one_to_sexp vars pat fail = case pat - | (dflt_branch f) => f - | (branch tests f) => (chain_ctors vars tests f fail); - - last_to_sexp : List Sexp -> Pattern -> Sexp; - last_to_sexp vars pat = case pat - | (dflt_branch f) => f - | (branch tests f) => (chain_ctors_nofail vars tests f); - - test_fun : List Sexp -> Pattern -> Sexp -> Sexp; - test_fun vars pat fail = (quote (lambda (_ : Unit) -> - (uquote (one_to_sexp vars pat (quote ((uquote fail) ())))))); - - last_test_fun : List Sexp -> Pattern -> Sexp; - last_test_fun vars pat = (quote (lambda (_ : Unit) -> - (uquote (last_to_sexp vars pat)))); - - %% Same thing as not_unique_sym, I can reuse the name because - %% only the last defined is important - - fail_sym : Sexp; - fail_sym = Sexp_symbol " %fail sym% "; - - helper : List Sexp -> List Pattern -> Sexp; - helper vars pats = case pats - | (cons p pats) => (case pats - | (cons _ _) => Sexp_node (Sexp_symbol "let_in_") - (cons (Sexp_node (Sexp_symbol "_;_") - (cons (Sexp_node (Sexp_symbol "_=_") (cons fail_sym - (cons (helper vars pats) nil))) nil)) - (cons (test_fun vars p fail_sym) nil)) - | nil => (last_test_fun vars p)) - | nil => Sexp_error; - -in IO_return (quote ((uquote (helper vars pats)) ())); - -%% -%% The macro we want. -%% - -case_ = macro (lambda args -> let - - foldi : (?a -> Int -> ?b -> ?b) -> Int -> ?b -> List ?a -> ?b; - foldi f i o xs = case xs - | nil => o - | cons x xs => foldi f (i + 1) (f x i o) xs; - - case0 : List Sexp -> IO Sexp; - case0 args = let - - vars : List Sexp; - vars = case args - | (cons s ss) => get_exprs s - | nil => nil; - - pats : List Pattern; - pats = case args - | (cons s ss) => get_cases ss - | nil => nil; - - num_vars : IO (List Sexp); - num_vars = get_num_vars vars; - - free_vars : IO (List Sexp); - free_vars = get_num_vars vars; - - vars_wrap : List Sexp -> List Sexp -> Sexp -> IO Sexp; - vars_wrap fvars nvars fun = let - - rvars : List Sexp; - rvars = List_reverse vars nil; - - nfun : Sexp; - nfun = fun; - - in IO_return ( (foldi - (lambda v i fun -> (quote ( - let (uquote (List_nth i nvars Sexp_error)) = (uquote v); in (uquote fun)))) - 0 nfun vars)); - - in do - { - pats <- expand_cases pats; - num_vars <- num_vars; - free_vars <- free_vars; - f <- pattern_to_sexp num_vars pats; - vars_wrap free_vars num_vars f; - }; - - %% Only the Sexp after "_|_" are interesting - - case1 : Sexp -> List Sexp -> IO Sexp; - case1 s ss = if_then_else_ (Sexp_eq (Sexp_symbol "_|_") s) - (case0 ss) - (IO_return Sexp_error); - - err = (lambda _ -> IO_return Sexp_error); - -%% 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) -);

===================================== src/REPL.ml ===================================== @@ -235,7 +235,7 @@ let rec repl i clxp rctx = let (i, clxp, rctx) = try readfiles args (i, clxp, rctx) false - with Util.Stop_Compilation s -> + with Stop_Compilation s -> (print_string s; (i,clxp,rctx)) in repl clxp rctx; @@ -261,8 +261,8 @@ let rec repl i clxp rctx = List.iter (print_eval_result i) ret; repl clxp rctx with e -> match e with - | Util.Stop_Compilation msg -> (print_string msg; repl clxp rctx) - | _ -> repl clxp rctx) + | Stop_Compilation msg -> (print_string msg; repl clxp rctx) + | _ -> catch_error (); repl clxp rctx)

let arg_files = ref []

===================================== src/debruijn.ml ===================================== @@ -143,13 +143,17 @@ let _make_senv_type = (0, _make_scope) let _make_myers = M.nil

let _get_related_name (n : db_ridx) name map = - let r = Str.regexp (name^".*") in - SMap.fold (fun name idx ps -> + let r = Str.regexp (".*"^name^".*") in + let search r = SMap.fold (fun name idx ps -> if (Str.string_match r name 0) then (n - idx - 1)::ps else ps - ) map [] + ) map [] in + if ((String.sub name 0 1) = "_" || + (String.sub name ((String.length name) - 1) 1) = "_") then + search r + else []

(* Public methods: DO USE * ---------------------------------- *)

===================================== src/elab.ml ===================================== @@ -140,14 +140,16 @@ let elab_check_sort (ctx : elab_context) lsort var ltp =

let elab_check_proper_type (ctx : elab_context) ltp var = try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) var ltp - with e -> print_string "Exception while checking type `"; - lexp_print ltp; - (match var with - | (_, None) -> () - | (_, Some name) - -> print_string ("` of var `" ^ name ^"`\n")); - print_lexp_ctx (ectx_to_lctx ctx); - raise e + with e -> match e with + | Stop_Compilation _ -> raise e + | _ -> print_string "Exception while checking type `"; + lexp_print ltp; + (match var with + | (_, None) -> () + | (_, Some name) + -> print_string ("` of var `" ^ name ^"`\n")); + print_lexp_ctx (ectx_to_lctx ctx); + raise e

let elab_check_def (ctx : elab_context) var lxp ltype = let lctx = ectx_to_lctx ctx in @@ -155,10 +157,12 @@ let elab_check_def (ctx : elab_context) var lxp ltype =

let lexp_string e = lexp_string (L.clean e) in let ltype' = try OL.check lctx lxp - with e -> - lexp_error loc lxp "Error while type-checking"; - print_lexp_ctx (ectx_to_lctx ctx); - raise e in + with e -> match e with + (* lexp_error is fatal but Stop_Compilation isn't *) + | Stop_Compilation _ -> raise e + | _ -> lexp_error loc lxp "Error while type-checking"; + print_lexp_ctx (ectx_to_lctx ctx); + raise e in if (try OL.conv_p (ectx_to_lctx ctx) ltype ltype' with e -> print_string ("Exception while conversion-checking types:\n"); @@ -1108,21 +1112,24 @@ and lexp_decls_1 _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs

in (EV.set_getenv nctx; - _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) + let res = _lexp_decls_1 sdecls ectx nctx pending_decls pending_defs in + (stop_on_error (); res))

and lexp_p_decls (sdecls : sexp list) (ctx : elab_context) : ((vname * lexp * ltype) list list * elab_context) = - match sdecls with - | [] -> [], ectx_new_scope ctx - | _ -> let decls, sdecls, nctx = lexp_decls_1 sdecls ctx ctx SMap.empty [] in - let declss, nnctx = lexp_p_decls sdecls nctx in - decls :: declss, nnctx + let impl sdecls ctx = match sdecls with + | [] -> [], ectx_new_scope ctx + | _ -> let decls, sdecls, nctx = lexp_decls_1 sdecls ctx ctx SMap.empty [] in + let declss, nnctx = lexp_p_decls sdecls nctx in + decls :: declss, nnctx in + let res = impl sdecls ctx in (stop_on_error (); res)

and lexp_parse_all (p: sexp list) (ctx: elab_context) : lexp list = - List.map (fun pe -> let e, _ = infer pe ctx in e) p + let res = List.map (fun pe -> let e, _ = infer pe ctx in e) p in + (stop_on_error (); res)

and lexp_parse_sexp (ctx: elab_context) (e : sexp) : lexp = - let e, _ = infer e ctx in e + let e, _ = infer e ctx in (stop_on_error (); e)

(* -------------------------------------------------------------------------- * Special forms implementation @@ -1545,6 +1552,8 @@ let lexp_print_var_info ctx = print_string "\n") done

+let _in_pervasive = ref true + (* arguments : elab_context from where load is called, loc is location of load call, @@ -1563,7 +1572,10 @@ let sform_load usr_elctx loc sargs ot =

(* read file as elab_context *) let ld_elctx = match sargs with - | [String (_,file_name)] -> read_file file_name !_sform_default_ectx + | [String (_,file_name)] -> if !_in_pervasive then + read_file file_name usr_elctx + else + read_file file_name !_sform_default_ectx | _ -> (error loc "argument to load should be one file name (String)"; !_sform_default_ectx) in

(* get lexp_context *) @@ -1575,9 +1587,18 @@ let sform_load usr_elctx loc sargs ot = let usr_len = M.length usr_lctx in let dflt_len = M.length dflt_lctx in

- (* create a tuple from context and shift it to user context *) - let tuple = OL.ctx2tup dflt_lctx ld_lctx in - let tuple' = (Lexp.mkSusp tuple (S.shift (usr_len - dflt_len))) in + (* create a tuple from context and shift it to user context * + * also check if we are in pervasive in which case * + * we want to load in the current context rather than the default *) + let tuple = if !_in_pervasive then + OL.ctx2tup usr_lctx ld_lctx + else + OL.ctx2tup dflt_lctx ld_lctx in + + let tuple' = if !_in_pervasive then + tuple + else + (Lexp.mkSusp tuple (S.shift (usr_len - dflt_len))) in

(tuple',Lazy)

@@ -1665,7 +1686,9 @@ let default_ectx

builtin_size := get_size lctx; + let _ = _in_pervasive := true in let lctx = read_file (btl_folder ^ "/pervasive.typer") lctx in + let _ = _in_pervasive := false in let _ = _set_default_ectx lctx in lctx

@@ -1688,7 +1711,8 @@ let _lexp_expr_str (str: string) (tenv: token_env)

(* specialized version *) let lexp_expr_str str ctx = - _lexp_expr_str str default_stt (ectx_get_grammar ctx) (Some ";") ctx + try _lexp_expr_str str default_stt (ectx_get_grammar ctx) (Some ";") ctx + with Stop_Compilation s -> (print_string s; [])

let _lexp_decl_str (str: string) tenv grm limit (ctx : elab_context) = let sdecls = _sexp_parse_str str tenv grm limit in @@ -1696,7 +1720,8 @@ let _lexp_decl_str (str: string) tenv grm limit (ctx : elab_context) =

(* specialized version *) let lexp_decl_str str ctx = - _lexp_decl_str str default_stt (ectx_get_grammar ctx) (Some ";") ctx + try _lexp_decl_str str default_stt (ectx_get_grammar ctx) (Some ";") ctx + with Stop_Compilation s -> (print_string s; ([],ctx))

(* Eval String @@ -1709,7 +1734,7 @@ let _eval_expr_str str lctx rctx silent = (EV.eval_all elxps rctx silent)

let eval_expr_str str lctx rctx = try _eval_expr_str str lctx rctx false - with Util.Stop_Compilation s -> (print_string s; []) + with Stop_Compilation s -> (print_string s; [])

let eval_decl_str str lctx rctx = let prev_lctx, prev_rctx = lctx, rctx in @@ -1717,5 +1742,5 @@ let eval_decl_str str lctx rctx = let lxps, lctx = lexp_decl_str str lctx in let elxps = (List.map OL.clean_decls lxps) in (EV.eval_decls_toplevel elxps rctx), lctx - with Util.Stop_Compilation s -> (print_string s; prev_rctx, prev_lctx) + with Stop_Compilation s -> (print_string s; prev_rctx, prev_lctx)

===================================== src/lexp.ml ===================================== @@ -215,7 +215,7 @@ let mkCall (f, es) * that is transient and hence immediately GC'd. *) let hcs_table : ((lexp * subst), lexp) Hashtbl.t = Hashtbl.create 1000

-(* When building the type of a tuple (x1=e1, x2=e2, ..., xn=en) +(* When computing the type of "load"ed modules * we end up building substitutions of the form * * ((Susp e3 (((Susp e2 (e1 · id)) · e1 · id) @@ -223,11 +223,18 @@ let hcs_table : ((lexp * subst), lexp) Hashtbl.t = Hashtbl.create 1000 * · ((Susp e2 (e1 · id)) · e1 · id) * · e1 · id) * - * with exponential size (but lots of sharing). So it's indispensible + * with 2^n size (but lots of sharing). So it's indispensible * to memoize the computation to avoid the exponential waste of time. * - * FIXME: I still don't understand why we build substitutions - * of such a shape! *) + * This shows up because of the dependent type of `let`: + * + * let z = e₃ in e : τ[e₃/z] + * let y = e₂ in let z = e₃ in e : (τ[e₃/z])[e₂/y] = τ[(e₃[e₂/y])/z,e₂/y] + * let x = e₁ in let y = e₂ in let z = e₃ in e + * : (τ[(e₃[e₂/y])/z,e₂/y])[e₁/x] + * = τ[(e₃[(e₂[e₁/x])/y,e₁/x])/z,(e₂[e₁/x])/y,e₁/x] + * ... + *)

let rec mkSusp e s = if S.identity_p s then e else

===================================== src/opslexp.ml ===================================== @@ -366,9 +366,34 @@ let dbset_push ak erased = let nerased = DB.set_sink 1 erased in if ak = P.Aerasable then DB.set_set 0 nerased else nerased

+let nerased_let defs erased = + (* Let bindings are not erasable, with the important exception of + * let-bindings of the form `x = y` where `y` is an erasable var. + * This exception is designed so that macros like `case` which need to + * rebind variables to user-specified names can do so without having + * to pay attention to whether the var is erasable or not. + *) + (* FIXME: Maybe allow more cases of erasable let-bindings. *) + let nerased = DB.set_sink (List.length defs) erased in + let es = List.map + (fun (_v, e, _t) -> + (* Look for `x = y` where `y` is an erasable var. + * FIXME: `nerased` assumes all the vars in `defs` + * will be non-erasable, so in `let x = z; y = x ...` + * where `z` is erasable, `x` will be found + * to be erasable, but not `y`. *) + match e with Var (_, idx) -> DB.set_mem idx nerased + | _ -> false) + defs in + if not (List.mem true es) then nerased else + List.fold_left + (fun erased e + -> dbset_push (if e then P.Aerasable else P.Aexplicit) erased) + erased es + (* "check ctx e" should return τ when "Δ ⊢ e : τ" *) -let rec check' erased ctx e = - let check = check' in +let rec check'' erased ctx e = + let check = check'' in let assert_type ctx e t t' = if conv_p ctx t t' then () else (U.msg_error "TC" (lexp_location e) @@ -433,14 +458,17 @@ let rec check' erased ctx e = -> (let _ = check_type DB.set_empty ctx t in DB.lctx_extend ctx v ForwardRef t)) ctx defs in - (* FIXME: Allow erasable let-bindings! *) - let nerased = DB.set_sink (List.length defs) erased in + let nerased = nerased_let defs erased in let nctx = DB.lctx_extend_rec ctx defs in (* FIXME: Termination checking! Positivity-checker! *) let _ = List.fold_left (fun n (v, e, t) - -> assert_type nctx e - (push_susp t (S.shift n)) - (check nerased nctx e); + -> assert_type + nctx e + (push_susp t (S.shift n)) + (check (if DB.set_mem (n - 1) nerased + then DB.set_empty + else nerased) + nctx e); n - 1) (List.length defs) defs in mkSusp (check nerased nctx e) @@ -624,7 +652,11 @@ let rec check' erased ctx e = check erased ctx e | MVar (_, t, _) -> push_susp t s)

-let check = check' DB.set_empty +let check' ctx e = + let res = check'' DB.set_empty ctx e in + (U.stop_on_error (); res) + +let check = check'

(** Compute the set of free (meta)variables. **)

@@ -919,7 +951,7 @@ and clean_map cases = (** Turning a set of declarations into an object. **)

let ctx2tup ctx nctx = - U.debug_msg ("Entering ctx2tup\n"); + (*U.debug_msg ("Entering ctx2tup\n");*) assert (M.length nctx >= M.length ctx && ctx == M.nthcdr (M.length nctx - M.length ctx) nctx); let rec get_blocs nctx blocs = @@ -937,7 +969,7 @@ let ctx2tup ctx nctx = let type_label = (loc, "record") in let offset = List.length types in let types = List.rev types in - U.debug_msg ("Building tuple of size " ^ string_of_int offset ^ "\n"); + (*U.debug_msg ("Building tuple of size " ^ string_of_int offset ^ "\n");*) Call (Cons (Inductive (loc, type_label, [], SMap.add cons_name (List.map (fun (oname, t)

===================================== src/util.ml ===================================== @@ -66,30 +66,71 @@ let typer_unreachable s = raise (Unreachable_error s) exception Stop_Compilation of string let stop_compilation s = raise (Stop_Compilation s)

+(* `error list * warning list` both of type `level * kind * section * loc * msg` *) +type error_log_type = ((int * string * string * location * string) list * + (int * string * string * location * string) list) + +let empty_error_log : error_log_type = ([],[]) + +let error_log = ref empty_error_log + +let error_count () : int = let errors, _ = !error_log in + List.length errors + +let warning_count () : int = let _, warnings = !error_log in + List.length warnings + +let new_error lvl kind section loc msg = let errors, warnings = !error_log in + error_log := ((lvl,kind,section,loc,msg)::errors,warnings) + +let new_warning lvl kind section loc msg = let errors, warnings = !error_log in + error_log := (errors,(lvl,kind,section,loc,msg)::warnings) + +let reset_error_log () = error_log := empty_error_log + (* Section is the name of the compilation step [for debugging] *) (* 'prerr' output is ugly *) -let msg_message stop lvl kind section (loc: location) msg = - let preppend_loc msg = (loc.file +let msg_message (error : bool) lvl kind section (loc: location) msg = + let message = (loc.file ^ ":" ^ string_of_int loc.line ^ ":" ^ string_of_int loc.column ^ ":" ^ kind ^ (if section = "" then " " else "(" ^ section ^ ") ") ^ msg ^ "\n") in + + if error then + new_error lvl kind section loc msg + else + new_warning lvl kind section loc msg; + if lvl <= !typer_verbose then - (print_string (preppend_loc msg); - if stop then - stop_compilation (preppend_loc "Compiler stopped on first error") - else ()) - else if stop then - stop_compilation (preppend_loc "Compiler stopped on first error") + print_string message else ()

-(* I would like to add optional stop on warning but I think *) -(* warning may be thrown at runtime *) +let stop_on_error () = if (0 < (error_count ())) then + (let count = error_count () in + reset_error_log (); + stop_compilation + ("Compiler stopped after: "^(string_of_int count)^" error\n")) + else () + +let stop_on_warning () = (stop_on_error (); + if (0 < (warning_count ())) then + let count = warning_count () in + reset_error_log (); + stop_compilation + ("Compiler stopped after: "^(string_of_int count)^" warning\n") + else ()) + +let catch_error () = try stop_on_error () + with e -> match e with + | Stop_Compilation msg -> print_string msg + | _ -> ()

let msg_fatal s l m = msg_message false 0 "[X] Fatal " s l m; flush stdout; + reset_error_log (); internal_error "Compiler Fatal Error"

let msg_error = msg_message true 1 "Error:"

===================================== tests/array_test.ml ===================================== @@ -149,6 +149,8 @@ let _ = (add_test "ARRAY" "Array.get" (fun () ->

let _ = (add_test "ARRAY" "Array.empty, List->Array" (fun () -> let dcode = " + List->Array = list.List->Array; + empty1 = Array_empty ();

empty2 = List->Array nil;

===================================== tests/case_test.ml ===================================== @@ -14,12 +14,8 @@ open Env let ectx = Elab.default_ectx let rctx = Elab.default_rctx

+let case_decl = "" (* - Macro case break some test so I read definition here. - It's temporary. I will need to modify other test to use ##case_ (which is what - they need to test) or modify the macro to work with everything (there's strange - case in eval_test.ml which I did not expect). -*) let case_decl = let read_file filename = let lines = ref [] in let chan = open_in filename in @@ -32,6 +28,7 @@ let case_decl = let read_file filename = List.rev !lines

in String.concat "\n" (read_file "samples/case2.typer") +*)

(* eval case.typer only once! *) let rctx, ectx = Elab.eval_decl_str case_decl ectx rctx

===================================== tests/eval_test.ml ===================================== @@ -92,7 +92,7 @@ let _ = test_eval_eqv_named "let TrueProp = typecons TrueProp I; I = datacons TrueProp I; x = let a = 1; b = 2 in I - in (case x | I => c) : Int;" (* == *) "3" + in (case x | I => c);" (* == *) "3"

let _ = test_eval_eqv_named "Let3" @@ -104,7 +104,15 @@ let _ = test_eval_eqv_named TrueProp = typecons TrueProp I; I = datacons TrueProp I; x = let a = 1; b = 2 in I - in (case x | I => c) : Int;" (* == *) "3" + in (case x | I => c);" (* == *) "3" + +let _ = test_eval_eqv_named + "Let-erasable" + + "c = 3; e = 1; f = 2; d = 4;" + + "let id = lambda t ≡> lambda (x : t) -> x; + in (lambda t ≡> let t1 = t in id (t := t1)) 3" (* == *) "3"

(* Lambda * ------------------------ *)

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