X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=8bdb409e923ed19387be8a66fb1b765492ceb582;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=7e0996f4f59ef693050b9aef47d03b941c56934a;hpb=8b55faddb06e3c4b0a13839210bb49170939b33e;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 7e0996f4f..8bdb409e9 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -29,11 +29,11 @@ open DisambiguateTypes open UriManager exception No_choices of domain_item -exception NoWellTypedInterpretation +exception NoWellTypedInterpretation of string Lazy.t list exception PathNotWellFormed (** raised when an environment is not enough informative to decide *) -exception Try_again +exception Try_again of string Lazy.t type aliases = bool * DisambiguateTypes.environment @@ -56,43 +56,40 @@ let descr_of_domain_item = function type 'a test_result = | Ok of 'a * Cic.metasenv - | Ko - | Uncertain + | Ko of string Lazy.t + | Uncertain of string Lazy.t let refine_term metasenv context uri term ugraph = (* if benchmark then incr actual_refinements; *) assert (uri=None); - let metasenv, term = - CicMkImplicit.expand_implicits metasenv [] context term in debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term))); try let term', _, metasenv',ugraph1 = CicRefine.type_of_aux' metasenv context term ugraph in (Ok (term', metasenv')),ugraph1 with - | CicRefine.Uncertain s -> - debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force s) ^ "] " ^ CicPp.ppterm term)) ; - Uncertain,ugraph + | CicRefine.Uncertain msg -> + debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ; + Uncertain (msg (*lazy ("Uncertain trying to refine: " ^ CicMetaSubst.ppterm_in_context [] term context ^ "\n" ^ Lazy.force msg)*)),ugraph | CicRefine.RefineFailure msg -> debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" (CicPp.ppterm term) (Lazy.force msg))); - Ko,ugraph + Ko (msg (*lazy ("Error trying to refine: " ^ CicMetaSubst.ppterm_in_context [] term context ^ "\n" ^ Lazy.force msg)*)),ugraph let refine_obj metasenv context uri obj ugraph = assert (context = []); - let metasenv, obj = CicMkImplicit.expand_implicits_in_obj metasenv [] obj in debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj))) ; try let obj', metasenv,ugraph = CicRefine.typecheck metasenv uri obj in (Ok (obj', metasenv)),ugraph with - | CicRefine.Uncertain s -> - debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force s) ^ "] " ^ CicPp.ppobj obj)) ; - Uncertain,ugraph + | CicRefine.Uncertain msg -> + debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppobj obj)) ; + Uncertain (msg (*lazy ("Uncertain trying to refine: " ^ CicPp.ppobj obj ^ "\n" ^ Lazy.force msg)*)),ugraph | CicRefine.RefineFailure msg -> debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" (CicPp.ppobj obj) (Lazy.force msg))) ; - Ko,ugraph + Ko (msg (*lazy ("Error trying to refine: " ^ CicPp.ppobj obj ^ "\n" ^ Lazy.force msg)*)),ugraph let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () = try @@ -152,21 +149,27 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast = let (indtype_uri, indtype_no) = match indty_ident with | Some (indty_ident, _) -> - (match resolve env (Id indty_ident) () with + (match resolve env (Id indty_ident) () with | Cic.MutInd (uri, tyno, _) -> (uri, tyno) - | Cic.Implicit _ -> raise Try_again - | _ -> raise Invalid_choice) + | Cic.Implicit _ -> + raise (Try_again (lazy "The type of the term to be matched + is still unknown")) + | _ -> + raise (Invalid_choice (lazy "The type of the term to be matched is not (co)inductive!"))) | None -> let fst_constructor = match branches with | ((head, _, _), _) :: _ -> head - | [] -> raise Invalid_choice + | [] -> raise (Invalid_choice (lazy "The type of the term to be matched is an inductive type without constructors that cannot be determined")) in (match resolve env (Id fst_constructor) () with | Cic.MutConstruct (indtype_uri, indtype_no, _, _) -> (indtype_uri, indtype_no) - | Cic.Implicit _ -> raise Try_again - | _ -> raise Invalid_choice) + | Cic.Implicit _ -> + raise (Try_again (lazy "The type of the term to be matched + is still unknown")) + | _ -> + raise (Invalid_choice (lazy "The type of the term to be matched is not (co)inductive!"))) in Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term, (List.map do_branch branches)) @@ -216,14 +219,37 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast = | `Inductive -> (fun (var, _, _, _) cic -> incr counter; - Cic.LetIn (Cic.Name var, Cic.Fix (!counter, funs), cic)) + let fix = Cic.Fix (!counter,funs) in + match cic with + Cic.Rel 1 -> fix + | (Cic.Appl (Cic.Rel 1::l)) -> + (try + let l' = + List.map + (function t -> + let t',subst,metasenv = + CicMetaSubst.delift_rels [] [] 1 t + in + assert (subst=[]); + assert (metasenv=[]); + t') l + in + Cic.Appl (fix::l') + with + CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> + Cic.LetIn (Cic.Name var, fix, cic)) + | _ -> Cic.LetIn (Cic.Name var, fix, cic)) | `CoInductive -> let funs = List.map (fun (name, _, typ, body) -> (name, typ, body)) funs in (fun (var, _, _, _) cic -> incr counter; - Cic.LetIn (Cic.Name var, Cic.CoFix (!counter, funs), cic)) + let cofix = Cic.CoFix (!counter,funs) in + match cic with + Cic.Rel 1 -> cofix + | (Cic.Appl (Cic.Rel 1::l)) -> Cic.Appl (cofix::l) + | _ -> Cic.LetIn (Cic.Name var, cofix, cic)) in List.fold_right (build_term inductiveFuns) inductiveFuns cic_body | CicNotationPt.Ident _ @@ -258,7 +284,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast = (try List.assoc s ids_to_uris, aux loc context term with Not_found -> - raise Invalid_choice)) + raise (Invalid_choice (lazy "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on")))) subst | None -> List.map (fun uri -> uri, Cic.Implicit None) uris) in @@ -302,10 +328,10 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast = *) t | _ -> - raise Invalid_choice + raise (Invalid_choice (lazy "??? Can this happen?")) with CicEnvironment.CircularDependency _ -> - raise Invalid_choice)) + raise (Invalid_choice (lazy "Circular dependency in the environment")))) | CicNotationPt.Implicit -> Cic.Implicit None | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole) | CicNotationPt.Num (num, i) -> resolve env (Num i) ~num () @@ -788,18 +814,19 @@ let foo () = (k , ugraph1 ) in refine_profiler.HExtlib.profile foo () with - | Try_again -> Uncertain, ugraph - | Invalid_choice -> Ko, ugraph + | Try_again msg -> Uncertain msg, ugraph + | Invalid_choice msg -> Ko msg, ugraph in (* (4) build all possible interpretations *) + let (@@) (l1,l2) (l1',l2') = l1@l1', l2@l2' in let rec aux aliases diff lookup_in_todo_dom todo_dom base_univ = match todo_dom with | [] -> assert (lookup_in_todo_dom = None); (match test_env aliases [] base_univ with | Ok (thing, metasenv),new_univ -> - [ aliases, diff, metasenv, thing, new_univ ] - | Ko,_ | Uncertain,_ -> []) + [ aliases, diff, metasenv, thing, new_univ ], [] + | Ko msg,_ | Uncertain msg,_ -> [],[msg]) | item :: remaining_dom -> debug_print (lazy (sprintf "CHOOSED ITEM: %s" (string_of_domain_item item))); @@ -808,7 +835,7 @@ in refine_profiler.HExtlib.profile foo () None -> lookup_choices item | Some choices -> choices in match choices with - [] -> [] + [] -> [], [lazy "No choices"] | [codomain_item] -> (* just one choice. We perform a one-step look-up and if the next set of choices is also a singleton we @@ -830,20 +857,21 @@ in refine_profiler.HExtlib.profile foo () (match test_env new_env remaining_dom base_univ with | Ok (thing, metasenv),new_univ -> (match remaining_dom with - | [] -> [ new_env, new_diff, metasenv, thing, new_univ ] + | [] -> + [ new_env, new_diff, metasenv, thing, new_univ ], [] | _ -> aux new_env new_diff lookup_in_todo_dom remaining_dom new_univ) - | Uncertain,new_univ -> + | Uncertain msg,new_univ -> (match remaining_dom with - | [] -> [] + | [] -> [], [msg] | _ -> aux new_env new_diff lookup_in_todo_dom remaining_dom new_univ) - | Ko,_ -> []) + | Ko msg,_ -> [], [msg]) | _::_ -> let rec filter univ = function - | [] -> [] + | [] -> [],[] | codomain_item :: tl -> debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item))); let new_env = Environment.add item codomain_item aliases in @@ -851,17 +879,17 @@ in refine_profiler.HExtlib.profile foo () (match test_env new_env remaining_dom univ with | Ok (thing, metasenv),new_univ -> (match remaining_dom with - | [] -> [ new_env, new_diff, metasenv, thing, new_univ ] + | [] -> [ new_env, new_diff, metasenv, thing, new_univ ], [] | _ -> aux new_env new_diff None remaining_dom new_univ - ) @ + ) @@ filter univ tl - | Uncertain,new_univ -> + | Uncertain msg,new_univ -> (match remaining_dom with - | [] -> [] + | [] -> [],[msg] | _ -> aux new_env new_diff None remaining_dom new_univ - ) @ + ) @@ filter univ tl - | Ko,_ -> filter univ tl) + | Ko msg,_ -> ([],[msg]) @@ filter univ tl) in filter base_univ choices in @@ -869,11 +897,11 @@ in refine_profiler.HExtlib.profile foo () try let res = match aux aliases [] None todo_dom base_univ with - | [] -> raise NoWellTypedInterpretation - | [_,diff,metasenv,t,ugraph] -> + | [],errors -> raise (NoWellTypedInterpretation errors) + | [_,diff,metasenv,t,ugraph],_ -> debug_print (lazy "SINGLE INTERPRETATION"); [diff,metasenv,t,ugraph], false - | l -> + | l,_ -> debug_print (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l))); let choices = List.map