| C.Lambda (name,so,ta) ->
C.Lambda (name, subst_inductive_type_with_dummy_mutind so,
subst_inductive_type_with_dummy_mutind ta)
+ | C.LetIn (name,so,ty,ta) ->
+ C.LetIn (name, subst_inductive_type_with_dummy_mutind so,
+ subst_inductive_type_with_dummy_mutind ty,
+ subst_inductive_type_with_dummy_mutind ta)
| C.Appl tl ->
C.Appl (List.map subst_inductive_type_with_dummy_mutind tl)
| C.MutCase (uri,i,outtype,term,pl) ->
exp_named_subst
in
C.Const (uri,exp_named_subst')
+ | C.Var (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map
+ (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
+ exp_named_subst
+ in
+ C.Var (uri,exp_named_subst')
| C.MutInd (uri,typeno,exp_named_subst) ->
let exp_named_subst' =
List.map
strictly_positive ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) ta
| C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
- | C.Appl ((C.MutInd (uri,i,exp_named_subst))::tl) ->
+ | C.Appl ((C.MutInd (uri,i,exp_named_subst))::_)
+ | (C.MutInd (uri,i,exp_named_subst)) as t ->
+ let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in
let (ok,paramsno,ity,cl,name) =
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
List.fold_right
(fun x i -> i && does_not_occur context n nn x)
arguments true &&
- (*CSC: MEGAPATCH3 (sara' quella giusta?)*)
List.fold_right
(fun x i ->
i &&
| (n, te) ->
raise (AssertFailure (lazy (sprintf "9 (%d, %s)" n (CicPp.ppterm te))))
-(*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *)
and check_is_really_smaller_arg ~subst context n nn kl x safes te =
- (*CSC: forse la whd si puo' fare solo quando serve veramente. *)
- (*CSC: cfr guarded_by_destructors *)
let module C = Cic in
let module U = UriManager in
+ (*CSC: we could perform beta-iota(-zeta?) immediately, and
+ delta only on-demand when it fails without *)
match CicReduction.whd ~subst context te with
C.Rel m when List.mem m safes -> true
- | C.Rel _ -> false
- | C.Var _
- | C.Meta _
- | C.Sort _
- | C.Implicit _
- | C.Cast _
-(* | C.Cast (te,ty) ->
- check_is_really_smaller_arg ~subst n nn kl x safes te &&
- check_is_really_smaller_arg ~subst n nn kl x safes ty*)
-(* | C.Prod (_,so,ta) ->
- check_is_really_smaller_arg ~subst n nn kl x safes so &&
- check_is_really_smaller_arg ~subst (n+1) (nn+1) kl (x+1)
- (List.map (fun x -> x + 1) safes) ta*)
- | C.Prod _ -> raise (AssertFailure (lazy "10"))
- | C.Lambda (name,so,ta) ->
- check_is_really_smaller_arg ~subst context n nn kl x safes so &&
- check_is_really_smaller_arg ~subst ((Some (name,(C.Decl so)))::context)
- (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
- | C.LetIn (name,so,ty,ta) ->
- check_is_really_smaller_arg ~subst context n nn kl x safes so &&
- check_is_really_smaller_arg ~subst context n nn kl x safes ty &&
- check_is_really_smaller_arg ~subst ((Some (name,(C.Def (so,ty))))::context)
- (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
- | C.Appl (he::_) ->
- (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
- (*CSC: solo perche' non abbiamo trovato controesempi *)
- check_is_really_smaller_arg ~subst context n nn kl x safes he
- | C.Appl [] -> raise (AssertFailure (lazy "11"))
+ | C.Rel _
+ | C.Appl _
+ | C.MutConstruct _
| C.Const _
- | C.MutInd _ -> raise (AssertFailure (lazy "12"))
- | C.MutConstruct _ -> false
+ | C.Var _ -> false
+ | C.Lambda (name,ty,ta) ->
+ check_is_really_smaller_arg ~subst (Some (name,Cic.Decl ty)::context)
+ (n+1) (nn+1) kl (x+1) (List.map (fun n -> n+1) safes) ta
| C.MutCase (uri,i,outtype,term,pl) ->
(match term with
- C.Rel m when List.mem m safes || m = x ->
- let (lefts_and_tys,len,isinductive,paramsno,cl) =
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
- match o with
- C.InductiveDefinition (tl,_,paramsno,_) ->
- let tys =
- List.map
- (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl
- in
- let (_,isinductive,_,cl) = List.nth tl i in
- let cl' =
- List.map
- (fun (id,ty) ->
- (id, snd (split_prods ~subst tys paramsno ty))) cl in
- let lefts =
- match tl with
- [] -> assert false
- | (_,_,ty,_)::_ ->
- fst (split_prods ~subst [] paramsno ty)
- in
- (lefts@tys,List.length tl,isinductive,paramsno,cl')
- | _ ->
- raise (TypeCheckerFailure
- (lazy ("Unknown mutual inductive definition:" ^
- UriManager.string_of_uri uri)))
- in
- if not isinductive then
- List.fold_right
- (fun p i ->
- i && check_is_really_smaller_arg ~subst context n nn kl x safes p)
- pl true
- else
- let pl_and_cl =
- try
- List.combine pl cl
- with
- Invalid_argument _ ->
- raise (TypeCheckerFailure (lazy "not enough patterns"))
- in
- 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') =
- get_new_safes ~subst context p c rl' safes n nn x
- in
- i &&
- check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
- ) pl_and_cl true
- | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
+ C.Rel m | C.Appl ((C.Rel m)::_) when List.mem m safes || m = x ->
let (lefts_and_tys,len,isinductive,paramsno,cl) =
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
i && check_is_really_smaller_arg ~subst context n nn kl x safes p)
pl true
else
- let pl_and_cl =
- try
- List.combine pl cl
- with
- 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 ->
+ List.for_all2
+ (fun p (_,c) ->
let rl' =
let debrujinedte = debrujin_constructor uri len c in
- recursive_args lefts_and_tys 0 len debrujinedte
+ recursive_args lefts_and_tys paramsno
+ (len+paramsno) debrujinedte
in
let (e, safes',n',nn',x',context') =
get_new_safes ~subst context p c rl' safes n nn x
in
- i &&
- check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
- ) pl_and_cl true
+ check_is_really_smaller_arg
+ ~subst context' n' nn' kl x' safes' e
+ ) pl cl
| _ ->
List.fold_right
(fun p i ->
) ([],0) fl
and safes' = List.map (fun x -> x + len) safes in
List.fold_right
- (fun (_,_,ty,bo) i ->
- i &&
- check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl
- x_plus_len safes' bo
- ) fl true
- | C.CoFix (_, fl) ->
- let len = List.length fl in
- let n_plus_len = n + len
- and nn_plus_len = nn + len
- and x_plus_len = x + len
- and tys,_ =
- List.fold_left
- (fun (types,len) (n,ty,_) ->
- (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
- len+1)
- ) ([],0) fl
- and safes' = List.map (fun x -> x + len) safes in
- List.fold_right
- (fun (_,ty,bo) i ->
+ (fun (_,_,_,bo) i ->
i &&
check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl
x_plus_len safes' bo
) fl true
+ | t ->
+ raise (AssertFailure (lazy ("An inhabitant of an inductive type in normal form cannot have this shape: " ^ CicPp.ppterm t)))
-and guarded_by_destructors ~subst context n nn kl x safes =
+and guarded_by_destructors ~subst context n nn kl x safes t =
let module C = Cic in
let module U = UriManager in
- function
+ match CicReduction.whd ~subst context t with
C.Rel m when m > n && m <= nn -> false
| C.Rel m ->
(match List.nth context (m-1) with
i && guarded_by_destructors ~subst context n nn kl x safes param
) tl true &&
check_is_really_smaller_arg ~subst context n nn kl x safes (List.nth tl k)
- | C.Appl tl ->
- List.fold_right
- (fun t i -> i && guarded_by_destructors ~subst context n nn kl x safes t)
- tl true
| C.Var (_,exp_named_subst)
| C.Const (_,exp_named_subst)
| C.MutInd (_,_,exp_named_subst)
guarded_by_destructors ~subst context n nn kl x safes outtype &&
(*CSC: manca ??? il controllo sul tipo di term? *)
List.fold_right
- (fun (p,(_,c,brujinedc)) i ->
- let rl' = recursive_args lefts_and_tys 0 len brujinedc in
+ (fun (p,(name,c,brujinedc)) i ->
+ i &&
+ let rl' = recursive_args
+ lefts_and_tys paramsno (len+paramsno) brujinedc in
let (e,safes',n',nn',x',context') =
get_new_safes ~subst context p c rl' safes n nn x
in
- i &&
guarded_by_destructors ~subst context' n' nn' kl x' safes' e
) pl_and_cl true
| C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
(fun (p,(_,c)) i ->
let rl' =
let debrujinedte = debrujin_constructor uri len c in
- recursive_args lefts_and_tys 0 len debrujinedte
+ recursive_args lefts_and_tys paramsno
+ (len+paramsno) debrujinedte
in
let (e, safes',n',nn',x',context') =
get_new_safes ~subst context p c rl' safes n nn x
(fun p i -> i && guarded_by_destructors ~subst context n nn kl x safes p)
pl true
)
- | C.Fix (_, fl) ->
+ | C.Appl (C.Fix (fixno, fl)::_) | C.Fix (fixno,fl) as t->
+ let l = match t with C.Appl (_::tl) -> tl | _ -> [] in
let len = List.length fl in
- let n_plus_len = n + len
- and nn_plus_len = nn + len
- and x_plus_len = x + len
- and tys,_ =
+ let n_plus_len = n + len in
+ let nn_plus_len = nn + len in
+ let x_plus_len = x + 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
- and safes' = List.map (fun x -> x + len) safes in
- List.fold_right
- (fun (_,_,ty,bo) i ->
- i && guarded_by_destructors ~subst context n nn kl x_plus_len safes' ty &&
- guarded_by_destructors ~subst (tys@context) n_plus_len nn_plus_len kl
- x_plus_len safes' bo
- ) fl true
+ ) ([],0) fl in
+ let safes' = List.map (fun x -> x + len) safes in
+ List.for_all
+ (guarded_by_destructors ~subst context n nn kl x safes) l &&
+ snd (List.fold_left
+ (fun (fixno',i) (_,recno,ty,bo) ->
+ fixno'+1,
+ i &&
+ guarded_by_destructors ~subst context n nn kl x_plus_len safes' ty &&
+ if
+ fixno' = fixno &&
+ List.length l > recno &&
+ (*case where the recursive argument is already really_smaller *)
+ check_is_really_smaller_arg ~subst context n nn kl x safes
+ (List.nth l recno)
+ then
+ let bo_without_lambdas,_,context =
+ eat_lambdas ~subst (tys@context) (recno+1) bo
+ in
+ (* we assume the formal argument to be safe *)
+ guarded_by_destructors ~subst context (n_plus_len+recno+1)
+ (nn_plus_len+recno+1) kl (x_plus_len+recno+1)
+ (1::List.map (fun x -> x+recno+1) safes')
+ bo_without_lambdas
+ else
+ guarded_by_destructors ~subst (tys@context) n_plus_len nn_plus_len
+ kl x_plus_len safes' bo
+ ) (0,true) fl)
| C.CoFix (_, fl) ->
let len = List.length fl in
let n_plus_len = n + len
guarded_by_destructors ~subst (tys@context) n_plus_len nn_plus_len kl
x_plus_len safes' bo
) fl true
+ | C.Appl tl ->
+ List.fold_right
+ (fun t i -> i && guarded_by_destructors ~subst context n nn kl x safes t)
+ tl true
(* the boolean h means already protected *)
(* args is the list of arguments the type of the constructor that may be *)
(len + eaten) kl 1 [] m) then
raise
(TypeCheckerFailure
- (lazy ("Fix: not guarded by destructors")))
+ (lazy ("Fix: not guarded by destructors:"^CicPp.ppterm t)))
else
ugraph2
end
CicUniv.empty_ugraph)
;;
-Deannotate.type_of_aux' := fun context t -> fst (type_of_aux' [] context t CicUniv.oblivion_ugraph);;
+Deannotate.type_of_aux' :=
+ fun context t ->
+ ignore (
+ List.fold_right
+ (fun el context ->
+ (match el with
+ None -> ()
+ | Some (_,Cic.Decl ty) ->
+ ignore (type_of_aux' [] context ty CicUniv.oblivion_ugraph)
+ | Some (_,Cic.Def (bo,ty)) ->
+ ignore (type_of_aux' [] context ty CicUniv.oblivion_ugraph);
+ ignore (type_of_aux' [] context bo CicUniv.oblivion_ugraph));
+ el::context
+ ) context []);
+ fst (type_of_aux' [] context t CicUniv.oblivion_ugraph);;
projects / helm.git / blobdiff