- 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))))
-
- 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