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

Makefile

@@ -8,7 +8,7 @@ pull: tools/pull.$(EXTENSION)
 
 PREPRO = camlp4o -I `ocamlfind query ulex` pa_ulex.cma pr_o.cmo $(SYNTAX) -sep "\n"
 
-profile: misc/q_symbol.cmo
+profile: misc/q_symbol.cmo.stamp
 	rm -Rf prepro
 	mkdir prepro
 	for i in $(DIRS); do \

Makefile.distrib

@@ -42,9 +42,9 @@ CAMLC_P = ocamlc -g
 DEPEND_OCAMLDEP = misc/q_symbol.cmo
 ifeq ($(PROFILE), true)
   CAMLOPT_P = ocamlopt -p -inline 10000
-  ifeq ($(NATIVE), false) 
+  ifeq ($(NATIVE), false)
     CAMLC_P = ocamlcp -p a
-    SYNTAX_PARSER = 
+    SYNTAX_PARSER =
     DEPEND_OCAMLDEP =
   endif
 else
@@ -136,7 +136,7 @@ help:
 	@echo "  clean :  back to the starting point"
 	@echo "  uninstall : remove installed files"
 
-# Source directories 
+# Source directories
 
 DIRS = misc parser schema typing types compile runtime driver query ocamliface win32
 CLEAN_DIRS = $(DIRS) tools tests
@@ -229,7 +229,7 @@ endif
 all: $(ALL_TARGET)
 
 OBJECTS += driver/run.cmo
-CDUCE = $(OBJECTS) driver/start.cmo 
+CDUCE = $(OBJECTS) driver/start.cmo
 
 ALL_OBJECTS = $(OBJECTS) \
  driver/start.cmo driver/examples.cmo \
@@ -279,6 +279,7 @@ clean:
 	for i in $(CLEAN_DIRS); do \
 	(cd $$i; rm -f *.cmi *.cmo *.cma *.cmx *.o *.a *.cmxa *~); \
 	done
+	rm -f misc/q_symbol.cmo.stamp
 	(cd ocamliface; $(MAKE) clean)
 	rm -f `find . -name "*~"`
 	rm -f *.cmi *.cmo *.cma *.cmx *.a *.cmxa *.o *~ META
@@ -301,35 +302,31 @@ distclean: clean
 
 ocamliface/mltypes.$(EXTENSION): ocamliface/caml_cduce.$(EXTENSION)
 
-$(ALL_OBJECTS:.cmo=.$(EXTENSION)): misc/q_symbol.cmo
 $(ALL_INTERFACES): misc/q_symbol.cmo
-
-.SUFFIXES: .ml .mli .cmo .cmi .cmx
+$(ALL_OBJECTS:.cmo=.cmi): misc/q_symbol.cmo
+$(ALL_OBJECTS:.cmo=.cmx) caml_cduce.cmx: misc/q_symbol.cmo
+$(ALL_OBJECTS) caml_cduce.cmo: misc/q_symbol.cmo
+$(OCAMLIFACE)/mlstub.$(EXTENSION): SYNTAX += q_MLast.cmo
 
 misc/q_symbol.cmo: misc/q_symbol.ml
-	@echo "Build $@"		  
-	$(HIDE)$(CAMLC) -c -pp camlp4orf $<
-
-types/%.cmo: types/%.ml
 	@echo "Build $@"
-	$(HIDE)$(CAMLC) -c $(INCLUDES) $<
+	$(HIDE) $(CAMLC) -c -pp camlp4orf $<
+
+.SUFFIXES: .ml .mli .cmo .cmi .cmx
+
+types/boolVar.cmo: SYNTAX_PARSER=
+types/boolVar.cmi: SYNTAX_PARSER=
+types/boolVar.cmx: SYNTAX_PARSER=
 
 .ml.cmo:
 	@echo "Build $@"
 	$(HIDE)$(CAMLC) -c $(INCLUDES) $(SYNTAX_PARSER) $<
 
