#================================================================== SET VARIABLES takes a list of goals and returns a list of original variables, a binding environment and a counting environment as well as the original goals. Set_variables IS OPERATION Goals { EACH ( OPERATION It ( Variables := cull link ( EACH ( first second ) (second It) ) ; Bndev := ( tally Variables ) reshape [[ ]] ; Refev := ( tally Variables ) reshape [ -1 ] ; It Bndev Refev Variables ) ) Goals } #================================================================== BUILD PREDICATE TABLE generates a predicate table from a list of sentences represented in the ILR syntax. build_pred_table IS OPERATION Clauses { Pt := [ ] [ ] ; Index := 0 ; FOR S WITH Clauses DO Found Location := S @ @ [ 1, 1 , 1 , 0 ] seek Pt @ 0 ; IF not Found THEN Pt := ( Pt @ 0 link S @ @ [ 1, 1 , 1 , 0 ] ) ( Pt @ 1 link [ [ [ Index , S @@[1, 0] ] ] ] ) ; ELSE Values := Pt @ @ [ 1 , Location ] link [ [ Index , S @@[1, 0] ] ] ; Pt := Values [ 1 , Location ] deepplace Pt ; ENDIF ; Index := Index + 1 ; ENDFOR ; Pt } build_logic is op Filename { dropblanks is op A { A := reverse A; reverse (o find (` EACHRIGHT = A) drop A) }; Fn := open Filename "r; Clauses := Null; Goals := Null; Failed := o; WHILE not isfault (sentence := readfile Fn) DO WHILE last dropblanks sentence = `, DO IF not isfault(line := readfile Fn) THEN sentence := sentence link line; ELSE exit 1; ENDIF; ENDWHILE; IF not empty dropblanks sentence and not(first sentence = `#) THEN Structure := logparse sentence; IF isfault Structure THEN write sentence; write Structure; Failed := l; exit l; ELSE Type Result Vars := Structure; IF Type in ("axiom "rule) THEN Clauses := Clauses link [Type Result Vars]; ELSEIF Type in ("goal "goals) THEN IF empty Goals THEN Goals := [Type Result Vars]; ELSE Goals := Goals append (Type Result Vars); ENDIF; ELSE write sentence; write (Phrase 'Error --> ') Result; Failed := l; Exit l; ENDIF; ENDIF; ENDIF; ENDWHILE; close fn; IF not Failed THEN (set_variables Goals) (Clauses (build_pred_table Clauses)) ELSE ??parse_failed ENDIF } build_goals is { Class := ??; WHILE Class ~= "goals DO Class Result Vars := logparse readscreen 'Goal > '; ENDWHILE; Set_variables [Class Result Vars] } prover is external operation prove_goal is op RNAME { goals := build_goals; Results Success := prover Goals (value RName) ; IF Success THEN writescreen 'succeeded'; ELSE write 'failed'; ENDIF; write "Results; write Results; go := readscreen 'press return to continue '; }