From 1641d372cb167eb85984d5491f076727bea3d6ea Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 23 Dec 2002 21:07:55 +0000 Subject: [PATCH] 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. --- helm/ocaml/cic_unification/cicRefine.ml | 11 +++++++++++ helm/ocaml/cic_unification/cicRefine.mli | 1 + 2 files changed, 12 insertions(+) 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 -- 2.39.2