goals.tex revision bb1a72b84b087ebe2aae9e73ecf3caaefcb8a206
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu% Ligatur-Problem (z.b. bei specific wird aus dem fi eine ligatur
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu% gemacht, danach nicht mehr suchbar im acrobat-reader) wird mit
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu% diesem Eintrag behoben. Toll!
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu%%%%%%%%%%%%%%%%%%%%%%%%%%
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu\RequirePackage{ifpdf}
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu\RequirePackage{cmap}% Improve PDF text search.
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu%%%%%%%%%%%%%%%%%%%%%%%%%%
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu\documentclass[11pt,draft,a4paper]{article}%{scrartcl}%{report}
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu\usepackage{xspace}
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu\usepackage{amsmath}
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu\newcommand{\freecad}{FreeCAD\xspace}
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu\newcommand{\opencasc}{Open CASCADE\xspace}
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu\newcommand{\hets}{Hets\xspace}
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu\newcommand{\bash}[1]{{\tt #1}}
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu\newcommand{\haskell}[1]{{\tt #1}}
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu\newcommand{\setsep}[2]{\{#1~|~#2\}}
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu\newcommand{\leftsem}{[\![} %%
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu\newcommand{\rightsem}{]\!]} %%
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu\newcommand{\setsem}[1]{\leftsem #1 \rightsem} %% set semantics
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu\begin{document}
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu\title{Internship Goals for Robert Savu}
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu\author{Ewaryst Schulz}
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu\section{Reading \freecad documents}
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert SavuGiven a document containing a \freecad design (typically a *.fcstd-file) we want to import it into \hets. This requires the following:
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu\begin{description}
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu \item[Abstract Syntax:] an appropriate representation in \hets for \freecad designs,
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu i.e., the \freecad abstract syntax (mostly done)
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu \item[Semantics:] \freecad terms should have a semantics in the sense of 3D Pointsets (see section \ref{sec:semantics})
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu \item[Import:] an import method translating \freecad documents into this
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu representation (partly done, has to be integrated into one method)
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu \item[\hets Integration:] a complete integration of the \freecad logic into the \hets
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu logic-graph (partly done, signature and simple static analysis missing)
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu \item[\hets tool:] a hook into the hets program to open \freecad documents from there, i.e., \bash{hets -g test.fcstd} should work
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu \item[Pretty printing] for basic \freecad specs, i.e.,
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu \haskell{Pretty}-instances for the \freecad abstract syntax
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu\end{description}
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu\subsection{Semantics}
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu\label{sec:semantics}
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert SavuWe first give the semantics of some base objects such as rectangles,
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savuboxes, and cylinders. The goal is to specify the semantics for each of
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savuthe base objects used in the abstract syntax of \freecad and also for
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savuthe transformation by rotations and translations as well as for
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savucompound objects such as \haskell{Cut}, \haskell{Common},
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu\haskell{Fusion}, etc..
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu\begin{align}
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu\setsem{Rectangle(w, l)} & = \text{The set consisting of the four sides of the }\notag\\
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu & \qquad \text{rectangle in the x-y-plane}\notag\\
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu & = \setsep{(x,y,0)}{x\in[0,l], y\in\{0,w\}}\notag\\
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu & \quad \cup \setsep{(x,y,0)}{x\in\{0,l\}, y\in[0,w]}\\
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu\setsem{Box(h, l, w)} & = \text{The solid bounded by the faces of the box}\notag\\
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu & = [0,l]\times[0,w]\times[0,h]\\
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu\setsem{Cylinder(a, h, r)} & = \text{The ``pac-man'' cylinder along z-axis}\notag\\
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu & = circle\times[0,h]\\
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu \text{where}~ circle &=\setsep{(\rho\cdot cos(\alpha),\rho\cdot sin(\alpha))}{\alpha \in [0,a], \rho \in [0,r]}\notag\\
bb1a72b84b087ebe2aae9e73ecf3caaefcb8a206Robert Savu\setsem{Sphere(a_1, a_2, a_3, r)} & = \text{The intersection between a full sphere and a 'pac-man' cylinder}\notag\\
bb1a72b84b087ebe2aae9e73ecf3caaefcb8a206Robert Savu& \text {on the z-axis (which may cut a 'cake-slice' and also the nort-pole/south-pole caps)}\notag\\
bb1a72b84b087ebe2aae9e73ecf3caaefcb8a206Robert Savu& = \setsep{(x,y,z)}{x + y + z \leq r} \cap \notag\\
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu& \setsep{(\rho\cdot cos(\alpha),\rho\cdot sin(\alpha),z)}{z \in [sin(a_1),sin(a_2)]. \rho \in [0, \infty], \alpha \in [0, a_3]}\\
bb1a72b84b087ebe2aae9e73ecf3caaefcb8a206Robert Savu\setsem{Cone(a, r_1, r_2, h)} & = \text{The intersection between a fullright circular cone and a 'pac-man' cylinder}\notag\\
bb1a72b84b087ebe2aae9e73ecf3caaefcb8a206Robert Savu& = \setsep{(\rho \cdot cos(\alpha), \rho \cdot sin(\alpha), z)}{\rho \leq r_1 + {{z}\over{h}} \cdot (r_2 - r_1). z \in [0,h],\alpha \in [0, a]} \\
bb1a72b84b087ebe2aae9e73ecf3caaefcb8a206Robert Savu\setsem{Torus(a_1, a_2, a_3, r_1, r_2)} & = \text{a bit trickier: union between a torus and a cylinder with the same center and the}\notag\\
bb1a72b84b087ebe2aae9e73ecf3caaefcb8a206Robert Savu& \text {same symmetry axis all intersected with an infinite-radius z-axis centered 'pac-man' cylinder}\notag\\
bb1a72b84b087ebe2aae9e73ecf3caaefcb8a206Robert Savu& = \{(x,y,z)\} \cup \{(x_2,y_2,z_2)\}\notag\\
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu& \text{where:}\notag\\
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu& circle = \setsep{(\rho\cdot cos(\alpha), \rho\cdot sin(\alpha))}{\alpha \in [a_1, a_2], \rho \in [0,r_2]}\notag\\
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu& (rad, z) \in \setsep{(m,n)}{(-(m-r_1), n)\in circle}\notag\\
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu& x = rad\cdot cos (ang) \notag\\
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu& y = rad\cdot sin (ang) \notag\\
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu& ang \in [0, a_3] \notag\\
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu& \text{if } (a_1 \geq -180) \text{or} (a_2 \leq 180) \text {then} \notag\\
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu& (x_2,y_2,z_2 - r_2 \cdot sin(a_1)) \in \notag\\
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu&\setsem{Cone(a_3, r_1 - r_2 \cdot cos(a_1), r_1 - r_2 \cdot cos(a_2), sin(a_2) - sin(a_1))}\\
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu\setsem{Circle(sa, ea, r)} & = \setsep{(x,y,z)}{x = r\cdot cos(\alpha), y = r \cdot sin(\alpha), z = 0, \alpha \in [sa, ea]}\\
257da458dcbcd80e9a60a8d02990956cb1a8178aRobert Savu\end{document}