goals.git
4 years agoUpdate TODO.
Richard W.M. Jones [Tue, 7 Jan 2020 15:30:53 +0000 (15:30 +0000)]
Update TODO.

4 years agoeval: Split running external code according to return type.
Richard W.M. Jones [Tue, 7 Jan 2020 13:31:46 +0000 (13:31 +0000)]
eval: Split running external code according to return type.

Previously we were wrongly hiding stdout in some cases.

Fixes commit a48b05d35f0646322e8178ff10f8ed7af3e739aa
and commit 2ac1b84cb49ad04e27b4543436b0227153fbfb15.

4 years agoImplement pure functions.
Richard W.M. Jones [Tue, 7 Jan 2020 08:57:58 +0000 (08:57 +0000)]
Implement pure functions.

4 years agolexer: Use @{...} for quiet code sections.
Richard W.M. Jones [Mon, 6 Jan 2020 21:38:07 +0000 (21:38 +0000)]
lexer: Use @{...} for quiet code sections.

4 years agoparser: Fix parsing of patterns containing explicit tactic names.
Richard W.M. Jones [Mon, 6 Jan 2020 20:54:09 +0000 (20:54 +0000)]
parser: Fix parsing of patterns containing explicit tactic names.

4 years agoparser: Fix tracking of beginning of line for error messages.
Richard W.M. Jones [Mon, 6 Jan 2020 20:51:39 +0000 (20:51 +0000)]
parser: Fix tracking of beginning of line for error messages.

4 years agoCopy system environment into initial env, and also add %stdlib.
Richard W.M. Jones [Mon, 6 Jan 2020 12:53:15 +0000 (12:53 +0000)]
Copy system environment into initial env, and also add %stdlib.

4 years agoAllow functions "returning strings" (etc), redefine sort function.
Richard W.M. Jones [Mon, 6 Jan 2020 09:51:15 +0000 (09:51 +0000)]
Allow functions "returning strings" (etc), redefine sort function.

4 years agoStandardize running code in a single function, include prelude.sh.
Richard W.M. Jones [Sun, 5 Jan 2020 21:23:59 +0000 (21:23 +0000)]
Standardize running code in a single function, include prelude.sh.

4 years agoUpdate TODO
Richard W.M. Jones [Sun, 5 Jan 2020 21:09:45 +0000 (21:09 +0000)]
Update TODO

4 years agoFunctions return expressions instead of only lists of strings.
Richard W.M. Jones [Sun, 5 Jan 2020 13:10:43 +0000 (13:10 +0000)]
Functions return expressions instead of only lists of strings.

4 years agobuild: Create dependencies for Goalfile itself.
Richard W.M. Jones [Sat, 4 Jan 2020 12:02:24 +0000 (12:02 +0000)]
build: Create dependencies for Goalfile itself.

4 years agostdlib: Implement sort function.
Richard W.M. Jones [Sat, 4 Jan 2020 11:56:00 +0000 (11:56 +0000)]
stdlib: Implement sort function.

4 years agoUpdate TODO.
Richard W.M. Jones [Sat, 4 Jan 2020 11:48:22 +0000 (11:48 +0000)]
Update TODO.

4 years agobuild: Generate complete OCaml dependencies.
Richard W.M. Jones [Sat, 4 Jan 2020 09:49:21 +0000 (09:49 +0000)]
build: Generate complete OCaml dependencies.

Because we didn't use -I src on the ocamldep command line, ocamldep
didn't generate the complete set of dependencies.

4 years agoAst: Standard location for ocamldoc comments.
Richard W.M. Jones [Sat, 4 Jan 2020 09:41:52 +0000 (09:41 +0000)]
Ast: Standard location for ocamldoc comments.

4 years agostdlib: Implement wildcard function.
Richard W.M. Jones [Fri, 3 Jan 2020 21:45:34 +0000 (21:45 +0000)]
stdlib: Implement wildcard function.

4 years agoImplement functions.
Richard W.M. Jones [Fri, 3 Jan 2020 21:33:48 +0000 (21:33 +0000)]
Implement functions.

4 years agoAst: Remove functions which were moved to Eval module.
Richard W.M. Jones [Fri, 3 Jan 2020 21:10:16 +0000 (21:10 +0000)]
Ast: Remove functions which were moved to Eval module.

Updates commit f36210fd16a8e4e4d6ecdd8825bf8b8307943472.

4 years agobuild: Add depend goal and 'make depend'.
Richard W.M. Jones [Fri, 3 Jan 2020 19:26:13 +0000 (19:26 +0000)]
build: Add depend goal and 'make depend'.

