Stream: Elpi users & devs

Topic: ✔ Problem of unifying evars?

Pierre Vial (Sep 13 2022 at 09:29):

Hello,
I'm trying to write a tactic which, given a term m which is of the form:

match e with
  | C0 .... => f_0
  | C1 x1 .... xn =>  f1
  | .... end.

produces the statement : forall (x1 : A1) ... (xn : An), e = C1 x1 ... xn -> m = f1
Right now, I'm doing this:

Elpi Accumulate lp:{{
  pred essai i : term, i : list term, i : term, i : term, i : term, o : term.
     essai (fun X Ty F) L M E C  (prod X Ty Re) :- !, pi x\ decl x _ Ty =>  essai (F x) [x | L ] M E C  (Re x).
      essai F L M E C (prod _ (app [{{ @eq }}, _ , E , app [C | L] ]) (c\ app [{{@eq}}, _ , M , F ]) ).
}}.

Elpi Query lp:{{.     %%% This query produces an untypable term, but it succeeds
  essai (fun _ X0 c0\ fun _ (X1 c0) c1\ {{ true}}) []
  {{(match 2 with
  | 0 => true
  | S k => false
  end) }}
  {{2}} {{S}} P.
}}.


Elpi Tactic mytac.
Elpi Accumulate lp:{{
  solve (goal _ _ _ _ [trm M] as G) GL :-
    M  = (match E _ LCases),  coq.typecheck E Ty Ok,
    (global (indt I)  = Ty ; app [global (indt I) | _ ] = Ty),  coq.env.indt I _ _ P TyI Ks KTs,
    std.map Ks (x\ y\ y = global (indc x)) LCtors, %coq.say LCtors,
    std.nth 1 LCtors C,  std.nth 1 LCases F,   coq.mk-n-holes P H,
 coq.say "Ty is" Ty "\n\nF is " F  "\n\nM is" M  "\n\nE is" E "\n\nC is" C,
 essai F [] M E C Re, coq.say Re.        %%% If this line is commented, the queries below succeed
Elpi Typecheck.

Tactic Notation "mytac" constr(l) := elpi mytac (l).
Goal 2 +2 = 5.
mytac
     (match 2 with
  | 0 => true
  | S k => false
  end).
  mytac (match [1 ; 2] with
   | [] => false
   | _ :: _ => true
   end
  ).
Abort.

For some reason, the two last queries fail (without a specific message error). I dont' understand what does not work, since the tactic type-checks, and the parameters, which are printed, seem of the good form. So is this some problem of unifying an elpi variable?

Pierre Vial (Sep 13 2022 at 20:03):

What is very mysterious is that if I replace the last query of the tactic mytac (i.e. the line essai F [] M E C Re, coq.say Re) with the query

essai (fun _ X0 c0\ fun _ (X1 c0) c1\ {{ true}}) []
  {{(match 2 with
  | 0 => true
  | S k => false
  end) }}  {{2}} {{S}} P.

the calls of mytac below also fail.
I really don't understand why it should be so. I guess the problem is neither with unification nor with typechecking

Enrico Tassi (Sep 14 2022 at 06:14):

I'm sorry I don't have much time today. One mistake is that the third argument of coq.typecheck is Ok which is a variable, and not the constant ok.
The idiomatic way of calling it is std.assert-ok! (coq.typecheck T Ty) " some message" which tests if the result is ok, if not it prints the error message produced by Coq and prefixes it with some message.

Pierre Vial (Sep 14 2022 at 07:38):

Unfortunately, it does not seem that the problem was with ok, which I just corrected (actually, the printing commands below ensured that the type was correctly read)

Pierre Vial (Sep 14 2022 at 09:26):

OK, thanks to @Chantal Keller and @Louise Dubois de Prisque , I understood where the problem was: the predicate essai should have been between Elpi Tactic mytac. and Elpi Typecheck.
I was mistaken into thinking that accumulation would pass through Elpi tactics, commands and programs

Notification Bot (Sep 14 2022 at 10:38):

Pierre Vial has marked this topic as resolved.

Last updated: Oct 13 2024 at 01:02 UTC