New library to collect Prolog code manipuation

Request For Comments
#1

I’ve stared library(prolog_code) to collect predicates I’ve written 25 times to reason about Prolog code. Please comment on the naming and primitives in this library. The name of the library itself is also not ideal. All more recent libraries that are more intended to deal with the Prolog system than applications are named prolog_* and I wasn’t happy about meta, not reflexive and was out of ideas :frowning:

So, if you know about commonly used predicates for code manipulation that should belong here, you have a more conventional name or more conventional semantics, let me know.

The current file is at is on github

3 Likes
#2

The level at which the predicates interact with the data was so low that I did not look at the predicates as working with Prolog code but as looking at the arguments as either data structures used for logic analysis or parsing/pretty printing data structures used for logic analysis.

This reminded me a lot of the code from “Handbook of Practical Logic and Automated Reasoning” (WorldCat) by John Harrison, especially the foundation code.

Note: Code is written in OCaml

prop.ml - Basic stuff for propositional logic: datatype, parsing and printing.
   Of note is: Routine simplification.
formulas.ml - Polymorphic type of formulas with parser and printer.

The code constructively builds upon itself. Along the way is
unif.ml - Unification for first order terms.
resolution.ml - Resolution

and continues to build up to an interactive theorem prover.

The book can be used as an introduction to concepts for the HOL Light theorem prover, so for me code analysis and theorem proving have many touch points.

Anyway, may be of value, may not. :slightly_smiling_face:

#3

Thanks for the pointers

That is exactly the aim of this library. Whenever you try to reason about code or construct code on the fly there are a number of boring conversions that you need to do over and over again. Lots of these already appear in the core system to support the compiler as well as the various code analysis and macro expansion libraries. Most of the use cases use locally hacked up routines that are typically not really reusable. I’m about to write some more for automating tasks around tabling and decided to avoid writing the same boring stuff again and again :slight_smile:

1 Like