Stefan pushed to branch master at Stefan / Typer

Commits: 91395fc2 by Stefan Monnier at 2017-09-19T20:07:58Z Make define-operator's effect "immediately" visible

* src/debruijn.ml (ectx_get_grammar): New function.

* src/elab.ml (sform_immediate, default_ectx.read_file, lexp_expr_str) (lexp_decl_str)): Use it. (lexp_p_decls): Make new scope for body of `let`.

* tests/eval_test.ml (define-operator): No need for workaround any more.

* src/lexer.ml (unescape.split): Use string_sub.

* src/lexp.ml (_lexp_str): Avoid corner case bug. (get_binary_op_name): Catch corner case bug.

* src/opslexp.ml (clean_map): Prefer `map` when the `i` is not used.

* src/prelexer.ml (prelex_string.getline): Use string_sub.

- - - - -

9 changed files:

- src/debruijn.ml - src/elab.ml - src/eval.ml - src/inverse_subst.ml - src/lexer.ml - src/lexp.ml - src/opslexp.ml - src/prelexer.ml - tests/eval_test.ml

Changes:

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -200,6 +200,9 @@ let ectx_new_scope ectx : elab_context = let ectx_get_scope (ectx : elab_context) : (scope_level * lctx_length) = let (_, _, _, sl) = ectx in sl

+let ectx_get_grammar (ectx : elab_context) : Grammar.grammar = + let (grm, _, _, _) = ectx in grm + let env_lookup_by_index index (ctx: lexp_context): env_elem = Myers.nth index ctx

