Commits

Sébastien Ferré committed 91fc652

Bug fixes in transformations.

Comments (0)

Files changed (4)

 *)
 
     val h : (string, int ref) Hashtbl.t = Hashtbl.create 11
+    val mutable generated : var list = []
+
     method get_prefix prefix =
       let cpt =
 	try Hashtbl.find h prefix
 	  Hashtbl.add h prefix cpt;
 	  cpt in
       incr cpt;
-      if prefix <> "" && !cpt = 1
-      then prefix
-      else prefix ^ string_of_int !cpt
+      let v =
+	if prefix <> "" && !cpt = 1
+	then prefix
+	else prefix ^ string_of_int !cpt in
+      generated <- v::generated;
+      v
 
     method get = self#get_prefix ""
+
+    method generated v = List.mem v generated
   end
 
 let var_list = 
   | Det (Name n, _), Det (Qu (An,_), f2) -> Ext.mem (store#get_entity n) (store#tab_extent ~obs f2 : Ext.t)
   | Det (Qu (An,_), f1), Det (Qu (An,_), f2) -> entails_p1 ~obs store f1 f2
   | _ -> same_s1 ~obs store np1 np2
+and entails_s2 det1 det2 =
+  match det1, det2 with
+  | Name n1, Name n2 -> n1 = n2
+  | Name _, Qu _ -> true
+  | Ref v1, Ref v2 -> v1 = v2
+  | Ref _, Qu _ -> true
+  | Qu (qu1,_), Qu (qu2,_) -> entails_qu qu1 qu2
+  | _ -> false
+and entails_qu qu1 qu2 =
+  match qu1, qu2 with
+  | _, An -> true
+  | _ -> qu1 = qu2
 and entails_p1 ~obs store f1 f2 =
   match f1, f2 with
   | Type a1, Type a2 ->

src/lisql_concept.ml

       else
 	let supp = (nb,nb) in
 	List.fold_left
-	  (fun varmap v -> Varmap.add v supp varmap)
+	  (fun varmap v ->
+	    if gv#generated v
+	    then varmap
+	    else Varmap.add v supp varmap)
 	  Varmap.empty self#accessible_vars
     method in_ext (rank : int) (ext : Ext.t) : supp =
       if rank = 0
     method equal_vars (rank : int) : supp Varmap.t =
       List.fold_left
 	(fun varmap v ->
-	  let supp =
-	    if rank = 0
-	    then
-	      let i =
-		self#fold_answers
-		  (fun acc m ->
-		    if window_var w m v
-		    then acc+1
-		    else acc)
-		  0 in
-	      (i, self#nb_answers)
-	    else
-	      match self#rank_ext rank with
-	      | None -> (0,0)
-	      | Some e ->
-		  let n = Ext.cardinal e in
-		  (n,n) in
-	  if not (is_empty_supp supp)
-	  then Varmap.add v supp varmap
-	  else varmap)
+	  if gv#generated v
+	  then varmap
+	  else
+	    let supp =
+	      if rank = 0
+	      then
+		let i =
+		  self#fold_answers
+		    (fun acc m ->
+		      if window_var w m v
+		      then acc+1
+		      else acc)
+		    0 in
+		(i, self#nb_answers)
+	      else
+		match self#rank_ext rank with
+		| None -> (0,0)
+		| Some e ->
+		    let n = Ext.cardinal e in
+		    (n,n) in
+	    if not (is_empty_supp supp)
+	    then Varmap.add v supp varmap
+	    else varmap)
 	Varmap.empty
 	self#accessible_vars
 
       let s = intent_s ~obs store gv s0 k in
       new concept_w0 ~obs store gv s ~ltransf ~insert_s1:true ~insert_p1:true
   | AtS1 (Det (det,f), k) ->
-      of_focus ~obs store (AtP1 (f, Det1 (det,f,k)))
+      let ltransf = ltransf_base (det = top_s2 && f = top_p1) in
+      let ltransf =
+	match det with
+	| Name _ -> Describe :: ltransf
+	| Qu (qu,_) ->
+	    List.fold_left
+	      (fun res q -> if q = qu then res else InsertQu q :: res)
+	      ltransf [An; Every; Only]
+	| _ -> ltransf in
+      let k' = Det1 (det,f,k) in
+      let w_int, s = intent_p1 ~obs store gv f k' in
+      let descr = descr_p1 f k' in
+      new concept_w1 ~obs store gv s w_int descr ~ltransf ~insert_s1:true ~insert_p1:true
   | AtS1 (np,k) ->
       let ltransf = ltransf_base (np = top_s1) in
       let s = intent_s1 ~obs store gv np k in
   | AtP1 (f,k) ->
       let ltransf = ltransf_base (f = top_p1) in
       let ltransf =
-	match k with
-	| Det1 (Name _, _, _) -> Describe :: ltransf
-	| Det1 (Qu (qu,_), _, _) ->
-	    List.fold_left
-	      (fun res q -> if q = qu then res else InsertQu q :: res)
-	      ltransf [An; Every; Only]
-	| _ -> ltransf in
-      let ltransf =
 	match f with
 	| Role (r,_) ->
 	    ( match r with

src/lisql_feature.ml

 
 (* insertion of features *)
 
-let focus_insert store (x : feature) (foc : focus) : focus option =
-  let foc' =
-    let xx =
-      match x#spec with
-      | Spec_Something -> `S1 (top_s2, top_p1)
-      | Spec_Name n ->
-	  ( match n with
-	  | Rdf.Blank _ ->
-	      ( match store#description ~obs:Tarpit.blind_observer n with 
-	      | Det (det,f) -> `S1 (det,f)
-	      | _ -> assert false )
-	  | _ -> `S1 (name_s2 n, top_p1) )
-      | Spec_Ref v -> `S1 (ref_s2 v, top_p1)
-      | Spec_Some v -> `S1 (var_s2 v, top_p1)
-      | Spec_Thing -> `P1 top_p1
-      | Spec_Class c -> `P1 (has_type c)
-      | Spec_Role (ori,p) -> `P1 (role ori p)
-      | Spec_Structure (funct,arity) -> `P1 (make_struct_arg funct arity 0)
-      | Spec_Argument (funct,arity,i) -> `P1 (make_struct_arg funct arity i) in
-    match xx with
-    | `S1 (d,f) ->
-	( match foc with
-	| AtS _ -> Transf.focus_and_s (Is (Det (d,f), top_p1)) foc
-	| AtS1 (Det (det,_c),k) -> Some (AtS1 (Det (Transf.merge_s2 det d, f), k))
-	| AtS1 _ -> Transf.focus_and_s1 (Det (d,f)) foc
-	| AtP1 (_c, Det1 (det,_,k)) -> Some (AtP1 (f, Det1 (Transf.merge_s2 det d, f, k)))
-	| AtP1 _ -> Transf.focus_and_p1 (Role (Self, Det (d,f))) foc
-	| _ -> None )
-    | `P1 f ->
-	( match foc with
-	| AtS _ ->
-	    ( match f with
-	    | Type _ | Struct _ -> Transf.focus_and_s (Is (an f, top_p1)) foc
-	    | _ -> Transf.focus_and_s (Is (top_s1,f)) foc )
-	| AtS1 (Det (det,c),k) -> Transf.focus_and_p1 f (AtP1 (c, Det1 (det,c,k)))
-	| AtS1 _ -> Transf.focus_and_s1 (an f) foc
-	| AtS2 (det, Det0 (_,c,k)) -> Transf.focus_and_p1 f (AtP1 (c, Det1 (det,c,k)))
-	| AtS2 _ -> None
-	| AtP1 _ -> Transf.focus_and_p1 f foc
-	| AtP2 _ -> None ) in
-  match foc' with
-  | None -> None
-  | Some foc' ->
-      let foc'' = focus_next_postfix_down foc' in
-      if Transf.focus_default_filter foc''
-      then Some foc''
-      else focus_next_postfix ~filter:Transf.focus_default_filter foc''
+let ast_of_spec store (spec : spec) : [`S1 of s2 * p1 | `P1 of p1] =
+  match spec with
+  | Spec_Something -> `S1 (top_s2, top_p1)
+  | Spec_Name n ->
+      ( match n with
+      | Rdf.Blank _ ->
+	  ( match store#description ~obs:Tarpit.blind_observer n with 
+	  | Det (det,f) -> `S1 (det,f)
+	  | _ -> assert false )
+      | _ -> `S1 (name_s2 n, top_p1) )
+  | Spec_Ref v -> `S1 (ref_s2 v, top_p1)
+  | Spec_Some v -> `S1 (var_s2 v, top_p1)
+  | Spec_Thing -> `P1 top_p1
+  | Spec_Class c -> `P1 (has_type c)
+  | Spec_Role (ori,p) -> `P1 (role ori p)
+  | Spec_Structure (funct,arity) -> `P1 (make_struct_arg funct arity 0)
+  | Spec_Argument (funct,arity,i) -> `P1 (make_struct_arg funct arity i)
+
+let focus_insert_aux store (x : feature) (foc : focus) : focus option =
+  match ast_of_spec store x#spec with
+  | `S1 (d,f) ->
+      ( match foc with
+      | AtS _ -> Transf.focus_and_s (Is (Det (d,f), top_p1)) foc
+      | AtS1 (Det (det,_c),k) when (entails_s2 det d || entails_s2 d det) ->
+	  Some (AtS1 (Det (Transf.merge_s2 det d, f), k))
+      | AtS1 _ -> Transf.focus_and_s1 (Det (d,f)) foc
+      | AtP1 (_c, Det1 (det,_,k)) -> Some (AtP1 (f, Det1 (Transf.merge_s2 det d, f, k)))
+      | AtP1 _ -> Transf.focus_and_p1 (Role (Self, Det (d,f))) foc
+      | _ -> None )
+  | `P1 f ->
+      ( match foc with
+      | AtS _ ->
+	  ( match f with
+	  | Type _ | Struct _ -> Transf.focus_and_s (Is (an f, top_p1)) foc
+	  | _ -> Transf.focus_and_s (Is (top_s1,f)) foc )
+      | AtS1 (Det (det,c),k) -> Transf.focus_and_p1 f (AtP1 (c, Det1 (det,c,k)))
+      | AtS1 _ -> Transf.focus_and_s1 (an f) foc
+(*      | AtS2 (det, Det0 (_,c,k)) -> Transf.focus_and_p1 f (AtP1 (c, Det1 (det,c,k))) *)
+      | AtP1 _ -> Transf.focus_and_p1 f foc
+      | _ -> None )
+
+let focus_simpl = function
+  | AtS1 (np, Is0 (_,f,k)) when np = top_s1 && f = top_p1 -> AtS (top_s,k)
+  | AtP1 (c, Det1 (det,_, Is0 (_,f,k))) when c = top_p1 && det = top_s2 && f = top_p1 -> AtS (top_s,k)
+  | AtP1 (f, Is1 (np,_,k)) when np = top_s1 && f = top_p1 -> AtS (top_s,k)
+  | foc -> foc
+
+let focus_tab_after_insert foc' =
+  let foc'' = focus_next_postfix_down foc' in
+  if Transf.focus_default_filter foc''
+  then Some foc''
+  else focus_next_postfix ~filter:Transf.focus_default_filter foc''
+
+let focus_insert store x foc =
+  Option.bind
+    (focus_insert_aux store x foc)
+    (fun foc' -> focus_tab_after_insert (focus_simpl foc'))
 
 let focus_insert_list store xs foc =
