noms qualifies (mais pas encore de uses)

src/parser.mly

@@ -167,6 +167,15 @@ list0_decl:
    { $1 }
 ;
 
+ident:
+| IDENT { { id = $1; id_loc = loc () } }
+;
+
+qualid:
+| ident           { Qident $1 }
+| ident DOT ident { Qdot ($1, $3) }
+;
+
 decl:
 | external_ LOGIC list1_ident_sep_comma COLON logic_type
    { Logic (loc_i 3, $1, $3, $5) }
@@ -266,13 +275,13 @@ primitive_type:
    { PPTunit }
 */
 | type_var 
-   { PPTvarid ($1, loc ()) }
-| ident 
-   { PPTexternal ([], $1, loc ()) }
-| primitive_type ident
-   { PPTexternal ([$1], $2, loc_i 2) }
-| LEFTPAR primitive_type COMMA list1_primitive_type_sep_comma RIGHTPAR ident
-   { PPTexternal ($2 :: $4, $6, loc_i 6) }
+   { PPTvarid $1 }
+| qualid
+   { PPTexternal ([], $1) }
+| primitive_type qualid
+   { PPTexternal ([$1], $2) }
+| LEFTPAR primitive_type COMMA list1_primitive_type_sep_comma RIGHTPAR qualid
+   { PPTexternal ($2 :: $4, $6) }
 /*
 | LEFTPAR list1_primitive_type_sep_comma RIGHTPAR
    { match $2 with [p] -> p | _ -> raise Parse_error }
@@ -350,9 +359,9 @@ lexpr:
    { infix_pp $1 PPmod $3 }
 | MINUS lexpr %prec uminus
    { prefix_pp PPneg $2 }
-| ident
+| qualid
    { mk_pp (PPvar $1) }
-| ident LEFTPAR list1_lexpr_sep_comma RIGHTPAR
+| qualid LEFTPAR list1_lexpr_sep_comma RIGHTPAR
    { mk_pp (PPapp ($1, $3)) }
 /***
 | qualid_ident LEFTSQ lexpr RIGHTSQ
@@ -361,14 +370,14 @@ lexpr:
 | IF lexpr THEN lexpr ELSE lexpr %prec prec_if 
    { mk_pp (PPif ($2, $4, $6)) }
 | FORALL list1_ident_sep_comma COLON primitive_type triggers 
-  DOT lexpr %prec prec_forall
+  COMMA lexpr %prec prec_forall
    { let rec mk = function
        | [] -> assert false
        | [id] -> mk_pp (PPforall (id, $4, $5, $7))
        | id :: l -> mk_pp (PPforall (id, $4, [], mk l))
      in
      mk $2 }
-| EXISTS ident COLON primitive_type DOT lexpr %prec prec_exists
+| EXISTS ident COLON primitive_type COMMA lexpr %prec prec_exists
    { mk_pp (PPexists ($2, $4, $6)) }
 | INTEGER
    { mk_pp (PPconst (ConstInt $1)) }
@@ -402,8 +411,8 @@ match_case:
 ;
 
 pattern:
-| ident                                         { ($1, [], loc ()) }
-| ident LEFTPAR list1_ident_sep_comma RIGHTPAR  { ($1, $3, loc ()) }
+| qualid                                         { ($1, [], loc ()) }
+| qualid LEFTPAR list1_ident_sep_comma RIGHTPAR  { ($1, $3, loc ()) }
 ;
 
 triggers:
@@ -443,15 +452,13 @@ list1_type_var_sep_comma:
 | type_var COMMA list1_type_var_sep_comma { $1 :: $3 }
 ;
 
-ident:
-| IDENT { $1 }
-;
-
+/***
 qualid_ident:
 | IDENT          { $1, None }
 | IDENT AT       { $1, Some "" }
 | IDENT AT IDENT { $1, Some $3 }
 ;
+***/
 
 ident_or_string:
 | IDENT  { $1 }

src/ptree.mli

@@ -36,6 +36,12 @@ type pp_infix =
 type pp_prefix = 
   PPneg | PPnot
 
+type ident = { id : string; id_loc : loc }
+
+type qualid =
+  | Qident of ident
+  | Qdot of ident * ident
+
 type ppure_type =
 (*
   | PPTint
@@ -43,26 +49,26 @@ type ppure_type =
   | PPTreal
   | PPTunit
 *)
-  | PPTvarid of string * Loc.position
-  | PPTexternal of ppure_type list * string * Loc.position
+  | PPTvarid of ident
+  | PPTexternal of ppure_type list * qualid
 
 type lexpr = 
   { pp_loc : loc; pp_desc : pp_desc }
 
 and pp_desc =
