diff --git a/src/compiler.ml b/src/compiler.ml index 7374b8652..b1736ba39 100644 --- a/src/compiler.ml +++ b/src/compiler.ml @@ -627,8 +627,7 @@ end = struct let rec check_loc_tye ~type_abbrevs ~kinds ctx { loc; it } = check_tye ~loc ~type_abbrevs ~kinds ctx it and check_tye ~loc ~type_abbrevs ~kinds ctx = function - | Prop -> TypeAssignment.Prop - | Any -> Any + | Any -> TypeAssignment.Any | Const(Bound _,c) -> check_param_exists ~loc c ctx; UVar c | Const(Global _,c) -> check_global_exists ~loc c type_abbrevs kinds 0; Cons c | App(c,x,xs) -> @@ -1257,7 +1256,7 @@ end = struct | Some (F f) -> fst f | Some (Lam _) -> error "Not fully applied type_abbrev..." end - | Prop | Any -> Relational + | Any -> Relational | App(c,x,xs) -> (* TODO: if we accept polymorphic type with functional arguments, like `:functional pred do i:(list (:functional pred))`, then we should extend @@ -1368,7 +1367,7 @@ end = struct | Functional l -> head_ag_func_pairing functional_preds head_args l | BoundVar v -> error "unreachable branch" - and check_body func_vars = Format.eprintf "Check body todo\n%!"; func_vars + and check_body func_vars = func_vars let rec check_clause ~loc ~functional_preds func_vars ScopedTerm.{it} = match it with @@ -1472,6 +1471,7 @@ type checked_compilation_unit = { precomputed_kinds : Arity.t F.Map.t; precomputed_types : TypeAssignment.overloaded_skema F.Map.t; precomputed_type_abbrevs : (TypeAssignment.skema * Loc.t) F.Map.t; + precomputed_functional_preds : Functionality.t F.Map.t; type_checking_time : float; } [@@deriving show] @@ -1940,11 +1940,30 @@ end = struct - TArr (t1,t2) with t2 = prop with TPred (o:t1), - TArr (t1,t2) with t2 = TPred l with TPred (o:t1, l) *) - (* let rec flatten_arrows *) + let flatten_arrows = + let rec is_pred = function + | Ast.TypeExpression.TConst a -> F.show a = "prop" + | TArr(_,r) -> is_pred r.tit + | TApp (_, _, _) | TPred (_, _) -> false + in + let rec flatten tloc = function + | Ast.TypeExpression.TArr (l,r) -> (Ast.Mode.Output, l) :: flatten_loc r + | TConst c when F.equal c F.propf -> [] + | tit -> [Output,{tit;tloc}] + and flatten_loc {tit;tloc} = flatten tloc tit + and main = function + | Ast.TypeExpression.TPred (b, l) -> + Ast.TypeExpression.TPred (b, List.map (fun (a, b) -> a, main_loc b) l) + | TConst _ as t -> t + | TApp (n, x, xs) -> TApp (n, main_loc x, List.map main_loc xs) + | TArr (l, r) when is_pred r.tit -> TPred (Ast.Structured.Relation, (Output, main_loc l) :: flatten_loc r) + | TArr (l, r) -> TArr(main_loc l, main_loc r) + and main_loc {tit;tloc} = {tit=main tit;tloc} + in main_loc let rec scope_tye ctx ~loc t : ScopedTypeExpression.t_ = match t with - | Ast.TypeExpression.TConst c when F.show c = "prop" -> Prop + | Ast.TypeExpression.TConst c when F.show c = "prop" -> Pred (Relation,[]) | TConst c when F.show c = "any" -> Any | TConst c when F.Set.mem c ctx -> Const(Bound elpi_language,c) | TConst c -> Const(Global false,c) @@ -1955,7 +1974,9 @@ end = struct App(c,scope_loc_tye ctx x, List.map (scope_loc_tye ctx) xs) | TPred(m,xs) -> Pred(m,List.map (fun (m,t) -> m, scope_loc_tye ctx t) xs) | TArr(s,t) -> Arrow(NotVariadic, scope_loc_tye ctx s, scope_loc_tye ctx t) - and scope_loc_tye ctx { tloc; tit } = { loc = tloc; it = scope_tye ctx ~loc:tloc tit } + and scope_loc_tye ctx { tloc; tit } = { loc = tloc; it = scope_tye ctx ~loc:tloc tit } + let scope_loc_tye ctx (t: Ast.Structured.functionality Ast.TypeExpression.t) = + scope_loc_tye ctx @@ flatten_arrows t let compile_type { Ast.Type.name; loc; attributes; ty } = let open ScopedTypeExpression in @@ -1967,7 +1988,6 @@ end = struct | Const(Bound _, _) -> assert false (* there are no binders yet *) | Const(Global _,c) when is_uvar_name c -> F.Set.add c e | Const(Global _,_) -> e - | Prop -> e | Any -> e | Arrow(_,x,y) -> aux (aux e x) y | Pred(_,l) -> List.fold_left aux e (List.map snd l) @@ -3729,7 +3749,9 @@ end = struct (* Functionality *) let check_func_begin = Unix.gettimeofday () in - let functional_preds = FunctionalityChecker.merge_types_and_abbrevs ~old:ofp ~types ~type_abbrevs in + let functional_preds = + FunctionalityChecker.merge_types_and_abbrevs ~old:F.Map.empty ~types ~type_abbrevs in + let all_functional_preds = FunctionalityChecker.merge ofp functional_preds in let check_func_end = Unix.gettimeofday () in (* Typeabbreviation *) @@ -3778,6 +3800,7 @@ end = struct precomputed_kinds =all_kinds; precomputed_type_abbrevs = all_type_abbrevs; precomputed_types = all_types; + precomputed_functional_preds = all_functional_preds; type_checking_time = check_end -. check_begin +. check_t_end -. check_t_begin +. check_k_end -. check_k_begin +. check_func_end +. check_func_begin } end @@ -4259,11 +4282,11 @@ in let extend1 flags (state, { Assembled.hash; clauses = cl; symbols; prolog_program; indexing; modes = om; kinds = ok; functional_preds = ofp; types = ot; type_abbrevs = ota; chr = ochr; toplevel_macros = otlm; total_type_checking_time }) - { version; base_hash; checked_code = { CheckedFlat.toplevel_macros; kinds; types; types_indexing; type_abbrevs; modes; functional_preds; clauses; chr; builtins}; precomputed_kinds; precomputed_type_abbrevs; precomputed_types; type_checking_time } = + { version; base_hash; checked_code = { CheckedFlat.toplevel_macros; kinds; types; types_indexing; type_abbrevs; modes; functional_preds; clauses; chr; builtins}; precomputed_kinds; precomputed_type_abbrevs; precomputed_functional_preds; precomputed_types; type_checking_time; } = let symbols, prolog_program, indexing = update_indexing state symbols prolog_program modes types_indexing indexing in let kinds, type_abbrevs, types, functional_preds = if hash = base_hash then - precomputed_kinds, precomputed_type_abbrevs, precomputed_types, functional_preds + precomputed_kinds, precomputed_type_abbrevs, precomputed_types, precomputed_functional_preds else let kinds = Flatten.merge_kinds ok kinds in let type_abbrevs = merge_type_abbrevs ota type_abbrevs in diff --git a/src/compiler_data.ml b/src/compiler_data.ml index fc2f607d0..69dafcc8e 100644 --- a/src/compiler_data.ml +++ b/src/compiler_data.ml @@ -63,7 +63,7 @@ module ScopedTypeExpression = struct end type t_ = - | Prop | Any + | Any | Const of Scope.t * F.t | App of F.t * e * e list | Arrow of Ast.Structured.variadic * e * e @@ -83,12 +83,12 @@ module ScopedTypeExpression = struct | _ -> 2 let rec pretty_e fmt = function - | Prop -> fprintf fmt "prop" | Any -> fprintf fmt "any" | Const(_,c) -> F.pp fmt c | App(f,x,xs) -> fprintf fmt "@[%a@ %a@]" F.pp f (Util.pplist (pretty_e_parens ~lvl:app) " ") (x::xs) | Arrow(NotVariadic,s,t) -> fprintf fmt "@[%a ->@ %a@]" (pretty_e_parens ~lvl:arrs) s pretty_e_loc t | Arrow(Variadic,s,t) -> fprintf fmt "%a ..-> %a" (pretty_e_parens ~lvl:arrs) s pretty_e_loc t + | Pred(_,[]) -> fprintf fmt "prop" | Pred(_,l) -> fprintf fmt "pred %a" (Util.pplist pretty_ie ", ") l and pretty_ie fmt (i,e) = fprintf fmt "%s:%a" (match i with Ast.Mode.Input -> "i" | Output -> "o") pretty_e_loc e @@ -121,7 +121,6 @@ module ScopedTypeExpression = struct | App(c1,x,xs), App(c2,y,ys) -> F.equal c1 c2 && eqt ctx x y && Util.for_all2 (eqt ctx) xs ys | Arrow(b1,s1,t1), Arrow(b2,s2,t2) -> b1 == b2 && eqt ctx s1 s2 && eqt ctx t1 t2 | Pred(f1,l1), Pred(f2,l2) -> f1 == f2 && Util.for_all2 (fun (m1,t1) (m2,t2) -> Ast.Mode.compare m1 m2 == 0 && eqt ctx t1 t2) l1 l2 - | Prop, Prop -> true | Any, Any -> true | _ -> false @@ -140,7 +139,6 @@ module ScopedTypeExpression = struct if it' == it then orig else { it = it'; loc } and smart_map_scoped_ty f orig = match orig with - | Prop -> orig | Any -> orig | Const((Scope.Bound _| Scope.Global true),_) -> orig | Const(Scope.Global false,c) ->