Skip to content

Commit 3ce44c0

Browse files
erikdsjostromerikdsjostrom
committed
Clean up and simplifying
1 parent a996ca6 commit 3ce44c0

File tree

2 files changed

+98
-94
lines changed

2 files changed

+98
-94
lines changed

‎Physics/src/Calculus/SyntaxTree.lhs‎

Lines changed: 87 additions & 86 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,16 @@
11
> module Calculus.SyntaxTree where
22

3-
> import Calculus.Calculus
3+
> import Calculus.Calculus as C
44
> import Data.Tree as T
55
> import Data.Tree.Pretty as P
66

7-
> -- | Pretty prints expressions as trees
7+
Pretty prints expressions as trees
8+
89
> printExpr :: FunExpr -> IO ()
910
> printExpr = putStrLn . drawVerticalTree . makeTree
1011

11-
> -- | Pretty prints the steps taken when canonifying an expression
12+
Pretty prints the steps taken when canonifying an expression
13+
1214
> prettyCan :: FunExpr -> IO ()
1315
> prettyCan e =
1416
> let t = makeTree e
@@ -19,8 +21,8 @@
1921
> putStrLn $ drawVerticalTree t
2022
> prettyCan e'
2123

22-
> -- Possible generalization, make it work on lists of Expr
23-
> -- | Pretty prints syntactic checking of equality
24+
Pretty prints syntactic checking of equality
25+
2426
> prettyEqual :: FunExpr -> FunExpr -> IO Bool
2527
> prettyEqual e1 e2 = if e1 == e2 then
2628
> do
@@ -32,147 +34,146 @@
3234
> putStrLn $ drawVerticalForest [makeTree e1, makeTree e2]
3335
> let c1 = canonify e1
3436
> c2 = canonify e2
35-
> in if c1 == e1 && c2 == e2 then putStrLn "Can't simplify no more" >> return False
36-
> else prettyEqual c1 c2
37-
38-
> -- Parse an expression as a Tree of Strings
39-
> makeTree :: FunExpr -> T.Tree String
40-
> makeTree (e1 :+ e2) = T.Node "+" [makeTree e1, makeTree e2]
41-
> makeTree (e1 :- e2) = T.Node "-" [makeTree e1, makeTree e2]
42-
> makeTree (e1 :* e2) = T.Node "*" [makeTree e1, makeTree e2]
43-
> makeTree (e1 :/ e2) = T.Node "Div" [makeTree e1, makeTree e2]
44-
> makeTree (Exp :. e) = T.Node "Exp" [makeTree e]
45-
> makeTree (e1 :. e2) = T.Node "o" [makeTree e1, makeTree e2]
46-
> makeTree Id = T.Node "Id" []
47-
> --makeTree (Lambda s e) = T.Node ("Lambda " ++ s) [makeTree e]
48-
> --makeTree (Func s) = T.Node s []
49-
> --makeTree (Delta e) = T.Node "Delta" [makeTree e]
50-
> makeTree (D e) = T.Node "D" [makeTree e]
51-
> --makeTree (e1 :$ e2) = T.Node "$" [makeTree e1, makeTree e2]
52-
> makeTree (Const num) = T.Node (show (floor num)) [] -- | Note the use of floor
53-
> makeTree Exp = T.Node "Exp" []
54-
> makeTree e = error $ show e
55-
56-
> -- Staged for removal
57-
> equals :: FunExpr -> FunExpr -> Bool
58-
> -- Addition is commutative
59-
> equals (e1 :+ e2) (e3 :+ e4) = (canonify (e1 :+ e2) == canonify (e3 :+ e4)) ||
60-
> (canonify (e1 :+ e2) == canonify (e4 :+ e3))
61-
> -- | Addition is associative
62-
> -- equals (e1 :+ (e2 :+ e3)) = undefined
63-
> -- Multiplication is commutative
64-
> equals (e1 :* e2) (e3 :* e4) = (canonify (e1 :* e2) == canonify (e3 :* e4)) ||
65-
> (canonify (e1 :* e2) == canonify (e4 :* e3))
66-
> equals e1 e2 = canonify e1 == canonify e2
37+
> in if c1 == e1 && c2 == e2 then putStrLn "Can't simplify no more"
38+
> >> return False
39+
> else prettyEqual c1 c2
40+
41+
Syntactic checking of equality
42+
43+
> equal :: FunExpr -> FunExpr -> Bool
44+
> equal e1 e2 = case e1 == e2 of
45+
> True -> True
46+
> False -> let c1 = canonify e1
47+
> c2 = canonify e2
48+
> in case e1 == c1 && c2 == e2 of
49+
> True -> False
50+
> False -> equal c1 c2
51+
52+
Parse an expression as a Tree of Strings
53+
54+
> makeTree :: FunExpr -> Tree String
55+
> makeTree (e1 :+ e2) = Node "+" [makeTree e1, makeTree e2]
56+
> makeTree (e1 :- e2) = Node "-" [makeTree e1, makeTree e2]
57+
> makeTree (e1 :* e2) = Node "*" [makeTree e1, makeTree e2]
58+
> makeTree (e1 :/ e2) = Node "Div" [makeTree e1, makeTree e2]
59+
> makeTree (e1 :^ e2) = Node "**" [makeTree e1, makeTree e2]
60+
> makeTree (e1 :. e2) = Node "o" [makeTree e1, makeTree e2]
61+
> makeTree (D e) = Node "d/dx" [makeTree e]
62+
> makeTree (Delta r e) = Node "Δ" [makeTree (Const r), makeTree e]
63+
> makeTree (I r e) = Node "I" [makeTree (Const r), makeTree e]
64+
> makeTree Id = Node "Id" []
65+
> makeTree Exp = Node "Exp" []
66+
> makeTree Log = Node "Log" []
67+
> makeTree Sin = Node "Sin" []
68+
> makeTree Cos = Node "Cos" []
69+
> makeTree Asin = Node "Asin" []
70+
> makeTree Acos = Node "Acos" []
71+
> makeTree (Const num) = Node (show (floor num)) [] -- | Note the use of floor
72+
73+
Of course this is all bit too verbose, but I'm keeping it that way until every
74+
case is covered, Calculus is a bit of a black box for me right now
6775

