change syntax

README.md

@@ -72,7 +72,7 @@ claire
                   | inst(ident,predicate)
                   | noApply(rule)
                   | ident*argument.
-    decl        ::= theorem(thmIndex,formula,proof([command]))
+    decl        ::= theorem(thmIndex,formula,proof:[command])
                   | axiom(thmIndex,formula)
                   | import(atom)
                   | printProof
@@ -363,15 +363,15 @@ Prologは `=../2` を使って複合項を分離できるので分離して`or`,
                                   R=(G,[[Assm_|Assms]⊦Props|J_])
                                 },Err,{R=comError(inst, cannotInstantiate(Err),J)}).
     com(inst(_,_)    ,_,J,R) :- !,R=comError(inst,'empty judgement',J).
-    com(com(defer,[]),G,J,R) :- !,J=[J1|J_],append(J_,[J1],J_2),R=(G,J_2).
-    com(com(Com,Args),G,J,R) :- member(Com=Cmd,G.coms),
+    com(defer*[]     ,G,J,R) :- !,J=[J1|J_],append(J_,[J1],J_2),R=(G,J_2).
+    com(Com*Args     ,G,J,R) :- member(Com=Cmd,G.coms),
                                 !,catch({
                                   call(Cmd,G,Args,J,Cs),!,comRun((G,J),Cs,J_),!,R=(G,J_)
                                 },E,{
                                   E=comError(_,Err,_)->R=comError(Com,Err,J);
                                   true               ->R=comError(Com,E,J)
                                 }).
-    com(com(Com,_)   ,_,J,R) :- R=comError(Com, noSuchCom(Com),J).
+    com(Com*_        ,_,J,R) :- R=comError(Com, noSuchCom(Com),J).
 
 コマンドは規則を実行するapply,規則が動くことを確認するnoApply、定理を使って判断を増やすuse、判断のトップの置換をするinst、ユーザー定義コマンドを実行するcomがあります。ユーザー定義の組み込みコマンドにはdeferコマンドがありこれは最初の判断を最後に移動します。
 
@@ -392,7 +392,7 @@ Prologは `=../2` を使って複合項を分離できるので分離して`or`,
     decl(axiom(Idx,F),    G,R) :- !,catch({
                                     infer(G,F),!,insertThm(Idx,F,G,R)
                                   },Err,{R=error(axiom,typeError(F,Err))}).
-    decl(theorem(Idx,F,P),G,R) :- !,catch({ P=proof(Cs),
+    decl(theorem(Idx,F,P),G,R) :- !,catch({ P=proof:Cs,
                                     infer(G,F),!,G_=G.put(proof,[]),!,
                                     proofRun((G_,[[]⊦[F]]),Cs,insertThm(Idx,F),R)
                                   },Err,{R=error(theorem,typeError(F,Err))}).
@@ -404,7 +404,7 @@ Prologは `=../2` を使って複合項を分離できるので分離して`or`,
                                   },_,{R=error(plFile, plFileLoadError(N))}).
     decl(Dec*Arg,G,R) :- member(Dec=Fun,G.decls),!,
                                   call(Fun,Arg,Ds),declRun(G,Ds,R).
-    decl(D\ec*_,  _,R) :- !,R=error(Dec,noSuchDecl(Dec)).
+    decl(Dec*_,  _,R) :- !,R=error(Dec,noSuchDecl(Dec)).
 
 
 importは他のclファイルを読み込みます。

lib/hol.cl

@@ -51,17 +51,17 @@ axiom('True_or_False', eq*[or*[eqt*['P',true],eqt*['P',false]], true]).
 
 %% equality
 
-theorem(eqsym,eq*[eqt*[s,t],true] ==> eq*[eqt*[t,s],true],proof([
+theorem(eqsym,eq*[eqt*[s,t],true] ==> eq*[eqt*[t,s],true],proof:[
   apply([impR]),
   implyL*i([(eqsubst,['P':([x]=>eq*[eqt*[x,s],true])])]),
   implyR*[],
   use(eqrefl,[]),
   genR*i([(s,[])]),
   apply([forallR(t)]),
   apply([i])
-])).
+]).
 
