Skip to content

GitLab

Commit 87acc186 authored by Pietro Abate's avatar Pietro Abate
Browse files

[r2004-12-26 23:43:53 by afrisch] Oops 

Original author: afrisch
Date: 2004-12-26 23:43:54+00:00
parent 4b3cadd9
Hide whitespace changes
Inline Side-by-side
Showing with 189 additions and 239 deletions
driver/cduce.ml
View file @ 87acc186
......@@ -194,8 +194,8 @@ let debug ppf tenv cenv = function
Format.fprintf ppf "[DEBUG:compile]@.";
let t = Typer.typ tenv t
and pl = List.map (Typer.pat tenv) pl in
(* Patterns.Compile.debug_compile ppf t pl *)
Patterns.demo_compile ppf (Types.descr t) (List.map Patterns.descr pl)
Patterns.Compile.debug_compile ppf t pl
(* Patterns.demo_compile ppf (Types.descr t) (List.map Patterns.descr pl) *)
| `Explain (t,e) ->
Format.fprintf ppf "[DEBUG:explain]@.";
let t = Typer.typ tenv t in
......
misc/custom.ml
View file @ 87acc186
......@@ -36,6 +36,8 @@ let dump_list ?(sep="; ") f ppf l =
);
Format.pp_print_string ppf " ]"
let dump_array ?(sep="; ") f ppf a = dump_list ~sep f ppf (Array.to_list a)
module String : T with type t = string = struct
type t = string
let dump = Format.pp_print_string
......@@ -82,6 +84,34 @@ module Bool : T with type t = bool = struct
let deserialize = Serialize.Get.bool
end
module Array(X : T) = struct
module Elem = X
type t = X.t array
let dump = dump_array X.dump
let check a = Array.iter X.check a
let rec compare_elems a1 a2 i l =
if (i = l) then 0
else
let c = X.compare a1.(i) a2.(i) in
if c <> 0 then c else compare_elems a1 a2 (succ i) l
let compare a1 a2 =
let l1 = Array.length a1 and l2 = Array.length a2 in
let c = Pervasives.compare l1 l2 in if c <> 0 then c
else compare_elems a1 a2 0 l1
let equal a1 a2 = compare a1 a2 == 0
let hash a =
let h = ref (Array.length a) in
Array.iter (fun x -> h := 17 * !h + X.hash x) a;
!h
let serialize t x = Serialize.Put.array X.serialize t x
let deserialize t = Serialize.Get.array X.deserialize t
end
module List(X : T) = struct
module Elem = X
type t = X.t list
......
types/patterns.ml
View file @ 87acc186
......@@ -98,6 +98,11 @@ let define x ((accept,fv,_) as d) =
Types.define x.accept accept;
x.descr <- d
let cons fv d =
let q = make fv in
define q d;
q
let constr x = (x,IdSet.empty,Constr x)
let cup ((acc1,fv1,_) as x1) ((acc2,fv2,_) as x2) =
if not (IdSet.equal fv1 fv2) then (
......@@ -484,70 +489,63 @@ module Normal = struct
| Some x -> Format.fprintf ppf "Some(%a)" print_result x
| None -> Format.fprintf ppf "None"
module NodeSet =
SortedList.Make(Node)
module NodeSet = SortedList.Make(Node)
type nnf = NodeSet.t * Types.t (* pl,t; t <= \accept{pl} *)
module Nnf = struct
type t = NodeSet.t * Types.t * IdSet.t (* pl,t; t <= \accept{pl} *)
let check (pl,t,xs) =
List.iter (fun p -> assert(Types.subtype t (Types.descr p.accept)))
(NodeSet.get pl)
let print ppf (pl,t,xs) =
Format.fprintf ppf "@[(pl=%a;t=%a)@]" NodeSet.dump pl Types.Print.print t
let compare (l1,t1,xs1) (l2,t2,xs2) =
let c = NodeSet.compare l1 l2 in if c <> 0 then c
else let c = Types.compare t1 t2 in if c <> 0 then c
else IdSet.compare xs1 xs2
let hash (l,t,xs) =
(NodeSet.hash l) + 17 * (Types.hash t) + 257 * (IdSet.hash xs)
let equal x y = compare x y == 0
end
let check_nnf (pl,t) =
List.iter (fun p -> assert(Types.subtype t (Types.descr p.accept)))
(NodeSet.get pl)
module NBasic = struct
include Custom.Dummy
let serialize s _ = failwith "Patterns.NLineBasic.serialize"
type t = result * Types.t
let compare (r1,t1) (r2,t2) =
let c = compare_result r1 r2 in if c <> 0 then c
else Types.compare t1 t2
let equal x y = compare x y == 0
let hash (r,t) = hash_result r + 17 * Types.hash t
end
let print_nnf ppf (pl,t) =
Format.fprintf ppf "@[(pl=%a;t=%a)@]" NodeSet.dump pl Types.Print.print t
let compare_nnf (l1,t1) (l2,t2) =
let c = NodeSet.compare l1 l2 in if c <> 0 then c
else Types.compare t1 t2
module NProd = struct
type t = result * Nnf.t * Nnf.t
let hash_nnf (l,t) =
(NodeSet.hash l) + 17 * (Types.hash t)
let serialize s _ = failwith "Patterns.NLineProd.serialize"
let deserialize s = failwith "Patterns.NLineProd.deserialize"
let check x = ()
let dump ppf (r,x,y) =
Format.fprintf ppf "@[(result=%a;x=%a;y=%a)@]"
print_result r Nnf.print x Nnf.print y
module NLineBasic =
SortedList.Make(
struct
include Custom.Dummy
let serialize s _ = failwith "Patterns.NLineBasic.serialize"
type t = result * Types.t
let compare (r1,t1) (r2,t2) =
let c = compare_result r1 r2 in if c <> 0 then c
else Types.compare t1 t2
let equal x y = compare x y == 0
let hash (r,t) = hash_result r + 17 * Types.hash t
end
)
let compare (r1,x1,y1) (r2,x2,y2) =
let c = compare_result r1 r2 in if c <> 0 then c
else let c = Nnf.compare x1 x2 in if c <> 0 then c
else Nnf.compare y1 y2
let equal x y = compare x y == 0
let hash (r,x,y) = hash_result r + 17 * (Nnf.hash x) + 267 * (Nnf.hash y)
end
module NLineProd =
SortedList.Make(
struct
(* include Custom.Dummy*)
let serialize s _ = failwith "Patterns.NLineProd.serialize"
let deserialize s = failwith "Patterns.NLineProd.deserialize"
let check x = ()
let dump ppf (r,x,y) =
Format.fprintf ppf "@[(result=%a;x=%a;y=%a)@]"
print_result r
print_nnf x
print_nnf y
type t = result * nnf * nnf
let compare (r1,x1,y1) (r2,x2,y2) =
let c = compare_result r1 r2 in if c <> 0 then c
else let c = compare_nnf x1 x2 in if c <> 0 then c
else compare_nnf y1 y2
let equal x y = compare x y == 0
let hash (r,x,y) =
hash_result r + 17 * (hash_nnf x) + 267 * (hash_nnf y)
end
)
module NLineBasic = SortedList.Make(NBasic)
module NLineProd = SortedList.Make(NProd)
type record =
| RecNolabel of result option * result option
| RecLabel of label * NLineProd.t
type t = {
nfv : fv;
ncatchv: fv;
na : Types.t;
nbasic : NLineBasic.t;
nprod : NLineProd.t;
......@@ -570,39 +568,37 @@ module Normal = struct
print_record nf.nrecord
let compare_nf t1 t2 =
include Custom.Dummy
let compare_record t1 t2 = match t1,t2 with
| RecNolabel (s1,n1), RecNolabel (s2,n2) ->
(match (s1,s2,n1,n2) with
| Some r1, Some r2, _, _ -> compare_result r1 r2
| None, Some _, _, _ -> -1
| Some _, None, _, _ -> 1
| None,None,Some r1, Some r2 -> compare_result r1 r2
| None,None,None, Some _ -> -1
| None,None, Some _, None -> 1
| None,None, None, None -> 0)
| RecNolabel (_,_), _ -> -1
| _, RecNolabel (_,_) -> 1
| RecLabel (l1,p1), RecLabel (l2,p2) ->
let c = LabelPool.compare l1 l2 in if c <> 0 then c
else NLineProd.compare p1 p2
let compare t1 t2 =
if t1 == t2 then 0
else
(* TODO: reorder; remove comparison of nfv ? *)
let c = IdSet.compare t1.nfv t2.nfv in if c <> 0 then c
else let c = IdSet.compare t1.ncatchv t2.ncatchv in if c <> 0 then c
else let c = Types.compare t1.na t2.na in if c <> 0 then c
else let c = NLineBasic.compare t1.nbasic t2.nbasic in if c <> 0 then c
else let c = NLineProd.compare t1.nprod t2.nprod in if c <> 0 then c
else let c = NLineProd.compare t1.nxml t2.nxml in if c <> 0 then c
else match t1.nrecord, t2.nrecord with
| RecNolabel (s1,n1), RecNolabel (s2,n2) ->
let c = match (s1,s2) with
| None,None -> 0
| Some r1, Some r2 -> compare_result r1 r2
| None, _ -> -1
| _, None -> 1 in
if c <> 0 then c
else (match (n1,n2) with
| None,None -> 0
| Some r1, Some r2 -> compare_result r1 r2
| None, _ -> -1
| _, None -> 1)
| RecNolabel (_,_), _ -> -1
| _, RecNolabel (_,_) -> 1
| RecLabel (l1,p1), RecLabel (l2,p2) ->
let c = LabelPool.compare l1 l2 in if c <> 0 then c
else NLineProd.compare p1 p2
else compare_record t1.nrecord t2.nrecord
let fus = IdMap.union_disj
let nempty lab =
{ nfv = IdSet.empty; ncatchv = IdSet.empty;
{ nfv = IdSet.empty;
na = Types.empty;
nbasic = NLineBasic.empty;
nprod = NLineProd.empty;
......@@ -618,7 +614,6 @@ module Normal = struct
(* assert (Types.is_empty (Types.cap nf1.na nf2.na)); *)
(* assert (nf1.nfv = nf2.nfv); *)
{ nfv = nf1.nfv;
ncatchv = IdSet.cap nf1.ncatchv nf2.ncatchv;
na = Types.cup nf1.na nf2.na;
nbasic = NLineBasic.cup nf1.nbasic nf2.nbasic;
nprod = NLineProd.cup nf1.nprod nf2.nprod;
......@@ -641,12 +636,14 @@ module Normal = struct
double_fold f (NLineProd.get l1) (NLineProd.get l2)
let ncap nf1 nf2 =
let prod accu (res1,(pl1,t1),(ql1,s1)) (res2,(pl2,t2),(ql2,s2)) =
let prod accu (res1,(pl1,t1,xs1),(ql1,s1,ys1)) (res2,(pl2,t2,xs2),(ql2,s2,ys2)) =
let t = Types.cap t1 t2 in
if Types.is_empty t then accu else
let s = Types.cap s1 s2 in
if Types.is_empty s then accu else
(fus res1 res2, (NodeSet.cup pl1 pl2,t),(NodeSet.cup ql1 ql2,s))
(fus res1 res2,
(NodeSet.cup pl1 pl2, t, IdSet.cup xs1 xs2),
(NodeSet.cup ql1 ql2, s, IdSet.cup ys1 ys2))
:: accu
in
let basic accu (res1,t1) (res2,t2) =
......@@ -669,7 +666,6 @@ module Normal = struct
| _ -> assert false
in
{ nfv = IdSet.cup nf1.nfv nf2.nfv;
ncatchv = IdSet.cup nf1.ncatchv nf2.ncatchv;
na = Types.cap nf1.na nf2.na;
nbasic = NLineBasic.from_list (double_fold basic
(NLineBasic.get nf1.nbasic)
......@@ -679,134 +675,107 @@ module Normal = struct
nrecord = record nf1.nrecord nf2.nrecord;
}
let nnode p = NodeSet.singleton p, Types.descr p.accept
let nc t = NodeSet.empty, t
let nnode p xs = NodeSet.singleton p, Types.descr p.accept, xs
let nc t = NodeSet.empty, t, IdSet.empty
let ncany = nc Types.any
let ncany_abs = nc Types.Record.any_or_absent
let empty_res = IdMap.empty
let ntimes lab acc p q =
let src_p = IdMap.constant SLeft p.fv
and src_q = IdMap.constant SRight q.fv in
let single_basic src t = NLineBasic.singleton (src, t)
let single_prod src p q = NLineProd.singleton (src, p,q)
let ntimes lab acc p q xs =
let xsp = IdSet.cap xs p.fv and xsq = IdSet.cap xs q.fv in
let src_p = IdMap.constant SLeft xsp
and src_q = IdMap.constant SRight xsq in
let src = IdMap.merge_elem SRecompose src_p src_q in
{ nempty lab with
nfv = IdSet.cup p.fv q.fv;
nfv = xs;
na = acc;
nprod = NLineProd.singleton (src, nnode p, nnode q);
nprod = single_prod src (nnode p xsp) (nnode q xsq)
}
let nxml lab acc p q =
let src_p = IdMap.constant SLeft p.fv
and src_q = IdMap.constant SRight q.fv in
let nxml lab acc p q xs =
let xsp = IdSet.cap xs p.fv and xsq = IdSet.cap xs q.fv in
let src_p = IdMap.constant SLeft xsp
and src_q = IdMap.constant SRight xsq in
let src = IdMap.merge_elem SRecompose src_p src_q in
{ nempty lab with
nfv = IdSet.cup p.fv q.fv;
nfv = xs;
na = acc;
nxml = NLineProd.singleton (src, nnode p, nnode q);
nxml = single_prod src (nnode p xsp) (nnode q xsq)
}
let nrecord lab acc l p =
let nrecord lab acc l p xs =
assert (IdSet.equal xs (fv p));
match lab with
| None -> assert false
| Some label ->
assert (label <= l);
if l == label then
let src = IdMap.constant SLeft p.fv in
{ nempty lab with
nfv = p.fv;
na = acc;
nrecord = RecLabel(label,
NLineProd.singleton (src,nnode p, ncany))}
else
let src = IdMap.constant SRight p.fv in
let p' = make p.fv in (* optimize this ... *)
(* cache the results to avoid looping ... *)
define p' (record l p);
{ nempty lab with
nfv = p.fv;
na = acc;
nrecord =
RecLabel(label,
NLineProd.singleton(src,nc Types.Record.any_or_absent,
nnode p') )}
let src,lft,rgt =
if l == label
then SLeft, nnode p xs, ncany
else SRight, ncany_abs, nnode (cons p.fv (record l p)) xs
in
let src = IdMap.constant src xs in
{ nempty lab with
nfv = xs;
na = acc;
nrecord = RecLabel(label, single_prod src lft rgt) }
let nconstr lab t =
let aux l = NLineProd.from_list
(List.map (fun (t1,t2) -> empty_res, nc t1,nc t2) l) in
let record =
match lab with
| None ->
let (x,y) = Types.Record.empty_cases t in
RecNolabel ((if x then Some empty_res else None),
let record = match lab with
| None ->
let (x,y) = Types.Record.empty_cases t in
RecNolabel ((if x then Some empty_res else None),
(if y then Some empty_res else None))
| Some l ->
(*
let ppf = Format.std_formatter in
Format.fprintf ppf "Constr record t=%a l=%a@."
Types.Print.print t Label.print (LabelPool.value l);
let sp = Types.Record.split_normal t l in
List.iter (fun (t1,t2) ->
Format.fprintf ppf "t1=%a t2=%a@."
Types.Print.print t1
Types.Print.print t2) sp;
*)
RecLabel (l,aux (Types.Record.split_normal t l))
in
| Some l ->
RecLabel (l,aux (Types.Record.split_normal t l)) in
{ nempty lab with
na = t;
nbasic = NLineBasic.singleton (empty_res, Types.cap t any_basic);
nbasic = single_basic empty_res (Types.cap t any_basic);
nprod = aux (Types.Product.normal t);
nxml = aux (Types.Product.normal ~kind:`XML t);
nrecord = record
}
let nconstant lab x c =
let l = IdMap.singleton x (SConst c) in
{ nfv = IdSet.singleton x;
ncatchv = IdSet.empty;
na = Types.any;
nbasic = NLineBasic.singleton (l,any_basic);
nprod = NLineProd.singleton (l,ncany,ncany);
nxml = NLineProd.singleton (l,ncany,ncany);
nrecord = match lab with
| None -> RecNolabel (Some l, Some l)
| Some lab ->
RecLabel (lab, NLineProd.singleton
(l,nc Types.Record.any_or_absent,
ncany))
}
let ncapture lab x =
let l = IdMap.singleton x SCatch in
{ nfv = IdSet.singleton x;
ncatchv = IdSet.singleton x;
let nany lab res =
{ nfv = IdMap.domain res;
na = Types.any;
nbasic = NLineBasic.singleton (l,any_basic);
nprod = NLineProd.singleton (l,ncany,ncany);
nxml = NLineProd.singleton (l,ncany,ncany);
nbasic = single_basic res any_basic;
nprod = single_prod res ncany ncany;
nxml = single_prod res ncany ncany;
nrecord = match lab with
| None -> RecNolabel (Some l, Some l)
| Some lab ->
RecLabel (lab, NLineProd.singleton
(l,nc Types.Record.any_or_absent,
ncany))
| None -> RecNolabel (Some res, Some res)
| Some lab -> RecLabel (lab, single_prod res ncany_abs ncany)
}
let rec nnormal lab (acc,fv,d) =
if Types.is_empty acc
then nempty lab
let nconstant lab x c = nany lab (IdMap.singleton x (SConst c))
let ncapture lab x = nany lab (IdMap.singleton x SCatch)
let rec nnormal lab ((acc,fv,d) as p) xs =
let xs = IdSet.cap xs fv in
if not (IdSet.equal xs fv) then
(Format.fprintf Format.std_formatter
"ERR: p=%a xs=%a fv=%a@." Print.print p Print.print_xs xs Print.print_xs fv;
exit 1);
if Types.is_empty acc then nempty lab
else if IdSet.is_empty xs then nconstr lab acc
else match d with
| Constr t -> nconstr lab t
| Cap (p,q) -> ncap (nnormal lab p) (nnormal lab q)
| Constr t -> assert false
| Cap (p,q) -> ncap (nnormal lab p xs) (nnormal lab q xs)
| Cup ((acc1,_,_) as p,q) ->
ncup (nnormal lab p) (ncap (nnormal lab q)
(nconstr lab (Types.neg acc1)))
| Times (p,q) -> ntimes lab acc p q
| Xml (p,q) -> nxml lab acc p q
ncup
(nnormal lab p xs)
(ncap (nnormal lab q xs) (nconstr lab (Types.neg acc1)))
| Times (p,q) -> ntimes lab acc p q xs
| Xml (p,q) -> nxml lab acc p q xs
| Capture x -> ncapture lab x
| Constant (x,c) -> nconstant lab x c
| Record (l,p) -> nrecord lab acc l p
| Record (l,p) -> nrecord lab acc l p xs
| Dummy -> assert false
(*TODO: when an operand of Cap has its first_label > lab,
......@@ -824,39 +793,14 @@ module Normal = struct
| _ -> LabelPool.dummy_max
let remove_catchv n =
let ncv = n.ncatchv in
let nlinesbasic l =
NLineBasic.map (fun (res,x) -> (IdMap.diff res ncv,x)) l in
let nlinesprod l =
NLineProd.map (fun (res,x,y) -> (IdMap.diff res ncv,x,y)) l in
{ nfv = IdSet.diff n.nfv ncv;
ncatchv = n.ncatchv;
na = n.na;
nbasic = nlinesbasic n.nbasic;
nprod = nlinesprod n.nprod;
nxml = nlinesprod n.nxml;
nrecord = (match n.nrecord with
| RecNolabel (x,y) ->
let x = match x with
| Some res -> Some (IdMap.diff res ncv)
| None -> None in
let y = match y with
| Some res -> Some (IdMap.diff res ncv)
| None -> None in
RecNolabel (x,y)
| RecLabel (lab,l) -> RecLabel (lab, nlinesprod l))
}
let print_node_list ppf pl =
List.iter (fun p -> Format.fprintf ppf "%a;" Node.dump p) pl
let normal l t pl =
remove_catchv
(List.fold_left
(fun a p -> ncap a (nnormal l (descr p)))
(nconstr l t)
pl)
let normal l t pl xs =
List.fold_left
(fun a p -> ncap a (nnormal l (descr p) xs))
(nconstr l t)
pl
(*
let normal l t pl =
......@@ -1051,29 +995,9 @@ struct
let cur_id = State.ref "Patterns.cur_id" 0
(* TODO: save dispatchers ? *)
module NfMap = Map.Make(
struct
type t = Normal.t
let compare = Normal.compare_nf
end)
module DispMap = Map.Make(
struct
type t = Types.t * Normal.t array
let rec compare_rec a1 a2 i =
if i < 0 then 0
else
let c = Normal.compare_nf a1.(i) a2.(i) in
if c <> 0 then c else compare_rec a1 a2 (i - 1)
let compare (t1,a1) (t2,a2) =
let c = Types.compare t1 t2 in if c <> 0 then c
else let l1 = Array.length a1 and l2 = Array.length a2 in
if l1 < l2 then -1 else if l1 > l2 then 1
else compare_rec a1 a2 (l1 - 1)
end
)
module NfMap = Map.Make(Normal)
module DispMap = Map.Make(Custom.Pair(Types)(Custom.Array(Normal)))
(* Try with a hash-table ! *)
......@@ -1227,14 +1151,14 @@ struct
let get_tests pl f t d post =
let accu = ref [] in
let aux i x =
let (pl,ty), info = f x in
let (pl,ty,xs), info = f x in
let pl = Normal.NodeSet.get pl in
accu := (ty,pl,i,info) :: !accu in
accu := (ty,pl,xs,i,info) :: !accu in
Array.iteri (fun i -> List.iter (aux i)) pl;
let lab =
List.fold_left
(fun l (ty,pl,_,_) ->
(fun l (ty,pl,_,_,_) ->
List.fold_left
(fun l p -> min l (Normal.first_label (descr p)))
(min l (Types.Record.first_label ty))
......@@ -1246,9 +1170,9 @@ struct
let pats = ref NfMap.empty in
let nb_p = ref 0 in
List.iter
(fun (ty,pl,i,info) ->
let p = Normal.normal lab ty pl in
let x = (i, p.Normal.ncatchv, info) in
(fun (ty,pl,xs,i,info) ->
let p = Normal.normal lab ty pl xs in
let x = (i, IdSet.empty (* p.Normal.ncatchv *) , info) in
try
let s = NfMap.find p !pats in
s := x :: !s
......@@ -1283,11 +1207,8 @@ struct
let (_,brs) =
List.fold_left
(fun (t,brs) (p,e) ->
let p' = (Normal.NodeSet.singleton p,t) in
(* let td = Types.descr (accept p) in
let t' =