6876
> canonify :: FunExpr -> FunExpr
69-
> -- | Addition
70-
> -- | e + 0 = e
77+
78+
Addition
79+
7180
> canonify (e :+ Const 0) = canonify e
7281
> canonify (Const 0 :+ e) = canonify e
73-
> -- | Lifting
7482
> canonify (Const x :+ Const y) = Const (x + y)
7583
> canonify (e1 :+ e2) = canonify e1 :+ canonify e2
7684

77-
> -- | Subtraction
78-
> -- | e - 0 = e
85+
Subtraction
86+
7987
> canonify (e :- Const 0) = canonify e
80-
> -- | 0 - b = -b
81-
> --canonify (Const 0 :- b) = negate (canonify b)
82-
> -- | Lifting
8388
> canonify (Const a :- Const b) = Const (a - b)
8489
> canonify (e1 :- e2) = canonify e1 :- canonify e2
85-
>
86-
> -- | Multiplication
87-
> -- | e * 0 = 0 (Kills the tree immediately)
90+
91+
Multiplication
92+
8893
> canonify (_ :* Const 0) = Const 0
8994
> canonify (Const 0 :* _) = Const 0
90-
> -- | e * 1 = e
9195
> canonify (e :* Const 1) = canonify e
9296
> canonify (Const 1 :* e) = canonify e
93-
> -- | Lifting
9497
> canonify (Const a :* Const b) = Const (a * b)
95-
> -- | Propagate
9698
> canonify (e1 :* e2) = canonify e1 :* canonify e2
97-
>
98-
> -- | Division
99+
100+
Division
101+
99102
> canonify (Const a :/ Const b) = Const (a / b)
100103
> canonify (e1 :/ e2) = canonify e1 :/ canonify e2
101-
>
102-
> -- | Lambda
103-
> --canonify (Lambda p b) = Lambda p (canonify b)
104-
>
105-
> -- | Function
106-
> --canonify (Func string) = Func string
107-
>
108-
> -- | Application
109-
> --canonify (e1 :$ e2) = canonify e1 :$ canonify e2
110-
>
111-
> -- | Delta
112-
> --canonify (Delta e) = Delta $ canonify e
113-
>
114-
> -- | Derivative
104+
105+
Delta
106+
107+
> canonify (Delta r e) = Delta r $ canonify e
108+
109+
Derivatives
110+
115111
> canonify (D e) = derive e
116-
>
117-
> -- | Catch all
118-
> canonify (Const x) = Const x
119-
> canonify Id = Id
112+
113+
Composition
114+
120115
> canonify (e1 :. e2) = canonify e1 :. canonify e2
121-
> canonify e = error $ show e
122116

