open CicNotationPt
-exception Value_not_found of string
-
type value =
| TermValue of term
| StringValue of string
| OptType of value_type
| ListType of value_type
+exception Value_not_found of string
+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
+let lookup env name =
+ try
+ List.assoc name env
+ with Not_found -> raise (Value_not_found name)
+
let lookup_value env name =
try
snd (List.assoc name env)
let remove env name = List.remove_assoc name env
let lookup_term env name =
- match lookup_value env name with
- | TermValue x -> x
- | _ -> raise (Value_not_found name)
+ match lookup env name with
+ | _, TermValue x -> x
+ | ty, _ -> raise (Type_mismatch (name, ty))
let lookup_num env name =
- match lookup_value env name with
- | NumValue x -> x
- | _ -> raise (Value_not_found name)
+ match lookup env name with
+ | _, NumValue x -> x
+ | ty, _ -> raise (Type_mismatch (name, ty))
let lookup_string env name =
- match lookup_value env name with
- | StringValue x -> x
- | _ -> raise (Value_not_found name)
+ match lookup env name with
+ | _, StringValue x -> x
+ | ty, _ -> raise (Type_mismatch (name, ty))
+
+let lookup_opt env name =
+ match lookup env name with
+ | _, OptValue x -> x
+ | ty, _ -> raise (Type_mismatch (name, ty))
+
+let lookup_list env name =
+ match lookup env name with
+ | _, ListValue x -> x
+ | ty, _ -> raise (Type_mismatch (name, ty))
let opt_binding_some (n, (ty, v)) = (n, (OptType ty, OptValue (Some v)))
let opt_binding_none (n, (ty, v)) = (n, (OptType ty, OptValue None))
| _ -> false
let declarations_of_env = List.map (fun (name, (ty, _)) -> (name, ty))
+let declarations_of_term p =
+ List.map declaration_of_var (CicNotationUtil.variables_of_term p)
+
+let rec combine decls values =
+ match decls, values with
+ | [], [] -> []
+ | (name, ty) :: decls, v :: values ->
+ (name, (ty, v)) :: (combine decls values)
+ | _ -> assert false
let coalesce_env declarations env_list =
let env0 = List.map list_binding_of_name declarations in