Reindented.

[helm.git] / helm / software / components / cic_disambiguation / disambiguate.ml

diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml
index 6dd82cc288c42731702bd8b94220d31b5502e8a9..dbdb1530f8bd46c6f000b707df82652391633832 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 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 _ ->


@@ -246,8 +247,16 @@ 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!")))
         in
         let branches =
                 raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
         in
         let branches =

+         if create_dummy_ids then
+          List.map
+           (function
+               Ast.Wildcard,term -> ("wildcard",None,[]), term
+             | Ast.Pattern _,_ ->
+                raise (Invalid_choice (Some loc, lazy "Syntax error: the left hand side of a branch patterns must be \"_\""))
+           ) branches
+         else

          match fst(CicEnvironment.get_obj CicUniv.empty_ugraph indtype_uri) with
          match fst(CicEnvironment.get_obj CicUniv.empty_ugraph indtype_uri) with

-            Cic.InductiveDefinition (il,_,_,_) ->
+            Cic.InductiveDefinition (il,_,leftsno,_) ->

              let _,_,_,cl =
               try
                List.nth il indtype_no
              let _,_,_,cl =
               try
                List.nth il indtype_no


@@ -261,14 +270,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 +302,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 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 +725,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