one more lazy/loc

diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml
index 9d42899c6895fffeeb3366f210c7dd6a3fbbe2f4..47e9c182189efb83e9b8be3518ed448dff80553f 100644 (file)
--- a/helm/software/components/cic_disambiguation/disambiguate.ml
+++ b/helm/software/components/cic_disambiguation/disambiguate.ml
@@ -232,13 +232,13 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
                  raise (Try_again (lazy "The type of the term to be matched
                   is still unknown"))
               | _ ->
-                raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
+                raise (Invalid_choice (lazy (loc,"The type of the term to be matched is not (co)inductive!"))))
           | None ->
               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"))
+                 | [] -> raise (Invalid_choice (lazy (loc,"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 branches)) () with
               | Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
@@ -247,7 +247,7 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
                  raise (Try_again (lazy "The type of the term to be matched
                   is still unknown"))
               | _ ->
-                raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
+                raise (Invalid_choice (lazy (loc,"The type of the term to be matched is not (co)inductive!"))))
         in
         let branches =
          if create_dummy_ids then
@@ -255,7 +255,7 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
            (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 \"_\""))
+                raise (Invalid_choice (lazy (loc, "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
@@ -278,17 +278,15 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
                        [] ->
                         if unrecognized != [] then
                          raise (Invalid_choice
-                          (Some loc,
-                           lazy
+                          (lazy (loc,
                             ("Unrecognized constructors: " ^
-                             String.concat " " unrecognized)))
+                             String.concat " " unrecognized))))
                         else if useless > 0 then
                          raise (Invalid_choice
-                          (Some loc,
-                           lazy
+                           (lazy (loc,
                             ("The last " ^ string_of_int useless ^
                              "case" ^ if useless > 1 then "s are" else " is" ^
-                             " unused")))
+                             " unused"))))
                         else
                          []
                      | (Ast.Wildcard,_)::tl when not unused ->
@@ -304,7 +302,7 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
                        [] ->
                         raise
                          (Invalid_choice
-                          (Some loc, lazy ("Missing case: " ^ name)))
+                          (lazy (loc, ("Missing case: " ^ name))))
                      | ((Ast.Wildcard, _) as branch :: _) as branches ->
                          branch, branches
                      | (Ast.Pattern (name',_,_),_) as branch :: tl
@@ -322,8 +320,8 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
                         else
                          raise
                           (Invalid_choice
-                           (Some loc,
-                             lazy ("Wrong number of arguments for " ^ name)))
+                            (lazy (loc,"Wrong number of arguments for " ^
+                            name)))
                      | Ast.Wildcard,term ->
                         let rec mk_lambdas =
                          function
@@ -482,7 +480,7 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
                     (try
                       List.assoc s ids_to_uris, aux ~localize loc context term
                      with Not_found ->
-                       raise (Invalid_choice (Some loc, lazy "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on"))))
+                       raise (Invalid_choice (lazy (loc, "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on")))))
                   subst
             | None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
           in
@@ -526,10 +524,10 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
 *)
                 t
             | _ ->
-              raise (Invalid_choice (Some loc, lazy "??? Can this happen?"))
+              raise (Invalid_choice (lazy (loc, "??? Can this happen?")))
            with 
              CicEnvironment.CircularDependency _ -> 
-               raise (Invalid_choice (None, lazy "Circular dependency in the environment"))))
+               raise (Invalid_choice (lazy (loc,"Circular dependency in the environment")))))
     | CicNotationPt.Implicit -> Cic.Implicit None
     | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
     | CicNotationPt.Num (num, i) -> resolve env (Num i) ~num ()
@@ -1147,8 +1145,7 @@ let foo () =
 in refine_profiler.HExtlib.profile foo ()
         with
         | Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg))
-        | Invalid_choice (None,msg) -> Ko(lazy (Stdpp.dummy_loc,Lazy.force msg))
-        | Invalid_choice (Some loc,msg) -> Ko (lazy (loc,Lazy.force msg))
+        | Invalid_choice loc_msg -> Ko loc_msg
       in
       (* (4) build all possible interpretations *)
       let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in

diff --git a/helm/software/components/cic_disambiguation/disambiguateChoices.ml b/helm/software/components/cic_disambiguation/disambiguateChoices.ml
index c3fa7efb2805cf953cf9cee4545f69c416984ca5..bf14623d7a6943e28839b6d5379237c960594230 100644 (file)
--- a/helm/software/components/cic_disambiguation/disambiguateChoices.ml
+++ b/helm/software/components/cic_disambiguation/disambiguateChoices.ml
@@ -62,7 +62,8 @@ let mk_choice (dsc, args, appl_pattern) =
         try
          combine_with_rest names cic_args
         with Invalid_argument _ ->
