type env = expr Env.t
and pattern =
- | PTactic of loc * id * substs list
+ | PPred of loc * id * substs list
and expr =
| EGoalDefn of loc * goal
- | ETacticDefn of loc * tactic
- | ECallGoal of loc * id * expr list
- | ECallTactic of loc * id * expr list
+ | 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
and constant =
| CString of string
and goal = param_decl list * pattern list * expr list * code option
-and tactic = param_decl list * code
+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
string_loc loc name in
goal
-let gettactic env loc name =
- assert (name.[0] = '*');
+let getfunc env loc name =
let expr =
try Env.find name env
with Not_found ->
- failwithf "%a: tactic ‘%s’ not found" string_loc loc name in
- let tactic =
+ failwithf "%a: func ‘%s’ not found" string_loc loc name in
+ let func =
match expr with
- | ETacticDefn (loc, tactic) -> tactic
+ | EFuncDefn (loc, func) -> func
| _ ->
- failwithf "%a: tried to call ‘%s’ which is not a tactic"
+ failwithf "%a: tried to call ‘%s’ which is not a function"
string_loc loc name in
- tactic
+ func
-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
-
- | EGoalDefn (loc, _) ->
- failwithf "%a: cannot use goal in constant expression"
- string_loc loc
-
- | ETacticDefn (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
-
- | EGoalDefn (loc, _) ->
- failwithf "%a: cannot use goal in shell expansion"
- string_loc loc
-
- | ETacticDefn (loc, _) ->
- failwithf "%a: cannot use tactic in shell expansion"
- string_loc loc
+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 = {
and string_def () (name, expr) =
match expr with
| EGoalDefn (loc, goal) -> string_goal () (Some name, goal) ^ "\n"
- | ETacticDefn (loc, tactic) -> string_tactic () (Some name, tactic) ^ "\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))
(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_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
- | PTactic (loc, name, params) ->
+ | PPred (loc, name, params) ->
sprintf "%s (%s)" name (String.concat ", "
(List.map (string_substs ()) params))
and string_expr () = function
| EGoalDefn (loc, goal) -> string_goal () (None, goal)
- | ETacticDefn (loc, goal) -> string_tactic () (None, goal)
- | ECallGoal (loc, name, params) ->
+ | 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))
- | ECallTactic (loc, name, params) ->
+ | EPredCtor (loc, name, params) ->
sprintf "%s (%s)"
name (String.concat ", " (List.map (string_expr ()) params))
| EVar (loc, var) -> var
git.annexia.org / goals.git / blobdiff