Proof: Difference between revisions
Content added Content deleted
m (→{{header|Wren}}: Minor tidy) |
(Added FreeBASIC) |
||
Line 622: | Line 622: | ||
Qed. |
Qed. |
||
</syntaxhighlight> |
</syntaxhighlight> |
||
=={{header|FreeBASIC}}== |
|||
{{trans|Phix}} |
|||
<syntaxhighlight lang="vbnet">Type Axioma |
|||
r As String |
|||
s As String |
|||
End Type |
|||
Dim Shared axiomas(1 To 6) As Axioma |
|||
axiomas(1).r = "even+1": axiomas(1).s = "odd" |
|||
axiomas(2).r = "even": axiomas(2).s = "2*int" |
|||
axiomas(3).r = "2*int+2*int": axiomas(3).s = "2*(int+int)" |
|||
axiomas(4).r = "(int+int)": axiomas(4).s = "int" |
|||
axiomas(5).r = "2*int": axiomas(5).s = "even" |
|||
axiomas(6).r = "odd": axiomas(6).s = "2*int+1" |
|||
Sub Proof(a As String, b As String) |
|||
'-- try to convert a into b using only the above axiomas |
|||
Dim As String w = a |
|||
Dim As String seen() ' -- (avoid infinite loops) |
|||
Dim As Integer i, k, hit |
|||
Do |
|||
Print Using """&"""; w |
|||
Redim Preserve seen(Lbound(seen) To Ubound(seen) + 1) |
|||
seen(Ubound(seen)) = w |
|||
If w = b Then Exit Do |
|||
hit = 0 |
|||
For i = Lbound(axiomas) To Ubound(axiomas) |
|||
k = Instr(w, axiomas(i).r) |
|||
If k > 0 Then |
|||
w = Left(w, k - 1) & axiomas(i).s & Mid(w, k + Len(axiomas(i).r)) |
|||
hit = i |
|||
Exit For |
|||
End If |
|||
Next i |
|||
Print " == "; |
|||
Loop Until hit = 0 |
|||
Print Using "{""&"", ""&"", &}"; a; b; Iif(w = b, "true", "false") |
|||
End Sub |
|||
Proof("even+even", "even") |
|||
Proof("even+1", "odd") |
|||
'--bad proofs: |
|||
Proof("int", "even") |
|||
Sleep</syntaxhighlight> |
|||
{{out}} |
|||
<pre>"even+even" |
|||
== "2*int+even" |
|||
== "2*int+2*int" |
|||
== "2*(int+int)" |
|||
== "2*int" |
|||
== "even" |
|||
{"even+even", "even", true} |
|||
"even+1" |
|||
== "odd" |
|||
{"even+1", "odd", true} |
|||
"int" |
|||
{"int", "even", false}</pre> |
|||
=={{header|Go}}== |
=={{header|Go}}== |