viewcvs.cgi/typing/typer.ml

(* I. Transform the abstract syntax of types and patterns into
      the internal form *)

open Location
open Ast

exception Pattern of string
exception NonExhaustive of Types.descr
exception MultipleLabel of Types.label
exception Constraint of Types.descr * Types.descr * string
exception ShouldHave of Types.descr * string
exception WrongLabel of Types.descr * Types.label
exception UnboundId of string

let raise_loc loc exn = raise (Location (loc,exn))

(* Internal representation as a graph (desugar recursive types and regexp),
   to compute freevars, etc... *)

type ti = {
  id : int; 
  mutable loc' : loc;
  mutable fv : string SortedList.t option; 
  mutable descr': descr;
  mutable type_node: Types.node option;
  mutable pat_node: Patterns.node option
} 
and descr =
   [ `Alias of string * ti
   | `Type of Types.descr
   | `Or of ti * ti
   | `And of ti * ti * bool
   | `Diff of ti * ti
   | `Times of ti * ti
   | `Arrow of ti * ti
   | `Record of Types.label * bool * ti
   | `Capture of Patterns.capture
   | `Constant of Patterns.capture * Types.const
   ]
    

module S = struct type t = string let compare = compare end
module StringMap = Map.Make(S)
module StringSet = Set.Make(S)

let mk' =
  let counter = ref 0 in
  fun loc ->
    incr counter;
    let rec x = { 
      id = !counter; 
      loc' = loc; 
      fv = None; 
      descr' = `Alias ("__dummy__", x);  
      type_node = None; 
      pat_node = None 
    } in
    x

let cons loc d =
  let x = mk' loc in
  x.descr' <- d;
  x
    
(* Note:
   Compilation of Regexp is implemented as a ``rewriting'' of
   the parsed syntax, in order to be able to print its result
   (for debugging for instance)
   
   It would be possible (and a little more efficient) to produce
   directly ti nodes.
*)
    
module Regexp = struct
  let memo = Hashtbl.create 51
  let defs = ref []
  let name =
    let c = ref 0 in
    fun () ->
      incr c;
      "#" ^ (string_of_int !c)

  let rec seq_vars accu = function
    | Epsilon | Elem _ -> accu
    | Seq (r1,r2) | Alt (r1,r2) -> seq_vars (seq_vars accu r1) r2
    | Star r | WeakStar r -> seq_vars accu r
    | SeqCapture (v,r) -> seq_vars (StringSet.add v accu) r

  let rec propagate vars = function
    | Epsilon -> `Epsilon
    | Elem x -> `Elem (vars,x)
    | Seq (r1,r2) -> `Seq (propagate vars r1,propagate vars r2)
    | Alt (r1,r2) -> `Alt (propagate vars r1, propagate vars r2)
    | Star r -> `Star (propagate vars r)
    | WeakStar r -> `WeakStar (propagate vars r)
    | SeqCapture (v,x) -> propagate (StringSet.add v vars) x

  let cup r1 r2 = 
    match (r1,r2) with
      | (_, `Empty) -> r1
      | (`Empty, _) -> r2
      | (`Res t1, `Res t2) -> `Res (mk noloc (Or (t1,t2)))

  let rec compile fin e seq : [`Res of Ast.ppat | `Empty] = 
    if List.mem seq e then `Empty
    else 
      let e = seq :: e in
      match seq with
        | [] ->
            `Res fin
        | `Epsilon :: rest -> 
            compile fin e rest
        | `Elem (vars,x) :: rest -> 
            let capt = StringSet.fold
                         (fun v t -> mk noloc (And (t, (mk noloc (Capture v)), true)))
                         vars x in
            `Res (mk noloc (Prod (capt, guard_compile fin rest)))
        | `Seq (r1,r2) :: rest -> 
            compile fin e (r1 :: r2 :: rest)
        | `Alt (r1,r2) :: rest -> 
            cup (compile fin e (r1::rest)) (compile fin e (r2::rest))
        | `Star r :: rest -> cup (compile fin e (r::seq)) (compile fin e rest) 
        | `WeakStar r :: rest -> cup (compile fin e rest) (compile fin e (r::seq))

  and guard_compile fin seq =
    try Hashtbl.find memo seq 
    with
        Not_found ->
          let n = name () in
          let v = mk noloc (PatVar n) in
          Hashtbl.add memo seq v;
          let d = compile fin [] seq in
          (match d with
             | `Empty -> assert false
             | `Res d -> defs := (n,d) :: !defs);
          v


  let atom_nil = Types.mk_atom "nil"
  let constant_nil v t = 
    mk noloc (And (t, (mk noloc (Constant (v, Types.Atom atom_nil))), true))

  let compile regexp queue : ppat =
    let vars = seq_vars StringSet.empty regexp in
    let fin = StringSet.fold constant_nil vars queue in
    let n = guard_compile fin [propagate StringSet.empty regexp] in
    Hashtbl.clear memo;
    let d = !defs in
    defs := [];
    mk noloc (Recurs (n,d))
end

let compile_regexp = Regexp.compile


