git.annexia.org
/
goals.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
86051da
)
Fix ‘goal’ when it appears as a target (meaning ‘goal()’).
author
Richard W.M. Jones
<rjones@redhat.com>
Tue, 31 Dec 2019 09:08:35 +0000
(09:08 +0000)
committer
Richard W.M. Jones
<rjones@redhat.com>
Tue, 31 Dec 2019 09:09:04 +0000
(09:09 +0000)
src/eval.ml
patch
|
blob
|
history
diff --git
a/src/eval.ml
b/src/eval.ml
index
66b0164
..
1688b5f
100644
(file)
--- a/
src/eval.ml
+++ b/
src/eval.ml
@@
-40,10
+40,20
@@
and evaluate_target env = function
let args = List.map (Ast.to_constant env) args in
run_tactic env loc name args
let args = List.map (Ast.to_constant env) args in
run_tactic env loc name args
- (* Look up the variable and substitute it. *)
+ (* If this is a goal then it's the same as calling goal(). If not
+ * then look up the variable and substitute it.
+ *)
| Ast.EVar (loc, name) ->
let expr = Ast.getvar env loc name in
| Ast.EVar (loc, name) ->
let expr = Ast.getvar env loc name in
- evaluate_target env expr
+ (match expr with
+ | EGoal (loc, ([], _, _, _)) ->
+ evaluate_target env (Ast.ECallGoal (loc, name, []))
+ | EGoal _ ->
+ failwithf "%a: cannot call %s() since this goal has parameters"
+ Ast.string_loc loc name
+ | _ ->
+ evaluate_target env expr
+ )
(* Lists are inlined when found as a target. *)
| Ast.EList (loc, exprs) ->
(* Lists are inlined when found as a target. *)
| Ast.EList (loc, exprs) ->