/[mojave]/metaprl/theories/tactic/mptop.ml
ViewVC logotype

Annotation of /metaprl/theories/tactic/mptop.ml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2911 - (hide annotations) (download)
Thu Feb 24 01:42:53 2000 UTC (21 years, 5 months ago) by jyh
File size: 21399 byte(s)
Planning for update to .prla files.

1 jyh 2494 (*
2     * Define a resource to evaluate toplevel expressions.
3     *
4     * ----------------------------------------------------------------
5     *
6     * This file is part of MetaPRL, a modular, higher order
7     * logical framework that provides a logical programming
8     * environment for OCaml and other languages.
9     *
10     * See the file doc/index.html for information on Nuprl,
11     * OCaml, and more information about this system.
12     *
13     * Copyright (C) 1998 Jason Hickey, Cornell University
14 jyh 2525 *
15 jyh 2494 * This program is free software; you can redistribute it and/or
16     * modify it under the terms of the GNU General Public License
17     * as published by the Free Software Foundation; either version 2
18     * of the License, or (at your option) any later version.
19 jyh 2525 *
20 jyh 2494 * This program is distributed in the hope that it will be useful,
21     * but WITHOUT ANY WARRANTY; without even the implied warranty of
22     * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
23     * GNU General Public License for more details.
24 jyh 2525 *
25 jyh 2494 * You should have received a copy of the GNU General Public License
26     * along with this program; if not, write to the Free Software
27     * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
28 jyh 2525 *
29 jyh 2494 * Author: Jason Hickey
30     * jyh@cs.cornell.edu
31     *)
32    
33     open MLast
34    
35     open Refiner.Refiner.TermType
36 jyh 2911 open Refiner.Refiner.TermAddr
37 jyh 2494 open Refiner.Refiner.RefineError
38     open Mp_resource
39    
40 jyh 2743 open Tactic_type.Tacticals
41     open Tactic_type.Conversionals
42 jyh 2494
43     (************************************************************************
44     * TYPES *
45     ************************************************************************)
46    
47     (*
48     * These are the values that we recognize.
49     *)
50     type expr =
51     (* Base types *)
52     UnitExpr of unit
53     | BoolExpr of bool
54     | IntExpr of int
55     | StringExpr of string
56     | TermExpr of term
57     | TacticExpr of tactic
58     | ConvExpr of conv
59 jyh 2811 | AddressExpr of address
60 jyh 2494
61     (* Uptyped tuples and functions *)
62     | ListExpr of expr list
63     | TupleExpr of expr list
64     | FunExpr of (expr -> expr)
65    
66     (* Common cases are typed *)
67     | UnitFunExpr of (unit -> expr)
68     | BoolFunExpr of (bool -> expr)
69     | IntFunExpr of (int -> expr)
70     | StringFunExpr of (string -> expr)
71     | TermFunExpr of (term -> expr)
72     | TacticFunExpr of (tactic -> expr)
73     | IntTacticFunExpr of ((int -> tactic) -> expr)
74     | ConvFunExpr of (conv -> expr)
75 jyh 2811 | AddressFunExpr of (address -> expr)
76 jyh 2494
77     (* These functions take lists *)
78     | AddrFunExpr of (int list -> expr)
79     | StringListFunExpr of (string list -> expr)
80     | TermListFunExpr of (term list -> expr)
81     | TacticListFunExpr of (tactic list -> expr)
82     | ConvListFunExpr of (conv list -> expr)
83    
84     (*
85     * The resource maps strings to values.
86     *)
87     type top_data =
88     Empty
89     | Label of string * top_data
90     | Expr of string * expr * top_data
91     | Join of top_data * top_data
92    
93     type top_table =
94     (string, string * expr) Hashtbl.t
95    
96 jyh 2630 resource (string * expr, top_table, top_data, unit) toploop_resource
97 jyh 2494
98     (************************************************************************
99     * IMPLEMENTATION *
100     ************************************************************************)
101    
102     (*
103     * Construct a hash table of all the values.
104     * As in ML, the newer values override the previous.
105     *)
106     let collect_table data =
107     let hash = Hashtbl.create 201 in
108     let rec collect mod_name labels = function
109     Empty ->
110     labels
111     | (Label (mod_name, next)) as label ->
112     if List.memq label labels then
113     labels
114     else
115     collect mod_name (label :: labels) next
116     | Expr (name, expr, next) ->
117     let labels = collect mod_name labels next in
118     Hashtbl.add hash name (mod_name, expr);
119     labels
120    
121     | Join (next1, next2) ->
122     let labels = collect mod_name labels next1 in
123     collect mod_name labels next2
124     in
125 jyh 2577 let _ = collect "." [] data in
126 jyh 2494 hash
127    
128     (*
129     * Wrap up the joiner.
130     *)
131 jyh 2629 let join_resource base1 base2 =
132     Join (base1, base2)
133 jyh 2494
134 jyh 2629 let extract_resource data =
135 jyh 2494 collect_table data
136    
137 jyh 2629 let improve_resource data (name, expr) =
138     Expr (name, expr, data)
139 jyh 2494
140 jyh 2629 let close_resource data mod_name =
141     Label (String.capitalize mod_name, data)
142 jyh 2494
143     (************************************************************************
144     * COMPILING *
145     ************************************************************************)
146    
147     (*
148     * Right now most things are not supported.
149     *)
150     let not_supported loc str =
151 nogin 2502 Stdpp.raise_with_loc loc (RefineError ("mptop", StringStringError ("operation is not implemented", str)))
152 jyh 2494
153     let type_error loc str =
154     Stdpp.raise_with_loc loc (RefineError ("type error", StringError str))
155    
156     (*
157     * Convert a list to a term list.
158     *)
159     let some_list_of_list f loc = function
160     ListExpr l ->
161     List.map f l
162     | _ ->
163     type_error loc "expr should be a list"
164    
165     let term_expr loc = function
166     TermExpr t ->
167     t
168     | _ ->
169     type_error loc "expr should be a term"
170    
171     let int_expr loc = function
172     IntExpr t ->
173     t
174     | _ ->
175     type_error loc "expr should be an int"
176    
177     let string_expr loc = function
178     StringExpr t ->
179     t
180     | _ ->
181     type_error loc "expr should be a string"
182    
183     let tactic_expr loc = function
184     TacticExpr t ->
185     t
186     | _ ->
187     type_error loc "expr should be a tactic"
188    
189     let conv_expr loc = function
190     ConvExpr t ->
191     t
192     | _ ->
193     type_error loc "expr should be a conv"
194    
195     let term_list_of_list loc = some_list_of_list (term_expr loc) loc
196     let int_list_of_list loc = some_list_of_list (int_expr loc) loc
197     let string_list_of_list loc = some_list_of_list (string_expr loc) loc
198     let tactic_list_of_list loc = some_list_of_list (tactic_expr loc) loc
199     let conv_list_of_list loc = some_list_of_list (conv_expr loc) loc
200    
201     (*
202     * Want an int tactic.
203     *)
204     let int_tactic_expr loc = function
205     IntFunExpr f ->
206     (fun i ->
207     match f i with
208     TacticExpr tac ->
209     tac
210     | _ ->
211     type_error loc "int tactic expected")
212     | _ ->
213     type_error loc "int tactic expected"
214    
215     (*
216     * Lookup a variable from the table.
217     *)
218     let rec mk_var_expr base loc v =
219     try snd (Hashtbl.find base v) with
220     Not_found ->
221     Stdpp.raise_with_loc loc (RefineError ("mk_var_expr", StringStringError ("undefined variable", v)))
222    
223     and mk_proj_expr base loc expr =
224     let rec search modname v = function
225     (modname', expr) :: tl ->
226     if modname' = modname then
227     expr
228     else
229     search modname v tl
230     | [] ->
231     Stdpp.raise_with_loc loc (**)
232     (RefineError ("mk_proj_expr",
233     StringStringError ("undefined variable", modname ^ "." ^ v)))
234     in
235     let lookup names v =
236     match names with
237     [modname] ->
238     begin
239     try search modname v (Hashtbl.find_all base v) with
240     Not_found ->
241     Stdpp.raise_with_loc loc (**)
242     (RefineError ("mk_proj_expr",
243     StringStringError ("undefined variable", modname ^ "." ^ v)))
244     end
245     | _ ->
246     Stdpp.raise_with_loc loc (**)
247     (RefineError ("mk_proj_expr", StringError "nested modules are not implemented"))
248     in
249     let rec collect names expr =
250     match expr with
251     (<:expr< $uid: name$ . $e2$ >>) ->
252 nogin 2772 collect (name :: names) e2
253 jyh 2494 | (<:expr< $lid: v$ >>) ->
254     lookup names v
255     | _ ->
256     not_supported loc "expr projection"
257     in
258     collect [] expr
259    
260     (*
261     * For an application, we lookup the function and try to
262     * specialize the argument.
263     *)
264     and mk_apply_expr base loc f a =
265     let a = mk_expr base a in
266     match mk_expr base f with
267     FunExpr f ->
268     f a
269     | UnitFunExpr f ->
270     begin
271     match a with
272     UnitExpr () ->
273     f ()
274     | _ ->
275     type_error loc "expr should be unit"
276     end
277     | BoolFunExpr f ->
278     begin
279     match a with
280     BoolExpr a ->
281     f a
282     | _ ->
283     type_error loc "expr should be a bool"
284     end
285     | IntFunExpr f ->
286     begin
287     match a with
288     IntExpr a ->
289     f a
290     | _ ->
291     type_error loc "expr should be int"
292     end
293     | StringFunExpr f ->
294     begin
295     match a with
296     StringExpr a ->
297     f a
298     | _ ->
299     type_error loc "expr should be a string"
300     end
301     | TermFunExpr f ->
302     begin
303     match a with
304     TermExpr a ->
305     f a
306     | _ ->
307     type_error loc "expr should be a term"
308     end
309     | TacticFunExpr f ->
310     begin
311     match a with
312     TacticExpr a ->
313     f a
314     | _ ->
315     type_error loc "expr should be a tactic"
316     end
317     | IntTacticFunExpr f ->
318     f (int_tactic_expr loc a)
319     | ConvFunExpr f ->
320     begin
321     match a with
322     ConvExpr a ->
323     f a
324     | _ ->
325     type_error loc "expr should be a conversion"
326     end
327 jyh 2811 | AddressFunExpr f ->
328     begin
329     match a with
330     AddressExpr a ->
331     f a
332     | _ ->
333 jyh 2911 f (make_address (int_list_of_list loc a))
334 jyh 2811 end
335 jyh 2494
336     | AddrFunExpr f ->
337     f (int_list_of_list loc a)
338     | StringListFunExpr f ->
339     f (string_list_of_list loc a)
340     | TermListFunExpr f ->
341     f (term_list_of_list loc a)
342     | TacticListFunExpr f ->
343     f (tactic_list_of_list loc a)
344     | ConvListFunExpr f ->
345     f (conv_list_of_list loc a)
346     | UnitExpr _
347     | BoolExpr _
348     | IntExpr _
349     | StringExpr _
350     | TermExpr _
351     | TacticExpr _
352     | ConvExpr _
353 jyh 2811 | AddressExpr _
354 jyh 2494 | ListExpr _
355     | TupleExpr _ ->
356     type_error loc "expr should be a function"
357    
358     (*
359     * A tuple of expressions.
360     * We only support unit for now.
361     *)
362     and mk_tuple_expr base loc = function
363     [] ->
364     UnitExpr ()
365     | _ ->
366     not_supported loc "tuple expression"
367    
368     and mk_expr base expr =
369     let loc = loc_of_expr expr in
370     match expr with
371     (<:expr< $e1$ . $e2$ >> as expr) ->
372     mk_proj_expr base loc expr
373     | (<:expr< $e1$ $e2$ >>) ->
374     mk_apply_expr base loc e1 e2
375     | (<:expr< $e1$ .( $e2$ ) >>) ->
376     not_supported loc "array subscript"
377     | (<:expr< [| $list:el$ |] >>) ->
378     not_supported loc "array"
379     | (<:expr< $e1$ := $e2$ >>) ->
380     not_supported loc "assignment"
381     | (<:expr< $chr:c$ >>) ->
382     not_supported loc "char"
383     (*
384     | (<:expr< ( $e$ :> $t$ ) >>) ->
385     *)
386     | MLast.ExCoe (_, e, t) ->
387     not_supported loc "class coercion"
388     | (<:expr< $flo:s$ >>) ->
389     not_supported loc "float"
390     | (<:expr< for $s$ = $e1$ $to:b$ $e2$ do $list:el$ done >>) ->
391     not_supported loc "for loop"
392     | (<:expr< fun [ $list:pwel$ ] >>) ->
393     not_supported loc "fun"
394     | (<:expr< if $e1$ then $e2$ else $e3$ >>) ->
395     not_supported loc "ifthenelse"
396     | (<:expr< $int:s$ >>) ->
397     IntExpr (int_of_string s)
398     | (<:expr< let $rec:b$ $list:pel$ in $e$ >>) ->
399     not_supported loc "let"
400     | (<:expr< $lid:s$ >>) ->
401     mk_var_expr base loc s
402     | MLast.ExLmd _ ->
403     not_supported loc "local module"
404     | (<:expr< match $e$ with [ $list:pwel$ ] >>) ->
405     not_supported loc "match"
406     (*
407     | (<:expr< new $e$ >>) ->
408     *)
409     | MLast.ExNew _ ->
410     not_supported loc "new"
411     (*
412     | (<:expr< {< $list:sel$ >} >>) ->
413     *)
414     | MLast.ExOvr _ ->
415     not_supported loc "stream"
416     (*
417     | (<:expr< { $list:eel$ } >>) ->
418     *)
419     | MLast.ExRec _ ->
420     not_supported loc "record"
421     | (<:expr< do $list:el$ return $e$ >>) ->
422     not_supported loc "do"
423     (*
424     | (<:expr< $e$ # $i$ >>) ->
425     *)
426     | MLast.ExSnd _ ->
427     not_supported loc "class projection"
428     | (<:expr< $e1$ .[ $e2$ ] >>) ->
429     not_supported loc "string subscript"
430     | (<:expr< $str:s$ >>) ->
431     StringExpr s
432     | (<:expr< try $e$ with [ $list:pwel$ ] >>) ->
433     not_supported loc "try"
434     | (<:expr< ( $list:el$ ) >>) ->
435     mk_tuple_expr base loc el
436     | (<:expr< ( $e$ : $t$ ) >>) ->
437     mk_expr base e
438     | (<:expr< $uid:s$ >>) ->
439 jyh 2525 mk_var_expr base loc s
440 jyh 2494 | (<:expr< while $e$ do $list:el$ done >>) ->
441     not_supported loc "while"
442     | MLast.ExAnt (_, e) ->
443     not_supported loc "ExAnt"
444 jyh 2629 | MLast.ExXnd (_, _, e) ->
445     mk_expr base e
446 jyh 2494
447     and mk_patt base patt =
448     let loc = loc_of_patt patt in
449     match patt with
450     (<:patt< $p1$ . $p2$ >>) ->
451     not_supported loc "patt projection"
452     | (<:patt< ( $p1$ as $p2$ ) >>) ->
453     not_supported loc "patt"
454     | (<:patt< _ >>) ->
455     not_supported loc "wild pattern"
456     | (<:patt< $p1$ $p2$ >>) ->
457     not_supported loc "pattern application"
458     | (<:patt< [| $list: pl$ |] >>) ->
459     not_supported loc "array patterns"
460     | (<:patt< $chr:c$ >>) ->
461     not_supported loc "pattern char"
462     | (<:patt< $int:s$ >>) ->
463     not_supported loc "pattern int"
464     | (<:patt< $lid:v$ >>) ->
465     not_supported loc "pattern var"
466     | (<:patt< $p1$ | $p2$ >>) ->
467     not_supported loc "pattern choice"
468     | (<:patt< $p1$ .. $p2$ >>) ->
469     not_supported loc "pattern range"
470     | (<:patt< { $list:ppl$ } >>) ->
471     not_supported loc "pattern list"
472     | (<:patt< $str:s$ >>) ->
473     not_supported loc "pattern string"
474     | (<:patt< ( $list:pl$ ) >>) ->
475     not_supported loc "pattern list"
476     | (<:patt< ( $p$ : $t'$ ) >>) ->
477     not_supported loc "pattern cast"
478     | (<:patt< $uid:s$ >>) ->
479     not_supported loc "pattern uid"
480     | MLast.PaAnt (_, p) ->
481     not_supported loc "pattern PaAnt"
482 jyh 2629 | MLast.PaXnd _ ->
483     not_supported loc "patterm PaXnd"
484 jyh 2494
485     and mk_type base t =
486     let loc = loc_of_ctyp t in
487     match t with
488     (<:ctyp< $t1$ . $t2$ >>) ->
489     not_supported loc "type projection"
490     | (<:ctyp< $t1$ as $t2$ >>) ->
491     not_supported loc "type"
492     | (<:ctyp< _ >>) ->
493     not_supported loc "type wildcard"
494     | (<:ctyp< $t1$ $t2$ >>) ->
495     not_supported loc "type application"
496     | (<:ctyp< $t1$ -> $t2$ >>) ->
497     not_supported loc "type function"
498     (*
499     | (<:ctyp< # $i$ >>) ->
500     *)
501     | MLast.TyCls _ ->
502     not_supported loc "type method"
503     | (<:ctyp< $lid:s$ >>) ->
504     not_supported loc "type var"
505     | (<:ctyp< '$s$ >>) ->
506     not_supported loc "type param"
507     | (<:ctyp< $t1$ == $t2$ >>) ->
508     not_supported loc "type equality"
509 jyh 2577 (*
510 jyh 2494 | (<:ctyp< < $list:stl$ $dd:b$ > >>) ->
511 jyh 2577 *)
512     | MLast.TyObj (loc, _, _) ->
513 jyh 2494 not_supported loc "type class"
514     | (<:ctyp< { $list:sbtl$ } >>) ->
515     not_supported loc "type record"
516     | (<:ctyp< [ $list:stll$ ] >>) ->
517     not_supported loc "type list"
518     | (<:ctyp< ( $list:tl$ ) >>) ->
519     not_supported loc "type product"
520     | (<:ctyp< $uid:s$ >>) ->
521     not_supported loc "type constructor var"
522 jyh 2629 | MLast.TyXnd (_, _, t) ->
523     mk_type base t
524 jyh 2494
525     and mk_sig_item base si =
526     let loc = loc_of_sig_item si in
527     match si with
528     (*
529     (<:sig_item< class $list:ctl$ >>) ->
530     *)
531     MLast.SgCls _
532     | MLast.SgClt _ ->
533     not_supported loc "sig class"
534     | (<:sig_item< declare $list:sil$ end >>) ->
535     mk_sig_item base (List_util.last sil)
536     | (<:sig_item< exception $s$ of $list:tl$ >>) ->
537     not_supported loc "sig exception"
538     | (<:sig_item< external $s$ : $t$ = $list:sl$ >>) ->
539     not_supported loc "sig external"
540     | SgInc (_, mt) ->
541     not_supported loc "sig SgInc"
542     | (<:sig_item< module $s$ : $mt$ >>) ->
543     not_supported loc "sig module"
544     | (<:sig_item< module type $s$ = $mt$ >>) ->
545     not_supported loc "sig module type"
546     | (<:sig_item< open $sl$ >>) ->
547     not_supported loc "sig open"
548 nogin 2859 | (<:sig_item< type $list:tdl$ >>) ->
549 jyh 2494 not_supported loc "sig type"
550     | (<:sig_item< value $s$ : $t$ >>) ->
551     not_supported loc "sig value"
552    
553     and mk_str_item base si =
554     let loc = loc_of_str_item si in
555     match si with
556     (*
557     (<:str_item< class $list:cdl$ >>) ->
558     *)
559     MLast.StCls _
560     | MLast.StClt _ ->
561     not_supported loc "str class"
562     | (<:str_item< declare $list:stl$ end >>) ->
563     mk_str_item base (List_util.last stl)
564     | (<:str_item< exception $s$ of $list:tl$ >>) ->
565     not_supported loc "str exception"
566     | (<:str_item< $exp:e$ >>) ->
567     mk_expr base e
568     | (<:str_item< external $s$ : $t$ = $list:sl$ >>) ->
569     not_supported loc "str external"
570     | (<:str_item< module $s$ = $me$ >>) ->
571     not_supported loc "str module"
572     | (<:str_item< module type $s$ = $mt$ >>) ->
573     not_supported loc "str module type"
574     | (<:str_item< open $sl$ >>) ->
575     not_supported loc "str module open"
576 nogin 2859 | (<:str_item< type $list:tdl$ >>) ->
577 jyh 2494 not_supported loc "str type"
578     | (<:str_item< value $rec:b$ $list:pel$ >>) ->
579     not_supported loc "str let"
580    
581     and mk_module_type base mt =
582     let loc = loc_of_module_type mt in
583     match mt with
584     (<:module_type< $mt1$ . $mt2$ >>) ->
585     not_supported loc "module type projection"
586     | (<:module_type< $mt1$ $mt2$ >>) ->
587     not_supported loc "module type application"
588     | (<:module_type< functor ( $s$ : $mt1$ ) -> $mt2$ >>) ->
589     not_supported loc "module type functor"
590     | (<:module_type< $lid:i$ >>) ->
591     not_supported loc "module type var"
592     | (<:module_type< sig $list:sil$ end >>) ->
593     not_supported loc "module type sig"
594     | (<:module_type< $uid:i$ >>) ->
595     not_supported loc "module type var"
596     | (<:module_type< $mt$ with $list:wcl$ >>) ->
597     not_supported loc "module type constraint"
598    
599     and mk_wc base = function
600     WcTyp (loc, sl1, sl2, t) ->
601     not_supported loc "with clause type"
602     | WcMod (loc, sl1, mt) ->
603     not_supported loc "with clause module"
604    
605     and mk_module_expr base me =
606     let loc = loc_of_module_expr me in
607     match me with
608     (<:module_expr< $me1$ . $me2$ >>) ->
609     not_supported loc "module expr projection"
610     | (<:module_expr< $me1$ $me2$ >>) ->
611     not_supported loc "module expr application"
612     | (<:module_expr< functor ( $s$ : $mt$ ) -> $me$ >>) ->
613     not_supported loc "module expr functor"
614     | (<:module_expr< struct $list:sil$ end >>) ->
615     not_supported loc "module expr struct"
616     | (<:module_expr< ( $me$ : $mt$) >>) ->
617     not_supported loc "module expr type"
618     | (<:module_expr< $uid:i$ >>) ->
619     not_supported loc "module expr id"
620    
621     (************************************************************************
622     * RESOURCES *
623     ************************************************************************)
624    
625     (*
626     * Include the common library functions.
627     *)
628     let int_int_fun_int_expr f =
629     IntFunExpr (fun i -> IntFunExpr (fun j -> IntExpr (f i j)))
630    
631 jyh 2525 let cons_expr =
632     FunExpr (fun e1 ->
633     FunExpr (fun e2 ->
634     match e2 with
635     ListExpr e2 ->
636     ListExpr (e1 :: e2)
637     | _ ->
638     raise (RefineError ("cons_expr", StringError "type mismatch"))))
639    
640 jyh 2494 let values =
641     ["+", int_int_fun_int_expr ( + );
642     "-", int_int_fun_int_expr ( - );
643     "*", int_int_fun_int_expr ( * );
644 jyh 2525 "/", int_int_fun_int_expr ( / );
645     "::", cons_expr;
646     "()", UnitExpr ();
647     "[]", ListExpr [];
648 jyh 2549 "True", BoolExpr true;
649     "False", BoolExpr false]
650 jyh 2494
651 jyh 2525
652 jyh 2494 let rec add_resources base = function
653     (name, expr) :: tl ->
654     add_resources (Expr (name, expr, base)) tl
655     | [] ->
656     base
657    
658     let toploop_resource =
659 jyh 2629 Mp_resource.create (**)
660     { resource_join = join_resource;
661     resource_extract = extract_resource;
662     resource_improve = improve_resource;
663 jyh 2630 resource_improve_arg = Mp_resource.improve_arg_fail "toploop_resource";
664 jyh 2629 resource_close = close_resource
665     }
666     (add_resources Empty values)
667 jyh 2494
668 jyh 2629 let get_resource modname =
669     Mp_resource.find toploop_resource modname
670 jyh 2494
671     let expr_of_ocaml_expr = mk_expr
672     let expr_of_ocaml_str_item = mk_str_item
673    
674     (*
675     * -*-
676     * Local Variables:
677     * Caml-master: "refiner"
678     * End:
679     * -*-
680     *)

Properties

Name Value
svn:eol-style native
svn:keywords Author Date Id Revision

  ViewVC Help
Powered by ViewVC 1.1.26