-  List.fold_left
-    (fun res x ->
-      Option.bind res
-	(fun foc -> focus_insert store x foc))
-    (Some foc) xs
+  Option.bind
+    (List.fold_left
+       (fun res x ->
+	 Option.bind res
+	   (fun foc -> focus_insert_aux store x foc))
+       (Some foc) xs)
+    focus_tab_after_insert
 
 let focus_insert_list_or store xs foc =
-  match xs with
-  | [] -> None
-  | x::xs1 ->
-      List.fold_left
-	(fun res x ->
-	  Option.bind res
-	    (fun foc ->
-	      Option.bind (Transf.focus_or foc)
-		(fun foc -> focus_insert store x foc)))
-	(focus_insert store x foc) xs1
+  Option.bind
+    (match xs with
+    | [] -> None
+    | x::xs1 ->
+	List.fold_left
+	  (fun res x ->
+	    Option.bind res
+	      (fun foc ->
+		Option.bind (Transf.focus_or foc)
+		  (fun foc -> focus_insert_aux store x foc)))
+	  (focus_insert_aux store x foc) xs1)
+    focus_tab_after_insert
 
 let focus_insert_list_not store xs foc =
-  List.fold_left
-    (fun res x ->
-      Option.bind res
-	(fun foc ->
-	  Option.bind (Transf.focus_and_not foc)
-	    (fun foc ->
-	      Option.bind (focus_insert store x foc)
-		(fun foc -> focus_up foc))))
-    (Some foc) xs
+  Option.bind
+    (List.fold_left
+       (fun res x ->
+	 Option.bind res
+	   (fun foc ->
+	     Option.bind (Transf.focus_and_not foc)
+	       (fun foc ->
+		 Option.bind (focus_insert_aux store x foc)
+		   (fun foc -> focus_up foc))))
+       (Some foc) xs)
+    focus_tab_after_insert

