- 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 localization_tbl 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))))
-
- and avoid_double_coercion context subst metasenv ugraph t ty =
- if not !pack_coercions then
- t,ty,subst,metasenv,ugraph
- else
- let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in
- if b then
- let source_carr = CoercGraph.source_of c2 in
- let tgt_carr = CicMetaSubst.apply_subst subst ty in
- (match CoercGraph.look_for_coercion metasenv subst context source_carr tgt_carr
- with
- | CoercGraph.SomeCoercion candidates ->
- let selected =
- HExtlib.list_findopt
- (function (metasenv,last,c) ->
- match c with
- | c when not (CoercGraph.is_composite c) ->
- debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
- None
- | c ->
- let subst,metasenv,ugraph =
- fo_unif_subst subst context metasenv last head ugraph in
- debug_print (lazy ("\nprovo" ^ CicPp.ppterm c));
- (try
- debug_print
- (lazy
- ("packing: " ^
- CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm c));
- let newt,_,subst,metasenv,ugraph =
- type_of_aux subst metasenv context c ugraph in
- debug_print (lazy "tipa...");
- let subst, metasenv, ugraph =
- (* COME MAI C'ERA UN IF su !pack_coercions ??? *)
- fo_unif_subst subst context metasenv newt t ugraph
- in
- debug_print (lazy "unifica...");
- Some (newt, ty, subst, metasenv, ugraph)
- with
- | RefineFailure s | Uncertain s when not !pack_coercions->
- debug_print s; debug_print (lazy "stop\n");None
- | RefineFailure s | Uncertain s ->
- debug_print s;debug_print (lazy "goon\n");
- try
- let old_pack_coercions = !pack_coercions in
- pack_coercions := false; (* to avoid diverging *)
- let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
- type_of_aux subst metasenv context c1_c2_implicit ugraph
- in
- pack_coercions := old_pack_coercions;
- let b, _, _, _, _ =
- is_a_double_coercion refined_c1_c2_implicit
- in
- if b then
- None
- else
- let head' =
- match refined_c1_c2_implicit with
- | Cic.Appl l -> HExtlib.list_last l
- | _ -> assert false
- in
- let subst, metasenv, ugraph =
- try fo_unif_subst subst context metasenv
- head head' ugraph
- with RefineFailure s| Uncertain s->
- debug_print s;assert false
- in
- let subst, metasenv, ugraph =
- fo_unif_subst subst context metasenv
- refined_c1_c2_implicit t ugraph
- in
- Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph)
- with
- | RefineFailure s | Uncertain s ->
- pack_coercions := true;debug_print s;None
- | exn -> pack_coercions := true; raise exn))
- candidates
- in
- (match selected with
- | Some x -> x
- | None ->
- debug_print
- (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
- t, ty, subst, metasenv, ugraph)
- | _ -> t, ty, subst, metasenv, ugraph)
- else
- t, ty, subst, metasenv, ugraph
-
- and typeof_list subst metasenv context ugraph l =
- let tlbody_and_type,subst,metasenv,ugraph =
- List.fold_right
- (fun x (res,subst,metasenv,ugraph) ->
- let x',ty,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context x ugraph
- in
- (x', ty)::res,subst',metasenv',ugraph1
- ) l ([],subst,metasenv,ugraph)
- in
- tlbody_and_type,subst,metasenv,ugraph
-
- and eat_prods
- allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph
- =
- (* given he:hety, gives beack all (c he) such that (c e):?->? *)
- let fix_arity n metasenv context subst he hetype ugraph =
- let hetype = CicMetaSubst.apply_subst subst hetype in
- (* instead of a dummy functional type we may create the real product
- * using args_bo_and_ty, but since coercions lookup ignores the
- * actual ariety we opt for the simple solution *)
- let fty = Cic.Prod(Cic.Anonymous, Cic.Sort Cic.Prop, Cic.Sort Cic.Prop) in
- match CoercGraph.look_for_coercion metasenv subst context hetype fty with
- | CoercGraph.NoCoercion -> []
- | CoercGraph.NotHandled ->
- raise (MoreArgsThanExpected (n,Uncertain (lazy "")))
- | CoercGraph.SomeCoercionToTgt candidates
- | CoercGraph.SomeCoercion candidates ->
- HExtlib.filter_map
- (fun (metasenv,last,coerc) ->
- let pp t =
- CicMetaSubst.ppterm_in_context ~metasenv subst t context in
- try
- let subst,metasenv,ugraph =
- fo_unif_subst subst context metasenv last he ugraph in
- debug_print (lazy ("New head: "^ pp coerc));
- let tty,ugraph =
- CicTypeChecker.type_of_aux' ~subst metasenv context coerc
- ugraph
- in
- debug_print (lazy (" has type: "^ pp tty));
- Some (coerc,tty,subst,metasenv,ugraph)
- with
- | Uncertain _ | RefineFailure _
- | HExtlib.Localized (_,Uncertain _)
- | HExtlib.Localized (_,RefineFailure _) -> None
- | exn -> assert false)
- candidates
- in
- (* aux function to process the type of the head and the args in parallel *)
- let rec eat_prods_and_args metasenv subst context he hetype ugraph newargs =
- function
- | [] -> newargs,subst,metasenv,he,hetype,ugraph
- | (hete, hety)::tl as args ->
- match (CicReduction.whd ~subst context hetype) with
- | Cic.Prod (n,s,t) ->
- let arg,subst,metasenv,ugraph =
- coerce_to_something allow_coercions localization_tbl
- hete hety s subst metasenv context ugraph in
- eat_prods_and_args
- metasenv subst context he (CicSubstitution.subst (fst arg) t)
- ugraph (newargs@[arg]) tl
- | _ ->
- let he =
- match he, newargs with
- | _, [] -> he
- | Cic.Appl l, _ -> Cic.Appl (l@List.map fst newargs)
- | _ -> Cic.Appl (he::List.map fst newargs)
- in
- (*{{{*) debug_print (lazy
- let pp x =
- CicMetaSubst.ppterm_in_context ~metasenv subst x context in
- "Fixing arity of: "^ pp he ^ "\n that has type: "^ pp hetype^
- "\n but is applyed to: " ^ String.concat ";"
- (List.map (fun (t,_)->pp t) args_bo_and_ty)); (*}}}*)
- let possible_fixes =
- fix_arity (List.length args) metasenv context subst he hetype
- ugraph in
- match
- HExtlib.list_findopt
- (fun (he,hetype,subst,metasenv,ugraph) ->
- (* {{{ *)debug_print (lazy ("Try fix: "^
- CicMetaSubst.ppterm_in_context ~metasenv subst he context));
- debug_print (lazy (" of type: "^
- CicMetaSubst.ppterm_in_context
- ~metasenv subst hetype context)); (* }}} *)
- try
- Some (eat_prods_and_args
- metasenv subst context he hetype ugraph [] args)
- with
- | RefineFailure _ | Uncertain _
- | HExtlib.Localized (_,RefineFailure _)
- | HExtlib.Localized (_,Uncertain _) -> None)
- possible_fixes
- with
- | Some x -> x
- | None ->
- raise
- (MoreArgsThanExpected
- (List.length args, RefineFailure (lazy "")))
- in
- (* first we check if we are in the simple case of a meta closed term *)
- let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
- if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then
- (* this optimization is to postpone fix_arity (the most common case)*)
- subst,metasenv,ugraph,hetype,he,args_bo_and_ty
- else
- (* this (says CSC) is also useful to infer dependent types *)
- let pristinemenv = metasenv in
- let metasenv,hetype' =
- mk_prod_of_metas metasenv context subst args_bo_and_ty