| _ ->
raise (TypeCheckerFailure ("Unknown variable:" ^ U.string_of_uri uri))
-and does_not_occur context n nn te =
+and does_not_occur ?(subst=[]) context n nn te =
let module C = Cic in
(*CSC: whd sembra essere superflua perche' un caso in cui l'occorrenza *)
(*CSC: venga mangiata durante la whd sembra presentare problemi di *)
(*CSC: universi *)
- match CicReduction.whd context te with
+ match CicReduction.whd ~subst context te with
C.Rel m when m > n && m <= nn -> false
| C.Rel _
- | C.Meta _ (* CSC: Are we sure? No recursion?*)
| 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
| C.Cast (te,ty) ->
- does_not_occur context n nn te && does_not_occur context n nn 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 context n nn so &&
- does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
- 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 context n nn so &&
- does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
+ 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,dest) ->
- does_not_occur context n nn so &&
- does_not_occur ((Some (name,(C.Def (so,None))))::context)
+ does_not_occur ~subst context n nn so &&
+ does_not_occur ~subst ((Some (name,(C.Def (so,None))))::context)
(n + 1) (nn + 1) dest
| C.Appl l ->
- List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
+ 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 context n nn x)
+ 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 context n nn out && does_not_occur context n nn te &&
- List.fold_right (fun x i -> i && does_not_occur context n nn x) pl true
+ 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
in
List.fold_right
(fun (_,_,ty,bo) i ->
- i && does_not_occur context n nn ty &&
- does_not_occur (tys @ context) n_plus_len nn_plus_len bo
+ 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
in
List.fold_right
(fun (_,ty,bo) i ->
- i && does_not_occur context n nn ty &&
- does_not_occur (tys @ context) n_plus_len nn_plus_len bo
+ 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 *)
let dummy_mutind =
C.MutInd (HelmLibraryObjects.Datatypes.nat_URI,0,[])
in
- (*CSC mettere in cicSubstitution *)
+ (*CSC: mettere in cicSubstitution *)
let rec subst_inductive_type_with_dummy_mutind =
function
C.MutInd (uri',0,_) when UriManager.eq uri' uri ->
) cl' true
| t -> does_not_occur context n nn t
-(*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
+(* the inductive type indexes are s.t. n < x <= nn *)
and are_all_occurrences_positive context uri indparamsno i n nn te =
let module C = Cic in
match CicReduction.whd context te with
| C.Fix _
| C.CoFix _ -> raise (AssertFailure "6") (* due to type-checking *)
-and get_new_safes ?(subst = []) context p c rl safes n nn x =
+and get_new_safes ~subst context p c rl safes n nn x =
let module C = Cic in
let module U = UriManager in
let module R = CicReduction in
(Printf.sprintf "Get New Safes: c=%s ; p=%s"
(CicPp.ppterm c) (CicPp.ppterm p)))
-and split_prods ?(subst = []) context n te =
+and split_prods ~subst context n te =
let module C = Cic in
let module R = CicReduction in
- match (n, R.whd context te) with
+ match (n, R.whd ~subst context te) with
(0, _) -> context,te
| (n, C.Prod (name,so,ta)) when n > 0 ->
split_prods ~subst ((Some (name,(C.Decl so)))::context) (n - 1) ta
| (_, _) -> raise (AssertFailure "8")
-and eat_lambdas ?(subst = []) context n te =
+and eat_lambdas ~subst context n te =
let module C = Cic in
let module R = CicReduction in
match (n, R.whd ~subst context te) with
raise (AssertFailure (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 =
+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
- match CicReduction.whd context te with
+ match CicReduction.whd ~subst context te with
C.Rel m when List.mem m safes -> true
| C.Rel _ -> false
| C.Var _
recursive_args tys 0 len debrujinedte
in
let (e, safes',n',nn',x',context') =
- get_new_safes context p c rl' safes n nn x
+ 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
x_plus_len safes' bo
) fl true
-and guarded_by_destructors ?(subst = []) context n nn kl x safes =
+and guarded_by_destructors ~subst context n nn kl x safes =
let module C = Cic in
let module U = UriManager in
function
(match List.nth context (n-1) with
Some (_,C.Decl _) -> true
| Some (_,C.Def (bo,_)) ->
- guarded_by_destructors context m nn kl x safes
+ guarded_by_destructors ~subst context m nn kl x safes
(CicSubstitution.lift m bo)
| None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
)
| C.Sort _
| C.Implicit _ -> true
| C.Cast (te,ty) ->
- guarded_by_destructors context n nn kl x safes te &&
- guarded_by_destructors context n nn kl x safes ty
+ guarded_by_destructors ~subst context n nn kl x safes te &&
+ guarded_by_destructors ~subst context n nn kl x safes ty
| C.Prod (name,so,ta) ->
- guarded_by_destructors context n nn kl x safes so &&
- guarded_by_destructors ((Some (name,(C.Decl so)))::context)
+ guarded_by_destructors ~subst context n nn kl x safes so &&
+ guarded_by_destructors ~subst ((Some (name,(C.Decl so)))::context)
(n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
| C.Lambda (name,so,ta) ->
- guarded_by_destructors context n nn kl x safes so &&
- guarded_by_destructors ((Some (name,(C.Decl so)))::context)
+ guarded_by_destructors ~subst context n nn kl x safes so &&
+ guarded_by_destructors ~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,ta) ->
- guarded_by_destructors context n nn kl x safes so &&
- guarded_by_destructors ((Some (name,(C.Def (so,None))))::context)
+ guarded_by_destructors ~subst context n nn kl x safes so &&
+ guarded_by_destructors ~subst ((Some (name,(C.Def (so,None))))::context)
(n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
| C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
let k = List.nth kl (m - n - 1) in
else
List.fold_right
(fun param i ->
- i && guarded_by_destructors context n nn kl x safes param
+ 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 context n nn kl x safes t)
+ (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)
| C.MutConstruct (_,_,_,exp_named_subst) ->
List.fold_right
- (fun (_,t) i -> i && guarded_by_destructors context n nn kl x safes t)
+ (fun (_,t) i -> i && guarded_by_destructors ~subst context n nn kl x safes t)
exp_named_subst true
| C.MutCase (uri,i,outtype,term,pl) ->
- (match CicReduction.whd context term with
+ (match CicReduction.whd ~subst context term with
C.Rel m when List.mem m safes || m = x ->
let (tys,len,isinductive,paramsno,cl) =
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
UriManager.string_of_uri uri))
in
if not isinductive then
- guarded_by_destructors context n nn kl x safes outtype &&
- guarded_by_destructors context n nn kl x safes term &&
+ guarded_by_destructors ~subst context n nn kl x safes outtype &&
+ guarded_by_destructors ~subst context n nn kl x safes term &&
(*CSC: manca ??? il controllo sul tipo di term? *)
List.fold_right
(fun p i ->
- i && guarded_by_destructors context n nn kl x safes p)
+ i && guarded_by_destructors ~subst context n nn kl x safes p)
pl true
else
let pl_and_cl =
Invalid_argument _ ->
raise (TypeCheckerFailure "not enough patterns")
in
- guarded_by_destructors context n nn kl x safes outtype &&
+ 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 tys 0 len brujinedc in
let (e,safes',n',nn',x',context') =
- get_new_safes context p c rl' safes n nn x
+ get_new_safes ~subst context p c rl' safes n nn x
in
i &&
- guarded_by_destructors context' n' nn' kl x' safes' e
+ 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 ->
let (tys,len,isinductive,paramsno,cl) =
UriManager.string_of_uri uri))
in
if not isinductive then
- guarded_by_destructors context n nn kl x safes outtype &&
- guarded_by_destructors context n nn kl x safes term &&
+ guarded_by_destructors ~subst context n nn kl x safes outtype &&
+ guarded_by_destructors ~subst context n nn kl x safes term &&
(*CSC: manca ??? il controllo sul tipo di term? *)
List.fold_right
(fun p i ->
- i && guarded_by_destructors context n nn kl x safes p)
+ i && guarded_by_destructors ~subst context n nn kl x safes p)
pl true
else
let pl_and_cl =
Invalid_argument _ ->
raise (TypeCheckerFailure "not enough patterns")
in
- guarded_by_destructors context n nn kl x safes outtype &&
+ guarded_by_destructors ~subst context n nn kl x safes outtype &&
(*CSC: manca ??? il controllo sul tipo di term? *)
List.fold_right
(fun t i ->
- i && guarded_by_destructors context n nn kl x safes t)
+ i && guarded_by_destructors ~subst context n nn kl x safes t)
tl true &&
List.fold_right
(fun (p,(_,c)) i ->
recursive_args tys 0 len debrujinedte
in
let (e, safes',n',nn',x',context') =
- get_new_safes context p c rl' safes n nn x
+ get_new_safes ~subst context p c rl' safes n nn x
in
i &&
- guarded_by_destructors context' n' nn' kl x' safes' e
+ guarded_by_destructors ~subst context' n' nn' kl x' safes' e
) pl_and_cl true
| _ ->
- guarded_by_destructors context n nn kl x safes outtype &&
- guarded_by_destructors context n nn kl x safes term &&
+ guarded_by_destructors ~subst context n nn kl x safes outtype &&
+ guarded_by_destructors ~subst context n nn kl x safes term &&
(*CSC: manca ??? il controllo sul tipo di term? *)
List.fold_right
- (fun p i -> i && guarded_by_destructors context n nn kl x safes p)
+ (fun p i -> i && guarded_by_destructors ~subst context n nn kl x safes p)
pl true
)
| C.Fix (_, fl) ->
and safes' = List.map (fun x -> x + len) safes in
List.fold_right
(fun (_,_,ty,bo) i ->
- i && guarded_by_destructors context n nn kl x_plus_len safes' ty &&
- guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
+ 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
| C.CoFix (_, fl) ->
List.fold_right
(fun (_,ty,bo) i ->
i &&
- guarded_by_destructors context n nn kl x_plus_len safes' ty &&
- guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
+ 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
(* the boolean h means already protected *)
(* args is the list of arguments the type of the constructor that may be *)
(* found in head position must be applied to. *)
-(*CSC: coInductiveTypeURI non cambia mai di ricorsione in ricorsione *)
-and guarded_by_constructors context n nn h te args coInductiveTypeURI =
+and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI =
let module C = Cic in
(*CSC: There is a lot of code replication between the cases X and *)
(*CSC: (C.Appl X tl). Maybe it will be better to define a function *)
(*CSC: that maps X into (C.Appl X []) when X is not already a C.Appl *)
- match CicReduction.whd context te with
+ match CicReduction.whd ~subst context te with
C.Rel m when m > n && m <= nn -> h
| C.Rel _ -> true
| C.Meta _
(* the term has just been type-checked *)
raise (AssertFailure "17")
| C.Lambda (name,so,de) ->
- does_not_occur context n nn so &&
- guarded_by_constructors ((Some (name,(C.Decl so)))::context)
+ does_not_occur ~subst context n nn so &&
+ guarded_by_constructors ~subst ((Some (name,(C.Decl so)))::context)
(n + 1) (nn + 1) h de args coInductiveTypeURI
| C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
h &&
- List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
+ List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) tl true
| C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) ->
let consty =
let obj,_ =
UriManager.string_of_uri uri))
in
let rec analyse_branch context ty te =
- match CicReduction.whd context ty with
+ match CicReduction.whd ~subst context ty with
C.Meta _ -> raise (AssertFailure "34")
| C.Rel _
| C.Var _
| C.Sort _ ->
- does_not_occur context n nn te
+ does_not_occur ~subst context n nn te
| C.Implicit _
| C.Cast _ ->
raise (AssertFailure "24")(* due to type-checking *)
raise (AssertFailure "25")(* due to type-checking *)
| C.Appl ((C.MutInd (uri,_,_))::_) as ty
when uri == coInductiveTypeURI ->
- guarded_by_constructors context n nn true te [] coInductiveTypeURI
+ guarded_by_constructors ~subst context n nn true te []
+ coInductiveTypeURI
| C.Appl ((C.MutInd (uri,_,_))::_) as ty ->
- guarded_by_constructors context n nn true te tl coInductiveTypeURI
+ guarded_by_constructors ~subst context n nn true te tl
+ coInductiveTypeURI
| C.Appl _ ->
- does_not_occur context n nn te
+ does_not_occur ~subst context n nn te
| C.Const _ -> raise (AssertFailure "26")
| C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
- guarded_by_constructors context n nn true te [] coInductiveTypeURI
+ guarded_by_constructors ~subst context n nn true te []
+ coInductiveTypeURI
| C.MutInd _ ->
- does_not_occur context n nn te
+ does_not_occur ~subst context n nn te
| C.MutConstruct _ -> raise (AssertFailure "27")
(*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
(*CSC: in head position. *)
raise (AssertFailure "28")(* due to type-checking *)
in
let rec analyse_instantiated_type context ty l =
- match CicReduction.whd context ty with
+ match CicReduction.whd ~subst context ty with
C.Rel _
| C.Var _
| C.Meta _
raise (AssertFailure "30")(* due to type-checking *)
| C.Appl _ ->
List.fold_left
- (fun i x -> i && does_not_occur context n nn x) true l
+ (fun i x -> i && does_not_occur ~subst context n nn x) true l
| C.Const _ -> raise (AssertFailure "31")
| C.MutInd _ ->
List.fold_left
- (fun i x -> i && does_not_occur context n nn x) true l
+ (fun i x -> i && does_not_occur ~subst context n nn x) true l
| C.MutConstruct _ -> raise (AssertFailure "32")
(*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
(*CSC: in head position. *)
function
[] -> true
| tlhe::tltl as l ->
- let consty' = CicReduction.whd context consty in
+ let consty' = CicReduction.whd ~subst context consty in
match args with
he::tl ->
begin
C.Prod (_,_,de) ->
let instantiated_de = CicSubstitution.subst he de in
(*CSC: siamo sicuri che non sia troppo forte? *)
- does_not_occur context n nn tlhe &
+ does_not_occur ~subst context n nn tlhe &
instantiate_type tl instantiated_de tltl
| _ ->
(*CSC:We do not consider backbones with a MutCase, a *)
in
instantiate_type args consty tl
| C.Appl ((C.CoFix (_,fl))::tl) ->
- List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
+ List.fold_left (fun i x -> i && does_not_occur ~subst context n nn x) true tl &&
let len = List.length fl in
let n_plus_len = n + len
and nn_plus_len = nn + len
and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
List.fold_right
(fun (_,ty,bo) i ->
- i && does_not_occur context n nn ty &&
- guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
- args coInductiveTypeURI
+ i && does_not_occur ~subst context n nn ty &&
+ guarded_by_constructors ~subst (tys@context) n_plus_len nn_plus_len
+ h bo args coInductiveTypeURI
) fl true
| C.Appl ((C.MutCase (_,_,out,te,pl))::tl) ->
- List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
- does_not_occur context n nn out &&
- does_not_occur context n nn te &&
+ List.fold_left (fun i x -> i && does_not_occur ~subst context n nn x) true tl &&
+ does_not_occur ~subst context n nn out &&
+ does_not_occur ~subst context n nn te &&
List.fold_right
(fun x i ->
i &&
- guarded_by_constructors context n nn h x args coInductiveTypeURI
+ guarded_by_constructors ~subst context n nn h x args
+ coInductiveTypeURI
) pl true
| C.Appl l ->
- List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
+ 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) ->
List.fold_right
- (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
+ (fun (_,x) i -> i && does_not_occur ~subst context n nn x) exp_named_subst true
| C.MutInd _ -> assert false
| C.MutConstruct (_,_,_,exp_named_subst) ->
List.fold_right
- (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
+ (fun (_,x) i -> i && does_not_occur ~subst context n nn x) exp_named_subst true
| C.MutCase (_,_,out,te,pl) ->
- does_not_occur context n nn out &&
- does_not_occur context n nn te &&
+ does_not_occur ~subst context n nn out &&
+ does_not_occur ~subst context n nn te &&
List.fold_right
(fun x i ->
i &&
- guarded_by_constructors context n nn h x args coInductiveTypeURI
+ guarded_by_constructors ~subst context n nn h x args
+ coInductiveTypeURI
) pl true
| C.Fix (_,fl) ->
let len = List.length fl in
and tys = List.map (fun (n,_,ty,_)-> Some (C.Name n,(C.Decl ty))) fl in
List.fold_right
(fun (_,_,ty,bo) i ->
- i && does_not_occur context n nn ty &&
- does_not_occur (tys@context) n_plus_len nn_plus_len bo
+ 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
and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
List.fold_right
(fun (_,ty,bo) i ->
- i && does_not_occur context n nn ty &&
- guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
+ i && does_not_occur ~subst context n nn ty &&
+ guarded_by_constructors ~subst (tys@context) n_plus_len nn_plus_len
+ h bo
args coInductiveTypeURI
) fl true
CicReduction.are_convertible ~subst ~metasenv context so ind ugraph
| (_,_) -> false,ugraph
-and type_of_branch context argsno need_dummy outtype term constype =
+and type_of_branch ~subst context argsno need_dummy outtype term constype =
let module C = Cic in
let module R = CicReduction in
- match R.whd context constype with
+ match R.whd ~subst context constype with
C.MutInd (_,_,_) ->
if need_dummy then
outtype
C.Appl l -> C.Appl (l@[C.Rel 1])
| t -> C.Appl [t ; C.Rel 1]
in
- C.Prod (C.Anonymous,so,type_of_branch
+ C.Prod (C.Anonymous,so,type_of_branch ~subst
((Some (name,(C.Decl so)))::context) argsno need_dummy
(CicSubstitution.lift 1 outtype) term' de)
| _ -> raise (AssertFailure "20")
with the actual context *)
-and check_metasenv_consistency ~logger ?(subst=[]) metasenv context
+and check_metasenv_consistency ~logger ~subst metasenv context
canonical_context l ugraph
=
let module C = Cic in
(* The type of the LetIn is reduced. Much faster than the previous
solution. Moreover the inferred type is probably very different
from the expected one.
- (CicReduction.whd context
+ (CicReduction.whd ~subst context
(C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)))
*)
(* One-step LetIn reduction. Even faster than the previous solution.
(*
let (parameters, arguments, exp_named_subst),ugraph2 =
let ty,ugraph2 = type_of_aux context term ugraph1 in
- match R.whd context ty with
+ match R.whd ~subst context ty with
(*CSC manca il caso dei CAST *)
(*CSC: ma servono i parametri (uri,i)? Se si', perche' non serve anche il *)
(*CSC: parametro exp_named_subst? Se no, perche' non li togliamo? *)
let ty_cons,ugraph3 = type_of_aux ~logger context cons ugraph1 in
(* 2 is skipped *)
let ty_branch =
- type_of_branch context parsno need_dummy outtype cons
+ type_of_branch ~subst context parsno need_dummy outtype cons
ty_cons in
let b1,ugraph4 =
R.are_convertible
let's control the guarded by
destructors conditions D{f,k,x,M}
*)
- if not (guarded_by_destructors context' eaten
+ if not (guarded_by_destructors ~subst context' eaten
(len + eaten) kl 1 [] m) then
raise
(TypeCheckerFailure
if b then
begin
(* let's control that the returned type is coinductive *)
- match returns_a_coinductive context ty with
+ match returns_a_coinductive ~subst context ty with
None ->
raise
(TypeCheckerFailure
let's control the guarded by constructors
conditions C{f,M}
*)
- if not (guarded_by_constructors (types @ context)
- 0 len false bo [] uri) then
+ if not (guarded_by_constructors ~subst
+ (types @ context) 0 len false bo [] uri) then
raise
(TypeCheckerFailure
("CoFix: not guarded by constructors"))
let (_,ty,_) = List.nth fl i in
ty,ugraph2
- and check_exp_named_subst ~logger ?(subst = []) context ugraph =
+ and check_exp_named_subst ~logger ~subst context ugraph =
let rec check_exp_named_subst_aux ~logger esubsts l ugraph =
match l with
[] -> ugraph
in
check_exp_named_subst_aux ~logger [] ugraph
- and sort_of_prod ?(subst = []) context (name,s) (t1, t2) ugraph =
+ and sort_of_prod ~subst context (name,s) (t1, t2) ugraph =
let module C = Cic in
let t1' = CicReduction.whd ~subst context t1 in
let t2' = CicReduction.whd ~subst ((Some (name,C.Decl s))::context) t2 in
"Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1')
(CicPp.ppterm t2')))
- and eat_prods ?(subst = []) context hetype l ugraph =
+ and eat_prods ~subst context hetype l ugraph =
(*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
(*CSC: cucinati *)
match l with
"Appl: this is not a function, it cannot be applied")
)
- and returns_a_coinductive context ty =
+ and returns_a_coinductive ~subst context ty =
let module C = Cic in
- match CicReduction.whd context ty with
+ match CicReduction.whd ~subst context ty with
C.MutInd (uri,i,_) ->
(*CSC: definire una funzioncina per questo codice sempre replicato *)
let obj,_ =
UriManager.string_of_uri uri))
)
| C.Prod (n,so,de) ->
- returns_a_coinductive ((Some (n,C.Decl so))::context) de
+ returns_a_coinductive ~subst ((Some (n,C.Decl so))::context) de
| _ -> None
in
let module C = Cic in
match CicReduction.whd context c with
C.Prod (n,so,de) ->
- (*CSC: [] is an empty metasenv. Is it correct? *)
let s,ugraph1 = type_of_aux' ~logger [] context so ugraph in
let b = (s = C.Sort C.Prop || s = C.Sort C.Set || s = C.Sort C.CProp) in
if b then
false,ugraph1
| _ -> true,ugraph (*CSC: we trust the type-checker *)
in
- let (context',dx) = split_prods context paramsno c in
+ let (context',dx) = split_prods ~subst:[] context paramsno c in
is_small_aux ~logger context' dx ugraph
and type_of ~logger t ugraph =
projects / helm.git / commitdiff