- try
- fo_unif_subst subst context metasenv instance instance'
- ugraph
- with
- exn ->
- enrich localization_tbl p exn
- ~f:(function _ ->
- lazy ("The term " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst p
- context ^ " has type " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst instance'
- context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst instance
- context)))
- (subst,metasenv,ugraph5) pl' outtypeinstances
- in
- C.MutCase (uri, i, outtype, term', pl'),
- CicReduction.head_beta_reduce
- (CicMetaSubst.apply_subst subst
- (C.Appl(outtype::right_args@[term']))),
- subst,metasenv,ugraph6)
- | C.Fix (i,fl) ->
- let fl_ty',subst,metasenv,types,ugraph1,len =
- List.fold_left
- (fun (fl,subst,metasenv,types,ugraph,len) (n,_,ty,_) ->
- let ty',_,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context ty ugraph
- in
- fl @ [ty'],subst',metasenv',
- Some (C.Name n,(C.Decl (CicSubstitution.lift len ty')))
- :: types, ugraph, len+1
- ) ([],subst,metasenv,[],ugraph,0) fl
- in
- let context' = types@context in
- let fl_bo',subst,metasenv,ugraph2 =
- List.fold_left
- (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
- let bo',ty_of_bo,subst,metasenv,ugraph1 =
- type_of_aux subst metasenv context' bo ugraph in
- let expected_ty = CicSubstitution.lift len ty in
- let subst',metasenv',ugraph' =
- try
- fo_unif_subst subst context' metasenv
- ty_of_bo expected_ty ugraph1
- with
- exn ->
- enrich localization_tbl bo exn
- ~f:(function _ ->
- lazy ("The term " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst bo
- context' ^ " has type " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
- context' ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
- context'))
- in
- fl @ [bo'] , subst',metasenv',ugraph'
- ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
- in
- let ty = List.nth fl_ty' i in
- (* now we have the new ty in fl_ty', the new bo in fl_bo',
- * and we want the new fl with bo' and ty' injected in the right
- * place.
- *)
- let rec map3 f l1 l2 l3 =
- match l1,l2,l3 with
- | [],[],[] -> []
- | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
- | _ -> assert false
- in
- let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
- fl_ty' fl_bo' fl
- in
- C.Fix (i,fl''),ty,subst,metasenv,ugraph2
- | C.CoFix (i,fl) ->
- let fl_ty',subst,metasenv,types,ugraph1,len =
- List.fold_left
- (fun (fl,subst,metasenv,types,ugraph,len) (n,ty,_) ->
- let ty',_,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context ty ugraph
- in
- fl @ [ty'],subst',metasenv',
- Some (C.Name n,(C.Decl (CicSubstitution.lift len ty'))) ::
- types, ugraph1, len+1
- ) ([],subst,metasenv,[],ugraph,0) fl
- in
- let context' = types@context in
- let fl_bo',subst,metasenv,ugraph2 =
- List.fold_left
- (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
- let bo',ty_of_bo,subst,metasenv,ugraph1 =
- type_of_aux subst metasenv context' bo ugraph in
- let expected_ty = CicSubstitution.lift len ty in
- let subst',metasenv',ugraph' =
- try
- fo_unif_subst subst context' metasenv
- ty_of_bo expected_ty ugraph1
- with
- exn ->
- enrich localization_tbl bo exn
- ~f:(function _ ->
- lazy ("The term " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst bo
- context' ^ " has type " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
- context' ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
- context))
- in
- fl @ [bo'],subst',metasenv',ugraph'
- ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
- in
- let ty = List.nth fl_ty' i in
- (* now we have the new ty in fl_ty', the new bo in fl_bo',
- * and we want the new fl with bo' and ty' injected in the right
- * place.
- *)
- let rec map3 f l1 l2 l3 =
- match l1,l2,l3 with
- | [],[],[] -> []
- | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
- | _ -> assert false
- in
- let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
- fl_ty' fl_bo' fl
- in
- C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
- in
- relocalize localization_tbl t t';
- res
-
- (* check_metasenv_consistency checks that the "canonical" context of a
- metavariable is consitent - up to relocation via the relocation list l -
- with the actual context *)
- and check_metasenv_consistency
- metano subst metasenv context canonical_context l ugraph
- =
- let module C = Cic in
- let module R = CicReduction in
- let module S = CicSubstitution in
- let lifted_canonical_context =
- let rec aux i =
- function
- [] -> []
- | (Some (n,C.Decl t))::tl ->
- (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
- | None::tl -> None::(aux (i+1) tl)
- | (Some (n,C.Def (t,ty)))::tl ->
- (Some
- (n,
- C.Def
- (S.subst_meta l (S.lift i t),
- S.subst_meta l (S.lift i ty)))) :: (aux (i+1) tl)
- in
- aux 1 canonical_context
- in
- try
- List.fold_left2
- (fun (l,subst,metasenv,ugraph) t ct ->
- match (t,ct) with
- _,None ->
- l @ [None],subst,metasenv,ugraph
- | Some t,Some (_,C.Def (ct,_)) ->
- (*CSC: the following optimization is to avoid a possibly
- expensive reduction that can be easily avoided and
- that is quite frequent. However, this is better
- handled using levels to control reduction *)
- let optimized_t =
- match t with
- Cic.Rel n ->
- (try
- match List.nth context (n - 1) with
- Some (_,C.Def (te,_)) -> S.lift n te
- | _ -> t
- with
- Failure _ -> t)
- | _ -> t
- in
- let subst',metasenv',ugraph' =
- (try
-(*prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e'
- * il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");*)
- fo_unif_subst subst context metasenv optimized_t ct ugraph
- with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm ~metasenv subst optimized_t) (CicMetaSubst.ppterm ~metasenv subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
- in
- l @ [Some t],subst',metasenv',ugraph'
- | Some t,Some (_,C.Decl ct) ->
- let t',inferredty,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context t ugraph
- in
- let subst'',metasenv'',ugraph2 =
- (try
- fo_unif_subst
- subst' context metasenv' inferredty ct ugraph1
- with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm metasenv' subst' inferredty) (CicMetaSubst.ppterm metasenv' subst' t) (CicMetaSubst.ppterm metasenv' subst' ct) (match e with AssertFailure msg -> Lazy.force msg | RefineFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
- in
- l @ [Some t'], subst'',metasenv'',ugraph2
- | None, Some _ ->
- raise (RefineFailure (lazy (sprintf "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s" (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))) ([],subst,metasenv,ugraph) l lifted_canonical_context
- with
- Invalid_argument _ ->
- raise
- (RefineFailure
- (lazy (sprintf
- "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
- (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l)))
- (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))
-
- and check_exp_named_subst metasubst metasenv context tl ugraph =
- let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
- match tl with
- [] -> [],metasubst,metasenv,ugraph
- | (uri,t)::tl ->
- let ty_uri,ugraph1 = type_of_variable uri ugraph in
- let typeofvar =
- CicSubstitution.subst_vars substs ty_uri in
- (* CSC: why was this code here? it is wrong
- (match CicEnvironment.get_cooked_obj ~trust:false uri with
- Cic.Variable (_,Some bo,_,_) ->
- raise
- (RefineFailure (lazy
- "A variable with a body can not be explicit substituted"))
- | Cic.Variable (_,None,_,_) -> ()
- | _ ->
- raise
- (RefineFailure (lazy
- ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
- ) ;
- *)
- let t',typeoft,metasubst',metasenv',ugraph2 =
- type_of_aux metasubst metasenv context t ugraph1 in
- let subst = uri,t' in
- let metasubst'',metasenv'',ugraph3 =
- try
- fo_unif_subst
- metasubst' context metasenv' typeoft typeofvar ugraph2
- with _ ->
- raise (RefineFailure (lazy
- ("Wrong Explicit Named Substitution: " ^
- CicMetaSubst.ppterm metasenv' metasubst' typeoft ^
- " not unifiable with " ^
- CicMetaSubst.ppterm metasenv' metasubst' typeofvar)))
- in
- (* FIXME: no mere tail recursive! *)
- let exp_name_subst, metasubst''', metasenv''', ugraph4 =
- check_exp_named_subst_aux
- metasubst'' metasenv'' (substs@[subst]) tl ugraph3
- in
- ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
- in
- check_exp_named_subst_aux metasubst metasenv [] tl ugraph
-
-
- and sort_of_prod localize subst metasenv context (name,s) t (t1, t2)
- ugraph
- =
- let module C = Cic in
- let context_for_t2 = (Some (name,C.Decl s))::context in
- let t1'' = CicReduction.whd ~subst context t1 in
- let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
- match (t1'', t2'') with
- | (C.Sort s1, C.Sort s2) when (s2 = C.Prop || s2 = C.Set) ->
- (* different than Coq manual!!! *)
- C.Sort s2,subst,metasenv,ugraph
- | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
- let t' = CicUniv.fresh() in
- (try
- let ugraph1 = CicUniv.add_ge t' t1 ugraph in
- let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
- C.Sort (C.Type t'),subst,metasenv,ugraph2
- with
- CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
- | (C.Sort (C.CProp t1), C.Sort (C.CProp t2)) ->
- let t' = CicUniv.fresh() in
- (try
- let ugraph1 = CicUniv.add_ge t' t1 ugraph in
- let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
- C.Sort (C.CProp t'),subst,metasenv,ugraph2
- with
- CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
- | (C.Sort (C.Type t1), C.Sort (C.CProp t2)) ->
- let t' = CicUniv.fresh() in
- (try
- let ugraph1 = CicUniv.add_ge t' t1 ugraph in
- let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
- C.Sort (C.CProp t'),subst,metasenv,ugraph2
- with
- CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
- | (C.Sort (C.CProp t1), C.Sort (C.Type t2)) ->
- let t' = CicUniv.fresh() in
- (try
- let ugraph1 = CicUniv.add_ge t' t1 ugraph in
- let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
- C.Sort (C.Type t'),subst,metasenv,ugraph2
- with
- CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
- | (C.Sort _,C.Sort (C.Type t1)) ->
- C.Sort (C.Type t1),subst,metasenv,ugraph
- | (C.Sort _,C.Sort (C.CProp t1)) ->
- C.Sort (C.CProp t1),subst,metasenv,ugraph
- | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
- | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
- (* TODO how can we force the meta to become a sort? If we don't we
- * break the invariant that refine produce only well typed terms *)
- (* TODO if we check the non meta term and if it is a sort then we
- * are likely to know the exact value of the result e.g. if the rhs
- * is a Sort (Prop | Set | CProp) then the result is the rhs *)
- let (metasenv,idx) =
- CicMkImplicit.mk_implicit_sort metasenv subst in
- let (subst, metasenv,ugraph1) =
- try
- fo_unif_subst subst context_for_t2 metasenv
- (C.Meta (idx,[])) t2'' ugraph
- with _ -> assert false (* unification against a metavariable *)
- in
- t2'',subst,metasenv,ugraph1
- | (C.Sort _,_)
- | (C.Meta _,_) ->
- enrich localization_tbl s
- (RefineFailure
- (lazy
- (sprintf
- "%s is supposed to be a type, but its type is %s"
- (CicMetaSubst.ppterm_in_context ~metasenv subst t context)
- (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context))))
- | _,_ ->
- enrich localization_tbl t
- (RefineFailure
- (lazy
- (sprintf
- "%s is supposed to be a type, but its type is %s"
- (CicMetaSubst.ppterm_in_context ~metasenv subst s context)
- (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context))))