2.
disambiguateChoices.cmi: disambiguateTypes.cmi
disambiguate.cmi: disambiguateTypes.cmi
+cicDisambiguate.cmi: disambiguateTypes.cmi disambiguate.cmi
disambiguateTypes.cmo: disambiguateTypes.cmi
disambiguateTypes.cmx: disambiguateTypes.cmi
disambiguateChoices.cmo: disambiguateTypes.cmi disambiguateChoices.cmi
disambiguateChoices.cmx: disambiguateTypes.cmx disambiguateChoices.cmi
-disambiguate.cmo: disambiguateTypes.cmi disambiguateChoices.cmi \
- disambiguate.cmi
-disambiguate.cmx: disambiguateTypes.cmx disambiguateChoices.cmx \
- disambiguate.cmi
+disambiguate.cmo: disambiguateTypes.cmi disambiguate.cmi
+disambiguate.cmx: disambiguateTypes.cmx disambiguate.cmi
+cicDisambiguate.cmo: disambiguateTypes.cmi disambiguate.cmi \
+ cicDisambiguate.cmi
+cicDisambiguate.cmx: disambiguateTypes.cmx disambiguate.cmx \
+ cicDisambiguate.cmi
number_notation.cmo: disambiguateTypes.cmi disambiguateChoices.cmi
number_notation.cmx: disambiguateTypes.cmx disambiguateChoices.cmx
disambiguateChoices.cmi: disambiguateTypes.cmi
disambiguate.cmi: disambiguateTypes.cmi
+cicDisambiguate.cmi: disambiguateTypes.cmi disambiguate.cmi
disambiguateTypes.cmo: disambiguateTypes.cmi
disambiguateTypes.cmx: disambiguateTypes.cmi
disambiguateChoices.cmo: disambiguateTypes.cmi disambiguateChoices.cmi
disambiguateChoices.cmx: disambiguateTypes.cmx disambiguateChoices.cmi
-disambiguate.cmo: disambiguateTypes.cmi disambiguateChoices.cmi \
- disambiguate.cmi
-disambiguate.cmx: disambiguateTypes.cmx disambiguateChoices.cmx \
- disambiguate.cmi
+disambiguate.cmo: disambiguateTypes.cmi disambiguate.cmi
+disambiguate.cmx: disambiguateTypes.cmx disambiguate.cmi
+cicDisambiguate.cmo: disambiguateTypes.cmi disambiguate.cmi \
+ cicDisambiguate.cmi
+cicDisambiguate.cmx: disambiguateTypes.cmx disambiguate.cmx \
+ cicDisambiguate.cmi
number_notation.cmo: disambiguateTypes.cmi disambiguateChoices.cmi
number_notation.cmx: disambiguateTypes.cmx disambiguateChoices.cmx
INTERFACE_FILES = \
disambiguateTypes.mli \
disambiguateChoices.mli \
- disambiguate.mli
+ disambiguate.mli \
+ cicDisambiguate.mli
IMPLEMENTATION_FILES = \
$(patsubst %.mli, %.ml, $(INTERFACE_FILES)) \
$(patsubst %,%_notation.ml,$(NOTATIONS))
| Ko of (Stdpp.location * string) Lazy.t
| Uncertain of (Stdpp.location * string) Lazy.t
-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
- (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)) ;
- Uncertain (lazy (loc,Lazy.force msg))
- | CicRefine.RefineFailure msg ->
- debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
- (CicPp.ppterm term) (Lazy.force msg)));
- 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
- (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)) ;
- Uncertain (lazy (loc,Lazy.force msg))
- | CicRefine.RefineFailure msg ->
- debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
- (CicPp.ppobj obj) (Lazy.force msg))) ;
- Ko (lazy (loc,Lazy.force msg))
- | exn -> raise exn
- in
- process_exn Stdpp.dummy_loc exn
-
let resolve (env: 'term codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () =
try
snd (Environment.find item env) env num args
in
aux 1 context
-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
- resolve env (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 ->
- 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 ~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 resolve env (Id indty_ident) () with
- | Cic.MutInd (uri, tyno, _) -> (uri, tyno)
- | Cic.Implicit _ ->
- raise (Try_again (lazy "The type of the term to be matched
- is still unknown"))
- | _ ->
- raise (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 (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 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 (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 (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 (Invalid_choice
- (lazy (loc,
- ("Unrecognized constructors: " ^
- String.concat " " unrecognized))))
- else if useless > 0 then
- raise (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
- (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
- (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 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 = 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
- resolve env (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 (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 (Invalid_choice (lazy (loc, "??? Can this happen?")))
- with
- CicEnvironment.CircularDependency _ ->
- raise (Invalid_choice (lazy (loc,"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 ~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) ->
- resolve env (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: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
-;;
-
-
let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
| Ast.AttributedTerm (`Loc loc, term) ->
domain_of_term ~loc ~context term
List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context
in
domain_of_term ~context term
-
(* dom1 \ dom2 *)
let domain_diff dom1 dom2 =
(* let domain_diff = Domain.diff *)
context:'context ->
metasenv:'metasenv ->
subst:'subst ->
- mk_implicit:([ `Closed ] option -> 'refined_thing) ->
+ mk_implicit:(bool -> 'refined_term) ->
initial_ugraph:'ugraph ->
- hint: ('metasenv -> 'raw_thing -> 'raw_thing) *
- (('refined_thing,'metasenv,'subst,'ugraph) test_result ->
- ('refined_thing,'metasenv,'subst,'ugraph) test_result) ->
- aliases:'refined_thing DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t ->
- universe:'refined_thing DisambiguateTypes.codomain_item list
- DisambiguateTypes.Environment.t option ->
- lookup_in_library:((selection_mode:[ `MULTIPLE | `SINGLE ] ->
- ?ok:string ->
- ?enable_button_for_non_vars:bool ->
- title:string ->
- msg:string ->
- id:string ->
- UriManager.uri list -> UriManager.uri list) ->
- (title:string -> ?id:string -> unit -> UriManager.uri option) ->
- DisambiguateTypes.Environment.key ->
- 'refined_thing DisambiguateTypes.codomain_item list) ->
+ hint:
+ ('metasenv -> 'raw_thing -> 'raw_thing) *
+ (('refined_thing,'metasenv,'subst,'ugraph) test_result ->
+ ('refined_thing,'metasenv,'subst,'ugraph) test_result) ->
+ aliases:'refined_term DisambiguateTypes.codomain_item
+ DisambiguateTypes.Environment.t ->
+ universe:'refined_term DisambiguateTypes.codomain_item list
+ DisambiguateTypes.Environment.t option ->
+ lookup_in_library:(
+ DisambiguateTypes.interactive_user_uri_choice_type ->
+ DisambiguateTypes.input_or_locate_uri_type ->
+ DisambiguateTypes.Environment.key ->
+ 'refined_term DisambiguateTypes.codomain_item list) ->
uri:'uri ->
pp_thing:('ast_thing -> string) ->
domain_of_thing:(context:'context -> 'ast_thing -> domain) ->
- interpretate_thing:(context:'context ->
- env:'refined_thing DisambiguateTypes.codomain_item
- DisambiguateTypes.Environment.t ->
- uri:'uri ->
- is_path:bool -> 'ast_thing -> localization_tbl:'cichash -> 'raw_thing) ->
- refine_thing:('metasenv ->
- 'subst ->
- 'context ->
- 'uri ->
- 'raw_thing ->
- 'ugraph -> localization_tbl:'cichash ->
- ('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
+ interpretate_thing:(
+ context:'context ->
+ env:'refined_term DisambiguateTypes.codomain_item
+ DisambiguateTypes.Environment.t ->
+ uri:'uri ->
+ is_path:bool ->
+ 'ast_thing ->
+ localization_tbl:'cichash ->
+ 'raw_thing) ->
+ refine_thing:(
+ 'metasenv -> 'subst -> 'context -> 'uri ->
+ 'raw_thing -> 'ugraph -> localization_tbl:'cichash ->
+ ('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
localization_tbl:'cichash ->
string * int * 'ast_thing ->
((DisambiguateTypes.Environment.key *
- 'refined_thing DisambiguateTypes.codomain_item) list *
+ 'refined_term DisambiguateTypes.codomain_item) list *
'metasenv * 'subst * 'refined_thing * 'ugraph)
- list * bool
-
- 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 ->(* previous interpretation status *)
- universe:Cic.term DisambiguateTypes.multiple_environment option ->
- lookup_in_library:((selection_mode:[ `MULTIPLE | `SINGLE ] ->
- ?ok:string ->
- ?enable_button_for_non_vars:bool ->
- title:string ->
- msg:string ->
- id:string ->
- UriManager.uri list -> UriManager.uri list) ->
- (title:string -> ?id:string -> unit -> UriManager.uri option) ->
- DisambiguateTypes.Environment.key ->
- Cic.term DisambiguateTypes.codomain_item list) ->
- CicNotationPt.term disambiguator_input ->
- ((DisambiguateTypes.domain_item * Cic.term DisambiguateTypes.codomain_item) list *
- Cic.metasenv * (* new metasenv *)
- Cic.substitution *
- Cic.term*
- CicUniv.universe_graph) list * (* disambiguated term *)
- bool
-
- val disambiguate_obj :
- ?fresh_instances:bool ->
- aliases:Cic.term DisambiguateTypes.environment ->(* previous interpretation status *)
- universe:Cic.term DisambiguateTypes.multiple_environment option ->
- uri:UriManager.uri option -> (* required only for inductive types *)
- lookup_in_library:((selection_mode:[ `MULTIPLE | `SINGLE ] ->
- ?ok:string ->
- ?enable_button_for_non_vars:bool ->
- title:string ->
- msg:string ->
- id:string ->
- UriManager.uri list -> UriManager.uri list) ->
- (title:string -> ?id:string -> unit -> UriManager.uri option) ->
- DisambiguateTypes.Environment.key ->
- Cic.term DisambiguateTypes.codomain_item list) ->
- CicNotationPt.term CicNotationPt.obj disambiguator_input ->
- ((DisambiguateTypes.domain_item * Cic.term DisambiguateTypes.codomain_item) list *
- Cic.metasenv * (* new metasenv *)
- Cic.substitution *
- Cic.obj *
- CicUniv.universe_graph) list * (* disambiguated obj *)
- bool
+ list * bool
end
module Make (C: Callbacks) =
("Implicit",
(match item with
| Id _ | Num _ ->
- (fun _ _ _ -> mk_implicit (Some `Closed))
- | Symbol _ -> (fun _ _ _ -> mk_implicit None)))
+ (fun _ _ _ -> mk_implicit true)
+ | Symbol _ -> (fun _ _ _ -> mk_implicit false)))
env in
aux (aux env l) tl in
let filled_env = aux aliases todo_dom in
CicEnvironment.CircularDependency s ->
failwith "Disambiguate: circular dependency"
- 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 mk_implicit x = Cic.Implicit x 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
- | Ok (t,m,s,ug) ->
- (match t with
- | Cic.Cast(t,_) -> Ok (t,m,s,ug)
- | _ -> assert false)
- | k -> k
- in
- let localization_tbl = Cic.CicHash.create 503 in
- disambiguate_thing ~context ~metasenv ~subst
- ~initial_ugraph ~aliases ~mk_implicit
- ~universe ~lookup_in_library
- ~uri:None ~pp_thing:CicNotationPp.pp_term
- ~domain_of_thing: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 mk_implicit x = Cic.Implicit x in
- 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
- disambiguate_thing ~context:[] ~metasenv:[] ~subst:[]
- ~aliases ~universe ~uri ~mk_implicit
- ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term)
- ~domain_of_thing: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
bool) list
exception PathNotWellFormed
-val interpretate_path :
- context:Cic.name list -> CicNotationPt.term -> Cic.term
-
type 'a disambiguator_input = string * int * 'a
type domain = domain_tree list
exception Try_again of string Lazy.t
+val resolve :
+ 'term DisambiguateTypes.environment ->
+ DisambiguateTypes.Environment.key ->
+ ?num:string -> ?args:'term list -> unit -> 'term
+
+val find_in_context: string -> Cic.name list -> int
+
val domain_of_ast_term: context:Cic.name list -> CicNotationPt.term -> domain
+val domain_of_term: context:
+ (Cic.name * 'a) option list -> CicNotationPt.term -> domain
+val domain_of_obj:
+ context:(Cic.name * 'a) option list ->
+ CicNotationPt.term CicNotationPt.obj -> domain
module type Disambiguator =
sig
context:'context ->
metasenv:'metasenv ->
subst:'subst ->
- mk_implicit:([ `Closed ] option -> 'refined_thing) ->
+ mk_implicit:(bool -> 'refined_term) ->
initial_ugraph:'ugraph ->
- hint: ('metasenv -> 'raw_thing -> 'raw_thing) *
- (('refined_thing,'metasenv,'subst,'ugraph) test_result ->
- ('refined_thing,'metasenv,'subst,'ugraph) test_result) ->
- aliases:'refined_thing DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t ->
- universe:'refined_thing DisambiguateTypes.codomain_item list
- DisambiguateTypes.Environment.t option ->
- lookup_in_library:((selection_mode:[ `MULTIPLE | `SINGLE ] ->
- ?ok:string ->
- ?enable_button_for_non_vars:bool ->
- title:string ->
- msg:string ->
- id:string ->
- UriManager.uri list -> UriManager.uri list) ->
- (title:string -> ?id:string -> unit -> UriManager.uri option) ->
- DisambiguateTypes.Environment.key ->
- 'refined_thing DisambiguateTypes.codomain_item list) ->
+ hint:
+ ('metasenv -> 'raw_thing -> 'raw_thing) *
+ (('refined_thing,'metasenv,'subst,'ugraph) test_result ->
+ ('refined_thing,'metasenv,'subst,'ugraph) test_result) ->
+ aliases:'refined_term DisambiguateTypes.codomain_item
+ DisambiguateTypes.Environment.t ->
+ universe:'refined_term DisambiguateTypes.codomain_item list
+ DisambiguateTypes.Environment.t option ->
+ lookup_in_library:(
+ DisambiguateTypes.interactive_user_uri_choice_type ->
+ DisambiguateTypes.input_or_locate_uri_type ->
+ DisambiguateTypes.Environment.key ->
+ 'refined_term DisambiguateTypes.codomain_item list) ->
uri:'uri ->
pp_thing:('ast_thing -> string) ->
domain_of_thing:(context:'context -> 'ast_thing -> domain) ->
- interpretate_thing:(context:'context ->
- env:'refined_thing DisambiguateTypes.codomain_item
- DisambiguateTypes.Environment.t ->
- uri:'uri ->
- is_path:bool -> 'ast_thing -> localization_tbl:'cichash -> 'raw_thing) ->
- refine_thing:('metasenv ->
- 'subst ->
- 'context ->
- 'uri ->
- 'raw_thing ->
- 'ugraph -> localization_tbl:'cichash ->
- ('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
+ interpretate_thing:(
+ context:'context ->
+ env:'refined_term DisambiguateTypes.codomain_item
+ DisambiguateTypes.Environment.t ->
+ uri:'uri ->
+ is_path:bool ->
+ 'ast_thing ->
+ localization_tbl:'cichash ->
+ 'raw_thing) ->
+ refine_thing:(
+ 'metasenv -> 'subst -> 'context -> 'uri ->
+ 'raw_thing -> 'ugraph -> localization_tbl:'cichash ->
+ ('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
localization_tbl:'cichash ->
string * int * 'ast_thing ->
((DisambiguateTypes.Environment.key *
- 'refined_thing DisambiguateTypes.codomain_item) list *
+ 'refined_term DisambiguateTypes.codomain_item) list *
'metasenv * 'subst * 'refined_thing * 'ugraph)
- list * bool
-
- 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 ->(* previous interpretation status *)
- universe:Cic.term DisambiguateTypes.multiple_environment option ->
- lookup_in_library:((selection_mode:[ `MULTIPLE | `SINGLE ] ->
- ?ok:string ->
- ?enable_button_for_non_vars:bool ->
- title:string ->
- msg:string ->
- id:string ->
- UriManager.uri list -> UriManager.uri list) ->
- (title:string -> ?id:string -> unit -> UriManager.uri option) ->
- DisambiguateTypes.Environment.key ->
- Cic.term DisambiguateTypes.codomain_item list) ->
- CicNotationPt.term disambiguator_input ->
- ((DisambiguateTypes.domain_item * Cic.term DisambiguateTypes.codomain_item) list *
- Cic.metasenv * (* new metasenv *)
- Cic.substitution *
- Cic.term*
- CicUniv.universe_graph) list * (* disambiguated term *)
- bool
-
- val disambiguate_obj :
- ?fresh_instances:bool ->
- aliases:Cic.term DisambiguateTypes.environment ->(* previous interpretation status *)
- universe:Cic.term DisambiguateTypes.multiple_environment option ->
- uri:UriManager.uri option -> (* required only for inductive types *)
- lookup_in_library:((selection_mode:[ `MULTIPLE | `SINGLE ] ->
- ?ok:string ->
- ?enable_button_for_non_vars:bool ->
- title:string ->
- msg:string ->
- id:string ->
- UriManager.uri list -> UriManager.uri list) ->
- (title:string -> ?id:string -> unit -> UriManager.uri option) ->
- DisambiguateTypes.Environment.key ->
- Cic.term DisambiguateTypes.codomain_item list) ->
- CicNotationPt.term CicNotationPt.obj disambiguator_input ->
- ((DisambiguateTypes.domain_item * Cic.term DisambiguateTypes.codomain_item) list *
- Cic.metasenv * (* new metasenv *)
- Cic.substitution *
- Cic.obj *
- CicUniv.universe_graph) list * (* disambiguated obj *)
- bool
+ list * bool
end
module Make (C : DisambiguateTypes.Callbacks) : Disambiguator
(fun e (name,descr,t) -> Environment.add (Id name) (descr,fun _ _ _ -> t) e)
e l
+type interactive_user_uri_choice_type =
+ selection_mode:[`SINGLE | `MULTIPLE] ->
+ ?ok:string ->
+ ?enable_button_for_non_vars:bool ->
+ title:string -> msg:string -> id:string -> UriManager.uri list ->
+ UriManager.uri list
+
+type interactive_interpretation_choice_type = string -> int ->
+ (Stdpp.location list * string * string) list list -> int list
+
+type input_or_locate_uri_type =
+ title:string -> ?id:string -> unit -> UriManager.uri option
+
module type Callbacks =
sig
- val interactive_user_uri_choice:
- selection_mode:[`SINGLE | `MULTIPLE] ->
- ?ok:string ->
- ?enable_button_for_non_vars:bool ->
- title:string -> msg:string -> id:string -> UriManager.uri list ->
- UriManager.uri list
- val interactive_interpretation_choice:
- string -> int ->
- (Stdpp.location list * string * string) list list -> int list
- val input_or_locate_uri:
- title:string -> ?id:string -> unit -> UriManager.uri option
+ val interactive_user_uri_choice : interactive_user_uri_choice_type
+
+ val interactive_interpretation_choice :
+ interactive_interpretation_choice_type
+
+ val input_or_locate_uri: input_or_locate_uri_type
end
let string_of_domain_item = function
(string * string * 'term) list -> 'term multiple_environment ->
'term multiple_environment
+type interactive_user_uri_choice_type =
+ selection_mode:[`SINGLE | `MULTIPLE] ->
+ ?ok:string ->
+ ?enable_button_for_non_vars:bool ->
+ title:string -> msg:string -> id:string -> UriManager.uri list ->
+ UriManager.uri list
+
+type interactive_interpretation_choice_type = string -> int ->
+ (Stdpp.location list * string * string) list list -> int list
+
+type input_or_locate_uri_type =
+ title:string -> ?id:string -> unit -> UriManager.uri option
+
module type Callbacks =
sig
- val interactive_user_uri_choice :
- selection_mode:[`SINGLE | `MULTIPLE] ->
- ?ok:string ->
- ?enable_button_for_non_vars:bool ->
- title:string -> msg:string -> id:string -> UriManager.uri list ->
- UriManager.uri list
-
- val interactive_interpretation_choice :
- string -> int ->
- (Stdpp.location list * string * string) list list -> int list
-
- (** @param title gtk window title for user prompting
- * @param id unbound identifier which originated this callback invocation *)
- val input_or_locate_uri:
- title:string -> ?id:string -> unit -> UriManager.uri option
+ val interactive_user_uri_choice : interactive_user_uri_choice_type
+
+ val interactive_interpretation_choice :
+ interactive_interpretation_choice_type
+
+ val input_or_locate_uri: input_or_locate_uri_type
end
val string_of_domain_item: domain_item -> string
freshNamesGenerator.cmi
freshNamesGenerator.cmx: cicTypeChecker.cmx cicSubstitution.cmx \
freshNamesGenerator.cmi
-cicDischarge.cmo: cicEnvironment.cmi cicDischarge.cmi
-cicDischarge.cmx: cicEnvironment.cmx cicDischarge.cmi
+cicDischarge.cmo: cicTypeChecker.cmi cicEnvironment.cmi cicDischarge.cmi
+cicDischarge.cmx: cicTypeChecker.cmx cicEnvironment.cmx cicDischarge.cmi
freshNamesGenerator.cmi
freshNamesGenerator.cmx: cicTypeChecker.cmx cicSubstitution.cmx \
freshNamesGenerator.cmi
-cicDischarge.cmo: cicEnvironment.cmi cicDischarge.cmi
-cicDischarge.cmx: cicEnvironment.cmx cicDischarge.cmi
+cicDischarge.cmo: cicTypeChecker.cmi cicEnvironment.cmi cicDischarge.cmi
+cicDischarge.cmx: cicTypeChecker.cmx cicEnvironment.cmx cicDischarge.cmi
grafiteParser.cmx: grafiteParser.cmi
cicNotation2.cmo: grafiteParser.cmi cicNotation2.cmi
cicNotation2.cmx: grafiteParser.cmx cicNotation2.cmi
-grafiteDisambiguator.cmo: grafiteDisambiguator.cmi
-grafiteDisambiguator.cmx: grafiteDisambiguator.cmi
-grafiteDisambiguate.cmo: grafiteDisambiguator.cmi grafiteDisambiguate.cmi
-grafiteDisambiguate.cmx: grafiteDisambiguator.cmx grafiteDisambiguate.cmi
+multiPassDisambiguator.cmo: multiPassDisambiguator.cmi
+multiPassDisambiguator.cmx: multiPassDisambiguator.cmi
+grafiteDisambiguate.cmo: multiPassDisambiguator.cmi grafiteDisambiguate.cmi
+grafiteDisambiguate.cmx: multiPassDisambiguator.cmx grafiteDisambiguate.cmi
grafiteWalker.cmo: grafiteParser.cmi grafiteWalker.cmi
grafiteWalker.cmx: grafiteParser.cmx grafiteWalker.cmi
print_grammar.cmo: print_grammar.cmi
grafiteParser.cmx: grafiteParser.cmi
cicNotation2.cmo: grafiteParser.cmi cicNotation2.cmi
cicNotation2.cmx: grafiteParser.cmx cicNotation2.cmi
-grafiteDisambiguator.cmo: grafiteDisambiguator.cmi
-grafiteDisambiguator.cmx: grafiteDisambiguator.cmi
-grafiteDisambiguate.cmo: grafiteDisambiguator.cmi grafiteDisambiguate.cmi
-grafiteDisambiguate.cmx: grafiteDisambiguator.cmx grafiteDisambiguate.cmi
+multiPassDisambiguator.cmo: multiPassDisambiguator.cmi
+multiPassDisambiguator.cmx: multiPassDisambiguator.cmi
+grafiteDisambiguate.cmo: multiPassDisambiguator.cmi grafiteDisambiguate.cmi
+grafiteDisambiguate.cmx: multiPassDisambiguator.cmx grafiteDisambiguate.cmi
grafiteWalker.cmo: grafiteParser.cmi grafiteWalker.cmi
grafiteWalker.cmx: grafiteParser.cmx grafiteWalker.cmi
print_grammar.cmo: print_grammar.cmi
dependenciesParser.mli \
grafiteParser.mli \
cicNotation2.mli \
- grafiteDisambiguator.mli \
+ multiPassDisambiguator.mli \
grafiteDisambiguate.mli \
grafiteWalker.mli \
print_grammar.mli \
let lexicon_status = !lexicon_status_ref in
let (diff, metasenv, subst, cic, _) =
singleton "first"
- (GrafiteDisambiguator.disambiguate_term
+ (MultiPassDisambiguator.disambiguate_term
~aliases:lexicon_status.LexiconEngine.aliases
?goal ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
~lookup_in_library
let lexicon_status = !lexicon_status_ref in
let (diff, metasenv, _, cic, ugraph) =
singleton "second"
- (GrafiteDisambiguator.disambiguate_term ~lookup_in_library
+ (MultiPassDisambiguator.disambiguate_term ~lookup_in_library
~initial_ugraph:ugraph ~aliases:lexicon_status.LexiconEngine.aliases
~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
~context ~metasenv ~subst:[] ?goal
let disambiguate_pattern
text prefix_len lexicon_status_ref (wanted, hyp_paths, goal_path)
=
- let interp path = Disambiguate.interpretate_path [] path in
+ let interp path =CicDisambiguate.interpretate_path [] path in
let goal_path = HExtlib.map_option interp goal_path in
let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
let wanted =
| None -> raise BaseUriNotSetYet)
| CicNotationPt.Inductive _ -> assert false
| CicNotationPt.Theorem _ -> None in
-(*
+ (*
(match obj with
CicNotationPt.Theorem (_,_,ty,_) ->
(try
let [_,_,_,ty],_ =
- NGrafiteDisambiguator.disambiguate_term
+ NMultiPassDisambiguator.disambiguate_term
~context:[] ~metasenv:[] ~subst:[]
~aliases:DisambiguateTypes.Environment.empty
~universe:(Some DisambiguateTypes.Environment.empty)
in
prerr_endline ("NUOVA DISAMBIGUAZIONE OK!!!!!!!!! " ^
NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] ty)
- with NGrafiteDisambiguator.DisambiguationError _ ->
+ with NMultiPassDisambiguator.DisambiguationError _ ->
prerr_endline "ERRORE NUOVA DISAMBIGUAZIONE";
assert false
| exn -> ())
| _ -> ()
- );
-*)
+ ); *)
let (diff, metasenv, _, cic, _) =
singleton "third"
- (GrafiteDisambiguator.disambiguate_obj ~lookup_in_library
+ (MultiPassDisambiguator.disambiguate_obj ~lookup_in_library
~aliases:lexicon_status.LexiconEngine.aliases
~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~uri
(text,prefix_len,obj)) in
+++ /dev/null
-(* Copyright (C) 2004-2005, 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 HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-(* $Id$ *)
-
-open Printf
-
-let debug = false;;
-let debug_print s =
- if debug then prerr_endline (Lazy.force s);;
-
-exception Ambiguous_input
-(* the integer is an offset to be added to each location *)
-exception DisambiguationError of
- int *
- ((Stdpp.location list * string * string) list *
- (DisambiguateTypes.domain_item * string) list *
- (Stdpp.location * string) Lazy.t * bool) list list
- (** parameters are: option name, error message *)
-exception Unbound_identifier of string
-
-type choose_uris_callback =
- id:string -> UriManager.uri list -> UriManager.uri list
-
-type choose_interp_callback =
- string -> int ->
- (Stdpp.location list * string * string) list list -> int list
-
-let mono_uris_callback ~id =
- if Helm_registry.get_opt_default Helm_registry.get_bool ~default:true
- "matita.auto_disambiguation"
- then
- function l -> l
- else
- raise Ambiguous_input
-
-let mono_interp_callback _ _ _ = raise Ambiguous_input
-
-let _choose_uris_callback = ref mono_uris_callback
-let _choose_interp_callback = ref mono_interp_callback
-let set_choose_uris_callback f = _choose_uris_callback := f
-let set_choose_interp_callback f = _choose_interp_callback := f
-
-module Callbacks =
- struct
- let interactive_user_uri_choice ~selection_mode ?ok
- ?(enable_button_for_non_vars = true) ~title ~msg ~id uris =
- !_choose_uris_callback ~id uris
-
- let interactive_interpretation_choice interp =
- !_choose_interp_callback interp
-
- let input_or_locate_uri ~(title:string) ?id () = None
- (* Zack: I try to avoid using this callback. I therefore assume that
- * the presence of an identifier that can't be resolved via "locate"
- * query is a syntax error *)
- end
-
-module Disambiguator = Disambiguate.Make (Callbacks)
-
-(* implement module's API *)
-
-let only_one_pass = ref false;;
-
-let disambiguate_thing ~aliases ~universe
- ~(f:?fresh_instances:bool ->
- aliases:'term DisambiguateTypes.environment ->
- universe:'term DisambiguateTypes.multiple_environment option ->
- 'a -> 'b)
- ~(drop_aliases: ?minimize_instances:bool -> 'b -> 'b)
- ~(drop_aliases_and_clear_diff: 'b -> 'b)
- (thing: 'a)
-=
- assert (universe <> None);
- let library = false, DisambiguateTypes.Environment.empty, None in
- let multi_aliases = false, DisambiguateTypes.Environment.empty, universe in
- let mono_aliases = true, aliases, Some DisambiguateTypes.Environment.empty in
- let passes = (* <fresh_instances?, aliases, coercions?> *)
- if !only_one_pass then
- [ (true, mono_aliases, false) ]
- else
- [ (true, mono_aliases, false);
- (true, multi_aliases, false);
- (true, mono_aliases, true);
- (true, multi_aliases, true);
- (true, library, false);
- (* for demo to reduce the number of interpretations *)
- (true, library, true);
- ]
- in
- let try_pass (fresh_instances, (_, aliases, universe), insert_coercions) =
- CicRefine.insert_coercions := insert_coercions;
- f ~fresh_instances ~aliases ~universe thing
- in
- let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) =
- if use_mono_aliases then
- drop_aliases ~minimize_instances:true res (* one shot aliases *)
- else if user_asked then
- drop_aliases ~minimize_instances:true res (* one shot aliases *)
- else
- drop_aliases_and_clear_diff res
- in
- let rec aux i errors passes =
- debug_print (lazy ("Pass: " ^ string_of_int i));
- match passes with
- [ pass ] ->
- (try
- set_aliases pass (try_pass pass)
- with Disambiguate.NoWellTypedInterpretation (offset,newerrors) ->
- raise (DisambiguationError (offset, errors @ [newerrors])))
- | hd :: tl ->
- (try
- set_aliases hd (try_pass hd)
- with Disambiguate.NoWellTypedInterpretation (_offset,newerrors) ->
- aux (i+1) (errors @ [newerrors]) tl)
- | [] -> assert false
- in
- let saved_insert_coercions = !CicRefine.insert_coercions in
- try
- let res = aux 1 [] passes in
- CicRefine.insert_coercions := saved_insert_coercions;
- res
- with exn ->
- CicRefine.insert_coercions := saved_insert_coercions;
- raise exn
-
-type disambiguator_thing =
- { do_it :
- 'a 'b 'term.
- aliases:'term DisambiguateTypes.environment ->
- universe:'term DisambiguateTypes.multiple_environment option ->
- f:(?fresh_instances:bool ->
- aliases:'term DisambiguateTypes.environment ->
- universe:'term DisambiguateTypes.multiple_environment option ->
- 'a -> 'b * bool) ->
- drop_aliases:(?minimize_instances:bool -> 'b * bool -> 'b * bool) ->
- drop_aliases_and_clear_diff:('b * bool -> 'b * bool) -> 'a -> 'b * bool
- }
-
-let disambiguate_thing =
- let profiler = HExtlib.profile "disambiguate_thing" in
- { do_it =
- fun ~aliases ~universe ~f ~drop_aliases ~drop_aliases_and_clear_diff thing
- -> profiler.HExtlib.profile
- (disambiguate_thing ~aliases ~universe ~f ~drop_aliases
- ~drop_aliases_and_clear_diff) thing
- }
-
-let drop_aliases ?(minimize_instances=false) (choices, user_asked) =
- let module D = DisambiguateTypes in
- let minimize d =
- if not minimize_instances then
- d
- else
- let rec aux =
- function
- [] -> []
- | (D.Symbol (s,n),((descr,_) as ci)) as he::tl when n > 0 ->
- if
- List.for_all
- (function
- (D.Symbol (s2,_),(descr2,_)) -> s2 <> s || descr = descr2
- | _ -> true
- ) d
- then
- (D.Symbol (s,0),ci)::(aux tl)
- else
- he::(aux tl)
- | (D.Num n,((descr,_) as ci)) as he::tl when n > 0 ->
- if
- List.for_all
- (function (D.Num _,(descr2,_)) -> descr = descr2 | _ -> true) d
- then
- (D.Num 0,ci)::(aux tl)
- else
- he::(aux tl)
- | he::tl -> he::(aux tl)
- in
- aux d
- in
- (List.map (fun (d, a, b, c, e) -> minimize d, a, b, c, e) choices),
- user_asked
-
-let drop_aliases_and_clear_diff (choices, user_asked) =
- (List.map (fun (_, a, b, c, d) -> [], a, b, c, d) choices),
- user_asked
-
-let disambiguate_term ?fresh_instances ~context ~metasenv ~subst ?goal ?initial_ugraph ~aliases ~universe ~lookup_in_library term
- =
- assert (fresh_instances = None);
- let f =
- Disambiguator.disambiguate_term ~lookup_in_library ~context ~metasenv ~subst ?goal ?initial_ugraph
- in
- disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
- ~drop_aliases_and_clear_diff term
-
-let disambiguate_obj ?fresh_instances ~aliases ~universe ~uri ~lookup_in_library obj =
- assert (fresh_instances = None);
- let f = Disambiguator.disambiguate_obj ~lookup_in_library ~uri in
- disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
- ~drop_aliases_and_clear_diff obj
-
-let disambiguate_thing ~context = assert false
+++ /dev/null
-(* Copyright (C) 2004-2005, 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 HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-(** raised when ambiguous input is found but not expected (e.g. in the batch
- * compiler) *)
-exception Ambiguous_input
-(* the integer is an offset to be added to each location *)
-exception DisambiguationError of
- int *
- ((Stdpp.location list * string * string) list *
- (DisambiguateTypes.domain_item * string) list *
- (Stdpp.location * string) Lazy.t * bool) list list
- (** parameters are: option name, error message *)
-
-(** initially false; for debugging only (???) *)
-val only_one_pass: bool ref
-
-type choose_uris_callback = id:string -> UriManager.uri list -> UriManager.uri list
-type choose_interp_callback =
- string -> int -> (Stdpp.location list * string * string) list list ->
- int list
-
-val set_choose_uris_callback: choose_uris_callback -> unit
-val set_choose_interp_callback: choose_interp_callback -> unit
-
-(** @raise Ambiguous_input if called, default value for internal
- * choose_uris_callback if not set otherwise with set_choose_uris_callback
- * above *)
-val mono_uris_callback: choose_uris_callback
-
-(** @raise Ambiguous_input if called, default value for internal
- * choose_interp_callback if not set otherwise with set_choose_interp_callback
- * above *)
-val mono_interp_callback: choose_interp_callback
-
-(** for GUI callbacks see MatitaGui.interactive_{interp,user_uri}_choice *)
-
-include Disambiguate.Disambiguator
--- /dev/null
+(* Copyright (C) 2004-2005, 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 HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+(* $Id$ *)
+
+open Printf
+
+let debug = false;;
+let debug_print s =
+ if debug then prerr_endline (Lazy.force s);;
+
+exception Ambiguous_input
+(* the integer is an offset to be added to each location *)
+exception DisambiguationError of
+ int *
+ ((Stdpp.location list * string * string) list *
+ (DisambiguateTypes.domain_item * string) list *
+ (Stdpp.location * string) Lazy.t * bool) list list
+ (** parameters are: option name, error message *)
+exception Unbound_identifier of string
+
+let mono_uris_callback ~selection_mode ?ok
+ ?(enable_button_for_non_vars = true) ~title ~msg ~id =
+ if Helm_registry.get_opt_default Helm_registry.get_bool ~default:true
+ "matita.auto_disambiguation"
+ then
+ function l -> l
+ else
+ raise Ambiguous_input
+
+let mono_interp_callback _ _ _ = raise Ambiguous_input
+
+let _choose_uris_callback = ref mono_uris_callback
+let _choose_interp_callback = ref mono_interp_callback
+let set_choose_uris_callback f = _choose_uris_callback := f
+let set_choose_interp_callback f = _choose_interp_callback := f
+
+module Callbacks =
+ struct
+ let interactive_user_uri_choice = !_choose_uris_callback
+
+ let interactive_interpretation_choice interp =
+ !_choose_interp_callback interp
+
+ let input_or_locate_uri ~(title:string) ?id () = None
+ (* Zack: I try to avoid using this callback. I therefore assume that
+ * the presence of an identifier that can't be resolved via "locate"
+ * query is a syntax error *)
+ end
+
+module Disambiguator = CicDisambiguate.Make (Callbacks)
+
+(* implement module's API *)
+
+let only_one_pass = ref false;;
+
+let disambiguate_thing ~aliases ~universe
+ ~(f:?fresh_instances:bool ->
+ aliases:'term DisambiguateTypes.environment ->
+ universe:'term DisambiguateTypes.multiple_environment option ->
+ 'a -> 'b)
+ ~(drop_aliases: ?minimize_instances:bool -> 'b -> 'b)
+ ~(drop_aliases_and_clear_diff: 'b -> 'b)
+ (thing: 'a)
+=
+ assert (universe <> None);
+ let library = false, DisambiguateTypes.Environment.empty, None in
+ let multi_aliases = false, DisambiguateTypes.Environment.empty, universe in
+ let mono_aliases = true, aliases, Some DisambiguateTypes.Environment.empty in
+ let passes = (* <fresh_instances?, aliases, coercions?> *)
+ if !only_one_pass then
+ [ (true, mono_aliases, false) ]
+ else
+ [ (true, mono_aliases, false);
+ (true, multi_aliases, false);
+ (true, mono_aliases, true);
+ (true, multi_aliases, true);
+ (true, library, false);
+ (* for demo to reduce the number of interpretations *)
+ (true, library, true);
+ ]
+ in
+ let try_pass (fresh_instances, (_, aliases, universe), insert_coercions) =
+ CicRefine.insert_coercions := insert_coercions;
+ f ~fresh_instances ~aliases ~universe thing
+ in
+ let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) =
+ if use_mono_aliases then
+ drop_aliases ~minimize_instances:true res (* one shot aliases *)
+ else if user_asked then
+ drop_aliases ~minimize_instances:true res (* one shot aliases *)
+ else
+ drop_aliases_and_clear_diff res
+ in
+ let rec aux i errors passes =
+ debug_print (lazy ("Pass: " ^ string_of_int i));
+ match passes with
+ [ pass ] ->
+ (try
+ set_aliases pass (try_pass pass)
+ with Disambiguate.NoWellTypedInterpretation (offset,newerrors) ->
+ raise (DisambiguationError (offset, errors @ [newerrors])))
+ | hd :: tl ->
+ (try
+ set_aliases hd (try_pass hd)
+ with Disambiguate.NoWellTypedInterpretation (_offset,newerrors) ->
+ aux (i+1) (errors @ [newerrors]) tl)
+ | [] -> assert false
+ in
+ let saved_insert_coercions = !CicRefine.insert_coercions in
+ try
+ let res = aux 1 [] passes in
+ CicRefine.insert_coercions := saved_insert_coercions;
+ res
+ with exn ->
+ CicRefine.insert_coercions := saved_insert_coercions;
+ raise exn
+
+type disambiguator_thing =
+ { do_it :
+ 'a 'b 'term.
+ aliases:'term DisambiguateTypes.environment ->
+ universe:'term DisambiguateTypes.multiple_environment option ->
+ f:(?fresh_instances:bool ->
+ aliases:'term DisambiguateTypes.environment ->
+ universe:'term DisambiguateTypes.multiple_environment option ->
+ 'a -> 'b * bool) ->
+ drop_aliases:(?minimize_instances:bool -> 'b * bool -> 'b * bool) ->
+ drop_aliases_and_clear_diff:('b * bool -> 'b * bool) -> 'a -> 'b * bool
+ }
+
+let disambiguate_thing =
+ let profiler = HExtlib.profile "disambiguate_thing" in
+ { do_it =
+ fun ~aliases ~universe ~f ~drop_aliases ~drop_aliases_and_clear_diff thing
+ -> profiler.HExtlib.profile
+ (disambiguate_thing ~aliases ~universe ~f ~drop_aliases
+ ~drop_aliases_and_clear_diff) thing
+ }
+
+let drop_aliases ?(minimize_instances=false) (choices, user_asked) =
+ let module D = DisambiguateTypes in
+ let minimize d =
+ if not minimize_instances then
+ d
+ else
+ let rec aux =
+ function
+ [] -> []
+ | (D.Symbol (s,n),((descr,_) as ci)) as he::tl when n > 0 ->
+ if
+ List.for_all
+ (function
+ (D.Symbol (s2,_),(descr2,_)) -> s2 <> s || descr = descr2
+ | _ -> true
+ ) d
+ then
+ (D.Symbol (s,0),ci)::(aux tl)
+ else
+ he::(aux tl)
+ | (D.Num n,((descr,_) as ci)) as he::tl when n > 0 ->
+ if
+ List.for_all
+ (function (D.Num _,(descr2,_)) -> descr = descr2 | _ -> true) d
+ then
+ (D.Num 0,ci)::(aux tl)
+ else
+ he::(aux tl)
+ | he::tl -> he::(aux tl)
+ in
+ aux d
+ in
+ (List.map (fun (d, a, b, c, e) -> minimize d, a, b, c, e) choices),
+ user_asked
+
+let drop_aliases_and_clear_diff (choices, user_asked) =
+ (List.map (fun (_, a, b, c, d) -> [], a, b, c, d) choices),
+ user_asked
+
+let disambiguate_term ?fresh_instances ~context ~metasenv ~subst ?goal ?initial_ugraph ~aliases ~universe ~lookup_in_library term
+ =
+ assert (fresh_instances = None);
+ let f =
+ Disambiguator.disambiguate_term ~lookup_in_library ~context ~metasenv ~subst ?goal ?initial_ugraph
+ in
+ disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
+ ~drop_aliases_and_clear_diff term
+
+let disambiguate_obj ?fresh_instances ~aliases ~universe ~uri ~lookup_in_library obj =
+ assert (fresh_instances = None);
+ let f = Disambiguator.disambiguate_obj ~lookup_in_library ~uri in
+ disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
+ ~drop_aliases_and_clear_diff obj
--- /dev/null
+(* Copyright (C) 2004-2005, 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 HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+(** raised when ambiguous input is found but not expected (e.g. in the batch
+ * compiler) *)
+exception Ambiguous_input
+(* the integer is an offset to be added to each location *)
+exception DisambiguationError of
+ int *
+ ((Stdpp.location list * string * string) list *
+ (DisambiguateTypes.domain_item * string) list *
+ (Stdpp.location * string) Lazy.t * bool) list list
+ (** parameters are: option name, error message *)
+
+(** initially false; for debugging only (???) *)
+val only_one_pass: bool ref
+
+val set_choose_uris_callback:
+ DisambiguateTypes.interactive_user_uri_choice_type -> unit
+
+val set_choose_interp_callback:
+ DisambiguateTypes.interactive_interpretation_choice_type -> unit
+
+(** @raise Ambiguous_input if called, default value for internal
+ * choose_uris_callback if not set otherwise with set_choose_uris_callback
+ * above *)
+val mono_uris_callback: DisambiguateTypes.interactive_user_uri_choice_type
+
+(** @raise Ambiguous_input if called, default value for internal
+ * choose_interp_callback if not set otherwise with set_choose_interp_callback
+ * above *)
+val mono_interp_callback: DisambiguateTypes.interactive_interpretation_choice_type
+
+(** for GUI callbacks see MatitaGui.interactive_{interp,user_uri}_choice *)
+
+include CicDisambiguate.CicDisambiguator
Disambiguate.Ko loc_msg
;;
-let resolve (env: NCic.term codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () =
- ignore (env,item,num,args);
- try
- snd (Environment.find item env) env num args
- with Not_found ->
- failwith ("Domain item not found: " ^
- (DisambiguateTypes.string_of_domain_item item))
-
(* TODO move it to Cic *)
let find_in_context name context =
let rec aux acc = function
| 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
- resolve env (Symbol (symb, i)) ~args:cic_args ()
+ Disambiguate.resolve env (Symbol (symb, i)) ~args:cic_args ()
| CicNotationPt.Appl terms ->
NCic.Appl (List.map (aux ~localize loc context) terms)
| CicNotationPt.Binder (binder_kind, (var, typ), body) ->
| `Pi
| `Forall -> NCic.Prod (cic_name, cic_type, cic_body)
| `Exists ->
- resolve env (Symbol ("exists", 0))
+ Disambiguate.resolve env (Symbol ("exists", 0))
~args:[ cic_type; NCic.Lambda (cic_name, cic_type, cic_body) ] ())
| CicNotationPt.Case (term, indty_ident, outtype, branches) ->
let cic_term = aux ~localize loc context term in
let indtype_ref =
match indty_ident with
| Some (indty_ident, _) ->
- (match resolve env (Id indty_ident) () with
+ (match Disambiguate.resolve env (Id indty_ident) () with
| NCic.Const r -> r
| NCic.Implicit _ ->
raise (Disambiguate.Try_again
"because it is an inductive type without constructors "^
"or because all patterns use wildcards")))
in
- (match resolve env (Id (fst_constructor branches)) () with
+ (match Disambiguate.resolve env (Id (fst_constructor branches)) () with
| NCic.Const r -> r
| NCic.Implicit _ ->
raise (Disambiguate.Try_again
assert (subst = None);
(try
NCic.Rel (find_in_context name context)
- with Not_found -> resolve env (Id name) ())
+ with Not_found -> Disambiguate.resolve env (Id name) ())
| CicNotationPt.Uri (name, subst) ->
assert (subst = None);
(try
| CicNotationPt.Implicit -> NCic.Implicit `Term
| CicNotationPt.UserInput -> assert false (*NCic.Implicit (Some `Hole)
patterns not implemented *)
- | CicNotationPt.Num (num, i) -> resolve env (Num i) ~num ()
+ | CicNotationPt.Num (num, i) -> Disambiguate.resolve env (Num i) ~num ()
| CicNotationPt.Meta (index, subst) ->
let cic_subst =
List.map
| CicNotationPt.Sort (`CProp _u) -> NCic.Sort (NCic.Type
[false,NUri.uri_of_string "cic:/matita/pts/CProp.univ"])
| CicNotationPt.Symbol (symbol, instance) ->
- resolve env (Symbol (symbol, instance)) ()
+ Disambiguate.resolve env (Symbol (symbol, instance)) ()
| _ -> assert false (* god bless Bologna *)
and aux_option ~localize loc context annotation = function
| None -> NCic.Implicit annotation
Disambiguator.disambiguate_thing
~context ~metasenv ~initial_ugraph:() ~aliases
~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
- ~mk_implicit:(function None -> NCic.Implicit `Term
- | Some `Closed -> NCic.Implicit `Closed)
+ ~mk_implicit:(function false -> NCic.Implicit `Term
+ | true -> NCic.Implicit `Closed)
~lookup_in_library ~domain_of_thing:domain_of_term
~interpretate_thing:(interpretate_term (?create_dummy_ids:None))
~refine_thing:refine_term (text,prefix_len,term)
nCicPp.cmi: nCic.cmo
nCicEnvironment.cmi: nUri.cmi nReference.cmi nCic.cmo
nCicReduction.cmi: nCic.cmo
-nCicTypeChecker.cmi: nUri.cmi nCic.cmo
+nCicTypeChecker.cmi: nUri.cmi nReference.cmi nCic.cmo
nCicUntrusted.cmi: nCic.cmo
nCic.cmo: nUri.cmi nReference.cmi
nCic.cmx: nUri.cmx nReference.cmx
nCic2OCic.cmx: nUri.cmx nReference.cmx nCic.cmx nCic2OCic.cmi
nCicLibrary.cmo: oCic2NCic.cmi nUri.cmi nCic2OCic.cmi nCicLibrary.cmi
nCicLibrary.cmx: oCic2NCic.cmx nUri.cmx nCic2OCic.cmx nCicLibrary.cmi
-nCicPp.cmo: nUri.cmi nReference.cmi nCicLibrary.cmi nCic.cmo nCicPp.cmi
-nCicPp.cmx: nUri.cmx nReference.cmx nCicLibrary.cmx nCic.cmx nCicPp.cmi
+nCicPp.cmo: nUri.cmi nReference.cmi nCicSubstitution.cmi nCicLibrary.cmi \
+ nCic.cmo nCicPp.cmi
+nCicPp.cmx: nUri.cmx nReference.cmx nCicSubstitution.cmx nCicLibrary.cmx \
+ nCic.cmx nCicPp.cmi
nCicEnvironment.cmo: nUri.cmi nReference.cmi nCicLibrary.cmi nCic.cmo \
nCicEnvironment.cmi
nCicEnvironment.cmx: nUri.cmx nReference.cmx nCicLibrary.cmx nCic.cmx \
nCicEnvironment.cmi
nCicReduction.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \
- nCicEnvironment.cmi nCic.cmo nCicReduction.cmi
+ nCicPp.cmi nCicEnvironment.cmi nCic.cmo nCicReduction.cmi
nCicReduction.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \
- nCicEnvironment.cmx nCic.cmx nCicReduction.cmi
+ nCicPp.cmx nCicEnvironment.cmx nCic.cmx nCicReduction.cmi
nCicTypeChecker.cmo: nUri.cmi nReference.cmi nCicUtils.cmi \
nCicSubstitution.cmi nCicReduction.cmi nCicPp.cmi nCicEnvironment.cmi \
nCic.cmo nCicTypeChecker.cmi
nReference.cmi: nUri.cmi
nCicUtils.cmi: nCic.cmx
-nCicPp.cmi: nCic.cmx
nCicSubstitution.cmi: nCic.cmx
oCic2NCic.cmi: nUri.cmi nReference.cmi nCic.cmx
nCic2OCic.cmi: nUri.cmi nReference.cmi nCic.cmx
nCicLibrary.cmi: nUri.cmi nCic.cmx
+nCicPp.cmi: nCic.cmx
nCicEnvironment.cmi: nUri.cmi nReference.cmi nCic.cmx
nCicReduction.cmi: nCic.cmx
-nCicTypeChecker.cmi: nUri.cmi nCic.cmx
+nCicTypeChecker.cmi: nUri.cmi nReference.cmi nCic.cmx
nCicUntrusted.cmi: nCic.cmx
nCic.cmo: nUri.cmi nReference.cmi
nCic.cmx: nUri.cmx nReference.cmx
nReference.cmx: nUri.cmx nReference.cmi
nCicUtils.cmo: nReference.cmi nCic.cmx nCicUtils.cmi
nCicUtils.cmx: nReference.cmx nCic.cmx nCicUtils.cmi
-nCicPp.cmo: nUri.cmi nReference.cmi nCicLibrary.cmi nCic.cmx nCicPp.cmi
-nCicPp.cmx: nUri.cmx nReference.cmx nCicLibrary.cmx nCic.cmx nCicPp.cmi
nCicSubstitution.cmo: nReference.cmi nCicUtils.cmi nCic.cmx \
nCicSubstitution.cmi
nCicSubstitution.cmx: nReference.cmx nCicUtils.cmx nCic.cmx \
nCic2OCic.cmx: nUri.cmx nReference.cmx nCic.cmx nCic2OCic.cmi
nCicLibrary.cmo: oCic2NCic.cmi nUri.cmi nCic2OCic.cmi nCicLibrary.cmi
nCicLibrary.cmx: oCic2NCic.cmx nUri.cmx nCic2OCic.cmx nCicLibrary.cmi
+nCicPp.cmo: nUri.cmi nReference.cmi nCicSubstitution.cmi nCicLibrary.cmi \
+ nCic.cmx nCicPp.cmi
+nCicPp.cmx: nUri.cmx nReference.cmx nCicSubstitution.cmx nCicLibrary.cmx \
+ nCic.cmx nCicPp.cmi
nCicEnvironment.cmo: nUri.cmi nReference.cmi nCicLibrary.cmi nCic.cmx \
nCicEnvironment.cmi
nCicEnvironment.cmx: nUri.cmx nReference.cmx nCicLibrary.cmx nCic.cmx \
nCicEnvironment.cmi
nCicReduction.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \
- nCicEnvironment.cmi nCic.cmx nCicReduction.cmi
+ nCicPp.cmi nCicEnvironment.cmi nCic.cmx nCicReduction.cmi
nCicReduction.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \
- nCicEnvironment.cmx nCic.cmx nCicReduction.cmi
+ nCicPp.cmx nCicEnvironment.cmx nCic.cmx nCicReduction.cmi
nCicTypeChecker.cmo: nUri.cmi nReference.cmi nCicUtils.cmi \
nCicSubstitution.cmi nCicReduction.cmi nCicPp.cmi nCicEnvironment.cmi \
nCic.cmx nCicTypeChecker.cmi
nCicMetaSubst.cmx: nCicMetaSubst.cmi
nCicUnification.cmo: nCicMetaSubst.cmi nCicUnification.cmi
nCicUnification.cmx: nCicMetaSubst.cmx nCicUnification.cmi
-nCicRefiner.cmo: nCicRefiner.cmi
-nCicRefiner.cmx: nCicRefiner.cmi
+nCicRefiner.cmo: nCicUnification.cmi nCicMetaSubst.cmi nCicRefiner.cmi
+nCicRefiner.cmx: nCicUnification.cmx nCicMetaSubst.cmx nCicRefiner.cmi
paramodulation/equality_indexing.cmx: paramodulation/utils.cmx \
paramodulation/equality.cmx paramodulation/equality_indexing.cmi
paramodulation/indexing.cmo: paramodulation/utils.cmi \
- paramodulation/subst.cmi paramodulation/founif.cmi \
+ paramodulation/subst.cmi proofEngineTypes.cmi paramodulation/founif.cmi \
paramodulation/equality_indexing.cmi paramodulation/equality.cmi \
paramodulation/indexing.cmi
paramodulation/indexing.cmx: paramodulation/utils.cmx \
- paramodulation/subst.cmx paramodulation/founif.cmx \
+ paramodulation/subst.cmx proofEngineTypes.cmx paramodulation/founif.cmx \
paramodulation/equality_indexing.cmx paramodulation/equality.cmx \
paramodulation/indexing.cmi
paramodulation/saturation.cmo: paramodulation/utils.cmi \
paramodulation/equality_indexing.cmx: paramodulation/utils.cmx \
paramodulation/equality.cmx paramodulation/equality_indexing.cmi
paramodulation/indexing.cmo: paramodulation/utils.cmi \
- paramodulation/subst.cmi paramodulation/founif.cmi \
+ paramodulation/subst.cmi proofEngineTypes.cmi paramodulation/founif.cmi \
paramodulation/equality_indexing.cmi paramodulation/equality.cmi \
paramodulation/indexing.cmi
paramodulation/indexing.cmx: paramodulation/utils.cmx \
- paramodulation/subst.cmx paramodulation/founif.cmx \
+ paramodulation/subst.cmx proofEngineTypes.cmx paramodulation/founif.cmx \
paramodulation/equality_indexing.cmx paramodulation/equality.cmx \
paramodulation/indexing.cmi
paramodulation/saturation.cmo: paramodulation/utils.cmi \
*)
addDebugSeparator ();
addDebugItem "enable multiple disambiguation passes (default)"
- (fun _ -> GrafiteDisambiguator.only_one_pass := false);
+ (fun _ -> MultiPassDisambiguator.only_one_pass := false);
addDebugItem "enable only one disambiguation pass"
- (fun _ -> GrafiteDisambiguator.only_one_pass := true);
+ (fun _ -> MultiPassDisambiguator.only_one_pass := true);
addDebugItem "always show all disambiguation errors"
(fun _ -> MatitaGui.all_disambiguation_passes := true);
addDebugItem "prune disambiguation errors"
None, ("Disambiguation choice not found: " ^ Lazy.force msg)
| MatitaEngine.EnrichedWithLexiconStatus (exn,_) ->
None, "EnrichedWithLexiconStatus "^snd(to_string exn)
- | GrafiteDisambiguator.DisambiguationError (offset,errorll) ->
+ | MultiPassDisambiguator.DisambiguationError (offset,errorll) ->
let loc =
match errorll with
| ((_,_,loc_msg,_)::_)::_ ->
| [loffset,[_,envs_and_diffs,msg,significant]] ->
let _,env,diff = List.hd envs_and_diffs in
notify_exn
- (GrafiteDisambiguator.DisambiguationError
+ (MultiPassDisambiguator.DisambiguationError
(offset,[[env,diff,lazy (loffset,Lazy.force msg),significant]]));
| _::_ ->
let dialog = new disambiguationErrors () in
~start:source_buffer#start_iter
~stop:source_buffer#end_iter;
notify_exn
- (GrafiteDisambiguator.DisambiguationError
+ (MultiPassDisambiguator.DisambiguationError
(offset,[[env,diff,lazy(loffset,Lazy.force msg),significant]]))
));
let return _ =
f ();
unlock_world ()
with
- | GrafiteDisambiguator.DisambiguationError (offset,errorll) ->
+ | MultiPassDisambiguator.DisambiguationError (offset,errorll) ->
(try
interactive_error_interp
~all_passes:!all_disambiguation_passes source_buffer
let _ =
(* disambiguator callbacks *)
- GrafiteDisambiguator.set_choose_uris_callback (interactive_uri_choice ());
- GrafiteDisambiguator.set_choose_interp_callback (interactive_interp_choice ());
+ MultiPassDisambiguator.set_choose_uris_callback
+ (fun ~selection_mode ?ok ?(enable_button_for_non_vars=false) ~title ~msg ->
+ interactive_uri_choice ~selection_mode ?ok_label:ok ~title ~msg ());
+ MultiPassDisambiguator.set_choose_interp_callback (interactive_interp_choice ());
(* gtk initialization *)
GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *)
GMathView.add_configuration_path BuildTimeConf.gtkmathview_conf;
?hide_uri_entry:bool -> ?hide_try:bool -> ?ok_label:string ->
?ok_action:[`AUTO|`SELECT] ->
?copy_cb:(string -> unit) -> unit ->
- GrafiteDisambiguator.choose_uris_callback
+ id:'a -> UriManager.uri list -> UriManager.uri list
(** @raise MatitaTypes.Cancel *)
val interactive_interp_choice:
unit ->
- GrafiteDisambiguator.choose_interp_callback
+ DisambiguateTypes.interactive_interpretation_choice_type
("Do not catch top-level exception "
^ "(useful for backtrace inspection)");
"-onepass",
- Arg.Unit (fun () -> GrafiteDisambiguator.only_one_pass := true),
+ Arg.Unit (fun () -> MultiPassDisambiguator.only_one_pass := true),
"Enable only one disambiguation pass";
]
else []
script ex loc
=
let module TAPp = GrafiteAstPp in
- let module MD = GrafiteDisambiguator in
+ let module MD = MultiPassDisambiguator in
let module ML = MatitaMisc in
try
ignore (buffer#move_mark (`NAME "beginning_of_statement")
HExtlib.Localized (floc, exn) ->
HExtlib.raise_localized_exception
~offset:(MatitaGtkMisc.utf8_string_length parsed_text) floc exn
- | GrafiteDisambiguator.DisambiguationError (offset,errorll) ->
+ | MultiPassDisambiguator.DisambiguationError (offset,errorll) ->
raise
- (GrafiteDisambiguator.DisambiguationError
+ (MultiPassDisambiguator.DisambiguationError
(offset+parsed_text_length, errorll))
in
assert (text=""); (* no macros inside comments, please! *)
projects / helm.git / commitdiff