-  | PPvar of string
-  | PPapp of string * lexpr list
+  | PPvar of qualid
+  | PPapp of qualid * lexpr list
   | PPtrue
   | PPfalse
   | PPconst of constant
   | PPinfix of lexpr * pp_infix * lexpr
   | PPprefix of pp_prefix * lexpr
   | PPif of lexpr * lexpr * lexpr
-  | PPforall of string * ppure_type * lexpr list list * lexpr
-  | PPexists of string * ppure_type * lexpr
+  | PPforall of ident * ppure_type * lexpr list list * lexpr
+  | PPexists of ident * ppure_type * lexpr
   | PPnamed of string * lexpr
-  | PPlet of string * lexpr * lexpr
-  | PPmatch of lexpr * ((string * string list * loc) * lexpr) list
+  | PPlet of ident* lexpr * lexpr
+  | PPmatch of lexpr * ((qualid * ident list * loc) * lexpr) list
 
 (*s Declarations. *)
 
@@ -72,19 +78,19 @@ type plogic_type =
   | PPredicate of ppure_type list
   | PFunction of ppure_type list * ppure_type
 
-type uses = string
+type uses = ident
 
 type logic_decl = 
-  | Logic of loc * external_ * string list * plogic_type
-  | Predicate_def of loc * string * (loc * string * ppure_type) list * lexpr
-  | Inductive_def of loc * string * plogic_type * (loc * string * lexpr) list
+  | Logic of loc * external_ * ident list * plogic_type
+  | Predicate_def of loc * ident * (loc * ident * ppure_type) list * lexpr
+  | Inductive_def of loc * ident * plogic_type * (loc * ident * lexpr) list
   | Function_def 
-      of loc * string * (loc * string * ppure_type) list * ppure_type * lexpr
-  | Axiom of loc * string * lexpr
-  | Goal of loc * string * lexpr
-  | TypeDecl of loc * external_ * string list * string
-  | AlgType of (loc * string list * string
-      * (loc * string * ppure_type list) list) list
-  | Theory of loc * string * uses list * logic_decl list
+      of loc * ident * (loc * ident * ppure_type) list * ppure_type * lexpr
+  | Axiom of loc * ident * lexpr
+  | Goal of loc * ident * lexpr
+  | TypeDecl of loc * external_ * ident list * ident
+  | AlgType of (loc * ident list * ident
+      * (loc * ident * ppure_type list) list) list
+  | Theory of loc * ident * uses list * logic_decl list
 
 type logic_file = logic_decl list

src/test.why

 
 (* test file *)
 
-theory test  
+theory int
+
+  type int
+
+end
+
+theory list
 
   type 'a list
 
@@ -9,24 +15,40 @@ theory test
 
   logic cons : 'a, 'a list -> 'a list
 
-  type int
+  logic is_nil : 'a list -> prop
 
-  logic length : 'a list -> int
+  logic length : 'a list -> int.int
 
-  logic is_nil : 'a list -> prop
+end
 
-  logic eq : 'a, 'a -> prop
+theory eq 
 
-  axiom a : forall x : 'a. not eq(nil, cons(nil, nil))
+  logic eq : 'a, 'a -> prop
 
 end
 
-theory test2
+theory set
 
   type elt
 
   type t 
 
+  logic In : elt, t -> prop
+
+  logic empty : t
+
+  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))
+
 end
+
+theory test
+
+ axiom a : forall x : 'a, not eq.eq(list.nil, list.cons(list.nil, list.nil))
+
+end
+

src/typing.ml

@@ -25,16 +25,17 @@ open Ptree
 type error = 
   | ClashType of string
   | BadTypeArity of string
-  | UnboundType of string
-  | TypeArity of string * int * int
+  | UnboundType of qualid
+  | TypeArity of qualid * int * int
   | Clash of string
   | PredicateExpected
   | TermExpected
-  | UnboundSymbol of string
+  | UnboundSymbol of qualid
   | TermExpectedType of (formatter -> unit) * (formatter -> unit) 
       (* actual / expected *)
   | BadNumberOfArguments of Name.t * int * int 
   | ClashTheory of string
+  | UnboundTheory of string
 
 exception Error of error
 
@@ -42,15 +43,19 @@ let error ?loc e = match loc with
   | None -> raise (Error e)
   | Some loc -> raise (Loc.Located (loc, Error e))
 
