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

pretty printing

Browse source
This commit is contained in:
William Ball 2024-08-12 00:22:16 -07:00
parent c1c25e643b
commit 0c458b0833
8 changed files with 149 additions and 69 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
lib/forgejo.ballcloud.cc/wball/proof-checker/FORMULA.sig
View file

@ -20,4 +20,7 @@ sig
val matchVariable: int -> t * t -> Term.t option
val occurs: Term.t -> t -> bool
val ppd: int -> int -> t -> string
val pp: t -> string
end

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

@ -75,18 +75,63 @@ struct
| matchVariable x (Iff (phi, psi), Iff (phi', psi')) =
Term.mergeOption
(matchVariable x (phi, phi'), matchVariable x (psi, psi'))
| matchVariable x (Exists phi, Exists psi) = matchVariable (x + 1) (phi, psi)
| matchVariable x (Forall phi, Forall psi) = matchVariable (x + 1) (phi, psi)
| matchVariable x (Exists phi, Exists psi) =
matchVariable (x + 1) (phi, psi)
| matchVariable x (Forall phi, Forall psi) =
matchVariable (x + 1) (phi, psi)
| matchVariable _ _ = raise MatchFailure
fun occurs t (Relation (_, ts)) = List.exists (Term.occurs t) ts
| occurs t (Equal (p, q)) = Term.occurs t p orelse Term.occurs t q
fun occurs t (Relation (_, ts)) =
List.exists (Term.occurs t) ts
| occurs t (Equal (p, q)) =
Term.occurs t p orelse Term.occurs t q
| occurs t Bottom = false
| occurs t (Neg phi) = occurs t phi
| occurs t (Conj (phi, psi)) = occurs t phi orelse occurs t psi
| occurs t (Disj (phi, psi)) = occurs t phi orelse occurs t psi
| occurs t (Impl (phi, psi)) = occurs t phi orelse occurs t psi
| occurs t (Iff (phi, psi)) = occurs t phi orelse occurs t psi
| occurs t (Exists phi) = occurs (Term.incVars t) phi
| occurs t (Forall phi) = occurs (Term.incVars t) phi
| occurs t (Conj (phi, psi)) =
occurs t phi orelse occurs t psi
| occurs t (Disj (phi, psi)) =
occurs t phi orelse occurs t psi
| occurs t (Impl (phi, psi)) =
occurs t phi orelse occurs t psi
| occurs t (Iff (phi, psi)) =
occurs t phi orelse occurs t psi
| occurs t (Exists phi) =
occurs (Term.incVars t) phi
| occurs t (Forall phi) =
occurs (Term.incVars t) phi
val precedence =
fn Bottom => 10
| Relation _ => 10
| Equal _ => 10
| Neg _ => 9
| Conj _ => 8
| Disj _ => 7
| Impl _ => 6
| Iff _ => 5
| Forall _ => 4
| Exists _ => 4
fun ppd d prec prop =
let
val np = precedence prop
val str =
case prop of
Bottom => "\226\138\165"
| Relation (f, args) =>
f ^ "(" ^ (String.concatWith ", " (map (Term.ppd d) args)) ^ ")"
| 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
| Conj (phi, psi) => ppd d np phi ^ " \226\136\167 " ^ ppd d np psi
| Disj (phi, psi) => ppd d np phi ^ " \226\136\168 " ^ ppd d np psi
| Impl (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
| Exists phi => "\226\136\131" ^ Var.name d ^ ". " ^ ppd (d + 1) np phi
in
if np < prec then "(" ^ str ^ ")" else str
end
val pp = ppd 0 0
end

5
lib/forgejo.ballcloud.cc/wball/proof-checker/Proof.sml
View file

@ -20,7 +20,7 @@ struct
| ExistsI
| ExistsE
exception ProofError of int
exception ProofError of string
datatype t = Proof of {children: t list, label: label, formula: Formula.t}
@ -209,8 +209,7 @@ struct
| _ => false handle MatchFailure => false)
| valid
( Proof
{ children =
[ kid as Proof {formula = Exists phi, ...} ]
{ children = [kid as Proof {formula = Exists phi, ...}]
, label = ExistsE
, formula = psi
}

4
lib/forgejo.ballcloud.cc/wball/proof-checker/TERM.sig
View file

@ -18,4 +18,8 @@ sig
val incVars: t -> t
val occurs: t -> t -> bool
val ppd: int -> t -> string
val pp: t -> string
end

25
lib/forgejo.ballcloud.cc/wball/proof-checker/Term.sml
View file

@ -46,16 +46,33 @@ struct
| matchVariable x (Function (f, ts), Function (g, ss)) =
foldl mergeOption NONE (map (matchVariable x)
(ListPair.zipEq (ts, ss) handle UnequalLengths => raise MatchFailure))
| matchVariable _ (Free s1, Free s2) = if s1 = s2 then NONE else raise MatchFailure
| matchVariable _ (Free s1, Free s2) =
if s1 = s2 then NONE else raise MatchFailure
| matchVariable _ _ = raise MatchFailure
fun incVars (Var x) = Var (x + 1)
| incVars (Function (f, args)) = Function (f, map incVars args)
fun incVars (Var x) =
Var (x + 1)
| incVars (Function (f, args)) =
Function (f, map incVars args)
| incVars t = t
fun occurs (Const s1) (Const s2) = s1 = s2
| occurs (Var x1) (Var x2) = x1 = x2
| occurs t (Function (_, ts)) = List.exists (occurs t) ts
| occurs t (Function (_, ts)) =
List.exists (occurs t) ts
| occurs (Free s1) (Free s2) = s1 = s2
| occurs _ _ = false
fun ppd depth (Const s) = s
| ppd depth (Free s) = s
| ppd depth (Var x) =
Var.name (depth - x - 1)
| ppd depth (Function (f, x :: rest)) =
f ^ "("
^
(foldl (fn (s, acc) => acc ^ ", " ^ s) (ppd depth x)
(map (ppd depth) rest)) ^ ")"
| ppd depth (Function (f, [])) = f ^ "()"
val pp = ppd 0
end

4
lib/forgejo.ballcloud.cc/wball/proof-checker/VAR.sig Normal file
View file

@ -0,0 +1,4 @@
signature VAR =
sig
val name: int -> string
end

6
lib/forgejo.ballcloud.cc/wball/proof-checker/Var.sml Normal file
View file

@ -0,0 +1,6 @@
structure Var: VAR =
struct
val name_list = ["x", "y", "z", "w", "u", "v"]
fun name x =
if x < 6 then List.nth (name_list, x) else "x" ^ Int.toString (x - 6)
end

2
lib/forgejo.ballcloud.cc/wball/proof-checker/proof-checker.mlb
View file

@ -1,6 +1,8 @@
$(SML_LIB)/basis/basis.mlb
../../../github.com/diku-dk/sml-parse/parse.mlb
../../../github.com/diku-dk/sml-parse/simple_token.mlb
VAR.sig
Var.sml
TERM.sig
Term.sml
FORMULA.sig