I haven't minimized this much, but here's a self-contained file reproducing the error:
Require Import Ltac2.Ltac2.
Module Option.
Ltac2 equal (eqb : 'a -> 'b -> bool) (x : 'a option) (y : 'b option)
:= match x with
| None
=> match y with
| None => true
| Some _ => false
end
| Some x
=> match y with
| None => false
| Some y => eqb x y
end
end.
End Option.
Module List.
Ltac2 rec fold_right f a ls :=
match ls with
| [] => a
| l :: ls => f l (fold_right f a ls)
end.
Ltac2 rec fold_left (f : 'a -> 'b -> 'a) (xs : 'b list) (a : 'a) :=
match xs with
| [] => a
| x :: xs => fold_left f xs (f a x)
end.
Ltac2 rec map f ls :=
match ls with
| [] => []
| l :: ls => f l :: map f ls
end.
Ltac2 rec iter f ls :=
match ls with
| [] => ()
| l :: ls => f l; iter f ls
end.
Ltac2 rec find f xs :=
match xs with
| [] => None
| x :: xs => match f x with
| true => Some x
| false => find f xs
end
end.
Ltac2 rec find_rev f xs :=
match xs with
| [] => None
| x :: xs => match find_rev f xs with
| Some v => Some v
| None => match f x with
| true => Some x
| false => None
end
end
end.
Ltac2 rec rev_append l l' :=
match l with
| [] => l'
| x :: xs => rev_append xs (x :: l')
end.
Ltac2 rev ls := rev_append ls [].
Ltac2 rec all f ls :=
match ls with
| [] => true
| x :: xs => match f x with
| true => all f xs
| false => false
end
end.
Ltac2 rec app ls1 ls2 :=
match ls1 with
| [] => ls2
| x :: xs => x :: app xs ls2
end.
Ltac2 rec any f ls :=
match ls with
| [] => false
| x :: xs => match f x with
| true => true
| false => any f xs
end
end.
End List.
Module Message.
Ltac2 join sep ms :=
match ms with
| [] => Message.of_string ""
| m :: ms
=> List.fold_left (fun a b => Message.concat a (Message.concat sep b))
ms
m
end.
Ltac2 print sep ms :=
match sep with
| Some sep
=> Message.print (Message.join sep ms)
| None => Message.print (Message.join (Message.of_string "") ms)
end.
End Message.
Module Ident.
Ltac2 rec find_error id xs :=
match xs with
| [] => None
| x :: xs
=> let ((id', val)) := x in
match Ident.equal id id' with
| true => Some val
| false => find_error id xs
end
end.
Ltac2 find id xs :=
match find_error id xs with
| None => Control.zero Not_found
| Some val => val
end.
End Ident.
Module Control.
Ltac2 Type match_options := { multi : bool ; lazy : bool ; reverse : bool }.
Ltac2 update_reverse (opts : match_options) (new_val : bool) :=
{ multi := opts.(multi) ; lazy := opts.(lazy) ; reverse := new_val }.
Ltac2 update_multi (opts : match_options) (new_val : bool) :=
{ multi := new_val ; lazy := opts.(lazy) ; reverse := opts.(reverse) }.
Ltac2 update_lazy (opts : match_options) (new_val : bool) :=
{ multi := opts.(multi) ; lazy := new_val ; reverse := opts.(reverse) }.
Ltac2 rec multimatch_list_aux (f : 'a -> 'b) (ls : 'a list) (e : exn) :=
match ls with
| [] => Control.zero e
| x :: xs => Control.plus
(fun () => f x)
(fun e' =>
match e' with
| Match_failure => multimatch_list_aux f xs e
| _ => multimatch_list_aux f xs e'
end)
end.
Ltac2 multimatch_list (f : 'a -> 'b) (ls : 'a list) :=
multimatch_list_aux f ls Match_failure.
Ltac2 match_list_gen (opts : match_options) (f : 'a -> 'b) (ls : 'a list) :=
let maybe_once := match opts.(multi) with
| false => Control.once
| true => fun f => f ()
end in
let ls := match opts.(reverse) with
| true => List.rev ls
| false => ls
end in
maybe_once (fun () => multimatch_list f ls).
Ltac2 match_list f ls :=
Control.once (fun () => multimatch_list f ls).
Ltac2 match0_gen opts constr_val branches :=
match opts.(lazy) with
| true
=> Control.match_list_gen
opts
(fun v
=> let ((pat, tac)) := v in
let matches := Pattern.matches pat constr_val in
fun () => tac matches)
branches
()
| false
=> Control.match_list_gen
opts
(fun v
=> let ((pat, tac)) := v in
let matches := Pattern.matches pat constr_val in
tac matches)
branches
end.
Ltac2 match_goal_gen
(opts : match_options)
(branches : ((((ident * constr option * constr) list) * constr -> 'a) list))
:=
let ctx := match opts.(reverse) with
| true => Control.hyps ()
| false => List.rev (Control.hyps ())
end in
let gl := Control.goal () in
let opts := update_reverse opts false in
Control.match_list_gen
opts
(fun f => f (ctx, gl))
branches.
Ltac2 match0 constr_val branches :=
match0_gen { multi := false ; lazy := false ; reverse := false } constr_val branches.
Ltac2 lazymatch0 constr_val branches :=
match0_gen { multi := false ; lazy := true ; reverse := false } constr_val branches.
Ltac2 multimatch0 constr_val branches :=
match0_gen { multi := true ; lazy := false ; reverse := false } constr_val branches.
Ltac2 app_nonlinear_bindings existing_bindings new_bindings :=
match List.all
(fun b
=> let ((id, body)) := b in
match Ident.find_error id existing_bindings with
| None => true
| Some body' => Constr.equal body body'
end)
new_bindings with
| true => List.app existing_bindings new_bindings
| false => Control.zero Match_failure
end.
Ltac2 rec enforce_distinct_hyps (ls : (ident option * ident) list) :=
match ls with
| [] => ()
| x :: xs
=> let ((id, idh)) := x in
match List.any
(fun ((id', idh'))
=> match Ident.equal idh idh' with
| true => true
| false
=> match id with
| None => false
| Some id
=> match id' with
| None => false
| Some id' => Ident.equal id id'
end
end
end)
xs
with
| true => Control.zero Match_failure
| false => enforce_distinct_hyps xs
end
end.
Ltac2 Type PatternType := [ NormalPattern | ContextPattern (ident option) ].
Ltac2 pattern_gen_matches (pat : PatternType * pattern) (v : constr) :=
let ((pat_ty, pat)) := pat in
match pat_ty with
| NormalPattern
=> (None, Pattern.matches pat v)
| ContextPattern id
=> let ((ctx, bindings)) := Pattern.matches_subterm pat v in
(Some (id, ctx), bindings)
end.
Ltac2 match_goal0_gen_aux
(opts : match_options)
(branches : (((ident option * (PatternType * pattern) option * (PatternType * pattern)) list) *
(PatternType * pattern) *
((((ident option * Pattern.context) option) list (* body ctx *)) *
(((ident option * Pattern.context) option) list (* type ctx *)) *
((ident option * Pattern.context) option (* goal ctx *)) *
((ident option * ident) list (* hyp name bindings *)) *
((ident * constr) list (* bindings *))
-> 'a))
list)
:=
let opts_no_rev := update_reverse opts false in
let opts_no_rev_multi := update_multi opts_no_rev true in
match_goal_gen
opts
(List.map
(fun ((hyp_pats, gl_pat, tac)) ((hyps, gl))
=> let ((gl_ctx, gl_bindings)) := pattern_gen_matches gl_pat gl in
let hyp_matches :=
List.map
(fun ((id, body_pat, ty_pat))
=> Control.match_list_gen
opts_no_rev_multi
(fun ((idh, body, ty))
=> let ((body_ctx, body_bindings)) :=
match body_pat with
| None => (None, [])
| Some body_pat
=> match body with
| None => Control.zero Match_failure
| Some body
=> pattern_gen_matches body_pat body
end
end in
let ((ty_ctx, ty_bindings)) :=
pattern_gen_matches ty_pat ty in
((id, idh), body_ctx, ty_ctx,
app_nonlinear_bindings body_bindings ty_bindings))
hyps)
hyp_pats in
let ((id_idh, body_ctxs, ty_ctxs, bindings)) :=
List.fold_right
(fun ((id_idh', body_ctx', ty_ctx', bindings'))
((id_idh, body_ctxs, ty_ctxs, bindings))
=> ((id_idh' :: id_idh),
(body_ctx' :: body_ctxs),
(ty_ctx' :: ty_ctxs),
app_nonlinear_bindings bindings' bindings))
([], [], [], [])
hyp_matches in
enforce_distinct_hyps id_idh;
let bindings := app_nonlinear_bindings bindings gl_bindings in
tac (body_ctxs, ty_ctxs, gl_ctx, id_idh, bindings))
branches).
Ltac2 match_goal0_gen opts branches :=
let opts_no_lazy := update_lazy opts false in
match opts.(lazy) with
| false
=> match_goal0_gen_aux opts_no_lazy branches
| true
=> match_goal0_gen_aux
opts_no_lazy
(List.map
(fun ((hyps, gl, tac))
=> (hyps, gl, (fun args () => tac args)))
branches)
()
end.
Ltac2 match_goal0 branches :=
match_goal0_gen { multi := false ; lazy := false ; reverse := false } branches.
Ltac2 lazymatch_goal0 branches :=
match_goal0_gen { multi := false ; lazy := true ; reverse := false } branches.
Ltac2 match_hyps1_gen lazy ty_pattern tac :=
match_goal0_gen
{ multi := false ; lazy := lazy ; reverse := false }
[([(None, None, (NormalPattern, ty_pattern))],
(NormalPattern, pattern:(_)),
(fun ((body_ctx, ty_ctx, gl_ctx, hyp_names, bindings))
=> match hyp_names with
| [] => Control.throw Not_found
| h :: _
=> let ((_, hyp)) := h in
tac hyp bindings
end))].
Ltac2 match_hyps1 ty_pattern tac :=
match_hyps1_gen false ty_pattern tac.
Ltac2 lazymatch_hyps1 ty_pattern tac :=
match_hyps1_gen true ty_pattern tac.
End Control.
Class Ltac1Result {T} (v : T) := {}.
Ltac finishLtac1 v := assert (Ltac1Result v) by constructor.
Ltac2 get_ltac1_result () :=
Control.lazymatch_hyps1
(pattern:(Ltac1Result ?v))
(fun id matches
=> let val := Ident.find @v matches in
Std.clear [id];
val).
Class Ltac1Results {T} (v : list T) := {}.
Ltac finishLtac1s v := assert (Ltac1Result v) by constructor.
Ltac2 rec list_of_constr_list (ls : constr) :=
Control.lazymatch0
ls
[((pattern:((?x :: ?xs)%list)),
(fun matches
=> let x := Ident.find @x matches in
let xs := Ident.find @xs matches in
x :: list_of_constr_list xs))
;
((pattern:(_)),
(fun _ => ls :: []))].
Ltac2 get_ltac1_results () :=
Control.lazymatch_hyps1
(pattern:(Ltac1Results ?v))
(fun id matches
=> let val := Ident.find @v matches in
Std.clear [id];
list_of_constr_list val).
Class Ltac2Result {T} (v : T) := {}.
Ltac2 finishLtac2 v :=
Notations.refine '((fun res : Ltac2Result $v => _) ltac2:(Notations.constructor)).
Ltac get_ltac2_result _ :=
let dummy := match goal with _ => idtac "get_ltac2_result" end in
lazymatch goal with
| [ res : Ltac2Result ?v |- _ ]
=> let dummy := match goal with
| _ => clear res
end in
v
end.
(** Override this to get a faster [reify_type] *)
Ltac base_reify_type ty :=
lazymatch constr:(I : True) with ?v => v end.
Ltac2 mutable base_reify_type ty :=
Message.print None [Message.of_string "base_reify_type: "; Message.of_constr ty];
finishLtac2 ty;
Message.print None [Message.of_string "base_reify_type: calling Ltac1"];
ltac1:(let ty := get_ltac2_result () in
idtac "base_reify_type: ltac1:" ty;
let v := base_reify_type ty in
finishLtac1 v);
get_ltac1_result ().
(*strip_type_cast '(_ : reify type $ty).*)
Ltac2 reify_base_type ty := base_reify_type ty.
Goal True.
base_reify_type 'nat.
React
Typescript
Django
Laravel
Facebook
Microsoft
Google
Alibaba
D3
Tencent