Commit 1a1d2bea authored by MARCHE Claude's avatar MARCHE Claude

Jessie3: preliminary support for generic types

parent 6673640c
...@@ -74,6 +74,24 @@ let ctype ty = ...@@ -74,6 +74,24 @@ let ctype ty =
let logic_types = Hashtbl.create 257 let logic_types = Hashtbl.create 257
let type_vars = ref []
let find_type_var v =
try
List.assoc v !type_vars
with Not_found -> Self.fatal "type variable %s not found" v
let push_type_var v =
let tv = Ty.create_tvsymbol (Ident.id_fresh v) in
type_vars := (v,tv) :: !type_vars
let pop_type_var v =
match !type_vars with
| (w,_) :: r ->
if v=w then type_vars := r
else Self.fatal "pop_type_var: %s expected,found %s" v w
| [] -> Self.fatal "pop_type_var: empty"
let rec logic_type ty = let rec logic_type ty =
match ty with match ty with
| Linteger -> int_type | Linteger -> int_type
...@@ -85,7 +103,7 @@ let rec logic_type ty = ...@@ -85,7 +103,7 @@ let rec logic_type ty =
Ty.ty_app ts (List.map logic_type args) Ty.ty_app ts (List.map logic_type args)
with Not_found -> Self.fatal "logic type %s not found" lt.lt_name with Not_found -> Self.fatal "logic type %s not found" lt.lt_name
end end
| Lvar _ | Lvar v -> Ty.ty_var (find_type_var v)
| Ctype _ | Ctype _
| Larrow (_, _) -> | Larrow (_, _) ->
Self.not_yet_implemented "logic_type" Self.not_yet_implemented "logic_type"
...@@ -302,18 +320,27 @@ let rec annot ~in_axiomatic a _loc (theories,decls) = ...@@ -302,18 +320,27 @@ let rec annot ~in_axiomatic a _loc (theories,decls) =
(theories,d::decls) (theories,d::decls)
| Dfun_or_pred (li, _loc) -> | Dfun_or_pred (li, _loc) ->
begin begin
match li.l_labels, li.l_tparams,li.l_body with match li.l_labels with
| [],[],LBnone -> | [] ->
let ls,_ = create_lsymbol li in List.iter push_type_var li.l_tparams;
(theories,Decl.create_param_decl ls :: decls) let d =
| [],[],LBterm d -> match li.l_body with
let ls,args = create_lsymbol li in | LBnone ->
let (_ty,d) = term d in let ls,_ = create_lsymbol li in
let def = Decl.make_ls_defn ls args d in Decl.create_param_decl ls
(theories,Decl.create_logic_decl [def] :: decls) | LBterm d ->
let ls,args = create_lsymbol li in
let (_ty,d) = term d in
let def = Decl.make_ls_defn ls args d in
Decl.create_logic_decl [def]
| _ ->
Self.not_yet_implemented "Dfun_or_pred, other bodies"
in
List.iter pop_type_var (List.rev li.l_tparams);
(theories,d :: decls)
| _ -> | _ ->
Self.not_yet_implemented "Dfun_or_pred with labels or vars" Self.not_yet_implemented "Dfun_or_pred with labels"
end end
| Dlemma(name,is_axiom,labels,vars,p,loc) -> | Dlemma(name,is_axiom,labels,vars,p,loc) ->
begin begin
......
/* run.config
OPT: -journal-disable -jessie3
*/
/*@ axiomatic Bag { /*@ axiomatic Bag {
@ type bag<X>; @ type bag<X>;
@ // logic integer occ<X>(<X> x, bag<X> b); @ logic integer occ<X>(X x, bag<X> b);
@ // axiom extensionality<X>: \forall bag<X> b1,b2; @ // axiom extensionality<X>: \forall bag<X> b1,b2;
@ // (\forall <X> x, occ(x,b1) == occ(x,b2)) ==> b1 == b2; @ // (\forall X x; occ(x,b1) == occ(x,b2)) ==> b1 == b2;
@ // logic bag<X> singleton<X>(<X> x); @ logic bag<X> empty<X>;
@ // axiom occ_singleton_eq<X>: \forall <X> x; @
@ // occ(x,singleton(x)) == 1; @ logic bag<X> singleton<X>(X x);
@ // axiom occ_singleton_neq<X>: \forall <X> x,y; @ // axiom occ_singleton_eq<X>: \forall X x;
@ // x != y ==> occ(x,singleton(y)) == 0; @ // occ(x,singleton(x)) == 1;
@ // logic bag<X> bag_union<X>(bag<X> b1,bag<X> b2); @ // axiom occ_singleton_neq<X>: \forall X x,y;
@ // axiom occ_union<X>: \forall <X> x, bag<X> b1,b2; @ // x != y ==> occ(x,singleton(y)) == 0;
@ // occ(x,union(b1,b2)) == occ(x,b1) + occ(x,b2); @ logic bag<X> bag_union<X>(bag<X> b1,bag<X> b2);
@ lemma l2: f1(1) == 2; @ // axiom occ_union<X>: \forall X x, bag<X> b1,b2;
@ // occ(x,bag_union(b1,b2)) == occ(x,b1) + occ(x,b2);
@ } @ }
@*/ @*/
/*
Local Variables:
compile-command: "frama-c -add-path ../.. -jessie3 generic.c"
End:
*/
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