*)
exception NotImplemented;;
-exception Impossible;;
+exception Impossible of int;;
exception NotWellTyped of string;;
exception WrongUriToConstant of string;;
exception WrongUriToVariable of string;;
instantiate_parameters tl
(CicSubstitution.subst he ta)
| (C.Cast (te,_), _) -> instantiate_parameters params te
- | (t,l) -> raise Impossible
+ | (t,l) -> raise (Impossible 1)
and strictly_positive n nn te =
let module C = Cic in
raise (NotPositiveOccurrences (U.string_of_uri uri))
else
match !r with
- Some _ -> raise Impossible
+ Some _ -> raise (Impossible 2)
| None -> r := Some (recursive_args 0 len te)
) cl ;
(i + 1)
| C.Meta _
| C.Sort _
| C.Implicit
- | C.Cast _ (*CSC ??? *) -> raise Impossible (* due to type-checking *)
+ | C.Cast _ (*CSC ??? *) -> raise (Impossible 3) (* due to type-checking *)
| C.Prod (_,so,de) ->
(not (does_not_occur n nn so))::(recursive_args (n+1) (nn + 1) de)
- | C.Lambda _ -> raise Impossible (* due to type-checking *)
+ | C.Lambda _ -> raise (Impossible 4) (* due to type-checking *)
| C.LetIn _ -> raise NotImplemented
| C.Appl _ -> []
| C.Const _
- | C.Abst _ -> raise Impossible
+ | C.Abst _ -> raise (Impossible 5)
| C.MutInd _
| C.MutConstruct _
| C.MutCase _
| C.Fix _
- | C.CoFix _ -> raise Impossible (* due to type-checking *)
+ | C.CoFix _ -> raise (Impossible 6) (* due to type-checking *)
and get_new_safes p c rl safes n nn x =
let module C = Cic in
get_new_safes ta2 ta1 tl safes'' (n+1) (nn+1) (x+1)
| (C.MutInd _, e, []) -> (e,safes,n,nn,x)
| (C.Appl _, e, []) -> (e,safes,n,nn,x)
- | (_,_,_) -> raise Impossible
+ | (_,_,_) -> raise (Impossible 7)
and eat_prods n te =
let module C = Cic in
match (n, R.whd te) with
(0, _) -> te
| (n, C.Prod (_,_,ta)) when n > 0 -> eat_prods (n - 1) ta
- | (_, _) -> raise Impossible
+ | (_, _) -> raise (Impossible 8)
and eat_lambdas n te =
let module C = Cic in
| (n, C.Lambda (_,_,ta)) when n > 0 ->
let (te, k) = eat_lambdas (n - 1) ta in
(te, k + 1)
- | (_, _) -> raise Impossible
+ | (_, _) -> raise (Impossible 9)
(*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *)
and check_is_really_smaller_arg n nn kl x safes te =
check_is_really_smaller_arg n nn kl x safes so &&
check_is_really_smaller_arg (n+1) (nn+1) kl (x+1)
(List.map (fun x -> x + 1) safes) ta*)
- | C.Prod _ -> raise Impossible
+ | C.Prod _ -> raise (Impossible 10)
| C.Lambda (_,so,ta) ->
check_is_really_smaller_arg n nn kl x safes so &&
check_is_really_smaller_arg (n+1) (nn+1) kl (x+1)
(*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
(*CSC: solo perche' non abbiamo trovato controesempi *)
check_is_really_smaller_arg n nn kl x safes he
- | C.Appl [] -> raise Impossible
+ | C.Appl [] -> raise (Impossible 11)
| C.Const _
| C.Abst _
- | C.MutInd _ -> raise Impossible
+ | C.MutInd _ -> raise (Impossible 12)
| C.MutConstruct _ -> false
| C.MutCase (uri,_,i,outtype,term,pl) ->
(match term with
Some rl' ->
let (_,rl'') = split rl' paramsno in
rl''
- | None -> raise Impossible
+ | None -> raise (Impossible 13)
in
let (e,safes',n',nn',x') =
get_new_safes p c rl' safes n nn x
Some rl' ->
let (_,rl'') = split rl' paramsno in
rl''
- | None -> raise Impossible
+ | None -> raise (Impossible 14)
in
let (e, safes',n',nn',x') =
get_new_safes p c rl' safes n nn x
Some rl' ->
let (_,rl'') = split rl' paramsno in
rl''
- | None -> raise Impossible
+ | None -> raise (Impossible 15)
in
let (e,safes',n',nn',x') =
get_new_safes p c rl' safes n nn x
Some rl' ->
let (_,rl'') = split rl' paramsno in
rl''
- | None -> raise Impossible
+ | None -> raise (Impossible 16)
in
let (e, safes',n',nn',x') =
get_new_safes p c rl' safes n nn x
guarded_by_constructors n nn h te &&
guarded_by_constructors n nn h ty
| C.Prod (_,so,de) ->
- raise Impossible (* the term has just been type-checked *)
+ raise (Impossible 17) (* the term has just been type-checked *)
| C.Lambda (_,so,de) ->
does_not_occur n nn so &&
guarded_by_constructors (n + 1) (nn + 1) h de
let (_,is_inductive,_,cl) = List.nth itl i in
let (_,cons,rrec_args) = List.nth cl (j - 1) in
(match !rrec_args with
- None -> raise Impossible
+ None -> raise (Impossible 18)
| Some rec_args -> (not is_inductive, rec_args)
)
| _ ->
raise (WrongUriToMutualInductiveDefinitions
(U.string_of_uri uri))
)
- | _ -> raise Impossible
+ | _ -> raise (Impossible 19)
)
| (C.Sort C.Type, C.Prod (_,so,_)) when not need_dummy ->
CicReduction.are_convertible so ind
C.Prod (C.Name "pippo",so,type_of_branch argsno need_dummy
(CicSubstitution.lift 1 outtype)
(C.Appl [CicSubstitution.lift 1 term ; C.Rel 1]) de)
- | _ -> raise Impossible
+ | _ -> raise (Impossible 20)
and type_of t =
ty
| C.Meta n -> raise NotImplemented
| C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
- | C.Implicit -> raise Impossible
+ | C.Implicit -> raise (Impossible 21)
| C.Cast (te,ty) ->
let _ = type_of ty in
if R.are_convertible (type_of_aux env te) ty then ty
let cty = cooked_type_of_constant uri cookingsno in
decr fdebug ;
cty
- | C.Abst _ -> raise Impossible
+ | C.Abst _ -> raise (Impossible 22)
| C.MutInd (uri,cookingsno,i) ->
incr fdebug ;
let cty = cooked_type_of_mutual_inductive_defs uri cookingsno i in
projects / helm.git / commitdiff