Commit 0acf2a7b authored by Pietro Abate's avatar Pietro Abate

Minor changes

parent 7237f129
......@@ -16,13 +16,11 @@ let nth (l : [('a)*])(n : Int) : 'a =
| [el; rest] -> if n >> 0 then aux rest (n - 1) else el in
if n << 0 then raise "Invalid_argument \"List.nth\"" else aux l n
(* Typing error
let rev (l : [('a)*]) : [('a)*] =
let aux (l : [('a)*])(res : [('a)*]) : [('a)*] = match l with
| [] -> res
| [el; rest] -> aux rest ([el] @ res) in
aux l []
*)
(* Iterators *)
......@@ -37,12 +35,10 @@ let iteri (f : (Int -> 'a -> []))(l : [('a)*]) : [] =
in
aux f l 0
(* Same typing error as rev
let mapf (f : 'a -> 'b)(l : [('a)*]) : [('b)*] =
let aux (f : 'a -> 'b)(l : [('a)*])(acc : [('b)*]) : [('b)*] = match l with
| [] -> acc
| [el; rest] -> aux f rest (acc @ [el]) in
aux f l []
*)
(* List scanning *)
......@@ -1778,13 +1778,14 @@ struct
DescrHash.add memo d s;
s
end with Not_found ->
if d.absent then
alloc [Abs (prepare ({d with absent=false}))]
else if worth_complement d then
alloc [Neg (prepare (neg d))]
else
let slot = alloc [] in
if not (worth_abbrev d) then slot.state <- `Expand;
if d.absent then
alloc [Abs (prepare ({d with absent=false}))]
else if worth_complement d then
alloc [Neg (prepare (neg d))]
else
let slot = alloc [] in
if not (worth_abbrev d) then
slot.state <- `Expand;
DescrHash.add memo d slot;
......@@ -1802,8 +1803,8 @@ struct
List.fold_left (fun acc (p,n) ->
let (_,l1) =
List.fold_left (fun (has_tlv,acc) -> function
|(`Var v) as x when (TLV.mem (x,true) tlv) -> (true,acc)
|(`Var v) as x -> (has_tlv,(Atomic (fun ppf -> Var.pp ppf x))::acc)
|(`Var v) (* as x when (TLV.mem (x,true) tlv) *) -> (true,acc)
(* |(`Var v) as x -> (has_tlv,(Atomic (fun ppf -> Var.pp ppf x))::acc) *)
|`Atm bdd ->
begin match has_tlv,acc with
|true,[] -> if is_full bdd then (has_tlv,[]) else (has_tlv,print bdd)
......@@ -1814,8 +1815,8 @@ struct
in
let l2 =
List.fold_left (fun acc -> function
|(`Var v) as x when (TLV.mem (x,false) tlv) -> acc
|(`Var v) as x -> (Atomic (fun ppf -> Format.fprintf ppf "~ %a" Var.pp x))::acc
|(`Var v) (* as x when (TLV.mem (x,false) tlv) *) -> acc
(* |(`Var v) as x -> (Atomic (fun ppf -> Format.fprintf ppf "~ %a" Var.pp x))::acc *)
|`Atm bdd -> assert false
) [] n
in
......@@ -2626,7 +2627,7 @@ struct
let rec pretty_name i acc =
let ni,nm = i/26, i mod 26 in
let acc = acc ^ (String.make 1 (OldChar.chr (OldChar.code 'A' + nm))) in
let acc = acc ^ (String.make 1 (OldChar.chr (OldChar.code 'a' + nm))) in
if ni == 0 then acc else pretty_name ni acc
let collect_variables v =
......@@ -2655,7 +2656,7 @@ struct
(* polarity conflict, replace the binding by a new, pretty-printed variable *)
if ((td == t_emp) && not pos) || ((td == t_any) && pos) then begin
let id = pretty_name !idx "" in
let x = var (Var.mk ~fresh:false ~repr:(Var.id d) id) in
let x = var (Var.mk ~fresh:false id) in
incr idx;
Hashtbl.replace vars d x ;
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