From dcba75e27122e96abc0da1a171c35766d8cf8862 Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Tue, 17 Dec 2024 15:01:37 +0100 Subject: [PATCH] wip --- src/compiler/type_checker.ml | 115 ++++++++++++++++++++++++----- tests/sources/eta_as.elpi | 1 + tests/sources/hyp_uvar.elpi | 1 + tests/sources/lyp/lyp_machine.elpi | 2 +- tests/sources/map.elpi | 4 +- tests/sources/map_list.elpi | 4 +- 6 files changed, 104 insertions(+), 23 deletions(-) diff --git a/src/compiler/type_checker.ml b/src/compiler/type_checker.ml index ce5850a8c..602e90615 100644 --- a/src/compiler/type_checker.ml +++ b/src/compiler/type_checker.ml @@ -220,17 +220,37 @@ let check ~is_rule ~type_abbrevs ~kinds ~types:env ~unknown (t : ScopedTerm.t) ~ | CData c -> check_cdata ~loc ~tyctx kinds c ety | Spill(_,{contents = Phantom _}) -> assert false | Spill(sp,info) -> check_spill ~positive ctx ~loc ~tyctx sp info ety + (* | App (Global _ as gid, pi, ({it=Lam (s,cty,tya,bo)} as x), []) when F.equal pi F.pif -> + begin + let err ty = error_bad_ety ~loc ~tyctx ~ety ScopedTerm.pretty_ (App(Scope.mkGlobal ~escape_ns:true ()(*sucks*),pi,x,[])) ty in + if unify prop ety then + let _ = + let m = TypeAssignment.MVal Input in + let s = TypeAssignment.(Arr (MVal Input, NotVariadic,UVar (MutableOnce.make (F.from_string "A")),prop)) in + let t = prop in + let xs = check_loc_if_not_phantom ~positive ~tyctx:(Some pi) ctx x ~ety:s in + Format.eprintf "-- Checked term %a with ety %a; mode is %a@." ScopedTerm.pretty x TypeAssignment.pretty_mut_once s TypeAssignment.pretty_tmode m; + begin + match TypeAssignment.deref_tmode m with + | MVal Input when positive -> propagate_ground ctx x; + | MVal Output when positive -> () (*check_ground ctx x; BIG TODO*) + | MVal Input -> check_ground ctx x; + | MVal Output -> propagate_ground ctx x; + | _ -> assert (not @@ TypeAssignment.is_arrow_to_prop s) + end; + infer_mode ctx m x; + check_app_single ~positive ctx ~loc (pi,gid) t (x::[]) xs + in [] + else err prop + end *) | App(Global _ as gid,c,x,xs) -> check_app ~positive ctx ~loc ~tyctx (c,gid) (global_type env ~loc c) (x::xs) ety | App(Bound lang as gid,c,x,xs) -> check_app ~positive ctx ~loc ~tyctx (c,gid) (local_type ctx ~loc (c,lang)) (x::xs) ety (* TODO: regola ad hoc "pi (lam x\ ...)" che mette x a ground, eg: chr-scope-change *) - | Lam(c,cty,tya,t) -> - let xxx = check_lam ~positive ctx ~loc ~tyctx c cty tya t ety in - Format.eprintf "@[end checking %a : %a@]\n" ScopedTerm.pretty_ x TypeAssignment.pretty_mut_once_raw ety; - xxx + | Lam(c,cty,tya,t) -> check_lam ~positive ctx ~loc ~tyctx c cty tya t ety | Discard -> [] | Var(c,args) -> check_app ~positive ctx ~loc ~tyctx (c, Bound elpi_language (*hack*)) (uvar_type ~loc c) args ety | Cast(t,ty) -> - let ty = TypeAssignment.subst (fun f -> Some (TypeAssignment.UVar(MutableOnce.make f))) @@ check_loc_tye ~type_abbrevs ~kinds F.Set.empty ty in + let ty = TypeAssignment.subst (fun f -> Some (UVar(MutableOnce.make f))) @@ check_loc_tye ~type_abbrevs ~kinds F.Set.empty ty in let spills = check_loc ~positive ctx ~tyctx:None t ~ety:ty in if unify ty ety then spills else error_bad_ety ~valid_mode ~loc ~tyctx ScopedTerm.pretty_ x ty ~ety @@ -289,13 +309,22 @@ let check ~is_rule ~type_abbrevs ~kinds ~types:env ~unknown (t : ScopedTerm.t) ~ if unify ty ety then [] else error_bad_cdata_ety ~tyctx ~loc c ty ~ety + and deref_ ~loc tya = + if true then tya else + if MutableOnce.is_set tya then + match MutableOnce.get tya |> TypeAssignment.unval with + | UVar var -> deref_ ~loc var + | _ -> error ~loc "Mutable once cannot be set in a already set term" + else tya + and check_lam ~positive ctx ~loc ~tyctx c cty tya t ety = let name_lang = match c with Some c -> c | None -> fresh_name (), elpi_language in - let set_tya_ret f = MutableOnce.set ~loc tya (Val f); f in + let set_tya_ret f = MutableOnce.set ~loc (deref_ ~loc tya) (Val f); f in let src = set_tya_ret @@ match cty with | None -> mk_uvar "Src" | Some x -> TypeAssignment.subst (fun f -> Some (UVar(MutableOnce.make f))) @@ check_loc_tye ~type_abbrevs ~kinds F.Set.empty x - in + in + Format.eprintf "Ty is setted to %a@." (MutableOnce.pp TypeAssignment.pp) (tya); let tgt = mk_uvar "Tgt" in (* let () = Format.eprintf "lam ety %a\n" TypeAssignment.pretty ety in *) let mode = TypeAssignment.MRef (MutableOnce.make F.dummyname) in @@ -356,7 +385,7 @@ let check ~is_rule ~type_abbrevs ~kinds ~types:env ~unknown (t : ScopedTerm.t) ~ check_app_overloaded ~positive ctx ~loc (c,cid) ety args targs l l end | Single (id,ty) -> - Format.eprintf "%a: 1 option: %a\n" F.pp c TypeAssignment.pretty_mut_once_raw ty; + Format.eprintf "%a: 1 option: %a@." F.pp c TypeAssignment.pretty_mut_once_raw ty; let err ty = if args = [] then error_bad_ety ~valid_mode ~loc ~tyctx ~ety F.pp c ty (* uvar *) else error_bad_ety ~valid_mode ~loc ~tyctx ~ety ScopedTerm.pretty_ (App(Scope.mkGlobal ~escape_ns:true ()(* sucks *),c,List.hd args,List.tl args)) ty in @@ -383,7 +412,7 @@ let check ~is_rule ~type_abbrevs ~kinds ~types:env ~unknown (t : ScopedTerm.t) ~ if List.length args > List.length srcs then monodirectional () (* will error *) else if any_arg_is_spill args then monodirectional () - else bidirectional srcs tgt + else (Format.eprintf "HERE@."; bidirectional srcs tgt) (* REDO PROCESSING ONE SRC at a time *) and check_app_overloaded ~positive ctx ~loc (c, cid as c_w_id) ety args targs alltys = function @@ -402,22 +431,66 @@ let check ~is_rule ~type_abbrevs ~kinds ~types:env ~unknown (t : ScopedTerm.t) ~ if try_unify (arrow_of_tys srcs tgt) (arrow_of_tys (decore_with_dummy_mode targs) ety) then (resolve_gid id cid;[]) (* TODO: here we should something ? *) else check_app_overloaded ~positive ctx ~loc c_w_id ety args targs alltys ts + and get_mode m = + match TypeAssignment.deref_tmode m with + | MVal v -> v + | _ -> error "flex mode cannot be get" + + and closed_term ctx {loc; it} = match it with + | CData _ | Const _ | Discard -> () + | App (_,_,x,xs) -> List.iter (closed_term ctx) (x::xs) + | Impl (_,_,_) -> failwith "TODO" + | Cast (t, _) -> closed_term ctx t + | Var (_, _) -> failwith "TODO" + | Lam (_, _, _, _) -> failwith "TODO" + | Spill (_, _) -> failwith "TODO" + + and check_ground_args ctx ty args = + match args, ty with + | [], _ -> () + | x::xs, TypeAssignment.Arr (m,NotVariadic,l,r) -> + let m = get_mode m in + if m = Input then check_ground ctx x; + check_ground_args ctx r xs + | x::xs, Arr (m,Variadic,_,_) -> + let m = get_mode m in + if m = Input then check_ground ctx x; + check_ground_args ctx ty xs + | _ -> anomaly "unreachable branch" + and check_ground ctx { loc; it } = match it with - | Const(Scope.Bound l,f) -> + | Discard | CData _ | Const(Global _,_) -> () + | Const(Bound l,f) -> begin match Scope.Map.find_opt (f,l) ctx with | None -> anomaly "unbound" | Some { ground = IGround } -> () - | Some _ -> error ~loc (F.show f ^ " not gound " ^ Scope.Map.show pp_ctx ctx) + | Some _ -> error ~loc (F.show f ^ " not ground " ^ Scope.Map.show pp_ctx ctx) end | Var(f,args) -> begin match F.Map.find_opt f !sigma with | None -> anomaly "arg already typed" | Some { ground = IGround } -> () - | Some _ -> error ~loc (F.show f ^ " not gound: " ^ F.Map.show pp_sigma !sigma) + | Some _ -> error ~loc (F.show f ^ " not ground: " ^ F.Map.show pp_sigma !sigma) end - | _ -> () (* TODO *) + | Cast (t, _) -> check_ground ctx t + | _ -> () + | App (Global _, c, x, xs) -> + let ty = failwith "TODO: should get the type of the constant c, but getting it from the ctx is not good, due to Overloaded symbols..." in + check_ground_args ctx ty (x::xs) + | App (Bound lang, c, x, xs) -> + let ty = failwith "TODO: same problem as 3 lines above..."(*local_type ctx ~loc (c,lang)*) in + check_ground_args ctx ty (x::xs) + | Lam (s, _, tya, bo) -> failwith "TODO" (* TODO: + here we can use tya to add the type of s into ctx to the recursive call + moreover, s is ground or unkown depending on its mode. the mode can + be found in the ty from the 2nd argument of check_ground + *) + | Impl (true, a, b) -> check_ground ctx b (* TODO: check also a*) + | Impl (false, a, b) -> failwith "TODO" + | Spill (_, _) -> failwith "TODO" and propagate_ground ctx { loc ; it } = match it with + | Discard | CData _ | Const(Global _,_) -> () | Const(Scope.Bound l,f) -> begin match Scope.Map.find_opt (f,l) ctx with | None -> anomaly "unbound" @@ -431,9 +504,13 @@ let check ~is_rule ~type_abbrevs ~kinds ~types:env ~unknown (t : ScopedTerm.t) ~ | Some info -> info.ground <- IGround end | App(s,f,x,xs) -> - (* TODO: only on i: arguments, if a prop *) List.iter (propagate_ground ctx) (x::xs) - | _ -> () (* TODO *) + | Cast (t, _) -> propagate_ground ctx t + | _ -> () + | Impl (_, _, _) -> failwith "TODO" + | Lam (_, _, _, _) -> failwith "TODO" + | Spill (_, _) -> failwith "TODO" + and infer_mode ctx m { loc; it } = match it with @@ -450,13 +527,15 @@ let check ~is_rule ~type_abbrevs ~kinds ~types:env ~unknown (t : ScopedTerm.t) ~ match args with | [] -> ty | x :: xs -> - Format.eprintf "checking app %a against %a\n" ScopedTerm.pretty_ (ScopedTerm.App(snd c, fst c,x,xs)) TypeAssignment.pretty_mut_once_raw ty; + Format.eprintf "@[Checking term %a with type %a@]@." ScopedTerm.pretty x TypeAssignment.pretty_mut_once_raw ty; + (* Format.eprintf "checking app %a against %a@." ScopedTerm.pretty_ (ScopedTerm.App(snd c, fst c,x,xs)) TypeAssignment.pretty_mut_once_raw ty; *) match ty with | TypeAssignment.Arr(_(*TODO: @FissoreD*), Variadic,s,t) -> let xs = check_loc_if_not_phantom ~positive ~tyctx:(Some (fst c)) ctx x ~ety:s @ xs in if xs = [] then t else check_app_single ~positive ctx ~loc c ty (x::consumed) xs | Arr(m,NotVariadic,s,t) -> let xs = check_loc_if_not_phantom ~positive ~tyctx:(Some (fst c)) ctx x ~ety:s @ xs in + Format.eprintf "-- Checked term %a with ety %a; mode is %a@." ScopedTerm.pretty x TypeAssignment.pretty_mut_once s TypeAssignment.pretty_tmode m; begin match TypeAssignment.deref_tmode m with | MVal Input when positive -> propagate_ground ctx x; @@ -466,7 +545,7 @@ let check ~is_rule ~type_abbrevs ~kinds ~types:env ~unknown (t : ScopedTerm.t) ~ | _ -> assert (not @@ TypeAssignment.is_arrow_to_prop s) (* TODO: if the conclusion in unknown, fail *) end; infer_mode ctx m x; - check_app_single ~positive ctx ~loc c t (x::consumed) xs + check_app_single ~positive ctx ~loc c t (x::consumed) xs | Any -> check_app_single ~positive ctx ~loc c ty (x::consumed) xs | UVar m when MutableOnce.is_set m -> check_app_single ~positive ctx ~loc c (TypeAssignment.deref m) consumed (x :: xs) @@ -625,7 +704,7 @@ let check ~is_rule ~type_abbrevs ~kinds ~types:env ~unknown (t : ScopedTerm.t) ~ unif ~matching t1 t2 | _,_ -> false - and unify x (y: TypeAssignment.t MutableOnce.t TypeAssignment.t_) = unif ~matching:false x y + and unify (x: TypeAssignment.t MutableOnce.t TypeAssignment.t_) (y: TypeAssignment.t MutableOnce.t TypeAssignment.t_) = unif ~matching:false x y and try_matching ~pat:((_,x),vars) y = let vars = F.Map.bindings vars |> List.map snd |> List.map cell_of, [] in let deref x = cell_of (TypeAssignment.deref x) in diff --git a/tests/sources/eta_as.elpi b/tests/sources/eta_as.elpi index e44b3a444..9b9647bd7 100644 --- a/tests/sources/eta_as.elpi +++ b/tests/sources/eta_as.elpi @@ -38,6 +38,7 @@ unif_2 (x\ y\ X x y). type u any. +:untyped tests-uvar :- print "--------- uvar_1", not(uvar_1 (bar (x \ u))), diff --git a/tests/sources/hyp_uvar.elpi b/tests/sources/hyp_uvar.elpi index 1c37459a2..b89ff1cc9 100644 --- a/tests/sources/hyp_uvar.elpi +++ b/tests/sources/hyp_uvar.elpi @@ -1,5 +1,6 @@ pred f i:any. +:untyped main :- (f uvar :- print "ok") => (f X, not(f 1)), var X. \ No newline at end of file diff --git a/tests/sources/lyp/lyp_machine.elpi b/tests/sources/lyp/lyp_machine.elpi index 52f37ef79..0d6f95702 100644 --- a/tests/sources/lyp/lyp_machine.elpi +++ b/tests/sources/lyp/lyp_machine.elpi @@ -235,7 +235,7 @@ conv_t T1 S1 S2 X2 :- def_l X2 T2, !, % print "d", % Implied conversion %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -type conv_i id -> term -> stack -> stack -> term -> id -> prop. +pred conv_i i:id, o:term, o:stack, o:stack, o:term, i:id. conv_i X1 _ S1 S2 T2 X2 :- X1 < X2, !, conv_t X1 S1 S2 T2. diff --git a/tests/sources/map.elpi b/tests/sources/map.elpi index a5f52564a..5b35ccbbd 100644 --- a/tests/sources/map.elpi +++ b/tests/sources/map.elpi @@ -6,14 +6,14 @@ build N M X X1 :- std.map.add N N X XR, build N1 M XR X1. -pred test i:int, i:int, i:(int -> A -> int -> prop), i:A. +pred test i:int, i:int, i:(pred i:int, i:A, o:int), i:A. test N N _ _ :- !. test N M F X :- N1 is N + 1, std.assert! (F N X N) "not found", test N1 M F X. -pred test2 i:int, i:int, i:(int -> A -> A -> prop), i:A. +pred test2 i:int, i:int, i:(pred i:int, i:A, o:A), i:A. test2 N N _ _ :- !. test2 N M F X :- N1 is N + 1, diff --git a/tests/sources/map_list.elpi b/tests/sources/map_list.elpi index 94fa6b466..c00a9cf74 100644 --- a/tests/sources/map_list.elpi +++ b/tests/sources/map_list.elpi @@ -26,14 +26,14 @@ build N M X X1 :- add N N X XR, build N1 M XR X1. -pred test i:int, i:int, i:(int -> A -> int -> prop), i:A. +pred test i:int, i:int, i:(pred i:int, i:A, o:int), i:A. test N N _ _ :- !. test N M F X :- N1 is N + 1, std.assert! (F N X N) "not found", test N1 M F X. -pred test2 i:int, i:int, i:(int -> A -> A -> prop), i:A. +pred test2 i:int, i:int, i:(pred i:int, i:A, o:A), i:A. test2 N N _ _ :- !. test2 N M F X :- N1 is N + 1,