X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=src%2Fast.ml;h=587c888660980d622f867294c89dc5c88d2f9d08;hb=7b7cd85810f18286a36215cc164b659bf7db142c;hp=5b31c0ddd9e5bf5f558fa05918be8c937ef18d3b;hpb=98a2cfdd3bdf5641e268e7db7c7ea2d23656b296;p=goals.git

diff --git a/src/ast.ml b/src/ast.ml
index 5b31c0d..587c888 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -17,24 +17,44 @@
  * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
  *)
 
+open Lexing
 open Printf
 
-module StringMap = Map.Make (String)
+open Utils
 
-type env = expr StringMap.t
+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 string_loc () loc =
+  let pos = fst loc in
+  sprintf "%s:%d:%d" pos.pos_fname pos.pos_lnum (pos.pos_cnum - pos.pos_bol)
+let print_loc fp loc =
+  fprintf fp "%s" (string_loc () loc)
+
+type env = expr Env.t
 and pattern =
-  | PTactic of id * substs list
-  | PVar of id
+  | PTactic of loc * id * substs list
 and expr =
-  | EGoal of goal
-  | ECall of id * expr list
-  | EVar of id
-  | EList of expr list
-  | ESubsts of substs
-  | EConstant of constant
+  | EGoal of loc * goal
+  | 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
@@ -42,6 +62,123 @@ and subst =
   | 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 *)
@@ -73,64 +210,76 @@ let iter_with_commas
       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 (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
-  | PTactic (name, params) ->
-     fprintf fp "%s (" name;
-     iter_with_commas fp print_substs params;
-     fprintf fp ")"
-  | PVar id -> print_id fp id
-
-and print_expr fp = function
-  | EGoal _ -> assert false (* printed above *)
-  | ECall (name, params) ->
-     fprintf fp "%s (" name;
-     iter_with_commas fp print_expr params;
-     fprintf fp ")"
-  | EVar var -> print_id fp var
-  | EList xs ->
-     fprintf fp "[";
-     iter_with_commas fp print_expr xs;
-     fprintf fp "]"
-  | ESubsts s -> print_substs fp s
-  | EConstant c -> print_constant fp c
-
-and print_constant fp = function
-  | CString s -> fprintf fp "%S" s
+  | 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) ->
+     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) ->
+     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 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 (