8 val empty : Proof.context |
8 val empty : Proof.context |
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 initialise : Proof.context -> term list -> Proof.context |
14 val initialise : Proof.context -> term list -> Proof.context |
14 val initialise' : theory -> TermC.as_string list -> Proof.context |
15 val initialise' : theory -> TermC.as_string list -> Proof.context |
15 val get_assumptions : Proof.context -> term list |
16 val get_assumptions : Proof.context -> term list |
16 val insert_assumptions : term list -> Proof.context -> Proof.context |
17 val insert_assumptions : term list -> Proof.context -> Proof.context |
17 val avoid_contradict: term -> term list -> term * term list |
18 val avoid_contradict: term -> term list -> term * term list |
35 |
36 |
36 val declare_constraints = Variable.declare_constraints |
37 val declare_constraints = Variable.declare_constraints |
37 fun add_constraints ts ctxt = |
38 fun add_constraints ts ctxt = |
38 fold Variable.declare_constraints (TermC.vars' ts) ctxt |
39 fold Variable.declare_constraints (TermC.vars' ts) ctxt |
39 |
40 |
|
41 fun build_while_parsing_ [] (ts, ctxt) = (ts, ctxt) |
|
42 | build_while_parsing_ (str :: strs) (ts, ctxt) = |
|
43 let |
|
44 val t as (_ $ tm) = Syntax.read_term ctxt str |
|
45 handle ERROR msg => raise ERROR ("ContextC.build_while_parsing " ^ quote str ^ " " ^ msg) |
|
46 val vars = TermC.vars tm |
|
47 val ctxt' = add_constraints vars ctxt |
|
48 in build_while_parsing_ strs (ts @ [t], ctxt') end |
|
49 (* shouldn't that be done by fold ? |
|
50 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) |
|
52 |
40 (* in Subproblem take respective actual arguments from program *) |
53 (* in Subproblem take respective actual arguments from program *) |
|
54 (* FIXME: should be replaced by build_while_parsing *) |
41 fun initialise ctxt ts = |
55 fun initialise ctxt ts = |
42 let |
56 let |
43 val frees = TermC.vars' ts |
57 val frees = TermC.vars' ts |
44 val _ = TermC.raise_type_conflicts frees |
58 val _ = TermC.raise_type_conflicts frees |
45 in |
59 in |