git.annexia.org
/
goals.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
stdlib: Fix *file tactic.
[goals.git]
/
src
/
ast.ml
diff --git
a/src/ast.ml
b/src/ast.ml
index
c828bb0
..
c3b3969
100644
(file)
--- a/
src/ast.ml
+++ b/
src/ast.ml
@@
-22,7
+22,12
@@
open Printf
open Utils
open Utils
-module Env = Map.Make (String)
+module Env = struct
+ include Map.Make (String)
+
+ let merge env env' =
+ List.fold_left (fun env (k, v) -> add k v env) env (bindings env')
+end
type loc = position * position
let noloc = dummy_pos, dummy_pos
type loc = position * position
let noloc = dummy_pos, dummy_pos
@@
-36,11
+41,11
@@
let print_loc fp loc =
type env = expr Env.t
and pattern =
| PTactic of loc * id * substs list
type env = expr Env.t
and pattern =
| PTactic of loc * id * substs list
- | PVar of loc * id
and expr =
and expr =
- | EGoal of loc * goal
- | ECall of loc * id * expr list
- | ETactic of loc * id * expr list
+ | EGoalDefn of loc * goal
+ | ETacticDefn of loc * tactic
+ | ECallGoal of loc * id * expr list
+ | ETacticCtor of loc * id * expr list
| EVar of loc * id
| EList of loc * expr list
| ESubsts of loc * substs
| EVar of loc * id
| EList of loc * expr list
| ESubsts of loc * substs
@@
-48,6
+53,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 tactic = param_decl list * code
and param_decl = id
and id = string
and code = substs
and param_decl = id
and id = string
and code = substs
@@
-68,12
+74,26
@@
let getgoal env loc name =
failwithf "%a: goal ‘%s’ not found" string_loc loc name in
let goal =
match expr with
failwithf "%a: goal ‘%s’ not found" string_loc loc name in
let goal =
match expr with
- | EGoal (loc, goal) -> goal
+ | EGoal
Defn
(loc, goal) -> goal
| _ ->
failwithf "%a: tried to call ‘%s’ which is not a goal"
string_loc loc name in
goal
| _ ->
failwithf "%a: tried to call ‘%s’ which is not a goal"
string_loc loc name in
goal
+let gettactic env loc name =
+ assert (name.[0] = '*');
+ let expr =
+ try Env.find name env
+ with Not_found ->
+ failwithf "%a: tactic ‘%s’ not found" string_loc loc name in
+ let tactic =
+ match expr with
+ | 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
let rec to_constant env = function
| EConstant (loc, c) -> c
@@
-88,18
+108,22
@@
let rec to_constant env = function
failwithf "%a: list found where constant expression expected"
string_loc loc
failwithf "%a: list found where constant expression expected"
string_loc loc
- | ECall (loc, name, _) ->
+ | ECall
Goal
(loc, name, _) ->
failwithf "%a: cannot use goal ‘%s’ in constant expression"
string_loc loc name
failwithf "%a: cannot use goal ‘%s’ in constant expression"
string_loc loc name
- | ETactic (loc, name, _) ->
- failwithf "%a: cannot use tactic ‘
*
%s’ in constant expression"
+ | ETactic
Ctor
(loc, name, _) ->
+ failwithf "%a: cannot use tactic ‘%s’ in constant expression"
string_loc loc name
string_loc loc name
- | EGoal (loc, _) ->
+ | EGoal
Defn
(loc, _) ->
failwithf "%a: cannot use goal in constant expression"
string_loc 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 (
and substitute env loc substs =
let b = Buffer.create 13 in
List.iter (
@@
-139,18
+163,22
@@
and expr_to_shell_string env = function
(* These are shell quoted so we can just concat them with space. *)
String.concat " " strs
(* These are shell quoted so we can just concat them with space. *)
String.concat " " strs
- | ECall (loc, name, _) ->
+ | ECall
Goal
(loc, name, _) ->
failwithf "%a: cannot use goal ‘%s’ in shell expansion"
string_loc loc name
(* Tactics expand to the first parameter. *)
failwithf "%a: cannot use goal ‘%s’ in shell expansion"
string_loc loc name
(* Tactics expand to the first parameter. *)
- | ETactic (loc, _, []) -> Filename.quote ""
- | ETactic (loc, _, (arg :: _)) -> expr_to_shell_string env arg
+ | ETactic
Ctor
(loc, _, []) -> Filename.quote ""
+ | ETactic
Ctor
(loc, _, (arg :: _)) -> expr_to_shell_string env arg
- | EGoal (loc, _) ->
+ | EGoal
Defn
(loc, _) ->
failwithf "%a: cannot use goal in shell expansion"
string_loc 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
+
module Substs = struct
type t = {
mutable elems : subst list; (* built in reverse order *)
module Substs = struct
type t = {
mutable elems : subst list; (* built in reverse order *)
@@
-190,7
+218,8
@@
and print_env fp env = output_string fp (string_env () env)
and string_def () (name, expr) =
match expr with
and string_def () (name, expr) =
match expr with
- | EGoal (loc, goal) -> string_goal () (Some name, goal) ^ "\n"
+ | EGoalDefn (loc, goal) -> string_goal () (Some name, goal) ^ "\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))
| expr -> sprintf "let %s = %a\n" name string_expr expr;
and print_def fp name expr = output_string fp (string_def () (name, expr))
@@
-203,23
+232,28
@@
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_tactic () (name, (param_decls, code)) =
+ sprintf "tactic%s (%s) = { ... }"
+ (match name with None -> "" | Some name -> " " ^ name)
+ (String.concat ", " (List.map (string_param_decl ()) param_decls))
+
and string_param_decl () name = name
and string_pattern () = function
| PTactic (loc, name, params) ->
and string_param_decl () name = name
and string_pattern () = function
| PTactic (loc, name, params) ->
- sprintf "*%s (%s)" name (String.concat ", "
- (List.map (string_substs ()) params));
- | PVar (loc, id) -> id
+ sprintf "%s (%s)" name (String.concat ", "
+ (List.map (string_substs ()) params))
and print_pattern fp p = output_string fp (string_pattern () p)
and string_expr () = function
and print_pattern fp p = output_string fp (string_pattern () p)
and string_expr () = function
- | EGoal (loc, goal) -> string_goal () (None, goal)
- | ECall (loc, name, params) ->
+ | EGoalDefn (loc, goal) -> string_goal () (None, goal)
+ | ETacticDefn (loc, goal) -> string_tactic () (None, goal)
+ | ECallGoal (loc, name, params) ->
sprintf "%s (%s)"
name (String.concat ", " (List.map (string_expr ()) params))
sprintf "%s (%s)"
name (String.concat ", " (List.map (string_expr ()) params))
- | ETactic (loc, name, params) ->
- sprintf "
*
%s (%s)"
+ | ETactic
Ctor
(loc, name, params) ->
+ sprintf "%s (%s)"
name (String.concat ", " (List.map (string_expr ()) params))
| EVar (loc, var) -> var
| EList (loc, xs) ->
name (String.concat ", " (List.map (string_expr ()) params))
| EVar (loc, var) -> var
| EList (loc, xs) ->