- Denv.specialize keeps labels

- programs: labelled annotations and labelled WPs
- ide: color labels in source view

src/ide/gmain.ml

@@ -874,9 +874,12 @@ let move_to_line (v : GSourceView2.source_view) line =
 let orange_bg = source_view#buffer#create_tag 
   ~name:"orange_bg" [`BACKGROUND "orange"] 
 
+let erase_color_loc (v:GSourceView2.source_view) =
+  let buf = v#buffer in
+  buf#remove_tag orange_bg ~start:buf#start_iter ~stop:buf#end_iter
+
 let color_loc (v:GSourceView2.source_view) l b e =
   let buf = v#buffer in
-  buf#remove_tag orange_bg ~start:buf#start_iter ~stop:buf#end_iter;
   let top = buf#start_iter in
   let start = top#forward_lines (l-1) in
   let start = start#forward_chars b in
@@ -893,6 +896,7 @@ let scroll_to_id id =
 	    current_file := f;
 	  end;
 	move_to_line source_view (l-1);
+	erase_color_loc source_view;
 	color_loc source_view l b e
     | Ident.Fresh -> 
 	source_view#source_buffer#set_text "Fresh ident (no position available)\n";
@@ -901,10 +905,33 @@ let scroll_to_id id =
 	source_view#source_buffer#set_text "Derived ident (no position available)\n";
 	current_file := ""
 
+let color_label = function
+  | _, Some loc when (fst loc).Lexing.pos_fname = !current_file ->
+      let _, l, b, e = Loc.extract loc in
+      color_loc source_view l b e
+  | _ ->
+      ()
+
+let rec color_f_labels () f =
+  List.iter color_label f.Term.f_label;
+  Term.f_fold color_t_labels color_f_labels () f
+
+and color_t_labels () t =
+  List.iter color_label t.Term.t_label;
+  Term.t_fold color_t_labels color_f_labels () t
+
 let scroll_to_source_goal g =
   let t = g.Model.task in
   let id = (Task.task_goal t).Decl.pr_name in
-  scroll_to_id id
+  scroll_to_id id;
+  match t with
+    | Some 
+	{ Task.task_decl = 
+	    { Theory.td_node = 
+		Theory.Decl { Decl.d_node = Decl.Dprop (Decl.Pgoal, _, f) }}} ->
+	color_f_labels () f
+    | _ ->
+	assert false
 
 let scroll_to_theory th = 
   let t = th.Model.theory in

src/parser/denv.ml

@@ -296,10 +296,12 @@ and specialize_pattern_node ~loc htv = function
       Por (specialize_pattern ~loc htv p, specialize_pattern ~loc htv q)
 
 let rec specialize_term ~loc htv t =  
-  { dt_node = specialize_term_node  ~loc htv t.t_node;
-    dt_ty   = specialize_ty         ~loc htv t.t_ty; }
+  let dt = 
+    { dt_node = specialize_term_node  ~loc htv t.t_node;
+      dt_ty   = specialize_ty         ~loc htv t.t_ty; }
+  in
+  List.fold_left (fun t l -> { t with dt_node = Tnamed (l, t) }) dt t.t_label
 
-(* TODO: labels are lost *)
 and specialize_term_node ~loc htv = function
   | Term.Tbvar _ ->
       assert false
@@ -327,7 +329,11 @@ and specialize_term_node ~loc htv = function
 	    specialize_fmla ~loc htv f)
 
 (* TODO: labels are lost *)
-and specialize_fmla ~loc htv f = match f.f_node with
+and specialize_fmla ~loc htv f = 
+  let df = specialize_fmla_node ~loc htv f.f_node in
+  List.fold_left (fun f l -> Fnamed (l, f)) df f.f_label
+
+and specialize_fmla_node ~loc htv = function
   | Term.Fapp (ls, tl) ->
       Fapp (ls, List.map (specialize_term ~loc htv) tl)
   | Term.Fquant (q, fq) ->

src/programs/pgm_env.ml

@@ -174,9 +174,12 @@ let parse_string f loc s =
   reloc loc lb;
   f lb
 
-let logic_lexpr (loc, s) = parse_string Lexer.parse_lexpr loc s
+let logic_lexpr ((pos, _) as loc, s) = 
+  let e = parse_string Lexer.parse_lexpr pos s in
+  let lab = Ident.label ~loc "annotation" in
+  { e with Ptree.pp_desc = Ptree.PPnamed (lab, e) }
 
-let logic_decls (loc, s) e env =
+let logic_decls ((loc, _), s) e env =
   let parse = Lexer.parse_list0_decl e Mnm.empty env.uc in
   { env with uc = parse_string parse loc s }
 

src/programs/pgm_env.mli

@@ -64,9 +64,9 @@ val add_global : preid -> type_v -> env -> lsymbol * env
 
 val add_decl : decl -> env -> env
 
-val logic_lexpr : Lexing.position * string -> Ptree.lexpr
+val logic_lexpr : Loc.position * string -> Ptree.lexpr
 
-val logic_decls : Lexing.position * string -> Env.env -> env -> env
+val logic_decls : Loc.position * string -> Env.env -> env -> env
 
 val add_exception : preid -> ty option -> env -> lsymbol * env
 

src/programs/pgm_lexer.mll

@@ -185,10 +185,10 @@ rule token = parse
   | "{"
       { logic_start_loc := loc lexbuf; 
 	let s = logic lexbuf in
-	LOGIC (fst !logic_start_loc, s) }
+	LOGIC ((fst !logic_start_loc, snd (loc lexbuf)), s) }
   (* FIXME: allow newlines as well *)
   | "{" space* "}"
-      { LOGIC (lexeme_start_p lexbuf, "true") }
+      { LOGIC (loc lexbuf, "true") }
   | "{{"
       { LEFTBLEFTB }
   | "}}"

src/programs/pgm_parser.mly

@@ -88,8 +88,8 @@
 
   let ty_unit () = Tpure (PPTtyapp ([], Qident (id_unit ())))
 
-  let lexpr_true () = symbol_start_pos (), "true"
-  let lexpr_false () = symbol_start_pos (), "false"
+  let lexpr_true () = loc (), "true"
+  let lexpr_false () = loc (), "false"
 
   let empty_effect = { pe_reads = []; pe_writes = []; pe_raises = [] }
 
@@ -112,7 +112,7 @@
 %token <string> OP1 OP2 OP3 OP4 OPPREF
 %token <Why.Ptree.real_constant> REAL
 %token <string> STRING
-%token <Lexing.position * string> LOGIC
+%token <Why.Loc.position * string> LOGIC
 
 /* keywords */
 

src/programs/pgm_ptree.ml

@@ -31,7 +31,7 @@ type assertion_kind = Aassert | Aassume | Acheck
 
 type lazy_op = LazyAnd | LazyOr
 
-type logic = Lexing.position * string
+type logic = Loc.position * string
 
 type lexpr = logic
 

src/programs/pgm_wp.ml

@@ -258,7 +258,8 @@ let rec wp_expr env e q =
   let lab = fresh_label env in
   let q = post_map (old_label env lab) q in
   let f = wp_desc env e q in
-  erase_label env lab f
+  let f = erase_label env lab f in
+  f_label [label ~loc:e.expr_loc "WP-loc"] f
 
 and wp_desc env e q = match e.expr_desc with
   | Elogic t ->

tests/test-jcf.why

@@ -4,7 +4,7 @@
 theory Test
   use import int.Int
   logic (*) int int
-  goal G : forall x:int. 1 * 2 -> x * 3
+  goal G : forall x : int. 1 * 2 -> x * 3
 end