Functional programming for compiling and decompiling computer-aided design
Functional programming for compiling and decompiling computer-aided design
复制标题
DOI：
10.1145/3236794
复制
发表时间：
2018-07
影响因子：
--
通讯作者：
Chandrakana Nandi;James R. Wilcox;P. Panchekha;Taylor Blau;D. Grossman;Zachary Tatlock
中科院分区：
文献类型：
--
作者：
Chandrakana Nandi;James R. Wilcox;P. Panchekha;Taylor Blau;D. Grossman;Zachary Tatlock
台式机制造技术（例如3D打印）越来越受欢迎，因为它们降低了按需生产定制对象的成本和复杂性。不幸的是，通常被称为“制造商”的早期采用者的充满活力的社区不是当前可用的软件管道服务的良好。今天的用户必须组成特质的工具序列，这些工具通常是最初为专家专家设计的专有软件的变体。本文提出了基本的编程技术技术，以为计算机辅助设计（CAD）软件管道提供改进的严格，降低的复杂性和新功能，以适用于3D打印等应用程序。从固体几何是一种编程语言的角度开始，组成性，典型语义，编译器的正确性和程序合成都在我们的方法中扮演关键角色。具体而言，我们为称为lambdacad和多边形表面网状中间表示的CAD定义了纯粹的功能语言。然后，我们将两种语言的典型语义定义为3D固体，以及从CAD到网格的编译器，并伴随着语义保存的证明。我们通过基于评估上下文来开发一种新颖的综合算法来说明该基金会的实用性，以“反编译”难以从在线制造商社区下载的难以编辑的网格，回到更典型的CAD程序。我们所有的原型都已在OCAML中实施，以进一步探索用于台式机制造的功能编程。
Desktop-manufacturing techniques like 3D printing are increasingly popular because they reduce the cost and complexity of producing customized objects on demand. Unfortunately, the vibrant communities of early adopters, often referred to as "makers," are not well-served by currently available software pipelines. Users today must compose idiosyncratic sequences of tools which are typically repurposed variants of proprietary software originally designed for expert specialists. This paper proposes fundamental programming-languages techniques to bring improved rigor, reduced complexity, and new functionality to the computer-aided design (CAD) software pipeline for applications like 3D-printing. Compositionality, denotational semantics, compiler correctness, and program synthesis all play key roles in our approach, starting from the perspective that solid geometry is a programming language. Specifically, we define a purely functional language for CAD called LambdaCAD and a polygon surface-mesh intermediate representation. We then define denotational semantics of both languages to 3D solids and a compiler from CAD to mesh accompanied by a proof of semantics preservation. We illustrate the utility of this foundation by developing a novel synthesis algorithm based on evaluation contexts to "reverse compile" difficult-to-edit meshes downloaded from online maker communities back to more-editable CAD programs. All our prototypes have been implemented in OCaml to enable further exploration of functional programming for desktop manufacturing.