+let print_qualid fmt = function
+  | Qident s -> fprintf fmt "%s" s.id
+  | Qdot (m, s) -> fprintf fmt "%s.%s" m.id s.id
+
 let report fmt = function
   | ClashType s ->
       fprintf fmt "clash with previous type %s" s
   | BadTypeArity s ->
       fprintf fmt "duplicate type parameter %s" s
   | UnboundType s ->
-       fprintf fmt "Unbound type '%s'" s
+       fprintf fmt "Unbound type '%a'" print_qualid s
   | TypeArity (id, a, n) ->
-      fprintf fmt "@[The type %s expects %d argument(s),@ " id a;
+      fprintf fmt "@[The type %a expects %d argument(s),@ " print_qualid id a;
       fprintf fmt "but is applied to %d argument(s)@]" n
   | Clash id ->
       fprintf fmt "Clash with previous constant %s" id
@@ -59,7 +64,7 @@ let report fmt = function
   | TermExpected ->
       fprintf fmt "syntax error: term expected"
   | UnboundSymbol s ->
-       fprintf fmt "Unbound symbol '%s'" s
+       fprintf fmt "Unbound symbol '%a'" print_qualid s
   | BadNumberOfArguments (s, n, m) ->
       fprintf fmt "@[Symbol `%a' is aplied to %d terms,@ " Name.print s n;
       fprintf fmt "but is expecting %d arguments@]" m
@@ -68,6 +73,8 @@ let report fmt = function
       fprintf fmt "@ but is expected to have type@ "; ty2 fmt; fprintf fmt "@]"
   | ClashTheory s ->
       fprintf fmt "clash with previous theory %s" s
+  | UnboundTheory s ->
+      fprintf fmt "unbound theory %s" s
 
 (** typing environments *)
 
@@ -193,34 +200,11 @@ let find_user_type_var x env =
     Hashtbl.add env.utyvars x v;
     v
  
-(** Typing types *)
-
-(* parsed types -> intermediate types *)
-let rec dty env = function
-  | PPTvarid (x, _) -> 
-      Tyvar (find_user_type_var x env)
-  | PPTexternal (p, id, loc) ->
-      if not (M.mem id env.env.tysymbols) then error ~loc (UnboundType id);
-      let s = M.find id env.env.tysymbols in
-      let np = List.length p in
-      let a = List.length s.Ty.ts_args in
-      if np <> a then error ~loc (TypeArity (id, a, np));
-      Tyapp (s, List.map (dty env) p)
-
-(* intermediate types -> types *)
-let rec ty = function
-  | Tyvar { type_val = Some t } ->
-      ty t
-  | Tyvar { tvsymbol = tv } ->
-      Ty.ty_var tv
-  | Tyapp (s, tl) ->
-      Ty.ty_app s (List.map ty tl)
-
 (* Specialize *)
 
 module Htv = Hashtbl.Make(Name)
 
-let find_type_var tv env =
+let find_type_var env tv =
   try
     Htv.find env tv
   with Not_found ->
@@ -230,21 +214,67 @@ let find_type_var tv env =
  
 let rec specialize env t = match t.Ty.ty_node with
   | Ty.Tyvar tv -> 
-      Tyvar (find_type_var tv env)
+      Tyvar (find_type_var env tv)
   | Ty.Tyapp (s, tl) ->
       Tyapp (s, List.map (specialize env) tl)
+
+let find_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_theory m env in
+      f x.id env
+
+let specialize_tysymbol x env =
+  let s = find find_tysymbol x env.env in
+  let env = Htv.create 17 in
+  s, List.map (find_type_var env) s.Ty.ts_args
 	
 let specialize_fsymbol x env =
-  let s = find_fsymbol x env.env in
+  let s = find find_fsymbol x env.env in
   let tl, t = s.fs_scheme in
   let env = Htv.create 17 in
   s, List.map (specialize env) tl, specialize env t
 
 let specialize_psymbol x env =
-  let s = find_psymbol x env.env in
+  let s = find find_psymbol x env.env in
   let env = Htv.create 17 in
   s, List.map (specialize env) s.ps_scheme
 
+(** Typing types *)
+
+let qloc = function
+  | Qident x -> x.id_loc
+  | Qdot (m, x) -> Loc.join m.id_loc x.id_loc
+
+(* parsed types -> intermediate types *)
+let rec dty env = function
+  | PPTvarid {id=x} -> 
+      Tyvar (find_user_type_var x env)
+  | PPTexternal (p, x) ->
+      let loc = qloc x in
+      let s, tv = 
+	try specialize_tysymbol x env
+	with Not_found -> error ~loc:loc (UnboundType x);
+      in
+      let np = List.length p in
+      let a = List.length tv in
+      if np <> a then error ~loc (TypeArity (x, a, np));
+      Tyapp (s, List.map (dty env) p)
+
+(* intermediate types -> types *)
+let rec ty = function
+  | Tyvar { type_val = Some t } ->
+      ty t
+  | Tyvar { tvsymbol = tv } ->
+      Ty.ty_var tv
+  | Tyapp (s, tl) ->
+      Ty.ty_app s (List.map ty tl)
+
 (** Typing terms and formulas *)
 
 type dterm = { dt_node : dterm_node; dt_ty : dty }
