From 0668a57af9ba1476aedf5a9e216f23ab20e99663 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 9 Nov 2024 15:30:23 +0100 Subject: [PATCH] [compiler+determinacy] no modes in AST + new check determinacy + unique_type_id - AST has no modes - in the old representation the predicate `type p int -> prop.` did not produce a mode for p. - therefore, Structured.program has no more a modes field - we delegate the computation of modes to Scoped_Quotation_Macro.run - flatten_arrows - objects with type `TArr (l, r)` where `r` has Prop as rightmost type, is transformed into `TPred (...)` by flatten_arrows. - the result of this call to flatten_arrows is used next to build modes and determinacy relations of predicates - IdPos.t - IdPos is a new module representing unique identifiers for elpi objects. - using integers is not possible due to the potential fusion of different units - therefore we use the position of a parsed terms as its id - unique ids are used by the typechecker which sets a unique id to the type of global constants - type of bound variables - the type of bound variables is attached to the lam node by the typechecker - determinacy checker - input arguments functionality setting - body premise inference and check --- src/compiler/compiler.ml | 224 ++++--- src/compiler/compiler_data.ml | 90 ++- src/compiler/determinacy_checker.ml | 764 +++++++++++++++++------ src/compiler/determinacy_checker.mli | 23 +- src/compiler/dune | 3 +- src/compiler/test_compiler_data.ml | 3 +- src/compiler/type_checker.ml | 30 +- src/parser/ast.ml | 1 - src/parser/ast.mli | 1 - src/utils/util.ml | 1 + src/utils/util.mli | 1 + tests/sources/functionality/test1.elpi | 1 + tests/sources/functionality/test10.elpi | 1 + tests/sources/functionality/test11.elpi | 3 +- tests/sources/functionality/test12.elpi | 1 + tests/sources/functionality/test13.elpi | 1 + tests/sources/functionality/test14.elpi | 1 + tests/sources/functionality/test15.elpi | 1 + tests/sources/functionality/test16.elpi | 1 + tests/sources/functionality/test17.elpi | 1 + tests/sources/functionality/test18.elpi | 1 + tests/sources/functionality/test19.elpi | 1 + tests/sources/functionality/test2.elpi | 6 +- tests/sources/functionality/test20.elpi | 1 + tests/sources/functionality/test21.elpi | 1 + tests/sources/functionality/test22.elpi | 3 +- tests/sources/functionality/test23.elpi | 1 + tests/sources/functionality/test24.elpi | 1 + tests/sources/functionality/test25.elpi | 1 + tests/sources/functionality/test26.elpi | 1 + tests/sources/functionality/test27.elpi | 1 + tests/sources/functionality/test28.elpi | 1 + tests/sources/functionality/test29.elpi | 1 + tests/sources/functionality/test3.elpi | 1 + tests/sources/functionality/test30.elpi | 1 + tests/sources/functionality/test3_1.elpi | 11 + tests/sources/functionality/test4.elpi | 1 + tests/sources/functionality/test5.elpi | 1 + tests/sources/functionality/test6.elpi | 1 + tests/sources/functionality/test7.elpi | 1 + tests/sources/functionality/test8.elpi | 1 + tests/sources/functionality/test9.elpi | 1 + tests/sources/progs/progs3.mod | 2 +- tests/sources/progs/progs4.mod | 2 +- tests/sources/progs/tr1_test.mod | 8 +- tests/sources/progs/tr2_test.mod | 10 +- tests/suite/correctness_FO.ml | 23 +- 47 files changed, 839 insertions(+), 397 deletions(-) create mode 100644 tests/sources/functionality/test3_1.elpi diff --git a/src/compiler/compiler.ml b/src/compiler/compiler.ml index 37d09faa4..ef95dc4f8 100644 --- a/src/compiler/compiler.ml +++ b/src/compiler/compiler.ml @@ -271,7 +271,7 @@ module Assembled = struct types : TypeAssignment.overloaded_skema_with_id F.Map.t; type_abbrevs : (TypeAssignment.skema_w_id * Loc.t) F.Map.t; modes : (mode * Loc.t) F.Map.t; - functional_preds: Determinacy_checker.func_map; + functional_preds: Determinacy_checker.t; } [@@deriving show] @@ -479,11 +479,39 @@ end = struct (* {{{ *) | TConst c -> TConst c } + + (* + replaces + - TArr (t1,t2) when t2 = Prop -> TPred (o:t1), + - TArr (t1,t2) when t2 = TPred l -> TPred (o:t1, l) + *) + let flatten_arrows toplevel_func = + 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 (toplevel_func, (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 structure_type_expression loc toplevel_func valid t = - match t.TypeExpression.tit with - | TPred([],p) -> - { t with tit = TPred(toplevel_func,List.map (fun (m,p) -> m, structure_type_expression_aux ~loc valid p) p) } - | x -> structure_type_expression_aux ~loc valid t + let res = match t.TypeExpression.tit with + | TPred([],p) -> + { t with tit = TPred(toplevel_func,List.map (fun (m,p) -> m, structure_type_expression_aux ~loc valid p) p) } + | x -> structure_type_expression_aux ~loc valid t + in flatten_arrows toplevel_func res let structure_kind_attributes { Type.attributes; loc; name; ty } = let ty = structure_type_expression loc () (function [] -> Some () | _ -> None) ty in @@ -538,97 +566,96 @@ end = struct (* {{{ *) { TypeAbbreviation.name; value = aux value; nparams; loc } let run _ dl = - let rec aux_run ns blocks clauses macros kinds types tabbrs modes chr accs = function + let rec aux_run ns blocks clauses macros kinds types tabbrs chr accs = function | Program.Ignored _ :: rest -> - aux_run ns blocks clauses macros kinds types tabbrs modes chr accs rest + aux_run ns blocks clauses macros kinds types tabbrs chr accs rest | (Program.End _ :: _ | []) as rest -> { body = List.rev (cl2b clauses @ blocks); types = (*List.rev*) types; (* we prefer the last one *) kinds = List.rev kinds; type_abbrevs = List.rev tabbrs; - macros = List.rev macros; - modes = List.rev modes }, + macros = List.rev macros }, List.rev chr, rest | Program.Begin loc :: rest -> - let p, chr1, rest = aux_run ns [] [] [] [] [] [] [] [] accs rest in + let p, chr1, rest = aux_run ns [] [] [] [] [] [] [] accs rest in if chr1 <> [] then error "CHR cannot be declared inside an anonymous block"; aux_end_block loc ns (Accumulated p :: cl2b clauses @ blocks) - [] macros kinds types tabbrs modes chr accs rest + [] macros kinds types tabbrs chr accs rest | Program.Constraint (loc, ctx_filter, clique) :: rest -> if chr <> [] then error "Constraint blocks cannot be nested"; - let p, chr, rest = aux_run ns [] [] [] [] [] [] [] [] accs rest in + let p, chr, rest = aux_run ns [] [] [] [] [] [] [] accs rest in aux_end_block loc ns (Constraints({ctx_filter;clique;rules=chr},p) :: cl2b clauses @ blocks) - [] macros kinds types tabbrs modes [] accs rest + [] macros kinds types tabbrs [] accs rest | Program.Namespace (loc, n) :: rest -> - let p, chr1, rest = aux_run (n::ns) [] [] [] [] [] [] [] [] StrSet.empty rest in + let p, chr1, rest = aux_run (n::ns) [] [] [] [] [] [] [] StrSet.empty rest in if chr1 <> [] then error "CHR cannot be declared inside a namespace block"; aux_end_block loc ns (Namespace (n,p) :: cl2b clauses @ blocks) - [] macros kinds types tabbrs modes chr accs rest + [] macros kinds types tabbrs chr accs rest | Program.Shorten (loc,[]) :: _ -> anomaly ~loc "parser returns empty list of shorten directives" | Program.Shorten (loc,directives) :: rest -> let shorthand (full_name,short_name) = { iloc = loc; full_name; short_name } in let shorthands = List.map shorthand directives in - let p, chr1, rest = aux_run ns [] [] [] [] [] [] [] [] accs rest in + let p, chr1, rest = aux_run ns [] [] [] [] [] [] [] accs rest in if chr1 <> [] then error "CHR cannot be declared after a shorthand"; aux_run ns ((Shorten(shorthands,p) :: cl2b clauses @ blocks)) - [] macros kinds types tabbrs modes chr accs rest + [] macros kinds types tabbrs chr accs rest | Program.Accumulated (_,[]) :: rest -> - aux_run ns blocks clauses macros kinds types tabbrs modes chr accs rest + aux_run ns blocks clauses macros kinds types tabbrs chr accs rest | Program.Accumulated (loc,{ file_name; digest; ast = a } :: more) :: rest -> let rest = Program.Accumulated (loc, more) :: rest in let digest = String.concat "." (digest :: List.map F.show ns) in if StrSet.mem digest accs then begin (* Printf.eprintf "skip: %s\n%!" filename; *) - aux_run ns blocks clauses macros kinds types tabbrs modes chr accs rest + aux_run ns blocks clauses macros kinds types tabbrs chr accs rest end else begin (* Printf.eprintf "acc: %s -> %d\n%!" filename (List.length a); *) - aux_run ns blocks clauses macros kinds types tabbrs modes chr + aux_run ns blocks clauses macros kinds types tabbrs chr (StrSet.add digest accs) (Program.Begin loc :: a @ Program.End loc :: rest) end | Program.Clause c :: rest -> let c = structure_clause_attributes c in - aux_run ns blocks (c::clauses) macros kinds types tabbrs modes chr accs rest + aux_run ns blocks (c::clauses) macros kinds types tabbrs chr accs rest | Program.Macro m :: rest -> - aux_run ns blocks clauses (m::macros) kinds types tabbrs modes chr accs rest + aux_run ns blocks clauses (m::macros) kinds types tabbrs chr accs rest | Program.Pred t :: rest -> let t = structure_type_attributes t in - aux_run ns blocks clauses macros kinds (t :: types) tabbrs (t::modes) chr accs rest + aux_run ns blocks clauses macros kinds (t :: types) tabbrs chr accs rest | Program.Kind [] :: rest -> - aux_run ns blocks clauses macros kinds types tabbrs modes chr accs rest + aux_run ns blocks clauses macros kinds types tabbrs chr accs rest | Program.Kind (k::ks) :: rest -> let k = structure_kind_attributes k in - aux_run ns blocks clauses macros (k :: kinds) types tabbrs modes chr accs (Program.Kind ks :: rest) + aux_run ns blocks clauses macros (k :: kinds) types tabbrs chr accs (Program.Kind ks :: rest) | Program.Type [] :: rest -> - aux_run ns blocks clauses macros kinds types tabbrs modes chr accs rest + aux_run ns blocks clauses macros kinds types tabbrs chr accs rest | Program.Type (t::ts) :: rest -> if List.mem Functional t.attributes then error ~loc:t.loc "functional attribute only applies to pred"; let t = structure_type_attributes t in - aux_run ns blocks clauses macros kinds (t :: types) tabbrs modes chr accs (Program.Type ts :: rest) + aux_run ns blocks clauses macros kinds (t :: types) tabbrs chr accs (Program.Type ts :: rest) | Program.TypeAbbreviation abbr :: rest -> let abbr = structure_type_abbreviation abbr in - aux_run ns blocks clauses macros kinds types (abbr :: tabbrs) modes chr accs rest + aux_run ns blocks clauses macros kinds types (abbr :: tabbrs) chr accs rest | Program.Chr r :: rest -> let r = structure_chr_attributes r in - aux_run ns blocks clauses macros kinds types tabbrs modes (r::chr) accs rest + aux_run ns blocks clauses macros kinds types tabbrs (r::chr) accs rest - and aux_end_block loc ns blocks clauses macros kinds types tabbrs modes chr accs rest = + and aux_end_block loc ns blocks clauses macros kinds types tabbrs chr accs rest = match rest with | Program.End _ :: rest -> - aux_run ns blocks clauses macros kinds types tabbrs modes chr accs rest + aux_run ns blocks clauses macros kinds types tabbrs chr accs rest | _ -> error ~loc "matching } is missing" in - let blocks, chr, rest = aux_run [] [] [] [] [] [] [] [] [] StrSet.empty dl in + let blocks, chr, rest = aux_run [] [] [] [] [] [] [] [] StrSet.empty dl in begin match rest with | [] -> () | Program.End loc :: _ -> error ~loc "extra }" @@ -771,32 +798,6 @@ end = struct let c = (F.show f).[0] in c = '@' - (* - replaces - - TArr (t1,t2) with t2 = prop with TPred (o:t1), - - TArr (t1,t2) with t2 = TPred l with TPred (o:t1, l) - *) - 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" -> Pred (Relation,[]) @@ -812,7 +813,7 @@ end = struct | 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 } let scope_loc_tye ctx (t: Ast.Structured.functionality Ast.TypeExpression.t) = - scope_loc_tye ctx @@ flatten_arrows t + scope_loc_tye ctx t let compile_type { Ast.Type.name; loc; attributes; ty } = let open ScopedTypeExpression in @@ -889,11 +890,12 @@ end = struct ScopedTerm.Cast(t,ty) | Lam (c,ty,b) when is_discard c -> let ty = ty |> Option.map (fun ty -> scope_loc_tye F.Set.empty (RecoverStructure.structure_type_expression ty.Ast.TypeExpression.tloc Ast.Structured.Relation (function [] -> Some Ast.Structured.Relation | _ -> None) ty)) in - ScopedTerm.Lam (None,ty,scope_loc_term ~state ctx b) + ScopedTerm.Lam (None,ty,ScopedTerm.mk_empty_lam_type None, scope_loc_term ~state ctx b) | Lam (c,ty,b) -> if has_dot c then error ~loc "Bound variables cannot contain the namespaec separator '.'"; let ty = ty |> Option.map (fun ty -> scope_loc_tye F.Set.empty (RecoverStructure.structure_type_expression ty.Ast.TypeExpression.tloc Ast.Structured.Relation (function [] -> Some Ast.Structured.Relation | _ -> None) ty)) in - ScopedTerm.Lam (Some (c,elpi_language),ty,scope_loc_term ~state (F.Set.add c ctx) b) + let name = Some (c,elpi_language) in + ScopedTerm.Lam (name,ty, ScopedTerm.mk_empty_lam_type name,scope_loc_term ~state (F.Set.add c ctx) b) | CData c -> ScopedTerm.CData c (* CData.hcons *) | App ({ it = Const _},[]) -> anomaly "Application node with no arguments" | App ({ it = Lam _},_) -> @@ -947,22 +949,30 @@ end = struct name, ab let check_duplicate_mode name (mode, loc) map = - if F.Map.mem name map && fst (F.Map.find name map) <> mode then + match F.Map.find_opt name map with + | Some (mode2,loc2) when mode2 <> mode -> error ~loc - ("Duplicate mode declaration for " ^ F.show name ^ " (also at "^ - Loc.show (snd (F.Map.find name map)) ^ ")") + (Format.asprintf "Duplicate mode declaration for %a (also at %a)\n Mode1 = %a\n Mode2 = %a" F.pp name Loc.pp loc2 pp_mode mode pp_mode mode2) + | _ -> () - let compile_mode modes { Ast.Type.name; loc; ty = { Ast.TypeExpression.tit } } = + let compile_mode_aux modes ({value;name} :ScopedTypeExpression.t) = let fix_mode = function Ast.Mode.Input -> Util.Input | Ast.Mode.Output -> Util.Output in let rec type_to_mode = function - | m, Ast.TypeExpression.{ tit = TPred(_,l) } -> Ho(fix_mode m,List.map type_to_mode l) + | m, ScopedTypeExpression.{it = Pred(_,l)} -> Ho(fix_mode m,List.map type_to_mode l) | m, _ -> Fo (fix_mode m) in - match tit with - | Ast.TypeExpression.TPred(_,l) -> + let rec type_to_mode_under_abs = function + | ScopedTypeExpression.Lam (_,b) -> type_to_mode_under_abs b + | Ty {it = Pred (_,l);loc} -> let args = List.map type_to_mode l in - check_duplicate_mode name (args,loc) modes; - F.Map.add name (args,loc) modes - | _ -> modes + check_duplicate_mode name (args,loc) modes; + F.Map.add name (args,loc) modes + | Ty _ -> modes + in + type_to_mode_under_abs value + + let compile_mode name l modes = + if F.equal F.rimplf name || F.equal F.implf name then modes + else List.fold_left compile_mode_aux modes l let defs_of_map m = F.Map.bindings m |> List.fold_left (fun x (a,_) -> F.Set.add a x) F.Set.empty let defs_of_assoclist m = m |> List.fold_left (fun x (a,_) -> F.Set.add a x) F.Set.empty @@ -1022,12 +1032,12 @@ end = struct let run state ~toplevel_macros p : Scoped.program = - let rec compile_program omacros state { Ast.Structured.macros; kinds; types; type_abbrevs; modes; body } = + let rec compile_program omacros state { Ast.Structured.macros; kinds; types; type_abbrevs; body } = let toplevel_macros, active_macros = List.fold_left (compile_macro state) (F.Map.empty,omacros) macros in let type_abbrevs = List.map compile_type_abbrev type_abbrevs in let kinds = List.fold_left compile_kind F.Map.empty kinds in let types = List.fold_left (fun m t -> map_append t.Ast.Type.name (TypeList.make @@ compile_type t) m) F.Map.empty (List.rev types) in - let modes = List.fold_left compile_mode F.Map.empty modes in + let modes = F.Map.fold compile_mode types F.Map.empty in let defs_m = defs_of_map modes in let defs_k = defs_of_map kinds in let defs_t = defs_of_map types in @@ -1165,10 +1175,10 @@ module Flatten : sig let xs' = smart_map aux_loc xs in if c == c' && x == x' && xs == xs' then it else App(scope,c',x',xs') - | Lam(n,ty,b) -> + | Lam(n,ty,tya,b) -> let b' = aux_loc b in let ty' = option_smart_map (ScopedTypeExpression.smart_map_scoped_loc_ty f) ty in - if b == b' && ty' == ty then it else Lam(n,ty',b') + if b == b' && ty' == ty then it else Lam(n,ty',tya,b') | Var(c,l) -> let l' = smart_map aux_loc l in if l == l' then it else Var(c,l') @@ -1339,7 +1349,7 @@ end = struct let { Assembled.modes = om; functional_preds = ofp; kinds = ok; types = ot; type_abbrevs = ota; toplevel_macros = otlm } = base_signature in let { Flat.modes; kinds; types; type_abbrevs; toplevel_macros } = signature in let all_kinds = Flatten.merge_kinds ok kinds in - (* let func_setter_object = new Determinacy_checker.merger ofp in *) + let func_setter_object = new Determinacy_checker.merger ofp in let check_k_begin = Unix.gettimeofday () in let all_type_abbrevs, type_abbrevs = List.fold_left (fun (all_type_abbrevs,type_abbrevs) (name, scoped_ty) -> @@ -1353,9 +1363,7 @@ end = struct ("Duplicate type abbreviation for " ^ F.show name ^ ". Previous declaration: " ^ Loc.show otherloc) end - else - (); - (* func_setter_object#add_ty_abbr name id scoped_ty; *) + else func_setter_object#add_ty_abbr id scoped_ty; F.Map.add name ((id, ty),loc) all_type_abbrevs, F.Map.add name ((id,ty),loc) type_abbrevs) (ota,F.Map.empty) type_abbrevs in let check_k_end = Unix.gettimeofday () in @@ -1367,7 +1375,7 @@ end = struct let raw_types = types in let types = F.Map.mapi (fun name e -> let tys = Type_checker.check_types ~type_abbrevs:all_type_abbrevs ~kinds:all_kinds e in - (* func_setter_object#add_func_ty_list name e tys; *) + func_setter_object#add_func_ty_list e tys; tys) types in let types_indexing = F.Map.filter_map (fun k tyl -> @@ -1383,9 +1391,10 @@ end = struct let all_types = Flatten.merge_type_assignments ot types in let all_toplevel_macros = Flatten.merge_toplevel_macros otlm toplevel_macros in let all_modes = Flatten.merge_modes om modes in - - { Assembled.modes; functional_preds = (* func_setter_object#get_local_func; *)ofp; kinds; types; type_abbrevs; toplevel_macros }, - { Assembled.modes = all_modes; functional_preds = (* func_setter_object#get_all_func; *)ofp; kinds = all_kinds; types = all_types; type_abbrevs = all_type_abbrevs; toplevel_macros = all_toplevel_macros }, + let all_functional_preds = func_setter_object#merge in + + { Assembled.modes; functional_preds = func_setter_object#get_local_func; kinds; types; type_abbrevs; toplevel_macros }, + { Assembled.modes = all_modes; functional_preds = all_functional_preds; kinds = all_kinds; types = all_types; type_abbrevs = all_type_abbrevs; toplevel_macros = all_toplevel_macros }, check_t_end -. check_t_begin +. check_k_end -. check_k_begin, types_indexing @@ -1401,7 +1410,7 @@ end = struct let unknown = List.fold_left (fun unknown ({ Ast.Clause.body; loc; attributes = { Ast.Structured.typecheck } }) -> if typecheck then let unknown = Type_checker.check ~is_rule:true ~unknown ~type_abbrevs ~kinds ~types body ~exp:(Val Prop) in - (* Determinacy_checker.check_clause ~loc ~functional_preds:func_setter_object#get_all_func body; *) + Determinacy_checker.check_clause ~loc ~env:functional_preds body ~modes; unknown else unknown) F.Map.empty clauses in @@ -1645,7 +1654,7 @@ end = struct else D.mkApp c x xs (* lambda terms *) | Const(Bound l,c) -> allocate_bound_symbol t.loc ctx (c,l) - | Lam(c,_,t) -> D.mkLam @@ todbl (push ctx c) t + | Lam(c,_,_,t) -> D.mkLam @@ todbl (push ctx c) t | App(Bound l,c,x,xs) -> let c = lookup_bound t.loc ctx (c,l) in let x = todbl ctx x in @@ -1690,7 +1699,7 @@ end = struct | Const(g,c) -> mkApp g c args | App(g,c,x,xs) -> mkApp g c (x :: xs @ args) | Var _ - | Discard | Lam (_, _, _) + | Discard | Lam (_, _, _, _) | CData _ | Spill (_, _) | Cast (_, _) -> assert false and aux_last = function | [] -> assert false @@ -1711,11 +1720,11 @@ end = struct (* barendregt_convention (naive implementation) *) let rec bc ctx t = match t with - | Lam(None,o,t) -> Lam(None,o,bc_loc ctx t) - | Lam(Some (c,l),o,t) when List.mem (c,l) ctx -> + | Lam(None,o,tya,t) -> Lam(None,o,tya,bc_loc ctx t) + | Lam(Some (c,l),o,tya,t) when List.mem (c,l) ctx -> let d = fresh () in - bc ctx (Lam(Some (d,l),o,rename_loc l c d t)) - | Lam(Some c,o,t) -> Lam (Some c,o, bc_loc (c :: ctx) t) + bc ctx (Lam(Some (d,l),o,tya,rename_loc l c d t)) + | Lam(Some c,o,tya,t) -> Lam (Some c,o,tya, bc_loc (c :: ctx) t) | Impl(b,t1,t2) -> Impl(b,bc_loc ctx t1, bc_loc ctx t2) | Cast(t,ty) -> Cast(bc_loc ctx t,ty) | Spill(t,i) -> Spill(bc_loc ctx t,i) @@ -1738,14 +1747,14 @@ end = struct let expr = app t vars in spills @ [{vars; vars_names; expr}], vars (* globals and builtins *) - | App(Global _ as f,c,{ it = Lam(Some v,o,t); loc = tloc; ty = tty },[]) when F.equal F.pif c -> + | App(Global _ as f,c,{ it = Lam(Some v,o,tya,t); loc = tloc; ty = tty },[]) when F.equal F.pif c -> let ctx = v :: ctx in let spilled, t = spill1 ctx t in - [], [{loc;ty;it = App(f,c,{ it = Lam(Some v,o,add_spilled spilled t); loc = tloc; ty = tty },[])}] - | App(Global _ as f,c,{ it = Lam(Some v,o,t); loc = tloc; ty = tty },[]) when F.equal F.sigmaf c -> + [], [{loc;ty;it = App(f,c,{ it = Lam(Some v,o,tya,add_spilled spilled t); loc = tloc; ty = tty },[])}] + | App(Global _ as f,c,{ it = Lam(Some v,o,tya,t); loc = tloc; ty = tty },[]) when F.equal F.sigmaf c -> let ctx = ctx in (* not to be put in scope of spills *) let spilled, t = spill1 ctx t in - [], [{loc;ty;it = App(f,c,{ it = Lam(Some v,o,add_spilled spilled t); loc = tloc; ty = tty },[])}] + [], [{loc;ty;it = App(f,c,{ it = Lam(Some v,o,tya,add_spilled spilled t); loc = tloc; ty = tty },[])}] | App(g,c,x,xs) -> let last = if F.equal F.andf c then List.length xs else -1 in let spills, args = List.split @@ List.mapi (fun i -> spill ~extra:(if i = last then extra else 0) ctx) (x :: xs) in @@ -1771,17 +1780,17 @@ end = struct let it = Impl(true,premise,conclusion) in [], [add_spilled spilled { it; loc; ty }] (* lambda terms *) - | Lam(None,o,t) -> + | Lam(None,o,tya,t) -> let spills, t = spill1 ctx t in - spills, [{ it = Lam(None,o,t); loc; ty }] - | Lam(Some c,o,t) -> + spills, [{ it = Lam(None,o,tya,t); loc; ty }] + | Lam(Some c,o,tya,t) -> let spills, t = spill1 (c::ctx) t in let (t,_), spills = map_acc (fun (t,n) { vars; vars_names; expr } -> let all_names = vars_names @ n in - (t,all_names), { vars; vars_names; expr = mk_loc ~loc @@ App(Scope.mkGlobal ~escape_ns:true (),F.pif,mk_loc ~loc @@ Lam(Some c,o,expr),[]) }) + (t,all_names), { vars; vars_names; expr = mk_loc ~loc @@ App(Scope.mkGlobal ~escape_ns:true (),F.pif,mk_loc ~loc @@ Lam(Some c,o,tya,expr),[]) }) (t,[]) spills in - spills, [{ it = Lam(Some c,o,t); loc; ty }] + spills, [{ it = Lam(Some c,o,tya,t); loc; ty }] (* holes *) | Var(c,xs) -> let spills, args = List.split @@ List.map (spill ctx) xs in @@ -2188,23 +2197,6 @@ let symtab : (constant * D.term) F.Map.t D.State.component = D.State.declare ~execution_is_over:(fun _ -> None) ~init:(fun () -> F.Map.empty) () - - -let global_name_to_constant state s = - let map = State.get symtab state in - fst @@ F.Map.find (F.from_string s) map - -let symtab : (constant * D.term) F.Map.t D.State.component = D.State.declare - ~descriptor:D.elpi_state_descriptor - ~name:"elpi:symbol_table" - ~pp:(fun fmt _ -> Format.fprintf fmt "") - ~clause_compilation_is_over:(fun x -> x) - ~goal_compilation_begins:(fun x -> x) - ~goal_compilation_is_over:(fun ~args:_ x -> Some x) - ~compilation_is_over:(fun x -> Some x) - ~execution_is_over:(fun _ -> None) - ~init:(fun () -> F.Map.empty) - let global_name_to_constant state s = let map = State.get symtab state in diff --git a/src/compiler/compiler_data.ml b/src/compiler/compiler_data.ml index ae4e0cf6e..dec3b2f4d 100644 --- a/src/compiler/compiler_data.ml +++ b/src/compiler/compiler_data.ml @@ -4,23 +4,37 @@ open Elpi_runtime open Util module F = Ast.Func +module IdPos : sig + type t [@@deriving show,ord] + module Map : Map.S with type key = t + module Set : Set.S with type elt = t + + val make_loc : Loc.t -> t + val make_str : string -> t +end = struct + include Loc + module Map = Map.Make(Loc) + module Set = Set.Make(Loc) + let make_loc loc = loc + let make_str str = make_loc (Loc.initial str) +end + module Scope = struct type language = string [@@ deriving show, ord] - type type_decl_id = int + type type_decl_id = IdPos.t [@@ deriving show, ord] - let dummy_type_decl_id = 0 - let fresh_type_decl_id = - let i = ref 0 in fun () -> incr i; !i + let dummy_type_decl_id = IdPos.make_str "dummy" + let fresh_type_decl_id loc = (IdPos.make_loc loc) let is_dummy_type_decl_id x = x <= 0 type t = | Bound of language (* bound by a lambda, stays bound *) | Global of { escape_ns : bool; (* when true name space elimination does not touch this constant *) - (* mutable decl_id : type_decl_id; [@equal fun _ _ -> true XXX since it is broken ] type checking assigns a unique id *) + mutable decl_id : type_decl_id; } [@@ deriving show, ord] @@ -34,7 +48,7 @@ module Scope = struct end) let mkGlobal ?(escape_ns=false) ?(decl_id = dummy_type_decl_id) () = - Global { escape_ns (*; decl_id*) } + Global { escape_ns ; decl_id } end let elpi_language : Scope.language = "lp" @@ -241,7 +255,7 @@ module TypeAssignment = struct type overloaded_skema = skema overloading [@@ deriving show] - type skema_w_id = int * skema + type skema_w_id = IdPos.t * skema [@@ deriving show, ord] type overloaded_skema_with_id = skema_w_id overloading [@@ deriving show] @@ -282,7 +296,7 @@ module TypeAssignment = struct let apply (_,sk:skema_w_id) args = apply F.Map.empty sk args let eq_skema_w_id (_,x) (_,y) = compare_skema x y = 0 - let diff_id_check ((id1:int),_) (id2,_) = assert (id1<>id2) + let diff_id_check ((id1:IdPos.t),_) (id2,_) = assert (id1<>id2) let diff_ids_check e = List.iter (diff_id_check e) let rec remove_mem e acc = function @@ -440,7 +454,7 @@ module ScopedTerm = struct | Discard | Var of F.t * t list | App of Scope.t * F.t * t * t list - | Lam of (F.t * Scope.language) option * ScopedTypeExpression.e option * t + | Lam of (F.t * Scope.language) option * ScopedTypeExpression.e option * TypeAssignment.t MutableOnce.t * t | CData of CData.t | Spill of t * spill_info ref | Cast of t * ScopedTypeExpression.e @@ -459,18 +473,26 @@ module ScopedTerm = struct | Lam _ -> lam | _ -> 2 - let rec pretty fmt { it } = pretty_ fmt it + let get_lam_name = function None -> F.from_string "_" | Some (n,_) -> n + let mk_empty_lam_type name = MutableOnce.make (get_lam_name name) + + let rec pretty_lam fmt n ste (mta:TypeAssignment.t MutableOnce.t) it = + fprintf fmt "%a" F.pp (get_lam_name n); + if MutableOnce.is_set mta then + fprintf fmt ": %a " TypeAssignment.pretty (match MutableOnce.get mta with Val a -> a) + else Option.iter (fun e -> fprintf fmt ": %a " ScopedTypeExpression.pretty_e e) ste; + fprintf fmt "\\ %a" pretty it; + + and pretty fmt { it } = pretty_ fmt it and pretty_ fmt = function | Impl(true,t1,t2) -> fprintf fmt "(%a => %a)" pretty t1 pretty t2 | Impl(_,t1,t2) -> fprintf fmt "(%a :- %a)" pretty t1 pretty t2 | Const(_,f) -> fprintf fmt "%a" F.pp f | Discard -> fprintf fmt "_" - | Lam(None,None,t) -> fprintf fmt "_\\ %a" pretty t - | Lam(None,Some ty,t) -> fprintf fmt "_ : %a\\ %a" ScopedTypeExpression.pretty_e ty pretty t - | Lam(Some (f,_),None,t) -> fprintf fmt "%a\\ %a" F.pp f pretty t - | Lam(Some (f,_),Some ty,t) -> fprintf fmt "%a : %a\\ %a" F.pp f ScopedTypeExpression.pretty_e ty pretty t + | Lam(n, ste, mta, it) -> pretty_lam fmt n ste mta it | App(Global _,f,x,[]) when F.equal F.spillf f -> fprintf fmt "{%a}" pretty x - | App(_,f,x,xs) -> fprintf fmt "%a %a" F.pp f (Util.pplist ~pplastelem:(pretty_parens_lam ~lvl:app) (pretty_parens ~lvl:app) " ") (x::xs) + | App(_,f,x,xs) when F.equal F.pif f || F.equal F.sigmaf f -> fprintf fmt "%a %a" F.pp f (Util.pplist ~pplastelem:(pretty_parens_lam ~lvl:app) (pretty_parens ~lvl:app) " ") (x::xs) + | App(_,f,x,xs) -> fprintf fmt "%a %a" F.pp f (Util.pplist (pretty_parens ~lvl:app) " ") (x::xs) | Var(f,[]) -> fprintf fmt "%a" F.pp f | Var(f,xs) -> fprintf fmt "%a %a" F.pp f (Util.pplist (pretty_parens ~lvl:app) " ") xs | CData c -> fprintf fmt "%a" CData.pp c @@ -482,7 +504,7 @@ module ScopedTerm = struct if lvl >= lvl_of it then fprintf fmt "(%a)" pretty_ it else pretty_ fmt it and pretty_parens_lam ~lvl fmt x = - match x.it with Lam _ -> pretty_ fmt x.it | _ -> pretty_parens ~lvl fmt x + match x.it with Lam _ -> fprintf fmt "%a" pretty_ x.it | _ -> pretty_parens ~lvl fmt x let equal ?(types=true) t1 t2 = @@ -494,8 +516,8 @@ module ScopedTerm = struct | Var(n1,l1), Var(n2,l2) -> eq_uvar ctx n1 n2 && Util.for_all2 (eq ctx) l1 l2 | App(Global _ as b1,c1,x,xs), App(Global _ as b2,c2,y,ys) -> b1 = b2 && F.equal c1 c2 && eq ctx x y && Util.for_all2 (eq ctx) xs ys | App(Bound l1,c1,x,xs), App(Bound l2,c2,y,ys) -> l1 = l2 && eq_var ctx l1 c1 c2 && eq ctx x y && Util.for_all2 (eq ctx) xs ys - | Lam(None,ty1, b1), Lam (None,ty2, b2) -> eq ctx b1 b2 && (not types || Option.equal (ScopedTypeExpression.eqt (empty ())) ty1 ty2) - | Lam(Some (c1,l1),ty1,b1), Lam(Some (c2,l2),ty2, b2) -> l1 = l2 && eq (push_ctx l1 c1 c2 ctx) b1 b2 && (not types || Option.equal (ScopedTypeExpression.eqt (empty ())) ty1 ty2) + | Lam(None,ty1, _,b1), Lam (None,ty2,_, b2) -> eq ctx b1 b2 && (not types || Option.equal (ScopedTypeExpression.eqt (empty ())) ty1 ty2) + | Lam(Some (c1,l1),ty1,_,b1), Lam(Some (c2,l2),ty2,_, b2) -> l1 = l2 && eq (push_ctx l1 c1 c2 ctx) b1 b2 && (not types || Option.equal (ScopedTypeExpression.eqt (empty ())) ty1 ty2) | Spill(b1,n1), Spill (b2,n2) -> n1 == n2 && eq ctx b1 b2 | CData c1, CData c2 -> CData.equal c1 c2 | Cast(t1,ty1), Cast(t2,ty2) -> eq ctx t1 t2 && (not types || ScopedTypeExpression.eqt (empty ()) ty1 ty2) @@ -523,7 +545,7 @@ module ScopedTerm = struct | Const(s,c) -> Const(s,c) | Opaque c -> CData c | Cast(t,ty) -> Cast(of_simple_term_loc t, ScopedTypeExpression.of_simple_type_loc ty) - | Lam(c,ty,t) -> Lam(c,Option.map ScopedTypeExpression.of_simple_type_loc ty,of_simple_term_loc t) + | Lam(c,ty,t) -> Lam(c,Option.map ScopedTypeExpression.of_simple_type_loc ty, mk_empty_lam_type c,of_simple_term_loc t) | App(s,c,x,xs) when F.equal c F.implf || F.equal c F.implf -> begin match xs with | [y] -> Impl(F.equal c F.implf,of_simple_term_loc x, of_simple_term_loc y) @@ -550,8 +572,8 @@ module ScopedTerm = struct | App(Bound l',c',x,xs) when l = l' && F.equal c c' -> App(Bound l,d,rename_loc l c d x, List.map (rename_loc l c d) xs) | App(g,v,x,xs) -> App(g,v,rename_loc l c d x, List.map (rename_loc l c d) xs) - | Lam(Some (c',l'),_,_) when l = l' && F.equal c c' -> t - | Lam(v,ty,t) -> Lam(v,ty,rename_loc l c d t) + | Lam(Some (c',l'),_,_,_) when l = l' && F.equal c c' -> t + | Lam(v,ty,tya,t) -> Lam(v,ty,tya,rename_loc l c d t) | Spill(t,i) -> Spill(rename_loc l c d t,i) | Cast(t,ty) -> Cast(rename_loc l c d t,ty) | Var(v,xs) -> Var(v,List.map (rename_loc l c d) xs) @@ -566,27 +588,27 @@ module ScopedTerm = struct | Var (_,args) -> List.fold_left fv acc args | App(Bound l,c,x,xs) -> List.fold_left fv (Scope.Set.add (c,l) acc) (x::xs) | App(Global _,_,x,xs) -> List.fold_left fv acc (x::xs) - | Lam(None,_,t) -> fv acc t - | Lam(Some (c,l),_,t) -> Scope.Set.union acc @@ Scope.Set.remove (c,l) (fv Scope.Set.empty t) + | Lam(None,_,_,t) -> fv acc t + | Lam(Some (c,l),_,_,t) -> Scope.Set.union acc @@ Scope.Set.remove (c,l) (fv Scope.Set.empty t) | Spill(t,_) -> fv acc t | Cast(t,_) -> fv acc t | Discard | Const _ | CData _ -> acc in let rec load_subst ~loc t (args : t list) map fvset = match t, args with - | Lam(None,_,t), _ :: xs -> load_subst_loc t xs map fvset - | Lam(Some c,_,t), x :: xs -> load_subst_loc t xs (Scope.Map.add c x map) (fv fvset x) + | Lam(None,_,_,t), _ :: xs -> load_subst_loc t xs map fvset + | Lam(Some c,_,_,t), x :: xs -> load_subst_loc t xs (Scope.Map.add c x map) (fv fvset x) | t, xs -> app ~loc (subst map fvset t) xs and load_subst_loc { it; loc } args map fvset = load_subst ~loc it args map fvset and subst (map : t Scope.Map.t) fv t = match t with | Impl(b,t1,t2) -> Impl(b,subst_loc map fv t1, subst_loc map fv t2) - | Lam(None,ty,t) -> Lam(None,ty,subst_loc map fv t) - | Lam(Some (c,l),ty,t) when not @@ Scope.Map.mem (c,l) map && not @@ Scope.Set.mem (c,l) fv -> - Lam(Some (c,l),ty,subst_loc map fv @@ t) - | Lam(Some (c,l),ty,t) -> + | Lam(None,ty,tya,t) -> Lam(None,ty,tya,subst_loc map fv t) + | Lam(Some (c,l),ty,tya,t) when not @@ Scope.Map.mem (c,l) map && not @@ Scope.Set.mem (c,l) fv -> + Lam(Some (c,l),ty,tya,subst_loc map fv @@ t) + | Lam(Some (c,l),ty,tya,t) -> let d = fresh () in - Lam(Some (d,l),ty,subst_loc map fv @@ rename_loc l c d t) + Lam(Some (d,l),ty,tya,subst_loc map fv @@ rename_loc l c d t) | Const(Bound l,c) when Scope.Map.mem (c,l) map -> unlock @@ Scope.Map.find (c,l) map | Const _ -> t | App(Bound l,c,x,xs) when Scope.Map.mem (c,l) map -> @@ -653,6 +675,14 @@ module ScopedTerm = struct end | _ -> false end + + let rec get_clause_hd = function + | Const (_,c) -> c + | App(_,n,_,_) -> n + | Impl(false,l,_) -> get_clause_hd l.it + | _ -> error "Not a clause" + + let is_var = function Var _ -> true | _ -> false end diff --git a/src/compiler/determinacy_checker.ml b/src/compiler/determinacy_checker.ml index 7a59dbabb..91eaa36c1 100644 --- a/src/compiler/determinacy_checker.ml +++ b/src/compiler/determinacy_checker.ml @@ -1,235 +1,589 @@ (* elpi: embedded lambda prolog interpreter *) (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) -open Elpi_util -open Util -open Elpi_parser -open Ast +open Elpi_util.Util +open Elpi_parser.Ast open Compiler_data - module C = Constants -exception StopCheck +let to_print f = if true then f () (* TYPE DECLARATION FOR FUNCTIONALITY *) -type f = - | Functional of f list (* Used for functional preds, the f list represents the functionality relation of the arguments *) - | Relational of f list (* Used for non-functional preds, the f list represents the functionality relation of the arguments *) - | NoProp (* Used for kinds like list, int, string... and abstractions not being props like: (int -> list bool), (string -> nat -> string) *) - | AssumedFunctional (* Currently used for variadic functions, like print, halt... *) - | BoundVar of F.t -[@@ deriving show, ord] +type functionality = + | Functional (** -> for functional preds *) + | Relational (** -> for non-functional preds *) + | NoProp of functionality list (** -> for kinds like list, int, string *) + | BoundVar of F.t (** -> in predicates like: std.exists or in parametric type abbreviations. *) + | AssumedFunctional (** -> variadic predicates: never backtrackc *) + | Arrow of functionality * functionality (** -> abstractions *) + | Any +[@@deriving show, ord] + +type functionality_abs = + | Lam of F.t * functionality_abs (** e.g: type abbrev (t X) (list X) becomes: Lam A (F (Arrow A NoProp))*) + | F of functionality +[@@deriving show, ord] + +type functionality_loc = Loc.t * functionality_abs [@@deriving show, ord] +type t = { ty_abbr : functionality_loc F.Map.t; cmap : (F.t * functionality) IdPos.Map.t } [@@deriving show, ord] + +let arr a b = Arrow (a, b) +let rec bvars2any = function Arrow (l, r) -> arr (bvars2any l) (bvars2any r) | BoundVar _ -> Any | e -> e +let rec eat_lambdas = function Lam (_, b) -> eat_lambdas b | F b -> bvars2any b + +type env = t (* This is for the cleaner signatures in this files for objects with type t *) + +let compare_functionality_loc a b = compare_functionality_abs (snd a) (snd b) +let compare_fname a b = compare_functionality_loc (snd a) (snd b) +let mk_func_map ty_abbr cmap = { ty_abbr; cmap } +let empty_fmap = { ty_abbr = F.Map.empty; cmap = IdPos.Map.empty } +let get_functionality_tabbr_opt map k = F.Map.find_opt k map.ty_abbr + +let rec get_namef = function + | ScopedTerm.App (_, n, _, _) | Const (_, n) -> n + | Impl (false, a, _) -> get_namef a.it + | Var (n, _) -> n + | e -> error (Format.asprintf "get_name error is not a clause %a" ScopedTerm.pretty_ e) + +let functionality_pi_sigma = arr (arr Any Functional) Functional + +let get_functionality ~loc ~env k = + if k = Scope.dummy_type_decl_id then Any + else + try + let name, func = IdPos.Map.find k env.cmap in + if F.equal F.pif name || F.equal F.sigmaf name then functionality_pi_sigma else func + with e -> + Format.eprintf "Error at %a with const %a\n%!" Loc.pp loc IdPos.pp k; + raise e -type t' = Lam of F.t * t' | F of f [@@ deriving show, ord] -type t = Loc.t * t' [@@ deriving show, ord] +(* AUXILIARY FUNCTIONS *) +let rec subst ~loc sigma = function + | BoundVar k as t -> ( + match F.Map.find_opt k sigma with + | None -> t + | Some (F f) -> f + | Some (Lam (_, b)) -> error ~loc "type_abbrev not fully applied") + | Arrow (l, r) -> arr (subst ~loc sigma l) (subst ~loc sigma r) + | NoProp l -> NoProp (List.map (subst ~loc sigma) l) + | (AssumedFunctional | Functional | Relational | Any) as t -> t + +let rec beta ~loc sigma = function + | Lam (n, b), x :: xs -> beta ~loc (F.Map.add n (F x) sigma) (b, xs) + | Lam (_, b), [] -> error ~loc "type_abbrev is not fully applied" + | F t, [] -> subst ~loc sigma t + | F _, _ :: _ -> anomaly ~loc "type_abbrev is too much applied" -type func_map = { - ty_abbr: Scope.type_decl_id F.Map.t; (* Invariant every type_abbrev const is already in cmap *) - cmap: (F.t * t) C.Map.t -} [@@ deriving show, ord] +let beta = beta F.Map.empty -type fname = F.t * t [@@deriving show,ord] +(* COMPILATION from SCOPE_TYPE_EXPRESSION TO FUNCTIONALITY *) +module Compilation = struct + let add_type ~loc is_type_abbr env ~n ~id v = + if is_type_abbr && F.Map.mem n env.ty_abbr then error (Format.asprintf "Adding again type_abbrev %a" F.pp n); + if is_type_abbr then + let ty_abbr = F.Map.add n (loc, v) env.ty_abbr in + mk_func_map ty_abbr env.cmap + else + let cmap = IdPos.Map.add id (n, eat_lambdas v) env.cmap in + mk_func_map env.ty_abbr cmap + + let merge f1 f2 = + let pp_fname fmt (x, y) = Format.fprintf fmt "(%a,%a)" F.pp x pp_functionality_loc y in + let compare_fname (x0, y0) (x1, y1) = + let cmp = F.compare x0 x1 in + if cmp = 0 then compare_functionality_loc y0 y1 else cmp + in + let union_same pk pe cmpe k e1 e2 = + (* if cmpe e1 e2 = 0 then *) + Some e1 + (* else error (Format.asprintf "The key %a has two different values (v1:%a) (v2:%a)" pk k pe e1 pe e2) *) + in + let cmap = IdPos.Map.union (union_same pp_int pp_fname compare_fname) f1.cmap f2.cmap in + let ty_abbr = F.Map.union (union_same F.pp pp_int Int.compare) f1.ty_abbr f2.ty_abbr in + mk_func_map ty_abbr cmap -let pp_locs fmt (l: t list) = - Format.fprintf fmt "[%a]" (pplist (fun fmt -> Format.fprintf fmt "%a" Loc.pp) ",") (List.map fst l) + let rec arr2list = function ScopedTypeExpression.Arrow (_, l, r) -> l.it :: arr2list r.it | e -> [] + let rec fold last f = function [] -> last | x :: xs -> arr (f x) (fold last f xs) + let apply_snd f (_, a) = f a + + let rec type2func_ty_abbr ~pfile ~loc bound_vars (env : env) c args = + match get_functionality_tabbr_opt env c with + | None -> + (* -> c is a kind (like list, int, ...) *) + NoProp (List.map (type2func_loc ~pfile ~loc bound_vars env) args) + | Some (_, f) -> + (* -> c is a type-abbrev *) + beta ~loc (f, List.map (type2func_loc ~pfile ~loc bound_vars env) args) + + and type2func ~pfile ~loc bound_vars (env : env) = function + | ScopedTypeExpression.Pred (Function, xs) -> + fold Functional (apply_snd @@ type2func_loc ~pfile ~loc bound_vars env) xs + | Pred (Relation, xs) -> fold Relational (apply_snd @@ type2func_loc ~pfile ~loc bound_vars env) xs + | Const (_, c) when F.Set.mem c bound_vars -> BoundVar c + | Const (_, c) -> type2func_ty_abbr ~pfile ~loc bound_vars env c [] + | App (c, x, xs) -> type2func_ty_abbr ~pfile ~loc bound_vars env c (x :: xs) + | Arrow (Variadic, _, _) -> AssumedFunctional + (* Invariant: the rightmost type in the right branch is not a prop due flatten_arrows in compiler *) + | Arrow (NotVariadic, l, r) -> + arr (type2func_loc ~pfile ~loc bound_vars env l) (type2func_loc ~pfile ~loc bound_vars env r) + | Any -> Any -let compare_t (a:t) (b:t) = compare_t' (snd a) (snd b) + and type2func_loc ~pfile ~loc bvars env ScopedTypeExpression.{ it } = type2func ~pfile ~loc bvars env it -let compare_fname a b = compare_t (snd a) (snd b) + let rec type2func_lam ~pfile bound_vars type_abbrevs = function + | ScopedTypeExpression.Lam (n, t) -> + let loc, r = type2func_lam ~pfile (F.Set.add n bound_vars) type_abbrevs t in + (loc, Lam (n, r)) + | Ty { it; loc } -> (loc, F (type2func ~pfile ~loc bound_vars type_abbrevs it)) -let mk_func_map ty_abbr cmap = {ty_abbr; cmap} + let type2func env (x : ScopedTypeExpression.t) = type2func_lam F.Set.empty env x.value ~pfile:None +end -let empty_fmap = {ty_abbr = F.Map.empty; cmap = C.Map.empty} +let merge = Compilation.merge -let get_functionality_tabbr_opt map k = match F.Map.find_opt k map.ty_abbr with - None -> None | Some e -> Some (C.Map.find e map.cmap) +let rec functionality_leq ~loc a b = + match (a, b) with + | NoProp _, x -> functionality_leq ~loc Any x + | x, NoProp _ -> functionality_leq ~loc x Any + | _, Any -> true + | Any, _ -> false + | BoundVar _, _ | _, BoundVar _ -> true (* TODO: this is not correct... -> use ref with uvar to make unification *) + | _, Relational -> true + | Relational, _ -> false + | Functional, Functional -> true + | AssumedFunctional, _ -> true + | _, AssumedFunctional -> error ~loc (Format.asprintf "Cannot compare AssumedFunctional with different functionality") + | Arrow (l1, r1), Arrow (l2, r2) -> functionality_leq ~loc l2 l1 && functionality_leq ~loc r1 r2 + | Arrow _, _ | _, Arrow _ -> + error ~loc (Format.asprintf "Type error1 in comparing %a and %a" pp_functionality a pp_functionality b) +(* | NoProp _, _ | _, NoProp _ -> error ~loc "Type error2" *) + +let functionality_leq ~loc a b = + let res = functionality_leq ~loc a b in + Format.eprintf "Going to compare %a and %a = %b@." pp_functionality a pp_functionality b res; + res + +let functionality_leq_error ~loc ?(pref = "") a b = + if not (functionality_leq ~loc a b) then + error ~loc + (Format.asprintf "[%s] Functionality error at %a is not less then %a" pref pp_functionality a pp_functionality b) + +let split_bang t = + let rec split_bang_list bef aft = function + | [] -> (bef, aft) + | x :: xs -> + let bef, aft = split_bang bef aft x in + split_bang_list bef aft xs + and split_bang bef aft (ScopedTerm.{ it } as t) = + match it with + | Const (_, t) when F.equal F.cutf t -> (List.append bef (List.rev aft), []) + | App (_, hd, x, xs) when F.equal F.andf hd -> split_bang_list bef aft (x :: xs) + | _ -> (bef, t :: aft) + and split_bang_loc bef aft t = split_bang bef aft t in + let bef, aft = split_bang_loc [] [] t in + (bef, List.rev aft) + +let min ~loc f1 f2 = if functionality_leq ~loc f1 f2 then f1 else f2 +let max ~loc f1 f2 = if functionality_leq ~loc f1 f2 then f2 else f1 + +module EnvMaker (M : Map.S) : sig + type t [@@deriving show] + + val add : loc:Loc.t -> v:functionality -> t -> M.key -> t + val get : t -> M.key -> functionality option + val mem : t -> M.key -> bool + val empty : t +end = struct + type t = functionality ref M.t [@@deriving show] + + let add ~loc ~(v : functionality) (env : t) (n : M.key) : t = + match M.find_opt n env with + | None -> M.add n (ref v) env + | Some v' -> + (* functionality_leq_error ~loc ~pref:("Adding setted var " ^ M.show_key n) v !v'; *) + v' := min ~loc v !v'; + env + + let get (env : t) (k : M.key) = + try Option.map (fun x -> !x) (M.find_opt k env) + with e -> + Format.eprintf "Cannot find the key %a in the map\n" M.pp_key k; + raise e + + let mem env k = M.mem k env + let empty = M.empty +end -let get_functionality map k = C.Map.find k map.cmap +module Env = EnvMaker (F.Map) +module Ctx = EnvMaker (Scope.Map) + +let eat_abs ~loc = function + | AssumedFunctional -> (Any, AssumedFunctional) + | Any -> (Any, Any) + | Arrow (l, r) -> (l, r) + | BoundVar _ -> error ~loc "TODO:?" + | _ -> error ~loc "Type error3" + +let not_functional_call_error ~loc t = + error ~loc (Format.asprintf "Non functional premise call %a\n" ScopedTerm.pretty_ t) + +module Checker_clause = struct + let check ~modes ~(global : env) ~loc tm = + let env = ref Env.empty in + let pp_env fmt () : unit = Format.fprintf fmt "Env : %a" Env.pp !env in + let add_env ~v n = env := Env.add ~loc !env ~v n in + let not_mem n = Env.mem !env n |> not in + let add_ctx ctx ~v n = Ctx.add ~loc ctx ~v n in + + let get_mode c = + match F.Map.find_opt c modes with + | None -> error ~loc (Format.asprintf "Cannot find mode for %a" F.pp c) + | Some (e, _) -> List.map (function Fo m | Ho (m, _) -> m) e + in -(* AUXILIARY FUNCTIONS *) -let rec subst ~loc sigma : f -> f = function - | BoundVar k as t -> - begin match F.Map.find_opt k sigma with - | None -> t - | Some (F f) -> f - | Some (Lam (_,b)) -> error ~loc "type_abbrev not fully applied" - end - | Functional l -> Functional (List.map (subst ~loc sigma) l) - | AssumedFunctional | Relational _ | NoProp as t -> t - -let rec bind ~loc sigma : (t'*f list) -> f = function - | Lam (n,b), x::xs -> bind ~loc (F.Map.add n (F x) sigma) (b,xs) - | Lam (_,b), [] -> error ~loc "type_abbrev is not fully applied" - | F t, [] -> subst ~loc sigma t - | F _, _::_ -> anomaly ~loc "type_abbrev is too much applied" + let rec fold_left_partial f acc args modes = + match (args, modes) with + | [], _ -> acc + | x :: xs, y :: ys -> fold_left_partial f (f acc x y) xs ys + | _ :: _, [] -> error ~loc:tm.ScopedTerm.loc "Invalid application" + in -(* COMPILATION from SCOPE_TYPE_EXPRESSION TO FUNCTIONALITY *) -module Compilation = struct - let add_type is_type_abbr fmap ~n ~id v = - (* if F.Map.mem n fmap.ty_abbr then - error (Format.asprintf "Adding again type_abbrev %a" F.pp n); *) - let cmap = C.Map.add id (n,v) fmap.cmap in - let ty_abbr = if is_type_abbr then F.Map.add n id fmap.ty_abbr else fmap.ty_abbr in - mk_func_map ty_abbr cmap + let fold_on_modes input output tm args modes = + fold_left_partial + (fun func arg mode -> + match func with + | Any -> Any + | Arrow (l, r) -> if mode = Input then input arg l r else output arg l r + | _ -> error ~loc:arg.ScopedTerm.loc "Type error") + tm args modes + in - let merge f1 f2 = - let union_same pk pe cmpe k e1 e2 = - (* if cmpe e1 e2 = 0 then *) - Some e1 - (* else error (Format.asprintf "The key %a has two different values (v1:%a) (v2:%a)" pk k pe e1 pe e2) *) + let get_funct_of_term ctx = function + | ScopedTerm.Var (v, args) -> Env.get !env v + | Const (Global { decl_id }, _) -> + Some (match get_functionality ~loc ~env:global decl_id with Relational -> Functional | e -> e) + | App (Global { decl_id }, _, _, _) -> Some (get_functionality ~loc ~env:global decl_id) + | App (Bound scope, f, _, _) | Const (Bound scope, f) -> Ctx.get ctx (f, scope) + | CData _ -> Some (NoProp []) + | Spill _ -> error ~loc "get_funct_of_term of spilling: " + | e -> error ~loc (Format.asprintf "get_funct_of_term %a" ScopedTerm.pp_t_ e) in - let cmap = C.Map.union (union_same pp_int pp_fname compare_fname) f1.cmap f2.cmap in - let ty_abbr = F.Map.union (union_same F.pp pp_int Int.compare) f1.ty_abbr f2.ty_abbr in - mk_func_map ty_abbr cmap - let map_snd f = List.map (fun (_, ScopedTypeExpression.{it}) -> f it) + let get_func_hd ctx t = + let rec get_right_most = function Arrow (_, r) -> get_right_most r | e -> e in + Option.value ~default:Any (get_funct_of_term ctx t) |> get_right_most + in - let rec type2func_ty_abbr ~loc bound_vars (fmap: func_map) c args = - match get_functionality_tabbr_opt fmap c with - | None -> NoProp (* -> c is a kind (like list, int, ...) *) - | Some (_,f) -> (* -> c is a type-abbrev *) - bind ~loc F.Map.empty (snd f, List.map (type2func_loc ~loc bound_vars fmap) args) + let functionality_beta f args ctx = + Format.eprintf "To be reduced: %a applied to the func of %a in env: %a@." pp_functionality f + (pplist ScopedTerm.pretty ",,,, ") args pp_env (); + let xs = List.map (fun ScopedTerm.{ it } -> get_funct_of_term ctx it) args in + let rec aux = function + | Some x :: xs, _ :: args, Arrow (l, r) -> + Format.eprintf "x is %a and l is %a\n" pp_functionality x pp_functionality l; + if functionality_leq ~loc x l then aux (xs, args, r) else Any + | None :: xs, ScopedTerm.{ it = Var (name, _args) } :: args, Arrow ((NoProp _ as np), r) -> + (* TODO: consider args... *) + add_env name ~v:np; + aux (xs, args, r) + | None :: xs, _, _ -> Any + | [], _, f -> f + | _ -> error ~loc "Type error4" + in + aux (xs, args, f) + in - and type2func ~loc bound_vars (fmap: func_map) : ScopedTypeExpression.t_ -> f = function - | Pred(Function, xs) -> Functional (map_snd (type2func ~loc bound_vars fmap) xs) - | Pred(Relation, xs) -> Relational (map_snd (type2func ~loc bound_vars fmap) xs) - | Const (_,c) when F.Set.mem c bound_vars -> BoundVar c - | Const (_,c) -> type2func_ty_abbr ~loc bound_vars fmap c [] - | App(c,x,xs) -> type2func_ty_abbr ~loc bound_vars fmap c (x::xs) - | Arrow (Variadic, _, _) -> AssumedFunctional - (* Invariant: the rightmost type in the right branch is not a prop due flatten_arrows in compiler *) - | Arrow (NotVariadic,_,_) -> NoProp - | Any -> NoProp - and type2func_loc ~loc bvars fmap ScopedTypeExpression.{it} = type2func ~loc bvars fmap it + let rec unify_func (t1 : ScopedTerm.t_) (t2 : ScopedTerm.t_) (ctx : Ctx.t) : unit = + match (t1, t2) with + (* No var is set *) + | Var (_n, _args), Var (_n1, args1) when not_mem _n && not_mem _n1 -> + error ~loc (Format.asprintf "Var-var case in unfy-func v1:%a - v2:%a" ScopedTerm.pp_t_ t1 ScopedTerm.pp_t_ t2) + (* Left var is set *) + | Var (_n, _args), Var (_n1, args1) when not_mem _n1 -> + add_env + ~v:(get_funct_of_term ctx t1 |> Option.get) + _n1 (* TODO: THIS IS WRONG: SHOULD TAKE INTO ACCOUNT THE ARGS OF BOTH VARS... *) + (* Right var is set *) + | Var (_n, _args), Var (_n1, args1) when not_mem _n -> + add_env + ~v:(get_funct_of_term ctx t2 |> Option.get) + _n (* TODO: THIS IS WRONG: SHOULD TAKE INTO ACCOUNT THE ARGS OF BOTH VARS... *) + (* Both var are set *) + | Var (_n, _args), Var (_n1, args1) -> assert (get_funct_of_term ctx t1 = get_funct_of_term ctx t2) + (* TODO: THIS IS WRONG: SHOULD TAKE INTO ACCOUNT THE ARGS OF BOTH VARS... *) + (* The variable is not set *) + | Var (vname, args), App (_, n, x, xs) when not_mem vname -> + Format.eprintf "Going to make beta reduction of %a with func = %a@." F.pp n pp_functionality + (get_funct_of_term ctx t2 |> Option.get); + let v = functionality_beta (get_funct_of_term ctx t2 |> Option.get) (x :: xs) ctx in + Format.eprintf "Beta reduced functionality is %a@." pp_functionality v; + add_env vname ~v + | Var (vname, args), Const _ when not_mem vname -> add_env vname ~v:(get_funct_of_term ctx t2 |> Option.get) + (* The variable is set into the dict *) + | Var (vname, args), App (_, n, x, xs) -> + let func_t2 = get_funct_of_term ctx t2 |> Option.get in + Format.eprintf "Functionality unification of %a and %a@." ScopedTerm.pretty_ t1 ScopedTerm.pretty_ t2; + let v = functionality_beta func_t2 (x :: xs) ctx in + Format.eprintf "Beta reduced functionality is %a@." pp_functionality v; + add_env vname ~v + | Var (vname, args), Const _ -> add_env vname ~v:(get_funct_of_term ctx t2 |> Option.get) + (* Swap call *) + | x, Var _ when not (ScopedTerm.is_var x) -> unify_func t2 t1 ctx + | _ -> + error ~loc + (Format.asprintf "trying to unify \n- %a and \n- %a in \n %a@." ScopedTerm.pretty_ t1 ScopedTerm.pretty_ t2 + pp_env ()) + in - let rec type2func_lam bound_vars type_abbrevs : ScopedTypeExpression.v_ -> t = function - | Lam (n, t) -> - let (loc, r) = type2func_lam (F.Set.add n bound_vars) type_abbrevs t in - loc, Lam (n,r) - | Ty {it;loc} -> loc, F (type2func ~loc bound_vars type_abbrevs it) + let check_head_input = + let rec build_hyps_head_aux ctx = function + | [], _ -> () + | ScopedTerm.{ it } :: tl, Arrow (l, r) -> + build_hyp_head ctx l it; + build_hyps_head_aux ctx (tl, r) + | _ :: _, _ -> anomaly "Type error5" + and build_hyp_head (ctx : Ctx.t) (assumed : functionality) (t : ScopedTerm.t_) = + match t with + | ScopedTerm.Const _ | Discard | CData _ -> () + | Var (n, _args) -> add_env n ~v:assumed + | Lam (None, _, _type, { it }) -> build_hyp_head ctx (eat_abs ~loc assumed |> snd) it + | Lam (Some x, _, _type, { it }) -> + let v, assumed = eat_abs ~loc assumed in + build_hyp_head (add_ctx ctx x ~v) assumed it (* TODO: Here I use any instead of Relational ...*) + | Impl (true, _hd, { it }) -> () (* TODO: this is ignored *) + | Impl (false, _, _) -> () (* TODO: this is ignored *) + | App (_, n, x, [ y ]) when F.equal F.isf n || F.equal F.eqf n -> unify_func x.it y.it ctx + (* | App (_, n, x, [ y ]) when F.equal F.isf n || F.equal F.eqf n -> unify_func x.it y.it ctx *) + | App (_, n, x, xs) -> ( + to_print (fun () -> + Format.eprintf ".The global app is %a and its functionality is %a@." F.pp n + (Format.pp_print_option pp_functionality) + (get_funct_of_term ctx t)); + match get_funct_of_term ctx t with + | None -> () (* TODO: The functionality of t is not already known... should be taken into account *) + | Some e -> ( + (* TODO: check functionality of e is leq of exp: otherwise we can raise a warning? *) + (* TODO: in the head, if we expect a relational prop, and we destruct a functional term, then all args of the term are relational *) + match e with + | Any | BoundVar _ | AssumedFunctional -> + build_hyps_head_aux ctx (x :: xs, List.fold_right (fun _ acc -> arr Any acc) (x :: xs) Any) + | Functional | Relational | NoProp _ -> assert false + | Arrow (l, r) -> build_hyps_head_aux ctx (x :: xs, e))) + | Cast ({ it }, _) -> build_hyp_head ctx assumed it + | Spill _ -> error ~loc "Spill in the head" + and build_hyps_head_modes ctx func args modes = match args, func, modes with + | [],_,_ -> () + | arg::args, Arrow (l,r), Input :: modes -> + build_hyp_head ctx l arg.ScopedTerm.it; + build_hyps_head_modes ctx r args modes + | _::args, Arrow (_,r), Output :: modes -> + build_hyps_head_modes ctx r args modes + | _, _, _ -> error ~loc (Format.asprintf "Type error %a [%a] [%a]" pp_functionality func (pplist ScopedTerm.pretty ",") args (pplist pp_arg_mode ",") modes) + + (* fold_on_modes (fun t l r -> + build_hyp_head ctx l t.ScopedTerm.it; Functional) + (fun _ _ _ -> Any) *) + and build_hyps_head (ctx : Ctx.t) (t : ScopedTerm.t_) = + match t with + | ScopedTerm.Const _ -> () + | App (Global { decl_id }, f, x, xs) -> ( + match get_funct_of_term ctx t with + | None -> assert false (* TODO: The functionality is not know... *) + | Some e -> + Format.eprintf "Before call to build_hyps_head_modes, func is %a@." pp_functionality e; + build_hyps_head_modes ctx e (x :: xs) (get_mode f) |> ignore ) + | App (Bound _, f, _, _) -> error ~loc (Format.asprintf "No signature for predicate %a@." F.pp f) + | Var _ -> error ~loc "Flex term used has head of a clause" + | _ -> failwith "type error7" + in + build_hyps_head + in - let type2func f (x:ScopedTypeExpression.t) = type2func_lam F.Set.empty f x.value + let check_body ctxx tm exp : unit = + let rec func2mode = function Arrow (_, r) -> Output :: func2mode r | _ -> [] in + let get_mode n f = try get_mode n with _ -> func2mode f in + let rec infer_app n ctx t args = + to_print (fun () -> Format.eprintf "The global app is %a@." F.pp n); + match get_funct_of_term ctx t with + | None -> + error ~loc (Format.asprintf "TODO2 %a" pp_env ()) + (* TODO: The functionality of t is not known... should be taken into account *) + | Some e -> + let modes = get_mode n e in + + Format.eprintf "The functionality of %a is %a@." F.pp n pp_functionality e; + let valid_call = valid_call ctx e args modes in + + Format.eprintf "Valid call for %a is %a@." F.pp n pp_functionality valid_call; + + if valid_call <> Any then infer_outputs ctx e args modes + else ( + infer_outputs_fail ctx e args modes |> ignore; + Any) + and valid_call ctx = + fold_on_modes + (fun e l r -> + let inferred = infer ctx e in + if functionality_leq ~loc:e.ScopedTerm.loc inferred l then r else Any) + (fun _ _ r -> r) + and infer_outputs ctx = + fold_on_modes + (fun _ _ r -> r) + (fun e l r -> + let inferred = infer ctx e in + Format.eprintf "Before setting %a and l is %a@." ScopedTerm.pretty e pp_functionality l; + match e.ScopedTerm.it with + | Var (n, []) -> + add_env n ~v:l; + r + | _ -> if functionality_leq ~loc:e.loc inferred l then r else Any) + and infer_outputs_fail ctx = + fold_on_modes + (fun _ _ r -> r) + (fun e l r -> + match e.ScopedTerm.it with + | Var (n, []) -> + add_env n ~v:Any; + r + | _ -> assert false) + and infer ctx ({ it = t; loc } : ScopedTerm.t) : functionality = + match t with + | ScopedTerm.Const _ | CData _ -> get_funct_of_term ctx t |> Option.get + | Discard -> Functional + | Var (n, []) -> ( match Env.get !env n with None -> Any | Some e -> e) + | Var (n, args) -> infer_app n ctx t args + | Lam (None, _, _type, t) -> arr Any (infer ctx t) + | Lam (Some vname, _, _type, t) -> arr Any (infer (add_ctx ctx vname ~v:Any) t) + | Impl (true, _hd, t) -> infer ctx t (* TODO: hd is ignored *) + | Impl (false, _, t) -> infer ctx t (* TODO: this is ignored *) + | App (_, n, x, [ y ]) when F.equal F.isf n || F.equal F.eqf n -> + unify_func x.it y.it ctx; + Functional + | App (_, n, x, xs) when F.equal F.andf n -> + let args = x :: xs in + List.fold_right (fun e acc -> infer ctx e |> max ~loc:e.ScopedTerm.loc acc) args Functional + | App (_, n, x, []) when F.equal F.pif n || F.equal F.sigmaf n -> ( + match infer ctx x with + | Arrow (_, r) -> r + | e -> error ~loc (Format.asprintf "Type error (%a is not a function)" ScopedTerm.pretty_ t)) + | App (_, n, x, xs) -> ( + to_print (fun () -> Format.eprintf "The global app is %a@." F.pp n); + match get_funct_of_term ctx t with + | None -> + error ~loc "TODO22" (* TODO: The functionality of t is not known... should be taken into account *) + | Some e -> infer_app n ctx t (x :: xs)) + | Cast (t, _) -> infer ctx t + | Spill (a, b) -> error ~loc "TODO3" (* error ~loc "Spill NYI" *) + and check ctx (t : ScopedTerm.t) (exp : functionality) : unit = + let before, after = split_bang t in + List.iter (fun e -> infer ctx e |> ignore) before; + + List.iter + (fun e -> + let inferred = infer ctx e in + Format.eprintf "Inferred is %a and expected is %a@." pp_functionality inferred pp_functionality exp; + functionality_leq_error ~loc:e.ScopedTerm.loc inferred exp) + after + in + + check ctxx tm exp + in + + let main ctx (tm : ScopedTerm.t_) : unit = + let hd, body = + match tm with + | App _ | Const _ -> (tm, None) + | Impl (false, hd, body) -> (hd.it, Some body) + | Var _ -> failwith "flexible clause..." + | _ -> failwith "Type error8" + in + Format.eprintf "=====================================================@."; + to_print (fun () -> Format.eprintf "The head is `%a`@." ScopedTerm.pretty_ hd); + check_head_input ctx hd; + Format.eprintf "END HEAD CHECK@."; + + to_print (fun () -> Format.eprintf "The contex_head is %a@." pp_env ()); + Option.iter (fun body -> check_body ctx body (get_func_hd ctx hd)) body + in + main Ctx.empty tm.it end -let merge = Compilation.merge -let rec functionalities_leq l1 l2 = match l1, l2 with - | _, [] -> true (* l2 can be any length (due to partial application) *) - | x::xs, y::ys -> functionality_leq x y && functionalities_leq xs ys - | [], _ -> error "the first list of functional args is can't been smaller then the second one: type error" - -and functionality_leq a b = match a, b with - | AssumedFunctional, AssumedFunctional -> true - | AssumedFunctional, t -> error (Format.asprintf "Cannot compare %a with %a" pp_f a pp_f b) (* TODO: print could be passed in a functional position *) - | _, AssumedFunctional -> error (Format.asprintf "Cannot compare %a with %a" pp_f a pp_f b) - | Relational xs, Relational ys -> functionalities_leq xs ys - | _, Relational _ -> true - | Relational _, _ -> false - | Functional xs, Functional ys -> functionalities_leq xs ys - | BoundVar _, _ | _, BoundVar _ -> true (* TODO: this is not correct... *) - | NoProp, NoProp -> true - | NoProp, _ | _, NoProp -> error "Type error, expected noProp found predicate" - -let functionality_leq_err ~loc c f' f = - if not (functionality_leq f' f) then - error ~loc (Format.asprintf "Functionality of %a is %a and is not included in %a" F.pp c pp_f f' pp_f f) - -let rec eat_lambdas = function - | Lam (_,b) -> eat_lambdas b - | F b -> b - -let get_functionality_bvars map k = - F.Map.find k map |> eat_lambdas - -(* - Invariant every constant in the map is functional: - i.e. for each k in the domain, map[k] = Functional [...] -*) -let is_functional map k = match get_functionality_bvars map k with - | Functional _ | NoProp | AssumedFunctional -> true - | Relational _ | BoundVar _ -> false - -let rec head_ag_func_pairing functional_preds args fs = - let func_vars = ref F.Map.empty in - let rec aux ~loc f = function - | ScopedTerm.Const (Global _,c) -> (* Look into type_abbrev for global symbols *) - (* Format.eprintf "1Looking for the constant %a\n%!" F.pp c; *) - begin match get_functionality_bvars functional_preds c with - | (f') -> functionality_leq_err ~loc c f' f - (* | Lam _ -> failwith "Error not fully applied" *) - end - | Const _ -> failwith "TODO" - | App(_,hd,x,xs) -> - Format.eprintf "2Looking for the constant %a -- %a\n%!" F.pp hd (pplist ScopedTerm.pp ",") (x::xs); - let f' = get_functionality_bvars functional_preds hd in - (* let f' = bind functional_preds (f', List.map (get_functionality functional_preds) (x::xs)) in *) - functionality_leq_err ~loc hd f' f; - begin match f' with - | Functional l -> aux' (x::xs) l - | _ -> () - end - | Impl _ -> error "TODO" (* Example p (a => b) *) - | Discard -> () - | Var (v, ag) -> - begin match F.Map.find_opt v !func_vars with - | None -> func_vars := F.Map.add v f !func_vars (* -> First appereance of the variable in the head *) - | Some f' -> functionality_leq_err ~loc v f' f - end - | Lam (None, _type, {it}) -> failwith "TODO" - | Lam (Some (e,_), _type, {it}) -> failwith "TODO" - | CData _ -> assert (f = NoProp) (* note that this is also true, otherwise we would have a type error *) - | Spill _ -> error "Spill in the head of a clause forbidden" - | Cast ({it},_) -> aux ~loc f it - and aux' args fs = match args, fs with - | [], [] -> () - | ScopedTerm.{it;loc}::xs, y::ys -> aux ~loc y it; aux' xs ys - | _ -> failwith "Partial application ??" - in - aux' args fs; - !func_vars - -and check_head functional_preds func_vars head_name head_args = - match get_functionality_bvars functional_preds head_name with - | NoProp -> raise StopCheck - | AssumedFunctional -> raise StopCheck - | Functional l | Relational l -> head_ag_func_pairing functional_preds head_args l - | BoundVar v -> error "unreachable branch" - -and check_body func_vars = func_vars - -let rec check_clause ~loc ~functional_preds func_vars ScopedTerm.{it} = - match it with - | Impl(false, hd, body) -> - check_clause ~loc ~functional_preds func_vars hd |> check_body - | App(_,c,x,xs) -> - begin - if String.starts_with ~prefix:"std.map." (F.show c) then func_vars - else func_vars (* TODO: activate the check by uncommenting the following lines... *) - (* try check_head functional_preds func_vars c (x::xs) - with StopCheck -> func_vars *) - end - | Const (_,_) -> func_vars (* a predicate with arity 0 is functional *) - | _ -> error ~loc "invalid type" - -let check_clause ~loc ~functional_preds t = - check_clause ~loc ~functional_preds F.Map.empty t |> ignore - -class merger (all_func: func_map) = object(self) - val mutable all_func = all_func - val mutable local_func = empty_fmap - - method private add_func is_ty_abbr n id ty = - let func = Compilation.type2func all_func ty in - if is_ty_abbr then all_func <- Compilation.add_type is_ty_abbr ~id ~n all_func func; - local_func <- Compilation.add_type is_ty_abbr ~id ~n local_func func; - - method get_all_func = all_func - method get_local_func = local_func - - method add_ty_abbr = self#add_func true - - method add_func_ty_list name ty (ty_w_id : TypeAssignment.overloaded_skema_with_id) = - let id_list = match ty_w_id with Single e -> [fst e] | Overloaded l -> List.map fst l in - List.iter2 (self#add_func false name) id_list ty - -end \ No newline at end of file +let to_check_clause ScopedTerm.{ it; loc } = + let n = get_namef it in + false && (not (F.equal n F.mainf)) && Re.Str.string_match (Re.Str.regexp ".*test.*") (Loc.show loc) 0 + +let check_clause ~loc ~env ~modes t = + if to_check_clause t then ( + (* check_clause ~loc ~env F.Map.empty t |> ignore *) + Format.eprintf "============== STARTING mode checking@."; + (* Format.eprintf "Modes are [%a]" (F.Map.pp (fun fmt ((e:mode_aux list),_) -> Format.fprintf fmt "%a" pp_mode e)) (modes); *) + (* Format.eprintf "Functional preds are %a@." pp env; *) + Checker_clause.check ~modes ~global:env ~loc t) + +class merger (all_func : env) = + object (self) + val mutable all_func = all_func + val mutable local_func = empty_fmap + + method private add_func is_ty_abbr id ty = + let loc, func = Compilation.type2func all_func ty in + let n = ty.name in + (* Format.eprintf "Adding constant %a with id %i\n%!" F.pp n id; *) + if is_ty_abbr then all_func <- Compilation.add_type ~loc is_ty_abbr ~id ~n all_func func; + local_func <- Compilation.add_type ~loc is_ty_abbr ~id ~n local_func func + + method get_all_func = all_func + method get_local_func = local_func + method add_ty_abbr = self#add_func true + + method add_func_ty_list ty (ty_w_id : TypeAssignment.overloaded_skema_with_id) = + let id_list = match ty_w_id with Single e -> [ fst e ] | Overloaded l -> List.map fst l in + List.iter2 (self#add_func false) id_list ty + + method merge : env = merge all_func local_func + end + +module Test = struct + let global_default = Scope.Global { escape_ns = false; decl_id = Scope.dummy_type_decl_id } + let addloc2te it = ScopedTypeExpression.{ it; loc = Loc.initial "" } + + let build_full_te name value = + ScopedTypeExpression.{ value; loc = Loc.initial ""; indexing = None; nparams = 0; name } + + let const e = addloc2te (Const (global_default, e)) + let mkapp n args = addloc2te @@ App (n, List.hd args, List.tl args) + let pred l = addloc2te (Pred (Relation, List.map (fun e -> (Mode.Output, e)) l)) + let arrta a b = TypeAssignment.Arr (NotVariadic, a, b) + let boolf = F.from_string "bool" + + let%test "test_type2func" = + let builder = new merger empty_fmap in + + (* Typeabbrev ta: (A\ A -> A -> prop) *) + let ta_id, ta = + let fA = F.from_string "A" in + let constA = addloc2te (Const (Bound "elpi", fA)) in + let ta_id = IdPos.make_str "ta_id" in + let ta_name = F.from_string "ta_name" in + let ty = ScopedTypeExpression.(Lam (fA, Ty (pred [ constA; constA ]))) in + (ta_id, build_full_te ta_name ty) + in + + (* pred p i:(ta bool) *) + let ty_id, tyexpr, ty_overloading = + let ty = ScopedTypeExpression.Ty (pred [ mkapp ta.name [ const boolf ] ]) in + + let ty_name = F.from_string "ty_name" in + let ty_id = IdPos.make_str "ty_id" in + + let tyos = TypeAssignment.(Single (ty_id, Ty (arrta (Cons boolf) (arrta (Cons boolf) Prop)))) in + (ty_id, [ build_full_te ty_name ty ], tyos) + in + + builder#add_ty_abbr ta_id ta; + builder#add_func_ty_list tyexpr ty_overloading; + + let all_func = builder#merge in + IdPos.Map.find ty_id all_func.cmap |> snd = arr (arr (NoProp []) (arr (NoProp []) Relational)) Relational +end diff --git a/src/compiler/determinacy_checker.mli b/src/compiler/determinacy_checker.mli index e40f9ee37..809f7e7d8 100644 --- a/src/compiler/determinacy_checker.mli +++ b/src/compiler/determinacy_checker.mli @@ -1,25 +1,22 @@ (* elpi: embedded lambda prolog interpreter *) (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) -open Elpi_parser -open Ast open Compiler_data +open Elpi_util.Util type t [@@ deriving show, ord] -type func_map [@@ deriving show, ord] +val empty_fmap : t -val empty_fmap : func_map +val check_clause : loc:Loc.t -> env:t -> modes:(mode*Loc.t) F.Map.t -> ScopedTerm.t -> unit -val check_clause : loc:Loc.t -> functional_preds:func_map -> - ScopedTerm.t -> unit +val merge : t -> t -> t -val merge : func_map -> func_map -> func_map - -class merger : func_map -> +class merger : t -> object - method get_all_func : func_map - method get_local_func : func_map - method add_ty_abbr : F.t -> Scope.type_decl_id -> ScopedTypeExpression.t -> unit - method add_func_ty_list : F.t -> TypeList.t -> TypeAssignment.overloaded_skema_with_id -> unit + method get_all_func : t + method get_local_func : t + method add_ty_abbr : Scope.type_decl_id -> ScopedTypeExpression.t -> unit + method add_func_ty_list : TypeList.t -> TypeAssignment.overloaded_skema_with_id -> unit + method merge : t end diff --git a/src/compiler/dune b/src/compiler/dune index 42d8afdef..84c19588a 100644 --- a/src/compiler/dune +++ b/src/compiler/dune @@ -2,7 +2,8 @@ (name elpi_compiler) (public_name elpi.compiler) (preprocess (per_module - ((pps ppx_deriving.std) compiler_data compiler determinacy_checker))) + ((pps ppx_deriving.std ppx_inline_test) compiler_data compiler determinacy_checker))) + (inline_tests) (libraries re.str unix stdlib-shims elpi.parser elpi.util elpi.runtime) (modules compiler_data type_checker determinacy_checker compiler) ) diff --git a/src/compiler/test_compiler_data.ml b/src/compiler/test_compiler_data.ml index 36a1476ff..521c949fd 100644 --- a/src/compiler/test_compiler_data.ml +++ b/src/compiler/test_compiler_data.ml @@ -41,7 +41,7 @@ open ScopedTerm let loc = Ast.Loc.initial "x" let ty = MutableOnce.create @@ Val Prop let c3 = { loc; it = CData (Ast.cint.cin 3); ty };; -let lam v t = { loc; ty; it = Lam(Some(F.from_string v,""),None,t)} +let lam v t = { loc; ty; it = Lam(Some(F.from_string v,""),None,MutableOnce.make (F.from_string""),t)} let var v = { loc; ty; it = Const(Bound "",F.from_string v)} let app c l = { loc; ty; it = App(Scope.mkGlobal ~escape_ns:true (),F.from_string c,List.hd l,List.tl l)} @@ -50,3 +50,4 @@ let () = pp_t (app "f" [app "g" [var "x"]]) "f (g x)";; let () = pp_t (lam "x" (var "x")) "x\\ x";; let () = pp_t (app "pi" [lam "x" (var "x")]) "pi x\\ x";; let () = pp_t (app "q" [lam "x" (var "x"); app "f" [var "x"]]) "q (x\\ x) (f x)";; +let () = pp_t (app "q" [lam "x" (var "x")]) "q (x\\ x)";; diff --git a/src/compiler/type_checker.ml b/src/compiler/type_checker.ml index b55435500..371136a16 100644 --- a/src/compiler/type_checker.ml +++ b/src/compiler/type_checker.ml @@ -61,7 +61,7 @@ let check_type ~type_abbrevs ~kinds ~loc ctx x : TypeAssignment.skema_w_id = TypeAssignment.Lam(c,aux_params ~loc (F.Set.add c ctx) t) | Ty t -> TypeAssignment.Ty(check_loc_tye ~type_abbrevs ~kinds ctx t) in - Scope.fresh_type_decl_id (), aux_params ~loc ctx x + Scope.fresh_type_decl_id loc, aux_params ~loc ctx x let check_types ~type_abbrevs ~kinds lst : TypeAssignment.overloaded_skema_with_id = match List.map (fun { value; loc } -> check_type ~type_abbrevs ~kinds ~loc F.Set.empty value) lst with @@ -114,7 +114,7 @@ let error_bad_ety2 ~loc ~tyctx ~ety1 ~ety2 pp c tx = error ~loc msg let error_bad_function_ety ~loc ~tyctx ~ety c t = - let msg = Format.asprintf "@[%a is a function@ but %a expects a term of type@ %a@]" ScopedTerm.pretty_ ScopedTerm.(Lam(c,None,t)) pp_tyctx tyctx TypeAssignment.pretty ety in + let msg = Format.asprintf "@[%a is a function@ but %a expects a term of type@ %a@]" ScopedTerm.pretty_ ScopedTerm.(Lam(c,None,ScopedTerm.mk_empty_lam_type c,t)) pp_tyctx tyctx TypeAssignment.pretty ety in error ~loc msg let error_bad_const_ety_l ~loc ~tyctx ~ety c txl = @@ -138,11 +138,11 @@ let error_not_poly ~loc c ty sk = TypeAssignment.pretty sk) type ret = TypeAssignment.t MutableOnce.t TypeAssignment.t_ -type ret_id = int * TypeAssignment.t MutableOnce.t TypeAssignment.t_ +type ret_id = IdPos.t * TypeAssignment.t MutableOnce.t TypeAssignment.t_ type spilled_phantoms = ScopedTerm.t list let local_type ctx ~loc c : ret_id TypeAssignment.overloading = - try TypeAssignment.Single (0, Scope.Map.find c ctx) (* local types have no id, 0 is given by default *) + try TypeAssignment.Single (Scope.dummy_type_decl_id, Scope.Map.find c ctx) (* local types have no id, 0 is given by default *) with Not_found -> anomaly ~loc "free variable" type classification = @@ -205,7 +205,7 @@ let check ~is_rule ~type_abbrevs ~kinds ~types:env ~unknown (t : ScopedTerm.t) ~ | Spill(sp,info) -> check_spill ctx ~loc ~tyctx sp info ety | App(Global _ as gid,c,x,xs) -> check_app ctx ~loc ~tyctx (c,gid) (global_type env ~loc c) (x::xs) ety | App(Bound lang as gid,c,x,xs) -> check_app ctx ~loc ~tyctx (c,gid) (local_type ctx ~loc (c,lang)) (x::xs) ety - | Lam(c,cty,t) -> check_lam ctx ~loc ~tyctx c cty t ety + | Lam(c,cty,tya,t) -> check_lam ctx ~loc ~tyctx c cty tya t ety | Discard -> [] | Var(c,args) -> check_app ctx ~loc ~tyctx (c, Bound elpi_language (*hack*)) (uvar_type ~loc c) args ety | Cast(t,ty) -> @@ -214,10 +214,9 @@ let check ~is_rule ~type_abbrevs ~kinds ~types:env ~unknown (t : ScopedTerm.t) ~ if unify ty ety then spills else error_bad_ety ~loc ~tyctx ScopedTerm.pretty_ x ty ~ety - and resolve_gid id _ = () - (*function + and resolve_gid id = function | Scope.Global x -> x.decl_id <- id - | _ -> ()*) + | _ -> () and global_type env ~loc c : ret_id TypeAssignment.overloading = try TypeAssignment.fresh_overloaded @@ F.Map.find c env @@ -227,7 +226,7 @@ let check ~is_rule ~type_abbrevs ~kinds ~types:env ~unknown (t : ScopedTerm.t) ~ Single (id,TypeAssignment.unval ty) with Not_found -> let ty = TypeAssignment.Val (mk_uvar (Format.asprintf "Unknown_type_of_%a_" F.pp c)) in - let id = Scope.fresh_type_decl_id () in + let id = Scope.fresh_type_decl_id loc in unknown_global := F.Map.add c (ty,id,loc) !unknown_global; Single (id,TypeAssignment.unval ty) @@ -267,10 +266,13 @@ 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 check_lam ctx ~loc ~tyctx c cty t ety = + and check_lam ctx ~loc ~tyctx c cty tya t ety = let name_lang = match c with Some c -> c | None -> fresh_name (), elpi_language in let src = match cty with - | None -> mk_uvar "Src" + | None -> + let v = mk_uvar "Src" in + MutableOnce.set tya (Val v); + v | Some x -> TypeAssignment.subst (fun f -> Some (TypeAssignment.UVar(MutableOnce.make f))) @@ check_loc_tye ~type_abbrevs ~kinds F.Set.empty x in let tgt = mk_uvar "Tgt" in @@ -448,7 +450,7 @@ let check ~is_rule ~type_abbrevs ~kinds ~types:env ~unknown (t : ScopedTerm.t) ~ let c, args = let rec head it = match it with - | App(Global _,f,{ it = Lam(_,_,x) },[]) when F.equal F.pif f -> head x.it + | App(Global _,f,{ it = Lam(_,_,_,x) },[]) when F.equal F.pif f -> head x.it | Impl(false,{ it = App(Global _,c',x,xs) },_) -> c', x :: xs | Impl(false,{ it = Const(Global _,c') },_) -> c', [] | App(Global _,c,x,xs) -> c, x :: xs @@ -497,11 +499,11 @@ let check ~is_rule ~type_abbrevs ~kinds ~types:env ~unknown (t : ScopedTerm.t) ~ try let ty, nocc, loc = F.Map.find c !sigma in sigma := F.Map.add c (ty,nocc+1,loc) !sigma; - Single (0, TypeAssignment.unval @@ ty) (* TODO: not sure of this... *) + Single (Scope.dummy_type_decl_id, TypeAssignment.unval @@ ty) with Not_found -> let ty = TypeAssignment.UVar (MutableOnce.make c) in sigma := F.Map.add c (TypeAssignment.Val ty,1,loc) !sigma; - Single (0, ty) (* TODO: not sure of this... *) + Single (Scope.dummy_type_decl_id, ty) and unif ~matching t1 t2 = (* Format.eprintf "%a = %a\n" TypeAssignment.pretty t1 TypeAssignment.pretty t2; *) let open TypeAssignment in diff --git a/src/parser/ast.ml b/src/parser/ast.ml index a75872e3d..e34f533fb 100644 --- a/src/parser/ast.ml +++ b/src/parser/ast.ml @@ -361,7 +361,6 @@ type program = { kinds : (unit,unit) Type.t list; types : (tattribute,functionality) Type.t list; type_abbrevs : (Func.t,functionality TypeExpression.t) TypeAbbreviation.t list; - modes : (tattribute,functionality) Type.t list; body : block list; } and cattribute = { diff --git a/src/parser/ast.mli b/src/parser/ast.mli index 5cbb0df97..703b5438c 100644 --- a/src/parser/ast.mli +++ b/src/parser/ast.mli @@ -224,7 +224,6 @@ type program = { kinds : (unit,unit) Type.t list; types : (tattribute,functionality) Type.t list; type_abbrevs : (Func.t,functionality TypeExpression.t) TypeAbbreviation.t list; - modes : (tattribute,functionality) Type.t list; body : block list; } and ('func,'term) block_constraint = { diff --git a/src/utils/util.ml b/src/utils/util.ml index bd528e89d..be00a6c90 100644 --- a/src/utils/util.ml +++ b/src/utils/util.ml @@ -259,6 +259,7 @@ type mode_aux = | Fo of arg_mode | Ho of arg_mode * mode and mode = mode_aux list +[@@deriving show, ord] let get_arg_mode = function Fo a -> a | Ho (a,_) -> a diff --git a/src/utils/util.mli b/src/utils/util.mli index afca995fb..2d11687c7 100644 --- a/src/utils/util.mli +++ b/src/utils/util.mli @@ -127,6 +127,7 @@ type mode_aux = | Fo of arg_mode | Ho of arg_mode * mode and mode = mode_aux list +[@@deriving show, ord] val for_all3b3 : argsdepth:int -> (argsdepth:int -> matching:bool -> 'x -> 'y -> 'z -> 'a -> 'a -> bool) -> 'x -> 'y -> 'z -> 'a list -> 'a list -> mode -> bool -> bool (*uses physical equality and calls anomaly if the element is not in the list*) diff --git a/tests/sources/functionality/test1.elpi b/tests/sources/functionality/test1.elpi index cda353f09..b85dae814 100644 --- a/tests/sources/functionality/test1.elpi +++ b/tests/sources/functionality/test1.elpi @@ -1,3 +1,4 @@ +% NO :functional pred p i:int, o:int. diff --git a/tests/sources/functionality/test10.elpi b/tests/sources/functionality/test10.elpi index 5b66cecd6..2c0221b9a 100644 --- a/tests/sources/functionality/test10.elpi +++ b/tests/sources/functionality/test10.elpi @@ -1,3 +1,4 @@ +% NO :functional pred p i:int, o:int. diff --git a/tests/sources/functionality/test11.elpi b/tests/sources/functionality/test11.elpi index 482f22889..447fd3011 100644 --- a/tests/sources/functionality/test11.elpi +++ b/tests/sources/functionality/test11.elpi @@ -1,9 +1,10 @@ +% NO :functional pred p i:int, o:int. % here we have variables in input position, overlap detection, % makes the predicate not functional... -% NOTE: the query p 1 Y has two solution for Y +% NOTE: the query p 1 Y has two solutions for Y p 1 2. p X 3. diff --git a/tests/sources/functionality/test12.elpi b/tests/sources/functionality/test12.elpi index c4ee597af..138331eac 100644 --- a/tests/sources/functionality/test12.elpi +++ b/tests/sources/functionality/test12.elpi @@ -1,3 +1,4 @@ +% YES :functional pred p i:int, o:int. diff --git a/tests/sources/functionality/test13.elpi b/tests/sources/functionality/test13.elpi index 2b39592bf..8daf17a3e 100644 --- a/tests/sources/functionality/test13.elpi +++ b/tests/sources/functionality/test13.elpi @@ -1,3 +1,4 @@ +% NO :functional pred p i:int, o:int. diff --git a/tests/sources/functionality/test14.elpi b/tests/sources/functionality/test14.elpi index 70e313ac7..e69bdf92b 100644 --- a/tests/sources/functionality/test14.elpi +++ b/tests/sources/functionality/test14.elpi @@ -1,3 +1,4 @@ +% NO :functional pred f i:int, o:int. diff --git a/tests/sources/functionality/test15.elpi b/tests/sources/functionality/test15.elpi index 1c897c8ce..ef2425af4 100644 --- a/tests/sources/functionality/test15.elpi +++ b/tests/sources/functionality/test15.elpi @@ -1,3 +1,4 @@ +% YES :functional pred f i:int, o:int. diff --git a/tests/sources/functionality/test16.elpi b/tests/sources/functionality/test16.elpi index f4a5de8a1..a08b104f0 100644 --- a/tests/sources/functionality/test16.elpi +++ b/tests/sources/functionality/test16.elpi @@ -1,3 +1,4 @@ +% YES :functional pred p i:int, o:int. diff --git a/tests/sources/functionality/test17.elpi b/tests/sources/functionality/test17.elpi index fa3c40f2b..cebf2da11 100644 --- a/tests/sources/functionality/test17.elpi +++ b/tests/sources/functionality/test17.elpi @@ -1,3 +1,4 @@ +% YES pred q o:int. :functional diff --git a/tests/sources/functionality/test18.elpi b/tests/sources/functionality/test18.elpi index fc3e5278c..e2a22dcd9 100644 --- a/tests/sources/functionality/test18.elpi +++ b/tests/sources/functionality/test18.elpi @@ -1,3 +1,4 @@ +% NO pred q o:int. :functional diff --git a/tests/sources/functionality/test19.elpi b/tests/sources/functionality/test19.elpi index 7cb09d89f..65a19a3d3 100644 --- a/tests/sources/functionality/test19.elpi +++ b/tests/sources/functionality/test19.elpi @@ -1,3 +1,4 @@ +% NO pred q o:int. :functional diff --git a/tests/sources/functionality/test2.elpi b/tests/sources/functionality/test2.elpi index b5bc6fb28..ff2590b57 100644 --- a/tests/sources/functionality/test2.elpi +++ b/tests/sources/functionality/test2.elpi @@ -1,16 +1,20 @@ +% YES :functional pred p i:int, o:int. :functional pred s o:int. +pred r i:int, o:int. +pred q o:int. + % THIS IS OK since a bang preclude distinct outputs p 1 3. p 2 3 :- !. /* functional context: everything before the cut is irrelevant for functionality */ /* moreover, we have parentheses around commas, i.e. a tree-like ast */ p 2 A :- (r 3 A, q A, std.map [] std.rev []), (!, true). -p 2 X :- !, s X. /* X is a functional output of s */ +p 2 X :- !, s X. /* X is a functionally determined by s */ p 2 5. main. \ No newline at end of file diff --git a/tests/sources/functionality/test20.elpi b/tests/sources/functionality/test20.elpi index 98f929d56..644eb087a 100644 --- a/tests/sources/functionality/test20.elpi +++ b/tests/sources/functionality/test20.elpi @@ -1,3 +1,4 @@ +% YES pred q o:int. :functional pred q' o:int. diff --git a/tests/sources/functionality/test21.elpi b/tests/sources/functionality/test21.elpi index 2b2ecae38..b19273e05 100644 --- a/tests/sources/functionality/test21.elpi +++ b/tests/sources/functionality/test21.elpi @@ -1,3 +1,4 @@ +% NO :functional pred wrong-if i:prop, i:(:functional pred), i:(:functional pred). wrong-if P Q _ :- !, P, Q, print "123". diff --git a/tests/sources/functionality/test22.elpi b/tests/sources/functionality/test22.elpi index a7ef93a3d..8a4a05b3e 100644 --- a/tests/sources/functionality/test22.elpi +++ b/tests/sources/functionality/test22.elpi @@ -1,5 +1,6 @@ +% YES :functional pred f o:int. -:functional pred r o:(:functional pred o:int). +:functional pred r o:(func -> int). f R :- r X, X R. diff --git a/tests/sources/functionality/test23.elpi b/tests/sources/functionality/test23.elpi index 54a6cc4ab..101acada1 100644 --- a/tests/sources/functionality/test23.elpi +++ b/tests/sources/functionality/test23.elpi @@ -1,3 +1,4 @@ +% NO :functional pred f i:int, o:int. diff --git a/tests/sources/functionality/test24.elpi b/tests/sources/functionality/test24.elpi index 9b574274f..a488c5509 100644 --- a/tests/sources/functionality/test24.elpi +++ b/tests/sources/functionality/test24.elpi @@ -1,3 +1,4 @@ +% NO :functional pred f o:int. diff --git a/tests/sources/functionality/test25.elpi b/tests/sources/functionality/test25.elpi index 53fe04b54..ee0c43423 100644 --- a/tests/sources/functionality/test25.elpi +++ b/tests/sources/functionality/test25.elpi @@ -1,3 +1,4 @@ +% NO :functional pred f o:int. :functional pred r o:(pred o:int). diff --git a/tests/sources/functionality/test26.elpi b/tests/sources/functionality/test26.elpi index a4053ad78..b7c547205 100644 --- a/tests/sources/functionality/test26.elpi +++ b/tests/sources/functionality/test26.elpi @@ -1,3 +1,4 @@ +% NO kind tm type. type app tm -> tm -> tm. diff --git a/tests/sources/functionality/test27.elpi b/tests/sources/functionality/test27.elpi index d93cc7025..b18a76b27 100644 --- a/tests/sources/functionality/test27.elpi +++ b/tests/sources/functionality/test27.elpi @@ -1,3 +1,4 @@ +% NO kind tm type. type app tm -> tm -> tm. diff --git a/tests/sources/functionality/test28.elpi b/tests/sources/functionality/test28.elpi index 87ecdda7a..20180fc8e 100644 --- a/tests/sources/functionality/test28.elpi +++ b/tests/sources/functionality/test28.elpi @@ -1,3 +1,4 @@ +% YES pred q o:int. q 1. q 2. diff --git a/tests/sources/functionality/test29.elpi b/tests/sources/functionality/test29.elpi index e8770ef1e..1b45dcc33 100644 --- a/tests/sources/functionality/test29.elpi +++ b/tests/sources/functionality/test29.elpi @@ -1,3 +1,4 @@ +% YES :functional pred r o:int, o:int. :functional pred p i:(pred i:int). diff --git a/tests/sources/functionality/test3.elpi b/tests/sources/functionality/test3.elpi index 63569a5a2..b0701a4c7 100644 --- a/tests/sources/functionality/test3.elpi +++ b/tests/sources/functionality/test3.elpi @@ -1,3 +1,4 @@ +% NO :functional pred q o:int. diff --git a/tests/sources/functionality/test30.elpi b/tests/sources/functionality/test30.elpi index 78c268902..6f986956c 100644 --- a/tests/sources/functionality/test30.elpi +++ b/tests/sources/functionality/test30.elpi @@ -1,3 +1,4 @@ +% NO pred r i:int, o:int. :functional pred p i:(:functional pred i:int). diff --git a/tests/sources/functionality/test3_1.elpi b/tests/sources/functionality/test3_1.elpi new file mode 100644 index 000000000..a8973a63a --- /dev/null +++ b/tests/sources/functionality/test3_1.elpi @@ -0,0 +1,11 @@ +% NO +:functional +pred q o:int. + +pred t o:int. + + +% TEST 3 +q Y :- Y = {t}. % This breaks functionality, t is not functional + +main. \ No newline at end of file diff --git a/tests/sources/functionality/test4.elpi b/tests/sources/functionality/test4.elpi index 46ee25e67..45548abc3 100644 --- a/tests/sources/functionality/test4.elpi +++ b/tests/sources/functionality/test4.elpi @@ -1,3 +1,4 @@ +% YES :functional pred p i:int, o:int. diff --git a/tests/sources/functionality/test5.elpi b/tests/sources/functionality/test5.elpi index 5c6241a21..a6ae8f21c 100644 --- a/tests/sources/functionality/test5.elpi +++ b/tests/sources/functionality/test5.elpi @@ -1,3 +1,4 @@ +% NO :functional pred p i:int, o:int. diff --git a/tests/sources/functionality/test6.elpi b/tests/sources/functionality/test6.elpi index 52bb8cbfb..f8186cf1c 100644 --- a/tests/sources/functionality/test6.elpi +++ b/tests/sources/functionality/test6.elpi @@ -1,3 +1,4 @@ +% YES :functional pred p i:int, o:int. diff --git a/tests/sources/functionality/test7.elpi b/tests/sources/functionality/test7.elpi index cff7ffef6..8355a3c75 100644 --- a/tests/sources/functionality/test7.elpi +++ b/tests/sources/functionality/test7.elpi @@ -1,3 +1,4 @@ +% NO :functional pred p i:int, o:int. diff --git a/tests/sources/functionality/test8.elpi b/tests/sources/functionality/test8.elpi index 0e6bfccf1..491784cc9 100644 --- a/tests/sources/functionality/test8.elpi +++ b/tests/sources/functionality/test8.elpi @@ -1,3 +1,4 @@ +% NO :functional pred p i:int, o:int. diff --git a/tests/sources/functionality/test9.elpi b/tests/sources/functionality/test9.elpi index 0384ad3ff..c9f428613 100644 --- a/tests/sources/functionality/test9.elpi +++ b/tests/sources/functionality/test9.elpi @@ -1,3 +1,4 @@ +% NO :functional pred p i:int, o:int. diff --git a/tests/sources/progs/progs3.mod b/tests/sources/progs/progs3.mod index 3a3657955..73a256199 100644 --- a/tests/sources/progs/progs3.mod +++ b/tests/sources/progs/progs3.mod @@ -4,5 +4,5 @@ accumulate tr1_test. main3 :- %--- script3 --- - test 1, test 2, not (test 3). + test_nb 1, test_nb 2, not (test_nb 3). diff --git a/tests/sources/progs/progs4.mod b/tests/sources/progs/progs4.mod index b5e56ad88..d7e792f18 100644 --- a/tests/sources/progs/progs4.mod +++ b/tests/sources/progs/progs4.mod @@ -4,5 +4,5 @@ accumulate tr2_test. main4 :- %--- script4 --- - test 1, test 2, not (test 3), test 4. + test_nb 1, test_nb 2, not (test_nb 3), test_nb 4. diff --git a/tests/sources/progs/tr1_test.mod b/tests/sources/progs/tr1_test.mod index 7ab4e8920..2b57e46ca 100644 --- a/tests/sources/progs/tr1_test.mod +++ b/tests/sources/progs/tr1_test.mod @@ -8,11 +8,11 @@ module tr1_test. accumulate terms, tr_recognizer. -type test int -> o. +type test_nb int -> o. -test 1 :- trm trfact1 F, tl_rec F. +test_nb 1 :- trm trfact1 F, tl_rec F. -test 2 :- trm gcd2 F, tl_rec F. +test_nb 2 :- trm gcd2 F, tl_rec F. -test 3 :- trm appnd F, tl_rec F. +test_nb 3 :- trm appnd F, tl_rec F. diff --git a/tests/sources/progs/tr2_test.mod b/tests/sources/progs/tr2_test.mod index 141395962..e1f51ccc5 100644 --- a/tests/sources/progs/tr2_test.mod +++ b/tests/sources/progs/tr2_test.mod @@ -6,13 +6,13 @@ module tr2_test. accumulate terms, general_tr. -type test int -> o. +type test_nb int -> o. -test 1 :- trm trfact1 F, tailrec F. +test_nb 1 :- trm trfact1 F, tailrec F. -test 2 :- trm gcd2 F, tailrec F. +test_nb 2 :- trm gcd2 F, tailrec F. -test 3 :- trm appnd F, tailrec F. +test_nb 3 :- trm appnd F, tailrec F. -test 4 :- trm trfact2 F, tailrec F. +test_nb 4 :- trm trfact2 F, tailrec F. diff --git a/tests/suite/correctness_FO.ml b/tests/suite/correctness_FO.ml index 8d1a25a6b..93b26fa6c 100644 --- a/tests/suite/correctness_FO.ml +++ b/tests/suite/correctness_FO.ml @@ -230,4 +230,25 @@ let () = declare "mode_checking_ho" |] in mode_check expected "mode_checking_ho" )) - () \ No newline at end of file + () + +let () = + let status = Test. + [|Failure; Success; Failure; Success; Failure; (*05*) + Success; Failure; Failure; Failure; Failure; (*10*) + Failure; Success; Failure; Failure; Success; (*15*) + Success; Success; Failure; Failure; Success; (*20*) + Failure; Success; Failure; Failure; Failure; (*25*) + Failure; Failure; Success; Success; Failure|] in + let ignore = [1;5;7;8;9;10;11;13;16;17;20;24;26;27;28;30] in + (* interesting tests:24 *) + for i = 0 to -1 (* Array.length status - 1*) do + if not (List.mem (i+1) ignore) then ( + let name = Printf.sprintf "functionality/test%d.elpi" (i+1) in + let descr = Printf.sprintf "functionality%d" (i+1) in + declare descr + ~source_elpi:name + ~description:descr + ~expectation:status.(i) + ()) + done