117+
Catch all
118+
119+
> canonify e = e
120+
121+
"Proofs"
122+
--------------
123123

124-
> -- | "Proofs"
125124
> syntacticProofOfComForMultiplication :: FunExpr -> FunExpr -> IO Bool
126125
> syntacticProofOfComForMultiplication e1 e2 = prettyEqual (e1 :* e2) (e2 :* e1)
127-
>
126+
128127
> syntacticProofOfAssocForMultiplication :: FunExpr -> FunExpr -> FunExpr -> IO Bool
129128
> syntacticProofOfAssocForMultiplication e1 e2 e3 = prettyEqual (e1 :* (e2 :* e3))
130129
> ((e1 :* e2) :* e3)
131-
>
130+
132131
> syntacticProofOfDistForMultiplication :: FunExpr -> FunExpr -> FunExpr -> IO Bool
133132
> syntacticProofOfDistForMultiplication e1 e2 e3 = prettyEqual (e1 :* (e2 :+ e3))
134133
> ((e1 :* e2) :+ (e1 :* e3))
135-
>
134+
136135
> {- syntacticProofOfIdentityForMultiplication :: FunExpr -> IO Bool -}
137136
> {- syntacticProofOfIdentityForMultiplication e = -}
138137
> {- putStrLn "[*] Checking right identity" >> -}
139138
> {- prettyEqual e (1 :* e) >> -}
140139
> {- putStrLn "[*] Checking left identity" >> -}
141140
> {- prettyEqual e (e :* 1) -}
142-
>
141+
143142
> {- syntacticProofOfPropertyOf0ForMultiplication :: FunExpr -> IO Bool -}
144143
> {- syntacticProofOfPropertyOf0ForMultiplication e = -}
145144
> {- prettyEqual (e :* 0) 0 -}
146-
>
145+
147146
> -- | Fails since default implementation of negate x for Num is 0 - x
148147
> {- syntacticProofOfPropertyOfNegationForMultiplication :: FunExpr -> IO Bool -}
149148
> {- syntacticProofOfPropertyOfNegationForMultiplication e = -}
150149
> {- prettyEqual (Const (-1) :* e) (negate e) -}
151-
>
150+
152151
> syntacticProofOfComForAddition :: FunExpr -> FunExpr -> IO Bool
153152
> syntacticProofOfComForAddition e1 e2 = prettyEqual (e1 :+ e2) (e2 :+ e1)
154-
>
153+
155154
> syntacticProofOfAssocForAddition :: FunExpr -> FunExpr -> FunExpr -> IO Bool
156155
> syntacticProofOfAssocForAddition e1 e2 e3 = prettyEqual (e1 :+ (e2 :+ e3))
157156
> ((e1 :+ e2) :+ e3)
158-
>
157+
159158
> test :: FunExpr -> FunExpr -> IO Bool
160159
> test b c = prettyEqual b (a :* c)
161160
> where
162161
> a = b :/ c
163-
>
164-
>
162+
163+
165164
> syntacticProofOfIdentityForAddition :: FunExpr -> IO Bool
166165
> syntacticProofOfIdentityForAddition e = putStrLn "[*] Checking right identity" >>
167166
> prettyEqual e (0 :+ e) >>
168167
> putStrLn "[*] Checking left identity" >>
169168
> prettyEqual e (e :+ 0)
170-
>
171-
> -- | Dummy expressions
172-
> --eT = D (Func "sin") :+ Func "cos" :$ (Const 2 :+ Const 3) :* (Const 3 :+ Const 2 :* Delta (Const 1 :+ Const 2)) :/ (Const 5 :- (Const 4 :+ Const 8)) :+ Lambda "x" (Const 2)
169+
170+
Dummy expressions
171+
173172
> e1 = Const 1
174173
> e2 = Const 2
175174
> e3 = Const 3
176175
> e4 = (Const 1 :+ Const 2) :* (Const 3 :+ Const 4)
177176
> e5 = (Const 1 :+ Const 2) :* (Const 4 :+ Const 3)
178177
> e6 = Const 2 :+ Const 3 :* Const 8 :* Const 19
178+
> e7 = (Delta 3 ((Delta (0 - 5) (I 7 Acos)) :. (Acos :* Exp)))
179+

