Commits

Sébastien Ferré committed 73f897a

[logicMonad] new version of [sumonad], based on related paper

  • Participants
  • Parent commits e98cfe8

Comments (0)

Files changed (5)

monad/example_sparql.ml

+
+type var = string
+type term = URI of string | Literal of string | Var of var
+type binding = (var * term option) list
+
+let project lv binding =
+  List.map (fun v -> try List.assoc v binding with _ -> None) lv
+
+class type state =
+object
+  method binding : binding
+  method bind : binding -> state
+  method get : var -> term option
+  method subst : term -> term
+  method triples : term * term * term -> binding list
+end
+
+type gp = unit u_monad with u_state = state and u_error = string
+type constr = bool u_monad with u_state = state and u_error = string
+type expr = term u_monad with u_state = state and u_error = string
+type query = (term option list) u_monad with u_state = state and u_error = string
+
+let get v : expr = u_def (
+  let state = u_state in
+  match state#get v with
+    | Some t -> return t
+    | None -> raise "unbound variable")
+
+(* queries *)
+
+let ask (p : gp) : query = u_def (succeeds p; return [])
+
+let select (lv : var list) (p : gp) = u_def (p; let state = u_state in return (project lv state#binding))
+
+(* graph patterns *)
+
+let triple (s : term) (p : term) (o : term) = u_def (
+  let state = u_state in
+  let s = return (state#subst s) in
+  let p = return (state#subst p) in
+  let o = return (state#subst o) in
+  let binding = LogicMonad.List.choose (state#triples (s,p,o)) in
+  u_state <- state#bind binding)
+
+let join (p1 : gp) (p2 : gp) : gp = u_def (p1; p2)
+
+let union (p1 : gp) (p2 : gp) : gp = u_def (p1 | p2)
+
+let minus (p1 : gp) (p2 : gp) : gp = u_def (p1; fails p2)
+
+let optional (p1 : gp) : gp = u_def (if _ = p1 then return () else return ())
+
+let filter (p : gp) (c : constr) : gp = u_def (p; let b = c in guard b)
+
+let bind (v : var) (t : term) : gp = u_def (
+  let state = u_state in
+  match state#get v with
+    | Some t0 -> guard (t0 = t)
+    | None -> u_state <- state#bind [(v, Some t)])
+
+class type aggregator =
+object
+  method put : term list -> term -> unit
+  method get : (term list * term) u_monad
+end
+
+let aggreg (init : 'a) (f : 'a -> term option -> 'a) (h : 'a -> term option) ~(group_by : var list) ~(as_ : var) (y : var) (p1 : gp) : gp =
+  let lz = group_by in
+  let x = as_ in
+  u_def (
+    let l = fold
+      (fun l binding ->
+	let k = List.map binding#get lz in
+	let v = binding#get y in
+	let v0 = try List.assoc k l with Not_found -> init in
+	(k, f v0 v) :: List.remove_assoc k l)
+      []
+      (u_def (p1; u_state)) in
+    let k, v = LogicMonad.List.choose l in
+    let state = u_state in
+    u_state <- state#bind ((x, h v) :: List.combine lz k))
+
+let count =
+  aggreg 0
+    (fun n -> function None -> n | Some _ -> n+1)
+    (fun n -> Some (Literal (string_of_int n)))
+let count_distinct =
+  aggreg []
+    (fun l -> function None -> l | Some x -> if List.mem x l then l else x::l)
+    (fun l -> Some (Literal (string_of_int (List.length l))))
+let group_concat ?(sep = "") =
+  aggreg ""
+    (fun s -> function Some (Literal s2) -> if s="" then s2 else s^sep^s2 | _ -> s)
+    (fun s -> if s="" then None else Some (Literal s))
+
+(* constraints *)
+
+let exists (p1 : gp) : constr = u_def (if _ = succeeds p1 then return true else return false)
+
+let not_exists (p1 : gp) : constr = u_def (if _ = fails p1 then return true else return false)
+
+let diff (v1 : var) (v2 : var) : constr = u_def (let t1 = get v1 in let t2 = get v2 in return (t1 = t2))
+
+(* expressions *)
+
+let concat (v1 : var) (v2 : var) : expr = u_def (
+  let t1 = get v1 in
+  let t2 = get v2 in
+  match t1, t2 with
+    | Literal s1, Literal s2 -> return (Literal (s1^s2)))
+
+
+(* examples *)
+
+(* let q_femme = u_def (let x = femme in u_return x) = u_def femme = femme *)
+let q_femme = select ["x"] (triple (Var "x") (URI "a") (URI "femme"))
+
+(* let q_person = u_def (femme | homme) *)
+
+(* let q_brother = u_def (let x,z = parent in let y,z = parent in u_guard (x <> y); u_return (x,y)) *)
+let q_brother = select ["x";"y"]
+  (filter
+     (join
+	(triple (Var "x") (URI "parent") (Var "z"))
+	(triple (Var "y") (URI "parent") (Var "z")))
+     (diff "x" "y"))
+
+let q_child_count = select ["x";"n"]
+  (count_distinct "y" ~as_:"n"
+     (triple (Var "y") (URI "parent") (Var "x"))
+     ~group_by:["x"])

monad/examples.ml

+
+module State =
+struct
+  type t = { cpt : int }
+
+  let init = { cpt = 0 }
+    
+  let get = u_def (let s = u_state in return s.cpt)
+  let incr = u_def (let s = u_state in u_state <- { cpt = s.cpt + 1 })
+  let print_line str = u_def (return (print_endline str))
+end
+
+let rec safe_aux (p1,p2,p3) = (* low diagonal, line, high diagonal *)
+  function
+    | [] -> true
+    | p::ps1 -> p <> p1 && p <> p2 && safe_aux (p1-1,p2,p3+1) ps1
+let safe p ps1 = safe_aux (p-1,p,p+1) ps1
+
+let rec nqueens n k =
+  if k=0
+  then u_def (
+    let i = State.get in
+    State.print_line ("k=" ^ string_of_int i);
+    return [])
+  else u_def (
+    let ps1 = State.incr; nqueens n (k-1) in
+    let p = LogicMonad.Int.range 1 n in
+    guard (safe p ps1);
+    return (p::ps1))
+
+let print_sol ps =
+  List.iter (fun p -> print_int p; print_char ' ') ps;
+  print_newline ()
+
+let _ = 
+  let n = try int_of_string Sys.argv.(1) with _ -> 4 in
+  let k = try int_of_string Sys.argv.(2) with _ -> 10 in
+  if u_test with u_state = State.init;
+    succeeds (nqueens n n)
+  then
+    print_endline "There are solutions!";
+(*
+  let sols = u_run with u_state = State.init; bagof ~limit:k (nqueens n n) in
+  List.iter print_sol sols
+*)
+  u_run with u_state = State.init;
+    iter ~limit:k
+      print_sol
+      (nqueens n n)
+
+(* ---------------- *)
+
+class virtual expr =
+object (self)
+  method virtual get : string -> string u_monad with u_state = State.t and u_error = string
+  method virtual look : string -> string u_monad with u_state = State.t and u_error = string
+
+  method parse_add = u_def (
+    let v1 = self#parse_mult in
+    let f = self#parse_add_aux in
+    return (f v1))
+  method parse_add_aux = u_def
+    begin
+      | self#look "+";
+        let v2 = self#parse_mult in
+	let f = self#parse_add_aux in
+	return (fun v1 -> f (v1 + v2))
+      | return (fun v1 -> v1)
+    end
+  method parse_mult = u_def (
+    let v1 = self#parse_atom in
+    let f = self#parse_mult_aux in
+    return (f v1))
+  method parse_mult_aux = u_def
+    begin
+      | self#look "*";
+        let v2 = self#parse_atom in
+	let f = self#parse_mult_aux in
+	return (fun v1 -> f (v1 * v2))
+      | return (fun v1 -> v1)
+    end
+  method parse_atom = u_def
+    begin
+      | let s = self#get "[0-9]+" in
+	return (int_of_string s)
+      | self#look "(";
+	let v = self#parse_add in
+	self#look ")";
+	return v
+    end
+end
+
+(* ----------------- *)
+
+type tree = Leaf | Node of int * tree * tree
+
+let rec post_order = function
+  | Leaf -> u_def return 0
+  | Node (i,left,right) -> u_def (
+    let sum_left = post_order left in
+    let sum_right = post_order right in
+    let sum = return (sum_left + sum_right + i) in
+    yield sum;
+    return sum)
+
+let post_order_run =
+  u_run
+    try post_order (Node (1, Node (2, Leaf, Leaf), Node (3, Leaf, Node (4, Leaf, Leaf)))); return ()
+    with sum -> return (print_int sum; print_newline ())
+(* post_order sum: 2, 4, 7, 10 *)

monad/logicMonad.ml

+
+(* streams as implementation of MonadPlus *)
+
+module Stream =
+struct
+  type 'a t =
+    | Nil
+    | Single of 'a
+    | Cons of 'a * 'a t
+    | Concat of 'a t * 'a t
+    | Lazy of 'a t Lazy.t
+
+  let make_concat = function
+      | Nil, str2 -> str2
+      | str1, Nil -> str1
+      | Single x, str2 -> Cons (x,str2)
+      | str1, str2 -> Concat (str1,str2)
+
+  let return (x : 'a) : 'a t = Single x
+
+  let rec bind (str : 'a t) (k : 'a -> 'b t) : 'b t =
+    match str with
+      | Nil -> Nil
+      | Single x -> k x
+      | Cons (x,str1) ->
+	let k_x = k x in
+	let k_str1 = bind str1 k in
+	make_concat (k_x, k_str1)
+      | Concat (str1,str2) ->
+	let k_str1 = bind str1 k in
+	let k_str2 = bind str2 k in
+	make_concat (k_str1, k_str2)
+      | Lazy lstr -> Lazy (lazy (bind (Lazy.force lstr) k))
+
+  let mzero = Nil
+
+  let mplus str1 str2 = make_concat (str1,str2)
+
+  let rec split : 'a t -> ('a * 'a t) option = function
+    | Nil -> None
+    | Single x -> Some (x, Nil)
+    | Cons (x,str1) -> Some (x, str1)
+    | Concat (str1,str2) ->
+      ( match split str1 with
+	| None -> split str2
+	| Some (x1,str11) -> Some (x1, make_concat (str11,str2)) )
+    | Lazy lstr -> split (Lazy.force lstr)
+
+  let rec interleave str1 str2 =
+    match split str1 with
+      | None -> str2
+      | Some (x,str11) -> Cons (x, Lazy (lazy (interleave str2 str11)))
+
+  let rec fold (f : 'acc -> 'a -> 'acc) (init : 'acc) (str : 'a t) : 'acc =
+    match split str with
+      | None -> init
+      | Some (x,str1) -> fold f (f init x) str1
+end
+
+(* types for MonadPlus(MonadState(MonadError(Id))) *)
+
+type ('a,'e) either = Result of 'a | Error of 'e
+
+type ('a,'e,'s) t = 's -> (('a,'e) either * 's) Stream.t
+
+let lift (k : 'a -> ('b,'e,'s) t) : ('a,'e) either * 's -> (('b,'e) either * 's) Stream.t = function
+  | Result x, s1 -> k x s1
+  | Error e, s1 -> Stream.return (Error e, s1)
+
+(* implementation for Monad *)
+
+let return (x : 'a) : ('a,'e,'s) t =
+  fun s -> Stream.return (Result x, s)
+
+let rec bind (m : ('a,'e,'s) t) (k : 'a -> ('b,'e,'s) t) : ('b,'e,'s) t =
+  fun s -> Stream.bind (m s) (lift k)
+
+(* implementation for MonadPlus *)
+
+let mzero : ('a,'e,'s) t =
+  fun s -> Stream.mzero
+
+let mplus (m1 : ('a,'e,'s) t) (m2 : ('a,'e,'s) t) : ('a,'e,'s) t =
+  fun s -> Stream.mplus (m1 s) (m2 s)
+
+let mguard (cond : bool) : (unit,'e,'s) t =
+  fun s ->
+    if cond
+    then Stream.return (Result (), s)
+    else Stream.mzero
+
+let rec msplit str =
+  match Stream.split str with
+    | None -> None
+    | Some (xes,str1) ->
+      match xes with
+	| Result x, s1 -> Some (x,s1,str1)
+	| Error _, _ -> msplit str1
+
+let ifte (m1 : ('a,'e,'s) t) (k1 : 'a -> ('b,'e,'s) t) (m2 : ('b,'e,'s) t) : ('b,'e,'s) t =
+  fun s ->
+    match msplit (m1 s) with
+      | None -> m2 s
+      | Some (x,s1,str1) -> Stream.mplus (k1 x s1) (Stream.bind str1 (lift k1))
+
+let once (m : ('a,'e,'s) t) : ('a,'e,'s) t =
+  fun s ->
+    match msplit (m s) with
+      | None -> Stream.mzero
+      | Some (x,s1,str1) -> Stream.return (Result x,s1)
+
+let mplus_fair (m1 : ('a,'e,'s) t) (m2 : ('a,'e,'s) t) : ('a,'e,'s) t =
+  fun s -> Stream.interleave (m1 s) (m2 s)
+
+let bind_fair (m : ('a,'e,'s) t) (k : 'a -> ('b,'e,'s) t) : ('b,'e,'s) t =
+  fun s ->
+    match msplit (m s) with
+      | None -> Stream.mzero
+      | Some (x,s1,str1) -> Stream.interleave (k x s1) (Stream.bind str1 (lift k))
+
+let rec fold ?(limit : int option) (f : 'acc -> 'a -> 'acc) (init : 'acc) (m : ('a,'e,'s) t) : ('acc,'e,'s) t =
+  fun s ->
+    let n = match limit with Some n when n>=0 -> n | _ -> -1 in
+    let res = fold_aux f init (m s) n in
+    Stream.return (Result res, s)
+and fold_aux f acc str n =
+  if n = 0
+  then acc
+  else
+    match msplit str with
+      | None -> acc
+      | Some (x,s1,str1) ->
+	let n1 = if n>0 then n-1 else -1 in
+	fold_aux f (f acc x) str1 n1
+
+(* implementation of MonadError *)
+
+let raise_ (e : 'e) : ('a,'e,'s) t =
+  fun s -> Stream.return (Error e, s)
+
+let rec catch (m : ('a,'e,'s) t) (k : 'e -> ('a,'e,'s) t) : ('a,'e,'s) t =
+  fun s ->
+    Stream.bind (m s) (fun xes ->
+      match xes with
+	| Result x, s1 -> Stream.return xes
+	| Error e, s1 -> k e s1)
+
+(* implementation of MonadState *)
+
+let get : ('s,'e,'s) t =
+  fun s -> Stream.return (Result s, s)
+
+let put (s2 : 's) : (unit,'e,'s) t =
+  fun s -> Stream.return (Result (), s2)
+
+let modify (f : 's -> 's) : (unit,'e,'s) t =
+  fun s -> Stream.return (Result (), f s)
+
+let local (s1 : 's1) (m : ('a,'e,'s1) t) : ('a,'e,'s) t =
+  fun s -> Stream.bind (m s1) (fun (xe,_) -> Stream.return (xe,s))
+
+(* composed monadic operations *)
+
+let yield e = mplus (raise_ e) (return ())
+
+let succeeds m = ifte (once m) (fun _ -> return ()) mzero
+let fails m = ifte (once m) (fun _ -> mzero) (return ())
+
+let exists m pred = succeeds (bind m (fun x -> mguard (pred x)))
+let for_all m pred = fails (bind m (fun x -> mguard (not (pred x))))
+
+let bagof ?limit m = fold ?limit (fun acc x -> x::acc) [] m
+
+(* running monads *)
+
+let run (m : ('a,'e,'s) t) (s : 's) : 'a =
+  match msplit (m s) with
+    | None -> raise Not_found
+    | Some (x,s1,str1) -> x
+
+let test (m : ('a,'e,'s) t) (s : 's) : bool =
+  match msplit (m s) with
+    | None -> false
+    | Some _ -> true
+
+(* primitive monads for syntax extension *)
+
+module PA_atom =
+struct
+  let return x = return x
+  let fail = mzero
+  let guard c = mguard c
+  let yield x = yield x
+
+  let local s = fun m -> local s m
+  let once = fun m -> once m
+  let succeeds = fun m -> succeeds m
+  let fails = fun m -> fails m
+  let bagof ?limit = fun m -> bagof ?limit m
+
+  let fold ?limit f init = fun m-> fold ?limit f init m
+  let iter ?limit f = fun m -> fold ?limit (fun _ x -> f x) () m
+  let exists pred = fun m -> exists m pred
+  let for_all pred = fun m -> for_all m pred
+end
+
+(* useful monads *)
+
+module Int =
+struct
+  let rec range (a  : int) (b : int) : (int,'e,'s) t =
+    bind (mguard (a <= b)) (fun _ -> mplus (return a) (range (a+1) b))
+end
+
+module List =
+struct
+  let rec choose : 'a list -> ('a,'e,'s) t = function
+    | [] -> mzero
+    | x::l -> mplus (return x) (choose l)
+
+  let rec map (f : 'a -> ('b,'e,'s) t) : 'a list -> ('b list,'e,'s) t = function
+    | [] -> return []
+    | x::lx -> bind (f x) (fun y -> bind (map f lx) (fun ly -> return (y::ly)))
+end
 OCAMLDOCFLAGS= -d doc $(INCLUDES)
 
 # The list of object files
-OBJ = sumonad.cmo
+OBJ = logicMonad.cmo
 
-all: sumonad.cma pa_sumonad.cmo
+all: logicMonad.cma pa_logicMonad.cmo
 	echo
 
-sumonad.cma: $(OBJ)
-	ocamlc $(OCAMLFLAGS) -a -o sumonad.cma $(OBJ)
-	ocamlopt $(OCAMLFLAGS) -a -o sumonad.cmxa $(OBJ:.cmo=.cmx)
+logicMonad.cma: $(OBJ)
+	ocamlc $(OCAMLFLAGS) -a -o logicMonad.cma $(OBJ)
+	ocamlopt $(OCAMLFLAGS) -a -o logicMonad.cmxa $(OBJ:.cmo=.cmx)
 
-pa_sumonad.cmo: pa_sumonad.ml
-	ocamlc -I +camlp4 camlp4lib.cma -pp camlp4orf -c pa_sumonad.ml
+pa_logicMonad.cmo: pa_logicMonad.ml
+	ocamlc -I +camlp4 camlp4lib.cma -pp camlp4orf -c pa_logicMonad.ml
 
-essai.exe: essai.ml
-	ocamlc -o essai.exe -pp "camlp4o -I . pa_sumonad.cmo" str.cma sumonad.cma essai.ml
+#all: sumonad.cma pa_sumonad.cmo
+#	echo
+
+#sumonad.cma: $(OBJ)
+#	ocamlc $(OCAMLFLAGS) -a -o sumonad.cma $(OBJ)
+#	ocamlopt $(OCAMLFLAGS) -a -o sumonad.cmxa $(OBJ:.cmo=.cmx)
+
+#pa_sumonad.cmo: pa_sumonad.ml
+#	ocamlc -I +camlp4 camlp4lib.cma -pp camlp4orf -c pa_sumonad.ml
+
+#essai.exe: essai.ml
+#	ocamlc -o essai.exe -pp "camlp4o -I . pa_sumonad.cmo" str.cma sumonad.cma essai.ml
 
 # Common rules
 .SUFFIXES: .ml .mli .cmo .cmi
 	ocamlopt $(OCAMLFLAGS) -c $<
 
 %.exe: %.ml
-	ocamlc -o $@ -pp "camlp4o -I . pa_sumonad.cmo" str.cma sumonad.cma $<
+	ocamlc -o $@ -pp "camlp4o -I . pa_logicMonad.cmo" str.cma logicMonad.cma $<
 
 # Documentationg
 html:

monad/pa_logicMonad.ml

+
+open Camlp4.PreCast
+open Syntax
+
+EXTEND Gram
+  GLOBAL: expr ctyp;
+
+  ctyp: LEVEL "simple"
+      [ [ a = SELF; "u_monad"; es_opt = OPT [ "with"; es = ctyp_args -> es ] ->
+         let e, s = match es_opt with Some es -> es | None -> <:ctyp< _ >>, <:ctyp< _ >> in
+         <:ctyp< LogicMonad.t $a$ $e$ $s$ >>
+	] ];
+
+  ctyp_args:
+    [ [ "u_state"; "="; s = ctyp; eo = OPT [ "and"; "u_error"; "="; e = ctyp -> e ] ->
+        let e = match eo with Some e -> e | None -> <:ctyp< _ >> in
+	e, s
+      | "u_error"; "="; e = ctyp; so = OPT [ "and"; "u_state"; "="; s = ctyp -> s ] ->
+        let s = match so with Some s -> s | None -> <:ctyp< _ >> in
+	e, s
+      ] ];
+
+  expr: LEVEL "top"
+      [ [ "u_def"; m = monad -> m
+	| "u_run"; s = state; m = monad -> <:expr< LogicMonad.run $m$ $s$ >>
+	| "u_test"; s = state; m = monad -> <:expr< LogicMonad.test $m$ $s$ >>
+	] ];
+
+  state:
+    [ [ s_opt = OPT [ "with"; "u_state"; "="; s = expr LEVEL "top"; ";" -> s ] ->
+      match s_opt with None -> <:expr< () >> | Some s -> s ] ];
+
+  monad:
+    [ [ m = atom -> <:expr< let open LogicMonad.PA_atom in $m$ >> ] ];
+
+  block:
+      [ [ "begin"; OPT "|"; m = alt; "end" -> m
+	| "("; OPT "|"; m = alt; ")" -> m 
+	] ];
+    
+  alt:
+      [ [ m1 = seq; m2o = OPT [ "|"; m2 = alt -> m2 ] ->
+        match m2o with
+	| None -> m1
+	| Some m2 -> <:expr< LogicMonad.mplus $m1$ $m2$ >>
+	] ];
+
+  seq:
+    [ [ m1 = atom; m2o = OPT [ ";"; m2 = seq -> m2 ] ->
+      match m2o with
+	| None -> m1
+	| Some m2 -> <:expr< LogicMonad.bind $m1$ (fun _ -> $m2$) >>
+        ] ];
+
+  atom:
+    [ [ m = block -> m
+      | "if"; x = ipatt; "="; m1 = alt; "then"; m2 = atom; m3o = OPT [ "else"; m3 = atom -> m3 ] ->
+        let k2 = <:expr< fun $pat:x$ -> $m2$ >> in
+        let m3 = match m3o with Some m3 -> m3 | None -> <:expr< LogicMonad.mzero >> in
+        <:expr< LogicMonad.ifte $m1$ $k2$ $m3$ >>
+      | "let"; (x,m1) = quantif; "in"; m2 = seq ->
+        <:expr< LogicMonad.bind $m1$ (fun $pat:x$ -> $m2$) >>
+      | "match"; e = expr LEVEL "top"; "with"; OPT "|"; k = conts ->
+        <:expr< fun s -> $k$ $e$ s >>
+      | "try"; m = alt; "with"; OPT "|"; k = conts ->
+        <:expr< LogicMonad.catch $m$ $k$ >>
+      | "raise"; e = expr LEVEL "top" -> <:expr< LogicMonad.raise_ $e$ >>
+      | "u_state"; "<-"; e = expr LEVEL "top" ->
+        <:expr< LogicMonad.put $e$ >>
+      | "u_state" ->
+        <:expr< LogicMonad.get >>
+      | "#"; id = a_LIDENT; le = LIST0 [ e = expr LEVEL "top" -> e ] ->
+        let app = List.fold_left (fun res arg -> <:expr< $res$ $arg$ >>) <:expr< u_state # $lid:id$ >> le in 
+	<:expr< fun u_state -> $app$ u_state >>
+      | m = expr LEVEL "top" -> m ] ];
+
+  quantif:
+      [ [ x = ipatt; "="; m = alt -> x, m ] ];
+
+  conts:
+    [ [ k1 = cont; k2o = OPT [ "|"; k2 = conts -> k2 ] ->
+      match k2o with
+	| None -> k1
+	| Some k2 -> <:expr< fun x -> LogicMonad.mplus ($k1$ x) ($k2$ x) >>
+      ] ];
+
+  cont:
+    [ [ x = ipatt; "->"; m = seq -> <:expr< fun [ $pat:x$ -> $m$ | _ -> LogicMonad.mzero ] >> ] ];
+ 
+END;