From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 23 Dec 2002 21:07:55 +0000 (+0000)
Subject: Refine can now also raise Uncertain. The exception is raised every
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1641d372cb167eb85984d5491f076727bea3d6ea;p=helm.git

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 f7a0ab2e8..e5e846982 100644
--- 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 18884bb12..338f50663 100644
--- 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