-
Notifications
You must be signed in to change notification settings - Fork 0
/
cnv.php
90 lines (85 loc) · 1.98 KB
/
cnv.php
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
<?php
foreach(glob("results/*.txt") as $name) {
change($name);
}
foreach(glob("*.pl") as $name) {
change($name,true);
}
function change($name,$m=false) {
echo "$name\n";
$s = file_get_contents("$name");
$s = file_get_contents("../prolog1/$name");
/*
if($m){
$s = '
:- op(1200, xfx, [ --,iff ]).
term_expansion(A -- B, B :- A).
term_expansion(A iff B, A :- B).
'.$s;
}
*/
$keywords = array(
"tBool"=>"bool",
"tNat"=>"nat",
"tUnit"=>"unit",
"tFloat"=>"float",
"tString"=>"string",
"tTop"=>"top",
"tBot"=>"bot",
"tVar"=>"var",
"tArr"=>"arr",
"tRecord"=>"record",
"tAll"=>"all",
"tSome"=>"some",
"tAbs"=>"abs",
"tApp"=>"app",
"tRec"=>"rec",
"mTrue"=>"true",
"mFalse"=>"false",
"mIf"=>"if",
"mZero"=>"zero",
"mSucc"=>"succ",
"mPred"=>"pred",
"mIsZero"=>"iszero",
"mUnit"=>"unit",
"mFloat"=>"float",
"mTimesfloat"=>"timesfloat",
"mString"=>"string",
"mVar"=>"var",
"mAbs"=>"fn",
"mApp"=>"app",
"mLet"=>"let",
"mFix"=>"fix",
"mInert"=>"inert",
"mAscribe"=>"as",
"mRecord"=>"record",
"mProj"=>"proj",
"mTAbs"=>"tfn",
"mTApp"=>"tapp",
"mPack"=>"pack",
"mUnpack"=>"unpack",
"mUpdate"=>"update",
"tVariant"=>"variant",
"tRef"=>"ref",
"tSource"=>"source",
"tSink"=>"sink",
"mZero"=>"zero",
"mPred"=>"pred",
"mTag"=>"tag",
"mCase"=>"case",
"mRef"=>"ref",
"mDeref"=>"deref",
"mAssign"=>"assign",
"mLoc"=>"loc",
"mTry"=>"try",
"mError"=>"error",
"mFold"=>"fold",
"mUnfold"=>"unfold",
"kStar" => "*",
"G"=>"Γ",
);
foreach($keywords as $k=>$v) {
$s = preg_replace('/\\b'.$k.'\\b/s',$v,$s);
}
file_put_contents($name, $s);
}