coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Building a constructive term from inside an ML tactic

From: e AT x80.org (Emilio Jesús Gallego Arias)
To: Talia Ringer <tringer AT cs.washington.edu>
Cc: Coq-Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Building a constructive term from inside an ML tactic
Date: Wed, 11 Apr 2018 17:21:29 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=e AT x80.org; spf=Pass smtp.mailfrom=e AT x80.org; spf=Pass smtp.helo=postmaster AT x80.org
Ironport-phdr: 9a23:sQVZfRIURI1Rzdy8odmcpTZWNBhigK39O0sv0rFitYgRI/7xwZ3uMQTl6Ol3ixeRBMOHs6kC07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffwtFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QKsqUjq+8ahkVB7oiD8GNzEn9mHXltdwh79frB64uhBz35LYbISTOfFjfK3SYMkaSHJBUMhPSiJBBY28YYUNAOQCM+lXoJXyqkASrReiHwSgGP/jxyVKi3LwwKY00/4hEQbD3AE4Ad0Dq3vVodbpOKsIVuC11qbIxijHY/1Z3Df96YzIchEmofqRWbx/b9HR0VM0FwjYj1ufs4jlPzeL2eQCtGiQ8vZtVfiui2E9sAF9pz6izdoihInOg4Ia0FHE9SNhzYY6JN24VE57YcO/H5dKqy6aMI52T8U/SG9roCY30qAKtJ24cSQQ1pgr2R/SZ+aaf4WK/x7vTvudLDlmiH59er+yhQy+/VWgx+D/TMW4zVVHojZfntXSuX0Byxre4dWdRPRn5EeuwzOP2hjT6u5aJUA0krLWKpEiz7IsjJYTtl7DHiDulEX3iq+ZaFkk9/C15+nkYbjqvIGQO5F1hw3kL6gjmNGzDf4lPgUAQWSX4eG826fi/U39TrVKlPo2kqzBvZ/EPskaqa20DxNP3oYk8Ra/AC+q0M4EknkfMFJFZBWHgpD1NFHJOfD0FOuwg1CxkDhw3P3GJb3gApDVLnfZirvhfLB961RdyAUp19xf6YhUWfk9J6fPU0vwvZTiDxk2Phb8l/r9CdNy25k2UnnJHaaCMKLUvkOP4KQiL/TaN6EPvzOoJtA1t6aoimU20R8weKit3JxfSn2jjO8uDEydZXfjhZ8oC2YDpUttH6TRlFSeXGsLND6JVKUm62R+Udr+VNaRdsWWmLWEmRyDMNhTb2FCBEqLFCa6Z9XcHfAWZ3DLe5Mzonk/TbGkDrQZ+1S2rgarmao3dqzT4CJK7cu+hugw3PXakFQJzRIxD8mZ1DDfXzEs2GQSSG1v0Q==
Organization: X80 Heavy Industries

Talia Ringer
<tringer AT cs.washington.edu>
writes:

> Here's one way to build an inductive type and one of it's constructors
> given its FQ name and the index of the constructor, with example code that
> I wrote for sigT, which you can modify as needed. Zero guarantees it's
> up-to-date or the best way but hopefully it gets you somewhere.
>
> let coq_init_specif = ModPath.MPfile (DirPath.make (List.map
> Id.of_string ["Specif"; "Init"; "Coq"]))
>
> let sigT =
> mkInd (MutInd.make1 (KerName.make2 coq_init_specif (Label.make "sigT")),
> 0)
>
>
> let existT =
> mkConstruct (fst (destInd sigT), 1)

Indeed this is a very low-level way of accessing identifiers and I don't
recommend using it, as it will be fragile wrt refactorings.

The best way is to use the facilities of Coqlib:

https://github.com/coq/coq/blob/v8.8/library/coqlib.mli

But even these facilities will change soon to introduce a more abstract
interface so plugins can interact well with people that provide a custom
stdlib.

E.

[Coq-Club] Building a constructive term from inside an ML tactic, Kenneth Roe, 04/10/2018
- Re: [Coq-Club] Building a constructive term from inside an ML tactic, Talia Ringer, 04/10/2018
  - Re: [Coq-Club] Building a constructive term from inside an ML tactic, Emilio Jesús Gallego Arias, 04/11/2018