-(* Take any expression and simplify it down to a constant.
- * If the expression cannot be simplified then this throws
- * an error.
- *)
-and simplify env = function
- | Ast.EConstant (loc, c) -> c
-
- | Ast.EVar (loc, name) ->
- let expr =
- try Ast.Env.find name env
- with Not_found ->
- failwithf "%a: variable ‘%s’ not found" Ast.string_loc loc name in
- simplify env expr
-
- | Ast.ESubsts (loc, str) ->
- Ast.CString (substitute loc env str)
-
- | Ast.EList (loc, _) ->
- failwithf "%a: list found where constant expression expected"
- Ast.string_loc loc
-
- | Ast.ECall (loc, name, _) ->
- failwithf "%a: cannot use goal ‘%s’ in constant expression"
- Ast.string_loc loc name
-
- | Ast.ETactic (loc, name, _) ->
- failwithf "%a: cannot use tactic ‘*%s’ in constant expression"
- Ast.string_loc loc name
-
- | Ast.EGoal (loc, _) ->
- failwithf "%a: cannot use goal in constant expression"
- Ast.string_loc loc
-
-(* Take a substitution list and try to turn it into a simple
- * string by evaluating every variable. If not possible this
- * throws an error. Returns a string.
- *)
-and substitute loc env substs =
- let b = Buffer.create 13 in
- List.iter (
- function
- | Ast.SString s -> Buffer.add_string b s
- | Ast.SVar name ->
- let expr =
- try Ast.Env.find name env
- with Not_found ->
- failwithf "%a: variable ‘%s’ not found" Ast.string_loc loc name in
- match simplify env expr with
- | Ast.CString s -> Buffer.add_string b s
- ) substs;
- Buffer.contents b