git.annexia.org
/
goals.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Implement functions.
[goals.git]
/
src
/
ast.ml
diff --git
a/src/ast.ml
b/src/ast.ml
index
b4f86e7
..
922827c
100644
(file)
--- 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
| PTactic of loc * id * substs list
and expr =
| EGoalDefn of loc * goal
+ | EFuncDefn of loc * func
| ETacticDefn of loc * tactic
| ETacticDefn of loc * tactic
- | ECall
Goal
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
| ETacticCtor of loc * id * expr list
| EVar of loc * id
| EList of loc * expr list
@@
-53,6
+54,7
@@
and expr =
and constant =
| CString of string
and goal = param_decl list * pattern list * expr list * code option
and constant =
| CString of string
and goal = param_decl list * pattern list * expr list * code option
+and func = param_decl list * code
and tactic = param_decl list * code
and param_decl = id
and id = string
and tactic = param_decl list * code
and param_decl = id
and id = string
@@
-80,6
+82,19
@@
let getgoal env loc name =
string_loc loc name in
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 =
let gettactic env loc name =
assert (name.[0] = '*');
let expr =
@@
-134,6
+149,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"
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;
| ETacticDefn (loc, tactic) -> string_tactic () (Some name, tactic) ^ "\n"
| expr -> sprintf "let %s = %a\n" name string_expr expr;
@@
-147,6
+163,11
@@
and string_goal () (name, (param_decls, patterns, exprs, code)) =
(String.concat ", " (List.map (string_expr ()) exprs))
(match code with None -> "" | Some code -> " = { ... }")
(String.concat ", " (List.map (string_expr ()) exprs))
(match code with None -> "" | Some code -> " = { ... }")
+and string_func () (name, (param_decls, code)) =
+ sprintf "function%s (%s) = { ... }"
+ (match name with None -> "" | Some name -> " " ^ name)
+ (String.concat ", " (List.map (string_param_decl ()) param_decls))
+
and string_tactic () (name, (param_decls, code)) =
sprintf "tactic%s (%s) = { ... }"
(match name with None -> "" | Some name -> " " ^ name)
and string_tactic () (name, (param_decls, code)) =
sprintf "tactic%s (%s) = { ... }"
(match name with None -> "" | Some name -> " " ^ name)
@@
-163,8
+184,9
@@
and print_pattern fp p = output_string fp (string_pattern () p)
and string_expr () = function
| EGoalDefn (loc, goal) -> string_goal () (None, goal)
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)
| ETacticDefn (loc, goal) -> string_tactic () (None, goal)
- | ECall
Goal
(loc, name, params) ->
+ | ECall (loc, name, params) ->
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))
| ETacticCtor (loc, name, params) ->