[r2002-10-26 21:32:21 by cvscast] Empty log message

Original author: cvscast
Date: 2002-10-26 21:32:21+00:00

parser/ast.ml

@@ -22,7 +22,8 @@ and pexpr = pexpr' located
 and pexpr' = 
   (* For debugging the typer: an expression with prescribed type *)
   | DebugTyper of ppat
-    
+
+  | Forget of pexpr * ppat    
   (* CDuce is a Lambda-calculus ... *)
   | Var of string
   | Apply of pexpr * pexpr
@@ -54,7 +55,7 @@ and ppat' =
   | Recurs of ppat * (string * ppat) list
   | Internal of Types.descr
   | Or of ppat * ppat
-  | And of ppat * ppat
+  | And of ppat * ppat * bool
   | Diff of ppat * ppat
   | Prod of ppat * ppat
   | Arrow of ppat * ppat

parser/parser.ml

@@ -65,6 +65,8 @@ EXTEND
 	mk loc (Abstraction { fun_name = f; fun_iface = a; fun_body = b })
     | (p,e1) = let_binding; "in"; e2 = expr LEVEL "top"->
         mk loc (Match (e1,[p,e2]))
+    | e = expr; ":"; p = pat ->
+	mk loc (Forget (e,p))
     ]
 
     
@@ -109,6 +111,7 @@ EXTEND
 	  
   let_binding: [
     [ "let"; p = pat; "="; e = expr -> (p,e)
+    | "let"; p = pat; ":"; t = pat; "="; e = expr -> (p, mk noloc (Forget (e,t)))
     | "let"; "fun"; (f,a,b) = fun_decl ->
 	let p = match f with 
 	  | Some x -> mk loc (Capture x)
@@ -175,8 +178,9 @@ EXTEND
             -> mk loc (Recurs (x,b)) ]
     | RIGHTA [ x = pat; "->"; y = pat -> mk loc (Arrow (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)) ]
+    | "simple" [ x = pat; "&"; y = pat -> mk loc (And (x,y,true)) 
+(*	       | x = pat; ":"; y = pat -> mk loc (And (x,y,false))   *)
+	       | x = pat; "-"; y = pat -> mk loc (Diff (x,y)) ]
     | 
       [ "{"; r = record_spec; "}" -> r
       | LIDENT "_" -> mk loc (Internal Types.any)
@@ -220,7 +224,7 @@ EXTEND
                 ] SEP ";" ->
         match r with
           | [] -> mk loc (Internal Types.Record.any)
-          | h::t -> List.fold_left (fun t1 t2 -> mk loc (And (t1,t2))) h t
+          | h::t -> List.fold_left (fun t1 t2 -> mk loc (And (t1,t2,true))) h t
       ] ];
   
   char:

runtime/value.ml

@@ -182,6 +182,7 @@ and run_disp_field v bindings fields l vl = function
 
 let rec eval env e0 = 
   match e0.Typed.exp_descr with
+    | Typed.Forget (e,_) -> eval env e
     | Typed.Var s -> Env.find s env
     | Typed.Apply (f,arg) ->  eval_apply (eval env f) (eval env arg)
     | Typed.Abstraction a ->

types/patterns.ml

@@ -9,7 +9,7 @@ exception IllFormedCap of fv * fv
 type d =
   | Constr of Types.node
   | Cup of descr * descr
-  | Cap of descr * descr
+  | Cap of descr * descr * bool
   | Times of node * node
   | Record of Types.label * node
   | Capture of capture
@@ -36,9 +36,9 @@ let constr x = (Types.descr x,[],Constr x)
 let cup ((acc1,fv1,_) as x1) ((acc2,fv2,_) as x2) = 
   if fv1 <> fv2 then raise (IllFormedCup (fv1,fv2));
   (Types.cup acc1 acc2, SortedList.cup fv1 fv2, Cup (x1,x2))
-let cap ((acc1,fv1,_) as x1) ((acc2,fv2,_) as x2) = 
+let cap ((acc1,fv1,_) as x1) ((acc2,fv2,_) as x2) e = 
   if not (SortedList.disjoint fv1 fv2) then raise (IllFormedCap (fv1,fv2));
-  (Types.cap acc1 acc2, SortedList.cup fv1 fv2, Cap (x1,x2))
+  (Types.cap acc1 acc2, SortedList.cup fv1 fv2, Cap (x1,x2,e))
 let times x y =
   (Types.times x.accept y.accept, SortedList.cup x.fv y.fv, Times (x,y))
 let record l x = 
