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": ...

diff --git a/src/ast.ml b/src/ast.ml
index c828bb0..9e5784b 100644 (file)
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -36,7 +36,6 @@ let print_loc fp loc =
 type env = expr Env.t
 and pattern =
   | PTactic of loc * id * substs list
-  | PVar of loc * id
 and expr =
   | EGoal of loc * goal
   | ECall of loc * id * expr list
@@ -208,8 +207,7 @@ and string_param_decl () name = name
 and string_pattern () = function
   | PTactic (loc, name, params) ->
      sprintf "*%s (%s)" name (String.concat ", "
-                                (List.map (string_substs ()) params));
-  | PVar (loc, id) -> id
+                                (List.map (string_substs ()) params))
 
 and print_pattern fp p = output_string fp (string_pattern () p)
 

diff --git a/src/ast.mli b/src/ast.mli
index 9bb2c9a..7a8e43f 100644 (file)
--- a/src/ast.mli
+++ b/src/ast.mli
@@ -40,9 +40,6 @@ type env = expr Env.t
 and pattern =
   (** match tactic such as *file ("filename") *)
   | PTactic of loc * id * substs list
-  (** match named variable, which must be a string, ETactic or
-      a list of those *)
-  | PVar of loc * id
 and expr =
   (** goal (params) = patterns : exprs = code *)
   | EGoal of loc * goal

diff --git a/src/eval.ml b/src/eval.ml
index 46455f7..af57213 100644 (file)
--- a/src/eval.ml
+++ b/src/eval.ml
@@ -85,8 +85,6 @@ and run_goal env loc name args (params, patterns, deps, code) =
         let expr_of_pattern = function
           | Ast.PTactic (loc, tactic, targs) ->
              Ast.ETactic (loc, tactic, List.map expr_of_substs targs)
-          | Ast.PVar (loc, name) ->
-             Ast.EVar (loc, name)
         in
         let pexprs = List.map expr_of_pattern patterns in
         let env = Ast.Env.add "@" (Ast.EList (Ast.noloc, pexprs)) env in
@@ -131,7 +129,6 @@ and needs_rebuild env loc deps pattern =
      assert (List.length targs = 1);
      let targ = List.hd targs in
      not (Sys.file_exists targ)
-  | Ast.PVar _ -> assert false (* XXX not implemented *)
 
 (* Find the goal which matches the given tactic and run it.
  * cargs is a list of parameters (all constants).
@@ -195,7 +192,6 @@ and run_tactic env loc tactic cargs =
  *)
 and matching_pattern env loc tactic cargs pattern params =
   match pattern with
-  | Ast.PVar (loc, name) -> assert false (* TODO! *)
   | Ast.PTactic (loc, ttactic, targs)
        when tactic <> ttactic ||
             List.length cargs <> List.length targs ->

diff --git a/src/parser.mly b/src/parser.mly
index c47ac59..f058044 100644 (file)
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -86,7 +86,6 @@ patterns:
 pattern:
     | STRING     { Ast.PTactic ($loc, "file", [$1]) }
     | ID pattern_params { Ast.PTactic ($loc, $1, $2) }
-    | ID         { Ast.PVar ($loc, $1) }
     ;
 pattern_params:
     | LEFT_PAREN separated_list(COMMA, pattern_param) RIGHT_PAREN { $2 }