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

accepted:

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

diff --git a/components/acic_content/cicNotationPp.ml b/components/acic_content/cicNotationPp.ml
index 2873912c0129d51b9b17e9a6f2f3aae80c144797..4bd2f93ed2c633a8e0bb902d83e9bf50189301d6 100644 (file)
--- a/components/acic_content/cicNotationPp.ml
+++ b/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_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))
 
 and pp_patterns patterns =
   sprintf "[%s]" (String.concat " | " (List.map pp_pattern patterns))

diff --git a/components/acic_content/cicNotationPt.ml b/components/acic_content/cicNotationPt.ml
index 27ec5734f1a9065aa9762feac57aa20cd31b8771..d9d92ad6fc5b905cbb9ba0600c441fc95a4d7bf3 100644 (file)
--- a/components/acic_content/cicNotationPt.ml
+++ b/components/acic_content/cicNotationPt.ml
@@ -105,7 +105,9 @@ type term =
 
 and meta_subst = term option
 and subst = string * 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 *)
 
 and box_kind = H | V | HV | HOV
 and box_spec = box_kind * bool * bool (* kind, spacing, indent *)

diff --git a/components/acic_content/cicNotationUtil.ml b/components/acic_content/cicNotationUtil.ml
index f331b79ca8d2da4c3a545c54b6789dcb1eb59a7b..99aafa44051765813c6f198ad71cd7945a626cbc 100644 (file)
--- a/components/acic_content/cicNotationUtil.ml
+++ b/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
     | 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
   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_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 ;
   and aux_definition (params, var, term, decrno) =
     List.iter aux_capture_var params ;
     aux_capture_var var ;

diff --git a/components/acic_content/termAcicContent.ml b/components/acic_content/termAcicContent.ml
index 9a30b50fb6ef1b2618171c38f74ebc490e52e1da..257d2440ba87b66c93e6863f660e715318bb0d35 100644 (file)
--- a/components/acic_content/termAcicContent.ml
+++ b/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
               (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))
           with Invalid_argument _ -> assert false
         in
         idref id (Ast.Case (k te, Some case_indty, Some (k ty), patterns))

diff --git a/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml
index 3d671cd7fd62b5b4fa800559dd80fb79b34a2939..1fea419215f3a0fddf12441585bc753fab6b8794 100644 (file)
--- a/components/cic_disambiguation/disambiguate.ml
+++ b/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 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 =
           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 ->
               | _ ->
                 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
               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 _ ->
               | 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
                   [] ->
               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
                 | (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)))
                         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
                      | 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
               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
   | 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
       in
       let branches_dom =
         List.fold_left (fun dom branch -> dom @ do_branch branch) [] branches in

diff --git a/components/content_pres/cicNotationParser.ml b/components/content_pres/cicNotationParser.ml
index 05075f0c3f2f9d8981747e913212fd3dcbcdd8e4..461e2fc9f755e9b0f868188ac4b535accd4b996d 100644 (file)
--- a/components/content_pres/cicNotationParser.ml
+++ b/components/content_pres/cicNotationParser.ml
@@ -457,10 +457,12 @@ EXTEND
     ]
   ];
   match_pattern: [
     ]
   ];
   match_pattern: [

-    [ id = IDENT -> id, None, []
+    [ id = IDENT -> Ast.Pattern (id, None, [])

     | LPAREN; id = IDENT; vars = LIST1 possibly_typed_name; RPAREN ->
     | 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: [
     ]
   ];
   binder: [

diff --git a/components/content_pres/termContentPres.ml b/components/content_pres/termContentPres.ml
index 110c78e46e43820fc4ae280e80090f9b35c40544..0ee424f18570d318b74d942d936573029d206eed 100644 (file)
--- a/components/content_pres/termContentPres.ml
+++ b/components/content_pres/termContentPres.ml
@@ -151,8 +151,11 @@ let pp_ast0 t k =
            space
          ]
         in
            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
         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_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 =
   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 =