oblivion ugraph everywhere outside the kernel

[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..ad8028d165a73f4ba5e6923a27cc8daf8cc6e8f1 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 =

-         match fst(CicEnvironment.get_obj CicUniv.empty_ugraph indtype_uri) with
-            Cic.InductiveDefinition (il,_,_,_) ->
+         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.oblivion_ugraph indtype_uri) with
+            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


@@ -304,13 +345,13 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
     | CicNotationPt.LetIn ((name, typ), def, body) ->
         let cic_def = aux ~localize loc context def in
         let cic_name = CicNotationUtil.cic_name_of_name name in
     | CicNotationPt.LetIn ((name, typ), def, body) ->
         let cic_def = aux ~localize loc context def in
         let cic_name = CicNotationUtil.cic_name_of_name name in

-        let cic_def =
+        let cic_typ =

           match typ with
           match typ with

-          | None -> cic_def
-          | Some t -> Cic.Cast (cic_def, aux ~localize loc context t)
+          | None -> Cic.Implicit (Some `Type)
+          | Some t -> aux ~localize loc context t

         in
         let cic_body = aux ~localize loc (cic_name :: context) body in
         in
         let cic_body = aux ~localize loc (cic_name :: context) body in

-        Cic.LetIn (cic_name, cic_def, cic_body)
+        Cic.LetIn (cic_name, cic_def, cic_typ, cic_body)

     | CicNotationPt.LetRec (kind, defs, body) ->
         let context' =
           List.fold_left
     | CicNotationPt.LetRec (kind, defs, body) ->
         let context' =
           List.fold_left


@@ -390,9 +431,9 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
                Cic.CoFix (n,coinductiveFuns)
         in
          let counter = ref ~-1 in
                Cic.CoFix (n,coinductiveFuns)
         in
          let counter = ref ~-1 in

-         let build_term funs (var,_,_,_) t =
+         let build_term funs (var,_,ty,_) t =

           incr counter;
           incr counter;

-          Cic.LetIn (Cic.Name var, fix_or_cofix !counter, t)
+          Cic.LetIn (Cic.Name var, fix_or_cofix !counter, ty, t)

          in
           (match cic_body with
               `AvoidLetInNoAppl n ->
          in
           (match cic_body with
               `AvoidLetInNoAppl n ->


@@ -443,16 +484,16 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
           (try 
             match cic with
             | Cic.Const (uri, []) ->
           (try 
             match cic with
             | Cic.Const (uri, []) ->

-                let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+                let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in

                 let uris = CicUtil.params_of_obj o in
                 Cic.Const (uri, mk_subst uris)
             | Cic.Var (uri, []) ->
                 let uris = CicUtil.params_of_obj o in
                 Cic.Const (uri, mk_subst uris)
             | Cic.Var (uri, []) ->

-                let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+                let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in

                 let uris = CicUtil.params_of_obj o in
                 Cic.Var (uri, mk_subst uris)
             | Cic.MutInd (uri, i, []) ->
                (try
                 let uris = CicUtil.params_of_obj o in
                 Cic.Var (uri, mk_subst uris)
             | Cic.MutInd (uri, i, []) ->
                (try

-                 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+                 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in

                  let uris = CicUtil.params_of_obj o in
                  Cic.MutInd (uri, i, mk_subst uris)
                 with
                  let uris = CicUtil.params_of_obj o in
                  Cic.MutInd (uri, i, mk_subst uris)
                 with


@@ -465,7 +506,7 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
                   (*here the explicit_named_substituion is assumed to be of length 0 *)
                   Cic.MutInd (uri,i,[]))
             | Cic.MutConstruct (uri, i, j, []) ->
                   (*here the explicit_named_substituion is assumed to be of length 0 *)
                   Cic.MutInd (uri,i,[]))
             | Cic.MutConstruct (uri, i, j, []) ->

-                let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+                let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in

                 let uris = CicUtil.params_of_obj o in
                 Cic.MutConstruct (uri, i, j, mk_subst uris)
             | Cic.Meta _ | Cic.Implicit _ as t ->
                 let uris = CicUtil.params_of_obj o in
                 Cic.MutConstruct (uri, i, j, mk_subst uris)
             | Cic.Meta _ | Cic.Implicit _ as t ->


@@ -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


@@ -930,7 +976,7 @@ module Make (C: Callbacks) =
 let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
 
     let disambiguate_thing ~dbd ~context ~metasenv
 let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
 
     let disambiguate_thing ~dbd ~context ~metasenv

-      ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe
+      ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe

       ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing 
       (thing_txt,thing_txt_prefix_len,thing)
     =
       ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing 
       (thing_txt,thing_txt_prefix_len,thing)
     =


@@ -1230,7 +1276,7 @@ in refine_profiler.HExtlib.profile foo ()
         failwith "Disambiguate: circular dependency"
 
     let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
         failwith "Disambiguate: circular dependency"
 
     let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv

-      ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe 
+      ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe 

       (text,prefix_len,term)
     =
       let term =
       (text,prefix_len,term)
     =
       let term =