X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationEnv.ml;h=62212f92fba871d7462d1b3ac80bb13d0574a193;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=f7f11c46db4a2951f355acc9d169bce233a586bd;hpb=f7759f86b755f4f7dc2b23edd52ed4d2e5c028fe;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationEnv.ml b/helm/ocaml/cic_notation/cicNotationEnv.ml index f7f11c46d..62212f92f 100644 --- a/helm/ocaml/cic_notation/cicNotationEnv.ml +++ b/helm/ocaml/cic_notation/cicNotationEnv.ml @@ -23,10 +23,10 @@ * 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 @@ -44,7 +44,7 @@ exception Type_mismatch of string * value_type 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 @@ -56,7 +56,10 @@ let lookup_value env name = 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 @@ -91,19 +94,19 @@ let opt_declaration (n, ty) = (n, OptType ty) 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 *)