Wildcard patterns implemented in case analysis. The following term is now

accepted:

 match n with
  [ A => O
  | B m => m
  | _ => O
  ]

diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml
index 2873912c0129d51b9b17e9a6f2f3aae80c144797..4bd2f93ed2c633a8e0bb902d83e9bf50189301d6 100644 (file)
--- a/helm/software/components/acic_content/cicNotationPp.ml
+++ b/helm/software/components/acic_content/cicNotationPp.ml
@@ -176,20 +176,24 @@ let rec pp_term ?(pp_parens = true) t =
 and pp_subst (name, term) = sprintf "%s \\Assign %s" name (pp_term term)
 and pp_substs substs = String.concat "; " (List.map pp_subst substs)
 
-and pp_pattern ((head, href, vars), term) =
-  let head_pp =
-    head ^
-    (match debug_printing, href with
-    | true, Some uri -> sprintf "(i.e.%s)" (UriManager.string_of_uri uri)
-    | _ -> "")
-  in
-  sprintf "%s \\Rightarrow %s"
-    (match vars with
-    | [] -> head_pp
-    | _ ->
-        sprintf "(%s %s)" head_pp
-          (String.concat " " (List.map (pp_capture_variable pp_term) vars)))
-    (pp_term term)
+and pp_pattern =
+ function
+    Ast.Pattern (head, href, vars), term ->
+     let head_pp =
+       head ^
+       (match debug_printing, href with
+       | true, Some uri -> sprintf "(i.e.%s)" (UriManager.string_of_uri uri)
+       | _ -> "")
+     in
+     sprintf "%s \\Rightarrow %s"
+       (match vars with
+       | [] -> head_pp
+       | _ ->
+           sprintf "(%s %s)" head_pp
+             (String.concat " " (List.map (pp_capture_variable pp_term) vars)))
+       (pp_term term)
+  | Ast.Wildcard, term ->
+     sprintf "_ \\Rightarrow %s" (pp_term term)
 
 and pp_patterns patterns =
   sprintf "[%s]" (String.concat " | " (List.map pp_pattern patterns))

diff --git a/helm/software/components/acic_content/cicNotationPt.ml b/helm/software/components/acic_content/cicNotationPt.ml
index 27ec5734f1a9065aa9762feac57aa20cd31b8771..d9d92ad6fc5b905cbb9ba0600c441fc95a4d7bf3 100644 (file)
--- a/helm/software/components/acic_content/cicNotationPt.ml
+++ b/helm/software/components/acic_content/cicNotationPt.ml
@@ -105,7 +105,9 @@ type term =
 
 and meta_subst = term option
 and subst = string * term
-and case_pattern = string * href option * term capture_variable list
+and case_pattern =
+   Pattern of string * href option * term capture_variable list
+ | Wildcard
 
 and box_kind = H | V | HV | HOV
 and box_spec = box_kind * bool * bool (* kind, spacing, indent *)

diff --git a/helm/software/components/acic_content/cicNotationUtil.ml b/helm/software/components/acic_content/cicNotationUtil.ml
index f331b79ca8d2da4c3a545c54b6789dcb1eb59a7b..99aafa44051765813c6f198ad71cd7945a626cbc 100644 (file)
--- a/helm/software/components/acic_content/cicNotationUtil.ml
+++ b/helm/software/components/acic_content/cicNotationUtil.ml
@@ -67,8 +67,11 @@ let visit_ast ?(special_k = fun _ -> assert false) k =
     | Some term -> Some (k term)
   and aux_capture_variable (term, typ_opt) = k term, aux_opt typ_opt
   and aux_patterns patterns = List.map aux_pattern patterns
-  and aux_pattern ((head, hrefs, vars), term) =
-    ((head, hrefs, List.map aux_capture_variable vars), k term)
+  and aux_pattern =
+   function
+      Ast.Pattern (head, hrefs, vars), term ->
+        Ast.Pattern (head, hrefs, List.map aux_capture_variable vars), k term
+    | Ast.Wildcard, term -> Ast.Wildcard, k term
   and aux_subst (name, term) = (name, k term)
   and aux_substs substs = List.map aux_subst substs
   in
@@ -213,8 +216,10 @@ let meta_names_of_term term =
   and aux_branch (pattern, term) =
     aux_pattern pattern ;
     aux term
-  and aux_pattern (head, _, vars) = 
-    List.iter aux_capture_var vars
+  and aux_pattern =
+   function
+      Ast.Pattern (head, _, vars) -> List.iter aux_capture_var vars
+    | Ast.Wildcard -> ()
   and aux_definition (params, var, term, decrno) =
     List.iter aux_capture_var params ;
     aux_capture_var var ;

diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml
index 9a30b50fb6ef1b2618171c38f74ebc490e52e1da..257d2440ba87b66c93e6863f660e715318bb0d35 100644 (file)
--- a/helm/software/components/acic_content/termAcicContent.ml
+++ b/helm/software/components/acic_content/termAcicContent.ml
@@ -197,8 +197,8 @@ let ast_of_acic0 term_info acic k =
               (fun (name, ty) pat ->
                 incr j;
                 let (capture_variables, rhs) = eat_branch lpsno ty pat in
-                ((name, Some (ctor_puri !j), capture_variables), rhs))
-              constructors patterns
+                Ast.Pattern (name, Some (ctor_puri !j), capture_variables), rhs
+              ) constructors patterns
           with Invalid_argument _ -> assert false
         in
         idref id (Ast.Case (k te, Some case_indty, Some (k ty), patterns))

diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml
index 3d671cd7fd62b5b4fa800559dd80fb79b34a2939..1fea419215f3a0fddf12441585bc753fab6b8794 100644 (file)
--- a/helm/software/components/cic_disambiguation/disambiguate.ml
+++ b/helm/software/components/cic_disambiguation/disambiguate.ml
@@ -203,18 +203,18 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
         let cic_term = aux ~localize loc context term in
         let cic_outtype = aux_option ~localize loc context None outtype in
         let do_branch ((head, _, args), term) =
-          let rec do_branch' context = function
-            | [] -> aux ~localize loc context term
-            | (name, typ) :: tl ->
-                let cic_name = CicNotationUtil.cic_name_of_name name in
-                let cic_body = do_branch' (cic_name :: context) tl in
-                let typ =
-                  match typ with
-                  | None -> Cic.Implicit (Some `Type)
-                  | Some typ -> aux ~localize loc context typ
-                in
-                Cic.Lambda (cic_name, typ, cic_body)
-          in
+         let rec do_branch' context = function
+           | [] -> aux ~localize loc context term
+           | (name, typ) :: tl ->
+               let cic_name = CicNotationUtil.cic_name_of_name name in
+               let cic_body = do_branch' (cic_name :: context) tl in
+               let typ =
+                 match typ with
+                 | None -> Cic.Implicit (Some `Type)
+                 | Some typ -> aux ~localize loc context typ
+               in
+               Cic.Lambda (cic_name, typ, cic_body)
+         in
           do_branch' context args
         in
         let indtype_uri, indtype_no =
@@ -231,12 +231,13 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
               | _ ->
                 raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
           | None ->
-              let fst_constructor =
-                match branches with
-                | ((head, _, _), _) :: _ -> head
-                | [] -> raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is an inductive type without constructors that cannot be determined"))
+              let rec fst_constructor =
+                function
+                   (Ast.Pattern (head, _, _), _) :: _ -> head
+                 | (Ast.Wildcard, _) :: tl -> fst_constructor tl
+                 | [] -> raise (Invalid_choice (Some loc, lazy "The type of the term to be matched cannot be determined because it is an inductive type without constructors or because all patterns use wildcards"))
               in
