programs: logic/inductive in modules

parent 9f981b82
......@@ -36,10 +36,10 @@ module Array
logic ([]) (a: array 'a) (i :int) : 'a = get a.elts i
parameter ([]) : a:array 'a -> i:int ->
parameter get : a:array 'a -> i:int ->
{ 0 <= i < length a } 'a reads a { result = a[i] }
parameter ([<-]) : a:array 'a -> i:int -> v:'a ->
parameter set : a:array 'a -> i:int -> v:'a ->
{ 0 <= i < length a } unit writes a { a.elts = (old a.elts)[i <- v] }
parameter length : a:array 'a -> {} int { result = a.length }
......@@ -106,7 +106,7 @@ module TestArray
let test_append () =
let a1 = make 17 2 in
assert { a1[3] = 2 };
a1[3 <- 4];
set a1 3 4;
assert { a1[3] = 4 };
let a2 = make 25 3 in
assert { a2[0] = 3 }; (* needed to prove a[17]=3 below *)
......
......@@ -216,13 +216,13 @@ let use_export_theory uc th =
in
add_ns th.th_export uc
let add_impure_typedecl env d uc =
let add_impure_pdecl env ltm d uc =
{ uc with uc_impure =
Typing.add_decl env Mnm.empty uc.uc_impure (Ptree.TypeDecl d) }
Typing.add_decl env ltm uc.uc_impure d }
let add_effect_typedecl env d uc =
let add_effect_pdecl env ltm d uc =
{ uc with uc_effect =
Typing.add_decl env Mnm.empty uc.uc_effect (Ptree.TypeDecl d); }
Typing.add_decl env ltm uc.uc_effect d; }
let add_pure_pdecl env ltm d uc =
{ uc with uc_pure = Typing.add_decl env ltm uc.uc_pure d; }
......
......@@ -54,13 +54,16 @@ val add_impure_decl : Decl.decl -> uc -> uc
val add_effect_decl : Decl.decl -> uc -> uc
val add_pure_decl : Decl.decl -> uc -> uc
val add_impure_typedecl : Env.env -> Ptree.type_decl list -> uc -> uc
val add_effect_typedecl : Env.env -> Ptree.type_decl list -> uc -> uc
val add_impure_pdecl :
Env.env -> Theory.theory Theory.Mnm.t -> Ptree.decl -> uc -> uc
val add_effect_pdecl :
Env.env -> Theory.theory Theory.Mnm.t -> Ptree.decl -> uc -> uc
val add_pure_pdecl :
Env.env -> Theory.theory Theory.Mnm.t -> Ptree.decl -> uc -> uc
val add_pdecl :
Env.env -> Theory.theory Theory.Mnm.t -> Ptree.decl -> uc -> uc
(** add in impure, effect and pure *)
(** exceptions *)
......
......@@ -193,7 +193,7 @@ type iexpr = {
}
and iexpr_desc =
| IElogic of Term.term
| IElogic of Term.term (* pure *)
| IElocal of ivsymbol
| IEglobal of psymbol * itype_v
| IEapply of iexpr * ivsymbol
......
......@@ -438,7 +438,7 @@ and dexpr_desc ~ghost env loc = function
let tyv = specialize_type_v ~loc (Htv.create 17) tv in
DEglobal (ps, tyv), dpurify_type_v tyv
| PSlogic ->
let tyl, ty = Denv.specialize_lsymbol ~loc ps.ps_pure in
let tyl, ty = Denv.specialize_lsymbol ~loc ps.ps_impure in
let ty = match ty with
| Some ty -> ty
| None -> dty_bool env.uc
......@@ -945,7 +945,9 @@ let make_logic_app gl loc ty ls el =
let rec make args = function
| [] ->
begin match ls.ls_value with
| Some _ -> IElogic (t_app ls (List.rev args) (purify ty))
| Some _ ->
let t = t_app ls (List.rev args) (purify ty) in
IElogic t
| None -> IElogic (mk_t_if gl (f_app ls (List.rev args)))
end
| ({ iexpr_desc = IElogic t }, _) :: r ->
......@@ -1045,7 +1047,7 @@ and iexpr_desc gl env loc ty = function
| DElogic ls ->
begin match ls.ls_args, ls.ls_value with
| [], Some _ ->
IElogic (t_app ls [] ty)
IElogic (t_app ls [] (purify ty))
| [], None ->
IElogic (mk_t_if gl (f_app ls []))
| al, _ ->
......@@ -1063,7 +1065,8 @@ and iexpr_desc gl env loc ty = function
make_logic_app gl loc ty ls args
| _ ->
let f = iexpr gl env f in
(make_app gl loc ty f args).iexpr_desc
let e = make_app gl loc ty f args in
e.iexpr_desc
end
| DEfun (bl, e1) ->
let env, bl = map_fold_left (iubinder gl) env bl in
......@@ -1943,9 +1946,9 @@ let add_types env ltm uc dl =
{ d with td_params = params; td_model = false; td_def = def }
in
let dli = List.map (add_regions ~effect:false) dl in
let uc = Pgm_module.add_impure_typedecl env dli uc in
let uc = Pgm_module.add_impure_pdecl env ltm (Ptree.TypeDecl dli) uc in
let dle = List.map (add_regions ~effect:true) dl in
let uc = Pgm_module.add_effect_typedecl env dle uc in
let uc = Pgm_module.add_effect_pdecl env ltm (Ptree.TypeDecl dle) uc in
(* 4. add mtsymbols in module *)
let add_mt d =
let x = d.td_ident.id in
......@@ -2017,6 +2020,59 @@ let add_types env ltm uc dl =
List.iter (fun d -> visit d.td_ident.id) dl;
uc
let add_logics env ltm uc d =
let uc = Pgm_module.add_pure_pdecl env ltm d uc in
let region =
let c = ref (-1) in
fun loc ->
incr c; { id = "r" ^ string_of_int !c; id_lab = []; id_loc = loc }
in
let rec add_regions_to_type = function
| PPTtyvar _ as ty ->
ty
| PPTtyapp (tyl, q) ->
let loc = Typing.qloc q in
let p = Typing.string_list_of_qualid [] q in
let ts = ns_find_ts (get_namespace (impure_uc uc)) p in
let n = (get_mtsymbol ts).mt_regions in
let reg = ref [] in
for i = 1 to n do reg := PPTtyvar (region loc) :: !reg done;
PPTtyapp (List.rev !reg @ List.map add_regions_to_type tyl, q)
| PPTtuple tyl ->
PPTtuple (List.map add_regions_to_type tyl)
in
let add_param (x, ty) = (x, add_regions_to_type ty) in
let add_regions d =
{ d with
ld_params = List.map add_param d.ld_params;
ld_type = option_map add_regions_to_type d.ld_type;
ld_def = None; }
in
let add_ps uc d =
let x = d.ld_ident.id in
let get th = ns_find_ls (get_namespace th) [x] in
let impure = get (impure_uc uc) in
let effect = get (effect_uc uc) in
let pure = get (pure_uc uc) in
ignore (create_psymbol ~impure ~effect ~pure ~kind:PSlogic)
in
let add uc d0 =
let d = LogicDecl [add_regions d0] in
let uc = Pgm_module.add_impure_pdecl env ltm d uc in
let uc = Pgm_module.add_effect_pdecl env ltm d uc in
add_ps uc d0;
uc
in
let addi uc d =
add uc { ld_loc = d.in_loc; ld_ident = d.in_ident;
ld_params = List.map add_param d.in_params;
ld_type = None; ld_def = None; }
in
match d with
| LogicDecl dl -> List.fold_left add uc dl
| IndDecl dl -> List.fold_left addi uc dl
| Meta _ | UseClone _ | PropDecl _ | TypeDecl _ -> assert false
let find_module penv lmod q id = match q with
| [] ->
(* local module *)
......@@ -2121,8 +2177,7 @@ let rec decl ~wp env penv ltm lmod uc = function
| Ptree.Dlogic (TypeDecl d) ->
add_types env ltm uc d
| Ptree.Dlogic (LogicDecl _ | IndDecl _ as d) ->
Pgm_module.add_pure_pdecl env ltm d uc
(* TODO: add in impure and effect as well, with extra args for regions *)
add_logics env ltm uc d
| Ptree.Dlogic (PropDecl _ | Meta _ as d) ->
Pgm_module.add_pure_pdecl env ltm d uc
| Ptree.Dlogic (UseClone _ as d) ->
......
module M
logic d : int
type pointer model int
let test_cd3d () = d
logic null : pointer
parameter f : 'a -> 'a
let foo () = f null
end
(***
module TestRef
use import int.Int
......@@ -44,8 +49,6 @@ module TestRef
end
(***
module Array
type t
......
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