X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_disambiguation%2Fdisambiguate.ml;h=d58dc9854bceef447083e2ff628bfe99ef6eee91;hb=cc23f034c9419186602d9250456241f2eba90d7c;hp=bfeb65d37ea2d39888abb3303026ead0ad5d62e7;hpb=d4232ba846e48a959637d94445f169deca5464b4;p=helm.git diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml index bfeb65d37..d58dc9854 100644 --- a/helm/software/components/cic_disambiguation/disambiguate.ml +++ b/helm/software/components/cic_disambiguation/disambiguate.ml @@ -30,9 +30,14 @@ open Printf open DisambiguateTypes open UriManager +module Ast = CicNotationPt + (* the integer is an offset to be added to each location *) exception NoWellTypedInterpretation of - int * ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * Token.flocation option * string Lazy.t) list + int * + ((Stdpp.location list * string * string) list * + (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * + Stdpp.location option * string Lazy.t * bool) list exception PathNotWellFormed (** raised when an environment is not enough informative to decide *) @@ -41,6 +46,46 @@ exception Try_again of string Lazy.t type aliases = bool * DisambiguateTypes.environment type 'a disambiguator_input = string * int * 'a +type domain = domain_tree list +and domain_tree = Node of Stdpp.location list * domain_item * domain + +let rec string_of_domain = + function + [] -> "" + | Node (_,domain_item,l)::tl -> + DisambiguateTypes.string_of_domain_item domain_item ^ + " [ " ^ string_of_domain l ^ " ] " ^ string_of_domain tl + +let rec filter_map_domain f = + function + [] -> [] + | Node (locs,domain_item,l)::tl -> + match f locs domain_item with + None -> filter_map_domain f l @ filter_map_domain f tl + | Some res -> res :: filter_map_domain f l @ filter_map_domain f tl + +let rec map_domain f = + function + [] -> [] + | Node (locs,domain_item,l)::tl -> + f locs domain_item :: map_domain f l @ map_domain f tl + +let uniq_domain dom = + let rec aux seen = + function + [] -> seen,[] + | Node (locs,domain_item,l)::tl -> + if List.mem domain_item seen then + let seen,l = aux seen l in + let seen,tl = aux seen tl in + seen, l @ tl + else + let seen,l = aux (domain_item::seen) l in + let seen,tl = aux seen tl in + seen, Node (locs,domain_item,l)::tl + in + snd (aux [] dom) + let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) else () @@ -60,8 +105,8 @@ let descr_of_domain_item = function type 'a test_result = | Ok of 'a * Cic.metasenv - | Ko of Token.flocation option * string Lazy.t - | Uncertain of Token.flocation option * string Lazy.t + | Ko of Stdpp.location option * string Lazy.t + | Uncertain of Stdpp.location option * string Lazy.t let refine_term metasenv context uri term ugraph ~localization_tbl = (* if benchmark then incr actual_refinements; *) @@ -127,9 +172,10 @@ let find_in_context name context = in aux 1 context -let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast +let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~uri ~is_path ast ~localization_tbl = + (* create_dummy_ids shouldbe used only for interpretating patterns *) assert (uri = None); let rec aux ~localize loc (context: Cic.name list) = function | CicNotationPt.AttributedTerm (`Loc loc, term) -> @@ -157,21 +203,24 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast 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 ~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 ~localize loc context typ - in - Cic.Lambda (cic_name, typ, cic_body) - in + let rec do_branch' context = function + | [] -> 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 ~localize loc context typ + in + Cic.Lambda (cic_name, typ, cic_body) + in do_branch' context args in - let (indtype_uri, indtype_no) = + let indtype_uri, indtype_no = + if create_dummy_ids then + (UriManager.uri_of_string "cic:/fake_indty.con", 0) + else match indty_ident with | Some (indty_ident, _) -> (match resolve env (Id indty_ident) () with @@ -180,21 +229,112 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast 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!"))) + raise (Invalid_choice (Some loc, 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 (lazy "The type of the term to be matched is an inductive type without constructors that cannot be determined")) + let rec fst_constructor = + function + (Ast.Pattern (head, _, _), _) :: _ -> head + | (Ast.Wildcard, _) :: tl -> fst_constructor tl + | [] -> raise (Invalid_choice (Some loc, lazy "The type of the term to be matched cannot be determined because it is an inductive type without constructors or because all patterns use wildcards")) in - (match resolve env (Id fst_constructor) () with + (match resolve env (Id (fst_constructor branches)) () with | Cic.MutConstruct (indtype_uri, indtype_no, _, _) -> (indtype_uri, indtype_no) | 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!"))) + raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!"))) + in + let branches = + if create_dummy_ids then + List.map + (function + Ast.Wildcard,term -> ("wildcard",None,[]), term + | Ast.Pattern _,_ -> + raise (Invalid_choice (Some loc, lazy "Syntax error: the left hand side of a branch patterns must be \"_\"")) + ) branches + else + match fst(CicEnvironment.get_obj CicUniv.empty_ugraph indtype_uri) with + Cic.InductiveDefinition (il,_,leftsno,_) -> + let _,_,_,cl = + try + List.nth il indtype_no + with _ -> assert false + in + let rec count_prod t = + match CicReduction.whd [] t with + Cic.Prod (_, _, t) -> 1 + (count_prod t) + | _ -> 0 + in + let rec sort branches cl = + match cl with + [] -> + let rec analyze unused unrecognized useless = + function + [] -> + if unrecognized != [] then + raise (Invalid_choice + (Some loc, + lazy + ("Unrecognized constructors: " ^ + String.concat " " unrecognized))) + else if useless > 0 then + raise (Invalid_choice + (Some loc, + lazy + ("The last " ^ string_of_int useless ^ + "case" ^ if useless > 1 then "s are" else " is" ^ + " unused"))) + else + [] + | (Ast.Wildcard,_)::tl when not unused -> + analyze true unrecognized useless tl + | (Ast.Pattern (head,_,_),_)::tl when not unused -> + analyze unused (head::unrecognized) useless tl + | _::tl -> analyze unused unrecognized (useless + 1) tl + in + analyze false [] 0 branches + | (name,ty)::cltl -> + let rec find_and_remove = + function + [] -> + raise + (Invalid_choice + (Some loc, lazy ("Missing case: " ^ name))) + | ((Ast.Wildcard, _) as branch :: _) as branches -> + branch, branches + | (Ast.Pattern (name',_,_),_) as branch :: tl + when name = name' -> + branch,tl + | branch::tl -> + let found,rest = find_and_remove tl in + found, branch::rest + in + let branch,tl = find_and_remove branches in + match branch with + Ast.Pattern (name,y,args),term -> + if List.length args = count_prod ty - leftsno then + ((name,y,args),term)::sort tl cltl + else + raise + (Invalid_choice + (Some loc, + lazy ("Wrong number of arguments for " ^ name))) + | Ast.Wildcard,term -> + let rec mk_lambdas = + function + 0 -> term + | n -> + CicNotationPt.Binder + (`Lambda, (CicNotationPt.Ident ("_", None), None), + mk_lambdas (n - 1)) + in + (("wildcard",None,[]), + mk_lambdas (count_prod ty - leftsno)) :: sort tl cltl + in + sort branches cl + | _ -> assert false in Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term, (List.map do_branch branches)) @@ -205,13 +345,13 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast | CicNotationPt.LetIn ((name, typ), def, body) -> let cic_def = aux ~localize loc context def in let cic_name = CicNotationUtil.cic_name_of_name name in - let cic_def = + let cic_typ = match typ with - | None -> cic_def - | Some t -> Cic.Cast (cic_def, aux ~localize loc context t) + | None -> Cic.Implicit (Some `Type) + | Some t -> aux ~localize loc context t in let cic_body = aux ~localize loc (cic_name :: context) body in - Cic.LetIn (cic_name, cic_def, cic_body) + Cic.LetIn (cic_name, cic_def, cic_typ, cic_body) | CicNotationPt.LetRec (kind, defs, body) -> let context' = List.fold_left @@ -222,14 +362,14 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast 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) -> + Cic.Rel n when n <= List.length defs -> `AvoidLetInNoAppl n + | Cic.Appl (Cic.Rel n::l) when n <= List.length defs -> (try let l' = List.map (function t -> let t',subst,metasenv = - CicMetaSubst.delift_rels [] [] 1 t + CicMetaSubst.delift_rels [] [] (List.length defs) t in assert (subst=[]); assert (metasenv=[]); @@ -241,10 +381,10 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast match body with CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) -> let l' = List.map (aux ~localize loc context) l in - `AvoidLetIn l' + `AvoidLetIn (n,l') | _ -> assert false else - `AvoidLetIn l' + `AvoidLetIn (n,l') with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> if localize then @@ -279,42 +419,32 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast (name, decr_idx, cic_type, cic_body)) defs in - let counter = ref ~-1 in - let build_term funs = - (* this is the body of the fold_right function below. Rationale: Fix - * and CoFix cases differs only in an additional index in the - * inductiveFun list, see Cic.term *) - match kind with - | `Inductive -> - (fun (var, _, _, _) cic -> - incr counter; - 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))) + let fix_or_cofix n = + match kind with + `Inductive -> Cic.Fix (n,inductiveFuns) | `CoInductive -> - let funs = - List.map (fun (name, _, typ, body) -> (name, typ, body)) funs + let coinductiveFuns = + List.map + (fun (name, _, typ, body) -> name, typ, body) + inductiveFuns in - (fun (var, _, _, _) cic -> - incr counter; - 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))) + Cic.CoFix (n,coinductiveFuns) in - (match - List.fold_right (build_term inductiveFuns) inductiveFuns - (`Recipe cic_body) - with - `Recipe _ -> assert false - | `Term t -> t) + let counter = ref ~-1 in + let build_term funs (var,_,ty,_) t = + incr counter; + Cic.LetIn (Cic.Name var, fix_or_cofix !counter, ty, t) + in + (match cic_body with + `AvoidLetInNoAppl n -> + let n' = List.length inductiveFuns - n in + fix_or_cofix n' + | `AvoidLetIn (n,l) -> + let n' = List.length inductiveFuns - n in + Cic.Appl (fix_or_cofix n'::l) + | `AddLetIn cic_body -> + List.fold_right (build_term inductiveFuns) inductiveFuns + cic_body) | CicNotationPt.Ident _ | CicNotationPt.Uri _ when is_path -> raise PathNotWellFormed | CicNotationPt.Ident (name, subst) @@ -347,7 +477,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast (try List.assoc s ids_to_uris, aux ~localize loc context term with Not_found -> - raise (Invalid_choice (lazy "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on")))) + raise (Invalid_choice (Some loc, 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 @@ -391,10 +521,10 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast *) t | _ -> - raise (Invalid_choice (lazy "??? Can this happen?")) + raise (Invalid_choice (Some loc, lazy "??? Can this happen?")) with CicEnvironment.CircularDependency _ -> - raise (Invalid_choice (lazy "Circular dependency in the environment")))) + raise (Invalid_choice (None, 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 () @@ -424,7 +554,8 @@ let interpretate_path ~context 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 + interpretate_term ~create_dummy_ids:true + ~context ~env:Environment.empty ~uri:None ~is_path:true path ~localization_tbl, localization_tbl) let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl = @@ -529,103 +660,115 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl = let bo' = Some (interpretate_term [] env None false bo) in Cic.Constant (name,bo',ty',[],attrs)) - - (* e.g. [5;1;1;1;2;3;4;1;2] -> [2;1;4;3;5] *) -let rev_uniq = - let module SortedItem = - struct - type t = DisambiguateTypes.domain_item - let compare = Pervasives.compare - end - in - let module Map = Map.Make (SortedItem) in - fun l -> - let rev_l = List.rev l in - let (members, uniq_rev_l) = - List.fold_left - (fun (members, rev_l) (loc,elt) -> - try - let locs = Map.find elt members in - if List.mem loc locs then - members, rev_l - else - Map.add elt (loc::locs) members, rev_l - with - | Not_found -> Map.add elt [loc] members, elt :: rev_l) - (Map.empty, []) rev_l - in - List.rev_map - (fun e -> try Map.find e members,e with Not_found -> assert false) - uniq_rev_l - -(* "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 = HExtlib.dummy_floc) context = function - | CicNotationPt.AttributedTerm (`Loc loc, term) -> - domain_rev_of_term ~loc context term - | CicNotationPt.AttributedTerm (_, term) -> - domain_rev_of_term ~loc context term - | CicNotationPt.Appl terms -> - List.fold_left - (fun dom term -> domain_rev_of_term ~loc context term @ dom) [] terms - | CicNotationPt.Binder (kind, (var, typ), body) -> - let kind_dom = - match kind with - | `Exists -> [ loc, Symbol ("exists", 0) ] - | _ -> [] +let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function + | Ast.AttributedTerm (`Loc loc, term) -> + domain_of_term ~loc ~context term + | Ast.AttributedTerm (_, term) -> + domain_of_term ~loc ~context term + | Ast.Symbol (symbol, instance) -> + [ Node ([loc], Symbol (symbol, instance), []) ] + (* to be kept in sync with Ast.Appl (Ast.Symbol ...) *) + | Ast.Appl (Ast.Symbol (symbol, instance) as hd :: args) + | Ast.Appl (Ast.AttributedTerm (_,Ast.Symbol (symbol, instance)) as hd :: args) + -> + let args_dom = + List.fold_right + (fun term acc -> domain_of_term ~loc ~context term @ acc) + args [] in + let loc = + match hd with + Ast.AttributedTerm (`Loc loc,_) -> loc + | _ -> loc in - let type_dom = domain_rev_of_term_option ~loc context typ in - let body_dom = - domain_rev_of_term ~loc - (CicNotationUtil.cic_name_of_name var :: context) body + [ Node ([loc], Symbol (symbol, instance), args_dom) ] + | Ast.Appl (Ast.Ident (name, subst) as hd :: args) + | Ast.Appl (Ast.AttributedTerm (_,Ast.Ident (name, subst)) as hd :: args) -> + let args_dom = + List.fold_right + (fun term acc -> domain_of_term ~loc ~context term @ acc) + args [] in + let loc = + match hd with + Ast.AttributedTerm (`Loc loc,_) -> loc + | _ -> loc in - body_dom @ type_dom @ kind_dom - | CicNotationPt.Case (term, indty_ident, outtype, branches) -> - let term_dom = domain_rev_of_term ~loc context term in - let outtype_dom = domain_rev_of_term_option loc context outtype in - let get_first_constructor = function + (try + (* the next line can raise Not_found *) + ignore(find_in_context name context); + if subst <> None then + Ast.fail loc "Explicit substitutions not allowed here" + else + args_dom + with Not_found -> + (match subst with + | None -> [ Node ([loc], Id name, args_dom) ] + | Some subst -> + let terms = + List.fold_left + (fun dom (_, term) -> + let dom' = domain_of_term ~loc ~context term in + dom @ dom') + [] subst in + [ Node ([loc], Id name, terms @ args_dom) ])) + | Ast.Appl terms -> + List.fold_right + (fun term acc -> domain_of_term ~loc ~context term @ acc) + terms [] + | Ast.Binder (kind, (var, typ), body) -> + let type_dom = domain_of_term_option ~loc ~context typ in + let body_dom = + domain_of_term ~loc + ~context:(CicNotationUtil.cic_name_of_name var :: context) body in + (match kind with + | `Exists -> [ Node ([loc], Symbol ("exists", 0), (type_dom @ body_dom)) ] + | _ -> type_dom @ body_dom) + | Ast.Case (term, indty_ident, outtype, branches) -> + let term_dom = domain_of_term ~loc ~context term in + let outtype_dom = domain_of_term_option ~loc ~context outtype in + let rec get_first_constructor = function | [] -> [] - | ((head, _, _), _) :: _ -> [ loc, Id head ] - in - let do_branch ((head, _, args), term) = - let (term_context, args_domain) = - List.fold_left - (fun (cont, dom) (name, typ) -> - (CicNotationUtil.cic_name_of_name name :: cont, - (match typ with - | None -> dom - | Some typ -> domain_rev_of_term ~loc cont typ @ dom))) - (context, []) args - in - args_domain @ domain_rev_of_term ~loc term_context term + | (Ast.Pattern (head, _, _), _) :: _ -> [ Node ([loc], Id head, []) ] + | _ :: tl -> get_first_constructor tl in + let do_branch = + function + Ast.Pattern (head, _, args), term -> + let (term_context, args_domain) = + List.fold_left + (fun (cont, dom) (name, typ) -> + (CicNotationUtil.cic_name_of_name name :: cont, + (match typ with + | None -> dom + | Some typ -> dom @ domain_of_term ~loc ~context:cont typ))) + (context, []) args + in + domain_of_term ~loc ~context:term_context term @ args_domain + | Ast.Wildcard, term -> + domain_of_term ~loc ~context term in let branches_dom = - List.fold_left (fun dom branch -> do_branch branch @ dom) [] branches - in - branches_dom @ outtype_dom @ term_dom @ + List.fold_left (fun dom branch -> dom @ do_branch branch) [] branches in (match indty_ident with | None -> get_first_constructor branches - | Some (ident, _) -> [ loc, Id ident ]) - | CicNotationPt.Cast (term, ty) -> - let term_dom = domain_rev_of_term ~loc context term in - let ty_dom = domain_rev_of_term ~loc context ty in - ty_dom @ term_dom - | CicNotationPt.LetIn ((var, typ), body, where) -> - let body_dom = domain_rev_of_term ~loc context body in - let type_dom = domain_rev_of_term_option loc context typ in + | Some (ident, _) -> [ Node ([loc], Id ident, []) ]) + @ term_dom @ outtype_dom @ branches_dom + | Ast.Cast (term, ty) -> + let term_dom = domain_of_term ~loc ~context term in + let ty_dom = domain_of_term ~loc ~context ty in + term_dom @ ty_dom + | Ast.LetIn ((var, typ), body, where) -> + let body_dom = domain_of_term ~loc ~context body in + let type_dom = domain_of_term_option ~loc ~context typ in let where_dom = - domain_rev_of_term ~loc - (CicNotationUtil.cic_name_of_name var :: context) where - in - where_dom @ type_dom @ body_dom - | CicNotationPt.LetRec (kind, defs, where) -> + domain_of_term ~loc + ~context:(CicNotationUtil.cic_name_of_name var :: context) where in + body_dom @ type_dom @ where_dom + | Ast.LetRec (kind, defs, where) -> let add_defs context = List.fold_left (fun acc (_, (var, _), _, _) -> CicNotationUtil.cic_name_of_name var :: acc ) context defs in - let where_dom = domain_rev_of_term ~loc (add_defs context) where in + let where_dom = domain_of_term ~loc ~context:(add_defs context) where in let defs_dom = List.fold_left (fun dom (params, (_, typ), body, _) -> @@ -635,112 +778,108 @@ let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function (fun acc (var,_) -> CicNotationUtil.cic_name_of_name var :: acc) context params) in - domain_rev_of_term ~loc context' body @ - domain_rev_of_term_option ~loc context typ @ List.rev (snd (List.fold_left (fun (context,res) (var,ty) -> CicNotationUtil.cic_name_of_name var :: context, - res @ domain_rev_of_term_option ~loc context ty) + domain_of_term_option ~loc ~context ty @ res) (add_defs context,[]) params)) + @ domain_of_term_option ~loc ~context:context' typ + @ domain_of_term ~loc ~context:context' body ) [] defs in - where_dom @ defs_dom - | CicNotationPt.Ident (name, subst) -> + defs_dom @ where_dom + | Ast.Ident (name, subst) -> (try (* 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" + Ast.fail loc "Explicit substitutions not allowed here" else [] with Not_found -> (match subst with - | None -> [loc, Id name] + | None -> [ Node ([loc], Id name, []) ] | Some subst -> - List.fold_left - (fun dom (_, term) -> - let dom' = domain_rev_of_term ~loc context term in - dom' @ dom) - [loc, Id name] subst)) - | CicNotationPt.Uri _ -> [] - | CicNotationPt.Implicit -> [] - | CicNotationPt.Num (num, i) -> [loc, Num i ] - | CicNotationPt.Meta (index, local_context) -> + let terms = + List.fold_left + (fun dom (_, term) -> + let dom' = domain_of_term ~loc ~context term in + dom @ dom') + [] subst in + [ Node ([loc], Id name, terms) ])) + | Ast.Uri _ -> [] + | Ast.Implicit -> [] + | Ast.Num (num, i) -> [ Node ([loc], Num i, []) ] + | Ast.Meta (index, local_context) -> List.fold_left - (fun dom term -> domain_rev_of_term_option loc context term @ dom) [] - local_context - | CicNotationPt.Sort _ -> [] - | CicNotationPt.Symbol (symbol, instance) -> [loc, Symbol (symbol, instance) ] - | CicNotationPt.UserInput - | CicNotationPt.Literal _ - | CicNotationPt.Layout _ - | CicNotationPt.Magic _ - | CicNotationPt.Variable _ -> assert false + (fun dom term -> dom @ domain_of_term_option ~loc ~context term) + [] local_context + | Ast.Sort _ -> [] + | Ast.UserInput + | Ast.Literal _ + | Ast.Layout _ + | Ast.Magic _ + | Ast.Variable _ -> assert false -and domain_rev_of_term_option ~loc context = function +and domain_of_term_option ~loc ~context = function | None -> [] - | Some t -> domain_rev_of_term ~loc context t + | Some t -> domain_of_term ~loc ~context t -let domain_of_term ~context ast = rev_uniq (domain_rev_of_term context ast) +let domain_of_term ~context term = + uniq_domain (domain_of_term ~context term) let domain_of_obj ~context ast = assert (context = []); - let domain_rev = match ast with - | CicNotationPt.Theorem (_,_,ty,bo) -> - (match bo with + | Ast.Theorem (_,_,ty,bo) -> + domain_of_term [] ty + @ (match bo with None -> [] - | Some bo -> domain_rev_of_term [] bo) @ - domain_rev_of_term [] ty - | CicNotationPt.Inductive (params,tyl) -> - let dom = - List.flatten ( - List.rev_map - (fun (_,_,ty,cl) -> - List.flatten ( - List.rev_map - (fun (_,ty) -> domain_rev_of_term [] ty) cl) @ - domain_rev_of_term [] ty) tyl) in - let dom = + | Some bo -> domain_of_term [] bo) + | Ast.Inductive (params,tyl) -> + let context, dom = List.fold_left - (fun dom (_,ty) -> + (fun (context, dom) (var, ty) -> + let context' = CicNotationUtil.cic_name_of_name var :: context in match ty with - None -> dom - | Some ty -> domain_rev_of_term [] ty @ dom - ) dom params - in - List.filter - (fun (_,name) -> - not ( List.exists (fun (name',_) -> - match CicNotationUtil.cic_name_of_name name' with - Cic.Anonymous -> false - | Cic.Name name' -> name = Id name') params - || List.exists (fun (name',_,_,_) -> name = Id name') tyl) - ) dom - | CicNotationPt.Record (params,_,ty,fields) -> - let dom = - List.flatten - (List.rev_map (fun (_,ty,_,_) -> domain_rev_of_term [] ty) fields) in - let dom = + None -> context', dom + | Some ty -> context', dom @ domain_of_term context ty + ) ([], []) params in + let context_w_types = + List.rev_map + (fun (var, _, _, _) -> Cic.Name var) tyl + @ context in + dom + @ List.flatten ( + List.map + (fun (_,_,ty,cl) -> + domain_of_term context ty + @ List.flatten ( + List.map + (fun (_,ty) -> domain_of_term context_w_types ty) cl)) + tyl) + | CicNotationPt.Record (params,var,ty,fields) -> + let context, dom = List.fold_left - (fun dom (_,ty) -> + (fun (context, dom) (var, ty) -> + let context' = CicNotationUtil.cic_name_of_name var :: context in match ty with - None -> dom - | Some ty -> domain_rev_of_term [] ty @ dom - ) (dom @ domain_rev_of_term [] ty) params - in - List.filter - (fun (_,name) -> - not ( List.exists (fun (name',_) -> - match CicNotationUtil.cic_name_of_name name' with - Cic.Anonymous -> false - | Cic.Name name' -> name = Id name') params - || List.exists (fun (name',_,_,_) -> name = Id name') fields) - ) dom - in - rev_uniq domain_rev + None -> context', dom + | Some ty -> context', dom @ domain_of_term context ty + ) ([], []) params in + let context_w_types = Cic.Name var :: context in + dom + @ domain_of_term context ty + @ snd + (List.fold_left + (fun (context,res) (name,ty,_,_) -> + Cic.Name name::context, res @ domain_of_term context ty + ) (context_w_types,[]) fields) + +let domain_of_obj ~context obj = + uniq_domain (domain_of_obj ~context obj) (* dom1 \ dom2 *) let domain_diff dom1 dom2 = @@ -759,13 +898,19 @@ let domain_diff dom1 dom2 = | item -> elt = item ) dom2 in - List.filter (fun (_,elt) -> not (is_in_dom2 elt)) dom1 + let rec aux = + function + [] -> [] + | Node (_,elt,l)::tl when is_in_dom2 elt -> aux (l @ tl) + | Node (loc,elt,l)::tl -> Node (loc,elt,aux l)::(aux tl) + in + aux dom1 module type Disambiguator = sig val disambiguate_term : ?fresh_instances:bool -> - dbd:HMysql.dbd -> + dbd:HSql.dbd -> context:Cic.context -> metasenv:Cic.metasenv -> ?initial_ugraph:CicUniv.universe_graph -> @@ -780,11 +925,11 @@ sig val disambiguate_obj : ?fresh_instances:bool -> - dbd:HMysql.dbd -> + dbd:HSql.dbd -> aliases:DisambiguateTypes.environment ->(* previous interpretation status *) universe:DisambiguateTypes.multiple_environment option -> uri:UriManager.uri option -> (* required only for inductive types *) - CicNotationPt.obj disambiguator_input -> + CicNotationPt.term CicNotationPt.obj disambiguator_input -> ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * Cic.metasenv * (* new metasenv *) Cic.obj * @@ -843,8 +988,8 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" in debug_print (lazy ("TERM IS: " ^ (pp_thing thing))); let thing_dom = domain_of_thing ~context:disambiguate_context thing in - debug_print (lazy (sprintf "DISAMBIGUATION DOMAIN: %s" - (string_of_domain (List.map snd thing_dom)))); + debug_print + (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"(string_of_domain thing_dom))); (* debug_print (lazy (sprintf "DISAMBIGUATION ENVIRONMENT: %s" (DisambiguatePp.pp_environment aliases))); @@ -852,9 +997,10 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" (match universe with None -> "None" | Some _ -> "Some _"))); *) let current_dom = - Environment.fold (fun item _ dom -> item :: dom) aliases [] - in + Environment.fold (fun item _ dom -> item :: dom) aliases [] in let todo_dom = domain_diff thing_dom current_dom in + debug_print + (lazy (sprintf "DISAMBIGUATION DOMAIN AFTER DIFF: %s"(string_of_domain todo_dom))); (* (2) lookup function for any item (Id/Symbol/Num) *) let lookup_choices = fun item -> @@ -863,8 +1009,11 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" match item with | Id id -> choices_of_id dbd id | Symbol (symb, _) -> - List.map DisambiguateChoices.mk_choice + (try + List.map DisambiguateChoices.mk_choice (TermAcicContent.lookup_interpretations symb) + with + TermAcicContent.Interpretation_not_found -> []) | Num instance -> DisambiguateChoices.lookup_num_choices () in @@ -910,16 +1059,19 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" (* (3) test an interpretation filling with meta uninterpreted identifiers *) let test_env aliases todo_dom ugraph = - let filled_env = - List.fold_left - (fun env (_,item) -> - Environment.add item - ("Implicit", - (match item with - | Id _ | Num _ -> (fun _ _ _ -> Cic.Implicit (Some `Closed)) - | Symbol _ -> (fun _ _ _ -> Cic.Implicit None))) env) - aliases todo_dom - in + let rec aux env = function + | [] -> env + | Node (_, item, l) :: tl -> + let env = + Environment.add item + ("Implicit", + (match item with + | Id _ | Num _ -> + (fun _ _ _ -> Cic.Implicit (Some `Closed)) + | Symbol _ -> (fun _ _ _ -> Cic.Implicit None))) + env in + aux (aux env l) tl in + let filled_env = aux aliases todo_dom in try let localization_tbl = Cic.CicHash.create 503 in let cic_thing = @@ -934,19 +1086,24 @@ let foo () = in refine_profiler.HExtlib.profile foo () with | Try_again msg -> Uncertain (None,msg), ugraph - | Invalid_choice msg -> Ko (None,msg), ugraph + | Invalid_choice (loc,msg) -> Ko (loc,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 = + let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in + (* aux returns triples Ok/Uncertain/Ko *) + (* rem_dom is the concatenation of all the remainin domains *) + let rec aux aliases diff lookup_in_todo_dom todo_dom rem_dom base_univ = + debug_print (lazy ("ZZZ: " ^ string_of_domain todo_dom)); match todo_dom with | [] -> assert (lookup_in_todo_dom = None); - (match test_env aliases [] base_univ with + (match test_env aliases rem_dom base_univ with | Ok (thing, metasenv),new_univ -> - [ aliases, diff, metasenv, thing, new_univ ], [] - | Ko (loc,msg),_ | Uncertain (loc,msg),_ -> [],[diff,loc,msg]) - | (locs,item) :: remaining_dom -> + [ aliases, diff, metasenv, thing, new_univ ], [], [] + | Ko (loc,msg),_ -> [],[],[aliases,diff,loc,msg,true] + | Uncertain (loc,msg),new_univ -> + [],[aliases,diff,loc,msg,new_univ],[]) + | Node (locs,item,inner_dom) :: remaining_dom -> debug_print (lazy (sprintf "CHOOSED ITEM: %s" (string_of_domain_item item))); let choices = @@ -955,9 +1112,11 @@ in refine_profiler.HExtlib.profile foo () | Some choices -> choices in match choices with [] -> - [], [diff, - Some (List.hd locs), - lazy ("No choices for " ^ string_of_domain_item item)] + [], [], + [aliases, diff, Some (List.hd locs), + lazy ("No choices for " ^ string_of_domain_item item), + true] +(* | [codomain_item] -> (* just one choice. We perform a one-step look-up and if the next set of choices is also a singleton we @@ -986,51 +1145,117 @@ in refine_profiler.HExtlib.profile foo () remaining_dom new_univ) | Uncertain (loc,msg),new_univ -> (match remaining_dom with - | [] -> [], [diff,loc,msg] + | [] -> [], [new_env,new_diff,loc,msg,true] | _ -> aux new_env new_diff lookup_in_todo_dom remaining_dom new_univ) - | Ko (loc,msg),_ -> [], [diff,loc,msg]) + | Ko (loc,msg),_ -> [], [new_env,new_diff,loc,msg,true]) +*) | _::_ -> + let mark_not_significant failures = + List.map + (fun (env, diff, loc, msg, _b) -> + env, diff, loc, msg, false) + failures in + let classify_errors ((ok_l,uncertain_l,error_l) as outcome) = + if ok_l <> [] || uncertain_l <> [] then + ok_l,uncertain_l,mark_not_significant error_l + else + outcome in 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 let new_diff = (item,codomain_item)::diff in - (match test_env new_env remaining_dom univ with + (match + test_env new_env (inner_dom@remaining_dom@rem_dom) univ + with | Ok (thing, metasenv),new_univ -> - (match remaining_dom with - | [] -> [new_env,new_diff,metasenv,thing,new_univ], [] - | _ -> aux new_env new_diff None remaining_dom new_univ - ) @@ - filter univ tl + let res = + (match inner_dom with + | [] -> + [new_env,new_diff,metasenv,thing,new_univ], [], [] + | _ -> + aux new_env new_diff None inner_dom + (remaining_dom@rem_dom) new_univ + ) + in + res @@ filter univ tl | Uncertain (loc,msg),new_univ -> - (match remaining_dom with - | [] -> [],[diff,loc,msg] - | _ -> aux new_env new_diff None remaining_dom new_univ - ) @@ - filter univ tl - | Ko (loc,msg),_ -> ([],[diff,loc,msg]) @@ filter univ tl) + let res = + (match inner_dom with + | [] -> [],[new_env,new_diff,loc,msg,new_univ],[] + | _ -> + aux new_env new_diff None inner_dom + (remaining_dom@rem_dom) new_univ + ) + in + res @@ filter univ tl + | Ko (loc,msg),_ -> + let res = [],[],[new_env,new_diff,loc,msg,true] in + res @@ filter univ tl) in - filter base_univ choices + let ok_l,uncertain_l,error_l = + classify_errors (filter base_univ choices) + in + let res_after_ok_l = + List.fold_right + (fun (env,diff,_,_,univ) res -> + aux env diff None remaining_dom rem_dom univ @@ res + ) ok_l ([],[],error_l) + in + List.fold_right + (fun (env,diff,_,_,univ) res -> + aux env diff None remaining_dom rem_dom univ @@ res + ) uncertain_l res_after_ok_l in + let aux' aliases diff lookup_in_todo_dom todo_dom base_univ = + match test_env aliases todo_dom base_univ with + | Ok _,_ + | Uncertain _,_ -> + aux aliases diff lookup_in_todo_dom todo_dom [] base_univ + | Ko (loc,msg),_ -> [],[],[aliases,diff,loc,msg,true] in let base_univ = initial_ugraph in try let res = - match aux aliases [] None todo_dom base_univ with - | [],errors -> raise (NoWellTypedInterpretation (0,errors)) - | [_,diff,metasenv,t,ugraph],_ -> + match aux' aliases [] None todo_dom base_univ with + | [],uncertain,errors -> + let errors = + List.map + (fun (env,diff,loc,msg,_) -> (env,diff,loc,msg,true) + ) uncertain @ errors + in + let errors = + List.map + (fun (env,diff,loc,msg,significant) -> + let env' = + filter_map_domain + (fun locs domain_item -> + try + let description = + fst (Environment.find domain_item env) + in + Some (locs,descr_of_domain_item domain_item,description) + with + Not_found -> None) + thing_dom + in + env',diff,loc,msg,significant + ) errors + in + 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 (fun (env, _, _, _, _) -> - List.map - (fun (locs,domain_item) -> + map_domain + (fun locs domain_item -> let description = fst (Environment.find domain_item env) in @@ -1059,7 +1284,8 @@ in refine_profiler.HExtlib.profile foo () in disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term - ~domain_of_thing:domain_of_term ~interpretate_thing:interpretate_term + ~domain_of_thing:domain_of_term + ~interpretate_thing:(interpretate_term (?create_dummy_ids:None)) ~refine_thing:refine_term (text,prefix_len,term) let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri @@ -1069,7 +1295,7 @@ 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:CicNotationPp.pp_obj ~domain_of_thing:domain_of_obj + ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) ~domain_of_thing:domain_of_obj ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj (text,prefix_len,obj) end