Skip to content

GitLab

C
cduce
Commit 18ae0d03 authored by Pietro Abate's avatar Pietro Abate
Browse files
Options

Fix apply rule in typer 

- refactoring in types.ml
- add Types.squareapply
- other fixes
parent fd4c762b
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 326 additions and 402 deletions
compile/compile.ml
View file @ 18ae0d03
......@@ -78,6 +78,9 @@ let fresharg =
let s = Printf.sprintf "__ARG%d" !count in
incr count;
(0,U.mk s)
(*
(Ns.Uri.mk (U.mk ""),U.mk s)
*)
;;
(* Comp for Lambda.sigma but simplify if possible. *)
......@@ -189,7 +192,6 @@ and compile_abstr env a =
let d = domain(env.sigma) in
Var.Set.is_empty (Var.Set.inter d vars)
in
let (slots,nb_slots,fun_env) =
(* we add a nameless empty slot for the argument *)
if is_mono then ([Dummy],1,fun_env)
......@@ -197,7 +199,6 @@ and compile_abstr env a =
let (x, y) = fresharg () in
([Dummy;Dummy],2,Env.add (Ns.Uri.from_int x, y) (Env 1) fun_env)
in
let (slots,nb_slots,fun_env) =
(* here De Bruijn indexes are reshuffled *)
List.fold_left
......@@ -215,7 +216,6 @@ and compile_abstr env a =
)
(slots,nb_slots,fun_env) (IdSet.get a.Typed.fun_fv)
in
let slots = Array.of_list (List.rev slots) in
let env =
{ env with vars = fun_env;
......@@ -224,18 +224,18 @@ and compile_abstr env a =
max_stack = ref 0 }
in
let body = compile_branches env a.Typed.fun_body in
let rec lift = function
|Sel(Env i, iface, s) -> Sel(Env (i+nb_slots),iface,lift s)
|Comp(s1,s2) -> Comp(lift s1,lift s2)
let rec lift n = function
|Sel(Env i, iface, s) -> Sel(Env (i+n),iface,lift n s)
|Comp(s1,s2) -> Comp(lift n s1,lift n s2)
|s -> s
in
if is_mono then
Abstraction(slots, a.Typed.fun_iface, body, !(env.max_stack))
else
let sigma = match env.sigma with
| Identity -> Identity
| _ -> Sel(Env 1,a.Typed.fun_iface,lift(env.sigma)) in
| _ -> Sel(Env 1,a.Typed.fun_iface,lift nb_slots (env.sigma))
in
PolyAbstraction(slots, a.Typed.fun_iface, body, !(env.max_stack), sigma)
and compile_branches env (brs : Typed.branches) =
......@@ -316,15 +316,17 @@ let eval ~run ~show (tenv,cenv,codes) e =
let run_show ~run ~show tenv cenv codes ids =
if run then
let () = Eval.eval_toplevel codes in
List.iter
(fun (id,_) -> show (Some id)
(Typer.find_value id tenv)
(Some (Eval.eval_var (find id cenv)))) ids
List.iter (fun (id,_) ->
show (Some id)
(Typer.find_value id tenv)
(Some (Eval.eval_var (find id cenv)))
) ids
else
List.iter
(fun (id,_) -> show (Some id)
(Typer.find_value id tenv)
None) ids
List.iter (fun (id,_) ->
show (Some id)
(Typer.find_value id tenv)
None
) ids
let let_decl ~run ~show (tenv,cenv,codes) p e =
let (tenv,decl,ids) = Typer.type_let_decl tenv p e in
......
test_arity6.ml deleted 100644 → 0
View file @ fd4c762b
let l = ["`$A0 -> Int" , ["(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> Int"] ;
"`$A0 -> `$A0" , ["(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> `$A1"] ;
"`$A0 -> (`$A0)" , ["(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> Int"] ;
"(`$A00 -> `$A0) -> Int" , ["`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> (`$A0 , `$A1 , `$A2 , `$A3 , `$A4)"] ;
"(`$A00 -> `$A0) -> `$A1" , ["(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> `$A1"] ;
"`$A0 -> `$A1 -> Int" , ["`$A0 -> `$A0" ;
"`$A0 -> `$A1 -> `$A2 -> (`$A0 , `$A1 , `$A2)"] ;
"`$A0 -> `$A1 -> `$A0" , ["`$A0 -> `$A0" ;
"(`$A00 -> `$A0) -> `$A1"] ;
"`$A0 -> `$A1 -> (`$A0 , `$A1)" , ["(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> `$A1" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A5 -> Int"] ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> Int" , ["`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> (`$A0 , `$A1 , `$A2 , `$A3 , `$A4)" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> `$A1"] ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> `$A1" , ["(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> (`$A55 -> `$A5) -> `$A1" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A0"] ;
"`$A0 -> `$A1 -> `$A2 -> Int" , ["`$A0 -> `$A1 -> `$A2 -> Int" ;
"`$A0 -> `$A1 -> `$A2 -> `$A0" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A5 -> `$A0"] ;
"`$A0 -> `$A1 -> `$A2 -> `$A0" , ["`$A0 -> `$A1 -> `$A2 -> (`$A0 , `$A1 , `$A2)" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A5 -> `$A0" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> `$A1"] ;
"`$A0 -> `$A1 -> `$A2 -> (`$A0 , `$A1 , `$A2)" , ["(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> (`$A55 -> `$A5) -> `$A1" ;
"`$A0 -> `$A1 -> `$A2 -> (`$A0 , `$A1 , `$A2)" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> (`$A55 -> `$A5) -> Int"] ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> Int" , ["(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> (`$A55 -> `$A5) -> Int" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A5 -> Int" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> (`$A55 -> `$A5) -> `$A1"] ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> `$A1" , ["`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A5 -> (`$A0 , `$A1 , `$A2 , `$A3 , `$A4 , `$A5)" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> (`$A55 -> `$A5) -> Int" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> Int"] ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> Int" , ["`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A0" ;
"`$A0 -> `$A1 -> Int" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> (`$A0 , `$A1 , `$A2 , `$A3 , `$A4)" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> Int"] ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A0" , ["(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> (`$A55 -> `$A5) -> Int" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> Int" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> Int" ;
"(`$A00 -> `$A0) -> `$A1"] ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> (`$A0 , `$A1 , `$A2 , `$A3)" , ["`$A0 -> `$A1 -> Int" ;
"(`$A00 -> `$A0) -> `$A1" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> (`$A0 , `$A1 , `$A2 , `$A3)" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> (`$A0 , `$A1 , `$A2 , `$A3)"] ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> Int" , ["(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> `$A1" ;
"`$A0 -> `$A1 -> (`$A0 , `$A1)" ;
"`$A0 -> `$A1 -> (`$A0 , `$A1)" ;
"`$A0 -> `$A1 -> `$A0"] ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> `$A1" , ["`$A0 -> Int" ;
"`$A0 -> `$A1 -> `$A2 -> `$A0" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> Int" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> `$A2 -> Int"] ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> Int" , ["(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> (`$A55 -> `$A5) -> Int" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A0" ;
"`$A0 -> `$A1 -> `$A0" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> `$A1" ;
"`$A0 -> `$A1 -> `$A2 -> (`$A0 , `$A1 , `$A2)"] ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A0" , ["(`$A00 -> `$A0) -> `$A1" ;
"`$A0 -> (`$A0)" ;
"`$A0 -> `$A1 -> `$A0" ;
"`$A0 -> `$A1 -> `$A0" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> Int"] ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> (`$A0 , `$A1 , `$A2 , `$A3 , `$A4)" , ["(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> `$A1" ;
"`$A0 -> `$A1 -> `$A2 -> Int" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> Int" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> (`$A0 , `$A1 , `$A2 , `$A3)" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> (`$A55 -> `$A5) -> `$A1"] ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> Int" , ["`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A5 -> `$A0" ;
"(`$A00 -> `$A0) -> `$A1" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A5 -> `$A0" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> (`$A55 -> `$A5) -> `$A1" ;
"(`$A00 -> `$A0) -> Int"] ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> `$A1" , ["(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> `$A1" ;
"`$A0 -> (`$A0)" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A0" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> Int" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> Int"] ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A5 -> Int" , ["`$A0 -> Int" ;
"`$A0 -> `$A1 -> Int" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> Int" ;
"`$A0 -> `$A1 -> `$A2 -> `$A0" ;
"`$A0 -> `$A1 -> (`$A0 , `$A1)" ;
"`$A0 -> Int"] ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A5 -> `$A0" , ["(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> (`$A55 -> `$A5) -> `$A1" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A5 -> (`$A0 , `$A1 , `$A2 , `$A3 , `$A4 , `$A5)" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> (`$A0 , `$A1 , `$A2 , `$A3)" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> (`$A0 , `$A1 , `$A2 , `$A3)" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> Int" ;
"`$A0 -> `$A1 -> `$A2 -> Int"] ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A5 -> (`$A0 , `$A1 , `$A2 , `$A3 , `$A4 , `$A5)" , ["`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A5 -> `$A0" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> Int" ;
"`$A0 -> (`$A0)" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A5 -> (`$A0 , `$A1 , `$A2 , `$A3 , `$A4 , `$A5)" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A0" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> Int"] ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> (`$A55 -> `$A5) -> Int" , ["(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> `$A1" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> Int" ;
"`$A0 -> `$A1 -> Int" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> `$A5 -> `$A0" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> Int" ;
"`$A0 -> `$A1 -> `$A2 -> `$A3 -> `$A4 -> (`$A0 , `$A1 , `$A2 , `$A3 , `$A4)"] ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> (`$A55 -> `$A5) -> `$A1" , ["`$A0 -> Int" ;
"`$A0 -> `$A0" ;
"`$A0 -> `$A1 -> Int" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> `$A1" ;
"(`$A00 -> `$A0) -> `$A1" ;
"(`$A00 -> `$A0) -> (`$A11 -> `$A1) -> (`$A22 -> `$A2) -> (`$A33 -> `$A3) -> (`$A44 -> `$A4) -> `$A1"]]
tests/libtest/tallyingTest.ml
View file @ 18ae0d03
......@@ -185,6 +185,14 @@ let norm_tests () = [
[P(V "A","Int");P(V "B","Bool")]
];
"{a=(`$A , `$B)}","{a=(Int , Bool)}", mk_s [
[P(V "A","Empty")];
[P(V "B","Empty")];
[P(V "A","Int");P(V "B","Bool")]
];
"{a=(Int , Bool)}","{a=(`$A , `$B)}", mk_s [ [N("Int", V "A");N("Bool", V "B")] ];
"(Int , Bool)","(`$A , `$B)", mk_s [ [N("Int", V "A");N("Bool", V "B")] ];
"(Bool , Bool)","(`$A , `$B)", mk_s [ [N("Bool", V "A");N("Bool", V "B")] ];
......@@ -315,7 +323,11 @@ let tallying_tests = [
[("{a=Int}","Any")], [[]];
[("{a=`$A}","Any")], [[]];
[("{a=Int}","{a=(Int|Bool)}")], [[]];
(*
[("{a=Bool -> Bool}","{b=Int -> `$A}")], [[]];
[("{a=(Int -> Int) | (Bool -> Bool)}","{b=(`$A -> `$B)}")], [[]];
[("{a=Int} -> Int", "{a=`$A} -> `$A")], [[]];
*)
]
(* to test tallying { sigma_i } -- > for all i => s sigma_i <= t sigma_i *)
......@@ -339,10 +351,6 @@ let test_tallying =
) (Types.subtype s_sigma t_sigma) true
) sigma
) l
(*
let elem s = SubStSet.of_list (List.map (fun l -> ESet.of_list l) s) in
SubStSet.assert_equal (elem expected) (elem result)
*)
with Tallying.Step1Fail -> assert_equal expected []
)
) tallying_tests
......@@ -458,7 +466,7 @@ let test_apply =
(print_test msg s t) >:: (fun _ ->
try
let (s,t) = (parse_typ s,parse_typ t) in
let (sl,s,t,g) = Types.apply_raw s t in
let (sl,s,t,g) = Types.apply_raw Var.Set.empty s t in
let gamma = Types.cons (Types.var (Var.mk "Gamma")) in
......
tests/libtest/typesTest.ml
View file @ 18ae0d03
......@@ -130,6 +130,7 @@ let test_set_operations =
;;
let squaresubtype_tests = [
"`$A -> `$A", "Bool -> Bool", [], true;
"`$A -> `$B", "Int -> Bool", [], true;
"`$A -> `$B", "Int -> Bool", ["A"], false;
"`$A -> `$A", "(Int -> Int) & (Bool -> Bool)", [], true;
......@@ -200,7 +201,6 @@ let test_rec_subtitutions =
) rec_subst_tests
;;
let subtype_tests = [
"Int" , "Any", true;
"`A | Int" , "`A", false;
......@@ -221,6 +221,10 @@ let subtype_tests = [
"0--*" , "Int", true;
"1--5" , "1--*", true;
"1--5" , "1--5", true;
"3" , "Int", true;
"Int" , "0--*", false ;
"1--5" , "1--4", false ;
"Int" , "0--*", false ;
"Any -> `A" , "Any", true;
......@@ -244,12 +248,10 @@ let subtype_tests = [
"Any -> `A" , "Any -> Empty", false ;
"`A -> `B" , "`A -> `C", false ;
"Int" , "0--*", false ;
"1--5" , "1--4", false ;
"Int" , "0--*", false ;
"Int -> Int", "Empty -> Any", true;
"Any", "Any \\ Char", false;
(* polymorphic cduce extension *)
"`$X" , "Any", true;
......@@ -257,7 +259,6 @@ let subtype_tests = [
"Any", "`$X | (Any \\ `$X)", true;
"Any", "(42 & `$X) | (Any \\ (42 & `$X))", true;
"Any", "(41 & `$X) | (Any \\ (42 & `$X))", false;
"Any", "Any \\ Char", false;
"(`$A -> Bool, `$B -> `$B)", "(Int | Bool -> Int, `$A -> `$B)", false;
(* ({ (int , true) } , { }) *)
"Int -> Int", "`$A -> `$A", false;
......
types/types.ml
View file @ 18ae0d03
This diff is collapsed.
types/types.mli
View file @ 18ae0d03
......@@ -250,13 +250,13 @@ module Arrow : sig
val sample: t -> t
(** [check_strenghten t s]
Assume that [t] is an intersection of arrow types
representing the interface of an abstraction;
check that this abstraction has type [s] (otherwise raise Not_found)
and returns a refined type for this abstraction.
*)
val check_strenghten: t -> t -> t
(* [check_strenghten t s]
Assume that [t] is an intersection of arrow types
representing the interface of an abstraction;
check that this abstraction has type [s] (otherwise raise Not_found)
and returns a refined type for this abstraction.
*)
val check_iface: (t * t) list -> t -> bool
......@@ -266,16 +266,18 @@ module Arrow : sig
(* Always succeed; no check <= Arrow.any *)
val domain: t -> descr
(* Always succeed; no check on the domain *)
val apply: t -> descr -> descr
(* Always succeed; no check on the domain *)
(** True if the type of the argument is needed to obtain
the type of the result (must use [apply]; otherwise,
[apply_noarg] is enough *)
val need_arg : t -> bool
(* True if the type of the argument is needed to obtain
the type of the result (must use [apply]; otherwise,
[apply_noarg] is enough *)
val apply_noarg : t -> descr
end
end
module Int : sig
val has_int : t -> Intervals.V.t -> bool
......@@ -316,7 +318,6 @@ val cond_partition: t -> (t * t) list -> t list
The result is a partition of the first argument which is precise enough
to answer all the questions. *)
module Print :
sig
val register_global : string -> Ns.QName.t -> t -> unit
......@@ -442,17 +443,18 @@ module Tallying : sig
end
val apply : t -> t -> Tallying.CS.sl
(** Square Subtype relation. [squaresubtype delta s t] .
True if there exists a substitution such that s < t only
considering variables that are not in delta *)
val squaresubtype : Var.Set.t -> t -> t -> (Tallying.CS.sl * bool)
val apply_full : t -> t -> t
(** apply_raw s t returns the 4-tuple (subst,ss, tt, res) where
subst is the set of substitution that make the application succeed,
ss and tt are the expansions of s and t corresponding to that substitution
and res is the type of the result of the application
*)
val apply_raw : t -> t -> Tallying.CS.sl * t * t * t
and res is the type of the result of the application *)
val apply_full : Var.Set.t -> t -> t -> t
val apply_raw : Var.Set.t -> t -> t -> Tallying.CS.sl * t * t * t
val squareapply : Var.Set.t -> t -> t -> (Tallying.CS.sl * t)
(** Square Subtype relation. [squaresubtype s t delta sl] .
True if there exists a substitution in sl such that s < t only
considering variables that are not in delta *)
val squaresubtype : Var.Set.t -> t -> t -> (Tallying.CS.sl * bool)
typing/typed.ml
View file @ 18ae0d03
......@@ -114,8 +114,7 @@ module Print = struct
| Types.Atom(a) -> Format.fprintf ppf "Atom(%s)" (Atoms.V.to_string a)
| Types.Char(c) -> Format.fprintf ppf "Char(%d)" (Chars.V.to_int c)
| Types.Pair(c1, c2) -> Format.fprintf ppf "(%a,%a)" pp_const c1 pp_const c2
| Types.String(_, _, s, _) ->
Format.fprintf ppf "\"%s\"" (Encodings.Utf8.to_string s)
| Types.String(_, _, s, _) -> Format.fprintf ppf "\"%s\"" (Encodings.Utf8.to_string s)
| _ -> assert false
let rec pp_typed ppf e =
......
typing/typer.ml
View file @ 18ae0d03
......@@ -113,7 +113,6 @@ let empty_env = {
let enter_id x i env =
{ env with ids = Env.add x i env.ids }
let type_using env loc x cu =
try
let cu = !load_comp_unit cu in
......@@ -182,14 +181,12 @@ let rec const env loc = function
(* I. Transform the abstract syntax of types and patterns into
the internal form *)
let find_schema_component sch name =
try ESchemaComponent (Env.find name sch.sch_comps)
with Not_found ->
raise (Error (Printf.sprintf "No component named '%s' found in schema '%s'"
(Ns.QName.to_string name) sch.sch_uri))
let navig loc env0 (env,comp) id =
match comp with
| ECDuce cu ->
......@@ -217,7 +214,6 @@ let navig loc env0 (env,comp) id =
| _ -> error loc "Invalid dot access"
*)
let rec find_global env loc ids =
match ids with
| id::rest ->
......@@ -822,9 +818,14 @@ let require loc t s =
if not (Types.subtype t s) then raise_loc loc (Constraint (t, s))
let verify loc t s =
require loc t s;
require loc t s;
t
let squareverify loc delta t s =
if not (snd(Types.squaresubtype delta t s)) then
raise_loc loc (Constraint (t, s));
t
let verify_noloc t s =
if not (Types.subtype t s) then raise (Constraint (t, s));
t
......@@ -874,8 +875,11 @@ and type_check' loc env ed constr precise = match ed with
| Abstraction a ->
let t =
try Types.Arrow.check_strenghten a.fun_typ constr
with Not_found ->
(* try Types.Arrow.check_strenghten a.fun_typ constr *)
try begin
if snd(Types.squaresubtype env.delta a.fun_typ constr) then a.fun_typ
else raise Not_found
end with Not_found ->
should_have loc constr
"but the interface of the abstraction is not compatible"
in
......@@ -942,20 +946,45 @@ and type_check' loc env ed constr precise = match ed with
(ed,localize loc (flatten (type_map loc env true e b) constr) precise)
| Apply (e1,e2) ->
let t1_t = type_check env e1 Types.Arrow.any true in
let t1 = type_check env e1 Types.any true in
let t2 = type_check env e2 Types.any true in
let (sl,res) =
(* t [_delta 0 -> 1 *)
(* s [_delta dom(t) *)
try Types.squareapply env.delta t1 t2
with Types.Tallying.UnSatConstr _ ->
raise_loc loc (Constraint (Types.Arrow.domain(Types.Arrow.get t1),t2))
in
(Apply(e1,e2),verify loc res constr)
(*
let (sJ,is_subtype) = Types.squaresubtype env.delta t1_t Types.Arrow.any in
if not is_subtype then raise_loc loc (Constraint (t, s));
Format.printf "Apply e1 ->>%a\n\n" Typed.Print.pp_typed e1;
let t1 = Types.Arrow.get t1_t in
let dom = Types.Arrow.domain t1 in
let res =
let sI,res =
if Types.Arrow.need_arg t1 then
let t2 = type_check env e2 dom true in
Types.Arrow.apply t1 t2
let (sl,is_subtype) = Types.squaresubtype env.delta t2 dom in
if not is_subtype then raise_loc loc (Constraint (t, s));
Format.printf "Apply e2 ->>%a\n\n" Typed.Print.pp_typed e2;
Types.apply_full env.delta t1_t t2
else begin
ignore (type_check env e2 dom false);
(* s [_delta dom(t) *)
let t2 = type_check env e2 dom false in
let (sl,is_subtype) = Types.squaresubtype env.delta t2 dom in
if not is_subtype then raise_loc loc (Constraint (t, s));
(* ignore (type_check env e2 dom false); *)
Format.printf "Apply e2 ->>%a\n\n" Typed.Print.pp_typed e2;
Types.Arrow.apply_noarg t1
end
in
(ed,verify loc res constr)
(Apply(Subst(e1,sJ),Subst(e2,sI)),verify loc res constr)
*)
| Var s ->
(ed,verify loc (find_value s env) constr)
......
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