From b26c4349ed1401d2ac9904deb47efbd4c454d98e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 19 Jan 2005 16:03:27 +0000 Subject: [PATCH] coercion application --- helm/ocaml/cic_unification/cicRefine.ml | 418 +++++++++++++++--------- 1 file changed, 267 insertions(+), 151 deletions(-) diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 566a531cc..24171327c 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -46,6 +46,23 @@ let rec split l n = | (_,_) -> raise (AssertFailure "split: list too short") ;; +let look_for_coercion src tgt = + if (src = (CicUtil.term_of_uri "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)")) && + (tgt = (CicUtil.term_of_uri "cic:/Coq/Reals/Rdefinitions/R.con")) + then + begin + prerr_endline "TROVATA coercion"; + Some (CicUtil.term_of_uri "cic://Coq/Reals/Raxioms/INR.con") + end + else + begin + prerr_endline (sprintf "NON TROVATA la coercion %s %s" (CicPp.ppterm src) + (CicPp.ppterm tgt)); + None + end +;; + + let rec type_of_constant uri ugraph = let module C = Cic in let module R = CicReduction in @@ -175,8 +192,10 @@ and type_of_aux' metasenv context t ugraph = C.Rel n -> (try match List.nth context (n - 1) with - Some (_,C.Decl t) -> S.lift n t,subst,metasenv, ugraph - | Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv, ugraph + Some (_,C.Decl ty) -> + t,S.lift n ty,subst,metasenv, ugraph + | Some (_,C.Def (_,Some ty)) -> + t,S.lift n ty,subst,metasenv, ugraph | Some (_,C.Def (bo,None)) -> type_of_aux subst metasenv context (S.lift n bo) ugraph | None -> raise (RefineFailure "Rel to hidden hypothesis") @@ -184,61 +203,74 @@ and type_of_aux' metasenv context t ugraph = _ -> raise (RefineFailure "Not a close term") ) | C.Var (uri,exp_named_subst) -> - let subst',metasenv',ugraph1 = - check_exp_named_subst subst metasenv context exp_named_subst ugraph in - let ty_uri,ugraph1 = type_of_variable uri ugraph in - + let exp_named_subst',subst',metasenv',ugraph1 = + check_exp_named_subst + subst metasenv context exp_named_subst ugraph + in + let ty_uri,ugraph1 = type_of_variable uri ugraph in let ty = - CicSubstitution.subst_vars exp_named_subst ty_uri + CicSubstitution.subst_vars exp_named_subst' ty_uri in - ty,subst',metasenv',ugraph1 + C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1 | C.Meta (n,l) -> (try - let (canonical_context, term,ty) = CicUtil.lookup_subst n subst in - let subst,metasenv,ugraph1 = + let (canonical_context, term,ty) = + CicUtil.lookup_subst n subst + in + let l',subst',metasenv',ugraph1 = check_metasenv_consistency n subst metasenv context canonical_context l ugraph in (* trust or check ??? *) - CicSubstitution.lift_meta l ty, subst, metasenv, ugraph1 + C.Meta (n,l'),CicSubstitution.lift_meta l' ty, + subst', metasenv', ugraph1 (* type_of_aux subst metasenv context (CicSubstitution.lift_meta l term) *) with CicUtil.Subst_not_found _ -> let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in - let subst,metasenv, ugraph1 = + let l',subst',metasenv', ugraph1 = check_metasenv_consistency n subst metasenv context canonical_context l ugraph in - CicSubstitution.lift_meta l ty, subst, metasenv,ugraph1) - (* TASSI: CONSTRAINT *) - | C.Sort (C.Type t) -> - let t' = CicUniv.fresh() in - let ugraph1 = CicUniv.add_gt t' t ugraph in - (C.Sort (C.Type t')),subst,metasenv,ugraph1 - (* TASSI: CONSTRAINT *) - | C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph + C.Meta (n,l'),CicSubstitution.lift_meta l' ty, + subst', metasenv',ugraph1) + | C.Sort (C.Type tno) -> + let tno' = CicUniv.fresh() in + let ugraph1 = CicUniv.add_gt tno' tno ugraph in + t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1 + | C.Sort _ -> + t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph | C.Implicit _ -> raise (AssertFailure "21") | C.Cast (te,ty) -> - let _,subst',metasenv',ugraph1 = - type_of_aux subst metasenv context ty ugraph in - let inferredty,subst'',metasenv'',ugraph2 = + let ty',_,subst',metasenv',ugraph1 = + type_of_aux subst metasenv context ty ugraph + in + let te',inferredty,subst'',metasenv'',ugraph2 = type_of_aux subst' metasenv' context te ugraph1 in (try let subst''',metasenv''',ugraph3 = - fo_unif_subst subst'' context metasenv'' inferredty ty ugraph2 + fo_unif_subst subst'' context metasenv'' + inferredty ty' ugraph2 in - ty,subst''',metasenv''',ugraph3 + C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3 with _ -> raise (RefineFailure "Cast")) | C.Prod (name,s,t) -> - let sort1,subst',metasenv',ugraph1 = type_of_aux subst metasenv context s ugraph in - let sort2,subst'',metasenv'',ugraph2 = - type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) t ugraph1 + let s',sort1,subst',metasenv',ugraph1 = + type_of_aux subst metasenv context s ugraph + in + let t',sort2,subst'',metasenv'',ugraph2 = + type_of_aux subst' metasenv' + ((Some (name,(C.Decl s')))::context) t ugraph1 in - sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2) ugraph2 + let sop,subst''',metasenv''',ugraph3 = + sort_of_prod subst'' metasenv'' + context (name,s') (sort1,sort2) ugraph2 + in + C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3 | C.Lambda (n,s,t) -> - let sort1,subst',metasenv',ugraph1 = + let s',sort1,subst',metasenv',ugraph1 = type_of_aux subst metasenv context s ugraph in (match CicReduction.whd ~subst:subst' context sort1 with @@ -250,61 +282,80 @@ and type_of_aux' metasenv context t ugraph = instead it is a term of type %s" (CicPp.ppterm s) (CicPp.ppterm sort1))) ) ; - let type2,subst'',metasenv'',ugraph2 = - type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t ugraph1 + let t',type2,subst'',metasenv'',ugraph2 = + type_of_aux subst' metasenv' + ((Some (n,(C.Decl s')))::context) t ugraph1 in - C.Prod (n,s,type2),subst'',metasenv'',ugraph2 + C.Lambda (n,s',t'),C.Prod (n,s',type2), + subst'',metasenv'',ugraph2 | C.LetIn (n,s,t) -> (* only to check if s is well-typed *) - let ty,subst',metasenv',ugraph1 = + let s',ty,subst',metasenv',ugraph1 = type_of_aux subst metasenv context s ugraph in - let inferredty,subst'',metasenv'',ugraph2 = - type_of_aux subst' metasenv' ((Some (n,(C.Def (s,Some ty))))::context) t ugraph1 + let t',inferredty,subst'',metasenv'',ugraph2 = + type_of_aux subst' metasenv' + ((Some (n,(C.Def (s',Some ty))))::context) t ugraph1 in - (* One-step LetIn reduction. Even faster than the previous solution. - Moreover the inferred type is closer to the expected one. *) - CicSubstitution.subst s inferredty,subst',metasenv',ugraph2 + (* One-step LetIn reduction. + * Even faster than the previous solution. + * Moreover the inferred type is closer to the expected one. + *) + C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty, + subst',metasenv',ugraph2 | C.Appl (he::((_::_) as tl)) -> - let hetype,subst',metasenv',ugraph1 = + let he',hetype,subst',metasenv',ugraph1 = type_of_aux subst metasenv context he ugraph in let tlbody_and_type,subst'',metasenv'',ugraph2 = List.fold_right (fun x (res,subst,metasenv,ugraph) -> - let ty,subst',metasenv',ugraph1 = + let x',ty,subst',metasenv',ugraph1 = type_of_aux subst metasenv context x ugraph in - (x, ty)::res,subst',metasenv',ugraph1 + (x', ty)::res,subst',metasenv',ugraph1 ) tl ([],subst',metasenv',ugraph1) in - eat_prods subst'' metasenv'' context hetype tlbody_and_type ugraph2 + let tl',applty,subst''',metasenv''',ugraph3 = + eat_prods subst'' metasenv'' context + hetype tlbody_and_type ugraph2 + in + C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3 | C.Appl _ -> raise (RefineFailure "Appl: no arguments") | C.Const (uri,exp_named_subst) -> - let subst',metasenv',ugraph1 = - check_exp_named_subst subst metasenv context exp_named_subst ugraph in + let exp_named_subst',subst',metasenv',ugraph1 = + check_exp_named_subst subst metasenv context + exp_named_subst ugraph in let ty_uri,ugraph2 = type_of_constant uri ugraph1 in let cty = - CicSubstitution.subst_vars exp_named_subst ty_uri + CicSubstitution.subst_vars exp_named_subst' ty_uri in - cty,subst',metasenv',ugraph2 + C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2 | C.MutInd (uri,i,exp_named_subst) -> - let subst',metasenv',ugraph1 = - check_exp_named_subst subst metasenv context exp_named_subst ugraph + let exp_named_subst',subst',metasenv',ugraph1 = + check_exp_named_subst subst metasenv context + exp_named_subst ugraph in let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in let cty = - CicSubstitution.subst_vars exp_named_subst ty_uri in - cty,subst',metasenv',ugraph2 + CicSubstitution.subst_vars exp_named_subst' ty_uri in + C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2 | C.MutConstruct (uri,i,j,exp_named_subst) -> - let subst',metasenv',ugraph1 = - check_exp_named_subst subst metasenv context exp_named_subst ugraph in - let ty_uri,ugraph2 = type_of_mutual_inductive_constr uri i j ugraph1 in + let exp_named_subst',subst',metasenv',ugraph1 = + check_exp_named_subst subst metasenv context + exp_named_subst ugraph + in + let ty_uri,ugraph2 = + type_of_mutual_inductive_constr uri i j ugraph1 + in let cty = - CicSubstitution.subst_vars exp_named_subst ty_uri in - cty,subst',metasenv',ugraph2 + CicSubstitution.subst_vars exp_named_subst' ty_uri + in + C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst', + metasenv',ugraph2 | C.MutCase (uri, i, outtype, term, pl) -> - (* first, get the inductive type (and noparams) in the environment *) + (* first, get the inductive type (and noparams) + * in the environment *) let (_,b,arity,constructors), expl_params, no_left_params,ugraph = (* let obj = @@ -320,66 +371,79 @@ and type_of_aux' metasenv context t ugraph = | _ -> raise (RefineFailure - ("Unkown mutual inductive definition " ^ U.string_of_uri uri)) in + ("Unkown mutual inductive definition " ^ + U.string_of_uri uri)) + in let rec count_prod t = match CicReduction.whd ~subst context t with C.Prod (_, _, t) -> 1 + (count_prod t) - | _ -> 0 in + | _ -> 0 + in let no_args = count_prod arity in (* now, create a "generic" MutInd *) let metasenv,left_args = - CicMkImplicit.n_fresh_metas metasenv subst context no_left_params in + CicMkImplicit.n_fresh_metas metasenv subst context no_left_params + in let metasenv,right_args = let no_right_params = no_args - no_left_params in if no_right_params < 0 then assert false - else CicMkImplicit.n_fresh_metas metasenv subst context no_right_params in + else CicMkImplicit.n_fresh_metas + metasenv subst context no_right_params + in let metasenv,exp_named_subst = CicMkImplicit.fresh_subst metasenv subst context expl_params in let expected_type = if no_args = 0 then C.MutInd (uri,i,exp_named_subst) else - C.Appl (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args)) + C.Appl + (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args)) in (* check consistency with the actual type of term *) - let actual_type,subst,metasenv,ugraph1 = + let term',actual_type,subst,metasenv,ugraph1 = type_of_aux subst metasenv context term ugraph in - let _, subst, metasenv,ugraph2 = + let expected_type',_, subst, metasenv,ugraph2 = type_of_aux subst metasenv context expected_type ugraph1 in let actual_type = CicReduction.whd ~subst context actual_type in let subst,metasenv,ugraph3 = - fo_unif_subst subst context metasenv expected_type actual_type ugraph2 + fo_unif_subst subst context metasenv + expected_type' actual_type ugraph2 in - (* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *) - let (_,outtypeinstances,subst,metasenv,ugraph4) = + (* TODO: check if the sort elimination + * is allowed: [(I q1 ... qr)|B] *) + let (pl',_,outtypeinstances,subst,metasenv,ugraph4) = List.fold_left - (fun (j,outtypeinstances,subst,metasenv,ugraph) p -> + (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p -> let constructor = if left_args = [] then (C.MutConstruct (uri,i,j,exp_named_subst)) else (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::left_args)) in - let actual_type,subst,metasenv,ugraph1 = - type_of_aux subst metasenv context p ugraph in - let expected_type, subst, metasenv,ugraph2 = - type_of_aux subst metasenv context constructor ugraph1 in + let p',actual_type,subst,metasenv,ugraph1 = + type_of_aux subst metasenv context p ugraph + in + let constructor',expected_type, subst, metasenv,ugraph2 = + type_of_aux subst metasenv context constructor ugraph1 + in let outtypeinstance,subst,metasenv,ugraph3 = - check_branch - 0 context metasenv subst - no_left_params actual_type constructor expected_type ugraph2 in - (j+1,outtypeinstance::outtypeinstances,subst,metasenv,ugraph3)) - (1,[],subst,metasenv,ugraph3) pl in + check_branch 0 context metasenv subst no_left_params + actual_type constructor expected_type ugraph2 + in + (pl @ [p'],j+1, + outtypeinstance::outtypeinstances,subst,metasenv,ugraph3)) + ([],1,[],subst,metasenv,ugraph3) pl + in (* we are left to check that the outype matches his instances. The easy case is when the outype is specified, that amount to a trivial check. Otherwise, we should guess a type from its instances *) (* easy case *) - let _, subst, metasenv,ugraph5 = + let _,_, subst, metasenv,ugraph5 = type_of_aux subst metasenv context - (C.Appl ((outtype :: right_args) @ [term])) ugraph4 + (C.Appl ((outtype :: right_args) @ [term'])) ugraph4 in let (subst,metasenv,ugraph6) = List.fold_left @@ -410,53 +474,96 @@ and type_of_aux' metasenv context t ugraph = (* CicMetaSubst.whd subst context appl *) CicReduction.whd ~subst context appl in - fo_unif_subst subst context metasenv instance instance' ugraph) - (subst,metasenv,ugraph5) outtypeinstances in - CicReduction.whd ~subst - context (C.Appl(outtype::right_args@[term])),subst,metasenv,ugraph6 + fo_unif_subst subst context metasenv + instance instance' ugraph) + (subst,metasenv,ugraph5) outtypeinstances + in + C.MutCase (uri, i, outtype, term', pl'), + CicReduction.whd ~subst context + (C.Appl(outtype::right_args@[term])), + subst,metasenv,ugraph6 | C.Fix (i,fl) -> - let subst,metasenv,types,ugraph1 = + let fl_ty',subst,metasenv,types,ugraph1 = List.fold_left - (fun (subst,metasenv,types,ugraph) (n,_,ty,_) -> - let _,subst',metasenv',ugraph1 = type_of_aux subst metasenv context ty ugraph in - subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types, ugraph - ) (subst,metasenv,[],ugraph) fl + (fun (fl,subst,metasenv,types,ugraph) (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 ty')) :: types, ugraph + ) ([],subst,metasenv,[],ugraph) fl in let len = List.length types in let context' = types@context in - let subst,metasenv,ugraph2 = + let fl_bo',subst,metasenv,ugraph2 = List.fold_left - (fun (subst,metasenv,ugraph) (name,x,ty,bo) -> - let ty_of_bo,subst,metasenv,ugraph1 = + (fun (fl,subst,metasenv,ugraph) (name,x,ty,bo) -> + let bo',ty_of_bo,subst,metasenv,ugraph1 = type_of_aux subst metasenv context' bo ugraph in + let subst',metasenv',ugraph' = fo_unif_subst subst context' metasenv ty_of_bo (CicSubstitution.lift len ty) ugraph1 - ) (subst,metasenv,ugraph1) fl in + in + fl @ [bo'] , subst',metasenv',ugraph' + ) ([],subst,metasenv,ugraph1) fl + in let (_,_,ty,_) = List.nth fl i in - ty,subst,metasenv,ugraph2 + (* 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 subst,metasenv,types,ugraph1 = + let fl_ty',subst,metasenv,types,ugraph1 = List.fold_left - (fun (subst,metasenv,types,ugraph) (n,ty,_) -> - let _,subst',metasenv',ugraph1 = type_of_aux subst metasenv context ty ugraph in - subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types, ugraph1 - ) (subst,metasenv,[],ugraph) fl + (fun (fl,subst,metasenv,types,ugraph) (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 ty')) :: types, ugraph1 + ) ([],subst,metasenv,[],ugraph) fl in let len = List.length types in let context' = types@context in - let subst,metasenv,ugraph2 = + let fl_bo',subst,metasenv,ugraph2 = List.fold_left - (fun (subst,metasenv,ugraph) (name,ty,bo) -> - let ty_of_bo,subst,metasenv,ugraph1 = + (fun (fl,subst,metasenv,ugraph) (name,ty,bo) -> + let bo',ty_of_bo,subst,metasenv,ugraph1 = type_of_aux subst metasenv context' bo ugraph in + let subst',metasenv',ugraph' = fo_unif_subst subst context' metasenv - ty_of_bo (CicSubstitution.lift len ty) ugraph1 - ) (subst,metasenv,ugraph1) fl in - + ty_of_bo (CicSubstitution.lift len ty) ugraph1 + in + fl @ [bo'],subst',metasenv',ugraph' + ) ([],subst,metasenv,ugraph1) fl + in let (_,ty,_) = List.nth fl i in - ty,subst,metasenv,ugraph2 + (* 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 (* check_metasenv_consistency checks that the "canonical" context of a metavariable is consitent - up to relocation via the relocation list l - @@ -485,28 +592,34 @@ and type_of_aux' metasenv context t ugraph = in try List.fold_left2 - (fun (subst,metasenv,ugraph) t ct -> + (fun (l,subst,metasenv,ugraph) t ct -> match (t,ct) with _,None -> - subst,metasenv,ugraph + l @ [None],subst,metasenv,ugraph | Some t,Some (_,C.Def (ct,_)) -> + let subst',metasenv',ugraph' = (try fo_unif_subst subst context metasenv t ct ugraph with e -> raise (RefineFailure (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct) (match e with AssertFailure msg -> msg | _ -> (Printexc.to_string e))))) + in + l @ [Some t],subst',metasenv',ugraph' | Some t,Some (_,C.Decl ct) -> - let inferredty,subst',metasenv',ugraph1 = + 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 (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 subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with AssertFailure msg -> msg | _ -> (Printexc.to_string e))))) + in + l @ [Some t'], subst'',metasenv'',ugraph2 | None, Some _ -> raise (RefineFailure (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 subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext subst canonical_context))) - ) (subst,metasenv,ugraph) l lifted_canonical_context + ) ([],subst,metasenv,ugraph) l lifted_canonical_context with Invalid_argument _ -> raise @@ -519,7 +632,7 @@ and type_of_aux' metasenv context t ugraph = 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 + [] -> [],metasubst,metasenv,ugraph | ((uri,t) as subst)::tl -> let ty_uri,ugraph1 = type_of_variable uri ugraph in let typeofvar = @@ -537,18 +650,26 @@ and type_of_aux' metasenv context t ugraph = ("Unkown variable definition " ^ UriManager.string_of_uri uri)) ) ; *) - let typeoft,metasubst',metasenv',ugraph2 = + let t',typeoft,metasubst',metasenv',ugraph2 = type_of_aux metasubst metasenv context t ugraph1 in let metasubst'',metasenv'',ugraph3 = try - fo_unif_subst metasubst' context metasenv' typeoft typeofvar ugraph2 + fo_unif_subst + metasubst' context metasenv' typeoft typeofvar ugraph2 with _ -> raise (RefineFailure - ("Wrong Explicit Named Substitution: " ^ CicMetaSubst.ppterm metasubst' typeoft ^ - " not unifiable with " ^ CicMetaSubst.ppterm metasubst' typeofvar)) + ("Wrong Explicit Named Substitution: " ^ + CicMetaSubst.ppterm metasubst' typeoft ^ + " not unifiable with " ^ + CicMetaSubst.ppterm 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 - check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl ugraph3 + ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4 in check_exp_named_subst_aux metasubst metasenv [] tl ugraph @@ -594,13 +715,17 @@ and type_of_aux' metasenv context t ugraph = let rec mk_prod metasenv context = function [] -> - let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv subst context in + let (metasenv, idx) = + CicMkImplicit.mk_implicit_type metasenv subst context + in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in metasenv,Cic.Meta (idx, irl) | (_,argty)::tl -> - let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv subst context in + let (metasenv, idx) = + CicMkImplicit.mk_implicit_type metasenv subst context + in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in @@ -643,57 +768,48 @@ and type_of_aux' metasenv context t ugraph = in let rec eat_prods metasenv subst context hetype ugraph = function - [] -> metasenv,subst,hetype,ugraph + | [] -> [],metasenv,subst,hetype,ugraph | (hete, hety)::tl -> (match hetype with Cic.Prod (n,s,t) -> - let subst,metasenv,ugraph1 = + let arg,subst,metasenv,ugraph1 = try - fo_unif_subst subst context metasenv hety s ugraph + let subst,metasenv,ugraph1 = + fo_unif_subst subst context metasenv hety s ugraph + in + hete,subst,metasenv,ugraph1 with exn -> - prerr_endline (Printf.sprintf "hety=%s\ns=%s\nmetasenv=%s" - (CicMetaSubst.ppterm subst hety) - (CicMetaSubst.ppterm subst s) - (CicMetaSubst.ppmetasenv metasenv subst)); - raise exn - - (* - try - fo_unif_subst subst context metasenv hety s - with _ -> - prerr_endline("senza subst fallisce"); - let hety = CicMetaSubst.apply_subst subst hety in - let s = CicMetaSubst.apply_subst subst s in - prerr_endline ("unifico = " ^(CicPp.ppterm hety)); - prerr_endline ("con = " ^(CicPp.ppterm s)); - fo_unif_subst subst context metasenv hety s *) + (* we search a coercion from hety to s *) + let coer = look_for_coercion + (CicMetaSubst.apply_subst subst hety) + (CicMetaSubst.apply_subst subst s) + in + match coer with + | None -> raise exn + | Some c -> + (Cic.Appl [ c ; hete ]), subst, metasenv, ugraph in - (* DEBUG - let t1 = CicMetaSubst.subst subst hete t in - let t2 = CicSubstitution.subst hete t in - prerr_endline ("con subst = " ^(CicPp.ppterm t1)); - prerr_endline ("senza subst = " ^(CicPp.ppterm t2)); - prerr_endline("++++++++++metasenv prima di eat_prods:\n" ^ - (CicMetaSubst.ppmetasenv metasenv subst)); - prerr_endline("++++++++++subst prima di eat_prods:\n" ^ - (CicMetaSubst.ppsubst subst)); - *) + let coerced_args,metasenv',subst',t',ugraph2 = eat_prods metasenv subst context (* (CicMetaSubst.subst subst hete t) tl *) (CicSubstitution.subst hete t) ugraph1 tl + in + arg::coerced_args,metasenv',subst',t',ugraph2 | _ -> assert false ) in - let metasenv,subst,t,ugraph2 = + let coerced_args,metasenv,subst,t,ugraph2 = eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type in - t,subst,metasenv,ugraph2 - (* eat prods ends here! *) + coerced_args,t,subst,metasenv,ugraph2 in - let ty,subst',metasenv',ugraph1 = + + (* eat prods ends here! *) + + let t',ty,subst',metasenv',ugraph1 = type_of_aux [] metasenv context t ugraph in - let substituted_t = CicMetaSubst.apply_subst subst' t in + let substituted_t = CicMetaSubst.apply_subst subst' t' in let substituted_ty = CicMetaSubst.apply_subst subst' ty in (* Andrea: ho rimesso qui l'applicazione della subst al metasenv dopo che ho droppato l'invariante che il metsaenv -- 2.39.2