X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=667c50770536bb7187df52a2cc460991b32cf20f;hb=f1dc70ca55058b2983cd23b829d856df3b41b9a7;hp=f203e6d790edc4b2cc6e413afa8e1c40c6935964;hpb=8523a35427aa3fdf40a0e14b8aac3428c8aa13f0;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index f203e6d79..667c50770 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -23,17 +23,20 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf open DisambiguateTypes open UriManager -exception No_choices of domain_item -exception NoWellTypedInterpretation +(* the integer is an offset to be added to each location *) +exception NoWellTypedInterpretation of + int * (Token.flocation option * 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,40 +59,56 @@ let descr_of_domain_item = function type 'a test_result = | Ok of 'a * Cic.metasenv - | Ko - | Uncertain + | Ko of Token.flocation option * string Lazy.t + | Uncertain of Token.flocation option * string Lazy.t -let refine_term metasenv context uri term ugraph = +let refine_term metasenv context uri term ugraph ~localization_tbl = (* if benchmark then incr actual_refinements; *) assert (uri=None); debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term))); try let term', _, metasenv',ugraph1 = - CicRefine.type_of_aux' metasenv context term ugraph in + CicRefine.type_of_aux' metasenv context term ugraph ~localization_tbl in (Ok (term', metasenv')),ugraph1 with - | CicRefine.Uncertain s -> - debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force s) ^ "] " ^ CicPp.ppterm term)) ; - Uncertain,ugraph - | CicRefine.RefineFailure msg -> - debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" - (CicPp.ppterm term) (Lazy.force msg))); - Ko,ugraph - -let refine_obj metasenv context uri obj ugraph = + exn -> + let rec process_exn loc = + function + HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn + | CicRefine.Uncertain msg -> + debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ; + Uncertain (loc,msg),ugraph + | CicRefine.RefineFailure msg -> + debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" + (CicPp.ppterm term) (Lazy.force msg))); + Ko (loc,msg),ugraph + | exn -> raise exn + in + process_exn None exn + +let refine_obj metasenv context uri obj ugraph ~localization_tbl = assert (context = []); debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj))) ; try - let obj', metasenv,ugraph = CicRefine.typecheck metasenv uri obj in + let obj', metasenv,ugraph = + CicRefine.typecheck metasenv uri obj ~localization_tbl + in (Ok (obj', metasenv)),ugraph with - | CicRefine.Uncertain s -> - debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force s) ^ "] " ^ CicPp.ppobj obj)) ; - Uncertain,ugraph - | CicRefine.RefineFailure msg -> - debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" - (CicPp.ppobj obj) (Lazy.force msg))) ; - Ko,ugraph + exn -> + let rec process_exn loc = + function + HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn + | CicRefine.Uncertain msg -> + debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppobj obj)) ; + Uncertain (loc,msg),ugraph + | CicRefine.RefineFailure msg -> + debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" + (CicPp.ppobj obj) (Lazy.force msg))) ; + Ko (loc,msg),ugraph + | exn -> raise exn + in + process_exn None exn let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () = try @@ -99,7 +118,7 @@ let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ? (DisambiguateTypes.string_of_domain_item item)) (* TODO move it to Cic *) -let find_in_context name (context: Cic.name list) = +let find_in_context name context = let rec aux acc = function | [] -> raise Not_found | Cic.Name hd :: tl when hd = name -> acc @@ -107,20 +126,25 @@ let find_in_context name (context: Cic.name list) = in aux 1 context -let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast = +let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast + ~localization_tbl += assert (uri = None); - let rec aux loc (context: Cic.name list) = function + let rec aux ~localize loc (context: Cic.name list) = function | CicNotationPt.AttributedTerm (`Loc loc, term) -> - aux loc context term - | CicNotationPt.AttributedTerm (_, term) -> aux loc context term + let res = aux ~localize loc context term in + if localize then Cic.CicHash.add localization_tbl res loc; + res + | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) -> - let cic_args = List.map (aux loc context) args in + let cic_args = List.map (aux ~localize loc context) args in resolve env (Symbol (symb, i)) ~args:cic_args () - | CicNotationPt.Appl terms -> Cic.Appl (List.map (aux loc context) terms) + | CicNotationPt.Appl terms -> + Cic.Appl (List.map (aux ~localize loc context) terms) | CicNotationPt.Binder (binder_kind, (var, typ), body) -> - let cic_type = aux_option loc context (Some `Type) typ in + let cic_type = aux_option ~localize loc context (Some `Type) typ in let cic_name = CicNotationUtil.cic_name_of_name var in - let cic_body = aux loc (cic_name :: context) body in + let cic_body = aux ~localize loc (cic_name :: context) body in (match binder_kind with | `Lambda -> Cic.Lambda (cic_name, cic_type, cic_body) | `Pi @@ -129,18 +153,18 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast = resolve env (Symbol ("exists", 0)) ~args:[ cic_type; Cic.Lambda (cic_name, cic_type, cic_body) ] ()) | CicNotationPt.Case (term, indty_ident, outtype, branches) -> - let cic_term = aux loc context term in - let cic_outtype = aux_option loc context None outtype in + let cic_term = aux ~localize loc context term in + let cic_outtype = aux_option ~localize loc context None outtype in let do_branch ((head, _, args), term) = let rec do_branch' context = function - | [] -> aux loc context term + | [] -> aux ~localize loc context term | (name, typ) :: tl -> let cic_name = CicNotationUtil.cic_name_of_name name in let cic_body = do_branch' (cic_name :: context) tl in let typ = match typ with | None -> Cic.Implicit (Some `Type) - | Some typ -> aux loc context typ + | Some typ -> aux ~localize loc context typ in Cic.Lambda (cic_name, typ, cic_body) in @@ -149,37 +173,43 @@ 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)) | CicNotationPt.Cast (t1, t2) -> - let cic_t1 = aux loc context t1 in - let cic_t2 = aux loc context t2 in + let cic_t1 = aux ~localize loc context t1 in + let cic_t2 = aux ~localize loc context t2 in Cic.Cast (cic_t1, cic_t2) | CicNotationPt.LetIn ((name, typ), def, body) -> - let cic_def = aux loc context def in + let cic_def = aux ~localize loc context def in let cic_name = CicNotationUtil.cic_name_of_name name in let cic_def = match typ with | None -> cic_def - | Some t -> Cic.Cast (cic_def, aux loc context t) + | Some t -> Cic.Cast (cic_def, aux ~localize loc context t) in - let cic_body = aux loc (cic_name :: context) body in + let cic_body = aux ~localize loc (cic_name :: context) body in Cic.LetIn (cic_name, cic_def, cic_body) | CicNotationPt.LetRec (kind, defs, body) -> let context' = @@ -188,12 +218,50 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast = CicNotationUtil.cic_name_of_name name :: acc) context defs in - let cic_body = aux loc context' body in + let cic_body = + let unlocalized_body = aux ~localize:false loc context' body in + match unlocalized_body with + Cic.Rel 1 -> `AvoidLetInNoAppl + | 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 + (* We can avoid the LetIn. But maybe we need to recompute l' + so that it is localized *) + if localize then + match body with + CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) -> + let l' = List.map (aux ~localize loc context) l in + `AvoidLetIn l' + | _ -> assert false + else + `AvoidLetIn l' + with + CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> + if localize then + `AddLetIn (aux ~localize loc context' body) + else + `AddLetIn unlocalized_body) + | _ -> + if localize then + `AddLetIn (aux ~localize loc context' body) + else + `AddLetIn unlocalized_body + in let inductiveFuns = List.map (fun ((name, typ), body, decr_idx) -> - let cic_body = aux loc context' body in - let cic_type = aux_option loc context (Some `Type) typ in + let cic_body = aux ~localize loc context' body in + let cic_type = + aux_option ~localize loc context (Some `Type) typ in let name = match CicNotationUtil.cic_name_of_name name with | Cic.Anonymous -> @@ -213,16 +281,33 @@ 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 + `Recipe (`AddLetIn cic) -> + `Term (Cic.LetIn (Cic.Name var, fix, cic)) + | `Recipe (`AvoidLetIn l) -> `Term (Cic.Appl (fix::l)) + | `Recipe `AvoidLetInNoAppl -> `Term fix + | `Term t -> `Term (Cic.LetIn (Cic.Name var, fix, t))) | `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 + `Recipe (`AddLetIn cic) -> + `Term (Cic.LetIn (Cic.Name var, cofix, cic)) + | `Recipe (`AvoidLetIn l) -> `Term (Cic.Appl (cofix::l)) + | `Recipe `AvoidLetInNoAppl -> `Term cofix + | `Term t -> `Term (Cic.LetIn (Cic.Name var, cofix, t))) in - List.fold_right (build_term inductiveFuns) inductiveFuns cic_body + (match + List.fold_right (build_term inductiveFuns) inductiveFuns + (`Recipe cic_body) + with + `Recipe _ -> assert false + | `Term t -> t) | CicNotationPt.Ident _ | CicNotationPt.Uri _ when is_path -> raise PathNotWellFormed | CicNotationPt.Ident (name, subst) @@ -253,9 +338,9 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast = List.map (fun (s, term) -> (try - List.assoc s ids_to_uris, aux loc context term + List.assoc s ids_to_uris, aux ~localize 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 @@ -299,17 +384,19 @@ 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 () | CicNotationPt.Meta (index, subst) -> let cic_subst = List.map - (function None -> None | Some term -> Some (aux loc context term)) + (function + None -> None + | Some term -> Some (aux ~localize loc context term)) subst in Cic.Meta (index, cic_subst) @@ -320,22 +407,25 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast = | CicNotationPt.Symbol (symbol, instance) -> resolve env (Symbol (symbol, instance)) () | _ -> assert false (* god bless Bologna *) - and aux_option loc (context: Cic.name list) annotation = function + and aux_option ~localize loc (context: Cic.name list) annotation = function | None -> Cic.Implicit annotation - | Some term -> aux loc context term + | Some term -> aux ~localize loc context term in - match ast with - | CicNotationPt.AttributedTerm (`Loc loc, term) -> aux loc context term - | term -> aux dummy_floc context term + aux ~localize:true HExtlib.dummy_floc context ast let interpretate_path ~context path = - interpretate_term ~context ~env:Environment.empty ~uri:None ~is_path:true path + let localization_tbl = Cic.CicHash.create 23 in + (* here we are throwing away useful localization informations!!! *) + fst ( + interpretate_term ~context ~env:Environment.empty ~uri:None ~is_path:true + path ~localization_tbl, localization_tbl) -let interpretate_obj ~context ~env ~uri ~is_path obj = +let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl = assert (context = []); assert (is_path = false); + let interpretate_term = interpretate_term ~localization_tbl in match obj with - | GrafiteAst.Inductive (params,tyl) -> + | CicNotationPt.Inductive (params,tyl) -> let uri = match uri with Some uri -> uri | None -> assert false in let context,params = let context,res = @@ -357,15 +447,6 @@ let interpretate_obj ~context ~env ~uri ~is_path obj = i + 1,(name,name,Cic.MutInd (uri,i,[]))::res ) (0,[]) tyl) in let con_env = DisambiguateTypes.env_of_list name_to_uris env in - let undebrujin t = - snd - (List.fold_right - (fun (name,_,_,_) (i,t) -> - (*here the explicit_named_substituion is assumed to be of length 0 *) - let t' = Cic.MutInd (uri,i,[]) in - let t = CicSubstitution.subst t' t in - i - 1,t - ) tyl (List.length tyl - 1,t)) in let tyl = List.map (fun (name,b,ty,cl) -> @@ -376,14 +457,14 @@ let interpretate_obj ~context ~env ~uri ~is_path obj = let ty' = add_params (interpretate_term context con_env None false ty) in - name,undebrujin ty' + name,ty' ) cl in name,b,ty',cl' ) tyl in Cic.InductiveDefinition (tyl,[],List.length params,[]) - | GrafiteAst.Record (params,name,ty,fields) -> + | CicNotationPt.Record (params,name,ty,fields) -> let uri = match uri with Some uri -> uri | None -> assert false in let context,params = let context,res = @@ -401,7 +482,7 @@ let interpretate_obj ~context ~env ~uri ~is_path obj = let fields' = snd ( List.fold_left - (fun (context,res) (name,ty) -> + (fun (context,res) (name,ty,_coercion) -> let context' = Cic.Name name :: context in context',(name,interpretate_term context env None false ty)::res ) (context,[]) fields) in @@ -418,10 +499,10 @@ let interpretate_obj ~context ~env ~uri ~is_path obj = concl fields' in let con' = add_params con in let tyl = [name,true,ty',["mk_" ^ name,con']] in - let field_names = List.map fst fields in + let field_names = List.map (fun (x,_,y) -> x,y) fields in Cic.InductiveDefinition (tyl,[],List.length params,[`Class (`Record field_names)]) - | GrafiteAst.Theorem (flavour, name, ty, bo) -> + | CicNotationPt.Theorem (flavour, name, ty, bo) -> let attrs = [`Flavour flavour] in let ty' = interpretate_term [] env None false ty in (match bo with @@ -457,7 +538,7 @@ let rev_uniq = (* "aux" keeps domain in reverse order and doesn't care about duplicates. * Domain item more in deep in the list will be processed first. *) -let rec domain_rev_of_term ?(loc = dummy_floc) context = function +let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function | CicNotationPt.AttributedTerm (`Loc loc, term) -> domain_rev_of_term ~loc context term | CicNotationPt.AttributedTerm (_, term) -> @@ -533,7 +614,8 @@ let rec domain_rev_of_term ?(loc = dummy_floc) context = function where_dom @ defs_dom | CicNotationPt.Ident (name, subst) -> (try - let index = find_in_context name context in + (* the next line can raise Not_found *) + ignore(find_in_context name context); if subst <> None then CicNotationPt.fail loc "Explicit substitutions not allowed here" else @@ -572,12 +654,12 @@ let domain_of_obj ~context ast = assert (context = []); let domain_rev = match ast with - | GrafiteAst.Theorem (_,_,ty,bo) -> + | CicNotationPt.Theorem (_,_,ty,bo) -> (match bo with None -> [] | Some bo -> domain_rev_of_term [] bo) @ domain_of_term [] ty - | GrafiteAst.Inductive (params,tyl) -> + | CicNotationPt.Inductive (params,tyl) -> let dom = List.flatten ( List.rev_map @@ -597,21 +679,21 @@ let domain_of_obj ~context ast = not ( List.exists (fun (name',_) -> name = Id name') params || List.exists (fun (name',_,_,_) -> name = Id name') tyl) ) dom - | GrafiteAst.Record (params,_,ty,fields) -> + | CicNotationPt.Record (params,_,ty,fields) -> let dom = List.flatten - (List.rev_map (fun (_,ty) -> domain_rev_of_term [] ty) fields) in + (List.rev_map (fun (_,ty,_) -> domain_rev_of_term [] ty) fields) in let dom = - List.filter - (fun name-> - not ( List.exists (fun (name',_) -> name = Id name') params - || List.exists (fun (name',_) -> name = Id name') fields) - ) dom - in List.fold_left (fun dom (_,ty) -> domain_rev_of_term [] ty @ dom ) (dom @ domain_rev_of_term [] ty) params + in + List.filter + (fun name-> + not ( List.exists (fun (name',_) -> name = Id name') params + || List.exists (fun (name',_,_) -> name = Id name') fields) + ) dom in rev_uniq domain_rev @@ -647,7 +729,7 @@ sig aliases:DisambiguateTypes.environment ->(* previous interpretation status *) universe:DisambiguateTypes.multiple_environment option -> uri:UriManager.uri option -> (* required only for inductive types *) - GrafiteAst.obj -> + CicNotationPt.obj -> ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * Cic.metasenv * (* new metasenv *) Cic.obj * @@ -658,7 +740,7 @@ end module Make (C: Callbacks) = struct let choices_of_id dbd id = - let uris = MetadataQuery.locate ~dbd id in + let uris = Whelp.locate ~dbd id in let uris = match uris with | [] -> @@ -715,7 +797,6 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" let todo_dom = domain_diff thing_dom current_dom in (* (2) lookup function for any item (Id/Symbol/Num) *) let lookup_choices = - let id_choices = Hashtbl.create 1023 in fun item -> let choices = let lookup_in_library () = @@ -723,7 +804,7 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" | Id id -> choices_of_id dbd id | Symbol (symb, _) -> List.map DisambiguateChoices.mk_choice - (CicNotationRew.lookup_interpretations symb) + (TermAcicContent.lookup_interpretations symb) | Num instance -> DisambiguateChoices.lookup_num_choices () in @@ -731,10 +812,14 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" | None -> lookup_in_library () | Some e -> (try + let item = + match item with + | Symbol (symb, _) -> Symbol (symb, 0) + | item -> item + in Environment.find item e - with Not_found -> lookup_in_library ()) + with Not_found -> []) in - if choices = [] then raise (No_choices item); choices in (* @@ -776,27 +861,31 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" aliases todo_dom in try + let localization_tbl = Cic.CicHash.create 503 in let cic_thing = interpretate_thing ~context:disambiguate_context ~env:filled_env - ~uri ~is_path:false thing + ~uri ~is_path:false thing ~localization_tbl in let foo () = - let k,ugraph1 = refine_thing metasenv context uri cic_thing ugraph in + let k,ugraph1 = + refine_thing metasenv context uri cic_thing ugraph ~localization_tbl + in (k , ugraph1 ) in refine_profiler.HExtlib.profile foo () with - | Try_again -> Uncertain, ugraph - | Invalid_choice -> Ko, ugraph + | Try_again msg -> Uncertain (None,msg), ugraph + | Invalid_choice msg -> Ko (None,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 (loc,msg),_ | Uncertain (loc,msg),_ -> [],[loc,msg]) | item :: remaining_dom -> debug_print (lazy (sprintf "CHOOSED ITEM: %s" (string_of_domain_item item))); @@ -805,7 +894,8 @@ in refine_profiler.HExtlib.profile foo () None -> lookup_choices item | Some choices -> choices in match choices with - [] -> [] + [] -> + [], [None,lazy ("No choices for " ^ string_of_domain_item item)] | [codomain_item] -> (* just one choice. We perform a one-step look-up and if the next set of choices is also a singleton we @@ -827,20 +917,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 (loc,msg),new_univ -> (match remaining_dom with - | [] -> [] + | [] -> [], [loc,msg] | _ -> aux new_env new_diff lookup_in_todo_dom remaining_dom new_univ) - | Ko,_ -> []) + | Ko (loc,msg),_ -> [], [loc,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 @@ -848,17 +939,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 (loc,msg),new_univ -> (match remaining_dom with - | [] -> [] + | [] -> [],[loc,msg] | _ -> aux new_env new_diff None remaining_dom new_univ - ) @ + ) @@ filter univ tl - | Ko,_ -> filter univ tl) + | Ko (loc,msg),_ -> ([],[loc,msg]) @@ filter univ tl) in filter base_univ choices in @@ -866,11 +957,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 (0,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 @@ -911,33 +1002,8 @@ in refine_profiler.HExtlib.profile foo () if fresh_instances then CicNotationUtil.freshen_obj obj else obj in disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri - ~pp_thing:GrafiteAstPp.pp_obj ~domain_of_thing:domain_of_obj + ~pp_thing:CicNotationPp.pp_obj ~domain_of_thing:domain_of_obj ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj obj end -module Trivial = -struct - exception Ambiguous_term of string Lazy.t - exception Exit - module Callbacks = - struct - let interactive_user_uri_choice ~selection_mode ?ok - ?(enable_button_for_non_vars = true) ~title ~msg ~id uris = - raise Exit - let interactive_interpretation_choice interp = raise Exit - let input_or_locate_uri ~(title:string) ?id = raise Exit - end - module Disambiguator = Make (Callbacks) - let disambiguate_string ~dbd ?(context = []) ?(metasenv = []) ?initial_ugraph - ?(aliases = DisambiguateTypes.Environment.empty) term - = - let ast = - CicNotationParser.parse_level2_ast (Ulexing.from_utf8_string term) - in - try - fst (Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast - ?initial_ugraph ~aliases ~universe:None) - with Exit -> raise (Ambiguous_term (lazy term)) -end -