4 years agobuild: Don't always pass -d to goals.
Richard W.M. Jones [Fri, 3 Jan 2020 19:24:24 +0000 (19:24 +0000)]
build: Don't always pass -d to goals.

We can enable debugging on a case-by-case basis when necessary.

4 years agobuild: Fix construction of parser.mli
Richard W.M. Jones [Fri, 3 Jan 2020 19:23:50 +0000 (19:23 +0000)]
build: Fix construction of parser.mli

4 years agobuild: Fix ocamldep invocation.
Richard W.M. Jones [Fri, 3 Jan 2020 19:19:01 +0000 (19:19 +0000)]
build: Fix ocamldep invocation.

4 years agobuild: Fix 'goals clean' rule.
Richard W.M. Jones [Fri, 3 Jan 2020 19:18:48 +0000 (19:18 +0000)]
build: Fix 'goals clean' rule.

4 years agostdlib: Fix *file tactic.
Richard W.M. Jones [Fri, 3 Jan 2020 19:07:11 +0000 (19:07 +0000)]
stdlib: Fix *file tactic.

Broken test if there is more than one dependency.

4 years agorun: Fix whitespace.
Richard W.M. Jones [Fri, 3 Jan 2020 19:07:07 +0000 (19:07 +0000)]
run: Fix whitespace.

4 years agorun: Better debugging and error messages for goals and tactics.
Richard W.M. Jones [Fri, 3 Jan 2020 18:49:31 +0000 (18:49 +0000)]
run: Better debugging and error messages for goals and tactics.

4 years agorun: If multiple goals match a tactic, at most one must have a CODE section.
Richard W.M. Jones [Fri, 3 Jan 2020 15:09:28 +0000 (15:09 +0000)]
run: If multiple goals match a tactic, at most one must have a CODE section.

This now works the same way as make.

4 years agoDon't default to echoing tactic command.
Richard W.M. Jones [Fri, 3 Jan 2020 15:12:02 +0000 (15:12 +0000)]
Don't default to echoing tactic command.

4 years agoUpdate TODO
Richard W.M. Jones [Fri, 3 Jan 2020 11:24:24 +0000 (11:24 +0000)]
Update TODO

4 years agoIn dependency file, use ; between statements.
Richard W.M. Jones [Fri, 3 Jan 2020 14:50:55 +0000 (14:50 +0000)]
In dependency file, use ; between statements.

So this parses correctly.

4 years agoparser: Optional semicolon between statements.
Richard W.M. Jones [Fri, 3 Jan 2020 14:48:54 +0000 (14:48 +0000)]
parser: Optional semicolon between statements.

4 years agoSimplify Constructor -> Ctor.
Richard W.M. Jones [Fri, 3 Jan 2020 11:35:56 +0000 (11:35 +0000)]
Simplify Constructor -> Ctor.

4 years agoRename Eval -> Run, split out some Ast functions into new Eval.
Richard W.M. Jones [Fri, 3 Jan 2020 11:33:31 +0000 (11:33 +0000)]
Rename Eval -> Run, split out some Ast functions into new Eval.

This gives us more consistent nomenclature:

  - "Run" for running targets.
  - "Eval" for simplifying and evaluating expressions, etc.
  - "Ast" is a library of AST-related structures.

4 years agoeval: Don't check target was rebuilt if there is no code.
Richard W.M. Jones [Fri, 3 Jan 2020 08:11:18 +0000 (08:11 +0000)]
eval: Don't check target was rebuilt if there is no code.

A pure dependency rule like:

  "foo.o": "foo.c"

doesn't contain any code, so it doesn't make sense to check if the
target has been rebuilt.

4 years agoUse goals itself exclusively to build.
Richard W.M. Jones [Mon, 30 Dec 2019 21:27:57 +0000 (21:27 +0000)]
Use goals itself exclusively to build.

4 years agoeval: Goals with no targets always need a rebuild.
Richard W.M. Jones [Fri, 3 Jan 2020 08:02:29 +0000 (08:02 +0000)]
eval: Goals with no targets always need a rebuild.

4 years agoeval: If multiple goals match a tactic, run them all.
Richard W.M. Jones [Fri, 3 Jan 2020 07:54:11 +0000 (07:54 +0000)]
eval: If multiple goals match a tactic, run them all.

