Stefan pushed to branch master at Stefan / Typer

Commits: b57544ca by Stefan Monnier at 2016-10-09T10:46:54-04:00 * src/debruijn.ml (replace_by): Remove, unused

* src/debug_util.ml (mdecl): Move from lparse.ml. * src/lparse.ml (mdecl): Move to debug_util.ml.

- - - - -

3 changed files:

- src/debruijn.ml - src/debug_util.ml - src/lparse.ml

Changes:

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -273,36 +273,6 @@ let env_lookup_type ctx (v : vref): lexp = let env_lookup_expr ctx (v : vref): lexp option = lctx_lookup_value (ectx_to_lctx ctx) v

-(* replace an expression by another *) -(* Most of the time it should be O(1) but it can be O(n) *) -let replace_by ctx name by = - let (a, env, b) = ctx in - let idx = senv_lookup name ctx in - (* lookup and replace *) - let rec replace_by' ctx by acc = - match ctx with - | M.Mnil -> debruijn_error dummy_location - ("Replace error. This expression does not exist: " ^ name) - | M.Mcons((_, None, _, _) as elem, tl1, i, tl2) -> - (* Skip some elements if possible *) - if idx <= i then replace_by' tl1 by (elem::acc) - else replace_by' tl2 by (elem::acc) - (* replace_by' tl1 by (elem::acc) *) - - | M.Mcons((_, Some (b, n), _, _) as elem, tl1, i, tl2) -> - if n = name then - (M.cons by tl1), acc - else - (* Skip some elements if possible *) - if idx <= i then replace_by' tl1 by (elem::acc) - else replace_by' tl2 by (elem::acc) - (* replace_by' tl1 by (elem::acc) *) in - - let nenv, decls = replace_by' env by [] in - (* add old declarations *) - let nenv = List.fold_left (fun ctx elem -> M.cons elem ctx) nenv decls in - (a, nenv, b) - (* -------------------------------------------------------------------------- *) (* PropertyMap *) (* -------------------------------------------------------------------------- *)

===================================== src/debug_util.ml ===================================== --- a/src/debug_util.ml +++ b/src/debug_util.ml @@ -215,6 +215,12 @@ let format_source () = ) else (List.iter (fun str -> print_string str; print_string "\n") result;)

+(* merged declaration, allow us to process declaration in multiple pass *) +(* first detect recursive decls then lexp decls*) +type mdecl = + | Ldecl of symbol * pexp option * pexp option + | Lmcall of symbol * sexp list + let lexp_detect_recursive pdecls = (* Pack mutually recursive declarations *) (* mutually recursive def must use forward declarations *)

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -76,12 +76,6 @@ let lexp_debug_message loc lxp message = lexp_fatal loc message

-(* merged declaration, allow us to process declaration in multiple pass *) -(* first detect recursive decls then lexp decls*) -type mdecl = - | Ldecl of symbol * pexp option * pexp option - | Lmcall of symbol * sexp list - let elab_check_sort (ctx : elab_context) lsort (l, name) ltp = match OL.lexp_whnf lsort (ectx_to_lctx ctx) with | Sort (_, _) -> () (* All clear! *)

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