From c2c11fa85819168f01da0d4745019115d4b46683 Mon Sep 17 00:00:00 2001 From: Jon Sterling Date: Thu, 26 May 2022 21:44:33 +0200 Subject: [PATCH 1/3] add a TODO --- src/core/Refiner.ml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/core/Refiner.ml b/src/core/Refiner.ml index 45b196f5a..6946641da 100644 --- a/src/core/Refiner.ml +++ b/src/core/Refiner.ml @@ -852,6 +852,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 From cc51b5698b72d715f42304fb1e87881cf7f0d98f Mon Sep 17 00:00:00 2001 From: Jon Sterling Date: Thu, 26 May 2022 23:54:56 +0200 Subject: [PATCH 2/3] TODO --- src/core/Refiner.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/core/Refiner.ml b/src/core/Refiner.ml index 6946641da..0a55bdb49 100644 --- a/src/core/Refiner.ml +++ b/src/core/Refiner.ml @@ -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 From d8fcf1a38ce55bfe7f8f09709dfdbb61d906b2fb Mon Sep 17 00:00:00 2001 From: Jon Sterling Date: Thu, 26 May 2022 23:55:46 +0200 Subject: [PATCH 3/3] TODO --- src/frontend/Tactics.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/frontend/Tactics.ml b/src/frontend/Tactics.ml index c93a1e50a..cf14fa727 100644 --- a/src/frontend/Tactics.ml +++ b/src/frontend/Tactics.ml @@ -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 ->