@@ -280,13 +310,13 @@ let rec dterm env t =
   { dt_node = n; dt_ty = ty }
 
 and dterm_node loc env = function
-  | PPvar x ->
-      begin try
-	(* local variable *)
-	let ty = M.find x env.dvars in
-	Tvar x, ty
-      with Not_found -> try 
-	(* 0-arity symbol (constant) *)
+  | PPvar (Qident {id=x}) when M.mem x env.dvars ->
+      (* local variable *)
+      let ty = M.find x env.dvars in
+      Tvar x, ty
+  | PPvar x -> 
+      (* 0-arity symbol (constant) *)
+      begin try 
 	let s, tyl, ty = specialize_fsymbol x env in
 	let n = List.length tyl in
 	if n > 0 then error ~loc (BadNumberOfArguments (s.fs_name, 0, n));
@@ -318,14 +348,14 @@ and dfmla env e = match e.pp_desc with
       error ~loc:e.pp_loc PredicateExpected
   | PPif (a, b, c) ->
       Fif (dfmla env a, dfmla env b, dfmla env c)  
-  | PPforall (id, ty, _, a) -> (* TODO: triggers *)
+  | PPforall ({id=x}, ty, _, a) -> (* TODO: triggers *)
       let ty = dty env ty in
-      let env = { env with dvars = M.add id ty env.dvars } in
-      Fquant (Fforall, id, ty, dfmla env a)
-  | PPexists (id, ty, a) -> (* TODO: triggers *)
+      let env = { env with dvars = M.add x ty env.dvars } in
+      Fquant (Fforall, x, ty, dfmla env a)
+  | PPexists ({id=x}, ty, a) -> (* TODO: triggers *)
       let ty = dty env ty in
-      let env = { env with dvars = M.add id ty env.dvars } in
-      Fquant (Fexists, id, ty, dfmla env a)
+      let env = { env with dvars = M.add x ty env.dvars } in
+      Fquant (Fexists, x, ty, dfmla env a)
   | PPapp (x, tl) ->
       let s, tyl = 
 	try 
@@ -387,19 +417,19 @@ and fmla env = function
 open Ptree
 
 let add_type loc ext sl s env =
-  if M.mem s env.tysymbols then error ~loc (ClashType s);
+  if M.mem s.id env.tysymbols then error ~loc (ClashType s.id);
   let tyvars = ref M.empty in
-  let add_ty_var x =
+  let add_ty_var {id=x} =
     if M.mem x !tyvars then error ~loc (BadTypeArity x);
     let v = Name.from_string x in
     tyvars := M.add x v !tyvars;
     v
   in
   let vl = List.map add_ty_var sl in
-  let ty = Ty.create_tysymbol (Name.from_string s) vl None in
-  add_tysymbol s ty env
+  let ty = Ty.create_tysymbol (Name.from_string s.id) vl None in
+  add_tysymbol s.id ty env
 
-let add_function loc pl t env id =
+let add_function loc pl t env {id=id} =
   if M.mem id env.fsymbols then error ~loc (Clash id);
   let denv = create_denv env in
   let pl = List.map (dty denv) pl and t = dty denv t in
@@ -407,7 +437,7 @@ let add_function loc pl t env id =
   let s = create_fsymbol (Name.from_string id) (pl, t) false in
   { env with fsymbols = M.add id s env.fsymbols }
 
-let add_predicate loc pl env id =
+let add_predicate loc pl env {id=id} =
   if M.mem id env.psymbols then error ~loc (Clash id);
   let denv = create_denv env in
   let pl = List.map (dty denv) pl in
@@ -447,7 +477,12 @@ and add_decls env = List.fold_left add_decl env
 
 and add_theory loc s u dl env =
   assert (is_empty env);
-  if M.mem s env.theories then error ~loc (ClashTheory s);
+  if M.mem s.id env.theories then error ~loc:s.id_loc (ClashTheory s.id);
   let env = add_decls env dl in
-  { empty with theories = M.add s env env.theories }
+  { empty with theories = M.add s.id env env.theories }
 
+(*
+Local Variables: 
+compile-command: "make -C .. test"
+End: 
+*)