Typer
Discussions par mois
- ----- 2026 -----
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2025 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2024 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2023 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2022 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2021 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2020 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2019 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2018 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2017 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2016 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
Juin 2016
- 5 participants
- 23 discussions
[Git][monnier/typer][unification] 3 commits: debug recursion on wrong lexp in _unify_call
by BONNEVALLE Vincent 30 Jui '16
by BONNEVALLE Vincent 30 Jui '16
30 Jui '16
BONNEVALLE Vincent pushed to branch unification at Stefan / Typer
Commits:
1fbfe683 by n3f4s at 2016-06-30T22:24:57+02:00
debug recursion on wrong lexp in _unify_call
- - - - -
3f93815b by n3f4s at 2016-06-30T22:26:01+02:00
better printing for debugging & test
- - - - -
c520b3e9 by n3f4s at 2016-06-30T22:26:16+02:00
add test case
- - - - -
4 changed files:
- src/debug_fun.ml
- src/fmt_lexp.ml
- src/unification.ml
- tests/unify_test.ml
Changes:
=====================================
src/debug_fun.ml
=====================================
--- a/src/debug_fun.ml
+++ b/src/debug_fun.ml
@@ -1,7 +1,8 @@
open Fmt_lexp
-let _debug = true
+(*let _debug = true*)
+let _debug = false
let logs = ref []
@@ -22,6 +23,7 @@ let clear_indent () =
indent := !indent + 1;
) (!logs);
logs := [];
+ print_newline ();
())
let debug_print_lexp lxp =
=====================================
src/fmt_lexp.ml
=====================================
--- a/src/fmt_lexp.ml
+++ b/src/fmt_lexp.ml
@@ -21,7 +21,7 @@ let rec string_of_lxp lxp =
| Let (_) -> "Let(..)"
| Var ((_, name), idx) -> "Var(" ^ name ^ ", #" ^(string_of_int idx) ^ ")"
| Arrow (_, _, a, _, b) -> "Arrow(" ^ (string_of_lxp a) ^ " => " ^ (string_of_lxp b) ^ ")"
- | Lambda (_,(_, name), dcl, body) -> "Lambda(" ^ name ^ " : " ^ (string_of_lxp dcl) ^ " => (" ^ (string_of_lxp body) ^ ") )"
+ | Lambda (_,(_, name), dcl, body) -> "Lambda(" ^ name ^ ": " ^ (string_of_lxp dcl) ^ " => (" ^ (string_of_lxp body) ^ "))"
| Metavar (value, (_, name)) -> "Metavar(" ^ (string_of_int value) ^ ", " ^ name ^ ")"
| Call (_) -> "Call(...)"
| Inductive _ -> ("Inductive") ^ "(...)"
=====================================
src/unification.ml
=====================================
--- a/src/unification.ml
+++ b/src/unification.ml
@@ -252,10 +252,13 @@ and _unify_call (call: lexp) (lxp: lexp) (subst: substitution) : return_type =
| None -> None
| Some tail -> _unify_inner ((lxp1, lxp2)::(tail)) subst)
in
- match (call, lxp) with
- | (Call (lxp1, lxp_list1), Call (lxp2, lxp_list2)) -> try_zip_fold lxp_list1 lxp_list2 lxp lxp2 subst
+ let tmp = match (call, lxp) with
+ | (Call (lxp_left, lxp_list1), Call (lxp_right, lxp_list2)) -> try_zip_fold lxp_list1 lxp_list2 lxp_left lxp_right subst
| (Call _, _) -> Some ((subst, [(call, lxp)]))
| (_, _) -> None
+ in match tmp with
+ | None -> Debug_fun.debug_print_unify "_unify_call" call lxp " -> unification failed"; tmp
+ | Some _ -> Debug_fun.debug_print_unify "_unify_call" call lxp " -> unification success"; tmp
(** Apply unsusp to the Susp and unify the result with the lexp
*)
@@ -416,12 +419,19 @@ and _unify_inner (lxp_l: (lexp * lexp) list) (subst: substitution) : return_type
(lxp_list: (lexp * lexp) list) : return_type =
match _unify_inner lxp_list s with
(*| None -> Some (s, c)*)
- | None -> Debug_fun.debug_print "_unify_inner.merge" "unification failed"; None
- | Some (s_,c_) -> Debug_fun.debug_print "_unify_inner.merge" "unification success"; Some (s_, c@c_)
+ | None -> None
+ | Some (s_,c_) -> Some (s_, c@c_)
in
- match lxp_l with
+ let tmp = match lxp_l with
| (lxp1, lxp2)::tail -> ( match unify lxp1 lxp2 subst with
| Some (s, c) -> merge (s, c) tail
- | None -> Debug_fun.debug_print "_unify_inner" "unification failed"; None)
- | [] -> Debug_fun.debug_print "_unify_inner" "unification success : list empty"; Some (subst, [])
+ | None -> None)
+ | [] -> Some (subst, [])
+ in match tmp with
+ | None -> ( match lxp_l with
+ | [] -> Debug_fun.debug_print "_unify_inner" " -> list empty"; tmp
+ | (l1, l2)::_ -> Debug_fun.debug_print_unify "_unify_inner" l1 l2 " -> unification failed"; tmp )
+ | Some _ -> ( match lxp_l with
+ | [] -> Debug_fun.debug_print "_unify_inner" " -> list empty"; tmp
+ | (l1, l2)::_ -> Debug_fun.debug_print_unify "_unify_inner" l1 l2 " -> unification success"; tmp )
=====================================
tests/unify_test.ml
=====================================
--- a/tests/unify_test.ml
+++ b/tests/unify_test.ml
@@ -50,11 +50,11 @@ let fmt (lst: (lexp * lexp * result * result) list): string list =
lst
in let l, c1, c2, r = max_dim str_lst
in List.map (fun (l1, l2, r1, r2) -> (padding_right l1 l ' ')
- ^ " , "
+ ^ ","
^ (padding_right l2 c1 ' ')
- ^ " -> got : "
+ ^ "-> got: "
^ (padding_right r2 r ' ')
- ^ " expected : "
+ ^ "expected: "
^ (padding_right r1 c2 ' ')
) str_lst
@@ -70,6 +70,10 @@ let str_case2 = "i = case 0
| 0 => 12
| _ => 12"
let str_let = "i = let a = 5 in a + 1"
+let str_let2 = "j = let b = 5 in b"
+let str_lambda = "sqr = lambda (x : Int) -> x * x;"
+let str_lambda2 = "sqr = lambda (x : Int) -> x * x;"
+let str_lambda3 = "sqr = lambda (x : Int) -> lambda (y : Int) -> x * y;"
let generate_ltype_from_str str =
List.hd ((fun (lst, _) ->
@@ -85,22 +89,25 @@ let generate_lexp_from_str str =
(List.flatten lst))
(lexp_decl_str str default_lctx))
-let input_induct = generate_lexp_from_str str_induct
-let input_int_4 = generate_lexp_from_str str_int_4
-let input_int_3 = generate_lexp_from_str str_int_3
-let input_case = generate_lexp_from_str str_case
-let input_case2 = generate_lexp_from_str str_case2
-let input_let = generate_lexp_from_str str_let
+let input_induct = generate_lexp_from_str str_induct
+let input_int_4 = generate_lexp_from_str str_int_4
+let input_int_3 = generate_lexp_from_str str_int_3
+let input_case = generate_lexp_from_str str_case
+let input_case2 = generate_lexp_from_str str_case2
+let input_let = generate_lexp_from_str str_let
+let input_let2 = generate_lexp_from_str str_let
+let input_lambda = generate_lexp_from_str str_lambda
+let input_lambda2 = generate_lexp_from_str str_lambda2
+let input_lambda3 = generate_lexp_from_str str_lambda3
let generate_testable (_: lexp list) : ((lexp * lexp * result) list) =
- ( Builtin ((Util.dummy_location, "Int=3"), Imm (Integer (Util.dummy_location, 3))),
- Imm (Integer (Util.dummy_location, 3)), Equivalent)
-
- ::( Var ((Util.dummy_location, "x"), 3),
- Var ((Util.dummy_location, "y"), 4), Nothing )
-
- ::( Var ((Util.dummy_location, "x"), 3),
- Metavar (0, (Util.dummy_location, "M")), Unification )
+ (input_induct , input_induct , Equivalent)
+ ::(input_int_4 , input_int_4 , Equivalent)
+ ::(input_int_3 , input_int_4 , Nothing)
+ ::(input_case , input_int_4 , Constraint)
+ ::(input_case , input_induct , Constraint)
+ ::(input_case , input_case , Equivalent)
+ ::(input_case , input_case2 , Nothing)
::( Lambda ((Aexplicit),
(Util.dummy_location, "L1"),
@@ -111,58 +118,42 @@ let generate_testable (_: lexp list) : ((lexp * lexp * result) list) =
Var((Util.dummy_location, "z"), 4),
Imm (Integer (Util.dummy_location, 3))), Unification )
- ::( Cons (((Util.dummy_location, "Cons"), 3), (Util.dummy_location, "Cons")) ,
- Imm (Integer (Util.dummy_location, 3)) , Nothing )
-
- ::( Cons (((Util.dummy_location, "Cons"), 3), (Util.dummy_location, "Cons")) ,
- Imm (Integer (Util.dummy_location, 3)), Nothing)
-
- ::( Cons (((Util.dummy_location, "Cons"), 3), (Util.dummy_location, "Cons")) ,
- Var ((Util.dummy_location, "y"), 4), Nothing )
-
- ::( Cons (((Util.dummy_location, "Cons"), 3), (Util.dummy_location, "Cons")) ,
- Metavar (0, (Util.dummy_location, "M")), Unification )
-
- ::( Cons (((Util.dummy_location, "Cons"), 3), (Util.dummy_location, "Cons")) ,
- Lambda ((Aexplicit),
- (Util.dummy_location, "L2"),
- Var((Util.dummy_location, "z"), 4),
- Imm (Integer (Util.dummy_location, 3))), Nothing )
-
- ::(input_induct , input_induct , Equivalent)
-
- ::(input_int_4 , input_int_4 , Equivalent)
-
- ::(input_int_3 , input_int_4 , Nothing)
-
- ::(input_case , input_int_4 , Constraint)
- ::(input_case , input_induct , Constraint)
- ::(input_case , input_case , Equivalent)
- ::(input_case , input_case2 , Nothing)
-
- ::(input_let , input_induct , Constraint)
- ::(input_let , input_int_4 , Constraint)
- ::(input_let , input_case , Constraint)
- ::(input_let , input_let , Equivalent)
+ ::(input_let , input_induct , Constraint)
+ ::(input_let , input_int_4 , Constraint)
+ ::(input_let , input_case , Constraint)
+ ::(input_let , input_let , Equivalent)
+ ::(input_let2 , input_let , Equivalent)
+ ::(input_let2 , input_let2 , Equivalent)
+
+ ::(input_lambda , input_int_4 , Nothing)
+ ::(input_lambda , input_induct , Nothing)
+ ::(input_lambda , input_case , Constraint)
+ ::(input_lambda , input_case2 , Constraint)
+ ::(input_lambda , input_let , Constraint)
+ ::(input_lambda , input_induct , Nothing)
+ ::(input_lambda , input_lambda , Equivalent)
+
+ ::(input_lambda2 , input_int_4 , Nothing)
+ ::(input_lambda2 , input_induct , Nothing)
+ ::(input_lambda2 , input_case , Constraint)
+ ::(input_lambda2 , input_case2 , Constraint)
+ ::(input_lambda2 , input_let , Constraint)
+ ::(input_lambda2 , input_induct , Nothing)
+ ::(input_lambda2 , input_lambda , Equivalent)
+ ::(input_lambda2 , input_lambda2 , Equivalent)
+ ::(input_lambda2 , input_lambda3 , Constraint)
+ ::(input_lambda3 , input_lambda3 , Equivalent)
- ::(Let (Util.dummy_location,
- [], (*TODO : better tests*)
- Var ((Util.dummy_location, "x_let"), 9)) ,
- Lambda ((Aexplicit),
- (Util.dummy_location, "L2"),
- Var((Util.dummy_location, "z"), 4),
- Imm (Integer (Util.dummy_location, 3))), Constraint )
::[]
let test_input (lxp1: lexp) (lxp2: lexp) (subst: substitution): unif_res =
- (*do_debug (fun () -> print_string (fmt_unification_of lxp1 lxp2));*)
- clear_indent ();
let res = unify lxp1 lxp2 subst in
- match res with
+ let tmp = match res with
| Some (s, []) when s = empty_subst -> (Equivalent, res, lxp1, lxp2)
| Some (_, []) -> (Unification, res, lxp1, lxp2)
| Some _ -> (Constraint, res, lxp1, lxp2)
| None -> (Nothing, res, lxp1, lxp2)
+ in clear_indent (); tmp
let check (lxp1: lexp ) (lxp2: lexp ) (res: result) (subst: substitution ): bool =
let r, _, _, _ = test_input lxp1 lxp2 subst
@@ -181,10 +172,12 @@ let unifications = List.map
in (l1, l2, res, r))
(generate_testable [])
+let idx = ref 0
let _ = List.map
(fun (str, (l1, l2, expected, res)) ->
+ idx := !idx + 1;
add_test "UNIFICATION"
- (str)
+ ((if !idx < 10 then "0" else "") ^ (string_of_int !idx) ^ " " ^ str )
(fun () -> if expected = res then success () else failure ()))
(List.combine (fmt unifications) unifications )
View it on GitLab: https://gitlab.com/monnier/typer/compare/239ce52674b8835de01bc1836510f70cee…
1
0
[Git][monnier/typer][unification] 2 commits: improved debug logging
by BONNEVALLE Vincent 30 Jui '16
by BONNEVALLE Vincent 30 Jui '16
30 Jui '16
BONNEVALLE Vincent pushed to branch unification at Stefan / Typer
Commits:
9245f2c3 by n3f4s at 2016-06-30T17:54:13+02:00
improved debug logging
- - - - -
239ce526 by n3f4s at 2016-06-30T17:57:21+02:00
refactoring : extract function
extract inner match into function to avoid "arrow pattern" with multiple
level of match
- - - - -
2 changed files:
- src/debug_fun.ml
- src/unification.ml
Changes:
=====================================
src/debug_fun.ml
=====================================
--- a/src/debug_fun.ml
+++ b/src/debug_fun.ml
@@ -1,21 +1,28 @@
open Fmt_lexp
-let _debug = false
+let _debug = true
-let indent = ref 0
+let logs = ref []
let do_debug func =
if _debug then (func ()) else ()
-let debug_print str =
- do_debug (fun () -> print_string str; print_newline (); ())
+let debug_print str1 str2 =
+ logs := ((padding_left str1 20 ' ')^" : ", (str2^"\n"))::(!logs); ()
let clear_indent () =
- do_debug (fun () -> indent := 0; ())
-
-let unindent () =
- do_debug (fun () -> indent := (max 0 (!indent - 1)); ())
+ let indent = ref 0
+ in
+ do_debug (fun () ->
+ List.iter (fun (s1, s2) ->
+ print_string s1;
+ print_string (String.make (!indent * 2) '-');
+ print_string s2;
+ indent := !indent + 1;
+ ) (!logs);
+ logs := [];
+ ())
let debug_print_lexp lxp =
let str = colored_string_of_lxp lxp str_yellow str_magenta
@@ -23,13 +30,12 @@ let debug_print_lexp lxp =
let debug_print_unify fn lhs rhs str =
let debug_print_unify fn lhs rhs str =
- print_string (padding_left fn 10 ' ');
- print_string " : ";
- print_string (String.make (!indent * 4) '-');
- debug_print_lexp lhs;
- print_string " , ";
- debug_print_lexp rhs;
- print_string str;
- indent := !indent + 1;
- print_newline ();
+ let tmp = ((padding_left fn 20 ' ') ^ " : ",
+ (colored_string_of_lxp lhs str_yellow str_magenta)
+ ^ " , "
+ ^ colored_string_of_lxp rhs str_yellow str_magenta
+ ^ str ^ "\n")
+ in
+ logs := tmp::(!logs);
in do_debug (fun () -> debug_print_unify fn lhs rhs str; ())
+
=====================================
src/unification.ml
=====================================
--- a/src/unification.ml
+++ b/src/unification.ml
@@ -48,7 +48,7 @@ let zip_map (l1: 'a list ) (l2: 'b list ) (f: ('a -> 'b -> 'c)): 'c list option
match ll1, ll2 with
| (h1::t1, h2::t2) -> (f h1 h2)::(zip_ t1 t2 f)
| ([], []) -> []
- | _, _ -> []
+ | _, _ -> [] (* Should never happen since we check length before actually calling the recursion but without this case, the compiler complains*)
in if List.length l1 = List.length l2 then Some (zip_ l1 l2 f) else None
let zip (l1: 'a list) (l2: 'b list): (('a * 'b) list option) = zip_map l1 l2 (fun x z -> (x, z))
@@ -74,26 +74,26 @@ let zip_fold list1 list2 f =
*)
let rec unify (l: lexp) (r: lexp) (subst: substitution) : return_type =
let tmp = match (l, r) with
- | (_, Metavar _) -> _unify_metavar r l subst
- | (_, Call _) -> _unify_call r l subst
- | (_, Case _) -> _unify_case r l subst
- | (_, Susp _) -> _unify_susp r l subst
- | (_, Let _) -> _unify_let r l subst
- | (Imm _, _) -> _unify_imm l r subst
- | (Cons _, _) -> _unify_cons l r subst
- | (Builtin _, _) -> _unify_builtin l r subst
- | (Let _, _) -> _unify_let l r subst
- | (Var _, _) -> _unify_var l r subst
- | (Arrow _, _) -> _unify_arrow l r subst
- | (Lambda _, _) -> _unify_lambda l r subst
- | (Metavar _, _) -> _unify_metavar l r subst
- | (Call _, _) -> _unify_call l r subst
- | (Susp _, _) -> _unify_susp l r subst
- | (Case _, _) -> _unify_case l r subst
- | (Inductive _, _) -> _unfiy_induct l r subst
- | (Sort _, _) -> _unify_sort l r subst
- | (SortLevel _, _) -> _unify_sortlvl l r subst
-(* | (_, _) -> None*)
+ | (_, Metavar _) -> _unify_metavar r l subst
+ | (_, Call _) -> _unify_call r l subst
+ | (_, Case _) -> _unify_case r l subst
+ | (_, Susp _) -> _unify_susp r l subst
+ | (_, Let _) -> _unify_let r l subst
+ | (Imm _, _) -> _unify_imm l r subst
+ | (Cons _, _) -> _unify_cons l r subst
+ | (Builtin _, _) -> _unify_builtin l r subst
+ | (Let _, _) -> _unify_let l r subst
+ | (Var _, _) -> _unify_var l r subst
+ | (Arrow _, _) -> _unify_arrow l r subst
+ | (Lambda _, _) -> _unify_lambda l r subst
+ | (Metavar _, _) -> _unify_metavar l r subst
+ | (Call _, _) -> _unify_call l r subst
+ | (Susp _, _) -> _unify_susp l r subst
+ | (Case _, _) -> _unify_case l r subst
+ | (Inductive _, _) -> _unfiy_induct l r subst
+ | (Sort _, _) -> _unify_sort l r subst
+ | (SortLevel _, _) -> _unify_sortlvl l r subst
+ (* | (_, _) -> None*)
in match tmp with
| Some _ -> Debug_fun.debug_print_unify "unify" l r " -> unification success"; tmp
| None -> Debug_fun.debug_print_unify "unify" l r " -> unification failed"; tmp
@@ -124,13 +124,14 @@ and _unify_imm (l: lexp) (r: lexp) (subst: substitution) : return_type =
* Cons, Cons -> if Cons ~= Cons then OK else ERROR
* Cons, _ -> ERROR
*)
+(*FIXME which parameter of Cons is it's name ?*)
+(* symbol = (location * string)*)
+(*TODO in index comparison : shift indexes ?*)
and _unify_cons (cons: lexp) (lxp: lexp) (subst: substitution) : return_type =
- (* symbol = (location * string)*)
match (cons, lxp) with
- (*FIXME which parameter of Cons is it's name ?*)
| (Cons ((_, idx), (_, name)),
Cons ((_, idx2), (_, name2))) when name = name2 ->
- if idx = idx2 then Some (subst, []) (*TODO shift indexes ?*)
+ if idx = idx2 then Some (subst, [])
else None
| (_, _) -> None
@@ -151,27 +152,33 @@ and _unify_builtin (bltin: lexp) (lxp: lexp) (subst: substitution) : return_type
* Let , lexp -> constraint
*)
and _unify_let (let_: lexp) (lxp: lexp) (subst: substitution) : return_type =
- match (let_, lxp) with
- | (Let (_, m, lxp_), Let (_, m1, lxp2)) ->
- let f = (fun (_, lxp, lt) acc -> lxp::lt::acc)
- in (match zip_fold m m1 f with
- | Some [] -> Some (subst, []) (* ??? *)
- | None -> None
- | Some tail -> _unify_inner ((lxp_, lxp2)::(tail)) subst )
+ let concat = (fun (_, lxp, lt) acc -> lxp::lt::acc)
+ in
+ let try_zip_fold m m1 f lxp_ lxp2 subst = match zip_fold m m1 f with
+ | Some [] -> Some (subst, []) (* ??? *)
+ | None -> None
+ | Some tail -> _unify_inner ((lxp_, lxp2)::(tail)) subst
+ in
+ let tmp = match (let_, lxp) with
+ | (Let (_, m, lxp_), Let (_, m1, lxp2)) -> try_zip_fold m m1 concat lxp_ lxp2 subst
| (Let _, _) -> Some (subst, [(let_, lxp)])
| _, _ -> None
+ in match tmp with
+ | Some _ -> Debug_fun.debug_print_unify "_unify_let" let_ lxp " -> unification success"; tmp
+ | None -> Debug_fun.debug_print_unify "_unify_let" let_ lxp " -> unification failed"; tmp
(** Unify a Var and a lexp, if possible
* (Var, Var) -> unify if they have the same debruijn index FIXME : shift indexes
* (Var, Metavar) -> unify_metavar Metavar var subst
* (Var _, _) -> unfiy lexp Var subst
*)
+(*FIXME : check for the value of Var -> need context ?*)
and _unify_var (var: lexp) (r: lexp) (subst: substitution) : return_type =
match (var, r) with
| (Var (_, idx1), Var (_, idx2))
-> if idx1 = idx2 then Some ((subst, []))
else None
- | (Var _, Imm _) -> Some (subst, [(var, r)])(*FIXME : check for the value of Var -> need context ?*)
+ | (Var _, Imm _) -> Some (subst, [(var, r)])
| (Var _, _) -> unify r var subst (*returns to unify*)
| (_, _) -> None
@@ -188,12 +195,10 @@ and _unify_arrow (arrow: lexp) (lxp: lexp) (subst: substitution)
| (Arrow (var_kind1, _, ltype1, _, lexp1), Arrow (var_kind2, _, ltype2, _, lexp2))
-> if var_kind1 = var_kind2
then _unify_inner ((ltype1, ltype2)::(lexp1, lexp2)::[]) subst
- (* _unify_inner_arrow ltype1 lexp1 ltype2 lexp2 subst *)
else None
| (Arrow _, Imm _) -> None
- | (Arrow _, Var _) -> Some (subst, [(arrow, lxp)]) (* FIXME Var can contain type ???*)
+ | (Arrow _, Var _) -> Some (subst, [(arrow, lxp)])
| (Arrow _, _) -> unify lxp arrow subst
- (*| (Arrow _, Call _) -> None*) (* Call can return type (?) *)
| (_, _) -> None
(** Unify a Lambda and a lexp if possible
@@ -209,7 +214,6 @@ and _unify_lambda (lambda: lexp) (lxp: lexp) (subst: substitution) : return_type
| (Lambda (var_kind1, _, ltype1, lexp1), Lambda (var_kind2, _, ltype2, lexp2))
-> if var_kind1 = var_kind2
then _unify_inner ((ltype1, ltype2)::(lexp1, lexp2)::[]) subst
- (*then _unify_inner_arrow ltype1 lexp1 ltype2 lexp2 subst*)
else None
| (Lambda _, Var _) -> Some ((subst, [(lambda, lxp)]))
| (Lambda _, Let _) -> Some ((subst, [(lambda, lxp)]))
@@ -226,13 +230,15 @@ and _unify_lambda (lambda: lexp) (lxp: lexp) (subst: substitution) : return_type
* metavar , lexp -> OK
*)
and _unify_metavar (meta: lexp) (lxp: lexp) (subst: substitution) : return_type =
+ let find_or_unify metavar value lxp s =
+ match find_or_none metavar s with
+ | None -> Some ((associate value lxp s, []))
+ | Some (lxp_) -> unify lxp_ lxp s
+ in
match (meta, lxp) with
| (Metavar (val1, _), Metavar (val2, _)) when val1 = val2 ->
Some ((subst, []))
- | (Metavar (v, _), _) -> (
- match find_or_none meta subst with
- | None -> Some ((associate v lxp subst, []))
- | Some (lxp_) -> unify lxp_ lxp subst)
+ | (Metavar (v, _), _) -> find_or_unify meta v lxp subst
| (_, _) -> None
(** Unify a Call (call) and a lexp (lxp)
@@ -240,14 +246,14 @@ and _unify_metavar (meta: lexp) (lxp: lexp) (subst: substitution) : return_type
* Call , lexp -> CONSTRAINT
*)
and _unify_call (call: lexp) (lxp: lexp) (subst: substitution) : return_type =
+ let f = (fun (_, x) acc -> x::acc)
+ in let try_zip_fold lst1 lst2 lxp1 lxp2 subst = (match zip_fold lst1 lst2 f with
+ | Some [] -> Some (subst, [])
+ | None -> None
+ | Some tail -> _unify_inner ((lxp1, lxp2)::(tail)) subst)
+ in
match (call, lxp) with
- | (Call (lxp1, lxp_list1), Call (lxp2, lxp_list2)) ->
- let f = (fun (_, x) acc -> x::acc)
- in let tail = zip_fold lxp_list1 lxp_list2 f
- in (match tail with
- | Some [] -> Some (subst, [])
- | None -> None
- | Some tail -> _unify_inner ((lxp1, lxp2)::(tail)) subst)
+ | (Call (lxp1, lxp_list1), Call (lxp2, lxp_list2)) -> try_zip_fold lxp_list1 lxp_list2 lxp lxp2 subst
| (Call _, _) -> Some ((subst, [(call, lxp)]))
| (_, _) -> None
@@ -263,17 +269,23 @@ and _unify_susp (susp_: lexp) (lxp: lexp) (subst: substitution) : return_type =
* Case, _ -> Constraint
*)
and _unify_case (case: lexp) (lxp: lexp) (subst: substitution) : return_type =
+ let merge (_, c) r2 = match r2 with
+ | None -> None
+ | Some (s', c') -> Some (s', c@c')
+ in
+ let match_unify_inner lst sm1 sm2 s = match _unify_inner lst s with
+ | None -> None
+ | Some (s, c) -> merge (s, c) (_unify_inner_case (zip (SMap.bindings sm1) (SMap.bindings sm2)) s)
+ in
+ let match_lxp_opt lo1 lo2 tail sm1 sm2 s = match lo1, lo2 with
+ | Some lxp1, Some lxp2 -> match_unify_inner ((lxp1, lxp2)::tail) sm1 sm2 s
+ | _, _ -> None
+ in
let tmp = match case, lxp with
- | (Case (_, lxp, lt11, lt12, smap, lxpopt), Case (_, lxp2, lt21, lt22, smap2, lxopt2))
- -> ( match lxpopt, lxopt2 with
- | Some l1, Some l2 -> (match _unify_inner ((lxp, lxp2)::(lt11, lt21)::(lt12, lt22)::(l1, l2)::[]) subst with
- | Some (s, c) -> (match _unify_inner_case (zip (SMap.bindings smap) (SMap.bindings smap2)) s with
- | Some (s', c') -> Some (s', c@c')
- | None -> None)
- | None -> None)
- | _, _ -> None)
- | (Case _, _) -> Some (subst, [(case, lxp)])
- | (_, _) -> None
+ | (Case (_, lxp, lt11, lt12, smap, lxpopt), Case (_, lxp2, lt21, lt22, smap2, lxopt2))
+ -> match_lxp_opt lxpopt lxopt2 ((lt11, lt21)::(lt12, lt22)::[]) smap smap2 subst
+ | (Case _, _) -> Some (subst, [(case, lxp)])
+ | (_, _) -> None
in match tmp with
| Some _ -> Debug_fun.debug_print_unify "_unify_case" case lxp " -> unification success"; tmp
| None -> Debug_fun.debug_print_unify "_unify_case" case lxp " -> unification failed"; tmp
@@ -337,8 +349,8 @@ and _unify_sort (sort_: lexp) (lxp: lexp) (subst: substitution) : return_type =
and is_same arglist arglist2 =
match arglist, arglist2 with
| (akind, _)::t1, (akind2, _)::t2 when akind = akind2 -> is_same t1 t2
- | [], [] -> Debug_fun.debug_print "is_same -> unification success"; true
- | _, _ -> Debug_fun.debug_print "is_same -> unification failed"; false
+ | [], [] -> Debug_fun.debug_print "is_same" " unification success"; true
+ | _, _ -> Debug_fun.debug_print "is_same" " unification failed"; false
(** try to unify the SMap part of the case *)
and _unify_inner_case l s =
@@ -347,12 +359,12 @@ and _unify_inner_case l s =
| ((key, (_, arglist, lxp)), (key2, (_, arglist2, lxp2)))::tail when key = key2 ->
(if is_same arglist arglist2 then ( match unify lxp lxp2 s with
| Some (s', c) -> (match _unify_inner_case tail s' with
- | Some (s_, c_) -> Debug_fun.debug_print "_unify_inner_case -> unification success"; Some (s_, c@c_)
- | None -> Debug_fun.debug_print "_unify_inner_case -> unification failed"; None)
- | None -> Debug_fun.debug_print "_unify_inner_case -> unification failed"; None)
+ | Some (s_, c_) -> Debug_fun.debug_print "_unify_inner_case" "unification success"; Some (s_, c@c_)
+ | None -> Debug_fun.debug_print "_unify_inner_case" "unification failed"; None)
+ | None -> Debug_fun.debug_print "_unify_inner_case" "unification failed"; None)
else None)
- | [] -> Debug_fun.debug_print "_unify_inner_lxp -> unification success"; Some (s, [])
- | _ -> Debug_fun.debug_print "_unify_inner_case -> unification failed"; None
+ | [] -> Debug_fun.debug_print "_unify_inner_lxp" "unification success"; Some (s, [])
+ | _ -> Debug_fun.debug_print "_unify_inner_case" "unification failed"; None
in (match l with
| Some [] -> Some (s, [])
| None -> None
@@ -404,12 +416,12 @@ and _unify_inner (lxp_l: (lexp * lexp) list) (subst: substitution) : return_type
(lxp_list: (lexp * lexp) list) : return_type =
match _unify_inner lxp_list s with
(*| None -> Some (s, c)*)
- | None -> Debug_fun.debug_print "_unify_inner.merge -> unification failed"; None
- | Some (s_,c_) -> Debug_fun.debug_print "_unify_inner.merge -> unification success"; Some (s_, c@c_)
+ | None -> Debug_fun.debug_print "_unify_inner.merge" "unification failed"; None
+ | Some (s_,c_) -> Debug_fun.debug_print "_unify_inner.merge" "unification success"; Some (s_, c@c_)
in
match lxp_l with
| (lxp1, lxp2)::tail -> ( match unify lxp1 lxp2 subst with
| Some (s, c) -> merge (s, c) tail
- | None -> Debug_fun.debug_print "_unify_inner -> unification failed"; None)
- | [] -> Debug_fun.debug_print "_unify_inner -> unification failed : list empty"; Some (subst, [])
+ | None -> Debug_fun.debug_print "_unify_inner" "unification failed"; None)
+ | [] -> Debug_fun.debug_print "_unify_inner" "unification success : list empty"; Some (subst, [])
View it on GitLab: https://gitlab.com/monnier/typer/compare/817f5f19c651c927ee2825b90f15c8e351…
1
0
[Git][monnier/typer][unification] 3 commits: improved debug printing
by BONNEVALLE Vincent 30 Jui '16
by BONNEVALLE Vincent 30 Jui '16
30 Jui '16
BONNEVALLE Vincent pushed to branch unification at Stefan / Typer
Commits:
2f8bf17e by n3f4s at 2016-06-30T16:01:58+02:00
improved debug printing
- - - - -
156353fa by n3f4s at 2016-06-30T16:03:49+02:00
zip returns option for error handling & refactor
zip return an option for the case when the two list don't have the same
size (-> error), and the empty list case (-> not an error)
extract some function for readability
- - - - -
817f5f19 by n3f4s at 2016-06-30T16:06:20+02:00
add debug printing, correct _unify_inner, add test
_unify_inner returns a substitution if it receive an empty list
change one of the case test to have more difference between the two case
- - - - -
3 changed files:
- src/debug_fun.ml
- src/unification.ml
- tests/unify_test.ml
Changes:
=====================================
src/debug_fun.ml
=====================================
--- a/src/debug_fun.ml
+++ b/src/debug_fun.ml
@@ -1,13 +1,16 @@
open Fmt_lexp
-let _debug = true
+let _debug = false
let indent = ref 0
let do_debug func =
if _debug then (func ()) else ()
+let debug_print str =
+ do_debug (fun () -> print_string str; print_newline (); ())
+
let clear_indent () =
do_debug (fun () -> indent := 0; ())
@@ -20,7 +23,6 @@ let debug_print_lexp lxp =
let debug_print_unify fn lhs rhs str =
let debug_print_unify fn lhs rhs str =
- print_newline ();
print_string (padding_left fn 10 ' ');
print_string " : ";
print_string (String.make (!indent * 4) '-');
@@ -29,4 +31,5 @@ let debug_print_unify fn lhs rhs str =
debug_print_lexp rhs;
print_string str;
indent := !indent + 1;
+ print_newline ();
in do_debug (fun () -> debug_print_unify fn lhs rhs str; ())
=====================================
src/unification.ml
=====================================
--- a/src/unification.ml
+++ b/src/unification.ml
@@ -2,8 +2,6 @@
open Lexp
open Sexp
-open Debug_fun
-
module VMap = Map.Make (struct type t = int let compare = compare end)
type substitution = lexp VMap.t
@@ -11,15 +9,15 @@ type constraints = (lexp * lexp) list
(* IMPROVEMENT For error handling : can carry location and name of type error *)
(*type 'a result =*)
- (*| Some of 'a*)
- (*| Error of Util.location * string (*location * type name*)*)
- (*| Nil*)
+(*| Some of 'a*)
+(*| Error of Util.location * string (*location * type name*)*)
+(*| Nil*)
(*let result_to_option (e: 'a result) : ('a option) =*)
- (*match e with*)
- (*| Some elt -> Some elt*)
- (*| Error _ -> None*)
- (*| Nil -> None*)
+(*match e with*)
+(*| Some elt -> Some elt*)
+(*| Error _ -> None*)
+(*| Nil -> None*)
let global_last_metavar = ref 0
let create_metavar = global_last_metavar := !global_last_metavar + 1; !global_last_metavar
@@ -45,20 +43,15 @@ let find_or_none (value: lexp) (map: substitution) : lexp option =
let empty_subst = (VMap.empty)
(* Zip while applying a function, returns empty list if l1 & l2 have different size*)
-let zip_map (l1: 'a list ) (l2: 'b list ) (f: ('a -> 'b -> 'c)): 'c list=
+let zip_map (l1: 'a list ) (l2: 'b list ) (f: ('a -> 'b -> 'c)): 'c list option =
let rec zip_ ll1 ll2 f =
match ll1, ll2 with
- | (h1::t1, h2::t2) -> (match zip_ t1 t2 f with
- | None -> None
- | Some t -> Some ((f h1 h2)::t))
- | ([], []) -> Some []
- | ([], _) -> None
- | (_, []) -> None
- in match zip_ l1 l2 f with
- | None -> []
- | Some l -> l
+ | (h1::t1, h2::t2) -> (f h1 h2)::(zip_ t1 t2 f)
+ | ([], []) -> []
+ | _, _ -> []
+ in if List.length l1 = List.length l2 then Some (zip_ l1 l2 f) else None
-let zip (l1: 'a list) (l2: 'b list): (('a * 'b) list) = zip_map l1 l2 (fun x z -> (x, z))
+let zip (l1: 'a list) (l2: 'b list): (('a * 'b) list option) = zip_map l1 l2 (fun x z -> (x, z))
let zip_fold list1 list2 f =
let l1 = List.fold_right (f) list1 []
@@ -79,10 +72,8 @@ let zip_fold list1 list2 f =
* If (_unify_X X Y) don't handle the case (X, Y), it call (unify Y X)
* The metavar unifyer is the end rule, it can't call unify with it's parameter (changing their order)
*)
-
let rec unify (l: lexp) (r: lexp) (subst: substitution) : return_type =
- debug_print_unify "unify" l r "";
- match (l, r) with
+ let tmp = match (l, r) with
| (_, Metavar _) -> _unify_metavar r l subst
| (_, Call _) -> _unify_call r l subst
| (_, Case _) -> _unify_case r l subst
@@ -103,6 +94,9 @@ let rec unify (l: lexp) (r: lexp) (subst: substitution) : return_type =
| (Sort _, _) -> _unify_sort l r subst
| (SortLevel _, _) -> _unify_sortlvl l r subst
(* | (_, _) -> None*)
+ in match tmp with
+ | Some _ -> Debug_fun.debug_print_unify "unify" l r " -> unification success"; tmp
+ | None -> Debug_fun.debug_print_unify "unify" l r " -> unification failed"; tmp
(********************************* Type specific unify *******************************)
@@ -157,16 +151,15 @@ and _unify_builtin (bltin: lexp) (lxp: lexp) (subst: substitution) : return_type
* Let , lexp -> constraint
*)
and _unify_let (let_: lexp) (lxp: lexp) (subst: substitution) : return_type =
- debug_print_unify "_unify_let" let_ lxp "";
match (let_, lxp) with
| (Let (_, m, lxp_), Let (_, m1, lxp2)) ->
let f = (fun (_, lxp, lt) acc -> lxp::lt::acc)
- in let tail = zip_fold m m1 f
- in (match tail with
- | [] -> debug_print_unify "_unify_let" let_ lxp " -> No unification"; None
- | _ -> _unify_inner ((lxp_, lxp2)::(tail)) subst )
- | (Let _, _) -> debug_print_unify "_unify_let" let_ lxp " -> Constraint"; Some (subst, [(let_, lxp)])
- | _, _ -> debug_print_unify "_unify_let" let_ lxp " -> No unification"; None
+ in (match zip_fold m m1 f with
+ | Some [] -> Some (subst, []) (* ??? *)
+ | None -> None
+ | Some tail -> _unify_inner ((lxp_, lxp2)::(tail)) subst )
+ | (Let _, _) -> Some (subst, [(let_, lxp)])
+ | _, _ -> None
(** Unify a Var and a lexp, if possible
* (Var, Var) -> unify if they have the same debruijn index FIXME : shift indexes
@@ -252,8 +245,9 @@ and _unify_call (call: lexp) (lxp: lexp) (subst: substitution) : return_type =
let f = (fun (_, x) acc -> x::acc)
in let tail = zip_fold lxp_list1 lxp_list2 f
in (match tail with
- | [] -> None
- | _ -> _unify_inner ((lxp1, lxp2)::(tail)) subst)
+ | Some [] -> Some (subst, [])
+ | None -> None
+ | Some tail -> _unify_inner ((lxp1, lxp2)::(tail)) subst)
| (Call _, _) -> Some ((subst, [(call, lxp)]))
| (_, _) -> None
@@ -269,7 +263,7 @@ and _unify_susp (susp_: lexp) (lxp: lexp) (subst: substitution) : return_type =
* Case, _ -> Constraint
*)
and _unify_case (case: lexp) (lxp: lexp) (subst: substitution) : return_type =
- match case, lxp with
+ let tmp = match case, lxp with
| (Case (_, lxp, lt11, lt12, smap, lxpopt), Case (_, lxp2, lt21, lt22, smap2, lxopt2))
-> ( match lxpopt, lxopt2 with
| Some l1, Some l2 -> (match _unify_inner ((lxp, lxp2)::(lt11, lt21)::(lt12, lt22)::(l1, l2)::[]) subst with
@@ -280,6 +274,9 @@ and _unify_case (case: lexp) (lxp: lexp) (subst: substitution) : return_type =
| _, _ -> None)
| (Case _, _) -> Some (subst, [(case, lxp)])
| (_, _) -> None
+ in match tmp with
+ | Some _ -> Debug_fun.debug_print_unify "_unify_case" case lxp " -> unification success"; tmp
+ | None -> Debug_fun.debug_print_unify "_unify_case" case lxp " -> unification failed"; tmp
(** Unify a Inductive and a lexp
* Inductive, Inductive -> try unify
@@ -289,13 +286,20 @@ and _unify_case (case: lexp) (lxp: lexp) (subst: substitution) : return_type =
*)
and _unfiy_induct (induct: lexp) (lxp: lexp) (subst: substitution) : return_type =
let transform (a, b, c) (d, e, f) = ((a, Some b, c), (d, Some e, f))
- in match (induct, lxp) with
+ and merge m1 m2 (s, c) : return_type = match (_unify_induct_sub_list (SMap.bindings m1) (SMap.bindings m2) s) with
+ | Some (s', c') -> Some (s', c@c')
+ | None -> None
+ in
+ let zip_unify lst subst m1 m2 : return_type = match _unify_inner_induct lst subst with
+ | None -> None
+ | Some (s, c) -> merge m1 m2 (s, c)
+ in
+ match (induct, lxp) with
| (Inductive (_, lbl1, farg1, m1), Inductive (_, lbl2, farg2, m2)) when lbl1 = lbl2 ->
- (match _unify_inner_induct (zip_map farg1 farg2 transform) subst with
- | None -> None
- | Some (s, c) -> (match (_unify_induct_sub_list (SMap.bindings m1) (SMap.bindings m2) s) with
- | Some (s', c') -> Some (s', c@c')
- | None -> None))
+ (match zip_map farg1 farg2 transform with
+ | Some [] -> Some (subst, [])
+ | Some lst -> zip_unify lst subst m1 m2
+ | None -> None)
| (Inductive _, Var _) -> Some (subst, [(induct, lxp)])
| (_, _) -> None
@@ -333,8 +337,8 @@ and _unify_sort (sort_: lexp) (lxp: lexp) (subst: substitution) : return_type =
and is_same arglist arglist2 =
match arglist, arglist2 with
| (akind, _)::t1, (akind2, _)::t2 when akind = akind2 -> is_same t1 t2
- | [], [] -> true
- | _, _ -> false
+ | [], [] -> Debug_fun.debug_print "is_same -> unification success"; true
+ | _, _ -> Debug_fun.debug_print "is_same -> unification failed"; false
(** try to unify the SMap part of the case *)
and _unify_inner_case l s =
@@ -343,21 +347,22 @@ and _unify_inner_case l s =
| ((key, (_, arglist, lxp)), (key2, (_, arglist2, lxp2)))::tail when key = key2 ->
(if is_same arglist arglist2 then ( match unify lxp lxp2 s with
| Some (s', c) -> (match _unify_inner_case tail s' with
- | Some (s_, c_) -> Some (s_, c@c_)
- | None -> None)
- | None -> None)
+ | Some (s_, c_) -> Debug_fun.debug_print "_unify_inner_case -> unification success"; Some (s_, c@c_)
+ | None -> Debug_fun.debug_print "_unify_inner_case -> unification failed"; None)
+ | None -> Debug_fun.debug_print "_unify_inner_case -> unification failed"; None)
else None)
- | [] -> Some (s, [])
- | _ -> None
+ | [] -> Debug_fun.debug_print "_unify_inner_lxp -> unification success"; Some (s, [])
+ | _ -> Debug_fun.debug_print "_unify_inner_case -> unification failed"; None
in (match l with
- | [] -> None
- | _ -> _unify_inner_case l s)
+ | Some [] -> Some (s, [])
+ | None -> None
+ | Some l -> _unify_inner_case l s)
(***** for Inductive *****)
(** for _unify_induct : unify the formal arg*)
and _unify_inner_induct lst subst : return_type =
- let test ((a1, _, l1), (a2, _, l2)) subst : return_type = if a1 = a2
- then unify l1 l2 subst
+ let test ((a1, _, l1), (a2, _, l2)) subst : return_type =
+ if a1 = a2 then unify l1 l2 subst
else None
in
List.fold_left (fun a e -> (match a with
@@ -369,12 +374,21 @@ and _unify_inner_induct lst subst : return_type =
(** unify the SMap of list in Inductive *)
and _unify_induct_sub_list l1 l2 subst =
- let test l1 l2 subst = match l1, l2 with
- | (k1, v1)::t1, (k2, v2)::t2 when k1 = k2 -> (match _unify_inner_induct (zip v1 v2) subst with
- | Some (s, c) -> (match (_unify_induct_sub_list t1 t2 s) with
- | Some (s1, c1) -> Some (s1, c1@c)
- | None -> Some (s, c))
- | None -> (_unify_induct_sub_list t1 t2 subst))
+ let test l1 l2 subst =
+ let merge l1 l2 subst (s, c) = match (_unify_induct_sub_list l1 l2 subst) with
+ | Some (s1, c1) -> Some (s1, c1@c)
+ | None -> Some (s, c)
+ in
+ let unify_zip lst t1 t2 = match _unify_inner_induct lst subst with
+ | Some (s, c) -> merge l1 l2 subst (s, c)
+ | None -> (_unify_induct_sub_list t1 t2 subst)
+ in
+ match l1, l2 with
+ | (k1, v1)::t1, (k2, v2)::t2 when k1 = k2 ->
+ (match zip v1 v2 with
+ | Some [] -> Some (subst, [])
+ | Some lst -> unify_zip lst t1 t2
+ | None -> None)
| _, _ -> None
in test l1 l2 subst
@@ -389,12 +403,13 @@ and _unify_inner (lxp_l: (lexp * lexp) list) (subst: substitution) : return_type
let merge ((s, c): (substitution * constraints))
(lxp_list: (lexp * lexp) list) : return_type =
match _unify_inner lxp_list s with
- | None -> Some (s, c)
- | Some (s_,c_) -> Some (s_, c@c_)
+ (*| None -> Some (s, c)*)
+ | None -> Debug_fun.debug_print "_unify_inner.merge -> unification failed"; None
+ | Some (s_,c_) -> Debug_fun.debug_print "_unify_inner.merge -> unification success"; Some (s_, c@c_)
in
match lxp_l with
| (lxp1, lxp2)::tail -> ( match unify lxp1 lxp2 subst with
| Some (s, c) -> merge (s, c) tail
- | None -> None)
- | [] -> None
+ | None -> Debug_fun.debug_print "_unify_inner -> unification failed"; None)
+ | [] -> Debug_fun.debug_print "_unify_inner -> unification failed : list empty"; Some (subst, [])
=====================================
tests/unify_test.ml
=====================================
--- a/tests/unify_test.ml
+++ b/tests/unify_test.ml
@@ -68,7 +68,6 @@ let str_case = "i = case 0
| _ => 5"
let str_case2 = "i = case 0
| 0 => 12
-| 1 => 12
| _ => 12"
let str_let = "i = let a = 5 in a + 1"
View it on GitLab: https://gitlab.com/monnier/typer/compare/48bc17483a8220a5a93b16abb905703c40…
1
0
[Git][monnier/typer][unification] 5 commits: add printing function for the lexp
by BONNEVALLE Vincent 29 Jui '16
by BONNEVALLE Vincent 29 Jui '16
29 Jui '16
BONNEVALLE Vincent pushed to branch unification at Stefan / Typer
Commits:
57ff42c3 by n3f4s at 2016-06-29T22:48:00+02:00
add printing function for the lexp
- - - - -
107698ef by n3f4s at 2016-06-29T22:48:25+02:00
add printing function for debugging
- - - - -
476e08f2 by n3f4s at 2016-06-29T22:49:48+02:00
add print for debugging
- - - - -
490c9126 by n3f4s at 2016-06-29T22:50:06+02:00
change result of _unify_inner
_unify_inner returned None instead of non-error value, which caused the
unification of the a let with himself to fail
- - - - -
48bc1748 by n3f4s at 2016-06-29T22:51:38+02:00
add test case for let
- - - - -
4 changed files:
- + src/debug_fun.ml
- + src/fmt_lexp.ml
- src/unification.ml
- tests/unify_test.ml
Changes:
=====================================
src/debug_fun.ml
=====================================
--- /dev/null
+++ b/src/debug_fun.ml
@@ -0,0 +1,32 @@
+
+open Fmt_lexp
+
+let _debug = true
+
+let indent = ref 0
+
+let do_debug func =
+ if _debug then (func ()) else ()
+
+let clear_indent () =
+ do_debug (fun () -> indent := 0; ())
+
+let unindent () =
+ do_debug (fun () -> indent := (max 0 (!indent - 1)); ())
+
+let debug_print_lexp lxp =
+ let str = colored_string_of_lxp lxp str_yellow str_magenta
+ in do_debug (fun () -> print_string str; ())
+
+let debug_print_unify fn lhs rhs str =
+ let debug_print_unify fn lhs rhs str =
+ print_newline ();
+ print_string (padding_left fn 10 ' ');
+ print_string " : ";
+ print_string (String.make (!indent * 4) '-');
+ debug_print_lexp lhs;
+ print_string " , ";
+ debug_print_lexp rhs;
+ print_string str;
+ indent := !indent + 1;
+ in do_debug (fun () -> debug_print_unify fn lhs rhs str; ())
=====================================
src/fmt_lexp.ml
=====================================
--- /dev/null
+++ b/src/fmt_lexp.ml
@@ -0,0 +1,68 @@
+
+open Sexp
+open Lexp
+open Fmt
+
+let _color = true
+
+let str_red str = if _color then red ^ str ^ reset else str
+let str_green str = if _color then green ^ str ^ reset else str
+let str_magenta str = if _color then magenta ^ str ^ reset else str
+let str_yellow str = if _color then yellow ^ str ^ reset else str
+let str_cyan str = if _color then cyan ^ str ^ reset else str
+
+let rec string_of_lxp lxp =
+ match lxp with
+ | Imm (Integer (_, value)) -> "Integer(" ^ (string_of_int value) ^ ")"
+ | Imm (String (_, value)) -> "String(" ^ value ^ ")"
+ | Imm (Float (_, value)) -> "Float(" ^ (string_of_float value) ^ ")"
+ | Cons (((_,name),_),_) -> "Cons(" ^ name ^ ")"
+ | Builtin ((_, name), _) -> "Builtin(" ^ name ^ ")"
+ | Let (_) -> "Let(..)"
+ | Var ((_, name), idx) -> "Var(" ^ name ^ ", #" ^(string_of_int idx) ^ ")"
+ | Arrow (_, _, a, _, b) -> "Arrow(" ^ (string_of_lxp a) ^ " => " ^ (string_of_lxp b) ^ ")"
+ | Lambda (_,(_, name), dcl, body) -> "Lambda(" ^ name ^ " : " ^ (string_of_lxp dcl) ^ " => (" ^ (string_of_lxp body) ^ ") )"
+ | Metavar (value, (_, name)) -> "Metavar(" ^ (string_of_int value) ^ ", " ^ name ^ ")"
+ | Call (_) -> "Call(...)"
+ | Inductive _ -> ("Inductive") ^ "(...)"
+ | Sort _ -> ("Sort") ^ "(...)"
+ | SortLevel _ -> ("SortLevel") ^ "(...)"
+ | Case _ -> ("Case") ^ "(...)"
+ | Susp _ -> "Susp(...)"
+ | _ -> "Unidentified Lexp"
+
+let colored_string_of_lxp lxp lcol vcol =
+ match lxp with
+ | Imm (Integer (_, value)) -> (lcol "Integer") ^ "(" ^ (vcol (string_of_int value)) ^ ")"
+ | Imm (String (_, value)) -> (lcol "String") ^ "(" ^ (vcol value ) ^ ")"
+ | Imm (Float (_, value)) -> (lcol "Float" ) ^ "(" ^ (vcol (string_of_float value)) ^ ")"
+ | Cons (((_,name),_),_) -> (lcol "Cons" ) ^ "(" ^ (vcol name) ^ ")"
+ | Builtin ((_, name), _) -> (lcol "Builtin") ^ "(" ^ (vcol name) ^ ")"
+ | Let (_) -> (lcol "Let(..)")
+ | Var ((_, name), idx) -> (lcol "Var" ) ^ "(" ^ (vcol name ) ^ ", " ^ (vcol ("#" ^ (string_of_int idx))) ^ ")"
+ | Arrow (_, _, a, _, b) -> (lcol "Arrow(") ^ (vcol (string_of_lxp a)) ^ " => " ^ (vcol (string_of_lxp b)) ^ ")"
+ | Lambda (_,(_, name), dcl, body) -> (lcol "Lambda") ^ "(" ^ (vcol name) ^ " : " ^ (vcol (string_of_lxp dcl))
+ ^ " => (" ^ (vcol (string_of_lxp body)) ^ "))"
+ | Metavar (value, (_, name)) -> (lcol "Metavar" ) ^ "(" ^ (vcol (string_of_int value)) ^ ", " ^ (vcol name) ^ ")"
+ | Call (_) -> (lcol "Call(...)" )
+ | Case _ -> (lcol "Case") ^ "(...)"
+ | Inductive _ -> (lcol "Inductive") ^ "(...)"
+ | Sort _ -> (lcol "Sort") ^ "(...)"
+ | SortLevel _ -> (lcol "SortLevel") ^ "(...)"
+ | Susp _ -> (lcol "Susp") ^ "(...)"
+ | _ -> (lcol "Unidentified Lexp")
+
+let padding_right (str: string ) (dim: int ) (char_: char) : string =
+ let diff = (dim - String.length str) + 5
+ in let rpad = diff
+ in str ^ (String.make rpad char_)
+
+let padding_left (str: string ) (dim: int ) (char_: char) : string =
+ let diff = (dim - String.length str) + 5
+ in let lpad = diff
+ in (String.make lpad char_) ^ str
+
+let center (str: string ) (dim: int ) (char_: char) : string =
+ let diff = (dim - String.length str) + 5
+ in let lpad, rpad = ((diff / 2 ), ((diff / 2) + (diff mod 2)))
+ in (String.make lpad char_) ^ str ^ (String.make lpad char_)
=====================================
src/unification.ml
=====================================
--- a/src/unification.ml
+++ b/src/unification.ml
@@ -2,25 +2,28 @@
open Lexp
open Sexp
+open Debug_fun
+
module VMap = Map.Make (struct type t = int let compare = compare end)
type substitution = lexp VMap.t
type constraints = (lexp * lexp) list
+
(* IMPROVEMENT For error handling : can carry location and name of type error *)
-(*type 'a expected =*)
-(*| Some of 'a*)
-(*| Error of Util.location * string (*location * type name*)*)
-(*| None*)
+(*type 'a result =*)
+ (*| Some of 'a*)
+ (*| Error of Util.location * string (*location * type name*)*)
+ (*| Nil*)
+
+(*let result_to_option (e: 'a result) : ('a option) =*)
+ (*match e with*)
+ (*| Some elt -> Some elt*)
+ (*| Error _ -> None*)
+ (*| Nil -> None*)
let global_last_metavar = ref 0
let create_metavar = global_last_metavar := !global_last_metavar + 1; !global_last_metavar
-(*let expected_to_option (e: 'a expected) : ('a option) =*)
-(*match e with*)
-(*| Some elt -> Some elt*)
-(*| Error _ -> None*)
-(*| None -> None*)
-
(* For convenience *)
type return_type = (substitution * constraints) option
@@ -78,6 +81,7 @@ let zip_fold list1 list2 f =
*)
let rec unify (l: lexp) (r: lexp) (subst: substitution) : return_type =
+ debug_print_unify "unify" l r "";
match (l, r) with
| (_, Metavar _) -> _unify_metavar r l subst
| (_, Call _) -> _unify_call r l subst
@@ -153,15 +157,16 @@ and _unify_builtin (bltin: lexp) (lxp: lexp) (subst: substitution) : return_type
* Let , lexp -> constraint
*)
and _unify_let (let_: lexp) (lxp: lexp) (subst: substitution) : return_type =
+ debug_print_unify "_unify_let" let_ lxp "";
match (let_, lxp) with
| (Let (_, m, lxp_), Let (_, m1, lxp2)) ->
- let f = (fun (_, t, x) acc -> t::x::acc)
+ let f = (fun (_, lxp, lt) acc -> lxp::lt::acc)
in let tail = zip_fold m m1 f
in (match tail with
- | [] -> None
+ | [] -> debug_print_unify "_unify_let" let_ lxp " -> No unification"; None
| _ -> _unify_inner ((lxp_, lxp2)::(tail)) subst )
- | (Let _, _) -> Some (subst, [(let_, lxp)])
- | _, _ -> None
+ | (Let _, _) -> debug_print_unify "_unify_let" let_ lxp " -> Constraint"; Some (subst, [(let_, lxp)])
+ | _, _ -> debug_print_unify "_unify_let" let_ lxp " -> No unification"; None
(** Unify a Var and a lexp, if possible
* (Var, Var) -> unify if they have the same debruijn index FIXME : shift indexes
@@ -281,7 +286,7 @@ and _unify_case (case: lexp) (lxp: lexp) (subst: substitution) : return_type =
* Inductive, Var -> constraint
* Inductive, Call/Metavar/Case/Let -> constraint
* Inductive, _ -> None
- *)
+*)
and _unfiy_induct (induct: lexp) (lxp: lexp) (subst: substitution) : return_type =
let transform (a, b, c) (d, e, f) = ((a, Some b, c), (d, Some e, f))
in match (induct, lxp) with
@@ -348,7 +353,6 @@ and _unify_inner_case l s =
| [] -> None
| _ -> _unify_inner_case l s)
-
(***** for Inductive *****)
(** for _unify_induct : unify the formal arg*)
and _unify_inner_induct lst subst : return_type =
@@ -385,7 +389,7 @@ and _unify_inner (lxp_l: (lexp * lexp) list) (subst: substitution) : return_type
let merge ((s, c): (substitution * constraints))
(lxp_list: (lexp * lexp) list) : return_type =
match _unify_inner lxp_list s with
- | None -> None (* Some (s, c) *)
+ | None -> Some (s, c)
| Some (s_,c_) -> Some (s_, c@c_)
in
match lxp_l with
@@ -393,3 +397,4 @@ and _unify_inner (lxp_l: (lexp * lexp) list) (subst: substitution) : return_type
| Some (s, c) -> merge (s, c) tail
| None -> None)
| [] -> None
+
=====================================
tests/unify_test.ml
=====================================
--- a/tests/unify_test.ml
+++ b/tests/unify_test.ml
@@ -17,6 +17,9 @@ open Str
open Debug
+open Fmt_lexp
+open Debug_fun
+
type result =
| Constraint
| Unification
@@ -27,27 +30,6 @@ type unif_res = (result * (substitution * constraints) option * lexp * lexp)
type triplet = string * string * string
-(* String & lexp formatting *)
-let rec string_of_lxp lxp =
- match lxp with
- | Imm (Integer (_, value)) -> "Integer(" ^ (string_of_int value) ^ ")"
- | Imm (String (_, value)) -> "String(" ^ value ^ ")"
- | Imm (Float (_, value)) -> "Float(" ^ (string_of_float value) ^ ")"
- | Cons (((_,name),_),_) -> "Cons(" ^ name ^ ")"
- | Builtin ((_, name), _) -> "Builtin(" ^ name ^ ")"
- | Let (_) -> "Let(..)"
- | Var ((_, name), idx) -> "Var(" ^ name ^ ", #" ^(string_of_int idx) ^ ")"
- | Arrow (_, _, a, _, b) -> "Arrow(" ^ (string_of_lxp a) ^ " => " ^ (string_of_lxp b) ^ ")"
- | Lambda (_,(_, name), dcl, body) -> "Lambda(" ^ name ^ " : " ^ (string_of_lxp dcl) ^ " => (" ^ (string_of_lxp body) ^ ") )"
- | Metavar (value, (_, name)) -> "Metavar(" ^ (string_of_int value) ^ ", " ^ name ^ ")"
- | Call (_) -> "Call(...)"
- | Inductive _ -> ("Inductive") ^ "(...)"
- | Sort _ -> ("Sort") ^ "(...)"
- | SortLevel _ -> ("SortLevel") ^ "(...)"
- | Case _ -> ("Case") ^ "(...)"
- | Susp _ -> "Susp(...)"
- | _ -> "???"
-
let string_of_result r =
match r with
| Constraint -> "Constraint"
@@ -62,11 +44,6 @@ let max_dim (lst: (string * string * string * string) list): (int * int * int *i
(0, 0, 0, 0)
lst
-let padding_right (str: string ) (dim: int ) (char_: char) : string =
- let diff = (dim - String.length str) + 5
- in let rpad = diff
- in str ^ (String.make rpad char_)
-
let fmt (lst: (lexp * lexp * result * result) list): string list =
let str_lst = List.map
(fun (l1, l2, r1, r2) -> ((string_of_lxp l1), (string_of_lxp l2), (string_of_result r1), (string_of_result r2)))
@@ -75,11 +52,11 @@ let fmt (lst: (lexp * lexp * result * result) list): string list =
in List.map (fun (l1, l2, r1, r2) -> (padding_right l1 l ' ')
^ " , "
^ (padding_right l2 c1 ' ')
- ^ " -> got :"
+ ^ " -> got : "
^ (padding_right r2 r ' ')
^ " expected : "
^ (padding_right r1 c2 ' ')
- ) str_lst
+ ) str_lst
(* Inputs for the test *)
let str_induct = "Nat = inductive_ (dNat) (zero) (succ Nat)"
@@ -93,6 +70,7 @@ let str_case2 = "i = case 0
| 0 => 12
| 1 => 12
| _ => 12"
+let str_let = "i = let a = 5 in a + 1"
let generate_ltype_from_str str =
List.hd ((fun (lst, _) ->
@@ -113,6 +91,7 @@ let input_int_4 = generate_lexp_from_str str_int_4
let input_int_3 = generate_lexp_from_str str_int_3
let input_case = generate_lexp_from_str str_case
let input_case2 = generate_lexp_from_str str_case2
+let input_let = generate_lexp_from_str str_let
let generate_testable (_: lexp list) : ((lexp * lexp * result) list) =
( Builtin ((Util.dummy_location, "Int=3"), Imm (Integer (Util.dummy_location, 3))),
@@ -152,13 +131,21 @@ let generate_testable (_: lexp list) : ((lexp * lexp * result) list) =
Imm (Integer (Util.dummy_location, 3))), Nothing )
::(input_induct , input_induct , Equivalent)
+
::(input_int_4 , input_int_4 , Equivalent)
+
::(input_int_3 , input_int_4 , Nothing)
+
::(input_case , input_int_4 , Constraint)
::(input_case , input_induct , Constraint)
::(input_case , input_case , Equivalent)
::(input_case , input_case2 , Nothing)
+ ::(input_let , input_induct , Constraint)
+ ::(input_let , input_int_4 , Constraint)
+ ::(input_let , input_case , Constraint)
+ ::(input_let , input_let , Equivalent)
+
::(Let (Util.dummy_location,
[], (*TODO : better tests*)
Var ((Util.dummy_location, "x_let"), 9)) ,
@@ -170,6 +157,7 @@ let generate_testable (_: lexp list) : ((lexp * lexp * result) list) =
let test_input (lxp1: lexp) (lxp2: lexp) (subst: substitution): unif_res =
(*do_debug (fun () -> print_string (fmt_unification_of lxp1 lxp2));*)
+ clear_indent ();
let res = unify lxp1 lxp2 subst in
match res with
| Some (s, []) when s = empty_subst -> (Equivalent, res, lxp1, lxp2)
View it on GitLab: https://gitlab.com/monnier/typer/compare/46aab4745eeb6b8ae28c7e7e6ac1643aa8…
1
0
[Git][monnier/typer][unification] 4 commits: move doc, error management with List.combine
by BONNEVALLE Vincent 29 Jui '16
by BONNEVALLE Vincent 29 Jui '16
29 Jui '16
BONNEVALLE Vincent pushed to branch unification at Stefan / Typer
Commits:
3950fd86 by n3f4s at 2016-06-28T20:48:58+02:00
move doc, error management with List.combine
switch from List.combine to zip to handle case where the two list have
different size
- - - - -
ee113a9e by n3f4s at 2016-06-28T21:43:38+02:00
add test case
- - - - -
ddfe6931 by n3f4s at 2016-06-28T22:39:03+02:00
debug recursion on wrong variable
- - - - -
46aab474 by n3f4s at 2016-06-29T20:51:49+02:00
remove useless code & add test from typer code
add lexp generation from typer code in unification test
add better printing system for unification test
- - - - -
2 changed files:
- src/unification.ml
- tests/unify_test.ml
Changes:
=====================================
src/unification.ml
=====================================
--- a/src/unification.ml
+++ b/src/unification.ml
@@ -41,49 +41,28 @@ let find_or_none (value: lexp) (map: substitution) : lexp option =
let empty_subst = (VMap.empty)
-(**
- * Imm , Imm -> if Imm =/= Imm then ERROR else OK
-
- * Cons , Cons -> ERROR
-
- * Builtin , Builtin -> if Builtin =/= Buitin
- then ERROR else OK
- * Builtin , lexp -> UNIFY lexp of Builtin with lexp
-
- * Let , Let -> UNIFY inside of Let
- * Let , lexp -> CONSTRAINT
-
- * Var , Var -> if db_index ~= db_index UNIFY else ERROR
- * Var , MetaVar -> UNIFY Metavar
- * Var , lexp -> CONSTRAINT
-
- * Arrow , Arrow -> if var_kind = var_kind
- then UNIFY ltype & lexp else ERROR
- * Arrow , Imm -> ERROR
- * Arrow , Var -> CONSTRAINT
-
- * lexp , {metavar <-> none} -> UNIFY
- * lexp , {metavar <-> lexp} -> UNFIFY lexp subst[metavar]
- * metavar , metavar -> if Metavar = Metavar then OK else ERROR
- * metavar , lexp -> OK
-
- * Lamda , Lambda -> if var_kind = var_kind
- then UNIFY ltype & lxp else ERROR
- * Lambda , Var -> CONSTRAINT
- * Lambda , lexp -> ERROR
-
- * Call , lexp -> CONSTRAINT
-
- * Case , lexp -> ERROR (or CONSTRAINT ?)
- * Susp , lexp -> UNIFY (unsusp Susp) lexp
- * Inductive , Inductive -> UNIFY
- * Inductive , lexp -> ERROR (???)
-
- (*TODO*)
- * Sort , lexp ->
- * SortLevel , lexp ->
- * lexp , lexp ->
+(* Zip while applying a function, returns empty list if l1 & l2 have different size*)
+let zip_map (l1: 'a list ) (l2: 'b list ) (f: ('a -> 'b -> 'c)): 'c list=
+ let rec zip_ ll1 ll2 f =
+ match ll1, ll2 with
+ | (h1::t1, h2::t2) -> (match zip_ t1 t2 f with
+ | None -> None
+ | Some t -> Some ((f h1 h2)::t))
+ | ([], []) -> Some []
+ | ([], _) -> None
+ | (_, []) -> None
+ in match zip_ l1 l2 f with
+ | None -> []
+ | Some l -> l
+
+let zip (l1: 'a list) (l2: 'b list): (('a * 'b) list) = zip_map l1 l2 (fun x z -> (x, z))
+
+let zip_fold list1 list2 f =
+ let l1 = List.fold_right (f) list1 []
+ and l2 = List.fold_right (f) list2 []
+ in zip l1 l2
+(**
* lexp is equivalent to _ in ocaml
* (Let , lexp) == (lexp , Let)
* UNIFY -> recursive call or dispatching
@@ -119,7 +98,7 @@ let rec unify (l: lexp) (r: lexp) (subst: substitution) : return_type =
| (Inductive _, _) -> _unfiy_induct l r subst
| (Sort _, _) -> _unify_sort l r subst
| (SortLevel _, _) -> _unify_sortlvl l r subst
-(*| (_, _) -> None*)
+(* | (_, _) -> None*)
(********************************* Type specific unify *******************************)
@@ -143,6 +122,10 @@ and _unify_imm (l: lexp) (r: lexp) (subst: substitution) : return_type =
| (Imm _, _) -> unify r l subst
| (_, _) -> None
+(** Unify a Cons and a lexp
+ * Cons, Cons -> if Cons ~= Cons then OK else ERROR
+ * Cons, _ -> ERROR
+*)
and _unify_cons (cons: lexp) (lxp: lexp) (subst: substitution) : return_type =
(* symbol = (location * string)*)
match (cons, lxp) with
@@ -170,21 +153,20 @@ and _unify_builtin (bltin: lexp) (lxp: lexp) (subst: substitution) : return_type
* Let , lexp -> constraint
*)
and _unify_let (let_: lexp) (lxp: lexp) (subst: substitution) : return_type =
- let combine list1 list2 f =
- let l1 = List.fold_right (f) list1 []
- and l2 = List.fold_right (f) list2 []
- in List.combine l1 l2
- in match (let_, lxp) with
+ match (let_, lxp) with
| (Let (_, m, lxp_), Let (_, m1, lxp2)) ->
let f = (fun (_, t, x) acc -> t::x::acc)
- in _unify_inner ((lxp_, lxp2)::(combine m m1 f)) subst
+ in let tail = zip_fold m m1 f
+ in (match tail with
+ | [] -> None
+ | _ -> _unify_inner ((lxp_, lxp2)::(tail)) subst )
| (Let _, _) -> Some (subst, [(let_, lxp)])
| _, _ -> None
(** Unify a Var and a lexp, if possible
* (Var, Var) -> unify if they have the same debruijn index FIXME : shift indexes
* (Var, Metavar) -> unify_metavar Metavar var subst
- * (_, _) -> None
+ * (Var _, _) -> unfiy lexp Var subst
*)
and _unify_var (var: lexp) (r: lexp) (subst: substitution) : return_type =
match (var, r) with
@@ -199,6 +181,7 @@ and _unify_var (var: lexp) (r: lexp) (subst: substitution) : return_type =
* (Arrow, Arrow) -> if var_kind = var_kind
then unify ltype & lexp (Arrow (var_kind, _, ltype, lexp))
else None
+ * (Arrow, Var) -> Constraint
* (_, _) -> None
*)
and _unify_arrow (arrow: lexp) (lxp: lexp) (subst: substitution)
@@ -216,7 +199,12 @@ and _unify_arrow (arrow: lexp) (lxp: lexp) (subst: substitution)
| (_, _) -> None
(** Unify a Lambda and a lexp if possible
- * See above for result
+ * Lamda , Lambda -> if var_kind = var_kind
+ then UNIFY ltype & lxp else ERROR
+ * Lambda , Var -> CONSTRAINT
+ * Lambda , Call -> Constraint
+ * Lambda , Let -> Constraint
+ * Lambda , lexp -> unify lexp lambda subst
*)
and _unify_lambda (lambda: lexp) (lxp: lexp) (subst: substitution) : return_type =
match (lambda, lxp) with
@@ -234,8 +222,10 @@ and _unify_lambda (lambda: lexp) (lxp: lexp) (subst: substitution) : return_type
| (_, _) -> None
(** Unify a Metavar and a lexp if possible
- * See above for result
- * Metavar is the 'end' of the rules i.e. : it can call unify with his argument (re-ordered)
+ * lexp , {metavar <-> none} -> UNIFY
+ * lexp , {metavar <-> lexp} -> UNFIFY lexp subst[metavar]
+ * metavar , metavar -> if Metavar = Metavar then OK else ERROR
+ * metavar , lexp -> OK
*)
and _unify_metavar (meta: lexp) (lxp: lexp) (subst: substitution) : return_type =
match (meta, lxp) with
@@ -247,18 +237,23 @@ and _unify_metavar (meta: lexp) (lxp: lexp) (subst: substitution) : return_type
| Some (lxp_) -> unify lxp_ lxp subst)
| (_, _) -> None
+(** Unify a Call (call) and a lexp (lxp)
+ * Call , Call -> UNIFY
+ * Call , lexp -> CONSTRAINT
+*)
and _unify_call (call: lexp) (lxp: lexp) (subst: substitution) : return_type =
- let combine list1 list2 f =
- let l1 = List.fold_right (f) list1 []
- and l2 = List.fold_right (f) list2 []
- in List.combine l1 l2
- in match (call, lxp) with
+ match (call, lxp) with
| (Call (lxp1, lxp_list1), Call (lxp2, lxp_list2)) ->
let f = (fun (_, x) acc -> x::acc)
- in _unify_inner ((lxp1, lxp2)::(combine lxp_list1 lxp_list2 f)) subst
+ in let tail = zip_fold lxp_list1 lxp_list2 f
+ in (match tail with
+ | [] -> None
+ | _ -> _unify_inner ((lxp1, lxp2)::(tail)) subst)
| (Call _, _) -> Some ((subst, [(call, lxp)]))
| (_, _) -> None
+(** Apply unsusp to the Susp and unify the result with the lexp
+*)
and _unify_susp (susp_: lexp) (lxp: lexp) (subst: substitution) : return_type =
match susp_ with
| Susp _ -> unify (unsusp_all susp_) lxp subst
@@ -273,7 +268,7 @@ and _unify_case (case: lexp) (lxp: lexp) (subst: substitution) : return_type =
| (Case (_, lxp, lt11, lt12, smap, lxpopt), Case (_, lxp2, lt21, lt22, smap2, lxopt2))
-> ( match lxpopt, lxopt2 with
| Some l1, Some l2 -> (match _unify_inner ((lxp, lxp2)::(lt11, lt21)::(lt12, lt22)::(l1, l2)::[]) subst with
- | Some (s, c) -> (match _unify_inner_case (List.combine (SMap.bindings smap) (SMap.bindings smap2)) s with
+ | Some (s, c) -> (match _unify_inner_case (zip (SMap.bindings smap) (SMap.bindings smap2)) s with
| Some (s', c') -> Some (s', c@c')
| None -> None)
| None -> None)
@@ -285,11 +280,13 @@ and _unify_case (case: lexp) (lxp: lexp) (subst: substitution) : return_type =
* Inductive, Inductive -> try unify
* Inductive, Var -> constraint
* Inductive, Call/Metavar/Case/Let -> constraint
- * Inductive, _ -> None*)
+ * Inductive, _ -> None
+ *)
and _unfiy_induct (induct: lexp) (lxp: lexp) (subst: substitution) : return_type =
- match (induct, lxp) with
+ let transform (a, b, c) (d, e, f) = ((a, Some b, c), (d, Some e, f))
+ in match (induct, lxp) with
| (Inductive (_, lbl1, farg1, m1), Inductive (_, lbl2, farg2, m2)) when lbl1 = lbl2 ->
- (match _unify_inner_induct_1 (List.combine farg1 farg2) subst with
+ (match _unify_inner_induct (zip_map farg1 farg2 transform) subst with
| None -> None
| Some (s, c) -> (match (_unify_induct_sub_list (SMap.bindings m1) (SMap.bindings m2) s) with
| Some (s', c') -> Some (s', c@c')
@@ -297,6 +294,10 @@ and _unfiy_induct (induct: lexp) (lxp: lexp) (subst: substitution) : return_type
| (Inductive _, Var _) -> Some (subst, [(induct, lxp)])
| (_, _) -> None
+(** Unify a SortLevel with a lexp
+ * SortLevel, SortLevel -> if SortLevel ~= SortLevel then OK else ERROR
+ * SortLevel, _ -> ERROR
+*)
and _unify_sortlvl (sortlvl: lexp) (lxp: lexp) (subst: substitution) : return_type =
match sortlvl, lxp with
| (SortLevel s, SortLevel s2) -> (match s, s2 with
@@ -305,6 +306,11 @@ and _unify_sortlvl (sortlvl: lexp) (lxp: lexp) (subst: substitution) : return_ty
| _, _ -> None)
| _, _ -> None
+(** Unify a Sort and a lexp
+ * Sort, Sort -> if Sort ~= Sort then OK else ERROR
+ * Sort, Var -> Constraint
+ * Sort, lexp -> ERROR
+*)
and _unify_sort (sort_: lexp) (lxp: lexp) (subst: substitution) : return_type =
match sort_, lxp with
| (Sort (_, srt), Sort (_, srt2)) -> (match srt, srt2 with
@@ -312,8 +318,8 @@ and _unify_sort (sort_: lexp) (lxp: lexp) (subst: substitution) : return_type =
| StypeOmega, StypeOmega -> Some (subst, [])
| StypeLevel, StypeLevel -> Some (subst, [])
| _, _ -> None)
- | Sort _, Var _ -> Some (subst, [(sort_, lxp)])
- | _, _ -> None
+ | Sort _, Var _ -> Some (subst, [(sort_, lxp)])
+ | _, _ -> None
(************************ Helper function **************************************)
@@ -327,43 +333,25 @@ and is_same arglist arglist2 =
(** try to unify the SMap part of the case *)
and _unify_inner_case l s =
- let rec _unify_inner_case l s =
- match l with
- | ((key, (_, arglist, lxp)), (key2, (_, arglist2, lxp2)))::t when key = key2 ->
+ let rec _unify_inner_case list_ s =
+ match list_ with
+ | ((key, (_, arglist, lxp)), (key2, (_, arglist2, lxp2)))::tail when key = key2 ->
(if is_same arglist arglist2 then ( match unify lxp lxp2 s with
- | Some (s', c) -> (match _unify_inner_case l s' with
+ | Some (s', c) -> (match _unify_inner_case tail s' with
| Some (s_, c_) -> Some (s_, c@c_)
| None -> None)
| None -> None)
else None)
| [] -> Some (s, [])
| _ -> None
- in _unify_inner_case l s
+ in (match l with
+ | [] -> None
+ | _ -> _unify_inner_case l s)
(***** for Inductive *****)
-(*
- Those part of Inductive :
- * ((arg_kind * vdef * ltype) list) (* formal Args *)
- * ((arg_kind * vdef option * ltype) list)
- are almost identical except for the 'vdef option' (which is ignored) so the same function (_unify_inner_induct) should
- work for those part, but it don't work because of 'vdef option'
-*)
-(** for _unfiy_induct_sub_list*)
-and _unify_inner_induct_2 lst subst : return_type =
- let test ((a1, _, l1), (a2, _, l2)) subst : return_type = if a1 = a2
- then unify l1 l2 subst
- else None
- in
- List.fold_left (fun a e -> (match a with
- | Some (s, c) -> (match test e s with
- | Some (s1, c1) -> Some (s1, c1@c)
- | None -> Some (s, c))
- | None -> test e subst)
- ) None lst
-
(** for _unify_induct : unify the formal arg*)
-and _unify_inner_induct_1 lst subst : return_type =
+and _unify_inner_induct lst subst : return_type =
let test ((a1, _, l1), (a2, _, l2)) subst : return_type = if a1 = a2
then unify l1 l2 subst
else None
@@ -378,7 +366,7 @@ and _unify_inner_induct_1 lst subst : return_type =
(** unify the SMap of list in Inductive *)
and _unify_induct_sub_list l1 l2 subst =
let test l1 l2 subst = match l1, l2 with
- | (k1, v1)::t1, (k2, v2)::t2 when k1 = k2 -> (match _unify_inner_induct_2 (List.combine v1 v2) subst with
+ | (k1, v1)::t1, (k2, v2)::t2 when k1 = k2 -> (match _unify_inner_induct (zip v1 v2) subst with
| Some (s, c) -> (match (_unify_induct_sub_list t1 t2 s) with
| Some (s1, c1) -> Some (s1, c1@c)
| None -> Some (s, c))
@@ -405,5 +393,3 @@ and _unify_inner (lxp_l: (lexp * lexp) list) (subst: substitution) : return_type
| Some (s, c) -> merge (s, c) tail
| None -> None)
| [] -> None
-
-
=====================================
tests/unify_test.ml
=====================================
--- a/tests/unify_test.ml
+++ b/tests/unify_test.ml
@@ -27,11 +27,6 @@ type unif_res = (result * (substitution * constraints) option * lexp * lexp)
type triplet = string * string * string
-let _debug = false
-
-let do_debug func =
- if _debug then (func ()) else ()
-
(* String & lexp formatting *)
let rec string_of_lxp lxp =
match lxp with
@@ -53,75 +48,6 @@ let rec string_of_lxp lxp =
| Susp _ -> "Susp(...)"
| _ -> "???"
-let _color = false
-let str_red str = if _color then red ^ str ^ reset else str
-let str_green str = if _color then green ^ str ^ reset else str
-let str_magenta str = if _color then magenta ^ str ^ reset else str
-let str_yellow str = if _color then yellow ^ str ^ reset else str
-let str_cyan str = if _color then cyan ^ str ^ reset else str
-
-let colored_string_of_lxp lxp lcol vcol =
- match lxp with
- | Imm (Integer (_, value)) -> (lcol "Integer") ^ "(" ^ (vcol (string_of_int value)) ^ ")"
- | Imm (String (_, value)) -> (lcol "String") ^ "(" ^ (vcol value ) ^ ")"
- | Imm (Float (_, value)) -> (lcol "Float" ) ^ "(" ^ (vcol (string_of_float value)) ^ ")"
- | Cons (((_,name),_),_) -> (lcol "Cons" ) ^ "(" ^ (vcol name) ^ ")"
- | Builtin ((_, name), _) -> (lcol "Builtin") ^ "(" ^ (vcol name) ^ ")"
- | Let (_) -> (lcol "Let(..)")
- | Var ((_, name), idx) -> (lcol "Var" ) ^ "(" ^ (vcol name ) ^ ", " ^ (vcol ("#" ^ (string_of_int idx))) ^ ")"
- | Arrow (_, _, a, _, b) -> (lcol "Arrow(") ^ (vcol (string_of_lxp a)) ^ " => " ^ (vcol (string_of_lxp b)) ^ ")"
- | Lambda (_,(_, name), dcl, body) -> (lcol "Lambda") ^ "(" ^ (vcol name) ^ " : " ^ (vcol (string_of_lxp dcl))
- ^ " => (" ^ (vcol (string_of_lxp body)) ^ "))"
- | Metavar (value, (_, name)) -> (lcol "Metavar" ) ^ "(" ^ (vcol (string_of_int value)) ^ ", " ^ (vcol name) ^ ")"
- | Call (_) -> (lcol "Call(...)" )
- | Case _ -> (lcol "Case") ^ "(...)"
- | Inductive _ -> (lcol "Inductive") ^ "(...)"
- | Sort _ -> (lcol "Sort") ^ "(...)"
- | SortLevel _ -> (lcol "SortLevel") ^ "(...)"
- | Susp _ -> (lcol "Susp") ^ "(...)"
- | _ -> "???"
-
-let padding_right (str: string ) (dim: int ) (char_: char) : string =
- let diff = (dim - String.length str) + 5
- in let rpad = diff
- in str ^ (String.make rpad char_)
-
-let padding_left (str: string ) (dim: int ) (char_: char) : string =
- let diff = (dim - String.length str) + 5
- in let lpad = diff
- in (String.make lpad char_) ^ str
-
-let center (str: string ) (dim: int ) (char_: char) : string =
- let diff = (dim - String.length str) + 5
- in let lpad, rpad = ((diff / 2 ), ((diff / 2) + (diff mod 2)))
- in (String.make lpad char_) ^ str ^ (String.make lpad char_)
-
-let get_max_dim (str_list : triplet list ) : (int * int * int) =
- let max_ i s = max i (String.length s)
- in (List.fold_left
- (fun (al,ac,ar) (el, ec, er) -> ((max_ al el), (max_ ac ec), (max_ ar er)))
- (0, 0, 0) str_list)
-
-let fmt_unification_result (l: unif_res): string =
- match l with
- | (Constraint, _, lxp1, lxp2) ->
- "{ \"result\" : " ^ (str_yellow "\"Constraint\"") ^ ", \"lexp_left\" : \"" ^ (str_yellow (string_of_lxp lxp1)) ^ "\", \"lexp_right\" : \"" ^ (str_yellow (string_of_lxp lxp2)) ^ "\"}"
- | (Unification, _, lxp1, lxp2) ->
- "{ \"result\" : " ^ (str_yellow "\"Unification\"") ^ ", \"lexp_left\" : \"" ^ (str_yellow (string_of_lxp lxp1)) ^ "\", \"lexp_right\" : \"" ^ (str_yellow (string_of_lxp lxp2)) ^ "\"}"
- | (Equivalent, _, lxp1, lxp2) ->
- "{ \"result\" : " ^ (str_yellow "\"Equivalent\"") ^ ", \"lexp_left\" : \"" ^ (str_yellow (string_of_lxp lxp1)) ^ "\", \"lexp_right\" : \"" ^ (str_yellow (string_of_lxp lxp2)) ^ "\"}"
- | (Nothing, _, lxp1, lxp2) ->
- "{ \"result\" : " ^ (str_yellow "\"Nothing\"") ^ ", \"lexp_left\" : \"" ^ (str_yellow (string_of_lxp lxp1)) ^ "\", \"lexp_right\" : \"" ^ (str_yellow (string_of_lxp lxp2)) ^ "\"}"
-
-let fmt_all (r: unif_res list) =
- List.map fmt_unification_result r
-
-let fmt_unification_of lxp1 lxp2 =
- "Unifying " ^ (colored_string_of_lxp lxp1 str_yellow str_cyan)
- ^ " -> "
- ^ (colored_string_of_lxp lxp2 str_yellow str_cyan)
- ^ "\n"
-
let string_of_result r =
match r with
| Constraint -> "Constraint"
@@ -129,77 +55,68 @@ let string_of_result r =
| Equivalent -> "Equivalent"
| Nothing -> "Nothing"
-let fmt_title l1 l2 r = string_of_lxp l1 ^ ", " ^ string_of_lxp l2 ^ " -> " ^ string_of_result r
-
-(* Inputs for the test *)
-let input_, _ = lexp_decl_str "
- sqr = lambda (x : Int) -> x * x;
- cube = lambda (x : Int) -> x * (sqr x);
-
- mult = lambda (x : Int) -> lambda (y : Int) -> x * y;
-
- twice = (mult 2);
-
- let_fun = lambda (x : Int) ->
- let a = (twice x); b = (mult 2 x); in
- a + b;" default_lctx
-
-let input = List.flatten (List.map (fun (_, l, l2)-> l::l2::[]) (List.flatten input_))
-
-let man_input =
- Imm (Integer (Util.dummy_location, 3))
- ::Imm (Integer (Util.dummy_location, 4))
- ::Builtin ((Util.dummy_location, "Int=3"), Imm (Integer (Util.dummy_location, 3)))
- ::Var ((Util.dummy_location, "x"), 3)
- ::Var ((Util.dummy_location, "y"), 4)
- ::Metavar (0, (Util.dummy_location, "M"))
- ::[]
-
-
-(* Test sample generation *)
-let rec range (begin_: int) (end_: int) : (int list) =
- if begin_ >= end_
- then []
- else begin_::(range (begin_+1) end_)
-
-let generate_combination (r: int list) (input: lexp list) : ((lexp * lexp) list) =
- let begin_ = List.hd r
- in List.map (fun idx -> ((List.nth input begin_ ), (List.nth input idx)) ) r
-
-let generate_couples (input: lexp list) : ((lexp * lexp) list) =
- let length = List.length input
- in List.fold_left (fun acc elt -> (generate_combination (range elt length) input)@acc) [] (range 0 length)
-
-(* Testing the sample *)
+let max_dim (lst: (string * string * string * string) list): (int * int * int *int) =
+ let max i l = max i (String.length l)
+ in List.fold_left
+ (fun (la, ca1, ca2, ra) (l, c1, c2, r) -> ((max la l), (max ca1 c1), (max ca2 c2), (max ra r)))
+ (0, 0, 0, 0)
+ lst
-let test_input (lxp1: lexp) (lxp2: lexp) (subst: substitution): unif_res =
- do_debug (fun () -> print_string (fmt_unification_of lxp1 lxp2));
- let res = unify lxp1 lxp2 subst in
- match res with
- | Some (s, []) when s = empty_subst -> (Equivalent, res, lxp1, lxp2)
- | Some (_, []) -> (Unification, res, lxp1, lxp2)
- | Some _ -> (Constraint, res, lxp1, lxp2)
- | None -> (Nothing, res, lxp1, lxp2)
-
-let test_samples (samples: (lexp * lexp) list) (subst: substitution): (unif_res list) =
- List.map (fun (l1, l2) -> test_input l1 l2 subst) samples
+let padding_right (str: string ) (dim: int ) (char_: char) : string =
+ let diff = (dim - String.length str) + 5
+ in let rpad = diff
+ in str ^ (String.make rpad char_)
-(* Testing the inputs *)
+let fmt (lst: (lexp * lexp * result * result) list): string list =
+ let str_lst = List.map
+ (fun (l1, l2, r1, r2) -> ((string_of_lxp l1), (string_of_lxp l2), (string_of_result r1), (string_of_result r2)))
+ lst
+ in let l, c1, c2, r = max_dim str_lst
+ in List.map (fun (l1, l2, r1, r2) -> (padding_right l1 l ' ')
+ ^ " , "
+ ^ (padding_right l2 c1 ' ')
+ ^ " -> got :"
+ ^ (padding_right r2 r ' ')
+ ^ " expected : "
+ ^ (padding_right r1 c2 ' ')
+ ) str_lst
-let tests (input: lexp list) sample_generator formatter : (string list) =
- let samples = sample_generator input
- in let res = test_samples samples empty_subst
- in formatter res
+(* Inputs for the test *)
+let str_induct = "Nat = inductive_ (dNat) (zero) (succ Nat)"
+let str_int_3 = "i = 3"
+let str_int_4 = "i = 4"
+let str_case = "i = case 0
+| 1 => 2
+| 0 => 42
+| _ => 5"
+let str_case2 = "i = case 0
+| 0 => 12
+| 1 => 12
+| _ => 12"
+
+let generate_ltype_from_str str =
+ List.hd ((fun (lst, _) ->
+ (List.map
+ (fun (_, _, ltype) -> ltype))
+ (List.flatten lst))
+ (lexp_decl_str str default_lctx))
+
+let generate_lexp_from_str str =
+ List.hd ((fun (lst, _) ->
+ (List.map
+ (fun (_, lxp, _) -> lxp))
+ (List.flatten lst))
+ (lexp_decl_str str default_lctx))
+
+let input_induct = generate_lexp_from_str str_induct
+let input_int_4 = generate_lexp_from_str str_int_4
+let input_int_3 = generate_lexp_from_str str_int_3
+let input_case = generate_lexp_from_str str_case
+let input_case2 = generate_lexp_from_str str_case2
let generate_testable (_: lexp list) : ((lexp * lexp * result) list) =
- ( Imm (Integer (Util.dummy_location, 3)) ,
- Imm (Integer (Util.dummy_location, 3)) , Equivalent)
-
- ::( Imm (Integer (Util.dummy_location, 4)) ,
- Imm (Integer (Util.dummy_location, 3)) , Nothing )
-
- ::( Builtin ((Util.dummy_location, "Int=3"), Imm (Integer (Util.dummy_location, 3))),
- Imm (Integer (Util.dummy_location, 3)), Equivalent)
+ ( Builtin ((Util.dummy_location, "Int=3"), Imm (Integer (Util.dummy_location, 3))),
+ Imm (Integer (Util.dummy_location, 3)), Equivalent)
::( Var ((Util.dummy_location, "x"), 3),
Var ((Util.dummy_location, "y"), 4), Nothing )
@@ -233,8 +150,33 @@ let generate_testable (_: lexp list) : ((lexp * lexp * result) list) =
(Util.dummy_location, "L2"),
Var((Util.dummy_location, "z"), 4),
Imm (Integer (Util.dummy_location, 3))), Nothing )
+
+ ::(input_induct , input_induct , Equivalent)
+ ::(input_int_4 , input_int_4 , Equivalent)
+ ::(input_int_3 , input_int_4 , Nothing)
+ ::(input_case , input_int_4 , Constraint)
+ ::(input_case , input_induct , Constraint)
+ ::(input_case , input_case , Equivalent)
+ ::(input_case , input_case2 , Nothing)
+
+ ::(Let (Util.dummy_location,
+ [], (*TODO : better tests*)
+ Var ((Util.dummy_location, "x_let"), 9)) ,
+ Lambda ((Aexplicit),
+ (Util.dummy_location, "L2"),
+ Var((Util.dummy_location, "z"), 4),
+ Imm (Integer (Util.dummy_location, 3))), Constraint )
::[]
+let test_input (lxp1: lexp) (lxp2: lexp) (subst: substitution): unif_res =
+ (*do_debug (fun () -> print_string (fmt_unification_of lxp1 lxp2));*)
+ let res = unify lxp1 lxp2 subst in
+ match res with
+ | Some (s, []) when s = empty_subst -> (Equivalent, res, lxp1, lxp2)
+ | Some (_, []) -> (Unification, res, lxp1, lxp2)
+ | Some _ -> (Constraint, res, lxp1, lxp2)
+ | None -> (Nothing, res, lxp1, lxp2)
+
let check (lxp1: lexp ) (lxp2: lexp ) (res: result) (subst: substitution ): bool =
let r, _, _, _ = test_input lxp1 lxp2 subst
in if r = res then true else false
@@ -246,19 +188,18 @@ let test_if (input: lexp list) sample_generator checker : bool =
| [] -> true
in test_if_ (sample_generator input) checker
-(*let print_as_json (input: lexp list) =*)
- (*let h::t = tests input (generate_couples) (fmt_all)*)
- (*in let s = "[\n" ^ (List.fold_right (fun e a -> a ^ e ^ ",\n") t "") ^ h ^ "\n]\n"*)
- (*in print_string s*)
-
-(*let () = print_as_json (input@man_input)*)
+let unifications = List.map
+ (fun (l1, l2, res) ->
+ let r, _, _, _ = test_input l1 l2 empty_subst
+ in (l1, l2, res, r))
+ (generate_testable [])
let _ = List.map
- (fun (l1, l2, r) ->
+ (fun (str, (l1, l2, expected, res)) ->
add_test "UNIFICATION"
- (fmt_title l1 l2 r)
- (fun () -> if test_if [] (fun _ -> [(l1, l2, r)]) check then success () else failure ()))
- (generate_testable [])
+ (str)
+ (fun () -> if expected = res then success () else failure ()))
+ (List.combine (fmt unifications) unifications )
let _ = run_all ()
View it on GitLab: https://gitlab.com/monnier/typer/compare/86e66e3146beed48763067b0477466ae04…
1
0
28 Jui '16
BONNEVALLE Vincent pushed to branch unification at Stefan / Typer
Commits:
29ba9a05 by Pierre Delaunay at 2016-06-14T17:05:37-04:00
remove dead code
- - - - -
1bf06575 by Pierre Delaunay at 2016-06-14T17:56:19-04:00
Handle macro decls
Changes to be committed:
* src/debug_util.ml : added some debug options
* src/lparse.ml : Handle macro decls
* src/eval.ml :
- added (run-io)
- new function (get_predef_eval) retuns a evaluated predef
* btl/types.typer : added (run-io)
- - - - -
7d78d71b by Pierre Delaunay at 2016-06-14T20:00:25-04:00
delete dead code + add macro decls test
Changes to be committed:
* src/eval.ml : remove dead code
* tests/macro_test.ml: new test
* btl/types.typer : added properties
* src/lparse.ml : added properties
* src/debruijn.ml :
* new function (add_property)
* new function (dump_properties)
* src/debug_util.ml:
* new debug option (dump-prop)
- - - - -
642376ae by Pierre Delaunay at 2016-06-25T18:16:01-04:00
Context accessors and Monad handling. modified travis script
Changes to be committed:
*.travis.yml
* src/debruijn.ml:
- new function (get_attribute)
- new function (has_attribute)
- modify calling convention of (add_attribute) (better consistency)
* btl/types.typer
- added builtin context accessors (decltype) and (declexpr)
* src/eval.ml
- fix monad handling
* src/lparse.ml
- added context accessor as builtin macro
- - - - -
d5da7869 by Pierre Delaunay at 2016-06-25T18:35:09-04:00
new calling convention for builtin functions
(location -> int -> value_type list -> runtime_env -> value_type)
^~~~^ new
This allows us to have a more accurate call trace when eval
is called inside a builtin-function.
Changes to be committed:
* btl/types.typer
* src/builtin.ml
* src/eval.ml
- - - - -
f530a2dd by Pierre Delaunay at 2016-06-26T11:23:25-04:00
Moved builtin macro implementation
Changes to be committed:
* btl/types.typer: change type of some accessors
* src/builtin.ml :
- fix predef shifting
- moved builtin macro implementation there
* src/debruijn.ml: remove dead code
* src/lparse.ml
- builtin macro are now recognized inside (handle_macro_call)
- - - - -
e0141d3f by n3f4s at 2016-06-27T16:38:38+02:00
Merge branch 'master' into unification
- - - - -
716e4d39 by n3f4s at 2016-06-27T16:42:20+02:00
add naive unification for Sort & SortLevel
- - - - -
c2f914ab by n3f4s at 2016-06-27T17:48:41+02:00
re-ordering code for readability
- - - - -
1a8f1f70 by n3f4s at 2016-06-27T17:49:21+02:00
add _unify_sort* to top level unify function
- - - - -
4e00bcc5 by n3f4s at 2016-06-27T22:54:55+02:00
add unification case for _unify_sort
- - - - -
d50e1e6a by n3f4s at 2016-06-27T23:47:55+02:00
correct _unify_induct
- - - - -
8757daba by n3f4s at 2016-06-27T23:48:44+02:00
add unification for Var & Susp with Sort
- - - - -
ba72e9be by n3f4s at 2016-06-28T16:22:56+02:00
Add Case, Let, and Susp to the first unifyed types
- - - - -
b4776a7e by n3f4s at 2016-06-28T16:25:18+02:00
correct case unification
Unification with Case returns a constraint
Check result of unification of the 'inside' of the Case for unification
Case, Case
- - - - -
86e66e31 by n3f4s at 2016-06-28T16:27:39+02:00
Correct _unify_induct & _unify_sort
- - - - -
13 changed files:
- − -
- .travis.yml
- btl/types.typer
- src/builtin.ml
- src/debruijn.ml
- src/debug_util.ml
- src/env.ml
- src/eval.ml
- src/lparse.ml
- src/unification.ml
- tests/macro_test.ml
- tests/unify_test.ml
- − w_file
Changes:
=====================================
- deleted
=====================================
--- a/-
+++ /dev/null
=====================================
.travis.yml
=====================================
--- a/.travis.yml
+++ b/.travis.yml
@@ -3,16 +3,12 @@ language: ocaml
env:
- OCAML_VERSION=4.02
-addons:
- apt:
- packages:
- - opam
-
-before_script:
- - opam config setup -a
- - opam config env
+sudo: true
before_script:
+ - sudo apt-get -qq update
+ - sudo apt-get install opam
+ - opam init --auto-setup
- opam config setup -a
- opam config env
=====================================
btl/types.typer
=====================================
--- a/btl/types.typer
+++ b/btl/types.typer
@@ -27,6 +27,7 @@
%*
%* Description:
%* Define builtin types and functions
+%* This file MUST be correctly typed
%*
%* ---------------------------------------------------------------------------
@@ -34,12 +35,14 @@
% Base Types
% -----------------------------------------------------
-Type = Built-in "Type";
-Int = Built-in "Int";
-Float = Built-in "Float";
-String = Built-in "String";
-Sexp = Built-in "Sexp";
-Unit = Built-in "Unit";
+Type = Built-in "Type";
+Int = Built-in "Int";
+Float = Built-in "Float";
+String = Built-in "String";
+Sexp = Built-in "Sexp";
+
+Unit = Built-in "Unit"; % Nothing
+Context = Built-in "Context"; % Lexp Context
% Basic operators
_+_ = Built-in "_+_" (Int -> Int -> Int);
@@ -134,6 +137,11 @@ bind = Built-in "bind" (
FileHandle = Built-in "FileHandle";
% define operation on file handle
+run-io = Built-in "run-io" (
+ (a : Type) ≡>
+ (b : Type) ≡>
+ IO a -> (a -> IO b) -> (IO b) -> Unit);
+
open = Built-in "open" (String -> String -> IO FileHandle);
write = Built-in "write" (FileHandle -> String -> IO Unit);
read = Built-in "read" (FileHandle -> Int -> IO String);
@@ -143,15 +151,20 @@ read = Built-in "read" (FileHandle -> Int -> IO String);
% -----------------------------------------------------
Attribute = Built-in "Attribute";
-new-attribute = Built-in "new-attribute" (Type -> Attribute);
-
-
-
-
+new-attribute = Built-in "new-attribute" (Macro);
+add-attribute = Built-in "add-attribute" (Macro);
+attribute = Macro_ add-attribute;
+get-attribute = Built-in "get-attribute" Macro;
+has-attribute = Built-in "has-attribute" (Macro);
+% -----------------------------------------------------
+% Context Accessors
+% -----------------------------------------------------
+decltype = Built-in "decltype" Macro;
+declexpr = Built-in "declexpr" Macro;
=====================================
src/builtin.ml
=====================================
--- a/src/builtin.ml
+++ b/src/builtin.ml
@@ -51,19 +51,31 @@ type predef_table = (lexp option ref) SMap.t
let predef_name = [
"cons";
- "nil"
+ "nil";
+ "Unit";
+ "True";
+ "False";
+ "Bool";
]
+let builtin_size = ref 0
+
let predef_map : predef_table =
(* add predef name, expr will be populated when parsing *)
List.fold_left (fun m name ->
SMap.add name (ref None) m) SMap.empty predef_name
-let get_predef name =
+let get_predef_raw (name: string) : lexp =
match !(SMap.find name predef_map) with
| Some exp -> exp
| None -> builtin_error dloc "Try to access an empty predefined"
+let get_predef name ctx =
+ let r = (get_size ctx) - !builtin_size in
+ let v = mkSusp (get_predef_raw name) (S.shift r) in
+ v
+
+
let set_predef name lexp =
SMap.find name predef_map := lexp
@@ -94,7 +106,7 @@ let type_float = Builtin((dloc, "Float"), type0)
let type_string = Builtin((dloc, "String"), type0)
(* Builtin of builtin * string * ltype *)
-let _generic_binary_iop name f loc (args_val: value_type list)
+let _generic_binary_iop name f loc (depth: int) (args_val: value_type list)
(ctx: runtime_env) =
let l, r = match args_val with
@@ -114,11 +126,11 @@ let idiv_impl = _generic_binary_iop "Integer::div" (fun a b -> a / b)
(* loc is given by the compiler *)
-let none_fun : (location -> value_type list -> runtime_env -> value_type)
+let none_fun : (location -> int -> value_type list -> runtime_env -> value_type)
= (fun loc args_val ctx ->
builtin_error loc "Requested Built-in was not implemented")
-let make_symbol loc args_val ctx =
+let make_symbol loc depth args_val ctx =
(* symbol is a simple string *)
let lxp = match args_val with
| [r] -> r
@@ -158,10 +170,12 @@ let rec tlist2olist acc expr =
tlist2olist (hd::acc) tl
| Vcons((_, "nil"), []) -> List.rev acc
| _ ->
+ print_string (value_name expr); print_string "\n";
value_print expr;
+
builtin_error dloc "List conversion failure'"
-let make_node loc args_val ctx =
+let make_node loc depth args_val ctx =
let op, tlist = match args_val with
| [Vsexp(op); lst] -> op, lst
@@ -185,7 +199,7 @@ let make_node loc args_val ctx =
Vsexp(Node(op, s))
-let make_string loc args_val ctx =
+let make_string loc depth args_val ctx =
let lxp = match args_val with
| [r] -> r
| _ -> builtin_error loc ("string_ expects 1 argument") in
@@ -194,7 +208,7 @@ let make_string loc args_val ctx =
| Vstring(str) -> Vsexp(String(loc, str))
| _ -> builtin_error loc ("string_ expects one string as argument")
-let make_integer loc args_val ctx =
+let make_integer loc depth args_val ctx =
let lxp = match args_val with
| [r] -> r
| _ -> builtin_error loc ("integer_ expects 1 argument") in
@@ -203,24 +217,24 @@ let make_integer loc args_val ctx =
| Vint(str) -> Vsexp(Integer(loc, str))
| _ -> builtin_error loc ("integer_ expects one string as argument")
-let make_float loc args_val ctx = Vdummy
-let make_block loc args_val ctx = Vdummy
+let make_float loc depth args_val ctx = Vdummy
+let make_block loc depth args_val ctx = Vdummy
let ttrue = Vcons((dloc, "True"), [])
let tfalse = Vcons((dloc, "False"), [])
let btyper b = if b then ttrue else tfalse
-let string_eq loc args_val ctx =
+let string_eq loc depth args_val ctx =
match args_val with
| [Vstring(s1); Vstring(s2)] -> btyper (s1 = s2)
| _ -> builtin_error loc "string_eq expects 2 strings"
-let int_eq loc args_val ctx =
+let int_eq loc depth args_val ctx =
match args_val with
| [Vint(s1); Vint(s2)] -> btyper (s1 = s2)
| _ -> builtin_error loc "int_eq expects 2 integer"
-let sexp_eq loc args_val ctx =
+let sexp_eq loc depth args_val ctx =
match args_val with
| [Vsexp(s1); Vsexp(s2)] -> (
match s1, s2 with
@@ -232,54 +246,41 @@ let sexp_eq loc args_val ctx =
| _ -> builtin_error loc "int_eq expects 2 sexp"
-let open_impl loc args_val ctx =
+let open_impl loc depth args_val ctx =
let file, mode = match args_val with
| [Vstring(file_name); Vstring(mode)] -> file_name, mode
| _ -> builtin_error loc "open expects 2 strings" in
- (* open file *) (* return a file handle *)
- match mode with
- | "r" -> Vin(open_in file)
- | "w" -> Vout(open_out file)
- | _ -> builtin_error loc "wrong open mode"
-
+ (* open file *) (* return a file handle *)
+ Vcommand(fun () ->
+ match mode with
+ | "r" -> Vin(open_in file)
+ | "w" -> Vout(open_out file)
+ | _ -> builtin_error loc "wrong open mode")
-let read_impl loc args_val ctx =
+let read_impl loc depth args_val ctx =
let channel = match args_val with
| [Vin(c); _] -> c
| _ ->
List.iter (fun v -> value_print v; print_string "\n") args_val;
- builtin_error loc "read expects a in_channel" in
+ builtin_error loc "read expects an in_channel" in
let line = input_line channel in
Vstring(line)
-let write_impl loc args_val ctx =
+let write_impl loc depth args_val ctx =
let channel, msg = match args_val with
| [Vout(c); Vstring(msg)] -> c, msg
| _ ->
List.iter (fun v -> value_print v) args_val;
- builtin_error loc "read expects a out_channel" in
+ builtin_error loc "read expects an out_channel" in
fprintf channel "%s" msg;
Vdummy
-let new_attribute loc args_val ctx =
- builtin_warning loc "new-attributes to be implemented";
- Vdummy
-
-(*
- * Should we have a function that
- * -> returns a new context inside typer ? (So we need to add a ctx type too)
- * -> returns current context ?
- * -> pexp_eval expr
- * -> lexp_eval expr
- * -> ou seulement: 'eval expr ctx'
- *)
-
let is_lbuiltin idx ctx =
let bsize = 1 in
let csize = get_size ctx in
@@ -288,3 +289,85 @@ let is_lbuiltin idx ctx =
true
else
false
+
+(* --------------------------------------------------------------------------
+ * Built-in Macro
+ * -------------------------------------------------------------------------- *)
+
+(* Those are function that are evaluated during lexp_parse *)
+
+let get_attribute_impl loc largs ctx ftype =
+
+ let (vi, vn), (ai, an) = match largs with
+ | [Var((_, vn), vi); Var((_, an), ai)] -> (vi, vn), (ai, an)
+ | _ -> builtin_error loc "get-attribute expects two arguments" in
+
+ let lxp = get_property ctx (vi, vn) (ai, an) in
+ let ltype = env_lookup_expr ctx ((loc, an), ai) in
+ lxp, ltype
+
+let new_attribute_impl loc largs ctx ftype =
+
+ let eltp = match largs with
+ | [eltp] -> eltp
+ | _ -> builtin_warning loc "new-attribute expects one argument"; type0 in
+
+ eltp, ftype
+
+let has_attribute_impl loc largs ctx ftype =
+
+ let (vi, vn), (ai, an) = match largs with
+ | [Var((_, vn), vi); Var((_, an), ai)] -> (vi, vn), (ai, an)
+ | _ -> builtin_error loc "has-attribute expects two arguments" in
+
+ let b = has_property ctx (vi, vn) (ai, an) in
+
+ let rvar = if b then get_predef "True" ctx else get_predef "False" ctx in
+ rvar, (get_predef "Bool" ctx)
+
+let declexpr_impl loc largs ctx ftype =
+
+ let (vi, vn) = match largs with
+ | [Var((_, vn), vi)] -> (vi, vn)
+ | _ -> builtin_error loc "declexpr expects one argument" in
+
+ let lxp = env_lookup_expr ctx ((loc, vn), vi) in
+ let ltp = env_lookup_type ctx ((loc, vn), vi) in
+ lxp, ftype
+
+
+let decltype_impl loc largs ctx ftype =
+
+ let (vi, vn) = match largs with
+ | [Var((_, vn), vi)] -> (vi, vn)
+ | _ -> builtin_error loc "decltype expects one argument" in
+
+ let ltype = env_lookup_type ctx ((loc, vn), vi) in
+ (* mkSusp prop (S.shift (var_i + 1)) *)
+ ltype, type0
+
+let builtin_macro = [
+ ("decltype", decltype_impl);
+ ("declexpr", declexpr_impl);
+ ("get-attribute", get_attribute_impl);
+ ("new-attribute", new_attribute_impl);
+ ("has-attribute", has_attribute_impl);
+]
+
+type macromap =
+ (location -> lexp list -> lexp_context -> lexp -> (lexp * lexp)) SMap.t
+
+let macro_impl_map : macromap =
+ List.fold_left (fun map (name, funct) ->
+ SMap.add name funct map) SMap.empty builtin_macro
+
+let get_macro_impl loc name =
+ try SMap.find name macro_impl_map
+ with Not_found -> builtin_error loc ("Builtin macro" ^ name ^ " not found")
+
+let is_builtin_macro name =
+ try SMap.find name macro_impl_map; true
+ with Not_found -> false
+
+
+
=====================================
src/debruijn.ml
=====================================
--- a/src/debruijn.ml
+++ b/src/debruijn.ml
@@ -123,20 +123,6 @@ let _name_error loc estr str =
debruijn_error loc ("DeBruijn index refers to wrong name. " ^
"Expected: \"" ^ estr ^ "\" got \"" ^ str ^ "\"")
-(*
-let env_set_var_info ctx (def: vref) (v: lexp option) (t: lexp) =
- let ((dv_size, _), info_env, _) = ctx in
- let ((loc, ename), dbi) = def in
-
- try(let rf = (Myers.nth dbi info_env) in
- let (_, (_, name), _, _) = !rf in
-
- (* Check if names match *)
- _name_error loc ename name;
-
- rf := (0, (loc, ename), v, t))
- with
- Not_found -> debruijn_error loc "DeBruijn index out of bounds!" *)
(* generic lookup *)
let _env_lookup ctx (v: vref): env_elem =
@@ -158,7 +144,7 @@ let _env_lookup ctx (v: vref): env_elem =
let env_lookup_type ctx (v : vref): lexp =
let (_, idx) = v in
let (_, _, _, ltp) = _env_lookup ctx v in
- mkSusp ltp (S.shift (idx + 1))
+ mkSusp ltp (S.shift (idx + 0))
let env_lookup_expr ctx (v : vref): lexp =
let (_, idx) = v in
@@ -203,3 +189,84 @@ let replace_by ctx name by =
let nenv = List.fold_left (fun ctx elem -> cons elem ctx) nenv decls in
(a, nenv, b)
+(* -------------------------------------------------------------------------- *)
+(* PropertyMap *)
+(* -------------------------------------------------------------------------- *)
+
+
+let add_property ctx (var_i, var_n) (att_i, att_n) (prop: lexp)
+ : lexp_context =
+
+ let (a, b, property_map) = ctx in
+ let n = get_size ctx in
+
+ (* get_var properties *)
+ let vmap = try PropertyMap.find (var_i, var_n) property_map
+ with Not_found -> PropertyMap.empty in
+
+ (* add property *)
+ let nvmap = PropertyMap.add (n - att_i, att_n) prop vmap in
+
+ (* update properties *)
+ let property_map = PropertyMap.add (n - var_i, var_n) nvmap property_map in
+
+ (a, b, property_map)
+
+let get_property ctx (var_i, var_n) (att_i, att_n): lexp =
+ let (a, b, property_map) = ctx in
+ let n = get_size ctx in
+
+ (* /!\ input index are reversed or not ? I think not so I shift them *)
+ let pmap = try PropertyMap.find (n - var_i, var_n) property_map
+ with Not_found ->
+ debruijn_error dummy_location ("Variable \"" ^ var_n ^ "\" does not have any properties") in
+
+ let prop = try PropertyMap.find (n - att_i, att_n) pmap
+ with Not_found ->
+ debruijn_error dummy_location ("Property \"" ^ att_n ^ "\" not found") in
+ mkSusp prop (S.shift (var_i + 1))
+
+
+let has_property ctx (var_i, var_n) (att_i, att_n): bool =
+ let (a, b, property_map) = ctx in
+ let n = get_size ctx in
+
+ try
+ let pmap = PropertyMap.find (n - var_i, var_n) property_map in
+ let prop = PropertyMap.find (n - att_i, att_n) pmap in
+ true
+ with Not_found -> false
+
+
+let dump_properties ctx =
+ let (a, b, property_map) = ctx in
+ print_string (make_title " Properties ");
+
+ make_rheader [
+ (Some ('l', 10), "V-NAME");
+ (Some ('l', 4), "RIDX");
+ (Some ('l', 10), "P-NAME");
+ (Some ('l', 4), "RIDX");
+ (Some ('l', 32), "LEXP")];
+
+ print_string (make_sep '-');
+
+ PropertyMap.iter (fun (var_i, var_n) pmap ->
+ print_string " | ";
+ lalign_print_string var_n 10; print_string " | ";
+ ralign_print_int var_i 4; print_string " | ";
+ let first = ref true in
+
+ PropertyMap.iter (fun (att_i, att_n) lxp ->
+ (if (!first = false) then
+ print_string (make_line ' ' 20)
+ else
+ first := false);
+
+ lalign_print_string att_n 10; print_string " | ";
+ ralign_print_int att_i 4; print_string " : ";
+ lexp_print lxp; print_string "\n") pmap) property_map;
+
+ print_string (make_sep '-');
+
+
=====================================
src/debug_util.ml
=====================================
--- a/src/debug_util.ml
+++ b/src/debug_util.ml
@@ -275,71 +275,59 @@ let main () =
let octx = default_lctx in
(* Debug declarations merging *)
+ (if (get_p_option "merge-debug") then(
+ let merged = lexp_detect_recursive pexps in
- (** )
- let merged = lexp_detect_recursive pexps in
+ List.iter (fun lst ->
+ print_string (make_line '-' 80);
+ print_string "\n";
- let _ = List.iter (fun lst ->
- print_string (make_line '-' 80);
- print_string "\n";
+ List.iter (fun v ->
+ match v with
+ | Ldecl((l, s), pxp, ptp) -> (
+ lalign_print_string s 20;
- List.iter (fun v ->
- match v with
- | Ldecl((l, s), pxp, ptp) -> (
- lalign_print_string s 20;
+ let _ = match ptp with
+ | Some pxp -> pexp_print pxp;
+ | None -> print_string " " in
- let _ = match ptp with
- | Some pxp -> pexp_print pxp;
- | None -> print_string " " in
+ print_string "\n";
+ lalign_print_string s 20;
- print_string "\n";
- lalign_print_string s 20;
+ let _ = match pxp with
+ | Some pxp -> pexp_print pxp;
+ | None -> print_string " " in
- let _ = match pxp with
- | Some pxp -> pexp_print pxp;
- | None -> print_string " " in
+ print_string "\n")
+ | Lmcall((l, s), _ ) ->
+ print_string s; print_string "\n"
+ ) lst;
- print_string "\n")
- | Lmcall((l, s), _ ) ->
- print_string s; print_string "\n"
- ) lst;
-
- ) merged in ( **)
+ ) merged));
(* debug lexp parsing once merged *)
let lexps, nctx = _lexp_decls pexps octx 0 in
+ (* use the new way of parsing expr *)
+ let ctx = nctx in
+ let flexps = List.flatten lexps in
- (*
- List.iter (fun ((l, s), lxp, ltp) ->
- lalign_print_string s 20;
- lexp_print ltp; print_string "\n";
+ (if (get_p_option "lexp-merge-debug") then(
+ List.iter (fun ((l, s), lxp, ltp) ->
+ lalign_print_string s 20;
+ lexp_print ltp; print_string "\n";
- lalign_print_string s 20;
- lexp_print lxp; print_string "\n";
+ lalign_print_string s 20;
+ lexp_print lxp; print_string "\n";
- ) decls; *)
+ ) flexps));
- (* use the new way of parsing expr *)
- let ctx = nctx in
- let flexps = List.flatten lexps in
+ (if (get_p_option "dump-prop") then(
+ dump_properties ctx;
+ print_string "\n"));
- (* convert a lctx context into a typecheck context *)
- (* they will be the same in the future *)
+ (* get typecheck context *)
let lctx_to_cctx (lctx: lexp_context) =
let (_, env, _) = ctx in env in
- (*
- let (_, env, _) = lctx in
- let n = Myers.length env in
-
- let rec loop i env cctx =
- if i = (-1) then cctx else (
- let i, v, olxp, ltp = !(Myers.nth i env) in
- let vlxp = match olxp with
- | Some lxp -> TC.LetDef lxp
- | None -> TC.ForwardRef in
- let cctx = Myers.cons (i, Some v, vlxp, ltp) cctx in
- loop (i - 1) env cctx) in
- loop n env Myers.nil in *)
(if (get_p_option "typecheck") then(
print_string (make_title " TYPECHECK ");
@@ -349,9 +337,8 @@ let main () =
List.iter (fun (_, lxp, _) ->
let _ = TC.check cctx lxp in ()) flexps;
- print_string (make_line '-' 76);
-
- ));
+ print_string (" " ^ (make_line '-' 76));
+ print_string "\n";));
(if (get_p_option "lexp") then(
print_string (make_title " Lexp ");
@@ -360,20 +347,8 @@ let main () =
(if (get_p_option "lctx") then(
print_lexp_ctx nctx; print_string "\n"));
-
- (*
- List.iter (fun ((_, n), lxp, _) ->
- print_string n; print_string "\n")
- (List.flatten lexps); *)
-
let clean_lxp = EL.clean_toplevel lexps in
- (*
- List.iter (fun ((_, n), lxp) ->
- print_string n; print_string "\n";
- ) (List.flatten clean_lxp);
- *)
-
(* Eval declaration *)
let rctx = default_rctx in
print_string yellow;
=====================================
src/env.ml
=====================================
--- a/src/env.ml
+++ b/src/env.ml
@@ -49,6 +49,7 @@ let env_error loc msg =
let str_idx idx = "[" ^ (string_of_int idx) ^ "]"
+
type value_type =
| Vint of int
| Vstring of string
@@ -61,7 +62,8 @@ type value_type =
| Vdummy
| Vin of in_channel
| Vout of out_channel
- | Vbind of elexp list
+ | Vcommand of (unit -> value_type)
+
let rec value_print (vtp: value_type) =
match vtp with
@@ -81,11 +83,7 @@ let rec value_print (vtp: value_type) =
| Vdummy -> print_string "value_print_dummy"
| Vin _ -> print_string "in_channel"
| Vout _ -> print_string "out_channel"
- | Vbind [a; b] -> print_string "bind (";
- elexp_print a; print_string ") (";
- elexp_print b; print_string ")";
-
- | Vbind _ -> print_string "bind"
+ | Vcommand _ -> print_string "command"
(* | _ -> print_string "debug print" *)
let value_location (vtp: value_type) =
@@ -108,7 +106,7 @@ let value_name v =
| Vdummy -> "Vdummy"
| Vin _ -> "Vin"
| Vout _ -> "Vout"
- | Vbind _ -> "Vbind"
+ | Vcommand _ -> "Vcommand"
(* Runtime Environ *)
type env_cell = (string option * value_type) ref
=====================================
src/eval.ml
=====================================
--- a/src/eval.ml
+++ b/src/eval.ml
@@ -61,6 +61,7 @@ let _eval_max_recursion_depth = ref 255
let reset_eval_trace () = _global_eval_trace := []
let _builtin_lookup = ref SMap.empty
+
(* This is an internal definition
* 'i' is the recursion depth used to print the call trace *)
let rec _eval lxp ctx i: (value_type) =
@@ -83,7 +84,7 @@ let rec _eval lxp ctx i: (value_type) =
| Lambda ((_, n), lxp) -> Closure(n, lxp, ctx)
| Builtin ((_, str)) -> Vbuiltin(str)
- (* Return a value stored in env *)
+ (* Return a value stored in env *)
| Var((loc, name), idx) as e ->
eval_var ctx e ((loc, name), idx)
@@ -100,8 +101,13 @@ let rec _eval lxp ctx i: (value_type) =
| Case (loc, target, pat, dflt)
-> (eval_case ctx i loc target pat dflt)
- | _ -> print_string "debug catch-all eval: ";
- elexp_print lxp; print_string "\n"; Vstring("eval Not Implemented")
+ | Type -> Vcons((tloc, "Unit"), [])
+
+
+and get_predef_eval name ctx =
+ let r = (get_rte_size ctx) - !builtin_size in
+ let v = mkSusp (get_predef_raw name) (S.shift r) in
+ _eval (erase_type v) ctx 0
and eval_var ctx lxp v =
let ((loc, name), idx) = v in
@@ -111,38 +117,34 @@ and eval_var ctx lxp v =
and eval_call ctx i lname eargs =
let loc = elexp_location lname in
- let args = List.map (fun e ->
- (* elexp_print e; print_string "\n"; *)
- _eval e ctx (i + 1)) eargs in
let f = _eval lname ctx (i + 1) in
+ (* standard function *)
let rec eval_call f args ctx =
- match f, args with
- | Vcons (n, []), _ ->
- let e = Vcons(n, args) in
- (* value_print e; print_string "\n"; *) e
-
- (* we add an argument to the closure *)
- | Closure (n, lxp, ctx), hd::tl ->
- let nctx = add_rte_variable (Some n) hd ctx in
- let ret = _eval lxp nctx (i + 1) in
- eval_call ret tl nctx
+ match f, args with
+ | Vcons (n, []), _ ->
+ let e = Vcons(n, args) in
+ (* value_print e; print_string "\n"; *) e
- (* bind is lazily evaluated *)
- | Vbuiltin ("bind"), _ ->
- Vbind eargs
+ (* we add an argument to the closure *)
+ | Closure (n, lxp, ctx), hd::tl ->
+ let nctx = add_rte_variable (Some n) hd ctx in
+ let ret = _eval lxp nctx (i + 1) in
+ eval_call ret tl nctx
- | Vbuiltin (str), args ->
- (* lookup the built-in implementation and call it *)
- (get_builtin_impl str loc) loc args ctx
+ | Vbuiltin (str), args ->
+ (* lookup the built-in implementation and call it *)
+ (get_builtin_impl str loc) loc (i + 1) args ctx
- (* return result of eval *)
- | _, [] -> f
+ (* return result of eval *)
+ | _, [] -> f
- | _ -> debug_msg (value_print f);
- eval_error loc "Cannot eval function" in
+ | _ -> debug_msg (value_print f);
+ eval_error loc "Cannot eval function" in
- eval_call f args ctx
+ (* eval function here *)
+ let args = List.map (fun e -> _eval e ctx (i + 1)) eargs in
+ eval_call f args ctx
and eval_case ctx i loc target pat dflt =
(* Eval target *)
@@ -231,36 +233,62 @@ and typer_builtins_impl = [
("eval_" , typer_eval);
("open" , open_impl);
("bind" , bind_impl);
+ ("run-io" , run_io);
("read" , read_impl);
("write" , write_impl);
- ("new-attribute" , new_attribute)
-
]
-and bind_impl loc args_val ctx =
+
+and bind_impl loc depth args_val ctx =
let io, cb = match args_val with
| [io; callback] -> io, callback
| _ -> builtin_error loc "bind expects two arguments" in
+ (* build Vcommand from io function *)
+ let cmd = match io with
+ | Vcommand (cmd) -> cmd
+ | _ -> builtin_error loc "bind first arguments must be a monad" in
+
+ (* bind returns another Vcommand *)
+ Vcommand (fun () ->
(* get callback *)
- let body, ctx = match cb with
- | Closure(_, body, ctx) -> body, ctx
- | _ -> builtin_error loc "A Closure was expected" in
+ let body, ctx = match cb with
+ | Closure(_, body, ctx) -> body, ctx
+ | _ -> builtin_error loc "A Closure was expected" in
+
+ (* run given command *)
+ let underlying = cmd () in
(* add evaluated IO to arg list *)
- let nctx = add_rte_variable None io ctx in
+ let nctx = add_rte_variable None underlying ctx in
(* eval callback *)
- _eval body nctx 0
+ _eval body nctx depth)
+
+and run_io loc depth args_val ctx =
+
+ let io, ltp = match args_val with
+ | [io; ltp] -> io, ltp
+ | _ -> builtin_error loc "run-io expects 2 arguments" in
+
+ let cmd = match io with
+ | Vcommand (cmd) -> cmd
+ | _ -> builtin_error loc "run-io expects a monad as first argument" in
+
+ (* run given command *)
+ let _ = cmd () in
+
+ (* return given type *)
+ ltp
-and typer_eval loc args ctx =
+and typer_eval loc depth args ctx =
let arg = match args with
| [a] -> a
| _ -> eval_error loc "eval_ expects a single argument" in
(* I need to be able to lexp sexp but I don't have lexp ctx *)
match arg with
(* Nodes that can be evaluated *)
- | Closure (_, body, ctx) -> _eval body ctx 1
+ | Closure (_, body, ctx) -> _eval body ctx depth
(* Leaf *)
| _ -> arg
@@ -279,7 +307,7 @@ and get_builtin_impl str loc =
(* Sexp -> (Sexp -> List Sexp -> Sexp) -> (String -> Sexp) ->
(String -> Sexp) -> (Int -> Sexp) -> (Float -> Sexp) -> (List Sexp -> Sexp)
-> Sexp *)
-and sexp_dispatch loc args ctx =
+and sexp_dispatch loc depth args ctx =
let eval a b = _eval a b 1 in
let sxp, nd, sym, str, it, flt, blk, rctx = match args with
| [sxp; Closure(_, nd, rctx); Closure(_, sym, _);
@@ -373,45 +401,3 @@ let from_lctx (ctx: lexp_context) rm: runtime_env =
done;
!rctx
-
- (* let ((n, _), env, _) = ctx in
- let rctx = ref make_runtime_ctx in
-
- let bsize = 0 in
- let csize = n - 1 in
-
- (* add all variables * )
- for i = bsize to csize do
- let name = match (Myers.nth (csize - i) env) with
- | (_, Some (_, name), _, _) -> Some name
- | _ -> None in
-
- rctx := add_rte_variable name Vdummy (!rctx)
- done; *)
-
- let diff = csize - bsize in
-
- (* process all of them *)
- for i = 0 to diff do
- try
- let j = diff - i (* - 1 *) in
- let name, exp = match Myers.nth (csize - i) env with
- | (_, Some (_, name), LetDef exp, _) -> Some name, Some exp
- | _ -> None, None in
-
- let vxp = match exp with
- | Some lxp ->
- let lxp = (erase_type lxp) in
- (try (eval lxp !rctx)
- with e -> elexp_print lxp;
- print_string "\n"; raise e)
-
- | None -> Vdummy in
- rctx := add_rte_variable name vxp (!rctx)
-
- with Not_found ->
- print_int n; print_string " ";
- print_int (csize - i); print_string "\n ";
- raise Not_found
- done;
- !rctx *)
=====================================
src/lparse.ml
=====================================
--- a/src/lparse.ml
+++ b/src/lparse.ml
@@ -456,102 +456,60 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i =
Call(vf, new_args), ltp in
let handle_macro_call (loc, name) =
- (* look up for definition *)
- let idx = try senv_lookup name ctx
+ (* check for builtin *)
+ match is_builtin_macro name with
+ | true ->
+ let pargs = List.map pexp_parse sargs in
+ let largs = _lexp_parse_all pargs ctx i in
+ (get_macro_impl loc name) loc largs ctx ltp
+
+ (* user defined macro *)
+ | false ->(
+ (* look up for definition *)
+ let idx = try senv_lookup name ctx
+ with Not_found ->
+ lexp_fatal loc ("Could not find Variable: " ^ name) in
+
+ (* Get the macro *)
+ let lxp = try env_lookup_expr ctx ((loc, name), idx)
with Not_found ->
- lexp_fatal loc ("Could not find Variable: " ^ name) in
-
- (* Get the macro *)
- let lxp = try env_lookup_expr ctx ((loc, name), idx) (* with
- | e -> e
- | _ -> lexp_fatal loc "The macro cannot be expanded"; *)
- with Not_found ->
- lexp_fatal loc (name ^ " was found but " ^ (string_of_int idx) ^
- " is not a correct index.") in
-
- let lxp = match unsusp_all lxp with
- | Call(Var((_, "Macro_"), _), [(_, fct)]) -> fct
- | _ ->
- print_string "\n";
- print_string (lexp_to_string lxp); print_string "\n";
- lexp_print lxp; print_string "\n";
- lexp_fatal loc "Macro is ill formed" in
-
- (* Build function to be called *)
- let arg = olist2tlist_lexp sargs ctx in
-
- let lxp = Call(lxp, [(Aexplicit, arg)]) in
- let elexp = EL.erase_type lxp in
- let rctx = (from_lctx ctx 0) in
-
- (*
- let rargs = eval (EL.erase_type arg) rctx in
- let rctx = add_rte_variable None rargs rctx in
-
- let lxp = Susp(lxp, (SU.shift 1)) in
- let body = eval (EL.erase_type lxp) rctx in
-
- print_string "HERE2\n";
- value_print body; *)
- (*
-
- print_string "\n\n";
- lexp_print lxp; print_string "\n\n"; *)
-
- (* print_string "DH: ";
- value_print (eval (EL.erase_type arg) rctx); print_string "\n"; *)
- (*
- print_rte_ctx rctx; print_string "\n";
- print_lexp_ctx ctx; print_string "\n";*)
-
- _global_eval_trace := [];
-
- let vxp = try eval elexp rctx
- with e ->
- print_eval_trace ();
- raise e in
-
- let sxp = match vxp with
- | Vsexp(sxp) -> sxp
- (* Those are sexp converted by the eval function *)
- | Vint(i) -> Integer(dloc, i)
- | Vstring(s) -> String(dloc, s)
- | Vfloat(f) -> Float(dloc, f)
- (* I have vdum here WHY *)
- | v -> debug_msg (value_print v);
- lexp_fatal loc "Macro_ expects '(List Sexp) -> Sexp'" in
-
-
- let pxp = pexp_parse sxp in
- _lexp_p_infer pxp ctx (i + 1) in
-
- (*
- let handle_qq loc =
- (* In quasi quote we need to traverse the sexp tree and evaluate
- * (uq) calls *)
-
- let rec seek_n_replace sxp =
- match sxp with
- (* Unquote *)
- | Node (Symbol(_, "uquote"), [arg]) ->(
- let parg = pexp_parse arg in
- let larg, _ = _lexp_p_infer parg ctx i in
- let vsxp = eval larg (from_lctx ctx) in
- match vsxp with
- | Vint (i) -> Integer(loc, i)
- | Vstring (s) -> String (loc, s)
- | Vsexp(sxp) -> sxp
- | _ ->
- value_print vsxp;
- lexp_warning loc "Sexp was expected"; Epsilon)
-
- | Node (op, lst) -> Node(op, (List.map seek_n_replace lst))
- | _ -> sxp in
-
- let sxp = match sargs with
- | [sxp] -> seek_n_replace sxp
- | _ -> lexp_error loc "qquote expects a sexp"; Epsilon in
- Imm(sxp), type_sexp in *)
+ lexp_fatal loc (name ^ " was found but " ^ (string_of_int idx) ^
+ " is not a correct index.") in
+
+ let lxp = match unsusp_all lxp with
+ | Call(Var((_, "Macro_"), _), [(_, fct)]) -> fct
+ | _ ->
+ print_string "\n";
+ print_string (lexp_to_string lxp); print_string "\n";
+ lexp_print lxp; print_string "\n";
+ lexp_fatal loc "Macro is ill formed" in
+
+ (* Build function to be called *)
+ let arg = olist2tlist_lexp sargs ctx in
+
+ let lxp = Call(lxp, [(Aexplicit, arg)]) in
+ let elexp = EL.erase_type lxp in
+ let rctx = (from_lctx ctx 0) in
+
+ _global_eval_trace := [];
+
+ let vxp = try eval elexp rctx
+ with e ->
+ print_eval_trace ();
+ raise e in
+
+ let sxp = match vxp with
+ | Vsexp(sxp) -> sxp
+ (* Those are sexp converted by the eval function *)
+ | Vint(i) -> Integer(dloc, i)
+ | Vstring(s) -> String(dloc, s)
+ | Vfloat(f) -> Float(dloc, f)
+ (* I have vdum here WHY *)
+ | v -> debug_msg (value_print v);
+ lexp_fatal loc "Macro_ expects '(List Sexp) -> Sexp'" in
+
+ let pxp = pexp_parse sxp in
+ _lexp_p_infer pxp ctx (i + 1)) in
(* determine function type *)
match fun_name, ltp with
@@ -564,7 +522,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i =
Call(body, new_args), ltp
| (Pvar (l, n), Var((_, "Macro"), _)) ->
- (* FIXME: check db_idx points too a Macro type *)
+ (* FIXME: check db_idx points to a Macro type *)
handle_macro_call (l, n)
(* Call to Vanilla or constructor *)
@@ -581,9 +539,9 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i =
Call(body, new_args), ltp
| e, _ ->
- pexp_print e; print_string "\n";
- print_string ((pexp_to_string e) ^ "\n");
- lexp_fatal (pexp_location e) "This expression cannot be called"
+ pexp_print e; print_string "\n";
+ print_string ((pexp_to_string e) ^ "\n");
+ lexp_fatal (pexp_location e) "This expression cannot be called"
(* Read a pattern and create the equivalent representation *)
@@ -670,7 +628,7 @@ and lexp_parse_inductive ctors ctx i =
(* Macro declaration handling, return a list of declarations
* to be processed *)
-and lexp_decls_macro (loc, mname) sargs ctx: pdecl list =
+and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * lexp_context) =
(* lookup for mname_ *)
let idx = try senv_lookup mname ctx
with Not_found ->
@@ -690,26 +648,43 @@ and lexp_decls_macro (loc, mname) sargs ctx: pdecl list =
lexp_print lxp; print_string "\n";
lexp_fatal loc "Macro is ill formed" in
- (* build new function *)
- let arg = olist2tlist_lexp sargs ctx in
- let lxp = Call(lxp, [(Aexplicit, arg)]) in
- let elexp = EL.erase_type lxp in
- let rctx = (from_lctx ctx 0) in
+ match lxp with
+ | Var((_, "add-attribute"), _) ->(
+ (* Builtin macro *)
+ let pargs = List.map pexp_parse sargs in
+ let largs = _lexp_parse_all pargs ctx 0 in
+
+ (* extract info *)
+ let var, att, fn = match largs with
+ | [Var((_, vn), vi); Var((_, an), ai); fn] -> (vi, vn), (ai, an), fn
+ | _ -> lexp_fatal loc "add-attribute expects 3 args" in
- (* get a list of declaration *)
- let decls = eval elexp rctx in
+ let ctx = add_property ctx var att fn in
+
+ [], ctx
+ )
+ (* Standard Macro *)
+ | _ -> (
+ (* build new function *)
+ let arg = olist2tlist_lexp sargs ctx in
+ let lxp = Call(lxp, [(Aexplicit, arg)]) in
+ let elexp = EL.erase_type lxp in
+ let rctx = (from_lctx ctx 0) in
- (* convert typer list to ocaml *)
- let decls = tlist2olist [] decls in
+ (* get a list of declaration *)
+ let decls = eval elexp rctx in
- (* extract sexp from result *)
- let decls = List.map (fun g ->
- match g with
- | Vsexp(sxp) -> sxp
- | _ -> lexp_fatal loc "Macro expects sexp list") decls in
+ (* convert typer list to ocaml *)
+ let decls = tlist2olist [] decls in
- (* read as pexp_declaraton *)
- pexp_decls_all decls
+ (* extract sexp from result *)
+ let decls = List.map (fun g ->
+ match g with
+ | Vsexp(sxp) -> sxp
+ | _ -> lexp_fatal loc "Macro expects sexp list") decls in
+
+ (* read as pexp_declaraton *)
+ pexp_decls_all decls, ctx)
(* Parse let declaration *)
and lexp_p_decls decls ctx = _lexp_decls decls ctx 0
@@ -797,9 +772,19 @@ and _lexp_decls decls ctx i: ((vdef * lexp * ltype) list list * lexp_context) =
let all = ref [] in
let ctx = List.fold_left (fun ctx decl ->
- let d, ctx = _lexp_rec_decl decl ctx i in
- all := d::!all;
- ctx) ctx decls in
+ match decl with
+ (* Special case *)
+ | [Lmcall ((l, s), sargs)] ->
+ (* get pexp decls *)
+ let pdecls, ctx = lexp_decls_macro (l, s) sargs ctx in
+ let decls, ctx = _lexp_decls pdecls ctx i in
+ all := (List.append (List.rev decls) !all);
+ ctx
+
+ | _ ->
+ let d, ctx = _lexp_rec_decl decl ctx i in
+ all := d::!all;
+ ctx) ctx decls in
(List.rev !all), ctx
@@ -853,171 +838,9 @@ and _lexp_rec_decl decls ctx i =
(List.rev !lst), ctx
- (*
-and _lexp_decls decls ctx i: (((vdef * lexp * ltype) list list) * lexp_context) =
-
- let names = ref [] in (* decls name in correct order *)
- let glob = ref SMap.empty in
- let mut = ref [] in
- let offset = ref 1 in
- let last_decls = ref "" in
- let recursive_mode = ref false in
-
- let ctx = List.fold_left (fun vctx expr ->
- _global_lexp_trace := [];
- match expr with
- | Pexpr((l, s), pxp) ->(
- try let idx = senv_lookup s vctx in
- let ltp = env_lookup_type vctx ((l, s), idx) in
- let lxp = lexp_p_check pxp ltp vctx in
- (* update declaration *)
- glob := SMap.add s (l, s, Some lxp, ltp) !glob;
-
- (* check if recursive definition *)
- (if !last_decls = s && !recursive_mode then
- (
- (* print_string "RECURSIVE END\n"; *)
- (* push every variable with the correct offset *)
- let d = List.rev !mut in
- let length = (List.length d) + 1 in
- let j = ref 0 in
-
- let vctx =
- List.fold_left (fun vctx n ->
- let (l, s, lxp, ltp) = SMap.find n !glob in
- let lxp = match lxp with
- | Some lxp -> LetDef lxp
- | None -> lexp_warning dloc "ForwardRef are not allowed";
- ForwardRef in
-
- j := !j + 1;
- replace_by vctx s (length - !j, Some (l, s), lxp, ltp)) vctx d
-
- in
-
- (* Clean everything *)
- mut := [];
- last_decls := "";
- recursive_mode := false;
- vctx
- )
- else
- (
- (if !recursive_mode then offset := !offset + 1);
- (* update context *)
- replace_by vctx s (1, Some (l, s), (LetDef lxp), ltp);
- ));
-
- with Not_found ->
- (* Add dummy first *)
- let tctx = env_extend vctx (l, s) ForwardRef dltype in
- let lxp, ltp = lexp_p_infer pxp tctx in
-
- names := [s]::!names;
-
- (if !recursive_mode then (
- offset := !offset + 1;
- mut := s::!mut));
-
- glob := SMap.add s (l, s, Some lxp, ltp) !glob;
-
- env_extend vctx (l, s) (LetDef lxp) ltp)
-
- | Ptype((l, s), ptp) ->
- (if !recursive_mode then () else
- last_decls := s;
- offset := 1);
-
- recursive_mode := true;
- names := [s]::!names;
- mut := s::!mut;
-
- (* get type *)
- let ltp, _ = lexp_p_infer ptp vctx in
- (* push *)
- glob := SMap.add s (l, s, None, ltp) !glob;
- env_extend vctx (l, s) ForwardRef ltp
-
- | Pmcall((l, n), sargs) -> (
- let pdecls = lexp_decls_macro (l, n) sargs vctx in
- let _, _ =_lexp_decls pdecls vctx (i + 1) in
-
- vctx)
-
- (* | _ -> vctx*)) ctx decls in
-
- (*
- (if List.length !mut != 0 then names := !mut::!names); *)
-
- (* return a list containing mutually recursive def *)
- let merge_list names =
- List.fold_left (fun acc key ->
- let (l, s, lxp, ltp) = SMap.find key !glob in
- let lxp = match lxp with
- | Some lxp -> lxp
- | None -> dltype in
-
- (*
- let ltp = unsusp_all ltp in
- let lxp = unsusp_all lxp in *)
- ((l, s), lxp, ltp)::acc) [] names in
-
- let decls = List.map (fun names ->
- merge_list names) (List.rev !names) in
-
- decls, ctx
-*)
-
and lexp_decls_toplevel decls ctx =
_lexp_decls decls ctx 1
- (* let names = ref [] in
- let offset = ref 0 in
- let merged = ref SMap.empty in
- let acc = ref [] in
-
- let ctx = List.fold_left (fun vctx expr ->
- match expr with
- | Pexpr ((l, s), pxp) ->(
- try let idx = senv_lookup s vctx in
- let ltp = env_lookup_type vctx ((l, s), idx) in
- let lxp = lexp_p_check pxp ltp vctx in
- let (_, _, _, ltp) = SMap.find s !merged in
- merged := SMap.add s (l, s, Some lxp, ltp) !merged;
- let r = !offset in
- let r = if r = 0 then 1 else r in
- offset := 0;
- replace_by vctx s (r, Some (l, s), (LetDef lxp), ltp);
-
- with Not_found ->
- (* Add dummy first *)
- let tctx = env_extend vctx (l, s) ForwardRef dltype in
- let lxp, ltp = lexp_p_infer pxp tctx in
- names := s::!names;
- merged := SMap.add s (l, s, Some lxp, ltp) !merged;
- env_extend vctx (l, s) (LetDef lxp) ltp)
-
- | Ptype ((l, s), ptp) ->
- offset := !offset + 1;
- let ltp, _ = lexp_p_infer ptp vctx in
- names := s::!names;
- merged := SMap.add s (l, s, None, ltp) !merged;
- env_extend vctx (l, s) ForwardRef ltp
-
- | _ -> vctx) ctx decls in
-
- (* merge type and expr *)
- let decls = List.fold_left (fun acc key ->
- let (l, s, lxp, ltp) = SMap.find key !merged in
- let lxp = match lxp with
- | Some lxp -> lxp
- | None -> dltype in
- let ltp = unsusp_all ltp in
- let lxp = unsusp_all lxp in
- ((l, s), lxp, ltp)::acc) [] !names in
-
- decls, ctx *)
-
and _lexp_parse_all (p: pexp list) (ctx: lexp_context) i : lexp list =
let rec loop (plst: pexp list) ctx (acc: lexp list) =
@@ -1160,12 +983,13 @@ let default_lctx =
List.iter (fun ((_, s), _, _) ->
print_string (s ^ ", ")) decls; print_string "] \n") d; *)
+ builtin_size := get_size lctx;
+
(* Once default builtin are set we can populate the predef table *)
try
List.iter (fun name ->
let idx = senv_lookup name lctx in
- let v = Var((dloc, name), idx) in (*
- let value = (env_lookup_expr lctx v) in *)
+ let v = Var((dloc, name), idx) in
set_predef name (Some v)) predef_name;
(* -- DONE -- *)
lctx
@@ -1194,13 +1018,6 @@ let default_rctx =
let rctx = eval_decls_toplevel (EL.clean_toplevel d) rctx in
_global_eval_trace := [];
rctx
- (*
- try (from_lctx (default_lctx))
- with e ->(
- print_eval_trace ();
- lexp_error dloc "Could not convert lexp context into rte context";
- raise e) *)
-
(* String Parsing
* --------------------------------------------------------- *)
=====================================
src/unification.ml
=====================================
--- a/src/unification.ml
+++ b/src/unification.ml
@@ -91,6 +91,8 @@ let empty_subst = (VMap.empty)
* CONSTRAINT -> returns a constraint
*)
+(****************************** Top level unify *************************************)
+
(** Dispatch to the right unifyer.
* If (_unify_X X Y) don't handle the case (X, Y), it call (unify Y X)
* The metavar unifyer is the end rule, it can't call unify with it's parameter (changing their order)
@@ -100,6 +102,9 @@ let rec unify (l: lexp) (r: lexp) (subst: substitution) : return_type =
match (l, r) with
| (_, Metavar _) -> _unify_metavar r l subst
| (_, Call _) -> _unify_call r l subst
+ | (_, Case _) -> _unify_case r l subst
+ | (_, Susp _) -> _unify_susp r l subst
+ | (_, Let _) -> _unify_let r l subst
| (Imm _, _) -> _unify_imm l r subst
| (Cons _, _) -> _unify_cons l r subst
| (Builtin _, _) -> _unify_builtin l r subst
@@ -112,107 +117,32 @@ let rec unify (l: lexp) (r: lexp) (subst: substitution) : return_type =
| (Susp _, _) -> _unify_susp l r subst
| (Case _, _) -> _unify_case l r subst
| (Inductive _, _) -> _unfiy_induct l r subst
- | (_, _) -> None
+ | (Sort _, _) -> _unify_sort l r subst
+ | (SortLevel _, _) -> _unify_sortlvl l r subst
+(*| (_, _) -> None*)
-(** Check arg_king in (arg_kind * vdef option) list in Case *)
-and is_same arglist arglist2 =
- match arglist, arglist2 with
- | (akind, _)::t1, (akind2, _)::t2 when akind = akind2 -> is_same t1 t2
- | [], [] -> true
- | _, _ -> false
+(********************************* Type specific unify *******************************)
-(** try to unify the SMap part of the case *)
-and _unify_inner_case l s =
- let rec _unify_inner_case l s =
- match l with
- | ((key, (_, arglist, lxp)), (key2, (_, arglist2, lxp2)))::t when key = key2 ->
- (if is_same arglist arglist2 then ( match unify lxp lxp2 s with
- | Some (s', c) -> (match _unify_inner_case l s' with
- | Some (s_, c_) -> Some (s_, c@c_)
- | None -> None)
- | None -> None)
- else None)
- | [] -> Some (s, [])
- | _ -> None
- in _unify_inner_case l s
-
-(** Unify a Case with a lexp
- * Case, Var -> constraint (if the variable type and the type of the return value is equivalent, it should be unifiable)
- * Case, Case -> try to unify
- * Case, _ -> None
- *)
-and _unify_case (case: lexp) (lxp: lexp) (subst: substitution) : return_type =
-(* Maybe Constraint instead ?*)
- match case, lxp with
- | (Case (_, lxp, lt11, lt12, smap, lxpopt), Case (_, lxp2, lt21, lt22, smap2, lxopt2))
- -> ( match lxpopt, lxopt2 with
- | Some l1, Some l2 -> (match _unify_inner ((lxp, lxp2)::(lt11, lt21)::(lt12, lt22)::(l1, l2)::[]) subst with
- | Some (s, c) -> _unify_inner_case (List.combine (SMap.bindings smap) (SMap.bindings smap2)) s (* TODO match on result *)
- | None -> None)
- | _, _ -> None)
- | (Case _, Var _) -> Some (subst, [(case, lxp)]) (* ??? *)
- | (_, _) -> None
-
-(*
- Those part of Inductive :
- * ((arg_kind * vdef * ltype) list) (* formal Args *)
- * ((arg_kind * vdef option * ltype) list)
- are almost identical except for the 'vdef option' (which is ignored) so the same function (_unify_inner_induct) should
- work for those part, but it don't work because of 'vdef option'
+(** Unify two Imm if they match <=> Same type and same value
+ * Add one of the Imm (the first arguement) to the substitution
+ * Imm, Imm -> if Imm =/= Imm then ERROR else OK
+ * Imm, lexp -> unify lexp Imm
*)
-(** for _unfiy_induct_sub_list*)
-and _unify_inner_induct_2 lst subst : return_type =
- let test ((a1, _, l1), (a2, _, l2)) subst : return_type = if a1 = a2
- then unify l1 l2 subst
+and _unify_imm (l: lexp) (r: lexp) (subst: substitution) : return_type =
+ match (l, r) with
+ | (Imm (String (_, v1)), Imm (String (_, v2)))
+ -> if v1 = v2 then Some ((subst, []))
else None
- in
- List.fold_left (fun a e -> (match a with
- | Some (s, c) -> (match test e s with
- | Some (s1, c1) -> Some (s1, c1@c)
- | None -> Some (s, c))
- | None -> test e subst)
- ) None lst
-
-(** for _unify_induct : unify the formal arg*)
-and _unify_inner_induct_1 lst subst : return_type =
- let test ((a1, _, l1), (a2, _, l2)) subst : return_type = if a1 = a2
- then unify l1 l2 subst
+ | (Imm (Integer (_, v1)), Imm (Integer (_, v2)))
+ -> if v1 = v2 then Some ((subst, []))
else None
- in
- List.fold_left (fun a e -> (match a with
- | Some (s, c) -> (match test e s with
- | Some (s1, c1) -> Some (s1, c1@c)
- | None -> Some (s, c))
- | None -> test e subst)
- ) None lst
-
-(** unify the SMap of list in Inductive *)
-and _unify_induct_sub_list l1 l2 subst =
- let test l1 l2 subst = match l1, l2 with
- | (k1, v1)::t1, (k2, v2)::t2 when k1 = k2 -> (match _unify_inner_induct_2 (List.combine v1 v2) subst with
- | Some (s, c) -> (match (_unify_induct_sub_list t1 t2 s) with
- | Some (s1, c1) -> Some (s1, c1@c)
- | None -> Some (s, c))
- | None -> (_unify_induct_sub_list t1 t2 subst))
- | _, _ -> None
- in test l1 l2 subst
-
-(** Unify a Inductive and a lexp
- * Inductive, Inductive -> try t unify
- * Inductive, _ -> None*)
-and _unfiy_induct (induct: lexp) (lxp: lexp) (subst: substitution) : return_type =
- match (induct, lxp) with
- | (Inductive (_, lbl1, farg1, m1), Inductive (_, lbl2, farg2, m2)) when lbl1 = lbl2 ->
- (match _unify_inner_induct_1 (List.combine farg1 farg2) subst with
- | None -> None
- | Some (s, c) -> _unify_induct_sub_list (SMap.bindings m1) (SMap.bindings m2) s)
+ | (Imm (Float (_, v1)), Imm (Float (_, v2)))
+ -> if v1 = v2 then Some ((subst, []))
+ else None
+ | (Imm _, Imm _) -> None
+ | (Imm _, _) -> unify r l subst
| (_, _) -> None
-and _unify_susp (susp_: lexp) (lxp: lexp) (subst: substitution) : return_type =
- match susp_ with
- | Susp _ -> unify (unsusp_all susp_) lxp subst
- | _ -> None
-
and _unify_cons (cons: lexp) (lxp: lexp) (subst: substitution) : return_type =
(* symbol = (location * string)*)
match (cons, lxp) with
@@ -223,16 +153,67 @@ and _unify_cons (cons: lexp) (lxp: lexp) (subst: substitution) : return_type =
else None
| (_, _) -> None
-and _unify_call (call: lexp) (lxp: lexp) (subst: substitution) : return_type =
- let combine list1 list2 =
- let l1 = List.fold_right (fun (_, x) acc -> x::acc) list1 []
- and l2 = List.fold_right (fun (_, x) acc -> x::acc) list2 []
+(** Unify a builtin (bltin) and a lexp (lxp) if it is possible
+ * If the two arguments are builtin, unify based on name
+ * If it's a Builtin and an other lexp, unify lexp part of Builtin with the lexp
+*)
+and _unify_builtin (bltin: lexp) (lxp: lexp) (subst: substitution) : return_type =
+ match (bltin, lxp) with
+ | (Builtin ((_, name1), _), Builtin ((_, name2),_))
+ -> if name1 = name2 then Some ((subst, []))
+ else None (* assuming that builtin have unique name *)
+ | (Builtin (_, lxp_bltin), _) -> unify lxp_bltin lxp subst
+ | (_, _) -> None
+
+(** Unify a Let (let_) and a lexp (lxp), if possible
+ * Let , Let -> check the 'inside' of the let
+ * Let , lexp -> constraint
+*)
+and _unify_let (let_: lexp) (lxp: lexp) (subst: substitution) : return_type =
+ let combine list1 list2 f =
+ let l1 = List.fold_right (f) list1 []
+ and l2 = List.fold_right (f) list2 []
in List.combine l1 l2
- in match (call, lxp) with
- | (Call (lxp1, lxp_list1), Call (lxp2, lxp_list2)) ->
- _unify_inner ((lxp1, lxp2)::(combine lxp_list1 lxp_list2)) subst
- | (Call _, _) -> Some ((subst, [(call, lxp)]))
- | (_, _) -> None
+ in match (let_, lxp) with
+ | (Let (_, m, lxp_), Let (_, m1, lxp2)) ->
+ let f = (fun (_, t, x) acc -> t::x::acc)
+ in _unify_inner ((lxp_, lxp2)::(combine m m1 f)) subst
+ | (Let _, _) -> Some (subst, [(let_, lxp)])
+ | _, _ -> None
+
+(** Unify a Var and a lexp, if possible
+ * (Var, Var) -> unify if they have the same debruijn index FIXME : shift indexes
+ * (Var, Metavar) -> unify_metavar Metavar var subst
+ * (_, _) -> None
+*)
+and _unify_var (var: lexp) (r: lexp) (subst: substitution) : return_type =
+ match (var, r) with
+ | (Var (_, idx1), Var (_, idx2))
+ -> if idx1 = idx2 then Some ((subst, []))
+ else None
+ | (Var _, Imm _) -> Some (subst, [(var, r)])(*FIXME : check for the value of Var -> need context ?*)
+ | (Var _, _) -> unify r var subst (*returns to unify*)
+ | (_, _) -> None
+
+(** Unify a Arrow and a lexp if possible
+ * (Arrow, Arrow) -> if var_kind = var_kind
+ then unify ltype & lexp (Arrow (var_kind, _, ltype, lexp))
+ else None
+ * (_, _) -> None
+*)
+and _unify_arrow (arrow: lexp) (lxp: lexp) (subst: substitution)
+ : return_type =
+ match (arrow, lxp) with
+ | (Arrow (var_kind1, _, ltype1, _, lexp1), Arrow (var_kind2, _, ltype2, _, lexp2))
+ -> if var_kind1 = var_kind2
+ then _unify_inner ((ltype1, ltype2)::(lexp1, lexp2)::[]) subst
+ (* _unify_inner_arrow ltype1 lexp1 ltype2 lexp2 subst *)
+ else None
+ | (Arrow _, Imm _) -> None
+ | (Arrow _, Var _) -> Some (subst, [(arrow, lxp)]) (* FIXME Var can contain type ???*)
+ | (Arrow _, _) -> unify lxp arrow subst
+ (*| (Arrow _, Call _) -> None*) (* Call can return type (?) *)
+ | (_, _) -> None
(** Unify a Lambda and a lexp if possible
* See above for result
@@ -266,100 +247,152 @@ and _unify_metavar (meta: lexp) (lxp: lexp) (subst: substitution) : return_type
| Some (lxp_) -> unify lxp_ lxp subst)
| (_, _) -> None
-(** Unify a Arrow and a lexp if possible
- * (Arrow, Arrow) -> if var_kind = var_kind
- then unify ltype & lexp (Arrow (var_kind, _, ltype, lexp))
- else None
- * (_, _) -> None
+and _unify_call (call: lexp) (lxp: lexp) (subst: substitution) : return_type =
+ let combine list1 list2 f =
+ let l1 = List.fold_right (f) list1 []
+ and l2 = List.fold_right (f) list2 []
+ in List.combine l1 l2
+ in match (call, lxp) with
+ | (Call (lxp1, lxp_list1), Call (lxp2, lxp_list2)) ->
+ let f = (fun (_, x) acc -> x::acc)
+ in _unify_inner ((lxp1, lxp2)::(combine lxp_list1 lxp_list2 f)) subst
+ | (Call _, _) -> Some ((subst, [(call, lxp)]))
+ | (_, _) -> None
+
+and _unify_susp (susp_: lexp) (lxp: lexp) (subst: substitution) : return_type =
+ match susp_ with
+ | Susp _ -> unify (unsusp_all susp_) lxp subst
+ | _ -> None
+
+(** Unify a Case with a lexp
+ * Case, Case -> try to unify
+ * Case, _ -> Constraint
*)
-and _unify_arrow (arrow: lexp) (lxp: lexp) (subst: substitution)
- : return_type =
- match (arrow, lxp) with
- | (Arrow (var_kind1, _, ltype1, _, lexp1), Arrow (var_kind2, _, ltype2, _, lexp2))
- -> if var_kind1 = var_kind2
- then _unify_inner ((ltype1, ltype2)::(lexp1, lexp2)::[]) subst
- (* _unify_inner_arrow ltype1 lexp1 ltype2 lexp2 subst *)
- else None
- | (Arrow _, Imm _) -> None
- | (Arrow _, Var _) -> Some (subst, [(arrow, lxp)]) (* FIXME Var can contain type ???*)
- | (Arrow _, _) -> unify lxp arrow subst
- (*| (Arrow _, Call _) -> None*) (* Call can return type (?) *)
+and _unify_case (case: lexp) (lxp: lexp) (subst: substitution) : return_type =
+ match case, lxp with
+ | (Case (_, lxp, lt11, lt12, smap, lxpopt), Case (_, lxp2, lt21, lt22, smap2, lxopt2))
+ -> ( match lxpopt, lxopt2 with
+ | Some l1, Some l2 -> (match _unify_inner ((lxp, lxp2)::(lt11, lt21)::(lt12, lt22)::(l1, l2)::[]) subst with
+ | Some (s, c) -> (match _unify_inner_case (List.combine (SMap.bindings smap) (SMap.bindings smap2)) s with
+ | Some (s', c') -> Some (s', c@c')
+ | None -> None)
+ | None -> None)
+ | _, _ -> None)
+ | (Case _, _) -> Some (subst, [(case, lxp)])
+ | (_, _) -> None
+
+(** Unify a Inductive and a lexp
+ * Inductive, Inductive -> try unify
+ * Inductive, Var -> constraint
+ * Inductive, Call/Metavar/Case/Let -> constraint
+ * Inductive, _ -> None*)
+and _unfiy_induct (induct: lexp) (lxp: lexp) (subst: substitution) : return_type =
+ match (induct, lxp) with
+ | (Inductive (_, lbl1, farg1, m1), Inductive (_, lbl2, farg2, m2)) when lbl1 = lbl2 ->
+ (match _unify_inner_induct_1 (List.combine farg1 farg2) subst with
+ | None -> None
+ | Some (s, c) -> (match (_unify_induct_sub_list (SMap.bindings m1) (SMap.bindings m2) s) with
+ | Some (s', c') -> Some (s', c@c')
+ | None -> None))
+ | (Inductive _, Var _) -> Some (subst, [(induct, lxp)])
| (_, _) -> None
-(** Unify lexp & ltype (Arrow (_,_,ltype, lexp)) of two Arrow*)
-and _unify_inner_arrow (lt1: lexp) (lxp1: lexp)
- (lt2: lexp) (lxp2: lexp) (subst: substitution): return_type =
- match unify lt1 lt2 subst with
- | Some (subst_, const) -> ( (*bracket for formating*)
- match unify lxp1 lxp2 subst_ with
- | Some (s, c) -> Some(s, const@c)
- | None -> None )
- | None -> None
+and _unify_sortlvl (sortlvl: lexp) (lxp: lexp) (subst: substitution) : return_type =
+ match sortlvl, lxp with
+ | (SortLevel s, SortLevel s2) -> (match s, s2 with
+ | SLn i, SLn j when i = j -> Some (subst, [])
+ | SLsucc l1, SLsucc l2 -> unify l1 l2 subst (* Is SLsucc some kind of linked list ? *)
+ | _, _ -> None)
+ | _, _ -> None
-(** Unify a Var and a lexp, if possible
- * (Var, Var) -> unify if they have the same debruijn index FIXME : shift indexes
- * (Var, Metavar) -> unify_metavar Metavar var subst
- * (_, _) -> None
+and _unify_sort (sort_: lexp) (lxp: lexp) (subst: substitution) : return_type =
+ match sort_, lxp with
+ | (Sort (_, srt), Sort (_, srt2)) -> (match srt, srt2 with
+ | Stype lxp1, Stype lxp2 -> unify lxp1 lxp2 subst
+ | StypeOmega, StypeOmega -> Some (subst, [])
+ | StypeLevel, StypeLevel -> Some (subst, [])
+ | _, _ -> None)
+ | Sort _, Var _ -> Some (subst, [(sort_, lxp)])
+ | _, _ -> None
+
+(************************ Helper function **************************************)
+
+(***** for Case *****)
+(** Check arg_king in (arg_kind * vdef option) list in Case *)
+and is_same arglist arglist2 =
+ match arglist, arglist2 with
+ | (akind, _)::t1, (akind2, _)::t2 when akind = akind2 -> is_same t1 t2
+ | [], [] -> true
+ | _, _ -> false
+
+(** try to unify the SMap part of the case *)
+and _unify_inner_case l s =
+ let rec _unify_inner_case l s =
+ match l with
+ | ((key, (_, arglist, lxp)), (key2, (_, arglist2, lxp2)))::t when key = key2 ->
+ (if is_same arglist arglist2 then ( match unify lxp lxp2 s with
+ | Some (s', c) -> (match _unify_inner_case l s' with
+ | Some (s_, c_) -> Some (s_, c@c_)
+ | None -> None)
+ | None -> None)
+ else None)
+ | [] -> Some (s, [])
+ | _ -> None
+ in _unify_inner_case l s
+
+
+(***** for Inductive *****)
+(*
+ Those part of Inductive :
+ * ((arg_kind * vdef * ltype) list) (* formal Args *)
+ * ((arg_kind * vdef option * ltype) list)
+ are almost identical except for the 'vdef option' (which is ignored) so the same function (_unify_inner_induct) should
+ work for those part, but it don't work because of 'vdef option'
*)
-and _unify_var (var: lexp) (r: lexp) (subst: substitution) : return_type =
- match (var, r) with
- | (Var (_, idx1), Var (_, idx2))
- -> if idx1 = idx2 then Some ((subst, []))
+(** for _unfiy_induct_sub_list*)
+and _unify_inner_induct_2 lst subst : return_type =
+ let test ((a1, _, l1), (a2, _, l2)) subst : return_type = if a1 = a2
+ then unify l1 l2 subst
else None
- | (Var _, Imm _) -> Some (subst, [(var, r)])(*FIXME : check for the value of Var -> need context ?*)
- | (Var _, _) -> unify r var subst (*returns to unify*)
- | (_, _) -> None
+ in
+ List.fold_left (fun a e -> (match a with
+ | Some (s, c) -> (match test e s with
+ | Some (s1, c1) -> Some (s1, c1@c)
+ | None -> Some (s, c))
+ | None -> test e subst)
+ ) None lst
-(** Unify two Imm if they match <=> Same type and same value
- * Add one of the Imm (the first arguement) to the substitution *)
-and _unify_imm (l: lexp) (r: lexp) (subst: substitution) : return_type =
- match (l, r) with
- | (Imm (String (_, v1)), Imm (String (_, v2)))
- -> if v1 = v2 then Some ((subst, []))
- else None
- | (Imm (Integer (_, v1)), Imm (Integer (_, v2)))
- -> if v1 = v2 then Some ((subst, []))
- else None
- | (Imm (Float (_, v1)), Imm (Float (_, v2)))
- -> if v1 = v2 then Some ((subst, []))
+(** for _unify_induct : unify the formal arg*)
+and _unify_inner_induct_1 lst subst : return_type =
+ let test ((a1, _, l1), (a2, _, l2)) subst : return_type = if a1 = a2
+ then unify l1 l2 subst
else None
- | (Imm _, Imm _) -> None
- | (Imm _, _) -> unify r l subst
- | (_, _) -> None
+ in
+ List.fold_left (fun a e -> (match a with
+ | Some (s, c) -> (match test e s with
+ | Some (s1, c1) -> Some (s1, c1@c)
+ | None -> Some (s, c))
+ | None -> test e subst)
+ ) None lst
-(** Unify a builtin (bltin) and a lexp (lxp) if it is possible
- * If the two arguments are builtin, unify based on name
- * If it's a Builtin and an other lexp, unify lexp part of Builtin with the lexp
-*)
-and _unify_builtin (bltin: lexp) (lxp: lexp) (subst: substitution) : return_type =
- match (bltin, lxp) with
- | (Builtin ((_, name1), _), Builtin ((_, name2),_))
- -> if name1 = name2 then Some ((subst, []))
- else None (* assuming that builtin have unique name *)
- | (Builtin (_, lxp_bltin), _) -> unify lxp_bltin lxp subst
- | (_, _) -> None
+(** unify the SMap of list in Inductive *)
+and _unify_induct_sub_list l1 l2 subst =
+ let test l1 l2 subst = match l1, l2 with
+ | (k1, v1)::t1, (k2, v2)::t2 when k1 = k2 -> (match _unify_inner_induct_2 (List.combine v1 v2) subst with
+ | Some (s, c) -> (match (_unify_induct_sub_list t1 t2 s) with
+ | Some (s1, c1) -> Some (s1, c1@c)
+ | None -> Some (s, c))
+ | None -> (_unify_induct_sub_list t1 t2 subst))
+ | _, _ -> None
+ in test l1 l2 subst
-(** Unify a Let (let_) and a lexp (lxp), if possible
- * Let , Let -> check the 'inside' of the let
- * Let , lexp -> constraint
-*)
-and _unify_let (let_: lexp) (lxp: lexp) (subst: substitution) : return_type =
- match (let_, lxp) with
- | (Let (_, m, lxp_), Let (_, m1, lxp2)) ->
- _unify_inner ((lxp_, lxp2)::(combine m m1)) subst
- | (Let _, _) -> Some (subst, [(let_, lxp)])
- | _, _ -> None
+(***** general *****)
(** take two list [(vdef * ltype * lexp), (vdef2 * ltype2 * lexp2)...]
map them to [ltype, lexp, ltype2, lexp2, ...]
and zip them to
[(ltype * ltype), (lexp * lexp), (ltype2 * ltype2), (lexp2 * lexp2), ...]
*)
-and combine list1 list2 =
- let l1 = List.fold_right (fun (_, t, x) acc -> t::x::acc) list1 []
- and l2 = List.fold_right (fun (_, t, x) acc -> t::x::acc) list2 []
- in List.combine l1 l2
-
and _unify_inner (lxp_l: (lexp * lexp) list) (subst: substitution) : return_type =
let merge ((s, c): (substitution * constraints))
(lxp_list: (lexp * lexp) list) : return_type =
=====================================
tests/macro_test.ml
=====================================
--- a/tests/macro_test.ml
+++ b/tests/macro_test.ml
@@ -66,5 +66,33 @@ let _ = (add_test "MACROS" "macros base" (fun () ->
)
+let _ = (add_test "MACROS" "macros decls" (fun () ->
+ reset_eval_trace ();
+
+ let dcode = "
+ decls-impl = lambda (x : List Sexp) ->
+ cons (node_ (symbol_ \"_=_\")
+ (cons (symbol_ \"a\") (cons (integer_ 1) nil)))
+ (cons (node_ (symbol_ \"_=_\")
+ (cons (symbol_ \"b\") (cons (integer_ 2) nil))) nil);
+
+ my-decls = Macro_ decls-impl;
+
+ my-decls Nat;" in
+
+ let rctx, lctx = eval_decl_str dcode lctx rctx in
+
+ let ecode = "a; b;" in
+
+ let ret = eval_expr_str ecode lctx rctx in
+
+ match ret with
+ | [Vint(a); Vint(b)] ->
+ if (a = 1 && b = 2) then success () else failure ()
+
+ | _ -> failure ())
+)
+
+
(* run all tests *)
let _ = run_all ()
=====================================
tests/unify_test.ml
=====================================
--- a/tests/unify_test.ml
+++ b/tests/unify_test.ml
@@ -71,7 +71,7 @@ let colored_string_of_lxp lxp lcol vcol =
| Var ((_, name), idx) -> (lcol "Var" ) ^ "(" ^ (vcol name ) ^ ", " ^ (vcol ("#" ^ (string_of_int idx))) ^ ")"
| Arrow (_, _, a, _, b) -> (lcol "Arrow(") ^ (vcol (string_of_lxp a)) ^ " => " ^ (vcol (string_of_lxp b)) ^ ")"
| Lambda (_,(_, name), dcl, body) -> (lcol "Lambda") ^ "(" ^ (vcol name) ^ " : " ^ (vcol (string_of_lxp dcl))
- ^ " => (" ^ (vcol (string_of_lxp body)) ^ ") )"
+ ^ " => (" ^ (vcol (string_of_lxp body)) ^ "))"
| Metavar (value, (_, name)) -> (lcol "Metavar" ) ^ "(" ^ (vcol (string_of_int value)) ^ ", " ^ (vcol name) ^ ")"
| Call (_) -> (lcol "Call(...)" )
| Case _ -> (lcol "Case") ^ "(...)"
=====================================
w_file deleted
=====================================
--- a/w_file
+++ /dev/null
View it on GitLab: https://gitlab.com/monnier/typer/compare/674cb6429529361ee34a2c26abe59ab876…
1
0
Setepenre pushed to branch master at Stefan / Typer
Commits:
f530a2dd by Pierre Delaunay at 2016-06-26T11:23:25-04:00
Moved builtin macro implementation
Changes to be committed:
* btl/types.typer: change type of some accessors
* src/builtin.ml :
- fix predef shifting
- moved builtin macro implementation there
* src/debruijn.ml: remove dead code
* src/lparse.ml
- builtin macro are now recognized inside (handle_macro_call)
- - - - -
6 changed files:
- .travis.yml
- btl/types.typer
- src/builtin.ml
- src/debruijn.ml
- src/eval.ml
- src/lparse.ml
Changes:
=====================================
.travis.yml
=====================================
--- a/.travis.yml
+++ b/.travis.yml
@@ -8,7 +8,7 @@ sudo: true
before_script:
- sudo apt-get -qq update
- sudo apt-get install opam
- - opam init
+ - opam init --auto-setup
- opam config setup -a
- opam config env
=====================================
btl/types.typer
=====================================
--- a/btl/types.typer
+++ b/btl/types.typer
@@ -151,13 +151,13 @@ read = Built-in "read" (FileHandle -> Int -> IO String);
% -----------------------------------------------------
Attribute = Built-in "Attribute";
-new-attribute = Built-in "new-attribute" (Type -> Attribute);
+new-attribute = Built-in "new-attribute" (Macro);
-add-attribute = Built-in "add-attribute" (Sexp -> Sexp -> Sexp -> List Sexp);
+add-attribute = Built-in "add-attribute" (Macro);
attribute = Macro_ add-attribute;
get-attribute = Built-in "get-attribute" Macro;
-has-attribute = Built-in "has-attribute" (String -> Attribute -> Bool);
+has-attribute = Built-in "has-attribute" (Macro);
% -----------------------------------------------------
% Context Accessors
=====================================
src/builtin.ml
=====================================
--- a/src/builtin.ml
+++ b/src/builtin.ml
@@ -52,7 +52,10 @@ type predef_table = (lexp option ref) SMap.t
let predef_name = [
"cons";
"nil";
- "Unit"
+ "Unit";
+ "True";
+ "False";
+ "Bool";
]
let builtin_size = ref 0
@@ -62,11 +65,17 @@ let predef_map : predef_table =
List.fold_left (fun m name ->
SMap.add name (ref None) m) SMap.empty predef_name
-let get_predef name =
+let get_predef_raw (name: string) : lexp =
match !(SMap.find name predef_map) with
| Some exp -> exp
| None -> builtin_error dloc "Try to access an empty predefined"
+let get_predef name ctx =
+ let r = (get_size ctx) - !builtin_size in
+ let v = mkSusp (get_predef_raw name) (S.shift r) in
+ v
+
+
let set_predef name lexp =
SMap.find name predef_map := lexp
@@ -272,16 +281,6 @@ let write_impl loc depth args_val ctx =
fprintf channel "%s" msg;
Vdummy
-
-(*
- * Should we have a function that
- * -> returns a new context inside typer ? (So we need to add a ctx type too)
- * -> returns current context ?
- * -> pexp_eval expr
- * -> lexp_eval expr
- * -> ou seulement: 'eval expr ctx'
- *)
-
let is_lbuiltin idx ctx =
let bsize = 1 in
let csize = get_size ctx in
@@ -290,3 +289,85 @@ let is_lbuiltin idx ctx =
true
else
false
+
+(* --------------------------------------------------------------------------
+ * Built-in Macro
+ * -------------------------------------------------------------------------- *)
+
+(* Those are function that are evaluated during lexp_parse *)
+
+let get_attribute_impl loc largs ctx ftype =
+
+ let (vi, vn), (ai, an) = match largs with
+ | [Var((_, vn), vi); Var((_, an), ai)] -> (vi, vn), (ai, an)
+ | _ -> builtin_error loc "get-attribute expects two arguments" in
+
+ let lxp = get_property ctx (vi, vn) (ai, an) in
+ let ltype = env_lookup_expr ctx ((loc, an), ai) in
+ lxp, ltype
+
+let new_attribute_impl loc largs ctx ftype =
+
+ let eltp = match largs with
+ | [eltp] -> eltp
+ | _ -> builtin_warning loc "new-attribute expects one argument"; type0 in
+
+ eltp, ftype
+
+let has_attribute_impl loc largs ctx ftype =
+
+ let (vi, vn), (ai, an) = match largs with
+ | [Var((_, vn), vi); Var((_, an), ai)] -> (vi, vn), (ai, an)
+ | _ -> builtin_error loc "has-attribute expects two arguments" in
+
+ let b = has_property ctx (vi, vn) (ai, an) in
+
+ let rvar = if b then get_predef "True" ctx else get_predef "False" ctx in
+ rvar, (get_predef "Bool" ctx)
+
+let declexpr_impl loc largs ctx ftype =
+
+ let (vi, vn) = match largs with
+ | [Var((_, vn), vi)] -> (vi, vn)
+ | _ -> builtin_error loc "declexpr expects one argument" in
+
+ let lxp = env_lookup_expr ctx ((loc, vn), vi) in
+ let ltp = env_lookup_type ctx ((loc, vn), vi) in
+ lxp, ftype
+
+
+let decltype_impl loc largs ctx ftype =
+
+ let (vi, vn) = match largs with
+ | [Var((_, vn), vi)] -> (vi, vn)
+ | _ -> builtin_error loc "decltype expects one argument" in
+
+ let ltype = env_lookup_type ctx ((loc, vn), vi) in
+ (* mkSusp prop (S.shift (var_i + 1)) *)
+ ltype, type0
+
+let builtin_macro = [
+ ("decltype", decltype_impl);
+ ("declexpr", declexpr_impl);
+ ("get-attribute", get_attribute_impl);
+ ("new-attribute", new_attribute_impl);
+ ("has-attribute", has_attribute_impl);
+]
+
+type macromap =
+ (location -> lexp list -> lexp_context -> lexp -> (lexp * lexp)) SMap.t
+
+let macro_impl_map : macromap =
+ List.fold_left (fun map (name, funct) ->
+ SMap.add name funct map) SMap.empty builtin_macro
+
+let get_macro_impl loc name =
+ try SMap.find name macro_impl_map
+ with Not_found -> builtin_error loc ("Builtin macro" ^ name ^ " not found")
+
+let is_builtin_macro name =
+ try SMap.find name macro_impl_map; true
+ with Not_found -> false
+
+
+
=====================================
src/debruijn.ml
=====================================
--- a/src/debruijn.ml
+++ b/src/debruijn.ml
@@ -123,20 +123,6 @@ let _name_error loc estr str =
debruijn_error loc ("DeBruijn index refers to wrong name. " ^
"Expected: \"" ^ estr ^ "\" got \"" ^ str ^ "\"")
-(*
-let env_set_var_info ctx (def: vref) (v: lexp option) (t: lexp) =
- let ((dv_size, _), info_env, _) = ctx in
- let ((loc, ename), dbi) = def in
-
- try(let rf = (Myers.nth dbi info_env) in
- let (_, (_, name), _, _) = !rf in
-
- (* Check if names match *)
- _name_error loc ename name;
-
- rf := (0, (loc, ename), v, t))
- with
- Not_found -> debruijn_error loc "DeBruijn index out of bounds!" *)
(* generic lookup *)
let _env_lookup ctx (v: vref): env_elem =
@@ -284,15 +270,3 @@ let dump_properties ctx =
print_string (make_sep '-');
-
-
-
-
-
-
-
-
-
-
-
-
=====================================
src/eval.ml
=====================================
--- a/src/eval.ml
+++ b/src/eval.ml
@@ -84,7 +84,7 @@ let rec _eval lxp ctx i: (value_type) =
| Lambda ((_, n), lxp) -> Closure(n, lxp, ctx)
| Builtin ((_, str)) -> Vbuiltin(str)
- (* Return a value stored in env *)
+ (* Return a value stored in env *)
| Var((loc, name), idx) as e ->
eval_var ctx e ((loc, name), idx)
@@ -101,13 +101,12 @@ let rec _eval lxp ctx i: (value_type) =
| Case (loc, target, pat, dflt)
-> (eval_case ctx i loc target pat dflt)
- | _ -> print_string "debug catch-all eval: ";
- elexp_print lxp; print_string "\n"; Vdummy
+ | Type -> Vcons((tloc, "Unit"), [])
and get_predef_eval name ctx =
let r = (get_rte_size ctx) - !builtin_size in
- let v = mkSusp (get_predef name) (S.shift r) in
+ let v = mkSusp (get_predef_raw name) (S.shift r) in
_eval (erase_type v) ctx 0
and eval_var ctx lxp v =
@@ -250,7 +249,7 @@ and bind_impl loc depth args_val ctx =
| Vcommand (cmd) -> cmd
| _ -> builtin_error loc "bind first arguments must be a monad" in
- (* bind return another Vcommand *)
+ (* bind returns another Vcommand *)
Vcommand (fun () ->
(* get callback *)
let body, ctx = match cb with
=====================================
src/lparse.ml
=====================================
--- a/src/lparse.ml
+++ b/src/lparse.ml
@@ -456,52 +456,60 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i =
Call(vf, new_args), ltp in
let handle_macro_call (loc, name) =
- (* look up for definition *)
- let idx = try senv_lookup name ctx
- with Not_found ->
- lexp_fatal loc ("Could not find Variable: " ^ name) in
-
- (* Get the macro *)
- let lxp = try env_lookup_expr ctx ((loc, name), idx)
- with Not_found ->
- lexp_fatal loc (name ^ " was found but " ^ (string_of_int idx) ^
- " is not a correct index.") in
-
- let lxp = match unsusp_all lxp with
- | Call(Var((_, "Macro_"), _), [(_, fct)]) -> fct
- | _ ->
- print_string "\n";
- print_string (lexp_to_string lxp); print_string "\n";
- lexp_print lxp; print_string "\n";
- lexp_fatal loc "Macro is ill formed" in
-
- (* Build function to be called *)
- let arg = olist2tlist_lexp sargs ctx in
-
- let lxp = Call(lxp, [(Aexplicit, arg)]) in
- let elexp = EL.erase_type lxp in
- let rctx = (from_lctx ctx 0) in
-
- _global_eval_trace := [];
-
- let vxp = try eval elexp rctx
- with e ->
- print_eval_trace ();
- raise e in
-
- let sxp = match vxp with
- | Vsexp(sxp) -> sxp
- (* Those are sexp converted by the eval function *)
- | Vint(i) -> Integer(dloc, i)
- | Vstring(s) -> String(dloc, s)
- | Vfloat(f) -> Float(dloc, f)
- (* I have vdum here WHY *)
- | v -> debug_msg (value_print v);
- lexp_fatal loc "Macro_ expects '(List Sexp) -> Sexp'" in
+ (* check for builtin *)
+ match is_builtin_macro name with
+ | true ->
+ let pargs = List.map pexp_parse sargs in
+ let largs = _lexp_parse_all pargs ctx i in
+ (get_macro_impl loc name) loc largs ctx ltp
+ (* user defined macro *)
+ | false ->(
+ (* look up for definition *)
+ let idx = try senv_lookup name ctx
+ with Not_found ->
+ lexp_fatal loc ("Could not find Variable: " ^ name) in
- let pxp = pexp_parse sxp in
- _lexp_p_infer pxp ctx (i + 1) in
+ (* Get the macro *)
+ let lxp = try env_lookup_expr ctx ((loc, name), idx)
+ with Not_found ->
+ lexp_fatal loc (name ^ " was found but " ^ (string_of_int idx) ^
+ " is not a correct index.") in
+
+ let lxp = match unsusp_all lxp with
+ | Call(Var((_, "Macro_"), _), [(_, fct)]) -> fct
+ | _ ->
+ print_string "\n";
+ print_string (lexp_to_string lxp); print_string "\n";
+ lexp_print lxp; print_string "\n";
+ lexp_fatal loc "Macro is ill formed" in
+
+ (* Build function to be called *)
+ let arg = olist2tlist_lexp sargs ctx in
+
+ let lxp = Call(lxp, [(Aexplicit, arg)]) in
+ let elexp = EL.erase_type lxp in
+ let rctx = (from_lctx ctx 0) in
+
+ _global_eval_trace := [];
+
+ let vxp = try eval elexp rctx
+ with e ->
+ print_eval_trace ();
+ raise e in
+
+ let sxp = match vxp with
+ | Vsexp(sxp) -> sxp
+ (* Those are sexp converted by the eval function *)
+ | Vint(i) -> Integer(dloc, i)
+ | Vstring(s) -> String(dloc, s)
+ | Vfloat(f) -> Float(dloc, f)
+ (* I have vdum here WHY *)
+ | v -> debug_msg (value_print v);
+ lexp_fatal loc "Macro_ expects '(List Sexp) -> Sexp'" in
+
+ let pxp = pexp_parse sxp in
+ _lexp_p_infer pxp ctx (i + 1)) in
(* determine function type *)
match fun_name, ltp with
@@ -513,59 +521,8 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i =
let new_args = List.map (fun g -> (Aexplicit, g)) largs in
Call(body, new_args), ltp
- (* Context acessor *)
- | Pvar(l, "decltype"), _ ->
- let pargs = List.map pexp_parse sargs in
- let largs = _lexp_parse_all pargs ctx i in
- let (vi, vn) = match largs with
- | [Var((_, vn), vi)] -> (vi, vn)
- | _ -> lexp_fatal l "decltype expects one argument" in
-
- let ltype = env_lookup_type ctx ((dloc, vn), vi) in
- (* mkSusp prop (S.shift (var_i + 1)) *)
- ltype, dltype
-
- | Pvar(l, "declexpr"), _ ->
- let pargs = List.map pexp_parse sargs in
- let largs = _lexp_parse_all pargs ctx i in
- let (vi, vn) = match largs with
- | [Var((_, vn), vi)] -> (vi, vn)
- | _ -> lexp_fatal l "declexpr expects one argument" in
-
- let lxp = env_lookup_expr ctx ((dloc, vn), vi) in
- let ltp = env_lookup_type ctx ((dloc, vn), vi) in
- lxp, ltp
-
- (* attributes are special case they does not exist after lexp_parsing
- * in that respect they are quite similar to macros *)
- | Pvar(l, "get-attribute"), _ ->
- let pargs = List.map pexp_parse sargs in
- let largs = _lexp_parse_all pargs ctx i in
- let (vi, vn), (ai, an) = match largs with
- | [Var((_, vn), vi); Var((_, an), ai)] -> (vi, vn), (ai, an)
- | _ -> lexp_fatal l "get-attribute expects two arguments" in
-
- let lxp = get_property ctx (vi, vn) (ai, an) in
- let ltype = env_lookup_expr ctx ((dloc, an), ai) in
- lxp, ltype
-
- (*
- | Pvar(l, "has-attribute"), _ -> *)
-
-
- | Pvar(l, "new-attribute"), _ ->
- let pargs = List.map pexp_parse sargs in
- let largs = _lexp_parse_all pargs ctx i in
-
- let eltp = match largs with
- | [eltp] -> eltp
- | _ -> lexp_warning l "new-attribute expects one argument";
- dltype in
-
- eltp, ltp
-
| (Pvar (l, n), Var((_, "Macro"), _)) ->
- (* FIXME: check db_idx points too a Macro type *)
+ (* FIXME: check db_idx points to a Macro type *)
handle_macro_call (l, n)
(* Call to Vanilla or constructor *)
@@ -1032,8 +989,7 @@ let default_lctx =
try
List.iter (fun name ->
let idx = senv_lookup name lctx in
- let v = Var((dloc, name), idx) in (*
- let value = (env_lookup_expr lctx v) in *)
+ let v = Var((dloc, name), idx) in
set_predef name (Some v)) predef_name;
(* -- DONE -- *)
lctx
View it on GitLab: https://gitlab.com/monnier/typer/commit/f530a2dd9a0dcf5222be0c4966f3690239d…
1
0
[Git][monnier/typer][master] Context accessors and Monad handling. modified travis script
by Setepenre 26 Jui '16
by Setepenre 26 Jui '16
26 Jui '16
Setepenre pushed to branch master at Stefan / Typer
Commits:
642376ae by Pierre Delaunay at 2016-06-25T18:16:01-04:00
Context accessors and Monad handling. modified travis script
Changes to be committed:
*.travis.yml
* src/debruijn.ml:
- new function (get_attribute)
- new function (has_attribute)
- modify calling convention of (add_attribute) (better consistency)
* btl/types.typer
- added builtin context accessors (decltype) and (declexpr)
* src/eval.ml
- fix monad handling
* src/lparse.ml
- added context accessor as builtin macro
- - - - -
9 changed files:
- − -
- .travis.yml
- btl/types.typer
- src/builtin.ml
- src/debruijn.ml
- src/env.ml
- src/eval.ml
- src/lparse.ml
- − w_file
Changes:
=====================================
- deleted
=====================================
--- a/-
+++ /dev/null
=====================================
.travis.yml
=====================================
--- a/.travis.yml
+++ b/.travis.yml
@@ -3,16 +3,11 @@ language: ocaml
env:
- OCAML_VERSION=4.02
-addons:
- apt:
- packages:
- - opam
-
-before_script:
- - opam config setup -a
- - opam config env
+sudo: true
before_script:
+ - sudo apt-get -qq update
+ - sudo apt-get install opam
- opam config setup -a
- opam config env
=====================================
btl/types.typer
=====================================
--- a/btl/types.typer
+++ b/btl/types.typer
@@ -27,6 +27,7 @@
%*
%* Description:
%* Define builtin types and functions
+%* This file MUST be correctly typed
%*
%* ---------------------------------------------------------------------------
@@ -34,12 +35,14 @@
% Base Types
% -----------------------------------------------------
-Type = Built-in "Type";
-Int = Built-in "Int";
-Float = Built-in "Float";
-String = Built-in "String";
-Sexp = Built-in "Sexp";
-Unit = Built-in "Unit";
+Type = Built-in "Type";
+Int = Built-in "Int";
+Float = Built-in "Float";
+String = Built-in "String";
+Sexp = Built-in "Sexp";
+
+Unit = Built-in "Unit"; % Nothing
+Context = Built-in "Context"; % Lexp Context
% Basic operators
_+_ = Built-in "_+_" (Int -> Int -> Int);
@@ -151,12 +154,17 @@ Attribute = Built-in "Attribute";
new-attribute = Built-in "new-attribute" (Type -> Attribute);
add-attribute = Built-in "add-attribute" (Sexp -> Sexp -> Sexp -> List Sexp);
+attribute = Macro_ add-attribute;
+get-attribute = Built-in "get-attribute" (String -> Attribute);
+has-attribute = Built-in "has-attribute" (String -> Attribute -> Bool);
+% -----------------------------------------------------
+% Context Accessors
+% -----------------------------------------------------
-
-
-
+decltype = Built-in "decltype" Macro;
+declexpr = Built-in "declexpr" Macro;
=====================================
src/builtin.ml
=====================================
--- a/src/builtin.ml
+++ b/src/builtin.ml
@@ -243,12 +243,12 @@ let open_impl loc args_val ctx =
| [Vstring(file_name); Vstring(mode)] -> file_name, mode
| _ -> builtin_error loc "open expects 2 strings" in
- (* open file *) (* return a file handle *)
- match mode with
- | "r" -> Vin(open_in file)
- | "w" -> Vout(open_out file)
- | _ -> builtin_error loc "wrong open mode"
-
+ (* open file *) (* return a file handle *)
+ Vcommand(fun () ->
+ match mode with
+ | "r" -> Vin(open_in file)
+ | "w" -> Vout(open_out file)
+ | _ -> builtin_error loc "wrong open mode")
let read_impl loc args_val ctx =
@@ -256,7 +256,7 @@ let read_impl loc args_val ctx =
| [Vin(c); _] -> c
| _ ->
List.iter (fun v -> value_print v; print_string "\n") args_val;
- builtin_error loc "read expects a in_channel" in
+ builtin_error loc "read expects an in_channel" in
let line = input_line channel in
Vstring(line)
@@ -267,15 +267,11 @@ let write_impl loc args_val ctx =
| [Vout(c); Vstring(msg)] -> c, msg
| _ ->
List.iter (fun v -> value_print v) args_val;
- builtin_error loc "read expects a out_channel" in
+ builtin_error loc "read expects an out_channel" in
fprintf channel "%s" msg;
Vdummy
-let new_attribute loc args_val ctx =
- builtin_warning loc "new-attributes to be implemented";
- Vdummy
-
(*
* Should we have a function that
=====================================
src/debruijn.ml
=====================================
--- a/src/debruijn.ml
+++ b/src/debruijn.ml
@@ -158,7 +158,7 @@ let _env_lookup ctx (v: vref): env_elem =
let env_lookup_type ctx (v : vref): lexp =
let (_, idx) = v in
let (_, _, _, ltp) = _env_lookup ctx v in
- mkSusp ltp (S.shift (idx + 1))
+ mkSusp ltp (S.shift (idx + 0))
let env_lookup_expr ctx (v : vref): lexp =
let (_, idx) = v in
@@ -208,7 +208,7 @@ let replace_by ctx name by =
(* -------------------------------------------------------------------------- *)
-let add_property ctx (var_n, var_i) (att_n, att_i) (prop: lexp)
+let add_property ctx (var_i, var_n) (att_i, att_n) (prop: lexp)
: lexp_context =
let (a, b, property_map) = ctx in
@@ -226,6 +226,31 @@ let add_property ctx (var_n, var_i) (att_n, att_i) (prop: lexp)
(a, b, property_map)
+let get_property ctx (var_i, var_n) (att_i, att_n): lexp =
+ let (a, b, property_map) = ctx in
+ let n = get_size ctx in
+
+ (* /!\ input index are reversed or not ? I think not so I shift them *)
+ let pmap = try PropertyMap.find (n - var_i, var_n) property_map
+ with Not_found ->
+ debruijn_error dummy_location ("Variable \"" ^ var_n ^ "\" does not have any properties") in
+
+ let prop = try PropertyMap.find (n - att_i, att_n) pmap
+ with Not_found ->
+ debruijn_error dummy_location ("Property \"" ^ att_n ^ "\" not found") in
+ mkSusp prop (S.shift (var_i + 1))
+
+
+let has_property ctx (var_i, var_n) (att_i, att_n): bool =
+ let (a, b, property_map) = ctx in
+ let n = get_size ctx in
+
+ try
+ let pmap = PropertyMap.find (n - var_i, var_n) property_map in
+ let prop = PropertyMap.find (n - att_i, att_n) pmap in
+ true
+ with Not_found -> false
+
let dump_properties ctx =
let (a, b, property_map) = ctx in
=====================================
src/env.ml
=====================================
--- a/src/env.ml
+++ b/src/env.ml
@@ -49,6 +49,7 @@ let env_error loc msg =
let str_idx idx = "[" ^ (string_of_int idx) ^ "]"
+
type value_type =
| Vint of int
| Vstring of string
@@ -61,7 +62,8 @@ type value_type =
| Vdummy
| Vin of in_channel
| Vout of out_channel
- | Vbind of elexp list
+ | Vcommand of (unit -> value_type)
+
let rec value_print (vtp: value_type) =
match vtp with
@@ -81,11 +83,7 @@ let rec value_print (vtp: value_type) =
| Vdummy -> print_string "value_print_dummy"
| Vin _ -> print_string "in_channel"
| Vout _ -> print_string "out_channel"
- | Vbind [a; b] -> print_string "bind (";
- elexp_print a; print_string ") (";
- elexp_print b; print_string ")";
-
- | Vbind _ -> print_string "bind"
+ | Vcommand _ -> print_string "command"
(* | _ -> print_string "debug print" *)
let value_location (vtp: value_type) =
@@ -108,7 +106,7 @@ let value_name v =
| Vdummy -> "Vdummy"
| Vin _ -> "Vin"
| Vout _ -> "Vout"
- | Vbind _ -> "Vbind"
+ | Vcommand _ -> "Vcommand"
(* Runtime Environ *)
type env_cell = (string option * value_type) ref
=====================================
src/eval.ml
=====================================
--- a/src/eval.ml
+++ b/src/eval.ml
@@ -102,7 +102,7 @@ let rec _eval lxp ctx i: (value_type) =
-> (eval_case ctx i loc target pat dflt)
| _ -> print_string "debug catch-all eval: ";
- elexp_print lxp; print_string "\n"; Vstring("eval Not Implemented")
+ elexp_print lxp; print_string "\n"; Vdummy
and get_predef_eval name ctx =
@@ -144,12 +144,8 @@ and eval_call ctx i lname eargs =
eval_error loc "Cannot eval function" in
(* eval function here *)
- match f with
- (* Does not eval args *)
- | Vbuiltin ("bind") -> Vbind eargs
- | _ ->
- let args = List.map (fun e -> _eval e ctx (i + 1)) eargs in
- eval_call f args ctx
+ let args = List.map (fun e -> _eval e ctx (i + 1)) eargs in
+ eval_call f args ctx
and eval_case ctx i loc target pat dflt =
(* Eval target *)
@@ -249,30 +245,42 @@ and bind_impl loc args_val ctx =
| [io; callback] -> io, callback
| _ -> builtin_error loc "bind expects two arguments" in
+ (* build Vcommand from io function *)
+ let cmd = match io with
+ | Vcommand (cmd) -> cmd
+ | _ -> builtin_error loc "bind first arguments must be a monad" in
+
+ (* bind return another Vcommand *)
+ Vcommand (fun () ->
(* get callback *)
- let body, ctx = match cb with
- | Closure(_, body, ctx) -> body, ctx
- | _ -> builtin_error loc "A Closure was expected" in
+ let body, ctx = match cb with
+ | Closure(_, body, ctx) -> body, ctx
+ | _ -> builtin_error loc "A Closure was expected" in
+
+ (* run given command *)
+ let underlying = cmd () in
(* add evaluated IO to arg list *)
- let nctx = add_rte_variable None io ctx in
+ let nctx = add_rte_variable None underlying ctx in
(* eval callback *)
- _eval body nctx 0
+ _eval body nctx 0)
and run_io loc args_val ctx =
- let io, callback = match args_val with
- | [Vbind([io; callback])] -> io, callback
- | _ -> builtin_error loc "run-io expects a single Vbind argument" in
+ let io, ltp = match args_val with
+ | [io; ltp] -> io, ltp
+ | _ -> builtin_error loc "run-io expects 2 arguments" in
+
+ let cmd = match io with
+ | Vcommand (cmd) -> cmd
+ | _ -> builtin_error loc "run-io expects a monad as first argument" in
- (* eval args *)
- let io = _eval io ctx 0 in
- let callback = _eval callback ctx 0 in
+ (* run given command *)
+ let _ = cmd () in
- (* eval bind *)
- let a = bind_impl loc [io; callback] ctx in
- get_predef_eval "Unit" ctx
+ (* return given type *)
+ ltp
and typer_eval loc args ctx =
let arg = match args with
=====================================
src/lparse.ml
=====================================
--- a/src/lparse.ml
+++ b/src/lparse.ml
@@ -513,7 +513,46 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i =
let new_args = List.map (fun g -> (Aexplicit, g)) largs in
Call(body, new_args), ltp
- (* attribute *)
+ (* Context acessor *)
+ | Pvar(l, "decltype"), _ ->
+ let pargs = List.map pexp_parse sargs in
+ let largs = _lexp_parse_all pargs ctx i in
+ let (vi, vn) = match largs with
+ | [Var((_, vn), vi)] -> (vi, vn)
+ | _ -> lexp_fatal l "decltype expects one argument" in
+
+ let ltype = env_lookup_type ctx ((dloc, vn), vi) in
+ (* mkSusp prop (S.shift (var_i + 1)) *)
+ ltype, dltype
+
+ | Pvar(l, "declexpr"), _ ->
+ let pargs = List.map pexp_parse sargs in
+ let largs = _lexp_parse_all pargs ctx i in
+ let (vi, vn) = match largs with
+ | [Var((_, vn), vi)] -> (vi, vn)
+ | _ -> lexp_fatal l "declexpr expects one argument" in
+
+ let lxp = env_lookup_expr ctx ((dloc, vn), vi) in
+ let ltp = env_lookup_type ctx ((dloc, vn), vi) in
+ lxp, ltp
+
+ (* attributes are special case they does not exist after lexp_parsing
+ * in that respect they are quite similar to macros *)
+ | Pvar(l, "get-attribute"), _ ->
+ let pargs = List.map pexp_parse sargs in
+ let largs = _lexp_parse_all pargs ctx i in
+ let (vi, vn), (ai, an) = match largs with
+ | [Var((_, vn), vi); Var((_, an), ai)] -> (vi, vn), (ai, an)
+ | _ -> lexp_fatal l "get-attribute expects two arguments" in
+
+ let lxp = get_property ctx (vi, vn) (ai, an) in
+ let ltype = env_lookup_expr ctx ((dloc, an), ai) in
+ lxp, ltype
+
+ (*
+ | Pvar(l, "has-attribute"), _ -> *)
+
+
| Pvar(l, "new-attribute"), _ ->
let pargs = List.map pexp_parse sargs in
let largs = _lexp_parse_all pargs ctx i in
@@ -660,7 +699,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * lexp_context) =
(* extract info *)
let var, att, fn = match largs with
- | [Var((_, vn), vi); Var((_, an), ai); fn] -> (vn, vi), (an, ai), fn
+ | [Var((_, vn), vi); Var((_, an), ai); fn] -> (vi, vn), (ai, an), fn
| _ -> lexp_fatal loc "add-attribute expects 3 args" in
let ctx = add_property ctx var att fn in
=====================================
w_file deleted
=====================================
--- a/w_file
+++ /dev/null
View it on GitLab: https://gitlab.com/monnier/typer/commit/642376aeff2e3cf8d5fc0d8685406009f6d…
3
3
25 Jui '16
Setepenre pushed to branch master at Stefan / Typer
Commits:
d5da7869 by Pierre Delaunay at 2016-06-25T18:35:09-04:00
new calling convention for builtin functions
(location -> int -> value_type list -> runtime_env -> value_type)
^~~~^ new
This allows us to have a more accurate call trace when eval
is called inside a builtin-function.
Changes to be committed:
* btl/types.typer
* src/builtin.ml
* src/eval.ml
- - - - -
4 changed files:
- .travis.yml
- btl/types.typer
- src/builtin.ml
- src/eval.ml
Changes:
=====================================
.travis.yml
=====================================
--- a/.travis.yml
+++ b/.travis.yml
@@ -8,6 +8,7 @@ sudo: true
before_script:
- sudo apt-get -qq update
- sudo apt-get install opam
+ - opam init
- opam config setup -a
- opam config env
=====================================
btl/types.typer
=====================================
--- a/btl/types.typer
+++ b/btl/types.typer
@@ -153,10 +153,10 @@ read = Built-in "read" (FileHandle -> Int -> IO String);
Attribute = Built-in "Attribute";
new-attribute = Built-in "new-attribute" (Type -> Attribute);
-add-attribute = Built-in "add-attribute" (Sexp -> Sexp -> Sexp -> List Sexp);
+add-attribute = Built-in "add-attribute" (Sexp -> Sexp -> Sexp -> List Sexp);
attribute = Macro_ add-attribute;
-get-attribute = Built-in "get-attribute" (String -> Attribute);
+get-attribute = Built-in "get-attribute" Macro;
has-attribute = Built-in "has-attribute" (String -> Attribute -> Bool);
% -----------------------------------------------------
=====================================
src/builtin.ml
=====================================
--- a/src/builtin.ml
+++ b/src/builtin.ml
@@ -97,7 +97,7 @@ let type_float = Builtin((dloc, "Float"), type0)
let type_string = Builtin((dloc, "String"), type0)
(* Builtin of builtin * string * ltype *)
-let _generic_binary_iop name f loc (args_val: value_type list)
+let _generic_binary_iop name f loc (depth: int) (args_val: value_type list)
(ctx: runtime_env) =
let l, r = match args_val with
@@ -117,11 +117,11 @@ let idiv_impl = _generic_binary_iop "Integer::div" (fun a b -> a / b)
(* loc is given by the compiler *)
-let none_fun : (location -> value_type list -> runtime_env -> value_type)
+let none_fun : (location -> int -> value_type list -> runtime_env -> value_type)
= (fun loc args_val ctx ->
builtin_error loc "Requested Built-in was not implemented")
-let make_symbol loc args_val ctx =
+let make_symbol loc depth args_val ctx =
(* symbol is a simple string *)
let lxp = match args_val with
| [r] -> r
@@ -166,7 +166,7 @@ let rec tlist2olist acc expr =
builtin_error dloc "List conversion failure'"
-let make_node loc args_val ctx =
+let make_node loc depth args_val ctx =
let op, tlist = match args_val with
| [Vsexp(op); lst] -> op, lst
@@ -190,7 +190,7 @@ let make_node loc args_val ctx =
Vsexp(Node(op, s))
-let make_string loc args_val ctx =
+let make_string loc depth args_val ctx =
let lxp = match args_val with
| [r] -> r
| _ -> builtin_error loc ("string_ expects 1 argument") in
@@ -199,7 +199,7 @@ let make_string loc args_val ctx =
| Vstring(str) -> Vsexp(String(loc, str))
| _ -> builtin_error loc ("string_ expects one string as argument")
-let make_integer loc args_val ctx =
+let make_integer loc depth args_val ctx =
let lxp = match args_val with
| [r] -> r
| _ -> builtin_error loc ("integer_ expects 1 argument") in
@@ -208,24 +208,24 @@ let make_integer loc args_val ctx =
| Vint(str) -> Vsexp(Integer(loc, str))
| _ -> builtin_error loc ("integer_ expects one string as argument")
-let make_float loc args_val ctx = Vdummy
-let make_block loc args_val ctx = Vdummy
+let make_float loc depth args_val ctx = Vdummy
+let make_block loc depth args_val ctx = Vdummy
let ttrue = Vcons((dloc, "True"), [])
let tfalse = Vcons((dloc, "False"), [])
let btyper b = if b then ttrue else tfalse
-let string_eq loc args_val ctx =
+let string_eq loc depth args_val ctx =
match args_val with
| [Vstring(s1); Vstring(s2)] -> btyper (s1 = s2)
| _ -> builtin_error loc "string_eq expects 2 strings"
-let int_eq loc args_val ctx =
+let int_eq loc depth args_val ctx =
match args_val with
| [Vint(s1); Vint(s2)] -> btyper (s1 = s2)
| _ -> builtin_error loc "int_eq expects 2 integer"
-let sexp_eq loc args_val ctx =
+let sexp_eq loc depth args_val ctx =
match args_val with
| [Vsexp(s1); Vsexp(s2)] -> (
match s1, s2 with
@@ -237,7 +237,7 @@ let sexp_eq loc args_val ctx =
| _ -> builtin_error loc "int_eq expects 2 sexp"
-let open_impl loc args_val ctx =
+let open_impl loc depth args_val ctx =
let file, mode = match args_val with
| [Vstring(file_name); Vstring(mode)] -> file_name, mode
@@ -250,7 +250,7 @@ let open_impl loc args_val ctx =
| "w" -> Vout(open_out file)
| _ -> builtin_error loc "wrong open mode")
-let read_impl loc args_val ctx =
+let read_impl loc depth args_val ctx =
let channel = match args_val with
| [Vin(c); _] -> c
@@ -261,7 +261,7 @@ let read_impl loc args_val ctx =
let line = input_line channel in
Vstring(line)
-let write_impl loc args_val ctx =
+let write_impl loc depth args_val ctx =
let channel, msg = match args_val with
| [Vout(c); Vstring(msg)] -> c, msg
=====================================
src/eval.ml
=====================================
--- a/src/eval.ml
+++ b/src/eval.ml
@@ -135,7 +135,7 @@ and eval_call ctx i lname eargs =
| Vbuiltin (str), args ->
(* lookup the built-in implementation and call it *)
- (get_builtin_impl str loc) loc args ctx
+ (get_builtin_impl str loc) loc (i + 1) args ctx
(* return result of eval *)
| _, [] -> f
@@ -239,7 +239,7 @@ and typer_builtins_impl = [
("write" , write_impl);
]
-and bind_impl loc args_val ctx =
+and bind_impl loc depth args_val ctx =
let io, cb = match args_val with
| [io; callback] -> io, callback
@@ -264,9 +264,9 @@ and bind_impl loc args_val ctx =
let nctx = add_rte_variable None underlying ctx in
(* eval callback *)
- _eval body nctx 0)
+ _eval body nctx depth)
-and run_io loc args_val ctx =
+and run_io loc depth args_val ctx =
let io, ltp = match args_val with
| [io; ltp] -> io, ltp
@@ -282,14 +282,14 @@ and run_io loc args_val ctx =
(* return given type *)
ltp
-and typer_eval loc args ctx =
+and typer_eval loc depth args ctx =
let arg = match args with
| [a] -> a
| _ -> eval_error loc "eval_ expects a single argument" in
(* I need to be able to lexp sexp but I don't have lexp ctx *)
match arg with
(* Nodes that can be evaluated *)
- | Closure (_, body, ctx) -> _eval body ctx 1
+ | Closure (_, body, ctx) -> _eval body ctx depth
(* Leaf *)
| _ -> arg
@@ -308,7 +308,7 @@ and get_builtin_impl str loc =
(* Sexp -> (Sexp -> List Sexp -> Sexp) -> (String -> Sexp) ->
(String -> Sexp) -> (Int -> Sexp) -> (Float -> Sexp) -> (List Sexp -> Sexp)
-> Sexp *)
-and sexp_dispatch loc args ctx =
+and sexp_dispatch loc depth args ctx =
let eval a b = _eval a b 1 in
let sxp, nd, sym, str, it, flt, blk, rctx = match args with
| [sxp; Closure(_, nd, rctx); Closure(_, sym, _);
View it on GitLab: https://gitlab.com/monnier/typer/commit/d5da7869ce48357edc95ab4d2bebc5b4e1b…
1
0
Bonjour,
Par rapport aux Monads,
Est-ce que ça ne devrait pas être la fonction bind qui
créé une Vcommand ?
i.e
c = bind (open "./_build/w_file.txt" "w")
(lambda (f : FileHandle) ->
write f "Hello");
a = run-io c Unit;
Dans ce cas run-io roule la commande qui a été créé par bind
--
Pierre Delaunay
2
1