Commit 7655fee1 authored by Julien Lopez's avatar Julien Lopez
Browse files

Add a check on sigmas domain before optimizing comp (relies on a dummy codomain

	function so it's not working for now)
[TESTS][LAMBDA] Add chars (shows it should be easy to use the '<uident> syntax
	for type variables in CDuce)
parent 2b3cb297
......@@ -66,6 +66,12 @@ let rec domain = function
|Comp (s1,s2) -> Var.Set.union (domain s1) (domain s2)
|Sel(_,_,sigma) -> (domain sigma)
let rec codomain = function
| Identity -> Var.Set.empty
| List(l) -> Types.Tallying.codomain l
| Comp(s1,s2) -> Var.Set.union (codomain s1) (codomain s2)
| Sel(_,_,sigma) -> (codomain sigma)
let fresharg =
let count = ref 0 in
function () ->
......@@ -82,6 +88,7 @@ let fresharg =
let rec comp s1 s2 = match s1, s2 with
| Identity, _ -> s2
| _, Identity -> s1
| _, _ when Var.Set.inter (domain s1) (codomain s2) != Var.Set.empty -> Comp(s1, s2)
(* If l1 subsigma of l2 or l2 subsigma of l1 then we keep the biggest *)
| List(l1), List(l2) -> (match Types.Tallying.subsigma l1 l2 with
| None -> Comp(s1, s2)
......
......@@ -63,68 +63,6 @@ let eval_var env locals = function
let tag_op_resolved = Obj.tag (Obj.repr (OpResolved ((fun _ -> assert false), [])))
let tag_const = Obj.tag (Obj.repr (Const (Obj.magic 0)))
(* ------------ Debugging printer *)
let print_lst f ppf l =
let rec aux ppf = function
|[] -> Format.fprintf ppf "@."
|[h] -> Format.fprintf ppf "%a" f h
|h::t -> Format.fprintf ppf "%a,%a" f h aux t
in
match l with
|[] -> Format.fprintf ppf ""
|_ -> Format.fprintf ppf "%a" aux l
let rec pp_sigma ppf =
let pp_aux ppf =
print_lst (fun ppf (t1,t2) ->
Format.fprintf ppf "(%a -> %a)"
Types.Print.print t1
Types.Print.print t2
) ppf
in
function
|Value.List ll -> Types.Tallying.CS.pp_sl ppf ll
|Value.Comp(s1,s2) -> Format.fprintf ppf "Comp(%a,%a)" pp_sigma s1 pp_sigma s2
|Value.Sel(x,iface,s) -> Format.fprintf ppf "Sel(%d,%a,%a)" x pp_aux iface pp_sigma s
|Value.Identity -> Format.fprintf ppf "Id"
|Value.Mono -> Format.fprintf ppf "Mono"
and pp_value ppf = function
| Value.Pair(v1, v2, sigma) ->
Format.fprintf ppf "(%a,%a,%a)"
pp_value v1
pp_value v2
pp_sigma sigma
| Xml(_,_,_,sigma) -> Format.fprintf ppf "Xml(%a)" pp_sigma sigma
| XmlNs(_,_,_,_,sigma) -> Format.fprintf ppf "XmlNs(%a)" pp_sigma sigma
| Record(_,sigma) -> Format.fprintf ppf "Record(%a)" pp_sigma sigma
| Atom(a) -> Format.fprintf ppf "Atom(%a)" Atoms.V.print a
| Integer(i) -> Format.fprintf ppf "%d" (Intervals.V.get_int i)
| Char(i) -> Format.fprintf ppf "Char()"
| Abstraction(None, _, sigma) ->
Format.fprintf ppf "Abstraction(None,%a)" pp_sigma sigma
| Abstraction(Some t, _, sigma) ->
Format.fprintf ppf "Abstraction(%a,%a)"
pp_iface t
pp_sigma sigma
| Abstract((name, _)) -> Format.fprintf ppf "Abstract(%s)" name
| String_latin1(_,_,s,_) -> Format.fprintf ppf "\"%s\"" s
| String_utf8(_,_,s,_) -> Format.fprintf ppf "\"%s\"" (Encodings.Utf8.get_str s)
| Concat(v1, v2) ->
Format.fprintf ppf "Concat(%a, %a)"
pp_value v1
pp_value v2
| Absent -> Format.fprintf ppf "Absent"
and pp_iface ppf l =
let f ppf (t1,t2) =
Format.fprintf ppf "(%a,%a)"
Types.Print.print t1
Types.Print.print t2
in
print_lst f ppf l
let pp_lambda_env ppf env locals =
let aux a =
let l = Array.to_list a in
......@@ -137,8 +75,6 @@ let pp_lambda_env ppf env locals =
in
Format.fprintf ppf "env = {%s}; locals = {%s}" (aux env) (aux locals)
(* ---------------- *)
let apply_sigma sigma = function
|Value.Pair(v1,v2,sigma') -> Value.Pair(v1,v2,Value.comp sigma sigma')
|Value.Abstraction(iface,f,sigma') -> Value.Abstraction(iface,f,Value.comp sigma sigma')
......
......@@ -24,6 +24,18 @@ and t =
| Concat of t * t
| Absent
let rec domain = function
| Identity | Mono -> Var.Set.empty
| List(l) -> Types.Tallying.domain l
| Comp(s1,s2) -> Var.Set.union (domain s1) (domain s2)
| Sel(_,_,sigma) -> (domain sigma)
let rec codomain = function
| Identity | Mono -> Var.Set.empty
| List(l) -> Types.Tallying.codomain l
| Comp(s1,s2) -> Var.Set.union (codomain s1) (codomain s2)
| Sel(_,_,sigma) -> (codomain sigma)
(*
Comp for Value.sigma but simplify if possible.
TODO: - Merge with the comp function in compile.ml
......@@ -34,6 +46,7 @@ let rec comp s1 s2 = match s1, s2 with
| _, Identity -> s1
| Mono, _ -> s2
| _, Mono -> s1
| _, _ when Var.Set.inter (domain s1) (codomain s2) != Var.Set.empty -> Comp(s1, s2)
(* If l1 subsigma of l2 or l2 subsigma of l1 then we keep the biggest *)
| List(l1), List(l2) -> (match Types.Tallying.subsigma l1 l2 with
| None -> Comp(s1, s2)
......@@ -342,7 +355,7 @@ let rec pp_value ppf = function
| Record(_,sigma) -> Format.fprintf ppf "Record(%a)" pp_sigma sigma
| Atom(a) -> Format.fprintf ppf "Atom(%a)" Atoms.V.print a
| Integer(i) -> Format.fprintf ppf "%d" (Big_int.int_of_big_int i)
| Char(i) -> Format.fprintf ppf "Char()"
| Char(i) -> Format.fprintf ppf "'%c'" (Chars.V.to_char i)
| Abstraction(None, _, sigma) ->
Format.fprintf ppf "Abstraction(None,%a)" pp_sigma sigma
| Abstraction(Some t, _, sigma) ->
......
......@@ -78,6 +78,9 @@ let rec _to_typed env l expr =
let i = Big_int.big_int_of_int 0 in
let s = Types.String (0, (String.length s) - 1, s, Types.Integer i) in
env, l, { exp_loc=loc; exp_typ=Builtin_defs.string; exp_descr=Cst s }
| Char (_, c) ->
env, l, { exp_loc=loc; exp_typ=Builtin_defs.char;
exp_descr=Cst (Types.Char (Chars.V.mk_char c)) }
| Atom (origloc, b) ->
let t = Builtin_defs.true_type in
let f = Builtin_defs.false_type in
......@@ -233,14 +236,16 @@ and parse_match_value env l list toptype = function
(t2, Patterns.Cap(d1, d2), list, l, is_subtype)
| MInt (_, i) ->
let t = Types.constant (Types.Integer(Big_int.big_int_of_int i)) in
let is_subtype = Types.subtype Builtin_defs.int
(type_of_ptype toptype) in
let is_subtype = Types.subtype t (type_of_ptype toptype) in
(t, Patterns.Constr(t), list, l, is_subtype)
| MString (_, s) ->
let zero = Types.Integer(Big_int.big_int_of_int 0) in
let t = Types.constant (Types.String(0, String.length s - 1, s, zero)) in
let is_subtype = Types.subtype Builtin_defs.string
(type_of_ptype toptype) in
let is_subtype = Types.subtype t (type_of_ptype toptype) in
(t, Patterns.Constr(t), list, l, is_subtype)
| MChar (_, c) ->
let t = Types.constant (Types.Char(Chars.V.mk_char c)) in
let is_subtype = Types.subtype t (type_of_ptype toptype) in
(t, Patterns.Constr(t), list, l, is_subtype)
| MAtom (origloc, b) ->
let t = match b with
......
......@@ -340,6 +340,9 @@ let tests_eval = "CDuce runtime tests (Typed -> Lambda -> Value)" >:::
assert_equal ~msg:"Test CDuce.runtime.string.simple failed"
~printer:(fun x -> x) "\"The cake is a lie\""
(run_test_eval "\"The cake is a lie\"");
assert_equal ~msg:"Test CDuce.runtime.string.char failed"
~printer:(fun x -> x) "'c'"
(run_test_eval "'c'");
);
"list" >:: ( fun test_ctxt ->
......@@ -482,6 +485,12 @@ let tests_eval = "CDuce runtime tests (Typed -> Lambda -> Value)" >:::
(run_test_eval "(fun tail x : ['A] : ['A] -> match x : ['A] with
| (_ : 'A) :: (rest : ['A]) -> rest).[3; 7; 8; 5]");
assert_equal ~msg:"Test CDuce.runtime.poly.multicomp failed"
~printer:(fun x -> x) "Abstraction((`$A,`$A),Sel(1,(`$A -> `$A),Comp({ { `$A = Int
} },{ { `$A = [ Char* ]
} })))"
(run_test_eval "(((fun f x : 'A : 'A -> x)[{A/Int}])[{A/String}])[{A/Int}]");
);
]
......
......@@ -11,6 +11,7 @@ type expr =
| Var of Loc.t * string
| Int of Loc.t * int
| String of Loc.t * string
| Char of Loc.t * char
| Atom of Loc.t * string
and fun_name = string
and fv = (int * string) list
......@@ -20,6 +21,7 @@ and match_value =
| MVar of Loc.t * string * ptype
| MInt of Loc.t * int
| MString of Loc.t * string
| MChar of Loc.t * char
| MAtom of Loc.t * string
and ptype =
| Type of string
......@@ -105,6 +107,7 @@ module ExprParser = struct
| "var" [ x = LIDENT -> Var(_loc, x) ]
| "int" [ x = INT -> Int(_loc, int_of_string x) ]
| "string" [ x = STRING -> String(_loc, x) ]
| "char" [ x = CHAR -> Char(_loc, x.[0]) ]
| "atom" [ "`"; x = LIDENT -> Atom(_loc, x) ]
| "subst" NONA [
e = SELF; "["; s = LIST0 sigma SEP ","; "]" -> Subst(_loc, e, s) ]
......@@ -128,6 +131,7 @@ module ExprParser = struct
| "var" [ x = LIDENT; ":"; t = type_id -> MVar(_loc, x, t) ]
| "int" [ x = INT -> MInt(_loc, int_of_string x) ]
| "string" [ x = STRING -> MString(_loc, x) ]
| "char" [ x = CHAR -> MChar(_loc, x.[0]) ]
| "atom" [ "`"; x = LIDENT -> MAtom(_loc, x) ]
| "empty" [ "["; "]" -> MAtom(_loc, "nil") ]
];
......@@ -167,6 +171,7 @@ let get_loc expr = match expr with
| Var (loc, _) -> loc
| Int (loc, _) -> loc
| String (loc, _) -> loc
| Char (loc, _) -> loc
| Atom (loc, _) -> loc
let caml_loc_to_cduce loc =
......
......@@ -10,6 +10,7 @@ type expr =
| Var of Loc.t * string
| Int of Loc.t * int
| String of Loc.t * string
| Char of Loc.t * char
| Atom of Loc.t * string
and fun_name = string
and fv = (int * string) list
......@@ -19,6 +20,7 @@ and match_value =
| MVar of Loc.t * string * ptype
| MInt of Loc.t * int
| MString of Loc.t * string
| MChar of Loc.t * char
| MAtom of Loc.t * string
and ptype =
| Type of string
......
......@@ -3238,6 +3238,13 @@ module Tallying = struct
) e acc
) Var.Set.empty ll
let codomain ll =
List.fold_left (fun acc e ->
CS.E.fold (fun v _ acc ->
Var.Set.add v acc
) e acc
) Var.Set.empty ll
(* Returns Some l2 if l1 is a subsigma of l2, Some l1 if l2 is a subsigma of
l1, None otherwise. *)
let subsigma l1 l2 =
......
......@@ -422,6 +422,7 @@ module Tallying : sig
val tallying : (t * t) list -> CS.sl
val (@@) : t -> CS.sigma -> t
val domain : CS.sl -> Var.Set.t
val codomain : CS.sl -> Var.Set.t
val subsigma : CS.sl -> CS.sl -> CS.sl option
val is_identity : CS.sl -> bool
......
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