monad added but maybe not so exploited

src/Sorting.v

@@ -85,46 +85,76 @@ Parameter DefautltSort:mysort.
 Parameter EqDecS : forall x y : mysort, {x = y} + {x <> y}. (*TODO not a parameter maybe it can be derived from orderType*)
 Parameter relSort: rel mysort. (*TODO same*)
 
-(*removed parenthesis case*)
+
+
+Class Monad (M : Type -> Type) := {
+  ret : forall {A}, A -> M A;
+  bind : forall {A B}, M A -> (A -> M B) -> M B
+}.
+
 Inductive pat : Type :=
+  | void_pat
+  | eps_pat
   | and_pat (p:pat) (p':pat)
   | or_pat (p:pat) (p':pat)
   | star_pat (p : pat)
   | baseS_pat (s:mysort).
 
-
 Record term : Type := 
   Term {fixedpart : list mysort ; optpart : list (list mysort)}.
 
-  (* \sigma w (w1 + ... + wm)*  *)
+Inductive LSigma (A : Type) : Type :=
+  SigRet : list A -> LSigma A.
+
+(* Instance Monad_list : Monad list := {
+  ret := fun A x => [x]; 
+  bind := fun A B (l:seq A) (f:A -> seq B) => concat (map f l)
+}.   *)
+
+Arguments SigRet {A} .
+Arguments ret {M _ A} _.
+Arguments bind {M _ A B} _ _.
+
+Instance Monad_Sigma : Monad LSigma := {
+  ret := fun A x => SigRet [x] ;
+  bind := fun A B (ls:LSigma A) (f:A -> LSigma B)  =>
+    match ls with
+    | SigRet l => SigRet(concat (map (fun x => match f x with SigRet y => y end) l))
+    end
+}.
+
 
-Definition flat_pat : Type := list term.
+Definition consM (x : term) (xs : LSigma term) : LSigma term :=
+  match xs with | SigRet lxs => SigRet (x::lxs) end.
+
+
+  (* \sigma w (w1 + ... + wm)*  *)
+Definition flat_pat : Type := LSigma term.
 Definition deflatten (fp : flat_pat) : pat. Admitted. 
 
+
 Fixpoint star_a_pattern (lt:list term) : flat_pat := 
   match lt with
-  | [] => []
-  (* | Term [] [] :: q => star_a_pattern q *)
+  | [] => SigRet []
   | Term s [] :: q => 
     let std_s := sort relSort s in 
-    Term [] [std_s] :: star_a_pattern q
-  (* | Term [] ls :: q => ls ++ star_a_pattern q *)
+    consM (Term [] [std_s]) (star_a_pattern q)
   | Term s ls :: q => 
     let std_s := sort relSort s in 
     let std_ls := map (fun sl => sort relSort sl) ls in 
-    Term [] [std_s] :: 
-      Term std_s (std_s::std_ls) :: star_a_pattern q
+    consM (Term [] [std_s])  
+      (consM (Term std_s (std_s::std_ls)) 
+        (star_a_pattern q))
   end.
 
 
 Fixpoint and_two_pattern (lt1:list term) (lt2:list term) : flat_pat := 
   match lt2 with
-  | [] => []
-  (* | Term [] [] :: q => star_a_pattern q *)
-  (* | Term s [] :: q => Term [] [s] :: star_a_pattern q *)
-  (* | Term [] ls :: q => ls ++ star_a_pattern q *)
+  | [] => SigRet []
   | Term s2 ls2 :: q => 
-    map (fun x => 
+    match and_two_pattern lt1 q with 
+    | SigRet q1 =>
+      SigRet (map (fun x => 
         match x with 
         | Term s1 ls1 => 
           let std_s1s2 := sort relSort (s1++s2) in 
@@ -132,15 +162,18 @@ Fixpoint and_two_pattern (lt1:list term) (lt2:list term) : flat_pat :=
             Term (std_s1s2) (std_ls1ls2) 
         end) 
         lt1 
-      ++ and_two_pattern lt1 q
+        ++ q1)
+    end
   end.
 
 (* Search foo. *)
 Fixpoint flatten (pattern:pat) : flat_pat :=
   match pattern with
+  | void_pat => SigRet [] 
+  | eps_pat => SigRet [] 
   | and_pat p p' => 
-  let fp := flatten p in 
-  let fp' := flatten p' in 
+  let fp := match flatten p with | SigRet fp => fp end in 
+  let fp' := match flatten p' with | SigRet fp' => fp' end in 
   and_two_pattern fp fp'
   (*fold_left (fun qt h => match  h with 
   | None => (map (fun f => add_l_opt f ((map (fun x => optpart x) fp'))) fp) ++ qt 
@@ -148,9 +181,14 @@ Fixpoint flatten (pattern:pat) : flat_pat :=
 (* [Build_foo (Some (fold_left (fun qt h => match fixedpart h with 
   | None => qt
   | Some h' => and_pat qt (fixedpart h') end) (fp ++ fp') None)) ((optpart fp) ++ optpart fp'))] *) (* and_pat (flatten p) (flatten p') *)
-  | or_pat p p' => flatten p ++ flatten p' (*retrouve les mêmes éléments dans flatten p et flatten p' *)
-  | star_pat p => star_a_pattern (flatten p)
-  | baseS_pat s => [Term [s] []]
+  | or_pat p p' => 
+    let fp := match flatten p with | SigRet fp => fp end in 
+    let fp' := match flatten p' with | SigRet fp' => fp' end in 
+    SigRet (fp ++ fp') (*retrouve les mêmes éléments dans flatten p et flatten p' *)
+  | star_pat p => 
+    let fp := match flatten p with | SigRet fp => fp end in 
+    star_a_pattern (fp)
+  | baseS_pat s => ret (Term [s] [])
   end.
 
 (*flatten p est sorted*)
@@ -174,7 +212,7 @@ Compute (flatten mypattern). *)
 
 (*missing the LinkGraph aspect*)
 Inductive constructor : Type :=
-  | ctrl_name (c:Kappa)
+  (* | ctrl_name (c:Kappa) I'm pretty sure this is no longer needed from the void_pat *)
   | patterns (c: Kappa) (p:pat).
 
 Inductive formation_rule : Type := 
@@ -202,12 +240,6 @@ Fixpoint check_nodes_of_sort_s {s i r o} {b:bigraph s i r o} (s: mysort) (l: lis
 
 
 
-Lemma lt_inter_lemma lp lqp : (lp < lp + lqp.+1)%coq_nat.
-Proof.
-  apply PeanoNat.Nat.lt_add_pos_r.
-  apply PeanoNat.Nat.lt_0_succ.
-Qed.
-
 
 Fixpoint derive_no_fixed_part (s:mysort) (l:list (list mysort)) 
     : list term := 
@@ -297,7 +329,7 @@ Lemma check_pattern_term_faster_eq_check_pattern_term (p:term) (l:list mysort) :
     ++ rewrite (Bool.orb_true_r (check_pattern_term te l)).
     rewrite (Bool.orb_true_r).
     reflexivity.
-    ++ Search (orb _ false).
+    ++ 
     rewrite (Bool.orb_false_r).
     rewrite (Bool.orb_false_r).
     Abort.
@@ -319,9 +351,10 @@ Lemma check_pattern_term_faster_eq_check_pattern_term (p:term) (l:list mysort) :
     else false  *)
 
 Definition check_pattern (fp:flat_pat) (l:list mysort)  : bool := 
+  let fpl := match fp with | SigRet fp => fp end in   
   fold_left 
     (fun qt p => orb (check_pattern_term p l) qt)
-    fp 
+    fpl 
     false.
   (* match fp with 
   | [] => false
@@ -348,11 +381,11 @@ Fixpoint get_children_sorts_list {s i r o} {b:bigraph s i r o} (l:list (get_node
 Definition check_constructor {s i r o}
   (b:bigraph s i r o) (s:mysort) (c:constructor) : bool :=
   match c with
-  | ctrl_name k =>
+  (* | ctrl_name k =>
     fold_left 
       (fun qt nh => (negb (not_is_atomic (b:=b) nh)) && qt)
       (get_nodes_control_k b k) 
-      true
+      true *)
   | patterns k p => 
     let llschildren := get_children_sorts_list (get_nodes_control_k b k) in
     fold_left