src/lisql_transf.ml

 let rec focus_delete : transf =
   fun foc ->
     match foc with
-    | AtS (s,k) -> if s = top_s then focus_up foc else focus_delete_s k
-    | AtS1 (np,k) -> if np = top_s1 then focus_up foc else focus_delete_s1 k
-    | AtS2 (det,k) -> if det = top_s2 then focus_up foc else focus_delete_s2 k
-    | AtP1 (f,k) -> if f = top_p1 then focus_up foc else focus_delete_p1 k
-    | AtP2 (r,k) -> if r = top_p2 then focus_up foc else focus_delete_p2 k
+    | AtS (s,k) -> focus_delete_s k
+    | AtS1 (np,k) -> focus_delete_s1 k
+    | AtS2 (det,k) -> focus_delete_s2 k
+    | AtP1 (f,k) -> focus_delete_p1 k
+    | AtP2 (r,k) -> focus_delete_p2 k
 and focus_delete_s k =
   match k with
   | SAndN (n,l,k') ->
 	| [] -> top_p1
 	| [f] -> f
 	| l' -> And l' in
-      Some (AtP1 (f',k'))
+      ( match k' with
+      | Det1 (det,_,k'') -> Some (AtS1 (Det (det,f'),k''))
+      | _ -> Some (AtP1 (f',k')) )
   | OrN (n,l,k') ->
       let f' =
 	match Common.list_remove_nth l n with
 	| [] -> top_p1
 	| [f] -> f
 	| l' -> Or l' in
-      Some (AtP1 (f',k'))
-  | _ -> Some (AtP1 (top_p1,k))
+      ( match k' with
+      | Det1 (det,_,k'') -> Some (AtS1 (Det (det,f'),k''))
+      | _ -> Some (AtP1 (f',k')) )
+  | _ ->
+      ( match k with
+      | Det1 (det,_,k') -> Some (AtS1 (Det (det,top_p1),k'))
+      | _ -> Some (AtP1 (top_p1,k)) )
 and focus_delete_p2 k =
   match k with
   | RAndN (n,l,k') ->
     | AtS2 _ -> None
     | AtP1 _ -> focus_and_p1 top_p1 foc
     | AtP2 _ -> focus_and_p2 top_p2 foc
-and focus_and_s (x : s) : transf =
+and focus_and_s x foc =
+  match x with
+  | SAnd lx ->
+      List.fold_left
+	(fun res x -> Option.bind res (fun foc -> focus_and_s_atom x foc))
+	(Some foc) lx
+  | _ -> focus_and_s_atom x foc
+and focus_and_s_atom (x : s) : transf =
   fun foc ->
     match focus_up_and foc with
     | AtS (s,k) ->
 	    then Some (AtS (top_s,k))
 	    else Some (AtS (x, SAndN (1, [s; x], k))))
     | _ -> None
-and focus_and_s1 (x : s1) : transf =
+and focus_and_s1 x foc =
+  match x with
+  | NAnd lx ->
+      List.fold_left
+	(fun res x -> Option.bind res (fun foc -> focus_and_s1_atom x foc))
+	(Some foc) lx
+  | _ -> focus_and_s1_atom x foc
+and focus_and_s1_atom (x : s1) : transf =
   fun foc ->
     match focus_up_and foc with
     | AtS1 (np,k) ->
 	      else Some (AtS1 (x, NAndN (List.length l, l@[x], k)))
 	| _ -> Some (AtS1 (x, NAndN (1, [np; x], k))))
     | _ -> None
-and focus_and_p1 (x : p1) : transf =
+and focus_and_p1 x foc =
+  match x with
+  | And lx ->
+      List.fold_left
+	(fun res x -> Option.bind res (fun foc -> focus_and_p1_atom x foc))
+	(Some foc) lx
+  | _ -> focus_and_p1_atom x foc
+and focus_and_p1_atom (x : p1) : transf =
   fun foc ->
     match focus_up_and foc with
     | AtP1 (f,k) ->
 	    then Some (AtP1 (top_p1,k))
 	    else Some (AtP1 (x, AndN (1, [f; x], k))))
     | _ -> None
-and focus_and_p2 (x : p2) : transf =
+and focus_and_p2 x foc =
+  match x with
+  | RAnd lx ->
+      List.fold_left
+	(fun res x -> Option.bind res (fun foc -> focus_and_p2_atom x foc))
+	(Some foc) lx
+  | _ -> focus_and_p2_atom x foc
+and focus_and_p2_atom (x : p2) : transf =
   fun foc ->
     match focus_up_and foc with
     | AtP2 (r,k) ->
     | AtS2 _ -> None
     | AtP1 _ -> focus_or_p1 top_p1 foc
     | AtP2 _ -> focus_or_p2 top_p2 foc
-and focus_or_s (x : s) : transf =
+and focus_or_s x foc =
+  match x with
+  | SOr lx ->
+      List.fold_left
+	(fun res x -> Option.bind res (fun foc -> focus_or_s_atom x foc))
+	(Some foc) lx
+  | _ -> focus_or_s_atom x foc
+and focus_or_s_atom (x : s) : transf =
   fun foc ->
     match focus_up_or foc with
     | AtS (s,k) ->
 	| SOr l -> Some (AtS (x, SOrN (List.length l, l@[x], k)))
 	| _ -> Some (AtS (x, SOrN (1, [s; x], k))) )
     | _ -> None
-and focus_or_s1 (x : s1) : transf =
+and focus_or_s1 x foc =
+  match x with
+  | NOr lx ->
+      List.fold_left
+	(fun res x -> Option.bind res (fun foc -> focus_or_s1_atom x foc))
+	(Some foc) lx
+  | _ -> focus_or_s1_atom x foc
+and focus_or_s1_atom (x : s1) : transf =
   fun foc ->
     match focus_up_or foc with
     | AtS1 (np,k) ->
 	| NOr l -> Some (AtS1 (x, NOrN (List.length l, l@[x], k)))
 	| _ -> Some (AtS1 (x, NOrN (1, [np;x], k))) )
     | _ -> None
-and focus_or_p1 (x : p1) : transf =
+and focus_or_p1 x foc =
+  match x with
+  | Or lx ->
+      List.fold_left
+	(fun res x -> Option.bind res (fun foc -> focus_or_p1_atom x foc))
+	(Some foc) lx
+  | _ -> focus_or_p1_atom x foc
+and focus_or_p1_atom (x : p1) : transf =
   fun foc ->
     match focus_up_or foc with
     | AtP1 (f,k) ->
 	| Or l -> Some (AtP1 (x, OrN (List.length l, l@[x], k)))
 	| _ -> Some (AtP1 (x, OrN (1, [f;x], k))) )
     | _ -> None
-and focus_or_p2 (x : p2) : transf =
+and focus_or_p2 x foc =
+  match x with
+  | ROr lx ->
+      List.fold_left
+	(fun res x -> Option.bind res (fun foc -> focus_or_p2_atom x foc))
+	(Some foc) lx
+  | _ -> focus_or_p2_atom x foc
+and focus_or_p2_atom (x : p2) : transf =
   fun foc ->
     match focus_up_or foc with
     | AtP2 (r,k) ->