Jean-Alexandre Barszcz pushed to branch master at Stefan / Typer
Commits: 588b6327 by Jean-Alexandre Barszcz at 2020-09-04T23:06:53-04:00 Fix `lexp_whnf` for Case
A substitution built with `cons`es happens all at once, in the sense that the terms in such a list are substituted independently, and thus should not be shifted one relative to another.
This commit removes such a shift that was made by mistake in the computation of the WHNF of a `Case` redex. The shift caused debruijn indexing errors in the body of branches with multiple fields.
Additionnally, this commit removes the arguments to the inductive type from the substitution applied to the branch, since they are not bound by the case.
- - - - -
2 changed files:
- src/opslexp.ml - tests/elab_test.ml
Changes:
===================================== src/opslexp.ml ===================================== @@ -157,15 +157,21 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = | _ -> e) (* Keep `e`, assuming it's more readable! *) | Case (l, e, rt, branches, default) -> let e' = lexp_whnf_aux e ctx in - let reduce name aargs = + let reduce it name aargs = + let targs = match lexp_lexp' (lexp_whnf_aux it ctx) with + | Inductive (_,_,fargs,_) -> fargs + | _ -> Log.log_error "Case on a non-inductive type in whnf!"; [] in try let (_, _, branch) = SMap.find name branches in let (subst, _) = List.fold_left - (fun (s,d) (_, arg) -> - (S.cons (L.mkSusp (lexp_whnf_aux arg ctx) (S.shift d)) s, - d + 1)) - (S.identity, 0) + (fun (s, targs) (_, arg) -> + match targs with + | [] -> (S.cons (lexp_whnf_aux arg ctx) s, []) + | _targ::targs -> + (* Ignore the type arguments *) + (s, targs)) + (S.identity, targs) aargs in lexp_whnf_aux (push_susp branch subst) ctx with Not_found @@ -177,10 +183,10 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = name ^ "in case expression"); mkCase (l, e, rt, branches, default) in (match lexp_lexp' e' with - | Cons (_, (_, name)) -> reduce name [] + | Cons (it, (_, name)) -> reduce it name [] | Call (f, aargs) -> (match lexp_lexp' (lexp_whnf_aux f ctx) with - | Cons (_, (_, name)) -> reduce name aargs + | Cons (it, (_, name)) -> reduce it name aargs | _ -> mkCase (l, e, rt, branches, default)) | _ -> mkCase (l, e, rt, branches, default)) | Metavar (idx, s, _)
===================================== tests/elab_test.ml ===================================== @@ -51,8 +51,24 @@ let generate_tests (name: string) (test input_gen fmt tester)
(* let input = "y = lambda x -> x + 1;" *) -let input = "id = lambda (α : Type) ≡> lambda (x : α) -> x; -res = id 3;" +let inputs = + [("identity", {| +id = lambda (α : Type) ≡> lambda (x : α) -> x; +res = id 3; + |}); + ("whnf of case", {| +Box = (typecons (Box (l : TypeLevel) (t : Type_ l)) (box t)); +box = (datacons Box box); +unbox b = ##case_ (b | box inside => inside); +alwaysbool b = ##case_ (b | box _ => Bool); + +example1 : unbox (box (lambda x -> Bool)) 1; +example1 = true; + +example2 : alwaysbool (box Int); +example2 = true; + |}); + ]
let generate_lexp_from_str str = List.hd ((fun (lst, _) -> @@ -63,9 +79,22 @@ let generate_lexp_from_str str =
let _ = generate_tests "TYPECHECK" - (fun () -> [generate_lexp_from_str input]) - (fun x -> List.map lexp_string x) - (fun x -> (x, true)) + (fun () -> inputs) + (fun x -> x) + (fun (name, input) -> + let result = + try + let ectx = Elab.default_ectx in + let pres = Prelexer.prelex_string input in + let sxps = Lexer.lex Grammar.default_stt pres in + let _lxps, _ectx = Elab.lexp_p_decls [] sxps ectx in + Log.stop_on_error(); + true + with + | Log.Stop_Compilation _ -> (Log.print_and_clear_log (); false) + | Log.Internal_error _ -> (Log.print_and_clear_log (); false) in + (name, result) + )
let lctx = Elab.default_ectx (* let _ = (add_test "TYPECHEK_LEXP" "lexp_print" (fun () ->
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/588b632700c98b007a1c9d3513767baf35...
Afficher les réponses par date