X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=src%2Fast.ml;h=8e56fb5fbef44d981548d46dd5781d34fee63a6c;hb=54c8ad92025a9c77c2b10644499b3944e1299187;hp=b4f86e7b368a49c62b0d364eb457d21789bab5a3;hpb=84972c63d0dbc5a0da05ae08a5b99a9ad81baadc;p=goals.git

diff --git a/src/ast.ml b/src/ast.ml
index b4f86e7..8e56fb5 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -43,8 +43,9 @@ and pattern =
   | PTactic of loc * id * substs list
 and expr =
   | EGoalDefn of loc * goal
+  | EFuncDefn of loc * func
   | ETacticDefn of loc * tactic
-  | ECallGoal of loc * id * expr list
+  | ECall of loc * id * expr list
   | ETacticCtor of loc * id * expr list
   | EVar of loc * id
   | EList of loc * expr list
@@ -53,10 +54,12 @@ and expr =
 and constant =
   | CString of string
 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
@@ -80,6 +83,19 @@ let getgoal env loc name =
          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 =
@@ -134,6 +150,7 @@ and print_env fp env = output_string fp (string_env () env)
 and string_def () (name, expr) =
   match expr with
   | 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;
 
@@ -145,12 +162,25 @@ and string_goal () (name, (param_decls, patterns, exprs, code)) =
     (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 -> " = { ... }")
+    (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)) =
-  sprintf "tactic%s (%s) = { ... }"
+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
 
@@ -163,8 +193,9 @@ 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)
   | ETacticDefn (loc, goal) -> string_tactic () (None, goal)
-  | ECallGoal (loc, name, params) ->
+  | ECall (loc, name, params) ->
      sprintf "%s (%s)"
        name (String.concat ", " (List.map (string_expr ()) params))
   | ETacticCtor (loc, name, params) ->