wball/proof_checker
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

renamed match_result variants to be less confusing

Browse source
This commit is contained in:
William Ball 2024-09-02 21:53:23 -07:00
parent 2dc7624ede
commit e996e578a8
4 changed files with 32 additions and 32 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
lib/kernel/formula.ml
View file

@ -15,11 +15,11 @@ let rec match_term t phi psi =
| Relation (r1, ts1), Relation (r2, ts2) -> | Relation (r1, ts1), Relation (r2, ts2) ->
if r1 = r2 && List.length ts1 = List.length ts2 then if r1 = r2 && List.length ts1 = List.length ts2 then
List.map2 (Term.match_term t) ts1 ts2 List.map2 (Term.match_term t) ts1 ts2
|> List.fold_left Term.merge_result None |> List.fold_left Term.merge_result NoneSubst
else MatchErr else MatchErr
| Equal (t1, s1), Equal (t2, s2) -> | Equal (t1, s1), Equal (t2, s2) ->
Term.(merge_result (match_term t t1 t2) (match_term t s1 s2)) Term.(merge_result (match_term t t1 t2) (match_term t s1 s2))
| Bottom, Bottom -> None | Bottom, Bottom -> NoneSubst
| Neg phi, Neg psi -> match_term t phi psi | Neg phi, Neg psi -> match_term t phi psi
| Conj (phi1, psi1), Conj (phi2, psi2) -> | Conj (phi1, psi1), Conj (phi2, psi2) ->
Term.merge_result (match_term t phi1 phi2) (match_term t psi1 psi2) Term.merge_result (match_term t phi1 phi2) (match_term t psi1 psi2)

34
lib/kernel/proof.ml
View file

@ -58,38 +58,38 @@ let rec valid res a { children; label; formula } =
valid res a left && valid res a right valid res a left && valid res a right
&& &&
match Formula.match_term t right.formula phi with match Formula.match_term t right.formula phi with
| All s' -> s = s' | AllSubst s' -> s = s'
| Some s' -> s = s' | SomeSubst s' -> s = s'
| None -> true | NoneSubst -> true
| MatchErr -> false) | MatchErr -> false)
| [ kid ], ForallI, Forall phi -> ( | [ kid ], ForallI, Forall phi -> (
valid res a kid valid res a kid
&& &&
match Formula.match_term (Var 0) phi kid.formula with match Formula.match_term (Var 0) phi kid.formula with
| All (Free x) -> List.exists (Formula.occurs (Free x)) a |> not | AllSubst (Free x) -> List.exists (Formula.occurs (Free x)) a |> not
| All _ -> false | AllSubst _ -> false
| None -> true | NoneSubst -> true
| Some _ | MatchErr -> false) | SomeSubst _ | MatchErr -> false)
| [ ({ formula = Forall phi; _ } as kid) ], ForallE, psi -> ( | [ ({ formula = Forall phi; _ } as kid) ], ForallE, psi -> (
valid res a kid valid res a kid
&& &&
match Formula.match_term (Var 0) phi psi with match Formula.match_term (Var 0) phi psi with
| All _ -> true | AllSubst _ -> true
| None -> Formula.occurs (Var 0) phi |> not | NoneSubst -> Formula.occurs (Var 0) phi |> not
| Some _ | MatchErr -> false) | SomeSubst _ | MatchErr -> false)
| [ kid ], ExistsI, Exists phi -> ( | [ kid ], ExistsI, Exists phi -> (
valid res a kid valid res a kid
&& &&
match Formula.match_term (Var 0) phi kid.formula with match Formula.match_term (Var 0) phi kid.formula with
| All _ -> true | AllSubst _ -> true
| None -> Formula.occurs (Var 0) phi |> not | NoneSubst -> Formula.occurs (Var 0) phi |> not
| Some _ | MatchErr -> false) | SomeSubst _ | MatchErr -> false)
| [ ({ formula = Exists phi; _ } as kid) ], ExistsE, psi -> ( | [ ({ formula = Exists phi; _ } as kid) ], ExistsE, psi -> (
valid res a kid valid res a kid
&& &&
match Formula.match_term (Var 0) phi psi with match Formula.match_term (Var 0) phi psi with
| All (Free x) -> List.exists (Formula.occurs (Free x)) a |> not | AllSubst (Free x) -> List.exists (Formula.occurs (Free x)) a |> not
| All _ -> false | AllSubst _ -> false
| None -> true | NoneSubst -> true
| Some _ | MatchErr -> false) | SomeSubst _ | MatchErr -> false)
| _ -> false | _ -> false

24
lib/kernel/term.ml
View file

@ -6,28 +6,28 @@ type t =
| Free of string | Free of string
| Function of string * t list | Function of string * t list
type match_result = All of t | Some of t | None | MatchErr type match_result = AllSubst of t | SomeSubst of t | NoneSubst | MatchErr
let merge_result m1 m2 = let merge_result m1 m2 =
match (m1, m2) with match (m1, m2) with
| All t1, All t2 -> if t1 = t2 then All t1 else MatchErr | AllSubst t1, AllSubst t2 -> if t1 = t2 then AllSubst t1 else MatchErr
| All t1, Some _ -> Some t1 | AllSubst t1, SomeSubst _ -> SomeSubst t1
| Some _, All t2 -> Some t2 | SomeSubst _, AllSubst t2 -> SomeSubst t2
| Some t1, Some t2 -> if t1 = t2 then Some t1 else MatchErr | SomeSubst t1, SomeSubst t2 -> if t1 = t2 then SomeSubst t1 else MatchErr
| None, _ -> m2 | NoneSubst, _ -> m2
| _, None -> m1 | _, NoneSubst -> m1
| _ -> MatchErr | _ -> MatchErr
let rec match_term x t1 t2 = let rec match_term x t1 t2 =
if x = t1 then if t1 = t2 then Some t2 else All t2 if x = t1 then if t1 = t2 then SomeSubst t2 else AllSubst t2
else else
match (t1, t2) with match (t1, t2) with
| Var v1, Var v2 -> if v1 = v2 then None else MatchErr | Var v1, Var v2 -> if v1 = v2 then NoneSubst else MatchErr
| Const s1, Const s2 -> if s1 = s2 then None else MatchErr | Const s1, Const s2 -> if s1 = s2 then NoneSubst else MatchErr
| Free s1, Free s2 -> if s1 = s2 then None else MatchErr | Free s1, Free s2 -> if s1 = s2 then NoneSubst else MatchErr
| Function (f1, ts1), Function (f2, ts2) -> | Function (f1, ts1), Function (f2, ts2) ->
if f1 = f2 && List.(length ts1 = length ts2) then if f1 = f2 && List.(length ts1 = length ts2) then
List.(map2 (match_term x) ts1 ts2 |> fold_left merge_result None) List.(map2 (match_term x) ts1 ts2 |> fold_left merge_result NoneSubst)
else MatchErr else MatchErr
| _ -> MatchErr | _ -> MatchErr

2
lib/kernel/term.mli
View file

@ -6,7 +6,7 @@ type t =
| Free of string | Free of string
| Function of string * t list | Function of string * t list
type match_result = All of t | Some of t | None | MatchErr type match_result = AllSubst of t | SomeSubst of t | NoneSubst | MatchErr
val merge_result : match_result -> match_result -> match_result val merge_result : match_result -> match_result -> match_result
val match_term : t -> t -> t -> match_result val match_term : t -> t -> t -> match_result