Setepenre pushed to branch master at Stefan / Typer

Commits: 3335b48a by Pierre Delaunay at 2016-05-23T18:10:47-04:00 Fix recursive definition handling

Changes to be committed: * src/debruijn.ml * src/lparse.ml

- - - - -

3 changed files:

- samples/nat.typer - src/debruijn.ml - src/lparse.ml

Changes:

===================================== samples/nat.typer ===================================== --- a/samples/nat.typer +++ b/samples/nat.typer @@ -21,10 +21,22 @@ plus = lambda (x : Nat) -> | succ z => succ (plus z y);

-n1 = (to-num zero); -n2 = (to-num one); -n3 = (to-num two); +odd : Nat -> Int; +even : Nat -> Int; +odd = lambda (n : Nat) -> case n + | zero => 0 + | succ y => (even y);

-m1 = (to-num (plus zero two)); % 2 -m2 = (to-num (plus two zero)); % 2 -m3 = (to-num (plus two one)); % 3 \ No newline at end of file +even = lambda (n : Nat) -> case n + | zero => 1 + | succ y => (odd y); + +%n1 = (to-num zero); +%n2 = (to-num one); +%n3 = (to-num two); + +%m1 = (to-num (plus zero two)); % 2 +%m2 = (to-num (plus two zero)); % 2 +%m3 = (to-num (plus two one)); % 3 + +o1 = (even two); \ No newline at end of file

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -176,7 +176,8 @@ let env_lookup_expr ctx (v : vref): lexp = let (r, _, lxp, _) = _env_lookup ctx v in

let lxp = match lxp with - | LetDef lxp -> lxp in + | LetDef lxp -> lxp + | _ -> Sort (dummy_location, Stype (SortLevel (SLn 0))) in

(if (r != 1) then ( let s1 = (Susp (lxp, (S.shift (idx - r + 1)))) in

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -234,7 +234,7 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = let inductive_type = Var((loc, type_name), idx) in

(* Get constructor args *) - let formal, args = match idt with + let formal, args = match unsusp_all idt with | Inductive(_, _, formal, ctor_def) -> ( try formal, (SMap.find cname ctor_def) with Not_found -> @@ -542,7 +542,7 @@ and lexp_read_pattern pattern exp target ctx: | Ppatvar ((loc, name) as var) ->( try( let idx = senv_lookup name ctx in - match (env_lookup_expr ctx ((loc, name), idx)) with + match unsusp_all (env_lookup_expr ctx ((loc, name), idx)) with (* We are matching a constructor *) | Cons _ -> (name, loc, []), ctx

View it on GitLab: https://gitlab.com/monnier/typer/commit/3335b48a67b752cbf208a59441031b21c12e...