Tallying.apply algorithm

- performance improvements (add memoization)
- fix infinite loops due to recursive structures
- add apply tests (kim)

tests/libtest/gen_apps.sh

@@ -2,7 +2,8 @@
 
 function print_line
 {
-    echo "Types.apply (parse_typ \"$1\") (parse_typ \"$2\")"
+    echo "Printf.printf \"$1  $2\\n\";;"
+    echo "Types.apply (parse_typ \"$1\") (parse_typ \"$2\");;"
 }
 
 function cduce_type

tests/libtest/tallyingTest.ml

 open OUnit
 open Types
 
-let parse_typ s =
+let parse_typ ?(variance=`Covariant) s =
   let st = Stream.of_string s in
   let astpat = Parser.pat st in 
-  let nodepat = Typer.typ Builtin.env astpat in
+  let nodepat = Typer.typ ~variance Builtin.env astpat in
   Types.descr nodepat
 ;;
 
@@ -21,7 +21,7 @@ module ESet = OUnitDiff.SetMake (struct
     if (v1,t1) == (v2,t2) then 0
     else let c = Var.compare v1 v2 in if c <> 0 then c
     else Types.compare (diff t1 a) (diff t2 a)
-  let pp_printer ppf (v,t) = Format.fprintf ppf "(%a = %s)" Var.print v (to_string Print.print t)
+  let pp_printer ppf (v,t) = Format.fprintf ppf "(%a = %s)" Var.dump v (to_string Print.print t)
   let pp_print_sep = OUnitDiff.pp_comma_separator
 end)
 

types/types.mli

@@ -142,7 +142,9 @@ val rec_of_list: bool -> (bool * Ns.Label.t * t) list -> t
 val empty_closed_record: t
 val empty_open_record: t
 
+(*
 val subst : t -> Var.var * t -> t
+*)
 
 (** Positive systems and least solutions **)
 
@@ -157,8 +159,10 @@ sig
   val xml: v -> v -> v
 
   val decompose : t -> v
-  val substitute : t -> Var.var -> t
+  val substitute : t -> (Var.var * t) -> t
+  val substituterec : t -> Var.var -> t
   val solve: v -> Node.t
+  val substitutefree : t -> t
 end
 
 (** Normalization **)
@@ -404,5 +408,4 @@ module Tallying : sig
 
 end
 
-  val appl : t -> t -> (Var.var * t) list list
-
+val apply : t -> t -> (Var.var * t) list list

types/var.ml

@@ -37,6 +37,7 @@ let ch_variance variance (`Var t) =
   |_,_ -> `Var { t with variance = `Both }
 
 let variance (`Var t) = t.variance
+let is_fresh (`Var t) = t.fresh
 
 module Set = Set.Make(
   struct 
@@ -65,6 +66,7 @@ end
 let mk ?fresh ?variance id = 
   `Var (make_id ?fresh ?variance id)
 
+
 let fresh : ?variance:[ `None| `Both | `ContraVariant | `Covariant ] -> unit -> [> var ] =
   let counter = ref 0 in
   fun ?variance -> fun _ ->

typing/typer.ml

@@ -310,7 +310,13 @@ module IType = struct
     all_delayed := []; 
     List.iter check_one_delayed l
 
-  let rec derecurs ?(variance=`Covariant) env p = match p.descr with
+  let rec derecurs variance env p = 
+    let neg = function
+      |`Covariant -> `ContraVariant
+      |`ContraVariant -> `Covariant
+      |cv -> cv
+    in
+    match p.descr with
     | TVar s -> begin
         try
           let v = Hashtbl.find env.penv_var s in
@@ -322,38 +328,38 @@ module IType = struct
         end
     end
     | PatVar ids -> derecurs_var env p.loc ids
-    | Recurs (p,b) -> derecurs (fst (derecurs_def env b)) p
+    | Recurs (p,b) -> derecurs variance (fst (derecurs_def variance env b)) p
     | Internal t -> mk_type t
     | NsT ns -> 
 	mk_type (Types.atom (Atoms.any_in_ns (parse_ns env.penv_tenv p.loc ns)))