4 years agolexer: Fix parsing of { characters in CODE sections.
Richard W.M. Jones [Fri, 3 Jan 2020 07:44:21 +0000 (07:44 +0000)]
lexer: Fix parsing of { characters in CODE sections.

4 years agoeval: Explicit function to evaluate goal arguments.
Richard W.M. Jones [Fri, 3 Jan 2020 07:44:00 +0000 (07:44 +0000)]
eval: Explicit function to evaluate goal arguments.

4 years agoRevert "eval: Expand goal args before running the goal."
Richard W.M. Jones [Fri, 3 Jan 2020 07:28:10 +0000 (07:28 +0000)]
Revert "eval: Expand goal args before running the goal."

This reverts commit 8509cad9b10205b7bec23eb59ba63e88c3d0fcb3.

4 years agoeval: Expand goal args before running the goal.
Richard W.M. Jones [Thu, 2 Jan 2020 16:11:39 +0000 (16:11 +0000)]
eval: Expand goal args before running the goal.

4 years agoLexer: Allow "-" char in the middle of identifier names.
Richard W.M. Jones [Thu, 2 Jan 2020 16:00:56 +0000 (16:00 +0000)]
Lexer: Allow "-" char in the middle of identifier names.

This allows eg maintainer-clean to be a goal name.

4 years agoAst: Rename ECallTactic to ETacticConstructor.
Richard W.M. Jones [Thu, 2 Jan 2020 15:59:48 +0000 (15:59 +0000)]
Ast: Rename ECallTactic to ETacticConstructor.

This is a constructor, it's not 'calling' anything.

4 years agoAst: Change EGoal -> EGoalDefn, ETactic -> ETacticDefn.
Richard W.M. Jones [Thu, 2 Jan 2020 15:57:48 +0000 (15:57 +0000)]
Ast: Change EGoal -> EGoalDefn, ETactic -> ETacticDefn.

4 years agoImplement -include (optional include) command.
Richard W.M. Jones [Mon, 30 Dec 2019 21:37:22 +0000 (21:37 +0000)]
Implement -include (optional include) command.

4 years agoFix ‘goal’ when it appears as a target (meaning ‘goal()’).
Richard W.M. Jones [Tue, 31 Dec 2019 09:08:35 +0000 (09:08 +0000)]
Fix ‘goal’ when it appears as a target (meaning ‘goal()’).

4 years agoMore TODO ideas.
Richard W.M. Jones [Tue, 31 Dec 2019 09:01:17 +0000 (09:01 +0000)]
More TODO ideas.

4 years agoAdd some more debugging.
Richard W.M. Jones [Tue, 31 Dec 2019 09:01:08 +0000 (09:01 +0000)]
Add some more debugging.

4 years agoImplement -d (debug) option.
Richard W.M. Jones [Mon, 30 Dec 2019 21:51:40 +0000 (21:51 +0000)]
Implement -d (debug) option.

4 years agoChange -V to -v for compat with make.
Richard W.M. Jones [Mon, 30 Dec 2019 21:41:17 +0000 (21:41 +0000)]
Change -V to -v for compat with make.

4 years agostdlib: Add some rules for OCaml code.
Richard W.M. Jones [Mon, 30 Dec 2019 21:27:20 +0000 (21:27 +0000)]
stdlib: Add some rules for OCaml code.

4 years agoImplement stdlib directory, -I, --no-prelude, etc.
Richard W.M. Jones [Sat, 28 Dec 2019 18:43:25 +0000 (18:43 +0000)]
Implement stdlib directory, -I, --no-prelude, etc.

4 years agoDefine OCaml Config module in ./configure, ./run script, --version option.
Richard W.M. Jones [Sat, 28 Dec 2019 19:54:50 +0000 (19:54 +0000)]
Define OCaml Config module in ./configure, ./run script, --version option.

4 years agoImplement tactics.
Richard W.M. Jones [Sat, 28 Dec 2019 16:28:41 +0000 (16:28 +0000)]
Implement tactics.

4 years agoRemove Ast.PVar.
Richard W.M. Jones [Sat, 28 Dec 2019 08:52:35 +0000 (08:52 +0000)]
Remove Ast.PVar.

Pure variables as patterns are disallowed.  Patterns have a distinct
type from expressions so allowing an expression to be substituted
causes complications.  In particular we want to know statically how
many targets a goal has, which is not possible if a variable can be
substituted here.

You can still write:

  "%name": ...

4 years agoRun code with set -e / set -x.
Richard W.M. Jones [Sat, 28 Dec 2019 08:50:19 +0000 (08:50 +0000)]
Run code with set -e / set -x.

4 years agoActually run goal code.
Richard W.M. Jones [Fri, 27 Dec 2019 20:26:43 +0000 (20:26 +0000)]
Actually run goal code.

4 years agoAdd implicit tactic rebuild.
Richard W.M. Jones [Fri, 27 Dec 2019 20:18:08 +0000 (20:18 +0000)]
Add implicit tactic rebuild.

We don't need to look for a goal covering every tactic, if the tactic
doesn't need rebuilding.

4 years agoSubstitute %<, %@ etc variables into code.
Richard W.M. Jones [Fri, 27 Dec 2019 19:47:16 +0000 (19:47 +0000)]
Substitute %<, %@ etc variables into code.

4 years agoAdd Ast.to_shell_script.
Richard W.M. Jones [Fri, 27 Dec 2019 19:56:19 +0000 (19:56 +0000)]
Add Ast.to_shell_script.

Previously we were confusing Ast.substitute with the place where we
need to shell quote.

4 years agoHard code *file tactic.
Richard W.M. Jones [Fri, 27 Dec 2019 19:05:03 +0000 (19:05 +0000)]
Hard code *file tactic.

4 years agoImplement tactic matching.
Richard W.M. Jones [Fri, 27 Dec 2019 14:45:00 +0000 (14:45 +0000)]
Implement tactic matching.

4 years agotodo: Note default parameters.
Richard W.M. Jones [Fri, 27 Dec 2019 13:37:55 +0000 (13:37 +0000)]
todo: Note default parameters.

4 years agoFactor out param_decl and improvements to AST printing.
Richard W.M. Jones [Thu, 26 Dec 2019 16:24:31 +0000 (16:24 +0000)]
Factor out param_decl and improvements to AST printing.

4 years agoRefactor evaluation.
Richard W.M. Jones [Tue, 24 Dec 2019 18:10:57 +0000 (18:10 +0000)]
Refactor evaluation.

Also more work on pattern matching and when to rebuild.

4 years agoFix file() -> *file() in comment about tactics.
Richard W.M. Jones [Wed, 25 Dec 2019 14:34:07 +0000 (14:34 +0000)]
Fix file() -> *file() in comment about tactics.

Updates commit b14ff66c953e6a73e9ac2fe8d42dd68e92e58f53.

4 years agoRename Ast.StringMap -> Ast.Env
Richard W.M. Jones [Wed, 25 Dec 2019 14:30:38 +0000 (14:30 +0000)]
Rename Ast.StringMap -> Ast.Env

4 years agoBegin converting Ast print functions so they can be used with format %a.
Richard W.M. Jones [Mon, 23 Dec 2019 20:44:01 +0000 (20:44 +0000)]
Begin converting Ast print functions so they can be used with format %a.

4 years agoSend debug message to stderr.
Richard W.M. Jones [Mon, 23 Dec 2019 20:43:08 +0000 (20:43 +0000)]
Send debug message to stderr.

4 years agoPrint errors (Failure exceptions) nicely.
Richard W.M. Jones [Mon, 23 Dec 2019 20:42:11 +0000 (20:42 +0000)]
Print errors (Failure exceptions) nicely.

4 years agoDefine *file() syntax for tactic constructors.
Richard W.M. Jones [Mon, 23 Dec 2019 19:08:14 +0000 (19:08 +0000)]
Define *file() syntax for tactic constructors.

Alternative syntaxes considered where ~file and &file.

4 years agoAttach parser location information to AST nodes.
Richard W.M. Jones [Mon, 23 Dec 2019 18:00:51 +0000 (18:00 +0000)]
Attach parser location information to AST nodes.

4 years agoBasic evaluation.
Richard W.M. Jones [Mon, 23 Dec 2019 11:48:41 +0000 (11:48 +0000)]
Basic evaluation.

4 years agoImplement -C / --directory option.
Richard W.M. Jones [Mon, 23 Dec 2019 11:53:09 +0000 (11:53 +0000)]
Implement -C / --directory option.

4 years agoAdd environment to store variables and goals.
Richard W.M. Jones [Mon, 23 Dec 2019 08:05:24 +0000 (08:05 +0000)]
Add environment to store variables and goals.

4 years agoCommand line parsing of anon args.
Richard W.M. Jones [Sun, 22 Dec 2019 18:17:06 +0000 (18:17 +0000)]
Command line parsing of anon args.

4 years agoExpose parsing of expressions from command line.
Richard W.M. Jones [Sun, 22 Dec 2019 16:59:59 +0000 (16:59 +0000)]
Expose parsing of expressions from command line.

4 years agoContinue command line parsing.
Richard W.M. Jones [Sat, 21 Dec 2019 20:46:46 +0000 (20:46 +0000)]
Continue command line parsing.

4 years agoRename parsing/ to src/
Richard W.M. Jones [Sat, 21 Dec 2019 17:01:52 +0000 (17:01 +0000)]
Rename parsing/ to src/

And some refactoring of the main code and command line parsing.

4 years agoInitial commit of parser.
Richard W.M. Jones [Thu, 19 Dec 2019 12:18:25 +0000 (12:18 +0000)]
Initial commit of parser.