| 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 =
let cic_body = do_branch' (name :: context) tl in
let typ =
match typ with
- | None -> Cic.Implicit
+ | None -> Cic.Implicit (Some `Type)
| Some typ -> aux loc context typ
in
Cic.Lambda (name, typ, cic_body)
do_branch' context args
in
let (indtype_uri, indtype_no) =
- match resolve env (Id indty_ident) () with
- | Cic.MutInd (uri, tyno, _) -> uri, tyno
- | Cic.Implicit -> raise Try_again
- | _ -> raise DisambiguateChoices.Invalid_choice
+ 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
+ | _ -> raise DisambiguateChoices.Invalid_choice)
+ | None ->
+ let fst_constructor =
+ match branches with
+ | ((head, _), _) :: _ -> head
+ | [] -> raise DisambiguateChoices.Invalid_choice
+ in
+ (match resolve env (Id fst_constructor) () with
+ | Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
+ (indtype_uri, indtype_no)
+ | Cic.Implicit _ -> raise Try_again
+ | _ -> raise DisambiguateChoices.Invalid_choice)
in
Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
(List.map do_branch branches))
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
- with Not_found -> resolve env (Id name) ())
- | CicAst.Implicit -> Cic.Implicit
+ with Not_found ->
+ let cic = 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 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, []) ->
+ let uris =
+ match CicEnvironment.get_obj uri with
+ | Cic.Constant (_, _, _, uris) -> uris
+ | _ -> assert false
+ in
+ Cic.Const (uri, mk_subst uris)
+ | Cic.Var (uri, []) ->
+ let uris =
+ match CicEnvironment.get_obj uri with
+ | Cic.Variable (_, _, _, uris) -> uris
+ | _ -> assert false
+ in
+ Cic.Var (uri, mk_subst uris)
+ | Cic.MutInd (uri, i, []) ->
+ let uris =
+ match CicEnvironment.get_obj uri with
+ | Cic.InductiveDefinition (_, uris, _) -> uris
+ | _ -> assert false
+ in
+ Cic.MutInd (uri, i, mk_subst uris)
+ | Cic.MutConstruct (uri, i, j, []) ->
+ let uris =
+ match CicEnvironment.get_obj uri with
+ | Cic.InductiveDefinition (_, uris, _) -> uris
+ | _ -> assert false
+ in
+ Cic.MutConstruct (uri, i, j, mk_subst uris)
+ | Cic.Meta _ | Cic.Implicit _ as t ->
+(*
+ prerr_endline (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 ^ " := " ^ CicAstPp.pp_term term)
+ subst)));
+*)
+ t
+ | _ ->
+ raise DisambiguateChoices.Invalid_choice))
+ | CicAst.Implicit -> Cic.Implicit None
| CicAst.Num (num, i) -> resolve env (Num i) ~num ()
| CicAst.Meta (index, subst) ->
let cic_subst =
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)) ()
and aux_option loc context = function
- | None -> Cic.Implicit
+ | None -> Cic.Implicit (Some `Type)
| Some term -> aux loc context term
in
match ast with
| 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
let branches_dom =
List.fold_left (fun dom branch -> do_branch branch @ dom) [] branches
in
- branches_dom @ outtype_dom @ term_dom @ [ Id indty_ident ]
+ branches_dom @ outtype_dom @ term_dom @
+ (match indty_ident with None -> [] | Some ident -> [ Id ident ])
| CicAst.LetIn ((var, typ), body, where) ->
let body_dom = aux loc context body in
let type_dom = aux_option loc context typ in
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";
- []
- with Not_found -> [ Id name ])
+ "Explicit substitutions not allowed here"
+ else
+ []
+ with Not_found ->
+ (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) ->
(function uri,_ ->
MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
) result in
- C.output_html (`Msg (`T "Locate query:"));
- MQueryUtil.text_of_query
- (fun s -> C.output_html ~append_NL:false (`Msg (`T s)))
- "" query;
- C.output_html (`Msg (`T "Result:"));
- MQueryUtil.text_of_result
- (fun s -> C.output_html (`Msg (`T s))) "" result;
let uris' =
match uris with
| [] ->
[UriManager.string_of_uri (C.input_or_locate_uri
- ~title:("URI matching \"" ^ id ^ "\" unknown."))]
+ ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())]
| [uri] -> [uri]
| _ ->
C.interactive_user_uri_choice ~selection_mode:`MULTIPLE
let filled_env =
List.fold_left
(fun env item ->
- Environment.add item ("Implicit", fun _ _ _ -> Cic.Implicit) env)
+ Environment.add item
+ ("Implicit",
+ (match item with
+ | Id _ | Num _ -> (fun _ _ _ -> Cic.Implicit (Some `Closed))
+ | Symbol _ -> (fun _ _ _ -> Cic.Implicit None))) env)
current_env todo_dom
in
try
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"
(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
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
projects / helm.git / blobdiff