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 ->
+ (try
+ match cic with
+ | Cic.Const (uri, []) ->
+ let uris =
+ (*match CicEnvironment.get_obj uri with*)
+ match CicTypeChecker.typecheck 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*)
+ match CicTypeChecker.typecheck 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*)
+ match CicTypeChecker.typecheck 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*)
+ match CicTypeChecker.typecheck 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)));
+ 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))
+ t
+ | _ ->
+ raise DisambiguateChoices.Invalid_choice
+ with
+ CicEnvironment.CircularDependency _ ->
+ raise DisambiguateChoices.Invalid_choice))
| CicAst.Implicit -> Cic.Implicit None
| CicAst.Num (num, i) -> resolve env (Num i) ~num ()
| CicAst.Meta (index, subst) ->
in
(* (3) test an interpretation filling with meta uninterpreted identifiers
*)
- let test_env current_env todo_dom =
+ let test_env current_env todo_dom univ =
let filled_env =
List.fold_left
(fun env item ->
current_env todo_dom
in
try
+ CicUniv.set_working univ;
let cic_term =
interpretate ~context:disambiguate_context ~env:filled_env term
in
- refine metasenv context cic_term
+ let k = refine metasenv context cic_term in
+ let new_univ = CicUniv.get_working () in
+ (k , new_univ )
with
- | Try_again -> Uncertain
- | DisambiguateChoices.Invalid_choice -> Ko
+ | Try_again -> Uncertain,univ
+ | DisambiguateChoices.Invalid_choice -> Ko,univ
in
(* (4) build all possible interpretations *)
- let rec aux current_env todo_dom =
+ let rec aux current_env todo_dom base_univ =
match todo_dom with
| [] ->
- (match test_env current_env [] with
- | Ok (term, metasenv) -> [ current_env, metasenv, term ]
- | Ko | Uncertain -> [])
+ (match test_env current_env [] base_univ with
+ | Ok (term, metasenv),new_univ ->
+ [ current_env, metasenv, term, new_univ ]
+ | Ko,_ | Uncertain,_ -> [])
| item :: remaining_dom ->
debug_print (sprintf "CHOOSED ITEM: %s"
- (string_of_domain_item item));
+ (string_of_domain_item item));
let choices = lookup_choices item in
- let rec filter = function
+ let rec filter univ = function
| [] -> []
| codomain_item :: tl ->
debug_print (sprintf "%s CHOSEN" (fst codomain_item)) ;
let new_env =
Environment.add item codomain_item current_env
in
- (match test_env new_env remaining_dom with
- | Ok (term, metasenv) ->
+ (match test_env new_env remaining_dom univ with
+ | Ok (term, metasenv),new_univ ->
(match remaining_dom with
- | [] -> [ new_env, metasenv, term ]
- | _ -> aux new_env remaining_dom) @ filter tl
- | Uncertain ->
+ | [] -> [ new_env, metasenv, term, new_univ ]
+ | _ -> aux new_env remaining_dom new_univ )@
+ filter univ tl
+ | Uncertain,new_univ ->
(match remaining_dom with
| [] -> []
- | _ -> aux new_env remaining_dom) @ filter tl
- | Ko -> filter tl)
+ | _ -> aux new_env remaining_dom new_univ )@
+ filter univ tl
+ | Ko,_ -> filter univ tl)
in
- filter choices
+ filter base_univ choices
in
- match aux current_env todo_dom with
+ let base_univ = CicUniv.get_working () in
+ try
+ match aux current_env todo_dom base_univ with
| [] -> raise NoWellTypedInterpretation
- | [ _ ] as l ->
+ | [ e,me,t,u ] as l ->
debug_print "UNA SOLA SCELTA";
- l
+ CicUniv.set_working u;
+ [ e,me,t ]
| l ->
debug_print (sprintf "PIU' SCELTE (%d)" (List.length l));
let choices =
List.map
- (fun (env, _, _) ->
+ (fun (env, _, _, _) ->
List.map
(fun domain_item ->
let description =
l
in
let choosed = C.interactive_interpretation_choice choices in
- List.map (List.nth l) choosed
-
+ let l' = List.map (List.nth l) choosed in
+ match l' with
+ [] -> assert false
+ | [e,me,t,u] ->
+ CicUniv.set_working u;
+ (*CicUniv.print_working_graph ();*)
+ [e,me,t]
+ | hd::tl -> (* ok, testlibrary... cosi' stampa MANY... bah *)
+ List.map (fun (e,me,t,u) -> (e,me,t)) l'
+ with
+ CicEnvironment.CircularDependency s ->
+ raise (Failure "e chi la becca sta CircularDependency?");
end
projects / helm.git / blobdiff