X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=src%2Fast.ml;h=8e56fb5fbef44d981548d46dd5781d34fee63a6c;hb=54c8ad92025a9c77c2b10644499b3944e1299187;hp=62af83345bf03f2d34eec7162d1127142ee7c817;hpb=24cc20b33e3d81ed7d754391bef929276c1f4f42;p=goals.git diff --git a/src/ast.ml b/src/ast.ml index 62af833..8e56fb5 100644 --- a/src/ast.ml +++ b/src/ast.ml @@ -22,7 +22,12 @@ open Printf 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 @@ -36,11 +41,12 @@ let print_loc fp loc = type env = expr Env.t and pattern = | PTactic of loc * id * substs list - | PVar of loc * id and expr = - | EGoal of loc * goal + | EGoalDefn of loc * goal + | EFuncDefn of loc * func + | ETacticDefn of loc * tactic | ECall of loc * id * expr list - | ETactic of loc * id * expr list + | ETacticCtor of loc * id * expr list | EVar of loc * id | EList of loc * expr list | ESubsts of loc * substs @@ -48,9 +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 @@ -68,49 +77,38 @@ 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 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 - - | ECall (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" - string_loc loc name - - | EGoal (loc, _) -> - failwithf "%a: cannot use goal in constant expression" - string_loc loc +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 -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 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 module Substs = struct type t = { @@ -151,7 +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" + | 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)) @@ -162,25 +162,44 @@ 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, 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 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 - | EGoal (loc, goal) -> string_goal () (None, goal) + | 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)) - | ETactic (loc, name, params) -> - sprintf "*%s (%s)" + | ETacticCtor (loc, name, params) -> + sprintf "%s (%s)" name (String.concat ", " (List.map (string_expr ()) params)) | EVar (loc, var) -> var | EList (loc, xs) ->