Commits

Sébastien Ferré committed d87c550

Better handling of quantifiers in updates (especially retraction) + quantifier 'no'

Comments (0)

Files changed (8)

       | FContains of Ext.var * Ext.var
       | FDisplay of expr_prop
       | FForthe of fol_prop * fol_prop
-      | FForeach of fol_prop * fol_prop
+      | FForEvery of fol_prop * fol_prop
+      | FForNo of fol_prop * fol_prop
+      | FForOnly of fol_prop * fol_prop
       | FForany of fol_prop * fol_prop
       | FForN of int * Ext.var * fol_prop
       | FGiven of fol_prop * fol_prop
 	  list_of_fol_prop p1 @ list_of_fol_prop p2
       | p -> [p]
 
+(* should be used for queries only *)
     let rec eval_fol_prop vars p =
       match p with
       | Prop.Atom fol ->
 	  let d1, vars1, p1' = eval_fol_prop vars p1 in
 	  let d2, vars2, p2' = eval_fol_prop vars1 p2 in
 	  d1+d2, vars2, FForthe (p1',p2')
-      | FForeach (p1, Prop.Atom (FForeach (p21, p22))) ->
-	  eval_fol vars (FForeach (Prop.And (p1,p21), p22))
-      | FForeach (p1,p2) ->
+      | FForEvery (p1, Prop.Atom (FForEvery (p21, p22))) ->
+	  eval_fol vars (FForEvery (Prop.And (p1,p21), p22))
+      | FForEvery (p1,p2) ->
 	  let d1, vars1, p1' = eval_fol_prop vars p1 in
 	  let d2, _, p2' = eval_fol_prop vars1 p2 in
-	  d1+d2, vars, FForeach (p1',p2')
+	  d1+d2, vars, FForEvery (p1',p2')
+      | FForOnly (p1,p2) ->
+	  eval_fol vars (FForEvery (p2,p1))
+      | FForNo (p1,p2) ->
+	  eval_fol vars (FForEvery (p1, Prop.Not p2))
       | FForany (p1,p2) ->
 	  let _, vars1, p1' = eval_fol_prop vars p1 in
 	  let d2, vars2, p2' = eval_fol_prop vars1 p2 in
       end
 
 