@@ -74,8 +74,10 @@ let rec filter_descr t (_,fv,d) : (capture, Types.Positive.v) SortedMap.t =
 	  SortedMap.union cup_res
 	    (filter_descr (Types.cap t a) d1)
 	    (filter_descr (Types.diff t a) d2)
-      | Cap (d1,d2) ->
+      | Cap (d1,d2,true) ->
 	  SortedMap.union cup_res (filter_descr t d1) (filter_descr t d2)
+      | Cap ((a1,_,_) as d1, ((a2,_,_) as d2), false) ->
+	  SortedMap.union cup_res (filter_descr a2 d1) (filter_descr a1 d2)
       | Times (p1,p2) ->
 	  List.fold_left 
 	    (fun accu (d1,d2) ->
@@ -261,7 +263,7 @@ struct
     then empty
     else match d with
       | Constr t -> constr (Types.descr t)
-      | Cap (p,q) -> cap (nf p) (nf q)
+      | Cap (p,q,_) -> cap (nf p) (nf q)
       | Cup ((acc1,_,_) as p,q) -> cup acc1 (nf p) (nf q)
       | Times (p,q) -> times acc p q
       | Capture x -> capture x

types/patterns.mli

@@ -15,7 +15,7 @@ val define: node -> descr -> unit
 
 val constr : Types.node -> descr
 val cup    : descr -> descr -> descr
-val cap    : descr -> descr -> descr
+val cap    : descr -> descr -> bool -> descr
 
 val times  : node -> node -> descr 
 val record : Types.label -> node -> descr

typing/typed.ml

@@ -21,6 +21,7 @@ type texpr  = { exp_loc : loc;
 and  texpr' = 
   | DebugTyper of ttyp
 
+  | Forget of texpr * ttyp
   (* CDuce is a Lambda-calculus ... *)
   | Var of string
   | Apply of texpr * texpr

typing/typer.ml

@@ -29,7 +29,7 @@ and descr =
    [ `Alias of string * ti
    | `Type of Types.descr
    | `Or of ti * ti
-   | `And of ti * ti
+   | `And of ti * ti * bool
    | `Diff of ti * ti
    | `Times of ti * ti
    | `Arrow of ti * ti
@@ -113,7 +113,7 @@ module Regexp = struct
 	    compile fin e rest
 	| `Elem (vars,x) :: rest -> 
 	    let capt = StringSet.fold
-			 (fun v t -> mk noloc (And (t, (mk noloc (Capture v)))))
+			 (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 -> 
@@ -139,7 +139,7 @@ module Regexp = struct
 
   let atom_nil = Types.mk_atom "nil"
   let constant_nil v t = 
-    mk noloc (And (t, (mk noloc (Constant (v, Types.Atom atom_nil)))))
+    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
@@ -165,7 +165,7 @@ let rec compile env { loc = loc; descr = d } : ti =
   | 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) -> cons loc (`And (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))
@@ -189,7 +189,7 @@ let rec comp_fv seen s =
 	  match s.descr' with
 	    | `Alias (_,x) -> if List.memq s seen then [] else comp_fv (s :: seen) x
 	    | `Or (s1,s2) 
-	    | `And (s1,s2)
+	    | `And (s1,s2,_)
 	    | `Diff (s1,s2)
 	    | `Times (s1,s2)
 	    | `Arrow (s1,s2) -> SortedList.cup (comp_fv seen s1) (comp_fv seen s2)
@@ -214,7 +214,7 @@ let rec typ seen s : Types.descr =
 	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)
+    | `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)
@@ -243,10 +243,10 @@ let rec pat seen s : Patterns.descr =
 	       ("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) -> Patterns.cap (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)
+	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)
@@ -302,6 +302,9 @@ 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
@@ -406,6 +409,10 @@ let rec type_check env e constr precise =
   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 
@@ -475,24 +482,21 @@ and type_check' loc env e constr precise = match e with
 
       let constr' = Sequence.approx (Types.cap Sequence.any constr) in
       let exact = Types.subtype (Sequence.star constr') constr in
-
-      if exact then (
-	(* Note: typing mail fail because of the approx on t *)
-	let res = type_check_branches loc env (Sequence.approx t) 
-		    b constr' precise in
-	if precise then Sequence.star res else constr
-      )
-      else
-	(* 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' true) 
-	    t in
-	if not exact then check loc res constr "";
-	if precise then res else constr
+(*
+      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