Commit 3903816f authored by Pietro Abate's avatar Pietro Abate

fix type printing problem

parent b4e3e22a
......@@ -1683,6 +1683,7 @@ struct
| Record of (bool * nd) label_map * bool * bool
| Arrows of (nd * nd) list * (nd * nd) list
| Intersection of nd
| Union of nd
| Neg of nd
| Abs of nd
......@@ -1845,12 +1846,13 @@ struct
prepare_boolvar BoolChars.get (Chars.equal Chars.full) (fun bdd ->
match Chars.is_char bdd with
| Some c -> [(Char c)]
| None -> List.map (fun x -> (Atomic x)) (Chars.print bdd)
) not_seq.toplvars not_seq.chars;
| None -> [(Union(alloc (List.map (fun x -> (Atomic x)) (Chars.print bdd))))]
) not_seq.toplvars not_seq.chars;
prepare_boolvar BoolIntervals.get (Intervals.equal Intervals.full) (fun bdd ->
List.map (fun x -> (Atomic x)) (Intervals.print bdd)
) not_seq.toplvars not_seq.ints;
[(Union(alloc (List.map (fun x -> (Atomic x)) (Intervals.print bdd))))]
(* List.map (fun x -> (Atomic x)) (Intervals.print bdd) *)
) not_seq.toplvars not_seq.ints;
let bool =
Atoms.cup
......@@ -1858,9 +1860,12 @@ struct
(Atoms.atom (Atoms.V.mk_ascii "true"))
in
prepare_boolvar BoolAtoms.get (Atoms.equal Atoms.full) (fun bdd ->
if Atoms.equal bool bdd then [Atomic (fun ppf -> Format.fprintf ppf "Bool")]
else List.map (fun x -> (Atomic x)) (Atoms.print bdd)
) not_seq.toplvars not_seq.atoms;
if Atoms.equal bool bdd then
[Atomic (fun ppf -> Format.fprintf ppf "Bool")]
else
[(Union(alloc (List.map (fun x -> (Atomic x)) (Atoms.print bdd))))]
(* List.map (fun x -> (Atomic x)) (Atoms.print bdd) *)
) not_seq.toplvars not_seq.atoms;
(* pairs *)
prepare_boolvar BoolPair.get (Pair.equal Pair.full) (fun x ->
......@@ -1885,7 +1890,8 @@ struct
(Xml (tag, prepare ta, prepare tb))
) (Product.get t2);
) (Product.partition any_pair x)
)) not_seq.toplvars not_seq.xml;
)
) not_seq.toplvars not_seq.xml;
(* arrows *)
prepare_boolvar BoolPair.get (Pair.equal Pair.full) (fun x ->
......@@ -1893,14 +1899,14 @@ struct
let aux (t,s) = prepare (descr t), prepare (descr s) in
let p = List.map aux p and n = List.map aux n in
(Arrows (p,n))
) (Pair.get x)) not_seq.toplvars not_seq.arrow;
) (Pair.get x)) not_seq.toplvars not_seq.arrow;
(* records *)
prepare_boolvar BoolRec.get (Rec.equal Rec.full) (fun x ->
List.map (fun (r,some,none) ->
let r = LabelMap.map (fun (o,t) -> (o, prepare t)) r in
(Record (r,some,none))
) (Record.get { empty with record = BoolRec.atom (`Atm x) })) not_seq.toplvars not_seq.record;
) (Record.get { empty with record = BoolRec.atom (`Atm x) })) not_seq.toplvars not_seq.record;
List.iter (fun x -> add (Atomic x)) (Abstract.print not_seq.abstract);
......@@ -1956,6 +1962,7 @@ struct
| Regexp r -> assign_name_regexp r
| Pair (t1,t2) -> assign_name t1; assign_name t2
| Intersection t -> () (* assign_name t *)
| Union t -> () (* assign_name t *)
| Xml (tag,t2,t3) ->
(match tag with `Type t -> assign_name t | _ -> ());
assign_name t2;
......@@ -1999,6 +2006,7 @@ struct
| Regexp r -> Format.fprintf ppf "@[[ %a ]@]" (do_print_regexp 0) r
| Atomic a -> a ppf
| Intersection a -> Format.fprintf ppf "@[%a@]" (do_print_slot ~sep:"&" 0) a
| Union a -> Format.fprintf ppf "@[%a@]" (do_print_slot ~sep:"|" 0) a
| Pair (t1,t2) ->
Format.fprintf ppf "@[(%a,%a)@]"
(do_print_slot 0) t1
......
......@@ -946,40 +946,32 @@ and type_check' loc env ed constr precise = match ed with
(ed,localize loc (flatten (type_map loc env true e b) constr) precise)
| Apply (e1,e2) ->
Printf.printf "1\n";
let t1 = type_check env e1 Types.Arrow.any true in
(* t [_delta 0 -> 1 *)
begin try ignore(Types.Tallying.tallying ~delta:env.delta [(t1,Types.Arrow.any)])
with Types.Tallying.UnSatConstr _ -> raise_loc loc (Constraint (t1, Types.Arrow.any)) end;
Printf.printf "2\n";
let t1arrow = Types.Arrow.get t1 in
let dom = Types.Arrow.domain(t1arrow) in
let res =
if not(Types.is_closed env.delta dom) then begin
if not(Types.is_closed env.delta dom) then
(* get t2 without constraint check *)
Printf.printf "3\n";
let t2 = type_check env e2 Types.any true in
Printf.printf "4\n";
let (sl,res) =
(* s [_delta dom(t) *)
try Types.squareapply env.delta t1 t2
with Types.Tallying.UnSatConstr _ ->
raise_loc loc (Constraint (dom,t2))
in
Printf.printf "5\n";
res
end else begin
else begin
(* Monomorphic case as before *)
Printf.printf "44\n";
if Types.Arrow.need_arg t1arrow then begin
if Types.Arrow.need_arg t1arrow then
let t2 = type_check env e2 dom true in
Printf.printf "55\n";
Types.Arrow.apply t1arrow t2
end else begin
else begin
(ignore (type_check env e2 dom false);
Printf.printf "66\n";
Types.Arrow.apply_noarg t1arrow)
end
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