We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
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
(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "+implicit-core-hint-db,+implicits-in-term,+non-reversible-notation,+deprecated-intros-until-0,+deprecated-focus,+unused-intro-pattern,+deprecated-hint-constr,+fragile-hint-constr,+variable-collision,+unexpected-implicit-declaration,+omega-is-deprecated,+deprecated-instantiate-syntax,+non-recursive,+deprecated-hint-rewrite-without-locality,+deprecated-hint-without-locality,+deprecated-instance-without-locality,+undeclared-scope,+deprecated-typeclasses-transparency-without-locality,+future-coercion-class-field" "-w" "-deprecated-native-compiler-option,-native-compiler-disabled" "-R" "theories" "MetaCoq.Lob" "-top" "MetaCoq.Lob.Template.QuoteGround.Coq.MSets" "-native-compiler" "ondemand") -*- *) (* File reduced by coq-bug-minimizer from original input, then from 297 lines to 9 lines, then from 22 lines to 58 lines, then from 63 lines to 9 lines, then from 22 lines to 167 lines, then from 172 lines to 15 lines, then from 28 lines to 202 lines, then from 207 lines to 77 lines, then from 82 lines to 78 lines *) (* coqc version 8.16.0 compiled with OCaml 4.11.2 coqtop version 8.16.0 Expected coqc runtime on this file: 1.083 sec *) Require MetaCoq.Template.All. Import MetaCoq.Template.All. Import MetaCoq.Template.utils. Import MCMonadNotation. Class quotation_of {T} (t : T) := quoted_term_of : Ast.term. Class ground_quotable T := quote_ground : forall t : T, quotation_of t. Class debug_opt := debug : bool. Definition make_quotation_of {debug : debug_opt} {T} (t : T) : TemplateMonad (quotation_of t). Proof. simple refine (qt <- tmQuote t;; let tmInferQuotation t := (t <- tmUnquote t;; v <- (let '(existT_typed_term _ t) := t in tmInferInstance None (quotation_of t));; match v with | my_Some v => tmReturn v | my_None => (if debug then tmPrint (quotation_of t) else tmReturn tt);; tmFail "No typeclass instance" end) in match qt return TemplateMonad Ast.term with | tSort _ | tConst _ _ | tConstruct _ _ _ | tInt _ | tFloat _ | tInd _ _ => tmReturn qt | tCast t kind v => tmInferQuotation t | tApp f args => qf <- tmInferQuotation f;; qargs <- list_rect (fun _ => _) (tmReturn []) (fun arg args qargs => qarg <- tmInferQuotation arg;; qargs <- qargs;; tmReturn (qarg :: qargs)) args;; tmReturn (tApp qf qargs) | _ => tmFail "fail" end); exact _. Defined. Ltac make_quotation_of_goal _ := let t := match goal with |- quotation_of ?t => t end in run_template_program (make_quotation_of t) (fun v => exact v). #[export] Instance default_debug : debug_opt | 1000. Admitted. #[export] Existing Instance quote_ground. #[export] Hint Extern 2 (quotation_of ?t) => make_quotation_of_goal () : typeclass_instances. #[export] Instance quote_bool : ground_quotable bool. Admitted. #[export] Instance quote_eq_true {b} : ground_quotable (eq_true b). Admitted. Definition quote_of_iff {A B : Prop} {quoteA : ground_quotable A} {qA : quotation_of A} {qB : quotation_of B} (H : iff A B) {qH : quotation_of H} : ground_quotable B. Admitted. Import Coq.MSets.MSetInterface. Module QuoteWSetsOn (E : DecidableType) (Import W : WSetsOn E). #[export] Instance quote_Subset {x y} {qx : quotation_of x} {qy : quotation_of y} : ground_quotable (Subset x y). (quote_of_iff subset_spec). (* Error: Anomaly "in econstr: grounding a non evar-free term" Please report at http://coq.inria.fr/bugs/. *)
This is with Coq 8.16.
The text was updated successfully, but these errors were encountered:
No branches or pull requests
This is with Coq 8.16.
The text was updated successfully, but these errors were encountered: