(* TODO: - rewrite type-checking of operators to propagate constraint - check whether it is worth using recursive hash-consing internally *) open Location open Ast open Ident let (=) (x:int) y = x = y let (<=) (x:int) y = x <= y let (<) (x:int) y = x < y let (>=) (x:int) y = x >= y let (>) (x:int) y = x > y let debug_schema = false let warning loc msg = let v = Location.get_viewport () in let ppf = if Html.is_html v then Html.ppf v else Format.err_formatter in Format.fprintf ppf "Warning %a:@\n" Location.print_loc (loc,`Full); Location.html_hilight (loc,`Full); Format.fprintf ppf "%s@." msg exception NonExhaustive of Types.descr exception Constraint of Types.descr * Types.descr exception ShouldHave of Types.descr * string exception ShouldHave2 of Types.descr * string * Types.descr exception WrongLabel of Types.descr * label exception UnboundId of id * bool exception UnboundExtId of Types.CompUnit.t * id exception Error of string exception Warning of string * Types.t let raise_loc loc exn = raise (Location (loc,`Full,exn)) let raise_loc_str loc ofs exn = raise (Location (loc,`Char ofs,exn)) let error loc msg = raise_loc loc (Error msg) type item = | Type of Types.t | Val of Types.t type ext = | ECDuce of Types.CompUnit.t (* CDuce unit *) | EOCaml of string (* OCaml module *) | ESchema of string (* XML Schema *) module UEnv = Map.Make(U) type t = { ids : item Env.t; ns: Ns.table; cu: ext UEnv.t; } let hash _ = failwith "Typer.hash" let compare _ _ = failwith "Typer.compare" let dump ppf _ = failwith "Typer.dump" let equal _ _ = failwith "Typer.equal" let check _ = failwith "Typer.check" let load_schema_fwd = ref (fun x uri -> assert false) let enter_schema x uri env = let sch = !load_schema_fwd x uri in { env with cu = UEnv.add x (ESchema uri) env.cu } (* TODO: filter out builtin defs ? *) let serialize_item s = function | Type t -> Serialize.Put.bits 1 s 0; Types.serialize s t | Val t -> Serialize.Put.bits 1 s 1; Types.serialize s t let serialize s env = Serialize.Put.env Id.serialize serialize_item Env.iter s env.ids; Ns.serialize_table s env.ns; let schs = UEnv.fold (fun name cu accu -> match cu with ESchema uri -> (name,uri)::accu | _ -> accu) env.cu [] in Serialize.Put.list (Serialize.Put.pair U.serialize Serialize.Put.string) s schs let deserialize_item s = match Serialize.Get.bits 1 s with | 0 -> Type (Types.deserialize s) | 1 -> Val (Types.deserialize s) | _ -> assert false let deserialize s = let ids = Serialize.Get.env Id.deserialize deserialize_item Env.add Env.empty s in let ns = Ns.deserialize_table s in let schs = Serialize.Get.list (Serialize.Get.pair U.deserialize Serialize.Get.string) s in let env = { ids = ids; ns = ns; cu = UEnv.empty } in List.fold_left (fun env (name,uri) -> enter_schema name uri env) env schs let empty_env = { ids = Env.empty; ns = Ns.empty_table; cu = UEnv.empty; } let from_comp_unit = ref (fun (cu : Types.CompUnit.t) -> assert false) let has_comp_unit = ref (fun cu -> assert false) let has_ocaml_unit = ref (fun cu -> false) let has_static_external = ref (fun _ -> assert false) let enter_cu x cu env = { env with cu = UEnv.add x (ECDuce cu) env.cu } let find_cu loc x env = try UEnv.find x env.cu with Not_found -> if !has_comp_unit x then (ECDuce (Types.CompUnit.mk x)) else if !has_ocaml_unit x then (EOCaml (U.get_str x)) else error loc ("Cannot find external unit " ^ (U.to_string x)) let find_schema x env = try (match UEnv.find x env.cu with | ESchema s -> s | _ -> raise Not_found) with Not_found -> raise (Error (Printf.sprintf "%s: no such schema" (U.to_string x))) let enter_type id t env = { env with ids = Env.add id (Type t) env.ids } let enter_types l env = { env with ids = List.fold_left (fun accu (id,t) -> Env.add id (Type t) accu) env.ids l } let find_type id env = match Env.find id env.ids with | Type t -> t | Val _ -> raise Not_found let enter_value id t env = { env with ids = Env.add id (Val t) env.ids } let enter_values l env = { env with ids = List.fold_left (fun accu (id,t) -> Env.add id (Val t) accu) env.ids l } let enter_values_dummy l env = { env with ids = List.fold_left (fun accu id -> Env.add id (Val Types.empty) accu) env.ids l } let find_value id env = match Env.find id env.ids with | Val t -> t | _ -> raise Not_found let find_value_global loc cu id env = try find_value id (!from_comp_unit cu) with Not_found -> raise_loc loc (UnboundExtId (cu,id)) let value_name_ok id env = try match Env.find id env.ids with | Val t -> true | _ -> false with Not_found -> true let iter_values env f = Env.iter (fun x -> function Val t -> f x t; | _ -> ()) env.ids let register_types cu env = Env.iter (fun x t -> match t with | Type t -> Types.Print.register_global cu (Ident.value x) t | _ -> ()) env.ids (* Namespaces *) let set_ns_table_for_printer env = Ns.InternalPrinter.set_table env.ns let get_ns_table tenv = tenv.ns let enter_ns p ns env = { env with ns = Ns.add_prefix p ns env.ns } let protect_error_ns loc f x = try f x with Ns.UnknownPrefix ns -> raise_loc_generic loc ("Undefined namespace prefix " ^ (U.to_string ns)) let qname env loc t = protect_error_ns loc (Ns.map_tag env.ns) t let ident env loc t = let q = protect_error_ns loc (Ns.map_attr env.ns) t in Ident.ident q let has_value id env = try match Env.find (Ident.ident (Ns.map_attr env.ns id)) env.ids with | Val t -> true | _ -> false with Not_found | Ns.UnknownPrefix _ -> false let parse_atom env loc t = Atoms.V.of_qname (qname env loc t) let parse_ns env loc ns = protect_error_ns loc (Ns.map_prefix env.ns) ns let parse_label env loc t = let (ns,l) = protect_error_ns loc (Ns.map_attr env.ns) t in LabelPool.mk (ns,l) let parse_record env loc f r = let r = List.map (fun (l,x) -> (parse_label env loc l, f x)) r in LabelMap.from_list (fun _ _ -> raise_loc_generic loc "Duplicated record field") r let rec const env loc = function | LocatedExpr (loc,e) -> const env loc e | Pair (x,y) -> Types.Pair (const env loc x, const env loc y) | Xml (x,y) -> Types.Xml (const env loc x, const env loc y) | RecordLitt x -> Types.Record (parse_record env loc (const env loc) x) | String (i,j,s,c) -> Types.String (i,j,s,const env loc c) | Atom t -> Types.Atom (parse_atom env loc t) | Integer i -> Types.Integer i | Char c -> Types.Char c | Const c -> c | _ -> raise_loc_generic loc "This should be a scalar or structured constant" (* I. Transform the abstract syntax of types and patterns into the internal form *) (* Schema *) (* uri -> schema binding *) let schemas = Hashtbl.create 3 let find_schema_descr uri (name : Ns.qname) = try let sch = snd (Hashtbl.find schemas uri) in fst (Env.find (Ident.ident name) sch) with Not_found -> raise (Error (Printf.sprintf "No component named '%s' found in schema '%s'" (Ns.QName.to_string name) uri)) let find_type_global loc cu id env = match find_cu loc cu env with | ECDuce cu -> find_type id (!from_comp_unit cu) | EOCaml _ -> error loc "OCaml units don't export types" (* TODO *) | ESchema s -> find_schema_descr s (Ident.value id) module IType = struct type node = { mutable desc: desc; mutable smallhash: int; (* Local hash *) mutable rechash: int; (* Global (recursive) hash *) mutable sid: int; (* Sequential id used to compute rechash *) mutable t: Types.t option; mutable tnode: Types.Node.t option; mutable p: Patterns.descr option; mutable pnode: Patterns.node option; mutable fv: fv option } and desc = | ILink of node | IType of Types.descr * int | IOr of node * node | IAnd of node * node | IDiff of node * node | ITimes of node * node | IXml of node * node | IArrow of node * node | IOptional of node | IRecord of bool * (node * node option) label_map | ICapture of id | IConstant of id * Types.const let rec node_temp = { desc = ILink node_temp; smallhash = 0; rechash = 0; sid = 0; t = None; tnode = None; p = None; pnode = None; fv = None } (* Recursive hash-consing *) let hash_field f = function | (p, Some e) -> 1 + 17 * f p + 257 * f e | (p, None) -> 2 + 17 * f p let rec hash f n = match n.desc with | ILink n -> hash f n | IType (t,h) -> 1 + 17 * h | IOr (p1,p2) -> 2 + 17 * f p1 + 257 * f p2 | IAnd (p1,p2) -> 3 + 17 * f p1 + 257 * f p2 | IDiff (p1,p2) -> 4 + 17 * f p1 + 257 * f p2 | ITimes (p1,p2) -> 5 + 17 * f p1 + 257 * f p2 | IXml (p1,p2) -> 6 + 17 * f p1 + 257 * f p2 | IArrow (p1,p2) -> 7 + 17 * f p1 + 257 * f p2 | IOptional p -> 8 + 17 * f p | IRecord (o,r)->9+(if o then 17 else 0)+ 257*(LabelMap.hash (hash_field f) r) | ICapture x -> 10 + 17 * (Id.hash x) | IConstant (x,c) -> 11 + 17 * (Id.hash x) + 257*(Types.Const.hash c) let hash0 = hash (fun n -> 1) let hash1 = hash hash0 let hash2 = hash hash1 let hash3 = hash hash2 let smallhash n = if n.smallhash !=0 then n.smallhash else ( let h = hash2 n in n.smallhash <- h; h ) let rec repr = function | { desc = ILink n } as m -> let z = repr n in m.desc <- ILink z; z | n -> n let back = ref [] let rec prot_repr = function | { desc = ILink n } -> repr n | n -> n let link x y = match x,y with | { t = None } as x, y | y, ({ t = None } as x) -> back := (x,x.desc) :: !back; x.desc <- ILink y | _ -> assert false exception Unify let rec unify x y = if x == y then () else let x = prot_repr x and y = prot_repr y in if x == y then () else if (smallhash x != smallhash y) then raise Unify else if (x.t != None) && (y.t != None) then raise Unify (* x and y have been internalized; if they were equivalent, they would be equal *) else match x.desc,y.desc with | IType (tx,_), IType (ty,_) when Types.equal tx ty -> link x y | IOr (x1,x2), IOr (y1,y2) | IAnd (x1,x2), IAnd (y1,y2) | IDiff (x1,x2), IDiff (y1,y2) | ITimes (x1,x2), ITimes (y1,y2) | IXml (x1,x2), IXml (y1,y2) | IArrow (x1,x2), IArrow (y1,y2) -> link x y; unify x1 y1; unify x2 y2 | IOptional x1, IOptional y1 -> link x y; unify x1 y1 | IRecord (xo,xr), IRecord (yo,yr) when xo == yo -> link x y; LabelMap.may_collide unify_field Unify xr yr | ICapture xv, ICapture yv when Id.equal xv yv -> () | IConstant (xv,xc), IConstant (yv,yc) when Id.equal xv yv && Types.Const.equal xc yc -> () | _ -> raise Unify and unify_field f1 f2 = match f1,f2 with | (p1, Some e1), (p2, Some e2) -> unify p1 p2; unify e1 e2 | (p1, None), (p2, None) -> unify p1 p2 | _ -> raise Unify let may_unify x y = try unify x y; back := []; true with Unify -> List.iter (fun (x,xd) -> x.desc <- xd) !back; back := []; false module SmallHash = Hashtbl.Make( struct type t = node let equal = may_unify let hash = smallhash end ) let iter_field f = function | (x, Some y) -> f x; f y | (x, None) -> f x let iter f = function | IOr (x,y) | IAnd (x,y) | IDiff (x,y) | ITimes (x,y) | IXml (x,y) | IArrow (x,y) -> f x; f y | IOptional x -> f x | IRecord (_,r) -> LabelMap.iter (iter_field f) r | _ -> () let minimize ((mem,add) as h) = let rec aux n = let n = repr n in if mem n then () else ( let n = repr n in add n (); if n.t == None then iter aux n.desc ) in aux let to_clear = ref [] let sid = ref 0 let rec rechash n = let n = repr n in if (n.sid != 0) then 17 * n.sid else (incr sid; n.sid <- !sid; to_clear := n :: !to_clear; hash rechash n) let clear () = sid := 0; List.iter (fun x -> x.sid <- 0) !to_clear; to_clear := [] let rechash n = let n = repr n in if (n.rechash != 0) then n.rechash else (let h = rechash n in clear (); n.rechash <- h; h) module RecHash = Hashtbl.Make( struct type t = node let equal = may_unify let hash = smallhash end ) (** Two-phases recursive hash-consing **) (* let gtable = RecHash.create 17577 let internalize n = let local = SmallHash.create 17 in minimize (SmallHash.mem local, SmallHash.add local) n; minimize (RecHash.mem gtable, RecHash.add gtable) n; () *) (** Single-phase hash-consing **) let gtable = SmallHash.create 17 let internalize n = minimize (SmallHash.mem gtable, SmallHash.add gtable) n (* let internalize n = () *) (* Compute free variables *) let fv n = let fv = ref IdSet.empty in let rec aux n = let n = repr n in if (n.sid = 0) then ( n.sid <- 1; to_clear := n :: !to_clear; match n.fv, n.desc with | Some x, _ -> fv := IdSet.cup !fv x | None, (ICapture x | IConstant (x,_)) -> fv := IdSet.add x !fv | None, d -> iter aux d ) in assert(!to_clear == []); match n.fv with | Some x -> x | None -> aux n; clear (); n.fv <- Some !fv; !fv (* optimized version to check closedness *) let no_fv = Some IdSet.empty exception FoundFv of id let peek_fv n = let err x = raise (FoundFv x) in let rec aux n = let n = repr n in if (n.sid = 0) then ( n.sid <- 1; to_clear := n :: !to_clear; match n.fv, n.desc with | Some x, _ when IdSet.is_empty x -> () | Some x, _ -> err (IdSet.choose x) | None, (ICapture x | IConstant (x,_)) -> err x; | None, d -> iter aux d ) in assert(!to_clear == []); try match n.fv with | Some x when IdSet.is_empty x -> () | Some x -> err (IdSet.choose x) | None -> aux n; List.iter (fun n -> n.sid <- 0; n.fv <- no_fv) !to_clear; to_clear := [] with exn -> clear (); raise exn let check_no_fv loc n = try peek_fv n with FoundFv x -> raise_loc_generic loc ("Capture variable not allowed: " ^ (Ident.to_string x)) let has_no_fv n = try peek_fv n; true with FoundFv _ -> false (* From the intermediate representation to the internal one *) let rec typ n = let n = repr n in match n.t with | Some t -> t | None -> let t = compute_typ n.desc in n.t <- Some t; t and compute_typ = function | IType (t,_) -> t | IOr (s1,s2) -> Types.cup (typ s1) (typ s2) | IAnd (s1,s2) -> Types.cap (typ s1) (typ s2) | IDiff (s1,s2) -> Types.diff (typ s1) (typ s2) | ITimes (s1,s2) -> Types.times (typ_node s1) (typ_node s2) | IXml (s1,s2) -> Types.xml (typ_node s1) (typ_node s2) | IArrow (s1,s2) -> Types.arrow (typ_node s1) (typ_node s2) | IOptional s -> Types.Record.or_absent (typ s) | IRecord (o,r) -> Types.record' (o, LabelMap.map compute_typ_field r) | ILink _ -> assert false | ICapture _ | IConstant (_,_) -> assert false and compute_typ_field = function | (s, None) -> typ_node s | (s, Some _) -> raise (Patterns.Error "Or-else clauses are not allowed in types") and typ_node n = let n = repr n in match n.tnode with | Some t -> t | None -> let x = Types.make () in n.tnode <- Some x; Types.define x (typ n); x let rec pat n = let n = repr n in if IdSet.is_empty (fv n) then Patterns.constr (typ n) else match n.p with | Some p -> p | None -> let p = compute_pat n.desc in n.p <- Some p; p and compute_pat = function | IOr (s1,s2) -> Patterns.cup (pat s1) (pat s2) | IAnd (s1,s2) -> Patterns.cap (pat s1) (pat s2) | IDiff (s1,s2) when IdSet.is_empty (fv s2) -> let s2 = Types.neg (typ s2) in Patterns.cap (pat s1) (Patterns.constr s2) | IDiff _ -> raise (Patterns.Error "Differences are not allowed in patterns") | ITimes (s1,s2) -> Patterns.times (pat_node s1) (pat_node s2) | IXml (s1,s2) -> Patterns.xml (pat_node s1) (pat_node s2) | IOptional _ -> raise (Patterns.Error "Optional fields are not allowed in record patterns") | IRecord (o,r) -> let pats = ref [] in let aux l = function | (s,None) -> if IdSet.is_empty (fv s) then typ_node s else ( pats := Patterns.record l (pat_node s) :: !pats; Types.any_node ) | (s,Some e) -> if IdSet.is_empty (fv s) then raise (Patterns.Error "Or-else clauses are not allowed in types") else ( pats := Patterns.cup (Patterns.record l (pat_node s)) (pat e) :: !pats; Types.Record.any_or_absent_node ) in let constr = Types.record' (o,LabelMap.mapi aux r) in List.fold_left Patterns.cap (Patterns.constr constr) !pats (* TODO: can avoid constr when o=true, and all fields have fv *) | ICapture x -> Patterns.capture x | IConstant (x,c) -> Patterns.constant x c | IArrow _ -> raise (Patterns.Error "Arrows are not allowed in patterns") | IType _ | ILink _ -> assert false and pat_node n = let n = repr n in match n.pnode with | Some p -> p | None -> let x = Patterns.make (fv n) in try n.pnode <- Some x; Patterns.define x (pat n); x with exn -> n.pnode <- None; raise exn (* From AST to the intermediate representation *) type penv = { penv_tenv : t; penv_derec : node Env.t; } let penv tenv = { penv_tenv = tenv; penv_derec = Env.empty } let mk d = { node_temp with desc = d } let mk_delayed () = { node_temp with desc = ILink node_temp } let itype t = mk (IType (t, Types.hash t)) let iempty = itype Types.empty let ior p1 p2 = if p1.desc == iempty.desc then p2 else if p2.desc == iempty.desc then p1 else mk (IOr (p1,p2)) let iand p1 p2 = if (p1.desc == iempty.desc) || (p2.desc == iempty.desc) then iempty else mk (IAnd (p1,p2)) type regexp = | PElem of node | PGuard of node | PSeq of regexp list | PAlt of regexp list | PStar of regexp | PWeakStar of regexp let rec nullable = function | PElem _ -> false | PSeq rl -> List.for_all nullable rl | PAlt rl -> List.exists nullable rl | PStar _ | PWeakStar _ | PGuard _ -> true let eps = PSeq [] let emp = PAlt [] let seq r1 r2 = let r1 = match r1 with PSeq l -> l | x -> [ x ] in let r2 = match r2 with PSeq l -> l | x -> [ x ] in match r1 @ r2 with | [ x ] -> x | l -> PSeq l let alt r1 r2 = let r1 = match r1 with PAlt l -> l | x -> [ x ] in let r2 = match r2 with PAlt l -> l | x -> [ x ] in match r1 @ r2 with | [ x ] -> x | l -> PAlt l let rec merge_alt = function | PElem p::PElem q::l -> merge_alt (PElem (ior p q) :: l) | r::l -> r::(merge_alt l) | [] -> [] (* Works only for types, not patterns, because [ (x&Int|_) R' ] is possible *) let rec simplify_regexp = function | PSeq l -> PSeq (List.map simplify_regexp l) | PAlt l -> PAlt (merge_alt (List.map simplify_regexp l)) | PStar r | PWeakStar r -> PStar (simplify_regexp r) | x -> x let rec print_regexp ppf = function | PElem _ -> Format.fprintf ppf "Elem" | PGuard _ -> Format.fprintf ppf "Guard" | PSeq l -> Format.fprintf ppf "Seq(%a)" print_regexp_list l | PAlt l -> Format.fprintf ppf "Alt(%a)" print_regexp_list l | PStar r -> Format.fprintf ppf "Star(%a)" print_regexp r | PWeakStar r -> Format.fprintf ppf "WStar(%a)" print_regexp r and print_regexp_list ppf l = List.iter (fun x -> Format.fprintf ppf "%a;" print_regexp x) l let rec remove_regexp r q = match r with | PElem p -> mk (ITimes (p, q)) | PGuard p -> iand p q | PSeq l -> List.fold_right (fun r a -> remove_regexp r a) l q | PAlt rl -> List.fold_left (fun a r -> ior a (remove_regexp r q)) iempty rl | PStar r -> let x = mk_delayed () in let res = ior x q in x.desc <- ILink (remove_regexp_nullable r res iempty); res | PWeakStar r -> let x = mk_delayed () in let res = ior q x in x.desc <- ILink (remove_regexp_nullable r res iempty); res and remove_regexp_nullable r q_nonempty q_empty = if nullable r then remove_regexp2 r q_nonempty q_empty else remove_regexp r q_nonempty and remove_regexp2 r q_nonempty q_empty = (* Assume r is nullable *) if q_nonempty == q_empty then remove_regexp r q_nonempty else match r with | PSeq [] -> q_empty | PElem p -> assert false | PGuard p -> iand p q_empty | PSeq (r::rl) -> remove_regexp2 r (remove_regexp (PSeq rl) q_nonempty) (remove_regexp2 (PSeq rl) q_nonempty q_empty) | PAlt rl -> List.fold_left (fun a r -> ior a (remove_regexp_nullable r q_nonempty q_empty)) iempty rl | PStar r -> let x = mk_delayed () in x.desc <- ILink (remove_regexp_nullable r (ior x q_nonempty) iempty); ior x q_empty | PWeakStar r -> let x = mk_delayed () in x.desc <- ILink (remove_regexp_nullable r (ior q_nonempty x) iempty); ior q_empty x let cst_nil = Types.Atom Sequence.nil_atom let capture_all vars p = IdSet.fold (fun p x -> iand p (mk (ICapture x))) p vars let termin b vars p = if b then p else IdSet.fold (fun p x -> seq p (PGuard (mk (IConstant (x,cst_nil))))) p vars let rexp r = remove_regexp r (itype Sequence.nil_type) let all_delayed = ref [] let clean_on_err () = all_delayed := [] let delayed loc = let s = mk_delayed () in all_delayed := (loc,s) :: !all_delayed; s let check_one_delayed (loc,p) = let rec aux q = if p == q then raise Exit; aux2 q.desc and aux2 = function | IOr (q1,q2) | IAnd (q1,q2) | IDiff (q1,q2) -> aux q1; aux q2 | ILink q -> aux q | _ -> () in try aux2 p.desc with Exit -> error loc "Ill-formed recursion" let check_delayed () = let l = !all_delayed in all_delayed := []; List.iter check_one_delayed l let rec derecurs env p = match p.descr with | PatVar (cu,v) -> derecurs_var env p.loc cu v (* | SchemaVar (kind, schema_name, component_name) -> let name = qname env.penv_tenv p.loc component_name in itype (find_schema_descr env.penv_tenv kind schema_name name) *) | Recurs (p,b) -> derecurs (derecurs_def env b) p | Internal t -> itype t | NsT ns -> itype (Types.atom (Atoms.any_in_ns (parse_ns env.penv_tenv p.loc ns))) | Or (p1,p2) -> mk (IOr (derecurs env p1, derecurs env p2)) | And (p1,p2) -> mk (IAnd (derecurs env p1, derecurs env p2)) | Diff (p1,p2) -> mk (IDiff (derecurs env p1, derecurs env p2)) | Prod (p1,p2) -> mk (ITimes (derecurs env p1, derecurs env p2)) | XmlT (p1,p2) -> mk (IXml (derecurs env p1, derecurs env p2)) | Arrow (p1,p2) -> mk (IArrow (derecurs env p1, derecurs env p2)) | Optional p -> mk (IOptional (derecurs env p)) | Record (o,r) -> let aux = function | (p,Some e) -> (derecurs env p, Some (derecurs env e)) | (p,None) -> derecurs env p, None in mk (IRecord (o, parse_record env.penv_tenv p.loc aux r)) | Constant (x,c) -> mk (IConstant (ident env.penv_tenv p.loc x, const env.penv_tenv p.loc c)) | Cst c -> itype (Types.constant (const env.penv_tenv p.loc c)) | Regexp r -> let r,_ = derecurs_regexp IdSet.empty false IdSet.empty true env r in rexp r and derecurs_regexp vars b rvars f env = function (* - vars: seq variables to be propagated top-down and added to each captured element - b: below a star ? - rvars: seq variables that appear on the right of the regexp - f: tail position returns the set of seq variable of the regexp minus rvars (they have already been terminated if not below a star) *) | Epsilon -> PSeq [], IdSet.empty | Elem p -> PElem (capture_all vars (derecurs env p)), IdSet.empty | Guard p -> PGuard (derecurs env p), IdSet.empty | Seq (p1,p2) -> let (p2,v2) = derecurs_regexp vars b rvars f env p2 in let (p1,v1) = derecurs_regexp vars b (IdSet.cup rvars v2) false env p1 in seq p1 p2, IdSet.cup v1 v2 | Alt (p1,p2) -> let (p1,v1) = derecurs_regexp vars b rvars f env p1 and (p2,v2) = derecurs_regexp vars b rvars f env p2 in alt (termin b (IdSet.diff v2 v1) p1) (termin b (IdSet.diff v1 v2) p2), IdSet.cup v1 v2 | Star p -> let (p,v) = derecurs_regexp vars true rvars false env p in termin b v (PStar p), v | WeakStar p -> let (p,v) = derecurs_regexp vars true rvars false env p in termin b v (PWeakStar p), v | SeqCapture (loc,x,p) -> let x = ident env.penv_tenv loc x in let vars = if f then vars else IdSet.add x vars in let after = IdSet.mem rvars x in let rvars = IdSet.add x rvars in let (p,v) = derecurs_regexp vars b rvars false env p in (if f then seq (PGuard (mk (ICapture x))) p else termin (after || b) (IdSet.singleton x) p), (if after then v else IdSet.add x v) and derecurs_var env loc cu v = let v = ident env.penv_tenv loc v in match cu with | None -> (try Env.find v env.penv_derec with Not_found -> try itype (find_type v env.penv_tenv) with Not_found -> mk (ICapture v)) | Some cu -> (try itype (find_type_global loc cu v env.penv_tenv) with Not_found -> raise_loc_generic loc ("Unbound external type " ^ (U.get_str cu) ^ "." ^ (Ident.to_string v))) and derecurs_def env b = let seen = ref IdSet.empty in let b = List.map (fun (loc,v,p) -> let v = ident env.penv_tenv loc v in if IdSet.mem !seen v then raise_loc_generic loc ("Multiple definitions for the type identifer " ^ (Ident.to_string v)); seen := IdSet.add v !seen; (v,p,delayed loc)) b in let n = List.fold_left (fun env (v,p,s) -> Env.add v s env) env.penv_derec b in let env = { env with penv_derec = n } in List.iter (fun (v,p,s) -> s.desc <- ILink (derecurs env p)) b; env let derec penv p = let d = derecurs penv p in check_delayed (); internalize d; d (* API *) module Ids = Set.Make(Id) let type_defs env b = let penv = derecurs_def (penv env) b in let aux t = let d = derec penv t in check_no_fv t.loc d; try typ d with Patterns.Error s -> raise_loc_generic t.loc s in let b = List.map (fun (loc,v,p) -> let t = aux p in if (loc <> noloc) && (Types.is_empty t) then warning loc ("This definition yields an empty type for " ^ (U.to_string v)); let v = ident env loc v in (v,t)) b in List.iter (fun (v,t) -> Types.Print.register_global (Types.CompUnit.get_current ()) (Id.value v) t) b; b let type_defs env b = try type_defs env b with exn -> clean_on_err (); raise exn let typ_descr d = try internalize d; typ d with exn -> clean_on_err (); raise exn let typ env t = try let d = derec (penv env) t in check_no_fv t.loc d; try typ_node d with Patterns.Error s -> raise_loc_generic t.loc s with exn -> clean_on_err (); raise exn let pat env t = try let d = derec (penv env) t in try pat_node d with Patterns.Error s -> raise_loc_generic t.loc s with exn -> clean_on_err (); raise exn end let typ = IType.typ let pat = IType.pat let type_defs = IType.type_defs let dump_types ppf env = Env.iter (fun v -> function (Type _) -> Format.fprintf ppf " %a" Ident.print v | _ -> ()) env.ids let dump_ns ppf env = Ns.dump_table ppf env.ns (* II. Build skeleton *) type type_fun = Types.t -> bool -> Types.t module Fv = IdSet type branch = Branch of Typed.branch * branch list let cur_branch : branch list ref = ref [] let exp' loc e = { Typed.exp_loc = loc; Typed.exp_typ = Types.empty; Typed.exp_descr = e; } let exp loc fv e = fv, exp' loc e let exp_nil = exp' noloc (Typed.Cst Sequence.nil_cst) let pat_true = let n = Patterns.make Fv.empty in Patterns.define n (Patterns.constr Builtin_defs.true_type); n let pat_false = let n = Patterns.make Fv.empty in Patterns.define n (Patterns.constr Builtin_defs.false_type); n let ops = Hashtbl.create 13 let register_op op arity f = Hashtbl.add ops op (arity,f) let typ_op op = snd (Hashtbl.find ops op) let fun_name env a = match a.fun_name with | None -> None | Some (loc,s) -> Some (ident env loc s) let is_op env s = if (Env.mem s env.ids) then None else let (ns,s) = Id.value s in if Ns.equal ns Ns.empty then let s = U.get_str s in try let o = Hashtbl.find ops s in Some (s, fst o) with Not_found -> None else None let rec expr env loc = function | LocatedExpr (loc,e) -> expr env loc e | Forget (e,t) -> let (fv,e) = expr env loc e and t = typ env t in exp loc fv (Typed.Forget (e,t)) | Check (e,t) -> let (fv,e) = expr env loc e and t = typ env t in exp loc fv (Typed.Check (ref Types.empty,e,t)) | Var s -> var env loc s | Apply (e1,e2) -> let (fv1,e1) = expr env loc e1 and (fv2,e2) = expr env loc e2 in let fv = Fv.cup fv1 fv2 in (match e1.Typed.exp_descr with | Typed.Op (op,arity,args) when arity > 0 -> exp loc fv (Typed.Op (op,arity - 1,args @ [e2])) | _ -> exp loc fv (Typed.Apply (e1,e2))) | Abstraction a -> abstraction env loc a | (Integer _ | Char _ | Atom _ | Const _) as c -> exp loc Fv.empty (Typed.Cst (const env loc c)) | Pair (e1,e2) -> let (fv1,e1) = expr env loc e1 and (fv2,e2) = expr env loc e2 in exp loc (Fv.cup fv1 fv2) (Typed.Pair (e1,e2)) | Xml (e1,e2) -> let (fv1,e1) = expr env loc e1 and (fv2,e2) = expr env loc e2 in exp loc (Fv.cup fv1 fv2) (Typed.Xml (e1,e2)) | Dot (LocatedExpr (_,Var cu), id, tyargs) when not (has_value cu env) -> (match find_cu loc cu env with | ECDuce cu -> if tyargs != [] then error loc "CDuce externals cannot have type argument"; let id = ident env loc id in let t = find_value_global loc cu id env in exp loc Fv.empty (Typed.ExtVar (cu, id, t)) | EOCaml cu -> extern loc env (cu ^ "." ^ U.get_str id) tyargs (* TODO: allow nested OCaml modules A.B.C.x *) | ESchema _ -> error loc "Schema don't export values") | Dot (e,l,[]) -> let (fv,e) = expr env loc e in exp loc fv (Typed.Dot (e,parse_label env loc l)) | Dot (_,_,_::_) -> error loc "Field access cannot have type arguments" | RemoveField (e,l) -> let (fv,e) = expr env loc e in exp loc fv (Typed.RemoveField (e,parse_label env loc l)) | RecordLitt r -> let fv = ref Fv.empty in let r = parse_record env loc (fun e -> let (fv2,e) = expr env loc e in fv := Fv.cup !fv fv2; e) r in exp loc !fv (Typed.RecordLitt r) | String (i,j,s,e) -> let (fv,e) = expr env loc e in exp loc fv (Typed.String (i,j,s,e)) | Match (e,b) -> let (fv1,e) = expr env loc e and (fv2,b) = branches env b in exp loc (Fv.cup fv1 fv2) (Typed.Match (e, b)) | Map (e,b) -> let (fv1,e) = expr env loc e and (fv2,b) = branches env b in exp loc (Fv.cup fv1 fv2) (Typed.Map (e, b)) | Transform (e,b) -> let (fv1,e) = expr env loc e and (fv2,b) = branches env b in exp loc (Fv.cup fv1 fv2) (Typed.Transform (e, b)) | Xtrans (e,b) -> let (fv1,e) = expr env loc e and (fv2,b) = branches env b in exp loc (Fv.cup fv1 fv2) (Typed.Xtrans (e, b)) | Validate (e,schema,elt) -> let (fv,e) = expr env loc e in let uri = find_schema schema env in exp loc fv (Typed.Validate (e, uri, qname env loc elt)) | SelectFW (e,from,where) -> select_from_where env loc e from where | Try (e,b) -> let (fv1,e) = expr env loc e and (fv2,b) = branches env b in exp loc (Fv.cup fv1 fv2) (Typed.Try (e, b)) | NamespaceIn (pr,ns,e) -> let env = enter_ns pr ns env in expr env loc e | Ref (e,t) -> let (fv,e) = expr env loc e and t = typ env t in exp loc fv (Typed.Ref (e,t)) and if_then_else loc cond yes no = let b = { Typed.br_typ = Types.empty; Typed.br_branches = [ { Typed.br_loc = yes.Typed.exp_loc; Typed.br_used = false; Typed.br_vars_empty = Fv.empty; Typed.br_pat = pat_true; Typed.br_body = yes }; { Typed.br_loc = no.Typed.exp_loc; Typed.br_used = false; Typed.br_vars_empty = Fv.empty; Typed.br_pat = pat_false; Typed.br_body = no } ]; Typed.br_accept = Builtin_defs.bool; } in exp' loc (Typed.Match (cond,b)) and extern loc env s args = let args = List.map (typ env) args in try let (i,t) = if !has_static_external s then (`Builtin s, Externals.typ s args) else let (i,t) = Externals.resolve s args in (`Ext i, t) in exp loc Fv.empty (Typed.External (t,i)) with exn -> raise_loc loc exn and var env loc s = let id = ident env loc s in match is_op env id with | Some (s,arity) -> let need_ns = match s with "print_xml" | "print_xml_utf8" -> true | _ -> false in let e = Typed.Op (s, arity, []) in let e = if need_ns then Typed.NsTable (env.ns,e) else e in exp loc Fv.empty e | None -> (try ignore (find_value id env) with Not_found -> raise_loc loc (UnboundId (id, Env.mem id env.ids))); exp loc (Fv.singleton id) (Typed.Var id) and abstraction env loc a = let iface = List.map (fun (t1,t2) -> (typ env t1, typ env t2)) a.fun_iface in let t = List.fold_left (fun accu (t1,t2) -> Types.cap accu (Types.arrow t1 t2)) Types.any iface in let iface = List.map (fun (t1,t2) -> (Types.descr t1, Types.descr t2)) iface in let fun_name = fun_name env a in let env' = match fun_name with | None -> env | Some f -> enter_values_dummy [ f ] env in let (fv0,body) = branches env' a.fun_body in let fv = match fun_name with | None -> fv0 | Some f -> Fv.remove f fv0 in let e = Typed.Abstraction { Typed.fun_name = fun_name; Typed.fun_iface = iface; Typed.fun_body = body; Typed.fun_typ = t; Typed.fun_fv = fv } in exp loc fv e and branches env b = let fv = ref Fv.empty in let accept = ref Types.empty in let branch (p,e) = let cur_br = !cur_branch in cur_branch := []; let ploc = p.loc in let p = pat env p in let fvp = Patterns.fv p in let (fv2,e) = expr (enter_values_dummy fvp env) noloc e in let br_loc = merge_loc ploc e.Typed.exp_loc in (match Fv.pick (Fv.diff fvp fv2) with | None -> () | Some x -> let x = Ident.to_string x in warning br_loc ("The capture variable " ^ x ^ " is declared in the pattern but not used in the body of this branch. It might be a misspelled or undeclared type or name (if it isn't, use _ instead).")); let fv2 = Fv.diff fv2 fvp in fv := Fv.cup !fv fv2; accept := Types.cup !accept (Types.descr (Patterns.accept p)); let br = { Typed.br_loc = br_loc; Typed.br_used = br_loc == noloc; Typed.br_vars_empty = fvp; Typed.br_pat = p; Typed.br_body = e } in cur_branch := Branch (br, !cur_branch) :: cur_br; br in let b = List.map branch b in (!fv, { Typed.br_typ = Types.empty; Typed.br_branches = b; Typed.br_accept = !accept; } ) and select_from_where env loc e from where = let env = ref env in let all_fv = ref Fv.empty in let bound_fv = ref Fv.empty in let clause (p,e) = let ploc = p.loc in let p = pat !env p in let fvp = Patterns.fv p in let (fv2,e) = expr !env noloc e in env := enter_values_dummy fvp !env; all_fv := Fv.cup (Fv.diff fv2 !bound_fv) !all_fv; bound_fv := Fv.cup fvp !bound_fv; (ploc,p,fvp,e) in let from = List.map clause from in let where = List.map (expr !env noloc) where in let put_cond rest (fv,cond) = all_fv := Fv.cup (Fv.diff fv !bound_fv) !all_fv; if_then_else loc cond rest exp_nil in let aux (ploc,p,fvp,e) (where,rest) = (* Put here the conditions that depends on variables in fvp *) let (above,here) = List.partition (fun (v,_) -> Fv.disjoint v fvp) where in (* if cond then ... else [] *) let rest = List.fold_left put_cond rest here in (* transform e with p -> ... *) let b = { Typed.br_typ = Types.empty; Typed.br_branches = [ { Typed.br_loc = ploc; Typed.br_used = false; Typed.br_vars_empty = fvp; Typed.br_pat = p; Typed.br_body = rest } ]; Typed.br_accept = Types.descr (Patterns.accept p); } in let br_loc = merge_loc ploc e.Typed.exp_loc in (above,exp' br_loc (Typed.Transform (e, b))) in let (fv,e) = expr !env noloc e in let (where,rest) = List.fold_right aux from (where,e) in (* The remaining conditions are constant. Gives a warning for that. *) (match where with | (_,e) :: _ -> warning e.Typed.exp_loc "This 'where' condition does not depend on any captured variable" | _ -> ()); let rest = List.fold_left put_cond rest where in (Fv.cup !all_fv (Fv.diff fv !bound_fv)), rest let expr env e = snd (expr env noloc e) let let_decl env p e = { Typed.let_pat = pat env p; Typed.let_body = expr env e } (* Hide global "typing/parsing" environment *) (* III. Type-checks *) open Typed let localize loc f x = try f x with | (Error _ | Constraint (_,_)) as exn -> raise (Location.Location (loc,`Full,exn)) | Warning (s,t) -> warning loc s; t let require loc t s = if not (Types.subtype t s) then raise_loc loc (Constraint (t, s)) let verify loc t s = require loc t s; t let verify_noloc t s = if not (Types.subtype t s) then raise (Constraint (t, s)); t let check_str loc ofs t s = if not (Types.subtype t s) then raise_loc_str loc ofs (Constraint (t, s)); t let should_have loc constr s = raise_loc loc (ShouldHave (constr,s)) let should_have_str loc ofs constr s = raise_loc_str loc ofs (ShouldHave (constr,s)) let flatten arg constr precise = let constr' = Sequence.star (Sequence.approx (Types.cap Sequence.any constr)) in let sconstr' = Sequence.star constr' in let exact = Types.subtype constr' constr in if exact then let t = arg sconstr' precise in if precise then Sequence.flatten t else constr else let t = arg sconstr' true in verify_noloc (Sequence.flatten t) constr let rec type_check env e constr precise = let d = type_check' e.exp_loc env e.exp_descr constr precise in let d = if precise then d else constr in e.exp_typ <- Types.cup e.exp_typ d; d and type_check' loc env e constr precise = match e with | Forget (e,t) -> let t = Types.descr t in ignore (type_check env e t false); verify loc t constr | Check (t0,e,t) -> let te = type_check env e Types.any true in t0 := Types.cup !t0 te; verify loc (Types.cap te (Types.descr t)) constr | Abstraction a -> let t = try Types.Arrow.check_strenghten a.fun_typ constr with Not_found -> should_have loc constr "but the interface of the abstraction is not compatible" in let env = match a.fun_name with | None -> env | Some f -> enter_value f a.fun_typ env in List.iter (fun (t1,t2) -> let acc = a.fun_body.br_accept in if not (Types.subtype t1 acc) then raise_loc loc (NonExhaustive (Types.diff t1 acc)); ignore (type_check_branches loc env t1 a.fun_body t2 false) ) a.fun_iface; t | Match (e,b) -> let t = type_check env e b.br_accept true in type_check_branches loc env t b constr precise | Try (e,b) -> let te = type_check env e constr precise in let tb = type_check_branches loc env Types.any b constr precise in Types.cup te tb | Pair (e1,e2) -> type_check_pair loc env e1 e2 constr precise | Xml (e1,e2) -> type_check_pair ~kind:`XML loc env e1 e2 constr precise | RecordLitt r -> type_record loc env r constr precise | Map (e,b) -> type_map loc env false e b constr precise | Transform (e,b) -> localize loc (flatten (type_map loc env true e b) constr) precise | Apply (e1,e2) -> let t1 = type_check env e1 Types.Arrow.any true in let t1 = Types.Arrow.get t1 in let dom = Types.Arrow.domain t1 in let res = if Types.Arrow.need_arg t1 then let t2 = type_check env e2 dom true in Types.Arrow.apply t1 t2 else (ignore (type_check env e2 dom false); Types.Arrow.apply_noarg t1) in verify loc res constr | Var s -> verify loc (find_value s env) constr | ExtVar (cu,s,t) -> verify loc t constr | Cst c -> verify loc (Types.constant c) constr | String (i,j,s,e) -> type_check_string loc env 0 s i j e constr precise | Dot (e,l) -> let t = type_check env e Types.Record.any true in let t = try (Types.Record.project t l) with Not_found -> raise_loc loc (WrongLabel(t,l)) in verify loc t constr | RemoveField (e,l) -> let t = type_check env e Types.Record.any true in let t = Types.Record.remove_field t l in verify loc t constr | Xtrans (e,b) -> let t = type_check env e Sequence.any true in let t = Sequence.map_tree (fun t -> let resid = Types.diff t b.br_accept in let res = type_check_branches loc env t b Sequence.any true in (res,resid) ) t in verify loc t constr | Validate (e, uri, name) -> ignore (type_check env e Types.any false); let t = find_schema_descr uri name in verify loc t constr | Ref (e,t) -> ignore (type_check env e (Types.descr t) false); verify loc (Builtin_defs.ref_type t) constr | External (t,_) -> verify loc t constr | Op (op,_,args) -> let args = List.map (type_check env) args in let t = localize loc (typ_op op args constr) precise in verify loc t constr | NsTable (ns,e) -> type_check' loc env e constr precise and type_check_pair ?(kind=`Normal) loc env e1 e2 constr precise = let rects = Types.Product.normal ~kind constr in if Types.Product.is_empty rects then (match kind with | `Normal -> should_have loc constr "but it is a pair" | `XML -> should_have loc constr "but it is an XML element"); let need_s = Types.Product.need_second rects in let t1 = type_check env e1 (Types.Product.pi1 rects) (precise || need_s) in let c2 = Types.Product.constraint_on_2 rects t1 in if Types.is_empty c2 then raise_loc loc (ShouldHave2 (constr,"but the first component has type",t1)); let t2 = type_check env e2 c2 precise in if precise then match kind with | `Normal -> Types.times (Types.cons t1) (Types.cons t2) | `XML -> Types.xml (Types.cons t1) (Types.cons t2) else constr and type_check_string loc env ofs s i j e constr precise = if U.equal_index i j then type_check env e constr precise else let rects = Types.Product.normal constr in if Types.Product.is_empty rects then should_have_str loc ofs constr "but it is a string" else let need_s = Types.Product.need_second rects in let (ch,i') = U.next s i in let ch = Chars.V.mk_int ch in let tch = Types.constant (Types.Char ch) in let t1 = check_str loc ofs tch (Types.Product.pi1 rects) in let c2 = Types.Product.constraint_on_2 rects t1 in let t2 = type_check_string loc env (ofs + 1) s i' j e c2 precise in if precise then Types.times (Types.cons t1) (Types.cons t2) 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 if Types.is_empty pi then (let l = Label.to_string (LabelPool.value 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 (rconstr,res) ) (constr, []) (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' (false, LabelMap.from_list (fun _ _ -> assert false) res) in verify loc t constr and type_check_branches loc env targ brs constr precise = if Types.is_empty targ then Types.empty else ( brs.br_typ <- Types.cup brs.br_typ targ; branches_aux loc env targ (if precise then Types.empty else constr) constr precise brs.br_branches ) and branches_aux loc env targ tres constr precise = function | [] -> tres | b :: rem -> let p = b.br_pat in let acc = Types.descr (Patterns.accept p) in let targ' = Types.cap targ acc in if Types.is_empty targ' then branches_aux loc env targ tres constr precise rem else ( b.br_used <- true; let res = Patterns.filter targ' p in let res = IdMap.map Types.descr res in b.br_vars_empty <- IdMap.domain ( IdMap.filter (fun x t -> Types.subtype t Sequence.nil_type) (IdMap.restrict res b.br_vars_empty)); let env' = enter_values (IdMap.get res) env in let t = type_check env' b.br_body constr precise in let tres = if precise then Types.cup t tres else tres in let targ'' = Types.diff targ acc in if (Types.non_empty targ'') then branches_aux loc env targ'' tres constr precise rem else tres ) and type_map loc env def e b constr precise = let acc = if def then Sequence.any else Sequence.star b.br_accept in let t = type_check env e acc true in let constr' = Sequence.approx (Types.cap Sequence.any constr) in let exact = Types.subtype (Sequence.star constr') constr in (* Note: - could be more precise by integrating the decomposition of constr inside Sequence.map. *) let res = Sequence.map (fun t -> let res = type_check_branches loc env t b constr' (precise || (not exact)) in if def && not (Types.subtype t b.br_accept) then (require loc Sequence.nil_type constr'; Types.cup res Sequence.nil_type) else res) t in if exact then res else verify loc res constr and type_let_decl env l = let acc = Types.descr (Patterns.accept l.let_pat) in let t = type_check env l.let_body acc true in let res = Patterns.filter t l.let_pat in IdMap.mapi_to_list (fun x t -> (x, Types.descr t)) res and type_rec_funs env l = let typs = List.fold_left (fun accu -> function | { exp_descr=Abstraction { fun_typ = t; fun_name = Some f }; exp_loc=loc } -> if not (value_name_ok f env) then error loc "This function name clashes with a type name"; (f,t)::accu | _ -> assert false ) [] l in let env = enter_values typs env in List.iter (fun e -> ignore (type_check env e Types.any false)) l; typs let rec unused_branches b = List.iter (fun (Branch (br,s)) -> if not br.br_used then warning br.br_loc "This branch is not used" else ( if not (IdSet.is_empty br.br_vars_empty) then ( let msg = try let l = List.map (fun x -> let x = Ident.to_string x in if (String.compare x "$$$" = 0) then raise Exit else x) (IdSet.get br.br_vars_empty) in let l = String.concat "," l in "The following variables always match the empty sequence: " ^ l with Exit -> "This projection always returns the empty sequence" in warning br.br_loc msg ); unused_branches s ) ) b let report_unused_branches () = unused_branches !cur_branch; cur_branch := [] let clear_unused_branches () = cur_branch := [] (* API *) let type_expr env e = clear_unused_branches (); let e = expr env e in let t = type_check env e Types.any true in report_unused_branches (); (e,t) let type_let_decl env p e = clear_unused_branches (); let decl = let_decl env p e in let typs = type_let_decl env decl in report_unused_branches (); let env = enter_values typs env in (env,decl,typs) let type_let_funs env funs = clear_unused_branches (); let rec id = function | Ast.LocatedExpr (_,e) -> id e | Ast.Abstraction a -> fun_name env a | _ -> assert false in let ids = List.fold_left (fun accu f -> match id f with Some x -> x::accu | None -> accu) [] funs in let env' = enter_values_dummy ids env in let funs = List.map (expr env') funs in let typs = type_rec_funs env funs in report_unused_branches (); let env = enter_values typs env in (env,funs,typs) (* Schema stuff from now on ... *) (** convertion from XML Schema types (including global elements and attributes) to CDuce Types.descr *) module Schema_converter = struct open Printf open Schema_types open Schema_common open Encodings open IType let xsd = Schema_xml.xsd let is_xsd (ns,l) local = (Ns.equal ns xsd) && (String.compare (Utf8.get_str l) local = 0) let complex_memo = Hashtbl.create 213 let rexp re = rexp (simplify_regexp re) (* TODO: better approx *) let xsd_any_type = Types.any let nil_type = itype Sequence.nil_type let mk_len_regexp ?min ?max base = let rec repeat_regexp re = function | 0 -> eps | n -> seq re (repeat_regexp re (pred n)) in let min = match min with Some min -> min | _ -> 1 in let min_regexp = repeat_regexp base min in match max with | Some max -> (* assert (max >= min); Need to use Bigint comparison ! -- AF *) let rec aux acc = function | 0 -> acc | n -> aux (alt eps (seq base acc)) (pred n) in seq min_regexp (aux eps (max-min)) | None -> seq min_regexp (PStar base) let mk_seq_derecurs base facets = let min,max = match facets with | { length = Some (v, _) } -> v, Some v | { minLength = Some (v, _); maxLength = None } -> v, None | { minLength = None; maxLength = Some (v, _) } -> 1, Some v | { minLength = Some (a,_); maxLength = Some (b, _) } -> a, Some b | _ -> 1, Some 1 in Sequence.repet min max base let xsi_nil_field_map = LabelMap.singleton xsi_nil_label (Types.cons Builtin_defs.true_type) let xsi_nil_field_map' = LabelMap.singleton xsi_nil_label (itype Builtin_defs.true_type, None) let pcdata = PStar (PElem (itype (Types.char Chars.any))) let mix_regexp regexp = let rec aux = function | PSeq [] -> eps | PElem re -> PElem re | PGuard re -> assert false | PSeq (r::rl) -> seq (aux r) (seq pcdata (aux (PSeq rl))) | PAlt rl -> PAlt (List.map aux rl) | PStar re -> PStar (seq pcdata (aux re)) | PWeakStar re -> PWeakStar (seq pcdata (aux re)) in seq pcdata (seq (aux regexp) pcdata) let rec simple_type = function | { st_name = Some name } when Schema_builtin.is name -> Schema_builtin.cd_type (Schema_builtin.get name) (* This is non-sense ... | Derived (_, _, { enumeration = Some values }, _) -> (* enumeration *) itype (Types.choice_of_list (List.map (fun c -> Types.constant (Value.inv_const (Lazy.force c))) values)) | Derived (_, _, ({ maxInclusive = Some _ } as facets), _)(* boundaries *) | Derived (_, _, ({ maxExclusive = Some _ } as facets), _) | Derived (_, _, ({ minInclusive = Some _ } as facets), _) | Derived (_, _, ({ minExclusive = Some _ } as facets), _) -> itype (Types.interval (Schema_common.get_interval facets)) *) | { st_variety = Atomic st } -> (* TODO: apply facets *) Schema_builtin.cd_type (Schema_builtin.of_st st) | { st_variety = List item; st_facets = facets } -> mk_seq_derecurs (simple_type item) facets | { st_variety = Union members; st_facets = facets } -> let members = List.map simple_type members in List.fold_left (fun acc x -> Types.cup x acc) Types.empty members let rec regexp_of_term = function | Model group -> regexp_of_model_group group | Elt decl -> PElem (elt_decl decl) | Wildcard w -> PElem (wildcard w) and wildcard w = itype (Builtin_defs.any_xml_with_tag w.wild_first) and regexp_of_model_group = function | Choice l -> List.fold_left (fun acc particle -> alt acc (regexp_of_particle particle)) emp l | All l | Sequence l -> List.fold_left (fun acc particle -> seq acc (regexp_of_particle particle)) eps l and regexp_of_particle p = mk_len_regexp ?min:(Some p.part_min) ?max:p.part_max (regexp_of_term p.part_term) and get_complex ct = try Hashtbl.find complex_memo ct.ct_uid with Not_found -> let slot = delayed noloc in let attrs = attr_uses ct.ct_attrs in let r = mk (ITimes (attrs,slot)) in Hashtbl.add complex_memo ct.ct_uid r; slot.desc <- ILink (content ct.ct_content); r and complex nil ct = let c = get_complex ct in if nil then match c.desc with | ITimes ({ desc = IRecord (o,fields) },content) -> let fields = LabelMap.union_disj fields xsi_nil_field_map' in ior c (mk (ITimes (mk (IRecord (o,fields)), itype Sequence.nil_type))) | _ -> assert false else c and content = function | CT_empty -> itype Sequence.nil_type | CT_simple st -> itype (simple_type st) | CT_model (particle, mixed) -> let regexp = regexp_of_particle particle in let regexp = if mixed then mix_regexp regexp else regexp in rexp regexp (** @return a closed record *) and attr_uses (attrs,other) = (* TODO: produce directly internal types *) (* (is it better ? we wouln't benefit from hash-consing) *) let fields = List.map (fun at -> let r = match at.attr_use_cstr with | Some (`Fixed v) -> itype (Types.constant (Value.inv_const v)) | _ -> itype (simple_type at.attr_decl.attr_typdef) in let r = if at.attr_required then r else mk (IOptional r) in (LabelPool.mk at.attr_decl.attr_name, (r,None))) attrs in mk (IRecord (other, LabelMap.from_list_disj fields)) and att_decl att = let r = itype (simple_type att.attr_typdef) in mk (IRecord (false, LabelMap.from_list_disj [(LabelPool.mk att.attr_name, (r,None))])) and elt_decl elt = let atom_type = itype (Types.atom (Atoms.atom (Atoms.V.of_qname elt.elt_name))) in let content = match elt.elt_cstr,elt.elt_nillable with | Some (`Fixed _), true -> failwith "Fixed value constraint and nillable are incompatible" | Some (`Fixed v), false -> itype (Types.constant (Value.inv_const v)) | _, nil -> complex_type_def nil (Lazy.force elt.elt_typdef) in mk (IXml (atom_type, content)) and complex_type_def nil = function | AnyType -> itype (Types.times (Types.cons Types.empty_opened_record) (Types.cons xsd_any_type)) | Simple st -> let nonnil = Types.times (Types.cons Types.empty_closed_record) (Types.cons (simple_type st)) in let t = if nil then Types.cup nonnil (Types.times (Types.cons (Types.record' (false,xsi_nil_field_map))) (Types.cons Sequence.nil_type)) else nonnil in itype t | Complex ct -> complex nil ct let complex_type ct = mk (IXml (itype Types.any, complex false ct)) let model_group g = rexp (regexp_of_model_group g) let typ r = check_delayed (); IType.typ_descr r let type_def = function | AnyType -> xsd_any_type | Simple st -> simple_type st | Complex ct -> typ (complex_type ct) let elt_decl x = typ (elt_decl x) let att_decl x = typ (att_decl x) let attr_uses x = typ (attr_uses x) let model_group x = typ (model_group x.mg_def) let attr_group ag = attr_uses ag.ag_def end let get_schema_names env = UEnv.fold (fun n cu acc -> match cu with ESchema _ -> n :: acc | _ -> acc) env.cu [] open Schema_types open Schema_types open Schema_common open Schema_converter open Schema_validator let register_schema schema_name uri schema = let log_schema_component kind name cd_type = if not (Schema_builtin.is name) then begin Types.Print.register_global (Types.CompUnit.mk schema_name) name cd_type; Format.fprintf Format.std_formatter "Registering schema %s: %a@." kind Ns.QName.print name; end in let env = ref Env.empty in let defs kind name cd_type v lst = List.iter (fun def -> let name = name def in let cd_type = cd_type def in log_schema_component kind name cd_type; env := Env.add (Ident.ident name) (cd_type, v def) !env ) lst in (* defs "attribute" (fun a -> a.attr_name) att_decl (fun _ _ -> assert false) schema.attributes; *) defs "attribute group" (fun ag -> ag.ag_name) attr_group validate_attribute_group schema.attribute_groups; defs "model group" (fun mg -> mg.mg_name) model_group validate_model_group schema.model_groups; defs "type" name_of_type_definition type_def validate_type schema.types; defs "element" (fun e -> e.elt_name) elt_decl validate_element schema.elements; !env let real_load_schema schema_name uri = let schema = Schema_parser.schema_of_uri uri in let types = register_schema schema_name uri schema in Hashtbl.add schemas uri (schema,types); schema let load_schema name uri = try fst (Hashtbl.find schemas uri) with Not_found -> real_load_schema name uri let get_schema_validator uri name = let name = Ident.ident name in snd (Env.find name (snd (Hashtbl.find schemas uri))) let () = load_schema_fwd := load_schema let find_cu x env = match find_cu noloc x env with | ECDuce cu -> cu | _ -> raise (Error ("Cannot find external unit " ^ (U.to_string x)))