-              (match resolve env (Id fst_constructor) () with
+              (match resolve env (Id (fst_constructor branches)) () with
               | Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
                   (indtype_uri, indtype_no)
               | Cic.Implicit _ ->
@@ -261,14 +262,31 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
               let rec sort branches cl =
                match cl with
                   [] ->
-                   if branches = [] then []
-                   else
-                    raise (Invalid_choice
-                     (Some loc,
-                      lazy
-                       ("Unrecognized constructors: " ^
-                        String.concat " "
-                         (List.map (fun ((head,_,_),_) -> head) branches))))
+                   let rec analyze unused unrecognized useless =
+                    function
+                       [] ->
+                        if unrecognized != [] then
+                         raise (Invalid_choice
+                          (Some loc,
+                           lazy
+                            ("Unrecognized constructors: " ^
+                             String.concat " " unrecognized)))
+                        else if useless > 0 then
+                         raise (Invalid_choice
+                          (Some loc,
+                           lazy
+                            ("The last " ^ string_of_int useless ^
+                             "case" ^ if useless > 1 then "s are" else " is" ^
+                             " unused")))
+                        else
+                         []
+                     | (Ast.Wildcard,_)::tl when not unused ->
+                         analyze true unrecognized useless tl
+                     | (Ast.Pattern (head,_,_),_)::tl when not unused ->
+                         analyze unused (head::unrecognized) useless tl
+                     | _::tl -> analyze unused unrecognized (useless + 1) tl
+                   in
+                    analyze false [] 0 branches
                 | (name,ty)::cltl ->
                    let rec find_and_remove =
                     function
@@ -276,21 +294,36 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
                         raise
                          (Invalid_choice
                           (Some loc, lazy ("Missing case: " ^ name)))
-                     | ((name',_,_),_) as branch :: tl when name = name' ->
-                        branch,tl
+                     | ((Ast.Wildcard, _) as branch :: _) as branches ->
+                         branch, branches
+                     | (Ast.Pattern (name',_,_),_) as branch :: tl
+                        when name = name' ->
+                         branch,tl
                      | branch::tl ->
                         let found,rest = find_and_remove tl in
                          found, branch::rest
                    in
                     let branch,tl = find_and_remove branches in
-                    let (_,_,args),_ = branch in
-                     if List.length args = count_prod ty - leftsno then
-                      branch::sort tl cltl
-                     else
-                      raise
-                       (Invalid_choice
-                        (Some loc,
-                          lazy ("Wrong number of arguments for " ^ name)))
+                    match branch with
+                       Ast.Pattern (name,y,args),term ->
+                        if List.length args = count_prod ty - leftsno then
+                         ((name,y,args),term)::sort tl cltl
+                        else
+                         raise
+                          (Invalid_choice
+                           (Some loc,
+                             lazy ("Wrong number of arguments for " ^ name)))
+                     | Ast.Wildcard,term ->
+                        let rec mk_lambdas =
+                         function
+                            0 -> term
+                          | n ->
+                             CicNotationPt.Binder
+                              (`Lambda, (CicNotationPt.Ident ("_", None), None),
+                                mk_lambdas (n - 1))
+                        in
+                         (("wildcard",None,[]),
+                          mk_lambdas (count_prod ty - leftsno)) :: sort tl cltl
               in
                sort branches cl
           | _ -> assert false
@@ -684,20 +717,25 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
   | Ast.Case (term, indty_ident, outtype, branches) ->
       let term_dom = domain_of_term ~loc ~context term in
       let outtype_dom = domain_of_term_option ~loc ~context outtype in
-      let get_first_constructor = function
+      let rec get_first_constructor = function
         | [] -> []
-        | ((head, _, _), _) :: _ -> [ Node ([loc], Id head, []) ] in
-      let do_branch ((head, _, args), term) =
-        let (term_context, args_domain) =
-          List.fold_left
-            (fun (cont, dom) (name, typ) ->
-              (CicNotationUtil.cic_name_of_name name :: cont,
-               (match typ with
-               | None -> dom
-               | Some typ -> dom @ domain_of_term ~loc ~context:cont typ)))
-            (context, []) args
-        in
-        domain_of_term ~loc ~context:term_context term @ args_domain
+        | (Ast.Pattern (head, _, _), _) :: _ -> [ Node ([loc], Id head, []) ]
+        | _ :: tl -> get_first_constructor tl in
+      let do_branch =
+       function
+          Ast.Pattern (head, _, args), term ->
+           let (term_context, args_domain) =
+             List.fold_left
+               (fun (cont, dom) (name, typ) ->
+                 (CicNotationUtil.cic_name_of_name name :: cont,
+                  (match typ with
+                  | None -> dom
+                  | Some typ -> dom @ domain_of_term ~loc ~context:cont typ)))
+               (context, []) args
+           in
+            domain_of_term ~loc ~context:term_context term @ args_domain
+        | Ast.Wildcard, term ->
+            domain_of_term ~loc ~context term
       in
       let branches_dom =
         List.fold_left (fun dom branch -> dom @ do_branch branch) [] branches in

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index 05075f0c3f2f9d8981747e913212fd3dcbcdd8e4..461e2fc9f755e9b0f868188ac4b535accd4b996d 100644 (file)
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -457,10 +457,12 @@ EXTEND
     ]
   ];
   match_pattern: [
-    [ id = IDENT -> id, None, []
+    [ id = IDENT -> Ast.Pattern (id, None, [])
     | LPAREN; id = IDENT; vars = LIST1 possibly_typed_name; RPAREN ->
-        id, None, vars
-    | id = IDENT; vars = LIST1 possibly_typed_name -> id, None, vars
+       Ast.Pattern (id, None, vars)
+    | id = IDENT; vars = LIST1 possibly_typed_name ->
+       Ast.Pattern (id, None, vars)
+    | SYMBOL "_" -> Ast.Wildcard
     ]
   ];
   binder: [

diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml
index 110c78e46e43820fc4ae280e80090f9b35c40544..0ee424f18570d318b74d942d936573029d206eed 100644 (file)
--- a/helm/software/components/content_pres/termContentPres.ml
+++ b/helm/software/components/content_pres/termContentPres.ml
@@ -151,8 +151,11 @@ let pp_ast0 t k =
            space
          ]
         in
-        let mk_case_pattern (head, href, vars) =
-          hbox true false (ident_w_href href head :: List.map aux_var vars)
+        let mk_case_pattern =
+         function
+            Ast.Pattern (head, href, vars) ->
+             hbox true false (ident_w_href href head :: List.map aux_var vars)
+          | Ast.Wildcard -> builtin_symbol "_"
         in
         let patterns' =
           List.map
@@ -575,8 +578,11 @@ let instantiate_level2 env term =
   and aux_capture_var env (name, ty_opt) = (aux env name, aux_opt env ty_opt)
   and aux_branch env (pattern, term) =
     (aux_pattern env pattern, aux env term)
-  and aux_pattern env (head, hrefs, vars) =
-    (head, hrefs, List.map (aux_capture_var env) vars)
+  and aux_pattern env =
+   function
+      Ast.Pattern (head, hrefs, vars) ->
+       Ast.Pattern (head, hrefs, List.map (aux_capture_var env) vars)
+    | Ast.Wildcard -> Ast.Wildcard
   and aux_definition env (params, var, term, i) =
     (List.map (aux_capture_var env) params, aux_capture_var env var, aux env term, i)
   and aux_substs env substs =