Ast: Change EGoal -> EGoalDefn, ETactic -> ETacticDefn.

diff --git a/src/ast.ml b/src/ast.ml
index 587c888..1f67413 100644 (file)
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -42,8 +42,8 @@ type env = expr Env.t
 and pattern =
   | PTactic of loc * id * substs list
 and expr =
-  | EGoal of loc * goal
-  | ETactic of loc * tactic
+  | EGoalDefn of loc * goal
+  | ETacticDefn of loc * tactic
   | ECallGoal of loc * id * expr list
   | ECallTactic of loc * id * expr list
   | EVar of loc * id
@@ -74,7 +74,7 @@ let getgoal env loc name =
       failwithf "%a: goal ‘%s’ not found" string_loc loc name in
   let goal =
     match expr with
-    | EGoal (loc, goal) -> goal
+    | EGoalDefn (loc, goal) -> goal
     | _ ->
        failwithf "%a: tried to call ‘%s’ which is not a goal"
          string_loc loc name in
@@ -88,7 +88,7 @@ let gettactic env loc name =
       failwithf "%a: tactic ‘%s’ not found" string_loc loc name in
   let tactic =
     match expr with
-    | ETactic (loc, tactic) -> tactic
+    | ETacticDefn (loc, tactic) -> tactic
     | _ ->
        failwithf "%a: tried to call ‘%s’ which is not a tactic"
          string_loc loc name in
@@ -116,11 +116,11 @@ let rec to_constant env = function
      failwithf "%a: cannot use tactic ‘%s’ in constant expression"
        string_loc loc name
 
-  | EGoal (loc, _) ->
+  | EGoalDefn (loc, _) ->
      failwithf "%a: cannot use goal in constant expression"
        string_loc loc
 
-  | ETactic (loc, _) ->
+  | ETacticDefn (loc, _) ->
      failwithf "%a: cannot use tactic in constant expression"
        string_loc loc
 
@@ -171,11 +171,11 @@ and expr_to_shell_string env = function
   | ECallTactic (loc, _, []) -> Filename.quote ""
   | ECallTactic (loc, _, (arg :: _)) -> expr_to_shell_string env arg
 
-  | EGoal (loc, _) ->
+  | EGoalDefn (loc, _) ->
      failwithf "%a: cannot use goal in shell expansion"
        string_loc loc
 
-  | ETactic (loc, _) ->
+  | ETacticDefn (loc, _) ->
      failwithf "%a: cannot use tactic in shell expansion"
        string_loc loc
 
@@ -218,8 +218,8 @@ and print_env fp env = output_string fp (string_env () env)
 
 and string_def () (name, expr) =
   match expr with
-  | EGoal (loc, goal) -> string_goal () (Some name, goal) ^ "\n"
-  | ETactic (loc, tactic) -> string_tactic () (Some name, tactic) ^ "\n"
+  | EGoalDefn (loc, goal) -> string_goal () (Some name, goal) ^ "\n"
+  | ETacticDefn (loc, tactic) -> string_tactic () (Some name, tactic) ^ "\n"
   | expr -> sprintf "let %s = %a\n" name string_expr expr;
 
 and print_def fp name expr = output_string fp (string_def () (name, expr))
@@ -247,8 +247,8 @@ and string_pattern () = function
 and print_pattern fp p = output_string fp (string_pattern () p)
 
 and string_expr () = function
-  | EGoal (loc, goal) -> string_goal () (None, goal)
-  | ETactic (loc, goal) -> string_tactic () (None, goal)
+  | EGoalDefn (loc, goal) -> string_goal () (None, goal)
+  | ETacticDefn (loc, goal) -> string_tactic () (None, goal)
   | ECallGoal (loc, name, params) ->
      sprintf "%s (%s)"
        name (String.concat ", " (List.map (string_expr ()) params))

diff --git a/src/ast.mli b/src/ast.mli
index 831878d..1fee78e 100644 (file)
--- a/src/ast.mli
+++ b/src/ast.mli
@@ -45,9 +45,9 @@ and pattern =
   | PTactic of loc * id * substs list
 and expr =
   (** goal (params) = patterns : exprs code *)
-  | EGoal of loc * goal
+  | EGoalDefn of loc * goal
   (** tactic (params) = code *)
-  | ETactic of loc * tactic
+  | ETacticDefn of loc * tactic
   (** call goalname (params) etc. *)
   | ECallGoal of loc * id * expr list
   (** call *tactic (params) etc. *)

diff --git a/src/eval.ml b/src/eval.ml
index 1688b5f..770acf1 100644 (file)
--- a/src/eval.ml
+++ b/src/eval.ml
@@ -25,7 +25,7 @@ let rec evaluate_targets env exprs =
   List.iter (evaluate_target env) exprs
 
 and evaluate_target env = function
-  | Ast.EGoal _ | Ast.ETactic _ -> assert false
+  | Ast.EGoalDefn _ | Ast.ETacticDefn _ -> assert false
 
   (* Call a goal. *)
   | Ast.ECallGoal (loc, name, args) ->
@@ -46,9 +46,9 @@ and evaluate_target env = function
   | Ast.EVar (loc, name) ->
      let expr = Ast.getvar env loc name in
      (match expr with
-      | EGoal (loc, ([], _, _, _)) ->
+      | EGoalDefn (loc, ([], _, _, _)) ->
          evaluate_target env (Ast.ECallGoal (loc, name, []))
-      | EGoal _ ->
+      | EGoalDefn _ ->
          failwithf "%a: cannot call %s() since this goal has parameters"
            Ast.string_loc loc name
       | _ ->
@@ -186,7 +186,7 @@ and run_tactic env loc tactic cargs =
     let env = Ast.Env.bindings env in
     filter_map
       (function
-       | name, Ast.EGoal (loc, goal) -> Some (name, goal)
+       | name, Ast.EGoalDefn (loc, goal) -> Some (name, goal)
        | _ -> None) env in
 
   (* Find all patterns.  Returns a list of (pattern, name, goal). *)

diff --git a/src/parser.mly b/src/parser.mly
index e45e90b..6cb48f7 100644 (file)
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -99,16 +99,16 @@ stmt:
         | None ->
            sprintf "_goal@%d" $startpos.pos_lnum, []
         | Some x -> x in
-      name, Ast.EGoal ($loc, (params, $2, $4, $5))
+      name, Ast.EGoalDefn ($loc, (params, $2, $4, $5))
     }
     | goal_stmt CODE
     {
       let name, params = $1 in
-      name, Ast.EGoal ($loc, (params, [], [], Some $2))
+      name, Ast.EGoalDefn ($loc, (params, [], [], Some $2))
     }
     | TACTIC_KEYWORD TACTIC params_decl EQUALS CODE
     {
-      $2, Ast.ETactic ($loc, ($3, $5))
+      $2, Ast.ETacticDefn ($loc, ($3, $5))
     }
     | LET ID EQUALS expr { $2, $4 }
     ;