X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=src%2Fast.ml;h=8e56fb5fbef44d981548d46dd5781d34fee63a6c;hb=bed4036653ce47a91b96dd0ead65341aa80d6b97;hp=819e9ee254f402ba17166342a3537f1408fb6533;hpb=70be8e48106b13883da29574e7735ca85d8192cc;p=goals.git

diff --git a/src/ast.ml b/src/ast.ml
index 819e9ee..8e56fb5 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -20,7 +20,14 @@
 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
@@ -31,28 +38,78 @@ let string_loc () loc =
 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
+  | EGoalDefn of loc * goal
+  | EFuncDefn of loc * func
+  | ETacticDefn of loc * tactic
   | ECall of loc * id * expr list
-  | ETactic of loc * id * expr list
+  | ETacticCtor 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 tactic = 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 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
+    | ETacticDefn (loc, tactic) -> tactic
+    | _ ->
+       failwithf "%a: tried to call ‘%s’ which is not a tactic"
+         string_loc loc name in
+  tactic
+
 module Substs = struct
   type t = {
       mutable elems : subst list; (* built in reverse order *)
@@ -84,58 +141,78 @@ 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 (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"
+  | EGoalDefn (loc, goal) -> string_goal () (Some name, goal) ^ "\n"
+  | EFuncDefn (loc, func) -> string_func () (Some name, func) ^ "\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))
+
+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_tactic () (name, (param_decls, (code, quiet))) =
+  sprintf "tactic%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
   | PTactic (loc, name, params) ->
-     sprintf "*%s (%s)" name (String.concat ", "
-                                (List.map (string_substs ()) params));
-  | PVar (loc, id) -> id
+     sprintf "%s (%s)" name (String.concat ", "
+                                (List.map (string_substs ()) params))
 
 and print_pattern fp p = output_string fp (string_pattern () p)
 
-and print_expr fp = function
-  | EGoal _ -> assert false (* printed above *)
+and string_expr () = function
+  | EGoalDefn (loc, goal) -> string_goal () (None, goal)
+  | EFuncDefn (loc, func) -> string_func () (None, func)
+  | ETacticDefn (loc, goal) -> string_tactic () (None, goal)
   | ECall (loc, name, params) ->
-     fprintf fp "%s (" name;
-     iter_with_commas fp print_expr params;
-     fprintf fp ")"
-  | ETactic (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_expr ()) params))
+  | ETacticCtor (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
-
-and print_constant fp = function
-  | CString s -> fprintf fp "%S" s
+     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