open Lexing
open Printf
-module StringMap = Map.Make (String)
+module Env = Map.Make (String)
type loc = position * position
let noloc = dummy_pos, dummy_pos
let print_loc fp loc =
fprintf fp "%s" (string_loc () loc)
-type env = expr StringMap.t
+type env = expr Env.t
and pattern =
| PTactic of loc * id * substs list
| PVar of loc * id
) xs
let rec print_env fp env =
- StringMap.iter (print_def fp) env
+ Env.iter (print_def fp) env
and print_def fp name expr =
match expr with
* 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
*)
-module StringMap : sig
+module Env : sig
type key = string
type 'a t
val empty: 'a t
(** An environment is a set of variable and goal definitions, mapping
variable or goal name -> expression. *)
-type env = expr StringMap.t
+type env = expr Env.t
and pattern =
(** match tactic such as file ("filename") *)
| PTactic of loc * id * substs list
(* Call a goal. *)
| Ast.ECall (loc, name, args) ->
let expr =
- try Ast.StringMap.find name env
+ try Ast.Env.find name env
with Not_found ->
failwithf "%a: goal ‘%s’ not found" Ast.string_loc loc name in
let goal =
(* Look up the variable and substitute it. *)
| Ast.EVar (loc, name) ->
let expr =
- try Ast.StringMap.find name env
+ try Ast.Env.find name env
with Not_found ->
failwithf "%a: variable ‘%s’ not found" Ast.string_loc loc name in
evaluate_target env expr
and run_goal_for_tactic loc env tactic const_args =
(* Search across all goals for a matching tactic. *)
let goals =
- let env = Ast.StringMap.bindings env in
+ let env = Ast.Env.bindings env in
filter_map
(function (name, Ast.EGoal (loc, goal)) -> Some (name, goal) | _ -> None)
env in
failwithf "%a: calling goal ‘%s’ with wrong number of arguments"
Ast.string_loc loc name in
let env =
- List.fold_left (fun env (k, v) -> Ast.StringMap.add k v env)
+ List.fold_left (fun env (k, v) -> Ast.Env.add k v env)
env params in
(* Evaluate the dependencies first. *)
| Ast.EVar (loc, name) ->
let expr =
- try Ast.StringMap.find name env
+ try Ast.Env.find name env
with Not_found ->
failwithf "%a: variable ‘%s’ not found" Ast.string_loc loc name in
simplify env expr
| Ast.SString s -> Buffer.add_string b s
| Ast.SVar name ->
let expr =
- try Ast.StringMap.find name env
+ try Ast.Env.find name env
with Not_found ->
failwithf "%a: variable ‘%s’ not found" Ast.string_loc loc name in
match simplify env expr with