* 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
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 *)