Commit deae103a authored by Pietro Abate's avatar Pietro Abate
Browse files

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

Original author: cvscast
Date: 2002-10-26 21:32:21+00:00
parent 8683071e
......@@ -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
......
......@@ -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:
......
......@@ -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 ->
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment