open Lexing
open Printf
-module StringMap = Map.Make (String)
+open Utils
+
+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
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
and expr =
| EGoal of loc * goal
- | ECall of loc * id * expr list
+ | ETactic of loc * tactic
+ | ECallGoal of loc * id * expr list
+ | ECallTactic of loc * id * expr list
| EVar of loc * id
| EList of loc * expr list
| ESubsts of loc * substs
| EConstant of loc * constant
and constant =
| CString of string
-and goal = id list * pattern list * expr list * code option
+and goal = param_decl list * pattern list * expr list * code option
+and tactic = param_decl list * code
+and param_decl = id
and id = string
and code = substs
and substs = subst list
| SString of string
| SVar of id
+let getvar env loc name =
+ try Env.find name env
+ with Not_found ->
+ failwithf "%a: variable ‘%s’ not found" string_loc loc name
+
+let getgoal env loc name =
+ let expr =
+ try Env.find name env
+ with Not_found ->
+ failwithf "%a: goal ‘%s’ not found" string_loc loc name in
+ let goal =
+ match expr with
+ | EGoal (loc, goal) -> goal
+ | _ ->
+ failwithf "%a: tried to call ‘%s’ which is not a goal"
+ string_loc loc name in
+ goal
+
+let gettactic env loc name =
+ assert (name.[0] = '*');
+ let expr =
+ try Env.find name env
+ with Not_found ->
+ failwithf "%a: tactic ‘%s’ not found" string_loc loc name in
+ let tactic =
+ match expr with
+ | ETactic (loc, tactic) -> tactic
+ | _ ->
+ failwithf "%a: tried to call ‘%s’ which is not a tactic"
+ string_loc loc name in
+ tactic
+
+let rec to_constant env = function
+ | EConstant (loc, c) -> c
+
+ | EVar (loc, name) ->
+ let expr = getvar env loc name in
+ to_constant env expr
+
+ | ESubsts (loc, str) ->
+ CString (substitute env loc str)
+
+ | EList (loc, _) ->
+ failwithf "%a: list found where constant expression expected"
+ string_loc loc
+
+ | ECallGoal (loc, name, _) ->
+ failwithf "%a: cannot use goal ‘%s’ in constant expression"
+ string_loc loc name
+
+ | ECallTactic (loc, name, _) ->
+ failwithf "%a: cannot use tactic ‘%s’ in constant expression"
+ string_loc loc name
+
+ | EGoal (loc, _) ->
+ failwithf "%a: cannot use goal in constant expression"
+ string_loc loc
+
+ | ETactic (loc, _) ->
+ failwithf "%a: cannot use tactic in constant expression"
+ string_loc loc
+
+and substitute env loc substs =
+ let b = Buffer.create 13 in
+ List.iter (
+ function
+ | SString s -> Buffer.add_string b s
+ | SVar name ->
+ let expr = getvar env loc name in
+ match to_constant env expr with
+ | CString s -> Buffer.add_string b s
+ ) substs;
+ Buffer.contents b
+
+let rec to_shell_script env loc substs =
+ let b = Buffer.create 13 in
+ List.iter (
+ function
+ | SString s -> Buffer.add_string b s
+ | SVar name ->
+ let expr = getvar env loc name in
+ let s = expr_to_shell_string env expr in
+ Buffer.add_string b s
+ ) substs;
+ Buffer.contents b
+
+and expr_to_shell_string env = function
+ | EConstant (loc, CString s) -> Filename.quote s
+
+ | EVar (loc, name) ->
+ let expr = getvar env loc name in
+ expr_to_shell_string env expr
+
+ | ESubsts (loc, str) ->
+ Filename.quote (substitute env loc str)
+
+ | EList (loc, exprs) ->
+ let strs = List.map (expr_to_shell_string env) exprs in
+ (* These are shell quoted so we can just concat them with space. *)
+ String.concat " " strs
+
+ | ECallGoal (loc, name, _) ->
+ failwithf "%a: cannot use goal ‘%s’ in shell expansion"
+ string_loc loc name
+
+ (* Tactics expand to the first parameter. *)
+ | ECallTactic (loc, _, []) -> Filename.quote ""
+ | ECallTactic (loc, _, (arg :: _)) -> expr_to_shell_string env arg
+
+ | EGoal (loc, _) ->
+ failwithf "%a: cannot use goal in shell expansion"
+ string_loc loc
+
+ | ETactic (loc, _) ->
+ failwithf "%a: cannot use tactic in shell expansion"
+ string_loc loc
+
module Substs = struct
type t = {
mutable elems : subst list; (* built in reverse order *)
f fp x
) xs
-let rec print_env fp env =
- StringMap.iter (print_def fp) env
+let rec string_env () env =
+ let env = Env.bindings env in
+ String.concat "" (List.map (string_def ()) env)
-and print_def fp name expr =
+and print_env fp env = output_string fp (string_env () env)
+
+and string_def () (name, expr) =
match expr with
- | EGoal (loc, (params, patterns, exprs, code)) ->
- fprintf fp "goal %s (%s) =\n" name (String.concat ", " params);
- fprintf fp " ";
- iter_with_commas fp print_pattern patterns;
- fprintf fp " : ";
- iter_with_commas fp print_expr exprs;
- (match code with
- | None -> ()
- | Some code ->
- fprintf fp " {\n";
- print_code fp code;
- fprintf fp "\n }"
- );
- fprintf fp "\n"
- | expr ->
- fprintf fp "let %s = " name;
- print_expr fp expr;
- fprintf fp "\n"
-
-and print_pattern fp = function
+ | EGoal (loc, goal) -> string_goal () (Some name, goal) ^ "\n"
+ | ETactic (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))
+
+and string_goal () (name, (param_decls, patterns, exprs, code)) =
+ sprintf "goal%s (%s) = %s : %s%s"
+ (match name with None -> "" | Some name -> " " ^ name)
+ (String.concat ", " (List.map (string_param_decl ()) param_decls))
+ (String.concat ", " (List.map (string_pattern ()) patterns))
+ (String.concat ", " (List.map (string_expr ()) exprs))
+ (match code with None -> "" | Some code -> " = { ... }")
+
+and string_tactic () (name, (param_decls, code)) =
+ sprintf "tactic%s (%s) = { ... }"
+ (match name with None -> "" | Some name -> " " ^ name)
+ (String.concat ", " (List.map (string_param_decl ()) param_decls))
+
+and string_param_decl () name = name
+
+and string_pattern () = function
| PTactic (loc, name, params) ->
- fprintf fp "%s (" name;
- iter_with_commas fp print_substs params;
- fprintf fp ")"
- | PVar (loc, id) -> print_id fp id
-
-and print_expr fp = function
- | EGoal _ -> assert false (* printed above *)
- | ECall (loc, name, params) ->
- fprintf fp "%s (" name;
- iter_with_commas fp print_expr params;
- fprintf fp ")"
- | EVar (loc, var) -> print_id fp var
+ sprintf "%s (%s)" name (String.concat ", "
+ (List.map (string_substs ()) params))
+
+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)
+ | ECallGoal (loc, name, params) ->
+ sprintf "%s (%s)"
+ name (String.concat ", " (List.map (string_expr ()) params))
+ | ECallTactic (loc, name, params) ->
+ sprintf "%s (%s)"
+ name (String.concat ", " (List.map (string_expr ()) params))
+ | EVar (loc, var) -> var
| EList (loc, xs) ->
- fprintf fp "[";
- iter_with_commas fp print_expr xs;
- fprintf fp "]"
- | ESubsts (loc, s) -> print_substs fp s
- | EConstant (loc, c) -> print_constant fp c
+ sprintf "[%s]" (String.concat ", " (List.map (string_expr ()) xs))
+ | ESubsts (loc, s) -> string_substs () s
+ | EConstant (loc, c) -> string_constant () c
+
+and print_expr fp expr = output_string fp (string_expr () expr)
-and print_constant fp = function
- | CString s -> fprintf fp "%S" s
+and string_constant () = function
+ | CString s -> sprintf "%S" s
+
+and print_constant fp c = output_string fp (string_constant () c)
and print_id = output_string
-and print_substs fp xs =
- let xs =
+and string_substs () ss =
+ let ss =
List.map (
function
| SString s -> sprintf "%S" s
| SVar id -> id
- ) xs in
- fprintf fp "%s" (String.concat "+" xs)
+ ) ss in
+ (String.concat "+" ss)
+
+and print_substs fp ss = output_string fp (string_substs () ss)
and print_code fp xs =
List.iter (
git.annexia.org / goals.git / blobdiff