-    | Or (p1,p2) -> mk_or (derecurs env p1) (derecurs env p2)
-    | And (p1,p2) -> mk_and (derecurs env p1) (derecurs env p2)
-    | Diff (p1,p2) -> mk_diff (derecurs env p1) (derecurs env p2)
-    | Prod (p1,p2) -> mk_prod (derecurs env p1) (derecurs env p2)
-    | XmlT (p1,p2) -> mk_xml (derecurs env p1) (derecurs env p2)
-    | Arrow (p1,p2) -> mk_arrow (derecurs env p1) (derecurs ~variance:`ContraVariant env p2)
-    | Optional p -> mk_optional (derecurs env p)
+    | Or (p1,p2) -> mk_or (derecurs variance env p1) (derecurs variance env p2)
+    | And (p1,p2) -> mk_and (derecurs variance env p1) (derecurs variance env p2)
+    | Diff (p1,p2) -> mk_diff (derecurs variance env p1) (derecurs (neg variance) env p2)
+    | Prod (p1,p2) -> mk_prod (derecurs variance env p1) (derecurs variance env p2)
+    | XmlT (p1,p2) -> mk_xml (derecurs variance env p1) (derecurs variance env p2)
+    | Arrow (p1,p2) -> mk_arrow (derecurs (neg variance) env p1) (derecurs variance env p2)
+    | Optional p -> mk_optional (derecurs variance 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
+	  | (p,Some e) -> (derecurs variance env p, Some (derecurs variance env e))
+	  | (p,None) -> derecurs variance env p, None in
 	mk_record o (parse_record env.penv_tenv p.loc aux r)
     | Constant (x,c) -> 
 	mk_constant (ident env.penv_tenv p.loc x) (const env.penv_tenv p.loc c)
     | Cst c -> mk_type (Types.constant (const env.penv_tenv p.loc c))
-    | Regexp r -> rexp (derecurs_regexp env r)
-    | Concat (p1,p2) ->  mk_concat (derecurs env p1) (derecurs env p2)
-    | Merge (p1,p2) -> mk_merge (derecurs env p1) (derecurs env p2)
+    | Regexp r -> rexp (derecurs_regexp variance env r)
+    | Concat (p1,p2) ->  mk_concat (derecurs variance env p1) (derecurs variance env p2)
+    | Merge (p1,p2) -> mk_merge (derecurs variance env p1) (derecurs variance env p2)
 	  
-  and derecurs_regexp env = function
+  and derecurs_regexp variance env = function
     | Epsilon -> mk_epsilon
-    | Elem p -> mk_elem (derecurs env p)
-    | Guard p -> mk_guard (derecurs env p)
-    | Seq (p1,p2) -> mk_seq (derecurs_regexp env p1) (derecurs_regexp env p2)
-    | Alt (p1,p2) -> mk_alt (derecurs_regexp env p1) (derecurs_regexp env p2)
-    | Star p -> mk_star (derecurs_regexp env p)
-    | WeakStar p -> mk_weakstar (derecurs_regexp env p)
-    | SeqCapture (loc,x,p) -> mk_seqcapt (ident env.penv_tenv loc x) (derecurs_regexp env p)
+    | Elem p -> mk_elem (derecurs variance env p)
+    | Guard p -> mk_guard (derecurs variance env p)
+    | Seq (p1,p2) -> mk_seq (derecurs_regexp variance env p1) (derecurs_regexp variance env p2)
+    | Alt (p1,p2) -> mk_alt (derecurs_regexp variance env p1) (derecurs_regexp variance env p2)
+    | Star p -> mk_star (derecurs_regexp variance env p)
+    | WeakStar p -> mk_weakstar (derecurs_regexp variance env p)
+    | SeqCapture (loc,x,p) -> mk_seqcapt (ident env.penv_tenv loc x) (derecurs_regexp variance env p)
 	  
   and derecurs_var env loc ids =
     match ids with
@@ -366,7 +372,7 @@ module IType = struct
       | ids ->
 	  mk_type (find_global_type env.penv_tenv loc ids)
 	      
-  and derecurs_def env b =
+  and derecurs_def variance env b =
     let seen = ref IdSet.empty in
     let b = 
       List.map 
@@ -382,17 +388,16 @@ module IType = struct
 
     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) -> link s (derecurs env p)) b;
+    List.iter (fun (v,p,s) -> link s (derecurs variance env p)) b;
     (env, b)
 
-  let derec penv p =
-    let d = derecurs penv p in
+  let derec ?(variance=`Covariant) penv p =
+    let d = derecurs variance penv p in
     elim_concats ();
     check_delayed ();
-    internalize d;
+    (* internalize d; *)
     d
 
-
 (* API *)
 
   let check_no_fv loc n =
@@ -403,7 +408,7 @@ module IType = struct
 	    ("Capture variable not allowed: " ^ (Ident.to_string x))
 
   let type_defs env b =
-    let _,b' = derecurs_def (penv env) b in
+    let _,b' = derecurs_def `Covariant (penv env) b in
     elim_concats ();
     check_delayed ();
     let aux loc d =
@@ -427,9 +432,9 @@ module IType = struct
     try type_defs env b
     with exn -> clean_on_err (); raise exn
 
-  let typ env t = 
+  let typ ?(variance=`Covariant) env t = 
     try
-      let d = derec (penv env) t in
+      let d = derec ~variance (penv env) t in
       check_no_fv t.loc d;
       try typ_node d
       with Patterns.Error s -> raise_loc_generic t.loc s

typing/typer.mli

@@ -22,7 +22,7 @@ val find_value: id -> t -> Types.t
 val enter_type: id -> Types.t -> t -> t
 val iter_values: t -> (id -> Types.t -> unit) -> unit
 
-val typ: t -> Ast.ppat -> Types.Node.t
+val typ: ?variance:[ `Covariant|`ContraVariant|`Both|`None] -> t -> Ast.ppat -> Types.Node.t
 val pat: t -> Ast.ppat -> Patterns.node
 
 val dump_types: Format.formatter -> t -> unit