Commit a84b4fed authored by Julien Lopez's avatar Julien Lopez
Browse files

Better comp function

parent 72dc4f26
......@@ -85,28 +85,27 @@ let rec comp s1 s2 = match s1, s2 with
| Identity, _ -> s2
| _, Identity -> s1
| Comp(s3, s4), List(_) -> (match comp s4 s2 with
| Comp(_) -> Comp(s1, s2)
| res -> comp s3 res)
| List(_), Comp(s3, s4) | Sel(_), Comp(s3, s4) -> (match comp s1 s3 with
| Comp(_) -> Comp(s1, s2)
| res -> comp res s4)
| Comp(s3, s4), Comp(s5, s6) -> (match comp s4 s5 with
| Comp(_) -> Comp(s1, s2)
| res -> comp s3 (comp res s6))
(* If a variable in the image of s2 is in the domain of s1 we can't simplify *)
| _, _ when not (Var.Set.is_empty (Var.Set.inter (domain s1) (codomain s2)))
-> Comp(s1, s2)
| List(l1), List(l2) ->
| List(_), List(_) ->
if Var.Set.subset (domain s1) (domain s2) then s2 else Comp(s1, s2)
| Sel(_), List(_) ->
if Var.Set.subset (domain s1) (domain s2) then s2 else Comp(s1, s2)
(* If s1 is a Comp(s3, s4) and s2 a List(l), then if l has a subsigma in s3
or in s4 we return s1, else we return Comp(s1, s2) *)
| Comp(s3, s4), List(_) -> (match comp s3 s2 with
| Comp(_) as s5 when s3 != s5 -> (match comp s4 s2 with
| Comp(_) as s5 when s3 != s5 -> Comp(s1, s2)
| _ -> s1)
| _ -> s1)
(* Same case as above, but s1 is a List and s2 a Comp *)
| List(_), Comp(s3, s4) -> (match comp s3 s1 with
| Comp(_) as s5 when s3 != s5 -> (match comp s4 s1 with
| Comp(_) as s5 when s3 != s5 -> Comp(s1, s2)
| _ -> s2)
| _ -> s2)
(* Default: comp s1 s2 -> Comp(s1, s2). *)
(* To do? Do something else if s1 = Comp and s2 = Comp or if Sel *)
| _, _ -> Comp(s1, s2)
(* from intermediate explicitely typed language to Evaluation language (lambda) *)
......
......@@ -40,31 +40,31 @@ let rec codomain = function
let rec comp s1 s2 = match s1, s2 with
| Identity, _ -> s2
| _, Identity -> s1
| Mono, _ -> s2
| _, Mono -> s1
| Comp(s3, s4), List(_) -> (match comp s4 s2 with
| Comp(_) -> Comp(s1, s2)
| res -> comp s3 res)
| List(_), Comp(s3, s4) | Sel(_), Comp(s3, s4) -> (match comp s1 s3 with
| Comp(_) -> Comp(s1, s2)
| res -> comp res s4)
| Comp(s3, s4), Comp(s5, s6) -> (match comp s4 s5 with
| Comp(_) -> Comp(s1, s2)
| res -> comp s3 (comp res s6))
(* If a variable in the image of s2 is in the domain of s1 we can't simplify *)
| _, _ when not (Var.Set.is_empty (Var.Set.inter (domain s1) (codomain s2)))
-> Comp(s1, s2)
| List(l1), List(l2) ->
| List(_), List(_) ->
if Var.Set.subset (domain s1) (domain s2) then s2 else Comp(s1, s2)
| Sel(_), List(_) ->
if Var.Set.subset (domain s1) (domain s2) then s2 else Comp(s1, s2)
(* If s1 is a Comp(s3, s4) and s2 a List(l), then if l has a subsigma in s3
or in s4 we return s1, else we return Comp(s1, s2) *)
| Comp(s3, s4), List(_) -> (match comp s3 s2 with
| Comp(_) as s5 when s3 != s5 -> (match comp s4 s2 with
| Comp(_) as s5 when s3 != s5 -> Comp(s1, s2)
| _ -> s1)
| _ -> s1)
(* Same case as above, but s1 is a List and s2 a Comp *)
| List(_), Comp(s3, s4) -> (match comp s3 s1 with
| Comp(_) as s5 when s3 != s5 -> (match comp s4 s1 with
| Comp(_) as s5 when s3 != s5 -> Comp(s1, s2)
| _ -> s2)
| _ -> s2)
(* Default: comp s1 s2 -> Comp(s1, s2). *)
(* To do? Do something else if s1 = Comp and s2 = Comp or if Sel *)
| _, _ -> Comp(s1, s2)
(*
......
......@@ -503,8 +503,8 @@ let tests_eval = "CDuce runtime tests (Typed -> Lambda -> Value)" >:::
(run_test_eval "((((fun f x : 'A : 'A -> x)[{A/'B}])[{B/'A}])[{A/'B}])[{B/'A}]");
assert_equal ~msg:"Test CDuce.runtime.poly.multicomp.4 failed"
~printer:(fun x -> x) "Abstraction((`$A,`$A),Sel(1,(`$A -> `$A),Comp(Comp({ { `$B = Int
} },{ { `$A = Int } }),{ { `$A = `$B
~printer:(fun x -> x) "Abstraction((`$A,`$A),Sel(1,(`$A -> `$A),Comp({ { `$B = Int } },{ { `$A =
`$B
} })))"
(run_test_eval "(((((fun f x : 'A : 'A -> x)[{A/'B}])[{A/Int}])[{B/Int}])[{B/Int}])[{B/'A}]");
......
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