exception CicEnvironmentError;;
-and does_not_occur ?(subst=[]) context n nn te =
- let module C = Cic in
- match te with
- C.Rel m when m > n && m <= nn -> false
- | C.Rel m ->
- (try
- (match List.nth context (m-1) with
- Some (_,C.Def (bo,_)) ->
- does_not_occur ~subst context n nn (CicSubstitution.lift m bo)
- | _ -> true)
- with
- Failure _ -> assert false)
- | C.Sort _
- | C.Implicit _ -> true
- | C.Meta (_,l) ->
- List.fold_right
- (fun x i ->
- match x with
- None -> i
- | Some x -> i && does_not_occur ~subst context n nn x) l true &&
- (try
- let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in
- does_not_occur ~subst context n nn (CicSubstitution.subst_meta l term)
- with
- CicUtil.Subst_not_found _ -> true)
- | C.Cast (te,ty) ->
- does_not_occur ~subst context n nn te && does_not_occur ~subst context n nn ty
- | C.Prod (name,so,dest) ->
- does_not_occur ~subst context n nn so &&
- does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n + 1)
- (nn + 1) dest
- | C.Lambda (name,so,dest) ->
- does_not_occur ~subst context n nn so &&
- does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
- dest
- | C.LetIn (name,so,ty,dest) ->
- does_not_occur ~subst context n nn so &&
- does_not_occur ~subst context n nn ty &&
- does_not_occur ~subst ((Some (name,(C.Def (so,ty))))::context)
- (n + 1) (nn + 1) dest
- | C.Appl l ->
- List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) l true
- | C.Var (_,exp_named_subst)
- | C.Const (_,exp_named_subst)
- | C.MutInd (_,_,exp_named_subst)
- | C.MutConstruct (_,_,_,exp_named_subst) ->
- List.fold_right (fun (_,x) i -> i && does_not_occur ~subst context n nn x)
- exp_named_subst true
- | C.MutCase (_,_,out,te,pl) ->
- does_not_occur ~subst context n nn out && does_not_occur ~subst context n nn te &&
- List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) pl true
- | C.Fix (_,fl) ->
- let len = List.length fl in
- let n_plus_len = n + len in
- let nn_plus_len = nn + len in
- let tys,_ =
- List.fold_left
- (fun (types,len) (n,_,ty,_) ->
- (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
- len+1)
- ) ([],0) fl
- in
- List.fold_right
- (fun (_,_,ty,bo) i ->
- i && does_not_occur ~subst context n nn ty &&
- does_not_occur ~subst (tys @ context) n_plus_len nn_plus_len bo
- ) fl true
- | C.CoFix (_,fl) ->
- let len = List.length fl in
- let n_plus_len = n + len in
- let nn_plus_len = nn + len in
- let tys,_ =
- List.fold_left
- (fun (types,len) (n,ty,_) ->
- (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
- len+1)
- ) ([],0) fl
- in
- List.fold_right
- (fun (_,ty,bo) i ->
- i && does_not_occur ~subst context n nn ty &&
- does_not_occur ~subst (tys @ context) n_plus_len nn_plus_len bo
- ) fl true
-
(*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
(*CSC questa funzione e' simile alla are_all_occurrences_positive, ma fa *)
(*CSC dei controlli leggermente diversi. Viene invocata solamente dalla *)
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 &&
aux ty_he args_with_ty
;;
+exception DoesOccur;;
+
+let does_not_occur ~subst context n nn t =
+ let rec aux (context,n,nn as k) _ = function
+ | C.Rel m when m > n && m <= nn -> raise DoesOccur
+ | C.Rel m ->
+ (try (match List.nth context (m-1) with
+ | _,C.Def (bo,_) -> aux k () (S.lift m bo)
+ | _ -> ())
+ with Failure _ -> assert false)
+ | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) -> (* closed meta *) ()
+ | C.Meta (mno,(s,l)) ->
+ (try
+ let _,_,term,_ = U.lookup_subst mno subst in
+ aux (context,n+s,nn+s) () (S.subst_meta (0,l) term)
+ with CicUtil.Subst_not_found _ -> match l with
+ | C.Irl len -> if not (n >= s+len || s > nn) then raise DoesOccur
+ | C.Ctx lc -> List.iter (aux (context,n+s,nn+s) ()) lc)
+ | t -> U.fold (fun e (ctx,n,nn) -> (e::ctx,n+1,nn+1)) k aux () t
+ in
+ try aux (context,n,nn) () t; true
+ with DoesOccur -> false
+;;
+
let rec typeof ~subst ~metasenv context term =
let rec typeof_aux context = function
| C.Rel n ->
| C.Meta (n,l) as t ->
let canonical_context,ty =
try
- let _,c,_,ty = NCicUtils.lookup_subst n subst in c,ty
- with NCicUtils.Subst_not_found _ -> try
- let _,_,c,ty = NCicUtils.lookup_meta n metasenv in c,ty
- with NCicUtils.Meta_not_found _ ->
+ let _,c,_,ty = U.lookup_subst n subst in c,ty
+ with U.Subst_not_found _ -> try
+ let _,_,c,ty = U.lookup_meta n metasenv in c,ty
+ with U.Meta_not_found _ ->
raise (AssertFailure (lazy (Printf.sprintf
"%s not found" (NCicPp.ppterm t))))
in
S.subst_meta l (S.lift i ty)))::(lift_metas (i+1) tl)
in
lift_metas 1 canonical_context in
- let l = NCicUtils.expand_local_context lc_kind in
+ let l = U.expand_local_context lc_kind in
try
List.iter2
(fun t ct ->
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 / blobdiff