type domain = domain_tree list
and domain_tree = Node of Stdpp.location list * domain_item * domain
-let mono_uris_callback ~selection_mode ?ok
- ?(enable_button_for_non_vars = true) ~title ~msg ~id =
+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
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
+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 *)
match snd (mk_choice (Environment.find item env)), arg with
`Num_interp f, `Num_arg n -> f n
| `Sym_interp f, `Args l -> f l
- | `Sym_interp f, `Num_arg n -> (* Implicit number! *) f []
+ | `Sym_interp f, `Num_arg _n -> (* Implicit number! *) f []
| _,_ -> assert false
with Not_found ->
failwith ("Domain item not found: " ^
let find_in_context name context =
let rec aux acc = function
| [] -> raise Not_found
- | Some hd :: tl when hd = name -> acc
+ | Some hd :: _tl when hd = name -> acc
| _ :: tl -> aux (acc + 1) tl
in
aux 1 context
| _ :: tl -> get_first_constructor tl in
let do_branch =
function
- Ast.Pattern (head, _, args), term ->
+ Ast.Pattern (_head, _, args), term ->
let (term_context, args_domain) =
List.fold_left
(fun (cont, dom) (name, typ) ->
let where_dom =
domain_of_term ~loc ~context:(string_of_name var :: context) where in
body_dom @ type_dom @ where_dom
- | Ast.LetRec (kind, defs, where) ->
- let add_defs context =
- List.fold_left
- (fun acc (_, (var, _), _, _) -> string_of_name var :: acc
- ) context defs in
- let where_dom = domain_of_term ~loc ~context:(add_defs context) where in
- let defs_dom =
- List.fold_left
- (fun dom (params, (_, typ), body, _) ->
- let context' =
- add_defs
- (List.fold_left
- (fun acc (var,_) -> string_of_name var :: acc)
- context params)
- in
- List.rev
- (snd
- (List.fold_left
- (fun (context,res) (var,ty) ->
- string_of_name var :: context,
- domain_of_term_option ~loc ~context ty @ res)
- (add_defs context,[]) params))
- @ dom
- @ domain_of_term_option ~loc ~context:context' typ
- @ domain_of_term ~loc ~context:context' body
- ) [] defs
- in
- defs_dom @ where_dom
| Ast.Ident (name, subst) ->
(try
(* the next line can raise Not_found *)
| Ast.NRef _ -> []
| Ast.NCic _ -> []
| Ast.Implicit _ -> []
- | Ast.Num (num, i) -> [ Node ([loc], Num i, []) ]
- | Ast.Meta (index, local_context) ->
+ | Ast.Num (_num, i) -> [ Node ([loc], Num i, []) ]
+ | Ast.Meta (_index, local_context) ->
List.fold_left
(fun dom term -> dom @ domain_of_term_option ~loc ~context term)
[] local_context
let domain_of_term ~context term =
uniq_domain (domain_of_term ~context term)
+let domain_of_term_option ~context = function
+ | None -> []
+ | Some term -> domain_of_term ~context term
+
let domain_of_obj ~context ast =
assert (context = []);
match ast with
- | Ast.Theorem (_,_,ty,bo,_) ->
+ | Ast.Theorem (_,ty,bo,_) ->
domain_of_term [] ty
@ (match bo with
None -> []
| Some bo -> domain_of_term [] bo)
- | Ast.Inductive (params,tyl) ->
+ | Ast.Inductive (params,tyl,_) ->
let context, dom =
List.fold_left
(fun (context, dom) (var, ty) ->
List.map
(fun (_,ty) -> domain_of_term context_w_types ty) cl))
tyl)
- | Ast.Record (params,var,ty,fields) ->
+ | Ast.Record (params,var,ty,fields,_) ->
let context, dom =
List.fold_left
(fun (context, dom) (var, ty) ->
(fun (context,res) (name,ty,_,_) ->
Some name::context, res @ domain_of_term context ty
) (context_w_types,[]) fields)
+ | Ast.LetRec (_kind, defs, _) ->
+ let add_defs context =
+ List.fold_left
+ (fun acc (_, (var, _), _, _) -> string_of_name var :: acc
+ ) context defs in
+ let defs_dom =
+ List.fold_left
+ (fun dom (params, (_, typ), body, _) ->
+ let context' =
+ add_defs
+ (List.fold_left
+ (fun acc (var,_) -> string_of_name var :: acc)
+ context params)
+ in
+ List.rev
+ (snd
+ (List.fold_left
+ (fun (context,res) (var,ty) ->
+ string_of_name var :: context,
+ domain_of_term_option ~context ty @ res)
+ (add_defs context,[]) params))
+ @ dom
+ @ domain_of_term_option ~context:context' typ
+ @ domain_of_term ~context:context' body
+ ) [] defs
+ in
+ defs_dom
let domain_of_obj ~context obj =
uniq_domain (domain_of_obj ~context obj)
(match elt with
Symbol (symb',_) when symb = symb' -> true
| _ -> false)
- | Num i ->
+ | Num _i ->
(match elt with
Num _ -> true
| _ -> false)
let aliases, todo_dom =
let rec aux (aliases,acc) = function
| [] -> aliases, acc
- | (Node (_, item,extra) as node) :: tl ->
+ | Node (locs, item,extra) :: tl ->
let choices = lookup_choices item in
- if List.length choices <> 1 then aux (aliases, acc@[node]) tl
+ if List.length choices = 0 then
+ (* Quick failure *)
+ raise (NoWellTypedInterpretation (0,[[],[],(lazy (List.hd locs, "No choices for " ^ string_of_domain_item item)),true]))
+ else if List.length choices <> 1 then
+ let aliases,extra = aux (aliases,[]) extra in
+ aux (aliases, acc@[Node (locs,item,extra)]) tl
else
let tl = tl @ extra in
if Environment.mem item aliases then aux (aliases, acc) tl
in
aux (aliases,[]) todo_dom
in
+ debug_print
+ (lazy(sprintf "TODO DOM: %s"(string_of_domain todo_dom)));
(*
(* <benchmark> *)
(lazy (List.hd locs,
"No choices for " ^ string_of_domain_item item)),
true]
-(*
- | [codomain_item] ->
- (* just one choice. We perform a one-step look-up and
- if the next set of choices is also a singleton we
- skip this refinement step *)
- debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
- let new_env = Environment.add item codomain_item aliases in
- let new_diff = (item,codomain_item)::diff in
- let lookup_in_todo_dom,next_choice_is_single =
- match remaining_dom with
- [] -> None,false
- | (_,he)::_ ->
- let choices = lookup_choices he in
- Some choices,List.length choices = 1
- in
- if next_choice_is_single then
- aux new_env new_diff lookup_in_todo_dom remaining_dom
- base_univ
- else
- (match test_env new_env remaining_dom base_univ with
- | Ok (thing, metasenv),new_univ ->
- (match remaining_dom with
- | [] ->
- [ new_env, new_diff, metasenv, thing, new_univ ], []
- | _ ->
- aux new_env new_diff lookup_in_todo_dom
- remaining_dom new_univ)
- | Uncertain (loc,msg),new_univ ->
- (match remaining_dom with
- | [] -> [], [new_env,new_diff,loc,msg,true]
- | _ ->
- aux new_env new_diff lookup_in_todo_dom
- remaining_dom new_univ)
- | Ko (loc,msg),_ -> [], [new_env,new_diff,loc,msg,true])
-*)
| _::_ ->
let mark_not_significant failures =
List.map
(inner_dom@remaining_dom@rem_dom) base_univ
with
| Ok (thing, metasenv,subst,new_univ) ->
-(* prerr_endline "OK"; *)
+(*prerr_endline ((sprintf "CHOOSED ITEM OK: %s" (string_of_domain_item item)));*)
let res =
(match inner_dom with
| [] ->
in
res @@ filter tl
| Uncertain loc_msg ->
-(* prerr_endline ("UNCERTAIN"); *)
+(*prerr_endline ((sprintf "CHOOSED ITEM UNCERTAIN: %s" (string_of_domain_item item) ^ snd (Lazy.force loc_msg)));*)
let res =
(match inner_dom with
| [] -> [],[new_env,new_diff,loc_msg],[]
in
res @@ filter tl
| Ko loc_msg ->
-(* prerr_endline "KO"; *)
+(*prerr_endline ((sprintf "CHOOSED ITEM KO: %s" (string_of_domain_item item)));*)
let res = [],[],[new_env,new_diff,loc_msg,true] in
res @@ filter tl)
in
Not_found -> None)
thing_dom
in
- let diff= List.map (fun a,b -> a,description_of_alias b) diff in
+ let diff= List.map (fun (a,b) -> a,description_of_alias b) diff in
env',diff,loc_msg,significant
) errors
in
projects / helm.git / blobdiff