pofiles

create_element_environment([],_,Env,Env).

create_element_environment([Elem|ERest],Type,In,Out) :-
    env_store(Elem,Type,[enumerated_set_element],In,Inter),
    create_element_environment(ERest,Type,Inter,Out).

create_enum_environment(Enumerations,InitEnv) :-
    env_empty(Start),
    create_enum_environment2(Enumerations,Start,InitEnv).

create_enum_environment2([],InitEnv,InitEnv).

create_enum_environment2([set(Name,Elements)|Rest],In,Out) :-
    env_store(Name,set(global(Name)),[given_set],In,Inter1),
    create_element_environment(Elements,global(Name),Inter1,Inter2),
    create_enum_environment2(Rest,Inter2,Out).

extract_predicate_component(text(_)) --> [].

extract_predicate_component(predicate(P)) --> [P].

extract_predicate_components([]) --> [].

extract_predicate_components([Component|CRest]) -->
    extract_predicate_component(Component),
    extract_predicate_components(CRest).

load_popl_file(Filename,TypedProofs) :-
    reset_pofile,
    load_popl_terms(Filename,Proofs,Formulas,Enumerations),
    typecheck_proofs(Proofs,Formulas,Enumerations,TypedProofs).

load_popl_terms(Filename,Proofs,Formulas,Enumerations) :-
    % TODO: more robustness
    open(Filename,read,S),
    read(S,Term),
    close(S),
    Term = po_file(Proofs,Formulas,Enumerations,_Version).

reset_pofile.

typecheck_proof(proof(Id,Global,Local,Goals),Env,proof(Id,DefSets,Identifiers,TPrecondition,TGoal)) :-
    same_length(Global,TGlobal),
    same_length(Local,TLocal),
    same_length(Goals,TGoals),
    append([Global,Local,Goals],Untyped),
    append([TGlobal,TLocal,TGoals],Typed),
    opentype(Untyped,Env,Identifiers,DefSets,Typed),
    append(TGlobal,TLocal,TPreconditions),
    conjunct_predicates(TPreconditions,TPrecondition),
    conjunct_predicates(TGoals,TGoal).

typecheck_proofs(Proofs,Formulas,Enumerations,TypedProofs) :-
    create_enum_environment(Enumerations,InitEnv),
    unfold_proofs(Proofs,Formulas,FullProofs),
    typecheck_proofs2(FullProofs,InitEnv,TypedProofs).

typecheck_proofs2([],_,[]).

typecheck_proofs2([P|PRest],Env,[TP|TPRest]) :-
    typecheck_proof(P,Env,TP),
    typecheck_proofs2(PRest,Env,TPRest).

unfold_proof(proof(Id,GlobalHyp,LocalHyp,Goal),Formulas,proof(Id,UGH,ULH,UGoal)) :-
    unfold_references(GlobalHyp,Formulas,UGH),
    unfold_references(LocalHyp,Formulas,ULH),
    unfold_reference(Goal,Formulas,UGoal,[]).

unfold_proofs([],_,[]).

unfold_proofs([P|PRest],Formulas,[U|URest]) :-
    unfold_proof(P,Formulas,U),
    unfold_proofs(PRest,Formulas,URest).

unfold_reference(formula_ref(N),Formulas) -->
    {nth1(N,Formulas,formula(Components))},
    extract_predicate_components(Components).

unfold_references(References,Formulas,Components) :-
    unfold_references2(References,Formulas,Components,[]).

unfold_references2([],_) --> [].

unfold_references2([Ref|RRest],Formulas) -->
    unfold_reference(Ref,Formulas),
    unfold_references2(RRest,Formulas).