===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -377,7 +377,8 @@ and infer_type pexp ectx var = * could write `(a : TypeLevel) -> a -> a` instead of * `(a : TypeLevel) -> Type_ a -> Type_ a` *) | _ -> - (* FIXME: Here we rule out TypeLevel/TypeOmega. *) + (* FIXME: Here we rule out TypeLevel/TypeOmega. + * Maybe it's actually correct?! *) match Unif.unify (mkSort (lexp_location s, Stype (newMetalevel @@ -724,10 +725,10 @@ and track_fv rctx lctx e = "metavars" else if nc = [] then "a bug" - else let rec tfv i = + else let tfv i = let name = match Myers.nth i rctx with - | (Some n,_) -> n - | _ -> "<anon>" in + | (Some n,_) -> n + | _ -> "<anon>" in match Myers.nth i lctx with | (o, _, LetDef e, _) -> let drop = i + 1 - o in @@ -930,7 +931,7 @@ and lexp_decls_1 and lexp_p_decls (sdecls : sexp list) (ctx : elab_context) : ((vname * lexp * ltype) list list * elab_context) = match sdecls with - | [] -> [], ctx + | [] -> [], ectx_new_scope ctx | _ -> let decls, sdecls, nctx = lexp_decls_1 sdecls ctx ctx SMap.empty [] in let declss, nnctx = lexp_p_decls sdecls nctx in decls :: declss, nnctx @@ -1130,7 +1131,7 @@ let sform_immediate ctx loc sargs ot = | [(Integer _) as se] -> mkImm (se), Inferred DB.type_int | [(Float _) as se] -> mkImm (se), Inferred DB.type_float | [Block (sl, pts, el)] - -> let (grm, _, _, _) = ctx in + -> let grm = ectx_get_grammar ctx in let tokens = lex default_stt pts in let (se, _) = sexp_parse_all grm tokens None in elaborate ctx se ot @@ -1257,7 +1258,7 @@ let rec sform_lambda kind ctx loc sargs ot = match alt with | Inferred lt2' -> Inferred (mkArrow (ak2, ov, lt1, loc, lt2')) | _ -> alt) - + | lt -> let (lt1, lt2) = unify_with_arrow ctx loc lt kind arg olt1 in mklam lt1 (Some lt2)) @@ -1379,7 +1380,8 @@ let default_ectx let read_file file_name elctx = let pres = prelex_file file_name in let sxps = lex default_stt pres in - let nods = sexp_parse_all_to_list default_grammar sxps (Some ";") in + let nods = sexp_parse_all_to_list (ectx_get_grammar elctx) + sxps (Some ";") in let _, lctx = lexp_p_decls nods elctx in lctx in

@@ -1432,16 +1434,16 @@ let _lexp_expr_str (str: string) (tenv: token_env)

(* specialized version *) -let lexp_expr_str str lctx = - _lexp_expr_str str default_stt default_grammar (Some ";") lctx +let lexp_expr_str str ctx = + _lexp_expr_str str default_stt (ectx_get_grammar ctx) (Some ";") ctx

-let _lexp_decl_str (str: string) tenv grm limit ctx = +let _lexp_decl_str (str: string) tenv grm limit (ctx : elab_context) = let sdecls = _sexp_parse_str str tenv grm limit in - lexp_p_decls sdecls ctx + lexp_p_decls sdecls ctx

(* specialized version *) -let lexp_decl_str str lctx = - _lexp_decl_str str default_stt default_grammar (Some ";") lctx +let lexp_decl_str str ctx = + _lexp_decl_str str default_stt (ectx_get_grammar ctx) (Some ";") ctx

(* Eval String

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -372,7 +372,8 @@ and eval_case ctx i loc target pat dflt = (* extract constructor name and arguments *) let ctor_name, args = match v with | Vcons((_, cname), args) -> cname, args - | _ -> elexp_fatal loc target "Target is not a Constructor" in + | _ -> value_error loc v ("Target `" ^ elexp_string target + ^ "` is not a Constructor") in

(* Get working pattern *) try let (_, pat_args, exp) = SMap.find ctor_name pat in

===================================== src/inverse_subst.ml ===================================== --- a/src/inverse_subst.ml +++ b/src/inverse_subst.ml @@ -34,7 +34,7 @@ this program. If not, see http://www.gnu.org/licenses/. *) * * X[σ] = e ==> X[σ][σ⁻¹] = e[σ⁻¹] * - * so if we can find a σ⁻¹ such that σ ∘ σ⁻¹ = Id, e have X = e[σ⁻¹] + * so if we can find a σ⁻¹ such that σ ∘ σ⁻¹ = Id, we have X = e[σ⁻¹] * * So either left or right inverse can be used! *)

===================================== src/lexer.ml ===================================== --- a/src/lexer.ml +++ b/src/lexer.ml @@ -38,7 +38,7 @@ let unescape str = if b >= String.length str then [] else let e = try String.index_from str b '\' with Not_found -> String.length str in - String.sub str b (e - b) :: split (e + 1) + string_sub str b e :: split (e + 1) in String.concat "" (split 0)

let nexttoken (stt : token_env) (pts : pretoken list) bpos cpos

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -607,6 +607,7 @@ let is_binary_op str = if (c1 = '_') && (cn = '_') then true else false

let get_binary_op_name name = + assert (((String.length name) - 2) >= 1); String.sub name 1 ((String.length name) - 2)

let rec get_precedence expr ctx = @@ -718,9 +719,11 @@ and _lexp_str ctx (exp : lexp) : string = let decls = List.fold_left (fun str elem -> str ^ nl ^ (make_indent 1) ^ elem ^ " ") h1 decls in

- let n = String.length decls - 2 in + let n = String.length decls in (* remove last newline *) - let decls = (String.sub decls 0 n) in + let decls = if (n > 0) then + String.sub decls 0 (n - 2) + else decls in

(keyword "let ") ^ decls ^ (keyword " in ") ^ newline ^ (make_indent idt_lvl) ^ (lexp_stri idt_lvl body)

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -108,7 +108,7 @@ let lexp_close lctx e = * (of O(N) access time) * Oh well! *) L.clean (mkSusp e (lctx_to_subst lctx)) - +

(** Reduce to weak head normal form. * WHNF implies: @@ -890,5 +890,6 @@ and clean_map cases = | [] -> List.rev acc in clean_arg_list lst [] in

- SMap.mapi (fun key (l, args, expr) -> - (l, (clean_arg_list args), (erase_type expr))) cases + SMap.map (fun (l, args, expr) + -> (l, (clean_arg_list args), (erase_type expr))) + cases

===================================== src/prelexer.ml ===================================== --- a/src/prelexer.ml +++ b/src/prelexer.ml @@ -1,6 +1,6 @@ (* prelexer.ml --- First half of lexical analysis of Typer.

-Copyright (C) 2011-2012, 2016 Free Software Foundation, Inc. +Copyright (C) 2011-2017 Free Software Foundation, Inc.

Author: Stefan Monnier monnier@iro.umontreal.ca Keywords: languages, lisp, dependent types. @@ -152,7 +152,7 @@ let prelex_string str = with Not_found -> String.length str - 1 in let npos = i + 1 in pos := npos; - let line = String.sub str start (npos - start) in + let line = string_sub str start npos in (* print_string ("Read line: " ^ line); *) line in prelex "<string>" getline 1 [] []

===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -389,6 +389,7 @@ let _ = test_eval_eqv_named "Y"

"length_y = lambda t ≡> + %% FIXME: The `a` argument should be inferred! Y (a := List t) (witness := (lambda l -> 0)) (lambda length l -> case l @@ -415,10 +416,8 @@ let _ = test_eval_eqv_named define-operator "ELSE" 1 66; IF_THEN_ELSE_ = if_then_else_;"

- "{IF true THEN 2 ELSE 3};" - (* FIXME: the new grammar is not used at top-level yet! *) - (* "if true then 2 else 3;" *) - "{if true then 2 else 3};" + "IF true THEN 2 ELSE 3;" + "if true then 2 else 3;"

let _ = test_eval_eqv_named "Type Alias" "ListInt = List Int;" "" (* == *) ""

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

--- View it on GitLab: https://gitlab.com/monnier/typer/commit/91395fc27ad104a1ed95b64a1ec0c32998e7... You're receiving this email because of your account on gitlab.com.