Commit fb36149d authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Several fixes for handling of polymorphic variables and instanciation:

- fix the scoping of (fun ('a -> 'a -> 'a) x -> (fun ('a -> 'a) y -> ...))
so that the second interface uses the same 'a as the first
- prevent global declration of polymorphic values that are not functions (unsound
in the absence of value restriction because of side effects).
- add more complex test cases for polymorphic types and functions.
parent 56ff4182
Pipeline #166 passed with stages
in 7 minutes and 36 seconds
......@@ -147,7 +147,8 @@ let logical_not e = if_then_else e cst_false cst_true
let rec pat_fold f acc p =
let nacc = f acc p in
match p.descr with
| Poly _ | PatVar _ | Cst _ | NsT _ | Internal _ | Constant _ -> nacc
| Poly _ | Cst _ | NsT _ | Internal _ | Constant _ -> nacc
| PatVar (_, pl) -> List.fold_left (fun acc pi -> pat_fold f acc pi) acc pl
| Recurs (p0, pl) ->
List.fold_left
(fun acc (_, _, pi) -> pat_fold f acc pi)
......
......@@ -88,7 +88,7 @@ let id_dummy = U.mk "$$$"
let mk_app_pat loc var l =
match var.Cduce_loc.descr with
PatVar(p, []) -> mk loc (PatVar(p, l))
| _ -> assert false
| _ -> parsing_error loc "invalid parametric type"
%}
/* Keywords */
......@@ -312,7 +312,6 @@ match n with
%inline type_params:
| { [] }
| s = POLY { [ U.mk s ] }
| "(" l = separated_nonempty_list(",", POLY) ")" {
let seen = ref [] in
List.map (fun s ->
......@@ -739,17 +738,18 @@ namespace_binding_rem:
multi_prod lnopos (List.map snd args),
multi_prod lnopos (List.map fst args)
in
let tres, body = List.fold_right
(fun args (tres,body) ->
let _, tres, body = List.fold_right
(fun args (i, tres, body) ->
let (targ,arg) = mkfun args in
let name = (lop $sloc, label ("anonymous_" ^ (string_of_int i))) in
let e = Abstraction
{ fun_name = None; fun_poly = []; fun_iface = [targ,tres];
{ fun_name = Some name; fun_poly = []; fun_iface = [targ,tres];
fun_body = [arg,body] }
in
let t = mknoloc (Arrow (targ,tres)) in
(t,e)
(i+1, t,exp $sloc e)
)
others (tres, body)
others (0, tres, body)
in
let (targ,arg) = mkfun ((x,t) :: args) in
[(targ,tres)],[(arg,body)]
......
......@@ -666,17 +666,18 @@ module IType = struct
'%s"
(Ident.to_string v)
(Var.name (Var.Set.choose undecl)));
let vars_mapping =
(* recreate the mapping in the correct order *)
let vars_args = List.map (fun v -> List.assoc v penv.penv_var) args in
let final_vars =
(* create a sequence 'a -> 'a_0 for all variables *)
List.map (fun (_, v) -> (v, Var.(mk (name v)))) penv.penv_var
List.map (fun v -> v, Var.(mk (name v))) vars_args
in
let subst =
Types.Subst.from_list
(List.map (fun (v, vv) -> (v, Types.var vv)) vars_mapping)
(List.map (fun (v, vv) -> (v, Types.var vv)) final_vars)
in
let t_rhs = Types.Subst.apply_full subst t_rhs in
(v, t_rhs, List.map snd vars_mapping))
(v, t_rhs, List.map snd final_vars))
(List.rev b)
in
List.iter
......@@ -730,11 +731,22 @@ module IType = struct
raise exn
let typ vars env t =
let aux loc d =
internalize d;
check_no_fv loc d;
try typ_node d with Patterns.Error s -> raise_loc_generic loc s
in
try
let penv = { (penv env) with penv_var = vars } in
let d = derec penv t in
check_no_fv t.loc d;
try typ_node d with Patterns.Error s -> raise_loc_generic t.loc s
let res = aux t.loc d in
List.iter
(fun (cu, name, params, ti, loc) ->
let tti = aux loc ti in
Types.Print.register_global cu name ~params (Types.descr tti))
!to_register;
clean_params ();
res
with exn ->
clean_on_err ();
raise exn
......@@ -996,12 +1008,19 @@ and var env loc s =
with Not_found -> raise_loc loc (UnboundId (id, false)))
and abstraction env loc a =
(* When entering a function (fun 'a 'b ... .('a -> 'b -> … ))
for each variable 'x from the interface
- if 'x is in env.poly_vars, it is bound higher in the AST, we need
to keep the associated unique variable
- if 'x is not in env.poly_vars or 'x is in a.fun_poly, a fresh
name must be generated and kept for subsequent use of the variable.
*)
let vset = (* collect all type variables from the interface*)
List.fold_left
(fun acc (t1, t2) -> collect_vars (collect_vars acc t1) t2)
USet.empty a.fun_iface
in
let vset = (* remove variables that are locally monomorphic *)
let vset = (* remove variables that are in scope *)
List.fold_left (fun acc (v, _) -> USet.remove v acc) vset env.poly_vars
in
let vset = List.fold_left (fun acc v -> USet.add v acc) vset a.fun_poly in
......@@ -1226,10 +1245,12 @@ and type_check' loc env e constr precise =
let t =
if Types.subtype a.fun_typ constr then a.fun_typ
else
let name = match a.fun_name with Some s -> "abstraction " ^ Ident.to_string s| None -> "the abstraction" in
should_have loc constr (Format.asprintf
"but the interface (%a) of the abstraction is not compatible with type
"but the interface (%a) of %s is not compatible with type
(%a)"
Types.Print.print a.fun_typ
name
Types.Print.print constr)
in
let env = { env with mono_vars = Var.Set.cup env.mono_vars (Types.Subst.vars a.fun_typ) } in
......@@ -1539,8 +1560,17 @@ let type_let_decl env p e =
let decl = let_decl env p e in
let typs = type_let_decl env decl in
report_unused_branches ();
List.iter (fun (id, t) ->
let remt = Types.(diff t Function.any) in
let vars = Types.Subst.vars remt in
if not (Var.Set.is_empty vars) then
raise_loc_generic p.loc
(Format.asprintf "The type of identifier %a is %a.@\nIt contains polymorphic variables that cannot be generalized."
Ident.print id
Types.Print.print t)
) typs;
let env = enter_values typs env in
(env, decl, typs)
({ env with mono_vars = Var.Set.empty; poly_vars = [] }, decl, typs)
let type_let_funs env funs =
clear_unused_branches ();
......@@ -1559,6 +1589,7 @@ let type_let_funs env funs =
let typs = type_rec_funs env funs in
report_unused_branches ();
let env = enter_values typs env in
let env = { env with mono_vars = Var.Set.empty; poly_vars = [] } in
(env, funs, typs)
(*
......
......@@ -38,6 +38,14 @@
(rule (alias overloading) (action (diff overloading.exp overloading.out)))
; end: overloading.cd
; begin: patricia.cd
(rule (deps patricia.cd) (target patricia.cdo)
(action (ignore-outputs (with-accepted-exit-codes 0 (run cduce --compile %{deps})))))
(rule (deps patricia.cdo) (target patricia.out)
(action (ignore-stderr (with-stdout-to %{target} (with-accepted-exit-codes 0 (run cduce --run %{deps}))))))
(rule (alias patricia) (action (diff patricia.exp patricia.out)))
; end: patricia.cd
; begin: poly-ok.cd
(rule (deps poly-ok.cd) (target poly-ok.cdo)
(action (ignore-outputs (with-accepted-exit-codes 0 (run cduce --compile %{deps})))))
......@@ -62,6 +70,7 @@
(alias lazy)
(alias map_even)
(alias overloading)
(alias patricia)
(alias poly-ok)
(alias web_site)
))
(* Patricia trees
Chris Okasaki and Andrew Gill's paper Fast Mergeable Integer Maps
http://ittc.ku.edu/~andygill/papers/IntMap98.pdf
*)
type Leaf('a) = <leaf key=Caml_int> 'a
type Branch('a) = <brch pre=Caml_int bit=Caml_int>[ (Leaf('a)|Branch('a)) (Leaf('a)|Branch('a)) ]
type Dict('a) = [] | Branch('a) | Leaf('a)
let lowest_bit (x: Caml_int): Caml_int = Stdlib.land x (-x :? Caml_int)
let branching_bit (p0: Caml_int)(p1: Caml_int): Caml_int = lowest_bit (Stdlib.lxor p0 p1)
let mask (p: Caml_int) (m: Caml_int): Caml_int =
Stdlib.land p (Stdlib.pred m)
let match_prefix (k: Caml_int)(p: Caml_int)(m: Caml_int): Bool =
mask k m = p
let zero_bit (k: Caml_int)(m: Caml_int): Bool = Stdlib.land k m = 0
let lookup (k: Caml_int) (d: Dict ('a)) : ['a?] =
match d with
| [] -> []
| <brch pre=p bit=m>[ t0 t1 ] ->
if not (match_prefix k p m) then []
else if zero_bit k m then lookup k t0
else lookup k t1
| <leaf key=j> x -> if j=k then [ x ] else []
;;
let join (p0: Caml_int) (t0: Dict('a)\[]) (p1: Caml_int) (t1: Dict('a)\[]): Branch('a) =
let m = branching_bit p0 p1 in
if zero_bit p0 m then
<brch pre=(mask p0 m) bit=m>[t0 t1]
else
<brch pre=(mask p0 m) bit=m>[t1 t0]
let insert (c: 'a -> 'a -> 'a) (k: Caml_int) (x: 'a) (t: Dict('a)): Leaf('a)|Branch('a) =
let ins (Leaf('a)|Branch('a) -> Leaf('a)|Branch('a) ; [] -> Leaf('a) )
| [] -> <leaf key=k> x
| (<leaf key=j>y)&t ->
if j=k then <leaf key=k>(c x y)
else join k (<leaf key=k>x) j t
| (<brch pre=p bit=m>[ t0 t1 ])&t ->
if match_prefix k p m then
if zero_bit k m then <brch pre=p bit=m>[ (ins t0) t1 ]
else <brch pre=p bit=m>[ t0 (ins t1) ]
else join k (<leaf key=k>x) p t
in ins t
let max (x: 'a)(y: 'b): 'a|'b = if (x >> y) then x else y;;
let swap (f : 'a -> 'a -> 'a) (x: 'a) (y: 'a): 'a = f y x;;
let merge (c: 'a -> 'a -> 'a): (Dict('a),Dict('a)) -> Dict('a) =
fun aux( ([],[]) -> []
; (Dict('a),Dict('a))\([],[]) -> Dict('a)\[]
; (Branch('a),Branch('a)) -> Branch('a) )
| ([],t) | (t,[]) -> 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)) ]
else if (m << n) && (match_prefix q p m) then
if zero_bit q m then <brch pre=p bit=m>[ (aux(s0,t)) s1 ]
else <brch pre=p bit=m>[ s0 (aux(s1,t)) ]
else if (m >> n) && (match_prefix p q n) then
if zero_bit p n then <brch pre=q bit=n>[ (aux(s,t0)) t1 ]
else <brch pre=q bit=n>[ t0 (aux(s,t1)) ]
else join p s q t
let iteri (f : Caml_int -> 'a -> []) (m : Dict('a)) : [] =
match m with
[] -> []
| <leaf key=k>v -> f k v
| <brch ..>[t1 t2] -> iteri f t1 ; iteri f t2
let iter (f : 'a -> []) (m : Dict ('a)) : [] =
iteri (fun ( _ : Any) (x : 'a) : [] = f x) m
/*
*/
let update (_ : 'a) (x : 'a) : 'a = x
;;
let init (data : [(Caml_int, 'a)*]) : Dict ('a) =
let acc = ref (Dict('a)) [] in
let [] =
transform data with
(x, y) -> acc := insert update x y !acc
in
!acc
let [] =
let map1 = init [ (1, "A") (2, "B") (1, "C" )] in
let map2 = init [ (1, "HELLO") (* replaces "A" and "C" *)
(3, "WORLD") (0, "0") ] in
let map3 = merge update (map1, map2) in
iter (fun (x : Any ) : [] = print [ !(string_of x) '\n' ]) map3
\ No newline at end of file
"0"
"B"
"HELLO"
"WORLD"
let pretty (x : Int) : String = string_of x
;;
let even (Int -> Bool; ('a\Int) -> ('a\Int))
| x & Int -> (x mod 2) = 0
| x -> x
;;
let mmap (f : 'a -> 'b) (l : [ ('a) *] ) : [ ('b) *] =
match l with
[] -> []
| (e, ll) -> (f e, mmap f ll)
;;
let map_even = mmap even
;;
let g ( (Int -> Int) -> Int -> Int;
(Bool -> Bool) -> Bool -> Bool) x -> x
;;
let id ('a -> 'a) x -> x;;
let gid = g id;;
let id2g = id (id g);;
let churchtrue (x : 'a) (_ : 'b) : 'a = x in churchtrue 42;;
let max (x : 'a) (y : 'a) : 'a = if x >> y then x else y;;
max 42;;
(* some tricky examples *)
let f (_ : ('a | 'b | 'c)) (_ : (Int&'d&'e \1--3 )) : Any = raise "123";;
let e = (even mmap) ;;
let x = id (even (e even));; (* same type as map_even *)
/*
The type is below is [ (1--6 | 'a -> 1--6 | 'a)* ]
with weak variables 'a that cannot be safely generlized.
let twisted = id even (even mmap) even (mmap max [1 2 3 4 5 6]);;
let apply_to_3 (f: Int -> 'a): 'a = f 3 in
mmap apply_to_3 twisted
;;
*/
type A('a) = <a>('a)
type B('a) = <b>[ A('a) | B('a) ];;
let f (_ : 'a -> 'a -> 'a )(z : 'a) (_ : A('a) | B('a)) : A('a) = <a>z;;
let sum (x : Int) (y : Int) : Int = x + y;;
let x = f sum;;
let f ( x : B('a) ) : 'a =
match x with
<b>[ <a>i ] -> i
|<b>[ y ] -> f y
;;
let v = f <b>[<b>[<a>32]]
;;
\ No newline at end of file
......@@ -303,10 +303,12 @@ module Print = struct
with Not_found -> (
try
let gname, params = DescrMap.find d !named in
named := DescrMap.remove d !named; (* break a cycle for named types occuring in their parameters*)
let s = alloc [] in
s.state <- `GlobalName (gname, params);
DescrHash.add memo d s;
s.def <- [ Name (gname, List.map prepare params) ];
DescrHash.add memo d s;
named := DescrMap.add d (gname, params) !named;
s
with Not_found ->
if Absent.get d then alloc [ Abs (prepare Absent.(update d false)) ]
......@@ -509,7 +511,8 @@ module Print = struct
and assign_name_rec = function
| Neg t -> assign_name t
| Abs t -> assign_name t
| Name _ | Char _ | Atomic _ | Interval _ | Display _ | Var _ -> ()
| Char _ | Atomic _ | Interval _ | Display _ | Var _ -> ()
| Name (_, params) -> List.iter assign_name params
| Intersection l -> List.iter assign_name l
| Regexp r -> assign_name_regexp r
| Diff (t1, t2) ->
......@@ -639,18 +642,6 @@ module Print = struct
| Abs t -> Format.fprintf ppf "?(@[%a@])" (do_print_slot lv_min) t
| Var v -> Format.fprintf ppf "%a" Var.print v
| Name (n, []) -> print_gname ppf n
| Name
( n,
[
({
def = [ (Name (_, []) | Record _ | Pair _ | Char _ | Var _) ];
_;
} as param);
] ) ->
opar ppf ~level:lv_app pri;
Format.fprintf ppf "@[%a@ %a@]" print_gname n (do_print_slot lv_app)
param;
cpar ppf ~level:lv_app pri
| Name (n, params) ->
opar ppf ~level:lv_app pri;
Format.fprintf ppf "@[%a@ (@[%a@])@]" print_gname n
......
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