-types/%.cmx: types/%.ml
-	@echo "Build $@"
-	$(HIDE)$(CAMLOPT) $(FORPACKOPT) -c $(INCLUDES) $<
 
 .ml.cmx:
 	@echo "Build $@"
 	$(HIDE)$(CAMLOPT) $(FORPACKOPT) -c $(SYNTAX_PARSER) $(INCLUDES) $<
 
-types/%.cmi: types/%.mli
-	@echo "Build $@"
-	$(HIDE)$(CAMLC) -c $(INCLUDES) $<
-
 .mli.cmi:
 	@echo "Build $@"
 	$(HIDE)$(CAMLC) -c $(SYNTAX_PARSER) $(INCLUDES) $<
@@ -370,4 +367,3 @@ ocamliface/caml_cduce.cmo:
 ocamliface/caml_cduce.cmx:
 	@cd ocamliface; \
 	$(MAKE) caml_cduce.cmx
-

depend

@@ -24,8 +24,10 @@ types/sortedList.cmo : misc/custom.cmo types/sortedList.cmi
 types/sortedList.cmx : misc/custom.cmx types/sortedList.cmi
 misc/bool.cmo : misc/custom.cmo misc/bool.cmi
 misc/bool.cmx : misc/custom.cmx misc/bool.cmi
-types/ident.cmo : types/sortedList.cmi misc/ns.cmi misc/encodings.cmi
-types/ident.cmx : types/sortedList.cmx misc/ns.cmx misc/encodings.cmx
+types/ident.cmo : misc/utils.cmo types/sortedList.cmi misc/ns.cmi \
+    misc/encodings.cmi
+types/ident.cmx : misc/utils.cmx types/sortedList.cmx misc/ns.cmx \
+    misc/encodings.cmx
 types/intervals.cmo : types/intervals.cmi
 types/intervals.cmx : types/intervals.cmi
 types/chars.cmo : misc/custom.cmo types/chars.cmi
@@ -36,8 +38,10 @@ types/atoms.cmx : misc/upool.cmx types/sortedList.cmx misc/ns.cmx \
     misc/imap.cmx misc/encodings.cmx types/atoms.cmi
 types/normal.cmo : types/normal.cmi
 types/normal.cmx : types/normal.cmi
-types/var.cmo : misc/custom.cmo types/var.cmi
-types/var.cmx : misc/custom.cmx types/var.cmi
+types/var.cmo : misc/utils.cmo types/sortedList.cmi types/ident.cmo \
+    misc/custom.cmo types/var.cmi
+types/var.cmx : misc/utils.cmx types/sortedList.cmx types/ident.cmx \
+    misc/custom.cmx types/var.cmi
 types/boolVar.cmo : types/var.cmi misc/custom.cmo types/boolVar.cmi
 types/boolVar.cmx : types/var.cmx misc/custom.cmx types/boolVar.cmi
 types/types.cmo : types/var.cmi misc/utils.cmo misc/stats.cmi \
@@ -106,12 +110,14 @@ schema/schema_validator.cmx : runtime/value.cmx schema/schema_types.cmx \
     schema/schema_pcre.cmx schema/schema_common.cmx schema/schema_builtin.cmx \
     misc/ns.cmx misc/encodings.cmx types/atoms.cmx \
     schema/schema_validator.cmi
-types/patterns.cmo : misc/upool.cmi types/types.cmi types/sortedList.cmi \
-    types/sequence.cmi types/ident.cmo misc/encodings.cmi misc/custom.cmo \
-    types/chars.cmi compile/auto_pat.cmi types/atoms.cmi types/patterns.cmi
-types/patterns.cmx : misc/upool.cmx types/types.cmx types/sortedList.cmx \
-    types/sequence.cmx types/ident.cmx misc/encodings.cmx misc/custom.cmx \
-    types/chars.cmx compile/auto_pat.cmx types/atoms.cmx types/patterns.cmi
+types/patterns.cmo : misc/utils.cmo misc/upool.cmi types/types.cmi \
+    types/sortedList.cmi types/sequence.cmi types/ident.cmo \
+    misc/encodings.cmi misc/custom.cmo types/chars.cmi compile/auto_pat.cmi \
+    types/atoms.cmi types/patterns.cmi
+types/patterns.cmx : misc/utils.cmx misc/upool.cmx types/types.cmx \
+    types/sortedList.cmx types/sequence.cmx types/ident.cmx \
+    misc/encodings.cmx misc/custom.cmx types/chars.cmx compile/auto_pat.cmx \
+    types/atoms.cmx types/patterns.cmi
 compile/print_auto.cmo : types/types.cmi types/ident.cmo \
     compile/auto_pat.cmi compile/print_auto.cmi
 compile/print_auto.cmx : types/types.cmx types/ident.cmx \
