From ad586dd2ff1080ad6d71587a07772c2596b32a96 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 27 Nov 2008 12:26:03 +0000 Subject: [PATCH] disambiguate.ml splitted into disambiguate.ml and cicDisambiguate.ml --- .../cic_disambiguation/cicDisambiguate.ml | 701 ++++++++++++++++++ .../cic_disambiguation/cicDisambiguate.mli | 75 ++ 2 files changed, 776 insertions(+) create mode 100644 helm/software/components/cic_disambiguation/cicDisambiguate.ml create mode 100644 helm/software/components/cic_disambiguation/cicDisambiguate.mli diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.ml b/helm/software/components/cic_disambiguation/cicDisambiguate.ml new file mode 100644 index 000000000..a7e65bcfc --- /dev/null +++ b/helm/software/components/cic_disambiguation/cicDisambiguate.ml @@ -0,0 +1,701 @@ +(* +Copyright (C) 1999-2006, HELM Team. + +This file is part of HELM, an Hypertextual, Electronic +Library of Mathematics, developed at the Computer Science +Department, University of Bologna, Italy. + +HELM is free software; you can redistribute it and/or +modify it under the terms of the GNU General Public License +as published by the Free Software Foundation; either version 2 +of the License, or (at your option) any later version. + +HELM is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with this program; if not, write to the Free Software +Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA +02110-1301 USA. + +For details, see the HELM web site: http://helm.cs.unibo.it/ +*) + +open Printf +module Ast = CicNotationPt + +let debug = false +let debug_print s = if debug then prerr_endline (Lazy.force s) else () + +let refine_term metasenv subst 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 ~localization_tbl in + (Disambiguate.Ok (term', metasenv',[],ugraph1)) + with + exn -> + let rec process_exn loc = + function + HExtlib.Localized (loc,exn) -> process_exn loc exn + | CicRefine.Uncertain msg -> + debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ; + Disambiguate.Uncertain (lazy (loc,Lazy.force msg)) + | CicRefine.RefineFailure msg -> + debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" + (CicPp.ppterm term) (Lazy.force msg))); + Disambiguate.Ko (lazy (loc,Lazy.force msg)) + | exn -> raise exn + in + process_exn Stdpp.dummy_loc exn + +let refine_obj metasenv subst context uri obj ugraph ~localization_tbl = + assert (context = []); + assert (metasenv = []); + assert (subst = []); + debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj))) ; + try + let obj', metasenv,ugraph = + CicRefine.typecheck metasenv uri obj ~localization_tbl + in + (Disambiguate.Ok (obj', metasenv,[],ugraph)) + with + exn -> + let rec process_exn loc = + function + HExtlib.Localized (loc,exn) -> process_exn loc exn + | CicRefine.Uncertain msg -> + debug_print (lazy ("UNCERTAIN!!! [" ^ + (Lazy.force msg) ^ "] " ^ CicPp.ppobj obj)) ; + Disambiguate.Uncertain (lazy (loc,Lazy.force msg)) + | CicRefine.RefineFailure msg -> + debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" + (CicPp.ppobj obj) (Lazy.force msg))) ; + Disambiguate.Ko (lazy (loc,Lazy.force msg)) + | exn -> raise exn + in + process_exn Stdpp.dummy_loc exn +;; + +let interpretate_term ?(create_dummy_ids=false) ~context ~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 = function + | CicNotationPt.AttributedTerm (`Loc loc, 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 ~localize loc context) args in + Disambiguate.resolve env + (DisambiguateTypes.Symbol (symb, i)) ~args:cic_args () + | CicNotationPt.Appl terms -> + Cic.Appl (List.map (aux ~localize loc context) terms) + | CicNotationPt.Binder (binder_kind, (var, typ), body) -> + 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 ~localize loc (cic_name :: context) body in + (match binder_kind with + | `Lambda -> Cic.Lambda (cic_name, cic_type, cic_body) + | `Pi + | `Forall -> Cic.Prod (cic_name, cic_type, cic_body) + | `Exists -> + Disambiguate.resolve env (DisambiguateTypes.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 ~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 + do_branch' context args + in + 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 + Disambiguate.resolve env + (DisambiguateTypes.Id indty_ident) () + with + | Cic.MutInd (uri, tyno, _) -> (uri, tyno) + | Cic.Implicit _ -> + raise (Disambiguate.Try_again + (lazy "The type of the term to be matched + is still unknown")) + | _ -> + raise (DisambiguateTypes.Invalid_choice (lazy (loc,"The type of the term to be matched is not (co)inductive!")))) + | None -> + let rec fst_constructor = + function + (Ast.Pattern (head, _, _), _) :: _ -> head + | (Ast.Wildcard, _) :: tl -> fst_constructor tl + | [] -> raise (DisambiguateTypes.Invalid_choice (lazy (loc,"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 Disambiguate.resolve env + (DisambiguateTypes.Id (fst_constructor branches)) () with + | Cic.MutConstruct (indtype_uri, indtype_no, _, _) -> + (indtype_uri, indtype_no) + | Cic.Implicit _ -> + raise (Disambiguate.Try_again (lazy "The type of the term to be matched + is still unknown")) + | _ -> + raise (DisambiguateTypes.Invalid_choice (lazy (loc,"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 (DisambiguateTypes.Invalid_choice (lazy (loc, "Syntax error: the left hand side of a branch patterns must be \"_\""))) + ) branches + else + match fst(CicEnvironment.get_obj CicUniv.oblivion_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 (DisambiguateTypes.Invalid_choice + (lazy (loc, + ("Unrecognized constructors: " ^ + String.concat " " unrecognized)))) + else if useless > 0 then + raise (DisambiguateTypes.Invalid_choice + (lazy (loc, + ("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 + (DisambiguateTypes.Invalid_choice + (lazy (loc, ("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 + (DisambiguateTypes.Invalid_choice + (lazy (loc,"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)) + | CicNotationPt.Cast (t1, t2) -> + 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 ~localize loc context def in + let cic_name = CicNotationUtil.cic_name_of_name name in + let cic_typ = + match typ with + | 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_typ, cic_body) + | CicNotationPt.LetRec (kind, defs, body) -> + let context' = + List.fold_left + (fun acc (_, (name, _), _, _) -> + CicNotationUtil.cic_name_of_name name :: acc) + context defs + in + let cic_body = + let unlocalized_body = aux ~localize:false loc context' body in + match unlocalized_body with + 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 [] [] (List.length defs) 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)) -> + (* since we avoid the letin, the context has no + * recfuns in it *) + let l' = List.map (aux ~localize loc context) l in + `AvoidLetIn (n,l') + | _ -> assert false + else + `AvoidLetIn (n,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 (params, (name, typ), body, decr_idx) -> + let add_binders kind t = + List.fold_right + (fun var t -> CicNotationPt.Binder (kind, var, t)) params t + in + let cic_body = + aux ~localize loc context' (add_binders `Lambda body) in + let cic_type = + aux_option ~localize loc context (Some `Type) + (HExtlib.map_option (add_binders `Pi) typ) in + let name = + match CicNotationUtil.cic_name_of_name name with + | Cic.Anonymous -> + CicNotationPt.fail loc + "Recursive functions cannot be anonymous" + | Cic.Name name -> name + in + (name, decr_idx, cic_type, cic_body)) + defs + in + let fix_or_cofix n = + match kind with + `Inductive -> Cic.Fix (n,inductiveFuns) + | `CoInductive -> + let coinductiveFuns = + List.map + (fun (name, _, typ, body) -> name, typ, body) + inductiveFuns + in + Cic.CoFix (n,coinductiveFuns) + in + 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 Disambiguate.PathNotWellFormed + | CicNotationPt.Ident (name, subst) + | CicNotationPt.Uri (name, subst) as ast -> + let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in + (try + if is_uri ast then raise Not_found;(* don't search the env for URIs *) + let index = Disambiguate.find_in_context name context in + if subst <> None then + CicNotationPt.fail loc "Explicit substitutions not allowed here"; + Cic.Rel index + with Not_found -> + let cic = + if is_uri ast then (* we have the URI, build the term out of it *) + try + CicUtil.term_of_uri (UriManager.uri_of_string name) + with UriManager.IllFormedUri _ -> + CicNotationPt.fail loc "Ill formed URI" + else + Disambiguate.resolve env (DisambiguateTypes.Id name) () + in + let mk_subst uris = + let ids_to_uris = + List.map (fun uri -> UriManager.name_of_uri uri, uri) uris + in + (match subst with + | Some subst -> + List.map + (fun (s, term) -> + (try + List.assoc s ids_to_uris, aux ~localize loc context term + with Not_found -> + raise (DisambiguateTypes.Invalid_choice (lazy (loc, "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 + (try + match cic with + | Cic.Const (uri, []) -> + let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in + let uris = CicUtil.params_of_obj o in + Cic.Const (uri, mk_subst uris) + | Cic.Var (uri, []) -> + let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in + let uris = CicUtil.params_of_obj o in + Cic.Var (uri, mk_subst uris) + | Cic.MutInd (uri, i, []) -> + (try + let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in + let uris = CicUtil.params_of_obj o in + Cic.MutInd (uri, i, mk_subst uris) + with + CicEnvironment.Object_not_found _ -> + (* if we are here it is probably the case that during the + definition of a mutual inductive type we have met an + occurrence of the type in one of its constructors. + However, the inductive type is not yet in the environment + *) + (*here the explicit_named_substituion is assumed to be of length 0 *) + Cic.MutInd (uri,i,[])) + | Cic.MutConstruct (uri, i, j, []) -> + let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in + let uris = CicUtil.params_of_obj o in + Cic.MutConstruct (uri, i, j, mk_subst uris) + | Cic.Meta _ | Cic.Implicit _ as t -> +(* + debug_print (lazy (sprintf + "Warning: %s must be instantiated with _[%s] but we do not enforce it" + (CicPp.ppterm t) + (String.concat "; " + (List.map + (fun (s, term) -> s ^ " := " ^ CicNotationPtPp.pp_term term) + subst)))); +*) + t + | _ -> + raise (DisambiguateTypes.Invalid_choice (lazy (loc, "??? Can this happen?"))) + with + CicEnvironment.CircularDependency _ -> + raise (DisambiguateTypes.Invalid_choice (lazy (loc,"Circular dependency in the environment"))))) + | CicNotationPt.Implicit -> Cic.Implicit None + | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole) + | CicNotationPt.Num (num, i) -> Disambiguate.resolve env (DisambiguateTypes.Num i) ~num () + | CicNotationPt.Meta (index, subst) -> + let cic_subst = + List.map + (function + None -> None + | Some term -> Some (aux ~localize loc context term)) + subst + in + Cic.Meta (index, cic_subst) + | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop + | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set + | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u) + | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u) + | CicNotationPt.Symbol (symbol, instance) -> + Disambiguate.resolve env (DisambiguateTypes.Symbol (symbol, instance)) () + | _ -> assert false (* god bless Bologna *) + and aux_option ~localize loc context annotation = function + | None -> Cic.Implicit annotation + | Some term -> aux ~localize loc context term + in + aux ~localize:true HExtlib.dummy_floc context ast + +let interpretate_path ~context path = + let localization_tbl = Cic.CicHash.create 23 in + (* here we are throwing away useful localization informations!!! *) + fst ( + interpretate_term ~create_dummy_ids:true + ~context ~env:DisambiguateTypes.Environment.empty ~uri:None ~is_path:true + path ~localization_tbl, localization_tbl) + +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 + | CicNotationPt.Inductive (params,tyl) -> + let uri = match uri with Some uri -> uri | None -> assert false in + let context,params = + let context,res = + List.fold_left + (fun (context,res) (name,t) -> + let t = + match t with + None -> CicNotationPt.Implicit + | Some t -> t in + let name = CicNotationUtil.cic_name_of_name name in + name::context,(name, interpretate_term context env None false t)::res + ) ([],[]) params + in + context,List.rev res in + let add_params = + List.fold_right (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in + let name_to_uris = + snd ( + List.fold_left + (*here the explicit_named_substituion is assumed to be of length 0 *) + (fun (i,res) (name,_,_,_) -> + 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 tyl = + List.map + (fun (name,b,ty,cl) -> + let ty' = add_params (interpretate_term context env None false ty) in + let cl' = + List.map + (fun (name,ty) -> + let ty' = + add_params (interpretate_term context con_env None false ty) + in + name,ty' + ) cl + in + name,b,ty',cl' + ) tyl + in + Cic.InductiveDefinition (tyl,[],List.length params,[]) + | CicNotationPt.Record (params,name,ty,fields) -> + let uri = match uri with Some uri -> uri | None -> assert false in + let context,params = + let context,res = + List.fold_left + (fun (context,res) (name,t) -> + let t = + match t with + None -> CicNotationPt.Implicit + | Some t -> t in + let name = CicNotationUtil.cic_name_of_name name in + name::context,(name, interpretate_term context env None false t)::res + ) ([],[]) params + in + context,List.rev res in + let add_params = + List.fold_right + (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in + let ty' = add_params (interpretate_term context env None false ty) in + let fields' = + snd ( + List.fold_left + (fun (context,res) (name,ty,_coercion,arity) -> + let context' = Cic.Name name :: context in + context',(name,interpretate_term context env None false ty)::res + ) (context,[]) fields) in + let concl = + (*here the explicit_named_substituion is assumed to be of length 0 *) + let mutind = Cic.MutInd (uri,0,[]) in + if params = [] then mutind + else + Cic.Appl + (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in + let con = + List.fold_left + (fun t (name,ty) -> Cic.Prod (Cic.Name name,ty,t)) + concl fields' in + let con' = add_params con in + let tyl = [name,true,ty',["mk_" ^ name,con']] in + let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in + Cic.InductiveDefinition + (tyl,[],List.length params,[`Class (`Record field_names)]) + | CicNotationPt.Theorem (flavour, name, ty, bo) -> + let attrs = [`Flavour flavour] in + let ty' = interpretate_term [] env None false ty in + (match bo,flavour with + None,`Axiom -> + Cic.Constant (name,None,ty',[],attrs) + | Some bo,`Axiom -> assert false + | None,_ -> + Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],attrs) + | Some bo,_ -> + let bo' = Some (interpretate_term [] env None false bo) in + Cic.Constant (name,bo',ty',[],attrs)) +;; + +let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast + ~localization_tbl += + let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in +interpretate_term ~create_dummy_ids ~context ~env ~uri ~is_path ast +~localization_tbl +;; + + + + +module type CicDisambiguator = +sig + val disambiguate_term : + ?fresh_instances:bool -> + context:Cic.context -> + metasenv:Cic.metasenv -> + subst:Cic.substitution -> + ?goal:int -> + ?initial_ugraph:CicUniv.universe_graph -> + aliases:Cic.term DisambiguateTypes.environment -> + universe:Cic.term DisambiguateTypes.multiple_environment option -> + lookup_in_library:( + DisambiguateTypes.interactive_user_uri_choice_type -> + DisambiguateTypes.input_or_locate_uri_type -> + DisambiguateTypes.Environment.key -> + Cic.term DisambiguateTypes.codomain_item list) -> + CicNotationPt.term Disambiguate.disambiguator_input -> + ((DisambiguateTypes.domain_item * + Cic.term DisambiguateTypes.codomain_item) list * + Cic.metasenv * + Cic.substitution * + Cic.term* + CicUniv.universe_graph) list * + bool + + val disambiguate_obj : + ?fresh_instances:bool -> + aliases:Cic.term DisambiguateTypes.environment -> + universe:Cic.term DisambiguateTypes.multiple_environment option -> + uri:UriManager.uri option -> (* required only for inductive types *) + lookup_in_library:( + DisambiguateTypes.interactive_user_uri_choice_type -> + DisambiguateTypes.input_or_locate_uri_type -> + DisambiguateTypes.Environment.key -> + Cic.term DisambiguateTypes.codomain_item list) -> + CicNotationPt.term CicNotationPt.obj Disambiguate.disambiguator_input -> + ((DisambiguateTypes.domain_item * + Cic.term DisambiguateTypes.codomain_item) list * + Cic.metasenv * + Cic.substitution * + Cic.obj * + CicUniv.universe_graph) list * + bool +end + +module Make (C: DisambiguateTypes.Callbacks) = + struct + module Disambiguator = Disambiguate.Make(C) + + let mk_implicit = + function true -> Cic.Implicit (Some `Closed) + | _ -> Cic.Implicit None + ;; + + let disambiguate_term ?(fresh_instances=false) ~context ~metasenv + ~subst ?goal + ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe + ~lookup_in_library + (text,prefix_len,term) + = + let term = + if fresh_instances then CicNotationUtil.freshen_term term else term + in + let hint = match goal with + | None -> (fun _ x -> x), fun k -> k + | Some i -> + (fun metasenv t -> + let _,c,ty = CicUtil.lookup_meta i metasenv in + assert(c=context); + Cic.Cast(t,ty)), + function + | Disambiguate.Ok (t,m,s,ug) -> + (match t with + | Cic.Cast(t,_) -> Disambiguate.Ok (t,m,s,ug) + | _ -> assert false) + | k -> k + in + let localization_tbl = Cic.CicHash.create 503 in + Disambiguator.disambiguate_thing ~context ~metasenv ~subst + ~initial_ugraph ~aliases ~mk_implicit + ~universe ~lookup_in_library + ~uri:None ~pp_thing:CicNotationPp.pp_term + ~domain_of_thing:Disambiguate.domain_of_term + ~interpretate_thing:(interpretate_term (?create_dummy_ids:None)) + ~refine_thing:refine_term (text,prefix_len,term) + ~localization_tbl + ~hint + + let disambiguate_obj + ?(fresh_instances=false) ~aliases ~universe ~uri ~lookup_in_library + (text,prefix_len,obj) + = + let obj = + if fresh_instances then CicNotationUtil.freshen_obj obj else obj + in + let hint = + (fun _ x -> x), + fun k -> k + in + let localization_tbl = Cic.CicHash.create 503 in + Disambiguator.disambiguate_thing ~context:[] ~metasenv:[] ~subst:[] + ~aliases ~universe ~uri ~mk_implicit + ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) + ~domain_of_thing:Disambiguate.domain_of_obj + ~lookup_in_library + ~initial_ugraph:CicUniv.empty_ugraph + ~interpretate_thing:interpretate_obj + ~refine_thing:refine_obj + ~localization_tbl + ~hint + (text,prefix_len,obj) +end diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.mli b/helm/software/components/cic_disambiguation/cicDisambiguate.mli new file mode 100644 index 000000000..375723a76 --- /dev/null +++ b/helm/software/components/cic_disambiguation/cicDisambiguate.mli @@ -0,0 +1,75 @@ +(* + * +Copyright (C) 1999-2006, HELM Team. + +This file is part of HELM, an Hypertextual, Electronic +Library of Mathematics, developed at the Computer Science +Department, University of Bologna, Italy. + +HELM is free software; you can redistribute it and/or +modify it under the terms of the GNU General Public License +as published by the Free Software Foundation; either version 2 +of the License, or (at your option) any later version. + +HELM is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with this program; if not, write to the Free Software +Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA +02110-1301 USA. + +For details, see the HELM web site: http://helm.cs.unibo.it/ +*) + +val interpretate_path : + context:Cic.name list -> CicNotationPt.term -> Cic.term + +module type CicDisambiguator = +sig + val disambiguate_term : + ?fresh_instances:bool -> + context:Cic.context -> + metasenv:Cic.metasenv -> + subst:Cic.substitution -> + ?goal:int -> + ?initial_ugraph:CicUniv.universe_graph -> + aliases:Cic.term DisambiguateTypes.environment -> + universe:Cic.term DisambiguateTypes.multiple_environment option -> + lookup_in_library:( + DisambiguateTypes.interactive_user_uri_choice_type -> + DisambiguateTypes.input_or_locate_uri_type -> + DisambiguateTypes.Environment.key -> + Cic.term DisambiguateTypes.codomain_item list) -> + CicNotationPt.term Disambiguate.disambiguator_input -> + ((DisambiguateTypes.domain_item * + Cic.term DisambiguateTypes.codomain_item) list * + Cic.metasenv * + Cic.substitution * + Cic.term* + CicUniv.universe_graph) list * + bool + + val disambiguate_obj : + ?fresh_instances:bool -> + aliases:Cic.term DisambiguateTypes.environment -> + universe:Cic.term DisambiguateTypes.multiple_environment option -> + uri:UriManager.uri option -> (* required only for inductive types *) + lookup_in_library:( + DisambiguateTypes.interactive_user_uri_choice_type -> + DisambiguateTypes.input_or_locate_uri_type -> + DisambiguateTypes.Environment.key -> + Cic.term DisambiguateTypes.codomain_item list) -> + CicNotationPt.term CicNotationPt.obj Disambiguate.disambiguator_input -> + ((DisambiguateTypes.domain_item * + Cic.term DisambiguateTypes.codomain_item) list * + Cic.metasenv * + Cic.substitution * + Cic.obj * + CicUniv.universe_graph) list * + bool +end + +module Make (C : DisambiguateTypes.Callbacks) : CicDisambiguator -- 2.39.2