X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;ds=sidebyside;f=src%2Fast.ml;h=ec34956700a6cb13fb6e2d40a338d52a363334f3;hb=refs%2Fheads%2Fmaster;hp=5b31c0ddd9e5bf5f558fa05918be8c937ef18d3b;hpb=98a2cfdd3bdf5641e268e7db7c7ea2d23656b296;p=goals.git

diff --git a/src/ast.ml b/src/ast.ml
index 5b31c0d..ec34956 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -17,31 +17,99 @@
  * 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
+  | PPred 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
+  | EGoalDefn of loc * goal
+  | EFuncDefn of loc * func
+  | EPredDefn of loc * pred
+  | ECall of loc * id * expr list
+  | EPredCtor 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 func = param_decl list * returning * bool * code
+and pred = param_decl list * code
+and param_decl = id
 and id = string
-and code = substs
+and code = substs * bool
+and returning = RetExpr | RetStrings | RetString
 and substs = subst list
 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
+    | EGoalDefn (loc, goal) -> goal
+    | _ ->
+       failwithf "%a: tried to call ‘%s’ which is not a goal"
+         string_loc loc name in
+  goal
+
+let getfunc env loc name =
+  let expr =
+    try Env.find name env
+    with Not_found ->
+      failwithf "%a: func ‘%s’ not found" string_loc loc name in
+  let func =
+    match expr with
+    | EFuncDefn (loc, func) -> func
+    | _ ->
+       failwithf "%a: tried to call ‘%s’ which is not a function"
+         string_loc loc name in
+  func
+
+let getpred env loc name =
+  assert (String.length name >= 3 && String.sub name 0 3 = "is-");
+  let expr =
+    try Env.find name env
+    with Not_found ->
+      failwithf "%a: predicate ‘%s’ not found" string_loc loc name in
+  let pred =
+    match expr with
+    | EPredDefn (loc, pred) -> pred
+    | _ ->
+       failwithf "%a: tried to call ‘%s’ which is not a predicate"
+         string_loc loc name in
+  pred
+
 module Substs = struct
   type t = {
       mutable elems : subst list; (* built in reverse order *)
@@ -73,64 +141,91 @@ 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
+  | EGoalDefn (loc, goal) -> string_goal () (Some name, goal) ^ "\n"
+  | EFuncDefn (loc, func) -> string_func () (Some name, func) ^ "\n"
+  | EPredDefn (loc, pred) -> string_pred () (Some name, pred) ^ "\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, false) -> " = { ... }"
+                   | Some (code, true) -> " = @{ ... }")
+
+and string_func () (name, (param_decls, returning, pure, (code, quiet))) =
+  sprintf "%sfunction%s returning %s (%s) = %s{ ... }"
+    (if pure then "pure " else "")
+    (match name with None -> "" | Some name -> " " ^ name)
+    (match returning with RetExpr -> "expression"
+                        | RetString -> "string"
+                        | RetStrings -> "strings")
+    (String.concat ", " (List.map (string_param_decl ()) param_decls))
+    (if quiet then "@" else "")
+
+and string_pred () (name, (param_decls, (code, quiet))) =
+  sprintf "predicate%s (%s) = %s{ ... }"
+    (match name with None -> "" | Some name -> " " ^ name)
+    (String.concat ", " (List.map (string_param_decl ()) param_decls))
+    (if quiet then "@" else "")
+
+and string_param_decl () name = name
+
+and string_pattern () = function
+  | PPred (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
+  | EGoalDefn (loc, goal) -> string_goal () (None, goal)
+  | EFuncDefn (loc, func) -> string_func () (None, func)
+  | EPredDefn (loc, goal) -> string_pred () (None, goal)
+  | ECall (loc, name, params) ->
+     sprintf "%s (%s)"
+       name (String.concat ", " (List.map (string_expr ()) params))
+  | EPredCtor (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 (