Ambiguous parsing improved: refining is now used to prune-out not-well-typed

choices as soon as the term can not be refined. Unfortunately the whole
disambiguation is parsing-bound and not type-checking/refining bound.

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index f81dffc8543df69c1760235f6c12647bf3cb44f7..d1b9b9964e77be4b5f4e8265008a8c912e574454 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -1315,6 +1315,11 @@ let locate_one_id id =
 exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput;;
 exception AmbiguousInput;;
 
+type test_result =
+   Ok of Cic.term * Cic.metasenv
+ | Ko
+ | Uncertain
+
 let disambiguate_input context metasenv dom mk_metasenv_and_expr =
  let known_ids,resolve_id = !id_to_uris in
  let dom' =
@@ -1328,98 +1333,141 @@ let disambiguate_input context metasenv dom mk_metasenv_and_expr =
  in
   (* for each id in dom' we get the list of uris associated to it *)
   let list_of_uris = List.map locate_one_id dom' in
-  (* and now we compute the list of all possible assignments from id to uris *)
+  let tests_no =
+   List.fold_left (fun i uris -> i * List.length uris) 1 list_of_uris
+  in
+   if tests_no > 1 then
+    output_html (outputhtml ())
+     ("<h1>Disambiguation phase started: " ^
+       string_of_int tests_no ^ " cases will be tried.") ;
+  (* and now we compute the list of all possible assignments from *)
+  (* id to uris that generate well-typed terms                    *)
   let resolve_ids =
-   let rec aux ids list_of_uris =
+   (* function to test if a partial interpretation is so far correct *)
+   let test resolve_id residual_dom =
+    (* We put implicits in place of every identifier that is not *)
+    (* resolved by resolve_id                                    *)
+    let resolve_id'' =
+     let resolve_id' =
+      function id ->
+       match resolve_id id with
+          None -> None
+        | Some uri -> Some (CicTextualParser0.Uri uri)
+     in
+      List.fold_left
+       (fun f id ->
+         function id' ->
+          if id = id' then Some (CicTextualParser0.Implicit) else f id'
+       ) resolve_id' residual_dom
+    in
+     (* and we try to refine the term *)
+     let saved_status = !CicTextualParser0.metasenv in
+     let metasenv',expr = mk_metasenv_and_expr resolve_id'' in
+(*CSC: Bug here: we do not try to typecheck also the metasenv' *)
+     (* The parser is imperative ==> we must restore the old status ;-(( *)
+     CicTextualParser0.metasenv := saved_status ;
+      try
+       let term,_,_,metasenv'' =
+        CicRefine.type_of_aux' metasenv' context expr
+       in
+        Ok (term,metasenv'')
+      with
+         CicRefine.MutCaseFixAndCofixRefineNotImplemented ->
+          (try
+            let term = CicTypeChecker.type_of_aux' metasenv' context expr in
+             Ok (term,metasenv')
+           with _ -> Ko
+          )
+       | CicRefine.Uncertain _ ->
+prerr_endline ("%%% UNCERTAIN!!! " ^ CicPp.ppterm expr) ;
+          Uncertain
+       | _ ->
+prerr_endline ("%%% PRUNED!!! " ^ CicPp.ppterm expr) ;
+         Ko
+   in
+   let rec aux resolve_id ids list_of_uris =
     match ids,list_of_uris with
-       [],[] -> [resolve_id]
+       [],[] ->
+        (match test resolve_id [] with
+            Ok (term,metasenv) -> [resolve_id,term,metasenv]
+          | Ko | Uncertain -> [])
      | id::idtl,uris::uristl ->
-        let resolves = aux idtl uristl in
-         List.concat
-          (List.map
-            (function uri ->
-              List.map
-               (function f ->
-                 function id' -> if id = id' then Some uri else f id'
-               ) resolves
-            ) uris
-          )
+        let rec filter =
+         function
+            [] -> []
+          | uri::uritl ->
+             let resolve_id' =
+              function id' -> if id = id' then Some uri else resolve_id id'
+             in
+              (match test resolve_id' idtl with
+                  Ok (term,metasenv) ->
+                   (* the next three ``if''s are used to avoid the base   *)
+                   (* case where the term would be refined a second time. *)
+                   (if uristl = [] then
+                     [resolve_id',term,metasenv]
+                    else
+                     (aux resolve_id' idtl uristl)
+                   ) @ (filter uritl)
+                | Uncertain ->
+                   (if uristl = [] then []
+                    else
+                     (aux resolve_id' idtl uristl)
+                   ) @ (filter uritl)
+                | Ko ->
+                   filter uritl
+              )
+        in
+         filter uris
      | _,_ -> assert false
    in
-    aux dom' list_of_uris
+    aux resolve_id dom' list_of_uris
   in
-   let tests_no = List.length resolve_ids in
-    if tests_no > 1 then
-     output_html (outputhtml ())
-      ("<h1>Disambiguation phase started: " ^
-        string_of_int (List.length resolve_ids) ^ " cases will be tried.") ;
-   (* now we select only the ones that generates well-typed terms *)
-   let resolve_ids' =
-    let rec filter =
-     function
-        [] -> []
-      | resolve::tl ->
-         let metasenv',expr = mk_metasenv_and_expr resolve in
-          try
-(*CSC: Bug here: we do not try to typecheck also the metasenv' *)
-           let term,_,_,metasenv'' =
-            CicRefine.type_of_aux' metasenv' context expr
-           in
-            (* If metasen <> metasenv'' is a normal condition, we should *)
-            (* be prepared to apply the returned substitution to the     *)
-            (* whole current proof.                                      *)
-            if metasenv <> metasenv'' then
-             begin
-              prerr_endline
-               ("+++++ ASSERTION FAILED: " ^
-                "a refine operation should not modify the metasenv") ;
-              (* an assert would raise an exception that could be caught *)
-              exit 1
-             end ;
-            (resolve,term,metasenv'')::(filter tl)
-          with
-             CicRefine.MutCaseFixAndCofixRefineNotImplemented ->
-              (try
-                let term = CicTypeChecker.type_of_aux' metasenv' context expr in
-                 (resolve,term,metasenv')::(filter tl)
-               with _ -> filter tl
-              )
-           | _ -> filter tl
-    in
-     filter resolve_ids
+   List.iter
+    (function (resolve,term,newmetasenv) ->
+      (* If metasen <> newmetasenv is a normal condition, we should *)
+      (* be prepared to apply the returned substitution to the      *)
+      (* whole current proof.                                       *)
+      if metasenv <> newmetasenv then
+       begin
+        prerr_endline
+         ("+++++ ASSERTION FAILED: " ^
+          "a refine operation should not modify the metasenv") ;
+        (* an assert would raise an exception that could be caught *)
+        exit 1
+       end
+    ) resolve_ids ;
+   let resolve_id',term,metasenv' =
+    match resolve_ids with
+       [] -> raise ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
+     | [resolve_id] -> resolve_id
+     | _ ->
+       let choices =
+        List.map
+         (function (resolve,_,_) ->
+           List.map
+            (function id ->
+              id,
+               match resolve id with
+                  None -> assert false
+                | Some uri ->
+                   match uri with
+                      CicTextualParser0.ConUri uri
+                    | CicTextualParser0.VarUri uri ->
+                       UriManager.string_of_uri uri
+                    | CicTextualParser0.IndTyUri (uri,tyno) ->
+                       UriManager.string_of_uri uri ^ "#xpointer(1/" ^
+                        string_of_int (tyno+1) ^ ")"
+                    | CicTextualParser0.IndConUri (uri,tyno,consno) ->
+                       UriManager.string_of_uri uri ^ "#xpointer(1/" ^
+                        string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^                           ")"
+            ) dom
+         ) resolve_ids
+       in
+        let index = interactive_interpretation_choice choices in
+         List.nth resolve_ids index
    in
-    let resolve_id',term,metasenv' =
-     match resolve_ids' with
-        [] -> raise ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
-      | [resolve_id] -> resolve_id
-      | _ ->
-        let choices =
-         List.map
-          (function (resolve,_,_) ->
-            List.map
-             (function id ->
-               id,
-                match resolve id with
-                   None -> assert false
-                 | Some uri ->
-                    match uri with
-                       CicTextualParser0.ConUri uri
-                     | CicTextualParser0.VarUri uri ->
-                        UriManager.string_of_uri uri
-                     | CicTextualParser0.IndTyUri (uri,tyno) ->
-                        UriManager.string_of_uri uri ^ "#xpointer(1/" ^
-                         string_of_int (tyno+1) ^ ")"
-                     | CicTextualParser0.IndConUri (uri,tyno,consno) ->
-                        UriManager.string_of_uri uri ^ "#xpointer(1/" ^
-                         string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^                           ")"
-             ) dom
-          ) resolve_ids'
-        in
-         let index = interactive_interpretation_choice choices in
-          List.nth resolve_ids' index
-    in
-     id_to_uris := known_ids @ dom', resolve_id' ;
-     metasenv',term
+    id_to_uris := known_ids @ dom', resolve_id' ;
+    metasenv',term
 ;;
 
 (* A WIDGET TO ENTER CIC TERMS *)