From: Luca Padovani <luca.padovani@unito.it>
Date: Mon, 11 Jul 2005 14:53:23 +0000 (+0000)
Subject: * implemented unless
X-Git-Tag: pre_notation~37
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=26cce624c98e795521078794c748758798031704;p=helm.git

* implemented unless
---

diff --git a/helm/ocaml/cic_notation/cicNotationFwd.ml b/helm/ocaml/cic_notation/cicNotationFwd.ml
index 10bab9e36..f2e2c7164 100644
--- 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 1a0c02410..39c82b7da 100644
--- 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 3622a8c92..f3a6035d4 100644
--- 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 696580cdc..c3185d6a2 100644
--- 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 0a5a12853..56bf85474 100644
--- 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 740a9c146..f10efa754 100644
--- 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