-    let rec extension_of_fol ~obs (store : #Store.store) : fol_prop -> Ext.t =
-      (* TODO: return free variables *)
-      fun p ->
-	extension_fol_prop ~obs store p
-    and extension_fol_prop ~obs store : fol_prop -> fol_ext = function
+(* should be called after 'eval_fol' *)
+    let rec extension_fol_prop ~obs store : fol_prop -> fol_ext = function
       | Prop.Atom p -> extension_fol ~obs store p
       | Prop.And (p1,p2) ->
 	  let ext1 = extension_fol_prop ~obs store p1 in
 	  invalid_arg "Fol.extension_fol: display call"
       | FForthe (p1,p2) ->
 	  let ext1 = extension_fol_prop ~obs store p1 in
-	  let ext2 = extension_fol_prop ~obs store p2 in
+ 	  let ext2 = extension_fol_prop ~obs store p2 in
 	  Ext.join ~ordered:true ext1 ext2
-      | FForeach (p1,p2) ->
+      | FForEvery (p1,p2) ->
 	  let ext1 = extension_fol_prop ~obs store p1 in
 	  let ext2 = extension_fol_prop ~obs store p2 in
 	  Ext.check (Ext.forall ext1 ext2)
+      | FForOnly _ -> assert false (* failed to call 'eval_fol' *)
+      | FForNo _ -> assert false (* failed to call 'eval_fol' *)
       | FForany (p1,p2) ->
 	  let ext1 = extension_fol_prop ~obs store p1 in
 	  let ext2 = extension_fol_prop ~obs store p2 in
       | EConcat le ->
 	  Ext.expr_quote (List.map (extension_expr_prop ~obs store) le)
 
-    let rec assert_of_fol ~obs store : fol_prop -> Code.t list = function
-      | Prop.Atom p -> code_fol ~obs store Code.add p
-      | Prop.Not p1 -> retract_of_fol ~obs store p1
-      | Prop.And (p1,p2) ->
-	  assert_of_fol ~obs store p1 @
-	  assert_of_fol ~obs store p2
-      | p -> code_fol_prop ~obs store Code.add p
-    and retract_of_fol ~obs store : fol_prop -> Code.t list =
-      fun f ->
-	let e = extension_of_fol ~obs store f in
-	let c = code_fol_prop ~obs store Code.remove f in
-	[Code.foreach e c]
-    and code_fol_prop ~obs store frel = function
-      | Prop.Atom p -> code_fol ~obs store frel p
+    let extension_of_fol ~obs (store : #Store.store) (vars : Ext.var LSet.t) (p : fol_prop) : Ext.var LSet.t * Ext.t =
+      let _, vars1, p' = eval_fol_prop vars p in
+      vars1, extension_fol_prop ~obs store p'
+
+    let extension_of_expr ~obs store vars expr =
+      let _, vars1, expr' = eval_expr_prop vars expr in
+      vars1, extension_expr_prop ~obs store expr'
+
+
+    let assertor =
+      object
+	method is_assert = true
+	method is_retract = false
+	method update = Code.add
+      end
+
+    let retractor =
+      object
+	method is_assert = false
+	method is_retract = true
+	method update = Code.remove
+      end
+
+    let rec code_fol_prop ~obs store mode vars = function
+      | Prop.Atom p ->
+	  code_fol ~obs store mode vars p
       | Prop.And (p1,p2) ->
-	  code_fol_prop ~obs store frel p1 @
-	  code_fol_prop ~obs store frel p2
+	  code_fol_prop ~obs store mode vars p1 @
+	  code_fol_prop ~obs store mode vars p2
+      | Prop.Not p1 ->
+	  if mode#is_retract
+	  then code_fol_prop ~obs store assertor vars p1
+	  else
+	    let vars1, e = extension_of_fol ~obs store vars p1 in
+	    let lc = code_fol_prop ~obs store retractor vars1 p1 in
+	    [Code.foreach e lc]
       | Prop.Cond (Cond p0,p1,p2_opt) ->
-	  let ext0 = extension_fol_prop ~obs store p0 in
-	  let assert1 = assert_of_fol ~obs store p1 in
-	  let assert2 = Option.fold (assert_of_fol ~obs store) [] p2_opt in
-	  [Code.cond (Ext.succeeds ext0) assert1 assert2]
-      | _ -> invalid_arg "Fol.code_fol_prop: disjunction or negation"
-    and code_fol ~obs store frel : fol -> Code.t list = function
+	  let _vars1, ext0 = extension_of_fol ~obs store vars p0 in
+	  let lc1 = code_fol_prop ~obs store mode vars p1 in
+	  let lc2 = Option.fold (fun p2 -> code_fol_prop ~obs store mode vars p2) [] p2_opt in
+	  [Code.cond (Ext.succeeds ext0) lc1 lc2]
+      | _ -> invalid_arg "Fol.code_fol_prop: disjunction, negation, or optional"
+    and code_fol ~obs store mode vars : fol -> Code.t list = function
       | FTrue -> []
       | FBound v -> [] (* assert false *)
       | FEqual (x,expr) ->
-	  let exp = extension_expr_prop ~obs store expr in
+	  let vars1, exp = extension_of_expr ~obs store vars expr in
 	  [Code.equal x exp]
       | FAssign (x,y) ->
 	  [Code.assign x y]
 	  [Code.unify x y]
       | FDiff (x,y) -> assert false
       | FStat (s,p,o,t,src) ->
-	  [frel (store#get_statement :> rel)
+	  [mode#update (store#get_statement :> rel)
 	     ((Store._s, s) :: (Store._p, p) :: (Store._o, o) :: if t = "" then [] else [(Store._t, t)])]
       | FClass (cl,s,t,src) ->
-	  [frel (store#get_class cl :> rel)
+	  [mode#update (store#get_class cl :> rel)
 	     ((Store._s, s) :: if t = "" then [] else [(Store._t, t)])]
       | FProp (lm,pr,s,o,t,src) ->
-	  [frel (store#get_property pr :> rel)
+	  [mode#update (store#get_property pr :> rel)
 	     ((Store._s, s) :: (Store._o, o) :: if t = "" then [] else [(Store._t, t)])]
       | FFunct (funct,x,args,src) ->
-	  [frel (store#get_functor funct (Array.length args) :> rel)
+	  [mode#update (store#get_functor funct (Array.length args) :> rel)
 	     (("0", x) :: Array.to_list (Array.mapi (fun i arg -> (string_of_int (i+1), arg)) args))]
       | FPred _
       | FOrder _
 	  invalid_arg "Fol.code_fol: predicates cannot be asserted"
       | FProc (proc,args) ->
 	  [Code.proc proc
-	     (List.map (fun (pp,e) -> (pp,extension_expr_prop ~obs store e)) args)]
+	     (List.map
+		(fun (pp,e) ->
+		  let vars1, exp = extension_of_expr ~obs store vars e in
+		  pp, exp)
+		args)]
       | FDisplay e ->
-	  [Code.display (extension_expr_prop ~obs store e)]
+	  let vars1, exp = extension_of_expr ~obs store vars e in
+	  [Code.display exp]
       | FForthe (p1,p2) ->
-	  let ext1 = extension_fol_prop ~obs store p1 in
-	  let assert2 = assert_of_fol ~obs store p2 in
-	  [Code.foreach ext1 assert2]
-      | FForeach (p1,p2) ->
-	  let ext1 = extension_fol_prop ~obs store p1 in
-	  let assert2 = assert_of_fol ~obs store p2 in
-	  [Code.foreach ext1 assert2]
-      | FForany (p1,p2) ->
-	  let ext1 = extension_fol_prop ~obs store p1 in
-	  let assert2 = assert_of_fol ~obs store p2 in
-	  [Code.forany ext1 assert2]
+	  if mode#is_assert
+	  then
+	    let vars1, ext = extension_of_fol ~obs store vars p1 in
+	    let lc = code_fol_prop ~obs store assertor vars1 p2 in
+	    [Code.foreach ext lc]
+	  else invalid_arg "Ambiguous update: retracting on 'the'"
+      | FForEvery (p1,p2) ->
+	  if mode#is_assert
+	  then
+	    let vars1, ext = extension_of_fol ~obs store vars (Prop.And (p1, Prop.Not p2)) in
+	    let lc = code_fol_prop ~obs store assertor vars1 p2 in
+	    [Code.foreach ext lc]
+	  else invalid_arg "Ambiguous update: retracting on 'every'"
+      | FForOnly (p1,p2) ->
+	  if mode#is_assert
+	  then
+	    let vars1, ext = extension_of_fol ~obs store vars (Prop.And (Prop.Not p1, p2)) in
+	    let lc = code_fol_prop ~obs store retractor vars1 p2 in
+	    [Code.foreach ext lc]
+	  else invalid_arg "Ambiguous update: retracting on 'only'"
+      | FForNo (p1,p2) ->
+	  if mode#is_assert
+	  then
+	    let vars1, ext = extension_of_fol ~obs store vars (Prop.And (p1, p2)) in
+	    let lc = code_fol_prop ~obs store retractor vars1 p2 in
+	    [Code.foreach ext lc]
+	  else invalid_arg "Ambiguous update: retracting on 'no'"
+      | FForany (p1,p2) -> invalid_arg "Ambiguous update: 'for any'"
+(*
+	  let vars1, ext = extension_of_fol ~obs store vars p1 in
+	  let lc = code_fol_prop ~obs store vars1 p2 in
+	  [Code.forany ext lc]
+*)
       | FForN (n,x,p1) ->
-	  let assert1 = assert_of_fol ~obs store p1 in
-	  [Code.repeat n assert1]
+	  if mode#is_assert
+	  then
+	    let lc = code_fol_prop ~obs store assertor vars p1 in
+	    [Code.repeat n lc]
+	  else invalid_arg "Ambiguous update: retracting on 'exactly N'"
       | FGiven (p0,p1) ->
-	  let assert0 = code_fol_prop ~obs store Code.add p0 in
-	  let retract0 = code_fol_prop ~obs store Code.remove p0 in
-	  let assert1 = assert_of_fol ~obs store p1 in
-	  [Code.given assert0 retract0 assert1]
+	  if mode#is_assert
+	  then
+	    let assert0 = code_fol_prop ~obs store assertor vars p0 in
+	    let retract0 = code_fol_prop ~obs store retractor vars p0 in
+	    let assert1 = code_fol_prop ~obs store mode vars p1 in
+	    [Code.given assert0 retract0 assert1]
+	  else assert false
       | FLoop (p0,p1) ->
-	  let ext0 = extension_fol_prop ~obs store p0 in
-	  let assert1 = assert_of_fol ~obs store p1 in
-	  [Code.loop ext0 assert1]
+	  if mode#is_assert
+	  then
+	    let vars1, ext = extension_of_fol ~obs store vars p0 in
+	    let lc = code_fol_prop ~obs store mode vars1 p1 in
+	    [Code.loop ext lc]
+	  else assert false
+
+    let assert_of_fol ~obs store f = code_fol_prop ~obs store assertor [] f
+
+    let retract_of_fol ~obs store f = code_fol_prop ~obs store assertor [] (Prop.Not f)
 
   end
     let uri_InsertAn = Qname (prefix, "InsertAn")
     let uri_InsertEvery = Qname (prefix, "InsertEvery")
     let uri_InsertOnly = Qname (prefix, "InsertOnly")
+    let uri_InsertNo = Qname (prefix, "InsertNo")
     let uri_For = Qname (prefix, "For")
     let uri_QuoteUnquote = Qname (prefix, "QuoteUnquote")
     let uri_ToggleOpt = Qname (prefix, "ToggleOpt")
   let item_an = menu_apply_factory#add_item "a __" in
   let item_every = menu_apply_factory#add_item "every __" in
   let item_only = menu_apply_factory#add_item "only the __" in
+  let item_no = menu_apply_factory#add_item "no __" in
   let item_opt = menu_apply_factory#add_item "is or __" in
   let item_trans = menu_apply_factory#add_item "__ transitively" in
   let _ = menu_apply_factory#add_separator () in
       refresh_widget_transf item_an (InsertQu Lisql.AST.An);
       refresh_widget_transf item_every (InsertQu Lisql.AST.Every);
       refresh_widget_transf item_only (InsertQu Lisql.AST.Only);
+      refresh_widget_transf item_no (InsertQu Lisql.AST.No);
       refresh_widget_transf item_opt ToggleOpt;
       refresh_widget_transf item_trans ToggleTrans;
       refresh_widget item_name insert_s1;
 	(fun () -> callbacks#transf (Lisql.Transf.InsertQu Lisql.AST.Every));
       item_only # connect # activate ~callback:
 	(fun () -> callbacks#transf (Lisql.Transf.InsertQu Lisql.AST.Only));
+      item_no # connect # activate ~callback:
+	(fun () -> callbacks#transf (Lisql.Transf.InsertQu Lisql.AST.No));
       item_opt # connect # activate ~callback:
 	(fun () -> callbacks#transf Lisql.Transf.ToggleOpt);
       item_trans # connect # activate ~callback:
 	~text:"Set 'every' as the determiner";
       tooltips#set_tip item_only#coerce
 	~text:"Set 'only the' as the determiner";
+      tooltips#set_tip item_no#coerce
+	~text:"Set 'no' as the determiner";
 (*
       tooltips#set_tip cmd_subject#coerce
 	~text:"Reformulate the sentence so as to put the current focus as subject";
 	| Lisql.AST.An -> Logui.uri_InsertAn
 	| Lisql.AST.The -> assert false
 	| Lisql.AST.Every -> Logui.uri_InsertEvery
-	| Lisql.AST.Only -> Logui.uri_InsertOnly )
+	| Lisql.AST.Only -> Logui.uri_InsertOnly
+	| Lisql.AST.No -> Logui.uri_InsertNo )
     | ToggleNot -> Logui.uri_ToggleNot
     | ToggleMaybe -> Logui.uri_ToggleMaybe
     | ToggleOpt -> Logui.uri_ToggleOpt
 	  else if custom = "a" || custom = "an" then menu_transf (Lisql.Transf.InsertQu Lisql.AST.An)
 	  else if custom = "every" then menu_transf (Lisql.Transf.InsertQu Lisql.AST.Every)
 	  else if custom = "only" then menu_transf (Lisql.Transf.InsertQu Lisql.AST.Only)
+	  else if custom = "no" then menu_transf (Lisql.Transf.InsertQu Lisql.AST.No)
 	  else if custom = "opt" then menu_transf Lisql.Transf.ToggleOpt
 	  else if custom = "trans" then menu_transf Lisql.Transf.ToggleTrans
 	  else if custom = "?" then menu_name ()
 module Code = Code.Make
 module Prim = Primitive.Make
 module Store = Store.Make
-module Fol = Fol.Make
 module Namespace = Lisql_namespace
 module AST = Lisql_ast
 (*module Syntax1 = Lisql_syntax1 (* old-version parsing *)*)
   | The
   | Every
   | Only
-(*
   | No
+(*
   | Atleast of int
 *)
 and p1 =
 let the (f : p1) = Det (Qu (The, None), f)
 let every (f : p1) = Det (Qu (Every, None), f)
 let only (f : p1) = Det (Qu (Only, None), f)
+let no (f : p1) = Det (Qu (No, None), f)
 
 let name_is (n : Name.t) (f : p1) = Is (name_s1 n, f)
 
   | Quote _ -> true, lv
   | Ref v -> true, lv
   | Qu (An, v_opt) -> true, Option.fold (fun v -> v::lv) lv v_opt
-  | Qu ((The | Every | Only), _) -> false, lv
+  | Qu ((The | Every | Only | No), _) -> false, lv
 and accessible_vars_p1 ?(lv = []) = function
   | Type _ -> lv
   | Role (_, np) ->

src/lisql_concept.ml

 class concept_answers ~obs store gv (s : s) =
   let lv = List.rev (accessible_vars_s s) in
   let fol = Lisql_semantics.fol_s ~obs store gv s in
-  let _, _, fol = Fol.eval_fol_prop (LSet.empty ()) fol in
-  let ext = Fol.extension_of_fol ~obs store fol in
+  let _vars, ext = Fol.extension_of_fol ~obs store [] fol in (* TODO: use _vars instead of lv ? *)
 let _ = prerr_endline ext#string in
   let rel = ext#relation (store :> Extension.store) lv in
   let nb = Rel.cardinal rel in
 	| Qu (qu,_) ->
 	    List.fold_left
 	      (fun res q -> if q = qu then res else InsertQu q :: res)
-	      ltransf [An; Every; Only]
+	      ltransf [An; Every; Only; No]
 	| _ -> ltransf in
       let k' = Det1 (det,f,k) in
       let w_int, s = intent_p1 ~obs store gv f k' in

src/lisql_display.ml

   | The -> [`Kwd "the"]
   | Every -> [`Kwd "every"]
   | Only -> [`Kwd "only the"]
+  | No -> [`Kwd "no" ]
 and display_p1_vp ~obs store k prec f =
   [`Focus (AtP1 (f,k), display_p1_vp_aux ~obs store k prec f)]
 and display_p1_vp_aux ~obs store k prec = function

src/lisql_semantics.ml

   | An ->
       Prop.And (d1 x, d2 x)
   | The | Every ->
-      Prop.Atom (Fol.FForeach (d1 x, d2 x))
+      Prop.Atom (Fol.FForEvery (d1 x, d2 x))
   | Only ->
-      Prop.Atom (Fol.FForeach (d2 x, d1 x))
+      Prop.Atom (Fol.FForOnly (d1 x, d2 x))
+  | No ->
+      Prop.Atom (Fol.FForNo (d1 x, d2 x))
 and fol_p1 ~obs store gv (x : Extension.var) : p1 -> Fol.fol_prop = function
   | Type a ->
       Prop.Atom (Fol.FClass (a, x, "", ""))
+(* optimization leading to bugs in updates: ex., 'every fournisseur not remise ?' *)
+(*
   | Role (RAtom _ as r, Det (Qu (An, None), Thing)) ->
       fol_p2 ~obs store gv [] x "" r
+*)
   | Role (r1, Det (Qu (An, None), Role (r2, np))) when r1 = r2 && is_transitive ~obs store r1 ->
       fol_p1 ~obs store gv x (Role (r2,np))
   | Role (r,np) ->
 
 let rec fol_of_assertion ~obs store a =
   let gv = new gen_var in
-  let f1 = fol_s ~obs store gv a in
-  let _, _, f2 = Fol.eval_fol_prop (LSet.empty ()) f1 in
-  f2
+  fol_s ~obs store gv a
 
-let rec fol_of_class ~obs store bounded_vars x f =
+let fol_of_class ~obs store x f =
   let gv = new gen_var in
-  let f1 = fol_p1 ~obs store gv x f in
-  try
-    let _, vars, f2 = Fol.eval_fol_prop bounded_vars f1 in
-    if List.mem x vars
-    then false, f2
-    else raise (Fol.Unbound x)
-  with Fol.Unbound v ->
-    fol_of_class ~obs store bounded_vars x (And [Type Rdfs.uri_Resource; f])
+  fol_p1 ~obs store gv x f
+
 
            (* assertions *)
 
   | SMaybe s -> failwith "Invalid update: optional S (maybe)"
 and check_update_s1 = function
   | Det (Qu (An,_), f1) -> check_update_p1 f1
-  | Det (Qu ((The | Every | Only),_), f1) -> ()
+  | Det (Qu ((The | Every | Only | No),_), f1) -> ()
   | Det (_, f1) -> check_update_p1 f1
   | NAnd lnp -> List.iter check_update_s1 lnp
   | NOr lnp -> failwith "Invalid update: some disjunction between NPs"
     (* the i-th argument is unsignificant, and therefore allowed to be Thing *)
     
 	   
-let rec retract_s = function
+let rec retract_s = function s -> SNot s
+(*
   | Is (np,c) -> Is (np, Not c)
   | SAnd l -> SAnd (List.map retract_s l)
   | _ -> failwith "Lisql_semantics.retract_s: invalid coordination (or, maybe, not)"
+*)
 
 let tell store ~src (a : s) : unit =
   check_update_s a;
 
 let ask ~obs store (a : s) : bool =
   let fol = fol_of_assertion ~obs store a in
-  let ext = Fol.extension_of_fol ~obs store fol in
+  let _, ext = Fol.extension_of_fol ~obs store [] fol in
   ext#succeeds (store :> Extension.store) []
 
            (* extension *)
 let extension_s ~obs store (s : s) : Extension.t =
   Common.prof "Lisql_semantics.extension_s" (fun () ->
     let fol = fol_of_assertion ~obs store s in
-    let ext = Fol.extension_of_fol ~obs store fol in
+    let vars, ext = Fol.extension_of_fol ~obs store [] fol in
     ext)
 
+let rec ext_of_class ~obs store bounded_vars x f =
+  let f1 = fol_of_class ~obs store x f in
+  try
+    let vars, ext = Fol.extension_of_fol ~obs store bounded_vars f1 in
+    if List.mem x vars
+    then ext
+    else raise (Fol.Unbound x)
+  with Fol.Unbound v ->
+    ext_of_class ~obs store bounded_vars x (And [Type Rdfs.uri_Resource; f])
 
 let extension_p1 ~obs store ?(bounded_vars = LSet.empty ()) (f : p1) : Extension.t =
   Common.prof "Root.extension" (fun () ->
-    let _, fol = fol_of_class ~obs store bounded_vars var_root f in
-    let ext = Fol.extension_of_fol ~obs store fol in
+    let ext = ext_of_class ~obs store bounded_vars var_root f in
 (*print_endline ("Lisql.extension of: " ^ ext#string);*)
     ext)
 

src/lisql_syntax.ml

     [ "some" -> An
     | "the" -> The
     | "every" -> Every
-    | "only" -> Only ]
+    | "only" -> Only
+    | "no" -> No ]
 and parse_block = dcg "block"
     [ _ = parse_left_square_bracket; c = OPT parse_p1_seq ELSE Thing; _ = parse_right_square_bracket -> c
     | funct, i_opt, args = parse_struct_arg when "" i_opt = None -> Struct (funct,args) ]
     [ An -> "some"
     | The -> "the"
     | Every -> "every"
-    | Only -> "only" ]
+    | Only -> "only"
+    | No -> "no" ]
 and print_block = ipp
     [ Thing -> "[]"
     | Struct (funct,args) -> print_struct_arg of funct, None, args