Skip to content

GitLab

Commit 26bcb797 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

Merge branch 'master' of https://git.cduce.org/cduce 

Conflicts:
	tests/poly/red-black.cd
parents 9959b679 d9edaee1
Hide whitespace changes
Inline Side-by-side
parser/ulexer.ml
View file @ 26bcb797
......@@ -14,6 +14,7 @@ module Loc = struct
let to_tuple _ = assert false
let merge (x1, x2) (y1, y2) = (min x1 y1, max x2 y2)
let smart_merge a b = merge a b
let join (x1, _) = (x1, x1)
let move _ _ _ = assert false
let shift _ _ = assert false
......@@ -228,7 +229,7 @@ let rec token = lexer
| "[" ->
incr in_brackets;
return lexbuf (KEYWORD (L.utf8_lexeme lexbuf))
| "]" ->
| "]" ->
decr in_brackets;
return lexbuf (KEYWORD (L.utf8_lexeme lexbuf))
| '"' ->
......@@ -284,10 +285,10 @@ and token2 = lexer
| ".."
| ["?+*"] "?" | "#" ->
return lexbuf (KEYWORD (L.utf8_lexeme lexbuf))
| "[" ->
| "[" ->
incr in_brackets;
return lexbuf (KEYWORD (L.utf8_lexeme lexbuf))
| "]" ->
| "]" ->
decr in_brackets;
return lexbuf (KEYWORD (L.utf8_lexeme lexbuf))
| '"' ->
......@@ -354,10 +355,10 @@ and token2toplevel = lexer
| ".."
| ["?+*"] "?" | "#" ->
return lexbuf (KEYWORD (L.utf8_lexeme lexbuf))
| "[" ->
| "[" ->
incr in_brackets;
return lexbuf (KEYWORD (L.utf8_lexeme lexbuf))
| "]" ->
| "]" ->
decr in_brackets;
return lexbuf (KEYWORD (L.utf8_lexeme lexbuf))
| '"' ->
......@@ -442,7 +443,7 @@ and string start endchar = lexer
let token lexbuf =
if !in_brackets = 0 then token lexbuf
else if !toplevel then token2toplevel lexbuf
else if !toplevel then token2toplevel lexbuf
else token2 lexbuf
let lexbuf = ref None
......
tests/poly/patricia.cd
View file @ 26bcb797
......@@ -5,11 +5,11 @@
type Leaf = <leaf key=Caml_int> 'a
type Leaf('a) = <leaf key=Caml_int> 'a
type Branch = <brch pre=Caml_int bit=Caml_int>[ (Leaf|Branch) (Leaf|Branch) ]
type Branch('a) = <brch pre=Caml_int bit=Caml_int>[ (Leaf('a)|Branch('a)) (Leaf('a)|Branch('a)) ]
type Dict = [] | Branch | Leaf
type Dict('a) = [] | Branch('a) | Leaf('a)
let lowest_bit (x: Caml_int): Caml_int = Pervasives.land x ((0 - x):?Caml_int)
......@@ -25,7 +25,7 @@ let match_prefix (k: Caml_int)(p: Caml_int)(m: Caml_int): Bool =
let zero_bit (k: Caml_int)(m: Caml_int): Bool = Pervasives.land k m = 0
let lookup (k: Caml_int)(d: Dict) : ['a?] =
let lookup (k: Caml_int)(d: Dict('a)) : ['a?] =
match d with
| [] -> []
| <brch pre=p bit=m>[ t0 t1 ] ->
......@@ -35,7 +35,7 @@ let lookup (k: Caml_int)(d: Dict) : ['a?] =
| <leaf key=j> x -> if j=k then [ x ] else []
let join (p0: Caml_int)(t0: Dict\[])(p1: Caml_int)(t1: Dict\[]): Branch =
let join (p0: Caml_int)(t0: Dict('a)\[])(p1: Caml_int)(t1: Dict('a)\[]): Branch('a) =
let m = branching_bit p0 p1 in
if zero_bit p0 m then
<brch pre=(mask p0 m) bit=m>[t0 t1]
......@@ -44,8 +44,8 @@ let join (p0: Caml_int)(t0: Dict\[])(p1: Caml_int)(t1: Dict\[]): Branch =
let insert (c: 'a -> 'a -> 'a) (k: Caml_int) (x: 'a) (t: Dict): Leaf|Branch =
let ins (Leaf|Branch -> Leaf|Branch ; [] -> Leaf )
let insert (c: 'a -> 'a -> 'a) (k: Caml_int) (x: 'a) (t: Dict('a)): Leaf('a)|Branch('a) =
let ins (Leaf('a)|Branch('a) -> Leaf('a)|Branch('a) ; [] -> Leaf('a) )
| [] -> <leaf key=k> x
| (<leaf key=j>y)&t ->
if j=k then <leaf key=k>(c x y)
......@@ -57,14 +57,14 @@ let insert (c: 'a -> 'a -> 'a) (k: Caml_int) (x: 'a) (t: Dict): Leaf|Branch =
else join k (<leaf key=k>x) p t
in ins t
let max (x: 'a)(y: 'a): 'a = if (x >> y) then x else y;;
let max (x: 'a)(y: 'b): 'a|'b = if (x >> y) then x else y;;
let swap (f : 'a -> 'a -> 'a) (x: 'a)(y: 'a): 'a = f y x;;
let merge (c: 'a -> 'a -> 'a): (Dict,Dict) -> Dict =
let merge (c: 'a -> 'a -> 'a): (Dict('a),Dict('a)) -> Dict('a) =
fun aux( ([],[]) -> []
; (Dict,Dict)\([],[]) -> Dict\[]
; (Branch,Branch) -> Branch )
; (Dict('a),Dict('a))\([],[]) -> Dict('a)\[]
; (Branch('a),Branch('a)) -> Branch('a) )
| ([],t) | (t,[]) -> t
| (<leaf key=k>x , t) -> insert c k x t
| (t , <leaf key=k>x) -> insert (swap c) k x t
......
tests/poly/red-black-non-constructed.cd deleted 100644 → 0
View file @ 9959b679
type RBtree = Btree | Rtree
(* Black rooted RB tree: *)
type Btree = [] | <black elem='a>[ RBtree RBtree ]
(* Red rooted RB tree: *)
type Rtree = <red elem='a>[ Btree Btree ]
type Wrongtree = <red elem='a>( [ Rtree Btree ]
| [ Btree Rtree ])
type Unbalanced = <black elem='a>( [ Wrongtree RBtree ]
| [ RBtree Wrongtree ])
let balance ( Unbalanced -> Rtree ; 'b\Unbalanced -> 'b\Unbalanced )
| <black (z)>[ <red (y)>[ <red (x)>[ a b ] c ] d ]
| <black (z)>[ <red (x)>[ a <red (y)>[ b c ] ] d ]
| <black (x)>[ a <red (z)>[ <red (y)>[ b c ] d ] ]
| <black (x)>[ a <red (y)>[ b <red (z)>[ c d ] ] ] ->
<red (y)>[ <black (x)>[ a b ] <black (z)>[ c d ] ]
| x -> x
let insert (x : 'a) (t : Btree) : Btree =
let ins_aux ( [] -> Rtree;
Btree\[] -> RBtree\[];
Rtree -> Rtree|Wrongtree )
| [] -> <red elem=x>[ [] [] ]
| (<(color) elem=y>[ a b ]) & z ->
if x << y then balance <(color) elem=y>[ (ins_aux a) b ]
else if x >> y then balance <(color) elem=y>[ a (ins_aux b) ]
else z
in match ins_aux t with
| <_ (y)>[ a b ] -> <black (y)>[ a b ]
\ No newline at end of file
tests/poly/red-black.cd
View file @ 26bcb797
......@@ -8,10 +8,10 @@ type Btree('a) = [] | <black elem='a>[ RBtree('a) RBtree('a) ]
type Rtree('a) = <red elem='a>[ Btree('a) Btree('a) ]
type Wrongtree('a) = <red elem='a>( [ Rtree('a) Btree('a) ]
| [ Btree('a) Rtree('a) ])
| [ Btree('a) Rtree('a) ])
type Unbalanced('a) = <black elem='a>( [ Wrongtree('a) RBtree('a) ]
| [ RBtree('a) Wrongtree('a) ])
| [ RBtree('a) Wrongtree('a) ])
;;
(***************
......@@ -28,6 +28,9 @@ let balance ( Unbalanced('a) -> Rtree('a) ; 'b\Unbalanced('a) -> 'b\Unbalanced('
;;
************)
(* *)
(* Version 1: restrict the domain of balance to trees (ie, RBtree | Unbalanced) *)
(* *)
let balance ( Unbalanced('a) -> Rtree('a) ; 'b & RBtree('a) -> 'b & RBtree('a) )
| <black (z)>[ <red (y)>[ <red (x)>[ a b ] c ] d ]
......@@ -38,6 +41,13 @@ let balance ( Unbalanced('a) -> Rtree('a) ; 'b & RBtree('a) -> 'b & RBtree('a) )
| x -> x
;;
(* *)
(* Version 2: restrict the first branch to Unbalanced trees whatever *)
(* type it contains *)
(* *)
let balance ( Unbalanced('a) -> Rtree('a) ; 'b\Unbalanced(Any) -> 'b\Unbalanced(Any) )
| (<black (z)>[ <red (y)>[ <red (x)>[ a b ] c ] d ]
| <black (z)>[ <red (x)>[ a <red (y)>[ b c ] ] d ]
......@@ -47,13 +57,19 @@ let balance ( Unbalanced('a) -> Rtree('a) ; 'b\Unbalanced(Any) -> 'b\Unbalanced(
| x -> x
;;
(* *)
(* Version 3: Use the accepted type of the first branch (i.e. UTree) *)
(* to specify the behavious when the second branch is taken *)
(* *)
type UTree = <black (Any)>[ <red (Any)>[ <red (Any)>[ Any Any ] Any ] Any ]
| <black (Any)>[ <red (Any)>[ Any <red (Any)>[ Any Any ] ] Any ]
| <black (Any)>[ Any <red (Any)>[ <red (Any)>[ Any Any ] Any ] ]
| <black (Any)>[ Any <red (Any)>[ Any <red (Any)>[ Any Any ] ] ]
;;
let balance ( Unbalanced('a) -> Rtree('a) ; 'b\UTree -> 'b\UTree )
| <black (z)>[ <red (y)>[ <red (x)>[ a b ] c ] d ]
| <black (z)>[ <red (x)>[ a <red (y)>[ b c ] ] d ]
......@@ -63,6 +79,12 @@ let balance ( Unbalanced('a) -> Rtree('a) ; 'b\UTree -> 'b\UTree )
| x -> x
;;
(* Here we start the definition of *)
(* standard operations for red-black trees *)
let insert (x : 'a) (t : Btree('a)) : Btree('a)\[]=
let ins_aux ( [] -> Rtree('a);
Btree('a)\[] -> RBtree('a)\[];
......@@ -75,3 +97,114 @@ let insert (x : 'a) (t : Btree('a)) : Btree('a)\[]=
in match ins_aux t with
| <_ (y)>[ a b ] -> <black (y)>[ a b ]
let is_empty (RBtree('a) -> Bool) (*better type (Any\[] -> `false ; [] ->`true ) *)
| [] -> `true
| _ -> `false
let member (x : 'a) (t : RBtree('a)) : Bool =
(* better type: 'a -> ([] -> `false) & (RBtree('a) -> Bool) *)
match t with
| [] -> `false
| <_ elem=y>[ left right ] ->
(y = x) || ( member x (if x<<y then left else right) )
let singleton (x : 'a): Btree('a) = <black elem=x>[ [] [] ]
let cardinal ( RBtree('a) -> Int ) (* better type: [] -> 0, Any\[] -> [1--*] *)
| [] -> 0
| <_ ..>[ l r ] -> cardinal l + cardinal r + 1
(* The though case: deletion *)
(* remove the rightmost leave of the tree and return a flag to state
whether the resulting tree decreased the the depth of black nodes *)
let remove_min (RBtree('a)\[] -> [RBtree('a) Bool 'a])
(* black leaf: remove it and flag the depth decrease *)
| <black elem=x>[ [] [] ] ->
[ [] `true x ]
(* black node with red child: promote the child to black *)
| <black elem=x>[ ([] <red elem=y>[ l r ])
| (<red elem=y>[ l r ] [] )] ->
[ <black elem=y>[ l r ] `false x ]
(* you cannot have a red node with one empty sibling *)
| <black elem=Any>[ ([] <red ..>Any)
| (<red ..>Any []) ] ->
raise "impossible"
(* red node with at least on empty child : remove it without any flag *)
| <red elem=x>[ ([] n) | (n []) ] ->
[ n `false x ]
(* general case of a node with two non empty childs *)
| <(c) elem=x>[ l\[] r\[] ] ->
let [ ll d e ] = remove_min l in
let tree = <(c) elem=x>[ ll r ] in
if d then
(bubble_left tree)@[e]
else
[ tree `false e ]
| _ -> raise "impossible"
let blackify( (<_ ('a)>'b) -> <black ('a)>'b )
| <_ (x)>y -> <black (x)>y
let redify( (<_ ('a)>'b) -> <red ('a)>'b )
| <_ (x)>y -> <red (x)>y
(* increase the black depth of the right child of the argument and
flag whether the black depth of the tree is still to be incremented *)
let bubble_right ( RBtree('a)\[] -> (Btree('a) , Bool) )
| <black elem=y>[<red elem=x>[ ll\[] <black elem=re>[c d]] (e&<black ..>_) ] ->
( <black elem=re>[ <black elem=x>[(balance (redify ll)) c]
<black elem=y>[d e]
] , `true)
| <_ ..>[ [] _ ] ->
raise "impossible"
| <(c) elem=e>[ l r ] ->
(<black elem=e>[ (balance(redify l)) r ] , (c = `black))
(* increase the right depth of the right child of the argument and
flag whether the black depth of the tree is still to be incremented *)
let bubble_left ( RBtree('a)\[] -> (Btree('a) , Bool) )
| <black elem=z>[ (e&<black ..>_) <red elem=x>[ <black elem=w>[a b] ll\[] ] ] ->
( <black elem=w>[ <black elem=z>[ e a ]
<black elem=x>[ b (balance (redify ll)) ]
] , `true )
| <_ ..>[ _ [] ] ->
raise "impossible"
| <(c) elem=e>[ l r ] ->
(<black elem=e>[ l (balance (redify r)) ], (c = `black))
let remove(x : 'a)(t : RBtree('a) ) : RBtree('a) =
let remove_aux(RBtree('a) -> (RBtree('a),Bool) )
| [] ->
([],`false)
| <(c) elem=y>[ l r ] & tree ->
if (x << y ) then
let (ll,d) = remove_aux l in
let tree = <(c) elem=y>[ ll r ] in (* we must prove that tree is well-formed *)
if d then bubble_left tree else (tree,`false)
else if (x >> y) then
let (rr,d) = remove_aux r in
let tree = <(c) elem=y>[ l rr ] in
if d then bubble_right tree else (tree,`false)
else (* x = y *)
match tree with
| <(c) ..>[ [] [] ] -> ([], (c = `black))
| <black ..>[ ([] y) | (y []) ] -> (blackify y,`false)
| <(c) ..>[ l r ] ->
let [ ll d z ] = remove_min l in
let tree = <(c) elem=z>[ ll r] in
if d then bubble_left tree else (tree, `false)
in
let (sol,_) = remove_aux t in sol
\ No newline at end of file
types/boolVar.ml
View file @ 26bcb797
......@@ -19,14 +19,14 @@ end
module type S = sig
type s
type elem = s Var.pairvar
type elem = s Var.var_or_atom
include Custom.T
(* returns the union of all leaves in the BDD *)
val leafconj: t -> s
val get: t -> (elem list * elem list) list
val build : (elem list * elem list) list -> t
(* val build : (elem list * elem list) list -> t*)
val empty : t
val full : t
(* same as full, but we keep it for the moment to avoid chaging
......@@ -87,7 +87,7 @@ module Make (T : E) : S with type s = T.t = struct
*)
type s = T.t
type elem = s Var.pairvar
type elem = s Var.var_or_atom
module X : Custom.T with type t = elem = Var.Make(T)
type 'a bdd =
[ `True
......@@ -222,10 +222,11 @@ module Make (T : E) : S with type s = T.t = struct
| `True -> full
| `False -> empty
| `Split(_,x, p,i,n) ->
let p = cap (atom x) (aux p)
and i = aux i
and n = diff (aux n) (atom x) in
cup (cup p i) n
let x1 = atom x in
let p = cap x1 (aux p) in
let i = aux i in
let n = diff (aux n) x1 in
cup (cup p i) n
in
aux b
......
types/boolVar.mli
View file @ 26bcb797
......@@ -14,14 +14,14 @@ end
module type S = sig
type s
type elem = s Var.pairvar
type elem = s Var.var_or_atom
include Custom.T
(** returns the union of all leaves in the BDD *)
val leafconj: t -> s
val get: t -> (elem list * elem list) list
val build : (elem list * elem list) list -> t
(* val build : (elem list * elem list) list -> t *)
val empty : t
val full : t
(* same as full, but we keep it for the moment to avoid chaging the code everywhere *)
......
types/types.ml
View file @ 26bcb797
......@@ -2688,13 +2688,8 @@ module Positive = struct
let ty d = cons (`Type d)
let var d = cons (`Variable d)
let neg v = cons (`Neg v)
let cup vl =
match vl with
[ v ] -> v
| _ -> cons (`Cup vl)
let cap vl = match vl with
[ v ] -> v
| _ -> cons (`Cap vl)
let rec cup vl = cons (`Cup vl)
let cap vl = cons (`Cap vl)
let times v1 v2 = cons (`Times (v1,v2))
let arrow v1 v2 = cons (`Arrow (v1,v2))
let xml v1 v2 = cons (`Xml (v1,v2))
......@@ -2752,13 +2747,13 @@ module Positive = struct
and decompose_type t =
try DescrHash.find memo t
with Not_found ->
let node_t = forward () in
if no_var t then ty t
else
match check_var t with
`Pos v -> var v
| `Neg v -> neg (var v)
| `NotVar ->
let node_t = forward () in
let () = DescrHash.add memo t node_t in
let descr_t =
decompose_kind Atom.any atom (BoolAtoms.get t.atoms)
......@@ -2776,18 +2771,20 @@ module Positive = struct
decompose_type t
let solve v = internalize (make_node v)
let substitute_aux delta v subst =
(* [map_var f v] applies returns the type
[v{ 'a <- f 'a}] for all ['a] in [v]
*)
let map_var subst v =
let memo = MemoHash.create 17 in
let rec aux v subst =
try MemoHash.find memo v
with Not_found -> begin
with Not_found ->
let node_v = forward () in
MemoHash.add memo v node_v;
let () = MemoHash.add memo v node_v in
let new_v =
match v.def with
|`Type d -> `Type d
|`Variable d when Var.Set.mem d delta -> v.def
(* |`Variable d when Var.Set.mem d delta -> v.def *)
|`Variable d -> (subst d).def
|`Cup vl -> `Cup (List.map (fun v -> aux v subst) vl)
|`Cap vl -> `Cap (List.map (fun v -> aux v subst) vl)
......@@ -2800,62 +2797,57 @@ module Positive = struct
in
node_v.def <- new_v;
node_v
end
in
aux v subst
(* returns a recursive type where all occurrences of alpha n t
* are substituted with a recursive variable X *)
let substituterec t alpha =
if no_var t then t
else begin
let subst x d = if Var.equal d alpha then x else var d in
let x = forward () in
define x (substitute_aux Var.Set.empty (decompose t) (subst x));
descr(solve x)
end
let apply_subst ?(subst=(fun v -> var v)) ?(after=(fun x -> x)) t =
if no_var t then t else
let res = map_var subst (decompose t) in
let res = after res in
descr (solve res)
(* Given a type t and a polymorphic variable 'a occuring in t,
returns the type s which is the solution of 'a = t *)
let solve_rectype t alpha =
let x = forward () in
let subst d = if Var.equal d alpha then x else var d in
apply_subst ~subst:subst ~after:(fun y -> define x y;x) t
(* Pre-condition : alpha \not\in \delta *)
let substitute t (alpha,s) =
if no_var t then t
else begin
let subst s d = if Var.equal d alpha then s else var d in
let new_t = (substitute_aux Var.Set.empty (decompose t) (subst (ty s))) in
descr (solve new_t)
end
let vs = ty s in
let subst d = if Var.equal d alpha then vs else var d in
apply_subst ~subst:subst t
let substitute_list t l =
if no_var t then t
else begin
let subst l d =
try ty(snd(List.find (fun (alpha,_) -> Var.equal d alpha) l))
with Not_found -> var d
in
let new_t = (substitute_aux Var.Set.empty (decompose t) (subst l)) in
descr (solve new_t)
end
let subst d =
try
ty
@@ snd
@@ List.find (fun (alpha,_) -> Var.equal d alpha) l
with Not_found -> var d
in
apply_subst ~subst:subst t
let substitutefree delta t =
if no_var t then t else
let substitute_free delta t =
let h = Hashtbl.create 17 in
let subst h d =
try Hashtbl.find h d
with Not_found -> begin
let x = var (Var.fresh d) in
Hashtbl.add h d x ;
x
end
let subst d =
if Var.Set.mem d delta then var d else
try
Hashtbl.find h d
with Not_found ->
let x = var (Var.fresh d) in
Hashtbl.add h d x ;
x
in
let dec = decompose t in
let new_t = substitute_aux delta dec (subst h) in
descr (solve new_t)
apply_subst ~subst:subst t
let substitute_kind delta kind t =
if no_var t then t else
let subst kin d = var (Var.set_kind kind d) in
let dec = decompose t in
let new_t = substitute_aux delta dec (subst kind) in
descr (solve new_t)
let subst d =
if Var.Set.mem d delta then var d else
var (Var.set_kind kind d)
in
apply_subst ~subst:subst t
(* We cannot use the variance annotation of variables to simplify them,
since variables are shared amongst types. If we have two types
......@@ -2916,24 +2908,21 @@ module Positive = struct
aux true v;
vars
let clean_variables delta t =
let clean_type delta t =
if no_var t then t
else begin
let dec = decompose t in
let h = collect_variables delta dec in
let new_t =
substitute_aux delta dec (fun d ->
try Hashtbl.find h d
with Not_found -> assert false
)
map_var (fun d ->
try
Hashtbl.find h d
with Not_found -> assert false
) dec
in
descr (solve new_t)
end
let clean_type delta t =
if no_var t then t else
clean_variables delta t
let dump ppf t = pp ppf (decompose t)
end
......@@ -3473,8 +3462,8 @@ module Tallying = struct
(* Format.printf "e1 = %a\n" CS.print_e e1; *)
(* remove from E \ { (alpha,t) } every occurrences of alpha
* by mu X . (t{X/alpha}) with X fresh . X is a recursion variale *)
(* substituterec remove also all previously introduced fresh variables *)
let x = Positive.substituterec t alpha in
(* solve_rectype remove also all previously introduced fresh variables *)
let x = Positive.solve_rectype t alpha in
(* Format.printf "X = %a %a %a\n" Var.pp alpha Print.print x dump t; *)
let es =
CS.E.fold (fun beta s acc ->
......@@ -3616,7 +3605,7 @@ let squaresubtype delta s t =
try
let ss =
if i = 0 then s
else (cap (Positive.substitutefree delta s) (get ai (i-1)))
else (cap (Positive.substitute_free delta s) (get ai (i-1)))
in
set ai i ss;
tallying i;
......@@ -3665,8 +3654,8 @@ let apply_raw delta s t =
(* Format.printf "Starting expansion %i @\n@." i; *)
let (ss,tt) =
if i = 0 then (s,t) else
((cap (Positive.substitutefree delta s) (get ai (i-1))),
(cap (Positive.substitutefree delta t) (get aj (i-1))))
((cap (Positive.substitute_free delta s) (get ai (i-1))),
(cap (Positive.substitute_free delta t) (get aj (i-1))))
in
set ai i ss;
set aj i tt;
......
types/types.mli
View file @ 26bcb797
......@@ -71,30 +71,20 @@ end
module BoolAtoms : BoolVar.S with
type s = Atoms.t and
type elem = Atoms.t Var.pairvar
type elem = Atoms.t Var.var_or_atom
module BoolIntervals : BoolVar.S with
type s = Intervals.t and
type elem = Intervals.t Var.pairvar
type elem = Intervals.t Var.var_or_atom
module BoolChars : BoolVar.S with
type s = Chars.t and
type elem = Chars.t Var.pairvar
type elem = Chars.t Var.var_or_atom
module BoolAbstracts: BoolVar.S with
type s = Abstracts.t and
type elem = Abstracts.t Var.pairvar
type elem = Abstracts.t Var.var_or_atom
include Custom.T