From: Stefano Zacchiroli Date: Thu, 22 Jan 2004 10:30:52 +0000 (+0000) Subject: bugfixes, typos and the hell X-Git-Tag: V_0_5_1_3~8 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=99744ac02b9f208f6668d7efc9b21a8e3818cc39;p=helm.git bugfixes, typos and the hell --- diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index d822ec341..9434f5232 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -48,6 +48,8 @@ let debug t context = (*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*) ;; +let debug_print = prerr_endline + let rec split l n = match (l,n) with (l,0) -> ([], l) @@ -103,22 +105,22 @@ and type_of_mutual_inductive_constr uri i j = try to synthesize it from the above information, that is in general a second order unification problem. *) -and check_branch context metasenv subst left_args_no actualtype term expectedtype = +and check_branch n context metasenv subst left_args_no actualtype term expectedtype = let module C = Cic in - let module R = CicReduction in + let module R = CicMetaSubst in let module Un = CicUnification in - match R.whd context expectedtype with + match R.whd subst context expectedtype with C.MutInd (_,_,_) -> - (actualtype, [term]), subst, metasenv + (n,context,actualtype, [term]), subst, metasenv | C.Appl (C.MutInd (_,_,_)::tl) -> let (_,arguments) = split tl left_args_no in - (actualtype, arguments@[term]), subst, metasenv + (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 context actualtype with + (match R.whd subst context actualtype with C.Prod (name',so',de') -> - let subst,metsaenv = + let subst, metasenv = Un.fo_unif_subst subst context metasenv so so' in let term' = (match CicSubstitution.lift 1 term with @@ -126,7 +128,7 @@ and check_branch context metasenv subst left_args_no actualtype term expectedtyp | 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 ((Some (name,(C.Decl so)))::context) metasenv subst left_args_no de' term' de + check_branch (n+1) ((Some (name,(C.Decl so)))::context) metasenv subst left_args_no de' term' de | _ -> raise WrongArgumentNumber) | _ -> raise (NotRefinable "Prod or MutInd expected") @@ -143,7 +145,6 @@ and type_of_aux' metasenv context t = 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)) -> - prerr_endline "##### DA INVESTIGARE E CAPIRE" ; type_of_aux subst metasenv context (S.lift n bo) | None -> raise RelToHiddenHypothesis with @@ -264,7 +265,7 @@ and type_of_aux' metasenv context t = raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) in let rec count_prod t = - match CicReduction.whd context t with + match CicMetaSubst.whd subst context t with C.Prod (_, _, t) -> 1 + (count_prod t) | _ -> 0 in let no_args = count_prod arity in @@ -286,11 +287,13 @@ and type_of_aux' metasenv context t = (* 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 = CicMetaSubst.whd subst context actual_type in let subst,metasenv = - Un.fo_unif_subst - subst - context - metasenv expected_type (CicReduction.whd context actual_type) in + Un.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 @@ -299,8 +302,7 @@ and type_of_aux' metasenv context t = 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)) + (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 @@ -308,7 +310,7 @@ and type_of_aux' metasenv context t = type_of_aux subst metasenv context constructor in let outtypeinstance,subst,metasenv = check_branch - context metasenv subst + 0 context metasenv subst no_left_params actual_type constructor expected_type in (j+1,outtypeinstance::outtypeinstances,subst,metasenv)) (1,[],subst,metasenv) pl in @@ -317,14 +319,32 @@ and type_of_aux' metasenv context t = 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) (instance,args) -> - let instance' = - CicReduction.whd context (C.Appl(outtype::args)) in + (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 +*) + CicMetaSubst.whd subst context appl + in Un.fo_unif_subst subst context metasenv instance instance') (subst,metasenv) outtypeinstances in - CicReduction.whd + CicMetaSubst.whd subst context (C.Appl(outtype::right_args@[term])),subst,metasenv | C.Fix _ | C.CoFix _ -> raise MutCaseFixAndCofixRefineNotImplemented @@ -352,7 +372,8 @@ and type_of_aux' metasenv context t = List.fold_left2 (fun (subst,metasenv) t ct -> match (t,ct) with - _,None -> subst,metasenv + _,None -> + subst,metasenv | Some t,Some (_,C.Def (ct,_)) -> (try CicUnification.fo_unif_subst subst context metasenv t ct @@ -362,9 +383,11 @@ and type_of_aux' metasenv context t = type_of_aux subst metasenv context t in (try - CicUnification.fo_unif_subst subst context metasenv inferredty ct + CicUnification.fo_unif_subst + subst' context metasenv' inferredty ct with _ -> raise MetasenvInconsistency) - | _, _ -> raise MetasenvInconsistency + | _, _ -> + raise MetasenvInconsistency ) (subst,metasenv) l lifted_canonical_context and check_exp_named_subst metasubst metasenv context = @@ -399,11 +422,11 @@ and type_of_aux' metasenv context t = and sort_of_prod subst metasenv context (name,s) (t1, t2) = let module C = Cic in (* ti could be a metavariable in the domain of the substitution *) - let subst',metasenv' = CicUnification.unwind_subst metasenv subst in - let t1' = CicUnification.apply_subst subst' t1 in - let t2' = CicUnification.apply_subst subst' t2 in - let t1'' = CicReduction.whd context t1' in - let t2'' = CicReduction.whd ((Some (name,C.Decl s))::context) t2' in + let subst',metasenv' = CicMetaSubst.unwind_subst metasenv subst in + let t1' = CicMetaSubst.apply_subst subst' t1 in + let t2' = CicMetaSubst.apply_subst subst' t2 in + let t1'' = CicMetaSubst.whd subst' context t1' in + let t2'' = CicMetaSubst.whd subst' ((Some (name,C.Decl s))::context) 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 from Coq manual!!! *) @@ -411,12 +434,18 @@ and type_of_aux' metasenv context t = | (C.Sort s1, C.Sort s2) -> (*CSC manca la gestione degli universi!!! *) C.Sort C.Type,subst',metasenv' - | (C.Meta _,_) - | (_,C.Meta _) -> + | (C.Meta _,_) | (_,C.Meta _) -> + let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv context in + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context + in + C.Meta (idx, irl), subst, metasenv' +(* raise (Uncertain ("Two sorts were expected, found " ^ CicPp.ppterm t1'' ^ " and " ^ CicPp.ppterm t2'')) +*) | (_,_) -> raise (NotRefinable @@ -426,13 +455,10 @@ and type_of_aux' metasenv context t = function [] -> hetype,subst,metasenv | (hete, hety)::tl -> - (match (CicReduction.whd context hetype) with + (match (CicMetaSubst.whd subst context hetype) with Cic.Prod (n,s,t) -> let subst',metasenv' = - try CicUnification.fo_unif_subst subst context metasenv s hety - with _ -> - raise (NotRefinable "Appl: wrong parameter-type") in CicReduction.fdebug := -1 ; eat_prods subst' metasenv' context (CicSubstitution.subst hete t) tl @@ -446,49 +472,50 @@ and type_of_aux' metasenv context t = let ty,subst',metasenv' = type_of_aux [] metasenv context t in - let subst'',metasenv'' = CicUnification.unwind_subst metasenv' subst' in + let subst'',metasenv'' = CicMetaSubst.unwind_subst metasenv' subst' in (* we get rid of the metavariables that have been instantiated *) let metasenv''' = List.filter (function (i,_,_) -> not (List.exists (function (j,_) -> j=i) subst'')) metasenv'' in - CicUnification.apply_subst subst'' t, - CicUnification.apply_subst subst'' ty, - subst'', metasenv''' + CicMetaSubst.apply_subst subst'' t, + CicMetaSubst.apply_subst subst'' ty, + subst'', metasenv''' ;; (* DEBUGGING ONLY *) let type_of_aux' metasenv context term = try - let (t,ty,s,m) = - type_of_aux' metasenv context term - in + let (t,ty,s,m) = type_of_aux' metasenv context term in +(* List.iter (function (i,t) -> - prerr_endline ("+ ?" ^ string_of_int i ^ " := " ^ CicPp.ppterm t)) s ; + debug_print ("+ ?" ^ string_of_int i ^ " := " ^ CicPp.ppterm t)) s ; List.iter (function (i,_,t) -> - prerr_endline ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t)) m ; - prerr_endline + debug_print ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t)) m ; +*) + debug_print ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty) ; (t,ty,s,m) with - e -> + | CicUnification.AssertFailure msg as e -> + debug_print "@@@ REFINE FAILED: CicUnification.AssertFailure:"; + debug_print msg; + raise e + | CicUnification.UnificationFailure msg as e -> + debug_print "@@@ REFINE FAILED: CicUnification.UnificationFailure:"; + debug_print msg; + raise e + | e -> +(* List.iter (function (i,_,t) -> - prerr_endline ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t)) + debug_print ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t)) metasenv ; - prerr_endline ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ; +*) + debug_print ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ; raise e ;; - - - - - - - - -