* implemented unless

diff --git a/helm/ocaml/cic_notation/cicNotationFwd.ml b/helm/ocaml/cic_notation/cicNotationFwd.ml
index 10bab9e36fb3bcaedd333aec34ec64610077164d..f2e2c7164efa6244d045a073eb1331f13877a8ba 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationFwd.ml
+++ b/helm/ocaml/cic_notation/cicNotationFwd.ml
@@ -242,6 +242,8 @@ let instantiate_level2 env term =
               | _ -> assert false
             in
             instantiate_fold_right env)
+    | If (_, body)
+    | Unless (_, body) -> aux env body
     | _ -> assert false
   in
   aux env term

diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml
index 1a0c024104feaaab9f730ed16c5101c3f72ce965..39c82b7dadb66a1e095969c133ff2d9ab23d5078 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationMatcher.ml
+++ b/helm/ocaml/cic_notation/cicNotationMatcher.ml
@@ -277,7 +277,7 @@ struct
                let env' = Env.remove_names env (List.map fst magic_map) in
                Some (env', pid)))
         (fun _ -> None)
-        candidates
+        (List.rev candidates)
     in
     let match_cb rows =
       let candidates =
@@ -335,12 +335,9 @@ struct
           | _ -> assert false)
 
     | Pt.If (guard, p) ->
-       prerr_endline ("guard = " ^ CicNotationPp.pp_term guard) ;
-       prerr_endline ("p = " ^ CicNotationPp.pp_term p) ;
        let compiled_guard = compiler [guard, 0]
        and compiled_p = compiler [p, 0] in
          (fun term env ->
-            prerr_endline "GUARDIA?" ;
             match compiled_guard term with
               | None -> None
               | Some _ ->
@@ -348,10 +345,23 @@ struct
                     match compiled_p term with
                       | None -> None
                       | Some (env', _) ->
-                          prerr_endline "guardia ok" ;
                           Some (env' @ env)
                   end)
 
+    | Pt.Unless (guard, p) ->
+       let compiled_guard = compiler [guard, 0]
+       and compiled_p = compiler [p, 0] in
+         (fun term env ->
+            match compiled_guard term with
+              | None ->
+                  begin
+                    match compiled_p term with
+                      | None -> None
+                      | Some (env', _) ->
+                          Some (env' @ env)
+                  end
+              | Some _ -> None)
+
     | _ -> assert false
 end
 

diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml
index 3622a8c921edf290ddd3d47051b08c89a73ce87a..f3a6035d4c5d87918d63f3fe78cc1385434c27d6 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationParser.ml
+++ b/helm/ocaml/cic_notation/cicNotationParser.ml
@@ -478,6 +478,10 @@ EXTEND
       DELIM "\\["; guard = l2_pattern; DELIM "\\]";
       DELIM "\\["; p = l2_pattern; DELIM "\\]" ->
         If (guard, p)    
+    | SYMBOL "\\UNLESS";
+      DELIM "\\["; guard = l2_pattern; DELIM "\\]";
+      DELIM "\\["; p = l2_pattern; DELIM "\\]" ->
+        Unless (guard, p)        
     ]
   ];
   l2_pattern: LEVEL "10"  (* let in *)

diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml
index 696580cdc5442c97555cb9bea3cf64e5b0eb131b..c3185d6a251ba1ee2b63a1d8a4e63d80ebdfb453 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationPp.ml
+++ b/helm/ocaml/cic_notation/cicNotationPp.ml
@@ -158,6 +158,8 @@ and pp_magic = function
       sprintf "\\DEFAULT \\[%s\\] \\[%s\\]" (pp_term p_some) (pp_term p_none)
   | If (p_guard, p) ->
       sprintf "\\IF \\[%s\\] \\[%s\\]" (pp_term p_guard) (pp_term p)
+  | Unless (p_guard, p) ->
+      sprintf "\\UNLESS \\[%s\\] \\[%s\\]" (pp_term p_guard) (pp_term p)
 
 and pp_fold_kind = function
   | `Left -> "left"

diff --git a/helm/ocaml/cic_notation/cicNotationPt.ml b/helm/ocaml/cic_notation/cicNotationPt.ml
index 0a5a1285331c9210d9e99bcb53018e7c0d7ec9b2..56bf8547441bd218ee6fd393569902c558942cfe 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationPt.ml
+++ b/helm/ocaml/cic_notation/cicNotationPt.ml
@@ -117,7 +117,8 @@ and magic_term =
   | Fold of fold_kind * term * string list * term
     (* base case pattern, recursive case bound names, recursive case pattern *)
   | Default of term * term  (* "some" case pattern, "none" case pattern *)
-  | If of term * term (* guard, pattern *)
+  | If of term * term (* guard, body *)
+  | Unless of term * term (* guard, body *)
 
 and pattern_variable =
   (* level 1 and 2 variables *)

diff --git a/helm/ocaml/cic_notation/cicNotationUtil.ml b/helm/ocaml/cic_notation/cicNotationUtil.ml
index 740a9c1464af06c1a335c55a03ed09c7df9555cc..f10efa7545d82ff152d40af057fd4c188533b9e6 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationUtil.ml
+++ b/helm/ocaml/cic_notation/cicNotationUtil.ml
@@ -171,6 +171,7 @@ let visit_magic k = function
   | Fold (kind, t1, names, t2) -> Fold (kind, k t1, names, k t2)
   | Default (t1, t2) -> Default (k t1, k t2)
   | If (t1, t2) -> If (k t1, k t2)
+  | Unless (t1, t2) -> Unless (k t1, k t2)
 
 let variables_of_term t =
   let rec vars = ref [] in