Commit 01ee5746 authored by Pietro Abate's avatar Pietro Abate
Browse files

Merge branch 'propagate' of https://git.cduce.org/cduce into propagate

Conflicts:
	compile/compile.ml
parents 45b4e0aa 071890c0
......@@ -72,9 +72,13 @@ let fresharg =
(0,U.mk s)
;;
let comp = function
|Identity,s | s,Identity -> s
|s1,s2 -> Comp(s1,s2)
let comp s1 s2 = match s1, s2 with
| Identity, _ -> s2
| _, Identity -> s1
| List(l1), List(l2) -> (match Types.Tallying.subsigma l1 l2 with
| None -> Comp(s1, s2)
| Some l -> List(l))
| _, _ -> Comp(s1, s2)
(* from intermediate explicitely typed language to Evaluation language (lambda) *)
(* Typed -> Lambda *)
......@@ -94,7 +98,7 @@ and compile_aux env = function
in
if Var.Set.is_empty polyvars then Var (v)
else TVar(v,env.sigma)
| Typed.Subst(e,sl) -> compile { env with sigma = comp(env.sigma,(List sl)) } e
| Typed.Subst(e,sl) -> compile { env with sigma = comp env.sigma (List sl) } e
| Typed.ExtVar (cu,x,_) -> Var (find_ext cu x)
| Typed.Apply (e1,e2) -> Apply (compile env e1, compile env e2)
| Typed.Abstraction a -> compile_abstr env a
......
......@@ -76,11 +76,11 @@ let pp_lambda_env ppf env locals =
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'))
|Value.Xml(v1,v2,v3,sigma') -> Value.Xml(v1,v2,v3,Value.Comp(sigma,sigma'))
|Value.XmlNs(v1,v2,v3,ns,sigma') -> Value.XmlNs(v1,v2,v3,ns,Value.Comp(sigma,sigma'))
|Value.Record(m,sigma') -> Value.Record(m,Value.Comp(sigma,sigma'))
|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')
|Value.Xml(v1,v2,v3,sigma') -> Value.Xml(v1,v2,v3,Value.comp sigma sigma')
|Value.XmlNs(v1,v2,v3,ns,sigma') -> Value.XmlNs(v1,v2,v3,ns,Value.comp sigma sigma')
|Value.Record(m,sigma') -> Value.Record(m,Value.comp sigma sigma')
|v -> v
;;
......
......@@ -183,16 +183,12 @@ let rec run_disp_basic v f = function
let (@@) v sigma =
let open Value in
if sigma = Identity then v else
let comp = function
|Identity,s | s,Identity -> s
|s1,s2 -> Comp(s1,s2)
in
match v with
|Pair (v1,v2,s) -> Pair (v1,v2,comp(sigma,s))
|Xml (v1,v2,v3,s) -> Xml (v1,v2,v3,comp(sigma,s))
|XmlNs (v1,v2,v3,a,s) -> XmlNs (v1,v2,v3,a,comp(sigma,s))
|Record (r,s) -> Record (r,comp(sigma,s))
|Abstraction (iface,t,s) -> Abstraction (iface,t,comp(sigma,s))
|Pair (v1,v2,s) -> Pair (v1,v2,comp sigma s)
|Xml (v1,v2,v3,s) -> Xml (v1,v2,v3,comp sigma s)
|XmlNs (v1,v2,v3,a,s) -> XmlNs (v1,v2,v3,a,comp sigma s)
|Record (r,s) -> Record (r,comp sigma s)
|Abstraction (iface,t,s) -> Abstraction (iface,t,comp sigma s)
|_ -> v
let rec eval_sigma env =
......
......@@ -23,6 +23,14 @@ and t =
| Concat of t * t
| Absent
let comp s1 s2 = match s1, s2 with
| Identity, _ -> s2
| _, Identity -> s1
| List(l1), List(l2) -> (match Types.Tallying.subsigma l1 l2 with
| None -> Comp(s1, s2)
| Some l -> List(l))
| _, _ -> Comp(s1, s2)
(*
The only representation of the empty sequence is nil.
In particular, in String_latin1 and String_utf8, the string cannot be empty.
......
......@@ -24,6 +24,8 @@ and t =
| Concat of t * t
| Absent
val comp : sigma -> sigma -> sigma
module ValueSet: Set.S with type elt = t
exception CDuceExn of t
......
......@@ -151,9 +151,10 @@ and parse_abstr env l loc fun_name iface fv body =
let l = (match fun_name with
| None -> l
| Some (id, name) -> Locals.add name (id,fun_typ) l) in
(* Apparently, CDuce never uses btype (union of types of patterns) *)
let b, btype = parse_branches env l ptype [] Types.empty body in
let brs = { Typed.br_typ=btype; br_accept=accept_type btype;
br_branches=b } in
let t = type_of_ptype ptype in
let brs = { Typed.br_typ=t; br_accept=accept_type t; br_branches=b } in
let abstr = { Typed.fun_name=fun_name; fun_iface=iface; fun_body=brs;
fun_typ=fun_typ; fun_fv=fv } in
env, l, { Typed.exp_loc=caml_loc_to_cduce loc; exp_typ=fun_typ;
......
......@@ -72,9 +72,8 @@ let tests_poly_abstr = [
*)
"Test CDuce.lambda.identity_applied failed",
"Apply(Abstraction(Dummy,Dummy,,,,Sel(Env(1),(`$A -> `$A),Comp(Id,{ { `$A =
Int
} })),Env(1)),Const(2))",
"Apply(Abstraction(Dummy,Dummy,,,,Sel(Env(1),(`$A -> `$A),{ { `$A = Int
} }),Env(1)),Const(2))",
"(fun f x : 'A : 'A -> x)[{A/Int}].2";
];;
......@@ -236,7 +235,9 @@ Int -> Bool),(Bool -> Bool),(Any \\ (Int | Bool) -> Any \\ (Int | Bool)),Id))"
| x : (!Int) -> x).[4; \"hey\"; 3; 2]");
assert_equal ~msg:"Test CDuce.runtime.misc.map_even_hard failed"
~printer:(fun x -> x)
"(Atom(true),(\"hey\",((3,(5,Atom(nil),Id),Id),(Atom(true),(Abstraction((`$A,`$A),Sel(1,(`$A -> `$A),Id)),(Atom(false),Atom(nil),Id),Id),Id),Id),Id),Id)"
"(Atom(true),(\"hey\",((3,(5,Atom(nil),Id),{ { `$A = Int } ,{ `$A = Bool
} }),(Atom(true),(Abstraction((`$C,`$C),Comp({ { `$A = Int } ,{ `$A =
Bool } },Sel(1,(`$C -> `$C),Id))),(Atom(false),Atom(nil),Id),Id),Id),Id),Id),Id)"
(run_test_eval "(fun map f : ('A->'B) x : ['A] : ['B] ->
match x : ['A] with
| (el : 'A) :: (rest : ['A]) -> ((f.el), ((map.f).rest))
......@@ -444,9 +445,8 @@ X1 -> X1 where X1 = (Int,Int)),Id))"
(run_test_eval "fun f x : 'A : 'A -> x");
assert_equal ~msg:"Test CDuce.runtime.poly.identity failed"
~printer:(fun x -> x)
"Abstraction((`$A,`$A),Sel(1,(`$A -> `$A),Comp(Id,{ { `$A = Int
} ,{ `$A = [ Char* ]
} })))"
"Abstraction((`$A,`$A),Sel(1,(`$A -> `$A),{ { `$A = Int } ,{ `$A = [ Char* ]
} }))"
(run_test_eval "(fun f x : 'A : 'A -> x)[{A/Int},{A/String}]");
assert_equal ~msg:"Test CDuce.runtime.poly.identity_applied failed"
~printer:(fun x -> x) "2"
......
......@@ -3238,6 +3238,17 @@ module Tallying = struct
) 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 =
let rec aux l = function
| [] -> Some l
| x :: rest ->
(try ignore(List.find (fun y -> CS.E.compare Descr.compare x y = 0) l); aux l rest
with Not_found -> None)
in
if List.length l1 > List.length l2 then aux l1 l2 else aux l2 l1
end
exception Found of t * int * int * Tallying.CS.sl
......
......@@ -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 subsigma : CS.sl -> CS.sl -> CS.sl option
end
......
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