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...