Refine can now also raise Uncertain. The exception is raised every

time a metavariab le could be instantiated in such a way that the
term could become well-typed. Useful for ambiguous parsing.

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index f7a0ab2e877a36c3e851fc45f4f57ad69a47c17d..e5e8469824226e37c5a2c013345f5e8d17c7d879 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -25,6 +25,7 @@
 
 exception Impossible of int;;
 exception NotRefinable of string;;
+exception Uncertain of string;;
 exception WrongUriToConstant of string;;
 exception WrongUriToVariable of string;;
 exception WrongUriToMutualInductiveDefinitions of string;;
@@ -291,6 +292,12 @@ and type_of_aux' metasenv context t =
      | (C.Sort s1, C.Sort s2) ->
          (*CSC manca la gestione degli universi!!! *)
          C.Sort C.Type,subst',metasenv'
+     | (C.Meta _,_)
+     | (_,C.Meta _) ->
+       raise
+        (Uncertain
+          ("Two sorts were expected, found " ^ CicPp.ppterm t1'' ^ " and " ^
+           CicPp.ppterm t2''))
      | (_,_) ->
        raise
         (NotRefinable
@@ -310,6 +317,10 @@ and type_of_aux' metasenv context t =
          in
           CicReduction.fdebug := -1 ;
           eat_prods subst' metasenv' context (CicSubstitution.subst hete t) tl
+      | Cic.Meta _ as t ->
+         raise
+          (Uncertain
+            ("Prod expected, " ^ CicPp.ppterm t ^ " found"))
       | _ -> raise (NotRefinable "Appl: wrong Prod-type")
     )
  in

diff --git a/helm/ocaml/cic_unification/cicRefine.mli b/helm/ocaml/cic_unification/cicRefine.mli
index 18884bb12983c3ea86bf510c293ef16b1528c34b..338f50663dba12ac272dcbbc2ce9246e9cbb7074 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.mli
+++ b/helm/ocaml/cic_unification/cicRefine.mli
@@ -24,6 +24,7 @@
  *)
 
 exception NotRefinable of string
+exception Uncertain of string
 exception WrongUriToConstant of string
 exception WrongUriToVariable of string
 exception WrongUriToMutualInductiveDefinitions of string