let choices_avg = ref 0.
*)
-let descr_of_domain_item = function
- | Id s -> s
- | Symbol (s, _) -> s
- | Num i -> string_of_int i
-
type ('term,'metasenv,'subst,'graph) test_result =
| Ok of 'term * 'metasenv * 'subst * 'graph
| Ko of (Stdpp.location * string) Lazy.t
let string_of_name =
function
- | Ast.Ident (n, None) -> Some n
+ | Ast.Ident (n, _) -> Some n
| _ -> assert false
;;
domain_of_term ~loc ~context term
| Ast.AttributedTerm (_, term) ->
domain_of_term ~loc ~context term
- | Ast.Symbol (symbol, instance) ->
- [ Node ([loc], Symbol (symbol, instance), []) ]
+ | Ast.Symbol (name, attr) ->
+ [ Node ([loc], Symbol (name,attr), []) ]
(* to be kept in sync with Ast.Appl (Ast.Symbol ...) *)
- | Ast.Appl (Ast.Symbol (symbol, instance) as hd :: args)
- | Ast.Appl (Ast.AttributedTerm (_,Ast.Symbol (symbol, instance)) as hd :: args)
+ | Ast.Appl (Ast.Symbol (name, attr) as hd :: args)
+ | Ast.Appl (Ast.AttributedTerm (_,Ast.Symbol (name,attr)) as hd :: args)
->
let args_dom =
List.fold_right
Ast.AttributedTerm (`Loc loc,_) -> loc
| _ -> loc
in
- [ Node ([loc], Symbol (symbol, instance), args_dom) ]
- | Ast.Appl (Ast.Ident (name, subst) as hd :: args)
- | Ast.Appl (Ast.AttributedTerm (_,Ast.Ident (name, subst)) as hd :: args) ->
+ [ Node ([loc], Symbol (name,attr), args_dom) ]
+ | Ast.Appl (Ast.Ident (id,uri) as hd :: args)
+ | Ast.Appl (Ast.AttributedTerm (_,Ast.Ident (id,uri)) as hd :: args) ->
+ let uri = match uri with
+ | `Uri u -> Some u
+ | _ -> None
+ in
let args_dom =
List.fold_right
(fun term acc -> domain_of_term ~loc ~context term @ acc)
in
(try
(* the next line can raise Not_found *)
- ignore(find_in_context name context);
- if subst <> None then
- Ast.fail loc "Explicit substitutions not allowed here"
- else
+ ignore(find_in_context id context);
args_dom
with Not_found ->
- (match subst with
- | None -> [ Node ([loc], Id name, args_dom) ]
- | Some subst ->
- let terms =
- List.fold_left
- (fun dom (_, term) ->
- let dom' = domain_of_term ~loc ~context term in
- dom @ dom')
- [] subst in
- [ Node ([loc], Id name, terms @ args_dom) ]))
+ [ Node ([loc], Id (id,uri), args_dom) ] )
| Ast.Appl terms ->
List.fold_right
(fun term acc -> domain_of_term ~loc ~context term @ acc)
domain_of_term ~loc
~context:(string_of_name var :: context) body in
(match kind with
- | `Exists -> [ Node ([loc], Symbol ("exists", 0), (type_dom @ body_dom)) ]
+ | `Exists -> [ Node ([loc], Symbol ("exists",None), (type_dom @ body_dom)) ]
| _ -> type_dom @ body_dom)
| Ast.Case (term, indty_ident, outtype, branches) ->
let term_dom = domain_of_term ~loc ~context term in
let outtype_dom = domain_of_term_option ~loc ~context outtype in
let rec get_first_constructor = function
| [] -> []
- | (Ast.Pattern (head, _, _), _) :: _ -> [ Node ([loc], Id head, []) ]
+ | (Ast.Pattern (head, Some r, _), _) :: _ ->
+ [ Node ([loc], Id (head,Some (NReference.string_of_reference r)), []) ]
+ | (Ast.Pattern (head, None, _), _) :: _ ->
+ [ Node ([loc], Id (head,None), []) ]
| _ :: tl -> get_first_constructor tl in
let do_branch =
function
List.fold_left (fun dom branch -> dom @ do_branch branch) [] branches in
(match indty_ident with
| None -> get_first_constructor branches
- | Some (ident, _) -> [ Node ([loc], Id ident, []) ])
+ | Some (ident, None) -> [ Node ([loc], Id (ident,None) , []) ]
+ | Some (ident, Some r) ->
+ [ Node ([loc], Id (ident,Some (NReference.string_of_reference r)), []) ])
@ term_dom @ outtype_dom @ branches_dom
| Ast.Cast (term, ty) ->
let term_dom = domain_of_term ~loc ~context term in
) [] defs
in
defs_dom @ where_dom
- | Ast.Ident (name, subst) ->
+ | Ast.Ident (name, x) ->
+ let x = match x with
+ | `Uri u -> Some u
+ | _ -> None
+ in
(try
(* the next line can raise Not_found *)
- ignore(find_in_context name context);
- if subst <> None then
- Ast.fail loc "Explicit substitutions not allowed here"
- else
- []
+ ignore(find_in_context name context); []
with Not_found ->
+ (*
(match subst with
| None -> [ Node ([loc], Id name, []) ]
| Some subst ->
let dom' = domain_of_term ~loc ~context term in
dom @ dom')
[] subst in
- [ Node ([loc], Id name, terms) ]))
- | Ast.Uri _ -> []
+ [ Node ([loc], Id name, terms) ]))*)
+ [ Node ([loc], Id (name,x), []) ])
| Ast.NRef _ -> []
| Ast.NCic _ -> []
| Ast.Implicit _ -> []
let is_in_dom2 elt =
List.exists
(function
- | Symbol (symb, 0) ->
+ | Symbol (symb,None) ->
(match elt with
Symbol (symb',_) when symb = symb' -> true
| _ -> false)
- | Num i ->
+ | Num _ ->
(match elt with
Num _ -> true
| _ -> false)
let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
+(* generic function lifting splitting from type T to type (T list) *)
+let rec list_split item_split ctx pre post =
+ match post with
+ | [] -> []
+ | x :: post' ->
+ (item_split (fun v1 -> ctx (pre@v1::post')) x)@
+ list_split item_split ctx (pre@[x]) post'
+;;
+
+(* splits a 'term capture_variable *)
+let var_split ctx = function
+ | (_,None) -> []
+ | (v,Some ty) -> [(fun x -> ctx (v,Some x)),ty]
+;;
+
+let ity_split ctx (n,isind,ty,cl) =
+ [(fun x -> ctx (n,isind,x,cl)),ty]@
+ list_split (fun ctx0 (v,ty) -> [(fun x -> ctx0 (v,x)),ty])
+ (fun x -> ctx (n,isind,ty,x)) [] cl
+;;
+
+let field_split ctx (n,ty,b,m) =
+ [(fun x -> ctx (n,x,b,m)),ty]
+;;
+
+(* splits a defn. in a mutual LetRec block *)
+let letrecaux_split ctx (args,f,bo,n) =
+ list_split var_split (fun x -> ctx (x,f,bo,n)) [] args@
+ var_split (fun x -> ctx (args,x,bo,n)) f@
+ [(fun x -> ctx (args,f,x,n)),bo]
+;;
+
+(* splits a pattern (for case analysis) *)
+let pattern_split ctx = function
+ | Ast.Wildcard -> []
+ | Ast.Pattern (s,href,pl) ->
+ let rec auxpatt pre = function
+ | [] -> []
+ | (x,Some y as x')::post' ->
+ ((fun v -> ctx (Ast.Pattern (s,href,pre@(x,Some v)::post'))),y)
+ ::auxpatt (pre@[x']) post'
+ | (x,None as x')::post' -> auxpatt (pre@[x']) post'
+ in auxpatt [] pl
+;;
+
+ (* this function is used to get the children of a given node, together with
+ * their context
+ * contexts are expressed in the form of functions Ast -> Ast *)
+(* split : ('term -> 'a) -> 'term -> (('term -> 'a) * 'term) list *)
+let rec split ctx = function
+ | Ast.AttributedTerm (attr,t) ->
+ [(fun x -> ctx (Ast.AttributedTerm(attr,x))),t]
+ | Ast.Appl tl -> list_split split (fun x -> ctx (Ast.Appl x)) [] tl
+ | Ast.Binder (k,((n,None) as n'),body) ->
+ [ (fun v -> ctx (Ast.Binder (k,n',v))),body]
+ | Ast.Binder (k,((n,Some ty) as n'),body) ->
+ [(fun v -> ctx (Ast.Binder (k,(n,Some v),body))), ty
+ ;(fun v -> ctx (Ast.Binder (k,n',v))),body]
+ | Ast.Case (t,ity,outty,pl) ->
+ let outty_split = match outty with
+ | None -> []
+ | Some u -> [(fun x -> ctx (Ast.Case (t,ity,Some x,pl))),u]
+ in
+ ((fun x -> ctx (Ast.Case (x,ity,outty,pl))),t)::
+ outty_split@list_split
+ (fun ctx0 (p,x) ->
+ ((fun y -> ctx0 (p,y)),x)::pattern_split
+ (fun y -> ctx0 (y,x)) p) (fun x -> ctx (Ast.Case(t,ity,outty,x)))
+ [] pl
+ | Ast.Cast (u,v) -> [ (fun x -> ctx (Ast.Cast (x,v))),u
+ ; (fun x -> ctx (Ast.Cast (u,x))),v ]
+ | Ast.LetIn ((n,None) as n',u,v) ->
+ [ (fun x -> ctx (Ast.LetIn (n',x,v))), u
+ ; (fun x -> ctx (Ast.LetIn (n',u,x))), v ]
+ | Ast.LetIn ((n,Some t) as n',u,v) ->
+ [ (fun x -> ctx (Ast.LetIn ((n,Some x),u,v))), t
+ ; (fun x -> ctx (Ast.LetIn (n',x,v))), u
+ ; (fun x -> ctx (Ast.LetIn (n',u,x))), v ]
+ | Ast.LetRec (k,funs,where) -> (* we do not use where any more?? *)
+ list_split letrecaux_split (fun x -> ctx (Ast.LetRec(k,x,where))) [] funs
+ | _ -> [] (* leaves *)
+;;
+
+
+(* top_split : 'a -> ((term -> 'a) * term) list
+ * returns all the possible top-level (ctx,t) for its input *)
+let bfvisit ~pp_term top_split test t =
+ let rec aux = function
+ | [] -> None
+ | (ctx0,t0 as hd)::tl ->
+(* prerr_endline ("ok! length tl = " ^ string_of_int (List.length tl)); *)
+ prerr_endline ("t0 = " ^ pp_term t0);
+ if test t0 then (prerr_endline "caso 1"; Some hd)
+ else
+ let t0' = split ctx0 t0 in
+ (prerr_endline ("caso 2: length t0' = " ^ string_of_int
+ (List.length t0')); aux (tl@t0' (*split ctx0 t0*)))
+ (* in aux [(fun x -> x),t] *)
+ in aux (top_split t)
+;;
+
+let obj_split (o:Ast.term Ast.obj) = match o with
+ | Ast.Inductive (ls,itl) ->
+ list_split var_split (fun x -> Ast.Inductive (x,itl)) [] ls@
+ list_split ity_split (fun x -> Ast.Inductive (ls,x)) [] itl
+ | Ast.Theorem (flav,n,ty,None,p) ->
+ [(fun x -> Ast.Theorem (flav,n,x,None,p)), ty]
+ | Ast.Theorem (flav,n,ty,(Some bo as bo'),p) ->
+ [(fun x -> Ast.Theorem (flav,n,x,bo',p)), ty
+ ;(fun x -> Ast.Theorem (flav,n,ty,Some x,p)), bo]
+ | Ast.Record (ls,n,ty,fl) ->
+ list_split var_split (fun x -> Ast.Record (x,n,ty,fl)) [] ls@
+ [(fun x -> Ast.Record (ls,n,x,fl)),ty]@
+ list_split field_split (fun x -> Ast.Record (ls,n,ty,x)) [] fl
+;;
+
+let bfvisit_obj = bfvisit obj_split;;
+
+let bfvisit = bfvisit (fun t -> [(fun x -> x),t]) ;;
+
+(*let rec initialize_ast (* ~aliases *) ~universe ~lookup_in_library t =
+ let mk_alias = function
+ | Ast.Ident (id,_) -> DisambiguateTypes.Id (id,None)
+ | Ast.Symbol (sym,_) -> DisambiguateTypes.Symbol (sym,None)
+ | Ast.Num _ -> DisambiguateTypes.Num None
+ | _ -> assert false
+ in
+ let lookup_choices =
+ fun item ->
+ (*match universe with
+ | None ->
+ lookup_in_library
+ interactive_user_uri_choice
+ input_or_locate_uri item
+ | Some e ->
+ (try Environment.find item e
+ with Not_found -> [])
+*)
+ (try Environment.find item universe
+ with Not_found -> [])
+ in
+ match t with
+ | Ast.Ident (_,None)
+ | Ast.Num (_,None)
+ | Ast.Symbol (_,None) ->
+ let choices = lookup_choices (mk_alias t) in
+ if List.length choices <> 1 then t
+ else List.hd choices
+ (* but we lose info on closedness *)
+ | t -> Ast.map (initialize_ast ~universe ~lookup_in_library) t
+;;
+*)
+
+let domain_item_of_ast = function
+ | Ast.Ident (id,_) -> DisambiguateTypes.Id (id,None)
+ | Ast.Symbol (sym,_) -> DisambiguateTypes.Symbol (sym,None)
+ | Ast.Num (n,_) -> DisambiguateTypes.Num None
+ | Ast.Case(_,Some (ityname,_),_,_) -> DisambiguateTypes.Id (ityname,None)
+ | _ -> assert false
+;;
+
+let ast_of_alias_spec t alias = match (t,alias) with
+ | Ast.Ident _, GrafiteAst.Ident_alias (id,uri) -> Ast.Ident(id,`Uri uri)
+ | Ast.Case (t,_,oty,pl), GrafiteAst.Ident_alias (id,uri) ->
+ Ast.Case (t,Some (id,Some (NReference.reference_of_string uri)),oty,pl)
+ | _, GrafiteAst.Symbol_alias (sym,uri,desc) -> Ast.Symbol (sym,Some (uri,desc))
+ | Ast.Num(m,_), GrafiteAst.Number_alias (uri,desc) -> Ast.Num(m,Some (uri,desc))
+ | _ -> assert false
+;;
+
+let test_interpr ~context ~metasenv ~subst ~use_coercions ~expty ~env ~uri
+ ~interpretate_thing ~refine_thing ~ugraph ~mk_localization_tbl t =
+ try
+ let localization_tbl = mk_localization_tbl 503 in
+ let cic_thing =
+ interpretate_thing ~context ~env
+ ~uri ~is_path:false t ~localization_tbl
+ in
+ let foo () =
+ refine_thing metasenv subst context uri
+ ~use_coercions cic_thing expty ugraph ~localization_tbl
+ in match (refine_profiler.HExtlib.profile foo ()) with
+ | Ko _ -> false
+ | _ -> true
+ with
+ (*| Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg))
+ | Invalid_choice loc_msg -> Ko loc_msg*)
+ | Invalid_choice _ -> false
+ | _ -> true
+;;
+
+let rec disambiguate_list
+ ~context ~metasenv ~subst ~use_coercions ~expty ~env ~uri ~interpretate_thing
+ ~refine_thing ~ugraph ~visit ~universe ~mk_localization_tbl ~pp_thing ~pp_term ts =
+ let disambiguate_list =
+ disambiguate_list ~context ~metasenv ~subst ~use_coercions ~expty ~env ~uri
+ ~interpretate_thing ~refine_thing ~ugraph ~visit ~universe
+ ~mk_localization_tbl ~pp_thing ~pp_term
+ in
+ let test_interpr = test_interpr ~context ~metasenv ~subst ~use_coercions ~expty
+ ~env ~uri ~interpretate_thing ~refine_thing ~ugraph ~mk_localization_tbl
+ in
+ let find_choices item =
+ let a2s = function
+ | GrafiteAst.Ident_alias (id,_)
+ | GrafiteAst.Symbol_alias (id,_,_) -> id
+ | GrafiteAst.Number_alias _ -> "NUM"
+ in
+ let d2s = function
+ | Id (id,_)
+ | Symbol (id,_) -> id
+ | Num _ -> "NUM"
+ in
+ let res =
+ Environment.find item universe
+ in
+ prerr_endline (Printf.sprintf "choices for %s :\n%s"
+ (d2s item) (String.concat ", " (List.map a2s res)));
+ res
+ in
+
+ let get_instances ctx t =
+ try
+ let choices = find_choices (domain_item_of_ast t) in
+ List.map (fun t0 -> ctx (ast_of_alias_spec t t0)) choices
+ with
+ | Not_found -> []
+ in
+
+ match ts with
+ | [] -> None
+ | t0 :: tl ->
+ prerr_endline ("disambiguation of t0 = " ^ pp_thing t0);
+ let is_ambiguous = function
+ | Ast.Ident (_,`Ambiguous)
+ | Ast.Num (_,None)
+ | Ast.Symbol (_,None) -> true
+ | Ast.Case (_,Some (ity,None),_,_) ->
+ (prerr_endline ("ambiguous case" ^ ity);true)
+ | Ast.Case (_,None,_,_) -> prerr_endline "amb1";false
+ | Ast.Case (_,Some (ity,Some r),_,_) ->
+ (prerr_endline ("amb2 " ^ NReference.string_of_reference r);false)
+ | Ast.Ident (n,`Uri u) ->
+ (prerr_endline ("uri " ^ u ^ "inside IDENT " ^ n) ;false )
+ | _ -> false
+ in
+ let astpp = function
+ | Ast.Ident (id,_) -> "ID " ^ id
+ | Ast.Num _ -> "NUM"
+ | Ast.Symbol (sym,_) -> "SYM " ^ sym
+ | _ -> "ERROR!"
+ in
+ (* get first ambiguous subterm (or return disambiguated term) *)
+ match visit ~pp_term is_ambiguous t0 with
+ | None ->
+ prerr_endline ("not ambiguous:\n" ^ pp_thing t0);
+ Some (t0,tl)
+ | Some (ctx, t) ->
+ prerr_endline ("disambiguating node " ^ astpp t ^
+ "\nin " ^ pp_thing (ctx t));
+ (* get possible instantiations of t *)
+ let instances = get_instances ctx t in
+ (* perforate ambiguous subterms and test refinement *)
+ let survivors = List.filter test_interpr instances in
+ disambiguate_list (survivors@tl)
+;;
+
+
+(* let rec aux l =
+ match l with
+ | [] -> None
+ | (ctx,u)::vl ->
+ if test u
+ then (ctx,u)
+ else aux (vl@split ctx u)
+ in aux [t]
+;;*)
+
+(* let rec instantiate_ast = function
+ | Ident (n,Some _)
+ | Symbol (s,Some _)
+ | Num (n,Some _) as t -> []
+ | Ident (n,None) -> (* output: all possible instantiations of n *)
+ | Symbol (s,None) ->
+ | Num (n,None) ->
+
+
+ | AttributedTerm (a,u) -> AttributedTerm (a,f u)
+ | Appl tl -> Appl (List.map f tl)
+ | Binder (k,n,body) -> Binder (k,n,f body)
+ | Case (t,ity,oty,pl) ->
+ let pl' = List.map (fun (p,u) -> p,f u) pl in
+ Case (f t,ity,map_option f oty,pl')
+ | Cast (u,v) -> Cast (f u,f v)
+ | LetIn (n,u,v) -> LetIn (n,f u,f v)
+ | LetRec -> ada (* TODO *)
+ | t -> t
+*)
+
+let disambiguate_thing
+ ~context ~metasenv ~subst ~use_coercions
+ ~string_context_of_context
+ ~initial_ugraph:base_univ ~expty
+ ~mk_implicit ~description_of_alias ~fix_instance
+ ~aliases ~universe ~lookup_in_library
+ ~uri ~pp_thing ~pp_term ~domain_of_thing ~interpretate_thing ~refine_thing
+ ~visit ~mk_localization_tbl
+ (thing_txt,thing_txt_prefix_len,thing)
+=
+(* XXX: will be thrown away *)
+ let todo_dom = domain_of_thing ~context:(string_context_of_context context) thing
+ in
+ let rec aux_env env = function
+ | [] -> env
+ | Node (_, item, l) :: tl ->
+ let env =
+ Environment.add item
+ (mk_implicit
+ (match item with | Id _ | Num _ -> true | Symbol _ -> false))
+ env in
+ aux_env (aux_env env l) tl in
+ let env = aux_env aliases todo_dom in
+
+ let test_interpr = test_interpr ~context ~metasenv ~subst ~use_coercions ~expty
+ ~env ~uri ~interpretate_thing ~refine_thing ~ugraph:base_univ ~mk_localization_tbl
+ in
+(* real function *)
+ let rec aux tl =
+ match disambiguate_list ~mk_localization_tbl ~context ~metasenv ~subst
+ ~interpretate_thing ~refine_thing ~ugraph:base_univ ~visit
+ ~use_coercions ~expty ~uri ~env ~universe ~pp_thing
+ ~pp_term tl with
+ | None -> []
+ | Some (t,tl') -> t::aux tl'
+ in
+
+ let refine t =
+ let localization_tbl = mk_localization_tbl 503 in
+ match refine_thing metasenv subst context uri
+ ~use_coercions
+ (interpretate_thing ~context ~env ~uri ~is_path:false t ~localization_tbl)
+ expty base_univ ~localization_tbl with
+ | Ok (t',m',s',u') -> ([]:(Environment.key * 'f) list),m',s',t',u'
+ | Uncertain x ->
+ let _,err = Lazy.force x in
+ prerr_endline ("refinement uncertain after disambiguation: " ^ err);
+ assert false
+ | _ -> assert false
+ in
+ if not (test_interpr thing) then raise (NoWellTypedInterpretation (0,[]))
+ else
+ let res = aux [thing] in
+ let res =
+ HExtlib.filter_map (fun t -> try Some (refine t) with _ -> None) res
+ in
+ match res with
+ | [] -> raise (NoWellTypedInterpretation (0,[]))
+ | [t] -> res,false
+ | _ -> res,true
+;;
+
+(*
let disambiguate_thing
~context ~metasenv ~subst ~use_coercions
~string_context_of_context
true
in
res
+ *)
projects / helm.git / blobdiff