‎Physics/src/NewtonianMechanics/SingleParticle.lhs‎

Lines changed: 11 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -97,6 +97,9 @@ equal to the change in kinetic energy $E_k$ of the particle:
9797

9898
Let's codify this theorem:
9999

100+
PS: This used to work just fine, but it no longer does since the switch to
101+
FunExpr. Problem probably lies somewhere in SyntaxTree
102+
100103
> prop_WorkEnergyTheorem :: Mass -> VectorE -> VectorE -> IO Bool
101104
> prop_WorkEnergyTheorem m v1 v2 = prettyEqual deltaEnergy (kineticEnergy displacedParticle)
102105
> where
@@ -108,7 +111,9 @@ Let's codify this theorem:
108111

109112
> -- Test values
110113
> v1 = V3 (3 :* Id) (2 :* Id) (1 :* Id)
111-
> v2 = V3 2 2 (5 :* Id)
114+
> v2 = V3 0 0 (5 :* Id)
115+
> v3 = V3 0 (3 :* Id) 0 :: VectorE
116+
> v4 = V3 2 2 2 :: VectorE
112117
> m = 5
113118
> p1 = P v1 m
114119
> p2 = P v2 m
@@ -136,7 +141,7 @@ objects interacting, *r* is the distance between the centers of the masses and
136141
*G* is the gravitational constant.
137142

138143
The gravitational constant has been finely approximated through experiments
139-
and we can state it out code like this:
144+
and we can state it in our code like this:
140145

141146
> type Constant = FunExpr
142147
>
@@ -147,22 +152,20 @@ Now we can codify the law of universal gravitation using our definition
147152
of particles.
148153

149154
> lawOfUniversalGravitation :: Particle -> Particle -> FunExpr
150-
> lawOfUniversalGravitation p1 p2 = gravConst * ((m1 * m2) / r2)
155+
> lawOfUniversalGravitation p1 p2 = gravConst * ((m_1 * m_2) / r2)
151156
> where
152-
> m1 = mass p1
153-
> m2 = mass p2
157+
> m_1 = mass p1
158+
> m_2 = mass p2
154159
> r2 = square $ pos p2 - pos p1
155160

156161
If a particles position is defined as a vector representing its displacement
157162
from some origin O, then its heigh should be x. Or maybe it should be the
158163
magnitude of the vector, if the gravitational force originates from O. Hmmm
159164

160-
This seems so weird since I don't know what the frame of reference is...
165+
This seems weird since I don't know what the frame of reference is...
161166

162167
> potentialEnergy :: Particle -> Energy
163168
> potentialEnergy p = undefined
164169
> where
165170
> m = mass p
166171
> (V3 x _ _) = pos p
167-
168-
TODO!!!! Fix prettyCan $ lawOfUniversalGravitation p1 p2

0 commit comments

Comments
 (0)