X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=139a6417a3c33c6f6f4fb4328794ac4802a5195c;hb=c5d5bf37b1e4c4b9b499ed2cbfe27cf2ec181944;hp=06f18080d07466aaccba41ca71b3d83599ae4678;hpb=b029556cbcecb852dfc9cf25801f3dcc0bb762bb;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 06f18080d..139a6417a 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -57,13 +57,14 @@ let refine metasenv context term = | CicRefine.Uncertain _ -> debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ; Uncertain - | _ -> - (* TODO we should catch only the RefineFailure excecption *) + | CicRefine.RefineFailure _ -> debug_print ("%%% PRUNED!!! " ^ CicPp.ppterm term) ; Ko let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () = - snd (Environment.find item env) env num args + try + snd (Environment.find item env) env num args + with Not_found -> assert false (* TODO move it to Cic *) let find_in_environment name context = @@ -180,10 +181,9 @@ let interpretate ~context ~env ast = in List.fold_right (build_term inductiveFuns) inductiveFuns cic_body | CicAst.Ident (name, subst) -> - (* TODO hanlde explicit substitutions *) (try let index = find_in_environment name context in - if subst <> [] then + if subst <> None then CicTextualParser2.fail loc "Explicit substitutions not allowed here"; Cic.Rel index @@ -193,12 +193,16 @@ let interpretate ~context ~env ast = let ids_to_uris = List.map (fun uri -> UriManager.name_of_uri uri, uri) uris in - List.map - (fun (s, term) -> - (try - List.assoc s ids_to_uris, aux loc context term - with Not_found -> raise DisambiguateChoices.Invalid_choice)) - subst + (match subst with + | Some subst -> + List.map + (fun (s, term) -> + (try + List.assoc s ids_to_uris, aux loc context term + with Not_found -> + raise DisambiguateChoices.Invalid_choice)) + subst + | None -> List.map (fun uri -> uri, Cic.Implicit None) uris) in (match cic with | Cic.Const (uri, []) -> @@ -253,7 +257,7 @@ let interpretate ~context ~env ast = Cic.Meta (index, cic_subst) | CicAst.Sort `Prop -> Cic.Sort Cic.Prop | CicAst.Sort `Set -> Cic.Sort Cic.Set - | CicAst.Sort `Type -> Cic.Sort Cic.Type + | CicAst.Sort `Type -> Cic.Sort (Cic.Type (CicUniv.fresh())) (* TASSI *) | CicAst.Sort `CProp -> Cic.Sort Cic.CProp | CicAst.Symbol (symbol, instance) -> resolve env (Symbol (symbol, instance)) () @@ -274,10 +278,15 @@ let domain_of_term ~context ast = | CicAst.AttributedTerm (_, term) -> aux loc context term | CicAst.Appl terms -> List.fold_left (fun dom term -> aux loc context term @ dom) [] terms - | CicAst.Binder (_, (var, typ), body) -> + | CicAst.Binder (kind, (var, typ), body) -> + let kind_dom = + match kind with + | `Exists -> [ Symbol ("exists", 0) ] + | _ -> [] + in let type_dom = aux_option loc context typ in let body_dom = aux loc (var :: context) body in - body_dom @ type_dom + body_dom @ type_dom @ kind_dom | CicAst.Case (term, indty_ident, outtype, branches) -> let term_dom = aux loc context term in let outtype_dom = aux_option loc context outtype in @@ -317,19 +326,22 @@ let domain_of_term ~context ast = in where_dom @ defs_dom | CicAst.Ident (name, subst) -> - (* TODO hanlde explicit substitutions *) (try let index = find_in_environment name context in - if subst <> [] then + if subst <> None then CicTextualParser2.fail loc - "Explicit substitutions not allowed here"; - [] + "Explicit substitutions not allowed here" + else + [] with Not_found -> - List.fold_left - (fun dom (_, term) -> - let dom' = aux loc context term in - dom' @ dom) - [ Id name ] subst) + (match subst with + | None -> [Id name] + | Some subst -> + List.fold_left + (fun dom (_, term) -> + let dom' = aux loc context term in + dom' @ dom) + [Id name] subst)) | CicAst.Implicit -> [] | CicAst.Num (num, i) -> [ Num i ] | CicAst.Meta (index, local_context) -> @@ -391,13 +403,6 @@ module Make (C: Callbacks) = (function uri,_ -> MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri ) result in - HelmLogger.log (`Msg (`T "Locate query:")); - MQueryUtil.text_of_query - (fun s -> HelmLogger.log ~append_NL:false (`Msg (`T s))) - "" query; - HelmLogger.log (`Msg (`T "Result:")); - MQueryUtil.text_of_result - (fun s -> HelmLogger.log (`Msg (`T s))) "" result; let uris' = match uris with | [] -> @@ -484,7 +489,7 @@ module Make (C: Callbacks) = match todo_dom with | [] -> (match test_env current_env [] with - | Ok (term, metasenv) -> [ current_env, term, metasenv ] + | Ok (term, metasenv) -> [ current_env, metasenv, term ] | Ko | Uncertain -> []) | item :: remaining_dom -> debug_print (sprintf "CHOOSED ITEM: %s" @@ -500,7 +505,7 @@ module Make (C: Callbacks) = (match test_env new_env remaining_dom with | Ok (term, metasenv) -> (match remaining_dom with - | [] -> [ new_env, term, metasenv ] + | [] -> [ new_env, metasenv, term ] | _ -> aux new_env remaining_dom) @ filter tl | Uncertain -> (match remaining_dom with @@ -510,30 +515,27 @@ module Make (C: Callbacks) = in filter choices in - let (choosed_env, choosed_term, choosed_metasenv) = - match aux current_env todo_dom with - | [] -> raise NoWellTypedInterpretation - | [ x ] -> - debug_print "UNA SOLA SCELTA"; - x - | l -> - debug_print (sprintf "PIU' SCELTE (%d)" (List.length l)); - let choices = - List.map - (fun (env, _, _) -> - List.map - (fun domain_item -> - let description = - fst (Environment.find domain_item env) - in - (descr_of_domain_item domain_item, description)) - term_dom) - l - in - let choosed = C.interactive_interpretation_choice choices in - List.nth l choosed - in - (choosed_env, choosed_metasenv, choosed_term) + match aux current_env todo_dom with + | [] -> raise NoWellTypedInterpretation + | [ _ ] as l -> + debug_print "UNA SOLA SCELTA"; + l + | l -> + debug_print (sprintf "PIU' SCELTE (%d)" (List.length l)); + let choices = + List.map + (fun (env, _, _) -> + List.map + (fun domain_item -> + let description = + fst (Environment.find domain_item env) + in + (descr_of_domain_item domain_item, description)) + term_dom) + l + in + let choosed = C.interactive_interpretation_choice choices in + List.map (List.nth l) choosed end