Skip to content

🙈 Avoid matching on ElStable #372

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 3 commits into
base: main
Choose a base branch
from
Draft

🙈 Avoid matching on ElStable #372

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
c2c11fa
add a TODO
jonsterling May 26, 2022
cc51b56
TODO
jonsterling May 26, 2022
d8fcf1a
TODO
jonsterling May 26, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions src/core/Refiner.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -709,6 +709,7 @@ struct

let infer_nullary_ext : T.Chk.tac =
T.Chk.rule ~name:"Univ.infer_nullary_ext" @@ function
(* TODO: another place to avoid this kind of matching *)
| ElStable (`Ext (0,code ,`Global (Cof cof),bdry)) ->
let* cof = RM.lift_cmp @@ Sem.cof_con_to_cof cof in
let* () = Cof.assert_true cof in
Expand Down Expand Up @@ -852,6 +853,9 @@ struct
let* tac = match tacs lbl, tp with
| Some tac, _ -> RM.ret tac
| None, ElStable (`Ext (0,_ ,`Global (Cof cof), _)) ->
(* This is a case where we can avoid matching on ElStable.
We should instead check if the type is "judgmentally contractible" --- which can be implemented by a relatively simple type-directed algorithm.
*)
let* cof = RM.lift_cmp @@ Sem.cof_con_to_cof cof in
begin
RM.lift_cmp @@ CmpM.test_sequent [] cof |>> function
Expand Down
2 changes: 2 additions & 0 deletions src/frontend/Tactics.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,8 @@ open Monad.Notation (RM)
let is_total (sign : D.sign) =
let rec go acc = function
| D.Field (`User ["fib"],_,D.Clo ([],_)) -> RM.ret @@ acc

(* TODO: Let's avoid this kind of matching; maybe a good first step is even to make each field come equipped uniformly with a partial element. I favor that... *)
| D.Field (lbl,(D.ElStable (`Ext (0,_,`Global (Cof cof),_)) as tp),sign_clo) ->
let* cof = RM.lift_cmp @@ Sem.cof_con_to_cof cof in
RM.abstract (lbl :> Ident.t) tp @@ fun v ->
Expand Down