-         raise (Invalid_choice (None, lazy ("The notation " ^ dsc ^ " expects more arguments")))
+         raise (Invalid_choice (lazy (Stdpp.dummy_loc, 
+           "The notation " ^ dsc ^ " expects more arguments")))
     in
      let combined =
       TermAcicContent.instantiate_appl_pattern env' appl_pattern

diff --git a/helm/software/components/cic_disambiguation/disambiguateTypes.ml b/helm/software/components/cic_disambiguation/disambiguateTypes.ml
index 1eade4ca09850d1b6d6636d5b3bb8e203142e5ee..e9927c7b6cd9796d16bdaca975762194ec9c274e 100644 (file)
--- a/helm/software/components/cic_disambiguation/disambiguateTypes.ml
+++ b/helm/software/components/cic_disambiguation/disambiguateTypes.ml
@@ -40,7 +40,7 @@ type domain_item =
   | Symbol of string * int     (* literal, instance num *)
   | Num of int                 (* instance num *)
 
-exception Invalid_choice of Stdpp.location option * string Lazy.t
+exception Invalid_choice of (Stdpp.location * string) Lazy.t
 
 module OrderedDomain =
   struct

diff --git a/helm/software/components/cic_disambiguation/disambiguateTypes.mli b/helm/software/components/cic_disambiguation/disambiguateTypes.mli
index 00fe4114cdcde61ca5e5bde2e299bcda3c846985..d9cedf5f007faf2d4b9fae997eaa793ee550ea63 100644 (file)
--- a/helm/software/components/cic_disambiguation/disambiguateTypes.mli
+++ b/helm/software/components/cic_disambiguation/disambiguateTypes.mli
@@ -41,7 +41,7 @@ end
 
   (** to be raised when a choice is invalid due to some given parameter (e.g.
    * wrong number of Cic.term arguments received) *)
-exception Invalid_choice of Stdpp.location option * string Lazy.t
+exception Invalid_choice of (Stdpp.location * string) Lazy.t
 
 type codomain_item =
   string *  (* description *)

diff --git a/helm/software/components/cic_disambiguation/number_notation.ml b/helm/software/components/cic_disambiguation/number_notation.ml
index 9dece04ecda69100013d0f04c265b5b93ef8c7bf..37547bf581b97b6512d2a23e5e765cad061b62c6 100644 (file)
--- a/helm/software/components/cic_disambiguation/number_notation.ml
+++ b/helm/software/components/cic_disambiguation/number_notation.ml
@@ -40,7 +40,7 @@ let _ =
       (fun _ num _ ->
         let num = int_of_string num in
         if num = 0 then
-          raise (DisambiguateTypes.Invalid_choice (None, lazy "0 is not a valid positive number"))
+          raise (DisambiguateTypes.Invalid_choice (lazy (Stdpp.dummy_loc, "0 is not a valid positive number")))
         else
           HelmLibraryObjects.build_bin_pos num));
   DisambiguateChoices.add_num_choice

diff --git a/helm/software/components/ng_disambiguation/nDisambiguate.ml b/helm/software/components/ng_disambiguation/nDisambiguate.ml
index 2aa87372467b49568f41f1f192f922b526f5b552..d350a7f23c263b0dfa158b86511986b0317279d7 100644 (file)
--- a/helm/software/components/ng_disambiguation/nDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nDisambiguate.ml
@@ -34,6 +34,11 @@ module Ast = CicNotationPt
 
 let debug_print _ = ();;
 
+let cic_name_of_name = function
+  | Ast.Ident (n, None) ->  n
+  | _ -> assert false
+;;
+
 let refine_term metasenv subst context uri term _ ~localization_tbl =
   assert (uri=None);
   debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" 
@@ -48,22 +53,25 @@ let refine_term metasenv subst context uri term _ ~localization_tbl =
     in
      Disambiguate.Ok (term, metasenv, subst, ())
   with
