Commit 09a3d39d authored by POGODALLA Sylvain's avatar POGODALLA Sylvain
Browse files

code fix to remove warnerrors during dev build

parent 2541d5f5
......@@ -30,15 +30,14 @@ struct
exception Duplicate_type_interpretation
exception Duplicate_constant_interpretation
exception Missing_interpretation of string
(* module Dico = Utils.StringMap *)
type kind =
| Type
| Cst
module Pair =
struct
type kind =
| Type
| Cst
type t = string * kind
let compare (s,k) (s',k') =
match k,k' with
......@@ -112,11 +111,11 @@ struct
| Interpret s -> Signatures s
| Compose l -> Lexicons l
let name {name=n}=n
let name {name=n;_} = n
let get_sig {abstract_sig=abs;object_sig=obj} = abs,obj
let get_sig {abstract_sig=abs;object_sig=obj;_} = abs,obj
let empty name ?(non_linear=false) ~abs ~obj =
let empty ?(non_linear=false) ~abs ~obj name =
let prog =
(* if (Sg.is_2nd_order abs) && (not non_linear) then *)
if (Sg.is_2nd_order abs) then
......@@ -137,18 +136,18 @@ struct
timestamp = Unix.time ()}
let is_linear {non_linear_interpretation} = not non_linear_interpretation
let is_linear {non_linear_interpretation;_} = not non_linear_interpretation
let emit_missing_inter lex lst =
let lex_name,loc = name lex in
let abs_name,_ = Sg.name lex.abstract_sig in
raise (Error.Error (Error.Lexicon_error (Error.Missing_interpretations(lex_name,abs_name,lst),loc)))
let rec interpret_type abs_ty ({abstract_sig=abs_sg;dico=dico} as lex) =
let rec interpret_type abs_ty ({abstract_sig=abs_sg;dico=dico;_} as lex) =
match abs_ty with
| Lambda.Atom i ->
| Lambda.Atom _ ->
(let abs_ty_as_str = Sg.type_to_string abs_ty abs_sg in
match Dico.find (abs_ty_as_str,Type) dico with
match Dico.find (abs_ty_as_str,Pair.Type) dico with
| Type (_,obj_ty) -> Sg.expand_type obj_ty lex.object_sig
| Constant _ -> failwith "Bug"
| exception Not_found -> emit_missing_inter lex [abs_ty_as_str])
......@@ -161,7 +160,7 @@ struct
| Lambda.Fun (ty1,ty2) -> Lambda.Fun (interpret_type ty1 lex,interpret_type ty2 lex)
| _ -> failwith "Not yet implemented"
let rec interpret_term abs_t ({abstract_sig=abs_sg;dico=dico} as lex) =
let rec interpret_term abs_t ({abstract_sig=abs_sg;dico=dico;_} as lex) =
match abs_t with
| Lambda.Var _ -> abs_t
| Lambda.LVar i ->
......@@ -169,9 +168,9 @@ struct
Lambda.Var i
else
abs_t
| Lambda.Const i ->
| Lambda.Const _ ->
(let abs_term_as_str = Sg.term_to_string abs_t abs_sg in
match Dico.find (abs_term_as_str,Cst) dico with
match Dico.find (abs_term_as_str,Pair.Cst) dico with
| Constant (_,obj_t) -> obj_t
| Type _ -> failwith "Bug"
| exception Not_found -> emit_missing_inter lex [abs_term_as_str] )
......@@ -241,10 +240,10 @@ struct
}
let insert e ({dico=d} as lex) = match e with
let insert e ({dico=d;_} as lex) = match e with
| Abstract_syntax.Type (id,loc,ty) ->
let interpreted_type = Sg.convert_type ty lex.object_sig in
{lex with dico=Dico.add (id,Type) (Type (loc,interpreted_type)) d}
{lex with dico=Dico.add (id,Pair.Type) (Type (loc,interpreted_type)) d}
| Abstract_syntax.Constant (id,loc,t) ->
let abs_type=Sg.expand_type (Sg.type_of_constant id lex.abstract_sig) lex.abstract_sig in
let interpreted_type = interpret_type abs_type lex in
......@@ -256,11 +255,11 @@ struct
let prog = match lex.datalog_prog with
| None -> None
| Some p ->
let duplicated_entry = Dico.mem (id,Cst) d in
let duplicated_entry = Dico.mem (id,Pair.Cst) d in
let new_prog= add_rule_for_cst_in_prog id duplicated_entry abs_type (Signature.expand_term interpreted_term lex.object_sig) lex p in
Some new_prog in
{lex with
dico=Dico.add (id,Cst) (Constant (loc,interpreted_term)) d;
dico=Dico.add (id,Pair.Cst) (Constant (loc,interpreted_term)) d;
datalog_prog =prog}
let rebuild_prog lex =
......@@ -271,8 +270,8 @@ struct
Dico.fold
(fun (id,_) inter acc ->
match inter with
| Type (l,stype) -> acc
| Constant (l,t) ->
| Type (_,_) -> acc
| Constant (_,t) ->
add_rule_for_cst_in_prog
id
false (* When rebuilding, no risk of dublicated interpretations *)
......@@ -291,7 +290,7 @@ struct
| None,_ ->
let () = Logs.warn (fun m -> m "Parsing is not implemented for non 2nd order ACG.") in
SharedForest.SharedForest.empty
| Some {prog}, (Lambda.Atom _ as dist_type) ->
| Some {prog;_}, (Lambda.Atom _ as dist_type) ->
Log.info (fun m -> m "Before parsing. Program is currently:");
DatalogAbstractSyntax.Program.log_content Logs.Info (Datalog.Program.to_abstract prog) ;
Log.info (fun m -> m "That's all.");
......@@ -322,7 +321,7 @@ struct
Log.info (fun m -> m "Going to solve the query: \"%s\" with the program:" (DatalogAbstractSyntax.Predicate.to_string query temp_prog.Datalog.Program.pred_table temp_prog.Datalog.Program.const_table));
DatalogAbstractSyntax.Program.log_content Logs.Debug (Datalog.Program.to_abstract temp_prog);
let starting_parse_time = Sys.time () in
let derived_facts,derivations = Datalog.Program.seminaive temp_prog in
let _,derivations = Datalog.Program.seminaive temp_prog in
let ending_parse_time = Sys.time () in
let parse_forest = Datalog.Program.build_forest ~query:query derivations temp_prog in
let ending_building_forest_time = Sys.time () in
......@@ -347,7 +346,7 @@ struct
Log.debug (fun m -> m "Trying to get some analysis");
match lex.datalog_prog with
| None -> let () = Logs.warn (fun m -> m "Parsing is not yet implemented for non atomic distinguished type") in None,resume
| Some {rule_to_cst=rule_id_to_cst} ->
| Some {rule_to_cst=rule_id_to_cst;_} ->
match SharedForest.SharedForest.resumption resume with
| None,resume -> None,resume
| Some t,resume ->
......@@ -360,7 +359,7 @@ struct
let is_empty = SharedForest.SharedForest.is_empty
let to_string ({name=n,_;dico=d;abstract_sig=abs_sg;object_sig=obj_sg} as lex) =
let to_string ({name=n,_;dico=d;abstract_sig=abs_sg;object_sig=obj_sg;_} as lex) =
let buff=Buffer.create 80 in
let () = Printf.bprintf
buff
......@@ -382,12 +381,12 @@ struct
let () = match lex.datalog_prog with
| None -> Printf.bprintf buff "This lexicon was not recognized as having a 2nd order abstract signature\n"
(* | Some (p,_) -> *)
| Some {prog=p} ->
| Some {prog=p;_} ->
let () = Printf.bprintf buff "This lexicon recognized as having a 2nd order abstract signature. The associated datalog program is:\n" in
Buffer.add_buffer buff (DatalogAbstractSyntax.Program.to_buffer (Datalog.Program.to_abstract p)) in
Buffer.contents buff
let check ({dico=d;abstract_sig=abs} as lex) =
let check ({dico=d;abstract_sig=abs;_} as lex) =
let missing_interpretations =
Signature.fold
(fun e acc ->
......@@ -395,12 +394,12 @@ struct
| Some s ->
(match Sg.entry_to_data e with
| Sg.Type _ ->
if Dico.mem (s,Type) d then
if Dico.mem (s,Pair.Type) d then
acc
else
s::acc
| Sg.Term _ ->
if Dico.mem (s,Cst) d then
if Dico.mem (s,Pair.Cst) d then
acc
else
s::acc)
......@@ -431,6 +430,7 @@ struct
dico=Dico.empty;
datalog_prog=prog}in
{new_lex with timestamp=Unix.time ()}
[@@warning "-32"]
let compose lex1 lex2 n =
Log.info (fun m -> m "Compose %s(%s) as %s" (fst(name lex1)) (fst(name lex2)) (fst n));
......@@ -458,7 +458,7 @@ struct
let () = match lex.datalog_prog with
| None -> Printf.bprintf buff "This lexicon was not recognized as having a 2nd order abstract signature\n"
(* | Some (p,_) -> *)
| Some {prog=p} ->
| Some {prog=p;_} ->
let () = Printf.bprintf buff "This lexicon recognized as having a 2nd order abstract signature. The associated datalog program is:\n" in
Buffer.add_buffer buff (DatalogAbstractSyntax.Program.to_buffer (Datalog.Program.to_abstract p)) in
buff
......@@ -466,7 +466,7 @@ struct
let program_to_log src level lex =
match lex.datalog_prog with
| None -> Logs.msg ~src Logs.Warning (fun m -> m "This lexicon was not recognized as having a 2nd order abstract signature" )
| Some {prog=p} ->
| Some {prog=p;_} ->
let () = Logs.msg ~src level (fun m -> m "This lexicon is recognized as having a 2nd order abstract signature.") in
let () = Logs.msg ~src level (fun m -> m "The associated datalog program is:") in
DatalogAbstractSyntax.Program.log_content ~src level (Datalog.Program.to_abstract p)
......@@ -478,7 +478,7 @@ struct
let buff=Buffer.create 80 in
let () = Printf.bprintf buff "Parsing is not implemented for non 2nd order ACG\n!" in
buff
| Some {prog}, (Lambda.Atom _ as dist_type) ->
| Some {prog;_}, (Lambda.Atom _ as dist_type) ->
let dist_type_image = interpret_type dist_type lex in
let obj_term=
Sg.eta_long_form
......@@ -509,7 +509,7 @@ struct
let query_to_log src level term dist_type lex =
match lex.datalog_prog,Sg.expand_type dist_type lex.abstract_sig with
| None,_ -> Logs.msg ~src Logs.Warning (fun m -> m "Parsing is not implemented for non 2nd order ACG")
| Some {prog}, (Lambda.Atom _ as dist_type) ->
| Some {prog;_}, (Lambda.Atom _ as dist_type) ->
let dist_type_image = interpret_type dist_type lex in
let obj_term=
Sg.eta_long_form
......@@ -539,6 +539,8 @@ struct
(* let timestamp lex = {lex with timestamp=Unix.time ()} *)
let update lex e = failwith "Not yet implemented"
[@@warning "-27"]
end
......
......@@ -19,7 +19,6 @@
open UtilsLib
open Logic
open Abstract_syntax
open Interface
......@@ -136,7 +135,7 @@ struct
| Some (Signature _,_),Some v2,true ->
let () = erased_sig:=!erased_sig+1 in
Some v2
| Some (v1,_),Some (v2,_),false ->
| Some (_,_),Some (v2,_),false ->
match v2 with
| Signature sg ->
let _,pos=Sg.name sg in
......@@ -191,27 +190,27 @@ struct
else
raise (Error.Error (Error.Env_error (Error.Duplicated_lexicon name,(p1,p2))))
let iter f {map=e} = Env.iter (fun _ (d,_) -> f d) e
let iter f {map=e;_} = Env.iter (fun _ (d,_) -> f d) e
let fold f a {map=e} = Env.fold (fun _ (d,_) acc -> f d acc) e a
let fold f a {map=e;_} = Env.fold (fun _ (d,_) acc -> f d acc) e a
let sig_number {sig_number=n} = n
let lex_number {lex_number=n} = n
let sig_number {sig_number=n;_} = n
let lex_number {lex_number=n;_} = n
let get_signature s {map=e} =
let get_signature s {map=e;_} =
match Env.find s e with
| Signature sg,_ -> sg
| Lexicon _,_ -> raise (Signature_not_found s)
| exception Not_found -> raise (Signature_not_found s)
let get_lexicon s {map=e} =
let get_lexicon s {map=e;_} =
match Env.find s e with
| Signature _,_ -> raise (Lexicon_not_found s)
| Lexicon lex,_ -> lex
| exception Not_found -> raise (Lexicon_not_found s)
let get s {map=e} =
let get s {map=e;_} =
try
let data,_ = Env.find s e in
data
......@@ -219,7 +218,7 @@ struct
| Not_found -> raise (Entry_not_found s)
let compatible_version {version} = version = Version.version
let compatible_version {version;_} = version = Version.version
let stamp v = Printf.sprintf "acg object file version %s" v
......@@ -244,7 +243,7 @@ struct
let err = Error.System_error (Printf.sprintf "\"%s\" is not recognized as an acg object file" filename )in
let () = Printf.fprintf stderr "Error: %s\n%!" (Error.error_msg err filename) in
None
| Utils.No_file(f,msg) ->
| Utils.No_file(_,msg) ->
let err = Error.System_error (Printf.sprintf "No such file \"%s\" in %s" filename msg) in
let () = Printf.fprintf stderr "Error: %s\n%!" (Error.error_msg err filename) in
None
......@@ -253,7 +252,7 @@ let write filename env =
let () = Logs.debug (fun m -> m "The environment currently has %d signature(s) and %d lexicon(s)." (sig_number env) (lex_number env)) in
let new_env =
Env.fold
(fun k (d,dump) acc ->
(fun _ (d,dump) acc ->
if dump then
(* all data are inserted with the [false] value as [to_be_dumped] *)
insert d ~to_be_dumped:false acc
......@@ -272,13 +271,13 @@ let write filename env =
let unselect e = {e with focus=None}
let focus {focus=f} = f
let focus {focus=f;_} = f
exception Sig of Sg.t
let choose_signature {map=e} =
let choose_signature {map=e;_} =
try
let () = Env.fold
(fun _ c a ->
......
......@@ -18,7 +18,6 @@
(**************************************************************************)
open Logic
open Abstract_syntax
open Interface
......
......@@ -39,7 +39,7 @@ let set_infix l = infix_as_prefix := Some l
let unset_infix () = infix_as_prefix := None
let bad_infix_usage () = !infix_as_prefix
(*let bad_infix_usage () = !infix_as_prefix *)
type lex_error =
......
......@@ -94,7 +94,7 @@ sig
| Lexicon of t
val get_dependencies : t -> dependency
val empty : (string*Abstract_syntax.location) -> ?non_linear:bool -> abs:signature -> obj:signature -> t
val empty : ?non_linear:bool -> abs:signature -> obj:signature -> (string*Abstract_syntax.location) -> t
val is_linear : t -> bool
val name : t -> (string*Abstract_syntax.location)
val insert : Abstract_syntax.lex_entry -> t -> t
......
......@@ -242,7 +242,7 @@ module type Lexicon_sig =
val get_dependencies : t -> dependency
(** [empty name] returns the empty lexicon of name [name] *)
val empty : (string*Abstract_syntax.location) -> ?non_linear:bool -> abs:signature -> obj:signature -> t
val empty : ?non_linear:bool -> abs:signature -> obj:signature -> (string*Abstract_syntax.location) -> t
(** [is_linear l] returns [true] if the lexicon [l] is linear, and [false] otherwise *)
val is_linear : t -> bool
......
......@@ -194,6 +194,6 @@ struct
let prog=Datalog.Program.add_e_facts prog (e_facts,prog.Datalog.Program.const_table,prog.Datalog.Program.rule_id_gen) in
build_predicate_w_cst_args (name,image) prog
| (_,_,_)::tl -> failwith "Bug: querying non atomic types is not yet implemented"
[@@warning "-27"]
end
......@@ -41,7 +41,7 @@ struct
exception Not_functional_type
exception Not_yet_implemented
(* exception Not_yet_implemented *)
type entry = sig_entry
......@@ -63,7 +63,7 @@ struct
| Type of stype
| Term of (term*stype)
let find_term sym {terms=syms} =
let find_term sym {terms=syms;_} =
(* TODO : Replace by an assert within IFDEFDEBUG *)
match Symbols.find sym syms with
| Term_declaration (x,id,_,const_type) when sym=x-> Lambda.Const id,const_type
......@@ -73,7 +73,7 @@ struct
| _ -> failwith "Bug in find_term" (* x should return a Term, not a type *)
| exception Symbols.Not_found -> raise Not_found
let id_to_string {ids=ids} i =
let id_to_string {ids=ids;_} i =
match Id.find i ids with
| Type_declaration(s,_,_) -> Abstract_syntax.Default,s
| Type_definition(s,_,_,_) -> Abstract_syntax.Default,s
......@@ -104,9 +104,9 @@ struct
definition_timestamp=timestamp;
extension_timestamp=timestamp}
let name {name=n} = n
let name {name=n;_} = n
let find_atomic_type s {types=syms} =
let find_atomic_type s {types=syms;_} =
(* TODO : Replace by an assert within IFDEFDEBUG *)
match Symbols.find s syms with
| Type_declaration (x,id,_) when x=s -> Lambda.Atom id
......@@ -123,13 +123,14 @@ struct
| Type_definition (x,id,_,_) when x=s -> Lambda.DAtom id
| _ -> failwith "Bug in find_type" (* A type, not a term should be returned and x and s should match *)
| exception Symbols.Not_found -> raise Not_found
[@@warning "-32"]
let rec convert_type ty ({types=syms} as sg) =
let rec convert_type ty sg =
match ty with
| Abstract_syntax.Type_atom (s,l,args) -> find_atomic_type s sg
| Abstract_syntax.Linear_arrow (ty1,ty2,l) ->
| Abstract_syntax.Type_atom (s,_,_) -> find_atomic_type s sg
| Abstract_syntax.Linear_arrow (ty1,ty2,_) ->
Lambda.LFun (convert_type ty1 sg,convert_type ty2 sg)
| Abstract_syntax.Arrow (ty1,ty2,l) -> Lambda.Fun (convert_type ty1 sg,convert_type ty2 sg)
| Abstract_syntax.Arrow (ty1,ty2,_) -> Lambda.Fun (convert_type ty1 sg,convert_type ty2 sg)
let abstract_on_dependent_types lst sg=
List.fold_right
......@@ -137,7 +138,7 @@ struct
lst
Lambda.Type
let add_sig_type t e ({size=s;types=syms;ids=ids} as sg) =
let add_sig_type t e ({size=s;types=syms;ids=ids;_} as sg) =
try
(* First perform addition on the functional data structure *)
let new_symbols = Symbols.add t e syms in
......@@ -150,7 +151,7 @@ struct
| Symbols.Conflict -> raise Duplicate_type_definition
| Id.Conflict -> raise Duplicate_type_definition
let add_sig_term t e ({size=s;terms=syms;ids=ids} as sg) =
let add_sig_term t e ({size=s;terms=syms;ids=ids;_} as sg) =
try
(* First perform addition on the functional data structure *)
let new_symbols = Symbols.add t e syms in
......@@ -161,7 +162,7 @@ struct
| Id.Conflict -> raise Duplicate_term_definition
let rec expand_type ty ({ids=ids} as sg) =
let rec expand_type ty ({ids=ids;_} as sg) =
match ty with
| Lambda.Atom _ -> ty
| Lambda.DAtom i ->
......@@ -173,7 +174,7 @@ struct
| _ -> failwith "Not yet implemented"
let rec expand_term t ({ids=ids} as sg) =
let rec expand_term t ({ids=ids;_} as sg) =
match t with
| (Lambda.Var _| Lambda.LVar _ | Lambda.Const _) -> t
| Lambda.DConst i ->
......@@ -185,27 +186,27 @@ struct
| Lambda.App (u,v) -> Lambda.App (expand_term u sg,expand_term v sg)
| _ -> failwith "Not yet implemented"
let unfold_type_definition i ({ids=ids} as sg) =
let unfold_type_definition i ({ids=ids;_} as sg) =
match Id.find i ids with
| Type_definition (_,_,_,ty1) -> expand_type ty1 sg
| _ -> failwith "Bug in unfold_type_definition"
let unfold_term_definition i ({ids=ids} as sg) =
let unfold_term_definition i ({ids=ids;_} as sg) =
match Id.find i ids with
| Term_definition (_,_,_,_,t) -> expand_term t sg
| _ -> failwith "Bug in unfold_term_definition"
let get_type_of_const_id i ({ids=ids} as sg) =
let get_type_of_const_id i ({ids=ids;_} as sg) =
match Id.find i ids with
| Term_declaration (_,_,_,ty) -> expand_type ty sg
| Term_definition (_,_,_,ty,_) -> expand_type ty sg
| _ -> failwith "Should be applied only on constants"
| exception Id.Not_found -> failwith "Bug in get_type_of_const_id"
let rec decompose_functional_type ty ({ids=ids} as sg) =
let rec decompose_functional_type ty ({ids=ids;_} as sg) =
match ty with
| Lambda.LFun (ty1,ty2) -> ty1,ty2,Abstract_syntax.Linear
| Lambda.Fun (ty1,ty2) -> ty1,ty2,Abstract_syntax.Non_linear
......@@ -216,14 +217,14 @@ struct
| _ -> raise Not_functional_type
let rec get_binder_argument_functional_type x ({terms=terms} as sg) =
let get_binder_argument_functional_type x ({terms=terms;_} as sg) =
let ty =
match Symbols.find x terms with
| Term_declaration (_,_,_,ty) -> ty
| Term_definition (_,_,_,ty,_) -> ty
| _ -> failwith (Printf.sprintf "Bug: Request of the type of the non constant \"%s\"" x) in
try
let ty1,ty2,_ = decompose_functional_type ty sg in
let ty1,_,_ = decompose_functional_type ty sg in
let _,_,lin = decompose_functional_type ty1 sg in
Some lin
with
......@@ -248,14 +249,14 @@ struct
let unfold t sg = Lambda.normalize (expand_term t sg)
type temp_t=t
type temp_entry=entry
(* type temp_entry=entry *)
module Type_System=Type_system.Type_System.Make(
struct
exception Not_found
type t=temp_t
type entry=temp_entry
type stype=Lambda.stype
(* type entry=temp_entry *)
(* type stype=Lambda.stype *)
let expand_type = expand_type
let find_term = find_term
let type_to_string = type_to_string
......@@ -268,7 +269,7 @@ struct
let stamp_definition sg = {sg with definition_timestamp = Unix.time ()}
let add_entry e ({size=s} as sg) =
let add_entry e ({size=s;_} as sg) =
match e with
| Abstract_syntax.Type_decl (t,_,Abstract_syntax.K k) ->
stamp_declaration (add_sig_type t (Type_declaration (t,s,abstract_on_dependent_types k sg)) sg)
......@@ -283,25 +284,27 @@ struct
let t_term = typecheck term t_type sg in
stamp_definition (add_sig_term t (Term_definition (t,s,behavior,t_type,t_term)) sg)
let is_type s {types=syms} =
let is_type s {types=syms;_} =
match Symbols.find s syms with
| Type_declaration _ -> true
| Type_definition _ -> true
| _ -> false
| exception Symbols.Not_found -> false
let is_constant s {terms=syms;precedence} =
let is_constant s {terms=syms;_} =
match Symbols.find s syms with
| Term_declaration (_,_,behavior,_) -> true,Some behavior
| Term_definition (_,_,behavior,_,_) -> true,Some behavior
| _ -> false,None
| exception Symbols.Not_found -> false,None
let precedence s {precedence} =
(*
let precedence s {precedence;_} =
match Symbols.find s precedence with
| f,_ -> Some f
| exception Symbols.Not_found -> None
*)
let new_precedence ?before id sg =
match before, sg.max_pred with
| None, (f, None) ->
......@@ -314,7 +317,7 @@ struct
p, {sg with
max_pred = p, Some id;
precedence = Symbols.add id (p,max) sg.precedence}
| Some upper_bound, (f, None) ->
| Some _, (f, None) ->
(* Strange to give an upper bound when there is no max. Behaves
like introducing the first element *)
let p = f +. 1. in
......@@ -344,9 +347,11 @@ struct
let add_warnings _ sg = sg
let get_warnings _ = []
[@@warning "-32"]
let raw_to_string t = Lambda.raw_to_string t
[@@warning "-32"]
let behavior_to_string = function
| Abstract_syntax.Default -> ""
......@@ -407,9 +412,10 @@ struct
let () = Lambda.type_to_formatted_string Format.str_formatter ty f in
Utils.sformat "@];@]@]" in
()
[@@warning "-32"]
let to_string ({name=n;ids=ids} as sg) =
let to_string ({name=n;ids=ids;_} as sg) =
Printf.sprintf "signature %s = \n%send\n"
(fst n)
(fst (Id.fold
......@@ -425,14 +431,14 @@ struct
let t=typecheck t t_type sg in
t,t_type