X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=src%2Fast.ml;h=c3b3969f6c3eb69c4ab96e70aec063941baf2d51;hb=3ed50d510dbab127125a8af9f72554c2dec72ef5;hp=9f3326afc80ab59d3c888acff3dbbce23925b242;hpb=214f84c3b07227767fef90934895a167b15113a1;p=goals.git

diff --git a/src/ast.ml b/src/ast.ml
index 9f3326a..c3b3969 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -22,7 +22,12 @@ open Printf
 
 open Utils
 
-module Env = Map.Make (String)
+module Env = struct
+  include Map.Make (String)
+
+  let merge env env' =
+    List.fold_left (fun env (k, v) -> add k v env) env (bindings env')
+end
 
 type loc = position * position
 let noloc = dummy_pos, dummy_pos
@@ -37,10 +42,10 @@ 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
+  | ETacticCtor of loc * id * expr list
   | EVar of loc * id
   | EList of loc * expr list
   | ESubsts of loc * substs
@@ -69,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
@@ -83,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
@@ -107,15 +112,15 @@ let rec to_constant env = function
      failwithf "%a: cannot use goal ‘%s’ in constant expression"
        string_loc loc name
 
-  | ECallTactic (loc, name, _) ->
+  | ETacticCtor (loc, name, _) ->
      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
 
@@ -163,14 +168,14 @@ and expr_to_shell_string env = function
        string_loc loc name
 
   (* Tactics expand to the first parameter. *)
-  | ECallTactic (loc, _, []) -> Filename.quote ""
-  | ECallTactic (loc, _, (arg :: _)) -> expr_to_shell_string env arg
+  | ETacticCtor (loc, _, []) -> Filename.quote ""
+  | ETacticCtor (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
 
@@ -213,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))
@@ -242,12 +247,12 @@ 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))
-  | ECallTactic (loc, name, params) ->
+  | ETacticCtor (loc, name, params) ->
      sprintf "%s (%s)"
        name (String.concat ", " (List.map (string_expr ()) params))
   | EVar (loc, var) -> var