Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

debuggage typage

parent 4cebacb3
theory Test
type 'a t
type u = t
end
theory Test
type 'a t
type u = (int, int) t
end
theory Test
logic c : int
logic c : int
end
theory Test
type t = t
end
theory Test
type t = u
type u = t
end
theory Test
type 'a t = 'b
end
......@@ -99,6 +99,34 @@ theory Array
end
theory Set
type 'a t
logic mem ('a, 'a t)
logic empty : 'a t
axiom Empty_def1 : forall x : 'a. not mem(x, empty)
logic add ('a, 'a t) : 'a t
axiom Add_def1 :
forall x, y : 'a. forall s : 'a t.
mem(x, add(y, s)) <-> (x = y or mem(x, s))
logic union('a t, 'a t) : 'a t
axiom Union_def1 :
forall s1, s2 : 'a t. forall x : 'a.
mem(x, union(s1, s2)) <-> (mem(x, s1) or mem(x, s2))
logic equal(s1 : 'a t, s2 : 'a t) = forall x : 'a. mem(x, s1) <-> mem(x, s2)
end
(*
Local Variables:
compile-command: "make -C ../.. test"
......
theory Set
type 'a t
logic mem ('a , 'a t)
logic empty : 'a t
axiom empty_def1 : forall x:'a. not mem(x, empty)
logic add ('a, 'a t) : 'a t
axiom add_def1 : forall x,y:'a. forall s:'a t.
mem(x, add(y, s)) <-> (x = y or mem(x, s))
end
theory Set_list
use open List
logic add(x:'a,s:'a t) : 'a t = Cons(x,s)
......
......@@ -545,41 +545,21 @@ let add_types loc dl th =
let dl = List.map decl dl in
add_decl th (create_type dl)
(*
let add_function loc pl t th {id=id} =
let ns = get_namespace th in
if Mnm.mem id ns.ns_fs then error ~loc (Clash id);
let denv = create_denv th in
let pl = List.map (dty denv) pl and t = dty denv t in
let pl = List.map ty pl and t = ty t in
(* TODO: add the theory name to the long name *)
let v = id_user id loc in
let s = create_fsymbol v (pl, t) false in
add_decl th (create_logic [Lfunction (s, None)])
let add_predicate loc pl th {id=id} =
let ns = get_namespace th in
if Mnm.mem id ns.ns_ps then error ~loc (Clash id);
let denv = create_denv th in
let pl = List.map (dty denv) pl in
let pl = List.map ty pl in
(* TODO: add the theory name to the long name *)
let v = id_user id loc in
let s = create_psymbol v pl in
add_decl th (create_logic [Lpredicate (s, None)])
*)
let env_of_vsymbol_list vl =
List.fold_left (fun env v -> M.add v.vs_name.id_short v env) M.empty vl
let add_logics loc dl th =
let ns = get_namespace th in
let fsymbols = Hashtbl.create 17 in
let psymbols = Hashtbl.create 17 in
let denvs = Hashtbl.create 17 in
(* 1. create all symbols and make an environment with these symbols *)
let create_symbol th d =
let id = d.ld_ident.id in
if Hashtbl.mem denvs id || Mnm.mem id ns.ns_fs then error ~loc (Clash id);
let v = id_user id loc in
let denv = create_denv th in
Hashtbl.add denvs id denv;
let type_ty (_,t) = ty (dty denv t) in
let pl = List.map type_ty d.ld_params in
match d.ld_type with
......@@ -601,7 +581,9 @@ let add_logics loc dl th =
| None -> denv
| Some id -> { denv with dvars = M.add id.id (dty denv ty) denv.dvars }
in
let denv = List.fold_left dadd_var (create_denv th') d.ld_params in
let denv = Hashtbl.find denvs id in
let denv = { denv with th = th' } in
let denv = List.fold_left dadd_var denv d.ld_params in
let create_var (x, _) ty =
let id = match x with
| None -> id_fresh "%x"
......@@ -622,16 +604,22 @@ let add_logics loc dl th =
let env = env_of_vsymbol_list vl in
make_pdef ps vl (fmla env f)
end
| Some _ -> (* function *)
| Some ty -> (* function *)
let fs = Hashtbl.find fsymbols id in
begin match d.ld_def with
| None ->
Lfunction (fs, None)
| Some t ->
let loc = t.pp_loc in
let t = dterm denv t in
let vl = mk_vlist (fst fs.fs_scheme) in
let env = env_of_vsymbol_list vl in
make_fdef fs vl (term env t)
try
make_fdef fs vl (term env t)
with _ ->
error ~loc (TermExpectedType
((fun f -> print_dty f t.dt_ty),
(fun f -> print_dty f (dty denv ty))))
end
in
let dl = List.map type_decl dl in
......
(* test file *)
theory Test
logic id(x:'a) : 'a = x
end
theory TestPrelude
use prelude.Int
use prelude.List
......@@ -8,11 +12,13 @@ end
theory A
use import prelude.Int
type t
logic p(t)
logic q(x: t) = p(x)
logic c : int = 42
logic c' : real = 42.5
logic c : int
type 'a t
logic mem('a, 'a t)
logic p(s : 'a t) = forall x:'a. mem(x, s)
end
theory B
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment