Commit 696a55c3 authored by Pietro Abate's avatar Pietro Abate

[r2006-04-27 14:27:53 by afrisch] Fix memoization of witnesses. Better typing of records

Original author: afrisch
Date: 2006-04-27 14:27:54+00:00
parent 58322af1
This diff is collapsed.
......@@ -555,7 +555,7 @@ module Witness = struct
let equal w1 w2 = match w1,w2 with
| WPair (p1,q1,_), WPair (p2,q2,_)
| WXml (p1,q1,_), WPair (p2,q2,_) ->
| WXml (p1,q1,_), WXml (p2,q2,_) ->
equal_small p1 p2 && equal_small q1 q2
| WRecord (r1,o1,_), WRecord (r2,o2,_) ->
o1 == o2 && (LabelMap.equal equal_small r1 r2)
......@@ -577,14 +577,11 @@ module Witness = struct
let wslot () = { wuid = !wuid; wnodes_in = NodeSet.empty;
wnodes_out = NodeSet.empty }
let wmk w = (* incr wuid; w *) (* hash-consing disabled *)
try WHash.find wmemo w
with Not_found -> incr wuid; w
let wpair p1 p2 = wmk (WPair (p1,p2, wslot()))
let wxml p1 p2 = wmk (WXml (p1,p2, wslot()))
let wrecord r o = wmk (WRecord (r,o, wslot()))
let wfun f = wmk (WFun (f, wslot()))
let () =
Stats.register Stats.Summary
(fun ppf -> Format.fprintf ppf "Allocated witnesses:%i@\n" !wuid)
let rec print_witness ppf = function
| WInt i ->
......@@ -624,6 +621,20 @@ module Witness = struct
| WAbsent ->
Format.fprintf ppf "Absent"
let wmk w = (* incr wuid; w *) (* hash-consing disabled *)
try WHash.find wmemo w
with Not_found ->
incr wuid;
WHash.add wmemo w w;
(* Format.fprintf Format.std_formatter "W:%a@."
print_witness w; *)
w
let wpair p1 p2 = wmk (WPair (p1,p2, wslot()))
let wxml p1 p2 = wmk (WXml (p1,p2, wslot()))
let wrecord r o = wmk (WRecord (r,o, wslot()))
let wfun f = wmk (WFun (f, wslot()))
let bool_pair f =
BoolPair.compute
~empty:false ~full:true
......@@ -779,10 +790,10 @@ and check_times (left,right) s =
| (n1,n2) :: rest
when (Witness.node_has n1 w1) && (Witness.node_has n2 w2) ->
let right = seen @ rest in
let accu1' = diff accu1 (descr n1) in
guard s accu1' (fun w1 -> aux w1 w2 accu1' accu2 [] right);
let accu2' = diff accu2 (descr n2) in
guard s accu2' (fun w2 -> aux w1 w2 accu1 accu2' [] right)
guard s accu2' (fun w2 -> aux w1 w2 accu1 accu2' [] right);
let accu1' = diff accu1 (descr n1) in
guard s accu1' (fun w1 -> aux w1 w2 accu1' accu2 [] right)
| k :: rest -> aux w1 w2 accu1 accu2 (k::seen) rest
in
let (t1,t2) = cap_product any any left in
......@@ -796,10 +807,10 @@ and check_xml (left,right) s =
| (n1,n2) :: rest
when (Witness.node_has n1 w1) && (Witness.node_has n2 w2) ->
let right = seen @ rest in
let accu1' = diff accu1 (descr n1) in
guard s accu1' (fun w1 -> aux w1 w2 accu1' accu2 [] right);
let accu2' = diff accu2 (descr n2) in
guard s accu2' (fun w2 -> aux w1 w2 accu1 accu2' [] right)
guard s accu2' (fun w2 -> aux w1 w2 accu1 accu2' [] right);
let accu1' = diff accu1 (descr n1) in
guard s accu1' (fun w1 -> aux w1 w2 accu1' accu2 [] right)
| k :: rest -> aux w1 w2 accu1 accu2 (k::seen) rest
in
let (t1,t2) = cap_product any any_pair left in
......@@ -871,9 +882,10 @@ let is_empty d =
Stats.Timer.stop timer_subtype
(s.status == Empty)
let witness t =
if is_empty t then raise Not_found
else match (slot t).status with NEmpty w -> w | _ -> assert false
let getwit t = match (slot t).status with NEmpty w -> w | _ -> assert false
(* Assumes that is_empty has been called on t before. *)
let witness t = if is_empty t then raise Not_found else getwit t
(*
let is_empty d =
......@@ -995,7 +1007,7 @@ struct
let pi2 = List.fold_left (fun acc (_,t2) -> cup acc t2) empty
let pi2_restricted restr =
List.fold_left (fun acc (t1,t2) ->
if is_empty (cap t1 restr) then acc
if disjoint t1 restr then acc
else cup acc t2) empty
let restrict_1 rects pi1 =
......@@ -1050,8 +1062,7 @@ struct
let constraint_on_2 n t1 =
List.fold_left
(fun accu (d1,d2) ->
if is_empty (cap d1 t1) then accu else cap accu d2)
(fun accu (d1,d2) -> if disjoint d1 t1 then accu else cap accu d2)
any
n
......@@ -1146,7 +1157,6 @@ struct
let split_normal d l =
TR.boolean_normal (aux_split d l)
let pi l d = TR.pi1 (split d l)
let project d l =
......@@ -1254,6 +1264,16 @@ struct
(split d l)
in
aux [] [] d
type t = TR.t
let focus = split_normal
let get_this r = { (TR.pi1 r) with absent = false }
let need_others = function _::_::_ -> true | _ -> false
let constraint_on_others r t1 =
List.fold_left
(fun accu (d1,d2) -> if disjoint d1 t1 then accu else cap accu d2)
any_record
r
end
......
......@@ -189,6 +189,13 @@ module Record : sig
val remove_field: t -> label -> t
val get: t -> ((bool * t) label_map * bool * bool) list
type t
val focus: descr -> label -> t
val get_this: t -> descr
val need_others: t -> bool
val constraint_on_others: t -> descr -> descr
end
module Arrow : sig
......
......@@ -1028,31 +1028,34 @@ and type_check_string loc env ofs s i j e constr precise =
else constr
and type_record loc env r constr precise =
(* try to get rid of precise = true for values of fields *)
(* also: the use equivalent of need_second to optimize... *)
if not (Types.Record.has_record constr) then
should_have loc constr "but it is a record";
let (rconstr,res) =
List.fold_left
(fun (rconstr,res) (l,e) ->
(* could compute (split l e) once... *)
let pi = Types.Record.project_opt rconstr l in
let r = Types.Record.focus rconstr l in
let pi = Types.Record.get_this r in
if Types.is_empty pi then
(let l = Label.string_of_attr l in
should_have loc constr
(Printf.sprintf "Field %s is not allowed here." l));
let t = type_check env e pi true in
let rconstr = Types.Record.condition rconstr l t in
let res = (l,Types.cons t) :: res in
let t = type_check env e pi (precise || Types.Record.need_others r) in
let rconstr = Types.Record.constraint_on_others r t in
if Types.is_empty rconstr then
(let l = Label.string_of_attr l in
should_have loc constr
(Printf.sprintf "Type of field %s is not precise enough." l));
let res = if precise then LabelMap.add l (Types.cons t) res
else res in
(rconstr,res)
) (constr, []) (LabelMap.get r)
) (constr, LabelMap.empty) (LabelMap.get r)
in
if not (Types.Record.has_empty_record rconstr) then
should_have loc constr "More fields should be present";
let t =
Types.record_fields (false, LabelMap.from_list (fun _ _ -> assert false) res)
in
verify loc t constr
if precise then Types.record_fields (false, res)
else constr
and type_check_branches loc env targ brs constr precise =
......
......@@ -477,14 +477,14 @@ match page with
<td valign="top" align="left" style="width:100%">[
<table width="100%">[
<tr>[ <td valign="top" align="left"
style="border: 2px solid black; background: #ffffff;
text-align:center; color: #aa0000; font: bold 200% helvetica" >
style=("border: 2px solid black; background: #ffffff;
text-align:center; color: #aa0000; font: bold 200% helvetica" : Latin1)>
(text banner)
]
<tr>[
<td valign="top" align="left"
style="border: 1px solid black; background: #fccead">[
style=("border: 1px solid black; background: #fccead" : Latin1)>[
(* altbg c8ccd1 *)
<table width="100%" cellpadding="0" cellspacing="17">
(map main with x -> <tr>[ <td>[x] ])
......
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