X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.ml;h=36347ccd1a4f2c5b30f51c2b43b984af3e3a7146;hb=7e30c63fcf9f9fe1780ba7aa4d95fd0d8658548b;hp=e1253f8e8042cceec42add1498b88fe3986e0cef;hpb=07e176d2d2355cea8c5b9990cbbc3c7d234bfe15;p=helm.git diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index e1253f8e8..36347ccd1 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -146,12 +146,12 @@ let is_a_double_coercion t = | _ -> dummyres let more_args_than_expected - localization_tbl subst he context hetype' tlbody_and_type exn + localization_tbl metasenv subst he context hetype' tlbody_and_type exn = let msg = lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst he context ^ - " (that has type "^CicMetaSubst.ppterm_in_context subst hetype' context ^ + CicMetaSubst.ppterm_in_context ~metasenv subst he context ^ + " (that has type "^CicMetaSubst.ppterm_in_context ~metasenv subst hetype' context ^ ") is here applied to " ^ string_of_int (List.length tlbody_and_type) ^ " arguments that are more than expected") in @@ -427,11 +427,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t enrich localization_tbl te' ~f:(fun _ -> lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst'' te' + CicMetaSubst.ppterm_in_context metasenv'' subst'' te' context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst'' inferredty + CicMetaSubst.ppterm_in_context metasenv'' subst'' inferredty context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst'' ty' context)) exn + CicMetaSubst.ppterm_in_context metasenv'' subst'' ty' context)) exn ) | C.Prod (name,s,t) -> let carr t subst context = CicMetaSubst.apply_subst subst t in @@ -460,17 +460,17 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t enrich localization_tbl t (RefineFailure (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst t context ^ + CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " is not a type since it has type " ^ - CicMetaSubst.ppterm_in_context + CicMetaSubst.ppterm_in_context ~metasenv subst coercion_src context ^ " that is not a sort"))) | CoercGraph.NotMetaClosed -> enrich localization_tbl t (Uncertain (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst t context ^ + CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " is not a type since it has type " ^ - CicMetaSubst.ppterm_in_context + CicMetaSubst.ppterm_in_context ~metasenv subst coercion_src context ^ " that is not a sort"))) | CoercGraph.SomeCoercion candidates -> let selected = @@ -485,10 +485,10 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t enrich localization_tbl t (RefineFailure (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context + CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " is not a type since it has type " ^ - CicMetaSubst.ppterm_in_context + CicMetaSubst.ppterm_in_context ~metasenv subst coercion_src context ^ " that is not a sort")))) in @@ -534,17 +534,17 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t enrich localization_tbl s' (RefineFailure (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst s' context ^ + CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^ " is not a type since it has type " ^ - CicMetaSubst.ppterm_in_context + CicMetaSubst.ppterm_in_context ~metasenv subst coercion_src context ^ " that is not a sort"))) | CoercGraph.NotMetaClosed -> enrich localization_tbl s' (Uncertain (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst s' context ^ + CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^ " is not a type since it has type " ^ - CicMetaSubst.ppterm_in_context + CicMetaSubst.ppterm_in_context ~metasenv subst coercion_src context ^ " that is not a sort"))) | CoercGraph.SomeCoercion candidates -> let selected = @@ -559,9 +559,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t enrich localization_tbl s' (RefineFailure (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst s' context ^ + CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^ " is not a type since it has type " ^ - CicMetaSubst.ppterm_in_context + CicMetaSubst.ppterm_in_context ~metasenv subst coercion_src context ^ " that is not a sort"))) in @@ -691,11 +691,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t enrich localization_tbl term' exn ~f:(function _ -> lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst term' + CicMetaSubst.ppterm_in_context ~metasenv subst term' context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst actual_type + CicMetaSubst.ppterm_in_context ~metasenv subst actual_type context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst expected_type' context)) + CicMetaSubst.ppterm_in_context ~metasenv subst expected_type' context)) in let rec instantiate_prod t = function @@ -911,11 +911,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t enrich localization_tbl p exn ~f:(function _ -> lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst p + CicMetaSubst.ppterm_in_context ~metasenv subst p context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst instance' + CicMetaSubst.ppterm_in_context ~metasenv subst instance' context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst instance + CicMetaSubst.ppterm_in_context ~metasenv subst instance context))) (subst,metasenv,ugraph5) pl' outtypeinstances in @@ -952,11 +952,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t enrich localization_tbl bo exn ~f:(function _ -> lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst bo + CicMetaSubst.ppterm_in_context ~metasenv subst bo context' ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst ty_of_bo + CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo context' ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst expected_ty + CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty context)) in fl @ [bo'] , subst',metasenv',ugraph' @@ -1005,11 +1005,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t enrich localization_tbl bo exn ~f:(function _ -> lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst bo + CicMetaSubst.ppterm_in_context ~metasenv subst bo context' ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst ty_of_bo + CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo context' ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst expected_ty + CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty context)) in fl @ [bo'],subst',metasenv',ugraph' @@ -1070,7 +1070,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (try prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il Rel corrispondente. Si puo' ottimizzare il caso t = rel."); fo_unif_subst subst context metasenv t ct ugraph - with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e)))))) + with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm ~metasenv subst t) (CicMetaSubst.ppterm ~metasenv subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e)))))) in l @ [Some t],subst',metasenv',ugraph' | Some t,Some (_,C.Decl ct) -> @@ -1081,19 +1081,19 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il (try fo_unif_subst subst' context metasenv' inferredty ct ugraph1 - with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with AssertFailure msg -> Lazy.force msg | RefineFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e)))))) + with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm metasenv' subst' inferredty) (CicMetaSubst.ppterm metasenv' subst' t) (CicMetaSubst.ppterm metasenv' subst' ct) (match e with AssertFailure msg -> Lazy.force msg | RefineFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e)))))) in l @ [Some t'], subst'',metasenv'',ugraph2 | None, Some _ -> - raise (RefineFailure (lazy (sprintf "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s" (CicMetaSubst.ppterm subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext subst canonical_context))))) ([],subst,metasenv,ugraph) l lifted_canonical_context + raise (RefineFailure (lazy (sprintf "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s" (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))) ([],subst,metasenv,ugraph) l lifted_canonical_context with Invalid_argument _ -> raise (RefineFailure (lazy (sprintf "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s" - (CicMetaSubst.ppterm subst (Cic.Meta (metano, l))) - (CicMetaSubst.ppcontext subst canonical_context)))) + (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l))) + (CicMetaSubst.ppcontext ~metasenv subst canonical_context)))) and check_exp_named_subst metasubst metasenv context tl ugraph = let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph = @@ -1126,9 +1126,9 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il with _ -> raise (RefineFailure (lazy ("Wrong Explicit Named Substitution: " ^ - CicMetaSubst.ppterm metasubst' typeoft ^ + CicMetaSubst.ppterm metasenv' metasubst' typeoft ^ " not unifiable with " ^ - CicMetaSubst.ppterm metasubst' typeofvar))) + CicMetaSubst.ppterm metasenv' metasubst' typeofvar))) in (* FIXME: no mere tail recursive! *) let exp_name_subst, metasubst''', metasenv''', ugraph4 = @@ -1185,16 +1185,16 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il (lazy (sprintf "%s is supposed to be a type, but its type is %s" - (CicMetaSubst.ppterm_in_context subst t context) - (CicMetaSubst.ppterm_in_context subst t2 context)))) + (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 subst s context) - (CicMetaSubst.ppterm_in_context subst t1 context)))) + (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 @@ -1317,8 +1317,8 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il (* {{{ we search a coercion of the head (saturated) to funclass *) let metasenv = pristinemenv in debug_print (lazy - ("Fixing arity of: "^CicMetaSubst.ppterm subst hetype ^ - " since unif failed with: " ^ CicMetaSubst.ppterm subst hetype' + ("Fixing arity of: "^CicMetaSubst.ppterm ~metasenv subst hetype ^ + " since unif failed with: " ^ CicMetaSubst.ppterm ~metasenv subst hetype' (* ^ " cause: " ^ Lazy.force s *))); let how_many_args_are_needed = let rec aux n = function @@ -1355,7 +1355,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il HExtlib.list_findopt (fun coerc -> let t = Cic.Appl [coerc;x] in - debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm subst t)); + debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm ~metasenv subst t)); try (* we want this to be available in the error handler fo the * following (so it has its own try. *) @@ -1367,8 +1367,8 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il mk_prod_of_metas metasenv context subst remainder in debug_print (lazy - (" unif: " ^ CicMetaSubst.ppterm subst tty ^ " = " ^ - CicMetaSubst.ppterm subst hetype')); + (" unif: " ^ CicMetaSubst.ppterm ~metasenv subst tty ^ " = " ^ + CicMetaSubst.ppterm ~metasenv subst hetype')); let subst,metasenv,ugraph = fo_unif_subst_eat_prods subst context metasenv tty hetype' ugraph @@ -1392,7 +1392,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il | Some(subst,metasenv,ugraph,hetype',he,args_bo_and_ty)-> subst,metasenv,ugraph,hetype',he,args_bo_and_ty | None -> - more_args_than_expected localization_tbl + more_args_than_expected localization_tbl metasenv subst he context hetype args_bo_and_ty exn (* }}} end coercion to funclass stuff *) (* }}} end fix_arity *) @@ -1432,21 +1432,21 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il enrich localization_tbl hete exn ~f:(fun _ -> (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst hete + CicMetaSubst.ppterm_in_context ~metasenv subst hete context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst hety + CicMetaSubst.ppterm_in_context ~metasenv subst hety context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst s context + CicMetaSubst.ppterm_in_context ~metasenv subst s context (* "\nReason: " ^ Lazy.force e*)))) | CoercGraph.NotMetaClosed -> enrich localization_tbl hete exn ~f:(fun _ -> (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst hete + CicMetaSubst.ppterm_in_context ~metasenv subst hete context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst hety + CicMetaSubst.ppterm_in_context ~metasenv subst hety context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst s context + CicMetaSubst.ppterm_in_context ~metasenv subst s context (* "\nReason: " ^ Lazy.force e*)))) | CoercGraph.SomeCoercion candidates -> let selected = @@ -1476,21 +1476,21 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il enrich localization_tbl hete ~f:(fun _ -> (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst hete + CicMetaSubst.ppterm_in_context ~metasenv subst hete context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst hety + CicMetaSubst.ppterm_in_context ~metasenv subst hety context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst s context + CicMetaSubst.ppterm_in_context ~metasenv subst s context (* "\nReason: " ^ Lazy.force e*)))) exn)) | exn -> enrich localization_tbl hete ~f:(fun _ -> (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst hete + CicMetaSubst.ppterm_in_context ~metasenv subst hete context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst hety + CicMetaSubst.ppterm_in_context ~metasenv subst hety context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst s context + CicMetaSubst.ppterm_in_context ~metasenv subst s context (* "\nReason: " ^ Printexc.to_string exn*)))) exn (* }}} end coercion stuff *) in @@ -1508,7 +1508,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il metasenv subst context pristinehe he hetype' ugraph [] args_bo_and_ty with RefineFailure _ | Uncertain _ as exn -> (* unable to fix arity *) - more_args_than_expected localization_tbl + more_args_than_expected localization_tbl metasenv subst he context hetype args_bo_and_ty exn (* }}} *) in @@ -1523,7 +1523,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il fix_arity metasenv context subst he hetype args_bo_and_ty ugraph with RefineFailure _ | Uncertain _ as exn -> (* unable to fix arity *) - more_args_than_expected localization_tbl + more_args_than_expected localization_tbl metasenv subst he context hetype args_bo_and_ty exn in let coerced_args,subst,metasenv,he,t,ugraph =