make bench

bench/typing/bad/already_theory2.why

 theory A end
 theory B end
-theory C use A use A:B end
+theory C use A use B as A end

bench/typing/bad/clash_axiom1.why

+
+(* test file *)
+
+theory A
+  type t
+  axiom Ax : forall x:t. true
+end
+
+theory B
+  use export A
+  axiom Ax : true
+end
+

bench/typing/bad/clash_namespace1.why

+
+(* test file *)
+
+theory A
+  type t
+  axiom Ax : forall x:t. true
+end
+
+theory B
+  use A
+  use A
+end
+

src/core/theory.ml

@@ -145,8 +145,13 @@ let close_namespace uc n ~import =
   match uc.uc_visible, uc.uc_import, uc.uc_export with
   | v0 :: v1 :: stv, i0 :: i1 :: sti, e0 :: e1 :: ste ->
       let s = n.id_short in
-      let add ns1 ns2 = { ns2 with namespace = M.add s ns1 ns2.namespace } in
-      let v1 = add v0 v1 and i1 = add i0 i1 and e1 = add e0 e1 in
+      let add ~check ns1 ns2 = 
+	if check && M.mem s ns2.namespace then raise (ClashSymbol s);
+	{ ns2 with namespace = M.add s ns1 ns2.namespace } 
+      in
+      let v1 = add ~check:false v0 v1 in
+      let i1 = add ~check:true  i0 i1 in
+      let e1 = add ~check:false e0 e1 in
       let v1 = if import then fusion ~check:false v0 v1 else v1 in
       let i1 = if import then fusion ~check:true  i0 i1 else i1 in
       add_known n 
@@ -200,6 +205,9 @@ let clone_export th t i =
   Mps.iter check_ps i.inst_ps;
   assert false (* TODO *)
 
+let check_fmla k f =
+  () (* TODO *)
+
 let generic_add ~check x v m =
   if check && M.mem x m then raise (ClashSymbol x);
   M.add x v m
@@ -210,6 +218,8 @@ let add_fsymbol ~check x ty ns =
   { ns with fsymbols = generic_add ~check x ty ns.fsymbols }
 let add_psymbol ~check x ty ns = 
   { ns with psymbols = generic_add ~check x ty ns.psymbols }
+let add_prop ~check x v ns =
+  { ns with props = generic_add ~check x v ns.props }
 
 let add_symbol add x v uc = 
   match uc.uc_visible, uc.uc_import, uc.uc_export with
@@ -238,6 +248,10 @@ let add_decl uc d =
     | Dlogic [Lpredicate (ps, None)] ->
         let uc = add_param ps.ps_name uc in
         add_symbol add_psymbol ps.ps_name ps uc
+    | Dprop (k, id, f) ->
+	check_fmla uc.uc_known f;
+	let uc = add_known id uc in
+	add_symbol add_prop id f uc
     | _ ->
         assert false (* TODO *)
   in

src/parser/typing.ml

@@ -512,9 +512,12 @@ let term env t =
   let t = dterm denv t in
   term M.empty t
 
-let axiom loc s f env =
-  ignore (fmla env f);
-  env
+let add_prop k loc s f th =
+  let f = fmla th f in
+  try
+    add_decl th (Dprop (k, id_user s.id s.id loc, f))
+  with ClashSymbol _ ->
+    error ~loc (Clash s.id)
 
 let find_in_loadpath env f =
   let rec find c lp = match lp, c with
@@ -606,7 +609,7 @@ and add_decl env th = function
   | Logic (loc, ids, PFunction (pl, t)) ->
       List.fold_left (add_function loc pl t) th ids
   | Axiom (loc, s, f) ->
-      axiom loc s f th
+      add_prop Theory.Axiom loc s f th
   | Use (loc, use) ->
       let t = find_theory env use.use_theory in
       let n = match use.use_as with 

src/test.why

@@ -3,9 +3,11 @@
 
 theory A
   type t
+  axiom Ax : forall x:t. true
 end
 
 theory B
-  type t
+  use A
   use A
 end
+