@@ -156,14 +162,14 @@ parser/ast.cmo : types/types.cmi types/sequence.cmi misc/ns.cmi \
 parser/ast.cmx : types/types.cmx types/sequence.cmx misc/ns.cmx \
     types/intervals.cmx types/ident.cmx types/chars.cmx parser/cduce_loc.cmx \
     types/builtin_defs.cmx
-parser/parser.cmo : parser/ulexer.cmi types/types.cmi types/sequence.cmi \
-    misc/ns.cmi types/intervals.cmi types/ident.cmo misc/encodings.cmi \
-    types/chars.cmi parser/cduce_loc.cmi types/atoms.cmi parser/ast.cmo \
-    parser/parser.cmi
-parser/parser.cmx : parser/ulexer.cmx types/types.cmx types/sequence.cmx \
-    misc/ns.cmx types/intervals.cmx types/ident.cmx misc/encodings.cmx \
-    types/chars.cmx parser/cduce_loc.cmx types/atoms.cmx parser/ast.cmx \
-    parser/parser.cmi
+parser/parser.cmo : types/var.cmi parser/ulexer.cmi types/types.cmi \
+    types/sequence.cmi misc/ns.cmi types/intervals.cmi types/ident.cmo \
+    misc/encodings.cmi types/chars.cmi parser/cduce_loc.cmi types/atoms.cmi \
+    parser/ast.cmo parser/parser.cmi
+parser/parser.cmx : types/var.cmx parser/ulexer.cmx types/types.cmx \
+    types/sequence.cmx misc/ns.cmx types/intervals.cmx types/ident.cmx \
+    misc/encodings.cmx types/chars.cmx parser/cduce_loc.cmx types/atoms.cmx \
+    parser/ast.cmx parser/parser.cmi
 typing/typed.cmo : types/var.cmi misc/utils.cmo misc/upool.cmi \
     types/types.cmi schema/schema_validator.cmi types/patterns.cmi \
     misc/ns.cmi types/intervals.cmi types/ident.cmo misc/encodings.cmi \

ocaml @ f12f6969

-Subproject commit 35b008173b9a6af2ca3de5dacbc44367dbe6defc
+Subproject commit f12f696955d17ef8a9074f1dc7fe7be24d6c95e5

parser/ast.ml

@@ -105,7 +105,6 @@ and branches = (ppat * pexpr) list
 
 and ppat = ppat' located
 and ppat' =
-  | TVar of U.t (** polymorphic type variables *)
   | PatVar of U.t list
   | Cst of pexpr
   | NsT of U.t

parser/parser.ml

@@ -25,7 +25,7 @@ module Gram = Camlp4.Struct.Grammar.Static.Make(Ulexer)
 
 let id_dummy = U.mk "$$$"
 
-let ident s =
+let ident_aux s =
   let b = Buffer.create (String.length s) in
   let rec aux i =
     if (i = String.length s) then Buffer.contents b
@@ -35,8 +35,8 @@ let ident s =
   in
   aux 0
 
-let label s = U.mk (ident s)
-let ident s = U.mk (ident s)
+let label s = U.mk (ident_aux s)
+let ident s = U.mk (ident_aux s)
 
 let prog    = Gram.Entry.mk "prog"
 let top_phrases   = Gram.Entry.mk "toplevel phrases"