-  | NCicRefiner.Uncertain (msg) ->
-      debug_print (lazy ("UNCERTAIN: [" ^ snd (Lazy.force msg) ^ "] " ^ 
+  | NCicRefiner.Uncertain loc_msg ->
+      debug_print (lazy ("UNCERTAIN: [" ^ snd (Lazy.force loc_msg) ^ "] " ^ 
         NCicPp.ppterm ~metasenv ~subst ~context term)) ;
-      Disambiguate.Uncertain (loc,msg)
-  | NCicRefiner.RefineFailure (msg) ->
+      Disambiguate.Uncertain loc_msg
+  | NCicRefiner.RefineFailure loc_msg ->
       debug_print (lazy (sprintf "PRUNED:\nterm%s\nmessage:%s"
-        (NCicPp.ppterm ~metasenv ~subst ~context term) (snd(Lazy.force msg))));
-      Disambiguate.Ko (loc,msg,())
+        (NCicPp.ppterm ~metasenv ~subst ~context term) (snd(Lazy.force loc_msg))));
+      Disambiguate.Ko loc_msg
 ;;
 
 let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () =
+        assert false;;
+(*
   try
     snd (Environment.find item env) env num args
   with Not_found -> 
     failwith ("Domain item not found: " ^ 
       (DisambiguateTypes.string_of_domain_item item))
+*)
 
   (* TODO move it to Cic *)
 let find_in_context name context =
@@ -83,7 +91,7 @@ let interpretate_term
   let rec aux ~localize loc context = function
     | CicNotationPt.AttributedTerm (`Loc loc, term) ->
         let res = aux ~localize loc context term in
-         if localize then NCic.NCicHash.add localization_tbl res loc;
+         if localize then NCicUntrusted.NCicHash.add localization_tbl res loc;
          res
     | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term
     | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) ->
@@ -93,7 +101,7 @@ let interpretate_term
        NCic.Appl (List.map (aux ~localize loc context) terms)
     | CicNotationPt.Binder (binder_kind, (var, typ), body) ->
         let cic_type = aux_option ~localize loc context (Some `Type) typ in
-        let cic_name = CicNotationUtil.cic_name_of_name var in
+        let cic_name = cic_name_of_name var  in
         let cic_body = aux ~localize loc (cic_name :: context) body in
         (match binder_kind with
         | `Lambda -> NCic.Lambda (cic_name, cic_type, cic_body)
@@ -109,11 +117,11 @@ let interpretate_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_name = cic_name_of_name name in
                let cic_body = do_branch' (cic_name :: context) tl in
                let typ =
                  match typ with
-                 | None -> NCic.Implicit (Some `Type)
+                 | None -> NCic.Implicit `Type
                  | Some typ -> aux ~localize loc context typ
                in
                NCic.Lambda (cic_name, typ, cic_body)
@@ -127,12 +135,14 @@ let interpretate_term
           match indty_ident with
           | Some (indty_ident, _) ->
              (match resolve env (Id indty_ident) () with
-              | NCic.MutInd (uri, tyno, _) -> (uri, tyno)
+              | NCic.Const (NRef.Ref (uri, NRef.Ind  (_, tyno))) -> (uri, tyno)
               | NCic.Implicit _ ->
-                 raise (Disambiguate.Try_again (lazy "The type of the term to be matched
-                  is still unknown"))
+                 raise (Disambiguate.Try_again 
+                  (lazy "The type of the term to be matched is still unknown"))
               | _ ->
-                raise (DisambiguateTypes.Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
+                raise (DisambiguateTypes.Invalid_choice 
+                  (Some loc, 
+                    lazy "The type of the term to be matched is not (co)inductive!")))
           | None ->
               let rec fst_constructor =
                 function
@@ -247,7 +257,7 @@ let interpretate_term
         NCic.Cast (cic_t1, cic_t2)
     | 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_name = cic_name_of_name name in
         let cic_typ =
           match typ with
           | None -> NCic.Implicit (Some `Type)
@@ -259,7 +269,7 @@ let interpretate_term
         let context' =
           List.fold_left
             (fun acc (_, (name, _), _, _) ->
-              CicNotationUtil.cic_name_of_name name :: acc)
+              cic_name_of_name name :: acc)
             context defs
         in
         let cic_body =
@@ -315,7 +325,7 @@ let interpretate_term
                aux_option ~localize loc context (Some `Type)
                 (HExtlib.map_option (add_binders `Pi) typ) in
               let name =
-                match CicNotationUtil.cic_name_of_name name with
+                match cic_name_of_name name with
                 | NCic.Anonymous ->
                     CicNotationPt.fail loc
                       "Recursive functions cannot be anonymous"