Merge pull request #280 from FissoreD/scope-term

[functionality] add functionality field to program

Makefile

@@ -12,6 +12,8 @@ help:
 	@echo '  tests ONLY=rex         runs only tests matching rex'
 	@echo '  tests PROMOTE=true     runs and promote tests if different'
 	@echo '                           (can be combined with ONLY)'
+	@echo '  tests LN_NB=nb         sets max number of lines to print of failing tests'
+	@echo '                           (negave numbers means print all file)'
 	@echo
 	@echo '  git/treeish            checkout treeish and build elpi.git.treeish'
 	@echo
@@ -28,6 +30,7 @@ BUILD=_build/default
 SHELL:=/usr/bin/env bash
 TIMEOUT=90.0
 PROMOTE=false
+LN_NB=-1
 PWD=$(shell pwd)
 RUNNERS=\
   dune \
@@ -82,6 +85,7 @@ tests:
 		tests/test.exe \
 		--seed $$RANDOM \
 		--promote $(PROMOTE) \
+		--ln_nb=$(LN_NB) \
 		--timeout $(TIMEOUT) \
 		$(TIME) \
 		--sources=$(PWD)/tests/sources/ \

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 "@[<hov 2>%a@ %a@]" F.pp f (Util.pplist (pretty_e_parens ~lvl:app) " ") (x::xs)
     | Arrow(NotVariadic,s,t) -> fprintf fmt "@[<hov 2>%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) ->

src/data.ml

@@ -92,6 +92,19 @@ type mode_aux = Util.mode_aux =
 and mode = mode_aux list
 [@@ deriving show, ord]
 
+module Functionality = struct
+  type f = 
+    | Functional of f list
+    | Relational
+    | AssumedFunctional (* Currently used for variadic functions, like print, halt... *)
+    | BoundVar of F.t
+
+  and t = Lam of F.t * t | F of (f*Loc.t)
+  [@@ deriving show, ord]
+
+  let rec get_loc = function Lam (_,b) -> get_loc b | F(_,loc) -> loc
+end
+
 type ttype =
   | TConst of constant
   | TApp of constant * ttype * ttype list

tests/sources/functionality/README.md

