package acgtk

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file lambda.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
(**************************************************************************)
(*                                                                        *)
(*                 ACG development toolkit                                *)
(*                                                                        *)
(*                  Copyright 2008-2021 INRIA                             *)
(*                                                                        *)
(*  More information on "http://acg.gforge.inria.fr/"                     *)
(*  License: CeCILL, see the LICENSE file or "http://www.cecill.info"     *)
(*  Authors: see the AUTHORS file                                         *)
(*                                                                        *)
(*                                                                        *)
(*                                                                        *)
(*                                                                        *)
(*  $Rev::                              $:  Revision of last commit       *)
(*  $Author::                           $:  Author of last commit         *)
(*  $Date::                             $:  Date of last commit           *)
(*                                                                        *)
(**************************************************************************)

open UtilsLib
open Abstract_syntax
module Lambda = 

  struct

    exception Not_yet_implemented
    

    type kind = 
      Type 
    | Depend of stype * kind  (* the kind of a dependant type *)


    and  stype =
      Atom of int                       (* atomic type *)
    | DAtom of int                      (* defined atomic type *)
    | LFun of stype * stype             (* linear functional type *)
    | Fun of stype * stype              (* non linear functional type *)
    | Dprod of string * stype * stype   (* dependant product *)
    | Record of int * stype list        (* records *)
    | Variant of int * stype list       (* variants *) 
    | TAbs of string * stype            (* type abstraction *)
    | TApp of stype * term              (* type application *)

    
    and  term =
      Var of int                (* lambda variable *)
    | LVar of int               (* linear lambda variable *)
    | Const of int              (* constant *)
    | DConst of int             (* defined constant *)
    | Abs of string * term      (* lambda-abstraction *)
    | LAbs of string * term     (* linear lambda abstraction *)
    | App of term * term        (* application *)
    | Rcons of int * term list  (* record constructor:         *)
                                (* - the integer is the tag of *)
                                (*   the corresponding type.   *)
    | Proj of int * int *term   (* projection:                        *)
                                (* - the first integer is the tag of  *)
                                (*   the corresponding type;          *)
                                (* - the second integer is the index  *)
                                (*   of the projection.               *)
    | Vcons of int * int * term (* variant constructor:               *)
                                (* - the first integer is the tag of  *)
                                (*   the corresponding type;          *)
                                (* - the second integer is the number *)
                                (*   of the constructor.              *)
    | Case of int * term * (string * term) list
                                (* case analysis:              *)      
                                (* - the integer is the tag of *)
                                (*   the corresponding type.   *)
    | Unknown of int            (* meta-variable - used in higher-order  *)
                                (* matching                              *) 

    type env = (int * string) list

    type consts = int -> Abstract_syntax.syntactic_behavior * string

    let env_to_string e =
      Utils.string_of_list ", " (fun (i,s) -> Printf.sprintf "%d:%s" i s) e
                                                                
    let rec generate_var_name x (l_env, env) =
      if List.exists (fun (_,s) -> x=s) (l_env @ env) then
	generate_var_name (Printf.sprintf "%s'" x) (l_env, env)
      else
	x


     let rec unfold_labs acc level (l_env, env) = function
       | LAbs (x,t) ->
	   let x' = generate_var_name x (l_env, env) in
	     unfold_labs ((level,x')::acc) (level+1) ((level,x')::l_env,env) t
       | t -> acc,level,t

     let rec unfold_abs acc level (l_env, env) = function
       | Abs (x,t) -> 
	   let x' = generate_var_name x (l_env, env) in
	     unfold_abs ((level,x')::acc) (level+1) (l_env,(level,x')::env) t
       | t -> acc,level,t

     let rec unfold_app acc = function
       | App (t1,t2) -> unfold_app (t2::acc) t1
       | t -> acc,t
	
     let is_binder id id_to_sym =
       match id_to_sym id with
	 | Abstract_syntax.Binder,_ -> true
	 | _ -> false

     let is_infix id id_to_sym =
       match id_to_sym id with
	 | Abstract_syntax.Infix _ ,_ -> true
	 | _ -> false

     let is_prefix id id_to_sym =
       match id_to_sym id with
	 | (Abstract_syntax.Prefix|Abstract_syntax.Default),_ -> true
	 | _ -> false


     let rec unfold_binder binder l_level level id_to_sym acc (l_env, env) = function
       | App (Const i,LAbs(x,u)) when (is_binder i id_to_sym)&&(i=binder) ->
	   let x' = generate_var_name x (l_env, env) in
	     unfold_binder binder (l_level+1) level id_to_sym ((l_level,(x',Abstract_syntax.Linear))::acc) ((l_level,x')::l_env,env) u
       | App (Const i,Abs(x,u)) when (is_binder i id_to_sym)&&(i=binder) -> 
	   let x' = generate_var_name x (l_env, env) in
	     unfold_binder binder l_level (level+1) id_to_sym ((level,(x',Abstract_syntax.Non_linear))::acc) (l_env,(level,x')::env) u
       | t -> acc,l_level,level,t
	   
     let parenthesize (s,b) = match b with
       | true -> s
       | false -> Printf.sprintf "(%s)" s




     let left_paren = function
       | true -> "("
       | false -> ""

     let right_paren = function
       | true -> ")"
       | false -> ""



     let type_to_string ty id_to_sym =
       let rec type_to_string_aux ty =
	   match ty with
	     | Atom i -> snd (id_to_sym i),true
	     | DAtom i -> snd (id_to_sym i),true
	     | LFun (ty1,ty2) ->
		 Printf.sprintf "%s -> %s"
		   (parenthesize (type_to_string_aux ty1))
		   (fst (type_to_string_aux ty2)),
		 false
	     | Fun (ty1,ty2) ->
		 Printf.sprintf "%s => %s"
		   (parenthesize (type_to_string_aux ty1))
		   (fst (type_to_string_aux ty2)),
		 false
	     | _ -> failwith "Not yet implemented" in
	 fst (type_to_string_aux ty)

     let kind_to_string k id_to_sym =
       let rec kind_to_string_aux = function
	 | Type -> "type"
	 | Depend (ty,k') -> 
	     let k_str = kind_to_string_aux k' in
	       Printf.sprintf "(%s)%s" (type_to_string ty id_to_sym) k_str in
	 kind_to_string_aux k



     let type_to_formatted_string fmter ty id_to_sym =
       let rec type_to_string_aux ty paren =
	   match ty with
	     | Atom i -> Utils.fformat fmter "@[%s@]" (snd (id_to_sym i))
	     | DAtom i -> Utils.fformat fmter "@[%s@]" (snd (id_to_sym i))
	     | LFun (ty1,ty2) ->
	       let () = Utils.fformat fmter "@[<2>@[%s" (left_paren paren) in
	       let () = type_to_string_aux ty1 true in
	       let () = Utils.fformat fmter " ->@[<2>@ @[<2>@[" in
	       let () = type_to_string_aux ty2 true in
	       Utils.fformat fmter "@]@]@]@,%s@]@]" (right_paren paren)
	     | Fun (ty1,ty2) ->
	       let () = Utils.fformat fmter "@[<2>%s@[" (left_paren paren) in
	       let () = type_to_string_aux ty1 true in
	       let () = Utils.fformat fmter " =>@[<2>@ @[<2>@[" in
	       let () = type_to_string_aux ty2 true in
	       Utils.fformat fmter "@]@]@]@,%s@]@]" (right_paren paren)
	     | _ -> failwith "Not yet implemented" in
       let () = type_to_string_aux ty false in
       ()
(*       Utils.fformat fmter "@]" *)
       
       

     let kind_to_formatted_string fmter k id_to_sym =
       let rec kind_to_string_aux = function
	 | Type -> Utils.fformat fmter "@[type@]"
	 | Depend (ty,k') -> 
	   let () = Utils.fformat fmter "@[(" in
	   let () = type_to_formatted_string fmter ty id_to_sym in
	   let () = Utils.fformat fmter ")@]" in
	   kind_to_string_aux k' in
	 kind_to_string_aux k
		   




     let term_to_formatted_string fmter t id_to_sym =
       let rec term_to_string_aux t paren l_level level (l_env,env) =
	 match t with
	   | Var i -> Utils.fformat fmter "@[%s@]" (List.assoc (level - 1  - i) env)
	   | LVar i -> Utils.fformat fmter "@[%s@]" (List.assoc (l_level - 1  - i) l_env)
	   | Const i -> 
	     let _,x = id_to_sym i in
	     Utils.fformat fmter "@[%s@]" x
	   | DConst i ->
	     let _,x = id_to_sym i in
	     Utils.fformat fmter "@[%s@]" x
	   | Abs (x,t) ->
	     let x' = generate_var_name x (l_env, env) in
	     let vars,l,u=unfold_abs [level,x'] (level+1) (l_env,(level,x')::env) t in
	     let () = Utils.fformat fmter "@[@[%s@[<3>Lambda " (left_paren paren) in
	     let () = Utils.format_of_list fmter " " (fun (_,x) -> x) (List.rev vars) in
	     let () = Utils.fformat fmter ".@ @[@[" in
	     let _ = term_to_string_aux u false l_level l (l_env,vars@env) in
	     Utils.fformat fmter "@]@]@]@,%s@]@]" (right_paren paren)
	   | LAbs (x,t) ->
	     let x' = generate_var_name x (l_env, env) in
	     let vars,l,u=unfold_labs [l_level,x'] (l_level+1) ((l_level,x')::l_env,env) t in
	     let () = Utils.fformat fmter "@[@[%s@[<3>lambda " (left_paren paren) in
	     let () = Utils.format_of_list fmter " " (fun (_,x) -> x) (List.rev vars) in
	     let () = Utils.fformat fmter ".@ @[@[" in
	     let () = term_to_string_aux u false l level ((vars@l_env),env) in
	     Utils.fformat fmter "@]@]@]@,%s@]@]" (right_paren paren)
	   | App((Const s|DConst s),Abs(x,u)) when is_binder s id_to_sym ->
	     let x' = generate_var_name x (l_env, env) in
	     let vars,l_l,l,u = unfold_binder s l_level (level+1) id_to_sym [level,(x',Abstract_syntax.Non_linear)] (l_env,(level,x')::env) u in
	     let new_env=
	       List.fold_right
		 (fun  (l,(x,abs)) (l_acc,acc) ->
		   match abs with
		   | Abstract_syntax.Non_linear -> l_acc,(l,x)::acc
		   | Abstract_syntax.Linear -> (l,x)::l_acc,acc)
		 vars
		 (l_env,env) in
	     let () = Utils.fformat fmter "@[@[%s@[<3>%s " (left_paren paren) (let _,const = id_to_sym s in const) in
	     let () = Utils.format_of_list fmter " " (fun (_,(x,_)) -> x) (List.rev vars) in
	     let () = Utils.fformat fmter ".@ @[@[" in
	     let _ = term_to_string_aux u false l_l l new_env in
	     Utils.fformat fmter "@]@]@]@,%s@]@]" (right_paren paren)
	   | App((Const s|DConst s),LAbs(x,u)) when is_binder s id_to_sym ->
	     let x' = generate_var_name x (l_env, env) in
	     let vars,l_l,l,u = unfold_binder s (l_level+1) level id_to_sym [l_level,(x',Abstract_syntax.Linear)] ((l_level,x')::l_env,env) u in
	     let new_env=
	       List.fold_right
		 (fun  (l,(x,abs)) (l_acc,acc) ->
		   match abs with
		   | Abstract_syntax.Non_linear -> l_acc,(l,x)::acc
		   | Abstract_syntax.Linear -> (l,x)::l_acc,acc)
		 vars
		 (l_env,env) in
	     let () = Utils.fformat fmter "@[@[%s@[<3>%s " (left_paren paren) (let _,const = id_to_sym s in const) in
	     let () = Utils.format_of_list fmter " " (fun (_,(x,_)) -> x) (List.rev vars) in
	     let () = Utils.fformat fmter ".@ @[@[" in
	     let _ = term_to_string_aux u false l_l l new_env in
	     Utils.fformat fmter "@]@]@]@,%s@]@]" (right_paren paren)
	   | App(App((Const s|DConst s),t1),t2) when is_infix s id_to_sym ->
	     let () = Utils.fformat fmter "@[<2>@[%s@[" (left_paren paren) in
	     let () = term_to_string_aux t1 true l_level level (l_env,env) in
	     let () = Utils.fformat fmter "@]@ %s@ @[<2>@[" (let _,const=id_to_sym s in const) in
	     let () = term_to_string_aux t2 true l_level level (l_env,env) in
	     Utils.fformat fmter "@]@]@,%s@]@]" (right_paren paren)
	   | App(t1,t2) ->
	     let args,t11 = unfold_app [t2] t1 in
	     let () = Utils.fformat fmter "@[@[%s@[<2>@[" (left_paren paren) in
	     let () = term_to_string_aux t11 true l_level level (l_env,env) in
	     let () = Utils.fformat fmter "@]@[" in
	     let () = 
	       List.iter
		 (fun arg -> 
		   let () = Utils.fformat fmter "@ @[" in
		   let () = term_to_string_aux arg true l_level level (l_env,env) in
		   Utils.fformat fmter "@]")
		 args in
	     Utils.fformat fmter "@]@]@,%s@]@]" (right_paren paren)
	   | _ -> failwith "Not yet implemented" in
       let () = term_to_string_aux t false 0 0 ([],[]) in
       (* FIXME: I can't see where I forgot to close this box! *)
(*       let () = Utils.fformat fmter "@]" in *)
       ()



     let term_to_string t id_to_sym =
       let rec term_to_string_aux t l_level level (l_env,env) =
	 match t with
	   | Var i -> List.assoc (level - 1  - i) env,true
	   | LVar i -> List.assoc (l_level - 1  - i) l_env,true
	   | Const i -> let _,x = id_to_sym i in x,true
	   | DConst i -> let _,x = id_to_sym i in x,true
	   | Abs (x,t) ->
	       let x' = generate_var_name x (l_env, env) in
	       let vars,l,u=unfold_abs [level,x'] (level+1) (l_env,(level,x')::env) t in
		 Printf.sprintf
		   "Lambda %s. %s"
		   (Utils.string_of_list " " (fun (_,x) -> x) (List.rev vars))
		   (let str,_ = term_to_string_aux u l_level l (l_env,(vars@env)) in str),
	       false
	   | LAbs (x,t) ->
	       let x' = generate_var_name x (l_env, env) in
	       let vars,l,u=unfold_labs [l_level,x'] (l_level+1) ((l_level,x')::l_env,env) t in
		 Printf.sprintf
		   "lambda %s. %s"
		   (Utils.string_of_list " " (fun (_,x) -> x) (List.rev vars))
		   (let str,_ = term_to_string_aux u l level ((vars@l_env),env) in str),
	       false
	   | App((Const s|DConst s),Abs(x,u)) when is_binder s id_to_sym ->
	       let x' = generate_var_name x (l_env, env) in
	       let vars,l_l,l,u = unfold_binder s l_level (level+1) id_to_sym [level,(x',Abstract_syntax.Non_linear)] (l_env,(level,x')::env) u in
	       let new_env=
		 List.fold_right
		   (fun  (l,(x,abs)) (l_acc,acc) ->
		      match abs with
			| Abstract_syntax.Non_linear -> l_acc,(l,x)::acc
			| Abstract_syntax.Linear -> (l,x)::l_acc,acc)
		   vars
		   (l_env,env) in
		 Printf.sprintf
		   "%s %s. %s"
		   (let _,const = id_to_sym s in const)
		   (Utils.string_of_list " " (fun (_,(x,_)) -> x) (List.rev vars))
		   (let str,_ = term_to_string_aux u l_l l new_env in str),
	       false
	   | App((Const s|DConst s),LAbs(x,u)) when is_binder s id_to_sym ->
	       let x' = generate_var_name x (l_env, env) in
	       let vars,l_l,l,u = unfold_binder s (l_level+1) level id_to_sym [l_level,(x',Abstract_syntax.Linear)] ((l_level,x')::l_env,env) u in
	       let new_env=
		 List.fold_right
		   (fun  (l,(x,abs)) (l_acc,acc) ->
		      match abs with
			| Abstract_syntax.Non_linear -> l_acc,(l,x)::acc
			| Abstract_syntax.Linear -> (l,x)::l_acc,acc)
		   vars
		   (l_env,env) in
		 Printf.sprintf
		   "%s %s. %s"
		   (let _,const = id_to_sym s in const)
		   (Utils.string_of_list " " (fun (_,(x,_)) -> x) (List.rev vars))
		   (let str,_ = term_to_string_aux u l_l l new_env in str),
	       false
	   | App(App((Const s|DConst s),t1),t2) when is_infix s id_to_sym ->
	       Printf.sprintf
		 "%s %s %s" 
		 (parenthesize (term_to_string_aux t1 l_level level (l_env,env)))
		 (let _,const=id_to_sym s in const)
		 (parenthesize (term_to_string_aux t2 l_level level (l_env,env))),
	       false
	   | App(t1,t2) ->
	       let args,t11 = unfold_app [t2] t1 in
	       Printf.sprintf
		 "%s %s"
		 (parenthesize (term_to_string_aux t11 l_level level (l_env,env)))
		 (Utils.string_of_list " " (fun x -> parenthesize (term_to_string_aux x l_level level (l_env,env))) args),false 
	   | _ -> failwith "Not yet implemented" in
       let s = fst (term_to_string_aux t 0 0 ([],[])) in
       s


    let rec raw_to_string_aux = function
      | Var i  -> Printf.sprintf "(nl: %d)" i,true
      | LVar i -> Printf.sprintf "(l:%d)" i,true
      | (Const i 
	| DConst i)-> Printf.sprintf "[%d]" i,true
      | Abs (_,t) -> Printf.sprintf "Lambda.%s" (fst (raw_to_string_aux t)),false
      | LAbs (_,t) -> Printf.sprintf "lambda.%s" (fst (raw_to_string_aux t)),false
      | App (t,u) -> Printf.sprintf "%s %s" (parenthesize (raw_to_string_aux t)) (parenthesize (raw_to_string_aux u)),false	  
      | _ -> raise Not_yet_implemented

    let raw_to_string t = fst (raw_to_string_aux t)

    let rec raw_to_caml = function
      | Var i  -> Printf.sprintf "(Var %d)" i
      | LVar i -> Printf.sprintf "(LVar %d)" i
      | Const i -> Printf.sprintf "(Const %d)" i
      | DConst i-> Printf.sprintf "(DConst %d)" i
      | Abs (x,t) -> Printf.sprintf "(Abs (\"%s\",%s))" x (raw_to_caml t)
      | LAbs (x,t) -> Printf.sprintf "(LAbs (\"%s\",%s))" x (raw_to_caml t)
      | App (t,u) -> Printf.sprintf "(App (%s,%s))" (raw_to_caml t) (raw_to_caml u)
      | _ -> raise Not_yet_implemented
	

    let rec raw_type_to_string_aux = function
      | Atom i -> Printf.sprintf "(%d)" i,true
      | DAtom i -> Printf.sprintf "[%d]" i,true
      | LFun (alpha,beta) -> Printf.sprintf "%s -> %s" (parenthesize (raw_type_to_string_aux alpha)) (parenthesize (raw_type_to_string_aux beta)),false
      | Fun (alpha,beta) -> Printf.sprintf "%s => %s" (parenthesize (raw_type_to_string_aux alpha)) (fst (raw_type_to_string_aux beta)),false
      | _ -> failwith "Bug: Not yet implemented"

    let raw_type_to_string t = fst (raw_type_to_string_aux t)

    let rec raw_type_to_caml = function
      | Atom i -> Printf.sprintf "(Atom %d)" i
      | DAtom i -> Printf.sprintf "(DAtom %d)" i
      | LFun (alpha,beta) -> Printf.sprintf "(LFun (%s,%s))" (raw_type_to_caml alpha) (raw_type_to_caml beta)
      | Fun (alpha,beta) -> Printf.sprintf "(Fun (%s,%s))" (raw_type_to_caml alpha) (raw_type_to_caml beta)
      | _ -> failwith "Bug: Not yet implemented"



    (* [is_linear tm] true if the lambda-term [tm] is such *)
    (* that "x" occurs linearly in "lambda x. tm", i.e.,   *)
    (* the linear abstraction [LAbs ("x",tm)] satisfies    *)
    (* the linearity constraint.                           *)  
   
    let is_linear tm =
      let rec lin_occur n tm =
        match tm with
          Var _        -> false
        | LVar m       -> m = n
        | Const _      -> false
        | Abs (_, t)   -> lin_occur n t
        | LAbs (_, t)  -> lin_occur (n+1) t
        | App (t1, t2) -> (lin_occur n t1) <> (lin_occur n t2)
        | _            -> raise Not_yet_implemented
      in
      lin_occur 0 tm [@@warning "-32"]

    (* [is_lclosed tm] true if the lambda-term [tm] does not *)
    (* contain any free linear variable.                     *)

    let is_lclosed tm = 
      let rec lclosed n tm =
        match tm with
          Var _        -> true
        | LVar m       -> m < n
        | Const _      -> true
        | Unknown _    -> true
        | Abs (_, t)   -> lclosed n t
        | LAbs (_, t)  -> lclosed (n+1) t
        | App (t1, t2) -> (lclosed n t1) && (lclosed n t2)
        | _            -> raise Not_yet_implemented
      in
      lclosed 0 tm [@@warning "-32"]


    (* de Bruijn's indices lifting *)

    let lift l_i nl_i tm =
      let rec lift_aux l_level nl_level tm =
        match tm with
          Var i        -> if i < nl_level
                          then tm
                          else Var (i + nl_i)
        | LVar i       -> if i < l_level
                          then tm
                          else LVar (i + l_i)
        | Const _      -> tm
        | Unknown _    -> tm
        | Abs (x, t)   -> Abs (x, lift_aux l_level (nl_level + 1) t)
        | LAbs (x, t)  -> LAbs (x, lift_aux (l_level + 1) nl_level t)
        | App (t1, t2) -> App (lift_aux l_level nl_level t1, 
                               lift_aux l_level nl_level t2)
        | _            -> raise Not_yet_implemented
      in
      lift_aux 0 0 tm

    (* substitution of a non-linear variable tm1 [x:=tm2] *)

    let var_subst tm1 tm2 =  
      let rec subst l_level nl_level tm =
        match tm with
          Var i        -> if i = nl_level
                          then lift l_level nl_level tm2
                          else if i < nl_level
                               then tm
                               else Var (i-1)
        | LVar _       -> tm
        | Const _      -> tm
        | Unknown _    -> tm
        | Abs (x, t)   -> Abs (x, subst l_level (nl_level + 1) t)
        | LAbs (x, t)  -> LAbs (x, subst (l_level + 1) nl_level t)
        | App (t1, t2) -> App (subst l_level nl_level t1, 
                               subst l_level nl_level t2)
        | _            -> raise Not_yet_implemented
      in 
      subst 0 0 tm1

    (* substitution of a linear variable tm1 [x:=tm2] *)

    let lvar_subst tm1 tm2 =  
      let rec subst l_level nl_level tm =
        match tm with
          Var _        -> tm
        | LVar i       -> if i = l_level
                          then lift l_level nl_level tm2
                          else if i < l_level
                               then tm
                               else LVar (i-1)
        | Const _      -> tm
        | Unknown _    -> tm
        | Abs (x, t)   -> Abs (x, subst l_level (nl_level + 1) t)
        | LAbs (x, t)  -> LAbs (x, subst (l_level + 1) nl_level t)
        | App (t1, t2) -> App (subst l_level nl_level t1, 
                               subst l_level nl_level t2)
        | _            -> raise Not_yet_implemented
      in 
      subst 0 0 tm1

    (* substitution of a term in a type "ty [x:=tm]" *)
    (* tm cannot contain any free linear variable    *)

    let subst_in_type ty tm =
      let rec subst_tm level tm1 =
        match tm1 with
          Var i        -> if i = level
                          then lift 0 level tm
                          else if i < level
                               then tm
                               else Var (i-1)
        | LVar _       -> tm
        | Const _      -> tm
        | Unknown _    -> tm
        | Abs (x, t)   -> Abs (x, subst_tm (level + 1) t)
        | LAbs (x, t)  -> LAbs (x, subst_tm level t)
        | App (t1, t2) -> App (subst_tm level t1, subst_tm level t2)
        | _            -> raise Not_yet_implemented
      in
      let rec subst_ty level ty =
        match ty with
          Atom _              -> ty
        | LFun (ty1, ty2)     -> LFun (subst_ty level ty1, subst_ty level ty2)
        | Fun (ty1, ty2)     -> Fun (subst_ty level ty1, subst_ty level ty2)
        | Dprod (x, ty1, ty2) -> Dprod (x, 
                                        subst_ty level ty1, 
                                        subst_ty (level+1) ty2)
        | TApp (ty1, tm)      -> TApp (subst_ty level ty1, subst_tm level tm)
        | _                   -> raise Not_yet_implemented
      in
      subst_ty 0 ty

     (* [is_vacuous ty] true when "ty" deos not effectively depend on "x" *)
     (* in the dependent type "Dprod (x, t, ty)"                          *)

     let is_vacuous ty =
       let rec vacuous_tm n tm =
         match tm with
           Var i        -> i <> n 
         | LVar _       -> true
         | Const _      -> true
         | Unknown _    -> true
         | Abs (_, t)   -> vacuous_tm (n+1) t
         | LAbs (_, t)  -> vacuous_tm n t
         | App (t1, t2) -> (vacuous_tm n t1) && (vacuous_tm n t2)
         | _            -> raise Not_yet_implemented
       in
       let rec vacuous_ty n ty =
         match ty with
           Atom _              -> true
         | LFun (ty1, ty2)     -> (vacuous_ty n ty1) && (vacuous_ty n ty2)
         | Fun (ty1, ty2)     -> (vacuous_ty n ty1) && (vacuous_ty n ty2)
         | Dprod (_, ty1, ty2) -> (vacuous_ty n ty1) && (vacuous_ty (n+1) ty2)
         | TApp (ty1, tm)      -> (vacuous_ty n ty1) && (vacuous_tm n tm)
         | _                   -> raise Not_yet_implemented
       in
       vacuous_ty 0 ty [@@warning "-32"]


     (* beta-normalization *)

     let rec head_normalize ?id_to_term tm =
       match tm with
         Var _        -> tm
       | LVar _       -> tm
       | Const _      -> tm
       | DConst i     -> (match id_to_term with
			    | None -> tm
			    | Some f -> head_normalize ?id_to_term (f i))
       | Unknown _    -> tm
       | Abs (x, t1)  -> Abs (x, head_normalize ?id_to_term t1)
       | LAbs (x, t1) -> LAbs (x, head_normalize ?id_to_term t1)
       | App (t1, t2) -> (match head_normalize ?id_to_term t1 with
                           Abs (_, t)  -> head_normalize ?id_to_term (var_subst t t2)
                         | LAbs (_, t) -> head_normalize ?id_to_term (lvar_subst t t2)
                         | nt1         -> App (nt1, t2))
       | _            -> raise Not_yet_implemented

     let rec normalize ?id_to_term tm =
       match tm with
         Var _        -> tm
       | LVar _       -> tm
       | Const _      -> tm
       | DConst i     -> (match id_to_term with
			    | None -> tm
			    | Some f -> normalize ?id_to_term (f i))
       | Unknown _    -> tm
       | Abs (x, t)   -> Abs (x, normalize ?id_to_term t)
       | LAbs (x, t)  -> LAbs (x, normalize ?id_to_term t)
       | App (t1, t2) -> let nt2 = normalize ?id_to_term t2
                         in
                         (match normalize ?id_to_term t1 with
                            Abs (_, t)  -> normalize ?id_to_term (var_subst t nt2)
                          | LAbs (_, t) -> normalize ?id_to_term (lvar_subst t nt2)
                          | nt1         -> App (nt1, nt2))
       | _            -> raise Not_yet_implemented


     (* beta-equivalence *)

     let beta_convert tm1 tm2 =
       let rec convert tm1 tm2 =
         match (tm1, tm2) with
           (Var i, Var j)                       -> i = j
         | (LVar i, LVar j)                     -> i = j 
         | (Const i, Const j)                   -> i = j
         | (Unknown i, Unknown j)               -> i = j
         | (Abs (_, tm11), Abs (_, tm12))       -> convert tm11 tm12
         | (LAbs (_, tm11), LAbs (_, tm12))    -> convert tm11 tm12
         | (App (tm11, tm12), App (tm21, tm22)) -> (convert tm11 tm21) &&
                        (convert (head_normalize tm12) (head_normalize tm22))
         | _                                    -> false
       in
       convert (head_normalize tm1) (head_normalize tm2)

     (* type-normalization *)

     let rec type_normalize ty = 
       match ty with
        Atom _              -> ty
      | LFun (ty1, ty2)     -> LFun (type_normalize ty1, type_normalize ty2) 
      | Fun (ty1, ty2)      -> Fun (type_normalize ty1, type_normalize ty2) 
      | Dprod (x, ty1, ty2) -> Dprod (x, type_normalize ty1,
                                         type_normalize ty2)
      | TAbs (x, ty1)       -> TAbs (x, type_normalize ty1)
      | TApp (ty1, tm)      -> (match type_normalize ty1 with
                                  TAbs (_, nty1) -> subst_in_type nty1 tm
                                | nty1           -> TApp (nty1, tm))
      | _                   -> raise Not_yet_implemented

     (* type beta-equivalence *)

     let type_convert ty1 ty2 =
       let rec convert ty1 ty2 =
         match (ty1, ty2) with
         (Atom i, Atom j) 
           -> i = j
       | (LFun (ty11, ty12), LFun (ty21, ty22)) 
           -> (convert ty11 ty21) && (convert ty12 ty22)
       | (Fun (ty11, ty12), Fun (ty21, ty22)) 
           -> (convert ty11 ty21) && (convert ty12 ty22)
       | (Dprod (_, ty11, ty12), Dprod (_, ty21, ty22)) 
           -> (convert ty11 ty21) && (convert ty12 ty22)
       | (TAbs (_, ty11), TAbs (_, ty21))
           -> convert ty11 ty21
       | (TApp (ty11, tm1), TApp (ty21, tm2))
           -> (convert ty11 ty21) && (beta_convert tm1 tm2)
       | (_, _)
           -> false
       in
       convert (type_normalize ty1) (type_normalize ty2) [@@warning "-32"]


     let eta_long_form term stype f_get_type_of_constant =
       let rec eta_long_form_rec term stype ~is_functor linear_typing_env non_linear_typing_env =
	 match term,stype,is_functor with
	 | LVar i, None, is_f -> 
	   eta_long_form_rec (LVar i) (Some (List.nth linear_typing_env (i))) ~is_functor:is_f linear_typing_env non_linear_typing_env
	 | LVar i , Some (Atom _ as ty) , false ->
	     let () = assert (ty = List.nth linear_typing_env (i)) in
	     LVar (i),ty
	     
	 | LVar i , Some (LFun (_a,_b) as ty) ,true ->
	   let () = assert (ty = List.nth linear_typing_env (i))  in
	   LVar (i),ty
	     
	 | LVar i , Some (LFun (a,b) as ty),false ->
	   let () = assert (ty = List.nth linear_typing_env (i)) in
	   let new_var,_ = eta_long_form_rec (LVar 0) (Some a) ~is_functor:false [a] [] in
	   let res,_ = eta_long_form_rec (App(LVar (i+1),new_var)) (Some b) ~is_functor:false (a::linear_typing_env) non_linear_typing_env in
	   LAbs ("x",res),ty
	     
	 | LVar i , Some (Fun (a,b) as ty), true -> 
	   let () = assert (Fun(a,b) = List.nth linear_typing_env (i)) in
	   LVar (i),ty
	     
	 | LVar i , Some (Fun (a,b) as ty), false ->
	   let () = assert (Fun(a,b) = List.nth linear_typing_env (i)) in
	   let new_var,_ = eta_long_form_rec (Var 0) (Some a) ~is_functor:false [] [a] in
	   let res,_ = eta_long_form_rec (App(LVar i,new_var)) (Some b) ~is_functor:false linear_typing_env (a::non_linear_typing_env) in
	   Abs ("x",res),ty



	 | Var i, None, is_f -> 
	   eta_long_form_rec (Var i) (Some (List.nth non_linear_typing_env (i))) ~is_functor:is_f linear_typing_env non_linear_typing_env

	 | Var i , Some (Atom j as ty) , false -> 
	   let () = assert (Atom j = List.nth non_linear_typing_env (i)) in
	   Var (i),ty

	 | Var i , Some (LFun (a,b) as ty), true ->
	   let () = assert (LFun (a,b) = List.nth non_linear_typing_env (i)) in
	   Var (i),ty

	 | Var i , Some (LFun (a,b) as ty), false ->
	   let () = assert (LFun(a,b) = List.nth non_linear_typing_env (i)) in
	   let new_var,_ = eta_long_form_rec (LVar 0) (Some a) ~is_functor:false [a] [] in
	   let res,_=eta_long_form_rec (App(Var i,new_var))  (Some b) ~is_functor:false (a::linear_typing_env) non_linear_typing_env in
	   LAbs ("x",res),ty

	 | Var i , Some (Fun (a,b) as ty), true ->
	   let () = assert (Fun(a,b) = List.nth non_linear_typing_env (i)) in
	   Var (i),ty

	 | Var i , Some (Fun (a,b) as ty), false ->
	   let () = assert (Fun(a,b) = List.nth non_linear_typing_env (i)) in
	   let new_var,_ = eta_long_form_rec (Var 0) (Some a) ~is_functor:false [] [a] in
	   let res,_=eta_long_form_rec (App(Var (i+1),new_var)) (Some b) ~is_functor:false  linear_typing_env (a::non_linear_typing_env) in
	   Abs ("x",res),ty



	 | Const i,None,true -> term, f_get_type_of_constant i 
	 | Const i,None,false ->
	   eta_long_form_rec term (Some (f_get_type_of_constant i)) ~is_functor:false linear_typing_env non_linear_typing_env
	     
	 | Const _, Some (Atom _ as ty), false  -> term,ty
	 | Const _, Some (LFun (_a,_b) as ty), true -> term,ty
	 | Const _, Some (Fun (_a,_b) as ty), true -> term,ty
	 | Const _, Some (LFun (a,b) as ty), false -> 
	   let new_var,_ = eta_long_form_rec (LVar 0) (Some a) ~is_functor:false [a] [] in
	   let term = lift 1 0 term in
	   let res,_ = eta_long_form_rec (App(term,new_var)) (Some b) ~is_functor:false (a::linear_typing_env) non_linear_typing_env in
	   LAbs ("x",res),ty
	 | Const _, Some (Fun (a,b) as ty), false -> 
	   let new_var,_ = eta_long_form_rec (Var 0) (Some a) ~is_functor:false [] [a] in
	   let term = lift 0 1 term in
	   let res,_ = eta_long_form_rec (App(term,new_var)) (Some b) ~is_functor:false linear_typing_env (a::non_linear_typing_env) in
	   Abs ("x",res),ty
	     
	 | DConst _, _, _ -> failwith "All the definitions should have been unfolded"

	 | Abs (x,t), Some (Fun(a,b) as ty), false -> 
	   let t',_ = eta_long_form_rec t (Some b) ~is_functor:false linear_typing_env (a::non_linear_typing_env) in
	   Abs(x,t'),ty

	 | Abs _,None,_ -> failwith "The Term should be in normal form"

	 | Abs (_x,_t), _, false -> failwith "Bad typing"

	 | Abs (_x,_t), _, true -> failwith "The Term should be in normal form"

	 | LAbs (x,t), Some (LFun(a,b) as ty), false -> 
	   let t',_ = eta_long_form_rec t (Some b) ~is_functor:false (a::linear_typing_env) non_linear_typing_env in
	   LAbs(x,t'),ty

	 | LAbs _,None,_ -> failwith "The Term should be in normal form"

	 | LAbs (_x,_t), _, true -> failwith "The Term should be in normal form"

	 | LAbs (_x,_t), _, _ -> failwith "Bad typing"

	 | App (u,v), Some (Atom _ as ty), _ ->
	   let u',u_type = eta_long_form_rec u None ~is_functor:true linear_typing_env non_linear_typing_env in
	   (match u_type with
	   | (LFun (a,b)|Fun (a,b)) ->
	     let () = assert (b=ty) in
	     let v',_v_type = eta_long_form_rec v (Some a) ~is_functor:false linear_typing_env non_linear_typing_env  in
	     App (u',v'), b
	   | _ -> failwith "Should be well typed 1")

	 | App (u,v), Some (Fun (_,_) as ty), true ->
	   let u',u_type = eta_long_form_rec u None ~is_functor:true linear_typing_env non_linear_typing_env in
	   (match u_type with
	   | (LFun (a,b)|Fun (a,b)) ->
	     let () = assert (b=ty) in
	     let v',_v_type = eta_long_form_rec v (Some a) ~is_functor:false linear_typing_env non_linear_typing_env  in
	     App (u',v'), b
	   | _ -> failwith "Should be well typed 2")

	 | App (u,v), Some (Fun (a',b') as ty), false ->
	   let var',_= eta_long_form_rec (Var 0) (Some a') ~is_functor:false [] [a'] in
	   let u = lift 0 1 u in
	   let u',u_type = eta_long_form_rec u None ~is_functor:true linear_typing_env (a'::non_linear_typing_env) in
	   (match u_type with
	   | (LFun (a,b)|Fun (a,b)) ->
	     let () = assert (b=ty) in
	     let v = lift 0 1 v in
	     let v',_v_type = eta_long_form_rec v (Some a) ~is_functor:false linear_typing_env (a'::non_linear_typing_env)  in
	     let res,_=eta_long_form_rec (App (App (u',v'),var')) (Some b') ~is_functor:false linear_typing_env (a'::non_linear_typing_env) in
	     Abs("x",res), b
	   | _ -> failwith "Should be well typed 3")


	 | App (u,v), Some (LFun (_,_) as ty), true ->
	   let u',u_type = eta_long_form_rec u None ~is_functor:true linear_typing_env non_linear_typing_env in
	   (match u_type with
	   | (LFun (a,b)|Fun (a,b)) ->
	     let () = assert (b=ty) in
	     let v',_v_type = eta_long_form_rec v (Some a) ~is_functor:false linear_typing_env non_linear_typing_env  in
	     App (u',v'), b
	   | _ -> failwith "Should be well typed 4")

	 | App (u,v), Some (LFun (a',b') as ty), false ->
	   let var',_= eta_long_form_rec (LVar 0) (Some a') ~is_functor:false [a'] [] in
	   let u = lift 1 0 u in
	   let u',u_type = eta_long_form_rec u None ~is_functor:true (a'::linear_typing_env) non_linear_typing_env in
	   (match u_type with
	   | (LFun (a,b)|Fun (a,b)) ->
	     let () = assert (b=ty) in
	     let v = lift 1 0 v in
	     let v',_v_type = eta_long_form_rec v (Some a) ~is_functor:false (a'::linear_typing_env) non_linear_typing_env  in
	     let res,_ = eta_long_form_rec (App (App (u',v'),var')) (Some b') ~is_functor:false  (a'::linear_typing_env) non_linear_typing_env in
	     LAbs("x",res), b
	   | _ -> failwith "Should be well typed 5")
	     

	 | App (u,v), None , true ->
	   let u',u_type = eta_long_form_rec u None ~is_functor:true linear_typing_env non_linear_typing_env in
	   (match u_type with
	   | (LFun (a,b)|Fun (a,b)) ->
	     let v',_v_type = eta_long_form_rec v (Some a) ~is_functor:false linear_typing_env non_linear_typing_env  in
	     App (u',v'), b
	   | _ -> failwith "Should be well typed 6")

	 | App (_u,_v), None, false -> failwith "Probably a bug: the term cannot be a in a non functor position and an unknown type"

	   	   
	 |  _, Some (DAtom _) , _ -> failwith "type definitions should have been unfolded" 
	 | LVar _ , Some ty ,b -> failwith (Printf.sprintf "LVar Term should be well typed. Type: %s. Is_functor: %B" (raw_type_to_string ty) b)
	 | Var _ , _ , _  -> failwith "Var Term should be well typed"

	 | _ -> raise Not_yet_implemented in
       let term',_=eta_long_form_rec term (Some stype) ~is_functor:false [] [] in
       term'
	   
	   
	   
	   
	   
	   
	   






       


     (* We assume here that types in [ty] have been unfolded*)
     let rec order stype f_unfold_defined_type = 
       match stype with
       | Atom _ -> 1
       | DAtom i -> order (f_unfold_defined_type i) f_unfold_defined_type
       | LFun (alpha,beta) -> max ((order alpha f_unfold_defined_type)+1) (order beta f_unfold_defined_type)
       | Fun (alpha,beta) -> max ((order alpha f_unfold_defined_type)+1) (order beta f_unfold_defined_type)
       | _ -> failwith "Bug: order of type not defined for this type constructor"


     let is_2nd_order stype f_unfold_defined_type = 
       (order stype f_unfold_defined_type)<=2

     let rec unlinearize_term = function
       | Var i -> Var i
       | LVar i -> Var i
       | Const i -> Const i
       | DConst i -> DConst i
       | Abs (x,t) -> Abs(x,unlinearize_term t)
       | LAbs (x,t) -> Abs(x,unlinearize_term t)
       | App (t,u) -> App (unlinearize_term t,unlinearize_term u)
       | _ -> failwith "Unlinearization not implemented for this term"

     let rec unlinearize_type = function
       | Atom i -> Atom i
       | DAtom i -> DAtom i
       | LFun (ty1,ty2) -> Fun (unlinearize_type ty1,unlinearize_type ty2)
       | Fun  (ty1,ty2) -> Fun (unlinearize_type ty1,unlinearize_type ty2)
       | _ -> failwith "Unlinearization not implemented for this type"


  end


OCaml

Innovation. Community. Security.