* http://helm.cs.unibo.it/
*)
-open CicNotationPt
+module Ast = CicNotationPt
type value =
- | TermValue of term
+ | TermValue of Ast.term
| StringValue of string
| NumValue of string
| OptValue of value option
type declaration = string * value_type
type binding = string * (value_type * value)
-type t = (string * (value_type * value)) list
+type t = binding list
let lookup env name =
try
snd (List.assoc name env)
with Not_found -> raise (Value_not_found name)
-let remove env name = List.remove_assoc name env
+let remove_name env name = List.remove_assoc name env
+
+let remove_names env names =
+ List.filter (fun name, _ -> not (List.mem name names)) env
let lookup_term env name =
match lookup env name with
let list_declaration (n, ty) = (n, ListType ty)
let declaration_of_var = function
- | NumVar s -> s, NumType
- | IdentVar s -> s, StringType
- | TermVar s -> s, TermType
+ | Ast.NumVar s -> s, NumType
+ | Ast.IdentVar s -> s, StringType
+ | Ast.TermVar s -> s, TermType
| _ -> assert false
let value_of_term = function
- | Num (s, _) -> NumValue s
- | Ident (s, None) -> StringValue s
+ | Ast.Num (s, _) -> NumValue s
+ | Ast.Ident (s, None) -> StringValue s
| t -> TermValue t
let term_of_value = function
- | NumValue s -> Num (s, 0)
- | StringValue s -> Ident (s, None)
+ | NumValue s -> Ast.Num (s, 0)
+ | StringValue s -> Ast.Ident (s, None)
| TermValue t -> t
| _ -> assert false (* TO BE UNDERSTOOD *)