@@ -0,0 +1,41 @@
+# Functionality
+
+## About the tests
+
+### Success
+
+test2.elpi: functional ctx + functional premises (FO)
+test4.elpi: loading local clauses (with and without local pi)
+test6.elpi: nested local clauses
+test12.elpi: non overlapping heads using uvar keyword
+test15.elpi: non functional premise followed by bang
+test16.elpi: non functional premise using variable not used in the head
+test17.elpi: functional predicate with functional argument + nested
+test20.elpi: functional predicate with non functional argument declaration
+test22.elpi: functional ho output of a premise used to build the output of the rule
+test28.elpi: non functional prop in functional ctx call (do')
+test29.elpi: similar to previous
+
+
+### Failure
+
+test1.elpi: overlapping heads no bang rigid terms
+test3.elpi: non functional premise
+test5.elpi: local non functional clause
+test6.elpi: nested local non-functional clauses
+test7.elpi: local non-functional clauses
+test8.elpi: local non-functional clauses
+test9.elpi: local nested non-functional premises
+test10.elpi: local nested non-functional premises
+test11.elpi: overlapping heads using uvars
+test13.elpi: overlapping heads with two rules using the uvar keyword
+test14.elpi: non-functional variable used in variable used in the clause head
+test18.elpi: functional predicate with non functional argument
+test19.elpi: nested functional predicate with non functional argument
+test21.elpi: wrong-if: non-declared functional argument used in non functional ctx
+test23.elpi: similar to test14
+test24.elpi: ho output used in two different calls with different functionality relation
+test25.elpi: non functional ho output used to produce output of the rule
+test26.elpi: overlap with as operator
+test27.elpi: overlap with HO term in PF (B x) against (A x y)
+test30.elpi: non functional pred pass instead of functional, makes the premise non functional 

tests/sources/functionality/heads/heads01.elpi

@@ -0,0 +1,11 @@
+:functional pred q.
+
+:functional pred p i:(:functional pred).
+
+% THIS IS OK:
+% functionality relation of q is (Functional [])
+% functionality of first arg of p is (Functional [])
+% Functional [] ⊆ Functional []
+p q.
+
+main.

tests/sources/functionality/heads/heads02.elpi

@@ -0,0 +1,11 @@
+pred q.
+
+:functional pred p i:(:functional pred).
+
+% THIS FAILS:
+% functionality relation of q is (Relational [])
+% functionality of first arg of p is (Functional [])
+% Relational [] ⊈ Functional []
+p q.
+
+main.

tests/sources/functionality/heads/heads03.elpi

@@ -0,0 +1,13 @@
+:functional pred p i:(:functional pred i:(pred)).
+:functional pred r i:(:functional pred).
+
+% THIS IS OK:
+% functionality relation of p is (Functional [Functional [Relational []]])
+% functionality of r is (Functional [Functional []])
+% (p r) is GOOD since first arg of p is `Functional [Relational []]`
+% and Functional [Functional []] ⊆ Functional [Relational []]
+% r (p r) is GOOD is first arg of r is `Functional []` and
+% Functional [Functional [Relational []] ⊆ Functional []
+r (p r).
+
+main.

tests/sources/functionality/heads/heads04.elpi

@@ -0,0 +1,11 @@
+:functional pred p i:(:functional pred i:(:functional pred)).
+:functional pred r i:(pred).
+
+% THIS FAILS:
+% functionality relation of p is (Functional [Functional [Relational []]])
+% functionality of r is (Functional [Functional []])
+% (p r) is WRONG since first arg of p is `Functional [Functional []]`
+% and Functional [Relational []] ⊈ Functional [Functional []]
+r (p r).
+
+main.

tests/sources/functionality/heads/heads05.elpi

@@ -0,0 +1,7 @@
+:functional pred p i:(pred i:(pred)) i:(:functional pred i:(pred)) .
+
+% THIS FAILS: first A is relational. The second A is functional.
+% However relational ⊈ functional
+p A A.
+
+main.

tests/sources/functionality/heads/heads06.elpi

@@ -0,0 +1,7 @@
+:functional pred p i:(:functional pred i:(pred)) i:(pred i:(pred)).
+
+% THIS IS OK: first A is functional. The second A is relation.
+% functional ⊆ relational
+p A A.
+
+main.

tests/sources/functionality/heads/heads07.elpi

@@ -0,0 +1,10 @@
+:functional pred p i:(int -> (:functional pred) -> prop).
+
+pred q i:int, o:(:functional pred).
+
+% THIS IS OK:
+% functionality relation of q is 
+% (Relational [NoProp, Functional[]]) ⊆ (Relational [NoProp, Functional[]])
+p q.
+
+main.

tests/sources/functionality/heads/heads08.elpi

@@ -0,0 +1,9 @@
+:functional pred p i:((:functional pred) -> prop).
+
+pred q o:(pred).
+
+% functionality relation of q is 
+% (Relational [Relational]) ⊈ (Relational [Functional])
+p q.
+
+main.

tests/sources/functionality/heads/heads09_TODO.elpi

@@ -0,0 +1,7 @@
+:functional pred p i:((:functional pred) -> (:functional pred)).
+
+:functional pred q i:(:functional pred).
+
+p (x\q x).
+
+main.

tests/sources/functionality/test1.elpi

@@ -0,0 +1,10 @@
+:functional 
+pred p i:int, o:int.
+
+p 1 3.
+p 2 3.
+
+% The following rule hinders functionality, since `p 2 X` has two solutions for X
+p 2 4.
+
+main.

tests/sources/functionality/test1.m

@@ -0,0 +1,15 @@
+:- module test1.
+
+:- interface.
+:- import_module io.
+:- pred main(io::di, io::uo) is det.
+:- pred p(int::in, int::out) is nondet.
+
+:- implementation.
+:- import_module int.
+
+
+p(1,2).
+p(2,X) :- X = 3; X = 4.
+
+main(!IO).

tests/sources/functionality/test10.elpi

@@ -0,0 +1,11 @@
+:functional 
+pred p i:int, o:int.
+
+:functional
+pred q i:int, o:int.
+
+q 1 1.
+
+p 4 X :- pi x\ sigma Y\ q x Y => q x Y => q 1 X.
+
+main.

tests/sources/functionality/test11.elpi

@@ -0,0 +1,10 @@
+: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
+p 1 2.
+p X 3.
+
+main.

tests/sources/functionality/test12.elpi

@@ -0,0 +1,12 @@
+:functional
+pred p i:int, o:int.
+
+/* this slightly differs from test11.elpi since 
+ * we explicitly put the uvar keyword in place of a unification variable
+ * the input mode will therefore prevent the query `p 1 Y` to unify with 
+ * `p uvar 3.
+ */
+p 1 2.
+p uvar 3.
+
+main.

tests/sources/functionality/test13.elpi

@@ -0,0 +1,12 @@
+:functional
+pred p i:int, o:int.
+
+/* another version of test11.elpi and test12.elpi
+ * here the query `p 1 X` has clearly one distinct solution,
+ * but `p X Y` has two. Therefore, p is not guaranteed to be functional
+ */
+p 1 2.
+p (uvar as X_) 3.
+p (uvar as Y_) 4.
+
+main.

tests/sources/functionality/test14.elpi

@@ -0,0 +1,22 @@
+:functional
+pred f i:int, o:int.
+
+pred q o:int.
+
+:functional
+pred r i:int, o:int.
+
+q 1.
+q 2.
+
+r X X.
+
+% Recall: q is not functional!
+% Note: in warren, the following rule is considered functional
+% since the input X should be ground, and therefore, q X does not
+% create any choice point for `r X Y` where Y can be assinged to 2 distinct
+% values.
+% In the implementation using the input mode of elpi this is no more true.
+f X Y :- q X, r X Y.
+
+main :- std.findall (f _ _) L, print L. 

tests/sources/functionality/test15.elpi

@@ -0,0 +1,22 @@
+:functional
+pred f i:int, o:int.
+
+pred q o:int.
+
+:functional
+pred r i:int, o:int.
+
+q 1.
+q 2.
+
+r X X.
+
+% Recall: q is not functional!
+% This is similar to test14, but in this case, 
+% the output of q is Y (which can have several distinct assignments). 
+% However Y is functionally determined by then 1 Y :- q Y, r 1 Y.
+
+% Here the bang ensures that `Y` is functionally determined by the call to q
+f 2 Y :- q Y, !.
+
+main. 

tests/sources/functionality/test16.elpi

@@ -0,0 +1,13 @@
+:functional 
+pred p i:int, o:int.
+
+pred f o:int, o:int, o:int.
+
+% the variables of f are not used in the output, therefore, p remains functional 
+p 4 Y :- f Z X W, Y = 4.
+
+% case similar to the previous one, where the output is not instantiated 
+% all the variables in the body are never returned
+p 5 Y :- f Z X W, f X Z T.
+
+main.