Invalid_argument _ ->
raise (TypeCheckerFailure (lazy "not enough patterns"))
in
+ (*CSC: supponiamo come prima che nessun controllo sia necessario*)
+ (*CSC: sugli argomenti di una applicazione *)
List.fold_right
(fun (p,(_,c)) i ->
let rl' =
let debrujinedte = debrujin_constructor uri len c in
recursive_args lefts_and_tys 0 len debrujinedte
in
- let (e, safes',n',nn',x',context') =
+ let (e,safes',n',nn',x',context') =
get_new_safes ~subst context p c rl' safes n nn x
in
i &&
in
typeof_aux context term
+and check_mutual_inductive_defs _ = assert false
+and eat_lambdas ~subst _ _ _ = assert false
+and guarded_by_constructors ~subst _ _ _ _ _ _ _ = assert false
+and guarded_by_destructors ~subst _ _ _ _ _ _ _ = assert false
+and returns_a_coinductive ~subst _ _ = assert false
+
and type_of_constant ref = assert false (* USARE typecheck_obj0 *)
(* ALIAS typecheck *)
(*
| _ ->
raise (TypeCheckerFailure
(lazy ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri)))
+CASO COSTANTE
+CASO FIX/COFIX
*)
-and typecheck_obj0 = function
- obj -> assert false
-(*
- | C.Constant (_,Some te,ty,_,_) ->
- let _,ugraph = type_of ~logger ty ugraph in
- let ty_te,ugraph = type_of ~logger te ugraph in
- let b,ugraph = (CicReduction.are_convertible [] ty_te ty ugraph) in
- if not b then
- raise (TypeCheckerFailure
- (lazy
- ("the type of the body is not the one expected:\n" ^
- CicPp.ppterm ty_te ^ "\nvs\n" ^
- CicPp.ppterm ty)))
- else
- ugraph
- | C.Constant (_,None,ty,_,_) ->
- (* only to check that ty is well-typed *)
- let _,ugraph = type_of ~logger ty ugraph in
- ugraph
- | C.CurrentProof (_,conjs,te,ty,_,_) ->
- let _,ugraph =
- List.fold_left
- (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
- let _,ugraph =
- type_of_aux' ~logger metasenv context ty ugraph
- in
- metasenv @ [conj],ugraph
- ) ([],ugraph) conjs
- in
- let _,ugraph = type_of_aux' ~logger conjs [] ty ugraph in
- let type_of_te,ugraph =
- type_of_aux' ~logger conjs [] te ugraph
- in
- let b,ugraph = CicReduction.are_convertible [] type_of_te ty ugraph in
- if not b then
- raise (TypeCheckerFailure (lazy (sprintf
- "the current proof is not well typed because the type %s of the body is not convertible to the declared type %s"
- (CicPp.ppterm type_of_te) (CicPp.ppterm ty))))
- else
- ugraph
- | (C.InductiveDefinition _ as obj) ->
- check_mutual_inductive_defs ~logger uri obj ugraph
- | C.Fix (i,fl) ->
- let types,kl,ugraph1,len =
+and typecheck_obj0 (uri,height,metasenv,subst,kind) =
+ (* CSC: here we should typecheck the metasenv and the subst *)
+ assert (metasenv = [] && subst = []);
+ match kind with
+ | C.Constant (_,_,Some te,ty,_) ->
+ let _ = typeof ~subst ~metasenv [] ty in
+ let ty_te = typeof ~subst ~metasenv [] te in
+ if not (R.are_convertible ~subst ~metasenv [] ty_te ty) then
+ raise (TypeCheckerFailure (lazy (Printf.sprintf
+ "the type of the body is not the one expected:\n%s\nvs\n%s"
+ (NCicPp.ppterm ty_te) (NCicPp.ppterm ty))))
+ | C.Constant (_,_,None,ty,_) -> ignore (typeof ~subst ~metasenv [] ty)
+ | C.Inductive _ as obj -> check_mutual_inductive_defs uri obj
+ | C.Fixpoint (inductive,fl,_) ->
+ let types,kl,len =
List.fold_left
- (fun (types,kl,ugraph,len) (n,k,ty,_) ->
- let _,ugraph1 = type_of_aux ~logger context ty ugraph in
- (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
- k::kl,ugraph1,len+1)
- ) ([],[],ugraph,0) fl
+ (fun (types,kl,len) (_,n,k,ty,_) ->
+ let _ = typeof ~subst ~metasenv [] ty in
+ ((n,(C.Decl (S.lift len ty)))::types, k::kl,len+1)
+ ) ([],[],0) fl
in
- let ugraph2 =
- List.fold_left
- (fun ugraph (name,x,ty,bo) ->
- let ty_bo,ugraph1 =
- type_of_aux ~logger (types@context) bo ugraph
- in
- let b,ugraph2 =
- R.are_convertible ~subst ~metasenv (types@context)
- ty_bo (CicSubstitution.lift len ty) ugraph1 in
- if b then
- begin
- let (m, eaten, context') =
- eat_lambdas ~subst (types @ context) (x + 1) bo
- in
- (*
- let's control the guarded by
- destructors conditions D{f,k,x,M}
- *)
- if not (guarded_by_destructors ~subst context' eaten
- (len + eaten) kl 1 [] m) then
- raise
- (TypeCheckerFailure
- (lazy ("Fix: not guarded by destructors")))
- else
- ugraph2
- end
- else
- raise (TypeCheckerFailure (lazy ("Fix: ill-typed bodies")))
- ) ugraph1 fl in
- (*CSC: controlli mancanti solo su D{f,k,x,M} *)
- let (_,_,ty,_) = List.nth fl i in
- ty,ugraph2
- | C.CoFix (i,fl) ->
- let types,ugraph1,len =
- List.fold_left
- (fun (l,ugraph,len) (n,ty,_) ->
- let _,ugraph1 =
- type_of_aux ~logger context ty ugraph in
- (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::l,
- ugraph1,len+1)
- ) ([],ugraph,0) fl
- in
- let ugraph2 =
- List.fold_left
- (fun ugraph (_,ty,bo) ->
- let ty_bo,ugraph1 =
- type_of_aux ~logger (types @ context) bo ugraph
- in
- let b,ugraph2 =
- R.are_convertible ~subst ~metasenv (types @ context) ty_bo
- (CicSubstitution.lift len ty) ugraph1
- in
- if b then
- begin
- (* let's control that the returned type is coinductive *)
- match returns_a_coinductive ~subst context ty with
- None ->
- raise
- (TypeCheckerFailure
- (lazy "CoFix: does not return a coinductive type"))
- | Some uri ->
- (*
- let's control the guarded by constructors
- conditions C{f,M}
- *)
- if not (guarded_by_constructors ~subst
- (types @ context) 0 len false bo [] uri) then
- raise
- (TypeCheckerFailure
- (lazy "CoFix: not guarded by constructors"))
- else
- ugraph2
- end
- else
- raise
- (TypeCheckerFailure (lazy "CoFix: ill-typed bodies"))
- ) ugraph1 fl
- in
- let (_,ty,_) = List.nth fl i in
- ty,ugraph2
-
-*)
+ List.iter (fun (_,name,x,ty,bo) ->
+ let ty_bo = typeof ~subst ~metasenv types bo in
+ if not (R.are_convertible ~subst ~metasenv types ty_bo
+ (S.lift len ty))
+ then raise (TypeCheckerFailure (lazy ("(Co)Fix: ill-typed bodies")))
+ else
+ if inductive then begin
+ let m, eaten, context =
+ eat_lambdas ~subst types (x + 1) bo
+ in
+ (* guarded by destructors conditions D{f,k,x,M} *)
+ if not (guarded_by_destructors ~subst context eaten
+ (len + eaten) kl 1 [] m)
+ then
+ raise(TypeCheckerFailure(lazy("Fix: not guarded by destructors")))
+ end else
+ match returns_a_coinductive ~subst [] ty with
+ | None ->
+ raise (TypeCheckerFailure
+ (lazy "CoFix: does not return a coinductive type"))
+ | Some uri ->
+ (* guarded by constructors conditions C{f,M} *)
+ if not (guarded_by_constructors ~subst
+ types 0 len false bo [] uri)
+ then
+ raise (TypeCheckerFailure
+ (lazy "CoFix: not guarded by constructors"))
+ ) fl
let typecheck_obj (*uri*) obj = assert false (*
let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph obj in
projects / helm.git / commitdiff