From 3ef2bf19b2b0f3542f453f48f30d13c6d8be09a0 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 29 Nov 2004 12:24:09 +0000 Subject: [PATCH] - pass subst to FreshNameGenerator on mk_fresh_name invocations - removed assert failures on get_cooked_obj (rolled back last commit) - reindented (the huuuuuuuge) eat_prods function --- helm/ocaml/cic_unification/cicRefine.ml | 1280 +++++++++++------------ 1 file changed, 630 insertions(+), 650 deletions(-) diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 0f751b996..d778ff59f 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -47,73 +47,81 @@ let rec split l n = ;; let rec type_of_constant uri = - let module C = Cic in - let module R = CicReduction in - let module U = UriManager in - let obj = - try - CicEnvironment.get_cooked_obj uri - with Not_found -> assert false - in - match obj with - C.Constant (_,_,ty,_) -> ty - | C.CurrentProof (_,_,_,ty,_) -> ty - | _ -> - raise - (RefineFailure ("Unknown constant definition " ^ U.string_of_uri uri)) + let module C = Cic in + let module R = CicReduction in + let module U = UriManager in + (* + let obj = + try + CicEnvironment.get_cooked_obj uri + with Not_found -> assert false + in + *) + match CicEnvironment.get_obj uri with + C.Constant (_,_,ty,_) -> ty + | C.CurrentProof (_,_,_,ty,_) -> ty + | _ -> + raise + (RefineFailure ("Unknown constant definition " ^ U.string_of_uri uri)) and type_of_variable uri = - let module C = Cic in - let module R = CicReduction in - let module U = UriManager in - let obj = - try - CicEnvironment.get_cooked_obj uri - with Not_found -> assert false - in - match obj with - C.Variable (_,_,ty,_) -> ty - | _ -> - raise - (RefineFailure - ("Unknown variable definition " ^ UriManager.string_of_uri uri)) + let module C = Cic in + let module R = CicReduction in + let module U = UriManager in + (* + let obj = + try + CicEnvironment.get_cooked_obj uri + with Not_found -> assert false + in + *) + match CicEnvironment.get_obj uri with + C.Variable (_,_,ty,_) -> ty + | _ -> + raise + (RefineFailure + ("Unknown variable definition " ^ UriManager.string_of_uri uri)) and type_of_mutual_inductive_defs uri i = - let module C = Cic in - let module R = CicReduction in - let module U = UriManager in - let obj = - try - CicEnvironment.get_cooked_obj uri - with Not_found -> assert false - in - match obj with - C.InductiveDefinition (dl,_,_) -> - let (_,_,arity,_) = List.nth dl i in - arity - | _ -> - raise - (RefineFailure - ("Unknown mutual inductive definition " ^ U.string_of_uri uri)) + let module C = Cic in + let module R = CicReduction in + let module U = UriManager in + (* + let obj = + try + CicEnvironment.get_cooked_obj uri + with Not_found -> assert false + in + *) + match CicEnvironment.get_obj uri with + C.InductiveDefinition (dl,_,_) -> + let (_,_,arity,_) = List.nth dl i in + arity + | _ -> + raise + (RefineFailure + ("Unknown mutual inductive definition " ^ U.string_of_uri uri)) and type_of_mutual_inductive_constr uri i j = - let module C = Cic in - let module R = CicReduction in - let module U = UriManager in - let obj = - try - CicEnvironment.get_cooked_obj uri - with Not_found -> assert false - in - match obj with - C.InductiveDefinition (dl,_,_) -> - let (_,_,_,cl) = List.nth dl i in - let (_,ty) = List.nth cl (j-1) in - ty - | _ -> - raise - (RefineFailure - ("Unkown mutual inductive definition " ^ U.string_of_uri uri)) + let module C = Cic in + let module R = CicReduction in + let module U = UriManager in + (* + let obj = + try + CicEnvironment.get_cooked_obj uri + with Not_found -> assert false + in + *) + match CicEnvironment.get_obj uri with + C.InductiveDefinition (dl,_,_) -> + let (_,_,_,cl) = List.nth dl i in + let (_,ty) = List.nth cl (j-1) in + ty + | _ -> + raise + (RefineFailure + ("Unkown mutual inductive definition " ^ U.string_of_uri uri)) (* type_of_aux' is just another name (with a different scope) for type_of_aux *) @@ -124,621 +132,593 @@ and type_of_mutual_inductive_constr uri i j = The problem is that outype is in general unknown, and we should try to synthesize it from the above information, that is in general a second order unification problem. *) - + and check_branch n context metasenv subst left_args_no actualtype term expectedtype = let module C = Cic in - (* let module R = CicMetaSubst in *) + (* let module R = CicMetaSubst in *) let module R = CicReduction in - match R.whd ~subst context expectedtype with - C.MutInd (_,_,_) -> - (n,context,actualtype, [term]), subst, metasenv - | C.Appl (C.MutInd (_,_,_)::tl) -> - let (_,arguments) = split tl left_args_no in - (n,context,actualtype, arguments@[term]), subst, metasenv - | C.Prod (name,so,de) -> - (* we expect that the actual type of the branch has the due - number of Prod *) - (match R.whd ~subst context actualtype with - C.Prod (name',so',de') -> - let subst, metasenv = - fo_unif_subst subst context metasenv so so' in - let term' = - (match CicSubstitution.lift 1 term with - C.Appl l -> C.Appl (l@[C.Rel 1]) - | t -> C.Appl [t ; C.Rel 1]) in - (* we should also check that the name variable is anonymous in - the actual type de' ?? *) - check_branch (n+1) ((Some (name,(C.Decl so)))::context) metasenv subst left_args_no de' term' de - | _ -> raise (AssertFailure "Wrong number of arguments")) - | _ -> raise (AssertFailure "Prod or MutInd expected") + match R.whd ~subst context expectedtype with + C.MutInd (_,_,_) -> + (n,context,actualtype, [term]), subst, metasenv + | C.Appl (C.MutInd (_,_,_)::tl) -> + let (_,arguments) = split tl left_args_no in + (n,context,actualtype, arguments@[term]), subst, metasenv + | C.Prod (name,so,de) -> + (* we expect that the actual type of the branch has the due + number of Prod *) + (match R.whd ~subst context actualtype with + C.Prod (name',so',de') -> + let subst, metasenv = + fo_unif_subst subst context metasenv so so' in + let term' = + (match CicSubstitution.lift 1 term with + C.Appl l -> C.Appl (l@[C.Rel 1]) + | t -> C.Appl [t ; C.Rel 1]) in + (* we should also check that the name variable is anonymous in + the actual type de' ?? *) + check_branch (n+1) ((Some (name,(C.Decl so)))::context) metasenv subst left_args_no de' term' de + | _ -> raise (AssertFailure "Wrong number of arguments")) + | _ -> raise (AssertFailure "Prod or MutInd expected") and type_of_aux' metasenv context t = - let rec type_of_aux subst metasenv context t = - let module C = Cic in - let module S = CicSubstitution in - let module U = UriManager in - match t with -(* function *) - C.Rel n -> - (try - match List.nth context (n - 1) with - Some (_,C.Decl t) -> S.lift n t,subst,metasenv - | Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv - | Some (_,C.Def (bo,None)) -> - type_of_aux subst metasenv context (S.lift n bo) - | None -> raise (RefineFailure "Rel to hidden hypothesis") - with - _ -> raise (RefineFailure "Not a close term") - ) - | C.Var (uri,exp_named_subst) -> - let subst',metasenv' = - check_exp_named_subst subst metasenv context exp_named_subst in - let ty = - CicSubstitution.subst_vars exp_named_subst (type_of_variable uri) - in - ty,subst',metasenv' - | C.Meta (n,l) -> - (try - let (canonical_context, term,ty) = CicUtil.lookup_subst n subst in - let subst,metasenv = - check_metasenv_consistency n subst metasenv context - canonical_context l - in - (* trust or check ??? *) - CicSubstitution.lift_meta l ty, subst, metasenv - (* 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 = - check_metasenv_consistency n subst metasenv context - canonical_context l - in - CicSubstitution.lift_meta l ty, subst, metasenv) - (* TASSI: CONSTRAINT *) - | C.Sort (C.Type t) -> - let t' = CicUniv.fresh() in - if not (CicUniv.add_gt t' t ) then - assert false (* t' is fresh! an error in CicUniv *) - else - C.Sort (C.Type t'),subst,metasenv - (* TASSI: CONSTRAINT *) - | C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())),subst,metasenv - | C.Implicit _ -> raise (AssertFailure "21") - | C.Cast (te,ty) -> - let _,subst',metasenv' = - type_of_aux subst metasenv context ty in - let inferredty,subst'',metasenv'' = - type_of_aux subst' metasenv' context te - in - (try - let subst''',metasenv''' = - fo_unif_subst subst'' context metasenv'' inferredty ty - in - ty,subst''',metasenv''' - with - _ -> raise (RefineFailure "Cast")) - | C.Prod (name,s,t) -> - let sort1,subst',metasenv' = type_of_aux subst metasenv context s in - let sort2,subst'',metasenv'' = - type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) t - in - sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2) - | C.Lambda (n,s,t) -> - let sort1,subst',metasenv' = type_of_aux subst metasenv context s in - (match CicReduction.whd ~subst:subst' context sort1 with - C.Meta _ - | C.Sort _ -> () - | _ -> - raise (RefineFailure (sprintf - "Not well-typed lambda-abstraction: the source %s should be a type; + let rec type_of_aux subst metasenv context t = + let module C = Cic in + let module S = CicSubstitution in + let module U = UriManager in + match t with + (* function *) + C.Rel n -> + (try + match List.nth context (n - 1) with + Some (_,C.Decl t) -> S.lift n t,subst,metasenv + | Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv + | Some (_,C.Def (bo,None)) -> + type_of_aux subst metasenv context (S.lift n bo) + | None -> raise (RefineFailure "Rel to hidden hypothesis") + with + _ -> raise (RefineFailure "Not a close term") + ) + | C.Var (uri,exp_named_subst) -> + let subst',metasenv' = + check_exp_named_subst subst metasenv context exp_named_subst in + let ty = + CicSubstitution.subst_vars exp_named_subst (type_of_variable uri) + in + ty,subst',metasenv' + | C.Meta (n,l) -> + (try + let (canonical_context, term,ty) = CicUtil.lookup_subst n subst in + let subst,metasenv = + check_metasenv_consistency n subst metasenv context + canonical_context l + in + (* trust or check ??? *) + CicSubstitution.lift_meta l ty, subst, metasenv + (* 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 = + check_metasenv_consistency n subst metasenv context + canonical_context l + in + CicSubstitution.lift_meta l ty, subst, metasenv) + (* TASSI: CONSTRAINT *) + | C.Sort (C.Type t) -> + let t' = CicUniv.fresh() in + if not (CicUniv.add_gt t' t ) then + assert false (* t' is fresh! an error in CicUniv *) + else + C.Sort (C.Type t'),subst,metasenv + (* TASSI: CONSTRAINT *) + | C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())),subst,metasenv + | C.Implicit _ -> raise (AssertFailure "21") + | C.Cast (te,ty) -> + let _,subst',metasenv' = + type_of_aux subst metasenv context ty in + let inferredty,subst'',metasenv'' = + type_of_aux subst' metasenv' context te + in + (try + let subst''',metasenv''' = + fo_unif_subst subst'' context metasenv'' inferredty ty + in + ty,subst''',metasenv''' + with + _ -> raise (RefineFailure "Cast")) + | C.Prod (name,s,t) -> + let sort1,subst',metasenv' = type_of_aux subst metasenv context s in + let sort2,subst'',metasenv'' = + type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) t + in + sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2) + | C.Lambda (n,s,t) -> + let sort1,subst',metasenv' = type_of_aux subst metasenv context s in + (match CicReduction.whd ~subst:subst' context sort1 with + C.Meta _ + | C.Sort _ -> () + | _ -> + raise (RefineFailure (sprintf + "Not well-typed lambda-abstraction: the source %s should be a type; instead it is a term of type %s" (CicPp.ppterm s) - (CicPp.ppterm sort1))) - ) ; - let type2,subst'',metasenv'' = - type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t - in - C.Prod (n,s,type2),subst'',metasenv'' - | C.LetIn (n,s,t) -> - (* only to check if s is well-typed *) - let ty,subst',metasenv' = type_of_aux subst metasenv context s in - let inferredty,subst'',metasenv'' = - type_of_aux subst' metasenv' ((Some (n,(C.Def (s,Some ty))))::context) t - 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' - | C.Appl (he::((_::_) as tl)) -> - let hetype,subst',metasenv' = type_of_aux subst metasenv context he in - let tlbody_and_type,subst'',metasenv'' = - List.fold_right - (fun x (res,subst,metasenv) -> - let ty,subst',metasenv' = - type_of_aux subst metasenv context x - in - (x, ty)::res,subst',metasenv' - ) tl ([],subst',metasenv') - in - eat_prods subst'' metasenv'' context hetype tlbody_and_type - | C.Appl _ -> raise (RefineFailure "Appl: no arguments") - | C.Const (uri,exp_named_subst) -> - let subst',metasenv' = - check_exp_named_subst subst metasenv context exp_named_subst in - let cty = - CicSubstitution.subst_vars exp_named_subst (type_of_constant uri) - in - cty,subst',metasenv' - | C.MutInd (uri,i,exp_named_subst) -> - let subst',metasenv' = - check_exp_named_subst subst metasenv context exp_named_subst in - let cty = - CicSubstitution.subst_vars exp_named_subst - (type_of_mutual_inductive_defs uri i) - in - cty,subst',metasenv' - | C.MutConstruct (uri,i,j,exp_named_subst) -> - let subst',metasenv' = - check_exp_named_subst subst metasenv context exp_named_subst in - let cty = - CicSubstitution.subst_vars exp_named_subst - (type_of_mutual_inductive_constr uri i j) - in - cty,subst',metasenv' - | C.MutCase (uri, i, outtype, term, pl) -> - (* first, get the inductive type (and noparams) in the environment *) - let (_,b,arity,constructors), expl_params, no_left_params = - let obj = - try - CicEnvironment.get_cooked_obj ~trust:true uri - with Not_found -> assert false - in - match obj with - C.InductiveDefinition (l,expl_params,parsno) -> - List.nth l i , expl_params, parsno - | _ -> - raise - (RefineFailure - ("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 - 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 - 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 - 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)) - in - (* check consistency with the actual type of term *) - let actual_type,subst,metasenv = - type_of_aux subst metasenv context term in - let _, subst, metasenv = - type_of_aux subst metasenv context expected_type - in - let actual_type = CicReduction.whd ~subst context actual_type in - let subst,metasenv = - fo_unif_subst subst context metasenv expected_type actual_type - in - (* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *) - let (_,outtypeinstances,subst,metasenv) = - List.fold_left - (fun (j,outtypeinstances,subst,metasenv) p -> - let constructor = - if left_args = [] then - (C.MutConstruct (uri,i,j,exp_named_subst)) + (CicPp.ppterm sort1))) + ) ; + let type2,subst'',metasenv'' = + type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t + in + C.Prod (n,s,type2),subst'',metasenv'' + | C.LetIn (n,s,t) -> + (* only to check if s is well-typed *) + let ty,subst',metasenv' = type_of_aux subst metasenv context s in + let inferredty,subst'',metasenv'' = + type_of_aux subst' metasenv' ((Some (n,(C.Def (s,Some ty))))::context) t + 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' + | C.Appl (he::((_::_) as tl)) -> + let hetype,subst',metasenv' = type_of_aux subst metasenv context he in + let tlbody_and_type,subst'',metasenv'' = + List.fold_right + (fun x (res,subst,metasenv) -> + let ty,subst',metasenv' = + type_of_aux subst metasenv context x + in + (x, ty)::res,subst',metasenv' + ) tl ([],subst',metasenv') + in + eat_prods subst'' metasenv'' context hetype tlbody_and_type + | C.Appl _ -> raise (RefineFailure "Appl: no arguments") + | C.Const (uri,exp_named_subst) -> + let subst',metasenv' = + check_exp_named_subst subst metasenv context exp_named_subst in + let cty = + CicSubstitution.subst_vars exp_named_subst (type_of_constant uri) + in + cty,subst',metasenv' + | C.MutInd (uri,i,exp_named_subst) -> + let subst',metasenv' = + check_exp_named_subst subst metasenv context exp_named_subst in + let cty = + CicSubstitution.subst_vars exp_named_subst + (type_of_mutual_inductive_defs uri i) + in + cty,subst',metasenv' + | C.MutConstruct (uri,i,j,exp_named_subst) -> + let subst',metasenv' = + check_exp_named_subst subst metasenv context exp_named_subst in + let cty = + CicSubstitution.subst_vars exp_named_subst + (type_of_mutual_inductive_constr uri i j) + in + cty,subst',metasenv' + | C.MutCase (uri, i, outtype, term, pl) -> + (* first, get the inductive type (and noparams) in the environment *) + let (_,b,arity,constructors), expl_params, no_left_params = + (* + let obj = + try + CicEnvironment.get_cooked_obj ~trust:true uri + with Not_found -> assert false + in + *) + match CicEnvironment.get_obj uri with + C.InductiveDefinition (l,expl_params,parsno) -> + List.nth l i , expl_params, parsno + | _ -> + raise + (RefineFailure + ("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 + 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 + 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 + 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.MutConstruct (uri,i,j,exp_named_subst)::left_args)) - in - let actual_type,subst,metasenv = - type_of_aux subst metasenv context p in - let expected_type, subst, metasenv = - type_of_aux subst metasenv context constructor in - let outtypeinstance,subst,metasenv = - check_branch - 0 context metasenv subst - no_left_params actual_type constructor expected_type in - (j+1,outtypeinstance::outtypeinstances,subst,metasenv)) - (1,[],subst,metasenv) 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 *) + 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 = + type_of_aux subst metasenv context term in + let _, subst, metasenv = + type_of_aux subst metasenv context expected_type + in + let actual_type = CicReduction.whd ~subst context actual_type in + let subst,metasenv = + fo_unif_subst subst context metasenv expected_type actual_type + in + (* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *) + let (_,outtypeinstances,subst,metasenv) = + List.fold_left + (fun (j,outtypeinstances,subst,metasenv) 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 = + type_of_aux subst metasenv context p in + let expected_type, subst, metasenv = + type_of_aux subst metasenv context constructor in + let outtypeinstance,subst,metasenv = + check_branch + 0 context metasenv subst + no_left_params actual_type constructor expected_type in + (j+1,outtypeinstance::outtypeinstances,subst,metasenv)) + (1,[],subst,metasenv) 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 = - type_of_aux subst metasenv context - (C.Appl ((outtype :: right_args) @ [term])) - in - let (subst,metasenv) = - List.fold_left - (fun (subst,metasenv) (constructor_args_no,context,instance,args) -> - let instance' = - let appl = - let outtype' = - CicSubstitution.lift constructor_args_no outtype - in - C.Appl (outtype'::args) - in -(* - (* if appl is not well typed then the type_of below solves the - * problem *) - let (_, subst, metasenv) = - type_of_aux subst metasenv context appl - in -*) - (* DEBUG - let prova1 = CicMetaSubst.whd subst context appl in - let prova2 = CicReduction.whd ~subst context appl in - if not (prova1 = prova2) then - begin - prerr_endline ("prova1 =" ^ (CicPp.ppterm prova1)); - prerr_endline ("prova2 =" ^ (CicPp.ppterm prova2)); - end; - *) - (* CicMetaSubst.whd subst context appl *) - CicReduction.whd ~subst context appl - in - fo_unif_subst subst context metasenv instance instance') - (subst,metasenv) outtypeinstances in - CicReduction.whd ~subst - context (C.Appl(outtype::right_args@[term])),subst,metasenv - | C.Fix (i,fl) -> - let subst,metasenv,types = - List.fold_left - (fun (subst,metasenv,types) (n,_,ty,_) -> - let _,subst',metasenv' = type_of_aux subst metasenv context ty in - subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types - ) (subst,metasenv,[]) fl - in - let len = List.length types in - let context' = types@context in - let subst,metasenv = - List.fold_left - (fun (subst,metasenv) (name,x,ty,bo) -> - let ty_of_bo,subst,metasenv = - type_of_aux subst metasenv context' bo - in - fo_unif_subst subst context' metasenv - ty_of_bo (CicSubstitution.lift len ty) - ) (subst,metasenv) fl in - let (_,_,ty,_) = List.nth fl i in - ty,subst,metasenv - | C.CoFix (i,fl) -> - let subst,metasenv,types = - List.fold_left - (fun (subst,metasenv,types) (n,ty,_) -> - let _,subst',metasenv' = type_of_aux subst metasenv context ty in - subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types - ) (subst,metasenv,[]) fl - in - let len = List.length types in - let context' = types@context in - let subst,metasenv = - List.fold_left - (fun (subst,metasenv) (name,ty,bo) -> - let ty_of_bo,subst,metasenv = - type_of_aux subst metasenv context' bo - in - fo_unif_subst subst context' metasenv - ty_of_bo (CicSubstitution.lift len ty) - ) (subst,metasenv) fl in - - let (_,ty,_) = List.nth fl i in - ty,subst,metasenv + (* easy case *) + let _, subst, metasenv = + type_of_aux subst metasenv context + (C.Appl ((outtype :: right_args) @ [term])) + in + let (subst,metasenv) = + List.fold_left + (fun (subst,metasenv) (constructor_args_no,context,instance,args) -> + let instance' = + let appl = + let outtype' = + CicSubstitution.lift constructor_args_no outtype + in + C.Appl (outtype'::args) + in + (* + (* if appl is not well typed then the type_of below solves the + * problem *) + let (_, subst, metasenv) = + type_of_aux subst metasenv context appl + in + *) + (* DEBUG + let prova1 = CicMetaSubst.whd subst context appl in + let prova2 = CicReduction.whd ~subst context appl in + if not (prova1 = prova2) then + begin + prerr_endline ("prova1 =" ^ (CicPp.ppterm prova1)); + prerr_endline ("prova2 =" ^ (CicPp.ppterm prova2)); + end; + *) + (* CicMetaSubst.whd subst context appl *) + CicReduction.whd ~subst context appl + in + fo_unif_subst subst context metasenv instance instance') + (subst,metasenv) outtypeinstances in + CicReduction.whd ~subst + context (C.Appl(outtype::right_args@[term])),subst,metasenv + | C.Fix (i,fl) -> + let subst,metasenv,types = + List.fold_left + (fun (subst,metasenv,types) (n,_,ty,_) -> + let _,subst',metasenv' = type_of_aux subst metasenv context ty in + subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types + ) (subst,metasenv,[]) fl + in + let len = List.length types in + let context' = types@context in + let subst,metasenv = + List.fold_left + (fun (subst,metasenv) (name,x,ty,bo) -> + let ty_of_bo,subst,metasenv = + type_of_aux subst metasenv context' bo + in + fo_unif_subst subst context' metasenv + ty_of_bo (CicSubstitution.lift len ty) + ) (subst,metasenv) fl in + let (_,_,ty,_) = List.nth fl i in + ty,subst,metasenv + | C.CoFix (i,fl) -> + let subst,metasenv,types = + List.fold_left + (fun (subst,metasenv,types) (n,ty,_) -> + let _,subst',metasenv' = type_of_aux subst metasenv context ty in + subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types + ) (subst,metasenv,[]) fl + in + let len = List.length types in + let context' = types@context in + let subst,metasenv = + List.fold_left + (fun (subst,metasenv) (name,ty,bo) -> + let ty_of_bo,subst,metasenv = + type_of_aux subst metasenv context' bo + in + fo_unif_subst subst context' metasenv + ty_of_bo (CicSubstitution.lift len ty) + ) (subst,metasenv) fl in + + let (_,ty,_) = List.nth fl i in + ty,subst,metasenv - (* 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 - = - let module C = Cic in - let module R = CicReduction in - let module S = CicSubstitution in + (* 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 + = + 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.lift_meta l (S.lift i t))))::(aux (i+1) tl) - | (Some (n,C.Def (t,None)))::tl -> - (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl) - | None::tl -> None::(aux (i+1) tl) - | (Some (n,C.Def (t,Some ty)))::tl -> - (Some (n, - C.Def ((S.lift_meta l (S.lift i t)), - Some (S.lift_meta l (S.lift i ty))))) :: (aux (i+1) tl) - in - aux 1 canonical_context + let rec aux i = + function + [] -> [] + | (Some (n,C.Decl t))::tl -> + (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl) + | (Some (n,C.Def (t,None)))::tl -> + (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl) + | None::tl -> None::(aux (i+1) tl) + | (Some (n,C.Def (t,Some ty)))::tl -> + (Some (n, + C.Def ((S.lift_meta l (S.lift i t)), + Some (S.lift_meta l (S.lift i ty))))) :: (aux (i+1) tl) + in + aux 1 canonical_context in - try - List.fold_left2 - (fun (subst,metasenv) t ct -> - match (t,ct) with - _,None -> - subst,metasenv - | Some t,Some (_,C.Def (ct,_)) -> - (try - fo_unif_subst subst context metasenv t ct - 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))))) - | Some t,Some (_,C.Decl ct) -> - let inferredty,subst',metasenv' = - type_of_aux subst metasenv context t - in - (try - fo_unif_subst - subst' context metasenv' inferredty ct - 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))))) - | 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) l lifted_canonical_context - with - Invalid_argument _ -> - raise - (RefineFailure - (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 subst (Cic.Meta (metano, l))) - (CicMetaSubst.ppcontext subst canonical_context))) + try + List.fold_left2 + (fun (subst,metasenv) t ct -> + match (t,ct) with + _,None -> + subst,metasenv + | Some t,Some (_,C.Def (ct,_)) -> + (try + fo_unif_subst subst context metasenv t ct + 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))))) + | Some t,Some (_,C.Decl ct) -> + let inferredty,subst',metasenv' = + type_of_aux subst metasenv context t + in + (try + fo_unif_subst + subst' context metasenv' inferredty ct + 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))))) + | 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) l lifted_canonical_context + with + Invalid_argument _ -> + raise + (RefineFailure + (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 subst (Cic.Meta (metano, l))) + (CicMetaSubst.ppcontext subst canonical_context))) - and check_exp_named_subst metasubst metasenv context = - let rec check_exp_named_subst_aux metasubst metasenv substs = - function - [] -> metasubst,metasenv - | ((uri,t) as subst)::tl -> - let typeofvar = - CicSubstitution.subst_vars substs (type_of_variable 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 - "A variable with a body can not be explicit substituted") - | Cic.Variable (_,None,_,_) -> () - | _ -> - raise - (RefineFailure - ("Unkown variable definition " ^ UriManager.string_of_uri uri)) - ) ; -*) - let typeoft,metasubst',metasenv' = - type_of_aux metasubst metasenv context t - in - let metasubst'',metasenv'' = - try - fo_unif_subst metasubst' context metasenv' typeoft typeofvar - with _ -> - raise (RefineFailure - ("Wrong Explicit Named Substitution: " ^ CicMetaSubst.ppterm metasubst' typeoft ^ - " not unifiable with " ^ CicMetaSubst.ppterm metasubst' typeofvar)) - in - check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl - in - check_exp_named_subst_aux metasubst metasenv [] + and check_exp_named_subst metasubst metasenv context = + let rec check_exp_named_subst_aux metasubst metasenv substs = + function + [] -> metasubst,metasenv + | ((uri,t) as subst)::tl -> + let typeofvar = + CicSubstitution.subst_vars substs (type_of_variable 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 + "A variable with a body can not be explicit substituted") + | Cic.Variable (_,None,_,_) -> () + | _ -> + raise + (RefineFailure + ("Unkown variable definition " ^ UriManager.string_of_uri uri)) + ) ; + *) + let typeoft,metasubst',metasenv' = + type_of_aux metasubst metasenv context t + in + let metasubst'',metasenv'' = + try + fo_unif_subst metasubst' context metasenv' typeoft typeofvar + with _ -> + raise (RefineFailure + ("Wrong Explicit Named Substitution: " ^ CicMetaSubst.ppterm metasubst' typeoft ^ + " not unifiable with " ^ CicMetaSubst.ppterm metasubst' typeofvar)) + in + check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl + in + check_exp_named_subst_aux metasubst metasenv [] - and sort_of_prod subst metasenv context (name,s) (t1, t2) = - let module C = Cic in + and sort_of_prod subst metasenv context (name,s) (t1, t2) = + 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 or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *) - C.Sort s2,subst,metasenv - | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> - (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *) - let t' = CicUniv.fresh() in - if not (CicUniv.add_ge t' t1) || not (CicUniv.add_ge t' t2) then - assert false ; (* not possible, error in CicUniv *) - C.Sort (C.Type t'),subst,metasenv - | (C.Sort _,C.Sort (C.Type t1)) -> - (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *) - C.Sort (C.Type t1),subst,metasenv - | (C.Meta _, C.Sort _) -> t2'',subst,metasenv - | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) -> - (* TODO how can we force the meta to become a sort? If we don't we - * brake 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) = - fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2'' - in - t2'',subst,metasenv - | (_,_) -> - raise (RefineFailure (sprintf - "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)" - (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2) - (CicPp.ppterm t2''))) + match (t1'', t2'') with + (C.Sort s1, C.Sort s2) + when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *) + C.Sort s2,subst,metasenv + | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> + (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *) + let t' = CicUniv.fresh() in + if not (CicUniv.add_ge t' t1) || not (CicUniv.add_ge t' t2) then + assert false ; (* not possible, error in CicUniv *) + C.Sort (C.Type t'),subst,metasenv + | (C.Sort _,C.Sort (C.Type t1)) -> + (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *) + C.Sort (C.Type t1),subst,metasenv + | (C.Meta _, C.Sort _) -> t2'',subst,metasenv + | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) -> + (* TODO how can we force the meta to become a sort? If we don't we + * brake 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) = + fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2'' + in + t2'',subst,metasenv + | (_,_) -> + raise (RefineFailure (sprintf + "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)" + (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2) + (CicPp.ppterm t2''))) - and eat_prods subst metasenv context hetype tlbody_and_type = - let rec mk_prod metasenv context = - function - [] -> - 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 irl = - CicMkImplicit.identity_relocation_list_for_metavariable context - in - let meta = Cic.Meta (idx,irl) in - let name = - (* The name must be fresh for context. *) - (* Nevertheless, argty is well-typed only in context. *) - (* Thus I generate a name (name_hint) in context and *) - (* then I generate a name --- using the hint name_hint *) - (* --- that is fresh in (context'@context). *) - let name_hint = - (* Cic.Name "pippo" *) - FreshNamesGenerator.mk_fresh_name metasenv -(* (CicMetaSubst.apply_subst_metasenv subst metasenv) *) - (CicMetaSubst.apply_subst_context subst context) - Cic.Anonymous - (CicMetaSubst.apply_subst subst argty) - in - (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *) - FreshNamesGenerator.mk_fresh_name - [] context name_hint (Cic.Sort Cic.Prop) - in - let metasenv,target = - mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl - in - metasenv,Cic.Prod (name,meta,target) - in - let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in - let (subst, metasenv) = - fo_unif_subst subst context metasenv hetype hetype' - in - let rec eat_prods metasenv subst context hetype = + and eat_prods subst metasenv context hetype tlbody_and_type = + let rec mk_prod metasenv context = function - [] -> metasenv,subst,hetype - | (hete, hety)::tl -> - (match hetype with - Cic.Prod (n,s,t) -> - let subst,metasenv = - fo_unif_subst subst context metasenv hety s -(* - 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 *) + [] -> + 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 irl = + CicMkImplicit.identity_relocation_list_for_metavariable context + in + let meta = Cic.Meta (idx,irl) in + let name = + (* The name must be fresh for context. *) + (* Nevertheless, argty is well-typed only in context. *) + (* Thus I generate a name (name_hint) in context and *) + (* then I generate a name --- using the hint name_hint *) + (* --- that is fresh in (context'@context). *) + let name_hint = + (* Cic.Name "pippo" *) + FreshNamesGenerator.mk_fresh_name ~subst metasenv + (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *) + (CicMetaSubst.apply_subst_context subst context) + Cic.Anonymous + ~typ:(CicMetaSubst.apply_subst subst argty) 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)); - *) - eat_prods metasenv subst context - (* (CicMetaSubst.subst subst hete t) tl *) - (CicSubstitution.subst hete t) tl - | _ -> assert false - ) - in + (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *) + FreshNamesGenerator.mk_fresh_name ~subst + [] context name_hint ~typ:(Cic.Sort Cic.Prop) + in + let metasenv,target = + mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl + in + metasenv,Cic.Prod (name,meta,target) + in + let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in + let (subst, metasenv) = + try + fo_unif_subst subst context metasenv hetype hetype' + with exn -> + prerr_endline (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s" + (CicPp.ppterm hetype) + (CicPp.ppterm hetype') + (CicMetaSubst.ppmetasenv metasenv []) + (CicMetaSubst.ppsubst subst)); + raise exn + + in + let rec eat_prods metasenv subst context hetype = + function + [] -> metasenv,subst,hetype + | (hete, hety)::tl -> + (match hetype with + Cic.Prod (n,s,t) -> + let subst,metasenv = + try + fo_unif_subst subst context metasenv hety s + 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 *) + 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)); + *) + eat_prods metasenv subst context + (* (CicMetaSubst.subst subst hete t) tl *) + (CicSubstitution.subst hete t) tl + | _ -> assert false + ) + in let metasenv,subst,t = - eat_prods metasenv subst context hetype' tlbody_and_type + eat_prods metasenv subst context hetype' tlbody_and_type in - t,subst,metasenv -(* - let rec aux context' args (resty,subst,metasenv) = - function - [] -> resty,subst,metasenv - | (arg,argty)::tl -> - let args' = - List.map - (function - None -> assert false - | Some t -> Some (CicMetaSubst.lift subst 1 t) - ) args in - let argty' = CicMetaSubst.lift subst (List.length args) argty in - let name = - (* The name must be fresh for (context'@context). *) - (* Nevertheless, argty is well-typed only in context. *) - (* Thus I generate a name (name_hint) in context and *) - (* then I generate a name --- using the hint name_hint *) - (* --- that is fresh in (context'@context). *) - let name_hint = - FreshNamesGenerator.mk_fresh_name - (CicMetaSubst.apply_subst_metasenv subst metasenv) - (CicMetaSubst.apply_subst_context subst context) - Cic.Anonymous - (CicMetaSubst.apply_subst subst argty) - in - (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *) - FreshNamesGenerator.mk_fresh_name - [] (context'@context) name_hint (Cic.Sort Cic.Prop) - in - let context'' = Some (name, Cic.Decl argty') :: context' in - let (metasenv, idx) = - CicMkImplicit.mk_implicit_type metasenv (context'' @ context) in - let irl = - (Some (Cic.Rel 1))::args' @ - (CicMkImplicit.identity_relocation_list_for_metavariable ~start:2 - context) - in - let newmeta = Cic.Meta (idx, irl) in - let prod = Cic.Prod (name, argty, newmeta) in - let (_, subst, metasenv) = type_of_aux subst metasenv context prod in - let (subst, metasenv) = - fo_unif_subst subst context metasenv resty prod - in - aux context'' (Some arg :: args) - (CicMetaSubst.subst subst arg newmeta, subst, metasenv) tl + t,subst,metasenv + (* eat prods ends here! *) in - aux [] [] (hetype,subst,metasenv) tlbody_and_type -*) - in let ty,subst',metasenv' = - type_of_aux [] metasenv context t + type_of_aux [] metasenv context 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 -e' sempre istanziato *) - let substituted_metasenv = - CicMetaSubst.apply_subst_metasenv subst' metasenv' in - (* metasenv' *) -(* substituted_t,substituted_ty,substituted_metasenv *) -(* ANDREA: spostare tutta questa robaccia da un altra parte *) - let cleaned_t = - FreshNamesGenerator.clean_dummy_dependent_types substituted_t in - let cleaned_ty = - FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in - let cleaned_metasenv = - List.map + 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 + e' sempre istanziato *) + let substituted_metasenv = + CicMetaSubst.apply_subst_metasenv subst' metasenv' in + (* metasenv' *) + (* substituted_t,substituted_ty,substituted_metasenv *) + (* ANDREA: spostare tutta questa robaccia da un altra parte *) + let cleaned_t = + FreshNamesGenerator.clean_dummy_dependent_types substituted_t in + let cleaned_ty = + FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in + let cleaned_metasenv = + List.map (function (n,context,ty) -> - let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in - let context' = - List.map - (function - None -> None - | Some (n, Cic.Decl t) -> - Some (n, - Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t)) - | Some (n, Cic.Def (bo,ty)) -> - let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in - let ty' = - match ty with - None -> None - | Some ty -> - Some (FreshNamesGenerator.clean_dummy_dependent_types ty) - in - Some (n, Cic.Def (bo',ty')) - ) context - in - (n,context',ty') + let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in + let context' = + List.map + (function + None -> None + | Some (n, Cic.Decl t) -> + Some (n, + Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t)) + | Some (n, Cic.Def (bo,ty)) -> + let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in + let ty' = + match ty with + None -> None + | Some ty -> + Some (FreshNamesGenerator.clean_dummy_dependent_types ty) + in + Some (n, Cic.Def (bo',ty')) + ) context + in + (n,context',ty') ) substituted_metasenv - in - (cleaned_t,cleaned_ty,cleaned_metasenv) + in + (cleaned_t,cleaned_ty,cleaned_metasenv) ;; -- 2.39.2