Stefan pushed to branch master at Stefan / Typer Commits: 0e695aca by Stefan Monnier at 2018-09-17T17:23:29Z * src/elab.ml (sform_debruijn): New special form (register_special_forms): Register it. - - - - - 1 changed file: - src/elab.ml Changes: ===================================== src/elab.ml ===================================== @@ -1509,6 +1509,17 @@ let sform_type ctx loc sargs ot = | _ -> sexp_error loc "##Type_ expects one argument"; sform_dummy_ret ctx loc +let sform_debruijn ctx loc sargs ot = + match sargs with + | [Integer (l,i)] + -> if i < 0 || i > get_size ctx then + (sexp_error l "##DeBruijn indiex out of bounds"; + sform_dummy_ret ctx loc) + else + let lxp = mkVar ((loc, None), i) in (lxp, Lazy) + | _ -> (sexp_error loc "##DeBruijn expects one integer argument"; + sform_dummy_ret ctx loc) + (* Only print var info *) let lexp_print_var_info ctx = let ((m, _), env, _) = ctx in @@ -1532,6 +1543,7 @@ let register_special_forms () = List.iter add_special_form [ ("Built-in", sform_built_in); + ("DeBruijn", sform_debruijn); ("typer-identifier", sform_identifier); ("typer-immediate", sform_immediate); ("datacons", sform_datacons); View it on GitLab: https://gitlab.com/monnier/typer/commit/0e695aca54e25cd721768069be9b64ca8e91... -- View it on GitLab: https://gitlab.com/monnier/typer/commit/0e695aca54e25cd721768069be9b64ca8e91... You're receiving this email because of your account on gitlab.com.