From b14ff66c953e6a73e9ac2fe8d42dd68e92e58f53 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Mon, 23 Dec 2019 19:08:14 +0000 Subject: [PATCH] Define *file() syntax for tactic constructors. Alternative syntaxes considered where ~file and &file. --- src/ast.ml | 7 ++++++- src/ast.mli | 6 ++++-- src/eval.ml | 31 ++++++++++++++----------------- src/lexer.mll | 3 +++ src/parser.mly | 4 +++- tests/test1.gl | 2 +- 6 files changed, 31 insertions(+), 22 deletions(-) diff --git a/src/ast.ml b/src/ast.ml index 6a7823c..885eefe 100644 --- a/src/ast.ml +++ b/src/ast.ml @@ -38,6 +38,7 @@ and pattern = and expr = | EGoal of loc * goal | ECall of loc * id * expr list + | ETactic of loc * id * expr list | EVar of loc * id | EList of loc * expr list | ESubsts of loc * substs @@ -109,7 +110,7 @@ and print_def fp name expr = and print_pattern fp = function | PTactic (loc, name, params) -> - fprintf fp "%s (" name; + fprintf fp "*%s (" name; iter_with_commas fp print_substs params; fprintf fp ")" | PVar (loc, id) -> print_id fp id @@ -120,6 +121,10 @@ and print_expr fp = function fprintf fp "%s (" name; iter_with_commas fp print_expr params; fprintf fp ")" + | ETactic (loc, name, params) -> + fprintf fp "*%s (" name; + iter_with_commas fp print_expr params; + fprintf fp ")" | EVar (loc, var) -> print_id fp var | EList (loc, xs) -> fprintf fp "["; diff --git a/src/ast.mli b/src/ast.mli index 4162eb3..c7e3be4 100644 --- a/src/ast.mli +++ b/src/ast.mli @@ -45,9 +45,11 @@ and pattern = and expr = (** goal (params) = patterns : exprs = code *) | EGoal of loc * goal - (** goalname (params), tactic (params) etc. *) + (** goalname (params) etc. *) | ECall of loc * id * expr list - (** variable *) + (** *tactic (params) etc. *) + | ETactic of loc * id * expr list + (** variable, or goal call with no parameters *) | EVar of loc * id (** list *) | EList of loc * expr list diff --git a/src/eval.ml b/src/eval.ml index 779cb5d..e928564 100644 --- a/src/eval.ml +++ b/src/eval.ml @@ -25,21 +25,7 @@ let rec evaluate_targets env exprs = and evaluate_target env = function | Ast.EGoal _ -> assert false - (* This could be an instruction to call a goal, or it - * could be a tactic. - *) - | Ast.ECall (loc, "file", [filename]) (* XXX define tactics! *) -> - (* All parameters of tactics must be simple expressions (strings, - * in future booleans, numbers, etc). - *) - let args = [filename] in - let args = List.map (simplify env) args in - run_goal_for_tactic loc env "file" args - - | Ast.ECall (loc, "file", _) -> - failwithf "%a: file tactic called with wrong number of parameters" - Ast.string_loc loc - + (* Call a goal. *) | Ast.ECall (loc, name, args) -> let expr = try Ast.StringMap.find name env @@ -53,6 +39,13 @@ and evaluate_target env = function Ast.string_loc loc name in run_goal loc env name args goal + | Ast.ETactic (loc, name, args) -> + (* All parameters of tactics must be simple expressions (strings, + * in future booleans, numbers, etc). + *) + let args = List.map (simplify env) args in + run_goal_for_tactic loc env name args + (* Look up the variable and substitute it. *) | Ast.EVar (loc, name) -> let expr = @@ -65,7 +58,7 @@ and evaluate_target env = function | Ast.EList (loc, exprs) -> evaluate_targets env exprs - (* A string (with or without substitutions) implies file (filename). *) + (* A string (with or without substitutions) implies *file(filename). *) | Ast.ESubsts (loc, str) -> let str = substitute loc env str in run_goal_for_tactic loc env "file" [Ast.CString str] @@ -181,7 +174,11 @@ and simplify env = function Ast.string_loc loc | Ast.ECall (loc, name, _) -> - failwithf "%a: cannot use goal or tactic ‘%s’ in constant expression" + failwithf "%a: cannot use goal ‘%s’ in constant expression" + Ast.string_loc loc name + + | Ast.ETactic (loc, name, _) -> + failwithf "%a: cannot use tactic ‘*%s’ in constant expression" Ast.string_loc loc name | Ast.EGoal (loc, _) -> diff --git a/src/lexer.mll b/src/lexer.mll index d0f4a1d..a9b11d1 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -52,6 +52,9 @@ rule read = | "{" { read_code (Ast.Substs.create ()) (ref 1) lexbuf } | "goal" { GOAL } | "let" { LET } + | "*" id { let id = Lexing.lexeme lexbuf in + let len = String.length id in + TACTIC (String.sub id 1 (len-1)) } | id { ID (Lexing.lexeme lexbuf) } | _ { raise (SyntaxError ("unexpected character: " ^ Lexing.lexeme lexbuf)) } diff --git a/src/parser.mly b/src/parser.mly index 69cb063..3531b08 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -25,16 +25,17 @@ open Printf %token CODE %token COLON %token COMMA -%token ID %token EQUALS %token EOF %token GOAL +%token ID %token LEFT_ARRAY %token LEFT_PAREN %token LET %token RIGHT_ARRAY %token RIGHT_PAREN %token STRING +%token TACTIC (* Start nonterminals. *) %start file @@ -95,6 +96,7 @@ pattern_param: expr: | ID params { Ast.ECall ($loc, $1, $2) } | ID { Ast.EVar ($loc, $1) } + | TACTIC params { Ast.ETactic ($loc, $1, $2) } | STRING { Ast.ESubsts ($loc, $1) } | LEFT_ARRAY barelist RIGHT_ARRAY { Ast.EList ($loc, $2) } ; diff --git a/tests/test1.gl b/tests/test1.gl index fc059d0..afdcc34 100644 --- a/tests/test1.gl +++ b/tests/test1.gl @@ -1,6 +1,6 @@ # Test. -goal all = : ["file1.o", "file2.o"] +goal all = : "file1.o", *file("file2.o") "file1.o" : "file1.c" { echo file1.c "->" file1.o -- 1.8.3.1