@@ -256,20 +256,24 @@ unproduct tm =
256 try (unproduct (Var n1))
256 try (unproduct (Var n1))
257 try (unproduct (Var n2))
257 try (unproduct (Var n2))
259−||| If the goal is a tuple or a dependent pair, then split it into
259+||| Try to apply the constructors of the goal data type one by one,
260−||| two goals and return the new goal names.
260+||| and apply the first one that works. If one of the constructors work,
261−||| It fails if the goal is neither a `Pair` nor a `DPair`.
261+||| the explicit arguments to the constructor are created as new holes and
262+||| the hole names are returned in a list. The parameters of the type and
263+||| the implicit arguments of the constructor will be solved by unification.
264+||| Similar to `constructor` in Coq.
262−splitPair : Elab (TTName, TTName)
265+construct : Elab (List TTName)
264− let bug = [TextPart "Splitting created wrong number of holes"] in
265− case !goalType of
266+construct = case headName !goalType of
266− `(Pair ~A ~B) => do [x, y] <- apply `(MkPair {A=~A} {B=~B}) [False, False]
267+ Nothing =>
269− `(DPair ~A ~Pr) => do [x, y] <- apply `(MkDPair {a=~A} {P=~Pr}) [False, False]
272− _ => fail [TextPart "Goal is not a pair"]
268+ fail [TextPart "Goal is not of a type declared with the data keyword"]
270+ choiceMap (\(n, xs, _) => apply (Var n) (map shouldUnify xs) <* solve)
271+ !(constructors <$> lookupDatatypeExact h)
272+ <|> fail [TextPart "No constructors apply"]
274+ shouldUnify : CtorArg -> Bool
275+ shouldUnify (CtorField (MkFunArg _ _ Explicit _)) = False
276+ shouldUnify _ = True
274||| A special-purpose tactic that attempts to solve a goal using
278||| A special-purpose tactic that attempts to solve a goal using
275||| `Refl`. This is useful for ensuring that goals in fact are trivial
279||| `Refl`. This is useful for ensuring that goals in fact are trivial