mirror of
https://github.com/ProgramSnail/pass_strategy_synthesis.git
synced 2026-06-11 03:38:15 +00:00
struct: part sythesizer functions + some minor (mostly stylistic) analyzer corrections
This commit is contained in:
ProgramSnail
parent
b31415cf8e
commit
3e61eb3204
2 changed files with 480 additions and 53 deletions
|
|
@ -91,6 +91,14 @@ struct
|
|||
| x :: xs, _ -> x :: list_replace xs (id - 1) y
|
||||
| [], _ -> raise Not_found
|
||||
|
||||
(* TODO: FIXME: check if this foldl or foldr *)
|
||||
let rec list_foldl3 f (acc : 'a) (xs : 'b list) (ys : 'c list) (zs : 'd list) : 'a = match xs, ys, zs with
|
||||
| x :: xs, y :: ys, z :: zs -> list_foldl3 f (f acc x y z) xs ys zs
|
||||
| [], [], [] -> acc
|
||||
| _, _, _ -> raise Cant_fold3_error
|
||||
|
||||
(* --- *)
|
||||
|
||||
(* NOTE: old variant with assoc array *)
|
||||
(* let mem_get (mem : mem) (id : memid) : value = List.assoc id (fst mem) *)
|
||||
(* let mem_add (mem : mem) (v : value) : mem * memid = *)
|
||||
|
|
@ -147,31 +155,32 @@ struct
|
|||
|
||||
(* --- eval rules --- *)
|
||||
|
||||
(* TODO: FIXME: check if this foldl or foldr *)
|
||||
let rec list_foldl3 f (acc : 'a) (xs : 'b list) (ys : 'c list) (zs : 'd list) : 'a = match xs, ys, zs with
|
||||
| x :: xs, y :: ys, z :: zs -> list_foldl3 f (f acc x y z) xs ys zs
|
||||
| [], [], [] -> acc
|
||||
| _, _, _ -> raise Cant_fold3_error
|
||||
|
||||
(* - value construction *)
|
||||
|
||||
let rec valcopy (mem : mem) (v : value) (t : atype) : mem * value = match t, v with
|
||||
| UnitT (Rd, w), ZeroV -> (mem, v)
|
||||
| UnitT (Rd, w), SmthV -> (mem, v)
|
||||
| UnitT (Rd, w), BotV -> (mem, v)
|
||||
| UnitT (NRd, w), ZeroV -> (mem, BotV)
|
||||
| UnitT (NRd, w), SmthV -> (mem, BotV)
|
||||
| UnitT (NRd, w), BotV -> (mem, BotV)
|
||||
let rec valcopy (mem : mem) (v : value) (t : atype) : mem * value =
|
||||
if is_trivial_v v
|
||||
then match t with
|
||||
| UnitT (Rd, _) -> (mem, v)
|
||||
| UnitT (NRd, _) -> (mem, BotV)
|
||||
| _ -> raise @@ Typing_error "valcopy: trivial value, wrong type"
|
||||
else match t, v with
|
||||
(* NOTE: replaced with if | best choice ?? *)
|
||||
(* | UnitT (Rd, w), ZeroV -> (mem, v) *)
|
||||
(* | UnitT (Rd, w), SmthV -> (mem, v) *)
|
||||
(* | UnitT (Rd, w), BotV -> (mem, v) *)
|
||||
(* | UnitT (NRd, w), ZeroV -> (mem, BotV) *)
|
||||
(* | UnitT (NRd, w), SmthV -> (mem, BotV) *)
|
||||
(* | UnitT (NRd, w), BotV -> (mem, BotV) *)
|
||||
| FunT _, FunV _ -> (mem, v)
|
||||
| RefT (Rf, _), RefV _ -> (mem, v)
|
||||
| RefT (Cp, t), RefV id -> let (mem', v') = valcopy mem (mem_get mem id) t in
|
||||
let (mem'', id'') = mem_add mem' v' in
|
||||
(mem'', RefV id'')
|
||||
| TupleT ts, TupleV vs -> let folder = fun (mem, vs') v t -> let (mem', v') = valcopy mem v t in
|
||||
mem, v' :: vs' in
|
||||
(mem, v' :: vs') in
|
||||
let mem', vs' = List.fold_left2 folder (mem, []) vs ts in
|
||||
(mem', TupleV vs')
|
||||
| _, _ -> raise @@ Typing_error "valcopy"
|
||||
| _, _ -> raise @@ Typing_error "valcopy: not trivial value, wrong type"
|
||||
|
||||
(* - value update *)
|
||||
|
||||
|
|
@ -189,7 +198,7 @@ struct
|
|||
if is_trivial_v u && is_trivial_v v
|
||||
then (if u == v then u else BotV)
|
||||
else match u, v with
|
||||
| FunV ustmts, FunV vstmts -> FunV (ustmts @ vstmts)
|
||||
| FunV ustmts, FunV vstmts -> FunV (ustmts @ vstmts)
|
||||
| RefV a, RefV b -> if a == b then u else raise @@ Typing_error "valcomb: ref"
|
||||
| TupleV us, TupleV vs -> TupleV (List.map2 valcomb us vs)
|
||||
| _, _ -> raise @@ Typing_error "valcomb"
|
||||
|
|
@ -317,7 +326,6 @@ struct
|
|||
(mem'', (x, t) :: types, (x, id) :: vals)
|
||||
|
||||
(* - function evaluation *)
|
||||
|
||||
(* NOTE: not needed due to performed optimization in stmt_eval *)
|
||||
(* let func_eval (mem : mem) (vals : vals) (s : stmt) (ts : mtype list) (es : expr list) = *)
|
||||
|
||||
|
|
@ -368,15 +376,15 @@ struct
|
|||
then raise @@ Eval_error "choice"
|
||||
else (memcomb meml memr, typesl, valsl)
|
||||
|
||||
(* --- program execution --- *)
|
||||
(* --- program execution --- *)
|
||||
|
||||
let prog_eval (prog : prog) : state =
|
||||
match prog with (decls, s) ->
|
||||
let init_state = prog_init prog in
|
||||
stmt_eval init_state s
|
||||
let prog_eval (prog : prog) : state =
|
||||
match prog with (decls, s) ->
|
||||
let init_state = prog_init prog in
|
||||
stmt_eval init_state s
|
||||
|
||||
let prog_eval_noret (prog : prog) : unit =
|
||||
ignore @@ prog_eval prog
|
||||
let prog_eval_noret (prog : prog) : unit =
|
||||
ignore @@ prog_eval prog
|
||||
|
||||
(* --- tests --- *)
|
||||
|
||||
|
|
|
|||
|
|
@ -145,16 +145,16 @@ struct
|
|||
module Decl = struct
|
||||
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
|
||||
[%%ocanren_inject
|
||||
type nonrec ('d, 't, 'e, 'dl, 'mtl, 's) t = VarD of 'd * 't * 'e | FunD of 'd * 'dl * 'mtl * 's
|
||||
type nonrec ((* 'd, *) 't, 'e, 'dl, 'mtl, 's) t = VarD of (* 'd * *) 't * 'e | FunD of (* 'd * *) 'dl * 'mtl * 's
|
||||
[@@deriving gt ~options:{ show; gmap }]
|
||||
type ground = (Nat.ground, Type.ground, Expr.ground, Nat.ground List.ground, (Mode.ground * Type.ground) List.ground, Stmt.ground) t
|
||||
type ground = ((* Nat.ground, *) Type.ground, Expr.ground, Nat.ground List.ground, (Mode.ground * Type.ground) List.ground, Stmt.ground) t
|
||||
]
|
||||
end
|
||||
|
||||
module Prog = struct
|
||||
module Prg = struct
|
||||
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
|
||||
[%%ocanren_inject
|
||||
type nonrec ('dl, 's) t = Prog of 'dl * 's
|
||||
type nonrec ('dl, 's) t = Prg of 'dl * 's
|
||||
[@@deriving gt ~options:{ show; gmap }]
|
||||
type nonrec ground = (Decl.ground List.ground, Stmt.ground) t
|
||||
]
|
||||
|
|
@ -173,39 +173,39 @@ struct
|
|||
|
||||
(* --- *)
|
||||
|
||||
module Mem = struct
|
||||
module MemEnv = struct
|
||||
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
|
||||
[%%ocanren_inject
|
||||
type nonrec ('vl, 'd) t = Mem of 'vl * 'd
|
||||
type nonrec ('vl, 'd) t = MemEnv of 'vl * 'd
|
||||
[@@deriving gt ~options:{ show; gmap }]
|
||||
type nonrec ground = (Value.ground List.ground, Nat.ground) t
|
||||
]
|
||||
end
|
||||
|
||||
module Types = struct
|
||||
module TypesEnv = struct
|
||||
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
|
||||
[%%ocanren_inject
|
||||
type nonrec 'dtl t = Types of 'dtl
|
||||
type nonrec 'dtl t = TypesEnv of 'dtl
|
||||
[@@deriving gt ~options:{ show; gmap }]
|
||||
type nonrec ground = ((Nat.ground * Type.ground) List.ground) t
|
||||
]
|
||||
end
|
||||
|
||||
module Vals = struct
|
||||
module ValsEnv = struct
|
||||
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
|
||||
[%%ocanren_inject
|
||||
type nonrec 'ddl t = Vals of 'ddl
|
||||
type nonrec 'ddl t = ValsEnv of 'ddl
|
||||
[@@deriving gt ~options:{ show; gmap }]
|
||||
type nonrec ground = ((Nat.ground * Nat.ground) List.ground) t
|
||||
]
|
||||
end
|
||||
|
||||
module St = struct
|
||||
module StEnv = struct
|
||||
[@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
|
||||
[%%ocanren_inject
|
||||
type nonrec ('mem, 'types, 'vals) t = St of 'mem * 'types * 'vals
|
||||
type nonrec ('mem, 'types, 'vals) t = StEnv of 'mem * 'types * 'vals
|
||||
[@@deriving gt ~options:{ show; gmap }]
|
||||
type nonrec ground = (Mem.ground, Types.ground, Vals.ground) t
|
||||
type nonrec ground = (MemEnv.ground, TypesEnv.ground, ValsEnv.ground) t
|
||||
]
|
||||
end
|
||||
|
||||
|
|
@ -238,30 +238,449 @@ struct
|
|||
list_ntho xs' id' x' }
|
||||
}
|
||||
|
||||
let mem_geto mem id v = ocanren {
|
||||
fresh mem_data, mem_len, rev_id in
|
||||
Std.pair mem_data mem_len == mem &
|
||||
Nat.addo (Nat.s rev_id) id mem_len &
|
||||
list_ntho mem_data rev_id v
|
||||
|
||||
let rec list_foldlo f acc xs acc' = ocanren {
|
||||
xs == [] & acc' == acc |
|
||||
{ fresh x', xs', acc_upd in
|
||||
xs == x' :: xs' &
|
||||
list_foldlo f acc xs' acc_upd &
|
||||
f acc_upd x' acc' }
|
||||
}
|
||||
|
||||
let mem_addo mem v mem_with_id' = ocanren {
|
||||
fresh mem_data, mem_len, mem' in
|
||||
Std.pair mem_data mem_len == mem &
|
||||
mem' == Std.pair (v :: mem_data) (Nat.s mem_len) &
|
||||
Std.pair mem' mem_len == mem_with_id'
|
||||
let rec list_foldro f acc xs acc' = ocanren {
|
||||
xs == [] & acc' == acc |
|
||||
{ fresh x', xs', acc_upd in
|
||||
xs == x' :: xs' &
|
||||
f acc x' acc_upd &
|
||||
list_foldro f acc_upd xs' acc' }
|
||||
(* TODO: inf search on swap, investigate *)
|
||||
}
|
||||
|
||||
let mem_seto mem id v mem' = ocanren {
|
||||
fresh mem_data, mem_len, rev_id, mem_data' in
|
||||
Std.pair mem_data mem_len == mem &
|
||||
Nat.addo (Nat.s rev_id) id mem_len &
|
||||
list_replaceo mem_data rev_id v mem_data' &
|
||||
Std.pair mem_data' mem_len == mem'
|
||||
|
||||
let rec list_foldr2o f acc xs ys acc' = ocanren {
|
||||
xs == [] & ys == [] & acc' == acc |
|
||||
{ fresh x', xs', y', ys', acc_upd in
|
||||
xs == x' :: xs' &
|
||||
ys == y' :: ys' &
|
||||
f acc x' y' acc_upd &
|
||||
list_foldr2o f acc_upd xs' ys' acc' }
|
||||
}
|
||||
|
||||
let rec list_foldl2o f acc xs ys acc' = ocanren {
|
||||
xs == [] & ys == [] & acc' == acc |
|
||||
{ fresh x', xs', y', ys', acc_upd in
|
||||
xs == x' :: xs' &
|
||||
ys == y' :: ys' &
|
||||
list_foldl2o f acc xs' ys' acc_upd &
|
||||
f acc_upd x' y' acc' }
|
||||
}
|
||||
|
||||
let rec list_foldr3o f acc xs ys zs acc' = ocanren {
|
||||
xs == [] & ys == [] & zs == [] & acc' == acc |
|
||||
{ fresh x', xs', y', ys', z', zs', acc_upd in
|
||||
xs == x' :: xs' &
|
||||
ys == y' :: ys' &
|
||||
zs == z' :: zs' &
|
||||
f acc x' y' z' acc_upd &
|
||||
list_foldr3o f acc_upd xs' ys' zs' acc' }
|
||||
}
|
||||
|
||||
let rec list_foldl3o f acc xs ys zs acc' = ocanren {
|
||||
xs == [] & ys == [] & zs == [] & acc' == acc |
|
||||
{ fresh x', xs', y', ys', z', zs', acc_upd in
|
||||
xs == x' :: xs' &
|
||||
ys == y' :: ys' &
|
||||
zs == z' :: zs' &
|
||||
list_foldl3o f acc xs' ys' zs' acc_upd &
|
||||
f acc_upd x' y' z' acc' }
|
||||
}
|
||||
|
||||
let rec list_zip_witho f xs ys zs = ocanren {
|
||||
{ fresh x, xs', y, ys', z, zs' in
|
||||
xs == x :: xs' &
|
||||
ys == y :: ys' &
|
||||
zs == z :: zs' &
|
||||
f x y z &
|
||||
list_zip_witho f xs' ys' zs' } |
|
||||
{ fresh x, xs' in
|
||||
xs == x :: xs' &
|
||||
ys == [] &
|
||||
zs == [] } |
|
||||
{ fresh y, ys' in
|
||||
xs == [] &
|
||||
ys == y :: ys' &
|
||||
zs == [] } |
|
||||
{ xs == [] & ys == [] & zs == [] }
|
||||
}
|
||||
|
||||
(* --- *)
|
||||
|
||||
let mem_geto mem id v =
|
||||
let open MemEnv in
|
||||
ocanren {
|
||||
fresh mem_data, mem_len, rev_id in
|
||||
MemEnv (mem_data, mem_len) == mem &
|
||||
Nat.addo (Nat.s rev_id) id mem_len &
|
||||
list_ntho mem_data rev_id v
|
||||
}
|
||||
|
||||
let mem_addo mem v mem_with_id' =
|
||||
let open MemEnv in
|
||||
ocanren {
|
||||
fresh mem_data, mem_len, mem' in
|
||||
MemEnv (mem_data, mem_len) == mem &
|
||||
mem' == MemEnv (v :: mem_data, Nat.s mem_len) &
|
||||
Std.pair mem' mem_len == mem_with_id'
|
||||
}
|
||||
|
||||
let mem_seto mem id v mem' =
|
||||
let open MemEnv in
|
||||
ocanren {
|
||||
fresh mem_data, mem_len, rev_id, mem_data' in
|
||||
MemEnv (mem_data, mem_len) == mem &
|
||||
Nat.addo (Nat.s rev_id) id mem_len &
|
||||
list_replaceo mem_data rev_id v mem_data' &
|
||||
MemEnv (mem_data', mem_len) == mem'
|
||||
}
|
||||
|
||||
let is_trivial_vo v =
|
||||
let open Value in
|
||||
ocanren {
|
||||
v == ZeroV | v == SmthV | v == BotV
|
||||
}
|
||||
|
||||
let rec pathvaro p x =
|
||||
let open Path in
|
||||
ocanren {
|
||||
p == VarP x |
|
||||
{ fresh p' in p == DerefP p' & pathvaro p' x } |
|
||||
{ fresh p', _id in p == AccessP (p', _id) & pathvaro p' x }
|
||||
}
|
||||
|
||||
let types_assoco id types tp =
|
||||
let open TypesEnv in
|
||||
ocanren {
|
||||
fresh tps in
|
||||
types == TypesEnv tps &
|
||||
List.assoco id tps tp
|
||||
}
|
||||
|
||||
let vals_assoco id vals v =
|
||||
let open ValsEnv in
|
||||
ocanren {
|
||||
fresh vs in
|
||||
vals == ValsEnv vs &
|
||||
List.assoco id vs v
|
||||
}
|
||||
|
||||
let rec pathtypeo types p tp =
|
||||
let open Path in
|
||||
let open Type in
|
||||
ocanren {
|
||||
{ fresh x in
|
||||
p == VarP x &
|
||||
types_assoco x types tp } |
|
||||
{ fresh p', tp', _c in
|
||||
p == DerefP p' &
|
||||
pathtypeo types p' tp' &
|
||||
tp' == RefT (_c, tp) } |
|
||||
{ fresh p', id', tp', tps in
|
||||
p == AccessP (p', id') &
|
||||
pathtypeo types p' tp' &
|
||||
tp' == TupleT tps &
|
||||
list_ntho tps id' tp }
|
||||
}
|
||||
|
||||
let rec pathvalo mem vals p v =
|
||||
let open Path in
|
||||
let open Value in
|
||||
ocanren {
|
||||
{ fresh x, id in
|
||||
p == VarP x &
|
||||
vals_assoco x vals id &
|
||||
mem_geto mem id v } |
|
||||
{ fresh p', v', id in
|
||||
p == DerefP p' &
|
||||
pathvalo mem vals p' v' &
|
||||
v' == RefV id &
|
||||
mem_geto mem id v } |
|
||||
{ fresh p', id, v', vs in
|
||||
p == AccessP (p', id) &
|
||||
pathvalo mem vals p' v' &
|
||||
v' == TupleV vs &
|
||||
list_ntho vs id v }
|
||||
}
|
||||
|
||||
(* --- eval rules --- *)
|
||||
|
||||
(* - value construction *)
|
||||
|
||||
let rec valcopy_foldero mem_with_vs v tp mem_with_vs' =
|
||||
ocanren {
|
||||
fresh mem, vs, mem', v', mem_with_v', vs' in
|
||||
Std.pair mem vs == mem_with_vs &
|
||||
valcopyo mem v tp mem_with_v' &
|
||||
Std.pair mem' v' == mem_with_v' &
|
||||
vs' == v' :: vs &
|
||||
mem_with_vs' == Std.pair mem vs'
|
||||
}
|
||||
|
||||
and valcopyo mem v tp mem_with_id' =
|
||||
let open Type in
|
||||
let open Value in
|
||||
let open ReadCap in
|
||||
let open CopyCap in
|
||||
ocanren {
|
||||
{ fresh r, w in
|
||||
is_trivial_vo v &
|
||||
tp == UnitT (r, w) &
|
||||
{ { r == Rd & mem_with_id' == Std.pair mem v } |
|
||||
{ r == NRd & mem_with_id' == Std.pair mem BotV } } } |
|
||||
{ fresh stmts, ts in
|
||||
v == FunV stmts &
|
||||
tp == FunT ts &
|
||||
mem_with_id' == Std.pair mem v } |
|
||||
{ fresh c, tp', id in
|
||||
v == RefV id &
|
||||
tp == RefT (c, tp') &
|
||||
{ { c == Rf & mem_with_id' == Std.pair mem v } |
|
||||
{ fresh v, mem_cp, v_cp, mem_with_v_cp,
|
||||
mem_add, id_add, mem_with_id_add in
|
||||
c == Cp &
|
||||
mem_geto mem id v &
|
||||
valcopyo mem v tp mem_with_v_cp &
|
||||
Std.pair mem v_cp == mem_with_v_cp &
|
||||
mem_addo mem_cp v_cp mem_with_id_add &
|
||||
Std.pair mem_add id_add == mem_with_id_add &
|
||||
mem_with_id' == (mem_add, RefV id_add) } } } |
|
||||
{ fresh vs, tps, init_mem_with_vs, mem_with_vs', mem', vs' in
|
||||
v == TupleV vs &
|
||||
tp == TupleT tps &
|
||||
init_mem_with_vs == Std.pair mem [] &
|
||||
list_foldl2o valcopy_foldero init_mem_with_vs vs tps mem_with_vs' &
|
||||
Std.pair mem' vs' == mem_with_vs' &
|
||||
mem_with_id' == Std.pair mem' (TupleV vs') }
|
||||
}
|
||||
|
||||
(* - value update *)
|
||||
|
||||
let rec valupdo mem v p b mem_with_v' =
|
||||
let open Path in
|
||||
let open Value in
|
||||
ocanren {
|
||||
{ fresh x in
|
||||
p == VarP x &
|
||||
mem_with_v' == Std.pair mem b } |
|
||||
{ fresh p', id, v', mem_upd, v_upd, mem_with_v_upd, mem_st in
|
||||
p == DerefP p' &
|
||||
v == RefV id &
|
||||
mem_geto mem id v' &
|
||||
valupdo mem v' p' b mem_with_v_upd &
|
||||
Std.pair mem_upd v_upd == mem_with_v_upd &
|
||||
mem_seto mem_upd id v_upd mem_st &
|
||||
mem_with_v' == Std.pair mem_st (RefV id) } |
|
||||
{ fresh p', id, vs', v', mem_upd, v_upd, mem_with_v_upd, vs_upd in
|
||||
p == AccessP (p', id) &
|
||||
v == TupleV vs' &
|
||||
list_ntho vs' id v' &
|
||||
valupdo mem v' p' b mem_with_v_upd &
|
||||
Std.pair mem_upd v_upd == mem_with_v_upd &
|
||||
list_replaceo vs' id v_upd vs_upd &
|
||||
mem_with_v' == Std.pair mem_upd (TupleV vs_upd) }
|
||||
}
|
||||
|
||||
(* - value combination *)
|
||||
|
||||
let rec valcombo u v u' =
|
||||
let open Value in
|
||||
ocanren {
|
||||
{ is_trivial_vo u &
|
||||
is_trivial_vo v &
|
||||
(* TODO: do not use disequality constraint ? *)
|
||||
{ { u == v & u' == u } | { u =/= v & u' == BotV } } } |
|
||||
{ fresh ustmts, vstmts, ustmts' in
|
||||
u == FunV ustmts &
|
||||
v == FunV vstmts &
|
||||
(* TODO: swap stmts order o efficiency ? *)
|
||||
List.appendo ustmts vstmts ustmts' &
|
||||
u' == FunV ustmts' } |
|
||||
{ fresh a, b in
|
||||
u == RefV a &
|
||||
v == RefV b &
|
||||
a == b } |
|
||||
{ fresh us, vs, us' in
|
||||
u == TupleV us &
|
||||
v == TupleV vs &
|
||||
list_zip_witho valcombo us vs us' &
|
||||
u' == TupleV us' }
|
||||
}
|
||||
|
||||
let memcombo m n m' = ocanren {
|
||||
fresh mm, ml, nm, nl, mm' in
|
||||
Pair.pair mm ml == m &
|
||||
Pair.pair nm nl == n &
|
||||
list_zip_witho valcombo mm nm mm' &
|
||||
m' == Pair.pair mm' ml
|
||||
}
|
||||
|
||||
(* - expression evaluation *)
|
||||
|
||||
let rec exprvalo mem vals e v' =
|
||||
let open Expr in
|
||||
let open Value in
|
||||
ocanren {
|
||||
{ e == UnitE & v' == ZeroV } |
|
||||
{ fresh p in
|
||||
e == PathE p &
|
||||
pathvalo mem vals p v' } |
|
||||
{ fresh x, v in
|
||||
e == RefE x &
|
||||
vals_assoco x vals v &
|
||||
v' == RefV v } |
|
||||
{ fresh es, vs' in
|
||||
e == TupleE es &
|
||||
List.mapo (exprvalo mem vals) es vs' &
|
||||
v' == TupleV vs' }
|
||||
}
|
||||
|
||||
(* - expression typing *)
|
||||
|
||||
let rec exprtypeo types e tp' =
|
||||
let open Expr in
|
||||
let open Type in
|
||||
let open ReadCap in
|
||||
let open WriteCap in
|
||||
let open CopyCap in
|
||||
ocanren {
|
||||
{ e == UnitE & tp' == UnitT (Rd, NeverWr) } |
|
||||
{ fresh p in
|
||||
e == PathE p &
|
||||
pathtypeo types p tp' } |
|
||||
{ fresh x, tp in
|
||||
e == RefE x &
|
||||
types_assoco x types tp &
|
||||
tp' == RefT (Rf, tp) } |
|
||||
{ fresh es, tps' in
|
||||
e == TupleE es &
|
||||
List.mapo (exprtypeo types) es tps' &
|
||||
tp' == TupleT tps' }
|
||||
}
|
||||
|
||||
(* - context initialization *)
|
||||
|
||||
let add_declo st x d st' =
|
||||
let open StEnv in
|
||||
let open Decl in
|
||||
let open TypesEnv in
|
||||
let open ValsEnv in
|
||||
ocanren {
|
||||
fresh mem, types, vals in
|
||||
st == StEnv (mem, TypesEnv types, ValsEnv vals) &
|
||||
{
|
||||
{ fresh tp, e, v,
|
||||
mem_with_v_cp, mem_cp, v_cp,
|
||||
mem_with_id_add, mem_add, id_add in
|
||||
d == VarD (tp, e) &
|
||||
exprvalo mem (ValsEnv vals) e v &
|
||||
valcopyo mem v tp mem_with_v_cp &
|
||||
Pair.pair mem_cp v_cp == mem_with_v_cp &
|
||||
mem_addo mem_cp v_cp mem_with_id_add &
|
||||
Pair.pair mem_add id_add == mem_with_id_add &
|
||||
st' == StEnv (mem_add,
|
||||
TypesEnv ((Pair.pair x tp) :: types),
|
||||
ValsEnv ((Pair.pair x id_add) :: vals))
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
let empty_memo m =
|
||||
let open MemEnv in
|
||||
ocanren { m == MemEnv ([], 0) }
|
||||
|
||||
let empty_stateo st =
|
||||
let open StEnv in
|
||||
let open TypesEnv in
|
||||
let open ValsEnv in
|
||||
ocanren {
|
||||
fresh m in
|
||||
empty_memo m &
|
||||
st == StEnv (m, TypesEnv [], ValsEnv [])
|
||||
}
|
||||
|
||||
(* TODO: better way ??? *)
|
||||
let globals_min_ido x = ocanren { x == 1000 }
|
||||
|
||||
let prog_init_foldero st_with_id d st_with_id' =
|
||||
ocanren {
|
||||
fresh st, x, st' in
|
||||
Std.pair st x == st_with_id &
|
||||
add_declo st x d st' &
|
||||
st_with_id' == Std.pair st' (Nat.s x)
|
||||
}
|
||||
|
||||
let prog_inito prog st' =
|
||||
let open Prg in
|
||||
ocanren {
|
||||
fresh decls, s, st_init, min_id, st_with_id', _id' in
|
||||
prog == Prg (decls, s) &
|
||||
empty_stateo st_init &
|
||||
globals_min_ido min_id &
|
||||
list_foldlo prog_init_foldero (Std.pair st_init min_id) decls st_with_id' &
|
||||
Std.pair st' _id' == st_with_id'
|
||||
}
|
||||
|
||||
(* - call values spoil *)
|
||||
|
||||
(* TODO: check that negation is interpreted correctly *)
|
||||
let is_correct_args v r w _r' w' m c =
|
||||
let open Value in
|
||||
let open ReadCap in
|
||||
let open WriteCap in
|
||||
let open Mode in
|
||||
let open CopyCap in
|
||||
ocanren {
|
||||
{ r == NRd | v == ZeroV } &
|
||||
{ r == NRd | is_ino m } &
|
||||
{ is_not_outo m | w == AlwaysWr } &
|
||||
{ w == NeverWr |
|
||||
{ is_not_outo m & c == Cp } |
|
||||
w' == AlwaysWr } &
|
||||
is_trivial_vo v
|
||||
}
|
||||
|
||||
(* TODO *)
|
||||
|
||||
(* full spoil *)
|
||||
(* TODO *)
|
||||
|
||||
(* - funciton argument addition *)
|
||||
(* TODO *)
|
||||
|
||||
(* - function evaluation *)
|
||||
(* NOTE: not needed due to performed optimization in stmt_eval ? *)
|
||||
|
||||
(* - statement evaluation *)
|
||||
(* TODO *)
|
||||
|
||||
(* --- program execution --- *)
|
||||
|
||||
(* let prog_evalo prog st' = *)
|
||||
(* let open Prog in *)
|
||||
(* ocanren { *)
|
||||
(* fresh decls, s, init_st, *)
|
||||
(* prog == Prog (decls, s) & *)
|
||||
(* prog_inito prog init_st & *)
|
||||
(* stmt_evalo init_st s st' *)
|
||||
(* } *)
|
||||
|
||||
(* --- FIXME --- CURRENT REWRITE POINT --- FIXME --- *)
|
||||
|
||||
(* --- tests --- *)
|
||||
(* TODO *)
|
||||
|
||||
(* - shortcuts *)
|
||||
(* TODO *)
|
||||
|
||||
(* --- *)
|
||||
|
||||
(* let rec list_zip_witho f xs ys zs = ocanren { *)
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue