X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fcontent%2FnotationEnv.ml;h=6951760bf3a9fb18282db148041ee5c1fdd53262;hb=37ee4577977f031ae897b615784128911450acfa;hp=77ffd92f22b60e9d7fdce05d7949f85f00e1ffb5;hpb=a2412e41cda18a25d780ae631ee02d6ae05c52b1;p=helm.git diff --git a/matitaB/components/content/notationEnv.ml b/matitaB/components/content/notationEnv.ml index 77ffd92f2..6951760bf 100644 --- a/matitaB/components/content/notationEnv.ml +++ b/matitaB/components/content/notationEnv.ml @@ -32,18 +32,23 @@ type ident_or_var = | Var of string type value = - | TermValue of Ast.term + | TermValue of NotationPt.term | StringValue of ident_or_var | NumValue of string | OptValue of value option | ListValue of value list + (* optional name of Ast.Symbols that we want to contain the interpretation of this literal + * location of the literal we are parsing + * optional uri, optional desc *) + | DisambiguationValue of (string option * Stdpp.location * string option * string option) type value_type = - | TermType of int + | TermType of int (* the level of the expected term *) | StringType | NumType | OptType of value_type | ListType of value_type + | NoType exception Value_not_found of string exception Type_mismatch of string * value_type @@ -52,6 +57,21 @@ type declaration = string * value_type type binding = string * (value_type * value) type t = binding list +(* let rec pp_value = function + | TermValue t -> "T#" ^ NotationPp.pp_term (new NCicPp.status) t + | StringValue (Ident i) -> "I#" ^ i + | StringValue (Var v) -> "V#" ^ v + | NumValue n -> "N#" ^ n + | OptValue None -> "O#None" + | OptValue (Some v) -> "O#" ^ pp_value v + | ListValue vl -> "L#[" ^ (String.concat ";" (List.map pp_value vl)) ^ "]" + | DisambiguationValue _ -> "D#" + +let pp_binding = function + | s, (ty,v) -> Printf.sprintf "{ %s := %s : %s }" s (pp_value v) "..." + +let pp_env e = String.concat " " (List.map pp_binding e) *) + let lookup env name = try List.assoc name env