@@ -596,17 +596,17 @@ EXTEND Gram
   located_ident: [ [ a = ident_or_keyword -> (lop _loc,ident a) ] ];
 
   pat: [
-      [ x = pat; "where";
-        b = LIST1 [ (la,a) = located_ident; "="; y = pat ->
-		      (la,a,y) ] SEP "and"
-            -> mk _loc (Recurs (x,b)) ]
+    [ x = pat; "where";
+      b = LIST1 [ (la,a) = located_ident; "="; y = pat -> (la,a,y) ] SEP "and" -> 
+        mk _loc (Recurs (x,b)) ]
     | RIGHTA [ x = pat; "->"; y = pat -> mk _loc (Arrow (x,y))
              | x = pat; "@"; y = pat -> mk _loc (Concat (x,y))
              | x = pat; "+"; y = pat -> mk _loc (Merge (x,y)) ]
     | "no_arrow" [ x = pat; "|"; y = pat -> mk _loc (Or (x,y)) ]
     | "simple" [ x = pat; "&"; y = pat -> mk _loc (And (x,y))
 	       | x = pat; "\\"; y = pat -> mk _loc (Diff (x,y)) ]
-    | "var_typ" [ x = PTYPE -> mk _loc (TVar (ident x)) ]
+    | "var_typ" [ x = PTYPE -> 
+        mk _loc (Internal (Types.var (Var.mk (ident_aux x)))) ]
     |
       [ "{"; r = record_spec; "}" -> r
       | "ref"; p = pat ->

tests/poly/part2.cd

+
 let pretty (x : Int) : String = string_of x;;
 let even (Int -> Bool; ('a\Int) -> ('a\Int))
 | x & Int -> (x mod 2) = 0
@@ -42,10 +43,7 @@ let balance ( Unbal ->Rtree ; ('b \ Unbal) ->('b \ Unbal) )
   | x -> x
 ;;
 let r = balance <blk elem=1>[ <red elem=1>[ <red elem=1>[ 1 2] 3 ]4];;
-let id ('a -> 'a)
-    Int  -> "foo"
-  | x -> x
-;;
+
 
 (* some tricky examples *)
 

tests/poly/patricia.cd

@@ -66,7 +66,7 @@ let merge (c: 'a -> 'a -> 'a): (Dict,Dict) -> Dict =
           ; (Dict,Dict)\([],[]) -> Dict\[] 
           ; (Branch,Branch) -> Branch )
     | ([],t) | (t,[]) -> t
-    | (<leaf key=k>x , t) ->  insert c k x t         
+    | (<leaf key=k>x , t) ->  insert c k x t      
     | (t , <leaf key=k>x) ->  insert (swap c) k x t  
     | (<brch pre=p bit=m>[ s0 s1 ] , <brch pre=q bit=n>[ t0 t1 ])&(s,t) ->
         if (m=n) && (p=q) then  <brch pre=p bit=m>[ (aux(s0,t0)) (aux(s1,t1)) ]

types/types.ml

@@ -3387,7 +3387,7 @@ module Tallying = struct
 
   (* Add constraints of the form { alpha = ( s v fresh ) ^ t } *)
 
-  let solve s =
+  let solve delta s =
 
     let aux alpha (s,t) acc =
       (* we cannot solve twice the same variable *)
@@ -3406,9 +3406,11 @@ module Tallying = struct
                * means that the constraint is of the form (alpha,beta). *)
           if is_var t then begin
             let (beta,_) = extract_variable t in
-            let acc1 = aux beta (empty,any) acc in
-                (* alpha <= beta --> { empty <= alpha <= beta ; empty <= beta <= any } *)
-            aux alpha (s,t) acc1
+            if Var.Set.mem beta delta then aux alpha (s, t) acc
+            else
+              let acc1 = aux beta (empty,any) acc in
+            (* alpha <= beta --> { empty <= alpha <= beta ; empty <= beta <= any } *)
+              aux alpha (s,t) acc1
           end else
             (* alpha = ( s v fresh) ^ t *)
             aux alpha (s,t) acc;
@@ -3460,21 +3462,13 @@ module Tallying = struct
     if Pervasives.(n = CS.unsat) then raise Step1Fail else
     let m =
       CS.S.fold (fun c acc ->
-        try CS.ES.union (solve (merge delta c)) acc
+        try CS.ES.union (solve delta (merge delta c)) acc
         with UnSatConstr _ -> acc
       ) n CS.ES.empty
     in
     if CS.ES.is_empty m then raise Step2Fail else
     let el =
-      let dom e = CS.E.fold (fun v _ acc -> Var.Set.add v acc) e Var.Set.empty in
-      CS.ES.fold (fun e acc ->
-        let si = unify e in
-        (* XXX maybe we can eliminate solution earlier. Is it safe to do it here ? *)
-        (* it is a solution only if (dom(si) /\ delta = emptyset) *)
-        if Var.Set.is_empty (Var.Set.inter (dom(si)) delta) then
-          CS.ES.add si acc
-        else acc
-      ) m CS.ES.empty
+      CS.ES.fold (fun e acc -> CS.ES.add (unify e) acc ) m CS.ES.empty
     in
     (CS.ES.elements el)
 

types/types.mli

@@ -427,7 +427,7 @@ module Tallying : sig
 
   val norm : Var.Set.t -> t -> CS.s
   val merge : Var.Set.t -> CS.m -> CS.s
-  val solve : CS.s -> CS.es
+  val solve : Var.Set.t -> CS.s -> CS.es
   val unify : CS.sigma -> CS.sigma
 
   (* [s1 ... sn] . si is a solution for tallying problem

types/var.ml

+
 module V = struct
-  type t = { id : string ; fr : int }
-  let dump ppf t = Format.fprintf ppf "{%s(%d)}" t.id t.fr
+  type t = { id : Ident.U.t ; fr : int }
+  let dump ppf t = Format.fprintf ppf "{%a(%d)}" Ident.U.print t.id t.fr
   let compare x y = Pervasives.compare (x.id,x.fr) (y.id,y.fr)
   let equal x y = (compare x y) = 0
   let hash x = Hashtbl.hash (x.id,x.fr)
   let check _ = ()
-  let id x = x.id
 
   let is_fresh x = x.fr > 0
+  let fresh v = { v with fr = v.fr + 1 }
 
-  let mk id = { id = id ; fr = 0 }
-
-  let pp ppf x =
-    (*
-    let pre = if x.fr == 0 then "" else (Printf.sprintf "_fresh_%d" x.fr) in
-  *)
-    Format.fprintf ppf "'%s" x.id
+  let mk id = { id = Ident.U.mk id; fr = 0 }
+  let id x = Ident.U.get_str x.id
 
-  let fresh v = { v with fr = v.fr + 1 }
+  let pp ppf x = Format.fprintf ppf "'%a" Ident.U.print x.id
 end
 
 include V

types/var.mli

@@ -6,8 +6,8 @@ val pp : Format.formatter -> t -> unit
 val mk : string -> t
 val id : t -> string
 val fresh : t -> t
-val is_fresh : t -> bool
 (*
+val is_fresh : t -> bool
 val is_internal : t -> bool
 *)
 

typing/typer.ml

@@ -333,7 +333,6 @@ module IType = struct
   (* Ast -> symbolic type *)
   let rec derecurs env p =
     match p.descr with
-    | TVar s -> mk_type (Types.var (Var.mk (U.to_string s)))
     | PatVar ids -> derecurs_var env p.loc ids
     | Recurs (p,b) -> derecurs (fst (derecurs_def env b)) p
     | Internal t -> mk_type t
@@ -1112,8 +1111,17 @@ and type_check' loc env ed constr precise = match ed with
       (ed,verify loc t constr)
 
   | Ref (e,t) ->
-      ignore (type_check env e (Types.descr t) false);
-      (ed,verify loc (Builtin_defs.ref_type t) constr)
+      let td = Types.descr t in
+      let vars = Types.all_vars td in
+      if not(Var.Set.subset vars env.delta) then
+        error loc (
+          Printf.sprintf
+            "Type ref %s constains polymorphic variables"
+            (Types.Print.string_of_type td))
+      else begin
+        ignore (type_check env e td false);
+        (ed,verify loc (Builtin_defs.ref_type t) constr)
+      end
 
   | External (t,_) ->
       (ed,verify loc t constr)