let rec compile env { loc = loc; descr = d } : ti = 
  match (d : Ast.ppat') with
  | PatVar s -> 
      (try StringMap.find s env
       with Not_found -> 
         raise_loc loc (Pattern ("Undefined type variable " ^ s))
      )
  | Recurs (t, b) -> compile (compile_many env b) t
  | Regexp (r,q) -> compile env (Regexp.compile r q)
  | Internal t -> cons loc (`Type t)
  | Or (t1,t2) -> cons loc (`Or (compile env t1, compile env t2))
  | And (t1,t2,e) -> cons loc (`And (compile env t1, compile env t2,e))
  | Diff (t1,t2) -> cons loc (`Diff (compile env t1, compile env t2))
  | Prod (t1,t2) -> cons loc (`Times (compile env t1, compile env t2))
  | Arrow (t1,t2) -> cons loc (`Arrow (compile env t1, compile env t2))
  | Record (l,o,t) -> cons loc (`Record (l,o,compile env t))
  | Constant (x,v) -> cons loc (`Constant (x,v))
  | Capture x -> cons loc (`Capture x)

and compile_many env b = 
  let b = List.map (fun (v,t) -> (v,t,mk' t.loc)) b in
  let env = 
    List.fold_left (fun env (v,t,x) -> StringMap.add v x env) env b in
  List.iter (fun (v,t,x) -> x.descr' <- `Alias (v, compile env t)) b;
  env


let rec comp_fv seen s =
  match s.fv with
    | Some l -> l
    | None ->
        let l = 
          match s.descr' with
            | `Alias (_,x) -> if List.memq s seen then [] else comp_fv (s :: seen) x
            | `Or (s1,s2) 
            | `And (s1,s2,_)
            | `Diff (s1,s2)
            | `Times (s1,s2)
            | `Arrow (s1,s2) -> SortedList.cup (comp_fv seen s1) (comp_fv seen s2)
            | `Record (l,opt,s) -> comp_fv seen s
            | `Type _ -> []
            | `Capture x
            | `Constant (x,_) -> [x]
        in
        if seen = [] then s.fv <- Some l;
        l


let fv = comp_fv []

let rec typ seen s : Types.descr =
  match s.descr' with
    | `Alias (v,x) ->
        if List.memq s seen then 
          raise_loc s.loc' 
            (Pattern 
               ("Unguarded recursion on variable " ^ v ^ " in this type"))
        else typ (s :: seen) x
    | `Type t -> t
    | `Or (s1,s2) -> Types.cup (typ seen s1) (typ seen s2)
    | `And (s1,s2,_) ->  Types.cap (typ seen s1) (typ seen s2)
    | `Diff (s1,s2) -> Types.diff (typ seen s1) (typ seen s2)
    | `Times (s1,s2) -> Types.times (typ_node s1) (typ_node s2)
    | `Arrow (s1,s2) -> Types.arrow (typ_node s1) (typ_node s2)
    | `Record (l,o,s) -> Types.record l o (typ_node s)
    | `Capture _ | `Constant _ -> assert false

and typ_node s : Types.node =
  match s.type_node with
    | Some x -> x
    | None ->
        let x = Types.make () in
        s.type_node <- Some x;
        let t = typ [] s in
        Types.define x t;
        x

let type_node s = Types.internalize (typ_node s)

let rec pat seen s : Patterns.descr =
  if fv s = [] then Patterns.constr (type_node s) else
  match s.descr' with
    | `Alias (v,x) ->
        if List.memq s seen then 
          raise_loc s.loc' 
            (Pattern 
               ("Unguarded recursion on variable " ^ v ^ " in this pattern"))
        else pat (s :: seen) x
    | `Or (s1,s2) -> Patterns.cup (pat seen s1) (pat seen s2)
    | `And (s1,s2,e) -> Patterns.cap (pat seen s1) (pat seen s2) e
    | `Diff (s1,s2) when fv s2 = [] ->
        let s2 = Types.cons (Types.neg (Types.descr (type_node s2)))in
        Patterns.cap (pat seen s1) (Patterns.constr s2) true
    | `Diff _ ->
        raise_loc s.loc' (Pattern "Difference not allowed in patterns")
    | `Times (s1,s2) -> Patterns.times (pat_node s1) (pat_node s2)
    | `Record (l,false,s) -> Patterns.record l (pat_node s)
    | `Record _ ->
        raise_loc s.loc' 
          (Pattern "Optional field not allowed in record patterns")
    | `Capture x ->  Patterns.capture x
    | `Constant (x,c) -> Patterns.constant x c
    | `Arrow _ ->
        raise_loc s.loc' (Pattern "Arrow not allowed in patterns")
    | `Type _ -> assert false

and pat_node s : Patterns.node =
  match s.pat_node with
    | Some x -> x
    | None ->
        let x = Patterns.make (fv s) in
        s.pat_node <- Some x;
        let t = pat [] s in
        Patterns.define x t;
        x

let global_types = ref StringMap.empty

let mk_typ e =
  if fv e = [] then type_node e 
  else raise_loc e.loc' (Pattern "Capture variables are not allowed in types")
    

let typ e =
  mk_typ (compile !global_types e)

let pat e =
  let e = compile !global_types e in
  pat_node e

let register_global_types b =
  let env = compile_many !global_types b in
  List.iter (fun (v,_) -> 
               let d = Types.descr (mk_typ (StringMap.find v env)) in
               let d = Types.normalize d in
               Types.Print.register_global v d
            ) b;
  global_types := env


(* II. Build skeleton *)

module Fv = StringSet

let rec expr { loc = loc; descr = d } = 
  let (fv,td) = 
    match d with
      | DebugTyper t -> (Fv.empty, Typed.DebugTyper (typ t))
      | Forget (e,t) ->
          let (fv,e) = expr e and t = typ t in
          (fv, Typed.Forget (e,t))
      | Var s -> (Fv.singleton s, Typed.Var s)
      | Apply (e1,e2) -> 
          let (fv1,e1) = expr e1 and (fv2,e2) = expr e2 in
          (Fv.union fv1 fv2, Typed.Apply (e1,e2))
      | Abstraction a ->
          let iface = List.map (fun (t1,t2) -> (typ t1, typ 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 (fv0,body) = branches a.fun_body in
          let fv = match a.fun_name with
            | None -> fv0
            | Some f -> Fv.remove f fv0 in
          (fv,
           Typed.Abstraction 
             { Typed.fun_name = a.fun_name;
               Typed.fun_iface = iface;
               Typed.fun_body = body;
               Typed.fun_typ = t;
               Typed.fun_fv = Fv.elements fv0
             }
          )
      | Cst c -> (Fv.empty, Typed.Cst c)
      | Pair (e1,e2) ->
          let (fv1,e1) = expr e1 and (fv2,e2) = expr e2 in
          (Fv.union fv1 fv2, Typed.Pair (e1,e2))
      | Dot (e,l) ->
          let (fv,e) = expr e in
          (fv,  Typed.Dot (e,l))
      | RecordLitt r -> 
          let fv = ref Fv.empty in
          let r  = List.sort (fun (l1,_) (l2,_) -> compare l1 l2) r in
          let r = List.map 
                    (fun (l,e) -> 
                       let (fv2,e) = expr e in fv := Fv.union !fv fv2; (l,e))
                    r in
          let rec check = function
            | (l1,_) :: (l2,_) :: _ when l1 = l2 -> 
                raise_loc loc (MultipleLabel l1)
            | _ :: rem -> check rem
            | _ -> () in
          check r;
          (!fv, Typed.RecordLitt r)
      | Op (op,le) ->
          let (fvs,ltes) = List.split (List.map expr le) in
          let fv = List.fold_left Fv.union Fv.empty fvs in
          (fv, Typed.Op (op,ltes))
      | Match (e,b) -> 
          let (fv1,e) = expr e
          and (fv2,b) = branches b in
          (Fv.union fv1 fv2, Typed.Match (e, b))
      | Map (e,b) ->
          let (fv1,e) = expr e
          and (fv2,b) = branches b in
          (Fv.union fv1 fv2, Typed.Map (e, b))
  in
  fv,
  { Typed.exp_loc = loc;
    Typed.exp_typ = Types.empty;
    Typed.exp_descr = td;
  }
              
  and branches b = 
    let fv = ref Fv.empty in
    let accept = ref Types.empty in
    let b = List.map 
              (fun (p,e) ->
                 let (fv2,e) = expr e in
                 fv := Fv.union !fv fv2;
                 let p = pat p in
                 accept := Types.cup !accept (Types.descr (Patterns.accept p));
                 { Typed.br_used = false;
                   Typed.br_pat = p;
                   Typed.br_body = e }
              ) b in
    (!fv, 
     { 
       Typed.br_typ = Types.empty; 
       Typed.br_branches = b; 
       Typed.br_accept = !accept;
       Typed.br_compiled = None;
     } 
    )

module Env = StringMap

open Typed


let check loc t s msg =
  if not (Types.subtype t s) then raise_loc loc (Constraint (t, s, msg))

let rec type_check env e constr precise = 
(*  Format.fprintf Format.std_formatter "constr=%a precise=%b@\n"
    Types.Print.print_descr constr precise; 
*)
  let d = type_check' e.exp_loc env e.exp_descr constr precise 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);
      t
  | Abstraction a ->
      let t =
        try Types.Arrow.check_strenghten a.fun_typ constr 
        with Not_found -> 
          raise_loc loc 
          (ShouldHave
             (constr, "but the interface of the abstraction is not compatible"))
      in
      let env = match a.fun_name with
        | None -> env
        | Some f -> Env.add f a.fun_typ env in
      List.iter 
        (fun (t1,t2) ->
           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

  | Pair (e1,e2) -> 
      let rects = Types.Product.get constr in
      if Types.Product.is_empty rects then 
        raise_loc loc (ShouldHave (constr,"but it is a pair."));
      let pi1 = Types.Product.pi1 rects in

      let t1 = type_check env e1 (Types.Product.pi1 rects) 
                 (precise || (Types.Product.need_second rects))in
      let rects = Types.Product.restrict_1 rects t1 in
      let t2 = type_check env e2 (Types.Product.pi2 rects) precise in
      if precise then 
        Types.times (Types.cons t1) (Types.cons t2)
      else
        constr

  | RecordLitt r ->
      let rconstr = Types.Record.get constr in
      if Types.Record.is_empty rconstr then
        raise_loc loc (ShouldHave (constr,"but it is a record."));

      let (rconstr,res) = 
        List.fold_left 
          (fun (rconstr,res) (l,e) ->
             let rconstr = Types.Record.restrict_label_present rconstr l in
             let pi = Types.Record.project_field rconstr l in
             if Types.Record.is_empty rconstr then
               raise_loc loc 
                 (ShouldHave (constr,(Printf.sprintf 
                                        "Field %s is not allowed here."
                                        (Types.label_name l)
                                     )
                             ));
             let t = type_check env e pi true in
             let rconstr = Types.Record.restrict_field rconstr l t in
             
             let res = 
               if precise 
               then Types.cap res (Types.record l false (Types.cons t))
               else res in
             (rconstr,res)
          ) (rconstr, if precise then Types.Record.any else constr) r
      in
      res

  | Map (e,b) ->
      let t = type_check env e (Sequence.star b.br_accept) true in

      let constr' = Sequence.approx (Types.cap Sequence.any constr) in
      let exact = Types.subtype (Sequence.star constr') constr in
(*
      Format.fprintf Format.std_formatter 
        "(Map) constr = %a@;  exact = %b\n@." Types.Print.print_descr constr exact;
*)
      (* Note: 
         - could be more precise by integrating the decomposition
         of constr inside Sequence.map.
      *)
      let res = 
        Sequence.map 
          (fun t -> 
             type_check_branches loc env t b constr' (precise || (not exact)))
          t in
      if not exact then check loc res constr "";
      if precise then res else constr
  | Op ("@", [e1;e2]) ->
      let constr' = Sequence.star 
                      (Sequence.approx (Types.cap Sequence.any constr)) in
      let exact = Types.subtype constr' constr in
      if exact then
        let t1 = type_check env e1 constr' precise
        and t2 = type_check env e2 constr' precise in
        if precise then Sequence.concat t1 t2 else constr
      else
        (* Note:
           the knownledge of t1 may makes it useless to
           check t2 with 'precise' ... *)
        let t1 = type_check env e1 constr' true
        and t2 = type_check env e2 constr' true in
        let res = Sequence.concat t1 t2 in
        check loc res constr "";
        if precise then res else constr
  | Op ("flatten", [e]) ->
      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 = type_check env e sconstr' precise in
        if precise then Sequence.flatten t else constr
      else
        let t = type_check env e sconstr' true in
        let res = Sequence.flatten t in
        check loc res constr "";
        if precise then res else constr
  | _ -> 
      let t : Types.descr = compute_type' loc env e in
      check loc t constr "";
      t

and compute_type env e =
  type_check env e Types.any true

and compute_type' loc env = function
  | DebugTyper t -> Types.descr t
  | Var s -> 
      (try Env.find s env 
       with Not_found -> raise_loc loc (UnboundId s)
      )
  | 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
      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)
  | Cst c -> Types.constant c
  | Dot (e,l) ->
      let t = type_check env e Types.Record.any true in
         (try (Types.Record.project t l) 
          with Not_found -> raise_loc loc (WrongLabel(t,l)))
  | Op (op, el) ->
      let args = List.map (fun e -> (e.exp_loc, compute_type env e)) el in
      type_op loc op args
  | Map (e,b) ->
      let t = compute_type env e in
      Sequence.map (fun t -> type_check_branches loc env t b Types.any true) t

(* We keep these cases here to allow comparison and benchmarking ...
   Just comment the corresponding cases in type_check' to
   activate these ones.
*)
  | Pair (e1,e2) -> 
      let t1 = compute_type env e1 
      and t2 = compute_type env e2 in
      Types.times (Types.cons t1) (Types.cons t2)
  | RecordLitt r ->
      List.fold_left 
        (fun accu (l,e) ->
           let t = compute_type env e in
           let t = Types.record l false (Types.cons t) in
           Types.cap accu t
        ) Types.Record.any r


  | _ -> assert false

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
  | [] -> raise_loc loc (NonExhaustive targ)
  | 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 env' = List.fold_left 
                       (fun env (x,t) -> Env.add x (Types.descr t) env) 
                       env res 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_op loc op args =
  match (op,args) with
    | "+", [loc1,t1; loc2,t2] ->
        type_int_binop Intervals.add loc1 t1 loc2 t2
    | "-", [loc1,t1; loc2,t2] ->
        type_int_binop Intervals.sub loc1 t1 loc2 t2
    | ("*" | "/"), [loc1,t1; loc2,t2] ->
        type_int_binop (fun i1 i2 -> Intervals.any) loc1 t1 loc2 t2
    | "@", [loc1,t1; loc2,t2] ->
        check loc1 t1 Sequence.any
          "The first argument of @ must be a sequence";
        Sequence.concat t1 t2
    | "flatten", [loc1,t1] ->
        check loc1 t1 Sequence.seqseq 
          "The argument of flatten must be a sequence of sequences";
        Sequence.flatten t1
    | "load_xml", [loc1,t1] ->
        check loc1 t1 Sequence.string
          "The argument of load_xml must be a string (filename)";
        Types.any
    | _ -> assert false

and type_int_binop f loc1 t1 loc2 t2 =
  if not (Types.Int.is_int t1) then
    raise_loc loc1 
      (Constraint 
         (t1,Types.Int.any,
          "The first argument must be an integer"));
  if not (Types.Int.is_int t2) then
    raise_loc loc2
      (Constraint 
               (t2,Types.Int.any,
                "The second argument must be an integer"));
  Types.Int.put
    (f (Types.Int.get t1) (Types.Int.get t2));
  

1	abate	5	(* I. Transform the abstract syntax of types and patterns into
2			the internal form *)
3
4			open Location
5			open Ast
6
7	abate	9	exception Pattern of string
8			exception NonExhaustive of Types.descr
9	abate	28	exception MultipleLabel of Types.label
10	abate	9	exception Constraint of Types.descr * Types.descr * string
11	abate	19	exception ShouldHave of Types.descr * string
12	abate	26	exception WrongLabel of Types.descr * Types.label
13	abate	36	exception UnboundId of string
14	abate	5
15	abate	9	let raise_loc loc exn = raise (Location (loc,exn))
16
17	abate	5	(* Internal representation as a graph (desugar recursive types and regexp),
18			to compute freevars, etc... *)
19
20	abate	9	type ti = {
21	abate	5	id : int;
22			mutable loc' : loc;
23			mutable fv : string SortedList.t option;
24			mutable descr': descr;
25			mutable type_node: Types.node option;
26			mutable pat_node: Patterns.node option
27			}
28			and descr =
29	abate	9	[ `Alias of string * ti
30	abate	5	\| `Type of Types.descr
31			\| `Or of ti * ti
32	abate	54	\| `And of ti * ti * bool
33	abate	5	\| `Diff of ti * ti
34			\| `Times of ti * ti
35			\| `Arrow of ti * ti
36			\| `Record of Types.label * bool * ti
37			\| `Capture of Patterns.capture
38			\| `Constant of Patterns.capture * Types.const
39			]
40
41
42
43			module S = struct type t = string let compare = compare end
44			module StringMap = Map.Make(S)
45			module StringSet = Set.Make(S)
46
47			let mk' =
48			let counter = ref 0 in
49	abate	13	fun loc ->
50	abate	5	incr counter;
51	abate	9	let rec x = {
52			id = !counter;
53	abate	13	loc' = loc;
54	abate	9	fv = None;
55			descr' = `Alias ("__dummy__", x);
56			type_node = None;
57			pat_node = None
58			} in
59	abate	5	x
60
61			let cons loc d =
62	abate	13	let x = mk' loc in
63	abate	5	x.descr' <- d;
64			x
65
66			(* Note:
67			Compilation of Regexp is implemented as a ``rewriting'' of
68			the parsed syntax, in order to be able to print its result
69			(for debugging for instance)
70
71			It would be possible (and a little more efficient) to produce
72			directly ti nodes.
73			*)
74
75			module Regexp = struct
76			let memo = Hashtbl.create 51
77			let defs = ref []
78			let name =
79			let c = ref 0 in
80			fun () ->
81			incr c;
82			"#" ^ (string_of_int !c)
83
84			let rec seq_vars accu = function
85			\| Epsilon \| Elem _ -> accu
86			\| Seq (r1,r2) \| Alt (r1,r2) -> seq_vars (seq_vars accu r1) r2
87			\| Star r \| WeakStar r -> seq_vars accu r
88			\| SeqCapture (v,r) -> seq_vars (StringSet.add v accu) r
89
90			let rec propagate vars = function
91			\| Epsilon -> `Epsilon
92			\| Elem x -> `Elem (vars,x)
93			\| Seq (r1,r2) -> `Seq (propagate vars r1,propagate vars r2)
94			\| Alt (r1,r2) -> `Alt (propagate vars r1, propagate vars r2)
95			\| Star r -> `Star (propagate vars r)
96			\| WeakStar r -> `WeakStar (propagate vars r)
97			\| SeqCapture (v,x) -> propagate (StringSet.add v vars) x
98
99			let cup r1 r2 =
100			match (r1,r2) with
101			\| (_, `Empty) -> r1
102			\| (`Empty, _) -> r2
103			\| (`Res t1, `Res t2) -> `Res (mk noloc (Or (t1,t2)))
104
105			let rec compile fin e seq : [`Res of Ast.ppat \| `Empty] =
106			if List.mem seq e then `Empty
107			else
108			let e = seq :: e in
109			match seq with
110			\| [] ->
111			`Res fin
112			\| `Epsilon :: rest ->
113			compile fin e rest
114			\| `Elem (vars,x) :: rest ->
115			let capt = StringSet.fold
116	abate	54	(fun v t -> mk noloc (And (t, (mk noloc (Capture v)), true)))
117	abate	5	vars x in
118			`Res (mk noloc (Prod (capt, guard_compile fin rest)))
119			\| `Seq (r1,r2) :: rest ->
120			compile fin e (r1 :: r2 :: rest)
121			\| `Alt (r1,r2) :: rest ->
122			cup (compile fin e (r1::rest)) (compile fin e (r2::rest))
123			\| `Star r :: rest -> cup (compile fin e (r::seq)) (compile fin e rest)
124			\| `WeakStar r :: rest -> cup (compile fin e rest) (compile fin e (r::seq))
125
126			and guard_compile fin seq =
127			try Hashtbl.find memo seq
128			with
129			Not_found ->
130			let n = name () in
131			let v = mk noloc (PatVar n) in
132			Hashtbl.add memo seq v;
133			let d = compile fin [] seq in
134			(match d with
135			\| `Empty -> assert false
136			\| `Res d -> defs := (n,d) :: !defs);
137			v
138
139
140			let atom_nil = Types.mk_atom "nil"
141			let constant_nil v t =
142	abate	54	mk noloc (And (t, (mk noloc (Constant (v, Types.Atom atom_nil))), true))
143	abate	5
144			let compile regexp queue : ppat =
145			let vars = seq_vars StringSet.empty regexp in
146			let fin = StringSet.fold constant_nil vars queue in
147			let n = guard_compile fin [propagate StringSet.empty regexp] in
148			Hashtbl.clear memo;
149			let d = !defs in
150			defs := [];
151			mk noloc (Recurs (n,d))
152			end
153
154			let compile_regexp = Regexp.compile
155
156
157			let rec compile env { loc = loc; descr = d } : ti =
158			match (d : Ast.ppat') with
159			\| PatVar s ->
160			(try StringMap.find s env
161	abate	9	with Not_found ->
162			raise_loc loc (Pattern ("Undefined type variable " ^ s))
163	abate	5	)
164	abate	13	\| Recurs (t, b) -> compile (compile_many env b) t
165	abate	5	\| Regexp (r,q) -> compile env (Regexp.compile r q)
166			\| Internal t -> cons loc (`Type t)
167			\| Or (t1,t2) -> cons loc (`Or (compile env t1, compile env t2))
168	abate	54	\| And (t1,t2,e) -> cons loc (`And (compile env t1, compile env t2,e))
169	abate	5	\| Diff (t1,t2) -> cons loc (`Diff (compile env t1, compile env t2))
170			\| Prod (t1,t2) -> cons loc (`Times (compile env t1, compile env t2))
171			\| Arrow (t1,t2) -> cons loc (`Arrow (compile env t1, compile env t2))
172			\| Record (l,o,t) -> cons loc (`Record (l,o,compile env t))
173			\| Constant (x,v) -> cons loc (`Constant (x,v))
174			\| Capture x -> cons loc (`Capture x)
175
176	abate	13	and compile_many env b =
177			let b = List.map (fun (v,t) -> (v,t,mk' t.loc)) b in
178			let env =
179			List.fold_left (fun env (v,t,x) -> StringMap.add v x env) env b in
180			List.iter (fun (v,t,x) -> x.descr' <- `Alias (v, compile env t)) b;
181			env
182
183
184	abate	5	let rec comp_fv seen s =
185			match s.fv with
186			\| Some l -> l
187			\| None ->
188			let l =
189			match s.descr' with
190	abate	9	\| `Alias (_,x) -> if List.memq s seen then [] else comp_fv (s :: seen) x
191	abate	5	\| `Or (s1,s2)
192	abate	54	\| `And (s1,s2,_)
193	abate	5	\| `Diff (s1,s2)
194			\| `Times (s1,s2)
195			\| `Arrow (s1,s2) -> SortedList.cup (comp_fv seen s1) (comp_fv seen s2)
196			\| `Record (l,opt,s) -> comp_fv seen s
197			\| `Type _ -> []
198			\| `Capture x
199			\| `Constant (x,_) -> [x]
200			in
201			if seen = [] then s.fv <- Some l;
202			l
203
204
205			let fv = comp_fv []
206
207			let rec typ seen s : Types.descr =
208			match s.descr' with
209	abate	9	\| `Alias (v,x) ->
210			if List.memq s seen then
211			raise_loc s.loc'
212			(Pattern
213			("Unguarded recursion on variable " ^ v ^ " in this type"))
214	abate	5	else typ (s :: seen) x
215			\| `Type t -> t
216			\| `Or (s1,s2) -> Types.cup (typ seen s1) (typ seen s2)
217	abate	54	\| `And (s1,s2,_) -> Types.cap (typ seen s1) (typ seen s2)
218	abate	5	\| `Diff (s1,s2) -> Types.diff (typ seen s1) (typ seen s2)
219			\| `Times (s1,s2) -> Types.times (typ_node s1) (typ_node s2)
220			\| `Arrow (s1,s2) -> Types.arrow (typ_node s1) (typ_node s2)
221			\| `Record (l,o,s) -> Types.record l o (typ_node s)
222	abate	9	\| `Capture _ \| `Constant _ -> assert false
223	abate	5
224			and typ_node s : Types.node =
225			match s.type_node with
226			\| Some x -> x
227			\| None ->
228			let x = Types.make () in
229			s.type_node <- Some x;
230			let t = typ [] s in
231			Types.define x t;
232			x
233
234			let type_node s = Types.internalize (typ_node s)
235
236			let rec pat seen s : Patterns.descr =
237			if fv s = [] then Patterns.constr (type_node s) else
238			match s.descr' with
239	abate	9	\| `Alias (v,x) ->
240			if List.memq s seen then
241			raise_loc s.loc'
242			(Pattern
243			("Unguarded recursion on variable " ^ v ^ " in this pattern"))
244	abate	5	else pat (s :: seen) x
245			\| `Or (s1,s2) -> Patterns.cup (pat seen s1) (pat seen s2)
246	abate	54	\| `And (s1,s2,e) -> Patterns.cap (pat seen s1) (pat seen s2) e
247	abate	5	\| `Diff (s1,s2) when fv s2 = [] ->
248			let s2 = Types.cons (Types.neg (Types.descr (type_node s2)))in
249	abate	54	Patterns.cap (pat seen s1) (Patterns.constr s2) true
250	abate	9	\| `Diff _ ->
251			raise_loc s.loc' (Pattern "Difference not allowed in patterns")
252	abate	5	\| `Times (s1,s2) -> Patterns.times (pat_node s1) (pat_node s2)
253			\| `Record (l,false,s) -> Patterns.record l (pat_node s)
254	abate	9	\| `Record _ ->
255			raise_loc s.loc'
256			(Pattern "Optional field not allowed in record patterns")
257	abate	5	\| `Capture x -> Patterns.capture x
258			\| `Constant (x,c) -> Patterns.constant x c
259	abate	9	\| `Arrow _ ->
260			raise_loc s.loc' (Pattern "Arrow not allowed in patterns")
261			\| `Type _ -> assert false
262	abate	5
263			and pat_node s : Patterns.node =
264			match s.pat_node with
265			\| Some x -> x
266			\| None ->
267			let x = Patterns.make (fv s) in
268			s.pat_node <- Some x;
269			let t = pat [] s in
270			Patterns.define x t;
271			x
272
273	abate	13	let global_types = ref StringMap.empty
274
275			let mk_typ e =
276	abate	9	if fv e = [] then type_node e
277	abate	13	else raise_loc e.loc' (Pattern "Capture variables are not allowed in types")
278
279	abate	5
280	abate	13	let typ e =
281			mk_typ (compile !global_types e)
282
283	abate	5	let pat e =
284	abate	13	let e = compile !global_types e in
285	abate	5	pat_node e
286
287	abate	13	let register_global_types b =
288			let env = compile_many !global_types b in
289	abate	15	List.iter (fun (v,_) ->
290			let d = Types.descr (mk_typ (StringMap.find v env)) in
291	abate	36	let d = Types.normalize d in
292	abate	15	Types.Print.register_global v d
293			) b;
294	abate	13	global_types := env
295	abate	5
296
297			(* II. Build skeleton *)
298
299	abate	6	module Fv = StringSet
300
301	abate	5	let rec expr { loc = loc; descr = d } =
302	abate	6	let (fv,td) =
303	abate	5	match d with
304	abate	18	\| DebugTyper t -> (Fv.empty, Typed.DebugTyper (typ t))
305	abate	54	\| Forget (e,t) ->
306			let (fv,e) = expr e and t = typ t in
307			(fv, Typed.Forget (e,t))
308	abate	6	\| Var s -> (Fv.singleton s, Typed.Var s)
309			\| Apply (e1,e2) ->
310			let (fv1,e1) = expr e1 and (fv2,e2) = expr e2 in
311			(Fv.union fv1 fv2, Typed.Apply (e1,e2))
312	abate	5	\| Abstraction a ->
313	abate	6	let iface = List.map (fun (t1,t2) -> (typ t1, typ t2)) a.fun_iface in
314			let t = List.fold_left
315			(fun accu (t1,t2) -> Types.cap accu (Types.arrow t1 t2))
316			Types.any iface in
317	abate	9	let iface = List.map
318			(fun (t1,t2) -> (Types.descr t1, Types.descr t2))
319			iface in
320	abate	6	let (fv0,body) = branches a.fun_body in
321			let fv = match a.fun_name with
322			\| None -> fv0
323			\| Some f -> Fv.remove f fv0 in
324			(fv,
325			Typed.Abstraction
326			{ Typed.fun_name = a.fun_name;
327			Typed.fun_iface = iface;
328			Typed.fun_body = body;
329			Typed.fun_typ = t;
330			Typed.fun_fv = Fv.elements fv0
331			}
332			)
333			\| Cst c -> (Fv.empty, Typed.Cst c)
334			\| Pair (e1,e2) ->
335			let (fv1,e1) = expr e1 and (fv2,e2) = expr e2 in
336			(Fv.union fv1 fv2, Typed.Pair (e1,e2))
337	abate	26	\| Dot (e,l) ->
338			let (fv,e) = expr e in
339	abate	27	(fv, Typed.Dot (e,l))
340	abate	6	\| RecordLitt r ->
341			let fv = ref Fv.empty in
342	abate	47	let r = List.sort (fun (l1,_) (l2,_) -> compare l1 l2) r in
343	abate	6	let r = List.map
344			(fun (l,e) ->
345	abate	47	let (fv2,e) = expr e in fv := Fv.union !fv fv2; (l,e))
346			r in
347			let rec check = function
348			\| (l1,_) :: (l2,_) :: _ when l1 = l2 ->
349			raise_loc loc (MultipleLabel l1)
350			\| _ :: rem -> check rem
351			\| _ -> () in
352			check r;
353	abate	6	(!fv, Typed.RecordLitt r)
354	abate	16	\| Op (op,le) ->
355			let (fvs,ltes) = List.split (List.map expr le) in
356			let fv = List.fold_left Fv.union Fv.empty fvs in
357			(fv, Typed.Op (op,ltes))
358	abate	6	\| Match (e,b) ->
359			let (fv1,e) = expr e
360			and (fv2,b) = branches b in
361			(Fv.union fv1 fv2, Typed.Match (e, b))
362			\| Map (e,b) ->
363			let (fv1,e) = expr e
364			and (fv2,b) = branches b in
365			(Fv.union fv1 fv2, Typed.Map (e, b))
366	abate	5	in
367	abate	6	fv,
368			{ Typed.exp_loc = loc;
369	abate	5	Typed.exp_typ = Types.empty;
370			Typed.exp_descr = td;
371			}
372
373	abate	6	and branches b =
374			let fv = ref Fv.empty in
375	abate	19	let accept = ref Types.empty in
376	abate	6	let b = List.map
377			(fun (p,e) ->
378			let (fv2,e) = expr e in
379			fv := Fv.union !fv fv2;
380	abate	19	let p = pat p in
381			accept := Types.cup !accept (Types.descr (Patterns.accept p));
382	abate	6	{ Typed.br_used = false;
383	abate	19	Typed.br_pat = p;
384	abate	6	Typed.br_body = e }
385			) b in
386	abate	19	(!fv,
387			{
388			Typed.br_typ = Types.empty;
389			Typed.br_branches = b;
390	abate	45	Typed.br_accept = !accept;
391			Typed.br_compiled = None;
392	abate	19	}
393			)
394	abate	5
395	abate	6	module Env = StringMap
396
397			open Typed
398
399	abate	17
400			let check loc t s msg =
401			if not (Types.subtype t s) then raise_loc loc (Constraint (t, s, msg))
402
403	abate	19	let rec type_check env e constr precise =
404	abate	31	(* Format.fprintf Format.std_formatter "constr=%a precise=%b@\n"
405	abate	37	Types.Print.print_descr constr precise;
406			*)
407	abate	19	let d = type_check' e.exp_loc env e.exp_descr constr precise in
408	abate	6	e.exp_typ <- Types.cup e.exp_typ d;
409			d
410
411	abate	19	and type_check' loc env e constr precise = match e with
412	abate	54	\| Forget (e,t) ->
413			let t = Types.descr t in
414			ignore (type_check env e t false);
415			t
416	abate	19	\| Abstraction a ->
417			let t =
418			try Types.Arrow.check_strenghten a.fun_typ constr
419			with Not_found ->
420			raise_loc loc
421			(ShouldHave
422			(constr, "but the interface of the abstraction is not compatible"))
423			in
424			let env = match a.fun_name with
425			\| None -> env
426			\| Some f -> Env.add f a.fun_typ env in
427			List.iter
428			(fun (t1,t2) ->
429			ignore (type_check_branches loc env t1 a.fun_body t2 false)
430			) a.fun_iface;
431			t
432			\| Match (e,b) ->
433			let t = type_check env e b.br_accept true in
434			type_check_branches loc env t b constr precise
435	abate	30
436	abate	19	\| Pair (e1,e2) ->
437			let rects = Types.Product.get constr in
438			if Types.Product.is_empty rects then
439			raise_loc loc (ShouldHave (constr,"but it is a pair."));
440			let pi1 = Types.Product.pi1 rects in
441
442			let t1 = type_check env e1 (Types.Product.pi1 rects)
443			(precise \|\| (Types.Product.need_second rects))in
444			let rects = Types.Product.restrict_1 rects t1 in
445			let t2 = type_check env e2 (Types.Product.pi2 rects) precise in
446			if precise then
447			Types.times (Types.cons t1) (Types.cons t2)
448			else
449			constr
450	abate	30
451	abate	29	\| RecordLitt r ->
452			let rconstr = Types.Record.get constr in
453			if Types.Record.is_empty rconstr then
454			raise_loc loc (ShouldHave (constr,"but it is a record."));
455
456			let (rconstr,res) =
457			List.fold_left
458			(fun (rconstr,res) (l,e) ->
459			let rconstr = Types.Record.restrict_label_present rconstr l in
460			let pi = Types.Record.project_field rconstr l in
461			if Types.Record.is_empty rconstr then
462			raise_loc loc
463			(ShouldHave (constr,(Printf.sprintf
464			"Field %s is not allowed here."
465			(Types.label_name l)
466			)
467			));
468			let t = type_check env e pi true in
469			let rconstr = Types.Record.restrict_field rconstr l t in
470
471			let res =
472			if precise
473			then Types.cap res (Types.record l false (Types.cons t))
474			else res in
475			(rconstr,res)
476			) (rconstr, if precise then Types.Record.any else constr) r
477			in
478			res
479
480	abate	31	\| Map (e,b) ->
481			let t = type_check env e (Sequence.star b.br_accept) true in
482
483			let constr' = Sequence.approx (Types.cap Sequence.any constr) in
484			let exact = Types.subtype (Sequence.star constr') constr in
485	abate	54	(*
486			Format.fprintf Format.std_formatter
487			"(Map) constr = %a@; exact = %b\n@." Types.Print.print_descr constr exact;
488			*)
489			(* Note:
490			- could be more precise by integrating the decomposition
491			of constr inside Sequence.map.
492			*)
493			let res =
494			Sequence.map
495			(fun t ->
496			type_check_branches loc env t b constr' (precise \|\| (not exact)))
497			t in
498			if not exact then check loc res constr "";
499			if precise then res else constr
500	abate	31	\| Op ("@", [e1;e2]) ->
501			let constr' = Sequence.star
502			(Sequence.approx (Types.cap Sequence.any constr)) in
503			let exact = Types.subtype constr' constr in
504			if exact then
505			let t1 = type_check env e1 constr' precise
506			and t2 = type_check env e2 constr' precise in
507			if precise then Sequence.concat t1 t2 else constr
508			else
509			(* Note:
510			the knownledge of t1 may makes it useless to
511			check t2 with 'precise' ... *)
512			let t1 = type_check env e1 constr' true
513			and t2 = type_check env e2 constr' true in
514			let res = Sequence.concat t1 t2 in
515			check loc res constr "";
516			if precise then res else constr
517	abate	32	\| Op ("flatten", [e]) ->
518			let constr' = Sequence.star
519			(Sequence.approx (Types.cap Sequence.any constr)) in
520			let sconstr' = Sequence.star constr' in
521			let exact = Types.subtype constr' constr in
522			if exact then
523			let t = type_check env e sconstr' precise in
524			if precise then Sequence.flatten t else constr
525			else
526			let t = type_check env e sconstr' true in
527			let res = Sequence.flatten t in
528			check loc res constr "";
529			if precise then res else constr
530	abate	19	\| _ ->
531			let t : Types.descr = compute_type' loc env e in
532			check loc t constr "";
533			t
534
535			and compute_type env e =
536			type_check env e Types.any true
537
538	abate	6	and compute_type' loc env = function
539	abate	18	\| DebugTyper t -> Types.descr t
540	abate	36	\| Var s ->
541			(try Env.find s env
542			with Not_found -> raise_loc loc (UnboundId s)
543			)
544	abate	6	\| Apply (e1,e2) ->
545	abate	19	let t1 = type_check env e1 Types.Arrow.any true in
546			let t1 = Types.Arrow.get t1 in
547			let dom = Types.Arrow.domain t1 in
548			if Types.Arrow.need_arg t1 then
549			let t2 = type_check env e2 dom true in
550			Types.Arrow.apply t1 t2
551			else
552			(ignore (type_check env e2 dom false); Types.Arrow.apply_noarg t1)
553	abate	6	\| Cst c -> Types.constant c
554	abate	26	\| Dot (e,l) ->
555			let t = type_check env e Types.Record.any true in
556			(try (Types.Record.project t l)
557			with Not_found -> raise_loc loc (WrongLabel(t,l)))
558	abate	16	\| Op (op, el) ->
559			let args = List.map (fun e -> (e.exp_loc, compute_type env e)) el in
560			type_op loc op args
561	abate	17	\| Map (e,b) ->
562			let t = compute_type env e in
563	abate	19	Sequence.map (fun t -> type_check_branches loc env t b Types.any true) t
564	abate	30
565			(* We keep these cases here to allow comparison and benchmarking ...
566			Just comment the corresponding cases in type_check' to
567			activate these ones.
568			*)
569			\| Pair (e1,e2) ->
570			let t1 = compute_type env e1
571			and t2 = compute_type env e2 in
572			Types.times (Types.cons t1) (Types.cons t2)
573			\| RecordLitt r ->
574			List.fold_left
575			(fun accu (l,e) ->
576			let t = compute_type env e in
577			let t = Types.record l false (Types.cons t) in
578			Types.cap accu t
579			) Types.Record.any r
580
581
582	abate	19	\| _ -> assert false
583	abate	6
584	abate	19	and type_check_branches loc env targ brs constr precise =
585	abate	6	if Types.is_empty targ then Types.empty
586	abate	9	else (
587			brs.br_typ <- Types.cup brs.br_typ targ;
588	abate	19	branches_aux loc env targ
589			(if precise then Types.empty else constr)
590			constr precise brs.br_branches
591	abate	9	)
592	abate	6
593	abate	19	and branches_aux loc env targ tres constr precise = function
594	abate	9	\| [] -> raise_loc loc (NonExhaustive targ)
595	abate	6	\| b :: rem ->
596			let p = b.br_pat in
597			let acc = Types.descr (Patterns.accept p) in
598
599			let targ' = Types.cap targ acc in
600			if Types.is_empty targ'
601	abate	19	then branches_aux loc env targ tres constr precise rem
602	abate	6	else
603			( b.br_used <- true;
604			let res = Patterns.filter targ' p in
605			let env' = List.fold_left
606			(fun env (x,t) -> Env.add x (Types.descr t) env)
607			env res in
608	abate	19	let t = type_check env' b.br_body constr precise in
609			let tres = if precise then Types.cup t tres else tres in
610	abate	9	let targ'' = Types.diff targ acc in
611			if (Types.non_empty targ'') then
612	abate	19	branches_aux loc env targ'' tres constr precise rem
613	abate	9	else
614			tres
615	abate	6	)
616	abate	16
617			and type_op loc op args =
618			match (op,args) with
619	abate	51	\| "+", [loc1,t1; loc2,t2] ->
620	abate	16	type_int_binop Intervals.add loc1 t1 loc2 t2
621	abate	51	\| "-", [loc1,t1; loc2,t2] ->
622			type_int_binop Intervals.sub loc1 t1 loc2 t2
623			\| ("*" \| "/"), [loc1,t1; loc2,t2] ->
624	abate	16	type_int_binop (fun i1 i2 -> Intervals.any) loc1 t1 loc2 t2
625	abate	51	\| "@", [loc1,t1; loc2,t2] ->
626	abate	17	check loc1 t1 Sequence.any
627			"The first argument of @ must be a sequence";
628			Sequence.concat t1 t2
629	abate	51	\| "flatten", [loc1,t1] ->
630	abate	17	check loc1 t1 Sequence.seqseq
631			"The argument of flatten must be a sequence of sequences";
632			Sequence.flatten t1
633	abate	58	\| "load_xml", [loc1,t1] ->
634			check loc1 t1 Sequence.string
635			"The argument of load_xml must be a string (filename)";
636			Types.any
637	abate	16	\| _ -> assert false
638
639			and type_int_binop f loc1 t1 loc2 t2 =
640			if not (Types.Int.is_int t1) then
641			raise_loc loc1
642			(Constraint
643			(t1,Types.Int.any,
644			"The first argument must be an integer"));
645			if not (Types.Int.is_int t2) then
646			raise_loc loc2
647			(Constraint
648	abate	37	(t2,Types.Int.any,
649	abate	16	"The second argument must be an integer"));
650			Types.Int.put
651			(f (Types.Int.get t1) (Types.Int.get t2));
652
653