Stefan pushed to branch master at Stefan / Typer

Commits: 1e05e7c1 by Stefan Monnier at 2016-11-28T11:42:57-05:00 Fix WHNF of Let and recognize negative integers

* src/lexer.ml (nexttoken): Recognize negative integer.

* src/opslexp.ml (lexp_whnf): Really return WHNF for `Let`.

* tests/eval_test.ml ("Let"): Use negative integer, to test them. ("Lists"): Add tests using a different definition of List.

- - - - -

3 changed files:

- src/lexer.ml - src/opslexp.ml - tests/eval_test.ml

Changes:

===================================== src/lexer.ml ===================================== --- a/src/lexer.ml +++ b/src/lexer.ml @@ -49,7 +49,11 @@ let nexttoken (stt : token_env) (pts : pretoken list) bpos cpos | (Preblock (sl, bpts, el) :: pts) -> (Block (sl, bpts, el), pts, 0, 0) | (Prestring (loc, str) :: pts) -> (String (loc, str), pts, 0, 0) | (Pretoken ({file;line;column}, name) :: pts') - -> if digit_p name.[bpos] then + -> let char = name.[bpos] in + if digit_p char + || (char = '-' (* FIXME: Handle '+' as well! *) + && bpos + 1 < String.length name + && digit_p (name.[bpos + 1])) then let rec lexnum bp cp (np : num_part) = if bp >= String.length name then ((if np == NPint then

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -63,6 +63,7 @@ let lookup_value = DB.lctx_lookup_value * `let x₂ = e₂ in e₂`) will be interpreted in the remaining context, * which already provides "x₁". *) +(* FXIME: This creates an O(N^2) tree from an O(N) `let`! *) let rec lexp_defs_subst l s defs = match defs with | [] -> s | (_, lexp, _) :: defs' @@ -138,7 +139,7 @@ let lexp_whnf e (ctx : DB.lexp_context) meta_ctx : lexp = (* FIXME: I'd really prefer to use "native" recursive substitutions, using * ideally a trick similar to the db_offsets in lexp_context! *) | Let (l, defs, body) - -> push_susp body (lexp_defs_subst l S.identity defs) + -> lexp_whnf (push_susp body (lexp_defs_subst l S.identity defs)) ctx

| e -> e

===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -79,8 +79,8 @@ let _ = test_eval_eqv_named

"c = 3; e = 1; f = 2; d = 4;"

- "let a = 10; x = 50; y = 60; b = 20; - in a + b;" (* == *) "30" + "let a = -5; x = 50; y = 60; b = 20; + in a + b;" (* == *) "15"

let _ = test_eval_eqv_named "Let2" @@ -246,7 +246,13 @@ let _ = test_eval_eqv_named "my_list = cons 1 (cons 2 (cons 3 - (cons 4 nil)))" + (cons 4 nil))); + List' = let L : Type -> Type; + L = inductive_ (L (a : Type)) (nil) (cons a (L a)) + in L; + cons' = inductive-cons List' cons; + nil' = inductive-cons List' nil; + my_list' = (cons' 1 nil');"

"length my_list; head my_list;

View it on GitLab: https://gitlab.com/monnier/typer/commit/1e05e7c18a4dd35979426187a063f82fdcd3...