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

diff --git a/src/ast.ml b/src/ast.ml
index 587c888..8e56fb5 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -42,10 +42,11 @@ type env = expr Env.t
 and pattern =
   | PTactic of loc * id * substs list
 and expr =
-  | EGoal of loc * goal
-  | ETactic of loc * tactic
-  | ECallGoal of loc * id * expr list
-  | ECallTactic of loc * id * expr list
+  | EGoalDefn of loc * goal
+  | EFuncDefn of loc * func
+  | ETacticDefn of loc * tactic
+  | ECall of loc * id * expr list
+  | ETacticCtor of loc * id * expr list
   | EVar of loc * id
   | EList of loc * expr list
   | ESubsts of loc * substs
@@ -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
@@ -74,12 +77,25 @@ let getgoal env loc name =
       failwithf "%a: goal ‘%s’ not found" string_loc loc name in
   let goal =
     match expr with
-    | EGoal (loc, goal) -> goal
+    | 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 =
@@ -88,97 +104,12 @@ let gettactic env loc name =
       failwithf "%a: tactic ‘%s’ not found" string_loc loc name in
   let tactic =
     match expr with
-    | ETactic (loc, tactic) -> tactic
+    | ETacticDefn (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 *)
@@ -218,8 +149,9 @@ and print_env fp env = output_string fp (string_env () env)
 
 and string_def () (name, expr) =
   match expr with
-  | EGoal (loc, goal) -> string_goal () (Some name, goal) ^ "\n"
-  | ETactic (loc, tactic) -> string_tactic () (Some name, tactic) ^ "\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))
@@ -230,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
 
@@ -247,12 +192,13 @@ and string_pattern () = function
 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) ->
+  | 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) ->
      sprintf "%s (%s)"
        name (String.concat ", " (List.map (string_expr ()) params))
-  | ECallTactic (loc, name, params) ->
+  | ETacticCtor (loc, name, params) ->
      sprintf "%s (%s)"
        name (String.concat ", " (List.map (string_expr ()) params))
   | EVar (loc, var) -> var