distinction lident/uident a la Caml

src/lexer.mll

@@ -127,10 +127,12 @@
 
 let newline = '\n'
 let space = [' ' '\t' '\r']
-let alpha = ['a'-'z' 'A'-'Z']
-let letter = alpha | '_'
+let lalpha = ['a'-'z' '_']
+let ualpha = ['A'-'Z']
+let alpha = lalpha | ualpha
 let digit = ['0'-'9']
-let ident = letter (letter | digit | '\'')*
+let lident = lalpha (alpha | digit | '\'')*
+let uident = ualpha (alpha | digit | '\'')*
 let hexadigit = ['0'-'9' 'a'-'f' 'A'-'F']
 (*
 let hexafloat = '0' ['x' 'X'] (hexadigit* '.' hexadigit+ | hexadigit+ '.' hexadigit* ) ['p' 'P'] ['-' '+']? digit+
@@ -144,8 +146,10 @@ rule token = parse
       { newline lexbuf; token lexbuf }
   | space+  
       { token lexbuf }
-  | ident as id  
-      { try Hashtbl.find keywords id with Not_found -> IDENT id }
+  | lident as id  
+      { try Hashtbl.find keywords id with Not_found -> LIDENT id }
+  | uident as id  
+      { UIDENT id }
   | digit+ as s
       { INTEGER s }
   | (digit+ as i) ("" as f) ['e' 'E'] (['-' '+']? digit+ as e)

src/parser.mly

@@ -87,7 +87,7 @@
 
 /* Tokens */ 
 
-%token <string> IDENT
+%token <string> LIDENT UIDENT
 %token <string> INTEGER
 %token <Ptree.real_constant> FLOAT
 %token <string> STRING
@@ -168,12 +168,26 @@ list0_decl:
 ;
 
 ident:
-| IDENT { { id = $1; id_loc = loc () } }
+| LIDENT { { id = $1; id_loc = loc () } }
+| UIDENT { { id = $1; id_loc = loc () } }
 ;
 
-qualid:
-| ident           { Qident $1 }
-| ident DOT ident { Qdot ($1, $3) }
+lident:
+| LIDENT { { id = $1; id_loc = loc () } }
+;
+
+uident:
+| UIDENT { { id = $1; id_loc = loc () } }
+;
+
+lqualid:
+| lident             { Qident $1 }
+| uqualid DOT lident { Qdot ($1, $3) }
+;
+
+uqualid:
+| uident             { Qident $1 }
+| uqualid DOT uident { Qdot ($1, $3) }
 ;
 
 decl:
@@ -277,11 +291,11 @@ primitive_type:
 */
 | type_var 
    { PPTvarid $1 }
-| qualid
+| lqualid
    { PPTexternal ([], $1) }
-| primitive_type qualid
+| primitive_type lqualid
    { PPTexternal ([$1], $2) }
-| LEFTPAR primitive_type COMMA list1_primitive_type_sep_comma RIGHTPAR qualid
+| LEFTPAR primitive_type COMMA list1_primitive_type_sep_comma RIGHTPAR lqualid
    { PPTexternal ($2 :: $4, $6) }
 /*
 | LEFTPAR list1_primitive_type_sep_comma RIGHTPAR
@@ -360,9 +374,9 @@ lexpr:
    { infix_pp $1 PPmod $3 }
 | MINUS lexpr %prec uminus
    { prefix_pp PPneg $2 }
-| qualid
+| lqualid
    { mk_pp (PPvar $1) }
-| qualid LEFTPAR list1_lexpr_sep_comma RIGHTPAR
+| lqualid LEFTPAR list1_lexpr_sep_comma RIGHTPAR
    { mk_pp (PPapp ($1, $3)) }
 /***
 | qualid_ident LEFTSQ lexpr RIGHTSQ
@@ -412,8 +426,8 @@ match_case:
 ;
 
 pattern:
-| qualid                                         { ($1, [], loc ()) }
-| qualid LEFTPAR list1_ident_sep_comma RIGHTPAR  { ($1, $3, loc ()) }
+| uqualid                                         { ($1, [], loc ()) }
+| uqualid LEFTPAR list1_ident_sep_comma RIGHTPAR  { ($1, $3, loc ()) }
 ;
 
 triggers:
@@ -462,7 +476,7 @@ qualid_ident:
 ***/
 
 ident_or_string:
-| IDENT  { $1 }
+| ident  { $1.id }
 | STRING { $1 }
 ;
 

src/ptree.mli

@@ -40,7 +40,7 @@ type ident = { id : string; id_loc : loc }
 
 type qualid =
   | Qident of ident
-  | Qdot of ident * ident
+  | Qdot of qualid * ident
 
 type ppure_type =
 (*

src/test.why

 
 (* test file *)
 
-theory int
+theory Int
 
   type int
 
 end
 
-theory list
+theory List
 
-  uses int
+  uses Int
 
   type 'a list
 
@@ -19,11 +19,11 @@ theory list
 
   logic is_nil : 'a list -> prop
 
-  logic length : 'a list -> int.int
+  logic length : 'a list -> Int.int
 
 end
 
-theory eq 
+theory Eq 
 
   logic eq : 'a, 'a -> prop
 
@@ -31,30 +31,30 @@ end
 
 theory set
 
-  uses eq
+  uses Eq
 
   type elt
 
   type t 
 
-  logic In : elt, t -> prop
+  logic in_ : elt, t -> prop
 
   logic empty : t
 
-  axiom empty_def1 : forall x:elt, not In(x, empty)
+  axiom empty_def1 : forall x:elt, not in_(x, empty)
 
   logic add : elt, t -> t
 
   axiom add_def1 : forall x,y:elt, forall s:t, 
-                   In(x, add(y, s)) <-> (eq.eq(x, y) or In(x, s))
+                   in_(x, add(y, s)) <-> (Eq.eq(x, y) or in_(x, s))
 
 end
 
 theory test
 
-  uses eq, list
+  uses Eq, List
 
-  axiom a : forall x : 'a, not eq.eq(list.nil, list.cons(list.nil, list.nil))
+  axiom a : forall x : 'a, not Eq.eq(List.nil, List.cons(List.nil, List.nil))
 
 end
 

src/typing.ml

@@ -23,6 +23,7 @@ open Ptree
 (** errors *)
 
 type error = 
+  | Message of string
   | ClashType of string
   | BadTypeArity of string
   | UnboundType of qualid
@@ -43,11 +44,13 @@ let error ?loc e = match loc with
   | None -> raise (Error e)
   | Some loc -> raise (Loc.Located (loc, Error e))
 
-let print_qualid fmt = function
+let rec print_qualid fmt = function
   | Qident s -> fprintf fmt "%s" s.id
-  | Qdot (m, s) -> fprintf fmt "%s.%s" m.id s.id
+  | Qdot (m, s) -> fprintf fmt "%a.%s" print_qualid m s.id
 
 let report fmt = function
+  | Message s ->
+      fprintf fmt "%s" s
   | ClashType s ->
       fprintf fmt "clash with previous type %s" s
   | BadTypeArity s ->
@@ -99,9 +102,9 @@ let is_empty env =
   M.is_empty env.fsymbols &&
   M.is_empty env.psymbols
 
-let find_tysymbol s env = M.find s env.tysymbols
-let find_fsymbol s env = M.find s env.fsymbols
-let find_psymbol s env = M.find s env.psymbols
+let find_tysymbol s env = M.find s.id env.tysymbols
+let find_fsymbol s env = M.find s.id env.fsymbols
+let find_psymbol s env = M.find s.id env.psymbols
 
 let add_tysymbol x ty env = { env with tysymbols = M.add x ty env.tysymbols }
 
@@ -226,16 +229,17 @@ let rec specialize env t = match t.Ty.ty_node with
   | Ty.Tyapp (s, tl) ->
       Tyapp (s, List.map (specialize env) tl)
 
-let find_local_theory t env =
+let find_local_theory t env = 
   try M.find t.id env.theories
   with Not_found -> error ~loc:t.id_loc (UnboundTheory t.id)
 
-let find f q env = match q with
-  | Qident x -> 
-      f x.id env
-  | Qdot (m, x) -> 
-      let env = find_local_theory m env in
-      f x.id env
+let rec find_theory q env = match q with
+  | Qident t -> find_local_theory t env
+  | Qdot (q, t) -> let env = find_theory q env in find_local_theory t env
+
+let rec find f q env = match q with
+  | Qident x -> f x env
+  | Qdot (m, x) -> let env = find_theory m env in f x env
 
 let specialize_tysymbol x env =
   let s = find find_tysymbol x env.env in
@@ -255,9 +259,9 @@ let specialize_psymbol x env =
 
 (** Typing types *)
 
-let qloc = function
+let rec qloc = function
   | Qident x -> x.id_loc
-  | Qdot (m, x) -> Loc.join m.id_loc x.id_loc
+  | Qdot (m, x) -> Loc.join (qloc m) x.id_loc
 
 (* parsed types -> intermediate types *)
 let rec dty env = function
@@ -267,7 +271,7 @@ let rec dty env = function
       let loc = qloc x in
       let s, tv = 
 	try specialize_tysymbol x env
-	with Not_found -> error ~loc:loc (UnboundType x);
+	with Not_found -> error ~loc:loc (UnboundType x)
       in
       let np = List.length p in
       let a = List.length tv in

src/typing.mli

@@ -22,9 +22,9 @@ type env
 
 val empty : env
 
-val find_tysymbol : string -> env -> tysymbol
-val find_fsymbol : string -> env -> fsymbol
-val find_psymbol : string -> env -> psymbol
+val find_tysymbol : Ptree.ident -> env -> tysymbol
+val find_fsymbol : Ptree.ident -> env -> fsymbol
+val find_psymbol : Ptree.ident -> env -> psymbol
 
 (** typing *)