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

Compare commits

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

2 commits
9cf96669e1 ... 607b9f1d7d

Author SHA1 Message Date
William Ball
607b9f1d7d fixed parser ignoring tokens and flipped associativity the right way round 2024-08-13 16:08:08 -07:00
William Ball
55a1a9ce0a pretty printer now respects associativity 2024-08-13 16:07:54 -07:00
4 changed files with 22 additions and 10 deletions
Show stats Expand all files Collapse all files

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

@ -122,10 +122,12 @@ 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 => "~" ^ ppd d np phi | Neg phi => "\194\172" ^ ppd d np phi
| Conj (phi, psi) => ppd d np phi ^ " \226\136\167 " ^ ppd d np psi | Conj (phi, psi) =>
| Disj (phi, psi) => ppd d np phi ^ " \226\136\168 " ^ ppd d np psi ppd d np phi ^ " \226\136\167 " ^ ppd d (np + 1) psi
| Impl (phi, psi) => ppd d np phi ^ " => " ^ ppd d np psi | Disj (phi, 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 => (6, 7) fn AND => (7, 6)
| OR => (4, 5) | OR => (5, 4)
| RARROW => (3, 2) | RARROW => (2, 3)
| LRARROW => (1, 2) | LRARROW => (1, 1)
| _ => (~1, ~1) | _ => (~1, ~1)
exception NotOperator exception NotOperator
@ -122,8 +122,13 @@ 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 OK (v, r1, ts) if lprec < mprec then
else ((comb_p rprec) oo (fn res => comb (v, res))) rest if connective t then
((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,4 +18,6 @@ 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,4 +61,7 @@ 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