equal
deleted
inserted
replaced
9 val is_empty : Proof.context -> bool |
9 val is_empty : Proof.context -> bool |
10 val isac_ctxt : 'a -> Proof.context |
10 val isac_ctxt : 'a -> Proof.context |
11 val declare_constraints: term -> Proof.context -> Proof.context |
11 val declare_constraints: term -> Proof.context -> Proof.context |
12 val add_constraints: term list -> Proof.context -> Proof.context |
12 val add_constraints: term list -> Proof.context -> Proof.context |
13 val build_while_parsing: Formalise.model -> theory -> term list * Proof.context |
13 val build_while_parsing: Formalise.model -> theory -> term list * Proof.context |
14 val initialise : Proof.context -> term list -> Proof.context |
14 val init_for_prog: Proof.context -> term list -> Proof.context |
15 val initialise' : theory -> TermC.as_string list -> Proof.context |
|
16 val get_assumptions : Proof.context -> term list |
15 val get_assumptions : Proof.context -> term list |
17 val insert_assumptions : term list -> Proof.context -> Proof.context |
16 val insert_assumptions : term list -> Proof.context -> Proof.context |
18 val avoid_contradict: term -> term list -> term * term list |
17 val avoid_contradict: term -> term list -> term * term list |
19 val subpbl_to_caller : Proof.context -> term -> Proof.context -> term * Proof.context |
18 val subpbl_to_caller : Proof.context -> term -> Proof.context -> term * Proof.context |
20 |
19 |
49 (* shouldn't that be done by fold ? |
48 (* shouldn't that be done by fold ? |
50 fn: string * Proof.context -> term list * Proof.context -> term list * Proof.context *) |
49 fn: string * Proof.context -> term list * Proof.context -> term list * Proof.context *) |
51 fun build_while_parsing strs thy = build_while_parsing_ strs ([], Proof_Context.init_global thy) |
50 fun build_while_parsing strs thy = build_while_parsing_ strs ([], Proof_Context.init_global thy) |
52 |
51 |
53 (* in Subproblem take respective actual arguments from program *) |
52 (* in Subproblem take respective actual arguments from program *) |
54 (* FIXME: should be replaced by build_while_parsing *) |
53 fun init_for_prog ctxt ts = |
55 fun initialise ctxt ts = |
|
56 let |
54 let |
57 val frees = TermC.vars' ts |
55 val frees = TermC.vars' ts |
58 val _ = TermC.raise_type_conflicts frees |
|
59 in |
|
60 fold Variable.declare_constraints frees ctxt |
|
61 end |
|
62 (* in root-problem take respective formalisation *) |
|
63 fun initialise' thy fmz = |
|
64 let |
|
65 val ctxt = thy |> Proof_Context.init_global |
|
66 val frees = map (TermC.parseNEW' ctxt) fmz |> TermC.vars' |
|
67 val _ = TermC.raise_type_conflicts frees |
56 val _ = TermC.raise_type_conflicts frees |
68 in |
57 in |
69 fold Variable.declare_constraints frees ctxt |
58 fold Variable.declare_constraints frees ctxt |
70 end |
59 end |
71 |
60 |