June 2016 - Typer - mailman.iro.umontreal.ca

[Git][monnier/typer][unification] 3 commits: debug recursion on wrong lexp in _unify_call
by BONNEVALLE Vincent 30 Jun '16

30 Jun '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 Jun '16

30 Jun '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 Jun '16

30 Jun '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 Jun '16

29 Jun '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 Jun '16

29 Jun '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

[Git][monnier/typer][unification] 16 commits: remove dead code
by BONNEVALLE Vincent 28 Jun '16

28 Jun '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

[Git][monnier/typer][master] Moved builtin macro implementation
by Setepenre 26 Jun '16

26 Jun '16

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 Jun '16

26 Jun '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

[Git][monnier/typer][master] new calling convention for builtin functions
by Setepenre 25 Jun '16

25 Jun '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

Monads
by Pierre Delaunay 25 Jun '16

25 Jun '16

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