wball/proof-checker
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Compare commits

base: wball:607b9f1d7d68f4dfc6c1379c510fb1ec8b8d0c95
Branches Tags
wball:main
..
compare: wball:9cf96669e1cbe77a4ff234ab789863b896c7fc5a
Branches Tags
wball:main

No commits in common. "607b9f1d7d68f4dfc6c1379c510fb1ec8b8d0c95" and "9cf96669e1cbe77a4ff234ab789863b896c7fc5a" have entirely different histories.
607b9f1d7d ... 9cf96669e1

4 changed files with 10 additions and 22 deletions
Show stats Expand all files Collapse all files

10
lib/forgejo.ballcloud.cc/wball/proof-checker/kernel/Formula.sml
View file

@ -122,12 +122,10 @@ struct
f ^ "(" ^ (String.concatWith ", " (map (Term.ppd d) args)) ^ ")" f ^ "(" ^ (String.concatWith ", " (map (Term.ppd d) args)) ^ ")"
| Equal (t, s) => Term.ppd d t ^ " = " ^ Term.ppd d s | Equal (t, s) => Term.ppd d t ^ " = " ^ Term.ppd d s
| Neg (Equal (t, s)) => Term.ppd d t ^ " != " ^ Term.ppd d s | Neg (Equal (t, s)) => Term.ppd d t ^ " != " ^ Term.ppd d s
| Neg phi => "\194\172" ^ ppd d np phi | Neg phi => "~" ^ ppd d np phi
| Conj (phi, psi) => | Conj (phi, psi) => ppd d np phi ^ " \226\136\167 " ^ ppd d np psi
ppd d np phi ^ " \226\136\167 " ^ ppd d (np + 1) psi | Disj (phi, psi) => ppd d np phi ^ " \226\136\168 " ^ ppd d np psi
| Disj (phi, psi) => | Impl (phi, psi) => ppd d np phi ^ " => " ^ ppd d np psi
ppd d np phi ^ " \226\136\168 " ^ ppd d (np + 1) psi
| Impl (phi, psi) => ppd d (np + 1) phi ^ " => " ^ ppd d np psi
| Iff (phi, psi) => ppd d np phi ^ " <=> " ^ ppd d np psi | Iff (phi, psi) => ppd d np phi ^ " <=> " ^ ppd d np psi
| Forall phi => "\226\136\128" ^ Var.name d ^ ". " ^ ppd (d + 1) np phi | Forall phi => "\226\136\128" ^ Var.name d ^ ". " ^ ppd (d + 1) np phi
| Exists phi => "\226\136\131" ^ Var.name d ^ ". " ^ ppd (d + 1) np phi | Exists phi => "\226\136\131" ^ Var.name d ^ ". " ^ ppd (d + 1) np phi

17
lib/forgejo.ballcloud.cc/wball/proof-checker/parser/FormulaParser.sml
View file

@ -24,10 +24,10 @@ struct
open Scanner open Scanner
val prec = val prec =
fn AND => (7, 6) fn AND => (6, 7)
| OR => (5, 4) | OR => (4, 5)
| RARROW => (2, 3) | RARROW => (3, 2)
| LRARROW => (1, 1) | LRARROW => (1, 2)
| _ => (~1, ~1) | _ => (~1, ~1)
exception NotOperator exception NotOperator
@ -122,13 +122,8 @@ struct
val (lprec, rprec) = prec t val (lprec, rprec) = prec t
val comb = comb_func t val comb = comb_func t
in in
if lprec < mprec then if lprec < mprec then OK (v, r1, ts)
if connective t then else ((comb_p rprec) oo (fn res => comb (v, res))) rest
((comb_p 0) oo (fn res => comb (v, res))) rest
else
OK (v, r1, ts)
else
((comb_p rprec) oo (fn res => comb (v, res))) rest
end end
in in
comb_p 0 comb_p 0

2
lib/forgejo.ballcloud.cc/wball/proof-checker/parser/SCANNER.sig
View file

@ -18,6 +18,4 @@ sig
val scan: {srcname: string, input: string} -> (token * Region.reg) list val scan: {srcname: string, input: string} -> (token * Region.reg) list
val pp_token: token -> string val pp_token: token -> string
val connective: token -> bool
end end

3
lib/forgejo.ballcloud.cc/wball/proof-checker/parser/Scanner.sml
View file

@ -61,7 +61,4 @@ struct
| ERR => "unk" | ERR => "unk"
| HASH => "#" | HASH => "#"
| IDENT s => s | IDENT s => s
val connective =
fn AND => true | OR => true | RARROW => true | LRARROW => true | _ => false
end end