-theorem(eqssubst,eq*[eqt*[t,s],true] ==> 'P'*[s] ==> 'P'*[t],proof([
+theorem(eqssubst,eq*[eqt*[t,s],true] ==> 'P'*[s] ==> 'P'*[t],proof:[
   genR*i([(s,[])]),
   genR*i([(t,[])]),
   apply([forallR(r),forallR(t)]),
@@ -76,4 +76,4 @@ theorem(eqssubst,eq*[eqt*[t,s],true] ==> 'P'*[s] ==> 'P'*[t],proof([
   apply([forallR(s)]),
   use(eqsubst,['P':([x]=>'P'*[x])]),
   apply([i])
-])).
+]).

lib/preliminaries.cl

@@ -2,7 +2,7 @@ plFile('lib/commands').
 constant(eq,a->a->prop).
 axiom(refl, eq*[r,r]).
 axiom(subst, eq*[a,b]==>'P'*[a]==>'P'*[b]).
-theorem(sym, eq*[r,s]==>eq*[s,r],proof([
+theorem(sym, eq*[r,s]==>eq*[s,r],proof:[
   apply([impR]),
   apply([cut(forall(a,forall(b, eq*[a,b]==>eq*[a,a]==>eq*[b,a])))]),
   use(subst,[]),
@@ -16,9 +16,9 @@ theorem(sym, eq*[r,s]==>eq*[s,r],proof([
   use(refl,[]),
   assumption*[],
   assumption*[]
-])).
+]).
 
-theorem(trans, eq*[r,s]==>eq*[s,t]==>eq*[r,t],proof([
+theorem(trans, eq*[r,s]==>eq*[s,t]==>eq*[r,t],proof:[
   apply([impR, impR]),
   apply([cut(forall(a,forall(b,eq*[a,b]==>eq*[r,a]==>eq*[r,b])))]),
   use(subst,[]),
@@ -31,25 +31,25 @@ theorem(trans, eq*[r,s]==>eq*[s,t]==>eq*[r,t],proof([
   apply([impL]),
   assumption*[],
   assumption*[]
-])).
+]).
 plFile('lib/eqCommands').
 
 %%%%%%%%
 
 theorem('Curry',('P'*[]==>'Q'*[]==>'R'*[])==>(and('P'*[], 'Q'*[])==>'R'*[]),
-proof([
+proof:[
   apply([impR, impR, pL(1), impL, andL1]),
   assumption*[],
   implyR*[],
   apply([andL2]),
   assumption*[]
-])).
+]).
 
 theorem('Uncurry',(and('P'*[], 'Q'*[])==>'R'*[])==>('P'*[]==>'Q'*[]==>'R'*[]),
-proof([
+proof:[
   apply([impR, impR, impR, pL(2)]),
   implyR*[],
   apply([andR]),
   assumption*[],
   assumption*[]
-])).
+]).

pcla.pl

@@ -107,7 +107,7 @@
 decl(axiom(Idx,F),    G,R) :- !,catch({
                                 infer(G,F),!,insertThm(Idx,F,G,R)
                               },Err,{R=error(axiom,typeError(F,Err))}).
-decl(theorem(Idx,F,P),G,R) :- !,catch({ P=proof(Cs),
+decl(theorem(Idx,F,P),G,R) :- !,catch({ P=proof:Cs,
                                 infer(G,F),!,G_=G.put(proof,[]),!,
                                 proofRun((G_,[[]⊦[F]]),Cs,insertThm(Idx,F),R)
                               },Err,{R=error(theorem,typeError(F,Err))}).

syntax_check.pl

@@ -53,8 +53,7 @@
 command(inst(I,P)) :- ident(I),predicate(P).
 command(noApply(R)) :- rule(R).
 command(I*A) :- ident(I),argument(A).
-proof(proof(Cs)) :- maplist(command,Cs).
-decl(theorem(I,F,Pr)) :- thmIndex(I),formula(F),proof(Pr).
+decl(theorem(I,F,proof:Cs)) :- thmIndex(I),formula(F),maplist(command,Cs).
 decl(axiom(I,F)) :- thmIndex(I),formula(F).
 decl(import(X)) :- atom(X).
 decl(printProof).

syntax_rtg.pl

@@ -53,7 +53,7 @@
               | inst(ident,predicate)
               | noApply(rule)
               | ident*argument.
-decl        ::= theorem(thmIndex,formula,proof([command]))
+decl        ::= theorem(thmIndex,formula,proof:[command])
               | axiom(thmIndex,formula)
               | import(atom)
               | printProof